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