theorem LO.Modal.Hilbert.GL.Kripke.valid_on_FiniteTransitiveTreeClass_of_valid_on_TransitiveIrreflexiveFrameClass {φ : Formula ℕ} (h : Kripke.TransitiveIrreflexiveFiniteFrameClass ⊧ φ) (T : Kripke.FiniteTransitiveTree) : T.toFrame ⊧ φ

theorem LO.Modal.Hilbert.GL.Kripke.satisfies_at_root_on_FiniteTransitiveTree {φ : Formula ℕ} (h : ∀ (T : Kripke.FiniteTransitiveTree), T.toFrame ⊧ φ) (M : Kripke.FiniteTransitiveTreeModel) : Formula.Kripke.Satisfies M.toModel M.root φ

theorem LO.Modal.Hilbert.GL.Kripke.valid_on_TransitiveIrreflexiveFrameClass_of_satisfies_at_root_on_FiniteTransitiveTree {φ : Formula ℕ} : (∀ (M : Kripke.FiniteTransitiveTreeModel), Formula.Kripke.Satisfies M.toModel M.root φ) → Kripke.TransitiveIrreflexiveFiniteFrameClass ⊧ φ

theorem LO.Modal.Hilbert.GL.Kripke.provable_iff_satisfies_at_root_on_FiniteTransitiveTree {φ : Formula ℕ} : Hilbert.GL ℕ ⊢! φ ↔ ∀ (M : Kripke.FiniteTransitiveTreeModel), Formula.Kripke.Satisfies M.toModel M.root φ

theorem LO.Modal.Hilbert.GL.Kripke.unprovable_iff_exists_unsatisfies_at_root_on_FiniteTransitiveTree {φ : Formula ℕ} : Hilbert.GL ℕ ⊬ φ ↔ ∃ (M : Kripke.FiniteTransitiveTreeModel), ¬Formula.Kripke.Satisfies M.toModel M.root φ

def LO.Modal.Kripke.FiniteTransitiveTree.SimpleExtension (F : FiniteTransitiveTree) : FiniteTransitiveTree

Equations

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

def LO.Modal.Kripke.«term_↧» : Lean.TrailingParserDescr

Equations

• LO.Modal.Kripke.«term_↧» = Lean.ParserDescr.trailingNode `LO.Modal.Kripke.«term_↧» 1024 1024 (Lean.ParserDescr.symbol "↧")

instance LO.Modal.Kripke.FiniteTransitiveTree.SimpleExtension.instCoeWorld {T : FiniteTransitiveTree} : Coe T.World T↧.World

Equations

• LO.Modal.Kripke.FiniteTransitiveTree.SimpleExtension.instCoeWorld = { coe := Sum.inr }

@[simp]

theorem LO.Modal.Kripke.FiniteTransitiveTree.SimpleExtension.root_not_original {T : FiniteTransitiveTree} {x : T.World} : Sum.inr x ≠ T↧.root

theorem LO.Modal.Kripke.FiniteTransitiveTree.SimpleExtension.root_eq {T : FiniteTransitiveTree} : Sum.inl () = T↧.root

theorem LO.Modal.Kripke.FiniteTransitiveTree.SimpleExtension.forth {T : FiniteTransitiveTree} {x y : T.World} (h : x ≺ y) : T↧.Rel (Sum.inr x) (Sum.inr y)

def LO.Modal.Kripke.FiniteTransitiveTree.SimpleExtension.p_morphism {T : FiniteTransitiveTree} : T.toFrame →ₚ T↧.toFrame

Equations

• LO.Modal.Kripke.FiniteTransitiveTree.SimpleExtension.p_morphism = { toFun := fun (x : T.World) => Sum.inr x, forth := ⋯, back := ⋯ }

theorem LO.Modal.Kripke.FiniteTransitiveTree.SimpleExtension.through_original_root {T : FiniteTransitiveTree} {x : T↧.World} (h : T↧.root ≺ x) : x = Sum.inr T.root ∨ Sum.inr T.root ≺ x

@[reducible, inline]

abbrev LO.Modal.Kripke.FiniteTransitiveTreeModel.SimpleExtension (M : FiniteTransitiveTreeModel) : FiniteTransitiveTreeModel

Equations

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

def LO.Modal.Kripke.«term_↧_1» : Lean.TrailingParserDescr

Equations

• LO.Modal.Kripke.«term_↧_1» = Lean.ParserDescr.trailingNode `LO.Modal.Kripke.«term_↧_1» 1024 1024 (Lean.ParserDescr.symbol "↧")

instance LO.Modal.Kripke.FiniteTransitiveTreeModel.SimpleExtension.instCoeWorld {M : FiniteTransitiveTreeModel} : Coe M.World M↧.World

Equations

• LO.Modal.Kripke.FiniteTransitiveTreeModel.SimpleExtension.instCoeWorld = { coe := Sum.inr }

def LO.Modal.Kripke.FiniteTransitiveTreeModel.SimpleExtension.p_morphism {M : FiniteTransitiveTreeModel} : M.toModel →ₚ M↧.toModel

Equations

• LO.Modal.Kripke.FiniteTransitiveTreeModel.SimpleExtension.p_morphism = LO.Modal.Kripke.Model.PseudoEpimorphism.mkAtomic LO.Modal.Kripke.FiniteTransitiveTree.SimpleExtension.p_morphism ⋯

theorem LO.Modal.Kripke.FiniteTransitiveTreeModel.SimpleExtension.modal_equivalence_original_world {M : FiniteTransitiveTreeModel} {x : M.toModel.World} : x ↭ Sum.inr x