The invariant form would be something like: for any program state, there is eventually a state that will be reached that contains the ordered set containing inp

The invariant form would be something like: for any program state, there is eventually a state that will be reached that contains the ordered set containing input elements. My phrasing is rough, but it is an invariant that can be expressed by TLA+