YES(?,O(n^2))
11.03/6.87	YES(?,O(n^2))
11.03/6.87	
11.03/6.87	Problem:
11.03/6.87	 rev(ls) -> r1(ls,empty())
11.03/6.87	 r1(empty(),a) -> a
11.03/6.87	 r1(cons(x,k),a) -> r1(k,cons(x,a))
11.03/6.87	
11.03/6.87	Proof:
11.03/6.87	 Complexity Transformation Processor:
11.03/6.87	  strict:
11.03/6.87	   rev(ls) -> r1(ls,empty())
11.03/6.87	   r1(empty(),a) -> a
11.03/6.87	   r1(cons(x,k),a) -> r1(k,cons(x,a))
11.03/6.87	  weak:
11.03/6.87	   
11.03/6.87	  Matrix Interpretation Processor: dim=1
11.03/6.87	   
11.03/6.87	   max_matrix:
11.03/6.87	    1
11.03/6.87	   interpretation:
11.03/6.87	    [cons](x0, x1) = x0 + x1 + 1,
11.03/6.87	    
11.03/6.87	    [r1](x0, x1) = x0 + x1 + 102,
11.03/6.87	    
11.03/6.87	    [empty] = 2,
11.03/6.87	    
11.03/6.87	    [rev](x0) = x0 + 105
11.03/6.87	   orientation:
11.03/6.87	    rev(ls) = ls + 105 >= ls + 104 = r1(ls,empty())
11.03/6.87	    
11.03/6.87	    r1(empty(),a) = a + 104 >= a = a
11.03/6.87	    
11.03/6.87	    r1(cons(x,k),a) = a + k + x + 103 >= a + k + x + 103 = r1(k,cons(x,a))
11.03/6.87	   problem:
11.03/6.87	    strict:
11.03/6.87	     r1(cons(x,k),a) -> r1(k,cons(x,a))
11.03/6.87	    weak:
11.03/6.87	     rev(ls) -> r1(ls,empty())
11.03/6.87	     r1(empty(),a) -> a
11.03/6.87	   Matrix Interpretation Processor: dim=2
11.03/6.87	    
11.03/6.87	    max_matrix:
11.03/6.87	     [1 3]
11.03/6.87	     [0 1]
11.03/6.87	    interpretation:
11.03/6.87	                      [1 3]          [0]
11.03/6.87	     [cons](x0, x1) = [0 1]x0 + x1 + [1],
11.03/6.87	     
11.03/6.87	                    [1 1]       
11.03/6.87	     [r1](x0, x1) = [0 1]x0 + x1,
11.03/6.87	     
11.03/6.87	               [1]
11.03/6.87	     [empty] = [2],
11.03/6.87	     
11.03/6.87	                 [1 1]     [2]
11.03/6.87	     [rev](x0) = [0 1]x0 + [2]
11.03/6.87	    orientation:
11.03/6.87	                           [1 1]    [1 4]    [1]        [1 1]    [1 3]    [0]                  
11.03/6.87	     r1(cons(x,k),a) = a + [0 1]k + [0 1]x + [1] >= a + [0 1]k + [0 1]x + [1] = r1(k,cons(x,a))
11.03/6.87	     
11.03/6.87	               [1 1]     [2]    [1 1]     [1]                 
11.03/6.87	     rev(ls) = [0 1]ls + [2] >= [0 1]ls + [2] = r1(ls,empty())
11.03/6.87	     
11.03/6.87	                         [3]         
11.03/6.87	     r1(empty(),a) = a + [2] >= a = a
11.03/6.87	    problem:
11.03/6.87	     strict:
11.03/6.87	      
11.03/6.87	     weak:
11.03/6.87	      r1(cons(x,k),a) -> r1(k,cons(x,a))
11.03/6.87	      rev(ls) -> r1(ls,empty())
11.03/6.87	      r1(empty(),a) -> a
11.03/6.87	    Qed
11.03/6.88	EOF