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 ⋯ }

@[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_1, mem_K := LO.Modal.Hilbert.instHasKNatKT.proof_2 }

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

Equations

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

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

Equations

• LO.Modal.Hilbert.instKTNatFormulaKT = LO.Entailment.Modal.KT.mk

@[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.instHasKNatKD.proof_1, mem_K := LO.Modal.Hilbert.instHasKNatKD.proof_2 }

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

Equations

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

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

Equations

• LO.Modal.Hilbert.instKDNatFormulaKD = LO.Entailment.Modal.KD.mk

@[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.instHasKNatKB.proof_1, mem_K := LO.Modal.Hilbert.instHasKNatKB.proof_2 }

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

Equations

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

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

Equations

• LO.Modal.Hilbert.instKBNatFormulaKB = LO.Entailment.Modal.KB.mk

@[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.instHasKNatKDB.proof_1, mem_K := LO.Modal.Hilbert.instHasKNatKDB.proof_2 }

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

Equations

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

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

Equations

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

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

Equations

• LO.Modal.Hilbert.instKDBNatFormulaKDB = LO.Entailment.Modal.KDB.mk

@[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.instHasKNatKTB.proof_1, mem_K := LO.Modal.Hilbert.instHasKNatKTB.proof_2 }

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

Equations

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

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

Equations

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

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

Equations

• LO.Modal.Hilbert.instKTBNatFormulaKTB = LO.Entailment.Modal.KTB.mk

@[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.instHasKNatK4.proof_1, mem_K := LO.Modal.Hilbert.instHasKNatK4.proof_2 }

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

Equations

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

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

Equations

• LO.Modal.Hilbert.instK4NatFormulaK4 = LO.Entailment.Modal.K4.mk

@[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.instHasKNatK4Point2.proof_1, mem_K := LO.Modal.Hilbert.instHasKNatK4Point2.proof_2 }

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

Equations

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

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

Equations

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

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

Equations

• LO.Modal.Hilbert.instK4Point2NatFormulaK4Point2 = LO.Entailment.Modal.K4Point2.mk

@[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.instHasKNatK4Point3.proof_1, mem_K := LO.Modal.Hilbert.instHasKNatK4Point3.proof_2 }

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

Equations

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

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

Equations

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

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

Equations

• LO.Modal.Hilbert.instK4Point3NatFormulaK4Point3 = LO.Entailment.Modal.K4Point3.mk

@[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.instHasKNatKT4B.proof_1, mem_K := LO.Modal.Hilbert.instHasKNatKT4B.proof_2 }

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• LO.Modal.Hilbert.instKT4BNatFormulaKT4B = LO.Entailment.Modal.KT4B.mk

@[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.instHasKNatK45.proof_1, mem_K := LO.Modal.Hilbert.instHasKNatK45.proof_2 }

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

Equations

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

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

Equations

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

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

Equations

• LO.Modal.Hilbert.instK45NatFormulaK45 = LO.Entailment.Modal.K45.mk

@[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.instHasKNatKD4.proof_1, mem_K := LO.Modal.Hilbert.instHasKNatKD4.proof_2 }

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

Equations

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

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

Equations

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

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

Equations

• LO.Modal.Hilbert.instKD4NatFormulaKD4 = LO.Entailment.Modal.KD4.mk

@[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.instHasKNatKD5.proof_1, mem_K := LO.Modal.Hilbert.instHasKNatKD5.proof_2 }

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

Equations

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

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

Equations

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

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

Equations

• LO.Modal.Hilbert.instKD5NatFormulaKD5 = LO.Entailment.Modal.KD5.mk

@[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.instHasKNatKD45.proof_1, mem_K := LO.Modal.Hilbert.instHasKNatKD45.proof_2 }

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• LO.Modal.Hilbert.instKD45NatFormulaKD45 = LO.Entailment.Modal.KD45.mk

@[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.instHasKNatKB4.proof_1, mem_K := LO.Modal.Hilbert.instHasKNatKB4.proof_2 }

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

Equations

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

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

Equations

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

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

Equations

• LO.Modal.Hilbert.instKB4NatFormulaKB4 = LO.Entailment.Modal.KB4.mk

@[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.instHasKNatKB5.proof_1, mem_K := LO.Modal.Hilbert.instHasKNatKB5.proof_2 }

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

Equations

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

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

Equations

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

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

Equations

• LO.Modal.Hilbert.instKB5NatFormulaKB5 = LO.Entailment.Modal.KB5.mk

@[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.instHasKNatS4.proof_1, mem_K := LO.Modal.Hilbert.instHasKNatS4.proof_2 }

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

Equations

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

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

Equations

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

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

Equations

• LO.Modal.Hilbert.instS4NatFormulaS4 = LO.Entailment.Modal.S4.mk

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

@[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.instHasKNatS4Point2.proof_1, mem_K := LO.Modal.Hilbert.instHasKNatS4Point2.proof_2 }

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• LO.Modal.Hilbert.instS4Point2NatFormulaS4Point2 = LO.Entailment.Modal.S4Point2.mk

@[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.instHasKNatS4Point3.proof_1, mem_K := LO.Modal.Hilbert.instHasKNatS4Point3.proof_2 }

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

Equations

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

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

Equations

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

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

Equations

• LO.Modal.Hilbert.instHasPoint3NatS4Point3 = { p := 0, q := 1, ne_pq := LO.Modal.Hilbert.instHasPoint3NatS4Point3.proof_1, mem_Point3 := LO.Modal.Hilbert.instHasPoint3NatS4Point3.proof_2 }

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

Equations

• LO.Modal.Hilbert.instS4Point3NatFormulaS4Point3 = LO.Entailment.Modal.S4Point3.mk

@[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.instHasKNatK5.proof_1, mem_K := LO.Modal.Hilbert.instHasKNatK5.proof_2 }

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

Equations

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

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

Equations

• LO.Modal.Hilbert.instK5NatFormulaK5 = LO.Entailment.Modal.K5.mk

@[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.instHasKNatS5.proof_1, mem_K := LO.Modal.Hilbert.instHasKNatS5.proof_2 }

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

Equations

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

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

Equations

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

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

Equations

• LO.Modal.Hilbert.instS5NatFormulaS5 = LO.Entailment.Modal.S5.mk

@[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.instHasKNatGL.proof_1, mem_K := LO.Modal.Hilbert.instHasKNatGL.proof_2 }

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

Equations

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

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

Equations

• LO.Modal.Hilbert.instGLNatFormulaGL = LO.Entailment.Modal.GL.mk

@[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.instHasKNatGLPoint3.proof_1, mem_K := LO.Modal.Hilbert.instHasKNatGLPoint3.proof_2 }

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

Equations

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

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

Equations

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

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

Equations

• LO.Modal.Hilbert.instGLPoint3NatFormulaGLPoint3 = LO.Entailment.Modal.GLPoint3.mk

@[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.instHasKNatKH.proof_1, mem_K := LO.Modal.Hilbert.instHasKNatKH.proof_2 }

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

Equations

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

@[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.instHasKNatGrz.proof_1, mem_K := LO.Modal.Hilbert.instHasKNatGrz.proof_2 }

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

Equations

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

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

Equations

• LO.Modal.Hilbert.instGrzNatFormulaGrz = LO.Entailment.Modal.Grz.mk

@[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.instHasKNatGrzPoint2.proof_1, mem_K := LO.Modal.Hilbert.instHasKNatGrzPoint2.proof_2 }

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

Equations

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

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

Equations

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

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

Equations

• LO.Modal.Hilbert.instGrzNatFormulaGrzPoint2 = LO.Entailment.Modal.Grz.mk

@[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.instHasKNatGrzPoint3.proof_1, mem_K := LO.Modal.Hilbert.instHasKNatGrzPoint3.proof_2 }

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

Equations

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

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

Equations

• LO.Modal.Hilbert.instHasPoint3NatGrzPoint3 = { p := 0, q := 1, ne_pq := LO.Modal.Hilbert.instHasPoint3NatGrzPoint3.proof_1, mem_Point3 := LO.Modal.Hilbert.instHasPoint3NatGrzPoint3.proof_2 }

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

Equations

• LO.Modal.Hilbert.instGrzNatFormulaGrzPoint3 = LO.Entailment.Modal.Grz.mk

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.instHasKNatVer.proof_1, mem_K := LO.Modal.Hilbert.instHasKNatVer.proof_2 }

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

Equations

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

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

Equations

• LO.Modal.Hilbert.instVerNatFormulaVer = LO.Entailment.Modal.Ver.mk

@[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.instHasKNatTriv.proof_1, mem_K := LO.Modal.Hilbert.instHasKNatTriv.proof_2 }

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

Equations

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

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

Equations

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

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

Equations

• LO.Modal.Hilbert.instTrivNatFormulaTriv = LO.Entailment.Modal.Triv.mk

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.instHasKNatKTc.proof_1, mem_K := LO.Modal.Hilbert.instHasKNatKTc.proof_2 }

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

Equations

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

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

Equations

• LO.Modal.Hilbert.instKTcNatFormulaKTc = LO.Entailment.Modal.KTc.mk

@[reducible, inline]

abbrev LO.Modal.Hilbert.N : Hilbert ℕ

Equations

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