File: modularithmetic-98.events

package info (click to toggle)
acl2 8.5dfsg-5
links: PTS
area: main
in suites: bookworm
size: 991,452 kB
sloc: lisp: 15,567,759; javascript: 22,820; cpp: 13,929; ansic: 12,092; perl: 7,150; java: 4,405; xml: 3,884; makefile: 3,507; sh: 3,187; ruby: 2,633; ml: 763; python: 746; yacc: 723; awk: 295; csh: 186; php: 171; lex: 154; tcl: 49; asm: 23; haskell: 17
file content (5211 lines) | stat: -rw-r--r-- 192,610 bytes
(boot-strap nqthm)

;;; requires 17 minutes to prove-file on a 300MHZ Pentium II.

;;; Should look carefully at including extra lemmas for situations in which
;;; automatic disabling is used.  Many of the present lemmas assume normal
;;; forms which are only present when "canonical" lemmas are not disabled.

;;; This file contains a modular arithmetic library for nqthm-1992.  Lemmas
;;; within this file fall into two classes:  those commented "canonical,"
;;; which rewrite expressions to canonical form; and those uncommented, which
;;; simplify expressions already in canonical form.  A nesting order for
;;; function calls is established, and rewrite rules are provided which
;;; rewrite out of order expressions into the established nesting order.
;;; Because opening a function definition in effect behaves as a rewrite rule,
;;; the nesting order is constrained by existing function definitions.
;;; For example,

;;;      (plus x y) = (if (zerop x)
;;;                       (fix y)
;;;                       (add1 (plus (sub1 x) y)))

;;; places add1 outside of plus, and sub1 inside of plus.  Thus the nesting
;;; order must place add1, plus and sub1 in that order.  Among all orders
;;; satisfying these constraints, we choose the following:

;;; add1 plus times remainder quotient difference sub1

;;; Since nqthm applies lemmas in reverse chronological order, we place the
;;; more costly rules early in this file.

;;; The following lemma is costly, because as a linear rule it is applied
;;; before (remainder a b) is simplified.  Thus (remainder a b) is simplified
;;; twice for remainder-lessp-linear, and then again each time it occurs
;;; within the target formula.

(prove-lemma remainder-lessp-linear (rewrite)
  (and (implies (and (numberp b)
                     (not (equal b 0)))
                (lessp (remainder a b) b))
       (not (lessp a (remainder a b)))))

;;; canonical

(prove-lemma times-add1 (rewrite)
  (and (equal (times a (add1 b))
              (plus a (times a b)))
       (equal (times (add1 a) b)
              (plus b (times a b)))))

(prove-lemma times-zerop (rewrite)
  (implies (not (numberp b))
           (equal (times a b) 0)))

(prove-lemma times-0 (rewrite)
  (and (equal (times a 0) 0)
       (equal (times 0 a) 0)))

;;; We begin by removing times, remainder and quotient from within difference.

(prove-lemma quotient-remainder (elim)
  (implies (and (numberp a)
; do not eliminate destructors when b is 0
                (numberp b)
                (not (equal b 0)))
           (equal (plus (remainder a b)
                        (times b (quotient a b)))
                  a)))

(prove-lemma quotient-remainder-generalize (generalize)
  (implies (and (numberp b)
                (not (equal b 0)))
           (lessp (remainder a b) b)))

;;; We omit the commutative version because it will not occur after
;;; plus-commutes-meta is proven.

(prove-lemma quotient-remainder-rewrite (rewrite)
  (equal (plus (remainder a b)
               (times b (quotient a b)))
         (if (numberp a) a 0)))


(defn diff-times-ind (a b c)
  (if (lessp c a)
      0
    (if (zerop b)
        0
      (diff-times-ind a (sub1 b) (difference c a)))))

;;; canonical

;;; The following rule introduces (quotient c a) and (remainder c a) in cases
;;; where destructor elimination may not apply.  For this reason its
;;; application is discouraged by making the rule conditional on c < a*b.

(prove-lemma difference-times-arg1 (rewrite)
  (implies (lessp c (times a b))
           (equal (difference (times a b) c)
                  (plus (difference a (remainder c a))
                        (times a (difference
                                  (sub1 b)
                                  (quotient c a))))))
  ((induct (diff-times-ind a b c))))

(defn diff-times-1 (a)
  (if (and (equal (car a) 'difference)
           (equal (caadr a) 'times)
           (litatom (caddr a)))
      `(if (lessp ,(caddr a) ,(cadr a))
           (plus (difference ,(cadadr a) (remainder ,(caddr a) ,(cadadr a)))
                 (times ,(cadadr a)
                        (difference (sub1 ,(caddadr a))
                                    (quotient ,(caddr a) ,(cadadr a)))))
         (zero))
    a))

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

;;; The following meta rule rewrites a*b - c only in cases where c is a litatom.
;;; This assures that (quotient c a) and (remainder c a) will eventually be
;;; candidates for destructor elimination.

;;; canonical

(prove-lemma difference-times-arg1-meta ((meta difference))
  (equal (eval$ t a y)
         (eval$ t (diff-times-1 a) y)))

;;; canonical

(prove-lemma difference-times-arg1-simpler (rewrite)
  (implies (and (lessp c (plus a b))
                (numberp a)
                (not (equal a 0))
                (numberp b)
                (not (equal b 0))
                (numberp c)
                (not (equal c 0)))
           (equal (difference (times a b) c)
                  (if (lessp (sub1 a) (sub1 c))
                      (plus (difference (sub1 b)
                                        (difference (sub1 c)
                                                    (sub1 a)))
                            (times (sub1 a) (sub1 b)))
                    (plus (sub1 b)
                          (difference (sub1 a) (sub1 c))
                          (times (sub1 a) (sub1 b)))))))

;;; canonical

(prove-lemma difference-times-arg1-simplest (rewrite)
  (implies (and (not (lessp b c))
                (numberp a)  ; to avoid forced expansion
                (not (equal a 0))) ; of times
           (and
            (equal (difference (times a b) c)
                   (plus (difference b c) (times b (sub1 a))))
            (equal (difference (times b a) c)
                   (plus (difference b c) (times b (sub1 a)))))))

;;; canonical

(prove-lemma times-commutes (rewrite)
  (equal (times a b)
         (times b a)))

;;; The following two lemmas will be disabled after they are replaced by
;;; the permutative meta rules for plus and difference.

(prove-lemma plus-commutes (rewrite)
  (equal (plus a b)
         (plus b a)))

(prove-lemma plus-commutes-nest (rewrite)
  (equal (plus a (plus b c))
         (plus b (plus a c))))

(prove-lemma difference-times-arg1-kb (rewrite)
  (implies (and (equal (remainder c b) 0)
                (lessp c (times a b)))
           (and
            (equal (plus (difference a (remainder c a))
                         (times a (difference (sub1 b)
                                              (quotient c a))))
                   (plus b
                         (times b (difference (sub1 a)
                                              (quotient c b)))))
            (equal (plus (difference a (remainder c a))
                         (difference (sub1 b) (quotient c a))
                         (times (sub1 a)
                                (difference (sub1 b)
                                            (quotient c a))))
                   (plus b
                         (times b (difference (sub1 a)
                                              (quotient c b)))))
            (equal (plus (difference (sub1 b) (quotient c a))
                         (difference a (remainder c a))
                         (times (sub1 a)
                                (difference (sub1 b)
                                            (quotient c a))))
                   (plus b
                         (times b (difference (sub1 a)
                                              (quotient c b)))))))
  ((use (difference-times-arg1 (a a) (b b) (c c))
        (difference-times-arg1 (a b) (b a) (c c)))
   (disable difference-times-arg1)))

;;; canonical

;;; We make this conditional because rewriting the right hand side is costly.

(prove-lemma difference-times-arg2 (rewrite)
  (implies (not (lessp c (times b a)))
           (equal (difference c (times b a))
                  (plus (remainder c b)
                        (times b (difference (quotient c b) a)))))
  ((induct (diff-times-ind b a c))))

;;; canonical

(prove-lemma difference-times-arg2-preferred (rewrite)
  (implies (and (equal (remainder c a) 0)
                (not (lessp c (times b a))))
           (equal (difference c (times b a))
                  (times a (difference (quotient c a) b))))
  ((use (difference-times-arg2 (a a) (b b) (c c))
        (difference-times-arg2 (a b) (b a) (c c)))
   (disable difference-times-arg2)))

;;; canonical (preferred)

(prove-lemma difference-times-arg1-arg2 (rewrite)
  (and
   (equal (difference (times c a) (times c b))
          (times c (difference a b)))
   (equal (difference (times a c) (times c b))
          (times c (difference a b)))
   (equal (difference (times c a) (times b c))
          (times c (difference a b)))
   (equal (difference (times a c) (times b c))
          (times c (difference a b))))
  ((induct (difference a b))
   (disable difference-times-arg1-simplest
            difference-times-arg2
            difference-times-arg2-preferred
            difference-times-arg1-simpler
            plus-commutes
            plus-commutes-nest
            difference-times-arg1)))

;;; canonical

(prove-lemma sub1-difference (rewrite)
  (equal (sub1 (difference a b))
         (difference (sub1 a) b)))

;;; In the following lemma, we choose (lessp a b) rather than (not (lessp b a))
;;; so that the hypothesis of the rewrite rule is more likely to reduce to
;;; true or false.  Consider the case where (difference a b) is introduced by
;;; expanding (remainder a b) or (quotient a b).  In both cases the occurrence
;;; of (difference a b) is governed by the predicate (lessp a b).  So we adopt
;;; the policy of favoring (lessp a b) over (lessp b a) whenever b occurs as a
;;; subtrahend.  This same policy when applied to terms introduced on the right
;;; hand side of unconditional rewrite rules encourages function expansion,
;;; since it introduces terms which are likely to be already present
;;; in the term structure of the conjecture being proven.

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

;;; canonical

(prove-lemma sub1-remainder (rewrite)
  (equal (sub1 (remainder a b))
         (if (equal (remainder a b) 0)
             0
           (remainder (sub1 a) b))))

;;; canonical

(prove-lemma difference-remainder-arg1 (rewrite)
  (equal (difference (remainder a c) b)
         (if (lessp (remainder a c) b)
             0
           (remainder (difference a b) c)))
  ((induct (difference a b))))

;;; canonical

(prove-lemma difference-remainder-arg2 (rewrite)
  (implies (not (lessp b a))
           (equal (difference b (remainder a c))
                  (plus (difference b a)
                        (times c (quotient a c))))))

(defn lessp-quotient-ind (a b c)
  (if (zerop c)
      0
    (if (lessp b c)
        0
      (if (lessp a c)
          0
        (lessp-quotient-ind (difference a c) (difference b c) c)))))

;;; lessp-quotient will eventually mask this rule.

(prove-lemma lessp-quotient-arg1-linear (rewrite)
  (and (implies (not (lessp b a))
                (not (lessp (quotient b c)
                            (quotient a c))))
       (implies (lessp a b)
                (not (lessp (quotient b c)
                            (quotient a c)))))
  ((induct (lessp-quotient-ind a b c))))

;;; aka "min(a,b)"

(prove-lemma difference-difference-cancellation (rewrite)
  (equal (difference b (difference b a))
         (if (and (numberp a)
                  (numberp b))
             (if (lessp a b)
                 a
               b)
           0)))

;;; difference-elim is useful in situations where quotient-remainder
;;; will not apply because the first argument of quotient and remainder is a
;;; difference.

(prove-lemma difference-elim (elim)
  (implies (lessp b a)
           (equal (plus b (difference a b)) a)))

(prove-lemma difference-generalize (generalize)
  (and (numberp (difference a b))
       (not (lessp a (difference a b)))))

;;; Assuming (plus a b) is normalized, a is lexicographically smaller than
;;; b.  In order to minimize the likelihood of introducing costly inversions
;;; on the right hand side of this rule, we choose to place a within lessp
;;; and difference, when given a choice between a and b.  We use (lessp a c)
;;; rather than (not (lessp c a)) because (difference (plus a b) 0) will not
;;; otherwise immediately simplify.

;;; canonical

(prove-lemma difference-plus-arg1 (rewrite)
  (equal (difference (plus a b) c) ; a is lex smaller than b
         (if (lessp a c)
             (difference b (difference c a)) ; move smaller in
           (plus (difference a c) b))))      ; b could be plus nest

#|
;;; This version of difference-plus-arg1 avoids the case split on (lessp a c)
;;; but in practice did not perform as well as the more aggressive version.

;;; canonical

(prove-lemma difference-plus-arg1 (rewrite)
  (equal (difference (plus a b) c)
         (plus (difference b c)
               (difference a (difference c b)))))

|#
;;; We avoid the more natural equivalence (equal (difference a b) 0) iff
;;; (not (lessp b a)) in order to encourage the opening of functions such as
;;; (quotient a b) and (remainder a b).  Another way to rationalize this, is
;;; that if (difference a b) is already present, then (not (lessp a b)) is
;;; also likely to be present.  Thus (lessp a b) will be eliminated, and
;;; we will have new equality facts about a.

(prove-lemma difference-0 (rewrite)
  (equal (equal (difference a b) 0)
         (or (not (numberp a))
             (equal a 0)
             (equal a b)
             (lessp a b))))

(prove-lemma difference-difference-arg1-commutes (rewrite)
  (equal (difference (difference a b) c)
         (difference (difference a c) b)))

;;; This lemma is dangerous since it rewrites a potentially numerically
;;; smaller argument to a larger one.
;;; quotient-difference-arg1 can force expansion of quotient.  For example,
;;; consider (quotient a (add1 b)).

(prove-lemma quotient-difference-arg1 (rewrite)
  (implies (lessp c b)
           (equal (quotient (difference a c) b)
                  (if (lessp (remainder a b) c)
                      (quotient (difference a b) b)
                    (quotient a b))))
  ((induct (remainder a b))))

(prove-lemma difference-difference-difference-cancellation (rewrite)
  (and (equal (difference (difference b a) (difference c a))
              (if (lessp b a)
                  0
                (if (lessp c a)
                    (difference b a)
                  (difference b c))))
       (equal (difference (difference a b) (difference a c))
              (if (lessp a b)
                  0
                (if (lessp a c)
                    (difference a b)
                  (difference c b))))))

;;; Consider replacing (lessp (remainder b a) (remainder c a) by
;;; (lessp (plus b (times a (quotient c a)))
;;;        (plus c (times a (quotient b a))))

;;; canonical (qbca avoids repeated rewriting)

(prove-lemma difference-quotient-arg1-arg2 (rewrite)
  (implies (equal qbca (quotient (difference b c) a))
           (equal (difference (quotient b a) (quotient c a))
                  (if (lessp b c)
                      0
                    (if (lessp (remainder b a) (remainder c a))
                        (add1 qbca)
                      qbca))))
  ((induct (lessp-quotient-ind b c a))))

;;; The goal of this library is to reduce the "entropy" of symbolic
;;; expressions, that is the number of ways that a canonical object in the
;;; logic may be expressed.  The expressions b + (a - c) and a + (b - c)
;;; are equal, provided a >= c and b >= c.  This suggests a conditional
;;; permutative rule.  However, such a rule would convert the normalized
;;; expression (plus (times x y) (difference a (difference b c))) to
;;; (plus a (difference (times x y) (difference b c))).  This problem
;;; arises because nqthm's term order does not obey our function
;;; nesting conventions.  So we create our own term order, and represent
;;; permutative rules on difference and plus by meta rules.  This approach
;;; does not work when the permutative rule compares two "non-tame" function
;;; applications (e.g. EVAL$), since nqthm replaces non-tame functions by
;;; variable symbols before applying the meta rule.  For this reason we retain
;;; (disabled) versions of several permutative rewrite rules, notably
;;; plus-commutes and plus-commutes-nest.

;;; Compare two exploded litatoms.
;;; lit-ord returns true iff a is strictly less than b.

(defn lit-ord (a b)
  (if (listp a)
      (if (listp b)
          (or (lessp (car a) (car b))
              (and (equal (car a) (car b))
                   (lit-ord (cdr a) (cdr b))))
        f)
    (if (listp b)
        t
      (lessp a b))))

;;; There is a problem with permutative meta rules when applied to non-tame
;;; terms.  nqthm replaces the non-tame term with a tame one by substituting
;;; new variables for the non-tame subterms.  It does this before applying
;;; the body of the meta rule.  This makes any syntactic checks based upon
;;; the specific structure of a subterm ineffective.  We provide an
;;; implementation specific solution by treating all variables beginning
;;; with vvv- as placeholders for non-tame terms.  We place vvv- at the
;;; upper end of the term order, and return f whenever the result depends
;;; on comparing two variables beginning with vvv-.

;;; Test whether an exploded litatom is a placeholder for a non-tame term.

(defn wild (a)
  (and (equal (car a) 86)
       (equal (cadr a) 86)
       (equal (caddr a) 86)
       (equal (cadddr a) 45)))

;;; Count the number of cons's within a.

(defn size (a)
  (if (listp a)
      (add1 (plus (size (car a)) (size (cdr a))))
    0))

(defn fcn-idx (a)
  (cond ((equal a 'plus) 6)
        ((equal a 'times) 5)
        ((equal a 'difference) 1)
        ((equal a 'add1) 7)
        ((equal a 'sub1) 0)
        ((equal a 'remainder) 3)
        ((equal a 'quotient) 2)
        ((equal a 'exp) 4)
        (t f)))

;;; (sub-expr a b f) returns true iff a is a subexpression of b.
;;; If b is a proper list, then (sub-expr 'nil b f) is always true.

(defn sub-expr (a b arg?)
  (if (listp b)
      (if arg?
          (or (sub-expr a (car b) f)
              (sub-expr a (cdr b) t))
        (or (equal a b)
            (sub-expr a (cdr b) t)))
    (equal a b))) ; don't bother checking arg? at this point

;;; Compare two terms

;;; (lex a b f) returns true iff a is difference from b, and either
;;; 1. a is a subexpression of b, or
;;; 2. b is not a subexpression of a, and
;;;    a is strictly less than b in the order
;;;       0 1 2 ...
;;;       a b c ... z aa ab ...
;;;       sub1 difference quotient remainder exp times plus add1
;;;       {all other functions}
;;;       {non-tame terms}
;;;    or a and b begin with the same function symbol and
;;;       either the size of a is less than that of b, or
;;;       the sizes are equal and the first argument ai in a which differs
;;;       from the corresponding argument bi in b satisfies (lex ai bi f).

;;; lex has the trichotomy property if a and b are not both wild and of type
;;; listp, litatom or numberp.  That is to say, the only things which are
;;; not comparable are two wild terms, or terms not of type listp, litatom
;;; or numberp.  However, lex is not transitive.

;;; The flag sz is included to prevent (if true) recalculation of the sizes
;;; of a and b.

(defn lex (a b sz)
  (if (equal a b)
      f
    (if (sub-expr a b f)
        t
      (if (sub-expr b a f)
          f
        (if (listp a)
            (if (listp b)
                (or (lex (car a) (car b) sz)
                    (and (equal (car a) (car b))
                         (if sz
                             (lex (cdr a) (cdr b) sz)
                           (let ((sa (size a))
                                 (sb (size b)))
                             (or (lessp sa sb)
                                 (and (equal sa sb)
                                      (lex (cdr a) (cdr b) t)))))))
              (and (litatom b)
                   (wild (unpack b))))
          (if (listp b)
              (not (and (litatom a)
                        (wild (unpack a))))
            (if (litatom a)
                (if (wild (unpack a))
                    f
                  (if (litatom b)
                      (if (wild (unpack b))
                          t
                        (let ((c (fcn-idx a))
                              (d (fcn-idx b)))
                          (if d
                              (if c
                                  (lessp c d)
                                f)
                            (if c
                                t
                              (lit-ord (unpack a) (unpack b))))))
                    f))
              (if (numberp a)
                  (if (litatom b)
                      t
                    (if (numberp b)
                        (lessp a b)
                      f))
                (or (litatom b)
                    (numberp b))))))))))

;;; The following sequence of rewrites demonstrate the need for a secondary
;;; sort within lex which uses the size of the term.  Without this, as is
;;; shown, the sequence cycles.
;;;
;;; Wherever a difference occurs introduce the constraint necessary for the
;;; result to remain non-negative.  Then all constraints are satisfied using
;;; A = 2, B = 3, C = 1, D = 0.  The lexicographic constraints are
;;; satisfied by choosing A, B, C, D to be new function symbols above ADD1,
;;; where B is smaller than D.
;;;
;;; (A + C) - (B + D) -> {difference-plus-arg2}
;;; ((A + C) - B) - D -> {difference-plus-arg1}
;;; (C - (B - A)) - D -> {difference-difference-arg2-commutes-meta}
;;; (A - (B - C)) - D -> {difference-difference-arg1-commutes-meta}
;;; (A - D) - (B - C) -> {difference-difference-arg2-commutes-meta}
;;; C - (B - (A - D)) -> {difference-difference-arg2-commutes-meta}
;;; C - (D + (B - A)) -> {difference-plus-arg2}
;;; (C - D) - (B - A) -> {difference-difference-arg2-commutes}
;;; A - (B - (C - D)) -> {difference-difference-arg2-commutes}
;;; A - (D + (B - C)) -> {difference-plus-arg2}
;;; (A - D) - (B - C) -> which cycles

;;; The following tree illustrates the relationship among the permutative
;;; meta rules for difference and plus.
;;;
;;;
;;;                         (a + b) - c
;;;                            /    \
;;;                    a < c  /      \ a >= c
;;;                          /        \
;;;                         /          \
;;;                  b - (c - a)   b + (a - c) or (a - c) + b
;;;                       /\           / \
;;;               c >= a /  \ c<a a<c /   \ a >= c
;;;                     /    \       /     \
;;;                    /\     b     b      /\
;;;                   /  \                /  \
;;;           c >= b /    \ c < b  b < c /    \ b >= c
;;;                 /      \            /      \
;;;                /        \          /        \
;;;               /          \        /          \
;;;       a - (c - b)  a + (b - c)  a - (c - b)  a + (b - c)
;;;
;;;                         c - (b + a)
;;;                              |
;;;                              |
;;;                         (c - a) - b
;;;                              |
;;;                              |
;;;                         (c - b) - a
;;;

;;; b + (a - c) -> (b - c) + a if b is lexicographically less than a.
;;; (a - c) + b -> (b - c) + a if b is lexicographically less than a.

;;; The right hand side is oriented assuming plus-commutes-meta has
;;; already been applied to the left hand side.  Thus we are assured
;;; that (b - c) << a when (a - c) << b << a

(defn plus-diff (a)
  (if (equal (car a) 'plus)
      (if (and (equal (caaddr a) 'difference)
               (lex (cadr a) (cadr (caddr a)) f)) ; b << a
          `(if (lessp ,(cadaddr a) ,(caddr (caddr a))) ; a < c
               (if (numberp ,(cadr a)) ,(cadr a) (zero))
             (if (lessp ,(cadr a) ,(caddr (caddr a))) ; b < c
                 (difference ,(cadaddr a)             ; a - (c - b)
                             (difference ,(caddr (caddr a)) ,(cadr a)))
               (plus (difference ,(cadr a) ,(caddr (caddr a))) ,(cadaddr a))))
        (if (and (equal (caadr a) 'difference)
                 (lex (caddr a) (cadadr a) f))   ; b << a
            `(if (lessp ,(cadadr a) ,(caddr (cadr a))) ; a < c
                 (if (numberp ,(caddr a)) ,(caddr a) (zero))
               (if (lessp ,(caddr a) ,(caddr (cadr a))) ; b < c
                   (difference ,(cadadr a)              ; a - (c - b)
                               (difference ,(caddr (cadr a)) ,(caddr a)))
                 (plus (difference ,(caddr a) ,(caddr (cadr a))) ,(cadadr a))))
          a))
    a))

;;; When a rule is potentially costly, rather than combining several rewrites
;;; under a common name we provide separate rules so that the inexpensive rule
;;; is still available after the costly one is disabled.  We do not provide
;;; a rule for (not (numberp a)) in plus-zerop, because this will be treated
;;; by function expansion.  Furthermore, when plus is expanded there will be
;;; no recursive call of plus where the first argument is not numberp.

(prove-lemma plus-zerop (rewrite)
  (implies (not (numberp b))
           (equal (plus a b) (if (numberp a) a 0))))

;;; We include the case (plus 0 a) because it may arise from the expansion
;;; of (plus 1 a).  Recursive functions do not expand fully, unless all
;;; arguments are explicit values.

(prove-lemma plus-0 (rewrite)
  (and (equal (plus a 0) (if (numberp a) a 0))
       (equal (plus 0 a) (if (numberp a) a 0))))

;;; This rule is costly on deep plus nests which are equated to 0.

(prove-lemma plus-is-0 (rewrite)
  (equal (equal (plus a b) 0)
         (and (or (not (numberp a))
                  (equal a 0))
              (or (not (numberp b))
                  (equal b 0)))))

;;; canonical

(prove-lemma plus-difference-commutes-meta ((meta plus))
  (equal (eval$ t a y)
         (eval$ t (plus-diff a) y))
  ((disable lex)))

;;; We order the terms within a normalized plus nest from lexicographically
;;; large to small as we procede from the outer to the inner levels.  This
;;; moves the smallest addend next to difference, and increases the likelihood
;;; of having a favorable term to move within difference using
;;; plus-difference-commutes-meta.  In a similar fashion, we order the terms
;;; within a difference nest to maximize the likelihood of having a favorable
;;; term to exchange at its outer level.

(defn plus-com (a)
  (if (and (equal (car a) 'plus)
           (not (equal (caaddr a) 'plus))
           (lex (caddr a) (cadr a) f))
      `(plus ,(caddr a) ,(cadr a))
    a))

;;; canonical

(prove-lemma plus-commutes-meta ((meta plus))
  (equal (eval$ t a y)
         (eval$ t (plus-com a) y))
  ((disable lex)))

(disable plus-commutes)

;;; a + (b + c) -> b + (a + c) if a is lexicographically less than b.

(defn plus-plus-com (a)
  (if (and (equal (car a) 'plus)
           (equal (caaddr a) 'plus)
           (lex (cadr (caddr a)) (cadr a) f))
      `(plus ,(cadr (caddr a)) (plus ,(cadr a) ,(caddr (caddr a))))
    a))

;;; canonical

(prove-lemma plus-commutes-nest-meta ((meta plus))
  (equal (eval$ t a y)
         (eval$ t (plus-plus-com a) y))
  ((disable lex)))

(disable plus-commutes-nest)

;;; We now correct inversions involving add1, plus, times and sub1.

;;; canonical

(prove-lemma plus-add1 (rewrite)
  (and (equal (plus a (add1 b))
              (add1 (plus a b)))
       (equal (plus (add1 a) b)
              (add1 (plus a b)))))

;;; (sub1 (add1 x)) is already present as an axiom

;;; canonical

(prove-lemma times-plus (rewrite)
  (and (equal (times (plus a b) c)
              (plus (times a c) (times b c)))
       (equal (times c (plus a b))
              (plus (times c a) (times c b)))))

;;; This rule in effect forces an expansion of plus, regardless of the value
;;; of a.  This will not lead to infinite expansion, provided sub1 is not
;;; driven down to plus infinitely often from the enclosing expression.

;;; We do not include normalization lemmas for sub1 inside of plus, since
;;; they would conflict with plus-difference-commutes-meta.  Furthermore,
;;; there is a natural normalization which occurs when plus is expanded.
;;; As plus-commutes-meta moves litatoms to the left, expansion of plus will
;;; tend to distribute sub1's uniformly over all litatoms occurring with the
;;; plus nest.

;;; canonical (needed to avoid "expand" hints)

(prove-lemma sub1-plus (rewrite)
  (equal (sub1 (plus a b))
         (if (or (not (numberp a))
                 (equal a 0))
             (sub1 b)
           (plus (sub1 a) b)))) ; b may be a plus nest

;;; canonical

(prove-lemma sub1-times (rewrite)
  (equal (sub1 (times a b))
         (if (or (not (numberp a))
                 (equal a 0))
             0
           (plus (sub1 b) (times b (sub1 a))))))

;;; canonical

(prove-lemma plus-associates-right (rewrite)
  (equal (plus (plus a b) c)
         (plus a (plus b c))))

(prove-lemma no-divisors-of-zero (rewrite)
  (equal (equal (times a b) 0)
         (or (not (numberp b))
             (equal b 0)
             (not (numberp a))
             (equal a 0))))

;;; canonical

(prove-lemma times-commutes-nest (rewrite)
  (equal (times a (times b c))
         (times b (times a c))))

;;; canonical

(prove-lemma times-associates-right (rewrite)
  (equal (times (times a b) c)
         (times a (times b c))))

(prove-lemma lessp-times-linear (rewrite)
  (and (implies (and (not (lessp b a))
                     (numberp c)
                     (not (equal c 0)))
                (and (not (lessp (times c b) a))
                     (not (lessp (times b c) a))))
       (implies (and (lessp a b)
                     (numberp c)
                     (not (equal c 0)))
                (and (lessp a (times b c))
                     (lessp a (times c b))))))

(prove-lemma lessp-times-both-linear (rewrite)
  (and (implies (and (lessp a b)
                     (not (lessp d c))
                     (numberp d)
                     (not (equal d 0)))
                (and (lessp (times a c) (times b d))
                     (lessp (times c a) (times b d))
                     (lessp (times a c) (times d b))
                     (lessp (times c a) (times d b))))
       (implies (and (lessp a b)
                     (lessp c d))
                (and (lessp (times a c) (times b d))
                     (lessp (times c a) (times b d)))))
  ((induct (lessp a b))))

(prove-lemma lessp-times-single-linear (rewrite)
  (and (implies (and (lessp a b)
                     (not (equal c 0))
                     (numberp c))
                (and (lessp (times a c) (times b c))
                     (lessp (times c a) (times b c))
                     (lessp (times a c) (times c b))
                     (lessp (times c a) (times c b))))
       (implies (not (lessp b a))
                (and (not (lessp (times b c) (times a c)))
                     (not (lessp (times c b) (times a c)))
                     (not (lessp (times b c) (times c a)))
                     (not (lessp (times c b) (times c a)))))
       (implies (lessp a b)
                (and (not (lessp (times b c) (times a c)))
                     (not (lessp (times c b) (times a c)))
                     (not (lessp (times b c) (times c a)))
                     (not (lessp (times c b) (times c a))))))
  ((induct (lessp a b))
   (disable sub1-times
            sub1-plus
            plus-is-0)))

;;; We include this cancellation lemma to reduce the opportunities for the
;;; above linear rules.  It also compensates for a deficiency of linear
;;; (Presburger) arithmetic which does not use properties of times.  So we
;;; remove times from inside lessp whenever possible.  Additionally, we
;;; favor (and (numberp c) (not (equal c 0))) to (lessp 0 c), because
;;; linear arithmetic is not consistently employed (e.g. when relieving
;;; the hypotheses of rewrite rules.

(prove-lemma lessp-times-cancellation (rewrite)
  (and
   (equal (lessp (times a c) (times b c))
          (and (numberp c) (not (equal c 0)) (lessp a b)))
   (equal (lessp (times c a) (times b c))
          (and (numberp c) (not (equal c 0)) (lessp a b)))
   (equal (lessp (times a c) (times c b))
          (and (numberp c) (not (equal c 0)) (lessp a b)))
   (equal (lessp (times c a) (times c b))
          (and (numberp c) (not (equal c 0)) (lessp a b)))
   (equal (lessp (times c b) c)
          (and (numberp c)
               (not (equal c 0))
               (or (not (numberp b))
                   (equal b 0))))
   (equal (lessp (times b c) c)
          (and (numberp c)
               (not (equal c 0))
               (or (not (numberp b))
                   (equal b 0))))
   (equal (lessp c (times c b))
          (and (numberp c)
               (not (equal c 0))
               (not (equal (sub1 b) 0))))
   (equal (lessp c (times b c))
          (and (numberp c)
               (not (equal c 0))
               (not (equal (sub1 b) 0)))))
  ((disable lessp-times-single-linear
            sub1-times
            sub1-plus
            lessp-times-linear)))

(prove-lemma lessp-facts (rewrite)
  (and (equal (lessp a a) f)
       (equal (lessp a 0) f)
       (equal (lessp 0 a)
              (and (numberp a) (not (equal a 0))))
       (equal (lessp (sub1 a) a)
              (and (numberp a) (not (equal a 0))))
       (equal (lessp a (sub1 a)) f)
       (equal (lessp (sub1 (sub1 a)) a)
              (and (numberp a) (not (equal a 0))))
       (equal (lessp a (sub1 (sub1 a))) f)))

;;; We include the following lemma because nqthm does not normalize
;;; if-expressions when relieving the hypotheses of rewrite rules.
;;; Consequently expressions such as (not (lessp b a)), which expands to
;;; (if (lessp b a) F T), will not benefit from linear arithmetic.

(prove-lemma dichotomy (rewrite)
  (and
   (implies (and (lessp x a)      ; use free variable x to avoid
                 (equal x b))     ; rewriting (lessp b a), but
            (equal (lessp a b) f)) ; not (equal x b) unfortunately.
   (implies (and (lessp b x)       ; (lessp x a) must precede
                 (equal x a))      ; (equal x b) to avoid rewriting
            (equal (lessp a b) f))
   (implies (and (not (lessp x a))
                 (equal x b)
                 (numberp b)
                 (not (equal b 0))
                 (not (equal a x)))
            (equal (lessp a b) t))
   (implies (and (not (lessp b x))
                 (equal x a)
                 (numberp b)
                 (not (equal b 0))
                 (not (equal b x)))
            (equal (lessp a b) t))))

;;; Extend the nesting order to add1, plus, times, difference, sub1

;;; canonical

;;; We choose to push add1 to the inside rather than to the outside in order
;;; to move more rapidly to a normal form.

(prove-lemma difference-add1 (rewrite)
  (and (equal (difference (add1 a) b)
              (if (or (not (numberp b))
                      (equal b 0))
                  (add1 a)
                (difference a (sub1 b))))
       (equal (difference a (add1 b))
              (difference (sub1 a) b))))

;;; canonical

(prove-lemma add1-difference (rewrite)
  (equal (add1 (difference a b))
         (if (or (not (numberp b))
                 (equal b 0))
             (add1 a)
           (if (lessp a b)
               1
             (difference a (sub1 b))))))

;;; canonical

(prove-lemma difference-plus-arg2 (rewrite)
  (equal (difference a (plus b c))
         (difference (difference a c) b)))

;;; (a - b) - c -> (a - c) - b if c is lexicographically less than b.

(defn diff-diff-1 (a)
  (if (and (equal (car a) 'difference)
           (equal (caadr a) 'difference)
           (lex (caddr a) (caddadr a) f))
      `(difference (difference ,(cadadr a) ,(caddr a)) ,(caddadr a))
    a))

;;; canonical

(prove-lemma difference-difference-arg1-commutes-meta ((meta difference))
  (equal (eval$ t a y)
         (eval$ t (diff-diff-1 a) y))
  ((disable lex)))

(disable difference-difference-arg1-commutes)

;;; b - (c - a) -> a - (c - b) if b is lexicographically less than a.

(defn diff-diff-2 (a)
  (if (and (equal (car a) 'difference)
           (equal (caaddr a) 'difference)
           (lex (cadr a) (caddaddr a) f))
      `(if (lessp ,(cadaddr a) ,(caddaddr a)) ; c < a
           (if (numberp ,(cadr a)) ,(cadr a) (zero))
         (if (lessp ,(cadaddr a) ,(cadr a)) ; c < b
             (plus ,(caddaddr a)
                   (difference ,(cadr a) ,(cadaddr a)))
           (difference ,(caddaddr a)
                       (difference ,(cadaddr a) ,(cadr a)))))
    a))

;;; canonical

(prove-lemma difference-difference-arg2-commutes-meta ((meta difference))
  (equal (eval$ t a y)
         (eval$ t (diff-diff-2 a) y))
  ((disable lex)))

;;; We may omit the meta rule to permute a and d within d + (b - (c - a)),
;;; assuming that normalization has progressed to the point where nesting
;;; order inversions are largely absent.  In this case lex will be transitive,
;;; since subexpression inclusion implies normal lex ordering without
;;; subexpression inclusion checks.  So plus-difference-commutes-meta and
;;; difference-difference-arg2-commutes-meta will assure that a << b << d.
;;; From transitivity, a << d.

(prove-lemma difference-facts (rewrite)
  (and (equal (difference a a) 0)
       (equal (difference a (sub1 a))
              (if (or (not (numberp a))
                      (equal a 0))
                  0
                1))
       (equal (difference a (sub1 (sub1 a)))
              (if (or (not (numberp a))
                      (equal a 0))
                  0
                (if (equal a 1)
                    1
                  2)))
       (equal (difference (sub1 b) (difference b a))
              (if (lessp a b)
                  (sub1 a)
                (sub1 b)))
       (equal (difference b (difference (sub1 b) a))
              (if (numberp b)
                  (if (lessp a b)
                      (add1 a)
                    b)
                0))))

(prove-lemma remainder-lessp-rewrite (rewrite)
  (and (equal (lessp (remainder a b) b)
              (and (numberp b)
                   (not (equal b 0))))
       (equal (lessp (remainder a b) a)
              (and (numberp b)
                   (not (equal b 0))
                   (not (lessp a b))))
       (equal (lessp a (remainder a b)) f)
       (equal (lessp b (remainder a b))
              (and (or (not (numberp b)) (equal b 0))
                   (numberp a)
                   (not (equal a 0)))))
  ((disable lessp-times-single-linear)))

(prove-lemma quotient-lessp-linear (rewrite)
  (and (not (lessp a (times b (quotient a b))))
       (not (lessp a (plus (quotient a b)
                           (times (sub1 b) (quotient a b)))))))

;;; Create meta rule for eliminating a factor from both sides of an equality.

;;; Assume that products are in normal form, i.e. no leftmost argument to
;;; times begins with times and the arguments to times proceeding from left
;;; to right are lexicographically sorted.

(prove-lemma count-decreases (rewrite)
  (implies (not (equal (car a) 0))
           (and (lessp (count (cadr a)) (count a))
                (lessp (count (caddr a)) (count a)))))

;;; Assume that a and b are in normal form, i.e. no leftmost argument to
;;; times begins with times and the arguments to times proceeding from left
;;; to right are lexicographically sorted.

;;; (factor? a b) returns true if the factors of b are a sub bag of the
;;; factors of a.  factor? may not recognize some cases where b divides
;;; a syntactically if a and b are not in normal form.

(defn factor? (a b)
  (if (equal (car a) 'times)
      (if (equal (car b) 'times)
          (if (equal (cadr a) (cadr b))
              (factor? (caddr a) (caddr b))
            (factor? (caddr a) b))
        (if (equal (cadr a) b)
            t
          (factor? (caddr a) b)))
    (equal a b)))

;;; (tail? a b) returns true if b is a tail of the times nest in a.

(defn tail? (a b)
  (if (equal a b)
      t
    (if (equal (car a) 'times)
        (tail? (caddr a) b)
      f)))

(prove-lemma tail?-is-transitive (rewrite)
  (implies (and (tail? a b)
                (tail? b c))
           (tail? a c)))

(prove-lemma tail?-implies-factor? (rewrite)
  (implies (tail? a b)
           (factor? a b))
  ((induct (factor? a b))))

(prove-lemma factor?-tail?-helper-1 nil
  (implies (and (factor? a (cons 'times (cons b x)))
                (not (listp x)))
           (factor? a 0)))

(prove-lemma factor?-tail?-helper-2 (rewrite)
  (implies (and (factor? a b)
                (equal (car b) 'times))
           (factor? a (caddr b)))
  ((use (factor?-tail?-helper-1 (a a) (x (cddr b))))
   (disable tail?
            tail?-implies-factor?)))

(prove-lemma factor?-tail? (rewrite)
  (implies (and (factor? a b)
                (tail? c a))
           (factor? c b))
  ((induct (factor? c b))))

(prove-lemma factor?-is-transitive (rewrite)
  (and (implies (and (factor? a b)
                     (factor? b c))
                (factor? a c))
       (implies (and (factor? b c)
                     (factor? a b))
                (factor? a c))))

;;; If a and b are in normal form (using times-commutes and times-associates),
;;; then gcd? returns the largest common subsequence of factors in a and b.
;;; If no such subsequence exists, then gcd? returns false.  In all cases,
;;; if gcd? is non false then it returns a common subsequence of a and b.
;;; The subsequence is only guaranteed to be maximal when a and b are in
;;; normal form.  We do not prove that the subsequence is maximal, since it
;;; does not affect the soundness of the derived meta rule.  This procedure
;;; is a bit complex.  It makes use of the property that a and b are
;;; lexicographically sorted to infer from (factor? b (cadr a)) and
;;; (cadr a) /= (cadr b) that (cadr b) is not a factor of a.

(defn gcd? (a b)
  (if (equal (car a) 'times)
      (if (equal (caadr a) 'times)
          f
        (if (equal (car b) 'times)
            (if (equal (cadr a) (cadr b))
                (if (gcd? (caddr a) (caddr b))
                    `(times ,(cadr a) ,(gcd? (caddr a) (caddr b)))
                  (cadr a))
              (if (factor? b (cadr a))
                  (gcd? a (caddr b))
                (gcd? (caddr a) b)))
          (if (factor? a b)
              b
            f)))
    (if (factor? b a)
        a
      f))
  ((lessp (plus (count a) (count b)))))

(prove-lemma factor?-gcd? (rewrite)
  (implies (gcd? a b)
           (and (factor? a (gcd? a b))
                (factor? b (gcd? a b)))))

(disable tail?-is-transitive)
(disable tail?-implies-factor?)
(disable factor?-tail?-helper-2)
(disable factor?-tail?)

;;; `(fix ,(remove-factors a b)) before use.

(defn remove-factors (a b)
  (if (equal (car a) 'times)
      (if (equal (car b) 'times)
          (if (equal (cadr a) (cadr b))
              (remove-factors (caddr a) (caddr b))
            `(times ,(cadr a) ,(remove-factors (caddr a) b)))
        (if (equal (cadr a) b)
            (caddr a)
          `(times ,(cadr a) ,(remove-factors (caddr a) b))))
    (if (equal a b)
        '(add1 (zero))
      a)))

(prove-lemma factor?-divides (rewrite)
  (implies (factor? a b)
           (equal (times (eval$ t b y)
                         (eval$ t (remove-factors a b) y))
                  (if (numberp (eval$ t a y))
                      (eval$ t a y)
                    0)))
  ((induct (remove-factors a b))
   (disable sub1-times
            plus-commutes-meta)))

;;; Find the largest factor occurring in all summands of a.

(defn gcd?-sum (a)
  (if (equal (car a) 'plus)
      (gcd? (cadr a) (gcd?-sum (caddr a)))
    a))

;;; Remove the factor b from the sum a.

(defn remove-sum (a b)
  (if (equal (car a) 'plus)
      `(plus ,(remove-factors (cadr a) b)
             ,(remove-sum (caddr a) b))
    (remove-factors a b)))

(prove-lemma gcd?-sum-divides nil
  (implies (and (gcd?-sum a) ; factor of every summand of a
                (factor? (gcd?-sum a) b))
           (equal (times (eval$ t b y)
                         (eval$ t (remove-sum a b) y))
                  (if (numberp (eval$ t a y))
                      (eval$ t a y)
                    0)))
  ((induct (remove-sum a b))))

;;; Remove factor from both sides of an equality

(defn t-cancel (a)
  (if (and (equal (car a) 'equal)
           (not (equal (cadr a) (caddr a)))) ; => lhs or rhs is numberp
      (let ((b (gcd? (gcd?-sum (cadr a)) (gcd?-sum (caddr a)))))
        (if (and b (not (equal b '(add1 (zero)))) (not (equal b ''1)))
            `(if (and (numberp ,b)
                      (not (equal ,b (zero))))
                 (equal (fix ,(remove-sum (cadr a) b))
                        (fix ,(remove-sum (caddr a) b)))
               (and (numberp ,(cadr a))
                    (numberp ,(caddr a))))
          a))
    a))

(defn t-c-ind (a b)
  (if (equal (car a) 'plus)
      (if (equal (car b) 'plus)
          (t-c-ind (caddr a) (caddr b))
        (t-c-ind (caddr a) b))
    (if (equal (car b) 'plus)
        (t-c-ind a (caddr b))
      nil))
  ((lessp (plus (count a) (count b)))))

(prove-lemma t-cancel-numberp-helper nil
  (implies (and (not (equal a b))
                (gcd? (cons a c) (cons b d)))
           (or (equal a 'times)
               (equal b 'times))))

(prove-lemma t-cancel-numberp nil
  (implies (and (not (equal a b))
                (gcd? (gcd?-sum a) (gcd?-sum b)))
           (or (numberp (eval$ t a y))
               (numberp (eval$ t b y))))
  ((induct (t-c-ind a b))
   (use (t-cancel-numberp-helper (a (car a)) (b (car b))
                                 (c (cdr a)) (d (cdr b))))
   (disable eval$
            no-divisors-of-zero
            plus-add1
            times-associates-right
            quotient-remainder-rewrite
            times-plus)))

(prove-lemma equal-plus-cancel (rewrite)
  (and (equal (equal a (plus a b))
              (and (numberp a)
                   (or (not (numberp b))
                       (equal b 0))))
       (equal (equal a (plus b a))
              (and (numberp a)
                   (or (not (numberp b))
                       (equal b 0))))
       (equal (equal (plus a b) a)
              (and (numberp a)
                   (or (not (numberp b))
                       (equal b 0))))
       (equal (equal (plus b a) a)
              (and (numberp a)
                   (or (not (numberp b))
                       (equal b 0))))))

(prove-lemma equal-times-cancel (rewrite)
  (and (equal (equal (times a c) (times b c))
              (or (not (numberp c))
                  (equal c 0)
                  (equal (fix a) (fix b))))
       (equal (equal (times c a) (times b c))
              (or (not (numberp c))
                  (equal c 0)
                  (equal (fix a) (fix b))))
       (equal (equal (times a c) (times c b))
              (or (not (numberp c))
                  (equal c 0)
                  (equal (fix a) (fix b))))
       (equal (equal (times c a) (times c b))
              (or (not (numberp c))
                  (equal c 0)
                  (equal (fix a) (fix b))))
       (equal (equal c (times c b))
              (and (numberp c)
                   (or (equal c 0)
                       (equal b 1))))
       (equal (equal c (times b c))
              (and (numberp c)
                   (or (equal c 0)
                       (equal b 1))))
       (equal (equal (times c b) c)
              (and (numberp c)
                   (or (equal c 0)
                       (equal b 1))))
       (equal (equal (times b c) c)
              (and (numberp c)
                   (or (equal c 0)
                       (equal b 1)))))
  ((induct (difference a b))
   (expand (times b c))
   (disable sub1-times)))

(prove-lemma gcd?-sum-of-non-number-1 (rewrite)
  (implies (and (not (numberp (eval$ t a y)))
                (gcd? (gcd?-sum a) b))
           (equal (gcd?-sum a) a))
  ((induct (gcd?-sum a))))

(prove-lemma gcd?-sum-of-non-number-2 (rewrite)
  (implies (and (not (numberp (eval$ t a y)))
                (gcd? b (gcd?-sum a)))
           (equal (gcd?-sum a) a))
  ((induct (gcd?-sum a))))

(prove-lemma gcd?-of-non-number-1 (rewrite)
  (implies (and (not (numberp (eval$ t a y)))
                (gcd? (gcd?-sum a) b))
           (equal (gcd? a b) a))
  ((induct (gcd? a b))))

(prove-lemma gcd?-of-non-number-2 (rewrite)
  (implies (and (not (numberp (eval$ t a y)))
                (gcd? b (gcd?-sum a)))
           (equal (gcd? b a) a))
  ((induct (gcd? a b))))

(prove-lemma fix-eval$ (rewrite)
  (implies (equal (car a) 'fix)
           (equal (eval$ t a y)
                  (fix (eval$ t (cadr a) y)))))

(prove-lemma times-eval$ (rewrite)
  (implies (equal (car a) 'times)
           (equal (eval$ t a y)
                  (times (eval$ t (cadr a) y)
                         (eval$ t (caddr a) y)))))

(prove-lemma equal-eval$ (rewrite)
  (implies (equal (car a) 'equal)
           (equal (eval$ t a y)
                  (equal (eval$ t (cadr a) y)
                         (eval$ t (caddr a) y)))))

(prove-lemma if-eval$ (rewrite)
  (implies (equal (car a) 'if)
           (equal (eval$ t a y)
                  (if (eval$ t (cadr a) y)
                      (eval$ t (caddr a) y)
                    (eval$ t (cadddr a) y)))))

(prove-lemma equal-times-cancel-helper (rewrite)
  (implies (and (equal (times a b) c)
                (equal (times a d) c)
                (numberp a)
                (not (equal a 0))
                (numberp b)
                (numberp d))
           (equal (equal b d) t)))

(prove-lemma equal-times-cancel-meta ((meta equal))
  (equal (eval$ t a y)
         (eval$ t (t-cancel a) y))
  ((use (gcd?-sum-divides (a (cadr a))
                          (b (gcd? (gcd?-sum (cadr a)) (gcd?-sum (caddr a)))))
        (gcd?-sum-divides (a (caddr a))
                          (b (gcd? (gcd?-sum (cadr a)) (gcd?-sum (caddr a)))))
        (t-cancel-numberp (a (cadr a)) (b (caddr a))))
   (disable gcd?-sum
            plus-commutes-meta
            remove-sum)))


(disable equal-times-cancel-helper)

(defn t-cancel-lessp (a)
  (if (and (equal (car a) 'lessp)
           (not (equal (cadr a) (caddr a)))) ; => lhs or rhs is numberp
      (let ((b (gcd? (gcd?-sum (cadr a)) (gcd?-sum (caddr a)))))
        (if (and b (not (equal b '(add1 (zero)))) (not (equal b ''1)))
            `(if (and (numberp ,b)
                      (not (equal ,b (zero))))
                 (lessp ,(remove-sum (cadr a) b)
                        ,(remove-sum (caddr a) b))
               (false))
          a))
    a))

(prove-lemma lessp-times-cancel-meta-helper-1 (rewrite)
  (implies (and (not (equal a b))
                (gcd? (gcd?-sum a) (gcd?-sum b))
                (not (numberp (eval$ t a y))))
           (factor? (gcd?-sum b) a))
  ((use (factor?-gcd? (a (gcd?-sum a)) (b (gcd?-sum b))))))

(prove-lemma lessp-times-cancel-meta-helper-2 (rewrite)
  (implies (and (equal a (times c d))
                (equal b (times c e))
                (not (zerop c)))
           (equal (lessp a b)
                  (lessp d e))))

(prove-lemma lessp-times-cancel-meta ((meta lessp))
  (equal (eval$ t a y)
         (eval$ t (t-cancel-lessp a) y))
  ((use (gcd?-sum-divides (a (cadr a))
                          (b (gcd? (gcd?-sum (cadr a)) (gcd?-sum (caddr a)))))
        (gcd?-sum-divides (a (caddr a))
                          (b (gcd? (gcd?-sum (cadr a)) (gcd?-sum (caddr a)))))
        (t-cancel-numberp (a (cadr a)) (b (caddr a))))
   (disable plus-commutes-meta)))

(disable lessp-times-cancel-meta-helper-1)
(disable lessp-times-cancel-meta-helper-2)
(disable factor?-is-transitive)
(disable factor?-gcd?)
(disable factor?-divides)
(disable gcd?-sum-divides)
(disable gcd?-sum-of-non-number-1)
(disable gcd?-sum-of-non-number-2)
(disable gcd?-of-non-number-1)
(disable gcd?-of-non-number-2)

(prove-lemma difference-cancellation (rewrite)
  (and (equal (equal (difference a c)
                     (difference b c))
              (or (and (lessp a c) (lessp b c))
                  (and (lessp a c) (equal b c))
                  (and (lessp b c) (equal a c))
                  (equal (fix a) (fix b))))
       (equal (equal (difference c a)
                     (difference c b))
              (or (and (lessp c a) (lessp c b))
                  (and (lessp c a) (equal (fix b) (fix c)))
                  (and (lessp c b) (equal (fix a) (fix c)))
                  (equal (fix a) (fix b))))))

;;; Provide meta-rules for add1/plus/times cancellation within equal and lessp.

;;; Find the first occurrence of difference within the times-normalized list a.

(defn find-difference-times (a)
  (if (equal (car a) 'times)
      (if (equal (caadr a) 'difference)
          (cadr a)
        (find-difference-times (caddr a)))
    (if (equal (car a) 'difference)
        a
      f)))

;;; Find the first occurrence of difference within the plus-times-normalized a.

(defn find-difference-plus (a)
  (if (equal (car a) 'plus)
      (if (find-difference-times (cadr a))
          (find-difference-times (cadr a))
        (find-difference-plus (caddr a)))
    (find-difference-times a)))

;;; Find the first occurrence of difference within the add1/plus/times nest a.

(defn find-difference (a)
  (if (equal (car a) 'add1)
      (find-difference (cadr a))
    (find-difference-plus a)))

;;; Compute positive or negative addend associated with a difference term
;;; within a times nest.

(defn get-addend-times (a c)
  (if (equal (car a) 'times)
      (if (equal (caadr a) 'difference)
          (if c
              `(times ,(cadadr a) ,(caddr a))
            `(times ,(caddadr a) ,(caddr a)))
        `(times ,(cadr a) ,(get-addend-times (caddr a) c)))
    (if (equal (car a) 'difference)
        (if c (cadr a) (caddr a))
      f)))

;;; Compute positive or negative addend associated with a difference term
;;; within a plus/times nest.

(defn get-addend-plus (a c)
  (if (equal (car a) 'plus)
      (if (find-difference-times (cadr a))
          (get-addend-times (cadr a) c)
        (get-addend-plus (caddr a) c))
    (get-addend-times a c)))

;;; Compute positive or negative addend associated with a difference term
;;; within an add1/plus/times nest.

(defn get-addend (a c)
  (if (equal (car a) 'add1)
      (get-addend (cadr a) c)
    (get-addend-plus a c)))

;;; Delete the first difference term from a plus/times nest.

(defn remove-difference-plus (a)
  (if (equal (car a) 'plus)
      (if (find-difference-times (cadr a))
          (caddr a)
        `(plus ,(cadr a) ,(remove-difference-plus (caddr a))))
    '(zero)))

;;; Delete the first difference term from an add1/plus/times nest.

(defn remove-difference (a)
  (if (equal (car a) 'add1)
      `(add1 ,(remove-difference (cadr a)))
    (remove-difference-plus a)))

;;; Transpose negative portion of first difference across equal.

(defn equal-transpose (a)
  (if (equal (car a) 'equal)
      (if (find-difference (cadr a))
          (let ((b (find-difference (cadr a))))
            `(if (not (lessp ,(cadr b) ,(caddr b)))
                 (and (numberp ,(caddr a))
                      (equal (plus ,(get-addend (cadr a) t)
                                   ,(remove-difference (cadr a)))
                             (plus ,(get-addend (cadr a) f) ,(caddr a))))
               (equal (fix ,(remove-difference (cadr a)))
                      ,(caddr a))))
        (if (find-difference (caddr a))
            (let ((b (find-difference (caddr a))))
              `(if (not (lessp ,(cadr b) ,(caddr b)))
                   (and (numberp ,(cadr a))
                        (equal (plus ,(get-addend (caddr a) f) ,(cadr a))
                               (plus ,(get-addend (caddr a) t)
                                     ,(remove-difference (caddr a)))))
                 (equal ,(cadr a)
                        (fix ,(remove-difference (caddr a))))))
          a))
    a))

(prove-lemma remove-difference-times-subtracts (rewrite)
  (implies (find-difference-times a)
           (equal (eval$ t a y)
                  (difference (eval$ t (get-addend-times a t) y)
                              (eval$ t (get-addend-times a f) y))))
  ((induct (find-difference-times a))
   (disable plus-difference-commutes-meta)))

(prove-lemma remove-difference-plus-subtracts (rewrite)
  (implies (find-difference-plus a)
           (equal (eval$ t a y)
                  (plus (difference
                         (eval$ t (get-addend-plus a t) y)
                         (eval$ t (get-addend-plus a f) y))
                        (eval$ t (remove-difference-plus a) y))))
  ((induct (find-difference-plus a))
   (disable plus-commutes-meta
            plus-commutes-nest-meta
            plus-difference-commutes-meta)))


(prove-lemma remove-difference-subtracts (rewrite)
  (implies (find-difference a)
           (equal (eval$ t a y)
                  (plus (difference
                         (eval$ t (get-addend a t) y)
                         (eval$ t (get-addend a f) y))
                        (eval$ t (remove-difference a) y))))
  ((induct (find-difference a))))

(prove-lemma lessp-find-difference-times-1 (rewrite)
  (implies (lessp (eval$ t (cadr (find-difference-times a)) y)
                  (eval$ t (caddr (find-difference-times a)) y))
           (not (lessp (eval$ t (get-addend-times a f) y)
                       (eval$ t (get-addend-times a t) y))))
  ((induct (find-difference-times a))))

(prove-lemma lessp-find-difference-plus-1 (rewrite)
  (implies (lessp (eval$ t (cadr (find-difference-plus a)) y)
                  (eval$ t (caddr (find-difference-plus a)) y))
           (not (lessp (eval$ t (get-addend-plus a f) y)
                       (eval$ t (get-addend-plus a t) y))))
  ((induct (find-difference-plus a))))

(prove-lemma lessp-find-difference-1 (rewrite)
  (implies (lessp (eval$ t (cadr (find-difference a)) y)
                  (eval$ t (caddr (find-difference a)) y))
           (not (lessp (eval$ t (get-addend a f) y)
                       (eval$ t (get-addend a t) y))))
  ((induct (find-difference a))))

(prove-lemma lessp-find-difference-times-2 (rewrite)
  (implies (lessp (eval$ t (get-addend-times a t) y)
                  (eval$ t (get-addend-times a f) y))
           (lessp (eval$ t (cadr (find-difference-times a)) y)
                  (eval$ t (caddr (find-difference-times a)) y)))
  ((induct (find-difference-times a))))

(prove-lemma lessp-find-difference-plus-2 (rewrite)
  (implies (lessp (eval$ t (get-addend-plus a t) y)
                  (eval$ t (get-addend-plus a f) y))
           (lessp (eval$ t (cadr (find-difference-plus a)) y)
                  (eval$ t (caddr (find-difference-plus a)) y)))
  ((induct (find-difference-plus a))))

(prove-lemma lessp-find-difference-2 (rewrite)
  (implies (lessp (eval$ t (get-addend a t) y)
                  (eval$ t (get-addend a f) y))
           (lessp (eval$ t (cadr (find-difference a)) y)
                  (eval$ t (caddr (find-difference a)) y)))
  ((induct (find-difference a))))

;;; canonical (trades difference for plus across equal)

(prove-lemma equal-transpose-meta ((meta equal))
  (equal (eval$ t a y)
         (eval$ t (equal-transpose a) y))
  ((disable find-difference-times
            find-difference-plus
            remove-difference-plus-subtracts
            plus-difference-commutes-meta
            remove-difference-times-subtracts
            get-addend
            if-eval$
            fix-eval$
            times-eval$)))

(defn lessp-transpose (a)
  (if (equal (car a) 'lessp)
      (if (find-difference (cadr a))
          (let ((b (find-difference (cadr a))))
            `(if (not (lessp ,(cadr b) ,(caddr b)))
                 (lessp (plus ,(get-addend (cadr a) t)
                              ,(remove-difference (cadr a)))
                        (plus ,(get-addend (cadr a) f) ,(caddr a)))
               (lessp ,(remove-difference (cadr a))
                      ,(caddr a))))
        (if (find-difference (caddr a))
            (let ((b (find-difference (caddr a))))
              `(if (not (lessp ,(cadr b) ,(caddr b)))
                   (lessp (plus ,(get-addend (caddr a) f) ,(cadr a))
                          (plus ,(get-addend (caddr a) t)
                                ,(remove-difference (caddr a))))
                 (lessp ,(cadr a)
                        ,(remove-difference (caddr a)))))
          a))
    a))

(prove-lemma lessp-plus-difference (rewrite)
  (and (equal (lessp (plus c (difference a b)) d)
              (if (not (lessp a b))
                  (lessp (plus c a) (plus d b))
                (lessp c d)))
       (equal (lessp c (plus d (difference a b)))
              (if (not (lessp a b))
                  (lessp (plus c b) (plus d a))
                (lessp c d))))
  ((induct (difference a b))
   (disable plus-difference-commutes-meta ; necessary to prevent
            sub1-plus)))                  ; bind stack overflow

(prove-lemma numberp-get-addend-times (rewrite)
  (implies (and (find-difference-times a)
                (not (numberp (eval$ t (get-addend-times a c) y))))
           (and (equal (get-addend-times a t)
                       (cadr (find-difference-times a)))
                (equal (get-addend-times a f)
                       (caddr (find-difference-times a)))))
  ((induct (find-difference-times a))))

(prove-lemma numberp-get-addend-plus (rewrite)
  (implies (and (find-difference-plus a)
                (not (numberp (eval$ t (get-addend-plus a c) y))))
           (and (equal (get-addend-plus a t)
                       (cadr (find-difference-plus a)))
                (equal (get-addend-plus a f)
                       (caddr (find-difference-plus a)))))
  ((induct (find-difference-plus a))))

(prove-lemma numberp-get-addend (rewrite)
  (implies (and (find-difference a)
                (not (numberp (eval$ t (get-addend a c) y))))
           (and (equal (get-addend a t)
                       (cadr (find-difference a)))
                (equal (get-addend a f)
                       (caddr (find-difference a)))))
  ((induct (find-difference a))))

(prove-lemma equal-get-addend-times (rewrite)
  (implies (and (equal (eval$ t (get-addend-times a t) y)
                       (eval$ t (get-addend-times a f) y))
                (numberp (eval$ t (get-addend-times a f) y))
                (lessp (eval$ t (cadr (find-difference-times a)) y)
                       (eval$ t (caddr (find-difference-times a)) y)
                       ))
           (and (equal (eval$ t (get-addend-times a f) y) 0)
                (equal (eval$ t (get-addend-times a t) y) 0)))
  ((induct (find-difference-times a))
   (disable find-difference-plus
            remove-difference-plus-subtracts
            lessp-find-difference-times-2
            numberp-get-addend-times
            remove-difference-times-subtracts
            lessp-find-difference-times-1
            lessp-times-cancel-meta
            find-difference
            remove-difference-subtracts)))

(prove-lemma equal-get-addend-plus (rewrite)
  (implies (and (equal (eval$ t (get-addend-plus a t) y)
                       (eval$ t (get-addend-plus a f) y))
                (numberp (eval$ t (get-addend-plus a f) y))
                (lessp (eval$ t (cadr (find-difference-plus a)) y)
                       (eval$ t (caddr (find-difference-plus a)) y)
                       ))
           (and (equal (eval$ t (get-addend-plus a f) y) 0)
                (equal (eval$ t (get-addend-plus a t) y) 0)))
  ((induct (find-difference-plus a))
   (disable find-difference-times
            get-addend-times
            lessp-find-difference-plus-1
            lessp-find-difference-plus-2
            remove-difference-plus-subtracts
            numberp-get-addend-plus
            lessp-find-difference-times-1
            lessp-find-difference-times-2
            numberp-get-addend-times
            remove-difference-times-subtracts)))

(prove-lemma equal-get-addend (rewrite)
  (implies (and (equal (eval$ t (get-addend a t) y)
                       (eval$ t (get-addend a f) y))
                (numberp (eval$ t (get-addend a f) y))
                (lessp (eval$ t (cadr (find-difference a)) y)
                       (eval$ t (caddr (find-difference a)) y)
                       ))
           (and (equal (eval$ t (get-addend a f) y) 0)
                (equal (eval$ t (get-addend a t) y) 0)))
  ((induct (find-difference a))
   (disable find-difference-times
            get-addend-plus
            find-difference-plus
            lessp-find-difference-1
            lessp-find-difference-2
            numberp-get-addend-plus
            remove-difference-plus-subtracts
            lessp-find-difference-plus-1
            lessp-find-difference-plus-2)))

;;; canonical (trades difference for plus across lessp)

(prove-lemma lessp-transpose-meta ((meta lessp))
  (equal (eval$ t a y)
         (eval$ t (lessp-transpose a) y))
  ((enable plus-commutes)
   (disable plus-commutes-meta
            plus-difference-commutes-meta
            find-difference-times
            find-difference-plus
            remove-difference-plus-subtracts
            difference-lessp
            equal-transpose-meta
            get-addend
            remove-difference-times-subtracts
            dichotomy
            sub1-difference
            if-eval$
            times-eval$
            equal-eval$
            fix-eval$)))

(disable equal-get-addend)
(disable equal-get-addend-plus)
(disable equal-get-addend-times)
(disable numberp-get-addend)
(disable numberp-get-addend-plus)
(disable numberp-get-addend-times)
(disable lessp-plus-difference)
(disable lessp-find-difference-2)
(disable lessp-find-difference-plus-2)
(disable lessp-find-difference-times-2)
(disable lessp-find-difference-1)
(disable lessp-find-difference-plus-1)
(disable lessp-find-difference-times-1)
(disable remove-difference-subtracts)
(disable remove-difference-plus-subtracts)
(disable remove-difference-times-subtracts)

;;; remove the term x from the add1/plus nest a

(defn plus-remove (a x)
  (if x
      (if (equal a x)
          '(zero)
        (if (listp a)
            (if (equal (car a) 'add1)
                (if (plus-remove (cadr a) x)
                    `(add1 ,(plus-remove (cadr a) x))
                  f)
              (if (equal (car a) 'plus)
                  (if (equal (cadr a) x)
                      (if (caddr a)
                          (caddr a)
                        '(zero))
                    (if (plus-remove (caddr a) x)
                        `(plus ,(cadr a) ,(plus-remove (caddr a) x))
                      f))
                f))
          f))
    f))

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

(prove-lemma plus-remove-ge (rewrite)
  (implies (plus-remove a x)
           (not (lessp (eval$ t a y) (eval$ t x y))))
  ((induct (plus-remove a x))))

(prove-lemma plus-remove-subtracts (rewrite)
  (implies (plus-remove a x)
           (equal (fix (eval$ t (plus-remove a x) y))
                  (difference (eval$ t a y)
                              (eval$ t x y))))
  ((induct (plus-remove a x))
   (disable fix-eval$
            times-eval$
            equal-eval$
            lessp-transpose-meta
            if-eval$)))

;;; find a term which occurs within both add1/plus nests a and b

(defn overlap? (a b)
  (if (plus-remove a b)
      b
    (if (listp b)
        (if (equal (car b) 'add1)
            (overlap? a (cadr b))
          (if (equal (car b) 'plus)
              (if (plus-remove a (cadr b))
                  (cadr b)
                (overlap? a (caddr b)))
            f))
      f)))

(prove-lemma overlap?-add1-is-symmetric (rewrite)
  (implies (and (equal (car b) 'add1)
                (overlap? (cadr b) a))
           (overlap? b a)))

(prove-lemma overlap?-plus-is-symmetric (rewrite)
  (implies (and (equal (car b) 'plus)
                (overlap? (caddr b) a))
           (overlap? b a)))

(prove-lemma overlap?-is-symmetric (rewrite)
  (implies (overlap? a b)
           (overlap? b a)))

(disable overlap?-add1-is-symmetric)

(disable overlap?-plus-is-symmetric)

(prove-lemma overlap?-implies-plus-remove (rewrite)
  (implies (overlap? a b)
           (and (plus-remove a (overlap? a b))
                (plus-remove b (overlap? a b)))))

;;; remove a cancelling pair of terms from add1/plus nests within equal

(defn p-cancel-equal (a)
  (if (and (equal (car a) 'equal)
           (overlap? (cadr a) (caddr a))
           (not (equal (cadr a) (caddr a))))
      (if (plus-remove (cadr a) (caddr a))
          `(and (numberp ,(caddr a))
                (equal (zero) (fix ,(plus-remove (cadr a) (caddr a)))))
        (if (plus-remove (caddr a) (cadr a))
            `(and (numberp ,(cadr a))
                  (equal (zero) (fix ,(plus-remove (caddr a) (cadr a)))))
          `(equal (fix ,(plus-remove (cadr a)
                                     (overlap? (cadr a) (caddr a))))
                  (fix ,(plus-remove (caddr a)
                                     (overlap? (cadr a) (caddr a)))))))
    a))

(prove-lemma eval$-overlap?-le (rewrite)
  (and (not (lessp (eval$ t a x)
                   (eval$ t (overlap? a b) x)))
       (not (lessp (eval$ t b x)
                   (eval$ t (overlap? a b) x))))
  ((induct (overlap? a b))))

(prove-lemma plus-remove-implies-numberp (rewrite)
  (implies (and (plus-remove a b)
                (not (equal a b)))
           (numberp (eval$ t a y))))

(prove-lemma overlap?-implies-numberp-1 (rewrite)
  (implies (and (overlap? a b)
                (not (plus-remove a b)))
           (numberp (eval$ t b y)))
  ((expand (overlap? a b))))

(prove-lemma overlap?-implies-numberp-2 (rewrite)
  (implies (and (overlap? b a)
                (not (plus-remove a b)))
           (numberp (eval$ t b y)))
  ((use (overlap?-is-symmetric (a a) (b b)))
   (disable overlap?-is-symmetric)))

(prove-lemma equal-plus-cancel-helper (rewrite)
  (IMPLIES (AND (NOT (EQUAL V Z))
                (PLUS-REMOVE Z V)
                (EQUAL (EVAL$ T V Y) (EVAL$ T Z Y)))
           (NUMBERP (EVAL$ T V Y)))
  ((use (plus-remove-implies-numberp (a z) (b v)))))

;;; Placed here because the following meta rule is preferred

(prove-lemma equal-add1 (rewrite)
  (and (equal (equal a (add1 b))
              (if (numberp b)
                  (and (numberp a)
                       (not (equal a 0))
                       (equal b (sub1 a)))
                (equal a 1)))
       (equal (equal (add1 b) a)
              (if (numberp b)
                  (and (numberp a)
                       (not (equal a 0))
                       (equal b (sub1 a)))
                (equal a 1)))))

;;; canonical (preferred)

(prove-lemma equal-plus-cancel-meta ((meta equal))
  (equal (eval$ t a y)
         (eval$ t (p-cancel-equal a) y))
  ((enable plus-commutes
           plus-commutes-nest-meta)
   (disable plus-commutes-meta
            plus-commutes-nest-meta
            difference-lessp
            equal-transpose-meta)))

(disable equal-plus-cancel-helper)

;;; remove a cancelling pair of terms from add1/plus nests within lessp

(defn p-cancel-lessp (a)
  (if (and (equal (car a) 'lessp)
           (overlap? (cadr a) (caddr a)))
      (if (plus-remove (cadr a) (caddr a))
          '(false)
        `(lessp ,(plus-remove (cadr a)
                              (overlap? (cadr a) (caddr a)))
                ,(plus-remove (caddr a)
                              (overlap? (cadr a) (caddr a)))))
    a))

(prove-lemma lessp-eval$ (rewrite)
  (implies (equal (car a) 'lessp)
           (equal (eval$ t a y)
                  (lessp (eval$ t (cadr a) y)
                         (eval$ t (caddr a) y)))))

(prove-lemma difference-is-monotonic (rewrite)
  (and (equal (lessp (difference a b)
                     (difference c b))
              (and (lessp a c)
                   (lessp b c)))
       (equal (lessp (difference c a)
                     (difference c b))
              (and (lessp b a)
                   (lessp b c)))))

(prove-lemma lessp-plus-cancel-helper (rewrite)
  (implies (overlap? a b)
           (equal (lessp (eval$ t (plus-remove a (overlap? a b)) y)
                         (eval$ t (plus-remove b (overlap? a b)) y))
                  (lessp (eval$ t a y)
                         (eval$ t b y))))
  ((use (difference-is-monotonic
         (a (eval$ t a y))
         (b (eval$ t (overlap? a b) y))
         (c (eval$ t b y)))
        (plus-remove-subtracts (a a) (x (overlap? a b)) (y y))
        (plus-remove-subtracts (a b) (x (overlap? a b)) (y y)))
   (disable difference-is-monotonic
            plus-remove-subtracts
            lessp-transpose-meta
            equal-transpose-meta
            difference-lessp
            equal-eval$
            fix-eval$
            lessp-eval$
            times-eval$
            if-eval$
            overlap?-is-symmetric
            overlap?-implies-numberp-1
            overlap?-implies-numberp-2)))

(prove-lemma lessp-plus-cancel-meta ((meta lessp))
  (equal (eval$ t a y)
         (eval$ t (p-cancel-lessp a) y)))

(disable plus-remove-ge)
(disable plus-remove-subtracts)
(disable overlap?-implies-plus-remove)
(disable eval$-overlap?-le)
(disable lessp-plus-cancel-helper)
(disable overlap?-is-symmetric)
(disable plus-remove-implies-numberp)
(disable overlap?-implies-numberp-1)
(disable overlap?-implies-numberp-2)

(prove-lemma lessp-odometer-helper nil
  (implies (and (not (lessp z x))
                (not (lessp z y)))
           (equal (lessp (plus x (times a z))
                         (plus y (times b z)))
                  (and (numberp z)
                       (not (equal z 0))
                       (not (lessp b a))
                       (or (lessp x y)
                           (and (lessp a b)
                                (or (lessp x z)
                                    (and (numberp y)
                                         (not (equal y 0)))))
                           (lessp a (sub1 b))))))
  ((induct (difference b a)) ; for speed
   (disable lessp-times-single-linear
            sub1-plus
            sub1-times
            equal-plus-cancel-meta
            no-divisors-of-zero
            plus-associates-right
            plus-commutes-meta)))

(prove-lemma lessp-odometer-simple (rewrite)
  (implies (and (lessp a b)
                (equal (remainder c b) 0)
                (equal (remainder d b) 0))
           (and (equal (lessp (plus a c) d)
                       (lessp c d))
                (equal (lessp (plus c a) d)
                       (lessp c d))
                (equal (lessp d (plus a c))
                       (if (or (not (numberp a)) (equal a 0))
                           (lessp d c)
                         (not (lessp c d))))
                (equal (lessp d (plus c a))
                       (if (or (not (numberp a)) (equal a 0))
                           (lessp d c)
                         (not (lessp c d))))))
  ((use (lessp-odometer-helper (z b) (x a) (a (quotient c b))
                               (b (quotient d b)) (y 0))
        (lessp-odometer-helper (z b) (x 0) (a (quotient d b))
                               (b (quotient c b)) (y a)))
   (disable sub1-times
            times-plus
            times-associates-right
            times-commutes-nest
            sub1-plus
            lessp-times-both-linear
            difference-plus-arg1
            equal-plus-cancel-meta
            lessp-times-single-linear
            quotient-lessp-linear
            difference-lessp
            lessp-times-linear
            no-divisors-of-zero
            remainder-lessp-linear
            difference-not-lessp)))


(prove-lemma lessp-odometer (rewrite)
  (let ((rhs (and (numberp z)
                  (not (equal z 0))
                  (not (lessp b a))
                  (or (lessp x y)
                      (and (lessp a b)
                           (or (lessp x z)
                               (and (numberp y)
                                    (not (equal y 0)))))
                      (lessp a (sub1 b))))))
    (implies (and (not (lessp z x))
                  (not (lessp z y)))
             (and (equal (lessp (plus x (times a z))
                                (plus y (times b z)))
                         rhs)
                  (equal (lessp (plus x (times z a))
                                (plus y (times b z)))
                         rhs)
                  (equal (lessp (plus x (times a z))
                                (plus y (times z b)))
                         rhs)
                  (equal (lessp (plus x (times z a))
                                (plus y (times z b)))
                         rhs)
                  (equal (lessp (plus (times a z) x)
                                (plus y (times b z)))
                         rhs)
                  (equal (lessp (plus (times z a) x)
                                (plus y (times b z)))
                         rhs)
                  (equal (lessp (plus (times a z) x)
                                (plus y (times z b)))
                         rhs)
                  (equal (lessp (plus (times z a) x)
                                (plus y (times z b)))
                         rhs)
                  (equal (lessp (plus x (times a z))
                                (plus (times b z) y))
                         rhs)
                  (equal (lessp (plus x (times z a))
                                (plus (times b z) y))
                         rhs)
                  (equal (lessp (plus x (times a z))
                                (plus (times z b) y))
                         rhs)
                  (equal (lessp (plus x (times z a))
                                (plus (times z b) y))
                         rhs)
                  (equal (lessp (plus (times a z) x)
                                (plus (times b z) y))
                         rhs)
                  (equal (lessp (plus (times z a) x)
                                (plus (times b z) y))
                         rhs)
                  (equal (lessp (plus (times a z) x)
                                (plus (times z b) y))
                         rhs)
                  (equal (lessp (plus (times z a) x)
                                (plus (times z b) y))
                         rhs))))
  ((use (lessp-odometer-helper (a a) (b b) (x x) (y y) (z z)))
   (disable times
            lessp
            dichotomy
            lessp-times-linear
            lessp-times-single-linear
            lessp-odometer-simple
            difference-times-arg1-simplest)))

(prove-lemma lessp-half-odometer-left (rewrite)
  (let ((rhs (and (numberp z)
                  (not (equal z 0))
                  (not (lessp b a))
                  (or (and (numberp y)
                           (not (equal y 0)))
                      (lessp a b)))))
    (implies (not (lessp z y))
             (and
              (equal (lessp (times a z) (plus y (times b z))) rhs)
              (equal (lessp (times z a) (plus y (times b z))) rhs)
              (equal (lessp (times a z) (plus y (times z b))) rhs)
              (equal (lessp (times z a) (plus y (times z b))) rhs)
              (equal (lessp (times a z) (plus (times b z) y)) rhs)
              (equal (lessp (times z a) (plus (times b z) y)) rhs)
              (equal (lessp (times a z) (plus (times z b) y)) rhs)
              (equal (lessp (times z a) (plus (times z b) y)) rhs)
              )))
  ((use (lessp-odometer (a a) (b b) (x 0) (y y) (z z)))
   (disable lessp-odometer
            sub1-times
            sub1-plus
            no-divisors-of-zero
            plus-is-0)))

(prove-lemma lessp-half-odometer-right (rewrite)
  (let ((rhs (and (numberp z)
                  (not (equal z 0))
                  (lessp a b)
                  (or (not (equal z x))
                      (lessp a (sub1 b))))))
    (implies (not (lessp z x))
             (and
              (equal (lessp (plus x (times a z)) (times b z)) rhs)
              (equal (lessp (plus x (times z a)) (times b z)) rhs)
              (equal (lessp (plus x (times a z)) (times z b)) rhs)
              (equal (lessp (plus x (times z a)) (times z b)) rhs)
              (equal (lessp (plus (times a z) x) (times b z)) rhs)
              (equal (lessp (plus (times z a) x) (times b z)) rhs)
              (equal (lessp (plus (times a z) x) (times z b)) rhs)
              (equal (lessp (plus (times z a) x) (times z b)) rhs)
              ))))

(prove-lemma lessp-quarter-odometer-left (rewrite)
  (let ((rhs1 (if (or (not (numberp c))
                      (equal c 0))
                  (lessp b a)
                (if (or (equal (sub1 c) 0)
                        (not (numberp b))
                        (equal b 0))
                    (and (numberp a)
                         (not (equal a 0)))
                  t)))
        (rhs2 (if (or (not (numberp c))
                      (equal c 0)
                      (not (numberp d))
                      (equal d 0))
                  (lessp b a)
                (if (or (not (numberp b))
                        (equal b 0)
                        (and (equal (sub1 c) 0)
                             (equal (sub1 d) 0)))
                    (and (numberp a)
                         (not (equal a 0)))
                  t))))
    (and
     (equal (lessp b (plus a (times b c))) rhs1)
     (equal (lessp b (plus (times b c) a)) rhs1)
     (equal (lessp b (plus a (times c b))) rhs1)
     (equal (lessp b (plus (times c b) a)) rhs1)
     (equal (lessp b (plus a (times c (times d b)))) rhs2)
     (equal (lessp b (plus a (times c (times b d)))) rhs2)
     (equal (lessp b (plus (times c (times d b)) a)) rhs2)
     (equal (lessp b (plus (times c (times b d)) a)) rhs2)))
  ((induct (difference a b))
   (disable plus-commutes-meta
            plus-commutes-nest-meta
            lessp-times-single-linear
            sub1-times)))


(prove-lemma lessp-quarter-odometer-right (rewrite)
  (let ((rhs1 (and (lessp a b)
                   (or (not (numberp c))
                       (equal c 0))))
        (rhs2 (and (lessp a b)
                   (or (not (numberp c))
                       (equal c 0)
                       (not (numberp d))
                       (equal d 0)))))
    (and (equal (lessp (plus a (times b c)) b) rhs1)
         (equal (lessp (plus (times b c) a) b) rhs1)
         (equal (lessp (plus a (times c b)) b) rhs1)
         (equal (lessp (plus (times c b) a) b) rhs1)
         (equal (lessp (plus a (times c (times d b))) b) rhs2)
         (equal (lessp (plus (times c (times d b)) a) b) rhs2)
         (equal (lessp (plus a (times c (times b d))) b) rhs2)
         (equal (lessp (plus (times c (times b d)) a) b) rhs2)))
  ((induct (difference a b))
   (disable difference-times-arg1-simplest
            lessp-times-single-linear
            difference-times-arg1
            sub1-times
            plus-commutes-meta
            plus-commutes-nest-meta
            lessp-odometer-simple
            difference-times-arg1-simpler)))

;;; This appears costly, but the free variable b may make it efficient.

(prove-lemma equal-odometer-simple (rewrite)
  (let ((rhs (and (or (not (numberp a)) (equal a 0))
                  (numberp d)
                  (or (equal c d)
                      (and (equal d 0)
                           (not (numberp c)))))))
    (implies (and (lessp a b)
                  (equal (remainder c b) 0)
                  (equal (remainder d b) 0))
             (and (equal (equal (plus a c) d) rhs)
                  (equal (equal (plus c a) d) rhs)
                  (equal (equal d (plus a c)) rhs)
                  (equal (equal d (plus c a)) rhs))))
  ((induct (lessp-quotient-ind c d b))
   (disable difference-lessp
            equal-transpose-meta
            lessp-transpose-meta
            difference-0
            sub1-difference
            plus-commutes-meta)))

(prove-lemma equal-odometer (rewrite)
  (implies (and (lessp a z)
                (lessp b z))
           (and (equal (equal (plus a (times z x))
                              (plus b (times z y)))
                       (and (equal (fix a) (fix b))
                            (equal (fix x) (fix y))))
                (equal (equal (plus (times z x) a)
                              (plus b (times z y)))
                       (and (equal (fix a) (fix b))
                            (equal (fix x) (fix y))))
                (equal (equal (plus a (times z x))
                              (plus (times z y) b))
                       (and (equal (fix a) (fix b))
                            (equal (fix x) (fix y))))
                (equal (equal (plus (times z x) a)
                              (plus (times z y) b))
                       (and (equal (fix a) (fix b))
                            (equal (fix x) (fix y))))
                (equal (equal (plus a (times x z))
                              (plus b (times z y)))
                       (and (equal (fix a) (fix b))
                            (equal (fix x) (fix y))))
                (equal (equal (plus (times x z) a)
                              (plus b (times z y)))
                       (and (equal (fix a) (fix b))
                            (equal (fix x) (fix y))))
                (equal (equal (plus a (times x z))
                              (plus (times z y) b))
                       (and (equal (fix a) (fix b))
                            (equal (fix x) (fix y))))
                (equal (equal (plus (times x z) a)
                              (plus (times z y) b))
                       (and (equal (fix a) (fix b))
                            (equal (fix x) (fix y))))
                (equal (equal (plus a (times z x))
                              (plus b (times y z)))
                       (and (equal (fix a) (fix b))
                            (equal (fix x) (fix y))))
                (equal (equal (plus (times z x) a)
                              (plus b (times y z)))
                       (and (equal (fix a) (fix b))
                            (equal (fix x) (fix y))))
                (equal (equal (plus a (times z x))
                              (plus (times y z) b))
                       (and (equal (fix a) (fix b))
                            (equal (fix x) (fix y))))
                (equal (equal (plus (times z x) a)
                              (plus (times y z) b))
                       (and (equal (fix a) (fix b))
                            (equal (fix x) (fix y))))
                (equal (equal (plus a (times x z))
                              (plus b (times y z)))
                       (and (equal (fix a) (fix b))
                            (equal (fix x) (fix y))))
                (equal (equal (plus (times x z) a)
                              (plus b (times y z)))
                       (and (equal (fix a) (fix b))
                            (equal (fix x) (fix y))))
                (equal (equal (plus a (times x z))
                              (plus (times y z) b))
                       (and (equal (fix a) (fix b))
                            (equal (fix x) (fix y))))
                (equal (equal (plus (times x z) a)
                              (plus (times y z) b))
                       (and (equal (fix a) (fix b))
                            (equal (fix x) (fix y))))))
  ((induct (difference x y))
   (disable equal-odometer-simple
            lessp-times-both-linear
            times-plus
            sub1-times
            no-divisors-of-zero
            times-zerop
            plus-is-0
            equal-plus-cancel-meta
            lessp-times-single-linear)))

(prove-lemma equal-half-odometer (rewrite)
  (implies (lessp b z)
           (and (equal (equal (times z x)
                              (plus b (times z y)))
                       (and (or (not (numberp b))
                                (equal b 0))
                            (equal (fix x) (fix y))))
                (equal (equal (times z x)
                              (plus (times z y) b))
                       (and (or (not (numberp b))
                                (equal b 0))
                            (equal (fix x) (fix y))))
                (equal (equal (times x z)
                              (plus b (times z y)))
                       (and (or (not (numberp b))
                                (equal b 0))
                            (equal (fix x) (fix y))))
                (equal (equal (times x z)
                              (plus (times z y) b))
                       (and (or (not (numberp b))
                                (equal b 0))
                            (equal (fix x) (fix y))))
                (equal (equal (times z x)
                              (plus b (times y z)))
                       (and (or (not (numberp b))
                                (equal b 0))
                            (equal (fix x) (fix y))))
                (equal (equal (times z x)
                              (plus (times y z) b))
                       (and (or (not (numberp b))
                                (equal b 0))
                            (equal (fix x) (fix y))))
                (equal (equal (times x z)
                              (plus b (times y z)))
                       (and (or (not (numberp b))
                                (equal b 0))
                            (equal (fix x) (fix y))))
                (equal (equal (times x z)
                              (plus (times y z) b))
                       (and (or (not (numberp b))
                                (equal b 0))
                            (equal (fix x) (fix y))))

                (equal (equal (plus b (times z y))
                              (times z x))
                       (and (or (not (numberp b))
                                (equal b 0))
                            (equal (fix x) (fix y))))
                (equal (equal (plus (times z y) b)
                              (times z x))
                       (and (or (not (numberp b))
                                (equal b 0))
                            (equal (fix x) (fix y))))
                (equal (equal (plus b (times z y))
                              (times x z))
                       (and (or (not (numberp b))
                                (equal b 0))
                            (equal (fix x) (fix y))))
                (equal (equal (plus (times z y) b)
                              (times x z))
                       (and (or (not (numberp b))
                                (equal b 0))
                            (equal (fix x) (fix y))))
                (equal (equal (plus b (times y z))
                              (times z x))
                       (and (or (not (numberp b))
                                (equal b 0))
                            (equal (fix x) (fix y))))
                (equal (equal (plus (times y z) b)
                              (times z x))
                       (and (or (not (numberp b))
                                (equal b 0))
                            (equal (fix x) (fix y))))
                (equal (equal (plus b (times y z))
                              (times x z))
                       (and (or (not (numberp b))
                                (equal b 0))
                            (equal (fix x) (fix y))))
                (equal (equal (plus (times y z) b)
                              (times x z))
                       (and (or (not (numberp b))
                                (equal b 0))
                            (equal (fix x) (fix y))))))
  ((use (equal-odometer (a 0) (b b) (x x) (y y) (z z)))
   (disable equal-odometer
            equal-odometer-simple
            difference-times-arg1-simplest
            lessp-times-cancel-meta
            sub1-times)))

(prove-lemma equal-quarter-odometer (rewrite)
  (let ((rhs1 (and (numberp b)
                   (if (or (not (numberp c))
                           (equal c 0))
                       (if (numberp a)
                           (equal a b)
                         (equal b 0))
                     (if (equal (sub1 c) 0)
                         (or (not (numberp a))
                             (equal a 0))
                       (and (equal b 0)
                            (or (not (numberp a))
                                (equal a 0)))))))
        (rhs2 (and (numberp b)
                   (if (or (not (numberp c))
                           (equal c 0)
                           (not (numberp d))
                           (equal d 0))
                       (if (numberp a)
                           (equal a b)
                         (equal b 0))
                     (if (and (equal (sub1 c) 0)
                              (equal (sub1 d) 0))
                         (or (not (numberp a))
                             (equal a 0))
                       (and (equal b 0)
                            (or (not (numberp a))
                                (equal a 0))))))))
    (and
     (equal (equal b (plus a (times b c))) rhs1)
     (equal (equal b (plus (times b c) a)) rhs1)
     (equal (equal b (plus a (times c b))) rhs1)
     (equal (equal b (plus (times c b) a)) rhs1)
     (equal (equal (plus a (times b c)) b) rhs1)
     (equal (equal (plus (times b c) a) b) rhs1)
     (equal (equal (plus a (times c b)) b) rhs1)
     (equal (equal (plus (times c b) a) b) rhs1)

     (equal (equal b (plus a (times c (times d b)))) rhs2)
     (equal (equal b (plus a (times c (times b d)))) rhs2)
     (equal (equal b (plus (times c (times d b)) a)) rhs2)
     (equal (equal b (plus (times c (times b d)) a)) rhs2)
     (equal (equal (plus a (times c (times d b))) b) rhs2)
     (equal (equal (plus a (times c (times b d))) b) rhs2)
     (equal (equal (plus (times c (times d b)) a) b) rhs2)
     (equal (equal (plus (times c (times b d)) a) b) rhs2)))
  ((disable sub1-times
            sub1-plus
            times-associates-right
            lessp-facts
            plus-commutes-meta
            plus-commutes-nest-meta
            times-plus)))

;;; Provide a meta rule to cancel complementary terms within a plus nest.

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

;;; parses a summand, returning a list of (a . b)'s, where "a" is a subtrahend
;;; and "b" is either nil or a multiplier of the subtrahend.  We assume that
;;; x is a summand in normal form.  We treat only the simplest and most
;;; commonly occurring cases, i.e. we ignore times nests and do not expand
;;; products of differences.  The latter simplification is justified by
;;; reducing the complexity of rewrites, and the former has the weak
;;; justification of possibly improving the run time performance of meta-plus
;;; and certainly reducing the programming complexity of this meta rule.

(defn parse-term-neg (x)
  (if (equal (car x) 'difference)
      (list (list (caddr x))) ; ? - a
    (if (equal (car x) 'times)
        (if (equal (caadr x) 'difference)
            (if (equal (caaddr x) 'difference)
                (list (cons (caddadr x) (caddr x)) ; (? - a) * b
                      (cons (caddaddr x) (cadr x))) ; b * (? - a)
              (list (cons (caddadr x) (caddr x))))  ; (? - a) * b
          (if (equal (caaddr x) 'difference)
              (list (cons (caddaddr x) (cadr x))) ; b * (? - a)
            nil))
      nil)))

;;; Extract a list of all (subtrahend)'s and (subtrahend . multiplier)'s
;;; from the plus nest x.  We assume that x is in normal form.

(defn collect-neg (x)
  (if (listp x)
      (if (equal (car x) 'plus)
          (append (parse-term-neg (cadr x))
                  (collect-neg (caddr x)))
        (parse-term-neg x))
    nil))

;;; Find a pair (a . b) from y such that a * b (or just "a" if b is nil)
;;; occurs as a summand or minuend (after distributing times over difference)
;;; in x.  flg is used to prevent full exploration of plus nests in the first
;;; argument of plus (which should not happen if x is normalized).
;;; We do not treat the commutative version of (a . b) because the resulting
;;; rewrite would introduce an inversion of the nesting order.

(defn find-comp (flg x y)
  (if (member (list x) y)
      (list x) ; a
    (if (listp x)
        (if (and (equal (car x) 'difference)
                 (member (list (cadr x)) y))
            (list (cadr x)) ; a - ?
          (if (equal (car x) 'times)
              (if (member (cons (cadr x) (caddr x)) y)
                  (cons (cadr x) (caddr x)) ; a * b
                (if (member (cons (caddr x) (cadr x)) y)
                    (cons (caddr x) (cadr x)) ; b * a
                  (if (and (equal (caadr x) 'difference)
                           (member (cons (cadadr x) (caddr x)) y))
                      (cons (cadadr x) (caddr x)) ; (a - ?) * b
                    (if (and (equal (caaddr x) 'difference)
                             (member (cons (cadaddr x) (cadr x)) y))
                        (cons (cadaddr x) (cadr x)) ; b * (a - ?)
                      f))))
            (if (and flg
                     (equal (car x) 'plus))
                (if (find-comp f (cadr x) y)
                    (find-comp f (cadr x) y)
                  (find-comp t (caddr x) y))
              f)))
      f)))

;;; recognizer predicate for complementary positive term
;;; (We do not use is-pos? within find-comp for efficiency reasons.)
;;; x is a summand, y is an (a . b) pair

(defn is-pos? (x y)
  (and (listp y)
       (if (equal (cdr y) nil)
           (or (equal x (car y))
               (equal x `(difference ,(car y) ,(caddr x))))
         (or (equal x `(times ,(car y) ,(cdr y)))
             (equal x `(times ,(cdr y) ,(car y)))
             (equal x `(times (difference ,(car y) ,(caddadr x)) ,(cdr y)))
             (equal x `(times ,(cdr y)
                              (difference ,(car y) ,(caddaddr x))))))))

;;; Identify first complementary positive term.
;;; x is a plus nest, y is an (a . b) pair

(defn first-pos (x y)
  (if (is-pos? x y)
      x
    (if (and (listp x)
             (equal (car x) 'plus))
        (if (is-pos? (cadr x) y)
            (cadr x)
          (first-pos (caddr x) y))
      f)))

;;; delete the first positive occurrence of y from the plus nest x

(defn delete-pos (x y)
  (if (is-pos? x y)
      '(zero)
    (if (and (listp x) (equal (car x) 'plus))
        (if (is-pos? (cadr x) y)
            (caddr x)
          (if (is-pos? (caddr x) y)
              (cadr x)
            (list 'plus (cadr x) (delete-pos (caddr x) y))))
      x)))

(prove-lemma delete-pos-subtracts (rewrite)
  (equal (plus (eval$ t (first-pos x y) a)
               (eval$ t (delete-pos x y) a))
         (fix (eval$ t x a)))
  ((induct (first-pos x y))
   (disable is-pos?)))

;;; recognizer predicate for negative complementary term
;;; x is a summand, y is an (a . b) pair

(defn is-neg? (x y)
  (and (listp y)
       (if (equal (cdr y) nil)
           (equal x `(difference ,(cadr x) ,(car y)))
         (or (equal x `(times (difference ,(cadadr x) ,(car y)) ,(cdr y)))
             (equal x `(times ,(cdr y) (difference ,(cadaddr x) ,(car y))))))))

;;; Identify the first negative occurrence of y in the plus nest x.  We assume
;;; that x is the result of applying delete-pos.

(defn first-neg (x y)
  (if (is-neg? x y)
      x
    (if (and (listp x) (equal (car x) 'plus))
        (if (is-neg? (cadr x) y)
            (cadr x)
          (first-neg (caddr x) y))
      '(zero))))
; We do not return f here because delete-pos may have eliminated the negative
; occurrence as well.

;;; Delete the first negative occurrence of y from the plus nest x.

(defn delete-neg (x y)
  (if (is-neg? x y)
      '(zero)
    (if (and (listp x) (equal (car x) 'plus))
        (if (is-neg? (cadr x) y)
            (caddr x)
          (if (is-neg? (caddr x) y)
              (cadr x)
            (list 'plus (cadr x) (delete-neg (caddr x) y))))
      x))) ; y should be such that this does not happen

(prove-lemma delete-neg-subtracts (rewrite)
  (and (equal (plus (eval$ t (first-neg x y) a)
                    (eval$ t (delete-neg x y) a))
              (fix (eval$ t x a)))
       (equal (plus (eval$ t (delete-neg x y) a)
                    (eval$ t (first-neg x y) a))
              (fix (eval$ t x a))))
  ((induct (first-neg x y))
   (disable is-neg?)))

;;; Compose a new reduced term equivalent to x + y.
;;; We use the orientation (lessp ,(cadr y) ,(caddr y)) to encourage function
;;; expansion.  We assume that y is generated from first-neg.

(defn compose (x y)               ; x + y
  (if (equal (car y) 'difference) ; x + (? - ?)
      (if (equal x (caddr y))     ; x + (? - x)
          `(if (lessp ,(cadr y) ,(caddr y))
               (fix ,x)
             (fix ,(cadr y)))
        (if (and (equal (car x) 'difference) ; (? - ?) + (? - ?)
                 (equal (cadr x) (caddr y))) ; (a - ?) + (? - a)
            `(if (lessp ,(cadr y) ,(caddr y))
                 ,x
               (if (lessp ,(cadr x) ,(caddr x))
                   ,y
                 (difference ,(cadr y) ,(caddr x))))
          `(plus ,x ,y))) ; should not happen
    (if (and (equal (car y) 'times) (equal (car x) 'times))
        (if (equal (caadr y) 'difference) ; (? * ?) + ((? - ?) * ?)
            (if (or (equal x `(times ,(caddadr y) ,(caddr y))) ; (a * b) +
                    (equal x `(times ,(caddr y) ,(caddadr y)))) ; ((? - a) * b)
                `(if (lessp ,(cadadr y) ,(caddadr y))
                     ,x
                   (times ,(cadadr y) ,(caddr y)))
              (if (and (equal (caadr x) 'difference) ; ((b - ?) * a) +
                       (equal (caddr x) (caddr y))   ; ((? - b) * a)
                       (equal (cadadr x) (caddadr y)))
                  `(if (lessp ,(cadadr y) ,(caddadr y))
                       ,x
                     (if (lessp ,(cadadr x) ,(caddadr x))
                         ,y
                       (times (difference ,(cadadr y) ,(caddadr x))
                              ,(caddr y))))
                (if (and (equal (caaddr x) 'difference) ; (a * (b - ?)) +
                         (equal (cadr x) (caddr y)) ; ((? - b) * a)
                         (equal (cadaddr x) (caddadr y)))
                    `(if (lessp ,(cadadr y) ,(caddadr y))
                         ,x
                       (if (lessp ,(cadaddr x) ,(caddaddr x))
                           ,y
                         (times (difference ,(cadadr y) ,(caddaddr x))
                                ,(caddr y))))
                  `(plus ,x ,y))))     ; should not happen
          (if (equal (caaddr y) 'difference) ; (? * ?) + (? * (? - ?))
              (if (or (equal x `(times ,(caddaddr y) ,(cadr y))) ; (a * b) +
                      (equal x `(times ,(cadr y) ,(caddaddr y)))) ; b * (? - a)
                  `(if (lessp ,(cadaddr y) ,(caddaddr y))
                       ,x
                     (times ,(cadr y) ,(cadaddr y)))
                (if (and (equal (caadr x) 'difference) ; ((b - ?) * a) +
                         (equal (caddr x) (cadr y))    ; (a * (? - b))
                         (equal (caddaddr y) (cadadr x)))
                    `(if (lessp ,(cadaddr y) ,(caddaddr y))
                         ,x
                       (if (lessp ,(cadadr x) ,(caddadr x))
                           ,y
                         (times ,(cadr y)
                                (difference ,(cadaddr y) ,(caddadr x)))))
                  (if (and (equal (caaddr x) 'difference) ; (a * (b - ?)) +
                           (equal (cadr x) (cadr y)) ; (a * (? - b))
                           (equal (cadaddr x) (caddaddr y)))
                      `(if (lessp ,(cadaddr y) ,(caddaddr y))
                           ,x
                         (if (lessp ,(cadaddr x) ,(caddaddr x))
                             ,y
                           (times ,(cadr y)
                                  (difference ,(cadaddr y) ,(caddaddr x)))))
                    `(plus ,x ,y)))) ; should not happen
            `(plus ,x ,y)))          ; should not happen
      (if (equal y '(zero)) ; only arises if difference-lessp is disabled
          (if (and (equal (car x) 'difference)
                   (equal (cadr x) (caddr x)))
              '(zero)
            `(fix ,x))
        `(plus ,x ,y))))) ; should not happen

(prove-lemma compose-helper (rewrite)
  (and (equal (plus (times d b) (times d (difference a b)))
              (if (lessp a b)
                  (times d b)
                (times d a)))
       (equal (plus (times b d) (times d (difference a b)))
              (if (lessp a b)
                  (times d b)
                (times d a)))))

(prove-lemma compose-is-correct (rewrite)
  (equal (eval$ t (compose x y) a)
         (plus (eval$ t x a) (eval$ t y a)))
  ((enable plus-commutes
           plus-commutes-nest)
   (disable eval$
            plus-commutes-meta
            plus-commutes-nest-meta
            plus-difference-commutes-meta
            lessp-eval$
            if-eval$
            equal-eval$
            fix-eval$
            equal-half-odometer
            difference-lessp
            equal-transpose-meta
            lessp-transpose-meta
            dichotomy
            difference-eval$
            plus-eval$
            sub1-times
            sub1-difference
            lessp-times-single-linear
            difference-not-lessp)))

;;; Remove complementary pair from plus nest.

(defn diff-cancel (a)
  (let ((y (find-comp t a (collect-neg a))))
    (if y
        (let ((x (delete-pos a y)))
          `(plus
            ,(compose (first-pos a y) (first-neg x y))
            ,(delete-neg x y)))
      a)))

(prove-lemma meta-plus-helper-1 (rewrite)
  (equal (plus (eval$ t (first-pos a y) b)
               (eval$ t (delete-neg (delete-pos a y) y) b)
               (eval$ t (first-neg (delete-pos a y) y) b))
         (fix (eval$ t a b)))
  ((induct (first-pos a y))
   (disable is-pos?
            plus-commutes-meta
            plus-commutes-nest-meta
            lessp-eval$
            if-eval$
            times-eval$
            equal-eval$
            fix-eval$)))

(prove-lemma meta-plus-helper-2 (rewrite)
  (implies (find-comp t a (collect-neg a))
           (numberp (eval$ t a b)))
  ((induct (collect-neg a))))

(disable delete-neg-subtracts)

(prove-lemma meta-plus ((meta plus))
  (equal (eval$ t a b)
         (eval$ t (diff-cancel a) b))
  ((enable plus-commutes
           plus-commutes-nest)
   (disable plus-commutes-meta
            plus-commutes-nest-meta
            compose)))

(disable delete-pos-subtracts)
(disable compose-helper)
(disable compose-is-correct)
(disable meta-plus-helper-1)
(disable meta-plus-helper-2)

(prove-lemma quotient-is-unique-temp nil
  (implies (lessp c b)
           (equal (quotient (plus c (times a b)) b)
                  (if (numberp a) a 0)))
  ((induct (times a b))))

;;; Add quotient and remainder to nesting order as follows
;;; add1, plus, times, remainder, quotient, difference, sub1

;;; J does not like the idea of introducing 1 less than the modulus/dividend
;;; in proofs where the modulus is constant.  My only come back was that this
;;; allows more possibilities for induction (say inducting on the modulus).
;;; J then proved the only example of this within the present file
;;; (lessp-quotient-arg2-linear) without inducting on the modulus.

(prove-lemma quotient-add1-arg2-helper-1 nil
  (implies (and (not (lessp (sub1 q) r))
                (lessp r b)
                (equal a (plus r (times b q)))
                (not (lessp a (plus (sub1 q) (times b (sub1 q))))))
           (equal (quotient a (add1 b))
                  (sub1 q)))
  ((use (quotient-is-unique-temp
         (a (sub1 q))
         (b (add1 b))
         (c (difference (plus b r) (sub1 q)))))
   (disable lessp-transpose-meta
            difference-plus-arg1
            difference-plus-arg2
            difference-lessp
            dichotomy
            equal-transpose-meta
            lessp-times-single-linear
            equal-odometer-simple
            lessp-quotient-arg1-linear
            sub1-times
            lessp-times-both-linear
            difference-add1
            times-plus
            no-divisors-of-zero
            difference-times-arg1-simplest
            lessp-times-cancel-meta
            lessp-times-linear
            plus-associates-right
            difference-not-lessp
            difference-times-arg1-meta
            remainder-lessp-linear)))

(prove-lemma quotient-add1-arg2-helper-2 nil
  (implies (and (numberp q)
                (lessp (sub1 q) r)
                (lessp r b)
                (equal a (plus r (times b q)))
                (not (lessp a (plus (sub1 q) (times b (sub1 q))))))
           (equal (quotient a (add1 b))
                  q))
  ((use (quotient-is-unique-temp (a q)
                                 (b (add1 b))
                                 (c (difference r q))))
   (disable lessp-transpose-meta
            lessp-odometer-simple
            equal-odometer-simple
            difference-times-arg1-simplest
            lessp-quotient-arg1-linear
            difference-times-arg1
            sub1-times
            sub1-plus
            difference-times-arg1-simpler
            no-divisors-of-zero
            plus-is-0
            difference-plus-arg1
            difference-not-lessp)))

(prove-lemma remainder-as-quotient nil
  (equal (remainder a b)
         (difference a (times b (quotient a b))))
  ((use (quotient-remainder-rewrite (a a) (b b)))
   (disable quotient-remainder-rewrite
            quotient-remainder
            quotient
            remainder
            difference-times-arg2)))

;;; quotient-add1-arg2 was derived using the following calculations:
;;;
;;; Let a = q*b + r = p*(b + 1) + s, where r < b and s < b + 1, and p = q - k.
;;;
;;; p = q - k <=> q*b + r = (q - k)*(b + 1) + s
;;;           <=> r + k*(b + 1) = s + q
;;;           <=> r + (k - 1)*(b + 1) < q <= r + k*(b + 1) for k > 0, and
;;;               q <= r for k = 0
;;;
;;; The last equivalence allows us to define k in terms of q and r.  We treat
;;; only the case k = 0 and k = 1 in the lemma quotient-add1-arg2.  In either
;;; case we have
;;;
;;; q <= r + b + 1, or equivalently
;;;
;;; (b + 1)*(q - 1) <= a, or equivalently
;;;
;;; a <= (b + 1)*(r + b)
;;;
;;; Since we know that the right hand side of quotient-add1-arg2 will involve
;;; q - 1, we choose (b + 1)*(q - 1) <= a as the hypothesis rather than the
;;; expression involving r.  This avoids having to simplify (remainder a b)
;;; in the hypothesis and (quotient (difference a b) b) in the conclusion.
;;; Instead, using the temporary variable qdab, we simplify
;;; (quotient (difference a b) b) only once.

;;; canonical

(prove-lemma quotient-add1-arg2 (rewrite)
  (implies (and (equal qdab (quotient (difference a b) b))
                (not (lessp a (plus qdab (times b qdab)))))
           (equal (quotient a (add1 b))
                  (if (lessp (plus b qdab (times b qdab)) a)
                      (if (or (not (numberp b))
                              (equal b 0))
                          a
                        (add1 qdab))
                    qdab)))
  ((use (quotient-add1-arg2-helper-1 (a a)
                                     (b b)
                                     (r (difference (difference a b)
                                                    (times b qdab)))
                                     (q (add1 qdab)))
        (quotient-add1-arg2-helper-2 (a a)
                                     (b b)
                                     (r (difference (difference a b)
                                                    (times b qdab)))
                                     (q (add1 qdab)))
        (remainder-as-quotient (a a) (b b)))
   (disable lessp-transpose-meta
            equal-transpose-meta
            difference-lessp
            lessp-quotient-arg1-linear
            dichotomy
            lessp-times-single-linear
            lessp-odometer-simple
            equal-odometer-simple
            sub1-difference
            times-plus
            lessp-times-both-linear
            times-commutes-nest
            difference-plus-arg1
            difference-not-lessp
            difference-times-arg2-preferred)))

;;; remainder-add1-arg2 uses the same calculations as quotient-add1-arg2.
;;; In particular k is defined by
;;;
;;; r + k*(b + 1) = s + q
;;;
;;; r < q <=> k > 0
;;;

;;; canonical

(prove-lemma remainder-add1-arg2 (rewrite)
  (implies (and (equal qdab (quotient (difference a b) b))
                (not (lessp a (plus qdab (times b qdab)))))
           (equal (remainder a (add1 b))
                  (if (lessp (plus b qdab (times b qdab)) a)
                      (if (or (not (numberp b))
                              (equal b 0))
                          0
                        (remainder
                         (difference (sub1 a) qdab) b))
                    (if (lessp a b)
                        (if (numberp a) a 0)
                      (difference b (difference qdab
                                                (remainder a b)))))))
  ((use (remainder-as-quotient (a a) (b (add1 b)))
        (remainder-as-quotient (a a) (b b))
        (difference-remainder-arg1 (a a) (b (quotient a b)) (c b)))
   (disable difference-remainder-arg1
            difference-times-arg2 ; needed
            lessp-transpose-meta
            equal-transpose-meta
            difference-lessp
            lessp-times-single-linear
            dichotomy
            difference-difference-arg1-commutes-meta
            lessp-quotient-arg1-linear
            times-plus
            difference-times-arg2-preferred
            sub1-difference
            sub1-plus
            difference-not-lessp
            remainder-lessp-linear
            lessp-times-both-linear
            sub1-times)))

;;; We include the following lemma to cover alternative formulations of the
;;; hypothesis of remainder-add1-arg2

(prove-lemma remainder-add1-arg2-trigger (rewrite)
  (implies (not (lessp (plus b (remainder a b))
                       (quotient (difference a b) b)))
           (equal (lessp
                   a
                   (plus
                    (quotient (difference a b) b)
                    (times b (quotient (difference a b) b))))

                  f))
  ((disable lessp-transpose-meta
            difference-lessp
            lessp-times-single-linear
            times-plus
            sub1-times)))

;;; canonical

(prove-lemma quotient-add1-arg2-trigger (rewrite)
  (implies (lessp a (plus b b (times b b)))
           (equal
            (lessp a (plus (quotient (difference a b) b)
                           (times b (quotient (difference a b) b))))
            f))
  ((induct (quotient a b))
   (disable lessp-transpose-meta
            equal-transpose-meta
            lessp-times-single-linear
            times-associates-right
            sub1-times
            difference-lessp
            lessp-times-both-linear
            equal-odometer-simple
            times-commutes-nest
            dichotomy
            difference-plus-arg2
            lessp-odometer-simple
            sub1-difference
            equal-plus-cancel-meta
            difference-difference-arg1-commutes-meta
            difference-not-lessp)))

(prove-lemma quotient-add1-arg1-helper nil
  (equal (quotient (add1 a) b)
         (if (or (not (numberp b)) (equal b 0))
             0
           (if (equal (remainder a b) (sub1 b))
               (add1 (quotient a b))
             (quotient a b))))
  ((disable lessp-transpose-meta
            lessp-times-single-linear
            quotient-add1-arg2
            difference-plus-arg1
            equal-transpose-meta
            sub1-difference
            difference-times-arg2
            difference-plus-arg2
            sub1-times
            dichotomy
            difference-times-arg2-preferred
            equal-quarter-odometer
            no-divisors-of-zero
            sub1-plus
            equal-times-cancel-meta
            quotient-difference-arg1)))

;;; canonical (qab avoids repeated rewriting)

(prove-lemma quotient-add1-arg1 (rewrite)
  (implies (equal qab (quotient a b))
           (equal (quotient (add1 a) b)
                  (if (or (not (numberp b)) (equal b 0))
                      0
                    (if (equal (remainder a b) (sub1 b))
                        (add1 qab)
                      qab))))
  ((use (quotient-add1-arg1-helper (a a) (b b)))))

;;; canonical (preferred)

(prove-lemma remainder-add1-arg2-simple (rewrite)
  (and (equal (remainder (plus a (times b a)) (add1 b)) 0)
       (equal (remainder (plus a (times a b)) (add1 b)) 0))
  ((use (times-add1 (a a) (b b))) ; for speed
   (disable times-add1
            remainder-add1-arg2
            plus-associates-right
            plus-commutes
            difference-lessp
            lessp-times-single-linear
            sub1-times
            lessp-times-cancel-meta
            difference-times-arg1-simplest
            difference-times-arg1
            difference-plus-arg2
            difference-times-arg2
            lessp-transpose-meta
            equal-transpose-meta)))

(prove-lemma remainder-plus-arg1-helper (rewrite)
  (equal (remainder (plus c d (times b a)) b)
         (remainder (plus c d) b))
  ((induct (times a b))
   (disable dichotomy
            times-plus
            sub1-times
            difference-times-arg1-simplest
            lessp-times-single-linear
            lessp-transpose-meta
            difference-lessp
            plus-is-0
            sub1-plus
            difference-times-arg1
            equal-transpose-meta
            sub1-difference)))

(prove-lemma remainder-plus-arg1-helper-1 nil
  (equal (remainder (plus a b) c)
         (if (lessp (plus (remainder a c)
                          (remainder b c))
                    c)
             (plus (remainder a c) (remainder b c))
           (if (or (not (numberp c))
                   (equal c 0))
               (plus a b)
             (difference (remainder a c)
                         (difference c
                                     (remainder b c))))))
  ((induct (remainder a c))
   (expand (remainder (plus a b) c))
   (disable lessp-transpose-meta
            equal-transpose-meta
            quotient-add1-arg2
            remainder-add1-arg2
            dichotomy
            sub1-times
            lessp-times-single-linear
            lessp-odometer-simple
            difference-times-arg1-simplest
            sub1-plus
            difference-is-monotonic
            lessp-times-cancel-meta
            remainder-lessp-linear
            difference-not-lessp
            difference-0)))

;;; canonical (rac and rbc avoid repeated rewriting)

(prove-lemma remainder-plus-arg1 (rewrite)
  (implies (and (equal rac (remainder a c))
                (equal rbc (remainder b c)))
           (equal (remainder (plus a b) c)
                  (if (lessp (plus rac rbc) c)
                      (plus rac rbc)
                    (if (or (not (numberp c))
                            (equal c 0))
                        (plus a b)
                      (difference rac (difference c rbc))))))
  ((use (remainder-plus-arg1-helper-1 (a a) (b b) (c c)))))

(disable remainder-plus-arg1-helper)

(prove-lemma quotient-plus-arg1-helper nil
  (implies (and (lessp r c)
                (lessp s c))
           (equal (quotient (plus (plus r (times a c))
                                  (plus s (times b c)))
                            c)
                  (if (lessp (plus r s) c)
                      (plus a b)
                    (add1 (plus a b)))))
  ((induct (plus a b))
   (do-not-generalize t)
   (disable lessp-transpose-meta
            dichotomy
            lessp-times-single-linear
            times-plus
            sub1-times
            equal-transpose-meta
            equal-odometer-simple
            difference-times-arg1-simplest
            lessp-odometer-simple
            sub1-difference
            sub1-plus
            no-divisors-of-zero
            difference-0
            difference-not-lessp)))

;;; canonical

(prove-lemma quotient-plus-arg1 (rewrite)
  (implies (equal ans (plus (quotient a c) (quotient b c)))
           (equal (quotient (plus a b) c)
                  (if (or (not (numberp c))
                          (equal c 0))
                      0
                    (if (lessp (plus a b) (plus c (times c ans)))
                        ans
                      (add1 ans)))))
  ((use (quotient-plus-arg1-helper (r (remainder a c))
                                   (s (remainder b c))
                                   (a (quotient a c))
                                   (b (quotient b c))))
   (disable dichotomy
            sub1-times
            difference-times-arg1-simplest
            difference-times-arg1
            difference-times-arg1-simpler
            lessp-transpose-meta
            equal-transpose-meta
            difference-plus-arg2
            lessp-times-single-linear
            remainder-plus-arg1
            lessp-odometer-simple
            remainder
            no-divisors-of-zero
            difference-lessp
            difference-0
            sub1-difference
            quotient-lessp-linear
            lessp-times-linear
            sub1-plus
            lessp-times-cancel-meta
            plus-is-0
            difference-not-lessp)))

(prove-lemma quotient-is-unique (rewrite)
  (implies (lessp c a)
           (and (equal (quotient (plus c (times b a)) a) (fix b))
                (equal (quotient (plus c (times a b)) a) (fix b))
                (equal (quotient (plus (times b a) c) a) (fix b))
                (equal (quotient (plus (times a b) c) a) (fix b))))
  ((induct (times b a))))

;;; canonical

;;; Even though this lemma is true unconditionally, we include the
;;; hypotheses to (in most cases) prevent looping.  This will not work
;;; in the presence of inconsistent hypotheses.

(prove-lemma quotient-times-arg1 (rewrite)
  (and
   (implies (and (numberp c)
                 (not (equal c 0))
                 (not (lessp b c)))
            (equal (quotient (times a b) c)
                   (plus (quotient (times a (remainder b c)) c)
                         (times a (quotient b c)))))
   (implies (and (numberp c)
                 (not (equal c 0))
                 (not (lessp b c)))
            (equal (quotient (times b a) c)
                   (plus (quotient (times a (remainder b c)) c)
                         (times a (quotient b c))))))
  ((induct (times a b))
   (disable dichotomy
            difference-times-arg1-simplest
            difference-times-arg1-simpler
            sub1-times
            difference-times-arg1
            difference-lessp
            lessp-times-single-linear
            difference-plus-arg2
            lessp-odometer-simple
            difference-times-arg2
            lessp-transpose-meta
            no-divisors-of-zero
            equal-odometer-simple
            equal-transpose-meta
            lessp-times-cancel-meta
            equal-times-cancel-meta
            lessp-times-linear
            lessp-times-both-linear
            equal-add1
            remainder-plus-arg1
            sub1-difference
            sub1-plus
            difference-times-arg1-meta
            difference-not-lessp
            sub1-remainder
            remainder-lessp-linear)))

(prove-lemma remainder-times-remainder-arg1 (rewrite)
  (and (equal (remainder (times a (remainder b c)) c)
              (remainder (times a b) c))
       (equal (remainder (times (remainder b c) a) c)
              (remainder (times a b) c)))
  ((induct (times a b)) ; for speed
   (disable difference-lessp
            dichotomy
            difference-times-arg1
            difference-difference-arg1-commutes-meta
            difference-times-arg1-simpler
            sub1-times
            no-divisors-of-zero
            equal-transpose-meta
            sub1-plus
            difference-times-arg1-simplest
            plus-is-0
            difference-not-lessp
            difference-times-arg1-meta)))

;;; canonical

(prove-lemma remainder-times-arg1 (rewrite)
  (implies (and (equal rhs (times (remainder b a) (remainder c a)))
                (or (not (numberp a))
                    (equal a 0)
                    (lessp rhs a)))
           (equal (remainder (times b c) a) rhs))
  ((use (remainder-times-remainder-arg1 (a (remainder b a))
                                        (b c)
                                        (c a))
        (remainder-times-remainder-arg1 (a c)
                                        (b b)
                                        (c a)))
   (disable remainder-times-remainder-arg1
            difference-times-arg1
            dichotomy
            difference-times-arg1-simpler
            sub1-times
            no-divisors-of-zero
            difference-times-arg1-meta
            lessp-quotient-arg1-linear
            remainder-lessp-linear
            difference-not-lessp
            difference-lessp)))

(prove-lemma remainder-times-arg1-simple (rewrite)
  (and (equal (remainder (times a b) b) 0)
       (equal (remainder (times b a) b) 0)))

(prove-lemma lessp-quotient-arg2-linear-helper nil
  (implies (not (zerop a))
           (not (lessp (quotient b a)
                       (quotient b (add1 a)))))
  ((use (quotient-remainder-rewrite (a b) (b (add1 a))))
   (disable lessp-transpose-meta
            quotient-lessp-linear
            remainder-add1-arg2
            sub1-plus
            equal-transpose-meta
            sub1-difference
            plus-is-0
            sub1-times
            difference-add1
            no-divisors-of-zero
            plus-associates-right
            difference-not-lessp
            remainder-lessp-linear)))

(prove-lemma lessp-quotient-arg2-linear (rewrite)
  (and (implies (and (not (lessp b a))
                     (numberp a)
                     (not (equal a 0)))
                (not (lessp (quotient c a)
                            (quotient c b))))
       (implies (and (lessp a b)
                     (numberp a)
                     (not (equal a 0)))
                (not (lessp (quotient c a)
                            (quotient c b)))))
  ((induct (plus b a))
   (use (lessp-quotient-arg2-linear-helper
         (a (sub1 b))
         (b c)))))

;;; canonical

(prove-lemma sub1-quotient (rewrite)
  (equal (sub1 (quotient a b))
         (quotient (difference a b) b)))

(prove-lemma equal-remainder-difference-arg1 (rewrite)
  (implies (not (equal b c)) ; to prevent most common looping
           (equal (equal (remainder (difference a b) c) 0)
                  (or (lessp a b)
                      (equal (remainder a c)
                             (remainder b c)))))
  ((disable difference-plus-arg2
            dichotomy
            remainder-times-arg1
            lessp-odometer-simple
            sub1-remainder
            lessp-times-single-linear
            times-plus
            times-commutes
            sub1-plus
            difference-is-monotonic
            difference-plus-arg1
            equal-quarter-odometer
            plus-is-0
            difference-times-arg1-simplest
            difference-times-arg1-simpler
            sub1-times
            remainder-lessp-linear
            difference-not-lessp
            equal-odometer-simple
            difference-lessp)))

(prove-lemma remainder-difference-arg1 (rewrite)
  (implies (equal (remainder a c) b)
           (equal (remainder (difference a b) c) 0)))

(prove-lemma remainder-plus-arg1-kb (rewrite)
  (implies (and (equal rac (remainder a c))
                (equal rbc (remainder b c)))
           (equal (remainder (add1 (plus a b)) c)
                  (if (lessp (plus rac rbc) (sub1 c))
                      (add1 (plus rac rbc))
                    (if (or (not (numberp c))
                            (equal c 0))
                        (add1 (plus a b))
                      (difference rac (difference (sub1 c) rbc))))))
  ((use (remainder-plus-arg1-helper-1 (a (add1 a)) (b b) (c c))
        (sub1-remainder (a (add1 a)) (b c)))
   (expand (remainder (add1 a) (add1 x)))
   (disable remainder-plus-arg1
            sub1-remainder
            quotient-remainder
            remainder-add1-arg2
            difference-remainder-arg1
            difference-remainder-arg2
            difference-plus-arg1
            dichotomy
            sub1-plus
            plus-is-0
            difference-plus-arg2
            equal-odometer-simple
            lessp-odometer-simple
            remainder-lessp-linear
            difference-not-lessp
            difference-lessp)))

(prove-lemma remainder-times-minus-one (rewrite)
  (and (equal (remainder (times a b) (add1 b))
              (if (or (not (numberp a))
                      (equal a 0))
                  0
                (difference b (remainder (sub1 a) (add1 b)))))
       (equal (remainder (times b a) (add1 b))
              (if (or (not (numberp a))
                      (equal a 0))
                  0
                (difference b (remainder (sub1 a) (add1 b))))))
  ((use (remainder-add1-arg2-simple (a a) (b b)))
   (enable remainder-lessp-linear)
   (disable remainder-add1-arg2-simple
            remainder-add1-arg2
            remainder
            remainder-times-arg1
            times
            difference-remainder-arg2
            sub1-remainder
            remainder-plus-arg1
            difference-lessp
            difference-add1
            sub1-times
            sub1-plus
            dichotomy
            remainder-difference-arg1
            lessp-times-single-linear
            times-plus
            equal-plus-cancel-meta
            no-divisors-of-zero
            difference-difference-arg2-commutes-meta
            difference-remainder-arg1)))

(prove-lemma remainder-times-minus-one-normal (rewrite)
  (and (equal (remainder (times a (sub1 b)) b)
              (if (or (not (numberp a))
                      (equal a 0))
                  0
                (difference (sub1 b) (remainder (sub1 a) b))))
       (equal (remainder (times (sub1 b) a) b)
              (if (or (not (numberp a))
                      (equal a 0))
                  0
                (difference (sub1 b) (remainder (sub1 a) b)))))
  ((use (remainder-times-minus-one (a a) (b (sub1 b))))
   (disable remainder-times-minus-one
            times
            remainder-times-arg1
            remainder-lessp-linear
            difference-not-lessp
            difference-times-arg1-meta)))

;;; Lengthy self-proof (requires remainder-if and plus-if)

(prove-lemma remainder-times-minus-one-kb (rewrite)
  (and (equal (remainder (plus b (times b (sub1 a))) (add1 b))
              (difference b (remainder (sub1 a) (add1 b))))
       (equal (remainder (plus b (times (sub1 a) b)) (add1 b))
              (difference b (remainder (sub1 a) (add1 b))))
       (equal (remainder (plus a (times a (sub1 b))) (add1 b))
              (if (or (not (numberp a))
                      (equal a 0))
                  0
                (difference b (remainder (sub1 a) (add1 b)))))
       (equal (remainder (plus a (times (sub1 b) a)) (add1 b))
              (if (or (not (numberp a))
                      (equal a 0))
                  0
                (difference b (remainder (sub1 a) (add1 b)))))
; the next 5 are included because they were observed during the  self-proof
       (equal (remainder (plus a (sub1 b) (times (sub1 a) (sub1 b)))
                         (add1 b))
              (if (or (not (numberp a))
                      (equal a 0))
                  (sub1 b)
                (difference b (remainder (sub1 a) (add1 b)))))
       (equal (remainder (plus (sub1 b) a (times (sub1 a) (sub1 b)))
                         (add1 b))
              (if (or (not (numberp a))
                      (equal a 0))
                  (sub1 b)
                (difference b (remainder (sub1 a) (add1 b)))))
       (equal (remainder (plus a (sub1 b) (times (sub1 b) (sub1 a)))
                         (add1 b))
              (if (or (not (numberp a))
                      (equal a 0))
                  (sub1 b)
                (difference b (remainder (sub1 a) (add1 b)))))
       (equal (remainder (plus (sub1 b) a (times (sub1 b) (sub1 a)))
                         (add1 b))
              (if (or (not (numberp a))
                      (equal a 0))
                  (sub1 b)
                (difference b (remainder (sub1 a) (add1 b)))))

       (equal (remainder (plus b (sub1 a) (times (sub1 a) (sub1 b)))
                         (add1 b))
              (if (or (not (numberp a))
                      (equal a 0))
                  (if (numberp b) b 0)
                (difference b (remainder (sub1 a) (add1 b)))))
       (equal (remainder (plus (sub1 a) b (times (sub1 a) (sub1 b)))
                         (add1 b))
              (if (or (not (numberp a))
                      (equal a 0))
                  (if (numberp b) b 0)
                (difference b (remainder (sub1 a) (add1 b)))))
       (equal (remainder (plus b (sub1 a) (times (sub1 b) (sub1 a)))
                         (add1 b))
              (if (or (not (numberp a))
                      (equal a 0))
                  (if (numberp b) b 0)
                (difference b (remainder (sub1 a) (add1 b)))))
       (equal (remainder (plus (sub1 a) b (times (sub1 b) (sub1 a)))
                         (add1 b))
              (if (or (not (numberp a))
                      (equal a 0))
                  (if (numberp b) b 0)
                (difference b (remainder (sub1 a) (add1 b)))))

       (equal (remainder (add1 (plus   (sub1 a)
                                       (sub1 b)
                                       (times (sub1 a) (sub1 b))))
                         (add1 b))
              (if (or (not (numberp a))
                      (equal a 0))
                  (if (numberp b) b 0)
                (difference b (remainder (sub1 a) (add1 b)))))
       (equal (remainder (add1 (plus (sub1 b)
                                     (sub1 a)
                                     (times (sub1 a) (sub1 b))))
                         (add1 b))
              (if (or (not (numberp a))
                      (equal a 0))
                  (if (numberp b) b 0)
                (difference b (remainder (sub1 a) (add1 b)))))
       (equal (remainder (add1 (plus   (sub1 a)
                                       (sub1 b)
                                       (times (sub1 b) (sub1 a))))
                         (add1 b))
              (if (or (not (numberp a))
                      (equal a 0))
                  (if (numberp b) b 0)
                (difference b (remainder (sub1 a) (add1 b)))))

       (equal (remainder (add1 (plus   (sub1 b)
                                       (sub1 a)
                                       (times (sub1 b) (sub1 a))))
                         (add1 b))
              (if (or (not (numberp a))
                      (equal a 0))
                  (if (numberp b) b 0)
                (difference b (remainder (sub1 a) (add1 b))))))
  ((use (remainder-times-minus-one (a a) (b b)))
   (disable remainder-times-minus-one ; remember to disable just
            remainder-add1-arg2       ; about everything when
            difference-lessp          ; proving kb rules
            lessp-transpose-meta
            equal-transpose-meta
            remainder-plus-arg1
            dichotomy
            difference-remainder-arg2
            remainder-plus-arg1-kb
            difference-remainder-arg1
            difference-plus-arg1
            difference-times-arg1
            lessp-times-single-linear
            sub1-remainder
            difference-add1
            remainder-difference-arg1
            sub1-plus
            equal-add1
            plus-is-0
            difference-not-lessp
            remainder-lessp-linear
            remainder-times-arg1)))

(prove-lemma remainder-times-minus-one-normal-kb (rewrite)
  (and (equal (remainder (plus (sub1 b)
                               (times (sub1 b) (sub1 a)))
                         b)
              (difference (sub1 b) (remainder (sub1 a) b)))
       (equal (remainder (plus (sub1 b)
                               (times (sub1 a) (sub1 b)))
                         b)
              (difference (sub1 b) (remainder (sub1 a) b)))
       (equal (remainder (plus a (times a (sub1 (sub1 b))))
                         b)
              (if (or (not (numberp b))
                      (equal b 0))
                  (if (numberp a) a 0)
                (if (or (equal (sub1 b) 0)
                        (not (numberp a))
                        (equal a 0))
                    0
                  (difference (sub1 b) (remainder (sub1 a) b)))))
       (equal (remainder (plus a (times (sub1 (sub1 b)) a))
                         b)
              (if (or (not (numberp b))
                      (equal b 0))
                  (if (numberp a) a 0)
                (if (or (equal (sub1 b) 0)
                        (not (numberp a))
                        (equal a 0))
                    0
                  (difference (sub1 b) (remainder (sub1 a) b)))))

       (equal (remainder (plus (sub1 b)
                               (sub1 b)
                               (times (sub1 b) (sub1 (sub1 a))))
                         b)
              (if (equal (sub1 a) 0)
                  (sub1 (sub1 b))
                (difference (sub1 b) (remainder (sub1 a) b))))
       (equal (remainder (plus (sub1 b)
                               (sub1 b)
                               (times (sub1 (sub1 a)) (sub1 b)))
                         b)
              (if (equal (sub1 a) 0)
                  (sub1 (sub1 b))
                (difference (sub1 b) (remainder (sub1 a) b)))))
  ((use (remainder-times-minus-one-normal (a a) (b b)))
   (expand (times a (sub1 b))
           (times (sub1 a) (sub1 (sub1 b)))
           (times (sub1 a) (sub1 b))
           (times (sub1 b) (sub1 (sub1 a))))
   (disable remainder-times-minus-one-normal
            remainder-plus-arg1
            equal-transpose-meta
            lessp-transpose-meta
            dichotomy
            sub1-remainder
            sub1-quotient
            difference-lessp
            lessp-times-single-linear
            quotient-add1-arg2
            difference-remainder-arg1
            difference-remainder-arg2
            quotient-remainder
            remainder-plus-arg1-kb
            difference-times-arg1-simpler
            difference-times-arg1-simplest
            difference-times-arg1
            remainder-difference-arg1
            remainder-times-arg1
            sub1-plus
            difference-0
            sub1-times
            plus-is-0
            sub1-difference
            lessp-times-both-linear
            no-divisors-of-zero
            lessp-times-linear
            lessp-times-cancel-meta
            difference-times-arg2
            difference-plus-arg2
            lessp-quarter-odometer-left
            remainder-lessp-linear
            quotient-difference-arg1)))

;;; canonical

(prove-lemma remainder-add1-arg1 (rewrite)
  (equal (remainder (add1 a) b)
         (if (or (lessp a (sub1 b))
                 (not (numberp b))
                 (equal b 0))
             (add1 a)
           (remainder (difference a (sub1 b)) b))))

(prove-lemma remainder-plus-modulus-kb (rewrite)
  (and
   (equal (remainder (add1 (add1 (plus (sub1 b) c))) (add1 b))
          (remainder c (add1 b)))
   (equal (remainder (add1 (add1 (plus c (sub1 b)))) (add1 b))
          (remainder c (add1 b))))
  ((disable remainder-add1-arg1
            remainder-add1-arg2
            remainder-lessp-linear)))

(prove-lemma remainder-plus-arg1-simple (rewrite)
  (implies (and (not (lessp (plus a b) c))
                (not (lessp c a)))
           (and
            (equal (remainder (plus a b) c)
                   (remainder (difference b (difference c a)) c))
            (equal (remainder (plus b a) c)
                   (remainder (difference b (difference c a)) c))))
  ((expand (remainder (plus a b) c))
   (disable remainder-plus-arg1
            lessp-transpose-meta
            difference-lessp
            dichotomy
            remainder-lessp-linear
            remainder-difference-arg1
            difference-not-lessp)))

;;; canonical (preferred)

(prove-lemma modulus-sub1-cancellation (rewrite)
  (and (equal (equal (remainder (times a b) (add1 b)) 0)
              (equal (remainder a (add1 b)) 0))
       (equal (equal (remainder (times b a) (add1 b)) 0)
              (equal (remainder a (add1 b)) 0)))
  ((disable
    difference-difference-arg1-commutes-meta
    lessp-quotient-arg2-linear
    sub1-remainder
    quotient-lessp-linear
    sub1-quotient
    remainder-plus-arg1-simple
    lessp-transpose-meta
    equal-transpose-meta
    quotient
    dichotomy
    difference-lessp
    remainder-add1-arg2
    difference-times-arg1-simplest
    lessp-times-single-linear
    difference-times-arg1
    difference-remainder-arg2
    lessp-times-both-linear
    sub1-times
    times-plus
    lessp-times-linear
    remainder-lessp-linear
    difference-not-lessp)))

(prove-lemma quotient-times-arg1-kb (rewrite)
  (and
   (implies
    (and (numberp c)
         (not (equal c 0))
         (not (lessp b c)))
    (equal (quotient (plus b (times a b)) c)
           (if (lessp (plus (remainder b c)
                            (remainder (times a b) c))
                      c)
               (plus (quotient b c)
                     (quotient (times a (remainder b c)) c)
                     (times a (quotient b c)))
             (add1 (plus (quotient b c)
                         (quotient (times a (remainder b c)) c)
                         (times a (quotient b c)))))))
   (implies
    (and (numberp c)
         (not (equal c 0))
         (not (lessp b c)))
    (equal (quotient (plus b (times b a)) c)
           (if (lessp (plus (remainder b c)
                            (remainder (times a b) c))
                      c)
               (plus (quotient b c)
                     (quotient (times a (remainder b c)) c)
                     (times a (quotient b c)))
             (add1 (plus (quotient b c)
                         (quotient (times a (remainder b c)) c)
                         (times a (quotient b c))))))))
  ((use (quotient-times-arg1 (a (add1 a)) (b b) (c c))
        (quotient-remainder-rewrite (a b) (b c))
        (quotient-remainder-rewrite (a (times a b)) (b c)))
   (disable ; must not disable  quotient-times-arg1
    remainder-times-arg1
    quotient-remainder-rewrite
    quotient-remainder
    lessp
    times
    plus
    difference-times-arg1-simplest
    lessp-quotient-arg2-linear
    quotient-lessp-linear
    quotient
    lessp-times-single-linear
    dichotomy
    lessp-odometer-simple
    difference-times-arg1
    difference-times-arg1-simpler
    remainder-difference-arg1
    difference-lessp
    equal-times-cancel-meta
    equal-half-odometer
    sub1-times
    lessp-times-linear
    remainder-lessp-linear
    difference-not-lessp
    difference-times-arg1-meta)))

(prove-lemma quotient-times-minus-one-helper (rewrite)
  (implies (not (lessp b (sub1 a)))
           (and (equal (quotient (times a b) (add1 b))
                       (sub1 a))
                (equal (quotient (times b a) (add1 b))
                       (sub1 a))))
  ((use (quotient-is-unique (a (add1 b))
                            (b (sub1 a))
                            (c (difference b (sub1 a)))))
   (disable quotient-is-unique
            quotient-plus-arg1
            quotient-add1-arg2
            difference-plus-arg1
            lessp-times-single-linear
            remainder-difference-arg1
            difference-times-arg2-preferred
            remainder-add1-arg1
            difference-lessp)))

;;; This lemma is needed because quotient-times-arg1 was weakened to prevent
;;; looping.

(prove-lemma quotient-times-arg1-simple (rewrite)
  (implies (equal (remainder a c) 0)
           (and (equal (quotient (times a b) c)
                       (times b (quotient a c)))
                (equal (quotient (times b a) c)
                       (times b (quotient a c)))))
  ((disable lessp-transpose-meta
            equal-transpose-meta
            dichotomy
            sub1-times
            sub1-difference
            difference-0
            difference-lessp
            sub1-quotient
            difference-times-arg1
            no-divisors-of-zero
            difference-times-arg1-simpler
            lessp-quotient-arg1-linear
            difference-times-arg1-simplest
            sub1-plus
            lessp-times-cancel-meta
            plus-is-0
            difference-times-arg1-meta
            difference-not-lessp
            remainder-lessp-linear
            difference-times-arg1-kb
            sub1-remainder)))

;;; times-1 is needed to expand (times 2 a) in those cases where (add1 0)
;;; is not present within the term structure of the formula being proven.
;;; It also prevents bind-stack overflows due to equal-times-cancel-meta.

(prove-lemma times-1 (rewrite)
  (and (equal (times 1 a) (if (numberp a) a 0))
       (equal (times a 1) (if (numberp a) a 0))))

;;; canonical (preferred)

(prove-lemma quotient-times-minus-one (rewrite)
  (and (equal (quotient (times a b) (add1 b))
              (if (equal (remainder a (add1 b)) 0)
                  (times b (quotient a (add1 b)))
                (plus (remainder (sub1 a) (add1 b))
                      (times b (quotient a (add1 b))))))
       (equal (quotient (times b a) (add1 b))
              (if (equal (remainder a (add1 b)) 0)
                  (times b (quotient a (add1 b)))
                (plus (remainder (sub1 a) (add1 b))
                      (times b (quotient a (add1 b)))))))
  ((use (quotient-remainder-rewrite (a a) (b (add1 b))))
   (expand (times x (sub1 b))
           (times b (sub1 x)))
   (disable quotient-remainder-rewrite
            quotient-add1-arg2
            remainder-add1-arg2
            times
            times-add1
            equal-add1
            sub1-quotient
            lessp-transpose-meta
            remainder-plus-arg1-simple
            quotient-lessp-linear
            lessp-times-single-linear
            difference-times-arg1
            difference-times-arg1-simpler
            remainder-lessp-linear
            difference-not-lessp)))

(disable quotient-times-minus-one-helper)

;;; This lemma is included for cases in which sub1-elim has not produced
;;; a term suitable for quotient-times-minus-one.

(prove-lemma quotient-times-minus-one-normal (rewrite)
  (and (equal (quotient (times a (sub1 b)) b)
              (if (equal (remainder a b) 0)
                  (times (sub1 b) (quotient a b))
                (if (or (not (numberp b))
                        (equal b 0))
                    0
                  (plus (remainder (sub1 a) b)
                        (times (sub1 b) (quotient a b))))))
       (equal (quotient (times (sub1 b) a) b)
              (if (equal (remainder a b) 0)
                  (times (sub1 b) (quotient a b))
                (if (or (not (numberp b))
                        (equal b 0))
                    0
                  (plus (remainder (sub1 a) b)
                        (times (sub1 b) (quotient a b)))))))
  ((use (quotient-times-minus-one (a a) (b (sub1 b))))
   (disable quotient-times-minus-one
            quotient-plus-arg1
            sub1-quotient
            difference-lessp
            difference-plus-arg1
            difference-times-arg1
            difference-not-lessp)))

;;; Needed to speed up quotient-times-minus-one-kb

(prove-lemma quotient-1-2 (rewrite)
  (and (equal (quotient a 1) (if (numberp a) a 0))
       (equal (quotient (add1 (add1 a)) 2)
              (add1 (quotient a 2)))
       (equal (quotient (plus a a) 2) (if (numberp a) a 0))
       (equal (quotient (plus a (plus a b)) 2)
              (plus a (quotient b 2))))
  ((induct (plus a b)) ; for speed
   (disable quotient-plus-arg1
            quotient-add1-arg1
            dichotomy
            lessp-transpose-meta
            difference-lessp
            remainder-plus-arg1
            difference-plus-arg1
            difference-add1
            equal-transpose-meta
            difference-0
            sub1-quotient
            plus-commutes-meta
            difference-difference-arg1-commutes-meta
            sub1-difference
            sub1-plus
            quotient-difference-arg1
            equal-odometer-simple
            remainder-add1-arg2
            remainder-plus-arg1-simple
            plus-associates-right
            modulus-sub1-cancellation
            difference-not-lessp)))

;;; Needs plus-if in order to prevent quotient-plus-arg1 from firing first.

(prove-lemma quotient-times-minus-one-kb (rewrite)
  (and (equal (quotient (plus b (times b (sub1 a))) (add1 b))
              (if (equal (remainder a (add1 b)) 0)
                  (times b (quotient a (add1 b)))
                (plus (remainder (sub1 a) (add1 b))
                      (times b (quotient a (add1 b))))))
       (equal (quotient (plus b (times (sub1 a) b)) (add1 b))
              (if (equal (remainder a (add1 b)) 0)
                  (times b (quotient a (add1 b)))
                (plus (remainder (sub1 a) (add1 b))
                      (times b (quotient a (add1 b))))))
       (equal (quotient (plus a (times a (sub1 b))) (add1 b))
              (if (or (not (numberp b))
                      (equal b 0))
                  (if (numberp a) a 0)
                (if (equal (remainder a (add1 b)) 0)
                    (times b (quotient a (add1 b)))
                  (plus (remainder (sub1 a) (add1 b))
                        (times b (quotient a (add1 b)))))))
       (equal (quotient (plus a (times (sub1 b) a)) (add1 b))
              (if (or (not (numberp b))
                      (equal b 0))
                  (if (numberp a) a 0)
                (if (equal (remainder a (add1 b)) 0)
                    (times b (quotient a (add1 b)))
                  (plus (remainder (sub1 a) (add1 b))
                        (times b (quotient a (add1 b)))))))
       (equal (quotient (plus a (sub1 b) (times (sub1 a) (sub1 b)))
                        (add1 b))
              (if (or (not (numberp b))
                      (equal b 0))
                  (if (numberp a) a 0)
                (if (equal (remainder a (add1 b)) 0)
                    (times b (quotient a (add1 b)))
                  (plus (remainder (sub1 a) (add1 b))
                        (times b (quotient a (add1 b)))))))
       (equal (quotient (plus a (sub1 b) (times (sub1 b) (sub1 a)))
                        (add1 b))
              (if (or (not (numberp b))
                      (equal b 0))
                  (if (numberp a) a 0)
                (if (equal (remainder a (add1 b)) 0)
                    (times b (quotient a (add1 b)))
                  (plus (remainder (sub1 a) (add1 b))
                        (times b (quotient a (add1 b)))))))
       (equal (quotient (plus (sub1 b) a (times (sub1 a) (sub1 b)))
                        (add1 b))
              (if (or (not (numberp b))
                      (equal b 0))
                  (if (numberp a) a 0)
                (if (equal (remainder a (add1 b)) 0)
                    (times b (quotient a (add1 b)))
                  (plus (remainder (sub1 a) (add1 b))
                        (times b (quotient a (add1 b)))))))
       (equal (quotient (plus (sub1 b) a (times (sub1 b) (sub1 a)))
                        (add1 b))
              (if (or (not (numberp b))
                      (equal b 0))
                  (if (numberp a) a 0)
                (if (equal (remainder a (add1 b)) 0)
                    (times b (quotient a (add1 b)))
                  (plus (remainder (sub1 a) (add1 b))
                        (times b (quotient a (add1 b)))))))

       (equal (quotient (plus b (sub1 a) (times (sub1 b) (sub1 a)))
                        (add1 b))
              (if (or (not (numberp b))
                      (equal b 0))
                  (sub1 a)
                (if (equal (remainder a (add1 b)) 0)
                    (times b (quotient a (add1 b)))
                  (plus (remainder (sub1 a) (add1 b))
                        (times b (quotient a (add1 b)))))))
       (equal (quotient (plus b (sub1 a) (times (sub1 a) (sub1 b)))
                        (add1 b))
              (if (or (not (numberp b))
                      (equal b 0))
                  (sub1 a)
                (if (equal (remainder a (add1 b)) 0)
                    (times b (quotient a (add1 b)))
                  (plus (remainder (sub1 a) (add1 b))
                        (times b (quotient a (add1 b)))))))
       (equal (quotient (plus (sub1 a) b (times (sub1 b) (sub1 a)))
                        (add1 b))
              (if (or (not (numberp b))
                      (equal b 0))
                  (sub1 a)
                (if (equal (remainder a (add1 b)) 0)
                    (times b (quotient a (add1 b)))
                  (plus (remainder (sub1 a) (add1 b))
                        (times b (quotient a (add1 b)))))))
       (equal (quotient (plus (sub1 a) b (times (sub1 a) (sub1 b)))
                        (add1 b))
              (if (or (not (numberp b))
                      (equal b 0))
                  (sub1 a)
                (if (equal (remainder a (add1 b)) 0)
                    (times b (quotient a (add1 b)))
                  (plus (remainder (sub1 a) (add1 b))
                        (times b (quotient a (add1 b)))))))

       (equal (quotient (add1 (plus (sub1 a)
                                    (sub1 b)
                                    (times (sub1 a) (sub1 b))))
                        (add1 b))
              (if (or (not (numberp b))
                      (equal b 0))
                  (if (or (not (numberp a))
                          (equal a 0))
                      1
                    a)
                (if (equal (remainder a (add1 b)) 0)
                    (times b (quotient a (add1 b)))
                  (plus (remainder (sub1 a) (add1 b))
                        (times b (quotient a (add1 b)))))))
       (equal (quotient (add1 (plus (sub1 b)
                                    (sub1 a)
                                    (times (sub1 b) (sub1 a))))
                        (add1 b))
              (if (or (not (numberp b))
                      (equal b 0))
                  (if (or (not (numberp a))
                          (equal a 0))
                      1
                    a)
                (if (equal (remainder a (add1 b)) 0)
                    (times b (quotient a (add1 b)))
                  (plus (remainder (sub1 a) (add1 b))
                        (times b (quotient a (add1 b)))))))
       (equal (quotient (add1 (plus (sub1 b)
                                    (sub1 a)
                                    (times (sub1 a) (sub1 b))))
                        (add1 b))
              (if (or (not (numberp b))
                      (equal b 0))
                  (if (or (not (numberp a))
                          (equal a 0))
                      1
                    a)
                (if (equal (remainder a (add1 b)) 0)
                    (times b (quotient a (add1 b)))
                  (plus (remainder (sub1 a) (add1 b))
                        (times b (quotient a (add1 b)))))))
       (equal (quotient (add1 (plus (sub1 a)
                                    (sub1 b)
                                    (times (sub1 b) (sub1 a))))
                        (add1 b))
              (if (or (not (numberp b))
                      (equal b 0))
                  (if (or (not (numberp a))
                          (equal a 0))
                      1
                    a)
                (if (equal (remainder a (add1 b)) 0)
                    (times b (quotient a (add1 b)))
                  (plus (remainder (sub1 a) (add1 b))
                        (times b (quotient a (add1 b))))))))
  ((use (quotient-times-minus-one (a a) (b b))
        (times-add1 (a a) (b (sub1 b))))
   (disable quotient-times-minus-one
            times-add1
            lessp-transpose-meta
            equal-transpose-meta
            quotient-add1-arg1
            quotient-add1-arg2
            difference-0
            difference-lessp
            dichotomy
            lessp-times-single-linear
            remainder-add1-arg2
            difference-plus-arg1
            difference-add1
            difference-times-arg1
            sub1-quotient
            lessp-times-both-linear
            sub1-difference
            sub1-times
            quotient-difference-arg1
            difference-times-arg1-simpler
            lessp-times-linear
            sub1-remainder
            plus-associates-right
            plus-commutes
            equal-odometer-simple
            no-divisors-of-zero
            difference-times-arg1-simplest
            sub1-plus
            plus-is-0
            difference-not-lessp
            remainder-difference-arg1
            remainder-lessp-linear)))

(prove-lemma quotient-times-minus-one-normal-kb (rewrite)
  (and
   (equal (quotient (plus (sub1 b) (times (sub1 b) (sub1 a))) b)
          (if (equal (sub1 b) 0)
              0
            (if (equal (remainder a b) 0)
                (times (sub1 b) (quotient a b))
              (plus (remainder (sub1 a) b)
                    (times (sub1 b) (quotient a b))))))
   (equal (quotient (plus (sub1 b) (times (sub1 a) (sub1 b))) b)
          (if (equal (sub1 b) 0)
              0
            (if (equal (remainder a b) 0)
                (times (sub1 b) (quotient a b))
              (plus (remainder (sub1 a) b)
                    (times (sub1 b) (quotient a b))))))
   (equal (quotient (plus a (times a (sub1 (sub1 b)))) b)
          (if (equal (sub1 b) 0)
              (quotient a b)
            (if (equal (remainder a b) 0)
                (times (sub1 b) (quotient a b))
              (plus (remainder (sub1 a) b)
                    (times (sub1 b) (quotient a b))))))
   (equal (quotient (plus a (times (sub1 (sub1 b)) a)) b)
          (if (equal (sub1 b) 0)
              (quotient a b)
            (if (equal (remainder a b) 0)
                (times (sub1 b) (quotient a b))
              (plus (remainder (sub1 a) b)
                    (times (sub1 b) (quotient a b))))))
   (equal (quotient (plus (sub1 b)
                          (sub1 b)
                          (times (sub1 (sub1 a)) (sub1 b)))
                    b)
          (if (equal (sub1 b) 0)
              0
            (if (equal (sub1 a) 0)
                1
              (if (equal (remainder a b) 0)
                  (times (sub1 b) (quotient a b))
                (plus (remainder (sub1 a) b)
                      (times (sub1 b) (quotient a b)))))))
   (equal (quotient (plus (sub1 b)
                          (sub1 b)
                          (times (sub1 b) (sub1 (sub1 a))))
                    b)
          (if (equal (sub1 b) 0)
              0
            (if (equal (sub1 a) 0)
                1
              (if (equal (remainder a b) 0)
                  (times (sub1 b) (quotient a b))
                (plus (remainder (sub1 a) b)
                      (times (sub1 b) (quotient a b))))))))
  ((use (quotient-times-minus-one-normal (a a) (b b)))
   (expand (times a (sub1 b))
           (times a (sub1 (sub1 b)))
           (times (sub1 a) (sub1 b))
           (times (sub1 b) (sub1 (sub1 a)))
           (times (sub1 a) (sub1 (sub1 b)))
           (quotient (plus x x) (add1 x))
           (quotient (add1 (add1 (plus v z z (times v z))))
                     (add1 (add1 z))))
   (disable quotient-times-minus-one-normal
            remainder
            quotient-remainder
            lessp-plus-cancel-meta
            lessp-transpose-meta
            equal-transpose-meta
            lessp-times-single-linear
            quotient-add1-arg2
            quotient-add1-arg1
            quotient-plus-arg1
            dichotomy
            remainder-plus-arg1-simple
            equal-odometer-simple
            remainder-plus-arg1
            quotient-difference-arg1
            remainder-add1-arg2
            difference-lessp
            times-plus
            sub1-quotient
            difference-0
            lessp-quotient-arg2-linear
            sub1-difference
            difference-times-arg1
            difference-times-arg1-simpler
            lessp-quotient-arg1-linear
            difference-not-lessp)))

;;; canonical

(prove-lemma quotient-plus-arg2 (rewrite)
  (and (implies (and (numberp a)
                     (not (equal a 0))
                     (not (lessp (remainder c a)
                                 (times b (quotient c a)))))
                (equal (quotient c (plus a b))
                       (quotient c a)))
       (implies (and (numberp a)
                     (not (equal a 0))
                     (not (lessp (remainder c a)
                                 (times b (quotient c a)))))
                (equal (quotient c (plus b a))
                       (quotient c a)))
       (implies (and (numberp a)
                     (not (equal a 0))
                     (lessp (remainder c a)
                            (times b (quotient c a)))
                     (not (lessp
                           (plus a (remainder c a))
                           (times b (quotient (difference c a) a)))))
                (equal (quotient c (plus a b))
                       (quotient (difference c a) a)))
       (implies (and (numberp a)
                     (not (equal a 0))
                     (lessp (remainder c a)
                            (times b (quotient c a)))
                     (not (lessp
                           (plus a (remainder c a))
                           (times b (quotient (difference c a) a)))))
                (equal (quotient c (plus b a))
                       (quotient (difference c a) a))))
  ((use (quotient-is-unique (a (plus a b))
                            (b (quotient c a))
                            (c (difference
                                (remainder c a)
                                (times b (quotient c a)))))
        (quotient-is-unique
         (a (plus a b))
         (b (quotient (difference c a) a))
         (c (difference
             (plus a (remainder c a))
             (times b (quotient (difference c a) a))))))
   (disable quotient-is-unique
            lessp-transpose-meta
            difference-lessp
            equal-transpose-meta
            quotient-plus-arg1
            dichotomy
            difference-plus-arg1
            lessp-quotient-arg2-linear
            remainder-difference-arg1
            sub1-quotient
            difference-0
            difference-times-arg2-preferred
            difference-times-arg2
            equal-odometer-simple
            lessp-odometer-simple
            lessp-half-odometer-left
            lessp-quotient-arg1-linear
            lessp-times-single-linear
            lessp-plus-cancel-meta
            sub1-difference
            sub1-plus
            sub1-remainder
            sub1-times
            no-divisors-of-zero
            lessp-times-cancel-meta
            quotient-difference-arg1
            times
            difference-not-lessp
            difference-plus-arg2)))

;;; canonical

;;; We omit permutative cases involving non tame terms.

(prove-lemma quotient-plus-arg2-simple (rewrite)
  (and (equal (quotient (plus (times a c) (times b c)) (plus a b))
              (if (equal (plus a b) 0) 0 (fix c)))
       (equal (quotient (plus (times a c) (times c b)) (plus a b))
              (if (equal (plus a b) 0) 0 (fix c)))
       (equal (quotient (plus (times a c) (times c b)) (plus b a))
              (if (equal (plus a b) 0) 0 (fix c)))

       (equal (quotient (plus (times c a) (times c b)) (plus a b))
              (if (equal (plus a b) 0) 0 (fix c)))
       (equal (quotient (plus (times c a) (times b c)) (plus a b))
              (if (equal (plus a b) 0) 0 (fix c)))
       (equal (quotient (plus (times c a) (times b c)) (plus b a))
              (if (equal (plus a b) 0) 0 (fix c))))
  ((use (quotient-times-arg1-simple (a (plus a b))
                                    (b c)
                                    (c (plus a b))))
   (disable quotient-times-arg1-simple
            quotient-plus-arg1
            quotient-plus-arg2
            difference-plus-arg2
            equal-odometer-simple
            difference-lessp
            dichotomy
            lessp-transpose-meta
            difference-times-arg2-preferred
            remainder-plus-arg1
            difference-remainder-arg1
            equal-transpose-meta
            sub1-remainder
            remainder-difference-arg1
            sub1-plus
            sub1-times
            difference-times-arg2
            difference-times-arg1
            lessp-times-single-linear
            no-divisors-of-zero
            difference-times-arg1-simplest
            lessp-odometer-simple
            difference-times-arg1-meta
            remainder-lessp-linear
            difference-times-arg1-simpler
            sub1-difference
            difference-0
            difference-not-lessp
            lessp-times-cancel-meta)))

;;; I could find no good canonical rule for remainder-plus-arg2

(prove-lemma remainder-plus-arg2 (rewrite)
  (and
   (equal (remainder (plus (times a c) (times b c)) (plus a b)) 0)
   (equal (remainder (plus (times a c) (times c b)) (plus a b)) 0)
   (equal (remainder (plus (times a c) (times c b)) (plus b a)) 0)

   (equal (remainder (plus (times c a) (times c b)) (plus a b)) 0)
   (equal (remainder (plus (times c a) (times b c)) (plus a b)) 0)
   (equal (remainder (plus (times c a) (times b c)) (plus b a)) 0))
  ((use (remainder-times-arg1-simple (a c) (b (plus a b))))
   (disable remainder-times-arg1-simple
            remainder-plus-arg1
            difference-plus-arg2
            difference-plus-arg1
            lessp-transpose-meta
            difference-lessp
            sub1-plus
            sub1-times
            remainder-plus-arg1-simple
            difference-times-arg1-simplest
            difference-times-arg1
            no-divisors-of-zero
            plus-is-0)))

;;; canonical

(prove-lemma quotient-times-arg2 (rewrite)
  (equal (quotient a (times zb zc))
         (quotient (quotient a zb) zc))
  ((expand (quotient z (times zb zc)))
   (disable lessp-transpose-meta
            equal-transpose-meta
            sub1-quotient
            sub1-times
            difference-times-arg2
            remainder-plus-arg1-simple
            lessp-times-both-linear
            lessp-odometer
            lessp-quarter-odometer-right
            lessp-half-odometer-left
            lessp-quarter-odometer-left
            difference-times-arg2-preferred)))

;;; canonical

(prove-lemma remainder-times-arg2 (rewrite)
  (equal (remainder a (times zb zc))
         (plus (remainder a zb)
               (times zb (remainder (quotient a zb) zc))))
  ((use (quotient-remainder (a a) (b (times zb zc)))
        (quotient-remainder (a (quotient a zb)) (b zc)))
   (disable quotient-remainder-rewrite
            sub1-quotient
            difference-times-arg2
            difference-times-arg1
            remainder-times-arg1
            remainder-plus-arg1
            difference-plus-arg1
            sub1-times

            remainder-plus-arg1-simple
            equal-plus-cancel-meta
            equal-odometer-simple
            sub1-remainder
            difference-lessp
            quotient-lessp-linear
            remainder-difference-arg1
            sub1-plus
            plus-is-0
            lessp-times-single-linear
            plus-associates-right
            lessp-times-both-linear
            plus-commutes-nest
            difference-times-arg2-preferred
            lessp-times-linear
            difference-not-lessp
            remainder-lessp-linear)))
;;; canonical

(prove-lemma difference-associates (rewrite)
  (implies (not (lessp c d))
           (equal (difference (difference a (difference b c)) d)
                  (if (lessp b c)
                      (difference a d)
                    (difference
                     a
                     (difference b (difference c d))))))
  ((disable equal-transpose-meta
            lessp-transpose-meta)))

;;; canonical

(prove-lemma quotient-plus-times-minus-one (rewrite)
  (implies (and (not (lessp c a))
                (not (lessp b (difference c a))))
           (and (equal (quotient (plus (times b a) c) (add1 b))
                       (if (numberp a) a 0))
                (equal (quotient (plus (times a b) c) (add1 b))
                       (if (numberp a) a 0))
                (equal (quotient (plus c (times b a)) (add1 b))
                       (if (numberp a) a 0))
                (equal (quotient (plus c (times a b)) (add1 b))
                       (if (numberp a) a 0))))
  ((use (quotient-is-unique (a (add1 b))
                            (b a)
                            (c (difference c a))))
   (disable quotient-is-unique
            difference-plus-arg1
            difference-times-arg2
            no-divisors-of-zero
            sub1-plus
            difference-add1
            plus-zerop
            sub1-times
            difference-lessp
            quotient-plus-arg1
            quotient-add1-arg2
            quotient-remainder
            lessp-times-single-linear
            equal-transpose-meta
            dichotomy
            plus-is-0
            lessp-times-linear
            lessp-half-odometer-right
            sub1-difference
            equal-plus-cancel-meta
            lessp-times-cancel-meta
            equal-add1)))

;;; canonical

(prove-lemma add1-remainder-sub1-arg1 (rewrite)
  (equal (add1 (remainder (sub1 a) b))
         (if (or (not (numberp a))
                 (equal a 0))
             1
           (if (equal (remainder a b) 0)
               b
             (remainder a b))))
  ((disable quotient-remainder)))

;;; The inversion correcting lemmas are now complete.  We include here some
;;; generally useful simplifications.

(prove-lemma remainder-minus-one-as-0 (rewrite)
  (and (implies (and (equal b (remainder x (add1 b))) ; avoid
                     (equal x (sub1 a)))              ; rewriting
                (equal (remainder a (add1 b)) 0))
       (implies (and (equal (remainder x (add1 b)) b)
                     (equal x (sub1 a)))
                (equal (remainder a (add1 b)) 0)))
  ((disable remainder-add1-arg2
            sub1-quotient)))

(prove-lemma quotient-remainder-rewrite-kb (rewrite)
  (and (equal (plus b
                    (remainder a b)
                    (times b (quotient (difference a b) b)))
              (if (lessp a b)
                  (plus a b)
                (if (numberp a) a 0)))
       (equal (plus (quotient a b)
                    (remainder a b)
                    (times (sub1 b) (quotient a b)))
              (if (numberp a) a 0))
       (equal (plus (sub1 b)
                    (quotient a b)
                    (remainder a b)
                    (times (sub1 b) (quotient (difference a b) b)))
              (if (lessp a b)
                  (plus a (sub1 b))
                (if (numberp a) a 0))))
  ((use (quotient-remainder (a a) (b b)))
   (disable difference-lessp
            sub1-quotient
            lessp-transpose-meta
            lessp-quotient-arg2-linear
            lessp-times-single-linear
            equal-transpose-meta
            dichotomy
            remainder-difference-arg1
            quotient-lessp-linear
            sub1-remainder
            sub1-plus
            quotient-difference-arg1
            plus-is-0
            difference-not-lessp)))

(prove-lemma remainder-sub1-cancellation (rewrite)
  (equal (equal (remainder (sub1 a) c)
                (remainder (sub1 b) c))
         (if (or (not (numberp a))
                 (equal a 0))
             (equal (remainder (sub1 b) c) 0)
           (if (or (not (numberp b))
                   (equal b 0))
               (equal (remainder (sub1 a) c) 0)
             (equal (remainder a c)
                    (remainder b c)))))
  ((use (sub1-remainder (a a) (b c))
        (sub1-remainder (a b) (b c)))
   (disable sub1-remainder
            quotient-remainder
            remainder-add1-arg2
            difference-lessp
            remainder-minus-one-as-0
            lessp-transpose-meta
            difference-difference-arg1-commutes-meta
            equal-transpose-meta
            difference-0
            sub1-difference
            remainder-lessp-linear
            difference-not-lessp)))

;;; Trade quotient for times in lessp.

(prove-lemma lessp-quotient (rewrite)
  (and (equal (lessp b (quotient c a))
              (and (numberp a)
                   (not (equal a 0))
                   (not (lessp c (plus a (times a b))))))
       (equal (lessp (quotient c b) a)
              (or (lessp c (times a b))
                  (and (or (not (numberp b))
                           (equal b 0))
                       (numberp a)
                       (not (equal a 0))))))
  ((disable sub1-quotient
            difference-lessp
            lessp-transpose-meta
            quotient-lessp-linear
            equal-transpose-meta
            sub1-difference
            sub1-plus
            equal-times-cancel-meta
            quotient-times-arg1-simple
            lessp-times-linear
            difference-not-lessp)))

;;; The following two lemmas are required because nqthm does not open
;;;  recursive definitions more than once.

(prove-lemma remainder-of-modulus (rewrite)
  (equal (remainder a a) 0))

(prove-lemma quotient-is-1 (rewrite)
  (equal (quotient a a)
         (if (or (not (numberp a))
                 (equal a 0))
             0
           1)))

(prove-lemma equal-quotient-0 (rewrite)
  (equal (equal (quotient a b) 0)
         (or (not (numberp b))
             (equal b 0)
             (lessp a b))))

(prove-lemma plus-1 (rewrite)
  (and (equal (plus 1 a) (add1 a))
       (equal (plus a 1) (add1 a))))

(prove-lemma sub1-decreases (rewrite)
  (and
   (equal (equal (sub1 a) a)
          (equal a 0))
   (equal (equal (sub1 (sub1 a)) a)
          (equal a 0))))

(prove-lemma lessp-2 (rewrite)
  (equal (lessp a 2)
         (equal (sub1 a) 0)))

(prove-lemma lessp-remainder-by-2 (rewrite)
  (equal (lessp (times (remainder a 2) (remainder b 2)) 2) t)
  ((disable sub1-remainder
            sub1-times)))

(prove-lemma remainder-1-2 (rewrite)
  (and (equal (remainder a 1) 0)
       (equal (remainder (plus a a) 2) 0)
       (equal (remainder (plus a (plus a b)) 2)
              (remainder b 2))
       (equal (remainder (times a (sub1 a)) 2) 0)
       (equal (remainder (times a a) 2)
              (remainder a 2))
       (equal (remainder (times a (times a b)) 2)
              (remainder (times a b) 2)))
  ((expand (remainder x 2)
           (lessp x 2)
           (remainder b 2)
           (times b (times x x)))
   (disable remainder
            times
            plus
            lessp
            remainder-add1-arg2
            lessp-transpose-meta
            sub1-difference
            remainder-difference-arg1
            difference-lessp
            sub1-decreases
            equal-transpose-meta
            remainder-plus-arg1-simple
            difference-remainder-arg2
            sub1-times
            dichotomy
            lessp-facts
            times-zerop)))

(prove-lemma equal-difference-difference-cancellation (rewrite)
  (equal (equal a (difference b (difference c a)))
         (if (lessp c a)
             (equal a (if (numberp b) b 0))
           (if (lessp (plus a b) c)
               (equal a 0)
             (and (numberp a)
                  (equal (if (numberp b) b 0)
                         (if (numberp c) c 0)))))))

;;; Since the proof is not immediate, we include this Knuth-Bendix version
;;; of lessp-times.  In most cases, we expect times expansion, sub1 elimination
;;; and lessp-plus-cancel-meta to render this unnecessary.

(prove-lemma lessp-times-kb (rewrite)
  (and (equal (lessp (plus b (times b (sub1 a))) a)
              (and (not (zerop a))
                   (zerop b)))
       (equal (lessp (plus b (times (sub1 a) b)) a)
              (and (not (zerop a))
                   (zerop b)))
       (equal (lessp a (plus b (times b (sub1 a))))
              (or (and (zerop a)
                       (not (zerop b)))
                  (and (not (zerop a))
                       (not (zerop b))
                       (not (equal (sub1 b) 0)))))
       (equal (lessp a (plus b (times (sub1 a) b)))
              (or (and (zerop a)
                       (not (zerop b)))
                  (and (not (zerop a))
                       (not (zerop b))
                       (not (equal (sub1 b) 0)))))))

;;; This lemma is provided for situations where (times b c) is not naturally
;;; expanded.

(prove-lemma equal-plus-times-cancellation (rewrite)
  (let ((rhs (and (numberp c)
                  (or (and (numberp b)
                           (not (equal b 0))
                           (or (not (numberp a))
                               (equal a 0))
                           (or (equal c 0)
                               (equal (sub1 b) 0)))
                      (and (or (not (numberp b))
                               (equal b 0))
                           (equal (fix a) c))))))
    (and (equal (equal (plus a (times b c)) c) rhs)
         (equal (equal (plus (times b c) a) c) rhs)
         (equal (equal (plus a (times c b)) c) rhs)
         (equal (equal (plus (times c b) a) c) rhs))))

(prove-lemma remainder-remainder (rewrite)
  (implies (equal (remainder a b) 0)
           (and (equal (remainder (remainder c a) b)
                       (remainder c b))
                (equal (remainder (remainder c b) a)
                       (remainder c b))))
  ((disable remainder-lessp-linear
            remainder-plus-arg1-simple
            difference-not-lessp
            lessp-times-single-linear)))

(prove-lemma remainder-plus-remainder-arg1 (rewrite)
  (and (implies (equal (remainder b d) 0)
                (equal (remainder (plus a (remainder c b)) d)
                       (remainder (plus a c) d)))
       (implies (equal (remainder b d) 0)
                (equal (remainder (plus (remainder c b) a) d)
                       (remainder (plus c a) d))))
  ((disable remainder-lessp-linear
            dichotomy
            difference-not-lessp
            difference-lessp
            sub1-remainder
            sub1-plus
            remainder-difference-arg1
            difference-remainder-arg2
            sub1-difference
            remainder-plus-arg1-simple)))

(prove-lemma remainder-times-arg1-arg2 (rewrite)
  (and
   (equal (remainder (times a c) (times b c))
          (times c (remainder a b)))
   (equal (remainder (times c a) (times b c))
          (times c (remainder a b)))
   (equal (remainder (times a c) (times c b))
          (times c (remainder a b)))
   (equal (remainder (times c a) (times c b))
          (times c (remainder a b))))
  ((disable sub1-remainder
            lessp-transpose-meta
            difference-lessp
            difference-remainder-arg1
            sub1-plus
            sub1-times
            sub1-quotient
            remainder-difference-arg1
            equal-transpose-meta
            dichotomy
            difference-difference-arg1-commutes-meta
            difference-times-arg1
            lessp-times-single-linear
            difference-times-arg1-simpler
            equal-quotient-0
            quotient-lessp-linear
            equal-odometer-simple
            lessp-times-linear
            lessp-odometer-simple
            times-add1
            difference-times-arg1-meta
            difference-not-lessp
            remainder-lessp-linear
            sub1-difference
            quotient-plus-arg2
            plus-commutes-nest-meta
            quotient-times-arg1
            quotient-times-arg2
            no-divisors-of-zero
            difference-times-arg1-simplest
            remainder-times-arg1
            remainder-plus-arg1-simple)))

(prove-lemma quotient-times-arg2-commutes (rewrite)
  (and (equal (quotient (quotient (times a c) b) c)
              (if (or (not (numberp c))
                      (equal c 0))
                  0
                (quotient a b)))
       (equal (quotient (quotient (times c a) b) c)
              (if (or (not (numberp c))
                      (equal c 0))
                  0
                (quotient a b))))
  ((use (quotient-times-arg2 (a (times a c)) (zb c) (zc b))
        (quotient-times-arg2 (a (times a c)) (zb b) (zc c)))
   (disable quotient-times-arg2
            lessp-transpose-meta
            sub1-remainder
            sub1-quotient
            difference-lessp
            plus-is-0
            dichotomy
            remainder-times-arg2
            lessp-quotient-arg1-linear
            lessp-quotient
            equal-quotient-0
            lessp-quotient-arg2-linear
            difference-times-arg1-arg2
            quotient-plus-arg1
            difference-times-arg1
            sub1-times
            difference-not-lessp
            difference-times-arg1-meta
            remainder-lessp-linear)))

(prove-lemma quotient-times-arg1-arg2 (rewrite)
  (and
   (equal (quotient (times a c) (times b c))
          (if (or (not (numberp c)) (equal c 0))
              0
            (quotient a b)))
   (equal (quotient (times c a) (times b c))
          (if (or (not (numberp c)) (equal c 0))
              0
            (quotient a b)))
   (equal (quotient (times a c) (times c b))
          (if (or (not (numberp c)) (equal c 0))
              0
            (quotient a b)))
   (equal (quotient (times c a) (times c b))
          (if (or (not (numberp c)) (equal c 0))
              0
            (quotient a b))))
  ((disable times
            lessp-times-single-linear
            lessp-transpose-meta
            lessp-odometer-simple
            quotient-plus-arg1
            quotient-lessp-linear
            remainder-plus-arg1-simple
            equal-times-cancel-meta
            difference-lessp
            lessp-quotient
            difference-plus-arg1
            difference-times-arg2
            dichotomy
            equal-transpose-meta
            quotient-remainder
            difference-times-arg1-meta
            difference-not-lessp
            remainder-lessp-linear)))

(prove-lemma lessp-quotient-arg1-kb-linear (rewrite)
  (and (implies (and (not (lessp b a))
                     (numberp c)
                     (not (equal c 0)))
                (lessp a (plus c (times c (quotient b c)))))
       (implies (and (lessp a b) ; because of free variables
                     (numberp c)
                     (not (equal c 0)))
                (lessp a (plus c (times c (quotient b c))))))
  ((disable equal-odometer-simple)))

(prove-lemma lessp-quotient-arg2-kb-linear (rewrite)
  (and (implies (and (not (lessp b a))
                     (numberp a)
                     (not (equal a 0)))
                (lessp c (plus a (times b (quotient c a)))))
       (implies (and (not (lessp b a))
                     (numberp a)
                     (not (equal a 0)))
                (lessp c (plus a (times (quotient c a) b)))))
  ((disable lessp-times-linear
            sub1-quotient
            lessp-times-single-linear
            lessp-transpose-meta
            difference-not-lessp
            lessp-odometer-simple)))

(prove-lemma plus-difference-difference-cancellation (rewrite)
  (and (implies (and (not (lessp b a))
                     (not (lessp (plus c a) b)))
                (equal (plus b d (difference c (difference b a)))
                       (plus a c d)))
       (implies (and (not (lessp b a))
                     (not (lessp (plus c a) b)))
                (equal (plus b (difference c (difference b a)) d)
                       (plus a c d)))
       (implies (and (not (lessp b a))
                     (not (lessp (plus c a) b)))
                (equal (plus b (difference c (difference b a)))
                       (plus a c)))))

(prove-lemma quotient-times-arg2-kb (rewrite)
  (equal (quotient (quotient a b) c)
         (quotient (quotient a c) b))
  ((use (quotient-times-arg2 (a a) (zb b) (zc c))
        (quotient-times-arg2 (a a) (zb c) (zc b)))
   (disable quotient-times-arg2
            quotient
            times)))

(prove-lemma times-quotient-remainder (rewrite)
  (and
   (equal (plus (times a (remainder c b))
                (times a b (quotient c b)))
          (times c a))
   (equal (plus (times a (remainder c b))
                (times b a (quotient c b)))
          (times c a))
   (equal (plus (times (remainder c b) a)
                (times b (quotient c b) a))
          (times c a))

   (equal (plus (times a d (remainder c b))
                (times a d b (quotient c b)))
          (times c a d))
   (equal (plus (times a d (remainder c b))
                (times a b d (quotient c b)))
          (times c a d))
   (equal (plus (times a d (remainder c b))
                (times b a d (quotient c b)))
          (times c a d))
   (equal (plus (times a (remainder c b) d)
                (times a b (quotient c b) d))
          (times c a d))
   (equal (plus (times a (remainder c b) d)
                (times b a (quotient c b) d))
          (times c a d))

   (equal (plus (times a (remainder c b))
                (times a b (quotient c b))
                d)
          (plus (times c a) d))
   (equal (plus (times a (remainder c b))
                (times b a (quotient c b))
                d)
          (plus (times c a) d))
   (equal (plus (times (remainder c b) a)
                (times b (quotient c b) a)
                d)
          (plus (times c a) d))

   (equal (plus (times a d (remainder c b))
                (times a d b (quotient c b))
                e)
          (plus (times c a d) e))
   (equal (plus (times a d (remainder c b))
                (times a b d (quotient c b))
                e)
          (plus (times c a d) e))
   (equal (plus (times a d (remainder c b))
                (times b a d (quotient c b))
                e)
          (plus (times c a d) e))
   (equal (plus (times a b (quotient c b) d)
                (times a (remainder c b) d)
                e)
          (plus (times c a d) e))
   (equal (plus (times a (remainder c b) d)
                (times b a (quotient c b) d)
                e)
          (plus (times c a d) e)))
  ((disable sub1-times
            plus-commutes-meta
            equal-half-odometer
            lessp-times-cancel-meta
            sub1-quotient
            lessp-transpose-meta
            difference-not-lessp
            sub1-remainder
            difference-lessp
            equal-quotient-0
            remainder-difference-arg1
            remainder-lessp-linear
            equal-odometer
            lessp-quarter-odometer-right)))

(prove-lemma quotient-sub1-arg1 (rewrite)
  (equal (quotient (sub1 a) b)
         (if (or (not (numberp b))
                 (equal b 0))
             0
           (if (equal (sub1 b) 0)
               (sub1 a)
             (if (equal (remainder a b) 0)
                 (quotient (difference a b) b)
               (quotient a b)))))
  ((disable remainder-lessp-linear
            dichotomy
            plus-commutes-nest-meta
            plus-commutes-meta
            lessp-transpose-meta
            equal-transpose-meta
            difference-not-lessp
            lessp-times-single-linear)))


;;; lessp-cross-dot-linear and not-lessp-dot-cross-linear are expensive,
;;; when applied using the key (times a b).  If a is a complex expression,
;;; it gets duplicated when rewriting (times a a) within the right hand side.

;;; The following two lemmas are not needed for proofs in this event file.
;;; They will be enabled at the end of this proof file.

(prove-lemma lessp-cross-dot-linear (rewrite)
  (implies (or (lessp a b)
               (lessp b a)
               (and (not (equal a b))
                    (or (and (numberp a) (not (equal a 0)))
                        (and (numberp b) (not (equal b 0))))))
           (lessp (plus (times a b) (times a b))
                  (plus (times a a) (times b b))))
  ((induct (lessp a b))))

(disable lessp-cross-dot-linear)

(prove-lemma not-lessp-dot-cross-linear (rewrite)
  (not (lessp (plus (times a a) (times b b))
              (plus (times a b) (times a b))))
  ((induct (lessp a b))))

(disable not-lessp-dot-cross-linear)

;;; These rewrite rules should be placed at the end of the event file to
;;; assure that they are applied first.  They are here because we have
;;; economized on various Knuth-Bendix rules, by assuming if-normalization
;;; occurs.  In fact, if-normalization only occurs after rewriting has
;;; finished.  These rules are expensive and are rarely needed.  For this
;;; reason we include them in a deftheory so that they may be easily
;;; disabled.

;;; times-if is needed to speed up difference-times-arg1-arg2.  In particular
;;; it avoids using difference-times-arg1 needlessly, by simplifying
;;; (times b (quotient a a)) to (if (equal a 0) 0 (if (numberp a) b 0)).

(prove-lemma times-if (rewrite)
  (implies (equal aa a) ; to avoid repeated rewriting
           (and (equal (times a (if b c d))
                       (if b (times aa c) (times aa d)))
                (equal (times (if b c d) a)
                       (if b (times c aa) (times d aa))))))


(prove-lemma plus-if (rewrite)
  (implies (equal dd d)
           (and (equal (plus (if a b c) d)
                       (if a (plus b dd) (plus c dd)))
                (equal (plus d (if a b c))
                       (if a (plus dd b) (plus dd c))))))

(prove-lemma difference-if (rewrite)
  (implies
   (equal dd d)
   (and (equal (difference (if a b c) d)
               (if a (difference b dd) (difference c dd)))
        (equal (difference d (if a b c))
               (if a (difference dd b) (difference dd c))))))

(prove-lemma lessp-if (rewrite)
  (implies (equal dd d)
           (and (equal (lessp (if a b c) d)
                       (if a (lessp b dd) (lessp c dd)))
                (equal (lessp d (if a b c))
                       (if a (lessp dd b) (lessp dd c))))))

(prove-lemma equal-if (rewrite)
  (implies (equal dd d)
           (equal (equal (if a b c) d)
                  (if a (equal b dd) (equal c dd)))))

(prove-lemma add1-if (rewrite)
  (equal (add1 (if a b c))
         (if a (add1 b) (add1 c))))

(prove-lemma sub1-if (rewrite)
  (equal (sub1 (if a b c))
         (if a (sub1 b) (sub1 c))))

(prove-lemma remainder-if (rewrite)
  (implies (equal dd d)
           (and
            (equal (remainder (if a b c) d)
                   (if a (remainder b dd) (remainder c dd)))
            (equal (remainder dd (if a b c))
                   (if a (remainder dd b) (remainder dd c))))))

(prove-lemma quotient-if (rewrite)
  (implies (equal dd d)
           (and
            (equal (quotient (if a b c) d)
                   (if a (quotient b dd) (quotient c dd)))
            (equal (quotient dd (if a b c))
                   (if a (quotient dd b) (quotient dd c))))))

(deftheory if-normalization
  (times-if
   plus-if
   difference-if
   lessp-if
   equal-if
   add1-if
   sub1-if
   remainder-if
   quotient-if))

(make-lib "modularithmetic-98")