(VAR x )
(RULES 
        R(x,B2) -> B2
        B1 ->= R(T,B1)
)