YES(?,O(n^1))
3.18/1.16	YES(?,O(n^1))
3.18/1.16	
3.18/1.16	Problem:
3.18/1.16	 a(b(a(x1))) -> a(b(b(a(x1))))
3.18/1.16	 b(b(b(x1))) -> b(b(x1))
3.18/1.16	
3.18/1.16	Proof:
3.18/1.16	 Complexity Transformation Processor:
3.18/1.16	  strict:
3.18/1.16	   a(b(a(x1))) -> a(b(b(a(x1))))
3.18/1.16	   b(b(b(x1))) -> b(b(x1))
3.18/1.16	  weak:
3.18/1.16	   
3.18/1.16	  Matrix Interpretation Processor: dim=1
3.18/1.16	   
3.18/1.16	   max_matrix:
3.18/1.16	    1
3.18/1.16	   interpretation:
3.18/1.16	    [b](x0) = x0 + 1,
3.18/1.16	    
3.18/1.16	    [a](x0) = x0 + 2
3.18/1.16	   orientation:
3.18/1.16	    a(b(a(x1))) = x1 + 5 >= x1 + 6 = a(b(b(a(x1))))
3.18/1.16	    
3.18/1.16	    b(b(b(x1))) = x1 + 3 >= x1 + 2 = b(b(x1))
3.18/1.16	   problem:
3.18/1.16	    strict:
3.18/1.16	     a(b(a(x1))) -> a(b(b(a(x1))))
3.18/1.16	    weak:
3.18/1.16	     b(b(b(x1))) -> b(b(x1))
3.18/1.16	   Matrix Interpretation Processor: dim=4
3.18/1.16	    
3.18/1.16	    max_matrix:
3.18/1.16	     [1 1 1 1]
3.18/1.16	     [0 0 1 1]
3.18/1.16	     [0 0 0 1]
3.18/1.16	     [0 0 0 0]
3.18/1.16	    interpretation:
3.18/1.16	               [1 1 0 1]  
3.18/1.16	               [0 0 0 0]  
3.18/1.16	     [b](x0) = [0 0 0 1]x0
3.18/1.16	               [0 0 0 0]  ,
3.18/1.16	     
3.18/1.16	               [1 0 1 0]     [0]
3.18/1.16	               [0 0 1 1]     [1]
3.18/1.16	     [a](x0) = [0 0 0 0]x0 + [0]
3.18/1.16	               [0 0 0 0]     [1]
3.18/1.16	    orientation:
3.18/1.16	                   [1 0 2 1]     [3]    [1 0 2 1]     [2]                 
3.18/1.16	                   [0 0 0 0]     [2]    [0 0 0 0]     [1]                 
3.18/1.16	     a(b(a(x1))) = [0 0 0 0]x1 + [0] >= [0 0 0 0]x1 + [0] = a(b(b(a(x1))))
3.18/1.16	                   [0 0 0 0]     [1]    [0 0 0 0]     [1]                 
3.18/1.16	     
3.18/1.16	                   [1 1 0 1]      [1 1 0 1]             
3.18/1.16	                   [0 0 0 0]      [0 0 0 0]             
3.18/1.16	     b(b(b(x1))) = [0 0 0 0]x1 >= [0 0 0 0]x1 = b(b(x1))
3.18/1.16	                   [0 0 0 0]      [0 0 0 0]             
3.18/1.16	    problem:
3.18/1.16	     strict:
3.18/1.16	      
3.18/1.16	     weak:
3.18/1.16	      a(b(a(x1))) -> a(b(b(a(x1))))
3.18/1.16	      b(b(b(x1))) -> b(b(x1))
3.18/1.16	    Qed
3.18/1.17	EOF