% =================================================================
:- pred constr(bool). 
:- mode constr(in). 
:- ignore constr/1.
% =================================================================
% Program
:- pred append(list(int),list(int),list(int)).
:- mode append(in,in,out).

append([],Ys,Ys).  
append([X|Xs],Ys,[X|Zs]) :- append(Xs,Ys,Zs).

% =================================================================
% Catamorphisms.   
% -------------

% all_grt(List,N,Res) Res iff all elements of List are >= N
:- pred all_grt(list(int),int,bool).
:- mode all_grt(in,in,out).
:- cata all_grt/3-1.

all_grt([],N,Res) :- constr( Res ).   
all_grt([Y|Ys],N,Res) :- constr( Res=ite(Y>N,ResYs,false) ), all_grt(Ys,N,ResYs). 

% =================================================================
% ------ Verification of contract on append:  
:- pred ff1.
ff1 :-                                                
  constr( ~((B1 & B2) = B3) ), 
  all_grt(Xs,K,B1), all_grt(Ys,K,B2), all_grt(Zs,K,B3),
  append(Xs,Ys,Zs).
% =================================================================
:- query ff1/0.
% =================================================================