proposition: Theorem conditional_reduction (S : IMSELL_sig) : (exists a b i : S, a ≤ i /\ b ≤ i /\ a ≰ b /\ b ≰ a /\ ~ U a /\ ~ U b /\ U i) -> @ndMM2_ACCEPT nat ⪯ @IMSELL_cf_PROVABILITY S.
proof: Proof. intros (a & b & i & ?). apply reduces_dependent; exists. intros (Σ & u & x & y). exists (ndmm2_imsell_ctx _ a b i Σ x y, imsell_var _ (2+u)). apply ndmm2_imsell_correct; simpl; tauto. Qed.
imports: List Permutation Arith Lia Undecidability.MinskyMachines(ndMM2) Undecidability.ILL(IMSELL imsell) Undecidability.Shared.Libs.DLW(utils pos vec) Undecidability.Synthetic(Definitions ReducibilityFacts)