(STRATEGY
    INNERMOST)

(VAR
    N X X1 X2 Y Z)
(DATATYPES
    A = µX.< cs(X, X), r(X), nt(X), ns(X), 0, nil, nf(X, X) >)
(SIGNATURES
    t :: [A] -> A
    q :: [A] -> A
    d :: [A] -> A
    p :: [A x A] -> A
    f :: [A x A] -> A
    s :: [A] -> A
    a :: [A] -> A)
(RULES
    t(N) -> cs(r(q(N)),nt(ns(N)))
    q(0()) -> 0()
    q(s(X)) -> s(p(q(X),d(X)))
    d(0()) -> 0()
    d(s(X)) -> s(s(d(X)))
    p(0(),X) -> X
    p(X,0()) -> X
    p(s(X),s(Y)) -> s(s(p(X,Y)))
    f(0(),X) -> nil()
    f(s(X),cs(Y,Z)) -> cs(Y
                         ,nf(X,a(Z)))
    t(X) -> nt(X)
    s(X) -> ns(X)
    f(X1,X2) -> nf(X1,X2)
    a(nt(X)) -> t(a(X))
    a(ns(X)) -> s(a(X))
    a(nf(X1,X2)) -> f(a(X1),a(X2))
    a(X) -> X)