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))))) SCC Processor: #sccs: 2 #rules: 2 #arcs: 5/9 DPs: max#(N(L(x),N(y,z))) -> 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))))) Subterm Criterion Processor: simple projection: pi(max#) = 0 problem: DPs: 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))))) Qed DPs: max#(N(L(s(x)),L(s(y)))) -> max#(N(L(x),L(y))) 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))))) Matrix Interpretation Processor: dimension: 1 interpretation: [max#](x0) = x0, [s](x0) = x0 + 1, [N](x0, x1) = x1, [0] = 0, [max](x0) = x0, [L](x0) = x0 orientation: max#(N(L(s(x)),L(s(y)))) = y + 1 >= y = max#(N(L(x),L(y))) max(L(x)) = x >= x = x max(N(L(0()),L(y))) = y >= y = y max(N(L(s(x)),L(s(y)))) = y + 1 >= y + 1 = s(max(N(L(x),L(y)))) max(N(L(x),N(y,z))) = z >= z = max(N(L(x),L(max(N(y,z))))) problem: DPs: 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))))) Qed