def LO.Modal.Formula.BoxdotTranslation {α : Type u_1} : LO.Modal.Formula α → LO.Modal.Formula α

Equations

• LO.Modal.Formula.atom aᵇ = LO.Modal.Formula.atom a
• LO.Modal.Formula.falsumᵇ = ⊥
• φ.imp ψᵇ = φᵇ ➝ ψᵇ
• φ.boxᵇ = ⊡φᵇ

def LO.Modal.«term_ᵇ» : Lean.TrailingParserDescr

Equations

• LO.Modal.«term_ᵇ» = Lean.ParserDescr.trailingNode `LO.Modal.«term_ᵇ» 90 90 (Lean.ParserDescr.symbol "ᵇ")

class LO.Modal.BoxdotProperty {α : Type u_1} (H₁ H₂ : LO.Modal.Hilbert α) : Prop

• bdp : ∀ {φ : LO.Modal.Formula α}, H₁ ⊢! φᵇ ↔ H₂ ⊢! φ

theorem LO.Modal.boxdotTranslated {α : Type u_1} [DecidableEq α] {φ : LO.Modal.Formula α} {H₁ H₂ : LO.Modal.Hilbert α} [H₁.IsNormal] [H₂.IsNormal] (h : ∀ φ ∈ H₁.axioms, H₂ ⊢! φᵇ) : H₁ ⊢! φ → H₂ ⊢! φᵇ