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