The 
 <A HREF = "temporal-formula.html">temporal formula</A>
<PRE>
  <A HREF = "WF.html">WF</A>      <A HREF = "WF.html">(</A><A HREF = "AX-exp.html">AX</A><A HREF = "WF.html">)</A>
    <A HREF = "pair-xy-exp.html">&lt;x, y&gt;</A>
</PRE> 
asserts of a 
 <A HREF = "behavior.html">behavior</A> 
that infinitely many 
 <A HREF = "step.html">steps</A> 
occur that increment
  <A HREF = "x-exp.html"><CODE>x</CODE></A>.
(These are 
  <A HREF = "AX-exp.html"><CODE>AX</CODE></A>
 <A HREF = "step.html">steps</A>.)