% =================================================================
:- 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,Y,R), constr(Y=158). % error: snoc(T,Y,R) --> 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            % a total function
:- pred listMinMax(list(int),bool,int,int).
:- mode listMinMax(in,out,out,out). 
:- cata listMinMax/4-1.
listMinMax([],IsDef,A,B) :- constr( (~IsDef) & (A=0 & B=0) ). % 0 and 0 can be any two int.
listMinMax([H|T],IsDef,Min,Max) :-  
          constr(( IsDef & 
                     ((Min = ite(IsDefT, ite(H<MinT,H,MinT), H)) &
                      (Max = ite(IsDefT, ite(H>MaxT,H,MaxT), H)))
                )),
            listMinMax(T,IsDefT,MinT,MaxT).
 
% ===========================================================

% Property
:- pred ff1.
ff1 :-
  constr( ~( (IsDefL=IsDefR) & ((N1=N2) & (M1=M2)) ) ),    
  listMinMax(L,IsDefL,N1,M1),
	rev(L,R),
  listMinMax(R,IsDefR,N2,M2).

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