YES(?,O(n^1))
3.99/1.38	YES(?,O(n^1))
3.99/1.38	
3.99/1.38	Problem:
3.99/1.38	 a(b(a(x1))) -> b(a(x1))
3.99/1.38	 b(b(b(x1))) -> b(a(b(x1)))
3.99/1.38	 a(a(x1)) -> b(b(b(x1)))
3.99/1.38	
3.99/1.38	Proof:
3.99/1.38	 Complexity Transformation Processor:
3.99/1.38	  strict:
3.99/1.38	   a(b(a(x1))) -> b(a(x1))
3.99/1.38	   b(b(b(x1))) -> b(a(b(x1)))
3.99/1.38	   a(a(x1)) -> b(b(b(x1)))
3.99/1.38	  weak:
3.99/1.38	   
3.99/1.38	  Matrix Interpretation Processor: dim=1
3.99/1.38	   
3.99/1.38	   max_matrix:
3.99/1.38	    1
3.99/1.38	   interpretation:
3.99/1.38	    [b](x0) = x0 + 138,
3.99/1.38	    
3.99/1.38	    [a](x0) = x0 + 23
3.99/1.38	   orientation:
3.99/1.38	    a(b(a(x1))) = x1 + 184 >= x1 + 161 = b(a(x1))
3.99/1.38	    
3.99/1.38	    b(b(b(x1))) = x1 + 414 >= x1 + 299 = b(a(b(x1)))
3.99/1.38	    
3.99/1.38	    a(a(x1)) = x1 + 46 >= x1 + 414 = b(b(b(x1)))
3.99/1.38	   problem:
3.99/1.38	    strict:
3.99/1.38	     a(a(x1)) -> b(b(b(x1)))
3.99/1.38	    weak:
3.99/1.38	     a(b(a(x1))) -> b(a(x1))
3.99/1.38	     b(b(b(x1))) -> b(a(b(x1)))
3.99/1.38	   Matrix Interpretation Processor: dim=4
3.99/1.38	    
3.99/1.38	    max_matrix:
3.99/1.38	     [1 1 1 0]
3.99/1.38	     [0 0 1 1]
3.99/1.38	     [0 0 0 1]
3.99/1.38	     [0 0 0 0]
3.99/1.38	    interpretation:
3.99/1.38	               [1 0 1 0]     [0]
3.99/1.38	               [0 0 0 0]     [0]
3.99/1.38	     [b](x0) = [0 0 0 0]x0 + [1]
3.99/1.38	               [0 0 0 0]     [0],
3.99/1.38	     
3.99/1.38	               [1 1 0 0]     [1]
3.99/1.38	               [0 0 1 1]     [1]
3.99/1.38	     [a](x0) = [0 0 0 1]x0 + [1]
3.99/1.38	               [0 0 0 0]     [1]
3.99/1.38	    orientation:
3.99/1.38	                [1 1 1 1]     [3]    [1 0 1 0]     [2]              
3.99/1.38	                [0 0 0 1]     [3]    [0 0 0 0]     [0]              
3.99/1.38	     a(a(x1)) = [0 0 0 0]x1 + [2] >= [0 0 0 0]x1 + [1] = b(b(b(x1)))
3.99/1.38	                [0 0 0 0]     [1]    [0 0 0 0]     [0]              
3.99/1.38	     
3.99/1.38	                   [1 1 0 1]     [3]    [1 1 0 1]     [2]           
3.99/1.38	                   [0 0 0 0]     [2]    [0 0 0 0]     [0]           
3.99/1.38	     a(b(a(x1))) = [0 0 0 0]x1 + [1] >= [0 0 0 0]x1 + [1] = b(a(x1))
3.99/1.38	                   [0 0 0 0]     [1]    [0 0 0 0]     [0]           
3.99/1.38	     
3.99/1.38	                   [1 0 1 0]     [2]    [1 0 1 0]     [2]              
3.99/1.38	                   [0 0 0 0]     [0]    [0 0 0 0]     [0]              
3.99/1.38	     b(b(b(x1))) = [0 0 0 0]x1 + [1] >= [0 0 0 0]x1 + [1] = b(a(b(x1)))
3.99/1.38	                   [0 0 0 0]     [0]    [0 0 0 0]     [0]              
3.99/1.38	    problem:
3.99/1.38	     strict:
3.99/1.38	      
3.99/1.38	     weak:
3.99/1.38	      a(a(x1)) -> b(b(b(x1)))
3.99/1.38	      a(b(a(x1))) -> b(a(x1))
3.99/1.38	      b(b(b(x1))) -> b(a(b(x1)))
3.99/1.38	    Qed
3.99/1.39	EOF