Documentation

Logic.Modal.Standard.Kripke.GL.MDP

source
def LO.Modal.Standard.tacticLefta :
Lean.ParserDescr
Equations
Instances For
    source
    def LO.Modal.Standard.tacticRighta :
    Lean.ParserDescr
    Equations
    Instances For
      source
      @[reducible, inline]
      abbrev LO.Modal.Standard.Kripke.GL_MDPCounterexampleFrame (F₁ : LO.Modal.Standard.Kripke.FiniteTransitiveTree) (F₂ : LO.Modal.Standard.Kripke.FiniteTransitiveTree) :
      LO.Modal.Standard.Kripke.FiniteTransitiveTree
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        instance LO.Modal.Standard.Kripke.GL_MDPCounterexampleFrame.instCoeWorld {F₁ : LO.Modal.Standard.Kripke.FiniteTransitiveTree} {F₂ : LO.Modal.Standard.Kripke.FiniteTransitiveTree} :
        Coe F₁.World (LO.Modal.Standard.Kripke.GL_MDPCounterexampleFrame F₁ F₂).World
        Equations
        • LO.Modal.Standard.Kripke.GL_MDPCounterexampleFrame.instCoeWorld = { coe := Sum.inr ∘ Sum.inl }
        source
        instance LO.Modal.Standard.Kripke.GL_MDPCounterexampleFrame.instCoeWorld_1 {F₁ : LO.Modal.Standard.Kripke.FiniteTransitiveTree} {F₂ : LO.Modal.Standard.Kripke.FiniteTransitiveTree} :
        Coe F₂.World (LO.Modal.Standard.Kripke.GL_MDPCounterexampleFrame F₁ F₂).World
        Equations
        • LO.Modal.Standard.Kripke.GL_MDPCounterexampleFrame.instCoeWorld_1 = { coe := Sum.inr ∘ Sum.inr }
        source
        def LO.Modal.Standard.Kripke.GL_MDPCounterexampleFrame.p_morphism₁ {F₁ : LO.Modal.Standard.Kripke.FiniteTransitiveTree} {F₂ : LO.Modal.Standard.Kripke.FiniteTransitiveTree} :
        F₁.toFrame →ₚ (LO.Modal.Standard.Kripke.GL_MDPCounterexampleFrame F₁ F₂).toFrame
        Equations
        • LO.Modal.Standard.Kripke.GL_MDPCounterexampleFrame.p_morphism₁ = { toFun := fun (x : F₁.World) => Sum.inr (Sum.inl x), forth := ⋯, back := ⋯ }
        Instances For
          source
          def LO.Modal.Standard.Kripke.GL_MDPCounterexampleFrame.p_morphism₂ {F₁ : LO.Modal.Standard.Kripke.FiniteTransitiveTree} {F₂ : LO.Modal.Standard.Kripke.FiniteTransitiveTree} :
          F₂.toFrame →ₚ (LO.Modal.Standard.Kripke.GL_MDPCounterexampleFrame F₁ F₂).toFrame
          Equations
          • LO.Modal.Standard.Kripke.GL_MDPCounterexampleFrame.p_morphism₂ = { toFun := fun (x : F₂.World) => Sum.inr (Sum.inr x), forth := ⋯, back := ⋯ }
          Instances For
            source
            theorem LO.Modal.Standard.Kripke.GL_MDPCounterexampleFrame.through_original_root {F₁ : LO.Modal.Standard.Kripke.FiniteTransitiveTree} {F₂ : LO.Modal.Standard.Kripke.FiniteTransitiveTree} {x : (LO.Modal.Standard.Kripke.GL_MDPCounterexampleFrame F₁ F₂).World} (h : LO.Modal.Standard.Kripke.Frame.Rel' (LO.Modal.Standard.Kripke.GL_MDPCounterexampleFrame F₁ F₂).root x) :
            (x = (Sum.inr ∘ Sum.inl) F₁.root ∨ LO.Modal.Standard.Kripke.Frame.Rel' (Sum.inr (Sum.inl F₁.root)) x) ∨ x = (Sum.inr ∘ Sum.inr) F₂.root ∨ LO.Modal.Standard.Kripke.Frame.Rel' (Sum.inr (Sum.inr F₂.root)) x
            source
            @[reducible, inline]
            abbrev LO.Modal.Standard.Kripke.GL_MDPCounterexampleModel {α : Type u_1} (M₁ : LO.Modal.Standard.Kripke.FiniteTransitiveTreeModel α) (M₂ : LO.Modal.Standard.Kripke.FiniteTransitiveTreeModel α) :
            LO.Modal.Standard.Kripke.FiniteTransitiveTreeModel α
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              instance LO.Modal.Standard.Kripke.GL_MDPCounterexampleModel.instCoeWorld {α : Type u_1} {M₁ : LO.Modal.Standard.Kripke.FiniteTransitiveTreeModel α} {M₂ : LO.Modal.Standard.Kripke.FiniteTransitiveTreeModel α} :
              Coe M₁.World (LO.Modal.Standard.Kripke.GL_MDPCounterexampleModel M₁ M₂).World
              Equations
              • LO.Modal.Standard.Kripke.GL_MDPCounterexampleModel.instCoeWorld = { coe := Sum.inr ∘ Sum.inl }
              source
              instance LO.Modal.Standard.Kripke.GL_MDPCounterexampleModel.instCoeWorld_1 {α : Type u_1} {M₁ : LO.Modal.Standard.Kripke.FiniteTransitiveTreeModel α} {M₂ : LO.Modal.Standard.Kripke.FiniteTransitiveTreeModel α} :
              Coe M₂.World (LO.Modal.Standard.Kripke.GL_MDPCounterexampleModel M₁ M₂).World
              Equations
              • LO.Modal.Standard.Kripke.GL_MDPCounterexampleModel.instCoeWorld_1 = { coe := Sum.inr ∘ Sum.inr }
              source
              def LO.Modal.Standard.Kripke.GL_MDPCounterexampleModel.p_morphism₁ {α : Type u_1} {M₁ : LO.Modal.Standard.Kripke.FiniteTransitiveTreeModel α} {M₂ : LO.Modal.Standard.Kripke.FiniteTransitiveTreeModel α} :
              M₁.toModel →ₚ (LO.Modal.Standard.Kripke.GL_MDPCounterexampleModel M₁ M₂).toModel
              Equations
              Instances For
                source
                theorem LO.Modal.Standard.Kripke.GL_MDPCounterexampleModel.modal_equivalence_original_world₁ {α : Type u_1} {M₁ : LO.Modal.Standard.Kripke.FiniteTransitiveTreeModel α} {M₂ : LO.Modal.Standard.Kripke.FiniteTransitiveTreeModel α} {x : M₁.toModel.World} :
                x ↭ (Sum.inr ∘ Sum.inl) x
                source
                def LO.Modal.Standard.Kripke.GL_MDPCounterexampleModel.p_morphism₂ {α : Type u_1} {M₁ : LO.Modal.Standard.Kripke.FiniteTransitiveTreeModel α} {M₂ : LO.Modal.Standard.Kripke.FiniteTransitiveTreeModel α} :
                M₂.toModel →ₚ (LO.Modal.Standard.Kripke.GL_MDPCounterexampleModel M₁ M₂).toModel
                Equations
                Instances For
                  source
                  theorem LO.Modal.Standard.Kripke.GL_MDPCounterexampleModel.modal_equivalence_original_world₂ {α : Type u_1} {M₁ : LO.Modal.Standard.Kripke.FiniteTransitiveTreeModel α} {M₂ : LO.Modal.Standard.Kripke.FiniteTransitiveTreeModel α} {x : M₂.toModel.World} :
                  x ↭ (Sum.inr ∘ Sum.inr) x
                  source
                  theorem LO.Modal.Standard.GL_MDP_Aux {α : Type u_1} [Inhabited α] [DecidableEq α] {X : LO.Modal.Standard.Theory α} {p₁ : LO.Modal.Standard.Formula α} {p₂ : LO.Modal.Standard.Formula α} (h : (□''X) *⊢[𝐆𝐋]! □p₁ ⋎ □p₂) :
                  (□''X) *⊢[𝐆𝐋]! □p₁ ∨ (□''X) *⊢[𝐆𝐋]! □p₂
                  source
                  theorem LO.Modal.Standard.GL_MDP {α : Type u_1} [Inhabited α] [DecidableEq α] {p₁ : LO.Modal.Standard.Formula α} {p₂ : LO.Modal.Standard.Formula α} (h : 𝐆𝐋 ⊢! □p₁ ⋎ □p₂) :
                  𝐆𝐋 ⊢! p₁ ∨ 𝐆𝐋 ⊢! p₂
                  source
                  instance LO.Modal.Standard.instModalDisjunctiveFormulaDeductionParameterGL {α : Type u_1} [Inhabited α] [DecidableEq α] :
                  LO.System.ModalDisjunctive 𝐆𝐋
                  Equations
                  • ⋯ = ⋯