@[reducible, inline]

abbrev LO.Modal.Logic.Empty : Logic

Equations

• LO.Modal.Logic.Empty = ∅

@[reducible, inline]

abbrev LO.Modal.Logic.Univ : Logic

Equations

• LO.Modal.Logic.Univ = Set.univ

@[reducible, inline]

abbrev LO.Modal.Logic.K4 : Logic

Equations

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

theorem LO.Modal.Logic.K4.eq_TransitiveKripkeFrameClass_Logic : Logic.K4 = Kripke.FrameClass.trans.logic

@[reducible, inline]

abbrev LO.Modal.Logic.K4Point2 : Logic

Equations

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

theorem LO.Modal.Logic.K4Point2.eq_TransitiveWeakConfluentKripkeFrameClass_Logic : Logic.K4Point2 = Kripke.FrameClass.trans_weakConfluent.logic

@[reducible, inline]

abbrev LO.Modal.Logic.K4Point3 : Logic

Equations

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

theorem LO.Modal.Logic.K4Point3.eq_TransitiveWeakConnectedKripkeFrameClass_Logic : Logic.K4Point3 = Kripke.FrameClass.trans_weakConnected.logic

@[reducible, inline]

abbrev LO.Modal.Logic.K45 : Logic

Equations

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

theorem LO.Modal.Logic.K45.eq_TransitiveEuclideanKripkeFrameClass_Logic : Logic.K45 = Kripke.FrameClass.trans_eucl.logic

@[reducible, inline]

abbrev LO.Modal.Logic.K5 : Logic

Equations

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

theorem LO.Modal.Logic.K5.eq_EuclideanKripkeFrameClass_Logic : Logic.K5 = Kripke.FrameClass.eucl.logic

@[reducible, inline]

abbrev LO.Modal.Logic.KB : Logic

Equations

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

theorem LO.Modal.Logic.KB.eq_SymmetricKripkeFrameClass_Logic : Logic.KB = Kripke.FrameClass.symm.logic

@[reducible, inline]

abbrev LO.Modal.Logic.KB4 : Logic

Equations

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

theorem LO.Modal.Logic.KB4.eq_ReflexiveTransitiveKripkeFrameClass_Logic : Logic.KB4 = Kripke.FrameClass.symm_trans.logic

@[reducible, inline]

abbrev LO.Modal.Logic.KB5 : Logic

Equations

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

theorem LO.Modal.Logic.KB5.eq_ReflexiveEuclideanKripkeFrameClass_Logic : Logic.KB5 = Kripke.FrameClass.symm_eucl.logic

@[reducible, inline]

abbrev LO.Modal.Logic.KD : Logic

Equations

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

theorem LO.Modal.Logic.KD.eq_SerialKripkeFrameClass_Logic : Logic.KD = Kripke.FrameClass.serial.logic

@[reducible, inline]

abbrev LO.Modal.Logic.KD4 : Logic

Equations

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

theorem LO.Modal.Logic.KD4.eq_SerialTransitiveKripkeFrameClass_Logic : Logic.KD4 = Kripke.FrameClass.serial_trans.logic

@[reducible, inline]

abbrev LO.Modal.Logic.KD45 : Logic

Equations

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

theorem LO.Modal.Logic.KD45.eq_SerialTransitiveEuclideanKripkeFrameClass_Logic : Logic.KD45 = Kripke.FrameClass.serial_trans_eucl.logic

@[reducible, inline]

abbrev LO.Modal.Logic.KD5 : Logic

Equations

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

theorem LO.Modal.Logic.KD5.eq_SerialEuclideanKripkeFrameClass_Logic : Logic.KD5 = Kripke.FrameClass.serial_eucl.logic

@[reducible, inline]

abbrev LO.Modal.Logic.KDB : Logic

Equations

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

theorem LO.Modal.Logic.KDB.eq_SerialSymmetricKripkeFrameClass_Logic : Logic.KDB = Kripke.FrameClass.serial_symm.logic

@[reducible, inline]

abbrev LO.Modal.Logic.KT : Logic

Equations

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

theorem LO.Modal.Logic.KT.eq_ReflexiveKripkeFrameClass_Logic : Logic.KT = Kripke.FrameClass.refl.logic

@[reducible, inline]

abbrev LO.Modal.Logic.KTB : Logic

Equations

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

theorem LO.Modal.Logic.KTB.eq_ReflexiveSymmetricKripkeFrameClass_Logic : Logic.KTB = Kripke.FrameClass.refl_symm.logic

@[reducible, inline]

abbrev LO.Modal.Logic.S4 : Logic

Equations

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

theorem LO.Modal.Logic.S4.eq_ReflexiveTransitiveKripkeFrameClass_Logic : Logic.S4 = Kripke.FrameClass.preorder.logic

@[reducible, inline]

abbrev LO.Modal.Logic.S4Point2 : Logic

Equations

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

theorem LO.Modal.Logic.S4Point2.eq_ReflexiveTransitiveConfluentKripkeFrameClass_Logic : Logic.S4Point2 = Kripke.FrameClass.confluent_preorder.logic

theorem LO.Modal.Logic.S4Point2.Kripke.eq_finite_confluent_preorder_Logic : Logic.S4Point2 = Kripke.FrameClass.finite_confluent_preorder.logic

@[reducible, inline]

abbrev LO.Modal.Logic.S4Point3 : Logic

Equations

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

theorem LO.Modal.Logic.S4Point3.eq_ReflexiveTransitiveConnectedKripkeFrameClass_Logic : Logic.S4Point3 = Kripke.FrameClass.connected_preorder.logic

theorem LO.Modal.Logic.S4Point3.Kripke.eq_finite_connected_preorder_Logic : Logic.S4Point3 = Kripke.FrameClass.finite_connected_preorder.logic

@[reducible, inline]

abbrev LO.Modal.Logic.S5 : Logic

Equations

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

theorem LO.Modal.Logic.S5.eq_ReflexiveEuclideanKripkeFrameClass_Logic : Logic.S5 = Kripke.FrameClass.refl_eucl.logic

theorem LO.Modal.Logic.S5.eq_UniversalKripkeFrameClass_Logic : Logic.S5 = Kripke.FrameClass.universal.logic

@[reducible, inline]

abbrev LO.Modal.Logic.S5Grz : Logic

Equations

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

@[reducible, inline]

abbrev LO.Modal.Logic.GL : Logic

Equations

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

theorem LO.Modal.Logic.GL.eq_TransitiveIrreflexiveFiniteKripkeFrameClass_Logic : Logic.GL = Kripke.FrameClass.finite_trans_irrefl.logic

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

@[reducible, inline]

abbrev LO.Modal.Logic.GLPoint3 : Logic

Equations

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

theorem LO.Modal.Logic.GLPoint3.Kripke.eq_finiteStrictLinearOrder_logic : Logic.GLPoint3 = Kripke.FrameClass.finite_strict_linear_order.logic

@[reducible, inline]

abbrev LO.Modal.Logic.KH : Logic

Equations

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

@[reducible, inline]

abbrev LO.Modal.Logic.Grz : Logic

Equations

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

theorem LO.Modal.Logic.Grz.eq_ReflexiveTransitiveAntiSymmetricFiniteKripkeFrameClass_Logic : Logic.Grz = Kripke.FrameClass.finite_partial_order.logic

@[reducible, inline]

abbrev LO.Modal.Logic.GrzPoint2 : Logic

Equations

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

theorem LO.Modal.Logic.GrzPoint2.eq_ReflexiveTransitiveAntiSymmetricConfluentFiniteKripkeFrameClass_Logic : Logic.GrzPoint2 = Kripke.FrameClass.finite_confluent_partial_order.logic

@[reducible, inline]

abbrev LO.Modal.Logic.GrzPoint3 : Logic

Equations

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

theorem LO.Modal.Logic.GrzPoint3.eq_ReflexiveTransitiveAntiSymmetricConnectedFiniteKripkeFrameClass_Logic : Logic.GrzPoint3 = Kripke.FrameClass.finite_connected_partial_order.logic

@[reducible, inline]

abbrev LO.Modal.Logic.Triv : Logic

Equations

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

theorem LO.Modal.Logic.Triv.eq_EqualityKripkeFrameClass_Logic : Logic.Triv = Kripke.FrameClass.equality.logic

theorem LO.Modal.Logic.Triv.Kripke.eq_finite_equality_logic : Logic.Triv = Kripke.FrameClass.finite_equality.logic

@[reducible, inline]

abbrev LO.Modal.Logic.Ver : Logic

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.FrameClass.isolated.logic

theorem LO.Modal.Logic.Ver.Kripke.eq_finite_isolated_logic : Logic.Ver = Kripke.FrameClass.finite_isolated.logic

@[reducible, inline]

abbrev LO.Modal.Logic.KTc : Logic

Equations

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

theorem LO.Modal.Logic.KTc.eq_CoreflexiveKripkeFrameClass_Logic : Logic.KTc = Kripke.FrameClass.corefl.logic