IndexingOfTrees

This structure contains all functions for computing indices of trees and which do not depend on the particular data type stored in the nodes of the tree.

Signature of IndexingOfTrees

List of Import References :
See BOOL
See DENOTATION
See Nat

SIGNATURE IndexingOfTrees

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

IMPORT Nat ONLY nat

Handling Indices

root is the index of the root, left and right produce the index of the left and right child respectively.

FUN root: nat
FUN up: nat -> nat
FUN left: nat -> nat
FUN right: nat -> nat

These functions check, whether the index points to the root, to a location in the left or a location in the subtree.

FUN root? : nat -> bool
FUN left? : nat -> bool
FUN right? : nat -> bool

These functions adjust the index, so that it points to the same location in the subtree, as the original index did, i.e. t!i is equal to left(t)!unleft(i). The functions are undefined, if the index does not point into the left (right) subtree).

FUN unleft: nat -> nat
FUN unright: nat -> nat

next node: Tree,
prev node: Subsystem Binary Trees,
up to node: Subsystem Binary Trees