PUBS: A Practical Upper Bounds Solver
```
(* * * * * * * * * * *
* Resource Aware ML *
* * * * * * * * * * *
*
* File:
*   duplicates.raml
*
* Author:
*   Jan Hoffmann (2010)
*
* Resource Bound:
*   O(n^2*m)
*
* Description:
*   The function nub removes duplicates from a list of lists.  The runtime
*   is O(n^2*m) if n is the size of the outer list an m is the maximal
*   size of the inner lists.
*)

eq : (L(int),L(int)) -> bool

eq (l1,l2) = let _=tick(1) in
match l1 with
| nil -> match l2 with
| nil -> true
| (y::ys) -> false
| (x::xs) -> match l2 with
| nil -> false
| (y::ys) -> (x == y) and (eq (xs,ys));

(*
eq(eq(L1,L2),1,[],[L1=0]).
eq(eq(L1,L2),1,[],[L1>=1,L2=0]).
eq(eq(L1,L2),1,[eq(Ls1,Ls2)],[L1>=1,L2>=1,Ls1=L1-1,Ls2=L2-1]).
*)
(* nub removes duplicates from a list of lists. *)
nub : L(L(int)) -> L(L(int))

nub l = let _=tick(1) in
match l with
| nil -> nil
| (x::xs) -> x::nub( remove(x,xs) );

(*
eq(nub(L1,L2),1,[],[L1=0]).
eq(nub(L1,L2),1,[remove(X,Ls1,L2),nub(L3,L2)],[L1>=1,Ls1 = L1-1, L3 =< Ls1]).
*)
remove : (L(int),L(L(int))) -> L(L(int))

remove (x,l) = let _=tick(1) in
match l with
| nil -> nil
| (y::ys) -> if eq (x,y) then remove(x,ys)
else y::remove(x,ys);
(*
eq(remove(X,L1,L2),1,[],[L1=0]).
eq(remove(X,L1,L2),1,[eq(X,L2),remove(X,Ls1,L2)],[L1>=1,Ls1 = L1-1]).
eq(remove(X,L1,L2),1,[remove(X,Ls1,L2)],[L1>=1,Ls1 = L1-1]).
*)

```