YES(?,O(n^1))
12.67/3.45	YES(?,O(n^1))
12.67/3.46	
12.67/3.46	Problem:
12.67/3.46	 max(L(x)) -> x
12.67/3.46	 max(N(L(0()),L(y))) -> y
12.67/3.46	 max(N(L(s(x)),L(s(y)))) -> s(max(N(L(x),L(y))))
12.67/3.46	 max(N(L(x),N(y,z))) -> max(N(L(x),L(max(N(y,z)))))
12.67/3.46	
12.67/3.46	Proof:
12.67/3.46	 Complexity Transformation Processor:
12.67/3.46	  strict:
12.67/3.46	   max(L(x)) -> x
12.67/3.46	   max(N(L(0()),L(y))) -> y
12.67/3.46	   max(N(L(s(x)),L(s(y)))) -> s(max(N(L(x),L(y))))
12.67/3.46	   max(N(L(x),N(y,z))) -> max(N(L(x),L(max(N(y,z)))))
12.67/3.46	  weak:
12.67/3.46	   
12.67/3.46	  Matrix Interpretation Processor: dim=1
12.67/3.46	   
12.67/3.46	   max_matrix:
12.67/3.46	    1
12.67/3.46	   interpretation:
12.67/3.46	    [s](x0) = x0 + 7,
12.67/3.46	    
12.67/3.46	    [N](x0, x1) = x0 + x1 + 1,
12.67/3.46	    
12.67/3.46	    [0] = 0,
12.67/3.46	    
12.67/3.46	    [max](x0) = x0,
12.67/3.46	    
12.67/3.46	    [L](x0) = x0
12.67/3.46	   orientation:
12.67/3.46	    max(L(x)) = x >= x = x
12.67/3.46	    
12.67/3.46	    max(N(L(0()),L(y))) = y + 1 >= y = y
12.67/3.46	    
12.67/3.46	    max(N(L(s(x)),L(s(y)))) = x + y + 15 >= x + y + 8 = s(max(N(L(x),L(y))))
12.67/3.46	    
12.67/3.46	    max(N(L(x),N(y,z))) = x + y + z + 2 >= x + y + z + 2 = max(N(L(x),L(max(N(y,z)))))
12.67/3.46	   problem:
12.67/3.46	    strict:
12.67/3.46	     max(L(x)) -> x
12.67/3.46	     max(N(L(x),N(y,z))) -> max(N(L(x),L(max(N(y,z)))))
12.67/3.46	    weak:
12.67/3.46	     max(N(L(0()),L(y))) -> y
12.67/3.46	     max(N(L(s(x)),L(s(y)))) -> s(max(N(L(x),L(y))))
12.67/3.46	   Matrix Interpretation Processor: dim=1
12.67/3.46	    
12.67/3.46	    max_matrix:
12.67/3.46	     1
12.67/3.46	    interpretation:
12.67/3.46	     [s](x0) = x0 + 3,
12.67/3.46	     
12.67/3.46	     [N](x0, x1) = x0 + x1,
12.67/3.46	     
12.67/3.46	     [0] = 3,
12.67/3.46	     
12.67/3.46	     [max](x0) = x0,
12.67/3.46	     
12.67/3.46	     [L](x0) = x0 + 10
12.67/3.46	    orientation:
12.67/3.46	     max(L(x)) = x + 10 >= x = x
12.67/3.46	     
12.67/3.46	     max(N(L(x),N(y,z))) = x + y + z + 10 >= x + y + z + 20 = max(N(L(x),L(max(N(y,z)))))
12.67/3.46	     
12.67/3.46	     max(N(L(0()),L(y))) = y + 23 >= y = y
12.67/3.46	     
12.67/3.46	     max(N(L(s(x)),L(s(y)))) = x + y + 26 >= x + y + 23 = s(max(N(L(x),L(y))))
12.67/3.46	    problem:
12.67/3.46	     strict:
12.67/3.46	      max(N(L(x),N(y,z))) -> max(N(L(x),L(max(N(y,z)))))
12.67/3.46	     weak:
12.67/3.46	      max(L(x)) -> x
12.67/3.46	      max(N(L(0()),L(y))) -> y
12.67/3.46	      max(N(L(s(x)),L(s(y)))) -> s(max(N(L(x),L(y))))
12.67/3.46	    Bounds Processor:
12.67/3.46	     bound: 1
12.67/3.46	     enrichment: match
12.67/3.46	     automaton:
12.67/3.46	      final states: {5}
12.67/3.46	      transitions:
12.67/3.46	       max1(10) -> 7,5
12.67/3.46	       max1(6) -> 7*
12.67/3.46	       N1(3,1) -> 6*
12.67/3.46	       N1(3,3) -> 6*
12.67/3.46	       N1(8,17) -> 6*
12.67/3.46	       N1(4,2) -> 6*
12.67/3.46	       N1(4,4) -> 6*
12.67/3.46	       N1(9,8) -> 10*
12.67/3.46	       N1(1,2) -> 6*
12.67/3.46	       N1(1,4) -> 6*
12.67/3.46	       N1(2,1) -> 6*
12.67/3.46	       N1(2,3) -> 6*
12.67/3.46	       N1(3,2) -> 6*
12.67/3.46	       N1(3,4) -> 6*
12.67/3.46	       N1(4,1) -> 6*
12.67/3.46	       N1(4,3) -> 6*
12.67/3.46	       N1(1,1) -> 6*
12.67/3.46	       N1(1,3) -> 6*
12.67/3.46	       N1(2,2) -> 6*
12.67/3.46	       N1(2,4) -> 6*
12.67/3.46	       L1(5) -> 17*
12.67/3.46	       L1(7) -> 8*
12.67/3.46	       L1(2) -> 9*
12.67/3.46	       L1(4) -> 9*
12.67/3.46	       L1(1) -> 9*
12.67/3.46	       L1(3) -> 9*
12.67/3.46	       s1(5) -> 7*
12.67/3.46	       max0(2) -> 5*
12.67/3.46	       max0(4) -> 5*
12.67/3.46	       max0(1) -> 5*
12.67/3.46	       max0(3) -> 5*
12.67/3.46	       N0(3,1) -> 1*
12.67/3.46	       N0(3,3) -> 1*
12.67/3.46	       N0(4,2) -> 1*
12.67/3.46	       N0(4,4) -> 1*
12.67/3.46	       N0(1,2) -> 1*
12.67/3.46	       N0(1,4) -> 1*
12.67/3.46	       N0(2,1) -> 1*
12.67/3.46	       N0(2,3) -> 1*
12.67/3.46	       N0(3,2) -> 1*
12.67/3.46	       N0(3,4) -> 1*
12.67/3.46	       N0(4,1) -> 1*
12.67/3.46	       N0(4,3) -> 1*
12.67/3.46	       N0(1,1) -> 1*
12.67/3.46	       N0(1,3) -> 1*
12.67/3.46	       N0(2,2) -> 1*
12.67/3.46	       N0(2,4) -> 1*
12.67/3.46	       L0(2) -> 2*
12.67/3.46	       L0(4) -> 2*
12.67/3.46	       L0(1) -> 2*
12.67/3.46	       L0(3) -> 2*
12.67/3.46	       00() -> 3*
12.67/3.46	       s0(5) -> 5*
12.67/3.46	       s0(2) -> 4*
12.67/3.46	       s0(4) -> 4*
12.67/3.46	       s0(1) -> 4*
12.67/3.46	       s0(3) -> 4*
12.67/3.46	       1 -> 7,5
12.67/3.46	       2 -> 7,5
12.67/3.46	       3 -> 7,5
12.67/3.46	       4 -> 7,5
12.67/3.46	       5 -> 7*
12.67/3.46	       7 -> 5*
12.67/3.46	     problem:
12.67/3.46	      strict:
12.67/3.46	       
12.67/3.46	      weak:
12.67/3.46	       max(N(L(x),N(y,z))) -> max(N(L(x),L(max(N(y,z)))))
12.67/3.46	       max(L(x)) -> x
12.67/3.46	       max(N(L(0()),L(y))) -> y
12.67/3.46	       max(N(L(s(x)),L(s(y)))) -> s(max(N(L(x),L(y))))
12.67/3.46	     Qed
12.67/3.46	EOF