1 2 3
x
| 1 2 3
x
|
| Doing behavioral proofs by explicit coinduction can be a bit tedious,
especially if the definition of the candidate relation is complex. In our
exprrience, it is always much easier to do these proofs using circular
coinductive rewriting, and in the present case, this is actually trivial.
However, it is important to understand what coinduction really is, and the best way to do this is to first understand explicit coinduction. |