The temporal expression (if
ever occurs in a temporal sequence, it occurs only after the first occurrence of
) may be defined as
. Recall that
(
“waits for”
) is typically defined to mean
(either
repeats forever or
repeats until
occurs).
The following equivalence defines in terms of
. Note that
(eventually
) is short for
, and
holds in one state iff
occurs in the next state.
This post has been a shameless test of my new-found typesetting abilities.
Notice how TeX images with and without descending letters both line up correctly with the baseline. The trick is that I normalize the descent by including an extra \vert~ at the beginning of every inline expression, then trim it off.
You won't find that attention to detail anywhere else.