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

 Name                    Last modified      Size  Description
 Parent Directory                             -   
 Makefile                06-May-2001 07:31  789   
 certify.lsp             07-Jan-2001 21:10  304   
 meta-plus-equal.lisp    19-May-1997 12:24  8.6K  
 meta-plus-lessp.lisp    19-May-1997 12:25   11K  
 meta-times-equal.lisp   18-May-2000 16:47   15K  
 meta.lisp               19-May-1997 10:49  1.1K  
 pseudo-termp-lemmas...> 27-Oct-1995 17:58  3.2K  
 term-defuns.lisp        11-Jul-2005 13:16  4.1K  
 term-lemmas.lisp        19-May-1997 12:25  3.0K  

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.