def vocabOfFormula : Formula → Finset Char

Equations

• vocabOfFormula Formula.bottom = ∅
• vocabOfFormula (·c) = {c}
• vocabOfFormula (~φ) = vocabOfFormula φ
• vocabOfFormula (φ⋀ψ) = vocabOfFormula φ ∪ vocabOfFormula ψ
• vocabOfFormula (□φ) = vocabOfFormula φ

def vocabOfSetFormula : Finset Formula → Finset Char

Equations

• vocabOfSetFormula x✝ = x✝.biUnion vocabOfFormula

class HasVocabulary (α : Type) : Type

• voc : α → Finset Char

instance formulaHasVocabulary : HasVocabulary Formula

Equations

• formulaHasVocabulary = { voc := vocabOfFormula }

instance setFormulaHasVocabulary : HasVocabulary (Finset Formula)

Equations

• setFormulaHasVocabulary = { voc := vocabOfSetFormula }

@[simp]

theorem vocOfNeg {ϕ : Formula} : vocabOfFormula (~ϕ) = vocabOfFormula ϕ

theorem vocElem_subs_vocSet {ϕ : Formula} {X : Finset Formula} : ϕ ∈ X → vocabOfFormula ϕ ⊆ vocabOfSetFormula X

theorem vocMonotone {X Y : Finset Formula} (hyp : X ⊆ Y) : HasVocabulary.voc X ⊆ HasVocabulary.voc Y

theorem vocErase {X : Finset Formula} {ϕ : Formula} : HasVocabulary.voc (X \ {ϕ}) ⊆ HasVocabulary.voc X

theorem vocUnion {X Y : Finset Formula} : HasVocabulary.voc (X ∪ Y) = HasVocabulary.voc X ∪ HasVocabulary.voc Y

theorem vocPreserved (X : Finset Formula) (ψ ϕ : Formula) : ψ ∈ X → HasVocabulary.voc ϕ = HasVocabulary.voc ψ → HasVocabulary.voc X = HasVocabulary.voc (X \ {ψ} ∪ {ϕ})

theorem vocPreservedTwo {X : Finset Formula} (ψ ϕ1 ϕ2 : Formula) : ψ ∈ X → HasVocabulary.voc {ϕ1, ϕ2} = HasVocabulary.voc ψ → HasVocabulary.voc X = HasVocabulary.voc (X \ {ψ} ∪ {ϕ1, ϕ2})

theorem vocPreservedSub {X : Finset Formula} (ψ ϕ : Formula) : ψ ∈ X → HasVocabulary.voc ϕ ⊆ HasVocabulary.voc ψ → HasVocabulary.voc (X \ {ψ} ∪ {ϕ}) ⊆ HasVocabulary.voc X