proposition: Fact mm_multi_erase_compute i e : e⇢zero = 0 -> exists e', (forall j, dst <= j < k+dst -> e'⇢j = 0) /\ (forall j, ~ dst <= j < k+dst -> e'⇢j = e⇢j) /\ (i,mm_multi_erase i) // (i,e) ->> (2*k+i,e').
proof: Proof. Proof using Hdz. intros H; unfold mm_multi_erase. destruct mm_list_erase_compute with (zero := zero) (ll := list_an dst k) (i := i) (e := e) as (e' & H1 & H2 & H3); auto. * rewrite Forall_forall; intros j; rewrite list_an_spec; intros; lia. * rew length in H3; exists e'; msplit 2; auto. + intros; apply H1, list_an_spec; lia. + intros; apply H2; rewrite list_an_spec; lia. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils pos vec subcode sss) Undecidability.MinskyMachines.MMenv(env mme_defs)