:-module(_,[bsts/2],[]).
'$applied_packages'([prelude,nonpure,condcomp,regtypes,assertions,rtchecks_shallow,fsyntax,predefres(res_steps),resdefs,resdefs/resources_decl,nativeprops,basicmodes,argnames,expander]).
:-add_clause_trans(expander_tr:expand_clause/4,9910).
:-prop bst/1.
:-prop min_/2.
:-prop max_/2.
:-prop bst_/3.
:-entry bsts(E,L):(num(E),bst(L)).
:-check calls bsts(E,L):(num(E),bst(L)).
:-true pred bsts(E,L):(num(E),term(L))=>(num(E),rt2(L)).
:-true pred bsts(E,L):(mshare([[L]]),ground([E]))=>(mshare([[L]]),ground([E])).
:-check calls bsts_i(E,L):(num(E),bst(L)).
:-true pred bsts_i(E,L):(num(E),term(L))=>(num(E),rt2(L)).
:-true pred bsts_i(E,L):(mshare([[L]]),ground([E]))=>(mshare([[L]]),ground([E])).
:-prop bst(_A).
:-prop min_(_A,_B).
:-prop max_(_A,_B).
:-prop bst_(_A,_B,_C).
:-prop rt2/1+regtype.

bsts(_1,_2) :-
        'bsts$pre'(_1,_2),
        'bsts$cls'(_1,_2).
'bsts$pre'(_2,_1) :-
        reify_check(bst(_1),[_1],_4),
        reify_check(num(_2),[_2],_3),
        _5 is _3/\_4,
        _6 is _5,
        _7 is _5,
        _8 is _6\/_7,
        warn_if_false(_8,'CP').
'bsts$cls'(A,B) :-
        bsts_i(A,B).
bsts_i(_3,_4) :-
        'bsts_i$pre'(_3,_4),
        'bsts_i$cls'(_3,_4).
'bsts_i$pre'(_4,_3) :-
        reify_check(bst(_3),[_3],_6),
        reify_check(num(_4),[_4],_5),
        _7 is _5/\_6,
        _8 is _7,
        _9 is _8,
        warn_if_false(_9,'CP').
'bsts_i$cls'(E,t(_1,E,_2)) :-
        !.
'bsts_i$cls'(E,t(L,X,_1)) :-
        E<X,
        bsts_i(E,L).
'bsts_i$cls'(E,t(_1,X,R)) :-
        E>X,
        bsts_i(E,R).
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,_1) :-
        fail,
        !.
min_(t(nil,E,_1),E) :-
        !.
min_(t(L,_E,_R),Min) :-
        min_(L,Min).
max_(nil,_1) :-
        fail,
        !.
max_(t(_1,E,nil),E) :-
        !.
max_(t(_L,_E,R),Max) :-
        max_(R,Max).
bst_(nil,_1,_2) :-
        !.
bst_(t(L,E,R),Min,Max) :-
        Min=<E,
        E=<Max,
        bst_(L,Min,E),
        bst_(R,E,Max).
rt2(t(A,B,C)) :-
        term(A),
        arithexpression(B),
        term(C).