YES(O(1),O(n^1))
9.77/2.83	YES(O(1),O(n^1))
9.77/2.83	
9.77/2.83	We are left with following problem, upon which TcT provides the
9.77/2.83	certificate YES(O(1),O(n^1)).
9.77/2.83	
9.77/2.83	Strict Trs:
9.77/2.83	  { a__and(X1, X2) -> and(X1, X2)
9.77/2.83	  , a__and(true(), X) -> mark(X)
9.77/2.83	  , a__and(false(), Y) -> false()
9.77/2.83	  , mark(true()) -> true()
9.77/2.83	  , mark(false()) -> false()
9.77/2.83	  , mark(0()) -> 0()
9.77/2.83	  , mark(s(X)) -> s(X)
9.77/2.83	  , mark(add(X1, X2)) -> a__add(mark(X1), X2)
9.77/2.83	  , mark(nil()) -> nil()
9.77/2.83	  , mark(cons(X1, X2)) -> cons(X1, X2)
9.77/2.83	  , mark(first(X1, X2)) -> a__first(mark(X1), mark(X2))
9.77/2.83	  , mark(from(X)) -> a__from(X)
9.77/2.83	  , mark(and(X1, X2)) -> a__and(mark(X1), X2)
9.77/2.83	  , mark(if(X1, X2, X3)) -> a__if(mark(X1), X2, X3)
9.77/2.83	  , a__if(X1, X2, X3) -> if(X1, X2, X3)
9.77/2.83	  , a__if(true(), X, Y) -> mark(X)
9.77/2.83	  , a__if(false(), X, Y) -> mark(Y)
9.77/2.83	  , a__add(X1, X2) -> add(X1, X2)
9.77/2.83	  , a__add(0(), X) -> mark(X)
9.77/2.83	  , a__add(s(X), Y) -> s(add(X, Y))
9.77/2.83	  , a__first(X1, X2) -> first(X1, X2)
9.77/2.83	  , a__first(0(), X) -> nil()
9.77/2.83	  , a__first(s(X), cons(Y, Z)) -> cons(Y, first(X, Z))
9.77/2.83	  , a__from(X) -> cons(X, from(s(X)))
9.77/2.83	  , a__from(X) -> from(X) }
9.77/2.83	Obligation:
9.77/2.83	  innermost runtime complexity
9.77/2.83	Answer:
9.77/2.83	  YES(O(1),O(n^1))
9.77/2.83	
9.77/2.83	The weightgap principle applies (using the following nonconstant
9.77/2.83	growth matrix-interpretation)
9.77/2.83	
9.77/2.83	The following argument positions are usable:
9.77/2.83	  Uargs(a__and) = {1}, Uargs(a__if) = {1}, Uargs(a__add) = {1},
9.77/2.83	  Uargs(a__first) = {1, 2}
9.77/2.83	
9.77/2.83	TcT has computed the following matrix interpretation satisfying
9.77/2.83	not(EDA) and not(IDA(1)).
9.77/2.83	
9.77/2.83	     [a__and](x1, x2) = [1] x1 + [0]         
9.77/2.83	                                             
9.77/2.83	               [true] = [0]                  
9.77/2.83	                                             
9.77/2.83	           [mark](x1) = [0]                  
9.77/2.83	                                             
9.77/2.83	              [false] = [0]                  
9.77/2.83	                                             
9.77/2.83	  [a__if](x1, x2, x3) = [1] x1 + [0]         
9.77/2.83	                                             
9.77/2.83	     [a__add](x1, x2) = [1] x1 + [0]         
9.77/2.83	                                             
9.77/2.83	                  [0] = [0]                  
9.77/2.83	                                             
9.77/2.83	              [s](x1) = [0]                  
9.77/2.83	                                             
9.77/2.83	        [add](x1, x2) = [1] x1 + [5]         
9.77/2.83	                                             
9.77/2.83	   [a__first](x1, x2) = [1] x1 + [1] x2 + [0]
9.77/2.83	                                             
9.77/2.83	                [nil] = [7]                  
9.77/2.83	                                             
9.77/2.83	       [cons](x1, x2) = [0]                  
9.77/2.83	                                             
9.77/2.83	      [first](x1, x2) = [1] x1 + [1] x2 + [5]
9.77/2.83	                                             
9.77/2.83	        [a__from](x1) = [5]                  
9.77/2.83	                                             
9.77/2.83	           [from](x1) = [5]                  
9.77/2.83	                                             
9.77/2.83	        [and](x1, x2) = [1] x1 + [7]         
9.77/2.83	                                             
9.77/2.83	     [if](x1, x2, x3) = [1] x1 + [7]         
9.77/2.83	
9.77/2.83	The order satisfies the following ordering constraints:
9.77/2.83	
9.77/2.83	              [a__and(X1, X2)] =  [1] X1 + [0]                  
9.77/2.83	                               ?  [1] X1 + [7]                  
9.77/2.83	                               =  [and(X1, X2)]                 
9.77/2.83	                                                                
9.77/2.83	           [a__and(true(), X)] =  [0]                           
9.77/2.83	                               >= [0]                           
9.77/2.83	                               =  [mark(X)]                     
9.77/2.83	                                                                
9.77/2.83	          [a__and(false(), Y)] =  [0]                           
9.77/2.83	                               >= [0]                           
9.77/2.83	                               =  [false()]                     
9.77/2.83	                                                                
9.77/2.83	                [mark(true())] =  [0]                           
9.77/2.83	                               >= [0]                           
9.77/2.83	                               =  [true()]                      
9.77/2.83	                                                                
9.77/2.83	               [mark(false())] =  [0]                           
9.77/2.83	                               >= [0]                           
9.77/2.83	                               =  [false()]                     
9.77/2.83	                                                                
9.77/2.83	                   [mark(0())] =  [0]                           
9.77/2.83	                               >= [0]                           
9.77/2.83	                               =  [0()]                         
9.77/2.83	                                                                
9.77/2.83	                  [mark(s(X))] =  [0]                           
9.77/2.83	                               >= [0]                           
9.77/2.83	                               =  [s(X)]                        
9.77/2.83	                                                                
9.77/2.83	           [mark(add(X1, X2))] =  [0]                           
9.77/2.83	                               >= [0]                           
9.77/2.83	                               =  [a__add(mark(X1), X2)]        
9.77/2.83	                                                                
9.77/2.83	                 [mark(nil())] =  [0]                           
9.77/2.83	                               ?  [7]                           
9.77/2.83	                               =  [nil()]                       
9.77/2.83	                                                                
9.77/2.83	          [mark(cons(X1, X2))] =  [0]                           
9.77/2.83	                               >= [0]                           
9.77/2.83	                               =  [cons(X1, X2)]                
9.77/2.83	                                                                
9.77/2.83	         [mark(first(X1, X2))] =  [0]                           
9.77/2.83	                               >= [0]                           
9.77/2.83	                               =  [a__first(mark(X1), mark(X2))]
9.77/2.83	                                                                
9.77/2.83	               [mark(from(X))] =  [0]                           
9.77/2.83	                               ?  [5]                           
9.77/2.83	                               =  [a__from(X)]                  
9.77/2.83	                                                                
9.77/2.83	           [mark(and(X1, X2))] =  [0]                           
9.77/2.83	                               >= [0]                           
9.77/2.83	                               =  [a__and(mark(X1), X2)]        
9.77/2.83	                                                                
9.77/2.83	        [mark(if(X1, X2, X3))] =  [0]                           
9.77/2.83	                               >= [0]                           
9.77/2.83	                               =  [a__if(mark(X1), X2, X3)]     
9.77/2.83	                                                                
9.77/2.83	           [a__if(X1, X2, X3)] =  [1] X1 + [0]                  
9.77/2.83	                               ?  [1] X1 + [7]                  
9.77/2.83	                               =  [if(X1, X2, X3)]              
9.77/2.83	                                                                
9.77/2.83	         [a__if(true(), X, Y)] =  [0]                           
9.77/2.83	                               >= [0]                           
9.77/2.83	                               =  [mark(X)]                     
9.77/2.83	                                                                
9.77/2.83	        [a__if(false(), X, Y)] =  [0]                           
9.77/2.83	                               >= [0]                           
9.77/2.83	                               =  [mark(Y)]                     
9.77/2.83	                                                                
9.77/2.83	              [a__add(X1, X2)] =  [1] X1 + [0]                  
9.77/2.83	                               ?  [1] X1 + [5]                  
9.77/2.83	                               =  [add(X1, X2)]                 
9.77/2.83	                                                                
9.77/2.83	              [a__add(0(), X)] =  [0]                           
9.77/2.83	                               >= [0]                           
9.77/2.83	                               =  [mark(X)]                     
9.77/2.83	                                                                
9.77/2.83	             [a__add(s(X), Y)] =  [0]                           
9.77/2.83	                               >= [0]                           
9.77/2.83	                               =  [s(add(X, Y))]                
9.77/2.83	                                                                
9.77/2.83	            [a__first(X1, X2)] =  [1] X1 + [1] X2 + [0]         
9.77/2.83	                               ?  [1] X1 + [1] X2 + [5]         
9.77/2.83	                               =  [first(X1, X2)]               
9.77/2.83	                                                                
9.77/2.83	            [a__first(0(), X)] =  [1] X + [0]                   
9.77/2.83	                               ?  [7]                           
9.77/2.83	                               =  [nil()]                       
9.77/2.83	                                                                
9.77/2.83	  [a__first(s(X), cons(Y, Z))] =  [0]                           
9.77/2.83	                               >= [0]                           
9.77/2.83	                               =  [cons(Y, first(X, Z))]        
9.77/2.83	                                                                
9.77/2.83	                  [a__from(X)] =  [5]                           
9.77/2.83	                               >  [0]                           
9.77/2.83	                               =  [cons(X, from(s(X)))]         
9.77/2.83	                                                                
9.77/2.83	                  [a__from(X)] =  [5]                           
9.77/2.83	                               >= [5]                           
9.77/2.83	                               =  [from(X)]                     
9.77/2.83	                                                                
9.77/2.83	
9.77/2.83	Further, it can be verified that all rules not oriented are covered by the weightgap condition.
9.77/2.83	
9.77/2.83	We are left with following problem, upon which TcT provides the
9.77/2.83	certificate YES(O(1),O(n^1)).
9.77/2.83	
9.77/2.83	Strict Trs:
9.77/2.83	  { a__and(X1, X2) -> and(X1, X2)
9.77/2.83	  , a__and(true(), X) -> mark(X)
9.77/2.83	  , a__and(false(), Y) -> false()
9.77/2.83	  , mark(true()) -> true()
9.77/2.83	  , mark(false()) -> false()
9.77/2.83	  , mark(0()) -> 0()
9.77/2.83	  , mark(s(X)) -> s(X)
9.77/2.83	  , mark(add(X1, X2)) -> a__add(mark(X1), X2)
9.77/2.83	  , mark(nil()) -> nil()
9.77/2.83	  , mark(cons(X1, X2)) -> cons(X1, X2)
9.77/2.83	  , mark(first(X1, X2)) -> a__first(mark(X1), mark(X2))
9.77/2.83	  , mark(from(X)) -> a__from(X)
9.77/2.83	  , mark(and(X1, X2)) -> a__and(mark(X1), X2)
9.77/2.83	  , mark(if(X1, X2, X3)) -> a__if(mark(X1), X2, X3)
9.77/2.83	  , a__if(X1, X2, X3) -> if(X1, X2, X3)
9.77/2.83	  , a__if(true(), X, Y) -> mark(X)
9.77/2.83	  , a__if(false(), X, Y) -> mark(Y)
9.77/2.83	  , a__add(X1, X2) -> add(X1, X2)
9.77/2.83	  , a__add(0(), X) -> mark(X)
9.77/2.83	  , a__add(s(X), Y) -> s(add(X, Y))
9.77/2.83	  , a__first(X1, X2) -> first(X1, X2)
9.77/2.83	  , a__first(0(), X) -> nil()
9.77/2.83	  , a__first(s(X), cons(Y, Z)) -> cons(Y, first(X, Z))
9.77/2.83	  , a__from(X) -> from(X) }
9.77/2.83	Weak Trs: { a__from(X) -> cons(X, from(s(X))) }
9.77/2.83	Obligation:
9.77/2.83	  innermost runtime complexity
9.77/2.83	Answer:
9.77/2.83	  YES(O(1),O(n^1))
9.77/2.83	
9.77/2.83	The weightgap principle applies (using the following nonconstant
9.77/2.83	growth matrix-interpretation)
9.77/2.83	
9.77/2.83	The following argument positions are usable:
9.77/2.83	  Uargs(a__and) = {1}, Uargs(a__if) = {1}, Uargs(a__add) = {1},
9.77/2.83	  Uargs(a__first) = {1, 2}
9.77/2.83	
9.77/2.83	TcT has computed the following matrix interpretation satisfying
9.77/2.83	not(EDA) and not(IDA(1)).
9.77/2.83	
9.77/2.83	     [a__and](x1, x2) = [1] x1 + [4]         
9.77/2.83	                                             
9.77/2.83	               [true] = [0]                  
9.77/2.83	                                             
9.77/2.83	           [mark](x1) = [0]                  
9.77/2.83	                                             
9.77/2.83	              [false] = [0]                  
9.77/2.83	                                             
9.77/2.83	  [a__if](x1, x2, x3) = [1] x1 + [0]         
9.77/2.83	                                             
9.77/2.83	     [a__add](x1, x2) = [1] x1 + [0]         
9.77/2.83	                                             
9.77/2.83	                  [0] = [0]                  
9.77/2.83	                                             
9.77/2.83	              [s](x1) = [0]                  
9.77/2.83	                                             
9.77/2.83	        [add](x1, x2) = [1] x1 + [5]         
9.77/2.83	                                             
9.77/2.83	   [a__first](x1, x2) = [1] x1 + [1] x2 + [0]
9.77/2.83	                                             
9.77/2.83	                [nil] = [7]                  
9.77/2.83	                                             
9.77/2.83	       [cons](x1, x2) = [0]                  
9.77/2.83	                                             
9.77/2.83	      [first](x1, x2) = [1] x1 + [1] x2 + [5]
9.77/2.83	                                             
9.77/2.83	        [a__from](x1) = [5]                  
9.77/2.83	                                             
9.77/2.83	           [from](x1) = [5]                  
9.77/2.83	                                             
9.77/2.83	        [and](x1, x2) = [1] x1 + [3]         
9.77/2.83	                                             
9.77/2.83	     [if](x1, x2, x3) = [1] x1 + [7]         
9.77/2.83	
9.77/2.83	The order satisfies the following ordering constraints:
9.77/2.83	
9.77/2.83	              [a__and(X1, X2)] =  [1] X1 + [4]                  
9.77/2.83	                               >  [1] X1 + [3]                  
9.77/2.83	                               =  [and(X1, X2)]                 
9.77/2.83	                                                                
9.77/2.83	           [a__and(true(), X)] =  [4]                           
9.77/2.83	                               >  [0]                           
9.77/2.83	                               =  [mark(X)]                     
9.77/2.83	                                                                
9.77/2.83	          [a__and(false(), Y)] =  [4]                           
9.77/2.83	                               >  [0]                           
9.77/2.83	                               =  [false()]                     
9.77/2.83	                                                                
9.77/2.83	                [mark(true())] =  [0]                           
9.77/2.83	                               >= [0]                           
9.77/2.83	                               =  [true()]                      
9.77/2.83	                                                                
9.77/2.83	               [mark(false())] =  [0]                           
9.77/2.83	                               >= [0]                           
9.77/2.83	                               =  [false()]                     
9.77/2.83	                                                                
9.77/2.83	                   [mark(0())] =  [0]                           
9.77/2.83	                               >= [0]                           
9.77/2.83	                               =  [0()]                         
9.77/2.83	                                                                
9.77/2.83	                  [mark(s(X))] =  [0]                           
9.77/2.83	                               >= [0]                           
9.77/2.83	                               =  [s(X)]                        
9.77/2.83	                                                                
9.77/2.83	           [mark(add(X1, X2))] =  [0]                           
9.77/2.83	                               >= [0]                           
9.77/2.83	                               =  [a__add(mark(X1), X2)]        
9.77/2.83	                                                                
9.77/2.83	                 [mark(nil())] =  [0]                           
9.77/2.83	                               ?  [7]                           
9.77/2.83	                               =  [nil()]                       
9.77/2.83	                                                                
9.77/2.83	          [mark(cons(X1, X2))] =  [0]                           
9.77/2.83	                               >= [0]                           
9.77/2.83	                               =  [cons(X1, X2)]                
9.77/2.83	                                                                
9.77/2.83	         [mark(first(X1, X2))] =  [0]                           
9.77/2.83	                               >= [0]                           
9.77/2.83	                               =  [a__first(mark(X1), mark(X2))]
9.77/2.83	                                                                
9.77/2.83	               [mark(from(X))] =  [0]                           
9.77/2.83	                               ?  [5]                           
9.77/2.83	                               =  [a__from(X)]                  
9.77/2.83	                                                                
9.77/2.83	           [mark(and(X1, X2))] =  [0]                           
9.77/2.83	                               ?  [4]                           
9.77/2.83	                               =  [a__and(mark(X1), X2)]        
9.77/2.83	                                                                
9.77/2.83	        [mark(if(X1, X2, X3))] =  [0]                           
9.77/2.83	                               >= [0]                           
9.77/2.83	                               =  [a__if(mark(X1), X2, X3)]     
9.77/2.83	                                                                
9.77/2.83	           [a__if(X1, X2, X3)] =  [1] X1 + [0]                  
9.77/2.83	                               ?  [1] X1 + [7]                  
9.77/2.83	                               =  [if(X1, X2, X3)]              
9.77/2.83	                                                                
9.77/2.83	         [a__if(true(), X, Y)] =  [0]                           
9.77/2.83	                               >= [0]                           
9.77/2.83	                               =  [mark(X)]                     
9.77/2.83	                                                                
9.77/2.83	        [a__if(false(), X, Y)] =  [0]                           
9.77/2.83	                               >= [0]                           
9.77/2.83	                               =  [mark(Y)]                     
9.77/2.83	                                                                
9.77/2.83	              [a__add(X1, X2)] =  [1] X1 + [0]                  
9.77/2.83	                               ?  [1] X1 + [5]                  
9.77/2.83	                               =  [add(X1, X2)]                 
9.77/2.83	                                                                
9.77/2.83	              [a__add(0(), X)] =  [0]                           
9.77/2.83	                               >= [0]                           
9.77/2.83	                               =  [mark(X)]                     
9.77/2.83	                                                                
9.77/2.83	             [a__add(s(X), Y)] =  [0]                           
9.77/2.83	                               >= [0]                           
9.77/2.83	                               =  [s(add(X, Y))]                
9.77/2.83	                                                                
9.77/2.83	            [a__first(X1, X2)] =  [1] X1 + [1] X2 + [0]         
9.77/2.83	                               ?  [1] X1 + [1] X2 + [5]         
9.77/2.83	                               =  [first(X1, X2)]               
9.77/2.83	                                                                
9.77/2.83	            [a__first(0(), X)] =  [1] X + [0]                   
9.77/2.83	                               ?  [7]                           
9.77/2.83	                               =  [nil()]                       
9.77/2.83	                                                                
9.77/2.83	  [a__first(s(X), cons(Y, Z))] =  [0]                           
9.77/2.83	                               >= [0]                           
9.77/2.83	                               =  [cons(Y, first(X, Z))]        
9.77/2.83	                                                                
9.77/2.83	                  [a__from(X)] =  [5]                           
9.77/2.83	                               >  [0]                           
9.77/2.83	                               =  [cons(X, from(s(X)))]         
9.77/2.83	                                                                
9.77/2.83	                  [a__from(X)] =  [5]                           
9.77/2.83	                               >= [5]                           
9.77/2.83	                               =  [from(X)]                     
9.77/2.83	                                                                
9.77/2.83	
9.77/2.83	Further, it can be verified that all rules not oriented are covered by the weightgap condition.
9.77/2.83	
9.77/2.83	We are left with following problem, upon which TcT provides the
9.77/2.83	certificate YES(O(1),O(n^1)).
9.77/2.83	
9.77/2.83	Strict Trs:
9.77/2.83	  { mark(true()) -> true()
9.77/2.83	  , mark(false()) -> false()
9.77/2.83	  , mark(0()) -> 0()
9.77/2.83	  , mark(s(X)) -> s(X)
9.77/2.83	  , mark(add(X1, X2)) -> a__add(mark(X1), X2)
9.77/2.83	  , mark(nil()) -> nil()
9.77/2.83	  , mark(cons(X1, X2)) -> cons(X1, X2)
9.77/2.83	  , mark(first(X1, X2)) -> a__first(mark(X1), mark(X2))
9.77/2.83	  , mark(from(X)) -> a__from(X)
9.77/2.83	  , mark(and(X1, X2)) -> a__and(mark(X1), X2)
9.77/2.83	  , mark(if(X1, X2, X3)) -> a__if(mark(X1), X2, X3)
9.77/2.83	  , a__if(X1, X2, X3) -> if(X1, X2, X3)
9.77/2.83	  , a__if(true(), X, Y) -> mark(X)
9.77/2.83	  , a__if(false(), X, Y) -> mark(Y)
9.77/2.83	  , a__add(X1, X2) -> add(X1, X2)
9.77/2.83	  , a__add(0(), X) -> mark(X)
9.77/2.83	  , a__add(s(X), Y) -> s(add(X, Y))
9.77/2.83	  , a__first(X1, X2) -> first(X1, X2)
9.77/2.83	  , a__first(0(), X) -> nil()
9.77/2.83	  , a__first(s(X), cons(Y, Z)) -> cons(Y, first(X, Z))
9.77/2.83	  , a__from(X) -> from(X) }
9.77/2.83	Weak Trs:
9.77/2.83	  { a__and(X1, X2) -> and(X1, X2)
9.77/2.83	  , a__and(true(), X) -> mark(X)
9.77/2.83	  , a__and(false(), Y) -> false()
9.77/2.83	  , a__from(X) -> cons(X, from(s(X))) }
9.77/2.83	Obligation:
9.77/2.83	  innermost runtime complexity
9.77/2.83	Answer:
9.77/2.83	  YES(O(1),O(n^1))
9.77/2.83	
9.77/2.83	The weightgap principle applies (using the following nonconstant
9.77/2.83	growth matrix-interpretation)
9.77/2.83	
9.77/2.83	The following argument positions are usable:
9.77/2.83	  Uargs(a__and) = {1}, Uargs(a__if) = {1}, Uargs(a__add) = {1},
9.77/2.83	  Uargs(a__first) = {1, 2}
9.77/2.83	
9.77/2.83	TcT has computed the following matrix interpretation satisfying
9.77/2.83	not(EDA) and not(IDA(1)).
9.77/2.83	
9.77/2.83	     [a__and](x1, x2) = [1] x1 + [4]         
9.77/2.83	                                             
9.77/2.83	               [true] = [0]                  
9.77/2.83	                                             
9.77/2.83	           [mark](x1) = [0]                  
9.77/2.83	                                             
9.77/2.83	              [false] = [0]                  
9.77/2.83	                                             
9.77/2.83	  [a__if](x1, x2, x3) = [1] x1 + [4]         
9.77/2.83	                                             
9.77/2.83	     [a__add](x1, x2) = [1] x1 + [0]         
9.77/2.83	                                             
9.77/2.83	                  [0] = [0]                  
9.77/2.83	                                             
9.77/2.83	              [s](x1) = [0]                  
9.77/2.83	                                             
9.77/2.83	        [add](x1, x2) = [1] x1 + [5]         
9.77/2.83	                                             
9.77/2.83	   [a__first](x1, x2) = [1] x1 + [1] x2 + [0]
9.77/2.83	                                             
9.77/2.83	                [nil] = [7]                  
9.77/2.83	                                             
9.77/2.83	       [cons](x1, x2) = [0]                  
9.77/2.83	                                             
9.77/2.83	      [first](x1, x2) = [1] x1 + [1] x2 + [5]
9.77/2.83	                                             
9.77/2.83	        [a__from](x1) = [5]                  
9.77/2.83	                                             
9.77/2.83	           [from](x1) = [5]                  
9.77/2.83	                                             
9.77/2.83	        [and](x1, x2) = [1] x1 + [3]         
9.77/2.83	                                             
9.77/2.83	     [if](x1, x2, x3) = [1] x1 + [7]         
9.77/2.83	
9.77/2.83	The order satisfies the following ordering constraints:
9.77/2.83	
9.77/2.83	              [a__and(X1, X2)] =  [1] X1 + [4]                  
9.77/2.83	                               >  [1] X1 + [3]                  
9.77/2.83	                               =  [and(X1, X2)]                 
9.77/2.83	                                                                
9.77/2.83	           [a__and(true(), X)] =  [4]                           
9.77/2.83	                               >  [0]                           
9.77/2.83	                               =  [mark(X)]                     
9.77/2.83	                                                                
9.77/2.83	          [a__and(false(), Y)] =  [4]                           
9.77/2.83	                               >  [0]                           
9.77/2.83	                               =  [false()]                     
9.77/2.83	                                                                
9.77/2.83	                [mark(true())] =  [0]                           
9.77/2.83	                               >= [0]                           
9.77/2.83	                               =  [true()]                      
9.77/2.83	                                                                
9.77/2.83	               [mark(false())] =  [0]                           
9.77/2.83	                               >= [0]                           
9.77/2.83	                               =  [false()]                     
9.77/2.83	                                                                
9.77/2.83	                   [mark(0())] =  [0]                           
9.77/2.83	                               >= [0]                           
9.77/2.83	                               =  [0()]                         
9.77/2.83	                                                                
9.77/2.83	                  [mark(s(X))] =  [0]                           
9.77/2.83	                               >= [0]                           
9.77/2.83	                               =  [s(X)]                        
9.77/2.83	                                                                
9.77/2.83	           [mark(add(X1, X2))] =  [0]                           
9.77/2.83	                               >= [0]                           
9.77/2.83	                               =  [a__add(mark(X1), X2)]        
9.77/2.83	                                                                
9.77/2.83	                 [mark(nil())] =  [0]                           
9.77/2.83	                               ?  [7]                           
9.77/2.83	                               =  [nil()]                       
9.77/2.83	                                                                
9.77/2.83	          [mark(cons(X1, X2))] =  [0]                           
9.77/2.83	                               >= [0]                           
9.77/2.83	                               =  [cons(X1, X2)]                
9.77/2.83	                                                                
9.77/2.83	         [mark(first(X1, X2))] =  [0]                           
9.77/2.83	                               >= [0]                           
9.77/2.83	                               =  [a__first(mark(X1), mark(X2))]
9.77/2.83	                                                                
9.77/2.83	               [mark(from(X))] =  [0]                           
9.77/2.83	                               ?  [5]                           
9.77/2.83	                               =  [a__from(X)]                  
9.77/2.83	                                                                
9.77/2.83	           [mark(and(X1, X2))] =  [0]                           
9.77/2.83	                               ?  [4]                           
9.77/2.83	                               =  [a__and(mark(X1), X2)]        
9.77/2.83	                                                                
9.77/2.83	        [mark(if(X1, X2, X3))] =  [0]                           
9.77/2.83	                               ?  [4]                           
9.77/2.83	                               =  [a__if(mark(X1), X2, X3)]     
9.77/2.83	                                                                
9.77/2.83	           [a__if(X1, X2, X3)] =  [1] X1 + [4]                  
9.77/2.83	                               ?  [1] X1 + [7]                  
9.77/2.83	                               =  [if(X1, X2, X3)]              
9.77/2.83	                                                                
9.77/2.83	         [a__if(true(), X, Y)] =  [4]                           
9.77/2.83	                               >  [0]                           
9.77/2.83	                               =  [mark(X)]                     
9.77/2.83	                                                                
9.77/2.83	        [a__if(false(), X, Y)] =  [4]                           
9.77/2.83	                               >  [0]                           
9.77/2.83	                               =  [mark(Y)]                     
9.77/2.83	                                                                
9.77/2.83	              [a__add(X1, X2)] =  [1] X1 + [0]                  
9.77/2.83	                               ?  [1] X1 + [5]                  
9.77/2.83	                               =  [add(X1, X2)]                 
9.77/2.83	                                                                
9.77/2.83	              [a__add(0(), X)] =  [0]                           
9.77/2.83	                               >= [0]                           
9.77/2.83	                               =  [mark(X)]                     
9.77/2.83	                                                                
9.77/2.83	             [a__add(s(X), Y)] =  [0]                           
9.77/2.83	                               >= [0]                           
9.77/2.83	                               =  [s(add(X, Y))]                
9.77/2.83	                                                                
9.77/2.83	            [a__first(X1, X2)] =  [1] X1 + [1] X2 + [0]         
9.77/2.83	                               ?  [1] X1 + [1] X2 + [5]         
9.77/2.83	                               =  [first(X1, X2)]               
9.77/2.83	                                                                
9.77/2.83	            [a__first(0(), X)] =  [1] X + [0]                   
9.77/2.83	                               ?  [7]                           
9.77/2.83	                               =  [nil()]                       
9.77/2.83	                                                                
9.77/2.83	  [a__first(s(X), cons(Y, Z))] =  [0]                           
9.77/2.83	                               >= [0]                           
9.77/2.83	                               =  [cons(Y, first(X, Z))]        
9.77/2.83	                                                                
9.77/2.83	                  [a__from(X)] =  [5]                           
9.77/2.83	                               >  [0]                           
9.77/2.83	                               =  [cons(X, from(s(X)))]         
9.77/2.83	                                                                
9.77/2.83	                  [a__from(X)] =  [5]                           
9.77/2.83	                               >= [5]                           
9.77/2.83	                               =  [from(X)]                     
9.77/2.83	                                                                
9.77/2.83	
9.77/2.83	Further, it can be verified that all rules not oriented are covered by the weightgap condition.
9.77/2.83	
9.77/2.83	We are left with following problem, upon which TcT provides the
9.77/2.83	certificate YES(O(1),O(n^1)).
9.77/2.83	
9.77/2.83	Strict Trs:
9.77/2.83	  { mark(true()) -> true()
9.77/2.83	  , mark(false()) -> false()
9.77/2.83	  , mark(0()) -> 0()
9.77/2.83	  , mark(s(X)) -> s(X)
9.77/2.83	  , mark(add(X1, X2)) -> a__add(mark(X1), X2)
9.77/2.83	  , mark(nil()) -> nil()
9.77/2.83	  , mark(cons(X1, X2)) -> cons(X1, X2)
9.77/2.83	  , mark(first(X1, X2)) -> a__first(mark(X1), mark(X2))
9.77/2.83	  , mark(from(X)) -> a__from(X)
9.77/2.83	  , mark(and(X1, X2)) -> a__and(mark(X1), X2)
9.77/2.83	  , mark(if(X1, X2, X3)) -> a__if(mark(X1), X2, X3)
9.77/2.83	  , a__if(X1, X2, X3) -> if(X1, X2, X3)
9.77/2.83	  , a__add(X1, X2) -> add(X1, X2)
9.77/2.83	  , a__add(0(), X) -> mark(X)
9.77/2.83	  , a__add(s(X), Y) -> s(add(X, Y))
9.77/2.83	  , a__first(X1, X2) -> first(X1, X2)
9.77/2.83	  , a__first(0(), X) -> nil()
9.77/2.83	  , a__first(s(X), cons(Y, Z)) -> cons(Y, first(X, Z))
9.77/2.83	  , a__from(X) -> from(X) }
9.77/2.83	Weak Trs:
9.77/2.83	  { a__and(X1, X2) -> and(X1, X2)
9.77/2.83	  , a__and(true(), X) -> mark(X)
9.77/2.83	  , a__and(false(), Y) -> false()
9.77/2.83	  , a__if(true(), X, Y) -> mark(X)
9.77/2.83	  , a__if(false(), X, Y) -> mark(Y)
9.77/2.83	  , a__from(X) -> cons(X, from(s(X))) }
9.77/2.83	Obligation:
9.77/2.83	  innermost runtime complexity
9.77/2.83	Answer:
9.77/2.83	  YES(O(1),O(n^1))
9.77/2.83	
9.77/2.83	The weightgap principle applies (using the following nonconstant
9.77/2.83	growth matrix-interpretation)
9.77/2.83	
9.77/2.83	The following argument positions are usable:
9.77/2.83	  Uargs(a__and) = {1}, Uargs(a__if) = {1}, Uargs(a__add) = {1},
9.77/2.83	  Uargs(a__first) = {1, 2}
9.77/2.83	
9.77/2.83	TcT has computed the following matrix interpretation satisfying
9.77/2.83	not(EDA) and not(IDA(1)).
9.77/2.83	
9.77/2.83	     [a__and](x1, x2) = [1] x1 + [4]         
9.77/2.83	                                             
9.77/2.83	               [true] = [0]                  
9.77/2.83	                                             
9.77/2.83	           [mark](x1) = [0]                  
9.77/2.83	                                             
9.77/2.83	              [false] = [0]                  
9.77/2.83	                                             
9.77/2.83	  [a__if](x1, x2, x3) = [1] x1 + [4]         
9.77/2.83	                                             
9.77/2.83	     [a__add](x1, x2) = [1] x1 + [0]         
9.77/2.83	                                             
9.77/2.83	                  [0] = [0]                  
9.77/2.83	                                             
9.77/2.83	              [s](x1) = [0]                  
9.77/2.83	                                             
9.77/2.83	        [add](x1, x2) = [1] x1 + [5]         
9.77/2.83	                                             
9.77/2.83	   [a__first](x1, x2) = [1] x1 + [1] x2 + [0]
9.77/2.83	                                             
9.77/2.83	                [nil] = [7]                  
9.77/2.83	                                             
9.77/2.83	       [cons](x1, x2) = [0]                  
9.77/2.83	                                             
9.77/2.83	      [first](x1, x2) = [1] x1 + [1] x2 + [5]
9.77/2.83	                                             
9.77/2.83	        [a__from](x1) = [5]                  
9.77/2.83	                                             
9.77/2.83	           [from](x1) = [5]                  
9.77/2.83	                                             
9.77/2.83	        [and](x1, x2) = [1] x1 + [3]         
9.77/2.83	                                             
9.77/2.83	     [if](x1, x2, x3) = [1] x1 + [3]         
9.77/2.83	
9.77/2.83	The order satisfies the following ordering constraints:
9.77/2.83	
9.77/2.83	              [a__and(X1, X2)] =  [1] X1 + [4]                  
9.77/2.83	                               >  [1] X1 + [3]                  
9.77/2.83	                               =  [and(X1, X2)]                 
9.77/2.83	                                                                
9.77/2.83	           [a__and(true(), X)] =  [4]                           
9.77/2.83	                               >  [0]                           
9.77/2.83	                               =  [mark(X)]                     
9.77/2.83	                                                                
9.77/2.83	          [a__and(false(), Y)] =  [4]                           
9.77/2.83	                               >  [0]                           
9.77/2.84	                               =  [false()]                     
9.77/2.84	                                                                
9.77/2.84	                [mark(true())] =  [0]                           
9.77/2.84	                               >= [0]                           
9.77/2.84	                               =  [true()]                      
9.77/2.84	                                                                
9.77/2.84	               [mark(false())] =  [0]                           
9.77/2.84	                               >= [0]                           
9.77/2.84	                               =  [false()]                     
9.77/2.84	                                                                
9.77/2.84	                   [mark(0())] =  [0]                           
9.77/2.84	                               >= [0]                           
9.77/2.84	                               =  [0()]                         
9.77/2.84	                                                                
9.77/2.84	                  [mark(s(X))] =  [0]                           
9.77/2.84	                               >= [0]                           
9.77/2.84	                               =  [s(X)]                        
9.77/2.84	                                                                
9.77/2.84	           [mark(add(X1, X2))] =  [0]                           
9.77/2.84	                               >= [0]                           
9.77/2.84	                               =  [a__add(mark(X1), X2)]        
9.77/2.84	                                                                
9.77/2.84	                 [mark(nil())] =  [0]                           
9.77/2.84	                               ?  [7]                           
9.77/2.84	                               =  [nil()]                       
9.77/2.84	                                                                
9.77/2.84	          [mark(cons(X1, X2))] =  [0]                           
9.77/2.84	                               >= [0]                           
9.77/2.84	                               =  [cons(X1, X2)]                
9.77/2.84	                                                                
9.77/2.84	         [mark(first(X1, X2))] =  [0]                           
9.77/2.84	                               >= [0]                           
9.77/2.84	                               =  [a__first(mark(X1), mark(X2))]
9.77/2.84	                                                                
9.77/2.84	               [mark(from(X))] =  [0]                           
9.77/2.84	                               ?  [5]                           
9.77/2.84	                               =  [a__from(X)]                  
9.77/2.84	                                                                
9.77/2.84	           [mark(and(X1, X2))] =  [0]                           
9.77/2.84	                               ?  [4]                           
9.77/2.84	                               =  [a__and(mark(X1), X2)]        
9.77/2.84	                                                                
9.77/2.84	        [mark(if(X1, X2, X3))] =  [0]                           
9.77/2.84	                               ?  [4]                           
9.77/2.84	                               =  [a__if(mark(X1), X2, X3)]     
9.77/2.84	                                                                
9.77/2.84	           [a__if(X1, X2, X3)] =  [1] X1 + [4]                  
9.77/2.84	                               >  [1] X1 + [3]                  
9.77/2.84	                               =  [if(X1, X2, X3)]              
9.77/2.84	                                                                
9.77/2.84	         [a__if(true(), X, Y)] =  [4]                           
9.77/2.84	                               >  [0]                           
9.77/2.84	                               =  [mark(X)]                     
9.77/2.84	                                                                
9.77/2.84	        [a__if(false(), X, Y)] =  [4]                           
9.77/2.84	                               >  [0]                           
9.77/2.84	                               =  [mark(Y)]                     
9.77/2.84	                                                                
9.77/2.84	              [a__add(X1, X2)] =  [1] X1 + [0]                  
9.77/2.84	                               ?  [1] X1 + [5]                  
9.77/2.84	                               =  [add(X1, X2)]                 
9.77/2.84	                                                                
9.77/2.84	              [a__add(0(), X)] =  [0]                           
9.77/2.84	                               >= [0]                           
9.77/2.84	                               =  [mark(X)]                     
9.77/2.84	                                                                
9.77/2.84	             [a__add(s(X), Y)] =  [0]                           
9.77/2.84	                               >= [0]                           
9.77/2.84	                               =  [s(add(X, Y))]                
9.77/2.84	                                                                
9.77/2.84	            [a__first(X1, X2)] =  [1] X1 + [1] X2 + [0]         
9.77/2.84	                               ?  [1] X1 + [1] X2 + [5]         
9.77/2.84	                               =  [first(X1, X2)]               
9.77/2.84	                                                                
9.77/2.84	            [a__first(0(), X)] =  [1] X + [0]                   
9.77/2.84	                               ?  [7]                           
9.77/2.84	                               =  [nil()]                       
9.77/2.84	                                                                
9.77/2.84	  [a__first(s(X), cons(Y, Z))] =  [0]                           
9.77/2.84	                               >= [0]                           
9.77/2.84	                               =  [cons(Y, first(X, Z))]        
9.77/2.84	                                                                
9.77/2.84	                  [a__from(X)] =  [5]                           
9.77/2.84	                               >  [0]                           
9.77/2.84	                               =  [cons(X, from(s(X)))]         
9.77/2.84	                                                                
9.77/2.84	                  [a__from(X)] =  [5]                           
9.77/2.84	                               >= [5]                           
9.77/2.84	                               =  [from(X)]                     
9.77/2.84	                                                                
9.77/2.84	
9.77/2.84	Further, it can be verified that all rules not oriented are covered by the weightgap condition.
9.77/2.84	
9.77/2.84	We are left with following problem, upon which TcT provides the
9.77/2.84	certificate YES(O(1),O(n^1)).
9.77/2.84	
9.77/2.84	Strict Trs:
9.77/2.84	  { mark(true()) -> true()
9.77/2.84	  , mark(false()) -> false()
9.77/2.84	  , mark(0()) -> 0()
9.77/2.84	  , mark(s(X)) -> s(X)
9.77/2.84	  , mark(add(X1, X2)) -> a__add(mark(X1), X2)
9.77/2.84	  , mark(nil()) -> nil()
9.77/2.84	  , mark(cons(X1, X2)) -> cons(X1, X2)
9.77/2.84	  , mark(first(X1, X2)) -> a__first(mark(X1), mark(X2))
9.77/2.84	  , mark(from(X)) -> a__from(X)
9.77/2.84	  , mark(and(X1, X2)) -> a__and(mark(X1), X2)
9.77/2.84	  , mark(if(X1, X2, X3)) -> a__if(mark(X1), X2, X3)
9.77/2.84	  , a__add(X1, X2) -> add(X1, X2)
9.77/2.84	  , a__add(0(), X) -> mark(X)
9.77/2.84	  , a__add(s(X), Y) -> s(add(X, Y))
9.77/2.84	  , a__first(X1, X2) -> first(X1, X2)
9.77/2.84	  , a__first(0(), X) -> nil()
9.77/2.84	  , a__first(s(X), cons(Y, Z)) -> cons(Y, first(X, Z))
9.77/2.84	  , a__from(X) -> from(X) }
9.77/2.84	Weak Trs:
9.77/2.84	  { a__and(X1, X2) -> and(X1, X2)
9.77/2.84	  , a__and(true(), X) -> mark(X)
9.77/2.84	  , a__and(false(), Y) -> false()
9.77/2.84	  , a__if(X1, X2, X3) -> if(X1, X2, X3)
9.77/2.84	  , a__if(true(), X, Y) -> mark(X)
9.77/2.84	  , a__if(false(), X, Y) -> mark(Y)
9.77/2.84	  , a__from(X) -> cons(X, from(s(X))) }
9.77/2.84	Obligation:
9.77/2.84	  innermost runtime complexity
9.77/2.84	Answer:
9.77/2.84	  YES(O(1),O(n^1))
9.77/2.84	
9.77/2.84	The weightgap principle applies (using the following nonconstant
9.77/2.84	growth matrix-interpretation)
9.77/2.84	
9.77/2.84	The following argument positions are usable:
9.77/2.84	  Uargs(a__and) = {1}, Uargs(a__if) = {1}, Uargs(a__add) = {1},
9.77/2.84	  Uargs(a__first) = {1, 2}
9.77/2.84	
9.77/2.84	TcT has computed the following matrix interpretation satisfying
9.77/2.84	not(EDA) and not(IDA(1)).
9.77/2.84	
9.77/2.84	     [a__and](x1, x2) = [1] x1 + [0]         
9.77/2.84	                                             
9.77/2.84	               [true] = [4]                  
9.77/2.84	                                             
9.77/2.84	           [mark](x1) = [0]                  
9.77/2.84	                                             
9.77/2.84	              [false] = [4]                  
9.77/2.84	                                             
9.77/2.84	  [a__if](x1, x2, x3) = [1] x1 + [0]         
9.77/2.84	                                             
9.77/2.84	     [a__add](x1, x2) = [1] x1 + [1]         
9.77/2.84	                                             
9.77/2.84	                  [0] = [0]                  
9.77/2.84	                                             
9.77/2.84	              [s](x1) = [0]                  
9.77/2.84	                                             
9.77/2.84	        [add](x1, x2) = [1] x1 + [5]         
9.77/2.84	                                             
9.77/2.84	   [a__first](x1, x2) = [1] x1 + [1] x2 + [0]
9.77/2.84	                                             
9.77/2.84	                [nil] = [7]                  
9.77/2.84	                                             
9.77/2.84	       [cons](x1, x2) = [0]                  
9.77/2.84	                                             
9.77/2.84	      [first](x1, x2) = [1] x1 + [1] x2 + [5]
9.77/2.84	                                             
9.77/2.84	        [a__from](x1) = [5]                  
9.77/2.84	                                             
9.77/2.84	           [from](x1) = [5]                  
9.77/2.84	                                             
9.77/2.84	        [and](x1, x2) = [1] x1 + [0]         
9.77/2.84	                                             
9.77/2.84	     [if](x1, x2, x3) = [1] x1 + [0]         
9.77/2.84	
9.77/2.84	The order satisfies the following ordering constraints:
9.77/2.84	
9.77/2.84	              [a__and(X1, X2)] =  [1] X1 + [0]                  
9.77/2.84	                               >= [1] X1 + [0]                  
9.77/2.84	                               =  [and(X1, X2)]                 
9.77/2.84	                                                                
9.77/2.84	           [a__and(true(), X)] =  [4]                           
9.77/2.84	                               >  [0]                           
9.77/2.84	                               =  [mark(X)]                     
9.77/2.84	                                                                
9.77/2.84	          [a__and(false(), Y)] =  [4]                           
9.77/2.84	                               >= [4]                           
9.77/2.84	                               =  [false()]                     
9.77/2.84	                                                                
9.77/2.84	                [mark(true())] =  [0]                           
9.77/2.84	                               ?  [4]                           
9.77/2.84	                               =  [true()]                      
9.77/2.84	                                                                
9.77/2.84	               [mark(false())] =  [0]                           
9.77/2.84	                               ?  [4]                           
9.77/2.84	                               =  [false()]                     
9.77/2.84	                                                                
9.77/2.84	                   [mark(0())] =  [0]                           
9.77/2.84	                               >= [0]                           
9.77/2.84	                               =  [0()]                         
9.77/2.84	                                                                
9.77/2.84	                  [mark(s(X))] =  [0]                           
9.77/2.84	                               >= [0]                           
9.77/2.84	                               =  [s(X)]                        
9.77/2.84	                                                                
9.77/2.84	           [mark(add(X1, X2))] =  [0]                           
9.77/2.84	                               ?  [1]                           
9.77/2.84	                               =  [a__add(mark(X1), X2)]        
9.77/2.84	                                                                
9.77/2.84	                 [mark(nil())] =  [0]                           
9.77/2.84	                               ?  [7]                           
9.77/2.84	                               =  [nil()]                       
9.77/2.84	                                                                
9.77/2.84	          [mark(cons(X1, X2))] =  [0]                           
9.77/2.84	                               >= [0]                           
9.77/2.84	                               =  [cons(X1, X2)]                
9.77/2.84	                                                                
9.77/2.84	         [mark(first(X1, X2))] =  [0]                           
9.77/2.84	                               >= [0]                           
9.77/2.84	                               =  [a__first(mark(X1), mark(X2))]
9.77/2.84	                                                                
9.77/2.84	               [mark(from(X))] =  [0]                           
9.77/2.84	                               ?  [5]                           
9.77/2.84	                               =  [a__from(X)]                  
9.77/2.84	                                                                
9.77/2.84	           [mark(and(X1, X2))] =  [0]                           
9.77/2.84	                               >= [0]                           
9.77/2.84	                               =  [a__and(mark(X1), X2)]        
9.77/2.84	                                                                
9.77/2.84	        [mark(if(X1, X2, X3))] =  [0]                           
9.77/2.84	                               >= [0]                           
9.77/2.84	                               =  [a__if(mark(X1), X2, X3)]     
9.77/2.84	                                                                
9.77/2.84	           [a__if(X1, X2, X3)] =  [1] X1 + [0]                  
9.77/2.84	                               >= [1] X1 + [0]                  
9.77/2.84	                               =  [if(X1, X2, X3)]              
9.77/2.84	                                                                
9.77/2.84	         [a__if(true(), X, Y)] =  [4]                           
9.77/2.84	                               >  [0]                           
9.77/2.84	                               =  [mark(X)]                     
9.77/2.84	                                                                
9.77/2.84	        [a__if(false(), X, Y)] =  [4]                           
9.77/2.84	                               >  [0]                           
9.77/2.84	                               =  [mark(Y)]                     
9.77/2.84	                                                                
9.77/2.84	              [a__add(X1, X2)] =  [1] X1 + [1]                  
9.77/2.84	                               ?  [1] X1 + [5]                  
9.77/2.84	                               =  [add(X1, X2)]                 
9.77/2.84	                                                                
9.77/2.84	              [a__add(0(), X)] =  [1]                           
9.77/2.84	                               >  [0]                           
9.77/2.84	                               =  [mark(X)]                     
9.77/2.84	                                                                
9.77/2.84	             [a__add(s(X), Y)] =  [1]                           
9.77/2.84	                               >  [0]                           
9.77/2.84	                               =  [s(add(X, Y))]                
9.77/2.84	                                                                
9.77/2.84	            [a__first(X1, X2)] =  [1] X1 + [1] X2 + [0]         
9.77/2.84	                               ?  [1] X1 + [1] X2 + [5]         
9.77/2.84	                               =  [first(X1, X2)]               
9.77/2.84	                                                                
9.77/2.84	            [a__first(0(), X)] =  [1] X + [0]                   
9.77/2.84	                               ?  [7]                           
9.77/2.84	                               =  [nil()]                       
9.77/2.84	                                                                
9.77/2.84	  [a__first(s(X), cons(Y, Z))] =  [0]                           
9.77/2.84	                               >= [0]                           
9.77/2.84	                               =  [cons(Y, first(X, Z))]        
9.77/2.84	                                                                
9.77/2.84	                  [a__from(X)] =  [5]                           
9.77/2.84	                               >  [0]                           
9.77/2.84	                               =  [cons(X, from(s(X)))]         
9.77/2.84	                                                                
9.77/2.84	                  [a__from(X)] =  [5]                           
9.77/2.84	                               >= [5]                           
9.77/2.84	                               =  [from(X)]                     
9.77/2.84	                                                                
9.77/2.84	
9.77/2.84	Further, it can be verified that all rules not oriented are covered by the weightgap condition.
9.77/2.84	
9.77/2.84	We are left with following problem, upon which TcT provides the
9.77/2.84	certificate YES(O(1),O(n^1)).
9.77/2.84	
9.77/2.84	Strict Trs:
9.77/2.84	  { mark(true()) -> true()
9.77/2.84	  , mark(false()) -> false()
9.77/2.84	  , mark(0()) -> 0()
9.77/2.84	  , mark(s(X)) -> s(X)
9.77/2.84	  , mark(add(X1, X2)) -> a__add(mark(X1), X2)
9.77/2.84	  , mark(nil()) -> nil()
9.77/2.84	  , mark(cons(X1, X2)) -> cons(X1, X2)
9.77/2.84	  , mark(first(X1, X2)) -> a__first(mark(X1), mark(X2))
9.77/2.84	  , mark(from(X)) -> a__from(X)
9.77/2.84	  , mark(and(X1, X2)) -> a__and(mark(X1), X2)
9.77/2.84	  , mark(if(X1, X2, X3)) -> a__if(mark(X1), X2, X3)
9.77/2.84	  , a__add(X1, X2) -> add(X1, X2)
9.77/2.84	  , a__first(X1, X2) -> first(X1, X2)
9.77/2.84	  , a__first(0(), X) -> nil()
9.77/2.84	  , a__first(s(X), cons(Y, Z)) -> cons(Y, first(X, Z))
9.77/2.84	  , a__from(X) -> from(X) }
9.77/2.84	Weak Trs:
9.77/2.84	  { a__and(X1, X2) -> and(X1, X2)
9.77/2.84	  , a__and(true(), X) -> mark(X)
9.77/2.84	  , a__and(false(), Y) -> false()
9.77/2.84	  , a__if(X1, X2, X3) -> if(X1, X2, X3)
9.77/2.84	  , a__if(true(), X, Y) -> mark(X)
9.77/2.84	  , a__if(false(), X, Y) -> mark(Y)
9.77/2.84	  , a__add(0(), X) -> mark(X)
9.77/2.84	  , a__add(s(X), Y) -> s(add(X, Y))
9.77/2.84	  , a__from(X) -> cons(X, from(s(X))) }
9.77/2.84	Obligation:
9.77/2.84	  innermost runtime complexity
9.77/2.84	Answer:
9.77/2.84	  YES(O(1),O(n^1))
9.77/2.84	
9.77/2.84	The weightgap principle applies (using the following nonconstant
9.77/2.84	growth matrix-interpretation)
9.77/2.84	
9.77/2.84	The following argument positions are usable:
9.77/2.84	  Uargs(a__and) = {1}, Uargs(a__if) = {1}, Uargs(a__add) = {1},
9.77/2.84	  Uargs(a__first) = {1, 2}
9.77/2.84	
9.77/2.84	TcT has computed the following matrix interpretation satisfying
9.77/2.84	not(EDA) and not(IDA(1)).
9.77/2.84	
9.77/2.84	     [a__and](x1, x2) = [1] x1 + [4]         
9.77/2.84	                                             
9.77/2.84	               [true] = [4]                  
9.77/2.84	                                             
9.77/2.84	           [mark](x1) = [0]                  
9.77/2.84	                                             
9.77/2.84	              [false] = [4]                  
9.77/2.84	                                             
9.77/2.84	  [a__if](x1, x2, x3) = [1] x1 + [0]         
9.77/2.84	                                             
9.77/2.84	     [a__add](x1, x2) = [1] x1 + [4]         
9.77/2.84	                                             
9.77/2.84	                  [0] = [0]                  
9.77/2.84	                                             
9.77/2.84	              [s](x1) = [0]                  
9.77/2.84	                                             
9.77/2.84	        [add](x1, x2) = [1] x1 + [1]         
9.77/2.84	                                             
9.77/2.84	   [a__first](x1, x2) = [1] x1 + [1] x2 + [0]
9.77/2.84	                                             
9.77/2.84	                [nil] = [7]                  
9.77/2.84	                                             
9.77/2.84	       [cons](x1, x2) = [0]                  
9.77/2.84	                                             
9.77/2.84	      [first](x1, x2) = [1] x1 + [1] x2 + [5]
9.77/2.84	                                             
9.77/2.84	        [a__from](x1) = [5]                  
9.77/2.84	                                             
9.77/2.84	           [from](x1) = [5]                  
9.77/2.84	                                             
9.77/2.84	        [and](x1, x2) = [1] x1 + [3]         
9.77/2.84	                                             
9.77/2.84	     [if](x1, x2, x3) = [1] x1 + [0]         
9.77/2.84	
9.77/2.84	The order satisfies the following ordering constraints:
9.77/2.84	
9.77/2.84	              [a__and(X1, X2)] =  [1] X1 + [4]                  
9.77/2.84	                               >  [1] X1 + [3]                  
9.77/2.84	                               =  [and(X1, X2)]                 
9.77/2.84	                                                                
9.77/2.84	           [a__and(true(), X)] =  [8]                           
9.77/2.84	                               >  [0]                           
9.77/2.84	                               =  [mark(X)]                     
9.77/2.84	                                                                
9.77/2.84	          [a__and(false(), Y)] =  [8]                           
9.77/2.84	                               >  [4]                           
9.77/2.84	                               =  [false()]                     
9.77/2.84	                                                                
9.77/2.84	                [mark(true())] =  [0]                           
9.77/2.84	                               ?  [4]                           
9.77/2.84	                               =  [true()]                      
9.77/2.84	                                                                
9.77/2.84	               [mark(false())] =  [0]                           
9.77/2.84	                               ?  [4]                           
9.77/2.84	                               =  [false()]                     
9.77/2.84	                                                                
9.77/2.84	                   [mark(0())] =  [0]                           
9.77/2.84	                               >= [0]                           
9.77/2.84	                               =  [0()]                         
9.77/2.84	                                                                
9.77/2.84	                  [mark(s(X))] =  [0]                           
9.77/2.84	                               >= [0]                           
9.77/2.84	                               =  [s(X)]                        
9.77/2.84	                                                                
9.77/2.84	           [mark(add(X1, X2))] =  [0]                           
9.77/2.84	                               ?  [4]                           
9.77/2.84	                               =  [a__add(mark(X1), X2)]        
9.77/2.84	                                                                
9.77/2.84	                 [mark(nil())] =  [0]                           
9.77/2.84	                               ?  [7]                           
9.77/2.84	                               =  [nil()]                       
9.77/2.84	                                                                
9.77/2.84	          [mark(cons(X1, X2))] =  [0]                           
9.77/2.84	                               >= [0]                           
9.77/2.84	                               =  [cons(X1, X2)]                
9.77/2.84	                                                                
9.77/2.84	         [mark(first(X1, X2))] =  [0]                           
9.77/2.84	                               >= [0]                           
9.77/2.84	                               =  [a__first(mark(X1), mark(X2))]
9.77/2.84	                                                                
9.77/2.84	               [mark(from(X))] =  [0]                           
9.77/2.84	                               ?  [5]                           
9.77/2.84	                               =  [a__from(X)]                  
9.77/2.84	                                                                
9.77/2.84	           [mark(and(X1, X2))] =  [0]                           
9.77/2.84	                               ?  [4]                           
9.77/2.84	                               =  [a__and(mark(X1), X2)]        
9.77/2.84	                                                                
9.77/2.84	        [mark(if(X1, X2, X3))] =  [0]                           
9.77/2.84	                               >= [0]                           
9.77/2.84	                               =  [a__if(mark(X1), X2, X3)]     
9.77/2.84	                                                                
9.77/2.84	           [a__if(X1, X2, X3)] =  [1] X1 + [0]                  
9.77/2.84	                               >= [1] X1 + [0]                  
9.77/2.84	                               =  [if(X1, X2, X3)]              
9.77/2.84	                                                                
9.77/2.84	         [a__if(true(), X, Y)] =  [4]                           
9.77/2.84	                               >  [0]                           
9.77/2.84	                               =  [mark(X)]                     
9.77/2.84	                                                                
9.77/2.84	        [a__if(false(), X, Y)] =  [4]                           
9.77/2.84	                               >  [0]                           
9.77/2.84	                               =  [mark(Y)]                     
9.77/2.84	                                                                
9.77/2.84	              [a__add(X1, X2)] =  [1] X1 + [4]                  
9.77/2.84	                               >  [1] X1 + [1]                  
9.77/2.84	                               =  [add(X1, X2)]                 
9.77/2.84	                                                                
9.77/2.84	              [a__add(0(), X)] =  [4]                           
9.77/2.84	                               >  [0]                           
9.77/2.84	                               =  [mark(X)]                     
9.77/2.84	                                                                
9.77/2.84	             [a__add(s(X), Y)] =  [4]                           
9.77/2.84	                               >  [0]                           
9.77/2.84	                               =  [s(add(X, Y))]                
9.77/2.84	                                                                
9.77/2.84	            [a__first(X1, X2)] =  [1] X1 + [1] X2 + [0]         
9.77/2.84	                               ?  [1] X1 + [1] X2 + [5]         
9.77/2.84	                               =  [first(X1, X2)]               
9.77/2.84	                                                                
9.77/2.84	            [a__first(0(), X)] =  [1] X + [0]                   
9.77/2.84	                               ?  [7]                           
9.77/2.84	                               =  [nil()]                       
9.77/2.84	                                                                
9.77/2.84	  [a__first(s(X), cons(Y, Z))] =  [0]                           
9.77/2.84	                               >= [0]                           
9.77/2.84	                               =  [cons(Y, first(X, Z))]        
9.77/2.84	                                                                
9.77/2.84	                  [a__from(X)] =  [5]                           
9.77/2.84	                               >  [0]                           
9.77/2.84	                               =  [cons(X, from(s(X)))]         
9.77/2.84	                                                                
9.77/2.84	                  [a__from(X)] =  [5]                           
9.77/2.84	                               >= [5]                           
9.77/2.84	                               =  [from(X)]                     
9.77/2.84	                                                                
9.77/2.84	
9.77/2.84	Further, it can be verified that all rules not oriented are covered by the weightgap condition.
9.77/2.84	
9.77/2.84	We are left with following problem, upon which TcT provides the
9.77/2.84	certificate YES(O(1),O(n^1)).
9.77/2.84	
9.77/2.84	Strict Trs:
9.77/2.84	  { mark(true()) -> true()
9.77/2.84	  , mark(false()) -> false()
9.77/2.84	  , mark(0()) -> 0()
9.77/2.84	  , mark(s(X)) -> s(X)
9.77/2.84	  , mark(add(X1, X2)) -> a__add(mark(X1), X2)
9.77/2.84	  , mark(nil()) -> nil()
9.77/2.84	  , mark(cons(X1, X2)) -> cons(X1, X2)
9.77/2.84	  , mark(first(X1, X2)) -> a__first(mark(X1), mark(X2))
9.77/2.84	  , mark(from(X)) -> a__from(X)
9.77/2.84	  , mark(and(X1, X2)) -> a__and(mark(X1), X2)
9.77/2.84	  , mark(if(X1, X2, X3)) -> a__if(mark(X1), X2, X3)
9.77/2.84	  , a__first(X1, X2) -> first(X1, X2)
9.77/2.84	  , a__first(0(), X) -> nil()
9.77/2.84	  , a__first(s(X), cons(Y, Z)) -> cons(Y, first(X, Z))
9.77/2.84	  , a__from(X) -> from(X) }
9.77/2.84	Weak Trs:
9.77/2.84	  { a__and(X1, X2) -> and(X1, X2)
9.77/2.84	  , a__and(true(), X) -> mark(X)
9.77/2.84	  , a__and(false(), Y) -> false()
9.77/2.84	  , a__if(X1, X2, X3) -> if(X1, X2, X3)
9.77/2.84	  , a__if(true(), X, Y) -> mark(X)
9.77/2.84	  , a__if(false(), X, Y) -> mark(Y)
9.77/2.84	  , a__add(X1, X2) -> add(X1, X2)
9.77/2.84	  , a__add(0(), X) -> mark(X)
9.77/2.84	  , a__add(s(X), Y) -> s(add(X, Y))
9.77/2.84	  , a__from(X) -> cons(X, from(s(X))) }
9.77/2.84	Obligation:
9.77/2.84	  innermost runtime complexity
9.77/2.84	Answer:
9.77/2.84	  YES(O(1),O(n^1))
9.77/2.84	
9.77/2.84	The weightgap principle applies (using the following nonconstant
9.77/2.84	growth matrix-interpretation)
9.77/2.84	
9.77/2.84	The following argument positions are usable:
9.77/2.84	  Uargs(a__and) = {1}, Uargs(a__if) = {1}, Uargs(a__add) = {1},
9.77/2.84	  Uargs(a__first) = {1, 2}
9.77/2.84	
9.77/2.84	TcT has computed the following matrix interpretation satisfying
9.77/2.84	not(EDA) and not(IDA(1)).
9.77/2.84	
9.77/2.84	     [a__and](x1, x2) = [1] x1 + [4]         
9.77/2.84	                                             
9.77/2.84	               [true] = [4]                  
9.77/2.84	                                             
9.77/2.84	           [mark](x1) = [0]                  
9.77/2.84	                                             
9.77/2.84	              [false] = [4]                  
9.77/2.84	                                             
9.77/2.84	  [a__if](x1, x2, x3) = [1] x1 + [0]         
9.77/2.84	                                             
9.77/2.84	     [a__add](x1, x2) = [1] x1 + [4]         
9.77/2.84	                                             
9.77/2.84	                  [0] = [0]                  
9.77/2.84	                                             
9.77/2.84	              [s](x1) = [0]                  
9.77/2.84	                                             
9.77/2.84	        [add](x1, x2) = [1] x1 + [2]         
9.77/2.84	                                             
9.77/2.84	   [a__first](x1, x2) = [1] x1 + [1] x2 + [0]
9.77/2.84	                                             
9.77/2.84	                [nil] = [7]                  
9.77/2.84	                                             
9.77/2.84	       [cons](x1, x2) = [0]                  
9.77/2.84	                                             
9.77/2.84	      [first](x1, x2) = [1] x1 + [1] x2 + [5]
9.77/2.84	                                             
9.77/2.84	        [a__from](x1) = [5]                  
9.77/2.84	                                             
9.77/2.84	           [from](x1) = [1]                  
9.77/2.84	                                             
9.77/2.84	        [and](x1, x2) = [1] x1 + [3]         
9.77/2.84	                                             
9.77/2.84	     [if](x1, x2, x3) = [1] x1 + [0]         
9.77/2.84	
9.77/2.84	The order satisfies the following ordering constraints:
9.77/2.84	
9.77/2.84	              [a__and(X1, X2)] =  [1] X1 + [4]                  
9.77/2.84	                               >  [1] X1 + [3]                  
9.77/2.84	                               =  [and(X1, X2)]                 
9.77/2.84	                                                                
9.77/2.84	           [a__and(true(), X)] =  [8]                           
9.77/2.84	                               >  [0]                           
9.77/2.84	                               =  [mark(X)]                     
9.77/2.84	                                                                
9.77/2.84	          [a__and(false(), Y)] =  [8]                           
9.77/2.84	                               >  [4]                           
9.77/2.84	                               =  [false()]                     
9.77/2.84	                                                                
9.77/2.84	                [mark(true())] =  [0]                           
9.77/2.84	                               ?  [4]                           
9.77/2.84	                               =  [true()]                      
9.77/2.84	                                                                
9.77/2.84	               [mark(false())] =  [0]                           
9.77/2.84	                               ?  [4]                           
9.77/2.84	                               =  [false()]                     
9.77/2.84	                                                                
9.77/2.84	                   [mark(0())] =  [0]                           
9.77/2.84	                               >= [0]                           
9.77/2.84	                               =  [0()]                         
9.77/2.84	                                                                
9.77/2.84	                  [mark(s(X))] =  [0]                           
9.77/2.84	                               >= [0]                           
9.77/2.84	                               =  [s(X)]                        
9.77/2.84	                                                                
9.77/2.84	           [mark(add(X1, X2))] =  [0]                           
9.77/2.84	                               ?  [4]                           
9.77/2.84	                               =  [a__add(mark(X1), X2)]        
9.77/2.84	                                                                
9.77/2.84	                 [mark(nil())] =  [0]                           
9.77/2.84	                               ?  [7]                           
9.77/2.84	                               =  [nil()]                       
9.77/2.84	                                                                
9.77/2.84	          [mark(cons(X1, X2))] =  [0]                           
9.77/2.84	                               >= [0]                           
9.77/2.84	                               =  [cons(X1, X2)]                
9.77/2.84	                                                                
9.77/2.84	         [mark(first(X1, X2))] =  [0]                           
9.77/2.84	                               >= [0]                           
9.77/2.84	                               =  [a__first(mark(X1), mark(X2))]
9.77/2.84	                                                                
9.77/2.84	               [mark(from(X))] =  [0]                           
9.77/2.84	                               ?  [5]                           
9.77/2.84	                               =  [a__from(X)]                  
9.77/2.84	                                                                
9.77/2.84	           [mark(and(X1, X2))] =  [0]                           
9.77/2.84	                               ?  [4]                           
9.77/2.84	                               =  [a__and(mark(X1), X2)]        
9.77/2.84	                                                                
9.77/2.84	        [mark(if(X1, X2, X3))] =  [0]                           
9.77/2.84	                               >= [0]                           
9.77/2.84	                               =  [a__if(mark(X1), X2, X3)]     
9.77/2.84	                                                                
9.77/2.84	           [a__if(X1, X2, X3)] =  [1] X1 + [0]                  
9.77/2.84	                               >= [1] X1 + [0]                  
9.77/2.84	                               =  [if(X1, X2, X3)]              
9.77/2.84	                                                                
9.77/2.84	         [a__if(true(), X, Y)] =  [4]                           
9.77/2.84	                               >  [0]                           
9.77/2.84	                               =  [mark(X)]                     
9.77/2.84	                                                                
9.77/2.84	        [a__if(false(), X, Y)] =  [4]                           
9.77/2.84	                               >  [0]                           
9.77/2.84	                               =  [mark(Y)]                     
9.77/2.84	                                                                
9.77/2.84	              [a__add(X1, X2)] =  [1] X1 + [4]                  
9.77/2.84	                               >  [1] X1 + [2]                  
9.77/2.84	                               =  [add(X1, X2)]                 
9.77/2.84	                                                                
9.77/2.84	              [a__add(0(), X)] =  [4]                           
9.77/2.84	                               >  [0]                           
9.77/2.84	                               =  [mark(X)]                     
9.77/2.84	                                                                
9.77/2.84	             [a__add(s(X), Y)] =  [4]                           
9.77/2.84	                               >  [0]                           
9.77/2.84	                               =  [s(add(X, Y))]                
9.77/2.84	                                                                
9.77/2.84	            [a__first(X1, X2)] =  [1] X1 + [1] X2 + [0]         
9.77/2.84	                               ?  [1] X1 + [1] X2 + [5]         
9.77/2.84	                               =  [first(X1, X2)]               
9.77/2.84	                                                                
9.77/2.84	            [a__first(0(), X)] =  [1] X + [0]                   
9.77/2.84	                               ?  [7]                           
9.77/2.84	                               =  [nil()]                       
9.77/2.84	                                                                
9.77/2.84	  [a__first(s(X), cons(Y, Z))] =  [0]                           
9.77/2.84	                               >= [0]                           
9.77/2.84	                               =  [cons(Y, first(X, Z))]        
9.77/2.84	                                                                
9.77/2.84	                  [a__from(X)] =  [5]                           
9.77/2.84	                               >  [0]                           
9.77/2.84	                               =  [cons(X, from(s(X)))]         
9.77/2.84	                                                                
9.77/2.84	                  [a__from(X)] =  [5]                           
9.77/2.84	                               >  [1]                           
9.77/2.84	                               =  [from(X)]                     
9.77/2.84	                                                                
9.77/2.84	
9.77/2.84	Further, it can be verified that all rules not oriented are covered by the weightgap condition.
9.77/2.84	
9.77/2.84	We are left with following problem, upon which TcT provides the
9.77/2.84	certificate YES(O(1),O(n^1)).
9.77/2.84	
9.77/2.84	Strict Trs:
9.77/2.84	  { mark(true()) -> true()
9.77/2.84	  , mark(false()) -> false()
9.77/2.84	  , mark(0()) -> 0()
9.77/2.84	  , mark(s(X)) -> s(X)
9.77/2.84	  , mark(add(X1, X2)) -> a__add(mark(X1), X2)
9.77/2.84	  , mark(nil()) -> nil()
9.77/2.84	  , mark(cons(X1, X2)) -> cons(X1, X2)
9.77/2.84	  , mark(first(X1, X2)) -> a__first(mark(X1), mark(X2))
9.77/2.84	  , mark(from(X)) -> a__from(X)
9.77/2.84	  , mark(and(X1, X2)) -> a__and(mark(X1), X2)
9.77/2.84	  , mark(if(X1, X2, X3)) -> a__if(mark(X1), X2, X3)
9.77/2.84	  , a__first(X1, X2) -> first(X1, X2)
9.77/2.84	  , a__first(0(), X) -> nil()
9.77/2.84	  , a__first(s(X), cons(Y, Z)) -> cons(Y, first(X, Z)) }
9.77/2.84	Weak Trs:
9.77/2.84	  { a__and(X1, X2) -> and(X1, X2)
9.77/2.84	  , a__and(true(), X) -> mark(X)
9.77/2.84	  , a__and(false(), Y) -> false()
9.77/2.84	  , a__if(X1, X2, X3) -> if(X1, X2, X3)
9.77/2.84	  , a__if(true(), X, Y) -> mark(X)
9.77/2.84	  , a__if(false(), X, Y) -> mark(Y)
9.77/2.84	  , a__add(X1, X2) -> add(X1, X2)
9.77/2.84	  , a__add(0(), X) -> mark(X)
9.77/2.84	  , a__add(s(X), Y) -> s(add(X, Y))
9.77/2.84	  , a__from(X) -> cons(X, from(s(X)))
9.77/2.84	  , a__from(X) -> from(X) }
9.77/2.84	Obligation:
9.77/2.84	  innermost runtime complexity
9.77/2.84	Answer:
9.77/2.84	  YES(O(1),O(n^1))
9.77/2.84	
9.77/2.84	The weightgap principle applies (using the following nonconstant
9.77/2.84	growth matrix-interpretation)
9.77/2.84	
9.77/2.84	The following argument positions are usable:
9.77/2.84	  Uargs(a__and) = {1}, Uargs(a__if) = {1}, Uargs(a__add) = {1},
9.77/2.84	  Uargs(a__first) = {1, 2}
9.77/2.84	
9.77/2.84	TcT has computed the following matrix interpretation satisfying
9.77/2.84	not(EDA) and not(IDA(1)).
9.77/2.84	
9.77/2.84	     [a__and](x1, x2) = [1] x1 + [0]         
9.77/2.84	                                             
9.77/2.84	               [true] = [4]                  
9.77/2.84	                                             
9.77/2.84	           [mark](x1) = [0]                  
9.77/2.84	                                             
9.77/2.84	              [false] = [4]                  
9.77/2.84	                                             
9.77/2.84	  [a__if](x1, x2, x3) = [1] x1 + [0]         
9.77/2.84	                                             
9.77/2.84	     [a__add](x1, x2) = [1] x1 + [4]         
9.77/2.84	                                             
9.77/2.84	                  [0] = [0]                  
9.77/2.84	                                             
9.77/2.84	              [s](x1) = [0]                  
9.77/2.84	                                             
9.77/2.84	        [add](x1, x2) = [1] x1 + [1]         
9.77/2.84	                                             
9.77/2.84	   [a__first](x1, x2) = [1] x1 + [1] x2 + [1]
9.77/2.84	                                             
9.77/2.84	                [nil] = [6]                  
9.77/2.84	                                             
9.77/2.84	       [cons](x1, x2) = [0]                  
9.77/2.84	                                             
9.77/2.84	      [first](x1, x2) = [1] x1 + [1] x2 + [5]
9.77/2.84	                                             
9.77/2.84	        [a__from](x1) = [5]                  
9.77/2.84	                                             
9.77/2.84	           [from](x1) = [2]                  
9.77/2.84	                                             
9.77/2.84	        [and](x1, x2) = [1] x1 + [0]         
9.77/2.84	                                             
9.77/2.84	     [if](x1, x2, x3) = [1] x1 + [0]         
9.77/2.84	
9.77/2.84	The order satisfies the following ordering constraints:
9.77/2.84	
9.77/2.84	              [a__and(X1, X2)] =  [1] X1 + [0]                  
9.77/2.84	                               >= [1] X1 + [0]                  
9.77/2.84	                               =  [and(X1, X2)]                 
9.77/2.84	                                                                
9.77/2.84	           [a__and(true(), X)] =  [4]                           
9.77/2.84	                               >  [0]                           
9.77/2.84	                               =  [mark(X)]                     
9.77/2.84	                                                                
9.77/2.84	          [a__and(false(), Y)] =  [4]                           
9.77/2.84	                               >= [4]                           
9.77/2.84	                               =  [false()]                     
9.77/2.84	                                                                
9.77/2.84	                [mark(true())] =  [0]                           
9.77/2.84	                               ?  [4]                           
9.77/2.84	                               =  [true()]                      
9.77/2.84	                                                                
9.77/2.84	               [mark(false())] =  [0]                           
9.77/2.84	                               ?  [4]                           
9.77/2.84	                               =  [false()]                     
9.77/2.84	                                                                
9.77/2.84	                   [mark(0())] =  [0]                           
9.77/2.84	                               >= [0]                           
9.77/2.84	                               =  [0()]                         
9.77/2.84	                                                                
9.77/2.84	                  [mark(s(X))] =  [0]                           
9.77/2.84	                               >= [0]                           
9.77/2.84	                               =  [s(X)]                        
9.77/2.84	                                                                
9.77/2.84	           [mark(add(X1, X2))] =  [0]                           
9.77/2.84	                               ?  [4]                           
9.77/2.84	                               =  [a__add(mark(X1), X2)]        
9.77/2.84	                                                                
9.77/2.84	                 [mark(nil())] =  [0]                           
9.77/2.84	                               ?  [6]                           
9.77/2.84	                               =  [nil()]                       
9.77/2.84	                                                                
9.77/2.84	          [mark(cons(X1, X2))] =  [0]                           
9.77/2.84	                               >= [0]                           
9.77/2.84	                               =  [cons(X1, X2)]                
9.77/2.84	                                                                
9.77/2.84	         [mark(first(X1, X2))] =  [0]                           
9.77/2.84	                               ?  [1]                           
9.77/2.84	                               =  [a__first(mark(X1), mark(X2))]
9.77/2.84	                                                                
9.77/2.84	               [mark(from(X))] =  [0]                           
9.77/2.84	                               ?  [5]                           
9.77/2.84	                               =  [a__from(X)]                  
9.77/2.84	                                                                
9.77/2.84	           [mark(and(X1, X2))] =  [0]                           
9.77/2.84	                               >= [0]                           
9.77/2.84	                               =  [a__and(mark(X1), X2)]        
9.77/2.84	                                                                
9.77/2.84	        [mark(if(X1, X2, X3))] =  [0]                           
9.77/2.84	                               >= [0]                           
9.77/2.84	                               =  [a__if(mark(X1), X2, X3)]     
9.77/2.84	                                                                
9.77/2.84	           [a__if(X1, X2, X3)] =  [1] X1 + [0]                  
9.77/2.84	                               >= [1] X1 + [0]                  
9.77/2.84	                               =  [if(X1, X2, X3)]              
9.77/2.84	                                                                
9.77/2.84	         [a__if(true(), X, Y)] =  [4]                           
9.77/2.84	                               >  [0]                           
9.77/2.84	                               =  [mark(X)]                     
9.77/2.84	                                                                
9.77/2.84	        [a__if(false(), X, Y)] =  [4]                           
9.77/2.84	                               >  [0]                           
9.77/2.84	                               =  [mark(Y)]                     
9.77/2.84	                                                                
9.77/2.84	              [a__add(X1, X2)] =  [1] X1 + [4]                  
9.77/2.84	                               >  [1] X1 + [1]                  
9.77/2.84	                               =  [add(X1, X2)]                 
9.77/2.84	                                                                
9.77/2.84	              [a__add(0(), X)] =  [4]                           
9.77/2.84	                               >  [0]                           
9.77/2.84	                               =  [mark(X)]                     
9.77/2.84	                                                                
9.77/2.84	             [a__add(s(X), Y)] =  [4]                           
9.77/2.84	                               >  [0]                           
9.77/2.84	                               =  [s(add(X, Y))]                
9.77/2.84	                                                                
9.77/2.84	            [a__first(X1, X2)] =  [1] X1 + [1] X2 + [1]         
9.77/2.84	                               ?  [1] X1 + [1] X2 + [5]         
9.77/2.84	                               =  [first(X1, X2)]               
9.77/2.84	                                                                
9.77/2.84	            [a__first(0(), X)] =  [1] X + [1]                   
9.77/2.84	                               ?  [6]                           
9.77/2.84	                               =  [nil()]                       
9.77/2.84	                                                                
9.77/2.84	  [a__first(s(X), cons(Y, Z))] =  [1]                           
9.77/2.84	                               >  [0]                           
9.77/2.84	                               =  [cons(Y, first(X, Z))]        
9.77/2.84	                                                                
9.77/2.84	                  [a__from(X)] =  [5]                           
9.77/2.84	                               >  [0]                           
9.77/2.84	                               =  [cons(X, from(s(X)))]         
9.77/2.84	                                                                
9.77/2.84	                  [a__from(X)] =  [5]                           
9.77/2.84	                               >  [2]                           
9.77/2.84	                               =  [from(X)]                     
9.77/2.84	                                                                
9.77/2.84	
9.77/2.84	Further, it can be verified that all rules not oriented are covered by the weightgap condition.
9.77/2.84	
9.77/2.84	We are left with following problem, upon which TcT provides the
9.77/2.84	certificate YES(O(1),O(n^1)).
9.77/2.84	
9.77/2.84	Strict Trs:
9.77/2.84	  { mark(true()) -> true()
9.77/2.84	  , mark(false()) -> false()
9.77/2.84	  , mark(0()) -> 0()
9.77/2.84	  , mark(s(X)) -> s(X)
9.77/2.84	  , mark(add(X1, X2)) -> a__add(mark(X1), X2)
9.77/2.84	  , mark(nil()) -> nil()
9.77/2.84	  , mark(cons(X1, X2)) -> cons(X1, X2)
9.77/2.84	  , mark(first(X1, X2)) -> a__first(mark(X1), mark(X2))
9.77/2.84	  , mark(from(X)) -> a__from(X)
9.77/2.84	  , mark(and(X1, X2)) -> a__and(mark(X1), X2)
9.77/2.84	  , mark(if(X1, X2, X3)) -> a__if(mark(X1), X2, X3)
9.77/2.84	  , a__first(X1, X2) -> first(X1, X2)
9.77/2.84	  , a__first(0(), X) -> nil() }
9.77/2.84	Weak Trs:
9.77/2.84	  { a__and(X1, X2) -> and(X1, X2)
9.77/2.84	  , a__and(true(), X) -> mark(X)
9.77/2.84	  , a__and(false(), Y) -> false()
9.77/2.84	  , a__if(X1, X2, X3) -> if(X1, X2, X3)
9.77/2.84	  , a__if(true(), X, Y) -> mark(X)
9.77/2.84	  , a__if(false(), X, Y) -> mark(Y)
9.77/2.84	  , a__add(X1, X2) -> add(X1, X2)
9.77/2.84	  , a__add(0(), X) -> mark(X)
9.77/2.84	  , a__add(s(X), Y) -> s(add(X, Y))
9.77/2.84	  , a__first(s(X), cons(Y, Z)) -> cons(Y, first(X, Z))
9.77/2.84	  , a__from(X) -> cons(X, from(s(X)))
9.77/2.84	  , a__from(X) -> from(X) }
9.77/2.84	Obligation:
9.77/2.84	  innermost runtime complexity
9.77/2.84	Answer:
9.77/2.84	  YES(O(1),O(n^1))
9.77/2.84	
9.77/2.84	The weightgap principle applies (using the following nonconstant
9.77/2.84	growth matrix-interpretation)
9.77/2.84	
9.77/2.84	The following argument positions are usable:
9.77/2.84	  Uargs(a__and) = {1}, Uargs(a__if) = {1}, Uargs(a__add) = {1},
9.77/2.84	  Uargs(a__first) = {1, 2}
9.77/2.84	
9.77/2.84	TcT has computed the following matrix interpretation satisfying
9.77/2.84	not(EDA) and not(IDA(1)).
9.77/2.84	
9.77/2.84	     [a__and](x1, x2) = [1] x1 + [0]         
9.77/2.84	                                             
9.77/2.84	               [true] = [0]                  
9.77/2.84	                                             
9.77/2.84	           [mark](x1) = [0]                  
9.77/2.84	                                             
9.77/2.84	              [false] = [0]                  
9.77/2.84	                                             
9.77/2.84	  [a__if](x1, x2, x3) = [1] x1 + [4]         
9.77/2.84	                                             
9.77/2.84	     [a__add](x1, x2) = [1] x1 + [4]         
9.77/2.84	                                             
9.77/2.84	                  [0] = [0]                  
9.77/2.84	                                             
9.77/2.84	              [s](x1) = [0]                  
9.77/2.84	                                             
9.77/2.84	        [add](x1, x2) = [1] x1 + [2]         
9.77/2.84	                                             
9.77/2.84	   [a__first](x1, x2) = [1] x1 + [1] x2 + [1]
9.77/2.84	                                             
9.77/2.84	                [nil] = [0]                  
9.77/2.84	                                             
9.77/2.84	       [cons](x1, x2) = [0]                  
9.77/2.84	                                             
9.77/2.84	      [first](x1, x2) = [1] x1 + [1] x2 + [5]
9.77/2.84	                                             
9.77/2.84	        [a__from](x1) = [4]                  
9.77/2.84	                                             
9.77/2.84	           [from](x1) = [2]                  
9.77/2.84	                                             
9.77/2.84	        [and](x1, x2) = [1] x1 + [0]         
9.77/2.84	                                             
9.77/2.84	     [if](x1, x2, x3) = [1] x1 + [3]         
9.77/2.84	
9.77/2.84	The order satisfies the following ordering constraints:
9.77/2.84	
9.77/2.84	              [a__and(X1, X2)] =  [1] X1 + [0]                  
9.77/2.84	                               >= [1] X1 + [0]                  
9.77/2.84	                               =  [and(X1, X2)]                 
9.77/2.84	                                                                
9.77/2.84	           [a__and(true(), X)] =  [0]                           
9.77/2.84	                               >= [0]                           
9.77/2.84	                               =  [mark(X)]                     
9.77/2.84	                                                                
9.77/2.84	          [a__and(false(), Y)] =  [0]                           
9.77/2.84	                               >= [0]                           
9.77/2.84	                               =  [false()]                     
9.77/2.84	                                                                
9.77/2.84	                [mark(true())] =  [0]                           
9.77/2.84	                               >= [0]                           
9.77/2.84	                               =  [true()]                      
9.77/2.84	                                                                
9.77/2.84	               [mark(false())] =  [0]                           
9.77/2.84	                               >= [0]                           
9.77/2.84	                               =  [false()]                     
9.77/2.84	                                                                
9.77/2.84	                   [mark(0())] =  [0]                           
9.77/2.84	                               >= [0]                           
9.77/2.84	                               =  [0()]                         
9.77/2.84	                                                                
9.77/2.84	                  [mark(s(X))] =  [0]                           
9.77/2.84	                               >= [0]                           
9.77/2.84	                               =  [s(X)]                        
9.77/2.84	                                                                
9.77/2.84	           [mark(add(X1, X2))] =  [0]                           
9.77/2.84	                               ?  [4]                           
9.77/2.84	                               =  [a__add(mark(X1), X2)]        
9.77/2.84	                                                                
9.77/2.84	                 [mark(nil())] =  [0]                           
9.77/2.84	                               >= [0]                           
9.77/2.84	                               =  [nil()]                       
9.77/2.84	                                                                
9.77/2.84	          [mark(cons(X1, X2))] =  [0]                           
9.77/2.84	                               >= [0]                           
9.77/2.84	                               =  [cons(X1, X2)]                
9.77/2.84	                                                                
9.77/2.84	         [mark(first(X1, X2))] =  [0]                           
9.77/2.84	                               ?  [1]                           
9.77/2.84	                               =  [a__first(mark(X1), mark(X2))]
9.77/2.84	                                                                
9.77/2.84	               [mark(from(X))] =  [0]                           
9.77/2.84	                               ?  [4]                           
9.77/2.84	                               =  [a__from(X)]                  
9.77/2.84	                                                                
9.77/2.84	           [mark(and(X1, X2))] =  [0]                           
9.77/2.84	                               >= [0]                           
9.77/2.84	                               =  [a__and(mark(X1), X2)]        
9.77/2.84	                                                                
9.77/2.84	        [mark(if(X1, X2, X3))] =  [0]                           
9.77/2.84	                               ?  [4]                           
9.77/2.84	                               =  [a__if(mark(X1), X2, X3)]     
9.77/2.84	                                                                
9.77/2.84	           [a__if(X1, X2, X3)] =  [1] X1 + [4]                  
9.77/2.84	                               >  [1] X1 + [3]                  
9.77/2.84	                               =  [if(X1, X2, X3)]              
9.77/2.84	                                                                
9.77/2.84	         [a__if(true(), X, Y)] =  [4]                           
9.77/2.84	                               >  [0]                           
9.77/2.84	                               =  [mark(X)]                     
9.77/2.84	                                                                
9.77/2.84	        [a__if(false(), X, Y)] =  [4]                           
9.77/2.84	                               >  [0]                           
9.77/2.84	                               =  [mark(Y)]                     
9.77/2.84	                                                                
9.77/2.84	              [a__add(X1, X2)] =  [1] X1 + [4]                  
9.77/2.84	                               >  [1] X1 + [2]                  
9.77/2.84	                               =  [add(X1, X2)]                 
9.77/2.84	                                                                
9.77/2.84	              [a__add(0(), X)] =  [4]                           
9.77/2.84	                               >  [0]                           
9.77/2.84	                               =  [mark(X)]                     
9.77/2.84	                                                                
9.77/2.84	             [a__add(s(X), Y)] =  [4]                           
9.77/2.84	                               >  [0]                           
9.77/2.84	                               =  [s(add(X, Y))]                
9.77/2.84	                                                                
9.77/2.84	            [a__first(X1, X2)] =  [1] X1 + [1] X2 + [1]         
9.77/2.84	                               ?  [1] X1 + [1] X2 + [5]         
9.77/2.84	                               =  [first(X1, X2)]               
9.77/2.84	                                                                
9.77/2.84	            [a__first(0(), X)] =  [1] X + [1]                   
9.77/2.84	                               >  [0]                           
9.77/2.84	                               =  [nil()]                       
9.77/2.84	                                                                
9.77/2.84	  [a__first(s(X), cons(Y, Z))] =  [1]                           
9.77/2.84	                               >  [0]                           
9.77/2.84	                               =  [cons(Y, first(X, Z))]        
9.77/2.84	                                                                
9.77/2.84	                  [a__from(X)] =  [4]                           
9.77/2.84	                               >  [0]                           
9.77/2.84	                               =  [cons(X, from(s(X)))]         
9.77/2.84	                                                                
9.77/2.84	                  [a__from(X)] =  [4]                           
9.77/2.84	                               >  [2]                           
9.77/2.84	                               =  [from(X)]                     
9.77/2.84	                                                                
9.77/2.84	
9.77/2.84	Further, it can be verified that all rules not oriented are covered by the weightgap condition.
9.77/2.84	
9.77/2.84	We are left with following problem, upon which TcT provides the
9.77/2.84	certificate YES(O(1),O(n^1)).
9.77/2.84	
9.77/2.84	Strict Trs:
9.77/2.84	  { mark(true()) -> true()
9.77/2.84	  , mark(false()) -> false()
9.77/2.84	  , mark(0()) -> 0()
9.77/2.84	  , mark(s(X)) -> s(X)
9.77/2.84	  , mark(add(X1, X2)) -> a__add(mark(X1), X2)
9.77/2.84	  , mark(nil()) -> nil()
9.77/2.84	  , mark(cons(X1, X2)) -> cons(X1, X2)
9.77/2.84	  , mark(first(X1, X2)) -> a__first(mark(X1), mark(X2))
9.77/2.84	  , mark(from(X)) -> a__from(X)
9.77/2.84	  , mark(and(X1, X2)) -> a__and(mark(X1), X2)
9.77/2.84	  , mark(if(X1, X2, X3)) -> a__if(mark(X1), X2, X3)
9.77/2.84	  , a__first(X1, X2) -> first(X1, X2) }
9.77/2.84	Weak Trs:
9.77/2.84	  { a__and(X1, X2) -> and(X1, X2)
9.77/2.84	  , a__and(true(), X) -> mark(X)
9.77/2.84	  , a__and(false(), Y) -> false()
9.77/2.84	  , a__if(X1, X2, X3) -> if(X1, X2, X3)
9.77/2.84	  , a__if(true(), X, Y) -> mark(X)
9.77/2.84	  , a__if(false(), X, Y) -> mark(Y)
9.77/2.84	  , a__add(X1, X2) -> add(X1, X2)
9.77/2.84	  , a__add(0(), X) -> mark(X)
9.77/2.84	  , a__add(s(X), Y) -> s(add(X, Y))
9.77/2.84	  , a__first(0(), X) -> nil()
9.77/2.84	  , a__first(s(X), cons(Y, Z)) -> cons(Y, first(X, Z))
9.77/2.84	  , a__from(X) -> cons(X, from(s(X)))
9.77/2.84	  , a__from(X) -> from(X) }
9.77/2.84	Obligation:
9.77/2.84	  innermost runtime complexity
9.77/2.84	Answer:
9.77/2.84	  YES(O(1),O(n^1))
9.77/2.84	
9.77/2.84	The weightgap principle applies (using the following nonconstant
9.77/2.84	growth matrix-interpretation)
9.77/2.84	
9.77/2.84	The following argument positions are usable:
9.77/2.84	  Uargs(a__and) = {1}, Uargs(a__if) = {1}, Uargs(a__add) = {1},
9.77/2.84	  Uargs(a__first) = {1, 2}
9.77/2.84	
9.77/2.84	TcT has computed the following matrix interpretation satisfying
9.77/2.84	not(EDA) and not(IDA(1)).
9.77/2.84	
9.77/2.84	     [a__and](x1, x2) = [1] x1 + [0]         
9.77/2.84	                                             
9.77/2.84	               [true] = [0]                  
9.77/2.84	                                             
9.77/2.84	           [mark](x1) = [0]                  
9.77/2.84	                                             
9.77/2.84	              [false] = [0]                  
9.77/2.84	                                             
9.77/2.84	  [a__if](x1, x2, x3) = [1] x1 + [4]         
9.77/2.84	                                             
9.77/2.84	     [a__add](x1, x2) = [1] x1 + [4]         
9.77/2.84	                                             
9.77/2.84	                  [0] = [0]                  
9.77/2.84	                                             
9.77/2.84	              [s](x1) = [0]                  
9.77/2.84	                                             
9.77/2.84	        [add](x1, x2) = [1] x1 + [1]         
9.77/2.84	                                             
9.77/2.84	   [a__first](x1, x2) = [1] x1 + [1] x2 + [1]
9.77/2.84	                                             
9.77/2.84	                [nil] = [1]                  
9.77/2.84	                                             
9.77/2.84	       [cons](x1, x2) = [0]                  
9.77/2.84	                                             
9.77/2.84	      [first](x1, x2) = [1] x1 + [1] x2 + [0]
9.77/2.84	                                             
9.77/2.84	        [a__from](x1) = [4]                  
9.77/2.84	                                             
9.77/2.84	           [from](x1) = [2]                  
9.77/2.84	                                             
9.77/2.84	        [and](x1, x2) = [1] x1 + [0]         
9.77/2.84	                                             
9.77/2.84	     [if](x1, x2, x3) = [1] x1 + [3]         
9.77/2.84	
9.77/2.84	The order satisfies the following ordering constraints:
9.77/2.84	
9.77/2.84	              [a__and(X1, X2)] =  [1] X1 + [0]                  
9.77/2.84	                               >= [1] X1 + [0]                  
9.77/2.84	                               =  [and(X1, X2)]                 
9.77/2.84	                                                                
9.77/2.84	           [a__and(true(), X)] =  [0]                           
9.77/2.84	                               >= [0]                           
9.77/2.84	                               =  [mark(X)]                     
9.77/2.84	                                                                
9.77/2.84	          [a__and(false(), Y)] =  [0]                           
9.77/2.84	                               >= [0]                           
9.77/2.84	                               =  [false()]                     
9.77/2.84	                                                                
9.77/2.84	                [mark(true())] =  [0]                           
9.77/2.85	                               >= [0]                           
9.77/2.85	                               =  [true()]                      
9.77/2.85	                                                                
9.77/2.85	               [mark(false())] =  [0]                           
9.77/2.85	                               >= [0]                           
9.77/2.85	                               =  [false()]                     
9.77/2.85	                                                                
9.77/2.85	                   [mark(0())] =  [0]                           
9.77/2.85	                               >= [0]                           
9.77/2.85	                               =  [0()]                         
9.77/2.85	                                                                
9.77/2.85	                  [mark(s(X))] =  [0]                           
9.77/2.85	                               >= [0]                           
9.77/2.85	                               =  [s(X)]                        
9.77/2.85	                                                                
9.77/2.85	           [mark(add(X1, X2))] =  [0]                           
9.77/2.85	                               ?  [4]                           
9.77/2.85	                               =  [a__add(mark(X1), X2)]        
9.77/2.85	                                                                
9.77/2.85	                 [mark(nil())] =  [0]                           
9.77/2.85	                               ?  [1]                           
9.77/2.85	                               =  [nil()]                       
9.77/2.85	                                                                
9.77/2.85	          [mark(cons(X1, X2))] =  [0]                           
9.77/2.85	                               >= [0]                           
9.77/2.85	                               =  [cons(X1, X2)]                
9.77/2.85	                                                                
9.77/2.85	         [mark(first(X1, X2))] =  [0]                           
9.77/2.85	                               ?  [1]                           
9.77/2.85	                               =  [a__first(mark(X1), mark(X2))]
9.77/2.85	                                                                
9.77/2.85	               [mark(from(X))] =  [0]                           
9.77/2.85	                               ?  [4]                           
9.77/2.85	                               =  [a__from(X)]                  
9.77/2.85	                                                                
9.77/2.85	           [mark(and(X1, X2))] =  [0]                           
9.77/2.85	                               >= [0]                           
9.77/2.85	                               =  [a__and(mark(X1), X2)]        
9.77/2.85	                                                                
9.77/2.85	        [mark(if(X1, X2, X3))] =  [0]                           
9.77/2.85	                               ?  [4]                           
9.77/2.85	                               =  [a__if(mark(X1), X2, X3)]     
9.77/2.85	                                                                
9.77/2.85	           [a__if(X1, X2, X3)] =  [1] X1 + [4]                  
9.77/2.85	                               >  [1] X1 + [3]                  
9.77/2.85	                               =  [if(X1, X2, X3)]              
9.77/2.85	                                                                
9.77/2.85	         [a__if(true(), X, Y)] =  [4]                           
9.77/2.85	                               >  [0]                           
9.77/2.85	                               =  [mark(X)]                     
9.77/2.85	                                                                
9.77/2.85	        [a__if(false(), X, Y)] =  [4]                           
9.77/2.85	                               >  [0]                           
9.77/2.85	                               =  [mark(Y)]                     
9.77/2.85	                                                                
9.77/2.85	              [a__add(X1, X2)] =  [1] X1 + [4]                  
9.77/2.85	                               >  [1] X1 + [1]                  
9.77/2.85	                               =  [add(X1, X2)]                 
9.77/2.85	                                                                
9.77/2.85	              [a__add(0(), X)] =  [4]                           
9.77/2.85	                               >  [0]                           
9.77/2.85	                               =  [mark(X)]                     
9.77/2.85	                                                                
9.77/2.85	             [a__add(s(X), Y)] =  [4]                           
9.77/2.85	                               >  [0]                           
9.77/2.85	                               =  [s(add(X, Y))]                
9.77/2.85	                                                                
9.77/2.85	            [a__first(X1, X2)] =  [1] X1 + [1] X2 + [1]         
9.77/2.85	                               >  [1] X1 + [1] X2 + [0]         
9.77/2.85	                               =  [first(X1, X2)]               
9.77/2.85	                                                                
9.77/2.85	            [a__first(0(), X)] =  [1] X + [1]                   
9.77/2.85	                               >= [1]                           
9.77/2.85	                               =  [nil()]                       
9.77/2.85	                                                                
9.77/2.85	  [a__first(s(X), cons(Y, Z))] =  [1]                           
9.77/2.85	                               >  [0]                           
9.77/2.85	                               =  [cons(Y, first(X, Z))]        
9.77/2.85	                                                                
9.77/2.85	                  [a__from(X)] =  [4]                           
9.77/2.85	                               >  [0]                           
9.77/2.85	                               =  [cons(X, from(s(X)))]         
9.77/2.85	                                                                
9.77/2.85	                  [a__from(X)] =  [4]                           
9.77/2.85	                               >  [2]                           
9.77/2.85	                               =  [from(X)]                     
9.77/2.85	                                                                
9.77/2.85	
9.77/2.85	Further, it can be verified that all rules not oriented are covered by the weightgap condition.
9.77/2.85	
9.77/2.85	We are left with following problem, upon which TcT provides the
9.77/2.85	certificate YES(O(1),O(n^1)).
9.77/2.85	
9.77/2.85	Strict Trs:
9.77/2.85	  { mark(true()) -> true()
9.77/2.85	  , mark(false()) -> false()
9.77/2.85	  , mark(0()) -> 0()
9.77/2.85	  , mark(s(X)) -> s(X)
9.77/2.85	  , mark(add(X1, X2)) -> a__add(mark(X1), X2)
9.77/2.85	  , mark(nil()) -> nil()
9.77/2.85	  , mark(cons(X1, X2)) -> cons(X1, X2)
9.77/2.85	  , mark(first(X1, X2)) -> a__first(mark(X1), mark(X2))
9.77/2.85	  , mark(from(X)) -> a__from(X)
9.77/2.85	  , mark(and(X1, X2)) -> a__and(mark(X1), X2)
9.77/2.85	  , mark(if(X1, X2, X3)) -> a__if(mark(X1), X2, X3) }
9.77/2.85	Weak Trs:
9.77/2.85	  { a__and(X1, X2) -> and(X1, X2)
9.77/2.85	  , a__and(true(), X) -> mark(X)
9.77/2.85	  , a__and(false(), Y) -> false()
9.77/2.85	  , a__if(X1, X2, X3) -> if(X1, X2, X3)
9.77/2.85	  , a__if(true(), X, Y) -> mark(X)
9.77/2.85	  , a__if(false(), X, Y) -> mark(Y)
9.77/2.85	  , a__add(X1, X2) -> add(X1, X2)
9.77/2.85	  , a__add(0(), X) -> mark(X)
9.77/2.85	  , a__add(s(X), Y) -> s(add(X, Y))
9.77/2.85	  , a__first(X1, X2) -> first(X1, X2)
9.77/2.85	  , a__first(0(), X) -> nil()
9.77/2.85	  , a__first(s(X), cons(Y, Z)) -> cons(Y, first(X, Z))
9.77/2.85	  , a__from(X) -> cons(X, from(s(X)))
9.77/2.85	  , a__from(X) -> from(X) }
9.77/2.85	Obligation:
9.77/2.85	  innermost runtime complexity
9.77/2.85	Answer:
9.77/2.85	  YES(O(1),O(n^1))
9.77/2.85	
9.77/2.85	The weightgap principle applies (using the following nonconstant
9.77/2.85	growth matrix-interpretation)
9.77/2.85	
9.77/2.85	The following argument positions are usable:
9.77/2.85	  Uargs(a__and) = {1}, Uargs(a__if) = {1}, Uargs(a__add) = {1},
9.77/2.85	  Uargs(a__first) = {1, 2}
9.77/2.85	
9.77/2.85	TcT has computed the following matrix interpretation satisfying
9.77/2.85	not(EDA) and not(IDA(1)).
9.77/2.85	
9.77/2.85	     [a__and](x1, x2) = [1] x1 + [4]         
9.77/2.85	                                             
9.77/2.85	               [true] = [4]                  
9.77/2.85	                                             
9.77/2.85	           [mark](x1) = [1]                  
9.77/2.85	                                             
9.77/2.85	              [false] = [4]                  
9.77/2.85	                                             
9.77/2.85	  [a__if](x1, x2, x3) = [1] x1 + [0]         
9.77/2.85	                                             
9.77/2.85	     [a__add](x1, x2) = [1] x1 + [4]         
9.77/2.85	                                             
9.77/2.85	                  [0] = [0]                  
9.77/2.85	                                             
9.77/2.85	              [s](x1) = [0]                  
9.77/2.85	                                             
9.77/2.85	        [add](x1, x2) = [1] x1 + [1]         
9.77/2.85	                                             
9.77/2.85	   [a__first](x1, x2) = [1] x1 + [1] x2 + [6]
9.77/2.85	                                             
9.77/2.85	                [nil] = [0]                  
9.77/2.85	                                             
9.77/2.85	       [cons](x1, x2) = [0]                  
9.77/2.85	                                             
9.77/2.85	      [first](x1, x2) = [1] x1 + [1] x2 + [2]
9.77/2.85	                                             
9.77/2.85	        [a__from](x1) = [0]                  
9.77/2.85	                                             
9.77/2.85	           [from](x1) = [0]                  
9.77/2.85	                                             
9.77/2.85	        [and](x1, x2) = [1] x1 + [3]         
9.77/2.85	                                             
9.77/2.85	     [if](x1, x2, x3) = [1] x1 + [0]         
9.77/2.85	
9.77/2.85	The order satisfies the following ordering constraints:
9.77/2.85	
9.77/2.85	              [a__and(X1, X2)] =  [1] X1 + [4]                  
9.77/2.85	                               >  [1] X1 + [3]                  
9.77/2.85	                               =  [and(X1, X2)]                 
9.77/2.85	                                                                
9.77/2.85	           [a__and(true(), X)] =  [8]                           
9.77/2.85	                               >  [1]                           
9.77/2.85	                               =  [mark(X)]                     
9.77/2.85	                                                                
9.77/2.85	          [a__and(false(), Y)] =  [8]                           
9.77/2.85	                               >  [4]                           
9.77/2.85	                               =  [false()]                     
9.77/2.85	                                                                
9.77/2.85	                [mark(true())] =  [1]                           
9.77/2.85	                               ?  [4]                           
9.77/2.85	                               =  [true()]                      
9.77/2.85	                                                                
9.77/2.85	               [mark(false())] =  [1]                           
9.77/2.85	                               ?  [4]                           
9.77/2.85	                               =  [false()]                     
9.77/2.85	                                                                
9.77/2.85	                   [mark(0())] =  [1]                           
9.77/2.85	                               >  [0]                           
9.77/2.85	                               =  [0()]                         
9.77/2.85	                                                                
9.77/2.85	                  [mark(s(X))] =  [1]                           
9.77/2.85	                               >  [0]                           
9.77/2.85	                               =  [s(X)]                        
9.77/2.85	                                                                
9.77/2.85	           [mark(add(X1, X2))] =  [1]                           
9.77/2.85	                               ?  [5]                           
9.77/2.85	                               =  [a__add(mark(X1), X2)]        
9.77/2.85	                                                                
9.77/2.85	                 [mark(nil())] =  [1]                           
9.77/2.85	                               >  [0]                           
9.77/2.85	                               =  [nil()]                       
9.77/2.85	                                                                
9.77/2.85	          [mark(cons(X1, X2))] =  [1]                           
9.77/2.85	                               >  [0]                           
9.77/2.85	                               =  [cons(X1, X2)]                
9.77/2.85	                                                                
9.77/2.85	         [mark(first(X1, X2))] =  [1]                           
9.77/2.85	                               ?  [8]                           
9.77/2.85	                               =  [a__first(mark(X1), mark(X2))]
9.77/2.85	                                                                
9.77/2.85	               [mark(from(X))] =  [1]                           
9.77/2.85	                               >  [0]                           
9.77/2.85	                               =  [a__from(X)]                  
9.77/2.85	                                                                
9.77/2.85	           [mark(and(X1, X2))] =  [1]                           
9.77/2.85	                               ?  [5]                           
9.77/2.85	                               =  [a__and(mark(X1), X2)]        
9.77/2.85	                                                                
9.77/2.85	        [mark(if(X1, X2, X3))] =  [1]                           
9.77/2.85	                               >= [1]                           
9.77/2.85	                               =  [a__if(mark(X1), X2, X3)]     
9.77/2.85	                                                                
9.77/2.85	           [a__if(X1, X2, X3)] =  [1] X1 + [0]                  
9.77/2.85	                               >= [1] X1 + [0]                  
9.77/2.85	                               =  [if(X1, X2, X3)]              
9.77/2.85	                                                                
9.77/2.85	         [a__if(true(), X, Y)] =  [4]                           
9.77/2.85	                               >  [1]                           
9.77/2.85	                               =  [mark(X)]                     
9.77/2.85	                                                                
9.77/2.85	        [a__if(false(), X, Y)] =  [4]                           
9.77/2.85	                               >  [1]                           
9.77/2.85	                               =  [mark(Y)]                     
9.77/2.85	                                                                
9.77/2.85	              [a__add(X1, X2)] =  [1] X1 + [4]                  
9.77/2.85	                               >  [1] X1 + [1]                  
9.77/2.85	                               =  [add(X1, X2)]                 
9.77/2.85	                                                                
9.77/2.85	              [a__add(0(), X)] =  [4]                           
9.77/2.85	                               >  [1]                           
9.77/2.85	                               =  [mark(X)]                     
9.77/2.85	                                                                
9.77/2.85	             [a__add(s(X), Y)] =  [4]                           
9.77/2.85	                               >  [0]                           
9.77/2.85	                               =  [s(add(X, Y))]                
9.77/2.85	                                                                
9.77/2.85	            [a__first(X1, X2)] =  [1] X1 + [1] X2 + [6]         
9.77/2.85	                               >  [1] X1 + [1] X2 + [2]         
9.77/2.85	                               =  [first(X1, X2)]               
9.77/2.85	                                                                
9.77/2.85	            [a__first(0(), X)] =  [1] X + [6]                   
9.77/2.85	                               >  [0]                           
9.77/2.85	                               =  [nil()]                       
9.77/2.85	                                                                
9.77/2.85	  [a__first(s(X), cons(Y, Z))] =  [6]                           
9.77/2.85	                               >  [0]                           
9.77/2.85	                               =  [cons(Y, first(X, Z))]        
9.77/2.85	                                                                
9.77/2.85	                  [a__from(X)] =  [0]                           
9.77/2.85	                               >= [0]                           
9.77/2.85	                               =  [cons(X, from(s(X)))]         
9.77/2.85	                                                                
9.77/2.85	                  [a__from(X)] =  [0]                           
9.77/2.85	                               >= [0]                           
9.77/2.85	                               =  [from(X)]                     
9.77/2.85	                                                                
9.77/2.85	
9.77/2.85	Further, it can be verified that all rules not oriented are covered by the weightgap condition.
9.77/2.85	
9.77/2.85	We are left with following problem, upon which TcT provides the
9.77/2.85	certificate YES(O(1),O(n^1)).
9.77/2.85	
9.77/2.85	Strict Trs:
9.77/2.85	  { mark(true()) -> true()
9.77/2.85	  , mark(false()) -> false()
9.77/2.85	  , mark(add(X1, X2)) -> a__add(mark(X1), X2)
9.77/2.85	  , mark(first(X1, X2)) -> a__first(mark(X1), mark(X2))
9.77/2.85	  , mark(and(X1, X2)) -> a__and(mark(X1), X2)
9.77/2.85	  , mark(if(X1, X2, X3)) -> a__if(mark(X1), X2, X3) }
9.77/2.85	Weak Trs:
9.77/2.85	  { a__and(X1, X2) -> and(X1, X2)
9.77/2.85	  , a__and(true(), X) -> mark(X)
9.77/2.85	  , a__and(false(), Y) -> false()
9.77/2.85	  , mark(0()) -> 0()
9.77/2.85	  , mark(s(X)) -> s(X)
9.77/2.85	  , mark(nil()) -> nil()
9.77/2.85	  , mark(cons(X1, X2)) -> cons(X1, X2)
9.77/2.85	  , mark(from(X)) -> a__from(X)
9.77/2.85	  , a__if(X1, X2, X3) -> if(X1, X2, X3)
9.77/2.85	  , a__if(true(), X, Y) -> mark(X)
9.77/2.85	  , a__if(false(), X, Y) -> mark(Y)
9.77/2.85	  , a__add(X1, X2) -> add(X1, X2)
9.77/2.85	  , a__add(0(), X) -> mark(X)
9.77/2.85	  , a__add(s(X), Y) -> s(add(X, Y))
9.77/2.85	  , a__first(X1, X2) -> first(X1, X2)
9.77/2.85	  , a__first(0(), X) -> nil()
9.77/2.85	  , a__first(s(X), cons(Y, Z)) -> cons(Y, first(X, Z))
9.77/2.85	  , a__from(X) -> cons(X, from(s(X)))
9.77/2.85	  , a__from(X) -> from(X) }
9.77/2.85	Obligation:
9.77/2.85	  innermost runtime complexity
9.77/2.85	Answer:
9.77/2.85	  YES(O(1),O(n^1))
9.77/2.85	
9.77/2.85	The weightgap principle applies (using the following nonconstant
9.77/2.85	growth matrix-interpretation)
9.77/2.85	
9.77/2.85	The following argument positions are usable:
9.77/2.85	  Uargs(a__and) = {1}, Uargs(a__if) = {1}, Uargs(a__add) = {1},
9.77/2.85	  Uargs(a__first) = {1, 2}
9.77/2.85	
9.77/2.85	TcT has computed the following matrix interpretation satisfying
9.77/2.85	not(EDA) and not(IDA(1)).
9.77/2.85	
9.77/2.85	     [a__and](x1, x2) = [1] x1 + [1] x2 + [0]         
9.77/2.85	                                                      
9.77/2.85	               [true] = [4]                           
9.77/2.85	                                                      
9.77/2.85	           [mark](x1) = [1] x1 + [1]                  
9.77/2.85	                                                      
9.77/2.85	              [false] = [0]                           
9.77/2.85	                                                      
9.77/2.85	  [a__if](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [4]
9.77/2.85	                                                      
9.77/2.85	     [a__add](x1, x2) = [1] x1 + [1] x2 + [0]         
9.77/2.85	                                                      
9.77/2.85	                  [0] = [4]                           
9.77/2.85	                                                      
9.77/2.85	              [s](x1) = [0]                           
9.77/2.85	                                                      
9.77/2.85	        [add](x1, x2) = [1] x1 + [1] x2 + [0]         
9.77/2.85	                                                      
9.77/2.85	   [a__first](x1, x2) = [1] x1 + [1] x2 + [6]         
9.77/2.85	                                                      
9.77/2.85	                [nil] = [5]                           
9.77/2.85	                                                      
9.77/2.85	       [cons](x1, x2) = [0]                           
9.77/2.85	                                                      
9.77/2.85	      [first](x1, x2) = [1] x1 + [1] x2 + [0]         
9.77/2.85	                                                      
9.77/2.85	        [a__from](x1) = [4]                           
9.77/2.85	                                                      
9.77/2.85	           [from](x1) = [3]                           
9.77/2.85	                                                      
9.77/2.85	        [and](x1, x2) = [1] x1 + [1] x2 + [0]         
9.77/2.85	                                                      
9.77/2.85	     [if](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0]
9.77/2.85	
9.77/2.85	The order satisfies the following ordering constraints:
9.77/2.85	
9.77/2.85	              [a__and(X1, X2)] =  [1] X1 + [1] X2 + [0]         
9.77/2.85	                               >= [1] X1 + [1] X2 + [0]         
9.77/2.85	                               =  [and(X1, X2)]                 
9.77/2.85	                                                                
9.77/2.85	           [a__and(true(), X)] =  [1] X + [4]                   
9.77/2.85	                               >  [1] X + [1]                   
9.77/2.85	                               =  [mark(X)]                     
9.77/2.85	                                                                
9.77/2.85	          [a__and(false(), Y)] =  [1] Y + [0]                   
9.77/2.85	                               >= [0]                           
9.77/2.85	                               =  [false()]                     
9.77/2.85	                                                                
9.77/2.85	                [mark(true())] =  [5]                           
9.77/2.85	                               >  [4]                           
9.77/2.85	                               =  [true()]                      
9.77/2.85	                                                                
9.77/2.85	               [mark(false())] =  [1]                           
9.77/2.85	                               >  [0]                           
9.77/2.85	                               =  [false()]                     
9.77/2.85	                                                                
9.77/2.85	                   [mark(0())] =  [5]                           
9.77/2.85	                               >  [4]                           
9.77/2.85	                               =  [0()]                         
9.77/2.85	                                                                
9.77/2.85	                  [mark(s(X))] =  [1]                           
9.77/2.85	                               >  [0]                           
9.77/2.85	                               =  [s(X)]                        
9.77/2.85	                                                                
9.77/2.85	           [mark(add(X1, X2))] =  [1] X1 + [1] X2 + [1]         
9.77/2.85	                               >= [1] X1 + [1] X2 + [1]         
9.77/2.85	                               =  [a__add(mark(X1), X2)]        
9.77/2.85	                                                                
9.77/2.85	                 [mark(nil())] =  [6]                           
9.77/2.85	                               >  [5]                           
9.77/2.85	                               =  [nil()]                       
9.77/2.85	                                                                
9.77/2.85	          [mark(cons(X1, X2))] =  [1]                           
9.77/2.85	                               >  [0]                           
9.77/2.85	                               =  [cons(X1, X2)]                
9.77/2.85	                                                                
9.77/2.85	         [mark(first(X1, X2))] =  [1] X1 + [1] X2 + [1]         
9.77/2.85	                               ?  [1] X1 + [1] X2 + [8]         
9.77/2.85	                               =  [a__first(mark(X1), mark(X2))]
9.77/2.85	                                                                
9.77/2.85	               [mark(from(X))] =  [4]                           
9.77/2.85	                               >= [4]                           
9.77/2.85	                               =  [a__from(X)]                  
9.77/2.85	                                                                
9.77/2.85	           [mark(and(X1, X2))] =  [1] X1 + [1] X2 + [1]         
9.77/2.85	                               >= [1] X1 + [1] X2 + [1]         
9.77/2.85	                               =  [a__and(mark(X1), X2)]        
9.77/2.85	                                                                
9.77/2.85	        [mark(if(X1, X2, X3))] =  [1] X1 + [1] X2 + [1] X3 + [1]
9.77/2.85	                               ?  [1] X1 + [1] X2 + [1] X3 + [5]
9.77/2.85	                               =  [a__if(mark(X1), X2, X3)]     
9.77/2.85	                                                                
9.77/2.85	           [a__if(X1, X2, X3)] =  [1] X1 + [1] X2 + [1] X3 + [4]
9.77/2.85	                               >  [1] X1 + [1] X2 + [1] X3 + [0]
9.77/2.85	                               =  [if(X1, X2, X3)]              
9.77/2.85	                                                                
9.77/2.85	         [a__if(true(), X, Y)] =  [1] X + [1] Y + [8]           
9.77/2.85	                               >  [1] X + [1]                   
9.77/2.85	                               =  [mark(X)]                     
9.77/2.85	                                                                
9.77/2.85	        [a__if(false(), X, Y)] =  [1] X + [1] Y + [4]           
9.77/2.85	                               >  [1] Y + [1]                   
9.77/2.85	                               =  [mark(Y)]                     
9.77/2.85	                                                                
9.77/2.85	              [a__add(X1, X2)] =  [1] X1 + [1] X2 + [0]         
9.77/2.85	                               >= [1] X1 + [1] X2 + [0]         
9.77/2.85	                               =  [add(X1, X2)]                 
9.77/2.85	                                                                
9.77/2.85	              [a__add(0(), X)] =  [1] X + [4]                   
9.77/2.85	                               >  [1] X + [1]                   
9.77/2.85	                               =  [mark(X)]                     
9.77/2.85	                                                                
9.77/2.85	             [a__add(s(X), Y)] =  [1] Y + [0]                   
9.77/2.85	                               >= [0]                           
9.77/2.85	                               =  [s(add(X, Y))]                
9.77/2.85	                                                                
9.77/2.85	            [a__first(X1, X2)] =  [1] X1 + [1] X2 + [6]         
9.77/2.85	                               >  [1] X1 + [1] X2 + [0]         
9.77/2.85	                               =  [first(X1, X2)]               
9.77/2.85	                                                                
9.77/2.85	            [a__first(0(), X)] =  [1] X + [10]                  
9.77/2.85	                               >  [5]                           
9.77/2.85	                               =  [nil()]                       
9.77/2.85	                                                                
9.77/2.85	  [a__first(s(X), cons(Y, Z))] =  [6]                           
9.77/2.85	                               >  [0]                           
9.77/2.85	                               =  [cons(Y, first(X, Z))]        
9.77/2.85	                                                                
9.77/2.85	                  [a__from(X)] =  [4]                           
9.77/2.85	                               >  [0]                           
9.77/2.85	                               =  [cons(X, from(s(X)))]         
9.77/2.85	                                                                
9.77/2.85	                  [a__from(X)] =  [4]                           
9.77/2.85	                               >  [3]                           
9.77/2.85	                               =  [from(X)]                     
9.77/2.85	                                                                
9.77/2.85	
9.77/2.85	Further, it can be verified that all rules not oriented are covered by the weightgap condition.
9.77/2.85	
9.77/2.85	We are left with following problem, upon which TcT provides the
9.77/2.85	certificate YES(O(1),O(n^1)).
9.77/2.85	
9.77/2.85	Strict Trs:
9.77/2.85	  { mark(add(X1, X2)) -> a__add(mark(X1), X2)
9.77/2.85	  , mark(first(X1, X2)) -> a__first(mark(X1), mark(X2))
9.77/2.85	  , mark(and(X1, X2)) -> a__and(mark(X1), X2)
9.77/2.85	  , mark(if(X1, X2, X3)) -> a__if(mark(X1), X2, X3) }
9.77/2.85	Weak Trs:
9.77/2.85	  { a__and(X1, X2) -> and(X1, X2)
9.77/2.85	  , a__and(true(), X) -> mark(X)
9.77/2.85	  , a__and(false(), Y) -> false()
9.77/2.85	  , mark(true()) -> true()
9.77/2.85	  , mark(false()) -> false()
9.77/2.85	  , mark(0()) -> 0()
9.77/2.85	  , mark(s(X)) -> s(X)
9.77/2.85	  , mark(nil()) -> nil()
9.77/2.85	  , mark(cons(X1, X2)) -> cons(X1, X2)
9.77/2.85	  , mark(from(X)) -> a__from(X)
9.77/2.85	  , a__if(X1, X2, X3) -> if(X1, X2, X3)
9.77/2.85	  , a__if(true(), X, Y) -> mark(X)
9.77/2.85	  , a__if(false(), X, Y) -> mark(Y)
9.77/2.85	  , a__add(X1, X2) -> add(X1, X2)
9.77/2.85	  , a__add(0(), X) -> mark(X)
9.77/2.85	  , a__add(s(X), Y) -> s(add(X, Y))
9.77/2.85	  , a__first(X1, X2) -> first(X1, X2)
9.77/2.85	  , a__first(0(), X) -> nil()
9.77/2.85	  , a__first(s(X), cons(Y, Z)) -> cons(Y, first(X, Z))
9.77/2.85	  , a__from(X) -> cons(X, from(s(X)))
9.77/2.85	  , a__from(X) -> from(X) }
9.77/2.85	Obligation:
9.77/2.85	  innermost runtime complexity
9.77/2.85	Answer:
9.77/2.85	  YES(O(1),O(n^1))
9.77/2.85	
9.77/2.85	We use the processor 'matrix interpretation of dimension 1' to
9.77/2.85	orient following rules strictly.
9.77/2.85	
9.77/2.85	Trs:
9.77/2.85	  { mark(add(X1, X2)) -> a__add(mark(X1), X2)
9.77/2.85	  , mark(first(X1, X2)) -> a__first(mark(X1), mark(X2)) }
9.77/2.85	
9.77/2.85	The induced complexity on above rules (modulo remaining rules) is
9.77/2.85	YES(?,O(n^1)) . These rules are moved into the corresponding weak
9.77/2.85	component(s).
9.77/2.85	
9.77/2.85	Sub-proof:
9.77/2.85	----------
9.77/2.85	  The following argument positions are usable:
9.77/2.85	    Uargs(a__and) = {1}, Uargs(a__if) = {1}, Uargs(a__add) = {1},
9.77/2.85	    Uargs(a__first) = {1, 2}
9.77/2.85	  
9.77/2.85	  TcT has computed the following constructor-based matrix
9.77/2.85	  interpretation satisfying not(EDA).
9.77/2.85	  
9.77/2.85	       [a__and](x1, x2) = [1] x1 + [2] x2 + [0]         
9.77/2.85	                                                        
9.77/2.85	                 [true] = [0]                           
9.77/2.85	                                                        
9.77/2.85	             [mark](x1) = [2] x1 + [0]                  
9.77/2.85	                                                        
9.77/2.85	                [false] = [0]                           
9.77/2.85	                                                        
9.77/2.85	    [a__if](x1, x2, x3) = [1] x1 + [2] x2 + [2] x3 + [0]
9.77/2.85	                                                        
9.77/2.85	       [a__add](x1, x2) = [1] x1 + [2] x2 + [4]         
9.77/2.85	                                                        
9.77/2.85	                    [0] = [4]                           
9.77/2.85	                                                        
9.77/2.85	                [s](x1) = [4]                           
9.77/2.85	                                                        
9.77/2.85	          [add](x1, x2) = [1] x1 + [1] x2 + [4]         
9.77/2.85	                                                        
9.77/2.85	     [a__first](x1, x2) = [1] x1 + [1] x2 + [4]         
9.77/2.85	                                                        
9.77/2.85	                  [nil] = [4]                           
9.77/2.85	                                                        
9.77/2.85	         [cons](x1, x2) = [0]                           
9.77/2.85	                                                        
9.77/2.85	        [first](x1, x2) = [1] x1 + [1] x2 + [4]         
9.77/2.85	                                                        
9.77/2.85	          [a__from](x1) = [0]                           
9.77/2.85	                                                        
9.77/2.85	             [from](x1) = [0]                           
9.77/2.85	                                                        
9.77/2.85	          [and](x1, x2) = [1] x1 + [1] x2 + [0]         
9.77/2.85	                                                        
9.77/2.85	       [if](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0]
9.77/2.85	  
9.77/2.85	  The order satisfies the following ordering constraints:
9.77/2.85	  
9.77/2.85	                [a__and(X1, X2)] =  [1] X1 + [2] X2 + [0]         
9.77/2.85	                                 >= [1] X1 + [1] X2 + [0]         
9.77/2.85	                                 =  [and(X1, X2)]                 
9.77/2.85	                                                                  
9.77/2.85	             [a__and(true(), X)] =  [2] X + [0]                   
9.77/2.85	                                 >= [2] X + [0]                   
9.77/2.85	                                 =  [mark(X)]                     
9.77/2.85	                                                                  
9.77/2.85	            [a__and(false(), Y)] =  [2] Y + [0]                   
9.77/2.85	                                 >= [0]                           
9.77/2.85	                                 =  [false()]                     
9.77/2.85	                                                                  
9.77/2.85	                  [mark(true())] =  [0]                           
9.77/2.85	                                 >= [0]                           
9.77/2.85	                                 =  [true()]                      
9.77/2.85	                                                                  
9.77/2.85	                 [mark(false())] =  [0]                           
9.77/2.85	                                 >= [0]                           
9.77/2.85	                                 =  [false()]                     
9.77/2.85	                                                                  
9.77/2.85	                     [mark(0())] =  [8]                           
9.77/2.85	                                 >  [4]                           
9.77/2.85	                                 =  [0()]                         
9.77/2.85	                                                                  
9.77/2.85	                    [mark(s(X))] =  [8]                           
9.77/2.85	                                 >  [4]                           
9.77/2.85	                                 =  [s(X)]                        
9.77/2.85	                                                                  
9.77/2.85	             [mark(add(X1, X2))] =  [2] X1 + [2] X2 + [8]         
9.77/2.85	                                 >  [2] X1 + [2] X2 + [4]         
9.77/2.85	                                 =  [a__add(mark(X1), X2)]        
9.77/2.85	                                                                  
9.77/2.85	                   [mark(nil())] =  [8]                           
9.77/2.85	                                 >  [4]                           
9.77/2.85	                                 =  [nil()]                       
9.77/2.85	                                                                  
9.77/2.85	            [mark(cons(X1, X2))] =  [0]                           
9.77/2.85	                                 >= [0]                           
9.77/2.85	                                 =  [cons(X1, X2)]                
9.77/2.85	                                                                  
9.77/2.85	           [mark(first(X1, X2))] =  [2] X1 + [2] X2 + [8]         
9.77/2.85	                                 >  [2] X1 + [2] X2 + [4]         
9.77/2.85	                                 =  [a__first(mark(X1), mark(X2))]
9.77/2.85	                                                                  
9.77/2.85	                 [mark(from(X))] =  [0]                           
9.77/2.85	                                 >= [0]                           
9.77/2.85	                                 =  [a__from(X)]                  
9.77/2.85	                                                                  
9.77/2.85	             [mark(and(X1, X2))] =  [2] X1 + [2] X2 + [0]         
9.77/2.85	                                 >= [2] X1 + [2] X2 + [0]         
9.77/2.85	                                 =  [a__and(mark(X1), X2)]        
9.77/2.85	                                                                  
9.77/2.85	          [mark(if(X1, X2, X3))] =  [2] X1 + [2] X2 + [2] X3 + [0]
9.77/2.85	                                 >= [2] X1 + [2] X2 + [2] X3 + [0]
9.77/2.85	                                 =  [a__if(mark(X1), X2, X3)]     
9.77/2.85	                                                                  
9.77/2.85	             [a__if(X1, X2, X3)] =  [1] X1 + [2] X2 + [2] X3 + [0]
9.77/2.85	                                 >= [1] X1 + [1] X2 + [1] X3 + [0]
9.77/2.85	                                 =  [if(X1, X2, X3)]              
9.77/2.85	                                                                  
9.77/2.85	           [a__if(true(), X, Y)] =  [2] X + [2] Y + [0]           
9.77/2.85	                                 >= [2] X + [0]                   
9.77/2.85	                                 =  [mark(X)]                     
9.77/2.85	                                                                  
9.77/2.85	          [a__if(false(), X, Y)] =  [2] X + [2] Y + [0]           
9.77/2.85	                                 >= [2] Y + [0]                   
9.77/2.85	                                 =  [mark(Y)]                     
9.77/2.85	                                                                  
9.77/2.85	                [a__add(X1, X2)] =  [1] X1 + [2] X2 + [4]         
9.77/2.85	                                 >= [1] X1 + [1] X2 + [4]         
9.77/2.85	                                 =  [add(X1, X2)]                 
9.77/2.85	                                                                  
9.77/2.85	                [a__add(0(), X)] =  [2] X + [8]                   
9.77/2.85	                                 >  [2] X + [0]                   
9.77/2.85	                                 =  [mark(X)]                     
9.77/2.85	                                                                  
9.77/2.85	               [a__add(s(X), Y)] =  [2] Y + [8]                   
9.77/2.85	                                 >  [4]                           
9.77/2.85	                                 =  [s(add(X, Y))]                
9.77/2.85	                                                                  
9.77/2.85	              [a__first(X1, X2)] =  [1] X1 + [1] X2 + [4]         
9.77/2.85	                                 >= [1] X1 + [1] X2 + [4]         
9.77/2.85	                                 =  [first(X1, X2)]               
9.77/2.85	                                                                  
9.77/2.85	              [a__first(0(), X)] =  [1] X + [8]                   
9.77/2.85	                                 >  [4]                           
9.77/2.85	                                 =  [nil()]                       
9.77/2.85	                                                                  
9.77/2.85	    [a__first(s(X), cons(Y, Z))] =  [8]                           
9.77/2.85	                                 >  [0]                           
9.77/2.85	                                 =  [cons(Y, first(X, Z))]        
9.77/2.85	                                                                  
9.77/2.85	                    [a__from(X)] =  [0]                           
9.77/2.85	                                 >= [0]                           
9.77/2.85	                                 =  [cons(X, from(s(X)))]         
9.77/2.85	                                                                  
9.77/2.85	                    [a__from(X)] =  [0]                           
9.77/2.85	                                 >= [0]                           
9.77/2.85	                                 =  [from(X)]                     
9.77/2.85	                                                                  
9.77/2.85	
9.77/2.85	We return to the main proof.
9.77/2.85	
9.77/2.85	We are left with following problem, upon which TcT provides the
9.77/2.85	certificate YES(O(1),O(n^1)).
9.77/2.85	
9.77/2.85	Strict Trs:
9.77/2.85	  { mark(and(X1, X2)) -> a__and(mark(X1), X2)
9.77/2.85	  , mark(if(X1, X2, X3)) -> a__if(mark(X1), X2, X3) }
9.77/2.85	Weak Trs:
9.77/2.85	  { a__and(X1, X2) -> and(X1, X2)
9.77/2.85	  , a__and(true(), X) -> mark(X)
9.77/2.85	  , a__and(false(), Y) -> false()
9.77/2.85	  , mark(true()) -> true()
9.77/2.85	  , mark(false()) -> false()
9.77/2.85	  , mark(0()) -> 0()
9.77/2.85	  , mark(s(X)) -> s(X)
9.77/2.85	  , mark(add(X1, X2)) -> a__add(mark(X1), X2)
9.77/2.85	  , mark(nil()) -> nil()
9.77/2.85	  , mark(cons(X1, X2)) -> cons(X1, X2)
9.77/2.85	  , mark(first(X1, X2)) -> a__first(mark(X1), mark(X2))
9.77/2.85	  , mark(from(X)) -> a__from(X)
9.77/2.85	  , a__if(X1, X2, X3) -> if(X1, X2, X3)
9.77/2.85	  , a__if(true(), X, Y) -> mark(X)
9.77/2.85	  , a__if(false(), X, Y) -> mark(Y)
9.77/2.85	  , a__add(X1, X2) -> add(X1, X2)
9.77/2.85	  , a__add(0(), X) -> mark(X)
9.77/2.85	  , a__add(s(X), Y) -> s(add(X, Y))
9.77/2.85	  , a__first(X1, X2) -> first(X1, X2)
9.77/2.85	  , a__first(0(), X) -> nil()
9.77/2.85	  , a__first(s(X), cons(Y, Z)) -> cons(Y, first(X, Z))
9.77/2.85	  , a__from(X) -> cons(X, from(s(X)))
9.77/2.85	  , a__from(X) -> from(X) }
9.77/2.85	Obligation:
9.77/2.85	  innermost runtime complexity
9.77/2.85	Answer:
9.77/2.85	  YES(O(1),O(n^1))
9.77/2.85	
9.77/2.85	We use the processor 'matrix interpretation of dimension 1' to
9.77/2.85	orient following rules strictly.
9.77/2.85	
9.77/2.85	Trs: { mark(if(X1, X2, X3)) -> a__if(mark(X1), X2, X3) }
9.77/2.85	
9.77/2.85	The induced complexity on above rules (modulo remaining rules) is
9.77/2.85	YES(?,O(n^1)) . These rules are moved into the corresponding weak
9.77/2.85	component(s).
9.77/2.85	
9.77/2.85	Sub-proof:
9.77/2.85	----------
9.77/2.85	  The following argument positions are usable:
9.77/2.85	    Uargs(a__and) = {1}, Uargs(a__if) = {1}, Uargs(a__add) = {1},
9.77/2.85	    Uargs(a__first) = {1, 2}
9.77/2.85	  
9.77/2.85	  TcT has computed the following constructor-based matrix
9.77/2.85	  interpretation satisfying not(EDA).
9.77/2.85	  
9.77/2.85	       [a__and](x1, x2) = [1] x1 + [4] x2 + [0]         
9.77/2.85	                                                        
9.77/2.85	                 [true] = [0]                           
9.77/2.85	                                                        
9.77/2.85	             [mark](x1) = [4] x1 + [0]                  
9.77/2.85	                                                        
9.77/2.85	                [false] = [0]                           
9.77/2.85	                                                        
9.77/2.85	    [a__if](x1, x2, x3) = [1] x1 + [4] x2 + [4] x3 + [1]
9.77/2.85	                                                        
9.77/2.85	       [a__add](x1, x2) = [1] x1 + [4] x2 + [0]         
9.77/2.85	                                                        
9.77/2.85	                    [0] = [2]                           
9.77/2.85	                                                        
9.77/2.85	                [s](x1) = [0]                           
9.77/2.85	                                                        
9.77/2.85	          [add](x1, x2) = [1] x1 + [1] x2 + [0]         
9.77/2.85	                                                        
9.77/2.85	     [a__first](x1, x2) = [1] x1 + [1] x2 + [0]         
9.77/2.85	                                                        
9.77/2.85	                  [nil] = [0]                           
9.77/2.85	                                                        
9.77/2.85	         [cons](x1, x2) = [0]                           
9.77/2.85	                                                        
9.77/2.85	        [first](x1, x2) = [1] x1 + [1] x2 + [0]         
9.77/2.85	                                                        
9.77/2.85	          [a__from](x1) = [0]                           
9.77/2.85	                                                        
9.77/2.85	             [from](x1) = [0]                           
9.77/2.85	                                                        
9.77/2.85	          [and](x1, x2) = [1] x1 + [1] x2 + [0]         
9.77/2.85	                                                        
9.77/2.85	       [if](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [1]
9.77/2.85	  
9.77/2.85	  The order satisfies the following ordering constraints:
9.77/2.85	  
9.77/2.85	                [a__and(X1, X2)] =  [1] X1 + [4] X2 + [0]         
9.77/2.85	                                 >= [1] X1 + [1] X2 + [0]         
9.77/2.85	                                 =  [and(X1, X2)]                 
9.77/2.85	                                                                  
9.77/2.85	             [a__and(true(), X)] =  [4] X + [0]                   
9.77/2.85	                                 >= [4] X + [0]                   
9.77/2.85	                                 =  [mark(X)]                     
9.77/2.85	                                                                  
9.77/2.85	            [a__and(false(), Y)] =  [4] Y + [0]                   
9.77/2.85	                                 >= [0]                           
9.77/2.85	                                 =  [false()]                     
9.77/2.85	                                                                  
9.77/2.85	                  [mark(true())] =  [0]                           
9.77/2.85	                                 >= [0]                           
9.77/2.85	                                 =  [true()]                      
9.77/2.85	                                                                  
9.77/2.85	                 [mark(false())] =  [0]                           
9.77/2.85	                                 >= [0]                           
9.77/2.85	                                 =  [false()]                     
9.77/2.85	                                                                  
9.77/2.85	                     [mark(0())] =  [8]                           
9.77/2.85	                                 >  [2]                           
9.77/2.85	                                 =  [0()]                         
9.77/2.85	                                                                  
9.77/2.85	                    [mark(s(X))] =  [0]                           
9.77/2.85	                                 >= [0]                           
9.77/2.85	                                 =  [s(X)]                        
9.77/2.85	                                                                  
9.77/2.85	             [mark(add(X1, X2))] =  [4] X1 + [4] X2 + [0]         
9.77/2.85	                                 >= [4] X1 + [4] X2 + [0]         
9.77/2.85	                                 =  [a__add(mark(X1), X2)]        
9.77/2.85	                                                                  
9.77/2.85	                   [mark(nil())] =  [0]                           
9.77/2.85	                                 >= [0]                           
9.77/2.85	                                 =  [nil()]                       
9.77/2.85	                                                                  
9.77/2.85	            [mark(cons(X1, X2))] =  [0]                           
9.77/2.85	                                 >= [0]                           
9.77/2.85	                                 =  [cons(X1, X2)]                
9.77/2.85	                                                                  
9.77/2.85	           [mark(first(X1, X2))] =  [4] X1 + [4] X2 + [0]         
9.77/2.85	                                 >= [4] X1 + [4] X2 + [0]         
9.77/2.85	                                 =  [a__first(mark(X1), mark(X2))]
9.77/2.85	                                                                  
9.77/2.85	                 [mark(from(X))] =  [0]                           
9.77/2.85	                                 >= [0]                           
9.77/2.85	                                 =  [a__from(X)]                  
9.77/2.85	                                                                  
9.77/2.85	             [mark(and(X1, X2))] =  [4] X1 + [4] X2 + [0]         
9.77/2.85	                                 >= [4] X1 + [4] X2 + [0]         
9.77/2.85	                                 =  [a__and(mark(X1), X2)]        
9.77/2.85	                                                                  
9.77/2.85	          [mark(if(X1, X2, X3))] =  [4] X1 + [4] X2 + [4] X3 + [4]
9.77/2.85	                                 >  [4] X1 + [4] X2 + [4] X3 + [1]
9.77/2.85	                                 =  [a__if(mark(X1), X2, X3)]     
9.77/2.85	                                                                  
9.77/2.85	             [a__if(X1, X2, X3)] =  [1] X1 + [4] X2 + [4] X3 + [1]
9.77/2.85	                                 >= [1] X1 + [1] X2 + [1] X3 + [1]
9.77/2.85	                                 =  [if(X1, X2, X3)]              
9.77/2.85	                                                                  
9.77/2.85	           [a__if(true(), X, Y)] =  [4] X + [4] Y + [1]           
9.77/2.85	                                 >  [4] X + [0]                   
9.77/2.85	                                 =  [mark(X)]                     
9.77/2.85	                                                                  
9.77/2.85	          [a__if(false(), X, Y)] =  [4] X + [4] Y + [1]           
9.77/2.85	                                 >  [4] Y + [0]                   
9.77/2.85	                                 =  [mark(Y)]                     
9.77/2.85	                                                                  
9.77/2.85	                [a__add(X1, X2)] =  [1] X1 + [4] X2 + [0]         
9.77/2.85	                                 >= [1] X1 + [1] X2 + [0]         
9.77/2.85	                                 =  [add(X1, X2)]                 
9.77/2.85	                                                                  
9.77/2.85	                [a__add(0(), X)] =  [4] X + [2]                   
9.77/2.85	                                 >  [4] X + [0]                   
9.77/2.85	                                 =  [mark(X)]                     
9.77/2.85	                                                                  
9.77/2.85	               [a__add(s(X), Y)] =  [4] Y + [0]                   
9.77/2.85	                                 >= [0]                           
9.77/2.85	                                 =  [s(add(X, Y))]                
9.77/2.85	                                                                  
9.77/2.85	              [a__first(X1, X2)] =  [1] X1 + [1] X2 + [0]         
9.77/2.85	                                 >= [1] X1 + [1] X2 + [0]         
9.77/2.85	                                 =  [first(X1, X2)]               
9.77/2.85	                                                                  
9.77/2.85	              [a__first(0(), X)] =  [1] X + [2]                   
9.77/2.85	                                 >  [0]                           
9.77/2.85	                                 =  [nil()]                       
9.77/2.85	                                                                  
9.77/2.85	    [a__first(s(X), cons(Y, Z))] =  [0]                           
9.77/2.85	                                 >= [0]                           
9.77/2.85	                                 =  [cons(Y, first(X, Z))]        
9.77/2.85	                                                                  
9.77/2.85	                    [a__from(X)] =  [0]                           
9.77/2.85	                                 >= [0]                           
9.77/2.85	                                 =  [cons(X, from(s(X)))]         
9.77/2.85	                                                                  
9.77/2.85	                    [a__from(X)] =  [0]                           
9.77/2.85	                                 >= [0]                           
9.77/2.85	                                 =  [from(X)]                     
9.77/2.85	                                                                  
9.77/2.85	
9.77/2.85	We return to the main proof.
9.77/2.85	
9.77/2.85	We are left with following problem, upon which TcT provides the
9.77/2.85	certificate YES(O(1),O(n^1)).
9.77/2.85	
9.77/2.85	Strict Trs: { mark(and(X1, X2)) -> a__and(mark(X1), X2) }
9.77/2.85	Weak Trs:
9.77/2.85	  { a__and(X1, X2) -> and(X1, X2)
9.77/2.85	  , a__and(true(), X) -> mark(X)
9.77/2.85	  , a__and(false(), Y) -> false()
9.77/2.85	  , mark(true()) -> true()
9.77/2.85	  , mark(false()) -> false()
9.77/2.85	  , mark(0()) -> 0()
9.77/2.85	  , mark(s(X)) -> s(X)
9.77/2.85	  , mark(add(X1, X2)) -> a__add(mark(X1), X2)
9.77/2.85	  , mark(nil()) -> nil()
9.77/2.85	  , mark(cons(X1, X2)) -> cons(X1, X2)
9.77/2.85	  , mark(first(X1, X2)) -> a__first(mark(X1), mark(X2))
9.77/2.85	  , mark(from(X)) -> a__from(X)
9.77/2.85	  , mark(if(X1, X2, X3)) -> a__if(mark(X1), X2, X3)
9.77/2.85	  , a__if(X1, X2, X3) -> if(X1, X2, X3)
9.77/2.85	  , a__if(true(), X, Y) -> mark(X)
9.77/2.85	  , a__if(false(), X, Y) -> mark(Y)
9.77/2.85	  , a__add(X1, X2) -> add(X1, X2)
9.77/2.85	  , a__add(0(), X) -> mark(X)
9.77/2.85	  , a__add(s(X), Y) -> s(add(X, Y))
9.77/2.85	  , a__first(X1, X2) -> first(X1, X2)
9.77/2.85	  , a__first(0(), X) -> nil()
9.77/2.85	  , a__first(s(X), cons(Y, Z)) -> cons(Y, first(X, Z))
9.77/2.85	  , a__from(X) -> cons(X, from(s(X)))
9.77/2.85	  , a__from(X) -> from(X) }
9.77/2.85	Obligation:
9.77/2.85	  innermost runtime complexity
9.77/2.85	Answer:
9.77/2.85	  YES(O(1),O(n^1))
9.77/2.85	
9.77/2.85	We use the processor 'matrix interpretation of dimension 1' to
9.77/2.85	orient following rules strictly.
9.77/2.85	
9.77/2.85	Trs: { mark(and(X1, X2)) -> a__and(mark(X1), X2) }
9.77/2.85	
9.77/2.85	The induced complexity on above rules (modulo remaining rules) is
9.77/2.85	YES(?,O(n^1)) . These rules are moved into the corresponding weak
9.77/2.85	component(s).
9.77/2.85	
9.77/2.85	Sub-proof:
9.77/2.85	----------
9.77/2.85	  The following argument positions are usable:
9.77/2.85	    Uargs(a__and) = {1}, Uargs(a__if) = {1}, Uargs(a__add) = {1},
9.77/2.85	    Uargs(a__first) = {1, 2}
9.77/2.85	  
9.77/2.85	  TcT has computed the following constructor-based matrix
9.77/2.85	  interpretation satisfying not(EDA).
9.77/2.85	  
9.77/2.85	       [a__and](x1, x2) = [1] x1 + [2] x2 + [4]         
9.77/2.85	                                                        
9.77/2.85	                 [true] = [4]                           
9.77/2.85	                                                        
9.77/2.85	             [mark](x1) = [2] x1 + [0]                  
9.77/2.85	                                                        
9.77/2.85	                [false] = [4]                           
9.77/2.85	                                                        
9.77/2.85	    [a__if](x1, x2, x3) = [1] x1 + [2] x2 + [2] x3 + [0]
9.77/2.85	                                                        
9.77/2.85	       [a__add](x1, x2) = [1] x1 + [2] x2 + [4]         
9.77/2.85	                                                        
9.77/2.85	                    [0] = [4]                           
9.77/2.85	                                                        
9.77/2.85	                [s](x1) = [4]                           
9.77/2.85	                                                        
9.77/2.85	          [add](x1, x2) = [1] x1 + [1] x2 + [4]         
9.77/2.85	                                                        
9.77/2.85	     [a__first](x1, x2) = [1] x1 + [1] x2 + [0]         
9.77/2.85	                                                        
9.77/2.85	                  [nil] = [4]                           
9.77/2.85	                                                        
9.77/2.85	         [cons](x1, x2) = [4]                           
9.77/2.85	                                                        
9.77/2.85	        [first](x1, x2) = [1] x1 + [1] x2 + [0]         
9.77/2.85	                                                        
9.77/2.85	          [a__from](x1) = [4]                           
9.77/2.85	                                                        
9.77/2.85	             [from](x1) = [4]                           
9.77/2.85	                                                        
9.77/2.85	          [and](x1, x2) = [1] x1 + [1] x2 + [4]         
9.77/2.85	                                                        
9.77/2.85	       [if](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0]
9.77/2.85	  
9.77/2.85	  The order satisfies the following ordering constraints:
9.77/2.85	  
9.77/2.85	                [a__and(X1, X2)] =  [1] X1 + [2] X2 + [4]         
9.77/2.85	                                 >= [1] X1 + [1] X2 + [4]         
9.77/2.85	                                 =  [and(X1, X2)]                 
9.77/2.85	                                                                  
9.77/2.85	             [a__and(true(), X)] =  [2] X + [8]                   
9.77/2.85	                                 >  [2] X + [0]                   
9.77/2.85	                                 =  [mark(X)]                     
9.77/2.85	                                                                  
9.77/2.85	            [a__and(false(), Y)] =  [2] Y + [8]                   
9.77/2.85	                                 >  [4]                           
9.77/2.85	                                 =  [false()]                     
9.77/2.85	                                                                  
9.77/2.85	                  [mark(true())] =  [8]                           
9.77/2.85	                                 >  [4]                           
9.77/2.85	                                 =  [true()]                      
9.77/2.85	                                                                  
9.77/2.85	                 [mark(false())] =  [8]                           
9.77/2.85	                                 >  [4]                           
9.77/2.85	                                 =  [false()]                     
9.77/2.85	                                                                  
9.77/2.85	                     [mark(0())] =  [8]                           
9.77/2.85	                                 >  [4]                           
9.77/2.85	                                 =  [0()]                         
9.77/2.85	                                                                  
9.77/2.85	                    [mark(s(X))] =  [8]                           
9.77/2.85	                                 >  [4]                           
9.77/2.85	                                 =  [s(X)]                        
9.77/2.85	                                                                  
9.77/2.85	             [mark(add(X1, X2))] =  [2] X1 + [2] X2 + [8]         
9.77/2.85	                                 >  [2] X1 + [2] X2 + [4]         
9.77/2.85	                                 =  [a__add(mark(X1), X2)]        
9.77/2.85	                                                                  
9.77/2.85	                   [mark(nil())] =  [8]                           
9.77/2.85	                                 >  [4]                           
9.77/2.85	                                 =  [nil()]                       
9.77/2.85	                                                                  
9.77/2.85	            [mark(cons(X1, X2))] =  [8]                           
9.77/2.85	                                 >  [4]                           
9.77/2.85	                                 =  [cons(X1, X2)]                
9.77/2.85	                                                                  
9.77/2.85	           [mark(first(X1, X2))] =  [2] X1 + [2] X2 + [0]         
9.77/2.85	                                 >= [2] X1 + [2] X2 + [0]         
9.77/2.85	                                 =  [a__first(mark(X1), mark(X2))]
9.77/2.85	                                                                  
9.77/2.85	                 [mark(from(X))] =  [8]                           
9.77/2.85	                                 >  [4]                           
9.77/2.85	                                 =  [a__from(X)]                  
9.77/2.85	                                                                  
9.77/2.85	             [mark(and(X1, X2))] =  [2] X1 + [2] X2 + [8]         
9.77/2.85	                                 >  [2] X1 + [2] X2 + [4]         
9.77/2.85	                                 =  [a__and(mark(X1), X2)]        
9.77/2.85	                                                                  
9.77/2.85	          [mark(if(X1, X2, X3))] =  [2] X1 + [2] X2 + [2] X3 + [0]
9.77/2.85	                                 >= [2] X1 + [2] X2 + [2] X3 + [0]
9.77/2.85	                                 =  [a__if(mark(X1), X2, X3)]     
9.77/2.85	                                                                  
9.77/2.85	             [a__if(X1, X2, X3)] =  [1] X1 + [2] X2 + [2] X3 + [0]
9.77/2.85	                                 >= [1] X1 + [1] X2 + [1] X3 + [0]
9.77/2.85	                                 =  [if(X1, X2, X3)]              
9.77/2.85	                                                                  
9.77/2.85	           [a__if(true(), X, Y)] =  [2] X + [2] Y + [4]           
9.77/2.85	                                 >  [2] X + [0]                   
9.77/2.85	                                 =  [mark(X)]                     
9.77/2.85	                                                                  
9.77/2.85	          [a__if(false(), X, Y)] =  [2] X + [2] Y + [4]           
9.77/2.85	                                 >  [2] Y + [0]                   
9.77/2.85	                                 =  [mark(Y)]                     
9.77/2.85	                                                                  
9.77/2.85	                [a__add(X1, X2)] =  [1] X1 + [2] X2 + [4]         
9.77/2.85	                                 >= [1] X1 + [1] X2 + [4]         
9.77/2.85	                                 =  [add(X1, X2)]                 
9.77/2.85	                                                                  
9.77/2.85	                [a__add(0(), X)] =  [2] X + [8]                   
9.77/2.85	                                 >  [2] X + [0]                   
9.77/2.85	                                 =  [mark(X)]                     
9.77/2.85	                                                                  
9.77/2.85	               [a__add(s(X), Y)] =  [2] Y + [8]                   
9.77/2.85	                                 >  [4]                           
9.77/2.85	                                 =  [s(add(X, Y))]                
9.77/2.85	                                                                  
9.77/2.85	              [a__first(X1, X2)] =  [1] X1 + [1] X2 + [0]         
9.77/2.85	                                 >= [1] X1 + [1] X2 + [0]         
9.77/2.85	                                 =  [first(X1, X2)]               
9.77/2.85	                                                                  
9.77/2.85	              [a__first(0(), X)] =  [1] X + [4]                   
9.77/2.85	                                 >= [4]                           
9.77/2.85	                                 =  [nil()]                       
9.77/2.85	                                                                  
9.77/2.85	    [a__first(s(X), cons(Y, Z))] =  [8]                           
9.77/2.85	                                 >  [4]                           
9.77/2.85	                                 =  [cons(Y, first(X, Z))]        
9.77/2.85	                                                                  
9.77/2.85	                    [a__from(X)] =  [4]                           
9.77/2.85	                                 >= [4]                           
9.77/2.85	                                 =  [cons(X, from(s(X)))]         
9.77/2.85	                                                                  
9.77/2.85	                    [a__from(X)] =  [4]                           
9.77/2.85	                                 >= [4]                           
9.77/2.85	                                 =  [from(X)]                     
9.77/2.85	                                                                  
9.77/2.85	
9.77/2.85	We return to the main proof.
9.77/2.85	
9.77/2.85	We are left with following problem, upon which TcT provides the
9.77/2.85	certificate YES(O(1),O(1)).
9.77/2.85	
9.77/2.85	Weak Trs:
9.77/2.85	  { a__and(X1, X2) -> and(X1, X2)
9.77/2.85	  , a__and(true(), X) -> mark(X)
9.77/2.85	  , a__and(false(), Y) -> false()
9.77/2.85	  , mark(true()) -> true()
9.77/2.85	  , mark(false()) -> false()
9.77/2.85	  , mark(0()) -> 0()
9.77/2.85	  , mark(s(X)) -> s(X)
9.77/2.85	  , mark(add(X1, X2)) -> a__add(mark(X1), X2)
9.77/2.85	  , mark(nil()) -> nil()
9.77/2.85	  , mark(cons(X1, X2)) -> cons(X1, X2)
9.77/2.85	  , mark(first(X1, X2)) -> a__first(mark(X1), mark(X2))
9.77/2.85	  , mark(from(X)) -> a__from(X)
9.77/2.85	  , mark(and(X1, X2)) -> a__and(mark(X1), X2)
9.77/2.85	  , mark(if(X1, X2, X3)) -> a__if(mark(X1), X2, X3)
9.77/2.85	  , a__if(X1, X2, X3) -> if(X1, X2, X3)
9.77/2.85	  , a__if(true(), X, Y) -> mark(X)
9.77/2.85	  , a__if(false(), X, Y) -> mark(Y)
9.77/2.85	  , a__add(X1, X2) -> add(X1, X2)
9.77/2.85	  , a__add(0(), X) -> mark(X)
9.77/2.85	  , a__add(s(X), Y) -> s(add(X, Y))
9.77/2.85	  , a__first(X1, X2) -> first(X1, X2)
9.77/2.85	  , a__first(0(), X) -> nil()
9.77/2.85	  , a__first(s(X), cons(Y, Z)) -> cons(Y, first(X, Z))
9.77/2.85	  , a__from(X) -> cons(X, from(s(X)))
9.77/2.85	  , a__from(X) -> from(X) }
9.77/2.85	Obligation:
9.77/2.85	  innermost runtime complexity
9.77/2.85	Answer:
9.77/2.85	  YES(O(1),O(1))
9.77/2.85	
9.77/2.85	Empty rules are trivially bounded
9.77/2.85	
9.77/2.85	Hurray, we answered YES(O(1),O(n^1))
9.77/2.86	EOF