MAYBE Time: 0.230 Problem: Equations: TRS: pAC(x,zero()) -> x pAC(f(x),f(y)) -> f(pAC(x,y)) f(zero()) -> zero() pAC(g(x),g(y)) -> g(pAC(x,y)) g(zero()) -> zero() m(one(),x) -> x m(x,one()) -> x f(one()) -> one() g(one()) -> one() m(z,pAC(x,y)) -> pAC(m(z,x),m(z,y)) m(pAC(x,y),z) -> pAC(m(x,z),m(y,z)) m(f(x),f(y)) -> f(m(x,y)) m(g(x),g(y)) -> g(m(x,y)) Proof: Open