YES(?,O(n^1))
4.54/1.28	YES(?,O(n^1))
4.54/1.28	
4.54/1.28	We are left with following problem, upon which TcT provides the
4.54/1.28	certificate YES(?,O(n^1)).
4.54/1.28	
4.54/1.28	Strict Trs:
4.54/1.28	  { a__zeros() -> cons(0(), zeros())
4.54/1.28	  , a__zeros() -> zeros()
4.54/1.28	  , a__tail(X) -> tail(X)
4.54/1.28	  , a__tail(cons(X, XS)) -> mark(XS)
4.54/1.28	  , mark(cons(X1, X2)) -> cons(mark(X1), X2)
4.54/1.28	  , mark(0()) -> 0()
4.54/1.28	  , mark(zeros()) -> a__zeros()
4.54/1.28	  , mark(tail(X)) -> a__tail(mark(X)) }
4.54/1.28	Obligation:
4.54/1.28	  innermost runtime complexity
4.54/1.28	Answer:
4.54/1.28	  YES(?,O(n^1))
4.54/1.28	
4.54/1.28	The problem is match-bounded by 4. The enriched problem is
4.54/1.28	compatible with the following automaton.
4.54/1.28	{ a__zeros_0() -> 1
4.54/1.28	, a__zeros_1() -> 1
4.54/1.28	, a__zeros_2() -> 1
4.54/1.28	, a__zeros_3() -> 1
4.54/1.28	, cons_0(2, 2) -> 2
4.54/1.28	, cons_1(1, 2) -> 1
4.54/1.28	, cons_1(3, 4) -> 1
4.54/1.28	, cons_2(5, 6) -> 1
4.54/1.28	, cons_3(7, 8) -> 1
4.54/1.28	, cons_4(9, 10) -> 1
4.54/1.28	, 0_0() -> 2
4.54/1.28	, 0_1() -> 1
4.54/1.28	, 0_1() -> 3
4.54/1.28	, 0_2() -> 5
4.54/1.28	, 0_3() -> 7
4.54/1.28	, 0_4() -> 9
4.54/1.28	, zeros_0() -> 2
4.54/1.28	, zeros_1() -> 1
4.54/1.28	, zeros_1() -> 4
4.54/1.28	, zeros_2() -> 1
4.54/1.28	, zeros_2() -> 6
4.54/1.28	, zeros_3() -> 1
4.54/1.28	, zeros_3() -> 8
4.54/1.28	, zeros_4() -> 1
4.54/1.28	, zeros_4() -> 10
4.54/1.28	, a__tail_0(2) -> 1
4.54/1.28	, a__tail_1(1) -> 1
4.54/1.28	, mark_0(2) -> 1
4.54/1.28	, mark_1(2) -> 1
4.54/1.28	, mark_2(2) -> 1
4.54/1.28	, mark_2(4) -> 1
4.54/1.28	, mark_2(6) -> 1
4.54/1.28	, mark_2(8) -> 1
4.54/1.28	, mark_2(10) -> 1
4.54/1.28	, tail_0(2) -> 2
4.54/1.28	, tail_1(2) -> 1
4.54/1.28	, tail_2(1) -> 1 }
4.54/1.28	
4.54/1.28	Hurray, we answered YES(?,O(n^1))
4.54/1.29	EOF