For any 
 <A HREF = "action.html">action</A>
<CODE> A </CODE> and 
 <A HREF = "state-function.html">state function</A>
<CODE> v </CODE>, the
 <A HREF = "action.html">action</A>
<PRE>
  [A]
     v
</PRE> 
is defined to equal 
<PRE>
  A <A HREF = "disj.html">\/</A> (<A HREF ="vp.html">v'</A> = v)
</PRE>
This action is true of a
 <A HREF = "step.html">step</A> 
iff the 
 <A HREF = "step.html">step</A> 
is an 
 <A HREF = "step.html"><CODE>A</CODE>-step</A> 
or a
<A HREF = "stuttering-step.html">&quot;stuttering step&quot;</A> 
that leaves <CODE>v</CODE> unchanged.