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

Equations

• LO.System.diaTc = LO.System.impTrans'' (LO.System.impTrans'' LO.System.dni (LO.System.contra₀' LO.System.axiomT)) (LO.System.and₂' LO.System.diaDuality)

@[simp]

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

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

Equations

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

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