An 
 <A HREF = "action.html">action</A>
 <CODE>A</CODE> 
is <EM>enabled</EM> in a
   <A HREF = "states.html">state</A>
   <CODE>s</CODE>
iff there exists a 
   <A HREF = "states.html">state</A>
   <CODE>t</CODE>
such that
   <CODE>&lt;s, t&gt;</CODE>
is an
 <A HREF = "step.html"><CODE>A</CODE>-step</A>.

<P><BR>An 
 <A HREF = "action.html">action</A>
is <EM>disabled</EM> iff it is not enabled.

<P><BR>
We let 
<PRE>  Enabled A</PRE> 
denote the
 <A HREF = "state-predicate.html">state predicate</A>
that is true in 
   <A HREF = "states.html">state</A>
   <CODE>s</CODE>
iff <CODE>A</CODE> is enabled in 
   <A HREF = "states.html">state</A>
   <CODE>s</CODE>.