The 
 <A HREF = "temporal-formula.html">temporal formula</A>
<PRE>
  <A HREF = "WF.html">WF </A>(<A HREF = "xp-eq-xplus1.html">x' = x+1</A><A HREF = "WF.html">)</A>
    <A HREF = "WF.html">x</A>
</PRE> 
is satisfied by a 
 <A HREF = "behavior.html">behavior</A> 
iff there are infinitely many 
 <CODE><A HREF = "xp-eq-xplus1.html">x' = x+1</A></CODE>
 <A HREF = "step.html">steps</A>.
It is an instance of the TLA construct
<PRE>
  <A HREF = "WF.html">WF (A)</A>
    <A HREF = "WF.html">v</A>
</PRE>