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