proposition: Theorem TM_computable_to_BSM_computable {k} (R : Vector.t nat k -> nat -> Prop) : TM_computable R -> BSM_computable R.
proof: Proof. intros (n & Σ & s & b & Hsb & M & HM1 & HM2) % TM_computable_iff. destruct (@PREP_spec k n Σ s b) as [PREP HPREP]. destruct (BSM_complete_simulation M (1 + k) (length PREP)) as (Mbsm & Hf & Hb). destruct (@POSTP_spec k n Σ s b (length (PREP ++ Mbsm))) as [POSTP HPOSTP]. eapply BSM_computable_iff. eexists. exists 0. exists (PREP ++ Mbsm ++ POSTP). split. - intros v m (q & t & Heval & Hhd)% HM1. rewrite (Vector.eta t), Hhd in Heval. eapply Hf in Heval. eapply BSM_sss.eval_iff in Heval. setoid_rewrite BSM_sss.eval_iff. fold plus. edestruct (HPOSTP) as [out HPOSTP']. eexists. eexists. split. + eapply subcode_sss_compute_trans with (P := (0, PREP)). 1:auto. 1: eapply HPREP. eapply subcode_sss_compute_trans with (P := (|PREP|, Mbsm)). 1:auto. 1: eapply Heval. eapply subcode_sss_compute_trans with (P := (|PREP ++ Mbsm|, POSTP)). 1:auto. 1: rewrite <- app_length. 1: eapply HPOSTP'. bsm sss stop. reflexivity. + cbn. right. rewrite !app_length. lia. - intros. edestruct Hb as (? & ? & HbH). 2:eapply HM2. 2:eapply HbH. eapply subcode_sss_terminates. 2:{ eapply subcode_sss_terminates_inv. 1: eapply bsm_sss_fun. 1: eapply H. 2:{ split. 1: eapply HPREP. cbn. lia. } auto. } auto. 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)