For any 
 <A HREF = "temporal-formula.html">temporal formula</A>
<CODE>F</CODE>, the 
 <A HREF = "temporal-formula.html">temporal formula</A>
<CODE>&lt;&gt;F</CODE> 
asserts that  <CODE>F</CODE> is <EM>eventually</EM> true.


<P><BR><BR>
More precisely, <CODE>&lt;&gt;F</CODE> is true for a
 <A HREF = "behavior.html">behavior</A> 
<PRE> 
  s , s , s , ... 
   1   2   3
</PRE> 
if and only if <CODE>F</CODE>
is true for the 
 <A HREF = "behavior.html">behavior</A> 
<PRE>
  s , s   , s   , ...
   N   N+1   N+2
</PRE> for
some <CODE>N &gt; 0</CODE>.  Equivalently,
<PRE>
  <>F  <A HREF = "deq.html">==</A>  <A HREF = "neg.html">~</A> <A HREF = "box.html">[]</A> <A HREF = "neg.html">~</A> F
</PRE>



<P><BR><BR>
The symbol <CODE>&lt;&gt;</CODE> also appears as an indivisible part of
the operator 
<PRE>
  &lt;&gt;&lt;A&gt;
       v
</PRE>
where <CODE>A</CODE> is an
 <A HREF = "action.html">action</A>
and  <CODE>v</CODE> is a
 <A HREF = "state-function.html">state function</A>.
This formula is true of a behavior iff some 
 <A HREF = "step.html">step</A> 
of the
behavior is a
<PRE>
  <A HREF = "angleact.html">&lt;A&gt;</A>
     <A HREF = "angleact.html">v</A>
</PRE>
 <A HREF = "step.html">step</A>.  Equivalently,
<PRE>
  &lt;&gt;&lt;A&gt;  <A HREF = "deq.html">==</A>  <A HREF = "neg.html">~</A> <A HREF = "box.html">[]</A> <A HREF = "sqact.html">[</A><A HREF = "neg.html">~</A><A HREF = "sqact.html">A]</A>
       v              <A HREF = "sqact.html">v</A>
</PRE>