(STRATEGY
    INNERMOST)

(VAR
    n x xs y)
(DATATYPES
    A = µX.< nil, cons(X, X), true, false, 0, s(X), ys >)
(SIGNATURES
    qsort :: [A] -> A
    filterlow :: [A x A] -> A
    if1 :: [A x A x A x A] -> A
    filterhigh :: [A x A] -> A
    if2 :: [A x A x A x A] -> A
    ge :: [A x A] -> A
    append :: [A x A] -> A
    last :: [A] -> A)
(RULES
    qsort(nil()) -> nil()
    qsort(cons(x,xs)) ->
      append(qsort(filterlow(last(cons(x
                                      ,xs))
                            ,cons(x,xs)))
            ,cons(last(cons(x,xs))
                 ,qsort(filterhigh(last(cons(x
                                            ,xs))
                                  ,cons(x,xs)))))
    filterlow(n,nil()) -> nil()
    filterlow(n,cons(x,xs)) ->
      if1(ge(n,x),n,x,xs)
    if1(true(),n,x,xs) ->
      filterlow(n,xs)
    if1(false(),n,x,xs) -> cons(x
                               ,filterlow(n,xs))
    filterhigh(n,nil()) -> nil()
    filterhigh(n,cons(x,xs)) ->
      if2(ge(x,n),n,x,xs)
    if2(true(),n,x,xs) ->
      filterhigh(n,xs)
    if2(false(),n,x,xs) -> cons(x
                               ,filterhigh(n,xs))
    ge(x,0()) -> true()
    ge(0(),s(x)) -> false()
    ge(s(x),s(y)) -> ge(x,y)
    append(nil(),ys()) -> ys()
    append(cons(x,xs),ys()) ->
      cons(x,append(xs,ys()))
    last(nil()) -> 0()
    last(cons(x,nil())) -> x
    last(cons(x,cons(y,xs))) ->
      last(cons(y,xs)))