S5

def LO.Entailment.diaboxBox {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [Entailment F S] {𝓢 : S} [Entailment.S5 𝓢] {φ : F} : 𝓢 ⊢ ◇□φ ==> □φ

Imported declaration from the Incompleteness formalization.

Equations

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

@[simp]

theorem LO.Entailment.diaboxBox! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [Entailment.S5 𝓢] {φ : F} : 𝓢 ⊢! ◇□φ ==> □φ

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

Imported declaration from the Incompleteness formalization.

Equations

• LO.Entailment.diaboxBox' h = LO.Entailment.diaboxBox⨀h

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

def LO.Entailment.rmDiabox {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [Entailment F S] {𝓢 : S} [Entailment.S5 𝓢] {φ : F} : 𝓢 ⊢ ◇□φ ==> φ

Imported declaration from the Incompleteness formalization.

Equations

• LO.Entailment.rmDiabox = LO.Entailment.impTrans'' LO.Entailment.diaboxBox LO.Entailment.axiomT

@[simp]

theorem LO.Entailment.rmDiabox! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [Entailment.S5 𝓢] {φ : F} : 𝓢 ⊢! ◇□φ ==> φ

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

Imported declaration from the Incompleteness formalization.

Equations

• LO.Entailment.rmDiabox' h = LO.Entailment.rmDiabox⨀h

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