@[reducible, inline]

abbrev LO.Modal.Kripke.GL_MDPCounterexampleFrame (F₁ : LO.Kripke.FiniteTransitiveTree) (F₂ : LO.Kripke.FiniteTransitiveTree) : LO.Kripke.FiniteTransitiveTree

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• LO.Modal.Kripke.GL_MDPCounterexampleFrame.instCoeWorld = { coe := Sum.inr ∘ Sum.inl }

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

Equations

• LO.Modal.Kripke.GL_MDPCounterexampleFrame.instCoeWorld_1 = { coe := Sum.inr ∘ Sum.inr }

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

• LO.Modal.Kripke.GL_MDPCounterexampleFrame.p_morphism₁ = { toFun := fun (x : F₁.World) => Sum.inr (Sum.inl x), forth := ⋯, back := ⋯ }

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

• LO.Modal.Kripke.GL_MDPCounterexampleFrame.p_morphism₂ = { toFun := fun (x : F₂.World) => Sum.inr (Sum.inr x), forth := ⋯, back := ⋯ }

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]

abbrev LO.Modal.Kripke.GL_MDPCounterexampleModel {α : Type u_1} (M₁ : LO.Kripke.FiniteTransitiveTreeModel α) (M₂ : LO.Kripke.FiniteTransitiveTreeModel α) : LO.Kripke.FiniteTransitiveTreeModel α

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• LO.Modal.Kripke.GL_MDPCounterexampleModel.instCoeWorld = { coe := Sum.inr ∘ Sum.inl }

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

Equations

• LO.Modal.Kripke.GL_MDPCounterexampleModel.instCoeWorld_1 = { coe := Sum.inr ∘ Sum.inr }

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₁ ⋯

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} : x ↭ (Sum.inr ∘ Sum.inl) x

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₂ ⋯

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} : x ↭ (Sum.inr ∘ Sum.inr) x

theorem LO.Modal.GL_MDP_Aux {α : Type u_1} [Inhabited α] [DecidableEq α] {X : LO.Modal.Theory α} {p₁ : LO.Modal.Formula α} {p₂ : LO.Modal.Formula α} (h : (□''X) *⊢[𝐆𝐋]! □p₁ ⋎ □p₂) : (□''X) *⊢[𝐆𝐋]! □p₁ ∨ (□''X) *⊢[𝐆𝐋]! □p₂

theorem LO.Modal.GL_MDP {α : Type u_1} [Inhabited α] [DecidableEq α] {p₁ : LO.Modal.Formula α} {p₂ : LO.Modal.Formula α} (h : 𝐆𝐋 ⊢! □p₁ ⋎ □p₂) : 𝐆𝐋 ⊢! p₁ ∨ 𝐆𝐋 ⊢! p₂

instance LO.Modal.instModalDisjunctiveFormulaHilbertGL {α : Type u_1} [Inhabited α] [DecidableEq α] : LO.System.ModalDisjunctive 𝐆𝐋

Equations

• ⋯ = ⋯