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:
 Complexity 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
   max_matrix:
    1
    interpretation:
     [s](x0) = x0 + 9,
     
     [N](x0, x1) = x0 + x1,
     
     [0] = 6,
     
     [max](x0) = x0 + 2,
     
     [L](x0) = x0 + 3
    orientation:
     max(L(x)) = x + 5 >= x = x
     
     max(N(L(0()),L(y))) = y + 14 >= y = y
     
     max(N(L(s(x)),L(s(y)))) = x + y + 26 >= x + y + 17 = s(max(N(L(x),L(y))))
     
     max(N(L(x),N(y,z))) = x + y + z + 5 >= x + y + z + 10 = 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
     automaton:
      final states: {5}
      transitions:
       max1(10) -> 7,5
       max1(6) -> 7*
       N1(3,1) -> 6*
       N1(3,3) -> 6*
       N1(8,17) -> 6*
       N1(4,2) -> 6*
       N1(4,4) -> 6*
       N1(9,8) -> 10*
       N1(1,2) -> 6*
       N1(1,4) -> 6*
       N1(2,1) -> 6*
       N1(2,3) -> 6*
       N1(3,2) -> 6*
       N1(3,4) -> 6*
       N1(4,1) -> 6*
       N1(4,3) -> 6*
       N1(1,1) -> 6*
       N1(1,3) -> 6*
       N1(2,2) -> 6*
       N1(2,4) -> 6*
       L1(5) -> 17*
       L1(7) -> 8*
       L1(2) -> 9*
       L1(4) -> 9*
       L1(1) -> 9*
       L1(3) -> 9*
       s1(5) -> 7*
       max0(2) -> 5*
       max0(4) -> 5*
       max0(1) -> 5*
       max0(3) -> 5*
       N0(3,1) -> 1*
       N0(3,3) -> 1*
       N0(4,2) -> 1*
       N0(4,4) -> 1*
       N0(1,2) -> 1*
       N0(1,4) -> 1*
       N0(2,1) -> 1*
       N0(2,3) -> 1*
       N0(3,2) -> 1*
       N0(3,4) -> 1*
       N0(4,1) -> 1*
       N0(4,3) -> 1*
       N0(1,1) -> 1*
       N0(1,3) -> 1*
       N0(2,2) -> 1*
       N0(2,4) -> 1*
       L0(2) -> 2*
       L0(4) -> 2*
       L0(1) -> 2*
       L0(3) -> 2*
       00() -> 3*
       s0(5) -> 5*
       s0(2) -> 4*
       s0(4) -> 4*
       s0(1) -> 4*
       s0(3) -> 4*
       1 -> 7,5
       2 -> 7,5
       3 -> 7,5
       4 -> 7,5
       5 -> 7*
       7 -> 5*
     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