** 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 WF = ... : {s|Type}(Rel s s)->Prop TWF = ... : {s|Type}(Rel s s)->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] (preorder P /\ {Q:Rel s s}(ClosedR Q S)->SubRel Q P) prekernelRelL = ... : {s|Type}{S:Rel s s}[P=coimpliesRel S S] (preorder P /\ {Q:Rel s s}(ClosedL Q S)->SubRel Q P) kernelRel = ... : {s|Type}{S:Rel s s}(sym S)->[kerS=symkernelRel S] (equiv kerS /\ {Q:Rel s s}(ClosedL Q S)->(ClosedR Q S)-> SubRel Q kerS)