proposition: Fact sss_steps_mm_pos_nat i P k st1 st2 e1 : snd st1 ⋈ e1 -> (i,P) /v/ st1 -[k]-> st2 -> exists e2, snd st2 ⋈ e2 /\ (i,@mm_pos_nat n P) /e/ (fst st1,e1) -[k]-> (fst st2,e2).
proof: Proof. intros H1 H2; revert H2 e1 H1. induction 1 as [ (j,v) | k (j1,v1) (j2,v2) (j3,v3) H1 H2 IH2 ]; simpl; intros e1 H3. + exists e1; split; auto; constructor. + destruct H1 as (q & l & rho & r & e & [= <- G2] & [= -> <-] & G3). destruct sss_mm_pos_nat with (2 := G3) (1 := H3) as (e2 & G4 & G5); simpl in *. destruct IH2 with (1 := G4) as (e3 & G6 & G7). exists e3; split; auto. constructor 2 with (st2 := (j2,e2)); auto. exists i, (mm_pos_nat l), (mm_var_map (@pos2nat _) rho), (mm_pos_nat r), e1; msplit 2; auto. * f_equal; subst P; unfold mm_pos_nat; repeat (rewrite map_app; simpl); auto. * unfold mm_pos_nat; 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)