YES(O(1),O(1))
2.42/1.22	YES(O(1),O(1))
2.42/1.22	
2.42/1.22	We are left with following problem, upon which TcT provides the
2.42/1.22	certificate YES(O(1),O(1)).
2.42/1.22	
2.42/1.22	Strict Trs:
2.42/1.22	  { f(g(i(a(), b(), b'()), c()), d()) ->
2.42/1.22	    if(e(), f(.(b(), c()), d'()), f(.(b'(), c()), d'()))
2.42/1.22	  , f(g(h(a(), b()), c()), d()) ->
2.42/1.22	    if(e(), f(.(b(), g(h(a(), b()), c())), d()), f(c(), d'())) }
2.42/1.22	Obligation:
2.42/1.22	  runtime complexity
2.42/1.22	Answer:
2.42/1.22	  YES(O(1),O(1))
2.42/1.22	
2.42/1.22	The input is overlay and right-linear. Switching to innermost
2.42/1.22	rewriting.
2.42/1.22	
2.42/1.22	We are left with following problem, upon which TcT provides the
2.42/1.22	certificate YES(O(1),O(1)).
2.42/1.22	
2.42/1.22	Strict Trs:
2.42/1.22	  { f(g(i(a(), b(), b'()), c()), d()) ->
2.42/1.22	    if(e(), f(.(b(), c()), d'()), f(.(b'(), c()), d'()))
2.42/1.22	  , f(g(h(a(), b()), c()), d()) ->
2.42/1.22	    if(e(), f(.(b(), g(h(a(), b()), c())), d()), f(c(), d'())) }
2.42/1.22	Obligation:
2.42/1.22	  innermost runtime complexity
2.42/1.22	Answer:
2.42/1.22	  YES(O(1),O(1))
2.42/1.22	
2.42/1.22	We add the following weak dependency pairs:
2.42/1.22	
2.42/1.22	Strict DPs:
2.42/1.22	  { f^#(g(i(a(), b(), b'()), c()), d()) ->
2.42/1.22	    c_1(f^#(.(b(), c()), d'()), f^#(.(b'(), c()), d'()))
2.42/1.22	  , f^#(g(h(a(), b()), c()), d()) ->
2.42/1.22	    c_2(f^#(.(b(), g(h(a(), b()), c())), d()), f^#(c(), d'())) }
2.42/1.22	
2.42/1.22	and mark the set of starting terms.
2.42/1.22	
2.42/1.22	We are left with following problem, upon which TcT provides the
2.42/1.22	certificate YES(O(1),O(1)).
2.42/1.22	
2.42/1.22	Strict DPs:
2.42/1.22	  { f^#(g(i(a(), b(), b'()), c()), d()) ->
2.42/1.22	    c_1(f^#(.(b(), c()), d'()), f^#(.(b'(), c()), d'()))
2.42/1.22	  , f^#(g(h(a(), b()), c()), d()) ->
2.42/1.22	    c_2(f^#(.(b(), g(h(a(), b()), c())), d()), f^#(c(), d'())) }
2.42/1.22	Strict Trs:
2.42/1.22	  { f(g(i(a(), b(), b'()), c()), d()) ->
2.42/1.22	    if(e(), f(.(b(), c()), d'()), f(.(b'(), c()), d'()))
2.42/1.22	  , f(g(h(a(), b()), c()), d()) ->
2.42/1.22	    if(e(), f(.(b(), g(h(a(), b()), c())), d()), f(c(), d'())) }
2.42/1.22	Obligation:
2.42/1.22	  innermost runtime complexity
2.42/1.22	Answer:
2.42/1.22	  YES(O(1),O(1))
2.42/1.22	
2.42/1.22	No rule is usable, rules are removed from the input problem.
2.42/1.22	
2.42/1.22	We are left with following problem, upon which TcT provides the
2.42/1.22	certificate YES(O(1),O(1)).
2.42/1.22	
2.42/1.22	Strict DPs:
2.42/1.22	  { f^#(g(i(a(), b(), b'()), c()), d()) ->
2.42/1.22	    c_1(f^#(.(b(), c()), d'()), f^#(.(b'(), c()), d'()))
2.42/1.22	  , f^#(g(h(a(), b()), c()), d()) ->
2.42/1.22	    c_2(f^#(.(b(), g(h(a(), b()), c())), d()), f^#(c(), d'())) }
2.42/1.22	Obligation:
2.42/1.22	  innermost runtime complexity
2.42/1.22	Answer:
2.42/1.22	  YES(O(1),O(1))
2.42/1.22	
2.42/1.22	The weightgap principle applies (using the following constant
2.42/1.22	growth matrix-interpretation)
2.42/1.22	
2.42/1.22	The following argument positions are usable:
2.42/1.22	  none
2.42/1.22	
2.42/1.22	TcT has computed the following constructor-restricted matrix
2.42/1.22	interpretation.
2.42/1.22	
2.42/1.22	      [g](x1, x2) = [0]
2.42/1.22	                    [0]
2.42/1.22	                       
2.42/1.22	  [i](x1, x2, x3) = [0]
2.42/1.22	                    [0]
2.42/1.22	                       
2.42/1.22	              [a] = [0]
2.42/1.22	                    [0]
2.42/1.22	                       
2.42/1.22	              [b] = [0]
2.42/1.22	                    [0]
2.42/1.22	                       
2.42/1.22	             [b'] = [0]
2.42/1.22	                    [0]
2.42/1.22	                       
2.42/1.22	              [c] = [0]
2.42/1.22	                    [0]
2.42/1.22	                       
2.42/1.22	              [d] = [0]
2.42/1.22	                    [0]
2.42/1.22	                       
2.42/1.22	      [.](x1, x2) = [0]
2.42/1.22	                    [0]
2.42/1.22	                       
2.42/1.22	             [d'] = [0]
2.42/1.22	                    [0]
2.42/1.22	                       
2.42/1.22	      [h](x1, x2) = [0]
2.42/1.22	                    [0]
2.42/1.22	                       
2.42/1.22	    [f^#](x1, x2) = [1]
2.42/1.22	                    [0]
2.42/1.22	                       
2.42/1.22	    [c_1](x1, x2) = [1]
2.42/1.22	                    [0]
2.42/1.22	                       
2.42/1.22	    [c_2](x1, x2) = [0]
2.42/1.22	                    [0]
2.42/1.22	
2.42/1.22	The order satisfies the following ordering constraints:
2.42/1.22	
2.42/1.22	  [f^#(g(i(a(), b(), b'()), c()), d())] =  [1]                                                         
2.42/1.22	                                           [0]                                                         
2.42/1.22	                                        >= [1]                                                         
2.42/1.22	                                           [0]                                                         
2.42/1.22	                                        =  [c_1(f^#(.(b(), c()), d'()), f^#(.(b'(), c()), d'()))]      
2.42/1.22	                                                                                                       
2.42/1.22	        [f^#(g(h(a(), b()), c()), d())] =  [1]                                                         
2.42/1.22	                                           [0]                                                         
2.42/1.22	                                        >  [0]                                                         
2.42/1.22	                                           [0]                                                         
2.42/1.22	                                        =  [c_2(f^#(.(b(), g(h(a(), b()), c())), d()), f^#(c(), d'()))]
2.42/1.22	                                                                                                       
2.42/1.22	
2.42/1.22	Further, it can be verified that all rules not oriented are covered by the weightgap condition.
2.42/1.22	
2.42/1.22	We are left with following problem, upon which TcT provides the
2.42/1.22	certificate YES(O(1),O(1)).
2.42/1.22	
2.42/1.22	Strict DPs:
2.42/1.22	  { f^#(g(i(a(), b(), b'()), c()), d()) ->
2.42/1.22	    c_1(f^#(.(b(), c()), d'()), f^#(.(b'(), c()), d'())) }
2.42/1.22	Weak DPs:
2.42/1.22	  { f^#(g(h(a(), b()), c()), d()) ->
2.42/1.22	    c_2(f^#(.(b(), g(h(a(), b()), c())), d()), f^#(c(), d'())) }
2.42/1.22	Obligation:
2.42/1.22	  innermost runtime complexity
2.42/1.22	Answer:
2.42/1.22	  YES(O(1),O(1))
2.42/1.22	
2.42/1.22	We estimate the number of application of {1} by applications of
2.42/1.22	Pre({1}) = {}. Here rules are labeled as follows:
2.42/1.22	
2.42/1.22	  DPs:
2.42/1.22	    { 1: f^#(g(i(a(), b(), b'()), c()), d()) ->
2.42/1.22	         c_1(f^#(.(b(), c()), d'()), f^#(.(b'(), c()), d'()))
2.42/1.22	    , 2: f^#(g(h(a(), b()), c()), d()) ->
2.42/1.22	         c_2(f^#(.(b(), g(h(a(), b()), c())), d()), f^#(c(), d'())) }
2.42/1.22	
2.42/1.22	We are left with following problem, upon which TcT provides the
2.42/1.22	certificate YES(O(1),O(1)).
2.42/1.22	
2.42/1.22	Weak DPs:
2.42/1.22	  { f^#(g(i(a(), b(), b'()), c()), d()) ->
2.42/1.22	    c_1(f^#(.(b(), c()), d'()), f^#(.(b'(), c()), d'()))
2.42/1.22	  , f^#(g(h(a(), b()), c()), d()) ->
2.42/1.22	    c_2(f^#(.(b(), g(h(a(), b()), c())), d()), f^#(c(), d'())) }
2.42/1.22	Obligation:
2.42/1.22	  innermost runtime complexity
2.42/1.22	Answer:
2.42/1.22	  YES(O(1),O(1))
2.42/1.22	
2.42/1.22	The following weak DPs constitute a sub-graph of the DG that is
2.42/1.22	closed under successors. The DPs are removed.
2.42/1.22	
2.42/1.22	{ f^#(g(i(a(), b(), b'()), c()), d()) ->
2.42/1.22	  c_1(f^#(.(b(), c()), d'()), f^#(.(b'(), c()), d'()))
2.42/1.22	, f^#(g(h(a(), b()), c()), d()) ->
2.42/1.22	  c_2(f^#(.(b(), g(h(a(), b()), c())), d()), f^#(c(), d'())) }
2.42/1.22	
2.42/1.22	We are left with following problem, upon which TcT provides the
2.42/1.22	certificate YES(O(1),O(1)).
2.42/1.22	
2.42/1.22	Rules: Empty
2.42/1.22	Obligation:
2.42/1.22	  innermost runtime complexity
2.42/1.22	Answer:
2.42/1.22	  YES(O(1),O(1))
2.42/1.22	
2.42/1.22	Empty rules are trivially bounded
2.42/1.22	
2.42/1.22	Hurray, we answered YES(O(1),O(1))
2.42/1.22	EOF