YES(?,O(n^1))
35.72/12.76	YES(?,O(n^1))
35.72/12.76	
35.72/12.76	We are left with following problem, upon which TcT provides the
35.72/12.76	certificate YES(?,O(n^1)).
35.72/12.76	
35.72/12.76	Strict Trs:
35.72/12.76	  { b(x, y) -> c(a(c(y), a(0(), x)))
35.72/12.76	  , a(y, x) -> y
35.72/12.76	  , a(y, c(b(a(0(), x), 0()))) -> b(a(c(b(0(), y)), x), 0()) }
35.72/12.76	Obligation:
35.72/12.76	  runtime complexity
35.72/12.76	Answer:
35.72/12.76	  YES(?,O(n^1))
35.72/12.76	
35.72/12.76	The problem is match-bounded by 1. The enriched problem is
35.72/12.76	compatible with the following automaton.
35.72/12.76	{ b_0(2, 2) -> 1
35.72/12.76	, b_0(2, 4) -> 1
35.72/12.76	, b_0(4, 2) -> 1
35.72/12.76	, b_0(4, 4) -> 1
35.72/12.76	, c_0(2) -> 2
35.72/12.76	, c_0(2) -> 3
35.72/12.76	, c_0(4) -> 2
35.72/12.76	, c_0(4) -> 3
35.72/12.76	, c_1(2) -> 5
35.72/12.76	, c_1(2) -> 6
35.72/12.76	, c_1(4) -> 5
35.72/12.76	, c_1(4) -> 6
35.72/12.76	, c_1(5) -> 1
35.72/12.76	, a_0(2, 2) -> 3
35.72/12.76	, a_0(2, 4) -> 3
35.72/12.76	, a_0(4, 2) -> 3
35.72/12.76	, a_0(4, 4) -> 3
35.72/12.76	, a_1(6, 7) -> 5
35.72/12.76	, a_1(8, 2) -> 7
35.72/12.76	, a_1(8, 4) -> 7
35.72/12.76	, 0_0() -> 3
35.72/12.76	, 0_0() -> 4
35.72/12.76	, 0_1() -> 7
35.72/12.76	, 0_1() -> 8 }
35.72/12.76	
35.72/12.76	Hurray, we answered YES(?,O(n^1))
35.72/12.79	EOF