YES(?,O(n^1))
51.52/29.42	YES(?,O(n^1))
51.52/29.42	
51.52/29.42	We are left with following problem, upon which TcT provides the
51.52/29.42	certificate YES(?,O(n^1)).
51.52/29.42	
51.52/29.42	Strict Trs:
51.52/29.42	  { f(x, h1(y, z)) -> h2(0(), x, h1(y, z))
51.52/29.42	  , f(j(x, y), y) -> g(f(x, k(y)))
51.52/29.42	  , g(h2(x, y, h1(z, u))) -> h2(s(x), y, h1(z, u))
51.52/29.42	  , k(h1(x, y)) -> h1(s(x), y)
51.52/29.42	  , k(h(x)) -> h1(0(), x)
51.52/29.42	  , h2(x, j(y, h1(z, u)), h1(z, u)) -> h2(s(x), y, h1(s(z), u))
51.52/29.42	  , i(f(x, h(y))) -> y
51.52/29.42	  , i(h2(s(x), y, h1(x, z))) -> z }
51.52/29.42	Obligation:
51.52/29.42	  derivational complexity
51.52/29.42	Answer:
51.52/29.42	  YES(?,O(n^1))
51.52/29.42	
51.52/29.42	The problem is match-bounded by 2. The enriched problem is
51.52/29.42	compatible with the following automaton.
51.52/29.42	{ f_0(1, 1) -> 1
51.52/29.42	, f_1(1, 5) -> 4
51.52/29.42	, j_0(1, 1) -> 1
51.52/29.42	, g_0(1) -> 1
51.52/29.42	, g_1(4) -> 1
51.52/29.42	, g_1(4) -> 4
51.52/29.42	, k_0(1) -> 1
51.52/29.42	, k_1(1) -> 5
51.52/29.42	, h1_0(1, 1) -> 1
51.52/29.42	, h1_1(1, 1) -> 3
51.52/29.42	, h1_1(2, 1) -> 1
51.52/29.42	, h1_1(2, 1) -> 5
51.52/29.42	, h1_1(9, 1) -> 3
51.52/29.42	, h1_2(2, 1) -> 7
51.52/29.42	, h1_2(9, 1) -> 5
51.52/29.42	, h2_0(1, 1, 1) -> 1
51.52/29.42	, h2_1(2, 1, 3) -> 1
51.52/29.42	, h2_1(2, 1, 5) -> 1
51.52/29.42	, h2_1(2, 1, 5) -> 4
51.52/29.42	, h2_1(10, 1, 5) -> 4
51.52/29.42	, h2_2(6, 1, 5) -> 4
51.52/29.42	, h2_2(6, 1, 7) -> 4
51.52/29.42	, h2_2(8, 1, 5) -> 1
51.52/29.42	, h2_2(8, 1, 5) -> 4
51.52/29.43	, h2_2(8, 1, 7) -> 1
51.52/29.43	, h2_2(8, 1, 7) -> 4
51.52/29.43	, h2_2(9, 1, 5) -> 1
51.52/29.43	, h2_2(9, 1, 5) -> 4
51.52/29.43	, h2_2(9, 1, 7) -> 1
51.52/29.43	, h2_2(9, 1, 7) -> 4
51.52/29.43	, 0_0() -> 1
51.52/29.43	, 0_1() -> 2
51.52/29.43	, 0_2() -> 6
51.52/29.43	, s_0(1) -> 1
51.52/29.43	, s_1(1) -> 2
51.52/29.43	, s_1(2) -> 2
51.52/29.43	, s_1(6) -> 10
51.52/29.43	, s_1(8) -> 2
51.52/29.43	, s_1(9) -> 2
51.52/29.43	, s_1(10) -> 2
51.52/29.43	, s_2(2) -> 9
51.52/29.43	, s_2(6) -> 8
51.52/29.43	, s_2(8) -> 8
51.52/29.43	, s_2(9) -> 8
51.52/29.43	, s_2(10) -> 8
51.52/29.43	, i_0(1) -> 1
51.52/29.43	, h_0(1) -> 1 }
51.52/29.43	
51.52/29.43	Hurray, we answered YES(?,O(n^1))
51.52/29.46	EOF