#|
 Copyright (C) 1993 by Matt Wilding.
 This script is hereby placed in the public domain, and therefore unlimited
 editing and redistribution is permitted.
 NO WARRANTY
 Matt Wilding 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 Matt Wilding 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.
|#

Event: Start with the library "piton" using the compiled version.

;; NIM Piton proof
;; Matt Wilding 4-15-92
;; modified 7-92 to work on Piton library
;; This script takes 10 hours to run on a 64 meg Sparc2
;; This work is described in Technical Report #78.  A presentation
;; about this work was made at the CLI research review in April 92.
#|
Nim is a game played with piles of matches.  Two opponents alternate
taking at least one match from exactly one pile until there are no
matches left.  The player who takes the last match loses.
Piton is an assembly-level language with a formal semantics and a
verified compiler.  Piton is described in CLI tech report #22.  One of
the machines to which Piton is targeted is FM9001, a microprocessor
that has a formal semantics and that has been fabricated.

This proof script leads NQTHM to a proof that a Piton program that
"plays" Nim does so optimally.  Informally, this means
a) A Piton program (see function CM-PROG) when run on the Piton
interpreter and given as input a reasonable Nim state yields a new
Nim state equal to what is calculated by function COMPUTER-MOVE.
(See event COMPUTER-MOVE-IMPLEMENTED.)
b) COMPUTER-MOVE generates valid moves.  That is, it removes at
least one match from exactly one pile.  (VALID-MOVEP-COMPUTER-MOVE)
c) Depth-first search of the state space of all possible moves is
used to define what is meant by optimal Nim play.  Exhaustive search
is used to find if there is a strategy for a Nim player to ensures
eventual victory from the current Nim state.  An optimal strategy
transforms any state for which there exists such a winning strategy
into a state from which exhaustive search can find no winning
strategy.
   Exhaustive search of all possible moves from a NIM state is
formalized in the function WSP.  The optimalilty of the strategy
COMPUTER-MOVE is proved in the event COMPUTER-MOVE-WORKS.
d) The FM9001 Piton compiler correctness theorem assumes that the
Piton state that is to be run contains valid Piton code, fit into
an FM9001's memory, and use constants of word size 32.  A Piton
state (used in the Indiana test described below) was constructed
that contains the Nim program, and is proved to meet the compiler
correctness constraints (CM-PROG-FM9001-LOADABLE)
The algorithm used by the program is non-obvious and very efficient,
avoiding the need to search.  (I invented the programming trick only
to subsequently discover that it has been known since the beginning
of the century.)  See tech report #78 for a description.
(Constant bounds on the number of Piton instructions executed while
running this program have been proved using PC-NQTHM.  These events
are not included in this NQTHM-processable script, but the theorem is
included in comments later in this file for completeness.)
This script was developed using only those events from the Piton
library necessary to define the interpreter and the naturals library.
In July 92 it was modified somewhat to "fit" onto the Piton library
that sits on top of the FM9001 library.  The immediate motivation was

to make it easier to include in the upcoming NQTHM-1992 proveall
release being put together by Boyer.  The Piton library contains the
events of the FM9001 library.  The FM9001 library contains an older
version of the naturals library (though not explicitly with a
note-lib).  Thus, this script requires only the Piton library.
In May 92, in consultation with researchers at Indiana University, I
compiled the Nim Piton program for the FM9001 and sent the image to
Indiana.  They ran the image and generated an optimal NIM move on a
fabricated FM9001 they had wired up.  The intial image and part of the
resulting image is included in a comment at the end of this script.  A
non-trivial program compiled using a reasonably-complex compiler for a
small microprocessor worked without any conventional testing done on
any of the components, and everyone was pleased but not surprised.
|#

Event: Set the status of the events in the theory addition. The status of each event is to be set as follows. Anything not otherwise mentioned is to be enabled. Name this event ‘addition-on’.

Event: Set the status of the events in the theory multiplication. The status of each event is to be set as follows. Anything not otherwise mentioned is to be enabled. Name this event ‘multiplication-on’.

Event: Set the status of the events in the theory remainders. The status of each event is to be set as follows. Anything not otherwise mentioned is to be enabled. Name this event ‘remainders-on’.

Event: Set the status of the events in the theory quotients. The status of each event is to be set as follows. Anything not otherwise mentioned is to be enabled. Name this event ‘quotients-on’.

Event: Set the status of the events in the theory exponentiation. The status of each event is to be set as follows. Anything not otherwise mentioned is to be enabled. Name this event ‘exponentiation-on’.

Event: Set the status of the events in the theory logs. The status of each event is to be set as follows. Anything not otherwise mentioned is to be enabled.

Name this event ‘logs-on’.

Event: Set the status of the events in the theory gcds. The status of each event is to be set as follows. Anything not otherwise mentioned is to be enabled. Name this event ‘gcds-on’.

Definition: clock-plus (x, y) = (x + y)

Theorem: p-add1 p (p0 , 1 + n) = p (p-step (p0 ), n)

Theorem: p-0 (n ≃ 0) → (p (p0 , n) = p0 )

Theorem: clock-plus-function p (p0 , clock-plus (x, y)) = p (p (p0 , x), y)

Event: Disable p-add1.

Theorem: clock-plus-add1 p (p0 , clock-plus (1 + x, y)) = p (p0 , 1 + clock-plus (x, y))

Event: Disable clock-plus.

Theorem: clock-plus-0 (x ≃ 0) → (clock-plus (x, y) = fix (y))

Theorem: fix-clock-plus fix (clock-plus (x, y)) = clock-plus (x, y)

Theorem: p-step1-opener p-step1 (cons (opcode, operands), p) = if p-ins-okp (cons (opcode, operands), p)

then p-ins-step (cons (opcode, operands), p) else p-halt (p, x-y-error-msg ('p, opcode)) endif

Event: Disable p-step1.

Theorem: p-opener (p (s, 0) = s) ∧ (p (p-state (pc, ctrl, temp, prog, data, max-ctrl, max-temp, word-size, psw),

1 + n) = p (p-step (p-state (pc, ctrl, temp, prog, data, max-ctrl, max-temp, word-size, psw)),

n))

Event: Disable p.

Definition: at-least-morep (base, delta, value) = (value ≮ (base + delta))

Theorem: at-least-morep-normalize (at-least-morep (1 + base, delta, value) = at-least-morep (base, 1 + delta, value)) ∧ (at-least-morep (base, 1 + delta, 1 + value)

= at-least-morep (base, delta, value))

Theorem: at-least-morep-linear (at-least-morep (base, d1 , value) ∧ (d1 ≮ d2 )) → at-least-morep (base, d2 , value)

Theorem: lessp-as-at-least-morep at-least-morep (base, delta, value) → (((value < x) = (¬ at-least-morep (x, 0, value)))

∧ ((x < value) = at-least-morep (x, 1, value)))

Event: Disable at-least-morep.

Definition: nat-to-bv (nat, size) = if size ≃ 0 then nil

elseif nat < exp (2, size − 1) then cons (0, nat-to-bv (nat, size − 1)) else cons (1, nat-to-bv (nat − exp (2, size − 1), size − 1)) endif

Definition: nat-to-bv-state (state, size) = if listp (state)

then cons (nat-to-bv (car (state), size), nat-to-bv-state (cdr (state), size)) else nil endif

;; a more elegant way to write this program would be to use the
;; bit-vector of all 0's initially, then xor all the elements of
;; the array.  But we don't want a pointer to memory to
;; ever have an improper value, so we write things this way

Definition: xor-bvs-program

= '(xor-bvs
(vecs-addr numvecs)
nil
(push-local vecs-addr)
(fetch)
(push-local numvecs)
(sub1-nat)
(pop-local numvecs)
(dl loop nil (push-local numvecs))
(test-nat-and-jump zero done)
(push-local numvecs)
(sub1-nat)
(pop-local numvecs)
(push-local vecs-addr)
(push-constant (nat 1))
(add-addr)
(set-local vecs-addr)
(fetch)
(xor-bitv)
(jump loop)
(dl done nil (ret)))

Definition: bit-vectors-piton (array, size) = if listp (array)

then listp (car (array)) ∧ (caar (array) = 'bitv) ∧ bit-vectorp (cadar (array), size) ∧ (cddar (array) = nil) ∧ bit-vectors-piton (cdr (array), size)

else array = nil endif

Definition: array (name, segment) = cdr (assoc (name, segment))

;; vecs is name of state

Definition: xor-bvs-input-conditionp (p0 ) = ((car (top (p-temp-stk (p0 ))) = 'nat)

∧ (car (top (cdr (p-temp-stk (p0 )))) = 'addr) ∧ (cdadr (top (cdr (p-temp-stk (p0 )))) = 0) ∧ listp (cadr (top (cdr (p-temp-stk (p0 ))))) ∧ (cddr (top (p-temp-stk (p0 ))) = nil) ∧ (cddr (top (cdr (p-temp-stk (p0 )))) = nil) ∧ definedp (caadr (top (cdr (p-temp-stk (p0 )))), p-data-segment (p0 )) ∧ bit-vectors-piton (array (caadr (top (cdr (p-temp-stk (p0 )))),

p-data-segment (p0 )), p-word-size (p0 ))

∧ (cadr (top (p-temp-stk (p0 )))

= length (array (caadr (top (cdr (p-temp-stk (p0 )))),

p-data-segment (p0 ))))

∧ at-least-morep (p-ctrl-stk-size (p-ctrl-stk (p0 )),

                4,

p-max-ctrl-stk-size (p0 ))

∧ at-least-morep (length (p-temp-stk (p0 )),

                2,

p-max-temp-stk-size (p0 ))

∧ (untag (top (p-temp-stk (p0 ))) ≄ 0) ∧ (untag (top (p-temp-stk (p0 ))) < exp (2, p-word-size (p0 ))) ∧ listp (p-ctrl-stk (p0 )))

; time to run loop

Definition: xor-bvs-clock-loop (numvecs) = if numvecs ≃ 0 then 3

else 12 + xor-bvs-clock-loop (numvecs − 1) endif

; time to run xor-bvs, including call and ret

Definition: xor-bvs-clock (numvecs) = (6 + xor-bvs-clock-loop (numvecs − 1))

Definition: xor-bvs-array (current, array, n, array-size) = if n ≃ 0 then current

else xor-bvs-array (xor-bitv (current,

untag (get (array-size − n, array))),

array, n − 1, array-size) endif Theorem: lessp-1-exp (1 < exp (a, b)) = ((1 < a) ∧ (b ≄ 0))

Theorem: bit-vectors-piton-means (bit-vectors-piton (state, size) ∧ (p < length (state))) → ((car (get (p, state)) = 'bitv)

∧ listp (get (p, state))

∧ bit-vectorp (cadr (get (p, state)), size)

∧ (cddr (get (p, state)) = nil))

Definition: xor-bvs-loop-correctness-general-induct (i, current, n, s, data-segment) = if i ≃ 0 then t

else xor-bvs-loop-correctness-general-induct (i − 1,

xor-bitv (current,

cadr (get (n − i,

array (s,

data-segment)))),

n, s, data-segment) endif

;; in Piton library
;(prove-lemma bit-vectorp-xor-bitv (rewrite)
;      (implies
;       (and
;        (bit-vectorp x size)
;        (bit-vectorp y size))
;       (bit-vectorp (xor-bitv x y) size)))

Event: Enable bit-vectorp-xor-bitv.

Theorem: xor-bvs-loop-correctness-general ((length (array (s, data-segment)) < exp (2, word-size)) ∧ (word-size ≄ 0) ∧ listp (ctrl-stk) ∧ bit-vectors-piton (array (s, data-segment), word-size) ∧ at-least-morep (length (temp-stk), 3, max-temp-stk-size) ∧ (definition ('xor-bvs, prog-segment) = xor-bvs-program) ∧ definedp (s, data-segment) ∧ (i ∈ N) ∧ (i < n) ∧ bit-vectorp (current, word-size)

∧ (n = length (array (s, data-segment))))

→ (p (p-state ('(pc (xor-bvs . 5)),

cons (list (list (cons ('vecs-addr,

list ('addr, cons (s, (n − i) − 1))), cons ('numvecs, list ('nat, i))),

ret-pc), ctrl-stk),

cons (list ('bitv, current), temp-stk), prog-segment, data-segment, max-ctrl-stk-size, max-temp-stk-size, word-size,

             'run),

xor-bvs-clock-loop (i)) = p-state (ret-pc,

ctrl-stk,

cons (list ('bitv,

xor-bvs-array (current, array (s, data-segment), i, n)),

temp-stk), prog-segment, data-segment, max-ctrl-stk-size, max-temp-stk-size, word-size,

              'run))

Theorem: difference-x-sub1-x-better (x − (x − 1)) = if 0 < x then 1

else 0 endif

Theorem: xor-bvs-loop-correctness ((length (array (s, data-segment)) < exp (2, word-size)) ∧ (word-size ≄ 0) ∧ listp (ctrl-stk) ∧ bit-vectors-piton (array (s, data-segment), word-size) ∧ at-least-morep (length (temp-stk), 3, max-temp-stk-size) ∧ (definition ('xor-bvs, prog-segment) = xor-bvs-program) ∧ definedp (s, data-segment) ∧ (0 < n)

∧ bit-vectorp (current, word-size) ∧ (n = length (array (s, data-segment))))

→ (p (p-state ('(pc (xor-bvs . 5)),

cons (list (list (cons ('vecs-addr, list ('addr, cons (s, 0))),

cons ('numvecs, list ('nat, n − 1))), ret-pc),

ctrl-stk), cons (list ('bitv, current), temp-stk), prog-segment, data-segment, max-ctrl-stk-size, max-temp-stk-size, word-size,

'run),

xor-bvs-clock-loop (n − 1)) = p-state (ret-pc,

ctrl-stk, cons (list ('bitv,

xor-bvs-array (current, array (s, data-segment), n − 1, n)),

temp-stk), prog-segment, data-segment, max-ctrl-stk-size, max-temp-stk-size, word-size,

 'run))

Theorem: exp-0 (x ≃ 0) → ((exp (x, y)

= if y ≃ 0 then 1

else 0 endif) ∧ (exp (y, x) = 1))

Theorem: bit-vectors-piton-means-more (listp (x) ∧ bit-vectors-piton (x, size)) → (list ('bitv, cadar (x)) = car (x))

;; xor-bvs of an array of at least one bit vector

Definition: xor-bvs (array)

= if listp (array) then xor-bitv (car (array), xor-bvs (cdr (array))) else nil endif

Definition: untag-array (array) = if listp (array) then cons (untag (car (array)), untag-array (cdr (array)))

else nil endif

Theorem: bit-vectorp-get bit-vectors-piton (array, size) → (bit-vectorp (untag (get (n, array)), size) = (n < length (array)))

;(prove-lemma difference-sub1-arg2 (rewrite)
;      (equal
;       (difference a (sub1 n))
;       (if (zerop n) (fix a)
; (if (lessp a n) 0 (add1 (difference a n))))))

Event: Enable difference-sub1-arg2.

Theorem: xor-bitv-commutative (length (a) = length (b)) → (xor-bitv (a, b) = xor-bitv (b, a))

Theorem: xor-bitv-commutative2 (length (a) = length (b)) → (xor-bitv (a, xor-bitv (b, c)) = xor-bitv (b, xor-bitv (a, c)))

Theorem: xor-bitv-associative (length (a) = length (b)) → (xor-bitv (xor-bitv (a, b), c) = xor-bitv (a, xor-bitv (b, c)))

Theorem: length-from-bit-vectorp bit-vectorp (x, s) → (length (x) = fix (s))

Theorem: length-xor-bitv length (xor-bitv (a, b)) = length (a)

Theorem: length-cadr-get-bit-vectors-piton (bit-vectors-piton (x, l) ∧ (i < length (x))) → (length (cadr (get (i, x))) = fix (l))

Theorem: equal-xor-bitv-x-x (bit-vectorp (b, length (a)) ∧ bit-vectorp (c, length (a))) → ((xor-bitv (a, b) = xor-bitv (a, c)) = (b = c))

Definition: bit-vectorp-induct (size, a, b) = if size ≃ 0 then t

else bit-vectorp-induct (size − 1, cdr (a), cdr (b)) endif

Theorem: bit-vectorp-xor-bitv2 bit-vectorp (xor-bitv (a, b), size) = (length (a) = fix (size))

Definition: bit-vectorsp (bvs, size) = if listp (bvs)

then bit-vectorp (car (bvs), size) ∧ bit-vectorsp (cdr (bvs), size)

else bvs = nil endif

Theorem: length-xor-bvs bit-vectorsp (bvs, length (car (bvs))) → (length (xor-bvs (bvs)) = length (car (bvs)))

Theorem: bit-vectorsp-untag bit-vectors-piton (x, s) → bit-vectorsp (untag-array (x), s)

Theorem: bit-vectorsp-cdr-untag bit-vectors-piton (cdr (x), s) → bit-vectorsp (cdr (untag-array (x)), s)

;; actually part of npiton-defs, but not supporter of p
;;
;(DEFN NTHCDR
;      (N L)
;      (IF (ZEROP N)
;          L
;          (NTHCDR (SUB1 N) (CDR L))))

Event: Enable nthcdr.

Theorem: bit-vectorsp-nthcdr (bit-vectorsp (x, s) ∧ (n < length (x))) → bit-vectorsp (nthcdr (n, x), s)

Theorem: bit-vectorp-xor-bvs (bit-vectorsp (x, size) ∧ listp (x)) → bit-vectorp (xor-bvs (x), size)

Theorem: length-untag-array length (untag-array (x)) = length (x)

;(prove-lemma listp-nthcdr (rewrite)
;      (equal
;       (listp (nthcdr n x))
;       (lessp n (length x)))
;      ((enable nthcdr)))

Event: Enable listp-nthcdr.

Theorem: nthcdr-open (n < length (x)) → (nthcdr (n, x) = cons (get (n, x), nthcdr (1 + n, x)))

Theorem: get-untag-array (n < length (x)) → (get (n, untag-array (x)) = cadr (get (n, x)))

Theorem: equal-xor-bitv-x-x-special (bit-vectorp (b, length (a)) ∧ bit-vectorp (xor-bitv (z, c), length (a))) → ((xor-bitv (a, b) = xor-bitv (z, xor-bitv (a, c)))

= (b = xor-bitv (z, c)))

Definition: fix-bit (b) = if b = 0 then 0

else 1 endif

Theorem: xor-bitv-0 (xor-bit (x, 0) = fix-bit (x)) ∧ (xor-bit (0, x) = fix-bit (x))

Theorem: xor-bitv-nlistp (¬ listp (c)) → (xor-bitv (a, xor-bitv (b, c)) = xor-bitv (a, b))

Theorem: xor-bitv-nlistp2 (bit-vectorp (a, b) ∧ (¬ listp (c))) → (xor-bitv (a, c) = a)

Theorem: xor-bvs-array-rewrite (bit-vectors-piton (array, length (current)) ∧ bit-vectorp (current, length (current)) ∧ (n < length (array)) ∧ (length (array) = as)) → (xor-bvs-array (current, array, n, as)

= xor-bitv (current, xor-bvs (nthcdr (as − n, untag-array (array)))))

;; in npiton-defs but not a supporter of p
;(PROVE-LEMMA EQUAL-LENGTH-0
;             (REWRITE)
;             (EQUAL (EQUAL (LENGTH X) '0)
;                    (NLISTP X)))

Event: Enable equal-length-0.

Theorem: correctness-of-xor-bvs-helper ((p0 = p-state (pc, ctrl-stk, append (list (tag ('nat, numvecs), tag ('addr, cons (state, 0))),

temp-stk), prog-segment, data-segment, max-ctrl-stk-size, max-temp-stk-size, word-size,

'run))

∧ (p-current-instruction (p0 ) = '(call xor-bvs)) ∧ (definition ('xor-bvs, prog-segment) = xor-bvs-program) ∧ xor-bvs-input-conditionp (p0 )) → (p (p0 , xor-bvs-clock (numvecs))

= p-state (add1-addr (pc), ctrl-stk, cons (list ('bitv,

xor-bvs-array (untag (car (array (state,

data-segment))),

array (state, data-segment), numvecs − 1, numvecs)),

temp-stk), prog-segment, data-segment, max-ctrl-stk-size, max-temp-stk-size, word-size,

  'run))

Theorem: length-cadar-bvs (bit-vectors-piton (x, s) ∧ listp (x)) → (length (cadar (x)) = fix (s))

Theorem: bit-vectorp-from-bit-vectors-piton bit-vectors-piton (x, s) → ((bit-vectorp (cadar (x), s) = listp (x))

∧ (bit-vectorp (cadr (get (n, x)), s) = (n < length (x))))

Theorem: nthcdr-1 nthcdr (1, a) = cdr (a)

Theorem: listp-untag-array listp (untag-array (x)) = listp (x)

Theorem: xor-bvs-input-conditionp-means-xor-bvs-hack (xor-bvs-input-conditionp (p-state (pc, ctrl-stk, cons (list ('nat, numvecs),

cons (list ('addr, cons (state, 0)),

temp-stk)),

prog-segment, data-segment, max-ctrl-stk-size, max-temp-stk-size, word-size,

'run))

∧ (0 < word-size)) → (xor-bvs-array (untag (car (array (state, data-segment))),

array (state, data-segment), numvecs − 1, numvecs)

= xor-bvs (untag-array (array (state, data-segment))))

Theorem: correctness-of-xor-bvs ((p0 = p-state (pc,

ctrl-stk, cons (n, cons (s, temp-stk)), prog-segment, data-segment, max-ctrl-stk-size, max-temp-stk-size, word-size,

'run))

∧ (0 < word-size) ∧ (p-current-instruction (p0 ) = '(call xor-bvs)) ∧ (definition ('xor-bvs, prog-segment) = xor-bvs-program) ∧ xor-bvs-input-conditionp (p0 )) → (p (p-state (pc,

ctrl-stk, cons (n, cons (s, temp-stk)), prog-segment, data-segment, max-ctrl-stk-size, max-temp-stk-size, word-size,

'run),

xor-bvs-clock (cadr (n))) = p-state (add1-addr (pc),

ctrl-stk, cons (list ('bitv, xor-bvs (untag-array (array (caadr (s),

data-segment)))),

temp-stk), prog-segment, data-segment, max-ctrl-stk-size, max-temp-stk-size, word-size,

                'run))

Definition: example-xor-bvs-p-state

= p-state ('(pc (main . 0)),
          '((nil (pc (main . 0)))),

nil,

          list ('(main nil nil
                (push-constant (addr (arr . 0)))
                (push-constant (nat 3))
                (call xor-bvs)
                (ret)),

xor-bvs-program),

          '((arr
             (bitv (0 1 0 1 1 0 0 1))
             (bitv (0 0 0 0 0 0 0 1))
             (bitv (0 1 1 0 1 0 0 1)))),
          10,
          8,
          8,
          'run)
;;;; push-1-vector
;; Piton currently does not provide any mechanism for creating a
;; bit vector except as an operation on other bit vectors.  Until
;; this apparent flaw is fixed, we'll write our program as a
;; function of the word size.

Definition: one-bit-vector (wordsize) = if wordsize < 2 then list (1)

else cons (0, one-bit-vector (wordsize − 1)) endif

Definition: push-1-vector-program (wordsize)

= list ('push-1-vector,

nil, nil, list ('push-constant, list ('bitv, one-bit-vector (wordsize))), list ('ret))

Definition: example-push-1-vector-state

= p-state ('(pc (main . 0)),
          '((nil (pc (main . 0)))),

nil,

          list ('(main nil nil (call push-1-vector) (ret)),

push-1-vector-program (8)), nil,

          10,
          8,
          8,
          'run)

Definition: push-1-vector-input-conditionp (p0 ) = ((p-max-ctrl-stk-size (p0 )

≮ (2 + p-ctrl-stk-size (p-ctrl-stk (p0 ))))

∧ (p-max-temp-stk-size (p0 ) ≮ (1 + length (p-temp-stk (p0 )))) ∧ listp (p-ctrl-stk (p0 )))

;(prove-lemma length-append (rewrite)
;      (equal
;       (length (append a b))
;       (plus (length a) (length b))))

Event: Enable length-append.

Theorem: equal-assoc-cons (assoc (k, a) = cons (x, y)) → ((car (assoc (k, a)) = x) ∧ (cdr (assoc (k, a)) = y))

Theorem: correctness-of-push-1-vector ((p0 = p-state (pc,

ctrl-stk, temp-stk, prog-segment, data-segment, max-ctrl-stk-size, max-temp-stk-size, word-size,

        'run))

∧ (p-current-instruction (p0 ) = '(call push-1-vector)) ∧ (definition ('push-1-vector, prog-segment)

= push-1-vector-program (word-size)) ∧ push-1-vector-input-conditionp (p0 )) → (p (p0 , 3)

= p-state (add1-addr (pc), ctrl-stk, cons (list ('bitv, one-bit-vector (word-size)), temp-stk), prog-segment, data-segment, max-ctrl-stk-size, max-temp-stk-size, word-size,

          'run))
;;;; nat-to-bv

Definition: nat-to-bv-program

= '(nat-to-bv
(value)
((current-bit (nat 0)) (temp (nat 0)))
(call push-1-vector)
(pop-local current-bit)
(call push-1-vector)
(rsh-bitv)
(dl loop nil (push-local value))
(test-nat-and-jump zero done)
(push-local value)
(div2-nat)
(pop-local temp)
(pop-local value)
(push-local temp)
(test-nat-and-jump zero lab)
(push-local current-bit)
(xor-bitv)
(dl lab nil (push-local current-bit))
(lsh-bitv)
(pop-local current-bit)
(jump loop)
(dl done nil (ret)))

Definition: example-nat-to-bv-state

= p-state ('(pc (main . 0)),
          '((nil (pc (main . 0)))),

nil,

          list ('(main nil nil
                (push-constant (nat 86))
                (call nat-to-bv)
                (ret)),

push-1-vector-program (8), nat-to-bv-program),

nil,

          10,
          8,
          8,
          'run)

Definition: zero-bit-vector (size) = if size ≃ 0 then nil

else cons (0, zero-bit-vector (size − 1)) endif

Definition: nat-to-bv2-helper (value, current-bit, bit-vector) = if value ≃ 0 then bit-vector

else nat-to-bv2-helper (value ÷ 2, append (cdr (current-bit), list (0)), if (value mod 2) = 1 then xor-bitv (current-bit, bit-vector) else bit-vector endif) endif

Definition: nat-to-bv2 (value, size) = nat-to-bv2-helper (value, one-bit-vector (size), zero-bit-vector (size))

Definition: nat-to-bv-loop-clock (value) = if value ≃ 0 then 3

else if (value mod 2) = 0 then 12 else 14 endif + nat-to-bv-loop-clock (value ÷ 2) endif

Definition: correctness-of-nat-to-bv-general-induct (value, cb, temp, bv) = if value ≃ 0 then t else correctness-of-nat-to-bv-general-induct (value ÷ 2,

append (cdr (cb),

list (0)), list ('nat,

value mod 2), if (value mod 2)

                                          = 0

then bv

else xor-bitv (bv, cb) endif) endif

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

Theorem: lessp-exp-simple ((x < y) ∧ (z ≄ 0)) → (x < exp (y, z))

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

Theorem: lessp-remainder-x-exp-x ((x mod y) < exp (y, z)) = (((z ≃ 0) ∧ ((x mod y) = 0)) ∨ ((z ≄ 0) ∧ (y ≄ 0)))

Theorem: bit-vectorp-append bit-vectorp (x, x-size) → (bit-vectorp (append (x, y), size)

= (bit-vectorp (y, size − x-size) ∧ (size ≮ x-size)))

Theorem: correctness-of-nat-to-bv-general (listp (ctrl-stk) ∧ at-least-morep (length (temp-stk), 3, max-temp-stk-size) ∧ (definition ('nat-to-bv, prog-segment) = nat-to-bv-program) ∧ (value ∈ N) ∧ (0 < word-size) ∧ (value < exp (2, word-size)) ∧ bit-vectorp (bv, word-size) ∧ bit-vectorp (cb, word-size))

→ (p (p-state ('(pc (nat-to-bv . 4)),

cons (list (list (cons ('value, list ('nat, value)),

                          cons ('current-bit, list ('bitv, cb)),

cons ('temp, temp)), ret-pc),

ctrl-stk), cons (list ('bitv, bv), temp-stk), prog-segment, data-segment, max-ctrl-stk-size, max-temp-stk-size, word-size,

              'run),

nat-to-bv-loop-clock (value)) = p-state (ret-pc,

ctrl-stk,

cons (list ('bitv, nat-to-bv2-helper (value, cb, bv)),

temp-stk), prog-segment, data-segment, max-ctrl-stk-size, max-temp-stk-size, word-size,

                'run))

Definition: nat-to-bv-clock (value) = (9 + nat-to-bv-loop-clock (value))

Definition: nat-to-bv-input-conditionp (p0 ) = ((cadr (top (p-temp-stk (p0 ))) < exp (2, p-word-size (p0 )))

∧ (cadr (top (p-temp-stk (p0 ))) ∈ N)

∧ at-least-morep (p-ctrl-stk-size (p-ctrl-stk (p0 )),

                     7,

p-max-ctrl-stk-size (p0 ))

∧ (0 < p-word-size (p0 ))

∧ at-least-morep (length (p-temp-stk (p0 )),

                     2,

p-max-temp-stk-size (p0 ))

∧ listp (p-ctrl-stk (p0 )))

Theorem: bit-vectorp-one-bit-vector bit-vectorp (one-bit-vector (s), s) = (0 < s)

Theorem: bit-vectorp-zero-bit-vector bit-vectorp (zero-bit-vector (s), s)

Theorem: all-but-last-one-bit-vector all-but-last (one-bit-vector (s)) = zero-bit-vector (s − 1)

Theorem: correctness-of-nat-to-bv-helper ((p0 = p-state (pc, ctrl-stk, cons (list ('nat, value), temp-stk), prog-segment, data-segment, max-ctrl-stk-size, max-temp-stk-size, word-size,

'run))

∧ (p-current-instruction (p0 ) = '(call nat-to-bv)) ∧ (definition ('nat-to-bv, prog-segment) = nat-to-bv-program) ∧ (definition ('push-1-vector, prog-segment)

= push-1-vector-program (word-size)) ∧ nat-to-bv-input-conditionp (p0 )) → (p (p0 , nat-to-bv-clock (value))

= p-state (add1-addr (pc), ctrl-stk, cons (list ('bitv, nat-to-bv2 (value, word-size)),

temp-stk), prog-segment, data-segment, max-ctrl-stk-size, max-temp-stk-size, word-size,

  'run))

Definition: bv-to-nat (bv) = if listp (bv)

then (fix-bit (car (bv)) ∗ exp (2, length (cdr (bv))))

+ bv-to-nat (cdr (bv)) else 0 endif

Theorem: length-nat-to-bv length (nat-to-bv (nat, size)) = fix (size)

Theorem: bv-to-nat-nat-to-bv bv-to-nat (nat-to-bv (nat, size)) = if nat < exp (2, size) then fix (nat)

else exp (2, size) − 1 endif

Event: Enable exp.

Theorem: nat-to-bv-simple (x ≃ 0) → ((nat-to-bv (x, y) = zero-bit-vector (y)) ∧ (nat-to-bv (y, x) = nil))

Theorem: nat-to-bv-bv-to-nat bit-vectorp (bv, size) → (nat-to-bv (bv-to-nat (bv), size) = bv)

Theorem: bv-to-nat-append bv-to-nat (append (x, y)) = (bv-to-nat (y) + (exp (2, length (y)) ∗ bv-to-nat (x)))

Theorem: lessp-plus-hacks (((a + (b + (c + ((d ∗ e) + (d ∗ e))))) < (e + e)) = ((d ≃ 0) ∧ ((a + (b + c)) < (e + e)))) ∧ (((a + (b + (c + (e + ((d ∗ g) + h))))) < g)

= ((d ≃ 0) ∧ ((a + (b + (c + (e + h)))) < g)))

Theorem: bv-to-nat-xor-bitv (bit-vectorp (x, size) ∧ bit-vectorp (y, size) ∧ (and-bitv (x, y) = zero-bit-vector (size))) → (bv-to-nat (xor-bitv (x, y)) = (bv-to-nat (x) + bv-to-nat (y)))

Theorem: lessp-bv-to-nat-exp-2 bit-vectorp (x, size) → ((bv-to-nat (x) < exp (2, size)) = t)

Theorem: equal-nat-to-bv (bit-vectorp (bv, size) ∧ (y < exp (2, size))) → (((nat-to-bv (y, size) = bv) = (bv-to-nat (bv) = fix (y)))

∧ ((bv = nat-to-bv (y, size)) = (fix (y) = bv-to-nat (bv))))

Definition: least-bit-higher-than-high-bit (x, y) = if listp (x)

then (length (x) = length (y))

∧ if car (y) ≠ 0 then all-zero-bitvp (x)

else least-bit-higher-than-high-bit (cdr (x), cdr (y)) endif

else y ≃ nil endif

Theorem: least-bit-higher-means-and-0 (bit-vectorp (x, size) ∧ bit-vectorp (y, size) ∧ least-bit-higher-than-high-bit (x, y)) → ((and-bitv (x, y) = zero-bit-vector (size))

∧ (and-bitv (y, x) = zero-bit-vector (size)))

Theorem: all-zero-bitvp-zero-bit-vector all-zero-bitvp (zero-bit-vector (size))

Theorem: bv-to-nat-one-bit-vector bv-to-nat (one-bit-vector (size)) = 1

;; renamed from firstn to avoid conflict with similar but different
;; definition in piton library

Definition: make-list-from (n, list) = if n ≃ 0 then nil

else cons (car (list), make-list-from (n − 1, cdr (list))) endif

Theorem: length-make-list-from length (make-list-from (n, list)) = fix (n)

Theorem: make-list-from-1 make-list-from (1, x) = list (car (x))

Theorem: listp-make-list-from listp (make-list-from (n, x)) = (n ≄ 0)

Definition: double-cdr-induct (x, z) = if listp (x) then double-cdr-induct (cdr (x), cdr (z))

else t endif

Theorem: all-zero-bitvp-append all-zero-bitvp (append (x, y)) = (all-zero-bitvp (x) ∧ all-zero-bitvp (y))

Theorem: least-bit-higher-than-high-bit-append-0s (all-zero-bitvp (y) ∧ (length (z) = length (append (x, y)))) → (least-bit-higher-than-high-bit (append (x, y), z)

= least-bit-higher-than-high-bit (x, make-list-from (length (x), z)))

Theorem: equal-xor-bitv-x-y-1 (xor-bitv (a, b) = b) = (bit-vectorp (b, length (a)) ∧ all-zero-bitvp (a))

Theorem: equal-xor-bitv-x-y-2 (xor-bitv (a, b) = a) = (all-zero-bitvp (make-list-from (length (a), b))

∧ bit-vectorp (a, length (a)))

Theorem: least-bit-higher-than-high-bit-simple all-zero-bitvp (x) → (least-bit-higher-than-high-bit (x, y) = (length (x) = length (y)))

Theorem: make-list-from-is-all-but-last (length (x) = (1 + n)) → (make-list-from (n, x) = all-but-last (x))

Theorem: least-bit-higher-all-but-last least-bit-higher-than-high-bit (a, b) → (least-bit-higher-than-high-bit (a, cons (0, all-but-last (b)))

= listp (a))

Definition: at-most-one-bit-on (bv) = if listp (bv)

then if car (bv) = 0 then at-most-one-bit-on (cdr (bv))

else all-zero-bitvp (cdr (bv)) endif else t endif

;
;(prove-lemma length-all-but-last (rewrite)
;      (equal
;       (length (all-but-last x))
;       (if (listp x) (sub1 (length x)) 0)))

Event: Enable length-all-but-last.

Theorem: listp-xor-bitv listp (xor-bitv (a, b)) = listp (a)

Theorem: all-zero-bitvp-means-at-most-one-bit-on all-zero-bitvp (x) → at-most-one-bit-on (x)

Theorem: at-most-one-bit-on-append at-most-one-bit-on (append (a, b)) = ((all-zero-bitvp (a) ∧ at-most-one-bit-on (b))

∨ (at-most-one-bit-on (a) ∧ all-zero-bitvp (b)))

Definition: fix-bitv (list) = if listp (list)

then cons (if car (list) = 0 then 0 else 1 endif, fix-bitv (cdr (list)))

else nil endif

Theorem: xor-bitv-nlistp3 (¬ listp (x)) → ((xor-bitv (x, y) = nil) ∧ (xor-bitv (y, x) = fix-bitv (y)))

Event: Disable xor-bitv-nlistp.

Event: Disable xor-bitv-nlistp2.

Theorem: fix-bitv-all-but-last fix-bitv (all-but-last (x)) = all-but-last (fix-bitv (x))

Theorem: all-but-last-xor-bitv all-but-last (xor-bitv (a, b)) = if length (b) < length (a) then xor-bitv (all-but-last (a), b)

else xor-bitv (all-but-last (a), all-but-last (b)) endif

Theorem: least-bit-higher-cons-xor-bitv-hack (least-bit-higher-than-high-bit (cdr (x), a) ∧ least-bit-higher-than-high-bit (cdr (x), b)) → (least-bit-higher-than-high-bit (x, cons (0, xor-bitv (a, b)))

= listp (x))

Theorem: least-bit-higher-cdr-all-but-last least-bit-higher-than-high-bit (a, b) → least-bit-higher-than-high-bit (cdr (a), all-but-last (b))

Theorem: least-bit-higher-x-all-but-last-x at-most-one-bit-on (x) → least-bit-higher-than-high-bit (cdr (x), all-but-last (x))

Theorem: nat-to-bv-equiv-helper (bit-vectorp (cb, size) ∧ bit-vectorp (bv, size) ∧ (0 < size) ∧ ((bv-to-nat (bv) + (bv-to-nat (cb) ∗ value)) < exp (2, size)) ∧ at-most-one-bit-on (cb) ∧ least-bit-higher-than-high-bit (cb, bv)) → (nat-to-bv2-helper (value, cb, bv)

= nat-to-bv ((bv-to-nat (cb) ∗ value) + bv-to-nat (bv), size))

Theorem: at-most-one-bit-on-one-bit-vector at-most-one-bit-on (one-bit-vector (size))

Theorem: bv-to-nat-all-zero-bitvp all-zero-bitvp (x) → (bv-to-nat (x) = 0)

Theorem: least-bit-higher-than-high-bit-simple2 all-zero-bitvp (x) → (least-bit-higher-than-high-bit (y, x) = (length (x) = length (y)))

Theorem: length-zero-bit-vector length (zero-bit-vector (size)) = fix (size)

Theorem: length-one-bit-vector length (one-bit-vector (size)) = if size ≃ 0 then 1

else size endif

Theorem: nat-to-bv-equivalence ((value < exp (2, size)) ∧ (0 < size)) → (nat-to-bv2 (value, size) = nat-to-bv (value, size))

Theorem: correctness-of-nat-to-bv ((p0 = p-state (pc,

ctrl-stk, cons (v, temp-stk), prog-segment, data-segment, max-ctrl-stk-size, max-temp-stk-size, word-size,

'run))

∧ (car (v) = 'nat) ∧ (cddr (v) = nil) ∧ (p-current-instruction (p0 ) = '(call nat-to-bv)) ∧ (definition ('nat-to-bv, prog-segment) = nat-to-bv-program) ∧ (definition ('push-1-vector, prog-segment)

= push-1-vector-program (word-size)) ∧ (num = cadr (v)) ∧ nat-to-bv-input-conditionp (p0 )) → (p (p-state (pc,

ctrl-stk, cons (v, temp-stk), prog-segment, data-segment, max-ctrl-stk-size, max-temp-stk-size, word-size,

'run),

nat-to-bv-clock (num)) = p-state (add1-addr (pc),

ctrl-stk,

cons (list ('bitv, nat-to-bv (cadr (v), word-size)),

temp-stk), prog-segment, data-segment, max-ctrl-stk-size, max-temp-stk-size, word-size,

          'run))
;;;; bv-to-nat

Definition: bv-to-nat-program

= '(bv-to-nat
(bv)
((current-bit (nat 0)) (current-2power (nat 0)))
(push-constant (nat 1))
(pop-local current-2power)
(call push-1-vector)
(pop-local current-bit)
(push-constant (nat 0))
(dl loop nil (push-local bv))
(push-local current-bit)
(and-bitv)
(test-bitv-and-jump all-zero lab)
(push-local current-2power)
(add-nat)
(dl lab nil (push-local current-bit))
(lsh-bitv)
(set-local current-bit)
(test-bitv-and-jump all-zero done)
(push-local current-2power)
(mult2-nat)
(pop-local current-2power)
(jump loop)
(dl done nil (ret)))

Definition: example-bv-to-nat-state

= p-state ('(pc (main . 0)),
     '((nil (pc (main . 0)))),

nil,

     list ('(main nil nil
          (push-constant (bitv (1 0 1 1 0 0 0 1)))
          (call bv-to-nat)
          (ret)),

push-1-vector-program (8), bv-to-nat-program),

nil,

          8,
          8,
          'run)

Definition: trailing-zeros-helper (list, acc) = if listp (list)

then trailing-zeros-helper (cdr (list), if car (list) = 0 then 1 + acc else 0 endif)

else fix (acc) endif

Definition: trailing-zeros (list) = trailing-zeros-helper (list, 0)

Theorem: trailing-zeros-of-all-zero-bitvp all-zero-bitvp (bv) → (trailing-zeros-helper (bv, n) = (length (bv) + n))

Theorem: non-zero-means-acc-irrelevant-spec (¬ all-zero-bitvp (bv)) → (trailing-zeros-helper (bv, 1 + x) = trailing-zeros-helper (bv, x))

Theorem: non-zero-means-acc-irrelevant ((¬ all-zero-bitvp (bv)) ∧ (x ≠ 0)) → (trailing-zeros-helper (bv, x) = trailing-zeros-helper (bv, 0))

Theorem: trailing-zeros-helper-append trailing-zeros-helper (append (x, y), acc) = if all-zero-bitvp (y) then trailing-zeros-helper (x, acc)

+ length (y)

else trailing-zeros-helper (y, acc) endif

Theorem: trailing-zeros-append trailing-zeros (append (x, y)) = if all-zero-bitvp (y) then trailing-zeros (x) + length (y)

else trailing-zeros (y) endif

Theorem: lessp-trailing-zeros-helper (n ≮ (acc + length (x))) → ((n < trailing-zeros-helper (x, acc)) = f)

Definition: last (list) = if listp (list)

then if listp (cdr (list)) then last (cdr (list))

else car (list) endif else 0 endif Theorem: equal-trailing-zeros-helper-0 (trailing-zeros-helper (x, acc) = 0) = (((acc ≃ 0) ∧ (x ≃ nil)) ∨ (last (x) ≠ 0))

Theorem: lessp-length-cdr-trailing ((length (cdr (x)) < trailing-zeros-helper (x, acc)) ∧ listp (x)) → (all-zero-bitvp (x) ∧ all-zero-bitvp (cdr (x)))

Theorem: not-all-zero-bitvp-cdr-means (¬ all-zero-bitvp (cdr (x))) → (trailing-zeros-helper (x, acc) = trailing-zeros-helper (cdr (x), 0))

Definition: bv-to-nat2-helper (bv, cb, current-2power) = if all-zero-bitvp (cb) then 0

else if all-zero-bitvp (and-bitv (bv, cb)) then 0 else current-2power endif + bv-to-nat2-helper (bv,

append (cdr (cb), list (0)), 2 ∗ current-2power) endif

Definition: bv-to-nat2 (bv) = bv-to-nat2-helper (bv, one-bit-vector (length (bv)), 1)

Theorem: lessp-length-trailing-zeros-hack (acc ≃ 0) → (length (x) ≮ trailing-zeros-helper (x, acc))

Definition: bv-to-nat-loop-clock (cb, bv) = if all-zero-bitvp (cdr (cb))

then if (car (cb) = 0) ∨ (car (bv) = 0) then 9

else 11 endif else if all-zero-bitvp (and-bitv (cb, bv)) then 12

else 14 endif

+ bv-to-nat-loop-clock (append (cdr (cb), '(0)), bv) endif

Definition: bv-to-nat-induct (value, bv, cb, current-2power) = if all-zero-bitvp (cb) then 0

else bv-to-nat-induct (if all-zero-bitvp (and-bitv (bv, cb)) then 0 else current-2power endif + value, bv, append (cdr (cb), list (0)), 2 ∗ current-2power) endif Definition: double-cdr-with-sub1-induct (x, y, n) = if listp (x) then double-cdr-with-sub1-induct (cdr (x), cdr (y), n − 1)

else t endif

Theorem: bit-vectorp-and-bitv-better bit-vectorp (and-bitv (x, y), size) = (length (x) = fix (size))

Theorem: lessp-bv-to-nat-exp bit-vectorp (x, size) → (bv-to-nat (x) < exp (2, size))

Theorem: equal-bv-to-nat-0 bit-vectorp (x, size) → ((bv-to-nat (x) = 0) = all-zero-bitvp (x))

;(prove-lemma commutativity-of-and-bitv (rewrite)
;      (implies
;       (equal (length x) (length y))
;       (equal (and-bitv x y) (and-bitv y x))))

Event: Enable commutativity-of-and-bitv.

Theorem: commutativity2-of-and-bitv (length (x) = length (y)) → (and-bitv (x, and-bitv (y, z)) = and-bitv (y, and-bitv (x, z)))

Theorem: associativity-of-and-bitv (length (x) = length (y)) → (and-bitv (and-bitv (x, y), z) = and-bitv (x, and-bitv (y, z)))

Theorem: all-zero-bitvp-and-bitv all-zero-bitvp (x) → (all-zero-bitvp (and-bitv (x, y)) ∧ all-zero-bitvp (and-bitv (y, x)))

Theorem: bv-to-nat-loop-clock-open all-zero-bitvp (x) → (bv-to-nat-loop-clock (x, y) = 9)

Theorem: bv-to-nat2-helper-hack (all-zero-bitvp (z) ∧ (length (d) = length (z))) → (bv-to-nat2-helper (cons (1, d), cons (1, z), v) = fix (v))

Theorem: bv-to-nat2-helper-hack2 (all-zero-bitvp (z) ∧ (length (d) = length (z))) → (bv-to-nat2-helper (cons (0, d), cons (1, z), v) = 0)

Theorem: correctness-of-bv-to-nat-general (listp (ctrl-stk) ∧ at-least-morep (length (temp-stk), 3, max-temp-stk-size) ∧ (definition ('bv-to-nat, prog-segment) = bv-to-nat-program) ∧ (c2p ∈ N) ∧ (0 < word-size) ∧ at-most-one-bit-on (cb) ∧ (c2p = bv-to-nat (cb)) ∧ bit-vectorp (bv, word-size) ∧ bit-vectorp (cb, word-size) ∧ (value ∈ N) ∧ (value < c2p))

→ (p (p-state ('(pc (bv-to-nat . 5)),

cons (list (list (cons ('bv, list ('bitv, bv)),

                         cons ('current-bit, list ('bitv, cb)),
                         cons ('current-2power, list ('nat, c2p))),

ret-pc), ctrl-stk),

cons (list ('nat, value), temp-stk),

prog-segment, data-segment, max-ctrl-stk-size, max-temp-stk-size, word-size,

             'run),

bv-to-nat-loop-clock (cb, bv)) = p-state (ret-pc,

ctrl-stk,

cons (list ('nat,

bv-to-nat2-helper (bv, cb, c2p) + value), temp-stk),

prog-segment, data-segment, max-ctrl-stk-size, max-temp-stk-size, word-size,

              'run))

Definition: bv-to-nat-clock (word-size, bv) = (8 + bv-to-nat-loop-clock (one-bit-vector (word-size), bv))

Definition: bv-to-nat-input-conditionp (p0 )

= ((car (top (p-temp-stk (p0 ))) = 'bitv) ∧ (cddr (top (p-temp-stk (p0 ))) = nil) ∧ bit-vectorp (cadr (top (p-temp-stk (p0 ))), p-word-size (p0 )) ∧ at-least-morep (p-ctrl-stk-size (p-ctrl-stk (p0 )),

       7,

p-max-ctrl-stk-size (p0 ))

∧ (0 < p-word-size (p0 )) ∧ at-least-morep (length (p-temp-stk (p0 )),

       2,

p-max-temp-stk-size (p0 ))

∧ listp (p-ctrl-stk (p0 )))

Theorem: correctness-of-bv-to-nat-helper ((p0 = p-state (pc,

ctrl-stk, cons (list ('bitv, bv), temp-stk), prog-segment, data-segment, max-ctrl-stk-size, max-temp-stk-size, word-size,

'run))

∧ (p-current-instruction (p0 ) = '(call bv-to-nat)) ∧ (definition ('bv-to-nat, prog-segment) = bv-to-nat-program) ∧ (definition ('push-1-vector, prog-segment)

= push-1-vector-program (word-size)) ∧ bv-to-nat-input-conditionp (p0 )) → (p (p0 , bv-to-nat-clock (word-size, bv))

= p-state (add1-addr (pc), ctrl-stk, cons (list ('nat, bv-to-nat2 (bv)), temp-stk), prog-segment, data-segment, max-ctrl-stk-size, max-temp-stk-size, word-size,

  'run))

Theorem: bit-vectorp-append-better bit-vectorp (x, length (x)) → (bit-vectorp (append (x, y), size)

= (bit-vectorp (y, length (y)) ∧ (fix (size) = (length (x) + length (y)))))

Theorem: bit-vectorp-hack bit-vectorp (x, a + length (cdr (x))) = (if listp (x) then a = 1

else a ≃ 0 endif

∧ bit-vectorp (x, length (x)))

Theorem: bv-to-nat-one-bit ((¬ all-zero-bitvp (x)) ∧ at-most-one-bit-on (x) ∧ bit-vectorp (x, size)) → (bv-to-nat (x) = exp (2, trailing-zeros (x)))

Theorem: lessp-sub1-plus-hack ((x − 1) < (y + x)) = ((x ≄ 0) ∨ (y ≄ 0))

Theorem: quotient-plus-hack ((a + b + b) ÷ 2) = ((a ÷ 2) + b)

Theorem: bv-to-nat-all-but-last bit-vectorp (x, size) → (bv-to-nat (all-but-last (x)) = (bv-to-nat (x) ÷ 2))

Theorem: make-list-from-cons make-list-from (n, cons (a, b)) = if n ≃ 0 then nil

else cons (a, make-list-from (n − 1, b)) endif

Theorem: equal-plus-times-hack ((a + (a ∗ b) + (a ∗ c)) = (a ∗ d)) = ((a ≃ 0) ∨ ((1 + b + c) = d))

;(defn nth (n list)
;  (if (zerop n)
;      (car list)
;    (nth (sub1 n) (cdr list))))

Event: Enable nth.

Theorem: last-make-list-from last (make-list-from (n, x)) = if n ≃ 0 then 0

else nth (n − 1, x) endif

Theorem: make-list-from-nlistp (x ≃ nil) → (make-list-from (n, x) = zero-bit-vector (n))

Theorem: nth-nlistp (x ≃ nil) → (nth (n, x) = 0)

Theorem: bit-vectorp-make-list-from bit-vectorp (x, size) → bit-vectorp (make-list-from (n, x), n)

Theorem: equal-bv-to-nat-0-2 bit-vectorp (x, length (x)) → ((bv-to-nat (x) = 0) = all-zero-bitvp (x))

Theorem: bv-to-nat-make-list-from-from-sub1-make-list-from (bv-to-nat (make-list-from (n − 1, v)) = 0) → (bv-to-nat (make-list-from (n, v))

= if n ≃ 0 then 0 else fix-bit (nth (n − 1, v)) endif)

Theorem: plus-bv-to-nat-make-list-from (bv-to-nat (make-list-from (z − 1, v)) + bv-to-nat (make-list-from (z − 1, v))) = (bv-to-nat (make-list-from (z, v))

− fix-bit (last (make-list-from (z, v))))

Theorem: equal-bv-to-nat-1 bit-vectorp (x, length (x)) → ((bv-to-nat (x) = 1)

= (all-zero-bitvp (all-but-last (x)) ∧ (last (x) = 1)))

Theorem: lessp-1-hack (1 < a) = ((a ≄ 0) ∧ (a ≠ 1))

Theorem: not-equal-nth-0-means ((nth (n, v) ≠ 0) ∧ (n < s)) → (¬ all-zero-bitvp (make-list-from (s, v)))

Theorem: all-zero-bitvp-all-but-last-means (all-zero-bitvp (all-but-last (x)) ∧ (length (x) = length (y)) ∧ (0 < trailing-zeros-helper (y, acc))) → all-zero-bitvp (and-bitv (x, y))

Theorem: all-zero-bitvp-all-but-last-means-spec (all-zero-bitvp (all-but-last (x)) ∧ (length (x) = length (y)) ∧ (0 < trailing-zeros-helper (y, 0))) → all-zero-bitvp (and-bitv (x, y))

Theorem: all-zero-means-to-and-bitv all-zero-bitvp (x) → ((and-bitv (x, y) = zero-bit-vector (length (x)))

∧ (and-bitv (y, x) = zero-bit-vector (length (y))))

Theorem: trailing-zeros-nth-proof ((n = ((length (x) − trailing-zeros-helper (x, acc)) − 1)) ∧ (¬ all-zero-bitvp (x))) → (nth (n, x) ≠ 0)

Theorem: trailing-zeros-nth-spec ((n = ((length (x) − trailing-zeros-helper (x, 0)) − 1)) ∧ (¬ all-zero-bitvp (x))) → (nth (n, x) ≠ 0)

Theorem: and-bitv-special ((nth (n, w) = 0) ∧ (nth (n, x) ≠ 0) ∧ (length (x) = length (x)) ∧ at-most-one-bit-on (x)) → (and-bitv (w, x) = zero-bit-vector (length (w)))

Theorem: equal-trailing-zeros-length-spec (trailing-zeros-helper (x, acc) = (acc + length (x))) = all-zero-bitvp (x)

Theorem: equal-trailing-zeros-length (acc ≃ 0) → ((trailing-zeros-helper (x, acc) = length (x)) = all-zero-bitvp (x))

Theorem: bit-vectorp-trailing-zeros bit-vectorp (x, trailing-zeros-helper (x, acc)) = (all-zero-bitvp (x) ∧ bit-vectorp (x, length (x)) ∧ (acc ≃ 0))

Theorem: quotient-exp-hack (b ≄ 0) → (((x + exp (b, y)) ÷ b)

= if y ≃ 0 then (1 + x) ÷ b else exp (b, y − 1) + (x ÷ b) endif)

;(defn properp (list)
;  (if (listp list)
;      (properp (cdr list))
;    (equal list nil)))

Theorem: bit-vectorp-means-properp bit-vectorp (x, length (x)) → properp (x)

Theorem: make-list-from-simplify ((n = length (x)) ∧ properp (x)) → (make-list-from (n, x) = x)

Theorem: equal-add1-plus-hack (((1 + (a + b)) = (c + (d + a))) = ((1 + b) = (c + d))) ∧ (((1 + (a + b)) = (c + a)) = ((1 + b) = fix (c))) ∧ (((1 + a) = (b + a)) = (1 = fix (b)))

Theorem: plus-quotient-bv-to-nat ((bv-to-nat (x) ÷ 2) + (bv-to-nat (x) ÷ 2)) = (bv-to-nat (x) − fix-bit (last (x)))

Theorem: equal-plus-times-hack2 (((a ∗ b) + (a ∗ c)) = (a ∗ d)) = ((a ≃ 0) ∨ ((b + c) = fix (d)))

Theorem: and-bitv-special-special ((last (w) = 0) ∧ (last (x) ≠ 0) ∧ (length (x) = length (w)) ∧ at-most-one-bit-on (x)) → (and-bitv (w, x) = zero-bit-vector (length (w)))

Theorem: and-bitv-special-3 ((length (x) = length (y)) ∧ (last (x) ≠ 0) ∧ (last (y) ≠ 0)) → (¬ all-zero-bitvp (and-bitv (x, y)))

Theorem: and-bitv-special-4 ((nth (n, w) ≠ 0) ∧ (nth (n, x) ≠ 0) ∧ (length (x) = length (x))) → (¬ all-zero-bitvp (and-bitv (w, x)))

Theorem: and-bitv-special-5 ((last (w) = 0) ∧ (last (x) ≠ 0) ∧ ((1 + length (x)) = length (w)) ∧ at-most-one-bit-on (x)) → (and-bitv (w, cons (0, x)) = zero-bit-vector (length (w)))

Theorem: and-bitv-special-6 ((last (w) ≠ 0) ∧ (last (x) ≠ 0) ∧ ((1 + length (x)) = length (w))) → (¬ all-zero-bitvp (and-bitv (w, cons (0, x))))

Theorem: not-last-0-means-not-all-0 (last (x) ≠ 0) → (¬ all-zero-bitvp (x))

Theorem: bit-vectorp-plus-length-hack (bit-vectorp (x, z + length (x)) = (bit-vectorp (x, length (x)) ∧ (z ≃ 0))) ∧ (bit-vectorp (x, (1 + z) + length (cdr (x)))

= (bit-vectorp (x, length (x)) ∧ listp (x) ∧ (z ≃ 0)))

Theorem: last-append last (append (x, y)) = if listp (y) then last (y)

else last (x) endif

Theorem: bv-to-nat2-helper-bv-to-nat (at-most-one-bit-on (cb) ∧ bit-vectorp (cb, size) ∧ bit-vectorp (bv, size) ∧ (c2 = bv-to-nat (cb))) → (bv-to-nat2-helper (bv, cb, c2 )

= bv-to-nat (append (make-list-from (length (bv) − trailing-zeros (cb), bv), zero-bit-vector (trailing-zeros (cb)))))

Theorem: bv-to-nat2-helper-bv-to-nat-better (at-most-one-bit-on (cb) ∧ bit-vectorp (cb, length (cb)) ∧ bit-vectorp (bv, length (cb)) ∧ (c2 = bv-to-nat (cb))) → (bv-to-nat2-helper (bv, cb, c2 )

= bv-to-nat (append (make-list-from (length (bv) − trailing-zeros (cb), bv), zero-bit-vector (trailing-zeros (cb)))))

Theorem: nlistp-bv-to-nat2 (¬ listp (x)) → (bv-to-nat2-helper (x, a, b) = 0)

Theorem: bv-to-nat2-bv-to-nat-helper (x ≃ nil) → (bv-to-nat2 (x) = bv-to-nat (x))

Theorem: bit-vectorp-one-bit-vector-rewrite bit-vectorp (one-bit-vector (s), n) = if s ≃ 0 then n = 1

else fix (s) = fix (n) endif

Theorem: trailing-zeros-helper-one-bit-vector trailing-zeros-helper (one-bit-vector (n), acc) = 0

Theorem: bv-to-nat2-bv-to-nat bit-vectorp (x, length (x)) → (bv-to-nat2 (x) = bv-to-nat (x))

Theorem: bv-length-weaker bit-vectorp (x, s) → bit-vectorp (x, length (x))

Theorem: correctness-of-bv-to-nat ((p0 = p-state (pc,

ctrl-stk, cons (b, temp-stk), prog-segment, data-segment, max-ctrl-stk-size, max-temp-stk-size, word-size,

'run))

∧ (p-current-instruction (p0 ) = '(call bv-to-nat)) ∧ (definition ('bv-to-nat, prog-segment) = bv-to-nat-program) ∧ (definition ('push-1-vector, prog-segment)

= push-1-vector-program (word-size)) ∧ (bv = cadr (b)) ∧ bv-to-nat-input-conditionp (p0 )) → (p (p-state (pc,

ctrl-stk, cons (b, temp-stk), prog-segment, data-segment, max-ctrl-stk-size, max-temp-stk-size, word-size,

'run),

bv-to-nat-clock (word-size, bv)) = p-state (add1-addr (pc),

ctrl-stk,

cons (list ('nat, bv-to-nat (bv)), temp-stk), prog-segment, data-segment, max-ctrl-stk-size, max-temp-stk-size, word-size,

  'run))
;;;; number-with-at-least

Definition: number-with-at-least-program

= '(number-with-at-least
(nums-addr numnums min)

((i (nat 0)))
(push-constant (nat 0))
(set-local i)
(dl loop nil (push-local nums-addr))
(fetch)
(push-local min)
(lt-nat)
(test-bool-and-jump t lab)
(add1-nat)
(dl lab nil (push-local numnums))
(push-local i)
(add1-nat)
(set-local i)
(sub-nat)
(test-nat-and-jump zero done)
(push-local nums-addr)
(push-constant (nat 1))
(add-addr)
(pop-local nums-addr)
(jump loop)
(dl done nil (ret)))

Definition: example-number-with-at-least-state

= p-state ('(pc (main . 0)),
     '((nil (pc (main . 0)))),

nil,

     list ('(main nil nil
          (push-constant (addr (nums . 0)))
          (push-constant (nat 5))
          (push-constant (nat 3))
          (call number-with-at-least)
          (ret)),

number-with-at-least-program),

     '((nums
        (nat 3)
        (nat 8)
        (nat 9)
        (nat 2)
        (nat 100))),
     10,
     8,
     8,
     'run)

Definition: number-with-at-least (numlist, min) = if listp (numlist)

then if car (numlist) < min then number-with-at-least (cdr (numlist), min) else 1 + number-with-at-least (cdr (numlist), min) endif

else 0 endif

Definition: nat-list-piton (array, word-size) = if listp (array)

then listp (car (array))

∧ (caar (array) = 'nat) ∧ (cadar (array) ∈ N) ∧ (cddar (array) = nil) ∧ (cadar (array) < exp (2, word-size)) ∧ nat-list-piton (cdr (array), word-size)

else array = nil endif

Definition: number-with-at-least-general-induct (i, current, n, s, min, data-segment) = if i < n

then number-with-at-least-general-induct (1 + i,

if cadr (get (i,

array (s,

data-segment)))

< min then current else 1 + current endif, n, s, min, data-segment)

else t endif

Definition: number-with-at-least-clock-loop (i, min, array) = if i ≮ length (array) then 0

else if cadr (get (i, array)) < min then 0 else 1 endif + if (1 + i) = length (array) then 12

else 16 + number-with-at-least-clock-loop (1 + i, min, array) endif endif

Theorem: equal-difference-1 ((x − y) = 1) = (x = (1 + y))

Theorem: nat-list-piton-means (nat-list-piton (state, size) ∧ (p < length (state))) → ((car (get (p, state)) = 'nat)

∧ listp (get (p, state))

∧ (cadr (get (p, state)) ∈ N)

∧ (cadr (get (p, state)) < exp (2, size)) ∧ (cddr (get (p, state)) = nil))

Theorem: number-with-at-least-nlistp (¬ listp (x)) → (number-with-at-least (x, min) = 0)

Theorem: equal-add1-length ((1 + x) = length (y)) = (listp (y) ∧ (fix (x) = length (cdr (y))))

Event: Disable number-with-at-least-clock-loop.

Theorem: length-cdr-untag-array length (cdr (untag-array (x))) = length (cdr (x))

Theorem: number-with-at-least-correctness-general ((length (array (s, data-segment)) < exp (2, word-size)) ∧ (word-size ≄ 0) ∧ listp (ctrl-stk) ∧ nat-list-piton (array (s, data-segment), word-size) ∧ at-least-morep (length (temp-stk), 3, max-temp-stk-size) ∧ (definition ('number-with-at-least, prog-segment)

= number-with-at-least-program) ∧ definedp (s, data-segment) ∧ (min < exp (2, word-size)) ∧ (min ∈ N) ∧ (i < n) ∧ (i ∈ N) ∧ (n < exp (2, word-size)) ∧ (current ∈ N) ∧ (i ≮ current) ∧ (n = length (array (s, data-segment))))

→ (p (p-state ('(pc (number-with-at-least . 2)),

cons (list (list (cons ('nums-addr, list ('addr, cons (s, i))), cons ('numnums, list ('nat, n)), cons ('min, list ('nat, min)), cons ('i, list ('nat, i))),

ret-pc), ctrl-stk),

cons (list ('nat, current), temp-stk), prog-segment, data-segment, max-ctrl-stk-size, max-temp-stk-size, word-size,

          'run),

number-with-at-least-clock-loop (i, min, array (s, data-segment))) = p-state (ret-pc,

ctrl-stk,

cons (list ('nat,

current + number-with-at-least (nthcdr (i,

untag-array (array (s,

data-segment))),

min)),

temp-stk), prog-segment, data-segment, max-ctrl-stk-size, max-temp-stk-size, word-size,

           'run))

Definition: number-with-at-least-clock (min, array) = (3 + number-with-at-least-clock-loop (0, min, array))

Definition: number-with-at-least-input-conditionp (p0 ) = ((car (car (p-temp-stk (p0 ))) = 'nat)

∧ (cddr (car (p-temp-stk (p0 ))) = nil) ∧ (car (cadr (p-temp-stk (p0 ))) = 'nat) ∧ (cddr (cadr (p-temp-stk (p0 ))) = nil) ∧ (car (caddr (p-temp-stk (p0 ))) = 'addr) ∧ (cdadr (caddr (p-temp-stk (p0 ))) = 0) ∧ (cddr (caddr (p-temp-stk (p0 ))) = nil) ∧ listp (cadr (caddr (p-temp-stk (p0 )))) ∧ (length (array (car (cadr (caddr (p-temp-stk (p0 )))),

p-data-segment (p0 )))

< exp (2, p-word-size (p0 ))) ∧ (p-word-size (p0 ) ≄ 0) ∧ listp (p-ctrl-stk (p0 )) ∧ nat-list-piton (array (car (cadr (caddr (p-temp-stk (p0 )))),

p-data-segment (p0 )), p-word-size (p0 ))

∧ at-least-morep (p-ctrl-stk-size (p-ctrl-stk (p0 )),

                6,

p-max-ctrl-stk-size (p0 ))

∧ at-least-morep (length (p-temp-stk (p0 )),

                0,

p-max-temp-stk-size (p0 ))

∧ (definition ('number-with-at-least, p-prog-segment (p0 ))

= number-with-at-least-program) ∧ definedp (car (cadr (caddr (p-temp-stk (p0 )))), p-data-segment (p0 )) ∧ (cadr (car (p-temp-stk (p0 ))) < exp (2, p-word-size (p0 ))) ∧ (cadr (car (p-temp-stk (p0 ))) ∈ N) ∧ (0 < cadr (cadr (p-temp-stk (p0 )))) ∧ (cadr (cadr (p-temp-stk (p0 )))

= length (array (car (cadr (caddr (p-temp-stk (p0 )))), p-data-segment (p0 )))))

Theorem: correctness-of-number-with-at-least ((p0 = p-state (pc,

ctrl-stk,

cons (m, cons (n, cons (s, temp-stk))), prog-segment, data-segment, max-ctrl-stk-size, max-temp-stk-size, word-size,

          'run))

∧ (p-current-instruction (p0 ) = '(call number-with-at-least)) ∧ number-with-at-least-input-conditionp (p0 ) ∧ (minc = cadr (m)) ∧ (arrayc = array (car (cadr (s)), data-segment))) → (p (p-state (pc,

ctrl-stk,

cons (m, cons (n, cons (s, temp-stk))), prog-segment, data-segment, max-ctrl-stk-size, max-temp-stk-size, word-size,

          'run),

number-with-at-least-clock (minc, arrayc)) = p-state (add1-addr (pc),

ctrl-stk,

cons (list ('nat, number-with-at-least (untag-array (array (car (cadr (s)),

data-segment)),

cadr (m))),

temp-stk), prog-segment, data-segment, max-ctrl-stk-size, max-temp-stk-size, word-size,

          'run))
;; highest-bit

Definition: highest-bit-program

= '(highest-bit
(bv)
((cb (nat 0)))
(call push-1-vector)
(set-local cb)
(rsh-bitv)
(dl loop nil (push-local cb))
(test-bitv-and-jump all-zero done)
(push-local bv)
(push-local cb)
(and-bitv)
(test-bitv-and-jump all-zero lab)
(pop)
(push-local cb)
(dl lab nil (push-local cb))
(lsh-bitv)
(pop-local cb)
(jump loop)
(dl done nil (ret)))

Definition: example-highest-bit-state

= p-state ('(pc (main . 0)),
     '((nil (pc (main . 0)))),

nil,

     list ('(main nil nil
          (push-constant (bitv (0 0 0 0 0 0 0 0)))
          (call highest-bit)
          (push-constant (bitv (0 0 1 1 0 1 0 0)))

                (call highest-bit)
                (push-constant (bitv (1 0 1 1 0 1 0 0)))
                (call highest-bit)
                (ret)),

highest-bit-program, push-1-vector-program (8)),

nil,

          10,
          8,
          8,
          'run)

Definition: highest-bit (x) = if listp (x)

then if car (x) = 0 then cons (0, highest-bit (cdr (x)))

else cons (1, zero-bit-vector (length (cdr (x)))) endif else nil endif

Theorem: listp-highest-bit listp (highest-bit (x)) = listp (x)

Theorem: length-highest-bit length (highest-bit (x)) = length (x)

Definition: highest-bit-loop-clock (cb, bv) = if all-zero-bitvp (cb) then 3

else 10

+ if all-zero-bitvp (and-bitv (cb, bv)) then 0

else 2 endif + highest-bit-loop-clock (append (cdr (cb), '(0)), bv) endif

Definition: highest-bit-induct (current, bv, cb) = if all-zero-bitvp (cb) then t

else highest-bit-induct (if all-zero-bitvp (and-bitv (cb, bv)) then current else cb endif, bv, append (cdr (cb), '(0))) endif

Theorem: bit-vectorp-simple-not (length (x) ≠ fix (y)) → (¬ bit-vectorp (x, y))

Theorem: at-most-one-bit-on-cdr at-most-one-bit-on (x) → at-most-one-bit-on (cdr (x))

Theorem: equal-one-bit-vector (x = one-bit-vector (z)) = (((z ≃ 0) ∧ (x = '(1)))

∨ (bit-vectorp (x, z) ∧ all-zero-bitvp (all-but-last (x)) ∧ (last (x) ≠ 0)))

Theorem: at-most-one-bit-is-all-zeros (last (x) ≠ 0) → (at-most-one-bit-on (x) = all-zero-bitvp (all-but-last (x)))

Definition: highest-bit2-helper (current, cb, bv) = if all-zero-bitvp (cb) then current

else highest-bit2-helper (if all-zero-bitvp (and-bitv (bv, cb)) then current else cb endif, append (cdr (cb), '(0)), bv) endif

Theorem: equal-x-zero-bit-vector (x = zero-bit-vector (y)) = (all-zero-bitvp (x) ∧ bit-vectorp (x, y))

Theorem: all-zero-bitvp-all-but-last-simple all-zero-bitvp (x) → all-zero-bitvp (all-but-last (x))

Theorem: equal-trailing-zeros-acc-irrelevant (trailing-zeros-helper (x, acc1 ) = trailing-zeros-helper (x, acc2 )) = ((fix (acc1 ) = fix (acc2 )) ∨ (¬ all-zero-bitvp (x)))

Theorem: lessp-trailing-zeros (¬ all-zero-bitvp (z)) → (trailing-zeros-helper (z, acc) < length (z))

Theorem: nthcdr-append nthcdr (n, append (x, y)) = if length (x) < n then nthcdr (n − length (x), y)

else append (nthcdr (n, x), y) endif

Theorem: listp-zero-bit-vector listp (zero-bit-vector (x)) = (x ≄ 0)

Theorem: and-bitv-append and-bitv (append (x, y), z) = append (and-bitv (x, make-list-from (length (x), z)),

and-bitv (y, nthcdr (length (x), z)))

Theorem: and-bitv-append2 (length (append (x, y)) = length (z)) → (and-bitv (z, append (x, y))

= append (and-bitv (x, make-list-from (length (x), z)), and-bitv (y, nthcdr (length (x), z))))

Theorem: all-zero-bitvp-and-bitv-append all-zero-bitvp (and-bitv (z, append (x, y))) = (all-zero-bitvp (and-bitv (make-list-from (length (x), z), x))

∧ all-zero-bitvp (and-bitv (nthcdr (length (x), z), y)))

Theorem: length-cdr-zero-bit-vector length (cdr (zero-bit-vector (x))) = (x − 1)

Theorem: length-nthcdr length (nthcdr (n, x)) = (length (x) − n)

Event: Disable and-bitv-special.

Event: Disable and-bitv-special-special.

Event: Disable and-bitv-special-3.

Event: Disable and-bitv-special-4.

Event: Disable and-bitv-special-5.

Event: Disable and-bitv-special-6.

Theorem: bit-vectorp-zero-bit-vector-better bit-vectorp (zero-bit-vector (x), size) = (fix (x) = fix (size))

Theorem: highest-bit-correctness-general ((word-size ≄ 0) ∧ at-most-one-bit-on (cb) ∧ listp (ctrl-stk) ∧ at-least-morep (length (temp-stk), 3, max-temp-stk-size) ∧ (definition ('highest-bit, prog-segment) = highest-bit-program) ∧ bit-vectorp (bv, word-size) ∧ bit-vectorp (cb, word-size) ∧ bit-vectorp (current, word-size))

 → (p (p-state ('(pc (highest-bit . 3)),

cons (list (list (cons ('bv, list ('bitv, bv)),

cons ('cb, list ('bitv, cb))), ret-pc),

ctrl-stk), cons (list ('bitv, current), temp-stk), prog-segment, data-segment, max-ctrl-stk-size, max-temp-stk-size, word-size,

              'run),

highest-bit-loop-clock (cb, bv)) = p-state (ret-pc,

ctrl-stk,

cons (list ('bitv, highest-bit2-helper (current, cb, bv)),

temp-stk), prog-segment, data-segment, max-ctrl-stk-size, max-temp-stk-size, word-size,

                'run))

Theorem: make-list-from-simple (n ≃ 0) → (make-list-from (n, x) = nil)

Theorem: not-all-zero-bitvp-make-list-from (all-zero-bitvp (make-list-from (n1 , x)) ∧ (n1 ≮ n2 )) → all-zero-bitvp (make-list-from (n2 , x))

Event: Disable nthcdr-open.

;(prove-lemma listp-append (rewrite)
;      (equal
;       (listp (append x y))
;       (or (listp x) (listp y))))

Event: Enable listp-append.

Theorem: highest-bit2-helper-cons-1 ((¬ all-zero-bitvp (cb)) ∧ at-most-one-bit-on (cb) ∧ (length (cb) = length (bv)) ∧ bit-vectorp (cb, length (cb))

∧ (car (bv) = 1)) → (highest-bit2-helper (current, cb, bv)

= cons (1, zero-bit-vector (length (cdr (bv)))))

Theorem: bit-vectorp-append-cdr-hack bit-vectorp (x, n) → (bit-vectorp (append (cdr (x), '(0)), n) = listp (x))

Definition: triple-cdr-with-sub1-induct (x, y, z, n) = if n ≃ 0 then t

else triple-cdr-with-sub1-induct (cdr (x), cdr (y), cdr (z), n − 1) endif

Theorem: car-append-better car (append (x, y)) = if listp (x) then car (x)

else car (y) endif

Theorem: open-highest-when-and-not-0 ((¬ all-zero-bitvp (and-bitv (x, y))) ∧ (length (x) = length (y))) → (highest-bit2-helper (c, x, y)

= highest-bit2-helper (x, append (cdr (x), '(0)), y))

;(prove-lemma cdr-append (rewrite)
;      (equal
;       (cdr (append x y))
;       (if (listp x)
;   (append (cdr x) y)
; (cdr y))))

Event: Enable cdr-append.

Theorem: highest-bit2-helper-cons-0 ((¬ all-zero-bitvp (cb)) ∧ at-most-one-bit-on (cb) ∧ bit-vectorp (cb, size) ∧ bit-vectorp (bv, size) ∧ bit-vectorp (current, size) ∧ (car (bv) = 0) ∧ (car (current) = 0)) → (highest-bit2-helper (current, cb, bv)

= cons (0, highest-bit2-helper (cdr (current), cdr (cb), cdr (bv))))

Theorem: highest-bit2-helper-cons-0-rewrite ((¬ all-zero-bitvp (cb)) ∧ at-most-one-bit-on (cb)

∧ bit-vectorp (cb, length (cb)) ∧ bit-vectorp (bv, length (cb)) ∧ bit-vectorp (current, length (cb)) ∧ (car (bv) = 0) ∧ (car (current) = 0)) → (highest-bit2-helper (current, cb, bv)

= cons (0, highest-bit2-helper (cdr (current), cdr (cb), cdr (bv))))

Theorem: append-zeros-0 (all-zero-bitvp (x) ∧ properp (x)) → (append (x, '(0)) = cons (0, x))

Theorem: highest-bit2-helper-cons-helper (bit-vectorp (bv, size) ∧ bit-vectorp (cb, size) ∧ at-most-one-bit-on (cb) ∧ at-most-one-bit-on (current) ∧ (¬ all-zero-bitvp (cb)) ∧ (all-zero-bitvp (current)

∨ (trailing-zeros (current) < trailing-zeros (cb))) ∧ bit-vectorp (current, size) ∧ (size ≄ 0)) → (highest-bit2-helper (current, cb, bv)

= if car (bv) = 0 then cons (0,

highest-bit2-helper (cdr (current), cdr (cb), cdr (bv)))

else cons (1, zero-bit-vector (size − 1)) endif)

Theorem: highest-bit2-helper-cons-helper-rewrite (bit-vectorp (bv, length (bv)) ∧ bit-vectorp (cb, length (bv)) ∧ at-most-one-bit-on (cb) ∧ at-most-one-bit-on (current) ∧ (¬ all-zero-bitvp (cb)) ∧ (all-zero-bitvp (current)

∨ (trailing-zeros (current) < trailing-zeros (cb))) ∧ bit-vectorp (current, length (bv)) ∧ listp (bv)) → (highest-bit2-helper (current, cb, bv)

= if car (bv) = 0 then cons (0,

highest-bit2-helper (cdr (current), cdr (cb), cdr (bv)))

else cons (1, zero-bit-vector (length (bv) − 1)) endif)

Theorem: bit-vectorp-cdr-from-free bit-vectorp (x, n) → (bit-vectorp (cdr (x), s) = ((1 + s) = n))

Theorem: all-zero-bitvp-one-bit-vector ¬ all-zero-bitvp (one-bit-vector (x))

Theorem: trailing-zeros-one-bit-vector trailing-zeros (one-bit-vector (n)) = 0

Theorem: cdr-zero-one-bit-vector (cdr (one-bit-vector (x)) = if x < 2 then nil

else one-bit-vector (x − 1) endif) ∧ (cdr (zero-bit-vector (x))

= if x ≃ 0 then 0 else zero-bit-vector (x − 1) endif)

Theorem: highest-bit2-helper-highest-bit (bit-vectorp (bv, word-size) ∧ (word-size ≄ 0)) → (highest-bit2-helper (zero-bit-vector (word-size),

one-bit-vector (word-size), bv)

= highest-bit (bv))

Definition: highest-bit-input-conditionp (p0 ) = ((car (top (p-temp-stk (p0 ))) = 'bitv)

∧ (cddr (top (p-temp-stk (p0 ))) = nil)

∧ (p-word-size (p0 ) ≄ 0) ∧ listp (p-ctrl-stk (p0 )) ∧ at-least-morep (p-ctrl-stk-size (p-ctrl-stk (p0 )),

                     6,

p-max-ctrl-stk-size (p0 ))

∧ at-least-morep (length (p-temp-stk (p0 )),

                     2,

p-max-temp-stk-size (p0 ))

∧ (definition ('highest-bit, p-prog-segment (p0 ))

= highest-bit-program) ∧ (definition ('push-1-vector, p-prog-segment (p0 )) = push-1-vector-program (p-word-size (p0 )))

∧ bit-vectorp (cadr (top (p-temp-stk (p0 ))), p-word-size (p0 )))

Definition: highest-bit-clock (bv) = (6 + highest-bit-loop-clock (one-bit-vector (length (bv)), bv))

Theorem: cons-0-zero-bit-vector cons (0, zero-bit-vector (x)) = zero-bit-vector (1 + x)

Event: Disable cons-0-zero-bit-vector.

Theorem: correctness-of-highest-bit ((p0 = p-state (pc,

ctrl-stk, cons (b, temp-stk), prog-segment, data-segment, max-ctrl-stk-size, max-temp-stk-size, word-size,

'run))

∧ (p-current-instruction (p0 ) = '(call highest-bit)) ∧ (bc = cadr (b)) ∧ highest-bit-input-conditionp (p0 )) → (p (p-state (pc,

ctrl-stk, cons (b, temp-stk), prog-segment, data-segment, max-ctrl-stk-size, max-temp-stk-size, word-size,

'run),

highest-bit-clock (bc)) = p-state (add1-addr (pc),

ctrl-stk,

cons (list ('bitv, highest-bit (cadr (b))), temp-stk), prog-segment, data-segment, max-ctrl-stk-size, max-temp-stk-size, word-size,

  'run))
;; match-and-xor

Definition: match-and-xor-program

= '(match-and-xor
(vecs numvecs match xor-vector)
((i (nat 0)))
(push-constant (nat 0))

(pop-local i)
(dl loop nil (push-local vecs))
(fetch)
(push-local match)
(and-bitv)
(test-bitv-and-jump not-all-zeros found)
(push-local i)
(add1-nat)
(set-local i)
(push-local numvecs)
(lt-nat)
(test-bool-and-jump f done)
(push-local vecs)
(push-constant (nat 1))
(add-addr)
(pop-local vecs)
(jump loop)
(dl found nil (push-local vecs))
(fetch)
(push-local xor-vector)
(xor-bitv)
(push-local vecs)
(deposit)
(dl done nil (ret)))

Definition: example-match-and-xor-p-state

= p-state ('(pc (main . 0)),
     '((nil (pc (main . 0)))),

nil,

     list ('(main nil nil
          (push-constant (addr (arr . 0)))
          (push-constant (nat 6))
          (push-constant (bitv (0 0 0 1 0 0 0 0)))
          (push-constant (bitv (1 1 1 1 1 1 1 1)))
          (call match-and-xor)
          (ret)),

match-and-xor-program),

     '((arr
        (bitv (0 1 0 0 1 0 0 1))
        (bitv (0 0 0 0 0 0 0 1))
        (bitv (0 0 0 1 0 0 0 1))
        (bitv (0 0 0 0 0 0 0 1))
        (bitv (0 0 0 1 0 0 0 1))

             (bitv (0 1 1 0 1 0 0 1)))),
          10,
          8,
          8,
          'run)

Definition: match-and-xor (bvs, match, xor-vector) = if listp (bvs)

then if all-zero-bitvp (and-bitv (car (bvs), match))

then cons (car (bvs), match-and-xor (cdr (bvs), match, xor-vector)) else cons (xor-bitv (car (bvs), xor-vector), cdr (bvs)) endif

else nil endif

Definition: match-and-xor-loop-clock (bvs, match) = if listp (bvs)

then if all-zero-bitvp (and-bitv (car (bvs), match))

then if listp (cdr (bvs))

then 16 + match-and-xor-loop-clock (cdr (bvs), match) else 12 endif

else 12 endif else 0 endif

Definition: tag-array (tag, array) = if listp (array)

then cons (tag (tag, car (array)), tag-array (tag, cdr (array)))

else nil endif

Definition: match-and-xor-general-induct (numvecs, i) = if i < numvecs then match-and-xor-general-induct (numvecs, 1 + i)

else t endif

Theorem: tag-array-untag-array bit-vectors-piton (x, length (untag (car (x)))) → (tag-array ('bitv, untag-array (x)) = x)

Theorem: bit-vectors-piton-free-means bit-vectors-piton (x, size) → (bit-vectors-piton (x, length (cadr (car (x))))

∧ (bit-vectors-piton (cdr (x), length (cadr (cadr (x)))) = listp (x)))

Theorem: listp-cdr-nthcdr listp (cdr (nthcdr (i, x))) = (i < length (cdr (x)))

Theorem: nthcdr-untag-array nthcdr (i, untag-array (x)) = if i < length (x) then untag-array (nthcdr (i, x))

elseif fix (i) = length (x) then nil else 0 endif

Theorem: put-length-cdr properp (x) → (put (val, length (cdr (x)), x) = append (all-but-last (x), list (val)))

Theorem: nthcdr-length-cdr properp (x) → (nthcdr (length (cdr (x)), x)

= if listp (x) then list (last (x))

else nil endif)

Theorem: get-length-cdr get (length (cdr (x)), x) = if listp (x) then last (x)

else 0 endif

Theorem: append-all-but-last-last properp (x) → (append (all-but-last (x), list (last (x)))

= if x ≃ nil then list (last (x))

else x endif)

Theorem: listp-cdr-untag-array listp (cdr (untag-array (x))) = listp (cdr (x))

Theorem: bit-vectorp-last bit-vectors-piton (bvs, s) → (bit-vectorp (cadr (last (bvs)), s) = listp (bvs))

Theorem: bit-vectors-piton-means-properp bit-vectors-piton (x, s) → properp (x)

Theorem: bit-vectors-piton-means-last (bit-vectors-piton (state, size) ∧ listp (state)) → ((car (last (state)) = 'bitv)

∧ listp (last (state))

∧ bit-vectorp (cadr (last (state)), size) ∧ (cddr (last (state)) = nil) ∧ (length (cadr (last (state))) = fix (size)))

Theorem: list-bitv-cadr-bitvp ((car (x) = 'bitv) ∧ (cddr (x) = nil)) → (list ('bitv, cadr (x)) = x)

Theorem: equal-x-put-assoc-x (x = put-assoc (val, name, x)) = ((¬ definedp (name, x)) ∨ (assoc (name, x) = cons (name, val)))

Theorem: cons-n-assoc-n listp (assoc (n, d)) → (cons (n, cdr (assoc (n, d)))

= if definedp (n, d) then assoc (n, d) else cons (n, 0) endif)

Theorem: cons-n-cadr-list-assoc-n (cddr (assoc (n, d)) = nil) → (list (n, cadr (assoc (n, d)))

= if definedp (n, d) then assoc (n, d) else cons (n, 0) endif)

Theorem: cons-n-assoc-n-hack listp (cdr (assoc (n, d))) → (cons (n, cdr (assoc (n, d)))

= if definedp (n, d) then assoc (n, d) else cons (n, 0) endif)

Theorem: car-untag-array car (untag-array (x)) = untag (car (x))

Theorem: car-nthcdr car (nthcdr (i, x)) = get (i, x)

Theorem: tag-array-cdr-untag-array-hack bit-vectors-piton (x, length (untag (car (x)))) → (tag-array ('bitv, cdr (untag-array (x)))

= if listp (x) then cdr (x) else nil endif)

Theorem: bit-vectors-piton-means-car (bit-vectors-piton (state, size) ∧ listp (state)) → ((caar (state) = 'bitv)

∧ listp (car (state))

∧ bit-vectorp (cadr (car (state)), size) ∧ (cddr (car (state)) = nil) ∧ (length (cadr (car (state))) = fix (size)))

Theorem: equal-put-assoc (put-assoc (v1 , n, s) = put-assoc (v2 , n, s)) = ((¬ definedp (n, s)) ∨ (v1 = v2 ))

Theorem: get-nlistp-better (i ≮ length (x)) → (get (i, x) = 0)

Theorem: equal-append-zero-bit-vector-zero-bit-vector (append (zero-bit-vector (n1 ), x) = append (zero-bit-vector (n2 ), y)) = if n1 < n2 then x = append (zero-bit-vector (n2 − n1 ), y)

else y = append (zero-bit-vector (n1 − n2 ), x) endif

Theorem: append-make-list-from-cons-get-hack append (make-list-from (i, x), cons (get (i, x), y)) = append (make-list-from (1 + i, x), y)

Theorem: cdr-untag-array-nthcdr (i < length (x)) → (cdr (untag-array (nthcdr (i, x))) = untag-array (nthcdr (i, cdr (x))))

Theorem: equal-nil-nthcdr-length (nil = nthcdr (length (x), x)) = properp (x)

Theorem: lessp-0-length-better (x ≃ 0) → ((x < length (y)) = listp (y))

Theorem: bit-vectors-piton-means-get-cdr bit-vectors-piton (state, size) → ((car (get (i, cdr (state)))

= if i < length (cdr (state)) then 'bitv

else 0 endif) ∧ (listp (get (i, cdr (state))) = (i < length (cdr (state)))) ∧ (bit-vectorp (cadr (get (i, cdr (state))), size)

= (i < length (cdr (state)))) ∧ (cddr (get (i, cdr (state)))

= if i < length (cdr (state)) then nil

else 0 endif)

∧ (length (cadr (get (i, cdr (state))))

= if i < length (cdr (state)) then fix (size) else 0 endif))

Theorem: bit-vectors-piton-nthcdr bit-vectors-piton (x, s1 ) → ((bit-vectors-piton (nthcdr (i, x), s)

= (((i < length (x)) ∧ (fix (s1 ) = fix (s)))

∨ (fix (i) = length (x)))) ∧ (bit-vectors-piton (nthcdr (i, cdr (x)), s)

= ((i < length (x))

∧ ((fix (s) = fix (s1 )) ∨ (fix (i) = length (cdr (x)))))))

Theorem: tag-array-untag-array-nthcdr-cddr-hack ((i < length (x)) ∧ bit-vectors-piton (x, s)) → (tag-array ('bitv, untag-array (nthcdr (i, cdr (x))))

= nthcdr (i, cdr (x)))

Theorem: append-make-list-from-put-hack (i < length (x)) → (append (make-list-from (i, x), cons (v, nthcdr (i, cdr (x)))) = put (v, i, x))

Event: Enable lessp-sub1-x-x.

Event: Enable lessp-x-x.

Theorem: correctness-of-match-and-xor-general (listp (ctrl-stk) ∧ at-least-morep (p-ctrl-stk-size (ctrl-stk), 7, max-ctrl-stk-size) ∧ at-least-morep (length (temp-stk), 4, max-temp-stk-size) ∧ (definition ('match-and-xor, prog-segment)

= match-and-xor-program) ∧ bit-vectorp (match, word-size) ∧ bit-vectorp (xor-vector, word-size) ∧ (numvecs = length (array (vecs, data-segment))) ∧ bit-vectors-piton (array (vecs, data-segment), word-size) ∧ definedp (vecs, data-segment) ∧ (i ∈ N) ∧ (i < numvecs) ∧ (length (array (vecs, data-segment)) < exp (2, word-size)))

→ (p (p-state ('(pc (match-and-xor . 2)),

cons (list (list (cons ('vecs, list ('addr, cons (vecs, i))), cons ('numvecs, list ('nat, numvecs)), cons ('match, list ('bitv, match)),

                         cons ('xor-vector,

list ('bitv, xor-vector)), cons ('i, list ('nat, i))),

ret-pc), ctrl-stk),

temp-stk, prog-segment, data-segment, max-ctrl-stk-size, max-temp-stk-size, word-size,

'run),

match-and-xor-loop-clock (nthcdr (i,

untag-array (array (vecs,

data-segment))),

match))

= p-state (ret-pc, ctrl-stk, temp-stk, prog-segment, put-assoc (append (make-list-from (i,

array (vecs,

data-segment)),

tag-array ('bitv,

match-and-xor (untag-array (nthcdr (i,

array (vecs,

data-segment))),

match,

xor-vector))),

vecs,

data-segment),

max-ctrl-stk-size, max-temp-stk-size, word-size,

'run))

Definition: match-and-xor-clock (bvs, match) = (3 + match-and-xor-loop-clock (bvs, match))

Definition: match-and-xor-input-conditionp (p0 ) = ((car (top (p-temp-stk (p0 ))) = 'bitv)

∧ (cddr (top (p-temp-stk (p0 ))) = nil) ∧ (car (top (cdr (p-temp-stk (p0 )))) = 'bitv) ∧ (cddr (top (cdr (p-temp-stk (p0 )))) = nil) ∧ (car (top (cddr (p-temp-stk (p0 )))) = 'nat) ∧ (cddr (top (cddr (p-temp-stk (p0 )))) = nil) ∧ (car (top (cdddr (p-temp-stk (p0 )))) = 'addr) ∧ (cdr (cadr (top (cdddr (p-temp-stk (p0 ))))) = 0) ∧ listp (cadr (top (cdddr (p-temp-stk (p0 )))))

∧ (cddr (top (cdddr (p-temp-stk (p0 )))) = nil) ∧ (cadr (top (cddr (p-temp-stk (p0 )))) ≄ 0) ∧ listp (p-ctrl-stk (p0 )) ∧ at-least-morep (p-ctrl-stk-size (p-ctrl-stk (p0 )),

                7,

p-max-ctrl-stk-size (p0 ))

∧ at-least-morep (length (p-temp-stk (p0 )),

                0,

p-max-temp-stk-size (p0 ))

∧ (definition ('match-and-xor, p-prog-segment (p0 ))

= match-and-xor-program) ∧ bit-vectorp (cadr (top (cdr (p-temp-stk (p0 )))), p-word-size (p0 )) ∧ bit-vectorp (cadr (top (p-temp-stk (p0 ))), p-word-size (p0 )) ∧ (cadr (top (cddr (p-temp-stk (p0 ))))

= length (array (car (cadr (top (cdddr (p-temp-stk (p0 ))))), p-data-segment (p0 ))))

∧ definedp (car (cadr (top (cdddr (p-temp-stk (p0 ))))),

p-data-segment (p0 ))

∧ (length (array (car (cadr (top (cdddr (p-temp-stk (p0 ))))),

p-data-segment (p0 )))

< exp (2, p-word-size (p0 ))) ∧ bit-vectors-piton (array (car (cadr (top (cdddr (p-temp-stk (p0 ))))),

p-data-segment (p0 )), p-word-size (p0 )))

Theorem: correctness-of-match-and-xor ((p0 = p-state (pc,

ctrl-stk,

cons (x, cons (m, cons (n, cons (v, temp-stk)))), prog-segment, data-segment, max-ctrl-stk-size, max-temp-stk-size, word-size,

          'run))

∧ (p-current-instruction (p0 ) = '(call match-and-xor)) ∧ match-and-xor-input-conditionp (p0 ) ∧ (match = cadr (m)) ∧ (vecs-to-match = untag-array (array (caadr (v), data-segment)))) → (p (p-state (pc,

ctrl-stk,

cons (x, cons (m, cons (n, cons (v, temp-stk)))), prog-segment, data-segment, max-ctrl-stk-size, max-temp-stk-size, word-size,

         'run),

match-and-xor-clock (vecs-to-match, match)) = p-state (add1-addr (pc),

ctrl-stk, temp-stk, prog-segment, put-assoc (tag-array ('bitv,

match-and-xor (untag-array (array (caadr (v),

data-segment)),

cadr (m), cadr (x))),

caadr (v), data-segment),

max-ctrl-stk-size, max-temp-stk-size, word-size,

          'run))
;;; nat-to-bv-list

Definition: nat-to-bv-list-program

= '(nat-to-bv-list
(nat-list bv-list length)
((i (nat 0)))
(dl loop nil (push-local nat-list))
(fetch)
(call nat-to-bv)
(push-local bv-list)
(deposit)
(push-local i)
(add1-nat)
(set-local i)
(push-local length)
(eq)
(test-bool-and-jump t done)
(push-local nat-list)
(push-constant (nat 1))
(add-addr)
(pop-local nat-list)

      (push-local bv-list)
      (push-constant (nat 1))
      (add-addr)
      (pop-local bv-list)
      (jump loop)
      (dl done nil (ret)))

Definition: example-nat-to-bv-list-p-state

= p-state ('(pc (main . 0)),
          '((nil (pc (main . 0)))),

nil,

          list ('(main nil nil
                (push-constant (addr (arr . 0)))
                (push-constant (addr (arr2 . 0)))
                (push-constant (nat 6))
                (call nat-to-bv-list)
                (ret)),

nat-to-bv-list-program, nat-to-bv-program, push-1-vector-program (8)),

          '((arr
             (nat 3)
             (nat 5)
             (nat 8)
             (nat 0)
             (nat 23)
             (nat 9))
            (arr2 nil nil nil nil nil nil)),
          100,
          80,
          8,
          'run)

Definition: nat-to-bv-list (nat-list, size) = if listp (nat-list)

then cons (nat-to-bv (car (nat-list), size),

nat-to-bv-list (cdr (nat-list), size))

else nil endif

Definition: nat-to-bv-list-loop-clock (i, nats) = if i < length (nats)

then clock-plus ('2, clock-plus (nat-to-bv-clock (untag (get (i, nats))), if i < length (cdr (nats)) then clock-plus ('17,

nat-to-bv-list-loop-clock (1 + i,

nats))

else '9 endif))

else '0 endif

Definition: nat-to-bv-list-loop-induct (i, nats, bvs-name, word-size, data-segment) = if (i < length (nats)) ∧ (i < length (cdr (nats)))

then nat-to-bv-list-loop-induct (1 + i, nats, bvs-name, word-size, put-assoc (append (make-list-from (i,

cdr (assoc (bvs-name,

data-segment))),

cons (list ('bitv,

nat-to-bv (untag (get (i,

nats)),

word-size)),

nthcdr (1 + i,

cdr (assoc (bvs-name,

data-segment))))),

bvs-name, data-segment))

else t endif

Theorem: nat-list-piton-means-car (nat-list-piton (state, size) ∧ listp (state)) → ((caar (state) = 'nat)

∧ listp (car (state))

∧ (cadr (car (state)) ∈ N)

∧ (cadr (car (state)) < exp (2, size))

∧ ((cadr (car (state)) < exp (2, size)) = t)

∧ (cddr (car (state)) = nil))

Definition: array-pitonp (array, length) = if listp (array)

then (length ≄ 0) ∧ array-pitonp (cdr (array), length − 1)

else (array = nil) ∧ (length ≃ 0) endif

Theorem: nat-list-piton-means-last nat-list-piton (state, size) → ((car (last (state))

= if listp (state) then 'nat

else 0 endif) ∧ (listp (last (state)) = listp (state)) ∧ (cadr (last (state)) ∈ N) ∧ ((cadr (last (state)) < exp (2, size)) = t) ∧ (cddr (last (state))

= if listp (state) then nil else 0 endif))

Theorem: nat-list-piton-means-last-cdr (nat-list-piton (state, size) ∧ listp (state)) → ((car (last (cdr (state)))

= if listp (cdr (state)) then 'nat

else 0 endif) ∧ (listp (last (cdr (state))) = listp (cdr (state))) ∧ (cadr (last (cdr (state))) ∈ N) ∧ ((cadr (last (cdr (state))) < exp (2, size)) = t) ∧ (cddr (last (cdr (state)))

= if listp (cdr (state)) then nil else 0 endif))

;(prove-lemma definedp-put-assoc (rewrite)
;      (equal
;       (definedp n (put-assoc v n1 a))
;       (definedp n a)))

Event: Enable definedp-put-assoc.

Theorem: assoc-put-assoc-better assoc (n1 , put-assoc (v, n2 , a)) = if definedp (n1 , a)

then if n1 = n2 then cons (n1 , v) else assoc (n1 , a) endif

else f endif

Event: Disable nat-to-bv-list-loop-clock.

Theorem: get-add1 (n < 4) → (get (1 + n, x) = get (n, cdr (x)))

Theorem: get-0-better (n ≃ 0) → (get (n, x) = car (x))

Theorem: length-cdr-tag-array length (cdr (tag-array (l, x))) = length (cdr (x))

Theorem: length-nat-to-bv-list length (nat-to-bv-list (x, s)) = length (x)

Theorem: length-cdr-nat-to-bv-list length (cdr (nat-to-bv-list (x, s))) = length (cdr (x))

Theorem: length-tag-array length (tag-array (l, x)) = length (x)

Theorem: listp-tag-array listp (tag-array (l, x)) = listp (x)

Theorem: listp-nat-to-bv-list listp (nat-to-bv-list (x, s)) = listp (x)

Theorem: array-pitonp-tag-array array-pitonp (tag-array (l, x), length) = (length (x) = fix (length))

Theorem: array-pitonp-append array-pitonp (append (x, y), size) = ((size ≮ length (x)) ∧ array-pitonp (y, size − length (x)))

Theorem: nat-list-piton-means-cadr (nat-list-piton (state, size) ∧ listp (cdr (state))) → ((caadr (state) = 'nat)

∧ listp (cadr (state))

∧ (cadr (cadr (state)) ∈ N)

∧ (cadr (cadr (state)) < exp (2, size))

∧ ((cadr (cadr (state)) < exp (2, size)) = t) ∧ (cddr (cadr (state)) = nil))

Theorem: array-pitonp-add1 array-pitonp (x, 1 + n) = (listp (x) ∧ array-pitonp (cdr (x), n))

;(prove-lemma put-assoc-put-assoc (rewrite)
;      (equal
;       (put-assoc v n (put-assoc v2 n a))
;       (put-assoc v n a)))

Event: Enable put-assoc-put-assoc.

Theorem: length-cdr-nlistp (¬ listp (cdr (x))) → (length (x)

= if listp (x) then 1 else 0 endif)

Theorem: equal-nil-cdr-tag-array-hack (nil = cdr (tag-array (l, x))) = (length (x) = 1)

Theorem: length-from-array-pitonp array-pitonp (x, s) → (length (x) = fix (s))

Event: Disable nat-to-bv-clock.

Event: Disable nat-to-bv-list-loop-clock.

Theorem: nat-list-piton-means-get nat-list-piton (state, size) → ((car (get (p, state))

= if p < length (state) then 'nat

else 0 endif) ∧ (listp (get (p, state)) = (p < length (state))) ∧ (cadr (get (p, state)) ∈ N) ∧ ((cadr (get (p, state)) < exp (2, size)) = t) ∧ (cddr (get (p, state))

= if p < length (state) then nil else 0 endif))

Theorem: nat-list-piton-means-get-cdr (nat-list-piton (state, size) ∧ listp (state)) → ((car (get (p, cdr (state)))

= if p < length (cdr (state)) then 'nat

else 0 endif) ∧ (listp (get (p, cdr (state))) = (p < length (cdr (state)))) ∧ (cadr (get (p, cdr (state))) ∈ N) ∧ ((cadr (get (p, cdr (state))) < exp (2, size)) = t) ∧ (cddr (get (p, cdr (state)))

= if p < length (cdr (state)) then nil else 0 endif))

Event: Disable nat-list-piton-means.

Theorem: length-put-better length (put (v, n, a)) = if n < length (a) then length (a)

else 1 + n endif

Theorem: cons-car-x-put-append-make-list-from-hack cons (car (put (v, x, b)), append (make-list-from (x, cdr (put (v, x, b))), y)) = append (make-list-from (x, b), cons (v, y))

Theorem: array-pitonp-put (array-pitonp (a, l) ∧ (fix (l) = fix (length))) → (array-pitonp (put (v, n, a), length) = (n < length (a)))

Theorem: array-pitonp-means-properp (array-pitonp (x, s) → properp (x)) ∧ (array-pitonp (cdr (x), s) → properp (x))

Theorem: put-length-cdr-general (properp (x) ∧ (length (x) = length (y))) → (put (val, length (cdr (y)), x) = append (all-but-last (x), list (val)))

Theorem: nthcdr-x-cdr-put-x properp (a) → (nthcdr (x, cdr (put (val, x, a)))

= if x < length (a) then nthcdr (x, cdr (a)) else nil endif)

Theorem: equal-append-a-append-a (append (a, b) = append (a, c)) = (b = c)

;The correctness lemma of nat-to-bv-list could be more general -
;the proof assumes the data areas are distinct, though the program
;works when they're not.  I did it this way because I had assumed
;I'd need distinct arrays in NIM, and designed the proof accordingly.
;This is a weakness I should correct in this proof as it will lead
;to sloppy use of memory in the program, but it takes so long
;to do these proofs I'll wait.

Theorem: correctness-of-nat-to-bv-list-general (listp (ctrl-stk) ∧ at-least-morep (p-ctrl-stk-size (ctrl-stk), 13, max-ctrl-stk-size) ∧ at-least-morep (length (temp-stk), 3, max-temp-stk-size) ∧ (definition ('nat-to-bv-list, prog-segment)

= nat-to-bv-list-program)

∧ (definition ('nat-to-bv, prog-segment) = nat-to-bv-program) ∧ (definition ('push-1-vector, prog-segment)

= push-1-vector-program (word-size)) ∧ (length = length (array (nats, data-segment))) ∧ array-pitonp (array (bvs, data-segment), length) ∧ nat-list-piton (array (nats, data-segment), word-size) ∧ definedp (nats, data-segment) ∧ definedp (bvs, data-segment) ∧ (word-size ≄ 0) ∧ (i ∈ N) ∧ (i < length) ∧ (length < exp (2, word-size)) ∧ (nats ≠ bvs) ∧ (natlist = array (nats, data-segment)))

→ (p (p-state ('(pc (nat-to-bv-list . 0)),

cons (list (list (cons ('nat-list,

list ('addr, cons (nats, i))), cons ('bv-list, list ('addr, cons (bvs, i))), cons ('length, list ('nat, length)), cons ('i, list ('nat, i))),

ret-pc), ctrl-stk),

temp-stk, prog-segment, data-segment, max-ctrl-stk-size, max-temp-stk-size, word-size,

             'run),

nat-to-bv-list-loop-clock (i, natlist)) = p-state (ret-pc,

ctrl-stk, temp-stk, prog-segment, put-assoc (append (make-list-from (i,

array (bvs,

data-segment)),

tag-array ('bitv,

nat-to-bv-list (untag-array (nthcdr (i,

array (nats,

data-segment))),

word-size))),

bvs,

data-segment), max-ctrl-stk-size, max-temp-stk-size, word-size,

           'run))

Definition: nat-to-bv-list-clock (natlist) = clock-plus (1, nat-to-bv-list-loop-clock (0, natlist))

Definition: nat-to-bv-list-input-conditionp (p0 ) = (listp (p-ctrl-stk (p0 ))

∧ at-least-morep (p-ctrl-stk-size (p-ctrl-stk (p0 )),

                13,

p-max-ctrl-stk-size (p0 ))

∧ at-least-morep (length (p-temp-stk (p0 )),

                0,

p-max-temp-stk-size (p0 ))

∧ (definition ('nat-to-bv-list, p-prog-segment (p0 ))

= nat-to-bv-list-program) ∧ (definition ('nat-to-bv, p-prog-segment (p0 ))

= nat-to-bv-program) ∧ (definition ('push-1-vector, p-prog-segment (p0 ))

= push-1-vector-program (p-word-size (p0 ))) ∧ (cadr (top (p-temp-stk (p0 )))

= length (array (caadr (top (cddr (p-temp-stk (p0 )))), p-data-segment (p0 ))))

∧ array-pitonp (array (caadr (top (cdr (p-temp-stk (p0 )))),

p-data-segment (p0 )), cadr (top (p-temp-stk (p0 ))))

∧ nat-list-piton (array (caadr (top (cddr (p-temp-stk (p0 )))),

p-data-segment (p0 )), p-word-size (p0 ))

∧ definedp (caadr (top (cddr (p-temp-stk (p0 )))), p-data-segment (p0 )) ∧ definedp (caadr (top (cdr (p-temp-stk (p0 )))), p-data-segment (p0 )) ∧ (p-current-instruction (p0 ) = '(call nat-to-bv-list)) ∧ (p-word-size (p0 ) ≄ 0) ∧ (caadr (top (cddr (p-temp-stk (p0 ))))

≠ caadr (top (cdr (p-temp-stk (p0 ))))) ∧ (car (top (p-temp-stk (p0 ))) = 'nat) ∧ (cadr (top (p-temp-stk (p0 ))) ≄ 0) ∧ (cadr (top (p-temp-stk (p0 ))) < exp (2, p-word-size (p0 ))) ∧ (cddr (top (p-temp-stk (p0 ))) = nil) ∧ (car (top (cdr (p-temp-stk (p0 )))) = 'addr)

∧ listp (cadr (top (cdr (p-temp-stk (p0 ))))) ∧ (cdadr (top (cdr (p-temp-stk (p0 )))) = 0) ∧ (cddr (top (cdr (p-temp-stk (p0 )))) = nil) ∧ (car (top (cddr (p-temp-stk (p0 )))) = 'addr) ∧ listp (cadr (top (cddr (p-temp-stk (p0 ))))) ∧ (cdadr (top (cddr (p-temp-stk (p0 )))) = 0) ∧ (cddr (top (cddr (p-temp-stk (p0 )))) = nil))

Theorem: correctness-of-nat-to-bv-list ((p0 = p-state (pc,

ctrl-stk, cons (l, cons (b, cons (n, temp-stk))), prog-segment, data-segment, max-ctrl-stk-size, max-temp-stk-size, word-size,

'run))

∧ nat-to-bv-list-input-conditionp (p0 ) ∧ (natlist = array (caadr (n), data-segment))) → (p (p-state (pc,

ctrl-stk, cons (l, cons (b, cons (n, temp-stk))), prog-segment, data-segment, max-ctrl-stk-size, max-temp-stk-size, word-size,

'run),

nat-to-bv-list-clock (natlist)) = p-state (add1-addr (pc),

ctrl-stk,

temp-stk,

prog-segment,

put-assoc (tag-array ('bitv,

nat-to-bv-list (untag-array (array (caadr (n),

data-segment)),

word-size)),

caadr (b), data-segment),

max-ctrl-stk-size,

max-temp-stk-size,

word-size,

  'run))

Event: Disable nat-to-bv-list-program.

Event: Disable match-and-xor-program.

Event: Disable highest-bit-program.

Event: Disable number-with-at-least-program.

Event: Disable bv-to-nat-program.

Event: Disable nat-to-bv-program.

Event: Disable push-1-vector-program.

Event: Disable xor-bvs-program.

;; bv-to-nat-list

Definition: bv-to-nat-list-program

= '(bv-to-nat-list
(bv-list nat-list length)
((i (nat 0)))
(dl loop nil (push-local bv-list))
(fetch)
(call bv-to-nat)
(push-local nat-list)
(deposit)
(push-local i)
(add1-nat)
(set-local i)
(push-local length)
(eq)
(test-bool-and-jump t done)
(push-local nat-list)
(push-constant (nat 1))
(add-addr)
(pop-local nat-list)
(push-local bv-list)

(push-constant (nat 1))
(add-addr)
(pop-local bv-list)
(jump loop)
(dl done nil (ret)))

Definition: example-bv-to-nat-list-p-state

= p-state ('(pc (main . 0)),
'((nil (pc (main . 0)))),

nil,

list ('(main nil nil
      (push-constant (addr (arr . 0)))
      (push-constant (addr (arr2 . 0)))
      (push-constant (nat 6))
      (call bv-to-nat-list)
      (ret)),

bv-to-nat-list-program, bv-to-nat-program, push-1-vector-program (8)),

'((arr
   (bitv (0 1 0 1 0 1 0 0))
   (bitv (1 1 1 1 1 1 1 1))
   (bitv (0 1 0 1 0 1 0 0))
   (bitv (0 1 0 1 0 1 0 0))
   (bitv (0 0 0 0 0 0 0 0))
   (bitv (0 1 0 1 0 1 0 0)))
  (arr2 nil nil nil nil nil nil)),
100,
80,
8,
'run)

Definition: bv-to-nat-list-input-conditionp (p0 ) = (listp (p-ctrl-stk (p0 ))

∧ at-least-morep (p-ctrl-stk-size (p-ctrl-stk (p0 )),

          13,

p-max-ctrl-stk-size (p0 ))

∧ at-least-morep (length (p-temp-stk (p0 )),

          0,

p-max-temp-stk-size (p0 ))

∧ (definition ('bv-to-nat-list, p-prog-segment (p0 )) = bv-to-nat-list-program)

∧ (definition ('bv-to-nat, p-prog-segment (p0 ))

= bv-to-nat-program) ∧ (definition ('push-1-vector, p-prog-segment (p0 ))

= push-1-vector-program (p-word-size (p0 ))) ∧ (cadr (top (p-temp-stk (p0 )))

= length (array (caadr (top (cddr (p-temp-stk (p0 )))), p-data-segment (p0 ))))

∧ array-pitonp (array (caadr (top (cdr (p-temp-stk (p0 )))),

p-data-segment (p0 )), cadr (top (p-temp-stk (p0 ))))

∧ bit-vectors-piton (array (caadr (top (cddr (p-temp-stk (p0 )))),

p-data-segment (p0 )), p-word-size (p0 ))

∧ definedp (caadr (top (cddr (p-temp-stk (p0 )))), p-data-segment (p0 )) ∧ definedp (caadr (top (cdr (p-temp-stk (p0 )))), p-data-segment (p0 )) ∧ (p-current-instruction (p0 ) = '(call bv-to-nat-list)) ∧ (p-word-size (p0 ) ≄ 0) ∧ (caadr (top (cddr (p-temp-stk (p0 ))))

≠ caadr (top (cdr (p-temp-stk (p0 ))))) ∧ (car (top (p-temp-stk (p0 ))) = 'nat) ∧ (cadr (top (p-temp-stk (p0 ))) ≄ 0) ∧ (cadr (top (p-temp-stk (p0 ))) < exp (2, p-word-size (p0 ))) ∧ (cddr (top (p-temp-stk (p0 ))) = nil) ∧ (car (top (cdr (p-temp-stk (p0 )))) = 'addr) ∧ listp (cadr (top (cdr (p-temp-stk (p0 ))))) ∧ (cdadr (top (cdr (p-temp-stk (p0 )))) = 0) ∧ (cddr (top (cdr (p-temp-stk (p0 )))) = nil) ∧ (car (top (cddr (p-temp-stk (p0 )))) = 'addr) ∧ listp (cadr (top (cddr (p-temp-stk (p0 ))))) ∧ (cdadr (top (cddr (p-temp-stk (p0 )))) = 0) ∧ (cddr (top (cddr (p-temp-stk (p0 )))) = nil))

Definition: bv-to-nat-list-loop-clock (wordsize, i, bvs) = if i < length (bvs)

then clock-plus ('2,

clock-plus (bv-to-nat-clock (wordsize, untag (get (i, bvs))), if i < length (cdr (bvs)) then clock-plus ('17,

bv-to-nat-list-loop-clock (wordsize, 1 + i, bvs))

else '9 endif))

else '0 endif Definition: bv-to-nat-list (bv-list) = if listp (bv-list)

then cons (bv-to-nat (car (bv-list)), bv-to-nat-list (cdr (bv-list))) else nil endif

Definition: bv-to-nat-list-loop-induct (i, bvs, nats-name, data-segment) = if (i < length (bvs)) ∧ (i < length (cdr (bvs)))

then bv-to-nat-list-loop-induct (1 + i, bvs, nats-name, put-assoc (append (make-list-from (i,

cdr (assoc (nats-name,

data-segment))),

cons (list ('nat,

bv-to-nat (untag (get (i,

bvs)))),

nthcdr (1 + i,

cdr (assoc (nats-name,

data-segment))))),

nats-name, data-segment))

else t endif

Event: Disable bv-to-nat-clock.

Theorem: correctness-of-bv-to-nat-list-general (listp (ctrl-stk) ∧ at-least-morep (p-ctrl-stk-size (ctrl-stk), 13, max-ctrl-stk-size) ∧ at-least-morep (length (temp-stk), 3, max-temp-stk-size) ∧ (definition ('bv-to-nat-list, prog-segment)

= bv-to-nat-list-program) ∧ (definition ('bv-to-nat, prog-segment) = bv-to-nat-program) ∧ (definition ('push-1-vector, prog-segment)

= push-1-vector-program (word-size)) ∧ (length = length (array (bvs, data-segment))) ∧ bit-vectors-piton (array (bvs, data-segment), word-size) ∧ array-pitonp (array (nats, data-segment), length) ∧ definedp (nats, data-segment) ∧ definedp (bvs, data-segment) ∧ (word-size ≄ 0) ∧ (i ∈ N) ∧ (i < length)

∧ (length < exp (2, word-size)) ∧ (nats ≠ bvs) ∧ (bvlist = array (bvs, data-segment)))

→ (p (p-state ('(pc (bv-to-nat-list . 0)),

cons (list (list (cons ('bv-list, list ('addr, cons (bvs, i))),

            cons ('nat-list,

list ('addr, cons (nats, i))), cons ('length, list ('nat, length)), cons ('i, list ('nat, i))),

ret-pc), ctrl-stk),

temp-stk, prog-segment, data-segment, max-ctrl-stk-size, max-temp-stk-size, word-size,

'run),

bv-to-nat-list-loop-clock (word-size, i, bvlist)) = p-state (ret-pc,

ctrl-stk, temp-stk, prog-segment, put-assoc (append (make-list-from (i,

array (nats,

data-segment)),

tag-array ('nat,

bv-to-nat-list (untag-array (nthcdr (i,

array (bvs,

data-segment)))))),

nats,

data-segment),

max-ctrl-stk-size, max-temp-stk-size, word-size,

 'run))

Definition: bv-to-nat-list-clock (word-size, natlist) = clock-plus (1, bv-to-nat-list-loop-clock (word-size, 0, natlist))

Event: Disable bv-to-nat-list-loop-clock.

Event: Disable bv-to-nat-list-program.

Theorem: correctness-of-bv-to-nat-list ((p0 = p-state (pc,

ctrl-stk, cons (l, cons (n, cons (b, temp-stk))), prog-segment, data-segment, max-ctrl-stk-size, max-temp-stk-size, word-size,

'run))

∧ bv-to-nat-list-input-conditionp (p0 ) ∧ (bvlist = array (caadr (b), data-segment))) → (p (p-state (pc,

ctrl-stk, cons (l, cons (n, cons (b, temp-stk))), prog-segment, data-segment, max-ctrl-stk-size, max-temp-stk-size, word-size,

'run),

bv-to-nat-list-clock (word-size, bvlist)) = p-state (add1-addr (pc),

ctrl-stk,

temp-stk,

prog-segment,

put-assoc (tag-array ('nat,

bv-to-nat-list (untag-array (array (caadr (b),

data-segment)))),

caadr (n), data-segment),

max-ctrl-stk-size,

max-temp-stk-size,

word-size,

  'run))
;; max-nat

Definition: max-nat-program

= '(max-nat
(nat-list length)

((i (nat 0)) (j (nat 0)))
(push-constant (nat 0))
(dl loop nil (set-local j))
(push-local j)
(push-local nat-list)
(fetch)
(set-local j)
(lt-nat)
(test-bool-and-jump f lab)
(pop)
(push-local j)
(dl lab nil (push-local i))
(add1-nat)
(set-local i)
(push-local length)
(eq)
(test-bool-and-jump t done)
(push-local nat-list)
(push-constant (nat 1))
(add-addr)
(pop-local nat-list)
(jump loop)
(dl done nil (ret)))

Definition: example-max-nat-p-state

= p-state ('(pc (main . 0)),
     '((nil (pc (main . 0)))),

nil,

     list ('(main nil nil
          (push-constant (addr (arr . 0)))
          (push-constant (nat 6))
          (call max-nat)
          (ret)),

max-nat-program),

     '((arr
        (nat 3)
        (nat 10)
        (nat 3)
        (nat 6)
        (nat 9)
        (nat 0))
       (arr2 nil nil nil nil nil nil)),
     100,

          8,
          'run)

Definition: max-list-helper (val, x) = if listp (x)

then if val < car (x) then max-list-helper (car (x), cdr (x))

else max-list-helper (val, cdr (x)) endif else fix (val) endif

Definition: max-list (x) = if listp (x)

then if max-list (cdr (x)) < car (x) then car (x)

else max-list (cdr (x)) endif else 0 endif

Theorem: max-list-helper-max-list max-list-helper (val, x) = if max-list (x) < val then val

else max-list (x) endif

Theorem: max-list-helper-max-list-0 max-list-helper (0, x) = max-list (x)

Event: Disable max-list-helper-max-list.

Definition: max-nat-loop-clock (val, i, nats) = if i < length (nats)

then if val < untag (get (i, nats))

then if i < length (cdr (nats)) then clock-plus (20,

max-nat-loop-clock (untag (get (i, nats)), 1 + i, nats))

else 16 endif elseif i < length (cdr (nats)) then clock-plus (18, max-nat-loop-clock (val, 1 + i, nats)) else 14 endif

else 0 endif

Definition: max-nat-loop-induct (i, j , x, natlist, length)

= if i < length

then max-nat-loop-induct (1 + i, get (i, natlist), if untag (get (i, natlist)) < untag (x) then list ('nat, untag (x)) else list ('nat, untag (get (i, natlist))) endif, natlist, length)

else t endif

Theorem: list-nat-from-assoc-nat-list-piton-hack nat-list-piton (nl, s) → (((z < length (cdr (nl)))

→ (list ('nat, cadr (get (z, cdr (nl)))) = get (z, cdr (nl)))) ∧ (listp (nl)

→ ((list ('nat, cadr (last (nl))) = last (nl)) ∧ (list ('nat, cadr (car (nl))) = car (nl)))))

Theorem: correctness-of-max-nat-general (listp (ctrl-stk) ∧ at-least-morep (p-ctrl-stk-size (ctrl-stk), 4, max-ctrl-stk-size) ∧ at-least-morep (length (temp-stk), 4, max-temp-stk-size) ∧ (definition ('max-nat, prog-segment) = max-nat-program) ∧ (length = length (array (nats, data-segment))) ∧ nat-list-piton (array (nats, data-segment), word-size) ∧ definedp (nats, data-segment) ∧ (word-size ≄ 0) ∧ (i ∈ N) ∧ (i < length) ∧ (untag (x) ∈ N) ∧ (untag (x) < exp (2, word-size)) ∧ (car (x) = 'nat) ∧ (cddr (x) = nil) ∧ (length < exp (2, word-size)) ∧ (natlist = array (nats, data-segment)))

→ (p (p-state ('(pc (max-nat . 1)),

cons (list (list (cons ('nat-list,

list ('addr, cons (nats, i))), cons ('length, list ('nat, length)), cons ('i, list ('nat, i)), cons ('j, j )),

ret-pc), ctrl-stk), cons (x, temp-stk), prog-segment, data-segment, max-ctrl-stk-size, max-temp-stk-size, word-size,

'run),

max-nat-loop-clock (untag (x), i, array (nats, data-segment))) = p-state (ret-pc,

ctrl-stk, cons (list ('nat,

max-list-helper (untag (x),

untag-array (nthcdr (i,

array (nats,

data-segment))))),

temp-stk), prog-segment, data-segment, max-ctrl-stk-size, max-temp-stk-size, word-size,

'run))

Definition: max-nat-clock (natlist) = clock-plus (2, max-nat-loop-clock (0, 0, natlist))

Definition: max-nat-input-conditionp (p0 ) = (listp (p-ctrl-stk (p0 ))

∧ at-least-morep (p-ctrl-stk-size (p-ctrl-stk (p0 )),

     6,

p-max-ctrl-stk-size (p0 ))

∧ at-least-morep (length (p-temp-stk (p0 )),

     2,

p-max-temp-stk-size (p0 ))

∧ (definition ('max-nat, p-prog-segment (p0 ))

= max-nat-program) ∧ (untag (top (p-temp-stk (p0 )))

= length (array (car (untag (top (cdr (p-temp-stk (p0 ))))),

p-data-segment (p0 ))))

∧ nat-list-piton (array (car (untag (top (cdr (p-temp-stk (p0 ))))),

p-data-segment (p0 )), p-word-size (p0 ))

∧ definedp (car (untag (top (cdr (p-temp-stk (p0 ))))), p-data-segment (p0 ))

∧ (p-word-size (p0 ) ≄ 0) ∧ (untag (top (p-temp-stk (p0 ))) ≄ 0) ∧ (car (top (p-temp-stk (p0 ))) = 'nat) ∧ (car (top (cdr (p-temp-stk (p0 )))) = 'addr) ∧ listp (untag (top (cdr (p-temp-stk (p0 ))))) ∧ (untag (top (p-temp-stk (p0 ))) < exp (2, p-word-size (p0 ))) ∧ (cddr (top (cdr (p-temp-stk (p0 )))) = nil) ∧ (cddr (top (p-temp-stk (p0 ))) = nil) ∧ (cdr (untag (top (cdr (p-temp-stk (p0 ))))) = 0))

Theorem: correctness-of-max-nat ((p0 = p-state (pc,

ctrl-stk,

cons (n, cons (s, temp-stk)), prog-segment, data-segment, max-ctrl-stk-size, max-temp-stk-size, word-size,

          'run))

∧ (p-current-instruction (p0 ) = '(call max-nat)) ∧ max-nat-input-conditionp (p0 ) ∧ (natlist = array (car (untag (s)), data-segment))) → (p (p-state (pc,

ctrl-stk,

cons (n, cons (s, temp-stk)), prog-segment, data-segment, max-ctrl-stk-size, max-temp-stk-size, word-size,

          'run),

max-nat-clock (natlist)) = p-state (add1-addr (pc),

ctrl-stk,

cons (list ('nat, max-list (untag-array (natlist))),

temp-stk), prog-segment, data-segment, max-ctrl-stk-size, max-temp-stk-size, word-size,

           'run))

Event: Disable max-nat-program.

;; replace-value
;; replace the first occurrence of oldval by newval in list
;; of naturals (assumes oldval occurs in list)

Definition: replace-value-program

= '(replace-value
(list oldval newval)
nil
(dl loop nil (push-local list))
(fetch)
(push-local oldval)
(eq)
(test-bool-and-jump t done)
(push-local list)
(push-constant (nat 1))
(add-addr)
(pop-local list)
(jump loop)
(dl done nil (push-local newval))
(push-local list)
(deposit)
(ret))

Definition: example-replace-value-p-state

= p-state ('(pc (main . 0)),
     '((nil (pc (main . 0)))),

nil,

     list ('(main nil nil
          (push-constant (addr (arr . 0)))
          (push-constant (nat 3))
          (push-constant (nat 4))
          (call replace-value)
          (ret)),

replace-value-program),

     '((arr
        (nat 9)
        (nat 10)
        (nat 3)
        (nat 6)
        (nat 9)

             (nat 0))),
          100,
          80,
          8,
          'run)

Definition: replace-value-loop-clock (i, list, oldvalue) = if i < length (list)

then if get (i, list) = oldvalue then 9

else clock-plus (10,

replace-value-loop-clock (1 + i, list, oldvalue)) endif

else 0 endif

Definition: replace-value-loop-induct (i, list, list-addr) = if i < length (list)

then replace-value-loop-induct (1 + i, list, add1-addr (list-addr)) else t endif

Definition: replace-value (list, oldvalue, newvalue) = if listp (list)

then if car (list) = oldvalue then cons (newvalue, cdr (list))

else cons (car (list),

replace-value (cdr (list), oldvalue, newvalue)) endif

else nil endif

Theorem: member-nthcdr-means (x ∈ nthcdr (i, y)) → (x ∈ y)

Theorem: member-of-natlist-means (nat-list-piton (y, s) ∧ (x ∈ y)) → (listp (x)

∧ (car (x) = 'nat) ∧ (cadr (x) ∈ N) ∧ (cadr (x) < exp (2, s)) ∧ (cddr (x) = nil))

Theorem: replace-value-nthcdr-open ((get (x, a) ≠ old) ∧ (x < length (a))) → (replace-value (nthcdr (x, a), old, new)

= cons (get (x, a), replace-value (nthcdr (x, cdr (a)), old, new)))

Theorem: list-nat-cadr-get-hack (nat-list-piton (y, s) ∧ (x < length (y))) → (list ('nat, cadr (get (x, y))) = get (x, y))

Theorem: member-nthcdr-simplify ((i < length (x)) ∧ (a ∉ nthcdr (i, cdr (x)))) → ((a ∈ nthcdr (i, x)) = (a = get (i, x)))

Theorem: append-make-list-from-cons-cdr (i < length (y)) → (append (make-list-from (i, y), cons (v, cdr (nthcdr (i, y)))) = put (v, i, y))

Theorem: correctness-of-replace-value-general (listp (ctrl-stk) ∧ at-least-morep (length (temp-stk), 2, max-temp-stk-size) ∧ (definition ('replace-value, prog-segment)

= replace-value-program) ∧ nat-list-piton (array (list, data-segment), word-size) ∧ definedp (list, data-segment) ∧ (word-size ≄ 0) ∧ (i ∈ N) ∧ (vallist = array (list, data-segment)) ∧ (car (list-addr) = 'addr) ∧ (cddr (list-addr) = nil) ∧ listp (untag (list-addr)) ∧ (car (untag (list-addr)) = list) ∧ (cdr (untag (list-addr)) = i) ∧ (car (newvalue) = 'nat) ∧ (cddr (newvalue) = nil) ∧ (car (oldvalue) = 'nat) ∧ (cddr (oldvalue) = nil) ∧ (cadr (oldvalue) ∈ N) ∧ (cadr (oldvalue) < exp (2, word-size)) ∧ (untag (newvalue) ∈ N) ∧ (untag (newvalue) < exp (2, word-size)) ∧ (oldvalue ∈ nthcdr (i, vallist)))

→ (p (p-state ('(pc (replace-value . 0)),

cons (list (list (cons ('list, list-addr), cons ('oldval, oldvalue), cons ('newval, newvalue)),

ret-pc), ctrl-stk),

temp-stk, prog-segment, data-segment, max-ctrl-stk-size, max-temp-stk-size, word-size,

'run),

replace-value-loop-clock (i, vallist, oldvalue)) = p-state (ret-pc,

ctrl-stk, temp-stk, prog-segment, put-assoc (append (make-list-from (i,

array (list,

data-segment)),

replace-value (nthcdr (i,

array (list,

data-segment)),

oldvalue, newvalue)),

list,

data-segment),

max-ctrl-stk-size, max-temp-stk-size, word-size,

'run))

Definition: replace-value-clock (list, ov) = clock-plus (1, replace-value-loop-clock (0, list, ov))

Definition: replace-value-input-conditionp (p0 ) = (listp (p-ctrl-stk (p0 ))

∧ at-least-morep (length (p-temp-stk (p0 )),

     0,

p-max-temp-stk-size (p0 ))

∧ at-least-morep (p-ctrl-stk-size (p-ctrl-stk (p0 )),

     5,

p-max-ctrl-stk-size (p0 ))

∧ (definition ('replace-value, p-prog-segment (p0 ))

= replace-value-program) ∧ nat-list-piton (array (car (untag (top (cddr (p-temp-stk (p0 ))))),

p-data-segment (p0 )), p-word-size (p0 ))

∧ definedp (car (untag (top (cddr (p-temp-stk (p0 ))))), p-data-segment (p0 ))

∧ (p-word-size (p0 ) ≄ 0) ∧ (car (top (cddr (p-temp-stk (p0 )))) = 'addr) ∧ (cddr (top (cddr (p-temp-stk (p0 )))) = nil) ∧ listp (untag (top (cddr (p-temp-stk (p0 ))))) ∧ (cdr (untag (top (cddr (p-temp-stk (p0 ))))) = 0) ∧ (car (top (p-temp-stk (p0 ))) = 'nat) ∧ (cddr (top (p-temp-stk (p0 ))) = nil) ∧ (untag (top (p-temp-stk (p0 ))) ∈ N) ∧ (untag (top (p-temp-stk (p0 ))) < exp (2, p-word-size (p0 ))) ∧ (top (cdr (p-temp-stk (p0 )))

∈ array (car (untag (top (cddr (p-temp-stk (p0 ))))), p-data-segment (p0 ))))

Theorem: correctness-of-replace-value ((p0 = p-state (pc,

ctrl-stk,

cons (nv, cons (ov, cons (nats, temp-stk))), prog-segment, data-segment, max-ctrl-stk-size, max-temp-stk-size, word-size,

          'run))

∧ (p-current-instruction (p0 ) = '(call replace-value)) ∧ replace-value-input-conditionp (p0 ) ∧ (natlist = array (car (untag (nats)), data-segment)) ∧ (ov = ov2 )) → (p (p-state (pc,

ctrl-stk,

cons (nv, cons (ov, cons (nats, temp-stk))), prog-segment, data-segment, max-ctrl-stk-size, max-temp-stk-size, word-size,

          'run),

replace-value-clock (natlist, ov2 )) = p-state (add1-addr (pc),

ctrl-stk, temp-stk, prog-segment, put-assoc (replace-value (natlist, ov, nv),

caadr (nats), data-segment), max-ctrl-stk-size, max-temp-stk-size, word-size,

          'run))

Event: Disable replace-value-program.

;; smart-move

Definition: smart-move-program

= '(smart-move
(state numpiles work-area)
((i (nat 0)))
(push-local state)
(push-local numpiles)
(push-constant (nat 2))
(call number-with-at-least)
(push-constant (nat 2))
(lt-nat)
(test-bool-and-jump t lab)
(push-local state)
(push-local work-area)
(push-local numpiles)
(call nat-to-bv-list)
(push-local work-area)
(push-local numpiles)
(push-local work-area)
(push-local numpiles)
(call xor-bvs)
(set-local i)
(call highest-bit)
(push-local i)
(call match-and-xor)
(push-local work-area)
(push-local state)
(push-local numpiles)
(call bv-to-nat-list)
(ret)
(dl lab nil (push-local state))
(push-local state)
(push-local numpiles)
(call max-nat)

(push-local state)
(push-local numpiles)
(push-constant (nat 1))
(call number-with-at-least)
(div2-nat)
(pop-local i)
(pop)
(push-local i)
(call replace-value)
(ret))

Definition: example-smart-move-p-state

= p-state ('(pc (main . 0)),
'((nil (pc (main . 0)))),

nil,

list ('(main nil nil
(push-constant (addr (arr . 0)))
(push-constant (nat 4))
(push-constant (addr (arr5 . 0)))
(call smart-move)
(push-constant (addr (arr2 . 0)))
(push-constant (nat 4))
(push-constant (addr (arr5 . 0)))
(call smart-move)
(push-constant (addr (arr3 . 0)))
(push-constant (nat 4))
(push-constant (addr (arr5 . 0)))
(call smart-move)
(push-constant (addr (arr4 . 0)))
(push-constant (nat 4))
(push-constant (addr (arr5 . 0)))
(call smart-move)
(ret)),

replace-value-program, max-nat-program, bv-to-nat-list-program, nat-to-bv-list-program, match-and-xor-program, highest-bit-program, number-with-at-least-program, bv-to-nat-program, nat-to-bv-program, push-1-vector-program (8), xor-bvs-program, smart-move-program),

'((arr (nat 3) (nat 4) (nat 2) (nat 1))
  (arr2 (nat 1) (nat 1) (nat 1) (nat 9))
  (arr3 (nat 1) (nat 1) (nat 0) (nat 9))
  (arr4 (nat 0) (nat 0) (nat 0) (nat 0))
  (arr5 (nat 3) (nat 4) (nat 2) (nat 1))),
100,
80,
8,
'run)

Definition: smart-move (state, wordsize) = if number-with-at-least (state, 2) < 2

then replace-value (state, max-list (state), number-with-at-least (state, 1) mod 2)

else bv-to-nat-list (match-and-xor (nat-to-bv-list (state, wordsize),

highest-bit (xor-bvs (nat-to-bv-list (state,

wordsize))),

xor-bvs (nat-to-bv-list (state, wordsize)))) endif

(defn smart-move-clock (state wordsize)
(clock-plus 4
(clock-plus (number-with-at-least-clock 2 (tag-array 'nat state))
(clock-plus 3
(if (lessp (number-with-at-least state 2) 2)
(clock-plus 3
(clock-plus (max-nat-clock (tag-array 'nat state))
(clock-plus 3
(clock-plus (number-with-at-least-clock
1 (tag-array 'nat state))
(clock-plus 4
(clock-plus (replace-value-clock (tag-array 'nat state)
(list 'nat (max-list state)))
1))))))
(clock-plus 3
(clock-plus (nat-to-bv-list-clock (tag-array 'nat state))
(clock-plus 4
(clock-plus (xor-bvs-clock (length state))

   (clock-plus 1
    (clock-plus (highest-bit-clock
 (xor-bvs (nat-to-bv-list state wordsize)))
     (clock-plus 1
      (clock-plus (match-and-xor-clock
   (nat-to-bv-list state wordsize)
   (highest-bit
    (xor-bvs (nat-to-bv-list state wordsize))))
       (clock-plus 3
(clock-plus (bv-to-nat-list-clock
     wordsize
     (tag-array
      'bitv
      (match-and-xor
       (nat-to-bv-list state wordsize)
       (highest-bit
(xor-bvs (nat-to-bv-list state wordsize)))
       (xor-bvs (nat-to-bv-list state wordsize)))))
    1)))))))))))))))

Event: Disable replace-value-clock.

Event: Disable max-nat-clock.

Event: Disable bv-to-nat-list-clock.

Event: Disable nat-to-bv-list-clock.

Event: Disable match-and-xor-clock.

Event: Disable highest-bit-clock.

Event: Disable number-with-at-least-clock.

Event: Disable bv-to-nat-clock.

Event: Disable nat-to-bv-clock.

Event: Disable xor-bvs-clock.

Event: Disable replace-value-program. Event: Disable max-nat-program. Event: Disable bv-to-nat-list-program. Event: Disable nat-to-bv-list-program. Event: Disable match-and-xor-program. Event: Disable highest-bit-program. Event: Disable number-with-at-least-program. Event: Disable bv-to-nat-program. Event: Disable nat-to-bv-program. Event: Disable push-1-vector-program. Event: Disable *1*xor-bvs-program. Event: Disable *1*replace-value-program. Event: Disable *1*max-nat-program. Event: Disable *1*bv-to-nat-list-program. Event: Disable *1*nat-to-bv-list-program. Event: Disable *1*match-and-xor-program. Event: Disable *1*highest-bit-program. Event: Disable *1*number-with-at-least-program.

Event: Disable *1*bv-to-nat-program.

Event: Disable *1*nat-to-bv-program.

Event: Disable *1*push-1-vector-program.

Event: Disable *1*xor-bvs-program.

Definition: nat-listp (list, size) = if listp (list)

then (car (list) ∈ N) ∧ (car (list) < exp (2, size)) ∧ nat-listp (cdr (list), size)

else list = nil endif

Theorem: bv-to-nat-list-nat-to-bv-list nat-listp (x, size) → (bv-to-nat-list (nat-to-bv-list (x, size)) = x)

Theorem: bit-vectorsp-nat-to-bv-list bit-vectorsp (nat-to-bv-list (x, size), size)

Theorem: nat-to-bv-list-bv-to-nat-list bit-vectorsp (x, size) → (nat-to-bv-list (bv-to-nat-list (x), size) = x)

Theorem: bit-vectorsp-match-and-xor bit-vectorsp (x, size) → bit-vectorsp (match-and-xor (x, y, z), size)

Theorem: equal-sub1-add1 (((x − 1) = (1 + y)) = (x = (1 + (1 + y)))) ∧ (((x − 1) = 0) = ((x ≃ 0) ∨ (x = 1)))

;; part of more recent naturals library that's missing from Piton library

Theorem: equal-times-x-x (((x ∗ y) = x) = (((x ∈ N) ∧ (y = 1)) ∨ (x = 0))) ∧ (((y ∗ x) = x) = (((x ∈ N) ∧ (y = 1)) ∨ (x = 0)))

Theorem: equal-exp-x-y-x (exp (x, y) = x) = ((x = 1) ∨ ((x = 0) ∧ (y ≄ 0)) ∨ ((x ∈ N) ∧ (y = 1)))

Theorem: lessp-number-with-at-least length (x) ≮ number-with-at-least (x, min)

Theorem: bit-vectors-piton-tag-array bit-vectorsp (x, size) → bit-vectors-piton (tag-array ('bitv, x), size)

Theorem: tag-array-untag-array-of-nat-list-piton nat-list-piton (x, size) → (tag-array ('nat, untag-array (x)) = x)

Theorem: tag-array-untag-array-of-bit-vectors-piton bit-vectors-piton (x, size) → (tag-array ('bitv, untag-array (x)) = x)

Theorem: bit-vectorp-xor-bvs-nat-to-bv-list bit-vectorp (xor-bvs (nat-to-bv-list (x, s)), s) = (listp (x) ∨ (s ≃ 0))

Theorem: listp-cdr-assoc-hack-from-free ((length (cdr (assoc (x, y))) = free) ∧ (free ≄ 0)) → listp (cdr (assoc (x, y)))

Theorem: bit-vectorp-highest-bit bit-vectorp (x, s) → bit-vectorp (highest-bit (x), s)

Theorem: length-match-and-xor length (match-and-xor (list, m, v)) = length (list)

Theorem: array-pitonp-from-nat-list-piton nat-list-piton (x, s) → (array-pitonp (x, length) = (fix (length) = length (x)))

Theorem: untag-array-tag-array-of-bit-vectorsp bit-vectorsp (x, size) → (untag-array (tag-array (l, x)) = x)

Theorem: untag-array-tag-array-of-nat-to-bv-list untag-array (tag-array (l, nat-to-bv-list (x, size))) = nat-to-bv-list (x, size)

Theorem: untag-array-tag-array-of-match-and-xor-hack untag-array (tag-array (l, match-and-xor (nat-to-bv-list (x, s), y, z))) = match-and-xor (nat-to-bv-list (x, s), y, z)

Theorem: member-list-max-list nat-list-piton (x, s) → ((list ('nat, max-list (untag-array (x))) ∈ x) = listp (x))

Theorem: tag-array-replace-value-untag-array nat-list-piton (x, s) → (tag-array ('nat, replace-value (untag-array (x), y, z))

= replace-value (x, list ('nat, y), list ('nat, z)))

Definition: smart-move-input-conditionp (p0 ) = (listp (p-ctrl-stk (p0 ))

∧ at-least-morep (length (p-temp-stk (p0 )),

                3,

p-max-temp-stk-size (p0 ))

∧ at-least-morep (p-ctrl-stk-size (p-ctrl-stk (p0 )),

                19,

p-max-ctrl-stk-size (p0 ))

∧ (1 < p-word-size (p0 )) ∧ (cddr (top (p-temp-stk (p0 ))) = nil) ∧ (cddr (top (cdr (p-temp-stk (p0 )))) = nil) ∧ (cddr (top (cddr (p-temp-stk (p0 )))) = nil) ∧ (car (top (p-temp-stk (p0 ))) = 'addr) ∧ (car (top (cdr (p-temp-stk (p0 )))) = 'nat) ∧ (untag (top (cdr (p-temp-stk (p0 )))) < exp (2, p-word-size (p0 ))) ∧ (untag (top (cdr (p-temp-stk (p0 )))) ≄ 0) ∧ (car (top (cddr (p-temp-stk (p0 )))) = 'addr) ∧ listp (untag (top (p-temp-stk (p0 )))) ∧ listp (untag (top (cddr (p-temp-stk (p0 ))))) ∧ (cdr (untag (top (p-temp-stk (p0 )))) = 0) ∧ (cdr (untag (top (cddr (p-temp-stk (p0 ))))) = 0) ∧ definedp (car (untag (top (p-temp-stk (p0 )))), p-data-segment (p0 )) ∧ definedp (car (untag (top (cddr (p-temp-stk (p0 ))))),

p-data-segment (p0 ))

∧ (car (untag (top (p-temp-stk (p0 ))))

≠ car (untag (top (cddr (p-temp-stk (p0 )))))) ∧ nat-list-piton (array (car (untag (top (cddr (p-temp-stk (p0 ))))),

p-data-segment (p0 )), p-word-size (p0 ))

∧ array-pitonp (array (car (untag (top (p-temp-stk (p0 )))),

p-data-segment (p0 )), untag (top (cdr (p-temp-stk (p0 )))))

∧ (length (array (car (untag (top (cddr (p-temp-stk (p0 ))))),

p-data-segment (p0 )))

= untag (top (cdr (p-temp-stk (p0 ))))) ∧ (assoc ('smart-move, p-prog-segment (p0 ))

= smart-move-program) ∧ (assoc ('replace-value, p-prog-segment (p0 ))

= replace-value-program) ∧ (assoc ('max-nat, p-prog-segment (p0 )) = max-nat-program) ∧ (assoc ('bv-to-nat-list, p-prog-segment (p0 ))

= bv-to-nat-list-program) ∧ (assoc ('nat-to-bv-list, p-prog-segment (p0 ))

= nat-to-bv-list-program) ∧ (assoc ('match-and-xor, p-prog-segment (p0 ))

= match-and-xor-program) ∧ (assoc ('highest-bit, p-prog-segment (p0 ))

= highest-bit-program) ∧ (assoc ('number-with-at-least, p-prog-segment (p0 ))

= number-with-at-least-program) ∧ (assoc ('bv-to-nat, p-prog-segment (p0 ))

= bv-to-nat-program) ∧ (assoc ('nat-to-bv, p-prog-segment (p0 ))

= nat-to-bv-program) ∧ (assoc ('push-1-vector, p-prog-segment (p0 ))

= push-1-vector-program (p-word-size (p0 ))) ∧ (assoc ('xor-bvs, p-prog-segment (p0 )) = xor-bvs-program))

Theorem: correctness-of-smart-move ((p0 = p-state (pc,

ctrl-stk, cons (wa, cons (np, cons (s, temp-stk))), prog-segment, data-segment, max-ctrl-stk-size, max-temp-stk-size, word-size,

'run))

∧ (p-current-instruction (p0 ) = '(call smart-move)) ∧ (state = untag-array (array (car (untag (s)), data-segment))) ∧ (word-size = word-size2 ) ∧ smart-move-input-conditionp (p0 )) → (p (p-state (pc,

ctrl-stk, cons (wa, cons (np, cons (s, temp-stk))), prog-segment, data-segment, max-ctrl-stk-size, max-temp-stk-size, word-size,

'run),

smart-move-clock (state, word-size2 )) = p-state (add1-addr (pc),

ctrl-stk,

temp-stk,

prog-segment,

put-assoc (tag-array ('nat,

smart-move (state, word-size)),

car (untag (s)),

if number-with-at-least (state, 2) < 2 then data-segment else put-assoc (tag-array ('bitv,

nat-to-bv-list (smart-move (state,

word-size),

word-size)),

car (untag (wa)), data-segment) endif),

max-ctrl-stk-size, max-temp-stk-size, word-size,

          'run))

Event: Disable smart-move-clock.

Event: Disable smart-move-program.

Event: Disable *1*smart-move-program.

;; delay

Definition: delay-program

= '(delay
(time)
nil
(dl lab nil (push-local time))
(sub1-nat)
(set-local time)
(no-op)
(no-op)
(no-op)
(no-op)
(test-nat-and-jump zero done)
(no-op)
(jump lab)
(dl done nil (ret)))

Definition: example-delay-p-state

= p-state ('(pc (main . 0)),
'((nil (pc (main . 0)))),

nil,

list ('(main nil nil
      (push-constant (nat 4))
      (call delay)
      (ret)),

delay-program), nil,

100,
80,
8,
'run)

Definition: delay-loop-clock (time) = if time < 2 then 9

else 10 + delay-loop-clock (time − 1) endif

Theorem: correctness-of-delay-general (listp (ctrl-stk) ∧ (definition ('delay, prog-segment) = delay-program) ∧ at-least-morep (length (temp-stk), 1, max-temp-stk-size) ∧ (0 < time) ∧ (time < exp (2, word-size)))

→ (p (p-state ('(pc (delay . 0)),

cons (list (list (cons ('time, list ('nat, time))), ret-pc),

ctrl-stk), temp-stk, prog-segment, data-segment, max-ctrl-stk-size, max-temp-stk-size, word-size,

    'run),

delay-loop-clock (time)) = p-state (ret-pc,

ctrl-stk, temp-stk, prog-segment, data-segment, max-ctrl-stk-size, max-temp-stk-size, word-size,

     'run))

Definition: delay-input-conditionp (p0 ) = (listp (p-ctrl-stk (p0 ))

∧ (definition ('delay, p-prog-segment (p0 )) = delay-program) ∧ (car (top (p-temp-stk (p0 ))) = 'nat) ∧ at-least-morep (length (p-temp-stk (p0 )),

       0,

p-max-temp-stk-size (p0 ))

∧ at-least-morep (p-ctrl-stk-size (p-ctrl-stk (p0 )),

       3,

p-max-ctrl-stk-size (p0 ))

∧ (0 < cadr (top (p-temp-stk (p0 )))) ∧ (cadr (top (p-temp-stk (p0 ))) < exp (2, p-word-size (p0 ))) ∧ (cddr (top (p-temp-stk (p0 ))) = nil))

Definition: delay-clock (time) = (1 + delay-loop-clock (time))

Theorem: correctness-of-delay ((p0 = p-state (pc,

ctrl-stk, cons (n, temp-stk), prog-segment, data-segment, max-ctrl-stk-size, max-temp-stk-size, word-size,

'run))

∧ (p-current-instruction (p0 ) = '(call delay)) ∧ delay-input-conditionp (p0 ) ∧ (time = cadr (n))) → (p (p-state (pc,

ctrl-stk, cons (n, temp-stk), prog-segment, data-segment, max-ctrl-stk-size, max-temp-stk-size, word-size,

'run),

delay-clock (time)) = p-state (add1-addr (pc),

ctrl-stk,

temp-stk,

prog-segment, data-segment, max-ctrl-stk-size, max-temp-stk-size, word-size,

          'run))
;; computer-move

Definition: computer-move-program

= '(computer-move
(state numpiles work-area)
((i (nat 0)))
(push-constant (nat 250))
(call delay)
(push-constant (nat 250))
(call delay)
(push-constant (nat 250))
(call delay)
(push-constant (nat 250))
(call delay)
(push-local state)
(push-local numpiles)
(push-constant (nat 2))
(call number-with-at-least)
(test-nat-and-jump zero lab)
(push-local state)
(push-local work-area)
(push-local numpiles)
(call nat-to-bv-list)
(push-local work-area)
(push-local numpiles)
(call xor-bvs)
(test-bitv-and-jump all-zero lab)
(push-local state)
(push-local numpiles)
(push-local work-area)
(call smart-move)
(ret)
(dl lab nil (push-local state))
(push-local state)
(push-local numpiles)
(call max-nat)

(pop-local i)
(push-local i)
(push-local i)
(sub1-nat)
(call replace-value)
(ret))

Definition: example-computer-move-p-state

= p-state ('(pc (main . 0)),
'((nil (pc (main . 0)))),

nil,

list ('(main nil nil
(push-constant (addr (arr . 0)))
(push-constant (nat 4))
(push-constant (addr (arr5 . 0)))
(call computer-move)
(push-constant (addr (arr2 . 0)))
(push-constant (nat 4))
(push-constant (addr (arr5 . 0)))
(call computer-move)
(push-constant (addr (arr3 . 0)))
(push-constant (nat 4))
(push-constant (addr (arr5 . 0)))
(call computer-move)
(push-constant (addr (arr4 . 0)))
(push-constant (nat 4))
(push-constant (addr (arr5 . 0)))
(call computer-move)
(ret)),

computer-move-program, delay-program, replace-value-program, max-nat-program, bv-to-nat-list-program, nat-to-bv-list-program, match-and-xor-program, highest-bit-program, number-with-at-least-program, bv-to-nat-program, nat-to-bv-program, push-1-vector-program (8), xor-bvs-program, smart-move-program),

          '((arr (nat 3) (nat 4) (nat 2) (nat 1))
            (arr2 (nat 1) (nat 1) (nat 1) (nat 0))
            (arr3 (nat 1) (nat 1) (nat 0) (nat 9))
            (arr4 (nat 7) (nat 4) (nat 2) (nat 2))
            (arr5 (nat 3) (nat 4) (nat 2) (nat 1))),
          100,
          80,
          8,
          'run)

Definition: computer-move (state, wordsize) = if (number-with-at-least (state, 2) = 0)

∨ all-zero-bitvp (xor-bvs (nat-to-bv-list (state, wordsize))) then replace-value (state, max-list (state), max-list (state) − 1) else smart-move (state, wordsize) endif

Event: Disable delay-clock.

(defn computer-move-clock (state wordsize)
  (clock-plus
   2
   (clock-plus (delay-clock 250)
       (clock-plus 1 (clock-plus (delay-clock 250)
       (clock-plus 1 (clock-plus (delay-clock 250)
       (clock-plus 1 (clock-plus (delay-clock 250)
  (clock-plus
   3
   (clock-plus
    (number-with-at-least-clock 2 (tag-array 'nat state))
    (clock-plus
     1
    (if (equal (number-with-at-least state 2) 0)
(clock-plus
    3
    (clock-plus
     (max-nat-clock (tag-array 'nat state))
     (clock-plus
      4
      (clock-plus
       (replace-value-clock
(tag-array 'nat state)

(list 'nat (max-list state)))
       1))))
  (clock-plus
   3
   (clock-plus
    (nat-to-bv-list-clock (tag-array 'nat state))
    (clock-plus
     2
     (clock-plus
      (xor-bvs-clock (length state))
      (clock-plus
       1
       (if (all-zero-bitvp (xor-bvs (nat-to-bv-list state wordsize)))
   (clock-plus
    3
    (clock-plus
     (max-nat-clock (tag-array 'nat state))
     (clock-plus
      4
      (clock-plus
       (replace-value-clock
(tag-array 'nat state)
(list 'nat (max-list state)))
       1))))
 (clock-plus
  3
  (clock-plus
   (smart-move-clock state wordsize)
   1)))))))))))))))))))))

Definition: computer-move-input-conditionp (p0 ) = ((¬ all-zero-bitvp (untag-array (array (car (untag (top (cddr (p-temp-stk (p0 ))))),

p-data-segment (p0 )))))

∧ listp (p-ctrl-stk (p0 ))

∧ at-least-morep (length (p-temp-stk (p0 )),

                     3,

p-max-temp-stk-size (p0 ))

∧ at-least-morep (p-ctrl-stk-size (p-ctrl-stk (p0 )),

                     25,

p-max-ctrl-stk-size (p0 ))

∧ (7 < p-word-size (p0 )) ∧ (p-word-size (p0 ) ≄ 0) ∧ (p-word-size (p0 ) ≠ 1)

∧ (cddr (top (p-temp-stk (p0 ))) = nil) ∧ (cddr (top (cdr (p-temp-stk (p0 )))) = nil) ∧ (cddr (top (cddr (p-temp-stk (p0 )))) = nil) ∧ (car (top (p-temp-stk (p0 ))) = 'addr) ∧ (car (top (cdr (p-temp-stk (p0 )))) = 'nat) ∧ (untag (top (cdr (p-temp-stk (p0 )))) < exp (2, p-word-size (p0 ))) ∧ (untag (top (cdr (p-temp-stk (p0 )))) ≄ 0) ∧ (car (top (cddr (p-temp-stk (p0 )))) = 'addr) ∧ listp (untag (top (p-temp-stk (p0 )))) ∧ listp (untag (top (cddr (p-temp-stk (p0 ))))) ∧ (cdr (untag (top (p-temp-stk (p0 )))) = 0) ∧ (cdr (untag (top (cddr (p-temp-stk (p0 ))))) = 0) ∧ definedp (car (untag (top (p-temp-stk (p0 )))), p-data-segment (p0 )) ∧ definedp (car (untag (top (cddr (p-temp-stk (p0 ))))),

p-data-segment (p0 ))

∧ (car (untag (top (p-temp-stk (p0 ))))

≠ car (untag (top (cddr (p-temp-stk (p0 )))))) ∧ nat-list-piton (array (car (untag (top (cddr (p-temp-stk (p0 ))))),

p-data-segment (p0 )), p-word-size (p0 ))

∧ array-pitonp (array (car (untag (top (p-temp-stk (p0 )))),

p-data-segment (p0 )), untag (top (cdr (p-temp-stk (p0 )))))

∧ (length (array (car (untag (top (cddr (p-temp-stk (p0 ))))),

p-data-segment (p0 )))

= untag (top (cdr (p-temp-stk (p0 ))))) ∧ (assoc ('delay, p-prog-segment (p0 )) = delay-program) ∧ (assoc ('computer-move, p-prog-segment (p0 ))

= computer-move-program) ∧ (assoc ('smart-move, p-prog-segment (p0 ))

= smart-move-program) ∧ (assoc ('replace-value, p-prog-segment (p0 ))

= replace-value-program) ∧ (assoc ('max-nat, p-prog-segment (p0 )) = max-nat-program) ∧ (assoc ('bv-to-nat-list, p-prog-segment (p0 ))

= bv-to-nat-list-program) ∧ (assoc ('nat-to-bv-list, p-prog-segment (p0 ))

= nat-to-bv-list-program) ∧ (assoc ('match-and-xor, p-prog-segment (p0 ))

= match-and-xor-program) ∧ (assoc ('highest-bit, p-prog-segment (p0 ))

= highest-bit-program) ∧ (assoc ('number-with-at-least, p-prog-segment (p0 ))

= number-with-at-least-program)

∧ (assoc ('bv-to-nat, p-prog-segment (p0 ))

= bv-to-nat-program) ∧ (assoc ('nat-to-bv, p-prog-segment (p0 ))

= nat-to-bv-program) ∧ (assoc ('push-1-vector, p-prog-segment (p0 )) = push-1-vector-program (p-word-size (p0 )))

∧ (assoc ('xor-bvs, p-prog-segment (p0 )) = xor-bvs-program))

Theorem: numberp-max-list max-list (x) ∈ N

Theorem: max-0-means nat-list-piton (x, s) → ((max-list (untag-array (x)) = 0) = all-zero-bitvp (untag-array (x)))

Theorem: max-list-not-too-big (nat-list-piton (x, s) ∧ (s ≄ 0)) → ((max-list (untag-array (x)) < exp (2, s))

∧ (((max-list (untag-array (x)) − 1) < exp (2, s)) = t))

Event: Disable delay-clock.

Event: Disable *1*delay-clock.

Theorem: lessp-exp-2-8-hack ((7 < free) ∧ (x = free) ∧ (val < 256)) → ((val < exp (2, x)) = t)

Theorem: correctness-of-computer-move ((p0 = p-state (pc,

ctrl-stk,

cons (wa, cons (np, cons (s, temp-stk))), prog-segment, data-segment, max-ctrl-stk-size, max-temp-stk-size, word-size,

             'run))

∧ (p-current-instruction (p0 ) = '(call computer-move)) ∧ (state = untag-array (array (car (untag (s)), data-segment))) ∧ (word-size = word-size2 ) ∧ computer-move-input-conditionp (p0 )) → (p (p-state (pc,

ctrl-stk, cons (wa, cons (np, cons (s, temp-stk))), prog-segment, data-segment, max-ctrl-stk-size, max-temp-stk-size, word-size,

'run),

computer-move-clock (state, word-size2 )) = p-state (add1-addr (pc),

ctrl-stk, temp-stk, prog-segment, put-assoc (tag-array ('nat,

computer-move (state, word-size)),

car (untag (s)),

if number-with-at-least (state, 2) = 0

then data-segment

else put-assoc (if all-zero-bitvp (xor-bvs (nat-to-bv-list (state,

word-size)))

∨ (number-with-at-least (state,

                                               2)

< 2) then tag-array ('bitv,

nat-to-bv-list (state,

word-size))

else tag-array ('bitv,

nat-to-bv-list (computer-move (state,

word-size),

word-size)) endif,

car (untag (wa)), data-segment) endif),

max-ctrl-stk-size, max-temp-stk-size, word-size,

'run))
;;;;
;;;;
;;;;
;;;;
;;;; Having proved the behavior of the programs, we now introduce
;;;; the spec to which we've been writing code.
;;;;
;;;;

;;;;

Definition: sum (list) = if listp (list) then car (list) + sum (cdr (list))

else 0 endif

Theorem: sum-append sum (append (x, y)) = (sum (x) + sum (y))

;; returns a list of states that are valid moves from

Definition: all-valid-moves-helper (old, val, origval, new) = if val ≃ 0

then if new ≃ nil then nil

else all-valid-moves-helper (append (old, list (origval)), car (new), car (new), cdr (new)) endif

else cons (append (old, cons (val − 1, new)), all-valid-moves-helper (old, val − 1, origval, new)) endif

Definition: all-valid-moves (x) = all-valid-moves-helper (nil, car (x), car (x), cdr (x))

Definition: max-sum (list) = if listp (list)

then if sum (car (list)) < max-sum (cdr (list)) then max-sum (cdr (list))

else sum (car (list)) endif else 0 endif

Theorem: nat-listp-append properp (x) → (nat-listp (append (x, y), size)

= (nat-listp (x, size) ∧ nat-listp (y, size)))

;(prove-lemma properp-append (rewrite)
;      (equal
;       (properp (append x y))
;       (properp y)))

Event: Enable properp-append.

Definition: nat-listp-simple (list) = if listp (list) then (car (list) ∈ N) ∧ nat-listp-simple (cdr (list))

else list = nil endif

Theorem: nat-listp-simple-append properp (x) → (nat-listp-simple (append (x, y))

= (nat-listp-simple (x) ∧ nat-listp-simple (y)))

Theorem: lessp-max-sum-helper ((c ≮ temp) ∧ properp (x) ∧ nat-listp-simple (append (x, cons (c, y))) ∧ (¬ all-zero-bitvp (append (x, cons (c, y))))) → (max-sum (all-valid-moves-helper (x, temp, c, y))

< sum (append (x, cons (c, y))))

Theorem: lessp-max-sum-all-valid-moves (nat-listp-simple (s) ∧ (¬ all-zero-bitvp (s))) → ((max-sum (all-valid-moves (s)) < sum (s)) = t)

Theorem: lessp-sum-max-sum max-sum (x) ≮ sum (car (x))

Event: Disable all-valid-moves.

Definition: wsp-measure (state, flag) = cons (if flag then 1 + sum (state)

else 1 + max-sum (state) endif, if flag then 0 else length (state) endif)

;; wsp searchs for a successor to  the current state on
;; a path to a guaranteed win.
;; if flag
;;      state is a nim state - return state if all zeros.
;;      Return a successor state not wsp if one exists, f otherwise
;; if not flag
;;      state is a list of states - return member of list if it is
;;      not wsp, f is no such member.

Definition: wsp (state, flag) = if flag

then if all-zero-bitvp (state) ∨ (¬ nat-listp-simple (state)) then state else wsp (all-valid-moves (state), f) endif

elseif listp (state)

then if ¬ wsp (car (state), t) then car (state) else wsp (cdr (state), f) endif

else f endif

Definition: green-statep (state, wordsize) = ((number-with-at-least (state, 2) ≃ 0)

= all-zero-bitvp (xor-bvs (nat-to-bv-list (state, wordsize))))

Definition: non-green-in-list (list, wordsize) = if listp (list)

then (¬ green-statep (car (list), wordsize))

∨ non-green-in-list (cdr (list), wordsize) else f endif

Theorem: nat-listp-means-nat-listp-simple nat-listp (x, s) → nat-listp-simple (x)

Theorem: xor-bitv-zero-bit-vector all-zero-bitvp (x) → (xor-bitv (x, y) = make-list-from (length (x), fix-bitv (y)))

Theorem: fix-bitv-xor-bitv fix-bitv (xor-bitv (x, y)) = xor-bitv (x, y)

Theorem: fix-bitv-and-bitv fix-bitv (and-bitv (x, y)) = and-bitv (x, y)

Theorem: fix-bitv-xor-bvs fix-bitv (xor-bvs (x)) = xor-bvs (x)

Theorem: all-zero-bitvp-make-list-from-simple all-zero-bitvp (x) → all-zero-bitvp (make-list-from (n, x))

Theorem: all-zero-bitvp-xor-bvs-nat-to-bv-list-zeros all-zero-bitvp (x) → all-zero-bitvp (xor-bvs (nat-to-bv-list (x, s)))

Theorem: number-with-at-least-of-all-zeros all-zero-bitvp (x) → (number-with-at-least (x, m)

= if m ≃ 0 then length (x)

else 0 endif)

Definition: nat-listp-listp (list, wordsize) = if listp (list)

then nat-listp (car (list), wordsize)

∧ nat-listp-listp (cdr (list), wordsize) else t endif

Theorem: nat-listp-listp-all-valid-moves-helper (nat-listp (a, s) ∧ (b < exp (2, s)) ∧ (c < exp (2, s)) ∧ (b ∈ N) ∧ (c ∈ N) ∧ nat-listp (d, s) ∧ properp (a)) → nat-listp-listp (all-valid-moves-helper (a, b, c, d), s)

Theorem: nat-listp-listp-all-valid-moves nat-listp (a, s) → nat-listp-listp (all-valid-moves (a), s)

Theorem: listp-all-valid-move-helper nat-listp-simple (d) → (listp (all-valid-moves-helper (a, b, c, d))

= ((¬ all-zero-bitvp (d)) ∨ (b ≄ 0)))

Theorem: listp-all-valid-move nat-listp-simple (x) → (listp (all-valid-moves (x)) = (¬ all-zero-bitvp (x)))

Theorem: number-with-at-least-append number-with-at-least (append (x, y), m) = (number-with-at-least (x, m) + number-with-at-least (y, m))

Theorem: length-xor-bvs2 bit-vectorsp (x, s) → (length (xor-bvs (x))

= if listp (x) then fix (s)

else 0 endif)

Theorem: xor-bitv-xor-bvs-hack bit-vectorsp (z, length (y)) → (xor-bitv (xor-bitv (y, xor-bvs (z)), x)

= if listp (z) then xor-bitv (y, xor-bitv (xor-bvs (z), x)) else xor-bitv (y, x) endif)

Theorem: xor-bitv-fix-bitv (xor-bitv (fix-bitv (x), y) = xor-bitv (x, y)) ∧ (xor-bitv (x, fix-bitv (y)) = xor-bitv (x, y))

Theorem: xor-bvs-append (bit-vectorsp (x, s) ∧ bit-vectorsp (y, s) ∧ (s ∈ N)) → (xor-bvs (append (x, y))

= if listp (x) then xor-bitv (xor-bvs (x), xor-bvs (y)) else xor-bvs (y) endif)

Theorem: xor-bvs-append-hack bit-vectorsp (y, ws) → (xor-bvs (append (nat-to-bv-list (a, ws), y))

= if listp (a)

then xor-bitv (xor-bvs (nat-to-bv-list (a, ws)), xor-bvs (y)) else xor-bvs (y) endif)

Theorem: nat-to-bv-list-append nat-to-bv-list (append (x, y), s) = append (nat-to-bv-list (x, s), nat-to-bv-list (y, s))

Theorem: bit-vectorp-nat-to-bv bit-vectorp (nat-to-bv (x, s), s2 ) = (fix (s) = fix (s2 ))

Theorem: fix-bitv-nat-to-bv fix-bitv (nat-to-bv (x, s)) = nat-to-bv (x, s)

Theorem: fix-bitv-zero-bit-vector fix-bitv (zero-bit-vector (x)) = zero-bit-vector (x)

Theorem: all-zero-bitvp-nat-to-bv all-zero-bitvp (nat-to-bv (x, s)) = ((x ≃ 0) ∨ (s ≃ 0))

Theorem: all-zero-bitvp-xor-bitv-better all-zero-bitvp (xor-bitv (x, y)) = (fix-bitv (x) = make-list-from (length (x), fix-bitv (y)))

Theorem: length-xor-bvs-nat-to-bv-list length (xor-bvs (nat-to-bv-list (x, s))) = if listp (x) then fix (s)

else 0 endif Theorem: fix-bitv-make-list-from fix-bitv (make-list-from (s, x)) = make-list-from (s, fix-bitv (x))

Definition: double-sub1-cdr (n1 , n2 , l) = if (n1 ≃ 0) ∨ (n2 ≃ 0) then t

else double-sub1-cdr (n1 − 1, n2 − 1, cdr (l)) endif

Theorem: make-list-from-make-list-from make-list-from (s1 , make-list-from (s2 , x)) = if s2 < s1

then append (make-list-from (s2 , x), zero-bit-vector (s1 − s2 )) else make-list-from (s1 , x) endif

;(prove-lemma associativity-of-append (rewrite)
;      (equal
;       (append (append a b) c)
;       (append a (append b c))))

Event: Enable associativity-of-append.

;(prove-lemma append-cons (rewrite)
;      (equal
;       (append (cons a b) c)
;       (cons a (append b c))))

Event: Enable append-cons.

Theorem: properp-xor-bvs properp (xor-bvs (x))

Theorem: properp-xor-bitv properp (xor-bitv (x, y))

Definition: member-number-with-at-least (x, min) = if listp (x)

then if number-with-at-least (car (x), min) ≄ 0 then car (x)

else member-number-with-at-least (cdr (x), min) endif else f endif

Theorem: xor-bvs-nat-to-bv-list-zerop-ws (ws ≃ 0) → (xor-bvs (nat-to-bv-list (x, ws)) = nil)

Definition: nat-listp-listp-simple (x) = if listp (x)

then nat-listp-simple (car (x)) ∧ nat-listp-listp-simple (cdr (x)) else x = nil endif

Theorem: non-green-in-list-zerop-ws ((ws ≃ 0) ∧ nat-listp-listp-simple (x)) → (non-green-in-list (x, ws) ↔ member-number-with-at-least (x, 2))

Theorem: nat-listp-listp-simple-means-properp nat-listp-listp-simple (x) → properp (x)

Theorem: nat-listp-simple-means-properp nat-listp-simple (x) → properp (x)

Theorem: make-list-from-xor-bvs-nat-to-bv-list (fix (ws) = fix (s)) → (make-list-from (ws, xor-bvs (nat-to-bv-list (x, s)))

= if listp (x) then xor-bvs (nat-to-bv-list (x, s)) else zero-bit-vector (ws) endif)

Theorem: last-xor-bitv last (xor-bitv (x, y)) = if listp (x) then xor-bit (last (x), nth (length (x) − 1, y))

else 0 endif

Theorem: last-one-bit-vector last (one-bit-vector (x)) = 1

Theorem: nth-as-last ((1 + n) = length (x)) → (nth (n, x) = last (x))

Theorem: listp-nat-to-bv listp (nat-to-bv (x, s)) = (s ≄ 0)

;(prove-lemma remainder-plus-x-x-2 (rewrite)
;      (equal (remainder (plus x x) 2) 0))

Event: Enable remainder-plus-x-x-2.

Theorem: last-nat-to-bv last (nat-to-bv (x, s)) = if (s ≃ 0) ∨ ((x < exp (2, s)) ∧ ((x mod 2) = 0)) then 0

else 1 endif Theorem: fix-bitv-one-bit-vector fix-bitv (one-bit-vector (x)) = one-bit-vector (x)

Theorem: nat-to-bv-1 nat-to-bv (1, x) = if x ≃ 0 then nil

else one-bit-vector (x) endif

Theorem: last-zero-bit-vector last (zero-bit-vector (x)) = 0

Theorem: nat-to-bv-2 nat-to-bv (x, 2) = if x ≃ 0 then list (0, 0)

elseif x = 1 then list (0, 1) elseif x = 2 then list (1, 0) else list (1, 1) endif

Theorem: all-zero-bitvp-all-but-last-nat-to-bv all-zero-bitvp (all-but-last (nat-to-bv (x, s))) = ((x < 2) ∨ (s < 2))

Theorem: xor-bvs-of-list-of-0s-and-1s (number-with-at-least (c, 2) ≃ 0) → (xor-bvs (nat-to-bv-list (c, ws))

= if (c ≃ nil) ∨ (ws ≃ 0) then nil elseif (sum (c) mod 2) = 0 then zero-bit-vector (ws) else one-bit-vector (ws) endif)

Theorem: equal-nat-to-bv-nlistp (x ≃ nil) → ((x = nat-to-bv (y, s)) = ((x = nil) ∧ (s ≃ 0)))

Theorem: different-lengths-means-different-hack (fix (s1 ) ≠ fix (s2 )) → (length (nat-to-bv (x, s1 )) ≠ length (nat-to-bv (y, s2 )))

Theorem: different-lengths-means-different (fix (s1 ) ≠ fix (s2 )) → (nat-to-bv (x, s1 ) ≠ nat-to-bv (y, s2 ))

Definition: nat-to-bv-induct (x, y, s1 , s2 ) = if s1 ≃ 0 then t

else nat-to-bv-induct (if x < exp (2, s1 − 1) then x else x − exp (2, s1 − 1) endif, if y < exp (2, s2 − 1) then y else y − exp (2, s2 − 1) endif, s1 − 1, s2 − 1) endif Definition: all-ones-vector (x) = if x ≃ 0 then nil

else cons (1, all-ones-vector (x − 1)) endif

Theorem: not-lessp-exp-means-all-ones (x ≮ (exp (2, s) − 1)) → (nat-to-bv (x, s) = all-ones-vector (s))

Theorem: lessp-sub1-plus-sub1-hack (y ≄ 0) → ((((x + y) − 1) < ((y − 1) + z)) = (x < z))

Theorem: equal-cons-zero-bit-vector-nat-to-bv (cons (0, zero-bit-vector (x)) = nat-to-bv (a, b)) = (((1 + x) = fix (b)) ∧ (a ≃ 0))

Theorem: equal-all-ones-vector-all-ones-vector (all-ones-vector (x) = all-ones-vector (y)) = (fix (x) = fix (y))

Theorem: equal-all-ones-vector-cons (all-ones-vector (x) = cons (a, b)) = ((x ≄ 0) ∧ (a = 1) ∧ (all-ones-vector (x − 1) = b))

Theorem: different-lengths-obvious (x = y) → (length (x) = length (y))

Theorem: equal-all-ones-vector-nlistp (x ≃ nil) → ((all-ones-vector (y) = x) = ((x = nil) ∧ (y ≃ 0)))

Theorem: length-all-ones-vector length (all-ones-vector (x)) = fix (x)

Theorem: different-lengths-hack (fix (x) ≠ fix (y)) → (all-ones-vector (x) ≠ nat-to-bv (a, y))

Theorem: lessp-difference-arg1 (x ≮ y) → (((x − y) < z) = (x < (y + z)))

Theorem: equal-difference (x ≮ y) → (((x − y) = z) = ((fix (x) = (y + z)) ∧ (z ∈ N)))

Theorem: equal-exp (fix (a) = fix (b)) → ((exp (a, c) = exp (b, d))

= ((a = 1) ∨ ((a ≃ 0) ∧ ((c ≃ 0) = (d ≃ 0))) ∨ (fix (c) = fix (d))))

Theorem: equal-all-ones-nat-to-bv (all-ones-vector (x) = nat-to-bv (a, b)) = ((fix (x) = fix (b)) ∧ (a ≮ (exp (2, b) − 1)))

Theorem: equal-nat-to-bv-nat-to-bv (nat-to-bv (x, s1 ) = nat-to-bv (y, s2 )) = ((fix (s1 ) = fix (s2 ))

∧ ((fix (x) = fix (y)) ∨ ((x ≮ (exp (2, s1 ) − 1)) ∧ (y ≮ (exp (2, s1 ) − 1)))))

Theorem: listp-xor-bvs listp (xor-bvs (x)) = listp (car (x))

Theorem: car-nat-to-bv-list car (nat-to-bv-list (x, s)) = if listp (x) then nat-to-bv (car (x), s)

else 0 endif

;; from later version of naturals that is used in this proof

Theorem: quotient-difference ((x − y) ÷ z) = if (x mod z) < (y mod z) then ((x ÷ z) − (y ÷ z)) − 1

else (x ÷ z) − (y ÷ z) endif

Event: Enable difference-x-sub1-x.

Theorem: all-but-last-nat-to-bv all-but-last (nat-to-bv (x, s)) = if s ≃ 0 then nil

else nat-to-bv (x ÷ 2, s − 1) endif

Theorem: equal-last-xor-bvs-1 (last (xor-bvs (x)) = 1) = (last (xor-bvs (x)) ≠ 0)

Theorem: not-green-state-means ((¬ green-statep (append (a, cons (b, c)), ws)) ∧ (d < exp (2, ws)) ∧ (b < d)) → (green-statep (append (a, cons (d, c)), ws)

= ((ws ≄ 0) ∨ (number-with-at-least (append (a, cons (d, c)), 2) ≃ 0)))

Theorem: green-in-list-all-valid-moves-helper (nat-listp (a, ws)

∧ nat-listp (d, ws) ∧ (c ∈ N) ∧ (c < exp (2, ws)) ∧ properp (a) ∧ non-green-in-list (all-valid-moves-helper (a, b, c, d), ws) ∧ (c ≮ b) ∧ (b ∈ N)) → green-statep (append (a, cons (c, d)), ws)

Theorem: green-in-list-all-valid-moves-means (nat-listp (x, ws) ∧ non-green-in-list (all-valid-moves (x), ws)) → green-statep (x, ws)

Definition: valid-movep (s1 , s2 ) = if listp (s1 ) ∧ listp (s2 )

then ((car (s2 ) < car (s1 )) ∧ (car (s2 ) ∈ N) ∧ (cdr (s1 ) = cdr (s2 ))) ∨ ((car (s1 ) = car (s2 )) ∧ valid-movep (cdr (s1 ), cdr (s2 )))

else f endif

Definition: match-member (m, list) = if listp (list)

then if ¬ all-zero-bitvp (and-bitv (car (list), m)) then car (list)

else match-member (m, cdr (list)) endif else f endif

Theorem: xor-bvs-match-and-xor bit-vectorsp (list, length (value)) → (xor-bvs (match-and-xor (list, match, value))

= if match-member (match, list) then xor-bitv (value, xor-bvs (list)) else xor-bvs (list) endif)

Definition: remove-highest-bits (x) = if listp (x) then cons (cdar (x), remove-highest-bits (cdr (x)))

else nil endif

Theorem: car-remove-highest-bits car (remove-highest-bits (x)) = cdr (car (x))

Theorem: equal-car-highest-bit-1 (car (highest-bit (x)) = 1) = (highest-bit (x) = cons (1, zero-bit-vector (length (x) − 1)))

Theorem: car-xor-bitv car (xor-bitv (x, y)) = if listp (x) then xor-bit (car (x), car (y))

else 0 endif

Theorem: match-member-cons-0 match-member (cons (0, x), y) ↔ match-member (x, remove-highest-bits (y))

Theorem: match-member-cons (bit-vectorsp (v, length (cons (a, b))) ∧ (car (xor-bvs (v)) ≠ 0)) → (match-member (cons (a, b), v)

↔ ((a ≠ 0) ∨ match-member (b, remove-highest-bits (v))))

Theorem: equal-highest-bit-cons-1 (highest-bit (x) = cons (1, y)) = ((car (x) ≠ 0) ∧ (y = zero-bit-vector (length (x) − 1)))

Theorem: length-cdr-xor-bitv length (cdr (xor-bitv (x, y))) = length (cdr (x))

Theorem: length-fix-bitv length (fix-bitv (x)) = length (x)

Theorem: length-cdr-xor-bvs bit-vectorsp (x, s) → (length (cdr (xor-bvs (x)))

= if listp (x) then s − 1 else 0 endif)

Definition: highest-bits-induct (x, s) = if listp (x)

then if listp (car (x))

then if car (highest-bit (xor-bvs (x))) = 1 then t

else highest-bits-induct (remove-highest-bits (x), s − 1) endif else t endif

else t endif

Theorem: bit-vectorsp-remove-highest-bits bit-vectorsp (x, 1 + s) → bit-vectorsp (remove-highest-bits (x), s)

Theorem: xor-bvs-remove-highest-bits bit-vectorsp (x, s) → (xor-bvs (remove-highest-bits (x))

= if listp (x) ∧ (s ≄ 0) then cdr (xor-bvs (x))

else nil endif)

Theorem: match-member-highest-bit-xor-bvs bit-vectorsp (x, s) → (match-member (highest-bit (xor-bvs (x)), x)

↔ (¬ all-zero-bitvp (xor-bvs (x))))

Theorem: match-member-highest-bit-xor-bvs-rewrite bit-vectorsp (x, length (xor-bvs (x))) → (match-member (highest-bit (xor-bvs (x)), x)

↔ (¬ all-zero-bitvp (xor-bvs (x))))

Theorem: bit-vectorsp-nat-to-bv-list-better bit-vectorsp (nat-to-bv-list (x, size), size2 ) = ((x ≃ nil) ∨ (fix (size) = fix (size2 )))

Theorem: match-member-at-least-min-means (match-member (y, nat-to-bv-list (x, ws)) ∧ (bv-to-nat (match-member (y, nat-to-bv-list (x, ws))) ≮ min)) → (number-with-at-least (x, min) ≠ 0)

Theorem: bit-vectorp-highest-bit-xor-bvs bit-vectorp (highest-bit (xor-bvs (x)), ws) = bit-vectorp (xor-bvs (x), ws)

Theorem: number-with-at-least-match-and-xor (nat-listp (x, ws) ∧ bit-vectorp (y, ws) ∧ bit-vectorp (z, ws)) → (number-with-at-least (bv-to-nat-list (match-and-xor (nat-to-bv-list (x,

ws),

y, z)),

min) = if match-member (y, nat-to-bv-list (x, ws)) then (number-with-at-least (x, min) + if bv-to-nat (xor-bitv (z,

match-member (y,

nat-to-bv-list (x,

ws))))

< min then 0 else 1 endif)

− if bv-to-nat (match-member (y, nat-to-bv-list (x, ws)))

< min then 0 else 1 endif

else number-with-at-least (x, min) endif)

Theorem: number-with-at-least-replace-value number-with-at-least (replace-value (x, e, v), min) = if e ∈ x then (number-with-at-least (x, min) + if v < min then 0 else 1 endif) − if e < min then 0 else 1 endif

else number-with-at-least (x, min) endif

Theorem: max-list-means-number-0 ((max-list (x) = n) ∧ (n < m)) → (number-with-at-least (x, m) = 0)

Theorem: member-max-list nat-listp-simple (x) → ((max-list (x) ∈ x) = listp (x))

Theorem: listp-replace-value listp (replace-value (x, e, v)) = listp (x)

Theorem: member-means-lessp-sum (e ∈ x) → (sum (x) ≮ e)

Theorem: sum-replace-value sum (replace-value (x, e, v)) = if e ∈ x then (sum (x) + v) − e

else sum (x) endif

Theorem: remainder-difference-2 ((x − y) mod 2) = if x < y then 0

elseif (x mod 2) = (y mod 2) then 0 else 1 endif

Theorem: lessp-max-list sum (x) ≮ max-list (x)

Theorem: remainder-plus-remainder ((((x mod y) + z) mod y) = ((x + z) mod y)) ∧ (((z + (x mod y)) mod y) = ((x + z) mod y))

Theorem: remainder-plus-remainder2 (((z + (a + (x mod y))) mod y) = ((z + (a + x)) mod y)) ∧ (((z + ((x mod y) + a)) mod y) = ((z + (a + x)) mod y))

Theorem: lessp-max-list-from-number-with-at-least ((number-with-at-least (x, m) = 0) ∧ (m ≄ 0)) → (max-list (x) < m)

Theorem: number-with-at-least-as-sum (number-with-at-least (x, 2) ≃ 0) → (number-with-at-least (x, 1) = sum (x))

Theorem: equal-remainder-add1-2 (((1 + x) mod 2) = ((1 + y) mod 2)) = ((x mod 2) = (y mod 2))

Theorem: remainder-plus-sum-number-hack (number-with-at-least (x, 2) = 1) → (((sum (x) + number-with-at-least (x, 1)) mod 2)

= ((1 + max-list (x)) mod 2))

Theorem: equal-remainder-add1 (((1 + x) mod y) = (x mod y)) = (y = 1)

Theorem: max-0-means-sum-0 (sum (x) = 0) = (max-list (x) = 0)

Theorem: max-0-means-all-zero-bitvp ((max-list (x) = 0) ∧ nat-listp-simple (x)) → all-zero-bitvp (x)

Theorem: remainder-add1-2 ((((1 + x) mod 2) = 0) = ((x mod 2) = 1)) ∧ ((((1 + x) mod 2) = 1) = ((x mod 2) = 0))

Theorem: remainder-sub1-2 (x ≄ 0) → (((((x − 1) mod 2) = 0) = ((x mod 2) = 1))

∧ ((((x − 1) mod 2) = 1) = ((x mod 2) = 0)))

Theorem: equal-x-remainder-sub1-x (((x − 1) mod y) = x) = (x = 0)

Theorem: computer-move-makes-non-green (green-statep (x, ws) ∧ nat-listp (x, ws) ∧ listp (x) ∧ (ws ≄ 0) ∧ (¬ all-zero-bitvp (x))) → (¬ green-statep (computer-move (x, ws), ws))

Theorem: nat-listp-simplify (ws ≃ 0) → (nat-listp (x, ws) = (properp (x) ∧ all-zero-bitvp (x)))

Theorem: computer-move-makes-non-green-rewrite (green-statep (x, ws) ∧ nat-listp (x, ws) ∧ (¬ all-zero-bitvp (x))) → (¬ green-statep (computer-move (x, ws), ws))

Definition: make-properp (x) = if listp (x) then cons (car (x), make-properp (cdr (x)))

else nil endif Theorem: properp-make-properp properp (x) → (make-properp (x) = x)

Theorem: replace-value-simplify (x ∉ y) → (replace-value (y, x, z) = make-properp (y))

Theorem: member-make-properp (x ∈ make-properp (y)) = (x ∈ y)

Theorem: valid-movep-x-x ¬ valid-movep (x, x)

Theorem: valid-movep-replace-value properp (x) → (valid-movep (x, replace-value (x, y, z))

= ((y ∈ x) ∧ (z < y) ∧ (z ∈ N)))

Theorem: number-with-at-least-max-list ((number-with-at-least (x, m) = v) ∧ (0 < v)) → (max-list (x) ≮ m)

Theorem: valid-movep-match-and-xor (nat-listp (x, ws) ∧ bit-vectorp (y, ws) ∧ bit-vectorp (z, ws)) → (valid-movep (x,

bv-to-nat-list (match-and-xor (nat-to-bv-list (x, ws), y, z)))

= (match-member (y, nat-to-bv-list (x, ws))

∧ (bv-to-nat (xor-bitv (z,

match-member (y,

nat-to-bv-list (x, ws))))

< bv-to-nat (match-member (y, nat-to-bv-list (x, ws))))))

Definition: lessp-bv (x, y) = if listp (x) ∧ listp (y)

then if fix-bit (car (x)) = fix-bit (car (y)) then lessp-bv (cdr (x), cdr (y)) else car (x) = 0 endif

else f endif

Theorem: lessp-bv-to-nat bv-to-nat (x) < exp (2, length (x))

Theorem: lessp-as-lessp-bv (length (x) = length (y)) → ((bv-to-nat (x) < bv-to-nat (y)) = lessp-bv (x, y))

Theorem: fix-bitv-highest-bit fix-bitv (highest-bit (x)) = highest-bit (x)

Theorem: properp-highest-bit properp (highest-bit (x))

Theorem: bit-vectorp-fix-bitv bit-vectorp (fix-bitv (x), s) = (length (x) = fix (s))

Theorem: lessp-bv-xor-bitv (length (x) = length (y)) → (lessp-bv (xor-bitv (x, y), y)

= (¬ all-zero-bitvp (and-bitv (y, highest-bit (x)))))

Theorem: length-match-member-nat-to-bv-list length (match-member (a, nat-to-bv-list (x, ws))) = if match-member (a, nat-to-bv-list (x, ws)) then fix (ws)

else 0 endif

Theorem: bit-vectorsp-remove-highest-bits2 bit-vectorsp (x, s1 ) → (bit-vectorsp (remove-highest-bits (x), s2 )

= (((1 + s2 ) = s1 ) ∨ (¬ listp (x))))

Theorem: match-member-high-bit-xor-bvs-helper bit-vectorsp (x, ws) → (match-member (highest-bit (xor-bvs (x)), x)

↔ (¬ all-zero-bitvp (xor-bvs (x))))

Theorem: match-member-high-bit-xor-bvs match-member (highest-bit (xor-bvs (nat-to-bv-list (y, ws))), nat-to-bv-list (y, ws)) ↔ (¬ all-zero-bitvp (xor-bvs (nat-to-bv-list (y, ws))))

Theorem: length-match-member match-member (a, nat-to-bv-list (x, ws)) → (length (match-member (a, nat-to-bv-list (x, ws))) = fix (ws))

Theorem: all-zero-bitvp-and-match-member bit-vectorsp (b, length (a)) → (all-zero-bitvp (and-bitv (a, match-member (a, b)))

= (¬ match-member (a, b)))

Theorem: valid-movep-computer-move-helper (nat-listp (x, ws) ∧ (¬ all-zero-bitvp (x)) ∧ (ws ≄ 0) ∧ listp (x)) → valid-movep (x, computer-move (x, ws))

;;; PART OF SPECIFICATION

Theorem: valid-movep-computer-move (nat-listp (x, ws) ∧ (¬ all-zero-bitvp (x))) → valid-movep (x, computer-move (x, ws))

Theorem: nthcdr-cdr nthcdr (n, cdr (x)) = cdr (nthcdr (n, x))

Theorem: make-list-from-append make-list-from (n, append (a, b)) = if length (a) < n then append (a, make-list-from (n − length (a), b))

else make-list-from (n, a) endif

Theorem: make-list-from-simplify-better (n = length (x)) → (make-list-from (n, x) = make-properp (x))

;(prove-lemma length-cons (rewrite)
;      (equal (length (cons a b)) (add1 (length b))))

Event: Enable length-cons.

Theorem: cdr-nthcdr-cons cdr (nthcdr (n, cons (a, b))) = nthcdr (n, b)

Theorem: equal-append-2 (x = append (a, b)) = ((length (x) ≮ length (a))

∧ (make-list-from (length (a), x) = make-properp (a)) ∧ (nthcdr (length (a), x) = b))

Theorem: member-cons-all-valid-moves-helper1 listp (a) → ((cons (x, y) ∈ all-valid-moves-helper (a, b, c, d))

= ((x = car (a))

∧ (y ∈ all-valid-moves-helper (cdr (a), b, c, d))))

Theorem: member-all-valid-moves-means-prefix properp (a) → ((x ∈ all-valid-moves-helper (a, b, c, d))

→ (make-list-from (length (a), x) = a))

Theorem: equal-nthcdr-cons (n ≮ length (x)) → (nthcdr (n, x) ≠ cons (a, b))

Theorem: lessp-length-simple-member-all-valid-moves (length (a) ≮ length (x)) → (x ∉ all-valid-moves-helper (a, b, c, d))

Theorem: nth-cons nth (n, cons (a, b)) = if n ≃ 0 then a

else nth (n − 1, b) endif Theorem: nth-1 nth (1, x) = cadr (x)

Theorem: get-as-nth get (n, x) = nth (n, x)

Theorem: equal-cons-make-properp (cons (a, b) = make-properp (x)) = (listp (x) ∧ (a = car (x)) ∧ (b = make-properp (cdr (x))))

Theorem: nthcdr-cons-make-list-from-hack nthcdr (n, cons (a, make-list-from (n, z))) = if n ≃ 0 then list (a)

else list (nth (n − 1, z)) endif

Theorem: lessp-sub1-as-equal (a < b) → ((a < (b − 1)) = ((1 + a) ≠ b))

Theorem: equal-nthcdr-cons-better (nthcdr (n, x) = cons (a, b)) = ((n < length (x)) ∧ (nth (n, x) = a) ∧ (nthcdr (1 + n, x) = b))

Theorem: member-all-valid-moves-helper (nat-listp-simple (a) ∧ nat-listp-simple (d) ∧ (b ∈ N) ∧ (c ∈ N)) → ((x ∈ all-valid-moves-helper (a, b, c, d))

= ((make-list-from (length (a), x) = make-properp (a))

∧ (((nth (length (a), x) < b) ∧ (nth (length (a), x) ∈ N) ∧ (nthcdr (1 + length (a), x) = d)) ∨ ((nth (length (a), x) = c) ∧ valid-movep (d,

cdr (nthcdr (length (a), x)))))))

Theorem: member-all-valid-moves nat-listp-simple (x) → ((y ∈ all-valid-moves (x)) = valid-movep (x, y))

Theorem: valid-movep-and-makes-nongreen-means ((x ∈ y) ∧ (¬ green-statep (x, ws))) → non-green-in-list (y, ws)

Theorem: green-means-non-green-in-valid-moves (nat-listp (s, ws) ∧ (¬ all-zero-bitvp (s)) ∧ green-statep (s, ws)) → non-green-in-list (all-valid-moves (s), ws)

Theorem: green-in-list-all-valid-moves (nat-listp (s, ws) ∧ (¬ all-zero-bitvp (s))) → (non-green-in-list (all-valid-moves (s), ws) ↔ green-statep (s, ws))

Theorem: sum-when-all-zero all-zero-bitvp (x) → (sum (x) = 0)

Theorem: green-statep-all-zero-bitvp all-zero-bitvp (x) → green-statep (x, s)

Theorem: wsp-green-state-proof (((flag ∧ nat-listp (s, wordsize)) ∨ ((¬ flag) ∧ nat-listp-listp (s, wordsize))) ∧ listp (s)) → (wsp (s, flag)

↔ if flag then green-statep (s, wordsize) else non-green-in-list (s, wordsize) endif)

Theorem: wsp-green-state nat-listp (s, wordsize) → (wsp (s, t) ↔ green-statep (s, wordsize))

Theorem: nat-listp-replace-value (nat-listp (s, ws) ∧ (new < exp (2, ws)) ∧ (new ∈ N)) → nat-listp (replace-value (s, y, new), ws)

Theorem: nat-listp-bv-to-nat-list bit-vectorsp (x, s) → nat-listp (bv-to-nat-list (x), s)

Theorem: nat-listp-smart-move (nat-listp (s, ws) ∧ (ws ≄ 0)) → nat-listp (smart-move (s, ws), ws)

Theorem: all-zero-bitvp-max-list all-zero-bitvp (s) → (max-list (s) = 0)

Theorem: replace-value-x-x properp (x) → (replace-value (x, y, y) = x)

Theorem: smart-move-small-ws (nat-listp (s, ws) ∧ (ws ≃ 0)) → (smart-move (s, ws) = s)

Theorem: lessp-max-list-from-nat-listp nat-listp (s, ws) → (max-list (s) < exp (2, ws))

Theorem: nat-listp-computer-move nat-listp (s, ws) → nat-listp (computer-move (s, ws), ws)

;; PART OF SPECIFICATION

Theorem: computer-move-works (nat-listp (state, ws) ∧ (¬ all-zero-bitvp (state)) ∧ wsp (state, t)) → (¬ wsp (computer-move (state, ws), t))

Definition: nim-piton-ctrl-stk-requirement = 25

Definition: nim-piton-temp-stk-requirement = 3

Definition: computer-move-implemented-input-conditionp (p0 ) = (listp (p-ctrl-stk (p0 ))

∧ (7 < p-word-size (p0 )) ∧ (1 < p-word-size (p0 )) ∧ at-least-morep (length (p-temp-stk (p0 )),

nim-piton-temp-stk-requirement, p-max-temp-stk-size (p0 ))

∧ at-least-morep (p-ctrl-stk-size (p-ctrl-stk (p0 )), nim-piton-ctrl-stk-requirement, p-max-ctrl-stk-size (p0 ))

∧ (car (top (cddr (p-temp-stk (p0 )))) = 'addr) ∧ (cddr (top (cddr (p-temp-stk (p0 )))) = nil) ∧ listp (untag (top (cddr (p-temp-stk (p0 ))))) ∧ (cdr (untag (top (cddr (p-temp-stk (p0 ))))) = 0) ∧ definedp (car (untag (top (cddr (p-temp-stk (p0 ))))),

p-data-segment (p0 ))

∧ nat-list-piton (array (car (untag (top (cddr (p-temp-stk (p0 ))))),

p-data-segment (p0 )), p-word-size (p0 ))

∧ (car (top (cdr (p-temp-stk (p0 )))) = 'nat) ∧ (cddr (top (cdr (p-temp-stk (p0 )))) = nil) ∧ (length (array (car (untag (top (cddr (p-temp-stk (p0 ))))),

p-data-segment (p0 )))

= untag (top (cdr (p-temp-stk (p0 ))))) ∧ (untag (top (cdr (p-temp-stk (p0 )))) < exp (2, p-word-size (p0 ))) ∧ (untag (top (cdr (p-temp-stk (p0 )))) ≄ 0) ∧ (car (top (p-temp-stk (p0 ))) = 'addr) ∧ (cddr (top (p-temp-stk (p0 ))) = nil) ∧ listp (untag (top (p-temp-stk (p0 )))) ∧ (cdr (untag (top (p-temp-stk (p0 )))) = 0) ∧ definedp (car (untag (top (p-temp-stk (p0 )))), p-data-segment (p0 )) ∧ array-pitonp (array (car (untag (top (p-temp-stk (p0 )))),

p-data-segment (p0 )), untag (top (cdr (p-temp-stk (p0 )))))

∧ (car (untag (top (p-temp-stk (p0 ))))

≠ car (untag (top (cddr (p-temp-stk (p0 )))))) ∧ (¬ all-zero-bitvp (untag-array (array (car (untag (top (cddr (p-temp-stk (p0 ))))),

p-data-segment (p0 ))))))

;; cm-prog is the Nim program.  It may be disappointing to see that it is

;; a function of one argument rather than a constant, as programs ought to
;; be.  This is because we wish to use bit vectors in our program, and
;; because of a weakness in the Piton design there is no way to push
;; a bit-vector on the stack without knowing the word-size.  The only
;; subprogram that uses the word-size is push-1-vector, which is a
;; one-line program that pushes a one-vector onto the stack.

Definition: cm-prog (word-size) = list (xor-bvs-program,

push-1-vector-program (word-size), nat-to-bv-program, bv-to-nat-program, number-with-at-least-program, highest-bit-program, match-and-xor-program, nat-to-bv-list-program, bv-to-nat-list-program, max-nat-program, replace-value-program, smart-move-program, delay-program, computer-move-program)

Event: Disable computer-move-program.

Event: Disable *1*computer-move-program.

Theorem: car-xor-bvs-program car (xor-bvs-program) = 'xor-bvs

Theorem: car-push-1-vector-program car (push-1-vector-program (word-size)) = 'push-1-vector

Theorem: car-nat-to-bv-program car (nat-to-bv-program) = 'nat-to-bv

Theorem: car-bv-to-nat-program car (bv-to-nat-program) = 'bv-to-nat

Theorem: car-number-with-at-least-program car (number-with-at-least-program) = 'number-with-at-least

Theorem: car-highest-bit-program car (highest-bit-program) = 'highest-bit Theorem: car-match-and-xor-program car (match-and-xor-program) = 'match-and-xor

Theorem: car-nat-to-bv-list-program car (nat-to-bv-list-program) = 'nat-to-bv-list

Theorem: car-bv-to-nat-list-program car (bv-to-nat-list-program) = 'bv-to-nat-list

Theorem: car-max-nat-program car (max-nat-program) = 'max-nat

Theorem: car-replace-value-program car (replace-value-program) = 'replace-value

Theorem: car-smart-move-program car (smart-move-program) = 'smart-move

Theorem: car-delay-program car (delay-program) = 'delay

Event: Disable delay-program.

Theorem: car-computer-move-program car (computer-move-program) = 'computer-move

Theorem: equal-untag-array-tag-array-x-x (untag-array (tag-array (l, x)) = x) = properp (x)

Theorem: properp-replace-value properp (x) → properp (replace-value (x, y, z))

Theorem: properp-bv-to-nat-list properp (bv-to-nat-list (x))

Theorem: properp-nat-to-bv-list properp (nat-to-bv-list (x, ws))

Theorem: properp-computer-move properp (x) → properp (computer-move (x, s))

Theorem: properp-untag-array properp (untag-array (x))

Theorem: properp-tag-array properp (tag-array (l, x))

Theorem: computer-move-implemented ((p0 = p-state (pc,

ctrl-stk,

cons (wa, cons (np, cons (s, temp-stk))), append (cm-prog (word-size), prog-segment), data-segment, max-ctrl-stk-size, max-temp-stk-size, word-size,

              'run))

∧ (p-current-instruction (p0 ) = '(call computer-move)) ∧ computer-move-implemented-input-conditionp (p0 )) → let result be p (p0 ,

computer-move-clock (untag-array (array (car (untag (s)),

data-segment)),

word-size))

in

(p-pc (result) = add1-addr (pc)) ∧ (p-psw (result) = 'run) ∧ (untag-array (array (car (untag (s)), p-data-segment (result))) = computer-move (untag-array (array (car (untag (s)),

data-segment)),

word-size)) endlet

#|
A proof of some constant bounds on the computer-move-clock function
was developed that makes slight use of the proof-checker enhancement of
NQTHM.  For completeness, here is the final theorem of that
digression, with no proof included so that this script is executable
in NQTHM without the enhancement
             (implies (and (nat-listp state ws)
                           (lessp 0 ws)
                           (not (lessp 32 ws))
                           (lessp 1 (length state))
                           (not (lessp 6 (length state))))
                      (and (lessp 10000
                                  (computer-move-clock state ws))
                           (lessp (computer-move-clock state ws)
                                  20000)))
|#

Theorem: nim-piton-space-reasonable 1000 ≮ (nim-piton-ctrl-stk-requirement

+ nim-piton-temp-stk-requirement)

;; bind up defns for presentation purposes

Definition: good-non-empty-nim-statep (state, ws) = (nat-listp (state, ws) ∧ (¬ all-zero-bitvp (state)))

Theorem: valid-movep-computer-move-better good-non-empty-nim-statep (state, ws) → valid-movep (state, computer-move (state, ws))

Theorem: computer-move-works-better (good-non-empty-nim-statep (state, ws) ∧ wsp (state, t)) → (¬ wsp (computer-move (state, ws), t))

;;; An initial p-state to run the program on a particular NIM state, then
;;; enter an infinite loop.

Definition: example2-computer-move-p-state

= p-state ('(pc (main . 0)),
          '((nil (pc (main . 0)))),

nil,

          cons ('(main nil nil
                 (push-constant (addr (arr . 0)))
                 (push-constant (nat 4))
                 (push-constant (addr (arr5 . 0)))
                 (call computer-move)
                 (push-constant (nat 1))
                 (push-constant (addr (flag . 0)))
                 (deposit)
                 (dl loop nil (jump loop))
                 (ret)),

cm-prog (32)),

          '((arr (nat 15) (nat 4) (nat 7) (nat 1))
            (arr5 (nat 3) (nat 4) (nat 2) (nat 1))
            (flag (nat 0))),
          30,
          10,
          32,
          'run)
;;; Extra event that shows that the program is compilable and loadable

;;; onto FM9001, and that the correctness lemma for the Piton interpreter
;;; therefore holds.   (ref: J's e-mail of 10 April 92.)

Theorem: cm-prog-fm9001-loadable let p0 be example2-computer-move-p-state in proper-p-statep (p0 ) ∧ p-loadablep (p0 , 0) ∧ (p-word-size (p0 ) = 32) endlet

;;; Some events written by J Moore that produce an FM9001 image

Definition: pretty-load1 (p0 , offset) = i->m (r->i (p->r (p0 )), nil, offset)

Definition: pretty-vector1 (lst) = if lst ≃ nil then 0

elseif car (lst) then cons (49, pretty-vector1 (cdr (lst)))

else cons (48, pretty-vector1 (cdr (lst))) endif

Definition: pretty-vector (lst) = pack (cons (66, pretty-vector1 (lst)))

Definition: pretty-vector-lst (lst) = if lst ≃ nil then nil

else cons (pretty-vector (car (lst)), pretty-vector-lst (cdr (lst))) endif

Definition: pretty-state (m)

= list ('fm9001-state,

pretty-vector-lst (m-regs (m)), m-c-flg (m), m-v-flg (m), m-n-flg (m), m-z-flg (m), pretty-vector-lst (m-mem (m)))

Definition: pretty-load (p, offset) = pretty-state (pretty-load1 (p, offset))

;; Using pretty-load in r-loop, we produce the following image:
#|

(LIST 'FM9001-STATE
'(B00000000000000000000000000000000 B01001010001000000000000000000000
B01001010001000000000000000000000 B11111010001000000000000000000000
B00000000000000000000000000000000 B00000000000000000000000000000000
B00000000000000000000000000000000 B00000000000000000000000000000000
B00000000000000000000000000000000 B00000000000000000000000000000000
B00000000000000000000000000000000 B00000000000000000000000000000000
B00000000000000000000000000000000 B00000000000000000000000000000000
B00000000000000000000000000000000 B11010000000000000000000000000000)
F F F F
'(B11110000000000000000000000000000 B00100000000000000000000000000000
B11100000000000000000000000000000 B10000000000000000000000000000000
B11000000000000000000000000000000 B00100000000000000000000000000000
B01000000000000000000000000000000 B10000000000000000000000000000000
B00000000000000000000000000000000 B10000000000100010000011111110000
B01000000001000000000011111110000 B11111100001100010000011111110000
B00000000000000000000000000000000 B11111100001100010000011111110000
B00100000000000000000000000000000 B11111100001100010000011111110000
B00100000000000000000000000000000 B11111100000100010000011111110000
B10101000000000000000000000000000 B11111000001111000000011111110000
B10110101110000000000000000000000 B11111100001100010000011111110000
B10000000000000000000000000000000 B11111100001100010000011111110000
B00010000000000000000000000000000 B11001100000010000000011111110000
B11001100000010100000011111110000 B11111000001111000000011111110000
B11011000000000000000000000000000 B11111000001111000000011111110000
B11111000000000000000000000000000 B10000000000100000000011111110000
B01001100001000000000011111110000 B01001100001111000000011111110000
B10000000000100010000011111110000 B01000000001000000000011111110000
B11001100000100010000011111110000 B11001100000100010000011111110000
B11111100000010000000011111110000 B00000000000000000000000000000000
B01000000000010000000011111000000 B00101000001100010000011111110000
B11001100000010000000011111110000 B00101000001100010000011111110000
B11111100000010000000011111110000 B10000000000000000000000000000000
B01000000000010000000011111000000 B00101000001100010000011111110000
B11001000001100100000011110100000 B11111100000010000000011111110000
B10000000000000000000000000000000 B01000000000010000000011111000000
B11001100000010100000011111110000 B11111100000010000000011111110000
B10000000000000000000000000000000 B01000000000010000000011111000000
B00101000001100010000011111110000 B11001100001010001000011111110000
B11111100000010000000011111110000 B00011010000000000000000000000000
B00100000001111000000111011110000 B11111100000010000000011111110000
B10000000000000000000000000000000 B01000000000010000000011111000000
B00101000001100010000011111110000 B11001000001100100000011110100000
B11111100000010000000011111110000 B10000000000000000000000000000000

B01000000000010000000011111000000 B11001100000010100000011111110000
B11111100000010000000011111110000 B00000000000000000000000000000000
B01000000000010000000011111000000 B00101000001100010000011111110000
B11111100001100010000011111110000 B10000000000000000000000000000000
B11001100000010000000011111110000 B00100000001100100000011111000000
B11111100000010000000011111110000 B00000000000000000000000000000000
B01000000000010000000011111000000 B11001000000010100000011111110000
B11001100000010000000011111110000 B00101000001100010000011111110000
B11001100000010000000011111110000 B00100000001100100000011111010000
B11111000001111000000011111110000 B10101100000000000000000000000000
B11111000001111000000011111110000 B01011010000000000000000000000000
B10000000000100000000011111110000 B01001100001000000000011111110000
B01001100001111000000011111110000 B10000000000100010000011111110000
B01000000001000000000011111110000 B11111100001100010000011111110000
B10000000000000000000000000000000 B11111000001111000000011111110000
B11000110000000000000000000000000 B10000000000100000000011111110000
B01001100001000000000011111110000 B01001100001111000000011111110000
B10000000000100010000011111110000 B01000000001000000000011111110000
B11111100000100010000011111110000 B00000000000000000000000000000000
B11111100000100010000011111110000 B00000000000000000000000000000000
B11001100000100010000011111110000 B11111100000100010000011111110000
B10001110000000000000000000000000 B11111000001111000000011111110000
B10111010000000000000000000000000 B11111100000010000000011111110000
B10000000000000000000000000000000 B01000000000010000000011111000000
B11001100000010100000011111110000 B11111100000100010000011111110000
B10011110000000000000000000000000 B11111000001111000000011111110000
B10111010000000000000000000000000 B11001000001100100000011101010000
B11111100000010000000011111110000 B00000000000000000000000000000000
B01000000000010000000011111000000 B00101000001100010000011111110000
B11001100001010001000011111110000 B11111100000010000000011111110000
B01110101000000000000000000000000 B00100000001111000000111011110000
B11111100000010000000011111110000 B00000000000000000000000000000000
B01000000000010000000011111000000 B00101000001100010000011111110000
B11001100000010000001011111110000 B00100000000010000001011101010000
B00100000001100010000011111110000 B11111100001100010000011111110000
B00000000000000000000000000000000 B11111100001100100000100011110000
B10000000000000000000000000000000 B11111100000010000000011111110000
B01000000000000000000000000000000 B01000000000010000000011111000000
B11001100000010100000011111110000 B11111100000010000000011111110000
B00000000000000000000000000000000 B01000000000010000000011111000000
B11001100000010100000011111110000 B11111100000010000000011111110000
B01000000000000000000000000000000 B01000000000010000000011111000000
B00101000001100010000011111110000 B11001100001010001000011111110000
B11111100000010000000011111110000 B11000101000000000000000000000000

B00100000001111000000111011110000 B11111100000010000000011111110000
B10000000000000000000000000000000 B01000000000010000000011111000000
B00101000001100010000011111110000 B11001100000010000000011111110000
B00100000001100100000011111010000 B11111100000010000000011111110000
B10000000000000000000000000000000 B01000000000010000000011111000000
B00101000001100010000011111110000 B11001000001100100000011111000000
B11111100000010000000011111110000 B10000000000000000000000000000000
B01000000000010000000011111000000 B11001100000010100000011111110000
B11111000001111000000011111110000 B01011110000000000000000000000000
B11111000001111000000011111110000 B00001101000000000000000000000000
B10000000000100000000011111110000 B01001100001000000000011111110000
B01001100001111000000011111110000 B10000000000100010000011111110000
B01000000001000000000011111110000 B11111100000100010000011111110000
B00000000000000000000000000000000 B11111100000100010000011111110000
B00000000000000000000000000000000 B11001100000100010000011111110000
B11111100001100010000011111110000 B10000000000000000000000000000000
B11111100000010000000011111110000 B01000000000000000000000000000000
B01000000000010000000011111000000 B11001100000010100000011111110000
B11111100000100010000011111110000 B00100011000000000000000000000000
B11111000001111000000011111110000 B10111010000000000000000000000000
B11111100000010000000011111110000 B10000000000000000000000000000000
B01000000000010000000011111000000 B11001100000010100000011111110000
B11111100001100010000011111110000 B00000000000000000000000000000000
B11111100000010000000011111110000 B00000000000000000000000000000000
B01000000000010000000011111000000 B00101000001100010000011111110000
B11111100000010000000011111110000 B10000000000000000000000000000000
B01000000000010000000011111000000 B00101000001100010000011111110000
B11001100000010000000011111110000 B00100000001100100000011110110000
B11001100001010001000011111110000 B11111100000010000000011111110000
B01111011000000000000000000000000 B00100000001111000000111011110000
B11111100000010000000011111110000 B01000000000000000000000000000000
B01000000000010000000011111000000 B00101000001100010000011111110000
B11001100000010000000011111110000 B00100000001100100000011111000000
B11111100000010000000011111110000 B10000000000000000000000000000000
B01000000000010000000011111000000 B00101000001100010000011111110000
B11001000001100100000011111000000 B11111100000010000000011111110000
B10000000000000000000000000000000 B01000000000010000000011111000000
B11001000000010100000011111110000 B11001100001010001000011111110000
B11111100000010000000011111110000 B01101111000000000000000000000000
B00100000001111000000111011110000 B11111100000010000000011111110000
B01000000000000000000000000000000 B01000000000010000000011111000000
B00101000001100010000011111110000 B11001000001100100000011111000000
B11111100000010000000011111110000 B01000000000000000000000000000000
B01000000000010000000011111000000 B11001100000010100000011111110000

B11111000001111000000011111110000 B01010011000000000000000000000000
B11111000001111000000011111110000 B00011111000000000000000000000000
B10000000000100000000011111110000 B01001100001000000000011111110000
B01001100001111000000011111110000 B10000000000100010000011111110000
B01000000001000000000011111110000 B11111100000100010000011111110000
B00000000000000000000000000000000 B11001100000100010000011111110000
B11001100000100010000011111110000 B11001100000100010000011111110000
B11111100001100010000011111110000 B00000000000000000000000000000000
B11111100000010000000011111110000 B11000000000000000000000000000000
B01000000000010000000011111000000 B11001000000010100000011111110000
B11111100000010000000011111110000 B00000000000000000000000000000000
B01000000000010000000011111000000 B00101000001100010000011111110000
B11001100000010000000011111110000 B00101000001100010000011111110000
B11111100000010000000011111110000 B01000000000000000000000000000000
B01000000000010000000011111000000 B00101000001100010000011111110000
B11001100000010000000011111110000 B00100000001100100001011111100000
B11001000001100100000011111010000 B11111100001100100000100011110000
B10000000000000000000000000000000 B11001100001010001000011111110000
B11111100000010000000011111110000 B00111000100000000000000000000000
B00100000001111000000011011110000 B11001000001100100000011110000000
B11111100000010000000011111110000 B10000000000000000000000000000000
B01000000000010000000011111000000 B00101000001100010000011111110000
B11111100000010000000011111110000 B11000000000000000000000000000000
B01000000000010000000011111000000 B00101000001100010000011111110000
B11001000001100100000011110000000 B11111100000010000000011111110000
B11000000000000000000000000000000 B01000000000010000000011111000000
B11001000000010100000011111110000 B11001100000010000000011111110000
B00100000001100100000011111100000 B11001100001010001000011111110000
B11111100000010000000011111110000 B10111100100000000000000000000000
B00100000001111000000111011110000 B11111100000010000000011111110000
B00000000000000000000000000000000 B01000000000010000000011111000000
B00101000001100010000011111110000 B11111100001100010000011111110000
B10000000000000000000000000000000 B11001100000010000000011111110000
B00100000001100100000011111000000 B11111100000010000000011111110000
B00000000000000000000000000000000 B01000000000010000000011111000000
B11001100000010100000011111110000 B11111000001111000000011111110000
B00010000100000000000000000000000 B11111000001111000000011111110000
B11111100100000000000000000000000 B10000000000100000000011111110000
B01001100001000000000011111110000 B01001100001111000000011111110000
B10000000000100010000011111110000 B01000000001000000000011111110000
B11111100000100010000011111110000 B00000000000000000000000000000000
B11001100000100010000011111110000 B11111100000100010000011111110000
B11010010100000000000000000000000 B11111000001111000000011111110000
B10111010000000000000000000000000 B11111100000010000000011111110000

B10000000000000000000000000000000 B01000000000010000000011111000000
B11001000000010100000011111110000 B11001000001100100000011101010000
B11111100000010000000011111110000 B10000000000000000000000000000000
B01000000000010000000011111000000 B00101000001100010000011111110000
B11001100001010001000011111110000 B11111100000010000000011111110000
B01101110100000000000000000000000 B00100000001111000000111011110000
B11111100000010000000011111110000 B00000000000000000000000000000000
B01000000000010000000011111000000 B00101000001100010000011111110000
B11111100000010000000011111110000 B10000000000000000000000000000000
B01000000000010000000011111000000 B00101000001100010000011111110000
B11001100000010000000011111110000 B00100000001100100000011110110000
B11001100001010001000011111110000 B11111100000010000000011111110000
B11010110100000000000000000000000 B00100000001111000000111011110000
B11001100000010000000011111110000 B11111100000010000000011111110000
B10000000000000000000000000000000 B01000000000010000000011111000000
B00101000001100010000011111110000 B11111100000010000000011111110000
B10000000000000000000000000000000 B01000000000010000000011111000000
B00101000001100010000011111110000 B11001000001100100000011111000000
B11111100000010000000011111110000 B10000000000000000000000000000000
B01000000000010000000011111000000 B11001100000010100000011111110000
B11111000001111000000011111110000 B00001010100000000000000000000000
B11111000001111000000011111110000 B00011110100000000000000000000000
B10000000000100000000011111110000 B01001100001000000000011111110000
B01001100001111000000011111110000 B10000000000100010000011111110000
B01000000001000000000011111110000 B11111100000100010000011111110000
B00000000000000000000000000000000 B11001100000100010000011111110000
B11001100000100010000011111110000 B11001100000100010000011111110000
B11001100000100010000011111110000 B11111100001100010000011111110000
B00000000000000000000000000000000 B11111100000010000000011111110000
B00100000000000000000000000000000 B01000000000010000000011111000000
B11001100000010100000011111110000 B11111100000010000000011111110000
B00000000000000000000000000000000 B01000000000010000000011111000000
B00101000001100010000011111110000 B11001100000010000000011111110000
B00101000001100010000011111110000 B11111100000010000000011111110000
B01000000000000000000000000000000 B01000000000010000000011111000000
B00101000001100010000011111110000 B11001100000010000000011111110000
B00100000001100100000011110110000 B11001100001010001000011111110000
B11111100000010000000011111110000 B10111101100000000000000000000000
B00100000001111000000011011110000 B11111100000010000000011111110000
B00100000000000000000000000000000 B01000000000010000000011111000000
B00101000001100010000011111110000 B11001000001100100000011110000000
B11111100000010000000011111110000 B00100000000000000000000000000000
B01000000000010000000011111000000 B11001000000010100000011111110000
B11111100000010000000011111110000 B10000000000000000000000000000000

B01000000000010000000011111000000 B00101000001100010000011111110000
B11001100000010000000011111110000 B00100000001100100001011111100000
B11001000001100100000011111010000 B11111100001100100000100011110000
B10000000000000000000000000000000 B11001100001010001000011111110000
B11111100000010000000011111110000 B11110011100000000000000000000000
B00100000001111000000111011110000 B11111100000010000000011111110000
B00000000000000000000000000000000 B01000000000010000000011111000000
B00101000001100010000011111110000 B11111100001100010000011111110000
B10000000000000000000000000000000 B11001100000010000000011111110000
B00100000001100100000011111000000 B11111100000010000000011111110000
B00000000000000000000000000000000 B01000000000010000000011111000000
B11001100000010100000011111110000 B11111000001111000000011111110000
B10010001100000000000000000000000 B11111100000010000000011111110000
B00000000000000000000000000000000 B01000000000010000000011111000000
B00101000001100010000011111110000 B11001100000010000000011111110000
B00101000001100010000011111110000 B11111100000010000000011111110000
B11000000000000000000000000000000 B01000000000010000000011111000000
B00101000001100010000011111110000 B11001100000010000000011111110000
B00100000001100100000011111010000 B11111100000010000000011111110000
B00000000000000000000000000000000 B01000000000010000000011111000000
B00101000001100010000011111110000 B11001100000010000000011111110000
B11001100000010100000011111110000 B11111000001111000000011111110000
B10001011100000000000000000000000 B10000000000100000000011111110000
B01001100001000000000011111110000 B01001100001111000000011111110000
B10000000000100010000011111110000 B01000000001000000000011111110000
B11111100000100010000011111110000 B00000000000000000000000000000000
B11001100000100010000011111110000 B11001100000100010000011111110000
B11001100000100010000011111110000 B11111100000010000000011111110000
B00000000000000000000000000000000 B01000000000010000000011111000000
B00101000001100010000011111110000 B11001100000010000000011111110000
B00101000001100010000011111110000 B11111100000100010000011111110000
B10100111100000000000000000000000 B11111000001111000000011111110000
B01100110000000000000000000000000 B11111100000010000000011111110000
B10000000000000000000000000000000 B01000000000010000000011111000000
B00101000001100010000011111110000 B11001100000010000000011111110000
B11001100000010100000011111110000 B11111100000010000000011111110000
B11000000000000000000000000000000 B01000000000010000000011111000000
B00101000001100010000011111110000 B11001000001100100000011110000000
B11111100000010000000011111110000 B11000000000000000000000000000000
B01000000000010000000011111000000 B11001000000010100000011111110000
B11111100000010000000011111110000 B01000000000000000000000000000000
B01000000000010000000011111000000 B00101000001100010000011111110000
B11001100000010000000011111110000 B00100000001100101000011111010000
B11001000001100100000011111010000 B11111100001100100000111011110000

B10000000000000000000000000000000 B11001100001010001000011111110000
B11111100000010000000011111110000 B11011000010000000000000000000000
B00100000001111000000011011110000 B11111100000010000000011111110000
B00000000000000000000000000000000 B01000000000010000000011111000000
B00101000001100010000011111110000 B11111100001100010000011111110000
B10000000000000000000000000000000 B11001100000010000000011111110000
B00100000001100100000011111000000 B11111100000010000000011111110000
B00000000000000000000000000000000 B01000000000010000000011111000000
B11001100000010100000011111110000 B11111100000010000000011111110000
B10000000000000000000000000000000 B01000000000010000000011111000000
B00101000001100010000011111110000 B11111100001100010000011111110000
B10000000000000000000000000000000 B11001100000010000000011111110000
B00100000001100100000011111000000 B11111100000010000000011111110000
B10000000000000000000000000000000 B01000000000010000000011111000000
B11001100000010100000011111110000 B11111000001111000000011111110000
B11011011100000000000000000000000 B11111000001111000000011111110000
B10111000010000000000000000000000 B10000000000100000000011111110000
B01001100001000000000011111110000 B01001100001111000000011111110000
B10000000000100010000011111110000 B01000000001000000000011111110000
B11111100000100010000011111110000 B00000000000000000000000000000000
B11001100000100010000011111110000 B11001100000100010000011111110000
B11001100000100010000011111110000 B11111100000010000000011111110000
B00000000000000000000000000000000 B01000000000010000000011111000000
B00101000001100010000011111110000 B11001100000010000000011111110000
B00101000001100010000011111110000 B11111100000100010000011111110000
B10001100010000000000000000000000 B11111000001111000000011111110000
B11001101000000000000000000000000 B11111100000010000000011111110000
B10000000000000000000000000000000 B01000000000010000000011111000000
B00101000001100010000011111110000 B11001100000010000000011111110000
B11001100000010100000011111110000 B11111100000010000000011111110000
B11000000000000000000000000000000 B01000000000010000000011111000000
B00101000001100010000011111110000 B11001000001100100000011110000000
B11111100000010000000011111110000 B11000000000000000000000000000000
B01000000000010000000011111000000 B11001000000010100000011111110000
B11111100000010000000011111110000 B01000000000000000000000000000000
B01000000000010000000011111000000 B00101000001100010000011111110000
B11001100000010000000011111110000 B00100000001100101000011111010000
B11001000001100100000011111010000 B11111100001100100000111011110000
B10000000000000000000000000000000 B11001100001010001000011111110000
B11111100000010000000011111110000 B11100110010000000000000000000000
B00100000001111000000011011110000 B11111100000010000000011111110000
B10000000000000000000000000000000 B01000000000010000000011111000000
B00101000001100010000011111110000 B11111100001100010000011111110000
B10000000000000000000000000000000 B11001100000010000000011111110000

B00100000001100100000011111000000 B11111100000010000000011111110000
B10000000000000000000000000000000 B01000000000010000000011111000000
B11001100000010100000011111110000 B11111100000010000000011111110000
B00000000000000000000000000000000 B01000000000010000000011111000000
B00101000001100010000011111110000 B11111100001100010000011111110000
B10000000000000000000000000000000 B11001100000010000000011111110000
B00100000001100100000011111000000 B11111100000010000000011111110000
B00000000000000000000000000000000 B01000000000010000000011111000000
B11001100000010100000011111110000 B11111000001111000000011111110000
B11100100010000000000000000000000 B11111000001111000000011111110000
B10010110010000000000000000000000 B10000000000100000000011111110000
B01001100001000000000011111110000 B01001100001111000000011111110000
B10000000000100010000011111110000 B01000000001000000000011111110000
B11111100000100010000011111110000 B00000000000000000000000000000000
B11111100000100010000011111110000 B00000000000000000000000000000000
B11001100000100010000011111110000 B11001100000100010000011111110000
B11111100001100010000011111110000 B00000000000000000000000000000000
B11111100000010000000011111110000 B11000000000000000000000000000000
B01000000000010000000011111000000 B11001000000010100000011111110000
B11111100000010000000011111110000 B11000000000000000000000000000000
B01000000000010000000011111000000 B00101000001100010000011111110000
B11111100000010000000011111110000 B00000000000000000000000000000000
B01000000000010000000011111000000 B00101000001100010000011111110000
B11001100000010000000011111110000 B00101000001100010000011111110000
B11111100000010000000011111110000 B11000000000000000000000000000000
B01000000000010000000011111000000 B11001000000010100000011111110000
B11001100000010000000011111110000 B00100000001100100001011111100000
B11001000001100100000011111010000 B11111100001100100000100011110000
B10000000000000000000000000000000 B11001100001010001000011111110000
B11111100000010000000011111110000 B01101001010000000000000000000000
B00100000001111000000111011110000 B11001100000010000000011111110000
B11111100000010000000011111110000 B11000000000000000000000000000000
B01000000000010000000011111000000 B00101000001100010000011111110000
B11111100000010000000011111110000 B01000000000000000000000000000000
B01000000000010000000011111000000 B00101000001100010000011111110000
B11001000001100100000011110000000 B11111100000010000000011111110000
B01000000000000000000000000000000 B01000000000010000000011111000000
B11001000000010100000011111110000 B11111100000010000000011111110000
B10000000000000000000000000000000 B01000000000010000000011111000000
B00101000001100010000011111110000 B11001100000010000000011111110000
B00100000001100101000011111010000 B11001000001100100000011111010000
B11111100001100100000111011110000 B10000000000000000000000000000000
B11001100001010001000011111110000 B11111100000010000000011111110000
B01011101010000000000000000000000 B00100000001111000000011011110000

B11111100000010000000011111110000 B00000000000000000000000000000000
B01000000000010000000011111000000 B00101000001100010000011111110000
B11111100001100010000011111110000 B10000000000000000000000000000000
B11001100000010000000011111110000 B00100000001100100000011111000000
B11111100000010000000011111110000 B00000000000000000000000000000000
B01000000000010000000011111000000 B11001100000010100000011111110000
B11111000001111000000011111110000 B01101110010000000000000000000000
B11111000001111000000011111110000 B00111101010000000000000000000000
B10000000000100000000011111110000 B01001100001000000000011111110000
B01001100001111000000011111110000 B10000000000100010000011111110000
B01000000001000000000011111110000 B11001100000100010000011111110000
B11001100000100010000011111110000 B11001100000100010000011111110000
B11111100000010000000011111110000 B00000000000000000000000000000000
B01000000000010000000011111000000 B00101000001100010000011111110000
B11001100000010000000011111110000 B00101000001100010000011111110000
B11111100000010000000011111110000 B10000000000000000000000000000000
B01000000000010000000011111000000 B00101000001100010000011111110000
B11001100000010000000011111110000 B00100000001100101000011111010000
B11001000001100100000011111010000 B11111100001100100000111011110000
B10000000000000000000000000000000 B11001100001010001000011111110000
B11111100000010000000011111110000 B10100111010000000000000000000000
B00100000001111000000011011110000 B11111100000010000000011111110000
B00000000000000000000000000000000 B01000000000010000000011111000000
B00101000001100010000011111110000 B11111100001100010000011111110000
B10000000000000000000000000000000 B11001100000010000000011111110000
B00100000001100100000011111000000 B11111100000010000000011111110000
B00000000000000000000000000000000 B01000000000010000000011111000000
B11001100000010100000011111110000 B11111000001111000000011111110000
B00100011010000000000000000000000 B11111100000010000000011111110000
B01000000000000000000000000000000 B01000000000010000000011111000000
B00101000001100010000011111110000 B11111100000010000000011111110000
B00000000000000000000000000000000 B01000000000010000000011111000000
B00101000001100010000011111110000 B11001100000010000000011111110000
B11001100000010100000011111110000 B11111000001111000000011111110000
B10001111010000000000000000000000 B10000000000100000000011111110000
B01001100001000000000011111110000 B01001100001111000000011111110000
B10000000000100010000011111110000 B01000000001000000000011111110000
B11111100000100010000011111110000 B00000000000000000000000000000000
B11001100000100010000011111110000 B11001100000100010000011111110000
B11001100000100010000011111110000 B11111100000010000000011111110000
B00000000000000000000000000000000 B01000000000010000000011111000000
B00101000001100010000011111110000 B11111100000010000000011111110000
B10000000000000000000000000000000 B01000000000010000000011111000000
B00101000001100010000011111110000 B11111100001100010000011111110000

B01000000000000000000000000000000 B11111100000100010000011111110000
B10010000110000000000000000000000 B11111000001111000000011111110000
B11011111000000000000000000000000 B11111100001100010000011111110000
B01000000000000000000000000000000 B11001100000010000000011111110000
B00100000001100100001011111100000 B11001000001100100000011111010000
B11111100001100100000100011110000 B10000000000000000000000000000000
B11001100001010001000011111110000 B11111100000010000000011111110000
B01011010110000000000000000000000 B00100000001111000000011011110000
B11111100000010000000011111110000 B00000000000000000000000000000000
B01000000000010000000011111000000 B00101000001100010000011111110000
B11111100000010000000011111110000 B01000000000000000000000000000000
B01000000000010000000011111000000 B00101000001100010000011111110000
B11111100000010000000011111110000 B10000000000000000000000000000000
B01000000000010000000011111000000 B00101000001100010000011111110000
B11111100000100010000011111110000 B00100100110000000000000000000000
B11111000001111000000011111110000 B00101011100000000000000000000000
B11111100000010000000011111110000 B01000000000000000000000000000000
B01000000000010000000011111000000 B00101000001100010000011111110000
B11111100000010000000011111110000 B10000000000000000000000000000000
B01000000000010000000011111000000 B00101000001100010000011111110000
B11111100000010000000011111110000 B01000000000000000000000000000000
B01000000000010000000011111000000 B00101000001100010000011111110000
B11111100000010000000011111110000 B10000000000000000000000000000000
B01000000000010000000011111000000 B00101000001100010000011111110000
B11111100000100010000011111110000 B00011100110000000000000000000000
B11111000001111000000011111110000 B01000100000000000000000000000000
B11111100000010000000011111110000 B11000000000000000000000000000000
B01000000000010000000011111000000 B11001000000010100000011111110000
B11111100000100010000011111110000 B00000010110000000000000000000000
B11111000001111000000011111110000 B01000010100000000000000000000000
B11111100000010000000011111110000 B11000000000000000000000000000000
B01000000000010000000011111000000 B00101000001100010000011111110000
B11111100000100010000011111110000 B00010010110000000000000000000000
B11111000001111000000011111110000 B11011110100000000000000000000000
B11111100000010000000011111110000 B01000000000000000000000000000000
B01000000000010000000011111000000 B00101000001100010000011111110000
B11111100000010000000011111110000 B00000000000000000000000000000000
B01000000000010000000011111000000 B00101000001100010000011111110000
B11111100000010000000011111110000 B10000000000000000000000000000000
B01000000000010000000011111000000 B00101000001100010000011111110000
B11111100000100010000011111110000 B00011010110000000000000000000000
B11111000001111000000011111110000 B00000100010000000000000000000000
B11111000001111000000011111110000 B01110001110000000000000000000000
B11111100000010000000011111110000 B00000000000000000000000000000000

B01000000000010000000011111000000 B00101000001100010000011111110000
B11111100000010000000011111110000 B00000000000000000000000000000000
B01000000000010000000011111000000 B00101000001100010000011111110000
B11111100000010000000011111110000 B10000000000000000000000000000000
B01000000000010000000011111000000 B00101000001100010000011111110000
B11111100000100010000011111110000 B01010110110000000000000000000000
B11111000001111000000011111110000 B00110110010000000000000000000000
B11111100000010000000011111110000 B00000000000000000000000000000000
B01000000000010000000011111000000 B00101000001100010000011111110000
B11111100000010000000011111110000 B10000000000000000000000000000000
B01000000000010000000011111000000 B00101000001100010000011111110000
B11111100001100010000011111110000 B10000000000000000000000000000000
B11111100000100010000011111110000 B00011110110000000000000000000000
B11111000001111000000011111110000 B11011111000000000000000000000000
B11001100000010000001011111110000 B00100000000010000001011101010000
B00100000001100010000011111110000 B11111100001100010000011111110000
B00000000000000000000000000000000 B11111100001100100000100011110000
B10000000000000000000000000000000 B11111100000010000000011111110000
B11000000000000000000000000000000 B01000000000010000000011111000000
B11001100000010100000011111110000 B11001100000010000000011111110000
B11111100000010000000011111110000 B11000000000000000000000000000000
B01000000000010000000011111000000 B00101000001100010000011111110000
B11111100000100010000011111110000 B00110001110000000000000000000000
B11111000001111000000011111110000 B11111101010000000000000000000000
B11111000001111000000011111110000 B01110001110000000000000000000000
B10000000000100000000011111110000 B01001100001000000000011111110000
B01001100001111000000011111110000 B10000000000100010000011111110000
B01000000001000000000011111110000 B11001100000100010000011111110000
B11111100000010000000011111110000 B00000000000000000000000000000000
B01000000000010000000011111000000 B00101000001100010000011111110000
B11001000001100100000011110100000 B11111100000010000000011111110000
B00000000000000000000000000000000 B01000000000010000000011111000000
B11001000000010100000011111110000 B00100000000010000000011111110000
B00100000000010000000011111110000 B00100000000010000000011111110000
B00100000000010000000011111110000 B11001100001010001000011111110000
B11111100000010000000011111110000 B00010101110000000000000000000000
B00100000001111000000111011110000 B00100000000010000000011111110000
B11111000001111000000011111110000 B00101001110000000000000000000000
B11111000001111000000011111110000 B01010101110000000000000000000000
B10000000000100000000011111110000 B01001100001000000000011111110000
B01001100001111000000011111110000 B10000000000100010000011111110000
B01000000001000000000011111110000 B11111100000100010000011111110000
B00000000000000000000000000000000 B11001100000100010000011111110000
B11001100000100010000011111110000 B11001100000100010000011111110000

B11111100001100010000011111110000 B01011111000000000000000000000000
B11111100000100010000011111110000 B01011101110000000000000000000000
B11111000001111000000011111110000 B10001001110000000000000000000000
B11111100001100010000011111110000 B01011111000000000000000000000000
B11111100000100010000011111110000 B00000011110000000000000000000000
B11111000001111000000011111110000 B10001001110000000000000000000000
B11111100001100010000011111110000 B01011111000000000000000000000000
B11111100000100010000011111110000 B01100011110000000000000000000000
B11111000001111000000011111110000 B10001001110000000000000000000000
B11111100001100010000011111110000 B01011111000000000000000000000000
B11111100000100010000011111110000 B00110011110000000000000000000000
B11111000001111000000011111110000 B10001001110000000000000000000000
B11111100000010000000011111110000 B00000000000000000000000000000000
B01000000000010000000011111000000 B00101000001100010000011111110000
B11111100000010000000011111110000 B10000000000000000000000000000000
B01000000000010000000011111000000 B00101000001100010000011111110000
B11111100001100010000011111110000 B01000000000000000000000000000000
B11111100000100010000011111110000 B01011011110000000000000000000000
B11111000001111000000011111110000 B11011111000000000000000000000000
B11001100001010001000011111110000 B11111100000010000000011111110000
B00001000001000000000000000000000 B00100000001111000000111011110000
B11111100000010000000011111110000 B00000000000000000000000000000000
B01000000000010000000011111000000 B00101000001100010000011111110000
B11111100000010000000011111110000 B01000000000000000000000000000000
B01000000000010000000011111000000 B00101000001100010000011111110000
B11111100000010000000011111110000 B10000000000000000000000000000000
B01000000000010000000011111000000 B00101000001100010000011111110000
B11111100000100010000011111110000 B01110111110000000000000000000000
B11111000001111000000011111110000 B00101011100000000000000000000000
B11111100000010000000011111110000 B01000000000000000000000000000000
B01000000000010000000011111000000 B00101000001100010000011111110000
B11111100000010000000011111110000 B10000000000000000000000000000000
B01000000000010000000011111000000 B00101000001100010000011111110000
B11111100000100010000011111110000 B01011111110000000000000000000000
B11111000001111000000011111110000 B01000100000000000000000000000000
B11001100001010001000011111110000 B11111100000010000000011111110000
B00001000001000000000000000000000 B00100000001111000000111011110000
B11111100000010000000011111110000 B00000000000000000000000000000000
B01000000000010000000011111000000 B00101000001100010000011111110000
B11111100000010000000011111110000 B10000000000000000000000000000000
B01000000000010000000011111000000 B00101000001100010000011111110000
B11111100000010000000011111110000 B01000000000000000000000000000000
B01000000000010000000011111000000 B00101000001100010000011111110000
B11111100000100010000011111110000 B01110000001000000000000000000000

B11111000001111000000011111110000 B00101111010000000000000000000000
B11111000001111000000011111110000 B11001100001000000000000000000000
B11111100000010000000011111110000 B00000000000000000000000000000000
B01000000000010000000011111000000 B00101000001100010000011111110000
B11111100000010000000011111110000 B00000000000000000000000000000000
B01000000000010000000011111000000 B00101000001100010000011111110000
B11111100000010000000011111110000 B10000000000000000000000000000000
B01000000000010000000011111000000 B00101000001100010000011111110000
B11111100000100010000011111110000 B00000100001000000000000000000000
B11111000001111000000011111110000 B00110110010000000000000000000000
B11111100000010000000011111110000 B11000000000000000000000000000000
B01000000000010000000011111000000 B11001100000010100000011111110000
B11111100000010000000011111110000 B11000000000000000000000000000000
B01000000000010000000011111000000 B00101000001100010000011111110000
B11111100000010000000011111110000 B11000000000000000000000000000000
B01000000000010000000011111000000 B00101000001100010000011111110000
B11001000001100100000011110100000 B11111100000100010000011111110000
B10001100001000000000000000000000 B11111000001111000000011111110000
B11111101010000000000000000000000 B11111000001111000000011111110000
B11001100001000000000000000000000 B10000000000100000000011111110000
B01001100001000000000011111110000 B01001100001111000000011111110000
B00000000000000000000000000000000 B00000000000000000000000000000000
B00000000000000000000000000000000 B00000000000000000000000000000000
B00000000000000000000000000000000 B00000000000000000000000000000000
B00000000000000000000000000000000 B00000000000000000000000000000000
B00000000000000000000000000000000 B00000000000000000000000000000000
B00000000000000000000000000000000 B00000000000000000000000000000000
B00000000000000000000000000000000 B00000000000000000000000000000000
B00000000000000000000000000000000 B00000000000000000000000000000000
B00000000000000000000000000000000 B00000000000000000000000000000000
B00000000000000000000000000000000 B00000000000000000000000000000000
B00000000000000000000000000000000 B00000000000000000000000000000000
B00000000000000000000000000000000 B00000000000000000000000000000000
B00000000000000000000000000000000 B00000000000000000000000000000000
B00000000000000000000000000000000 B00000000000000000000000000000000
B01001010001000000000000000000000 B11010000000000000000000000000000
B00000000000000000000000000000000 B00000000000000000000000000000000
B00000000000000000000000000000000 B00000000000000000000000000000000
B00000000000000000000000000000000 B00000000000000000000000000000000
B00000000000000000000000000000000 B00000000000000000000000000000000
B00000000000000000000000000000000 B00000000000000000000000000000000
B00000000000000000000000000000000 B00000000000000000000000000000000
B01101100001000000000000000000000 B10101010001000000000000000000000
B11111010001000000000000000000000))

|#
;;  This image above executed on a fabricated FM9001 in a test jig at Indiana
;;  University with the help of M. Esen Tuna, Bhaskar Bose, and Steve Johnson.
;;  The resulting state that begins with the following:
#|
(2  4  7  1
2  4  7  1
1  266373121  266339330  266374207
0  266374207  4  266374207
4  266373183  21  266353695
941  266374207  1  266374207
8  266342451  266358835  266353695
27  266353695  31  266340353
266339378  266353714  266373121  266339330
266373171  266373171  266342463  0
65015810  266374164  266342451  266374164
266342463  1  65015810  266374164
98585619  266342463  1  65015810
266358835  266342463  1  65015810
266374164  266409011  266342463  88
259013636  266342463  1  65015810
266374164  98585619  266342463  1
65015810  266358835  266342463  0
....

Note that the Nim state beginning in location 0 of 15 4 7 1 has been
transformed into 2 4 7 1, which by proof we know is an optimal move.
|#

Index

add1-addr, 14, 15, 18, 22, 27, 33, 39, 44, 53, 62, 71, 77, 82, 84, 87, 96, 99, 106, 130

addition-on, 3 all-but-last, 21, 24–26, 34, 35, 47,

56, 68, 114, 116 all-but-last-nat-to-bv, 116 all-but-last-one-bit-vector, 21 all-but-last-xor-bitv, 26 all-ones-vector, 115, 116 all-valid-moves, 107–110, 117, 125 all-valid-moves-helper, 107, 108, 110,

117, 124, 125 all-zero-bitvp, 23–26, 29–31, 34–37,

46–52, 55, 102, 103, 105, 106, 108–111, 114, 117, 119, 121, 123, 125–127, 131

all-zero-bitvp-all-but-last-mea ns, 35 ns-spec, 35

all-zero-bitvp-all-but-last-nat

-to-bv, 114 all-zero-bitvp-all-but-last-simp

le, 47 all-zero-bitvp-and-bitv, 31 all-zero-bitvp-and-bitv-append, 48 all-zero-bitvp-and-match-member, 123 all-zero-bitvp-append, 24 all-zero-bitvp-make-list-from-si

mple, 109 all-zero-bitvp-max-list, 126 all-zero-bitvp-means-at-most-one

-bit-on, 25 all-zero-bitvp-nat-to-bv, 111 all-zero-bitvp-one-bit-vector, 52 all-zero-bitvp-xor-bitv-better, 111 all-zero-bitvp-xor-bvs-nat-to-bv

-list-zeros, 109 all-zero-bitvp-zero-bit-vector, 23 all-zero-means-to-and-bitv, 35 and-bitv, 23, 30, 31, 35–37, 46–48,

50, 55, 109, 117, 123 and-bitv-append, 47 and-bitv-append2, 48 and-bitv-special, 36 and-bitv-special-3, 37 and-bitv-special-4, 37 and-bitv-special-5, 37 and-bitv-special-6, 37 and-bitv-special-special, 37 append-all-but-last-last, 56 append-make-list-from-cons-cdr, 85 append-make-list-from-cons-get-

hack, 58 append-make-list-from-put-hack, 59 append-zeros-0, 51 array, 6–10, 14–16, 41–45, 59–62, 69–

71, 74–77, 80–82, 85–87, 95, 96, 103–105, 127, 130

array-pitonp, 64, 66–70, 74, 75, 94,

95, 104, 127 array-pitonp-add1, 66 array-pitonp-append, 66 array-pitonp-from-nat-list-pito

n, 94 array-pitonp-means-properp, 68 array-pitonp-put, 68 array-pitonp-tag-array, 66 assoc-put-assoc-better, 65 associativity-of-and-bitv, 31 at-least-morep, 5, 7–9, 20, 21, 32,

33, 42, 44, 48, 52, 59, 61, 68, 70, 73, 75, 80, 81, 85, 86, 95, 98, 99, 103, 127

at-least-morep-linear, 5 at-least-morep-normalize, 5 at-most-one-bit-is-all-zeros, 47 at-most-one-bit-on, 25, 26, 32, 34,

36–38, 47–51 at-most-one-bit-on-append, 25 at-most-one-bit-on-cdr, 47 at-most-one-bit-on-one-bit-vect

or, 26

bit-vectorp, 6, 8, 10–14, 20, 21, 23, 24, 26, 31–38, 46–52, 56– 59, 61, 94, 111, 119, 122, 123

bit-vectorp-and-bitv-better, 31 bit-vectorp-append, 20 bit-vectorp-append-better, 33 bit-vectorp-append-cdr-hack, 50 bit-vectorp-cdr-from-free, 51 bit-vectorp-fix-bitv, 123 bit-vectorp-from-bit-vectors-pit

on, 14 bit-vectorp-get, 11 bit-vectorp-hack, 34 bit-vectorp-highest-bit, 94 bit-vectorp-highest-bit-xor-bvs, 119 bit-vectorp-induct, 12 bit-vectorp-last, 56 bit-vectorp-make-list-from, 35 bit-vectorp-means-properp, 36 bit-vectorp-nat-to-bv, 111 bit-vectorp-one-bit-vector, 21 bit-vectorp-one-bit-vector-rewrite, 38 bit-vectorp-plus-length-hack, 37 bit-vectorp-simple-not, 46 bit-vectorp-trailing-zeros, 36 bit-vectorp-xor-bitv2, 12 bit-vectorp-xor-bvs, 12 bit-vectorp-xor-bvs-nat-to-bv-li

st, 94 bit-vectorp-zero-bit-vector, 21 bit-vectorp-zero-bit-vector-bette

r, 48 bit-vectors-piton, 6–14, 55–59, 61,

74, 75, 94 bit-vectors-piton-free-means, 55 bit-vectors-piton-means, 8 bit-vectors-piton-means-car, 57 bit-vectors-piton-means-get-cdr, 58 bit-vectors-piton-means-last, 56 bit-vectors-piton-means-more, 10 bit-vectors-piton-means-properp, 56 bit-vectors-piton-nthcdr, 58 bit-vectors-piton-tag-array, 94 bit-vectorsp, 12, 93, 94, 110, 111, 117–119, 123, 126

bit-vectorsp-cdr-untag, 12 bit-vectorsp-match-and-xor, 93 bit-vectorsp-nat-to-bv-list, 93 bit-vectorsp-nat-to-bv-list-bette

r, 119 bit-vectorsp-nthcdr, 12 bit-vectorsp-remove-highest-bit

s, 118 s2, 123

bit-vectorsp-untag, 12 bv-length-weaker, 38 bv-to-nat, 22, 23, 26, 31, 32, 34, 35, 37–39, 75, 119, 122

bv-to-nat-all-but-last, 34 bv-to-nat-all-zero-bitvp, 26 bv-to-nat-append, 23 bv-to-nat-clock, 32, 33, 39, 74 bv-to-nat-induct, 30 bv-to-nat-input-conditionp, 32, 33,

39 bv-to-nat-list, 75–77, 90, 93, 119, 122, 126, 129 bv-to-nat-list-clock, 76, 77 bv-to-nat-list-input-conditionp, 73, 77 bv-to-nat-list-loop-clock, 74, 76 bv-to-nat-list-loop-induct, 75 bv-to-nat-list-nat-to-bv-list, 93 bv-to-nat-list-program, 72, 73, 75,

89, 95, 101, 104, 128, 129 bv-to-nat-loop-clock, 30–32 bv-to-nat-loop-clock-open, 31 bv-to-nat-make-list-from-from-s ub1-make-list-from, 35

bv-to-nat-nat-to-bv, 22 bv-to-nat-one-bit, 34 bv-to-nat-one-bit-vector, 23 bv-to-nat-program, 28, 32, 33, 39,

73–75, 89, 96, 101, 105, 128 bv-to-nat-xor-bitv, 23 bv-to-nat2, 30, 33, 38 bv-to-nat2-bv-to-nat, 38 bv-to-nat2-bv-to-nat-helper, 38 bv-to-nat2-helper, 30–32, 38 bv-to-nat2-helper-bv-to-nat, 38 bv-to-nat2-helper-bv-to-nat-bette

r, 38 bv-to-nat2-helper-hack, 31 bv-to-nat2-helper-hack2, 31

car-append-better, 50 car-bv-to-nat-list-program, 129 car-bv-to-nat-program, 128 car-computer-move-program, 129 car-delay-program, 129 car-highest-bit-program, 128 car-match-and-xor-program, 129 car-max-nat-program, 129 car-nat-to-bv-list, 116 car-nat-to-bv-list-program, 129 car-nat-to-bv-program, 128 car-nthcdr, 57 car-number-with-at-least-progra

m, 128 car-push-1-vector-program, 128 car-remove-highest-bits, 117 car-replace-value-program, 129 car-smart-move-program, 129 car-untag-array, 57 car-xor-bitv, 118 car-xor-bvs-program, 128 cdr-nthcdr-cons, 124 cdr-untag-array-nthcdr, 58 cdr-zero-one-bit-vector, 52 clock-plus, 4, 64, 70, 74, 76, 79, 81,

84, 86 clock-plus-0, 4 clock-plus-add1, 4 clock-plus-function, 4 cm-prog, 128, 130, 131 cm-prog-fm9001-loadable, 132 commutativity2-of-and-bitv, 31 computer-move, 102, 106, 121, 123,

126, 129–131 computer-move-clock, 106, 130 computer-move-implemented, 130 computer-move-implemented-input -conditionp, 127, 130

computer-move-input-conditionp, 103,

105 computer-move-makes-non-green, 121 computer-move-makes-non-green-re

write, 121 computer-move-program, 100, 101, 104, 128, 129 computer-move-works, 126 computer-move-works-better, 131 cons-0-zero-bit-vector, 52 cons-car-x-put-append-make-list

-from-hack, 68 cons-n-assoc-n, 57 cons-n-assoc-n-hack, 57 cons-n-cadr-list-assoc-n, 57 correctness-of-bv-to-nat, 39 correctness-of-bv-to-nat-genera

l, 32 correctness-of-bv-to-nat-helper, 33 correctness-of-bv-to-nat-list, 77 correctness-of-bv-to-nat-list-ge

neral, 75 correctness-of-computer-move, 105 correctness-of-delay, 99 correctness-of-delay-general, 98 correctness-of-highest-bit, 53 correctness-of-match-and-xor, 61 correctness-of-match-and-xor-ge

neral, 59 correctness-of-max-nat, 82 correctness-of-max-nat-general, 80 correctness-of-nat-to-bv, 27 correctness-of-nat-to-bv-genera

l, 20

l-induct, 19, 20 correctness-of-nat-to-bv-helper, 21 correctness-of-nat-to-bv-list, 71 correctness-of-nat-to-bv-list-ge

neral, 68 correctness-of-number-with-at-le

ast, 44 correctness-of-push-1-vector, 17 correctness-of-replace-value, 87 correctness-of-replace-value-ge

neral, 85 correctness-of-smart-move, 96 correctness-of-xor-bvs, 15 correctness-of-xor-bvs-helper, 13

definedp, 7–9, 42, 44, 57–59, 61, 65, 69, 70, 74, 75, 80, 81, 85, 86, 95, 104, 127

definition, 8, 9, 14, 15, 18, 20, 22, 27, 32, 33, 39, 42, 44, 48, 52, 59, 61, 68–70, 73–75, 80, 81, 85, 86, 98, 99

delay-clock, 99 delay-input-conditionp, 99 delay-loop-clock, 98, 99 delay-program, 97–99, 101, 104, 128,

129 difference-x-sub1-x-better, 9 different-lengths-hack, 115 different-lengths-means-differe

nt, 114 nt-hack, 114

different-lengths-obvious, 115 double-cdr-induct, 24 double-cdr-with-sub1-induct, 31 double-sub1-cdr, 112

equal-add1-length, 42 equal-add1-plus-hack, 37 equal-all-ones-nat-to-bv, 116 equal-all-ones-vector-all-ones-ve

ctor, 115 equal-all-ones-vector-cons, 115 equal-all-ones-vector-nlistp, 115 equal-append-2, 124 equal-append-a-append-a, 68 equal-append-zero-bit-vector-ze

ro-bit-vector, 58 equal-assoc-cons, 17 equal-bv-to-nat-0, 31 equal-bv-to-nat-0-2, 35 equal-bv-to-nat-1, 35 equal-car-highest-bit-1, 117 equal-cons-make-properp, 125 equal-cons-zero-bit-vector-nat-t

o-bv, 115 equal-difference, 115 equal-difference-1, 41 equal-exp, 115 equal-exp-x-y-x, 93 equal-highest-bit-cons-1, 118 equal-last-xor-bvs-1, 116 equal-nat-to-bv, 23 equal-nat-to-bv-nat-to-bv, 116 equal-nat-to-bv-nlistp, 114 equal-nil-cdr-tag-array-hack, 67 equal-nil-nthcdr-length, 58 equal-nthcdr-cons, 124 equal-nthcdr-cons-better, 125 equal-one-bit-vector, 47 equal-plus-times-hack, 34 equal-plus-times-hack2, 37 equal-put-assoc, 58 equal-remainder-add1, 121 equal-remainder-add1-2, 121 equal-sub1-add1, 93 equal-times-x-x, 93 equal-trailing-zeros-acc-irrelev

ant, 47 equal-trailing-zeros-helper-0, 30 equal-trailing-zeros-length, 36 equal-trailing-zeros-length-spe

c, 36 equal-untag-array-tag-array-x-x, 129 equal-x-put-assoc-x, 57 equal-x-remainder-sub1-x, 121 equal-x-zero-bit-vector, 47 equal-xor-bitv-x-x, 11 equal-xor-bitv-x-x-special, 13 equal-xor-bitv-x-y-1, 24 equal-xor-bitv-x-y-2, 24 example-bv-to-nat-list-p-state, 73 example-bv-to-nat-state, 28 example-computer-move-p-state, 101 example-delay-p-state, 97 example-highest-bit-state, 45 example-match-and-xor-p-state, 54 example-max-nat-p-state, 78 example-nat-to-bv-list-p-state, 63 example-nat-to-bv-state, 19 example-number-with-at-least-st

ate, 40 example-push-1-vector-state, 17 example-replace-value-p-state, 83 example-smart-move-p-state, 89 example-xor-bvs-p-state, 16 example2-computer-move-p-state, 131,

132 exp, 5, 7–10, 20–23, 26, 27, 31, 34,

36, 41–44, 59, 61, 64–67, 69, 70, 74, 76, 80, 82, 84, 85, 87, 93, 95, 98, 99, 104, 105, 110, 113–117, 122, 126, 127

exp-0, 10 exponentiation-on, 3

fix-bit, 13, 22, 35, 37, 122 fix-bitv, 25, 26, 109, 111, 112, 114,

118, 122, 123 fix-bitv-all-but-last, 26 fix-bitv-and-bitv, 109 fix-bitv-highest-bit, 122 fix-bitv-make-list-from, 112 fix-bitv-nat-to-bv, 111 fix-bitv-one-bit-vector, 114 fix-bitv-xor-bitv, 109 fix-bitv-xor-bvs, 109 fix-bitv-zero-bit-vector, 111 fix-clock-plus, 4

gcds-on, 4 get, 7, 8, 11, 13, 14, 41, 42, 56–58,

64, 65, 67, 74, 75, 79, 80, 84, 85, 125

get-0-better, 65 get-add1, 65 get-as-nth, 125 get-length-cdr, 56 get-nlistp-better, 58 get-untag-array, 13 good-non-empty-nim-statep, 131 green-in-list-all-valid-moves, 125 green-in-list-all-valid-moves-he

lper, 116 green-in-list-all-valid-moves-me

ans, 117 green-means-non-green-in-valid-

moves, 125 green-statep, 109, 116, 117, 121, 125,

126 green-statep-all-zero-bitvp, 126

highest-bit, 46, 52, 53, 90, 94, 117–

119, 122, 123 highest-bit-clock, 52, 53 highest-bit-correctness-general, 48 highest-bit-induct, 46 highest-bit-input-conditionp, 52, 53 highest-bit-loop-clock, 46, 49, 52 highest-bit-program, 45, 46, 48, 52,

89, 96, 101, 104, 128 highest-bit2-helper, 47, 49–52 highest-bit2-helper-cons-0, 50 highest-bit2-helper-cons-0-rewrite, 50 highest-bit2-helper-cons-1, 49 highest-bit2-helper-cons-helper, 51

-rewrite, 51 highest-bit2-helper-highest-bit, 52 highest-bits-induct, 118

i->m, 132

last, 29, 30, 34, 35, 37, 38, 47, 56,

65, 80, 113, 114, 116 last-append, 38 last-make-list-from, 34 last-nat-to-bv, 113 last-one-bit-vector, 113 last-xor-bitv, 113 last-zero-bit-vector, 114 least-bit-higher-all-but-last, 25 least-bit-higher-cdr-all-but-la

st, 26 least-bit-higher-cons-xor-bitv-

hack, 26 least-bit-higher-means-and-0, 23 least-bit-higher-than-high-bit, 23–26 least-bit-higher-than-high-bit-

append-0s, 24 simple, 24 simple2, 26

least-bit-higher-x-all-but-last

-x, 26 length, 7–14, 17, 20–24, 26, 27, 29–

38, 41–44, 46–52, 55–59, 61, 63, 64, 66–70, 73–75, 79– 81, 84–86, 93–95, 98, 99, 103, 104, 108–111, 113–115, 117–119, 122–125, 127

length-all-ones-vector, 115 length-cadar-bvs, 14 length-cadr-get-bit-vectors-pit

on, 11 length-cdr-nat-to-bv-list, 66 length-cdr-nlistp, 67 length-cdr-tag-array, 66 length-cdr-untag-array, 42 length-cdr-xor-bitv, 118 length-cdr-xor-bvs, 118 length-cdr-zero-bit-vector, 48 length-fix-bitv, 118 length-from-array-pitonp, 67 length-from-bit-vectorp, 11 length-highest-bit, 46 length-make-list-from, 24 length-match-and-xor, 94 length-match-member, 123 length-match-member-nat-to-bv-li

st, 123 length-nat-to-bv, 22 length-nat-to-bv-list, 66 length-nthcdr, 48 length-one-bit-vector, 27 length-put-better, 68 length-tag-array, 66 length-untag-array, 12 length-xor-bitv, 11 length-xor-bvs, 12 length-xor-bvs-nat-to-bv-list, 111 length-xor-bvs2, 110 length-zero-bit-vector, 26 lessp-0-length-better, 58 lessp-1, 20 lessp-1-exp, 8 lessp-1-hack, 35 lessp-as-at-least-morep, 5 lessp-as-lessp-bv, 122 lessp-bv, 122, 123 lessp-bv-to-nat, 122 lessp-bv-to-nat-exp, 31 lessp-bv-to-nat-exp-2, 23 lessp-bv-xor-bitv, 123 lessp-difference-arg1, 115 lessp-exp-2-8-hack, 105 lessp-exp-simple, 20 lessp-length-cdr-trailing, 30 lessp-length-simple-member-all-v

alid-moves, 124 lessp-length-trailing-zeros-hac

k, 30 lessp-max-list, 120 lessp-max-list-from-nat-listp, 126 lessp-max-list-from-number-with

-at-least, 120 lessp-max-sum-all-valid-moves, 108 lessp-max-sum-helper, 108 lessp-number-with-at-least, 93 lessp-plus-hacks, 23 lessp-remainder-simple, 20 lessp-remainder-x-exp-x, 20 lessp-sub1-as-equal, 125 lessp-sub1-plus-hack, 34 lessp-sub1-plus-sub1-hack, 115 lessp-sum-max-sum, 108 lessp-trailing-zeros, 47 lessp-trailing-zeros-helper, 29 list-bitv-cadr-bitvp, 57 list-nat-cadr-get-hack, 85 list-nat-from-assoc-nat-list-pit

on-hack, 80 listp-all-valid-move, 110 listp-all-valid-move-helper, 110 listp-cdr-assoc-hack-from-free, 94 listp-cdr-nthcdr, 55 listp-cdr-untag-array, 56 listp-highest-bit, 46 listp-make-list-from, 24 listp-nat-to-bv, 113 listp-nat-to-bv-list, 66 listp-replace-value, 120 listp-tag-array, 66 listp-untag-array, 14 listp-xor-bitv, 25 listp-xor-bvs, 116 listp-zero-bit-vector, 47 logs-on, 4

m-c-flg, 132 m-mem, 132 m-n-flg, 132 m-regs, 132 m-v-flg, 132 m-z-flg, 132 make-list-from, 24, 34–36, 38, 47–

49, 58–60, 64, 68, 69, 75, 76, 85, 86, 109, 111–113, 124, 125

make-list-from-1, 24 make-list-from-append, 124 make-list-from-cons, 34 make-list-from-is-all-but-last, 24 make-list-from-make-list-from, 112 make-list-from-nlistp, 34 make-list-from-simple, 49 make-list-from-simplify, 36 make-list-from-simplify-better, 124 make-list-from-xor-bvs-nat-to-bv

-list, 113 make-properp, 121, 122, 124, 125 match-and-xor, 55, 60, 62, 90, 93,

94, 117, 119, 122 match-and-xor-clock, 60, 62 match-and-xor-general-induct, 55 match-and-xor-input-conditionp, 60,

61 match-and-xor-loop-clock, 55, 60 match-and-xor-program, 53, 54, 59,

61, 89, 96, 101, 104, 128, 129

match-member, 117–119, 122, 123 match-member-at-least-min-means, 119 match-member-cons, 118 match-member-cons-0, 118 match-member-high-bit-xor-bvs, 123 match-member-high-bit-xor-bvs-he

lper, 123 match-member-highest-bit-xor-bv

s, 119

s-rewrite, 119 max-0-means, 105 max-0-means-all-zero-bitvp, 121 max-0-means-sum-0, 121 max-list, 79, 82, 90, 94, 102, 105, 120–122, 126

max-list-helper, 79, 81 max-list-helper-max-list, 79 max-list-helper-max-list-0, 79 max-list-means-number-0, 120 max-list-not-too-big, 105 max-nat-clock, 81, 82 max-nat-input-conditionp, 81, 82 max-nat-loop-clock, 79, 81 max-nat-loop-induct, 79, 80 max-nat-program, 77, 78, 80, 81, 89, 95, 101, 104, 128, 129

max-sum, 107, 108

member-all-valid-moves, 125

member-all-valid-moves-helper, 125 member-all-valid-moves-means-pre

fix, 124 member-cons-all-valid-moves-helpe

r1, 124 member-list-max-list, 94 member-make-properp, 122 member-max-list, 120 member-means-lessp-sum, 120 member-nthcdr-means, 84 member-nthcdr-simplify, 85 member-number-with-at-least, 112,

113 member-of-natlist-means, 84 multiplication-on, 3

nat-list-piton, 41–43, 64–67, 69, 70, 80, 81, 84–86, 94, 95, 104, 105, 127

nat-list-piton-means, 42 nat-list-piton-means-cadr, 66 nat-list-piton-means-car, 64 nat-list-piton-means-get, 67 nat-list-piton-means-get-cdr, 67 nat-list-piton-means-last, 65 nat-list-piton-means-last-cdr, 65 nat-listp, 93, 107, 109, 110, 116, 117,

119, 121–123, 125, 126, 131 nat-listp-append, 107 nat-listp-bv-to-nat-list, 126 nat-listp-computer-move, 126 nat-listp-listp, 110, 126 nat-listp-listp-all-valid-moves, 110

-helper, 110 nat-listp-listp-simple, 113 nat-listp-listp-simple-means-pr

operp, 113 nat-listp-means-nat-listp-simple, 109 nat-listp-replace-value, 126 nat-listp-simple, 108–110, 113, 120,

121, 125 nat-listp-simple-append, 108 nat-listp-simple-means-properp, 113 nat-listp-simplify, 121 nat-listp-smart-move, 126 nat-to-bv, 5, 22, 23, 26, 27, 63, 64,

111, 113–116 nat-to-bv-1, 114 nat-to-bv-2, 114 nat-to-bv-bv-to-nat, 23 nat-to-bv-clock, 21, 22, 27, 64 nat-to-bv-equiv-helper, 26 nat-to-bv-equivalence, 27 nat-to-bv-induct, 114 nat-to-bv-input-conditionp, 21, 22,

27 nat-to-bv-list, 63, 66, 69, 71, 90, 93,

94, 97, 102, 106, 109, 111– 114, 116, 119, 122, 123, 129

nat-to-bv-list-append, 111 nat-to-bv-list-bv-to-nat-list, 93 nat-to-bv-list-clock, 70, 71 nat-to-bv-list-input-conditionp, 70, 71 nat-to-bv-list-loop-clock, 63, 64, 69,

70 nat-to-bv-list-loop-induct, 64 nat-to-bv-list-program, 62, 63, 68,

70, 89, 96, 101, 104, 128, 129

nat-to-bv-loop-clock, 19, 21

nat-to-bv-program, 18–20, 22, 27, 63, 69, 70, 89, 96, 101, 105, 128 nat-to-bv-simple, 22 nat-to-bv-state, 5 nat-to-bv2, 19, 22, 27 nat-to-bv2-helper, 19, 21, 26 nim-piton-ctrl-stk-requirement, 127,

131 nim-piton-space-reasonable, 131 nim-piton-temp-stk-requirement, 127,

131 nlistp-bv-to-nat2, 38 non-green-in-list, 109, 113, 117, 125,

126 non-green-in-list-zerop-ws, 113 non-zero-means-acc-irrelevant, 29 non-zero-means-acc-irrelevant-spe

c, 29 not-all-zero-bitvp-cdr-means, 30 not-all-zero-bitvp-make-list-fr

om, 49 not-equal-nth-0-means, 35 not-green-state-means, 116 not-last-0-means-not-all-0, 37 not-lessp-exp-means-all-ones, 115 nth, 34–37, 113, 124, 125 nth-1, 125 nth-as-last, 113 nth-cons, 124 nth-nlistp, 34 nthcdr, 12–14, 43, 47, 48, 55–60, 64,

68, 69, 75, 76, 81, 84–86, 124, 125

nthcdr-1, 14 nthcdr-append, 47 nthcdr-cdr, 124 nthcdr-cons-make-list-from-hack, 125 nthcdr-length-cdr, 56 nthcdr-open, 13 nthcdr-untag-array, 56 nthcdr-x-cdr-put-x, 68 number-with-at-least, 41–43, 45, 90,

93, 97, 102, 106, 109, 110, 112, 114, 116, 119–122

number-with-at-least-append, 110 number-with-at-least-as-sum, 120 number-with-at-least-clock, 43, 44 number-with-at-least-clock-loop, 41,

43 number-with-at-least-correctnes

s-general, 42 number-with-at-least-general-in

duct, 41 number-with-at-least-input-conditi

onp, 43, 44 number-with-at-least-match-and-

xor, 119 number-with-at-least-max-list, 122 number-with-at-least-nlistp, 42 number-with-at-least-of-all-zer

os, 110 number-with-at-least-program, 39, 40,

42, 44, 89, 96, 101, 104, 128

number-with-at-least-replace-va

lue, 119 numberp-max-list, 105

one-bit-vector, 16–19, 21, 23, 26, 27,

30, 32, 38, 47, 52, 113, 114 open-highest-when-and-not-0, 50 p, 4, 5, 9, 10, 14, 15, 18, 21, 22, 27,

32, 33, 39, 43, 44, 49, 53, 60, 62, 69, 71, 76, 77, 81, 82, 86, 87, 96, 98, 99, 106, 130

p->r, 132 p-0, 4 p-add1, 4 p-ctrl-stk, 7, 17, 21, 33, 43, 44, 52,

61, 70, 73, 81, 86, 95, 99, 103, 127

p-ctrl-stk-size, 7, 17, 21, 33, 44, 52, 59, 61, 68, 70, 73, 75, 80, 81, 86, 95, 99, 103, 127

p-current-instruction, 14, 15, 18, 22, 27, 33, 39, 44, 53, 61, 70, 74, 82, 87, 96, 99, 105, 130

p-data-segment, 7, 43, 44, 61, 70, 74, 81, 86, 87, 95, 103, 104, 127, 130

p-halt, 4 p-ins-okp, 4 p-ins-step, 4 p-loadablep, 132 p-max-ctrl-stk-size, 7, 17, 21, 33, 44,

52, 61, 70, 73, 81, 86, 95, 99, 103, 127 p-max-temp-stk-size, 7, 17, 21, 33,

44, 52, 61, 70, 73, 81, 86, 95, 99, 103, 127

p-opener, 4 p-pc, 130 p-prog-segment, 44, 52, 61, 70, 73,

74, 81, 86, 95, 96, 99, 104, 105

p-psw, 130

p-state, 4, 5, 9, 10, 14–19, 21, 22, 27–29, 32, 33, 39, 40, 43– 46, 49, 53, 55, 60–63, 69– 71, 73, 76, 77, 79, 81, 82, 84, 86–88, 90, 96–100, 102, 105, 106, 130, 131

p-step, 4, 5 p-step1, 4 p-step1-opener, 4 p-temp-stk, 7, 17, 21, 33, 43, 44, 52,

60, 61, 70, 71, 73, 74, 81, 82, 86, 87, 95, 99, 103, 104, 127

p-word-size, 7, 21, 33, 43, 44, 52, 61, 70, 74, 81, 82, 86, 87, 95, 96, 99, 103–105, 127, 132

plus-bv-to-nat-make-list-from, 35 plus-quotient-bv-to-nat, 37 pretty-load, 132 pretty-load1, 132 pretty-state, 132 pretty-vector, 132 pretty-vector-lst, 132 pretty-vector1, 132 proper-p-statep, 132 properp, 36, 51, 56, 58, 68, 107, 108,

110, 112, 113, 117, 121–124, 126, 129

properp-bv-to-nat-list, 129 properp-computer-move, 129 properp-highest-bit, 123 properp-make-properp, 122 properp-nat-to-bv-list, 129 properp-replace-value, 129 properp-tag-array, 129 properp-untag-array, 129 properp-xor-bitv, 112 properp-xor-bvs, 112 push-1-vector-input-conditionp, 17,

18 push-1-vector-program, 16–19, 22, 27,

28, 33, 39, 46, 52, 63, 69, 70, 73–75, 89, 96, 101, 105, 128

put, 56, 59, 68, 85 put-assoc, 57, 58, 60, 62, 64, 65, 69,

71, 75–77, 86, 87, 97, 106 put-length-cdr, 56 put-length-cdr-general, 68

quotient-difference, 116 quotient-exp-hack, 36 quotient-plus-hack, 34 quotients-on, 3

r->i, 132 remainder-add1-2, 121 remainder-difference-2, 120 remainder-plus-remainder, 120 remainder-plus-remainder2, 120 remainder-plus-sum-number-hack, 121 remainder-sub1-2, 121 remainders-on, 3 remove-highest-bits, 117, 118, 123 replace-value, 84, 86, 87, 90, 94, 102,

119, 120, 122, 126, 129 replace-value-clock, 86, 87 replace-value-input-conditionp, 86, 87 replace-value-loop-clock, 84, 86 replace-value-loop-induct, 84 replace-value-nthcdr-open, 84 replace-value-program, 83, 85, 86,

89, 95, 101, 104, 128, 129 replace-value-simplify, 122 replace-value-x-x, 126

smart-move, 90, 97, 102, 126 smart-move-clock, 96 smart-move-input-conditionp, 95, 96 smart-move-program, 88, 90, 95, 101,

104, 128, 129 smart-move-small-ws, 126 sum, 107, 108, 114, 120, 121, 126 sum-append, 107 sum-replace-value, 120 sum-when-all-zero, 126

tag, 14, 55 tag-array, 55, 57, 59, 60, 62, 66, 67,

69, 71, 76, 77, 94, 97, 106, 129

tag-array-cdr-untag-array-hack, 57 tag-array-replace-value-untag-a

rray, 94 tag-array-untag-array, 55 tag-array-untag-array-nthcdr-cd

dr-hack, 59 tag-array-untag-array-of-bit-ve

ctors-piton, 94 tag-array-untag-array-of-nat-li

st-piton, 94 top, 7, 21, 33, 52, 60, 61, 70, 71, 74,

81, 82, 86, 87, 95, 99, 103, 104, 127

trailing-zeros, 29, 34, 38, 51, 52 trailing-zeros-append, 29 trailing-zeros-helper, 29, 30, 35, 36,

38, 47 trailing-zeros-helper-append, 29 trailing-zeros-helper-one-bit-ve

ctor, 38 trailing-zeros-nth-proof, 36 trailing-zeros-nth-spec, 36 trailing-zeros-of-all-zero-bitvp, 29 trailing-zeros-one-bit-vector, 52 triple-cdr-with-sub1-induct, 50

untag, 7, 11, 14, 15, 55, 57, 64, 74, 75, 79–82, 85–87, 95–97, 103– 106, 127, 130

untag-array, 11–16, 42, 43, 45, 55– 62, 69, 71, 76, 77, 81, 82, 94, 96, 103, 105, 127, 129, 130

untag-array-tag-array-of-bit-ve

ctorsp, 94 untag-array-tag-array-of-match-

and-xor-hack, 94 untag-array-tag-array-of-nat-to

-bv-list, 94

valid-movep, 117, 122, 123, 125, 131 valid-movep-and-makes-nongreen-

means, 125 valid-movep-computer-move, 123 valid-movep-computer-move-bette

r, 131 valid-movep-computer-move-helpe

r, 123 valid-movep-match-and-xor, 122 valid-movep-replace-value, 122 valid-movep-x-x, 122

wsp, 109, 126, 131 wsp-green-state, 126 wsp-green-state-proof, 126 wsp-measure, 108

x-y-error-msg, 4 xor-bit, 13, 113, 118 xor-bitv, 7, 8, 11–13, 19, 20, 23–26,

55, 109, 111–113, 117–119, 122, 123

xor-bitv-0, 13 xor-bitv-associative, 11 xor-bitv-commutative, 11 xor-bitv-commutative2, 11 xor-bitv-fix-bitv, 111 xor-bitv-nlistp, 13 xor-bitv-nlistp2, 13 xor-bitv-nlistp3, 25 xor-bitv-xor-bvs-hack, 111 xor-bitv-zero-bit-vector, 109 xor-bvs, 10–13, 15, 16, 90, 94, 102,

106, 109–114, 116–119, 123 xor-bvs-append, 111 xor-bvs-append-hack, 111 xor-bvs-array, 7, 9, 10, 13–15 xor-bvs-array-rewrite, 13 xor-bvs-clock, 7, 14, 15 xor-bvs-clock-loop, 7, 9, 10 xor-bvs-input-conditionp, 6, 7, 14,

15 xor-bvs-input-conditionp-means-

xor-bvs-hack, 14 xor-bvs-loop-correctness, 9 xor-bvs-loop-correctness-genera

l, 8

l-induct, 8 xor-bvs-match-and-xor, 117 xor-bvs-nat-to-bv-list-zerop-ws, 112 xor-bvs-of-list-of-0s-and-1s, 114 xor-bvs-program, 6, 8, 9, 14–16, 90,

96, 101, 105, 128 xor-bvs-remove-highest-bits, 118

zero-bit-vector, 19, 21–23, 26, 34– 38, 46–48, 50–52, 58, 111– 115, 117, 118