class LO.Modal.Hilbert.HasT {α : Type u_1} (H : Hilbert α) : Type u_1

• p : α
• mem_T : Axioms.T (Formula.atom (p H)) ∈ H.axioms

instance LO.Modal.Hilbert.instHasAxiomTFormulaOfHasT {α : Type u_1} {H : Hilbert α} [DecidableEq α] [hT : H.HasT] : Entailment.HasAxiomT H

Equations

• LO.Modal.Hilbert.instHasAxiomTFormulaOfHasT = { T := fun (φ : LO.Modal.Formula α) => LO.Modal.Hilbert.Deduction.maxm ⋯ }

class LO.Modal.Hilbert.HasB {α : Type u_1} (H : Hilbert α) : Type u_1

• p : α
• mem_B : Axioms.B (Formula.atom (p H)) ∈ H.axioms

instance LO.Modal.Hilbert.instHasAxiomBFormulaOfHasB {α : Type u_1} {H : Hilbert α} [DecidableEq α] [hB : H.HasB] : Entailment.HasAxiomB H

Equations

• LO.Modal.Hilbert.instHasAxiomBFormulaOfHasB = { B := fun (φ : LO.Modal.Formula α) => LO.Modal.Hilbert.Deduction.maxm ⋯ }

class LO.Modal.Hilbert.HasD {α : Type u_1} (H : Hilbert α) : Type u_1

• p : α
• mem_D : Axioms.D (Formula.atom (p H)) ∈ H.axioms

instance LO.Modal.Hilbert.instHasAxiomDFormulaOfHasD {α : Type u_1} {H : Hilbert α} [DecidableEq α] [hD : H.HasD] : Entailment.HasAxiomD H

Equations

• LO.Modal.Hilbert.instHasAxiomDFormulaOfHasD = { D := fun (φ : LO.Modal.Formula α) => LO.Modal.Hilbert.Deduction.maxm ⋯ }

class LO.Modal.Hilbert.HasFour {α : Type u_1} (H : Hilbert α) : Type u_1

• p : α
• mem_Four : Axioms.Four (Formula.atom (p H)) ∈ H.axioms

instance LO.Modal.Hilbert.instHasAxiomFourFormulaOfHasFour {α : Type u_1} {H : Hilbert α} [DecidableEq α] [hFour : H.HasFour] : Entailment.HasAxiomFour H

Equations

• LO.Modal.Hilbert.instHasAxiomFourFormulaOfHasFour = { Four := fun (φ : LO.Modal.Formula α) => LO.Modal.Hilbert.Deduction.maxm ⋯ }

class LO.Modal.Hilbert.HasFive {α : Type u_1} (H : Hilbert α) : Type u_1

• p : α
• mem_Five : Axioms.Five (Formula.atom (p H)) ∈ H.axioms

instance LO.Modal.Hilbert.instHasAxiomFiveFormulaOfHasFive {α : Type u_1} {H : Hilbert α} [DecidableEq α] [hFive : H.HasFive] : Entailment.HasAxiomFive H

Equations

• LO.Modal.Hilbert.instHasAxiomFiveFormulaOfHasFive = { Five := fun (φ : LO.Modal.Formula α) => LO.Modal.Hilbert.Deduction.maxm ⋯ }

class LO.Modal.Hilbert.HasPoint2 {α : Type u_1} (H : Hilbert α) : Type u_1

• p : α
• mem_Point2 : Axioms.Point2 (Formula.atom (p H)) ∈ H.axioms

instance LO.Modal.Hilbert.instHasAxiomPoint2FormulaOfHasPoint2 {α : Type u_1} {H : Hilbert α} [DecidableEq α] [hPoint2 : H.HasPoint2] : Entailment.HasAxiomPoint2 H

Equations

• LO.Modal.Hilbert.instHasAxiomPoint2FormulaOfHasPoint2 = { Point2 := fun (φ : LO.Modal.Formula α) => LO.Modal.Hilbert.Deduction.maxm ⋯ }

class LO.Modal.Hilbert.HasWeakPoint2 {α : Type u_1} (H : Hilbert α) : Type u_1

• p : α
• q : α
• ne_pq : p H ≠ q H
• mem_WeakPoint2 : Axioms.WeakPoint2 (Formula.atom (p H)) (Formula.atom (q H)) ∈ H.axioms

instance LO.Modal.Hilbert.instHasAxiomWeakPoint2FormulaOfHasWeakPoint2 {α : Type u_1} {H : Hilbert α} [DecidableEq α] [hDotWeak2 : H.HasWeakPoint2] : Entailment.HasAxiomWeakPoint2 H

Equations

• LO.Modal.Hilbert.instHasAxiomWeakPoint2FormulaOfHasWeakPoint2 = { WeakPoint2 := fun (φ ψ : LO.Modal.Formula α) => LO.Modal.Hilbert.Deduction.maxm ⋯ }

class LO.Modal.Hilbert.HasPoint3 {α : Type u_1} (H : Hilbert α) : Type u_1

• p : α
• q : α
• ne_pq : p H ≠ q H
• mem_Point3 : Axioms.Point3 (Formula.atom (p H)) (Formula.atom (q H)) ∈ H.axioms

instance LO.Modal.Hilbert.instHasAxiomPoint3FormulaOfHasPoint3 {α : Type u_1} {H : Hilbert α} [DecidableEq α] [hPoint3 : H.HasPoint3] : Entailment.HasAxiomPoint3 H

Equations

• LO.Modal.Hilbert.instHasAxiomPoint3FormulaOfHasPoint3 = { Point3 := fun (φ ψ : LO.Modal.Formula α) => LO.Modal.Hilbert.Deduction.maxm ⋯ }

class LO.Modal.Hilbert.HasWeakPoint3 {α : Type u_1} (H : Hilbert α) : Type u_1

• p : α
• q : α
• ne_pq : p H ≠ q H
• mem_WeakPoint3 : Axioms.WeakPoint3 (Formula.atom (p H)) (Formula.atom (q H)) ∈ H.axioms

instance LO.Modal.Hilbert.instHasAxiomWeakPoint3FormulaOfHasWeakPoint3 {α : Type u_1} {H : Hilbert α} [DecidableEq α] [hDotWeak3 : H.HasWeakPoint3] : Entailment.HasAxiomWeakPoint3 H

Equations

• LO.Modal.Hilbert.instHasAxiomWeakPoint3FormulaOfHasWeakPoint3 = { WeakPoint3 := fun (φ ψ : LO.Modal.Formula α) => LO.Modal.Hilbert.Deduction.maxm ⋯ }

class LO.Modal.Hilbert.HasL {α : Type u_1} (H : Hilbert α) : Type u_1

• p : α
• mem_L : Axioms.L (Formula.atom (p H)) ∈ H.axioms

instance LO.Modal.Hilbert.instHasAxiomLFormulaOfHasL {α : Type u_1} {H : Hilbert α} [DecidableEq α] [hL : H.HasL] : Entailment.HasAxiomL H

Equations

• LO.Modal.Hilbert.instHasAxiomLFormulaOfHasL = { L := fun (φ : LO.Modal.Formula α) => LO.Modal.Hilbert.Deduction.maxm ⋯ }

class LO.Modal.Hilbert.HasGrz {α : Type u_1} (H : Hilbert α) : Type u_1

• p : α
• mem_Grz : Axioms.Grz (Formula.atom (p H)) ∈ H.axioms

instance LO.Modal.Hilbert.instHasAxiomGrzFormulaOfHasGrz {α : Type u_1} {H : Hilbert α} [DecidableEq α] [hGrz : H.HasGrz] : Entailment.HasAxiomGrz H

Equations

• LO.Modal.Hilbert.instHasAxiomGrzFormulaOfHasGrz = { Grz := fun (φ : LO.Modal.Formula α) => LO.Modal.Hilbert.Deduction.maxm ⋯ }

class LO.Modal.Hilbert.HasTc {α : Type u_1} (H : Hilbert α) : Type u_1

• p : α
• mem_Tc : Axioms.Tc (Formula.atom (p H)) ∈ H.axioms

instance LO.Modal.Hilbert.instHasAxiomTcFormulaOfHasTc {α : Type u_1} {H : Hilbert α} [DecidableEq α] [hTc : H.HasTc] : Entailment.HasAxiomTc H

Equations

• LO.Modal.Hilbert.instHasAxiomTcFormulaOfHasTc = { Tc := fun (φ : LO.Modal.Formula α) => LO.Modal.Hilbert.Deduction.maxm ⋯ }

class LO.Modal.Hilbert.HasVer {α : Type u_1} (H : Hilbert α) : Type u_1

• p : α
• mem_Ver : Axioms.Ver (Formula.atom (p H)) ∈ H.axioms

instance LO.Modal.Hilbert.instHasAxiomVerFormulaOfDecidableEqOfHasVer {α : Type u_1} {H : Hilbert α} [DecidableEq α] [hVer : H.HasVer] : Entailment.HasAxiomVer H

Equations

• LO.Modal.Hilbert.instHasAxiomVerFormulaOfDecidableEqOfHasVer = { Ver := fun (φ : LO.Modal.Formula α) => LO.Modal.Hilbert.Deduction.maxm ⋯ }

class LO.Modal.Hilbert.HasH {α : Type u_1} (H : Hilbert α) : Type u_1

• p : α
• mem_H : Axioms.H (Formula.atom (p H)) ∈ H.axioms

instance LO.Modal.Hilbert.instHasAxiomHFormulaOfHasH {α : Type u_1} {H : Hilbert α} [DecidableEq α] [hH : H.HasH] : Entailment.HasAxiomH H

Equations

• LO.Modal.Hilbert.instHasAxiomHFormulaOfHasH = { H := fun (φ : LO.Modal.Formula α) => LO.Modal.Hilbert.Deduction.maxm ⋯ }

class LO.Modal.Hilbert.HasZ {α : Type u_1} (H : Hilbert α) : Type u_1

• p : α
• mem_Z : Axioms.Z (Formula.atom (p H)) ∈ H.axioms

instance LO.Modal.Hilbert.instHasAxiomZFormulaOfHasZ {α : Type u_1} {H : Hilbert α} [DecidableEq α] [hZ : H.HasZ] : Entailment.HasAxiomZ H

Equations

• LO.Modal.Hilbert.instHasAxiomZFormulaOfHasZ = { Z := fun (φ : LO.Modal.Formula α) => LO.Modal.Hilbert.Deduction.maxm ⋯ }

class LO.Modal.Hilbert.HasM {α : Type u_1} (H : Hilbert α) : Type u_1

• p : α
• mem_M : Axioms.M (Formula.atom (p H)) ∈ H.axioms

instance LO.Modal.Hilbert.instHasAxiomMFormulaOfHasM {α : Type u_1} {H : Hilbert α} [DecidableEq α] [hM : H.HasM] : Entailment.HasAxiomM H

Equations

• LO.Modal.Hilbert.instHasAxiomMFormulaOfHasM = { M := fun (φ : LO.Modal.Formula α) => LO.Modal.Hilbert.Deduction.maxm ⋯ }

class LO.Modal.Hilbert.HasMk {α : Type u_1} (H : Hilbert α) : Type u_1

• p : α
• q : α
• ne_pq : p H ≠ q H
• mem_Mk : Axioms.Modal.Mk (Formula.atom (p H)) (Formula.atom (q H)) ∈ H.axioms

instance LO.Modal.Hilbert.instHasAxiomMkFormulaOfHasMk {α : Type u_1} {H : Hilbert α} [DecidableEq α] [H.HasMk] : Entailment.Modal.HasAxiomMk H

Equations

• LO.Modal.Hilbert.instHasAxiomMkFormulaOfHasMk = { Mk := fun (φ ψ : LO.Modal.Formula α) => LO.Modal.Hilbert.Deduction.maxm ⋯ }

@[reducible, inline]

abbrev LO.Modal.Hilbert.KT : Hilbert ℕ

Equations

• LO.Modal.Hilbert.KT = { axioms := {LO.Axioms.K (LO.Modal.Formula.atom 0) (LO.Modal.Formula.atom 1), LO.Axioms.T (LO.Modal.Formula.atom 0)} }

instance LO.Modal.Hilbert.instHasKNatKT : Hilbert.KT.HasK

Equations

• LO.Modal.Hilbert.instHasKNatKT = { p := 0, q := 1, ne_pq := LO.Modal.Hilbert.instHasKNatKT._proof_19, mem_K := LO.Modal.Hilbert.instHasKNatKT._proof_20 }

instance LO.Modal.Hilbert.instHasTNatKT : Hilbert.KT.HasT

Equations

• LO.Modal.Hilbert.instHasTNatKT = { p := 0, mem_T := LO.Modal.Hilbert.instHasTNatKT._proof_21 }

instance LO.Modal.Hilbert.instKTNatFormulaKT : Entailment.Modal.KT Hilbert.KT

Equations

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

@[reducible, inline]

abbrev LO.Modal.Hilbert.KD : Hilbert ℕ

Equations

• LO.Modal.Hilbert.KD = { axioms := {LO.Axioms.K (LO.Modal.Formula.atom 0) (LO.Modal.Formula.atom 1), LO.Axioms.D (LO.Modal.Formula.atom 0)} }

instance LO.Modal.Hilbert.instHasKNatKD : Hilbert.KD.HasK

Equations

• LO.Modal.Hilbert.instHasKNatKD = { p := 0, q := 1, ne_pq := LO.Modal.Hilbert.instHasKNatKT._proof_19, mem_K := LO.Modal.Hilbert.instHasKNatKD._proof_22 }

instance LO.Modal.Hilbert.instHasDNatKD : Hilbert.KD.HasD

Equations

• LO.Modal.Hilbert.instHasDNatKD = { p := 0, mem_D := LO.Modal.Hilbert.instHasDNatKD._proof_23 }

instance LO.Modal.Hilbert.instKDNatFormulaKD : Entailment.Modal.KD Hilbert.KD

Equations

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

@[reducible, inline]

abbrev LO.Modal.Hilbert.KB : Hilbert ℕ

Equations

• LO.Modal.Hilbert.KB = { axioms := {LO.Axioms.K (LO.Modal.Formula.atom 0) (LO.Modal.Formula.atom 1), LO.Axioms.B (LO.Modal.Formula.atom 0)} }

instance LO.Modal.Hilbert.instHasKNatKB : Hilbert.KB.HasK

Equations

• LO.Modal.Hilbert.instHasKNatKB = { p := 0, q := 1, ne_pq := LO.Modal.Hilbert.instHasKNatKT._proof_19, mem_K := LO.Modal.Hilbert.instHasKNatKB._proof_24 }

instance LO.Modal.Hilbert.instHasBNatKB : Hilbert.KB.HasB

Equations

• LO.Modal.Hilbert.instHasBNatKB = { p := 0, mem_B := LO.Modal.Hilbert.instHasBNatKB._proof_25 }

instance LO.Modal.Hilbert.instKBNatFormulaKB : Entailment.Modal.KB Hilbert.KB

Equations

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

@[reducible, inline]

abbrev LO.Modal.Hilbert.KDB : Hilbert ℕ

Equations

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

instance LO.Modal.Hilbert.instHasKNatKDB : Hilbert.KDB.HasK

Equations

• LO.Modal.Hilbert.instHasKNatKDB = { p := 0, q := 1, ne_pq := LO.Modal.Hilbert.instHasKNatKT._proof_19, mem_K := LO.Modal.Hilbert.instHasKNatKDB._proof_26 }

instance LO.Modal.Hilbert.instHasDNatKDB : Hilbert.KDB.HasD

Equations

• LO.Modal.Hilbert.instHasDNatKDB = { p := 0, mem_D := LO.Modal.Hilbert.instHasDNatKDB._proof_27 }

instance LO.Modal.Hilbert.instHasBNatKDB : Hilbert.KDB.HasB

Equations

• LO.Modal.Hilbert.instHasBNatKDB = { p := 0, mem_B := LO.Modal.Hilbert.instHasBNatKDB._proof_28 }

instance LO.Modal.Hilbert.instKDBNatFormulaKDB : Entailment.Modal.KDB Hilbert.KDB

Equations

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

@[reducible, inline]

abbrev LO.Modal.Hilbert.KTB : Hilbert ℕ

Equations

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

instance LO.Modal.Hilbert.instHasKNatKTB : Hilbert.KTB.HasK

Equations

• LO.Modal.Hilbert.instHasKNatKTB = { p := 0, q := 1, ne_pq := LO.Modal.Hilbert.instHasKNatKT._proof_19, mem_K := LO.Modal.Hilbert.instHasKNatKTB._proof_29 }

instance LO.Modal.Hilbert.instHasTNatKTB : Hilbert.KTB.HasT

Equations

• LO.Modal.Hilbert.instHasTNatKTB = { p := 0, mem_T := LO.Modal.Hilbert.instHasTNatKTB._proof_30 }

instance LO.Modal.Hilbert.instHasBNatKTB : Hilbert.KTB.HasB

Equations

• LO.Modal.Hilbert.instHasBNatKTB = { p := 0, mem_B := LO.Modal.Hilbert.instHasBNatKTB._proof_31 }

instance LO.Modal.Hilbert.instKTBNatFormulaKTB : Entailment.Modal.KTB Hilbert.KTB

Equations

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

@[reducible, inline]

abbrev LO.Modal.Hilbert.KM : Hilbert ℕ

Equations

• LO.Modal.Hilbert.KM = { axioms := {LO.Axioms.K (LO.Modal.Formula.atom 0) (LO.Modal.Formula.atom 1), LO.Axioms.M (LO.Modal.Formula.atom 0)} }

instance LO.Modal.Hilbert.instHasKNatKM : Hilbert.KM.HasK

Equations

• LO.Modal.Hilbert.instHasKNatKM = { p := 0, q := 1, ne_pq := LO.Modal.Hilbert.instHasKNatKT._proof_19, mem_K := LO.Modal.Hilbert.instHasKNatKM._proof_32 }

instance LO.Modal.Hilbert.instHasMNatKM : Hilbert.KM.HasM

Equations

• LO.Modal.Hilbert.instHasMNatKM = { p := 0, mem_M := LO.Modal.Hilbert.instHasMNatKM._proof_33 }

instance LO.Modal.Hilbert.instKMNatFormulaKM : Entailment.Modal.KM Hilbert.KM

Equations

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

instance LO.Modal.Hilbert.K_weakerThan_KM : Hilbert.K ⪯ Hilbert.KM

@[reducible, inline]

abbrev LO.Modal.Hilbert.K4 : Hilbert ℕ

Equations

• LO.Modal.Hilbert.K4 = { axioms := {LO.Axioms.K (LO.Modal.Formula.atom 0) (LO.Modal.Formula.atom 1), LO.Axioms.Four (LO.Modal.Formula.atom 0)} }

instance LO.Modal.Hilbert.instHasKNatK4 : Hilbert.K4.HasK

Equations

• LO.Modal.Hilbert.instHasKNatK4 = { p := 0, q := 1, ne_pq := LO.Modal.Hilbert.instHasKNatKT._proof_19, mem_K := LO.Modal.Hilbert.instHasKNatK4._proof_34 }

instance LO.Modal.Hilbert.instHasFourNatK4 : Hilbert.K4.HasFour

Equations

• LO.Modal.Hilbert.instHasFourNatK4 = { p := 0, mem_Four := LO.Modal.Hilbert.instHasFourNatK4._proof_35 }

instance LO.Modal.Hilbert.instK4NatFormulaK4 : Entailment.Modal.K4 Hilbert.K4

Equations

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

@[reducible, inline]

abbrev LO.Modal.Hilbert.K4Point1 : Hilbert ℕ

Equations

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

instance LO.Modal.Hilbert.instHasKNatK4Point1 : Hilbert.K4Point1.HasK

Equations

• LO.Modal.Hilbert.instHasKNatK4Point1 = { p := 0, q := 1, ne_pq := LO.Modal.Hilbert.instHasKNatKT._proof_19, mem_K := LO.Modal.Hilbert.instHasKNatK4Point1._proof_36 }

instance LO.Modal.Hilbert.instHasFourNatK4Point1 : Hilbert.K4Point1.HasFour

Equations

• LO.Modal.Hilbert.instHasFourNatK4Point1 = { p := 0, mem_Four := LO.Modal.Hilbert.instHasFourNatK4Point1._proof_37 }

instance LO.Modal.Hilbert.instHasMNatK4Point1 : Hilbert.K4Point1.HasM

Equations

• LO.Modal.Hilbert.instHasMNatK4Point1 = { p := 0, mem_M := LO.Modal.Hilbert.instHasMNatK4Point1._proof_38 }

instance LO.Modal.Hilbert.instK4Point1NatFormulaK4Point1 : Entailment.Modal.K4Point1 Hilbert.K4Point1

Equations

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

instance LO.Modal.Hilbert.K_weakerThan_K4Point1 : Hilbert.K ⪯ Hilbert.K4Point1

noncomputable instance LO.Modal.Hilbert.instK4Point1NatFormulaOfWeakerThanK4Point1 {H : Hilbert ℕ} [Hilbert.K4Point1 ⪯ H] : Entailment.Modal.K4Point1 H

Equations

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

@[reducible, inline]

abbrev LO.Modal.Hilbert.K4Point2 : Hilbert ℕ

Equations

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

instance LO.Modal.Hilbert.instHasKNatK4Point2 : Hilbert.K4Point2.HasK

Equations

• LO.Modal.Hilbert.instHasKNatK4Point2 = { p := 0, q := 1, ne_pq := LO.Modal.Hilbert.instHasKNatKT._proof_19, mem_K := LO.Modal.Hilbert.instHasKNatK4Point2._proof_42 }

instance LO.Modal.Hilbert.instHasFourNatK4Point2 : Hilbert.K4Point2.HasFour

Equations

• LO.Modal.Hilbert.instHasFourNatK4Point2 = { p := 0, mem_Four := LO.Modal.Hilbert.instHasFourNatK4Point2._proof_43 }

instance LO.Modal.Hilbert.instHasWeakPoint2NatK4Point2 : Hilbert.K4Point2.HasWeakPoint2

Equations

• LO.Modal.Hilbert.instHasWeakPoint2NatK4Point2 = { p := 0, q := 1, ne_pq := LO.Modal.Hilbert.instHasKNatKT._proof_19, mem_WeakPoint2 := LO.Modal.Hilbert.instHasWeakPoint2NatK4Point2._proof_44 }

instance LO.Modal.Hilbert.instK4Point2NatFormulaK4Point2 : Entailment.Modal.K4Point2 Hilbert.K4Point2

Equations

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

@[reducible, inline]

abbrev LO.Modal.Hilbert.K4Point3 : Hilbert ℕ

Equations

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

instance LO.Modal.Hilbert.instHasKNatK4Point3 : Hilbert.K4Point3.HasK

Equations

• LO.Modal.Hilbert.instHasKNatK4Point3 = { p := 0, q := 1, ne_pq := LO.Modal.Hilbert.instHasKNatKT._proof_19, mem_K := LO.Modal.Hilbert.instHasKNatK4Point3._proof_45 }

instance LO.Modal.Hilbert.instHasFourNatK4Point3 : Hilbert.K4Point3.HasFour

Equations

• LO.Modal.Hilbert.instHasFourNatK4Point3 = { p := 0, mem_Four := LO.Modal.Hilbert.instHasFourNatK4Point3._proof_46 }

instance LO.Modal.Hilbert.instHasWeakPoint3NatK4Point3 : Hilbert.K4Point3.HasWeakPoint3

Equations

• LO.Modal.Hilbert.instHasWeakPoint3NatK4Point3 = { p := 0, q := 1, ne_pq := LO.Modal.Hilbert.instHasKNatKT._proof_19, mem_WeakPoint3 := LO.Modal.Hilbert.instHasWeakPoint3NatK4Point3._proof_47 }

instance LO.Modal.Hilbert.instK4Point3NatFormulaK4Point3 : Entailment.Modal.K4Point3 Hilbert.K4Point3

Equations

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

@[reducible, inline]

abbrev LO.Modal.Hilbert.KT4B : Hilbert ℕ

Equations

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

instance LO.Modal.Hilbert.instHasKNatKT4B : Hilbert.KT4B.HasK

Equations

• LO.Modal.Hilbert.instHasKNatKT4B = { p := 0, q := 1, ne_pq := LO.Modal.Hilbert.instHasKNatKT._proof_19, mem_K := LO.Modal.Hilbert.instHasKNatKT4B._proof_48 }

instance LO.Modal.Hilbert.instHasTNatKT4B : Hilbert.KT4B.HasT

Equations

• LO.Modal.Hilbert.instHasTNatKT4B = { p := 0, mem_T := LO.Modal.Hilbert.instHasTNatKT4B._proof_49 }

instance LO.Modal.Hilbert.instHasFourNatKT4B : Hilbert.KT4B.HasFour

Equations

• LO.Modal.Hilbert.instHasFourNatKT4B = { p := 0, mem_Four := LO.Modal.Hilbert.instHasFourNatKT4B._proof_50 }

instance LO.Modal.Hilbert.instHasBNatKT4B : Hilbert.KT4B.HasB

Equations

• LO.Modal.Hilbert.instHasBNatKT4B = { p := 0, mem_B := LO.Modal.Hilbert.instHasBNatKT4B._proof_51 }

instance LO.Modal.Hilbert.instKT4BNatFormulaKT4B : Entailment.Modal.KT4B Hilbert.KT4B

Equations

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

@[reducible, inline]

abbrev LO.Modal.Hilbert.K45 : Hilbert ℕ

Equations

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

instance LO.Modal.Hilbert.instHasKNatK45 : Hilbert.K45.HasK

Equations

• LO.Modal.Hilbert.instHasKNatK45 = { p := 0, q := 1, ne_pq := LO.Modal.Hilbert.instHasKNatKT._proof_19, mem_K := LO.Modal.Hilbert.instHasKNatK45._proof_52 }

instance LO.Modal.Hilbert.instHasFourNatK45 : Hilbert.K45.HasFour

Equations

• LO.Modal.Hilbert.instHasFourNatK45 = { p := 0, mem_Four := LO.Modal.Hilbert.instHasFourNatK45._proof_53 }

instance LO.Modal.Hilbert.instHasFiveNatK45 : Hilbert.K45.HasFive

Equations

• LO.Modal.Hilbert.instHasFiveNatK45 = { p := 0, mem_Five := LO.Modal.Hilbert.instHasFiveNatK45._proof_54 }

instance LO.Modal.Hilbert.instK45NatFormulaK45 : Entailment.Modal.K45 Hilbert.K45

Equations

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

@[reducible, inline]

abbrev LO.Modal.Hilbert.KD4 : Hilbert ℕ

Equations

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

instance LO.Modal.Hilbert.instHasKNatKD4 : Hilbert.KD4.HasK

Equations

• LO.Modal.Hilbert.instHasKNatKD4 = { p := 0, q := 1, ne_pq := LO.Modal.Hilbert.instHasKNatKT._proof_19, mem_K := LO.Modal.Hilbert.instHasKNatKD4._proof_55 }

instance LO.Modal.Hilbert.instHasDNatKD4 : Hilbert.KD4.HasD

Equations

• LO.Modal.Hilbert.instHasDNatKD4 = { p := 0, mem_D := LO.Modal.Hilbert.instHasDNatKD4._proof_56 }

instance LO.Modal.Hilbert.instHasFourNatKD4 : Hilbert.KD4.HasFour

Equations

• LO.Modal.Hilbert.instHasFourNatKD4 = { p := 0, mem_Four := LO.Modal.Hilbert.instHasFourNatKD4._proof_57 }

instance LO.Modal.Hilbert.instKD4NatFormulaKD4 : Entailment.Modal.KD4 Hilbert.KD4

Equations

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

@[reducible, inline]

abbrev LO.Modal.Hilbert.KD5 : Hilbert ℕ

Equations

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

instance LO.Modal.Hilbert.instHasKNatKD5 : Hilbert.KD5.HasK

Equations

• LO.Modal.Hilbert.instHasKNatKD5 = { p := 0, q := 1, ne_pq := LO.Modal.Hilbert.instHasKNatKT._proof_19, mem_K := LO.Modal.Hilbert.instHasKNatKD5._proof_58 }

instance LO.Modal.Hilbert.instHasDNatKD5 : Hilbert.KD5.HasD

Equations

• LO.Modal.Hilbert.instHasDNatKD5 = { p := 0, mem_D := LO.Modal.Hilbert.instHasDNatKD5._proof_59 }

instance LO.Modal.Hilbert.instHasFiveNatKD5 : Hilbert.KD5.HasFive

Equations

• LO.Modal.Hilbert.instHasFiveNatKD5 = { p := 0, mem_Five := LO.Modal.Hilbert.instHasFiveNatKD5._proof_60 }

instance LO.Modal.Hilbert.instKD5NatFormulaKD5 : Entailment.Modal.KD5 Hilbert.KD5

Equations

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

@[reducible, inline]

abbrev LO.Modal.Hilbert.KD45 : Hilbert ℕ

Equations

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

instance LO.Modal.Hilbert.instHasKNatKD45 : Hilbert.KD45.HasK

Equations

• LO.Modal.Hilbert.instHasKNatKD45 = { p := 0, q := 1, ne_pq := LO.Modal.Hilbert.instHasKNatKT._proof_19, mem_K := LO.Modal.Hilbert.instHasKNatKD45._proof_61 }

instance LO.Modal.Hilbert.instHasDNatKD45 : Hilbert.KD45.HasD

Equations

• LO.Modal.Hilbert.instHasDNatKD45 = { p := 0, mem_D := LO.Modal.Hilbert.instHasDNatKD45._proof_62 }

instance LO.Modal.Hilbert.instHasFourNatKD45 : Hilbert.KD45.HasFour

Equations

• LO.Modal.Hilbert.instHasFourNatKD45 = { p := 0, mem_Four := LO.Modal.Hilbert.instHasFourNatKD45._proof_63 }

instance LO.Modal.Hilbert.instHasFiveNatKD45 : Hilbert.KD45.HasFive

Equations

• LO.Modal.Hilbert.instHasFiveNatKD45 = { p := 0, mem_Five := LO.Modal.Hilbert.instHasFiveNatKD45._proof_64 }

instance LO.Modal.Hilbert.instKD45NatFormulaKD45 : Entailment.Modal.KD45 Hilbert.KD45

Equations

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

@[reducible, inline]

abbrev LO.Modal.Hilbert.KB4 : Hilbert ℕ

Equations

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

instance LO.Modal.Hilbert.instHasKNatKB4 : Hilbert.KB4.HasK

Equations

• LO.Modal.Hilbert.instHasKNatKB4 = { p := 0, q := 1, ne_pq := LO.Modal.Hilbert.instHasKNatKT._proof_19, mem_K := LO.Modal.Hilbert.instHasKNatKB4._proof_65 }

instance LO.Modal.Hilbert.instHasBNatKB4 : Hilbert.KB4.HasB

Equations

• LO.Modal.Hilbert.instHasBNatKB4 = { p := 0, mem_B := LO.Modal.Hilbert.instHasBNatKB4._proof_66 }

instance LO.Modal.Hilbert.instHasFourNatKB4 : Hilbert.KB4.HasFour

Equations

• LO.Modal.Hilbert.instHasFourNatKB4 = { p := 0, mem_Four := LO.Modal.Hilbert.instHasFourNatKB4._proof_67 }

instance LO.Modal.Hilbert.instKB4NatFormulaKB4 : Entailment.Modal.KB4 Hilbert.KB4

Equations

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

@[reducible, inline]

abbrev LO.Modal.Hilbert.KB5 : Hilbert ℕ

Equations

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

instance LO.Modal.Hilbert.instHasKNatKB5 : Hilbert.KB5.HasK

Equations

• LO.Modal.Hilbert.instHasKNatKB5 = { p := 0, q := 1, ne_pq := LO.Modal.Hilbert.instHasKNatKT._proof_19, mem_K := LO.Modal.Hilbert.instHasKNatKB5._proof_68 }

instance LO.Modal.Hilbert.instHasBNatKB5 : Hilbert.KB5.HasB

Equations

• LO.Modal.Hilbert.instHasBNatKB5 = { p := 0, mem_B := LO.Modal.Hilbert.instHasBNatKB5._proof_69 }

instance LO.Modal.Hilbert.instHasFiveNatKB5 : Hilbert.KB5.HasFive

Equations

• LO.Modal.Hilbert.instHasFiveNatKB5 = { p := 0, mem_Five := LO.Modal.Hilbert.instHasFiveNatKB5._proof_70 }

instance LO.Modal.Hilbert.instKB5NatFormulaKB5 : Entailment.Modal.KB5 Hilbert.KB5

Equations

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

@[reducible, inline]

abbrev LO.Modal.Hilbert.S4 : Hilbert ℕ

Equations

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

instance LO.Modal.Hilbert.instHasKNatS4 : Hilbert.S4.HasK

Equations

• LO.Modal.Hilbert.instHasKNatS4 = { p := 0, q := 1, ne_pq := LO.Modal.Hilbert.instHasKNatKT._proof_19, mem_K := LO.Modal.Hilbert.instHasKNatS4._proof_71 }

instance LO.Modal.Hilbert.instHasTNatS4 : Hilbert.S4.HasT

Equations

• LO.Modal.Hilbert.instHasTNatS4 = { p := 0, mem_T := LO.Modal.Hilbert.instHasTNatS4._proof_72 }

instance LO.Modal.Hilbert.instHasFourNatS4 : Hilbert.S4.HasFour

Equations

• LO.Modal.Hilbert.instHasFourNatS4 = { p := 0, mem_Four := LO.Modal.Hilbert.instHasFourNatS4._proof_73 }

instance LO.Modal.Hilbert.instS4NatFormulaS4 : Entailment.Modal.S4 Hilbert.S4

Equations

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

instance LO.Modal.Hilbert.K4_weakerThan_S4 : Hilbert.K4 ⪯ Hilbert.S4

@[reducible, inline]

abbrev LO.Modal.Hilbert.S4Point1 : Hilbert ℕ

Equations

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

instance LO.Modal.Hilbert.instHasKNatS4Point1 : Hilbert.S4Point1.HasK

Equations

• LO.Modal.Hilbert.instHasKNatS4Point1 = { p := 0, q := 1, ne_pq := LO.Modal.Hilbert.instHasKNatKT._proof_19, mem_K := LO.Modal.Hilbert.instHasKNatS4Point1._proof_74 }

instance LO.Modal.Hilbert.instHasTNatS4Point1 : Hilbert.S4Point1.HasT

Equations

• LO.Modal.Hilbert.instHasTNatS4Point1 = { p := 0, mem_T := LO.Modal.Hilbert.instHasTNatS4Point1._proof_75 }

instance LO.Modal.Hilbert.instHasFourNatS4Point1 : Hilbert.S4Point1.HasFour

Equations

• LO.Modal.Hilbert.instHasFourNatS4Point1 = { p := 0, mem_Four := LO.Modal.Hilbert.instHasFourNatS4Point1._proof_76 }

instance LO.Modal.Hilbert.instHasMNatS4Point1 : Hilbert.S4Point1.HasM

Equations

• LO.Modal.Hilbert.instHasMNatS4Point1 = { p := 0, mem_M := LO.Modal.Hilbert.instHasMNatS4Point1._proof_77 }

instance LO.Modal.Hilbert.instS4Point1NatFormulaS4Point1 : Entailment.Modal.S4Point1 Hilbert.S4Point1

Equations

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

instance LO.Modal.Hilbert.K4Point1_weakerThan_S4Point1 : Hilbert.K4Point1 ⪯ Hilbert.S4Point1

@[reducible, inline]

abbrev LO.Modal.Hilbert.S4Point2 : Hilbert ℕ

Equations

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

instance LO.Modal.Hilbert.instHasKNatS4Point2 : Hilbert.S4Point2.HasK

Equations

• LO.Modal.Hilbert.instHasKNatS4Point2 = { p := 0, q := 1, ne_pq := LO.Modal.Hilbert.instHasKNatKT._proof_19, mem_K := LO.Modal.Hilbert.instHasKNatS4Point2._proof_78 }

instance LO.Modal.Hilbert.instHasTNatS4Point2 : Hilbert.S4Point2.HasT

Equations

• LO.Modal.Hilbert.instHasTNatS4Point2 = { p := 0, mem_T := LO.Modal.Hilbert.instHasTNatS4Point2._proof_79 }

instance LO.Modal.Hilbert.instHasFourNatS4Point2 : Hilbert.S4Point2.HasFour

Equations

• LO.Modal.Hilbert.instHasFourNatS4Point2 = { p := 0, mem_Four := LO.Modal.Hilbert.instHasFourNatS4Point2._proof_80 }

instance LO.Modal.Hilbert.instHasPoint2NatS4Point2 : Hilbert.S4Point2.HasPoint2

Equations

• LO.Modal.Hilbert.instHasPoint2NatS4Point2 = { p := 0, mem_Point2 := LO.Modal.Hilbert.instHasPoint2NatS4Point2._proof_81 }

instance LO.Modal.Hilbert.instS4Point2NatFormulaS4Point2 : Entailment.Modal.S4Point2 Hilbert.S4Point2

Equations

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

@[reducible, inline]

abbrev LO.Modal.Hilbert.S4Point3 : Hilbert ℕ

Equations

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

instance LO.Modal.Hilbert.instHasKNatS4Point3 : Hilbert.S4Point3.HasK

Equations

• LO.Modal.Hilbert.instHasKNatS4Point3 = { p := 0, q := 1, ne_pq := LO.Modal.Hilbert.instHasKNatKT._proof_19, mem_K := LO.Modal.Hilbert.instHasKNatS4Point3._proof_82 }

instance LO.Modal.Hilbert.instHasTNatS4Point3 : Hilbert.S4Point3.HasT

Equations

• LO.Modal.Hilbert.instHasTNatS4Point3 = { p := 0, mem_T := LO.Modal.Hilbert.instHasTNatS4Point3._proof_83 }

instance LO.Modal.Hilbert.instHasFourNatS4Point3 : Hilbert.S4Point3.HasFour

Equations

• LO.Modal.Hilbert.instHasFourNatS4Point3 = { p := 0, mem_Four := LO.Modal.Hilbert.instHasFourNatS4Point3._proof_84 }

instance LO.Modal.Hilbert.instHasPoint3NatS4Point3 : Hilbert.S4Point3.HasPoint3

Equations

• LO.Modal.Hilbert.instHasPoint3NatS4Point3 = { p := 0, q := 1, ne_pq := LO.Modal.Hilbert.instHasKNatKT._proof_19, mem_Point3 := LO.Modal.Hilbert.instHasPoint3NatS4Point3._proof_85 }

instance LO.Modal.Hilbert.instS4Point3NatFormulaS4Point3 : Entailment.Modal.S4Point3 Hilbert.S4Point3

Equations

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

@[reducible, inline]

abbrev LO.Modal.Hilbert.K5 : Hilbert ℕ

Equations

• LO.Modal.Hilbert.K5 = { axioms := {LO.Axioms.K (LO.Modal.Formula.atom 0) (LO.Modal.Formula.atom 1), LO.Axioms.Five (LO.Modal.Formula.atom 0)} }

instance LO.Modal.Hilbert.instHasKNatK5 : Hilbert.K5.HasK

Equations

• LO.Modal.Hilbert.instHasKNatK5 = { p := 0, q := 1, ne_pq := LO.Modal.Hilbert.instHasKNatKT._proof_19, mem_K := LO.Modal.Hilbert.instHasKNatK5._proof_86 }

instance LO.Modal.Hilbert.instHasFiveNatK5 : Hilbert.K5.HasFive

Equations

• LO.Modal.Hilbert.instHasFiveNatK5 = { p := 0, mem_Five := LO.Modal.Hilbert.instHasFiveNatK5._proof_87 }

instance LO.Modal.Hilbert.instK5NatFormulaK5 : Entailment.Modal.K5 Hilbert.K5

Equations

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

@[reducible, inline]

abbrev LO.Modal.Hilbert.S5 : Hilbert ℕ

Equations

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

instance LO.Modal.Hilbert.instHasKNatS5 : Hilbert.S5.HasK

Equations

• LO.Modal.Hilbert.instHasKNatS5 = { p := 0, q := 1, ne_pq := LO.Modal.Hilbert.instHasKNatKT._proof_19, mem_K := LO.Modal.Hilbert.instHasKNatS5._proof_88 }

instance LO.Modal.Hilbert.instHasTNatS5 : Hilbert.S5.HasT

Equations

• LO.Modal.Hilbert.instHasTNatS5 = { p := 0, mem_T := LO.Modal.Hilbert.instHasTNatS5._proof_89 }

instance LO.Modal.Hilbert.instHasFiveNatS5 : Hilbert.S5.HasFive

Equations

• LO.Modal.Hilbert.instHasFiveNatS5 = { p := 0, mem_Five := LO.Modal.Hilbert.instHasFiveNatS5._proof_90 }

instance LO.Modal.Hilbert.instS5NatFormulaS5 : Entailment.Modal.S5 Hilbert.S5

Equations

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

@[reducible, inline]

abbrev LO.Modal.Hilbert.GL : Hilbert ℕ

Equations

• LO.Modal.Hilbert.GL = { axioms := {LO.Axioms.K (LO.Modal.Formula.atom 0) (LO.Modal.Formula.atom 1), LO.Axioms.L (LO.Modal.Formula.atom 0)} }

instance LO.Modal.Hilbert.instHasKNatGL : Hilbert.GL.HasK

Equations

• LO.Modal.Hilbert.instHasKNatGL = { p := 0, q := 1, ne_pq := LO.Modal.Hilbert.instHasKNatKT._proof_19, mem_K := LO.Modal.Hilbert.instHasKNatGL._proof_91 }

instance LO.Modal.Hilbert.instHasLNatGL : Hilbert.GL.HasL

Equations

• LO.Modal.Hilbert.instHasLNatGL = { p := 0, mem_L := LO.Modal.Hilbert.instHasLNatGL._proof_92 }

instance LO.Modal.Hilbert.instGLNatFormulaGL : Entailment.Modal.GL Hilbert.GL

Equations

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

@[reducible, inline]

abbrev LO.Modal.Hilbert.GLPoint3 : Hilbert ℕ

Equations

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

instance LO.Modal.Hilbert.instHasKNatGLPoint3 : Hilbert.GLPoint3.HasK

Equations

• LO.Modal.Hilbert.instHasKNatGLPoint3 = { p := 0, q := 1, ne_pq := LO.Modal.Hilbert.instHasKNatKT._proof_19, mem_K := LO.Modal.Hilbert.instHasKNatGLPoint3._proof_93 }

instance LO.Modal.Hilbert.instHasLNatGLPoint3 : Hilbert.GLPoint3.HasL

Equations

• LO.Modal.Hilbert.instHasLNatGLPoint3 = { p := 0, mem_L := LO.Modal.Hilbert.instHasLNatGLPoint3._proof_94 }

instance LO.Modal.Hilbert.instHasWeakPoint3NatGLPoint3 : Hilbert.GLPoint3.HasWeakPoint3

Equations

• LO.Modal.Hilbert.instHasWeakPoint3NatGLPoint3 = { p := 0, q := 1, ne_pq := LO.Modal.Hilbert.instHasKNatKT._proof_19, mem_WeakPoint3 := LO.Modal.Hilbert.instHasWeakPoint3NatGLPoint3._proof_95 }

instance LO.Modal.Hilbert.instGLPoint3NatFormulaGLPoint3 : Entailment.Modal.GLPoint3 Hilbert.GLPoint3

Equations

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

@[reducible, inline]

abbrev LO.Modal.Hilbert.KH : Hilbert ℕ

Equations

• LO.Modal.Hilbert.KH = { axioms := {LO.Axioms.K (LO.Modal.Formula.atom 0) (LO.Modal.Formula.atom 1), LO.Axioms.H (LO.Modal.Formula.atom 0)} }

instance LO.Modal.Hilbert.instHasKNatKH : Hilbert.KH.HasK

Equations

• LO.Modal.Hilbert.instHasKNatKH = { p := 0, q := 1, ne_pq := LO.Modal.Hilbert.instHasKNatKT._proof_19, mem_K := LO.Modal.Hilbert.instHasKNatKH._proof_96 }

instance LO.Modal.Hilbert.instHasHNatKH : Hilbert.KH.HasH

Equations

• LO.Modal.Hilbert.instHasHNatKH = { p := 0, mem_H := LO.Modal.Hilbert.instHasHNatKH._proof_97 }

@[reducible, inline]

abbrev LO.Modal.Hilbert.Grz : Hilbert ℕ

Equations

• LO.Modal.Hilbert.Grz = { axioms := {LO.Axioms.K (LO.Modal.Formula.atom 0) (LO.Modal.Formula.atom 1), LO.Axioms.Grz (LO.Modal.Formula.atom 0)} }

instance LO.Modal.Hilbert.instHasKNatGrz : Hilbert.Grz.HasK

Equations

• LO.Modal.Hilbert.instHasKNatGrz = { p := 0, q := 1, ne_pq := LO.Modal.Hilbert.instHasKNatKT._proof_19, mem_K := LO.Modal.Hilbert.instHasKNatGrz._proof_98 }

instance LO.Modal.Hilbert.instHasGrzNatGrz : Hilbert.Grz.HasGrz

Equations

• LO.Modal.Hilbert.instHasGrzNatGrz = { p := 0, mem_Grz := LO.Modal.Hilbert.instHasGrzNatGrz._proof_99 }

instance LO.Modal.Hilbert.instGrzNatFormulaGrz : Entailment.Modal.Grz Hilbert.Grz

Equations

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

@[reducible, inline]

abbrev LO.Modal.Hilbert.GrzPoint2 : Hilbert ℕ

Equations

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

instance LO.Modal.Hilbert.instHasKNatGrzPoint2 : Hilbert.GrzPoint2.HasK

Equations

• LO.Modal.Hilbert.instHasKNatGrzPoint2 = { p := 0, q := 1, ne_pq := LO.Modal.Hilbert.instHasKNatKT._proof_19, mem_K := LO.Modal.Hilbert.instHasKNatGrzPoint2._proof_100 }

instance LO.Modal.Hilbert.instHasGrzNatGrzPoint2 : Hilbert.GrzPoint2.HasGrz

Equations

• LO.Modal.Hilbert.instHasGrzNatGrzPoint2 = { p := 0, mem_Grz := LO.Modal.Hilbert.instHasGrzNatGrzPoint2._proof_101 }

instance LO.Modal.Hilbert.instHasPoint2NatGrzPoint2 : Hilbert.GrzPoint2.HasPoint2

Equations

• LO.Modal.Hilbert.instHasPoint2NatGrzPoint2 = { p := 0, mem_Point2 := LO.Modal.Hilbert.instHasPoint2NatGrzPoint2._proof_102 }

instance LO.Modal.Hilbert.instGrzNatFormulaGrzPoint2 : Entailment.Modal.Grz Hilbert.GrzPoint2

Equations

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

@[reducible, inline]

abbrev LO.Modal.Hilbert.GrzPoint3 : Hilbert ℕ

Equations

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

instance LO.Modal.Hilbert.instHasKNatGrzPoint3 : Hilbert.GrzPoint3.HasK

Equations

• LO.Modal.Hilbert.instHasKNatGrzPoint3 = { p := 0, q := 1, ne_pq := LO.Modal.Hilbert.instHasKNatKT._proof_19, mem_K := LO.Modal.Hilbert.instHasKNatGrzPoint3._proof_103 }

instance LO.Modal.Hilbert.instHasGrzNatGrzPoint3 : Hilbert.GrzPoint3.HasGrz

Equations

• LO.Modal.Hilbert.instHasGrzNatGrzPoint3 = { p := 0, mem_Grz := LO.Modal.Hilbert.instHasGrzNatGrzPoint3._proof_104 }

instance LO.Modal.Hilbert.instHasPoint3NatGrzPoint3 : Hilbert.GrzPoint3.HasPoint3

Equations

• LO.Modal.Hilbert.instHasPoint3NatGrzPoint3 = { p := 0, q := 1, ne_pq := LO.Modal.Hilbert.instHasKNatKT._proof_19, mem_Point3 := LO.Modal.Hilbert.instHasPoint3NatGrzPoint3._proof_105 }

instance LO.Modal.Hilbert.instGrzNatFormulaGrzPoint3 : Entailment.Modal.Grz Hilbert.GrzPoint3

Equations

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

theorem LO.Modal.Hilbert.KT_weakerThan_Grz : Hilbert.KT ⪯ Hilbert.Grz

@[reducible, inline]

abbrev LO.Modal.Hilbert.Ver : Hilbert ℕ

Equations

• LO.Modal.Hilbert.Ver = { axioms := {LO.Axioms.K (LO.Modal.Formula.atom 0) (LO.Modal.Formula.atom 1), LO.Axioms.Ver (LO.Modal.Formula.atom 0)} }

instance LO.Modal.Hilbert.instHasKNatVer : Hilbert.Ver.HasK

Equations

• LO.Modal.Hilbert.instHasKNatVer = { p := 0, q := 1, ne_pq := LO.Modal.Hilbert.instHasKNatKT._proof_19, mem_K := LO.Modal.Hilbert.instHasKNatVer._proof_106 }

instance LO.Modal.Hilbert.instHasVerNatVer : Hilbert.Ver.HasVer

Equations

• LO.Modal.Hilbert.instHasVerNatVer = { p := 0, mem_Ver := LO.Modal.Hilbert.instHasVerNatVer._proof_107 }

instance LO.Modal.Hilbert.instVerNatFormulaVer : Entailment.Modal.Ver Hilbert.Ver

Equations

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

@[reducible, inline]

abbrev LO.Modal.Hilbert.Triv : Hilbert ℕ

Equations

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

instance LO.Modal.Hilbert.instHasKNatTriv : Hilbert.Triv.HasK

Equations

• LO.Modal.Hilbert.instHasKNatTriv = { p := 0, q := 1, ne_pq := LO.Modal.Hilbert.instHasKNatKT._proof_19, mem_K := LO.Modal.Hilbert.instHasKNatTriv._proof_108 }

instance LO.Modal.Hilbert.instHasTNatTriv : Hilbert.Triv.HasT

Equations

• LO.Modal.Hilbert.instHasTNatTriv = { p := 0, mem_T := LO.Modal.Hilbert.instHasTNatTriv._proof_109 }

instance LO.Modal.Hilbert.instHasTcNatTriv : Hilbert.Triv.HasTc

Equations

• LO.Modal.Hilbert.instHasTcNatTriv = { p := 0, mem_Tc := LO.Modal.Hilbert.instHasTcNatTriv._proof_110 }

instance LO.Modal.Hilbert.instTrivNatFormulaTriv : Entailment.Modal.Triv Hilbert.Triv

Equations

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

theorem LO.Modal.Hilbert.K4_weakerThan_Triv : Hilbert.K4 ⪯ Hilbert.Triv

@[reducible, inline]

abbrev LO.Modal.Hilbert.KTc : Hilbert ℕ

Equations

• LO.Modal.Hilbert.KTc = { axioms := {LO.Axioms.K (LO.Modal.Formula.atom 0) (LO.Modal.Formula.atom 1), LO.Axioms.Tc (LO.Modal.Formula.atom 0)} }

instance LO.Modal.Hilbert.instHasKNatKTc : Hilbert.KTc.HasK

Equations

• LO.Modal.Hilbert.instHasKNatKTc = { p := 0, q := 1, ne_pq := LO.Modal.Hilbert.instHasKNatKT._proof_19, mem_K := LO.Modal.Hilbert.instHasKNatKTc._proof_111 }

instance LO.Modal.Hilbert.instHasTcNatKTc : Hilbert.KTc.HasTc

Equations

• LO.Modal.Hilbert.instHasTcNatKTc = { p := 0, mem_Tc := LO.Modal.Hilbert.instHasTcNatKTc._proof_112 }

instance LO.Modal.Hilbert.instKTcNatFormulaKTc : Entailment.Modal.KTc Hilbert.KTc

Equations

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

@[reducible, inline]

abbrev LO.Modal.Hilbert.KD4Point3Z : Hilbert ℕ

Equations

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

instance LO.Modal.Hilbert.instHasKNatKD4Point3Z : Hilbert.KD4Point3Z.HasK

Equations

• LO.Modal.Hilbert.instHasKNatKD4Point3Z = { p := 0, q := 1, ne_pq := LO.Modal.Hilbert.instHasKNatKT._proof_19, mem_K := LO.Modal.Hilbert.instHasKNatKD4Point3Z._proof_113 }

instance LO.Modal.Hilbert.instHasDNatKD4Point3Z : Hilbert.KD4Point3Z.HasD

Equations

• LO.Modal.Hilbert.instHasDNatKD4Point3Z = { p := 0, mem_D := LO.Modal.Hilbert.instHasDNatKD4Point3Z._proof_114 }

instance LO.Modal.Hilbert.instHasFourNatKD4Point3Z : Hilbert.KD4Point3Z.HasFour

Equations

• LO.Modal.Hilbert.instHasFourNatKD4Point3Z = { p := 0, mem_Four := LO.Modal.Hilbert.instHasFourNatKD4Point3Z._proof_115 }

instance LO.Modal.Hilbert.instHasWeakPoint3NatKD4Point3Z : Hilbert.KD4Point3Z.HasWeakPoint3

Equations

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

instance LO.Modal.Hilbert.instHasZNatKD4Point3Z : Hilbert.KD4Point3Z.HasZ

Equations

• LO.Modal.Hilbert.instHasZNatKD4Point3Z = { p := 0, mem_Z := LO.Modal.Hilbert.instHasZNatKD4Point3Z._proof_117 }

instance LO.Modal.Hilbert.instKD4Point3ZNatFormulaKD4Point3Z : Entailment.Modal.KD4Point3Z Hilbert.KD4Point3Z

Equations

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

@[reducible, inline]

abbrev LO.Modal.Hilbert.KTMk : Hilbert ℕ

Equations

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

instance LO.Modal.Hilbert.instHasKNatKTMk : Hilbert.KTMk.HasK

Equations

• LO.Modal.Hilbert.instHasKNatKTMk = { p := 0, q := 1, ne_pq := LO.Modal.Hilbert.instHasKNatKT._proof_19, mem_K := LO.Modal.Hilbert.instHasKNatKTMk._proof_118 }

instance LO.Modal.Hilbert.instHasTNatKTMk : Hilbert.KTMk.HasT

Equations

• LO.Modal.Hilbert.instHasTNatKTMk = { p := 0, mem_T := LO.Modal.Hilbert.instHasTNatKTMk._proof_119 }

instance LO.Modal.Hilbert.instHasMkNatKTMk : Hilbert.KTMk.HasMk

Equations

• LO.Modal.Hilbert.instHasMkNatKTMk = { p := 0, q := 1, ne_pq := LO.Modal.Hilbert.instHasKNatKT._proof_19, mem_Mk := LO.Modal.Hilbert.instHasMkNatKTMk._proof_120 }

instance LO.Modal.Hilbert.instKTMkNatFormulaKTMk : Entailment.Modal.KTMk Hilbert.KTMk

Equations

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

@[reducible, inline]

abbrev LO.Modal.Hilbert.N : Hilbert ℕ

Equations

• LO.Modal.Hilbert.N = { axioms := ∅ }