(VAR x y )
(RULES 
        active(f(x)) -> mark(x)
        top(active(c)) -> top(mark(c))
        top(mark(x)) -> top(check(x))
        check(f(x)) -> f(check(x))
        check(x) -> start(match(f(X), x))
        match(f(x), f(y)) -> f(match(x, y))
        match(X, x) -> proper(x)
        proper(c) -> ok(c)
        proper(f(x)) -> f(proper(x))
        f(ok(x)) -> ok(f(x))
        start(ok(x)) -> found(x)
        f(found(x)) -> found(f(x))
        top(found(x)) -> top(active(x))
        active(f(x)) -> f(active(x))
        f(mark(x)) -> mark(f(x))
        
)