PUBS: A Practical Upper Bounds Solver
```
(* * * * * * * * * * *
* Resource Aware ML *
* * * * * * * * * * *
* File:
*   appendAll.raml
*
* Author:
*   Jan Hoffmann (2009)
*
* Resource Bound:
*   O(n)
*
* Description:
*   Implementations of functions that append lists (of lists (of lists)):
*   appendAll appends lists of lists, appendAll2 appends lists of lists of lists, ...
*
*   The example should show how RAML deals with inner lists.
*)

appendAll3 : L(L(L(L(int)))) -> L(int)

appendAll3 l =  let _=tick(1) in
match l with
| nil -> nil
| (l1::ls) -> append(appendAll2 l1,appendAll3 ls);

(*
eq(appendall3(H1,H2,R,C),1,[],[H1 =< 0]).
eq(appendall3(H1,H2,R,C),1,[inst([L1,L2],[out_appendall2(H2,R,C),out_appendall3(Hs,H2,R,C)],append(L1,L2)),append(L1,L2),out_appendall3(Hs,H2,R,C),out_appendall2(H2,R,C),appendall2(H2,R,C),appendall3(Hs,H2,R,C)],[H1>=1,Hs=H1-1]).

eq(out_appendall3(H1,H2,R,C),0,[],[H1 =< 0]).
eq(out_appendall3(H1,H2,R,C),0,[out_appendall2(H2,R,C),out_appendall3(Hs,H2,R,C)],[H1>=1,Hs=H1-1]).
*)

append : (L(int),L(int)) -> L(int)

append(l1,l2) =  let _=tick(1) in
match l1 with
| nil -> l2
| (x::xs) -> x::append(xs,l2);

(*
eq(append(N,M),1,[],[N =< 0]).
eq(append(N,M),1,[append(Np,M)],[N >= 1,Np = N-1]).
eq(inst(N,M,O),0,[],[]).
*)
appendAll : L(L(int)) -> L(int)

appendAll l =  let _=tick(1) in
match l with
| nil -> nil
| (l1::ls) -> append(l1,appendAll ls);

(*
eq(appendall(N,M),1,[],[N =< 0]).
eq(appendall(N,M),1,[inst([L],[out_appendall(NP,M)],append(M,L)),out_appendall(NP,M),append(M,L),appendall(Np,M)],[N >=1,Np=N-1]).
eq(out_appendall(N,M),0,[],[N =< 0]).
eq(out_appendall(N,M),nat(M),[out_appendall(Np,M)],[N >= 1,Np=N-1]).
*)

appendAll2 : L(L(L(int))) -> L(int)

appendAll2 l =  let _=tick(1) in
match l with
| nil -> nil
| (l1::ls) -> append(appendAll l1,appendAll2 ls);

(*
eq(appendall2(H,R,C),1,[],[H =< 0]).
eq(appendall2(H,R,C),1,[inst([L1,L2],[out_appendall(R,C),out_appendall2(H,R,C)],append(L1,L2)),append(L1,L2),out_appendall(R,C),out_appendall2(H,R,C),appendall(R,C),appendall2(Hs,R,C)],[H>=1,Hs=H-1,L >=0]).

eq(out_appendall2(H,R,C),0,[],[H =< 0]).
eq(out_appendall2(H,R,C),0,[out_appendall(R,C),out_appendall2(Hs,R,C)],[H>=1,Hs=H-1]).

*)

main = ()

```