YES(O(1),O(1))
12.58/4.93	YES(O(1),O(1))
12.58/4.93	
12.58/4.93	We are left with following problem, upon which TcT provides the
12.58/4.93	certificate YES(O(1),O(1)).
12.58/4.93	
12.58/4.93	Strict Trs:
12.58/4.93	  { g(X) -> u(h(X), h(X), X)
12.58/4.93	  , u(d(), c(Y), X) -> k(Y)
12.58/4.93	  , h(d()) -> c(a())
12.58/4.93	  , h(d()) -> c(b())
12.58/4.93	  , f(k(a()), k(b()), X) -> f(X, X, X) }
12.58/4.93	Obligation:
12.58/4.93	  runtime complexity
12.58/4.93	Answer:
12.58/4.93	  YES(O(1),O(1))
12.58/4.93	
12.58/4.93	We add the following weak dependency pairs:
12.58/4.93	
12.58/4.93	Strict DPs:
12.58/4.93	  { g^#(X) -> c_1(u^#(h(X), h(X), X))
12.58/4.93	  , u^#(d(), c(Y), X) -> c_2(Y)
12.58/4.93	  , h^#(d()) -> c_3()
12.58/4.93	  , h^#(d()) -> c_4()
12.58/4.93	  , f^#(k(a()), k(b()), X) -> c_5(f^#(X, X, X)) }
12.58/4.93	
12.58/4.93	and mark the set of starting terms.
12.58/4.93	
12.58/4.93	We are left with following problem, upon which TcT provides the
12.58/4.93	certificate YES(O(1),O(1)).
12.58/4.93	
12.58/4.93	Strict DPs:
12.58/4.93	  { g^#(X) -> c_1(u^#(h(X), h(X), X))
12.58/4.93	  , u^#(d(), c(Y), X) -> c_2(Y)
12.58/4.93	  , h^#(d()) -> c_3()
12.58/4.93	  , h^#(d()) -> c_4()
12.58/4.93	  , f^#(k(a()), k(b()), X) -> c_5(f^#(X, X, X)) }
12.58/4.93	Strict Trs:
12.58/4.93	  { g(X) -> u(h(X), h(X), X)
12.58/4.93	  , u(d(), c(Y), X) -> k(Y)
12.58/4.93	  , h(d()) -> c(a())
12.58/4.93	  , h(d()) -> c(b())
12.58/4.93	  , f(k(a()), k(b()), X) -> f(X, X, X) }
12.58/4.93	Obligation:
12.58/4.93	  runtime complexity
12.58/4.93	Answer:
12.58/4.93	  YES(O(1),O(1))
12.58/4.93	
12.58/4.93	We replace rewrite rules by usable rules:
12.58/4.93	
12.58/4.93	  Strict Usable Rules:
12.58/4.93	    { h(d()) -> c(a())
12.58/4.93	    , h(d()) -> c(b()) }
12.58/4.93	
12.58/4.93	We are left with following problem, upon which TcT provides the
12.58/4.93	certificate YES(O(1),O(1)).
12.58/4.93	
12.58/4.93	Strict DPs:
12.58/4.93	  { g^#(X) -> c_1(u^#(h(X), h(X), X))
12.58/4.93	  , u^#(d(), c(Y), X) -> c_2(Y)
12.58/4.93	  , h^#(d()) -> c_3()
12.58/4.93	  , h^#(d()) -> c_4()
12.58/4.93	  , f^#(k(a()), k(b()), X) -> c_5(f^#(X, X, X)) }
12.58/4.93	Strict Trs:
12.58/4.93	  { h(d()) -> c(a())
12.58/4.93	  , h(d()) -> c(b()) }
12.58/4.93	Obligation:
12.58/4.93	  runtime complexity
12.58/4.93	Answer:
12.58/4.93	  YES(O(1),O(1))
12.58/4.93	
12.58/4.93	The weightgap principle applies (using the following constant
12.58/4.93	growth matrix-interpretation)
12.58/4.93	
12.58/4.93	The following argument positions are usable:
12.58/4.93	  Uargs(c_1) = {1}, Uargs(u^#) = {1, 2}
12.58/4.93	
12.58/4.93	TcT has computed the following constructor-restricted matrix
12.58/4.93	interpretation.
12.58/4.93	
12.58/4.93	            [h](x1) = [2]                                 
12.58/4.93	                      [0]                                 
12.58/4.93	                                                          
12.58/4.93	                [d] = [0]                                 
12.58/4.93	                      [0]                                 
12.58/4.93	                                                          
12.58/4.93	            [c](x1) = [0]                                 
12.58/4.93	                      [0]                                 
12.58/4.93	                                                          
12.58/4.93	            [k](x1) = [0]                                 
12.58/4.93	                      [0]                                 
12.58/4.93	                                                          
12.58/4.93	                [a] = [0]                                 
12.58/4.93	                      [0]                                 
12.58/4.93	                                                          
12.58/4.93	                [b] = [0]                                 
12.58/4.93	                      [0]                                 
12.58/4.93	                                                          
12.58/4.93	          [g^#](x1) = [1 1] x1 + [1]                      
12.58/4.93	                      [1 1]      [2]                      
12.58/4.93	                                                          
12.58/4.93	          [c_1](x1) = [1 0] x1 + [0]                      
12.58/4.93	                      [0 1]      [2]                      
12.58/4.93	                                                          
12.58/4.93	  [u^#](x1, x2, x3) = [1 0] x1 + [2 0] x2 + [0 0] x3 + [1]
12.58/4.93	                      [1 1]      [0 0]      [1 1]      [2]
12.58/4.93	                                                          
12.58/4.93	          [c_2](x1) = [0 0] x1 + [1]                      
12.58/4.93	                      [1 1]      [1]                      
12.58/4.93	                                                          
12.58/4.93	          [h^#](x1) = [1 2] x1 + [2]                      
12.58/4.93	                      [2 1]      [2]                      
12.58/4.93	                                                          
12.58/4.93	              [c_3] = [1]                                 
12.58/4.93	                      [1]                                 
12.58/4.93	                                                          
12.58/4.93	              [c_4] = [1]                                 
12.58/4.93	                      [1]                                 
12.58/4.93	                                                          
12.58/4.93	  [f^#](x1, x2, x3) = [1]                                 
12.58/4.93	                      [2]                                 
12.58/4.93	                                                          
12.58/4.93	          [c_5](x1) = [2]                                 
12.58/4.93	                      [2]                                 
12.58/4.93	
12.58/4.93	The order satisfies the following ordering constraints:
12.58/4.93	
12.58/4.93	                  [h(d())] = [2]                      
12.58/4.93	                             [0]                      
12.58/4.93	                           > [0]                      
12.58/4.93	                             [0]                      
12.58/4.93	                           = [c(a())]                 
12.58/4.93	                                                      
12.58/4.93	                  [h(d())] = [2]                      
12.58/4.93	                             [0]                      
12.58/4.93	                           > [0]                      
12.58/4.93	                             [0]                      
12.58/4.93	                           = [c(b())]                 
12.58/4.93	                                                      
12.58/4.93	                  [g^#(X)] = [1 1] X + [1]            
12.58/4.93	                             [1 1]     [2]            
12.58/4.93	                           ? [0 0] X + [7]            
12.58/4.93	                             [1 1]     [6]            
12.58/4.93	                           = [c_1(u^#(h(X), h(X), X))]
12.58/4.93	                                                      
12.58/4.93	       [u^#(d(), c(Y), X)] = [0 0] X + [1]            
12.58/4.93	                             [1 1]     [2]            
12.58/4.93	                           ? [0 0] Y + [1]            
12.58/4.93	                             [1 1]     [1]            
12.58/4.93	                           = [c_2(Y)]                 
12.58/4.93	                                                      
12.58/4.93	                [h^#(d())] = [2]                      
12.58/4.93	                             [2]                      
12.58/4.93	                           > [1]                      
12.58/4.93	                             [1]                      
12.58/4.93	                           = [c_3()]                  
12.58/4.93	                                                      
12.58/4.93	                [h^#(d())] = [2]                      
12.58/4.93	                             [2]                      
12.58/4.93	                           > [1]                      
12.58/4.93	                             [1]                      
12.58/4.93	                           = [c_4()]                  
12.58/4.93	                                                      
12.58/4.93	  [f^#(k(a()), k(b()), X)] = [1]                      
12.58/4.93	                             [2]                      
12.58/4.93	                           ? [2]                      
12.58/4.93	                             [2]                      
12.58/4.93	                           = [c_5(f^#(X, X, X))]      
12.58/4.93	                                                      
12.58/4.93	
12.58/4.93	Further, it can be verified that all rules not oriented are covered by the weightgap condition.
12.58/4.93	
12.58/4.93	We are left with following problem, upon which TcT provides the
12.58/4.93	certificate YES(O(1),O(1)).
12.58/4.93	
12.58/4.93	Strict DPs:
12.58/4.93	  { g^#(X) -> c_1(u^#(h(X), h(X), X))
12.58/4.93	  , u^#(d(), c(Y), X) -> c_2(Y)
12.58/4.93	  , f^#(k(a()), k(b()), X) -> c_5(f^#(X, X, X)) }
12.58/4.93	Weak DPs:
12.58/4.93	  { h^#(d()) -> c_3()
12.58/4.93	  , h^#(d()) -> c_4() }
12.58/4.93	Weak Trs:
12.58/4.93	  { h(d()) -> c(a())
12.58/4.93	  , h(d()) -> c(b()) }
12.58/4.93	Obligation:
12.58/4.93	  runtime complexity
12.58/4.93	Answer:
12.58/4.93	  YES(O(1),O(1))
12.58/4.93	
12.58/4.93	We estimate the number of application of {1,3} by applications of
12.58/4.93	Pre({1,3}) = {2}. Here rules are labeled as follows:
12.58/4.93	
12.58/4.93	  DPs:
12.58/4.93	    { 1: g^#(X) -> c_1(u^#(h(X), h(X), X))
12.58/4.93	    , 2: u^#(d(), c(Y), X) -> c_2(Y)
12.58/4.93	    , 3: f^#(k(a()), k(b()), X) -> c_5(f^#(X, X, X))
12.58/4.93	    , 4: h^#(d()) -> c_3()
12.58/4.93	    , 5: h^#(d()) -> c_4() }
12.58/4.93	
12.58/4.93	We are left with following problem, upon which TcT provides the
12.58/4.93	certificate YES(O(1),O(1)).
12.58/4.93	
12.58/4.93	Strict DPs: { u^#(d(), c(Y), X) -> c_2(Y) }
12.58/4.93	Weak DPs:
12.58/4.93	  { g^#(X) -> c_1(u^#(h(X), h(X), X))
12.58/4.93	  , h^#(d()) -> c_3()
12.58/4.93	  , h^#(d()) -> c_4()
12.58/4.93	  , f^#(k(a()), k(b()), X) -> c_5(f^#(X, X, X)) }
12.58/4.93	Weak Trs:
12.58/4.93	  { h(d()) -> c(a())
12.58/4.93	  , h(d()) -> c(b()) }
12.58/4.93	Obligation:
12.58/4.93	  runtime complexity
12.58/4.93	Answer:
12.58/4.93	  YES(O(1),O(1))
12.58/4.93	
12.58/4.93	The following weak DPs constitute a sub-graph of the DG that is
12.58/4.93	closed under successors. The DPs are removed.
12.58/4.93	
12.58/4.93	{ g^#(X) -> c_1(u^#(h(X), h(X), X))
12.58/4.93	, h^#(d()) -> c_3()
12.58/4.93	, h^#(d()) -> c_4()
12.58/4.93	, f^#(k(a()), k(b()), X) -> c_5(f^#(X, X, X)) }
12.58/4.93	
12.58/4.93	We are left with following problem, upon which TcT provides the
12.58/4.93	certificate YES(O(1),O(1)).
12.58/4.93	
12.58/4.93	Strict DPs: { u^#(d(), c(Y), X) -> c_2(Y) }
12.58/4.93	Weak Trs:
12.58/4.93	  { h(d()) -> c(a())
12.58/4.93	  , h(d()) -> c(b()) }
12.58/4.93	Obligation:
12.58/4.93	  runtime complexity
12.58/4.93	Answer:
12.58/4.93	  YES(O(1),O(1))
12.58/4.93	
12.58/4.93	No rule is usable, rules are removed from the input problem.
12.58/4.93	
12.58/4.93	We are left with following problem, upon which TcT provides the
12.58/4.93	certificate YES(O(1),O(1)).
12.58/4.93	
12.58/4.93	Strict DPs: { u^#(d(), c(Y), X) -> c_2(Y) }
12.58/4.93	Obligation:
12.58/4.93	  runtime complexity
12.58/4.93	Answer:
12.58/4.93	  YES(O(1),O(1))
12.58/4.93	
12.58/4.93	We use the processor 'matrix interpretation of dimension 1' to
12.58/4.93	orient following rules strictly.
12.58/4.93	
12.58/4.93	DPs:
12.58/4.93	  { 1: u^#(d(), c(Y), X) -> c_2(Y) }
12.58/4.93	
12.58/4.93	Sub-proof:
12.58/4.93	----------
12.58/4.93	  The following argument positions are usable:
12.58/4.93	    none
12.58/4.93	  
12.58/4.93	  TcT has computed the following constructor-restricted matrix
12.58/4.93	  interpretation. Note that the diagonal of the component-wise maxima
12.58/4.93	  of interpretation-entries (of constructors) contains no more than 0
12.58/4.93	  non-zero entries.
12.58/4.93	  
12.58/4.93	                  [d] = [7]                  
12.58/4.93	                                             
12.58/4.93	              [c](x1) = [0]                  
12.58/4.93	                                             
12.58/4.93	    [u^#](x1, x2, x3) = [7] x2 + [7] x3 + [7]
12.58/4.93	                                             
12.58/4.93	            [c_2](x1) = [5]                  
12.58/4.93	  
12.58/4.93	  The order satisfies the following ordering constraints:
12.58/4.93	  
12.58/4.93	    [u^#(d(), c(Y), X)] = [7] X + [7]
12.58/4.93	                        > [5]        
12.58/4.93	                        = [c_2(Y)]   
12.58/4.93	                                     
12.58/4.93	
12.58/4.93	The strictly oriented rules are moved into the weak component.
12.58/4.93	
12.58/4.93	We are left with following problem, upon which TcT provides the
12.58/4.93	certificate YES(O(1),O(1)).
12.58/4.93	
12.58/4.93	Weak DPs: { u^#(d(), c(Y), X) -> c_2(Y) }
12.58/4.93	Obligation:
12.58/4.93	  runtime complexity
12.58/4.93	Answer:
12.58/4.93	  YES(O(1),O(1))
12.58/4.93	
12.58/4.93	The following weak DPs constitute a sub-graph of the DG that is
12.58/4.93	closed under successors. The DPs are removed.
12.58/4.93	
12.58/4.93	{ u^#(d(), c(Y), X) -> c_2(Y) }
12.58/4.93	
12.58/4.93	We are left with following problem, upon which TcT provides the
12.58/4.93	certificate YES(O(1),O(1)).
12.58/4.93	
12.58/4.93	Rules: Empty
12.58/4.93	Obligation:
12.58/4.93	  runtime complexity
12.58/4.93	Answer:
12.58/4.93	  YES(O(1),O(1))
12.58/4.93	
12.58/4.93	Empty rules are trivially bounded
12.58/4.93	
12.58/4.93	Hurray, we answered YES(O(1),O(1))
12.58/4.94	EOF