YES(?,O(n^1))
1088.38/297.02	YES(?,O(n^1))
1088.38/297.02	
1088.38/297.02	We are left with following problem, upon which TcT provides the
1088.38/297.02	certificate YES(?,O(n^1)).
1088.38/297.02	
1088.38/297.02	Strict Trs:
1088.38/297.02	  { active(f(x)) -> mark(f(f(x)))
1088.38/297.02	  , f(active(x)) -> active(f(x))
1088.38/297.02	  , f(mark(x)) -> mark(f(x))
1088.38/297.02	  , f(no(x)) -> no(f(x))
1088.38/297.02	  , chk(no(f(x))) ->
1088.38/297.02	    f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)))
1088.38/297.02	  , chk(no(c())) -> active(c())
1088.38/297.02	  , mat(f(x), f(y())) -> f(mat(x, y()))
1088.38/297.02	  , mat(f(x), c()) -> no(c())
1088.38/297.02	  , tp(mark(x)) ->
1088.38/297.02	    tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x))) }
1088.38/297.02	Obligation:
1088.38/297.02	  innermost runtime complexity
1088.38/297.02	Answer:
1088.38/297.02	  YES(?,O(n^1))
1088.38/297.02	
1088.38/297.02	The problem is match-bounded by 2. The enriched problem is
1088.38/297.02	compatible with the following automaton.
1088.38/297.02	{ active_0(3) -> 1
1088.38/297.02	, active_0(5) -> 1
1088.38/297.02	, active_0(7) -> 1
1088.38/297.02	, active_0(8) -> 1
1088.38/297.02	, active_0(9) -> 1
1088.38/297.02	, active_1(12) -> 4
1088.38/297.02	, active_2(26) -> 13
1088.38/297.02	, f_0(3) -> 2
1088.38/297.02	, f_0(5) -> 2
1088.38/297.02	, f_0(7) -> 2
1088.38/297.02	, f_0(8) -> 2
1088.38/297.02	, f_0(9) -> 2
1088.38/297.02	, f_1(3) -> 11
1088.38/297.02	, f_1(5) -> 11
1088.38/297.02	, f_1(7) -> 11
1088.38/297.02	, f_1(8) -> 11
1088.38/297.02	, f_1(9) -> 11
1088.38/297.02	, f_1(16) -> 15
1088.38/297.02	, f_1(17) -> 16
1088.38/297.02	, f_1(18) -> 17
1088.38/297.02	, f_1(19) -> 18
1088.38/297.02	, f_1(20) -> 19
1088.38/297.02	, f_1(21) -> 20
1088.38/297.02	, f_1(22) -> 21
1088.38/297.02	, f_1(23) -> 22
1088.38/297.02	, f_1(24) -> 23
1088.38/297.02	, f_1(25) -> 24
1088.38/297.02	, mark_0(3) -> 3
1088.38/297.02	, mark_0(5) -> 3
1088.38/297.02	, mark_0(7) -> 3
1088.38/297.02	, mark_0(8) -> 3
1088.38/297.02	, mark_0(9) -> 3
1088.38/297.02	, mark_1(11) -> 2
1088.38/297.02	, mark_1(11) -> 11
1088.38/297.02	, chk_0(3) -> 4
1088.38/297.02	, chk_0(5) -> 4
1088.38/297.02	, chk_0(7) -> 4
1088.38/297.02	, chk_0(8) -> 4
1088.38/297.02	, chk_0(9) -> 4
1088.38/297.02	, chk_1(14) -> 13
1088.38/297.02	, no_0(3) -> 5
1088.38/297.02	, no_0(5) -> 5
1088.38/297.02	, no_0(7) -> 5
1088.38/297.02	, no_0(8) -> 5
1088.38/297.02	, no_0(9) -> 5
1088.38/297.02	, no_1(11) -> 2
1088.38/297.02	, no_1(11) -> 11
1088.38/297.02	, no_1(12) -> 14
1088.38/297.02	, mat_0(3, 3) -> 6
1088.38/297.02	, mat_0(3, 5) -> 6
1088.38/297.02	, mat_0(3, 7) -> 6
1088.38/297.02	, mat_0(3, 8) -> 6
1088.38/297.02	, mat_0(3, 9) -> 6
1088.38/297.02	, mat_0(5, 3) -> 6
1088.38/297.02	, mat_0(5, 5) -> 6
1088.38/297.02	, mat_0(5, 7) -> 6
1088.38/297.02	, mat_0(5, 8) -> 6
1088.38/297.02	, mat_0(5, 9) -> 6
1088.38/297.02	, mat_0(7, 3) -> 6
1088.38/297.02	, mat_0(7, 5) -> 6
1088.38/297.02	, mat_0(7, 7) -> 6
1088.38/297.02	, mat_0(7, 8) -> 6
1088.38/297.02	, mat_0(7, 9) -> 6
1088.38/297.02	, mat_0(8, 3) -> 6
1088.38/297.02	, mat_0(8, 5) -> 6
1088.38/297.02	, mat_0(8, 7) -> 6
1088.38/297.02	, mat_0(8, 8) -> 6
1088.38/297.02	, mat_0(8, 9) -> 6
1088.38/297.02	, mat_0(9, 3) -> 6
1088.38/297.02	, mat_0(9, 5) -> 6
1088.38/297.02	, mat_0(9, 7) -> 6
1088.38/297.02	, mat_0(9, 8) -> 6
1088.38/297.02	, mat_0(9, 9) -> 6
1088.38/297.02	, mat_1(15, 3) -> 14
1088.38/297.02	, mat_1(15, 5) -> 14
1088.38/297.02	, mat_1(15, 7) -> 14
1088.38/297.02	, mat_1(15, 8) -> 14
1088.38/297.02	, mat_1(15, 9) -> 14
1088.38/297.02	, X_0() -> 7
1088.38/297.02	, X_1() -> 25
1088.38/297.02	, y_0() -> 8
1088.38/297.02	, c_0() -> 9
1088.38/297.02	, c_1() -> 12
1088.38/297.02	, c_2() -> 26
1088.38/297.02	, tp_0(3) -> 10
1088.38/297.02	, tp_0(5) -> 10
1088.38/297.02	, tp_0(7) -> 10
1088.38/297.02	, tp_0(8) -> 10
1088.38/297.02	, tp_0(9) -> 10
1088.38/297.02	, tp_1(13) -> 10 }
1088.38/297.02	
1088.38/297.02	Hurray, we answered YES(?,O(n^1))
1088.61/297.27	EOF