YES Time: 0.008021 TRS: { max L x -> x, max N(L x, N(y, z)) -> max N(L x, L max N(y, z)), max N(L 0(), L y) -> y, max N(L s x, L s y) -> s max N(L x, L y)} DP: DP: {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)), max# N(L s x, L s y) -> max# N(L x, L y)} TRS: { max L x -> x, max N(L x, N(y, z)) -> max N(L x, L max N(y, z)), max N(L 0(), L y) -> y, max N(L s x, L s y) -> s max N(L x, L y)} EDG: {(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(L x, L max N(y, z)), max# N(L s x, L s y) -> max# N(L x, L y))} STATUS: arrows: 0.777778 SCCS (0):