proposition: Theorem KOSBTM_to_BSM : HaltKOSBTM ⪯ Halt_BSM.
proof: Proof. unshelve eexists. - intros [M t]. exists 4. exists 0. exists (SIM M 0). exact (enc_tape t). - intros [M t]. setoid_rewrite Halt_BSM_iff. eapply SIM_correct. Qed.
imports: Undecidability.TM.KOSBTM.KOSBTM Undecidability.Shared.Libs.PSL.Vectors.FinNotation Undecidability.Shared.Libs.PSL.Vectors.Vectors Undecidability.Shared.Libs.PSL.EqDec List Arith Lia Bool Undecidability.Shared.Libs.DLW(utils list_bool pos vec subcode sss) Undecidability.StackMachines.BSM(bsm_defs) Undecidability.Synthetic.Definitions