(STRATEGY
    INNERMOST)

(VAR
    x x' y)
(DATATYPES
    A = µX.< S(X), 0 >)
(SIGNATURES
    power :: [A x A] -> A
    mult :: [A x A] -> A
    add0 :: [A x A] -> A
    + :: [A x A] -> A)
(RULES
    power(x',S(x)) -> mult(x'
                          ,power(x',x))
    mult(x',S(x)) -> add0(x'
                         ,mult(x',x))
    add0(x',S(x)) -> +(S(0())
                      ,add0(x',x))
    power(x,0()) -> S(0())
    mult(x,0()) -> 0()
    add0(x,0()) -> x
    +(x,S(0())) ->= S(x)
    +(S(0()),y) ->= S(y))