The expression &lt;α&gt;B means that there is an execution of α that terminates in a state that satisfies B. Moreover, if α is deterministic, this possible terminating execution is the unique execution of α. Thus, if one first manages to prove that a program is deterministic, this trick works well enough to prove its total correctness.