Patience: introducing a ghost variable
patience: added ghost state
patience: first part of invariant proved