Documentation

Logic.Modal.Standard.Kripke.ComplexityLimited

source
def LO.Modal.Standard.Kripke.Frame.ComplexityLimit {α : Type u_1} {F : LO.Modal.Standard.Kripke.Frame} (r : F.World) (p : LO.Modal.Standard.Formula α) :
LO.Modal.Standard.Kripke.Frame
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def LO.Modal.Standard.Kripke.Model.ComplexityLimit {α : Type u_1} {M : LO.Modal.Standard.Kripke.Model α} (w : M.World) (p : LO.Modal.Standard.Formula α) :
    LO.Modal.Standard.Kripke.Model α
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem LO.Modal.Standard.Kripke.iff_satisfy_complexity_limit_modelAux {α : Type u_1} [DecidableEq α] {M : LO.Modal.Standard.Kripke.Model α} {r : M.World} {x : M.World} {p : LO.Modal.Standard.Formula α} {q : LO.Modal.Standard.Formula α} (hq : q ∈ 𝒮 p) (hx : ∃ n ≤ p.complexity - q.complexity, LO.Modal.Standard.Kripke.Frame.RelItr' n r x) :
      x ⊧ q ↔ LO.Modal.Standard.Formula.Kripke.Satisfies (LO.Modal.Standard.Kripke.Model.ComplexityLimit r p) ⟨x, ⋯⟩ q
      source
      theorem LO.Modal.Standard.Kripke.iff_satisfy_complexity_limit_model {α : Type u_1} [DecidableEq α] {M : LO.Modal.Standard.Kripke.Model α} {r : M.World} {p : LO.Modal.Standard.Formula α} :
      r ⊧ p ↔ LO.Modal.Standard.Formula.Kripke.Satisfies (LO.Modal.Standard.Kripke.Model.ComplexityLimit r p) ⟨r, ⋯⟩ p
      source
      theorem LO.Modal.Standard.Kripke.complexity_limit_model_subformula_closedAux {α : Type u_1} [DecidableEq α] {M : LO.Modal.Standard.Kripke.Model α} {r : M.World} {p : LO.Modal.Standard.Formula α} {q₁ : LO.Modal.Standard.Formula α} {q₂ : LO.Modal.Standard.Formula α} (hq₁ : p ∈ 𝒮 q₁) (hq₂ : p ∈ 𝒮 q₂) :
      LO.Modal.Standard.Formula.Kripke.Satisfies (LO.Modal.Standard.Kripke.Model.ComplexityLimit r q₁) ⟨r, ⋯⟩ p → LO.Modal.Standard.Formula.Kripke.Satisfies (LO.Modal.Standard.Kripke.Model.ComplexityLimit r q₂) ⟨r, ⋯⟩ p
      source
      theorem LO.Modal.Standard.Kripke.complexity_limit_model_subformula_closed {α : Type u_1} [DecidableEq α] {M : LO.Modal.Standard.Kripke.Model α} {r : M.World} {p : LO.Modal.Standard.Formula α} {q : LO.Modal.Standard.Formula α} (hq : p ∈ 𝒮 q) :
      LO.Modal.Standard.Formula.Kripke.Satisfies (LO.Modal.Standard.Kripke.Model.ComplexityLimit r p) ⟨r, ⋯⟩ p ↔ LO.Modal.Standard.Formula.Kripke.Satisfies (LO.Modal.Standard.Kripke.Model.ComplexityLimit r q) ⟨r, ⋯⟩ p