YES(O(1),O(n^1))
83.60/48.03	YES(O(1),O(n^1))
83.60/48.03	
83.60/48.03	We are left with following problem, upon which TcT provides the
83.60/48.03	certificate YES(O(1),O(n^1)).
83.60/48.03	
83.60/48.03	Strict Trs:
83.60/48.03	  { f(X, X) -> c(X)
83.60/48.03	  , f(X, c(X)) -> f(s(X), X)
83.60/48.03	  , f(s(X), X) -> f(X, a(X)) }
83.60/48.03	Obligation:
83.60/48.03	  runtime complexity
83.60/48.03	Answer:
83.60/48.03	  YES(O(1),O(n^1))
83.60/48.03	
83.60/48.03	The weightgap principle applies (using the following nonconstant
83.60/48.03	growth matrix-interpretation)
83.60/48.03	
83.60/48.03	The following argument positions are usable:
83.60/48.03	  none
83.60/48.03	
83.60/48.03	TcT has computed the following matrix interpretation satisfying
83.60/48.03	not(EDA) and not(IDA(1)).
83.60/48.03	
83.60/48.03	  [f](x1, x2) = [1] x1 + [1] x2 + [7]
83.60/48.03	                                     
83.60/48.03	      [s](x1) = [7]                  
83.60/48.03	                                     
83.60/48.03	      [a](x1) = [3]                  
83.60/48.03	                                     
83.60/48.03	      [c](x1) = [7]                  
83.60/48.03	
83.60/48.03	The order satisfies the following ordering constraints:
83.60/48.03	
83.60/48.03	     [f(X, X)] =  [2] X + [7] 
83.60/48.03	               >= [7]         
83.60/48.03	               =  [c(X)]      
83.60/48.03	                              
83.60/48.03	  [f(X, c(X))] =  [1] X + [14]
83.60/48.03	               >= [1] X + [14]
83.60/48.03	               =  [f(s(X), X)]
83.60/48.03	                              
83.60/48.03	  [f(s(X), X)] =  [1] X + [14]
83.60/48.03	               >  [1] X + [10]
83.60/48.03	               =  [f(X, a(X))]
83.60/48.03	                              
83.60/48.03	
83.60/48.03	Further, it can be verified that all rules not oriented are covered by the weightgap condition.
83.60/48.03	
83.60/48.03	We are left with following problem, upon which TcT provides the
83.60/48.03	certificate YES(O(1),O(n^1)).
83.60/48.03	
83.60/48.03	Strict Trs:
83.60/48.03	  { f(X, X) -> c(X)
83.60/48.03	  , f(X, c(X)) -> f(s(X), X) }
83.60/48.03	Weak Trs: { f(s(X), X) -> f(X, a(X)) }
83.60/48.03	Obligation:
83.60/48.03	  runtime complexity
83.60/48.03	Answer:
83.60/48.03	  YES(O(1),O(n^1))
83.60/48.03	
83.60/48.03	The weightgap principle applies (using the following nonconstant
83.60/48.03	growth matrix-interpretation)
83.60/48.03	
83.60/48.03	The following argument positions are usable:
83.60/48.03	  none
83.60/48.03	
83.60/48.03	TcT has computed the following matrix interpretation satisfying
83.60/48.03	not(EDA) and not(IDA(1)).
83.60/48.03	
83.60/48.03	  [f](x1, x2) = [1] x1 + [1] x2 + [7]
83.60/48.03	                                     
83.60/48.03	      [s](x1) = [4]                  
83.60/48.03	                                     
83.60/48.03	      [a](x1) = [3]                  
83.60/48.03	                                     
83.60/48.03	      [c](x1) = [7]                  
83.60/48.03	
83.60/48.03	The order satisfies the following ordering constraints:
83.60/48.03	
83.60/48.03	     [f(X, X)] =  [2] X + [7] 
83.60/48.03	               >= [7]         
83.60/48.03	               =  [c(X)]      
83.60/48.03	                              
83.60/48.03	  [f(X, c(X))] =  [1] X + [14]
83.60/48.03	               >  [1] X + [11]
83.60/48.03	               =  [f(s(X), X)]
83.60/48.03	                              
83.60/48.03	  [f(s(X), X)] =  [1] X + [11]
83.60/48.03	               >  [1] X + [10]
83.60/48.03	               =  [f(X, a(X))]
83.60/48.03	                              
83.60/48.03	
83.60/48.03	Further, it can be verified that all rules not oriented are covered by the weightgap condition.
83.60/48.03	
83.60/48.03	We are left with following problem, upon which TcT provides the
83.60/48.03	certificate YES(O(1),O(n^1)).
83.60/48.03	
83.60/48.03	Strict Trs: { f(X, X) -> c(X) }
83.60/48.03	Weak Trs:
83.60/48.03	  { f(X, c(X)) -> f(s(X), X)
83.60/48.03	  , f(s(X), X) -> f(X, a(X)) }
83.60/48.03	Obligation:
83.60/48.03	  runtime complexity
83.60/48.03	Answer:
83.60/48.03	  YES(O(1),O(n^1))
83.60/48.03	
83.60/48.03	The weightgap principle applies (using the following nonconstant
83.60/48.03	growth matrix-interpretation)
83.60/48.03	
83.60/48.03	The following argument positions are usable:
83.60/48.03	  none
83.60/48.03	
83.60/48.03	TcT has computed the following matrix interpretation satisfying
83.60/48.03	not(EDA) and not(IDA(1)).
83.60/48.03	
83.60/48.03	  [f](x1, x2) = [1] x1 + [1] x2 + [7]
83.60/48.03	                                     
83.60/48.03	      [s](x1) = [3]                  
83.60/48.03	                                     
83.60/48.03	      [a](x1) = [3]                  
83.60/48.03	                                     
83.60/48.03	      [c](x1) = [3]                  
83.60/48.03	
83.60/48.03	The order satisfies the following ordering constraints:
83.60/48.03	
83.60/48.03	     [f(X, X)] =  [2] X + [7] 
83.60/48.03	               >  [3]         
83.60/48.03	               =  [c(X)]      
83.60/48.03	                              
83.60/48.03	  [f(X, c(X))] =  [1] X + [10]
83.60/48.03	               >= [1] X + [10]
83.60/48.03	               =  [f(s(X), X)]
83.60/48.03	                              
83.60/48.03	  [f(s(X), X)] =  [1] X + [10]
83.60/48.03	               >= [1] X + [10]
83.60/48.03	               =  [f(X, a(X))]
83.60/48.03	                              
83.60/48.03	
83.60/48.03	Further, it can be verified that all rules not oriented are covered by the weightgap condition.
83.60/48.03	
83.60/48.03	We are left with following problem, upon which TcT provides the
83.60/48.03	certificate YES(O(1),O(1)).
83.60/48.03	
83.60/48.03	Weak Trs:
83.60/48.03	  { f(X, X) -> c(X)
83.60/48.03	  , f(X, c(X)) -> f(s(X), X)
83.60/48.03	  , f(s(X), X) -> f(X, a(X)) }
83.60/48.03	Obligation:
83.60/48.03	  runtime complexity
83.60/48.03	Answer:
83.60/48.03	  YES(O(1),O(1))
83.60/48.03	
83.60/48.03	Empty rules are trivially bounded
83.60/48.03	
83.60/48.03	Hurray, we answered YES(O(1),O(n^1))
83.71/48.18	EOF