RAP Examples - Binary Trees

```{***********************************************************************}
{* SPECIFICATION OF BINARY TREES                                       *}
{***********************************************************************}

type BTREE
basedon NAT, BOOL
sort Tree
cons empty : Tree,
mk : (Tree,Nat,Tree)Tree
func left : (Tree)Tree,
right: (Tree)Tree,
node : (Tree)Nat,
isempty : (Tree)Bool
axioms all (t1,t2 : Tree, n : Nat)
{1}  left(mk(t1,n,t2)) -> t1,
{2}  right(mk(t1,n,t2)) -> t2,
{3}  node(mk(t1,n,t2)) -> n,
{4}  isempty(empty) -> true,
{5}  isempty(mk(t1,n,t2)) -> false
endoftype
complete BTREE except left, right, node
noetherian BTREE
display BTREE empty = "<>",
mk = "<_ _ _>",
isempty = "_ = <>"

{***********************************************************************}
{* SOME EXTENSIONS OF BINARY TREES                                     *}
{***********************************************************************}

type HBTREE
basedon BTREE, NAT, BOOL
func max   : (Nat,Nat)Nat,
hight : (Tree)Nat
axioms all (t1, t2 : Tree, m, n : Nat)
{1} le(m,n) = true  =>  max(m,n) -> n,
{2} le(m,n) = false  =>  max(m,n) -> m,
{3} hight(empty) -> 0,
{4} hight(mk(t1,n,t2)) -> succ(max(hight(t1),hight(t2)))
endoftype
noetherian HBTREE

type FBTREE
basedon BTREE, NAT, BOOL
func append  : (Tree,Tree)Tree,
flatten : (Tree)Tree
axioms all (t, t1, t2 : Tree, n : Nat)
{1} append(empty,t) -> t,
{2} append(mk(t1,n,t2),t) -> mk(t1,n,append(t2,t)),
{3} flatten(empty) -> empty,
{4} flatten(mk(t1,n,t2))  -> append(mk(empty,n,flatten(t1)),flatten(t2))
endoftype
noetherian HBTREE

{***********************************************************************}
{***********************************************************************}

basedon HBTREE, BTREE, NAT, BOOL
unknown t : Tree
goals   hight(t) = 3