YES(?,O(n^1))
13.66/6.85	YES(?,O(n^1))
13.66/6.85	
13.66/6.85	We are left with following problem, upon which TcT provides the
13.66/6.85	certificate YES(?,O(n^1)).
13.66/6.85	
13.66/6.85	Strict Trs:
13.66/6.85	  { h(x, c(y, z)) -> h(c(s(y), x), z)
13.66/6.85	  , h(c(s(x), c(s(0()), y)), z) -> h(y, c(s(0()), c(x, z))) }
13.66/6.85	Obligation:
13.66/6.85	  derivational complexity
13.66/6.85	Answer:
13.66/6.85	  YES(?,O(n^1))
13.66/6.85	
13.66/6.85	The problem is match-bounded by 2. The enriched problem is
13.66/6.85	compatible with the following automaton.
13.66/6.85	{ h_0(1, 1) -> 1
13.66/6.85	, h_1(1, 4) -> 1
13.66/6.85	, h_1(2, 1) -> 1
13.66/6.85	, h_1(2, 4) -> 1
13.66/6.85	, h_1(8, 4) -> 1
13.66/6.85	, h_1(10, 4) -> 1
13.66/6.85	, h_2(8, 4) -> 1
13.66/6.85	, h_2(8, 6) -> 1
13.66/6.85	, h_2(10, 1) -> 1
13.66/6.85	, h_2(10, 4) -> 1
13.66/6.85	, c_0(1, 1) -> 1
13.66/6.85	, c_1(1, 1) -> 6
13.66/6.85	, c_1(1, 4) -> 6
13.66/6.85	, c_1(3, 1) -> 2
13.66/6.85	, c_1(3, 2) -> 2
13.66/6.85	, c_1(3, 10) -> 2
13.66/6.85	, c_1(5, 4) -> 4
13.66/6.85	, c_1(5, 6) -> 4
13.66/6.85	, c_2(9, 1) -> 8
13.66/6.85	, c_2(9, 2) -> 8
13.66/6.85	, c_2(9, 8) -> 8
13.66/6.85	, c_2(9, 10) -> 8
13.66/6.85	, c_2(11, 8) -> 10
13.66/6.85	, s_0(1) -> 1
13.66/6.85	, s_1(1) -> 3
13.66/6.85	, s_1(7) -> 5
13.66/6.85	, s_2(1) -> 11
13.66/6.85	, s_2(5) -> 9
13.66/6.85	, 0_0() -> 1
13.66/6.85	, 0_1() -> 7 }
13.66/6.85	
13.66/6.85	Hurray, we answered YES(?,O(n^1))
13.66/6.86	EOF