Go backward to C.9 Real FunctionsGo up to C Logic Evaluator DefinitionsGo forward to C.11 Modular Arithmetic

## C.10 Equivalence Relations

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

// R is reflexive on S
pred isReflexive(R: Relation, S) <=>
forall(x in S: in(tuple(x, x), R));

// R is symmetric on S
pred isSymmetric(R: Relation, S) <=>
forall(t in R: in(tuple(.1(t), .0(t)), R));

// R is transitive on S
pred isTransitive(R: Relation, S) <=>
forall(s in R, t in R:
implies(=(.1(s), .0(t)), in(tuple(.0(s), .1(t)), R)));

// R is equivalence relation on S
pred isEquivalence(R: Relation, S) <=>
and(isRelation(R, S, S), isReflexive(R, S),
isSymmetric(R, S), isTransitive(R, S));

// class [x]_R
fun [](x, R: Relation) =
set(y in range(R): in(tuple(x, y), R), y);

// quotient set S/R
fun /(S, R: Relation) = set(x in S: true, [](x, R));

// D is partition on S
pred isPartition(D, S) <=>
and(forall(x in D: not(=(x, {}))),
forall(x in D, y in D: or(=(x, y), =(**(x, y), {}))),
=(++(D), S));

// induced relation ~D
fun ~(D) =
++(set(d in D: true, set(x in d, y in d: true, tuple(x, y))));

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

Author: Wolfgang Schreiner
Last Modification: October 4, 1999