def LO.System.iff_box_boxdot {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓢 : S} [System.S4 𝓢] {φ : F} : 𝓢 ⊢ □φ ⭤ ⊡φ

Equations

• LO.System.iff_box_boxdot = LO.System.iffIntro (LO.System.implyRightAnd LO.System.axiomT (LO.System.impId (□φ))) LO.System.and₂

@[simp]

theorem LO.System.iff_box_boxdot! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓢 : S} [System.S4 𝓢] {φ : F} : 𝓢 ⊢! □φ ⭤ ⊡φ

def LO.System.iff_dia_diadot {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓢 : S} [System.S4 𝓢] {φ : F} : 𝓢 ⊢ ◇φ ⭤ ⟐φ

Equations

• LO.System.iff_dia_diadot = LO.System.iffIntro LO.System.or₂ (LO.System.or₃'' LO.System.diaTc (LO.System.impId (◇φ)))

@[simp]

theorem LO.System.iff_dia_diadot! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓢 : S} [System.S4 𝓢] {φ : F} : 𝓢 ⊢! ◇φ ⭤ ⟐φ