% =================================================================
:- 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],[B|Xs]) :- constr( A=<B ). % error: [B|Xs] should be [A,B|Xs]
ord_ins(A,[B|Xs],[B|AXs]) :- constr( A>B ), 
     ord_ins(A,Xs,AXs).

% =================================================================
% catamorphism
:- pred length(list(int),int).
:- mode length(in,out).
:- cata length/2-1.

length([],L) :- constr((L=0)).
length([H|T],L) :-
  constr( (L=LT+1) ),
  length(T,LT).

% =================================================================
% Verification. 
% Property:
:- pred ff1.
ff1 :- 
   constr(~(LL=LS)), 
   length(L,LL), length(S,LS),  
   insertionsort(L,S).

:- pred ff2.
ff2 :- 
   constr( ~(LXL = (LL+1)) ), 
   length(L,LL), length(XL,LXL), 
   ord_ins(X,L,XL).

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