proposition: Theorem satisReduction : complement H10UPC_SAT ⪯ @satis sig_empty sig_binary falsity_on.
proof: Proof. exists (fun l => @F falsity_on l → falsity). split. * apply satisTransport. * apply satisInverseTransport. Qed.
imports: Undecidability.DiophantineConstraints(H10C) Undecidability.DiophantineConstraints.Util(H10UPC_facts) Undecidability.FOL(Syntax.Facts Deduction.FragmentNDFacts Semantics.Tarski.FragmentSoundness Semantics.Tarski.FragmentFacts Syntax.BinSig Semantics.Kripke.FragmentCore Semantics.Kripke.FragmentSoundness Semantics.Kripke.FragmentToTarski) Undecidability.Shared(Dec) Undecidability.Shared.Libs.PSL(Numbers) Coq(Arith Lia List) Undecidability.FOL.Reductions(H10UPC_to_FOL_friedman H10UPC_to_FOL_constructions) Undecidability.Synthetic.Definitions