proposition: Fact mm_multi_copy_compute k src dst i e : k+src <= dst -> k+dst <= tmp -> k+dst <= zero -> tmp <> zero -> e⇢tmp = 0 -> e⇢zero = 0 -> exists e', (forall j, j < k -> e'⇢(j+dst) = e⇢(j+src)) /\ (forall j, ~ dst <= j < k+dst -> e'⇢j = e⇢j) /\ (i,mm_multi_copy k src dst i) // (i,e) ->> (9*k+i,e').
proof: Proof. revert src dst i e; induction k as [ | k IHk ]; intros src dst i e; intros H1 H2 H3 H4 H5 H6. + exists e; split; [ | split ]; try (intros; lia). mm env stop. + destruct (@mm_copy_progress src dst tmp zero) with (i := i) (e := e) as (e1 & G1 & G2); try lia. destruct (IHk (S src) (S dst) (9+i)) with (e := e1) as (e2 & G3 & G4 & G5); try lia. { rewrite G1; assert (dst <> tmp); try lia; rew env. } { rewrite G1; assert (dst <> zero); try lia; rew env. } exists e2; split; [ | split ]. * intros [ | j ] Hj. - rewrite G4; try lia; simpl; rewrite G1; rew env. - replace (S j + dst) with (j+S dst) by lia. replace (S j + src) with (j+S src) by lia. rewrite G3; try lia. rewrite G1. assert (dst <> j+S src) by lia; rew env. * intros j Hj. rewrite G4; try lia. rewrite G1. assert (j <> dst) by lia; rew env. * unfold mm_multi_copy; fold mm_multi_copy. apply sss_compute_trans with (9+i,e1). - apply sss_progress_compute. revert G2; apply subcode_sss_progress; auto. - replace (9*S k+i) with (9*k+(9+i)) by lia. revert G5; apply subcode_sss_compute. subcode_tac; rewrite app_nil_r; auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils pos vec subcode sss) Undecidability.MinskyMachines.MMenv(env mme_defs)