It's the lemma I challenge, not the common case on certain of today's architectures. The use of the word "must" implies ∀, which is plainly not the case.