YES(?,O(n^1))
5.17/1.57	YES(?,O(n^1))
5.17/1.58	
5.17/1.58	Problem:
5.17/1.58	 a(a(a(x1))) -> b(x1)
5.17/1.58	 b(b(x1)) -> b(a(b(x1)))
5.17/1.58	 b(b(x1)) -> a(a(x1))
5.17/1.58	
5.17/1.58	Proof:
5.17/1.58	 Complexity Transformation Processor:
5.17/1.58	  strict:
5.17/1.58	   a(a(a(x1))) -> b(x1)
5.17/1.58	   b(b(x1)) -> b(a(b(x1)))
5.17/1.58	   b(b(x1)) -> a(a(x1))
5.17/1.58	  weak:
5.17/1.58	   
5.17/1.58	  Matrix Interpretation Processor: dim=1
5.17/1.58	   
5.17/1.58	   max_matrix:
5.17/1.58	    1
5.17/1.58	   interpretation:
5.17/1.58	    [b](x0) = x0 + 64,
5.17/1.58	    
5.17/1.58	    [a](x0) = x0 + 128
5.17/1.58	   orientation:
5.17/1.58	    a(a(a(x1))) = x1 + 384 >= x1 + 64 = b(x1)
5.17/1.58	    
5.17/1.58	    b(b(x1)) = x1 + 128 >= x1 + 256 = b(a(b(x1)))
5.17/1.58	    
5.17/1.58	    b(b(x1)) = x1 + 128 >= x1 + 256 = a(a(x1))
5.17/1.58	   problem:
5.17/1.58	    strict:
5.17/1.58	     b(b(x1)) -> b(a(b(x1)))
5.17/1.58	     b(b(x1)) -> a(a(x1))
5.17/1.58	    weak:
5.17/1.58	     a(a(a(x1))) -> b(x1)
5.17/1.58	   Matrix Interpretation Processor: dim=1
5.17/1.58	    
5.17/1.58	    max_matrix:
5.17/1.58	     1
5.17/1.58	    interpretation:
5.17/1.58	     [b](x0) = x0 + 54,
5.17/1.58	     
5.17/1.58	     [a](x0) = x0 + 21
5.17/1.58	    orientation:
5.17/1.58	     b(b(x1)) = x1 + 108 >= x1 + 129 = b(a(b(x1)))
5.17/1.58	     
5.17/1.58	     b(b(x1)) = x1 + 108 >= x1 + 42 = a(a(x1))
5.17/1.58	     
5.17/1.58	     a(a(a(x1))) = x1 + 63 >= x1 + 54 = b(x1)
5.17/1.58	    problem:
5.17/1.58	     strict:
5.17/1.58	      b(b(x1)) -> b(a(b(x1)))
5.17/1.58	     weak:
5.17/1.58	      b(b(x1)) -> a(a(x1))
5.17/1.58	      a(a(a(x1))) -> b(x1)
5.17/1.58	    Arctic Interpretation Processor:
5.17/1.58	     dimension: 2
5.17/1.58	     interpretation:
5.17/1.58	                [0 2]  
5.17/1.58	      [b](x0) = [2 4]x0,
5.17/1.58	      
5.17/1.58	                [2  1 ]  
5.17/1.58	      [a](x0) = [1  -&]x0
5.17/1.58	     orientation:
5.17/1.58	                 [4 6]      [3 5]                
5.17/1.58	      b(b(x1)) = [6 8]x1 >= [5 7]x1 = b(a(b(x1)))
5.17/1.58	      
5.17/1.58	                 [4 6]      [4 3]             
5.17/1.58	      b(b(x1)) = [6 8]x1 >= [3 2]x1 = a(a(x1))
5.17/1.58	      
5.17/1.58	                    [6 5]      [0 2]          
5.17/1.58	      a(a(a(x1))) = [5 4]x1 >= [2 4]x1 = b(x1)
5.17/1.58	     problem:
5.17/1.58	      strict:
5.17/1.58	       
5.17/1.58	      weak:
5.17/1.58	       b(b(x1)) -> b(a(b(x1)))
5.17/1.58	       b(b(x1)) -> a(a(x1))
5.17/1.58	       a(a(a(x1))) -> b(x1)
5.17/1.58	     Qed
5.17/1.58	EOF