instance LO.Modal.Hilbert.KD.Kripke.sound : LO.Sound (LO.Modal.Hilbert.KD ℕ) LO.Modal.Kripke.SerialFrameClass

Equations

• LO.Modal.Hilbert.KD.Kripke.sound = ⋯

instance LO.Modal.Hilbert.KD.consistent : LO.System.Consistent (LO.Modal.Hilbert.KD ℕ)

Equations

• LO.Modal.Hilbert.KD.consistent = ⋯

instance LO.Modal.Hilbert.KT.Kripke.sound : LO.Sound (LO.Modal.Hilbert.KT ℕ) LO.Modal.Kripke.ReflexiveFrameClass

Equations

• LO.Modal.Hilbert.KT.Kripke.sound = ⋯

instance LO.Modal.Hilbert.KT.consistent : LO.System.Consistent (LO.Modal.Hilbert.KT ℕ)

Equations

• LO.Modal.Hilbert.KT.consistent = ⋯

instance LO.Modal.Hilbert.KT.Kripke.complete : LO.Complete (LO.Modal.Hilbert.KT ℕ) LO.Modal.Kripke.ReflexiveFrameClass

Equations

• LO.Modal.Hilbert.KT.Kripke.complete = ⋯

instance LO.Modal.Hilbert.KB.Kripke.sound : LO.Sound (LO.Modal.Hilbert.KB ℕ) LO.Modal.Kripke.SymmetricFrameClass

Equations

• LO.Modal.Hilbert.KB.Kripke.sound = ⋯

instance LO.Modal.Hilbert.KB.consistent : LO.System.Consistent (LO.Modal.Hilbert.KB ℕ)

Equations

• LO.Modal.Hilbert.KB.consistent = ⋯

instance LO.Modal.Hilbert.KB.Kripke.complete : LO.Complete (LO.Modal.Hilbert.KB ℕ) LO.Modal.Kripke.SymmetricFrameClass

Equations

• LO.Modal.Hilbert.KB.Kripke.complete = ⋯

instance LO.Modal.Hilbert.KTB.Kripke.sound : LO.Sound (LO.Modal.Hilbert.KTB ℕ) LO.Modal.Kripke.ReflexiveSymmetricFrameClass

Equations

• LO.Modal.Hilbert.KTB.Kripke.sound = ⋯

instance LO.Modal.Hilbert.KTB.consistent : LO.System.Consistent (LO.Modal.Hilbert.KTB ℕ)

Equations

• LO.Modal.Hilbert.KTB.consistent = ⋯

instance LO.Modal.Hilbert.KTB.Kripke.complete : LO.Complete (LO.Modal.Hilbert.KTB ℕ) LO.Modal.Kripke.ReflexiveSymmetricFrameClass

Equations

• LO.Modal.Hilbert.KTB.Kripke.complete = ⋯

instance LO.Modal.Hilbert.K4.Kripke.sound : LO.Sound (LO.Modal.Hilbert.K4 ℕ) LO.Modal.Kripke.TransitiveFrameClass

Equations

• LO.Modal.Hilbert.K4.Kripke.sound = ⋯

instance LO.Modal.Hilbert.K4.consistent : LO.System.Consistent (LO.Modal.Hilbert.K4 ℕ)

Equations

• LO.Modal.Hilbert.K4.consistent = ⋯

instance LO.Modal.Hilbert.K4.Kripke.complete : LO.Complete (LO.Modal.Hilbert.K4 ℕ) LO.Modal.Kripke.TransitiveFrameClass

Equations

• LO.Modal.Hilbert.K4.Kripke.complete = ⋯

instance LO.Modal.Hilbert.K5.Kripke.sound : LO.Sound (LO.Modal.Hilbert.K5 ℕ) LO.Modal.Kripke.EuclideanFrameClass

Equations

• LO.Modal.Hilbert.K5.Kripke.sound = ⋯

instance LO.Modal.Hilbert.K5.consistent : LO.System.Consistent (LO.Modal.Hilbert.K5 ℕ)

Equations

• LO.Modal.Hilbert.K5.consistent = ⋯

instance LO.Modal.Hilbert.K5.Kripke.complete : LO.Complete (LO.Modal.Hilbert.K5 ℕ) LO.Modal.Kripke.EuclideanFrameClass

Equations

• LO.Modal.Hilbert.K5.Kripke.complete = ⋯

instance LO.Modal.Hilbert.S4.Kripke.sound : LO.Sound (LO.Modal.Hilbert.S4 ℕ) LO.Modal.Kripke.ReflexiveTransitiveFrameClass

Equations

• LO.Modal.Hilbert.S4.Kripke.sound = ⋯

instance LO.Modal.Hilbert.S4.consistent : LO.System.Consistent (LO.Modal.Hilbert.S4 ℕ)

Equations

• LO.Modal.Hilbert.S4.consistent = ⋯

instance LO.Modal.Hilbert.S4.Kripke.complete : LO.Complete (LO.Modal.Hilbert.S4 ℕ) LO.Modal.Kripke.ReflexiveTransitiveFrameClass

Equations

• LO.Modal.Hilbert.S4.Kripke.complete = ⋯

instance LO.Modal.Hilbert.S5.Kripke.sound : LO.Sound (LO.Modal.Hilbert.S5 ℕ) LO.Modal.Kripke.ReflexiveEuclideanFrameClass

Equations

• LO.Modal.Hilbert.S5.Kripke.sound = ⋯

instance LO.Modal.Hilbert.S5.consistent : LO.System.Consistent (LO.Modal.Hilbert.S5 ℕ)

Equations

• LO.Modal.Hilbert.S5.consistent = ⋯

instance LO.Modal.Hilbert.S5.Kripke.complete : LO.Complete (LO.Modal.Hilbert.S5 ℕ) LO.Modal.Kripke.ReflexiveEuclideanFrameClass

Equations

• LO.Modal.Hilbert.S5.Kripke.complete = ⋯

instance LO.Modal.Hilbert.KT4B.Kripke.sound : LO.Sound (LO.Modal.Hilbert.KT4B ℕ) LO.Modal.Kripke.ReflexiveTransitiveSymmetricFrameClass

Equations

• LO.Modal.Hilbert.KT4B.Kripke.sound = ⋯

instance LO.Modal.Hilbert.KT4B.consistent : LO.System.Consistent (LO.Modal.Hilbert.KT4B ℕ)

Equations

• LO.Modal.Hilbert.KT4B.consistent = ⋯

instance LO.Modal.Hilbert.KT4B.Kripke.complete : LO.Complete (LO.Modal.Hilbert.KT4B ℕ) LO.Modal.Kripke.ReflexiveTransitiveSymmetricFrameClass

Equations

• LO.Modal.Hilbert.KT4B.Kripke.complete = ⋯

instance LO.Modal.Hilbert.KD45.Kripke.sound : LO.Sound (LO.Modal.Hilbert.KD45 ℕ) LO.Modal.Kripke.SerialTransitiveEuclideanFrameClass

Equations

• LO.Modal.Hilbert.KD45.Kripke.sound = ⋯

instance LO.Modal.Hilbert.KD45.consistent : LO.System.Consistent (LO.Modal.Hilbert.KD45 ℕ)

Equations

• LO.Modal.Hilbert.KD45.consistent = ⋯

instance LO.Modal.Hilbert.KD45.Kripke.complete : LO.Complete (LO.Modal.Hilbert.KD45 ℕ) LO.Modal.Kripke.SerialTransitiveEuclideanFrameClass

Equations

• LO.Modal.Hilbert.KD45.Kripke.complete = ⋯

instance LO.Modal.Hilbert.K45.Kripke.sound : LO.Sound (LO.Modal.Hilbert.K45 ℕ) LO.Modal.Kripke.TransitiveEuclideanFrameClass

Equations

• LO.Modal.Hilbert.K45.Kripke.sound = ⋯

instance LO.Modal.Hilbert.K45.consistent : LO.System.Consistent (LO.Modal.Hilbert.K45 ℕ)

Equations

• LO.Modal.Hilbert.K45.consistent = ⋯

instance LO.Modal.Hilbert.K45.Kripke.complete : LO.Complete (LO.Modal.Hilbert.K45 ℕ) LO.Modal.Kripke.TransitiveEuclideanFrameClass

Equations

• LO.Modal.Hilbert.K45.Kripke.complete = ⋯

instance LO.Modal.Hilbert.KB4.Kripke.sound : LO.Sound (LO.Modal.Hilbert.KB4 ℕ) LO.Modal.Kripke.SymmetricTransitiveFrameClass

Equations

• LO.Modal.Hilbert.KB4.Kripke.sound = ⋯

instance LO.Modal.Hilbert.KB4.consistent : LO.System.Consistent (LO.Modal.Hilbert.KB4 ℕ)

Equations

• LO.Modal.Hilbert.KB4.consistent = ⋯

instance LO.Modal.Hilbert.KB4.Kripke.complete : LO.Complete (LO.Modal.Hilbert.KB4 ℕ) LO.Modal.Kripke.SymmetricTransitiveFrameClass

Equations

• LO.Modal.Hilbert.KB4.Kripke.complete = ⋯

instance LO.Modal.Hilbert.KB5.Kripke.sound : LO.Sound (LO.Modal.Hilbert.KB5 ℕ) LO.Modal.Kripke.SymmetricEuclideanFrameClass

Equations

• LO.Modal.Hilbert.KB5.Kripke.sound = ⋯

instance LO.Modal.Hilbert.KB5.consistent : LO.System.Consistent (LO.Modal.Hilbert.KB5 ℕ)

Equations

• LO.Modal.Hilbert.KB5.consistent = ⋯

instance LO.Modal.Hilbert.KB5.Kripke.complete : LO.Complete (LO.Modal.Hilbert.KB5 ℕ) LO.Modal.Kripke.SymmetricEuclideanFrameClass

Equations

• LO.Modal.Hilbert.KB5.Kripke.complete = ⋯

instance LO.Modal.Hilbert.KDB.Kripke.sound : LO.Sound (LO.Modal.Hilbert.KDB ℕ) LO.Modal.Kripke.SerialSymmetricFrameClass

Equations

• LO.Modal.Hilbert.KDB.Kripke.sound = ⋯

instance LO.Modal.Hilbert.KDB.consistent : LO.System.Consistent (LO.Modal.Hilbert.KDB ℕ)

Equations

• LO.Modal.Hilbert.KDB.consistent = ⋯

instance LO.Modal.Hilbert.KDB.Kripke.complete : LO.Complete (LO.Modal.Hilbert.KDB ℕ) LO.Modal.Kripke.SerialSymmetricFrameClass

Equations

• LO.Modal.Hilbert.KDB.Kripke.complete = ⋯

instance LO.Modal.Hilbert.KD4.Kripke.sound : LO.Sound (LO.Modal.Hilbert.KD4 ℕ) LO.Modal.Kripke.SerialTransitiveFrameClass

Equations

• LO.Modal.Hilbert.KD4.Kripke.sound = ⋯

instance LO.Modal.Hilbert.KD4.consistent : LO.System.Consistent (LO.Modal.Hilbert.KD4 ℕ)

Equations

• LO.Modal.Hilbert.KD4.consistent = ⋯

instance LO.Modal.Hilbert.KD4.Kripke.complete : LO.Complete (LO.Modal.Hilbert.KD4 ℕ) LO.Modal.Kripke.SerialTransitiveFrameClass

Equations

• LO.Modal.Hilbert.KD4.Kripke.complete = ⋯

instance LO.Modal.Hilbert.KD5.Kripke.sound : LO.Sound (LO.Modal.Hilbert.KD5 ℕ) LO.Modal.Kripke.SerialEuclideanFrameClass

Equations

• LO.Modal.Hilbert.KD5.Kripke.sound = ⋯

instance LO.Modal.Hilbert.KD5.consistent : LO.System.Consistent (LO.Modal.Hilbert.KD5 ℕ)

Equations

• LO.Modal.Hilbert.KD5.consistent = ⋯

instance LO.Modal.Hilbert.KD5.Kripke.complete : LO.Complete (LO.Modal.Hilbert.KD5 ℕ) LO.Modal.Kripke.SerialEuclideanFrameClass

Equations

• LO.Modal.Hilbert.KD5.Kripke.complete = ⋯