[an error occurred while processing this directive]
{***********************************************************************} {* 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 {***********************************************************************} {* SOME EXAMPLE TASKS *} {***********************************************************************} task T1 basedon HBTREE, BTREE, NAT, BOOL unknown t : Tree goals hight(t) = 3 endoftask task T2 basedon FBTREE, BTREE, NAT, BOOL unknown t : Tree goals flatten(flatten(t)) = flatten(t) endoftask[an error occurred while processing this directive] 31-Jul-2012, 14:17:22 CEST