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