fact: Fixpoint ksat {ff : falsity_flag} u (rho : nat -> domain) (phi : form) : Prop := match phi with | atom P v => k_P u (Vector.map (@eval _ _ _ k_interp rho) v) | falsity => False | bin Impl phi psi => forall v, reachable u v -> ksat v rho phi -> ksat v rho psi | quant All phi => forall j : domain, ksat u (j .: rho) phi end.
imports: Undecidability.FOL.Semantics.Tarski.FragmentFacts Undecidability.FOL.Semantics.Tarski.FragmentCore Undecidability.FOL.Syntax.Facts Undecidability(Shared.ListAutomation)