fact: Fixpoint translate_form {f:falsity_flag} (phi : (@form _ _ full_operators f)) {struct phi} : (@form _ _ FragmentSyntax.frag_operators falsity_on) := match phi with | falsity => falsity | atom P v => atom P v | bin Conj phi1 phi2 => conj_to_impl_chain phi1 (conj_to_impl_chain phi2 falsity) --> falsity | bin Disj phi1 phi2 => disj_to_impl_chain phi1 (disj_to_impl_chain phi2 falsity) | bin FullSyntax.Impl phi1 phi2 => conj_to_impl_chain phi1 (translate_form phi2) | quant FullSyntax.All phi => @quant _ _ _ falsity_on All (translate_form phi) | quant Ex phi => (@quant _ _ _ falsity_on All (translate_negated phi)) --> falsity end with translate_negated {f:falsity_flag} (phi : (@form _ _ full_operators f)) {struct phi} : (@form _ _ FragmentSyntax.frag_operators falsity_on) := match phi with | falsity => falsity --> falsity | atom P v => atom P v --> falsity | bin Conj phi1 phi2 => conj_to_impl_chain phi1 (conj_to_impl_chain phi2 falsity) | bin Disj phi1 phi2 => disj_to_impl_chain phi1 (disj_to_impl_chain phi2 falsity) --> falsity | bin FullSyntax.Impl phi1 phi2 => (conj_to_impl_chain phi1 (translate_form phi2)) --> falsity | quant Ex phi => @quant _ _ _ falsity_on All (translate_negated phi) | quant FullSyntax.All phi => (@quant _ _ _ falsity_on All (translate_form phi)) --> falsity end with conj_to_impl_chain {f:falsity_flag} (phi : (@form _ _ full_operators f)) (terminal : (@form _ _ FragmentSyntax.frag_operators falsity_on)) {struct phi} : (@form _ _ FragmentSyntax.frag_operators falsity_on) := match phi with | falsity => falsity --> terminal | atom P v => atom P v --> terminal | bin Conj phi1 phi2 => conj_to_impl_chain phi1 (conj_to_impl_chain phi2 terminal) | bin Disj phi1 phi2 => (disj_to_impl_chain phi1 (disj_to_impl_chain phi2 falsity)) --> terminal | bin FullSyntax.Impl phi1 phi2 => conj_to_impl_chain phi1 (translate_form phi2) --> terminal | quant FullSyntax.All phi => @quant _ _ _ falsity_on All (translate_form phi) --> terminal | quant Ex phi => ((@quant _ _ _ falsity_on All (translate_negated phi)) --> falsity) --> terminal end with disj_to_impl_chain {f:falsity_flag} (phi : (@form _ _ full_operators f)) (terminal : (@form _ _ FragmentSyntax.frag_operators falsity_on)) {struct phi} : (@form _ _ FragmentSyntax.frag_operators falsity_on) := match phi with | falsity => (falsity --> falsity) --> terminal | atom P v => (atom P v --> falsity) --> terminal | bin Conj phi1 phi2 => (conj_to_impl_chain phi1 (conj_to_impl_chain phi2 falsity)) --> terminal | bin Disj phi1 phi2 => disj_to_impl_chain phi1 (disj_to_impl_chain phi2 terminal) | bin FullSyntax.Impl phi1 phi2 => ((conj_to_impl_chain phi1 (translate_form phi2)) --> falsity) --> terminal | quant Ex phi => (@quant _ _ _ falsity_on All (translate_negated phi)) --> terminal | quant FullSyntax.All phi => ((@quant _ _ _ falsity_on All (translate_form phi)) --> falsity) --> terminal end.
imports: Vector Undecidability.FOL(Syntax.Facts) Undecidability.FOL.Semantics.Tarski(FullFacts FragmentFacts) Undecidability.FOL.Semantics.FiniteTarski(Full Fragment) Undecidability.Shared(Dec) Undecidability.Shared.Libs.PSL(Numbers) Coq(Arith Lia List) Undecidability.Shared.Libs.DLW.Wf(wf_finite) Undecidability.Synthetic(Definitions)