noncomputable def
LO.System.Grz.lemma_axiomFour_axiomT
{S : Type u_1}
{F : Type u_2}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
[LO.System F S]
{π’ : S}
[LO.System.Grz π’]
{Ο : F}
:
Equations
- LO.System.Grz.lemma_axiomFour_axiomT = LO.System.impTrans'' LO.System.lemma_Grzβ LO.System.axiomGrz
Instances For
noncomputable def
LO.System.Grz.axiomFour
{S : Type u_1}
{F : Type u_2}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
[LO.System F S]
{π’ : S}
[LO.System.Grz π’]
{Ο : F}
:
Equations
- LO.System.Grz.axiomFour = LO.System.ppq (LO.System.impTrans'' LO.System.Grz.lemma_axiomFour_axiomT LO.System.andβ)
Instances For
noncomputable instance
LO.System.Grz.instHasAxiomFour
{S : Type u_1}
{F : Type u_2}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
[LO.System F S]
{π’ : S}
[LO.System.Grz π’]
:
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}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
[LO.System F S]
{π’ : S}
[LO.System.Grz π’]
{Ο : F}
:
Equations
- LO.System.Grz.axiomT = LO.System.impTrans'' LO.System.Grz.lemma_axiomFour_axiomT LO.System.andβ
Instances For
noncomputable instance
LO.System.Grz.instHasAxiomT
{S : Type u_1}
{F : Type u_2}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
[LO.System F S]
{π’ : S}
[LO.System.Grz π’]
:
LO.System.HasAxiomT π’
Equations
- LO.System.Grz.instHasAxiomT = { T := fun (x : F) => LO.System.Grz.axiomT }