proposition: Fact sss_mm_pos_nat rho st1 st2 e1 : snd st1 ⋈ e1 -> rho /v/ st1 -1> st2 -> exists e2, snd st2 ⋈ e2 /\ mm_var_map (@pos2nat n) rho /e/ (fst st1,e1) -1> (fst st2,e2).
proof: Proof. revert st1 st2; intros (j1,v1) (j2,v2); simpl. intros H1 H2. destruct rho as [ x | x p ]; simpl in *; [ | case_eq (vec_pos v1 x); [ intros He1 | intros q Hq ] ]. - exists (e1⦃pos2nat x ⇠ S (e1⇢pos2nat x)⦄). apply mm_sss_INC_inv in H2. destruct H2 as (? & ?); subst; split. 2: constructor. intros p. destruct (pos_eq_dec x p) as [ -> | C ]; rew vec; rew env. rewrite H1; assert (pos2nat x <> pos2nat p); rew env. contradict C; revert C; apply pos2nat_inj. - exists e1. apply mm_sss_DEC0_inv in H2; destruct H2; subst; auto. split; auto; constructor; rewrite <- H1; auto. - exists (e1⦃pos2nat x ⇠ q⦄). apply mm_sss_DEC1_inv with (1 := Hq) in H2. destruct H2; subst; split. 2: constructor; rewrite <- H1; auto. intros j. destruct (pos_eq_dec x j) as [ -> | C ]; rew vec; rew env. rewrite H1; assert (pos2nat x <> pos2nat j); rew env. contradict C; revert C; apply pos2nat_inj. 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)