(VAR x y z)
(RULES
+(+(x, y), z) -> +(x, +(y, z))
+(x, 0) -> x
*(*(x, y), z) -> *(x, *(y, z))
*(x, 1) -> x
exp(0) -> 1
exp(+(x, y)) -> *(exp(x), exp(y))
)
(COMMENT Example 3.13 in \cite{SK90})