#|
 Copyright (C) 1994 by Computational Logic, Inc.  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) 1994 by Computational Logic, Inc.  All
 Rights Reserved."

 NO WARRANTY

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

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


             A Formal Model of Asynchronous Communication
                                 and
      Its Use in Mechanically Verifying a Biphase Mark Protocol


                           J Strother Moore

                         Technical Report 68
                             August, 1991

Abstract (of CLI Tech Report 68):

  In this paper we present a formal model of asynchronous
  communication as a function in the Boyer-Moore logic.  The
  function transforms the signal stream generated by one
  processor into the signal stream consumed by an independently
  clocked processor.  This transformation ``blurs'' edges and
  ``dilates'' time due to differences in the phases and rates of
  the two clocks and the communications delay.  The model can be
  used quantitatively to derive concrete performance bounds on
  asynchronous communications at ISO protocol level 1 (physical
  level).  We develop part of the reusable formal theory that
  permits the convenient application of the model.  We use the
  theory to show that a biphase mark protocol can be used to send
  messages of arbitrary length between two asynchronous
  processors.  We study two versions of the protocol, a
  conventional one which uses cells of size 32 cycles and an
  unconventional one which uses cells of size 18.  Our proof of
  the former protocol requires the ratio of the clock rates of
  the two processors to be within 3% of unity.  The
  unconventional biphase mark protocol permits the ratio to vary
  by 5%.  At nominal clock rates of 20MHz, the unconventional
  protocol allows transmissions at a burst rate of slightly over
  1MHz.  These claims are formally stated in terms of our model
  of asynchrony; the proofs of the claims have been mechanically
  checked with the Boyer-Moore theorem prover, NQTHM.  We
  conjecture that the protocol can be proved to work under our
  model for smaller cell sizes and more divergent clock rates but
  the proofs would be harder.  Known inadequacies of our model
  include that (a) distortion due to the presence of an edge is
  limited to the time span of the cycle during which the edge was
  written, (b) both clocks are assumed to be linear functions of
  time (i.e., the rate of a given clock is unwavering) and (c)
  reading ``on an edge'' produces a nondeterministically defined
  value rather than an indeterminate value.  We discuss these
  problems.

This event file contains all of the definitions and theorems mentioned
in CLI Tech Report 68.  In addition, it contains our proof that
``deterministic fuzzy edge detection is impossible,'' which is
mentioned in a footnote of the report.  However, the theorem BMP18 of
the paper is here called TOP and BMP18-LEMMA is here LOOP.  In
addition, the functions lst' and ts' of the paper are here named LST+
and TS+.

This proof deals with the case of an 18-bit cell divided into 
subcells of size 5 and 13.  The following numeric constants, which
occur in this file, are related to this particular choice of cell
configuration.  It is possible to obtain proofs of different 
configurations by consistently replacing these constants and replaying
the script.  The proof could be lifted to a much more general one,
but I just didn't feel like doing it.

 5 = mark-size
13 = code-size
18 = cell-size = (mark-size + code-size)
17 = cell-size-1
19 = cell-size+1
10 = sampling distance = mark-size+(code-size/2)-1
 4 = mark-size-1
12 = code-size-1

|#

; -------------------------------------------------------------------------
; Arithmetic

(boot-strap nqthm)

(defn rate-proximity (w r)
  (and (not (lessp (times 18 w) (times 17 r)))
       (not (lessp (times 19 r) (times 18 w)))))

(PROVE-LEMMA PLUS-ADD1
             (REWRITE)
             (EQUAL (PLUS X (ADD1 Y))
                    (ADD1 (PLUS X Y))))

(PROVE-LEMMA PLUS-COMMUTES1
             (REWRITE)
             (EQUAL (PLUS X Y) (PLUS Y X)))

(PROVE-LEMMA PLUS-COMMUTES2
             (REWRITE)
             (EQUAL (PLUS X Y Z) (PLUS Y X Z)))

(PROVE-LEMMA PLUS-ASSOCIATES
             (REWRITE)
             (EQUAL (PLUS (PLUS X Y) Z)
                    (PLUS X Y Z)))

(PROVE-LEMMA TIMES-0
             (REWRITE)
             (EQUAL (TIMES X 0) 0))

(PROVE-LEMMA TIMES-NON-NUMBERP
             (REWRITE)
             (IMPLIES (NOT (NUMBERP Z))
                      (EQUAL (TIMES X Z) 0)))

(PROVE-LEMMA TIMES-ADD1
             (REWRITE)
             (EQUAL (TIMES X (ADD1 Y))
                    (PLUS X (TIMES X Y))))

(PROVE-LEMMA TIMES-DISTRIBUTES1
             (REWRITE)
             (EQUAL (TIMES X (PLUS Y Z))
                    (PLUS (TIMES X Y) (TIMES X Z))))

(PROVE-LEMMA TIMES-COMMUTES1
             (REWRITE)
             (EQUAL (TIMES X Y) (TIMES Y X)))

(PROVE-LEMMA TIMES-COMMUTES2
             (REWRITE)
             (EQUAL (TIMES X Y Z) (TIMES Y X Z)))

(PROVE-LEMMA TIMES-ASSOCIATES
             (REWRITE)
             (EQUAL (TIMES (TIMES X Y) Z)
                    (TIMES X Y Z)))

(PROVE-LEMMA TIMES-DISTRIBUTES2
             (REWRITE)
             (EQUAL (TIMES (PLUS X Y) Z)
                    (PLUS (TIMES X Z) (TIMES Y Z))))

(PROVE-LEMMA DIFFERENCE-IS-0
             (REWRITE)
             (IMPLIES (NOT (LESSP Y X))
                      (EQUAL (DIFFERENCE X Y) 0)))

(PROVE-LEMMA DIFFERENCE-PLUS-CANCELLATION1
             (REWRITE)
             (EQUAL (DIFFERENCE (PLUS I X) I)
                    (FIX X)))

(PROVE-LEMMA DIFFERENCE-PLUS-CANCELLATION2
             (REWRITE)
             (EQUAL (DIFFERENCE (PLUS I X) (PLUS I Y))
                    (DIFFERENCE X Y)))

(PROVE-LEMMA DIFFERENCE-PLUS-CANCELLATION3
             (REWRITE)
             (EQUAL (DIFFERENCE (PLUS I J X) J)
                    (PLUS I X)))

(PROVE-LEMMA LESSP-REMAINDER
             (GENERALIZE)
             (EQUAL (LESSP (REMAINDER X Y) Y)
                    (NOT (ZEROP Y))))

(PROVE-LEMMA REMAINDER-QUOTIENT-ELIM
             (ELIM REWRITE)
             (IMPLIES (NUMBERP X)
                      (EQUAL (PLUS (REMAINDER X Y)
                                   (TIMES Y (QUOTIENT X Y)))
                             X)))

(PROVE-LEMMA QUOTIENT-PLUS-TIMES
             (REWRITE)
             (IMPLIES (NOT (ZEROP W))
                      (EQUAL (QUOTIENT (PLUS V (TIMES W I)) W)
                             (PLUS I (QUOTIENT V W))))
             ((INDUCT (TIMES I W))))

(defn len (x)
  (if (nlistp x) 0 (add1 (len (cdr x)))))

(PROVE-LEMMA EQUAL-LEN-0
             (REWRITE)
             (EQUAL (EQUAL (LEN X) 0)
                    (NLISTP X)))

(defn app (x y)
  (if (nlistp x)
      y
      (cons (car x) (app (cdr x) y))))

(PROVE-LEMMA APP-CANCELLATION
             (REWRITE)
             (EQUAL (EQUAL (APP A B) (APP A C))
                    (EQUAL B C)))

(prove-lemma app-assoc (rewrite)
  (equal (app (app a b) c) (app a (app b c))))

(prove-lemma len-app (rewrite)
  (equal (len (app a b)) (plus (len a) (len b))))


(PROVE-LEMMA QUOTIENT-X-X
             (REWRITE)
             (IMPLIES (NOT (ZEROP X))
                      (EQUAL (QUOTIENT X X) 1)))

(PROVE-LEMMA NOT-LESSP-TIMES-QUOTIENT
             (REWRITE)
             (NOT (LESSP N (TIMES W (QUOTIENT N W)))))

(PROVE-LEMMA TIMES-MONOTONIC
             (REWRITE)
             (IMPLIES (AND (NOT (ZEROP W)) (LESSP A B))
                      (LESSP (TIMES W A) (TIMES W B))))

(PROVE-LEMMA DIFFERENCE-PLUS
             (REWRITE)
             (EQUAL (DIFFERENCE (PLUS X Y) Y)
                    (FIX X)))

(PROVE-LEMMA NSIG*-ALG-LEMMA-HACK1
             (REWRITE)
             (IMPLIES (AND (LESSP N (QUOTIENT (PLUS R X) W))
                           (NUMBERP W)
                           (NOT (EQUAL W 0)))
                      (EQUAL (LESSP (PLUS TS (TIMES N W))
                                    (PLUS R TS X))
                             T))
             ((DISABLE TIMES-MONOTONIC)
              (USE (TIMES-MONOTONIC (A N)
                                    (B (QUOTIENT (PLUS R X) W))))))

(PROVE-LEMMA DIFFERENCE-PLUS-CANCELLATION-4
             (REWRITE)
             (EQUAL (DIFFERENCE (PLUS R TS X) (PLUS TS Y))
                    (DIFFERENCE (PLUS R X) Y)))

(PROVE-LEMMA NTS*-ALG-LEMMA2-HACK1
 (REWRITE)
 (IMPLIES
      (AND (LESSP N (QUOTIENT (PLUS R X) W))
           (NUMBERP X)
           (NOT (EQUAL R 0))
           (NUMBERP R)
           (NOT (LESSP (TIMES N W) (PLUS R X)))
           (NUMBERP N)
           (NOT (EQUAL W 0))
           (NUMBERP W)
           (LESSP X W))
      (EQUAL (EQUAL (QUOTIENT (PLUS R X) W)
                    (QUOTIENT (PLUS X
                                    (TIMES R
                                           (QUOTIENT (DIFFERENCE (TIMES N W) X)
                                                     R)))
                              W))
             T))
 ((DISABLE TIMES-MONOTONIC)
  (USE (TIMES-MONOTONIC (A N)
                        (B (QUOTIENT (PLUS R X) W))
                        (W W)))))

(PROVE-LEMMA TIMES-CANCELLATION1
             (REWRITE)
             (IMPLIES (NOT (ZEROP I))
                      (EQUAL (EQUAL (TIMES I J) (TIMES I K))
                             (EQUAL (FIX J) (FIX K))))
             ((INDUCT (LESSP J K))))

(PROVE-LEMMA TIMES-CANCELLATION2
             (REWRITE)
             (IMPLIES (NOT (ZEROP W))
                      (EQUAL (EQUAL (PLUS (TIMES W X) (TIMES W Y))
                                    (TIMES W Z))
                             (EQUAL (PLUS X Y) (FIX Z))))
             ((DISABLE TIMES-CANCELLATION1)
              (USE (TIMES-CANCELLATION1 (I W)
                                        (J (PLUS X Y))
                                        (K Z)))))

(PROVE-LEMMA DIFFERENCE-DIFFERENCE
             (REWRITE)
             (IMPLIES (NOT (LESSP B C))
                      (EQUAL (DIFFERENCE A (DIFFERENCE B C))
                             (DIFFERENCE (PLUS A C) B))))

(PROVE-LEMMA DIFFERENCE-DIFFERENCE-OTHER
             (REWRITE)
             (EQUAL (DIFFERENCE (DIFFERENCE A B) C)
                    (DIFFERENCE A (PLUS B C))))

(PROVE-LEMMA QUOTIENT-PLUS-TIMES2
             (REWRITE)
             (IMPLIES (NOT (ZEROP W))
                      (EQUAL (QUOTIENT (PLUS V (TIMES I W) (TIMES W J))
                                       W)
                             (PLUS I J (QUOTIENT V W))))
             ((DISABLE QUOTIENT-PLUS-TIMES)
              (USE (QUOTIENT-PLUS-TIMES (I (PLUS I J))))))

(prove-lemma difference-elim (elim)
  (implies (and (numberp i)
                (not (lessp i j)))
           (equal (plus j (difference i j)) i)))

(PROVE-LEMMA QUOTIENT-DIFFERENCE
             (REWRITE)
             (IMPLIES (AND (NOT (ZEROP W))
                           (NOT (LESSP A (TIMES W B))))
                      (EQUAL (QUOTIENT (DIFFERENCE A (TIMES W B))
                                       W)
                             (DIFFERENCE (QUOTIENT A W) B))))

(PROVE-LEMMA QUOTIENT-MONOTONIC-LEMMA
             (REWRITE)
             (IMPLIES (AND (LESSP Z1 Y)
                           (LESSP Z2 Y)
                           (NOT (EQUAL Y 0))
                           (NUMBERP Y)
                           (LESSP X V))
                      (EQUAL (LESSP (PLUS Z1 (TIMES Y X))
                                    (PLUS Z2 (TIMES V Y)))
                             T))
             ((INDUCT (LESSP X V))))

(PROVE-LEMMA NTR*-ALG-LEMMA2-HACK1
       (REWRITE)
       (IMPLIES (AND (LESSP N (QUOTIENT (PLUS R X) W))
                     (NUMBERP X)
                     (NOT (EQUAL R 0))
                     (NUMBERP R)
                     (NOT (LESSP (PLUS TS (TIMES N W))
                                 (PLUS R TS X)))
                     (NUMBERP N)
                     (NUMBERP TS)
                     (NOT (EQUAL W 0))
                     (NUMBERP W)
                     (NOT (LESSP (PLUS TS X) TS))
                     (LESSP (PLUS TS X) (PLUS TS W)))
                (EQUAL (EQUAL (PLUS R TS X)
                              (PLUS TS X
                                    (TIMES R
                                           (QUOTIENT (DIFFERENCE (TIMES N W) X)
                                                     R))))
                       T))
       ((DISABLE TIMES-MONOTONIC)
        (USE (TIMES-MONOTONIC (A N)
                              (B (QUOTIENT (PLUS R X) W))
                              (W W)))))

(PROVE-LEMMA NOT-LESSP-TIMES-QUOTIENT-OTHER
             (REWRITE)
             (IMPLIES (NOT (LESSP X R))
                      (NOT (LESSP (TIMES R (QUOTIENT X R)) R))))

(PROVE-LEMMA QUOTIENT-MONOTONIC
             (REWRITE)
             (IMPLIES (AND (NOT (ZEROP W))
                           (NOT (LESSP A B)))
                      (EQUAL (LESSP (QUOTIENT A W) (QUOTIENT B W))
                             F)))

(PROVE-LEMMA NLST*-ALG-LEMMA2-HACK1
 (REWRITE)
 (IMPLIES
  (AND (NUMBERP X)
       (NOT (EQUAL R 0))
       (NUMBERP R)
       (NOT (LESSP (PLUS TS (TIMES N W))
                   (PLUS R TS X)))
       (NUMBERP N)
       (NUMBERP TS)
       (NOT (EQUAL W 0))
       (NUMBERP W)
       (NOT (LESSP (PLUS TS X) TS))
       (LESSP (PLUS TS X) (PLUS TS W)))
  (EQUAL
   (PLUS
        (QUOTIENT (PLUS R X) W)
        (QUOTIENT (DIFFERENCE (PLUS X
                                    (TIMES R
                                           (QUOTIENT (DIFFERENCE (TIMES N W) X)
                                                     R)))
                              (TIMES W (QUOTIENT (PLUS R X) W)))
                  W))
   (QUOTIENT (PLUS X
                   (TIMES R
                          (QUOTIENT (DIFFERENCE (TIMES N W) X)
                                    R)))
             W)))
 ((DISABLE QUOTIENT-DIFFERENCE)
  (USE
      (QUOTIENT-DIFFERENCE (W W)
                           (A (PLUS X
                                    (TIMES R
                                           (QUOTIENT (DIFFERENCE (TIMES N W) X)
                                                     R))))
                           (B (QUOTIENT (PLUS R X) W))))))

(PROVE-LEMMA NSIG*-UPPER-BOUND-LEMMA1
             (REWRITE)
             (IMPLIES (NOT (ZEROP R))
                      (NOT (LESSP (QUOTIENT (TIMES N W) R)
                                  (QUOTIENT (DIFFERENCE (TIMES N W)
                                                        (DIFFERENCE TR TS))
                                            R)))))

(PROVE-LEMMA QUOTIENT-TIMES
             (REWRITE)
             (IMPLIES (NOT (ZEROP R))
                      (EQUAL (QUOTIENT (TIMES N R) R)
                             (FIX N)))
             ((DISABLE QUOTIENT-PLUS-TIMES)
              (USE (QUOTIENT-PLUS-TIMES (W R)
                                        (V 0)
                                        (I N)))))

(PROVE-LEMMA MULTIPLY-BOTH-SIDES-OF-LESSP
             (REWRITE)
             (IMPLIES (NOT (ZEROP R))
                      (EQUAL (LESSP (TIMES A R) (TIMES B R))
                             (LESSP A B))))

(PROVE-LEMMA LESSP-QUOTIENT-TO-LESSP-TIMES-LEMMA1 NIL
             (IMPLIES (AND (NOT (ZEROP R))
                           (NOT (LESSP (QUOTIENT X R) N)))
                      (NOT (LESSP X (TIMES N R))))
             ((DISABLE MULTIPLY-BOTH-SIDES-OF-LESSP)
              (USE (MULTIPLY-BOTH-SIDES-OF-LESSP (A (QUOTIENT X R))
                                                 (B N)))))

(PROVE-LEMMA LESSP-QUOTIENT-TO-LESSP-TIMES-LEMMA2 NIL
             (IMPLIES (AND (NOT (ZEROP R))
                           (NOT (LESSP X (TIMES N R))))
                      (NOT (LESSP (QUOTIENT X R) N)))
             ((DISABLE QUOTIENT-MONOTONIC)
              (USE (QUOTIENT-MONOTONIC (A X)
                                       (B (TIMES N R))
                                       (W R)))))

(PROVE-LEMMA LESSP-QUOTIENT-TO-LESSP-TIMES
             (REWRITE)
             (IMPLIES (NOT (ZEROP R))
                      (EQUAL (LESSP (QUOTIENT X R) N)
                             (LESSP X (TIMES N R))))
             ((USE (LESSP-QUOTIENT-TO-LESSP-TIMES-LEMMA1)
                   (LESSP-QUOTIENT-TO-LESSP-TIMES-LEMMA2))))

(PROVE-LEMMA QUOTIENT-PLUS-TIMES1
             (REWRITE)
             (IMPLIES (NOT (ZEROP R))
                      (EQUAL (QUOTIENT (PLUS (TIMES N R) Z) R)
                             (PLUS N (QUOTIENT Z R))))
             ((DISABLE QUOTIENT-PLUS-TIMES)
              (USE (QUOTIENT-PLUS-TIMES (V Z)
                                        (I N)
                                        (W R)))))

(PROVE-LEMMA EQUAL-TIMES-0
             (REWRITE)
             (EQUAL (EQUAL (TIMES I J) 0)
                    (OR (ZEROP I) (ZEROP J))))

(PROVE-LEMMA NSIG*-UPPER-BOUND-HACK1
             (REWRITE)
             (IMPLIES (AND (NOT (ZEROP R))
                           (NOT (LESSP R (TIMES 18 DELTA)))
                           (LESSP N 18))
                      (EQUAL (LESSP (TIMES N DELTA) R) T)))

(PROVE-LEMMA NSIG*-UPPER-BOUND-HACK2
           (REWRITE)
           (IMPLIES (AND (NOT (LESSP (PLUS R R (TIMES 17 R))
                                     (PLUS W (TIMES 17 W))))
                         (NOT (LESSP (PLUS W (TIMES 17 W))
                                     (TIMES 17 R)))
                         (NOT (ZEROP W))
                         (NOT (ZEROP R))
                         (NOT (ZEROP N))
                         (LESSP N 18)
                         (LESSP W R))
                    (EQUAL (PLUS W (TIMES W (SUB1 N)))
                           (PLUS (TIMES (SUB1 N) (DIFFERENCE R W))
                                 (DIFFERENCE W
                                             (TIMES (SUB1 N) (DIFFERENCE R W)))
                                 (TIMES W (SUB1 N))))))

(PROVE-LEMMA QUOTIENT-PLUS-TIMES3
             (REWRITE)
             (IMPLIES (NOT (ZEROP (PLUS X Z (TIMES X N))))
                      (EQUAL (QUOTIENT (PLUS Z
                                             (TIMES X N)
                                             (TIMES Z N)
                                             (TIMES X N N))
                                       (PLUS X Z (TIMES X N)))
                             (PLUS N
                                   (QUOTIENT Z (PLUS X Z (TIMES N X))))))
             ((DISABLE QUOTIENT-PLUS-TIMES)
              (USE (QUOTIENT-PLUS-TIMES (V Z)
                                        (W (PLUS X Z (TIMES X N)))
                                        (I N)))))

(PROVE-LEMMA NSIG*-UPPER-BOUND-HACK3
             (REWRITE)
             (IMPLIES (LESSP (PLUS Z (TIMES X (SUB1 N)))
                             (PLUS X Z (TIMES X (SUB1 N))))
                      (EQUAL (LESSP Z
                                    (PLUS X Z (TIMES X (SUB1 N))))
                             T)))

(PROVE-LEMMA INTRO-DELTA NIL
             (IMPLIES (AND (NUMBERP W) (NOT (LESSP W R)))
                      (EQUAL W (PLUS R (DIFFERENCE W R)))))

(PROVE-LEMMA NSIG*-UPPER-BOUND-LEMMA2-1 NIL
             (IMPLIES (AND (NUMBERP N)
                           (NOT (ZEROP W))
                           (NOT (ZEROP R))
                           (RATE-PROXIMITY W R)
                           (LESSP N 18)
                           (NOT (LESSP W R)))
                      (EQUAL (QUOTIENT (TIMES N W) R) N))
             ((USE (INTRO-DELTA))))

(PROVE-LEMMA NSIG*-UPPER-BOUND-LEMMA2-2 NIL
             (IMPLIES (AND (NUMBERP N)
                           (NOT (ZEROP W))
                           (NOT (ZEROP R))
                           (RATE-PROXIMITY W R)
                           (LESSP N 18)
                           (LESSP W R))
                      (EQUAL (QUOTIENT (TIMES N W) R)
                             (SUB1 N)))
             ((EXPAND (TIMES N W))))

(PROVE-LEMMA NSIG*-UPPER-BOUND-LEMMA2-EQUALITY
             (REWRITE)
             (IMPLIES (AND (NUMBERP N)
                           (NOT (ZEROP W))
                           (NOT (ZEROP R))
                           (RATE-PROXIMITY W R)
                           (LESSP N 18))
                      (EQUAL (QUOTIENT (TIMES N W) R)
                             (IF (LESSP W R) (SUB1 N) N)))
             ((DISABLE TIMES)
              (USE (NSIG*-UPPER-BOUND-LEMMA2-1)
                   (NSIG*-UPPER-BOUND-LEMMA2-2))))

(PROVE-LEMMA NSIG*-UPPER-BOUND-LEMMA2
             (REWRITE)
             (IMPLIES (AND (NUMBERP N)
                           (NOT (ZEROP W))
                           (NOT (ZEROP R))
                           (RATE-PROXIMITY W R)
                           (LESSP N 18))
                      (NOT (LESSP N (QUOTIENT (TIMES N W) R)))))

(PROVE-LEMMA NSIG*-LOWER-BOUND-LEMMA1
             (REWRITE)
             (IMPLIES (AND (NOT (ZEROP R))
                           (NOT (LESSP W TR-TS)))
                      (NOT (LESSP (QUOTIENT (DIFFERENCE (TIMES N W) TR-TS)
                                            R)
                                  (QUOTIENT (TIMES (SUB1 N) W) R)))))

(PROVE-LEMMA LESSP-TIMES
             (REWRITE)
             (IMPLIES (NOT (ZEROP N))
                      (NOT (LESSP (TIMES N W) W))))

(PROVE-LEMMA PLUS-CANCELLATION
             (REWRITE)
             (EQUAL (EQUAL (PLUS I J) (PLUS I K))
                    (EQUAL (FIX J) (FIX K))))

(defn boolp (x)
  (or (equal x t) (equal x f)))

(disable boolp)

(PROVE-LEMMA BOOLP-T
             (REWRITE)
             (IMPLIES (AND (BOOLP X) X)
                      (EQUAL (EQUAL T X) T))
             ((ENABLE BOOLP)))


(defn b-not (x) (not x))

(disable b-not)

(defn b-xor (x y)
  (if x (not y) (if y t f)))

(disable b-xor)

(prove-lemma b-xor-b-not (rewrite)
  (and (b-xor x (b-not x))
       (b-xor (b-not x) x))
  ((enable b-xor b-not)))

(defn smooth (prev-val lst)
  (if (nlistp lst)
      nil
      (if (b-xor prev-val (car lst))
          (cons 'q (smooth (car lst) (cdr lst)))
          (cons (car lst) (smooth (car lst) (cdr lst))))))

(defn reconcile-signals (a b)
  (if (equal a b) a 'q))

(defn sig (lst ts tr w)
  (if (nlistp lst)
      'q
      (if (lessp (plus ts w) tr)
          (reconcile-signals (car lst)
                             (sig (cdr lst) (plus ts w) tr w))
          (car lst))))

(defn endp (lst ts tr w)
  (if (nlistp lst)
      t
      (if (lessp (plus ts w) tr)
          (endp (cdr lst) (plus ts w) tr w)
          f)))

(defn lst+ (lst ts nxtr w)
  (if (nlistp lst)
      lst
      (if (lessp nxtr (plus ts w))
          lst
          (lst+ (cdr lst) (plus ts w) nxtr w))))

(defn ts+ (lst ts nxtr w)
  (if (nlistp lst)
      ts
      (if (lessp nxtr (plus ts w))
          ts
          (ts+ (cdr lst) (plus ts w) nxtr w))))

(prove-lemma lst+-weakly-shortens-lst (rewrite)
  (not (lessp (count lst)
              (count (lst+ lst ts tr w)))))

(prove-lemma ts+-increases-tr (rewrite)
  (implies (and (not (endp lst ts (plus r tr) w))
                (not (zerop r))
                (equal (count lst)
                       (count (lst+ lst ts (plus r tr) w))))
           (equal
            (lessp (difference (plus w (ts+ lst ts (plus r tr) w))
                               (plus r tr))
                   (difference (plus ts w)
                               tr))
            t))
  ((expand (lst+ lst ts (plus r tr) w)
           (ts+ lst ts (plus r tr) w))))

(defn warp (lst ts tr w r)
  (if (or (zerop r)
          (endp lst ts (plus tr r) w))
      nil
      (cons (sig lst ts (plus tr r) w)
            (warp (lst+ lst ts (plus tr r) w)
                  (ts+ lst ts (plus tr r) w)
                  (plus tr r)
                  w r)))
  ((ord-lessp (cons (cons (add1 (count lst)) 0)
                    (difference (plus ts w) tr)))))

(defn det (lst oracle)
  (if (nlistp lst)
      lst
      (if (equal (car lst) 'q)
          (cons (if (car oracle) t f) (det (cdr lst) (cdr oracle)))
          (cons (car lst) (det (cdr lst) oracle)))))

(defn async (lst ts tr w r oracle)
  (det (warp (smooth t lst) ts tr w r)
       oracle))

(defn listn (n value)
  (if (zerop n)
      nil
      (cons value
            (listn (sub1 n) value))))

(defn csig (prev-signal bit)
; CSIG stands for "contents signal"
  (if bit prev-signal (b-not prev-signal)))

(defn cell (prev-signal n1 n2 bit)
  (app (listn n1 (b-not prev-signal))
       (listn n2 (csig prev-signal bit))))

(defn cells (prev-signal n1 n2 msg)
  (if (nlistp msg)
      nil
      (app (cell prev-signal n1 n2 (car msg))
           (cells (csig prev-signal (car msg)) n1 n2 (cdr msg)))))

(defn send (msg pad1 n1 n2 pad2)
  (app (listn pad1 t)
       (app (cells t n1 n2 msg)
            (listn pad2 t))))

(defn scan (prev-signal lst)
  (if (nlistp lst)
      nil
      (if (b-xor prev-signal (car lst))
          lst
          (scan prev-signal (cdr lst)))))

(defn cdrn (n lst)
  (if (zerop n) lst (cdrn (sub1 n) (cdr lst))))

(defn nth (n lst)
  (car (cdrn n lst)))

(defn recv-bit (k lst)
  (if (b-xor (car lst) (nth k lst)) t f))

(defn recv (i flg k lst)
  (if (zerop i)
      nil
      (cons (recv-bit k (scan flg lst))
            (recv (sub1 i)
                  (nth k (scan flg lst))
                  k
                  (cdrn k (scan flg lst))))))

(defn bvp (x)
  (if (nlistp x)
      (equal x nil)
      (and (boolp (car x))
           (bvp (cdr x)))))

#|
We can now state the top level theorem without proof.

(prove-lemma top nil
  (implies (and (bvp msg)
                (numberp ts)
                (numberp tr)
                (not (zerop w))
                (not (zerop r))
                (not (lessp tr ts))
                (lessp tr (plus ts w))
                (rate-proximity w r)
                (numberp p1))
           (equal (recv (len msg)
                        t
                        10
                        (async (send msg p1 5 13 p2)
                               ts tr w r oracle))
                  msg)))

We will prove this by first massaging it into a different form,
suitable for induction.  The inductive form shall be called loop
instead of top.

|#
                
(disable listn)
(disable *1*listn)
(disable cell)
(disable *1*cell)
(disable csig)
(disable *1*csig)

(disable boolp)
(disable smooth)
(disable warp)
(disable det)
(disable recv-bit)
(disable scan)
(disable send)

(prove-lemma b-xor-x-x (rewrite)
  (not (b-xor x x))
  ((enable b-xor)))

; Our first goal will be to transform the recv-async-send theorem
; into the form we will prove inductively.  This is done by moving
; the initial header out through the smooth, warp, det, and recv, milking
; a 'q out of the smooth and easing it through the warp to nestle a
; cdrn around the smooth and leaving the det hanging on a q string.

; Because the warping is harder than the smoothing, we'll do it first.


(defn lst* (lst ts tr w r)
  (if (or (zerop r)
          (endp lst ts (plus tr r) w))
      lst
      (lst* (lst+ lst ts (plus tr r) w)
            (ts+ lst ts (plus tr r) w)
            (plus tr r)
            w r))
  ((ord-lessp (cons (cons (add1 (count lst)) 0)
                    (difference (plus ts w) tr)))))

(defn ts* (lst ts tr w r)
  (if (or (zerop r)
          (endp lst ts (plus tr r) w))
      ts
      (ts* (lst+ lst ts (plus tr r) w)
            (ts+ lst ts (plus tr r) w)
            (plus tr r)
            w r))
  ((ord-lessp (cons (cons (add1 (count lst)) 0)
                    (difference (plus ts w) tr)))))

(defn tr* (lst ts tr w r)
  (if (or (zerop r)
          (endp lst ts (plus tr r) w))
      tr
      (tr* (lst+ lst ts (plus tr r) w)
           (ts+ lst ts (plus tr r) w)
           (plus tr r)
           w r))
  ((ord-lessp (cons (cons (add1 (count lst)) 0)
                    (difference (plus ts w) tr)))))

(prove-lemma not-lessp-ts+ (rewrite)
  (implies (and (not (lessp tr ts))
                (not (zerop w)))
           (not (lessp tr (ts+ lst ts tr w)))))

(prove-lemma lessp-ts+ (rewrite)
  (implies (and (not (endp lst ts tr w))
                (not (lessp tr ts))
                (not (zerop w)))
           (lessp tr (plus w (ts+ lst ts tr w)))))

(prove-lemma lst+-app (rewrite)
  (implies (and (not (endp lst1 ts tr+ w))
                (not (zerop w)))
           (equal (lst+ (app lst1 lst2) ts tr+ w)
                  (app (lst+ lst1 ts tr+ w) lst2))))

(prove-lemma ts+-app (rewrite)
  (implies (and (not (endp lst1 ts tr+ w))
                (not (zerop w)))
           (equal (ts+ (app lst1 lst2) ts tr+ w)
                  (ts+ lst1 ts tr+ w))))

(prove-lemma sig-app (rewrite)
  (implies (and (not (endp lst1 ts tr+ w))
                (not (zerop w)))
           (equal (sig (app lst1 lst2) ts tr+ w)
                  (sig lst1 ts tr+ w))))

(prove-lemma endp-app (rewrite)
  (implies (and (not (endp lst1 ts tr+ w))
                (not (zerop w)))
           (not (endp (app lst1 lst2) ts tr+ w))))

(defn target (x) x)
(disable target)

(prove-lemma warp-app (rewrite)
  (implies (and (numberp ts)
                (numberp tr)
                (not (lessp tr ts))
                (lessp tr (plus ts w))
                (not (zerop w))
                (not (zerop r)))
           (equal (target (warp (app lst1 lst2) ts tr w r))
                  (app (warp lst1 ts tr w r)
                       (warp (app (lst* lst1 ts tr w r) lst2)
                             (ts* lst1 ts tr w r)
                             (tr* lst1 ts tr w r)
                             w r))))
  ((enable target warp)))

; The above lemma, when applied, will generate (warp (listn p1 t) ...)
; and (lst* (listn p1 t) ...) which we now simplify.

(defn nlst+ (n ts tr w)
  (if (zerop n)
      n
      (if (lessp tr (plus ts w))
          n
          (nlst+ (sub1 n) (plus ts w) tr w))))

(prove-lemma len-lst+ (rewrite)
  (equal (len (lst+ lst ts tr w))
         (nlst+ (len lst) ts tr w)))

(defn nts+ (n ts tr w)
  (if (zerop n)
      ts
      (if (lessp tr (plus ts w))
          ts
          (nts+ (sub1 n) (plus ts w) tr w))))

(prove-lemma len-ts+ (rewrite)
  (equal (ts+ lst ts tr w)
         (nts+ (len lst) ts tr w)))

(defn nendp (n ts tr w)
  (if (zerop n)
      t
      (if (lessp (plus ts w) tr)
          (nendp (sub1 n) (plus ts w) tr w)
          f)))

(prove-lemma len-endp (rewrite)
  (equal (endp lst ts tr w)
         (nendp (len lst) ts tr w)))

(prove-lemma lessp-nlst+ (rewrite)
  (not (lessp n (nlst+ n ts tr w))))

(prove-lemma nlst+-equal-n (rewrite)
  (equal (equal (nlst+ n ts (plus r tr) w) n)
         (or (zerop n) (lessp (plus r tr) (plus ts w)))))

(defn nlst* (n ts tr w r)
  (if (or (zerop r)
          (nendp n ts (plus tr r) w))
      n
      (nlst* (nlst+ n ts (plus tr r) w)
             (nts+ n ts (plus tr r) w)
             (plus tr r)
             w r))
  ((ord-lessp (cons (cons (add1 n) 0)
                    (difference (plus ts w) tr)))))

(prove-lemma len-lst* (rewrite)
  (equal (len (lst* lst ts tr w r))
         (nlst* (len lst) ts tr w r)))

(defn nts* (n ts tr w r)
  (if (or (zerop r)
          (nendp n ts (plus tr r) w))
      ts
      (nts* (nlst+ n ts (plus tr r) w)
             (nts+ n ts (plus tr r) w)
             (plus tr r)
             w r))
  ((ord-lessp (cons (cons (add1 n) 0)
                    (difference (plus ts w) tr)))))

(prove-lemma len-ts* (rewrite)
  (equal (ts* lst ts tr w r)
         (nts* (len lst) ts tr w r)))

(defn ntr* (n ts tr w r)
  (if (or (zerop r)
          (nendp n ts (plus tr r) w))
      tr
      (ntr* (nlst+ n ts (plus tr r) w)
             (nts+ n ts (plus tr r) w)
             (plus tr r)
             w r))
  ((ord-lessp (cons (cons (add1 n) 0)
                    (difference (plus ts w) tr)))))

(prove-lemma len-tr* (rewrite)
  (equal (tr* lst ts tr w r)
         (ntr* (len lst) ts tr w r)))

(prove-lemma len-listn (rewrite)
  (equal (len (listn n flg)) (fix n))
  ((enable listn)))

(defn lastn (n lst)
  (if (equal n (len lst))
      lst
      (if (nlistp lst)
          lst
          (lastn n (cdr lst)))))

(defn tailp (x lst)
  (if (equal x lst)
      t
      (if (nlistp lst)
          f
          (tailp x (cdr lst)))))

(prove-lemma tailp-transitive (rewrite)
  (implies (and (tailp x y) (tailp y z)) (tailp x z)))

(prove-lemma tailp-lst+ (rewrite)
  (tailp (lst+ lst ts tr w) lst))

(prove-lemma tailp-lst* (rewrite)
  (tailp (lst* lst ts tr w r) lst))

(prove-lemma len-lastn (rewrite)
  (equal (len (lastn n lst))
         (if (lessp (len lst) n)
             0
             (fix n))))

(prove-lemma tailp-implies-lastn-len (rewrite)
  (implies (tailp x y)
           (equal (lastn (len x) y) x)))

(prove-lemma lst*-is-lastn nil
  (equal (lastn (len (lst* lst ts tr w r)) lst)
         (lst* lst ts tr w r))
  ((disable len-lst*)))

(defn properp (x)
  (if (nlistp x)
      (equal x nil)
      (properp (cdr x))))

(prove-lemma lastn-nil (rewrite)
  (implies (and (properp lst)
                (lessp (len lst) n))
           (equal (lastn n lst) nil)))

(prove-lemma properp-listn (rewrite)
  (properp (listn n flg))
  ((enable listn)))

(prove-lemma lastn-listn (rewrite)
  (implies (and (numberp n)
                (numberp k)
                (not (lessp k n)))
           (equal (lastn n (listn k flg))
                  (listn n flg)))
  ((enable listn)
   (induct (listn k flg))))

(prove-lemma lessp-nlst* (rewrite)
  (not (lessp n (nlst* n ts tr w r))))

(prove-lemma lst*-listn (rewrite)
  (implies (numberp n)
           (equal (lst* (listn n flg) ts tr w r)
                  (listn (nlst* n ts tr w r) flg)))
  ((use (lst*-is-lastn (lst (listn n flg))))))

(defn n* (n ts tr w r)
  (if (or (zerop r)
          (nendp n ts (plus tr r) w))
      0
      (add1 (n* (nlst+ n ts (plus tr r) w)
                (nts+ n ts (plus tr r) w)
                (plus tr r)
                w r)))
  ((ord-lessp (cons (cons (add1 n) 0)
                    (difference (plus ts w) tr)))))

(prove-lemma not-lessp-nts+ (rewrite)
  (implies (and (not (lessp tr ts))
                (not (zerop w)))
           (not (lessp tr (nts+ n ts tr w)))))

(prove-lemma lessp-nts+ (rewrite)
  (implies (and (not (nendp n ts tr w))
                (not (lessp tr ts))
                (not (zerop w)))
           (lessp tr
                  (plus w (nts+ n ts tr w)))))

(prove-lemma lst+-listn (rewrite)
  (implies (and (numberp n)
                (not (nendp n ts tr+ w))
                (not (zerop w)))
           (equal (lst+ (listn n flg) ts tr+ w)
                  (listn (nlst+ n ts tr+ w) flg)))
  ((enable listn)))

(prove-lemma sig-listn (rewrite)
  (implies (and (not (equal r 0))
                (numberp r)
                (not (nendp n ts (plus r tr) w))
                (numberp n)
                (numberp ts)
                (numberp tr)
                (not (lessp tr ts))
                (lessp tr (plus ts w))
                (not (equal w 0))
                (numberp w))
           (equal (sig (listn n flg)
                       ts
                       (plus r tr)
                       w)
                  flg))
  ((enable listn)))

(prove-lemma warp-listn (rewrite)
  (implies (and (numberp n)
                (numberp ts)
                (numberp tr)
                (not (lessp tr ts))
                (lessp tr (plus ts w))
                (not (zerop w))
                (not (zerop r)))
           (equal (warp (listn n flg) ts tr w r)
                  (listn (n* n ts tr w r) flg)))
  ((induct (n* n ts tr w r))
   (enable listn)
   (expand (warp (listn n flg) ts tr w r))))  

(prove-lemma lst+-app-gap (rewrite)
  (implies (and (numberp ts)
                (numberp tr+)
                (nendp (len pad) ts tr+ w))
           (equal (lst+ (app pad lst)
                        ts tr+ w)
                  (lst+ lst
                        (plus ts (times (len pad) w))
                        tr+ w)))
  ((induct (endp pad ts tr+ w))))

(prove-lemma nts+-app-gap (rewrite)
  (implies (and (numberp ts)
                (numberp tr+)
                (numberp k)
                (nendp k ts tr+ w))
           (equal (nts+ (plus n k) ts tr+ w)
                  (nts+ n (plus ts (times k w)) tr+ w))))

(prove-lemma warp-app-gap (rewrite)
  (implies (and (numberp ts)
                (not (zerop r))
                (nendp (len pad) ts (plus r tr) w))
           (equal (warp (app pad lst)
                        ts tr w r)
                  (if (nendp (plus (len pad) (len lst))
                             ts
                             (plus r tr)
                             w)
                      nil
                      (cons (sig (app pad lst)
                                 ts
                                 (plus r tr)
                                 w)
                            (warp (lst+ lst
                                        (plus ts (times (len pad) w))
                                        (plus r tr)
                                        w)
                                  (nts+ (len lst)
                                        (plus ts (times (len pad) w))
                                        (plus r tr)
                                        w)
                                  (plus r tr)
                                  w r)))))
  ((expand (warp (app pad lst) ts tr w r))))

(prove-lemma nendp-nlst* (rewrite)
  (implies (and (numberp ts)
                (numberp tr)
                (not (zerop r))
                (not (zerop w))
                (not (lessp tr ts))
                (lessp tr (plus ts w)))
           (nendp (nlst* k ts tr w r)
                  (nts* k ts tr w r)
                  (plus r (ntr* k ts tr w r))
                  w)))

(defn nqg (k ts tr w r)

; Suppose we are at the front of a gap of len k, consisting of identical
; signals.  I.e., (nendp k ts (plus r tr) w) holds and the next k signals
; are all the same.  Suppose the k+1st signal is a 'q and that is followed
; by as many more signals as we wish.  How many q's do we spit out till we
; get past the q we see?  We assume the clock periods are within a factor
; of 2.

 (if (lessp (plus r tr)
            (plus w ts (times w k)))
     (if (lessp (plus r r tr)
                (plus w ts (times w k)))
         3 ; case c
         2) ; case d
     1)) ; case e

#|
(defn dwg (k ts tr w r)

; I have gotten this function wrong more times than I care to admit.
; I won't even try to explain the "logic" behind this defn.

  (let ((ts1 (plus ts (times k w)))
        (ts2 (plus ts w (times k w)))
        (ts3 (plus ts w w (times k w)))
        (tr1 (plus r tr))
        (tr2 (plus r r tr)))
    (cond ((lessp tr1 ts2)
           (if (lessp tr2 ts3) 0 1))
          ((equal tr1 ts2) 0)
          ((and (lessp ts2 tr1) (lessp tr1 ts3)) 0)
          ((lessp tr1 ts3) 0)
          (t 1))))
|#

(defn dwg (k ts tr w r)

; I have gotten this function wrong more times than I care to admit.
; I won't even try to explain the "logic" behind this defn.

  (if (lessp (plus r tr)
             (plus ts w (times k w)))
      (if (lessp (plus r r tr) (plus ts w w (times k w)))
          0
          1)
      (if (equal (plus r tr) (plus ts w (times k w)))
          0
          (if (and (lessp (plus ts w (times k w)) (plus r tr))
                   (lessp (plus r tr) (plus ts w w (times k w))))
              0
              (if (lessp (plus r tr) (plus ts w w (times k w)))
                  0
                  1)))))

(defn tsg (k ts tr w r)

; The value of ts after processing the gap described in nqg.
  
  (plus ts                            ; the header in n1
        (times w k)                   ; the gap of k
        w                             ; the q
        (times w (dwg k ts tr w r)))) ; the eaten element of n2

(defn trg (k ts tr w r)
; The tr value after processing the gap.

  (plus tr                           ; the header in k
        (times r (nqg k ts tr w r)))) ; the qs
        
(prove-lemma not-lessp-ntr*-nts* (rewrite)
  (implies (and (numberp ts)
                (numberp tr)
                (not (lessp tr ts))
                (lessp tr (plus ts w))
                (not (zerop w)))
           (not (lessp (ntr* k ts tr w r) (nts* k ts tr w r)))))

(prove-lemma lessp-ntr*-nts* (rewrite)
  (implies (and (numberp ts)
                (numberp tr)
                (not (lessp tr ts))
                (lessp tr (plus ts w))
                (not (zerop w)))
            (lessp (ntr* k ts tr w r) (plus w (nts* k ts tr w r)))))

(prove-lemma nendp-is-usually-f
             (rewrite)
             (implies (and (numberp ts)
                           (numberp tr)
                           (not (equal w 0))
                           (numberp w)
                           (not (equal r 0))
                           (numberp r)
                           (lessp tr (plus ts w))
                           (lessp w (times 2 r))
                           (lessp r (times 2 w))
                           (lessp 2 k))
                      (not (nendp k ts (plus r tr) w)))
             ((expand (nendp k ts (plus r tr) w)
                      (nendp (sub1 k)
                              (plus ts w)
                              (plus r tr)
                              w)
                      (nendp (sub1 (sub1 k))
                              (plus ts w w)
                              (plus r tr)
                              w))))

; Note: The following is the nts+ analogue of ts+-app.  However the
; rule is a little strange because one naturally would have written
; (nts+ (plus k rest) ...) since k is here the len of the initial
; portion of the list being scanned.  But in my actual application,
; the plus has been commuted so I commute it here.

(prove-lemma lessp-plus-nts*-times-w-nlst*-plus-r-ntr*-lemma (rewrite)
  (implies (and (nendp k ts (plus r tr) w)
                (numberp ts)
                (numberp tr)
                (not (equal w 0))
                (numberp w)
                (not (equal r 0))
                (numberp r)
                (not (lessp (plus r tr) ts))
                (lessp tr (plus ts w)))
           (not (lessp (plus r tr)
                       (plus ts (times k w))))))

(prove-lemma not-lessp-plus-r-ntr*-plus-nts*-times-w-nlst* (rewrite)
  (implies (and (numberp ts)
                (numberp tr)
                (not (zerop w))
                (not (zerop r))
                (not (lessp tr ts))
                (lessp tr (plus ts w)))
           (not (lessp (plus r (ntr* k ts tr w r))
                       (plus (nts* k ts tr w r)
                             (times w (nlst* k ts tr w r)))))))

; That takes care of ts'<=tr'.  Now I'll get tr' < ts'+w.  In our case,
; ts' is (nts+ m ts'' tr' w r).  Now nts+ is going to push ts'' to within
; w or tr' unless m runs out.  So we have to make an argument that
; m is big enough.  It turns out that we know m is at least 18
; (because it is the encoding of a listp msg) and so if we assume w and r
; are within a factor of 2 of eachother, we can manage.

; These helper lemmas are generated mechanically by just grabbing
; the unproved goals generated in the next real theorem and forcing
; the expansion of the relevant terms.  Chances are there are some
; irrelevant hypotheses.  Some helper's subsumed others or changed the
; course of the proof so as to make others irrelevant.  Thus, their
; numbering is not consecutive.

(prove-lemma helper1 (rewrite)
  (implies (and (numberp ts)
                (numberp tr)
                (not (equal w 0))
                (numberp w)
                (not (equal r 0))
                (numberp r)
                (not (lessp tr ts))
                (lessp tr (plus ts w))
                (lessp w (times 2 r))
                (lessp r (times 2 w))
                (listp rest)
                (lessp (plus ts w w) (plus r tr))
                (lessp (plus ts w) (plus r tr))
                (not (lessp (plus r tr) (plus ts w w))))
           (equal (warp (lst+ rest
                              (plus ts w w)
                              (plus r tr)
                              w)
                        (nts+ (len rest)
                              (plus ts w w)
                              (plus r tr)
                              w)
                        (plus r tr)
                        w r)
                  (warp rest
                        (plus ts w w)
                        (plus r tr)
                        w r)))
  ((expand (lst+ rest
                 (plus ts w w)
                 (plus r tr)
                 w)
           (nts+ (len rest)
                 (plus ts w w)
                 (plus r tr)
                 w))))

(prove-lemma helper5 (rewrite)
  (implies (and (numberp ts)
                (numberp tr)
                (numberp k)
                (not (equal w 0))
                (numberp w)
                (not (equal r 0))
                (numberp r)
                (not (lessp tr ts))
                (lessp tr (plus ts w))
                (lessp w (times 2 r))
                (lessp r (times 2 w))
                (listp rest)
                (listp (cdr rest))
                (equal (sub1 (sub1 k)) 0)
                (lessp (plus ts w w) (plus r tr))
                (lessp (plus ts w) (plus r tr))
                (lessp (plus r tr)
                       (plus ts w (times k w)))
                (not (lessp (plus r r tr)
                            (plus ts w (times k w))))
                (lessp (plus r r tr)
                       (plus ts w w (times k w))))
           (equal (warp (cons 'q rest)
                        (plus ts (times k w))
                        (plus r tr)
                        w r)
                  (cons 'q
                        (warp rest
                              (plus ts w (times k w))
                              (plus tr (times 2 r))
                              w r))))
  ((expand (warp (cons 'q rest)
                 (plus ts w (times w (sub1 k)))
                 (plus r tr)
                 w r)
           (times 2 r))))

(prove-lemma helper7 (rewrite)
  (implies (and (numberp ts)
                (numberp tr)
                (not (equal w 0))
                (numberp w)
                (not (equal r 0))
                (numberp r)
                (not (lessp tr ts))
                (lessp tr (plus ts w))
                (lessp w (times 2 r))
                (lessp r (times 2 w))
                (listp rest)
                (listp (cdr rest))
                (lessp (plus ts w) (plus r tr))
                (not (lessp (plus r tr) (plus ts w w)))
                (lessp (plus r tr) (plus ts w w w)))
           (equal (warp (cons flg1 (cons 'q rest))
                        ts tr w r)
                  (cons 'q
                        (warp rest
                              (plus ts w w)
                              (plus r tr)
                              w r))))
  ((expand (warp (cons flg1 (cons 'q rest))
                 ts tr w r))))

(prove-lemma helper8 (rewrite)
 (implies (and (numberp ts)
               (numberp tr)
               (not (equal w 0))
               (numberp w)
               (not (equal r 0))
               (numberp r)
               (not (lessp tr ts))
               (lessp tr (plus ts w))
               (lessp w (times 2 r))
               (lessp r (times 2 w))
               (listp rest)
               (listp (cdr rest))
               (lessp (plus ts w) (plus r tr))
               (not (lessp (plus r tr) (plus ts w)))
               (not (equal (plus r tr) (plus ts w)))
               (not (lessp (plus r tr) (plus ts w w))))
          (equal (warp (cons 'q rest) ts tr w r)
                 (cons 'q
                       (warp (cdr rest)
                             (plus ts w w)
                             (plus r tr)
                             w r))))
 ((expand (warp (cons 'q rest) ts tr w r)
          (lst+ (cdr rest)
                (plus ts w w)
                (plus r tr)
                w)
          (nts+ (len (cdr rest))
                (plus ts w w)
                (plus r tr)
                w)
          (lst+ rest
                (plus ts w)
                (plus r tr)
                w)
          (nts+ (add1 (len (cdr rest)))
                (plus ts w)
                (plus r tr)
                w))))

(prove-lemma helper9 (rewrite)
  (implies (and (numberp ts)
                (numberp tr)
                (not (equal w 0))
                (numberp w)
                (not (equal r 0))
                (numberp r)
                (not (lessp tr ts))
                (lessp tr (plus ts w))
                (lessp w (plus r r))
                (lessp r (times 2 w))
                (listp rest)
                (listp (cdr rest))
                (lessp (plus ts w) (plus r tr))
                (lessp (plus r tr) (plus ts w w))
                (not (lessp (plus r r tr) (plus ts w w)))
                (not (lessp (plus r r tr)
                            (plus ts w w w))))
           (equal (warp (cons flg1 (cons 'q rest))
                        ts tr w r)
                  (cons 'q
                        (cons 'q
                              (warp (cdr rest)
                                    (plus ts w w w)
                                    (plus r r tr)
                                    w r)))))
  ((expand (warp (cons flg1 (cons 'q rest))
                 ts tr w r))))

(prove-lemma helper10 (rewrite)
  (implies (and (numberp ts)
                (numberp tr)
                (not (equal w 0))
                (numberp w)
                (not (equal r 0))
                (numberp r)
                (not (lessp tr ts))
                (lessp tr (plus ts w))
                (lessp w (plus r r))
                (lessp r (times 2 w))
                (listp rest)
                (listp (cdr rest))
                (lessp (plus ts w) (plus r tr))
                (lessp (plus r tr) (plus ts w w))
                (not (lessp (plus r r tr) (plus ts w w)))
                (lessp (plus r r tr) (plus ts w w w)))
           (equal (warp (cons flg1 (cons 'q rest))
                        ts tr w r)
                  (cons 'q
                        (cons 'q
                              (warp rest
                                    (plus ts w w)
                                    (plus r r tr)
                                    w r)))))
  ((expand (warp (cons flg1 (cons 'q rest))
                 ts tr w r)
           (warp (cons 'q rest)
                 (plus ts w)
                 (plus r tr)
                 w r))))

(prove-lemma helper11 (rewrite)
  (implies (and (numberp ts)
                (numberp tr)
                (not (equal w 0))
                (numberp w)
                (not (equal r 0))
                (numberp r)
                (not (lessp tr ts))
                (lessp tr (plus ts w))
                (lessp w (plus r r))
                (lessp r (times 2 w))
                (listp rest)
                (listp (cdr rest))
                (lessp (plus ts w) (plus r tr))
                (lessp (plus r tr) (plus ts w w))
                (lessp (plus r r tr) (plus ts w w))
                (lessp (plus r r tr) (plus ts w w w)))
           (equal (warp (cons flg1 (cons 'q rest))
                        ts tr w r)
                  (cons 'q
                        (cons 'q
                              (cons 'q
                                    (warp rest
                                          (plus ts w w)
                                          (plus tr (times 3 r))
                                          w r))))))
  ((expand (warp (cons flg1 (cons 'q rest))
                 ts tr w r)
           (warp (cons 'q rest)
                 (plus ts w)
                 (plus r r tr)
                 w r)
           (warp (cons 'q rest)
                 (plus ts w)
                 (plus r tr)
                 w r)
           (times 2 r)
           (times 3 r))))

(prove-lemma lessp-times-18 (rewrite)
  (implies (listp msg)
           (not (lessp (times 18 (len msg)) 18))))

(prove-lemma listn-add1 (rewrite)
  (equal (listn (add1 n) flg)
         (cons flg (listn n flg)))
  ((enable listn)))

(prove-lemma helper14 (rewrite)
  (IMPLIES (AND (NUMBERP TS)
                (NUMBERP TR)
                (NOT (EQUAL W 0))
                (NUMBERP W)
                (NOT (EQUAL R 0))
                (NUMBERP R)
                (NOT (LESSP TR TS))
                (LESSP TR (PLUS TS W))
                (LESSP W (PLUS R R))
                (LESSP R (TIMES 2 W))
                (LISTP REST)
                (LISTP (CDR REST))
                (NOT (LESSP (PLUS R TR) (PLUS TS W)))
                (LESSP (PLUS R TR) (PLUS TS W W)))
           (EQUAL (WARP (CONS 'Q REST) TS TR W R)
                  (CONS 'Q
                        (WARP REST
                              (PLUS TS W)
                              (PLUS R TR)
                              W R))))
  ((expand (WARP (CONS 'Q REST) TS TR W R))))

(prove-lemma helper15 (rewrite)
  (IMPLIES (AND (NUMBERP TS)
                (NUMBERP TR)
                (NOT (EQUAL W 0))
                (NUMBERP W)
                (NOT (EQUAL R 0))
                (NUMBERP R)
                (NOT (LESSP TR TS))
                (LESSP TR (PLUS TS W))
                (LESSP W (PLUS R R))
                (LESSP R (TIMES 2 W))
                (LISTP REST)
                (LISTP (CDR REST))
                (LESSP (PLUS R TR) (PLUS TS W))
                (NOT (LESSP (PLUS R R TR) (PLUS TS W)))
                (LESSP (PLUS R R TR) (PLUS TS W W)))
           (EQUAL (WARP (CONS 'Q REST) TS TR W R)
                  (CONS 'Q
                        (CONS 'Q
                              (WARP REST
                                    (PLUS TS W)
                                    (PLUS R R TR)
                                    W R)))))
  ((expand (WARP (CONS 'Q REST) TS TR W R))))

(prove-lemma warp-app-across-gap (rewrite)
  (implies (and (numberp ts)
                (numberp tr)
                (numberp k)
                (not (zerop w))
                (not (zerop r))
                (not (lessp tr ts))
                (lessp tr (plus ts w))
                (lessp w (times 2 r))
                (lessp r (times 2 w))
                (listp rest)
                (listp (cdr rest))
                (nendp k ts (plus r tr) w))
           (equal (warp (app (listn k flg1)
                             (cons 'q rest))
                        ts tr w r)
                  (app (listn (nqg k ts tr w r) 'q)
                       (warp (cdrn (dwg k ts tr w r) rest)
                             (tsg k ts tr w r)
                             (trg k ts tr w r)
                             w r))))
  ((do-not-induct t)
   (enable listn)
   (expand (nendp k ts (plus r tr) w)
           (nendp (sub1 k)
                  (plus ts w)
                  (plus r tr)
                  w)
           (nendp (sub1 (sub1 k))
                  (plus ts w w)
                  (plus r tr)
                  w)
           (times 2 r))))

(disable helper1)
(disable helper5)
(disable helper7)
(disable helper8)
(disable helper9)
(disable helper10)
(disable helper11)
(disable helper14)
(disable helper15)

(disable nqg)
(disable dwg)
(disable tsg)
(disable trg)

(defn nq (n ts tr w r)
  (nqg (nlst* n ts tr w r)
       (nts* n ts tr w r)
       (ntr* n ts tr w r)
       w r))

(defn dw (n ts tr w r)
  (dwg (nlst* n ts tr w r)
       (nts* n ts tr w r)
       (ntr* n ts tr w r)
       w r))


(defn ts (n ts tr w r)
  (tsg (nlst* n ts tr w r)
       (nts* n ts tr w r)
       (ntr* n ts tr w r)
       w r))

(defn tr (n ts tr w r)
  (trg (nlst* n ts tr w r)
       (nts* n ts tr w r)
       (ntr* n ts tr w r)
       w r))

(prove-lemma lessp-2-len-implies-listps nil
  (implies (lessp 2 (len x))
           (and (listp x) (listp (cdr x)))))

(prove-lemma warp-app-listn-q1 nil
  (implies (and (numberp ts)
                (numberp tr)
                (not (zerop w))
                (not (zerop r))
                (not (lessp tr ts))
                (lessp tr (plus ts w))
                (lessp w (times 2 r))
                (lessp r (times 2 w))
                (numberp n1)
                (lessp 2 (len rest)))
           (equal (target (warp (app (listn n1 flg1) (cons 'q rest))
                                ts tr w r))
                  (app (listn (n* n1 ts tr w r) flg1)
                       (app (listn (nq n1 ts tr w r) 'q)
                            (warp (cdrn (dw n1 ts tr w r) rest)
                                  (ts n1 ts tr w r)
                                  (tr n1 ts tr w r)
                                  w r)))))
  ((use (lessp-2-len-implies-listps (x rest)))
   (disable warp-app-gap)))

(prove-lemma warp-app-listn-q (rewrite)
  (implies (and (numberp ts)
                (numberp tr)
                (not (zerop w))
                (not (zerop r))
                (not (lessp tr ts))
                (lessp tr (plus ts w))
                (lessp w (times 2 r))
                (lessp r (times 2 w))
                (numberp n1)
                (lessp 2 (len rest)))
           (equal (warp (app (listn n1 flg1) (cons 'q rest))
                        ts tr w r)
                  (app (listn (n* n1 ts tr w r) flg1)
                       (app (listn (nq n1 ts tr w r) 'q)
                            (warp (cdrn (dw n1 ts tr w r) rest)
                                  (ts n1 ts tr w r)
                                  (tr n1 ts tr w r)
                                  w r)))))
  ((use (warp-app-listn-q1))
   (enable target)))

(disable listn-add1)
(disable WARP-APP-ACROSS-GAP)
(disable WARP-APP-GAP)
(disable WARP-LISTN)
(disable warp-app)

; Now there are two applications we must think about:  the proof of top and
; the proof of loop.  We will deal with top first.  To explore I want to
; do the smoothing and det part of top now and then come back to warp.

; Now we do the smoothing.

(prove-lemma smooth-congruence (rewrite)
  (implies (not (b-xor flg1 flg2))
           (equal (equal (smooth flg2 rest)
                         (smooth flg1 rest))
                  t))
  ((enable b-xor smooth)))

(prove-lemma smooth-flg-app-listn-flg (rewrite)
  (implies (not (b-xor flg1 flg2))
           (equal (smooth flg1 (app (listn p1 flg2) rest))
                  (app (listn p1 flg2) (smooth flg1 rest))))
  ((induct (listn p1 flg2))
   (enable smooth listn)))
                                                 
(prove-lemma listp-app-listn (rewrite)
  (equal (listp (app (listn n flg) rest))
         (or (not (zerop n))
             (listp rest)))
  ((enable listn)))

(prove-lemma listp-cells (rewrite)
  (equal (listp (cells flg 5 13 msg)) (listp msg))
  ((enable cells cell)))

(disable listp-app-listn)

(prove-lemma car-app (rewrite)
  (equal (car (app a b))
         (if (listp a) (car a) (car b))))

(prove-lemma listp-listn (rewrite)
  (equal (listp (listn n flg))
         (not (zerop n)))
  ((enable listn)))

(prove-lemma car-cells (rewrite)
  (implies (listp msg)
           (equal (car (cells flg 5 13 msg))
                  (b-not flg)))
  ((expand (cells flg 5 13 msg)
           (listn 5 (b-not flg)))
   (enable cell listn)))

(disable car-app)

(prove-lemma top-smooth-step (rewrite)
  (implies (listp msg)
           (equal (smooth t (app (listn p1 t) (app (cells t 5 13 msg) (listn p2 t))))
                  (app (listn p1 t)
                       (cons 'q (smooth f (app (cdr (cells t 5 13 msg))
                                               (listn p2 t)))))))
  ((enable cells smooth)))

(disable smooth-flg-app-listn-flg)
(disable car-cells)
(disable listp-cells)

; Now past the det

(defn oracle* (lst oracle)
  (if (nlistp lst)
      oracle
      (if (equal (car lst) 'q)
          (oracle* (cdr lst) (cdr oracle))
          (oracle* (cdr lst) oracle))))

(disable oracle*)

(prove-lemma det-app (rewrite)
  (equal (det (app lst1 lst2) oracle)
         (app (det lst1 oracle)
              (det lst2 (oracle* lst1 oracle))))
  ((enable det oracle*)))

(prove-lemma det-listn (rewrite)
  (implies (not (equal flg 'q))
           (equal (det (listn n flg) oracle)
                  (listn n flg)))
  ((enable det listn)))

(prove-lemma oracle*-listn (rewrite)
  (implies (not (equal flg 'q))
           (equal (oracle* (listn n flg) oracle)
                  oracle))
  ((enable oracle* listn)))

; So now we combine all these.

(prove-lemma len-smooth (rewrite)
  (equal (len (smooth flg lst)) (len lst))
  ((enable smooth)))

(prove-lemma cdr-app (rewrite)
  (equal (cdr (app a b))
         (if (listp a) (app (cdr a) b) (cdr b))))

(prove-lemma top-async-send-lemma1 (rewrite)
  (implies (listp msg)
           (LESSP 2 (len (cdr (cells t 5 13 msg)))))
  ((expand (cells t 5 13 msg))
   (enable cell)))

(disable cdr-app)

(prove-lemma top-async-send (rewrite)
  (implies (and (bvp msg)
                (listp msg)
                (numberp ts)
                (numberp tr)
                (not (zerop w))
                (not (zerop r))
                (not (lessp tr ts))
                (lessp tr (plus ts w))
                (rate-proximity w r)
                (numberp p1))
           (equal (async (send msg p1 5 13 p2) ts tr w r oracle)
                  (app (listn (n* p1 ts tr w r) t)
                       (app (det (listn (nqg (nlst* p1 ts tr w r)
                                             (nts* p1 ts tr w r)
                                             (ntr* p1 ts tr w r)
                                             w r)
                                        'q)
                                 oracle)
                            (det (warp (cdrn (dwg (nlst* p1 ts tr w r)
                                                  (nts* p1 ts tr w r)
                                                  (ntr* p1 ts tr w r)
                                                  w r)
                                             (smooth f
                                                     (app (cdr (cells t 5 13 msg))
                                                          (listn p2 t))))
                                       (tsg (nlst* p1 ts tr w r)
                                            (nts* p1 ts tr w r)
                                            (ntr* p1 ts tr w r)
                                            w r)
                                       (trg (nlst* p1 ts tr w r)
                                            (nts* p1 ts tr w r)
                                            (ntr* p1 ts tr w r)
                                            w r)
                                       w r)
                                 (oracle* (listn (nqg (nlst* p1 ts tr w r)
                                                      (nts* p1 ts tr w r)
                                                      (ntr* p1 ts tr w r)
                                                      w r)
                                                 'q)
                                          oracle))))))
  ((disable app)
   (enable async send)))
                  
(disable top-async-send-lemma1)
(disable top-smooth-step)

; Now we get recv to eat the header.

(prove-lemma scan-app-listn (rewrite)
  (equal (scan flg (app (listn n flg) rest))
         (scan flg rest))
  ((enable scan listn)))

(prove-lemma top-recv-step (rewrite)
  (equal (recv n t k (app (listn p1 t) rest))
         (recv n t k rest))
  ((enable recv)))

#| At this point our top level goal looks like this
(equal (recv (len msg)
             t 10
             (app (det (listn (nqg (nlst* p1 ts tr w r)
                                   (nts* p1 ts tr w r)
                                   (ntr* p1 ts tr w r)
                                   w r)
                              'q)
                       oracle)
                  (det (warp (cdrn (dwg (nlst* p1 ts tr w r)
                                        (nts* p1 ts tr w r)
                                        (ntr* p1 ts tr w r)
                                        w r)
                                   (smooth f
                                           (app (cdr (cells t 5 13 msg))
                                                (listn p2 t))))
                             (tsg (nlst* p1 ts tr w r)
                                  (nts* p1 ts tr w r)
                                  (ntr* p1 ts tr w r)
                                  w r)
                             (trg (nlst* p1 ts tr w r)
                                  (nts* p1 ts tr w r)
                                  (ntr* p1 ts tr w r)
                                  w r)
                             w r)
                       (oracle* (listn (nqg (nlst* p1 ts tr w r)
                                            (nts* p1 ts tr w r)
                                            (ntr* p1 ts tr w r)
                                            w r)
                                       'q)
                                oracle))))
       msg)
and we will generalize it to
(equal (recv (len msg)
             t 10
             (app (det (listn nq 'q) oracle1)
                  (det (warp (cdrn dw
                                   (smooth f
                                           (app (cdr (cells t 5 13 msg))
                                                (listn p2 t))))
                             ts tr w r)
                       oracle2)))
       msg)
where we have the usual bounds on nq, dw, ts and tr.

To justify this generalization we must prove the theorems that the
expressions generalized satisfy the usual bounds.  We do that now.

|#

(prove-lemma nqg-bounds (rewrite)
  (and (lessp 0 (nqg n ts tr w r))
       (not (lessp 3 (nqg n ts tr w r))))
  ((enable nqg)))

(prove-lemma dwg-bounds (rewrite)
  (not (lessp 1 (dwg n ts tr w r)))
  ((enable dwg)))

; Typically trg and tsg will be instantiated as below.  We package up
; the required backchaining here.  It is my impression that the
; generalized form in which the * terms do not appear is not a
; theorem.  The proof of this relies upon 
; NOT-LESSP-PLUS-R-NTR*-PLUS-NTS*-TIMES-W-NLST*.

(prove-lemma not-lessp-trg*-tsg* (rewrite)
  (implies (and (numberp ts)
                (numberp tr)
                (numberp n)
                (not (zerop w))
                (not (zerop r))
                (not (lessp tr ts))
                (lessp tr (plus ts w))
                (lessp w (times 2 r))
                (lessp r (times 2 w)))
           (not (lessp (trg (nlst* n ts tr w r)
                            (nts* n ts tr w r)
                            (ntr* n ts tr w r)
                            w r)
                       (tsg (nlst* n ts tr w r)
                            (nts* n ts tr w r)
                            (ntr* n ts tr w r)
                            w r))))
  ((enable trg tsg nqg dwg)))

(prove-lemma lessp-trg*-plus-w-tsg* (rewrite)
  (implies (and (numberp ts)
                (numberp tr)
                (numberp n)
                (not (zerop w))
                (not (zerop r))
                (not (lessp tr ts))
                (lessp tr (plus ts w))
                (lessp w (times 2 r))
                (lessp r (times 2 w)))
           (lessp (trg (nlst* n ts tr w r)
                       (nts* n ts tr w r)
                       (ntr* n ts tr w r)
                       w r)
                  (plus w (tsg (nlst* n ts tr w r)
                               (nts* n ts tr w r)
                               (ntr* n ts tr w r)
                               w r))))
  ((enable trg tsg nqg dwg)))

#|
Consider the lhs of the concl of loop:

(recv (len msg)
      flg1
      10
      (app (det (listn nq 'q) oracle1)
           (det (warp (cdrn dw
                            (smooth flg2
                                    (app (cdr (cells flg1 5 13 msg))
                                         (listn p2 t))))
                      ts tr w r)
                oracle2)))

We will derive a killer rewrite rule that expands this, under the
conditions governing our induction, into (cons (car msg) ...) where
... is an instance of the lhs above.  I.e., the rule will step the
lhs of the ind concl into the induction hypothesis.  The derivation of
this rule will be documented by showing the successive steps.  The
actual discovery of the form of the lhs above and the steps was
made by proving the "killer rule" over and over again, each time
making some transformation.

The first step is to open (cells flg1 5 13 msg), drive the cdr around
the first cell and absorb it into the cell size, and associate the apps,
|#

(prove-lemma cdr-app-cell-cells (rewrite)
  (implies (not (zerop n1))
           (equal (cdr (app (cell flg1 n1 n2 bit) (cells flg2 n1 n2 msg)))
                  (app (cell flg1 (sub1 n1) n2 bit) (cells flg2 n1 n2 msg))))
  ((enable cdr-app cell listn)))

#|
So lhs becomes:
(recv (len msg)
      flg1
      10
      (app (det (listn nq 'q) oracle1)
           (det (warp (cdrn dw
                            (smooth flg2
                                    (app (cell flg1 4 13 (car msg))
                                         (app (cells (csig flg1 (car msg)) 5 13 (cdr msg))
                                              (listn p2 t)))))
                      ts tr w r)
                oracle2)))

Our next goal is to drive the smooth through the app.
|#
(prove-lemma smooth-flg-listn-flg (rewrite)
  (implies (not (b-xor flg1 flg2))
           (equal (smooth flg1 (listn n flg2)) (listn n flg2)))
  ((enable smooth listn)))

(prove-lemma not-b-xor-b-not (rewrite)
  (implies (b-xor flg1 flg2)
           (and (not (b-xor flg1 (b-not flg2)))
                (not (b-xor (b-not flg2) flg1))))
  ((enable b-xor b-not)))

(prove-lemma smooth-flg-app-listn-not-flg (rewrite)
  (implies (and (not (zerop n))
                (b-xor flg1 flg2))
           (equal (smooth flg1 (app (listn n flg2) rest))
                  (app (smooth flg1 (listn n flg2))
                       (smooth flg2 rest))))
  ((induct (listn n flg2))
   (enable smooth listn)))

(prove-lemma smooth-app-cell-app-cells (rewrite)
  (implies (and (not (zerop n1))
                (b-xor flg1 flg2))
           (equal (smooth flg1
                          (app (cell flg2 m1 n1 bit)
                               (app (cells (csig flg2 bit) m n msg)
                                    (listn p2 t))))
                  (app (smooth flg1 (cell flg2 m1 n1 bit))
                       (smooth (csig flg2 bit)
                               (app (cells (csig flg2 bit) m n msg)
                                    (listn p2 t))))))
  ((enable smooth listn cell csig smooth-flg-app-listn-flg)))

(disable smooth-flg-listn-flg)
(disable smooth-flg-app-listn-not-flg)

; If we had loop-stoppers on iff rules we could use an iff and be more efficient.
(prove-lemma b-xor-commutes (rewrite)
  (implies (b-xor x y) (b-xor y x))
  ((enable b-xor)))

#|
So lhs is now:
(recv (len msg)
      flg1
      10
      (app (det (listn nq 'q) oracle1)
           (det (warp (cdrn dw
                            (app (smooth flg2 (cell flg1 4 13 (car msg)))
                                 (smooth (csig flg1 (car msg))
                                         (app (cells (csig flg1 (car msg)) 5 13 (cdr msg))
                                              (listn p2 t)))))
                      ts tr w r)
                oracle2)))
Now drive the cdrn into the app and the smooth and absorb it in the
cell size.

|#

(prove-lemma listp-smooth-cell (rewrite)
  (implies (not (zerop m))
           (listp (smooth flg1 (cell flg2 m n bit))))
  ((enable cell smooth)
   (expand (listn m (b-not flg2)))))

(prove-lemma cdrn-dw-app-smooth-cell (rewrite)
  (implies (and (not (zerop m))
                (numberp dw)
                (not (lessp 1 dw)))
           (equal (cdrn dw (app (smooth flg1 (cell flg2 m n bit)) rest))
                  (app (cdrn dw (smooth flg1 (cell flg2 m n bit)))
                       rest)))
  ((enable cdr-app)
   (expand (cdrn dw (app (smooth flg1 (cell flg2 m n bit)) rest))
           (cdrn 1 (smooth flg1 (cell flg2 m n bit))))))

(prove-lemma car-listn (rewrite)
  (equal (car (listn n flg)) (if (zerop n) 0 flg))
  ((enable listn)))

(prove-lemma cdrn-dw-smooth-cell (rewrite)
  (implies (and (not (zerop m))
                (numberp dw)
                (not (lessp 1 dw))
                (b-xor flg1 flg2))
           (equal (cdrn dw (smooth flg2 (cell flg1 m n (car msg))))
                  (smooth flg2 (cell flg1 (difference m dw) n (car msg)))))
  ((enable cdr-app cell listn-add1 smooth)
   (expand (listn m (b-not flg1))
           (cdrn dw
                 (cons (b-not flg1)
                       (smooth (b-not flg1)
                               (app (listn (sub1 m) (b-not flg1))
                                    (listn n (csig flg1 (car msg)))))))
           (plus 1 x))
   (do-not-induct t)))

(disable car-listn)

#|
So lhs is
(recv (len msg)
      flg1
      10
      (app (det (listn nq 'q) oracle1)
           (det (warp (app (smooth flg2 (cell flg1 (difference 4 dw) 13 (car msg)))
                           (smooth (csig flg1 (car msg))
                                   (app (cells (csig flg1 (car msg)) 5 13 (cdr msg))
                                        (listn p2 t))))
                      ts tr w r)
                oracle2)))
Next we drive the warp through the app.  We do that by putting a TARGET around
the warp and enabling warp-app.  To simplify the resulting len expressions we
use:
|#

(prove-lemma len-cell (rewrite)
  (equal (len (cell flg m n bit))
         (plus m n))
  ((enable cell)))

(prove-lemma add1-plus-12-difference-4-dw (rewrite)
  (implies (not (lessp 1 dw))
           (equal (ADD1 (PLUS 12 (DIFFERENCE 4 DW)))
                  (difference 17 dw))))

#|
Det-app also applies to drive the det through the app.
So now lhs is
(recv
 (len msg)
 flg1 10
 (app (det (listn nq 'q) oracle1)
      (app (det (warp (smooth flg2
                              (cell flg1
                                    (difference 4 dw)
                                    13
                                    (car msg)))
                      ts tr w r)
                oracle2)
           (det (warp (app (lst* (smooth flg2
                                         (cell flg1
                                               (difference 4 dw)
                                               13
                                               (car msg)))
                                 ts tr w r)
                           (smooth (csig flg1 (car msg))
                                   (app (cells (csig flg1 (car msg)) 5
                                               13
                                               (cdr msg))
                                        (listn p2 t))))
                      (nts* (difference 17 dw) ts tr w r)
                      (ntr* (difference 17 dw) ts tr w r)
                      w r)
                (oracle* (app (lst* (smooth flg2
                                            (cell flg1
                                                  (difference 4 dw)
                                                  13
                                                  (car msg)))
                                    ts tr w r)
                              (smooth (csig flg1 (car msg))
                                      (app (cells (csig flg1 (car msg)) 5
                                                  13
                                                  (cdr msg))
                                           (listn p2 t))))
                         oracle2)))))

Consider the second warp expression, the one applied to (app (lst* ...)...).
We want to apply warp-app-listn-q to this, which expects 
(app (listn n1 flg1) (cons 'q rest))

So now we focus on causing that to happen.  The lst* produces a listn.
Our induction will make a base case out of the one-bit msg.  So we know
the current cell is followed by another and hence by an edge.
So our 'q comes from there.

We have this induction in mind but we don't yet know the ... parts. The
variables are listed in order of appearance.

(defn loop-ind-hint (nq oracle1 dw flg2 flg1 msg ts tr w r oracle2)
  (cond ((nlistp msg) t)
        ((nlistp (cdr msg)) t)
        (t (loop-ind-hint ... (cdr msg) ...))))

|#

; "The lst* produces a listn."

(prove-lemma lst*-is-lastn-nlst* (rewrite)
  (equal (lst* lst ts tr w r)
         (lastn (nlst* (len lst) ts tr w r) lst))
  ((use (lst*-is-lastn))))

(prove-lemma lastn-app (rewrite)
  (implies (not (lessp (len b) n))
           (equal (lastn n (app a b))
                  (lastn n b))))

(prove-lemma not-lessp-2-nlst* (rewrite)
  (implies (and (numberp ts)
                (numberp tr)
                (not (zerop w))
                (not (zerop r))
                (not (lessp tr ts))
                (lessp tr (plus ts w))
                (lessp w (times 2 r))
                (lessp r (times 2 w)))
           (not (lessp 2 (nlst* n ts tr w r)))))

(prove-lemma smooth-flg-listn-not-flg (rewrite)
  (implies (and (not (zerop n))
                (b-xor flg1 flg2))
           (equal (smooth flg1 (listn n flg2))
                  (cons 'q (listn (sub1 n) flg2))))
  ((enable smooth listn)))

(disable smooth-flg-listn-not-flg)

(prove-lemma lst*-smooth-cell (rewrite)
  (implies (and (numberp ts)
                (numberp tr)
                (not (zerop w))
                (not (zerop r))
                (not (lessp tr ts))
                (lessp tr (plus ts w))
                (lessp w (times 2 r))
                (lessp r (times 2 w))
                (not (zerop m))
                (numberp n)
                (lessp 2 n)
                (b-xor flg1 flg2))
           (equal (lst* (smooth flg2 (cell flg1 m n bit)) ts tr w r)
                  (listn (nlst* (plus m n) ts tr w r)
                         (csig flg1 bit))))
  ((enable csig cell smooth-flg-app-listn-flg smooth-flg-app-listn-not-flg
           smooth-flg-listn-flg smooth-flg-listn-not-flg)))

(disable lst*-is-lastn-nlst*)


#|
So lhs is
(recv
 (len msg)
 flg1 10
 (app (det (listn nq 'q) oracle1)
      (app (det (warp (smooth flg2
                              (cell flg1
                                    (difference 4 dw)
                                    13
                                    (car msg)))
                      ts tr w r)
                oracle2)
           (det (warp (app (listn (nlst* (difference 17 dw) ts tr w r)
                                  (csig flg1 (car msg)))
                           (smooth (csig flg1 (car msg))
                                   (app (cells (csig flg1 (car msg)) 5
                                               13
                                               (cdr msg))
                                        (listn p2 t))))
                      (nts* (difference 17 dw) ts tr w r)
                      (ntr* (difference 17 dw) ts tr w r)
                      w r)
                (oracle* (warp (smooth flg2
                                       (cell flg1
                                             (difference 4 dw)
                                             13
                                             (car msg)))
                               ts tr w r)
                         oracle2)))))

And we're going to milk a 'q out of the smoothing of the cells term.
|#

; "So our 'q comes from there."

(prove-lemma cdr-listn (rewrite)
  (equal (cdr (listn n flg))
         (if (zerop n) 0 (listn (sub1 n) flg)))
  ((expand (listn n flg))))

(disable cdr-listn)

(prove-lemma smooth-app-cells (rewrite)
  (implies (and (listp msg)
                (not (zerop m)))
           (equal (smooth flg
                          (app (cells flg m n msg)
                               (listn p2 t)))
                  (cons 'q (smooth (b-not flg)
                                   (app (cdr (cells flg m n msg))
                                        (listn p2 t))))))
  ((expand (cells flg m n msg))
   (enable cell smooth-flg-app-listn-not-flg smooth-flg-listn-not-flg cdr-app
           cdr-listn smooth-flg-app-listn-flg)))

#|
So lhs is
(recv
 (len msg)
 flg1 10
 (app (det (listn nq 'q) oracle1)
      (app (det (warp (smooth flg2
                              (cell flg1
                                    (difference 4 dw)
                                    13
                                    (car msg)))
                      ts tr w r)
                oracle2)
           (det (warp (app (listn (nlst* (difference 17 dw) ts tr w r)
                                  (csig flg1 (car msg)))
                           (cons 'q
                                 (smooth (b-not (csig flg1 (car msg)))
                                         (app (cdr (cells (csig flg1 (car msg)) 5
                                                          13
                                                          (cdr msg)))
                                              (listn p2 t)))))
                      (nts* (difference 17 dw) ts tr w r)
                      (ntr* (difference 17 dw) ts tr w r)
                      w r)
                (oracle* (warp (smooth flg2
                                       (cell flg1
                                             (difference 4 dw)
                                             13
                                             (car msg)))
                               ts tr w r)
                         oracle2)))))
Observe that warp-app-listn-q is now applicable if we can relieve the hypotheses.
The only nonobvious one is relieved by:
|#

(prove-lemma lessp-2-len-cdr-cells (rewrite)
  (implies (listp msg)
           (lessp 2 (len (cdr (cells flg 5 13 msg)))))
  ((expand (cells flg 5 13 msg))))

; So warp-app-listn-q will push the warp through the two apps and let
; det-app push the det through.  Note that while warp-app-listn-q normally
; kicks out some t's or f's before the 'qs the initial string here is
; empty because we're starting with only nlst* of them.  Of course, we
; have to know

(prove-lemma app-listn-0 (rewrite)
  (equal (app (listn 0 flg) rest) rest)
  ((enable listn)))

; We include the app because in the proof of our killer rule, app will be
; disabled.

; We are now ready to solidfy our gains as the first step of our killer
; rule. We use the name loop-killer-1a because it has a TARGET on our
; warp.  Loop-killer-1, next, doesn't. 

(prove-lemma loop-killer-1a nil
  (implies (and (bvp msg)
                (listp msg)
                (listp (cdr msg))
                (numberp ts)
                (numberp tr)
                (not (zerop w))
                (not (zerop r))
                (not (lessp tr ts))
                (lessp tr (plus ts w))
                (rate-proximity w r)

                (numberp nq)
                (not (lessp 3 nq))
                (numberp dw)
                (not (lessp 1 dw))
                (b-xor flg1 flg2))
           (equal (recv (len msg)
                        flg1
                        10
                        (app (det (listn nq 'q) oracle1)
                             (det (target (warp (cdrn dw
                                                      (smooth flg2
                                                              (app (cdr (cells flg1 5 13 msg))
                                                                   (listn p2 t))))
                                                ts tr w r))
                                  oracle2)))
                  (recv
                   (len msg)
                   flg1 10
                   (app (det (listn nq 'q) oracle1)
                        (app (det (warp (smooth flg2
                                                (cell flg1
                                                      (difference 4 dw)
                                                      13
                                                      (car msg)))
                                        ts tr w r)
                                  oracle2)
                             (app (det (listn (nqg (nlst* (difference 17 dw) ts tr w r)
                                                   (nts* (difference 17 dw) ts tr w r)
                                                   (ntr* (difference 17 dw) ts tr w r)
                                                   w r)
                                              'q)
                                       (oracle* (warp (smooth flg2
                                                              (cell flg1
                                                                    (difference 4 dw)
                                                                    13
                                                                    (car msg)))
                                                      ts tr w r)
                                                oracle2))
                                  (det (warp (cdrn (dwg (nlst* (difference 17 dw) ts tr w r)
                                                        (nts* (difference 17 dw) ts tr w r)
                                                        (ntr* (difference 17 dw) ts tr w r)
                                                        w r)
                                                   (smooth (b-not (csig flg1 (car msg)))
                                                           (app (cdr (cells (csig flg1 (car msg)) 5
                                                                            13
                                                                            (cdr msg)))
                                                                (listn p2 t))))
                                             (tsg (nlst* (difference 17 dw) ts tr w r)
                                                  (nts* (difference 17 dw) ts tr w r)
                                                  (ntr* (difference 17 dw) ts tr w r)
                                                  w r)
                                             (trg (nlst* (difference 17 dw) ts tr w r)
                                                  (nts* (difference 17 dw) ts tr w r)
                                                  (ntr* (difference 17 dw) ts tr w r)
                                                  w r)
                                             w r)
                                       (oracle* (listn (nqg (nlst* (difference 17 dw) ts tr w r)
                                                            (nts* (difference 17 dw) ts tr w r)
                                                            (ntr* (difference 17 dw) ts tr w r)
                                                            w r)
                                                       'q)
                                                (oracle* (warp (smooth flg2
                                                         (cell flg1
                                                               (difference 4 dw)
                                                               13
                                                               (car msg)))
                                                 ts tr w r)
                                           oracle2)))))))))
  ((disable len app cells)
   (enable warp-app)
   (expand (cells flg1 5 13 msg))))

(disable CDR-APP-CELL-CELLS)
(disable SMOOTH-APP-CELLS)
(disable smooth-app-cell-app-cells) ; used to be loop-smooth-step
(disable CDRN-DW-SMOOTH-CELL)
(disable CDRN-DW-APP-SMOOTH-CELL)
(disable LST*-SMOOTH-CELL)

(prove-lemma loop-killer-1 (rewrite)
  (implies (and (bvp msg)
                (listp msg)
                (listp (cdr msg))
                (numberp ts)
                (numberp tr)
                (not (zerop w))
                (not (zerop r))
                (not (lessp tr ts))
                (lessp tr (plus ts w))
                (rate-proximity w r)

                (numberp nq)
                (not (lessp 3 nq))
                (numberp dw)
                (not (lessp 1 dw))
                (b-xor flg1 flg2))
           (equal (recv (len msg)
                        flg1
                        10
                        (app (det (listn nq 'q) oracle1)
                             (det (warp (cdrn dw
                                              (smooth flg2
                                                      (app (cdr (cells flg1 5 13 msg))
                                                           (listn p2 t))))
                                        ts tr w r)
                                  oracle2)))
                  (recv
                   (len msg)
                   flg1 10
                   (app (det (listn nq 'q) oracle1)
                        (app (det (warp (smooth flg2
                                                (cell flg1
                                                      (difference 4 dw)
                                                      13
                                                      (car msg)))
                                        ts tr w r)
                                  oracle2)
                             (app (det (listn (nqg (nlst* (difference 17 dw) ts tr w r)
                                                   (nts* (difference 17 dw) ts tr w r)
                                                   (ntr* (difference 17 dw) ts tr w r)
                                                   w r)
                                              'q)
                                       (oracle* (warp (smooth flg2
                                                              (cell flg1
                                                                    (difference 4 dw)
                                                                    13
                                                                    (car msg)))
                                                      ts tr w r)
                                                oracle2))
                                  (det (warp (cdrn (dwg (nlst* (difference 17 dw) ts tr w r)
                                                        (nts* (difference 17 dw) ts tr w r)
                                                        (ntr* (difference 17 dw) ts tr w r)
                                                        w r)
                                                   (smooth (b-not (csig flg1 (car msg)))
                                                           (app (cdr (cells (csig flg1 (car msg)) 5
                                                                            13
                                                                            (cdr msg)))
                                                                (listn p2 t))))
                                             (tsg (nlst* (difference 17 dw) ts tr w r)
                                                  (nts* (difference 17 dw) ts tr w r)
                                                  (ntr* (difference 17 dw) ts tr w r)
                                                  w r)
                                             (trg (nlst* (difference 17 dw) ts tr w r)
                                                  (nts* (difference 17 dw) ts tr w r)
                                                  (ntr* (difference 17 dw) ts tr w r)
                                                  w r)
                                             w r)
                                       (oracle* (listn (nqg (nlst* (difference 17 dw) ts tr w r)
                                                            (nts* (difference 17 dw) ts tr w r)
                                                            (ntr* (difference 17 dw) ts tr w r)
                                                            w r)
                                                       'q)
                                                (oracle* (warp (smooth flg2
                                                         (cell flg1
                                                               (difference 4 dw)
                                                               13
                                                               (car msg)))
                                                 ts tr w r)
                                           oracle2)))))))))
  ((enable target)
   (use (loop-killer-1a))))

#|
Observe in the rhs of loop-killer-1 the emergence of an instance of the 
critical part of the lhs:

(app (det (listn nq 'q)
          oracle1)
     (det (warp (cdrn dw
                      (smooth flg2
                              (app (cdr (cells flg1 5 13 msg))
                                   (listn p2 t))))
                ts tr w r)
          oracle2))
From this instance we can read off our induction hypothesis:
|#

(defn loop-ind-hint (nq oracle1 dw flg2 flg1 msg ts tr w r oracle2)
  (if (nlistp msg)
      t
      (if (nlistp (cdr msg))
          t
          (loop-ind-hint (nqg (nlst* (difference 17 dw) ts tr w r)
                              (nts* (difference 17 dw) ts tr w r)
                              (ntr* (difference 17 dw) ts tr w r)
                              w r)
                         (oracle* (warp (smooth flg2
                                                (cell flg1
                                                      (difference 4 dw)
                                                      13
                                                      (car msg)))
                                        ts tr w r)
                                  oracle2)
                         (dwg (nlst* (difference 17 dw) ts tr w r)
                              (nts* (difference 17 dw) ts tr w r)
                              (ntr* (difference 17 dw) ts tr w r)
                              w r)
                         (b-not (csig flg1 (car msg)))
                         (csig flg1 (car msg))
                         (cdr msg)
                         (tsg (nlst* (difference 17 dw) ts tr w r)
                              (nts* (difference 17 dw) ts tr w r)
                              (ntr* (difference 17 dw) ts tr w r)
                              w r)
                         (trg (nlst* (difference 17 dw) ts tr w r)
                              (nts* (difference 17 dw) ts tr w r)
                              (ntr* (difference 17 dw) ts tr w r)
                              w r)
                         w r
                         (oracle* (listn (nqg (nlst* (difference 17 dw) ts tr w r)
                                              (nts* (difference 17 dw) ts tr w r)
                                              (ntr* (difference 17 dw) ts tr w r)
                                              w r)
                                         'q)
                                  (oracle* (warp (smooth flg2
                                                         (cell flg1
                                                               (difference 4 dw)
                                                               13
                                                               (car msg)))
                                                 ts tr w r)
                                           oracle2))))))
                          

#|
In order for this induction to work out, we have to be able to establish that
the instantiations satisfy the hypotheses of the theorem being proved.  We
have made sure of this through the previously proved lemmas NQG-BOUNDS,
DWG-BOUNDS, NOT-LESSP-TRG*-TSG* and LESSP-TRG*-PLUS-W-TSG*.

Loop-killer-1 does not get us back to the induction hypothesis because
we have to scan past the first cell.  So we now continue with our loop
killer development.  We aim for the following rewrite (under appropriate
hyps):

(equal (recv (len msg) flg1 10
             (app (det (listn nq 'q) oracle1)
                  (app (det (warp (smooth flg2 (cell flg1 (difference 4 dw) 13 bit))
                                  ts tr w r)
                            oracle)
                       rest)))
       (cons bit
             (recv (len (cdr msg))
                   (csig flg1 bit)
                   10
                   rest)))

This will be the conclusion of loop-killer-2.  Observe that killer-2 takes up
where killer-1 left off and, in conjunction with the induction hyp, will
reduce the lhs of the induction concl to (cons (car msg) (cdr msg)).

We resume our step-by-step development by considering the lhs recv above and
successively transforming it.

By opening up the lhs recv above we end up with two hard requirements.
The first is that recv reads the correct bit.  We'll call this
loop-killer-2a:
(recv-bit 10
          (scan flg1
                (app (det (listn nq 'q) oracle1)
                     (app (det (warp (smooth flg2
                                             (cell flg1
                                                   (difference 4 dw)
                                                   13
                                                   (car msg)))
                                     ts tr w r)
                               oracle)
                          rest))))
= (car msg)

The second is that it resumes it scan on a string of bits of the
correct parity.
Loop-killer-2b:
(cdrn 10
      (scan flg1
            (app (det (listn nq 'q) oracle1)
                 (app (det (warp (smooth flg2
                                         (cell flg1 (difference 4 dw) 13 (car msg))
                                 ts tr w r)
                           oracle)
                      rest)))))
= (app (listn ??? (csig flg1 x)) rest)
where ??? is some non-zero number we'll determine during the proof below.

It is loop-killer-2b that gets us back to our induction hyp and
so we will work on it first.  As usual the game is to move the app from
its hiding place in cell through smooth, warp, and det and then do some
arithmetic.

Because it is crucial to all that we do henceforth, we are going to
first show what (warp (smooth flg2 (cell flg1 m n bit)) ts tr w r)
looks like.


|#

(prove-lemma app-listn-flg-listn-flg (rewrite)
  (equal (app (listn m flg) (listn n flg))
         (listn (plus m n) flg))
  ((enable listn)))

(prove-lemma cdrn-listn (rewrite)
  (implies (not (lessp n dw))
           (equal (cdrn dw (listn n flg))
                  (listn (difference n dw) flg)))
  ((enable listn)))

; The requirement on n below stems from (a) smooth-flg-listn-flg, as it
; smooths the second subcell, needs to know that n is at least 1 so that it
; can take a 'q out; (b) warp-app-listn-q as it is warping that subcell
; needs to know that n-1 is greater than 2 so it can eat at most two
; signals after the q.

(prove-lemma warp-smooth-cell (rewrite)
  (implies (and (boolp bit)
                (numberp ts)
                (numberp tr)
                (not (zerop w))
                (not (zerop r))
                (not (lessp tr ts))
                (lessp tr (plus ts w))
                (rate-proximity w r)

                (numberp m)
                (numberp n)
                (lessp 3 n)
                (b-xor flg1 flg2))
           (equal (warp (smooth flg2 (cell flg1 m n bit))
                        ts tr w r)
                  (if bit
                      (APP (LISTN (N* M TS TR W R) (B-NOT FLG1))
                           (APP (LISTN (NQG (NLST* M TS TR W R)
                                            (NTS* M TS TR W R)
                                            (NTR* M TS TR W R)
                                            W R)
                                       'Q)
                                (LISTN (N* (DIFFERENCE (SUB1 N)
                                                       (DWG (NLST* M TS TR W R)
                                                            (NTS* M TS TR W R)
                                                            (NTR* M TS TR W R)
                                                            W R))
                                           (TSG (NLST* M TS TR W R)
                                                (NTS* M TS TR W R)
                                                (NTR* M TS TR W R)
                                                W R)
                                           (TRG (NLST* M TS TR W R)
                                                (NTS* M TS TR W R)
                                                (NTR* M TS TR W R)
                                                W R)
                                           W R)
                                       FLG1)))
                      (listn (n* (plus m n) ts tr w r) (b-not flg1)))))
                      
  ((do-not-induct t)
   (enable cell csig smooth-flg-app-listn-flg smooth-flg-app-listn-not-flg
           smooth-flg-listn-flg smooth-flg-listn-not-flg warp-listn)))

; To cdrn through the rhs above we need bounds on n*.  To prove the
; bounds we will have to characterize n* algebraically.  The bounds
; theorems are too weak to prove inductively.

(prove-lemma nendp-alg (rewrite)
  (implies (and (numberp ts)
                (numberp tr+)
                (not (zerop w))
                (lessp ts tr+))
           (equal (nendp n ts tr+ w)
                  (lessp (plus ts (times n w)) tr+))))

(prove-lemma nlst+-ts-plus-ts-w (rewrite)
  (implies (and (numberp n)
                (not (zerop w)))
           (equal (nlst+ n ts (plus ts w) w)
                  (sub1 n)))
  ((expand (nlst+ n ts (plus ts w) w)
           (nlst+ (sub1 n)
                  (plus ts w)
                  (plus ts w)
                  w))))

(prove-lemma nlst+-alg (rewrite)
  (implies (and (numberp n)
                (numberp ts)
                (numberp tr+)
                (not (zerop w))
                (lessp ts tr+))
           (equal (nlst+ n ts tr+ w)
                  (difference n (quotient (difference tr+ ts) w)))))

(disable nlst+-ts-plus-ts-w)

(prove-lemma not-lessp-nts+-ts (rewrite)
  (not (lessp (nts+ n ts tr+ w) ts)))

(prove-lemma nts+-alg (rewrite)
  (implies (and (numberp n)
                (numberp ts)
                (numberp tr+)
                (not (zerop w))
                (not (lessp tr+ ts)))
           (equal (nts+ n ts tr+ w)
                  (if (lessp (plus ts (times n w)) tr+)
                      (plus ts (times n w))
                      (plus ts (times w (quotient (difference tr+ ts) w)))))))

(prove-lemma n*-alg-lemma (rewrite)
  (implies
   (and (numberp x)
        (not (equal r 0))
        (numberp r)
        (not (nendp n ts (plus r ts x) w))
        (numberp n)
        (numberp ts)
        (numberp w)
        (not (equal w 0))
        (not (lessp (plus ts x) ts))
        (lessp (plus ts x) (plus ts w)))
   (equal
    (add1
     (quotient (difference (times w
                                  (nlst+ n ts (plus r ts x) w))
                           (difference (plus r ts x)
                                       (nts+ n ts (plus r ts x) w)))
               r))
    (quotient (difference (times n w) x)
              r))))

(disable nsig*-alg-lemma-hack1)

(prove-lemma n*-alg-hack1 (rewrite)
  (implies (and (nendp n ts (plus r tr) w)
                (numberp n)
                (numberp ts)
                (numberp tr)
                (numberp w)
                (not (equal w 0))
                (numberp r)
                (not (equal r 0))
                (not (lessp tr ts))
                (lessp tr (plus ts w))
                (not (lessp (times n w)
                            (difference tr ts))))
           (equal (lessp (difference (times n w)
                                     (difference tr ts))
                         r)
                  t)))

(prove-lemma n*-alg (rewrite)
  (implies (and (numberp n)
                (numberp ts)
                (numberp tr)
                (not (zerop w))
                (not (zerop r))
                (not (lessp tr ts))
                (lessp tr (plus ts w)))
           (equal (n* n ts tr w r)
                  (quotient (difference (times n w) (difference tr ts))
                            r)))
  ((disable nendp-alg nts+-alg nlst+-alg difference-difference-other difference-difference)))

(disable n*-alg-hack1)
(disable n*-alg)
(disable n*-alg-lemma)
(disable nts+-alg)
(disable nlst+-alg)
(disable nendp-alg)

(disable nsig*-upper-bound-hack1)
(disable nsig*-upper-bound-hack2)
(disable nsig*-upper-bound-hack3)
(disable nsig*-upper-bound-lemma2-equality)

(prove-lemma n*-upper-bound (rewrite)
  (implies (and (numberp n)
                (numberp ts)
                (numberp tr)
                (not (zerop w))
                (not (zerop r))
                (not (lessp tr ts))
                (lessp tr (plus ts w))
                (rate-proximity w r)
                (lessp n 18))
           (not (lessp n (n* n ts tr w r))))
  ((disable plus-commutes1 difference-difference)
   (enable n*-alg)))

(disable nsig*-upper-bound-lemma1)
(disable nsig*-upper-bound-lemma2)

(prove-lemma n*-lower-bound (rewrite)
  (implies (and (numberp n)
                (numberp ts)
                (numberp tr)
                (not (zerop w))
                (not (zerop r))
                (not (lessp tr ts))
                (lessp tr (plus ts w))
                (rate-proximity w r)
                (lessp n 18))
           (not (lessp (n* n ts tr w r) (sub1 (sub1 n)))))
  ((disable nsig*-lower-bound-lemma1 lessp-quotient-to-lessp-times
            quotient times plus difference lessp)
   (use (nsig*-lower-bound-lemma1 (tr-ts (difference tr ts)))
        (nsig*-upper-bound-lemma2-equality (n (sub1 n))))
   (enable n*-alg)))

(disable nsig*-lower-bound-lemma1)

; So now we know n-2 <= (n* n ts tr w r) <= n.

; Now we consider scanning and cdrning.

(prove-lemma len-det (rewrite)
  (equal (len (det lst oracle)) (len lst))
  ((enable det)))

(defn det-listn-hint (nq oracle)

; This is an induction for (det (listn nq 'q) oracle).

  (if (zerop nq)
      t
      (det-listn-hint (sub1 nq) (cdr oracle))))

(defn no (flg nq oracle)
  (if (zerop nq)
      0
      (if (b-xor flg (car oracle))
          nq
          (no flg (sub1 nq) (cdr oracle)))))

; The following lemma is provided by way of explanation.
(prove-lemma no-is-len-scan-det-listn nil
  (implies (numberp nq)
           (equal (no flg nq oracle)
                  (len (scan flg (det (listn nq 'q) oracle)))))
  ((enable listn det scan b-xor)))

(prove-lemma scan-flg-app-listn-not-flg (rewrite)
  (implies (and (lessp 0 n)
                (b-xor flg1 flg2))
           (equal (scan flg1 (app (listn n flg2) rest))
                  (app (listn n flg2) rest)))
  ((enable scan listn)))

(defn scan-oracle (flg nq oracle)
  (if (zerop nq)
      oracle
      (if (b-xor flg (car oracle))
          oracle
          (scan-oracle flg (sub1 nq) (cdr oracle)))))

; The following lemma looks horrible -- the det expression it introduces
; seems a bad trade.  But its oracle is irrelevant elsewhere and its len,
; which is in fact is all we care about, is simple.

(prove-lemma scan-app-det-listn (rewrite)
  (implies (and (lessp 0 n)
                (b-xor flg1 flg2))
           (equal (scan flg1 (app (det (listn nq 'q) oracle)
                                  (app (listn n flg2) rest)))
                  (app (det (listn (no flg1 nq oracle)
                                   'q)
                            (scan-oracle flg1 nq oracle))
                       (app (listn n flg2) rest))))
  ((induct (det-listn-hint nq oracle))
   (enable listn det scan b-xor)))

(disable scan-flg-app-listn-not-flg)

(prove-lemma cdrn-app (rewrite)
  (equal (cdrn n (app a b))
         (if (lessp n (len a))
             (app (cdrn n a) b)
             (cdrn (difference n (len a)) b))))

(prove-lemma not-lessp-no (rewrite)
  (not (lessp n (no flg n oracle))))

(prove-lemma boolp-implies-det-listn (rewrite)
  (implies (boolp flg)
           (equal (det (listn n flg) oracle)
                  (listn n flg)))
  ((enable boolp)))

; We are about to prove the key lemma that determines baud rate.

(prove-lemma len-warp nil
  (equal (len (warp lst ts tr w r))
         (n* (len lst) ts tr w r))
  ((enable warp)))

; To prove n*-plus we have to USE len-warp with an instantiation
; that causes warp-app-listn-q to fire.  Len-warp is of lemma class
; nil so that the equality thus derived stays around.  But it turns out
; that elsewhere in the proof we have to use len-warp as a rewrite rule!
; So we prove an instance of it that suits our purposes.

(prove-lemma n*-plus-lemma (rewrite)
  (equal (len (warp (listn (difference j dwg) f)
                    ts tr w r))
         (n* (difference j dwg)
             ts tr w r))
  ((use (len-warp (lst (listn (difference j dwg) f))))))

; The name n*-plus, below, suggests that the lhs is (n* (plus ...)
; ...) but in fact I named it after the rhs; couldn't bear to rewrite
; the other way.

(prove-lemma n*-plus (rewrite)
  (implies (and (numberp ts)
                (numberp tr)
                (not (zerop w))
                (not (zerop r))
                (not (lessp tr ts))
                (lessp tr (plus ts w))
                (lessp w (times 2 r))
                (lessp r (times 2 w))
                (lessp 2 j)
                (numberp i)
                (numberp j))
           (equal (plus (n* i ts tr w r)
                        (nqg (nlst* i ts tr w r)
                             (nts* i ts tr w r)
                             (ntr* i ts tr w r)
                             w r)
                        (n* (difference j
                                        (dwg (nlst* i ts tr w r)
                                             (nts* i ts tr w r)
                                             (ntr* i ts tr w r)
                                             w r))
                            (tsg (nlst* i ts tr w r)
                                 (nts* i ts tr w r)
                                 (ntr* i ts tr w r)
                                 w r)
                            (trg (nlst* i ts tr w r)
                                 (nts* i ts tr w r)
                                 (ntr* i ts tr w r)
                                 w r)
                            w r))
                  (n* (add1 (plus i j)) ts tr w r)))
  ((use (len-warp (lst (app (listn i t) (cons 'q (listn j f))))))))

(disable n*-plus-lemma)

; If this lemma can be proved for different constants then the
; whole proof can be shifted to those constants.  In particular
; make the replacements indicated below.
; To send cells of size: 32   24  16
;                        31   23  15
;                        16   12   8
;                        15   11   7

(prove-lemma loop-killer-2b (rewrite)
  (implies (and (listp msg)
                (boolp (car msg))
                (bvp (cdr msg))
                (numberp ts)
                (numberp tr)
                (not (zerop w))
                (not (zerop r))
                (not (lessp tr ts))
                (lessp tr (plus ts w))
                (rate-proximity w r)

                (numberp nq)
                (not (lessp 3 nq))
                (numberp dw)
                (not (lessp 1 dw))
                (boolp flg1)
                (b-xor flg1 flg2))
           (equal (cdrn 10
                        (scan flg1
                              (app (det (listn nq 'q) oracle1)
                                   (app (det (warp (smooth flg2 (cell flg1 (difference 4 dw) 13 (car msg)))
                                                   ts tr w r)
                                             oracle2)
                                        rest))))
                  (app (listn (difference (plus (no flg1 nq oracle1)
                                                (n* (difference 17 dw) ts tr w r))
                                          10)
                              (csig flg1 (car msg)))
                       rest)))
  ((enable csig)
   (do-not-induct t)))

(disable n*-plus)
(disable cdrn-app)
(disable scan-app-det-listn)
(disable boolp-implies-det-listn)
(disable warp-smooth-cell)

(prove-lemma car-det-listn (rewrite)
  (equal (car (det (listn n 'q) oracle))
         (if (zerop n)
             0
             (if (car oracle) t f)))
  ((induct (det-listn-hint n oracle))
   (enable listn det)))

(prove-lemma listp-det (rewrite)
  (equal (listp (det lst oracle)) (listp lst))
  ((enable det)))

(prove-lemma car-scan-oracle (rewrite)
  (implies (not (zerop (no flg nq oracle)))
           (iff (car (scan-oracle flg nq oracle)) (b-not flg)))
  ((enable listn listp-listn det b-xor b-not)))

(prove-lemma loop-killer-2a-lemma (rewrite)
  (implies (and (listp msg)
                (boolp (car msg))
                (bvp (cdr msg))
                (numberp ts)
                (numberp tr)
                (not (zerop w))
                (not (zerop r))
                (not (lessp tr ts))
                (lessp tr (plus ts w))
                (rate-proximity w r)

                (numberp nq)
                (not (lessp 3 nq))
                (numberp dw)
                (not (lessp 1 dw))
                (boolp flg1)
                (boolp flg2)
                (b-xor flg1 flg2))
           (equal (car (scan flg1
                             (app (det (listn nq 'q) oracle1)
                                  (app (det (warp (smooth flg2
                                                          (cell flg1
                                                                (difference 4 dw)
                                                                13
                                                                (car msg)))
                                                  ts tr w r)
                                            oracle)
                                       rest))))
                  (b-not flg1)))
  ((enable warp-smooth-cell scan-app-det-listn cdrn-app car-app car-listn
           boolp-implies-det-listn)
   (do-not-induct t)))

(disable car-det-listn)

(prove-lemma equal-difference-0 (rewrite)
  (equal (equal (difference x y) 0)
         (not (lessp y x))))

(prove-lemma loop-killer-2a (rewrite)
  (implies (and (listp msg)
                (boolp (car msg))
                (bvp (cdr msg))
                (numberp ts)
                (numberp tr)
                (not (zerop w))
                (not (zerop r))
                (not (lessp tr ts))
                (lessp tr (plus ts w))
                (rate-proximity w r)

                (numberp nq)
                (not (lessp 3 nq))
                (numberp dw)
                (not (lessp 1 dw))
                (boolp flg1)
                (boolp flg2)
                (b-xor flg1 flg2))
           (equal (recv-bit 10
                            (scan flg1
                                  (app (det (listn nq 'q) oracle1)
                                       (app (det (warp (smooth flg2
                                                               (cell flg1
                                                                     (difference 4 dw)
                                                                     13
                                                                     (car msg)))
                                                       ts tr w r)
                                                 oracle)
                                            rest))))
                  (car msg)))
  ((enable recv-bit car-app car-listn csig)
   (do-not-induct t)))

(disable loop-killer-2a-lemma)

; We also have to take care of the new flg computed by recv:

(prove-lemma loop-killer-2c (rewrite)
  (implies (and (listp msg)
                (boolp (car msg))
                (bvp (cdr msg))
                (numberp ts)
                (numberp tr)
                (not (zerop w))
                (not (zerop r))
                (not (lessp tr ts))
                (lessp tr (plus ts w))
                (rate-proximity w r)

                (numberp nq)
                (not (lessp 3 nq))
                (numberp dw)
                (not (lessp 1 dw)))
           (equal (car (app (listn (difference (plus (no flg1 nq oracle1)
                                                     (n* (difference 17 dw) ts tr w r))
                                               10)
                                   (csig flg1 (car msg)))
                            rest))
                  (csig flg1 (car msg))))
  ((enable car-app car-listn)
   (do-not-induct t)))
          
; Finally, we must show that recv just eats up the leading string of flgs:

(prove-lemma recv-app-listn (rewrite)
  (equal (recv n flg k (app (listn m flg) rest))
         (recv n flg k rest))
  ((expand (recv n flg k (app (listn m flg) rest))
           (recv n flg k rest))))

(prove-lemma loop-killer-2 (rewrite)
  (implies (and (listp msg)
                (boolp (car msg))
                (bvp (cdr msg))
                (numberp ts)
                (numberp tr)
                (not (zerop w))
                (not (zerop r))
                (not (lessp tr ts))
                (lessp tr (plus ts w))
                (rate-proximity w r)

                (numberp nq)
                (not (lessp 3 nq))
                (numberp dw)
                (not (lessp 1 dw))
                (boolp flg1)
                (boolp flg2)
                (b-xor flg1 flg2))
           (equal (recv (len msg) flg1 10
                        (app (det (listn nq 'q) oracle1)
                             (app (det (warp (smooth flg2 (cell flg1 (difference 4 dw) 13 (car msg)))
                                             ts tr w r)
                                       oracle)
                                  rest)))
                  (cons (car msg)
                        (recv (len (cdr msg))
                              (csig flg1 (car msg))
                              10
                              rest))))
  ((expand (recv (len msg) flg1 10
                 (app (det (listn nq 'q) oracle1)
                      (app (det (warp (smooth flg2 (cell flg1 (difference 4 dw) 13 (car msg)))
                                      ts tr w r)
                                oracle)
                           rest))))))

(disable recv-app-listn)

; We now turn to the base case in which msg of of len 1.  Our killer lemma
; will be named loop-killer-0.  This case is special because the cell is not
; always followed by an edge.  We'll do a blow-by-blow derivation of loop-killer-0,
; starting with the lhs of the loop concl; the killer lemma will reduce it to the
; rhs, which is just msg.  

#|
The lhs of loop-killer-0 is initially:
(RECV (LEN MSG)
      FLG1 10
      (APP (DET (LISTN NQ 'Q) ORACLE1)
           (DET (WARP (CDRN DW
                            (SMOOTH FLG2
                                    (APP (CDR (CELLS FLG1 5 13 MSG))
                                         (LISTN P2 T))))
                      TS TR W R)
                ORACLE2)))
where (listp msg) and (nlistp (cdr msg)) are known.
|#

(prove-lemma cdr-app-cell-rest (rewrite)
  (implies (not (zerop m))
           (equal (cdr (app (cell flg1 m n bit)
                            rest))
                  (app (cell flg1 (sub1 m) n bit)
                       rest)))
  ((enable cdr-app cell listn)))

(prove-lemma smooth-app-cell-rest (rewrite)
  (implies (and (not (zerop n))
                (b-xor flg2 flg1))
           (equal (smooth flg2 (app (cell flg1 m n bit) rest))
                  (app (smooth flg2 (cell flg1 m n bit))
                       (smooth (csig flg1 bit) rest))))
  ((enable cell smooth-flg-app-listn-flg smooth-flg-app-listn-not-flg
           smooth-flg-listn-flg smooth-flg-listn-not-flg csig b-not b-xor)))

#|
The lhs is now:
(RECV (LEN MSG)
      FLG1 10
      (APP (DET (LISTN NQ 'Q) ORACLE1)
           (DET (WARP (app (smooth flg2
                                   (cell flg1 (difference 4 dw) 13 (car msg)))
                           (smooth (csig flg1 (car msg)) (listn p2 t)))
                      TS TR W R)
                ORACLE2)))
We want to drive the warp inside the app and we will use warp-app to do it by
TARGETing the warp above.  This introduces a warp-smooth-cell instance, which
we need to analyze, and another warp-app instance about what happens after this
cell.  Normally we know what happens next is an edge, so we have a 'q there and
warp-app-listn-q is used instead of warp-app to do this work.  But here there is
no trailing 'q.  Luckily, we don't need to analyze what goes on after this cell
and so we'll just leave the trailing warp unsimplified.

So the lhs becomes
(RECV (LEN MSG)
      FLG1 10
      (APP (DET (LISTN NQ 'Q) ORACLE1)
           (DET (app (warp (smooth flg2
                                   (cell flg1 (difference 4 dw) 13 (car msg)))
                           ts tr w r)
                     (warp (app (lst* (smooth flg2 (cell flg1 (difference 4 dw) 13 (car msg)))
                                      ts tr w r)
                                (smooth (csig flg1 (car msg)) (listn p2 t)))
                           (ts* (smooth flg2 (cell flg1 (difference 4 dw) 13 (car msg)))
                                ts tr w r)
                           (tr* (smooth flg2 (cell flg1 (difference 4 dw) 13 (car msg)))
                                ts tr w r)
                           w r))
                ORACLE2)))
and we can apply det-app to produce
(RECV (LEN MSG)
      FLG1 10
      (APP (DET (LISTN NQ 'Q) ORACLE1)
           (app (det (warp (smooth flg2
                                   (cell flg1 (difference 4 dw) 13 (car msg)))
                           ts tr w r)
                     oracle2)
                (det ...))))
where we really don't care what is in the last det because it is beyond the
only cell we will read.

But now we can apply loop-killer-2 to this and get (list (car msg)).

|#

; The -0a below reminds us that this rule has a TARGET in it.
(prove-lemma loop-killer-0a nil
  (implies
   (and (listp msg)
        (boolp (car msg))
        (equal (cdr msg) nil)
        (numberp ts)
        (numberp tr)
        (not (equal w 0))
        (numberp w)
        (not (equal r 0))
        (numberp r)
        (not (lessp tr ts))
        (lessp tr (plus ts w))
        (rate-proximity w r)
        (numberp nq)
        (not (lessp 3 nq))
        (numberp dw)
        (not (lessp 1 dw))
        (boolp flg1)
        (boolp flg2)
        (b-xor flg1 flg2))
   (equal
    (recv (len msg)
          flg1 10
          (app (det (listn nq 'q) oracle1)
               (det (target (warp (cdrn dw
                                        (smooth flg2
                                                (app (cdr (cells flg1 5 13 msg))
                                                     (listn p2 t))))
                                  ts tr w r))
                    oracle2)))
    msg))
  ((expand (cells flg1 5 13 msg))
   (disable len)
   (enable cdrn-dw-smooth-cell cdrn-dw-app-smooth-cell warp-app)))

; We now remove the TARGET.

(prove-lemma loop-killer-0 (rewrite)
  (implies
   (and (listp msg)
        (boolp (car msg))
        (equal (cdr msg) nil)
        (numberp ts)
        (numberp tr)
        (not (equal w 0))
        (numberp w)
        (not (equal r 0))
        (numberp r)
        (not (lessp tr ts))
        (lessp tr (plus ts w))
        (rate-proximity w r)
        (numberp nq)
        (not (lessp 3 nq))
        (numberp dw)
        (not (lessp 1 dw))
        (boolp flg1)
        (boolp flg2)
        (b-xor flg1 flg2))
   (equal
    (recv (len msg)
          flg1 10
          (app (det (listn nq 'q) oracle1)
               (det (warp (cdrn dw
                                (smooth flg2
                                        (app (cdr (cells flg1 5 13 msg))
                                             (listn p2 t))))
                          ts tr w r)
                    oracle2)))
    msg))
  ((enable target)
   (use (loop-killer-0a))))

(disable cdr-app-cell-rest)

; The two hypotheses about flg1 and flg2 being boolp were added late in the
; development of the loop theorem and I have to prove that the inductive
; instantiation satisfies them.

(prove-lemma boolp-b-not (rewrite)
  (boolp (b-not x))
  ((enable boolp b-not)))

(prove-lemma boolp-csig (rewrite)
  (implies (boolp flg)
           (boolp (csig flg bit)))
  ((enable boolp b-not)))

(prove-lemma loop (rewrite)
  (implies (and (bvp msg)
                (numberp ts)
                (numberp tr)
                (not (zerop w))
                (not (zerop r))
                (not (lessp tr ts))
                (lessp tr (plus ts w))
                (rate-proximity w r)

                (numberp nq)
                (not (lessp 3 nq))
                (numberp dw)
                (not (lessp 1 dw))
                (boolp flg1)
                (boolp flg2)
                (b-xor flg1 flg2))
           (equal (recv (len msg)
                        flg1
                        10
                        (app (det (listn nq 'q) oracle1)
                             (det (warp (cdrn dw
                                              (smooth flg2
                                                      (app (cdr (cells flg1 5 13 msg))
                                                           (listn p2 t))))
                                        ts tr w r)
                                  oracle2)))
                  msg))
  ((disable cells len)
   (induct (loop-ind-hint nq oracle1 dw flg2 flg1 msg ts tr w r oracle2))))


; The proof idea here is to force the expansion of (bvp msg).  The nil
; case goes through.  The (listp msg) case allows the application of
; top-async-send, which converts the conclusion to an instance of our
; loop form.

(prove-lemma top nil
  (implies (and (bvp msg)
                (numberp ts)
                (numberp tr)
                (not (zerop w))
                (not (zerop r))
                (not (lessp tr ts))
                (lessp tr (plus ts w))
                (rate-proximity w r)
                (numberp p1))
           (equal (recv (len msg)
                        t
                        10
                        (async (send msg p1 5 13 p2)
                               ts tr w r oracle))
                  msg))
  ((disable async)
   (expand (bvp msg))))

; JSM
; July 31, 1991

; That concludes the main theorem.  During the course of discovering
; the proof above I also did some related work that I wish to preserve
; and hence include in this events file.  The first is the development
; of the algebraic identities for the recursive functions used to talk
; about warping.

(enable nendp-alg)

(prove-lemma nts*-alg-lemma1 (rewrite)
  (IMPLIES (AND (NUMBERP X)
                (equal (times n w) (plus r x))
                (NUMBERP N)
                (NUMBERP TS)
                (NOT (EQUAL W 0))
                (NUMBERP W)
                (NOT (EQUAL R 0))
                (NUMBERP R))
           (not (NENDP N TS (PLUS R TS X) W))))


(prove-lemma nts*-alg-lemma2 (rewrite)
  (implies
   (and (numberp x)
        (not (equal r 0))
        (numberp r)
        (not (nendp n ts (plus r ts x) w))
        (numberp n)
        (numberp ts)
        (not (equal w 0))
        (numberp w)
        (not (lessp (plus ts x) ts))
        (lessp (plus ts x) (plus ts w)))
   (equal
    (plus
     (nts+ n ts (plus r ts x) w)
     (times w
            (quotient
             (difference
              (plus r ts x
                    (times r
                           (quotient (difference (times w
                                                        (nlst+ n ts (plus r ts x) w))
                                                 (difference (plus r ts x)
                                                             (nts+ n ts (plus r ts x) w)))
                                     r)))
              (nts+ n ts (plus r ts x) w))
             w)))
    (plus ts
          (times w
                 (quotient (plus x
                                 (times r
                                        (quotient (difference (times n w) x)
                                                  r)))
                           w)))))
  ((enable nlst+-alg nts+-alg)))

(disable difference-difference)
(disable difference-difference-other)

; Acknowledgement:  This lemma was finally stated accurately by Matt Wilding.

(prove-lemma nts*-alg (rewrite)
  (implies (and (numberp n)
                (numberp ts)
                (numberp tr)
                (not (zerop w))
                (not (zerop r))
                (not (lessp tr ts))
                (lessp tr (plus ts w)))
           (equal (nts* n ts tr w r)
                  (plus ts
                        (times w
                               (quotient
                                (difference
                                 (plus tr
                                       (times r
                                              (quotient
                                               (difference (times n w)
                                                           (difference tr ts))
                                               r)))
                                 ts)
                                w)))))
  ((induct (nts* n ts tr w r))
   (disable nendp-alg nts+-alg nlst+-alg)))  

; The following lemma ought to be called ntr*-alg-lemma1 because it is the
; first in direct support of ntr*-alg.  But it is analogous to the ...lemma2
; lemmas of the other algebraic theorems (because its lemma1 needs were met by
; a prior lemma1).

(prove-lemma ntr*-alg-lemma2 (rewrite)
  (implies (and (numberp x)
                (not (equal r 0))
                (numberp r)