#| Copyright (C) 1990-1994 Computational Logic, Inc. All Rights Reserved. FM9001 PUBLIC SOFTWARE LICENSE Computational Logic, Inc. 1717 West Sixth, Suite 290 Austin, Texas 78703-4776 Please read this license carefully before using the FM9001 Software. By using the FM9001 Software, you are agreeing to be bound by the terms of this license. If you do not agree to the terms of this license, promptly return the FM9001 Software to the place where you obtained it. The FM9001 Software was developed by Computational Logic, Inc.(CLI). You own the disk or other medium on which the FM9001 Software is recorded, but CLI retains title to the FM9001 Software. The purposes of this license are to identify the FM9001 Software and to make the FM9001 Software, including its source code, freely available. This license allows you to use, copy, distribute and modify the FM9001 Software, on the condition that you comply with all the Copying Policies set out below. COPYING POLICIES 1. You may copy and distribute verbatim copies of the FM9001 Software as you receive it, in any medium, including embedding it verbatim in derivative works, provided that you a) conspicuously and appropriately publish on each copy a valid copyright notice "Copyright (C) 1990-1994 by Computational Logic, Inc. All Rights Reserved.", b) keep intact on all files the notices that refer to this License Agreement and to the absence of any warranty, and c) give all recipients of the FM9001 Software a copy of this License Agreement along with the program. 2. You may modify your copy or copies of the FM9001 Software or any portion of it, and copy and distribute such modifications provided you tell recipients that what they have is a modification by your organization of the CLI version of the FM9001 Software. 3. You may incorporate parts of the FM9001 Software into other programs provided that you acknowledge Computational Logic Inc. in the program documentation. CLI also requests, but does not require, that any improvements or extensions to the FM9001 Software be returned to one of the addresses below, so that they may be shared with other FM9001 users. The FM9001 Software, including its source, can be obtained by contacting one of these addresses. Software-Request or Software-Request@CLI.COM Computational Logic Inc. 1717 West Sixth, Suite 290 Austin, TX 78703-4776 NO WARRANTY BECAUSE THE FM9001 SOFTWARE IS LICENSED FREE OF CHARGE, WE PROVIDE ABSOLUTELY NO WARRANTY. THE SOFTWARE IS PROVIDED "AS IS" WITHOUT WARRANTY OF ANY KIND, EITHER EXPRESS OR IMPLIED, INCLUDING, BUT NOT LIMITED TO, ANY IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE. THE ENTIRE RISK AS TO THE QUALITY AND PERFORMANCE OF THE PROGRAM IS WITH YOU. SHOULD THE FM9001 SOFTWARE PROVE DEFECTIVE, YOU ASSUME THE COST OF ALL NECESSARY SERVICING, REPAIR OR CORRECTION. IN NO EVENT WILL COMPUTATIONAL LOGIC INC. BE LIABLE TO YOU FOR ANY DAMAGES, ANY LOST PROFITS, LOST MONIES, OR OTHER SPECIAL, INCIDENTAL OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE USE OR INABILITY TO USE THE FM9001 SOFTWARE (INCLUDING BUT NOT LIMITED TO LOSS OF DATA OR DATA BEING RENDERED INACCURATE OR LOSSES SUSTAINED BY THIRD PARTIES), EVEN IF YOU HAVE ADVISED US OF THE POSSIBILITY OF SUCH DAMAGES, OR FOR ANY CLAIM BY ANY OTHER PARTY. |# (BOOT-STRAP NQTHM) (SETQ REDUCE-TERM-CLOCK 2000) (DEFN DELETE (X L) (IF (LISTP L) (IF (EQUAL X (CAR L)) (CDR L) (CONS (CAR L) (DELETE X (CDR L)))) L)) (DEFN BAGDIFF (X Y) (IF (LISTP Y) (IF (MEMBER (CAR Y) X) (BAGDIFF (DELETE (CAR Y) X) (CDR Y)) (BAGDIFF X (CDR Y))) X)) (DEFN BAGINT (X Y) (IF (LISTP X) (IF (MEMBER (CAR X) Y) (CONS (CAR X) (BAGINT (CDR X) (DELETE (CAR X) Y))) (BAGINT (CDR X) Y)) NIL)) (DEFN OCCURRENCES (X L) (IF (LISTP L) (IF (EQUAL X (CAR L)) (ADD1 (OCCURRENCES X (CDR L))) (OCCURRENCES X (CDR L))) 0)) (DEFN SUBBAGP (X Y) (IF (LISTP X) (IF (MEMBER (CAR X) Y) (SUBBAGP (CDR X) (DELETE (CAR X) Y)) F) T)) (PROVE-LEMMA LISTP-DELETE (REWRITE) (EQUAL (LISTP (DELETE X L)) (IF (LISTP L) (OR (NOT (EQUAL X (CAR L))) (LISTP (CDR L))) F)) ((ENABLE DELETE) (INDUCT (DELETE X L)) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (TOGGLE LISTP-DELETE-OFF LISTP-DELETE T) (PROVE-LEMMA DELETE-NON-MEMBER (REWRITE) (IMPLIES (NOT (MEMBER X Y)) (EQUAL (DELETE X Y) Y)) ((ENABLE DELETE) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA DELETE-DELETE (REWRITE) (EQUAL (DELETE Y (DELETE X Z)) (DELETE X (DELETE Y Z))) ((ENABLE DELETE DELETE-NON-MEMBER) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA EQUAL-OCCURRENCES-ZERO (REWRITE) (EQUAL (EQUAL (OCCURRENCES X L) 0) (NOT (MEMBER X L))) ((ENABLE OCCURRENCES) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA MEMBER-NON-LIST (REWRITE) (IMPLIES (NOT (LISTP L)) (NOT (MEMBER X L))) ((ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA MEMBER-DELETE (REWRITE) (EQUAL (MEMBER X (DELETE Y L)) (IF (MEMBER X L) (IF (EQUAL X Y) (LESSP 1 (OCCURRENCES X L)) T) F)) ((ENABLE DELETE OCCURRENCES) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA MEMBER-DELETE-IMPLIES-MEMBERSHIP (REWRITE) (IMPLIES (MEMBER X (DELETE Y L)) (MEMBER X L)) ((ENABLE DELETE) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA OCCURRENCES-DELETE (REWRITE) (EQUAL (OCCURRENCES X (DELETE Y L)) (IF (EQUAL X Y) (IF (MEMBER X L) (SUB1 (OCCURRENCES X L)) 0) (OCCURRENCES X L))) ((ENABLE OCCURRENCES DELETE EQUAL-OCCURRENCES-ZERO) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA MEMBER-BAGDIFF (REWRITE) (EQUAL (MEMBER X (BAGDIFF A B)) (LESSP (OCCURRENCES X B) (OCCURRENCES X A))) ((ENABLE BAGDIFF OCCURRENCES EQUAL-OCCURRENCES-ZERO OCCURRENCES-DELETE) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA BAGDIFF-DELETE (REWRITE) (EQUAL (BAGDIFF (DELETE E X) Y) (DELETE E (BAGDIFF X Y))) ((ENABLE BAGDIFF DELETE DELETE-DELETE DELETE-NON-MEMBER MEMBER-BAGDIFF MEMBER-DELETE OCCURRENCES-DELETE) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA SUBBAGP-DELETE (REWRITE) (IMPLIES (SUBBAGP X (DELETE U Y)) (SUBBAGP X Y)) ((ENABLE DELETE SUBBAGP DELETE-DELETE MEMBER-DELETE-IMPLIES-MEMBERSHIP) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA SUBBAGP-CDR1 (REWRITE) (IMPLIES (SUBBAGP X Y) (SUBBAGP (CDR X) Y)) ((ENABLE SUBBAGP SUBBAGP-DELETE) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA SUBBAGP-CDR2 (REWRITE) (IMPLIES (SUBBAGP X (CDR Y)) (SUBBAGP X Y)) ((ENABLE DELETE SUBBAGP DELETE-NON-MEMBER SUBBAGP-CDR1) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA SUBBAGP-BAGINT1 (REWRITE) (SUBBAGP (BAGINT X Y) X) ((ENABLE DELETE SUBBAGP BAGINT SUBBAGP-CDR2) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA SUBBAGP-BAGINT2 (REWRITE) (SUBBAGP (BAGINT X Y) Y) ((ENABLE SUBBAGP BAGINT SUBBAGP-CDR2) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA OCCURRENCES-BAGINT (REWRITE) (EQUAL (OCCURRENCES X (BAGINT A B)) (IF (LESSP (OCCURRENCES X A) (OCCURRENCES X B)) (OCCURRENCES X A) (OCCURRENCES X B))) ((ENABLE OCCURRENCES BAGINT EQUAL-OCCURRENCES-ZERO OCCURRENCES-DELETE))) (PROVE-LEMMA OCCURRENCES-BAGDIFF (REWRITE) (EQUAL (OCCURRENCES X (BAGDIFF A B)) (DIFFERENCE (OCCURRENCES X A) (OCCURRENCES X B))) ((ENABLE OCCURRENCES BAGDIFF EQUAL-OCCURRENCES-ZERO OCCURRENCES-DELETE))) (PROVE-LEMMA MEMBER-BAGINT (REWRITE) (EQUAL (MEMBER X (BAGINT A B)) (AND (MEMBER X A) (MEMBER X B))) ((ENABLE BAGINT MEMBER-DELETE))) (DEFTHEORY BAGS (OCCURRENCES-BAGINT BAGDIFF-DELETE OCCURRENCES-BAGDIFF MEMBER-BAGINT MEMBER-BAGDIFF SUBBAGP-BAGINT2 SUBBAGP-BAGINT1 SUBBAGP-CDR2 SUBBAGP-CDR1 SUBBAGP-DELETE)) (PROVE-LEMMA EQUAL-PLUS-0 (REWRITE) (EQUAL (EQUAL (PLUS A B) 0) (AND (ZEROP A) (ZEROP B))) ((ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA PLUS-CANCELLATION (REWRITE) (EQUAL (EQUAL (PLUS A B) (PLUS A C)) (EQUAL (FIX B) (FIX C))) ((ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (TOGGLE PLUS-CANCELLATION-OFF PLUS-CANCELLATION T) (PROVE-LEMMA EQUAL-DIFFERENCE-0 (REWRITE) (AND (EQUAL (EQUAL (DIFFERENCE X Y) 0) (NOT (LESSP Y X))) (EQUAL (EQUAL 0 (DIFFERENCE X Y)) (NOT (LESSP Y X)))) ((INDUCT (DIFFERENCE X Y)) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA DIFFERENCE-CANCELLATION (REWRITE) (EQUAL (EQUAL (DIFFERENCE X Y) (DIFFERENCE Z Y)) (COND ((LESSP X Y) (NOT (LESSP Y Z))) ((LESSP Z Y) (NOT (LESSP Y X))) (T (EQUAL (FIX X) (FIX Z))))) ((ENABLE EQUAL-DIFFERENCE-0) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (TOGGLE DIFFERENCE-CANCELLATION-OFF DIFFERENCE-CANCELLATION T) (PROVE-LEMMA COMMUTATIVITY-OF-PLUS (REWRITE) (EQUAL (PLUS X Y) (PLUS Y X)) ((ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA COMMUTATIVITY2-OF-PLUS (REWRITE) (EQUAL (PLUS X Y Z) (PLUS Y X Z)) ((ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA PLUS-ZERO-ARG2 (REWRITE) (IMPLIES (ZEROP Y) (EQUAL (PLUS X Y) (FIX X))) ((INDUCT (PLUS X Y)) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA PLUS-ADD1-ARG1 (REWRITE) (EQUAL (PLUS (ADD1 A) B) (ADD1 (PLUS A B))) ((ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA PLUS-ADD1-ARG2 (REWRITE) (EQUAL (PLUS X (ADD1 Y)) (IF (NUMBERP Y) (ADD1 (PLUS X Y)) (ADD1 X))) ((ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA ASSOCIATIVITY-OF-PLUS (REWRITE) (EQUAL (PLUS (PLUS X Y) Z) (PLUS X Y Z)) ((ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA PLUS-DIFFERENCE-ARG1 (REWRITE) (EQUAL (PLUS (DIFFERENCE A B) C) (IF (LESSP B A) (DIFFERENCE (PLUS A C) B) (PLUS 0 C))) ((INDUCT (DIFFERENCE A B)) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA PLUS-DIFFERENCE-ARG2 (REWRITE) (EQUAL (PLUS A (DIFFERENCE B C)) (IF (LESSP C B) (DIFFERENCE (PLUS A B) C) (PLUS A 0))) ((INDUCT (PLUS A B)) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA DIFFERENCE-PLUS-CANCELLATION-PROOF NIL (EQUAL (DIFFERENCE (PLUS X Y) X) (FIX Y)) ((ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA DIFFERENCE-PLUS-CANCELLATION (REWRITE) (AND (EQUAL (DIFFERENCE (PLUS X Y) X) (FIX Y)) (EQUAL (DIFFERENCE (PLUS Y X) X) (FIX Y))) ((USE (DIFFERENCE-PLUS-CANCELLATION-PROOF (X X) (Y Y))) (ENABLE COMMUTATIVITY-OF-PLUS) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (TOGGLE DIFFERENCE-PLUS-CANCELLATION-OFF DIFFERENCE-PLUS-CANCELLATION T) (PROVE-LEMMA DIFFERENCE-PLUS-PLUS-CANCELLATION-PROOF NIL (EQUAL (DIFFERENCE (PLUS X Y) (PLUS X Z)) (DIFFERENCE Y Z)) ((ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA DIFFERENCE-PLUS-PLUS-CANCELLATION (REWRITE) (AND (EQUAL (DIFFERENCE (PLUS X Y) (PLUS X Z)) (DIFFERENCE Y Z)) (EQUAL (DIFFERENCE (PLUS Y X) (PLUS X Z)) (DIFFERENCE Y Z)) (EQUAL (DIFFERENCE (PLUS X Y) (PLUS Z X)) (DIFFERENCE Y Z)) (EQUAL (DIFFERENCE (PLUS Y X) (PLUS Z X)) (DIFFERENCE Y Z))) ((USE (DIFFERENCE-PLUS-PLUS-CANCELLATION-PROOF (X X) (Y Y) (Z Z))) (ENABLE COMMUTATIVITY-OF-PLUS) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (TOGGLE DIFFERENCE-PLUS-PLUS-CANCELLATION-OFF DIFFERENCE-PLUS-PLUS-CANCELLATION T) (PROVE-LEMMA DIFFERENCE-PLUS-PLUS-CANCELLATION-HACK (REWRITE) (EQUAL (DIFFERENCE (PLUS W X A) (PLUS Y Z A)) (DIFFERENCE (PLUS W X) (PLUS Y Z))) ((ENABLE COMMUTATIVITY-OF-PLUS COMMUTATIVITY2-OF-PLUS DIFFERENCE-PLUS-PLUS-CANCELLATION) (DO-NOT-INDUCT T) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (TOGGLE DIFFERENCE-PLUS-PLUS-CANCELLATION-HACK-OFF DIFFERENCE-PLUS-PLUS-CANCELLATION-HACK T) (PROVE-LEMMA DIFF-SUB1-ARG2 (REWRITE) (EQUAL (DIFFERENCE A (SUB1 B)) (COND ((ZEROP B) (FIX A)) ((LESSP A B) 0) (T (ADD1 (DIFFERENCE A B))))) ((INDUCT (DIFFERENCE A B)) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (TOGGLE DIFF-SUB1-ARG2-OFF DIFF-SUB1-ARG2 T) (PROVE-LEMMA DIFF-DIFF-ARG1 (REWRITE) (EQUAL (DIFFERENCE (DIFFERENCE X Y) Z) (DIFFERENCE X (PLUS Y Z))) ((ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA DIFF-DIFF-ARG2 (REWRITE) (EQUAL (DIFFERENCE A (DIFFERENCE B C)) (IF (LESSP B C) (FIX A) (DIFFERENCE (PLUS A C) B))) ((ENABLE DIFF-SUB1-ARG2 PLUS-ZERO-ARG2) (INDUCT (DIFFERENCE A B)) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA DIFF-DIFF-DIFF (REWRITE) (IMPLIES (AND (IF (LESSP A B) F T) (IF (LESSP C D) F T)) (EQUAL (DIFFERENCE (DIFFERENCE A B) (DIFFERENCE C D)) (DIFFERENCE (PLUS A D) (PLUS B C)))) ((ENABLE DIFF-DIFF-ARG1 DIFF-DIFF-ARG2 PLUS-DIFFERENCE-ARG2 PLUS-ZERO-ARG2) (DO-NOT-INDUCT T) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (TOGGLE DIFF-DIFF-DIFF-OFF DIFF-DIFF-DIFF T) (PROVE-LEMMA DIFFERENCE-LESSP-ARG1 (REWRITE) (IMPLIES (LESSP A B) (EQUAL (DIFFERENCE A B) 0)) ((ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (TOGGLE DIFFERENCE-LESSP-ARG1-OFF DIFFERENCE-LESSP-ARG1 T) (DEFN PLUS-FRINGE (X) (IF (AND (LISTP X) (EQUAL (CAR X) 'PLUS)) (APPEND (PLUS-FRINGE (CADR X)) (PLUS-FRINGE (CADDR X))) (LIST X))) (DEFN PLUS-TREE (L) (COND ((NLISTP L) ''0) ((NLISTP (CDR L)) (LIST 'FIX (CAR L))) ((NLISTP (CDDR L)) (LIST 'PLUS (CAR L) (CADR L))) (T (LIST 'PLUS (CAR L) (PLUS-TREE (CDR L)))))) (PROVE-LEMMA NUMBERP-EVAL$-PLUS (REWRITE) (IMPLIES (AND (LISTP X) (EQUAL (CAR X) 'PLUS)) (NUMBERP (EVAL$ T X A))) ((ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (TOGGLE NUMBERP-EVAL$-PLUS-OFF NUMBERP-EVAL$-PLUS T) (PROVE-LEMMA NUMBERP-EVAL$-PLUS-TREE (REWRITE) (NUMBERP (EVAL$ T (PLUS-TREE L) A)) ((ENABLE PLUS-TREE) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (TOGGLE NUMBERP-EVAL$-PLUS-TREE-OFF NUMBERP-EVAL$-PLUS-TREE T) (PROVE-LEMMA MEMBER-IMPLIES-PLUS-TREE-GREATEREQP (REWRITE) (IMPLIES (MEMBER X Y) (NOT (LESSP (EVAL$ T (PLUS-TREE Y) A) (EVAL$ T X A)))) ((ENABLE PLUS-TREE PLUS-ZERO-ARG2) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (TOGGLE MEMBER-IMPLIES-PLUS-TREE-GREATEREQP-OFF MEMBER-IMPLIES-PLUS-TREE-GREATEREQP T) (PROVE-LEMMA PLUS-TREE-DELETE (REWRITE) (EQUAL (EVAL$ T (PLUS-TREE (DELETE X Y)) A) (IF (MEMBER X Y) (DIFFERENCE (EVAL$ T (PLUS-TREE Y) A) (EVAL$ T X A)) (EVAL$ T (PLUS-TREE Y) A))) ((ENABLE DELETE PLUS-TREE DELETE-NON-MEMBER DIFFERENCE-PLUS-CANCELLATION EQUAL-DIFFERENCE-0 EQUAL-PLUS-0 LISTP-DELETE MEMBER-IMPLIES-PLUS-TREE-GREATEREQP NUMBERP-EVAL$-PLUS-TREE PLUS-ZERO-ARG2) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (TOGGLE PLUS-TREE-DELETE-OFF PLUS-TREE-DELETE T) (PROVE-LEMMA SUBBAGP-IMPLIES-PLUS-TREE-GREATEREQP (REWRITE) (IMPLIES (SUBBAGP X Y) (NOT (LESSP (EVAL$ T (PLUS-TREE Y) A) (EVAL$ T (PLUS-TREE X) A)))) ((ENABLE PLUS-TREE SUBBAGP MEMBER-IMPLIES-PLUS-TREE-GREATEREQP PLUS-TREE-DELETE PLUS-ZERO-ARG2 SUBBAGP-CDR2) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (TOGGLE SUBBAGP-IMPLIES-PLUS-TREE-GREATEREQP-OFF SUBBAGP-IMPLIES-PLUS-TREE-GREATEREQP T) (PROVE-LEMMA PLUS-TREE-BAGDIFF (REWRITE) (IMPLIES (SUBBAGP X Y) (EQUAL (EVAL$ T (PLUS-TREE (BAGDIFF Y X)) A) (DIFFERENCE (EVAL$ T (PLUS-TREE Y) A) (EVAL$ T (PLUS-TREE X) A)))) ((ENABLE BAGDIFF PLUS-TREE SUBBAGP COMMUTATIVITY-OF-PLUS DIFF-DIFF-ARG1 DIFFERENCE-LESSP-ARG1 MEMBER-IMPLIES-PLUS-TREE-GREATEREQP NUMBERP-EVAL$-PLUS-TREE PLUS-TREE-DELETE PLUS-ZERO-ARG2 SUBBAGP-CDR2 SUBBAGP-IMPLIES-PLUS-TREE-GREATEREQP) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (TOGGLE PLUS-TREE-BAGDIFF-OFF PLUS-TREE-BAGDIFF T) (PROVE-LEMMA NUMBERP-EVAL$-BRIDGE (REWRITE) (IMPLIES (EQUAL (EVAL$ T Z A) (EVAL$ T (PLUS-TREE X) A)) (NUMBERP (EVAL$ T Z A))) ((ENABLE PLUS-TREE NUMBERP-EVAL$-PLUS-TREE) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (TOGGLE NUMBERP-EVAL$-BRIDGE-OFF NUMBERP-EVAL$-BRIDGE T) (PROVE-LEMMA BRIDGE-TO-SUBBAGP-IMPLIES-PLUS-TREE-GREATEREQP (REWRITE) (IMPLIES (AND (SUBBAGP Y (PLUS-FRINGE Z)) (EQUAL (EVAL$ T Z A) (EVAL$ T (PLUS-TREE (PLUS-FRINGE Z)) A))) (EQUAL (LESSP (EVAL$ T Z A) (EVAL$ T (PLUS-TREE Y) A)) F)) ((ENABLE SUBBAGP PLUS-FRINGE PLUS-TREE SUBBAGP-IMPLIES-PLUS-TREE-GREATEREQP) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (TOGGLE BRIDGE-TO-SUBBAGP-IMPLIES-PLUS-TREE-GREATEREQP-OFF BRIDGE-TO-SUBBAGP-IMPLIES-PLUS-TREE-GREATEREQP T) (PROVE-LEMMA EVAL$-PLUS-TREE-APPEND (REWRITE) (EQUAL (EVAL$ T (PLUS-TREE (APPEND X Y)) A) (PLUS (EVAL$ T (PLUS-TREE X) A) (EVAL$ T (PLUS-TREE Y) A))) ((ENABLE PLUS-ZERO-ARG2 COMMUTATIVITY2-OF-PLUS COMMUTATIVITY-OF-PLUS EQUAL-PLUS-0 PLUS-CANCELLATION PLUS-TREE NUMBERP-EVAL$-PLUS-TREE NUMBERP-EVAL$-BRIDGE) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (TOGGLE EVAL$-PLUS-TREE-APPEND-OFF EVAL$-PLUS-TREE-APPEND T) (PROVE-LEMMA PLUS-TREE-PLUS-FRINGE (REWRITE) (EQUAL (EVAL$ T (PLUS-TREE (PLUS-FRINGE X)) A) (FIX (EVAL$ T X A))) ((ENABLE PLUS-ZERO-ARG2 COMMUTATIVITY-OF-PLUS PLUS-FRINGE PLUS-TREE NUMBERP-EVAL$-PLUS NUMBERP-EVAL$-BRIDGE EVAL$-PLUS-TREE-APPEND) (INDUCT (PLUS-FRINGE X)) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (TOGGLE PLUS-TREE-PLUS-FRINGE-OFF PLUS-TREE-PLUS-FRINGE T) (PROVE-LEMMA MEMBER-IMPLIES-NUMBERP (REWRITE) (IMPLIES (AND (MEMBER C (PLUS-FRINGE X)) (NUMBERP (EVAL$ T C A))) (NUMBERP (EVAL$ T X A))) ((ENABLE PLUS-FRINGE NUMBERP-EVAL$-PLUS) (INDUCT (PLUS-FRINGE X)) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (TOGGLE MEMBER-IMPLIES-NUMBERP-OFF MEMBER-IMPLIES-NUMBERP T) (PROVE-LEMMA CADR-EVAL$-LIST (REWRITE) (AND (EQUAL (CAR (EVAL$ 'LIST X A)) (EVAL$ T (CAR X) A)) (EQUAL (CDR (EVAL$ 'LIST X A)) (IF (LISTP X) (EVAL$ 'LIST (CDR X) A) 0))) ((ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (TOGGLE CADR-EVAL$-LIST-OFF CADR-EVAL$-LIST T) (PROVE-LEMMA EVAL$-QUOTE (REWRITE) (EQUAL (EVAL$ T (CONS 'QUOTE ARGS) A) (CAR ARGS)) ((ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (TOGGLE EVAL$-QUOTE-OFF EVAL$-QUOTE T) (PROVE-LEMMA LISTP-EVAL$ (REWRITE) (EQUAL (LISTP (EVAL$ 'LIST X A)) (LISTP X)) ((ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (TOGGLE LISTP-EVAL$-OFF LISTP-EVAL$ T) (DEFN CANCEL-EQUAL-PLUS (X) (IF (AND (LISTP X) (EQUAL (CAR X) 'EQUAL)) (COND ((AND (LISTP (CADR X)) (EQUAL (CAADR X) 'PLUS) (LISTP (CADDR X)) (EQUAL (CAADDR X) 'PLUS)) (LIST 'EQUAL (PLUS-TREE (BAGDIFF (PLUS-FRINGE (CADR X)) (BAGINT (PLUS-FRINGE (CADR X)) (PLUS-FRINGE (CADDR X))))) (PLUS-TREE (BAGDIFF (PLUS-FRINGE (CADDR X)) (BAGINT (PLUS-FRINGE (CADR X)) (PLUS-FRINGE (CADDR X))))))) ((AND (LISTP (CADR X)) (EQUAL (CAADR X) 'PLUS) (MEMBER (CADDR X) (PLUS-FRINGE (CADR X)))) (LIST 'IF (LIST 'NUMBERP (CADDR X)) (CONS 'EQUAL (CONS (PLUS-TREE (DELETE (CADDR X) (PLUS-FRINGE (CADR X)))) '('0))) (LIST 'QUOTE F))) ((AND (LISTP (CADDR X)) (EQUAL (CAADDR X) 'PLUS) (MEMBER (CADR X) (PLUS-FRINGE (CADDR X)))) (LIST 'IF (LIST 'NUMBERP (CADR X)) (LIST 'EQUAL ''0 (PLUS-TREE (DELETE (CADR X) (PLUS-FRINGE (CADDR X))))) (LIST 'QUOTE F))) (T X)) X)) (PROVE-LEMMA CORRECTNESS-OF-CANCEL-EQUAL-PLUS ((META EQUAL)) (EQUAL (EVAL$ T X A) (EVAL$ T (CANCEL-EQUAL-PLUS X) A)) ((ENABLE BRIDGE-TO-SUBBAGP-IMPLIES-PLUS-TREE-GREATEREQP CANCEL-EQUAL-PLUS DIFFERENCE-CANCELLATION EQUAL-DIFFERENCE-0 EVAL$-QUOTE MEMBER-IMPLIES-NUMBERP MEMBER-IMPLIES-PLUS-TREE-GREATEREQP NUMBERP-EVAL$-PLUS PLUS-TREE-BAGDIFF PLUS-TREE-DELETE PLUS-TREE-PLUS-FRINGE SUBBAGP-BAGINT1 SUBBAGP-BAGINT2) (DISABLE EVAL$) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (DEFN CANCEL-DIFFERENCE-PLUS (X) (IF (AND (LISTP X) (EQUAL (CAR X) 'DIFFERENCE)) (COND ((AND (LISTP (CADR X)) (EQUAL (CAADR X) 'PLUS) (LISTP (CADDR X)) (EQUAL (CAADDR X) 'PLUS)) (LIST 'DIFFERENCE (PLUS-TREE (BAGDIFF (PLUS-FRINGE (CADR X)) (BAGINT (PLUS-FRINGE (CADR X)) (PLUS-FRINGE (CADDR X))))) (PLUS-TREE (BAGDIFF (PLUS-FRINGE (CADDR X)) (BAGINT (PLUS-FRINGE (CADR X)) (PLUS-FRINGE (CADDR X))))))) ((AND (LISTP (CADR X)) (EQUAL (CAADR X) 'PLUS) (MEMBER (CADDR X) (PLUS-FRINGE (CADR X)))) (PLUS-TREE (DELETE (CADDR X) (PLUS-FRINGE (CADR X))))) ((AND (LISTP (CADDR X)) (EQUAL (CAADDR X) 'PLUS) (MEMBER (CADR X) (PLUS-FRINGE (CADDR X)))) ''0) (T X)) X)) (PROVE-LEMMA CORRECTNESS-OF-CANCEL-DIFFERENCE-PLUS ((META DIFFERENCE)) (EQUAL (EVAL$ T X A) (EVAL$ T (CANCEL-DIFFERENCE-PLUS X) A)) ((ENABLE CANCEL-DIFFERENCE-PLUS ASSOCIATIVITY-OF-PLUS BRIDGE-TO-SUBBAGP-IMPLIES-PLUS-TREE-GREATEREQP COMMUTATIVITY-OF-PLUS DIFF-DIFF-DIFF DIFFERENCE-LESSP-ARG1 DIFFERENCE-PLUS-PLUS-CANCELLATION-HACK EQUAL-DIFFERENCE-0 EVAL$-QUOTE MEMBER-IMPLIES-PLUS-TREE-GREATEREQP NUMBERP-EVAL$-PLUS PLUS-TREE-BAGDIFF PLUS-TREE-DELETE PLUS-TREE-PLUS-FRINGE SUBBAGP-BAGINT1 SUBBAGP-BAGINT2) (DISABLE EVAL$) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA DIFFERENCE-ELIM (ELIM) (IMPLIES (AND (NUMBERP Y) (NOT (LESSP Y X))) (EQUAL (PLUS X (DIFFERENCE Y X)) Y)) ((ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA DIFFERENCE-LEQ-ARG1 (REWRITE) (IMPLIES (IF (LESSP B A) F T) (EQUAL (DIFFERENCE A B) 0)) ((ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA DIFFERENCE-ADD1-ARG2 (REWRITE) (EQUAL (DIFFERENCE A (ADD1 B)) (IF (LESSP B A) (SUB1 (DIFFERENCE A B)) 0)) ((ENABLE DIFFERENCE-LEQ-ARG1) (INDUCT (DIFFERENCE A B)) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA DIFFERENCE-SUB1-ARG2 (REWRITE) (EQUAL (DIFFERENCE A (SUB1 B)) (COND ((ZEROP B) (FIX A)) ((LESSP A B) 0) (T (ADD1 (DIFFERENCE A B))))) ((ENABLE DIFF-SUB1-ARG2) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA DIFFERENCE-DIFFERENCE-ARG1 (REWRITE) (EQUAL (DIFFERENCE (DIFFERENCE X Y) Z) (DIFFERENCE X (PLUS Y Z))) ((ENABLE DIFF-DIFF-ARG1) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA DIFFERENCE-DIFFERENCE-ARG2 (REWRITE) (EQUAL (DIFFERENCE A (DIFFERENCE B C)) (IF (LESSP B C) (FIX A) (DIFFERENCE (PLUS A C) B))) ((ENABLE DIFF-DIFF-ARG2) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA DIFFERENCE-X-X (REWRITE) (EQUAL (DIFFERENCE X X) 0) ((ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA LESSP-DIFFERENCE-CANCELLATION (REWRITE) (EQUAL (LESSP (DIFFERENCE A C) (DIFFERENCE B C)) (IF (IF (LESSP A C) F T) (LESSP A B) (LESSP C B))) ((ENABLE EQUAL-DIFFERENCE-0) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (TOGGLE LESSP-DIFFERENCE-CANCELLATION-OFF LESSP-DIFFERENCE-CANCELLATION T) (DEFN CANCEL-LESSP-PLUS (X) (IF (AND (LISTP X) (EQUAL (CAR X) 'LESSP)) (COND ((AND (LISTP (CADR X)) (EQUAL (CAADR X) 'PLUS) (LISTP (CADDR X)) (EQUAL (CAADDR X) 'PLUS)) (LIST 'LESSP (PLUS-TREE (BAGDIFF (PLUS-FRINGE (CADR X)) (BAGINT (PLUS-FRINGE (CADR X)) (PLUS-FRINGE (CADDR X))))) (PLUS-TREE (BAGDIFF (PLUS-FRINGE (CADDR X)) (BAGINT (PLUS-FRINGE (CADR X)) (PLUS-FRINGE (CADDR X))))))) ((AND (LISTP (CADR X)) (EQUAL (CAADR X) 'PLUS) (MEMBER (CADDR X) (PLUS-FRINGE (CADR X)))) (LIST 'QUOTE F)) ((AND (LISTP (CADDR X)) (EQUAL (CAADDR X) 'PLUS) (MEMBER (CADR X) (PLUS-FRINGE (CADDR X)))) (LIST 'NOT (LIST 'ZEROP (PLUS-TREE (DELETE (CADR X) (PLUS-FRINGE (CADDR X))))))) (T X)) X)) (PROVE-LEMMA CORRECTNESS-OF-CANCEL-LESSP-PLUS ((META LESSP)) (EQUAL (EVAL$ T X A) (EVAL$ T (CANCEL-LESSP-PLUS X) A)) ((ENABLE CANCEL-LESSP-PLUS BRIDGE-TO-SUBBAGP-IMPLIES-PLUS-TREE-GREATEREQP EQUAL-DIFFERENCE-0 EVAL$-QUOTE LESSP-DIFFERENCE-CANCELLATION MEMBER-IMPLIES-PLUS-TREE-GREATEREQP NUMBERP-EVAL$-PLUS PLUS-TREE-BAGDIFF PLUS-TREE-DELETE PLUS-TREE-PLUS-FRINGE SUBBAGP-BAGINT1 SUBBAGP-BAGINT2) (DISABLE EVAL$) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (DEFTHEORY ADDITION (EQUAL-PLUS-0 EQUAL-DIFFERENCE-0 COMMUTATIVITY-OF-PLUS COMMUTATIVITY2-OF-PLUS PLUS-ZERO-ARG2 PLUS-ADD1-ARG2 PLUS-ADD1-ARG1 ASSOCIATIVITY-OF-PLUS PLUS-DIFFERENCE-ARG1 PLUS-DIFFERENCE-ARG2 DIFF-DIFF-ARG1 DIFF-DIFF-ARG2 CORRECTNESS-OF-CANCEL-EQUAL-PLUS CORRECTNESS-OF-CANCEL-DIFFERENCE-PLUS DIFFERENCE-ELIM DIFFERENCE-LEQ-ARG1 DIFFERENCE-ADD1-ARG2 DIFFERENCE-SUB1-ARG2 DIFFERENCE-DIFFERENCE-ARG1 DIFFERENCE-DIFFERENCE-ARG2 DIFFERENCE-X-X CORRECTNESS-OF-CANCEL-LESSP-PLUS)) (PROVE-LEMMA EQUAL-TIMES-0 (REWRITE) (EQUAL (EQUAL (TIMES X Y) 0) (OR (ZEROP X) (ZEROP Y))) ((ENABLE EQUAL-PLUS-0) (INDUCT (TIMES X Y)) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA EQUAL-TIMES-1 (REWRITE) (EQUAL (EQUAL (TIMES A B) 1) (AND (EQUAL A 1) (EQUAL B 1))) ((ENABLE EQUAL-PLUS-0) (INDUCT (TIMES A B)) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA EQUAL-SUB1-0 (REWRITE) (EQUAL (EQUAL (SUB1 X) 0) (OR (ZEROP X) (EQUAL X 1))) ((ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA TIMES-ZERO (REWRITE) (IMPLIES (ZEROP Y) (EQUAL (TIMES X Y) 0)) ((ENABLE PLUS-ZERO-ARG2 COMMUTATIVITY-OF-PLUS) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA TIMES-ADD1 (REWRITE) (EQUAL (TIMES X (ADD1 Y)) (IF (NUMBERP Y) (PLUS X (TIMES X Y)) (FIX X))) ((ENABLE PLUS-ZERO-ARG2 COMMUTATIVITY-OF-PLUS) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA COMMUTATIVITY-OF-TIMES (REWRITE) (EQUAL (TIMES Y X) (TIMES X Y)) ((ENABLE TIMES-ZERO TIMES-ADD1) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA TIMES-DISTRIBUTES-OVER-PLUS-PROOF NIL (EQUAL (TIMES X (PLUS Y Z)) (PLUS (TIMES X Y) (TIMES X Z))) ((ENABLE COMMUTATIVITY2-OF-PLUS ASSOCIATIVITY-OF-PLUS) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA TIMES-DISTRIBUTES-OVER-PLUS (REWRITE) (AND (EQUAL (TIMES X (PLUS Y Z)) (PLUS (TIMES X Y) (TIMES X Z))) (EQUAL (TIMES (PLUS X Y) Z) (PLUS (TIMES X Z) (TIMES Y Z)))) ((USE (TIMES-DISTRIBUTES-OVER-PLUS-PROOF (X X) (Y Y) (Z Z)) (TIMES-DISTRIBUTES-OVER-PLUS-PROOF (X Z) (Y X) (Z Y))) (ENABLE COMMUTATIVITY-OF-TIMES) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA COMMUTATIVITY2-OF-TIMES (REWRITE) (EQUAL (TIMES X Y Z) (TIMES Y X Z)) ((ENABLE COMMUTATIVITY-OF-TIMES TIMES-DISTRIBUTES-OVER-PLUS) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA ASSOCIATIVITY-OF-TIMES (REWRITE) (EQUAL (TIMES (TIMES X Y) Z) (TIMES X Y Z)) ((ENABLE COMMUTATIVITY-OF-TIMES COMMUTATIVITY2-OF-TIMES) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA TIMES-DISTRIBUTES-OVER-DIFFERENCE-PROOF NIL (EQUAL (TIMES (DIFFERENCE A B) C) (DIFFERENCE (TIMES A C) (TIMES B C))) ((ENABLE COMMUTATIVITY-OF-TIMES) (ENABLE-THEORY ADDITION GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA TIMES-DISTRIBUTES-OVER-DIFFERENCE (REWRITE) (AND (EQUAL (TIMES (DIFFERENCE A B) C) (DIFFERENCE (TIMES A C) (TIMES B C))) (EQUAL (TIMES A (DIFFERENCE B C)) (DIFFERENCE (TIMES A B) (TIMES A C)))) ((USE (TIMES-DISTRIBUTES-OVER-DIFFERENCE-PROOF (A A) (B B) (C C)) (TIMES-DISTRIBUTES-OVER-DIFFERENCE-PROOF (A B) (B C) (C A))) (ENABLE COMMUTATIVITY-OF-TIMES) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA TIMES-QUOTIENT-PROOF NIL (IMPLIES (AND (NOT (ZEROP X)) (EQUAL (REMAINDER Y X) 0)) (EQUAL (TIMES (QUOTIENT Y X) X) (FIX Y))) ((ENABLE TIMES-ZERO TIMES-ADD1) (INDUCT (REMAINDER Y X)) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA TIMES-QUOTIENT (REWRITE) (IMPLIES (AND (NOT (ZEROP Y)) (EQUAL (REMAINDER X Y) 0)) (AND (EQUAL (TIMES (QUOTIENT X Y) Y) (FIX X)) (EQUAL (TIMES Y (QUOTIENT X Y)) (FIX X)))) ((USE (TIMES-QUOTIENT-PROOF (X Y) (Y X))) (ENABLE COMMUTATIVITY-OF-TIMES) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA TIMES-1-ARG1 (REWRITE) (EQUAL (TIMES 1 X) (FIX X)) ((ENABLE TIMES-ZERO) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA LESSP-TIMES1-PROOF NIL (IMPLIES (AND (LESSP A B) (NOT (ZEROP C))) (EQUAL (LESSP A (TIMES B C)) T)) ((ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA LESSP-TIMES1 (REWRITE) (IMPLIES (AND (LESSP A B) (NOT (ZEROP C))) (AND (EQUAL (LESSP A (TIMES B C)) T) (EQUAL (LESSP A (TIMES C B)) T))) ((ENABLE COMMUTATIVITY-OF-TIMES) (USE (LESSP-TIMES1-PROOF (A A) (B B) (C C))) (DO-NOT-INDUCT T) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA LESSP-TIMES2-PROOF NIL (IMPLIES (AND (IF (LESSP B A) F T) (NOT (ZEROP C))) (EQUAL (LESSP (TIMES B C) A) F)) ((ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA LESSP-TIMES2 (REWRITE) (IMPLIES (AND (IF (LESSP B A) F T) (NOT (ZEROP C))) (AND (EQUAL (LESSP (TIMES B C) A) F) (EQUAL (LESSP (TIMES C B) A) F))) ((ENABLE COMMUTATIVITY-OF-TIMES) (USE (LESSP-TIMES2-PROOF (A A) (B B) (C C))) (DO-NOT-INDUCT T) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA LESSP-TIMES3-PROOF1 NIL (IMPLIES (AND (NOT (ZEROP A)) (LESSP 1 B)) (LESSP A (TIMES A B))) ((ENABLE-THEORY ADDITION GROUND-ZERO) (ENABLE TIMES-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA LESSP-TIMES3-PROOF2 NIL (IMPLIES (LESSP A (TIMES A B)) (AND (NOT (ZEROP A)) (LESSP 1 B))) ((ENABLE-THEORY ADDITION GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA LESSP-TIMES3 (REWRITE) (AND (EQUAL (LESSP A (TIMES A B)) (AND (NOT (ZEROP A)) (LESSP 1 B))) (EQUAL (LESSP A (TIMES B A)) (AND (NOT (ZEROP A)) (LESSP 1 B)))) ((ENABLE COMMUTATIVITY-OF-TIMES) (USE (LESSP-TIMES3-PROOF1 (A A) (B B)) (LESSP-TIMES3-PROOF2 (A A) (B B))) (DO-NOT-INDUCT T) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA LESSP-TIMES-CANCELLATION-PROOF NIL (EQUAL (LESSP (TIMES X Z) (TIMES Y Z)) (AND (NOT (ZEROP Z)) (LESSP X Y))) ((ENABLE COMMUTATIVITY-OF-TIMES CORRECTNESS-OF-CANCEL-LESSP-PLUS TIMES-ZERO) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA LESSP-TIMES-CANCELLATION1 (REWRITE) (AND (EQUAL (LESSP (TIMES X Z) (TIMES Y Z)) (AND (NOT (ZEROP Z)) (LESSP X Y))) (EQUAL (LESSP (TIMES Z X) (TIMES Y Z)) (AND (NOT (ZEROP Z)) (LESSP X Y))) (EQUAL (LESSP (TIMES X Z) (TIMES Z Y)) (AND (NOT (ZEROP Z)) (LESSP X Y))) (EQUAL (LESSP (TIMES Z X) (TIMES Z Y)) (AND (NOT (ZEROP Z)) (LESSP X Y)))) ((USE (LESSP-TIMES-CANCELLATION-PROOF (X X) (Y Y) (Z Z))) (ENABLE COMMUTATIVITY-OF-TIMES) (DO-NOT-INDUCT T) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (TOGGLE LESSP-TIMES-CANCELLATION1-OFF LESSP-TIMES-CANCELLATION1 T) (PROVE-LEMMA LESSP-PLUS-TIMES-PROOF NIL (IMPLIES (LESSP X A) (EQUAL (LESSP (PLUS X (TIMES A B)) (TIMES A C)) (LESSP B C))) ((ENABLE-THEORY ADDITION GROUND-ZERO) (ENABLE COMMUTATIVITY-OF-TIMES LESSP-TIMES-CANCELLATION1 LESSP-TIMES1 LESSP-TIMES2 LESSP-TIMES3 TIMES-ADD1 TIMES-ZERO) (INDUCT (LESSP B C)) (DISABLE-THEORY T))) (PROVE-LEMMA LESSP-PLUS-TIMES1 (REWRITE) (AND (EQUAL (LESSP (PLUS A (TIMES B C)) B) (AND (LESSP A B) (ZEROP C))) (EQUAL (LESSP (PLUS A (TIMES C B)) B) (AND (LESSP A B) (ZEROP C))) (EQUAL (LESSP (PLUS (TIMES C B) A) B) (AND (LESSP A B) (ZEROP C))) (EQUAL (LESSP (PLUS (TIMES B C) A) B) (AND (LESSP A B) (ZEROP C)))) ((USE (LESSP-PLUS-TIMES-PROOF (A B) (B C) (C 1) (X A))) (ENABLE COMMUTATIVITY-OF-PLUS COMMUTATIVITY-OF-TIMES TIMES-1-ARG1) (DO-NOT-INDUCT T) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA LESSP-PLUS-TIMES2 (REWRITE) (IMPLIES (AND (NOT (ZEROP A)) (LESSP X A)) (AND (EQUAL (LESSP (PLUS X (TIMES A B)) (TIMES A C)) (LESSP B C)) (EQUAL (LESSP (PLUS X (TIMES B A)) (TIMES A C)) (LESSP B C)) (EQUAL (LESSP (PLUS X (TIMES A B)) (TIMES C A)) (LESSP B C)) (EQUAL (LESSP (PLUS X (TIMES B A)) (TIMES C A)) (LESSP B C)) (EQUAL (LESSP (PLUS (TIMES A B) X) (TIMES A C)) (LESSP B C)) (EQUAL (LESSP (PLUS (TIMES B A) X) (TIMES A C)) (LESSP B C)) (EQUAL (LESSP (PLUS (TIMES A B) X) (TIMES C A)) (LESSP B C)) (EQUAL (LESSP (PLUS (TIMES B A) X) (TIMES C A)) (LESSP B C)))) ((ENABLE COMMUTATIVITY-OF-PLUS COMMUTATIVITY-OF-TIMES) (USE (LESSP-PLUS-TIMES-PROOF (A A) (B B) (C C) (X X))) (DO-NOT-INDUCT T) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA LESSP-1-TIMES (REWRITE) (EQUAL (LESSP 1 (TIMES A B)) (NOT (OR (ZEROP A) (ZEROP B) (AND (EQUAL A 1) (EQUAL B 1))))) ((ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (DEFN TIMES-TREE (X) (COND ((NLISTP X) ''1) ((NLISTP (CDR X)) (LIST 'FIX (CAR X))) ((NLISTP (CDDR X)) (LIST 'TIMES (CAR X) (CADR X))) (T (LIST 'TIMES (CAR X) (TIMES-TREE (CDR X)))))) (DEFN TIMES-FRINGE (X) (IF (AND (LISTP X) (EQUAL (CAR X) 'TIMES)) (APPEND (TIMES-FRINGE (CADR X)) (TIMES-FRINGE (CADDR X))) (LIST X))) (DEFN OR-ZEROP-TREE (X) (COND ((NLISTP X) '(FALSE)) ((NLISTP (CDR X)) (LIST 'ZEROP (CAR X))) ((NLISTP (CDDR X)) (LIST 'OR (LIST 'ZEROP (CAR X)) (LIST 'ZEROP (CADR X)))) (T (LIST 'OR (LIST 'ZEROP (CAR X)) (OR-ZEROP-TREE (CDR X)))))) (DEFN AND-NOT-ZEROP-TREE (X) (COND ((NLISTP X) '(TRUE)) ((NLISTP (CDR X)) (LIST 'NOT (LIST 'ZEROP (CAR X)))) (T (LIST 'AND (LIST 'NOT (LIST 'ZEROP (CAR X))) (AND-NOT-ZEROP-TREE (CDR X)))))) (PROVE-LEMMA NUMBERP-EVAL$-TIMES (REWRITE) (IMPLIES (EQUAL (CAR X) 'TIMES) (NUMBERP (EVAL$ T X A))) ((ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (TOGGLE NUMBERP-EVAL$-TIMES-OFF NUMBERP-EVAL$-TIMES T) (PROVE-LEMMA EVAL$-TIMES (REWRITE) (IMPLIES (EQUAL (CAR X) 'TIMES) (EQUAL (EVAL$ T X A) (TIMES (EVAL$ T (CADR X) A) (EVAL$ T (CADDR X) A)))) ((ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (TOGGLE EVAL$-TIMES-OFF EVAL$-TIMES T) (PROVE-LEMMA EVAL$-OR (REWRITE) (IMPLIES (EQUAL (CAR X) 'OR) (EQUAL (EVAL$ T X A) (OR (EVAL$ T (CADR X) A) (EVAL$ T (CADDR X) A)))) ((ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (TOGGLE EVAL$-OR-OFF EVAL$-OR T) (PROVE-LEMMA EVAL$-EQUAL (REWRITE) (IMPLIES (EQUAL (CAR X) 'EQUAL) (EQUAL (EVAL$ T X A) (EQUAL (EVAL$ T (CADR X) A) (EVAL$ T (CADDR X) A)))) ((ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (TOGGLE EVAL$-EQUAL-OFF EVAL$-EQUAL T) (PROVE-LEMMA EVAL$-LESSP (REWRITE) (IMPLIES (EQUAL (CAR X) 'LESSP) (EQUAL (EVAL$ T X A) (LESSP (EVAL$ T (CADR X) A) (EVAL$ T (CADDR X) A)))) ((ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (TOGGLE EVAL$-LESSP-OFF EVAL$-LESSP T) (PROVE-LEMMA EVAL$-QUOTIENT (REWRITE) (IMPLIES (EQUAL (CAR X) 'QUOTIENT) (EQUAL (EVAL$ T X A) (QUOTIENT (EVAL$ T (CADR X) A) (EVAL$ T (CADDR X) A)))) ((ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (TOGGLE EVAL$-QUOTIENT-OFF EVAL$-QUOTIENT T) (PROVE-LEMMA EVAL$-IF (REWRITE) (IMPLIES (EQUAL (CAR X) 'IF) (EQUAL (EVAL$ T X A) (IF (EVAL$ T (CADR X) A) (EVAL$ T (CADDR X) A) (EVAL$ T (CADDDR X) A)))) ((ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (TOGGLE EVAL$-IF-OFF EVAL$-IF T) (PROVE-LEMMA NUMBERP-EVAL$-TIMES-TREE (REWRITE) (NUMBERP (EVAL$ T (TIMES-TREE X) A)) ((ENABLE TIMES-TREE) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (TOGGLE NUMBERP-EVAL$-TIMES-TREE-OFF NUMBERP-EVAL$-TIMES-TREE T) (PROVE-LEMMA LESSP-TIMES-ARG1 NIL (IMPLIES (NOT (ZEROP A)) (EQUAL (NOT (LESSP (TIMES A X) (TIMES A Y))) (NOT (LESSP X Y)))) ((INDUCT (PLUS A X)) (ENABLE TIMES CORRECTNESS-OF-CANCEL-LESSP-PLUS) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA INFER-EQUALITY-FROM-NOT-LESSP NIL (IMPLIES (AND (NUMBERP A) (NUMBERP B)) (EQUAL (AND (NOT (LESSP A B)) (NOT (LESSP B A))) (EQUAL A B))) ((ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA EQUAL-TIMES-ARG1 (REWRITE) (IMPLIES (NOT (ZEROP A)) (EQUAL (EQUAL (TIMES A X) (TIMES A Y)) (EQUAL (FIX X) (FIX Y)))) ((USE (LESSP-TIMES-ARG1 (A A) (X X) (Y Y)) (LESSP-TIMES-ARG1 (A A) (X Y) (Y X)) (INFER-EQUALITY-FROM-NOT-LESSP (A (TIMES A X)) (B (TIMES A Y)))) (DO-NOT-INDUCT T) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (TOGGLE EQUAL-TIMES-ARG1-OFF EQUAL-TIMES-ARG1 T) (PROVE-LEMMA EQUAL-TIMES-BRIDGE (REWRITE) (EQUAL (EQUAL (TIMES A B) (TIMES C A D)) (OR (ZEROP A) (EQUAL (FIX B) (TIMES C D)))) ((ENABLE COMMUTATIVITY-OF-TIMES COMMUTATIVITY2-OF-TIMES EQUAL-TIMES-0 EQUAL-TIMES-ARG1 TIMES-ZERO) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (TOGGLE EQUAL-TIMES-BRIDGE-OFF EQUAL-TIMES-BRIDGE T) (PROVE-LEMMA EVAL$-TIMES-MEMBER (REWRITE) (IMPLIES (MEMBER E X) (EQUAL (EVAL$ T (TIMES-TREE X) A) (TIMES (EVAL$ T E A) (EVAL$ T (TIMES-TREE (DELETE E X)) A)))) ((ENABLE DELETE TIMES-TREE COMMUTATIVITY-OF-TIMES DELETE-NON-MEMBER EQUAL-TIMES-0 EQUAL-TIMES-BRIDGE LISTP-DELETE MEMBER-NON-LIST TIMES-1-ARG1 TIMES-ZERO) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (TOGGLE EVAL$-TIMES-MEMBER-OFF EVAL$-TIMES-MEMBER T) (PROVE-LEMMA ZEROP-MAKES-TIMES-TREE-ZERO (REWRITE) (IMPLIES (AND (NOT (EVAL$ T (AND-NOT-ZEROP-TREE X) A)) (SUBBAGP X Y)) (EQUAL (EVAL$ T (TIMES-TREE Y) A) 0)) ((ENABLE AND-NOT-ZEROP-TREE COMMUTATIVITY-OF-TIMES EVAL$-TIMES-MEMBER SUBBAGP TIMES-TREE TIMES-ZERO) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (TOGGLE ZEROP-MAKES-TIMES-TREE-ZERO-OFF ZEROP-MAKES-TIMES-TREE-ZERO T) (PROVE-LEMMA OR-ZEROP-TREE-IS-NOT-ZEROP-TREE (REWRITE) (EQUAL (EVAL$ T (OR-ZEROP-TREE X) A) (NOT (EVAL$ T (AND-NOT-ZEROP-TREE X) A))) ((ENABLE AND-NOT-ZEROP-TREE OR-ZEROP-TREE) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (TOGGLE OR-ZEROP-TREE-IS-NOT-ZEROP-TREE-OFF OR-ZEROP-TREE-IS-NOT-ZEROP-TREE T) (PROVE-LEMMA ZEROP-MAKES-TIMES-TREE-ZERO2 (REWRITE) (IMPLIES (AND (EVAL$ T (OR-ZEROP-TREE X) A) (SUBBAGP X Y)) (EQUAL (EVAL$ T (TIMES-TREE Y) A) 0)) ((USE (ZEROP-MAKES-TIMES-TREE-ZERO) (OR-ZEROP-TREE-IS-NOT-ZEROP-TREE)) (ENABLE OR-ZEROP-TREE SUBBAGP TIMES-TREE) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (TOGGLE ZEROP-MAKES-TIMES-TREE-ZERO2-OFF ZEROP-MAKES-TIMES-TREE-ZERO2 T) (PROVE-LEMMA TIMES-TREE-APPEND (REWRITE) (EQUAL (EVAL$ T (TIMES-TREE (APPEND X Y)) A) (TIMES (EVAL$ T (TIMES-TREE X) A) (EVAL$ T (TIMES-TREE Y) A))) ((ENABLE APPEND ASSOCIATIVITY-OF-TIMES COMMUTATIVITY-OF-TIMES COMMUTATIVITY2-OF-TIMES EQUAL-TIMES-0 EQUAL-TIMES-ARG1 EQUAL-TIMES-BRIDGE NUMBERP-EVAL$-TIMES-TREE TIMES-1-ARG1 TIMES-TREE TIMES-ZERO) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (TOGGLE TIMES-TREE-APPEND-OFF TIMES-TREE-APPEND T) (PROVE-LEMMA TIMES-TREE-OF-TIMES-FRINGE (REWRITE) (EQUAL (EVAL$ T (TIMES-TREE (TIMES-FRINGE X)) A) (FIX (EVAL$ T X A))) ((ENABLE COMMUTATIVITY-OF-TIMES EVAL$-TIMES TIMES-FRINGE TIMES-TREE TIMES-TREE-APPEND TIMES-ZERO) (INDUCT (TIMES-FRINGE X)) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (TOGGLE TIMES-TREE-OF-TIMES-FRINGE-OFF TIMES-TREE-OF-TIMES-FRINGE T) (DEFN CANCEL-LESSP-TIMES (X) (IF (AND (EQUAL (CAR X) 'LESSP) (EQUAL (CAADR X) 'TIMES) (EQUAL (CAADDR X) 'TIMES)) (IF (LISTP (BAGINT (TIMES-FRINGE (CADR X)) (TIMES-FRINGE (CADDR X)))) (LIST 'AND (AND-NOT-ZEROP-TREE (BAGINT (TIMES-FRINGE (CADR X)) (TIMES-FRINGE (CADDR X)))) (LIST 'LESSP (TIMES-TREE (BAGDIFF (TIMES-FRINGE (CADR X)) (BAGINT (TIMES-FRINGE (CADR X)) (TIMES-FRINGE (CADDR X))))) (TIMES-TREE (BAGDIFF (TIMES-FRINGE (CADDR X)) (BAGINT (TIMES-FRINGE (CADR X)) (TIMES-FRINGE (CADDR X))))))) X) X)) (PROVE-LEMMA EVAL$-LESSP-TIMES-TREE-BAGDIFF (REWRITE) (IMPLIES (AND (SUBBAGP X Y) (SUBBAGP X Z) (EVAL$ T (AND-NOT-ZEROP-TREE X) A)) (EQUAL (LESSP (EVAL$ T (TIMES-TREE (BAGDIFF Y X)) A) (EVAL$ T (TIMES-TREE (BAGDIFF Z X)) A)) (LESSP (EVAL$ T (TIMES-TREE Y) A) (EVAL$ T (TIMES-TREE Z) A)))) ((ENABLE AND-NOT-ZEROP-TREE BAGDIFF EVAL$-TIMES-MEMBER LESSP-TIMES-CANCELLATION1 SUBBAGP SUBBAGP-CDR1 SUBBAGP-CDR2 TIMES-TREE ZEROP-MAKES-TIMES-TREE-ZERO) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (TOGGLE EVAL$-LESSP-TIMES-TREE-BAGDIFF-OFF EVAL$-LESSP-TIMES-TREE-BAGDIFF T) (PROVE-LEMMA ZEROP-MAKES-LESSP-FALSE-BRIDGE (REWRITE) (IMPLIES (AND (EQUAL (CAR X) 'TIMES) (EQUAL (CAR Y) 'TIMES) (NOT (EVAL$ T (AND-NOT-ZEROP-TREE (BAGINT (TIMES-FRINGE X) (TIMES-FRINGE Y))) A))) (EQUAL (LESSP (TIMES (EVAL$ T (CADR X) A) (EVAL$ T (CADDR X) A)) (TIMES (EVAL$ T (CADR Y) A) (EVAL$ T (CADDR Y) A))) F)) ((ENABLE AND-NOT-ZEROP-TREE BAGINT COMMUTATIVITY-OF-TIMES DELETE EQUAL-TIMES-0 EVAL$-TIMES SUBBAGP-BAGINT1 SUBBAGP-BAGINT2 TIMES-FRINGE TIMES-TREE TIMES-TREE-APPEND TIMES-TREE-OF-TIMES-FRINGE TIMES-ZERO) (USE (ZEROP-MAKES-TIMES-TREE-ZERO (X (BAGINT (TIMES-FRINGE X) (TIMES-FRINGE Y))) (Y (TIMES-FRINGE X))) (ZEROP-MAKES-TIMES-TREE-ZERO (X (BAGINT (TIMES-FRINGE X) (TIMES-FRINGE Y))) (Y (TIMES-FRINGE Y)))) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (TOGGLE ZEROP-MAKES-LESSP-FALSE-BRIDGE-OFF ZEROP-MAKES-LESSP-FALSE-BRIDGE T) (PROVE-LEMMA CORRECTNESS-OF-CANCEL-LESSP-TIMES ((META LESSP)) (EQUAL (EVAL$ T X A) (EVAL$ T (CANCEL-LESSP-TIMES X) A)) ((ENABLE CANCEL-LESSP-TIMES EVAL$-LESSP-TIMES-TREE-BAGDIFF EVAL$-LESSP EVAL$-TIMES SUBBAGP-BAGINT1 SUBBAGP-BAGINT2 TIMES-TREE-OF-TIMES-FRINGE ZEROP-MAKES-LESSP-FALSE-BRIDGE) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (DEFN CANCEL-EQUAL-TIMES (X) (IF (AND (EQUAL (CAR X) 'EQUAL) (EQUAL (CAADR X) 'TIMES) (EQUAL (CAADDR X) 'TIMES)) (IF (LISTP (BAGINT (TIMES-FRINGE (CADR X)) (TIMES-FRINGE (CADDR X)))) (LIST 'OR (OR-ZEROP-TREE (BAGINT (TIMES-FRINGE (CADR X)) (TIMES-FRINGE (CADDR X)))) (LIST 'EQUAL (TIMES-TREE (BAGDIFF (TIMES-FRINGE (CADR X)) (BAGINT (TIMES-FRINGE (CADR X)) (TIMES-FRINGE (CADDR X))))) (TIMES-TREE (BAGDIFF (TIMES-FRINGE (CADDR X)) (BAGINT (TIMES-FRINGE (CADR X)) (TIMES-FRINGE (CADDR X))))))) X) X)) (PROVE-LEMMA ZEROP-MAKES-EQUAL-TRUE-BRIDGE (REWRITE) (IMPLIES (AND (EQUAL (CAR X) 'TIMES) (EQUAL (CAR Y) 'TIMES) (EVAL$ T (OR-ZEROP-TREE (BAGINT (TIMES-FRINGE X) (TIMES-FRINGE Y))) A)) (EQUAL (EQUAL (TIMES (EVAL$ T (CADR X) A) (EVAL$ T (CADDR X) A)) (TIMES (EVAL$ T (CADR Y) A) (EVAL$ T (CADDR Y) A))) T)) ((ENABLE BAGINT COMMUTATIVITY-OF-TIMES DELETE EQUAL-TIMES-0 EVAL$-TIMES OR-ZEROP-TREE SUBBAGP-BAGINT1 SUBBAGP-BAGINT2 TIMES-FRINGE TIMES-TREE TIMES-TREE-APPEND TIMES-TREE-OF-TIMES-FRINGE TIMES-ZERO) (USE (ZEROP-MAKES-TIMES-TREE-ZERO2 (X (BAGINT (TIMES-FRINGE X) (TIMES-FRINGE Y))) (Y (TIMES-FRINGE X))) (ZEROP-MAKES-TIMES-TREE-ZERO2 (X (BAGINT (TIMES-FRINGE X) (TIMES-FRINGE Y))) (Y (TIMES-FRINGE Y)))) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (TOGGLE ZEROP-MAKES-EQUAL-TRUE-BRIDGE-OFF ZEROP-MAKES-EQUAL-TRUE-BRIDGE T) (PROVE-LEMMA EVAL$-EQUAL-TIMES-TREE-BAGDIFF (REWRITE) (IMPLIES (AND (SUBBAGP X Y) (SUBBAGP X Z) (NOT (EVAL$ T (OR-ZEROP-TREE X) A))) (EQUAL (EQUAL (EVAL$ T (TIMES-TREE (BAGDIFF Y X)) A) (EVAL$ T (TIMES-TREE (BAGDIFF Z X)) A)) (EQUAL (EVAL$ T (TIMES-TREE Y) A) (EVAL$ T (TIMES-TREE Z) A)))) ((ENABLE AND-NOT-ZEROP-TREE BAGDIFF EQUAL-TIMES-ARG1 EVAL$-TIMES-MEMBER NUMBERP-EVAL$-TIMES-TREE OR-ZEROP-TREE OR-ZEROP-TREE-IS-NOT-ZEROP-TREE SUBBAGP SUBBAGP-CDR1 SUBBAGP-CDR2 TIMES-TREE ZEROP-MAKES-TIMES-TREE-ZERO) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (TOGGLE EVAL$-EQUAL-TIMES-TREE-BAGDIFF-OFF EVAL$-EQUAL-TIMES-TREE-BAGDIFF T) (PROVE-LEMMA CANCEL-EQUAL-TIMES-PRESERVES-INEQUALITY (REWRITE) (IMPLIES (AND (SUBBAGP Z X) (SUBBAGP Z Y) (NOT (EQUAL (EVAL$ T (TIMES-TREE X) A) (EVAL$ T (TIMES-TREE Y) A)))) (NOT (EQUAL (EVAL$ T (TIMES-TREE (BAGDIFF X Z)) A) (EVAL$ T (TIMES-TREE (BAGDIFF Y Z)) A)))) ((ENABLE BAGDIFF EVAL$-TIMES-MEMBER SUBBAGP SUBBAGP-CDR2 TIMES-TREE) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (TOGGLE CANCEL-EQUAL-TIMES-PRESERVES-INEQUALITY-OFF CANCEL-EQUAL-TIMES-PRESERVES-INEQUALITY T) (PROVE-LEMMA CANCEL-EQUAL-TIMES-PRESERVES-INEQUALITY-BRIDGE (REWRITE) (IMPLIES (AND (EQUAL (CAR X) 'TIMES) (EQUAL (CAR Y) 'TIMES) (NOT (EQUAL (TIMES (EVAL$ T (CADR X) A) (EVAL$ T (CADDR X) A)) (TIMES (EVAL$ T (CADR Y) A) (EVAL$ T (CADDR Y) A))))) (NOT (EQUAL (EVAL$ T (TIMES-TREE (BAGDIFF (TIMES-FRINGE X) (BAGINT (TIMES-FRINGE X) (TIMES-FRINGE Y)))) A) (EVAL$ T (TIMES-TREE (BAGDIFF (TIMES-FRINGE Y) (BAGINT (TIMES-FRINGE X) (TIMES-FRINGE Y)))) A)))) ((ENABLE BAGDIFF BAGINT COMMUTATIVITY-OF-TIMES SUBBAGP-BAGINT1 SUBBAGP-BAGINT2 TIMES-FRINGE TIMES-TREE TIMES-TREE-APPEND TIMES-TREE-OF-TIMES-FRINGE TIMES-ZERO) (USE (CANCEL-EQUAL-TIMES-PRESERVES-INEQUALITY (Z (BAGINT (TIMES-FRINGE X) (TIMES-FRINGE Y))) (X (TIMES-FRINGE X)) (Y (TIMES-FRINGE Y)))) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (TOGGLE CANCEL-EQUAL-TIMES-PRESERVES-INEQUALITY-BRIDGE-OFF CANCEL-EQUAL-TIMES-PRESERVES-INEQUALITY-BRIDGE T) (PROVE-LEMMA CORRECTNESS-OF-CANCEL-EQUAL-TIMES ((META EQUAL)) (EQUAL (EVAL$ T X A) (EVAL$ T (CANCEL-EQUAL-TIMES X) A)) ((ENABLE CANCEL-EQUAL-TIMES CANCEL-EQUAL-TIMES-PRESERVES-INEQUALITY-BRIDGE EVAL$-EQUAL EVAL$-EQUAL-TIMES-TREE-BAGDIFF EVAL$-TIMES SUBBAGP-BAGINT1 SUBBAGP-BAGINT2 TIMES-TREE-OF-TIMES-FRINGE ZEROP-MAKES-EQUAL-TRUE-BRIDGE) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (DEFTHEORY MULTIPLICATION (EQUAL-TIMES-0 EQUAL-TIMES-1 EQUAL-SUB1-0 TIMES-ZERO TIMES-ADD1 COMMUTATIVITY-OF-TIMES TIMES-DISTRIBUTES-OVER-PLUS COMMUTATIVITY2-OF-TIMES ASSOCIATIVITY-OF-TIMES TIMES-DISTRIBUTES-OVER-DIFFERENCE TIMES-QUOTIENT TIMES-1-ARG1 LESSP-TIMES1 LESSP-TIMES2 LESSP-TIMES3 LESSP-PLUS-TIMES1 LESSP-PLUS-TIMES2 LESSP-1-TIMES CORRECTNESS-OF-CANCEL-LESSP-TIMES CORRECTNESS-OF-CANCEL-EQUAL-TIMES)) (PROVE-LEMMA LESSP-REMAINDER (REWRITE GENERALIZE) (EQUAL (LESSP (REMAINDER X Y) Y) (NOT (ZEROP Y))) ((ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA REMAINDER-NOOP (REWRITE) (IMPLIES (LESSP A B) (EQUAL (REMAINDER A B) (FIX A))) ((ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA REMAINDER-OF-NON-NUMBER (REWRITE) (IMPLIES (NOT (NUMBERP A)) (EQUAL (REMAINDER A N) (REMAINDER 0 N))) ((ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA REMAINDER-ZERO (REWRITE) (IMPLIES (ZEROP X) (EQUAL (REMAINDER Y X) (FIX Y))) ((ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA PLUS-REMAINDER-TIMES-QUOTIENT (REWRITE) (EQUAL (PLUS (REMAINDER X Y) (TIMES Y (QUOTIENT X Y))) (FIX X)) ((ENABLE COMMUTATIVITY2-OF-PLUS COMMUTATIVITY-OF-PLUS TIMES-ZERO TIMES-ADD1 COMMUTATIVITY-OF-TIMES) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (TOGGLE PLUS-REMAINDER-TIMES-QUOTIENT-OFF PLUS-REMAINDER-TIMES-QUOTIENT T) (PROVE-LEMMA REMAINDER-QUOTIENT-ELIM (ELIM) (IMPLIES (AND (NOT (ZEROP Y)) (NUMBERP X)) (EQUAL (PLUS (REMAINDER X Y) (TIMES Y (QUOTIENT X Y))) X)) ((ENABLE PLUS-REMAINDER-TIMES-QUOTIENT) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA REMAINDER-ADD1 (REWRITE) (IMPLIES (EQUAL (REMAINDER A B) 0) (EQUAL (REMAINDER (ADD1 A) B) (REMAINDER 1 B))) ((ENABLE REMAINDER-NOOP) (ENABLE-THEORY ADDITION GROUND-ZERO) (INDUCT (REMAINDER A B)) (DISABLE-THEORY T))) (PROVE-LEMMA REMAINDER-PLUS-PROOF NIL (IMPLIES (EQUAL (REMAINDER B C) 0) (EQUAL (REMAINDER (PLUS A B) C) (REMAINDER A C))) ((ENABLE REMAINDER-NOOP) (ENABLE-THEORY ADDITION GROUND-ZERO) (INDUCT (REMAINDER B C)) (DISABLE-THEORY T))) (PROVE-LEMMA REMAINDER-PLUS (REWRITE) (IMPLIES (EQUAL (REMAINDER A C) 0) (AND (EQUAL (REMAINDER (PLUS A B) C) (REMAINDER B C)) (EQUAL (REMAINDER (PLUS B A) C) (REMAINDER B C)) (EQUAL (REMAINDER (PLUS X Y A) C) (REMAINDER (PLUS X Y) C)))) ((USE (REMAINDER-PLUS-PROOF (A B) (B A) (C C)) (REMAINDER-PLUS-PROOF (A A) (B B) (C C)) (REMAINDER-PLUS-PROOF (B A) (A (PLUS X Y)) (C C))) (ENABLE COMMUTATIVITY-OF-PLUS COMMUTATIVITY2-OF-PLUS ASSOCIATIVITY-OF-PLUS) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA EQUAL-REMAINDER-PLUS-0-PROOF NIL (IMPLIES (EQUAL (REMAINDER A C) 0) (EQUAL (EQUAL (REMAINDER (PLUS A B) C) 0) (EQUAL (REMAINDER B C) 0))) ((ENABLE REMAINDER-PLUS) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA EQUAL-REMAINDER-PLUS-0 (REWRITE) (IMPLIES (EQUAL (REMAINDER A C) 0) (AND (EQUAL (EQUAL (REMAINDER (PLUS A B) C) 0) (EQUAL (REMAINDER B C) 0)) (EQUAL (EQUAL (REMAINDER (PLUS B A) C) 0) (EQUAL (REMAINDER B C) 0)) (EQUAL (EQUAL (REMAINDER (PLUS X Y A) C) 0) (EQUAL (REMAINDER (PLUS X Y) C) 0)))) ((USE (EQUAL-REMAINDER-PLUS-0-PROOF (A A) (B B) (C C)) (EQUAL-REMAINDER-PLUS-0-PROOF (A B) (B A) (C C)) (EQUAL-REMAINDER-PLUS-0-PROOF (A A) (B (PLUS X Y)) (C C))) (ENABLE ASSOCIATIVITY-OF-PLUS COMMUTATIVITY-OF-PLUS COMMUTATIVITY2-OF-PLUS) (DO-NOT-INDUCT T) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA EQUAL-REMAINDER-PLUS-REMAINDER-PROOF NIL (IMPLIES (LESSP A C) (EQUAL (EQUAL (REMAINDER (PLUS A B) C) (REMAINDER B C)) (ZEROP A))) ((ENABLE REMAINDER-NOOP) (ENABLE-THEORY ADDITION GROUND-ZERO) (INDUCT (REMAINDER B C)) (DISABLE-THEORY T))) (PROVE-LEMMA EQUAL-REMAINDER-PLUS-REMAINDER (REWRITE) (IMPLIES (LESSP A C) (AND (EQUAL (EQUAL (REMAINDER (PLUS A B) C) (REMAINDER B C)) (ZEROP A)) (EQUAL (EQUAL (REMAINDER (PLUS B A) C) (REMAINDER B C)) (ZEROP A)))) ((USE (EQUAL-REMAINDER-PLUS-REMAINDER-PROOF (A A) (B B) (C C))) (ENABLE COMMUTATIVITY-OF-PLUS) (DO-NOT-INDUCT T) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (TOGGLE EQUAL-REMAINDER-PLUS-REMAINDER-OFF EQUAL-REMAINDER-PLUS-REMAINDER T) (PROVE-LEMMA REMAINDER-TIMES1-PROOF NIL (IMPLIES (EQUAL (REMAINDER B C) 0) (EQUAL (REMAINDER (TIMES A B) C) 0)) ((ENABLE-THEORY MULTIPLICATION ADDITION GROUND-ZERO) (ENABLE REMAINDER-PLUS REMAINDER-NOOP REMAINDER-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA REMAINDER-TIMES1 (REWRITE) (IMPLIES (EQUAL (REMAINDER B C) 0) (AND (EQUAL (REMAINDER (TIMES A B) C) 0) (EQUAL (REMAINDER (TIMES B A) C) 0))) ((USE (REMAINDER-TIMES1-PROOF (A A) (B B) (C C)) (REMAINDER-TIMES1-PROOF (A B) (B A) (C C))) (ENABLE COMMUTATIVITY-OF-TIMES) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA REMAINDER-TIMES1-INSTANCE-PROOF NIL (EQUAL (REMAINDER (TIMES X Y) Y) 0) ((ENABLE COMMUTATIVITY-OF-TIMES DIFFERENCE-PLUS-CANCELLATION REMAINDER-ZERO) (INDUCT (TIMES X Y)) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA REMAINDER-TIMES1-INSTANCE (REWRITE) (AND (EQUAL (REMAINDER (TIMES X Y) Y) 0) (EQUAL (REMAINDER (TIMES X Y) X) 0)) ((USE (REMAINDER-TIMES1-INSTANCE-PROOF (X X) (Y Y)) (REMAINDER-TIMES1-INSTANCE-PROOF (X Y) (Y X))) (ENABLE COMMUTATIVITY-OF-TIMES) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA REMAINDER-TIMES-TIMES-PROOF NIL (EQUAL (REMAINDER (TIMES X Y) (TIMES X Z)) (TIMES X (REMAINDER Y Z))) ((ENABLE-THEORY ADDITION MULTIPLICATION GROUND-ZERO) (ENABLE REMAINDER-ZERO) (INDUCT (REMAINDER Y Z)) (DISABLE-THEORY T))) (PROVE-LEMMA REMAINDER-TIMES-TIMES (REWRITE) (AND (EQUAL (REMAINDER (TIMES X Y) (TIMES X Z)) (TIMES X (REMAINDER Y Z))) (EQUAL (REMAINDER (TIMES X Z) (TIMES Y Z)) (TIMES (REMAINDER X Y) Z))) ((USE (REMAINDER-TIMES-TIMES-PROOF (X X) (Y Y) (Z Z)) (REMAINDER-TIMES-TIMES-PROOF (X Z) (Y X) (Z Y))) (ENABLE COMMUTATIVITY-OF-TIMES) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (TOGGLE REMAINDER-TIMES-TIMES-OFF REMAINDER-TIMES-TIMES T) (PROVE-LEMMA REMAINDER-TIMES2-PROOF NIL (IMPLIES (EQUAL (REMAINDER A Z) 0) (EQUAL (REMAINDER A (TIMES Z Y)) (TIMES Z (REMAINDER (QUOTIENT A Z) Y)))) ((ENABLE-THEORY ADDITION MULTIPLICATION GROUND-ZERO) (ENABLE LESSP-REMAINDER REMAINDER-NOOP REMAINDER-PLUS REMAINDER-QUOTIENT-ELIM REMAINDER-TIMES-TIMES REMAINDER-TIMES1-INSTANCE REMAINDER-ZERO) (DO-NOT-INDUCT T) (DISABLE-THEORY T))) (PROVE-LEMMA REMAINDER-TIMES2 (REWRITE) (IMPLIES (EQUAL (REMAINDER A Z) 0) (AND (EQUAL (REMAINDER A (TIMES Y Z)) (TIMES Z (REMAINDER (QUOTIENT A Z) Y))) (EQUAL (REMAINDER A (TIMES Z Y)) (TIMES Z (REMAINDER (QUOTIENT A Z) Y))))) ((USE (REMAINDER-TIMES2-PROOF (A A) (Y Y) (Z Z))) (ENABLE COMMUTATIVITY-OF-TIMES) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA REMAINDER-TIMES2-INSTANCE (REWRITE) (AND (EQUAL (REMAINDER (TIMES X Y) (TIMES X Z)) (TIMES X (REMAINDER Y Z))) (EQUAL (REMAINDER (TIMES X Z) (TIMES Y Z)) (TIMES (REMAINDER X Y) Z))) ((ENABLE REMAINDER-TIMES-TIMES) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA REMAINDER-DIFFERENCE1 (REWRITE) (IMPLIES (EQUAL (REMAINDER A C) (REMAINDER B C)) (EQUAL (REMAINDER (DIFFERENCE A B) C) (DIFFERENCE (REMAINDER A C) (REMAINDER B C)))) ((ENABLE LESSP-REMAINDER EQUAL-REMAINDER-PLUS-REMAINDER REMAINDER-PLUS REMAINDER-QUOTIENT-ELIM REMAINDER-TIMES1-INSTANCE) (ENABLE-THEORY ADDITION GROUND-ZERO) (DO-NOT-INDUCT T) (DISABLE-THEORY T))) (DEFN DOUBLE-REMAINDER-INDUCTION (A B C) (COND ((ZEROP C) 0) ((LESSP A C) 0) ((LESSP B C) 0) (T (DOUBLE-REMAINDER-INDUCTION (DIFFERENCE A C) (DIFFERENCE B C) C)))) (PROVE-LEMMA REMAINDER-DIFFERENCE2 (REWRITE) (IMPLIES (AND (EQUAL (REMAINDER A C) 0) (NOT (EQUAL (REMAINDER B C) 0))) (EQUAL (REMAINDER (DIFFERENCE A B) C) (IF (LESSP B A) (DIFFERENCE C (REMAINDER B C)) 0))) ((ENABLE EQUAL-REMAINDER-PLUS-0 LESSP-REMAINDER REMAINDER-NOOP REMAINDER-OF-NON-NUMBER REMAINDER-QUOTIENT-ELIM REMAINDER-TIMES1-INSTANCE REMAINDER-ZERO) (DISABLE TIMES-DISTRIBUTES-OVER-PLUS) (ENABLE-THEORY ADDITION MULTIPLICATION GROUND-ZERO) (INDUCT (DOUBLE-REMAINDER-INDUCTION A B C)) (DISABLE-THEORY T))) (PROVE-LEMMA REMAINDER-DIFFERENCE3 (REWRITE) (IMPLIES (AND (EQUAL (REMAINDER B C) 0) (NOT (EQUAL (REMAINDER A C) 0))) (EQUAL (REMAINDER (DIFFERENCE A B) C) (IF (LESSP B A) (REMAINDER A C) 0))) ((ENABLE REMAINDER-NOOP REMAINDER-OF-NON-NUMBER REMAINDER-ZERO) (ENABLE-THEORY ADDITION GROUND-ZERO) (INDUCT (DOUBLE-REMAINDER-INDUCTION A B C)) (DISABLE-THEORY T))) (TOGGLE REMAINDER-DIFFERENCE3-OFF REMAINDER-DIFFERENCE3 T) (PROVE-LEMMA EQUAL-REMAINDER-DIFFERENCE-0 (REWRITE) (EQUAL (EQUAL (REMAINDER (DIFFERENCE A B) C) 0) (IF (IF (LESSP A B) F T) (EQUAL (REMAINDER A C) (REMAINDER B C)) T)) ((ENABLE LESSP-REMAINDER REMAINDER-DIFFERENCE1 REMAINDER-OF-NON-NUMBER REMAINDER-PLUS REMAINDER-QUOTIENT-ELIM REMAINDER-TIMES1-INSTANCE REMAINDER-ZERO) (ENABLE-THEORY ADDITION GROUND-ZERO) (DO-NOT-INDUCT T) (DISABLE-THEORY T))) (TOGGLE EQUAL-REMAINDER-DIFFERENCE-0-OFF EQUAL-REMAINDER-DIFFERENCE-0 T) (PROVE-LEMMA LESSP-PLUS-FACT (REWRITE) (IMPLIES (AND (EQUAL (REMAINDER B X) 0) (EQUAL (REMAINDER C X) 0) (LESSP B C) (LESSP A X)) (EQUAL (LESSP (PLUS A B) C) T)) ((ENABLE-THEORY ADDITION GROUND-ZERO) (INDUCT (DOUBLE-REMAINDER-INDUCTION B C X)) (DISABLE-THEORY T))) (TOGGLE LESSP-PLUS-FACT-OFF LESSP-PLUS-FACT T) (PROVE-LEMMA REMAINDER-PLUS-FACT NIL (IMPLIES (AND (EQUAL (REMAINDER B X) 0) (EQUAL (REMAINDER C X) 0) (LESSP A X)) (EQUAL (REMAINDER (PLUS A B) C) (PLUS A (REMAINDER B C)))) ((ENABLE LESSP-PLUS-FACT REMAINDER-NOOP REMAINDER-DIFFERENCE1) (ENABLE-THEORY ADDITION MULTIPLICATION GROUND-ZERO) (INDUCT (REMAINDER B C)) (DISABLE-THEORY T))) (PROVE-LEMMA REMAINDER-PLUS-TIMES-TIMES-PROOF NIL (IMPLIES (LESSP A B) (EQUAL (REMAINDER (PLUS A (TIMES B C)) (TIMES B D)) (PLUS A (REMAINDER (TIMES B C) (TIMES B D))))) ((USE (REMAINDER-PLUS-FACT (A A) (X B) (B (TIMES B C)) (C (TIMES B D)))) (ENABLE REMAINDER-TIMES1-INSTANCE REMAINDER-TIMES2-INSTANCE) (DO-NOT-INDUCT T) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA REMAINDER-PLUS-TIMES-TIMES (REWRITE) (IMPLIES (LESSP A B) (AND (EQUAL (REMAINDER (PLUS A (TIMES B C)) (TIMES B D)) (PLUS A (REMAINDER (TIMES B C) (TIMES B D)))) (EQUAL (REMAINDER (PLUS A (TIMES C B)) (TIMES D B)) (PLUS A (REMAINDER (TIMES C B) (TIMES D B)))))) ((USE (REMAINDER-PLUS-TIMES-TIMES-PROOF (A A) (B B) (C C) (D D))) (ENABLE COMMUTATIVITY-OF-TIMES) (DO-NOT-INDUCT T) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA REMAINDER-PLUS-TIMES-TIMES-INSTANCE (REWRITE) (IMPLIES (LESSP A B) (AND (EQUAL (REMAINDER (PLUS A (TIMES B C) (TIMES B D)) (TIMES B E)) (PLUS A (TIMES B (REMAINDER (PLUS C D) E)))) (EQUAL (REMAINDER (PLUS A (TIMES C B) (TIMES D B)) (TIMES E B)) (PLUS A (TIMES B (REMAINDER (PLUS C D) E)))))) ((ENABLE COMMUTATIVITY-OF-TIMES REMAINDER-TIMES-TIMES REMAINDER-PLUS-TIMES-TIMES) (USE (TIMES-DISTRIBUTES-OVER-PLUS (X B) (Y C) (Z D))) (DO-NOT-INDUCT T) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA REMAINDER-REMAINDER (REWRITE) (IMPLIES (EQUAL (REMAINDER B A) 0) (EQUAL (REMAINDER (REMAINDER N B) A) (REMAINDER N A))) ((INDUCT (REMAINDER N B)) (ENABLE REMAINDER-PLUS REMAINDER-QUOTIENT-ELIM REMAINDER-ZERO) (ENABLE-THEORY ADDITION MULTIPLICATION GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA REMAINDER-1-ARG1 (REWRITE) (EQUAL (REMAINDER 1 X) (IF (EQUAL X 1) 0 1)) ((ENABLE DIFFERENCE-LEQ-ARG1) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA REMAINDER-1-ARG2 (REWRITE) (EQUAL (REMAINDER Y 1) 0) ((ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA REMAINDER-X-X (REWRITE) (EQUAL (REMAINDER X X) 0) ((ENABLE EQUAL-DIFFERENCE-0) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA TRANSITIVITY-OF-DIVIDES NIL (IMPLIES (AND (EQUAL (REMAINDER A B) 0) (EQUAL (REMAINDER B C) 0)) (EQUAL (REMAINDER A C) 0)) ((ENABLE REMAINDER REMAINDER-NOOP REMAINDER-PLUS) (ENABLE-THEORY ADDITION GROUND-ZERO) (DISABLE-THEORY T))) (DEFTHEORY REMAINDERS (LESSP-REMAINDER REMAINDER-NOOP REMAINDER-OF-NON-NUMBER REMAINDER-ZERO REMAINDER-QUOTIENT-ELIM REMAINDER-ADD1 REMAINDER-PLUS EQUAL-REMAINDER-PLUS-0 REMAINDER-TIMES1 REMAINDER-TIMES1-INSTANCE REMAINDER-TIMES2 REMAINDER-TIMES2-INSTANCE REMAINDER-DIFFERENCE1 REMAINDER-DIFFERENCE2 REMAINDER-PLUS-TIMES-TIMES REMAINDER-PLUS-TIMES-TIMES-INSTANCE REMAINDER-REMAINDER REMAINDER-1-ARG1 REMAINDER-1-ARG2 REMAINDER-X-X)) (PROVE-LEMMA QUOTIENT-NOOP (REWRITE) (IMPLIES (EQUAL B 1) (EQUAL (QUOTIENT A B) (FIX A))) ((ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA QUOTIENT-OF-NON-NUMBER (REWRITE) (IMPLIES (NOT (NUMBERP A)) (EQUAL (QUOTIENT A N) (QUOTIENT 0 N))) ((ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA QUOTIENT-ZERO (REWRITE) (IMPLIES (ZEROP X) (EQUAL (QUOTIENT Y X) 0)) ((ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA QUOTIENT-ADD1 (REWRITE) (IMPLIES (EQUAL (REMAINDER A B) 0) (EQUAL (QUOTIENT (ADD1 A) B) (IF (EQUAL B 1) (ADD1 (QUOTIENT A B)) (QUOTIENT A B)))) ((ENABLE QUOTIENT-NOOP) (ENABLE-THEORY ADDITION GROUND-ZERO) (INDUCT (REMAINDER A B)) (DISABLE-THEORY T))) (PROVE-LEMMA EQUAL-QUOTIENT-0 (REWRITE) (EQUAL (EQUAL (QUOTIENT A B) 0) (OR (ZEROP B) (LESSP A B))) ((INDUCT (QUOTIENT A B)) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA QUOTIENT-SUB1 (REWRITE) (IMPLIES (AND (NOT (ZEROP A)) (NOT (ZEROP B))) (EQUAL (QUOTIENT (SUB1 A) B) (IF (EQUAL (REMAINDER A B) 0) (SUB1 (QUOTIENT A B)) (QUOTIENT A B)))) ((ENABLE QUOTIENT-NOOP EQUAL-QUOTIENT-0) (ENABLE-THEORY ADDITION GROUND-ZERO) (INDUCT (REMAINDER A B)) (DISABLE-THEORY T))) (PROVE-LEMMA QUOTIENT-PLUS-PROOF NIL (IMPLIES (EQUAL (REMAINDER B C) 0) (EQUAL (QUOTIENT (PLUS A B) C) (PLUS (QUOTIENT A C) (QUOTIENT B C)))) ((ENABLE REMAINDER-NOOP) (ENABLE-THEORY ADDITION GROUND-ZERO) (INDUCT (REMAINDER B C)) (DISABLE-THEORY T))) (PROVE-LEMMA QUOTIENT-PLUS (REWRITE) (IMPLIES (EQUAL (REMAINDER A C) 0) (AND (EQUAL (QUOTIENT (PLUS A B) C) (PLUS (QUOTIENT A C) (QUOTIENT B C))) (EQUAL (QUOTIENT (PLUS B A) C) (PLUS (QUOTIENT A C) (QUOTIENT B C))) (EQUAL (QUOTIENT (PLUS X Y A) C) (PLUS (QUOTIENT (PLUS X Y) C) (QUOTIENT A C))))) ((USE (QUOTIENT-PLUS-PROOF (A B) (B A) (C C)) (QUOTIENT-PLUS-PROOF (A A) (B B) (C C)) (QUOTIENT-PLUS-PROOF (A (PLUS X Y)) (B A) (C C))) (ENABLE COMMUTATIVITY-OF-PLUS COMMUTATIVITY2-OF-PLUS ASSOCIATIVITY-OF-PLUS) (DO-NOT-INDUCT T) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA QUOTIENT-TIMES-INSTANCE-TEMP-PROOF NIL (EQUAL (QUOTIENT (TIMES Y X) Y) (IF (ZEROP Y) 0 (FIX X))) ((ENABLE TIMES-ZERO COMMUTATIVITY-OF-TIMES DIFFERENCE-PLUS-CANCELLATION) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA QUOTIENT-TIMES-INSTANCE-TEMP (REWRITE) (AND (EQUAL (QUOTIENT (TIMES Y X) Y) (IF (ZEROP Y) 0 (FIX X))) (EQUAL (QUOTIENT (TIMES X Y) Y) (IF (ZEROP Y) 0 (FIX X)))) ((USE (QUOTIENT-TIMES-INSTANCE-TEMP-PROOF (X X) (Y Y)) (QUOTIENT-TIMES-INSTANCE-TEMP-PROOF (X Y) (Y X))) (ENABLE COMMUTATIVITY-OF-TIMES) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (TOGGLE QUOTIENT-TIMES-INSTANCE-TEMP-OFF QUOTIENT-TIMES-INSTANCE-TEMP T) (PROVE-LEMMA QUOTIENT-TIMES-PROOF NIL (IMPLIES (EQUAL (REMAINDER A C) 0) (EQUAL (QUOTIENT (TIMES A B) C) (TIMES B (QUOTIENT A C)))) ((ENABLE-THEORY ADDITION MULTIPLICATION REMAINDERS GROUND-ZERO) (ENABLE QUOTIENT-PLUS QUOTIENT-NOOP EQUAL-QUOTIENT-0 QUOTIENT-TIMES-INSTANCE-TEMP) (INDUCT (REMAINDER A C)) (DISABLE-THEORY T))) (PROVE-LEMMA QUOTIENT-TIMES (REWRITE) (IMPLIES (EQUAL (REMAINDER A C) 0) (AND (EQUAL (QUOTIENT (TIMES A B) C) (TIMES B (QUOTIENT A C))) (EQUAL (QUOTIENT (TIMES B A) C) (TIMES B (QUOTIENT A C))))) ((ENABLE COMMUTATIVITY-OF-TIMES) (USE (QUOTIENT-TIMES-PROOF (A A) (B B) (C C))) (DO-NOT-INDUCT T) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA QUOTIENT-TIMES-INSTANCE (REWRITE) (AND (EQUAL (QUOTIENT (TIMES Y X) Y) (IF (ZEROP Y) 0 (FIX X))) (EQUAL (QUOTIENT (TIMES X Y) Y) (IF (ZEROP Y) 0 (FIX X)))) ((ENABLE QUOTIENT-TIMES-INSTANCE-TEMP) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA QUOTIENT-TIMES-TIMES-PROOF NIL (EQUAL (QUOTIENT (TIMES X Y) (TIMES X Z)) (IF (ZEROP X) 0 (QUOTIENT Y Z))) ((ENABLE-THEORY ADDITION GROUND-ZERO) (ENABLE LESSP-TIMES-CANCELLATION1 EQUAL-TIMES-0 TIMES-ZERO COMMUTATIVITY-OF-TIMES TIMES-DISTRIBUTES-OVER-DIFFERENCE) (INDUCT (QUOTIENT Y Z)) (DISABLE-THEORY T))) (PROVE-LEMMA QUOTIENT-TIMES-TIMES (REWRITE) (AND (EQUAL (QUOTIENT (TIMES X Y) (TIMES X Z)) (IF (ZEROP X) 0 (QUOTIENT Y Z))) (EQUAL (QUOTIENT (TIMES X Z) (TIMES Y Z)) (IF (ZEROP Z) 0 (QUOTIENT X Y)))) ((USE (QUOTIENT-TIMES-TIMES-PROOF (X X) (Y Y) (Z Z)) (QUOTIENT-TIMES-TIMES-PROOF (X Z) (Y X) (Z Y))) (ENABLE COMMUTATIVITY-OF-TIMES) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (TOGGLE QUOTIENT-TIMES-TIMES-OFF QUOTIENT-TIMES-TIMES T) (PROVE-LEMMA QUOTIENT-DIFFERENCE1 (REWRITE) (IMPLIES (EQUAL (REMAINDER A C) (REMAINDER B C)) (EQUAL (QUOTIENT (DIFFERENCE A B) C) (DIFFERENCE (QUOTIENT A C) (QUOTIENT B C)))) ((ENABLE-THEORY ADDITION MULTIPLICATION REMAINDERS GROUND-ZERO) (ENABLE QUOTIENT-PLUS QUOTIENT-TIMES-INSTANCE EQUAL-REMAINDER-PLUS-REMAINDER) (DO-NOT-INDUCT T) (DISABLE-THEORY T))) (PROVE-LEMMA QUOTIENT-LESSP-ARG1 (REWRITE) (IMPLIES (LESSP A B) (EQUAL (QUOTIENT A B) 0)) ((ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA QUOTIENT-DIFFERENCE2 (REWRITE) (IMPLIES (AND (EQUAL (REMAINDER A C) 0) (NOT (EQUAL (REMAINDER B C) 0))) (EQUAL (QUOTIENT (DIFFERENCE A B) C) (IF (LESSP B A) (DIFFERENCE (QUOTIENT A C) (ADD1 (QUOTIENT B C))) 0))) ((ENABLE EQUAL-QUOTIENT-0 EQUAL-REMAINDER-PLUS-0 QUOTIENT-TIMES-INSTANCE QUOTIENT-ZERO) (DISABLE TIMES-DISTRIBUTES-OVER-PLUS EQUAL-REMAINDER-DIFFERENCE-0 REMAINDER-DIFFERENCE3) (ENABLE-THEORY ADDITION MULTIPLICATION REMAINDERS GROUND-ZERO) (INDUCT (DOUBLE-REMAINDER-INDUCTION A B C)) (DISABLE-THEORY T))) (PROVE-LEMMA QUOTIENT-DIFFERENCE3 (REWRITE) (IMPLIES (AND (EQUAL (REMAINDER B C) 0) (NOT (EQUAL (REMAINDER A C) 0))) (EQUAL (QUOTIENT (DIFFERENCE A B) C) (IF (LESSP B A) (DIFFERENCE (QUOTIENT A C) (QUOTIENT B C)) 0))) ((ENABLE EQUAL-QUOTIENT-0 EQUAL-REMAINDER-PLUS-0 QUOTIENT-LESSP-ARG1 QUOTIENT-TIMES-INSTANCE QUOTIENT-ZERO) (DISABLE TIMES-DISTRIBUTES-OVER-PLUS EQUAL-REMAINDER-DIFFERENCE-0 REMAINDER-DIFFERENCE3) (ENABLE-THEORY ADDITION MULTIPLICATION REMAINDERS GROUND-ZERO) (INDUCT (DOUBLE-REMAINDER-INDUCTION A B C)) (DISABLE-THEORY T))) (PROVE-LEMMA REMAINDER-EQUALS-ITS-FIRST-ARGUMENT (REWRITE) (EQUAL (EQUAL A (REMAINDER A B)) (AND (NUMBERP A) (OR (ZEROP B) (LESSP A B)))) ((INDUCT (REMAINDER A B)) (ENABLE LESSP-REMAINDER REMAINDER-NOOP REMAINDER-ZERO) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (TOGGLE REMAINDER-EQUALS-ITS-FIRST-ARGUMENT-OFF REMAINDER-EQUALS-ITS-FIRST-ARGUMENT T) (PROVE-LEMMA QUOTIENT-REMAINDER-TIMES (REWRITE) (EQUAL (QUOTIENT (REMAINDER X (TIMES A B)) A) (REMAINDER (QUOTIENT X A) B)) ((ENABLE-THEORY ADDITION MULTIPLICATION REMAINDERS GROUND-ZERO) (ENABLE REMAINDER-EQUALS-ITS-FIRST-ARGUMENT QUOTIENT-NOOP QUOTIENT-PLUS QUOTIENT-TIMES-INSTANCE QUOTIENT-ZERO) (DO-NOT-INDUCT T) (DISABLE-THEORY T))) (PROVE-LEMMA QUOTIENT-REMAINDER (REWRITE) (IMPLIES (EQUAL (REMAINDER C A) 0) (EQUAL (QUOTIENT (REMAINDER B C) A) (REMAINDER (QUOTIENT B A) (QUOTIENT C A)))) ((ENABLE-THEORY ADDITION MULTIPLICATION REMAINDERS GROUND-ZERO) (ENABLE QUOTIENT-NOOP QUOTIENT-PLUS QUOTIENT-REMAINDER-TIMES QUOTIENT-TIMES-INSTANCE QUOTIENT-ZERO) (DO-NOT-INDUCT T) (DISABLE-THEORY T))) (PROVE-LEMMA QUOTIENT-REMAINDER-INSTANCE (REWRITE) (EQUAL (QUOTIENT (REMAINDER X (TIMES A B)) A) (REMAINDER (QUOTIENT X A) B)) ((ENABLE QUOTIENT-REMAINDER QUOTIENT-TIMES-INSTANCE REMAINDER-TIMES1-INSTANCE) (DO-NOT-INDUCT T) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA QUOTIENT-PLUS-FACT NIL (IMPLIES (AND (EQUAL (REMAINDER B X) 0) (EQUAL (REMAINDER C X) 0) (LESSP A X)) (EQUAL (QUOTIENT (PLUS A B) C) (QUOTIENT B C))) ((ENABLE QUOTIENT-LESSP-ARG1 LESSP-PLUS-FACT) (ENABLE-THEORY ADDITION MULTIPLICATION REMAINDERS GROUND-ZERO) (INDUCT (QUOTIENT B C)) (DISABLE-THEORY T))) (PROVE-LEMMA QUOTIENT-PLUS-TIMES-TIMES-PROOF NIL (IMPLIES (LESSP A B) (EQUAL (QUOTIENT (PLUS A (TIMES B C)) (TIMES B D)) (QUOTIENT (TIMES B C) (TIMES B D)))) ((USE (QUOTIENT-PLUS-FACT (A A) (X B) (B (TIMES B C)) (C (TIMES B D)))) (ENABLE REMAINDER-TIMES1-INSTANCE) (DO-NOT-INDUCT T) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA QUOTIENT-PLUS-TIMES-TIMES (REWRITE) (IMPLIES (LESSP A B) (AND (EQUAL (QUOTIENT (PLUS A (TIMES B C)) (TIMES B D)) (QUOTIENT (TIMES B C) (TIMES B D))) (EQUAL (QUOTIENT (PLUS A (TIMES B C)) (TIMES B D)) (QUOTIENT (TIMES B C) (TIMES B D))))) ((USE (QUOTIENT-PLUS-TIMES-TIMES-PROOF (A A) (B B) (C C) (D D))) (ENABLE COMMUTATIVITY-OF-TIMES) (DO-NOT-INDUCT T) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA QUOTIENT-PLUS-TIMES-TIMES-INSTANCE (REWRITE) (IMPLIES (LESSP A B) (AND (EQUAL (QUOTIENT (PLUS A (TIMES B C) (TIMES B D)) (TIMES B E)) (IF (ZEROP B) 0 (QUOTIENT (PLUS C D) E))) (EQUAL (QUOTIENT (PLUS A (TIMES C B) (TIMES D B)) (TIMES E B)) (IF (ZEROP B) 0 (QUOTIENT (PLUS D C) E))))) ((ENABLE COMMUTATIVITY-OF-TIMES COMMUTATIVITY-OF-PLUS QUOTIENT-TIMES-TIMES QUOTIENT-PLUS-TIMES-TIMES) (USE (TIMES-DISTRIBUTES-OVER-PLUS (X B) (Y C) (Z D))) (DO-NOT-INDUCT T) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA QUOTIENT-QUOTIENT (REWRITE) (EQUAL (QUOTIENT (QUOTIENT B A) C) (QUOTIENT B (TIMES A C))) ((ENABLE-THEORY ADDITION MULTIPLICATION REMAINDERS GROUND-ZERO) (DISABLE TIMES-DISTRIBUTES-OVER-PLUS) (ENABLE QUOTIENT-LESSP-ARG1 QUOTIENT-PLUS QUOTIENT-PLUS-TIMES-TIMES QUOTIENT-TIMES-INSTANCE QUOTIENT-TIMES-TIMES QUOTIENT-NOOP QUOTIENT-ZERO) (DO-NOT-INDUCT T) (DISABLE-THEORY T))) (PROVE-LEMMA LEQ-QUOTIENT NIL (IMPLIES (LESSP A B) (IF (LESSP (QUOTIENT B C) (QUOTIENT A C)) F T)) ((INDUCT (DOUBLE-REMAINDER-INDUCTION A B C)) (ENABLE QUOTIENT-LESSP-ARG1 QUOTIENT-ZERO) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA QUOTIENT-1-ARG2 (REWRITE) (EQUAL (QUOTIENT N 1) (FIX N)) ((ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA QUOTIENT-1-ARG1-CASESPLIT NIL (OR (ZEROP N) (EQUAL N 1) (LESSP 1 N)) ((ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA QUOTIENT-1-ARG1 (REWRITE) (EQUAL (QUOTIENT 1 N) (IF (EQUAL N 1) 1 0)) ((ENABLE QUOTIENT-LESSP-ARG1) (USE (QUOTIENT-1-ARG1-CASESPLIT)) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA QUOTIENT-X-X (REWRITE) (IMPLIES (NOT (ZEROP X)) (EQUAL (QUOTIENT X X) 1)) ((ENABLE DIFFERENCE-X-X) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA LESSP-QUOTIENT (REWRITE) (EQUAL (LESSP (QUOTIENT I J) I) (AND (NOT (ZEROP I)) (NOT (EQUAL J 1)))) ((ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (DEFN CANCEL-QUOTIENT-TIMES (X) (IF (AND (EQUAL (CAR X) 'QUOTIENT) (EQUAL (CAADR X) 'TIMES) (EQUAL (CAADDR X) 'TIMES)) (IF (LISTP (BAGINT (TIMES-FRINGE (CADR X)) (TIMES-FRINGE (CADDR X)))) (CONS 'IF (CONS (AND-NOT-ZEROP-TREE (BAGINT (TIMES-FRINGE (CADR X)) (TIMES-FRINGE (CADDR X)))) (CONS (LIST 'QUOTIENT (TIMES-TREE (BAGDIFF (TIMES-FRINGE (CADR X)) (BAGINT (TIMES-FRINGE (CADR X)) (TIMES-FRINGE (CADDR X))))) (TIMES-TREE (BAGDIFF (TIMES-FRINGE (CADDR X)) (BAGINT (TIMES-FRINGE (CADR X)) (TIMES-FRINGE (CADDR X)))))) '((ZERO))))) X) X)) (PROVE-LEMMA ZEROP-MAKES-QUOTIENT-ZERO-BRIDGE (REWRITE) (IMPLIES (AND (EQUAL (CAR X) 'TIMES) (EQUAL (CAR Y) 'TIMES) (NOT (EVAL$ T (AND-NOT-ZEROP-TREE (BAGINT (TIMES-FRINGE X) (TIMES-FRINGE Y))) A))) (EQUAL (QUOTIENT (TIMES (EVAL$ T (CADR X) A) (EVAL$ T (CADDR X) A)) (TIMES (EVAL$ T (CADR Y) A) (EVAL$ T (CADDR Y) A))) 0)) ((USE (ZEROP-MAKES-TIMES-TREE-ZERO (X (BAGINT (TIMES-FRINGE X) (TIMES-FRINGE Y))) (Y (TIMES-FRINGE X))) (ZEROP-MAKES-TIMES-TREE-ZERO (X (BAGINT (TIMES-FRINGE X) (TIMES-FRINGE Y))) (Y (TIMES-FRINGE Y)))) (ENABLE AND-NOT-ZEROP-TREE BAGINT DELETE EQUAL-QUOTIENT-0 EQUAL-TIMES-0 EVAL$-TIMES SUBBAGP-BAGINT1 SUBBAGP-BAGINT2 TIMES-FRINGE TIMES-TREE TIMES-TREE-APPEND TIMES-TREE-OF-TIMES-FRINGE ZEROP-MAKES-LESSP-FALSE-BRIDGE) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (TOGGLE ZEROP-MAKES-QUOTIENT-ZERO-BRIDGE-OFF ZEROP-MAKES-QUOTIENT-ZERO-BRIDGE T) (PROVE-LEMMA EVAL$-QUOTIENT-TIMES-TREE-BAGDIFF (REWRITE) (IMPLIES (AND (SUBBAGP X Y) (SUBBAGP X Z) (EVAL$ T (AND-NOT-ZEROP-TREE X) A)) (EQUAL (QUOTIENT (EVAL$ T (TIMES-TREE (BAGDIFF Y X)) A) (EVAL$ T (TIMES-TREE (BAGDIFF Z X)) A)) (QUOTIENT (EVAL$ T (TIMES-TREE Y) A) (EVAL$ T (TIMES-TREE Z) A)))) ((ENABLE AND-NOT-ZEROP-TREE BAGDIFF EQUAL-QUOTIENT-0 EVAL$-TIMES-MEMBER NUMBERP-EVAL$-TIMES-TREE QUOTIENT-TIMES-TIMES SUBBAGP SUBBAGP-CDR1 SUBBAGP-CDR2 TIMES-TREE ZEROP-MAKES-TIMES-TREE-ZERO) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (TOGGLE EVAL$-QUOTIENT-TIMES-TREE-BAGDIFF-OFF EVAL$-QUOTIENT-TIMES-TREE-BAGDIFF T) (PROVE-LEMMA CORRECTNESS-OF-CANCEL-QUOTIENT-TIMES ((META QUOTIENT)) (EQUAL (EVAL$ T X A) (EVAL$ T (CANCEL-QUOTIENT-TIMES X) A)) ((ENABLE CANCEL-QUOTIENT-TIMES EVAL$-QUOTIENT-TIMES-TREE-BAGDIFF EVAL$-QUOTIENT EVAL$-TIMES SUBBAGP-BAGINT1 SUBBAGP-BAGINT2 TIMES-TREE-OF-TIMES-FRINGE ZEROP-MAKES-QUOTIENT-ZERO-BRIDGE) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (DEFTHEORY QUOTIENTS (QUOTIENT-NOOP QUOTIENT-OF-NON-NUMBER QUOTIENT-ZERO QUOTIENT-ADD1 EQUAL-QUOTIENT-0 QUOTIENT-SUB1 QUOTIENT-PLUS QUOTIENT-TIMES QUOTIENT-TIMES-INSTANCE QUOTIENT-DIFFERENCE1 QUOTIENT-LESSP-ARG1 QUOTIENT-DIFFERENCE2 QUOTIENT-DIFFERENCE3 QUOTIENT-REMAINDER-TIMES QUOTIENT-REMAINDER QUOTIENT-REMAINDER-INSTANCE QUOTIENT-PLUS-TIMES-TIMES QUOTIENT-PLUS-TIMES-TIMES-INSTANCE QUOTIENT-QUOTIENT QUOTIENT-1-ARG2 QUOTIENT-1-ARG1 QUOTIENT-X-X LESSP-QUOTIENT CORRECTNESS-OF-CANCEL-QUOTIENT-TIMES)) (DEFN EXP (I J) (IF (ZEROP J) 1 (TIMES I (EXP I (SUB1 J))))) (DEFN LOG (BASE N) (COND ((LESSP BASE 2) 0) ((ZEROP N) 0) (T (ADD1 (LOG BASE (QUOTIENT N BASE)))))) (DEFN GCD (X Y) (COND ((ZEROP X) (FIX Y)) ((ZEROP Y) X) ((LESSP X Y) (GCD X (DIFFERENCE Y X))) (T (GCD (DIFFERENCE X Y) Y))) ((ORD-LESSP (CONS (ADD1 X) (FIX Y))))) (PROVE-LEMMA REMAINDER-EXP (REWRITE) (IMPLIES (NOT (ZEROP K)) (EQUAL (REMAINDER (EXP N K) N) 0)) ((ENABLE EXP REMAINDER-TIMES1-INSTANCE) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (DEFN DOUBLE-NUMBER-INDUCTION (I J) (COND ((ZEROP I) 0) ((ZEROP J) 0) (T (DOUBLE-NUMBER-INDUCTION (SUB1 I) (SUB1 J))))) (PROVE-LEMMA REMAINDER-EXP-EXP (REWRITE) (IMPLIES (IF (LESSP J I) F T) (EQUAL (REMAINDER (EXP A J) (EXP A I)) 0)) ((ENABLE EXP REMAINDER-1-ARG2 REMAINDER-TIMES2-INSTANCE) (ENABLE-THEORY ADDITION MULTIPLICATION GROUND-ZERO) (INDUCT (DOUBLE-NUMBER-INDUCTION I J)) (DISABLE-THEORY T))) (PROVE-LEMMA QUOTIENT-EXP (REWRITE) (IMPLIES (NOT (ZEROP K)) (EQUAL (QUOTIENT (EXP N K) N) (IF (ZEROP N) 0 (EXP N (SUB1 K))))) ((ENABLE EXP QUOTIENT-TIMES-INSTANCE) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA EXP-ZERO (REWRITE) (IMPLIES (ZEROP K) (EQUAL (EXP N K) 1)) ((ENABLE EXP) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA EXP-ADD1 (REWRITE) (EQUAL (EXP N (ADD1 K)) (TIMES N (EXP N K))) ((ENABLE EXP) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA EXP-PLUS (REWRITE) (EQUAL (EXP I (PLUS J K)) (TIMES (EXP I J) (EXP I K))) ((ENABLE EXP ASSOCIATIVITY-OF-TIMES COMMUTATIVITY-OF-TIMES) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA EXP-0-ARG1 (REWRITE) (EQUAL (EXP 0 K) (IF (ZEROP K) 1 0)) ((ENABLE EXP) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA EXP-1-ARG1 (REWRITE) (EQUAL (EXP 1 K) 1) ((ENABLE EXP) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA EXP-0-ARG2 (REWRITE) (EQUAL (EXP N 0) 1) ((ENABLE EXP) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA EXP-TIMES (REWRITE) (EQUAL (EXP (TIMES I J) K) (TIMES (EXP I K) (EXP J K))) ((ENABLE EXP ASSOCIATIVITY-OF-TIMES COMMUTATIVITY2-OF-TIMES EXP-ZERO) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA EXP-EXP (REWRITE) (EQUAL (EXP (EXP I J) K) (EXP I (TIMES J K))) ((ENABLE EXP EXP-ZERO EXP-1-ARG1 EXP-PLUS EXP-TIMES) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA EQUAL-EXP-0 (REWRITE) (EQUAL (EQUAL (EXP N K) 0) (AND (ZEROP N) (NOT (ZEROP K)))) ((ENABLE EXP EQUAL-TIMES-0) (INDUCT (EXP N K)) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA EQUAL-EXP-1 (REWRITE) (EQUAL (EQUAL (EXP N K) 1) (IF (ZEROP K) T (EQUAL N 1))) ((ENABLE EXP TIMES-ZERO TIMES-ADD1) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA EXP-DIFFERENCE (REWRITE) (IMPLIES (AND (IF (LESSP B C) F T) (NOT (ZEROP A))) (EQUAL (EXP A (DIFFERENCE B C)) (QUOTIENT (EXP A B) (EXP A C)))) ((ENABLE EXP) (ENABLE-THEORY ADDITION MULTIPLICATION REMAINDERS QUOTIENTS GROUND-ZERO) (DISABLE-THEORY T))) (DEFTHEORY EXPONENTIATION (EQUAL-EXP-0 EQUAL-EXP-1 EXP-EXP EXP-ADD1 EXP-TIMES EXP-1-ARG1 EXP-ZERO EXP-0-ARG2 EXP-0-ARG1 EXP-DIFFERENCE EXP-PLUS QUOTIENT-EXP REMAINDER-EXP-EXP REMAINDER-EXP)) (PROVE-LEMMA EQUAL-LOG-0 (REWRITE) (EQUAL (EQUAL (LOG BASE N) 0) (OR (LESSP BASE 2) (ZEROP N))) ((ENABLE LOG) (INDUCT (LOG BASE N)) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA LOG-0 (REWRITE) (IMPLIES (ZEROP N) (EQUAL (LOG BASE N) 0)) ((ENABLE LOG) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA LOG-1 (REWRITE) (IMPLIES (LESSP 1 BASE) (EQUAL (LOG BASE 1) 1)) ((ENABLE LOG) (INDUCT (LOG BASE N)) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (DEFN DOUBLE-LOG-INDUCTION (BASE A B) (COND ((LESSP BASE 2) 0) ((ZEROP A) 0) ((ZEROP B) 0) (T (DOUBLE-LOG-INDUCTION BASE (QUOTIENT A BASE) (QUOTIENT B BASE))))) (PROVE-LEMMA LEQ-LOG-LOG NIL (IMPLIES (IF (LESSP M N) F T) (IF (LESSP (LOG C M) (LOG C N)) F T)) ((ENABLE LOG) (INDUCT (DOUBLE-LOG-INDUCTION C N M)) (USE (LEQ-QUOTIENT (A N) (B M) (C C))) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA LOG-QUOTIENT (REWRITE) (IMPLIES (LESSP 1 C) (EQUAL (LOG C (QUOTIENT N C)) (SUB1 (LOG C N)))) ((ENABLE LOG) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA LOG-QUOTIENT-TIMES-PROOF NIL (IMPLIES (LESSP 1 C) (EQUAL (LOG C (QUOTIENT N (TIMES C M))) (SUB1 (LOG C (QUOTIENT N M))))) ((ENABLE LOG) (ENABLE-THEORY ADDITION MULTIPLICATION REMAINDERS QUOTIENTS GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA LOG-QUOTIENT-TIMES (REWRITE) (IMPLIES (LESSP 1 C) (AND (EQUAL (LOG C (QUOTIENT N (TIMES C M))) (SUB1 (LOG C (QUOTIENT N M)))) (EQUAL (LOG C (QUOTIENT N (TIMES M C))) (SUB1 (LOG C (QUOTIENT N M)))))) ((USE (LOG-QUOTIENT-TIMES-PROOF (C C) (N N) (M M))) (ENABLE COMMUTATIVITY-OF-TIMES) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA LOG-QUOTIENT-EXP (REWRITE) (IMPLIES (LESSP 1 C) (EQUAL (LOG C (QUOTIENT N (EXP C M))) (DIFFERENCE (LOG C N) M))) ((ENABLE EXP LOG LOG-QUOTIENT-TIMES) (ENABLE-THEORY ADDITION MULTIPLICATION REMAINDERS QUOTIENTS GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA LOG-TIMES-PROOF NIL (IMPLIES (AND (LESSP 1 C) (NOT (ZEROP N))) (EQUAL (LOG C (TIMES C N)) (ADD1 (LOG C N)))) ((ENABLE LOG) (ENABLE-THEORY ADDITION MULTIPLICATION REMAINDERS QUOTIENTS GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA LOG-TIMES (REWRITE) (IMPLIES (AND (LESSP 1 C) (NOT (ZEROP N))) (AND (EQUAL (LOG C (TIMES C N)) (ADD1 (LOG C N))) (EQUAL (LOG C (TIMES N C)) (ADD1 (LOG C N))))) ((USE (LOG-TIMES-PROOF (C C) (N N))) (ENABLE COMMUTATIVITY-OF-TIMES) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA LOG-TIMES-EXP-PROOF NIL (IMPLIES (AND (LESSP 1 C) (NOT (ZEROP N))) (EQUAL (LOG C (TIMES N (EXP C M))) (PLUS (LOG C N) M))) ((ENABLE LOG EXP) (ENABLE-THEORY ADDITION MULTIPLICATION REMAINDERS QUOTIENTS GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA LOG-TIMES-EXP (REWRITE) (IMPLIES (AND (LESSP 1 C) (NOT (ZEROP N))) (AND (EQUAL (LOG C (TIMES N (EXP C M))) (PLUS (LOG C N) M)) (EQUAL (LOG C (TIMES (EXP C M) N)) (PLUS (LOG C N) M)))) ((USE (LOG-TIMES-EXP-PROOF (C C) (N N) (M M))) (ENABLE COMMUTATIVITY-OF-TIMES) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA LOG-EXP (REWRITE) (IMPLIES (LESSP 1 C) (EQUAL (LOG C (EXP C N)) (ADD1 N))) ((ENABLE LOG EXP LOG-1) (ENABLE-THEORY ADDITION MULTIPLICATION REMAINDERS QUOTIENTS GROUND-ZERO) (DISABLE-THEORY T))) (DEFTHEORY LOGS (LOG-EXP LOG-TIMES-EXP LOG-TIMES LOG-QUOTIENT-EXP LOG-QUOTIENT-TIMES LOG-QUOTIENT LOG-1 LOG-0 EQUAL-LOG-0 EXP-EXP)) (PROVE-LEMMA COMMUTATIVITY-OF-GCD (REWRITE) (EQUAL (GCD B A) (GCD A B)) ((ENABLE GCD) (ENABLE-THEORY ADDITION GROUND-ZERO) (DISABLE-THEORY T))) (DEFN SINGLE-NUMBER-INDUCTION (N) (IF (ZEROP N) 0 (SINGLE-NUMBER-INDUCTION (SUB1 N)))) (PROVE-LEMMA GCD-0 (REWRITE) (AND (EQUAL (GCD 0 X) (FIX X)) (EQUAL (GCD X 0) (FIX X))) ((ENABLE GCD) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA GCD-1 (REWRITE) (AND (EQUAL (GCD 1 X) 1) (EQUAL (GCD X 1) 1)) ((ENABLE GCD) (ENABLE-THEORY ADDITION GROUND-ZERO) (INDUCT (SINGLE-NUMBER-INDUCTION X)) (DISABLE-THEORY T))) (PROVE-LEMMA EQUAL-GCD-0 (REWRITE) (EQUAL (EQUAL (GCD A B) 0) (AND (ZEROP A) (ZEROP B))) ((ENABLE GCD) (ENABLE-THEORY ADDITION GROUND-ZERO) (INDUCT (GCD A B)) (DISABLE-THEORY T))) (PROVE-LEMMA LESSP-GCD (REWRITE) (IMPLIES (NOT (ZEROP B)) (AND (EQUAL (LESSP B (GCD A B)) F) (EQUAL (LESSP B (GCD B A)) F))) ((ENABLE GCD COMMUTATIVITY-OF-GCD) (ENABLE-THEORY ADDITION GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA GCD-PLUS-INSTANCE-TEMP-PROOF NIL (EQUAL (GCD A (PLUS A B)) (GCD A B)) ((ENABLE GCD COMMUTATIVITY-OF-GCD) (ENABLE-THEORY ADDITION GROUND-ZERO) (INDUCT (GCD A B)) (DISABLE-THEORY T))) (PROVE-LEMMA GCD-PLUS-INSTANCE-TEMP (REWRITE) (AND (EQUAL (GCD A (PLUS A B)) (GCD A B)) (EQUAL (GCD A (PLUS B A)) (GCD A B))) ((ENABLE COMMUTATIVITY-OF-PLUS) (USE (GCD-PLUS-INSTANCE-TEMP-PROOF (A A) (B B))) (DO-NOT-INDUCT T) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA GCD-PLUS-PROOF NIL (IMPLIES (EQUAL (REMAINDER B A) 0) (EQUAL (GCD A (PLUS B C)) (GCD A C))) ((ENABLE GCD COMMUTATIVITY-OF-GCD GCD-1 GCD-PLUS-INSTANCE-TEMP) (ENABLE-THEORY ADDITION GROUND-ZERO) (INDUCT (REMAINDER B A)) (DISABLE-THEORY T))) (PROVE-LEMMA GCD-PLUS (REWRITE) (IMPLIES (EQUAL (REMAINDER B A) 0) (AND (EQUAL (GCD A (PLUS B C)) (GCD A C)) (EQUAL (GCD A (PLUS C B)) (GCD A C)) (EQUAL (GCD (PLUS B C) A) (GCD A C)) (EQUAL (GCD (PLUS C B) A) (GCD A C)))) ((ENABLE COMMUTATIVITY-OF-PLUS COMMUTATIVITY-OF-GCD) (USE (GCD-PLUS-PROOF (A A) (B B) (C C))) (DO-NOT-INDUCT T) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA GCD-PLUS-INSTANCE (REWRITE) (AND (EQUAL (GCD A (PLUS A B)) (GCD A B)) (EQUAL (GCD A (PLUS B A)) (GCD A B))) ((ENABLE GCD-PLUS-INSTANCE-TEMP) (DO-NOT-INDUCT T) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA REMAINDER-GCD (REWRITE) (AND (EQUAL (REMAINDER A (GCD A B)) 0) (EQUAL (REMAINDER B (GCD A B)) 0)) ((ENABLE GCD) (ENABLE-THEORY ADDITION REMAINDERS GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA DISTRIBUTIVITY-OF-TIMES-OVER-GCD-PROOF NIL (EQUAL (GCD (TIMES X Z) (TIMES Y Z)) (TIMES Z (GCD X Y))) ((ENABLE GCD COMMUTATIVITY-OF-GCD GCD-0 GCD-PLUS) (ENABLE-THEORY ADDITION MULTIPLICATION REMAINDERS GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA DISTRIBUTIVITY-OF-TIMES-OVER-GCD (REWRITE) (AND (EQUAL (GCD (TIMES X Z) (TIMES Y Z)) (TIMES Z (GCD X Y))) (EQUAL (GCD (TIMES Z X) (TIMES Y Z)) (TIMES Z (GCD X Y))) (EQUAL (GCD (TIMES X Z) (TIMES Z Y)) (TIMES Z (GCD X Y))) (EQUAL (GCD (TIMES Z X) (TIMES Z Y)) (TIMES Z (GCD X Y)))) ((USE (DISTRIBUTIVITY-OF-TIMES-OVER-GCD-PROOF (X X) (Y Y) (Z Z))) (ENABLE COMMUTATIVITY-OF-TIMES) (DO-NOT-INDUCT T) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA GCD-IS-THE-GREATEST NIL (IMPLIES (AND (NOT (ZEROP X)) (NOT (ZEROP Y)) (EQUAL (REMAINDER X Z) 0) (EQUAL (REMAINDER Y Z) 0)) (IF (LESSP (GCD X Y) Z) F T)) ((ENABLE GCD COMMUTATIVITY-OF-GCD DISTRIBUTIVITY-OF-TIMES-OVER-GCD EQUAL-GCD-0) (ENABLE-THEORY ADDITION MULTIPLICATION REMAINDERS GROUND-ZERO) (DO-NOT-INDUCT T) (DISABLE-THEORY T))) (PROVE-LEMMA COMMON-DIVISOR-DIVIDES-GCD (REWRITE) (IMPLIES (AND (EQUAL (REMAINDER X Z) 0) (EQUAL (REMAINDER Y Z) 0)) (EQUAL (REMAINDER (GCD X Y) Z) 0)) ((ENABLE GCD COMMUTATIVITY-OF-GCD DISTRIBUTIVITY-OF-TIMES-OVER-GCD EQUAL-GCD-0) (ENABLE-THEORY ADDITION MULTIPLICATION REMAINDERS GROUND-ZERO) (DO-NOT-INDUCT T) (DISABLE-THEORY T))) (PROVE-LEMMA ASSOCIATIVITY-OF-GCD-ZERO-CASE NIL (IMPLIES (OR (ZEROP A) (ZEROP B) (ZEROP C)) (EQUAL (GCD (GCD A B) C) (GCD A (GCD B C)))) ((ENABLE GCD GCD-0) (DO-NOT-INDUCT T) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA ASSOCIATIVITY-OF-GCD (REWRITE) (EQUAL (GCD (GCD A B) C) (GCD A (GCD B C))) ((ENABLE EQUAL-GCD-0 REMAINDER-GCD) (USE (GCD-IS-THE-GREATEST (X A) (Y (GCD B C)) (Z (GCD (GCD A B) C))) (GCD-IS-THE-GREATEST (X (GCD A B)) (Y C) (Z (GCD A (GCD B C)))) (ASSOCIATIVITY-OF-GCD-ZERO-CASE (A A) (B B) (C C)) (TRANSITIVITY-OF-DIVIDES (A A) (B (GCD A B)) (C (GCD (GCD A B) C))) (TRANSITIVITY-OF-DIVIDES (A B) (B (GCD A B)) (C (GCD (GCD A B) C))) (TRANSITIVITY-OF-DIVIDES (A B) (B (GCD B C)) (C (GCD A (GCD B C)))) (TRANSITIVITY-OF-DIVIDES (A C) (B (GCD B C)) (C (GCD A (GCD B C)))) (COMMON-DIVISOR-DIVIDES-GCD (X B) (Y C) (Z (GCD (GCD A B) C))) (COMMON-DIVISOR-DIVIDES-GCD (X A) (Y B) (Z (GCD A (GCD B C))))) (DO-NOT-INDUCT T) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA COMMUTATIVITY2-OF-GCD-ZERO-CASE NIL (IMPLIES (OR (ZEROP A) (ZEROP B) (ZEROP C)) (EQUAL (GCD B (GCD A C)) (GCD A (GCD B C)))) ((ENABLE GCD GCD-0 COMMUTATIVITY-OF-GCD) (DO-NOT-INDUCT T) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA COMMUTATIVITY2-OF-GCD (REWRITE) (EQUAL (GCD B (GCD A C)) (GCD A (GCD B C))) ((ENABLE EQUAL-GCD-0 REMAINDER-GCD) (USE (GCD-IS-THE-GREATEST (X A) (Y (GCD B C)) (Z (GCD B (GCD A C)))) (GCD-IS-THE-GREATEST (X B) (Y (GCD A C)) (Z (GCD A (GCD B C)))) (COMMUTATIVITY2-OF-GCD-ZERO-CASE (A A) (B B) (C C)) (TRANSITIVITY-OF-DIVIDES (A A) (B (GCD A C)) (C (GCD B (GCD A C)))) (TRANSITIVITY-OF-DIVIDES (A C) (B (GCD A C)) (C (GCD B (GCD A C)))) (TRANSITIVITY-OF-DIVIDES (A B) (B (GCD B C)) (C (GCD A (GCD B C)))) (TRANSITIVITY-OF-DIVIDES (A C) (B (GCD B C)) (C (GCD A (GCD B C)))) (COMMON-DIVISOR-DIVIDES-GCD (X B) (Y C) (Z (GCD B (GCD A C)))) (COMMON-DIVISOR-DIVIDES-GCD (X A) (Y C) (Z (GCD A (GCD B C))))) (DO-NOT-INDUCT T) (ENABLE-THEORY GROUND-ZERO) (DISABLE-THEORY T))) (PROVE-LEMMA GCD-X-X (REWRITE) (EQUAL (GCD X X) (FIX X)) ((ENABLE GCD) (ENABLE-THEORY ADDITION GROUND-ZERO) (INDUCT (SINGLE-NUMBER-INDUCTION X)) (DISABLE-THEORY T))) (PROVE-LEMMA GCD-IDEMPOTENCE (REWRITE) (AND (EQUAL (GCD X (GCD X Y)) (GCD X Y)) (EQUAL (GCD Y (GCD X Y)) (GCD X Y))) ((ENABLE GCD GCD-X-X GCD-PLUS REMAINDER-GCD GCD-1 COMMUTATIVITY-OF-GCD) (ENABLE-THEORY ADDITION GROUND-ZERO) (INDUCT (GCD X Y)) (DISABLE-THEORY T))) (DEFTHEORY GCDS (COMMUTATIVITY2-OF-GCD ASSOCIATIVITY-OF-GCD