Investigating Preconditions
Z contains a precondition operator pre which makes a schema out of a schema by hiding all the after and output variables of the given schema.
Therefore, since Enter1 is a schema then so is PreEnter1
Given a schema S, PreS indicates those states on which the operation S can be successfully carried out. So PreEnter1 tells us on which states Enter1 can be performed.
Precondition schemas can usually be simplified and their existential quantifier removed.