WellKnown

@[reducible, inline]

abbrev LO.Modal.Logic.K4 : Logic

Imported declaration from the Incompleteness formalization.

Equations

• LO.Modal.Logic.K4 = LO.Modal.Hilbert.K4.logic

theorem LO.Modal.Logic.K4.eq_TransitiveKripkeFrameClass_Logic : Logic.K4 = Kripke.TransitiveFrameClass.logic

@[reducible, inline]

abbrev LO.Modal.Logic.K45 : Logic

Imported declaration from the Incompleteness formalization.

Equations

• LO.Modal.Logic.K45 = LO.Modal.Hilbert.K45.logic

theorem LO.Modal.Logic.K45.eq_TransitiveEuclideanKripkeFrameClass_Logic : Logic.K45 = Kripke.TransitiveEuclideanFrameClass.logic

@[reducible, inline]

abbrev LO.Modal.Logic.K5 : Logic

Imported declaration from the Incompleteness formalization.

Equations

• LO.Modal.Logic.K5 = LO.Modal.Hilbert.K5.logic

theorem LO.Modal.Logic.K5.eq_EuclideanKripkeFrameClass_Logic : Logic.K5 = Kripke.EuclideanFrameClass.logic

@[reducible, inline]

abbrev LO.Modal.Logic.KB : Logic

Imported declaration from the Incompleteness formalization.

Equations

• LO.Modal.Logic.KB = LO.Modal.Hilbert.KB.logic

theorem LO.Modal.Logic.KB.eq_SymmetricKripkeFrameClass_Logic : Logic.KB = Kripke.SymmetricFrameClass.logic

@[reducible, inline]

abbrev LO.Modal.Logic.KB4 : Logic

Imported declaration from the Incompleteness formalization.

Equations

• LO.Modal.Logic.KB4 = LO.Modal.Hilbert.KB4.logic

theorem LO.Modal.Logic.KB4.eq_ReflexiveTransitiveKripkeFrameClass_Logic : Logic.KB4 = Kripke.SymmetricTransitiveFrameClass.logic

@[reducible, inline]

abbrev LO.Modal.Logic.KB5 : Logic

Imported declaration from the Incompleteness formalization.

Equations

• LO.Modal.Logic.KB5 = LO.Modal.Hilbert.KB5.logic

theorem LO.Modal.Logic.KB5.eq_ReflexiveEuclideanKripkeFrameClass_Logic : Logic.KB5 = Kripke.SymmetricEuclideanFrameClass.logic

@[reducible, inline]

abbrev LO.Modal.Logic.KD : Logic

Imported declaration from the Incompleteness formalization.

Equations

• LO.Modal.Logic.KD = LO.Modal.Hilbert.KD.logic

theorem LO.Modal.Logic.KD.eq_SerialKripkeFrameClass_Logic : Logic.KD = Kripke.SerialFrameClass.logic

@[reducible, inline]

abbrev LO.Modal.Logic.KD4 : Logic

Imported declaration from the Incompleteness formalization.

Equations

• LO.Modal.Logic.KD4 = LO.Modal.Hilbert.KD4.logic

theorem LO.Modal.Logic.KD4.eq_SerialTransitiveKripkeFrameClass_Logic : Logic.KD4 = Kripke.SerialTransitiveFrameClass.logic

@[reducible, inline]

abbrev LO.Modal.Logic.KD45 : Logic

Imported declaration from the Incompleteness formalization.

Equations

• LO.Modal.Logic.KD45 = LO.Modal.Hilbert.KD45.logic

theorem LO.Modal.Logic.KD45.eq_SerialTransitiveEuclideanKripkeFrameClass_Logic : Logic.KD45 = Kripke.SerialTransitiveEuclideanFrameClass.logic

@[reducible, inline]

abbrev LO.Modal.Logic.KD5 : Logic

Imported declaration from the Incompleteness formalization.

Equations

• LO.Modal.Logic.KD5 = LO.Modal.Hilbert.KD5.logic

theorem LO.Modal.Logic.KD5.eq_SerialEuclideanKripkeFrameClass_Logic : Logic.KD5 = Kripke.SerialEuclideanFrameClass.logic

@[reducible, inline]

abbrev LO.Modal.Logic.KDB : Logic

Imported declaration from the Incompleteness formalization.

Equations

• LO.Modal.Logic.KDB = LO.Modal.Hilbert.KDB.logic

theorem LO.Modal.Logic.KDB.eq_SerialSymmetricKripkeFrameClass_Logic : Logic.KDB = Kripke.SerialSymmetricFrameClass.logic

@[reducible, inline]

abbrev LO.Modal.Logic.KT : Logic

Imported declaration from the Incompleteness formalization.

Equations

• LO.Modal.Logic.KT = LO.Modal.Hilbert.KT.logic

theorem LO.Modal.Logic.KT.eq_ReflexiveKripkeFrameClass_Logic : Logic.KT = Kripke.ReflexiveFrameClass.logic

@[reducible, inline]

abbrev LO.Modal.Logic.KTB : Logic

Imported declaration from the Incompleteness formalization.

Equations

• LO.Modal.Logic.KTB = LO.Modal.Hilbert.KTB.logic

theorem LO.Modal.Logic.KTB.eq_ReflexiveSymmetricKripkeFrameClass_Logic : Logic.KTB = Kripke.ReflexiveSymmetricFrameClass.logic

@[reducible, inline]

abbrev LO.Modal.Logic.S4 : Logic

Imported declaration from the Incompleteness formalization.

Equations

• LO.Modal.Logic.S4 = LO.Modal.Hilbert.S4.logic

theorem LO.Modal.Logic.S4.eq_ReflexiveTransitiveKripkeFrameClass_Logic : Logic.S4 = Kripke.ReflexiveTransitiveFrameClass.logic

@[reducible, inline]

abbrev LO.Modal.Logic.S4Dot2 : Logic

Imported declaration from the Incompleteness formalization.

Equations

• LO.Modal.Logic.S4Dot2 = LO.Modal.Hilbert.S4Dot2.logic

theorem LO.Modal.Logic.S4Dot2.eq_ReflexiveTransitiveConfluentKripkeFrameClass_Logic : Logic.S4Dot2 = Kripke.ReflexiveTransitiveConfluentFrameClass.logic

@[reducible, inline]

abbrev LO.Modal.Logic.S4Dot3 : Logic

Imported declaration from the Incompleteness formalization.

Equations

• LO.Modal.Logic.S4Dot3 = LO.Modal.Hilbert.S4Dot3.logic

theorem LO.Modal.Logic.S4Dot3.eq_ReflexiveTransitiveConnectedKripkeFrameClass_Logic : Logic.S4Dot3 = Kripke.ReflexiveTransitiveConnectedFrameClass.logic

@[reducible, inline]

abbrev LO.Modal.Logic.S5 : Logic

Imported declaration from the Incompleteness formalization.

Equations

• LO.Modal.Logic.S5 = LO.Modal.Hilbert.S5.logic

theorem LO.Modal.Logic.S5.eq_ReflexiveEuclideanKripkeFrameClass_Logic : Logic.S5 = Kripke.ReflexiveEuclideanFrameClass.logic

theorem LO.Modal.Logic.S5.eq_UniversalKripkeFrameClass_Logic : Logic.S5 = Kripke.UniversalFrameClass.logic

@[reducible, inline]

abbrev LO.Modal.Logic.S5Grz : Logic

Imported declaration from the Incompleteness formalization.

Equations

• LO.Modal.Logic.S5Grz = LO.Modal.Hilbert.S5Grz.logic

@[reducible, inline]

abbrev LO.Modal.Logic.GL : Logic

Imported declaration from the Incompleteness formalization.

Equations

• LO.Modal.Logic.GL = LO.Modal.Hilbert.GL.logic

theorem LO.Modal.Logic.GL.eq_TransitiveIrreflexiveFiniteKripkeFrameClass_Logic : Logic.GL = Kripke.TransitiveIrreflexiveFiniteFrameClass.logic

instance LO.Modal.Logic.instUnnecessitationGL : Logic.GL.Unnecessitation

@[reducible, inline]

abbrev LO.Modal.Logic.KH : Logic

Imported declaration from the Incompleteness formalization.

Equations

• LO.Modal.Logic.KH = LO.Modal.Hilbert.KH.logic

@[reducible, inline]

abbrev LO.Modal.Logic.Grz : Logic

Imported declaration from the Incompleteness formalization.

Equations

• LO.Modal.Logic.Grz = LO.Modal.Hilbert.Grz.logic

theorem LO.Modal.Logic.Grz.eq_ReflexiveTransitiveAntiSymmetricFiniteKripkeFrameClass_Logic : Logic.Grz = Kripke.ReflexiveTransitiveAntiSymmetricFiniteFrameClass.logic

@[reducible, inline]

abbrev LO.Modal.Logic.Triv : Logic

Imported declaration from the Incompleteness formalization.

Equations

• LO.Modal.Logic.Triv = LO.Modal.Hilbert.Triv.logic

theorem LO.Modal.Logic.Triv.eq_EqualityKripkeFrameClass_Logic : Logic.Triv = Kripke.EqualityFrameClass.logic

@[reducible, inline]

abbrev LO.Modal.Logic.Ver : Logic

Imported declaration from the Incompleteness formalization.

Equations

• LO.Modal.Logic.Ver = LO.Modal.Hilbert.Ver.logic

instance LO.Modal.Logic.instNormalVer : Logic.Ver.Normal

theorem LO.Modal.Logic.Ver.eq_IsolatedFrameClass_Logic : Logic.Ver = Kripke.IsolatedFrameClass.logic