The formula
<PRE>
  <A HREF = "Pi-def.html">Pi</A> <A HREF = "equiv.html">\equiv</A> <A HREF = "EEPhi-exp.html">\EE y : 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 = "EEPhi-exp.html">\EE y : 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 = "EEPhi-exp.html">\EE y : Phi</A></CODE>,
or else it satisfies neither of them.

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