(VAR
    ls pivot rs x xs y ys z zs)

(DATATYPES
   a = µX. < nil, dd(c,X) >
   b = < true, false >
   c = µX. < s(X), 0 >
   d = < pair(a,a) >
 )

(SIGNATURES
   gt :: c x c -> b
   quicksort :: a -> a
   split :: c x a -> d
   quicksort' :: c x d -> a
   append :: a x a -> a
   split' :: b x c x d -> d
 )


(RULES
    gt(s(x),0)    -> true
    gt(0,s(y))    -> false
    gt(0,0)       -> false
    gt(s(x),s(y)) -> gt(x,y)

    quicksort(nil)            -> nil
    quicksort(dd(z,zs))       -> quicksort'(z,split(z,zs))
    quicksort'(z,pair(xs,ys)) -> append(quicksort(xs),dd(z,quicksort(ys)))

    split(pivot,nil)              -> pair(nil,nil)
    split(pivot,dd(x,xs))         -> split'(gt(x,pivot),x,split(pivot,xs))
    split'(true, x, pair(ls,rs))  -> pair(ls,dd(x,rs))
    split'(false, x, pair(ls,rs)) -> pair(dd(x,ls),rs)

    append(nil,ys)      -> ys
    append(dd(x,xs),ys) -> dd(x,append(xs,ys))
)