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

list_deletecopies([],[]).
list_deletecopies([X],[X,X]). %error: [X,X] ---> [X] 
list_deletecopies([X,X|T], ResT) :- cons(X,T,XT), list_deletecopies(XT,ResT).
list_deletecopies([X,Y|T], [X|ResT]) :- constr(~(X=Y)), cons(Y,T,YT),
      list_deletecopies(YT,ResT1), 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 listsize(list(int),int).
:- mode listsize(in,out).
:- cata listsize/2-1.

listsize([],L) :- L=1.
listsize([H|T],L) :-
  L=(LT+1),
  listsize(T,LT). 

%  
% =================================================================
% Verification.
% Property:
:- pred ff1.
ff1 :- 
   constr(~(CL >= CS)),
   listsize(L,CL), listsize(S,CS),
   list_deletecopies(L,S).

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

:- spec cons(H,T,HT) ==> listsize(T,TN), listsize(HT,HTN) => constr(true).

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