YES(O(1),O(1))
0.00/0.15	YES(O(1),O(1))
0.00/0.15	
0.00/0.15	We are left with following problem, upon which TcT provides the
0.00/0.15	certificate YES(O(1),O(1)).
0.00/0.15	
0.00/0.15	Strict Trs: { f(s(x), y, y) -> f(y, x, s(x)) }
0.00/0.15	Obligation:
0.00/0.15	  innermost runtime complexity
0.00/0.15	Answer:
0.00/0.15	  YES(O(1),O(1))
0.00/0.15	
0.00/0.15	We add the following weak dependency pairs:
0.00/0.15	
0.00/0.15	Strict DPs: { f^#(s(x), y, y) -> c_1(f^#(y, x, s(x))) }
0.00/0.15	
0.00/0.15	and mark the set of starting terms.
0.00/0.15	
0.00/0.15	We are left with following problem, upon which TcT provides the
0.00/0.15	certificate YES(O(1),O(1)).
0.00/0.15	
0.00/0.15	Strict DPs: { f^#(s(x), y, y) -> c_1(f^#(y, x, s(x))) }
0.00/0.15	Strict Trs: { f(s(x), y, y) -> f(y, x, s(x)) }
0.00/0.15	Obligation:
0.00/0.15	  innermost runtime complexity
0.00/0.15	Answer:
0.00/0.15	  YES(O(1),O(1))
0.00/0.15	
0.00/0.15	No rule is usable, rules are removed from the input problem.
0.00/0.15	
0.00/0.15	We are left with following problem, upon which TcT provides the
0.00/0.15	certificate YES(O(1),O(1)).
0.00/0.15	
0.00/0.15	Strict DPs: { f^#(s(x), y, y) -> c_1(f^#(y, x, s(x))) }
0.00/0.15	Obligation:
0.00/0.15	  innermost runtime complexity
0.00/0.15	Answer:
0.00/0.15	  YES(O(1),O(1))
0.00/0.15	
0.00/0.15	The weightgap principle applies (using the following constant
0.00/0.15	growth matrix-interpretation)
0.00/0.15	
0.00/0.15	The following argument positions are usable:
0.00/0.15	  none
0.00/0.15	
0.00/0.15	TcT has computed the following constructor-restricted matrix
0.00/0.15	interpretation.
0.00/0.15	
0.00/0.15	            [s](x1) = [0]
0.00/0.15	                      [0]
0.00/0.15	                         
0.00/0.15	  [f^#](x1, x2, x3) = [1]
0.00/0.15	                      [0]
0.00/0.15	                         
0.00/0.15	          [c_1](x1) = [0]
0.00/0.15	                      [0]
0.00/0.15	
0.00/0.15	The order satisfies the following ordering constraints:
0.00/0.15	
0.00/0.15	  [f^#(s(x), y, y)] = [1]                   
0.00/0.15	                      [0]                   
0.00/0.15	                    > [0]                   
0.00/0.15	                      [0]                   
0.00/0.15	                    = [c_1(f^#(y, x, s(x)))]
0.00/0.15	                                            
0.00/0.15	
0.00/0.15	Further, it can be verified that all rules not oriented are covered by the weightgap condition.
0.00/0.15	
0.00/0.15	We are left with following problem, upon which TcT provides the
0.00/0.15	certificate YES(O(1),O(1)).
0.00/0.15	
0.00/0.15	Weak DPs: { f^#(s(x), y, y) -> c_1(f^#(y, x, s(x))) }
0.00/0.15	Obligation:
0.00/0.15	  innermost runtime complexity
0.00/0.15	Answer:
0.00/0.15	  YES(O(1),O(1))
0.00/0.15	
0.00/0.15	The following weak DPs constitute a sub-graph of the DG that is
0.00/0.15	closed under successors. The DPs are removed.
0.00/0.15	
0.00/0.15	{ f^#(s(x), y, y) -> c_1(f^#(y, x, s(x))) }
0.00/0.15	
0.00/0.15	We are left with following problem, upon which TcT provides the
0.00/0.15	certificate YES(O(1),O(1)).
0.00/0.15	
0.00/0.15	Rules: Empty
0.00/0.15	Obligation:
0.00/0.15	  innermost runtime complexity
0.00/0.15	Answer:
0.00/0.15	  YES(O(1),O(1))
0.00/0.15	
0.00/0.15	Empty rules are trivially bounded
0.00/0.15	
0.00/0.15	Hurray, we answered YES(O(1),O(1))
0.00/0.15	EOF