YES(?,O(n^1))
929.23/297.10	YES(?,O(n^1))
929.23/297.10	
929.23/297.10	We are left with following problem, upon which TcT provides the
929.23/297.10	certificate YES(?,O(n^1)).
929.23/297.10	
929.23/297.10	Strict Trs:
929.23/297.10	  { active(f(f(a()))) -> mark(f(g(f(a()))))
929.23/297.10	  , active(g(X)) -> g(active(X))
929.23/297.10	  , f(ok(X)) -> ok(f(X))
929.23/297.10	  , g(mark(X)) -> mark(g(X))
929.23/297.10	  , g(ok(X)) -> ok(g(X))
929.23/297.10	  , proper(f(X)) -> f(proper(X))
929.23/297.10	  , proper(a()) -> ok(a())
929.23/297.10	  , proper(g(X)) -> g(proper(X))
929.23/297.10	  , top(mark(X)) -> top(proper(X))
929.23/297.10	  , top(ok(X)) -> top(active(X)) }
929.23/297.10	Obligation:
929.23/297.10	  runtime complexity
929.23/297.10	Answer:
929.23/297.10	  YES(?,O(n^1))
929.23/297.10	
929.23/297.10	The problem is match-bounded by 2. The enriched problem is
929.23/297.10	compatible with the following automaton.
929.23/297.10	{ active_0(3) -> 1
929.23/297.10	, active_0(4) -> 1
929.23/297.10	, active_0(7) -> 1
929.23/297.10	, active_1(3) -> 12
929.23/297.10	, active_1(4) -> 12
929.23/297.10	, active_1(7) -> 12
929.23/297.10	, active_2(11) -> 13
929.23/297.10	, f_0(3) -> 2
929.23/297.10	, f_0(4) -> 2
929.23/297.10	, f_0(7) -> 2
929.23/297.10	, f_1(3) -> 9
929.23/297.10	, f_1(4) -> 9
929.23/297.10	, f_1(7) -> 9
929.23/297.10	, a_0() -> 3
929.23/297.10	, a_1() -> 11
929.23/297.10	, mark_0(3) -> 4
929.23/297.10	, mark_0(4) -> 4
929.23/297.10	, mark_0(7) -> 4
929.23/297.10	, mark_1(10) -> 5
929.23/297.10	, mark_1(10) -> 10
929.23/297.10	, g_0(3) -> 5
929.23/297.10	, g_0(4) -> 5
929.23/297.10	, g_0(7) -> 5
929.23/297.10	, g_1(3) -> 10
929.23/297.10	, g_1(4) -> 10
929.23/297.10	, g_1(7) -> 10
929.23/297.10	, proper_0(3) -> 6
929.23/297.10	, proper_0(4) -> 6
929.23/297.10	, proper_0(7) -> 6
929.23/297.10	, proper_1(3) -> 12
929.23/297.10	, proper_1(4) -> 12
929.23/297.10	, proper_1(7) -> 12
929.23/297.10	, ok_0(3) -> 7
929.23/297.10	, ok_0(4) -> 7
929.23/297.10	, ok_0(7) -> 7
929.23/297.10	, ok_1(9) -> 2
929.23/297.10	, ok_1(9) -> 9
929.23/297.10	, ok_1(10) -> 5
929.23/297.10	, ok_1(10) -> 10
929.23/297.10	, ok_1(11) -> 6
929.23/297.10	, ok_1(11) -> 12
929.23/297.10	, top_0(3) -> 8
929.23/297.10	, top_0(4) -> 8
929.23/297.10	, top_0(7) -> 8
929.23/297.10	, top_1(12) -> 8
929.23/297.10	, top_2(13) -> 8 }
929.23/297.10	
929.23/297.10	Hurray, we answered YES(?,O(n^1))
929.23/297.16	EOF