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

 Name                    Last modified      Size  Description
 Parent Directory                             -   
 Makefile                17-Dec-2007 09:59  1.4K  
 abs.lisp                17-Dec-2007 09:59  2.0K  
 binomial.lisp           17-Dec-2007 09:59   13K  
 certify.lsp             17-Dec-2007 09:59  2.5K  
 equalities.acl2         17-Dec-2007 09:59  469   
 equalities.lisp         17-Dec-2007 09:59   24K  
 factorial.lisp          17-Dec-2007 09:59  1.0K  
 idiv.lisp               17-Dec-2007 09:59  4.6K  
 inequalities.lisp       17-Dec-2007 09:59   19K  
 mod-gcd.lisp            17-Dec-2007 09:59   19K  
 natp-posp.lisp          17-Dec-2007 09:59  3.8K  
 rational-listp.lisp     17-Dec-2007 09:59  1.3K  
 rationals.lisp          17-Dec-2007 09:59  8.9K  
 sumlist.lisp            17-Dec-2007 09:59  952   
 top-with-meta.lisp      17-Dec-2007 09:59  1.0K  
 top.lisp                17-Dec-2007 09:59  1.4K  

Please see Section 0 of ../arithmetic-4/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