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.9. Their semantics are as follows:

\begin{eqnarray*}
{} & \beta \mbox{$\:\vdash\:$}\mbox{\tt ref}\; s \mbox{$\:\lo...
...box{\tt (}t_1\mbox{\tt ,}...\mbox{\tt ,}t_n\mbox{\tt )}
& {}
\end{eqnarray*}





2004-08-06