YES
Time: 0.135656
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 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))}
    STATUS:
     arrows: 0.444444
     SCCS (2):
      Scc:
       {max# N(L x, N(y, z)) -> max# N(y, z)}
      Scc:
       {max# N(L s x, L s y) -> max# N(L x, L y)}
      
      SCC (1):
       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 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,
         
         [max](x0) = x0 + 1,
         
         [L](x0) = x0 + 1,
         
         [s](x0) = x0,
         
         [0] = 1,
         
         [max#](x0) = x0
        Strict:
         max# N(L x, N(y, z)) -> max# N(y, z)
         1 + 1x + 1y + 1z >= 0 + 1y + 1z
        Weak:
         max N(L s x, L s y) -> s max N(L x, L y)
         3 + 1x + 1y >= 3 + 1x + 1y
         max N(L 0(), L y) -> y
         4 + 1y >= 1y
         max N(L x, N(y, z)) -> max N(L x, L max N(y, z))
         2 + 1x + 1y + 1z >= 4 + 1x + 1y + 1z
         max L x -> x
         2 + 1x >= 1x
       Qed
     
     SCC (1):
      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 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) = 0,
        
        [L](x0) = x0 + 1,
        
        [s](x0) = x0 + 1,
        
        [0] = 1,
        
        [max#](x0) = x0
       Strict:
        max# N(L s x, L s y) -> max# N(L x, L y)
        2 + 0x + 1y >= 1 + 0x + 1y
       Weak:
        max N(L s x, L s y) -> s max N(L x, L y)
        0 + 0x + 0y >= 1 + 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