#|

 Copyright (C) 1994 by J Strother Moore.  All Rights Reserved.

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

 NO WARRANTY

 J Strother Moore 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 J Strother Moore 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.''

|#

(BOOT-STRAP NQTHM)
(COMPILE-UNCOMPILED-DEFNS "tmp")
(ADD-SHELL ZN NIL ZNP ((POS (ONE-OF NUMBERP)
                            ZERO)
                       (NEG (ONE-OF NUMBERP)
                            ZERO)))
(DEFN ZLESSP (X Y)
  (LESSP (PLUS (POS X)
               (NEG Y))
         (PLUS (NEG X)
               (POS Y))))
(DEFN ZLESSEQP (X Y)
  (NOT (ZLESSP Y X)))
(DEFN ZMAX (X Y)
  (IF (ZLESSP X Y)
      Y X))
(DEFN ZMIN (X Y)
  (IF (ZLESSP X Y)
      X Y))
(DEFN ZSUB1 (X)
  (ZN (POS X)
      (ADD1 (NEG X))))
(DEFN PZDIFFERENCE (X Y)
  (DIFFERENCE (PLUS (POS X)
                    (NEG Y))
              (PLUS (NEG X)
                    (POS Y))))
(DEFN M1 (X Y Z)
  (IF (ZLESSEQP X Y)
      0 1))
(DEFN M2 (X Y Z)
  (PZDIFFERENCE (ZMAX X (ZMAX Y Z))
                (ZMIN X (ZMIN Y Z))))
(DEFN M3 (X Y Z)
  (PZDIFFERENCE X (ZMIN X (ZMIN Y Z))))
(DEFN TAK0 (X Y Z)
  (IF (ZLESSEQP X Y)
      Y
      (IF (ZLESSEQP Y Z)
          Z X)))
(DEFN M (X Y Z)
  (CONS (M1 X Y Z)
        (CONS (M2 X Y Z)
              (CONS (M3 X Y Z)
                    NIL))))
(PROVE-LEMMA TAK0-SATISFIES-TAK-EQUATION NIL
             (EQUAL (TAK0 X Y Z)
                    (IF (ZLESSEQP X Y)
                        Y
                        (TAK0 (TAK0 (ZSUB1 X)
                                    Y Z)
                              (TAK0 (ZSUB1 Y)
                                    Z X)
                              (TAK0 (ZSUB1 Z)
                                    X Y)))))
(PROVE-LEMMA M1-LESSEQP-0 (REWRITE)
             (IMPLIES (NOT (ZLESSEQP X Y))
                      (NOT (LESSP (M1 X Y Z)
                                  (M1 (TAK0 (ZSUB1 X)
                                            Y Z)
                                      (TAK0 (ZSUB1 Y)
                                            Z X)
                                      (TAK0 (ZSUB1 Z)
                                            X Y))))))
(PROVE-LEMMA M1-LESSEQP-1 (REWRITE)
             (IMPLIES (NOT (ZLESSEQP X Y))
                      (NOT (LESSP (M1 X Y Z)
                                  (M1 (ZSUB1 X)
                                      Y Z)))))
(PROVE-LEMMA M1-LESSEQP-2 (REWRITE)
             (IMPLIES (NOT (ZLESSEQP X Y))
                      (NOT (LESSP (M1 X Y Z)
                                  (M1 (ZSUB1 Y)
                                      Z X)))))
(PROVE-LEMMA M1-LESSEQP-3 (REWRITE)
             (IMPLIES (NOT (ZLESSEQP X Y))
                      (NOT (LESSP (M1 X Y Z)
                                  (M1 (ZSUB1 Z)
                                      X Y)))))
(PROVE-LEMMA M2-LESSEQP-0 (REWRITE)
             (IMPLIES (NOT (ZLESSEQP X Y))
                      (NOT (LESSP (M2 X Y Z)
                                  (M2 (TAK0 (ZSUB1 X)
                                            Y Z)
                                      (TAK0 (ZSUB1 Y)
                                            Z X)
                                      (TAK0 (ZSUB1 Z)
                                            X Y))))))
(PROVE-LEMMA M2-LESSEQP-1 (REWRITE)
             (IMPLIES (NOT (ZLESSEQP X Y))
                      (NOT (LESSP (M2 X Y Z)
                                  (M2 (ZSUB1 X)
                                      Y Z)))))
(PROVE-LEMMA M2-LESSEQP-2 (REWRITE)
             (IMPLIES (AND (NOT (ZLESSEQP X Y))
                           (EQUAL (M1 (ZSUB1 Y)
                                      Z X)
                                  (M1 X Y Z)))
                      (NOT (LESSP (M2 X Y Z)
                                  (M2 (ZSUB1 Y)
                                      Z X)))))
(PROVE-LEMMA M2-LESSEQP-3 (REWRITE)
             (IMPLIES (AND (NOT (ZLESSEQP X Y))
                           (EQUAL (M1 (ZSUB1 Z)
                                      X Y)
                                  (M1 X Y Z)))
                      (NOT (LESSP (M2 X Y Z)
                                  (M2 (ZSUB1 Z)
                                      X Y)))))
(PROVE-LEMMA M3-LESSP-0 (REWRITE)
             (IMPLIES (AND (NOT (ZLESSEQP X Y))
                           (EQUAL (M1 (TAK0 (ZSUB1 X)
                                            Y Z)
                                      (TAK0 (ZSUB1 Y)
                                            Z X)
                                      (TAK0 (ZSUB1 Z)
                                            X Y))
                                  (M1 X Y Z)))
                      (LESSP (M3 (TAK0 (ZSUB1 X)
                                       Y Z)
                                 (TAK0 (ZSUB1 Y)
                                       Z X)
                                 (TAK0 (ZSUB1 Z)
                                       X Y))
                             (M3 X Y Z))))
(PROVE-LEMMA M3-LESSP-1 (REWRITE)
             (IMPLIES (AND (NOT (ZLESSEQP X Y))
                           (EQUAL (M1 (ZSUB1 X)
                                      Y Z)
                                  (M1 X Y Z)))
                      (LESSP (M3 (ZSUB1 X)
                                 Y Z)
                             (M3 X Y Z))))
(PROVE-LEMMA M3-LESSP-2 (REWRITE)
             (IMPLIES (AND (NOT (ZLESSEQP X Y))
                           (EQUAL (M1 (ZSUB1 Y)
                                      Z X)
                                  (M1 X Y Z)))
                      (LESSP (M3 (ZSUB1 Y)
                                 Z X)
                             (M3 X Y Z))))
(PROVE-LEMMA M3-LESSP-3 (REWRITE)
             (IMPLIES (AND (NOT (ZLESSEQP X Y))
                           (EQUAL (M1 (ZSUB1 Z)
                                      X Y)
                                  (M1 X Y Z)))
                      (LESSP (M2 (ZSUB1 Z)
                                 X Y)
                             (M2 X Y Z))))
(DISABLE ZLESSP)
(DISABLE M1)
(DISABLE M2)
(DISABLE M3)
(DISABLE TAK0)
(DISABLE ZSUB1)

(DEFN MAKE-ORDINAL3 (X)
  (CONS (CONS (ADD1 (CAR X)) 0)
        (CONS (ADD1 (CADR X))
              (FIX (CADDR X)))))
(PROVE-LEMMA ORDINALP-MAKE-ORDINAL3 NIL (ORDINALP (MAKE-ORDINAL3 X)))
(DEFN LEX3 (X Y)
  (ORD-LESSP (MAKE-ORDINAL3 X) (MAKE-ORDINAL3 Y)))
(PROVE-LEMMA M-GOES-DOWN-1 NIL
             (IMPLIES (NOT (ZLESSEQP X Y))
                      (LEX3 (M (ZSUB1 X)
                               Y Z)
                            (M X Y Z))))
(PROVE-LEMMA M-GOES-DOWN-2 NIL
             (IMPLIES (NOT (ZLESSEQP X Y))
                      (LEX3 (M (ZSUB1 Y)
                               Z X)
                            (M X Y Z))))
(PROVE-LEMMA M-GOES-DOWN-3 NIL
             (IMPLIES (NOT (ZLESSEQP X Y))
                      (LEX3 (M (ZSUB1 Z)
                               X Y)
                            (M X Y Z))))
(PROVE-LEMMA M-GOES-DOWN-0 NIL
             (IMPLIES (NOT (ZLESSEQP X Y))
                      (LEX3 (M (TAK0 (ZSUB1 X)
                                     Y Z)
                               (TAK0 (ZSUB1 Y)
                                     Z X)
                               (TAK0 (ZSUB1 Z)
                                     X Y))
                            (M X Y Z)))
             NIL)