YES Problem: max(L(x)) -> x max(N(L(0()),L(y))) -> y max(N(L(s(x)),L(s(y)))) -> s(max(N(L(x),L(y)))) max(N(L(x),N(y,z))) -> max(N(L(x),L(max(N(y,z))))) Proof: DP Processor: DPs: max#(N(L(s(x)),L(s(y)))) -> max#(N(L(x),L(y))) max#(N(L(x),N(y,z))) -> max#(N(y,z)) max#(N(L(x),N(y,z))) -> max#(N(L(x),L(max(N(y,z))))) TRS: max(L(x)) -> x max(N(L(0()),L(y))) -> y max(N(L(s(x)),L(s(y)))) -> s(max(N(L(x),L(y)))) max(N(L(x),N(y,z))) -> max(N(L(x),L(max(N(y,z))))) EDG Processor: DPs: max#(N(L(s(x)),L(s(y)))) -> max#(N(L(x),L(y))) max#(N(L(x),N(y,z))) -> max#(N(y,z)) max#(N(L(x),N(y,z))) -> max#(N(L(x),L(max(N(y,z))))) TRS: max(L(x)) -> x max(N(L(0()),L(y))) -> y max(N(L(s(x)),L(s(y)))) -> s(max(N(L(x),L(y)))) max(N(L(x),N(y,z))) -> max(N(L(x),L(max(N(y,z))))) graph: max#(N(L(s(x)),L(s(y)))) -> max#(N(L(x),L(y))) -> max#(N(L(s(x)),L(s(y)))) -> max#(N(L(x),L(y))) max#(N(L(x),N(y,z))) -> max#(N(L(x),L(max(N(y,z))))) -> max#(N(L(s(x)),L(s(y)))) -> max#(N(L(x),L(y))) max#(N(L(x),N(y,z))) -> max#(N(y,z)) -> max#(N(L(s(x)),L(s(y)))) -> max#(N(L(x),L(y))) max#(N(L(x),N(y,z))) -> max#(N(y,z)) -> max#(N(L(x),N(y,z))) -> max#(N(y,z)) max#(N(L(x),N(y,z))) -> max#(N(y,z)) -> max#(N(L(x),N(y,z))) -> max#(N(L(x),L(max(N(y,z))))) CDG Processor: DPs: max#(N(L(s(x)),L(s(y)))) -> max#(N(L(x),L(y))) max#(N(L(x),N(y,z))) -> max#(N(y,z)) max#(N(L(x),N(y,z))) -> max#(N(L(x),L(max(N(y,z))))) TRS: max(L(x)) -> x max(N(L(0()),L(y))) -> y max(N(L(s(x)),L(s(y)))) -> s(max(N(L(x),L(y)))) max(N(L(x),N(y,z))) -> max(N(L(x),L(max(N(y,z))))) graph: max#(N(L(x),N(y,z))) -> max#(N(L(x),L(max(N(y,z))))) -> max#(N(L(s(x)),L(s(y)))) -> max#(N(L(x),L(y))) SCC Processor: #sccs: 0 #rules: 0 #arcs: 1/9