Multiset relations: a tool for proving termination

This directory contains the supporting materials for the paper:

Multiset relations: a tool for proving termination
J.-L. Ruiz-Reina, J.-A. Alonso, M.-J. Hidalgo, F.-J. Martín
ACL2 Workshop 2000 Proceedings, Austin, TX, October 2000.

You can also obtain:
A gzipped tar file for this directory.

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

To certify the books:

  1) Check the variables ACL2 and STRUCTURES-BOOK in Makefile, and
     change them if needed.

  2) Then you can execute:

   make             : To certify everything.
   make multiset    :     "      multiset.lisp and defmul.lisp.
   make ackermann   :     "      ackermann.lisp.
   make mccarthy-91 :     "      mccarthy-91.lisp.
   make newman      :     "      all the books of Newman's lemma.

See the NOTE file for a technical note.

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.

`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.