proposition: Lemma POSTP_spec_strong i v out out' : v #> pos0 = out' -> v #> tmp pos0 = 0 -> v #> tmp pos1 = 0 -> v #> tmp pos2 = stack_enc (List.repeat true out) -> (i, POSTP i) /MM/ (i, v) ~~> (i + 18, v [ (out + out') / Fin.F1 ] [ (stack_enc nil) / tmp pos2] ).
proof: Proof. intros Htgt Htmp0 Htmp1 Htmp2. split. 2:{ cbn. lia. } induction out in v, Htgt, Htmp0, Htmp1, Htmp2, out', Htgt, Htmp2 |- *. - cbn [repeat] in Htmp2. eapply subcode_sss_compute_trans with (P := (i,mm_pop (tmp pos2) (tmp pos0) (tmp pos1) (i) (i+16) (i+16) (i+18))). 1: unfold POSTP; auto. { eapply sss_progress_compute. eapply mm_pop_void_progress; eauto. } mm sss stop. f_equal. eapply vec_pos_ext. fold plus. intros p. eapply (Fin.caseS' p). + rewrite vec_change_neq; eauto. rewrite vec_change_eq; eauto. + clear p. apply pos_left_right_rect. * intros p. rewrite !vec_change_neq; try congruence. intros ? % pos_nxt_inj. fold pos_right in H. eapply pos_right_left. now rewrite H. * intros p. eapply (Fin.caseS' p); clear p. -- rewrite !vec_change_neq; try congruence. eapply tmp2_tmp0. -- intros p. eapply (Fin.caseS' p); clear p. ++ rewrite !vec_change_neq; try congruence. intros H. eapply tmp1_tmp2. cbn. rewrite <- H. reflexivity. ++ intros p. eapply (Fin.caseS' p); clear p. ** rewrite vec_change_eq. 2: reflexivity. eauto. ** eapply Fin.case0. - cbn [repeat] in Htmp2. eapply subcode_sss_compute_trans with (P := (i,mm_pop (tmp pos2) (tmp pos0) (tmp pos1) (i) (i+16) (i+16) (i+18))). 1: unfold POSTP; auto. { eapply sss_progress_compute. eapply mm_pop_One_progress; eauto. } mm sss INC with pos0. 1: unfold POSTP. 1: auto. fold plus in *. mm sss DEC zero with (tmp pos0) i. 1: unfold POSTP. 1: auto. { rew vec. rewrite vec_change_neq; eauto. } rew vec. specialize IHout with (out' := S out'). replace (out + S out') with (S (out + out')) in IHout by lia. match goal with [ |- sss_compute _ _ _ (_, ?st) ] => evar (Vector.t nat (1 + k + n + 3)); enough (st = t) as ->; subst t end. 1: eapply IHout; rew vec. + rewrite vec_change_neq; eauto. + rewrite vec_change_neq; eauto. + rew vec. symmetry. rewrite vec_change_swap. 2: eauto. rewrite vec_change_idem, vec_change_swap; eauto. 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)