proposition: Fact mm_dup_progress i e : e⇢dst = 0 -> e⇢tmp = 0 -> e⇢zero = 0 -> exists e', e' ⋈ e⦃src⇠0⦄⦃dst⇠(e⇢src)⦄⦃tmp⇠(e⇢src)⦄ /\ (i,mm_dup i) // (i,e) -+> (4+i,e').
proof: Proof. Proof using Htz Hsz Hst Hsd Hdz Hdt. intros H1 H2 H3. destruct mm_dup_spec with (e := e) (x := 0) (y := 0) (i := i) (k := e⇢src) as (e' & H4 & H5); auto. exists e'; split; auto. intros j; rewrite H4, Nat.add_comm; auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils pos vec subcode sss) Undecidability.MinskyMachines.MMenv(env mme_defs)