def LO.System.Triv.axiomGrz {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [DecidableEq F] [LO.System F S] {𝓢 : S} [LO.System.Triv 𝓢] {φ : F} : 𝓢 ⊢ □(□(φ ➝ □φ) ➝ φ) ➝ φ

Equations

• LO.System.Triv.axiomGrz = LO.System.impTrans'' LO.System.axiomT (LO.System.p_pq_q⨀LO.System.nec LO.System.axiomTc)

instance LO.System.Triv.instHasAxiomGrz {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [DecidableEq F] [LO.System F S] {𝓢 : S} [LO.System.Triv 𝓢] : LO.System.HasAxiomGrz 𝓢

Equations

• LO.System.Triv.instHasAxiomGrz = { Grz := fun (x : F) => LO.System.Triv.axiomGrz }