Documentation

Foundation.Modal.Kripke.GL.MDP

@[reducible, inline]
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    Equations
    • LO.Modal.Kripke.GL_MDPCounterexampleFrame.instCoeWorld = { coe := Sum.inr Sum.inl }
    Equations
    • LO.Modal.Kripke.GL_MDPCounterexampleFrame.instCoeWorld_1 = { coe := Sum.inr Sum.inr }
    Equations
    • LO.Modal.Kripke.GL_MDPCounterexampleFrame.p_morphism₁ = { toFun := fun (x : F₁.World) => Sum.inr (Sum.inl x), forth := , back := }
    Instances For
      Equations
      • LO.Modal.Kripke.GL_MDPCounterexampleFrame.p_morphism₂ = { toFun := fun (x : F₂.World) => Sum.inr (Sum.inr x), forth := , back := }
      Instances For
        theorem LO.Modal.Kripke.GL_MDPCounterexampleFrame.through_original_root {F₁ : LO.Kripke.FiniteTransitiveTree} {F₂ : LO.Kripke.FiniteTransitiveTree} {x : (LO.Modal.Kripke.GL_MDPCounterexampleFrame F₁ F₂).World} (h : (LO.Modal.Kripke.GL_MDPCounterexampleFrame F₁ F₂).root x) :
        (x = (Sum.inr Sum.inl) F₁.root Sum.inr (Sum.inl F₁.root) x) x = (Sum.inr Sum.inr) F₂.root Sum.inr (Sum.inr F₂.root) x
        @[reducible, inline]
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          Equations
          • LO.Modal.Kripke.GL_MDPCounterexampleModel.instCoeWorld = { coe := Sum.inr Sum.inl }
          Equations
          • LO.Modal.Kripke.GL_MDPCounterexampleModel.instCoeWorld_1 = { coe := Sum.inr Sum.inr }
          Equations
          Instances For
            Equations
            Instances For
              theorem LO.Modal.GL_MDP {α : Type u_1} [Inhabited α] [DecidableEq α] {p₁ : LO.Modal.Formula α} {p₂ : LO.Modal.Formula α} (h : 𝐆𝐋 ⊢! p₁ p₂) :