(VAR X X1 X2 X3)
(RULES 
active(f(b,X,c)) -> mark(f(X,c,X))
active(c) -> mark(b)
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(b) -> ok(b)
proper(c) -> ok(c)
f(ok(X1),ok(X2),ok(X3)) -> ok(f(X1,X2,X3))
top(mark(X)) -> top(proper(X))
top(ok(X)) -> top(active(X))
)