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