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