(VAR x y z)
(RULES
  +(x,y) -> +(y,x)
  *(+(x,y),z) -> +(*(x,z),*(y,z))
  *(+(y,x),z) -> +(*(x,z),*(y,z))
)
(COMMENT
doi:10.1007/978-3-319-43144-4_18
[110] Example 7
)