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