The 
 <A HREF = "temporal-formula.html">temporal formula</A>
<PRE>
  <A HREF = "box.html">[]</A><A HREF = "sqact.html">[</A><A HREF = "xp-eq-xplus1.html">x' = x+1</A><A HREF = "sqact.html">]</A>
              <A HREF = "sqact.html">x</A>
</PRE> 
asserts of a 
 <A HREF = "behavior.html">behavior</A> 
that every 
 <A HREF = "step.html">step</A> 
is either an 
 <A HREF = "xp-eq-xplus1.html">x' = x+1</A> 
step or a 
  <A HREF = "stuttering-step.html">stuttering step</A> 
that leaves 
  <A HREF = "xinPi.html">x</A> 
unchanged.  It is an instance of the construct
<PRE>
  <A HREF = "box-sqact.html">[][A]</A>
       <A HREF = "box-sqact.html">v</A>
</PRE>