YES

TRS:

  active(g(X)) -> mark(h(X))
  active(c()) -> mark(d())
  active(h(d())) -> mark(g(c()))
  proper(g(X)) -> g(proper(X))
  proper(h(X)) -> h(proper(X))
  proper(c()) -> ok(c())
  proper(d()) -> ok(d())
  g(ok(X)) -> ok(g(X))
  h(ok(X)) -> ok(h(X))
  top(mark(X)) -> top(proper(X))
  top(ok(X)) -> top(active(X))

linear polynomial interpretations on N:

  active_A(x1) = x1 + 10
  active#_A(x1) = 1
  g_A(x1) = x1 + 9
  g#_A(x1) = x1 + 11
  mark_A(x1) = x1 + 2
  mark#_A(x1) = x1 + 5
  h_A(x1) = x1 + 5
  h#_A(x1) = x1 + 7
  c_A = 1
  c#_A = 15
  d_A = 9
  d#_A = 0
  proper_A(x1) = x1 + 1
  proper#_A(x1) = x1 + 4
  ok_A(x1) = x1 + 1
  ok#_A(x1) = x1 + 2
  top_A(x1) = 0
  top#_A(x1) = 3

precedence:

  d > g > ok > top > active > mark > proper > h > c