YES(?,O(n^2))
11.76/6.86	YES(?,O(n^2))
11.76/6.86	
11.76/6.86	Problem:
11.76/6.86	 __(__(X,Y),Z) -> __(X,__(Y,Z))
11.76/6.86	 __(X,nil()) -> X
11.76/6.86	 __(nil(),X) -> X
11.76/6.86	 and(tt(),X) -> activate(X)
11.76/6.86	 isNePal(__(I,__(P,I))) -> tt()
11.76/6.86	 activate(X) -> X
11.76/6.86	
11.76/6.86	Proof:
11.76/6.86	 Complexity Transformation Processor:
11.76/6.86	  strict:
11.76/6.86	   __(__(X,Y),Z) -> __(X,__(Y,Z))
11.76/6.86	   __(X,nil()) -> X
11.76/6.86	   __(nil(),X) -> X
11.76/6.86	   and(tt(),X) -> activate(X)
11.76/6.86	   isNePal(__(I,__(P,I))) -> tt()
11.76/6.86	   activate(X) -> X
11.76/6.86	  weak:
11.76/6.86	   
11.76/6.86	  Matrix Interpretation Processor: dim=1
11.76/6.86	   
11.76/6.86	   max_matrix:
11.76/6.86	    1
11.76/6.86	   interpretation:
11.76/6.86	    [isNePal](x0) = x0 + 64,
11.76/6.86	    
11.76/6.86	    [activate](x0) = x0 + 1,
11.76/6.86	    
11.76/6.86	    [and](x0, x1) = x0 + x1,
11.76/6.86	    
11.76/6.86	    [tt] = 241,
11.76/6.86	    
11.76/6.86	    [nil] = 96,
11.76/6.86	    
11.76/6.86	    [__](x0, x1) = x0 + x1 + 32
11.76/6.86	   orientation:
11.76/6.86	    __(__(X,Y),Z) = X + Y + Z + 64 >= X + Y + Z + 64 = __(X,__(Y,Z))
11.76/6.86	    
11.76/6.86	    __(X,nil()) = X + 128 >= X = X
11.76/6.86	    
11.76/6.86	    __(nil(),X) = X + 128 >= X = X
11.76/6.86	    
11.76/6.86	    and(tt(),X) = X + 241 >= X + 1 = activate(X)
11.76/6.86	    
11.76/6.86	    isNePal(__(I,__(P,I))) = 2I + P + 128 >= 241 = tt()
11.76/6.86	    
11.76/6.86	    activate(X) = X + 1 >= X = X
11.76/6.86	   problem:
11.76/6.86	    strict:
11.76/6.86	     __(__(X,Y),Z) -> __(X,__(Y,Z))
11.76/6.86	     isNePal(__(I,__(P,I))) -> tt()
11.76/6.86	    weak:
11.76/6.86	     __(X,nil()) -> X
11.76/6.86	     __(nil(),X) -> X
11.76/6.86	     and(tt(),X) -> activate(X)
11.76/6.86	     activate(X) -> X
11.76/6.86	   Matrix Interpretation Processor: dim=1
11.76/6.86	    
11.76/6.86	    max_matrix:
11.76/6.86	     1
11.76/6.86	    interpretation:
11.76/6.86	     [isNePal](x0) = x0 + 1,
11.76/6.86	     
11.76/6.86	     [activate](x0) = x0 + 1,
11.76/6.86	     
11.76/6.86	     [and](x0, x1) = x0 + x1 + 120,
11.76/6.86	     
11.76/6.86	     [tt] = 8,
11.76/6.86	     
11.76/6.86	     [nil] = 72,
11.76/6.86	     
11.76/6.86	     [__](x0, x1) = x0 + x1 + 5
11.76/6.86	    orientation:
11.76/6.86	     __(__(X,Y),Z) = X + Y + Z + 10 >= X + Y + Z + 10 = __(X,__(Y,Z))
11.76/6.86	     
11.76/6.86	     isNePal(__(I,__(P,I))) = 2I + P + 11 >= 8 = tt()
11.76/6.86	     
11.76/6.86	     __(X,nil()) = X + 77 >= X = X
11.76/6.86	     
11.76/6.86	     __(nil(),X) = X + 77 >= X = X
11.76/6.86	     
11.76/6.86	     and(tt(),X) = X + 128 >= X + 1 = activate(X)
11.76/6.86	     
11.76/6.86	     activate(X) = X + 1 >= X = X
11.76/6.86	    problem:
11.76/6.86	     strict:
11.76/6.86	      __(__(X,Y),Z) -> __(X,__(Y,Z))
11.76/6.86	     weak:
11.76/6.86	      isNePal(__(I,__(P,I))) -> tt()
11.76/6.86	      __(X,nil()) -> X
11.76/6.86	      __(nil(),X) -> X
11.76/6.86	      and(tt(),X) -> activate(X)
11.76/6.86	      activate(X) -> X
11.76/6.86	    Matrix Interpretation Processor: dim=2
11.76/6.86	     
11.76/6.86	     max_matrix:
11.76/6.86	      [1 2]
11.76/6.86	      [0 1]
11.76/6.86	     interpretation:
11.76/6.86	                      [1 2]  
11.76/6.86	      [isNePal](x0) = [0 1]x0,
11.76/6.86	      
11.76/6.86	                         
11.76/6.86	      [activate](x0) = x0,
11.76/6.86	      
11.76/6.86	                      [1 2]       
11.76/6.86	      [and](x0, x1) = [0 1]x0 + x1,
11.76/6.86	      
11.76/6.86	             [0]
11.76/6.86	      [tt] = [0],
11.76/6.86	      
11.76/6.86	              [2]
11.76/6.86	      [nil] = [0],
11.76/6.86	      
11.76/6.86	                     [1 2]          [0]
11.76/6.86	      [__](x0, x1) = [0 1]x0 + x1 + [1]
11.76/6.86	     orientation:
11.76/6.86	                      [1 4]    [1 2]        [2]    [1 2]    [1 2]        [0]                
11.76/6.86	      __(__(X,Y),Z) = [0 1]X + [0 1]Y + Z + [2] >= [0 1]X + [0 1]Y + Z + [2] = __(X,__(Y,Z))
11.76/6.86	      
11.76/6.86	                               [2 6]    [1 4]    [4]    [0]       
11.76/6.86	      isNePal(__(I,__(P,I))) = [0 2]I + [0 1]P + [2] >= [0] = tt()
11.76/6.86	      
11.76/6.86	                    [1 2]    [2]         
11.76/6.86	      __(X,nil()) = [0 1]X + [1] >= X = X
11.76/6.86	      
11.76/6.86	                        [2]         
11.76/6.86	      __(nil(),X) = X + [1] >= X = X
11.76/6.86	      
11.76/6.86	                                        
11.76/6.86	      and(tt(),X) = X >= X = activate(X)
11.76/6.86	      
11.76/6.86	                              
11.76/6.86	      activate(X) = X >= X = X
11.76/6.86	     problem:
11.76/6.86	      strict:
11.76/6.86	       
11.76/6.86	      weak:
11.76/6.86	       __(__(X,Y),Z) -> __(X,__(Y,Z))
11.76/6.86	       isNePal(__(I,__(P,I))) -> tt()
11.76/6.86	       __(X,nil()) -> X
11.76/6.86	       __(nil(),X) -> X
11.76/6.86	       and(tt(),X) -> activate(X)
11.76/6.86	       activate(X) -> X
11.76/6.86	     Qed
11.76/6.87	EOF