>>16
This tracks to me, and in both cases the additional element simplifies to (\exists x \in S(w) : x != abort). While we've been discussing I've been reread to where I was before my hiatus. I haven't run into any more confusion, and in fact I feel I have a pretty solid understanding now. Thanks everyone!
Beyond the actual knowledge of the subject the main lessons learned were to pay special attention to deviations from the norm, such as the fact that a non-deterministic mechanism clearly isn't a function but a multifunction. Probably also trying explicitly to model things as they are instead of as I would like them to be (or not at all), would help.