FunctionFreeAtom

A FunctionFreeAtom is a GeneralizedAtom with VarOrConsts.

@[reducible, inline]

abbrev FunctionFreeAtom (sig : Signature) [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] : Type (max (max u_3 u_2) u_1)

Equations

• FunctionFreeAtom sig = GeneralizedAtom sig (VarOrConst sig)

def FunctionFreeAtom.variables {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (a : FunctionFreeAtom sig) : List sig.V

Using VarOrConst.filterVars, we can obtain all variables from the terms of the FunctionFreeAtom.

Equations

• a.variables = VarOrConst.filterVars a.terms

def FunctionFreeAtom.constants {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (a : FunctionFreeAtom sig) : List sig.C

Using VarOrConst.filterConsts, we can obtain all constants from the terms of the FunctionFreeAtom.

Equations

• a.constants = VarOrConst.filterConsts a.terms

@[simp]

theorem FunctionFreeAtom.mem_variables {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {a : FunctionFreeAtom sig} {v : sig.V} : v ∈ a.variables ↔ VarOrConst.var v ∈ a.terms

A variable occurs in variables iff it is a term of the `FunctionFreeAtom.

@[simp]

theorem FunctionFreeAtom.mem_constants {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {a : FunctionFreeAtom sig} {c : sig.C} : c ∈ a.constants ↔ VarOrConst.const c ∈ a.terms

A constant occurs in constants iff it is a term of the `FunctionFreeAtom.