helphome pageduck scriptspecificationfirst proof page page 3 1 2 3 x

Inductive Properties of Lists, Part 2
Final Remarks


Although this proofweb is a bit more complex than our in previous examples, the main point is that it was built using what we learned from the failures in our previous attempts at the same main goal, that reversing a list twice yields the original list. This is similar to Joseph Campbell's notion of the hero's journey, a dangerous mission where failure can nevertheless result in bringing back valuable information or artifacts to the tribe.

It is also interesting to see how Kumo handles the associativity of append once it has been proved, by overwriting the declaration of that operation with a new declaration with the assoc attribute.


       This page was generated by Kumo on Tue Feb 13 19:34:15 PST 2001.