theorem List.Chain'.nodup_of_trans_irreflex {α : Type u_1} {l : List α} {R : α → α → Prop} (R_trans : Transitive R) (R_irrefl : Irreflexive R) (h_chain : List.Chain' R l) : l.Nodup

instance List.finiteNodupList {α : Type u_1} [DecidableEq α] [Finite α] : Finite { l : List α // l.Nodup }

Equations

• ⋯ = ⋯

theorem List.chains_finite {α : Type u_1} {R : α → α → Prop} [DecidableEq α] [Finite α] (R_trans : Transitive R) (R_irrefl : Irreflexive R) : Finite { l : List α // List.Chain' R l }

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

Equations

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

@[simp]

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

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

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

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

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

Equations

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

@[reducible, inline]

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

Equations

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

@[simp]

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

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

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

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

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

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

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

Equations

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

def LO.Kripke.Model.TreeUnravelling {α : Type u_1} (M : LO.Kripke.Model α) (r : M.World) : LO.Kripke.Model α

Equations

• M.TreeUnravelling r = { Frame := M.Frame.TreeUnravelling r, Valuation := fun (c : (M.Frame.TreeUnravelling r).World) (a : α) => M.Valuation ((↑c).getLast ⋯) a }

def LO.Kripke.Model.TreeUnravelling.pMorphism {α : Type u_1} (M : LO.Kripke.Model α) (r : M.World) : M.TreeUnravelling r →ₚ M

Equations

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

def LO.Kripke.Model.TransitiveTreeUnravelling {α : Type u_1} (M : LO.Kripke.Model α) (r : M.World) : LO.Kripke.Model α

Equations

• M.TransitiveTreeUnravelling r = { Frame := M.Frame.TransitiveTreeUnravelling r, Valuation := fun (c : (M.Frame.TransitiveTreeUnravelling r).World) (a : α) => M.Valuation ((↑c).getLast ⋯) a }

def LO.Kripke.Model.TransitiveTreeUnravelling.pMorphism {α : Type u_1} (M : LO.Kripke.Model α) (M_trans : Transitive M.Frame.Rel) (r : M.World) : M.TransitiveTreeUnravelling r →ₚ M

Equations

• LO.Kripke.Model.TransitiveTreeUnravelling.pMorphism M M_trans r = LO.Kripke.Model.PseudoEpimorphism.mkAtomic (LO.Kripke.Frame.TransitiveTreeUnravelling.pMorphism M.Frame M_trans r) ⋯

structure LO.Kripke.FiniteTransitiveTreeextends LO.Kripke.FiniteFrame : Type (u_1 + 1)

• World : Type u_1
• 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.Kripke.FiniteTransitiveTree.rel_assymetric (self : LO.Kripke.FiniteTransitiveTree) : Assymetric self.Rel

theorem LO.Kripke.FiniteTransitiveTree.rel_transitive (self : LO.Kripke.FiniteTransitiveTree) : Transitive self.Rel

@[reducible, inline]

abbrev LO.Kripke.FiniteTransitiveTree.Dep (α : Type u_1) : Type (u_2 + 1)

Equations

• LO.Kripke.FiniteTransitiveTree.Dep α = LO.Kripke.FiniteTransitiveTree

@[reducible, inline]

abbrev LO.Kripke.FiniteTransitiveTree.alt (T : LO.Kripke.FiniteTransitiveTree) {α : Type u_2} : LO.Kripke.FiniteTransitiveTree.Dep α

Equations

• T# = T

def LO.Kripke.«term_#» : Lean.TrailingParserDescr

Equations

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

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

@[reducible, inline]

abbrev LO.Kripke.Model.FiniteTransitiveTreeUnravelling {α : Type u_1} (M : LO.Kripke.Model α) (r : M.World) : LO.Kripke.Model α

Equations

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

structure LO.Kripke.FiniteTransitiveTreeModel (α : Type u_1) : Type (max u_1 (u_2 + 1))

• Tree : LO.Kripke.FiniteTransitiveTree
• Valuation : LO.Kripke.Valuation self.Tree.toFrame α

@[reducible, inline]

abbrev LO.Kripke.FiniteTransitiveTreeModel.World {α : Type u_1} (M : LO.Kripke.FiniteTransitiveTreeModel α) : Type u_2

Equations

• M.World = M.Tree.World

@[reducible, inline]

abbrev LO.Kripke.FiniteTransitiveTreeModel.root {α : Type u_1} (M : LO.Kripke.FiniteTransitiveTreeModel α) : M.World

Equations

• M.root = M.Tree.root

@[reducible, inline]

abbrev LO.Kripke.FiniteTransitiveTreeModel.toFrame {α : Type u_1} (M : LO.Kripke.FiniteTransitiveTreeModel α) : LO.Kripke.Frame

Equations

• M.toFrame = M.Tree.toFrame

@[reducible, inline]

abbrev LO.Kripke.FiniteTransitiveTreeModel.toModel {α : Type u_1} (M : LO.Kripke.FiniteTransitiveTreeModel α) : LO.Kripke.Model α

Equations

• M.toModel = { Frame := M.toFrame, Valuation := M.Valuation }

instance LO.Kripke.FiniteTransitiveTreeModel.instCoeModel {α : Type u_1} : Coe (LO.Kripke.FiniteTransitiveTreeModel α) (LO.Kripke.Model α)

Equations

• LO.Kripke.FiniteTransitiveTreeModel.instCoeModel = { coe := LO.Kripke.FiniteTransitiveTreeModel.toModel }

instance LO.Kripke.FiniteTransitiveTreeModel.instCoeSortType {α : Type u_1} : CoeSort (LO.Kripke.FiniteTransitiveTreeModel α) (Type u)

Equations

• LO.Kripke.FiniteTransitiveTreeModel.instCoeSortType = { coe := LO.Kripke.FiniteTransitiveTreeModel.World }

@[reducible, inline]

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

Equations

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