def LO.Modal.Kripke.Frame.TreeUnravelling (F : LO.Modal.Kripke.Frame) (r : F.World) : LO.Modal.Kripke.Frame

Equations

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

@[simp]

theorem LO.Modal.Kripke.Frame.TreeUnravelling.not_nil {F : LO.Modal.Kripke.Frame} {r : F.World} {c : (F.TreeUnravelling r).World} : ↑c ≠ []

theorem LO.Modal.Kripke.Frame.TreeUnravelling.rel_length {F : LO.Modal.Kripke.Frame} {r : F.World} {x y : (F.TreeUnravelling r).World} (h : x ≺ y) : (↑x).length < (↑y).length

theorem LO.Modal.Kripke.Frame.TreeUnravelling.irreflexive {F : LO.Modal.Kripke.Frame} {r : F.World} : Irreflexive (F.TreeUnravelling r).Rel

theorem LO.Modal.Kripke.Frame.TreeUnravelling.assymetric {F : LO.Modal.Kripke.Frame} {r : F.World} : Assymetric (F.TreeUnravelling r).Rel

def LO.Modal.Kripke.Frame.TreeUnravelling.PMorphism (F : LO.Modal.Kripke.Frame) (r : F.World) : F.TreeUnravelling r →ₚ F

Equations

• LO.Modal.Kripke.Frame.TreeUnravelling.PMorphism F r = { toFun := fun (c : (F.TreeUnravelling r).World) => (↑c).getLast ⋯, forth := ⋯, back := ⋯ }

@[reducible, inline]

abbrev LO.Modal.Kripke.Frame.TransitiveTreeUnravelling (F : LO.Modal.Kripke.Frame) (r : F.World) : LO.Modal.Kripke.Frame

Equations

• F.TransitiveTreeUnravelling r = F.TreeUnravelling r^+

@[simp]

theorem LO.Modal.Kripke.Frame.TransitiveTreeUnravelling.not_nil {F : LO.Modal.Kripke.Frame} {r : F.World} {c : (F.TransitiveTreeUnravelling r).World} : ↑c ≠ []

theorem LO.Modal.Kripke.Frame.TransitiveTreeUnravelling.rel_length {F : LO.Modal.Kripke.Frame} {r : F.World} {x y : (F.TransitiveTreeUnravelling r).World} (Rxy : x ≺ y) : (↑x).length < (↑y).length

theorem LO.Modal.Kripke.Frame.TransitiveTreeUnravelling.rel_transitive {F : LO.Modal.Kripke.Frame} {r : F.World} : Transitive (F.TransitiveTreeUnravelling r).Rel

theorem LO.Modal.Kripke.Frame.TransitiveTreeUnravelling.rel_asymmetric {F : LO.Modal.Kripke.Frame} {r : F.World} : Assymetric (F.TransitiveTreeUnravelling r).Rel

theorem LO.Modal.Kripke.Frame.TransitiveTreeUnravelling.rel_def {F : LO.Modal.Kripke.Frame} {r : F.World} {x y : (F.TransitiveTreeUnravelling r).World} : x ≺ y ↔ (↑x).length < (↑y).length ∧ ↑x <+: ↑y

theorem LO.Modal.Kripke.Frame.TransitiveTreeUnravelling.rooted {F : LO.Modal.Kripke.Frame} {r : F.World} : (F.TransitiveTreeUnravelling r).isRooted ⟨[r], ⋯⟩

def LO.Modal.Kripke.Frame.TransitiveTreeUnravelling.pMorphism (F : LO.Modal.Kripke.Frame) (F_trans : Transitive F.Rel) (r : F.World) : F.TransitiveTreeUnravelling r →ₚ F

Equations

• LO.Modal.Kripke.Frame.TransitiveTreeUnravelling.pMorphism F F_trans r = (LO.Modal.Kripke.Frame.TreeUnravelling.PMorphism F r).TransitiveClosure F_trans

def LO.Modal.Kripke.Model.TreeUnravelling (M : LO.Modal.Kripke.Model) (r : M.World) : LO.Modal.Kripke.Model

Equations

• M.TreeUnravelling r = { toFrame := M.TreeUnravelling r, Val := fun (c : (M.TreeUnravelling r).World) (a : ℕ) => M.Val ((↑c).getLast ⋯) a }

def LO.Modal.Kripke.Model.TreeUnravelling.pMorphism (M : LO.Modal.Kripke.Model) (r : M.World) : M.TreeUnravelling r →ₚ M

Equations

• LO.Modal.Kripke.Model.TreeUnravelling.pMorphism M r = LO.Modal.Kripke.Model.PseudoEpimorphism.mkAtomic (LO.Modal.Kripke.Frame.TreeUnravelling.PMorphism M.toFrame r) ⋯

def LO.Modal.Kripke.Model.TransitiveTreeUnravelling (M : LO.Modal.Kripke.Model) (r : M.World) : LO.Modal.Kripke.Model

Equations

• M.TransitiveTreeUnravelling r = { toFrame := M.TransitiveTreeUnravelling r, Val := fun (c : (M.TransitiveTreeUnravelling r).World) (a : ℕ) => M.Val ((↑c).getLast ⋯) a }

def LO.Modal.Kripke.Model.TransitiveTreeUnravelling.pMorphism (M : LO.Modal.Kripke.Model) (M_trans : Transitive M.Rel) (r : M.World) : M.TransitiveTreeUnravelling r →ₚ M

Equations

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

theorem LO.Modal.Kripke.Model.TransitiveTreeUnravelling.modal_equivalence_at_root (M : LO.Modal.Kripke.Model) (M_trans : Transitive M.Rel) (r : M.World) : ⟨[r], ⋯⟩ ↭ r

structure LO.Modal.Kripke.FiniteTransitiveTreeextends LO.Modal.Kripke.FiniteFrame, LO.Modal.Kripke.RootedFrame : Type 1

• World : Type
• Rel : Rel self.World self.World
• world_nonempty : Nonempty self.World
• world_finite : Finite self.World
• root : self.World
• root_rooted : self.isRooted self.root
• default : self.World
• rel_assymetric : Assymetric self.Rel
• rel_transitive : Transitive self.Rel

theorem LO.Modal.Kripke.FiniteTransitiveTree.rel_irreflexive (T : LO.Modal.Kripke.FiniteTransitiveTree) : Irreflexive T.Rel

@[reducible, inline]

abbrev LO.Modal.Kripke.Model.FiniteTransitiveTreeUnravelling (M : LO.Modal.Kripke.Model) (r : M.World) : LO.Modal.Kripke.Model

Equations

• M.FiniteTransitiveTreeUnravelling r = (M↾r).TransitiveTreeUnravelling ⟨r, ⋯⟩

structure LO.Modal.Kripke.FiniteTransitiveTreeModelextends LO.Modal.Kripke.FiniteTransitiveTree, LO.Modal.Kripke.Model : Type 1

• World : Type
• Rel : Rel self.World self.World
• world_nonempty : Nonempty self.World
• world_finite : Finite self.World
• root : self.World
• root_rooted : self.isRooted self.root
• default : self.World
• rel_assymetric : Assymetric self.Rel
• rel_transitive : Transitive self.Rel
• Val : LO.Modal.Kripke.Valuation self.toFrame

@[reducible, inline]

abbrev LO.Modal.Kripke.FiniteFrame.FiniteTransitiveTreeUnravelling (F : LO.Modal.Kripke.FiniteFrame) [DecidableEq F.World] (F_trans : Transitive F.Rel) (F_irrefl : Irreflexive F.Rel) (r : F.World) : LO.Modal.Kripke.FiniteTransitiveTree

Equations

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