INVARIANT NotStalemate SPECIFICATION Spec