proposition: Fact mm_list_erase_compute ll i e : Forall (fun x => x <> zero) ll -> e⇢zero = 0 -> exists e', (forall x, In x ll -> e'⇢x = 0) /\ (forall x, ~ In x ll -> e'⇢x = e⇢x) /\ (i,mm_list_erase ll i) // (i,e) ->> (2*length ll+i,e').
proof: Proof. intros H; revert H i e. induction 1 as [ | dst ll H1 H2 IH2 ]; intros i e H3. + simpl; exists e; repeat split; try tauto; mm env stop. + destruct mm_erase_progress with (dst := dst) (zero := zero) (i := i) (e := e) as (e1 & H4 & H5); auto. destruct IH2 with (i := 2+i) (e := e1) as (e2 & H6 & H7 & H8). { rewrite H4; rew env. } exists e2; split; [ | split ]. * intros x [ H | H ]; subst; auto. destruct in_dec with (1 := eq_nat_dec) (a := x) (l := ll) as [ H9 | H9 ]; auto. rewrite H7; auto; rewrite H4; rew env. * simpl; intros x Hx. rewrite H7, H4; try tauto. dest x dst; destruct Hx; auto. * apply sss_compute_trans with (2+i,e1). - apply sss_progress_compute. simpl; revert H5; apply subcode_sss_progress; auto. - replace (2*length (dst::ll)+i) with (2*length ll+(2+i)) by (rew length; lia). revert H8; simpl; 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)