#|
 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.
|#
; Matt Kaufmann, William R. Bevier, and Matt Wilding

Event: Start with the library "naturals" using the compiled version.

;; from /disk1/wilding/nums/integers.events.
;; 15 January 91 version by Matt Wilding.  Includes all of the
;; Matt Kaufmann's library's functionality, plus various additional
;; facts and numerous tiny changes, mostly having to do with igcd
;; and irem.
;; Several theories are set up:
;; integers  -  general integer strategy
;; integer-defns - integer definitions (does not include igcd)
;; nats-to-ints - rules that rewrite naturals to integers
;; 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))))))
|#

Definition: integerp (x) = if x ∈ N then t

elseif negativep (x) then negative-guts (x) ≄ 0 else f endif

Definition: fix-int (x) = if integerp (x) then x

else 0 endif

;; Even though I'll include a definition for izerop here, I'll
;; often avoid using it.

Definition: izerop (i) = (fix-int (i) = 0)

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

|#

Definition: ilessp (i, j ) = if negativep (i)

then if negativep (j ) then negative-guts (j ) < negative-guts (i) elseif i = (− 0) then 0 < j else t endif elseif negativep (j ) then f else i < j endif

Definition: ileq (i, j ) = (¬ ilessp (j , i))

Definition: iplus (x, y) = if negativep (x)

then if negativep (y)

then if (negative-guts (x) ≃ 0) ∧ (negative-guts (y) ≃ 0) then 0 else − (negative-guts (x) + negative-guts (y)) endif elseif y < negative-guts (x) then − (negative-guts (x) − y) else y − negative-guts (x) endif

elseif negativep (y)

then if x < negative-guts (y) then − (negative-guts (y) − x)

else x − negative-guts (y) endif else x + y endif

Definition: ineg (x) = if negativep (x) then negative-guts (x)

elseif x ≃ 0 then 0

else − x endif

Definition: idifference (x, y) = iplus (x, ineg (y))

Definition: iabs (i) = if negativep (i) then negative-guts (i)

else fix (i) endif

Definition: itimes (i, j ) = if negativep (i)

then if negativep (j ) then negative-guts (i) ∗ negative-guts (j )

else fix-int (− (negative-guts (i) ∗ j )) endif elseif negativep (j ) then fix-int (− (i ∗ negative-guts (j ))) else i ∗ j endif Definition: iquotient (i, j ) = if fix-int (j ) = 0 then 0

elseif negativep (i) then if negativep (j )

then if (negative-guts (i) mod negative-guts (j )) = 0 then negative-guts (i) ÷ negative-guts (j ) else 1 + (negative-guts (i) ÷ negative-guts (j )) endif

elseif (negative-guts (i) mod j ) = 0 then fix-int (− (negative-guts (i) ÷ j )) else fix-int (− (1 + (negative-guts (i) ÷ j ))) endif elseif negativep (j ) then fix-int (− (i ÷ negative-guts (j ))) else i ÷ j endif

Definition: iremainder (i, j ) = idifference (i, itimes (j , iquotient (i, j )))

Definition: idiv (i, j ) = if fix-int (j ) = 0 then 0

elseif negativep (i)

then if negativep (j ) then negative-guts (i) ÷ negative-guts (j ) elseif (negative-guts (i) mod j ) = 0 then fix-int (− (negative-guts (i) ÷ j )) else fix-int (− (1 + (negative-guts (i) ÷ j ))) endif

elseif negativep (j )

then if (i mod negative-guts (j )) = 0 then fix-int (− (i ÷ negative-guts (j ))) else fix-int (− (1 + (i ÷ negative-guts (j )))) endif

else i ÷ j endif

Definition: imod (i, j ) = idifference (fix-int (i), itimes (j , idiv (i, j )))

Definition: iquo (i, j ) = if fix-int (j ) = 0 then 0

elseif negativep (i)

then if negativep (j ) then negative-guts (i) ÷ negative-guts (j )

else fix-int (− (negative-guts (i) ÷ j )) endif elseif negativep (j ) then fix-int (− (i ÷ negative-guts (j ))) else i ÷ j endif

Definition: irem (i, j ) = idifference (fix-int (i), itimes (j , iquo (i, j )))

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

Event: Let us define the theory integer-defns to consist of the following events: integerp, fix-int, ilessp, iplus, ineg, iabs, itimes, iquotient, iremainder, idiv, imod, iquo, irem, ileq, idifference, izerop.

Event: Disable integerp.

Event: Disable fix-int.

Event: Disable ilessp.

Event: Disable iplus.

Event: Disable ineg.

Event: Disable iabs.

Event: 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 ----------

Theorem: integerp-fix-int integerp (fix-int (x))

Theorem: integerp-iplus integerp (iplus (x, y))

Theorem: integerp-idifference integerp (idifference (x, y))

Theorem: integerp-ineg integerp (ineg (x))

Theorem: integerp-iabs integerp (iabs (x))

Theorem: integerp-itimes integerp (itimes (x, y))

; ---------- 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.

Theorem: fix-int-remover integerp (x) → (fix-int (x) = x)

Theorem: fix-int-fix-int fix-int (fix-int (x)) = fix-int (x)

Theorem: fix-int-iplus fix-int (iplus (a, b)) = iplus (a, b)

Theorem: fix-int-idifference fix-int (idifference (a, b)) = idifference (a, b)

Theorem: fix-int-ineg fix-int (ineg (x)) = ineg (x)

Theorem: fix-int-iabs fix-int (iabs (x)) = iabs (x)

Theorem: fix-int-itimes fix-int (itimes (x, y)) = itimes (x, y)

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

Theorem: ineg-iplus ineg (iplus (a, b)) = iplus (ineg (a), ineg (b))

Theorem: ineg-ineg ineg (ineg (x)) = fix-int (x)

Theorem: ineg-fix-int ineg (fix-int (x)) = ineg (x)

Theorem: ineg-of-non-integerp (¬ integerp (x)) → (ineg (x) = 0)

;; I don't want the backchaining to slow down the prover.

Event: Disable ineg-of-non-integerp.

Theorem: ineg-0 ineg (0) = 0

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

Theorem: iplus-left-id (¬ integerp (x)) → (iplus (x, y) = fix-int (y))

;; I don't want the backchaining to slow down the prover.

Event: Disable iplus-left-id.

Theorem: iplus-right-id (¬ integerp (y)) → (iplus (x, y) = fix-int (x))

;; I don't want the backchaining to slow down the prover.

Event: Disable iplus-right-id.

Theorem: iplus-0-left iplus (0, x) = fix-int (x)

Theorem: iplus-0-right iplus (x, 0) = fix-int (x)

Theorem: commutativity2-of-iplus iplus (x, iplus (y, z)) = iplus (y, iplus (x, z))

Theorem: commutativity-of-iplus iplus (x, y) = iplus (y, x)

Theorem: associativity-of-iplus iplus (iplus (x, y), z) = iplus (x, iplus (y, z))

Theorem: iplus-cancellation-1 (iplus (a, b) = iplus (a, c)) = (fix-int (b) = fix-int (c))

Theorem: iplus-cancellation-2 (iplus (b, a) = iplus (c, a)) = (fix-int (b) = fix-int (c))

Theorem: iplus-ineg1 iplus (ineg (a), a) = 0

Theorem: iplus-ineg2 iplus (a, ineg (a)) = 0

Theorem: iplus-fix-int1 iplus (fix-int (a), b) = iplus (a, b)

Theorem: iplus-fix-int2 iplus (a, fix-int (b)) = iplus (a, b)

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

Theorem: idifference-fix-int1 idifference (fix-int (a), b) = idifference (a, b)

Theorem: idifference-fix-int2 idifference (a, fix-int (b)) = idifference (a, b)

; --------------------------------------------------------------------------------
; 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))))
|#

Definition: cancel-ineg-aux (x, y) = if listp (x)

then if car (x) = 'ineg

then if y = cadr (x) then ''0 elseif listp (y) then if car (y) = 'iplus

then if cadr (y) = cadr (x) then list ('fix-int, caddr (y)) elseif cancel-ineg-aux (x, caddr (y)) then list ('iplus,

cadr (y),

cancel-ineg-aux (x, caddr (y)))

else f endif else f endif

else f endif elseif y ≃ nil then f elseif car (y) = 'ineg then if x = cadr (y) then ''0

else f endif elseif car (y) = 'iplus then if listp (cadr (y))

then if caadr (y) = 'ineg

then if x = cadadr (y)

then list ('fix-int, caddr (y)) elseif cancel-ineg-aux (x, caddr (y)) then list ('iplus,

cadr (y),

cancel-ineg-aux (x, caddr (y)))

else f endif elseif cancel-ineg-aux (x, caddr (y)) then list ('iplus, cadr (y), cancel-ineg-aux (x, caddr (y))) else f endif

elseif cancel-ineg-aux (x, caddr (y)) then list ('iplus, cadr (y), cancel-ineg-aux (x, caddr (y))) else f endif

else f endif elseif y ≃ nil then f elseif car (y) = 'ineg then if x = cadr (y) then ''0

else f endif elseif car (y) = 'iplus then if listp (cadr (y))

then if caadr (y) = 'ineg

then if x = cadadr (y) then list ('fix-int, caddr (y)) elseif cancel-ineg-aux (x, caddr (y)) then list ('iplus, cadr (y), cancel-ineg-aux (x, caddr (y))) else f endif

elseif cancel-ineg-aux (x, caddr (y)) then list ('iplus, cadr (y), cancel-ineg-aux (x, caddr (y))) else f endif

elseif cancel-ineg-aux (x, caddr (y)) then list ('iplus, cadr (y), cancel-ineg-aux (x, caddr (y))) else f endif

else f endif

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

Definition: cancel-ineg (x) = if listp (x)

then if car (x) = 'iplus

then if cancel-ineg-aux (cadr (x), caddr (x)) then cancel-ineg-aux (cadr (x), caddr (x)) else x endif

else x endif else x endif

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

Theorem: eval$-list-cons eval$ ('list, cons (x, y), a) = cons (eval$ (t, x, a), eval$ ('list, y, a))

Theorem: eval$-list-nlistp (x ≃ nil) → (eval$ ('list, x, a) = nil)

Theorem: eval$-litatom litatom (x) → (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.

Event: Enable eval$-quote.

Theorem: eval$-other ((¬ litatom (x)) ∧ (x ≃ nil)) → (eval$ (t, x, a) = x)

Event: 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.

Definition: eval$-cancel-ineg-aux-fn (x, y, a) = if listp (x) ∧ (car (x) = 'ineg)

then if y = cadr (x) then 0

else let y1 be cadr (y),

y2 be caddr (y) in if y1 = cadr (x) then fix-int (eval$ (t, y2 , a)) elseif listp (y) then iplus (eval$ (t, y1 , a),

eval$-cancel-ineg-aux-fn (x, y2 , a))

else 0 endif endlet endif

else if car (y) = 'ineg then 0 else let y1 be cadr (y),

y2 be caddr (y) in if listp (y1 )

∧ (car (y1 ) = 'ineg) ∧ (x = cadr (y1 )) then fix-int (eval$ (t, y2 , a)) elseif listp (y) then iplus (eval$ (t, y1 , a),

eval$-cancel-ineg-aux-fn (x, y2 , a))

else 0 endif endlet endif endif

Theorem: eval$-cancel-ineg-aux-is-its-fn (cancel-ineg-aux (x, y) ≠ f) → (eval$ (t, cancel-ineg-aux (x, y), a) = eval$-cancel-ineg-aux-fn (x, y, a))

Theorem: iplus-ineg3 iplus (ineg (x), iplus (x, y)) = fix-int (y)

Theorem: iplus-ineg4 iplus (x, iplus (ineg (x), y)) = fix-int (y)

Theorem: iplus-ineg-promote iplus (y, ineg (x)) = iplus (ineg (x), y)

Theorem: iplus-x-y-ineg-x iplus (x, iplus (y, ineg (x))) = fix-int (y)

Event: Disable iplus-ineg-promote.

Theorem: correctness-of-cancel-ineg-aux (cancel-ineg-aux (x, y) ≠ f) → (eval$-cancel-ineg-aux-fn (x, y, a) = iplus (eval$ (t, x, a), eval$ (t, y, a)))

Theorem: correctness-of-cancel-ineg eval$ (t, x, a) = eval$ (t, cancel-ineg (x), a)

Event: 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)))
|#

Definition: iplus-fringe (x) = if listp (x)

then if car (x) = 'iplus then append (iplus-fringe (cadr (x)), iplus-fringe (caddr (x))) else list (x) endif

else list (x) endif Theorem: lessp-count-listp-cdr listp (cdr (x)) → (count (cdr (x)) < count (x))

Definition: iplus-tree-rec (l) = if cdr (l) ≃ nil then car (l)

else list ('iplus, car (l), iplus-tree-rec (cdr (l))) endif

Definition: iplus-tree (l) = if listp (l)

then if listp (cdr (l)) then iplus-tree-rec (l) else list ('fix-int, car (l)) endif

else ''0 endif

Definition: iplus-list (x) = if listp (x) then iplus (car (x), iplus-list (cdr (x)))

else 0 endif

Theorem: integerp-iplus-list integerp (iplus-list (x))

Theorem: eval$-iplus-tree-rec eval$ (t, iplus-tree-rec (x), a) = if listp (x)

then if listp (cdr (x)) then iplus-list (eval$ ('list, x, a))

else eval$ (t, car (x), a) endif else 0 endif

Theorem: eval$-iplus-tree eval$ (t, iplus-tree (x), a) = iplus-list (eval$ ('list, x, a))

Theorem: eval$-list-append 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))
|#

Definition: cancel-iplus (x) = if listp (x)

then if car (x) = 'equal

then if listp (cadr (x))

then if caadr (x) = 'iplus

then if listp (caddr (x))

then if caaddr (x) = 'iplus

then if listp (bagint (iplus-fringe (cadr (x)),

iplus-fringe (caddr (x))))

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

else x endif elseif caddr (x) ∈ iplus-fringe (cadr (x)) then list ('if,

list ('integerp, caddr (x)),

cons ('equal,

cons (iplus-tree (delete (caddr (x),

iplus-fringe (cadr (x)))),

         '('0))),

list ('quote, f))

else x endif elseif caddr (x) ∈ iplus-fringe (cadr (x)) then list ('if,

list ('integerp, caddr (x)),

cons ('equal,

cons (iplus-tree (delete (caddr (x),

iplus-fringe (cadr (x)))),

    '('0))),

list ('quote, f))

else x endif elseif listp (caddr (x)) then if caaddr (x) = 'iplus

then if cadr (x) ∈ iplus-fringe (caddr (x))

then list ('if, list ('integerp, cadr (x)),

list ('equal,
    ''0,

iplus-tree (delete (cadr (x),

iplus-fringe (caddr (x))))),

list ('quote, f))

else x endif else x endif

else x endif elseif listp (caddr (x)) then if caaddr (x) = 'iplus

then if cadr (x) ∈ iplus-fringe (caddr (x))

then list ('if, list ('integerp, cadr (x)),

list ('equal,

iplus-tree (delete (cadr (x),

iplus-fringe (caddr (x))))),

list ('quote, f))

else x endif else x endif

else x endif else x endif

else x endif

Theorem: eval$-cancel-iplus eval$ (t, cancel-iplus (x), a) = if listp (x) ∧ (car (x) = 'equal)

then if listp (cadr (x)) ∧ (caadr (x) = 'iplus) ∧ listp (caddr (x)) ∧ (caaddr (x) = 'iplus)

then let xs be iplus-fringe (cadr (x)),

ys be iplus-fringe (caddr (x)) in let bagint be bagint (xs, ys) in if listp (bagint) then iplus-list (eval$ ('list,

bagdiff (xs,

bagint (xs, ys)), a))

= iplus-list (eval$ ('list,

bagdiff (ys,

bagint (xs,

ys)),

a))

else eval$ (t, x, a) endif endlet endlet elseif listp (cadr (x))

∧ (caadr (x) = 'iplus) ∧ (caddr (x) ∈ iplus-fringe (cadr (x)))

then if integerp (eval$ (t, caddr (x), a))

then iplus-list (eval$ ('list, delete (caddr (x), iplus-fringe (cadr (x))), a))

     = 0

else f endif elseif listp (caddr (x))

∧ (caaddr (x) = 'iplus)

∧ (cadr (x) ∈ iplus-fringe (caddr (x))) then if integerp (eval$ (t, cadr (x), a))

then 0 = iplus-list (eval$ ('list,

delete (cadr (x),

iplus-fringe (caddr (x))), a))

else f endif else eval$ (t, x, a) endif

else eval$ (t, x, a) endif

Event: Disable cancel-iplus.

Theorem: eval$-iplus-list-delete (z ∈ y) → (iplus-list (eval$ ('list, delete (z, y), a))

= idifference (iplus-list (eval$ ('list, y, a)), eval$ (t, z, a)))

Theorem: eval$-iplus-list-bagdiff subbagp (x, y) → (iplus-list (eval$ ('list, bagdiff (y, x), a))

= idifference (iplus-list (eval$ ('list, y, a)), iplus-list (eval$ ('list, x, a))))

Theorem: iplus-list-append iplus-list (append (x, y)) = iplus (iplus-list (x), iplus-list (y))

Event: Disable iplus-tree.

;; because we want to use EVAL$-IPLUS-TREE for now

Theorem: not-integerp-implies-not-equal-iplus (¬ integerp (a)) → ((a = iplus (b, c)) = f)

Theorem: iplus-list-eval$-fringe iplus-list (eval$ ('list, iplus-fringe (x), a)) = fix-int (eval$ (t, x, a))

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

Theorem: iplus-ineg5-lemma-1 integerp (x) → ((x = iplus (y, iplus (ineg (z), w)))

= (x = iplus (ineg (z), iplus (y, w))))

Theorem: iplus-ineg5-lemma-2 (integerp (x) ∧ integerp (v)) → ((x = iplus (ineg (z), v)) = (iplus (x, z) = v))

Theorem: iplus-ineg5 integerp (x) → ((x = iplus (y, iplus (ineg (z), w))) = (iplus (x, z) = iplus (y, w)))

Event: Disable iplus-ineg5-lemma-1.

Event: Disable iplus-ineg5-lemma-2.

Theorem: iplus-ineg6 integerp (x) → ((x = iplus (y, iplus (w, ineg (z)))) = (iplus (x, z) = iplus (y, w)))

Theorem: eval$-iplus (listp (x) ∧ (car (x) = 'iplus)) → (eval$ (t, x, a) = iplus (eval$ (t, cadr (x), a), eval$ (t, caddr (x), a)))

Theorem: iplus-ineg7 (0 = iplus (x, ineg (y))) = (fix-int (y) = fix-int (x))

Theorem: correctness-of-cancel-iplus eval$ (t, x, a) = eval$ (t, cancel-iplus (x), a)

Event: Disable iplus-ineg5.

Event: 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.

Theorem: ilessp-fix-int-1 ilessp (fix-int (x), y) = ilessp (x, y)

Theorem: ilessp-fix-int-2 ilessp (x, fix-int (y)) = ilessp (x, y)

;; 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.

Definition: make-cancel-iplus-inequality-1 (x, y)

= list ('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))
|#

Definition: cancel-iplus-ilessp-1 (x) = if listp (x)

then if car (x) = 'ilessp

then make-cancel-iplus-inequality-1 (iplus-fringe (cadr (x)),

iplus-fringe (caddr (x)))

else x endif else x endif

;; 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.

Theorem: lessp-difference-plus-arg1 (w < ((w + y) − x)) = (x < y)

Theorem: lessp-difference-plus-arg1-commuted (w < ((y + w) − x)) = (x < y)

Theorem: iplus-cancellation-1-for-ilessp ilessp (iplus (a, b), iplus (a, c)) = ilessp (b, c)

Theorem: iplus-cancellation-2-for-ilessp ilessp (iplus (b, a), iplus (c, a)) = ilessp (b, c)

Theorem: correctness-of-cancel-iplus-ilessp-lemma eval$ (t, x, a) = eval$ (t, cancel-iplus-ilessp-1 (x), a)

Definition: iplus-tree-no-fix-int (l) = if listp (l) then iplus-tree-rec (l)

else ''0 endif

Theorem: eval$-ilessp-iplus-tree-no-fix-int 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))

Event: Disable iplus-tree-no-fix-int.

Theorem: make-cancel-iplus-inequality-simplifier eval$ (t, make-cancel-iplus-inequality-1 (x, y), a) = eval$ (t,

         list ('ilessp,

iplus-tree-no-fix-int (bagdiff (x, bagint (x, y))), iplus-tree-no-fix-int (bagdiff (y, bagint (x, y)))),

a)

#| 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.

Definition: cancel-iplus-ilessp (x) = if listp (x)

then if car (x) = 'ilessp

then if listp (bagint (iplus-fringe (cadr (x)),

iplus-fringe (caddr (x))))

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

else x endif else x endif

else x endif

Event: Disable make-cancel-iplus-inequality-1.

Theorem: correctness-of-cancel-iplus-ilessp eval$ (t, x, a) = eval$ (t, cancel-iplus-ilessp (x), a)

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

Theorem: itimes-zero1 (fix-int (x) = 0) → (itimes (x, y) = 0)

Theorem: itimes-0-left itimes (0, y) = 0

;; I don't want the backchaining to slow down the prover.

Event: Disable itimes-zero1.

Theorem: itimes-zero2 (fix-int (y) = 0) → (itimes (x, y) = 0)

Theorem: itimes-0-right itimes (x, 0) = 0

;; I don't want the backchaining to slow down the prover.

Event: Disable itimes-zero2.

Theorem: itimes-fix-int1 itimes (fix-int (a), b) = itimes (a, b)

Theorem: itimes-fix-int2 itimes (a, fix-int (b)) = itimes (a, b)

Theorem: commutativity-of-itimes itimes (x, y) = itimes (y, x)

Theorem: itimes-distributes-over-iplus-proof itimes (x, iplus (y, z)) = iplus (itimes (x, y), itimes (x, z))

Theorem: itimes-distributes-over-iplus (itimes (x, iplus (y, z)) = iplus (itimes (x, y), itimes (x, z))) ∧ (itimes (iplus (x, y), z) = iplus (itimes (x, z), itimes (y, z)))

Theorem: commutativity2-of-itimes itimes (x, itimes (y, z)) = itimes (y, itimes (x, z))

Theorem: associativity-of-itimes itimes (itimes (x, y), z) = itimes (x, itimes (y, z))

Theorem: equal-itimes-0 (itimes (x, y) = 0) = ((fix-int (x) = 0) ∨ (fix-int (y) = 0))

Theorem: equal-itimes-1 (itimes (a, b) = 1) = (((a = 1) ∧ (b = 1)) ∨ ((a = -1) ∧ (b = -1)))

Theorem: equal-itimes-minus-1 (itimes (a, b) = -1) = (((a = -1) ∧ (b = 1)) ∨ ((a = 1) ∧ (b = -1)))

Theorem: itimes-1-arg1 itimes (1, x) = fix-int (x)

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

Theorem: quotient-remainder-uniqueness ((a = (r + (b ∗ q))) ∧ (r < b)) → ((fix (r) = (a mod b)) ∧ (fix (q) = (a ÷ b)))

; 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.

Theorem: division-theorem-part1 integerp (i) → (iplus (iremainder (i, j ), itimes (j , iquotient (i, j ))) = i)

Theorem: division-theorem-part2 (integerp (j ) ∧ (j ≠ 0)) → (¬ ilessp (iremainder (i, j ), 0))

Theorem: division-theorem-part3 (integerp (j ) ∧ (j ≠ 0)) → ilessp (iremainder (i, j ), iabs (j ))

Theorem: division-theorem (integerp (i) ∧ integerp (j ) ∧ (j ≠ 0)) → ((iplus (iremainder (i, j ), itimes (j , iquotient (i, j ))) = i)

∧ (¬ ilessp (iremainder (i, j ), 0)) ∧ ilessp (iremainder (i, j ), iabs (j )))

Theorem: quotient-difference-lessp-arg2 (((a mod c) = 0) ∧ (b < c)) → (((a − b) ÷ c)

= if b ≃ 0 then a ÷ c elseif b < a then (a ÷ c) − (1 + (b ÷ c)) else 0 endif)

Theorem: iquotient-iremainder-uniqueness (integerp (i) ∧ integerp (j ) ∧ integerp (r) ∧ integerp (q) ∧ (j ≠ 0) ∧ (i = iplus (r, itimes (j , q)))

∧ (¬ ilessp (r, 0)) ∧ ilessp (r, iabs (j ))) → ((r = iremainder (i, j )) ∧ (q = iquotient (i, j )))

; 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.

Theorem: division-theorem-for-truncate-to-neginf-part1 integerp (i) → (iplus (imod (i, j ), itimes (j , idiv (i, j ))) = i)

Theorem: division-theorem-for-truncate-to-neginf-part2 ilessp (0, j ) → ((¬ ilessp (imod (i, j ), 0)) ∧ ilessp (imod (i, j ), j ))

Theorem: division-theorem-for-truncate-to-neginf-part3 (integerp (j ) ∧ ilessp (j , 0)) → ((¬ ilessp (0, imod (i, j ))) ∧ ilessp (j , imod (i, j )))

Theorem: division-theorem-for-truncate-to-neginf (integerp (i) ∧ integerp (j ) ∧ (j ≠ 0)) → ((iplus (imod (i, j ), itimes (j , idiv (i, j ))) = i)

∧ if ilessp (0, j ) then (¬ ilessp (imod (i, j ), 0)) ∧ ilessp (imod (i, j ), j ) else (¬ ilessp (0, imod (i, j )))

∧ ilessp (j , imod (i, j )) endif)

Theorem: idiv-imod-uniqueness (integerp (i) ∧ integerp (j ) ∧ integerp (r)

∧ integerp (q) ∧ (j ≠ 0) ∧ (i = iplus (r, itimes (j , q))) ∧ if ilessp (0, j ) then (¬ ilessp (r, 0)) ∧ ilessp (r, j )

else (¬ ilessp (0, r)) ∧ ilessp (j , r) endif) → ((r = imod (i, j )) ∧ (q = idiv (i, j )))

; 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.

Theorem: division-theorem-for-truncate-to-zero-part1 integerp (i) → (iplus (irem (i, j ), itimes (j , iquo (i, j ))) = i)

Theorem: division-theorem-for-truncate-to-zero-part2 (integerp (i) ∧ integerp (j ) ∧ (j ≠ 0) ∧ (¬ ilessp (i, 0))) → ((¬ ilessp (irem (i, j ), 0)) ∧ ilessp (irem (i, j ), iabs (j )))

Theorem: division-theorem-for-truncate-to-zero-part3 (integerp (i) ∧ integerp (j ) ∧ (j ≠ 0) ∧ ilessp (i, 0)) → ((¬ ilessp (0, irem (i, j ))) ∧ ilessp (ineg (iabs (j )), irem (i, j )))

Theorem: division-theorem-for-truncate-to-zero (integerp (i) ∧ integerp (j ) ∧ (j ≠ 0)) → ((iplus (irem (i, j ), itimes (j , iquo (i, j ))) = i)

∧ if ¬ ilessp (i, 0)

then (¬ ilessp (irem (i, j ), 0))

∧ ilessp (irem (i, j ), iabs (j )) else (¬ ilessp (0, irem (i, j )))

∧ ilessp (ineg (iabs (j )), irem (i, j )) endif)

Theorem: iquo-irem-uniqueness (integerp (i) ∧ integerp (j )

∧ integerp (r) ∧ integerp (q) ∧ (j ≠ 0) ∧ (i = iplus (r, itimes (j , q))) ∧ if ¬ ilessp (i, 0) then (¬ ilessp (r, 0)) ∧ ilessp (r, iabs (j ))

else (¬ ilessp (0, r)) ∧ ilessp (ineg (iabs (j )), r) endif) → ((r = irem (i, j )) ∧ (q = iquo (i, j )))

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

Theorem: itimes-ineg-1 itimes (ineg (x), y) = ineg (itimes (x, y))

Theorem: itimes-ineg-2 itimes (x, ineg (y)) = ineg (itimes (x, y))

Theorem: itimes-cancellation-1 (itimes (a, b) = itimes (a, c)) = ((fix-int (a) = 0) ∨ (fix-int (b) = fix-int (c)))

Theorem: itimes-cancellation-2 (itimes (b, a) = itimes (c, a)) = ((fix-int (a) = 0) ∨ (fix-int (b) = fix-int (c)))

Theorem: itimes-cancellation-3 (itimes (a, b) = itimes (c, a)) = ((fix-int (a) = 0) ∨ (fix-int (b) = fix-int (c)))

; ---------- Division Facts

Theorem: integerp-iquotient integerp (iquotient (i, j ))

Theorem: integerp-iremainder integerp (iremainder (i, j ))

Theorem: integerp-idiv integerp (idiv (i, j ))

Theorem: integerp-imod integerp (imod (i, j ))

Theorem: integerp-iquo integerp (iquo (i, j ))

Theorem: integerp-irem integerp (irem (i, j ))

Theorem: iquotient-fix-int1 iquotient (fix-int (i), j ) = iquotient (i, j )

Theorem: iquotient-fix-int2 iquotient (i, fix-int (j )) = iquotient (i, j )

Theorem: iremainder-fix-int1 iremainder (fix-int (i), j ) = iremainder (i, j )

Theorem: iremainder-fix-int2 iremainder (i, fix-int (j )) = iremainder (i, j )

Theorem: idiv-fix-int1 idiv (fix-int (i), j ) = idiv (i, j )

Theorem: idiv-fix-int2 idiv (i, fix-int (j )) = idiv (i, j )

Theorem: imod-fix-int1 imod (fix-int (i), j ) = imod (i, j )

Theorem: imod-fix-int2 imod (i, fix-int (j )) = imod (i, j )

Theorem: iquo-fix-int1 iquo (fix-int (i), j ) = iquo (i, j )

Theorem: iquo-fix-int2 iquo (i, fix-int (j )) = iquo (i, j )

Theorem: irem-fix-int1 irem (fix-int (i), j ) = irem (i, j )

Theorem: irem-fix-int2 irem (i, fix-int (j )) = irem (i, j )

Theorem: fix-int-iquotient fix-int (iquotient (i, j )) = iquotient (i, j )

Theorem: fix-int-iremainder fix-int (iremainder (i, j )) = iremainder (i, j )

Theorem: fix-int-idiv fix-int (idiv (i, j )) = idiv (i, j )

Theorem: fix-int-imod fix-int (imod (i, j )) = imod (i, j )

Theorem: fix-int-iquo fix-int (iquo (i, j )) = iquo (i, j )

Theorem: fix-int-irem fix-int (irem (i, j )) = irem (i, j )

Event: Disable iquotient.

Event: Disable iremainder.

Event: Disable idiv.

Event: Disable imod.

Event: Disable iquo.

Event: Disable irem.

; ---------- Meta lemma for itimes cancellation
;; I tried to adapt this somewhat from corresponding meta lemmas in
;; naturals library, but it seemed to get hairy.  So instead I'll try
;; to parallel the development I gave for IPLUS.  I'll be lazier here
;; about efficiency, so I'll use a completely analogous definition of
;; itimes-tree.  Notice that I've avoided the IZEROP-TREE approach
;; from the naturals version, in that I simply create the appropriate
;; common fringe into a product and say that this product is non-zero
;; when dividing both sides by it.  It can then be up to the user whether
;; or not to enable the (meta or rewrite) rule that says that izerop of a product reduces
;; to the disjunction of izerop of the factors.
#| The function below has no AND or OR, for efficiency
(defn itimes-fringe (x)
  (if (and (listp x)
           (equal (car x)
                  (quote itimes)))
      (append (itimes-fringe (cadr x))
              (itimes-fringe (caddr x)))

      (cons x nil)))
|#

Definition: itimes-fringe (x) = if listp (x)

then if car (x) = 'itimes then append (itimes-fringe (cadr (x)), itimes-fringe (caddr (x))) else list (x) endif

else list (x) endif

Definition: itimes-tree-rec (l) = if cdr (l) ≃ nil then car (l)

else list ('itimes, car (l), itimes-tree-rec (cdr (l))) endif

Definition: itimes-tree (l) = if listp (l)

then if listp (cdr (l)) then itimes-tree-rec (l) else list ('fix-int, car (l)) endif

else ''1 endif

Definition: itimes-list (x) = if listp (x) then itimes (car (x), itimes-list (cdr (x)))

else 1 endif

Theorem: integerp-itimes-list integerp (itimes-list (x))

Theorem: eval$-itimes-tree-rec listp (x) → (eval$ (t, itimes-tree-rec (x), a)

= if listp (cdr (x)) then itimes-list (eval$ ('list, x, a)) else eval$ (t, car (x), a) endif)

;; The following allows us to pretty much ignore itimes-tree forever.  (Notice
;; that it is disabled immediately below.)

Theorem: eval$-itimes-tree eval$ (t, itimes-tree (x), a) = itimes-list (eval$ ('list, x, a))

Event: Disable itimes-tree.

;; because we want to use EVAL$-ITIMES-TREE for now

Definition: make-cancel-itimes-equality (x, y, in-both) = list ('if,

list ('equal, itimes-tree (in-both), ''0), list ('quote, t),

       list ('equal,

itimes-tree (bagdiff (x, in-both)), itimes-tree (bagdiff (y, in-both))))

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

                             (list (cadr x)))
(list (quote quote) f))
x)
x)))
x))
|#

Definition: cancel-itimes (x) = if listp (x)

then if car (x) = 'equal

then if listp (cadr (x))

then if caadr (x) = 'itimes

then if listp (caddr (x))

then if caaddr (x) = 'itimes

then if listp (bagint (itimes-fringe (cadr (x)),

itimes-fringe (caddr (x)))) then make-cancel-itimes-equality (itimes-fringe (cadr (x)),

itimes-fringe (caddr (x)),

bagint (itimes-fringe (cadr (x)),

itimes-fringe (caddr (x))))

else x endif elseif caddr (x) ∈ itimes-fringe (cadr (x)) then list ('if,

list ('integerp, caddr (x)),

make-cancel-itimes-equality (itimes-fringe (cadr (x)), list (caddr (x)), list (caddr (x))),

list ('quote, f))

else x endif elseif caddr (x) ∈ itimes-fringe (cadr (x)) then list ('if,

list ('integerp, caddr (x)),

make-cancel-itimes-equality (itimes-fringe (cadr (x)), list (caddr (x)), list (caddr (x))),

list ('quote, f))

else x endif elseif listp (caddr (x)) then if caaddr (x) = 'itimes

then if cadr (x) ∈ itimes-fringe (caddr (x))

then list ('if, list ('integerp, cadr (x)), make-cancel-itimes-equality (list (cadr (x)),

itimes-fringe (caddr (x)), list (cadr (x))),

list ('quote, f))

else x endif else x endif

else x endif elseif listp (caddr (x)) then if caaddr (x) = 'itimes

then if cadr (x) ∈ itimes-fringe (caddr (x))

then list ('if, list ('integerp, cadr (x)), make-cancel-itimes-equality (list (cadr (x)),

itimes-fringe (caddr (x)), list (cadr (x))),

list ('quote, f))

else x endif else x endif

else x endif else x endif

else x endif

Theorem: itimes-list-append itimes-list (append (x, y)) = itimes (itimes-list (x), itimes-list (y))

Theorem: itimes-list-eval$-fringe itimes-list (eval$ ('list, itimes-fringe (x), a)) = fix-int (eval$ (t, x, a))

Theorem: integerp-eval$-itimes (car (x) = 'itimes) → integerp (eval$ (t, x, a))

Theorem: not-integerp-implies-not-equal-itimes (¬ integerp (a)) → ((a = itimes (b, c)) = f)

Theorem: itimes-list-eval$-delete (z ∈ y) → (itimes-list (eval$ ('list, y, a))

= itimes (eval$ (t, z, a), itimes-list (eval$ ('list, delete (z, y), a))))

Theorem: itimes-list-bagdiff subbagp (x, y) → (itimes-list (eval$ ('list, y, a))

= itimes (itimes-list (eval$ ('list, bagdiff (y, x), a)), itimes-list (eval$ ('list, x, a))))

Theorem: equal-itimes-list-eval$-list-delete ((c ∈ y) ∧ (fix-int (eval$ (t, c, a)) ≠ 0)) → ((x = itimes-list (eval$ ('list, delete (c, y), a)))

= (integerp (x)

∧ (itimes (x, eval$ (t, c, a)) = itimes-list (eval$ ('list, y, a)))))

Event: Disable itimes-list-eval$-delete.

;; I had trouble with the clausifier (thanks, J, for pointing that out
;; as the source of my trouble) in the proof of the meta lemma -- it's
;; getting rid of a case split.  So, I'll proceed by reducing
;; cancel-itimes in each case; see lemma eval$-make-cancel-itimes-equality
;; (and its -1 and -2 versions).

Theorem: member-append (a ∈ append (x, y)) = ((a ∈ x) ∨ (a ∈ y))

Theorem: member-izerop-itimes-fringe ((z ∈ itimes-fringe (x)) ∧ (fix-int (eval$ (t, z, a)) = 0)) → (fix-int (eval$ (t, x, a)) = 0)

Theorem: correctness-of-cancel-itimes-hack-1 ((w ∈ itimes-fringe (cons ('itimes, x1 ))) ∧ (fix-int (eval$ (t, w, a)) = 0) ∧ (fix-int (eval$ (t, car (x1 ), a)) ≠ 0)) → (fix-int (eval$ (t, cadr (x1 ), a)) = 0)

Event: Enable eval$-equal.

Theorem: eval$-make-cancel-itimes-equality eval$ (t, make-cancel-itimes-equality (x, y, in-both), a) = if eval$ (t, list ('equal, itimes-tree (in-both), ''0), a) then t

else itimes-list (eval$ ('list, bagdiff (x, in-both), a)) = itimes-list (eval$ ('list, bagdiff (y, in-both), a)) endif

Event: Disable make-cancel-itimes-equality.

;; Here's a special case that I hope helps with the clausifier problem.
;; The lemma above seems necessary for its proof.

Theorem: eval$-make-cancel-itimes-equality-1 eval$ (t, make-cancel-itimes-equality (list (x), y, list (x)), a) = if fix-int (eval$ (t, x, a)) = 0 then t

else 1 = itimes-list (eval$ ('list, delete (x, y), a)) endif

Theorem: equal-fix-int (fix-int (x) = x) = integerp (x)

;; Here's another special case that I hope helps with the clausifier problem.

Theorem: eval$-make-cancel-itimes-equality-2 eval$ (t, make-cancel-itimes-equality (x, list (y), list (y)), a) = if fix-int (eval$ (t, y, a)) = 0 then t

else 1 = itimes-list (eval$ ('list, delete (y, x), a)) endif

Theorem: eval$-equal-itimes-tree-itimes-fringe-0 (eval$ (t, list ('equal, itimes-tree (itimes-fringe (x)), ''0), a) ∧ (car (x) = 'itimes)) → (eval$ (t, x, a) = 0)

Theorem: izerop-eval-of-member-implies-itimes-list-0 ((z ∈ y) ∧ (fix-int (eval$ (t, z, a)) = 0)) → (itimes-list (eval$ ('list, y, a)) = 0)

#| The function below has no AND or OR, for efficiency
(defn subsetp (x y)
  (if (nlistp x)
      t
    (and (member (car x) y)
         (subsetp (cdr x) y))))
|#

Definition: subsetp (x, y) = if x ≃ nil then t

elseif car (x) ∈ y then subsetp (cdr (x), y)

else f endif

Theorem: subsetp-implies-itimes-list-eval$-equals-0 (subsetp (x, y) ∧ (itimes-list (eval$ ('list, x, a)) = 0)) → (itimes-list (eval$ ('list, y, a)) = 0)

Theorem: subbagp-subsetp subbagp (x, y) → subsetp (x, y)

Theorem: equal-0-itimes-list-eval$-bagint-1 (itimes-list (eval$ ('list, bagint (x, y), a)) = 0) → (itimes-list (eval$ ('list, x, a)) = 0)

Theorem: equal-0-itimes-list-eval$-bagint-2 (itimes-list (eval$ ('list, bagint (x, y), a)) = 0) → (itimes-list (eval$ ('list, y, a)) = 0)

Theorem: correctness-of-cancel-itimes-hack-2 (listp (u) ∧ (car (u) = 'itimes) ∧ listp (v) ∧ (car (v) = 'itimes) ∧ (eval$ (t, u, a) ≠ eval$ (t, v, a))) → (itimes-list (eval$ ('list,

bagdiff (itimes-fringe (u),

bagint (itimes-fringe (u), itimes-fringe (v))), a))

≠ itimes-list (eval$ ('list,

bagdiff (itimes-fringe (v),

bagint (itimes-fringe (u),

itimes-fringe (v))),

a)))

Theorem: correctness-of-cancel-itimes-hack-3-lemma ((u = itimes (a, b)) ∧ (fix-int (a) ≠ 0)) → ((u = itimes (a, c)) = (fix-int (b) = fix-int (c)))

Theorem: correctness-of-cancel-itimes-hack-3 (listp (u) ∧ (car (u) = 'itimes) ∧ listp (v) ∧ (car (v) = 'itimes) ∧ (eval$ (t, u, a) = eval$ (t, v, a)) ∧ (¬ eval$ (t,

            list ('equal,

itimes-tree (bagint (itimes-fringe (u), itimes-fringe (v))),

                ''0),

a)))

→ ((itimes-list (eval$ ('list,

bagdiff (itimes-fringe (u),

bagint (itimes-fringe (u), itimes-fringe (v))), a))

= itimes-list (eval$ ('list, bagdiff (itimes-fringe (v), bagint (itimes-fringe (u),

itimes-fringe (v))),

a)))

= t)

Event: Disable correctness-of-cancel-itimes-hack-3-lemma.

Theorem: correctness-of-cancel-itimes eval$ (t, x, a) = eval$ (t, cancel-itimes (x), a)

; ---------- Meta lemma for itimes cancellation on ilessp terms
;; I'll try to keep this similar to the approach for equalities above,
;; modified as in the iplus case (i.e. no fix-int is necessary).
;; EVAL$-EQUAL is currently enabled, but that's OK.

Definition: itimes-tree-no-fix-int (l) = if listp (l) then itimes-tree-rec (l)

else ''1 endif

;; The following allows us to pretty much ignore
;; itimes-tree-no-fix-int forever.  (Notice that it is disabled
;; immediately below.)

Theorem: eval$-itimes-tree-no-fix-int-1 ilessp (eval$ (t, itimes-tree-no-fix-int (x), a), y) = ilessp (eval$ (t, itimes-tree (x), a), y)

Theorem: eval$-itimes-tree-no-fix-int-2 ilessp (y, eval$ (t, itimes-tree-no-fix-int (x), a)) = ilessp (y, eval$ (t, itimes-tree (x), a))

Event: Disable itimes-tree-no-fix-int.

;; We want to use EVAL$-ITIMES-TREE, and ITIMES-TREE is still disabled
;; so we're in good shape.

Definition: make-cancel-itimes-inequality (x, y, in-both)

= list ('if, list ('ilessp, itimes-tree-no-fix-int (in-both), ''0),

       list ('ilessp,

itimes-tree-no-fix-int (bagdiff (y, in-both)), itimes-tree-no-fix-int (bagdiff (x, in-both))),

list ('if, list ('ilessp, ''0, itimes-tree-no-fix-int (in-both)),

           list ('ilessp,

itimes-tree-no-fix-int (bagdiff (x, in-both)), itimes-tree-no-fix-int (bagdiff (y, in-both))),

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

Definition: cancel-itimes-ilessp (x) = if listp (x)

then if car (x) = 'ilessp

then if listp (bagint (itimes-fringe (cadr (x)),

itimes-fringe (caddr (x)))) then make-cancel-itimes-inequality (itimes-fringe (cadr (x)),

itimes-fringe (caddr (x)),

bagint (itimes-fringe (cadr (x)),

itimes-fringe (caddr (x))))

else x endif else x endif

else x endif

Theorem: eval$-make-cancel-itimes-inequality eval$ (t, make-cancel-itimes-inequality (x, y, in-both), a) = if eval$ (t, list ('ilessp, itimes-tree-no-fix-int (in-both), ''0), a)

then ilessp (eval$ (t, itimes-tree-no-fix-int (bagdiff (y, in-both)), a),

eval$ (t, itimes-tree-no-fix-int (bagdiff (x, in-both)), a))

elseif eval$ (t, list ('ilessp, ''0, itimes-tree-no-fix-int (in-both)), a) then ilessp (eval$ (t, itimes-tree-no-fix-int (bagdiff (x, in-both)), a),

eval$ (t, itimes-tree-no-fix-int (bagdiff (y, in-both)), a))

else f endif

Event: Disable make-cancel-itimes-inequality.

Theorem: listp-bagint-with-singleton-implies-member listp (bagint (y, list (z))) → (z ∈ y)

Theorem: itimes-list-eval$-list-0 (0 ∈ x) → (itimes-list (eval$ ('list, x, a)) = 0)

Theorem: ilessp-itimes-right-positive ilessp (0, x) → (ilessp (y, z) = ilessp (itimes (y, x), itimes (z, x)))

Theorem: correctness-of-cancel-itimes-ilessp-hack-1 (subbagp (bag, x) ∧ subbagp (bag, y) ∧ ilessp (0, itimes-list (eval$ ('list, bag, a)))) → (ilessp (itimes-list (eval$ ('list, bagdiff (x, bag), a)),

itimes-list (eval$ ('list, bagdiff (y, bag), a))) = ilessp (itimes-list (eval$ ('list, x, a)),

itimes-list (eval$ ('list, y, a))))

Theorem: listp-bagint-with-singleton-member listp (bagint (y, list (z))) = (z ∈ y)

Theorem: correctness-of-cancel-itimes-ilessp-hack-2-lemma (0 ∈ itimes-fringe (w)) → (eval$ (t, w, a) = 0)

Theorem: correctness-of-cancel-itimes-ilessp-hack-2 (0 ∈ itimes-fringe (w)) → (¬ ilessp (eval$ (t, w, a), 0))

Event: Disable correctness-of-cancel-itimes-ilessp-hack-2-lemma.

;;; Now hack-3 and hack-4 below are all that's left to prove before the
;;; main result.

Theorem: ilessp-trichotomy (¬ ilessp (x, y)) → (ilessp (y, x) = (fix-int (x) ≠ fix-int (y)))

Theorem: correctness-of-cancel-itimes-ilessp-hack-3-lemma-1 ((0 = itimes-list (eval$ ('list, bag, a))) ∧ subsetp (bag, z)) → (itimes-list (eval$ ('list, z, a)) = 0)

Theorem: correctness-of-cancel-itimes-ilessp-hack-3-lemma-2 ((0 = itimes-list (eval$ ('list, bag, a))) ∧ subsetp (bag, itimes-fringe (x))) → (fix-int (eval$ (t, x, a)) = 0)

Theorem: same-fix-int-implies-not-ilessp (fix-int (x) = fix-int (y)) → (¬ ilessp (x, y))

Theorem: correctness-of-cancel-itimes-ilessp-hack-3 ((¬ ilessp (itimes-list (eval$ ('list, bag, a)), 0)) ∧ (¬ ilessp (0, itimes-list (eval$ ('list, bag, a)))) ∧ subbagp (bag, itimes-fringe (w)) ∧ subbagp (bag, itimes-fringe (v))) → (¬ ilessp (eval$ (t, w, a), eval$ (t, v, a)))

Theorem: ilessp-itimes-right-negative ilessp (x, 0) → (ilessp (y, z) = ilessp (itimes (z, x), itimes (y, x)))

Theorem: correctness-of-cancel-itimes-ilessp-hack-4 (subbagp (bag, x) ∧ subbagp (bag, y) ∧ ilessp (itimes-list (eval$ ('list, bag, a)), 0)) → (ilessp (itimes-list (eval$ ('list, bagdiff (x, bag), a)),

itimes-list (eval$ ('list, bagdiff (y, bag), a))) = ilessp (itimes-list (eval$ ('list, y, a)),

itimes-list (eval$ ('list, x, a))))

Event: Disable ilessp-trichotomy.

Event: Disable same-fix-int-implies-not-ilessp.

Theorem: correctness-of-cancel-itimes-ilessp eval$ (t, x, a) = eval$ (t, cancel-itimes-ilessp (x), a)

;; I think that the following lemma is safe because it won't be
;; called at all during relieve-hyps.

Theorem: ilessp-strict ilessp (x, y) → (¬ ilessp (y, x))

; ---------- Setting up the State ----------
;; I'll close by disabling (or enabling) those rules and definitions
;; whose status as left over from above isn't quite what I'd like.
;; I'm going to leave the eval$ rules on and eval$ off.

Event: Disable eval$-cancel-iplus. Event: Disable eval$-iplus. Event: Disable lessp-count-listp-cdr. Event: Disable eval$-iplus-tree-rec. Event: Disable eval$-iplus-tree.

;;(disable eval$-list-append) ;; Nice rule -- I'll keep it enabled

Event: Disable iplus-list-eval$-fringe. Event: Disable eval$-iplus-list-bagdiff. Event: Disable lessp-difference-plus-arg1. Event: Disable lessp-difference-plus-arg1-commuted. Event: Disable correctness-of-cancel-iplus-ilessp-lemma. Event: Disable eval$-ilessp-iplus-tree-no-fix-int. Event: Disable make-cancel-iplus-inequality-simplifier. Event: Disable quotient-difference-lessp-arg2. Event: Disable eval$-itimes-tree-rec. Event: Disable eval$-itimes-tree. Event: Disable itimes-list-eval$-fringe. Event: Disable integerp-eval$-itimes.

Event: Disable itimes-list-bagdiff. Event: Disable equal-itimes-list-eval$-list-delete. Event: Disable member-izerop-itimes-fringe. Event: Disable correctness-of-cancel-itimes-hack-1. Event: Disable eval$-make-cancel-itimes-equality. Event: Disable eval$-make-cancel-itimes-equality-1. Event: Disable eval$-make-cancel-itimes-equality-2. Event: Disable eval$-equal-itimes-tree-itimes-fringe-0. Event: Disable izerop-eval-of-member-implies-itimes-list-0. Event: Disable subsetp-implies-itimes-list-eval$-equals-0. Event: Disable equal-0-itimes-list-eval$-bagint-1. Event: Disable equal-0-itimes-list-eval$-bagint-2. Event: Disable correctness-of-cancel-itimes-hack-2. Event: Disable correctness-of-cancel-itimes-hack-3-lemma. Event: Disable correctness-of-cancel-itimes-hack-3. Event: Disable eval$-itimes-tree-no-fix-int-1. Event: Disable eval$-itimes-tree-no-fix-int-2. Event: Disable eval$-make-cancel-itimes-inequality.

Event: Disable listp-bagint-with-singleton-implies-member.

Event: Disable itimes-list-eval$-list-0.

Event: Disable correctness-of-cancel-itimes-ilessp-hack-1.

Event: Disable listp-bagint-with-singleton-member.

Event: Disable correctness-of-cancel-itimes-ilessp-hack-2.

Event: Disable correctness-of-cancel-itimes-ilessp-hack-3-lemma-1.

Event: Disable correctness-of-cancel-itimes-ilessp-hack-3-lemma-2.

Event: Disable correctness-of-cancel-itimes-ilessp-hack-3.

Event: Disable correctness-of-cancel-itimes-ilessp-hack-4.

;; The last one is a tough call, but I think it's OK.
;; (disable ilessp-strict)
;;;;;; ***** EXTRA META STUFF ***** ;;;;;;
;; The next goal is to improve itimes cancellation so that it looks
;; for common factors, and hence works on equations like
;;    x*y + x = x*z
;; and, for that matter,
;; a*x + -b*x = 0.
;; Rather than changing the existing cancel-itimes function, I'll
;; leave that one but disable its metalemma at the end.  Then if the
;; new version, which I'll call cancel-itimes-factors, is found to be
;; too slow, one can always disable its metalemma and re-enable the
;; metalemma for cancel-itimes.
;; Notice, by the way, that the existing cancel-itimes function is
;; useless for something like the following, since there's no special
;; treatment for INEG.  I'll remedy that in this version.

#|
(IMPLIES (AND (NOT (IZEROP X))
              (EQUAL (ITIMES A X) (INEG (ITIMES B X))))
         (EQUAL (FIX-INT A) (INEG B)))
|#

Definition: itimes-tree-ineg (l) = if listp (l)

then if car (l) = list ('quote, -1)

then if listp (cdr (l)) then list ('ineg, itimes-tree-rec (cdr (l)))

else car (l) endif else itimes-tree-rec (l) endif

else ''1 endif

Definition: itimes-factors (x) = if listp (x)

then if car (x) = 'itimes then append (itimes-factors (cadr (x)), itimes-factors (caddr (x))) elseif car (x) = 'iplus then let bag1 be itimes-factors (cadr (x)),

bag2 be itimes-factors (caddr (x)) in let inboth be bagint (bag1 , bag2 ) in if listp (inboth) then cons (list ('iplus,

itimes-tree-ineg (bagdiff (bag1 ,

inboth)),

itimes-tree-ineg (bagdiff (bag2 ,

inboth))),

inboth) else list (x) endif endlet endlet

elseif car (x) = 'ineg

then cons (list ('quote, -1), itimes-factors (cadr (x)))

else list (x) endif else list (x) endif

Theorem: itimes–1 itimes (-1, x) = ineg (x)

;; I'll need the following lemma because it's simplest not to deal with
;; e.g. (equal x x), where x is a variable, in the meta thing.  I'll do
;; the one after it too, simply because I'm thinking of it now.

Theorem: equal-ineg-ineg (ineg (x) = ineg (y)) = (fix-int (x) = fix-int (y))

Theorem: ilessp-ineg-ineg ilessp (ineg (x), ineg (y)) = ilessp (y, x)

Theorem: fix-int-eval$-itimes-tree-rec listp (x) → (fix-int (eval$ (t, itimes-tree-rec (x), a))

= itimes-list (eval$ ('list, x, a)))

Theorem: eval$-itimes-tree-ineg fix-int (eval$ (t, itimes-tree-ineg (x), a)) = itimes-list (eval$ ('list, x, a))

;; Now I want the above lemma to apply, but it doesn't, so the
;; following three lemmas are used instead.

Theorem: ineg-eval$-itimes-tree-ineg ineg (eval$ (t, itimes-tree-ineg (x), a)) = ineg (itimes-list (eval$ ('list, x, a)))

Theorem: iplus-eval$-itimes-tree-ineg (iplus (eval$ (t, itimes-tree-ineg (x), a), y) = iplus (itimes-list (eval$ ('list, x, a)), y)) ∧ (iplus (y, eval$ (t, itimes-tree-ineg (x), a))

= iplus (y, itimes-list (eval$ ('list, x, a))))

Theorem: itimes-eval$-itimes-tree-ineg (itimes (eval$ (t, itimes-tree-ineg (x), a), y) = itimes (itimes-list (eval$ ('list, x, a)), y)) ∧ (itimes (y, eval$ (t, itimes-tree-ineg (x), a))

= itimes (y, itimes-list (eval$ ('list, x, a))))

Event: Disable itimes-tree-ineg.

#| ****** The following definitions are for efficient execution of
   metafunctions.  They should probably be applied to all the metafunctions
   with fns arguments AND and OR.
(defmacro nqthm-macroexpand (defn &rest fns)
  `(nqthm-macroexpand-fn ',defn ',fns))
(defun nqthm-macroexpand-fn (defn fns)
  (iterate for fn in fns

           when (not (get fn 'sdefn))
           do (er soft (fn) |Sorry| |,| |but| |there| |is| |no| SDEFN
                  |for| (!ppr fn (quote |.|))))
  (let (name args body)
    (match! defn (defn name args body))
    (let ((arity-alist (cons (cons name (length args)) arity-alist)))
      (list 'defn name args
            (untranslate (normalize-ifs
                          (nqthm-macroexpand-term (translate body) fns)
                          nil nil nil))))))
(defun nqthm-macroexpand-term (term fns)
  (cond
   ((or (variablep term) (fquotep term))
    term)
   ((member-eq (ffn-symb term) fns)
    (let ((sdefn (get (ffn-symb term) 'sdefn)))
      (sub-pair-var (cadr sdefn)
                    (iterate for arg in (fargs term)
                             collect (nqthm-macroexpand-term arg fns))
                    (caddr sdefn))))
   (t (fcons-term (ffn-symb term)
                  (iterate for arg in (fargs term)
                           collect (nqthm-macroexpand-term arg fns))))))
|#
;; I "macroexpand" away the following below, so it's not really needed except
;; for the proof.  That is, I use it in the definition of cancel-itimes-factors,
;; but then get rid of it for cancel-itimes-factors-expanded, and although I
;; reason about the former, I USE the latter, for efficiency.

Definition: iplus-or-itimes-term (x) = if listp (x)

then case on car (x): case = iplus then t case = itimes then t case = ineg then if listp (cadr (x)) then car (cadr (x)) = 'itimes

else f endif otherwise f endcase

else f endif

Definition: cancel-itimes-factors (x) = if listp (x) ∧ (car (x) = 'equal)

then let bagint be bagint (itimes-factors (cadr (x)),

itimes-factors (caddr (x)))

in let new-equality be make-cancel-itimes-equality (itimes-factors (cadr (x)),

itimes-factors (caddr (x)), bagint)

in if iplus-or-itimes-term (cadr (x)) then if listp (bagint)

then if iplus-or-itimes-term (caddr (x)) then new-equality else list ('if,

                  list ('integerp,

caddr (x)), new-equality, list ('quote, f)) endif

else x endif elseif iplus-or-itimes-term (caddr (x)) then if listp (bagint)

then list ('if, list ('integerp, cadr (x)), new-equality, list ('quote, f))

else x endif else x endif endlet endlet

else x endif

;; The following was generated with the nqthm-macroexpand macro defined above.

;; The following was generated with the nqthm-macroexpand macro defined above.
(DEFN CANCEL-ITIMES-FACTORS-expanded (X)
(IF (LISTP X)
(IF (EQUAL (CAR X) 'EQUAL)
 (COND
  ((LISTP (CADR X))
   (CASE (CAR (CAR (CDR X)))
         (IPLUS (IF (LISTP (BAGINT (ITIMES-FACTORS (CADR X))
                                   (ITIMES-FACTORS (CADDR X))))

(IF (LISTP (CADDR X))
(CASE (CAR (CAR (CDR (CDR X))))
(IPLUS
(MAKE-CANCEL-ITIMES-EQUALITY
(ITIMES-FACTORS (CADR X))
(ITIMES-FACTORS (CADDR X))
(BAGINT (ITIMES-FACTORS (CADR X))
        (ITIMES-FACTORS (CADDR X)))))
(ITIMES
(MAKE-CANCEL-ITIMES-EQUALITY
(ITIMES-FACTORS (CADR X))
(ITIMES-FACTORS (CADDR X))
(BAGINT (ITIMES-FACTORS (CADR X))
        (ITIMES-FACTORS (CADDR X)))))
(INEG
(IF (LISTP (CADADDR X))
   (IF (EQUAL (CAADADDR X) 'ITIMES)
       (MAKE-CANCEL-ITIMES-EQUALITY
        (ITIMES-FACTORS (CADR X))
        (ITIMES-FACTORS (CADDR X))
        (BAGINT
         (ITIMES-FACTORS (CADR X))
         (ITIMES-FACTORS (CADDR X))))
       (LIST 'IF
             (LIST 'INTEGERP (CADDR X))
             (MAKE-CANCEL-ITIMES-EQUALITY
              (ITIMES-FACTORS (CADR X))
              (ITIMES-FACTORS (CADDR X))
              (BAGINT
               (ITIMES-FACTORS (CADR X))
               (ITIMES-FACTORS (CADDR X))))
             (LIST 'QUOTE F)))
   (LIST 'IF
         (LIST 'INTEGERP (CADDR X))
         (MAKE-CANCEL-ITIMES-EQUALITY
          (ITIMES-FACTORS (CADR X))
          (ITIMES-FACTORS (CADDR X))
          (BAGINT
           (ITIMES-FACTORS (CADR X))
           (ITIMES-FACTORS (CADDR X))))
         (LIST 'QUOTE F))))
(OTHERWISE
(LIST 'IF
     (LIST 'INTEGERP (CADDR X))

      (MAKE-CANCEL-ITIMES-EQUALITY
       (ITIMES-FACTORS (CADR X))
       (ITIMES-FACTORS (CADDR X))
       (BAGINT
        (ITIMES-FACTORS (CADR X))
        (ITIMES-FACTORS (CADDR X))))
      (LIST 'QUOTE F))))
(LIST 'IF (LIST 'INTEGERP (CADDR X))
(MAKE-CANCEL-ITIMES-EQUALITY
(ITIMES-FACTORS (CADR X))
(ITIMES-FACTORS (CADDR X))
(BAGINT
 (ITIMES-FACTORS (CADR X))
 (ITIMES-FACTORS (CADDR X))))
(LIST 'QUOTE F)))
X))
(ITIMES (IF (LISTP (BAGINT (ITIMES-FACTORS (CADR X))
     (ITIMES-FACTORS (CADDR X))))
(IF (LISTP (CADDR X))
(CASE (CAR (CAR (CDR (CDR X))))
(IPLUS
 (MAKE-CANCEL-ITIMES-EQUALITY
  (ITIMES-FACTORS (CADR X))
  (ITIMES-FACTORS (CADDR X))
  (BAGINT
   (ITIMES-FACTORS (CADR X))
   (ITIMES-FACTORS (CADDR X)))))
(ITIMES
 (MAKE-CANCEL-ITIMES-EQUALITY
  (ITIMES-FACTORS (CADR X))
  (ITIMES-FACTORS (CADDR X))
  (BAGINT
   (ITIMES-FACTORS (CADR X))
   (ITIMES-FACTORS (CADDR X)))))
(INEG
 (IF (LISTP (CADADDR X))
     (IF (EQUAL (CAADADDR X) 'ITIMES)
         (MAKE-CANCEL-ITIMES-EQUALITY
          (ITIMES-FACTORS (CADR X))
          (ITIMES-FACTORS (CADDR X))
          (BAGINT
           (ITIMES-FACTORS (CADR X))
           (ITIMES-FACTORS (CADDR X))))
         (LIST 'IF

              (LIST 'INTEGERP (CADDR X))
              (MAKE-CANCEL-ITIMES-EQUALITY
               (ITIMES-FACTORS (CADR X))
               (ITIMES-FACTORS (CADDR X))
               (BAGINT
                (ITIMES-FACTORS (CADR X))
                (ITIMES-FACTORS (CADDR X))))
              (LIST 'QUOTE F)))
    (LIST 'IF
          (LIST 'INTEGERP (CADDR X))
          (MAKE-CANCEL-ITIMES-EQUALITY
           (ITIMES-FACTORS (CADR X))
           (ITIMES-FACTORS (CADDR X))
           (BAGINT
            (ITIMES-FACTORS (CADR X))
            (ITIMES-FACTORS (CADDR X))))
          (LIST 'QUOTE F))))
(OTHERWISE
(LIST 'IF
      (LIST 'INTEGERP (CADDR X))
      (MAKE-CANCEL-ITIMES-EQUALITY
       (ITIMES-FACTORS (CADR X))
       (ITIMES-FACTORS (CADDR X))
       (BAGINT
        (ITIMES-FACTORS (CADR X))
        (ITIMES-FACTORS (CADDR X))))
      (LIST 'QUOTE F))))
(LIST 'IF (LIST 'INTEGERP (CADDR X))
(MAKE-CANCEL-ITIMES-EQUALITY
(ITIMES-FACTORS (CADR X))
(ITIMES-FACTORS (CADDR X))
(BAGINT (ITIMES-FACTORS (CADR X))
        (ITIMES-FACTORS (CADDR X))))
(LIST 'QUOTE F)))
X))
(INEG (COND
((LISTP (CADADR X))
(COND
((EQUAL (CAADADR X) 'ITIMES)
(IF (LISTP
(BAGINT (ITIMES-FACTORS (CADR X))
(ITIMES-FACTORS (CADDR X))))
(IF (LISTP (CADDR X))
(CASE (CAR (CAR (CDR (CDR X))))

(IPLUS
(MAKE-CANCEL-ITIMES-EQUALITY
(ITIMES-FACTORS (CADR X))
(ITIMES-FACTORS (CADDR X))
(BAGINT
 (ITIMES-FACTORS (CADR X))
 (ITIMES-FACTORS (CADDR X)))))
(ITIMES
(MAKE-CANCEL-ITIMES-EQUALITY
(ITIMES-FACTORS (CADR X))
(ITIMES-FACTORS (CADDR X))
(BAGINT
 (ITIMES-FACTORS (CADR X))
 (ITIMES-FACTORS (CADDR X)))))
(INEG
(IF (LISTP (CADADDR X))
   (IF
    (EQUAL (CAADADDR X) 'ITIMES)
    (MAKE-CANCEL-ITIMES-EQUALITY
     (ITIMES-FACTORS (CADR X))
     (ITIMES-FACTORS (CADDR X))
     (BAGINT
      (ITIMES-FACTORS (CADR X))
      (ITIMES-FACTORS (CADDR X))))
    (LIST 'IF
          (LIST 'INTEGERP (CADDR X))
          (MAKE-CANCEL-ITIMES-EQUALITY
           (ITIMES-FACTORS (CADR X))
           (ITIMES-FACTORS (CADDR X))
           (BAGINT
            (ITIMES-FACTORS (CADR X))
            (ITIMES-FACTORS (CADDR X))))
          (LIST 'QUOTE F)))
   (LIST 'IF
         (LIST 'INTEGERP (CADDR X))
         (MAKE-CANCEL-ITIMES-EQUALITY
          (ITIMES-FACTORS (CADR X))
          (ITIMES-FACTORS (CADDR X))
          (BAGINT
           (ITIMES-FACTORS (CADR X))
           (ITIMES-FACTORS (CADDR X))))
         (LIST 'QUOTE F))))
(OTHERWISE
(LIST 'IF

(LIST 'INTEGERP (CADDR X))
(MAKE-CANCEL-ITIMES-EQUALITY
 (ITIMES-FACTORS (CADR X))
 (ITIMES-FACTORS (CADDR X))
 (BAGINT
  (ITIMES-FACTORS (CADR X))
  (ITIMES-FACTORS (CADDR X))))
(LIST 'QUOTE F))))
(LIST 'IF
(LIST 'INTEGERP (CADDR X))
(MAKE-CANCEL-ITIMES-EQUALITY
(ITIMES-FACTORS (CADR X))
(ITIMES-FACTORS (CADDR X))
(BAGINT (ITIMES-FACTORS (CADR X))
  (ITIMES-FACTORS (CADDR X))))
(LIST 'QUOTE F)))
X))
((LISTP (CADDR X))
(CASE (CAR (CAR (CDR (CDR X))))
(IPLUS (IF
(LISTP
(BAGINT
(ITIMES-FACTORS (CADR X))
(ITIMES-FACTORS (CADDR X))))
(LIST 'IF
(LIST 'INTEGERP (CADR X))
(MAKE-CANCEL-ITIMES-EQUALITY
(ITIMES-FACTORS (CADR X))
(ITIMES-FACTORS (CADDR X))
(BAGINT
 (ITIMES-FACTORS (CADR X))
 (ITIMES-FACTORS (CADDR X))))
(LIST 'QUOTE F))
X))
(ITIMES (IF
(LISTP
(BAGINT
(ITIMES-FACTORS (CADR X))
(ITIMES-FACTORS (CADDR X))))
(LIST 'IF
(LIST 'INTEGERP (CADR X))
(MAKE-CANCEL-ITIMES-EQUALITY
 (ITIMES-FACTORS (CADR X))
 (ITIMES-FACTORS (CADDR X))

    (BAGINT
     (ITIMES-FACTORS (CADR X))
     (ITIMES-FACTORS (CADDR X))))
   (LIST 'QUOTE F))
X))
(INEG (IF (LISTP (CADADDR X))
(IF
(EQUAL (CAADADDR X) 'ITIMES)
(IF
(LISTP
 (BAGINT
  (ITIMES-FACTORS (CADR X))
  (ITIMES-FACTORS (CADDR X))))
(LIST 'IF
      (LIST 'INTEGERP (CADR X))
      (MAKE-CANCEL-ITIMES-EQUALITY
       (ITIMES-FACTORS (CADR X))
       (ITIMES-FACTORS (CADDR X))
       (BAGINT
        (ITIMES-FACTORS (CADR X))
        (ITIMES-FACTORS (CADDR X))))
      (LIST 'QUOTE F))
X)
X)
X))
(OTHERWISE X)))
(T X)))
((LISTP (CADDR X))
(CASE (CAR (CAR (CDR (CDR X))))
(IPLUS (IF
(LISTP
(BAGINT
(ITIMES-FACTORS (CADR X))
(ITIMES-FACTORS (CADDR X))))
(LIST 'IF
(LIST 'INTEGERP (CADR X))
(MAKE-CANCEL-ITIMES-EQUALITY
 (ITIMES-FACTORS (CADR X))
 (ITIMES-FACTORS (CADDR X))
 (BAGINT
  (ITIMES-FACTORS (CADR X))
  (ITIMES-FACTORS (CADDR X))))
(LIST 'QUOTE F))
X))

(ITIMES (IF
(LISTP
(BAGINT
(ITIMES-FACTORS (CADR X))
(ITIMES-FACTORS (CADDR X))))
(LIST 'IF
(LIST 'INTEGERP (CADR X))
(MAKE-CANCEL-ITIMES-EQUALITY
 (ITIMES-FACTORS (CADR X))
 (ITIMES-FACTORS (CADDR X))
 (BAGINT
  (ITIMES-FACTORS (CADR X))
  (ITIMES-FACTORS (CADDR X))))
(LIST 'QUOTE F))
X))
(INEG (IF (LISTP (CADADDR X))
(IF (EQUAL (CAADADDR X) 'ITIMES)
(IF
(LISTP
 (BAGINT
  (ITIMES-FACTORS (CADR X))
  (ITIMES-FACTORS (CADDR X))))
(LIST 'IF
      (LIST 'INTEGERP (CADR X))
      (MAKE-CANCEL-ITIMES-EQUALITY
       (ITIMES-FACTORS (CADR X))
       (ITIMES-FACTORS (CADDR X))
       (BAGINT
        (ITIMES-FACTORS (CADR X))
        (ITIMES-FACTORS (CADDR X))))
      (LIST 'QUOTE F))
X)
X)
X))
(OTHERWISE X)))
(T X)))
(OTHERWISE
(IF (LISTP (CADDR X))
(CASE (CAR (CAR (CDR (CDR X))))
(IPLUS (IF
(LISTP
(BAGINT (ITIMES-FACTORS (CADR X))
(ITIMES-FACTORS (CADDR X))))
(LIST 'IF

(LIST 'INTEGERP (CADR X))
(MAKE-CANCEL-ITIMES-EQUALITY
(ITIMES-FACTORS (CADR X))
(ITIMES-FACTORS (CADDR X))
(BAGINT
 (ITIMES-FACTORS (CADR X))
 (ITIMES-FACTORS (CADDR X))))
(LIST 'QUOTE F))
X))
(ITIMES (IF
(LISTP
(BAGINT
(ITIMES-FACTORS (CADR X))
(ITIMES-FACTORS (CADDR X))))
(LIST 'IF
(LIST 'INTEGERP (CADR X))
(MAKE-CANCEL-ITIMES-EQUALITY
 (ITIMES-FACTORS (CADR X))
 (ITIMES-FACTORS (CADDR X))
 (BAGINT
  (ITIMES-FACTORS (CADR X))
  (ITIMES-FACTORS (CADDR X))))
(LIST 'QUOTE F))
X))
(INEG (IF (LISTP (CADADDR X))
(IF (EQUAL (CAADADDR X) 'ITIMES)
(IF
(LISTP
 (BAGINT
  (ITIMES-FACTORS (CADR X))
  (ITIMES-FACTORS (CADDR X))))
(LIST 'IF
      (LIST 'INTEGERP (CADR X))
      (MAKE-CANCEL-ITIMES-EQUALITY
       (ITIMES-FACTORS (CADR X))
       (ITIMES-FACTORS (CADDR X))
       (BAGINT
        (ITIMES-FACTORS (CADR X))
        (ITIMES-FACTORS (CADDR X))))
      (LIST 'QUOTE F))
X)
X)
X))
(OTHERWISE X))

X))))
((LISTP (CADDR X))
(CASE (CAR (CAR (CDR (CDR X))))
(IPLUS (IF (LISTP (BAGINT (ITIMES-FACTORS (CADR X))
        (ITIMES-FACTORS (CADDR X))))
(LIST 'IF (LIST 'INTEGERP (CADR X))
(MAKE-CANCEL-ITIMES-EQUALITY
(ITIMES-FACTORS (CADR X))
(ITIMES-FACTORS (CADDR X))
(BAGINT (ITIMES-FACTORS (CADR X))
        (ITIMES-FACTORS (CADDR X))))
(LIST 'QUOTE F))
X))
(ITIMES (IF (LISTP (BAGINT (ITIMES-FACTORS (CADR X))
         (ITIMES-FACTORS (CADDR X))))
(LIST 'IF (LIST 'INTEGERP (CADR X))
(MAKE-CANCEL-ITIMES-EQUALITY
 (ITIMES-FACTORS (CADR X))
 (ITIMES-FACTORS (CADDR X))
 (BAGINT (ITIMES-FACTORS (CADR X))
         (ITIMES-FACTORS (CADDR X))))
(LIST 'QUOTE F))
X))
(INEG (IF (LISTP (CADADDR X))
(IF (EQUAL (CAADADDR X) 'ITIMES)
(IF (LISTP
 (BAGINT (ITIMES-FACTORS (CADR X))
         (ITIMES-FACTORS (CADDR X))))
(LIST 'IF
      (LIST 'INTEGERP (CADR X))
      (MAKE-CANCEL-ITIMES-EQUALITY
       (ITIMES-FACTORS (CADR X))
       (ITIMES-FACTORS (CADDR X))
       (BAGINT
        (ITIMES-FACTORS (CADR X))
        (ITIMES-FACTORS (CADDR X))))
      (LIST 'QUOTE F))
X)
X)
X))
(OTHERWISE X)))
(T X))
X)
X))

Theorem: cancel-itimes-factors-expanded-cancel-itimes-factors cancel-itimes-factors-expanded (x) = cancel-itimes-factors (x)

Event: Disable cancel-itimes-factors-expanded.

Event: Disable iplus-or-itimes-term.

Theorem: equal-itimes-list-eval$-list-delete-new-1 (fix-int (eval$ (t, elt, a)) ≠ 0) → ((x = itimes-list (eval$ ('list, delete (elt, bag), a)))

= if elt ∈ bag

then integerp (x)

∧ (itimes (x, eval$ (t, elt, a))

= itimes-list (eval$ ('list, bag, a)))

else x = itimes-list (eval$ ('list, bag, a)) endif)

Theorem: equal-itimes-list-eval$-list-delete-new-2 (fix-int (eval$ (t, elt, a)) ≠ 0) → ((itimes-list (eval$ ('list, delete (elt, bag), a)) = x)

= if elt ∈ bag

then integerp (x)

∧ (itimes (x, eval$ (t, elt, a))

= itimes-list (eval$ ('list, bag, a)))

else x = itimes-list (eval$ ('list, bag, a)) endif)

Theorem: itimes-itimes-list-eval$-list-delete (x ∈ bag) → (itimes (eval$ (t, x, a), itimes-list (eval$ ('list, delete (x, bag), a)))

= itimes-list (eval$ ('list, bag, a)))

Theorem: equal-itimes-list-eval$-list-bagdiff (subbagp (in-both, bag1 ) ∧ subbagp (in-both, bag2 ) ∧ (itimes-list (eval$ ('list, in-both, a)) ≠ 0)) → ((itimes-list (eval$ ('list, bagdiff (bag1 , in-both), a))

= itimes-list (eval$ ('list, bagdiff (bag2 , in-both), a))) = (itimes-list (eval$ ('list, bag1 , a))

= itimes-list (eval$ ('list, bag2 , a))))

Theorem: membership-of-0-implies-itimes-list-is-0 (0 ∈ x) → (itimes-list (x) = 0)

Theorem: member-0-eval$-list (0 ∈ x) → (0 ∈ eval$ ('list, x, a))

Theorem: itimes-list-eval$-factors-lemma itimes (itimes-list (eval$ ('list, bagint (bag1 , bag2 ), a)),

itimes-list (eval$ ('list, bagdiff (bag2 , bagint (bag1 , bag2 )), a))) = itimes-list (eval$ ('list, bag2 , a))

Theorem: itimes-list-eval$-factors-lemma-prime itimes (itimes-list (eval$ ('list, bagint (bag1 , bag2 ), a)),

itimes-list (eval$ ('list, bagdiff (bag1 , bagint (bag1 , bag2 )), a))) = itimes-list (eval$ ('list, bag1 , a))

Theorem: itimes-list-eval$-factors itimes-list (eval$ ('list, itimes-factors (x), a)) = fix-int (eval$ (t, x, a))

Theorem: iplus-or-itimes-term-integerp-eval$ iplus-or-itimes-term (x) → integerp (eval$ (t, x, a))

Theorem: eval$-list-bagint-0 (itimes-list (eval$ ('list, bagint (x, y), a)) = 0) → ((itimes-list (eval$ ('list, x, a)) = 0)

∧ (itimes-list (eval$ ('list, y, a)) = 0))

Theorem: eval$-list-bagint-0-implies-equal ((itimes-list (eval$ ('list, bagint (itimes-factors (v), itimes-factors (w)), a)) = 0) ∧ integerp (eval$ (t, v, a)) ∧ integerp (eval$ (t, w, a))) → ((eval$ (t, v, a) = eval$ (t, w, a)) = t)

Theorem: correctness-of-cancel-itimes-factors eval$ (t, x, a) = eval$ (t, cancel-itimes-factors-expanded (x), a)

;; OK -- now, the lessp case, finally.  Ugh!

Definition: cancel-itimes-ilessp-factors (x) = if listp (x)

then if car (x) = 'ilessp

then if listp (bagint (itimes-factors (cadr (x)),

itimes-factors (caddr (x)))) then make-cancel-itimes-inequality (itimes-factors (cadr (x)),

itimes-factors (caddr (x)),

bagint (itimes-factors (cadr (x)),

itimes-factors (caddr (x))))

else x endif else x endif

else x endif Theorem: bagint-singleton bagint (x, list (y)) = if y ∈ x then list (y)

else nil endif

Theorem: izerop-ilessp-0-relationship (fix-int (x) = 0) = ((¬ ilessp (x, 0)) ∧ (¬ ilessp (0, x)))

Theorem: ilessp-itimes-list-eval$-list-delete-helper-1 ilessp (0, w) → (ilessp (itimes (x, w), itimes (w, u)) = ilessp (x, u))

Theorem: ilessp-itimes-list-eval$-list-delete-helper-2 ilessp (w, 0) → (ilessp (itimes (w, u), itimes (x, w)) = ilessp (x, u))

Theorem: ilessp-itimes-list-eval$-list-delete ((z ∈ y) ∧ (fix-int (eval$ (t, z, a)) ≠ 0)) → (ilessp (x, itimes-list (eval$ ('list, delete (z, y), a)))

= if ilessp (0, eval$ (t, z, a))

then ilessp (itimes (x, eval$ (t, z, a)),

itimes-list (eval$ ('list, y, a)))

elseif ilessp (eval$ (t, z, a), 0)

then ilessp (itimes-list (eval$ ('list, y, a)),

itimes (x, eval$ (t, z, a)))

else f endif)

Theorem: ilessp-itimes-list-eval$-list-delete-prime-helper-1 ilessp (0, w) → (ilessp (itimes (w, u), itimes (x, w)) = ilessp (u, x))

Theorem: ilessp-itimes-list-eval$-list-delete-prime-helper-2 ilessp (w, 0) → (ilessp (itimes (x, w), itimes (w, u)) = ilessp (u, x))

Theorem: ilessp-itimes-list-eval$-list-delete-prime ((z ∈ y) ∧ (fix-int (eval$ (t, z, a)) ≠ 0)) → (ilessp (itimes-list (eval$ ('list, delete (z, y), a)), x)

= if ilessp (0, eval$ (t, z, a))

then ilessp (itimes-list (eval$ ('list, y, a)),

itimes (x, eval$ (t, z, a)))

elseif ilessp (eval$ (t, z, a), 0)

then ilessp (itimes (x, eval$ (t, z, a)),

itimes-list (eval$ ('list, y, a)))

else f endif)

;; **** Do I have anything like the following two lemmas for the equality case?
;; Should I?
;;;***** I should also consider if I've dealt with things like 0 = a*x + b*x, and
;;; simlilarly for ilessp.

Theorem: ilessp-0-itimes ilessp (0, itimes (x, y)) = ((ilessp (0, x) ∧ ilessp (0, y)) ∨ (ilessp (x, 0) ∧ ilessp (y, 0)))

Theorem: ilessp-itimes-0 ilessp (itimes (x, y), 0) = ((ilessp (0, x) ∧ ilessp (y, 0)) ∨ (ilessp (x, 0) ∧ ilessp (0, y)))

Theorem: ilessp-itimes-list-eval$-list-bagdiff (subbagp (in-both, bag1 ) ∧ subbagp (in-both, bag2 ) ∧ (itimes-list (eval$ ('list, in-both, a)) ≠ 0)) → (ilessp (itimes-list (eval$ ('list, bagdiff (bag1 , in-both), a)),

itimes-list (eval$ ('list, bagdiff (bag2 , in-both), a))) = if ilessp (0, itimes-list (eval$ ('list, in-both, a))) then ilessp (itimes-list (eval$ ('list, bag1 , a)),

itimes-list (eval$ ('list, bag2 , a)))

else ilessp (itimes-list (eval$ ('list, bag2 , a)), itimes-list (eval$ ('list, bag1 , a))) endif)

Theorem: zero-ilessp-implies-not-equal ilessp (0, x) → (0 ≠ x)

Theorem: ilessp-itimes-list-eval$-list-bagdiff-corollary-1 (subbagp (in-both, bag1 ) ∧ subbagp (in-both, bag2 ) ∧ ilessp (0, itimes-list (eval$ ('list, in-both, a)))) → (ilessp (itimes-list (eval$ ('list, bagdiff (bag1 , in-both), a)),

itimes-list (eval$ ('list, bagdiff (bag2 , in-both), a))) = ilessp (itimes-list (eval$ ('list, bag1 , a)),

itimes-list (eval$ ('list, bag2 , a))))

Theorem: ilessp-zero-implies-not-equal ilessp (x, 0) → (0 ≠ x)

Theorem: ilessp-itimes-list-eval$-list-bagdiff-corollary-2 (subbagp (in-both, bag1 ) ∧ subbagp (in-both, bag2 ) ∧ ilessp (itimes-list (eval$ ('list, in-both, a)), 0)) → (ilessp (itimes-list (eval$ ('list, bagdiff (bag1 , in-both), a)),

itimes-list (eval$ ('list, bagdiff (bag2 , in-both), a))) = ilessp (itimes-list (eval$ ('list, bag2 , a)),

itimes-list (eval$ ('list, bag1 , a))))

Theorem: member-0-itimes-factors-yields-0 (eval$ (t, w, a) ≠ 0) → (0 ∉ itimes-factors (w))

Theorem: member-0-itimes-factors-yields-0-ilessp-consequence-1 ilessp (eval$ (t, w, a), 0) → (0 ∉ itimes-factors (w))

Theorem: member-0-itimes-factors-yields-0-ilessp-consequence-2 ilessp (0, eval$ (t, w, a)) → (0 ∉ itimes-factors (w))

#|
(prove-lemma eval$-list-bagint-0 nil
  (implies (equal (itimes-list (eval$ 'list (bagint x y) a)) 0)
           (and (equal (itimes-list (eval$ 'list x a)) 0)
                (equal (itimes-list (eval$ 'list y a)) 0)))
  ((use (subsetp-implies-itimes-list-eval$-equals-0
         (x (bagint x y))
         (y x))
        (subsetp-implies-itimes-list-eval$-equals-0
         (x (bagint x y))
         (y y)))))
|#
#|
(prove-lemma eval$-list-bagint-0-implies-equal (rewrite)
  (implies (and (equal (itimes-list (eval$ 'list (bagint (itimes-factors v) (itimes-factors w)) a))
                       0)
                (integerp (eval$ t v a))
                (integerp (eval$ t w a)))
           (equal (equal (eval$ t v a) (eval$ t w a))
                  t))
  ((use (eval$-list-bagint-0 (x (itimes-factors v))
                             (y (itimes-factors w))))))
|#
;; At this point I'm going to switch the states of ilessp-trichotomy and
;; izerop-ilessp-0-relationship, for good (or till I change my mind again!).

Event: Enable ilessp-trichotomy.

Event: Disable izerop-ilessp-0-relationship.

Theorem: eval$-list-bagint-0-for-ilessp ((¬ ilessp (itimes-list (eval$ ('list, bagint (x, y), a)), 0)) ∧ (¬ ilessp (0, itimes-list (eval$ ('list, bagint (x, y), a))))) → ((fix-int (itimes-list (eval$ ('list, x, a))) = 0)

∧ (fix-int (itimes-list (eval$ ('list, y, a))) = 0))

Theorem: eval$-list-bagint-0-implies-equal-for-ilessp-lemma ((¬ ilessp (itimes-list (eval$ ('list,

bagint (itimes-factors (v), itimes-factors (w)), a)),

0))

∧ (¬ ilessp (0,

itimes-list (eval$ ('list,

bagint (itimes-factors (v),

itimes-factors (w)), a)))))

→ (fix-int (eval$ (t, v, a)) = fix-int (eval$ (t, w, a)))

Theorem: equal-fix-int-to-ilessp (fix-int (x) = fix-int (y)) → (¬ ilessp (x, y))

Theorem: eval$-list-bagint-0-implies-equal-for-ilessp ((¬ ilessp (itimes-list (eval$ ('list,

bagint (itimes-factors (v), itimes-factors (w)), a)),

0))

∧ (¬ ilessp (0,

itimes-list (eval$ ('list,

bagint (itimes-factors (v),

itimes-factors (w)), a)))))

→ ((¬ ilessp (eval$ (t, v, a), eval$ (t, w, a)))

∧ (¬ ilessp (eval$ (t, w, a), eval$ (t, v, a))))

;; The rewrite rule ILESSP-TRICHOTOMY seemed to mess up the proof of the following,
;; so I'm just going to leave it disabled.

Event: Disable ilessp-trichotomy.

Theorem: correctness-of-cancel-itimes-ilessp-factors eval$ (t, x, a) = eval$ (t, cancel-itimes-ilessp-factors (x), a)

;; OK -- now, the zero cases.

Event: Enable lessp-count-listp-cdr.

Definition: disjoin-equalities-with-0 (factors) = if listp (cdr (factors)) then list ('or,

list ('equal, list ('fix-int, car (factors)), ''0), disjoin-equalities-with-0 (cdr (factors))) else list ('equal, list ('fix-int, car (factors)), ''0) endif

Event: Disable lessp-count-listp-cdr.

Definition: cancel-factors-0 (x) = if listp (x)

then if car (x) = 'equal

then if cadr (x) = ''0

then let factors be itimes-factors (caddr (x)) in if listp (cdr (factors)) then disjoin-equalities-with-0 (factors) else x endif endlet

elseif caddr (x) = ''0

then let factors be itimes-factors (cadr (x)) in if listp (cdr (factors)) then disjoin-equalities-with-0 (factors) else x endif endlet

else x endif else x endif

else x endif

Definition: some-eval$s-to-0 (x, a) = if listp (x)

then (fix-int (eval$ (t, car (x), a)) = 0) ∨ some-eval$s-to-0 (cdr (x), a)

else f endif

Theorem: eval$-disjoin-equalities-with-0 listp (lst) → (eval$ (t, disjoin-equalities-with-0 (lst), a)

= some-eval$s-to-0 (lst, a))

Theorem: some-eval$s-to-0-append some-eval$s-to-0 (append (x, y), a) = (some-eval$s-to-0 (x, a) ∨ some-eval$s-to-0 (y, a))

Theorem: some-eval$s-to-0-eliminator some-eval$s-to-0 (x, a) = (itimes-list (eval$ ('list, x, a)) = 0)

Theorem: listp-cdr-factors-implies-integerp listp (cdr (itimes-factors (v))) → integerp (eval$ (t, v, a))

Theorem: correctness-of-cancel-factors-0 eval$ (t, x, a) = eval$ (t, cancel-factors-0 (x), a)

;; and now for inequalities...

Event: Enable lessp-count-listp-cdr.

Definition: conjoin-inequalities-with-0 (factors, parity) = if listp (cdr (factors))

then if parity

then list ('or,

list ('and, list ('ilessp, ''0, car (factors)), conjoin-inequalities-with-0 (cdr (factors), t)),

list ('and, list ('ilessp, car (factors), ''0), conjoin-inequalities-with-0 (cdr (factors), f)))

else list ('or,

list ('and, list ('ilessp, car (factors), ''0), conjoin-inequalities-with-0 (cdr (factors), t)),

list ('and, list ('ilessp, ''0, car (factors)), conjoin-inequalities-with-0 (cdr (factors), f))) endif

elseif parity then list ('ilessp, ''0, car (factors)) else list ('ilessp, car (factors), ''0) endif

Event: Disable lessp-count-listp-cdr.

Definition: cancel-factors-ilessp-0 (x) = if listp (x)

then if car (x) = 'ilessp

then if cadr (x) = ''0

then let factors be itimes-factors (caddr (x)) in if listp (cdr (factors)) then conjoin-inequalities-with-0 (factors, t) else x endif endlet elseif caddr (x) = ''0 then let factors be itimes-factors (cadr (x))

in

if listp (cdr (factors))

then conjoin-inequalities-with-0 (factors, f) else x endif endlet

else x endif else x endif

else x endif

Theorem: conjoin-inequalities-with-0-eliminator listp (x) → (eval$ (t, conjoin-inequalities-with-0 (x, parity), a)

= if parity then ilessp (0, itimes-list (eval$ ('list, x, a))) else ilessp (itimes-list (eval$ ('list, x, a)), 0) endif)

Theorem: correctness-of-cancel-factors-ilessp-0 eval$ (t, x, a) = eval$ (t, cancel-factors-ilessp-0 (x), a)

Event: Disable equal-itimes-list-eval$-list-delete-new-1.

Event: Disable equal-itimes-list-eval$-list-delete-new-2.

Event: Disable itimes-itimes-list-eval$-list-delete.

Event: Disable equal-itimes-list-eval$-list-bagdiff.

Event: Disable itimes-list-eval$-factors-lemma.

Event: Disable itimes-list-eval$-factors-lemma-prime.

Event: Disable itimes-list-eval$-factors.

Event: Disable iplus-or-itimes-term-integerp-eval$.

Event: Disable eval$-list-bagint-0.

Event: Disable eval$-list-bagint-0-implies-equal.

Event: Disable izerop-ilessp-0-relationship.

Event: Disable ilessp-itimes-list-eval$-list-delete-helper-1. Event: Disable ilessp-itimes-list-eval$-list-delete-helper-2. Event: Disable ilessp-itimes-list-eval$-list-delete. Event: Disable ilessp-itimes-list-eval$-list-delete-prime-helper-1. Event: Disable ilessp-itimes-list-eval$-list-delete-prime-helper-2. Event: Disable ilessp-itimes-list-eval$-list-delete-prime. Event: Disable ilessp-0-itimes. Event: Disable ilessp-itimes-0. Event: Disable listp-cdr-factors-implies-integerp.

;; We presumably have better meta-lemmas now, but if we want we
;; can disable those (i.e., correctness-of-cancel-itimes-factors,
;; correctness-of-cancel-itimes-ilessp-factors,
;; correctness-of-cancel-factors-0, and
;; correctness-of-cancel-factors-ilessp-0) and enable the two
;; mentioned below:

Event: Disable correctness-of-cancel-itimes. Event: Disable correctness-of-cancel-itimes-ilessp.

;; I'll disable some rules now, finally, that I'd previously thought
;; would be OK but now fear because of potential nasty backchaining.

Event: Disable not-integerp-implies-not-equal-iplus. Event: Disable not-integerp-implies-not-equal-itimes.

Event: Disable subbagp-subsetp.

Event: Disable eval$-list-bagint-0-implies-equal-for-ilessp.

; ---------- Cancel ineg terms from equalities and inequalities ----------

Definition: split-out-ineg-terms (x) = if listp (x)

then let pair be split-out-ineg-terms (cdr (x)),

a be car (x) in if listp (a) then if car (a) = 'ineg

then cons (car (pair), cons (cadr (a), cdr (pair))) elseif (car (a) = 'quote)

∧ negativep (cadr (a))

∧ (negative-guts (cadr (a)) ≠ 0) then cons (car (pair),

cons (list ('quote, negative-guts (cadr (a))),

cdr (pair))) else cons (cons (a, car (pair)), cdr (pair)) endif else cons (cons (a, car (pair)), cdr (pair)) endif endlet

else cons (nil, nil) endif

Definition: remove-inegs (x, y) = let xpair be split-out-ineg-terms (x),

ypair be split-out-ineg-terms (y) in if listp (cdr (xpair)) ∨ listp (cdr (ypair)) then cons (append (cdr (ypair), car (xpair)),

append (cdr (xpair), car (ypair)))

else f endif endlet

Definition: iplus-or-ineg-term (x) = (listp (x) ∧ ((car (x) = 'ineg) ∨ (car (x) = 'iplus)))

Definition: make-cancel-ineg-terms-equality (x) = let new-fringes be remove-inegs (iplus-fringe (cadr (x)),

iplus-fringe (caddr (x))) in if new-fringes then if iplus-or-ineg-term (cadr (x))

then if iplus-or-ineg-term (caddr (x))

then list ('equal, iplus-tree (car (new-fringes)), iplus-tree (cdr (new-fringes)))

else list ('if, list ('integerp, caddr (x)),

                     list ('equal,

iplus-tree (car (new-fringes)), iplus-tree (cdr (new-fringes))),

list ('quote, f)) endif

elseif iplus-or-ineg-term (caddr (x))

then list ('if, list ('integerp, cadr (x)),

                 list ('equal,

iplus-tree (car (new-fringes)), iplus-tree (cdr (new-fringes))),

list ('quote, f))

else x endif else x endif endlet

Definition: cancel-ineg-terms-from-equality (x) = if listp (x) ∧ (car (x) = 'equal)

then make-cancel-ineg-terms-equality (x)

else x endif

;; The following was created from nqthm-macroexpand with arguments
;; and or make-cancel-ineg-terms-equality iplus-or-ineg-term

Definition: cancel-ineg-terms-from-equality-expanded (x) = if listp (x)

then if car (x) = 'equal

then if remove-inegs (iplus-fringe (cadr (x)),

iplus-fringe (caddr (x)))

then if listp (cadr (x))

then case on car (car (cdr (x))): case = ineg then if listp (caddr (x))

then case on car (car (cdr (cdr (x)))): case = ineg then list ('equal, iplus-tree (car (remove-inegs (iplus-fringe (cadr (x)),

iplus-fringe (caddr (x))))),

iplus-tree (cdr (remove-inegs (iplus-fringe (cadr (x)),

iplus-fringe (caddr (x))))))

case = iplus then list ('equal,

iplus-tree (car (remove-inegs (iplus-fringe (cadr (x)),

iplus-fringe (caddr (x))))),

iplus-tree (cdr (remove-inegs (iplus-fringe (cadr (x)),

iplus-fringe (caddr (x))))))

otherwise list ('if,

            list ('integerp,

caddr (x)),

            list ('equal,

iplus-tree (car (remove-inegs (iplus-fringe (cadr (x)),

iplus-fringe (caddr (x))))),

iplus-tree (cdr (remove-inegs (iplus-fringe (cadr (x)),

iplus-fringe (caddr (x)))))),

list ('quote, f)) endcase

else list ('if, list ('integerp, caddr (x)),

  list ('equal,

iplus-tree (car (remove-inegs (iplus-fringe (cadr (x)),

iplus-fringe (caddr (x))))),

iplus-tree (cdr (remove-inegs (iplus-fringe (cadr (x)),

iplus-fringe (caddr (x)))))),

list ('quote, f)) endif

case = iplus then if listp (caddr (x))

then case on car (car (cdr (cdr (x)))): case = ineg then list ('equal,

iplus-tree (car (remove-inegs (iplus-fringe (cadr (x)),

iplus-fringe (caddr (x))))),

iplus-tree (cdr (remove-inegs (iplus-fringe (cadr (x)),

iplus-fringe (caddr (x))))))

case = iplus then list ('equal,

iplus-tree (car (remove-inegs (iplus-fringe (cadr (x)),

iplus-fringe (caddr (x))))),

iplus-tree (cdr (remove-inegs (iplus-fringe (cadr (x)),

iplus-fringe (caddr (x))))))

otherwise list ('if,

             list ('integerp,

caddr (x)),

list ('equal,

iplus-tree (car (remove-inegs (iplus-fringe (cadr (x)),

iplus-fringe (caddr (x))))),

iplus-tree (cdr (remove-inegs (iplus-fringe (cadr (x)),

iplus-fringe (caddr (x)))))),

list ('quote, f)) endcase

else list ('if, list ('integerp, caddr (x)),

list ('equal,

iplus-tree (car (remove-inegs (iplus-fringe (cadr (x)),

iplus-fringe (caddr (x))))),

iplus-tree (cdr (remove-inegs (iplus-fringe (cadr (x)),

iplus-fringe (caddr (x)))))),

list ('quote, f)) endif

otherwise if listp (caddr (x))

then case on car (car (cdr (cdr (x)))): case = ineg then list ('if,

list ('integerp,

cadr (x)),

list ('equal,

iplus-tree (car (remove-inegs (iplus-fringe (cadr (x)),

iplus-fringe (caddr (x))))),

iplus-tree (cdr (remove-inegs (iplus-fringe (cadr (x)),

iplus-fringe (caddr (x)))))),

list ('quote, f))

case = iplus then list ('if,

list ('integerp,

cadr (x)),

list ('equal,

iplus-tree (car (remove-inegs (iplus-fringe (cadr (x)),

iplus-fringe (caddr (x))))),

iplus-tree (cdr (remove-inegs (iplus-fringe (cadr (x)),

iplus-fringe (caddr (x)))))),

list ('quote, f))

otherwise x endcase else x endif endcase

elseif listp (caddr (x)) then case on car (car (cdr (cdr (x)))):

case = ineg then list ('if,

list ('integerp, cadr (x)),

                                list ('equal,

iplus-tree (car (remove-inegs (iplus-fringe (cadr (x)),

iplus-fringe (caddr (x))))),

iplus-tree (cdr (remove-inegs (iplus-fringe (cadr (x)),

iplus-fringe (caddr (x)))))),

list ('quote, f))

case = iplus then list ('if,

list ('integerp, cadr (x)),

                                 list ('equal,

iplus-tree (car (remove-inegs (iplus-fringe (cadr (x)),

iplus-fringe (caddr (x))))),

iplus-tree (cdr (remove-inegs (iplus-fringe (cadr (x)),

iplus-fringe (caddr (x)))))),

list ('quote, f))

otherwise x endcase else x endif

else x endif else x endif

else x endif

Theorem: cancel-ineg-terms-from-equality-cancel-ineg-terms-from-equality-expanded cancel-ineg-terms-from-equality-expanded (x) = cancel-ineg-terms-from-equality (x)

Event: Disable cancel-ineg-terms-from-equality-expanded.

Theorem: integerp-eval$-iplus-or-ineg-term iplus-or-ineg-term (x) → integerp (eval$ (t, x, a))

Event: Disable iplus-or-ineg-term.

Theorem: eval$-iplus-list-car-remove-inegs remove-inegs (x, y) → (iplus-list (eval$ ('list, car (remove-inegs (x, y)), a))

= iplus (iplus-list (eval$ ('list, car (split-out-ineg-terms (x)), a)), iplus-list (eval$ ('list, cdr (split-out-ineg-terms (y)), a))))

Theorem: eval$-iplus-list-cdr-remove-inegs remove-inegs (x, y) → (iplus-list (eval$ ('list, cdr (remove-inegs (x, y)), a))

= iplus (iplus-list (eval$ ('list, car (split-out-ineg-terms (y)), a)), iplus-list (eval$ ('list, cdr (split-out-ineg-terms (x)), a))))

Theorem: minus-ineg ((x ∈ N) ∧ (x ≠ 0)) → ((− x) = ineg (x))

Theorem: iplus-list-eval$-car-split-out-ineg-terms iplus-list (eval$ ('list, car (split-out-ineg-terms (x)), a)) = iplus (iplus-list (eval$ ('list, x, a)),

iplus-list (eval$ ('list, cdr (split-out-ineg-terms (x)), a)))

Event: Disable remove-inegs.

Theorem: correctness-of-cancel-ineg-terms-from-equality eval$ (t, x, a) = eval$ (t, cancel-ineg-terms-from-equality-expanded (x), a)

Definition: make-cancel-ineg-terms-inequality (x) = let new-fringes be remove-inegs (iplus-fringe (cadr (x)),

iplus-fringe (caddr (x)))

in

if new-fringes

then list ('ilessp, iplus-tree (car (new-fringes)), iplus-tree (cdr (new-fringes)))

else x endif endlet

Definition: cancel-ineg-terms-from-inequality (x) = if listp (x) ∧ (car (x) = 'ilessp)

then if iplus-or-ineg-term (cadr (x)) then make-cancel-ineg-terms-inequality (x) elseif iplus-or-ineg-term (caddr (x)) then make-cancel-ineg-terms-inequality (x) else x endif

else x endif

;; The following was created from nqthm-macroexpand with arguments
;; and or make-cancel-ineg-terms-inequality iplus-or-ineg-term

Definition: cancel-ineg-terms-from-inequality-expanded (x) = if listp (x)

then if car (x) = 'ilessp

then if listp (cadr (x))

then case on car (car (cdr (x))): case = ineg then if remove-inegs (iplus-fringe (cadr (x)),

iplus-fringe (caddr (x)))

then list ('ilessp,

iplus-tree (car (remove-inegs (iplus-fringe (cadr (x)),

iplus-fringe (caddr (x))))),

iplus-tree (cdr (remove-inegs (iplus-fringe (cadr (x)),

iplus-fringe (caddr (x))))))

else x endif case = iplus then if remove-inegs (iplus-fringe (cadr (x)),

iplus-fringe (caddr (x)))

then list ('ilessp,

iplus-tree (car (remove-inegs (iplus-fringe (cadr (x)),

iplus-fringe (caddr (x))))),

iplus-tree (cdr (remove-inegs (iplus-fringe (cadr (x)),

iplus-fringe (caddr (x))))))

else x endif otherwise if listp (caddr (x))

then case on car (car (cdr (cdr (x)))): case = ineg then if remove-inegs (iplus-fringe (cadr (x)),

iplus-fringe (caddr (x)))

then list ('ilessp,

iplus-tree (car (remove-inegs (iplus-fringe (cadr (x)),

iplus-fringe (caddr (x))))),

iplus-tree (cdr (remove-inegs (iplus-fringe (cadr (x)),

iplus-fringe (caddr (x))))))

else x endif case = iplus then if remove-inegs (iplus-fringe (cadr (x)),

iplus-fringe (caddr (x)))

then list ('ilessp,

iplus-tree (car (remove-inegs (iplus-fringe (cadr (x)),

iplus-fringe (caddr (x))))),

iplus-tree (cdr (remove-inegs (iplus-fringe (cadr (x)),

iplus-fringe (caddr (x))))))

else x endif otherwise x endcase

else x endif endcase

elseif listp (caddr (x)) then case on car (car (cdr (cdr (x)))):

case = ineg then if remove-inegs (iplus-fringe (cadr (x)),

iplus-fringe (caddr (x))) then list ('ilessp,

iplus-tree (car (remove-inegs (iplus-fringe (cadr (x)),

iplus-fringe (caddr (x))))),

iplus-tree (cdr (remove-inegs (iplus-fringe (cadr (x)),

iplus-fringe (caddr (x))))))

else x endif case = iplus then if remove-inegs (iplus-fringe (cadr (x)),

iplus-fringe (caddr (x)))

then list ('ilessp,

iplus-tree (car (remove-inegs (iplus-fringe (cadr (x)),

iplus-fringe (caddr (x))))),

iplus-tree (cdr (remove-inegs (iplus-fringe (cadr (x)),

iplus-fringe (caddr (x))))))

else x endif otherwise x endcase

else x endif else x endif

else x endif

Theorem: cancel-ineg-terms-from-inequality-cancel-ineg-terms-from-inequality-expanded cancel-ineg-terms-from-inequality-expanded (x) = cancel-ineg-terms-from-inequality (x)

Event: Disable cancel-ineg-terms-from-inequality-expanded.

Theorem: correctness-of-cancel-ineg-terms-from-inequality eval$ (t, x, a) = eval$ (t, cancel-ineg-terms-from-inequality-expanded (x), a)

Event: Disable minus-ineg.

Event: Disable integerp-eval$-iplus-or-ineg-term.

; ---------- Eliminating constants ----------
;; We want to combine in terms like (iplus 3 (iplus x 7)).  Also, when
;; two iplus terms are equated or in-equated, there should only be a
;; natural number summand on at most one side.  Finally, if one adds 1
;; to the right side of a strict inequality, a stronger inequality (in
;; a certain sense) is obtained by removing the 1 and making a non-strict
;; inequality in the other direction.

Theorem: plus-iplus ((i ∈ N) ∧ (j ∈ N)) → ((i + j ) = iplus (i, j ))

Theorem: iplus-constants iplus (1 + i, iplus (1 + j , x)) = iplus ((1 + i) + (1 + j ), x)

Theorem: numberp-is-integerp (w ∈ N) → integerp (w)

Theorem: difference-idifference ((x ∈ N) ∧ (y ∈ N) ∧ (x ≤ y)) → ((y − x) = idifference (y, x))

Theorem: cancel-constants-equal-lemma ((m ∈ N) ∧ (n ∈ N)) → ((iplus (m, x) = iplus (n, y))

= if m < n then fix-int (x) = iplus (n − m, y) else iplus (m − n, x) = fix-int (y) endif)

Theorem: cancel-constants-equal (iplus (1 + i, x) = iplus (1 + j , y)) = if i < j then fix-int (x) = iplus (j − i, y)

else iplus (i − j , x) = fix-int (y) endif

Theorem: ilessp-add1 (y ∈ N) → (ilessp (x, 1 + y) = (¬ ilessp (y, x)))

Theorem: ilessp-add1-iplus (y ∈ N) → (ilessp (x, iplus (1 + y, z)) = (¬ ilessp (iplus (y, z), x)))

Theorem: cancel-constants-ilessp-lemma-1 ((m ∈ N) ∧ (n ∈ N)) → (ilessp (iplus (m, x), iplus (n, y))

= if m < n then ilessp (x, iplus (n − m, y)) else ilessp (iplus (m − n, x), y) endif)

Theorem: cancel-constants-ilessp-lemma-2 ((m ∈ N) ∧ (n ∈ N)) → (ilessp (iplus (m, x), iplus (n, y))

= if m < n then ¬ ilessp (iplus ((n − m) − 1, y), x) else ilessp (iplus (m − n, x), y) endif)

Theorem: cancel-constants-ilessp ilessp (iplus (1 + i, x), iplus (1 + j , y)) = if i < j then ¬ ilessp (iplus ((j − i) − 1, y), x)

else ilessp (iplus (i − j , x), y) endif Event: Disable plus-iplus.

Event: Disable numberp-is-integerp.

Event: Disable difference-idifference.

;; new stuff about integers from rationals developement

Theorem: ilessp-irem ilessp (irem (x, y), y) = (ilessp (0, y) ∨ (izerop (y) ∧ ilessp (x, 0)))

Theorem: irem-noop ilessp (iabs (a), iabs (b)) → (irem (a, b) = fix-int (a))

Theorem: irem-of-0 ((fix-int (a) = 0) → (irem (a, x) = 0)) ∧ ((fix-int (a) = 0) → (irem (x, a) = fix-int (x)))

Theorem: iplus-irem-itimes-iquo iplus (irem (x, y), itimes (y, iquo (x, y))) = fix-int (x)

Event: Disable iplus-irem-itimes-iquo.

Theorem: irem-iquo-elim integerp (x) → (iplus (irem (x, y), itimes (y, iquo (x, y))) = x)

;; irem has a tough-to-deal-with definition.  Here's a better
;; one.

Definition: my-irem (x, y) = if fix-int (x) = 0 then 0

elseif negativep (x) then ineg (negative-guts (x) mod iabs (y))

else x mod iabs (y) endif

Theorem: irem-is-my-irem irem (x, y) = my-irem (x, y)

Theorem: irem-iplus-0-proof (irem (b, c) = 0) → ((irem (iplus (a, b), c) = 0) = (irem (a, c) = 0))

Theorem: irem-iplus-0 (irem (b, c) = 0) → (((irem (iplus (a, b), c) = 0) = (irem (a, c) = 0))

∧ ((irem (iplus (b, a), c) = 0) = (irem (a, c) = 0)))

Definition: igcd (x, y) = gcd (iabs (x), iabs (y))

Theorem: integerp-igcd integerp (igcd (x, y))

Theorem: commutativity-of-igcd igcd (x, y) = igcd (y, x)

Theorem: igcd-0 (igcd (0, x) = iabs (x)) ∧ (igcd (x, 0) = iabs (x))

Theorem: igcd-1 (igcd (1, x) = 1) ∧ (igcd (x, 1) = 1)

Theorem: equal-igcd-0 (igcd (a, b) = 0) = ((fix-int (a) = 0) ∧ (fix-int (b) = 0))

Theorem: igcd-non-negative ¬ ilessp (igcd (x, y), 0)

Theorem: ilessp-igcd (ilessp (b, igcd (a, b)) = (ilessp (b, 0) ∨ ((fix-int (a) ≠ 0) ∧ (fix-int (b) = 0)))) ∧ (ilessp (b, igcd (b, a))

= (ilessp (b, 0) ∨ ((fix-int (a) ≠ 0) ∧ (fix-int (b) = 0))))

Theorem: igcd-iplus-instance-proof ((ilessp (a, 0) = ilessp (b, 0)) ∨ (¬ ilessp (iabs (b), iabs (a)))) → (igcd (a, iplus (a, b)) = igcd (a, b))

Theorem: igcd-iplus ((ilessp (a, 0) = ilessp (b, 0)) ∨ (¬ ilessp (iabs (b), iabs (a)))) → ((igcd (a, iplus (a, b)) = igcd (a, b))

∧ (igcd (a, iplus (b, a)) = igcd (a, b)))

Event: Disable igcd.

Theorem: irem-igcd (irem (a, igcd (a, b)) = 0) ∧ (irem (b, igcd (a, b)) = 0)

Theorem: distributivity-of-itimes-over-igcd-proof igcd (itimes (x, z), itimes (y, z)) = itimes (iabs (z), igcd (x, y))

Theorem: distributivity-of-itimes-over-igcd (igcd (itimes (x, z), itimes (y, z)) = itimes (iabs (z), igcd (x, y))) ∧ (igcd (itimes (x, z), itimes (z, y)) = itimes (iabs (z), igcd (x, y))) ∧ (igcd (itimes (z, x), itimes (y, z)) = itimes (iabs (z), igcd (x, y))) ∧ (igcd (itimes (z, x), itimes (z, y)) = itimes (iabs (z), igcd (x, y)))

Theorem: common-divisor-divides-igcd ((irem (x, z) = 0) ∧ (irem (y, z) = 0)) → (irem (igcd (x, y), z) = 0)

Theorem: iabs-igcd iabs (igcd (x, y)) = igcd (x, y)

Theorem: associativity-of-igcd igcd (igcd (x, y), z) = igcd (x, igcd (y, z))

Theorem: commutativity2-of-igcd igcd (b, igcd (a, c)) = igcd (a, igcd (b, c))

Theorem: igcd-x-x igcd (x, x) = iabs (x)

Theorem: igcd-idempotence (igcd (x, igcd (x, y)) = igcd (x, y)) ∧ (igcd (y, igcd (x, y)) = igcd (x, y))

Theorem: iquo-0 (iquo (x, y) = 0) = ((fix-int (y) = 0) ∨ ilessp (iabs (x), iabs (y)))

Theorem: ilessp-0-iquo ilessp (0, iquo (x, y)) = ((ilessp (x, 0) = ilessp (y, 0))

∧ (fix-int (x) ≠ 0) ∧ (fix-int (y) ≠ 0) ∧ (¬ ilessp (iabs (x), iabs (y))))

Theorem: iabs-simplify (¬ ilessp (x, 0)) → (iabs (x) = fix-int (x))

Theorem: igcd-iquo-igcd-proof igcd (iquo (x, igcd (x, y)), iquo (y, igcd (x, y))) = if (fix-int (x) = 0) ∧ (fix-int (y) = 0) then 0

else 1 endif Theorem: ilessp-iquo-0 ilessp (iquo (x, y), 0) = ((ilessp (x, 0) ≠ ilessp (y, 0))

∧ (fix-int (x) ≠ 0) ∧ (fix-int (y) ≠ 0) ∧ (¬ ilessp (iabs (x), iabs (y))))

Theorem: iquo-1 iquo (x, 1) = fix-int (x)

Theorem: ilessp-0-igcd ilessp (0, igcd (x, y)) = ((¬ izerop (x)) ∨ (¬ izerop (y)))

Theorem: igcd-minus (¬ ilessp (x, 0)) → ((igcd (− x, y) = igcd (x, y)) ∧ (igcd (y, − x) = igcd (y, x)))

Theorem: iquo-0-arg (iquo (0, x) = 0) ∧ (iquo (x, 0) = 0)

Theorem: itimes-iquo (irem (x, y) = 0) → (itimes (y, iquo (x, y)) = fix-int (x))

Theorem: itimes-hack1-1 (integerp (a) ∧ integerp (b) ∧ (irem (a, ad) = 0) ∧ (irem (b, cb) = 0)) → (itimes (a, b) = itimes (ad, itimes (cb, itimes (iquo (a, ad), iquo (b, cb)))))

Theorem: itimes-hack1-1-1 (((¬ integerp (a)) ∨ (¬ integerp (b))) ∧ (irem (a, ad) = 0) ∧ (irem (b, cb) = 0)) → (itimes (a, b) = itimes (ad, itimes (cb, itimes (iquo (a, ad), iquo (b, cb)))))

Theorem: itimes-hack1-2 (integerp (c) ∧ integerp (d) ∧ (irem (c, cb) = 0) ∧ (irem (d, ad) = 0)) → (itimes (c, d) = itimes (ad, itimes (cb, itimes (iquo (c, cb), iquo (d, ad)))))

Theorem: itimes-hack1-2-1 (((¬ integerp (c)) ∨ (¬ integerp (d))) ∧ (irem (c, cb) = 0) ∧ (irem (d, ad) = 0)) → (itimes (c, d) = itimes (ad, itimes (cb, itimes (iquo (c, cb), iquo (d, ad)))))

Theorem: itimes-hack1 ((irem (a, ad) = 0) ∧ (irem (b, cb) = 0)

∧ (irem (c, cb) = 0) ∧ (irem (d, ad) = 0) ∧ (iquo (a, ad) = iquo (c, cb)) ∧ (iquo (d, ad) = iquo (b, cb))) → ((itimes (a, b) = itimes (c, d)) = t)

Theorem: iquo-x-x iquo (x, x) = if izerop (x) then 0

else 1 endif

Theorem: iquo-0-arg-better (fix-int (z) = 0) → ((iquo (z, x) = 0) ∧ (iquo (x, z) = 0))

Theorem: itimes-hack2 ((iquo (a, igcd (a, d)) = iquo (c, igcd (c, b))) ∧ (iquo (d, igcd (a, d)) = iquo (b, igcd (c, b)))) → ((itimes (a, b) = itimes (c, d)) = t)

;;;;;;
;;;;; Following until gcd-remainder-times-fact1-proof based on something
;;;;; originally suggested by matt kaufmann
;;;;;;

Theorem: gcd-factors-accept ordinalp (cons (1 + x, fix (y))) ∧ (((x ≄ 0) ∧ (y ≄ 0) ∧ (x < y))

→ ord-lessp (cons (1 + x, fix (y − x)), cons (1 + x, fix (y)))) ∧ (((x ≄ 0) ∧ (y ≄ 0) ∧ (x ≮ y))

→ ord-lessp (cons (1 + (x − y), fix (y)), cons (1 + x, fix (y))))

Definition: gcd-factors (x, y) = if x ≃ 0 then cons (0, 1)

elseif y ≃ 0 then cons (1, 0)

elseif x < y

then let factors be gcd-factors (x, y − x) in cons (idifference (car (factors), cdr (factors)), cdr (factors)) endlet

else let factors be gcd-factors (x − y, y) in cons (car (factors),

idifference (cdr (factors), car (factors))) endlet endif

Theorem: gcd-factors-gives-linear-combination let factors be gcd-factors (x, y) in let a be car (factors),

b be cdr (factors) in ((x ∈ N) ∧ (y ∈ N)) → (iplus (itimes (a, x), itimes (b, y)) = gcd (x, y)) endlet endlet

Theorem: gcd-factors-gives-linear-combination-rewrite let factors be gcd-factors (x, y) in let a be car (factors),

b be cdr (factors) in ((x ∈ N) ∧ (y ∈ N)) → (gcd (x, y) = iplus (itimes (a, x), itimes (b, y))) endlet endlet

Theorem: remainder-0-sufficiency ((x ∈ N) ∧ (c ∈ N) ∧ (itimes (x, p) = c)) → (((c mod x) = 0) = t)

Theorem: itimes-iquotient (iremainder (a, x) = 0) → (itimes (x, iquotient (a, x)) = fix-int (a))

Theorem: iquotient-0 iquotient (0, x) = 0

Theorem: iremainder-0 (iremainder (0, x) = 0) ∧ (iremainder (x, 0) = fix-int (x))

Theorem: itimes-iplus-hack ((x ∈ N) ∧ (y ∈ N) ∧ (c ∈ N) ∧ (iremainder (itimes (c, y), x) = 0)) → (itimes (x, iplus (itimes (c, a), itimes (b, iquotient (itimes (c, y), x))))

= itimes (c, iplus (itimes (a, x), itimes (b, y))))

Theorem: irem-0-iremainder-0-help1 (iremainder (x, y) = 0) → (irem (x, y) = 0)

Theorem: irem-0-iremainder-0-help2 (irem (x, y) = 0) → (iremainder (x, y) = 0)

Theorem: irem-0-iremainder-0 (iremainder (x, y) = 0) = (irem (x, y) = 0)

Theorem: equal-itimes-x-x ((itimes (x, y) = x) = ((integerp (x) ∧ (y = 1)) ∨ (x = 0))) ∧ ((itimes (y, x) = x) = ((integerp (x) ∧ (y = 1)) ∨ (x = 0)))

Theorem: divides-product-reduction-helper-1 ((x ∈ N) ∧ (y ∈ N) ∧ (c ∈ N) ∧ (((c ∗ y) mod x) = 0)) → (iremainder (itimes (c, y), x) = 0)

Theorem: divides-product-reduction-helper ((x ∈ N) ∧ (y ∈ N) ∧ (c ∈ N) ∧ (gcd (x, y) = 1) ∧ ((c mod x) ≠ 0)) → (((c ∗ y) mod x) ≠ 0)

Event: Disable divides-product-reduction-helper-1.

Theorem: divides-product-reduction ((x ∈ N) ∧ (y ∈ N) ∧ (c ∈ N) ∧ (gcd (x, y) = 1) ∧ ((c mod x) ≠ 0)) → ((((c ∗ y) mod x) ≠ 0) ∧ (((y ∗ c) mod x) ≠ 0))

Theorem: gcd-remainder-times-fact1-proof-non-numberp-case (((a ∉ N) ∨ (b ∉ N) ∨ (c ∉ N)) ∧ (gcd (a, b) = 1)) → ((((b ∗ c) mod a) = 0) = ((c mod a) = 0))

Theorem: gcd-remainder-times-fact1-proof-numberp-case ((a ∈ N) ∧ (b ∈ N) ∧ (c ∈ N) ∧ (gcd (a, b) = 1)) → ((((b ∗ c) mod a) = 0) = ((c mod a) = 0))

Theorem: gcd-remainder-times-fact1-proof (gcd (a, b) = 1) → ((((b ∗ c) mod a) = 0) = ((c mod a) = 0))

Theorem: divides-each-equality (((a mod b) = 0) ∧ ((b mod a) = 0)) = (fix (a) = fix (b))

;;; Before we go on, prove, disable, and set up theory about
;;; naturals --> integers

Theorem: times-to-itimes (a ∗ b) = if ilessp (a, 0) ∨ ilessp (b, 0) then 0

else itimes (a, b) endif

Event: Disable times-to-itimes.

Theorem: quotient-to-iquo (a ÷ b) = if ilessp (a, 0) ∨ ilessp (b, 0) then 0

else iquo (a, b) endif

Event: Disable quotient-to-iquo.

Theorem: zerop-izerop (a ≃ 0) = if ilessp (a, 0) then t

else izerop (a) endif

Event: Disable zerop-izerop.

Theorem: fix-to-fix-int fix (a) = if ilessp (a, 0) then 0

else fix-int (a) endif

Event: Disable fix-to-fix-int.

Theorem: plus-iplus2 (x + y) = if ilessp (x, 0)

then if ilessp (y, 0) then 0 else fix-int (y) endif elseif ilessp (y, 0) then fix-int (x) else iplus (x, y) endif

Event: Disable plus-iplus2.

Theorem: ilessp-lessp (x < y) = if ilessp (x, 0)

then if ilessp (y, 0) then f

else ilessp (0, y) endif else ilessp (x, y) endif

Event: Disable ilessp-lessp.

Theorem: numberp-ilessp (x ∈ N) = ((x = 0) ∨ ilessp (0, x))

Event: Disable numberp-ilessp.

Theorem: gcd-is-igcd gcd (x, y) = if ilessp (x, 0)

then if ilessp (y, 0) then 0

else fix-int (y) endif elseif ilessp (y, 0) then fix-int (x) else igcd (x, y) endif

Event: Disable gcd-is-igcd.

Theorem: negativep-ilessp integerp (x) → (negativep (x) = ilessp (x, 0))

Event: Disable negativep-ilessp.

Theorem: remainder-to-irem (x mod y) = if ilessp (x, 0) then 0

elseif ilessp (y, 0) then fix (x)

else irem (x, y) endif

Event: Disable remainder-to-irem.

Theorem: difference-idifference2 (x − y) = if ilessp (x, 0) then 0

elseif ilessp (y, 0) then fix-int (x)

elseif ilessp (x, y) then 0 else idifference (x, y) endif

Event: Disable difference-idifference2.

Theorem: add1-iplus (1 + x) = if x ∈ N then iplus (1, x)

else 1 endif

Event: Disable add1-iplus.

Event: Let us define the theory nats-to-ints to consist of the following events: add1-iplus, difference-idifference2, remainder-to-irem, negativep-ilessp, gcd-is-igcd, numberp-ilessp, ilessp-lessp, plus-iplus2, fix-to-fix-int, fix-to-fix-int, zeropizerop, quotient-to-iquo, times-to-itimes.

Theorem: times-gcd-fact-proof-1 ((gcd (a, c) = 1) ∧ (gcd (b, d) = 1))

→ (((fix (a) = fix (d)) ∧ (fix (b) = fix (c)))

→ ((a ∗ b) = (c ∗ d)))

Theorem: times-gcd-fact-proof-2-1 ((gcd (a, c) = 1) ∧ (gcd (b, d) = 1) ∧ ((d mod a) = 0)) → (((a ∗ b) = (c ∗ d))

→ ((fix (a) = fix (d)) ∧ (fix (b) = fix (c))))

Theorem: times-gcd-fact-proof-2-2 ((a ∗ b) = (c ∗ d)) → (((c ∗ d) mod a) = 0)

Theorem: times-gcd-fact-proof-2-3 ((gcd (a, c) = 1) ∧ (((c ∗ d) mod a) = 0)) → ((d mod a) = 0)

Theorem: times-gcd-fact-proof-2 ((gcd (a, c) = 1) ∧ (gcd (b, d) = 1)) → (((a ∗ b) = (c ∗ d))

→ ((fix (a) = fix (d)) ∧ (fix (b) = fix (c))))

Theorem: times-gcd-fact-proof ((gcd (a, c) = 1) ∧ (gcd (b, d) = 1)) → (((a ∗ b) = (c ∗ d))

= ((fix (a) = fix (d)) ∧ (fix (b) = fix (c))))

Theorem: times-gcd-fact ((gcd (a, c) = 1) ∧ (gcd (b, d) = 1)) → ((((a ∗ b) = (c ∗ d))

= ((fix (a) = fix (d)) ∧ (fix (b) = fix (c))))

∧ (((b ∗ a) = (c ∗ d))

= ((fix (a) = fix (d)) ∧ (fix (b) = fix (c)))))

;; poor choice of symbols a/c and d/b

Theorem: itimes-igcd-fact-proof ((igcd (a, c) = 1) ∧ (igcd (b, d) = 1) ∧ ilessp (0, b) ∧ ilessp (0, c)) → ((itimes (a, b) = itimes (c, d))

= ((fix-int (a) = fix-int (d)) ∧ (fix-int (b) = fix-int (c))))

Theorem: itimes-igcd-fact ((igcd (a, c) = 1) ∧ (igcd (b, d) = 1) ∧ ilessp (0, b) ∧ ilessp (0, c)) → (((itimes (a, b) = itimes (c, d))

= ((fix-int (a) = fix-int (d)) ∧ (fix-int (b) = fix-int (c)))) ∧ ((itimes (b, a) = itimes (c, d)) = ((fix-int (a) = fix-int (d))

∧ (fix-int (b) = fix-int (c))))

∧ ((itimes (a, b) = itimes (d, c))

= ((fix-int (a) = fix-int (d))

∧ (fix-int (b) = fix-int (c))))

∧ ((itimes (b, a) = itimes (d, c)) = ((fix-int (a) = fix-int (d))

∧ (fix-int (b) = fix-int (c)))))

Theorem: itimes-iquo-general (irem (x, y) = 0) → ((itimes (iquo (x, y), z) = iquo (itimes (x, z), y))

∧ (itimes (z, iquo (x, y)) = iquo (itimes (x, z), y)))

; another copy so that itimes-iquo-general doesn't get fired first

Theorem: itimes-iquo-copy (irem (x, y) = 0) → (itimes (y, iquo (x, y)) = fix-int (x))

Theorem: equal-iquo-iquo ((irem (x, y) = 0) ∧ (irem (z, y) = 0)) → ((iquo (x, y) = iquo (z, y)) = (fix-int (x) = fix-int (z)))

Theorem: idifference-x-x idifference (x, x) = 0

Theorem: irem-iquo-itimes-proof ((irem (a, y) = 0) ∧ (irem (b, z) = 0)) → (irem (iquo (itimes (a, b), y), z) = 0)

Theorem: irem-iquo-itimes ((irem (a, y) = 0) ∧ (irem (b, z) = 0)) → ((irem (iquo (itimes (a, b), y), z) = 0)

∧ (irem (iquo (itimes (b, a), y), z) = 0))

Theorem: equal-irem-itimes-0 ((irem (x, z) = 0) ∨ (irem (y, z) = 0)) → (irem (itimes (x, y), z) = 0)

Theorem: commutativity-of-iquo (irem (a, itimes (b, c)) = 0) → (iquo (iquo (a, c), b) = iquo (iquo (a, b), c))

Theorem: irem-itimes ((irem (x, y) = 0) ∧ (irem (iquo (x, y), z) = 0)) → (irem (x, itimes (y, z)) = 0)

Theorem: iquo-igcd-itimes-proof1 (ilessp (0, b) ∧ ilessp (0, d) ∧ (itimes (a, d) = itimes (b, c))) → ((iquo (a, igcd (a, b)) = iquo (c, igcd (c, d))) = t)

Theorem: iquo-igcd-itimes-proof2 (ilessp (0, b) ∧ ilessp (0, d) ∧ (itimes (a, d) = itimes (b, c))) → ((iquo (b, igcd (a, b)) = iquo (d, igcd (c, d))) = t)

Theorem: iquo-igcd-itimes1 (ilessp (0, b) ∧ ilessp (0, d) ∧ (itimes (a, d) = itimes (b, c))) → ((iquo (a, igcd (a, b)) = iquo (c, igcd (c, d)))

∧ (iquo (b, igcd (a, b)) = iquo (d, igcd (c, d))) ∧ (iquo (a, igcd (b, a)) = iquo (c, igcd (c, d))) ∧ (iquo (b, igcd (b, a)) = iquo (d, igcd (c, d))))

Theorem: iquo-igcd-itimes2 (ilessp (0, b) ∧ ilessp (0, d) ∧ (itimes (d, a) = itimes (b, c))) → ((iquo (a, igcd (a, b)) = iquo (c, igcd (c, d)))

∧ (iquo (b, igcd (a, b)) = iquo (d, igcd (c, d))) ∧ (iquo (a, igcd (b, a)) = iquo (c, igcd (c, d))) ∧ (iquo (b, igcd (b, a)) = iquo (d, igcd (c, d))))

Theorem: iquo-igcd-itimes3 (ilessp (0, b) ∧ ilessp (0, d) ∧ (itimes (a, d) = itimes (c, b))) → ((iquo (a, igcd (a, b)) = iquo (c, igcd (c, d)))

∧ (iquo (b, igcd (a, b)) = iquo (d, igcd (c, d))) ∧ (iquo (a, igcd (b, a)) = iquo (c, igcd (c, d))) ∧ (iquo (b, igcd (b, a)) = iquo (d, igcd (c, d))))

Theorem: equal-iquo-1 (irem (x, y) = 0) → ((iquo (x, y) = 1)

= ((fix-int (x) = fix-int (y)) ∧ (fix-int (x) ≠ 0)

∧ (fix-int (y) ≠ 0)))

#| replaced by below
(prove-lemma equal-x-gcd-x-y (rewrite)
      (implies
       (numberp y)
      (equal
       (equal x (gcd x y))
       (and
        (numberp x)
        (equal (remainder y x) 0))))
      ((enable-theory naturals)))
|#

Theorem: equal-x-igcd-x-y-proof (x = igcd (x, y)) = ((¬ ilessp (x, 0)) ∧ integerp (x) ∧ (irem (y, x) = 0))

Theorem: equal-x-igcd-x-y ((x = igcd (x, y)) = ((¬ ilessp (x, 0)) ∧ integerp (x) ∧ (irem (y, x) = 0))) ∧ ((x = igcd (y, x))

= ((¬ ilessp (x, 0)) ∧ integerp (x) ∧ (irem (y, x) = 0)))

Theorem: ilessp-iplus-igcd (ilessp (0, iplus (x, igcd (x, y))) = (ilessp (0, x) ∨ ((fix-int (x) = 0) ∧ (fix-int (y) ≠ 0)))) ∧ (ilessp (0, iplus (x, igcd (y, x)))

= (ilessp (0, x) ∨ ((fix-int (x) = 0) ∧ (fix-int (y) ≠ 0))))

Theorem: ilessp-iabs-arg1 ilessp (iabs (x), y) = (ilessp (x, y) ∧ ilessp (ineg (x), y))

Theorem: ilessp-iabs-arg2 ilessp (x, iabs (y)) = (ilessp (x, y) ∨ ilessp (x, ineg (y)))

Theorem: igcd-fix-int (igcd (fix-int (x), y) = igcd (x, y)) ∧ (igcd (x, fix-int (y)) = igcd (x, y))

Theorem: iquo-iquo iquo (iquo (a, b), c) = iquo (a, itimes (b, c))

Theorem: iplus-iquo-iquo ((irem (x, z) = 0) ∧ (irem (y, z) = 0)) → (iplus (iquo (x, z), iquo (y, z)) = iquo (iplus (x, y), z))

Theorem: igcd-iquo-iquo ((irem (x, z) = 0) ∧ (irem (y, z) = 0)) → (igcd (iquo (x, z), iquo (y, z)) = iquo (igcd (x, y), iabs (z)))

Theorem: iabs-ineg iabs (ineg (x)) = iabs (x)

Theorem: iquo-ineg (iquo (ineg (x), y) = ineg (iquo (x, y))) ∧ (iquo (x, ineg (y)) = ineg (iquo (x, y)))

Theorem: igcd-ineg (igcd (ineg (x), y) = igcd (x, y)) ∧ (igcd (x, ineg (y)) = igcd (x, y))

Theorem: igcd-0-better (fix-int (x) = 0) → ((igcd (x, y) = iabs (y)) ∧ (igcd (y, x) = iabs (y)))

Theorem: not-integerp-means (¬ integerp (x)) → (fix-int (x) = 0)

Theorem: fix-int-on-non-0 (ilessp (0, x) ∨ ilessp (x, 0)) → (fix-int (x) = x)

Event: Disable fix-int-on-non-0.

Theorem: ilessp-itimes-igcd-hack ilessp (itimes (y, x), igcd (x, z)) = (((fix-int (x) = 0) ∧ (fix-int (z) ≠ 0))

∨ ((fix-int (y) = 0)

∧ ((fix-int (x) ≠ 0) ∨ (fix-int (y) ≠ 0))) ∨ (ilessp (0, x) ∧ ilessp (y, 0)) ∨ (ilessp (0, y) ∧ ilessp (x, 0)))

;;;; a few rules to reduce terms like (irem (itimes ...) (itimes ...))
;;;; note that itimes commutativity rules makes our life simpler

Theorem: irem-0-backchain (irem (b, c) = 0) → (irem (itimes (a, b), c) = 0)

Theorem: irem-itimes-cancel irem (itimes (a, b), itimes (a, c)) = itimes (a, irem (b, c))

Theorem: irem-itimes-base (irem (itimes (a, b), a) = 0) ∧ (irem (itimes (b, a), a) = 0)

Theorem: fix-int-minus fix-int (− x) = if x ≃ 0 then 0

else − x endif

Theorem: iquo-iplus ((irem (x, z) = 0) ∧ (irem (y, z) = 0)) → (iquo (iplus (x, y), z) = iplus (iquo (x, z), iquo (y, z)))

Event: Disable iplus-iquo-iquo.

Theorem: ilessp-0-iplus-open ilessp (0, iplus (x, y)) = ((ilessp (0, x) ∧ ilessp (0, y))

∨ (ilessp (0, x) ∧ ilessp (iabs (y), x)) ∨ (ilessp (0, y) ∧ ilessp (iabs (x), y)))

Theorem: equal-iquo-0 (iquo (x, y) = 0) = (izerop (y) ∨ ilessp (iabs (x), iabs (y)))

Theorem: iabs-open-as-integers iabs (x) = if ilessp (x, 0) then ineg (x)

else fix-int (x) endif

;; doesn't work with correctness-of-cancel-ineg-terms-from-inequality!

Event: Disable iabs-open-as-integers.

Theorem: ilessp-itimes-igcd-hack2 ilessp (itimes (x, y), igcd (x, z)) = (((fix-int (x) = 0) ∧ (fix-int (z) ≠ 0))

∨ ((fix-int (y) = 0)

∧ ((fix-int (x) ≠ 0) ∨ (fix-int (y) ≠ 0))) ∨ (ilessp (0, x) ∧ ilessp (y, 0)) ∨ (ilessp (0, y) ∧ ilessp (x, 0)))

Theorem: ilessp-ineg-igcd-hack ilessp (ineg (itimes (c, y)), igcd (c, d)) = (ilessp (0, itimes (c, y))

∨ ((itimes (c, y) = 0) ∧ ilessp (0, igcd (c, d))))

Theorem: ilessp-iquo (ilessp (0, x) ∧ (irem (y, x) = 0) ∧ (irem (z, x) = 0)) → (ilessp (iquo (y, x), iquo (z, x)) = ilessp (y, z))

Event: Disable ilessp-0-iplus-open.

Theorem: ilessp-minus-0 ilessp (− x, 0) = ilessp (0, x)

Theorem: equal-fix-int-y (fix-int (y) ≠ 0) → (((fix-int (x) = y) = (x = y))

∧ ((y = fix-int (x)) = (y = x)))

Theorem: iabs-fix-int iabs (fix-int (x)) = iabs (x)

Theorem: equal-x-iabs-x (x = iabs (x)) = (integerp (x) ∧ (¬ ilessp (x, 0)))

Theorem: equal-fix-int-iabs (fix-int (x) = iabs (x)) = (¬ ilessp (x, 0))

Theorem: iabs-iabs iabs (iabs (x)) = iabs (x)

Theorem: fix-int-igcd fix-int (igcd (x, y)) = igcd (x, y)

Theorem: not-integerp ((x ∉ N) ∧ (¬ negativep (x))) → (¬ integerp (x))

Theorem: igcd-iplus-ineg (igcd (iplus (x, ineg (y)), z) = igcd (iplus (y, ineg (x)), z)) ∧ (igcd (z, iplus (x, ineg (y))) = igcd (z, iplus (y, ineg (x))))

Theorem: negativep-iplus-ineg (¬ negativep (iplus (x, ineg (y)))) → (negativep (iplus (y, ineg (x))) = (fix-int (x) ≠ fix-int (y)))

Theorem: negativep-iplus-ineg2 negativep (iplus (x, ineg (y))) → (¬ negativep (iplus (y, ineg (x))))

;;; some integer facts needed to prove the rational facts needed
;;; in Bill Young's challenge

Theorem: igcd-iplus-itimes-hack igcd (iplus (itimes (x, y), itimes (x, z)), itimes (x, p)) = itimes (iabs (x), igcd (iplus (y, z), p))

Theorem: iquo-itimes-iabs (irem (y, z) = 0) → (iquo (itimes (x, y), itimes (iabs (x), z))

= if ilessp (x, 0) then ineg (iquo (y, z)) elseif izerop (x) then 0 else iquo (y, z) endif)

Theorem: itimes-2 itimes (2, x) = iplus (x, x)

Theorem: iquo-iplus-itimes-iabs-hack (irem (iplus (y, z), p) = 0) → (iquo (iplus (itimes (x, y), itimes (x, z)), itimes (iabs (x), p))

= if ilessp (x, 0) then ineg (iquo (iplus (y, z), p)) elseif izerop (x) then 0 else iquo (iplus (y, z), p) endif)

Theorem: iabs-0 ((iabs (x) = 0) = (fix-int (x) = 0)) ∧ ((fix-int (x) = 0) → (iabs (x) = 0))

Theorem: ilessp-0-iabs ilessp (0, iabs (x)) = (ilessp (0, x) ∨ ilessp (x, 0))

;; stupid rule
;;(lemma ilessp-neg-pos (rewrite)
;;       (and
;;      (implies
;;       (and
;;        (ilessp 0 x)
;;        (not (ilessp 0 y)))
;;       (ilessp y x))
;;      (implies
;;       (and
;;        (not (ilessp x 0))
;;        (ilessp y 0))
;;       (ilessp y x))
;;      (implies
;;       (and
;;        (not (ilessp x 0))
;;        (not (ilessp 0 y)))
;;       (not (ilessp x y))))
;;       ((enable-theory integer-defns naturals)))
;; should include ilessp-iplus-hacks2 below

Theorem: ilessp-iplus-hacks (((¬ ilessp (0, x)) ∧ (¬ ilessp (0, y))) → (¬ ilessp (0, iplus (x, y)))) ∧ (((¬ ilessp (y, 0)) ∧ ilessp (x, z))

→ (ilessp (x, iplus (y, z)) ∧ ilessp (x, iplus (z, y)))) ∧ (((¬ ilessp (x, 0)) ∧ (¬ ilessp (y, 0)))

→ (¬ ilessp (iplus (x, y), 0))) ∧ ((ilessp (0, x) ∧ (¬ ilessp (y, 0)))

→ (ilessp (0, iplus (x, y)) ∧ ilessp (0, iplus (y, x)))) ∧ (((¬ ilessp (x, 0)) ∧ (¬ ilessp (y, z)))

→ ((¬ ilessp (iplus (y, x), z)) ∧ (¬ ilessp (iplus (x, y), z))))

Theorem: ilessp-iplus-hacks2 (ilessp (x, 0) ∧ (¬ ilessp (0, y))) → (ilessp (iplus (x, y), 0) ∧ ilessp (iplus (y, x), 0))

Theorem: ilessp-iplus-hacks3 ((ilessp (x, 0) ∧ (¬ ilessp (x, y))) → (ilessp (iplus (x, y), 0) ∧ ilessp (iplus (y, x), 0))) ∧ ((ilessp (0, x) ∧ (¬ ilessp (y, x)))

→ (ilessp (0, iplus (x, y)) ∧ ilessp (0, iplus (y, x)))) ∧ ((ilessp (x, y) ∧ (¬ ilessp (0, y)))

→ (ilessp (iplus (x, y), 0) ∧ ilessp (iplus (y, x), 0))) ∧ ((ilessp (y, x) ∧ (¬ ilessp (y, 0)))

→ (ilessp (0, iplus (x, y)) ∧ ilessp (0, iplus (y, x))))

Theorem: ilessp-itimes-itimes-instance ilessp (itimes (x, z), itimes (y, z)) = ((ilessp (0, z) ∧ ilessp (x, y)) ∨ (ilessp (z, 0) ∧ ilessp (y, x)))

; doesn't work yet (needed below?)
;(prove-lemma ilessp-itimes-iquo (rewrite)
;            (implies
;             (and
;              (equal (irem w vw) 0)
;              (equal (irem v vw) 0))
;            (equal
;             (ilessp (itimes d (iquo w vw))
;                     (itimes c (iquo v vw)))
;             (and
;              (not (equal (fix-int vw) 0))
;              (if (ilessp vw 0)
;                  (ilessp (itimes c v) (itimes d w))
;                (ilessp (itimes d w) (itimes c v))))))
;            ((disable ilessp-0-iplus irem-is-my-irem
;                      CORRECTNESS-OF-CANCEL-ITIMES-ILESSP-FACTORS
;                      CORRECTNESS-OF-CANCEL-ITIMES-ILESSP
;                      CORRECTNESS-OF-CANCEL-ITIMES-FACTORS)
;             (enable-theory integers)
;             (enable ilessp-trichotomy *1*fix-int iquo-0-arg-better
;                     itimes-iquo)
;             (use (ilessp-itimes-itimes-instance
;                   (z vw) (x (itimes d (iquo w vw)))
;                   (y (itimes c (iquo v vw)))))))
;
;; not working yet
;(prove-lemma rlessp-simple-rplus-reduce-proof (rewrite)

;       (equal
;       (rlessp x (simple-rplus (reduce y) z))
;       (rlessp x (simple-rplus y z)))
;       ((enable-theory rational-defns integers naturals)
;       (enable *1*itimes *1*ilessp *1*iplus *1*integerp
;               *1*fix-int *1*ilessp *1*integerp igcd-non-negative
;               ilessp-0-iquo ilessp-0-igcd iabs-igcd iabs-simplify
;               ilessp-igcd ilessp-trichotomy fix-int-igcd
;               equal-igcd-0
;               izerop negativep-ilessp fix-to-fix-int)
;       (disable ilessp-0-iplus)))
;

Theorem: ilessp-0-iplus-x-x ilessp (0, iplus (x, x)) = ilessp (0, x)

Theorem: ilessp-iplus-x-x-0 ilessp (iplus (x, x), 0) = ilessp (x, 0)

Theorem: iquo-x-iabs-x (iquo (x, iabs (x)) = if fix-int (x) = 0 then 0

elseif ilessp (x, 0) then -1 else 1 endif)

∧ (iquo (iabs (x), x)

= if fix-int (x) = 0 then 0 elseif ilessp (x, 0) then -1 else 1 endif)

Theorem: nintegerp-ilessp (¬ integerp (x)) → ((ilessp (x, y) = ilessp (0, y)) ∧ (ilessp (y, x) = ilessp (y, 0)))

Theorem: ilessp-x-igcd-x (ilessp (x, igcd (x, y)) = (ilessp (x, 0) ∨ ((fix-int (x) = 0) ∧ (fix-int (y) ≠ 0)))) ∧ (ilessp (x, igcd (y, x))

= (ilessp (x, 0) ∨ ((fix-int (x) = 0) ∧ (fix-int (y) ≠ 0))))

Theorem: ilessp-trans-hack (fix-int (x) = y) → ((ilessp (x, z) = ilessp (y, z)) ∧ (ilessp (z, x) = ilessp (z, y)))

Theorem: commutativity-of-itimes-iquo ((irem (w, x) = 0) ∧ (irem (d, x) = 0)) → (itimes (d, iquo (w, x)) = itimes (w, iquo (d, x)))

Theorem: ilessp-equal-trans-special-case ((fix-int (y) = x) ∧ (fix-int (x) = 0)) → ((ilessp (y, z) = ilessp (0, z)) ∧ (ilessp (z, y) = ilessp (z, 0)))

; ---------- Final DEFTHEORY event ----------
;; I'll go ahead and include iplus-list and itimes-list and lemmas
;; about them that were developed.
;; I've left out ILESSP-TRICHOTOMY because I'm scared it will slow
;; things down too much.  But it certainly represents useful
;; information.
;; MMW put ILESSP-TRICHOTOMY back because his experience with
;; rationals suggests that it gets used all the time. 1-10-91
;; We'll see how it goes.

Event: Let us define the theory integers to consist of the following events: ileq, idifference, integerp-fix-int, integerp-iplus, integerp-idifference, integerpineg, integerp-iabs, integerp-itimes, fix-int-remover, fix-int-fix-int, fix-int-iplus, fix-int-idifference, fix-int-ineg, fix-int-iabs, fix-int-itimes, ineg-iplus, ineg-ineg, ineg-fix-int, ineg-of-non-integerp, ineg-0, iplus-left-id, iplus-right-id, iplus-0-left, iplus-0-right, commutativity2-of-iplus, commutativity-of-iplus, associativity-of-iplus, iplus-cancellation-1, iplus-cancellation-2, iplus-ineg1, iplus-ineg2, iplusfix-int1, iplus-fix-int2, idifference-fix-int1, idifference-fix-int2, iplus-list, eval$- list-append, iplus-list-append, iplus-ineg3, iplus-ineg4, correctness-of-cancel-iplus, ilessp-fix-int-1, ilessp-fix-int-2, iplus-cancellation-1-for-ilessp, iplus-cancellation-2-for-ilessp, correctness-of-cancel-iplus-ilessp, itimes-0-left, itimes-0-right, itimesfix-int1, itimes-fix-int2, commutativity-of-itimes, itimes-distributes-over-iplus-proof, itimes-distributes-over-iplus, commutativity2-of-itimes, associativity-of-itimes, equal-itimes-0, equal-itimes-1, equal-itimes-minus-1, itimes-1-arg1, quotientremainder-uniqueness, division-theorem, itimes-ineg-1, itimes-ineg-2, itimes-cancellation-1, itimes-cancellation-2, itimes-cancellation-3, integerp-iquotient, integerp-iremainder, integerp-idiv, integerp-imod, integerp-iquo, integerp-irem, iquotient-fix-int1, iquotientfix-int2, iremainder-fix-int1, iremainder-fix-int2, idiv-fix-int1, idiv-fix-int2, imodfix-int1, imod-fix-int2, iquo-fix-int1, iquo-fix-int2, irem-fix-int1, irem-fix-int2, fix-int-iquotient, fix-int-iremainder, fix-int-idiv, fix-int-imod, fix-int-iquo, fixint-irem, itimes-list, itimes-list-append, member-append, equal-fix-int, subsetp, correctness-of-cancel-itimes, ilessp-trichotomy, correctness-of-cancel-itimes-ilessp, ilessp-strict, eval$-list-cons, eval$-list-nlistp, eval$-litatom, eval$-quote, eval$- other, iplus-x-y-ineg-x, correctness-of-cancel-ineg, integerp-iplus-list, eval$-iplus-list-delete, eval$-iplus-list-bagdiff, itimes-tree-ineg, itimes-factors, itimes–1, equalineg-ineg, ilessp-ineg-ineg, fix-int-eval$-itimes-tree-rec, eval$-itimes-tree-ineg, inegeval$-itimes-tree-ineg, iplus-eval$-itimes-tree-ineg, itimes-eval$-itimes-tree-ineg, iplus-or-itimes-term, cancel-itimes-factors, cancel-itimes-factors-expanded, cancelitimes-factors-expanded-cancel-itimes-factors, membership-of-0-implies-itimes-list-is-0, member-0-eval$-list, correctness-of-cancel-itimes-factors, cancel-itimes-ilessp-factors, bagint-singleton, ilessp-itimes-list-eval$-list-bagdiff, ilessp-itimes-list-eval$- list-bagdiff-corollary-1, member-0-itimes-factors-yields-0, member-0-itimes-factors-yields-0-ilessp-consequence-1, member-0-itimes-factors-yields-0-ilessp-consequence-2, ilessp-itimes-list-eval$-list-bagdiff-corollary-2, correctness-of-cancel-itimes-ilessp-factors, disjoin-equalities-with-0, cancel-factors-0, some-eval$s-to-0, eval$-disjoin-equalities-with-0, some-eval$s-to-0-append, some-eval$s-to-0-eliminator, correctnessof-cancel-factors-0, correctness-of-cancel-factors-ilessp-0, conjoin-inequalities-with-0, split-out-ineg-terms, correctness-of-cancel-ineg-terms-from-equality, correctnessof-cancel-ineg-terms-from-inequality, iplus-constants, cancel-constants-equal, ilesspadd1, ilessp-add1-iplus, cancel-constants-ilessp, ilessp-irem, irem-noop, iremof-0, irem-iquo-elim, irem-iplus-0, integerp-igcd, commutativity-of-igcd, igcd-0, igcd-1, equal-igcd-0, igcd-non-negative, ilessp-igcd, igcd-iplus, irem-igcd, distributivityof-itimes-over-igcd, common-divisor-divides-igcd, iabs-igcd, associativity-of-igcd, commutativity2-of-igcd, igcd-x-x, igcd-idempotence, iquo-0, ilessp-0-iquo, iabssimplify, igcd-iquo-igcd-proof, ilessp-iquo-0, iquo-1, ilessp-0-igcd, igcd-minus, itimes-iquo, iquo-x-x, iquo-0-arg-better, itimes-iquotient, iquotient-0, iremainder-0, irem-0-iremainder-0, equal-itimes-x-x, itimes-igcd-fact, itimes-iquo-general, itimes-iquo-copy, equal-iquo-iquo, idifference-x-x, irem-iquo-itimes, equal-irem-itimes-0, commutativity-of-iquo, irem-itimes, iquo-igcd-itimes1, iquo-igcd-itimes2, iquo-igcd-itimes3, equal-iquo-1, equal-x-igcd-x-y, ilessp-iplus-igcd, ilessp-iabs-arg1, ilessp-iabs-arg2, igcd-fix-int, iquo-iquo, igcd-iquo-iquo, iabs-ineg, iquoineg, igcd-ineg, igcd-0-better, not-integerp-means, ilessp-itimes-igcd-hack, irem-0-backchain, irem-itimes-cancel, irem-itimes-base, fix-int-minus, iquo-iplus, equaliquo-0, ilessp-iquo, ilessp-minus-0, equal-fix-int-y, iabs-fix-int, equal-x-iabs-x, equal-fix-int-iabs, iabs-iabs, fix-int-igcd, not-integerp, igcd-iplus-ineg, negativepiplus-ineg, negativep-iplus-ineg2, igcd-iplus-itimes-hack, iquo-itimes-iabs, itimes-2, iquo-iplus-itimes-iabs-hack, iabs-0, ilessp-0-iabs, ilessp-iplus-hacks, ilessp-iplus-hacks2, ilessp-iplus-hacks3, ilessp-0-iplus-x-x, ilessp-iplus-x-x-0, iquo-x-iabs-x, nintegerp-ilessp, ilessp-x-igcd-x, commutativity-of-itimes-iquo, izerop, *1*integerp, *1*fix-int, *1*ilessp, *1*iplus, *1*ineg, *1*iabs, *1*itimes, *1*iquotient, *1*iremainder, *1*idiv, *1*imod, *1*iquo, *1*irem, *1*ileq, *1*idifference, *1*izerop, *1*igcd.

Event: Disable iplus-irem-itimes-iquo.

Event: Disable irem-is-my-irem.

Event: Disable iquo-0-arg.

Event: Disable itimes-hack1. Event: Disable itimes-hack2. Event: Disable gcd-factors-gives-linear-combination. Event: Disable gcd-factors-gives-linear-combination-rewrite. Event: Disable remainder-0-sufficiency. Event: Disable itimes-iplus-hack. Event: Disable irem-0-iremainder-0-help1. Event: Disable irem-0-iremainder-0-help2. Event: Disable divides-product-reduction-helper. Event: Disable divides-product-reduction. Event: Disable divides-each-equality. Event: Disable times-gcd-fact. Event: Disable iplus-iquo-iquo. Event: Disable fix-int-on-non-0. Event: Disable iabs-open-as-integers. Event: Disable ilessp-itimes-igcd-hack2. Event: Disable ilessp-ineg-igcd-hack. Event: Disable ilessp-itimes-itimes-instance.

Event: Disable ilessp-trans-hack. Event: Disable ilessp-equal-trans-special-case. Event: Enable izerop. Event: Make the library "integers" and compile it.

Index

add1-iplus, 87 associativity-of-igcd, 81 associativity-of-iplus, 10 associativity-of-itimes, 26

bagdiff, 19–21, 23–25, 34, 36, 37,

39–43, 47, 60, 61, 63 bagint, 18–20, 23–25, 35, 39–42, 47,

50, 61, 62, 64, 65 bagint-singleton, 62

cancel-constants-equal, 78 cancel-constants-equal-lemma, 78 cancel-constants-ilessp, 78 cancel-constants-ilessp-lemma-1, 78 cancel-constants-ilessp-lemma-2, 78 cancel-factors-0, 66, 67 cancel-factors-ilessp-0, 67, 68 cancel-ineg, 14, 16 cancel-ineg-aux, 12–16 cancel-ineg-terms-from-equality, 71,

74 -cancel-ineg-terms-from-equality-

expanded, 74 -expanded, 71, 74, 75

cancel-ineg-terms-from-inequalit y, 75, 77 y-cancel-ineg-terms-from-inequality-

expanded, 77 y-expanded, 75, 77

cancel-iplus, 18, 20, 22 cancel-iplus-ilessp, 25 cancel-iplus-ilessp-1, 23, 24 cancel-itimes, 35, 40 cancel-itimes-factors, 50, 60 cancel-itimes-factors-expanded, 60, 61 cancel-itimes-factors-expanded-

cancel-itimes-factors, 60 cancel-itimes-ilessp, 41, 43 cancel-itimes-ilessp-factors, 61, 65 common-divisor-divides-igcd, 81 commutativity-of-igcd, 80 commutativity-of-iplus, 10 commutativity-of-iquo, 89 commutativity-of-itimes, 26 commutativity-of-itimes-iquo, 97 commutativity2-of-igcd, 81 commutativity2-of-iplus, 10 commutativity2-of-itimes, 26 conjoin-inequalities-with-0, 67, 68 conjoin-inequalities-with-0-eli

minator, 68 correctness-of-cancel-factors-0, 67 correctness-of-cancel-factors-i

lessp-0, 68 correctness-of-cancel-ineg, 16 correctness-of-cancel-ineg-aux, 16 correctness-of-cancel-ineg-term s-from-equality, 75 s-from-inequality, 77 correctness-of-cancel-iplus, 22 correctness-of-cancel-iplus-ile

ssp, 25

ssp-lemma, 24 correctness-of-cancel-itimes, 40 correctness-of-cancel-itimes-fa

ctors, 61 correctness-of-cancel-itimes-ha

ck-1, 37 ck-2, 39 ck-3, 39 ck-3-lemma, 39

correctness-of-cancel-itimes-ile ssp, 43 ssp-factors, 65 ssp-hack-1, 42 ssp-hack-2, 42 ssp-hack-2-lemma, 42 ssp-hack-3, 43 ssp-hack-3-lemma-1, 42 ssp-hack-3-lemma-2, 43 ssp-hack-4, 43 delete, 19–21, 36–38, 60, 62 difference-idifference, 78 difference-idifference2, 87 disjoin-equalities-with-0, 65, 66 distributivity-of-itimes-over-i

gcd, 81 gcd-proof, 81

divides-each-equality, 85 divides-product-reduction, 85 divides-product-reduction-helpe

r, 85 r-1, 85

division-theorem, 27 division-theorem-for-truncate-t

o-neginf, 28 o-neginf-part1, 28 o-neginf-part2, 28 o-neginf-part3, 28 o-zero, 29 o-zero-part1, 29 o-zero-part2, 29 o-zero-part3, 29

division-theorem-part1, 27 division-theorem-part2, 27 division-theorem-part3, 27

equal-0-itimes-list-eval$-bagi nt-1, 39 nt-2, 39

equal-fix-int, 38 equal-fix-int-iabs, 94 equal-fix-int-to-ilessp, 65 equal-fix-int-y, 93 equal-igcd-0, 80 equal-ineg-ineg, 48 equal-iquo-0, 93 equal-iquo-1, 90 equal-iquo-iquo, 89 equal-irem-itimes-0, 89 equal-itimes-0, 26 equal-itimes-1, 26 equal-itimes-list-eval$-list-b

agdiff, 60 equal-itimes-list-eval$-list-de lete, 37 lete-new-1, 60 lete-new-2, 60

equal-itimes-minus-1, 26 equal-itimes-x-x, 84 equal-x-iabs-x, 94 equal-x-igcd-x-y, 91 equal-x-igcd-x-y-proof, 91 eval$-cancel-ineg-aux-fn, 15, 16 eval$-cancel-ineg-aux-is-its-f

n, 15 eval$-cancel-iplus, 20 eval$-disjoin-equalities-with-

0, 66 eval$-equal-itimes-tree-itimes

-fringe-0, 38 eval$-ilessp-iplus-tree-no-fix

-int, 24 eval$-iplus, 22 eval$-iplus-list-bagdiff, 21 eval$-iplus-list-car-remove-ine

gs, 74 eval$-iplus-list-cdr-remove-ine

gs, 74 eval$-iplus-list-delete, 21 eval$-iplus-tree, 17 eval$-iplus-tree-rec, 17 eval$-itimes-tree, 33 eval$-itimes-tree-ineg, 48 eval$-itimes-tree-no-fix-int-1, 40 eval$-itimes-tree-no-fix-int-2, 40 eval$-itimes-tree-rec, 33 eval$-list-append, 17 eval$-list-bagint-0, 61 eval$-list-bagint-0-for-ilessp, 64 eval$-list-bagint-0-implies-eq

ual, 61

ual-for-ilessp, 65

ual-for-ilessp-lemma, 65 eval$-list-cons, 14 eval$-list-nlistp, 14 eval$-litatom, 14 eval$-make-cancel-itimes-equalit

y, 37 y-1, 38 y-2, 38

eval$-make-cancel-itimes-inequ

ality, 41 eval$-other, 14

fix-int, 5–11, 15, 16, 21–23, 25, 26, 30–32, 36–39, 42, 43, 48, 60–62, 64–66, 78–84, 86– 95, 97, 98

fix-int-eval$-itimes-tree-rec, 48 fix-int-fix-int, 9 fix-int-iabs, 9 fix-int-idifference, 9 fix-int-idiv, 31 fix-int-igcd, 94 fix-int-imod, 32 fix-int-ineg, 9 fix-int-iplus, 9 fix-int-iquo, 32 fix-int-iquotient, 31 fix-int-irem, 32 fix-int-iremainder, 31 fix-int-itimes, 9 fix-int-minus, 92 fix-int-on-non-0, 92 fix-int-remover, 9 fix-to-fix-int, 86

gcd, 80, 84–88 gcd-factors, 83, 84 gcd-factors-accept, 83 gcd-factors-gives-linear-combin

ation, 84 ation-rewrite, 84

gcd-is-igcd, 86 gcd-remainder-times-fact1-proof, 85

-non-numberp-case, 85 -numberp-case, 85

iabs, 6, 8, 9, 27–30, 79–82, 91–95,

97 iabs-0, 95 iabs-fix-int, 94 iabs-iabs, 94 iabs-igcd, 81 iabs-ineg, 91 iabs-open-as-integers, 93 iabs-simplify, 81 idifference, 6–9, 11, 21, 78, 83, 87,

89 idifference-fix-int1, 11 idifference-fix-int2, 11 idifference-x-x, 89 idiv, 7, 28–31 idiv-fix-int1, 31 idiv-fix-int2, 31 idiv-imod-uniqueness, 28 igcd, 80–83, 87–94, 97 igcd-0, 80 igcd-0-better, 92 igcd-1, 80 igcd-fix-int, 91 igcd-idempotence, 81 igcd-ineg, 91 igcd-iplus, 80 igcd-iplus-ineg, 94 igcd-iplus-instance-proof, 80 igcd-iplus-itimes-hack, 94 igcd-iquo-igcd-proof, 81 igcd-iquo-iquo, 91 igcd-minus, 82 igcd-non-negative, 80 igcd-x-x, 81 ileq, 6 ilessp, 6, 23, 24, 27–30, 40–43, 48,

62–65, 68, 78–82, 85–98 ilessp-0-iabs, 95 ilessp-0-igcd, 82 ilessp-0-iplus-open, 93 ilessp-0-iplus-x-x, 97 ilessp-0-iquo, 81 ilessp-0-itimes, 63 ilessp-add1, 78 ilessp-add1-iplus, 78 ilessp-equal-trans-special-case, 98 ilessp-fix-int-1, 23 ilessp-fix-int-2, 23 ilessp-iabs-arg1, 91 ilessp-iabs-arg2, 91 ilessp-igcd, 80 ilessp-ineg-igcd-hack, 93 ilessp-ineg-ineg, 48 ilessp-iplus-hacks, 95 ilessp-iplus-hacks2, 96 ilessp-iplus-hacks3, 96 ilessp-iplus-igcd, 91 ilessp-iplus-x-x-0, 97 ilessp-iquo, 93 ilessp-iquo-0, 82 ilessp-irem, 79 ilessp-itimes-0, 63 ilessp-itimes-igcd-hack, 92 ilessp-itimes-igcd-hack2, 93 ilessp-itimes-itimes-instance, 96 ilessp-itimes-list-eval$-list-

bagdiff, 63 bagdiff-corollary-1, 63 bagdiff-corollary-2, 63 delete, 62 delete-helper-1, 62 delete-helper-2, 62 delete-prime, 62 delete-prime-helper-1, 62 delete-prime-helper-2, 62

ilessp-itimes-right-negative, 43 ilessp-itimes-right-positive, 42 ilessp-lessp, 86 ilessp-minus-0, 93 ilessp-strict, 43 ilessp-trans-hack, 97 ilessp-trichotomy, 42 ilessp-x-igcd-x, 97 ilessp-zero-implies-not-equal, 63 imod, 7, 28–32 imod-fix-int1, 31 imod-fix-int2, 31 ineg, 6, 8–11, 15, 16, 21, 22, 29, 30,

47, 48, 75, 79, 91, 93–95 ineg-0, 10 ineg-eval$-itimes-tree-ineg, 48 ineg-fix-int, 9 ineg-ineg, 9 ineg-iplus, 9 ineg-of-non-integerp, 9 integer-defns, 8 integerp, 5, 8–10, 17, 20–22, 27–31,

33, 36–38, 60, 61, 67, 74, 78–80, 82, 84, 87, 91, 92, 94, 97

integerp-eval$-iplus-or-ineg-te

rm, 74 integerp-eval$-itimes, 36 integerp-fix-int, 8 integerp-iabs, 8 integerp-idifference, 8 integerp-idiv, 30 integerp-igcd, 80 integerp-imod, 30 integerp-ineg, 8 integerp-iplus, 8 integerp-iplus-list, 17 integerp-iquo, 30 integerp-iquotient, 30 integerp-irem, 31 integerp-iremainder, 30 integerp-itimes, 9 integerp-itimes-list, 33 integers, 99 iplus, 6, 8–11, 15–17, 21, 22, 24, 26–

30, 48, 74, 75, 78–80, 84, 86, 87, 91–97

iplus-0-left, 10 iplus-0-right, 10 iplus-cancellation-1, 10 iplus-cancellation-1-for-ilessp, 24 iplus-cancellation-2, 10 iplus-cancellation-2-for-ilessp, 24 iplus-constants, 78 iplus-eval$-itimes-tree-ineg, 48 iplus-fix-int1, 11 iplus-fix-int2, 11 iplus-fringe, 16, 18–21, 23, 25, 70–

77 iplus-ineg-promote, 15 iplus-ineg1, 11 iplus-ineg2, 11 iplus-ineg3, 15 iplus-ineg4, 15 iplus-ineg5, 22 iplus-ineg5-lemma-1, 21 iplus-ineg5-lemma-2, 22 iplus-ineg6, 22 iplus-ineg7, 22 iplus-iquo-iquo, 91 iplus-irem-itimes-iquo, 79 iplus-left-id, 10 iplus-list, 17, 20, 21, 74, 75 iplus-list-append, 21 iplus-list-eval$-car-split-out

-ineg-terms, 75 iplus-list-eval$-fringe, 21 iplus-or-ineg-term, 70, 71, 74, 75 iplus-or-itimes-term, 49, 50, 61 iplus-or-itimes-term-integerp-ev

al$, 61 iplus-right-id, 10 iplus-tree, 17, 19, 20, 23, 24, 71–77 iplus-tree-no-fix-int, 24, 25 iplus-tree-rec, 17, 24 iplus-x-y-ineg-x, 16 iquo, 7, 29–32, 79, 81–83, 85, 89–95,

97 iquo-0, 81 iquo-0-arg, 82 iquo-0-arg-better, 83 iquo-1, 82 iquo-fix-int1, 31 iquo-fix-int2, 31 iquo-igcd-itimes-proof1, 89 iquo-igcd-itimes-proof2, 90 iquo-igcd-itimes1, 90 iquo-igcd-itimes2, 90 iquo-igcd-itimes3, 90 iquo-ineg, 91 iquo-iplus, 92 iquo-iplus-itimes-iabs-hack, 95 iquo-iquo, 91 iquo-irem-uniqueness, 29 iquo-itimes-iabs, 94 iquo-x-iabs-x, 97 iquo-x-x, 83 iquotient, 7, 27, 28, 30, 31, 84 iquotient-0, 84 iquotient-fix-int1, 31 iquotient-fix-int2, 31 iquotient-iremainder-uniqueness, 27 irem, 7, 29–32, 79–84, 87, 89–95, 97 irem-0-backchain, 92 irem-0-iremainder-0, 84 irem-0-iremainder-0-help1, 84 irem-0-iremainder-0-help2, 84 irem-fix-int1, 31 irem-fix-int2, 31 irem-igcd, 80 irem-iplus-0, 80 irem-iplus-0-proof, 79 irem-iquo-elim, 79 irem-iquo-itimes, 89 irem-iquo-itimes-proof, 89 irem-is-my-irem, 79 irem-itimes, 89 irem-itimes-base, 92 irem-itimes-cancel, 92 irem-noop, 79 irem-of-0, 79 iremainder, 7, 27, 28, 30, 31, 84, 85 iremainder-0, 84 iremainder-fix-int1, 31 iremainder-fix-int2, 31 itimes, 6, 7, 9, 25–30, 33, 36, 37, 39,

42, 43, 47, 48, 60–63, 79, 81–85, 88–97

itimes–1, 47 itimes-0-left, 25 itimes-0-right, 26 itimes-1-arg1, 26 itimes-2, 94 itimes-cancellation-1, 30 itimes-cancellation-2, 30 itimes-cancellation-3, 30 itimes-distributes-over-iplus, 26 itimes-distributes-over-iplus-p

roof, 26 itimes-eval$-itimes-tree-ineg, 48 itimes-factors, 47, 50, 61, 63–68 itimes-fix-int1, 26 itimes-fix-int2, 26 itimes-fringe, 33, 35–43 itimes-hack1, 82 itimes-hack1-1, 82 itimes-hack1-1-1, 82 itimes-hack1-2, 82 itimes-hack1-2-1, 82 itimes-hack2, 83 itimes-igcd-fact, 88 itimes-igcd-fact-proof, 88 itimes-ineg-1, 30 itimes-ineg-2, 30 itimes-iplus-hack, 84 itimes-iquo, 82 itimes-iquo-copy, 89 itimes-iquo-general, 89 itimes-iquotient, 84 itimes-itimes-list-eval$-list-

delete, 60 itimes-list, 33, 36–40, 42, 43, 48, 60–

66, 68 itimes-list-append, 36 itimes-list-bagdiff, 36 itimes-list-eval$-delete, 36 itimes-list-eval$-factors, 61 itimes-list-eval$-factors-lemm

a, 61

a-prime, 61 itimes-list-eval$-fringe, 36 itimes-list-eval$-list-0, 42 itimes-tree, 33, 34, 37–40 itimes-tree-ineg, 47, 48 itimes-tree-no-fix-int, 40–42 itimes-tree-rec, 33, 40, 47, 48 itimes-zero1, 25 itimes-zero2, 25 izerop, 5, 79, 82, 83, 86, 93–95 izerop-eval-of-member-implies-iti

mes-list-0, 38 izerop-ilessp-0-relationship, 62 lessp-count-listp-cdr, 17 lessp-difference-plus-arg1, 23 lessp-difference-plus-arg1-comm

uted, 23 listp-bagint-with-singleton-imp

lies-member, 42 listp-bagint-with-singleton-mem

ber, 42 listp-cdr-factors-implies-intege

rp, 67

make-cancel-ineg-terms-equality, 70,

71 make-cancel-ineg-terms-inequalit

y, 75 make-cancel-iplus-inequality-1, 23, 24 make-cancel-iplus-inequality-si

mplifier, 24 make-cancel-itimes-equality, 34–38,

50 make-cancel-itimes-inequality, 40, 41,

61 member-0-eval$-list, 60 member-0-itimes-factors-yields-0-ilessp-consequence-1, 64 0-ilessp-consequence-2, 64 0, 63

member-append, 37

member-izerop-itimes-fringe, 37 membership-of-0-implies-itimes-

list-is-0, 60 minus-ineg, 75 my-irem, 79

nats-to-ints, 87 negativep-ilessp, 87 negativep-iplus-ineg, 94 negativep-iplus-ineg2, 94 nintegerp-ilessp, 97 not-integerp, 94 not-integerp-implies-not-equal-ip

lus, 21 not-integerp-implies-not-equal-iti

mes, 36 not-integerp-means, 92 numberp-ilessp, 86 numberp-is-integerp, 78

plus-iplus, 78 plus-iplus2, 86

quotient-difference-lessp-arg2, 27 quotient-remainder-uniqueness, 27 quotient-to-iquo, 85

remainder-0-sufficiency, 84 remainder-to-irem, 87 remove-inegs, 70–77

same-fix-int-implies-not-ilessp, 43 some-eval$s-to-0, 66 some-eval$s-to-0-append, 66 some-eval$s-to-0-eliminator, 66 split-out-ineg-terms, 70, 74, 75 subbagp, 21, 36, 38, 42, 43, 60, 63 subbagp-subsetp, 38 subsetp, 38, 42, 43 subsetp-implies-itimes-list-eva

l$-equals-0, 38

times-gcd-fact, 88 times-gcd-fact-proof, 88 times-gcd-fact-proof-1, 87 times-gcd-fact-proof-2, 88 times-gcd-fact-proof-2-1, 88 times-gcd-fact-proof-2-2, 88 times-gcd-fact-proof-2-3, 88 times-to-itimes, 85

zero-ilessp-implies-not-equal, 63 zerop-izerop, 86