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