(VAR x y z ) (RULES +(x,y) -> +(y,x) *(+(x,y),z) -> +(*(x,z),*(y,z)) *(+(y,x),z) -> +(*(x,z),*(y,z)) )