YES(O(1),O(1))
0.00/0.33	YES(O(1),O(1))
0.00/0.33	
0.00/0.33	We are left with following problem, upon which TcT provides the
0.00/0.33	certificate YES(O(1),O(1)).
0.00/0.33	
0.00/0.33	Strict Trs:
0.00/0.33	  { *(x, 0()) -> 0()
0.00/0.33	  , *(*(x, y), z) -> *(x, *(y, z))
0.00/0.33	  , *(i(x), x) -> 1()
0.00/0.33	  , *(1(), y) -> y }
0.00/0.33	Obligation:
0.00/0.33	  innermost runtime complexity
0.00/0.33	Answer:
0.00/0.33	  YES(O(1),O(1))
0.00/0.33	
0.00/0.33	We add the following weak dependency pairs:
0.00/0.33	
0.00/0.33	Strict DPs:
0.00/0.33	  { *^#(x, 0()) -> c_1()
0.00/0.33	  , *^#(*(x, y), z) -> c_2(*^#(x, *(y, z)))
0.00/0.33	  , *^#(i(x), x) -> c_3()
0.00/0.33	  , *^#(1(), y) -> c_4() }
0.00/0.33	
0.00/0.33	and mark the set of starting terms.
0.00/0.33	
0.00/0.33	We are left with following problem, upon which TcT provides the
0.00/0.33	certificate YES(O(1),O(1)).
0.00/0.33	
0.00/0.33	Strict DPs:
0.00/0.33	  { *^#(x, 0()) -> c_1()
0.00/0.33	  , *^#(*(x, y), z) -> c_2(*^#(x, *(y, z)))
0.00/0.33	  , *^#(i(x), x) -> c_3()
0.00/0.33	  , *^#(1(), y) -> c_4() }
0.00/0.33	Strict Trs:
0.00/0.33	  { *(x, 0()) -> 0()
0.00/0.33	  , *(*(x, y), z) -> *(x, *(y, z))
0.00/0.33	  , *(i(x), x) -> 1()
0.00/0.33	  , *(1(), y) -> y }
0.00/0.33	Obligation:
0.00/0.33	  innermost runtime complexity
0.00/0.33	Answer:
0.00/0.33	  YES(O(1),O(1))
0.00/0.33	
0.00/0.33	The weightgap principle applies (using the following constant
0.00/0.33	growth matrix-interpretation)
0.00/0.33	
0.00/0.33	The following argument positions are usable:
0.00/0.33	  Uargs(*) = {2}, Uargs(*^#) = {2}, Uargs(c_2) = {1}
0.00/0.33	
0.00/0.33	TcT has computed the following constructor-restricted matrix
0.00/0.33	interpretation.
0.00/0.33	
0.00/0.33	    [*](x1, x2) = [2 0] x1 + [1 0] x2 + [1]
0.00/0.33	                  [0 0]      [0 1]      [0]
0.00/0.33	                                           
0.00/0.33	        [i](x1) = [0]                      
0.00/0.33	                  [0]                      
0.00/0.33	                                           
0.00/0.33	            [1] = [0]                      
0.00/0.33	                  [0]                      
0.00/0.33	                                           
0.00/0.33	            [0] = [0]                      
0.00/0.33	                  [0]                      
0.00/0.33	                                           
0.00/0.33	  [*^#](x1, x2) = [2 0] x1 + [1 0] x2 + [0]
0.00/0.33	                  [0 0]      [0 0]      [0]
0.00/0.33	                                           
0.00/0.33	          [c_1] = [1]                      
0.00/0.33	                  [0]                      
0.00/0.33	                                           
0.00/0.33	      [c_2](x1) = [1 0] x1 + [1]           
0.00/0.33	                  [0 1]      [2]           
0.00/0.33	                                           
0.00/0.33	          [c_3] = [1]                      
0.00/0.33	                  [0]                      
0.00/0.33	                                           
0.00/0.33	          [c_4] = [1]                      
0.00/0.33	                  [0]                      
0.00/0.33	
0.00/0.33	The order satisfies the following ordering constraints:
0.00/0.33	
0.00/0.33	        [*(x, 0())] = [2 0] x + [1]                    
0.00/0.33	                      [0 0]     [0]                    
0.00/0.33	                    > [0]                              
0.00/0.33	                      [0]                              
0.00/0.33	                    = [0()]                            
0.00/0.33	                                                       
0.00/0.33	    [*(*(x, y), z)] = [4 0] x + [2 0] y + [1 0] z + [3]
0.00/0.33	                      [0 0]     [0 0]     [0 1]     [0]
0.00/0.33	                    > [2 0] x + [2 0] y + [1 0] z + [2]
0.00/0.33	                      [0 0]     [0 0]     [0 1]     [0]
0.00/0.33	                    = [*(x, *(y, z))]                  
0.00/0.33	                                                       
0.00/0.33	       [*(i(x), x)] = [1 0] x + [1]                    
0.00/0.33	                      [0 1]     [0]                    
0.00/0.33	                    > [0]                              
0.00/0.33	                      [0]                              
0.00/0.33	                    = [1()]                            
0.00/0.33	                                                       
0.00/0.33	        [*(1(), y)] = [1 0] y + [1]                    
0.00/0.33	                      [0 1]     [0]                    
0.00/0.33	                    > [1 0] y + [0]                    
0.00/0.33	                      [0 1]     [0]                    
0.00/0.33	                    = [y]                              
0.00/0.33	                                                       
0.00/0.33	      [*^#(x, 0())] = [2 0] x + [0]                    
0.00/0.33	                      [0 0]     [0]                    
0.00/0.33	                    ? [1]                              
0.00/0.33	                      [0]                              
0.00/0.33	                    = [c_1()]                          
0.00/0.33	                                                       
0.00/0.33	  [*^#(*(x, y), z)] = [4 0] x + [2 0] y + [1 0] z + [2]
0.00/0.33	                      [0 0]     [0 0]     [0 0]     [0]
0.00/0.33	                    ? [2 0] x + [2 0] y + [1 0] z + [2]
0.00/0.33	                      [0 0]     [0 0]     [0 0]     [2]
0.00/0.33	                    = [c_2(*^#(x, *(y, z)))]           
0.00/0.33	                                                       
0.00/0.33	     [*^#(i(x), x)] = [1 0] x + [0]                    
0.00/0.33	                      [0 0]     [0]                    
0.00/0.33	                    ? [1]                              
0.00/0.33	                      [0]                              
0.00/0.33	                    = [c_3()]                          
0.00/0.33	                                                       
0.00/0.33	      [*^#(1(), y)] = [1 0] y + [0]                    
0.00/0.33	                      [0 0]     [0]                    
0.00/0.33	                    ? [1]                              
0.00/0.33	                      [0]                              
0.00/0.33	                    = [c_4()]                          
0.00/0.33	                                                       
0.00/0.33	
0.00/0.33	Further, it can be verified that all rules not oriented are covered by the weightgap condition.
0.00/0.33	
0.00/0.33	We are left with following problem, upon which TcT provides the
0.00/0.33	certificate YES(O(1),O(1)).
0.00/0.33	
0.00/0.33	Strict DPs:
0.00/0.33	  { *^#(x, 0()) -> c_1()
0.00/0.33	  , *^#(*(x, y), z) -> c_2(*^#(x, *(y, z)))
0.00/0.33	  , *^#(i(x), x) -> c_3()
0.00/0.33	  , *^#(1(), y) -> c_4() }
0.00/0.33	Weak Trs:
0.00/0.33	  { *(x, 0()) -> 0()
0.00/0.33	  , *(*(x, y), z) -> *(x, *(y, z))
0.00/0.33	  , *(i(x), x) -> 1()
0.00/0.33	  , *(1(), y) -> y }
0.00/0.33	Obligation:
0.00/0.33	  innermost runtime complexity
0.00/0.33	Answer:
0.00/0.33	  YES(O(1),O(1))
0.00/0.33	
0.00/0.33	Consider the dependency graph:
0.00/0.33	
0.00/0.33	  1: *^#(x, 0()) -> c_1()
0.00/0.33	  
0.00/0.33	  2: *^#(*(x, y), z) -> c_2(*^#(x, *(y, z)))
0.00/0.33	     -->_1 *^#(i(x), x) -> c_3() :3
0.00/0.33	     -->_1 *^#(x, 0()) -> c_1() :1
0.00/0.33	  
0.00/0.33	  3: *^#(i(x), x) -> c_3()
0.00/0.33	  
0.00/0.33	  4: *^#(1(), y) -> c_4()
0.00/0.33	  
0.00/0.33	
0.00/0.33	Only the nodes {1,3,4} are reachable from nodes {1,3,4} that start
0.00/0.33	derivation from marked basic terms. The nodes not reachable are
0.00/0.33	removed from the problem.
0.00/0.33	
0.00/0.33	We are left with following problem, upon which TcT provides the
0.00/0.33	certificate YES(O(1),O(1)).
0.00/0.33	
0.00/0.33	Strict DPs:
0.00/0.33	  { *^#(x, 0()) -> c_1()
0.00/0.33	  , *^#(i(x), x) -> c_3()
0.00/0.33	  , *^#(1(), y) -> c_4() }
0.00/0.33	Weak Trs:
0.00/0.33	  { *(x, 0()) -> 0()
0.00/0.33	  , *(*(x, y), z) -> *(x, *(y, z))
0.00/0.33	  , *(i(x), x) -> 1()
0.00/0.33	  , *(1(), y) -> y }
0.00/0.33	Obligation:
0.00/0.33	  innermost runtime complexity
0.00/0.33	Answer:
0.00/0.33	  YES(O(1),O(1))
0.00/0.33	
0.00/0.33	We estimate the number of application of {1,2,3} by applications of
0.00/0.33	Pre({1,2,3}) = {}. Here rules are labeled as follows:
0.00/0.33	
0.00/0.33	  DPs:
0.00/0.33	    { 1: *^#(x, 0()) -> c_1()
0.00/0.33	    , 2: *^#(i(x), x) -> c_3()
0.00/0.33	    , 3: *^#(1(), y) -> c_4() }
0.00/0.33	
0.00/0.33	We are left with following problem, upon which TcT provides the
0.00/0.33	certificate YES(O(1),O(1)).
0.00/0.33	
0.00/0.33	Weak DPs:
0.00/0.33	  { *^#(x, 0()) -> c_1()
0.00/0.33	  , *^#(i(x), x) -> c_3()
0.00/0.33	  , *^#(1(), y) -> c_4() }
0.00/0.33	Weak Trs:
0.00/0.33	  { *(x, 0()) -> 0()
0.00/0.33	  , *(*(x, y), z) -> *(x, *(y, z))
0.00/0.33	  , *(i(x), x) -> 1()
0.00/0.33	  , *(1(), y) -> y }
0.00/0.33	Obligation:
0.00/0.33	  innermost runtime complexity
0.00/0.33	Answer:
0.00/0.33	  YES(O(1),O(1))
0.00/0.33	
0.00/0.33	The following weak DPs constitute a sub-graph of the DG that is
0.00/0.33	closed under successors. The DPs are removed.
0.00/0.33	
0.00/0.33	{ *^#(x, 0()) -> c_1()
0.00/0.33	, *^#(i(x), x) -> c_3()
0.00/0.33	, *^#(1(), y) -> c_4() }
0.00/0.33	
0.00/0.33	We are left with following problem, upon which TcT provides the
0.00/0.33	certificate YES(O(1),O(1)).
0.00/0.33	
0.00/0.33	Weak Trs:
0.00/0.33	  { *(x, 0()) -> 0()
0.00/0.33	  , *(*(x, y), z) -> *(x, *(y, z))
0.00/0.33	  , *(i(x), x) -> 1()
0.00/0.33	  , *(1(), y) -> y }
0.00/0.33	Obligation:
0.00/0.33	  innermost runtime complexity
0.00/0.33	Answer:
0.00/0.33	  YES(O(1),O(1))
0.00/0.33	
0.00/0.33	No rule is usable, rules are removed from the input problem.
0.00/0.33	
0.00/0.33	We are left with following problem, upon which TcT provides the
0.00/0.33	certificate YES(O(1),O(1)).
0.00/0.33	
0.00/0.33	Rules: Empty
0.00/0.33	Obligation:
0.00/0.33	  innermost runtime complexity
0.00/0.33	Answer:
0.00/0.33	  YES(O(1),O(1))
0.00/0.33	
0.00/0.33	Empty rules are trivially bounded
0.00/0.33	
0.00/0.33	Hurray, we answered YES(O(1),O(1))
0.00/0.34	EOF