YES Time: 0.010 Problem: Equations: TRS: plus(x,0()) -> x plus(x,s(y)) -> s(plus(x,y)) minAC(0(),y) -> 0() minAC(s(x),s(y)) -> s(minAC(x,y)) maxAC(0(),y) -> y maxAC(s(x),s(y)) -> s(maxAC(x,y)) Proof: AC-RPO Processor: precedence: plus > 0 > maxAC > minAC > s status: plus:mul problem: Equations: TRS: Qed