YES(?,O(n^2))
728.56/295.18	YES(?,O(n^2))
728.56/295.18	
728.56/295.18	Problem:
728.56/295.18	 a(a(x)) -> b(b(x))
728.56/295.18	 b(b(a(x))) -> a(b(b(x)))
728.56/295.18	
728.56/295.18	Proof:
728.56/295.18	 Complexity Transformation Processor:
728.56/295.18	  strict:
728.56/295.18	   a(a(x)) -> b(b(x))
728.56/295.18	   b(b(a(x))) -> a(b(b(x)))
728.56/295.18	  weak:
728.56/295.18	   
728.56/295.18	  Matrix Interpretation Processor: dim=1
728.56/295.18	   
728.56/295.18	   max_matrix:
728.56/295.18	    1
728.56/295.18	   interpretation:
728.56/295.18	    [b](x0) = x0,
728.56/295.18	    
728.56/295.18	    [a](x0) = x0 + 5
728.56/295.18	   orientation:
728.56/295.18	    a(a(x)) = x + 10 >= x = b(b(x))
728.56/295.18	    
728.56/295.18	    b(b(a(x))) = x + 5 >= x + 5 = a(b(b(x)))
728.56/295.18	   problem:
728.56/295.18	    strict:
728.56/295.18	     b(b(a(x))) -> a(b(b(x)))
728.56/295.18	    weak:
728.56/295.18	     a(a(x)) -> b(b(x))
728.56/295.18	   Matrix Interpretation Processor: dim=2
728.56/295.18	    
728.56/295.18	    max_matrix:
728.56/295.18	     [1 2]
728.56/295.18	     [0 1]
728.56/295.18	    interpretation:
728.56/295.18	               [1 1]     [0]
728.56/295.18	     [b](x0) = [0 1]x0 + [1],
728.56/295.18	     
728.56/295.18	               [1 2]     [0]
728.56/295.18	     [a](x0) = [0 1]x0 + [4]
728.56/295.18	    orientation:
728.56/295.18	                  [1 4]    [9]    [1 4]    [5]             
728.56/295.18	     b(b(a(x))) = [0 1]x + [6] >= [0 1]x + [6] = a(b(b(x)))
728.56/295.18	     
728.56/295.18	               [1 4]    [8]    [1 2]    [1]          
728.56/295.18	     a(a(x)) = [0 1]x + [8] >= [0 1]x + [2] = b(b(x))
728.56/295.18	    problem:
728.56/295.18	     strict:
728.56/295.18	      
728.56/295.18	     weak:
728.56/295.18	      b(b(a(x))) -> a(b(b(x)))
728.56/295.18	      a(a(x)) -> b(b(x))
728.56/295.18	    Qed
728.56/295.19	EOF