Termination w.r.t. Q of the given QTRS could not be shown:

(0) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

active(f(a, X, X)) → mark(f(X, b, b))
active(b) → mark(a)
active(f(X1, X2, X3)) → f(X1, active(X2), X3)
f(X1, mark(X2), X3) → mark(f(X1, X2, X3))
proper(f(X1, X2, X3)) → f(proper(X1), proper(X2), proper(X3))
proper(a) → ok(a)
proper(b) → ok(b)
f(ok(X1), ok(X2), ok(X3)) → ok(f(X1, X2, X3))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

Q is empty.