Next: Composite proofs
Up: Proof semantics
Previous: Rule applications
  Contents
There are five rules for equality reasoning:
- ref (for equality reflexivity)
- swap (symmetry)
- tran (transitivity)
- cong (functional congruence)
- rel-cong (relational congruence)
The syntax of such rule applications was described in Section 1.7.
Their semantics are as follows:
2004-08-04