(STRATEGY
    INNERMOST)

(VAR
    x y)
(DATATYPES
    A = µX.< 0, s(X), pair(X, X) >)
(SIGNATURES
    f :: [A] -> A
    g :: [A] -> A
    h :: [A] -> A
    p :: [A] -> A
    q :: [A] -> A
    + :: [A x A] -> A)
(RULES
    f(0()) -> 0()
    f(s(0())) -> s(0())
    f(s(s(x))) -> p(h(g(x)))
    g(0()) -> pair(s(0()),s(0()))
    g(s(x)) -> h(g(x))
    h(x) -> pair(+(p(x),q(x)),p(x))
    p(pair(x,y)) -> x
    q(pair(x,y)) -> y
    +(x,0()) -> x
    +(x,s(y)) -> s(+(x,y))
    f(s(s(x))) -> +(p(g(x)),q(g(x)))
    g(s(x)) -> pair(+(p(g(x))
                     ,q(g(x)))
                   ,p(g(x))))