In reply to Chinky:
The implication operator is not “bidirectional” in the sense that the implication is still satified when size == size_64 and cmd != B. The constraint is bidirectional in the choice of the random value for size affects the choice for cmd and vice versa. A better choice of words might be “simultaneously”.
What this means is if you pick a distribution for size, or constrain it such that choosing size==size_64 occurs only 1% of the time, there’s no way you could choose cmd==B more than 1% of the time as well.