#|
 Copyright (C) 1987, 1994 by William R. Bevier.  All Rights Reserved.

 You may copy and distribute verbatim copies of this Nqthm-1992 event script as
 you receive it, in any medium, including embedding it verbatim in derivative
 works, provided that you conspicuously and appropriately publish on each copy
 a valid copyright notice "Copyright (C) 1987, 1994 by William R. Bevier.  All
 Rights Reserved."

 NO WARRANTY

 William R. Bevier PROVIDES ABSOLUTELY NO WARRANTY.  THE EVENT SCRIPT IS
 PROVIDED "AS IS" WITHOUT WARRANTY OF ANY KIND, EITHER EXPRESS OR IMPLIED,
 INCLUDING, BUT NOT LIMITED TO, ANY IMPLIED WARRANTIES OF MERCHANTABILITY AND
 FITNESS FOR A PARTICULAR PURPOSE.  THE ENTIRE RISK AS TO THE QUALITY AND
 PERFORMANCE OF THE SCRIPT IS WITH YOU.  SHOULD THE SCRIPT PROVE DEFECTIVE, YOU
 ASSUME THE COST OF ALL NECESSARY SERVICING, REPAIR OR CORRECTION.

 IN NO EVENT WILL William R. Bevier BE LIABLE TO YOU FOR ANY DAMAGES, ANY LOST
 PROFITS, LOST MONIES, OR OTHER SPECIAL, INCIDENTAL OR CONSEQUENTIAL DAMAGES
 ARISING OUT OF THE USE OR INABILITY TO USE THIS SCRIPT (INCLUDING BUT NOT
 LIMITED TO LOSS OF DATA OR DATA BEING RENDERED INACCURATE OR LOSSES SUSTAINED
 BY THIRD PARTIES), EVEN IF YOU HAVE ADVISED US OF THE POSSIBILITY OF SUCH
 DAMAGES, OR FOR ANY CLAIM BY ANY OTHER PARTY.''

|#

;
; Kit Script for NQTHM-1992
; Bill Bevier
; Computational Logic, Inc.
; bevier@cli.com
;
; This script is derived from the original Kit proof script. The
; original script contains the events entered by the author, and
; extends over some 62 files. The original runs on a version of NQTHM
; modified by the author to handle deftheory events and hints, and to
; handle opening up of constant functions in a certain way.
;
; This script was derived by replaying the original in PC-NQTHM, and
; simultaneously writing out a translation of each event that would
; allow the script to play in NQTHM-1992. The main differences between
; the events which appear here and those in the original are:
; 
;   1. Constant expressions are expanded in place here. The body of no
;      definition or lemma is modified from the original other than the
;      replacement of a constant expression by its value. 
;   2. A few extra deftheory events and enable-theory hints are
;      required in this script, primarily for controlling *1* functions.
;  


(BOOT-STRAP NQTHM)

(PROVE-LEMMA PLUS-RIGHT-ID2
             (REWRITE)
             (IMPLIES (NOT (NUMBERP Y))
                      (EQUAL (PLUS X Y) (FIX X)))
             ((ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE PLUS-RIGHT-ID2)

(PROVE-LEMMA PLUS-ADD1
             (REWRITE)
             (EQUAL (PLUS X (ADD1 Y))
                    (IF (NUMBERP Y)
                        (ADD1 (PLUS X Y))
                        (ADD1 X)))
             ((ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE PLUS-ADD1)

(PROVE-LEMMA COMMUTATIVITY2-OF-PLUS
             (REWRITE)
             (EQUAL (PLUS X (PLUS Y Z))
                    (PLUS Y (PLUS X Z)))
             ((ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE COMMUTATIVITY2-OF-PLUS)

(PROVE-LEMMA COMMUTATIVITY-OF-PLUS
             (REWRITE)
             (EQUAL (PLUS X Y) (PLUS Y X))
             ((ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE COMMUTATIVITY-OF-PLUS)

(PROVE-LEMMA ASSOCIATIVITY-OF-PLUS
             (REWRITE)
             (EQUAL (PLUS (PLUS X Y) Z)
                    (PLUS X (PLUS Y Z)))
             ((ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE ASSOCIATIVITY-OF-PLUS)

(PROVE-LEMMA PLUS-EQUAL-0
             (REWRITE)
             (EQUAL (EQUAL (PLUS A B) '0)
                    (AND (ZEROP A) (ZEROP B)))
             ((ENABLE PLUS-RIGHT-ID2 COMMUTATIVITY-OF-PLUS)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE PLUS-EQUAL-0)

(PROVE-LEMMA DIFFERENCE-X-X
             (REWRITE)
             (EQUAL (DIFFERENCE X X) '0)
             ((ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE DIFFERENCE-X-X)

(PROVE-LEMMA DIFFERENCE-PLUS
             (REWRITE)
             (AND (EQUAL (DIFFERENCE (PLUS X Y) X)
                         (FIX Y))
                  (EQUAL (DIFFERENCE (PLUS Y X) X)
                         (FIX Y)))
             ((ENABLE PLUS-RIGHT-ID2 COMMUTATIVITY-OF-PLUS)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE DIFFERENCE-PLUS)

(PROVE-LEMMA PLUS-CANCELLATION
             (REWRITE)
             (EQUAL (EQUAL (PLUS A B) (PLUS A C))
                    (EQUAL (FIX B) (FIX C)))
             ((ENABLE PLUS-RIGHT-ID2 COMMUTATIVITY-OF-PLUS)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE PLUS-CANCELLATION)

(PROVE-LEMMA DIFFERENCE-0
             (REWRITE)
             (IMPLIES (NOT (LESSP Y X))
                      (EQUAL (DIFFERENCE X Y) '0))
             ((ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE DIFFERENCE-0)

(PROVE-LEMMA EQUAL-DIFFERENCE-0
             (REWRITE)
             (EQUAL (EQUAL '0 (DIFFERENCE X Y))
                    (NOT (LESSP Y X)))
             ((ENABLE DIFFERENCE-0)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE EQUAL-DIFFERENCE-0)

(PROVE-LEMMA DIFFERENCE-CANCELLATION-0
             (REWRITE)
             (EQUAL (EQUAL X (DIFFERENCE X Y))
                    (AND (NUMBERP X)
                         (OR (EQUAL X '0) (ZEROP Y))))
             ((ENABLE DIFFERENCE-0)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE DIFFERENCE-CANCELLATION-0)

(PROVE-LEMMA DIFFERENCE-CANCELLATION-1
             (REWRITE)
             (EQUAL (EQUAL (DIFFERENCE X Y)
                           (DIFFERENCE Z Y))
                    (IF (LESSP X Y)
                        (NOT (LESSP Y Z))
                        (IF (LESSP Z Y)
                            (NOT (LESSP Y X))
                            (EQUAL (FIX X) (FIX Z)))))
             ((ENABLE DIFFERENCE-0 EQUAL-DIFFERENCE-0)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE DIFFERENCE-CANCELLATION-1)

(PROVE-LEMMA TIMES-ZERO2
             (REWRITE)
             (IMPLIES (NOT (NUMBERP Y))
                      (EQUAL (TIMES X Y) '0))
             ((ENABLE PLUS-RIGHT-ID2 COMMUTATIVITY-OF-PLUS)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE TIMES-ZERO2)

(PROVE-LEMMA DISTRIBUTIVITY-OF-TIMES-OVER-PLUS
             (REWRITE)
             (EQUAL (TIMES X (PLUS Y Z))
                    (PLUS (TIMES X Y) (TIMES X Z)))
             ((ENABLE COMMUTATIVITY2-OF-PLUS ASSOCIATIVITY-OF-PLUS)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE DISTRIBUTIVITY-OF-TIMES-OVER-PLUS)

(PROVE-LEMMA TIMES-ADD1
             (REWRITE)
             (EQUAL (TIMES X (ADD1 Y))
                    (IF (NUMBERP Y)
                        (PLUS X (TIMES X Y))
                        (FIX X)))
             ((ENABLE PLUS-RIGHT-ID2 COMMUTATIVITY-OF-PLUS)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE TIMES-ADD1)

(PROVE-LEMMA COMMUTATIVITY-OF-TIMES
             (REWRITE)
             (EQUAL (TIMES X Y) (TIMES Y X))
             ((ENABLE TIMES-ZERO2 TIMES-ADD1)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE COMMUTATIVITY-OF-TIMES)

(PROVE-LEMMA COMMUTATIVITY2-OF-TIMES
             (REWRITE)
             (EQUAL (TIMES X (TIMES Y Z))
                    (TIMES Y (TIMES X Z)))
             ((ENABLE DISTRIBUTIVITY-OF-TIMES-OVER-PLUS COMMUTATIVITY-OF-TIMES)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE COMMUTATIVITY2-OF-TIMES)

(PROVE-LEMMA ASSOCIATIVITY-OF-TIMES
             (REWRITE)
             (EQUAL (TIMES (TIMES X Y) Z)
                    (TIMES X (TIMES Y Z)))
             ((ENABLE COMMUTATIVITY-OF-TIMES COMMUTATIVITY2-OF-TIMES)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE ASSOCIATIVITY-OF-TIMES)

(PROVE-LEMMA EQUAL-TIMES-0
             (REWRITE)
             (EQUAL (EQUAL (TIMES X Y) '0)
                    (OR (ZEROP X) (ZEROP Y)))
             ((ENABLE PLUS-EQUAL-0 TIMES-ZERO2 COMMUTATIVITY-OF-TIMES)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE EQUAL-TIMES-0)

(DEFN EXP
      (I J)
      (IF (ZEROP J)
          '1
          (TIMES I (EXP I (SUB1 J))))
      NIL)

(PROVE-LEMMA EXP-PLUS
             (REWRITE)
             (EQUAL (EXP I (PLUS J K))
                    (TIMES (EXP I J) (EXP I K)))
             ((ENABLE COMMUTATIVITY-OF-TIMES ASSOCIATIVITY-OF-TIMES EXP)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE EXP-PLUS)

(PROVE-LEMMA EQUAL-LESSP
             (REWRITE)
             (EQUAL (EQUAL (LESSP X Y) Z)
                    (IF (LESSP X Y)
                        (EQUAL '*1*TRUE Z)
                        (EQUAL '*1*FALSE Z)))
             ((ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE EQUAL-LESSP)

(PROVE-LEMMA DIFFERENCE-ELIM
             (ELIM)
             (IMPLIES (AND (NUMBERP Y) (NOT (LESSP Y X)))
                      (EQUAL (PLUS X (DIFFERENCE Y X)) Y))
             ((ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(PROVE-LEMMA REMAINDER-QUOTIENT
             (REWRITE)
             (EQUAL (PLUS (REMAINDER X Y)
                          (TIMES Y (QUOTIENT X Y)))
                    (FIX X))
             ((ENABLE COMMUTATIVITY2-OF-PLUS COMMUTATIVITY-OF-PLUS TIMES-ZERO2
                      TIMES-ADD1 COMMUTATIVITY-OF-TIMES)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE REMAINDER-QUOTIENT)

(PROVE-LEMMA REMAINDER-WRT-1
             (REWRITE)
             (EQUAL (REMAINDER Y '1) '0)
             ((ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE REMAINDER-WRT-1)

(PROVE-LEMMA REMAINDER-WRT-12
             (REWRITE)
             (IMPLIES (NOT (NUMBERP X))
                      (EQUAL (REMAINDER Y X) (FIX Y)))
             ((ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE REMAINDER-WRT-12)

(PROVE-LEMMA LESSP-REMAINDER2
             (REWRITE GENERALIZE)
             (EQUAL (LESSP (REMAINDER X Y) Y)
                    (NOT (ZEROP Y)))
             ((ENABLE EQUAL-LESSP REMAINDER-WRT-12)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE LESSP-REMAINDER2)

(PROVE-LEMMA REMAINDER-X-X
             (REWRITE)
             (EQUAL (REMAINDER X X) '0)
             ((ENABLE DIFFERENCE-0)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE REMAINDER-X-X)

(PROVE-LEMMA REMAINDER-QUOTIENT-ELIM
             (ELIM)
             (IMPLIES (AND (NOT (ZEROP Y)) (NUMBERP X))
                      (EQUAL (PLUS (REMAINDER X Y)
                                   (TIMES Y (QUOTIENT X Y)))
                             X))
             ((ENABLE REMAINDER-QUOTIENT)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(PROVE-LEMMA LESSP-TIMES-1
             (REWRITE)
             (IMPLIES (NOT (ZEROP I))
                      (NOT (LESSP (TIMES I J) J)))
             ((ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE LESSP-TIMES-1)

(PROVE-LEMMA LESSP-TIMES-2
             (REWRITE)
             (IMPLIES (NOT (ZEROP I))
                      (NOT (LESSP (TIMES J I) J)))
             ((ENABLE COMMUTATIVITY-OF-TIMES LESSP-TIMES-1)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE LESSP-TIMES-2)

(PROVE-LEMMA LESSP-QUOTIENT1
             (REWRITE)
             (EQUAL (LESSP (QUOTIENT I J) I)
                    (AND (NOT (ZEROP I))
                         (OR (ZEROP J) (NOT (EQUAL J '1)))))
             ((ENABLE PLUS-EQUAL-0 DIFFERENCE-0 EQUAL-DIFFERENCE-0
                      EQUAL-TIMES-0 EQUAL-LESSP LESSP-REMAINDER2
                      REMAINDER-QUOTIENT-ELIM LESSP-TIMES-1)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE LESSP-QUOTIENT1)

(PROVE-LEMMA LESSP-REMAINDER1
             (REWRITE)
             (EQUAL (LESSP (REMAINDER X Y) X)
                    (AND (NOT (ZEROP Y))
                         (AND (NOT (ZEROP X))
                              (NOT (LESSP X Y)))))
             ((ENABLE PLUS-EQUAL-0 COMMUTATIVITY-OF-TIMES EQUAL-TIMES-0
                      EQUAL-LESSP REMAINDER-WRT-12 LESSP-REMAINDER2
                      REMAINDER-QUOTIENT-ELIM)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE LESSP-REMAINDER1)

(PROVE-LEMMA DIFFERENCE-PLUS1
             (REWRITE)
             (EQUAL (DIFFERENCE (PLUS X Y) X)
                    (FIX Y))
             ((ENABLE DIFFERENCE-PLUS)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE DIFFERENCE-PLUS1)

(PROVE-LEMMA DIFFERENCE-PLUS2
             (REWRITE)
             (EQUAL (DIFFERENCE (PLUS Y X) X)
                    (FIX Y))
             ((ENABLE COMMUTATIVITY-OF-PLUS DIFFERENCE-PLUS1)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE DIFFERENCE-PLUS2)

(PROVE-LEMMA DIFFERENCE-PLUS-CANCELATION
             (REWRITE)
             (EQUAL (DIFFERENCE (PLUS X Y) (PLUS X Z))
                    (DIFFERENCE Y Z))
             ((ENABLE DIFFERENCE-0)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE DIFFERENCE-PLUS-CANCELATION)

(PROVE-LEMMA TIMES-DIFFERENCE
             (REWRITE)
             (EQUAL (TIMES X (DIFFERENCE C W))
                    (DIFFERENCE (TIMES C X) (TIMES W X)))
             ((ENABLE PLUS-EQUAL-0 DIFFERENCE-0 EQUAL-DIFFERENCE-0
                      COMMUTATIVITY-OF-TIMES EQUAL-TIMES-0 DIFFERENCE-ELIM
                      DIFFERENCE-PLUS-CANCELATION)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE TIMES-DIFFERENCE)

(DEFN DIVIDES
      (X Y)
      (ZEROP (REMAINDER Y X))
      NIL)

(PROVE-LEMMA DIVIDES-TIMES
             (REWRITE)
             (EQUAL (REMAINDER (TIMES X Z) Z) '0)
             ((ENABLE COMMUTATIVITY-OF-TIMES EQUAL-TIMES-0 REMAINDER-WRT-12
                      DIFFERENCE-PLUS1)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE DIVIDES-TIMES)

(PROVE-LEMMA DIFFERENCE-PLUS3
             (REWRITE)
             (EQUAL (DIFFERENCE (PLUS B (PLUS A C)) A)
                    (PLUS B C))
             ((ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE DIFFERENCE-PLUS3)

(PROVE-LEMMA DIFFERENCE-ADD1-CANCELLATION
             (REWRITE)
             (EQUAL (DIFFERENCE (ADD1 (PLUS Y Z)) Z)
                    (ADD1 Y))
             ((ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE DIFFERENCE-ADD1-CANCELLATION)

(PROVE-LEMMA REMAINDER-ADD1
             (REWRITE)
             (IMPLIES (AND (NOT (ZEROP Y))
                           (NOT (EQUAL Y '1)))
                      (NOT (EQUAL (REMAINDER (ADD1 (TIMES X Y)) Y)
                                  '0)))
             ((ENABLE COMMUTATIVITY-OF-PLUS DIFFERENCE-0
                      COMMUTATIVITY-OF-TIMES DIFFERENCE-ADD1-CANCELLATION)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE REMAINDER-ADD1)

(PROVE-LEMMA DIVIDES-PLUS-REWRITE1
             (REWRITE)
             (IMPLIES (AND (EQUAL (REMAINDER X Z) '0)
                           (EQUAL (REMAINDER Y Z) '0))
                      (EQUAL (REMAINDER (PLUS X Y) Z) '0))
             ((ENABLE PLUS-RIGHT-ID2 COMMUTATIVITY2-OF-PLUS
                      COMMUTATIVITY-OF-PLUS ASSOCIATIVITY-OF-PLUS
                      COMMUTATIVITY-OF-TIMES DIFFERENCE-ELIM REMAINDER-WRT-12
                      LESSP-REMAINDER2 REMAINDER-QUOTIENT-ELIM DIVIDES-TIMES
                      DIFFERENCE-PLUS3)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE DIVIDES-PLUS-REWRITE1)

(PROVE-LEMMA DIVIDES-PLUS-REWRITE2
             (REWRITE)
             (IMPLIES (AND (EQUAL (REMAINDER X Z) '0)
                           (NOT (EQUAL (REMAINDER Y Z) '0)))
                      (NOT (EQUAL (REMAINDER (PLUS X Y) Z) '0)))
             ((ENABLE COMMUTATIVITY2-OF-PLUS COMMUTATIVITY-OF-PLUS
                      ASSOCIATIVITY-OF-PLUS COMMUTATIVITY-OF-TIMES
                      DIFFERENCE-ELIM REMAINDER-WRT-12 LESSP-REMAINDER2
                      REMAINDER-QUOTIENT-ELIM DIFFERENCE-PLUS3)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE DIVIDES-PLUS-REWRITE2)

(PROVE-LEMMA DIVIDES-PLUS-REWRITE
             (REWRITE)
             (IMPLIES (EQUAL (REMAINDER X Z) '0)
                      (EQUAL (EQUAL (REMAINDER (PLUS X Y) Z) '0)
                             (EQUAL (REMAINDER Y Z) '0)))
             ((ENABLE DIVIDES-PLUS-REWRITE1 DIVIDES-PLUS-REWRITE2)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE DIVIDES-PLUS-REWRITE)

(PROVE-LEMMA LESSP-PLUS-CANCELATION
             (REWRITE)
             (EQUAL (LESSP (PLUS X Y) (PLUS X Z))
                    (LESSP Y Z))
             ((ENABLE EQUAL-LESSP)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE LESSP-PLUS-CANCELATION)

(PROVE-LEMMA DIVIDES-PLUS-REWRITE-COMMUTED
             (REWRITE)
             (IMPLIES (EQUAL (REMAINDER X Z) '0)
                      (EQUAL (EQUAL (REMAINDER (PLUS Y X) Z) '0)
                             (EQUAL (REMAINDER Y Z) '0)))
             ((ENABLE COMMUTATIVITY-OF-PLUS DIVIDES-PLUS-REWRITE)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE DIVIDES-PLUS-REWRITE-COMMUTED)

(PROVE-LEMMA EUCLID
             (REWRITE)
             (IMPLIES (EQUAL (REMAINDER X Z) '0)
                      (EQUAL (EQUAL (REMAINDER (DIFFERENCE Y X) Z)
                                    '0)
                             (IF (LESSP X Y)
                                 (EQUAL (REMAINDER Y Z) '0)
                                 '*1*TRUE)))
             ((ENABLE PLUS-RIGHT-ID2 COMMUTATIVITY2-OF-PLUS
                      COMMUTATIVITY-OF-PLUS DIFFERENCE-0
                      COMMUTATIVITY-OF-TIMES DIFFERENCE-ELIM REMAINDER-WRT-12
                      LESSP-REMAINDER2 REMAINDER-QUOTIENT-ELIM DIVIDES-TIMES
                      DIVIDES-PLUS-REWRITE1 DIVIDES-PLUS-REWRITE-COMMUTED)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE EUCLID)

(PROVE-LEMMA LESSP-TIMES-CANCELLATION
             (REWRITE)
             (EQUAL (LESSP (TIMES X Z) (TIMES Y Z))
                    (AND (NOT (ZEROP Z)) (LESSP X Y)))
             ((ENABLE TIMES-ZERO2 COMMUTATIVITY-OF-TIMES EQUAL-TIMES-0
                      EQUAL-LESSP)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE LESSP-TIMES-CANCELLATION)

(PROVE-LEMMA LESSP-PLUS-CANCELLATION3
             (REWRITE)
             (EQUAL (LESSP Y (PLUS X Y))
                    (NOT (ZEROP X)))
             ((ENABLE EQUAL-LESSP)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE LESSP-PLUS-CANCELLATION3)

(PROVE-LEMMA QUOTIENT-TIMES1
             (REWRITE)
             (IMPLIES (AND (NUMBERP Y)
                           (AND (NUMBERP X)
                                (AND (NOT (EQUAL X '0))
                                     (DIVIDES X Y))))
                      (EQUAL (TIMES X (QUOTIENT Y X)) Y))
             ((ENABLE LESSP-REMAINDER2 REMAINDER-QUOTIENT-ELIM DIVIDES)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE QUOTIENT-TIMES1)

(PROVE-LEMMA QUOTIENT-LESSP
             (REWRITE)
             (IMPLIES (AND (NOT (ZEROP X)) (LESSP X Y))
                      (NOT (EQUAL (QUOTIENT Y X) '0)))
             ((ENABLE COMMUTATIVITY-OF-PLUS COMMUTATIVITY-OF-TIMES
                      LESSP-REMAINDER2 REMAINDER-QUOTIENT-ELIM)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE QUOTIENT-LESSP)

(PROVE-LEMMA TIMES-ID-IFF-1
             (REWRITE)
             (EQUAL (EQUAL Z (TIMES W Z))
                    (AND (NUMBERP Z)
                         (OR (EQUAL Z '0) (EQUAL W '1))))
             ((ENABLE COMMUTATIVITY-OF-PLUS TIMES-ZERO2 COMMUTATIVITY-OF-TIMES
                      LESSP-TIMES-2)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE TIMES-ID-IFF-1)

(PROVE-LEMMA DIVIDES-TIMES1
             (REWRITE)
             (IMPLIES (EQUAL A (TIMES Z Y))
                      (EQUAL (REMAINDER A Z) '0))
             ((ENABLE COMMUTATIVITY-OF-TIMES DIVIDES-TIMES)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE DIVIDES-TIMES1)

(PROVE-LEMMA TIMES-IDENTITY1
             (REWRITE)
             (IMPLIES (AND (NUMBERP Y)
                           (AND (NOT (EQUAL Y '1))
                                (AND (NOT (EQUAL Y '0))
                                     (NOT (EQUAL X '0)))))
                      (NOT (EQUAL X (TIMES X Y))))
             ((ENABLE LESSP-TIMES-2)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE TIMES-IDENTITY1)

(PROVE-LEMMA TIMES-IDENTITY
             (REWRITE)
             (EQUAL (EQUAL X (TIMES X Y))
                    (OR (EQUAL X '0)
                        (AND (NUMBERP X) (EQUAL Y '1))))
             ((ENABLE PLUS-RIGHT-ID2 COMMUTATIVITY-OF-PLUS
                      COMMUTATIVITY-OF-TIMES LESSP-TIMES-2 TIMES-ID-IFF-1)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE TIMES-IDENTITY)

(PROVE-LEMMA QUOTIENT-DIVIDES
             (REWRITE)
             (IMPLIES (AND (NUMBERP Y)
                           (NOT (EQUAL (TIMES X (QUOTIENT Y X)) Y)))
                      (NOT (EQUAL (REMAINDER Y X) '0)))
             ((ENABLE TIMES-ZERO2 COMMUTATIVITY-OF-TIMES REMAINDER-WRT-12
                      LESSP-REMAINDER2 REMAINDER-QUOTIENT-ELIM)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE QUOTIENT-DIVIDES)

(PROVE-LEMMA REMAINDER-TIMES
             (REWRITE)
             (EQUAL (REMAINDER (TIMES Y X) Y) '0)
             ((ENABLE COMMUTATIVITY-OF-TIMES DIVIDES-TIMES)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE REMAINDER-TIMES)

(PROVE-LEMMA QUOTIENT-TIMES
             (REWRITE)
             (EQUAL (QUOTIENT (TIMES Y X) Y)
                    (IF (ZEROP Y) '0 (FIX X)))
             ((ENABLE TIMES-ZERO2 COMMUTATIVITY-OF-TIMES DIFFERENCE-PLUS1)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE QUOTIENT-TIMES)

(PROVE-LEMMA DISTRIBUTIVITY-OF-DIVIDES
             (REWRITE)
             (IMPLIES (AND (NOT (ZEROP A)) (DIVIDES A W))
                      (EQUAL (TIMES C (QUOTIENT W A))
                             (QUOTIENT (TIMES C W) A)))
             ((ENABLE TIMES-ZERO2 COMMUTATIVITY-OF-TIMES
                      COMMUTATIVITY2-OF-TIMES LESSP-REMAINDER2
                      REMAINDER-QUOTIENT-ELIM QUOTIENT-TIMES DIVIDES)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE DISTRIBUTIVITY-OF-DIVIDES)

(PROVE-LEMMA IF-TIMES-THEN-DIVIDES
             (REWRITE)
             (IMPLIES (AND (NOT (ZEROP C))
                           (NOT (DIVIDES C X)))
                      (NOT (EQUAL (TIMES C Y) X)))
             ((ENABLE REMAINDER-TIMES DIVIDES)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE IF-TIMES-THEN-DIVIDES)

(PROVE-LEMMA TIMES-EQUAL-1
             (REWRITE)
             (EQUAL (EQUAL (TIMES A B) '1)
                    (AND (NOT (EQUAL A '0))
                         (AND (NOT (EQUAL B '0))
                              (AND (NUMBERP A)
                                   (AND (NUMBERP B)
                                        (AND (EQUAL (SUB1 A) '0)
                                             (EQUAL (SUB1 B) '0)))))))
             ((ENABLE PLUS-RIGHT-ID2 COMMUTATIVITY-OF-PLUS
                      COMMUTATIVITY-OF-TIMES)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE TIMES-EQUAL-1)

(PROVE-LEMMA DIVIDES-IMPLIES-TIMES
             (REWRITE)
             (IMPLIES (AND (NOT (ZEROP A))
                           (AND (NUMBERP C)
                                (EQUAL (TIMES A C) B)))
                      (EQUAL (EQUAL C (QUOTIENT B A))
                             '*1*TRUE))
             ((ENABLE QUOTIENT-TIMES)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE DIVIDES-IMPLIES-TIMES)

(PROVE-LEMMA DIFFERENCE-1
             (REWRITE)
             (EQUAL (DIFFERENCE X '1) (SUB1 X))
             ((ENABLE DIFFERENCE-0)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE DIFFERENCE-1)

(PROVE-LEMMA DIFFERENCE-2
             (REWRITE)
             (EQUAL (DIFFERENCE (ADD1 (ADD1 X)) '2)
                    (FIX X))
             ((ENABLE DIFFERENCE-1)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE DIFFERENCE-2)

(PROVE-LEMMA HALF-PLUS
             (REWRITE)
             (EQUAL (QUOTIENT (PLUS X (PLUS X Y)) '2)
                    (PLUS X (QUOTIENT Y '2)))
             ((ENABLE PLUS-RIGHT-ID2 PLUS-ADD1 COMMUTATIVITY2-OF-PLUS
                      COMMUTATIVITY-OF-PLUS LESSP-REMAINDER2
                      REMAINDER-QUOTIENT-ELIM DIVIDES-IMPLIES-TIMES
                      DIFFERENCE-2)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE HALF-PLUS)

(PROVE-LEMMA TIMES-1
             (REWRITE)
             (EQUAL (TIMES '1 X) (FIX X))
             ((ENABLE TIMES-ZERO2)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE TIMES-1)

(PROVE-LEMMA EXP-OF-0
             (REWRITE)
             (EQUAL (EXP '0 K)
                    (IF (ZEROP K) '1 '0))
             ((ENABLE EXP)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE EXP-OF-0)

(PROVE-LEMMA EXP-OF-1
             (REWRITE)
             (EQUAL (EXP '1 K) '1)
             ((ENABLE EXP)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE EXP-OF-1)

(PROVE-LEMMA EXP-BY-0
             (REWRITE)
             (EQUAL (EXP X '0) '1)
             ((ENABLE EXP)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE EXP-BY-0)

(PROVE-LEMMA EXP-TIMES
             (REWRITE)
             (EQUAL (EXP (TIMES I J) K)
                    (TIMES (EXP I K) (EXP J K)))
             ((ENABLE COMMUTATIVITY2-OF-TIMES ASSOCIATIVITY-OF-TIMES EXP-BY-0
                      EXP)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE EXP-TIMES)

(PROVE-LEMMA EXP-EXP
             (REWRITE)
             (EQUAL (EXP (EXP I J) K)
                    (EXP I (TIMES J K)))
             ((ENABLE EXP-PLUS EXP-OF-1 EXP-BY-0 EXP-TIMES EXP)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE EXP-EXP)

(PROVE-LEMMA REMAINDER-PLUS-TIMES-1
             (REWRITE)
             (EQUAL (REMAINDER (PLUS X (TIMES I J)) J)
                    (REMAINDER X J))
             ((ENABLE COMMUTATIVITY2-OF-PLUS COMMUTATIVITY-OF-PLUS
                      ASSOCIATIVITY-OF-PLUS TIMES-ZERO2 COMMUTATIVITY-OF-TIMES
                      EQUAL-TIMES-0 REMAINDER-WRT-12 LESSP-REMAINDER2
                      REMAINDER-QUOTIENT-ELIM DIFFERENCE-PLUS1 DIVIDES-TIMES)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE REMAINDER-PLUS-TIMES-1)

(PROVE-LEMMA REMAINDER-PLUS-TIMES-2
             (REWRITE)
             (EQUAL (REMAINDER (PLUS X (TIMES J I)) J)
                    (REMAINDER X J))
             ((ENABLE COMMUTATIVITY-OF-TIMES REMAINDER-PLUS-TIMES-1)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE REMAINDER-PLUS-TIMES-2)

(PROVE-LEMMA REMAINDER-TIMES-1
             (REWRITE)
             (EQUAL (REMAINDER (TIMES B (TIMES A C)) A)
                    '0)
             ((ENABLE COMMUTATIVITY2-OF-TIMES REMAINDER-TIMES)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE REMAINDER-TIMES-1)

(PROVE-LEMMA REMAINDER-OF-1
             (REWRITE)
             (EQUAL (REMAINDER '1 X)
                    (IF (EQUAL X '1) '0 '1))
             ((ENABLE DIFFERENCE-0)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE REMAINDER-OF-1)

(PROVE-LEMMA REMAINDER-DIFFERENCE-TIMES
             (REWRITE)
             (EQUAL (REMAINDER (DIFFERENCE (TIMES P X) (TIMES P Y))
                               P)
                    '0)
             ((USE (DIVIDES-TIMES (X (DIFFERENCE X Y))
                                  (Z P)))
              (DISABLE DIVIDES-TIMES)
              (ENABLE COMMUTATIVITY-OF-TIMES TIMES-DIFFERENCE DIVIDES-TIMES
                      EUCLID REMAINDER-TIMES)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE REMAINDER-DIFFERENCE-TIMES)

(PROVE-LEMMA LESSP-REMAINDER-DIVISOR
             (REWRITE)
             (IMPLIES (NOT (ZEROP Y))
                      (LESSP (REMAINDER X Y) Y))
             ((ENABLE LESSP-REMAINDER2)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE LESSP-REMAINDER-DIVISOR)

(DEFTHEORY CL-ARITHMETIC
           (LESSP-REMAINDER-DIVISOR REMAINDER-DIFFERENCE-TIMES REMAINDER-OF-1
                                    REMAINDER-TIMES-1 REMAINDER-PLUS-TIMES-2
                                    REMAINDER-PLUS-TIMES-1 EXP-EXP EXP-TIMES
                                    EXP-BY-0 EXP-OF-1 EXP-OF-0 TIMES-1
                                    HALF-PLUS DIFFERENCE-2 DIFFERENCE-1
                                    DIVIDES-IMPLIES-TIMES TIMES-EQUAL-1
                                    IF-TIMES-THEN-DIVIDES
                                    DISTRIBUTIVITY-OF-DIVIDES QUOTIENT-TIMES
                                    REMAINDER-TIMES QUOTIENT-DIVIDES
                                    TIMES-IDENTITY TIMES-IDENTITY1
                                    DIVIDES-TIMES1 TIMES-ID-IFF-1
                                    QUOTIENT-LESSP QUOTIENT-TIMES1
                                    LESSP-PLUS-CANCELLATION3
                                    LESSP-TIMES-CANCELLATION EUCLID
                                    DIVIDES-PLUS-REWRITE-COMMUTED
                                    LESSP-PLUS-CANCELATION
                                    DIVIDES-PLUS-REWRITE DIVIDES-PLUS-REWRITE2
                                    DIVIDES-PLUS-REWRITE1 REMAINDER-ADD1
                                    DIFFERENCE-ADD1-CANCELLATION
                                    DIFFERENCE-PLUS3 DIVIDES-TIMES DIVIDES
                                    TIMES-DIFFERENCE
                                    DIFFERENCE-PLUS-CANCELATION
                                    DIFFERENCE-PLUS2 DIFFERENCE-PLUS1
                                    LESSP-REMAINDER1 LESSP-QUOTIENT1
                                    LESSP-TIMES-2 LESSP-TIMES-1
                                    REMAINDER-QUOTIENT-ELIM REMAINDER-X-X
                                    LESSP-REMAINDER2 REMAINDER-WRT-12
                                    REMAINDER-WRT-1 REMAINDER-QUOTIENT
                                    DIFFERENCE-ELIM EQUAL-LESSP EXP-PLUS
                                    EQUAL-TIMES-0 ASSOCIATIVITY-OF-TIMES
                                    COMMUTATIVITY2-OF-TIMES
                                    COMMUTATIVITY-OF-TIMES TIMES-ADD1
                                    DISTRIBUTIVITY-OF-TIMES-OVER-PLUS
                                    TIMES-ZERO2 DIFFERENCE-CANCELLATION-1
                                    DIFFERENCE-CANCELLATION-0
                                    EQUAL-DIFFERENCE-0 DIFFERENCE-0
                                    PLUS-CANCELLATION DIFFERENCE-PLUS
                                    DIFFERENCE-X-X PLUS-EQUAL-0
                                    ASSOCIATIVITY-OF-PLUS
                                    COMMUTATIVITY-OF-PLUS
                                    COMMUTATIVITY2-OF-PLUS PLUS-ADD1
                                    PLUS-RIGHT-ID2))

(DEFN NUMBER-AND-LIST-INDUCTION
      (N L)
      (IF (ZEROP N)
          '0
          (IF (LISTP L)
              (NUMBER-AND-LIST-INDUCTION (SUB1 N)
                                         (CDR L))
              '0))
      NIL)

(DEFN DOUBLE-NUMBER-INDUCTION
      (X Y)
      (IF (OR (ZEROP X) (ZEROP Y))
          '0
          (DOUBLE-NUMBER-INDUCTION (SUB1 X)
                                   (SUB1 Y)))
      NIL)

(DEFN DOUBLE-NUMBER-DOUBLE-LIST-INDUCTION
      (I J L1 L2)
      (IF (AND (LISTP L1) (LISTP L2))
          (IF (OR (ZEROP I) (ZEROP J))
              '0
              (DOUBLE-NUMBER-DOUBLE-LIST-INDUCTION (SUB1 I)
                                                   (SUB1 J)
                                                   (CDR L1)
                                                   (CDR L2)))
          '0)
      NIL)

(PROVE-LEMMA PLUS-0
             (REWRITE)
             (EQUAL (PLUS A '0) (FIX A))
             ((ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE PLUS-0)

(PROVE-LEMMA PLUS-1
             (REWRITE)
             (EQUAL (PLUS '1 X) (ADD1 X))
             ((ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE PLUS-1)

(PROVE-LEMMA PLUS-0-ARG1
             (REWRITE)
             (EQUAL (PLUS '0 X) (FIX X))
             ((ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE PLUS-0-ARG1)

(PROVE-LEMMA PLUS-DIFFERENCE-CANCELLATION
             (REWRITE)
             (IMPLIES (IF (LESSP B A) '*1*FALSE '*1*TRUE)
                      (EQUAL (PLUS A (DIFFERENCE B A))
                             (FIX B)))
             ((ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE PLUS-DIFFERENCE-CANCELLATION)

(PROVE-LEMMA CANONICALIZE-PLUS-TERMS1
             (REWRITE)
             (EQUAL (ADD1 (PLUS (ADD1 A) B))
                    (PLUS (ADD1 (ADD1 A)) B))
             ((ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE CANONICALIZE-PLUS-TERMS1)

(PROVE-LEMMA CANONICALIZE-PLUS-TERMS2
             (REWRITE)
             (EQUAL (PLUS (ADD1 A) (PLUS (ADD1 B) C))
                    (PLUS (PLUS (ADD1 A) (ADD1 B)) C))
             ((ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE CANONICALIZE-PLUS-TERMS2)

(PROVE-LEMMA CANONICALIZE-PLUS-TERMS3
             (REWRITE)
             (EQUAL (PLUS (TIMES A B) (PLUS (ADD1 C) D))
                    (PLUS (ADD1 C) (PLUS D (TIMES A B))))
             ((ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE CANONICALIZE-PLUS-TERMS3)

(PROVE-LEMMA PLUS-PLUS-DIFFERENCE
             (REWRITE)
             (IMPLIES (AND (NUMBERP I)
                           (AND (NUMBERP N)
                                (IF (LESSP N I)
                                    '*1*FALSE
                                    '*1*TRUE)))
                      (EQUAL (PLUS I (PLUS J (DIFFERENCE N I)))
                             (PLUS N J)))
             ((ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE PLUS-PLUS-DIFFERENCE)

(PROVE-LEMMA PLUS-TIMES-REDUCTION
             (REWRITE)
             (EQUAL (PLUS A (TIMES B A))
                    (TIMES (ADD1 B) A))
             ((ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE PLUS-TIMES-REDUCTION)

(PROVE-LEMMA PLUS-TIMES-SUB1-REDUCTION
             (REWRITE)
             (IMPLIES (NOT (ZEROP B))
                      (EQUAL (PLUS A (TIMES (SUB1 B) A))
                             (TIMES B A)))
             ((ENABLE PLUS-TIMES-REDUCTION)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE PLUS-TIMES-SUB1-REDUCTION)

(PROVE-LEMMA PLUS-COMMUTATIVITY-ASSOCIATIVITY-CROCK
             (REWRITE)
             (EQUAL (PLUS B (PLUS A C))
                    (PLUS A (PLUS B C)))
             ((ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE PLUS-COMMUTATIVITY-ASSOCIATIVITY-CROCK)

(PROVE-LEMMA DISTRIBUTIVITY-OF-TIMES-OVER-PLUS-BACKWARDS
             (REWRITE)
             (EQUAL (PLUS (TIMES A B) (TIMES A C))
                    (TIMES A (PLUS B C)))
             ((ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE DISTRIBUTIVITY-OF-TIMES-OVER-PLUS-BACKWARDS)

(PROVE-LEMMA DIFFERENCE-IS-ZERO
             (REWRITE)
             (IMPLIES (LESSP A B)
                      (EQUAL (DIFFERENCE A B) '0))
             ((ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE DIFFERENCE-IS-ZERO)

(PROVE-LEMMA DIFFERENCE-BY-LARGER-NUMBER
             (REWRITE)
             (EQUAL (DIFFERENCE (SUB1 X) X) '0)
             ((ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE DIFFERENCE-BY-LARGER-NUMBER)

(PROVE-LEMMA DIFFERENCE-ADD1-ARG1
             (REWRITE)
             (IMPLIES (IF (LESSP A B) '*1*FALSE '*1*TRUE)
                      (EQUAL (DIFFERENCE (ADD1 A) B)
                             (ADD1 (DIFFERENCE A B))))
             ((ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE DIFFERENCE-ADD1-ARG1)

(PROVE-LEMMA DIFFERENCE-ADD1-ARG2
             (REWRITE)
             (IMPLIES (LESSP B A)
                      (EQUAL (DIFFERENCE A (ADD1 B))
                             (SUB1 (DIFFERENCE A B))))
             ((ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE DIFFERENCE-ADD1-ARG2)

(PROVE-LEMMA SUB1-DIFFERENCE
             (REWRITE)
             (EQUAL (SUB1 (DIFFERENCE A B))
                    (DIFFERENCE (SUB1 A) B))
             ((INDUCT (DOUBLE-NUMBER-INDUCTION A B))
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE SUB1-DIFFERENCE)

(PROVE-LEMMA DIFFERENCE-SUB1-ARG1
             (REWRITE)
             (IMPLIES (LESSP B A)
                      (EQUAL (DIFFERENCE (SUB1 A) B)
                             (SUB1 (DIFFERENCE A B))))
             ((ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE DIFFERENCE-SUB1-ARG1)

(PROVE-LEMMA DIFFERENCE-SUB1-ARG2
             (REWRITE)
             (IMPLIES (AND (NOT (ZEROP B))
                           (IF (LESSP A B) '*1*FALSE '*1*TRUE))
                      (EQUAL (DIFFERENCE A (SUB1 B))
                             (ADD1 (DIFFERENCE A B))))
             ((ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE DIFFERENCE-SUB1-ARG2)

(PROVE-LEMMA DIFFERENCE-PLUS-CANCELLATION2-INSTANCE
             (REWRITE)
             (IMPLIES (IF (LESSP A C) '*1*FALSE '*1*TRUE)
                      (EQUAL (DIFFERENCE (PLUS (ADD1 A) B)
                                         (ADD1 C))
                             (PLUS (DIFFERENCE A C) B)))
             ((ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE DIFFERENCE-PLUS-CANCELLATION2-INSTANCE)

(PROVE-LEMMA DIFFERENCE-DIFFERENCE
             (REWRITE)
             (EQUAL (DIFFERENCE (DIFFERENCE A B) C)
                    (DIFFERENCE A (PLUS B C)))
             ((ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE DIFFERENCE-DIFFERENCE)

(PROVE-LEMMA YET-ANOTHER-DIFFERENCE-PLUS-CROCK
             (REWRITE)
             (EQUAL (DIFFERENCE (PLUS N (PLUS B A)) A)
                    (PLUS N B))
             ((ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE YET-ANOTHER-DIFFERENCE-PLUS-CROCK)

(PROVE-LEMMA NON-ZERO-DIFFERENCE
             (REWRITE)
             (IMPLIES (AND (NUMBERP A) (LESSP A B))
                      (NOT (EQUAL (DIFFERENCE B A) '0)))
             ((ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE NON-ZERO-DIFFERENCE)

(PROVE-LEMMA REWRITE-NON-ZERO-DIFFERENCE-AS-LESSP
             (REWRITE)
             (EQUAL (NOT (EQUAL (DIFFERENCE A B) '0))
                    (LESSP B A))
             ((ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE REWRITE-NON-ZERO-DIFFERENCE-AS-LESSP)

(PROVE-LEMMA REWRITE-ZERO-DIFFERENCE-AS-EQUALITY
             (REWRITE)
             (IMPLIES (IF (LESSP A B) '*1*FALSE '*1*TRUE)
                      (EQUAL (EQUAL (DIFFERENCE A B) '0)
                             (EQUAL (FIX A) (FIX B))))
             ((ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE REWRITE-ZERO-DIFFERENCE-AS-EQUALITY)

(PROVE-LEMMA REGROUP-FACT
             (REWRITE)
             (IMPLIES (AND (IF (LESSP A C) '*1*FALSE '*1*TRUE)
                           (IF (LESSP B D) '*1*FALSE '*1*TRUE))
                      (EQUAL (DIFFERENCE (PLUS A B) (PLUS C D))
                             (PLUS (DIFFERENCE A C)
                                   (DIFFERENCE B D))))
             ((ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE REGROUP-FACT)

(PROVE-LEMMA DIFFERENCE-EQUALS-0
             (REWRITE)
             (IMPLIES (AND (NUMBERP A)
                           (AND (NUMBERP B)
                                (IF (LESSP A B)
                                    '*1*FALSE
                                    '*1*TRUE)))
                      (EQUAL (EQUAL (DIFFERENCE A B) '0)
                             (EQUAL A B)))
             ((ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE DIFFERENCE-EQUALS-0)

(PROVE-LEMMA TIMES-ZERO3
             (REWRITE)
             (EQUAL (TIMES X '0) '0)
             ((ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE TIMES-ZERO3)

(PROVE-LEMMA DISTRIBUTIVITY-OF-TIMES-OVER-DIFFERENCE
             (REWRITE)
             (EQUAL (DIFFERENCE (TIMES A B) (TIMES A C))
                    (TIMES A (DIFFERENCE B C)))
             ((ENABLE TIMES-DIFFERENCE COMMUTATIVITY-OF-TIMES)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE DISTRIBUTIVITY-OF-TIMES-OVER-DIFFERENCE)

(PROVE-LEMMA EXP-2-NEVER-0
             (REWRITE)
             (EQUAL (LESSP '0 (EXP '2 I))
                    '*1*TRUE)
             ((ENABLE EXP)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE EXP-2-NEVER-0)

(PROVE-LEMMA EXP-2-NEVER-0-LINEAR
             (REWRITE)
             (LESSP '0 (EXP '2 I))
             ((ENABLE EXP-2-NEVER-0)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE EXP-2-NEVER-0-LINEAR)

(PROVE-LEMMA REMAINDER-NOOP
             (REWRITE)
             (IMPLIES (AND (NUMBERP A)
                           (AND (LESSP A B) (NOT (ZEROP B))))
                      (EQUAL (REMAINDER A B) A))
             ((ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE REMAINDER-NOOP)

(PROVE-LEMMA REMAINDER-ADD1-CASESPLIT
             (REWRITE)
             (IMPLIES (LESSP A B)
                      (EQUAL (REMAINDER (ADD1 A) B)
                             (IF (EQUAL (ADD1 A) B) '0 (ADD1 A))))
             ((ENABLE REMAINDER REMAINDER-NOOP)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE REMAINDER-ADD1-CASESPLIT)

(PROVE-LEMMA ZEROP-REMAINDER-DIFFERENCE
             (REWRITE)
             (IMPLIES (EQUAL (REMAINDER A B) '0)
                      (EQUAL (REMAINDER (DIFFERENCE A B) B)
                             '0))
             ((ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE ZEROP-REMAINDER-DIFFERENCE)

(PROVE-LEMMA QUOTIENT-X-X
             (REWRITE)
             (IMPLIES (NOT (ZEROP X))
                      (EQUAL (QUOTIENT X X) '1))
             ((ENABLE DIFFERENCE-X-X)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE QUOTIENT-X-X)

(PROVE-LEMMA REMAINDER-TIMES-OTHER-WAY
             (REWRITE)
             (EQUAL (REMAINDER (TIMES B A) A) '0)
             ((ENABLE REMAINDER-TIMES COMMUTATIVITY-OF-TIMES)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE REMAINDER-TIMES-OTHER-WAY)

(PROVE-LEMMA QUOTIENT-TIMES-OTHER-WAY
             (REWRITE)
             (EQUAL (QUOTIENT (TIMES B A) A)
                    (IF (ZEROP A) '0 (FIX B)))
             ((ENABLE QUOTIENT-TIMES COMMUTATIVITY-OF-TIMES)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE QUOTIENT-TIMES-OTHER-WAY)

(PROVE-LEMMA QUOTIENT-DIFFERENCE
             (REWRITE)
             (IMPLIES (NOT (LESSP I J))
                      (EQUAL (QUOTIENT (DIFFERENCE I J) J)
                             (SUB1 (QUOTIENT I J))))
             ((ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE QUOTIENT-DIFFERENCE)

(PROVE-LEMMA QUOTIENT-PLUS
             (REWRITE)
             (IMPLIES (NOT (ZEROP A))
                      (EQUAL (QUOTIENT (PLUS A B) A)
                             (ADD1 (QUOTIENT B A))))
             ((EXPAND (QUOTIENT (PLUS A B) A))
              (ENABLE DIFFERENCE-PLUS)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE QUOTIENT-PLUS)

(PROVE-LEMMA QUOTIENT-PLUS-TIMES
             (REWRITE)
             (IMPLIES (LESSP C B)
                      (EQUAL (QUOTIENT (PLUS C (TIMES B A)) B)
                             (FIX A)))
             ((ENABLE PLUS-0 COMMUTATIVITY2-OF-PLUS COMMUTATIVITY-OF-TIMES
                      QUOTIENT-PLUS)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE QUOTIENT-PLUS-TIMES)

(PROVE-LEMMA LEQ-TIMES
             NIL
             (IMPLIES (AND (NOT (ZEROP A))
                           (IF (LESSP C B) '*1*FALSE '*1*TRUE))
                      (IF (LESSP (TIMES A C) (TIMES A B))
                          '*1*FALSE
                          '*1*TRUE))
             ((ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(PROVE-LEMMA LESSP-REMAINDER-SUB1-CROCK NIL
             (IMPLIES (LESSP X N)
                      (LESSP (SUB1 X) N))
             ((ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(PROVE-LEMMA LEQ-PLUS NIL
             (IMPLIES (IF (LESSP C (PLUS A B))
                          '*1*FALSE
                          '*1*TRUE)
                      (IF (LESSP C A) '*1*FALSE '*1*TRUE))
             ((ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(PROVE-LEMMA LEQ-PLUS1 NIL
             (IMPLIES (IF (LESSP C (PLUS A B))
                          '*1*FALSE
                          '*1*TRUE)
                      (AND (IF (LESSP C A) '*1*FALSE '*1*TRUE)
                           (IF (LESSP C B)
                               '*1*FALSE
                               '*1*TRUE)))
             ((ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(PROVE-LEMMA LEQ-PLUS2 NIL
             (IMPLIES (IF (LESSP C (PLUS A B))
                          '*1*FALSE
                          '*1*TRUE)
                      (EQUAL (LESSP C A) '*1*FALSE))
             ((ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(PROVE-LEMMA LEQ-CASESPLIT NIL
             (IMPLIES (AND (NUMBERP A) (NUMBERP B))
                      (EQUAL (IF (LESSP B A) '*1*FALSE '*1*TRUE)
                             (OR (LESSP A B) (EQUAL A B))))
             ((ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(PROVE-LEMMA INTEGER-INEQUALITY-CASESPLIT NIL
             (IMPLIES (AND (NUMBERP I) (NUMBERP J))
                      (EQUAL (NOT (EQUAL I J))
                             (OR (LESSP I J) (LESSP J I))))
             ((ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(PROVE-LEMMA INTEGER-EQUALITY-CROCK NIL
             (IMPLIES (AND (NUMBERP A)
                           (AND (NUMBERP B)
                                (AND (LESSP A '1) (LESSP B '1))))
                      (EQUAL A B))
             ((ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(PROVE-LEMMA LESSP-REMAINDER-REMAINDER
             (REWRITE)
             (IMPLIES (AND (NOT (ZEROP C))
                           (NOT (ZEROP (REMAINDER B C))))
                      (EQUAL (LESSP (REMAINDER A (REMAINDER B C))
                                    C)
                             '*1*TRUE))
             ((ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE LESSP-REMAINDER-REMAINDER)

(PROVE-LEMMA LESSP-TIMES
             (REWRITE)
             (IMPLIES (AND (NOT (ZEROP A)) (LESSP B C))
                      (LESSP (TIMES A B) (TIMES A C)))
             ((ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE LESSP-TIMES)

(PROVE-LEMMA LEQ-PLUS-TIMES
             NIL
             (IMPLIES (AND (LESSP B C) (NOT (ZEROP A)))
                      (IF (LESSP (TIMES A C)
                                 (PLUS A (TIMES A B)))
                          '*1*FALSE
                          '*1*TRUE))
             ((ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(PROVE-LEMMA LESSP-DIFFERENCE NIL
             (IMPLIES (AND (NOT (ZEROP A)) (LESSP A B))
                      (LESSP (DIFFERENCE B A) B))
             ((ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(PROVE-LEMMA REMAINDER-DIFFERENCE-NON-ZERO
             (REWRITE)
             (IMPLIES (AND (NOT (ZEROP A))
                           (AND (NUMBERP B) (LESSP A B)))
                      (NOT (ZEROP (REMAINDER (DIFFERENCE B A) B))))
             ((ENABLE REMAINDER-NOOP)
              (DISABLE REMAINDER DIFFERENCE)
              (USE (LESSP-DIFFERENCE (A A) (B B)))
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE REMAINDER-DIFFERENCE-NON-ZERO)

(PROVE-LEMMA SUM-ZERO-IMPLIES-ADDENDS-ZERO
             NIL
             (IMPLIES (EQUAL (PLUS A B) '0)
                      (AND (ZEROP A) (ZEROP B)))
             ((ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(PROVE-LEMMA REMAINDER-ZERO-IMPLIES-LEQ-FACT
             (REWRITE)
             (IMPLIES (AND (EQUAL (REMAINDER A B) '0)
                           (NOT (ZEROP A)))
                      (EQUAL (LESSP A B) '*1*FALSE))
             ((ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE REMAINDER-ZERO-IMPLIES-LEQ-FACT)

(DEFN LESSP-QUOTIENT-INDUCTION
      (A B C)
      (IF (ZEROP B)
          '0
          (IF (ZEROP C)
              '0
              (IF (LESSP A C)
                  '0
                  (LESSP-QUOTIENT-INDUCTION (DIFFERENCE A C)
                                            (SUB1 B)
                                            C))))
      NIL)

(PROVE-LEMMA LESSP-QUOTIENT-REMAINDER-CROCK
             (REWRITE)
             (IMPLIES (AND (LESSP A (TIMES B C))
                           (AND (NOT (EQUAL B '0))
                                (AND (NUMBERP B)
                                     (AND (NOT (EQUAL C '0))
                                          (AND (NUMBERP C) (NUMBERP A))))))
                      (LESSP (QUOTIENT A C) B))
             ((INDUCT (LESSP-QUOTIENT-INDUCTION A B C))
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE LESSP-QUOTIENT-REMAINDER-CROCK)

(PROVE-LEMMA LESSP-QUOTIENT-REMAINDER
             (REWRITE)
             (IMPLIES (AND (NOT (ZEROP B)) (NOT (ZEROP C)))
                      (LESSP (QUOTIENT (REMAINDER A (TIMES B C)) C)
                             (FIX B)))
             ((ENABLE DIVIDES LESSP-REMAINDER2 LESSP-QUOTIENT-REMAINDER-CROCK
                      EQUAL-TIMES-0 REWRITE-ZERO-DIFFERENCE-AS-EQUALITY
                      QUOTIENT-X-X)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE LESSP-QUOTIENT-REMAINDER)

(PROVE-LEMMA LESSP-QUOTIENT-TIMES
             (REWRITE)
             (IMPLIES (LESSP A (TIMES B C))
                      (EQUAL (LESSP (QUOTIENT A C) B)
                             '*1*TRUE))
             ((INDUCT (LESSP-QUOTIENT-INDUCTION A B C))
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE LESSP-QUOTIENT-TIMES)

(DEFN MIN
      (A B)
      (IF (LESSP A B) A B)
      NIL)

(PROVE-LEMMA LESSP-TRANSITIVITY NIL
             (IMPLIES (AND (LESSP A B) (LESSP B C))
                      (LESSP A C))
             ((ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(PROVE-LEMMA REMAINDER-PLUS
             (REWRITE)
             (EQUAL (REMAINDER (PLUS A N) A)
                    (REMAINDER N A))
             ((ENABLE REMAINDER-WRT-12 PLUS-RIGHT-ID2 DIFFERENCE-PLUS1)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE REMAINDER-PLUS)

(PROVE-LEMMA REMAINDER-DIVIDES
             (REWRITE)
             (IMPLIES (AND (DIVIDES A U) (NUMBERP U))
                      (EQUAL (REMAINDER (PLUS U N) A)
                             (REMAINDER N A)))
             ((USE (QUOTIENT-DIVIDES (X A) (Y U)))
              (DISABLE REMAINDER PLUS TIMES)
              (ENABLE REMAINDER-PLUS-TIMES-2 PLUS-RIGHT-ID2 TIMES-ZERO2
                      COMMUTATIVITY-OF-TIMES REMAINDER-WRT-12 REMAINDER-PLUS
                      LESSP-REMAINDER2 REMAINDER-QUOTIENT-ELIM DIVIDES-TIMES1
                      COMMUTATIVITY-OF-PLUS DIVIDES)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE REMAINDER-DIVIDES)

(PROVE-LEMMA REMAINDER-REMAINDER
             (REWRITE)
             (IMPLIES (DIVIDES A B)
                      (EQUAL (REMAINDER (REMAINDER N B) A)
                             (REMAINDER N A)))
             ((INDUCT (REMAINDER N B))
              (DISABLE DIVIDES)
              (ENABLE ASSOCIATIVITY-OF-PLUS REMAINDER-DIVIDES DIFFERENCE-ELIM
                      LESSP-REMAINDER2 REMAINDER-QUOTIENT-ELIM
                      REMAINDER-WRT-12)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE REMAINDER-REMAINDER)

(PROVE-LEMMA LESSP-QUOTIENT
             NIL
             (IMPLIES (LESSP N (TIMES A B))
                      (LESSP (QUOTIENT N A) B))
             ((INDUCT (LESSP-QUOTIENT-INDUCTION N B A))
              (ENABLE TIMES-ADD1 TIMES-ZERO2 TIMES-ZERO3)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DEFN LESSP-QUOTIENT-QUOTIENT-INDUCTION
      (N A B)
      (IF (ZEROP N)
          '0
          (IF (LESSP A N)
              '0
              (IF (LESSP B N)
                  '0
                  (LESSP-QUOTIENT-QUOTIENT-INDUCTION N
                                                     (DIFFERENCE A N)
                                                     (DIFFERENCE B N)))))
      NIL)

(PROVE-LEMMA LESSP-QUOTIENT-QUOTIENT
             (REWRITE)
             (IMPLIES (AND (NOT (ZEROP N))
                           (AND (EQUAL (REMAINDER B N) '0)
                                (LESSP A B)))
                      (EQUAL (LESSP (QUOTIENT A N) (QUOTIENT B N))
                             '*1*TRUE))
             ((ENABLE REMAINDER-QUOTIENT-ELIM LESSP-REMAINDER2
                      COMMUTATIVITY-OF-TIMES)
              (INDUCT (LESSP-QUOTIENT-QUOTIENT-INDUCTION N A B))
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE LESSP-QUOTIENT-QUOTIENT)

(PROVE-LEMMA LESSP-TIMES-QUOTIENT
             (REWRITE)
             (IMPLIES (AND (NOT (ZEROP N))
                           (AND (NUMBERP I)
                                (AND (LESSP I J)
                                     (EQUAL (REMAINDER J N) '0))))
                      (EQUAL (LESSP (TIMES N (QUOTIENT I N)) J)
                             '*1*TRUE))
             ((USE (LESSP-QUOTIENT-QUOTIENT (A I)
                                            (B J)
                                            (N N))
                   (QUOTIENT-TIMES1 (X N) (Y J)))
              (ENABLE DIVIDES LESSP-TIMES)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE LESSP-TIMES-QUOTIENT)

(PROVE-LEMMA NOT-LESSP-TIMES-PLUS
             NIL
             (IMPLIES (AND (NUMBERP A)
                           (AND (NUMBERP V)
                                (AND (LESSP V N)
                                     (AND (NUMBERP B)
                                          (AND (NOT (EQUAL N '0))
                                               (AND (NUMBERP N)
                                                    (LESSP (PLUS V (TIMES A N))
                                                           (TIMES B N))))))))
                      (NOT (LESSP (TIMES B N)
                                  (PLUS (TIMES A N) N))))
             ((INDUCT (DOUBLE-NUMBER-INDUCTION A B))
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(PROVE-LEMMA NOT-LESSP-TIMES-PLUS-INSTANCE
      (REWRITE)
      (IMPLIES (AND (NUMBERP X)
                    (AND (NUMBERP V)
                         (AND (LESSP V N)
                              (AND (NUMBERP Z)
                                   (AND (NOT (EQUAL N '0))
                                        (AND (NUMBERP N)
                                             (LESSP (TIMES N Z)
                                                    (PLUS N (TIMES N X)))))))))
               (EQUAL (LESSP (PLUS V (TIMES N X))
                             (TIMES N Z))
                      '*1*FALSE))
      ((USE (NOT-LESSP-TIMES-PLUS (A X) (B Z)))
       (ENABLE COMMUTATIVITY-OF-TIMES COMMUTATIVITY-OF-PLUS)
       (ENABLE-THEORY GROUND-ZERO)
       (DISABLE-THEORY T)))

(DISABLE NOT-LESSP-TIMES-PLUS-INSTANCE)

(PROVE-LEMMA NOT-LESSP-PLUS-TIMES-QUOTIENT
             (REWRITE)
             (IMPLIES (AND (NOT (ZEROP N))
                           (AND (NUMBERP I)
                                (AND (LESSP I J)
                                     (EQUAL (REMAINDER J N) '0))))
                      (EQUAL (LESSP J
                                    (PLUS (TIMES N (QUOTIENT I N)) N))
                             '*1*FALSE))
             ((ENABLE-THEORY CL-ARITHMETIC GROUND-ZERO)
              (ENABLE NOT-LESSP-TIMES-PLUS-INSTANCE)
              (DISABLE-THEORY T)))

(DISABLE NOT-LESSP-PLUS-TIMES-QUOTIENT)

(PROVE-LEMMA QUOTIENT-PLUS-TIMES-REMAINDER
             (REWRITE)
             (IMPLIES (NOT (ZEROP N))
                      (EQUAL (QUOTIENT (PLUS (TIMES N A) (REMAINDER B N))
                                       N)
                             (FIX A)))
             ((USE (QUOTIENT-PLUS-TIMES (A A)
                                        (B N)
                                        (C (REMAINDER B N))))
              (ENABLE COMMUTATIVITY-OF-PLUS LESSP-REMAINDER2)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE QUOTIENT-PLUS-TIMES-REMAINDER)

(PROVE-LEMMA REMAINDER-PLUS-TIMES-REMAINDER
             (REWRITE)
             (EQUAL (REMAINDER (PLUS (TIMES N A) (REMAINDER B N))
                               N)
                    (REMAINDER B N))
             ((USE (REMAINDER-PLUS-TIMES-2 (J N)
                                           (I A)
                                           (X (REMAINDER B N))))
              (ENABLE COMMUTATIVITY-OF-PLUS REMAINDER-REMAINDER DIVIDES
                      REMAINDER-X-X)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE REMAINDER-PLUS-TIMES-REMAINDER)

(PROVE-LEMMA REMAINDER-NON-ZERO
             NIL
             (IMPLIES (AND (NOT (ZEROP N)) (LESSP N M))
                      (LESSP '0 (REMAINDER N M)))
             ((ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(PROVE-LEMMA PLUS-NOT-EQUAL
             (REWRITE)
             (IMPLIES (NOT (EQUAL (FIX B) (FIX C)))
                      (NOT (EQUAL (PLUS A B) (PLUS A C))))
             ((ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE PLUS-NOT-EQUAL)

(PROVE-LEMMA DIFFERENCE-PLUS4
             (REWRITE)
             (EQUAL (DIFFERENCE (PLUS A (PLUS B C))
                                (PLUS B C))
                    (FIX A))
             ((USE (DIFFERENCE-PLUS (Y A)
                                    (X (PLUS B C))))
              (ENABLE ASSOCIATIVITY-OF-PLUS)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE DIFFERENCE-PLUS4)

(PROVE-LEMMA REMAINDER-REMAINDER-INVERSE
             NIL
             (IMPLIES (DIVIDES A B)
                      (EQUAL (REMAINDER N A)
                             (REMAINDER (REMAINDER N B) A)))
             ((ENABLE REMAINDER-REMAINDER)
              (DISABLE REMAINDER)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(PROVE-LEMMA ASSOCIATIVITY-OF-PLUS-INVERSE
             NIL
             (EQUAL (PLUS A (PLUS B C))
                    (PLUS (PLUS A B) C))
             ((ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DEFN LENGTH
      (L)
      (IF (LISTP L)
          (ADD1 (LENGTH (CDR L)))
          '0)
      NIL)

(DEFN INSERT
      (I L)
      (IF (LISTP L)
          (IF (LESSP I (CAR L))
              (CONS I L)
              (CONS (CAR L) (INSERT I (CDR L))))
          (CONS I L))
      NIL)

(DEFN OCCURRENCES
      (X L)
      (IF (LISTP L)
          (IF (EQUAL X (CAR L))
              (ADD1 (OCCURRENCES X (CDR L)))
              (OCCURRENCES X (CDR L)))
          '0)
      NIL)

(DEFN REMOVE
      (X L)
      (IF (LISTP L)
          (IF (EQUAL X (CAR L))
              (CDR L)
              (CONS (CAR L) (REMOVE X (CDR L))))
          L)
      NIL)

(DEFN PERMUTATION
      (A B)
      (IF (LISTP A)
          (AND (MEMBER (CAR A) B)
               (PERMUTATION (CDR A)
                            (REMOVE (CAR A) B)))
          (NLISTP B))
      NIL)

(DEFN PLISTP
      (L)
      (IF (LISTP L)
          (PLISTP (CDR L))
          (EQUAL L 'NIL))
      NIL)

(DEFN SETP
      (L)
      (IF (LISTP L)
          (AND (NOT (MEMBER (CAR L) (CDR L)))
               (SETP (CDR L)))
          (EQUAL L 'NIL))
      NIL)

(DEFN SORTED
      (L)
      (IF (LISTP L)
          (IF (LISTP (CDR L))
              (IF (LESSP (CAR (CDR L)) (CAR L))
                  '*1*FALSE
                  (SORTED (CDR L)))
              '*1*TRUE)
          '*1*TRUE)
      NIL)

(PROVE-LEMMA NOT-LISTP-REMOVE
             (REWRITE)
             (IMPLIES (NOT (LISTP L))
                      (NOT (LISTP (REMOVE X (CONS X L)))))
             ((ENABLE REMOVE)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE NOT-LISTP-REMOVE)

(PROVE-LEMMA LENGTH-INSERT
             (REWRITE)
             (EQUAL (LENGTH (INSERT I L))
                    (ADD1 (LENGTH L)))
             ((ENABLE INSERT LENGTH)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE LENGTH-INSERT)

(PROVE-LEMMA LENGTH-REMOVE
             (REWRITE)
             (EQUAL (LENGTH (REMOVE X L))
                    (IF (MEMBER X L)
                        (SUB1 (LENGTH L))
                        (LENGTH L)))
             ((ENABLE REMOVE MEMBER LENGTH)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE LENGTH-REMOVE)

(PROVE-LEMMA LENGTH-PERMUTATION
             NIL
             (IMPLIES (PERMUTATION A B)
                      (EQUAL (LENGTH A) (LENGTH B)))
             ((ENABLE PERMUTATION LENGTH LENGTH-REMOVE)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(PROVE-LEMMA NUMBER-OF-OCCURRENCES-OF-SET-MEMBER-IS-1
             NIL
             (IMPLIES (AND (SETP L) (MEMBER X L))
                      (EQUAL (OCCURRENCES X L) '1))
             ((ENABLE SETP MEMBER OCCURRENCES)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(PROVE-LEMMA PLISTP-REMOVE
             (REWRITE)
             (EQUAL (PLISTP (REMOVE X L))
                    (PLISTP L))
             ((ENABLE PLISTP REMOVE)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE PLISTP-REMOVE)

(PROVE-LEMMA PLISTP-SET
             (REWRITE)
             (IMPLIES (SETP L) (PLISTP L))
             ((ENABLE SETP PLISTP)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE PLISTP-SET)

(PROVE-LEMMA INSERT-REMOVE
             (REWRITE)
             (IMPLIES (AND (SORTED L) (NOT (EQUAL X Y)))
                      (EQUAL (INSERT X (REMOVE Y L))
                             (REMOVE Y (INSERT X L))))
             ((ENABLE INSERT REMOVE SORTED)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE INSERT-REMOVE)

(PROVE-LEMMA MEMBER-INSERT
             (REWRITE)
             (IMPLIES (MEMBER X L)
                      (MEMBER X (INSERT I L)))
             ((ENABLE MEMBER INSERT)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE MEMBER-INSERT)

(PROVE-LEMMA NOT-MEMBER-INSERT
             (REWRITE)
             (IMPLIES (AND (NOT (MEMBER X L))
                           (NOT (EQUAL I X)))
                      (NOT (MEMBER X (INSERT I L))))
             ((ENABLE MEMBER INSERT)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE NOT-MEMBER-INSERT)

(PROVE-LEMMA MEMBER-REMOVE1
             NIL
             (IMPLIES (MEMBER X (REMOVE Y L))
                      (MEMBER X L))
             ((ENABLE MEMBER REMOVE)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(PROVE-LEMMA MEMBER-REMOVE2
             (REWRITE)
             (IMPLIES (AND (MEMBER X L) (NOT (EQUAL X Y)))
                      (MEMBER X (REMOVE Y L)))
             ((ENABLE MEMBER REMOVE)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE MEMBER-REMOVE2)

(PROVE-LEMMA NOT-MEMBER-REMOVE1
             (REWRITE)
             (IMPLIES (SETP L)
                      (NOT (MEMBER X (REMOVE X L))))
             ((ENABLE SETP MEMBER REMOVE)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE NOT-MEMBER-REMOVE1)

(PROVE-LEMMA NOT-MEMBER-REMOVE2
             (REWRITE)
             (IMPLIES (NOT (MEMBER X L))
                      (NOT (MEMBER X (REMOVE Y L))))
             ((ENABLE MEMBER REMOVE)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE NOT-MEMBER-REMOVE2)

(PROVE-LEMMA NOT-MEMBER-PERMUTATION
             NIL
             (IMPLIES (AND (PERMUTATION A B)
                           (NOT (MEMBER X B)))
                      (NOT (MEMBER X A)))
             ((ENABLE PERMUTATION MEMBER NOT-MEMBER-REMOVE2)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(PROVE-LEMMA MEMBER-PERMUTATION NIL
             (IMPLIES (AND (PERMUTATION A B) (MEMBER X B))
                      (MEMBER X A))
             ((ENABLE PERMUTATION MEMBER MEMBER-REMOVE2)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(PROVE-LEMMA REMOVE-REMOVE
             (REWRITE)
             (IMPLIES (NOT (EQUAL X Y))
                      (EQUAL (REMOVE Y (REMOVE X L))
                             (REMOVE X (REMOVE Y L))))
             ((ENABLE REMOVE)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE REMOVE-REMOVE)

(PROVE-LEMMA SORTED-INSERT
             (REWRITE)
             (IMPLIES (AND (SORTED L) (NOT (MEMBER I L)))
                      (SORTED (INSERT I L)))
             ((ENABLE SORTED INSERT MEMBER)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE SORTED-INSERT)

(PROVE-LEMMA SORTED-REMOVE
             (REWRITE)
             (IMPLIES (SORTED L)
                      (SORTED (REMOVE X L)))
             ((ENABLE SORTED REMOVE)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE SORTED-REMOVE)

(PROVE-LEMMA NOT-PERMUTATION
             (REWRITE)
             (IMPLIES (AND (LISTP B)
                           (NOT (MEMBER (CAR B) A)))
                      (NOT (PERMUTATION A B)))
             ((ENABLE PERMUTATION MEMBER REMOVE)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE NOT-PERMUTATION)

(PROVE-LEMMA PERMUTATION-RIGHT-CONS1
             (REWRITE)
             (IMPLIES (AND (LISTP B) (MEMBER (CAR B) A))
                      (EQUAL (PERMUTATION A B)
                             (PERMUTATION (REMOVE (CAR B) A)
                                          (CDR B))))
             ((ENABLE PERMUTATION MEMBER REMOVE)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE PERMUTATION-RIGHT-CONS1)

(PROVE-LEMMA PERMUTATION-RIGHT-CONS
             (REWRITE)
             (EQUAL (PERMUTATION A (CONS X B))
                    (IF (MEMBER X A)
                        (PERMUTATION (REMOVE X A) B)
                        '*1*FALSE))
             ((ENABLE NOT-PERMUTATION PERMUTATION-RIGHT-CONS1)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE PERMUTATION-RIGHT-CONS)

(PROVE-LEMMA COMMUTATIVITY-OF-PERMUTATION
             (REWRITE)
             (EQUAL (PERMUTATION B A)
                    (PERMUTATION A B))
             ((ENABLE PERMUTATION PERMUTATION-RIGHT-CONS)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE COMMUTATIVITY-OF-PERMUTATION)

(PROVE-LEMMA MEMBER-PERMUTATION2
             NIL
             (IMPLIES (AND (PERMUTATION B A) (MEMBER X B))
                      (MEMBER X A))
             ((USE (COMMUTATIVITY-OF-PERMUTATION (A A)
                                                 (B B))
                   (MEMBER-PERMUTATION (X X)
                                       (A A)
                                       (B B)))
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(PROVE-LEMMA PERMUTATION-REFLEXIVITY
             (REWRITE)
             (PERMUTATION L L)
             ((ENABLE PERMUTATION REMOVE)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE PERMUTATION-REFLEXIVITY)

(PROVE-LEMMA PERMUTATION-APPEND-CAR
             (REWRITE)
             (PERMUTATION (APPEND L (CONS X 'NIL))
                          (CONS X L))
             ((ENABLE PERMUTATION APPEND REMOVE MEMBER)
              (INDUCT (LENGTH L))
              (EXPAND (APPEND L (LIST X)))
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE PERMUTATION-APPEND-CAR)

(PROVE-LEMMA PERMUTATION-APPEND-INSERT
             (REWRITE)
             (IMPLIES (AND (PERMUTATION A B)
                           (AND (SORTED B)
                                (AND (NOT (MEMBER X A))
                                     (NOT (MEMBER X B)))))
                      (PERMUTATION (APPEND A (CONS X 'NIL))
                                   (INSERT X B)))
             ((ENABLE APPEND INSERT PERMUTATION SORTED INSERT-REMOVE
                      MEMBER-INSERT NOT-LISTP-REMOVE NOT-MEMBER-REMOVE2
                      SORTED-REMOVE)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE PERMUTATION-APPEND-INSERT)

(PROVE-LEMMA PERMUTATION-REMOVE-REMOVE
             (REWRITE)
             (IMPLIES (AND (PERMUTATION A B)
                           (AND (MEMBER X A) (MEMBER X B)))
                      (PERMUTATION (REMOVE X A)
                                   (REMOVE X B)))
             ((ENABLE PERMUTATION MEMBER REMOVE MEMBER-REMOVE2 REMOVE-REMOVE)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE PERMUTATION-REMOVE-REMOVE)

(DEFN TRANSITIVITY-OF-PERMUTATION-INDUCTION
      (A B C)
      (IF (LISTP A)
          (TRANSITIVITY-OF-PERMUTATION-INDUCTION (CDR A)
                                                 (REMOVE (CAR A) B)
                                                 (REMOVE (CAR A) C))
          '0)
      NIL)

(PROVE-LEMMA TRANSITIVITY-OF-PERMUTATION-BASE-CASE NIL
             (IMPLIES (AND (NLISTP A)
                           (AND (PERMUTATION A B)
                                (PERMUTATION B C)))
                      (PERMUTATION A C))
             ((EXPAND (PERMUTATION A B)
                      (PERMUTATION B C)
                      (PERMUTATION A C))
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(PROVE-LEMMA TRANSITIVITY-OF-PERMUTATION-INDUCTION-STEP
             NIL
             (IMPLIES (AND (LISTP A)
                           (AND (IMPLIES (AND (PERMUTATION (CDR A)
                                                           (REMOVE (CAR A) B))
                                              (PERMUTATION (REMOVE (CAR A) B)
                                                           (REMOVE (CAR A) C)))
                                         (PERMUTATION (CDR A)
                                                      (REMOVE (CAR A) C)))
                                (AND (PERMUTATION A B)
                                     (PERMUTATION B C))))
                      (PERMUTATION A C))
             ((EXPAND (PERMUTATION A B)
                      (PERMUTATION A C))
              (USE (MEMBER-PERMUTATION2 (X (CAR A))
                                        (B B)
                                        (A C)))
              (ENABLE PERMUTATION-REMOVE-REMOVE)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(PROVE-LEMMA TRANSITIVITY-OF-PERMUTATION NIL
             (IMPLIES (AND (PERMUTATION A B)
                           (PERMUTATION B C))
                      (PERMUTATION A C))
             ((INDUCT (TRANSITIVITY-OF-PERMUTATION-INDUCTION A B C))
              (USE (TRANSITIVITY-OF-PERMUTATION-BASE-CASE (A A)
                                                          (B B)
                                                          (C C))
                   (TRANSITIVITY-OF-PERMUTATION-INDUCTION-STEP (A A)
                                                               (B B)
                                                               (C C)))
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(PROVE-LEMMA SETP-REMOVE
             (REWRITE)
             (IMPLIES (SETP A) (SETP (REMOVE X A)))
             ((ENABLE SETP REMOVE NOT-MEMBER-REMOVE2)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE SETP-REMOVE)

(DEFN SETP-PERMUTATION-INDUCTION
      (A B)
      (IF (LISTP A)
          (SETP-PERMUTATION-INDUCTION (CDR A)
                                      (REMOVE (CAR A) B))
          '0)
      NIL)

(PROVE-LEMMA SETP-PERMUTATION-BASE-CASE NIL
             (IMPLIES (AND (NOT (LISTP A)) (PLISTP A))
                      (SETP A))
             ((ENABLE SETP PLISTP)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(PROVE-LEMMA SETP-PERMUTATION-INDUCTION-STEP
 NIL
 (IMPLIES
      (AND (LISTP A)
           (AND (SETP B)
                (AND (PLISTP A)
                     (AND (PERMUTATION A B)
                          (IMPLIES (AND (SETP (REMOVE (CAR A) B))
                                        (AND (PLISTP (CDR A))
                                             (PERMUTATION (CDR A)
                                                          (REMOVE (CAR A) B))))
                                   (SETP (CDR A)))))))
      (SETP A))
 ((ENABLE SETP PERMUTATION REMOVE MEMBER PLISTP NOT-MEMBER-REMOVE1 SETP-REMOVE)
  (USE (NOT-MEMBER-PERMUTATION (X (CAR A))
                               (A (CDR A))
                               (B (REMOVE (CAR A) B))))
  (ENABLE-THEORY GROUND-ZERO)
  (DISABLE-THEORY T)))

(PROVE-LEMMA SETP-PERMUTATION NIL
             (IMPLIES (AND (SETP B)
                           (AND (PLISTP A) (PERMUTATION A B)))
                      (SETP A))
             ((INDUCT (SETP-PERMUTATION-INDUCTION A B))
              (USE (SETP-PERMUTATION-BASE-CASE (A A))
                   (SETP-PERMUTATION-INDUCTION-STEP (A A)
                                                    (B B)))
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(PROVE-LEMMA SETP-INSERT
             (REWRITE)
             (IMPLIES (AND (SETP L) (NOT (MEMBER I L)))
                      (SETP (INSERT I L)))
             ((ENABLE SETP INSERT MEMBER NOT-MEMBER-INSERT)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE SETP-INSERT)

(DEFN GETNTH
      (N L)
      (IF (LISTP L)
          (IF (ZEROP N)
              (CAR L)
              (GETNTH (SUB1 N) (CDR L)))
          '0)
      NIL)

(DEFN PUTNTH
      (V N L)
      (IF (LISTP L)
          (IF (ZEROP N)
              (CONS V (CDR L))
              (CONS (CAR L)
                    (PUTNTH V (SUB1 N) (CDR L))))
          L)
      NIL)

(DEFN GETSEG
      (N K L)
      (IF (ZEROP K)
          'NIL
          (CONS (GETNTH N L)
                (GETSEG (ADD1 N) (SUB1 K) L)))
      NIL)

(DEFN PUTSEG
      (S N L)
      (IF (LISTP S)
          (PUTNTH (CAR S)
                  N
                  (PUTSEG (CDR S) (ADD1 N) L))
          L)
      NIL)

(DEFN FIXLENGTH
      (N L DEFAULT)
      (IF (LISTP L)
          (IF (ZEROP N)
              'NIL
              (CONS (CAR L)
                    (FIXLENGTH (SUB1 N) (CDR L) DEFAULT)))
          (IF (ZEROP N)
              'NIL
              (CONS DEFAULT
                    (FIXLENGTH (SUB1 N) L DEFAULT))))
      NIL)

(DEFN FIRSTN
      (N L)
      (IF (LISTP L)
          (IF (ZEROP N)
              'NIL
              (CONS (CAR L)
                    (FIRSTN (SUB1 N) (CDR L))))
          'NIL)
      NIL)

(DEFN NTHCDR
      (N L)
      (IF (LISTP L)
          (IF (ZEROP N)
              L
              (NTHCDR (SUB1 N) (CDR L)))
          L)
      NIL)

(PROVE-LEMMA NON-ZERO-LENGTH-IMPLIES-LISTP
             (REWRITE)
             (IMPLIES (NOT (ZEROP (LENGTH L)))
                      (LISTP L))
             ((ENABLE LENGTH)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE NON-ZERO-LENGTH-IMPLIES-LISTP)

(PROVE-LEMMA LISTP-IMPLIES-NON-ZERO-LENGTH
             (REWRITE)
             (IMPLIES (LISTP L)
                      (NOT (EQUAL (LENGTH L) '0)))
             ((ENABLE LENGTH)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE LISTP-IMPLIES-NON-ZERO-LENGTH)

(PROVE-LEMMA PLIST-OF-NON-ZERO-LENGTH-IS-A-LIST
             (REWRITE)
             (IMPLIES (AND (PLISTP A)
                           (NOT (EQUAL (LENGTH A) '0)))
                      (LISTP A))
             ((ENABLE PLISTP LENGTH)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE PLIST-OF-NON-ZERO-LENGTH-IS-A-LIST)

(PROVE-LEMMA LISTP-APPEND
             (REWRITE)
             (EQUAL (LISTP (APPEND A B))
                    (OR (LISTP A) (LISTP B)))
             ((ENABLE APPEND)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE LISTP-APPEND)

(PROVE-LEMMA LISTP-APPEND-LEFT
             (REWRITE)
             (IMPLIES (LISTP A)
                      (LISTP (APPEND A B)))
             ((ENABLE APPEND)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE LISTP-APPEND-LEFT)

(PROVE-LEMMA LISTP-GETSEG
             (REWRITE)
             (IMPLIES (NOT (ZEROP K))
                      (LISTP (GETSEG N K L)))
             ((ENABLE NON-ZERO-LENGTH-IMPLIES-LISTP GETSEG)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE LISTP-GETSEG)

(PROVE-LEMMA LISTP-PUTNTH
             (REWRITE)
             (EQUAL (LISTP (PUTNTH V N L))
                    (LISTP L))
             ((ENABLE PUTNTH)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE LISTP-PUTNTH)

(PROVE-LEMMA LISTP-PUTSEG
             (REWRITE)
             (EQUAL (LISTP (PUTSEG S N L))
                    (LISTP L))
             ((ENABLE PUTSEG LISTP-PUTNTH)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE LISTP-PUTSEG)

(PROVE-LEMMA REWRITE-CAR-TO-GETNTH-0
             (REWRITE)
             (EQUAL (CAR L) (GETNTH '0 L))
             ((ENABLE GETNTH)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE REWRITE-CAR-TO-GETNTH-0)

(PROVE-LEMMA CAR-APPEND-CASESPLIT
             (REWRITE)
             (EQUAL (CAR (APPEND A B))
                    (IF (LISTP A) (CAR A) (CAR B)))
             ((ENABLE APPEND)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE CAR-APPEND-CASESPLIT)

(PROVE-LEMMA CAR-APPEND
             (REWRITE)
             (IMPLIES (LISTP A)
                      (EQUAL (CAR (APPEND A B)) (CAR A)))
             ((ENABLE APPEND)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE CAR-APPEND)

(PROVE-LEMMA CAR-GETSEG
             (REWRITE)
             (IMPLIES (NOT (ZEROP K))
                      (EQUAL (CAR (GETSEG N K L))
                             (GETNTH N L)))
             ((ENABLE GETSEG)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE CAR-GETSEG)

(PROVE-LEMMA CAR-PUTNTH-ZERO
             (REWRITE)
             (IMPLIES (AND (LISTP L) (ZEROP N))
                      (EQUAL (CAR (PUTNTH V N L)) V))
             ((ENABLE PUTNTH)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE CAR-PUTNTH-ZERO)

(PROVE-LEMMA CAR-PUTSEG-ZERO
             (REWRITE)
             (IMPLIES (AND (ZEROP N)
                           (AND (LISTP S) (LISTP L)))
                      (EQUAL (CAR (PUTSEG S N L)) (CAR S)))
             ((ENABLE CAR-PUTNTH-ZERO PUTSEG)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE CAR-PUTSEG-ZERO)

(PROVE-LEMMA CDR-APPEND
             (REWRITE)
             (EQUAL (CDR (APPEND A B))
                    (IF (LISTP A)
                        (APPEND (CDR A) B)
                        (CDR B)))
             ((ENABLE APPEND)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE CDR-APPEND)

(PROVE-LEMMA CDR-GETSEG
             (REWRITE)
             (IMPLIES (NOT (ZEROP K))
                      (EQUAL (CDR (GETSEG N K L))
                             (GETSEG (ADD1 N) (SUB1 K) L)))
             ((ENABLE GETSEG)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE CDR-GETSEG)

(PROVE-LEMMA CDR-IS-NIL-WHEN-LENGTH-IS-1
             (REWRITE)
             (IMPLIES (AND (PLISTP L)
                           (EQUAL (LENGTH L) '1))
                      (EQUAL (EQUAL (CDR L) 'NIL)
                             '*1*TRUE))
             ((ENABLE PLISTP LENGTH)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE CDR-IS-NIL-WHEN-LENGTH-IS-1)

(PROVE-LEMMA PLIST-OF-LENGTH-0
             (REWRITE)
             (IMPLIES (AND (PLISTP L)
                           (EQUAL (LENGTH L) '0))
                      (EQUAL (EQUAL L 'NIL) '*1*TRUE))
             ((ENABLE PLISTP LENGTH)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE PLIST-OF-LENGTH-0)

(PROVE-LEMMA PLISTP-APPEND
             (REWRITE)
             (IMPLIES (PLISTP B)
                      (PLISTP (APPEND A B)))
             ((ENABLE PLISTP APPEND)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE PLISTP-APPEND)

(PROVE-LEMMA PLISTP-LIST1
             (REWRITE)
             (PLISTP (CONS X 'NIL))
             ((ENABLE PLISTP)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE PLISTP-LIST1)

(PROVE-LEMMA PLISTP-LIST2
             (REWRITE)
             (PLISTP (CONS X (CONS Y 'NIL)))
             ((ENABLE PLISTP)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE PLISTP-LIST2)

(PROVE-LEMMA PLISTP-PUTNTH
             (REWRITE)
             (IMPLIES (PLISTP L)
                      (PLISTP (PUTNTH V I L)))
             ((ENABLE PLISTP PUTNTH)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE PLISTP-PUTNTH)

(PROVE-LEMMA PLISTP-GETSEG
             (REWRITE)
             (PLISTP (GETSEG N K L))
             ((ENABLE PLISTP GETSEG)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE PLISTP-GETSEG)

(PROVE-LEMMA PLISTP-PUTSEG
             (REWRITE)
             (IMPLIES (PLISTP L)
                      (PLISTP (PUTSEG S N L)))
             ((ENABLE PLISTP PUTSEG PLISTP-PUTNTH)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE PLISTP-PUTSEG)

(PROVE-LEMMA PLISTP-FIXLENGTH
             (REWRITE)
             (PLISTP (FIXLENGTH N L V))
             ((ENABLE PLISTP FIXLENGTH)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE PLISTP-FIXLENGTH)

(PROVE-LEMMA LENGTH-APPEND
             (REWRITE)
             (EQUAL (LENGTH (APPEND A B))
                    (PLUS (LENGTH A) (LENGTH B)))
             ((ENABLE APPEND LENGTH)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE LENGTH-APPEND)

(PROVE-LEMMA LENGTH-PUTNTH
             (REWRITE)
             (EQUAL (LENGTH (PUTNTH N V L))
                    (LENGTH L))
             ((ENABLE PUTNTH LENGTH)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE LENGTH-PUTNTH)

(PROVE-LEMMA LENGTH-GETSEG
             (REWRITE)
             (EQUAL (LENGTH (GETSEG N K L))
                    (FIX K))
             ((ENABLE GETSEG LENGTH)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE LENGTH-GETSEG)

(PROVE-LEMMA LENGTH-PUTSEG
             (REWRITE)
             (EQUAL (LENGTH (PUTSEG S N L))
                    (LENGTH L))
             ((ENABLE LENGTH-PUTNTH PUTSEG)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE LENGTH-PUTSEG)

(PROVE-LEMMA LENGTH-FIXLENGTH
             (REWRITE)
             (EQUAL (LENGTH (FIXLENGTH N L DEFAULT))
                    (FIX N))
             ((ENABLE FIXLENGTH LENGTH)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE LENGTH-FIXLENGTH)

(PROVE-LEMMA APPEND-NON-LIST-LEFT
             (REWRITE)
             (IMPLIES (NOT (LISTP A))
                      (EQUAL (APPEND A B) B))
             ((ENABLE APPEND)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE APPEND-NON-LIST-LEFT)

(PROVE-LEMMA APPEND-NON-LIST-LEFT-COROLLARY
             (REWRITE)
             (IMPLIES (EQUAL (LENGTH A) '0)
                      (EQUAL (APPEND A B) B))
             ((ENABLE APPEND LENGTH)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE APPEND-NON-LIST-LEFT-COROLLARY)

(PROVE-LEMMA APPEND-NIL-ON-RIGHT
             (REWRITE)
             (IMPLIES (PLISTP A)
                      (EQUAL (APPEND A 'NIL) A))
             ((ENABLE APPEND PLISTP)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE APPEND-NIL-ON-RIGHT)

(PROVE-LEMMA APPEND-CDR
             (REWRITE)
             (IMPLIES (LISTP A)
                      (EQUAL (APPEND (CDR A) B)
                             (CDR (APPEND A B))))
             ((ENABLE APPEND)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE APPEND-CDR)

(PROVE-LEMMA APPEND-CROCK
             (REWRITE)
             (EQUAL (APPEND (CONS A 'NIL) (APPEND B C))
                    (APPEND (CONS A B) C))
             ((ENABLE APPEND)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE APPEND-CROCK)

(PROVE-LEMMA ASSOCIATIVITY-OF-APPEND
             (REWRITE)
             (EQUAL (APPEND (APPEND A B) C)
                    (APPEND A (APPEND B C)))
             ((ENABLE APPEND)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE ASSOCIATIVITY-OF-APPEND)

(PROVE-LEMMA APPEND-FIXLENGTH
             (REWRITE)
             (EQUAL (APPEND (FIXLENGTH A 'NIL DEFAULT)
                            (FIXLENGTH B 'NIL DEFAULT))
                    (FIXLENGTH (PLUS A B) 'NIL DEFAULT))
             ((ENABLE FIXLENGTH APPEND)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE APPEND-FIXLENGTH)

(PROVE-LEMMA GETNTH-0-2
             (REWRITE)
             (EQUAL (GETNTH '0 (CONS A (CONS B 'NIL)))
                    A)
             ((ENABLE GETNTH)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE GETNTH-0-2)

(PROVE-LEMMA GETNTH-1-2
             (REWRITE)
             (EQUAL (GETNTH '1 (CONS A (CONS B 'NIL)))
                    B)
             ((ENABLE GETNTH)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE GETNTH-1-2)

(PROVE-LEMMA LIST-GETNTH-0
             (REWRITE)
             (IMPLIES (AND (PLISTP L)
                           (EQUAL (LENGTH L) '1))
                      (EQUAL (CONS (GETNTH '0 L) 'NIL) L))
             ((ENABLE PLISTP GETNTH LENGTH PLIST-OF-LENGTH-0
                      NON-ZERO-LENGTH-IMPLIES-LISTP)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE LIST-GETNTH-0)

(PROVE-LEMMA OPEN-UP-GETNTH
             (REWRITE)
             (EQUAL (GETNTH (ADD1 N) (CONS A B))
                    (GETNTH N B))
             ((ENABLE GETNTH)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE OPEN-UP-GETNTH)

(PROVE-LEMMA OPEN-UP-GETNTH1
             (REWRITE)
             (IMPLIES (NOT (ZEROP N))
                      (EQUAL (GETNTH N (CONS A B))
                             (GETNTH (SUB1 N) B)))
             ((ENABLE GETNTH)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE OPEN-UP-GETNTH1)

(PROVE-LEMMA OPEN-UP-GETNTH-ON-ZERO
             (REWRITE)
             (EQUAL (GETNTH '0 (CONS A B)) A)
             ((ENABLE GETNTH)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE OPEN-UP-GETNTH-ON-ZERO)

(PROVE-LEMMA GETNTH-WITH-NON-NUMBER-INDEX
             (REWRITE)
             (IMPLIES (NOT (NUMBERP N))
                      (EQUAL (GETNTH N L) (GETNTH '0 L)))
             ((ENABLE GETNTH)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE GETNTH-WITH-NON-NUMBER-INDEX)

(PROVE-LEMMA GETNTH-APPEND-FOR-LENGTH-LEFT
             (REWRITE)
             (EQUAL (GETNTH (LENGTH A) (APPEND A B))
                    (IF (LISTP B) (CAR B) '0))
             ((ENABLE GETNTH APPEND LENGTH)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE GETNTH-APPEND-FOR-LENGTH-LEFT)

(PROVE-LEMMA GETNTH-APPEND-CASESPLIT
             (REWRITE)
             (EQUAL (GETNTH N (APPEND A B))
                    (IF (LESSP N (LENGTH A))
                        (GETNTH N A)
                        (GETNTH (DIFFERENCE N (LENGTH A)) B)))
             ((ENABLE GETNTH APPEND CAR-APPEND APPEND-NON-LIST-LEFT LENGTH)
              (INDUCT (GETNTH N A))
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE GETNTH-APPEND-CASESPLIT)

(PROVE-LEMMA GETNTH-APPEND-RIGHT
             (REWRITE)
             (IMPLIES (IF (LESSP N (LENGTH A))
                          '*1*FALSE
                          '*1*TRUE)
                      (EQUAL (GETNTH N (APPEND A B))
                             (GETNTH (DIFFERENCE N (LENGTH A)) B)))
             ((ENABLE GETNTH-APPEND-CASESPLIT LENGTH)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE GETNTH-APPEND-RIGHT)

(PROVE-LEMMA GETNTH-APPEND-LEFT
             (REWRITE)
             (IMPLIES (LESSP N (LENGTH A))
                      (EQUAL (GETNTH N (APPEND A B))
                             (GETNTH N A)))
             ((ENABLE GETNTH-APPEND-CASESPLIT LENGTH)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE GETNTH-APPEND-LEFT)

(PROVE-LEMMA GETNTH-PUTNTH-CASESPLIT
             (REWRITE)
             (EQUAL (GETNTH I (PUTNTH V J L))
                    (IF (LESSP I (LENGTH L))
                        (IF (EQUAL (FIX I) (FIX J))
                            V
                            (GETNTH I L))
                        (GETNTH I L)))
             ((ENABLE GETNTH PUTNTH LENGTH)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE GETNTH-PUTNTH-CASESPLIT)

(PROVE-LEMMA GETNTH-PUTNTH-COINCIDENCE
             (REWRITE)
             (IMPLIES (LESSP N (LENGTH L))
                      (EQUAL (GETNTH N (PUTNTH V N L)) V))
             ((ENABLE GETNTH-PUTNTH-CASESPLIT LENGTH)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE GETNTH-PUTNTH-COINCIDENCE)

(PROVE-LEMMA GETNTH-PUTNTH-NON-INTERFERENCE
             (REWRITE)
             (IMPLIES (NOT (EQUAL (FIX I) (FIX J)))
                      (EQUAL (GETNTH I (PUTNTH V J L))
                             (GETNTH I L)))
             ((ENABLE GETNTH-PUTNTH-CASESPLIT)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE GETNTH-PUTNTH-NON-INTERFERENCE)

(PROVE-LEMMA GETNTH-GETSEG-ZERO-INDEX
             (REWRITE)
             (IMPLIES (AND (NOT (ZEROP K)) (ZEROP I))
                      (EQUAL (GETNTH I (GETSEG N K L))
                             (GETNTH N L)))
             ((ENABLE GETNTH GETSEG)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE GETNTH-GETSEG-ZERO-INDEX)

(DEFN GETNTH-GETSEG-INDUCTION
      (I N K)
      (IF (OR (ZEROP I) (ZEROP K))
          '0
          (GETNTH-GETSEG-INDUCTION (SUB1 I)
                                   (ADD1 N)
                                   (SUB1 K)))
      NIL)

(PROVE-LEMMA GETNTH-GETSEG
             (REWRITE)
             (IMPLIES (LESSP I K)
                      (EQUAL (GETNTH I (GETSEG N K L))
                             (GETNTH (PLUS N I) L)))
             ((ENABLE GETSEG GETNTH GETNTH-GETSEG-ZERO-INDEX PLUS-0 PLUS-ADD1
                      PLUS-RIGHT-ID2)
              (INDUCT (GETNTH-GETSEG-INDUCTION I N K))
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE GETNTH-GETSEG)

(PROVE-LEMMA GETNTH-GETSEG-INVERSE
             (REWRITE)
             (IMPLIES (LESSP I K)
                      (EQUAL (GETNTH (PLUS N I) L)
                             (GETNTH I (GETSEG N K L))))
             ((ENABLE GETNTH-GETSEG)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE GETNTH-GETSEG-INVERSE)

(PROVE-LEMMA GETNTH-AFTER-PUTSEG
             (REWRITE)
             (IMPLIES (IF (LESSP I (PLUS N (LENGTH S)))
                          '*1*FALSE
                          '*1*TRUE)
                      (EQUAL (GETNTH I (PUTSEG S N L))
                             (GETNTH I L)))
             ((ENABLE PUTSEG GETNTH GETNTH-PUTNTH-CASESPLIT LENGTH)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE GETNTH-AFTER-PUTSEG)

(PROVE-LEMMA GETNTH-BEFORE-PUTSEG
             (REWRITE)
             (IMPLIES (LESSP I N)
                      (EQUAL (GETNTH I (PUTSEG S N L))
                             (GETNTH I L)))
             ((ENABLE PUTSEG GETNTH GETNTH-PUTNTH-CASESPLIT)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE GETNTH-BEFORE-PUTSEG)

(PROVE-LEMMA GETNTH-PUTSEG-COINCIDENCE
             (REWRITE)
             (IMPLIES (AND (IF (LESSP I N) '*1*FALSE '*1*TRUE)
                           (AND (LESSP (DIFFERENCE I N) (LENGTH S))
                                (LESSP I (LENGTH L))))
                      (EQUAL (GETNTH I (PUTSEG S N L))
                             (GETNTH (DIFFERENCE I N) S)))
             ((ENABLE PUTSEG GETNTH LENGTH CAR-PUTSEG-ZERO DIFFERENCE-X-X
                      DIFFERENCE-SUB1-ARG1 GETNTH-PUTNTH-CASESPLIT
                      LENGTH-PUTSEG LISTP-PUTSEG NON-ZERO-LENGTH-IMPLIES-LISTP)
              (INDUCT (PUTSEG S N L))
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE GETNTH-PUTSEG-COINCIDENCE)

(PROVE-LEMMA OPEN-PUTNTH-CASESPLIT
             (REWRITE)
             (EQUAL (PUTNTH V N (CONS A B))
                    (IF (ZEROP N)
                        (CONS V B)
                        (CONS A (PUTNTH V (SUB1 N) B))))
             ((ENABLE PUTNTH)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE OPEN-PUTNTH-CASESPLIT)

(PROVE-LEMMA OPEN-UP-PUTNTH1
             (REWRITE)
             (IMPLIES (NOT (ZEROP N))
                      (EQUAL (PUTNTH V N (CONS A B))
                             (CONS A (PUTNTH V (SUB1 N) B))))
             ((ENABLE PUTNTH)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE OPEN-UP-PUTNTH1)

(PROVE-LEMMA PUTNTH-INTO-NIL
             (REWRITE)
             (EQUAL (PUTNTH V I 'NIL) 'NIL)
             ((ENABLE PUTNTH)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE PUTNTH-INTO-NIL)

(PROVE-LEMMA OPEN-UP-PUTNTH-ON-ZERO
             (REWRITE)
             (EQUAL (PUTNTH VAL '0 (CONS A B))
                    (CONS VAL B))
             ((ENABLE PUTNTH)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE OPEN-UP-PUTNTH-ON-ZERO)

(PROVE-LEMMA PUTNTH-WITH-NON-NUMBER-INDEX
             (REWRITE)
             (IMPLIES (NOT (NUMBERP I))
                      (EQUAL (PUTNTH V I L)
                             (PUTNTH V '0 L)))
             ((ENABLE PUTNTH)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE PUTNTH-WITH-NON-NUMBER-INDEX)

(PROVE-LEMMA PUTNTH-HAS-NO-EFFECT
             (REWRITE)
             (IMPLIES (NOT (LESSP N (LENGTH L)))
                      (EQUAL (PUTNTH V N L) L))
             ((ENABLE PUTNTH LENGTH)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE PUTNTH-HAS-NO-EFFECT)

(PROVE-LEMMA PUTNTH-CONS1
             (REWRITE)
             (IMPLIES (ZEROP N)
                      (EQUAL (PUTNTH V N (CONS A B))
                             (CONS V B)))
             ((ENABLE PUTNTH)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE PUTNTH-CONS1)

(PROVE-LEMMA PUTNTH-CONS2
             (REWRITE)
             (IMPLIES (NOT (ZEROP N))
                      (EQUAL (PUTNTH V N (CONS A B))
                             (CONS A (PUTNTH V (SUB1 N) B))))
             ((ENABLE PUTNTH)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE PUTNTH-CONS2)

(PROVE-LEMMA PUTNTH-SHIFT
             (REWRITE)
             (IMPLIES (LESSP I (LENGTH L))
                      (EQUAL (PUTNTH V I L)
                             (APPEND (FIRSTN I L)
                                     (CONS V (NTHCDR (ADD1 I) L)))))
             ((ENABLE PUTNTH APPEND FIRSTN NTHCDR LENGTH)
              (INDUCT (NUMBER-AND-LIST-INDUCTION I L))
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE PUTNTH-SHIFT)

(PROVE-LEMMA PUTNTH-APPEND-CASESPLIT
             (REWRITE)
             (EQUAL (PUTNTH V N (APPEND A B))
                    (IF (LESSP N (LENGTH A))
                        (APPEND (PUTNTH V N A) B)
                        (APPEND A
                                (PUTNTH V
                                        (DIFFERENCE N (LENGTH A))
                                        B))))
             ((ENABLE PUTNTH APPEND LENGTH)
              (INDUCT (PUTNTH V N A))
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE PUTNTH-APPEND-CASESPLIT)

(PROVE-LEMMA PUTNTH-APPEND-RIGHT
             (REWRITE)
             (IMPLIES (IF (LESSP N (LENGTH A))
                          '*1*FALSE
                          '*1*TRUE)
                      (EQUAL (PUTNTH V N (APPEND A B))
                             (APPEND A
                                     (PUTNTH V
                                             (DIFFERENCE N (LENGTH A))
                                             B))))
             ((ENABLE PUTNTH-APPEND-CASESPLIT LENGTH)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE PUTNTH-APPEND-RIGHT)

(PROVE-LEMMA PUTNTH-APPEND-LEFT
             (REWRITE)
             (IMPLIES (LESSP N (LENGTH A))
                      (EQUAL (PUTNTH V N (APPEND A B))
                             (APPEND (PUTNTH V N A) B)))
             ((ENABLE PUTNTH-APPEND-CASESPLIT LENGTH)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE PUTNTH-APPEND-LEFT)

(PROVE-LEMMA PUTNTH-GETNTH-COINCIDENCE
             (REWRITE)
             (EQUAL (PUTNTH (GETNTH I L) I L) L)
             ((ENABLE GETNTH PUTNTH)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE PUTNTH-GETNTH-COINCIDENCE)

(PROVE-LEMMA PUTNTH-GETNTH-COINCIDENCE1
             (REWRITE)
             (IMPLIES (EQUAL (GETNTH I L1) (GETNTH I L2))
                      (EQUAL (PUTNTH (GETNTH I L1)
                                     I
                                     (PUTNTH V I L2))
                             L2))
             ((ENABLE PUTNTH GETNTH)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE PUTNTH-GETNTH-COINCIDENCE1)

(PROVE-LEMMA PUTNTH-PUTNTH-CASESPLIT
             (REWRITE)
             (IMPLIES (AND (NUMBERP I)
                           (AND (NUMBERP J)
                                (IF (LESSP J I)
                                    '*1*FALSE
                                    '*1*TRUE)))
                      (EQUAL (PUTNTH B J (PUTNTH A I L))
                             (IF (EQUAL I J)
                                 (PUTNTH B J L)
                                 (PUTNTH A I (PUTNTH B J L)))))
             ((ENABLE PUTNTH)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE PUTNTH-PUTNTH-CASESPLIT)

(PROVE-LEMMA PUTNTH-COINCIDENCE
             (REWRITE)
             (IMPLIES (EQUAL (FIX I) (FIX J))
                      (EQUAL (PUTNTH B J (PUTNTH A I L))
                             (PUTNTH B J L)))
             ((ENABLE PUTNTH)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE PUTNTH-COINCIDENCE)

(PROVE-LEMMA PUTNTH-NON-INTERFERENCE
             NIL
             (IMPLIES (NOT (EQUAL (FIX I) (FIX J)))
                      (EQUAL (PUTNTH B J (PUTNTH A I L))
                             (PUTNTH A I (PUTNTH B J L))))
             ((ENABLE PUTNTH)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(PROVE-LEMMA PUTNTH-NON-INTERFERENCE-COROLLARY1
             (REWRITE)
             (IMPLIES (LESSP (FIX I) (ADD1 J))
                      (EQUAL (PUTNTH B (ADD1 J) (PUTNTH A I L))
                             (PUTNTH A I (PUTNTH B (ADD1 J) L))))
             ((USE (PUTNTH-NON-INTERFERENCE (I I)
                                            (J (ADD1 J))
                                            (A A)
                                            (B B)
                                            (L L)))
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE PUTNTH-NON-INTERFERENCE-COROLLARY1)

(PROVE-LEMMA PUTNTH-NON-INTERFERENCE-COROLLARY2
             (REWRITE)
             (IMPLIES (LESSP (FIX I) (PLUS J K))
                      (EQUAL (PUTNTH B (PLUS J K) (PUTNTH A I L))
                             (PUTNTH A I (PUTNTH B (PLUS J K) L))))
             ((USE (PUTNTH-NON-INTERFERENCE (I I)
                                            (J (PLUS J K))
                                            (A A)
                                            (B B)
                                            (L L)))
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE PUTNTH-NON-INTERFERENCE-COROLLARY2)

(PROVE-LEMMA PUTNTH-PUTSEG-COINCIDENCE-PROOF
             (REWRITE)
             (IMPLIES (AND (NUMBERP N)
                           (AND (NUMBERP I)
                                (AND (IF (LESSP I N) '*1*FALSE '*1*TRUE)
                                     (LESSP (DIFFERENCE I N) (LENGTH S)))))
                      (EQUAL (PUTNTH V I (PUTSEG S N L))
                             (PUTSEG (PUTNTH V (DIFFERENCE I N) S)
                                     N L)))
             ((ENABLE PUTSEG PUTNTH LENGTH DIFFERENCE-X-X DIFFERENCE-SUB1-ARG1
                      LISTP-PUTSEG NON-ZERO-LENGTH-IMPLIES-LISTP
                      PUTNTH-PUTNTH-CASESPLIT)
              (INDUCT (PUTSEG S N L))
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE PUTNTH-PUTSEG-COINCIDENCE-PROOF)

(PROVE-LEMMA PUTSEG-WITH-NON-NUMBER-INDEX
             (REWRITE)
             (IMPLIES (NOT (NUMBERP N))
                      (EQUAL (PUTSEG S N L)
                             (PUTSEG S '0 L)))
             ((ENABLE PUTSEG PUTNTH-WITH-NON-NUMBER-INDEX)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE PUTSEG-WITH-NON-NUMBER-INDEX)

(PROVE-LEMMA PUTNTH-PUTSEG-COINCIDENCE
             (REWRITE)
             (IMPLIES (AND (IF (LESSP I N) '*1*FALSE '*1*TRUE)
                           (LESSP (DIFFERENCE I N) (LENGTH S)))
                      (EQUAL (PUTNTH V I (PUTSEG S N L))
                             (PUTSEG (PUTNTH V (DIFFERENCE I N) S)
                                     N L)))
             ((ENABLE PUTNTH-PUTSEG-COINCIDENCE-PROOF
                      PUTNTH-WITH-NON-NUMBER-INDEX
                      PUTSEG-WITH-NON-NUMBER-INDEX)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE PUTNTH-PUTSEG-COINCIDENCE)

(PROVE-LEMMA PUTNTH-PUTSEG-COINCIDENCE-INVERSE
             (REWRITE)
             (IMPLIES (AND (LESSP I (LENGTH S)) (NUMBERP I))
                      (EQUAL (PUTSEG (PUTNTH V I S) N L)
                             (PUTNTH V (PLUS I N) (PUTSEG S N L))))
             ((USE (PUTNTH-PUTSEG-COINCIDENCE (N N)
                                              (I (PLUS I N))
                                              (V V)
                                              (S S)
                                              (L L)))
              (ENABLE DIFFERENCE-PLUS2)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE PUTNTH-PUTSEG-COINCIDENCE-INVERSE)

(PROVE-LEMMA PUTNTH-AFTER-PUTSEG-PROOF
             (REWRITE)
             (IMPLIES (AND (NUMBERP I)
                           (AND (NUMBERP N)
                                (AND (IF (LESSP I N) '*1*FALSE '*1*TRUE)
                                     (IF (LESSP (DIFFERENCE I N) (LENGTH S))
                                         '*1*FALSE
                                         '*1*TRUE))))
                      (EQUAL (PUTNTH V I (PUTSEG S N L))
                             (PUTSEG S N (PUTNTH V I L))))
             ((ENABLE PUTNTH PUTSEG LENGTH PUTNTH-PUTNTH-CASESPLIT)
              (INDUCT (PUTSEG S N L))
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE PUTNTH-AFTER-PUTSEG-PROOF)

(PROVE-LEMMA PUTNTH-AFTER-PUTSEG
             (REWRITE)
             (IMPLIES (AND (IF (LESSP I N) '*1*FALSE '*1*TRUE)
                           (IF (LESSP (DIFFERENCE I N) (LENGTH S))
                               '*1*FALSE
                               '*1*TRUE))
                      (EQUAL (PUTNTH V I (PUTSEG S N L))
                             (PUTSEG S N (PUTNTH V I L))))
             ((ENABLE PUTNTH-AFTER-PUTSEG-PROOF PUTNTH-WITH-NON-NUMBER-INDEX
                      PUTSEG-WITH-NON-NUMBER-INDEX)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE PUTNTH-AFTER-PUTSEG)

(PROVE-LEMMA GETSEG-OF-LENGTH-ZERO
             (REWRITE)
             (IMPLIES (ZEROP K)
                      (EQUAL (GETSEG N K L) 'NIL))
             ((ENABLE GETSEG)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE GETSEG-OF-LENGTH-ZERO)

(PROVE-LEMMA GETSEG-ADD1-LENGTH
             (REWRITE)
             (EQUAL (GETSEG N (ADD1 K) L)
                    (APPEND (GETSEG N K L)
                            (CONS (GETNTH (PLUS N K) L) 'NIL)))
             ((ENABLE APPEND GETSEG PLUS-0 PLUS-RIGHT-ID2
                      GETNTH-WITH-NON-NUMBER-INDEX PLUS-ADD1)
              (INDUCT (GETSEG N K L))
              (EXPAND (GETSEG N 1 L))
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE GETSEG-ADD1-LENGTH)

(PROVE-LEMMA GETSEG-WITH-NON-NUMBER-INDEX
             (REWRITE)
             (IMPLIES (NOT (NUMBERP N))
                      (EQUAL (GETSEG N K L)
                             (GETSEG '0 K L)))
             ((ENABLE GETSEG GETNTH-WITH-NON-NUMBER-INDEX)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE GETSEG-WITH-NON-NUMBER-INDEX)

(PROVE-LEMMA GETSEG-ADD1-CONS
             (REWRITE)
             (EQUAL (GETSEG (ADD1 N) K (CONS A B))
                    (GETSEG N K B))
             ((ENABLE GETSEG GETNTH)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE GETSEG-ADD1-CONS)

(PROVE-LEMMA GETSEG-LENGTH-1
             NIL
             (EQUAL (GETSEG N '1 L)
                    (CONS (GETNTH N L) 'NIL))
             ((ENABLE GETSEG)
              (EXPAND (GETSEG N 1 L))
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(PROVE-LEMMA GETSEG-LENGTH-1-RULE
             (REWRITE)
             (IMPLIES (EQUAL K '1)
                      (EQUAL (GETSEG N K L)
                             (CONS (GETNTH N L) 'NIL)))
             ((USE (GETSEG-LENGTH-1 (N N) (K '1) (L L)))
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE GETSEG-LENGTH-1-RULE)

(PROVE-LEMMA GETSEG-ADD1-LENGTH2
             (REWRITE)
             (IMPLIES (AND (NUMBERP N)
                           (IF (LESSP (LENGTH L) (ADD1 N))
                               '*1*FALSE
                               '*1*TRUE))
                      (EQUAL (GETSEG N (ADD1 K) L)
                             (CONS (GETNTH N L)
                                   (GETSEG (ADD1 N) K L))))
             ((ENABLE GETNTH GETSEG LENGTH NON-ZERO-LENGTH-IMPLIES-LISTP)
              (INDUCT (NUMBER-AND-LIST-INDUCTION N L))
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE GETSEG-ADD1-LENGTH2)

(PROVE-LEMMA GETSEG-APPEND-RIGHT
             (REWRITE)
             (IMPLIES (IF (LESSP N (LENGTH A))
                          '*1*FALSE
                          '*1*TRUE)
                      (EQUAL (GETSEG N K (APPEND A B))
                             (GETSEG (DIFFERENCE N (LENGTH A))
                                     K B)))
             ((ENABLE GETSEG LENGTH GETNTH-APPEND-RIGHT DIFFERENCE-SUB1-ARG2)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE GETSEG-APPEND-RIGHT)

(PROVE-LEMMA
         GETSEG-ACROSS-APPEND
         (REWRITE)
         (IMPLIES (AND (NUMBERP N)
                       (AND (IF (LESSP (LENGTH A) N)
                                '*1*FALSE
                                '*1*TRUE)
                            (IF (LESSP (PLUS N K) (LENGTH A))
                                '*1*FALSE
                                '*1*TRUE)))
                  (EQUAL (GETSEG N K (APPEND A B))
                         (APPEND (GETSEG N (DIFFERENCE (LENGTH A) N) A)
                                 (GETSEG '0
                                         (DIFFERENCE K
                                                     (DIFFERENCE (LENGTH A) N))
                                         B))))
         ((ENABLE GETSEG APPEND GETNTH LENGTH APPEND-NIL-ON-RIGHT
                  APPEND-NON-LIST-LEFT-COROLLARY DIFFERENCE-X-X
                  DIFFERENCE-SUB1-ARG2 GETNTH-APPEND-FOR-LENGTH-LEFT
                  GETNTH-APPEND-LEFT GETSEG-ADD1-CONS GETSEG-APPEND-RIGHT
                  GETSEG-OF-LENGTH-ZERO PLISTP-GETSEG PLUS-0 PLUS-ADD1
                  PLUS-RIGHT-ID2 REWRITE-ZERO-DIFFERENCE-AS-EQUALITY)
          (INDUCT (NUMBER-AND-LIST-INDUCTION K A))
          (ENABLE-THEORY GROUND-ZERO)
          (DISABLE-THEORY T)))

(DISABLE GETSEG-ACROSS-APPEND)

(PROVE-LEMMA GETSEG-APPEND-LEFT
             (REWRITE)
             (IMPLIES (IF (LESSP (LENGTH A) (PLUS N K))
                          '*1*FALSE
                          '*1*TRUE)
                      (EQUAL (GETSEG N K (APPEND A B))
                             (GETSEG N K A)))
             ((ENABLE GETSEG LENGTH GETNTH-APPEND-LEFT)
              (DISABLE APPEND)
              (INDUCT (NUMBER-AND-LIST-INDUCTION K A))
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE GETSEG-APPEND-LEFT)

(PROVE-LEMMA GETSEG-AFTER-PUTNTH
             (REWRITE)
             (IMPLIES (LESSP N I)
                      (EQUAL (GETSEG I K (PUTNTH V N L))
                             (GETSEG I K L)))
             ((ENABLE GETSEG GETNTH-PUTNTH-CASESPLIT)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE GETSEG-AFTER-PUTNTH)

(PROVE-LEMMA GETSEG-BEFORE-PUTNTH
             (REWRITE)
             (IMPLIES (IF (LESSP N (PLUS I K))
                          '*1*FALSE
                          '*1*TRUE)
                      (EQUAL (GETSEG I K (PUTNTH V N L))
                             (GETSEG I K L)))
             ((ENABLE GETSEG GETNTH-PUTNTH-CASESPLIT)
              (INDUCT (GETSEG I K L))
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE GETSEG-BEFORE-PUTNTH)

(PROVE-LEMMA GETSEG-PUTNTH-COINCIDENCE
             (REWRITE)
             (IMPLIES (AND (IF (LESSP N I) '*1*FALSE '*1*TRUE)
                           (AND (LESSP (DIFFERENCE N I) K)
                                (LESSP N (LENGTH L))))
                      (EQUAL (GETSEG I K (PUTNTH V N L))
                             (PUTNTH V
                                     (DIFFERENCE N I)
                                     (GETSEG I K L))))
             ((ENABLE GETSEG LENGTH DIFFERENCE-SUB1-ARG1
                      GETNTH-PUTNTH-CASESPLIT GETSEG-OF-LENGTH-ZERO
                      GETSEG-AFTER-PUTNTH OPEN-PUTNTH-CASESPLIT
                      PUTNTH-WITH-NON-NUMBER-INDEX)
              (INDUCT (GETSEG I K L))
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE GETSEG-PUTNTH-COINCIDENCE)

(DEFN INTEGER-INDUCTION-INSTANCE
      (N K)
      (IF (ZEROP K)
          '0
          (INTEGER-INDUCTION-INSTANCE (ADD1 N)
                                      (SUB1 K)))
      NIL)

(PROVE-LEMMA GETSEG-GETSEG
             (REWRITE)
             (IMPLIES (IF (LESSP K (PLUS I J))
                          '*1*FALSE
                          '*1*TRUE)
                      (EQUAL (GETSEG I J (GETSEG N K L))
                             (GETSEG (PLUS N I) J L)))
             ((ENABLE GETSEG GETNTH-GETSEG PLUS-ADD1 PLUS-RIGHT-ID2 PLUS-0
                      GETNTH-WITH-NON-NUMBER-INDEX
                      GETSEG-WITH-NON-NUMBER-INDEX)
              (INDUCT (INTEGER-INDUCTION-INSTANCE I J))
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE GETSEG-GETSEG)

(PROVE-LEMMA GETSEG-AFTER-PUTSEG
             (REWRITE)
             (IMPLIES (IF (LESSP I (PLUS N (LENGTH S)))
                          '*1*FALSE
                          '*1*TRUE)
                      (EQUAL (GETSEG I K (PUTSEG S N L))
                             (GETSEG I K L)))
             ((ENABLE GETSEG PUTSEG LENGTH PLUS-ADD1 GETNTH-AFTER-PUTSEG)
              (INDUCT (INTEGER-INDUCTION-INSTANCE I K))
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE GETSEG-AFTER-PUTSEG)

(PROVE-LEMMA GETSEG-BEFORE-PUTSEG
             (REWRITE)
             (IMPLIES (IF (LESSP N (PLUS I K))
                          '*1*FALSE
                          '*1*TRUE)
                      (EQUAL (GETSEG I K (PUTSEG S N L))
                             (GETSEG I K L)))
             ((ENABLE GETSEG PUTSEG PLUS-ADD1 GETNTH-BEFORE-PUTSEG)
              (INDUCT (INTEGER-INDUCTION-INSTANCE I K))
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE GETSEG-BEFORE-PUTSEG)

(PROVE-LEMMA GETSEG-WITHIN-PUTSEG
             (REWRITE)
             (IMPLIES (AND (IF (LESSP I N) '*1*FALSE '*1*TRUE)
                           (AND (IF (LESSP (LENGTH L) (PLUS N (LENGTH S)))
                                    '*1*FALSE
                                    '*1*TRUE)
                                (IF (LESSP (PLUS N (LENGTH S)) (PLUS I K))
                                    '*1*FALSE
                                    '*1*TRUE)))
                      (EQUAL (GETSEG I K (PUTSEG S N L))
                             (GETSEG (DIFFERENCE I N) K S)))
             ((ENABLE GETSEG PUTSEG LENGTH PLUS-ADD1 GETNTH-PUTSEG-COINCIDENCE
                      DIFFERENCE-SUB1-ARG1 DIFFERENCE-SUB1-ARG2)
              (INDUCT (INTEGER-INDUCTION-INSTANCE I K))
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE GETSEG-WITHIN-PUTSEG)

(DEFN GETSEG-PUTSEG-INDUCTION
      (I K S N)
      (IF (ZEROP K)
          '0
          (IF (LISTP S)
              (GETSEG-PUTSEG-INDUCTION (ADD1 I)
                                       (SUB1 K)
                                       (CDR S)
                                       (ADD1 N))
              '0))
      NIL)

(PROVE-LEMMA PUTSEG-HAS-NO-EFFECT
             (REWRITE)
             (IMPLIES (NOT (LESSP N (LENGTH L)))
                      (EQUAL (PUTSEG S N L) L))
             ((ENABLE PUTSEG LENGTH PUTNTH-HAS-NO-EFFECT)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE PUTSEG-HAS-NO-EFFECT)

(PROVE-LEMMA PUTSEG-CONS2
             (REWRITE)
             (IMPLIES (NOT (ZEROP N))
                      (EQUAL (PUTSEG S N (CONS A B))
                             (CONS A (PUTSEG S (SUB1 N) B))))
             ((ENABLE PUTSEG PUTNTH-CONS2)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE PUTSEG-CONS2)

(PROVE-LEMMA
        GETSEG-AROUND-PUTSEG-PROOF
        (REWRITE)
        (IMPLIES (AND (NUMBERP I)
                      (AND (NUMBERP N)
                           (AND (IF (LESSP N I) '*1*FALSE '*1*TRUE)
                                (AND (IF (LESSP (LENGTH L) (PLUS N (LENGTH S)))
                                         '*1*FALSE
                                         '*1*TRUE)
                                     (IF (LESSP (PLUS I K) (PLUS N (LENGTH S)))
                                         '*1*FALSE
                                         '*1*TRUE)))))
                 (EQUAL (GETSEG I K (PUTSEG S N L))
                        (PUTSEG S
                                (DIFFERENCE N I)
                                (GETSEG I K L))))
        ((ENABLE GETSEG PUTSEG LENGTH GETNTH-BEFORE-PUTSEG
                 GETSEG-OF-LENGTH-ZERO GETSEG-PUTNTH-COINCIDENCE LENGTH-PUTSEG
                 PLUS-ADD1 PUTSEG-CONS2 PUTSEG-HAS-NO-EFFECT)
         (INDUCT (GETSEG-PUTSEG-INDUCTION I K S N))
         (ENABLE-THEORY GROUND-ZERO)
         (DISABLE-THEORY T)))

(DISABLE GETSEG-AROUND-PUTSEG-PROOF)

(PROVE-LEMMA NUMBERP-CASESPLIT
             NIL
             (OR (NUMBERP A) (NOT (NUMBERP A)))
             ((ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(PROVE-LEMMA GETSEG-AROUND-PUTSEG
             (REWRITE)
             (IMPLIES (AND (IF (LESSP N I) '*1*FALSE '*1*TRUE)
                           (AND (IF (LESSP (LENGTH L) (PLUS N (LENGTH S)))
                                    '*1*FALSE
                                    '*1*TRUE)
                                (IF (LESSP (PLUS I K) (PLUS N (LENGTH S)))
                                    '*1*FALSE
                                    '*1*TRUE)))
                      (EQUAL (GETSEG I K (PUTSEG S N L))
                             (PUTSEG S
                                     (DIFFERENCE N I)
                                     (GETSEG I K L))))
             ((USE (NUMBERP-CASESPLIT (A I))
                   (NUMBERP-CASESPLIT (A N))
                   (GETSEG-AROUND-PUTSEG-PROOF (I I)
                                               (N N)
                                               (K K)
                                               (S S)
                                               (L L))
                   (GETSEG-AROUND-PUTSEG-PROOF (I '0)
                                               (N N)
                                               (K K)
                                               (S S)
                                               (L L))
                   (GETSEG-AROUND-PUTSEG-PROOF (I I)
                                               (N '0)
                                               (K K)
                                               (S S)
                                               (L L))
                   (GETSEG-AROUND-PUTSEG-PROOF (I '0)
                                               (N '0)
                                               (K K)
                                               (S S)
                                               (L L)))
              (ENABLE GETSEG-WITH-NON-NUMBER-INDEX
                      PUTSEG-WITH-NON-NUMBER-INDEX)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE GETSEG-AROUND-PUTSEG)

(PROVE-LEMMA PUTSEG-NIL-SEGMENT
             (REWRITE)
             (EQUAL (PUTSEG 'NIL N L) L)
             ((ENABLE PUTSEG)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE PUTSEG-NIL-SEGMENT)

(PROVE-LEMMA PUTSEG-NON-LIST-SEGMENT
             (REWRITE)
             (IMPLIES (NOT (LISTP S))
                      (EQUAL (PUTSEG S N L) L))
             ((ENABLE PUTSEG)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE PUTSEG-NON-LIST-SEGMENT)

(PROVE-LEMMA OPEN-UP-PUTSEG-ON-SEGMENT-CONS
             (REWRITE)
             (IMPLIES (AND (NUMBERP N)
                           (IF (LESSP (LENGTH L)
                                      (PLUS N (LENGTH (CONS A B))))
                               '*1*FALSE
                               '*1*TRUE))
                      (EQUAL (PUTSEG (CONS A B) N L)
                             (PUTNTH A N
                                     (PUTSEG B (PLUS '1 N) L))))
             ((ENABLE PUTSEG LENGTH PLUS-ADD1 PLUS-1)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE OPEN-UP-PUTSEG-ON-SEGMENT-CONS)

(PROVE-LEMMA PUTSEG-CONS1
             (REWRITE)
             (IMPLIES (AND (ZEROP N) (LISTP S))
                      (EQUAL (PUTSEG S N (CONS A B))
                             (CONS (CAR S) (PUTSEG (CDR S) N B))))
             ((ENABLE PUTSEG PUTNTH-CONS1 PUTSEG-CONS2
                      PUTSEG-WITH-NON-NUMBER-INDEX)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE PUTSEG-CONS1)

(PROVE-LEMMA PUTSEG-GETSEG-COINCIDENCE
             (REWRITE)
             (IMPLIES (EQUAL I N)
                      (EQUAL (PUTSEG (GETSEG N K L) I L) L))
             ((ENABLE PUTSEG GETSEG PUTNTH-GETNTH-COINCIDENCE)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE PUTSEG-GETSEG-COINCIDENCE)

(PROVE-LEMMA EQUALITY-OF-GETNTH-BACKCHAIN-PROOF
             NIL
             (IMPLIES (AND (IF (LESSP I N) '*1*FALSE '*1*TRUE)
                           (AND (LESSP (DIFFERENCE I N) K)
                                (EQUAL (GETSEG N K L1)
                                       (GETSEG N K L2))))
                      (EQUAL (GETNTH I L1) (GETNTH I L2)))
             ((ENABLE GETSEG GETNTH GETNTH-GETSEG DIFFERENCE-X-X
                      PLUS-RIGHT-ID2)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DEFN NESTED-INTERVALS
      (N1 K1 N2 K2)
      (AND (IF (LESSP N2 N1)
               '*1*FALSE
               '*1*TRUE)
           (IF (LESSP (PLUS N1 K1) (PLUS N2 K2))
               '*1*FALSE
               '*1*TRUE))
      NIL)

(DEFN STRANGE-INDUCTION
      (A B C D)
      (IF (OR (ZEROP A) (ZEROP B))
          '0
          (STRANGE-INDUCTION (SUB1 A)
                             (SUB1 B)
                             (ADD1 C)
                             (ADD1 D)))
      NIL)

(PROVE-LEMMA PLUS-ARG2-MUST-BE-ZERO
             (REWRITE)
             (IMPLIES (AND (IF (LESSP I N) '*1*FALSE '*1*TRUE)
                           (IF (LESSP N (PLUS I J))
                               '*1*FALSE
                               '*1*TRUE))
                      (ZEROP J))
             ((ENABLE PLUS)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE PLUS-ARG2-MUST-BE-ZERO)

(PROVE-LEMMA GETSEG-MUST-BE-NIL
             (REWRITE)
             (IMPLIES (AND (IF (LESSP I N) '*1*FALSE '*1*TRUE)
                           (IF (LESSP N (PLUS I J))
                               '*1*FALSE
                               '*1*TRUE))
                      (EQUAL (GETSEG I J L) 'NIL))
             ((USE (PLUS-ARG2-MUST-BE-ZERO (I I)
                                           (J J)
                                           (N N)))
              (ENABLE GETSEG-OF-LENGTH-ZERO)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE GETSEG-MUST-BE-NIL)

(PROVE-LEMMA EQUALITY-OF-GETSEG-BACKCHAIN-BASE-CASE
             NIL
             (IMPLIES (AND (OR (ZEROP J) (ZEROP K))
                           (AND (NUMBERP I)
                                (AND (NUMBERP N)
                                     (AND (NESTED-INTERVALS N K I J)
                                          (EQUAL (GETSEG N K L1)
                                                 (GETSEG N K L2))))))
                      (EQUAL (GETSEG I J L1)
                             (GETSEG I J L2)))
             ((ENABLE NESTED-INTERVALS GETSEG-OF-LENGTH-ZERO
                      GETSEG-OF-LENGTH-ZERO PLUS-0 PLUS-RIGHT-ID2
                      GETSEG-MUST-BE-NIL)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(PROVE-LEMMA
 EQUALITY-OF-GETSEG-BACKCHAIN-INDUCTION-STEP-CASE1 NIL
 (IMPLIES
  (AND (NUMBERP I)
       (AND (NUMBERP N)
            (AND (NOT (ZEROP J))
                 (AND (NOT (ZEROP K))
                      (AND (IMPLIES (AND (NESTED-INTERVALS (ADD1 N)
                                                           (SUB1 K)
                                                           (ADD1 I)
                                                           (SUB1 J))
                                         (EQUAL (GETSEG (ADD1 N) (SUB1 K) L1)
                                                (GETSEG (ADD1 N) (SUB1 K) L2)))
                                    (EQUAL (GETSEG (ADD1 I) (SUB1 J) L1)
                                           (GETSEG (ADD1 I) (SUB1 J) L2)))
                           (AND (NESTED-INTERVALS N K I J)
                                (AND (EQUAL (GETSEG N K L1)
                                            (GETSEG N K L2))
                                     (EQUAL I N))))))))
  (EQUAL (GETSEG I J L1)
         (GETSEG I J L2)))
 ((ENABLE GETSEG NESTED-INTERVALS)
  (EXPAND (GETSEG N K L1)
          (GETSEG N K L2)
          (GETSEG I J L1)
          (GETSEG I J L2))
  (ENABLE-THEORY GROUND-ZERO)
  (DISABLE-THEORY T)))

(PROVE-LEMMA
 EQUALITY-OF-GETSEG-BACKCHAIN-INDUCTION-STEP-CASE2 NIL
 (IMPLIES
  (AND (NUMBERP I)
       (AND (NUMBERP N)
            (AND (NOT (ZEROP J))
                 (AND (NOT (ZEROP K))
                      (AND (IMPLIES (AND (NESTED-INTERVALS (ADD1 N)
                                                           (SUB1 K)
                                                           (ADD1 I)
                                                           (SUB1 J))
                                         (EQUAL (GETSEG (ADD1 N) (SUB1 K) L1)
                                                (GETSEG (ADD1 N) (SUB1 K) L2)))
                                    (EQUAL (GETSEG (ADD1 I) (SUB1 J) L1)
                                           (GETSEG (ADD1 I) (SUB1 J) L2)))
                           (AND (NESTED-INTERVALS N K I J)
                                (AND (EQUAL (GETSEG N K L1)
                                            (GETSEG N K L2))
                                     (LESSP N I))))))))
  (EQUAL (GETSEG I J L1)
         (GETSEG I J L2)))
 ((ENABLE GETSEG NESTED-INTERVALS)
  (EXPAND (GETSEG N K L1)
          (GETSEG N K L2)
          (GETSEG I J L1)
          (GETSEG I J L2))
  (USE (EQUALITY-OF-GETNTH-BACKCHAIN-PROOF (I I)
                                           (N (ADD1 N))
                                           (K (SUB1 K))
                                           (L1 L1)
                                           (L2 L2)))
  (ENABLE-THEORY GROUND-ZERO)
  (DISABLE-THEORY T)))

(PROVE-LEMMA EQUALITY-OF-GETSEG-BACKCHAIN-INDUCTION-STEP
 NIL
 (IMPLIES
  (AND (NUMBERP I)
       (AND (NUMBERP N)
            (AND (NOT (ZEROP J))
                 (AND (NOT (ZEROP K))
                      (AND (IMPLIES (AND (NESTED-INTERVALS (ADD1 N)
                                                           (SUB1 K)
                                                           (ADD1 I)
                                                           (SUB1 J))
                                         (EQUAL (GETSEG (ADD1 N) (SUB1 K) L1)
                                                (GETSEG (ADD1 N) (SUB1 K) L2)))
                                    (EQUAL (GETSEG (ADD1 I) (SUB1 J) L1)
                                           (GETSEG (ADD1 I) (SUB1 J) L2)))
                           (AND (NESTED-INTERVALS N K I J)
                                (EQUAL (GETSEG N K L1)
                                       (GETSEG N K L2))))))))
  (EQUAL (GETSEG I J L1)
         (GETSEG I J L2)))
 ((ENABLE NESTED-INTERVALS)
  (USE (LEQ-CASESPLIT (A I) (B N))
       (EQUALITY-OF-GETSEG-BACKCHAIN-INDUCTION-STEP-CASE1)
       (EQUALITY-OF-GETSEG-BACKCHAIN-INDUCTION-STEP-CASE2))
  (ENABLE-THEORY GROUND-ZERO)
  (DISABLE-THEORY T)))

(PROVE-LEMMA EQUALITY-OF-GETSEG-BACKCHAIN-PROOF NIL
             (IMPLIES (AND (