def LO.System.diabox_box {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓢 : S} [System.S5 𝓢] {φ : F} : 𝓢 ⊢ ◇□φ ➝ □φ

Equations

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

@[simp]

theorem LO.System.diabox_box! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓢 : S} [System.S5 𝓢] {φ : F} : 𝓢 ⊢! ◇□φ ➝ □φ

def LO.System.diabox_box' {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓢 : S} [System.S5 𝓢] {φ : F} (h : 𝓢 ⊢ ◇□φ) : 𝓢 ⊢ □φ

Equations

• LO.System.diabox_box' h = LO.System.diabox_box⨀h

theorem LO.System.diabox_box'! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓢 : S} [System.S5 𝓢] {φ : F} (h : 𝓢 ⊢! ◇□φ) : 𝓢 ⊢! □φ

def LO.System.rm_diabox {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓢 : S} [System.S5 𝓢] {φ : F} : 𝓢 ⊢ ◇□φ ➝ φ

Equations

• LO.System.rm_diabox = LO.System.impTrans'' LO.System.diabox_box LO.System.axiomT

@[simp]

theorem LO.System.rm_diabox! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓢 : S} [System.S5 𝓢] {φ : F} : 𝓢 ⊢! ◇□φ ➝ φ

def LO.System.rm_diabox' {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓢 : S} [System.S5 𝓢] {φ : F} (h : 𝓢 ⊢ ◇□φ) : 𝓢 ⊢ φ

Equations

• LO.System.rm_diabox' h = LO.System.rm_diabox⨀h

theorem LO.System.rm_diabox'! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓢 : S} [System.S5 𝓢] {φ : F} (h : 𝓢 ⊢! ◇□φ) : 𝓢 ⊢! φ