YES
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))))}
 RUF:
  Strict:
   {               max(L(x)) -> x,
       max(N(L(x), N(y, z))) -> max(N(L(x), L(max(N(y, z))))),
    max(N(L(s(x)), L(s(y)))) -> s(max(N(L(x), L(y))))}
  Weak:
   {}
  DP:
   Strict:
    {   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)))}
   Weak:
   {               max(L(x)) -> x,
       max(N(L(x), N(y, z))) -> max(N(L(x), L(max(N(y, z))))),
    max(N(L(s(x)), L(s(y)))) -> s(max(N(L(x), L(y))))}
   EDG:
    {(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(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))))))
     (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))))}
    SCCS:
     Scc:
      {max#(N(L(s(x)), L(s(y)))) -> max#(N(L(x), L(y)))}
     Scc:
      {max#(N(L(x), N(y, z))) -> max#(N(y, z))}
     SCC:
      Strict:
       {max#(N(L(s(x)), L(s(y)))) -> max#(N(L(x), L(y)))}
      Weak:
      {               max(L(x)) -> x,
          max(N(L(x), N(y, z))) -> max(N(L(x), L(max(N(y, z))))),
       max(N(L(s(x)), L(s(y)))) -> s(max(N(L(x), L(y))))}
      POLY:
       Argument Filtering:
        pi(s) = [0], pi(N) = 1, pi(L) = 0, pi(max#) = 0, pi(max) = []
       Usable Rules:
        {}
       Interpretation:
        [s](x0) = x0 + 1
       Strict:
        {}
       Weak:
        {               max(L(x)) -> x,
            max(N(L(x), N(y, z))) -> max(N(L(x), L(max(N(y, z))))),
         max(N(L(s(x)), L(s(y)))) -> s(max(N(L(x), L(y))))}
       Qed
     SCC:
      Strict:
       {max#(N(L(x), N(y, z))) -> max#(N(y, z))}
      Weak:
      {               max(L(x)) -> x,
          max(N(L(x), N(y, z))) -> max(N(L(x), L(max(N(y, z))))),
       max(N(L(s(x)), L(s(y)))) -> s(max(N(L(x), L(y))))}
      SPSC:
       Simple Projection:
        pi(max#) = 0
       Strict:
        {}
       Qed