YES

TRS:

  active(2nd(cons1(X,cons(Y,Z)))) -> mark(Y)
  active(2nd(cons(X,X1))) -> mark(2nd(cons1(X,X1)))
  active(from(X)) -> mark(cons(X,from(s(X))))
  active(2nd(X)) -> 2nd(active(X))
  active(cons(X1,X2)) -> cons(active(X1),X2)
  active(from(X)) -> from(active(X))
  active(s(X)) -> s(active(X))
  active(cons1(X1,X2)) -> cons1(active(X1),X2)
  active(cons1(X1,X2)) -> cons1(X1,active(X2))
  2nd(mark(X)) -> mark(2nd(X))
  cons(mark(X1),X2) -> mark(cons(X1,X2))
  from(mark(X)) -> mark(from(X))
  s(mark(X)) -> mark(s(X))
  cons1(mark(X1),X2) -> mark(cons1(X1,X2))
  cons1(X1,mark(X2)) -> mark(cons1(X1,X2))
  proper(2nd(X)) -> 2nd(proper(X))
  proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
  proper(from(X)) -> from(proper(X))
  proper(s(X)) -> s(proper(X))
  proper(cons1(X1,X2)) -> cons1(proper(X1),proper(X2))
  2nd(ok(X)) -> ok(2nd(X))
  cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
  from(ok(X)) -> ok(from(X))
  s(ok(X)) -> ok(s(X))
  cons1(ok(X1),ok(X2)) -> ok(cons1(X1,X2))
  top(mark(X)) -> top(proper(X))
  top(ok(X)) -> top(active(X))

linear polynomial interpretations on N:

  active_A(x1) = x1 + 6
  active#_A(x1) = 5
  2nd_A(x1) = x1
  2nd#_A(x1) = 4
  cons1_A(x1,x2) = x1 + x2
  cons1#_A(x1,x2) = 3
  cons_A(x1,x2) = x1 + x2
  cons#_A(x1,x2) = 2
  mark_A(x1) = 6
  mark#_A(x1) = 1
  from_A(x1) = x1
  from#_A(x1) = 4
  s_A(x1) = x1
  s#_A(x1) = 3
  proper_A(x1) = 0
  proper#_A(x1) = 5
  ok_A(x1) = x1 + 7
  ok#_A(x1) = 1
  top_A(x1) = x1
  top#_A(x1) = x1

precedence:

  ok > top > active = proper > 2nd > cons1 = from > cons = s > mark