% =================================================================
:- pred constr(bool).
:- mode constr(in).
:- ignore constr/1.
% ====================================================
% Program.
:- pred member(int,list(int),bool).
:- mode member(in,in,out).
member(X,[],B) :- B=false.
member(X,[Y|Ys],B) :-
      constr( B=ite(X=Y,false,B1) ) , % error: false should be true
      member(X,Ys,B1).

:- pred cons(int,list(int),list(int)).
:- mode cons(in,in,out).
cons(H,T,[H|T]).

% ====================================================
% catamorphism
:- pred listMin(list(int),bool,int).            
:- mode listMin(in,out,out).
:- cata listMin/3-1.

listMin([],IsDef,A) :- constr( ((~IsDef) & A=0) ).
listMin([H|T],IsDef,Min) :-
         constr( (IsDef & ( Min = ite(IsDefT, ite(H<MinT,H,MinT), H )) ) ),
         listMin(T,IsDefT,MinT).
 
% ====================================================
% verification.

:- pred ff1.
ff1 :-                              % member
   constr( ~(ite(IsDefMinL, ((X=MinL) => B), (~B)))),
   listMin(L,IsDefMinL,MinL),
   member(X,L,B).

:- pred ff2.
ff2 :-                              % listMin
   constr( ~(MinHT =< H) ),
   cons(H,T,HT),
   listMin(HT,IsDefMinHT,MinHT).

:- pred ff3.
ff3 :-                              % cons
  constr( ~( IsDefMinHT &
            (MinHT = ite(IsDefMinT,ite(H<MinT,H,MinT),H)) ) ),
  listMin(T,IsDefMinT,MinT), listMin(HT,IsDefMinHT,MinHT),
  cons(H,T,HT).
% ===============================================================
:- query ff1/0. 
:- query ff2/0. 
:- query ff3/0. 
% ===============================================================