(STRATEGY
    INNERMOST)

(VAR
    n x xs y)
(DATATYPES
    A = µX.< nil, cons(X, X), true, false, 0, s(X), ys >)
(SIGNATURES
    qsort :: [A] -> A
    qs :: [A x 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
    length :: [A] -> A
    half :: [A] -> A
    get :: [A x A] -> A)
(RULES
    qsort(xs) -> qs(half(length(xs))
                   ,xs)
    qs(n,nil()) -> nil()
    qs(n,cons(x,xs)) ->
      append(qs(half(n)
               ,filterlow(get(n,cons(x,xs))
                         ,cons(x,xs)))
            ,cons(get(n,cons(x,xs))
                 ,qs(half(n)
                    ,filterhigh(get(n,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()))
    length(nil()) -> 0()
    length(cons(x,xs)) ->
      s(length(xs))
    half(0()) -> 0()
    half(s(0())) -> 0()
    half(s(s(x))) -> s(half(x))
    get(n,nil()) -> 0()
    get(n,cons(x,nil())) -> x
    get(0(),cons(x,cons(y,xs))) -> x
    get(s(n),cons(x,cons(y,xs))) ->
      get(n,cons(y,xs)))