YES(?,O(n^2))
9.17/6.09	YES(?,O(n^2))
9.17/6.09	
9.17/6.09	Problem:
9.17/6.09	 __(__(X,Y),Z) -> __(X,__(Y,Z))
9.17/6.09	 __(X,nil()) -> X
9.17/6.09	 __(nil(),X) -> X
9.17/6.09	 U11(tt()) -> U12(tt())
9.17/6.09	 U12(tt()) -> tt()
9.17/6.09	 isNePal(__(I,__(P,I))) -> U11(tt())
9.17/6.09	 activate(X) -> X
9.17/6.09	
9.17/6.09	Proof:
9.17/6.09	 Complexity Transformation Processor:
9.17/6.09	  strict:
9.17/6.09	   __(__(X,Y),Z) -> __(X,__(Y,Z))
9.17/6.09	   __(X,nil()) -> X
9.17/6.09	   __(nil(),X) -> X
9.17/6.09	   U11(tt()) -> U12(tt())
9.17/6.09	   U12(tt()) -> tt()
9.17/6.09	   isNePal(__(I,__(P,I))) -> U11(tt())
9.17/6.09	   activate(X) -> X
9.17/6.09	  weak:
9.17/6.09	   
9.17/6.09	  Matrix Interpretation Processor: dim=1
9.17/6.09	   
9.17/6.09	   max_matrix:
9.17/6.09	    1
9.17/6.09	   interpretation:
9.17/6.09	    [activate](x0) = x0 + 1,
9.17/6.09	    
9.17/6.09	    [isNePal](x0) = x0 + 72,
9.17/6.09	    
9.17/6.09	    [U12](x0) = x0 + 207,
9.17/6.09	    
9.17/6.09	    [U11](x0) = x0,
9.17/6.09	    
9.17/6.09	    [tt] = 162,
9.17/6.09	    
9.17/6.09	    [nil] = 9,
9.17/6.09	    
9.17/6.09	    [__](x0, x1) = x0 + x1 + 156
9.17/6.09	   orientation:
9.17/6.09	    __(__(X,Y),Z) = X + Y + Z + 312 >= X + Y + Z + 312 = __(X,__(Y,Z))
9.17/6.09	    
9.17/6.09	    __(X,nil()) = X + 165 >= X = X
9.17/6.09	    
9.17/6.09	    __(nil(),X) = X + 165 >= X = X
9.17/6.09	    
9.17/6.09	    U11(tt()) = 162 >= 369 = U12(tt())
9.17/6.09	    
9.17/6.09	    U12(tt()) = 369 >= 162 = tt()
9.17/6.09	    
9.17/6.09	    isNePal(__(I,__(P,I))) = 2I + P + 384 >= 162 = U11(tt())
9.17/6.09	    
9.17/6.09	    activate(X) = X + 1 >= X = X
9.17/6.09	   problem:
9.17/6.09	    strict:
9.17/6.09	     __(__(X,Y),Z) -> __(X,__(Y,Z))
9.17/6.09	     U11(tt()) -> U12(tt())
9.17/6.09	    weak:
9.17/6.09	     __(X,nil()) -> X
9.17/6.09	     __(nil(),X) -> X
9.17/6.09	     U12(tt()) -> tt()
9.17/6.09	     isNePal(__(I,__(P,I))) -> U11(tt())
9.17/6.09	     activate(X) -> X
9.17/6.09	   Matrix Interpretation Processor: dim=1
9.17/6.09	    
9.17/6.09	    max_matrix:
9.17/6.09	     1
9.17/6.09	    interpretation:
9.17/6.09	     [activate](x0) = x0,
9.17/6.09	     
9.17/6.09	     [isNePal](x0) = x0 + 137,
9.17/6.09	     
9.17/6.09	     [U12](x0) = x0 + 136,
9.17/6.09	     
9.17/6.09	     [U11](x0) = x0 + 137,
9.17/6.09	     
9.17/6.09	     [tt] = 0,
9.17/6.09	     
9.17/6.09	     [nil] = 0,
9.17/6.09	     
9.17/6.09	     [__](x0, x1) = x0 + x1
9.17/6.09	    orientation:
9.17/6.09	     __(__(X,Y),Z) = X + Y + Z >= X + Y + Z = __(X,__(Y,Z))
9.17/6.09	     
9.17/6.09	     U11(tt()) = 137 >= 136 = U12(tt())
9.17/6.09	     
9.17/6.09	     __(X,nil()) = X >= X = X
9.17/6.09	     
9.17/6.09	     __(nil(),X) = X >= X = X
9.17/6.09	     
9.17/6.09	     U12(tt()) = 136 >= 0 = tt()
9.17/6.09	     
9.17/6.09	     isNePal(__(I,__(P,I))) = 2I + P + 137 >= 137 = U11(tt())
9.17/6.09	     
9.17/6.09	     activate(X) = X >= X = X
9.17/6.09	    problem:
9.17/6.09	     strict:
9.17/6.09	      __(__(X,Y),Z) -> __(X,__(Y,Z))
9.17/6.09	     weak:
9.17/6.09	      U11(tt()) -> U12(tt())
9.17/6.09	      __(X,nil()) -> X
9.17/6.09	      __(nil(),X) -> X
9.17/6.09	      U12(tt()) -> tt()
9.17/6.09	      isNePal(__(I,__(P,I))) -> U11(tt())
9.17/6.09	      activate(X) -> X
9.17/6.09	    Matrix Interpretation Processor: dim=2
9.17/6.09	     
9.17/6.09	     max_matrix:
9.17/6.09	      [1 5]
9.17/6.09	      [0 1]
9.17/6.09	     interpretation:
9.17/6.09	                       [1 1]  
9.17/6.09	      [activate](x0) = [0 1]x0,
9.17/6.09	      
9.17/6.09	                      [1 4]     [0]
9.17/6.09	      [isNePal](x0) = [0 0]x0 + [1],
9.17/6.09	      
9.17/6.09	                  [1 0]     [1]
9.17/6.09	      [U12](x0) = [0 0]x0 + [0],
9.17/6.09	      
9.17/6.09	                  [1 0]     [4]
9.17/6.09	      [U11](x0) = [0 0]x0 + [1],
9.17/6.09	      
9.17/6.09	             [6]
9.17/6.09	      [tt] = [0],
9.17/6.09	      
9.17/6.09	              [2]
9.17/6.09	      [nil] = [0],
9.17/6.09	      
9.17/6.09	                     [1 5]          [1]
9.17/6.09	      [__](x0, x1) = [0 1]x0 + x1 + [1]
9.17/6.09	     orientation:
9.17/6.09	                      [1  10]    [1 5]        [7]    [1 5]    [1 5]        [2]                
9.17/6.09	      __(__(X,Y),Z) = [0  1 ]X + [0 1]Y + Z + [2] >= [0 1]X + [0 1]Y + Z + [2] = __(X,__(Y,Z))
9.17/6.09	      
9.17/6.09	                  [10]    [7]            
9.17/6.09	      U11(tt()) = [1 ] >= [0] = U12(tt())
9.17/6.09	      
9.17/6.09	                    [1 5]    [3]         
9.17/6.09	      __(X,nil()) = [0 1]X + [1] >= X = X
9.17/6.09	      
9.17/6.09	                        [3]         
9.17/6.09	      __(nil(),X) = X + [1] >= X = X
9.17/6.09	      
9.17/6.09	                  [7]    [6]       
9.17/6.09	      U12(tt()) = [0] >= [0] = tt()
9.17/6.09	      
9.17/6.09	                               [2  13]    [1 9]    [10]    [10]            
9.17/6.09	      isNePal(__(I,__(P,I))) = [0  0 ]I + [0 0]P + [1 ] >= [1 ] = U11(tt())
9.17/6.09	      
9.17/6.09	                    [1 1]          
9.17/6.09	      activate(X) = [0 1]X >= X = X
9.17/6.09	     problem:
9.17/6.09	      strict:
9.17/6.09	       
9.17/6.09	      weak:
9.17/6.09	       __(__(X,Y),Z) -> __(X,__(Y,Z))
9.17/6.09	       U11(tt()) -> U12(tt())
9.17/6.09	       __(X,nil()) -> X
9.17/6.09	       __(nil(),X) -> X
9.17/6.09	       U12(tt()) -> tt()
9.17/6.09	       isNePal(__(I,__(P,I))) -> U11(tt())
9.17/6.09	       activate(X) -> X
9.17/6.09	     Qed
9.17/6.10	EOF