(VAR x)
(THEORY (AC f))
(RULES
f(x,one) -> x
f(i(x),x) -> one
)