proposition: Fact mma_mult_cst_progress v st : st = (5+k+i,v[0/src][(k*(v#>src)+(v#>dst))/dst]) -> (i,mma_mult_cst) // (i,v) -+> st.
proof: Proof. Proof using Hsd. intros ?; subst. apply mma_mult_cst_spec with (1 := eq_refl); do 2 f_equal. ring. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils list_bool gcd pos vec subcode sss) Undecidability.MinskyMachines.MMA(mma_defs)