proposition: Fact mm_mul2_progress v st : v#>dst = 0 -> v#>zero = 0 -> st = (4+i,v[0/src][(2*(v#>src))/dst]) -> (i,mm_mul2) // (i,v) -+> st.
proof: Proof. Proof using Hsz Hsd Hdz. intros H1 H2 ?; subst. apply mm_mul2_spec with (1 := eq_refl); auto. rewrite H1; f_equal; lia. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils list_bool pos vec subcode sss) Undecidability.MinskyMachines.MM(mm_defs)