(STRATEGY
    INNERMOST)

(VAR
    x y z)
(DATATYPES
    A = µX.< s(X), 0 >)
(SIGNATURES
    times :: [A x A] -> A
    plus :: [A x A] -> A)
(RULES
    times(x,plus(y,s(z))) ->
      plus(times(x
                ,plus(y,times(s(z),0())))
          ,times(x,s(z)))
    times(x,0()) -> 0()
    times(x,s(y)) -> plus(times(x,y)
                         ,x)
    plus(x,0()) -> x
    plus(x,s(y)) -> s(plus(x,y)))