YES(?,O(n^1))

Problem:
 max(L(x)) -> x
 max(N(L(0()),L(y))) -> y
 max(N(L(s(x)),L(s(y)))) -> s(max(N(L(x),L(y))))
 max(N(L(x),N(y,z))) -> max(N(L(x),L(max(N(y,z)))))

Proof:
 RT Transformation Processor:
  strict:
   max(L(x)) -> x
   max(N(L(0()),L(y))) -> y
   max(N(L(s(x)),L(s(y)))) -> s(max(N(L(x),L(y))))
   max(N(L(x),N(y,z))) -> max(N(L(x),L(max(N(y,z)))))
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   interpretation:
    [s](x0) = x0 + 12,
    
    [N](x0, x1) = x0 + x1 + 4,
    
    [0] = 8,
    
    [max](x0) = x0 + 10,
    
    [L](x0) = x0 + 4
   orientation:
    max(L(x)) = x + 14 >= x = x
    
    max(N(L(0()),L(y))) = y + 30 >= y = y
    
    max(N(L(s(x)),L(s(y)))) = x + y + 46 >= x + y + 34 = s(max(N(L(x),L(y))))
    
    max(N(L(x),N(y,z))) = x + y + z + 22 >= x + y + z + 36 = max(N(L(x),L(max(N(y,z)))))
   problem:
    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(0()),L(y))) -> y
     max(N(L(s(x)),L(s(y)))) -> s(max(N(L(x),L(y))))
   Bounds Processor:
    bound: 1
    enrichment: match-rt
    automaton:
     final states: {6,7}
     transitions:
      max1(17) -> 14,6
      max1(13) -> 14*
      N1(6,6) -> 13*
      N1(7,7) -> 13*
      N1(6,7) -> 13*
      N1(16,15) -> 17*
      N1(7,6) -> 13*
      L1(7) -> 16*
      L1(14) -> 15*
      L1(6) -> 16*
      s1(6) -> 14*
      max0(7) -> 6*
      max0(6) -> 6*
      N0(6,6) -> 6*
      N0(7,7) -> 6*
      N0(6,7) -> 6*
      N0(7,6) -> 6*
      L0(7) -> 6*
      L0(6) -> 6*
      00() -> 7*
      s0(7) -> 6*
      s0(6) -> 6*
      6 -> 14*
      7 -> 14,6
      14 -> 6*
    problem:
     strict:
      
     weak:
      max(N(L(x),N(y,z))) -> max(N(L(x),L(max(N(y,z)))))
      max(L(x)) -> x
      max(N(L(0()),L(y))) -> y
      max(N(L(s(x)),L(s(y)))) -> s(max(N(L(x),L(y))))
    Qed