YES(O(1),O(n^2))
162.00/64.26	YES(O(1),O(n^2))
162.00/64.26	
162.00/64.26	We are left with following problem, upon which TcT provides the
162.00/64.26	certificate YES(O(1),O(n^2)).
162.00/64.26	
162.00/64.26	Strict Trs:
162.00/64.26	  { naiverev(Cons(x, xs)) -> app(naiverev(xs), Cons(x, Nil()))
162.00/64.26	  , naiverev(Nil()) -> Nil()
162.00/64.26	  , app(Cons(x, xs), ys) -> Cons(x, app(xs, ys))
162.00/64.26	  , app(Nil(), ys) -> ys
162.00/64.26	  , notEmpty(Cons(x, xs)) -> True()
162.00/64.26	  , notEmpty(Nil()) -> False()
162.00/64.26	  , goal(xs) -> naiverev(xs) }
162.00/64.26	Obligation:
162.00/64.26	  innermost runtime complexity
162.00/64.26	Answer:
162.00/64.26	  YES(O(1),O(n^2))
162.00/64.26	
162.00/64.26	We add the following dependency tuples:
162.00/64.26	
162.00/64.26	Strict DPs:
162.00/64.26	  { naiverev^#(Cons(x, xs)) ->
162.00/64.26	    c_1(app^#(naiverev(xs), Cons(x, Nil())), naiverev^#(xs))
162.00/64.26	  , naiverev^#(Nil()) -> c_2()
162.00/64.26	  , app^#(Cons(x, xs), ys) -> c_3(app^#(xs, ys))
162.00/64.26	  , app^#(Nil(), ys) -> c_4()
162.00/64.26	  , notEmpty^#(Cons(x, xs)) -> c_5()
162.00/64.26	  , notEmpty^#(Nil()) -> c_6()
162.00/64.26	  , goal^#(xs) -> c_7(naiverev^#(xs)) }
162.00/64.26	
162.00/64.26	and mark the set of starting terms.
162.00/64.26	
162.00/64.26	We are left with following problem, upon which TcT provides the
162.00/64.26	certificate YES(O(1),O(n^2)).
162.00/64.26	
162.00/64.26	Strict DPs:
162.00/64.26	  { naiverev^#(Cons(x, xs)) ->
162.00/64.26	    c_1(app^#(naiverev(xs), Cons(x, Nil())), naiverev^#(xs))
162.00/64.26	  , naiverev^#(Nil()) -> c_2()
162.00/64.26	  , app^#(Cons(x, xs), ys) -> c_3(app^#(xs, ys))
162.00/64.26	  , app^#(Nil(), ys) -> c_4()
162.00/64.26	  , notEmpty^#(Cons(x, xs)) -> c_5()
162.00/64.26	  , notEmpty^#(Nil()) -> c_6()
162.00/64.26	  , goal^#(xs) -> c_7(naiverev^#(xs)) }
162.00/64.26	Weak Trs:
162.00/64.26	  { naiverev(Cons(x, xs)) -> app(naiverev(xs), Cons(x, Nil()))
162.00/64.26	  , naiverev(Nil()) -> Nil()
162.00/64.26	  , app(Cons(x, xs), ys) -> Cons(x, app(xs, ys))
162.00/64.26	  , app(Nil(), ys) -> ys
162.00/64.26	  , notEmpty(Cons(x, xs)) -> True()
162.00/64.26	  , notEmpty(Nil()) -> False()
162.00/64.26	  , goal(xs) -> naiverev(xs) }
162.00/64.26	Obligation:
162.00/64.26	  innermost runtime complexity
162.00/64.26	Answer:
162.00/64.26	  YES(O(1),O(n^2))
162.00/64.26	
162.00/64.26	We estimate the number of application of {2,4,5,6} by applications
162.00/64.26	of Pre({2,4,5,6}) = {1,3,7}. Here rules are labeled as follows:
162.00/64.26	
162.00/64.26	  DPs:
162.00/64.26	    { 1: naiverev^#(Cons(x, xs)) ->
162.00/64.26	         c_1(app^#(naiverev(xs), Cons(x, Nil())), naiverev^#(xs))
162.00/64.26	    , 2: naiverev^#(Nil()) -> c_2()
162.00/64.26	    , 3: app^#(Cons(x, xs), ys) -> c_3(app^#(xs, ys))
162.00/64.26	    , 4: app^#(Nil(), ys) -> c_4()
162.00/64.26	    , 5: notEmpty^#(Cons(x, xs)) -> c_5()
162.00/64.26	    , 6: notEmpty^#(Nil()) -> c_6()
162.00/64.26	    , 7: goal^#(xs) -> c_7(naiverev^#(xs)) }
162.00/64.26	
162.00/64.26	We are left with following problem, upon which TcT provides the
162.00/64.26	certificate YES(O(1),O(n^2)).
162.00/64.26	
162.00/64.26	Strict DPs:
162.00/64.26	  { naiverev^#(Cons(x, xs)) ->
162.00/64.26	    c_1(app^#(naiverev(xs), Cons(x, Nil())), naiverev^#(xs))
162.00/64.26	  , app^#(Cons(x, xs), ys) -> c_3(app^#(xs, ys))
162.00/64.26	  , goal^#(xs) -> c_7(naiverev^#(xs)) }
162.00/64.26	Weak DPs:
162.00/64.26	  { naiverev^#(Nil()) -> c_2()
162.00/64.26	  , app^#(Nil(), ys) -> c_4()
162.00/64.26	  , notEmpty^#(Cons(x, xs)) -> c_5()
162.00/64.26	  , notEmpty^#(Nil()) -> c_6() }
162.00/64.26	Weak Trs:
162.00/64.26	  { naiverev(Cons(x, xs)) -> app(naiverev(xs), Cons(x, Nil()))
162.00/64.26	  , naiverev(Nil()) -> Nil()
162.00/64.26	  , app(Cons(x, xs), ys) -> Cons(x, app(xs, ys))
162.00/64.26	  , app(Nil(), ys) -> ys
162.00/64.26	  , notEmpty(Cons(x, xs)) -> True()
162.00/64.26	  , notEmpty(Nil()) -> False()
162.00/64.26	  , goal(xs) -> naiverev(xs) }
162.00/64.26	Obligation:
162.00/64.26	  innermost runtime complexity
162.00/64.26	Answer:
162.00/64.26	  YES(O(1),O(n^2))
162.00/64.26	
162.00/64.26	The following weak DPs constitute a sub-graph of the DG that is
162.00/64.26	closed under successors. The DPs are removed.
162.00/64.26	
162.00/64.26	{ naiverev^#(Nil()) -> c_2()
162.00/64.26	, app^#(Nil(), ys) -> c_4()
162.00/64.26	, notEmpty^#(Cons(x, xs)) -> c_5()
162.00/64.26	, notEmpty^#(Nil()) -> c_6() }
162.00/64.26	
162.00/64.26	We are left with following problem, upon which TcT provides the
162.00/64.26	certificate YES(O(1),O(n^2)).
162.00/64.26	
162.00/64.26	Strict DPs:
162.00/64.26	  { naiverev^#(Cons(x, xs)) ->
162.00/64.26	    c_1(app^#(naiverev(xs), Cons(x, Nil())), naiverev^#(xs))
162.00/64.26	  , app^#(Cons(x, xs), ys) -> c_3(app^#(xs, ys))
162.00/64.26	  , goal^#(xs) -> c_7(naiverev^#(xs)) }
162.00/64.26	Weak Trs:
162.00/64.26	  { naiverev(Cons(x, xs)) -> app(naiverev(xs), Cons(x, Nil()))
162.00/64.26	  , naiverev(Nil()) -> Nil()
162.00/64.26	  , app(Cons(x, xs), ys) -> Cons(x, app(xs, ys))
162.00/64.26	  , app(Nil(), ys) -> ys
162.00/64.26	  , notEmpty(Cons(x, xs)) -> True()
162.00/64.26	  , notEmpty(Nil()) -> False()
162.00/64.26	  , goal(xs) -> naiverev(xs) }
162.00/64.26	Obligation:
162.00/64.26	  innermost runtime complexity
162.00/64.26	Answer:
162.00/64.26	  YES(O(1),O(n^2))
162.00/64.26	
162.00/64.26	Consider the dependency graph
162.00/64.26	
162.00/64.26	  1: naiverev^#(Cons(x, xs)) ->
162.00/64.26	     c_1(app^#(naiverev(xs), Cons(x, Nil())), naiverev^#(xs))
162.00/64.26	     -->_1 app^#(Cons(x, xs), ys) -> c_3(app^#(xs, ys)) :2
162.00/64.26	     -->_2 naiverev^#(Cons(x, xs)) ->
162.00/64.26	           c_1(app^#(naiverev(xs), Cons(x, Nil())), naiverev^#(xs)) :1
162.00/64.26	  
162.00/64.26	  2: app^#(Cons(x, xs), ys) -> c_3(app^#(xs, ys))
162.00/64.26	     -->_1 app^#(Cons(x, xs), ys) -> c_3(app^#(xs, ys)) :2
162.00/64.26	  
162.00/64.26	  3: goal^#(xs) -> c_7(naiverev^#(xs))
162.00/64.26	     -->_1 naiverev^#(Cons(x, xs)) ->
162.00/64.26	           c_1(app^#(naiverev(xs), Cons(x, Nil())), naiverev^#(xs)) :1
162.00/64.26	  
162.00/64.26	
162.00/64.26	Following roots of the dependency graph are removed, as the
162.00/64.26	considered set of starting terms is closed under reduction with
162.00/64.26	respect to these rules (modulo compound contexts).
162.00/64.26	
162.00/64.26	  { goal^#(xs) -> c_7(naiverev^#(xs)) }
162.00/64.26	
162.00/64.26	
162.00/64.26	We are left with following problem, upon which TcT provides the
162.00/64.26	certificate YES(O(1),O(n^2)).
162.00/64.26	
162.00/64.26	Strict DPs:
162.00/64.26	  { naiverev^#(Cons(x, xs)) ->
162.00/64.26	    c_1(app^#(naiverev(xs), Cons(x, Nil())), naiverev^#(xs))
162.00/64.26	  , app^#(Cons(x, xs), ys) -> c_3(app^#(xs, ys)) }
162.00/64.26	Weak Trs:
162.00/64.26	  { naiverev(Cons(x, xs)) -> app(naiverev(xs), Cons(x, Nil()))
162.00/64.26	  , naiverev(Nil()) -> Nil()
162.00/64.26	  , app(Cons(x, xs), ys) -> Cons(x, app(xs, ys))
162.00/64.26	  , app(Nil(), ys) -> ys
162.00/64.26	  , notEmpty(Cons(x, xs)) -> True()
162.00/64.26	  , notEmpty(Nil()) -> False()
162.00/64.26	  , goal(xs) -> naiverev(xs) }
162.00/64.26	Obligation:
162.00/64.26	  innermost runtime complexity
162.00/64.26	Answer:
162.00/64.26	  YES(O(1),O(n^2))
162.00/64.26	
162.00/64.26	We replace rewrite rules by usable rules:
162.00/64.26	
162.00/64.26	  Weak Usable Rules:
162.00/64.26	    { naiverev(Cons(x, xs)) -> app(naiverev(xs), Cons(x, Nil()))
162.00/64.26	    , naiverev(Nil()) -> Nil()
162.00/64.26	    , app(Cons(x, xs), ys) -> Cons(x, app(xs, ys))
162.00/64.26	    , app(Nil(), ys) -> ys }
162.00/64.26	
162.00/64.26	We are left with following problem, upon which TcT provides the
162.00/64.26	certificate YES(O(1),O(n^2)).
162.00/64.26	
162.00/64.26	Strict DPs:
162.00/64.26	  { naiverev^#(Cons(x, xs)) ->
162.00/64.26	    c_1(app^#(naiverev(xs), Cons(x, Nil())), naiverev^#(xs))
162.00/64.26	  , app^#(Cons(x, xs), ys) -> c_3(app^#(xs, ys)) }
162.00/64.26	Weak Trs:
162.00/64.26	  { naiverev(Cons(x, xs)) -> app(naiverev(xs), Cons(x, Nil()))
162.00/64.26	  , naiverev(Nil()) -> Nil()
162.00/64.26	  , app(Cons(x, xs), ys) -> Cons(x, app(xs, ys))
162.00/64.26	  , app(Nil(), ys) -> ys }
162.00/64.26	Obligation:
162.00/64.26	  innermost runtime complexity
162.00/64.26	Answer:
162.00/64.26	  YES(O(1),O(n^2))
162.00/64.26	
162.00/64.26	We use the processor 'polynomial interpretation' to orient
162.00/64.26	following rules strictly.
162.00/64.26	
162.00/64.26	DPs:
162.00/64.26	  { 1: naiverev^#(Cons(x, xs)) ->
162.00/64.26	       c_1(app^#(naiverev(xs), Cons(x, Nil())), naiverev^#(xs))
162.00/64.26	  , 2: app^#(Cons(x, xs), ys) -> c_3(app^#(xs, ys)) }
162.00/64.26	
162.00/64.26	Sub-proof:
162.00/64.26	----------
162.00/64.26	  We consider the following typing:
162.00/64.26	  
162.00/64.26	    naiverev :: c -> c
162.00/64.26	    Cons :: (a,c) -> c
162.00/64.26	    app :: (c,c) -> c
162.00/64.26	    Nil :: c
162.00/64.26	    naiverev^# :: c -> b
162.00/64.26	    c_1 :: (d,b) -> b
162.00/64.26	    app^# :: (c,c) -> d
162.00/64.26	    c_3 :: d -> d
162.00/64.26	  
162.00/64.26	  The following argument positions are considered usable:
162.00/64.26	  
162.00/64.26	    Uargs(c_1) = {1, 2}, Uargs(c_3) = {1}
162.00/64.26	  
162.00/64.26	  TcT has computed the following constructor-restricted
162.00/64.26	  typedpolynomial interpretation.
162.00/64.26	  
162.00/64.26	    [naiverev](x1) = x1       
162.00/64.26	                              
162.00/64.26	    [Cons](x1, x2) = 1 + x2   
162.00/64.26	                              
162.00/64.26	     [app](x1, x2) = x1 + x2  
162.00/64.26	                              
162.00/64.26	           [Nil]() = 0        
162.00/64.26	                              
162.00/64.26	  [naiverev^#](x1) = 2*x1^2   
162.00/64.26	                              
162.00/64.26	     [c_1](x1, x2) = 2*x1 + x2
162.00/64.26	                              
162.00/64.26	   [app^#](x1, x2) = 2*x1     
162.00/64.26	                              
162.00/64.26	         [c_3](x1) = x1       
162.00/64.26	                              
162.00/64.26	  
162.00/64.26	  This order satisfies the following ordering constraints.
162.00/64.26	  
162.00/64.26	      [naiverev(Cons(x, xs))] =  1 + xs                                                    
162.00/64.26	                              >= xs + 1                                                    
162.00/64.26	                              =  [app(naiverev(xs), Cons(x, Nil()))]                       
162.00/64.26	                                                                                           
162.00/64.26	            [naiverev(Nil())] =                                                            
162.00/64.26	                              >=                                                           
162.00/64.26	                              =  [Nil()]                                                   
162.00/64.26	                                                                                           
162.00/64.26	       [app(Cons(x, xs), ys)] =  1 + xs + ys                                               
162.00/64.26	                              >= 1 + xs + ys                                               
162.00/64.26	                              =  [Cons(x, app(xs, ys))]                                    
162.00/64.26	                                                                                           
162.00/64.26	             [app(Nil(), ys)] =  ys                                                        
162.00/64.26	                              >= ys                                                        
162.00/64.26	                              =  [ys]                                                      
162.00/64.26	                                                                                           
162.00/64.26	    [naiverev^#(Cons(x, xs))] =  2 + 4*xs + 2*xs^2                                         
162.00/64.26	                              >  4*xs + 2*xs^2                                             
162.00/64.26	                              =  [c_1(app^#(naiverev(xs), Cons(x, Nil())), naiverev^#(xs))]
162.00/64.26	                                                                                           
162.00/64.26	     [app^#(Cons(x, xs), ys)] =  2 + 2*xs                                                  
162.00/64.26	                              >  2*xs                                                      
162.00/64.26	                              =  [c_3(app^#(xs, ys))]                                      
162.00/64.26	                                                                                           
162.00/64.26	
162.00/64.26	The strictly oriented rules are moved into the weak component.
162.00/64.26	
162.00/64.26	We are left with following problem, upon which TcT provides the
162.00/64.26	certificate YES(O(1),O(1)).
162.00/64.26	
162.00/64.26	Weak DPs:
162.00/64.26	  { naiverev^#(Cons(x, xs)) ->
162.00/64.26	    c_1(app^#(naiverev(xs), Cons(x, Nil())), naiverev^#(xs))
162.00/64.26	  , app^#(Cons(x, xs), ys) -> c_3(app^#(xs, ys)) }
162.00/64.26	Weak Trs:
162.00/64.26	  { naiverev(Cons(x, xs)) -> app(naiverev(xs), Cons(x, Nil()))
162.00/64.26	  , naiverev(Nil()) -> Nil()
162.00/64.26	  , app(Cons(x, xs), ys) -> Cons(x, app(xs, ys))
162.00/64.26	  , app(Nil(), ys) -> ys }
162.00/64.26	Obligation:
162.00/64.26	  innermost runtime complexity
162.00/64.26	Answer:
162.00/64.26	  YES(O(1),O(1))
162.00/64.26	
162.00/64.26	The following weak DPs constitute a sub-graph of the DG that is
162.00/64.26	closed under successors. The DPs are removed.
162.00/64.26	
162.00/64.26	{ naiverev^#(Cons(x, xs)) ->
162.00/64.26	  c_1(app^#(naiverev(xs), Cons(x, Nil())), naiverev^#(xs))
162.00/64.26	, app^#(Cons(x, xs), ys) -> c_3(app^#(xs, ys)) }
162.00/64.26	
162.00/64.26	We are left with following problem, upon which TcT provides the
162.00/64.26	certificate YES(O(1),O(1)).
162.00/64.26	
162.00/64.26	Weak Trs:
162.00/64.26	  { naiverev(Cons(x, xs)) -> app(naiverev(xs), Cons(x, Nil()))
162.00/64.26	  , naiverev(Nil()) -> Nil()
162.00/64.26	  , app(Cons(x, xs), ys) -> Cons(x, app(xs, ys))
162.00/64.26	  , app(Nil(), ys) -> ys }
162.00/64.26	Obligation:
162.00/64.26	  innermost runtime complexity
162.00/64.26	Answer:
162.00/64.26	  YES(O(1),O(1))
162.00/64.26	
162.00/64.26	No rule is usable, rules are removed from the input problem.
162.00/64.26	
162.00/64.26	We are left with following problem, upon which TcT provides the
162.00/64.26	certificate YES(O(1),O(1)).
162.00/64.26	
162.00/64.26	Rules: Empty
162.00/64.26	Obligation:
162.00/64.26	  innermost runtime complexity
162.00/64.26	Answer:
162.00/64.26	  YES(O(1),O(1))
162.00/64.26	
162.00/64.26	Empty rules are trivially bounded
162.00/64.26	
162.00/64.26	Hurray, we answered YES(O(1),O(n^2))
162.26/64.32	EOF