YES
Time: 0.161046
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)}
  UR:
   {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 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 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 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 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(L x, L 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))}
    STATUS:
     arrows: 0.000000
     SCCS (1):
      Scc:
       {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)}
      
      SCC (3):
       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 0(), L y) -> y,
        max N(L s x, L s y) -> s max N(L x, L y)}
       POLY:
        Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
        Interpretation:
         [N](x0, x1) = x0,
         
         [max](x0) = x0,
         
         [L](x0) = x0,
         
         [s](x0) = x0 + 1,
         
         [0] = 0,
         
         [max#](x0) = x0
        Strict:
         max# N(L s x, L s y) -> max# N(L x, L y)
         1 + 0x + 1y >= 0 + 0x + 1y
         max# N(L x, N(y, z)) -> max# N(L x, L max N(y, z))
         0 + 0x + 0y + 1z >= 0 + 0x + 0y + 1z
         max# N(L x, N(y, z)) -> max# N(y, z)
         0 + 0x + 0y + 1z >= 0 + 0y + 1z
        Weak:
         max N(L s x, L s y) -> s max N(L x, L y)
         1 + 0x + 1y >= 1 + 0x + 1y
         max N(L 0(), L y) -> y
         0 + 1y >= 1y
         max N(L x, N(y, z)) -> max N(L x, L max N(y, z))
         0 + 0x + 0y + 1z >= 0 + 0x + 0y + 1z
         max L x -> x
         0 + 1x >= 1x
       SCCS (1):
        Scc:
         {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 (2):
         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))}
         Weak:
         {            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)}
         POLY:
          Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
          Interpretation:
           [N](x0, x1) = x0 + x1 + 1,
           
           [max](x0) = 0,
           
           [L](x0) = 1,
           
           [s](x0) = 0,
           
           [0] = 0,
           
           [max#](x0) = x0 + 1
          Strict:
           max# N(L x, N(y, z)) -> max# N(L x, L max N(y, z))
           4 + 0x + 1y + 1z >= 4 + 0x + 0y + 0z
           max# N(L x, N(y, z)) -> max# N(y, z)
           4 + 0x + 1y + 1z >= 2 + 1y + 1z
          Weak:
           max N(L s x, L s y) -> s max N(L x, L y)
           0 + 0x + 0y >= 0 + 0x + 0y
           max N(L 0(), L y) -> y
           0 + 0y >= 1y
           max N(L x, N(y, z)) -> max N(L x, L max N(y, z))
           0 + 0x + 0y + 0z >= 0 + 0x + 0y + 0z
           max L x -> x
           0 + 0x >= 1x
         SCCS (1):
          Scc:
           {max# N(L x, N(y, z)) -> max# N(L x, L max N(y, z))}
          
          SCC (1):
           Strict:
            {max# N(L x, N(y, z)) -> max# N(L x, L 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 0(), L y) -> y,
            max N(L s x, L s y) -> s max N(L x, L y)}
           POLY:
            Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
            Interpretation:
             [N](x0, x1) = x0 + 1,
             
             [max](x0) = 0,
             
             [L](x0) = 0,
             
             [s](x0) = 0,
             
             [0] = 0,
             
             [max#](x0) = x0
            Strict:
             max# N(L x, N(y, z)) -> max# N(L x, L max N(y, z))
             2 + 0x + 0y + 1z >= 1 + 0x + 0y + 0z
            Weak:
             max N(L s x, L s y) -> s max N(L x, L y)
             0 + 0x + 0y >= 0 + 0x + 0y
             max N(L 0(), L y) -> y
             0 + 0y >= 1y
             max N(L x, N(y, z)) -> max N(L x, L max N(y, z))
             0 + 0x + 0y + 0z >= 0 + 0x + 0y + 0z
             max L x -> x
             0 + 0x >= 1x
           Qed