Go backward to C.8 More on FunctionsGo up to C Logic Evaluator DefinitionsGo forward to C.10 Equivalence Relations

## C.9 Real Functions

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

// is B upper/lower bound of s in first n members of sequence s?
pred isUpperBound(B, s, n) <=>
forall(i in nat(0, n): <=R(apply(s, i), B));
pred isLowerBound(B, s, n) <=>
forall(i in nat(0, n): <=R(B, apply(s, i)));

// supremum/infimum of s considering only the first n members
fun sup(s, n) =
such(U in range(s):
and(isUpperBound(U, s, n),
forall(U' in range(s):
implies(isUpperBound(U', s, n), <=R(U, U')))), U);
fun inf(s, n) =
such(L in range(s):
and(isLowerBound(L, s, n),
forall(L' in range(s):
implies(isLowerBound(L', s, n), <=R(L', L)))), L);

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

Author: Wolfgang Schreiner
Last Modification: October 4, 1999