PUBS: A Practical Upper Bounds Solver
```
(* * * * * * * * * * *
* Resource Aware ML *
* * * * * * * * * * *
*
* File:
*   listsort.raml
*
* Author:
*   Jan Hoffmann (2010)
*
* Resource Bound:
*   O(n^2*m)
*
* Description:
*   Comparing lists of lists needs linear time.
*   Since insertion sort does a quadratic number of comparisons (in the worst case)
*   we need cubic time to sort a list of lists using islist below.
*
*   We derive a tight runtime bound.
*)

(*
eq(isortlist(R,C),1,[],[R=0]).
eq(isortlist(R,C),1,[insert(C,Rp,C),isortlist(Rp,C)],[R>=1,Rp = R-1]).
eq(insert(A,R,C),1,[],[R=0]).
eq(insert(A,R,C),1,[leq(A,C)],[R>=1]).
eq(insert(A,R,C),1,[leq(A,C),insert(A,Rs,C)],[R>=1,Rs = R-1]).
eq(leq(A,B),1,[],[A=0]).
eq(leq(A,B),1,[],[A >=1,B=0]).
eq(leq(A,B),1,[leq(Ap,Bp)],[A>=1,B>=1,Ap=A-1,Bp=B-1]).
*)

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

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

insert (x,l) =  let _=tick(1) in
match l with
| nil -> [x]
| (y::ys) -> if leq(x,y) then x::y::ys else y::insert(x,ys);

isortlist : L(L(int)) -> L(L(int))

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

main = ()

```