(VAR x y z)
(RULES
*(x,*(y,z)) -> *(otimes(x,y),z)
*(1,y) -> y
*(+(x,y),z) -> oplus(*(x,z),*(y,z))
*(x,oplus(y,z)) -> oplus(*(x,y),*(x,z))
)
(COMMENT Example 4.10 (A-Modules) in \cite{SK90})