YES(?,O(n^2))
22.00/9.78	YES(?,O(n^2))
22.00/9.79	
22.00/9.79	Problem:
22.00/9.79	 f(a,empty()) -> g(a,empty())
22.00/9.79	 f(a,cons(x,k)) -> f(cons(x,a),k)
22.00/9.79	 g(empty(),d) -> d
22.00/9.79	 g(cons(x,k),d) -> g(k,cons(x,d))
22.00/9.79	
22.00/9.79	Proof:
22.00/9.79	 Complexity Transformation Processor:
22.00/9.79	  strict:
22.00/9.79	   f(a,empty()) -> g(a,empty())
22.00/9.79	   f(a,cons(x,k)) -> f(cons(x,a),k)
22.00/9.79	   g(empty(),d) -> d
22.00/9.79	   g(cons(x,k),d) -> g(k,cons(x,d))
22.00/9.79	  weak:
22.00/9.79	   
22.00/9.79	  Matrix Interpretation Processor: dim=1
22.00/9.79	   
22.00/9.79	   max_matrix:
22.00/9.79	    1
22.00/9.79	   interpretation:
22.00/9.79	    [cons](x0, x1) = x0 + x1 + 162,
22.00/9.79	    
22.00/9.79	    [g](x0, x1) = x0 + x1,
22.00/9.79	    
22.00/9.79	    [f](x0, x1) = x0 + x1 + 6,
22.00/9.79	    
22.00/9.79	    [empty] = 1
22.00/9.79	   orientation:
22.00/9.79	    f(a,empty()) = a + 7 >= a + 1 = g(a,empty())
22.00/9.79	    
22.00/9.79	    f(a,cons(x,k)) = a + k + x + 168 >= a + k + x + 168 = f(cons(x,a),k)
22.00/9.79	    
22.00/9.79	    g(empty(),d) = d + 1 >= d = d
22.00/9.79	    
22.00/9.79	    g(cons(x,k),d) = d + k + x + 162 >= d + k + x + 162 = g(k,cons(x,d))
22.00/9.79	   problem:
22.00/9.79	    strict:
22.00/9.79	     f(a,cons(x,k)) -> f(cons(x,a),k)
22.00/9.79	     g(cons(x,k),d) -> g(k,cons(x,d))
22.00/9.79	    weak:
22.00/9.79	     f(a,empty()) -> g(a,empty())
22.00/9.79	     g(empty(),d) -> d
22.00/9.79	   Splitting Processor:
22.00/9.79	    strict:
22.00/9.79	     g(cons(x,k),d) -> g(k,cons(x,d))
22.00/9.79	    weak:
22.00/9.79	     f(a,empty()) -> g(a,empty())
22.00/9.79	     g(empty(),d) -> d
22.00/9.79	     f(a,cons(x,k)) -> f(cons(x,a),k)
22.00/9.79	    Matrix Interpretation Processor: dim=2
22.00/9.79	     
22.00/9.79	     max_matrix:
22.00/9.79	      [1 2]
22.00/9.79	      [0 1]
22.00/9.79	     interpretation:
22.00/9.79	                       [1 2]          [2]
22.00/9.79	      [cons](x0, x1) = [0 0]x0 + x1 + [1],
22.00/9.79	      
22.00/9.79	                    [1 1]       
22.00/9.79	      [g](x0, x1) = [0 1]x0 + x1,
22.00/9.79	      
22.00/9.79	                    [1 1]     [1 2]     [3]
22.00/9.79	      [f](x0, x1) = [0 1]x0 + [0 1]x1 + [0],
22.00/9.79	      
22.00/9.79	                [2]
22.00/9.79	      [empty] = [1]
22.00/9.79	     orientation:
22.00/9.79	                       [1 1]    [1 2]    [1 2]    [7]    [1 1]    [1 2]    [1 2]    [6]                 
22.00/9.79	      f(a,cons(x,k)) = [0 1]a + [0 1]k + [0 0]x + [1] >= [0 1]a + [0 1]k + [0 0]x + [1] = f(cons(x,a),k)
22.00/9.79	      
22.00/9.79	                           [1 1]    [1 2]    [3]        [1 1]    [1 2]    [2]                 
22.00/9.79	      g(cons(x,k),d) = d + [0 1]k + [0 0]x + [1] >= d + [0 1]k + [0 0]x + [1] = g(k,cons(x,d))
22.00/9.79	      
22.00/9.79	                     [1 1]    [7]    [1 1]    [2]               
22.00/9.79	      f(a,empty()) = [0 1]a + [1] >= [0 1]a + [1] = g(a,empty())
22.00/9.79	      
22.00/9.79	                         [3]         
22.00/9.79	      g(empty(),d) = d + [1] >= d = d
22.00/9.79	     problem:
22.00/9.79	      strict:
22.00/9.79	       
22.00/9.79	      weak:
22.00/9.79	       f(a,cons(x,k)) -> f(cons(x,a),k)
22.00/9.79	       g(cons(x,k),d) -> g(k,cons(x,d))
22.00/9.79	       f(a,empty()) -> g(a,empty())
22.00/9.79	       g(empty(),d) -> d
22.00/9.79	     Qed
22.00/9.79	    
22.00/9.79	    strict:
22.00/9.79	     f(a,cons(x,k)) -> f(cons(x,a),k)
22.00/9.79	    weak:
22.00/9.79	     g(cons(x,k),d) -> g(k,cons(x,d))
22.00/9.79	     f(a,empty()) -> g(a,empty())
22.00/9.79	     g(empty(),d) -> d
22.00/9.79	    Matrix Interpretation Processor: dim=2
22.00/9.79	     
22.00/9.79	     max_matrix:
22.00/9.79	      [1 1]
22.00/9.79	      [0 1]
22.00/9.79	     interpretation:
22.00/9.79	                       [1 0]          [0]
22.00/9.79	      [cons](x0, x1) = [0 0]x0 + x1 + [1],
22.00/9.79	      
22.00/9.79	                    [1 1]          [0]
22.00/9.79	      [g](x0, x1) = [0 1]x0 + x1 + [1],
22.00/9.79	      
22.00/9.79	                    [1 1]     [1 1]     [0]
22.00/9.79	      [f](x0, x1) = [0 1]x0 + [0 1]x1 + [1],
22.00/9.79	      
22.00/9.79	                [3]
22.00/9.79	      [empty] = [3]
22.00/9.79	     orientation:
22.00/9.79	                           [1 1]    [1 0]    [1]        [1 1]    [1 0]    [0]                 
22.00/9.79	      g(cons(x,k),d) = d + [0 1]k + [0 0]x + [2] >= d + [0 1]k + [0 0]x + [2] = g(k,cons(x,d))
22.00/9.79	      
22.00/9.79	                     [1 1]    [6]    [1 1]    [3]               
22.00/9.79	      f(a,empty()) = [0 1]a + [4] >= [0 1]a + [4] = g(a,empty())
22.00/9.79	      
22.00/9.79	                         [6]         
22.00/9.79	      g(empty(),d) = d + [4] >= d = d
22.00/9.79	      
22.00/9.79	                       [1 1]    [1 1]    [1 0]    [1]    [1 1]    [1 1]    [1 0]    [1]                 
22.00/9.79	      f(a,cons(x,k)) = [0 1]a + [0 1]k + [0 0]x + [2] >= [0 1]a + [0 1]k + [0 0]x + [2] = f(cons(x,a),k)
22.00/9.79	     problem:
22.00/9.79	      strict:
22.00/9.79	       
22.00/9.79	      weak:
22.00/9.79	       g(cons(x,k),d) -> g(k,cons(x,d))
22.00/9.79	       f(a,empty()) -> g(a,empty())
22.00/9.79	       g(empty(),d) -> d
22.00/9.79	       f(a,cons(x,k)) -> f(cons(x,a),k)
22.00/9.79	     Qed
22.00/9.79	EOF