% =================================================================
:- pred constr(bool).    
:- mode constr(in).
:- ignore constr/1.
% ===========================================================
% Program
:- pred rev(list(int),list(int)).
:- mode rev(in,out).
rev([],[]).
rev([H|T],R) :-
  rev(T,S),
  snoc(S,H,R).

:- pred snoc(list(int),int,list(int)).
:- mode snoc(in,in,out).  
snoc([],X,[X]).
snoc([X|Xs],Y,[X|Zs]) :-
  snoc(Xs,Y,Zs).
% ===========================================================
% Catamorphism       % total function 
:- pred listMax(list(int),bool,int).  
:- mode listMax(in,out,out).
:- cata listMax/3-1.

listMax([],IsDef,A) :- constr( (~IsDef) & (A=0) ). % 0 can be any int.
listMax([H|T],IsDef,Max) :-  
         constr( (IsDef & (Max = ite(IsDefT, ite(H>MaxT,H,MaxT), H )) ) ),   
         listMax(T,IsDefT,MaxT).  

% ===========================================================
% Property
:- pred ff1.
ff1 :-
  constr( ~(N1=N2) ), 
  listMax(L,IsDefLM,N1),
	rev(L,R),
  listMax(R,IsDefRM,N2).

:- pred ff2.
ff2 :-
      constr(~( IsDefC & (N2 = ite(IsDefA, ite(B>N1,B,N1), B)) )),
      listMax(A,IsDefA,N1), listMax(C,IsDefC,N2),
      snoc(A,B,C).
% ===========================================================
:- query ff1/0.
:- query ff2/0.
% ===========================================================