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