YES(?,O(n^1))
5.64/1.62	YES(?,O(n^1))
5.64/1.62	
5.64/1.62	Problem:
5.64/1.62	 b(b(x1)) -> c(c(c(c(x1))))
5.64/1.62	 c(x1) -> x1
5.64/1.62	 b(c(b(x1))) -> b(b(b(x1)))
5.64/1.62	
5.64/1.62	Proof:
5.64/1.62	 Complexity Transformation Processor:
5.64/1.62	  strict:
5.64/1.62	   b(b(x1)) -> c(c(c(c(x1))))
5.64/1.62	   c(x1) -> x1
5.64/1.62	   b(c(b(x1))) -> b(b(b(x1)))
5.64/1.62	  weak:
5.64/1.62	   
5.64/1.62	  Matrix Interpretation Processor: dim=1
5.64/1.62	   
5.64/1.62	   max_matrix:
5.64/1.62	    1
5.64/1.62	   interpretation:
5.64/1.62	    [c](x0) = x0 + 34,
5.64/1.62	    
5.64/1.62	    [b](x0) = x0 + 4
5.64/1.62	   orientation:
5.64/1.62	    b(b(x1)) = x1 + 8 >= x1 + 136 = c(c(c(c(x1))))
5.64/1.62	    
5.64/1.62	    c(x1) = x1 + 34 >= x1 = x1
5.64/1.62	    
5.64/1.62	    b(c(b(x1))) = x1 + 42 >= x1 + 12 = b(b(b(x1)))
5.64/1.62	   problem:
5.64/1.62	    strict:
5.64/1.62	     b(b(x1)) -> c(c(c(c(x1))))
5.64/1.62	    weak:
5.64/1.62	     c(x1) -> x1
5.64/1.62	     b(c(b(x1))) -> b(b(b(x1)))
5.64/1.62	   Arctic Interpretation Processor:
5.64/1.62	    dimension: 2
5.64/1.62	    interpretation:
5.64/1.62	               [0  3 ]  
5.64/1.62	     [c](x0) = [-& 0 ]x0,
5.64/1.62	     
5.64/1.62	               [2 3]  
5.64/1.62	     [b](x0) = [1 2]x0
5.64/1.62	    orientation:
5.64/1.62	                [4 5]      [0  3 ]                   
5.64/1.62	     b(b(x1)) = [3 4]x1 >= [-& 0 ]x1 = c(c(c(c(x1))))
5.64/1.62	     
5.64/1.62	             [0  3 ]             
5.64/1.62	     c(x1) = [-& 0 ]x1 >= x1 = x1
5.64/1.62	     
5.64/1.62	                   [6 7]      [6 7]                
5.64/1.62	     b(c(b(x1))) = [5 6]x1 >= [5 6]x1 = b(b(b(x1)))
5.64/1.62	    problem:
5.64/1.62	     strict:
5.64/1.62	      
5.64/1.62	     weak:
5.64/1.62	      b(b(x1)) -> c(c(c(c(x1))))
5.64/1.62	      c(x1) -> x1
5.64/1.62	      b(c(b(x1))) -> b(b(b(x1)))
5.64/1.62	    Qed
5.64/1.63	EOF