SetByBSTFold

This structure implements folding of sets.

Signature of SetByBSTFold

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

SIGNATURE SetByBSTFold[data,< :data ** data -> bool]

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

-- Version 1.1

IMPORT  SetByBST[data, <] ONLY set

Parameter

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

SORT data
FUN < : data**data->bool

The function f should be left-commutative: x o (y o z) = y o (x o z), since reduction order is implementation dependent.

Informally, + / {e0, e1, ..., en == e0 + (e1 + ( ... + en) ... )}. The function is undefined for empty sets.

FUN / : (data ** data -> data) ** set -> data

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