def LO.Modal.Kripke.ComplexityLimitedFrame {α : Type u_1} (F : LO.Kripke.Frame) (r : F.World) (p : LO.Modal.Formula α) : LO.Kripke.Frame

Equations

• LO.Modal.Kripke.ComplexityLimitedFrame F r p = LO.Kripke.Frame.mk ↑{x : F.World | ∃ n ≤ p.complexity, r ≺^[n] x} fun (x y : ↑{x : F.World | ∃ n ≤ p.complexity, r ≺^[n] x}) => ↑x ≺ ↑y

def LO.Modal.Kripke.ComplexityLimitedModel {α : Type u_1} (M : LO.Kripke.Model α) (w : M.World) (p : LO.Modal.Formula α) : LO.Kripke.Model α

Equations

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

theorem LO.Modal.Kripke.iff_satisfy_complexity_limit_modelAux {α : Type u_1} [DecidableEq α] {M : LO.Kripke.Model α} {r : M.World} {x : M.World} {p : LO.Modal.Formula α} {q : LO.Modal.Formula α} (hq : q ∈ 𝒮 p) (hx : ∃ n ≤ p.complexity - q.complexity, r ≺^[n] x) : x ⊧ q ↔ LO.Modal.Formula.Kripke.Satisfies (LO.Modal.Kripke.ComplexityLimitedModel M r p) ⟨x, ⋯⟩ q

theorem LO.Modal.Kripke.iff_satisfy_complexity_limit_model {α : Type u_1} [DecidableEq α] {M : LO.Kripke.Model α} {r : M.World} {p : LO.Modal.Formula α} : r ⊧ p ↔ LO.Modal.Formula.Kripke.Satisfies (LO.Modal.Kripke.ComplexityLimitedModel M r p) ⟨r, ⋯⟩ p

theorem LO.Modal.Kripke.complexity_limit_model_subformula_closedAux {α : Type u_1} [DecidableEq α] {M : LO.Kripke.Model α} {r : M.World} {p : LO.Modal.Formula α} {q₁ : LO.Modal.Formula α} {q₂ : LO.Modal.Formula α} (hq₁ : p ∈ 𝒮 q₁) (hq₂ : p ∈ 𝒮 q₂) : LO.Modal.Formula.Kripke.Satisfies (LO.Modal.Kripke.ComplexityLimitedModel M r q₁) ⟨r, ⋯⟩ p → LO.Modal.Formula.Kripke.Satisfies (LO.Modal.Kripke.ComplexityLimitedModel M r q₂) ⟨r, ⋯⟩ p

theorem LO.Modal.Kripke.complexity_limit_model_subformula_closed {α : Type u_1} [DecidableEq α] {M : LO.Kripke.Model α} {r : M.World} {p : LO.Modal.Formula α} {q : LO.Modal.Formula α} (hq : p ∈ 𝒮 q) : LO.Modal.Formula.Kripke.Satisfies (LO.Modal.Kripke.ComplexityLimitedModel M r p) ⟨r, ⋯⟩ p ↔ LO.Modal.Formula.Kripke.Satisfies (LO.Modal.Kripke.ComplexityLimitedModel M r q) ⟨r, ⋯⟩ p