noncomputable def LO.System.Grz.lemma_axiomFour_axiomT {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓢 : S} [System.Grz 𝓢] {φ : F} : 𝓢 ⊢ □φ ➝ φ ⋏ (□φ ➝ □□φ)

Equations

• LO.System.Grz.lemma_axiomFour_axiomT = LO.System.impTrans'' LO.System.lemma_Grz₁ LO.System.axiomGrz

noncomputable def LO.System.Grz.axiomFour {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓢 : S} [System.Grz 𝓢] {φ : F} : 𝓢 ⊢ □φ ➝ □□φ

Equations

• LO.System.Grz.axiomFour = LO.System.ppq (LO.System.impTrans'' LO.System.Grz.lemma_axiomFour_axiomT LO.System.and₂)

noncomputable instance LO.System.Grz.instHasAxiomFour {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓢 : S} [System.Grz 𝓢] : HasAxiomFour 𝓢

Equations

• LO.System.Grz.instHasAxiomFour = { Four := fun (x : F) => LO.System.Grz.axiomFour }

noncomputable def LO.System.Grz.axiomT {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓢 : S} [System.Grz 𝓢] {φ : F} : 𝓢 ⊢ □φ ➝ φ

Equations

• LO.System.Grz.axiomT = LO.System.impTrans'' LO.System.Grz.lemma_axiomFour_axiomT LO.System.and₁

noncomputable instance LO.System.Grz.instHasAxiomT {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓢 : S} [System.Grz 𝓢] : HasAxiomT 𝓢

Equations

• LO.System.Grz.instHasAxiomT = { T := fun (x : F) => LO.System.Grz.axiomT }