proposition: Fact sss_steps_mm_pos_nat_inv i P k st1 st2 v1 : v1 ⋈ snd st1 -> (i,@mm_pos_nat n P) /e/ st1 -[k]-> st2 -> exists v2, v2 ⋈ snd (st2) /\ (i,P) /v/ (fst st1,v1) -[k]-> (fst st2,v2).
proof: Proof. intros H1 H2; revert H2 v1 H1. induction 1 as [ (j,e) | k (j1,e1) (j2,e2) (j3,e3) H1 H2 IH2 ]; simpl; intros v1 H3. + exists v1; split; auto; constructor. + destruct H1 as (q & l & rho & r & e & [= <- G2] & [= -> <-] & G3). unfold mm_pos_nat in G2; apply map_middle_inv in G2. destruct G2 as (l' & rho' & r' & G2 & G4 & G5 & G6). subst rho l r. destruct sss_mm_pos_nat_inv with (2 := G3) (1 := H3) as (v2 & G7 & G8); simpl in *. destruct IH2 with (1 := G7) as (v3 & G9 & G10). exists v3; split; auto. constructor 2 with (st2 := (j2,v2)); auto. exists i, l', rho', r', v1; msplit 2; subst; auto; rew length; auto. Qed.
imports: List Arith Lia Max Undecidability.Shared.Libs.DLW(utils pos vec subcode sss) Undecidability.MinskyMachines(env mm_defs mme_defs mme_utils) Undecidability.MuRec.Util(recalg ra_mm_env)