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

oins(_1,_2,_3) :-
        'oins$pre'(_1,_2,_3,_4,_5,_6),
        'oins$cls'(_1,_2,_3),
        'oins$post'(_1,_2,_3,_4,_5,_6).
'oins$pre'(_2,_1,_3,_8,_10,_11) :-
        reify_check(listnum(_1),[_1],_6),
        reify_check(num(_2),[_2],_5),
        reify_check(sorted(_1),[_1],_7),
        reify_check(var(_3),[_3],_4),
        _12 is _4/\(_5/\_6),
        _9 is _4/\(_5/\_7),
        _8 is _9,
        _10 is _9,
        _11 is _12,
        _13 is _11\/_10\/_8,
        warn_if_false(_13,'CP').
'oins$post'(_1,_2,_3,_7,_,_) :-
        reify_check(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,
        _=1,
        _=1,
        _10 is _9,
        warn_if_false(_10,'AP').
'oins$cls'(A,B,C) :-
        oins_i(A,B,C).
oins_i(_1,_2,_3) :-
        'oins_i$pre'(_1,_2,_3,_4,_5),
        'oins_i$cls'(_1,_2,_3),
        'oins_i$post'(_1,_2,_3,_4,_5).
'oins_i$pre'(_1,_2,_3,_7,_9) :-
        reify_check(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 _8,
        _10 is _7\/_9,
        warn_if_false(_10,'CP').
'oins_i$post'(_1,_2,_3,_7,_) :-
        reify_check(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,
        _=1,
        _10 is _9,
        warn_if_false(_10,'AP').
'oins_i$cls'(X,[],[X]).
'oins_i$cls'(X,[Y|T],[X,Y|T]) :-
        X=<Y.
'oins_i$cls'(X,[Y|T],[Y|TT]) :-
        X>Y,
        oins_i(X,T,TT).
sorted([]).
sorted([_1]) :- !.
sorted([X|T]) :-
        head(T,_1),
        X=<_1,
        sorted(T).
head([X|_1],X).
listnum([]).
listnum([H|T]) :-
        num(H),
        listnum(T).
rt2([A|B]) :-
        num(A),
        listnum(B).