instance LO.Modal.Entailment.KT'.instHasAxiomT {S : Type u_1} {F : Type u_2} [DecidableEq F] [BasicModalLogicalConnective F] [Entailment S F] {𝓢 : S} [Entailment.KT' 𝓢] : HasAxiomT 𝓢

Equations

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

instance LO.Modal.Entailment.KT'.instKT {S : Type u_1} {F : Type u_2} [DecidableEq F] [BasicModalLogicalConnective F] [Entailment S F] {𝓢 : S} [Entailment.KT' 𝓢] : Entailment.KT 𝓢

Equations

• LO.Modal.Entailment.KT'.instKT = { toK := inst✝.toK, toHasAxiomT := LO.Modal.Entailment.KT'.instHasAxiomT }

instance LO.Modal.Entailment.KT'.instKP {S : Type u_1} {F : Type u_2} [DecidableEq F] [BasicModalLogicalConnective F] [Entailment S F] {𝓢 : S} [Entailment.KT' 𝓢] : Entailment.KP 𝓢

Equations

• LO.Modal.Entailment.KT'.instKP = { toK := inst✝.toK, toHasAxiomP := LO.Modal.Entailment.instHasAxiomP }

instance LO.Modal.Entailment.KT'.instKD {S : Type u_1} {F : Type u_2} [DecidableEq F] [BasicModalLogicalConnective F] [Entailment S F] {𝓢 : S} [Entailment.KT' 𝓢] : Entailment.KD 𝓢

Equations

• LO.Modal.Entailment.KT'.instKD = { toK := inst✝.toK, toHasAxiomD := LO.Modal.Entailment.KP.instHasAxiomD }

instance LO.Modal.Entailment.instET {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment S F] {𝓢 : S} [Entailment.KT 𝓢] : Entailment.ET 𝓢

Equations

• LO.Modal.Entailment.instET = { toE := LO.Modal.Entailment.instE, toHasAxiomT := inst✝.toHasAxiomT }

instance LO.Modal.Entailment.instKD {S : Type u_1} {F : Type u_2} [DecidableEq F] [BasicModalLogicalConnective F] [Entailment S F] {𝓢 : S} [Entailment.KT 𝓢] : Entailment.KD 𝓢

Equations

• LO.Modal.Entailment.instKD = { toK := inst✝.toK, toHasAxiomD := LO.Modal.Entailment.ET.instHasAxiomD }

@[simp]

theorem LO.Modal.Entailment.reduce_box_in_CAnt! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment S F] {𝓢 : S} [Entailment.KT 𝓢] {i n : ℕ} {φ : F} : 𝓢 ⊢ □^[i + n]φ ➝ □^[i]φ