@[reducible, inline]
abbrev
LO.Modal.Kripke.GL_MDPCounterexampleFrame
(F₁ : LO.Kripke.FiniteTransitiveTree)
(F₂ : LO.Kripke.FiniteTransitiveTree)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
instance
LO.Modal.Kripke.GL_MDPCounterexampleFrame.instCoeWorld
{F₁ : LO.Kripke.FiniteTransitiveTree}
{F₂ : LO.Kripke.FiniteTransitiveTree}
:
Coe F₁.World (LO.Modal.Kripke.GL_MDPCounterexampleFrame F₁ F₂).World
instance
LO.Modal.Kripke.GL_MDPCounterexampleFrame.instCoeWorld_1
{F₁ : LO.Kripke.FiniteTransitiveTree}
{F₂ : LO.Kripke.FiniteTransitiveTree}
:
Coe F₂.World (LO.Modal.Kripke.GL_MDPCounterexampleFrame F₁ F₂).World
def
LO.Modal.Kripke.GL_MDPCounterexampleFrame.p_morphism₁
{F₁ : LO.Kripke.FiniteTransitiveTree}
{F₂ : LO.Kripke.FiniteTransitiveTree}
:
F₁.toFrame →ₚ (LO.Modal.Kripke.GL_MDPCounterexampleFrame F₁ F₂).toFrame
Equations
Instances For
def
LO.Modal.Kripke.GL_MDPCounterexampleFrame.p_morphism₂
{F₁ : LO.Kripke.FiniteTransitiveTree}
{F₂ : LO.Kripke.FiniteTransitiveTree}
:
F₂.toFrame →ₚ (LO.Modal.Kripke.GL_MDPCounterexampleFrame F₁ F₂).toFrame
Equations
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)
:
@[reducible, inline]
abbrev
LO.Modal.Kripke.GL_MDPCounterexampleModel
{α : Type u_1}
(M₁ : LO.Kripke.FiniteTransitiveTreeModel α)
(M₂ : LO.Kripke.FiniteTransitiveTreeModel α)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
instance
LO.Modal.Kripke.GL_MDPCounterexampleModel.instCoeWorld
{α : Type u_1}
{M₁ : LO.Kripke.FiniteTransitiveTreeModel α}
{M₂ : LO.Kripke.FiniteTransitiveTreeModel α}
:
Coe M₁.World (LO.Modal.Kripke.GL_MDPCounterexampleModel M₁ M₂).World
instance
LO.Modal.Kripke.GL_MDPCounterexampleModel.instCoeWorld_1
{α : Type u_1}
{M₁ : LO.Kripke.FiniteTransitiveTreeModel α}
{M₂ : LO.Kripke.FiniteTransitiveTreeModel α}
:
Coe M₂.World (LO.Modal.Kripke.GL_MDPCounterexampleModel M₁ M₂).World
def
LO.Modal.Kripke.GL_MDPCounterexampleModel.p_morphism₁
{α : Type u_1}
{M₁ : LO.Kripke.FiniteTransitiveTreeModel α}
{M₂ : LO.Kripke.FiniteTransitiveTreeModel α}
:
M₁.toModel →ₚ (LO.Modal.Kripke.GL_MDPCounterexampleModel M₁ M₂).toModel
Equations
- LO.Modal.Kripke.GL_MDPCounterexampleModel.p_morphism₁ = LO.Kripke.Model.PseudoEpimorphism.mkAtomic LO.Modal.Kripke.GL_MDPCounterexampleFrame.p_morphism₁ ⋯
Instances For
theorem
LO.Modal.Kripke.GL_MDPCounterexampleModel.modal_equivalence_original_world₁
{α : Type u_1}
{M₁ : LO.Kripke.FiniteTransitiveTreeModel α}
{M₂ : LO.Kripke.FiniteTransitiveTreeModel α}
{x : M₁.toModel.World}
:
def
LO.Modal.Kripke.GL_MDPCounterexampleModel.p_morphism₂
{α : Type u_1}
{M₁ : LO.Kripke.FiniteTransitiveTreeModel α}
{M₂ : LO.Kripke.FiniteTransitiveTreeModel α}
:
M₂.toModel →ₚ (LO.Modal.Kripke.GL_MDPCounterexampleModel M₁ M₂).toModel
Equations
- LO.Modal.Kripke.GL_MDPCounterexampleModel.p_morphism₂ = LO.Kripke.Model.PseudoEpimorphism.mkAtomic LO.Modal.Kripke.GL_MDPCounterexampleFrame.p_morphism₂ ⋯
Instances For
theorem
LO.Modal.Kripke.GL_MDPCounterexampleModel.modal_equivalence_original_world₂
{α : Type u_1}
{M₁ : LO.Kripke.FiniteTransitiveTreeModel α}
{M₂ : LO.Kripke.FiniteTransitiveTreeModel α}
{x : M₂.toModel.World}
:
theorem
LO.Modal.GL_MDP
{α : Type u_1}
[Inhabited α]
[DecidableEq α]
{p₁ : LO.Modal.Formula α}
{p₂ : LO.Modal.Formula α}
(h : 𝐆𝐋 ⊢! □p₁ ⋎ □p₂)
:
instance
LO.Modal.instModalDisjunctiveFormulaHilbertGL
{α : Type u_1}
[Inhabited α]
[DecidableEq α]
:
Equations
- ⋯ = ⋯