YES(O(1),O(n^1))
0.00/0.64	YES(O(1),O(n^1))
0.00/0.64	
0.00/0.64	We are left with following problem, upon which TcT provides the
0.00/0.64	certificate YES(O(1),O(n^1)).
0.00/0.64	
0.00/0.64	Strict Trs:
0.00/0.64	  { plus(plus(X, Y), Z) -> plus(X, plus(Y, Z))
0.00/0.64	  , times(X, s(Y)) -> plus(X, times(Y, X)) }
0.00/0.64	Obligation:
0.00/0.64	  innermost runtime complexity
0.00/0.64	Answer:
0.00/0.64	  YES(O(1),O(n^1))
0.00/0.64	
0.00/0.64	The weightgap principle applies (using the following nonconstant
0.00/0.64	growth matrix-interpretation)
0.00/0.64	
0.00/0.64	The following argument positions are usable:
0.00/0.64	  Uargs(plus) = {2}
0.00/0.64	
0.00/0.64	TcT has computed the following matrix interpretation satisfying
0.00/0.64	not(EDA) and not(IDA(1)).
0.00/0.64	
0.00/0.64	   [plus](x1, x2) = [1] x2 + [5]         
0.00/0.64	                                         
0.00/0.64	  [times](x1, x2) = [1] x1 + [1] x2 + [7]
0.00/0.64	                                         
0.00/0.64	          [s](x1) = [1] x1 + [7]         
0.00/0.64	
0.00/0.64	The order satisfies the following ordering constraints:
0.00/0.64	
0.00/0.64	  [plus(plus(X, Y), Z)] = [1] Z + [5]           
0.00/0.64	                        ? [1] Z + [10]          
0.00/0.64	                        = [plus(X, plus(Y, Z))] 
0.00/0.64	                                                
0.00/0.64	       [times(X, s(Y))] = [1] X + [1] Y + [14]  
0.00/0.64	                        > [1] X + [1] Y + [12]  
0.00/0.64	                        = [plus(X, times(Y, X))]
0.00/0.64	                                                
0.00/0.64	
0.00/0.64	Further, it can be verified that all rules not oriented are covered by the weightgap condition.
0.00/0.64	
0.00/0.64	We are left with following problem, upon which TcT provides the
0.00/0.64	certificate YES(O(1),O(n^1)).
0.00/0.64	
0.00/0.64	Strict Trs: { plus(plus(X, Y), Z) -> plus(X, plus(Y, Z)) }
0.00/0.64	Weak Trs: { times(X, s(Y)) -> plus(X, times(Y, X)) }
0.00/0.64	Obligation:
0.00/0.64	  innermost runtime complexity
0.00/0.64	Answer:
0.00/0.64	  YES(O(1),O(n^1))
0.00/0.64	
0.00/0.64	We use the processor 'matrix interpretation of dimension 2' to
0.00/0.64	orient following rules strictly.
0.00/0.64	
0.00/0.64	Trs: { plus(plus(X, Y), Z) -> plus(X, plus(Y, Z)) }
0.00/0.64	
0.00/0.64	The induced complexity on above rules (modulo remaining rules) is
0.00/0.64	YES(?,O(n^1)) . These rules are moved into the corresponding weak
0.00/0.64	component(s).
0.00/0.64	
0.00/0.64	Sub-proof:
0.00/0.64	----------
0.00/0.64	  The following argument positions are usable:
0.00/0.64	    Uargs(plus) = {2}
0.00/0.64	  
0.00/0.64	  TcT has computed the following constructor-based matrix
0.00/0.64	  interpretation satisfying not(EDA) and not(IDA(1)).
0.00/0.64	  
0.00/0.64	     [plus](x1, x2) = [0 1] x1 + [1 0] x2 + [0]
0.00/0.64	                      [0 1]      [0 1]      [4]
0.00/0.64	                                               
0.00/0.64	    [times](x1, x2) = [1 1] x1 + [1 0] x2 + [1]
0.00/0.64	                      [1 1]      [1 0]      [1]
0.00/0.64	                                               
0.00/0.64	            [s](x1) = [1 1] x1 + [7]           
0.00/0.64	                      [0 0]      [0]           
0.00/0.64	  
0.00/0.64	  The order satisfies the following ordering constraints:
0.00/0.64	  
0.00/0.64	    [plus(plus(X, Y), Z)] = [0 1] X + [0 1] Y + [1 0] Z + [4]
0.00/0.64	                            [0 1]     [0 1]     [0 1]     [8]
0.00/0.64	                          > [0 1] X + [0 1] Y + [1 0] Z + [0]
0.00/0.64	                            [0 1]     [0 1]     [0 1]     [8]
0.00/0.64	                          = [plus(X, plus(Y, Z))]            
0.00/0.64	                                                             
0.00/0.64	         [times(X, s(Y))] = [1 1] X + [1 1] Y + [8]          
0.00/0.64	                            [1 1]     [1 1]     [8]          
0.00/0.64	                          > [1 1] X + [1 1] Y + [1]          
0.00/0.64	                            [1 1]     [1 1]     [5]          
0.00/0.64	                          = [plus(X, times(Y, X))]           
0.00/0.64	                                                             
0.00/0.64	
0.00/0.64	We return to the main proof.
0.00/0.64	
0.00/0.64	We are left with following problem, upon which TcT provides the
0.00/0.64	certificate YES(O(1),O(1)).
0.00/0.64	
0.00/0.64	Weak Trs:
0.00/0.64	  { plus(plus(X, Y), Z) -> plus(X, plus(Y, Z))
0.00/0.64	  , times(X, s(Y)) -> plus(X, times(Y, X)) }
0.00/0.64	Obligation:
0.00/0.64	  innermost runtime complexity
0.00/0.64	Answer:
0.00/0.64	  YES(O(1),O(1))
0.00/0.64	
0.00/0.64	Empty rules are trivially bounded
0.00/0.64	
0.00/0.64	Hurray, we answered YES(O(1),O(n^1))
0.00/0.64	EOF