YES(O(1),O(n^2))
152.82/59.02	YES(O(1),O(n^2))
152.82/59.02	
152.82/59.02	We are left with following problem, upon which TcT provides the
152.82/59.02	certificate YES(O(1),O(n^2)).
152.82/59.02	
152.82/59.02	Strict Trs:
152.82/59.02	  { rev(nil()) -> nil()
152.82/59.02	  , rev(.(x, y)) -> ++(rev(y), .(x, nil()))
152.82/59.02	  , ++(nil(), y) -> y
152.82/59.02	  , ++(.(x, y), z) -> .(x, ++(y, z))
152.82/59.02	  , car(.(x, y)) -> x
152.82/59.02	  , cdr(.(x, y)) -> y
152.82/59.02	  , null(nil()) -> true()
152.82/59.02	  , null(.(x, y)) -> false() }
152.82/59.02	Obligation:
152.82/59.02	  innermost runtime complexity
152.82/59.02	Answer:
152.82/59.02	  YES(O(1),O(n^2))
152.82/59.02	
152.82/59.02	We add the following dependency tuples:
152.82/59.02	
152.82/59.02	Strict DPs:
152.82/59.02	  { rev^#(nil()) -> c_1()
152.82/59.02	  , rev^#(.(x, y)) -> c_2(++^#(rev(y), .(x, nil())), rev^#(y))
152.82/59.02	  , ++^#(nil(), y) -> c_3()
152.82/59.02	  , ++^#(.(x, y), z) -> c_4(++^#(y, z))
152.82/59.02	  , car^#(.(x, y)) -> c_5()
152.82/59.02	  , cdr^#(.(x, y)) -> c_6()
152.82/59.02	  , null^#(nil()) -> c_7()
152.82/59.02	  , null^#(.(x, y)) -> c_8() }
152.82/59.02	
152.82/59.02	and mark the set of starting terms.
152.82/59.02	
152.82/59.02	We are left with following problem, upon which TcT provides the
152.82/59.02	certificate YES(O(1),O(n^2)).
152.82/59.02	
152.82/59.02	Strict DPs:
152.82/59.02	  { rev^#(nil()) -> c_1()
152.82/59.02	  , rev^#(.(x, y)) -> c_2(++^#(rev(y), .(x, nil())), rev^#(y))
152.82/59.02	  , ++^#(nil(), y) -> c_3()
152.82/59.02	  , ++^#(.(x, y), z) -> c_4(++^#(y, z))
152.82/59.02	  , car^#(.(x, y)) -> c_5()
152.82/59.02	  , cdr^#(.(x, y)) -> c_6()
152.82/59.02	  , null^#(nil()) -> c_7()
152.82/59.02	  , null^#(.(x, y)) -> c_8() }
152.82/59.02	Weak Trs:
152.82/59.02	  { rev(nil()) -> nil()
152.82/59.02	  , rev(.(x, y)) -> ++(rev(y), .(x, nil()))
152.82/59.02	  , ++(nil(), y) -> y
152.82/59.02	  , ++(.(x, y), z) -> .(x, ++(y, z))
152.82/59.02	  , car(.(x, y)) -> x
152.82/59.02	  , cdr(.(x, y)) -> y
152.82/59.02	  , null(nil()) -> true()
152.82/59.02	  , null(.(x, y)) -> false() }
152.82/59.02	Obligation:
152.82/59.02	  innermost runtime complexity
152.82/59.02	Answer:
152.82/59.02	  YES(O(1),O(n^2))
152.82/59.02	
152.82/59.02	We estimate the number of application of {1,3,5,6,7,8} by
152.82/59.02	applications of Pre({1,3,5,6,7,8}) = {2,4}. Here rules are labeled
152.82/59.02	as follows:
152.82/59.02	
152.82/59.02	  DPs:
152.82/59.02	    { 1: rev^#(nil()) -> c_1()
152.82/59.02	    , 2: rev^#(.(x, y)) -> c_2(++^#(rev(y), .(x, nil())), rev^#(y))
152.82/59.02	    , 3: ++^#(nil(), y) -> c_3()
152.82/59.02	    , 4: ++^#(.(x, y), z) -> c_4(++^#(y, z))
152.82/59.02	    , 5: car^#(.(x, y)) -> c_5()
152.82/59.02	    , 6: cdr^#(.(x, y)) -> c_6()
152.82/59.02	    , 7: null^#(nil()) -> c_7()
152.82/59.02	    , 8: null^#(.(x, y)) -> c_8() }
152.82/59.02	
152.82/59.02	We are left with following problem, upon which TcT provides the
152.82/59.02	certificate YES(O(1),O(n^2)).
152.82/59.02	
152.82/59.02	Strict DPs:
152.82/59.02	  { rev^#(.(x, y)) -> c_2(++^#(rev(y), .(x, nil())), rev^#(y))
152.82/59.02	  , ++^#(.(x, y), z) -> c_4(++^#(y, z)) }
152.82/59.02	Weak DPs:
152.82/59.02	  { rev^#(nil()) -> c_1()
152.82/59.02	  , ++^#(nil(), y) -> c_3()
152.82/59.02	  , car^#(.(x, y)) -> c_5()
152.82/59.02	  , cdr^#(.(x, y)) -> c_6()
152.82/59.02	  , null^#(nil()) -> c_7()
152.82/59.02	  , null^#(.(x, y)) -> c_8() }
152.82/59.02	Weak Trs:
152.82/59.02	  { rev(nil()) -> nil()
152.82/59.02	  , rev(.(x, y)) -> ++(rev(y), .(x, nil()))
152.82/59.02	  , ++(nil(), y) -> y
152.82/59.02	  , ++(.(x, y), z) -> .(x, ++(y, z))
152.82/59.02	  , car(.(x, y)) -> x
152.82/59.02	  , cdr(.(x, y)) -> y
152.82/59.02	  , null(nil()) -> true()
152.82/59.02	  , null(.(x, y)) -> false() }
152.82/59.02	Obligation:
152.82/59.02	  innermost runtime complexity
152.82/59.02	Answer:
152.82/59.02	  YES(O(1),O(n^2))
152.82/59.02	
152.82/59.02	The following weak DPs constitute a sub-graph of the DG that is
152.82/59.02	closed under successors. The DPs are removed.
152.82/59.02	
152.82/59.02	{ rev^#(nil()) -> c_1()
152.82/59.02	, ++^#(nil(), y) -> c_3()
152.82/59.02	, car^#(.(x, y)) -> c_5()
152.82/59.02	, cdr^#(.(x, y)) -> c_6()
152.82/59.02	, null^#(nil()) -> c_7()
152.82/59.02	, null^#(.(x, y)) -> c_8() }
152.82/59.02	
152.82/59.02	We are left with following problem, upon which TcT provides the
152.82/59.02	certificate YES(O(1),O(n^2)).
152.82/59.02	
152.82/59.02	Strict DPs:
152.82/59.02	  { rev^#(.(x, y)) -> c_2(++^#(rev(y), .(x, nil())), rev^#(y))
152.82/59.02	  , ++^#(.(x, y), z) -> c_4(++^#(y, z)) }
152.82/59.02	Weak Trs:
152.82/59.02	  { rev(nil()) -> nil()
152.82/59.02	  , rev(.(x, y)) -> ++(rev(y), .(x, nil()))
152.82/59.02	  , ++(nil(), y) -> y
152.82/59.02	  , ++(.(x, y), z) -> .(x, ++(y, z))
152.82/59.02	  , car(.(x, y)) -> x
152.82/59.02	  , cdr(.(x, y)) -> y
152.82/59.02	  , null(nil()) -> true()
152.82/59.02	  , null(.(x, y)) -> false() }
152.82/59.02	Obligation:
152.82/59.02	  innermost runtime complexity
152.82/59.02	Answer:
152.82/59.02	  YES(O(1),O(n^2))
152.82/59.02	
152.82/59.02	We replace rewrite rules by usable rules:
152.82/59.02	
152.82/59.02	  Weak Usable Rules:
152.82/59.02	    { rev(nil()) -> nil()
152.82/59.02	    , rev(.(x, y)) -> ++(rev(y), .(x, nil()))
152.82/59.02	    , ++(nil(), y) -> y
152.82/59.02	    , ++(.(x, y), z) -> .(x, ++(y, z)) }
152.82/59.02	
152.82/59.02	We are left with following problem, upon which TcT provides the
152.82/59.02	certificate YES(O(1),O(n^2)).
152.82/59.02	
152.82/59.02	Strict DPs:
152.82/59.02	  { rev^#(.(x, y)) -> c_2(++^#(rev(y), .(x, nil())), rev^#(y))
152.82/59.02	  , ++^#(.(x, y), z) -> c_4(++^#(y, z)) }
152.82/59.02	Weak Trs:
152.82/59.02	  { rev(nil()) -> nil()
152.82/59.02	  , rev(.(x, y)) -> ++(rev(y), .(x, nil()))
152.82/59.02	  , ++(nil(), y) -> y
152.82/59.02	  , ++(.(x, y), z) -> .(x, ++(y, z)) }
152.82/59.02	Obligation:
152.82/59.02	  innermost runtime complexity
152.82/59.02	Answer:
152.82/59.02	  YES(O(1),O(n^2))
152.82/59.02	
152.82/59.02	We use the processor 'polynomial interpretation' to orient
152.82/59.02	following rules strictly.
152.82/59.02	
152.82/59.02	DPs:
152.82/59.02	  { 1: rev^#(.(x, y)) -> c_2(++^#(rev(y), .(x, nil())), rev^#(y))
152.82/59.02	  , 2: ++^#(.(x, y), z) -> c_4(++^#(y, z)) }
152.82/59.02	
152.82/59.02	Sub-proof:
152.82/59.02	----------
152.82/59.02	  We consider the following typing:
152.82/59.02	  
152.82/59.02	    rev :: c -> c
152.82/59.02	    nil :: c
152.82/59.02	    . :: (a,c) -> c
152.82/59.02	    ++ :: (c,c) -> c
152.82/59.02	    rev^# :: c -> b
152.82/59.02	    c_2 :: (d,b) -> b
152.82/59.02	    ++^# :: (c,c) -> d
152.82/59.02	    c_4 :: d -> d
152.82/59.02	  
152.82/59.02	  The following argument positions are considered usable:
152.82/59.02	  
152.82/59.02	    Uargs(c_2) = {1, 2}, Uargs(c_4) = {1}
152.82/59.02	  
152.82/59.02	  TcT has computed the following constructor-restricted
152.82/59.02	  typedpolynomial interpretation.
152.82/59.02	  
152.82/59.02	       [rev](x1) = x1           
152.82/59.02	                                
152.82/59.02	         [nil]() = 0            
152.82/59.02	                                
152.82/59.02	     [.](x1, x2) = 1 + x2       
152.82/59.02	                                
152.82/59.02	    [++](x1, x2) = x1 + x2      
152.82/59.02	                                
152.82/59.02	     [rev^#](x1) = 2*x1^2       
152.82/59.02	                                
152.82/59.02	   [c_2](x1, x2) = 1 + 2*x1 + x2
152.82/59.02	                                
152.82/59.02	  [++^#](x1, x2) = 2*x1         
152.82/59.02	                                
152.82/59.02	       [c_4](x1) = x1           
152.82/59.02	                                
152.82/59.02	  
152.82/59.02	  This order satisfies the following ordering constraints.
152.82/59.02	  
152.82/59.02	          [rev(nil())] =                                            
152.82/59.02	                       >=                                           
152.82/59.02	                       =  [nil()]                                   
152.82/59.02	                                                                    
152.82/59.02	        [rev(.(x, y))] =  1 + y                                     
152.82/59.02	                       >= y + 1                                     
152.82/59.02	                       =  [++(rev(y), .(x, nil()))]                 
152.82/59.02	                                                                    
152.82/59.02	        [++(nil(), y)] =  y                                         
152.82/59.02	                       >= y                                         
152.82/59.02	                       =  [y]                                       
152.82/59.02	                                                                    
152.82/59.02	      [++(.(x, y), z)] =  1 + y + z                                 
152.82/59.02	                       >= 1 + y + z                                 
152.82/59.02	                       =  [.(x, ++(y, z))]                          
152.82/59.02	                                                                    
152.82/59.02	      [rev^#(.(x, y))] =  2 + 4*y + 2*y^2                           
152.82/59.02	                       >  1 + 4*y + 2*y^2                           
152.82/59.02	                       =  [c_2(++^#(rev(y), .(x, nil())), rev^#(y))]
152.82/59.02	                                                                    
152.82/59.02	    [++^#(.(x, y), z)] =  2 + 2*y                                   
152.82/59.02	                       >  2*y                                       
152.82/59.02	                       =  [c_4(++^#(y, z))]                         
152.82/59.02	                                                                    
152.82/59.02	
152.82/59.02	The strictly oriented rules are moved into the weak component.
152.82/59.02	
152.82/59.02	We are left with following problem, upon which TcT provides the
152.82/59.02	certificate YES(O(1),O(1)).
152.82/59.02	
152.82/59.02	Weak DPs:
152.82/59.02	  { rev^#(.(x, y)) -> c_2(++^#(rev(y), .(x, nil())), rev^#(y))
152.82/59.02	  , ++^#(.(x, y), z) -> c_4(++^#(y, z)) }
152.82/59.02	Weak Trs:
152.82/59.02	  { rev(nil()) -> nil()
152.82/59.02	  , rev(.(x, y)) -> ++(rev(y), .(x, nil()))
152.82/59.02	  , ++(nil(), y) -> y
152.82/59.02	  , ++(.(x, y), z) -> .(x, ++(y, z)) }
152.82/59.02	Obligation:
152.82/59.02	  innermost runtime complexity
152.82/59.02	Answer:
152.82/59.02	  YES(O(1),O(1))
152.82/59.02	
152.82/59.02	The following weak DPs constitute a sub-graph of the DG that is
152.82/59.02	closed under successors. The DPs are removed.
152.82/59.02	
152.82/59.02	{ rev^#(.(x, y)) -> c_2(++^#(rev(y), .(x, nil())), rev^#(y))
152.82/59.02	, ++^#(.(x, y), z) -> c_4(++^#(y, z)) }
152.82/59.02	
152.82/59.02	We are left with following problem, upon which TcT provides the
152.82/59.02	certificate YES(O(1),O(1)).
152.82/59.02	
152.82/59.02	Weak Trs:
152.82/59.02	  { rev(nil()) -> nil()
152.82/59.02	  , rev(.(x, y)) -> ++(rev(y), .(x, nil()))
152.82/59.02	  , ++(nil(), y) -> y
152.82/59.02	  , ++(.(x, y), z) -> .(x, ++(y, z)) }
152.82/59.02	Obligation:
152.82/59.02	  innermost runtime complexity
152.82/59.02	Answer:
152.82/59.02	  YES(O(1),O(1))
152.82/59.02	
152.82/59.02	No rule is usable, rules are removed from the input problem.
152.82/59.02	
152.82/59.02	We are left with following problem, upon which TcT provides the
152.82/59.02	certificate YES(O(1),O(1)).
152.82/59.02	
152.82/59.02	Rules: Empty
152.82/59.02	Obligation:
152.82/59.02	  innermost runtime complexity
152.82/59.02	Answer:
152.82/59.02	  YES(O(1),O(1))
152.82/59.02	
152.82/59.02	Empty rules are trivially bounded
152.82/59.02	
152.82/59.02	Hurray, we answered YES(O(1),O(n^2))
152.82/59.07	EOF