YES(?,O(n^1))
20.72/5.58	YES(?,O(n^1))
20.72/5.58	
20.72/5.58	We are left with following problem, upon which TcT provides the
20.72/5.58	certificate YES(?,O(n^1)).
20.72/5.58	
20.72/5.58	Strict Trs:
20.72/5.58	  { a__f(X) -> f(X)
20.72/5.58	  , a__f(0()) -> cons(0(), f(s(0())))
20.72/5.58	  , a__f(s(0())) -> a__f(a__p(s(0())))
20.72/5.58	  , a__p(X) -> p(X)
20.72/5.58	  , a__p(s(0())) -> 0()
20.72/5.58	  , mark(0()) -> 0()
20.72/5.58	  , mark(cons(X1, X2)) -> cons(mark(X1), X2)
20.72/5.58	  , mark(f(X)) -> a__f(mark(X))
20.72/5.58	  , mark(s(X)) -> s(mark(X))
20.72/5.58	  , mark(p(X)) -> a__p(mark(X)) }
20.72/5.58	Obligation:
20.72/5.58	  innermost runtime complexity
20.72/5.58	Answer:
20.72/5.58	  YES(?,O(n^1))
20.72/5.58	
20.72/5.58	The problem is match-bounded by 3. The enriched problem is
20.72/5.58	compatible with the following automaton.
20.72/5.58	{ a__f_0(2) -> 1
20.72/5.58	, a__f_1(7) -> 1
20.72/5.58	, a__f_1(8) -> 1
20.72/5.58	, a__f_1(8) -> 8
20.72/5.58	, a__f_2(11) -> 1
20.72/5.58	, a__f_2(11) -> 8
20.72/5.58	, 0_0() -> 2
20.72/5.58	, 0_1() -> 1
20.72/5.58	, 0_1() -> 3
20.72/5.58	, 0_1() -> 6
20.72/5.58	, 0_1() -> 8
20.72/5.58	, 0_2() -> 1
20.72/5.58	, 0_2() -> 7
20.72/5.58	, 0_2() -> 8
20.72/5.58	, 0_3() -> 11
20.72/5.58	, cons_0(2, 2) -> 2
20.72/5.58	, cons_1(3, 4) -> 1
20.72/5.58	, cons_1(8, 2) -> 1
20.72/5.58	, cons_1(8, 2) -> 8
20.72/5.58	, cons_2(7, 9) -> 1
20.72/5.58	, cons_2(7, 9) -> 8
20.72/5.58	, cons_3(11, 12) -> 1
20.72/5.58	, cons_3(11, 12) -> 8
20.72/5.58	, f_0(2) -> 2
20.72/5.58	, f_1(2) -> 1
20.72/5.58	, f_1(5) -> 4
20.72/5.58	, f_2(7) -> 1
20.72/5.58	, f_2(8) -> 1
20.72/5.58	, f_2(8) -> 8
20.72/5.58	, f_2(10) -> 9
20.72/5.58	, f_3(11) -> 1
20.72/5.58	, f_3(11) -> 8
20.72/5.58	, f_3(13) -> 12
20.72/5.58	, s_0(2) -> 2
20.72/5.58	, s_1(6) -> 5
20.72/5.58	, s_1(8) -> 1
20.72/5.58	, s_1(8) -> 8
20.72/5.58	, s_2(7) -> 10
20.72/5.58	, s_3(11) -> 13
20.72/5.58	, a__p_0(2) -> 1
20.72/5.58	, a__p_1(5) -> 7
20.72/5.58	, a__p_1(8) -> 1
20.72/5.58	, a__p_1(8) -> 8
20.72/5.58	, a__p_2(10) -> 11
20.72/5.58	, mark_0(2) -> 1
20.72/5.58	, mark_1(2) -> 8
20.72/5.58	, p_0(2) -> 2
20.72/5.58	, p_1(2) -> 1
20.72/5.58	, p_2(5) -> 7
20.72/5.58	, p_2(8) -> 1
20.72/5.58	, p_2(8) -> 8
20.72/5.58	, p_3(10) -> 11 }
20.72/5.58	
20.72/5.58	Hurray, we answered YES(?,O(n^1))
20.95/5.61	EOF