YES Time: 0.010 Problem: Equations: TRS: pAC(x,zero()) -> x pAC(i(x),x) -> zero() mAC(x,one()) -> x mAC(pAC(x,y),z) -> pAC(mAC(x,z),mAC(y,z)) mAC(x,x) -> x pAC(x,x) -> zero() Proof: AC-RPO Processor: precedence: one > i > mAC > pAC > zero status: problem: Equations: TRS: Qed