YES(?,O(n^1))
839.21/262.48	YES(?,O(n^1))
839.21/262.48	
839.21/262.48	We are left with following problem, upon which TcT provides the
839.21/262.48	certificate YES(?,O(n^1)).
839.21/262.48	
839.21/262.48	Strict Trs:
839.21/262.48	  { active(f(x)) -> f(active(x))
839.21/262.48	  , active(f(x)) -> mark(x)
839.21/262.48	  , f(mark(x)) -> mark(f(x))
839.21/262.48	  , f(ok(x)) -> ok(f(x))
839.21/262.48	  , f(found(x)) -> found(f(x))
839.21/262.48	  , top(active(c())) -> top(mark(c()))
839.21/262.48	  , top(mark(x)) -> top(check(x))
839.21/262.48	  , top(found(x)) -> top(active(x))
839.21/262.48	  , check(x) -> start(match(f(X()), x))
839.21/262.48	  , check(f(x)) -> f(check(x))
839.21/262.48	  , start(ok(x)) -> found(x)
839.21/262.48	  , match(f(x), f(y)) -> f(match(x, y))
839.21/262.48	  , match(X(), x) -> proper(x)
839.21/262.48	  , proper(f(x)) -> f(proper(x))
839.21/262.48	  , proper(c()) -> ok(c()) }
839.21/262.48	Obligation:
839.21/262.48	  innermost runtime complexity
839.21/262.48	Answer:
839.21/262.48	  YES(?,O(n^1))
839.21/262.48	
839.21/262.48	The problem is match-bounded by 3. The enriched problem is
839.21/262.48	compatible with the following automaton.
839.21/262.48	{ active_0(3) -> 1
839.21/262.48	, active_0(5) -> 1
839.21/262.48	, active_0(9) -> 1
839.21/262.48	, active_0(11) -> 1
839.21/262.48	, active_0(12) -> 1
839.21/262.48	, active_1(3) -> 14
839.21/262.48	, active_1(5) -> 14
839.21/262.48	, active_1(9) -> 14
839.21/262.48	, active_1(11) -> 14
839.21/262.48	, active_1(12) -> 14
839.21/262.48	, f_0(3) -> 2
839.21/262.48	, f_0(5) -> 2
839.21/262.48	, f_0(9) -> 2
839.21/262.48	, f_0(11) -> 2
839.21/262.48	, f_0(12) -> 2
839.21/262.48	, f_1(3) -> 13
839.21/262.48	, f_1(5) -> 13
839.21/262.48	, f_1(9) -> 13
839.21/262.48	, f_1(11) -> 13
839.21/262.48	, f_1(12) -> 13
839.21/262.48	, f_1(17) -> 16
839.21/262.48	, f_2(20) -> 19
839.21/262.48	, f_3(25) -> 24
839.21/262.48	, mark_0(3) -> 3
839.21/262.48	, mark_0(5) -> 3
839.21/262.48	, mark_0(9) -> 3
839.21/262.48	, mark_0(11) -> 3
839.21/262.48	, mark_0(12) -> 3
839.21/262.48	, mark_1(13) -> 2
839.21/262.48	, mark_1(13) -> 13
839.21/262.48	, mark_1(21) -> 14
839.21/262.48	, top_0(3) -> 4
839.21/262.48	, top_0(5) -> 4
839.21/262.48	, top_0(9) -> 4
839.21/262.48	, top_0(11) -> 4
839.21/262.48	, top_0(12) -> 4
839.21/262.48	, top_1(14) -> 4
839.21/262.48	, top_2(22) -> 4
839.21/262.48	, c_0() -> 5
839.21/262.48	, c_1() -> 21
839.21/262.48	, check_0(3) -> 6
839.21/262.48	, check_0(5) -> 6
839.21/262.48	, check_0(9) -> 6
839.21/262.48	, check_0(11) -> 6
839.21/262.48	, check_0(12) -> 6
839.21/262.48	, check_1(3) -> 14
839.21/262.48	, check_1(5) -> 14
839.21/262.48	, check_1(9) -> 14
839.21/262.48	, check_1(11) -> 14
839.21/262.48	, check_1(12) -> 14
839.21/262.48	, check_2(21) -> 22
839.21/262.48	, start_0(3) -> 7
839.21/262.48	, start_0(5) -> 7
839.21/262.48	, start_0(9) -> 7
839.21/262.48	, start_0(11) -> 7
839.21/262.48	, start_0(12) -> 7
839.21/262.48	, start_1(15) -> 6
839.21/262.48	, start_2(18) -> 14
839.21/262.48	, start_3(23) -> 22
839.21/262.48	, match_0(3, 3) -> 8
839.21/262.48	, match_0(3, 5) -> 8
839.21/262.48	, match_0(3, 9) -> 8
839.21/262.48	, match_0(3, 11) -> 8
839.21/262.48	, match_0(3, 12) -> 8
839.21/262.48	, match_0(5, 3) -> 8
839.21/262.48	, match_0(5, 5) -> 8
839.21/262.48	, match_0(5, 9) -> 8
839.21/262.48	, match_0(5, 11) -> 8
839.21/262.48	, match_0(5, 12) -> 8
839.21/262.48	, match_0(9, 3) -> 8
839.21/262.48	, match_0(9, 5) -> 8
839.21/262.48	, match_0(9, 9) -> 8
839.21/262.48	, match_0(9, 11) -> 8
839.21/262.48	, match_0(9, 12) -> 8
839.21/262.48	, match_0(11, 3) -> 8
839.21/262.48	, match_0(11, 5) -> 8
839.21/262.48	, match_0(11, 9) -> 8
839.21/262.48	, match_0(11, 11) -> 8
839.21/262.48	, match_0(11, 12) -> 8
839.21/262.48	, match_0(12, 3) -> 8
839.21/262.48	, match_0(12, 5) -> 8
839.21/262.48	, match_0(12, 9) -> 8
839.21/262.48	, match_0(12, 11) -> 8
839.21/262.48	, match_0(12, 12) -> 8
839.21/262.48	, match_1(16, 3) -> 15
839.21/262.48	, match_1(16, 5) -> 15
839.21/262.48	, match_1(16, 9) -> 15
839.21/262.48	, match_1(16, 11) -> 15
839.21/262.48	, match_1(16, 12) -> 15
839.21/262.48	, match_2(19, 3) -> 18
839.21/262.48	, match_2(19, 5) -> 18
839.21/262.48	, match_2(19, 9) -> 18
839.21/262.48	, match_2(19, 11) -> 18
839.21/262.48	, match_2(19, 12) -> 18
839.21/262.48	, match_3(24, 21) -> 23
839.21/262.48	, X_0() -> 9
839.21/262.48	, X_1() -> 17
839.21/262.48	, X_2() -> 20
839.21/262.48	, X_3() -> 25
839.21/262.48	, proper_0(3) -> 10
839.21/262.48	, proper_0(5) -> 10
839.21/262.48	, proper_0(9) -> 10
839.21/262.48	, proper_0(11) -> 10
839.21/262.48	, proper_0(12) -> 10
839.21/262.48	, proper_1(3) -> 8
839.21/262.48	, proper_1(5) -> 8
839.21/262.48	, proper_1(9) -> 8
839.21/262.48	, proper_1(11) -> 8
839.21/262.48	, proper_1(12) -> 8
839.21/262.48	, ok_0(3) -> 11
839.21/262.48	, ok_0(5) -> 11
839.21/262.48	, ok_0(9) -> 11
839.21/262.48	, ok_0(11) -> 11
839.21/262.48	, ok_0(12) -> 11
839.21/262.48	, ok_1(13) -> 2
839.21/262.48	, ok_1(13) -> 13
839.21/262.48	, ok_1(21) -> 8
839.21/262.48	, ok_1(21) -> 10
839.21/262.48	, found_0(3) -> 12
839.21/262.48	, found_0(5) -> 12
839.21/262.48	, found_0(9) -> 12
839.21/262.48	, found_0(11) -> 12
839.21/262.48	, found_0(12) -> 12
839.21/262.48	, found_1(3) -> 7
839.21/262.48	, found_1(5) -> 7
839.21/262.48	, found_1(9) -> 7
839.21/262.48	, found_1(11) -> 7
839.21/262.48	, found_1(12) -> 7
839.21/262.48	, found_1(13) -> 2
839.21/262.48	, found_1(13) -> 13 }
839.21/262.48	
839.21/262.48	Hurray, we answered YES(?,O(n^1))
839.21/262.48	EOF