% =================================================================
:- pred constr(bool).
:- mode constr(in).
:- ignore constr/1.
% ====================================================
% Program.
:- pred member(int,list(int),bool).
:- mode member(in,in,out).
member(X,[],false).
member(X,[Y|Ys],B) :-
      constr( B=ite(X=Y,true,B1) ) ,
      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).
 
% ====================================================
% Contract on member:
:- spec member(X,L,B) ==>
        listMin(L,IsDefMinL,MinL) =>
        constr( ite(IsDefMinL, ((X=MinL) => B), (~B)) ).

% Contract on listMin:
:- spec listMin(HT,IsDefMinHT,MinHT) ==>
        cons(H,T,HT) =>
        constr( MinHT =< H ).

% Contract on cons:
:- spec cons(H,T,HT) ==>
		 listMin(T,IsDefMinT,MinT), listMin(HT,IsDefMinHT,MinHT) =>
		 constr( IsDefMinHT &
             (MinHT = ite(IsDefMinT,ite(H<MinT,H,MinT),H))
           ).

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

% ====================================================
% NON-CATA predicates: cons constr member