% =================================================================
:- pred constr(bool).
:- mode constr(in).
:- ignore constr/1.
% =================================================================
% Program. 
% Delete all multiple copies on lists leaving one copy only.
% checking for all positive numbers
:- pred list_deletecopies_pos(list(int),list(int),bool).
:- mode list_deletecopies_pos(in,out,out).

list_deletecopies_pos([],[],B) :- constr(B).
list_deletecopies_pos([X],[X,Y],B) :- constr(B=(X>0)).    %error: [X,Y] --> [X]
list_deletecopies_pos([X,X|T], ResT, A) :- constr(A=(B&(X>0))), cons(X,T,XT), 
                       list_deletecopies_pos(XT,ResT,B).
list_deletecopies_pos([X,Y|T], [X|ResT], A) :- constr(A=(B&(X>0))),constr(~(X=Y)), 
      cons(Y,T,YT),
      list_deletecopies_pos(YT,ResT1,B), deleteall(X,ResT1,ResT).

% all elements X are deleted from a list, producing a new list.
:- pred deleteall(int,list(int),list(int)).
:- mode deleteall(in,in,out).

deleteall(X,[],[]).
deleteall(X,[X|T],Res) :- deleteall(X,T,Res).
deleteall(X,[H|T],[H|ResT]) :- constr(~(X=H)), deleteall(X,T,ResT).

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

% =================================================================
% catamorphism
:- pred listsum(list(int),int).
:- mode listsum(in,out).
:- cata listsum/2-1.

listsum([],S) :- S=0.
listsum([H|T],S) :-
  S=(H+ST),
  listsum(T,ST).

% =================================================================
% Verification.
% Property:
:- pred ff1.
ff1 :- 
     constr(~(P => (SL >= SS) )), 
     listsum(L,SL), listsum(S,SS),  
     list_deletecopies_pos(L,S,P).

:- spec deleteall(X,L,L1) ==>
                    listsum(L,LS), listsum(L1,L1S) => constr(true).

:- spec cons(H,T,HT) ==> 
                   listsum(T,TS), listsum(HT,HTS) => constr(true).

% =================================================================
:- query ff1/0.
% =================================================================