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

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