proposition: Lemma prep_spec (p : pos k) v i np : v #> pos0 = 0 -> v #> tmp pos0 = 0 -> v #> tmp pos1 = 0 -> v #> reg p = np -> (i, prep p i) /MM/ (i, v) ~~> (14 + i, v [ (stack_enc (List.repeat true (v #> reg p))) / reg p]).
proof: Proof. intros Htgt Htmp1 Htmp2 Hnp. unfold prep. split. 2:{ cbn. lia. } eapply sss_compute_trans. { eapply subcode_sss_compute with (P := (i,mm_transfert (reg p) (pos0) (pos_right (1 + k + n) Fin.F1) i)). 1: auto. eapply sss_progress_compute. eapply mm_transfert_progress; auto. } mm sss INC with (pos_left 3 (pos_left n (pos_right 1 p))). 1: replace (3 + i) with (i + 3) by lia. 1: auto. rew vec. replace (1 + (3 + i)) with (4 + i) by lia. rewrite vec_change_swap. 1: rewrite vec_change_idem. 1: pose (npm := 0). 1: match goal with [ |- context [vec_change ?v ?x 1]] => change (vec_change v x 1) with (vec_change v x (stack_enc (repeat true npm))) end. 1: assert (np = np + npm) by lia. 1: rewrite Hnp. 1: revert Hnp. 1: revert H. 2:auto. generalize np at 2 4. generalize npm. intros npr npl Heq Hnp. induction npl in npr, np, Heq, Hnp |- *. - eapply sss_compute_trans. { eapply subcode_sss_compute with (P := (i+4, DEC Fin.F1 (14 + i) :: List.nil)). 1: auto. mm sss DEC zero with pos0 (14 + i). 1: replace (4 + i) with (i + 4) by lia. 1: eapply subcode_refl. 1: rew vec. fold plus. mm sss stop. } mm sss stop. f_equal. cbn. rewrite vec_change_swap. 2:congruence. match goal with [ |- context [@vec_change ?X ?n ?vv ?x 0]] => replace (@vec_change X n vv x 0) with (vec_change vv x (v#>pos0)) end. 2: now rewrite Htgt. rewrite vec_change_same. subst. reflexivity. - eapply sss_compute_trans. { eapply subcode_sss_compute with (P := (i+4, DEC Fin.F1 (14 + i) :: List.nil)). 1: auto. mm sss DEC S with pos0 (14 + i) npl. 1: replace (4 + i) with (i + 4) by lia. 1: eapply subcode_refl. 1: rew vec. fold plus. mm sss stop. } rew vec. eapply sss_compute_trans. { eapply subcode_sss_compute with (P := (5 + i, mm_push_One (pos_left 3 (pos_left n (pos_right 1 p))) (pos_right (1 + k + n) pos0) (pos_right (1 + k + n) pos1) (5+i))). 1: replace (5 + i) with (i + 5) at 1 by lia; auto. eapply sss_progress_compute. eapply mm_push_One_progress; rew vec. - rewrite vec_change_neq; eauto. - rewrite vec_change_neq; eauto. } mm sss DEC zero with (pos_right (1 + k + n) Fin.F1) (4 + i). 1: replace (8 + (1 + (4 + i))) with (i + 13) by lia. 1: auto. 1: rewrite vec_change_neq. 2:auto. 1: rewrite vec_change_neq. 2:auto. 1: rewrite vec_change_neq. 2:auto. 1: eauto. rewrite vec_change_swap. 2:auto. rewrite vec_change_idem. change (true :: repeat true npr) with (repeat true (S npr)). eapply IHnpl. 1: lia. assumption. Qed.
imports: Undecidability.MinskyMachines(MM_computable MM_sss mm_utils) Undecidability.StackMachines(BSM_computable) Undecidability.Shared.Libs.DLW(vec pos sss subcode) Lia Vector Nat Arith List Undecidability.MinskyMachines.MM(mm_defs mm_utils mm_comp_strong)