proposition: Theorem reduction (S : IMSELL_sig3) : @ndMM2_ACCEPT nat ⪯ @IMSELL_cf_PROVABILITY3 S.
proof: Proof. destruct S as (S & HS). apply conditional_reduction, HS. Qed.
imports: List Permutation Arith Lia Undecidability.MinskyMachines(ndMM2) Undecidability.ILL(IMSELL imsell) Undecidability.Shared.Libs.DLW(utils pos vec) Undecidability.Synthetic(Definitions ReducibilityFacts)