The formula
<PRE>
  <A HREF = "Pi-def.html">Pi</A> <A HREF = "equiv.html">\equiv</A> <A HREF = "EE.html">\EE</A> <A HREF = "y-def.html">y</A> : <A HREF = "Phi-def.html">Phi</A>
</PRE>
asserts of a 
  <A HREF = "behavior.html">behavior</A> 
that formula
   <CODE><A HREF = "Pi-def.html">Pi</A></CODE>
is true iff formula
   <CODE><A HREF = "EE.html">\EE</A> <A HREF = "y-def.html">y</A> : <A HREF = "Phi-def.html">Phi</A></CODE>
is.  In other words, 
a
  <A HREF = "behavior.html">behavior</A> 
satisfies this formula iff it either satisfies both
   <CODE><A HREF = "Pi-def.html">Pi</A></CODE>
and
   <CODE><A HREF = "EE.html">\EE</A> <A HREF = "y-def.html">y</A> : <A HREF = "Phi-def.html">Phi</A></CODE>
or else it satisfies neither of them.

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