Abstrakter Datentyp "orientierter, gerichteter, knotenbewerteter binärer Baum":

Bem: alle Trägermengen enthalten das Fehlerelement #

Trägermengen	Intuition (Modell)
A	Menge von Werten
BA	Menge der binären Bäume mit Knotenwerten aus A
P = {L,R}*	Menge der Pfade über {links, rechts}
B = {true, false}	Menge der Wahrheitswerte
Funktionen:	intuitive Erklärung
e	Konstante "leerer Pfad"
L• : P -> P	Multiplikation mit L von links
R• : P -> P	Multiplikation mit R von links
E	Konstante "leerer Baum"
con: BAxAxBA -> BA	Der Baum con(B1,a,B2) hat eine Wurzel mit Wert a, an der links der Baum B1 und rechts der Baum B2 hängt.
sel: BAxP-> A	sel(B,p) liefert den Wert der an dem von der Wurzel von B aus durch p erreichten Knoten anliegt.
ins: BAxPxA -> BA	ins(B,p,a) liefert den Baum der aus B entsteht, wenn der Wert des durch p erreichten Knotens auf a gesetzt wird.
app: BAxPxA -> BA	app(B,pL,a) liefert den Baum, den man erhält, wenn man an das durch p erreichte Blatt einen linken Sohn mit dem Wert a hängt. Erreicht man durch p kein Blatt, so ergibt es einen Fehler.
cut: BAxP -> BA	cut(B,p) ist der Baum, der aus B entsteht, wenn man aus B den durch p erreichten Knoten samt seiner Nachfolger entfernt.
istBlatt: BAxP -> B	istBlatt(B,p) = true gdw. durch p in B ein Blatt erreicht wird

Axiome:

sel(E,p) = #

sel( con(B,a,C), e ) = a

sel( con(B,a,C), Lp ) = sel(B,p)

sel( con(B,a,C), Rp ) = sel(C,p)

ins(E,p,b) = #

ins( con(B,a,C), e , b ) = con(B,b,C)

ins( con(B,a,C), Lp , b ) = con( ins(B,p,b) , a , C )

ins( con(B,a,C), Rp , b ) = con(B , a , ins(C,p) , b )

app(E,e,b) = con(E,b,E)

app(E,p,b) = # <= p /=e

app(con(B,a,C), e , b ) = #

app(con(B,a,C), Lp , b ) = con( app(B,p,b), a , C)

app(con(B,a,C), Rp , b ) = con(B, a , app(C,p,b) )

cut(E,p) = #

cut( con(B,a,C) , e ) = E

cut( con(B,a,C) , Lp ) = con( cut(B,p) , a , C )

cut( con(B,a,C) , Rp ) = con( B , a , cut(C,p) )

istBlatt(E,p) = #

istBlatt( con(E,a,E) , e ) = true

istBlatt( con(B,a,C) , e ) = false <= B /=E or C /= E

istBlatt( con(B,a,C) , Lp ) = istBlatt(B,p)

istBlatt( con(B,a,C) , Rp ) = istBlatt(C,p)