0 QTRS
active(c) → mark(f(g(c))) active(f(g(X))) → mark(g(X)) proper(c) → ok(c) proper(f(X)) → f(proper(X)) proper(g(X)) → g(proper(X)) f(ok(X)) → ok(f(X)) g(ok(X)) → ok(g(X)) top(mark(X)) → top(proper(X)) top(ok(X)) → top(active(X))