Substitution

@[reducible, inline]

abbrev LO.Modal.Substitution (α : Type u_1) : Type u_1

Imported declaration from the Incompleteness formalization.

Equations

• LO.Modal.Substitution α = (α → LO.Modal.Formula α)

@[reducible, inline]

abbrev LO.Modal.Substitution.id {α : Type u_1} : Substitution α

Imported declaration from the Incompleteness formalization.

Equations

• LO.Modal.Substitution.id a = LO.Modal.Formula.atom a

def LO.Modal.Formula.subst {α : Type u_1} (s : Substitution α) : Formula α → Formula α

Imported declaration from the Incompleteness formalization.

Equations

• LO.Modal.Formula.atom a⟦s⟧ = s a
• LO.Modal.Formula.falsum⟦s⟧ = ⊥
• φ.box⟦s⟧ = □φ⟦s⟧
• φ.imp ψ⟦s⟧ = φ⟦s⟧ ==> ψ⟦s⟧

def LO.Modal.Formula.«term_⟦_⟧» : Lean.TrailingParserDescr

Imported declaration from the Incompleteness formalization.

Equations

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

@[simp]

theorem LO.Modal.Formula.subst_atom {α : Type u_1} {s : Substitution α} {a : α} : atom a⟦s⟧ = s a

@[simp]

theorem LO.Modal.Formula.subst_bot {α : Type u_1} {s : Substitution α} : ⊥⟦s⟧ = ⊥

@[simp]

theorem LO.Modal.Formula.subst_imp {α : Type u_1} {φ ψ : Formula α} {s : Substitution α} : (φ ==> ψ)⟦s⟧ = φ⟦s⟧ ==> ψ⟦s⟧

@[simp]

theorem LO.Modal.Formula.subst_neg {α : Type u_1} {φ : Formula α} {s : Substitution α} : (∼φ)⟦s⟧ = ∼φ⟦s⟧

@[simp]

theorem LO.Modal.Formula.subst_and {α : Type u_1} {φ ψ : Formula α} {s : Substitution α} : (φ ⋏ ψ)⟦s⟧ = φ⟦s⟧ ⋏ ψ⟦s⟧

@[simp]

theorem LO.Modal.Formula.subst_or {α : Type u_1} {φ ψ : Formula α} {s : Substitution α} : (φ ⋎ ψ)⟦s⟧ = φ⟦s⟧ ⋎ ψ⟦s⟧

@[simp]

theorem LO.Modal.Formula.subst_iff {α : Type u_1} {φ ψ : Formula α} {s : Substitution α} : (φ <=> ψ)⟦s⟧ = φ⟦s⟧ <=> ψ⟦s⟧

@[simp]

theorem LO.Modal.Formula.subst_box {α : Type u_1} {φ : Formula α} {s : Substitution α} : (□φ)⟦s⟧ = □φ⟦s⟧

@[simp]

theorem LO.Modal.Formula.subst_multibox {α : Type u_1} {φ : Formula α} {s : Substitution α} {n : ℕ} : (□^[n]φ)⟦s⟧ = □^[n]φ⟦s⟧

@[simp]

theorem LO.Modal.Formula.subst_dia {α : Type u_1} {φ : Formula α} {s : Substitution α} : (◇φ)⟦s⟧ = ◇φ⟦s⟧

@[simp]

theorem LO.Modal.Formula.subst_multidia {α : Type u_1} {φ : Formula α} {s : Substitution α} {n : ℕ} : (◇^[n]φ)⟦s⟧ = ◇^[n]φ⟦s⟧

@[simp]

theorem LO.Modal.subst_id {α : Type u_1} {φ : Formula α} : φ⟦Substitution.id⟧ = φ

def LO.Modal.Substitution.comp {α : Type u_1} (s₁ s₂ : Substitution α) : Substitution α

Imported declaration from the Incompleteness formalization.

Equations

• (s₁ ∘ s₂) a = s₁ a⟦s₂⟧

def LO.Modal.«term_∘_» : Lean.TrailingParserDescr

Imported declaration from the Incompleteness formalization.

Equations

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

@[simp]

theorem LO.Modal.subst_comp {α : Type u_1} {s₁ s₂ : Substitution α} {φ : Formula α} : φ⟦s₁ ∘ s₂⟧ = φ⟦s₁⟧⟦s₂⟧

class LO.Modal.SubstitutionClosed {α : Type u_1} (S : Set (Formula α)) : Prop

Imported declaration from the Incompleteness formalization.

• closed (φ : Formula α) : φ ∈ S → ∀ (s : Substitution α), φ⟦s⟧ ∈ S