:-module(_,[],[]).
'$applied_packages'([prelude,nonpure,condcomp,rtchecks_shallow,assertions,regtypes,fsyntax,nativeprops,predefres(res_steps),resdefs,resdefs/resources_decl,basicmodes,argnames,expander]).

:-prop sorted/1.
:-pred ord_insert(E,L,NL):(num(E),sorted(L),var(NL))=>(num(E),sorted(L),sorted(NL)).

sorted([]).
sorted([_]):-!.
sorted([X|T]):-
	X=< ~head(T),
	sorted(T).
head([X|_],X).

ord_insert(_1,_2,_3) :-
        'ord_insert$pre'(_1,_2,_3,_4),
        'ord_insert$cls'(_1,_2,_3),
        'ord_insert$post'(_1,_2,_3,_4).
'ord_insert$pre'(_1,_2,_3,_7) :-
        reify_check(rtc_num(_1),[_1],_5),
        reify_check(sorted(_2),[_2],_6),
        reify_check(var(_3),[_3],_4),
        _8 is _4/\(_5/\_6),
        _7 is _8,
        _9 is _7,
        warn_if_false(_9,'CP').
'ord_insert$post'(_1,_2,_3,_7) :-
        reify_check(rtc_num(_1),[_1],_5),
        reify_check(sorted(_2),[_2],_6),
        reify_check(sorted(_3),[_3],_4),
        _8 is _4/\(_5/\_6),
        _9 is _7#1\/_8,
        _10 is _9,
        warn_if_false(_10,'AP').
'ord_insert$cls'(X,[],[X]).
'ord_insert$cls'(X,[Y|T],[X,Y|T]) :-
        X=<Y.
'ord_insert$cls'(X,[Y|T],[Y|TT]) :-
        X>Y,
        ord_insert(X,T,TT).