#|

 Copyright (C) 1994 by Computational Logic, Inc.  All Rights Reserved.

 This script is hereby placed in the public domain, and therefore unlimited
 editing and redistribution is permitted.

 NO WARRANTY

 Computational Logic, Inc. PROVIDES ABSOLUTELY NO WARRANTY.  THE EVENT SCRIPT
 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 SCRIPT IS WITH YOU.  SHOULD THE SCRIPT 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 THIS SCRIPT (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.

|#

; ------------------------------------------------------------
; was bags.events
; ------------------------------------------------------------
(boot-strap nqthm)

(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))

(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))))

(disable listp-delete)

(LEMMA DELETE-NON-MEMBER (REWRITE)
       (IMPLIES (NOT (MEMBER X Y))
		(EQUAL (DELETE X Y) Y))
       ((ENABLE DELETE)))

(LEMMA DELETE-DELETE (REWRITE)
       (EQUAL (DELETE Y (DELETE X Z))
	      (DELETE X (DELETE Y Z)))
       ((ENABLE DELETE DELETE-NON-MEMBER)))

(lemma equal-occurrences-zero (rewrite)
       (equal (equal (occurrences x l) 0)
	      (not (member x l)))
       ((enable occurrences)))

(LEMMA MEMBER-NON-LIST (REWRITE)
       (IMPLIES (NOT (LISTP L))
		(NOT (MEMBER X L))))

(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)))


(LEMMA MEMBER-DELETE-IMPLIES-MEMBERSHIP (REWRITE)
       (IMPLIES (MEMBER X (DELETE Y L))
		(MEMBER X L))
       ((ENABLE DELETE)))

(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)))

(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)))

(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)))


(LEMMA SUBBAGP-DELETE (REWRITE)
       (IMPLIES (SUBBAGP X (DELETE U Y))
		(SUBBAGP X Y))
       ((ENABLE DELETE SUBBAGP DELETE-DELETE
		MEMBER-DELETE-IMPLIES-MEMBERSHIP)))

(LEMMA SUBBAGP-CDR1 (REWRITE)
       (IMPLIES (SUBBAGP X Y)
		(SUBBAGP (CDR X) Y))
       ((ENABLE SUBBAGP SUBBAGP-DELETE)))

(LEMMA SUBBAGP-CDR2 (REWRITE)
       (IMPLIES (SUBBAGP X (CDR Y))
		(SUBBAGP X Y))
       ((ENABLE DELETE SUBBAGP DELETE-NON-MEMBER SUBBAGP-CDR1)))

(LEMMA SUBBAGP-BAGINT1 (REWRITE)
       (SUBBAGP (BAGINT X Y) X)
       ((ENABLE DELETE SUBBAGP BAGINT SUBBAGP-CDR2)))

(LEMMA SUBBAGP-BAGINT2 (REWRITE)
       (SUBBAGP (BAGINT X Y) Y)
       ((ENABLE SUBBAGP BAGINT SUBBAGP-CDR2)))

(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))

; ------------------------------------------------------------
; was naturals.events
; ------------------------------------------------------------


;; Tue Sep 26 10:20:45 1989, from ~wilding/numerical/newnat.events

;; NATURALS Theory

;; Created by Bill Bevier 1988 (see CLI internal note 057)

;; Modifications by Bill Bevier and Matt Wilding (9/89) including
;; adding some new metalemmas for times, reorganizing the theories,
;; removing some extraneous lemmas, and removing dependence upon
;; other theories (by adding the pertinent lemmas).

;; This script requires the bags theory

;; This script sets up a theory for the NATURALS with the following subtheories
;; ADDITION
;; MULTIPLICATION
;; REMAINDER
;; QUOTIENT
;; EXPONENTIATION 
;; LOGS
;; GCDS

;; The theories of EXPONENTIATION, LOGS, and GCDS still need a lot of work

; --------------------------------------------------------------------------------
; ARITHMETIC
; --------------------------------------------------------------------------------

; -------------------- PLUS & DIFFERENCE --------------------

; ---------- EQUAL ----------

(lemma equal-plus-0 (rewrite)
       (equal (equal (plus a b) 0)
	      (and (zerop a)
		   (zerop b))))

(lemma plus-cancellation (rewrite)
       (equal (equal (plus a b) (plus a c))
	      (equal (fix b) (fix c))))

(disable plus-cancellation)

(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))))

(lemma difference-cancellation (rewrite)
       (equal (equal (difference x y) (difference z y))
	      (if (lessp x y)
		  (not (lessp y z))
		  (if (lessp z y)
		      (not (lessp y x))
		      (equal (fix x) (fix z)))))
       ((enable equal-difference-0)))

(disable difference-cancellation)

; ---------- PLUS ----------

(lemma commutativity-of-plus (rewrite)
       (equal (plus x y) (plus y x)))

(lemma commutativity2-of-plus (rewrite) 
       (equal (plus x (plus y z))
	      (plus y (plus x z))))

(lemma plus-zero-arg2 (rewrite)
       (implies (zerop y)
		(equal (plus x y)
		       (fix x)))
       ((induct (plus x y))))

(lemma plus-add1-arg1 (rewrite)
       (equal (plus (add1 a) b)
	      (add1 (plus a b))))

(lemma plus-add1-arg2 (rewrite)
       (equal (plus x (add1 y)) 
	      (if (numberp y)
		  (add1 (plus x y))
		  (add1 x))))

(lemma associativity-of-plus  (rewrite)
       (equal (plus (plus x y) z) (plus x (plus y z))))

(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))))
       
(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))))

; ---------- DIFFERENCE-PLUS cancellation rules ----------
;
; Here are the basic canonicalization rules for differences of sums. These
; are subsumed by the meta lemmas and are therefore globally disabled.
; They are here merely to prove the meta lemmas.

(lemma difference-plus-cancellation-proof ()
       (equal (difference (plus x y) x) (fix y)))


(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)))

(disable difference-plus-cancellation)

(lemma difference-plus-plus-cancellation-proof ()
       (equal (difference (plus x y) (plus x z))
	      (difference y z)))

(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)))

(disable difference-plus-plus-cancellation)

(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)))

(disable difference-plus-plus-cancellation-hack)

; Here are a few more facts about difference needed to prove the meta lemmas.
; These are disabled here. We re-prove them after the proof of the meta
; lemmas so that they will fire before the meta lemmas in subsequent proofs.

(lemma diff-sub1-arg2 (rewrite)
       (equal (difference a (sub1 b))
	      (if (zerop b)
		  (fix a)
		  (if (lessp a b)
		      0
		      (add1 (difference a b)))))
       ((induct (difference a b))))

(disable diff-sub1-arg2)

(lemma diff-diff-arg1 (rewrite)
    (equal (difference (difference x y) z)
	   (difference x (plus y z))))


(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))))


; diff-diff-diff should be removed, but since the hack lemmas for
; correctness-of-cancel-difference-plus are designed for it, we'll
; keep it around.

(lemma diff-diff-diff (rewrite)
       (implies (and (leq b a)
		     (leq d c))
		(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)))

(disable diff-diff-diff)

(lemma difference-lessp-arg1 (rewrite)
       (implies (lessp a b)
		(equal (difference a b) 0)))

(disable difference-lessp-arg1)

; --------------------------------------------------------------------------------
; Meta Lemmas to Cancel PLUS and DIFFERENCE expressions
; --------------------------------------------------------------------------------

; ---------- PLUS-TREE and PLUS-FRINGE ----------

(defn plus-fringe (x)
  (if (and (listp x) (equal (car x) 'plus))
      (append (plus-fringe (cadr x)) (plus-fringe (caddr x)))
      (cons x nil)))

(defn plus-tree (l)
  (if (nlistp l)
      ''0
	(if (nlistp (cdr l)) 
	    (list 'fix (car l))
	    (if (nlistp (cddr l))
		(list 'plus (car l) (cadr l))
		(list 'plus (car l) (plus-tree (cdr l)))))))

(lemma numberp-eval$-plus (rewrite)
       (implies (and (listp x) (equal (car x) 'plus))
		(numberp (eval$ t x a))))

(disable numberp-eval$-plus)

(lemma numberp-eval$-plus-tree (rewrite)
       (numberp (eval$ t (plus-tree l) a)) ((enable plus-tree)))

(disable numberp-eval$-plus-tree)

(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)))

(disable member-implies-plus-tree-greatereqp)

(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)))

(disable plus-tree-delete)

(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)))

(disable subbagp-implies-plus-tree-greatereqp)

(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)))

(disable plus-tree-bagdiff)

(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)))

(disable numberp-eval$-bridge)

(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)))

(disable bridge-to-subbagp-implies-plus-tree-greatereqp)

(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)))

(disable eval$-plus-tree-append)

(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))))

(disable plus-tree-plus-fringe)

(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))))

(disable member-implies-numberp)

(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))))

(disable cadr-eval$-list)

(lemma eval$-quote (rewrite)
       (equal (eval$ t (cons 'quote args) a) (car args)))

(disable eval$-quote)

(lemma listp-eval$ (rewrite)
       (equal (listp (eval$ 'list x a)) (listp x)))

(disable listp-eval$)

; ---------- CANCEL PLUS ----------

; CANCEL-EQUAL-PLUS cancels identical terms in a term which is the equality
; of two sums. For example,
; 
;   (EQUAL (PLUS A B C) (PLUS B D E)) => (EQUAL (PLUS A C) (PLUS D E))
;

(defn cancel-equal-plus (x)
  (if (and (listp x) (equal (car x) 'equal))
      (if (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))))))
	  (if (and (listp (cadr x)) (equal (caadr x) 'plus)
		   (member (caddr x) (plus-fringe (cadr x))))
	      (list 'if (list 'numberp (caddr x))
		     (list 'equal
			    (plus-tree
			     (delete (caddr x)
				     (plus-fringe (cadr x))))
			    ''0)
		     (list 'quote f))
	      (if (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))
		  x)))
      x))

(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$)))

; ---------- CANCEL-DIFFERENCE-PLUS ----------

; CANCEL-DIFFERENCE-PLUS cancels identical terms in a term which is the 
; difference of two sums. For example,
; 
;  (DIFFERENCE (PLUS A B C) (PLUS B D E)) => (DIFFERENCE (PLUS A C) (PLUS D E))
;
; Using rewrite rules, we canonicalize terms involving  PLUS and DIFFERENCE 
; to be the DIFFERENCE of two sums. Then CANCEL-DIFFERENCE-PLUS cancels out 
; like terms.

(defn cancel-difference-plus (x)
  (if (and (listp x) (equal (car x) 'difference))
      (if (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))))))
	  (if (and (listp (cadr x)) (equal (caadr x) 'plus)
		   (member (caddr x) (plus-fringe (cadr x))))
	      (plus-tree (delete (caddr x) (plus-fringe (cadr x))))
	      (if (and (listp (caddr x)) (equal (caaddr x) 'plus)
		       (member (cadr x) (plus-fringe (caddr x))))
		  ''0
		    x)))
      x))

(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$)))

; ---------- DIFFERENCE ----------

; Here are the rules for difference terms which we want to try before
; the meta lemmas. They help canonicalize terms to differences of sums.

(lemma difference-elim (elim)
       (implies (and (numberp y)
		     (not (lessp y x)))
		(equal (plus x (difference y x)) y)))

(lemma difference-leq-arg1 (rewrite)
       (implies (leq a b)
		(equal (difference a b) 0)))

(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))))

(lemma difference-sub1-arg2 (rewrite)
       (equal (difference a (sub1 b))
	      (if (zerop b)
		  (fix a)
		  (if (lessp a b)
		      0
		      (add1 (difference a b)))))
       ((enable diff-sub1-arg2)))

(lemma difference-difference-arg1 (rewrite)
       (equal (difference (difference x y) z)
	      (difference x (plus y z)))
       ((enable diff-diff-arg1)))

(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)))

(lemma difference-x-x (rewrite) 
       (equal (difference x x) 0))

; ---------- LESSP ----------

(lemma lessp-difference-cancellation (rewrite)
       (equal (lessp (difference a c)
		     (difference b c))
	      (if (leq c a)
		  (lessp a b)
		  (lessp c b)))
       ((enable equal-difference-0)))

(disable lessp-difference-cancellation)

; CANCEL-LESSP-PLUS cancels LESSP terms whose arguments are sums.
; Examples:
; (LESSP (PLUS A B C) (PLUS A C D)) -> (LESSP (FIX B) (FIX D))
; (LESSP A (PLUS A B))  -> (NOT (ZEROP (FIX B)))
; (LESSP (PLUS A B) A)  -> F

(defn cancel-lessp-plus (x)
  (if (and (listp x) (equal (car x) 'lessp))
      (if (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))))))
	  (if (and (listp (cadr x)) (equal (caadr x) 'plus)
		   (member (caddr x) (plus-fringe (cadr x))))
	      (list 'quote f)
	      (if (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))))))
		  x)))
      x))

(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$)))


; Define the available theory of addition.  To get the list of events to
; put in the theory, evaluate the following form in NQTHM at this point
; in the script. This form lists all  lemmas which are globally enabled,
; and which have non-null lemma type.
;
; (remove-if-not (function (lambda (x)
; 			   (and (member x (lemmas))
; 				(not (assoc x disabled-lemmas))
; 				(not (null (nth 2 (get x 'event)))))))
; 	       chronology)


(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))





; ---------- TIMES ----------

(lemma equal-times-0 (rewrite)
       (equal (equal (times x y) 0)
	      (or (zerop x)
		  (zerop y)))
       ((enable equal-plus-0)
	(induct (times x y))))

(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))))

;(lemma equal-sub1-times-0 (rewrite)
;       (equal (equal (sub1 (times a b)) 0)
;	      (or (zerop a)
;		  (zerop b)
;		  (and (equal a 1) (equal b 1)))))

(lemma equal-sub1-0 (rewrite)
       (equal (equal (sub1 x) 0)
	      (or (zerop x)
		  (equal x 1))))

(lemma times-zero (rewrite)
       (implies (zerop y)
		(equal (times x y) 0))
       ((enable plus-zero-arg2 commutativity-of-plus)))

(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)))

(lemma commutativity-of-times (rewrite)
       (equal (times y x) (times x y))
       ((enable times-zero times-add1)))

(lemma times-distributes-over-plus-proof ()
       (equal (times x (plus y z))
	      (plus (times x y) (times x z)))
       ((enable commutativity2-of-plus
		associativity-of-plus)))

(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)))

(lemma commutativity2-of-times (rewrite)
       (equal (times x y z)
	      (times y x z))
       ((enable commutativity-of-times
		times-distributes-over-plus)))

(lemma associativity-of-times (rewrite)
       (equal (times (times x y) z) 
	      (times x y z))
       ((enable commutativity-of-times 
		commutativity2-of-times)))

(lemma times-distributes-over-difference-proof ()
       (equal (times (difference a b) c)
	      (difference (times a c) (times b c)))
       ((enable commutativity-of-times)
	(enable-theory addition)))

(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)))

(lemma times-quotient-proof ()
       (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))))

(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)))

(lemma times-1-arg1 (rewrite)
       (equal (times 1 x) (fix x))
       ((enable times-zero)))

(lemma lessp-times1-proof ()
       (implies (and (lessp a b)
		     (not (zerop c)))
		(equal (lessp a (times b c))
		       t)))

(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)))

(lemma lessp-times2-proof ()
       (implies (and (leq a b)
		     (not (zerop c)))
		(equal (lessp (times b c) a)
		       f)))

(lemma lessp-times2 (rewrite)
       (implies (and (leq a b)
		     (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)))

(lemma lessp-times3-proof1 ()
       (implies (and (not (zerop a))
		     (lessp 1 b))
		(lessp a (times a b)))
       ((enable-theory addition)
	(enable times-zero)))

(lemma lessp-times3-proof2 ()
       (implies (lessp a (times a b))
		(and (not (zerop a))
		     (lessp 1 b)))
       ((enable-theory addition)))

(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)))


(lemma lessp-times-cancellation-proof ()
       (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)))


(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)))

(disable lessp-times-cancellation1)

(lemma lessp-plus-times-proof ()
       (implies (lessp x a)
		(equal (lessp (plus x (times a b))
			      (times a c))
		       (lessp b c)))
       ((enable-theory addition)
	(enable commutativity-of-times
		lessp-times-cancellation1
		lessp-times1 
		lessp-times2 
		lessp-times3
		times-add1
		times-zero)
	(induct (lessp b c))))

(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)))       

(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)))

(lemma lessp-1-times (rewrite)
       (equal (lessp 1 (times a b))
	      (not (or (zerop a)
		       (zerop b)
		       (and (equal a 1) (equal b 1))))))




;;; meta lemmas to cancel lessp-times and equal-times expressions
;; examples
;; (lessp (times b (times d a)) (times b (times e (times a f)))) -> 
;;                                            (and (and (not (zerop a)) 
;;                                                      (not (zerop b)))
;;                                                 (lessp (fix d) (times e f)))
;;
;; (equal (times b (times c d)) (times b d))    -> 
;;                                           (or (or (zerop b) (zerop d))
;;                                               (equal (fix c) 1))


(defn times-tree (x)
  (if (nlistp x) 
      ''1
      (if (nlistp (cdr x))
	  (list 'fix (car x))
	  (if (nlistp (cddr x))
	      (list 'times (car x) (cadr x))
	      (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)))
      (cons x nil)))

(defn or-zerop-tree (x)
  (if (nlistp x) 
      '(false)
      (if (nlistp (cdr x))
	  (list 'zerop (car x))
	  (if (nlistp (cddr x)) 
	      (list 'or (list 'zerop (car x)) (list 'zerop (cadr x)))
	      (list 'or (list 'zerop (car x)) (or-zerop-tree (cdr x)))))))

(defn and-not-zerop-tree (x)
  (if (nlistp x)
      '(true)
      (if (nlistp (cdr x))
	  (list 'not (list 'zerop (car x)))
	  (list 'and (list 'not (list 'zerop (car x)))
		 (and-not-zerop-tree (cdr x))))))

(lemma numberp-eval$-times (rewrite)
       (implies (equal (car x) 'times)
		(numberp (eval$ t x a))))

(disable numberp-eval$-times)


(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)))))

(disable eval$-times)


(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)))))

(disable eval$-or)

(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)))))

(disable eval$-equal)

(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)))))

(disable eval$-lessp)


(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)))))

(disable eval$-quotient)

(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)))))

(disable eval$-if)

(lemma numberp-eval$-times-tree (rewrite)
       (numberp (eval$ t (times-tree x) a))
       ((enable times-tree)))

(disable numberp-eval$-times-tree)


(lemma lessp-times-arg1 ()
       (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)))

(lemma infer-equality-from-not-lessp ()
       (implies	(and (numberp a)
		     (numberp b))
		(equal (and (not (lessp a b)) (not (lessp b a))) 
		       (equal a b))))

(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)))

(disable equal-times-arg1)

(lemma equal-times-bridge (rewrite)
       (equal (equal (times a b)
		     (times c (times 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)))

(disable equal-times-bridge)

(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)))

(disable eval$-times-member)

(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)))

(disable zerop-makes-times-tree-zero)

(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)))

(disable or-zerop-tree-is-not-zerop-tree)

(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)))

(disable zerop-makes-times-tree-zero2)

(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)))

(disable times-tree-append)

(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))))

(disable times-tree-of-times-fringe)

(defn cancel-lessp-times (x)
  (if (and (equal (car x) 'lessp)
	   (equal (caadr x) 'times)
	   (equal (caaddr x) 'times))
      (let ((inboth (bagint (times-fringe (cadr x))
			    (times-fringe (caddr x)))))
	(if (listp inboth)
	    (list 'and
		   (and-not-zerop-tree inboth)
		   (list 'lessp 
			  (times-tree (bagdiff (times-fringe (cadr x)) inboth))
			  (times-tree (bagdiff (times-fringe (caddr x)) inboth))))
	    x))
      x))



(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)))

(disable eval$-lessp-times-tree-bagdiff)

(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
		;MEMBER-CONS 
		 ;MEMBER-NON-LIST
		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))))))

(disable zerop-makes-lessp-false-bridge)


(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)))



(defn cancel-equal-times (x)
  (if (and (equal (car x) 'equal)
	   (equal (caadr x) 'times)
	   (equal (caaddr x) 'times))
      (let ((inboth (bagint (times-fringe (cadr x)) (times-fringe (caddr x)))))
	(if (listp inboth)
	    (list 'or 
		   (or-zerop-tree inboth)
		   (list 'equal
			  (times-tree (bagdiff (times-fringe (cadr x)) inboth))
			  (times-tree (bagdiff (times-fringe (caddr x)) inboth))))
	    x))
      x))

(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))))))

(disable zerop-makes-equal-true-bridge)
		       
(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)))

(disable eval$-equal-times-tree-bagdiff)

(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)))

(disable cancel-equal-times-preserves-inequality)

(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))))))

(disable cancel-equal-times-preserves-inequality-bridge)
		    
(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)))





; Define the available  theory of  multiplication.   To  get the list of
; events to put in the theory,  evaluate the following  form in NQTHM at
; this point  in  the  script. This   form  lists all lemmas   which are
; globally enabled, and which have non-null lemma type.
;
; (remove-if-not (function (lambda (x)
; 			   (and (member x (lemmas))
; 				(not (assoc x disabled-lemmas))
; 				(not (null (nth 2 (get x 'event))))
; 				(not (member x (nth 2 (get 'addition 'event)))))))
; 	       chronology)


(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))

; ---------- REMAINDER ----------

(lemma lessp-remainder (rewrite generalize)
       (equal (lessp (remainder x y) y) 
	      (not (zerop y))))

(lemma remainder-noop (rewrite)
       (implies (lessp a b)
		(equal (remainder a b)
		       (fix a))))

(lemma remainder-of-non-number (rewrite)
       (implies (not (numberp a))
		(equal (remainder a n)
		       (remainder 0 n))))

(lemma remainder-zero (rewrite)
       (implies (zerop x)
		(equal (remainder y x) 
		       (fix y))))

(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)))

(DISABLE PLUS-REMAINDER-TIMES-QUOTIENT)

(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)))

; (lemma remainder-sub1 (rewrite)
;        (implies (and (not (zerop a))
; 		     (not (zerop b)))
; 		(equal (remainder (sub1 a) b)
; 		       (if (equal (remainder a b) 0)
; 			   (sub1 b)
; 			   (sub1 (remainder a b)))))
;        ((enable lessp-remainder
; 		remainder-noop
; 		remainder-quotient-elim)
; 	(enable-theory addition)
; 	(induct (remainder a b))))

(lemma remainder-add1 (rewrite)
       (implies (equal (remainder a b) 0)
		(equal (remainder (add1 a) b)
		       (remainder 1 b)))
       ((enable remainder-noop)
	(enable-theory addition)
	(induct (remainder a b))))

(lemma remainder-plus-proof ()
       (implies (equal (remainder b c) 0)
		(equal (remainder (plus a b) c)
		       (remainder a c)))
       ((enable remainder-noop)
	(enable-theory addition)
	(induct (remainder b c))))

(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)))

(lemma equal-remainder-plus-0-proof ()
       (implies (equal (remainder a c) 0)
		(equal (equal (remainder (plus a b) c) 0)
		       (equal (remainder b c) 0)))
       ((enable remainder-plus)))

(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)))

(lemma equal-remainder-plus-remainder-proof ()
       (implies (lessp a c)
		(equal (equal (remainder (plus a b) c)
			      (remainder b c))
		       (zerop a)))
       ((enable remainder-noop)
	(enable-theory addition)
	(induct (remainder b c))))

(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)))

(DISABLE EQUAL-REMAINDER-PLUS-REMAINDER)

(lemma remainder-times1-proof ()
       (implies (equal (remainder b c) 0)
		(equal (remainder (times a b) c) 0))
       ((enable-theory multiplication addition)
	(enable remainder-plus
		remainder-noop
		remainder-zero)))

(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)))

(lemma remainder-times1-instance-proof ()
       (equal (remainder (times x y) y) 0)
       ((enable commutativity-of-times 
		difference-plus-cancellation
		remainder-zero)
	(induct (times x y))))

(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)))

(lemma remainder-times-times-proof ()
       (equal (remainder (times x y) (times x z))
	      (times x (remainder y z)))
       ((enable-theory addition multiplication)
	(enable remainder-zero)
	(induct (remainder y z))))

(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)))

(DISABLE REMAINDER-TIMES-TIMES)

(lemma remainder-times2-proof ()
       (implies (equal (remainder a z) 0)
		(equal (remainder a (times z y))
		       (times z (remainder (quotient a z) y))))
       ((enable-theory addition multiplication)
	(enable lessp-remainder
		remainder-noop
		remainder-plus
		remainder-quotient-elim
		remainder-times-times
		remainder-times1-instance
		remainder-zero)
	(do-not-induct t)))

(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)))

(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)))

(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)
	(do-not-induct t)))

(defn double-remainder-induction (a b c)
  (if (zerop c)
      0
      (if (lessp a c)
	  0
	  (if (lessp b c)
	      0
	      (double-remainder-induction (difference a c) (difference b c) c)))))

(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)
	(induct (double-remainder-induction a b c))))

(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)
	(induct (double-remainder-induction a b c))))

(DISABLE REMAINDER-DIFFERENCE3)

(lemma equal-remainder-difference-0 (rewrite)
       (equal (equal (remainder (difference a b) c) 0)
	      (if (leq b a)
		  (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)
	(do-not-induct t)))

(DISABLE EQUAL-REMAINDER-DIFFERENCE-0)

(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)
	(induct (double-remainder-induction b c x))))

(DISABLE LESSP-PLUS-FACT)

(lemma remainder-plus-fact ()
       (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)
	(induct (remainder b c))))

(lemma remainder-plus-times-times-proof ()
       (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)))

(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)))

; REMAINDER-PLUS-TIMES-TIMES-INSTANCE is the completion of the rules
; TIMES-DISTRIBUTES-OVER-PLUS, REMAINDER-TIMES-TIMES and REMAINDER-PLUS-TIMES-TIMES

(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)))

(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)))

(lemma remainder-1-arg1 (rewrite)
       (equal (remainder 1 x)
	      (if (equal x 1) 0 1))
       ((enable difference-leq-arg1)))

(lemma remainder-1-arg2 (rewrite)
       (equal (remainder y 1) 0))

(lemma remainder-x-x (rewrite)
       (equal (remainder x x) 0)
       ((enable equal-difference-0)))

(lemma transitivity-of-divides ()
       (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)))


; Define the available  theory of  remainder.   To  get the list of
; events to put in the theory,  evaluate the following  form in NQTHM at
; this point  in  the  script. This   form  lists all lemmas   which are
; globally enabled, and which have non-null lemma type.
;
; 
; (let ((lemmas (lemmas)))
;   (remove-if-not (function (lambda (x)
; 			     (and (member x lemmas)
; 				  (not (assoc x disabled-lemmas))
; 				  (not (null (nth 2 (get x 'event))))
; 				  (not (member x (nth 2 (get 'addition 'event))))
; 				  (not (member x (nth 2 (get 'multiplication 'event)))))))
; 		 chronology))


(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))

; ---------- QUOTIENT, DIVIDES  ----------

(lemma quotient-noop (rewrite)
       (implies (equal b 1)
		(equal (quotient a b)
		       (fix a))))

(lemma quotient-of-non-number (rewrite)
       (implies (not (numberp a))
		(equal (quotient a n)
		       (quotient 0 n))))

(lemma quotient-zero (rewrite)
       (implies (zerop x)
		(equal (quotient y x)
		       0)))

(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)
	(induct (remainder a b))))

(lemma equal-quotient-0 (rewrite)
       (equal (equal (quotient a b) 0)
	      (or (zerop b)
		  (lessp a b)))
       ((induct (quotient a b))))

(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)
	(induct (remainder a b))))

(lemma quotient-plus-proof ()
       (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)
	(induct (remainder b c))))

(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)))

; I need QUOTIENT-TIMES-INSTANCE to prove the more general QUOTIENT-TIMES,
; but I want QUOTIENT-TIMES-INSTANCE to be tried first (i.e. come after
; QUOTIENT-TIMES in the event list.) So first, prove QUOTIENT-TIMES-INSTANCE-TEMP,
; then prove QUOTIENT-TIMES, and finally give QUOTIENT-TIMES-INSTANCE.

(lemma quotient-times-instance-temp-proof ()
       (equal (quotient (times y x) y) 
	      (if (zerop y) 
		  0
		  (fix x)))
       ((enable times-zero commutativity-of-times difference-plus-cancellation)))

(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)))

(DISABLE QUOTIENT-TIMES-INSTANCE-TEMP)

(lemma quotient-times-proof ()
       (implies (equal (remainder a c) 0)
		(equal (quotient (times a b) c)
		       (times b (quotient a c))))
       ((enable-theory addition multiplication remainders)
	(enable quotient-plus quotient-noop equal-quotient-0
		quotient-times-instance-temp)
	(induct (remainder a c))))

(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)))

(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)))

(lemma quotient-times-times-proof ()
       (equal (quotient (times x y) (times x z))
	      (if (zerop x)
		  0
		  (quotient y z)))
       ((enable-theory addition)
	(enable lessp-times-cancellation1 equal-times-0 times-zero 
		commutativity-of-times times-distributes-over-difference)
	(induct (quotient y z))))

(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)))

(disable quotient-times-times)

(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)
	(enable quotient-plus
		quotient-times-instance
		equal-remainder-plus-remainder)
	(do-not-induct t)))

(lemma quotient-lessp-arg1 (rewrite)
       (implies (lessp a b)
		(equal (quotient a b) 0)))

(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)
	(induct (double-remainder-induction a b c))))

(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)
	(induct (double-remainder-induction a b c))))

(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)))

(DISABLE REMAINDER-EQUALS-ITS-FIRST-ARGUMENT)

(lemma quotient-remainder-times (rewrite)
       (equal (quotient (remainder x (times a b)) a)
	      (remainder (quotient x a) b))
       ((enable-theory addition multiplication remainders)
	(enable ;lessp-plus-times2
		remainder-equals-its-first-argument
		quotient-noop
		quotient-plus
		quotient-times-instance
		quotient-zero)
	(do-not-induct t)))

(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)
	(enable	quotient-noop
		quotient-plus
		quotient-remainder-times
		quotient-times-instance
		quotient-zero)
	(do-not-induct t)))

(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)))

(lemma quotient-plus-fact ()
       (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)
	(induct (quotient b c))))

(lemma quotient-plus-times-times-proof ()
       (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)))

(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)))

; QUOTIENT-PLUS-TIMES-TIMES-INSTANCE is the completion of the rules
; QUOTIENT-TIMES-TIMES, QUOTIENT-PLUS-TIMES-TIMES and TIMES-DISTRIBUTES-OVER-PLUS

(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)))

(lemma quotient-quotient (rewrite)
       (equal (quotient (quotient b a) c)
	      (quotient b (times a c)))
       ((enable-theory addition multiplication remainders)
	(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)))

(lemma leq-quotient ()
       (implies (lessp a b)
		(leq (quotient a c) (quotient b c)))
       ((induct (double-remainder-induction a b c))
	(enable quotient-lessp-arg1
		quotient-zero)))

(lemma quotient-1-arg2 (rewrite)
       (equal (quotient n 1)
	      (fix n)))

(lemma quotient-1-arg1-casesplit ()
       (or (zerop n)
	   (equal n 1)
	   (lessp 1 n)))

(lemma quotient-1-arg1 (rewrite)
       (equal (quotient 1 n)
	      (if (equal n 1)
		  1
		  0))
       ((enable quotient-lessp-arg1)
	(use (quotient-1-arg1-casesplit))))


(lemma quotient-x-x (rewrite)
       (implies (not (zerop x))
		(equal (quotient x x) 1))
       ((enable difference-x-x)))

(lemma lessp-quotient (rewrite)
       (equal (lessp (quotient i j) i)
	      (and (not (zerop i))
		   (not (equal j 1)))))


;; Metalemma to cancel quotient-times expressions

;; ex.
;; (quotient (times a b) (times c (times d a)))  -> 
;;                                           (if (not (zerop a))
;;                                               (quotient (fix b) (times c d))
;;                                            (zero))
;;

(defn cancel-quotient-times (x)
  (if (and (equal (car x) 'quotient)
	   (equal (caadr x) 'times)
	   (equal (caaddr x) 'times))
      (let ((inboth (bagint (times-fringe (cadr x))
			    (times-fringe (caddr x)))))
	(if (listp inboth)
	    (list 'if
		   (and-not-zerop-tree inboth)
		   (list 'quotient
			  (times-tree (bagdiff (times-fringe (cadr x)) inboth))
			  (times-tree (bagdiff (times-fringe (caddr x)) inboth)))
		   '(zero))
	    x))
      x))


(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
		;MEMBER-CONS 
		 ;MEMBER-NON-LIST
		SUBBAGP-BAGINT1 
		SUBBAGP-BAGINT2
		TIMES-FRINGE 
		TIMES-TREE
		TIMES-TREE-APPEND 
		TIMES-TREE-OF-TIMES-FRINGE
		ZEROP-MAKES-LESSP-FALSE-BRIDGE)))

(disable zerop-makes-quotient-zero-bridge)

(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)))

(disable eval$-quotient-times-tree-bagdiff)

(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)))

; Define the available theory of quotient.  To get the list of events to
; put in the theory, evaluate the following form in NQTHM at  this point
; in the script. This form lists all  lemmas which are globally enabled,
; and which have non-null lemma type.
;
; 
; (let ((lemmas (lemmas)))
;   (remove-if-not (function (lambda (x)
; 			     (and (member x lemmas)
; 				  (not (assoc x disabled-lemmas))
; 				  (not (null (nth 2 (get x 'event))))
; 				  (not (member x (nth 2 (get 'addition 'event))))
; 				  (not (member x (nth 2 (get 'multiplication 'event))))
; 				  (not (member x (nth 2 (get 'remainders 'event)))))))
; 		 chronology))



(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))


;;; exp, log, and gcd

(defn exp (i j)
  (if (zerop j)
      1
      (times i (exp i (sub1 j)))))


(defn log (base n)
  (if (lessp base 2)
      0
      (if (zerop n)
	  0
	  (add1 (log base (quotient n base))))))

(defn gcd (x y)
  (if (zerop x)
      (fix y)
      (if (zerop y)
	  x
	  (if (lessp x y)
	      (gcd  x (difference y x))
	      (gcd (difference x y) y))))
  ((ord-lessp (cons (add1 x) (fix y)))))

(lemma remainder-exp (rewrite)
       (implies (not (zerop k))
		(equal (remainder (exp n k) n) 0))
       ((enable exp remainder-times1-instance)))


(defn double-number-induction (i j)
  (if (zerop i)
      0
      (if (zerop j)
	  0
	  (double-number-induction (sub1 i) (sub1 j)))))


(lemma remainder-exp-exp (rewrite)
       (implies (leq i j)
		(equal (remainder (exp a j) (exp a i)) 0))
       ((enable exp
		remainder-1-arg2
		remainder-times2-instance)
	(enable-theory addition multiplication)
	(induct (double-number-induction i j))))


(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)))


(lemma exp-zero (rewrite)
       (implies (zerop k)
		(equal (exp n k) 1))
       ((enable exp)))

(lemma exp-add1 (rewrite)
       (equal (exp n (add1 k))
	      (times n (exp n k)))
       ((enable exp)))

(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)))

(lemma exp-0-arg1 (rewrite)
       (equal (exp 0 k)
	      (if (zerop k) 1 0))
       ((enable exp)))

(lemma exp-1-arg1 (rewrite)
       (equal (exp 1 k) 1)
       ((enable exp)))

(lemma exp-0-arg2 (rewrite)
       (equal (exp n 0) 1)
       ((enable exp)))

(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)))

(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)))

(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))))

(lemma equal-exp-1 (rewrite)
       (equal (equal (exp n k) 1)
	      (if (zerop k)
		  t
		  (equal n 1)))		  
       ((enable exp times-zero times-add1)))

(lemma exp-difference (rewrite)
       (implies (and (leq c b)
		     (not (zerop a)))
		(equal (exp a (difference b c))
		       (quotient (exp a b) (exp a c))))
       ((enable exp)
	(enable-theory addition multiplication remainders quotients)))

(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))


(lemma equal-log-0 (rewrite)
       (equal (equal (log base n) 0)
	      (or (lessp base 2)
		  (zerop n)))
       ((enable log)
	(induct (log base n))))

(lemma log-0 (rewrite)
       (implies (zerop n)
		(equal (log base n) 0))
       ((enable log)))

(lemma log-1 (rewrite)
       (implies (lessp 1 base)
		(equal (log base 1) 1))
       ((enable log)
	(induct (log base n))))

(defn double-log-induction (base a b)
  (if (lessp base 2)
      0
      (if (zerop a)
	  0
	  (if (zerop b)
	      0
	      (double-log-induction base (quotient a base) (quotient b base))))))

(lemma leq-log-log nil
       (implies (leq n m)
		(leq (log c n) (log c m)))
       ((enable log)
	(induct (double-log-induction c n m))
	(use (leq-quotient (a n) (b m) (c c)))))

(lemma log-quotient (rewrite)
       (implies (lessp 1 c)
		(equal (log c (quotient n c))
		       (sub1 (log c n))))
       ((enable log)))

(lemma log-quotient-times-proof ()
       (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)))

(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)))

(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)))

(lemma log-times-proof ()
       (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)))

(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)))

(lemma log-times-exp-proof ()
       (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)))


(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)))

(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)))

(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))



(lemma commutativity-of-gcd (rewrite)
       (equal (gcd b a) (gcd a b))
       ((enable gcd)
	(enable-theory addition)))

(defn single-number-induction (n)
  (if (zerop n)
      0
      (single-number-induction (sub1 n))))

(lemma gcd-0 (rewrite)
       (and (equal (gcd 0 x) (fix x))
	    (equal (gcd x 0) (fix x)))
       ((enable gcd)))

(lemma gcd-1 (rewrite)
       (and (equal (gcd 1 x) 1)
	    (equal (gcd x 1) 1))
       ((enable gcd)
	(enable-theory addition)
	(induct (single-number-induction x))))

(lemma equal-gcd-0 (rewrite)
       (equal (equal (gcd a b) 0)
	      (and (zerop a)
		   (zerop b)))
       ((enable gcd)
	(enable-theory addition)
	(induct (gcd a b))))

(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)))

(lemma gcd-plus-instance-temp-proof ()
       (equal (gcd a (plus a b))
	      (gcd a b))
       ((enable gcd commutativity-of-gcd)
	(enable-theory addition)
	(induct (gcd a b))))

(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)))

(lemma gcd-plus-proof ()
       (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)
	(induct (remainder b a))))

(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)))

(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)))

(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)))

(lemma distributivity-of-times-over-gcd-proof ()
       (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)))

(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)))

(lemma gcd-is-the-greatest nil
       (implies (and (not (zerop x))
		     (not (zerop y))
		     (equal (remainder x z) 0)
		     (equal (remainder y z) 0))
		(leq z (gcd x y)))
       ((enable gcd
		commutativity-of-gcd
		distributivity-of-times-over-gcd
		equal-gcd-0)
	(enable-theory addition multiplication remainders)
	(do-not-induct t)))

(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)
	(do-not-induct t)))

; We prove ASSOCIATIVITY-OF-GCD and COMMUTATIVITY2-OF-GCD roughly the same way.
; Use GCD-IS-THE-GREATEST twice to show that each side of the equality is
; less than or equal to the other side.

(lemma associativity-of-gcd-zero-case ()
       (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)))

(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)))

(lemma commutativity2-of-gcd-zero-case ()
       (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)))

(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)))

(lemma gcd-x-x (rewrite)
       (equal (gcd x x)
	      (fix x))
       ((enable gcd)
	(enable-theory addition)
	(induct (single-number-induction x))))

(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)
	(induct (gcd x y))))

(deftheory gcds
  (commutativity2-of-gcd
    associativity-of-gcd
    common-divisor-divides-gcd
    distributivity-of-times-over-gcd
    lessp-gcd
    equal-gcd-0
    gcd-0
    gcd-idempotence
    gcd-x-x 
    remainder-gcd
    gcd-plus
    gcd-plus-instance
    gcd-1
    commutativity-of-gcd))



(deftheory naturals
  (addition
   multiplication
   remainders
   quotients
   exponentiation
   logs
   gcds))

; ------------------------------------------------------------
; was integers.events
; ------------------------------------------------------------


;; By Matt Kaufmann, modified from earlier integer library of Bill
;; Bevier and Matt Wilding.  A few functions (even ILESSP) have
;; been changed, but I expect the functionality of this library to
;; include all the functionality of the old one in most or even all
;; cases.

;; Modified from /local/src/nqthm-libs/integers.events to get ILEQ
;; expressed in terms of ILESSP and IDIFFERENCE in terms of INEG and
;; IPLUS.  There are other changes too.  The highlights are the new
;; metalemmas.

;; I'm going to leave the eval$ rules on that are proved here, and
;; leave eval$ off.

;; My intention is that this library be used in a mode in which ILEQ
;; and IDIFFERENCE are left enabled.  Otherwise, the aforementioned
;; meta lemmas may not be very useful, and also a number of additional
;; replacement rules may be needed.

;; There are three theories created by this library.  INTEGER-DEFNS is
;; a list of definitions of all integer functions (not including the
;; cancellation metafunctions and their auxiliaries, though), except
;; that ILEQ and IDIFFERENCE have been omitted.  This is a useful
;; theory for an ENABLE-THEORY hint when one simply wants to blast all
;; integer functions open, and it's also useful if one wants to close
;; them down with a DISABLE-THEORY hint (perhaps to go with an
;; (ENABLE-THEORY T) hint).  Second, ALL-INTEGER-DEFNS is the same as
;; INTEGER-DEFNS except that ILEQ and IDIFFERENCE are included in this
;; one.  Finally, INTEGERS is a list of all events to be "exported as
;; enabled" from this file when working in a mode where everything not
;; enabled by an ENABLE-THEORY hint is to be disabled.  Notice that
;; some rewrite rules have been included that might appear to be
;; unnecessary in light of the metalemmas; that's because metalemmas
;; only work on tame terms.  However, there's no guarantee that the
;; rewrite rules alone will prove very useful (on non-tame terms).
;; Also notice that INTEGER-DEFNS is disjoint from INTEGERS, since we
;; expect the basic definitions (other than ILEQ and IDIFFERENCE) to
;; remain disabled.

;; It's easy to see what I have and haven't placed in INTEGERS, since
;; I'll simply comment out the event names that I want to exclude (see
;; end of this file).

;; One might wish to consider changing (fix-int (minus ...)) in some
;; of the definitions below to (ineg ...).

;; The following meta rules are in this library.  
;; (A little documentation added by Matt Wilding July 90)
;; 
;; CORRECTNESS-OF-CANCEL-INEG
;;  cancel the first argument of an iplus term with a member of the second 
;;  argument.
;; 
;;  ex:  (iplus (ineg y) (iplus (ineg x) (iplus y z)))  
;;     -->
;;       (iplus (ineg x) (fix-int z))
;; 
;; CORRECTNESS-OF-CANCEL-IPLUS
;;  cancel the sides of an equality of iplus sums
;; 
;;  ex:  (equal (iplus x (iplus y z)) (iplus a (iplus z x)))
;;     -->
;;       (equal (fix-int y) (fix-int a))
;; 
;; CORRECTNESS-OF-CANCEL-IPLUS-ILESSP
;;  cancel the sides of an ilessp inequality of sums
;; 
;;  ex:  (ilessp (iplus x (iplus y z)) (iplus a (iplus z x)))
;;     -->
;;       (ilessp y a)
;; 
;; CORRECTNESS-OF-CANCEL-ITIMES
;;  cancel the sides of an equality of itimes products
;;  
;;  ex: (equal (itimes x (itimes y z)) (itimes a (itimes z x)))
;;     -->
;;      (if (equal (itimes x z) '0)
;;        t
;;        (equal (fix-int y) (fix-int a)))
;; 
;; CORRECTNESS-OF-CANCEL-ITIMES-ILESSP
;;  cancel the sides of an inequality of itimes products
;; 
;;  ex: (ilessp (itimes x (itimes y z)) (itimes a (itimes z x)))
;;     -->
;;      (if (ilessp (itimes x z) '0)
;;         (ilessp a y)
;;        (if (ilessp 0 (itimes x z))
;;           (ilessp y a)
;;           f))
;; 
;; CORRECTNESS-OF-CANCEL-ITIMES-FACTORS
;;  cancel factors in equality terms
;;  ex: (equal (iplus (itimes x y) x) (itimes z x))
;;     -->
;;      (if (equal (fix-int x) '0)
;;         t
;;        (equal (fix-int (plus y 1)) (fix-int z)))
;; 
;; CORRECTNESS-OF-CANCEL-ITIMES-ILESSP-FACTORS
;;  cancel factors in ilessp terms
;;  ex: (equal (iplus (itimes x y) x) (itimes z x))
;;     -->
;;      (if (ilessp x '0)
;;         (ilessp z (iplus y 1))
;;        (if (ilessp '0 x)
;;           (ilessp (iplus y '1) z)
;;          f))
;; 
;; CORRECTNESS-OF-CANCEL-FACTORS-0
;;  factor one side of equality when other side is constant 0
;; 
;;  ex: (equal (iplus x (itimes x y)) '0)
;;     -->
;;      (or (equal (fix-int (iplus '1 y)) '0)
;;          (equal (fix-int x) '0))
;; 
;; CORRECTNESS-OF-CANCEL-FACTORS-ILESSP-0
;;  factor one side of inequality when other side is constant 0
;; 
;;  ex: (ilessp (iplus x (itimes x y)) '0)
;;     -->
;;      (or (and (ilessp (iplus '1 y) '0)
;;               (ilessp '0 x))
;;          (and (ilessp '0 (iplus '1 y))
;;               (ilessp x '0)))
;; 
;; CORRECTNESS-OF-CANCEL-INEG-TERMS-FROM-EQUALITY
;;  rewrite equality to remove ineg terms
;; 
;;  ex: (equal (iplus (ineg x) (ineg y)) (iplus (ineg z) w))
;;     --> 
;;      (equal (fix-int z) (iplus x (iplus y w)))
;; 
;; CORRECTNESS-OF-CANCEL-INEG-TERMS-FROM-INEQUALITY
;;  rewrite inequalities to remove ineg terms
;; 
;;  ex: (ilessp (iplus (ineg x) (ineg y)) (iplus (ineg z) w))
;;     -->
;;      (ilessp (fix-int z) (iplus x (iplus y w)))


;(note-lib "/local/src/nqthm-libs/naturals")

;(compile-uncompiled-defns "xxx")

; --------------------------------------------------------------------------------
; Integers
; --------------------------------------------------------------------------------

#| The function below has no AND or OR, for efficiency
(defn integerp (x)
  (or (numberp x)
      (and (negativep x)
	   (not (zerop (negative-guts x))))))
|#

(DEFN INTEGERP (X)
  (COND
   ((NUMBERP X) T)
   ((NEGATIVEP X) (NOT (ZEROP (NEGATIVE-GUTS X))))
   (T F)))

(defn fix-int (x)
  (if (integerp x) x 0))

;; Even though I'll include a definition for izerop here, I'll
;; often avoid using it.
(defn izerop (i)
  (equal (fix-int i) 0))

#| old version:
(defn izerop (i)
  (if (integerp i)
      (equal i 0)
      t))
|#

(defn ilessp (i j)
  (if (negativep i)
      (if (negativep j)
	  (lessp (negative-guts j) (negative-guts i))
	  (if (equal i (minus 0))
	      (lessp 0 j)
	    t))
      (if (negativep j)
	  f
	  (lessp i j))))

(defn ileq (i j)
  ;; I expect this to be enabled, in analogy to leq.
  (not (ilessp j i)))

(defn iplus (x y)
  (if (negativep x)
      (if (negativep y)
	  (if (and (zerop (negative-guts x))
		   (zerop (negative-guts y)))
	      0
	      (minus (plus (negative-guts x)
			   (negative-guts y))))
	  (if (lessp y (negative-guts x))
	      (minus (difference (negative-guts x) y))
	      (difference y (negative-guts x))))
      (if (negativep y)
	  (if (lessp x (negative-guts y))
	      (minus (difference (negative-guts y) x))
	      (difference x (negative-guts y)))
	  (plus x y))))

(defn ineg (x)
  (if (negativep x)
      (negative-guts x)
      (if (zerop x)
	  0
	  (minus x))))

(defn idifference (x y)
  ;; I find it troublesome to reason separately about idifference,
  ;; especially for metalemmas, so I intend to keep it enabled.
  (iplus x (ineg y)))

(defn iabs (i)
  (if (negativep i)
      (negative-guts i)
      (fix i)))

(defn itimes (i j)
  (if (negativep i)
      (if (negativep j)
	  (times (negative-guts i) (negative-guts j))
	  (fix-int (minus (times (negative-guts i) j))))
      (if (negativep j)
	  (fix-int (minus (times i (negative-guts j))))
	  (times i j))))

(defn iquotient (i j)
  (if (equal (fix-int j) 0)
      0
      (if (negativep i)
	  (if (negativep j)
	      (if (equal (remainder (negative-guts i) (negative-guts j)) 0)
		  (quotient (negative-guts i) (negative-guts j))
		  (add1 (quotient (negative-guts i) (negative-guts j))))
	      (if (equal (remainder (negative-guts i) j) 0)
		  (fix-int (minus (quotient (negative-guts i) j)))
		  (fix-int (minus (add1 (quotient (negative-guts i) j))))))
	  (if (negativep j)
	      (fix-int (minus (quotient i (negative-guts j))))
	      (quotient i j)))))

(defn iremainder (i j)
  (idifference i (itimes j (iquotient i j))))

(defn idiv (i j)
  (if (equal (fix-int j) 0)
      0
      (if (negativep i)
	  (if (negativep j)
	      (quotient (negative-guts i) (negative-guts j))
	      (if (equal (remainder (negative-guts i) j) 0)
		  (fix-int (minus (quotient (negative-guts i) j)))
		  (fix-int (minus (add1 (quotient (negative-guts i) j))))))
	  (if (negativep j)
	      (if (equal (remainder i (negative-guts j)) 0)
		  (fix-int (minus (quotient i (negative-guts j))))
		  (fix-int (minus (add1 (quotient i (negative-guts j))))))
	      (quotient i j)))))

(defn imod (i j)
  (idifference (fix-int i) (itimes j (idiv i j))))

(defn iquo (i j)
  (if (equal (fix-int j) 0)
      0
      (if (negativep i)
	  (if (negativep j)
	      (quotient (negative-guts i) (negative-guts j))
	      (fix-int (minus (quotient (negative-guts i) j))))
	  (if (negativep j)
	      (fix-int (minus (quotient i (negative-guts j))))
	      (quotient i j)))))

(defn irem (i j)
  (idifference (fix-int i) (itimes j (iquo i j))))

; ---------- DEFTHEORY events for definitions ----------

(deftheory integer-defns
  ;; omits ILEQ and IDIFFERENCE and IZEROP
  (integerp fix-int ilessp iplus ineg iabs itimes
	    iquotient iremainder idiv imod iquo irem))

(deftheory all-integer-defns
  (integerp fix-int izerop ilessp ileq iplus ineg idifference iabs itimes
	    iquotient iremainder idiv imod iquo irem))

(disable integerp)
(disable fix-int)
(disable ilessp)
(disable iplus)
(disable ineg)
(disable iabs)
(disable itimes)
;; I've disabled the rest later in the file, just because the lemmas
;; about division were (re-)proved with the remaining functions enabled.

; ---------- INTEGERP ----------

(lemma integerp-fix-int (rewrite)
       (integerp (fix-int x))
       ((enable integerp fix-int)))

(lemma integerp-iplus (rewrite)
       (integerp (iplus x y))
       ((enable integerp iplus)))

(lemma integerp-idifference (rewrite)
       (integerp (idifference x y))
       ((enable integerp-iplus idifference)))

(lemma integerp-ineg (rewrite)
       (integerp (ineg x))
       ((enable integerp ineg)))

(lemma integerp-iabs (rewrite)
       (integerp (iabs x))
       ((enable integerp iabs)))

(lemma integerp-itimes (rewrite)
       (integerp (itimes x y))
       ((enable integerp itimes fix-int)))

; ---------- FIX-INT ----------

;; The first of these, FIX-INT-REMOVER, is potentially dangerous from
;; a backchaining point of view, but I believe it's necessary.  At least
;; the lemmas below it should go a long way toward preventing its application.

(lemma fix-int-remover (rewrite)
  (implies (integerp x)
	   (equal (fix-int x) x))
  ((enable fix-int integerp)))

(lemma fix-int-fix-int (rewrite)
       (equal (fix-int (fix-int x))
	      (fix-int x))
       ((enable fix-int integerp)))

(lemma fix-int-iplus (rewrite)
       (equal (fix-int (iplus a b))
	      (iplus a b))
       ((enable fix-int integerp iplus)))

(lemma fix-int-idifference (rewrite)
       (equal (fix-int (idifference a b))
	      (idifference a b))
       ((enable fix-int-iplus idifference)))

(lemma fix-int-ineg (rewrite)
       (equal (fix-int (ineg x))
	      (ineg x))
       ((enable fix-int integerp ineg)))

(lemma fix-int-iabs (rewrite)
       (equal (fix-int (iabs x))
	      (iabs x))
       ((enable integerp fix-int iabs)))

(lemma fix-int-itimes (rewrite)
       (equal (fix-int (itimes x y))
	      (itimes x y))
       ((enable integerp itimes fix-int)))

; ---------- INEG ----------

(lemma ineg-iplus (rewrite)
       (equal (ineg (iplus a b))
	      (iplus (ineg a) (ineg b)))
       ((enable iplus ineg plus-zero-arg2)))

(lemma ineg-ineg (rewrite)
       (equal (ineg (ineg x))
	      (fix-int x))
       ((enable ineg fix-int integerp)))

(lemma ineg-fix-int (rewrite)
       (equal (ineg (fix-int x))
	      (ineg x))
       ((enable ineg fix-int integerp)))

(lemma ineg-of-non-integerp (rewrite)
  (implies (not (integerp x))
	   (equal (ineg x) 0))
  ((enable ineg integerp)))

;; I don't want the backchaining to slow down the prover.
(disable ineg-of-non-integerp)

(lemma ineg-0 (rewrite)
  (equal (ineg 0) 0)
  ((enable ineg)))

; ---------- IPLUS ----------

;; The first two of these really aren't necessary, in light
;; of the cancellation metalemma.

(lemma iplus-left-id (rewrite)
       (implies (not (integerp x))
		(equal (iplus x y)
		       (fix-int y)))
       ((enable integerp iplus fix-int)))

;; I don't want the backchaining to slow down the prover.
(disable iplus-left-id)

(lemma iplus-right-id (rewrite)
       (implies (not (integerp y))
		(equal (iplus x y)
		       (fix-int x)))
       ((enable integerp iplus fix-int plus-zero-arg2)))

;; I don't want the backchaining to slow down the prover.
(disable iplus-right-id)

(lemma iplus-0-left (rewrite)
       (equal (iplus 0 x) (fix-int x))
       ((enable iplus fix-int integerp)))

(lemma iplus-0-right (rewrite)
       ;; just in case we turn off commutativity
       (equal (iplus x 0) (fix-int x))
       ((enable iplus fix-int integerp)))

(lemma commutativity2-of-iplus (rewrite)
       (equal (iplus x (iplus y z)) (iplus y (iplus x z)))
       ((enable iplus commutativity2-of-plus)))

(lemma commutativity-of-iplus (rewrite)
       (equal (iplus x y) (iplus y x))
       ((enable iplus commutativity2-of-iplus)))

(lemma associativity-of-iplus (rewrite)
       (equal (iplus (iplus x y) z) (iplus x (iplus y z)))
       ((enable iplus)
	(enable-theory addition)))

(lemma iplus-cancellation-1 (rewrite)
       (equal (equal (iplus a b) (iplus a c))
	      (equal (fix-int b) (fix-int c)))
       ((enable iplus fix-int integerp)
	(enable-theory addition)))

(lemma iplus-cancellation-2 (rewrite)
       (equal (equal (iplus b a) (iplus c a))
	      (equal (fix-int b) (fix-int c)))
       ((use (iplus-cancellation-1))
	(enable commutativity-of-iplus)))

(lemma iplus-ineg1 (rewrite)
       (equal (iplus (ineg a) a) 0)
       ((enable iplus ineg integerp fix-int)))

(lemma iplus-ineg2 (rewrite)
       (equal (iplus a (ineg a)) 0)
       ((enable iplus ineg integerp fix-int)))

(lemma iplus-fix-int1 (rewrite)
       (equal (iplus (fix-int a) b)
	      (iplus a b))
       ((enable iplus fix-int integerp plus-zero-arg2)
	(do-not-induct t)))

(lemma iplus-fix-int2 (rewrite)
       (equal (iplus a (fix-int b))
	      (iplus a b))
       ((enable iplus fix-int integerp plus-zero-arg2)
	(do-not-induct t)))

; ---------- IDIFFERENCE ----------

;; mostly omitted, but I'll keep a few

(lemma idifference-fix-int1 (rewrite)
       (equal (idifference (fix-int a) b)
	      (idifference a b))
       ((enable idifference iplus-fix-int1)
	(do-not-induct t)))

(lemma idifference-fix-int2 (rewrite)
       (equal (idifference a (fix-int b))
	      (idifference a b))
       ((enable idifference iplus-fix-int2 ineg-fix-int)
	(do-not-induct t)))


; --------------------------------------------------------------------------------
; Cancel INEG
; --------------------------------------------------------------------------------

;; We assume that the given term (IPLUS x y) has the property that y has already
;; been reduced and x is not an iplus-term.  So, the only question is whether
;; or not the formal negative of x appears in the fringe of y.

#| The function below has no AND or OR, for efficiency
(defn cancel-ineg-aux (x y)
  ;; returns nil or else a new term provably equal to (IPLUS x y)
  (if (and (listp x)
	   (equal (car x) 'ineg))
      (cond 
       ((equal y (cadr x))
	''0)
       ((and (listp y)
	     (equal (car y) 'iplus))
	(let ((y1 (cadr y)) (y2 (caddr y)))
	  (if (equal y1 (cadr x))
	      (list 'fix-int y2)
	    (let ((z (cancel-ineg-aux x y2)))
	      (if z
		  (list 'iplus y1 z)
		f)))))
       (t f))
    (cond
     ((nlistp y)
      f)
     ((equal (car y) 'ineg)
      (if (equal x (cadr y))
	  ''0
	f))
     ((equal (car y) 'iplus)
      (let ((y1 (cadr y)) (y2 (caddr y)))
	(if (and (listp y1)
		 (equal (car y1) 'ineg)
		 (equal x (cadr y1)))
	    (list 'fix-int y2)
	  (let ((z (cancel-ineg-aux x y2)))
	    (if z
		(list 'iplus y1 z)
	      f)))))
     (t f))))
|#

(DEFN CANCEL-INEG-AUX (X Y)
      (COND
        ((LISTP X)
         (COND
           ((EQUAL (CAR X) 'INEG)
            (COND
              ((EQUAL Y (CADR X)) ''0)
              ((LISTP Y)
               (IF (EQUAL (CAR Y) 'IPLUS)
                   (COND
                     ((EQUAL (CADR Y) (CADR X))
                      (LIST 'FIX-INT (CADDR Y)))
                     ((CANCEL-INEG-AUX X (CADDR Y))
                      (LIST 'IPLUS (CADR Y)
                            (CANCEL-INEG-AUX X (CADDR Y))))
                     (T F))
                   F))
              (T F)))
           ((NLISTP Y) F)
           ((EQUAL (CAR Y) 'INEG) (IF (EQUAL X (CADR Y)) ''0 F))
           ((EQUAL (CAR Y) 'IPLUS)
            (COND
              ((LISTP (CADR Y))
               (COND
                 ((EQUAL (CAADR Y) 'INEG)
                  (COND
                    ((EQUAL X (CADADR Y)) (LIST 'FIX-INT (CADDR Y)))
                    ((CANCEL-INEG-AUX X (CADDR Y))
                     (LIST 'IPLUS (CADR Y)
                           (CANCEL-INEG-AUX X (CADDR Y))))
                    (T F)))
                 ((CANCEL-INEG-AUX X (CADDR Y))
                  (LIST 'IPLUS (CADR Y) (CANCEL-INEG-AUX X (CADDR Y))))
                 (T F)))
              ((CANCEL-INEG-AUX X (CADDR Y))
               (LIST 'IPLUS (CADR Y) (CANCEL-INEG-AUX X (CADDR Y))))
              (T F)))
           (T F)))
        ((NLISTP Y) F)
        ((EQUAL (CAR Y) 'INEG) (IF (EQUAL X (CADR Y)) ''0 F))
        ((EQUAL (CAR Y) 'IPLUS)
         (COND
           ((LISTP (CADR Y))
            (COND
              ((EQUAL (CAADR Y) 'INEG)
               (COND
                 ((EQUAL X (CADADR Y)) (LIST 'FIX-INT (CADDR Y)))
                 ((CANCEL-INEG-AUX X (CADDR Y))
                  (LIST 'IPLUS (CADR Y) (CANCEL-INEG-AUX X (CADDR Y))))
                 (T F)))
              ((CANCEL-INEG-AUX X (CADDR Y))
               (LIST 'IPLUS (CADR Y) (CANCEL-INEG-AUX X (CADDR Y))))
              (T F)))
           ((CANCEL-INEG-AUX X (CADDR Y))
            (LIST 'IPLUS (CADR Y) (CANCEL-INEG-AUX X (CADDR Y))))
           (T F)))
        (T F)))

#| The function below has no AND or OR, for efficiency
(defn cancel-ineg (x)
  (if (and (listp x)
	   (equal (car x) 'iplus))
      (let ((temp (cancel-ineg-aux (cadr x) (caddr x))))
	(if temp
	    temp
	  x))
    x))
|#

(DEFN CANCEL-INEG (X)
      (IF (LISTP X)
          (IF (EQUAL (CAR X) 'IPLUS)
              (IF (CANCEL-INEG-AUX (CADR X) (CADDR X))
                  (CANCEL-INEG-AUX (CADR X) (CADDR X))
		  X)
              X)
          X))

;; It seems a big win to turn off eval$.  I'll leave the recursive step out in
;; hopes that rewrite-eval$ handles it OK.

(prove-lemma eval$-list-cons (rewrite)
  (equal (eval$ 'list (cons x y) a)
	 (cons (eval$ t x a)
	       (eval$ 'list y a))))

(prove-lemma eval$-list-nlistp (rewrite)
  (implies (nlistp x)
	   (equal (eval$ 'list x a)
		  nil)))

(prove-lemma eval$-litatom (rewrite)
  (implies (litatom x)
	   (equal (eval$ t x a)
		  (cdr (assoc x a)))))

#|
(prove-lemma eval$-quotep (rewrite)
  (equal (eval$ t (list 'quote x) a)
	 x))
|#

;; In place of the above I'll do the following, from
;; the naturals library.
(enable eval$-quote)

(prove-lemma eval$-other (rewrite)
  (implies (and (not (litatom x))
		(nlistp x))
	   (equal (eval$ t x a)
		  x)))

(disable eval$)

;; What I'd like to do is say what (eval$ t (cancel-ineg-aux x y) a),
;; but a rewrite rule will loop because of the recursion.  So I
;; introduce a silly auxiliary function so that the opening-up
;; heuristics can help me.  The function body has (listp y) tests
;; so that it can be accepted.

(defn eval$-cancel-ineg-aux-fn (x y a)
  (if (and (listp x)
	   (equal (car x) 'ineg))
      (cond 
       ((equal y (cadr x))
	0)
       (t
	(let ((y1 (cadr y)) (y2 (caddr y)))
	  (if (equal y1 (cadr x))
	      (fix-int (eval$ t y2 a))
	    (if (listp y);; silly acceptability thing
		(iplus (eval$ t y1 a)
		       (eval$-cancel-ineg-aux-fn x y2 a))
	      0)))))
    (cond
     ((equal (car y) 'ineg)
      0)
     (t
      (let ((y1 (cadr y)) (y2 (caddr y)))
	(if (and (listp y1)
		 (equal (car y1) 'ineg)
		 (equal x (cadr y1)))
	    (fix-int (eval$ t y2 a))
	  (if (listp y);; silly acceptability thing
	      (iplus (eval$ t y1 a)
		     (eval$-cancel-ineg-aux-fn x y2 a))
	    0)))))))

(prove-lemma eval$-cancel-ineg-aux-is-its-fn (rewrite)
  (implies (not (equal (cancel-ineg-aux x y) f))
	   (equal (eval$ t (cancel-ineg-aux x y) a)
		  (eval$-cancel-ineg-aux-fn x y a))))

(prove-lemma iplus-ineg3 (rewrite)
  (equal (iplus (ineg x) (iplus x y))
	 (fix-int y))
  ((enable-theory integer-defns)))

(prove-lemma iplus-ineg4 (rewrite)
  (equal (iplus x (iplus (ineg x) y))
	 (fix-int y))
  ((use (iplus-ineg3 (x (ineg x)) (y y)))))

(prove-lemma iplus-ineg-promote (rewrite)
  (equal (iplus y (ineg x))
	 (iplus (ineg x) y)))

(prove-lemma iplus-x-y-ineg-x (rewrite)
  (equal (iplus x (iplus y (ineg x)))
	 (fix-int y)))
	     
(disable iplus-ineg-promote)

(prove-lemma correctness-of-cancel-ineg-aux (rewrite)
  (implies (not (equal (cancel-ineg-aux x y) f))
	   (equal (eval$-cancel-ineg-aux-fn x y a)
		  (iplus (eval$ t x a) (eval$ t y a))))
  ((induct (cancel-ineg-aux x y))))

(prove-lemma correctness-of-cancel-ineg ((meta iplus))
  (equal (eval$ t x a)
	 (eval$ t (cancel-ineg x) a))
  ((disable cancel-ineg-aux)))

(disable correctness-of-cancel-ineg-aux)

; --------------------------------------------------------------------------------
; Cancel IPLUS
; --------------------------------------------------------------------------------

;; All I do here is cancel like terms from both sides.  The problem of handling
;; INEG cancellation IS handled completely separately above.  That hasn't always
;; been the case -- in my first try I attempted to integrate the operations.
;; But now I see that for things like (equal z (iplus x (iplus y (ineg x))))
;; the integrated approach will fail.  Also, thanks to Matt Wilding, for pointing
;; out that the "four squares" example that Bill Pase sent me ran faster with
;; the newer approach (on his previously-implemented version for the rationals).

#| The function below has no AND or OR, for efficiency
(defn iplus-fringe (x)
  (if (and (listp x)
	   (equal (car x)
		  (quote iplus)))
      (append (iplus-fringe (cadr x))
	      (iplus-fringe (caddr x)))
      (cons x nil)))
|#

(DEFN IPLUS-FRINGE (X)
  (IF (LISTP X)
      (IF (EQUAL (CAR X) 'IPLUS)
	  (APPEND (IPLUS-FRINGE (CADR X)) (IPLUS-FRINGE (CADDR X)))
	  (LIST X))
      (LIST X)))

(prove-lemma lessp-count-listp-cdr (rewrite)
  (implies (listp (cdr x))
	   (lessp (count (cdr x)) (count x))))

(defn iplus-tree-rec (l)
  (if (nlistp (cdr l))
      (car l)
    (list (quote iplus)
	  (car l)
	  (iplus-tree-rec (cdr l)))))

(defn iplus-tree (l)
  (if (listp l)
      (if (listp (cdr l))
	  (iplus-tree-rec l)
	(list (quote fix-int)
	      (car l)))
    (quote (quote 0))))

(defn iplus-list (x)
  (if (listp x)
      (iplus (car x)
	     (iplus-list (cdr x)))
    0))

(prove-lemma integerp-iplus-list (rewrite)
  (integerp (iplus-list x)))

(prove-lemma eval$-iplus-tree-rec (rewrite)
  (equal (eval$ t (iplus-tree-rec x) a)
	 (if (listp x)
	     (if (listp (cdr x))
		 (iplus-list (eval$ 'list x a))
	       (eval$ t (car x) a))
	   0)))
	   
(prove-lemma eval$-iplus-tree (rewrite)
  (equal (eval$ t (iplus-tree x) a)
	 (iplus-list (eval$ 'list x a))))

(prove-lemma eval$-list-append (rewrite)
  (equal (eval$ 'list (append x y) a)
	 (append (eval$ 'list x a)
		 (eval$ 'list y a))))

#| The function below has no AND or OR, for efficiency
(defn cancel-iplus (x)
  (if (and (listp x)
	   (equal (car x) (quote equal)))
      (if (and (listp (cadr x))
	       (equal (caadr x) (quote iplus))
	       (listp (caddr x))
	       (equal (caaddr x) (quote iplus)))
	  (let ((xs (iplus-fringe (cadr x)))
		(ys (iplus-fringe (caddr x))))
	    (let ((bagint (bagint xs ys)))
	      (if (listp bagint)
		  (list (quote equal)
			(iplus-tree (bagdiff xs bagint))
			(iplus-tree (bagdiff ys bagint)))
		x)))
	(if (and (listp (cadr x))
		 (equal (caadr x) (quote iplus))
		 ;; We don't want to introduce the IF below unless something
		 ;; is "gained", or else we may get into an infinite rewriting loop.
		 (member (caddr x) (iplus-fringe (cadr x))))
	    (list (quote if)
		  (list (quote integerp) (caddr x))
		  (list (quote equal)
			(iplus-tree (delete (caddr x) (iplus-fringe (cadr x))))
			''0)
		  (list (quote quote) f))
	  (if (and (listp (caddr x))
		   (equal (caaddr x) (quote iplus))
		   (member (cadr x) (iplus-fringe (caddr x))))
	      (list (quote if)
		    (list (quote integerp) (cadr x))
		    (list (quote equal)
			  ''0
			  (iplus-tree (delete (cadr x) (iplus-fringe (caddr x)))))
		    (list (quote quote) f))
	    x)))
    x))
|#

(DEFN CANCEL-IPLUS (X)
  (IF (LISTP X)
      (IF (EQUAL (CAR X) 'EQUAL)
	  (COND
	   ((LISTP (CADR X))
	    (COND
	     ((EQUAL (CAADR X) 'IPLUS)
	      (COND
	       ((LISTP (CADDR X))
		(COND
		 ((EQUAL (CAADDR X) 'IPLUS)
		  (IF (LISTP (BAGINT (IPLUS-FRINGE (CADR X))
				     (IPLUS-FRINGE (CADDR X))))
		      (LIST 'EQUAL
			    (IPLUS-TREE
			     (BAGDIFF (IPLUS-FRINGE (CADR X))
                                      (BAGINT (IPLUS-FRINGE (CADR X))
					      (IPLUS-FRINGE (CADDR X)))))
			    (IPLUS-TREE
			     (BAGDIFF (IPLUS-FRINGE (CADDR X))
                                      (BAGINT (IPLUS-FRINGE (CADR X))
					      (IPLUS-FRINGE (CADDR X))))))
		      X))
		 ((MEMBER (CADDR X) (IPLUS-FRINGE (CADR X)))
		  (LIST 'IF (LIST 'INTEGERP (CADDR X))
			(CONS 'EQUAL
			      (CONS
			       (IPLUS-TREE
				(DELETE (CADDR X)
					(IPLUS-FRINGE (CADR X))))
			       '('0)))
			(LIST 'QUOTE F)))
		 (T X)))
	       ((MEMBER (CADDR X) (IPLUS-FRINGE (CADR X)))
		(LIST 'IF (LIST 'INTEGERP (CADDR X))
		      (CONS 'EQUAL
			    (CONS
			     (IPLUS-TREE
			      (DELETE (CADDR X)
                                      (IPLUS-FRINGE (CADR X))))
			     '('0)))
		      (LIST 'QUOTE F)))
	       (T X)))
	     ((LISTP (CADDR X))
	      (IF (EQUAL (CAADDR X) 'IPLUS)
		  (IF (MEMBER (CADR X) (IPLUS-FRINGE (CADDR X)))
		      (LIST 'IF (LIST 'INTEGERP (CADR X))
			    (LIST 'EQUAL ''0
				  (IPLUS-TREE
				   (DELETE (CADR X)
					   (IPLUS-FRINGE (CADDR X)))))
			    (LIST 'QUOTE F))
		      X)
		  X))
	     (T X)))
	   ((LISTP (CADDR X))
	    (IF (EQUAL (CAADDR X) 'IPLUS)
		(IF (MEMBER (CADR X) (IPLUS-FRINGE (CADDR X)))
		    (LIST 'IF (LIST 'INTEGERP (CADR X))
			  (LIST 'EQUAL ''0
				(IPLUS-TREE
				 (DELETE (CADR X)
					 (IPLUS-FRINGE (CADDR X)))))
			  (LIST 'QUOTE F))
		    X)
		X))
	   (T X))
	  X)
      X))

(lemma eval$-cancel-iplus (rewrite)
  (equal (eval$ t (cancel-iplus x) a)
	 (if (and (listp x)
		  (equal (car x) (quote equal)))
	     (if (and (listp (cadr x))
		      (equal (caadr x) (quote iplus))
		      (listp (caddr x))
		      (equal (caaddr x) (quote iplus)))
		 (let ((xs (iplus-fringe (cadr x)))
		       (ys (iplus-fringe (caddr x))))
		   (let ((bagint (bagint xs ys)))
		     (if (listp bagint)
			 (equal (iplus-list (eval$ 'list (bagdiff xs (bagint xs ys)) a))
				(iplus-list (eval$ 'list (bagdiff ys (bagint xs ys)) a)))
		       (eval$ t x a))))
	       (if (and (listp (cadr x))
			(equal (caadr x) (quote iplus))
			(member (caddr x) (iplus-fringe (cadr x))))
		   (if (integerp (eval$ t (caddr x) a))
		       (equal (iplus-list (eval$ 'list (delete (caddr x) (iplus-fringe (cadr x))) a))
			      0)
		     f)
		 (if (and (listp (caddr x))
			  (equal (caaddr x) (quote iplus))
			  (member (cadr x) (iplus-fringe (caddr x))))
		     (if (integerp (eval$ t (cadr x) a))
			 (equal 0
				(iplus-list (eval$ 'list (delete (cadr x) (iplus-fringe (caddr x))) a)))
		       f)
		   (eval$ t x a))))
	   (eval$ t x a)))
  ((enable eval$-iplus-tree cancel-iplus eval$-list-cons eval$-litatom eval$-quote)
   (disable eval$)))

(disable cancel-iplus)

(prove-lemma eval$-iplus-list-delete (rewrite)
  (implies (member z y)
	   (equal (iplus-list (eval$ 'list (delete z y) a))
		  (idifference (iplus-list (eval$ 'list y a))
			       (eval$ t z a)))))

(prove-lemma eval$-iplus-list-bagdiff (rewrite)
  (implies (subbagp x y)
	   (equal (iplus-list (eval$ 'list (bagdiff y x) a))
		  (idifference (iplus-list (eval$ 'list y a))
			       (iplus-list (eval$ 'list x a))))))

(prove-lemma iplus-list-append (rewrite)
  (equal (iplus-list (append x y))
	 (iplus (iplus-list x) (iplus-list y))))

(disable iplus-tree) ;; because we want to use EVAL$-IPLUS-TREE for now

(lemma not-integerp-implies-not-equal-iplus (rewrite)
       (implies (not (integerp a))
		(equal (equal a (iplus b c))
		       f))
       ((use (integerp-iplus (x b) (y c)))
	(enable integerp)
	(do-not-induct t)))

(prove-lemma iplus-list-eval$-fringe (rewrite)
       ;; similar to IPLUS-TREE-IPLUS-FRINGE
       (equal (iplus-list (eval$ 'list (iplus-fringe x) a))
	      (fix-int (eval$ t x a)))
       ((induct (iplus-fringe x))))

;; The following two lemmas aren't needed but they sure do
;; shorten the total proof time!!!

(prove-lemma iplus-ineg5-lemma-1 (rewrite)
  (implies (integerp x)
	   (equal (equal x (iplus y (iplus (ineg z) w)))
		  (equal x (iplus (ineg z) (iplus y w))))))

(prove-lemma iplus-ineg5-lemma-2 (rewrite)
  (implies (and (integerp x) (integerp v))
	   (equal (equal x (iplus (ineg z) v))
		  (equal (iplus x z) v))))

(lemma iplus-ineg5 (rewrite)
  (implies (integerp x)
	   (equal (equal x (iplus y (iplus (ineg z) w)))
		  (equal (iplus x z) (iplus y w))))
  ((enable iplus-ineg5-lemma-1 iplus-ineg5-lemma-2 integerp-iplus)))

(disable iplus-ineg5-lemma-1)

(disable iplus-ineg5-lemma-2)

(lemma iplus-ineg6 (rewrite)
  (implies (integerp x)
	   (equal (equal x (iplus y (iplus w (ineg z))))
		  (equal (iplus x z) (iplus y w))))
  ((use (iplus-ineg5)
	(commutativity-of-iplus (x w) (y (ineg z))))))

(prove-lemma eval$-iplus (rewrite)
  (implies (and (listp x)
		(equal (car x) 'iplus))
	   (equal (eval$ t x a)
		  (iplus (eval$ t (cadr x) a)
			 (eval$ t (caddr x) a)))))

(prove-lemma iplus-ineg7 (rewrite)
  (equal (equal 0 (iplus x (ineg y)))
	 (equal (fix-int y) (fix-int x)))
  ((enable-theory integer-defns)))

(prove-lemma correctness-of-cancel-iplus ((meta equal))
       (equal (eval$ t x a)
	      (eval$ t (cancel-iplus x) a)))

(disable iplus-ineg5)

(disable iplus-ineg6)

; --------------------------------------------------------------------------------
; Cancel IPLUS from ILESSP
; --------------------------------------------------------------------------------

;; This is similar to the cancellation of IPLUS terms from equalities,
;; handled above, and uses many of the same lemmas.  A small but definite
;; difference however is that for ILESSP we don't have to fix integers.

;; By luck we have that iplus-tree-rec is appropriate here, since
;; the lemma eval$-iplus-tree-rec shows that it (accidentally) behaves
;; properly on the empty list.

(prove-lemma ilessp-fix-int-1 (rewrite)
  (equal (ilessp (fix-int x) y)
	 (ilessp x y))
  ((enable-theory integer-defns)))

(prove-lemma ilessp-fix-int-2 (rewrite)
  (equal (ilessp x (fix-int y))
	 (ilessp x y))
  ((enable-theory integer-defns)))

;; Perhaps the easiest approach is to do everything with respect to the
;; same IPLUS-TREE function that we used before, and then once the
;; supposed meta-lemma is proved, go back and show that we get the
;; same answer if we use a version that doesn't fix-int singleton fringes.

(defn make-cancel-iplus-inequality-1 (x y)
  ;; x and y are term lists
  (list (quote ilessp)
	(iplus-tree (bagdiff
		     x
		     (bagint x y)))
	(iplus-tree (bagdiff
		     y
		     (bagint x y)))))

#| The function below has no AND or OR, for efficiency
(defn cancel-iplus-ilessp-1 (x)
  (if (and (listp x)
	   (equal (car x) (quote ilessp)))
      (make-cancel-iplus-inequality-1 (iplus-fringe (cadr x))
				      (iplus-fringe (caddr x)))
    x))
|#

(DEFN CANCEL-IPLUS-ILESSP-1 (X)
  (IF (LISTP X)
      (IF (EQUAL (CAR X) 'ILESSP)
	  (MAKE-CANCEL-IPLUS-INEQUALITY-1 (IPLUS-FRINGE (CADR X))
					  (IPLUS-FRINGE (CADDR X)))
	  X)
      X))

;; Notice that IPLUS-TREE-NO-FIX-INT is currently enabled, which is
;; good since we want to use EVAL$-IPLUS-TREE-NO-FIX-INT for now.

(prove-lemma lessp-difference-plus-arg1 (rewrite)
  (equal (lessp w (difference (plus w y) x))
	 (lessp x y)))

(prove-lemma lessp-difference-plus-arg1-commuted (rewrite)
  (equal (lessp w (difference (plus y w) x))
	 (lessp x y)))

(prove-lemma iplus-cancellation-1-for-ilessp (rewrite)
       (equal (ilessp (iplus a b) (iplus a c))
	      (ilessp b c))
       ((enable-theory integer-defns)))

(prove-lemma iplus-cancellation-2-for-ilessp (rewrite)
       (equal (ilessp (iplus b a) (iplus c a))
	      (ilessp b c)))

(prove-lemma correctness-of-cancel-iplus-ilessp-lemma nil
       (equal (eval$ t x a)
	      (eval$ t (cancel-iplus-ilessp-1 x) a)))

(defn iplus-tree-no-fix-int (l)
  (if (listp l)
      (iplus-tree-rec l)
    (quote (quote 0))))

(prove-lemma eval$-ilessp-iplus-tree-no-fix-int (rewrite)
  (equal (ilessp (eval$ t (iplus-tree-no-fix-int x) a)
		 (eval$ t (iplus-tree-no-fix-int y) a))
	 (ilessp (eval$ t (iplus-tree x) a)
		 (eval$ t (iplus-tree y) a))))

(disable iplus-tree-no-fix-int)

(lemma make-cancel-iplus-inequality-simplifier (rewrite)
       (equal (eval$ t (make-cancel-iplus-inequality-1 x y) a)
	      (eval$ t (list (quote ilessp)
			     (iplus-tree-no-fix-int (bagdiff
						     x
						     (bagint x y)))
			     (iplus-tree-no-fix-int (bagdiff
						     y
						     (bagint x y)))) a))
       ((enable make-cancel-iplus-inequality-1
		eval$-ilessp-iplus-tree-no-fix-int)
	(disable eval$)))

#| The function below has no AND or OR, for efficiency
(defn cancel-iplus-ilessp (x)
  (if (and (listp x)
	   (equal (car x) (quote ilessp)))
      (let ((x1 (iplus-fringe (cadr x)))
	    (y1 (iplus-fringe (caddr x))))
	(let ((bagint (bagint x1 y1)))
	  (if (listp bagint)
	      ;; I check (listp bagint) only for efficiency
	      (list (quote ilessp)
		    (iplus-tree-no-fix-int (bagdiff x1 bagint))
		    (iplus-tree-no-fix-int (bagdiff y1 bagint)))
	    x)))
    x))
|#

;; **** Should perhaps check that some argument of the ILESSP has function
;; symbol IPLUS, or else we may wind up dealing with (ILESSP 0 0).  That should
;; be harmless enough, though, even if *1*IPLUS is disabled; we'll just get the
;; same term back, the hard way.

(DEFN CANCEL-IPLUS-ILESSP (X)
  (IF (LISTP X)
      (IF (EQUAL (CAR X) 'ILESSP)
	  (IF (LISTP (BAGINT (IPLUS-FRINGE (CADR X))
			     (IPLUS-FRINGE (CADDR X))))
	      (LIST 'ILESSP
		    (IPLUS-TREE-NO-FIX-INT
		     (BAGDIFF (IPLUS-FRINGE (CADR X))
			      (BAGINT (IPLUS-FRINGE (CADR X))
                                      (IPLUS-FRINGE (CADDR X)))))
		    (IPLUS-TREE-NO-FIX-INT
		     (BAGDIFF (IPLUS-FRINGE (CADDR X))
			      (BAGINT (IPLUS-FRINGE (CADR X))
                                      (IPLUS-FRINGE (CADDR X))))))
	      X)
	  X)
      X))

(disable make-cancel-iplus-inequality-1)

(prove-lemma correctness-of-cancel-iplus-ilessp ((meta ilessp))
       (equal (eval$ t x a)
	      (eval$ t (cancel-iplus-ilessp x) a))
       ((use (correctness-of-cancel-iplus-ilessp-lemma))))

; ---------- Multiplication ----------

(lemma itimes-zero1 (rewrite)
       (implies (equal (fix-int x) 0)
		(equal (itimes x y) 0))
       ((enable itimes times fix-int integerp)
	(do-not-induct t)))

(prove-lemma itimes-0-left (rewrite)
       (equal (itimes 0 y) 0))

;; I don't want the backchaining to slow down the prover.
(disable itimes-zero1)

(lemma itimes-zero2 (rewrite)
       (implies (equal (fix-int y) 0)
		(equal (itimes x y) 0))
       ((enable itimes fix-int integerp times-zero)
	(do-not-induct t)))

(prove-lemma itimes-0-right (rewrite)
       (equal (itimes x 0) 0))

;; I don't want the backchaining to slow down the prover.
(disable itimes-zero2)

(lemma itimes-fix-int1 (rewrite)
       (equal (itimes (fix-int a) b)
	      (itimes a b))
       ((enable itimes fix-int integerp)
	(do-not-induct t)))

(lemma itimes-fix-int2 (rewrite)
       (equal (itimes a (fix-int b))
	      (itimes a b))
       ((enable itimes fix-int integerp times-zero)
	(do-not-induct t)))

(lemma commutativity-of-itimes (rewrite)
       (equal (itimes x y) (itimes y x))
       ((enable itimes fix-int integerp)
	(enable-theory multiplication)
	(do-not-induct t)))

(lemma itimes-distributes-over-iplus-proof ()
       (equal (itimes x (iplus y z))
	      (iplus (itimes x y) (itimes x z)))
       ((enable itimes iplus integerp fix-int
		commutativity2-of-iplus associativity-of-iplus)
	(enable-theory multiplication addition)
	(do-not-induct t)))

(lemma itimes-distributes-over-iplus (rewrite)
       (and (equal (itimes x (iplus y z))
		   (iplus (itimes x y) (itimes x z)))
	    (equal (itimes (iplus x y) z)
		   (iplus (itimes x z) (itimes y z))))
       ((use (itimes-distributes-over-iplus-proof (x x) (y y) (z z))
	     (itimes-distributes-over-iplus-proof (x z) (y x) (z y)))
	(enable commutativity-of-itimes)))

(lemma commutativity2-of-itimes (rewrite)
       (equal (itimes x (itimes y z))
	      (itimes y (itimes x z)))
       ((enable itimes integerp fix-int)
	(enable-theory multiplication)
	(do-not-induct t)))

(lemma associativity-of-itimes (rewrite)
       (equal (itimes (itimes x y) z) 
	      (itimes x (itimes y z)))
       ((enable itimes integerp fix-int)
	(enable-theory multiplication)
	(do-not-induct t)))

(lemma equal-itimes-0 (rewrite)
       (equal (equal (itimes x y) 0)
	      (or (equal (fix-int x) 0)
		  (equal (fix-int y) 0)))
       ((enable itimes integerp fix-int)
	(enable-theory multiplication)
	(do-not-induct t)))

(lemma equal-itimes-1 (rewrite)
       (equal (equal (itimes a b) 1)
	      (or (and (equal a 1)
		       (equal b 1))
		  (and (equal a -1)
		       (equal b -1))))
       ((enable itimes integerp fix-int)
	(enable-theory multiplication)
	(do-not-induct t)))

(lemma equal-itimes-minus-1 (rewrite)
       (equal (equal (itimes a b) -1)
	      (or (and (equal a -1)
		       (equal b 1))
		  (and (equal a 1)
		       (equal b -1))))
       ((enable itimes integerp fix-int)
	(enable-theory multiplication)
	(do-not-induct t)))

(lemma itimes-1-arg1 (rewrite)
       (equal (itimes 1 x) (fix-int x))
       ((enable integerp fix-int itimes)
	(enable-theory multiplication)
	(do-not-induct t)))

; ---------- Division ----------

(lemma quotient-remainder-uniqueness ()
       (implies (and (equal a (plus r (times b q)))
		     (lessp r b))
		(and (equal (fix r) (remainder a b))
		     (equal (fix q) (quotient a b))))
       ((enable-theory naturals)
	(enable remainder quotient)))


; We want to define IQUOTIENT and IREMAINDER. The standard approach to
; integer division derives from from the following theorem.
;
; Division Theorem:
; For all integers i,j, j not 0, there exist unique integers q and r
; which satisfy  i = jq + r,  0 <= r < |j|.
;
; The functions IQUOTIENT and IREMAINDER are intended to compute q and r.
; Therefore, to be satisfied that we have the right definitions, we must
; prove the above theorem.

(prove-lemma division-theorem-part1 ()
       (implies (integerp i)
		(equal (iplus (iremainder i j) (itimes j (iquotient i j)))
		       i)))

(prove-lemma division-theorem-part2 ()
       (implies (and (integerp j)
		     (not (equal j 0)))
		(not (ilessp (iremainder i j) 0)))
       ((enable-theory integer-defns)))

(prove-lemma division-theorem-part3 ()
       (implies (and (integerp j)
		     (not (equal j 0)))
		(ilessp (iremainder i j) (iabs j)))
       ((enable-theory integer-defns)))

(lemma division-theorem ()
       (implies (and (integerp i)
		     (integerp j)
		     (not (equal j 0)))
		(and (equal (iplus (iremainder i j) (itimes j (iquotient i j)))
			    i)
		     (not (ilessp (iremainder i j) 0))
		     (ilessp (iremainder i j) (iabs j))))
       ((use (division-theorem-part1 (i i) (j j))
	     (division-theorem-part2 (i i) (j j))
	     (division-theorem-part3 (i i) (j j)))))

(lemma quotient-difference-lessp-arg2 (rewrite)
       (implies (and (equal (remainder a c) 0)
		     (lessp b c))
		(equal (quotient (difference a b) c)
		       (if (zerop b)
			   (quotient a c)
			   (if (lessp b a)
			       (difference (quotient a c)
					   (add1 (quotient b c)))
			       0))))
       ((enable-theory naturals)
	(do-not-induct t)))

(lemma iquotient-iremainder-uniqueness ()
       (implies (and (integerp i)
		     (integerp j)
		     (integerp r)
		     (integerp q)
		     (not (equal j 0))
		     (equal i (iplus r (itimes j q)))
		     (not (ilessp r 0))
		     (ilessp r (iabs j)))
		(and (equal r (iremainder i j))
		     (equal q (iquotient i j))))
       ((enable iremainder iabs idifference iplus ineg
		fix-int itimes iquotient ilessp integerp
		quotient-difference-lessp-arg2)	
	(enable-theory naturals)
	(do-not-induct t)))
 
; It turns out that in computer arithmetic, notions of division other than that
; given by the division theorem are used. Two in particular, called
; "truncate towards negative infinity" and "truncate towards zero" are common.
; We present their definitions here. 

; Division Theorem (truncate towards negative infinity variant):
;
; For all integers i,j, j not 0, there exist unique integers q and r
; which satisfy  
;                i = jq + r,  0 <= r <  j  (j > 0)
;                             j <  r <= 0  (j < 0)
;
; In this version the integer quotient of two integers is the integer floor
; of the real quotient of the integers. The remainder has the sign of the
; divisor. The functions IDIV and IMOD are intended to compute q and r.
; Therefore, to be satisfied that we have the right definitions, we must
; prove the above theorem.

(prove-lemma division-theorem-for-truncate-to-neginf-part1 ()
       (implies (integerp i)
		(equal (iplus (imod i j) (itimes j (idiv i j)))
		       i))
       ((enable-theory integer-defns)))

(lemma division-theorem-for-truncate-to-neginf-part2 ()
       (implies (ilessp 0 j)
		(and (not (ilessp (imod i j) 0))
		     (ilessp (imod i j) j)))
       ((enable imod ilessp idifference iplus ineg
		itimes idiv integerp fix-int)
	(enable-theory naturals)
	(do-not-induct t)))

(lemma division-theorem-for-truncate-to-neginf-part3 ()
       (implies (and (integerp j)
		     (ilessp j 0))
		(and (not (ilessp 0 (imod i j)))
		     (ilessp j (imod i j))))
       ((enable imod ilessp idifference iplus ineg
		itimes idiv integerp fix-int)
	(enable-theory naturals)
	(do-not-induct t)))

(lemma division-theorem-for-truncate-to-neginf ()
       (implies (and (integerp i)
		     (integerp j)
		     (not (equal j 0)))
		(and (equal (iplus (imod i j) (itimes j (idiv i j)))
			    i)
		     (if (ilessp 0 j)
			 (and (not (ilessp (imod i j) 0))
			      (ilessp (imod i j) j))
			 (and (not (ilessp 0 (imod i j)))
			      (ilessp j (imod i j))))))
       ((use (division-theorem-for-truncate-to-neginf-part1 (i i) (j j))
	     (division-theorem-for-truncate-to-neginf-part2 (i i) (j j))
	     (division-theorem-for-truncate-to-neginf-part3 (i i) (j j)))
	(enable integerp ilessp)
	(do-not-induct t)))

(lemma idiv-imod-uniqueness ()
       (implies (and (integerp i)
		     (integerp j)
		     (integerp r)
		     (integerp q)
		     (not (equal j 0))
		     (equal i (iplus r (itimes j q)))
		     (if (ilessp 0 j)
			 (and (not (ilessp r 0))
			      (ilessp r j))
			 (and (not (ilessp 0 r))
			      (ilessp j r))))
		(and (equal r (imod i j))
		     (equal q (idiv i j))))
       ((enable imod iabs idifference iplus ineg
		fix-int itimes idiv ilessp integerp
		;lessp-plus-times-crock
		;lessp-times-crock1
		;lessp-times-crock2
		;lessp-times-crock3
		;lessp-times-crock4
		quotient-difference-lessp-arg2)	
	(enable-theory naturals)
	(do-not-induct t)))

; Division Theorem (truncate towards zero variant):
;
; For all integers i,j, j not 0, there exist unique integers q and r
; which satisfy  
;                i = jq + r,     0 <=  r  <  |j|  (i => 0)
;                             -|j| <   r  <= 0    (i < 0)
;
; In this version (iquo, irem), the integer quotient of two integers is the integer floor
; of the real quotient of the integers, if the real quotient is positive. If the
; real quotient is negative, the integer quotient is the integer ceiling of the
; real quotient. The remainder has the sign of the dividend. The functions IQUO 
; and IREM are intended to compute q and r. Therefore, to be satisfied that we
; have the right definitions, we must prove the above theorem.

(prove-lemma division-theorem-for-truncate-to-zero-part1 ()
       (implies (integerp i)
		(equal (iplus (irem i j) (itimes j (iquo i j)))
		       i))
       ((enable-theory integer-defns)))

(prove-lemma division-theorem-for-truncate-to-zero-part2 ()
       (implies (and (integerp i)
		     (integerp j)
		     (not (equal j 0))
		     (not (ilessp i 0)))
		(and (not (ilessp (irem i j) 0))
		     (ilessp (irem i j) (iabs j))))
       ((enable-theory integer-defns)))

(prove-lemma division-theorem-for-truncate-to-zero-part3 ()
       (implies (and (integerp i)
		     (integerp j)
		     (not (equal j 0))
		     (ilessp i 0))
		(and (not (ilessp 0 (irem i j)))
		     (ilessp (ineg (iabs j)) (irem i j))))
       ((enable-theory integer-defns)))

(lemma division-theorem-for-truncate-to-zero ()
       (implies (and (integerp i)
		     (integerp j)
		     (not (equal j 0)))
		(and (equal (iplus (irem i j) (itimes j (iquo i j)))
			    i)
		     (if (not (ilessp i 0))
			 (and (not (ilessp (irem i j) 0))
			      (ilessp (irem i j) (iabs j)))
			 (and (not (ilessp 0 (irem i j)))
			      (ilessp (ineg (iabs j)) (irem i j))))))
       ((use (division-theorem-for-truncate-to-zero-part1 (i i) (j j))
	     (division-theorem-for-truncate-to-zero-part2 (i i) (j j))
	     (division-theorem-for-truncate-to-zero-part3 (i i) (j j)))
	(enable integerp ilessp)
	(do-not-induct t)))

(prove-lemma iquo-irem-uniqueness ()
       (implies (and (integerp i)
		     (integerp j)
		     (integerp r)
		     (integerp q)
		     (not (equal j 0))
		     (equal i (iplus r (itimes j q)))
		     (if (not (ilessp i 0))
			 (and (not (ilessp r 0))
			      (ilessp r (iabs j)))
			 (and (not (ilessp 0 r))
			      (ilessp (ineg (iabs j)) r))))
		(and (equal r (irem i j))
		     (equal q (iquo i j))))
       ((enable-theory integer-defns)))

; ---------- Multiplication Facts

(prove-lemma itimes-ineg-1 (rewrite)
  (equal (itimes (ineg x) y)
	 (ineg (itimes x y)))
  ((enable-theory integer-defns)))

(prove-lemma itimes-ineg-2 (rewrite)
  (equal (itimes x (ineg y))
	 (ineg (itimes x y)))
  ((enable-theory integer-defns)))

(prove-lemma itimes-cancellation-1 (rewrite)
       (equal (equal (itimes a b) (itimes a c))
	      (or (equal (fix-int a) 0)
		  (equal (fix-int b) (fix-int c))))
       ((enable-theory integer-defns)))

(lemma itimes-cancellation-2 (rewrite)
       (equal (equal (itimes b a) (itimes c a))
	      (or (equal (fix-int a) 0)
		  (equal (fix-int b) (fix-int c))))
       ((use (itimes-cancellation-1))
	(enable commutativity-of-itimes)))

(lemma itimes-cancellation-3 (rewrite)
       (equal (equal (itimes a b) (itimes c a))
	      (or (equal (fix-int a) 0)
		  (equal (fix-int b) (fix-int c))))
       ((use (itimes-cancellation-1))
	(enable commutativity-of-itim