Tree

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

Imported declaration from the Incompleteness formalization.

• World : Type
• Rel : _root_.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 : IsTrans self.World self.Rel

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

def LO.Modal.Formula.Kripke.ValidOnFiniteTransitiveTreeFrame (T : Kripke.FiniteTransitiveTree) (φ : Formula ℕ) : Prop

Imported declaration from the Incompleteness formalization.

Equations

• LO.Modal.Formula.Kripke.ValidOnFiniteTransitiveTreeFrame T φ = (T.toFrame ⊧ φ)

@[implicit_reducible]

instance LO.Modal.ValidOnFiniteTransitiveTreeFrame.semantics : Semantics (Formula ℕ) Kripke.FiniteFrame

Equations

• LO.Modal.ValidOnFiniteTransitiveTreeFrame.semantics = { Realize := fun (F : LO.Modal.Kripke.FiniteFrame) => LO.Modal.Formula.Kripke.ValidOnFiniteFrame F }

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

Imported declaration from the Incompleteness formalization.

• World : Type
• Rel : _root_.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 : IsTrans self.World self.Rel
• Val : Valuation self.toFrame

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

Imported declaration from the Incompleteness formalization.

Equations

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

@[simp]

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

theorem LO.Modal.Kripke.Frame.TreeUnravelling.rel_length {F : 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 : Frame} {r : F.World} : Std.Irrefl (F.TreeUnravelling r).Rel

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

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

Imported declaration from the Incompleteness formalization.

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 : Frame) (r : F.World) : Frame

Imported declaration from the Incompleteness formalization.

Equations

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

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

theorem LO.Modal.Kripke.Frame.TransitiveTreeUnravelling.rel_length {F : 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 : Frame} {r : F.World} : IsTrans (F.TransitiveTreeUnravelling r).World (F.TransitiveTreeUnravelling r).Rel

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

theorem LO.Modal.Kripke.Frame.TransitiveTreeUnravelling.rel_def {F : 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 : Frame} {r : F.World} : (F.TransitiveTreeUnravelling r).isRooted ⟨[r], ⋯⟩

@[reducible, inline]

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

Imported declaration from the Incompleteness formalization.

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 : Model) (r : M.World) : Model

Imported declaration from the Incompleteness formalization.

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 : Model) (r : M.World) : M.TreeUnravelling r →ₚ M

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

@[reducible, inline]

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

@[reducible, inline]

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

Imported declaration from the Incompleteness formalization.

Equations

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

@[reducible, inline]

abbrev LO.Modal.Kripke.FiniteFrame.FiniteTransitiveTreeUnravelling (F : FiniteFrame) (F_trans : IsTrans F.World F.Rel) (F_irrefl : Std.Irrefl F.Rel) (r : F.World) : FiniteTransitiveTree

Imported declaration from the Incompleteness formalization.

Equations

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