YES(?,O(n^2))
17.71/7.67	YES(?,O(n^2))
17.71/7.67	
17.71/7.67	Problem:
17.71/7.67	 norm(nil()) -> 0()
17.71/7.67	 norm(g(x,y)) -> s(norm(x))
17.71/7.67	 f(x,nil()) -> g(nil(),x)
17.71/7.67	 f(x,g(y,z)) -> g(f(x,y),z)
17.71/7.67	 rem(nil(),y) -> nil()
17.71/7.67	 rem(g(x,y),0()) -> g(x,y)
17.71/7.67	 rem(g(x,y),s(z)) -> rem(x,z)
17.71/7.67	
17.71/7.67	Proof:
17.71/7.67	 Complexity Transformation Processor:
17.71/7.67	  strict:
17.71/7.67	   norm(nil()) -> 0()
17.71/7.67	   norm(g(x,y)) -> s(norm(x))
17.71/7.67	   f(x,nil()) -> g(nil(),x)
17.71/7.67	   f(x,g(y,z)) -> g(f(x,y),z)
17.71/7.67	   rem(nil(),y) -> nil()
17.71/7.67	   rem(g(x,y),0()) -> g(x,y)
17.71/7.67	   rem(g(x,y),s(z)) -> rem(x,z)
17.71/7.67	  weak:
17.71/7.67	   
17.71/7.67	  Matrix Interpretation Processor: dim=1
17.71/7.67	   
17.71/7.67	   max_matrix:
17.71/7.67	    1
17.71/7.67	   interpretation:
17.71/7.67	    [rem](x0, x1) = x0 + x1 + 246,
17.71/7.67	    
17.71/7.67	    [f](x0, x1) = x0 + x1 + 240,
17.71/7.67	    
17.71/7.67	    [s](x0) = x0 + 244,
17.71/7.67	    
17.71/7.67	    [g](x0, x1) = x0 + x1 + 13,
17.71/7.67	    
17.71/7.67	    [0] = 0,
17.71/7.67	    
17.71/7.67	    [norm](x0) = x0 + 128,
17.71/7.67	    
17.71/7.67	    [nil] = 19
17.71/7.67	   orientation:
17.71/7.67	    norm(nil()) = 147 >= 0 = 0()
17.71/7.67	    
17.71/7.67	    norm(g(x,y)) = x + y + 141 >= x + 372 = s(norm(x))
17.71/7.67	    
17.71/7.67	    f(x,nil()) = x + 259 >= x + 32 = g(nil(),x)
17.71/7.67	    
17.71/7.67	    f(x,g(y,z)) = x + y + z + 253 >= x + y + z + 253 = g(f(x,y),z)
17.71/7.67	    
17.71/7.67	    rem(nil(),y) = y + 265 >= 19 = nil()
17.71/7.67	    
17.71/7.67	    rem(g(x,y),0()) = x + y + 259 >= x + y + 13 = g(x,y)
17.71/7.67	    
17.71/7.67	    rem(g(x,y),s(z)) = x + y + z + 503 >= x + z + 246 = rem(x,z)
17.71/7.67	   problem:
17.71/7.67	    strict:
17.71/7.67	     norm(g(x,y)) -> s(norm(x))
17.71/7.67	     f(x,g(y,z)) -> g(f(x,y),z)
17.71/7.67	    weak:
17.71/7.67	     norm(nil()) -> 0()
17.71/7.67	     f(x,nil()) -> g(nil(),x)
17.71/7.67	     rem(nil(),y) -> nil()
17.71/7.67	     rem(g(x,y),0()) -> g(x,y)
17.71/7.67	     rem(g(x,y),s(z)) -> rem(x,z)
17.71/7.67	   Matrix Interpretation Processor: dim=1
17.71/7.67	    
17.71/7.67	    max_matrix:
17.71/7.67	     1
17.71/7.67	    interpretation:
17.71/7.67	     [rem](x0, x1) = x0 + x1,
17.71/7.67	     
17.71/7.67	     [f](x0, x1) = x0 + x1 + 2,
17.71/7.67	     
17.71/7.67	     [s](x0) = x0,
17.71/7.67	     
17.71/7.67	     [g](x0, x1) = x0 + x1 + 1,
17.71/7.67	     
17.71/7.67	     [0] = 0,
17.71/7.67	     
17.71/7.67	     [norm](x0) = x0 + 255,
17.71/7.67	     
17.71/7.67	     [nil] = 2
17.71/7.67	    orientation:
17.71/7.67	     norm(g(x,y)) = x + y + 256 >= x + 255 = s(norm(x))
17.71/7.67	     
17.71/7.67	     f(x,g(y,z)) = x + y + z + 3 >= x + y + z + 3 = g(f(x,y),z)
17.71/7.67	     
17.71/7.67	     norm(nil()) = 257 >= 0 = 0()
17.71/7.67	     
17.71/7.67	     f(x,nil()) = x + 4 >= x + 3 = g(nil(),x)
17.71/7.67	     
17.71/7.67	     rem(nil(),y) = y + 2 >= 2 = nil()
17.71/7.67	     
17.71/7.67	     rem(g(x,y),0()) = x + y + 1 >= x + y + 1 = g(x,y)
17.71/7.67	     
17.71/7.67	     rem(g(x,y),s(z)) = x + y + z + 1 >= x + z = rem(x,z)
17.71/7.67	    problem:
17.71/7.67	     strict:
17.71/7.67	      f(x,g(y,z)) -> g(f(x,y),z)
17.71/7.67	     weak:
17.71/7.67	      norm(g(x,y)) -> s(norm(x))
17.71/7.67	      norm(nil()) -> 0()
17.71/7.67	      f(x,nil()) -> g(nil(),x)
17.71/7.67	      rem(nil(),y) -> nil()
17.71/7.67	      rem(g(x,y),0()) -> g(x,y)
17.71/7.67	      rem(g(x,y),s(z)) -> rem(x,z)
17.71/7.67	    Matrix Interpretation Processor: dim=4
17.71/7.67	     
17.71/7.67	     max_matrix:
17.71/7.67	      [1 0 0 1]
17.71/7.67	      [0 0 1 1]
17.71/7.67	      [0 0 0 1]
17.71/7.67	      [0 0 0 1]
17.71/7.67	     interpretation:
17.71/7.67	                      [1 0 0 0]     [1 0 0 1]     [0]
17.71/7.67	                      [0 0 0 0]     [0 0 0 0]     [1]
17.71/7.67	      [rem](x0, x1) = [0 0 0 1]x0 + [0 0 0 0]x1 + [1]
17.71/7.67	                      [0 0 0 1]     [0 0 0 0]     [1],
17.71/7.67	      
17.71/7.67	                    [1 0 0 0]     [1 0 0 1]     [1]
17.71/7.67	                    [0 0 0 1]     [0 0 0 0]     [0]
17.71/7.67	      [f](x0, x1) = [0 0 0 1]x0 + [0 0 0 1]x1 + [0]
17.71/7.67	                    [0 0 0 1]     [0 0 0 1]     [1],
17.71/7.67	      
17.71/7.67	                [1 0 0 1]  
17.71/7.67	                [0 0 1 1]  
17.71/7.67	      [s](x0) = [0 0 0 0]x0
17.71/7.67	                [0 0 0 1]  ,
17.71/7.67	      
17.71/7.67	                    [1 0 0 0]     [1 0 0 0]     [0]
17.71/7.67	                    [0 0 0 0]     [0 0 0 0]     [0]
17.71/7.67	      [g](x0, x1) = [0 0 0 1]x0 + [0 0 0 0]x1 + [0]
17.71/7.67	                    [0 0 0 1]     [0 0 0 0]     [1],
17.71/7.67	      
17.71/7.67	            [0]
17.71/7.67	            [0]
17.71/7.67	      [0] = [0]
17.71/7.67	            [1],
17.71/7.67	      
17.71/7.67	                   [1 0 0 1]     [0]
17.71/7.67	                   [0 0 1 0]     [1]
17.71/7.67	      [norm](x0) = [0 0 0 1]x0 + [0]
17.71/7.67	                   [0 0 0 0]     [1],
17.71/7.67	      
17.71/7.67	              [1]
17.71/7.67	              [0]
17.71/7.67	      [nil] = [0]
17.71/7.67	              [1]
17.71/7.67	     orientation:
17.71/7.67	                    [1 0 0 0]    [1 0 0 1]    [1 0 0 0]    [2]    [1 0 0 0]    [1 0 0 1]    [1 0 0 0]    [1]              
17.71/7.67	                    [0 0 0 1]    [0 0 0 0]    [0 0 0 0]    [0]    [0 0 0 0]    [0 0 0 0]    [0 0 0 0]    [0]              
17.71/7.67	      f(x,g(y,z)) = [0 0 0 1]x + [0 0 0 1]y + [0 0 0 0]z + [1] >= [0 0 0 1]x + [0 0 0 1]y + [0 0 0 0]z + [1] = g(f(x,y),z)
17.71/7.67	                    [0 0 0 1]    [0 0 0 1]    [0 0 0 0]    [2]    [0 0 0 1]    [0 0 0 1]    [0 0 0 0]    [2]              
17.71/7.68	      
17.71/7.68	                     [1 0 0 1]    [1 0 0 0]    [1]    [1 0 0 1]    [1]             
17.71/7.68	                     [0 0 0 1]    [0 0 0 0]    [1]    [0 0 0 1]    [1]             
17.71/7.68	      norm(g(x,y)) = [0 0 0 1]x + [0 0 0 0]y + [1] >= [0 0 0 0]x + [0] = s(norm(x))
17.71/7.68	                     [0 0 0 0]    [0 0 0 0]    [1]    [0 0 0 0]    [1]             
17.71/7.68	      
17.71/7.68	                    [2]    [0]      
17.71/7.68	                    [1]    [0]      
17.71/7.68	      norm(nil()) = [1] >= [0] = 0()
17.71/7.68	                    [1]    [1]      
17.71/7.68	      
17.71/7.68	                   [1 0 0 0]    [3]    [1 0 0 0]    [1]             
17.71/7.68	                   [0 0 0 1]    [0]    [0 0 0 0]    [0]             
17.71/7.68	      f(x,nil()) = [0 0 0 1]x + [1] >= [0 0 0 0]x + [1] = g(nil(),x)
17.71/7.68	                   [0 0 0 1]    [2]    [0 0 0 0]    [2]             
17.71/7.68	      
17.71/7.68	                     [1 0 0 1]    [1]    [1]        
17.71/7.68	                     [0 0 0 0]    [1]    [0]        
17.71/7.68	      rem(nil(),y) = [0 0 0 0]y + [2] >= [0] = nil()
17.71/7.68	                     [0 0 0 0]    [2]    [1]        
17.71/7.68	      
17.71/7.68	                        [1 0 0 0]    [1 0 0 0]    [1]    [1 0 0 0]    [1 0 0 0]    [0]         
17.71/7.68	                        [0 0 0 0]    [0 0 0 0]    [1]    [0 0 0 0]    [0 0 0 0]    [0]         
17.71/7.68	      rem(g(x,y),0()) = [0 0 0 1]x + [0 0 0 0]y + [2] >= [0 0 0 1]x + [0 0 0 0]y + [0] = g(x,y)
17.71/7.68	                        [0 0 0 1]    [0 0 0 0]    [2]    [0 0 0 1]    [0 0 0 0]    [1]         
17.71/7.68	      
17.71/7.68	                         [1 0 0 0]    [1 0 0 0]    [1 0 0 2]    [0]    [1 0 0 0]    [1 0 0 1]    [0]           
17.71/7.68	                         [0 0 0 0]    [0 0 0 0]    [0 0 0 0]    [1]    [0 0 0 0]    [0 0 0 0]    [1]           
17.71/7.68	      rem(g(x,y),s(z)) = [0 0 0 1]x + [0 0 0 0]y + [0 0 0 0]z + [2] >= [0 0 0 1]x + [0 0 0 0]z + [1] = rem(x,z)
17.71/7.68	                         [0 0 0 1]    [0 0 0 0]    [0 0 0 0]    [2]    [0 0 0 1]    [0 0 0 0]    [1]           
17.71/7.68	     problem:
17.71/7.68	      strict:
17.71/7.68	       
17.71/7.68	      weak:
17.71/7.68	       f(x,g(y,z)) -> g(f(x,y),z)
17.71/7.68	       norm(g(x,y)) -> s(norm(x))
17.71/7.68	       norm(nil()) -> 0()
17.71/7.68	       f(x,nil()) -> g(nil(),x)
17.71/7.68	       rem(nil(),y) -> nil()
17.71/7.68	       rem(g(x,y),0()) -> g(x,y)
17.71/7.68	       rem(g(x,y),s(z)) -> rem(x,z)
17.71/7.68	     Qed
17.71/7.68	EOF