proposition: Fact mm_copy_progress i e : e⇢tmp = 0 -> e⇢zero = 0 -> exists e', e' ⋈ e⦃dst⇠(e⇢src)⦄ /\ (i,mm_copy i) // (i,e) -+> (9+i,e').
proof: Proof. Proof using Htz Hsz Hst Hsd Hdz Hdt. intros H0 H1. unfold mm_copy. destruct mm_erase_progress with (1 := Hdz) (i := i) (e := e) as (e0 & H2 & H3); auto. destruct mm_transfert_progress with (src := src) (dst := tmp) (zero := zero) (i := 2+i) (e := e0) as (e1 & H4 & H5); auto. 1,2: rewrite H2; rew env. destruct mm_dup_progress with (src := tmp) (dst := src) (tmp := dst) (zero := zero) (i := 5+i) (e := e1) as (e2 & H6 & H7); auto. 1,2,3: rewrite H4; rew env; rewrite H2; rew env. exists e2; split. * intros j. rewrite H6; dest j dst. - rewrite H4; rew env. rewrite H2; rew env. - dest j src. + rewrite H4; rew env. rewrite H2; rew env. + dest j tmp. rewrite H4; rew env. rewrite H2; rew env. * apply sss_progress_trans with (2+i,e0). { revert H3; apply subcode_sss_progress; auto. } apply sss_progress_trans with (5+i,e1). { revert H5; apply subcode_sss_progress; auto. } { revert H7; apply subcode_sss_progress; auto. } Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils pos vec subcode sss) Undecidability.MinskyMachines.MMenv(env mme_defs)