inductive LO.IntProp.Formula (α : Type u) : Type u

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

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

Equations

• LO.IntProp.instDecidableEqFormula = LO.IntProp.decEqFormula✝

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

Equations

• LO.IntProp.Formula.instLogicalConnective = LO.LogicalConnective.mk

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

Equations

• LO.IntProp.Formula.verum.toStr = "\\top"
• LO.IntProp.Formula.falsum.toStr = "\\bot"
• (LO.IntProp.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.IntProp.Formula.instRepr {α : Type u_1} [ToString α] : Repr (LO.IntProp.Formula α)

Equations

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

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

Equations

• LO.IntProp.Formula.instToString = { toString := LO.IntProp.Formula.toStr }

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem LO.IntProp.Formula.neg_inj {α : Type u_1} (p : LO.IntProp.Formula α) (q : LO.IntProp.Formula α) : ∼p = ∼q ↔ p = q

theorem LO.IntProp.Formula.iff_def {α : Type u_1} (p : LO.IntProp.Formula α) (q : LO.IntProp.Formula α) : p ⭤ q = (p ➝ q) ⋏ (q ➝ p)

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

Equations

• (LO.IntProp.Formula.atom a).complexity = 0
• LO.IntProp.Formula.verum.complexity = 0
• LO.IntProp.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.IntProp.Formula.complexity_bot {α : Type u_1} : ⊥.complexity = 0

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• LO.IntProp.Formula.instDecidableEq = LO.IntProp.Formula.hasDecEq

def LO.IntProp.Formula.toNat {α : Type u_1} [Encodable α] : LO.IntProp.Formula α → ℕ

Equations

• (LO.IntProp.Formula.atom a).toNat = Nat.pair 0 (Encodable.encode a) + 1
• LO.IntProp.Formula.verum.toNat = Nat.pair 1 0 + 1
• LO.IntProp.Formula.falsum.toNat = Nat.pair 2 0 + 1
• p.neg.toNat = Nat.pair 3 p.toNat + 1
• (p.imp q).toNat = Nat.pair 4 (Nat.pair p.toNat q.toNat) + 1
• (p.and q).toNat = Nat.pair 5 (Nat.pair p.toNat q.toNat) + 1
• (p.or q).toNat = Nat.pair 6 (Nat.pair p.toNat q.toNat) + 1

@[irreducible]

def LO.IntProp.Formula.ofNat {α : Type u_1} [Encodable α] : ℕ → Option (LO.IntProp.Formula α)

Equations

• One or more equations did not get rendered due to their size.
• LO.IntProp.Formula.ofNat 0 = none

theorem LO.IntProp.Formula.ofNat_toNat {α : Type u_1} [Encodable α] (p : LO.IntProp.Formula α) : LO.IntProp.Formula.ofNat p.toNat = some p

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

Equations

• LO.IntProp.Formula.instEncodable = { encode := LO.IntProp.Formula.toNat, decode := LO.IntProp.Formula.ofNat, encodek := ⋯ }

@[reducible, inline]

abbrev LO.IntProp.Theory (α : Type u) : Type u

Equations

• LO.IntProp.Theory α = Set (LO.IntProp.Formula α)

@[reducible, inline]

abbrev LO.IntProp.Context (α : Type u) : Type u

Equations

• LO.IntProp.Context α = Finset (LO.IntProp.Formula α)