|
 |
 |
 |
 |
 |
 |
 |
 |
 |
 |
 |
 |
 |
 |
 |
 |
 |
ä |
Axioms
|
|
|
|
ä |
Add(Create,
E) = Build(Create, E, Create)
|
|
|
|
ä |
Add(B,
E) =
|
|
if E < Data(B) then Add(Left(B),E)
|
|
else Add(Right(B),E)
|
|
|
|
ä |
Left(Create)
= Create
|
|
|
|
ä |
Right(Create)
= Create
|
|
|
|
ä |
Data(Create)
= Undefined
|
|
|
|
ä |
Left(Build(L,D,R))
= L
|
|
|
|
ä |
Right(Build(L,D,R))
= R
|
|
|
|
ä |
Data(Build(L,D,R)
= D
|
|
|
|
ä |
Is_empty(Create)
= true
|
|
|
|
ä |
Is_empty(Build(L,D,R))
= false
|
|
|
|
ä |
Contains(Create,E)
= false
|
|
|
|
ä |
Contains(Build(L,D,R),E)
=
|
|
if E = D then true
|
|
else if E < D then Contains(L,E)
|
|
else Contains(R,E)
|
|
|
|