(STRATEGY
    INNERMOST)

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