(VAR x y z)
(RULES
   *(e,x) -> x
   *(i(x),x) -> e
   i(e) -> e
   i(i(x)) -> x
   i(*(x,y)) -> *(i(x),i(y))
   f(*(x,y)) -> *(f(x),f(y))
   f(e) -> e
   f(i(x)) -> i(f(x))
   *(*(x,y),z) -> *(x,*(y,z))
   *(x,*(y,z)) -> *(*(x,y),z)
   *(x,y) -> *(y,x)
)
(COMMENT Example 3.16 of Winkler/Middeldorp RTA 2013)