My mistake was not realizing that Next is a full relation on the entire universe of states (I thought that it was a "constructive" partial relation), that for _every_ two states s and t, must determine whether t can be a next state of s or not. Then, on top of that, there's TLC's evaluation rules about the first encounter with a primed variable that must uniquely determine its value, and therefore cannot be a negation of the sort ~(x' = ...).Do I have it right?