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