:- 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).