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