class LO.InterpretabilityLogic.Veltman.Frame.IsILMinus_J4Plus_J5 (F : Frame) extends F.HasAxiomJ4, F.HasAxiomJ5 : Prop

• S_J4 {w x y : F.World} : x ≺[w] y → w ≺ y
• S_J5 {w x y : F.World} : w ≺ x → x ≺ y → x ≺[w] y

@[reducible, inline]

abbrev LO.InterpretabilityLogic.Veltman.FrameClass.ILMinus_J4Plus_J5 : FrameClass

Equations

• LO.InterpretabilityLogic.Veltman.FrameClass.ILMinus_J4Plus_J5 = {F : LO.InterpretabilityLogic.Veltman.Frame | F.IsILMinus_J4Plus_J5}

instance LO.InterpretabilityLogic.Veltman.instIsILMinus_J4Plus_J5TrivialFrame : trivialFrame.IsILMinus_J4Plus_J5

instance LO.InterpretabilityLogic.ILMinus_J4Plus_J5.Veltman.sound : Sound ILMinus_J4Plus_J5 Veltman.FrameClass.ILMinus_J4Plus_J5

instance LO.InterpretabilityLogic.ILMinus_J4Plus_J5.instConsistentFormulaNatLogic : Entailment.Consistent ILMinus_J4Plus_J5

instance LO.InterpretabilityLogic.instStrictlyWeakerThanFormulaNatLogicILMinus_J4PlusILMinus_J4Plus_J5 : ILMinus_J4Plus ⪱ ILMinus_J4Plus_J5

instance LO.InterpretabilityLogic.instStrictlyWeakerThanFormulaNatLogicILMinus_J5ILMinus_J4Plus_J5 : ILMinus_J5 ⪱ ILMinus_J4Plus_J5