In invariants it's awkward writing s(x) and s(y) all the time since s is universally quantified. So more typically you'll see invariants expressed directly in terms of the state variables. For the DivergingCounter, you'd more likely see its invariant in this more readable format:
We use this syntactic sugar
in the pre- and post-conditions already.