Go backward to C.13 Rationals as Equivalence ClassesGo up to C Logic Evaluator Definitions

## C.14 Order Relations

```// ----------------------------------------------------------------
// \$Id: evaluator.tex,v 1.7 1999/09/29 12:28:26 schreine Exp \$
// order relations
//
// (c) 1999, Wolfgang Schreiner, see file COPYRIGHT
// http://www.risc.uni-linz.ac.at/software/formal
// ----------------------------------------------------------------

// R is antisymmetric on S
pred isAntiSymmetric(R: Relation, S) <=>
forall(x in S, y in S:
implies(and(in(tuple(x, y), S), in(tuple(y, x), S)), =(x, y)));

// R is partial order on S
pred isPartialOrder(R: Relation, S) <=>
and(isRelation(R, S, S),
isReflexive(R, S),
isAntiSymmetric(R, S),
isTransitive(R, S));

// R is irreflexive on S
pred isIrreflexive(R: Relation, S) <=>
forall(x in S: not(in(tuple(x, x), R)));

// R is partial order on S
pred isQuasiOrder(R: Relation, S) <=>
and(isRelation(R, S, S),
isIrreflexive(R, S),
isAntiSymmetric(R, S),
isTransitive(R, S));

// x and y are incomparable with respect to R
pred areIncomparable(x, y, R) <=>
and(not(in(tuple(x, y), R)), not(in(tuple(y, x), R)));

// R is total order on S
pred isTotalOrder(R: Relation, S) <=>
and(isRelation(R, S, S),
not(exists(x in S, y in S: areIncomparable(x, y, R))));

// x is least/greatest element in S with respect to R
pred isLeast(x, S, R) <=>
and(in(x, S), forall(y in S: in(tuple(x, y), R)));
pred isGreatest(x, S, R) <=>
and(in(x, S), forall(y in S: in(tuple(y, x), R)));

// x is minimal/maximal element of S with respect to R
pred isMinimal(x, S, R) <=>
and(in(x, S), forall(y in S:
implies(in(tuple(y, x), R), =(y, x))));
pred isMaximal(x, S, R) <=>
and(in(x, S), forall(y in S:
implies(in(tuple(x, y), R), =(x, y))));

// x is lower/upper bound of S with respect to R
pred isLowerBound(x, S, R) <=>
forall(y in S: in(tuple(x, y), R));
pred isUpperBound(x, S, R) <=>
forall(y in S: in(tuple(y, x), R));

// x is infimum/supremum of S with respect to R
pred isInfimum(x, S, R) <=>
and(isLowerBound(x, S, R),
forall(y in domain(R):
implies(isLowerBound(y, S, R), in(tuple(y, x), R))));
pred isSupremum(x, S, R) <=>
and(isUpperBound(x, S, R),
forall(y in range(R):
implies(isUpperBound(y, S, R), in(tuple(x, y), R))));

// ----------------------------------------------------------------
// \$Id: evaluator.tex,v 1.7 1999/09/29 12:28:26 schreine Exp \$
// ----------------------------------------------------------------
```

Author: Wolfgang Schreiner
Last Modification: October 4, 1999