next up previous contents
Next: Composite proofs Up: Proof semantics Previous: Rule applications   Contents

Rules dealing with equality

There are five rules for equality reasoning:
  1. ref (for equality reflexivity)
  2. swap (symmetry)
  3. tran (transitivity)
  4. cong (functional congruence)
  5. rel-cong (relational congruence)
The syntax of such rule applications was described in Section 1.7. Their semantics are as follows:

\begin{eqnarray*}
{} & \beta \mbox{$\:\vdash\:$}\mbox{\tt ref}\; s \mbox{$\:\lo...
..._1\mbox{\tt ,}...\mbox{\tt ,}t_n\mbox{\tt )}
& {} \\ [0.06in]
\end{eqnarray*}





2004-08-04