YES
Time: 0.010226
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:
   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 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 (2):
     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 (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 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,
        
        [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:
        
      Qed
    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 s x, L s y) -> s max N(L x, L y)}
     SPSC:
      Simple Projection:
       pi(max#) = 0
      Strict:
       {}
      Qed