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>
  &lt;A&gt;
     v
</PRE> 
is defined to equal 
<PRE>
  A <A HREF = "conj.html">/\</A> (<A HREF ="vp.html">v'</A> <A HREF = "neq.html">\neq</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> 
that changes <CODE>v</CODE>.