def LO.System.imply_BoxBoxdot_Box {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [DecidableEq F] [LO.System F S] {𝓢 : S} [LO.System.K4 𝓢] {φ : F} : 𝓢 ⊢ □⊡φ ➝ □φ

Equations

• LO.System.imply_BoxBoxdot_Box = LO.System.impTrans'' LO.System.distribute_box_and LO.System.and₁

@[simp]

theorem LO.System.imply_boxboxdot_box {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [DecidableEq F] [LO.System F S] {𝓢 : S} [LO.System.K4 𝓢] {φ : F} : 𝓢 ⊢! □⊡φ ➝ □φ

def LO.System.imply_Box_BoxBoxdot {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [DecidableEq F] [LO.System F S] {𝓢 : S} [LO.System.K4 𝓢] {φ : F} : 𝓢 ⊢ □φ ➝ □⊡φ

Equations

• LO.System.imply_Box_BoxBoxdot = LO.System.impTrans'' (LO.System.implyRightAnd (LO.System.impId (□φ)) LO.System.axiomFour) LO.System.collect_box_and

@[simp]

theorem LO.System.imply_box_boxboxdot! {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [DecidableEq F] [LO.System F S] {𝓢 : S} [LO.System.K4 𝓢] {φ : F} : 𝓢 ⊢! □φ ➝ □⊡φ

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

Equations

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

def LO.System.imply_Box_BoxBoxdot'! {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [DecidableEq F] [LO.System F S] {𝓢 : S} [LO.System.K4 𝓢] {φ : F} (h : 𝓢 ⊢! □φ) : 𝓢 ⊢! □⊡φ

Equations

• ⋯ = ⋯

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

Equations

• LO.System.iff_Box_BoxBoxdot = LO.System.iffIntro LO.System.imply_Box_BoxBoxdot LO.System.imply_BoxBoxdot_Box

@[simp]

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

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

Equations

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

@[simp]

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

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

Equations

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

@[simp]

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

def LO.System.boxdotAxiomFour {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [DecidableEq F] [LO.System F S] {𝓢 : S} [LO.System.K4 𝓢] {φ : F} : 𝓢 ⊢ ⊡φ ➝ ⊡⊡φ

Equations

• LO.System.boxdotAxiomFour = LO.System.and₁' LO.System.iff_Boxdot_BoxdotBoxdot

@[simp]

theorem LO.System.boxdot_axiomFour! {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [DecidableEq F] [LO.System F S] {𝓢 : S} [LO.System.K4 𝓢] {φ : F} : 𝓢 ⊢! ⊡φ ➝ ⊡⊡φ