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

Event: Start with the initial nqthm theory.

Definition: rate-proximity (w, r) = (((18 ∗ w) ≮ (17 ∗ r)) ∧ ((19 ∗ r) ≮ (18 ∗ w)))

Theorem: plus-add1 (x + (1 + y)) = (1 + (x + y))

Theorem: plus-commutes1 (x + y) = (y + x)

Theorem: plus-commutes2 (x + y + z) = (y + x + z)

Theorem: plus-associates ((x + y) + z) = (x + y + z)

Theorem: times-0 (x ∗ 0) = 0

Theorem: times-non-numberp (z ∉ N) → ((x ∗ z) = 0)

Theorem: times-add1 (x ∗ (1 + y)) = (x + (x ∗ y))

Theorem: times-distributes1 (x ∗ (y + z)) = ((x ∗ y) + (x ∗ z))

Theorem: times-commutes1 (x ∗ y) = (y ∗ x)

Theorem: times-commutes2 (x ∗ y ∗ z) = (y ∗ x ∗ z)

Theorem: times-associates ((x ∗ y) ∗ z) = (x ∗ y ∗ z)

Theorem: times-distributes2 ((x + y) ∗ z) = ((x ∗ z) + (y ∗ z))

Theorem: difference-is-0 (y ≮ x) → ((x − y) = 0)

Theorem: difference-plus-cancellation1 ((i + x) − i) = fix (x)

Theorem: difference-plus-cancellation2 ((i + x) − (i + y)) = (x − y)

Theorem: difference-plus-cancellation3 ((i + j + x) − j ) = (i + x)

Theorem: lessp-remainder ((x mod y) < y) = (y ≄ 0)

Theorem: remainder-quotient-elim (x ∈ N) → (((x mod y) + (y ∗ (x ÷ y))) = x)

Theorem: quotient-plus-times (w ≄ 0) → (((v + (w ∗ i)) ÷ w) = (i + (v ÷ w)))

Definition: len (x) = if x ≃ nil then 0

else 1 + len (cdr (x)) endif

Theorem: equal-len-0 (len (x) = 0) = (x ≃ nil)

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

else cons (car (x), app (cdr (x), y)) endif Theorem: app-cancellation (app (a, b) = app (a, c)) = (b = c)

Theorem: app-assoc app (app (a, b), c) = app (a, app (b, c))

Theorem: len-app len (app (a, b)) = (len (a) + len (b))

Theorem: quotient-x-x (x ≄ 0) → ((x ÷ x) = 1)

Theorem: not-lessp-times-quotient n ≮ (w ∗ (n ÷ w))

Theorem: times-monotonic ((w ≄ 0) ∧ (a < b)) → ((w ∗ a) < (w ∗ b))

Theorem: difference-plus ((x + y) − y) = fix (x)

Theorem: nsig*-alg-lemma-hack1 ((n < ((r + x) ÷ w)) ∧ (w ∈ N) ∧ (w ≠ 0)) → (((ts + (n ∗ w)) < (r + ts + x)) = t)

Theorem: difference-plus-cancellation-4 ((r + ts + x) − (ts + y)) = ((r + x) − y)

Theorem: nts*-alg-lemma2-hack1 ((n < ((r + x) ÷ w)) ∧ (x ∈ N) ∧ (r ≠ 0) ∧ (r ∈ N) ∧ ((n ∗ w) ≮ (r + x)) ∧ (n ∈ N) ∧ (w ≠ 0) ∧ (w ∈ N) ∧ (x < w)) → ((((r + x) ÷ w)

= ((x + (r ∗ (((n ∗ w) − x) ÷ r))) ÷ w)) = t)

Theorem: times-cancellation1 (i ≄ 0) → (((i ∗ j ) = (i ∗ k)) = (fix (j ) = fix (k)))

Theorem: times-cancellation2 (w ≄ 0) → ((((w ∗ x) + (w ∗ y)) = (w ∗ z)) = ((x + y) = fix (z)))

Theorem: difference-difference (b ≮ c) → ((a − (b − c)) = ((a + c) − b))

Theorem: difference-difference-other ((a − b) − c) = (a − (b + c))

Theorem: quotient-plus-times2 (w ≄ 0) → (((v + (i ∗ w) + (w ∗ j )) ÷ w) = (i + j + (v ÷ w)))

Theorem: difference-elim ((i ∈ N) ∧ (i ≮ j )) → ((j + (i − j )) = i)

Theorem: quotient-difference ((w ≄ 0) ∧ (a ≮ (w ∗ b))) → (((a − (w ∗ b)) ÷ w) = ((a ÷ w) − b))

Theorem: quotient-monotonic-lemma ((z1 < y) ∧ (z2 < y) ∧ (y ≠ 0) ∧ (y ∈ N) ∧ (x < v)) → (((z1 + (y ∗ x)) < (z2 + (v ∗ y))) = t)

Theorem: ntr*-alg-lemma2-hack1 ((n < ((r + x) ÷ w)) ∧ (x ∈ N) ∧ (r ≠ 0) ∧ (r ∈ N) ∧ ((ts + (n ∗ w)) ≮ (r + ts + x)) ∧ (n ∈ N) ∧ (ts ∈ N) ∧ (w ≠ 0) ∧ (w ∈ N) ∧ ((ts + x) ≮ ts) ∧ ((ts + x) < (ts + w))) → (((r + ts + x)

= (ts + x + (r ∗ (((n ∗ w) − x) ÷ r)))) = t)

Theorem: not-lessp-times-quotient-other (x ≮ r) → ((r ∗ (x ÷ r)) ≮ r)

Theorem: quotient-monotonic ((w ≄ 0) ∧ (a ≮ b)) → (((a ÷ w) < (b ÷ w)) = f)

Theorem: nlst*-alg-lemma2-hack1 ((x ∈ N) ∧ (r ≠ 0) ∧ (r ∈ N) ∧ ((ts + (n ∗ w)) ≮ (r + ts + x)) ∧ (n ∈ N) ∧ (ts ∈ N) ∧ (w ≠ 0) ∧ (w ∈ N) ∧ ((ts + x) ≮ ts) ∧ ((ts + x) < (ts + w))) → ((((r + x) ÷ w)

+ (((x + (r ∗ (((n ∗ w) − x) ÷ r)))

− (w ∗ ((r + x) ÷ w)))
÷ w))

= ((x + (r ∗ (((n ∗ w) − x) ÷ r))) ÷ w))

Theorem: nsig*-upper-bound-lemma1 (r ≄ 0) → (((n ∗ w) ÷ r) ≮ (((n ∗ w) − (tr − ts)) ÷ r))

Theorem: quotient-times (r ≄ 0) → (((n ∗ r) ÷ r) = fix (n))

Theorem: multiply-both-sides-of-lessp (r ≄ 0) → (((a ∗ r) < (b ∗ r)) = (a < b))

Theorem: lessp-quotient-to-lessp-times-lemma1 ((r ≄ 0) ∧ ((x ÷ r) ≮ n)) → (x ≮ (n ∗ r))

Theorem: lessp-quotient-to-lessp-times-lemma2 ((r ≄ 0) ∧ (x ≮ (n ∗ r))) → ((x ÷ r) ≮ n)

Theorem: lessp-quotient-to-lessp-times (r ≄ 0) → (((x ÷ r) < n) = (x < (n ∗ r)))

Theorem: quotient-plus-times1 (r ≄ 0) → ((((n ∗ r) + z) ÷ r) = (n + (z ÷ r)))

Theorem: equal-times-0 ((i ∗ j ) = 0) = ((i ≃ 0) ∨ (j ≃ 0))

Theorem: nsig*-upper-bound-hack1 ((r ≄ 0) ∧ (r ≮ (18 ∗ delta)) ∧ (n < 18)) → (((n ∗ delta) < r) = t)

Theorem: nsig*-upper-bound-hack2 (((r + r + (17 ∗ r)) ≮ (w + (17 ∗ w))) ∧ ((w + (17 ∗ w)) ≮ (17 ∗ r)) ∧ (w ≄ 0) ∧ (r ≄ 0) ∧ (n ≄ 0) ∧ (n < 18) ∧ (w < r)) → ((w + (w ∗ (n − 1)))

= (((n − 1) ∗ (r − w))

+ (w − ((n − 1) ∗ (r − w)))
+ (w ∗ (n − 1))))

Theorem: quotient-plus-times3 ((x + z + (x ∗ n)) ≄ 0) → (((z + (x ∗ n) + (z ∗ n) + (x ∗ n ∗ n))

÷ (x + z + (x ∗ n)))

= (n + (z ÷ (x + z + (n ∗ x)))))

Theorem: nsig*-upper-bound-hack3 ((z + (x ∗ (n − 1))) < (x + z + (x ∗ (n − 1)))) → ((z < (x + z + (x ∗ (n − 1)))) = t)

Theorem: intro-delta ((w ∈ N) ∧ (w ≮ r)) → (w = (r + (w − r)))

Theorem: nsig*-upper-bound-lemma2-1 ((n ∈ N) ∧ (w ≄ 0) ∧ (r ≄ 0) ∧ rate-proximity (w, r) ∧ (n < 18) ∧ (w ≮ r)) → (((n ∗ w) ÷ r) = n)

Theorem: nsig*-upper-bound-lemma2-2 ((n ∈ N) ∧ (w ≄ 0) ∧ (r ≄ 0) ∧ rate-proximity (w, r) ∧ (n < 18) ∧ (w < r)) → (((n ∗ w) ÷ r) = (n − 1))

Theorem: nsig*-upper-bound-lemma2-equality ((n ∈ N) ∧ (w ≄ 0) ∧ (r ≄ 0) ∧ rate-proximity (w, r) ∧ (n < 18)) → (((n ∗ w) ÷ r)

= if w < r then n − 1 else n endif)

Theorem: nsig*-upper-bound-lemma2 ((n ∈ N) ∧ (w ≄ 0) ∧ (r ≄ 0) ∧ rate-proximity (w, r) ∧ (n < 18)) → (n ≮ ((n ∗ w) ÷ r))

Theorem: nsig*-lower-bound-lemma1 ((r ≄ 0) ∧ (w ≮ tr-ts)) → ((((n ∗ w) − tr-ts) ÷ r) ≮ (((n − 1) ∗ w) ÷ r))

Theorem: lessp-times (n ≄ 0) → ((n ∗ w) ≮ w)

Theorem: plus-cancellation ((i + j ) = (i + k)) = (fix (j ) = fix (k))

Definition: boolp (x) = ((x = t) ∨ (x = f))

Event: Disable boolp.

Theorem: boolp-t (boolp (x) ∧ x) → ((t = x) = t)

Definition: b-not (x) = (¬ x)

Event: Disable b-not.

Definition: b-xor (x, y) = if x then ¬ y

elseif y then t else f endif

Event: Disable b-xor.

Theorem: b-xor-b-not b-xor (x, b-not (x)) ∧ b-xor (b-not (x), x)

Definition: smooth (prev-val, lst) = if lst ≃ nil then nil

elseif b-xor (prev-val, car (lst))

then cons ('q, smooth (car (lst), cdr (lst)))

else cons (car (lst), smooth (car (lst), cdr (lst))) endif Definition: reconcile-signals (a, b) = if a = b then a

else 'q endif

Definition: sig (lst, ts, tr, w) = if lst ≃ nil then 'q

elseif (ts + w) < tr

then reconcile-signals (car (lst), sig (cdr (lst), ts + w, tr, w)) else car (lst) endif

Definition: endp (lst, ts, tr, w) = if lst ≃ nil then t

elseif (ts + w) < tr then endp (cdr (lst), ts + w, tr, w) else f endif

Definition: lst+ (lst, ts, nxtr, w) = if lst ≃ nil then lst

elseif nxtr < (ts + w) then lst

else lst+ (cdr (lst), ts + w, nxtr, w) endif

Definition: ts+ (lst, ts, nxtr, w) = if lst ≃ nil then ts

elseif nxtr < (ts + w) then ts

else ts+ (cdr (lst), ts + w, nxtr, w) endif

Theorem: lst+-weakly-shortens-lst count (lst) ≮ count (lst+ (lst, ts, tr, w))

Theorem: ts+-increases-tr ((¬ endp (lst, ts, r + tr, w)) ∧ (r ≄ 0) ∧ (count (lst) = count (lst+ (lst, ts, r + tr, w)))) → ((((w + ts+ (lst, ts, r + tr, w)) − (r + tr))

< ((ts + w) − tr))

= t)

Definition: warp (lst, ts, tr, w, r) = if (r ≃ 0) ∨ endp (lst, ts, tr + r, w) then nil

else cons (sig (lst, ts, tr + r, w), warp (lst+ (lst, ts, tr + r, w),

ts+ (lst, ts, tr + r, w), tr + r, w, r)) endif

Definition: det (lst, oracle) = if lst ≃ nil then lst

elseif car (lst) = 'q

then cons (if car (oracle) then t else f endif, det (cdr (lst), cdr (oracle))) else cons (car (lst), det (cdr (lst), oracle)) endif

Definition: async (lst, ts, tr, w, r, oracle) = det (warp (smooth (t, lst), ts, tr, w, r), oracle)

Definition: listn (n, value) = if n ≃ 0 then nil

else cons (value, listn (n − 1, value)) endif

Definition: csig (prev-signal, bit) = if bit then prev-signal

else b-not (prev-signal) endif

Definition: cell (prev-signal, n1 , n2 , bit) = app (listn (n1 , b-not (prev-signal)), listn (n2 , csig (prev-signal, bit)))

Definition: cells (prev-signal, n1 , n2 , msg) = if msg ≃ nil then nil

else app (cell (prev-signal, n1 , n2 , car (msg)), cells (csig (prev-signal, car (msg)), n1 , n2 , cdr (msg))) endif

Definition: send (msg, pad1 , n1 , n2 , pad2 ) = app (listn (pad1 , t), app (cells (t, n1 , n2 , msg), listn (pad2 , t)))

Definition: scan (prev-signal, lst) = if lst ≃ nil then nil

elseif b-xor (prev-signal, car (lst)) then lst else scan (prev-signal, cdr (lst)) endif Definition: cdrn (n, lst) = if n ≃ 0 then lst

else cdrn (n − 1, cdr (lst)) endif

Definition: nth (n, lst) = car (cdrn (n, lst))

Definition: recv-bit (k, lst) = if b-xor (car (lst), nth (k, lst)) then t

else f endif

Definition: recv (i, flg, k, lst) = if i ≃ 0 then nil

else cons (recv-bit (k, scan (flg, lst)), recv (i − 1,

nth (k, scan (flg, lst)),

k,

cdrn (k, scan (flg, lst)))) endif

Definition: bvp (x) = if x ≃ nil then x = nil

else boolp (car (x)) ∧ bvp (cdr (x)) endif

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

Event: Disable listn. Event: Disable *1*listn. Event: Disable cell. Event: Disable *1*cell. Event: Disable csig. Event: Disable *1*csig. Event: Disable boolp. Event: Disable smooth. Event: Disable warp. Event: Disable det. Event: Disable recv-bit. Event: Disable scan. Event: Disable send. Theorem: b-xor-x-x ¬ b-xor (x, x)

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

Definition: lst* (lst, ts, tr, w, r) = if (r ≃ 0) ∨ endp (lst, ts, tr + r, w) then lst

else lst* (lst+ (lst, ts, tr + r, w), ts+ (lst, ts, tr + r, w), tr + r, w,

r) endif

Definition: ts* (lst, ts, tr, w, r) = if (r ≃ 0) ∨ endp (lst, ts, tr + r, w) then ts

else ts* (lst+ (lst, ts, tr + r, w), ts+ (lst, ts, tr + r, w), tr + r, w,

r) endif

Definition: tr* (lst, ts, tr, w, r) = if (r ≃ 0) ∨ endp (lst, ts, tr + r, w) then tr

else tr* (lst+ (lst, ts, tr + r, w), ts+ (lst, ts, tr + r, w), tr + r, w,

r) endif

Theorem: not-lessp-ts+ ((tr ≮ ts) ∧ (w ≄ 0)) → (tr ≮ ts+ (lst, ts, tr, w))

Theorem: lessp-ts+ ((¬ endp (lst, ts, tr, w)) ∧ (tr ≮ ts) ∧ (w ≄ 0)) → (tr < (w + ts+ (lst, ts, tr, w)))

Theorem: lst+-app ((¬ endp (lst1 , ts, tr+, w)) ∧ (w ≄ 0)) → (lst+ (app (lst1 , lst2 ), ts, tr+, w) = app (lst+ (lst1 , ts, tr+, w), lst2 ))

Theorem: ts+-app ((¬ endp (lst1 , ts, tr+, w)) ∧ (w ≄ 0)) → (ts+ (app (lst1 , lst2 ), ts, tr+, w) = ts+ (lst1 , ts, tr+, w))

Theorem: sig-app ((¬ endp (lst1 , ts, tr+, w)) ∧ (w ≄ 0)) → (sig (app (lst1 , lst2 ), ts, tr+, w) = sig (lst1 , ts, tr+, w))

Theorem: endp-app ((¬ endp (lst1 , ts, tr+, w)) ∧ (w ≄ 0)) → (¬ endp (app (lst1 , lst2 ), ts, tr+, w))

Definition: target (x) = x

Event: Disable target.

Theorem: warp-app ((ts ∈ N) ∧ (tr ∈ N) ∧ (tr ≮ ts) ∧ (tr < (ts + w)) ∧ (w ≄ 0) ∧ (r ≄ 0)) → (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)))

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

Definition: nlst+ (n, ts, tr, w) = if n ≃ 0 then n

elseif tr < (ts + w) then n

else nlst+ (n − 1, ts + w, tr, w) endif

Theorem: len-lst+ len (lst+ (lst, ts, tr, w)) = nlst+ (len (lst), ts, tr, w)

Definition: nts+ (n, ts, tr, w) = if n ≃ 0 then ts

elseif tr < (ts + w) then ts

else nts+ (n − 1, ts + w, tr, w) endif

Theorem: len-ts+ ts+ (lst, ts, tr, w) = nts+ (len (lst), ts, tr, w)

Definition: nendp (n, ts, tr, w) = if n ≃ 0 then t

elseif (ts + w) < tr then nendp (n − 1, ts + w, tr, w) else f endif

Theorem: len-endp endp (lst, ts, tr, w) = nendp (len (lst), ts, tr, w)

Theorem: lessp-nlst+ n ≮ nlst+ (n, ts, tr, w)

Theorem: nlst+-equal-n (nlst+ (n, ts, r + tr, w) = n) = ((n ≃ 0) ∨ ((r + tr) < (ts + w)))

Definition: nlst* (n, ts, tr, w, r) = if (r ≃ 0) ∨ nendp (n, ts, tr + r, w) then n

else nlst* (nlst+ (n, ts, tr + r, w), nts+ (n, ts, tr + r, w), tr + r, w,

r) endif

Theorem: len-lst* len (lst* (lst, ts, tr, w, r)) = nlst* (len (lst), ts, tr, w, r)

Definition: nts* (n, ts, tr, w, r) = if (r ≃ 0) ∨ nendp (n, ts, tr + r, w) then ts

else nts* (nlst+ (n, ts, tr + r, w), nts+ (n, ts, tr + r, w), tr + r, w,

r) endif Theorem: len-ts* ts* (lst, ts, tr, w, r) = nts* (len (lst), ts, tr, w, r)

Definition: ntr* (n, ts, tr, w, r) = if (r ≃ 0) ∨ nendp (n, ts, tr + r, w) then tr

else ntr* (nlst+ (n, ts, tr + r, w), nts+ (n, ts, tr + r, w), tr + r, w,

r) endif

Theorem: len-tr* tr* (lst, ts, tr, w, r) = ntr* (len (lst), ts, tr, w, r)

Theorem: len-listn len (listn (n, flg)) = fix (n)

Definition: lastn (n, lst) = if n = len (lst) then lst

elseif lst ≃ nil then lst else lastn (n, cdr (lst)) endif

Definition: tailp (x, lst) = if x = lst then t

elseif lst ≃ nil then f else tailp (x, cdr (lst)) endif

Theorem: tailp-transitive (tailp (x, y) ∧ tailp (y, z)) → tailp (x, z)

Theorem: tailp-lst+ tailp (lst+ (lst, ts, tr, w), lst)

Theorem: tailp-lst* tailp (lst* (lst, ts, tr, w, r), lst)

Theorem: len-lastn len (lastn (n, lst)) = if len (lst) < n then 0

else fix (n) endif

Theorem: tailp-implies-lastn-len tailp (x, y) → (lastn (len (x), y) = x)

Theorem: lst*-is-lastn lastn (len (lst* (lst, ts, tr, w, r)), lst) = lst* (lst, ts, tr, w, r)

Definition: properp (x) = if x ≃ nil then x = nil

else properp (cdr (x)) endif

Theorem: lastn-nil (properp (lst) ∧ (len (lst) < n)) → (lastn (n, lst) = nil)

Theorem: properp-listn properp (listn (n, flg))

Theorem: lastn-listn ((n ∈ N) ∧ (k ∈ N) ∧ (k ≮ n)) → (lastn (n, listn (k, flg)) = listn (n, flg))

Theorem: lessp-nlst* n ≮ nlst* (n, ts, tr, w, r)

Theorem: lst*-listn (n ∈ N) → (lst* (listn (n, flg), ts, tr, w, r) = listn (nlst* (n, ts, tr, w, r), flg))

Definition: n* (n, ts, tr, w, r) = if (r ≃ 0) ∨ nendp (n, ts, tr + r, w) then 0

else 1 + n* (nlst+ (n, ts, tr + r, w), nts+ (n, ts, tr + r, w), tr + r, w,

r) endif

Theorem: not-lessp-nts+ ((tr ≮ ts) ∧ (w ≄ 0)) → (tr ≮ nts+ (n, ts, tr, w))

Theorem: lessp-nts+ ((¬ nendp (n, ts, tr, w)) ∧ (tr ≮ ts) ∧ (w ≄ 0)) → (tr < (w + nts+ (n, ts, tr, w)))

Theorem: lst+-listn ((n ∈ N) ∧ (¬ nendp (n, ts, tr+, w)) ∧ (w ≄ 0)) → (lst+ (listn (n, flg), ts, tr+, w) = listn (nlst+ (n, ts, tr+, w), flg))

Theorem: sig-listn ((r ≠ 0) ∧ (r ∈ N) ∧ (¬ nendp (n, ts, r + tr, w)) ∧ (n ∈ N) ∧ (ts ∈ N) ∧ (tr ∈ N) ∧ (tr ≮ ts) ∧ (tr < (ts + w)) ∧ (w ≠ 0) ∧ (w ∈ N)) → (sig (listn (n, flg), ts, r + tr, w) = flg)

Theorem: warp-listn ((n ∈ N) ∧ (ts ∈ N) ∧ (tr ∈ N) ∧ (tr ≮ ts) ∧ (tr < (ts + w)) ∧ (w ≄ 0) ∧ (r ≄ 0)) → (warp (listn (n, flg), ts, tr, w, r) = listn (n* (n, ts, tr, w, r), flg))

Theorem: lst+-app-gap ((ts ∈ N) ∧ (tr+ ∈ N) ∧ nendp (len (pad), ts, tr+, w)) → (lst+ (app (pad, lst), ts, tr+, w)

= lst+ (lst, ts + (len (pad) ∗ w), tr+, w))

Theorem: nts+-app-gap ((ts ∈ N) ∧ (tr+ ∈ N) ∧ (k ∈ N) ∧ nendp (k, ts, tr+, w)) → (nts+ (n + k, ts, tr+, w) = nts+ (n, ts + (k ∗ w), tr+, w))

Theorem: warp-app-gap ((ts ∈ N) ∧ (r ≄ 0) ∧ nendp (len (pad), ts, r + tr, w)) → (warp (app (pad, lst), ts, tr, w, r)

= if nendp (len (pad) + len (lst), ts, r + tr, w) then nil

else cons (sig (app (pad, lst), ts, r + tr, w),

warp (lst+ (lst, ts + (len (pad) ∗ w), r + tr, w), nts+ (len (lst),

ts + (len (pad) ∗ w), r + tr, w), r + tr, w, r)) endif)

Theorem: nendp-nlst* ((ts ∈ N) ∧ (tr ∈ N) ∧ (r ≄ 0) ∧ (w ≄ 0) ∧ (tr ≮ ts) ∧ (tr < (ts + w))) → nendp (nlst* (k, ts, tr, w, r), nts* (k, ts, tr, w, r), r + ntr* (k, ts, tr, w, r), w)

Definition: nqg (k, ts, tr, w, r) = if (r + tr) < (w + ts + (w ∗ k))

then if (r + r + tr) < (w + ts + (w ∗ k)) then 3

else 2 endif else 1 endif

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

Definition: dwg (k, ts, tr, w, r) = if (r + tr) < (ts + w + (k ∗ w)) then if (r + r + tr) < (ts + w + w + (k ∗ w)) then 0

else 1 endif elseif (r + tr) = (ts + w + (k ∗ w)) then 0 elseif ((ts + w + (k ∗ w)) < (r + tr))

∧ ((r + tr) < (ts + w + w + (k ∗ w))) then 0 elseif (r + tr) < (ts + w + w + (k ∗ w)) then 0 else 1 endif

Definition: tsg (k, ts, tr, w, r) = (ts + (w ∗ k) + w + (w ∗ dwg (k, ts, tr, w, r)))

; the eaten element of n2

Definition: trg (k, ts, tr, w, r) = (tr + (r ∗ nqg (k, ts, tr, w, r)))

; the qs

Theorem: not-lessp-ntr*-nts* ((ts ∈ N) ∧ (tr ∈ N) ∧ (tr ≮ ts) ∧ (tr < (ts + w)) ∧ (w ≄ 0)) → (ntr* (k, ts, tr, w, r) ≮ nts* (k, ts, tr, w, r))

Theorem: lessp-ntr*-nts* ((ts ∈ N) ∧ (tr ∈ N) ∧ (tr ≮ ts) ∧ (tr < (ts + w)) ∧ (w ≄ 0)) → (ntr* (k, ts, tr, w, r) < (w + nts* (k, ts, tr, w, r)))

Theorem: nendp-is-usually-f ((ts ∈ N) ∧ (tr ∈ N) ∧ (w ≠ 0) ∧ (w ∈ N) ∧ (r ≠ 0) ∧ (r ∈ N) ∧ (tr < (ts + w)) ∧ (w < (2 ∗ r)) ∧ (r < (2 ∗ w)) ∧ (2 < k)) → (¬ nendp (k, ts, 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.

Theorem: lessp-plus-nts*-times-w-nlst*-plus-r-ntr*-lemma (nendp (k, ts, r + tr, w) ∧ (ts ∈ N) ∧ (tr ∈ N) ∧ (w ≠ 0) ∧ (w ∈ N) ∧ (r ≠ 0) ∧ (r ∈ N) ∧ ((r + tr) ≮ ts) ∧ (tr < (ts + w))) → ((r + tr) ≮ (ts + (k ∗ w)))

Theorem: not-lessp-plus-r-ntr*-plus-nts*-times-w-nlst* ((ts ∈ N) ∧ (tr ∈ N) ∧ (w ≄ 0) ∧ (r ≄ 0) ∧ (tr ≮ ts) ∧ (tr < (ts + w))) → ((r + ntr* (k, ts, tr, w, r))

≮ (nts* (k, ts, tr, w, r) + (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.

Theorem: helper1 ((ts ∈ N) ∧ (tr ∈ N) ∧ (w ≠ 0) ∧ (w ∈ N) ∧ (r ≠ 0) ∧ (r ∈ N) ∧ (tr ≮ ts)

∧ (tr < (ts + w)) ∧ (w < (2 ∗ r)) ∧ (r < (2 ∗ w)) ∧ listp (rest) ∧ ((ts + w + w) < (r + tr)) ∧ ((ts + w) < (r + tr)) ∧ ((r + tr) ≮ (ts + w + w))) → (warp (lst+ (rest, ts + w + w, r + tr, w),

nts+ (len (rest), ts + w + w, r + tr, w), r + tr, w, r)

= warp (rest, ts + w + w, r + tr, w, r))

Theorem: helper5 ((ts ∈ N) ∧ (tr ∈ N) ∧ (k ∈ N) ∧ (w ≠ 0) ∧ (w ∈ N) ∧ (r ≠ 0) ∧ (r ∈ N) ∧ (tr ≮ ts) ∧ (tr < (ts + w)) ∧ (w < (2 ∗ r)) ∧ (r < (2 ∗ w)) ∧ listp (rest) ∧ listp (cdr (rest)) ∧ (((k − 1) − 1) = 0) ∧ ((ts + w + w) < (r + tr)) ∧ ((ts + w) < (r + tr)) ∧ ((r + tr) < (ts + w + (k ∗ w))) ∧ ((r + r + tr) ≮ (ts + w + (k ∗ w))) ∧ ((r + r + tr) < (ts + w + w + (k ∗ w)))) → (warp (cons ('q, rest), ts + (k ∗ w), r + tr, w, r)

= cons ('q, warp (rest, ts + w + (k ∗ w), tr + (2 ∗ r), w, r)))

Theorem: helper7 ((ts ∈ N) ∧ (tr ∈ N) ∧ (w ≠ 0) ∧ (w ∈ N) ∧ (r ≠ 0)

∧ (r ∈ N) ∧ (tr ≮ ts) ∧ (tr < (ts + w)) ∧ (w < (2 ∗ r)) ∧ (r < (2 ∗ w)) ∧ listp (rest) ∧ listp (cdr (rest)) ∧ ((ts + w) < (r + tr)) ∧ ((r + tr) ≮ (ts + w + w)) ∧ ((r + tr) < (ts + w + w + w))) → (warp (cons (flg1 , cons ('q, rest)), ts, tr, w, r)

= cons ('q, warp (rest, ts + w + w, r + tr, w, r)))

Theorem: helper8 ((ts ∈ N) ∧ (tr ∈ N) ∧ (w ≠ 0) ∧ (w ∈ N) ∧ (r ≠ 0) ∧ (r ∈ N) ∧ (tr ≮ ts) ∧ (tr < (ts + w)) ∧ (w < (2 ∗ r)) ∧ (r < (2 ∗ w)) ∧ listp (rest) ∧ listp (cdr (rest)) ∧ ((ts + w) < (r + tr)) ∧ ((r + tr) ≮ (ts + w)) ∧ ((r + tr) ≠ (ts + w)) ∧ ((r + tr) ≮ (ts + w + w))) → (warp (cons ('q, rest), ts, tr, w, r)

= cons ('q, warp (cdr (rest), ts + w + w, r + tr, w, r)))

Theorem: helper9 ((ts ∈ N) ∧ (tr ∈ N) ∧ (w ≠ 0) ∧ (w ∈ N) ∧ (r ≠ 0) ∧ (r ∈ N) ∧ (tr ≮ ts) ∧ (tr < (ts + w)) ∧ (w < (r + r)) ∧ (r < (2 ∗ w))

∧ listp (rest) ∧ listp (cdr (rest)) ∧ ((ts + w) < (r + tr)) ∧ ((r + tr) < (ts + w + w)) ∧ ((r + r + tr) ≮ (ts + w + w)) ∧ ((r + r + tr) ≮ (ts + w + w + w))) → (warp (cons (flg1 , cons ('q, rest)), ts, tr, w, r)

= cons ('q,

cons ('q,

warp (cdr (rest), ts + w + w + w, r + r + tr, w, r))))

Theorem: helper10 ((ts ∈ N) ∧ (tr ∈ N) ∧ (w ≠ 0) ∧ (w ∈ N) ∧ (r ≠ 0) ∧ (r ∈ N) ∧ (tr ≮ ts) ∧ (tr < (ts + w)) ∧ (w < (r + r)) ∧ (r < (2 ∗ w)) ∧ listp (rest) ∧ listp (cdr (rest)) ∧ ((ts + w) < (r + tr)) ∧ ((r + tr) < (ts + w + w)) ∧ ((r + r + tr) ≮ (ts + w + w)) ∧ ((r + r + tr) < (ts + w + w + w))) → (warp (cons (flg1 , cons ('q, rest)), ts, tr, w, r)

= cons ('q, cons ('q, warp (rest, ts + w + w, r + r + tr, w, r))))

Theorem: helper11 ((ts ∈ N) ∧ (tr ∈ N) ∧ (w ≠ 0) ∧ (w ∈ N) ∧ (r ≠ 0) ∧ (r ∈ N) ∧ (tr ≮ ts)

∧ (tr < (ts + w)) ∧ (w < (r + r)) ∧ (r < (2 ∗ w)) ∧ listp (rest) ∧ listp (cdr (rest)) ∧ ((ts + w) < (r + tr)) ∧ ((r + tr) < (ts + w + w)) ∧ ((r + r + tr) < (ts + w + w)) ∧ ((r + r + tr) < (ts + w + w + w))) → (warp (cons (flg1 , cons ('q, rest)), ts, tr, w, r)

= cons ('q,

cons ('q,

cons ('q, warp (rest, ts + w + w, tr + (3 ∗ r), w, r)))))

Theorem: lessp-times-18 listp (msg) → ((18 ∗ len (msg)) ≮ 18)

Theorem: listn-add1 listn (1 + n, flg) = cons (flg, listn (n, flg))

Theorem: helper14 ((ts ∈ N) ∧ (tr ∈ N) ∧ (w ≠ 0) ∧ (w ∈ N) ∧ (r ≠ 0) ∧ (r ∈ N) ∧ (tr ≮ ts) ∧ (tr < (ts + w)) ∧ (w < (r + r)) ∧ (r < (2 ∗ w)) ∧ listp (rest) ∧ listp (cdr (rest)) ∧ ((r + tr) ≮ (ts + w)) ∧ ((r + tr) < (ts + w + w))) → (warp (cons ('q, rest), ts, tr, w, r)

= cons ('q, warp (rest, ts + w, r + tr, w, r)))

Theorem: helper15 ((ts ∈ N) ∧ (tr ∈ N) ∧ (w ≠ 0) ∧ (w ∈ N) ∧ (r ≠ 0)

∧ (r ∈ N) ∧ (tr ≮ ts) ∧ (tr < (ts + w)) ∧ (w < (r + r)) ∧ (r < (2 ∗ w)) ∧ listp (rest) ∧ listp (cdr (rest)) ∧ ((r + tr) < (ts + w)) ∧ ((r + r + tr) ≮ (ts + w)) ∧ ((r + r + tr) < (ts + w + w))) → (warp (cons ('q, rest), ts, tr, w, r)

= cons ('q, cons ('q, warp (rest, ts + w, r + r + tr, w, r))))

Theorem: warp-app-across-gap ((ts ∈ N) ∧ (tr ∈ N) ∧ (k ∈ N) ∧ (w ≄ 0) ∧ (r ≄ 0) ∧ (tr ≮ ts) ∧ (tr < (ts + w)) ∧ (w < (2 ∗ r)) ∧ (r < (2 ∗ w)) ∧ listp (rest) ∧ listp (cdr (rest)) ∧ nendp (k, ts, r + tr, w)) → (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)))

Event: Disable helper1.

Event: Disable helper5.

Event: Disable helper7.

Event: Disable helper8.

Event: Disable helper9.

Event: Disable helper10.

Event: Disable helper11.

Event: Disable helper14.

Event: Disable helper15.

Event: Disable nqg.

Event: Disable dwg.

Event: Disable tsg.

Event: Disable trg.

Definition: 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)

Definition: 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)

Definition: 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)

Definition: 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)

Theorem: lessp-2-len-implies-listps (2 < len (x)) → (listp (x) ∧ listp (cdr (x)))

Theorem: warp-app-listn-q1 ((ts ∈ N) ∧ (tr ∈ N) ∧ (w ≄ 0) ∧ (r ≄ 0) ∧ (tr ≮ ts)

∧ (tr < (ts + w)) ∧ (w < (2 ∗ r)) ∧ (r < (2 ∗ w)) ∧ (n1 ∈ N) ∧ (2 < len (rest))) → (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))))

Theorem: warp-app-listn-q ((ts ∈ N) ∧ (tr ∈ N) ∧ (w ≄ 0) ∧ (r ≄ 0) ∧ (tr ≮ ts) ∧ (tr < (ts + w)) ∧ (w < (2 ∗ r)) ∧ (r < (2 ∗ w)) ∧ (n1 ∈ N) ∧ (2 < len (rest))) → (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))))

Event: Disable listn-add1.

Event: Disable warp-app-across-gap.

Event: Disable warp-app-gap.

Event: Disable warp-listn.

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

Theorem: smooth-congruence (¬ b-xor (flg1 , flg2 )) → ((smooth (flg2 , rest) = smooth (flg1 , rest)) = t)

Theorem: smooth-flg-app-listn-flg (¬ b-xor (flg1 , flg2 )) → (smooth (flg1 , app (listn (p1 , flg2 ), rest))

= app (listn (p1 , flg2 ), smooth (flg1 , rest)))

Theorem: listp-app-listn listp (app (listn (n, flg), rest)) = ((n ≄ 0) ∨ listp (rest))

Theorem: listp-cells listp (cells (flg, 5, 13, msg)) = listp (msg)

Event: Disable listp-app-listn.

Theorem: car-app car (app (a, b)) = if listp (a) then car (a)

else car (b) endif

Theorem: listp-listn listp (listn (n, flg)) = (n ≄ 0)

Theorem: car-cells listp (msg) → (car (cells (flg, 5, 13, msg)) = b-not (flg))

Event: Disable car-app.

Theorem: top-smooth-step listp (msg) → (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))))))

Event: Disable smooth-flg-app-listn-flg.

Event: Disable car-cells.

Event: Disable listp-cells.

; Now past the det

Definition: oracle* (lst, oracle) = if lst ≃ nil then oracle

elseif car (lst) = 'q then oracle* (cdr (lst), cdr (oracle)) else oracle* (cdr (lst), oracle) endif

Event: Disable oracle*.

Theorem: det-app det (app (lst1 , lst2 ), oracle) = app (det (lst1 , oracle), det (lst2 , oracle* (lst1 , oracle)))

Theorem: det-listn (flg ≠ 'q) → (det (listn (n, flg), oracle) = listn (n, flg))

Theorem: oracle*-listn (flg ≠ 'q) → (oracle* (listn (n, flg), oracle) = oracle)

; So now we combine all these.

Theorem: len-smooth len (smooth (flg, lst)) = len (lst)

Theorem: cdr-app cdr (app (a, b)) = if listp (a) then app (cdr (a), b)

else cdr (b) endif

Theorem: top-async-send-lemma1 listp (msg) → (2 < len (cdr (cells (t, 5, 13, msg))))

Event: Disable cdr-app.

Theorem: top-async-send (bvp (msg) ∧ listp (msg) ∧ (ts ∈ N) ∧ (tr ∈ N) ∧ (w ≄ 0) ∧ (r ≄ 0) ∧ (tr ≮ ts) ∧ (tr < (ts + w)) ∧ rate-proximity (w, r) ∧ (p1 ∈ N)) → (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)))))

Event: Disable top-async-send-lemma1.

Event: Disable top-smooth-step.

; Now we get recv to eat the header.

Theorem: scan-app-listn scan (flg, app (listn (n, flg), rest)) = scan (flg, rest)

Theorem: top-recv-step recv (n, t, k, app (listn (p1 , t), rest)) = recv (n, t, k, rest)

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

Theorem: nqg-bounds (0 < nqg (n, ts, tr, w, r)) ∧ (3 ≮ nqg (n, ts, tr, w, r))

Theorem: dwg-bounds 1 ≮ dwg (n, ts, tr, w, r)

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

Theorem: not-lessp-trg*-tsg* ((ts ∈ N) ∧ (tr ∈ N) ∧ (n ∈ N) ∧ (w ≄ 0) ∧ (r ≄ 0) ∧ (tr ≮ ts) ∧ (tr < (ts + w))

∧ (w < (2 ∗ r)) ∧ (r < (2 ∗ w))) → (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))

Theorem: lessp-trg*-plus-w-tsg* ((ts ∈ N) ∧ (tr ∈ N) ∧ (n ∈ N) ∧ (w ≄ 0) ∧ (r ≄ 0) ∧ (tr ≮ ts) ∧ (tr < (ts + w)) ∧ (w < (2 ∗ r)) ∧ (r < (2 ∗ w))) → (trg (nlst* (n, ts, tr, w, r), nts* (n, ts, tr, w, r), ntr* (n, ts, tr, w, r), w, r)

< (w + tsg (nlst* (n, ts, tr, w, r), nts* (n, ts, tr, w, r), ntr* (n, ts, tr, w, r), w, r)))

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

Theorem: cdr-app-cell-cells (n1 ≄ 0) → (cdr (app (cell (flg1 , n1 , n2 , bit), cells (flg2 , n1 , n2 , msg)))

= app (cell (flg1 , n1 − 1, n2 , bit), cells (flg2 , n1 , n2 , msg)))

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

Theorem: smooth-flg-listn-flg (¬ b-xor (flg1 , flg2 )) → (smooth (flg1 , listn (n, flg2 )) = listn (n, flg2 ))

Theorem: not-b-xor-b-not b-xor (flg1 , flg2 ) → ((¬ b-xor (flg1 , b-not (flg2 ))) ∧ (¬ b-xor (b-not (flg2 ), flg1 )))

Theorem: smooth-flg-app-listn-not-flg ((n ≄ 0) ∧ b-xor (flg1 , flg2 )) → (smooth (flg1 , app (listn (n, flg2 ), rest))

= app (smooth (flg1 , listn (n, flg2 )), smooth (flg2 , rest)))

Theorem: smooth-app-cell-app-cells ((n1 ≄ 0) ∧ b-xor (flg1 , flg2 )) → (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)))))

Event: Disable smooth-flg-listn-flg.

Event: Disable smooth-flg-app-listn-not-flg.

; If we had loop-stoppers on iff rules we could use an iff and be more efficient.

Theorem: b-xor-commutes b-xor (x, y) → b-xor (y, x)

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

Theorem: listp-smooth-cell (m ≄ 0) → listp (smooth (flg1 , cell (flg2 , m, n, bit)))

Theorem: cdrn-dw-app-smooth-cell ((m ≄ 0) ∧ (dw ∈ N) ∧ (1 ≮ dw)) → (cdrn (dw, app (smooth (flg1 , cell (flg2 , m, n, bit)), rest))

= app (cdrn (dw, smooth (flg1 , cell (flg2 , m, n, bit))), rest))

Theorem: car-listn car (listn (n, flg)) = if n ≃ 0 then 0

else flg endif

Theorem: cdrn-dw-smooth-cell ((m ≄ 0) ∧ (dw ∈ N) ∧ (1 ≮ dw) ∧ b-xor (flg1 , flg2 )) → (cdrn (dw, smooth (flg2 , cell (flg1 , m, n, car (msg))))

= smooth (flg2 , cell (flg1 , m − dw, n, car (msg))))

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

Theorem: len-cell len (cell (flg, m, n, bit)) = (m + n)

Theorem: add1-plus-12-difference-4-dw (1 ≮ dw) → ((1 + (12 + (4 − dw))) = (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."

Theorem: lst*-is-lastn-nlst* lst* (lst, ts, tr, w, r) = lastn (nlst* (len (lst), ts, tr, w, r), lst)

Theorem: lastn-app (len (b) ≮ n) → (lastn (n, app (a, b)) = lastn (n, b))

Theorem: not-lessp-2-nlst* ((ts ∈ N) ∧ (tr ∈ N) ∧ (w ≄ 0) ∧ (r ≄ 0) ∧ (tr ≮ ts) ∧ (tr < (ts + w)) ∧ (w < (2 ∗ r)) ∧ (r < (2 ∗ w))) → (2 ≮ nlst* (n, ts, tr, w, r))

Theorem: smooth-flg-listn-not-flg ((n ≄ 0) ∧ b-xor (flg1 , flg2 )) → (smooth (flg1 , listn (n, flg2 )) = cons ('q, listn (n − 1, flg2 )))

Event: Disable smooth-flg-listn-not-flg.

Theorem: lst*-smooth-cell ((ts ∈ N) ∧ (tr ∈ N) ∧ (w ≄ 0) ∧ (r ≄ 0) ∧ (tr ≮ ts) ∧ (tr < (ts + w)) ∧ (w < (2 ∗ r)) ∧ (r < (2 ∗ w)) ∧ (m ≄ 0)

∧ (n ∈ N) ∧ (2 < n) ∧ b-xor (flg1 , flg2 )) → (lst* (smooth (flg2 , cell (flg1 , m, n, bit)), ts, tr, w, r)

= listn (nlst* (m + n, ts, tr, w, r), csig (flg1 , bit)))

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

Theorem: cdr-listn cdr (listn (n, flg)) = if n ≃ 0 then 0

else listn (n − 1, flg) endif

Event: Disable cdr-listn.

Theorem: smooth-app-cells (listp (msg) ∧ (m ≄ 0)) → (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)))))

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

Theorem: lessp-2-len-cdr-cells listp (msg) → (2 < len (cdr (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

Theorem: app-listn-0 app (listn (0, flg), rest) = rest

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

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

Event: Disable cdr-app-cell-cells.

Event: Disable smooth-app-cells.

Event: Disable smooth-app-cell-app-cells.

; used to be loop-smooth-step

Event: Disable cdrn-dw-smooth-cell.

Event: Disable cdrn-dw-app-smooth-cell.

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

Definition: loop-ind-hint (nq, oracle1 , dw, flg2 , flg1 , msg, ts, tr, w, r, oracle2 ) = if msg ≃ nil then t

elseif cdr (msg) ≃ nil then t

else loop-ind-hint (nqg (nlst* (17 − dw, ts, tr, w, r), nts* (17 − dw, ts, tr, w, r), ntr* (17 − dw, ts, tr, w, r), w, r),

oracle* (warp (smooth (flg2 ,

cell (flg1 , 4 − dw,

                                           13,

car (msg))),

ts, tr, w, r),

oracle2 ), dwg (nlst* (17 − dw, ts, tr, w, r), nts* (17 − dw, ts, tr, w, r), ntr* (17 − dw, ts, tr, w, r), w, r),

b-not (csig (flg1 , car (msg))),

csig (flg1 , car (msg)),

cdr (msg),

tsg (nlst* (17 − dw, ts, tr, w, r), nts* (17 − dw, ts, tr, w, r), ntr* (17 − dw, ts, tr, w, r), w, r),

trg (nlst* (17 − dw, ts, tr, w, r), nts* (17 − dw, ts, tr, w, r), ntr* (17 − dw, ts, tr, w, r), w, r),

w, r, oracle* (listn (nqg (nlst* (17 − dw, ts, tr, w, r),

nts* (17 − dw, ts, tr, w, r), ntr* (17 − dw, ts, tr, w, r), w, r),

                               'q),

oracle* (warp (smooth (flg2 ,

cell (flg1 , 4 − dw,

                                                  13,

car (msg))),

ts, tr, w, r), oracle2 ))) endif

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

|#

Theorem: app-listn-flg-listn-flg app (listn (m, flg), listn (n, flg)) = listn (m + n, flg)

Theorem: cdrn-listn (n ≮ dw) → (cdrn (dw, listn (n, flg)) = listn (n − dw, flg))

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

Theorem: warp-smooth-cell (boolp (bit) ∧ (ts ∈ N) ∧ (tr ∈ N) ∧ (w ≄ 0) ∧ (r ≄ 0) ∧ (tr ≮ ts) ∧ (tr < (ts + w)) ∧ rate-proximity (w, r) ∧ (m ∈ N) ∧ (n ∈ N) ∧ (3 < n) ∧ b-xor (flg1 , flg2 )) → (warp (smooth (flg2 , cell (flg1 , m, n, bit)), ts, tr, w, r)

= if bit

then 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* ((n − 1)

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

else listn (n* (m + n, ts, tr, w, r), b-not (flg1 )) endif)

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

Theorem: nendp-alg ((ts ∈ N) ∧ (tr+ ∈ N) ∧ (w ≄ 0) ∧ (ts < tr+)) → (nendp (n, ts, tr+, w) = ((ts + (n ∗ w)) < tr+))

Theorem: nlst+-ts-plus-ts-w ((n ∈ N) ∧ (w ≄ 0)) → (nlst+ (n, ts, ts + w, w) = (n − 1))

Theorem: nlst+-alg ((n ∈ N) ∧ (ts ∈ N) ∧ (tr+ ∈ N) ∧ (w ≄ 0) ∧ (ts < tr+)) → (nlst+ (n, ts, tr+, w) = (n − ((tr+ − ts) ÷ w)))

Event: Disable nlst+-ts-plus-ts-w.

Theorem: not-lessp-nts+-ts nts+ (n, ts, tr+, w) ≮ ts Theorem: nts+-alg ((n ∈ N) ∧ (ts ∈ N) ∧ (tr+ ∈ N) ∧ (w ≄ 0) ∧ (tr+ ≮ ts)) → (nts+ (n, ts, tr+, w)

= if (ts + (n ∗ w)) < tr+ then ts + (n ∗ w) else ts + (w ∗ ((tr+ − ts) ÷ w)) endif)

Theorem: n*-alg-lemma ((x ∈ N) ∧ (r ≠ 0) ∧ (r ∈ N) ∧ (¬ nendp (n, ts, r + ts + x, w)) ∧ (n ∈ N) ∧ (ts ∈ N) ∧ (w ∈ N) ∧ (w ≠ 0) ∧ ((ts + x) ≮ ts) ∧ ((ts + x) < (ts + w))) → ((1 + (((w ∗ nlst+ (n, ts, r + ts + x, w))

− ((r + ts + x) − nts+ (n, ts, r + ts + x, w))) ÷ r))

= (((n ∗ w) − x) ÷ r))

Event: Disable nsig*-alg-lemma-hack1.

Theorem: n*-alg-hack1 (nendp (n, ts, r + tr, w) ∧ (n ∈ N) ∧ (ts ∈ N) ∧ (tr ∈ N) ∧ (w ∈ N) ∧ (w ≠ 0) ∧ (r ∈ N) ∧ (r ≠ 0) ∧ (tr ≮ ts) ∧ (tr < (ts + w)) ∧ ((n ∗ w) ≮ (tr − ts))) → ((((n ∗ w) − (tr − ts)) < r) = t)

Theorem: n*-alg ((n ∈ N) ∧ (ts ∈ N) ∧ (tr ∈ N) ∧ (w ≄ 0) ∧ (r ≄ 0)

∧ (tr ≮ ts) ∧ (tr < (ts + w))) → (n* (n, ts, tr, w, r) = (((n ∗ w) − (tr − ts)) ÷ r))

Event: Disable n*-alg-hack1.

Event: Disable n*-alg.

Event: Disable n*-alg-lemma.

Event: Disable nts+-alg.

Event: Disable nlst+-alg.

Event: Disable nendp-alg.

Event: Disable nsig*-upper-bound-hack1.

Event: Disable nsig*-upper-bound-hack2.

Event: Disable nsig*-upper-bound-hack3.

Event: Disable nsig*-upper-bound-lemma2-equality.

Theorem: n*-upper-bound ((n ∈ N) ∧ (ts ∈ N) ∧ (tr ∈ N) ∧ (w ≄ 0) ∧ (r ≄ 0) ∧ (tr ≮ ts) ∧ (tr < (ts + w)) ∧ rate-proximity (w, r) ∧ (n < 18)) → (n ≮ n* (n, ts, tr, w, r))

Event: Disable nsig*-upper-bound-lemma1.

Event: Disable nsig*-upper-bound-lemma2.

Theorem: n*-lower-bound ((n ∈ N) ∧ (ts ∈ N) ∧ (tr ∈ N) ∧ (w ≄ 0) ∧ (r ≄ 0) ∧ (tr ≮ ts) ∧ (tr < (ts + w)) ∧ rate-proximity (w, r) ∧ (n < 18)) → (n* (n, ts, tr, w, r) ≮ ((n − 1) − 1))

Event: Disable nsig*-lower-bound-lemma1.

; So now we know n-2 <= (n* n ts tr w r) <= n.
; Now we consider scanning and cdrning.

Theorem: len-det len (det (lst, oracle)) = len (lst)

Definition: det-listn-hint (nq, oracle) = if nq ≃ 0 then t

else det-listn-hint (nq − 1, cdr (oracle)) endif

Definition: no (flg, nq, oracle) = if nq ≃ 0 then 0

elseif b-xor (flg, car (oracle)) then nq else no (flg, nq − 1, cdr (oracle)) endif

; The following lemma is provided by way of explanation.

Theorem: no-is-len-scan-det-listn (nq ∈ N) → (no (flg, nq, oracle) = len (scan (flg, det (listn (nq, 'q), oracle))))

Theorem: scan-flg-app-listn-not-flg ((0 < n) ∧ b-xor (flg1 , flg2 )) → (scan (flg1 , app (listn (n, flg2 ), rest)) = app (listn (n, flg2 ), rest))

Definition: scan-oracle (flg, nq, oracle)

= if nq ≃ 0 then oracle elseif b-xor (flg, car (oracle)) then oracle else scan-oracle (flg, nq − 1, cdr (oracle)) endif

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

Theorem: scan-app-det-listn ((0 < n) ∧ b-xor (flg1 , flg2 )) → (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)))

Event: Disable scan-flg-app-listn-not-flg.

Theorem: cdrn-app cdrn (n, app (a, b)) = if n < len (a) then app (cdrn (n, a), b)

else cdrn (n − len (a), b) endif

Theorem: not-lessp-no n ≮ no (flg, n, oracle)

Theorem: boolp-implies-det-listn boolp (flg) → (det (listn (n, flg), oracle) = listn (n, flg))

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

Theorem: len-warp len (warp (lst, ts, tr, w, r)) = n* (len (lst), ts, tr, w, r)

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

Theorem: n*-plus-lemma len (warp (listn (j − dwg, f), ts, tr, w, r)) = n* (j − dwg, ts, tr, w, r)

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

Theorem: n*-plus ((ts ∈ N) ∧ (tr ∈ N) ∧ (w ≄ 0) ∧ (r ≄ 0) ∧ (tr ≮ ts) ∧ (tr < (ts + w)) ∧ (w < (2 ∗ r)) ∧ (r < (2 ∗ w)) ∧ (2 < j ) ∧ (i ∈ N) ∧ (j ∈ N)) → ((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* (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* (1 + (i + j ), ts, tr, w, r))

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

Theorem: loop-killer-2b (listp (msg) ∧ boolp (car (msg)) ∧ bvp (cdr (msg)) ∧ (ts ∈ N) ∧ (tr ∈ N) ∧ (w ≄ 0) ∧ (r ≄ 0) ∧ (tr ≮ ts) ∧ (tr < (ts + w)) ∧ rate-proximity (w, r) ∧ (nq ∈ N) ∧ (3 ≮ nq) ∧ (dw ∈ N) ∧ (1 ≮ dw) ∧ boolp (flg1 ) ∧ b-xor (flg1 , flg2 )) → (cdrn (10,

scan (flg1 ,

app (det (listn (nq, 'q), oracle1 ),

app (det (warp (smooth (flg2 ,

cell (flg1 , 4 − dw, 13, car (msg))), ts, tr, w, r),

oracle2 ), rest))))

= app (listn ((no (flg1 , nq, oracle1 ) + n* (17 − dw, ts, tr, w, r))

                − 10,

csig (flg1 , car (msg))), rest))

Event: Disable n*-plus.

Event: Disable cdrn-app.

Event: Disable scan-app-det-listn.

Event: Disable boolp-implies-det-listn.

Event: Disable warp-smooth-cell.

Theorem: car-det-listn car (det (listn (n, 'q), oracle)) = if n ≃ 0 then 0

elseif car (oracle) then t else f endif

Theorem: listp-det listp (det (lst, oracle)) = listp (lst)

Theorem: car-scan-oracle (no (flg, nq, oracle) ≄ 0) → (car (scan-oracle (flg, nq, oracle)) ↔ b-not (flg))

Theorem: loop-killer-2a-lemma (listp (msg) ∧ boolp (car (msg)) ∧ bvp (cdr (msg)) ∧ (ts ∈ N) ∧ (tr ∈ N) ∧ (w ≄ 0) ∧ (r ≄ 0) ∧ (tr ≮ ts) ∧ (tr < (ts + w)) ∧ rate-proximity (w, r) ∧ (nq ∈ N) ∧ (3 ≮ nq) ∧ (dw ∈ N) ∧ (1 ≮ dw) ∧ boolp (flg1 ) ∧ boolp (flg2 ) ∧ b-xor (flg1 , flg2 )) → (car (scan (flg1 ,

app (det (listn (nq, 'q), oracle1 ), app (det (warp (smooth (flg2 ,

cell (flg1 , 4 − dw, 13, car (msg))), ts, tr, w, r),

oracle), rest))))

= b-not (flg1 ))

Event: Disable car-det-listn.

Theorem: equal-difference-0 ((x − y) = 0) = (y ≮ x)

Theorem: loop-killer-2a (listp (msg) ∧ boolp (car (msg)) ∧ bvp (cdr (msg)) ∧ (ts ∈ N) ∧ (tr ∈ N) ∧ (w ≄ 0) ∧ (r ≄ 0) ∧ (tr ≮ ts) ∧ (tr < (ts + w)) ∧ rate-proximity (w, r) ∧ (nq ∈ N) ∧ (3 ≮ nq) ∧ (dw ∈ N) ∧ (1 ≮ dw) ∧ boolp (flg1 ) ∧ boolp (flg2 ) ∧ b-xor (flg1 , flg2 )) → (recv-bit (10,

scan (flg1 ,

app (det (listn (nq, 'q), oracle1 ),

app (det (warp (smooth (flg2 ,

cell (flg1 , 4 − dw,

                                            13,

car (msg))),

ts, tr, w, r),

oracle), rest))))

= car (msg))

Event: Disable loop-killer-2a-lemma.

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

Theorem: loop-killer-2c (listp (msg) ∧ boolp (car (msg)) ∧ bvp (cdr (msg)) ∧ (ts ∈ N) ∧ (tr ∈ N) ∧ (w ≄ 0) ∧ (r ≄ 0) ∧ (tr ≮ ts) ∧ (tr < (ts + w)) ∧ rate-proximity (w, r) ∧ (nq ∈ N) ∧ (3 ≮ nq) ∧ (dw ∈ N) ∧ (1 ≮ dw)) → (car (app (listn ((no (flg1 , nq, oracle1 ) + n* (17 − dw, ts, tr, w, r))

                − 10,

csig (flg1 , car (msg))), rest)) = csig (flg1 , car (msg)))

; Finally, we must show that recv just eats up the leading string of flgs:

Theorem: recv-app-listn recv (n, flg, k, app (listn (m, flg), rest)) = recv (n, flg, k, rest)

Theorem: loop-killer-2 (listp (msg) ∧ boolp (car (msg)) ∧ bvp (cdr (msg)) ∧ (ts ∈ N) ∧ (tr ∈ N) ∧ (w ≄ 0) ∧ (r ≄ 0)

∧ (tr ≮ ts) ∧ (tr < (ts + w)) ∧ rate-proximity (w, r) ∧ (nq ∈ N) ∧ (3 ≮ nq) ∧ (dw ∈ N) ∧ (1 ≮ dw) ∧ boolp (flg1 ) ∧ boolp (flg2 ) ∧ b-xor (flg1 , flg2 )) → (recv (len (msg),

flg1 ,

         10,

app (det (listn (nq, 'q), oracle1 ),

app (det (warp (smooth (flg2 , cell (flg1 , 4 − dw, 13, car (msg))), ts, tr, w, r),

oracle), rest)))

= cons (car (msg), recv (len (cdr (msg)), csig (flg1 , car (msg)), 10, rest)))

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

|#

Theorem: cdr-app-cell-rest (m ≄ 0) → (cdr (app (cell (flg1 , m, n, bit), rest))

= app (cell (flg1 , m − 1, n, bit), rest))

Theorem: smooth-app-cell-rest ((n ≄ 0) ∧ b-xor (flg2 , flg1 )) → (smooth (flg2 , app (cell (flg1 , m, n, bit), rest))

= app (smooth (flg2 , cell (flg1 , m, n, bit)), smooth (csig (flg1 , bit), rest)))

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

Theorem: loop-killer-0a (listp (msg) ∧ boolp (car (msg)) ∧ (cdr (msg) = nil) ∧ (ts ∈ N) ∧ (tr ∈ N) ∧ (w ≠ 0) ∧ (w ∈ N) ∧ (r ≠ 0) ∧ (r ∈ N) ∧ (tr ≮ ts) ∧ (tr < (ts + w)) ∧ rate-proximity (w, r) ∧ (nq ∈ N) ∧ (3 ≮ nq) ∧ (dw ∈ N) ∧ (1 ≮ dw) ∧ boolp (flg1 ) ∧ boolp (flg2 ) ∧ b-xor (flg1 , flg2 )) → (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)

; We now remove the TARGET.

Theorem: loop-killer-0 (listp (msg) ∧ boolp (car (msg)) ∧ (cdr (msg) = nil) ∧ (ts ∈ N) ∧ (tr ∈ N) ∧ (w ≠ 0) ∧ (w ∈ N) ∧ (r ≠ 0) ∧ (r ∈ N) ∧ (tr ≮ ts) ∧ (tr < (ts + w)) ∧ rate-proximity (w, r) ∧ (nq ∈ N) ∧ (3 ≮ nq) ∧ (dw ∈ N) ∧ (1 ≮ dw) ∧ boolp (flg1 ) ∧ boolp (flg2 ) ∧ b-xor (flg1 , flg2 )) → (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)

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

Theorem: boolp-b-not boolp (b-not (x))

Theorem: boolp-csig boolp (flg) → boolp (csig (flg, bit))

Theorem: loop (bvp (msg) ∧ (ts ∈ N) ∧ (tr ∈ N) ∧ (w ≄ 0) ∧ (r ≄ 0) ∧ (tr ≮ ts) ∧ (tr < (ts + w)) ∧ rate-proximity (w, r) ∧ (nq ∈ N) ∧ (3 ≮ nq) ∧ (dw ∈ N) ∧ (1 ≮ dw) ∧ boolp (flg1 ) ∧ boolp (flg2 ) ∧ b-xor (flg1 , flg2 )) → (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)

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

Theorem: top (bvp (msg) ∧ (ts ∈ N) ∧ (tr ∈ N) ∧ (w ≄ 0) ∧ (r ≄ 0) ∧ (tr ≮ ts) ∧ (tr < (ts + w)) ∧ rate-proximity (w, r) ∧ (p1 ∈ N)) → (recv (len (msg), t, 10, async (send (msg, p1 , 5, 13, p2 ), ts, tr, w, r, oracle))

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

Event: Enable nendp-alg.

Theorem: nts*-alg-lemma1 ((x ∈ N) ∧ ((n ∗ w) = (r + x)) ∧ (n ∈ N) ∧ (ts ∈ N) ∧ (w ≠ 0) ∧ (w ∈ N)

∧ (r ≠ 0) ∧ (r ∈ N)) → (¬ nendp (n, ts, r + ts + x, w))

Theorem: nts*-alg-lemma2 ((x ∈ N) ∧ (r ≠ 0) ∧ (r ∈ N) ∧ (¬ nendp (n, ts, r + ts + x, w)) ∧ (n ∈ N) ∧ (ts ∈ N) ∧ (w ≠ 0) ∧ (w ∈ N) ∧ ((ts + x) ≮ ts) ∧ ((ts + x) < (ts + w))) → ((nts+ (n, ts, r + ts + x, w)

+ (w ∗ (((r + ts + x + (r ∗ (((w ∗ nlst+ (n, ts, r + ts + x, w)) − ((r + ts + x)

− nts+ (n,

ts, r + ts + x, w)))

÷ r))) − nts+ (n, ts, r + ts + x, w)) ÷ w)))

= (ts + (w ∗ ((x + (r ∗ (((n ∗ w) − x) ÷ r)))

÷ w))))

Event: Disable difference-difference.

Event: Disable difference-difference-other.

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

Theorem: nts*-alg ((n ∈ N) ∧ (ts ∈ N) ∧ (tr ∈ N)

∧ (w ≄ 0) ∧ (r ≄ 0) ∧ (tr ≮ ts) ∧ (tr < (ts + w))) → (nts* (n, ts, tr, w, r)

= (ts + (w ∗ (((tr + (r ∗ (((n ∗ w) − (tr − ts))

÷ r)))

− ts)
÷ w))))

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

Theorem: ntr*-alg-lemma2 ((x ∈ N) ∧ (r ≠ 0) ∧ (r ∈ N) ∧ (¬ nendp (n, ts, r + ts + x, w)) ∧ (n ∈ N) ∧ (ts ∈ N) ∧ (w ≠ 0) ∧ (w ∈ N) ∧ ((ts + x) ≮ ts) ∧ ((ts + x) < (ts + w))) → ((r

+ ts + x + (r ∗ (((w ∗ nlst+ (n, ts, r + ts + x, w)) − ((r + ts + x)

− nts+ (n, ts, r + ts + x, w))) ÷ r)))

= (ts + x + (r ∗ (((n ∗ w) − x) ÷ r))))

Theorem: ntr*-alg ((n ∈ N) ∧ (ts ∈ N) ∧ (tr ∈ N) ∧ (w ≄ 0) ∧ (r ≄ 0) ∧ (tr ≮ ts) ∧ (tr < (ts + w))) → (ntr* (n, ts, tr, w, r)

= (tr + (r ∗ (((n ∗ w) − (tr − ts)) ÷ r))))

Theorem: nlst*-alg-lemma2 ((x ∈ N) ∧ (r ≠ 0) ∧ (r ∈ N) ∧ (¬ nendp (n, ts, r + ts + x, w)) ∧ (n ∈ N) ∧ (ts ∈ N) ∧ (w ≠ 0) ∧ (w ∈ N) ∧ ((ts + x) ≮ ts) ∧ ((ts + x) < (ts + w))) → ((nlst+ (n, ts, r + ts + x, w)

− (((ts + x + (r ∗ (((n ∗ w) − x) ÷ r))) − nts+ (n, ts, r + ts + x, w)) ÷ w))

= (n − ((x + (r ∗ (((n ∗ w) − x) ÷ r))) ÷ w)))

Theorem: nlst*-alg ((n ∈ N) ∧ (ts ∈ N) ∧ (tr ∈ N) ∧ (w ≄ 0) ∧ (r ≄ 0) ∧ (tr ≮ ts) ∧ (tr < (ts + w))) → (nlst* (n, ts, tr, w, r)

= (n − (((tr + (r ∗ (((n ∗ w) − (tr − ts)) ÷ r)))

− ts)
÷ w)))

Event: Disable nendp-alg.

Event: Disable nlst+-alg.

Event: Disable nts+-alg.

Event: Disable nts*-alg-lemma1.

Event: Disable nts*-alg-lemma2-hack1.

Event: Disable nts*-alg-lemma2.

Event: Disable nts*-alg.

Event: Disable ntr*-alg-lemma2-hack1.

Event: Disable ntr*-alg-lemma2.

Event: Disable ntr*-alg.

Event: Disable nlst*-alg-lemma2-hack1.

Event: Disable nlst*-alg-lemma2.

Event: Disable nlst*-alg.

; The second piece of preserved work is the proof that deterministic fuzzy edge
; detection is impossible.
; An Aside:  Does the Treatment of (X) Preclude Edge Detection?
; May 28, 1991.
; (Note: In this section we adopt the convention that when a list is
; treated as a series of signals arriving at a pin then the last
; (right-most) element of the list is the first signal to arrive.
; This convention is at variance with that used throughout the rest of
; our asychronous work, where the signals arrive in the order in which
; they appear in the list.  We adopted this convention to make our
; pictures of edges and our register chains look traditional.  None of
; the work in this section is used outside of this section.  The whole
; point is to explain why we use Q (which is nondeterministically t or
; f on each occurrence) rather than X (which, in the words of Bishop
; Brock, is "your worst nightmare").)
; I have been trying for some weeks, off and on, to write an edge
; detector that could tolerate an (X) at the edge and never be
; undefined.  I have proved that is impossible.  The formalization
; and proof are given below, after an informal sketch of the problem.
; Let a "fuzzy edge" be a sequence of signals that is initially
; all f's and then becomes all t's -- except that between
; the last f and the first t is an x, i.e.,

;    - - - - - - -
;                  \
;                    - - - - - - -
; ...t t t t t t t x f f f f f f f ...
; A "well-defined" circuit is one that always returns either t or f.
; That is, it never answers x.
; Finally, an "edge detector" is a sequential circuit that sits on the
; line listening to the incoming f's and reporting "no edge yet"; if the
; line eventually goes high, the circuit eventually reports "an edge
; came by."  I am willing to give the circuit designer as many leading
; f's and trailing t's as he wants and I don't care how long after the
; edge he says "an edge came by" as long as he is correct.
; So a "well-defined fuzzy edge detector" is one that always returns t
; or f and successfully detects a fuzzy edge eventually.
; Initially I thought I could build a well-defined fuzzy edge
; detector.  For example, chain three successive pulses into registers
; so that you could see "t x f" in registers r0, r1, and r2, and then
; see if r0 is t while r2 is f.  Well, that doesn't work because at
; the moment before you see "t x f" you see "x f f" and the logic
; described would produce an x.  So you say to yourself, ``there is
; only one x in the sequence, so if I widen the window to "t t x f f"
; in registers r0 through r4, and look for, say, r0 and -r3 or r1 and
; -r4, then that bad case, namely "t x f f f" won't get me.''  But now
; "x f f f f" will get you.  Nevertheless, the feeling persisted that
; since I could have as many t's and f's as I wanted and there was
; only one x, I could somehow (perhaps by majority voting?) protect
; myself from that x while still finding the edge.
; I prove below a theorem that tells me that you can't build a
; well-defined fuzzy edge detector.
; My theorem actually does not consider sequential circuits but
; instead addresses itself to combinational circuits that have access
; to an arbitrarily wide "window" in the signal.  One could imagine,
; for example, that the sequential circuit just chains the signal
; through a sequence of k registers, constantly maintaining a window k
; wide on the signal and testing that window with combinational logic.
; If a fuzzy edge comes through that window, the combinational logic
; circuit must detect it.

; There are k+2 different views of a fuzzy edge in a window k wide.  For
; example, if k is 6 then the 8 views are:
;   f f f f f f
;   x f f f f f
;   t x f f f f
;   t t x f f f
;   t t t x f f
;   t t t t x f
;   t t t t t x
;   t t t t t t
; I limit myself to combinational expressions in F-AND and F-NOT
; because I believe the rest of the primitives can be defined in terms
; of those two (and here I mean not just for T and F but also for X).
; I define an interpreter for F-AND and F-NOT expressions with
; variables v0, v1, ..., vk, where the variables address the
; corresponding positions in the window.  Call such an expression "a
; candidate fuzzy edge detector of width k."
; I prove that if a candidate fuzzy edge detector of width k is
; well-defined (T or F) on all k+2 views of the window, then it is
; constant!
; This work relies upon certain definitions from Warren and Bishop's
; stuff, namely:
; From (note-lib "/usr/home/brock/constants/lsi/reg")

Event: Add the shell x, with recognizer function symbol xp and no accessors.

; From (note-lib "/usr/home/brock/constants/lsi/reg")

Definition: f-not (a) = if boolp (a) then ¬ a

else x endif

; From (note-lib "/usr/home/brock/constants/lsi/reg")

Definition: f-and (a, b) = if (a = f) ∨ (b = f) then f elseif (a = t) ∧ (b = t) then t else x endif

Definition: exprp (x) = if x ≃ nil then (x = 't) ∨ (x = 'f) ∨ (x ∈ N)

elseif car (x) = 'f-not then exprp (cadr (x))

∧ (cddr (x) = nil)

else (car (x) = 'f-and)

∧ exprp (cadr (x)) ∧ exprp (caddr (x)) ∧ (cdddr (x) = nil) endif

Definition: max-var (x) = if x ≃ nil

then if (x = 't) ∨ (x = 'f) then 0

else x endif elseif car (x) = 'f-not then max-var (cadr (x)) else max (max-var (cadr (x)), max-var (caddr (x))) endif

Definition: width (x) = (1 + max-var (x))

; Any expression is a candidate for an edge detector of size k, where
; k is the width of the expression.
; To evaluate an expression of a given width, k, we must have a vector
; of length k which assigns values (positionally) to each of the k
; variables.  By convention, if a vector is insufficiently long or
; contains a non-Boolean assignment to a variable, we will assume it
; assigns (X) to that variable.  Thus, the empty vector is a
; convenient way to map all variables to (X).  This is unimportant in
; our main result but is used in a subsequent result that shows
; that an expression that is defined on nil is constant.

Definition: var-val (n, vector) = if boolp (nth (n, vector)) then nth (n, vector)

else x endif

; Here is the interpreter for expressions wrt a given vector:

Definition: val (x, vector) = if x ≃ nil

then if x = 't then t elseif x = 'f then f else var-val (x, vector) endif

elseif car (x) = 'f-not then f-not (val (cadr (x), vector)) else f-and (val (cadr (x), vector), val (caddr (x), vector)) endif

Event: Enable boolp.

Theorem: var-val-is-x-or-boolp (var-val (x, vector) ≠ x) → boolp (var-val (x, vector))

Theorem: val-is-x-or-boolp (val (x, vector) ≠ x) → boolp (val (x, vector))

Event: Disable boolp.

; We need to generate the complete list of k+2 views of an edge coming
; thorugh a window of width k.  We enumerate the edges as suggested
; below, e.g., 0 is the one containing all f's, k+1 contains all t's,
; etc.
; 5   t t t t
; 4   t t t x
; 3   t t x f
; 2   t x f f
; 1   x f f f
; 0   f f f f
; The order of enumeration is important to our proof.  In particular,
; if you think of the edges enumerated as above, then an integer, e.g.,
; 3, can either represent the given edge or all the edges at and below that
; one.  And we sometimes induct on these integers to build the set of all
; edges.  We use the property of the enumeration that if a variable is
; Boolean (never x) in all the edges at or below i, then it is in fact
; constant.

Definition: edge (k, i) = if k ≃ 0 then nil

elseif i < k then app (edge (k − 1, i), list (f)) elseif i = k then app (edge (k − 1, i), list (x)) else app (edge (k − 1, i − 1), list (t)) endif

; Note: In the original development of this theorem, we used the
; natural numbers to encode both edges and sets of edges.  This
; restricted our evaluation function to work only on edges and thus
; restricted what we could say about the value of expressions.  We
; therefore decided to represent edges as bit vectors as above.  But
; to preserve exactly the structure of the proof, we will prove the
; old definition of var-val in var-val-edge below.

Theorem: length-edge len (edge (k, i)) = fix (k)

Event: Enable cdrn-app.

Theorem: cdrn-too-big (n ≮ len (lst)) → (¬ listp (cdrn (n, lst)))

Theorem: lessp-n-1 (n < 1) = (n ≃ 0)

Theorem: nth-edge ((n ∈ N) ∧ (k ∈ N) ∧ (k ≄ 0)) → (car (cdrn (n, edge (k, i)))

= if n < k

then if (1 + n) < i then t elseif (1 + n) = i then x else f endif

else 0 endif)

Theorem: var-val-edge ((n ∈ N) ∧ (k ∈ N) ∧ (k ≄ 0) ∧ (n < k)) → (var-val (n, edge (k, i))

= if n < k

then if (1 + n) < i then t elseif (1 + n) = i then x else f endif

else x endif)

Event: Disable var-val.

Event: Disable edge.

; We now develop the idea that an expression is "well-defined", i.e.,
; its value is never x on any edge of the appropriate size.  To

; do this we have to check the value on every edge.

Definition: all-edges (k, i) = if i ≃ 0 then list (edge (k, 0))

else cons (edge (k, i), all-edges (k, i − 1)) endif

; The following function determines that x is well-defined for all
; vectors in a given set test-set:

Definition: well-defined1 (x, test-set) = if test-set ≃ nil then t

else (val (x, car (test-set)) ≠ x)

∧ well-defined1 (x, cdr (test-set)) endif

; So an expression is well-defined if it is well-defined on all the edges
; of the appropriate size.

Definition: well-defined (x) = well-defined1 (x, all-edges (width (x), 1 + width (x)))

; The theorem we wish to prove is:
; (implies (and (exprp x)
;               (well-defined x))
;          (equal (val x (edge (width x) i))
;                 (val x (edge (width x) 0))))
; That is, if an expression is well-defined on all edges, then it is
; constant on all edges.

Theorem: val-on-successive-edges-is-constant-when-defined (exprp (x) ∧ (i ≄ 0) ∧ (k ≮ width (x)) ∧ (val (x, edge (k, i)) ≠ x) ∧ (val (x, edge (k, i − 1)) ≠ x)) → (val (x, edge (k, i)) = val (x, edge (k, i − 1)))

Theorem: numberp-max-var exprp (x) → (max-var (x) ∈ N)

Theorem: val-is-x-or-boolp-2 ((val (x, vector) ≠ x) ∧ val (x, vector)) → (val (x, vector) = t)

Theorem: everything-defined-at-0 ((zero ≃ 0) ∧ exprp (x) ∧ (k ≮ width (x))) → (val (x, edge (k, zero)) ≠ x)

Theorem: well-defined1-is-a-universal-quantifier (exprp (x) ∧ (k ≮ width (x)) ∧ well-defined1 (x, all-edges (k, i)) ∧ (i ≮ j )) → (val (x, edge (k, j )) ≠ x)

Theorem: edge-at-non-numberp (i ∉ N) → (edge (k, i) = edge (k, 0))

Theorem: well-defined1-implies-constant (exprp (x) ∧ (k ≮ width (x)) ∧ well-defined1 (x, all-edges (k, i)) ∧ (i ≮ j )) → (val (x, edge (k, j )) = val (x, edge (k, 0)))

Theorem: edge-beyond-max ((1 + k) < i) → (edge (k, i) = edge (k, 1 + k))

Theorem: well-defined-implies-constant (exprp (x) ∧ well-defined (x)) → (val (x, edge (width (x), i)) = val (x, edge (width (x), 0)))

; Here is a related result.  It says that if an expression is defined
; on the vector that assigns x to each input, then the expression is
; constant.

Theorem: non-x-on-nil-implies-constant (exprp (x) ∧ (val (x, nil) ≠ x)) → (val (x, vector) = val (x, nil))

; Some stronger conjectures are not valid.  Consider for example,
; "When x is well-defined (on all edges) then x is constant."  This
; conjecture is falsified by the expression '(f-and (f-not 0) 1).
; As can be determined by r-loop, (well-defined '(f-and (f-not 0) 1)).
; But (val '(f-and (f-not 0) 1) (list f f)) = f
; while
;     (val '(f-and (f-not 0) 1) (list f t)) = t.

; The conjecture "When x is well-defined on some set of vectors s, then
; x is constant on s" is invalidated by the expression 0 on the set s =
; (list (list t) (list f)).
; One is tempted to strengthen the hypothesis above by additionally
; requiring that there exist a vector in s that makes each variable
; of x unknown.  That conjecture is invalidated by x =
; (f-and (f-not 0) 1), again, using the test set:
; (list (list f f) (list (x) f) (list t (x)) (list f t)).
; The first and last test vectors produce different well-defined values
; of x.  Observe that the only difference between this test set
; and the set of edges of size 2 is the last vector.
; Note added in proof: On Thursday, May 23, I listened to Matt
; Kaufmann talk about his "reset results" with Bishop and Warren.  His
; results established many monotonicity properties of dual-eval and
; got me once again considering the question "what is X?"  I had been
; trying to think of X as nondeterministically 1 or 0.  I talked with
; Bishop about what X was that afternoon.  Upon leaving Bishop's
; office at 6pm I had resolved to prove that you couldn't build a
; fuzzy edge detector with F-NOT and F-AND.  The suspicion that you
; couldn't do it had come to me while at Oberwulfach (I spent hours
; trying) but I decided to lay the problem aside afterwards and focus
; on the formalization of asynchronous communication.
; It took me a night and a day (Thursday evening and then Friday, May
; 24) to get the result its raw form (in which I used numbers to
; encode views through the window).  Then I set about cleaning it up
; by going to the vectors used here.  Lisa's birthday, the Memorial
; Day weekend, an air conditioning failure at CLI, and Matt Wilding's
; birthday party all prevented useful work on the weekend.  (But I
; thought a lot about the problem -- it was surprisingly hard to
; define (edge k i) in a way that let me easily prove the var-val
; theorem about it.)  On Tuesday, I worked another three hours before
; finally getting the file in the form shown.
; At that point I sent a message about it to Warren, Bishop and Matt.
; In my message I asked Matt whether these results were derivable from
; his monotonicity results.  His reply is below.
; From kaufmann@CLI.COM Tue May 28 14:44:01 1991
; Received: by CLI.COM (4.1/1); Tue, 28 May 91 14:43:59 CDT
; Date: Tue, 28 May 91 14:44:33 CDT

; From: Matt Kaufmann <kaufmann@CLI.COM>
; To: moore@CLI.COM
; Cc: Brock@CLI.COM, Hunt@CLI.COM
; Subject: Fuzzy Edge Detection
; Nice going.  Yes, I think that the kind of monotonicity results that I
; proved could be used to get your result (though I don't know if that
; would be any easier than whatever proof you gave).  (Maybe "kind of"
; could even be omitted above.)  The informal argument is as follows.
; Consider for example the following two successive rows.
; (r1)  t x f f f f
; (r2)  t t x f f f
; Notice that these both `approximate' the following row:
; (r3)  t t f f f f
; Now since circuits are monotone, and since (r1) approximates (r3), we
; have that f(r1) approximates f(r3), where f is the candidate fuzzy
; edge detector.  But since f(r1) is well-defined (i.e. T or F), then
; since T and F can only approximate themselves (respectively), we have
; that f(r1) = f(r3).  A similar argument shows f(r2) = f(r3).
; Therefore f(r1) = f(r2).  Arguing in this way we can show that for all
; successive rows r and r', f(r) = f(r'); hence by an easy induction,
; f(r) = f(r') for all rows r, r'.

Index

add1-plus-12-difference-4-dw, 38 all-edges, 77, 78 app, 4, 5, 11, 14, 15, 19, 27, 29–33,

36, 37, 40, 42, 43, 51, 52, 55, 56, 58, 60–63, 65–67, 75

app-assoc, 5 app-cancellation, 5 app-listn-0, 43 app-listn-flg-listn-flg, 51 async, 11, 32, 67

b-not, 9, 11, 30, 36, 42, 48, 51, 52,

59, 60, 66 b-xor, 9, 11–13, 30, 36–38, 40, 41,

51, 55, 56, 58–60, 62–66 b-xor-b-not, 9 b-xor-commutes, 37 b-xor-x-x, 13 boolp, 9, 12, 51, 56, 58–62, 64–66,

73–75 boolp-b-not, 66 boolp-csig, 66 boolp-implies-det-listn, 56 boolp-t, 9 bvp, 12, 32, 58–61, 66, 67

car-app, 30 car-cells, 30 car-det-listn, 59 car-listn, 38 car-scan-oracle, 59 cdr-app, 31 cdr-app-cell-cells, 36 cdr-app-cell-rest, 63 cdr-listn, 42 cdrn, 12, 27, 29, 32, 37, 38, 51, 56,

58, 65, 66, 76 cdrn-app, 56 cdrn-dw-app-smooth-cell, 37 cdrn-dw-smooth-cell, 38 cdrn-listn, 51 cdrn-too-big, 76 cell, 11, 36–38, 41, 48, 49, 51, 58,

60, 62, 63 cells, 11, 30–32, 36, 37, 42, 43, 65,

66 csig, 11, 37, 41, 48, 58, 61–63, 66

det, 11, 31–33, 55, 56, 58–62, 65–67 det-app, 31 det-listn, 31 det-listn-hint, 55 difference-difference, 6 difference-difference-other, 6 difference-elim, 6 difference-is-0, 4 difference-plus, 5 difference-plus-cancellation-4, 5 difference-plus-cancellation1, 4 difference-plus-cancellation2, 4 difference-plus-cancellation3, 4 dw, 28, 29 dwg, 20, 21, 27, 28, 32, 34, 48, 52,

57 dwg-bounds, 34

edge, 75–78 edge-at-non-numberp, 78 edge-beyond-max, 78 endp, 10, 14–16 endp-app, 15 equal-difference-0, 60 equal-len-0, 4 equal-times-0, 7 everything-defined-at-0, 78 exprp, 74, 77, 78

f-and, 73, 75 f-not, 73, 75

helper1, 22 helper10, 25 helper11, 25 helper14, 26 helper15, 26 helper5, 23 helper7, 23 helper8, 24 helper9, 24

intro-delta, 8

lastn, 17, 18, 40 lastn-app, 40 lastn-listn, 18 lastn-nil, 18 len, 4, 5, 15–19, 23, 26, 28, 29, 31,

38, 40, 43, 55, 56, 62, 64– 67, 76

len-app, 5 len-cell, 38 len-det, 55 len-endp, 16 len-lastn, 17 len-listn, 17 len-lst*, 16 len-lst+, 15 len-smooth, 31 len-tr*, 17 len-ts*, 17 len-ts+, 16 len-warp, 56 length-edge, 76 lessp-2-len-cdr-cells, 43 lessp-2-len-implies-listps, 28 lessp-n-1, 76 lessp-nlst*, 18 lessp-nlst+, 16 lessp-ntr*-nts*, 21 lessp-nts+, 18 lessp-plus-nts*-times-w-nlst*-p

lus-r-ntr*-lemma, 22 lessp-quotient-to-lessp-times, 7 lessp-quotient-to-lessp-times-le

mma1, 7 mma2, 7 lessp-remainder, 4 lessp-times, 9 lessp-times-18, 26 lessp-trg*-plus-w-tsg*, 35 lessp-ts+, 14 listn, 11, 17–19, 26, 27, 29–33, 36–

38, 40–43, 49, 51, 52, 55, 56, 58–62, 65, 66

listn-add1, 26 listp-app-listn, 30 listp-cells, 30 listp-det, 59 listp-listn, 30 listp-smooth-cell, 37 loop, 66 loop-ind-hint, 48, 49 loop-killer-0, 65 loop-killer-0a, 64 loop-killer-2, 61 loop-killer-2a, 60 loop-killer-2a-lemma, 59 loop-killer-2b, 58 loop-killer-2c, 61 lst*, 14–18, 40, 41 lst*-is-lastn, 18 lst*-is-lastn-nlst*, 40 lst*-listn, 18 lst*-smooth-cell, 40 lst+, 10, 11, 14, 15, 17–19, 23 lst+-app, 14 lst+-app-gap, 19 lst+-listn, 18 lst+-weakly-shortens-lst, 10

max-var, 74, 77 multiply-both-sides-of-lessp, 7

n*, 18, 19, 29, 32, 51, 52, 54–58, 61 n*-alg, 53 n*-alg-hack1, 53 n*-alg-lemma, 53 n*-lower-bound, 55 n*-plus, 57 n*-plus-lemma, 56 n*-upper-bound, 54 nendp, 16–22, 27, 52, 53, 68–70 nendp-alg, 52 nendp-is-usually-f, 21 nendp-nlst*, 20 nlst*, 16, 18, 20, 22, 28, 32, 35, 40,

41, 48, 49, 51, 52, 57, 70 nlst*-alg, 70 nlst*-alg-lemma2, 70 nlst*-alg-lemma2-hack1, 7 nlst+, 15–18, 52, 53, 68–70 nlst+-alg, 52 nlst+-equal-n, 16 nlst+-ts-plus-ts-w, 52 no, 55, 56, 58, 59, 61 no-is-len-scan-det-listn, 55 non-x-on-nil-implies-constant, 78 not-b-xor-b-not, 36 not-lessp-2-nlst*, 40 not-lessp-no, 56 not-lessp-ntr*-nts*, 21 not-lessp-nts+, 18 not-lessp-nts+-ts, 52 not-lessp-plus-r-ntr*-plus-nts*

-times-w-nlst*, 22 not-lessp-times-quotient, 5 not-lessp-times-quotient-other, 6 not-lessp-trg*-tsg*, 34 not-lessp-ts+, 14 nq, 28, 29 nqg, 20, 21, 27, 28, 32–34, 48, 49,

52, 57 nqg-bounds, 34 nsig*-alg-lemma-hack1, 5 nsig*-lower-bound-lemma1, 9 nsig*-upper-bound-hack1, 7 nsig*-upper-bound-hack2, 8 nsig*-upper-bound-hack3, 8 nsig*-upper-bound-lemma1, 7 nsig*-upper-bound-lemma2, 9 nsig*-upper-bound-lemma2-1, 8 nsig*-upper-bound-lemma2-2, 8 nsig*-upper-bound-lemma2-equalit

y, 9 nth, 12, 74 nth-edge, 76 ntr*, 17, 20–22, 28, 32, 35, 48, 49, 51, 52, 57, 69

ntr*-alg, 69

ntr*-alg-lemma2, 69 ntr*-alg-lemma2-hack1, 6 nts*, 16, 17, 20–22, 28, 32, 35, 48, 49, 51, 52, 57, 69

nts*-alg, 68

nts*-alg-lemma1, 67 nts*-alg-lemma2, 68 nts*-alg-lemma2-hack1, 5 nts+, 16–19, 23, 52, 53, 68–70 nts+-alg, 53 nts+-app-gap, 19 numberp-max-var, 77

oracle*, 31, 33, 48, 49

oracle*-listn, 31

plus-add1, 3 plus-associates, 3 plus-cancellation, 9 plus-commutes1, 3 plus-commutes2, 3 properp, 18 properp-listn, 18

quotient-difference, 6 quotient-monotonic, 6 quotient-monotonic-lemma, 6 quotient-plus-times, 4 quotient-plus-times1, 7 quotient-plus-times2, 6 quotient-plus-times3, 8 quotient-times, 7 quotient-x-x, 5

rate-proximity, 3, 8, 9, 32, 51, 54, 55, 58–62, 64–67

reconcile-signals, 10

recv, 12, 33, 61, 62, 65–67

recv-app-listn, 61 recv-bit, 12, 61 remainder-quotient-elim, 4

scan, 11, 12, 33, 55, 56, 58, 60, 61 scan-app-det-listn, 56 scan-app-listn, 33 scan-flg-app-listn-not-flg, 55 scan-oracle, 55, 56, 59 send, 11, 32, 67 sig, 10, 15, 19 sig-app, 15 sig-listn, 19 smooth, 9, 11, 30–32, 36–38, 40–42,

48, 49, 51, 58, 60, 62, 63, 65, 66

smooth-app-cell-app-cells, 37 smooth-app-cell-rest, 63 smooth-app-cells, 42 smooth-congruence, 30 smooth-flg-app-listn-flg, 30 smooth-flg-app-listn-not-flg, 36 smooth-flg-listn-flg, 36 smooth-flg-listn-not-flg, 40

tailp, 17 tailp-implies-lastn-len, 17 tailp-lst*, 17 tailp-lst+, 17 tailp-transitive, 17 target, 15, 29, 65 times-0, 3 times-add1, 3 times-associates, 4 times-cancellation1, 5 times-cancellation2, 6 times-commutes1, 4 times-commutes2, 4 times-distributes1, 3 times-distributes2, 4 times-monotonic, 5 times-non-numberp, 3 top, 67 top-async-send, 32 top-async-send-lemma1, 31 top-recv-step, 33 top-smooth-step, 30 tr, 28, 29 tr*, 14, 15, 17 trg, 21, 27, 28, 32, 35, 49, 52, 57 ts, 28, 29 ts*, 14, 15, 17 ts+, 10, 11, 14–16 ts+-app, 15 ts+-increases-tr, 10 tsg, 21, 27, 28, 32, 35, 49, 52, 57

val, 74, 75, 77, 78 val-is-x-or-boolp, 75 val-is-x-or-boolp-2, 78 val-on-successive-edges-is-const ant-when-defined, 77

var-val, 74–76 var-val-edge, 76 var-val-is-x-or-boolp, 75

warp, 10, 11, 15, 19, 20, 23–27, 29, 32, 48, 49, 51, 56, 58, 60, 62, 65–67

warp-app, 15

warp-app-across-gap, 27

warp-app-gap, 19 warp-app-listn-q, 29 warp-app-listn-q1, 28 warp-listn, 19 warp-smooth-cell, 51 well-defined, 77, 78 well-defined-implies-constant, 78 well-defined1, 77, 78 well-defined1-implies-constant, 78 well-defined1-is-a-universal-qu

antifier, 78 width, 74, 77, 78

x, 73–78