Go backward to C.11 Modular ArithmeticGo up to C Logic Evaluator DefinitionsGo forward to C.13 Rationals as Equivalence Classes

## C.12 Integers as Equivalence Classes

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

// just consider subset of N x N
fun Z' = set(x in nat(0, 6), y in nat(0, 6): true, tuple(x, y));

// x0-x1 = y0-y1
fun ~Z = set(x in Z', y in Z':
=(+N(.0(x), .1(y)), +N(.0(y), .1(x))), tuple(x, y));

// Z as a quotient set
fun Z = /(Z', ~Z);

// selector function
fun _(x) = such(a in x: true, a);

// equivalence class of x
fun []Z(x in Z') = [](x, ~Z);

// constants
fun Z0 = []Z(tuple(N0, N0));
fun Z1 = []Z(tuple(N1, N0));
fun Z2 = []Z(tuple(N2, N0));

// arithmetic
fun +Z(x in Z, y in Z) =
[]Z(tuple(+N(.0(_(x)), .0(_(y))), +N(.1(_(x)), .1(_(y)))));
fun -Z(x in Z) = []Z(tuple(.1(_(x)), .0(_(x))));
fun -Z(x in Z, y in Z) =
[]Z(tuple(+N(.0(_(x)), .1(_(y))), +N(.0(_(y)), .1(_(x)))));
fun *Z(x in Z, y in Z) =
[]Z(tuple(+N(*N(.0(_(x)), .0(_(y))), *N(.1(_(x)), .1(_(y)))),
+N(*N(.0(_(x)), .1(_(y))), *N(.1(_(x)), .0(_(y))))));

// order
pred <=Z(x in Z, y in Z) <=>
<=N(+N(.0(_(x)), .1(_(y))), +N(.0(_(y)), .1(_(x))));

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

Author: Wolfgang Schreiner
Last Modification: October 4, 1999