% =================================================================
:- pred constr(bool).
:- mode constr(in).
:- ignore constr/1.

% =================================================================
% Program. ascending sorting
:- pred insertionsort(list(int),list(int)).
:- mode insertionsort(in,out).

insertionsort([],[]). 
insertionsort([X|Xs],S) :- ord_ins(X,TS,S),
         insertionsort(Xs,TS).

:- pred ord_ins(int,list(int),list(int)).  
:- mode ord_ins(in,in,out).

ord_ins(A,[],[A]).
ord_ins(A,[B|Xs],[A,B|Xs]) :- constr( A=<B ).
ord_ins(A,[B|Xs],AXs) :- constr( A>B ),  %error on this line: AXs should be [B|AXs]
     ord_ins(A,Xs,AXs).

% =================================================================
% catamorphisms
:- pred count(int,list(int),int).
:- mode count(in,in,out).
:- cata count/3-2.

count(X,[],Res) :- constr( Res=0 ).
count(X,[Y|Ys],Res) :- 
    constr( Res=ite(X=Y,(ResT+1),ResT) ),  
    count(X,Ys,ResT).   

% =================================================================
% verification. 
% Property:
:- pred ff1.
ff1 :- 
   constr(~(CL = CS)), 
   count(X,L,CL), count(X,S,CS),  
   insertionsort(L,S).

:- pred ff2.
ff2 :- 
   constr( ~( CXL = ite(X=Y,(CL+1),CL) ) ), 
   count(Y,L,CL), count(Y,XL,CXL) , 
   ord_ins(X,L,XL).

% ==========================================================
:- query ff1/0.
:- query ff2/0.
% ==========================================================