YES(?,O(n^2))
34.81/12.17	YES(?,O(n^2))
34.81/12.17	
34.81/12.17	Problem:
34.81/12.17	 b(a(x1)) -> a(b(x1))
34.81/12.17	 a(a(a(x1))) -> b(a(a(b(x1))))
34.81/12.17	 b(b(b(b(x1)))) -> a(x1)
34.81/12.17	
34.81/12.17	Proof:
34.81/12.17	 Complexity Transformation Processor:
34.81/12.17	  strict:
34.81/12.17	   b(a(x1)) -> a(b(x1))
34.81/12.17	   a(a(a(x1))) -> b(a(a(b(x1))))
34.81/12.17	   b(b(b(b(x1)))) -> a(x1)
34.81/12.17	  weak:
34.81/12.17	   
34.81/12.17	  Matrix Interpretation Processor: dim=1
34.81/12.17	   
34.81/12.17	   max_matrix:
34.81/12.17	    1
34.81/12.17	   interpretation:
34.81/12.17	    [b](x0) = x0,
34.81/12.17	    
34.81/12.17	    [a](x0) = x0 + 4
34.81/12.17	   orientation:
34.81/12.17	    b(a(x1)) = x1 + 4 >= x1 + 4 = a(b(x1))
34.81/12.17	    
34.81/12.17	    a(a(a(x1))) = x1 + 12 >= x1 + 8 = b(a(a(b(x1))))
34.81/12.17	    
34.81/12.17	    b(b(b(b(x1)))) = x1 >= x1 + 4 = a(x1)
34.81/12.17	   problem:
34.81/12.17	    strict:
34.81/12.17	     b(a(x1)) -> a(b(x1))
34.81/12.17	     b(b(b(b(x1)))) -> a(x1)
34.81/12.17	    weak:
34.81/12.17	     a(a(a(x1))) -> b(a(a(b(x1))))
34.81/12.17	   Matrix Interpretation Processor: dim=1
34.81/12.17	    
34.81/12.17	    max_matrix:
34.81/12.17	     1
34.81/12.17	    interpretation:
34.81/12.17	     [b](x0) = x0 + 4,
34.81/12.17	     
34.81/12.17	     [a](x0) = x0 + 8
34.81/12.17	    orientation:
34.81/12.17	     b(a(x1)) = x1 + 12 >= x1 + 12 = a(b(x1))
34.81/12.17	     
34.81/12.17	     b(b(b(b(x1)))) = x1 + 16 >= x1 + 8 = a(x1)
34.81/12.17	     
34.81/12.17	     a(a(a(x1))) = x1 + 24 >= x1 + 24 = b(a(a(b(x1))))
34.81/12.17	    problem:
34.81/12.17	     strict:
34.81/12.17	      b(a(x1)) -> a(b(x1))
34.81/12.17	     weak:
34.81/12.17	      b(b(b(b(x1)))) -> a(x1)
34.81/12.17	      a(a(a(x1))) -> b(a(a(b(x1))))
34.81/12.17	    Matrix Interpretation Processor: dim=2
34.81/12.17	     
34.81/12.17	     max_matrix:
34.81/12.17	      [1 2]
34.81/12.17	      [0 1]
34.81/12.17	     interpretation:
34.81/12.17	                [1 1]     [0]
34.81/12.17	      [b](x0) = [0 1]x0 + [2],
34.81/12.17	      
34.81/12.17	                [1 2]     [0]
34.81/12.17	      [a](x0) = [0 1]x0 + [5]
34.81/12.17	     orientation:
34.81/12.17	                 [1 3]     [5]    [1 3]     [4]           
34.81/12.17	      b(a(x1)) = [0 1]x1 + [7] >= [0 1]x1 + [7] = a(b(x1))
34.81/12.17	      
34.81/12.17	                       [1 4]     [12]    [1 2]     [0]        
34.81/12.17	      b(b(b(b(x1)))) = [0 1]x1 + [8 ] >= [0 1]x1 + [5] = a(x1)
34.81/12.17	      
34.81/12.17	                    [1 6]     [30]    [1 6]     [30]                 
34.81/12.17	      a(a(a(x1))) = [0 1]x1 + [15] >= [0 1]x1 + [14] = b(a(a(b(x1))))
34.81/12.17	     problem:
34.81/12.17	      strict:
34.81/12.17	       
34.81/12.17	      weak:
34.81/12.17	       b(a(x1)) -> a(b(x1))
34.81/12.17	       b(b(b(b(x1)))) -> a(x1)
34.81/12.17	       a(a(a(x1))) -> b(a(a(b(x1))))
34.81/12.17	     Qed
34.81/12.17	EOF