Stephan, you are correct that there is no mention of motion in case. But this is due to me trying to get one thing working at a time. I was stuck on motions when next function wouldn't work. (I had MNext == mState = \E m \in M : MotionResponse(m) vs MNext == \E m \in M : MotionResponse(m). Was getting an error about nested arg. Didn't even notice I put "mState =" into the equation until after...ummm...2-3hrs of experimenting.)
So I'm just moving slowly as I attempt to put a spec together from scratch vs the ones from the video and books. Slow frustrating process as is the case with programming and now TLA^+.
Now that I have it working, I'm going to fill out the rest of the spec.
Lastly, yes, your comment helps. I'm writing down everything that seems to be unclear or not clearly stated from my perspective to create a help doc for those of use who need a little more hand holding until we can walk on our own.