proposition: Theorem reduction : SBTM_HALT ⪯ TM.HaltTM 1.
proof: Proof. exists ((fun '(existT _ M (q, t)) => existT2 _ _ (finType_CS bool) (M' M q) (| encode_tape t |)) ). move=> [M [q t]] /=. split. - by move=> [k] /simulation => /(_ q). - by move=> [?] [?] /inverse_simulation. Qed.
imports: Undecidability(TM.SBTM TM.Util.SBTM_facts) Undecidability.Shared.Libs.PSL.FiniteTypes.FinTypes PeanoNat Lia List ssreflect ssrbool ssrfun Undecidability.Synthetic.Definitions