(STRATEGY
    INNERMOST)

(VAR
    x x' x2)
(DATATYPES
    A = µX.< S(X), 0 >)
(SIGNATURES
    f :: [A x A] -> A
    h :: [A x A] -> A
    g :: [A x A] -> A)
(RULES
    f(S(x'),S(x)) -> h(g(x',S(x))
                      ,f(S(S(x')),x))
    h(0(),S(x)) -> h(0(),x)
    h(0(),0()) -> 0()
    g(S(x),S(x')) -> h(f(S(x),S(x'))
                      ,g(x,S(S(x'))))
    g(S(x),0()) -> 0()
    f(S(x),0()) -> 0()
    h(S(x),x2) -> h(x,x2)
    g(0(),x2) -> 0()
    f(0(),x2) -> 0())