structure LO.Kripke.Model.Bisimulation {α : Type u_1} (M₁ : LO.Kripke.Model α) (M₂ : LO.Kripke.Model α) : Type (max u_2 u_3)

• toRel : Rel M₁.World M₂.World
• atomic : ∀ {x₁ : M₁.World} {x₂ : M₂.World} {a : α}, self.toRel x₁ x₂ → (M₁.Valuation x₁ a ↔ M₂.Valuation x₂ a)
• forth : ∀ {x₁ y₁ : M₁.World} {x₂ : M₂.World}, self.toRel x₁ x₂ → x₁ ≺ y₁ → ∃ (y₂ : M₂.World), self.toRel y₁ y₂ ∧ x₂ ≺ y₂
• back : ∀ {x₁ : M₁.World} {x₂ y₂ : M₂.World}, self.toRel x₁ x₂ → x₂ ≺ y₂ → ∃ (y₁ : M₁.World), self.toRel y₁ y₂ ∧ x₁ ≺ y₁

theorem LO.Kripke.Model.Bisimulation.atomic {α : Type u_1} {M₁ : LO.Kripke.Model α} {M₂ : LO.Kripke.Model α} (self : M₁ ⇄ M₂) {x₁ : M₁.World} {x₂ : M₂.World} {a : α} : self.toRel x₁ x₂ → (M₁.Valuation x₁ a ↔ M₂.Valuation x₂ a)

theorem LO.Kripke.Model.Bisimulation.forth {α : Type u_1} {M₁ : LO.Kripke.Model α} {M₂ : LO.Kripke.Model α} (self : M₁ ⇄ M₂) {x₁ : M₁.World} {y₁ : M₁.World} {x₂ : M₂.World} : self.toRel x₁ x₂ → x₁ ≺ y₁ → ∃ (y₂ : M₂.World), self.toRel y₁ y₂ ∧ x₂ ≺ y₂

theorem LO.Kripke.Model.Bisimulation.back {α : Type u_1} {M₁ : LO.Kripke.Model α} {M₂ : LO.Kripke.Model α} (self : M₁ ⇄ M₂) {x₁ : M₁.World} {x₂ : M₂.World} {y₂ : M₂.World} : self.toRel x₁ x₂ → x₂ ≺ y₂ → ∃ (y₁ : M₁.World), self.toRel y₁ y₂ ∧ x₁ ≺ y₁

def LO.Kripke.«term_⇄_» : Lean.TrailingParserDescr

Equations

• LO.Kripke.«term_⇄_» = Lean.ParserDescr.trailingNode `LO.Kripke.term_⇄_ 80 81 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⇄ ") (Lean.ParserDescr.cat `term 81))

instance LO.Kripke.instCoeFunBisimulationForallWorldForallProp : {α : Type u_1} → {M₁ : LO.Kripke.Model α} → {M₂ : LO.Kripke.Model α} → CoeFun (M₁ ⇄ M₂) fun (x : M₁ ⇄ M₂) => M₁.World → M₂.World → Prop

Equations

• LO.Kripke.instCoeFunBisimulationForallWorldForallProp = { coe := fun (bi : M₁ ⇄ M₂) => bi.toRel }

structure LO.Kripke.Frame.PseudoEpimorphism (F₁ : LO.Kripke.Frame) (F₂ : LO.Kripke.Frame) : Type (max u_1 u_2)

• toFun : F₁.World → F₂.World
• forth : ∀ {x y : F₁.World}, x ≺ y → self.toFun x ≺ self.toFun y
• back : ∀ {w : F₁.World} {v : F₂.World}, self.toFun w ≺ v → ∃ (u : F₁.World), self.toFun u = v ∧ w ≺ u

theorem LO.Kripke.Frame.PseudoEpimorphism.forth {F₁ : LO.Kripke.Frame} {F₂ : LO.Kripke.Frame} (self : F₁ →ₚ F₂) {x : F₁.World} {y : F₁.World} : x ≺ y → self.toFun x ≺ self.toFun y

theorem LO.Kripke.Frame.PseudoEpimorphism.back {F₁ : LO.Kripke.Frame} {F₂ : LO.Kripke.Frame} (self : F₁ →ₚ F₂) {w : F₁.World} {v : F₂.World} : self.toFun w ≺ v → ∃ (u : F₁.World), self.toFun u = v ∧ w ≺ u

def LO.Kripke.«term_→ₚ_» : Lean.TrailingParserDescr

Equations

• LO.Kripke.«term_→ₚ_» = Lean.ParserDescr.trailingNode `LO.Kripke.term_→ₚ_ 80 81 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " →ₚ ") (Lean.ParserDescr.cat `term 81))

instance LO.Kripke.instCoeFunPseudoEpimorphismForallWorld {F₁ : LO.Kripke.Frame} {F₂ : LO.Kripke.Frame} : CoeFun (F₁ →ₚ F₂) fun (x : F₁ →ₚ F₂) => F₁.World → F₂.World

Equations

• LO.Kripke.instCoeFunPseudoEpimorphismForallWorld = { coe := fun (f : F₁ →ₚ F₂) => f.toFun }

def LO.Kripke.Frame.PseudoEpimorphism.id {F : LO.Kripke.Frame} : F →ₚ F

Equations

• LO.Kripke.Frame.PseudoEpimorphism.id = { toFun := id, forth := ⋯, back := ⋯ }

def LO.Kripke.Frame.PseudoEpimorphism.TransitiveClosure {F₁ : LO.Kripke.Frame} {F₂ : LO.Kripke.Frame} (f : F₁ →ₚ F₂) (F₂_trans : Transitive F₂.Rel) : F₁^+ →ₚ F₂

Equations

• f.TransitiveClosure F₂_trans = { toFun := f.toFun, forth := ⋯, back := ⋯ }

def LO.Kripke.Frame.PseudoEpimorphism.comp {F₁ : LO.Kripke.Frame} {F₂ : LO.Kripke.Frame} {F₃ : LO.Kripke.Frame} (f : F₁ →ₚ F₂) (g : F₂ →ₚ F₃) : F₁ →ₚ F₃

Equations

• f.comp g = { toFun := g.toFun ∘ f.toFun, forth := ⋯, back := ⋯ }

structure LO.Kripke.Model.PseudoEpimorphism {α : Type u_1} (M₁ : LO.Kripke.Model α) (M₂ : LO.Kripke.Model α) extends LO.Kripke.Frame.PseudoEpimorphism : Type (max u_2 u_3)

• toFun : M₁.Frame.World → M₂.Frame.World
• forth : ∀ {x y : M₁.Frame.World}, x ≺ y → self.toFun x ≺ self.toFun y
• back : ∀ {w : M₁.Frame.World} {v : M₂.Frame.World}, self.toFun w ≺ v → ∃ (u : M₁.Frame.World), self.toFun u = v ∧ w ≺ u
• atomic : ∀ {w : M₁.World} {a : α}, M₁.Valuation w a ↔ M₂.Valuation (self.toFun w) a

theorem LO.Kripke.Model.PseudoEpimorphism.atomic {α : Type u_1} {M₁ : LO.Kripke.Model α} {M₂ : LO.Kripke.Model α} (self : M₁ →ₚ M₂) {w : M₁.World} {a : α} : M₁.Valuation w a ↔ M₂.Valuation (self.toFun w) a

def LO.Kripke.«term_→ₚ__1» : Lean.TrailingParserDescr

Equations

• LO.Kripke.«term_→ₚ__1» = Lean.ParserDescr.trailingNode `LO.Kripke.term_→ₚ__1 80 81 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " →ₚ ") (Lean.ParserDescr.cat `term 81))

instance LO.Kripke.instCoeFunPseudoEpimorphismForallWorld_1 : {α : Type u_1} → {M₁ : LO.Kripke.Model α} → {M₂ : LO.Kripke.Model α} → CoeFun (M₁ →ₚ M₂) fun (x : M₁ →ₚ M₂) => M₁.World → M₂.World

Equations

• LO.Kripke.instCoeFunPseudoEpimorphismForallWorld_1 = { coe := fun (f : M₁ →ₚ M₂) => f.toFun }

def LO.Kripke.Model.PseudoEpimorphism.toFramePseudoEpimorphism {α : Type u_1} {M₁ : LO.Kripke.Model α} {M₂ : LO.Kripke.Model α} (f : M₁ →ₚ M₂) : M₁.Frame →ₚ M₂.Frame

Equations

• f.toFramePseudoEpimorphism = { toFun := f.toFun, forth := ⋯, back := ⋯ }

def LO.Kripke.Model.PseudoEpimorphism.id {α : Type u_1} {M : LO.Kripke.Model α} : M →ₚ M

Equations

• LO.Kripke.Model.PseudoEpimorphism.id = { toFun := id, forth := ⋯, back := ⋯, atomic := ⋯ }

def LO.Kripke.Model.PseudoEpimorphism.mkAtomic {α : Type u_1} {M₁ : LO.Kripke.Model α} {M₂ : LO.Kripke.Model α} (f : M₁.Frame →ₚ M₂.Frame) (atomic : ∀ {w : M₁.Frame.World} {a : α}, M₁.Valuation w a ↔ M₂.Valuation (f.toFun w) a) : M₁ →ₚ M₂

Equations

• LO.Kripke.Model.PseudoEpimorphism.mkAtomic f atomic = { toFun := f.toFun, forth := ⋯, back := ⋯, atomic := ⋯ }

def LO.Kripke.Model.PseudoEpimorphism.comp {α : Type u_1} {M₁ : LO.Kripke.Model α} {M₂ : LO.Kripke.Model α} {M₃ : LO.Kripke.Model α} (f : M₁ →ₚ M₂) (g : M₂ →ₚ M₃) : M₁ →ₚ M₃

Equations

• f.comp g = LO.Kripke.Model.PseudoEpimorphism.mkAtomic (f.toFramePseudoEpimorphism.comp g.toFramePseudoEpimorphism) ⋯

def LO.Kripke.Model.PseudoEpimorphism.bisimulation {α : Type u_1} {M₁ : LO.Kripke.Model α} {M₂ : LO.Kripke.Model α} (f : M₁ →ₚ M₂) : M₁ ⇄ M₂

Equations

• f.bisimulation = { toRel := Function.graph f.toFun, atomic := ⋯, forth := ⋯, back := ⋯ }

def LO.Kripke.Frame.isRooted (F : LO.Kripke.Frame) (r : F.World) : Prop

Equations

• F.isRooted r = ∀ (w : F.World), w ≠ r → r ≺ w

structure LO.Kripke.RootedFrameextends LO.Kripke.Frame : Type (u_1 + 1)

• World : Type u_1
• Rel : Rel self.World self.World
• World_nonempty : Nonempty self.World
• root : self.World
• root_rooted : self.isRooted self.root
• default : self.World

theorem LO.Kripke.RootedFrame.root_rooted (self : LO.Kripke.RootedFrame) : self.isRooted self.root

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

Equations

• F.PointGenerated r = LO.Kripke.Frame.mk ↑{w : F.World | w = r ∨ r ≺ w} fun (x y : ↑{w : F.World | w = r ∨ r ≺ w}) => ↑x ≺ ↑y

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

theorem LO.Kripke.Frame.PointGenerated.rel_irreflexive {F : LO.Kripke.Frame} {r : F.World} (F_irrefl : Irreflexive F.Rel) : Irreflexive (F.PointGenerated r).Rel

theorem LO.Kripke.Frame.PointGenerated.rel_universal {F : LO.Kripke.Frame} {r : F.World} (F_refl : Reflexive F.Rel) (F_eucl : Euclidean F.Rel) : Universal (F.PointGenerated r).Rel

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

instance LO.Kripke.Frame.PointGenerated.instFiniteWorld {F : LO.Kripke.Frame} {r : F.World} [Finite F.World] : Finite (F.PointGenerated r).World

Equations

• ⋯ = ⋯

instance LO.Kripke.Frame.PointGenerated.instDecidableEqWorld {F : LO.Kripke.Frame} {r : F.World} [DecidableEq F.World] : DecidableEq (F.PointGenerated r).World

Equations

• LO.Kripke.Frame.PointGenerated.instDecidableEqWorld = Subtype.instDecidableEq

@[reducible, inline]

abbrev LO.Kripke.Frame.PointGenerated' (F : LO.Kripke.Frame) (r : F.World) : LO.Kripke.RootedFrame

Equations

• F↾r = { toFrame := LO.Kripke.Frame.mk (F.PointGenerated r).World (F.PointGenerated r).Rel, root := ⟨r, ⋯⟩, root_rooted := ⋯, default := ⟨r, ⋯⟩ }

def LO.Kripke.«term_↾_» : Lean.TrailingParserDescr

Equations

• LO.Kripke.«term_↾_» = Lean.ParserDescr.trailingNode `LO.Kripke.term_↾_ 100 101 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "↾") (Lean.ParserDescr.cat `term 101))

theorem LO.Kripke.Frame.PointGenerated'.rel_transitive {F : LO.Kripke.Frame} {r : F.World} : Transitive F.Rel → Transitive (F↾r).Rel

theorem LO.Kripke.Frame.PointGenerated'.rel_irreflexive {F : LO.Kripke.Frame} {r : F.World} : Irreflexive F.Rel → Irreflexive (F↾r).Rel

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

Equations

• M↾r = { Frame := (M.Frame↾r).toFrame, Valuation := fun (w : (M.Frame↾r).World) (a : α) => M.Valuation (↑w) a }

def LO.Kripke.«term_↾__1» : Lean.TrailingParserDescr

Equations

• LO.Kripke.«term_↾__1» = Lean.ParserDescr.trailingNode `LO.Kripke.term_↾__1 100 101 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "↾") (Lean.ParserDescr.cat `term 101))

def LO.Kripke.Model.PointGenerated.bisimulation {α : Type u_1} (M : LO.Kripke.Model α) (M_trans : Transitive M.Frame.Rel) (r : M.World) : M↾r ⇄ M

Equations

• LO.Kripke.Model.PointGenerated.bisimulation M M_trans r = { toRel := fun (x : (M↾r).World) (y : M.World) => ↑x = y, atomic := ⋯, forth := ⋯, back := ⋯ }

theorem LO.Kripke.Model.PointGenerated.bisimulation.rooted : ∀ {α : Type u_1} {M : LO.Kripke.Model α} {r : M.World} (M_trans : autoParam (Transitive M.Frame.Rel) _auto✝), (LO.Kripke.Model.PointGenerated.bisimulation M M_trans r).toRel ⟨r, ⋯⟩ r

structure LO.Kripke.Frame.GeneratedSub (F₁ : LO.Kripke.Frame) (F₂ : LO.Kripke.Frame) extends LO.Kripke.Frame.PseudoEpimorphism : Type (max u_1 u_2)

• toFun : F₁.World → F₂.World
• forth : ∀ {x y : F₁.World}, x ≺ y → self.toFun x ≺ self.toFun y
• back : ∀ {w : F₁.World} {v : F₂.World}, self.toFun w ≺ v → ∃ (u : F₁.World), self.toFun u = v ∧ w ≺ u
• monic : Function.Injective self.toFun

theorem LO.Kripke.Frame.GeneratedSub.monic {F₁ : LO.Kripke.Frame} {F₂ : LO.Kripke.Frame} (self : F₁ ⊆ₚ F₂) : Function.Injective self.toFun

def LO.Kripke.«term_⊆ₚ_» : Lean.TrailingParserDescr

Equations

• LO.Kripke.«term_⊆ₚ_» = Lean.ParserDescr.trailingNode `LO.Kripke.term_⊆ₚ_ 80 81 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊆ₚ ") (Lean.ParserDescr.cat `term 81))

def LO.Kripke.Frame.successors {F : LO.Kripke.Frame} (x : F.World) : Set F.World

Equations

• LO.Kripke.Frame.successors x = {w : F.World | x ≺^* w}

def LO.Kripke.Frame.«term_↑*» : Lean.TrailingParserDescr

Equations

• LO.Kripke.Frame.«term_↑*» = Lean.ParserDescr.trailingNode `LO.Kripke.Frame.term_↑* 100 100 (Lean.ParserDescr.symbol "↑*")

def LO.Kripke.Frame.immediate_successors {F : LO.Kripke.Frame} (x : F.World) : Set F.World

Equations

• LO.Kripke.Frame.immediate_successors x = {w : F.World | x ≺ w}

def LO.Kripke.Frame.«term_↑¹» : Lean.TrailingParserDescr

Equations

• LO.Kripke.Frame.«term_↑¹» = Lean.ParserDescr.trailingNode `LO.Kripke.Frame.term_↑¹ 100 100 (Lean.ParserDescr.symbol "↑¹")

def LO.Kripke.Frame.proper_immediate_successors {F : LO.Kripke.Frame} (x : F.World) : Set F.World

Equations

• LO.Kripke.Frame.proper_immediate_successors x = {w : F.World | x ≠ w ∧ x ≺ w}

def LO.Kripke.Frame.«term_↑» : Lean.TrailingParserDescr

Equations

• LO.Kripke.Frame.«term_↑» = Lean.ParserDescr.trailingNode `LO.Kripke.Frame.term_↑ 100 100 (Lean.ParserDescr.symbol "↑")

def LO.Kripke.Frame.predeccsors {F : LO.Kripke.Frame} (x : F.World) : Set F.World

Equations

• LO.Kripke.Frame.predeccsors x = {w : F.World | w ≺^* x}

def LO.Kripke.Frame.«term_↓*» : Lean.TrailingParserDescr

Equations

• LO.Kripke.Frame.«term_↓*» = Lean.ParserDescr.trailingNode `LO.Kripke.Frame.term_↓* 100 100 (Lean.ParserDescr.symbol "↓*")

def LO.Kripke.Frame.immediate_predeccsors {F : LO.Kripke.Frame} (x : F.World) : Set F.World

Equations

• LO.Kripke.Frame.immediate_predeccsors x = {w : F.World | w ≺ x}

def LO.Kripke.Frame.«term_↓¹» : Lean.TrailingParserDescr

Equations

• LO.Kripke.Frame.«term_↓¹» = Lean.ParserDescr.trailingNode `LO.Kripke.Frame.term_↓¹ 100 100 (Lean.ParserDescr.symbol "↓¹")

def LO.Kripke.Frame.proper_immediate_predeccsors {F : LO.Kripke.Frame} (x : F.World) : Set F.World

Equations

• x↓ = {w : F.World | w ≠ x ∧ w ≺ x}

def LO.Kripke.Frame.«term_↓» : Lean.TrailingParserDescr

Equations

• LO.Kripke.Frame.«term_↓» = Lean.ParserDescr.trailingNode `LO.Kripke.Frame.term_↓ 100 100 (Lean.ParserDescr.symbol "↓")