:-module(_,[],[]). '$applied_packages'([prelude,nonpure,condcomp,rtchecks_shallow,regtypes,assertions,fsyntax,predefres(res_steps),resdefs,resdefs/resources_decl,nativeprops,basicmodes,argnames,expander]). :-add_clause_trans(expander_tr:expand_clause/4,9910). :-prop bin_tree/1+regtype. :-prop bst/1. :-pred bst_member(E,L):(num(E),bst(L)). bin_tree(nil). bin_tree(t(L,E,R)) :- bin_tree(L), bin_tree(R), num(E). 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). 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). bst_(nil,_,_) :- !. bst_(t(L,E,R),Min,Max) :- Min=<E, E=<Max, bst_(L,Min,E), bst_(R,E,Max). bst_member(_1,_2) :- 'bst_member$pre'(_1,_2), 'bst_member$cls'(_1,_2). 'bst_member$pre'(_2,_1) :- reify_check(bst(_1),[_1],_4), reify_check(rtc_num(_2),[_2],_3), _5 is _3/\_4, _6 is _5, _7 is _6, warn_if_false(_7,'CP'). 'bst_member$cls'(E,t(_,E,_)) :- !. 'bst_member$cls'(E,t(L,X,_)) :- E<X, bst_member(E,L). 'bst_member$cls'(E,t(_,X,R)) :- E>X, bst_member(E,R).