YES Time: 0.013 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-KBO Processor: precedence: maxAC ~ minAC > plus > s ~ 0 weight function: w0 = 8 w(s) = 15 w(0) = 8 w(plus) = w(maxAC) = w(minAC) = 0 problem: Equations: TRS: Qed