proposition: Theorem reduction : SBTM_HALT ⪯ BSM_HALTING.
proof: Proof. exists (fun '(existT _ M (q, t)) => existT _ 4 (existT _ 1 (existT _ (@P M q) (encode_tape t)))). move=> [M [q [[ls a] rs]]]. split. - move=> [k] /simulation => /(_ q) [v Hv] /=. exists (0, v). split => /=; [|lia]. rewrite /P. bsm sss POP empty with ZERO (encode_state M q) (encode_state M q). - move=> [] [i v] [] [?] H /= ?. rewrite /P in H. bsm inv POP empty with H ZERO (encode_state M q) (encode_state M q). + move: H => [?] [?] /inverse_simulation. by apply. + move=> []. lia. Qed.
imports: Undecidability.StackMachines(BSM BSM.bsm_defs) Undecidability.TM(SBTM Util.SBTM_facts) Undecidability.Shared.Libs.DLW(vec subcode sss) PeanoNat List Lia ssreflect ssrbool ssrfun Undecidability.Synthetic.Definitions