YES(?,O(n^2))
9.22/6.22	YES(?,O(n^2))
9.22/6.22	
9.22/6.22	Problem:
9.22/6.22	 div(X,e()) -> i(X)
9.22/6.22	 i(div(X,Y)) -> div(Y,X)
9.22/6.22	 div(div(X,Y),Z) -> div(Y,div(i(X),Z))
9.22/6.22	
9.22/6.22	Proof:
9.22/6.22	 Complexity Transformation Processor:
9.22/6.22	  strict:
9.22/6.22	   div(X,e()) -> i(X)
9.22/6.22	   i(div(X,Y)) -> div(Y,X)
9.22/6.22	   div(div(X,Y),Z) -> div(Y,div(i(X),Z))
9.22/6.22	  weak:
9.22/6.22	   
9.22/6.22	  Matrix Interpretation Processor: dim=1
9.22/6.22	   
9.22/6.22	   max_matrix:
9.22/6.22	    1
9.22/6.22	   interpretation:
9.22/6.22	    [i](x0) = x0 + 168,
9.22/6.22	    
9.22/6.22	    [div](x0, x1) = x0 + x1 + 66,
9.22/6.22	    
9.22/6.22	    [e] = 144
9.22/6.22	   orientation:
9.22/6.22	    div(X,e()) = X + 210 >= X + 168 = i(X)
9.22/6.22	    
9.22/6.22	    i(div(X,Y)) = X + Y + 234 >= X + Y + 66 = div(Y,X)
9.22/6.22	    
9.22/6.22	    div(div(X,Y),Z) = X + Y + Z + 132 >= X + Y + Z + 300 = div(Y,div(i(X),Z))
9.22/6.22	   problem:
9.22/6.22	    strict:
9.22/6.22	     div(div(X,Y),Z) -> div(Y,div(i(X),Z))
9.22/6.22	    weak:
9.22/6.22	     div(X,e()) -> i(X)
9.22/6.22	     i(div(X,Y)) -> div(Y,X)
9.22/6.22	   Matrix Interpretation Processor: dim=4
9.22/6.22	    
9.22/6.22	    max_matrix:
9.22/6.22	     [1 0 0 1]
9.22/6.22	     [0 0 0 1]
9.22/6.22	     [0 0 0 1]
9.22/6.22	     [0 0 0 1]
9.22/6.22	    interpretation:
9.22/6.22	               [1 0 0 1]  
9.22/6.22	               [0 0 0 1]  
9.22/6.22	     [i](x0) = [0 0 0 1]x0
9.22/6.22	               [0 0 0 1]  ,
9.22/6.22	     
9.22/6.22	                     [1 0 0 1]     [1 0 0 0]     [0]
9.22/6.22	                     [0 0 0 1]     [0 0 0 1]     [0]
9.22/6.22	     [div](x0, x1) = [0 0 0 1]x0 + [0 0 0 1]x1 + [0]
9.22/6.22	                     [0 0 0 1]     [0 0 0 1]     [1],
9.22/6.22	     
9.22/6.22	           [1]
9.22/6.22	           [0]
9.22/6.22	     [e] = [0]
9.22/6.22	           [0]
9.22/6.22	    orientation:
9.22/6.22	                       [1 0 0 2]    [1 0 0 1]    [1 0 0 0]    [1]    [1 0 0 2]    [1 0 0 1]    [1 0 0 0]    [0]                     
9.22/6.22	                       [0 0 0 1]    [0 0 0 1]    [0 0 0 1]    [1]    [0 0 0 1]    [0 0 0 1]    [0 0 0 1]    [1]                     
9.22/6.22	     div(div(X,Y),Z) = [0 0 0 1]X + [0 0 0 1]Y + [0 0 0 1]Z + [1] >= [0 0 0 1]X + [0 0 0 1]Y + [0 0 0 1]Z + [1] = div(Y,div(i(X),Z))
9.22/6.22	                       [0 0 0 1]    [0 0 0 1]    [0 0 0 1]    [2]    [0 0 0 1]    [0 0 0 1]    [0 0 0 1]    [2]                     
9.22/6.22	     
9.22/6.22	                  [1 0 0 1]    [1]    [1 0 0 1]        
9.22/6.22	                  [0 0 0 1]    [0]    [0 0 0 1]        
9.22/6.22	     div(X,e()) = [0 0 0 1]X + [0] >= [0 0 0 1]X = i(X)
9.22/6.22	                  [0 0 0 1]    [1]    [0 0 0 1]        
9.22/6.22	     
9.22/6.22	                   [1 0 0 2]    [1 0 0 1]    [1]    [1 0 0 0]    [1 0 0 1]    [0]           
9.22/6.22	                   [0 0 0 1]    [0 0 0 1]    [1]    [0 0 0 1]    [0 0 0 1]    [0]           
9.22/6.22	     i(div(X,Y)) = [0 0 0 1]X + [0 0 0 1]Y + [1] >= [0 0 0 1]X + [0 0 0 1]Y + [0] = div(Y,X)
9.22/6.22	                   [0 0 0 1]    [0 0 0 1]    [1]    [0 0 0 1]    [0 0 0 1]    [1]           
9.22/6.22	    problem:
9.22/6.22	     strict:
9.22/6.22	      
9.22/6.22	     weak:
9.22/6.22	      div(div(X,Y),Z) -> div(Y,div(i(X),Z))
9.22/6.22	      div(X,e()) -> i(X)
9.22/6.22	      i(div(X,Y)) -> div(Y,X)
9.22/6.22	    Qed
9.22/6.23	EOF