proposition: Theorem reduction : MM2_HALTS_ON_ZERO ⪯ @ndMM2_ACCEPT nat.
proof: Proof. apply reduces_dependent; exists. intros ((P,a),b). exists (existT _ (mm2_prog_enc P) (1,(a,b))). apply MM2_ndMM2_equiv. Qed.
imports: List Arith Lia Relations Undecidability.MinskyMachines(MM2 ndMM2) Undecidability.Shared.Libs.DLW(utils) Undecidability.Synthetic(Definitions ReducibilityFacts)