% ====================================================
:- 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).


% =================================================================
% Catamorphism.   
% -------------

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

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


% =================================================================
% Contracts.  
:- spec append(Xs,Ys,Zs) ==>                             % --- (1)
        all_leq(Xs,K,B1), all_leq(Ys,K,B2), all_leq(Zs,K,B3) => 
             constr( ((B1 & B2) = B3) ).                 % this is an iff

% =================================================================

% ------ Verification of contract on append:  
% negation of constr in contract                      
:- pred ff1.
ff1 :-                                                   % --- (1)
  constr( ~((B1 & B2) = B3) ),                           % this is an iff
  all_leq(Xs,K,B1), all_leq(Ys,K,B2), all_leq(Zs,K,B3),
  append(Xs,Ys,Zs).

% =================================================================


% NON-CATA predicates: append constr