(STRATEGY
    INNERMOST)

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