The formula 
<PRE>
  <A HREF = "xinPi.html">x</A> <A HREF = "eq.html">=</A> <A HREF = "zero.html">0</A>
</PRE>
is a 
  <A HREF = "state-predicate.html">state predicate</A>
that is true of a 
   <A HREF = "states.html">state</A>
iff the value of the
 <A HREF = "variables.html">variable</A> 
<CODE>x</CODE> in that 
   <A HREF = "states.html">state</A>
is <CODE><A HREF = "zero.html">0</A></CODE>.  Viewed
as a
 <A HREF = "temporal-formula.html">temporal formula</A>,
this formula is true of a
 <A HREF = "behavior.html">behavior</A> 
iff the value of <CODE>x</CODE> is <CODE>0</CODE> in the first 
   <A HREF = "states.html">state</A>
of the 
 <A HREF = "behavior.html">behavior</A>.