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