Index of /users/moore/acl2/v3-5/distrib/acl2-sources/books/arithmetic

 Name                    Last modified      Size  Description
 Parent Directory                             -   
 Makefile                13-Oct-2008 14:02  528   
 abs.lisp                13-Oct-2008 14:02  2.0K  
 binomial.lisp           13-Oct-2008 14:02   13K  
 equalities.acl2         13-Oct-2008 14:02  469   
 equalities.lisp         13-Oct-2008 14:02   24K  
 factorial.lisp          13-Oct-2008 14:02  1.0K  
 idiv.lisp               13-Oct-2008 14:02  4.6K  
 inequalities.lisp       13-Oct-2008 14:02   19K  
 mod-gcd.lisp            13-Oct-2008 14:02   19K  
 natp-posp.lisp          13-Oct-2008 14:02  3.8K  
 rational-listp.lisp     13-Oct-2008 14:02  1.3K  
 rationals.lisp          13-Oct-2008 14:02  8.9K  
 sumlist.lisp            13-Oct-2008 14:02  952   
 top-with-meta.lisp      13-Oct-2008 14:02  1.0K  
 top.lisp                13-Oct-2008 14:02  1.5K  

Advice on the use of arithmetic books (based largely on comments from
Robert Krug, and repeated in ../arithmetic-5/README):

  SUMMARY: Power users should include arithmetic-5/top; new users
  should probably instead include arithmetic/top-with-meta.

  Details:

  If you are willing to use dmr (see :doc dmr) and tolerate
  sometimes-slower (but more complete) reasoning, use arithmetic-5.
  Robert is not aware of any rewriting loops.

  If you are willing tolerate sometimes-slower (but more complete)
  reasoning, but you want to avoid dmr, use arithmetic-4.  However, if
  you're willing to use arithmetic-4, consider using arithmetic-5
  instead -- it doesn't require much more use of dmr, and it's much
  more up-to-date.  You may encounter rewriting loops.

  Don't use arithmetic-3.  It's not as powerful as arithmetic-4
  (Robert doesn't know if it's faster), and it has more rewriting
  loops than arithmetic-4.

  Note that arithmetic-2 is totally obsolete.  We may stop
  distributing it.

  If you want fast, lightweight arithmetic, use
  arithmetic/top-with-meta.

============================================================

Please see Section 0 of ../arithmetic-5/README for information about
which arithmetic books to use.

Contents of this directory:

README			This file
abs.lisp		Theorems about absolute value
binomial.lisp		A proof of the binomial theorem
certify.lsp		(ld "certify.lsp") to certify books in this directory
equalities.lisp		Arithmetic equality rules
factorial.lisp		Theorems about the factorial function
idiv.lisp		Theorems about integer division and related functions
inequalities.lisp	Arithmetic inequality rules
rational-listp.lisp	Very short book about lists of rationals
rationals-with-axioms-proved.lisp	Supersedes rationals-with-axioms.lisp
sumlist.lisp		Theorems about sum of a list of numbers
top.lisp		Putting it all together
top-with-meta.lisp      Extension of top.lisp by the books in ../meta

Many people contributed to these books, especially

  Bishop Brock
  John Cowles
  Matt Kaufmann  
  Art Flatau
  Ruben Gamboa