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