The formula
<PRE>
  <A HREF = "box-sqact.html">[][AX \/ AY]</A> 
              <A HREF = "box-sqact.html">&lt;x, y&gt;</A> 
</PRE>
is true of a behavior iff every step is either
an
  <A HREF = "AXorAY-exp.html"><CODE>AX \/ AY</CODE></A> 
 <A HREF = "step.html">step</A> 
or else it leaves the pair
  <A HREF = "pair-xy-exp.html"><CODE>&lt;x, y&gt;</CODE></A>
unchanged.

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