Yo, author of PT here. I'd say that given your use case, the book _probably_ won't be that useful to you. Among other things, I intentionally avoided teaching r

Yo, author of PT here. I'd say that given your use case, the book _probably_ won't be that useful to you. Among other things, I intentionally avoided teaching refinements. You'd probably be happier starting with either _Specifying Systems_[1] or the _Hyperbook_[2], particularly the latter's proof track. If you still have access to a copy of PT, I'd recommend reading chapter 7 (specifying and implementing algorithms) to see if that helps at all. The code is in PlusCal, but the general approach transfers to pure TLA+. [1]: https://lamport.azurewebsites.net/tla/book.html https://lamport.azurewebsites.net/tla/book.html [2]: https://lamport.azurewebsites.net/tla/hyperbook.html https://lamport.azurewebsites.net/tla/hyperbook.html EDIT: in terms of writing it as TLA+, you probably want something like EXTENDS Sequences IndicesBetween(X, A, B) == \A i \in 1..Len(X): /\ A[i] <= X[i] /\ B[i] >= X[i] Assuming `Len(X) <= Min(Len(A), Len(B))`.