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)) Proof: AC-RPO Processor: precedence: one > i > zero > mAC > pAC status: problem: Equations: TRS: Qed