proposition: Theorem reduction : MM2_HALTING ⪯ MM2_ZERO_HALTING.
proof: Proof. exists (fun '(P, a0, b0) => Argument.M' P a0 b0). intros [[P a0] b0]. constructor. - apply Argument.transport. - apply Argument.reflection. Qed.
imports: List PeanoNat Lia Relations.Relation_Operators Relations.Operators_Properties Undecidability.MinskyMachines.MM2 Undecidability.MinskyMachines.Util.MM2_facts ssreflect ssrbool ssrfun Undecidability.Synthetic.Definitions