@[reducible, inline]

abbrev LO.Propositional.Kripke2.FrameClass.F_Tra1 : FrameClass

Equations

• LO.Propositional.Kripke2.FrameClass.F_Tra1 = {F : LO.Propositional.Kripke2.Frame | F.IsTransitive}

instance LO.Propositional.Kripke2.instIsTransitiveTrivialFrame : trivialFrame.IsTransitive

instance LO.Propositional.HilbertF.F_Tra1.soundKripke2 : Sound HilbertF.F_Tra1 {F : Kripke2.Frame | F.IsTransitive}

instance LO.Propositional.HilbertF.F_Tra1.instConsistentFormulaNat : Entailment.Consistent HilbertF.F_Tra1

instance LO.Propositional.instStrictlyWeakerThanFormulaNatHilbertFFF_Tra1 : HilbertF.F ⪱ HilbertF.F_Tra1