YES(?,O(n^1))
30.70/20.43	YES(?,O(n^1))
30.70/20.43	
30.70/20.43	We are left with following problem, upon which TcT provides the
30.70/20.43	certificate YES(?,O(n^1)).
30.70/20.43	
30.70/20.43	Strict Trs:
30.70/20.43	  { c(y) -> y
30.70/20.43	  , c(c(c(y))) -> c(c(a(y, 0())))
30.70/20.43	  , c(a(a(0(), x), y)) -> a(c(c(c(0()))), y) }
30.70/20.43	Obligation:
30.70/20.43	  derivational complexity
30.70/20.43	Answer:
30.70/20.43	  YES(?,O(n^1))
30.70/20.43	
30.70/20.43	The problem is match-bounded by 3. The enriched problem is
30.70/20.43	compatible with the following automaton.
30.70/20.43	{ c_0(1) -> 1
30.70/20.43	, c_1(2) -> 1
30.70/20.43	, c_1(3) -> 1
30.70/20.43	, c_1(3) -> 2
30.70/20.43	, c_1(4) -> 5
30.70/20.43	, c_1(4) -> 6
30.70/20.43	, c_1(4) -> 7
30.70/20.43	, c_1(6) -> 5
30.70/20.43	, c_1(7) -> 5
30.70/20.43	, c_1(7) -> 6
30.70/20.43	, c_2(10) -> 5
30.70/20.43	, c_2(11) -> 5
30.70/20.43	, c_2(11) -> 10
30.70/20.43	, c_2(12) -> 13
30.70/20.43	, c_2(12) -> 14
30.70/20.43	, c_2(12) -> 15
30.70/20.43	, c_2(14) -> 13
30.70/20.43	, c_2(15) -> 13
30.70/20.43	, c_2(15) -> 14
30.70/20.43	, c_3(16) -> 13
30.70/20.43	, c_3(17) -> 13
30.70/20.43	, c_3(17) -> 16
30.70/20.43	, a_0(1, 1) -> 1
30.70/20.43	, a_1(1, 4) -> 1
30.70/20.43	, a_1(1, 4) -> 2
30.70/20.43	, a_1(1, 4) -> 3
30.70/20.43	, a_1(2, 7) -> 1
30.70/20.43	, a_1(2, 7) -> 2
30.70/20.43	, a_1(2, 7) -> 3
30.70/20.43	, a_1(3, 7) -> 1
30.70/20.43	, a_1(3, 7) -> 2
30.70/20.43	, a_1(3, 7) -> 3
30.70/20.43	, a_1(5, 1) -> 1
30.70/20.43	, a_1(5, 4) -> 1
30.70/20.43	, a_1(5, 4) -> 2
30.70/20.43	, a_1(5, 7) -> 1
30.70/20.43	, a_1(5, 7) -> 2
30.70/20.43	, a_2(4, 12) -> 5
30.70/20.43	, a_2(4, 12) -> 10
30.70/20.43	, a_2(4, 12) -> 11
30.70/20.43	, a_2(13, 4) -> 1
30.70/20.43	, a_2(13, 4) -> 2
30.70/20.43	, a_2(13, 7) -> 1
30.70/20.43	, a_2(13, 7) -> 2
30.70/20.43	, a_3(12, 18) -> 13
30.70/20.43	, a_3(12, 18) -> 16
30.70/20.43	, a_3(12, 18) -> 17
30.70/20.43	, 0_0() -> 1
30.70/20.43	, 0_1() -> 4
30.70/20.43	, 0_1() -> 5
30.70/20.43	, 0_1() -> 6
30.70/20.43	, 0_1() -> 7
30.70/20.43	, 0_2() -> 12
30.70/20.43	, 0_2() -> 13
30.70/20.43	, 0_2() -> 14
30.70/20.43	, 0_2() -> 15
30.70/20.43	, 0_3() -> 18 }
30.70/20.43	
30.70/20.43	Hurray, we answered YES(?,O(n^1))
30.70/20.46	EOF