** Module lib_rel Imports lib_nat
Pred = ... : (Type)->Type
Rel = ... : (Type)->(Type)->Type
preserves = ... : {s|Type}{t|Type}(s->t)->(Rel s s)->(Rel t t)->Prop
per = ... : {s|Type}(Rel s s)->Prop
equiv = ... : {s|Type}(Rel s s)->Prop
preorder = ... : {s|Type}(Rel s s)->Prop
PreorderEq = ... : {s|Type}{R:Rel s s}(preorder R)->Rel s s
SubPred = ... : {s|Type}(Pred s)->(Pred s)->Prop
reflSubPred = ... : {s|Type}refl (SubPred|s)
transSubPred = ... : {s|Type}trans (SubPred|s)
EqPred = ... : {s|Type}Rel (Pred s) (Pred s)
SubRel = ... : {s|Type}{t|Type}(Rel s t)->(Rel s t)->Prop
reflSubRel = ... : {s|Type}{t|Type}refl (SubRel|s|t)
transSubRel = ... : {s|Type}{t|Type}trans (SubRel|s|t)
EqRel = ... : {s|Type}{t|Type}Rel (Rel s t) (Rel s t)
andPred = ... : {s|Type}(Pred s)->(Pred s)->Pred s
orPred = ... : {s|Type}(Pred s)->(Pred s)->Pred s
impliesPred = ... : {s|Type}(Pred s)->(Pred s)->Pred s
notPred = ... : {s|Type}(Pred s)->Pred s
* andPredI = ... :
{s|Type}{E,F,G|Pred s}(SubPred E F)->(SubPred E G)->
SubPred E (andPred F G)
* andPredE1 = ... :
{s|Type}{E,F,G|Pred s}(SubPred E (andPred F G))->SubPred E F
* andPredE2 = ... :
{s|Type}{E,F,G|Pred s}(SubPred E (andPred F G))->SubPred E G
* orPredE = ... :
{s|Type}{E,F,G|Pred s}(SubPred F E)->(SubPred G E)->
SubPred (orPred F G) E
* orPredI1 = ... :
{s|Type}{E,F,G|Pred s}(SubPred E F)->SubPred E (orPred F G)
* orPredI2 = ... :
{s|Type}{E,F,G|Pred s}(SubPred E G)->SubPred E (orPred F G)
* impliesPredI = ... :
{s|Type}{E,F,G|Pred s}(SubPred (andPred F G) E)->
SubPred F (impliesPred G E)
* impliesPredE = ... :
{s|Type}{E,F,G|Pred s}(SubPred F (impliesPred G E))->
SubPred (andPred F G) E
existsf = ... : {s|Type}{t|Type}(t->s)->(Pred t)->Pred s
starf = ... : {s|Type}{t|Type}(t->s)->(Pred s)->Pred t
forallf = ... : {s|Type}{t|Type}(t->s)->(Pred t)->Pred s
* existsfE = ... :
{s|Type}{t|Type}{F|Pred s}{H|Pred t}{f|t->s}
(SubPred (existsf f H) F)->SubPred H (starf f F)
* existsfI = ... :
{s|Type}{t|Type}{F|Pred s}{H|Pred t}{f|t->s}
(SubPred H (starf f F))->SubPred (existsf f H) F
* forallfE = ... :
{s|Type}{t|Type}{F|Pred s}{H|Pred t}{f|t->s}
(SubPred F (forallf f H))->SubPred (starf f F) H
* forallfI = ... :
{s|Type}{t|Type}{F|Pred s}{H|Pred t}{f|t->s}
(SubPred (starf f F) H)->SubPred F (forallf f H)
op = ... : {s|Type}{t|Type}(Rel s t)->Rel t s
notRel = ... : {s|Type}{t|Type}(Rel s t)->Rel s t
andRel = ... : {s|Type}{t|Type}(Rel s t)->(Rel s t)->Rel s t
orRel = ... : {s|Type}{t|Type}(Rel s t)->(Rel s t)->Rel s t
composeRel = ... :
{s|Type}{t|Type}{u|Type}(Rel s t)->(Rel t u)->Rel s u
impliesRel = ... :
{s|Type}{t|Type}{u|Type}(Rel s t)->(Rel s u)->Rel t u
coimpliesRel = ... :
{s|Type}{t|Type}{u|Type}(Rel t u)->(Rel s u)->Rel s t
* andRelI = ... :
{s|Type}{t|Type}{P,Q,R|Rel s t}(SubRel R P)->(SubRel R Q)->
SubRel R (andRel P Q)
* andRelE1 = ... :
{s|Type}{t|Type}{P,Q,R|Rel s t}(SubRel R (andRel P Q))->SubRel R P
* andRelE2 = ... :
{s|Type}{t|Type}{P,Q,R|Rel s t}(SubRel R (andRel P Q))->SubRel R Q
* orRelE = ... :
{s|Type}{t|Type}{P,Q,R|Rel s t}(SubRel P R)->(SubRel Q R)->
SubRel (orRel P Q) R
* orRelI1 = ... :
{s|Type}{t|Type}{P,Q,R|Rel s t}(SubRel R P)->SubRel R (orRel P Q)
* orRelI2 = ... :
{s|Type}{t|Type}{P,Q,R|Rel s t}(SubRel R Q)->SubRel R (orRel P Q)
* impliesRelI = ... :
{s|Type}{t|Type}{u|Type}{R|Rel s t}{S|Rel t u}{T|Rel s u}
(SubRel (composeRel R S) T)->SubRel S (impliesRel R T)
* impliesRelE = ... :
{s|Type}{t|Type}{u|Type}{R|Rel s t}{S|Rel t u}{T|Rel s u}
(SubRel S (impliesRel R T))->SubRel (composeRel R S) T
* coimpliesRelI = ... :
{s|Type}{t|Type}{u|Type}{R|Rel s t}{S|Rel t u}{T|Rel s u}
(SubRel (composeRel R S) T)->SubRel R (coimpliesRel S T)
* coimpliesRelE = ... :
{s|Type}{t|Type}{u|Type}{R|Rel s t}{S|Rel t u}{T|Rel s u}
(SubRel R (coimpliesRel S T))->SubRel (composeRel R S) T
existsgh = ... :
{s|Type}{t|Type}{u|Type}{v|Type}(u->v->s)->(u->v->t)->(Rel u v)->
Rel s t
stargh = ... :
{s|Type}{t|Type}{u|Type}{v|Type}(u->v->s)->(u->v->t)->(Rel s t)->
Rel u v
forallgh = ... :
{s|Type}{t|Type}{u|Type}{v|Type}(u->v->s)->(u->v->t)->(Rel u v)->
Rel s t
* existsghE = ... :
{s|Type}{t|Type}{u|Type}{v|Type}{P|Rel s t}{U|Rel u v}{g|u->v->s}
{h|u->v->t}(SubRel (existsgh g h U) P)->SubRel U (stargh g h P)
* existsghI = ... :
{s|Type}{t|Type}{u|Type}{v|Type}{P|Rel s t}{U|Rel u v}{g|u->v->s}
{h|u->v->t}(SubRel U (stargh g h P))->SubRel (existsgh g h U) P
* forallghE = ... :
{s|Type}{t|Type}{u|Type}{v|Type}{P|Rel s t}{U|Rel u v}{g|u->v->s}
{h|u->v->t}(SubRel P (forallgh g h U))->SubRel (stargh g h P) U
* forallghI = ... :
{s|Type}{t|Type}{u|Type}{v|Type}{P|Rel s t}{U|Rel u v}{g|u->v->s}
{h|u->v->t}(SubRel (stargh g h P) U)->SubRel P (forallgh g h U)
KPred = ... : {s|Type}Prop->Pred s
KRelL = ... : {s|Type}{t|Type}(Pred s)->Rel s t
KRelR = ... : {s|Type}{t|Type}(Pred t)->Rel s t
leftKanPred = ... : {s|Type}{t|Type}(Rel s t)->(Pred s)->Pred t
rightKanPred = ... : {s|Type}{t|Type}(Rel s t)->(Pred s)->Pred t
* notPredIE = ... :
{s|Type}{E,F|Pred s}(SubPred E F)->SubPred (notPred F) (notPred E)
* notRelIE = ... :
{s|Type}{t|Type}{P,Q|Rel s t}(SubRel P Q)->
SubRel (notRel Q) (notRel P)
univPred = ... : {s|Type}Pred s
univRel = ... : {s|Type}{t|Type}Rel s t
emptyPred = ... : {s|Type}Pred s
emptyRel = ... : {s|Type}{t|Type}Rel s t
* univPredI = ... : {s|Type}{F|Pred s}SubPred F (univPred|s)
* emptyPredI = ... : {s|Type}{F|Pred s}SubPred (emptyPred|s) F
* univRelI = ... : {s|Type}{t|Type}{R|Rel s t}SubRel R (univRel|s|t)
* emptyRelI = ... : {s|Type}{t|Type}{R|Rel s t}SubRel (emptyRel|s|t) R
* existfunit = ... :
{s|Type}{t|Type}{H|Pred t}{f|t->s}SubPred H (starf f (existsf f H))
* existfcounit = ... :
{s|Type}{t|Type}{F|Pred s}{f|t->s}SubPred (existsf f (starf f F)) F
* forallfunit = ... :
{s|Type}{t|Type}{F|Pred s}{f|t->s}SubPred F (forallf f (starf f F))
* forallfcounit = ... :
{s|Type}{t|Type}{H|Pred t}{f|t->s}SubPred (starf f (forallf f H)) H
* existghunit = ... :
{s|Type}{t|Type}{u|Type}{v|Type}{U|Rel u v}{g|u->v->s}{h|u->v->t}
SubRel U (stargh g h (existsgh g h U))
* existghcounit = ... :
{s|Type}{t|Type}{u|Type}{v|Type}{P|Rel s t}{g|u->v->s}{h|u->v->t}
SubRel (existsgh g h (stargh g h P)) P
* forallghunit = ... :
{s|Type}{t|Type}{u|Type}{v|Type}{P|Rel s t}{g|u->v->s}{h|u->v->t}
SubRel P (forallgh g h (stargh g h P))
* forallghcounit = ... :
{s|Type}{t|Type}{u|Type}{v|Type}{U|Rel u v}{g|u->v->s}{h|u->v->t}
SubRel (stargh g h (forallgh g h U)) U
monotonePred = ... : {s|Type}{t|Type}((Pred s)->Pred t)->Prop
monotoneRel = ... :
{s|Type}{t|Type}{u|Type}{v|Type}((Rel s t)->Rel u v)->Prop
* opMono = ... :
{s|Type}{t|Type}{P,Q|Rel s t}(SubRel P Q)->SubRel (op P) (op Q)
* opInvol = ... : {s|Type}{t|Type}{P|Rel s t}SubRel P (op (op P))
* composeRelMonoL = ... :
{s|Type}{t|Type}{u|Type}{P|Rel s t}
monotoneRel|t|u|s|u (composeRel P)
composeRelR = ... :
{s|Type}{t|Type}{u|Type}(Rel t u)->(Rel s t)->Rel s u
* composeRelMonoR = ... :
{s|Type}{t|Type}{u|Type}{Q|Rel t u}
monotoneRel|s|t|s|u (composeRelR Q)
* composeRelEqL1 = ... :
{s|Type}{t|Type}{P|Rel s t}SubRel (composeRel (Eq|s) P) P
* composeRelEqL2 = ... :
{s|Type}{t|Type}{P|Rel s t}SubRel P (composeRel (Eq|s) P)
* composeRelEqR1 = ... :
{s|Type}{t|Type}{P|Rel s t}SubRel (composeRel P (Eq|t)) P
* composeRelEqR2 = ... :
{s|Type}{t|Type}{P|Rel s t}SubRel P (composeRel P (Eq|t))
* composeRelAssoc1 = ... :
{s|Type}{t|Type}{u|Type}{v|Type}{P|Rel s t}{Q|Rel t u}{R|Rel u v}
SubRel (composeRel (composeRel P Q) R)
(composeRel P (composeRel Q R))
* composeRelAssoc2 = ... :
{s|Type}{t|Type}{u|Type}{v|Type}{P|Rel s t}{Q|Rel t u}{R|Rel u v}
SubRel (composeRel P (composeRel Q R))
(composeRel (composeRel P Q) R)
* opcompose1 = ... :
{s|Type}{t|Type}{u|Type}{P|Rel s t}{Q|Rel t u}
SubRel (composeRel (op Q) (op P)) (op (composeRel P Q))
* opcompose2 = ... :
{s|Type}{t|Type}{u|Type}{P|Rel s t}{Q|Rel t u}
SubRel (op (composeRel P Q)) (composeRel (op Q) (op P))
ClosedL = ... : {s|Type}{t|Type}(Rel s s)->(Rel s t)->Prop
ClosedR = ... : {s|Type}{t|Type}(Rel t t)->(Rel s t)->Prop
symkernelRel = ... : {s|Type}(Rel s s)->Rel s s
* prekernelRelR = ... :
{s|Type}{S:Rel s s}[P=impliesRel S S]
and (preorder P) ({Q:Rel s s}(ClosedR Q S)->SubRel Q P)
* prekernelRelL = ... :
{s|Type}{S:Rel s s}[P=coimpliesRel S S]
and (preorder P) ({Q:Rel s s}(ClosedL Q S)->SubRel Q P)
* kernelRel = ... :
{s|Type}{S:Rel s s}(sym S)->[kerS=symkernelRel S]
and (equiv kerS)
({Q:Rel s s}(ClosedL Q S)->(ClosedR Q S)->SubRel Q kerS)