\E m \in M : mState[m] = "anything state here"
Went back to HyperBook and looked at the Math section. Everything lines up. I used the examples as templates that I modified to make sense with my spec (of course that is questionable at this point).
However, after talking with you I did redesign the spec as I noticed I didn't have enough states. There needed to an idle period (both movant and respondent "idle") after each state.
Still...with all my effort, I've emerged empty handed. I've been working on this all day. I can get BothNotActiveInv to work just fine but anything that mention mState or M doesn't work.
I did use the "Evaluate Constant _expression_" section and found that if I put:
m \in M # "any state here" it came back TRUE (and if = to any state, FALSE).
That is the closet I got to something working. So it recognizes m \in M but on with any elements of the set of M.