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, exists out, (i, POSTP) // (i, Vector.append ([] ## v) ((encode_bsm (encNatTM s b m ## t)))) ->> (i + length POSTP, Vector.append (repeat true m ## v) (out )) }.
proof: Proof. destruct (@POSTP_spec' k n Σ s b (i + (length (strpush_common s b)))) as [POSTP HPOST]. specialize HPOST with (m' := 0). exists (pop_many (pos_right (1 + k) Fin2) (length (strpush_common s b)) i ++ POSTP). intros v t m. specialize HPOST with (m := m). edestruct (HPOST v) as (out & HPOST'). exists out. eapply subcode_sss_compute_trans. 2: eapply pop_many_spec. { eexists [], _. cbn. split. 1: reflexivity. lia. } 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]. rewrite encode_bsm_ext. cbn [vec_pos vec_change pos_S_inv]. rewrite vec_pos_app_right. cbn [vec_pos vec_change pos_S_inv]. rewrite vec_app_spec. cbn [Vector.append] in *. rewrite vec_app_cons. rewrite NPeano.Nat.add_0_r in HPOST'. rewrite vec_app_spec. cbn [repeat] in HPOST'. replace (|strpush_common s b| + i) with (i + |strpush_common s b|) by lia. eapply subcode_sss_compute_trans. 2: apply HPOST'. 1: eexists _, []. 1: split. 1: now rewrite app_nil_r. 1: rewrite pop_many_length. 1: lia. bsm sss stop. f_equal. rewrite app_length, pop_many_length. cbn. lia. 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)