proposition: Theorem reduction : SBTM_HALT ⪯ SR.SR.
proof: Proof. exists ((fun '(existT _ M (q, t)) => (srs M, encode_config M q t, [1; 0]))). move=> [M [q t]] /=. split. - by move=> [?] /simulation. - by apply: inverse_simulation. Qed.
imports: Undecidability(TM.SBTM TM.Util.SBTM_facts) PeanoNat Lia List ssreflect ssrbool ssrfun Undecidability.Synthetic.Definitions