proposition: Lemma KOSBTM_complete_simulation n Σ (M : TM Σ n) : {M' : KOSBTM.KOSBTM | (forall q t t', TM.eval M (TM.start M) t q t' -> exists q', KOSBTM.eval M' Fin.F1 (complete_encode t) q' (complete_encode t')) /\ (forall t, (exists q' t', KOSBTM.eval M' Fin.F1 (complete_encode t) q' t') -> (exists q' t', TM.eval M (TM.start M) t q' t'))}.
proof: Proof. destruct (TM_sTM_simulation M) as (M1 & Hf1 & Hb1). destruct (binary_simulation M1) as (M2 & Hf2 & Hb2). destruct (KOSBTM_simulation M2) as (M3 & Hf3 & Hb3). exists M3. split. - intros q t t' [q1 [q2 [q3 H] % Hf3] % Hf2] % Hf1. eexists. eapply H. - intros t H % Hb3 % Hb2 % Hb1. exact H. 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)