(STRATEGY
    INNERMOST)

(VAR
    x y)
(DATATYPES
    A = µX.< 0, I(X) >)
(SIGNATURES
    O :: [A] -> A
    + :: [A x A] -> A
    * :: [A x A] -> A)
(RULES
    O(0()) -> 0()
    +(0(),x) -> x
    +(x,0()) -> x
    +(O(x),O(y)) -> O(+(x,y))
    +(O(x),I(y)) -> I(+(x,y))
    +(I(x),O(y)) -> I(+(x,y))
    +(I(x),I(y)) -> O(+(+(x,y)
                       ,I(0())))
    *(0(),x) -> 0()
    *(x,0()) -> 0()
    *(O(x),y) -> O(*(x,y))
    *(I(x),y) -> +(O(*(x,y)),y))