(VAR x y )
(RULES 
        Tl(O(x),y) -> Wr(check(x),y)
        Tl(O(x),y) -> Wr(x,check(y))
        Tl(N(x),y) -> Wr(check(x),y)
        Tl(N(x),y) -> Wr(x,check(y))
        Tr(x,O(y)) -> Wl(check(x),y)
        Tr(x,O(y)) -> Wl(x,check(y))
        Tr(x,N(y)) -> Wl(check(x),y)
        Tr(x,N(y)) -> Wl(x,check(y))
        Tl(B,y) -> Wr(check(B),y)
        Tl(B,y) -> Wr(B,check(y))
        Tr(x,B) -> Wl(check(x),B)
        Tr(x,B) -> Wl(x,check(B))
        Tl(O(x),y) ->= Wl(check(x),y)
        Tl(O(x),y) ->= Wl(x,check(y))
        Tl(N(x),y) ->= Wl(check(x),y)
        Tl(N(x),y) ->= Wl(x,check(y))
        Tr(x,O(y)) ->= Wr(check(x),y)
        Tr(x,O(y)) ->= Wr(x,check(y))
        Tr(x,N(y)) ->= Wr(check(x),y)
        Tr(x,N(y)) ->= Wr(x,check(y))
        B ->= N(B)
        check(O(x)) ->= ok(O(x))
        Wl(ok(x),y) ->= Tl(x,y)
        Wl(x,ok(y)) ->= Tl(x,y)
        Wr(ok(x),y) ->= Tr(x,y)
        Wr(x,ok(y)) ->= Tr(x,y)
        check(O(x)) ->= O(check(x))
        check(N(x)) ->= N(check(x))
        O(ok(x)) ->= ok(O(x))
        N(ok(x)) ->= ok(N(x))
)