:- module(_, [], [rtchecks_shallow, assertions,regtypes,fsyntax,nativeprops,predefres(res_steps)]). :- prop sorted/1. sorted([]). sorted([_]):-!. sorted([X|T]):- X=< ~head(T), sorted(T). head([X|_],X). :- pred oins(E,L,NL):(num(E),sorted(L),var(NL)) => (num(E),sorted(L),sorted(NL)). oins(X,[],[X]). oins(X,[Y|T],[X,Y|T]):- X =< Y. oins(X,[Y|T],[Y|TT]):- X > Y, oins(X,T,TT).