The transitions labeled by \(\)  abstractly represent the evaluation of
conditions (depending on which the branch of a conditional branching is chosen
or a loop is stopped). If our language contained boolean expressions, they
should actually be such, see [1]}. Notice that these transitions cannot
be contracted to a point in the semantics because it not be correct anymore:
for instance the semantics of \(¶a\)  would contain a loop.
