The
 <A HREF = "state-predicate.html">state predicate</A>
 <CODE>Init</CODE>
is satisfied by a 
   <A HREF = "states.html">state</A>
iff the values of 
  <A HREF = "x-exp.html"><CODE>x</CODE></A> 
and 
  <A HREF = "y-exp.html"><CODE>y</CODE></A> 
are both 
  <A HREF = "zero.html">zero</A>
in that
   <A HREF = "states.html">state</A>.
It is satisfied by a 
 <A HREF = "behavior.html">behavior</A> 
iff it is satisfied by the first
   <A HREF = "states.html">state</A>
of the
 <A HREF = "behavior.html">behavior</A>.

<BR><BR>
<HR>
<PRE>
               <B>You are in Explanation Mode</B>       <A HREF = "Init-def.html"><B>Click here for Definition Mode</B></A>
</PRE>
<HR>