(VAR x y1 y2)
(THEORY (AC p))
(RULES
p(zero,x) -> x
p(i(x),x) -> zero
phi(zero, y1) -> y1
phi(y1, phi(y2, x)) -> phi(p(y1,y2), x)
phi(g1(x), g2(y1)) -> phi(g2(y1), g1(x))
g1(zero) -> zero
g2(zero) -> zero
g1(p(x,y)) -> p(g1(x),g1(y))
g2(p(x,y)) -> p(g2(x),g2(y))
)