proposition: Theorem reduction : MMA2_HALTS_ON_ZERO ⪯ @ndMM2_ACCEPT nat.
proof: Proof. apply reduces_dependent; exists. intros (P & v); vec2 v into a b. exists (existT _ (mma2_prog_enc P) (1,(a,b))). apply MMA2_ndMM2_equiv. Qed.
imports: List Arith Lia Relations Undecidability.MinskyMachines(MMA mma_defs ndMM2) Undecidability.Shared.Libs.DLW(utils Vec.pos Vec.vec Code.subcode Code.sss) Undecidability.Synthetic(Definitions ReducibilityFacts)