proposition: Fact mm_set_progress n i e : e⇢zero = 0 -> exists e', e' ⋈ e⦃dst⇠n⦄ /\ (i,mm_set n i) // (i,e) -+> (2+n+i,e').
proof: Proof. Proof using Hdz. intros H; unfold mm_set. destruct (@mm_erase_progress _ _ Hdz i _ H) as (e1 & H1 & H2). destruct (mm_incs_spec (2+i) e1 n) as (e2 & H3 & H4). exists e2; split. + intros j; rewrite H3, H1. dest j dst; rewrite H1; rew env. + apply sss_progress_compute_trans with (2+i,e1). * revert H2; apply subcode_sss_progress; auto. * replace (2+n+i) with (n+(2+i)) by lia. revert H4; apply subcode_sss_compute; auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils pos vec subcode sss) Undecidability.MinskyMachines.MMenv(env mme_defs)