(VAR x y )
(RULES 
        top(ok(queue(old(x),bot))) -> top(check(queue(x,bot)))
        top(ok(queue(new(x),bot))) -> top(check(queue(x,bot)))
        top(ok(queue(bot,old(x)))) -> top(check(queue(bot,x)))
        top(ok(queue(bot,new(x)))) -> top(check(queue(bot,x)))
        top(ok(queue(old(x),old(y)))) -> top(check(queue(x,y)))
        top(ok(queue(old(x),new(y)))) -> top(check(queue(x,y)))
        top(ok(queue(new(x),old(y)))) -> top(check(queue(x,y)))
        top(ok(queue(new(x),new(y)))) -> top(check(queue(x,y)))
        top(ok(queue(old(x),y))) ->= top(check(queue(x,y)))
        top(ok(queue(new(x),y))) ->= top(check(queue(x,y)))
        bot ->= new(bot)
        check(old(x)) ->= ok(old(x))
        check(new(x)) ->= new(check(x))
        check(queue(x,y)) ->= queue(check(x),y)
        check(queue(x,y)) ->= queue(x,check(y))
        old(ok(x)) ->= ok(old(x))
        new(ok(x)) ->= ok(new(x))
        queue(ok(x),y) ->= ok(queue(x,y))
        queue(x,ok(y)) ->= ok(queue(x,y))
)