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