SetByBSTReduce

This structure provides reductions on sets.

Signature of SetByBSTReduce

List of Import References :
See BOOL
See BSTree
See DENOTATION
See Nat
See Option
See Pair
See Seq
See SetByBST
See Tree

SIGNATURE SetByBSTReduce [from,<,to]

$Date: 2010-09-30 18:24:17 +0200 (Do, 30. Sep 2010) $ ($Revision: 616 $)

IMPORT SetByBST[from,<] ONLY set

Parameter

from is the element type, < is a total strict order: the formula ALL x y. ~(x < y) AND ~(y < x) => x === y must hold. to is the result type of the reduction.

SORT from to

FUN < : from ** from -> bool

Reducing

(o, e)/ s reduces s by o with value e as initial 2nd argument. The function f should be left-commutative: x o (y o z) = y o (x o z), since reduction order is implementation dependent.

Informally, (o / e)({a,b,...,y,z) == a o (b o (...(y o (z o e))...))}.

FUN / : (from ** to -> to) ** to ** set[from,<] -> to

next node: SetByBSTMap,
prev node: SetByBSTMapEnv,
up to node: Subsystem Sets By Binary Search Trees