YES(?,O(n^1))
2.65/1.02	YES(?,O(n^1))
2.65/1.02	
2.65/1.02	We are left with following problem, upon which TcT provides the
2.65/1.02	certificate YES(?,O(n^1)).
2.65/1.02	
2.65/1.02	Strict Trs:
2.65/1.02	  { minus(n__0(), Y) -> 0()
2.65/1.02	  , minus(n__s(X), n__s(Y)) -> minus(activate(X), activate(Y))
2.65/1.02	  , 0() -> n__0()
2.65/1.02	  , activate(X) -> X
2.65/1.02	  , activate(n__0()) -> 0()
2.65/1.02	  , activate(n__s(X)) -> s(X)
2.65/1.02	  , geq(X, n__0()) -> true()
2.65/1.02	  , geq(n__0(), n__s(Y)) -> false()
2.65/1.02	  , geq(n__s(X), n__s(Y)) -> geq(activate(X), activate(Y))
2.65/1.02	  , div(0(), n__s(Y)) -> 0()
2.65/1.02	  , div(s(X), n__s(Y)) ->
2.65/1.02	    if(geq(X, activate(Y)),
2.65/1.02	       n__s(div(minus(X, activate(Y)), n__s(activate(Y)))),
2.65/1.02	       n__0())
2.65/1.02	  , s(X) -> n__s(X)
2.65/1.02	  , if(true(), X, Y) -> activate(X)
2.65/1.02	  , if(false(), X, Y) -> activate(Y) }
2.65/1.02	Obligation:
2.65/1.02	  innermost runtime complexity
2.65/1.02	Answer:
2.65/1.02	  YES(?,O(n^1))
2.65/1.02	
2.65/1.02	Arguments of following rules are not normal-forms:
2.65/1.02	
2.65/1.02	{ div(0(), n__s(Y)) -> 0()
2.65/1.02	, div(s(X), n__s(Y)) ->
2.65/1.02	  if(geq(X, activate(Y)),
2.65/1.02	     n__s(div(minus(X, activate(Y)), n__s(activate(Y)))),
2.65/1.02	     n__0()) }
2.65/1.02	
2.65/1.02	All above mentioned rules can be savely removed.
2.65/1.02	
2.65/1.02	We are left with following problem, upon which TcT provides the
2.65/1.02	certificate YES(?,O(n^1)).
2.65/1.02	
2.65/1.02	Strict Trs:
2.65/1.02	  { minus(n__0(), Y) -> 0()
2.65/1.02	  , minus(n__s(X), n__s(Y)) -> minus(activate(X), activate(Y))
2.65/1.02	  , 0() -> n__0()
2.65/1.02	  , activate(X) -> X
2.65/1.02	  , activate(n__0()) -> 0()
2.65/1.02	  , activate(n__s(X)) -> s(X)
2.65/1.02	  , geq(X, n__0()) -> true()
2.65/1.02	  , geq(n__0(), n__s(Y)) -> false()
2.65/1.02	  , geq(n__s(X), n__s(Y)) -> geq(activate(X), activate(Y))
2.65/1.02	  , s(X) -> n__s(X)
2.65/1.02	  , if(true(), X, Y) -> activate(X)
2.65/1.02	  , if(false(), X, Y) -> activate(Y) }
2.65/1.02	Obligation:
2.65/1.02	  innermost runtime complexity
2.65/1.02	Answer:
2.65/1.02	  YES(?,O(n^1))
2.65/1.02	
2.65/1.02	The problem is match-bounded by 4. The enriched problem is
2.65/1.02	compatible with the following automaton.
2.65/1.02	{ minus_0(2, 2) -> 1
2.65/1.02	, minus_1(3, 4) -> 1
2.65/1.02	, minus_2(5, 6) -> 1
2.65/1.02	, minus_3(7, 8) -> 1
2.65/1.02	, n__0_0() -> 1
2.65/1.02	, n__0_0() -> 2
2.65/1.02	, n__0_0() -> 3
2.65/1.02	, n__0_0() -> 4
2.65/1.02	, n__0_0() -> 5
2.65/1.02	, n__0_0() -> 6
2.65/1.02	, n__0_0() -> 7
2.65/1.02	, n__0_0() -> 8
2.65/1.02	, n__0_1() -> 1
2.65/1.02	, n__0_2() -> 1
2.65/1.02	, n__0_2() -> 3
2.65/1.02	, n__0_2() -> 4
2.65/1.02	, n__0_2() -> 5
2.65/1.02	, n__0_2() -> 6
2.65/1.02	, n__0_2() -> 7
2.65/1.02	, n__0_2() -> 8
2.65/1.02	, n__0_3() -> 1
2.65/1.02	, n__0_4() -> 1
2.65/1.02	, 0_0() -> 1
2.65/1.02	, 0_1() -> 1
2.65/1.02	, 0_1() -> 3
2.65/1.02	, 0_1() -> 4
2.65/1.02	, 0_1() -> 5
2.65/1.02	, 0_1() -> 6
2.65/1.02	, 0_1() -> 7
2.65/1.02	, 0_1() -> 8
2.65/1.02	, 0_2() -> 1
2.65/1.02	, 0_3() -> 1
2.65/1.02	, n__s_0(2) -> 1
2.65/1.02	, n__s_0(2) -> 2
2.65/1.02	, n__s_0(2) -> 3
2.65/1.02	, n__s_0(2) -> 4
2.65/1.02	, n__s_0(2) -> 5
2.65/1.02	, n__s_0(2) -> 6
2.65/1.02	, n__s_0(2) -> 7
2.65/1.02	, n__s_0(2) -> 8
2.65/1.02	, n__s_1(2) -> 1
2.65/1.02	, n__s_2(2) -> 1
2.65/1.02	, n__s_2(2) -> 3
2.65/1.02	, n__s_2(2) -> 4
2.65/1.02	, n__s_2(2) -> 5
2.65/1.02	, n__s_2(2) -> 6
2.65/1.02	, n__s_2(2) -> 7
2.65/1.02	, n__s_2(2) -> 8
2.65/1.02	, activate_0(2) -> 1
2.65/1.02	, activate_1(2) -> 1
2.65/1.02	, activate_1(2) -> 3
2.65/1.02	, activate_1(2) -> 4
2.65/1.02	, activate_2(2) -> 5
2.65/1.02	, activate_2(2) -> 6
2.65/1.02	, activate_3(2) -> 7
2.65/1.02	, activate_3(2) -> 8
2.65/1.02	, geq_0(2, 2) -> 1
2.65/1.02	, geq_1(4, 4) -> 1
2.65/1.02	, geq_2(6, 6) -> 1
2.65/1.02	, geq_3(8, 8) -> 1
2.65/1.02	, true_0() -> 1
2.65/1.02	, true_0() -> 2
2.65/1.02	, true_0() -> 3
2.65/1.02	, true_0() -> 4
2.65/1.02	, true_0() -> 5
2.65/1.02	, true_0() -> 6
2.65/1.02	, true_0() -> 7
2.65/1.02	, true_0() -> 8
2.65/1.02	, true_1() -> 1
2.65/1.02	, true_2() -> 1
2.65/1.02	, true_3() -> 1
2.65/1.02	, false_0() -> 1
2.65/1.02	, false_0() -> 2
2.65/1.02	, false_0() -> 3
2.65/1.02	, false_0() -> 4
2.65/1.02	, false_0() -> 5
2.65/1.02	, false_0() -> 6
2.65/1.02	, false_0() -> 7
2.65/1.02	, false_0() -> 8
2.65/1.02	, false_1() -> 1
2.65/1.02	, false_2() -> 1
2.65/1.02	, false_3() -> 1
2.65/1.02	, s_0(2) -> 1
2.65/1.02	, s_1(2) -> 1
2.65/1.02	, s_1(2) -> 3
2.65/1.02	, s_1(2) -> 4
2.65/1.02	, s_1(2) -> 5
2.65/1.02	, s_1(2) -> 6
2.65/1.02	, s_1(2) -> 7
2.65/1.02	, s_1(2) -> 8
2.65/1.02	, if_0(2, 2, 2) -> 1 }
2.65/1.02	
2.65/1.02	Hurray, we answered YES(?,O(n^1))
2.65/1.02	EOF