WellKnown

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

Imported declaration from the Incompleteness formalization.

• p : α

  Imported declaration from the Incompleteness formalization.

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

@[implicit_reducible]

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

Imported declaration from the Incompleteness formalization.

• p : α

  Imported declaration from the Incompleteness formalization.

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

@[implicit_reducible]

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

Imported declaration from the Incompleteness formalization.

• p : α

  Imported declaration from the Incompleteness formalization.

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

@[implicit_reducible]

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

Imported declaration from the Incompleteness formalization.

• p : α

  Imported declaration from the Incompleteness formalization.

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

@[implicit_reducible]

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

Imported declaration from the Incompleteness formalization.

• p : α

  Imported declaration from the Incompleteness formalization.

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

@[implicit_reducible]

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.HasDot2 {α : Type u_1} (H : Hilbert α) : Type u_1

Imported declaration from the Incompleteness formalization.

• p : α

  Imported declaration from the Incompleteness formalization.

• mem_Dot2 : Axioms.Dot2 (Formula.atom (p H)) ∈ H.axioms

@[implicit_reducible]

instance LO.Modal.Hilbert.instHasAxiomDot2FormulaOfHasDot2 {α : Type u_1} {H : Hilbert α} [DecidableEq α] [hDot2 : H.HasDot2] : Entailment.HasAxiomDot2 H

Equations

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

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

Imported declaration from the Incompleteness formalization.

• p : α

  Imported declaration from the Incompleteness formalization.

• q : α

  Imported declaration from the Incompleteness formalization.

• ne_pq : p H ≠ q H
• mem_Dot3 : Axioms.Dot3 (Formula.atom (p H)) (Formula.atom (q H)) ∈ H.axioms

@[implicit_reducible]

instance LO.Modal.Hilbert.instHasAxiomDot3FormulaOfHasDot3 {α : Type u_1} {H : Hilbert α} [DecidableEq α] [hDot3 : H.HasDot3] : Entailment.HasAxiomDot3 H

Equations

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

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

Imported declaration from the Incompleteness formalization.

• p : α

  Imported declaration from the Incompleteness formalization.

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

@[implicit_reducible]

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

Imported declaration from the Incompleteness formalization.

• p : α

  Imported declaration from the Incompleteness formalization.

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

@[implicit_reducible]

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

Imported declaration from the Incompleteness formalization.

• p : α

  Imported declaration from the Incompleteness formalization.

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

@[implicit_reducible]

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

Imported declaration from the Incompleteness formalization.

• p : α

  Imported declaration from the Incompleteness formalization.

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

@[implicit_reducible]

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

Equations

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

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

Imported declaration from the Incompleteness formalization.

• p : α

  Imported declaration from the Incompleteness formalization.

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

@[implicit_reducible]

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 ℕ

Imported declaration from the Incompleteness formalization.

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

@[implicit_reducible]

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 }

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[reducible, inline]

abbrev LO.Modal.Hilbert.KD : Hilbert ℕ

Imported declaration from the Incompleteness formalization.

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[reducible, inline]

abbrev LO.Modal.Hilbert.KB : Hilbert ℕ

Imported declaration from the Incompleteness formalization.

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[reducible, inline]

abbrev LO.Modal.Hilbert.KDB : Hilbert ℕ

Imported declaration from the Incompleteness formalization.

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[reducible, inline]

abbrev LO.Modal.Hilbert.KTB : Hilbert ℕ

Imported declaration from the Incompleteness formalization.

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[reducible, inline]

abbrev LO.Modal.Hilbert.K4 : Hilbert ℕ

Imported declaration from the Incompleteness formalization.

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[reducible, inline]

abbrev LO.Modal.Hilbert.KT4B : Hilbert ℕ

Imported declaration from the Incompleteness formalization.

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[reducible, inline]

abbrev LO.Modal.Hilbert.K45 : Hilbert ℕ

Imported declaration from the Incompleteness formalization.

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[reducible, inline]

abbrev LO.Modal.Hilbert.KD4 : Hilbert ℕ

Imported declaration from the Incompleteness formalization.

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[reducible, inline]

abbrev LO.Modal.Hilbert.KD5 : Hilbert ℕ

Imported declaration from the Incompleteness formalization.

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[reducible, inline]

abbrev LO.Modal.Hilbert.KD45 : Hilbert ℕ

Imported declaration from the Incompleteness formalization.

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[reducible, inline]

abbrev LO.Modal.Hilbert.KB4 : Hilbert ℕ

Imported declaration from the Incompleteness formalization.

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[reducible, inline]

abbrev LO.Modal.Hilbert.KB5 : Hilbert ℕ

Imported declaration from the Incompleteness formalization.

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[reducible, inline]

abbrev LO.Modal.Hilbert.S4 : Hilbert ℕ

Imported declaration from the Incompleteness formalization.

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

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

@[reducible, inline]

abbrev LO.Modal.Hilbert.S4Dot2 : Hilbert ℕ

Imported declaration from the Incompleteness formalization.

Equations

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

@[implicit_reducible]

instance LO.Modal.Hilbert.instHasKNatS4Dot2 : Hilbert.S4Dot2.HasK

Equations

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

@[implicit_reducible]

instance LO.Modal.Hilbert.instHasTNatS4Dot2 : Hilbert.S4Dot2.HasT

Equations

• LO.Modal.Hilbert.instHasTNatS4Dot2 = { p := 0, mem_T := LO.Modal.Hilbert.instHasTNatS4Dot2._proof_1 }

@[implicit_reducible]

instance LO.Modal.Hilbert.instHasFourNatS4Dot2 : Hilbert.S4Dot2.HasFour

Equations

• LO.Modal.Hilbert.instHasFourNatS4Dot2 = { p := 0, mem_Four := LO.Modal.Hilbert.instHasFourNatS4Dot2._proof_1 }

@[implicit_reducible]

instance LO.Modal.Hilbert.instHasDot2NatS4Dot2 : Hilbert.S4Dot2.HasDot2

Equations

• LO.Modal.Hilbert.instHasDot2NatS4Dot2 = { p := 0, mem_Dot2 := LO.Modal.Hilbert.instHasDot2NatS4Dot2._proof_1 }

@[implicit_reducible]

instance LO.Modal.Hilbert.instS4Dot2NatFormulaS4Dot2 : Entailment.S4Dot2 Hilbert.S4Dot2

Equations

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

@[reducible, inline]

abbrev LO.Modal.Hilbert.S4Dot3 : Hilbert ℕ

Imported declaration from the Incompleteness formalization.

Equations

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

@[implicit_reducible]

instance LO.Modal.Hilbert.instHasKNatS4Dot3 : Hilbert.S4Dot3.HasK

Equations

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

@[implicit_reducible]

instance LO.Modal.Hilbert.instHasTNatS4Dot3 : Hilbert.S4Dot3.HasT

Equations

• LO.Modal.Hilbert.instHasTNatS4Dot3 = { p := 0, mem_T := LO.Modal.Hilbert.instHasTNatS4Dot3._proof_1 }

@[implicit_reducible]

instance LO.Modal.Hilbert.instHasFourNatS4Dot3 : Hilbert.S4Dot3.HasFour

Equations

• LO.Modal.Hilbert.instHasFourNatS4Dot3 = { p := 0, mem_Four := LO.Modal.Hilbert.instHasFourNatS4Dot3._proof_1 }

@[implicit_reducible]

instance LO.Modal.Hilbert.instHasDot3NatS4Dot3 : Hilbert.S4Dot3.HasDot3

Equations

• LO.Modal.Hilbert.instHasDot3NatS4Dot3 = { p := 0, q := 1, ne_pq := LO.Modal.Hilbert.instHasKNatKT._proof_1, mem_Dot3 := LO.Modal.Hilbert.instHasDot3NatS4Dot3._proof_1 }

@[implicit_reducible]

instance LO.Modal.Hilbert.instS4Dot3NatFormulaS4Dot3 : Entailment.S4Dot3 Hilbert.S4Dot3

Equations

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

@[reducible, inline]

abbrev LO.Modal.Hilbert.K5 : Hilbert ℕ

Imported declaration from the Incompleteness formalization.

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[reducible, inline]

abbrev LO.Modal.Hilbert.S5 : Hilbert ℕ

Imported declaration from the Incompleteness formalization.

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[reducible, inline]

abbrev LO.Modal.Hilbert.GL : Hilbert ℕ

Imported declaration from the Incompleteness formalization.

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[reducible, inline]

abbrev LO.Modal.Hilbert.KH : Hilbert ℕ

Imported declaration from the Incompleteness formalization.

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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 ℕ

Imported declaration from the Incompleteness formalization.

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

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

@[reducible, inline]

abbrev LO.Modal.Hilbert.Ver : Hilbert ℕ

Imported declaration from the Incompleteness formalization.

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[reducible, inline]

abbrev LO.Modal.Hilbert.Triv : Hilbert ℕ

Imported declaration from the Incompleteness formalization.

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

instance LO.Modal.Hilbert.instTrivNatFormulaTriv : Entailment.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 wkn Hilbert.Triv

@[reducible, inline]

abbrev LO.Modal.Hilbert.N : Hilbert ℕ

Imported declaration from the Incompleteness formalization.

Equations

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