AX \/ AY is the
next-state
action
of formula
Phi.
It is the disjunction of the two
actions
AX
and
AY.
Thus, an
AX \/ AY
step
is either an
AX
step
or an
AY
step.
You are in Explanation Mode Click here for Definition Mode