inductive LO.Propositional.Superintuitionistic.Formula (α : Type u) : Type u

• atom: {α : Type u} → α → LO.Propositional.Superintuitionistic.Formula α
• verum: {α : Type u} → LO.Propositional.Superintuitionistic.Formula α
• falsum: {α : Type u} → LO.Propositional.Superintuitionistic.Formula α
• neg: {α : Type u} → LO.Propositional.Superintuitionistic.Formula α → LO.Propositional.Superintuitionistic.Formula α
• and: {α : Type u} → LO.Propositional.Superintuitionistic.Formula α → LO.Propositional.Superintuitionistic.Formula α → LO.Propositional.Superintuitionistic.Formula α
• or: {α : Type u} → LO.Propositional.Superintuitionistic.Formula α → LO.Propositional.Superintuitionistic.Formula α → LO.Propositional.Superintuitionistic.Formula α
• imp: {α : Type u} → LO.Propositional.Superintuitionistic.Formula α → LO.Propositional.Superintuitionistic.Formula α → LO.Propositional.Superintuitionistic.Formula α

instance LO.Propositional.Superintuitionistic.instDecidableEqFormula : {α : Type u_1} → [inst : DecidableEq α] → DecidableEq (LO.Propositional.Superintuitionistic.Formula α)

Equations

• LO.Propositional.Superintuitionistic.instDecidableEqFormula = LO.Propositional.Superintuitionistic.decEqFormula✝

instance LO.Propositional.Superintuitionistic.Formula.instLogicalConnective {α : Type u_1} : LO.LogicalConnective (LO.Propositional.Superintuitionistic.Formula α)

Equations

• LO.Propositional.Superintuitionistic.Formula.instLogicalConnective = LO.LogicalConnective.mk

def LO.Propositional.Superintuitionistic.Formula.toStr {α : Type u_1} [ToString α] : LO.Propositional.Superintuitionistic.Formula α → String

Equations

• LO.Propositional.Superintuitionistic.Formula.verum.toStr = "\\top"
• LO.Propositional.Superintuitionistic.Formula.falsum.toStr = "\\bot"
• (LO.Propositional.Superintuitionistic.Formula.atom a).toStr = "{" ++ toString a ++ "}"
• p.neg.toStr = "\\lnot " ++ p.toStr
• (p.and q).toStr = "\\left(" ++ p.toStr ++ " \\land " ++ q.toStr ++ "\\right)"
• (p.or q).toStr = "\\left(" ++ p.toStr ++ " \\lor " ++ q.toStr ++ "\\right)"
• (p.imp q).toStr = "\\left(" ++ p.toStr ++ " \\rightarrow " ++ q.toStr ++ "\\right)"

instance LO.Propositional.Superintuitionistic.Formula.instRepr {α : Type u_1} [ToString α] : Repr (LO.Propositional.Superintuitionistic.Formula α)

Equations

• LO.Propositional.Superintuitionistic.Formula.instRepr = { reprPrec := fun (t : LO.Propositional.Superintuitionistic.Formula α) (x : ℕ) => Std.Format.text t.toStr }

instance LO.Propositional.Superintuitionistic.Formula.instToString {α : Type u_1} [ToString α] : ToString (LO.Propositional.Superintuitionistic.Formula α)

Equations

• LO.Propositional.Superintuitionistic.Formula.instToString = { toString := LO.Propositional.Superintuitionistic.Formula.toStr }

@[simp]

theorem LO.Propositional.Superintuitionistic.Formula.and_inj {α : Type u_1} (p₁ : LO.Propositional.Superintuitionistic.Formula α) (q₁ : LO.Propositional.Superintuitionistic.Formula α) (p₂ : LO.Propositional.Superintuitionistic.Formula α) (q₂ : LO.Propositional.Superintuitionistic.Formula α) : p₁ ⋏ p₂ = q₁ ⋏ q₂ ↔ p₁ = q₁ ∧ p₂ = q₂

@[simp]

theorem LO.Propositional.Superintuitionistic.Formula.or_inj {α : Type u_1} (p₁ : LO.Propositional.Superintuitionistic.Formula α) (q₁ : LO.Propositional.Superintuitionistic.Formula α) (p₂ : LO.Propositional.Superintuitionistic.Formula α) (q₂ : LO.Propositional.Superintuitionistic.Formula α) : p₁ ⋎ p₂ = q₁ ⋎ q₂ ↔ p₁ = q₁ ∧ p₂ = q₂

@[simp]

theorem LO.Propositional.Superintuitionistic.Formula.imp_inj {α : Type u_1} (p₁ : LO.Propositional.Superintuitionistic.Formula α) (q₁ : LO.Propositional.Superintuitionistic.Formula α) (p₂ : LO.Propositional.Superintuitionistic.Formula α) (q₂ : LO.Propositional.Superintuitionistic.Formula α) : p₁ ⟶ p₂ = q₁ ⟶ q₂ ↔ p₁ = q₁ ∧ p₂ = q₂

@[simp]

theorem LO.Propositional.Superintuitionistic.Formula.neg_inj {α : Type u_1} (p : LO.Propositional.Superintuitionistic.Formula α) (q : LO.Propositional.Superintuitionistic.Formula α) : ~p = ~q ↔ p = q

theorem LO.Propositional.Superintuitionistic.Formula.iff_def {α : Type u_1} (p : LO.Propositional.Superintuitionistic.Formula α) (q : LO.Propositional.Superintuitionistic.Formula α) : p ⟷ q = (p ⟶ q) ⋏ (q ⟶ p)

def LO.Propositional.Superintuitionistic.Formula.complexity {α : Type u_1} : LO.Propositional.Superintuitionistic.Formula α → ℕ

Equations

• (LO.Propositional.Superintuitionistic.Formula.atom a).complexity = 0
• LO.Propositional.Superintuitionistic.Formula.verum.complexity = 0
• LO.Propositional.Superintuitionistic.Formula.falsum.complexity = 0
• p.neg.complexity = p.complexity + 1
• (p.imp q).complexity = max p.complexity q.complexity + 1
• (p.and q).complexity = max p.complexity q.complexity + 1
• (p.or q).complexity = max p.complexity q.complexity + 1

@[simp]

theorem LO.Propositional.Superintuitionistic.Formula.complexity_bot {α : Type u_1} : ⊥.complexity = 0

@[simp]

theorem LO.Propositional.Superintuitionistic.Formula.complexity_top {α : Type u_1} : ⊤.complexity = 0

@[simp]

theorem LO.Propositional.Superintuitionistic.Formula.complexity_atom {α : Type u_1} (a : α) : (LO.Propositional.Superintuitionistic.Formula.atom a).complexity = 0

@[simp]

theorem LO.Propositional.Superintuitionistic.Formula.complexity_imp {α : Type u_1} (p : LO.Propositional.Superintuitionistic.Formula α) (q : LO.Propositional.Superintuitionistic.Formula α) : (p ⟶ q).complexity = max p.complexity q.complexity + 1

@[simp]

theorem LO.Propositional.Superintuitionistic.Formula.complexity_imp' {α : Type u_1} (p : LO.Propositional.Superintuitionistic.Formula α) (q : LO.Propositional.Superintuitionistic.Formula α) : (p.imp q).complexity = max p.complexity q.complexity + 1

@[simp]

theorem LO.Propositional.Superintuitionistic.Formula.complexity_and {α : Type u_1} (p : LO.Propositional.Superintuitionistic.Formula α) (q : LO.Propositional.Superintuitionistic.Formula α) : (p ⋏ q).complexity = max p.complexity q.complexity + 1

@[simp]

theorem LO.Propositional.Superintuitionistic.Formula.complexity_and' {α : Type u_1} (p : LO.Propositional.Superintuitionistic.Formula α) (q : LO.Propositional.Superintuitionistic.Formula α) : (p.and q).complexity = max p.complexity q.complexity + 1

@[simp]

theorem LO.Propositional.Superintuitionistic.Formula.complexity_or {α : Type u_1} (p : LO.Propositional.Superintuitionistic.Formula α) (q : LO.Propositional.Superintuitionistic.Formula α) : (p ⋎ q).complexity = max p.complexity q.complexity + 1

@[simp]

theorem LO.Propositional.Superintuitionistic.Formula.complexity_or' {α : Type u_1} (p : LO.Propositional.Superintuitionistic.Formula α) (q : LO.Propositional.Superintuitionistic.Formula α) : (p.or q).complexity = max p.complexity q.complexity + 1

def LO.Propositional.Superintuitionistic.Formula.cases' {α : Type u_1} {C : LO.Propositional.Superintuitionistic.Formula α → Sort w} (hfalsum : C ⊥) (hverum : C ⊤) (hatom : (a : α) → C (LO.Propositional.Superintuitionistic.Formula.atom a)) (hneg : (p : LO.Propositional.Superintuitionistic.Formula α) → C (~p)) (himp : (p q : LO.Propositional.Superintuitionistic.Formula α) → C (p ⟶ q)) (hand : (p q : LO.Propositional.Superintuitionistic.Formula α) → C (p ⋏ q)) (hor : (p q : LO.Propositional.Superintuitionistic.Formula α) → C (p ⋎ q)) (p : LO.Propositional.Superintuitionistic.Formula α) : C p

Equations

• One or more equations did not get rendered due to their size.

def LO.Propositional.Superintuitionistic.Formula.rec' {α : Type u_1} {C : LO.Propositional.Superintuitionistic.Formula α → Sort w} (hfalsum : C ⊥) (hverum : C ⊤) (hatom : (a : α) → C (LO.Propositional.Superintuitionistic.Formula.atom a)) (hneg : (p : LO.Propositional.Superintuitionistic.Formula α) → C p → C (~p)) (himp : (p q : LO.Propositional.Superintuitionistic.Formula α) → C p → C q → C (p ⟶ q)) (hand : (p q : LO.Propositional.Superintuitionistic.Formula α) → C p → C q → C (p ⋏ q)) (hor : (p q : LO.Propositional.Superintuitionistic.Formula α) → C p → C q → C (p ⋎ q)) (p : LO.Propositional.Superintuitionistic.Formula α) : C p

Equations

• One or more equations did not get rendered due to their size.
• LO.Propositional.Superintuitionistic.Formula.rec' hfalsum hverum hatom hneg himp hand hor LO.Propositional.Superintuitionistic.Formula.falsum = hfalsum
• LO.Propositional.Superintuitionistic.Formula.rec' hfalsum hverum hatom hneg himp hand hor LO.Propositional.Superintuitionistic.Formula.verum = hverum
• LO.Propositional.Superintuitionistic.Formula.rec' hfalsum hverum hatom hneg himp hand hor (LO.Propositional.Superintuitionistic.Formula.atom a) = hatom a

def LO.Propositional.Superintuitionistic.Formula.hasDecEq {α : Type u_1} [DecidableEq α] (p : LO.Propositional.Superintuitionistic.Formula α) (q : LO.Propositional.Superintuitionistic.Formula α) : Decidable (p = q)

Equations

• One or more equations did not get rendered due to their size.

instance LO.Propositional.Superintuitionistic.Formula.instDecidableEq {α : Type u_1} [DecidableEq α] : DecidableEq (LO.Propositional.Superintuitionistic.Formula α)

Equations

• LO.Propositional.Superintuitionistic.Formula.instDecidableEq = LO.Propositional.Superintuitionistic.Formula.hasDecEq

@[reducible, inline]

abbrev LO.Propositional.Superintuitionistic.Formula.Node (α : Type u_1) : Type u_1

Equations

• LO.Propositional.Superintuitionistic.Formula.Node α = (α ⊕ Fin 2 ⊕ Fin 1 ⊕ Fin 3)

@[reducible]

def LO.Propositional.Superintuitionistic.Formula.Edge (α : Type u_1) : LO.Propositional.Superintuitionistic.Formula.Node α → Type

Equations

• One or more equations did not get rendered due to their size.

def LO.Propositional.Superintuitionistic.Formula.toW {α : Type u_1} : LO.Propositional.Superintuitionistic.Formula α → WType (LO.Propositional.Superintuitionistic.Formula.Edge α)

Equations

• (LO.Propositional.Superintuitionistic.Formula.atom a).toW = WType.mk (Sum.inl a) Empty.elim
• LO.Propositional.Superintuitionistic.Formula.falsum.toW = WType.mk (Sum.inr (Sum.inl 0)) Empty.elim
• LO.Propositional.Superintuitionistic.Formula.verum.toW = WType.mk (Sum.inr (Sum.inl 1)) Empty.elim
• p.neg.toW = WType.mk (Sum.inr (Sum.inr (Sum.inl 0))) fun (t : PUnit.{1}) => PUnit.rec p.toW t
• (p.imp q).toW = WType.mk (Sum.inr (Sum.inr (Sum.inr 0))) fun (t : Bool) => Bool.rec p.toW q.toW t
• (p.or q).toW = WType.mk (Sum.inr (Sum.inr (Sum.inr 1))) fun (t : Bool) => Bool.rec p.toW q.toW t
• (p.and q).toW = WType.mk (Sum.inr (Sum.inr (Sum.inr 2))) fun (t : Bool) => Bool.rec p.toW q.toW t

def LO.Propositional.Superintuitionistic.Formula.ofW {α : Type u_1} : WType (LO.Propositional.Superintuitionistic.Formula.Edge α) → LO.Propositional.Superintuitionistic.Formula α

Equations

• One or more equations did not get rendered due to their size.
• LO.Propositional.Superintuitionistic.Formula.ofW (WType.mk (Sum.inl a) f) = LO.Propositional.Superintuitionistic.Formula.atom a
• LO.Propositional.Superintuitionistic.Formula.ofW (WType.mk (Sum.inr (Sum.inl 0)) f) = LO.Propositional.Superintuitionistic.Formula.falsum
• LO.Propositional.Superintuitionistic.Formula.ofW (WType.mk (Sum.inr (Sum.inl 1)) f) = LO.Propositional.Superintuitionistic.Formula.verum
• LO.Propositional.Superintuitionistic.Formula.ofW (WType.mk (Sum.inr (Sum.inr (Sum.inl 0))) p) = (LO.Propositional.Superintuitionistic.Formula.ofW (p ())).neg

theorem LO.Propositional.Superintuitionistic.Formula.toW_ofW {α : Type u_1} (w : WType (LO.Propositional.Superintuitionistic.Formula.Edge α)) : (LO.Propositional.Superintuitionistic.Formula.ofW w).toW = w

def LO.Propositional.Superintuitionistic.Formula.equivW (α : Type u_1) : LO.Propositional.Superintuitionistic.Formula α ≃ WType (LO.Propositional.Superintuitionistic.Formula.Edge α)

Equations

• One or more equations did not get rendered due to their size.

instance LO.Propositional.Superintuitionistic.Formula.instFintypeEdge {α : Type u_1} (a : LO.Propositional.Superintuitionistic.Formula.Node α) : Fintype (LO.Propositional.Superintuitionistic.Formula.Edge α a)

Equations

• One or more equations did not get rendered due to their size.

instance LO.Propositional.Superintuitionistic.Formula.instPrimcodableEdge {α : Type u_1} (a : LO.Propositional.Superintuitionistic.Formula.Node α) : Primcodable (LO.Propositional.Superintuitionistic.Formula.Edge α a)

Equations

• One or more equations did not get rendered due to their size.

instance LO.Propositional.Superintuitionistic.Formula.instEncodable {α : Type u_1} [Encodable α] : Encodable (LO.Propositional.Superintuitionistic.Formula α)

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev LO.Propositional.Superintuitionistic.Theory (α : Type u) : Type u

Equations

• LO.Propositional.Superintuitionistic.Theory α = Set (LO.Propositional.Superintuitionistic.Formula α)

@[reducible, inline]

abbrev LO.Propositional.Superintuitionistic.AxiomSet (α : Type u) : Type u

Equations

• LO.Propositional.Superintuitionistic.AxiomSet α = Set (LO.Propositional.Superintuitionistic.Formula α)

@[reducible, inline]

abbrev LO.Propositional.Superintuitionistic.Context (α : Type u) : Type u

Equations

• LO.Propositional.Superintuitionistic.Context α = Finset (LO.Propositional.Superintuitionistic.Formula α)