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

 Name                    Last modified      Size  Description
 Parent Directory                             -   
 Makefile                17-Dec-2007 09:57  789   
 certify.lsp             17-Dec-2007 09:57  304   
 meta-plus-equal.lisp    17-Dec-2007 09:57  8.6K  
 meta-plus-lessp.lisp    17-Dec-2007 09:57   11K  
 meta-times-equal.lisp   17-Dec-2007 09:57   15K  
 meta.lisp               17-Dec-2007 09:57  1.1K  
 pseudo-termp-lemmas...> 17-Dec-2007 09:57  3.2K  
 term-defuns.lisp        17-Dec-2007 09:57  4.1K  
 term-lemmas.lisp        17-Dec-2007 09:57  3.0K  

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

This directory contains some meta rules for arithmetic.  They are shown below.
There is a long history of meta rules for Nqthm.  The ones below were first
proved, with hypotheses (because they preceded version 1.8 of ACL2), by John
Cowles, following a proof by Matt Kaufmann of the first of them, which in turn
followed a proof by Yuan Yu of that same lemma for Nqthm (who assisted Matt in
formulating the ACL2 version), who in turn followed similar proofs by previous
Nqthm users (probably starting with Boyer and Moore)!

cancel_plus-equal-correct (file meta-plus-equal.lisp)
  (equal (ev-plus-equal x a)
         (ev-plus-equal (cancel_plus-equal x) a))

cancel_plus-lessp-correct (file meta-plus-lessp.lisp)
  (equal (ev-plus-lessp x a)
         (ev-plus-lessp (cancel_plus-lessp x) a))

cancel_times-equal-correct (file meta-times-equal.lisp)
  (equal (ev-times-equal x a)
         (ev-times-equal (cancel_times-equal x) a))

Note that the book pseudo-termp-lemmas.lisp is not needed, but is included
since many of its lemmas were already around for version 1.7.