Documentation

Logic.Propositional.Classical.Basic.Formula

Equations
Equations
  • LO.Propositional.Classical.Formula.instLogicalConnective = LO.LogicalConnective.mk
Equations
Equations
Equations
  • LO.Propositional.Classical.Formula.instToString = { toString := LO.Propositional.Classical.Formula.toStr }
Equations
  • LO.Propositional.Classical.Formula.instDeMorgan = { verum := , falsum := , imply := , and := , or := , neg := }
Equations
@[simp]
@[simp]
@[simp]
theorem LO.Propositional.Classical.Formula.complexity_and {α : Type u} (p : LO.Propositional.Classical.Formula α) (q : LO.Propositional.Classical.Formula α) :
(p q).complexity = max p.complexity q.complexity + 1
@[simp]
theorem LO.Propositional.Classical.Formula.complexity_and' {α : Type u} (p : LO.Propositional.Classical.Formula α) (q : LO.Propositional.Classical.Formula α) :
(p.and q).complexity = max p.complexity q.complexity + 1
@[simp]
theorem LO.Propositional.Classical.Formula.complexity_or {α : Type u} (p : LO.Propositional.Classical.Formula α) (q : LO.Propositional.Classical.Formula α) :
(p q).complexity = max p.complexity q.complexity + 1
@[simp]
theorem LO.Propositional.Classical.Formula.complexity_or' {α : Type u} (p : LO.Propositional.Classical.Formula α) (q : LO.Propositional.Classical.Formula α) :
(p.or q).complexity = max p.complexity q.complexity + 1
def LO.Propositional.Classical.Formula.cases' {α : Type u} {C : LO.Propositional.Classical.Formula αSort w} (hverum : C ) (hfalsum : C ) (hatom : (a : α) → C (LO.Propositional.Classical.Formula.atom a)) (hnatom : (a : α) → C (LO.Propositional.Classical.Formula.natom a)) (hand : (p q : LO.Propositional.Classical.Formula α) → C (p q)) (hor : (p q : LO.Propositional.Classical.Formula α) → C (p q)) (p : LO.Propositional.Classical.Formula α) :
C p
Equations
  • One or more equations did not get rendered due to their size.
def LO.Propositional.Classical.Formula.rec' {α : Type u} {C : LO.Propositional.Classical.Formula αSort w} (hverum : C ) (hfalsum : C ) (hatom : (a : α) → C (LO.Propositional.Classical.Formula.atom a)) (hnatom : (a : α) → C (LO.Propositional.Classical.Formula.natom a)) (hand : (p q : LO.Propositional.Classical.Formula α) → C pC qC (p q)) (hor : (p q : LO.Propositional.Classical.Formula α) → C pC qC (p q)) (p : LO.Propositional.Classical.Formula α) :
C p
Equations
@[simp]
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • LO.Propositional.Classical.Formula.instDecidableEq = LO.Propositional.Classical.Formula.hasDecEq
Equations
  • LO.Propositional.Classical.instCollectionFormulaTheory = inferInstance