Sorry, I edited a bunch and the point was that the ordering can matter due to references to the new value on the rhs or due to a loop. So
a' = a + b + 1 and b' = a + b + 1
should be
a' = a + b' + 1 and b' = a' + b + 1
Or alternatively they can have non-primed right hand sides but occur in a loop and you have the same problem even though the rhs's are at-free. A syntactic constraint won't work unless it includes "and also no loops in at-mentioning blocks" which... well, yeah, we know how to reason about NFAs :)
Sorry again, trying to make too many points with a single example
a' = a + b + 1 and b' = a + b + 1
should be
a' = a + b' + 1 and b' = a' + b + 1
Or alternatively they can have non-primed right hand sides but occur in a loop and you have the same problem even though the rhs's are at-free. A syntactic constraint won't work unless it includes "and also no loops in at-mentioning blocks" which... well, yeah, we know how to reason about NFAs :)
Sorry again, trying to make too many points with a single example