lem

Lem is a tool for lightweight executable mathematics
Module Lem_relation
type (!'a, !'b) rel_pred = 'a -> 'b -> bool
type ('a, 'b) rel_set = ('a * 'b) Pset.set
type ('a, 'b) rel = ( 'a, 'b ) rel_set
val relEq : 'a -> 'b -> 'c Pset.set -> 'c Pset.set -> bool
val relToPred : 'c -> 'd -> 'e -> 'f -> ('a * 'b) Pset.set -> 'a -> 'b -> bool
val relFromPred : 'a Lem_basic_classes.setType_class -> 'b Lem_basic_classes.setType_class -> 'c -> 'd -> 'a Pset.set -> 'b Pset.set -> ( 'a -> 'b -> bool ) -> ('a * 'b) Pset.set
val relComp : 'a Lem_basic_classes.setType_class -> 'b -> 'c Lem_basic_classes.setType_class -> 'd -> 'e Lem_basic_classes.eq_class -> ('a * 'e) Pset.set -> ('e * 'c) Pset.set -> ('a * 'c) Pset.set
val relRestrict : 'a Lem_basic_classes.setType_class -> 'b -> ('a * 'a) Pset.set -> 'a Pset.set -> ('a * 'a) Pset.set
val relConverse : 'a Lem_basic_classes.setType_class -> 'b Lem_basic_classes.setType_class -> ('a * 'b) Pset.set -> ('b * 'a) Pset.set
val relDomain : 'a Lem_basic_classes.setType_class -> 'b -> ('a * 'c) Pset.set -> 'a Pset.set
val relRange : 'a -> 'b Lem_basic_classes.setType_class -> ('c * 'b) Pset.set -> 'b Pset.set
val relOver : 'a Lem_basic_classes.setType_class -> ('a * 'a) Pset.set -> 'a Pset.set -> bool
val relApply : 'a -> 'b Lem_basic_classes.setType_class -> 'c -> ('d * 'b) Pset.set -> 'd Pset.set -> 'b Pset.set
val isReflexiveOn : 'a -> 'b -> ('c * 'c) Pset.set -> 'c Pset.set -> bool
val isIrreflexiveOn : 'a -> 'b -> ('c * 'c) Pset.set -> 'c Pset.set -> bool
val isIrreflexive : 'a -> 'b Lem_basic_classes.eq_class -> ('b * 'b) Pset.set -> bool
val isSymmetricOn : 'a -> 'b -> ('c * 'c) Pset.set -> 'c Pset.set -> bool
val isSymmetric : 'a -> 'b -> ('c * 'c) Pset.set -> bool
val isAntisymmetricOn : 'a -> 'b Lem_basic_classes.eq_class -> ('b * 'b) Pset.set -> 'b Pset.set -> bool
val isAntisymmetric : 'a -> 'b Lem_basic_classes.eq_class -> ('b * 'b) Pset.set -> bool
val isTransitiveOn : 'a -> 'b -> ('c * 'c) Pset.set -> 'c Pset.set -> bool
val isTransitive : 'a Lem_basic_classes.setType_class -> 'b -> ('a * 'a) Pset.set -> bool
val isTotalOn : 'a -> 'b -> ('c * 'c) Pset.set -> 'c Pset.set -> bool
val isTrichotomousOn : 'a -> 'b Lem_basic_classes.eq_class -> ('b * 'b) Pset.set -> 'b Pset.set -> bool
val isSingleValued : 'a Lem_basic_classes.setType_class -> 'b Lem_basic_classes.setType_class -> 'c -> 'b Lem_basic_classes.eq_class -> ('a * 'b) Pset.set -> bool
val isEquivalenceOn : 'a -> 'b -> ('c * 'c) Pset.set -> 'c Pset.set -> bool
val isPreorderOn : 'a -> 'b -> ('c * 'c) Pset.set -> 'c Pset.set -> bool
val isPartialOrderOn : 'a -> 'b Lem_basic_classes.eq_class -> ('b * 'b) Pset.set -> 'b Pset.set -> bool
val isStrictPartialOrderOn : 'a -> 'b -> ('c * 'c) Pset.set -> 'c Pset.set -> bool
val isStrictPartialOrder : 'a Lem_basic_classes.setType_class -> 'a Lem_basic_classes.eq_class -> ('a * 'a) Pset.set -> bool
val isTotalOrderOn : 'a -> 'b Lem_basic_classes.eq_class -> ('b * 'b) Pset.set -> 'b Pset.set -> bool
val isStrictTotalOrderOn : 'a -> 'b Lem_basic_classes.eq_class -> ('b * 'b) Pset.set -> 'b Pset.set -> bool
val transitiveClosureAdd : 'a Lem_basic_classes.setType_class -> 'b -> 'a -> 'a -> ('a * 'a) Pset.set -> ('a * 'a) Pset.set
val reflexiveTransitiveClosureOn : 'a Lem_basic_classes.setType_class -> 'a Lem_basic_classes.eq_class -> ('a * 'a) Pset.set -> 'a Pset.set -> ('a * 'a) Pset.set
val withoutTransitiveEdges : 'a Lem_basic_classes.setType_class -> 'a Lem_basic_classes.eq_class -> ('a * 'a) Pset.set -> ('a * 'a) Pset.set