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.Modal.Standard.Kripke.Frame.TreeUnravelling (F : LO.Modal.Standard.Kripke.Frame) (r : F.World) : LO.Modal.Standard.Kripke.Frame

Equations

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

@[simp]

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

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

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

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

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

Equations

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

def LO.Modal.Standard.Kripke.Model.TreeUnravelling {α : Type u} (M : LO.Modal.Standard.Kripke.Model α) (r : M.World) : LO.Modal.Standard.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.Modal.Standard.Kripke.Model.TreeUnravelling.PMorphism {α : Type u} (M : LO.Modal.Standard.Kripke.Model α) (r : M.World) : M.TreeUnravelling r →ₚ M

Equations

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

@[reducible, inline]

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

Equations

• F.TransitiveTreeUnravelling r = (F.TreeUnravelling r).TransitiveClosure

@[simp]

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

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

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

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

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

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

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

Equations

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

def LO.Modal.Standard.Kripke.Model.TransitiveTreeUnravelling {α : Type u} (M : LO.Modal.Standard.Kripke.Model α) (r : M.World) : LO.Modal.Standard.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.Modal.Standard.Kripke.Model.TransitiveTreeUnravelling.PMorphism {α : Type u} (M : LO.Modal.Standard.Kripke.Model α) (M_trans : Transitive M.Frame.Rel) (r : M.World) : M.TransitiveTreeUnravelling r →ₚ M

Equations

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

theorem LO.Modal.Standard.Kripke.Model.TransitiveTreeUnravelling.modal_equivalence_to_root {α : Type u} (M : LO.Modal.Standard.Kripke.Model α) (M_trans : Transitive M.Frame.Rel) (r : M.World) : ⟨[r], ⋯⟩ ↭ r

structure LO.Modal.Standard.Kripke.FiniteTransitiveTreeextends LO.Modal.Standard.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.Modal.Standard.Kripke.FiniteTransitiveTree.rel_assymetric (self : LO.Modal.Standard.Kripke.FiniteTransitiveTree) : Assymetric self.Rel

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

@[reducible, inline]

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

Equations

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

@[reducible, inline]

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

Equations

• T# = T

def LO.Modal.Standard.Kripke.«term_#_2» : Lean.TrailingParserDescr

Equations

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

instance LO.Modal.Standard.Kripke.FiniteTransitiveTree.instSemanticsFormulaDep {α : Type u} : LO.Semantics (LO.Modal.Standard.Formula α) (LO.Modal.Standard.Kripke.FiniteTransitiveTree.Dep α)

Equations

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

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

@[reducible, inline]

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

Equations

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

@[reducible, inline]

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

Equations

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

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

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

@[reducible, inline]

abbrev LO.Modal.Standard.Kripke.FiniteTransitiveTreeModel.World {α : Type u} (M : LO.Modal.Standard.Kripke.FiniteTransitiveTreeModel α) : Type u_1

Equations

• M.World = M.Tree.World

@[reducible, inline]

abbrev LO.Modal.Standard.Kripke.FiniteTransitiveTreeModel.root {α : Type u} (M : LO.Modal.Standard.Kripke.FiniteTransitiveTreeModel α) : M.World

Equations

• M.root = M.Tree.root

@[reducible, inline]

abbrev LO.Modal.Standard.Kripke.FiniteTransitiveTreeModel.toFrame {α : Type u} (M : LO.Modal.Standard.Kripke.FiniteTransitiveTreeModel α) : LO.Modal.Standard.Kripke.Frame

Equations

• M.toFrame = M.Tree.toFrame

@[reducible, inline]

abbrev LO.Modal.Standard.Kripke.FiniteTransitiveTreeModel.toModel {α : Type u} (M : LO.Modal.Standard.Kripke.FiniteTransitiveTreeModel α) : LO.Modal.Standard.Kripke.Model α

Equations

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

instance LO.Modal.Standard.Kripke.FiniteTransitiveTreeModel.instCoeModel {α : Type u} : Coe (LO.Modal.Standard.Kripke.FiniteTransitiveTreeModel α) (LO.Modal.Standard.Kripke.Model α)

Equations

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

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

Equations

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

@[reducible]

instance LO.Modal.Standard.Kripke.FiniteTransitiveTreeModel.instSemanticsFormulaWorld {α : Type u} {M : LO.Modal.Standard.Kripke.FiniteTransitiveTreeModel α} : LO.Semantics (LO.Modal.Standard.Formula α) M.World

Equations

• LO.Modal.Standard.Kripke.FiniteTransitiveTreeModel.instSemanticsFormulaWorld = LO.Modal.Standard.Formula.Kripke.Satisfies.semantics

theorem LO.Modal.Standard.Kripke.valid_on_FiniteTransitiveTreeClass_of_valid_on_TransitiveIrreflexiveFrameClass {α : Type u} {p : LO.Modal.Standard.Formula α} (h : LO.Modal.Standard.Kripke.TransitiveIrreflexiveFrameClassꟳ.alt ⊧ p) (T : LO.Modal.Standard.Kripke.FiniteTransitiveTree) : T# ⊧ p

theorem LO.Modal.Standard.Kripke.satisfies_at_root_on_FiniteTransitiveTree {α : Type u} {p : LO.Modal.Standard.Formula α} (h : ∀ (F : LO.Modal.Standard.Kripke.FiniteTransitiveTree), F# ⊧ p) (M : LO.Modal.Standard.Kripke.FiniteTransitiveTreeModel α) : LO.Modal.Standard.Formula.Kripke.Satisfies M.toModel M.root p

theorem LO.Modal.Standard.Kripke.valid_on_TransitiveIrreflexiveFrameClass_of_satisfies_at_root_on_FiniteTransitiveTree {α : Type u} {p : LO.Modal.Standard.Formula α} : (∀ (M : LO.Modal.Standard.Kripke.FiniteTransitiveTreeModel α), LO.Modal.Standard.Formula.Kripke.Satisfies M.toModel M.root p) → LO.Modal.Standard.Kripke.TransitiveIrreflexiveFrameClassꟳ.alt ⊧ p

theorem LO.Modal.Standard.Kripke.iff_provable_GL_satisfies_at_root_on_FiniteTransitiveTree {α : Type u} [Inhabited α] [DecidableEq α] {p : LO.Modal.Standard.Formula α} : 𝐆𝐋 ⊢! p ↔ ∀ (M : LO.Modal.Standard.Kripke.FiniteTransitiveTreeModel α), LO.Modal.Standard.Formula.Kripke.Satisfies M.toModel M.root p

Segerberg [1971]?

theorem LO.Modal.Standard.Kripke.iff_unprovable_GL_exists_unsatisfies_at_root_on_FiniteTransitiveTree {α : Type u} [Inhabited α] [DecidableEq α] {p : LO.Modal.Standard.Formula α} : 𝐆𝐋 ⊬! p ↔ ∃ (M : LO.Modal.Standard.Kripke.FiniteTransitiveTreeModel α), ¬LO.Modal.Standard.Formula.Kripke.Satisfies M.toModel M.root p

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

Equations

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

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

Equations

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

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

Equations

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

@[simp]

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

theorem LO.Modal.Standard.Kripke.FiniteTransitiveTree.SimpleExtension.root_eq {F : LO.Modal.Standard.Kripke.FiniteTransitiveTree} {x : Fin 1} : Sum.inl x = F↧.root

theorem LO.Modal.Standard.Kripke.FiniteTransitiveTree.SimpleExtension.forth {F : LO.Modal.Standard.Kripke.FiniteTransitiveTree} {x : F.World} {y : F.World} (h : LO.Modal.Standard.Kripke.Frame.Rel' x y) : F↧.Rel (Sum.inr x) (Sum.inr y)

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

Equations

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

theorem LO.Modal.Standard.Kripke.FiniteTransitiveTree.SimpleExtension.through_original_root {F : LO.Modal.Standard.Kripke.FiniteTransitiveTree} {x : F↧.World} (h : LO.Modal.Standard.Kripke.Frame.Rel' F↧.root x) : x = Sum.inr F.root ∨ LO.Modal.Standard.Kripke.Frame.Rel' (Sum.inr F.root) x

@[reducible, inline]

abbrev LO.Modal.Standard.Kripke.FiniteTransitiveTreeModel.SimpleExtension {α : Type u} (M : LO.Modal.Standard.Kripke.FiniteTransitiveTreeModel α) : LO.Modal.Standard.Kripke.FiniteTransitiveTreeModel α

Equations

• M↧ = { Tree := M.Tree↧, Valuation := fun (x : M.Tree↧.World) (a : α) => match x with | Sum.inl val => M.Valuation M.Tree.root a | Sum.inr x => M.Valuation x a }

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

Equations

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

instance LO.Modal.Standard.Kripke.FiniteTransitiveTreeModel.SimpleExtension.instCoeWorld {α : Type u} {M : LO.Modal.Standard.Kripke.FiniteTransitiveTreeModel α} : Coe M.World M↧.World

Equations

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

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

Equations

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

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

theorem LO.Modal.Standard.GL_imply_boxdot_plain_of_imply_box_box {α : Type u_1} [DecidableEq α] [Inhabited α] {p : LO.Modal.Standard.Formula α} {q : LO.Modal.Standard.Formula α} : 𝐆𝐋 ⊢! □p ⟶ □q → 𝐆𝐋 ⊢! ⊡p ⟶ q

theorem LO.Modal.Standard.GL_unnecessitation! {α : Type u_1} [DecidableEq α] [Inhabited α] {p : LO.Modal.Standard.Formula α} : 𝐆𝐋 ⊢! □p → 𝐆𝐋 ⊢! p

noncomputable instance LO.Modal.Standard.instUnnecessitationDeductionParameterFormulaGL {α : Type u_1} [DecidableEq α] [Inhabited α] : LO.System.Unnecessitation 𝐆𝐋

Equations

• LO.Modal.Standard.instUnnecessitationDeductionParameterFormulaGL = { unnec := fun {p : LO.Modal.Standard.Formula α} (h : 𝐆𝐋 ⊢ □p) => Nonempty.some ⋯ }