FunctionFreeConjunction

A conjunction of FunctionFreeAtoms $p(x, y) \land q(y)$ can simply be represented as a list of FunctionFreeAtoms.

@[reducible, inline]

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

Equations

• FunctionFreeConjunction sig = List (FunctionFreeAtom sig)

def FunctionFreeConjunction.terms {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (conj : FunctionFreeConjunction sig) : List (VarOrConst sig)

The terms of a FunctionFreeConjunction are the terms of all its atoms.

Equations

• conj.terms = List.flatMap GeneralizedAtom.terms conj

def FunctionFreeConjunction.vars {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (conj : FunctionFreeConjunction sig) : List sig.V

The vars of a FunctionFreeConjunction are the variables of all its atoms.

Equations

• conj.vars = List.flatMap FunctionFreeAtom.variables conj

def FunctionFreeConjunction.consts {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (conj : FunctionFreeConjunction sig) : List sig.C

The consts of a FunctionFreeConjunction are the constants of all its atoms.

Equations

• conj.consts = List.flatMap FunctionFreeAtom.constants conj

def FunctionFreeConjunction.predicates {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (conj : FunctionFreeConjunction sig) : List sig.P

The predicates of a FunctionFreeConjunction are the predicates of all its atoms.

Equations

• conj.predicates = List.map GeneralizedAtom.predicate conj

@[simp]

theorem FunctionFreeConjunction.mem_vars {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {conj : FunctionFreeConjunction sig} {v : sig.V} : v ∈ conj.vars ↔ ∃ (f : FunctionFreeAtom sig), f ∈ conj ∧ VarOrConst.var v ∈ f.terms

Different from the definition, we can also say that a variable is in variables iff there is a FunctionFreeAtom in the conjunction that features the variable as a term.

theorem FunctionFreeConjunction.mem_vars' {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {conj : FunctionFreeConjunction sig} {v : sig.V} : v ∈ conj.vars ↔ VarOrConst.var v ∈ conj.terms

Different from the definition, we can also say that a variable is in variables iff it occurs as a term.

@[simp]

theorem FunctionFreeConjunction.mem_consts {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {conj : FunctionFreeConjunction sig} {c : sig.C} : c ∈ conj.consts ↔ ∃ (f : FunctionFreeAtom sig), f ∈ conj ∧ VarOrConst.const c ∈ f.terms

Different from the definition, we can also say that a constant is in consts iff there is a FunctionFreeAtom in the conjunction that features the constant as a term.

theorem FunctionFreeConjunction.mem_consts' {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {conj : FunctionFreeConjunction sig} {c : sig.C} : c ∈ conj.consts ↔ VarOrConst.const c ∈ conj.terms

Different from the definition, we can also say that a constant is in consts iff it occurs as a term.