proposition: Theorem reduction : MM2_ZERO_HALTING ⪯ SSTS01.
proof: Proof. eexists=> [mm]. split. - move=> [c'0] [Hc0c'0 Hc'0]. eexists. by apply: Argument.transport; [|apply: SR2ab.to_SR2ab; eassumption]. - move=> [N HN]. apply: SR2ab.to_MM2_ZERO_HALTING. by apply: Argument.inverse_transport; [|eassumption]. Qed.
imports: List Relation_Operators Operators_Properties PeanoNat Lia ssreflect ssrbool ssrfun Undecidability.Synthetic.Definitions