proposition: Lemma BSM_complete_simulation n Σ (M : TM Σ n) m i : { P | (forall q t t', TM.eval M (TM.start M) t q t' -> forall v'', BSM.eval (m + (4)) (i, P) (i, Vector.append v'' ((encode_bsm t))) (i + length P, Vector.append v'' ((encode_bsm t')))) /\ (forall t v'', (sss.sss_terminates (bsm_sss (n := (m + (4)))) (i, P) (i, Vector.append v'' ((encode_bsm t)))) -> (exists q' t', TM.eval M (TM.start M) t q' t'))}.
proof: Proof. destruct (@BSM_complete_simulation' n Σ M m i) as (P & H1 & H2). exists P. split. 1: exact H1. intros t v'' ([out1 out2] & H % BSM_sss.eval_iff). eapply H2. eauto. 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)