proposition: Lemma POSTP_spec' k n (Σ : finType) s b i : { POSTP | forall v : Vector.t _ k, forall t : Vector.t (tape Σ) (k + n), forall m m', exists out, (i, POSTP) // (i, Vector.append (repeat true m' ## v) ([] ::: [false] ::: skipn (length (strpush_common s b)) ((encode_bsm (encNatTM s b m ## t))@[Fin2]) ::: [] ::: vec_nil)) ->> (i + length POSTP, Vector.append (repeat true (m + m') ## v) (out )) }.
proof: Proof. pose (THESYM := encode_sym (projT1 (projT2 (FinTypes.finite_n (finType_CS (boundary + sigList (EncodeTapes.sigTape Σ))))) (inr (sigList_X (EncodeTapes.UnmarkedSymbol s))))). exists (pop_exactly (pos_right (1 + k) Fin2) (pos_right (1 + k) Fin0) (i + 4 + 2 * length THESYM) THESYM i ++ PUSH (pos_left 4 Fin0) true :: pop_many (pos_right (1 + k) Fin2) 2 (i + 1 + 2 * length THESYM) ++ POP (pos_right (1 + k) Fin0) i i :: nil). intros. induction m in i, m' |- *. - pose proof (encode_bsm_zero s b) as [n' Hn']. rewrite Hn'. unfold strpush_zero. rewrite <- !app_assoc. rewrite skipn_app'; [ | reflexivity]. edestruct (@pop_exactly_spec2 (1 + k + 4) (pos_right (1 + k) Fin2) (pos_right (1 + k) Fin0) (i + 4 + 2 * length THESYM)) as [x' Hpop]. 1:{ intros ? % pos_right_inj; congruence. } 3:{ eexists. eapply subcode_sss_compute_trans. 2: eapply Hpop. 1: auto. 1: eexists [], _. 1: cbn. 1: split. 2: lia. 1: reflexivity. bsm sss stop. apply f_equal2. 1: rewrite !app_length, pop_exactly_length. 1: cbn - [mult]. 1: lia. apply vec'_change_app_right. } 2:{ apply vec'_pos_app_right. } rewrite vec'_pos_app_right. cbn. intros (l' & Hneq). unfold THESYM in Hneq. eapply utils_list.list_app_inj in Hneq as []. 2: now rewrite !length_encode_sym. eapply encode_sym_inj in H. clear - H. destruct FinTypes.finite_n as [? [f H']]; cbn in *. destruct H' as [g [_ H2]]. eapply (f_equal g) in H. now rewrite !H2 in H. - edestruct IHm as [out IH]. eexists. rewrite encode_bsm_succ. unfold strpush_succ. fold THESYM. rewrite <- !app_assoc. rewrite skipn_app' by reflexivity. eapply subcode_sss_compute_trans. 2: eapply pop_exactly_spec1. { eexists [], _. split. 2:cbn;lia. { cbn. reflexivity. } } 1: { intros ? % pos_nxt_inj % pos_right_inj. discriminate. } 1: { cbn. rewrite vec'_pos_app_right. cbn. 1: reflexivity. } 1: { apply vec'_pos_app_right. } rewrite <- !vec_app_spec. rewrite vec_app_cons. cbn [vec_change pos_S_inv]. rewrite vec_change_app_right. cbn [vec_change pos_S_inv]. bsm sss PUSH with (pos_left 4 Fin0) true. 1: eexists (pop_exactly (pos_right (1 + k) pos2) (pos_right (1 + k) pos0) (i + 4 + 2 * (| THESYM |)) THESYM i), _. 1: { cbn. split. 1: reflexivity. rewrite pop_exactly_length. lia. } rewrite <- vec_app_cons. rewrite vec_change_app_left. cbn [vec_change pos_S_inv]. rewrite vec_pos_app_left. cbn [vec_pos pos_S_inv]. eapply subcode_sss_compute_trans. 2: eapply (@pop_many_spec (1 + k + 4) (pos_right (1 + k) Fin2) 2). { eexists (pop_exactly (pos_right (1 + k) Fin2) (pos_right (1 + k) Fin0) (i + 4 + 2 * length THESYM) THESYM i ++ PUSH (pos_left 4 Fin0) true :: nil), (POP (pos_right (1 + k) Fin0) i i :: nil). split. 1: simpl_list. 1: cbn - [mult]. 1: repeat f_equal. 1-4: cbn; lia. rewrite app_length, pop_exactly_length. cbn. lia. } rewrite vec_change_app_right. cbn [vec_change pos_S_inv]. rewrite vec_pos_app_right. cbn [vec_pos pos_S_inv]. rewrite skipn_plus. bsm sss POP empty with (pos_right (1 + k) Fin0) i i. 1: eexists (_ ++ _ :: _), []. 1: split. 1: rewrite app_nil_r. 1: simpl_list. 1: reflexivity. 1: rewrite app_length, pop_exactly_length. 1: cbn. 1: lia. 1: now rewrite vec_pos_app_right. match goal with [ |- sss_compute _ _ (_, ?st) _ ] => evar (ev : Vector.t (list bool) ((1 + k) + 4)); enough (st = ev) as ->; subst ev end. 1: match goal with [ |- sss_compute _ _ (_, _) (_, ?st) ] => evar (ev : Vector.t (list bool) ((1 + k) + 4)); enough (st = ev) as ->; subst ev end. 1: eapply IH. 1: instantiate (1 := S m'). 1: replace (m + S m') with (S (m + m')). 1: cbn [repeat plus]. 1: rewrite vec_app_cons. 1: now rewrite vec_app_spec. 1: lia. cbn [repeat]. rewrite vec_app_spec. assert (2 + (| strpush_common_short s b |) = | strpush_common s b |) as ->. { unfold strpush_common. rewrite app_length. cbn. lia. } reflexivity. Qed.
imports: Undecidability.StackMachines.BSM Undecidability.StackMachines.Util.BSM_computable Undecidability.TM.TM Undecidability.TM.Util.TM_facts Undecidability.TM.Util.TM_computable Undecidability.TM(TM Arbitrary_to_Binary mTM_to_TM HaltTM_1_to_HaltKOSBTM HaltKOSBTM_to_HaltBSM) Undecidability.Shared.Libs.DLW(vec pos sss subcode) Undecidability(bsm_utils bsm_defs) Undecidability.TM.Code.Code Undecidability.TM(Single.EncodeTapes)