(STRATEGY
    INNERMOST)

(VAR
    M N X Y Z)
(DATATYPES
    A = µX.< 0, s(X), true, false, nil, add(X, X), pair(X, X) >)
(SIGNATURES
    lt :: [A x A] -> A
    append :: [A x A] -> A
    split :: [A x A] -> A
    f_1 :: [A x A x A x A] -> A
    f_2 :: [A x A x A x A x A x A] -> A
    qsort :: [A] -> A
    f_3 :: [A x A x A] -> A)
(RULES
    lt(0(),s(X)) -> true()
    lt(s(X),0()) -> false()
    lt(s(X),s(Y)) -> lt(X,Y)
    append(nil(),Y) -> Y
    append(add(N,X),Y) -> add(N
                             ,append(X,Y))
    split(N,nil()) -> pair(nil()
                          ,nil())
    split(N,add(M,Y)) -> f_1(split(N
                                  ,Y)
                            ,N
                            ,M
                            ,Y)
    f_1(pair(X,Z),N,M,Y) -> f_2(lt(N
                                  ,M)
                               ,N
                               ,M
                               ,Y
                               ,X
                               ,Z)
    f_2(true(),N,M,Y,X,Z) -> pair(X
                                 ,add(M,Z))
    f_2(false(),N,M,Y,X,Z) ->
      pair(add(M,X),Z)
    qsort(nil()) -> nil()
    qsort(add(N,X)) -> f_3(split(N
                                ,X)
                          ,N
                          ,X)
    f_3(pair(Y,Z),N,X) ->
      append(qsort(Y)
            ,add(X,qsort(Z))))