K #

source

def LO.Entailment.multiboxAxiomK {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] {n : ℕ} {φ ψ : F} :

𝓢 ⊢ □^[n](φ ==> ψ) ==> □^[n]φ ==> □^[n]ψ

Imported declaration from the Incompleteness formalization.

Equations

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

Instances For

source

@[simp]

theorem LO.Entailment.multiboxAxiomK! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] {n : ℕ} {φ ψ : F} :

𝓢 ⊢! □^[n](φ ==> ψ) ==> □^[n]φ ==> □^[n]ψ

source

def LO.Entailment.multiboxAxiomK' {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] {n : ℕ} {φ ψ : F} (h : 𝓢 ⊢ □^[n](φ ==> ψ)) :

𝓢 ⊢ □^[n]φ ==> □^[n]ψ

Imported declaration from the Incompleteness formalization.

Equations

LO.Entailment.multiboxAxiomK' h = LO.Entailment.multiboxAxiomK ⨀h

Instances For

source

@[simp]

theorem LO.Entailment.multiboxAxiomK'! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] {n : ℕ} {φ ψ : F} (h : 𝓢 ⊢! □^[n](φ ==> ψ)) :

𝓢 ⊢! □^[n]φ ==> □^[n]ψ

source

def LO.Entailment.multiboxedImplyDistribute {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] {n : ℕ} {φ ψ : F} (h : 𝓢 ⊢ □^[n](φ ==> ψ)) :

𝓢 ⊢ □^[n]φ ==> □^[n]ψ

Alias of LO.Entailment.multiboxAxiomK'.

Imported declaration from the Incompleteness formalization.

Equations

@LO.Entailment.multiboxedImplyDistribute = @LO.Entailment.multiboxAxiomK'

Instances For

source

theorem LO.Entailment.multiboxed_imply_distribute! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] {n : ℕ} {φ ψ : F} (h : 𝓢 ⊢! □^[n](φ ==> ψ)) :

𝓢 ⊢! □^[n]φ ==> □^[n]ψ

Alias of LO.Entailment.multiboxAxiomK'!.

source

def LO.Entailment.boxIff' {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] {φ ψ : F} (h : 𝓢 ⊢ φ <=> ψ) :

𝓢 ⊢ □φ <=> □ψ

Imported declaration from the Incompleteness formalization.

Equations

LO.Entailment.boxIff' h = LO.Entailment.iffIntro (LO.Entailment.axiomK' (LO.Entailment.nec (LO.Entailment.and₁' h))) (LO.Entailment.axiomK' (LO.Entailment.nec (LO.Entailment.and₂' h)))

Instances For

source

@[simp]

theorem LO.Entailment.box_iff! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] {φ ψ : F} (h : 𝓢 ⊢! φ <=> ψ) :

𝓢 ⊢! □φ <=> □ψ

source

def LO.Entailment.multiboxIff' {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] {φ ψ : F} {n : ℕ} (h : 𝓢 ⊢ φ <=> ψ) :

𝓢 ⊢ □^[n]φ <=> □^[n]ψ

Imported declaration from the Incompleteness formalization.

Equations

LO.Entailment.multiboxIff' h = Nat.recAux (id h) (fun (n : ℕ) (ih : 𝓢 ⊢ □^[n]φ <=> □^[n]ψ) => ⋯.mpr (LO.Entailment.boxIff' ih)) n

Instances For

source

@[simp]

theorem LO.Entailment.multibox_iff! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] {φ ψ : F} {n : ℕ} (h : 𝓢 ⊢! φ <=> ψ) :

𝓢 ⊢! □^[n]φ <=> □^[n]ψ

source

def LO.Entailment.diaDualityMp {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] {φ : F} :

𝓢 ⊢ ◇φ ==> ∼□(∼φ)

Imported declaration from the Incompleteness formalization.

Equations

LO.Entailment.diaDualityMp = LO.Entailment.and₁' LO.Entailment.diaDuality

Instances For

source

@[simp]

theorem LO.Entailment.diaDualityMp! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] {φ : F} :

𝓢 ⊢! ◇φ ==> ∼□(∼φ)

source

def LO.Entailment.diaDualityMpr {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] {φ : F} :

𝓢 ⊢ ∼□(∼φ) ==> ◇φ

Imported declaration from the Incompleteness formalization.

Equations

LO.Entailment.diaDualityMpr = LO.Entailment.and₂' LO.Entailment.diaDuality

Instances For

source

@[simp]

theorem LO.Entailment.diaDualityMpr! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] {φ : F} :

𝓢 ⊢! ∼□(∼φ) ==> ◇φ

source

def LO.Entailment.diaDuality'.mp {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] {φ : F} (h : 𝓢 ⊢ ◇φ) :

𝓢 ⊢ ∼□(∼φ)

Imported declaration from the Incompleteness formalization.

Equations

LO.Entailment.diaDuality'.mp h = LO.Entailment.and₁' LO.Entailment.diaDuality⨀h

Instances For

source

def LO.Entailment.diaDuality'.mpr {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] {φ : F} (h : 𝓢 ⊢ ∼□(∼φ)) :

𝓢 ⊢ ◇φ

Imported declaration from the Incompleteness formalization.

Equations

LO.Entailment.diaDuality'.mpr h = LO.Entailment.and₂' LO.Entailment.diaDuality⨀h

Instances For

source

theorem LO.Entailment.dia_duality'! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] {φ : F} :

𝓢 ⊢! ◇φ ↔ 𝓢 ⊢! ∼□(∼φ)

source

def LO.Entailment.multiDiaDuality {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] {n : ℕ} {φ : F} :

𝓢 ⊢ ◇^[n]φ <=> ∼□^[n](∼φ)

Imported declaration from the Incompleteness formalization.

Equations

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

Instances For

source

theorem LO.Entailment.multidia_duality! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] {n : ℕ} {φ : F} :

𝓢 ⊢! ◇^[n]φ <=> ∼□^[n](∼φ)

source

theorem LO.Entailment.multidia_duality'! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] {n : ℕ} {φ : F} :

𝓢 ⊢! ◇^[n]φ ↔ 𝓢 ⊢! ∼□^[n](∼φ)

source

def LO.Entailment.diaIff' {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] {φ ψ : F} (h : 𝓢 ⊢ φ <=> ψ) :

𝓢 ⊢ ◇φ <=> ◇ψ

Imported declaration from the Incompleteness formalization.

Equations

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

Instances For

source

@[simp]

theorem LO.Entailment.dia_iff! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] {φ ψ : F} (h : 𝓢 ⊢! φ <=> ψ) :

𝓢 ⊢! ◇φ <=> ◇ψ

source

def LO.Entailment.multidiaIff' {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] {φ ψ : F} {n : ℕ} (h : 𝓢 ⊢ φ <=> ψ) :

𝓢 ⊢ ◇^[n]φ <=> ◇^[n]ψ

Imported declaration from the Incompleteness formalization.

Equations

LO.Entailment.multidiaIff' h = Nat.recAux (id h) (fun (n : ℕ) (ih : 𝓢 ⊢ ◇^[n]φ <=> ◇^[n]ψ) => ⋯.mpr (LO.Entailment.diaIff' ih)) n

Instances For

source

@[simp]

theorem LO.Entailment.multidia_iff! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] {φ ψ : F} {n : ℕ} (h : 𝓢 ⊢! φ <=> ψ) :

𝓢 ⊢! ◇^[n]φ <=> ◇^[n]ψ

source

def LO.Entailment.multiboxDuality {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] {n : ℕ} {φ : F} :

𝓢 ⊢ □^[n]φ <=> ∼◇^[n](∼φ)

Imported declaration from the Incompleteness formalization.

Equations

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

Instances For

source

@[simp]

theorem LO.Entailment.multibox_duality! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] {n : ℕ} {φ : F} :

𝓢 ⊢! □^[n]φ <=> ∼◇^[n](∼φ)

source

def LO.Entailment.boxDuality {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] {φ : F} :

𝓢 ⊢ □φ <=> ∼◇(∼φ)

Imported declaration from the Incompleteness formalization.

Equations

LO.Entailment.boxDuality = LO.Entailment.multiboxDuality

Instances For

source

@[simp]

theorem LO.Entailment.box_duality! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] {φ : F} :

𝓢 ⊢! □φ <=> ∼◇(∼φ)

source

def LO.Entailment.boxDualityMp {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] {φ : F} :

𝓢 ⊢ □φ ==> ∼◇(∼φ)

Imported declaration from the Incompleteness formalization.

Equations

LO.Entailment.boxDualityMp = LO.Entailment.and₁' LO.Entailment.boxDuality

Instances For

source

@[simp]

theorem LO.Entailment.boxDualityMp! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] {φ : F} :

𝓢 ⊢! □φ ==> ∼◇(∼φ)

source

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

𝓢 ⊢ ∼◇(∼φ)

Imported declaration from the Incompleteness formalization.

Equations

LO.Entailment.boxDualityMp' h = LO.Entailment.boxDualityMp ⨀h

Instances For

source

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

𝓢 ⊢! ∼◇(∼φ)

source

def LO.Entailment.boxDualityMpr {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] {φ : F} :

𝓢 ⊢ ∼◇(∼φ) ==> □φ

Imported declaration from the Incompleteness formalization.

Equations

LO.Entailment.boxDualityMpr = LO.Entailment.and₂' LO.Entailment.boxDuality

Instances For

source

@[simp]

theorem LO.Entailment.boxDualityMpr! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] {φ : F} :

𝓢 ⊢! ∼◇(∼φ) ==> □φ

source

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

𝓢 ⊢ □φ

Imported declaration from the Incompleteness formalization.

Equations

LO.Entailment.boxDualityMpr' h = LO.Entailment.boxDualityMpr ⨀h

Instances For

source

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

𝓢 ⊢! □φ

source

theorem LO.Entailment.multibox_duality'! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] {n : ℕ} {φ : F} :

𝓢 ⊢! □^[n]φ ↔ 𝓢 ⊢! ∼◇^[n](∼φ)

source

theorem LO.Entailment.box_duality'! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] {φ : F} :

𝓢 ⊢! □φ ↔ 𝓢 ⊢! ∼◇(∼φ)

source

def LO.Entailment.boxDni {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] {φ : F} :

𝓢 ⊢ □φ ==> □(∼∼φ)

Imported declaration from the Incompleteness formalization.

Equations

LO.Entailment.boxDni = LO.Entailment.axiomK' (LO.Entailment.nec LO.Entailment.dni)

Instances For

source

@[simp]

theorem LO.Entailment.boxDni! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] {φ : F} :

𝓢 ⊢! □φ ==> □(∼∼φ)

source

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

𝓢 ⊢ □(∼∼φ)

Imported declaration from the Incompleteness formalization.

Equations

LO.Entailment.boxDni' h = LO.Entailment.boxDni ⨀h

Instances For

source

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

𝓢 ⊢! □(∼∼φ)

source

def LO.Entailment.boxDne {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] {φ : F} :

𝓢 ⊢ □(∼∼φ) ==> □φ

Imported declaration from the Incompleteness formalization.

Equations

LO.Entailment.boxDne = LO.Entailment.axiomK' (LO.Entailment.nec LO.Entailment.dne)

Instances For

source

@[simp]

theorem LO.Entailment.boxDne! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] {φ : F} :

𝓢 ⊢! □(∼∼φ) ==> □φ

source

def LO.Entailment.boxDne' {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] {φ : F} (h : 𝓢 ⊢ □(∼∼φ)) :

𝓢 ⊢ □φ

Imported declaration from the Incompleteness formalization.

Equations

LO.Entailment.boxDne' h = LO.Entailment.boxDne ⨀h

Instances For

source

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

𝓢 ⊢! □φ

source

def LO.Entailment.multiboxverum {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] {n : ℕ} :

𝓢 ⊢ □^[n]⊤

Imported declaration from the Incompleteness formalization.

Equations

LO.Entailment.multiboxverum = LO.Entailment.multinec LO.Entailment.verum

Instances For

source

@[simp]

theorem LO.Entailment.multiboxverum! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] {n : ℕ} :

𝓢 ⊢! □^[n]⊤

source

def LO.Entailment.boxverum {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] :

𝓢 ⊢ □⊤

Imported declaration from the Incompleteness formalization.

Equations

LO.Entailment.boxverum = LO.Entailment.multiboxverum

Instances For

source

@[simp]

theorem LO.Entailment.boxverum! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] :

𝓢 ⊢! □⊤

source

def LO.Entailment.boxdotverum {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] :

𝓢 ⊢ ⊡⊤

Imported declaration from the Incompleteness formalization.

Equations

LO.Entailment.boxdotverum = LO.Entailment.andIntro LO.Entailment.verum LO.Entailment.boxverum

Instances For

source

@[simp]

theorem LO.Entailment.boxdotverum! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] :

𝓢 ⊢! ⊡⊤

source

def LO.Entailment.implyMultiboxDistribute' {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] {φ ψ : F} {n : ℕ} (h : 𝓢 ⊢ φ ==> ψ) :

𝓢 ⊢ □^[n]φ ==> □^[n]ψ

Imported declaration from the Incompleteness formalization.

Equations

LO.Entailment.implyMultiboxDistribute' h = LO.Entailment.multiboxAxiomK' (LO.Entailment.multinec h)

Instances For

source

theorem LO.Entailment.imply_multibox_distribute'! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] {φ ψ : F} {n : ℕ} (h : 𝓢 ⊢! φ ==> ψ) :

𝓢 ⊢! □^[n]φ ==> □^[n]ψ

source

def LO.Entailment.implyBoxDistribute' {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] {φ ψ : F} (h : 𝓢 ⊢ φ ==> ψ) :

𝓢 ⊢ □φ ==> □ψ

Imported declaration from the Incompleteness formalization.

Equations

LO.Entailment.implyBoxDistribute' h = LO.Entailment.implyMultiboxDistribute' h

Instances For

source

theorem LO.Entailment.imply_box_distribute'! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] {φ ψ : F} (h : 𝓢 ⊢! φ ==> ψ) :

𝓢 ⊢! □φ ==> □ψ

source

def LO.Entailment.distributeMultiboxAnd {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] {n : ℕ} {φ ψ : F} :

𝓢 ⊢ □^[n](φ ⋏ ψ) ==> □^[n]φ ⋏ □^[n]ψ

Imported declaration from the Incompleteness formalization.

Equations

LO.Entailment.distributeMultiboxAnd = LO.Entailment.implyRightAnd (LO.Entailment.implyMultiboxDistribute' LO.Entailment.and₁) (LO.Entailment.implyMultiboxDistribute' LO.Entailment.and₂)

Instances For

source

@[simp]

theorem LO.Entailment.distributeMultiboxAnd! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] {n : ℕ} {φ ψ : F} :

𝓢 ⊢! □^[n](φ ⋏ ψ) ==> □^[n]φ ⋏ □^[n]ψ

source

def LO.Entailment.distributeBoxAnd {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] {φ ψ : F} :

𝓢 ⊢ □(φ ⋏ ψ) ==> □φ ⋏ □ψ

Imported declaration from the Incompleteness formalization.

Equations

LO.Entailment.distributeBoxAnd = LO.Entailment.distributeMultiboxAnd

Instances For

source

@[simp]

theorem LO.Entailment.distributeBoxAnd! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] {φ ψ : F} :

𝓢 ⊢! □(φ ⋏ ψ) ==> □φ ⋏ □ψ

source

def LO.Entailment.distributeMultiboxAnd' {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] {n : ℕ} {φ ψ : F} (h : 𝓢 ⊢ □^[n](φ ⋏ ψ)) :

𝓢 ⊢ □^[n]φ ⋏ □^[n]ψ

Imported declaration from the Incompleteness formalization.

Equations

LO.Entailment.distributeMultiboxAnd' h = LO.Entailment.distributeMultiboxAnd ⨀h

Instances For

source

theorem LO.Entailment.distributeMultiboxAnd'! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] {n : ℕ} {φ ψ : F} (d : 𝓢 ⊢! □^[n](φ ⋏ ψ)) :

𝓢 ⊢! □^[n]φ ⋏ □^[n]ψ

source

def LO.Entailment.distributeBoxAnd' {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] {φ ψ : F} (h : 𝓢 ⊢ □(φ ⋏ ψ)) :

𝓢 ⊢ □φ ⋏ □ψ

Imported declaration from the Incompleteness formalization.

Equations

LO.Entailment.distributeBoxAnd' h = LO.Entailment.distributeMultiboxAnd' h

Instances For

source

theorem LO.Entailment.distributeBoxAnd'! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] {φ ψ : F} (d : 𝓢 ⊢! □(φ ⋏ ψ)) :

𝓢 ⊢! □φ ⋏ □ψ

source

theorem LO.Entailment.conj_cons! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] {φ : F} {Γ : List F} :

𝓢 ⊢! φ ⋏ ⋀Γ <=> ⋀(φ :: Γ)

source

@[simp]

theorem LO.Entailment.distribute_multibox_conj! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] {n : ℕ} {Γ : List F} :

𝓢 ⊢! □^[n]⋀Γ ==> ⋀□'^[n]Γ

source

@[simp]

theorem LO.Entailment.distribute_box_conj! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] {Γ : List F} :

𝓢 ⊢! □⋀Γ ==> ⋀□'Γ

source

def LO.Entailment.collectMultiboxAnd {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] {n : ℕ} {φ ψ : F} :

𝓢 ⊢ □^[n]φ ⋏ □^[n]ψ ==> □^[n](φ ⋏ ψ)

Imported declaration from the Incompleteness formalization.

Equations

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

Instances For

source

@[simp]

theorem LO.Entailment.collectMultiboxAnd! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] {n : ℕ} {φ ψ : F} :

𝓢 ⊢! □^[n]φ ⋏ □^[n]ψ ==> □^[n](φ ⋏ ψ)

source

def LO.Entailment.collectBoxAnd {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] {φ ψ : F} :

𝓢 ⊢ □φ ⋏ □ψ ==> □(φ ⋏ ψ)

Imported declaration from the Incompleteness formalization.

Equations

LO.Entailment.collectBoxAnd = LO.Entailment.collectMultiboxAnd

Instances For

source

@[simp]

theorem LO.Entailment.collectBoxAnd! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] {φ ψ : F} :

𝓢 ⊢! □φ ⋏ □ψ ==> □(φ ⋏ ψ)

source

def LO.Entailment.collectMultiboxAnd' {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] {n : ℕ} {φ ψ : F} (h : 𝓢 ⊢ □^[n]φ ⋏ □^[n]ψ) :

𝓢 ⊢ □^[n](φ ⋏ ψ)

Imported declaration from the Incompleteness formalization.

Equations

LO.Entailment.collectMultiboxAnd' h = LO.Entailment.collectMultiboxAnd ⨀h

Instances For

source

theorem LO.Entailment.collectMultiboxAnd'! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] {n : ℕ} {φ ψ : F} (h : 𝓢 ⊢! □^[n]φ ⋏ □^[n]ψ) :

𝓢 ⊢! □^[n](φ ⋏ ψ)

source

def LO.Entailment.collectBoxAnd' {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] {φ ψ : F} (h : 𝓢 ⊢ □φ ⋏ □ψ) :

𝓢 ⊢ □(φ ⋏ ψ)

Imported declaration from the Incompleteness formalization.

Equations

LO.Entailment.collectBoxAnd' h = LO.Entailment.collectMultiboxAnd' h

Instances For

source

theorem LO.Entailment.collectBoxAnd'! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] {φ ψ : F} (h : 𝓢 ⊢! □φ ⋏ □ψ) :

𝓢 ⊢! □(φ ⋏ ψ)

source

theorem LO.Entailment.multiboxConj'_iff! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] {n : ℕ} {Γ : List F} :

𝓢 ⊢! □^[n]⋀Γ ↔ ∀ φ ∈ Γ, 𝓢 ⊢! □^[n]φ

source

theorem LO.Entailment.boxConj'_iff! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] {Γ : List F} :

𝓢 ⊢! □⋀Γ ↔ ∀ φ ∈ Γ, 𝓢 ⊢! □φ

source

theorem LO.Entailment.multiboxconj_of_conjmultibox! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] {n : ℕ} {Γ : List F} (d : 𝓢 ⊢! ⋀□'^[n]Γ) :

𝓢 ⊢! □^[n]⋀Γ

source

@[simp]

theorem LO.Entailment.multibox_cons_conjAux₁! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] {n : ℕ} {φ : F} {Γ : List F} :

𝓢 ⊢! ⋀□'^[n](φ :: Γ) ==> ⋀□'^[n]Γ

source

@[simp]

theorem LO.Entailment.multibox_cons_conjAux₂! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] {n : ℕ} {φ : F} {Γ : List F} :

𝓢 ⊢! ⋀□'^[n](φ :: Γ) ==> □^[n]φ

source

@[simp]

theorem LO.Entailment.multibox_cons_conj! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] {n : ℕ} {φ : F} {Γ : List F} :

𝓢 ⊢! ⋀□'^[n](φ :: Γ) ==> ⋀□'^[n]Γ ⋏ □^[n]φ

source

@[simp]

theorem LO.Entailment.collect_multibox_conj! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] {n : ℕ} {Γ : List F} :

𝓢 ⊢! ⋀□'^[n]Γ ==> □^[n]⋀Γ

source

@[simp]

theorem LO.Entailment.collect_box_conj! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] {Γ : List F} :

𝓢 ⊢! ⋀□'Γ ==> □⋀Γ

source

def LO.Entailment.collectMultiboxOr {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] {n : ℕ} {φ ψ : F} :

𝓢 ⊢ □^[n]φ ⋎ □^[n]ψ ==> □^[n](φ ⋎ ψ)

Imported declaration from the Incompleteness formalization.

Equations

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

Instances For

source

@[simp]

theorem LO.Entailment.collectMultiboxOr! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] {n : ℕ} {φ ψ : F} :

𝓢 ⊢! □^[n]φ ⋎ □^[n]ψ ==> □^[n](φ ⋎ ψ)

source

def LO.Entailment.collectBoxOr {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] {φ ψ : F} :

𝓢 ⊢ □φ ⋎ □ψ ==> □(φ ⋎ ψ)

Imported declaration from the Incompleteness formalization.

Equations

LO.Entailment.collectBoxOr = LO.Entailment.collectMultiboxOr

Instances For

source

@[simp]

theorem LO.Entailment.collectBoxOr! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] {φ ψ : F} :

𝓢 ⊢! □φ ⋎ □ψ ==> □(φ ⋎ ψ)

source

def LO.Entailment.collectMultiboxOr' {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] {n : ℕ} {φ ψ : F} (h : 𝓢 ⊢ □^[n]φ ⋎ □^[n]ψ) :

𝓢 ⊢ □^[n](φ ⋎ ψ)

Imported declaration from the Incompleteness formalization.

Equations

LO.Entailment.collectMultiboxOr' h = LO.Entailment.collectMultiboxOr ⨀h

Instances For

source

theorem LO.Entailment.collectMultiboxOr'! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] {n : ℕ} {φ ψ : F} (h : 𝓢 ⊢! □^[n]φ ⋎ □^[n]ψ) :

𝓢 ⊢! □^[n](φ ⋎ ψ)

source

def LO.Entailment.collectBoxOr' {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] {φ ψ : F} (h : 𝓢 ⊢ □φ ⋎ □ψ) :

𝓢 ⊢ □(φ ⋎ ψ)

Imported declaration from the Incompleteness formalization.

Equations

LO.Entailment.collectBoxOr' h = LO.Entailment.collectMultiboxOr' h

Instances For

source

theorem LO.Entailment.collectBoxOr'! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] {φ ψ : F} (h : 𝓢 ⊢! □φ ⋎ □ψ) :

𝓢 ⊢! □(φ ⋎ ψ)

source

def LO.Entailment.diaOrInstOf {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] {χ φ ψ : F} (h : 𝓢 ⊢ χ ==> φ ⋎ ψ) :

𝓢 ⊢ ◇χ ==> ◇(φ ⋎ ψ)

Lift an implication with a disjunctive conclusion through possibility.

Equations

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

Instances For

source

def LO.Entailment.diaOrInst₁ {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] {φ ψ : F} :

𝓢 ⊢ ◇φ ==> ◇(φ ⋎ ψ)

Imported declaration from the Incompleteness formalization.

Equations

LO.Entailment.diaOrInst₁ = LO.Entailment.diaOrInstOf LO.Entailment.or₁

Instances For

source

@[simp]

theorem LO.Entailment.dia_or_inst₁! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] {φ ψ : F} :

𝓢 ⊢! ◇φ ==> ◇(φ ⋎ ψ)

source

def LO.Entailment.diaOrInst₂ {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] {ψ φ : F} :

𝓢 ⊢ ◇ψ ==> ◇(φ ⋎ ψ)

Imported declaration from the Incompleteness formalization.

Equations

LO.Entailment.diaOrInst₂ = LO.Entailment.diaOrInstOf LO.Entailment.or₂

Instances For

source

@[simp]

theorem LO.Entailment.dia_or_inst₂! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] {ψ φ : F} :

𝓢 ⊢! ◇ψ ==> ◇(φ ⋎ ψ)

source

def LO.Entailment.collectDiaOr {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] {φ ψ : F} :

𝓢 ⊢ ◇φ ⋎ ◇ψ ==> ◇(φ ⋎ ψ)

Imported declaration from the Incompleteness formalization.

Equations

LO.Entailment.collectDiaOr = LO.Entailment.or₃'' LO.Entailment.diaOrInst₁ LO.Entailment.diaOrInst₂

Instances For

source

@[simp]

theorem LO.Entailment.collectDiaOr! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] {φ ψ : F} :

𝓢 ⊢! ◇φ ⋎ ◇ψ ==> ◇(φ ⋎ ψ)

source

def LO.Entailment.collectDiaOr' {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] {φ ψ : F} (h : 𝓢 ⊢ ◇φ ⋎ ◇ψ) :

𝓢 ⊢ ◇(φ ⋎ ψ)

Imported declaration from the Incompleteness formalization.

Equations

LO.Entailment.collectDiaOr' h = LO.Entailment.collectDiaOr ⨀h

Instances For

source

@[simp]

theorem LO.Entailment.collectDiaOr'! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] {φ ψ : F} (h : 𝓢 ⊢! ◇φ ⋎ ◇ψ) :

𝓢 ⊢! ◇(φ ⋎ ψ)

source

@[simp]

theorem LO.Entailment.distribute_multidia_and! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] {n : ℕ} {φ ψ : F} :

𝓢 ⊢! ◇^[n](φ ⋏ ψ) ==> ◇^[n]φ ⋏ ◇^[n]ψ

source

@[simp]

theorem LO.Entailment.distribute_dia_and! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] {φ ψ : F} :

𝓢 ⊢! ◇(φ ⋏ ψ) ==> ◇φ ⋏ ◇ψ

source

@[simp]

theorem LO.Entailment.iff_conjmultidia_multidiaconj! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] {n : ℕ} {Γ : List F} :

𝓢 ⊢! ◇^[n]⋀Γ ==> ⋀◇'^[n]Γ

source

theorem LO.Entailment.distribute_dia_and'! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] {φ ψ : F} (h : 𝓢 ⊢! ◇(φ ⋏ ψ)) :

𝓢 ⊢! ◇φ ⋏ ◇ψ

source

def LO.Entailment.boxdotAxiomK {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] {φ ψ : F} :

𝓢 ⊢ ⊡(φ ==> ψ) ==> ⊡φ ==> ⊡ψ

Imported declaration from the Incompleteness formalization.

Equations

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

Instances For

source

@[simp]

theorem LO.Entailment.boxdot_axiomK! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] {φ ψ : F} :

𝓢 ⊢! ⊡(φ ==> ψ) ==> ⊡φ ==> ⊡ψ

source

def LO.Entailment.boxdotAxiomT {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] {φ : F} :

𝓢 ⊢ ⊡φ ==> φ

Imported declaration from the Incompleteness formalization.

Equations

LO.Entailment.boxdotAxiomT = LO.Entailment.and₁

Instances For

source

@[simp]

theorem LO.Entailment.boxdot_axiomT! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] {φ : F} :

𝓢 ⊢! ⊡φ ==> φ

source

def LO.Entailment.boxdotNec {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] {φ : F} (d : 𝓢 ⊢ φ) :

𝓢 ⊢ ⊡φ

Imported declaration from the Incompleteness formalization.

Equations

LO.Entailment.boxdotNec d = LO.Entailment.and₃' d (LO.Entailment.nec d)

Instances For

source

theorem LO.Entailment.boxdot_nec! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] {φ : F} (d : 𝓢 ⊢! φ) :

𝓢 ⊢! ⊡φ

source

def LO.Entailment.boxdotBox {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] {φ : F} :

𝓢 ⊢ ⊡φ ==> □φ

Imported declaration from the Incompleteness formalization.

Equations

LO.Entailment.boxdotBox = LO.Entailment.and₂

Instances For

source

theorem LO.Entailment.boxdot_box! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] {φ : F} :

𝓢 ⊢! ⊡φ ==> □φ

source

def LO.Entailment.BoxBoxdotBoxDotbox {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] {φ : F} :

𝓢 ⊢ □⊡φ ==> ⊡□φ

Imported declaration from the Incompleteness formalization.

Equations

LO.Entailment.BoxBoxdotBoxDotbox = LO.Entailment.impTrans'' LO.Entailment.distributeBoxAnd (LO.Entailment.impId (□φ ⋏ □□φ))

Instances For

source

theorem LO.Entailment.boxboxdot_boxdotbox {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] {φ : F} :

𝓢 ⊢! □⊡φ ==> ⊡□φ

source

noncomputable def LO.Entailment.lemmaGrz₁ {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] {φ : F} :

𝓢 ⊢ □φ ==> □(□(φ ⋏ (□φ ==> □□φ) ==> □(φ ⋏ (□φ ==> □□φ))) ==> φ ⋏ (□φ ==> □□φ))

Imported declaration from the Incompleteness formalization.

Equations

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

Instances For

source

theorem LO.Entailment.lemmaGrz₁! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] {φ : F} :

𝓢 ⊢! □φ ==> □(□(φ ⋏ (□φ ==> □□φ) ==> □(φ ⋏ (□φ ==> □□φ))) ==> φ ⋏ (□φ ==> □□φ))

source

theorem LO.Entailment.contextual_nec! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] {Γ : List F} {φ : F} (h : Γ ⊢[𝓢]! φ) :

(□'Γ) ⊢[𝓢]! □φ

source

theorem LO.Entailment.Context.provable_iff_boxed {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] {X : Set F} {φ : F} :

(□''X) *⊢[𝓢]! φ ↔ ∃ (Δ : List F), (∀ ψ ∈ □'Δ, ψ ∈ □''X) ∧ (□'Δ) ⊢[𝓢]! φ

Documentation

LeanPool.Incompleteness.Foundation.Modal.Entailment.K

K #