:- module(_,[],[rtchecks_shallow,
	regtypes, assertions,fsyntax, predefres(res_steps)]).

:- regtype bin_tree/1.
bin_tree(nil).
bin_tree(t(L,E,R)):-
	bin_tree(L),
	bin_tree(R),
	num(E).

:- prop bst/1.
bst(nil).
bst(t(nil,_E,nil)):-!.
bst(t(nil,E,R)):-!,
	max_(R,Max),
	bst_(R,E,Max).
bst(t(L,E,nil)):-!,
	min_(L,Min),
	bst_(L,Min,E).
bst(t(L,E,R)):-
	min_(L,Min),
	max_(R,Max),
	bst_(L,Min,E),
	bst_(R,E,Max).


bst_(nil,_1,_2) :- !.
bst_(t(_3,_4,_5),_1,_2) :-
        _1=<_4,
        _4=<_2,
        bst_(_3,_1,_4),
        bst_(_5,_4,_2).

min_(nil,_):-fail,!.
min_(t(nil,E,_),E):-!.
min_(t(L,_E,_R),Min):-
	min_(L,Min).

max_(nil,_):-fail,!.
max_(t(_,E,nil),E):-!.
max_(t(_L,_E,R),Max):-
	max_(R,Max).

:- entry bst_member/2:num*bin_tree.
:- pred bst_member(E,L):(num(E),bst(L)).
bst_member(E,t(_,E,_)):-!.
bst_member(E,t(L,X,_)):-
	E < X,
	bst_member(E,L).
bst_member(E,t(_,X,R)):-
	E > X,
	bst_member(E,R).