(STRATEGY
    INNERMOST)

(VAR
    m n x y)
(DATATYPES
    A = µX.< 0, true, s(X), false, nil, add(X, X) >)
(SIGNATURES
    le :: [A x A] -> A
    app :: [A x A] -> A
    low :: [A x A] -> A
    if_low :: [A x A x A] -> A
    high :: [A x A] -> A
    if_high :: [A x A x A] -> A
    head :: [A] -> A
    tail :: [A] -> A
    isempty :: [A] -> A
    quicksort :: [A] -> A
    if_qs :: [A x A x A x A] -> A)
(RULES
    le(0(),y) -> true()
    le(s(x),0()) -> false()
    le(s(x),s(y)) -> le(x,y)
    app(nil(),y) -> y
    app(add(n,x),y) -> add(n
                          ,app(x,y))
    low(n,nil()) -> nil()
    low(n,add(m,x)) -> if_low(le(m
                                ,n)
                             ,n
                             ,add(m,x))
    if_low(true(),n,add(m,x)) ->
      add(m,low(n,x))
    if_low(false(),n,add(m,x)) ->
      low(n,x)
    high(n,nil()) -> nil()
    high(n,add(m,x)) -> if_high(le(m
                                  ,n)
                               ,n
                               ,add(m,x))
    if_high(true(),n,add(m,x)) ->
      high(n,x)
    if_high(false(),n,add(m,x)) ->
      add(m,high(n,x))
    head(add(n,x)) -> n
    tail(add(n,x)) -> x
    isempty(nil()) -> true()
    isempty(add(n,x)) -> false()
    quicksort(x) -> if_qs(isempty(x)
                         ,low(head(x),tail(x))
                         ,head(x)
                         ,high(head(x),tail(x)))
    if_qs(true(),x,n,y) -> nil()
    if_qs(false(),x,n,y) ->
      app(quicksort(x)
         ,add(n,quicksort(y))))