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