YES(O(1),O(n^1))
0.00/0.54	YES(O(1),O(n^1))
0.00/0.54	
0.00/0.54	We are left with following problem, upon which TcT provides the
0.00/0.54	certificate YES(O(1),O(n^1)).
0.00/0.54	
0.00/0.54	Strict Trs:
0.00/0.54	  { ackin(s(X), s(Y)) -> u21(ackin(s(X), Y), X)
0.00/0.54	  , u21(ackout(X), Y) -> u22(ackin(Y, X)) }
0.00/0.54	Obligation:
0.00/0.54	  innermost runtime complexity
0.00/0.54	Answer:
0.00/0.54	  YES(O(1),O(n^1))
0.00/0.54	
0.00/0.54	The weightgap principle applies (using the following nonconstant
0.00/0.54	growth matrix-interpretation)
0.00/0.54	
0.00/0.54	The following argument positions are usable:
0.00/0.54	  Uargs(u21) = {1}, Uargs(u22) = {1}
0.00/0.54	
0.00/0.54	TcT has computed the following matrix interpretation satisfying
0.00/0.54	not(EDA) and not(IDA(1)).
0.00/0.54	
0.00/0.54	  [ackin](x1, x2) = [1] x2 + [7]
0.00/0.54	                                
0.00/0.54	          [s](x1) = [1] x1 + [7]
0.00/0.54	                                
0.00/0.54	    [u21](x1, x2) = [1] x1 + [7]
0.00/0.54	                                
0.00/0.54	     [ackout](x1) = [1] x1 + [7]
0.00/0.54	                                
0.00/0.54	        [u22](x1) = [1] x1 + [3]
0.00/0.54	
0.00/0.54	The order satisfies the following ordering constraints:
0.00/0.54	
0.00/0.54	  [ackin(s(X), s(Y))] =  [1] Y + [14]            
0.00/0.54	                      >= [1] Y + [14]            
0.00/0.54	                      =  [u21(ackin(s(X), Y), X)]
0.00/0.54	                                                 
0.00/0.54	  [u21(ackout(X), Y)] =  [1] X + [14]            
0.00/0.54	                      >  [1] X + [10]            
0.00/0.54	                      =  [u22(ackin(Y, X))]      
0.00/0.54	                                                 
0.00/0.54	
0.00/0.54	Further, it can be verified that all rules not oriented are covered by the weightgap condition.
0.00/0.54	
0.00/0.54	We are left with following problem, upon which TcT provides the
0.00/0.54	certificate YES(O(1),O(n^1)).
0.00/0.54	
0.00/0.54	Strict Trs: { ackin(s(X), s(Y)) -> u21(ackin(s(X), Y), X) }
0.00/0.54	Weak Trs: { u21(ackout(X), Y) -> u22(ackin(Y, X)) }
0.00/0.54	Obligation:
0.00/0.54	  innermost runtime complexity
0.00/0.54	Answer:
0.00/0.54	  YES(O(1),O(n^1))
0.00/0.54	
0.00/0.54	The weightgap principle applies (using the following nonconstant
0.00/0.54	growth matrix-interpretation)
0.00/0.54	
0.00/0.54	The following argument positions are usable:
0.00/0.54	  Uargs(u21) = {1}, Uargs(u22) = {1}
0.00/0.54	
0.00/0.54	TcT has computed the following matrix interpretation satisfying
0.00/0.54	not(EDA) and not(IDA(1)).
0.00/0.54	
0.00/0.54	  [ackin](x1, x2) = [1] x2 + [7]
0.00/0.54	                                
0.00/0.54	          [s](x1) = [1] x1 + [7]
0.00/0.54	                                
0.00/0.54	    [u21](x1, x2) = [1] x1 + [6]
0.00/0.54	                                
0.00/0.54	     [ackout](x1) = [1] x1 + [7]
0.00/0.54	                                
0.00/0.54	        [u22](x1) = [1] x1 + [3]
0.00/0.54	
0.00/0.54	The order satisfies the following ordering constraints:
0.00/0.54	
0.00/0.54	  [ackin(s(X), s(Y))] = [1] Y + [14]            
0.00/0.54	                      > [1] Y + [13]            
0.00/0.54	                      = [u21(ackin(s(X), Y), X)]
0.00/0.54	                                                
0.00/0.54	  [u21(ackout(X), Y)] = [1] X + [13]            
0.00/0.54	                      > [1] X + [10]            
0.00/0.54	                      = [u22(ackin(Y, X))]      
0.00/0.54	                                                
0.00/0.54	
0.00/0.54	Further, it can be verified that all rules not oriented are covered by the weightgap condition.
0.00/0.54	
0.00/0.54	We are left with following problem, upon which TcT provides the
0.00/0.54	certificate YES(O(1),O(1)).
0.00/0.54	
0.00/0.54	Weak Trs:
0.00/0.54	  { ackin(s(X), s(Y)) -> u21(ackin(s(X), Y), X)
0.00/0.54	  , u21(ackout(X), Y) -> u22(ackin(Y, X)) }
0.00/0.54	Obligation:
0.00/0.54	  innermost runtime complexity
0.00/0.54	Answer:
0.00/0.54	  YES(O(1),O(1))
0.00/0.54	
0.00/0.54	Empty rules are trivially bounded
0.00/0.54	
0.00/0.54	Hurray, we answered YES(O(1),O(n^1))
0.00/0.55	EOF