There is also web page about this work in our web server.

Contents of this directory:

README.html	this file
multiset.lisp	A proof of well-foundedness of the multiset relation induced by a well-founded relation. Also, useful rules for multisets.
defmul.lisp	Definition of demul and defmul-components macros.
examples/ackermann/ackermann.lisp	Termination of a tail-recursive version of Ackermann's function.
examples/mccarthy-91/mccarthy-91.lisp	Termination of an iterative version of McCarthy's 91 function.
The following books are part of Newman's lemma example:
examples/newman/abstract-proofs.lisp	Basic concepts about abstract reduction relations.
examples/newman/confluence.lisp	A decision algorithm of the equivalence relation described by a confluent and normalizing reduction
examples/newman/newman.lisp	A proof of Newman's lemma: "Local confluence and termination implies confluence". This book uses defmul.
examples/newman/local-confluence.lisp	A decision algorithm for the equivalence relation described by a terminating and locally confluent reduction relation.