The formula
<PRE>
  <A HREF = "xinPi.html">x</A>' = <A HREF = "xinPi.html">x</A> <A HREF = "plus.html">+</A> <A HREF = "one.html">1</A>
</PRE>
is an 
  <A HREF = "action.html">action</A>
that is true of a
 <A HREF = "step.html">step</A> 
 <CODE>&lt;s, t&gt;</CODE>
iff the value of 
  <CODE><A HREF = "xinPi.html">x</A></CODE> 
in
  <A HREF = "states.html">state</A>
<CODE>t</CODE>
equals its value in
  <A HREF = "states.html">state</A>
<CODE>s</CODE>
  <A HREF = "plus.html">plus</A> 
  <A HREF = "one.html">1</A>.