helphome pageduck scriptspecificationfirst proof page page 3 1 2 3 x

Doubly Reversed Flag
Final Remarks


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.


       This page was generated by Kumo on Tue Feb 13 17:33:10 PST 2001.