PUBS: A Practical Upper Bounds Solver
```
(* * * * * * * * * * *
* Resource Aware ML *
* * * * * * * * * * *
*
* File:
*   insertionsort.raml
*
* Author:
*   Jan Hoffmann (2009)
*
* Resource Bound:
*   O(n^2)
*
* Description:
*   Two implementations of the sorting algorithm insertion sort.
*
*   insertionsort admits a quatratic heap-space and time consumption.
*
*   insertionssortD uses the destructive insert function insertD.
*   Thus it has linear heap-space consumption while having still
*)

insertionsort : L(int) -> L(int)

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

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

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

insertionsortD : L(int) -> L(int)

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

(*
eq(insertionsortD(A),1,[],[A=0]).
eq(insertionsortD(A),1,[insertD(X,Ap),insertionsortD(Ap)],[A>=1,Ap=A-1]).
*)

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

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

(*
eq(insertD(A,B),1,[],[B=0]).
eq(insertD(A,B),1,[],[B>=1]).
eq(insertD(A,B),1,[insertD(A,Bp)],[B>=1,Bp = B-1]).
*)

```