YES(?,O(n^1))
5.42/1.97	YES(?,O(n^1))
5.42/1.97	
5.42/1.97	We are left with following problem, upon which TcT provides the
5.42/1.97	certificate YES(?,O(n^1)).
5.42/1.97	
5.42/1.97	Strict Trs:
5.42/1.97	  { a(x, g()) -> a(f(), a(g(), a(f(), x)))
5.42/1.97	  , a(f(), a(f(), x)) -> a(x, g()) }
5.42/1.97	Obligation:
5.42/1.97	  derivational complexity
5.42/1.97	Answer:
5.42/1.97	  YES(?,O(n^1))
5.42/1.97	
5.42/1.97	The problem is match-bounded by 4. The enriched problem is
5.42/1.97	compatible with the following automaton.
5.42/1.97	{ a_0(1, 1) -> 1
5.42/1.97	, a_0(1, 2) -> 1
5.42/1.97	, a_0(1, 3) -> 1
5.42/1.97	, a_0(2, 1) -> 1
5.42/1.97	, a_0(2, 2) -> 1
5.42/1.97	, a_0(2, 3) -> 1
5.42/1.97	, a_0(3, 1) -> 1
5.42/1.97	, a_0(3, 2) -> 1
5.42/1.97	, a_0(3, 3) -> 1
5.42/1.97	, a_1(1, 6) -> 1
5.42/1.97	, a_1(1, 6) -> 7
5.42/1.97	, a_1(1, 6) -> 15
5.42/1.97	, a_1(2, 6) -> 1
5.42/1.97	, a_1(2, 6) -> 7
5.42/1.97	, a_1(2, 6) -> 15
5.42/1.97	, a_1(3, 6) -> 1
5.42/1.97	, a_1(3, 6) -> 7
5.42/1.97	, a_1(3, 6) -> 15
5.42/1.97	, a_1(4, 5) -> 1
5.42/1.97	, a_1(5, 6) -> 1
5.42/1.97	, a_1(6, 6) -> 1
5.42/1.97	, a_1(6, 6) -> 7
5.42/1.97	, a_1(6, 6) -> 15
5.42/1.97	, a_1(6, 7) -> 5
5.42/1.97	, a_1(6, 10) -> 1
5.42/1.97	, a_1(6, 23) -> 22
5.42/1.97	, a_1(8, 1) -> 7
5.42/1.97	, a_1(8, 2) -> 7
5.42/1.97	, a_1(8, 3) -> 7
5.42/1.97	, a_1(8, 8) -> 10
5.42/1.97	, a_1(8, 16) -> 23
5.42/1.97	, a_1(8, 22) -> 15
5.42/1.97	, a_1(14, 6) -> 1
5.42/1.97	, a_2(5, 9) -> 7
5.42/1.97	, a_2(5, 9) -> 15
5.42/1.97	, a_2(9, 15) -> 14
5.42/1.97	, a_2(13, 14) -> 1
5.42/1.97	, a_2(14, 9) -> 7
5.42/1.97	, a_2(16, 1) -> 15
5.42/1.97	, a_2(16, 2) -> 15
5.42/1.97	, a_2(16, 3) -> 15
5.42/1.97	, a_2(16, 5) -> 15
5.42/1.97	, a_2(16, 6) -> 15
5.42/1.97	, a_2(16, 14) -> 7
5.42/1.97	, a_2(16, 14) -> 15
5.42/1.97	, a_2(16, 16) -> 15
5.42/1.97	, a_3(14, 19) -> 15
5.42/1.97	, a_3(17, 18) -> 7
5.42/1.97	, a_3(19, 20) -> 18
5.42/1.97	, a_3(21, 5) -> 20
5.42/1.97	, a_3(21, 14) -> 20
5.42/1.97	, a_3(21, 18) -> 15
5.42/1.97	, a_4(24, 25) -> 15
5.42/1.97	, a_4(26, 27) -> 25
5.42/1.97	, a_4(28, 14) -> 27
5.42/1.97	, f_0() -> 2
5.42/1.97	, f_1() -> 4
5.42/1.97	, f_1() -> 8
5.42/1.97	, f_2() -> 13
5.42/1.97	, f_2() -> 16
5.42/1.97	, f_3() -> 17
5.42/1.97	, f_3() -> 21
5.42/1.97	, f_4() -> 24
5.42/1.97	, f_4() -> 28
5.42/1.97	, g_0() -> 3
5.42/1.97	, g_1() -> 6
5.42/1.97	, g_2() -> 9
5.42/1.97	, g_3() -> 19
5.42/1.97	, g_4() -> 26 }
5.42/1.97	
5.42/1.97	Hurray, we answered YES(?,O(n^1))
5.42/1.98	EOF