proposition: Fact sss_mm_pos_nat_inv rho st1 st2 v1 : v1 ⋈ snd st1 -> mm_var_map (@pos2nat n) rho /e/ st1 -1> st2 -> exists v2, v2 ⋈ snd (st2) /\ rho /v/ (fst st1,v1) -1> (fst st2,v2).
proof: Proof. revert st1 st2; intros (j1,e1) (j2,e2); simpl. intros H1 H2. destruct rho as [ x | x p ]; simpl in *; [ | case_eq (e1⇢pos2nat x); [ intros He1 | intros q Hq ] ]. - exists (vec_change v1 x (S (vec_pos v1 x))). apply mm_sss_env_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 v1. apply mm_sss_env_DEC0_inv in H2; destruct H2; subst; auto. split; auto; constructor; rewrite H1; auto. - exists (vec_change v1 x q). apply mm_sss_env_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)