\documentstyle[makeidx]{article}
\makeindex
%\setlength{\oddsidemargin}{.5in}
%\setlength{\evensidemargin}{.5in}
%\setlength{\textwidth}{5.8in}
\begin{document}
%\setlength{\parindent}{0pt}
%\newcounter{bean}
%\begin{list}{\arabic{bean}.}{\usecounter{bean}\setlength{\leftmargin}{0pt}\setlength{\rightmargin}{0pt}\setlength{\listparindent}{20pt}\setlength{\parsep}{5pt}}
%\item[]

\begin{verbatim}#|

 Copyright (C) 1994 by Computational Logic, Inc.  All Rights Reserved.

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

 NO WARRANTY

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

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

; Nim game proof            Matt Wilding                   November 1991

; Requires the naturals library.

\end{verbatim}
\noindent{\sc Event}:   Start with the library {\tt{"naturals"}} using the compiled version.

\addvspace{18pt}

\begin{verbatim}#|
(Part of internal note 249)

CLI note #249:  A Verified NIM Strategy   Matt Wilding  Nov 1991

Introduction
------------

NIM is a two player game played with matches distributed into piles.
Players alternate removing at least one match from exactly one pile.
The player who removes the last match loses.  

NIM is particularly interesting because it would appear to make a good
FM9001 stack demo program.  The game has nice mathematical properties
that can be verified, it's a real game that people have played for
hundreds of years, and it's not I/O intensive.  (In fact, no input is
required to watch a game played between a "smart" player and his
"random" opponent.)

A simple strategy that guarantees a win for most initial game setups
has been discovered, and an NQTHM proof constructed that proves the
strategy works.  Subsequently, a reference to a 1901 paper by Charles
Bouton that proves this same NIM strategy correct has been discovered
in "Mathematical Puzzles and Diversions" by Martin Gardner.

An outline of the strategy and proof
------------------------------------
Let n be the number of piles.  Let p(i) be the number of matches in
pile i.  Let b(x) be the base 2 representation of x to some large
number of bits. Let XOR-BV(x,y) be the bitwise exclusive or of b(x)
and b(y).  Let XOR-BVS(x0, x1, ... xn) be XOR-BV(x0, XOR-BV(x1, ...)).

A state is a LOSER state if

  XOR-BVS(p(0),...,p(n)) = b(0) and there is an i such that P(i)>1
or
  XOR-BVS(P(0),...,p(n)) = b(1) and there is no i such that P(i)>1.

  Consider the following strategy:

  If no pile has 2 matches, remove the match in one pile.

  If there is exactly one pile with at least 2 matches, remove all the
  matches in that pile if there are an even number of non-empty piles
  and all but one match if there are an odd number of non-empty piles.

  Otherwise, find the highest bit position n such that there is an odd
  number of 1 bits in the binary representation of the piles.  Replace
  a pile with a 1 in bit position n with the "exclusive-or" of the
  other piles.

If not in a loser state and there are no piles with at least 2
matches, then clearly removing a non-empty pile is a valid move that
will make the state a loser state.

If not in a loser state and there is exactly one pile with at least 2
matches, removing the matches in that pile if there is an even number
of non-empty piles or all but one of the matches if an odd number of
non-empty piles is a valid move that will make a loser state.

Otherwise, again if not in a loser state, there must be at least 2
piles with at least 2 matches and a highest bit position n such with
an odd number of 1 bits.  Replacing a pile with a 1 bit in bit
position n in the manner described will reduce the number in that
pile, so this constitutes a valid move.  Also, the exclusive-or of
resulting piles will be all zeros, and there will still be at least 1
pile remaining with at least 2 matches, so the resulting state will be
a loser state.

Thus, the strategy transforms any non-losing state into a losing state
with a valid move.  Since any move from a loser state is a non-loser
state, and the empty state is not a loser state, the strategy above
will always yield a win if the game is in a non-losing state
immediately before a turn or if the game is in a losing state
immediately before the opponent's turn.

An example game
---------------

We get the theorem prover to print the evolving game state, and use
r-loop to evaluate an example:

      >(bm-trace (game-with-stupid-move :entry 
          (list (if (car arglist) 'computer 'player) 
                (bv-to-nat-state (cadr arglist)))))

      >(r-loop)

      Abbreviated Output Mode:  On
      Type ? for help.
      *(loser-state (nat-to-bv-state '(3 5 8) 5) 5)
       F
      *(reasonable-game-statep (nat-to-bv-state '(3 5 8) 5) 5)
       T
      *(game-with-stupid-move t (nat-to-bv-state '(3 5 8) 5) 5)
        1> (<<GAME-WITH-STUPID-MOVE>> '(COMPUTER (3 5 8)))
        2> (<<GAME-WITH-STUPID-MOVE>> '(PLAYER (3 5 6)))
        3> (<<GAME-WITH-STUPID-MOVE>> '(COMPUTER (2 5 6)))
        4> (<<GAME-WITH-STUPID-MOVE>> '(PLAYER (2 4 6)))
        5> (<<GAME-WITH-STUPID-MOVE>> '(COMPUTER (1 4 6)))
        6> (<<GAME-WITH-STUPID-MOVE>> '(PLAYER (1 4 5)))
        7> (<<GAME-WITH-STUPID-MOVE>> '(COMPUTER (0 4 5)))
        8> (<<GAME-WITH-STUPID-MOVE>> '(PLAYER (0 4 4)))
        9> (<<GAME-WITH-STUPID-MOVE>> '(COMPUTER (0 3 4)))
       10> (<<GAME-WITH-STUPID-MOVE>> '(PLAYER (0 3 3)))
       11> (<<GAME-WITH-STUPID-MOVE>> '(COMPUTER (0 2 3)))
       12> (<<GAME-WITH-STUPID-MOVE>> '(PLAYER (0 2 2)))
       13> (<<GAME-WITH-STUPID-MOVE>> '(COMPUTER (0 1 2)))
       14> (<<GAME-WITH-STUPID-MOVE>> '(PLAYER (0 1 0)))
       15> (<<GAME-WITH-STUPID-MOVE>> '(COMPUTER (0 0 0)))
       T
      *

|#

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{put} \\  
\=\+{\rm{put}}\,({\it{place\/}}, {\it{value\/}}, {\it{state\/}})\index{put} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{place\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\rm{cons}}\,({\it{value\/}}, {\rm{cdr}}\,({\it{state\/}})) \\ 
{\bf else }{\rm{cons}}\,({\rm{car}}\,({\it{state\/}}), {\rm{put}}\,({\it{place\/}} $-\;1$, {\it{value\/}}, {\rm{cdr}}\,({\it{state\/}}))\index{put})$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{get} \\  
\=\+{\rm{get}}\,({\it{place\/}}, {\it{state\/}})\index{get} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{place\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\rm{car}}\,({\it{state\/}}) \\ 
{\bf else }{\rm{get}}\,({\it{place\/}} $-\;1$, {\rm{cdr}}\,({\it{state\/}}))\index{get}$\;${\bf  endif}\-\-
\end{tabbing}


\begin{tabbing}{\sc Theorem}:  get-put \\ \index{get-put}
\=\+{\rm{get}}\,({\it{a1\/}}, {\rm{put}}\,({\it{a2\/}}, {\it{value\/}}, {\it{state\/}})\index{put})\index{get} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{fix}}\,({\it{a1\/}}) $=$ {\rm{fix}}\,({\it{a2\/}})$\;\;${\bf then }{\it{value\/}} \\ 
{\bf else }{\rm{get}}\,({\it{a1\/}}, {\it{state\/}})\index{get}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{length} \\  
\=\+{\rm{length}}\,({\it{list\/}})\index{length} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{list\/}})$\;\;${\bf then }$1\;+$ {\rm{length}}\,({\rm{cdr}}\,({\it{list\/}}))\index{length} \\ 
{\bf else }{\tt{0}}$\;${\bf  endif}\-\-
\end{tabbing}


\noindent{\sc Event}:   Introduce the function symbol {\it bv-size\index{bv-size}\/} of 0 arguments.

\addvspace{18pt}

\begin{tabbing}{\sc Definition}:\index{bitp}$\;\;$
{\rm{bitp}}\,({\it{bit\/}})\index{bitp} $=$ (({\it{bit\/}} $=$ {\tt{0}}) $\vee$ ({\it{bit\/}} $=$ {\tt{1}}))
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{bvp} \\  
\=\+{\rm{bvp}}\,({\it{bv\/}})\index{bvp} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{bv\/}})$\;\;${\bf then }{\rm{bitp}}\,({\rm{car}}\,({\it{bv\/}}))\index{bitp} $\wedge$ {\rm{bvp}}\,({\rm{cdr}}\,({\it{bv\/}}))\index{bvp} \\ 
{\bf else }{\it{bv\/}} $=$ {\bf{nil}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{bvsp} \\  
\=\+{\rm{bvsp}}\,({\it{bvs\/}})\index{bvsp} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{bvs\/}})$\;\;${\bf then }{\rm{bvp}}\,({\rm{car}}\,({\it{bvs\/}}))\index{bvp} $\wedge$ {\rm{bvsp}}\,({\rm{cdr}}\,({\it{bvs\/}}))\index{bvsp} \\ 
{\bf else }{\it{bvs\/}} $=$ {\bf{nil}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{good-state-of-size} \\  
\=\+{\rm{good-state-of-size}}\,({\it{state\/}}, {\it{size\/}})\index{good-state-of-size} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{state\/}}) \\ 
{\bf then }\=\+{\rm{bvp}}\,({\rm{car}}\,({\it{state\/}}))\index{bvp} \\ 
$\wedge$$\;\;\;\;$({\rm{length}}\,({\rm{car}}\,({\it{state\/}}))\index{length} $=$ {\rm{fix}}\,({\it{size\/}})) \\ 
$\wedge$$\;\;\;\;${\rm{good-state-of-size}}\,({\rm{cdr}}\,({\it{state\/}}), {\it{size\/}})\index{good-state-of-size}\- \\ 
{\bf else }{\it{state\/}} $=$ {\bf{nil}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{good-state} \\  
{\rm{good-state}}\,({\it{state\/}})\index{good-state} $=$ {\rm{good-state-of-size}}\,({\it{state\/}}, {\sc{bv-size}}\index{bv-size})\index{good-state-of-size}
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{lessp-bv} \\  
\=\+{\rm{lessp-bv}}\,({\it{bv1\/}}, {\it{bv2\/}})\index{lessp-bv} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{bv1\/}}) $\wedge$ {\rm{listp}}\,({\it{bv2\/}}) \\ 
{\bf then }\=\+({\rm{car}}\,({\it{bv1\/}}) $<$ {\rm{car}}\,({\it{bv2\/}})) \\ 
$\vee$$\;\;\;\;$(({\rm{car}}\,({\it{bv1\/}}) $=$ {\rm{car}}\,({\it{bv2\/}})) $\wedge$ {\rm{lessp-bv}}\,({\rm{cdr}}\,({\it{bv1\/}}), {\rm{cdr}}\,({\it{bv2\/}}))\index{lessp-bv})\- \\ 
{\bf else }{\bf{f}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{verbatim};; high order bit first
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{nat-to-bv} \\  
\=\+{\rm{nat-to-bv}}\,({\it{nat\/}}, {\it{size\/}})\index{nat-to-bv} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{size\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\bf{nil}} \\ 
{\bf elseif }{\it{nat\/}} $<$ {\rm{exp}}\,({\tt{2}}, {\it{size\/}} $-\;1$)\index{exp}$\;\;${\bf then }{\rm{cons}}\,({\tt{0}}, {\rm{nat-to-bv}}\,({\it{nat\/}}, {\it{size\/}} $-\;1$)\index{nat-to-bv}) \\ 
{\bf else }{\rm{cons}}\,({\tt{1}}, {\rm{nat-to-bv}}\,({\it{nat\/}} $-$ {\rm{exp}}\,({\tt{2}}, {\it{size\/}} $-\;1$)\index{exp}, {\it{size\/}} $-\;1$)\index{nat-to-bv})$\;${\bf  endif}\-\-
\end{tabbing}

\begin{verbatim};; most significant bit first
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{bv-to-nat} \\  
\=\+{\rm{bv-to-nat}}\,({\it{bv\/}})\index{bv-to-nat} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{bv\/}}) \\ 
{\bf then }({\rm{car}}\,({\it{bv\/}}) $*$ {\rm{exp}}\,({\tt{2}}, {\rm{length}}\,({\rm{cdr}}\,({\it{bv\/}}))\index{length})\index{exp}) $+$ {\rm{bv-to-nat}}\,({\rm{cdr}}\,({\it{bv\/}}))\index{bv-to-nat} \\ 
{\bf else }{\tt{0}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  length-nat-to-bv \\ \index{length-nat-to-bv}
{\rm{length}}\,({\rm{nat-to-bv}}\,({\it{nat\/}}, {\it{size\/}})\index{nat-to-bv})\index{length} $=$ {\rm{fix}}\,({\it{size\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  bv-to-nat-nat-to-bv \\ \index{bv-to-nat-nat-to-bv}
\=\+{\rm{bv-to-nat}}\,({\rm{nat-to-bv}}\,({\it{nat\/}}, {\it{size\/}})\index{nat-to-bv})\index{bv-to-nat} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{nat\/}} $<$ {\rm{exp}}\,({\tt{2}}, {\it{size\/}})\index{exp}$\;\;${\bf then }{\rm{fix}}\,({\it{nat\/}}) \\ 
{\bf else }{\rm{exp}}\,({\tt{2}}, {\it{size\/}})\index{exp} $-\;1$$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  lessp-bv-length \\ \index{lessp-bv-length}
{\rm{bvp}}\,({\it{x\/}})\index{bvp} $\rightarrow$ ({\rm{bv-to-nat}}\,({\it{x\/}})\index{bv-to-nat} $<$ {\rm{exp}}\,({\tt{2}}, {\rm{length}}\,({\it{x\/}})\index{length})\index{exp})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  lessp-bv-to-nat-bv-to-nat \\ \index{lessp-bv-to-nat-bv-to-nat}
\=\+(({\rm{length}}\,({\it{x\/}})\index{length} $=$ {\rm{length}}\,({\it{y\/}})\index{length}) $\wedge$ {\rm{bvp}}\,({\it{x\/}})\index{bvp} $\wedge$ {\rm{bvp}}\,({\it{y\/}})\index{bvp}) \\ 
$\rightarrow$$\;\;\;\;$(({\rm{bv-to-nat}}\,({\it{x\/}})\index{bv-to-nat} $<$ {\rm{bv-to-nat}}\,({\it{y\/}})\index{bv-to-nat}) $=$ {\rm{lessp-bv}}\,({\it{x\/}}, {\it{y\/}})\index{lessp-bv})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  lessp-bv-nat-to-bv-nat-to-bv \\ \index{lessp-bv-nat-to-bv-nat-to-bv}
\=\+(({\it{x\/}} $<$ {\rm{exp}}\,({\tt{2}}, {\it{size\/}})\index{exp}) $\wedge$ ({\it{y\/}} $<$ {\rm{exp}}\,({\tt{2}}, {\it{size\/}})\index{exp})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{lessp-bv}}\,({\rm{nat-to-bv}}\,({\it{x\/}}, {\it{size\/}})\index{nat-to-bv}, {\rm{nat-to-bv}}\,({\it{y\/}}, {\it{size\/}})\index{nat-to-bv})\index{lessp-bv} $=$ ({\it{x\/}} $<$ {\it{y\/}}))\-
\end{tabbing}

\begin{verbatim};; return the number of columns with value at least min
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{number-with-at-least} \\  
\=\+{\rm{number-with-at-least}}\,({\it{state\/}}, {\it{min\/}}, {\it{size\/}})\index{number-with-at-least} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{state\/}}) \\ 
{\bf then }\=\+{\bf if }$\neg$ {\rm{lessp-bv}}\,({\rm{car}}\,({\it{state\/}}), {\rm{nat-to-bv}}\,({\it{min\/}}, {\it{size\/}})\index{nat-to-bv})\index{lessp-bv} \\ 
{\bf then }$1\;+$ {\rm{number-with-at-least}}\,({\rm{cdr}}\,({\it{state\/}}), {\it{min\/}}, {\it{size\/}})\index{number-with-at-least} \\ 
{\bf else }{\rm{number-with-at-least}}\,({\rm{cdr}}\,({\it{state\/}}), {\it{min\/}}, {\it{size\/}})\index{number-with-at-least}$\;${\bf  endif}\- \\ 
{\bf else }{\tt{0}}$\;${\bf  endif}\-\-
\end{tabbing}
        
\begin{verbatim};; return a column number with value at least min
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{col-with-at-least} \\  
\=\+{\rm{col-with-at-least}}\,({\it{state\/}}, {\it{min\/}}, {\it{size\/}})\index{col-with-at-least} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{state\/}}) \\ 
{\bf then }\=\+{\bf if }$\neg$ {\rm{lessp-bv}}\,({\rm{car}}\,({\it{state\/}}), {\rm{nat-to-bv}}\,({\it{min\/}}, {\it{size\/}})\index{nat-to-bv})\index{lessp-bv}$\;\;${\bf then }{\tt{0}} \\ 
{\bf else }$1\;+$ {\rm{col-with-at-least}}\,({\rm{cdr}}\,({\it{state\/}}), {\it{min\/}}, {\it{size\/}})\index{col-with-at-least}$\;${\bf  endif}\- \\ 
{\bf else }{\bf{f}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{xor} \\  
\=\+{\rm{xor}}\,({\it{bit1\/}}, {\it{bit2\/}})\index{xor} \\ 
$=$$\;\;\;\;$\=\+{\bf if }({\it{bit1\/}} $\simeq {\tt{0}}$) $=$ ({\it{bit2\/}} $\simeq {\tt{0}}$)$\;\;${\bf then }{\tt{0}} \\ 
{\bf else }{\tt{1}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{xor-bv} \\  
\=\+{\rm{xor-bv}}\,({\it{bv1\/}}, {\it{bv2\/}})\index{xor-bv} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{bv1\/}}) $\wedge$ {\rm{listp}}\,({\it{bv2\/}}) \\ 
{\bf then }{\rm{cons}}\,({\rm{xor}}\,({\rm{car}}\,({\it{bv1\/}}), {\rm{car}}\,({\it{bv2\/}}))\index{xor}, {\rm{xor-bv}}\,({\rm{cdr}}\,({\it{bv1\/}}), {\rm{cdr}}\,({\it{bv2\/}}))\index{xor-bv}) \\ 
{\bf else }{\bf{nil}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{fix-bit} \\  
\=\+{\rm{fix-bit}}\,({\it{x\/}})\index{fix-bit} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{x\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\tt{0}} \\ 
{\bf else }{\tt{1}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{fix-xor-bv} \\  
\=\+{\rm{fix-xor-bv}}\,({\it{bv\/}})\index{fix-xor-bv} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{bv\/}})$\;\;${\bf then }{\rm{cons}}\,({\rm{fix-bit}}\,({\rm{car}}\,({\it{bv\/}}))\index{fix-bit}, {\rm{fix-xor-bv}}\,({\rm{cdr}}\,({\it{bv\/}}))\index{fix-xor-bv}) \\ 
{\bf else }{\bf{nil}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{xor-bvs} \\  
\=\+{\rm{xor-bvs}}\,({\it{bvs\/}})\index{xor-bvs} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{bvs\/}}) \\ 
{\bf then }\=\+{\bf if }{\rm{listp}}\,({\rm{cdr}}\,({\it{bvs\/}}))$\;\;${\bf then }{\rm{xor-bv}}\,({\rm{car}}\,({\it{bvs\/}}), {\rm{xor-bvs}}\,({\rm{cdr}}\,({\it{bvs\/}}))\index{xor-bvs})\index{xor-bv} \\ 
{\bf else }{\rm{fix-xor-bv}}\,({\rm{car}}\,({\it{bvs\/}}))\index{fix-xor-bv}$\;${\bf  endif}\- \\ 
{\bf else }{\bf{nil}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  bvp-fix-xor-bv \\ \index{bvp-fix-xor-bv}
{\rm{bvp}}\,({\rm{fix-xor-bv}}\,({\it{x\/}})\index{fix-xor-bv})\index{bvp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  bvp-fix-xor-bv-identity \\ \index{bvp-fix-xor-bv-identity}
{\rm{bvp}}\,({\it{x\/}})\index{bvp} $\rightarrow$ ({\rm{fix-xor-bv}}\,({\it{x\/}})\index{fix-xor-bv} $=$ {\it{x\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  commutativity-of-xor \\ \index{commutativity-of-xor}
{\rm{xor}}\,({\it{a\/}}, {\it{b\/}})\index{xor} $=$ {\rm{xor}}\,({\it{b\/}}, {\it{a\/}})\index{xor}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  associativity-of-xor \\ \index{associativity-of-xor}
{\rm{xor}}\,({\rm{xor}}\,({\it{a\/}}, {\it{b\/}})\index{xor}, {\it{c\/}})\index{xor} $=$ {\rm{xor}}\,({\it{a\/}}, {\rm{xor}}\,({\it{b\/}}, {\it{c\/}})\index{xor})\index{xor}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  commutativity2-of-xor \\ \index{commutativity2-of-xor}
{\rm{xor}}\,({\it{c\/}}, {\rm{xor}}\,({\it{a\/}}, {\it{b\/}})\index{xor})\index{xor} $=$ {\rm{xor}}\,({\it{a\/}}, {\rm{xor}}\,({\it{c\/}}, {\it{b\/}})\index{xor})\index{xor}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  commutativity-of-xor-bv \\ \index{commutativity-of-xor-bv}
{\rm{xor-bv}}\,({\it{a\/}}, {\it{b\/}})\index{xor-bv} $=$ {\rm{xor-bv}}\,({\it{b\/}}, {\it{a\/}})\index{xor-bv}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  associativity-of-xor-bv \\ \index{associativity-of-xor-bv}
{\rm{xor-bv}}\,({\rm{xor-bv}}\,({\it{a\/}}, {\it{b\/}})\index{xor-bv}, {\it{c\/}})\index{xor-bv} $=$ {\rm{xor-bv}}\,({\it{a\/}}, {\rm{xor-bv}}\,({\it{b\/}}, {\it{c\/}})\index{xor-bv})\index{xor-bv}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  commutativity2-of-xor-bv \\ \index{commutativity2-of-xor-bv}
{\rm{xor-bv}}\,({\it{c\/}}, {\rm{xor-bv}}\,({\it{a\/}}, {\it{b\/}})\index{xor-bv})\index{xor-bv} $=$ {\rm{xor-bv}}\,({\it{a\/}}, {\rm{xor-bv}}\,({\it{c\/}}, {\it{b\/}})\index{xor-bv})\index{xor-bv}
\end{tabbing}

\begin{verbatim};; return number of first vector with high bit on
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{high-bit-on} \\  
\=\+{\rm{high-bit-on}}\,({\it{bvs\/}})\index{high-bit-on} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{bvs\/}}) \\ 
{\bf then }\=\+{\bf if }{\rm{caar}}\,({\it{bvs\/}}) $=$ {\tt{1}}$\;\;${\bf then }{\tt{0}} \\ 
{\bf else }$1\;+$ {\rm{high-bit-on}}\,({\rm{cdr}}\,({\it{bvs\/}}))\index{high-bit-on}$\;${\bf  endif}\- \\ 
{\bf else }{\bf{f}}$\;${\bf  endif}\-\-
\end{tabbing}
  
\begin{tabbing}{\sc Definition}:\index{delete-pile} \\  
\=\+{\rm{delete-pile}}\,({\it{place\/}}, {\it{state\/}})\index{delete-pile} \\ 
$=$$\;\;\;\;$\=\+{\bf if }$\neg$ {\rm{listp}}\,({\it{state\/}})$\;\;${\bf then }{\it{state\/}} \\ 
{\bf elseif }{\it{place\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\rm{cdr}}\,({\it{state\/}}) \\ 
{\bf else }{\rm{cons}}\,({\rm{car}}\,({\it{state\/}}), {\rm{delete-pile}}\,({\it{place\/}} $-\;1$, {\rm{cdr}}\,({\it{state\/}}))\index{delete-pile})$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{delete-high-bits} \\  
\=\+{\rm{delete-high-bits}}\,({\it{state\/}})\index{delete-high-bits} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{state\/}})$\;\;${\bf then }{\rm{cons}}\,({\rm{cdar}}\,({\it{state\/}}), {\rm{delete-high-bits}}\,({\rm{cdr}}\,({\it{state\/}}))\index{delete-high-bits}) \\ 
{\bf else }{\bf{nil}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  find-high-out-of-sync-rewrite \\ \index{find-high-out-of-sync-rewrite}
\=\+({\rm{listp}}\,({\it{state\/}}) $\wedge$ {\rm{listp}}\,({\rm{car}}\,({\it{state\/}}))) \\ 
$\rightarrow$$\;\;\;\;$({\rm{length}}\,({\rm{car}}\,({\rm{delete-high-bits}}\,({\it{state\/}})\index{delete-high-bits}))\index{length} $<$ {\rm{length}}\,({\rm{car}}\,({\it{state\/}}))\index{length})\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{find-high-out-of-sync} \\  
\=\+{\rm{find-high-out-of-sync}}\,({\it{state\/}})\index{find-high-out-of-sync} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{state\/}}) \\ 
{\bf then }\=\+{\bf if }{\rm{listp}}\,({\rm{car}}\,({\it{state\/}})) \\ 
{\bf then }\=\+{\bf if }{\rm{car}}\,({\rm{xor-bvs}}\,({\it{state\/}})\index{xor-bvs}) $=$ {\tt{1}}$\;\;${\bf then }{\rm{high-bit-on}}\,({\it{state\/}})\index{high-bit-on} \\ 
{\bf else }{\rm{find-high-out-of-sync}}\,({\rm{delete-high-bits}}\,({\it{state\/}})\index{delete-high-bits})\index{find-high-out-of-sync}$\;${\bf  endif}\- \\ 
{\bf else }{\bf{f}}$\;${\bf  endif}\- \\ 
{\bf else }{\bf{f}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{smart-move} \\  
\=\+{\rm{smart-move}}\,({\it{state\/}}, {\it{size\/}})\index{smart-move} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{number-with-at-least}}\,({\it{state\/}}, {\tt{2}}, {\it{size\/}})\index{number-with-at-least} $=$ {\tt{0}} \\ 
{\bf then }{\rm{cons}}\,({\rm{col-with-at-least}}\,({\it{state\/}}, {\tt{1}}, {\it{size\/}})\index{col-with-at-least}, {\rm{nat-to-bv}}\,({\tt{0}}, {\it{size\/}})\index{nat-to-bv}) \\ 
{\bf elseif }{\rm{number-with-at-least}}\,({\it{state\/}}, {\tt{2}}, {\it{size\/}})\index{number-with-at-least} $=$ {\tt{1}} \\ 
{\bf then }{\rm{cons}}\,(\=\+{\rm{col-with-at-least}}\,({\it{state\/}}, {\tt{2}}, {\it{size\/}})\index{col-with-at-least}, \\ 
\=\+{\bf if }({\rm{number-with-at-least}}\,({\it{state\/}}, {\tt{1}}, {\it{size\/}})\index{number-with-at-least} ${}${\bf{mod}}${}$ {\tt{2}}) $=$ {\tt{0}} \\ 
{\bf then }{\rm{nat-to-bv}}\,({\tt{0}}, {\it{size\/}})\index{nat-to-bv} \\ 
{\bf else }{\rm{nat-to-bv}}\,({\tt{1}}, {\it{size\/}})\index{nat-to-bv}$\;${\bf  endif}\-)\- \\ 
{\bf else }\=\+{\bf let }\=\+{\it{badcol\/}}{\bf $\;$ be$\;\;$}{\rm{find-high-out-of-sync}}\,({\it{state\/}})\index{find-high-out-of-sync}\- \\ 
{\bf in} \\ 
{\rm{cons}}\,({\it{badcol\/}}, {\rm{xor-bvs}}\,({\rm{delete-pile}}\,({\it{badcol\/}}, {\it{state\/}})\index{delete-pile})\index{xor-bvs})$\;${\bf  endlet}\-$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{apply-move} \\  
{\rm{apply-move}}\,({\it{move\/}}, {\it{state\/}})\index{apply-move} $=$ {\rm{put}}\,({\rm{car}}\,({\it{move\/}}), {\rm{cdr}}\,({\it{move\/}}), {\it{state\/}})\index{put}
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{all-zeros} \\  
\=\+{\rm{all-zeros}}\,({\it{bv\/}})\index{all-zeros} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{bv\/}})$\;\;${\bf then }({\rm{car}}\,({\it{bv\/}}) $=$ {\tt{0}}) $\wedge$ {\rm{all-zeros}}\,({\rm{cdr}}\,({\it{bv\/}}))\index{all-zeros} \\ 
{\bf else }{\bf{t}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{loser-state} \\  
\=\+{\rm{loser-state}}\,({\it{state\/}}, {\it{size\/}})\index{loser-state} \\ 
$=$$\;\;\;\;$(\=\+(\=\+({\rm{number-with-at-least}}\,({\it{state\/}}, {\tt{2}}, {\it{size\/}})\index{number-with-at-least} $=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$(({\rm{number-with-at-least}}\,({\it{state\/}}, {\tt{1}}, {\it{size\/}})\index{number-with-at-least} ${}${\bf{mod}}${}$ {\tt{2}}) $=$ {\tt{1}}))\- \\ 
$\vee$$\;\;\;\;$(\=\+({\tt{0}} $<$ {\rm{number-with-at-least}}\,({\it{state\/}}, {\tt{2}}, {\it{size\/}})\index{number-with-at-least}) \\ 
$\wedge$$\;\;\;\;${\rm{all-zeros}}\,({\rm{xor-bvs}}\,({\it{state\/}})\index{xor-bvs})\index{all-zeros})\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{movep} \\  
\=\+{\rm{movep}}\,({\it{move\/}}, {\it{state\/}}, {\it{size\/}})\index{movep} \\ 
$=$$\;\;\;\;$(\=\+{\rm{lessp-bv}}\,({\rm{cdr}}\,({\it{move\/}}), {\rm{get}}\,({\rm{car}}\,({\it{move\/}}), {\it{state\/}})\index{get})\index{lessp-bv} \\ 
$\wedge$$\;\;\;\;$({\rm{length}}\,({\rm{cdr}}\,({\it{move\/}}))\index{length} $=$ {\it{size\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{bvp}}\,({\rm{cdr}}\,({\it{move\/}}))\index{bvp} \\ 
$\wedge$$\;\;\;\;$({\rm{car}}\,({\it{move\/}}) $<$ {\rm{length}}\,({\it{state\/}})\index{length}))\-\-
\end{tabbing}

\begin{verbatim};; the column of place has a 1 bit at the highest position 
;; whose xors are not 0
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{high-bit-out-of-sync} \\  
\=\+{\rm{high-bit-out-of-sync}}\,({\it{place\/}}, {\it{state\/}})\index{high-bit-out-of-sync} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{state\/}}) \\ 
{\bf then }\=\+{\bf if }{\rm{listp}}\,({\rm{car}}\,({\it{state\/}})) \\ 
{\bf then }\=\+(\=\+({\rm{car}}\,({\rm{get}}\,({\it{place\/}}, {\it{state\/}})\index{get}) $=$ {\tt{1}}) \\ 
$\wedge$$\;\;\;\;$({\rm{car}}\,({\rm{xor-bvs}}\,({\it{state\/}})\index{xor-bvs}) $=$ {\tt{1}}))\- \\ 
$\vee$$\;\;\;\;$(\=\+({\rm{car}}\,({\rm{xor-bvs}}\,({\it{state\/}})\index{xor-bvs}) $=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;${\rm{high-bit-out-of-sync}}\,(\=\+{\it{place\/}}, \\ 
{\rm{delete-high-bits}}\,({\it{state\/}})\index{delete-high-bits})\-\index{high-bit-out-of-sync})\-\- \\ 
{\bf else }{\bf{f}}$\;${\bf  endif}\- \\ 
{\bf else }{\bf{f}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{lessp-when-high-bit-recursion} \\  
\=\+{\rm{lessp-when-high-bit-recursion}}\,({\it{state\/}}, {\it{size\/}})\index{lessp-when-high-bit-recursion} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{size\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }{\rm{lessp-when-high-bit-recursion}}\,(\=\+{\rm{delete-high-bits}}\,({\it{state\/}})\index{delete-high-bits}, \\ 
{\it{size\/}} $-\;1$)\-\index{lessp-when-high-bit-recursion}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  equal-length-0 \\ \index{equal-length-0}
({\rm{length}}\,({\it{x\/}})\index{length} $=$ {\tt{0}}) $=$ ($\neg$ {\rm{listp}}\,({\it{x\/}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  equal-length-1 \\ \index{equal-length-1}
({\rm{length}}\,({\it{x\/}})\index{length} $=$ {\tt{1}}) $=$ ({\rm{listp}}\,({\it{x\/}}) $\wedge$ ($\neg$ {\rm{listp}}\,({\rm{cdr}}\,({\it{x\/}}))))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  good-state-of-size-delete-high-bits \\ \index{good-state-of-size-delete-high-!bits}
\=\+{\rm{good-state-of-size}}\,({\it{state\/}}, $1\;+$ {\it{x\/}})\index{good-state-of-size} \\ 
$\rightarrow$$\;\;\;\;${\rm{good-state-of-size}}\,({\rm{delete-high-bits}}\,({\it{state\/}})\index{delete-high-bits}, {\it{x\/}})\index{good-state-of-size}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  high-bit-out-of-sync-empty \\ \index{high-bit-out-of-sync-empty}
\=\+({\rm{good-state-of-size}}\,({\it{state\/}}, {\it{size\/}})\index{good-state-of-size} $\wedge$ ({\it{size\/}} $\simeq {\tt{0}}$)) \\ 
$\rightarrow$$\;\;\;\;$($\neg$ {\rm{high-bit-out-of-sync}}\,({\it{place\/}}, {\it{state\/}})\index{high-bit-out-of-sync})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  get-of-bad-place \\ \index{get-of-bad-place}
({\it{place\/}} $\not<$ {\rm{length}}\,({\it{state\/}})\index{length}) $\rightarrow$ ({\rm{get}}\,({\it{place\/}}, {\it{state\/}})\index{get} $=$ {\tt{0}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  listp-delete-high-bits \\ \index{listp-delete-high-bits}
{\rm{listp}}\,({\rm{delete-high-bits}}\,({\it{x\/}})\index{delete-high-bits}) $=$ {\rm{listp}}\,({\it{x\/}})
\end{tabbing}


\begin{tabbing}{\sc Definition}:\index{bv-not} \\  
\=\+{\rm{bv-not}}\,({\it{x\/}})\index{bv-not} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{x\/}} $=$ {\tt{0}}$\;\;${\bf then }{\tt{1}} \\ 
{\bf else }{\tt{0}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  bvp-xor-bv \\ \index{bvp-xor-bv}
{\rm{bvp}}\,({\rm{xor-bv}}\,({\it{x\/}}, {\it{y\/}})\index{xor-bv})\index{bvp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  bvp-xor-bvs \\ \index{bvp-xor-bvs}
{\rm{bvp}}\,({\rm{xor-bvs}}\,({\it{state\/}})\index{xor-bvs})\index{bvp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  equal-bitp-simplify \\ \index{equal-bitp-simplify}
({\rm{bitp}}\,({\it{x\/}})\index{bitp} $\wedge$ ({\it{x\/}} $\not=$ {\tt{0}})) $\rightarrow$ (({\it{x\/}} $=$ {\it{y\/}}) $=$ ({\it{y\/}} $=$ {\tt{1}}))
\end{tabbing}

\begin{verbatim};; make all bit equality constants into 0
\end{verbatim}\begin{tabbing}{\sc Theorem}:  equal-bit-1 \\ \index{equal-bit-1}
{\rm{bitp}}\,({\it{x\/}})\index{bitp} $\rightarrow$ (({\it{x\/}} $=$ {\tt{1}}) $=$ ({\it{x\/}} $\not=$ {\tt{0}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  bitp-car-bvp \\ \index{bitp-car-bvp}
{\rm{bvp}}\,({\it{x\/}})\index{bvp} $\rightarrow$ {\rm{bitp}}\,({\rm{car}}\,({\it{x\/}}))\index{bitp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  good-state-of-size-means-bvsp \\ \index{good-state-of-size-means-bvsp}
{\rm{good-state-of-size}}\,({\it{state\/}}, {\it{size\/}})\index{good-state-of-size} $\rightarrow$ {\rm{bvsp}}\,({\it{state\/}})\index{bvsp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  listp-xor-bv \\ \index{listp-xor-bv}
{\rm{listp}}\,({\rm{xor-bv}}\,({\it{x\/}}, {\it{y\/}})\index{xor-bv}) $=$ ({\rm{listp}}\,({\it{x\/}}) $\wedge$ {\rm{listp}}\,({\it{y\/}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  listp-xor-bvs \\ \index{listp-xor-bvs}
\=\+{\rm{good-state-of-size}}\,({\it{state\/}}, {\it{size\/}})\index{good-state-of-size} \\ 
$\rightarrow$$\;\;\;\;$({\rm{listp}}\,({\rm{xor-bvs}}\,({\it{state\/}})\index{xor-bvs}) $=$ ({\rm{listp}}\,({\it{state\/}}) $\wedge$ ({\tt{0}} $<$ {\it{size\/}})))\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  bvp-get \\ \index{bvp-get}
\=\+{\rm{good-state-of-size}}\,({\it{state\/}}, {\it{size\/}})\index{good-state-of-size} \\ 
$\rightarrow$$\;\;\;\;$({\rm{bvp}}\,({\rm{get}}\,({\it{place\/}}, {\it{state\/}})\index{get})\index{bvp} $=$ ({\it{place\/}} $<$ {\rm{length}}\,({\it{state\/}})\index{length}))\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  listp-get \\ \index{listp-get}
\=\+{\rm{good-state-of-size}}\,({\it{state\/}}, {\it{size\/}})\index{good-state-of-size} \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{listp}}\,({\rm{get}}\,({\it{place\/}}, {\it{state\/}})\index{get}) \\ 
$=$$\;\;\;\;$(({\it{place\/}} $<$ {\rm{length}}\,({\it{state\/}})\index{length}) $\wedge$ ({\tt{0}} $<$ {\it{size\/}})))\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  car-xor-bv \\ \index{car-xor-bv}
({\rm{listp}}\,({\it{x\/}}) $\wedge$ {\rm{listp}}\,({\it{y\/}})) $\rightarrow$ ({\rm{car}}\,({\rm{xor-bv}}\,({\it{x\/}}, {\it{y\/}})\index{xor-bv}) $=$ {\rm{xor}}\,({\rm{car}}\,({\it{x\/}}), {\rm{car}}\,({\it{y\/}}))\index{xor})
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{lessp-bv-recursion} \\  
\=\+{\rm{lessp-bv-recursion}}\,({\it{list\/}}, {\it{size\/}})\index{lessp-bv-recursion} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{size\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }{\rm{lessp-bv-recursion}}\,({\rm{cdr}}\,({\it{list\/}}), {\it{size\/}} $-\;1$)\index{lessp-bv-recursion}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{firstn} \\  
\=\+{\rm{firstn}}\,({\it{list\/}}, {\it{n\/}})\index{firstn} \\ 
$=$$\;\;\;\;$\=\+{\bf if }$\neg$ {\rm{listp}}\,({\it{list\/}})$\;\;${\bf then }{\it{list\/}} \\ 
{\bf elseif }{\it{n\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\bf{nil}} \\ 
{\bf else }{\rm{cons}}\,({\rm{car}}\,({\it{list\/}}), {\rm{firstn}}\,({\rm{cdr}}\,({\it{list\/}}), {\it{n\/}} $-\;1$)\index{firstn})$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{min} \\  
\=\+{\rm{min}}\,({\it{x\/}}, {\it{y\/}})\index{min} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{x\/}} $<$ {\it{y\/}}$\;\;${\bf then }{\rm{fix}}\,({\it{x\/}}) \\ 
{\bf else }{\rm{fix}}\,({\it{y\/}})$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  xor-bv-inverse \\ \index{xor-bv-inverse}
{\rm{xor-bv}}\,({\it{a\/}}, {\rm{xor-bv}}\,({\it{a\/}}, {\it{b\/}})\index{xor-bv})\index{xor-bv} $=$ {\rm{firstn}}\,({\rm{fix-xor-bv}}\,({\it{b\/}})\index{fix-xor-bv}, {\rm{min}}\,({\rm{length}}\,({\it{a\/}})\index{length}, {\rm{length}}\,({\it{b\/}})\index{length})\index{min})\index{firstn}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  xor-bv-fix-xor-bv \\ \index{xor-bv-fix-xor-bv}
\=\+({\rm{xor-bv}}\,({\rm{fix-xor-bv}}\,({\it{x\/}})\index{fix-xor-bv}, {\it{y\/}})\index{xor-bv} $=$ {\rm{xor-bv}}\,({\it{x\/}}, {\it{y\/}})\index{xor-bv}) \\ 
$\wedge$$\;\;\;\;$({\rm{xor-bv}}\,({\it{y\/}}, {\rm{fix-xor-bv}}\,({\it{x\/}})\index{fix-xor-bv})\index{xor-bv} $=$ {\rm{xor-bv}}\,({\it{y\/}}, {\it{x\/}})\index{xor-bv})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  firstn-noop \\ \index{firstn-noop}
({\it{x\/}} $\not<$ {\rm{length}}\,({\it{list\/}})\index{length}) $\rightarrow$ ({\rm{firstn}}\,({\it{list\/}}, {\it{x\/}})\index{firstn} $=$ {\it{list\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  xor-bvs-delete-high-bits \\ \index{xor-bvs-delete-high-bits}
\=\+{\rm{good-state-of-size}}\,({\it{state\/}}, {\it{size\/}})\index{good-state-of-size} \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{xor-bvs}}\,({\rm{delete-high-bits}}\,({\it{state\/}})\index{delete-high-bits})\index{xor-bvs} \\ 
$=$$\;\;\;\;$\=\+{\bf if }($\neg$ {\rm{listp}}\,({\it{state\/}})) $\vee$ ({\tt{1}} $\not<$ {\it{size\/}})$\;\;${\bf then }{\bf{nil}} \\ 
{\bf else }{\rm{cdr}}\,({\rm{xor-bvs}}\,({\it{state\/}})\index{xor-bvs})$\;${\bf  endif}\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  length-xor-bvs \\ \index{length-xor-bvs}
\=\+{\rm{good-state-of-size}}\,({\it{state\/}}, {\it{size\/}})\index{good-state-of-size} \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{length}}\,({\rm{xor-bvs}}\,({\it{state\/}})\index{xor-bvs})\index{length} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{state\/}})$\;\;${\bf then }{\rm{fix}}\,({\it{size\/}}) \\ 
{\bf else }{\tt{0}}$\;${\bf  endif}\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  listp-delete-pile \\ \index{listp-delete-pile}
\=\+{\rm{listp}}\,({\rm{delete-pile}}\,({\it{place\/}}, {\it{state\/}})\index{delete-pile}) \\ 
$=$$\;\;\;\;$({\rm{listp}}\,({\it{state\/}}) $\wedge$ ($\neg$ (({\it{place\/}} $\simeq {\tt{0}}$) $\wedge$ ($\neg$ {\rm{listp}}\,({\rm{cdr}}\,({\it{state\/}}))))))\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  xor-bvs-delete-pile \\ \index{xor-bvs-delete-pile}
\=\+({\rm{good-state-of-size}}\,({\it{state\/}}, {\it{size\/}})\index{good-state-of-size} $\wedge$ ({\it{place\/}} $<$ {\rm{length}}\,({\it{state\/}})\index{length})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{xor-bvs}}\,({\rm{delete-pile}}\,({\it{place\/}}, {\it{state\/}})\index{delete-pile})\index{xor-bvs} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\tt{1}} $<$ {\rm{length}}\,({\it{state\/}})\index{length} \\ 
{\bf then }{\rm{xor-bv}}\,({\rm{get}}\,({\it{place\/}}, {\it{state\/}})\index{get}, {\rm{xor-bvs}}\,({\it{state\/}})\index{xor-bvs})\index{xor-bv} \\ 
{\bf else }{\bf{nil}}$\;${\bf  endif}\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  listp-delete-pile-delete-high-bits \\ \index{listp-delete-pile-delete-high-bit!s}
\=\+{\rm{listp}}\,({\rm{delete-pile}}\,({\it{place\/}}, {\rm{delete-high-bits}}\,({\it{state\/}})\index{delete-high-bits})\index{delete-pile}) \\ 
$=$$\;\;\;\;${\rm{listp}}\,({\rm{delete-pile}}\,({\it{place\/}}, {\it{state\/}})\index{delete-pile})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  get-delete-high-bits \\ \index{get-delete-high-bits}
{\rm{get}}\,({\it{place\/}}, {\rm{delete-high-bits}}\,({\it{state\/}})\index{delete-high-bits})\index{get} $=$ {\rm{cdr}}\,({\rm{get}}\,({\it{place\/}}, {\it{state\/}})\index{get})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  delete-pile-delete-high-bits \\ \index{delete-pile-delete-high-bits}
\=\+{\rm{delete-pile}}\,({\it{place\/}}, {\rm{delete-high-bits}}\,({\it{state\/}})\index{delete-high-bits})\index{delete-pile} \\ 
$=$$\;\;\;\;${\rm{delete-high-bits}}\,({\rm{delete-pile}}\,({\it{place\/}}, {\it{state\/}})\index{delete-pile})\index{delete-high-bits}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  good-state-of-size-delete-pile \\ \index{good-state-of-size-delete-pile}
\=\+{\rm{good-state-of-size}}\,({\it{state\/}}, {\it{size\/}})\index{good-state-of-size} \\ 
$\rightarrow$$\;\;\;\;${\rm{good-state-of-size}}\,({\rm{delete-pile}}\,({\it{place\/}}, {\it{state\/}})\index{delete-pile}, {\it{size\/}})\index{good-state-of-size}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  silly-listp-cdr \\ \index{silly-listp-cdr}
({\tt{1}} $<$ {\rm{length}}\,({\it{x\/}})\index{length}) $\rightarrow$ {\rm{listp}}\,({\rm{cdr}}\,({\it{x\/}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  numberp-car-bv \\ \index{numberp-car-bv}
{\rm{bvp}}\,({\it{bv\/}})\index{bvp} $\rightarrow$ ({\rm{car}}\,({\it{bv\/}}) $\in\;${\bf{N}}${}$)
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  length-delete-high-bits \\ \index{length-delete-high-bits}
{\rm{length}}\,({\rm{delete-high-bits}}\,({\it{x\/}})\index{delete-high-bits})\index{length} $=$ {\rm{length}}\,({\it{x\/}})\index{length}
\end{tabbing}

\begin{verbatim};; special version to help with free variable problem of next lemma
\end{verbatim}\begin{tabbing}{\sc Theorem}:  xor-bvs-delete-high-bits-2 \\ \index{xor-bvs-delete-high-bits-2}
\=\+(({\it{size\/}} $\not=$ {\tt{0}}) $\wedge$ {\rm{good-state-of-size}}\,({\it{state\/}}, {\it{size\/}})\index{good-state-of-size}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{xor-bvs}}\,({\rm{delete-high-bits}}\,({\it{state\/}})\index{delete-high-bits})\index{xor-bvs} \\ 
$=$$\;\;\;\;$\=\+{\bf if }($\neg$ {\rm{listp}}\,({\it{state\/}})) $\vee$ ({\tt{1}} $\not<$ {\it{size\/}})$\;\;${\bf then }{\bf{nil}} \\ 
{\bf else }{\rm{cdr}}\,({\rm{xor-bvs}}\,({\it{state\/}})\index{xor-bvs})$\;${\bf  endif}\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  lessp-when-high-bit-out-of-sync-helper \\ \index{lessp-when-high-bit-out-of-sync!-helper}
\=\+(\=\+{\rm{good-state-of-size}}\,({\it{state\/}}, {\it{size\/}})\index{good-state-of-size} \\ 
$\wedge$$\;\;\;\;$({\it{place\/}} $<$ {\rm{length}}\,({\it{state\/}})\index{length}) \\ 
$\wedge$$\;\;\;\;$({\tt{1}} $<$ {\rm{length}}\,({\it{state\/}})\index{length}) \\ 
$\wedge$$\;\;\;\;${\rm{high-bit-out-of-sync}}\,({\it{place\/}}, {\it{state\/}})\index{high-bit-out-of-sync})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{lessp-bv}}\,({\rm{xor-bvs}}\,({\rm{delete-pile}}\,({\it{place\/}}, {\it{state\/}})\index{delete-pile})\index{xor-bvs}, {\rm{get}}\,({\it{place\/}}, {\it{state\/}})\index{get})\index{lessp-bv}\-
\end{tabbing}


\noindent{\sc Event}:   Disable xor-bvs-delete-high-bits-2.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  high-bit-out-of-sync-trivial \\ \index{high-bit-out-of-sync-trivial}
({\it{place\/}} $\not<$ {\rm{length}}\,({\it{state\/}})\index{length}) $\rightarrow$ ($\neg$ {\rm{high-bit-out-of-sync}}\,({\it{place\/}}, {\it{state\/}})\index{high-bit-out-of-sync})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  lessp-when-high-bit-out-of-sync \\ \index{lessp-when-high-bit-out-of-sync}
\=\+(\=\+{\rm{good-state-of-size}}\,({\it{state\/}}, {\it{size\/}})\index{good-state-of-size} \\ 
$\wedge$$\;\;\;\;$({\tt{1}} $<$ {\rm{length}}\,({\it{state\/}})\index{length}) \\ 
$\wedge$$\;\;\;\;${\rm{high-bit-out-of-sync}}\,({\it{place\/}}, {\it{state\/}})\index{high-bit-out-of-sync})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{lessp-bv}}\,({\rm{xor-bvs}}\,({\rm{delete-pile}}\,({\it{place\/}}, {\it{state\/}})\index{delete-pile})\index{xor-bvs}, {\rm{get}}\,({\it{place\/}}, {\it{state\/}})\index{get})\index{lessp-bv}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  bitp-car-xor-bvs \\ \index{bitp-car-xor-bvs}
{\rm{bitp}}\,({\rm{car}}\,({\rm{xor-bvs}}\,({\it{bvs\/}})\index{xor-bvs}))\index{bitp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  high-bit-on-works \\ \index{high-bit-on-works}
\=\+(({\rm{car}}\,({\rm{xor-bvs}}\,({\it{state\/}})\index{xor-bvs}) $=$ {\tt{1}}) $\wedge$ {\rm{bvsp}}\,({\it{state\/}})\index{bvsp}) \\ 
$\rightarrow$$\;\;\;\;$({\rm{car}}\,({\rm{get}}\,({\rm{high-bit-on}}\,({\it{state\/}})\index{high-bit-on}, {\it{state\/}})\index{get}) $=$ {\tt{1}})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  all-zeros-length-1 \\ \index{all-zeros-length-1}
({\rm{length}}\,({\it{x\/}})\index{length} $=$ {\tt{1}}) $\rightarrow$ ({\rm{all-zeros}}\,({\it{x\/}})\index{all-zeros} $=$ ({\rm{car}}\,({\it{x\/}}) $=$ {\tt{0}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  all-zeros-xor-bvs-simple \\ \index{all-zeros-xor-bvs-simple}
\=\+({\rm{good-state-of-size}}\,({\it{state\/}}, {\it{size\/}})\index{good-state-of-size} $\wedge$ ({\it{size\/}} $<$ {\tt{2}})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{all-zeros}}\,({\rm{xor-bvs}}\,({\it{state\/}})\index{xor-bvs})\index{all-zeros} \\ 
$=$$\;\;\;\;$(\=\+({\it{size\/}} $\simeq {\tt{0}}$) \\ 
$\vee$$\;\;\;\;$($\neg$ {\rm{listp}}\,({\it{state\/}})) \\ 
$\vee$$\;\;\;\;$({\rm{car}}\,({\rm{xor-bvs}}\,({\it{state\/}})\index{xor-bvs}) $=$ {\tt{0}}))\-)\-\-
\end{tabbing}
             
\begin{tabbing}{\sc Theorem}:  find-high-out-of-sync-works \\ \index{find-high-out-of-sync-works}
\=\+(($\neg$ {\rm{all-zeros}}\,({\rm{xor-bvs}}\,({\it{state\/}})\index{xor-bvs})\index{all-zeros}) $\wedge$ {\rm{good-state-of-size}}\,({\it{state\/}}, {\it{size\/}})\index{good-state-of-size}) \\ 
$\rightarrow$$\;\;\;\;${\rm{high-bit-out-of-sync}}\,({\rm{find-high-out-of-sync}}\,({\it{state\/}})\index{find-high-out-of-sync}, {\it{state\/}})\index{high-bit-out-of-sync}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  bvp-nat-to-bv \\ \index{bvp-nat-to-bv}
{\rm{bvp}}\,({\rm{nat-to-bv}}\,({\it{nat\/}}, {\it{size\/}})\index{nat-to-bv})\index{bvp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  silly-lessp-sub1-exp-length \\ \index{silly-lessp-sub1-exp-length}
(({\it{nat\/}} $\not<$ {\rm{exp}}\,({\tt{2}}, {\rm{length}}\,({\it{bv\/}})\index{length})\index{exp}) $\wedge$ {\rm{bvp}}\,({\it{bv\/}})\index{bvp}) $\rightarrow$ ({\it{nat\/}} $\not<$ {\rm{bv-to-nat}}\,({\it{bv\/}})\index{bv-to-nat})
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{all-ones} \\  
\=\+{\rm{all-ones}}\,({\it{size\/}})\index{all-ones} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{size\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\bf{nil}} \\ 
{\bf else }{\rm{cons}}\,({\tt{1}}, {\rm{all-ones}}\,({\it{size\/}} $-\;1$)\index{all-ones})$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  nat-to-bv-is-all-ones \\ \index{nat-to-bv-is-all-ones}
({\it{nat\/}} $\not<$ {\rm{exp}}\,({\tt{2}}, {\it{size\/}})\index{exp}) $\rightarrow$ ({\rm{nat-to-bv}}\,({\it{nat\/}}, {\it{size\/}})\index{nat-to-bv} $=$ {\rm{all-ones}}\,({\it{size\/}})\index{all-ones})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  length-all-ones \\ \index{length-all-ones}
{\rm{length}}\,({\rm{all-ones}}\,({\it{size\/}})\index{all-ones})\index{length} $=$ {\rm{fix}}\,({\it{size\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  bvp-all-ones \\ \index{bvp-all-ones}
{\rm{bvp}}\,({\rm{all-ones}}\,({\it{size\/}})\index{all-ones})\index{bvp}
\end{tabbing}
      
\begin{tabbing}{\sc Theorem}:  lessp-bv-all-ones-arg1 \\ \index{lessp-bv-all-ones-arg1}
{\rm{bvp}}\,({\it{bv\/}})\index{bvp} $\rightarrow$ ($\neg$ {\rm{lessp-bv}}\,({\rm{all-ones}}\,({\it{size\/}})\index{all-ones}, {\it{bv\/}})\index{lessp-bv})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  lessp-bv-all-ones-arg2 \\ \index{lessp-bv-all-ones-arg2}
\=\+(({\rm{length}}\,({\it{bv\/}})\index{length} $=$ {\it{size\/}}) $\wedge$ {\rm{bvp}}\,({\it{bv\/}})\index{bvp}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{lessp-bv}}\,({\it{bv\/}}, {\rm{all-ones}}\,({\it{size\/}})\index{all-ones})\index{lessp-bv} \\ 
$=$$\;\;\;\;$({\rm{bv-to-nat}}\,({\it{bv\/}})\index{bv-to-nat} $<$ ({\rm{exp}}\,({\tt{2}}, {\it{size\/}})\index{exp} $-\;1$)))\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  lessp-bv-nat-to-bv \\ \index{lessp-bv-nat-to-bv}
\=\+(({\rm{length}}\,({\it{bv\/}})\index{length} $=$ {\rm{fix}}\,({\it{size\/}})) $\wedge$ ({\it{nat\/}} $<$ {\rm{exp}}\,({\tt{2}}, {\it{size\/}})\index{exp}) $\wedge$ {\rm{bvp}}\,({\it{bv\/}})\index{bvp}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{lessp-bv}}\,({\rm{nat-to-bv}}\,({\it{nat\/}}, {\it{size\/}})\index{nat-to-bv}, {\it{bv\/}})\index{lessp-bv} $=$ ({\it{nat\/}} $<$ {\rm{bv-to-nat}}\,({\it{bv\/}})\index{bv-to-nat})) \\ 
$\wedge$$\;\;\;\;$({\rm{lessp-bv}}\,({\it{bv\/}}, {\rm{nat-to-bv}}\,({\it{nat\/}}, {\it{size\/}})\index{nat-to-bv})\index{lessp-bv} $=$ ({\rm{bv-to-nat}}\,({\it{bv\/}})\index{bv-to-nat} $<$ {\it{nat\/}})))\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  length-car-state \\ \index{length-car-state}
\=\+{\rm{good-state-of-size}}\,({\it{state\/}}, {\it{size\/}})\index{good-state-of-size} \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{length}}\,({\rm{car}}\,({\it{state\/}}))\index{length} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{state\/}})$\;\;${\bf then }{\rm{fix}}\,({\it{size\/}}) \\ 
{\bf else }{\tt{0}}$\;${\bf  endif}\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  bvp-car \\ \index{bvp-car}
({\rm{bvsp}}\,({\it{x\/}})\index{bvsp} $\wedge$ {\rm{listp}}\,({\it{x\/}})) $\rightarrow$ {\rm{bvp}}\,({\rm{car}}\,({\it{x\/}}))\index{bvp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  lessp-bv-zero \\ \index{lessp-bv-zero}
({\it{zero\/}} $\simeq {\tt{0}}$) $\rightarrow$ ($\neg$ {\rm{lessp-bv}}\,({\it{x\/}}, {\rm{nat-to-bv}}\,({\it{zero\/}}, {\it{size\/}})\index{nat-to-bv})\index{lessp-bv})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  number-with-at-least-zero \\ \index{number-with-at-least-zero}
({\it{zero\/}} $\simeq {\tt{0}}$) $\rightarrow$ ({\rm{number-with-at-least}}\,({\it{bv\/}}, {\it{zero\/}}, {\it{size\/}})\index{number-with-at-least} $=$ {\rm{length}}\,({\it{bv\/}})\index{length})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  lessp-1-exp \\ \index{lessp-1-exp}
({\tt{1}} $<$ {\rm{exp}}\,({\it{x\/}}, {\it{y\/}})\index{exp}) $=$ (({\tt{1}} $<$ {\it{x\/}}) $\wedge$ ({\it{y\/}} $\not\simeq {\tt{0}}$))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  lessp-x-exp-x-y \\ \index{lessp-x-exp-x-y}
({\it{x\/}} $<$ {\rm{exp}}\,({\it{x\/}}, {\it{y\/}})\index{exp}) $=$ ((({\it{x\/}} $\simeq {\tt{0}}$) $\wedge$ ({\it{y\/}} $\simeq {\tt{0}}$)) $\vee$ (({\tt{1}} $<$ {\it{x\/}}) $\wedge$ ({\tt{1}} $<$ {\it{y\/}})))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  lessp-bv-col-get-with-at-least \\ \index{lessp-bv-col-get-with-at-least}
\=\+(\=\+({\it{x\/}} $<$ {\it{y\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{y\/}} $<$ {\rm{exp}}\,({\tt{2}}, {\it{size\/}})\index{exp}) \\ 
$\wedge$$\;\;\;\;${\rm{good-state-of-size}}\,({\it{state\/}}, {\it{size\/}})\index{good-state-of-size} \\ 
$\wedge$$\;\;\;\;$({\rm{number-with-at-least}}\,({\it{state\/}}, {\it{y\/}}, {\it{size\/}})\index{number-with-at-least} $\not\simeq {\tt{0}}$))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{lessp-bv}}\,({\rm{nat-to-bv}}\,({\it{x\/}}, {\it{size\/}})\index{nat-to-bv}, {\rm{get}}\,({\rm{col-with-at-least}}\,({\it{state\/}}, {\it{y\/}}, {\it{size\/}})\index{col-with-at-least}, {\it{state\/}})\index{get})\index{lessp-bv}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  lessp-1-x-means-not-zerop-x \\ \index{lessp-1-x-means-not-zerop-x}
({\tt{1}} $<$ {\it{x\/}}) $\rightarrow$ ({\it{x\/}} $\not\simeq {\tt{0}}$)
\end{tabbing}


\begin{tabbing}{\sc Theorem}:  length-xor-bvs-delete-pile \\ \index{length-xor-bvs-delete-pile}
\=\+(({\tt{1}} $<$ {\rm{length}}\,({\it{state\/}})\index{length}) $\wedge$ {\rm{good-state-of-size}}\,({\it{state\/}}, {\it{size\/}})\index{good-state-of-size}) \\ 
$\rightarrow$$\;\;\;\;$({\rm{length}}\,({\rm{xor-bvs}}\,({\rm{delete-pile}}\,({\it{n\/}}, {\it{state\/}})\index{delete-pile})\index{xor-bvs})\index{length} $=$ {\rm{fix}}\,({\it{size\/}}))\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  high-bit-on-reasonable \\ \index{high-bit-on-reasonable}
\=\+(({\rm{car}}\,({\rm{xor-bvs}}\,({\it{state\/}})\index{xor-bvs}) $=$ {\tt{1}}) $\wedge$ {\rm{good-state-of-size}}\,({\it{state\/}}, {\it{size\/}})\index{good-state-of-size}) \\ 
$\rightarrow$$\;\;\;\;$({\rm{high-bit-on}}\,({\it{state\/}})\index{high-bit-on} $<$ {\rm{length}}\,({\it{state\/}})\index{length})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  find-high-out-of-sync-reasonable \\ \index{find-high-out-of-sync-reasonable}
\=\+({\rm{listp}}\,({\it{state\/}}) $\wedge$ {\rm{good-state-of-size}}\,({\it{state\/}}, {\it{size\/}})\index{good-state-of-size}) \\ 
$\rightarrow$$\;\;\;\;$({\rm{find-high-out-of-sync}}\,({\it{state\/}})\index{find-high-out-of-sync} $<$ {\rm{length}}\,({\it{state\/}})\index{length})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  col-with-at-least-reasonable \\ \index{col-with-at-least-reasonable}
\=\+(({\rm{number-with-at-least}}\,({\it{state\/}}, {\it{n\/}}, {\it{size\/}})\index{number-with-at-least} $\not\simeq {\tt{0}}$) $\wedge$ {\rm{good-state-of-size}}\,({\it{state\/}}, {\it{size\/}})\index{good-state-of-size}) \\ 
$\rightarrow$$\;\;\;\;$({\rm{col-with-at-least}}\,({\it{state\/}}, {\it{n\/}}, {\it{size\/}})\index{col-with-at-least} $<$ {\rm{length}}\,({\it{state\/}})\index{length})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  lessp-length \\ \index{lessp-length}
({\it{n\/}} $<$ {\rm{length}}\,({\it{state\/}})\index{length}) $\rightarrow$ {\rm{listp}}\,({\it{state\/}})
\end{tabbing}


\noindent{\sc Event}:   Disable equal-bitp-simplify.

\addvspace{18pt}



\begin{tabbing}{\sc Theorem}:  listp-nat-to-bv \\ \index{listp-nat-to-bv}
{\rm{listp}}\,({\rm{nat-to-bv}}\,({\it{n\/}}, {\it{size\/}})\index{nat-to-bv}) $=$ ({\it{size\/}} $\not\simeq {\tt{0}}$)
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  number-with-at-least-simple \\ \index{number-with-at-least-simple}
\=\+({\rm{good-state-of-size}}\,({\it{state\/}}, {\it{size\/}})\index{good-state-of-size} $\wedge$ ({\it{size\/}} $\simeq {\tt{0}}$)) \\ 
$\rightarrow$$\;\;\;\;$({\rm{number-with-at-least}}\,({\it{state\/}}, {\it{n\/}}, {\it{size\/}})\index{number-with-at-least} $=$ {\rm{length}}\,({\it{state\/}})\index{length})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  bitp-car \\ \index{bitp-car}
{\rm{bvp}}\,({\it{bv\/}})\index{bvp} $\rightarrow$ {\rm{bitp}}\,({\rm{car}}\,({\it{bv\/}}))\index{bitp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  car-xor-bv-better \\ \index{car-xor-bv-better}
\=\+{\rm{car}}\,({\rm{xor-bv}}\,({\it{x\/}}, {\it{y\/}})\index{xor-bv}) \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{x\/}}) $\wedge$ {\rm{listp}}\,({\it{y\/}})$\;\;${\bf then }{\rm{xor}}\,({\rm{car}}\,({\it{x\/}}), {\rm{car}}\,({\it{y\/}}))\index{xor} \\ 
{\bf else }{\tt{0}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  xor-bv-inverse-2 \\ \index{xor-bv-inverse-2}
{\rm{xor-bv}}\,({\it{b\/}}, {\rm{xor-bv}}\,({\it{a\/}}, {\it{a\/}})\index{xor-bv})\index{xor-bv} $=$ {\rm{firstn}}\,({\rm{fix-xor-bv}}\,({\it{b\/}})\index{fix-xor-bv}, {\rm{min}}\,({\rm{length}}\,({\it{a\/}})\index{length}, {\rm{length}}\,({\it{b\/}})\index{length})\index{min})\index{firstn}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  length-fix-xor-bv \\ \index{length-fix-xor-bv}
{\rm{length}}\,({\rm{fix-xor-bv}}\,({\it{x\/}})\index{fix-xor-bv})\index{length} $=$ {\rm{length}}\,({\it{x\/}})\index{length}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  xor-bvs-put \\ \index{xor-bvs-put}
\=\+(\=\+{\rm{good-state-of-size}}\,({\it{state\/}}, {\it{size\/}})\index{good-state-of-size} \\ 
$\wedge$$\;\;\;\;$({\rm{length}}\,({\it{value\/}})\index{length} $=$ {\it{size\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{place\/}} $<$ {\rm{length}}\,({\it{state\/}})\index{length}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{xor-bvs}}\,({\rm{put}}\,({\it{place\/}}, {\it{value\/}}, {\it{state\/}})\index{put})\index{xor-bvs} \\ 
$=$$\;\;\;\;${\rm{xor-bv}}\,({\rm{get}}\,({\it{place\/}}, {\it{state\/}})\index{get}, {\rm{xor-bv}}\,({\it{value\/}}, {\rm{xor-bvs}}\,({\it{state\/}})\index{xor-bvs})\index{xor-bv})\index{xor-bv})\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{triple-cdr-induction} \\  
\=\+{\rm{triple-cdr-induction}}\,({\it{a\/}}, {\it{b\/}}, {\it{c\/}})\index{triple-cdr-induction} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{a\/}}) $\wedge$ {\rm{listp}}\,({\it{b\/}}) $\wedge$ {\rm{listp}}\,({\it{c\/}}) \\ 
{\bf then }{\rm{triple-cdr-induction}}\,({\rm{cdr}}\,({\it{a\/}}), {\rm{cdr}}\,({\it{b\/}}), {\rm{cdr}}\,({\it{c\/}}))\index{triple-cdr-induction} \\ 
{\bf else }{\bf{t}}$\;${\bf  endif}\-\-
\end{tabbing}

      
\begin{tabbing}{\sc Theorem}:  all-zeros-xor-bv-identity \\ \index{all-zeros-xor-bv-identity}
\=\+(({\rm{length}}\,({\it{a\/}})\index{length} $=$ {\rm{length}}\,({\it{b\/}})\index{length}) $\wedge$ ({\rm{length}}\,({\it{b\/}})\index{length} $=$ {\rm{length}}\,({\it{c\/}})\index{length}) $\wedge$ {\rm{all-zeros}}\,({\it{c\/}})\index{all-zeros}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{all-zeros}}\,({\rm{xor-bv}}\,({\it{a\/}}, {\rm{xor-bv}}\,({\it{b\/}}, {\it{c\/}})\index{xor-bv})\index{xor-bv})\index{all-zeros} \\ 
$=$$\;\;\;\;$({\rm{fix-xor-bv}}\,({\it{a\/}})\index{fix-xor-bv} $=$ {\rm{fix-xor-bv}}\,({\it{b\/}})\index{fix-xor-bv}))\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  length-get \\ \index{length-get}
\=\+({\rm{good-state-of-size}}\,({\it{state\/}}, {\it{size\/}})\index{good-state-of-size} $\wedge$ ({\it{place\/}} $<$ {\rm{length}}\,({\it{state\/}})\index{length})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{length}}\,({\rm{get}}\,({\it{place\/}}, {\it{state\/}})\index{get})\index{length} $=$ {\rm{fix}}\,({\it{size\/}}))\-
\end{tabbing}
             
\begin{tabbing}{\sc Theorem}:  all-zeros-xor-bvs-put \\ \index{all-zeros-xor-bvs-put}
\=\+(\=\+{\rm{all-zeros}}\,({\rm{xor-bvs}}\,({\it{state\/}})\index{xor-bvs})\index{all-zeros} \\ 
$\wedge$$\;\;\;\;${\rm{good-state-of-size}}\,({\it{state\/}}, {\it{size\/}})\index{good-state-of-size} \\ 
$\wedge$$\;\;\;\;$({\rm{length}}\,({\it{value\/}})\index{length} $=$ {\it{size\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{place\/}} $<$ {\rm{length}}\,({\it{state\/}})\index{length}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{all-zeros}}\,({\rm{xor-bvs}}\,({\rm{put}}\,({\it{place\/}}, {\it{value\/}}, {\it{state\/}})\index{put})\index{xor-bvs})\index{all-zeros} \\ 
$=$$\;\;\;\;$({\rm{fix-xor-bv}}\,({\it{value\/}})\index{fix-xor-bv} $=$ {\rm{get}}\,({\it{place\/}}, {\it{state\/}})\index{get}))\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  lessp-bv-x-x \\ \index{lessp-bv-x-x}
$\neg$ {\rm{lessp-bv}}\,({\it{x\/}}, {\it{x\/}})\index{lessp-bv}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  put-get \\ \index{put-get}
({\it{x\/}} $<$ {\rm{length}}\,({\it{state\/}})\index{length}) $\rightarrow$ ({\rm{put}}\,({\it{x\/}}, {\rm{get}}\,({\it{x\/}}, {\it{state\/}})\index{get}, {\it{state\/}})\index{put} $=$ {\it{state\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  get-means-number-with-at-least \\ \index{get-means-number-with-at-least}
\=\+(($\neg$ {\rm{lessp-bv}}\,({\rm{get}}\,({\it{x\/}}, {\it{state\/}})\index{get}, {\rm{nat-to-bv}}\,({\it{n\/}}, {\it{size\/}})\index{nat-to-bv})\index{lessp-bv}) $\wedge$ ({\it{x\/}} $<$ {\rm{length}}\,({\it{state\/}})\index{length})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{number-with-at-least}}\,({\it{state\/}}, {\it{n\/}}, {\it{size\/}})\index{number-with-at-least} $\not=$ {\tt{0}})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  number-with-at-least-put \\ \index{number-with-at-least-put}
\=\+(\=\+({\it{p\/}} $<$ {\rm{length}}\,({\it{state\/}})\index{length}) \\ 
$\wedge$$\;\;\;\;${\rm{good-state-of-size}}\,({\it{state\/}}, {\it{size\/}})\index{good-state-of-size} \\ 
$\wedge$$\;\;\;\;$({\rm{length}}\,({\it{v\/}})\index{length} $=$ {\it{size\/}}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{number-with-at-least}}\,({\rm{put}}\,({\it{p\/}}, {\it{v\/}}, {\it{state\/}})\index{put}, {\it{n\/}}, {\it{size\/}})\index{number-with-at-least} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{lessp-bv}}\,({\rm{get}}\,({\it{p\/}}, {\it{state\/}})\index{get}, {\rm{nat-to-bv}}\,({\it{n\/}}, {\it{size\/}})\index{nat-to-bv})\index{lessp-bv} \\ 
{\bf then }\=\+{\bf if }{\rm{lessp-bv}}\,({\it{v\/}}, {\rm{nat-to-bv}}\,({\it{n\/}}, {\it{size\/}})\index{nat-to-bv})\index{lessp-bv} \\ 
{\bf then }{\rm{number-with-at-least}}\,({\it{state\/}}, {\it{n\/}}, {\it{size\/}})\index{number-with-at-least} \\ 
{\bf else }$1\;+$ {\rm{number-with-at-least}}\,({\it{state\/}}, {\it{n\/}}, {\it{size\/}})\index{number-with-at-least}$\;${\bf  endif}\- \\ 
{\bf elseif }{\rm{lessp-bv}}\,({\it{v\/}}, {\rm{nat-to-bv}}\,({\it{n\/}}, {\it{size\/}})\index{nat-to-bv})\index{lessp-bv} \\ 
{\bf then }{\rm{number-with-at-least}}\,({\it{state\/}}, {\it{n\/}}, {\it{size\/}})\index{number-with-at-least} $-\;1$ \\ 
{\bf else }{\rm{number-with-at-least}}\,({\it{state\/}}, {\it{n\/}}, {\it{size\/}})\index{number-with-at-least}$\;${\bf  endif}\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  all-zeros-xor-bvs-when-lone-big-simple \\ \index{all-zeros-xor-bvs-when-lone-big!-simple}
\=\+({\rm{good-state-of-size}}\,({\it{state\/}}, {\tt{1}})\index{good-state-of-size} $\wedge$ ({\rm{number-with-at-least}}\,({\it{state\/}}, {\tt{1}}, {\tt{1}})\index{number-with-at-least} $=$ {\tt{1}})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{car}}\,({\rm{xor-bvs}}\,({\it{state\/}})\index{xor-bvs}) $=$ {\tt{1}})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  plus-exp-2-x-exp-2-x \\ \index{plus-exp-2-x-exp-2-x}
({\rm{exp}}\,({\tt{2}}, {\it{x\/}})\index{exp} $+$ {\rm{exp}}\,({\tt{2}}, {\it{x\/}})\index{exp}) $=$ {\rm{exp}}\,({\tt{2}}, $1\;+$ {\it{x\/}})\index{exp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  lessp-exp-exp \\ \index{lessp-exp-exp}
\=\+({\rm{exp}}\,({\it{x\/}}, {\it{y\/}})\index{exp} $<$ {\rm{exp}}\,({\it{x\/}}, {\it{z\/}})\index{exp}) \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{x\/}} $\simeq {\tt{0}}$$\;\;${\bf then }({\it{y\/}} $\not\simeq {\tt{0}}$) $\wedge$ ({\it{z\/}} $\simeq {\tt{0}}$) \\ 
{\bf else }({\it{x\/}} $\not=$ {\tt{1}}) $\wedge$ ({\it{y\/}} $<$ {\it{z\/}})$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  nat-to-bv-exp \\ \index{nat-to-bv-exp}
({\it{n\/}} $\not<$ {\it{size\/}}) $\rightarrow$ ({\rm{nat-to-bv}}\,({\rm{exp}}\,({\tt{2}}, {\it{n\/}})\index{exp}, {\it{size\/}})\index{nat-to-bv} $=$ {\rm{all-ones}}\,({\it{size\/}})\index{all-ones})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  bv-to-nat-all-zeros \\ \index{bv-to-nat-all-zeros}
{\rm{bvp}}\,({\it{bv\/}})\index{bvp} $\rightarrow$ (({\rm{bv-to-nat}}\,({\it{bv\/}})\index{bv-to-nat} $=$ {\tt{0}}) $=$ {\rm{all-zeros}}\,({\it{bv\/}})\index{all-zeros})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  lessp-bv-to-nat-1 \\ \index{lessp-bv-to-nat-1}
{\rm{bvp}}\,({\it{bv\/}})\index{bvp} $\rightarrow$ (({\rm{bv-to-nat}}\,({\it{bv\/}})\index{bv-to-nat} $<$ {\tt{1}}) $=$ {\rm{all-zeros}}\,({\it{bv\/}})\index{all-zeros})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  car-nat-to-bv-exp \\ \index{car-nat-to-bv-exp}
\=\+({\it{n\/}} $<$ {\it{size\/}}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{car}}\,({\rm{nat-to-bv}}\,({\rm{exp}}\,({\tt{2}}, {\it{n\/}})\index{exp}, {\it{size\/}})\index{nat-to-bv}) \\ 
$=$$\;\;\;\;$\=\+{\bf if }($1\;+$ {\it{n\/}}) $=$ {\it{size\/}}$\;\;${\bf then }{\tt{1}} \\ 
{\bf else }{\tt{0}}$\;${\bf  endif}\-)\-\-
\end{tabbing}

\begin{verbatim};; let's disable some time wasters
\end{verbatim}
\noindent{\sc Event}:   Disable equal-bitp-simplify.

\addvspace{18pt}

\noindent{\sc Event}:   Disable all-zeros-xor-bvs-when-lone-big-simple.

\addvspace{18pt}

\noindent{\sc Event}:   Disable high-bit-on-reasonable.

\addvspace{18pt}

\noindent{\sc Event}:   Disable find-high-out-of-sync-reasonable.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  all-zeros-firstn-difference \\ \index{all-zeros-firstn-difference}
\=\+({\rm{bvp}}\,({\it{x\/}})\index{bvp} $\wedge$ ({\rm{length}}\,({\it{x\/}})\index{length} $=$ {\it{size\/}}) $\wedge$ ({\it{n\/}} $<$ {\it{size\/}})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{lessp-bv}}\,({\it{x\/}}, {\rm{nat-to-bv}}\,({\rm{exp}}\,({\tt{2}}, {\it{n\/}})\index{exp}, {\it{size\/}})\index{nat-to-bv})\index{lessp-bv} \\ 
$=$$\;\;\;\;${\rm{all-zeros}}\,({\rm{firstn}}\,({\it{x\/}}, {\it{size\/}} $-$ {\it{n\/}})\index{firstn})\index{all-zeros})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  all-zeros-xor-bv \\ \index{all-zeros-xor-bv}
\=\+({\rm{bvp}}\,({\it{a\/}})\index{bvp} $\wedge$ {\rm{bvp}}\,({\it{b\/}})\index{bvp} $\wedge$ ({\rm{length}}\,({\it{a\/}})\index{length} $=$ {\rm{length}}\,({\it{b\/}})\index{length})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{all-zeros}}\,({\rm{xor-bv}}\,({\it{a\/}}, {\it{b\/}})\index{xor-bv})\index{all-zeros} $=$ ({\it{a\/}} $=$ {\it{b\/}}))\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  lessp-bv-nat-to-bv-1 \\ \index{lessp-bv-nat-to-bv-1}
\=\+(({\rm{length}}\,({\it{x\/}})\index{length} $=$ {\it{size\/}}) $\wedge$ {\rm{bvp}}\,({\it{x\/}})\index{bvp}) \\ 
$\rightarrow$$\;\;\;\;$({\rm{lessp-bv}}\,({\it{x\/}}, {\rm{nat-to-bv}}\,({\tt{1}}, {\it{size\/}})\index{nat-to-bv})\index{lessp-bv} $=$ (({\tt{0}} $<$ {\it{size\/}}) $\wedge$ {\rm{all-zeros}}\,({\it{x\/}})\index{all-zeros}))\-
\end{tabbing}


\begin{tabbing}{\sc Definition}:\index{double-length-induction} \\  
\=\+{\rm{double-length-induction}}\,({\it{x\/}}, {\it{y\/}})\index{double-length-induction} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{x\/}}) $\wedge$ {\rm{listp}}\,({\it{y\/}})$\;\;${\bf then }{\rm{double-length-induction}}\,({\rm{cdr}}\,({\it{x\/}}), {\rm{cdr}}\,({\it{y\/}}))\index{double-length-induction} \\ 
{\bf else }{\bf{t}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  all-zeros-equal \\ \index{all-zeros-equal}
\=\+({\rm{bvp}}\,({\it{a\/}})\index{bvp} $\wedge$ {\rm{bvp}}\,({\it{b\/}})\index{bvp} $\wedge$ {\rm{all-zeros}}\,({\it{a\/}})\index{all-zeros} $\wedge$ {\rm{all-zeros}}\,({\it{b\/}})\index{all-zeros}) \\ 
$\rightarrow$$\;\;\;\;$(({\it{a\/}} $=$ {\it{b\/}}) $=$ ({\rm{length}}\,({\it{a\/}})\index{length} $=$ {\rm{length}}\,({\it{b\/}})\index{length}))\-
\end{tabbing}


\noindent{\sc Event}:   Disable all-zeros-equal.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  all-zeros-xor-bvs \\ \index{all-zeros-xor-bvs}
\=\+({\rm{good-state-of-size}}\,({\it{z\/}}, {\it{size\/}})\index{good-state-of-size} $\wedge$ ({\rm{number-with-at-least}}\,({\it{z\/}}, {\tt{1}}, {\it{size\/}})\index{number-with-at-least} $=$ {\tt{0}})) \\ 
$\rightarrow$$\;\;\;\;${\rm{all-zeros}}\,({\rm{xor-bvs}}\,({\it{z\/}})\index{xor-bvs})\index{all-zeros}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  length-firstn \\ \index{length-firstn}
{\rm{length}}\,({\rm{firstn}}\,({\it{list\/}}, {\it{size\/}})\index{firstn})\index{length} $=$ {\rm{min}}\,({\rm{length}}\,({\it{list\/}})\index{length}, {\it{size\/}})\index{min}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  length-xor-bv \\ \index{length-xor-bv}
{\rm{length}}\,({\rm{xor-bv}}\,({\it{a\/}}, {\it{b\/}})\index{xor-bv})\index{length} $=$ {\rm{min}}\,({\rm{length}}\,({\it{a\/}})\index{length}, {\rm{length}}\,({\it{b\/}})\index{length})\index{min}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  firstn-xor-bv \\ \index{firstn-xor-bv}
{\rm{firstn}}\,({\rm{xor-bv}}\,({\it{a\/}}, {\it{b\/}})\index{xor-bv}, {\it{size\/}})\index{firstn} $=$ {\rm{xor-bv}}\,({\rm{firstn}}\,({\it{a\/}}, {\it{size\/}})\index{firstn}, {\rm{firstn}}\,({\it{b\/}}, {\it{size\/}})\index{firstn})\index{xor-bv}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  all-zeros-xor-bvs-firstn \\ \index{all-zeros-xor-bvs-firstn}
\=\+(\=\+{\rm{good-state-of-size}}\,({\it{z\/}}, {\it{size\/}})\index{good-state-of-size} \\ 
$\wedge$$\;\;\;\;$({\it{n\/}} $<$ {\it{size\/}}) \\ 
$\wedge$$\;\;\;\;$({\rm{number-with-at-least}}\,({\it{z\/}}, {\rm{exp}}\,({\tt{2}}, {\it{n\/}})\index{exp}, {\it{size\/}})\index{number-with-at-least} $=$ {\tt{0}}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{all-zeros}}\,({\rm{firstn}}\,({\rm{xor-bvs}}\,({\it{z\/}})\index{xor-bvs}, {\it{size\/}} $-$ {\it{n\/}})\index{firstn})\index{all-zeros}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  all-zeros-if-firstn-zeros \\ \index{all-zeros-if-firstn-zeros}
{\rm{all-zeros}}\,({\it{x\/}})\index{all-zeros} $\rightarrow$ {\rm{all-zeros}}\,({\rm{firstn}}\,({\it{x\/}}, {\it{size\/}})\index{firstn})\index{all-zeros}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  good-state-of-size-length-xor-bvs \\ \index{good-state-of-size-length-xor-bv!s}
\=\+{\rm{good-state-of-size}}\,({\it{z\/}}, {\rm{length}}\,({\rm{xor-bvs}}\,({\it{z\/}})\index{xor-bvs})\index{length})\index{good-state-of-size} \\ 
$=$$\;\;\;\;${\rm{good-state-of-size}}\,({\it{z\/}}, {\rm{length}}\,({\rm{car}}\,({\it{z\/}}))\index{length})\index{good-state-of-size}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  bvp-firstn \\ \index{bvp-firstn}
{\rm{bvp}}\,({\it{x\/}})\index{bvp} $\rightarrow$ {\rm{bvp}}\,({\rm{firstn}}\,({\it{x\/}}, {\it{size\/}})\index{firstn})\index{bvp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  number-with-at-least-exp-2 \\ \index{number-with-at-least-exp-2}
\=\+(\=\+{\rm{good-state-of-size}}\,({\it{state\/}}, {\it{size\/}})\index{good-state-of-size} \\ 
$\wedge$$\;\;\;\;$({\it{n\/}} $<$ {\it{size\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{all-zeros}}\,({\rm{firstn}}\,({\rm{xor-bvs}}\,({\it{state\/}})\index{xor-bvs}, {\it{size\/}} $-$ {\it{n\/}})\index{firstn})\index{all-zeros})\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{number-with-at-least}}\,({\it{state\/}}, {\rm{exp}}\,({\tt{2}}, {\it{n\/}})\index{exp}, {\it{size\/}})\index{number-with-at-least} $\not=$ {\tt{1}})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  number-with-at-least-2 \\ \index{number-with-at-least-2}
\=\+(\=\+{\rm{good-state-of-size}}\,({\it{state\/}}, {\it{size\/}})\index{good-state-of-size} \\ 
$\wedge$$\;\;\;\;$({\tt{1}} $<$ {\it{size\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{all-zeros}}\,({\rm{xor-bvs}}\,({\it{state\/}})\index{xor-bvs})\index{all-zeros})\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{number-with-at-least}}\,({\it{state\/}}, {\tt{2}}, {\it{size\/}})\index{number-with-at-least} $\not=$ {\tt{1}})\-
\end{tabbing}


\begin{tabbing}{\sc Theorem}:  lessp-bv-all-zeros \\ \index{lessp-bv-all-zeros}
\=\+({\rm{all-zeros}}\,({\it{x\/}})\index{all-zeros} $\wedge$ ({\rm{length}}\,({\it{x\/}})\index{length} $=$ {\rm{length}}\,({\it{y\/}})\index{length}) $\wedge$ {\rm{bvp}}\,({\it{x\/}})\index{bvp} $\wedge$ {\rm{bvp}}\,({\it{y\/}})\index{bvp}) \\ 
$\rightarrow$$\;\;\;\;$(({\rm{lessp-bv}}\,({\it{x\/}}, {\it{y\/}})\index{lessp-bv} $=$ ($\neg$ {\rm{all-zeros}}\,({\it{y\/}})\index{all-zeros})) $\wedge$ ($\neg$ {\rm{lessp-bv}}\,({\it{y\/}}, {\it{x\/}})\index{lessp-bv}))\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  number-with-at-least-means-get \\ \index{number-with-at-least-means-get}
\=\+(\=\+{\rm{good-state-of-size}}\,({\it{state\/}}, {\it{size\/}})\index{good-state-of-size} \\ 
$\wedge$$\;\;\;\;$({\it{z\/}} $<$ {\rm{length}}\,({\it{state\/}})\index{length}) \\ 
$\wedge$$\;\;\;\;$({\rm{number-with-at-least}}\,({\it{state\/}}, {\it{n\/}}, {\it{size\/}})\index{number-with-at-least} $=$ {\tt{0}}))\- \\ 
$\rightarrow$$\;\;\;\;$(({\rm{bv-to-nat}}\,({\rm{get}}\,({\it{z\/}}, {\it{state\/}})\index{get})\index{bv-to-nat} $<$ {\it{n\/}}) $=$ {\bf{t}})\-
\end{tabbing}
              

\begin{tabbing}{\sc Theorem}:  remainder-sub1-hack \\ \index{remainder-sub1-hack}
\=\+(({\it{x\/}} ${}${\bf{mod}}${}$ {\it{y\/}}) $=$ {\it{p\/}}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+(({\it{x\/}} $-\;1$) ${}${\bf{mod}}${}$ {\it{y\/}}) \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{x\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }{\it{p\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\it{y\/}} $-\;1$ \\ 
{\bf else }{\it{p\/}} $-\;1$$\;${\bf  endif}\-)\-\-
\end{tabbing}

\begin{verbatim};; ought to be using more up-to-date naturals library!

\end{verbatim}\begin{tabbing}{\sc Theorem}:  equal-times-x \\ \index{equal-times-x}
(({\it{y\/}} $*$ {\it{x\/}}) $=$ {\it{x\/}}) $=$ (({\it{x\/}} $=$ {\tt{0}}) $\vee$ (({\it{x\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{y\/}} $=$ {\tt{1}})))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  equal-times-x-2 \\ \index{equal-times-x-2}
(({\it{x\/}} $*$ {\it{y\/}}) $=$ {\it{x\/}}) $=$ (({\it{x\/}} $=$ {\tt{0}}) $\vee$ (({\it{x\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{y\/}} $=$ {\tt{1}})))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  equal-exp-x-x \\ \index{equal-exp-x-x}
\=\+({\rm{exp}}\,({\it{x\/}}, {\it{y\/}})\index{exp} $=$ {\it{x\/}}) \\ 
$=$$\;\;\;\;$(({\it{x\/}} $=$ {\tt{1}}) $\vee$ (({\it{x\/}} $=$ {\tt{0}}) $\wedge$ ({\it{y\/}} $\not\simeq {\tt{0}}$)) $\vee$ (({\it{x\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{y\/}} $=$ {\tt{1}})))\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  lessp-bv-2-means \\ \index{lessp-bv-2-means}
\=\+({\rm{bvp}}\,({\it{x\/}})\index{bvp} $\wedge$ ({\tt{1}} $<$ {\rm{length}}\,({\it{x\/}})\index{length})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{lessp-bv}}\,({\it{x\/}}, {\rm{nat-to-bv}}\,({\tt{2}}, {\rm{length}}\,({\it{x\/}})\index{length})\index{nat-to-bv})\index{lessp-bv} \\ 
$=$$\;\;\;\;$({\rm{all-zeros}}\,({\it{x\/}})\index{all-zeros} $\vee$ ({\it{x\/}} $=$ {\rm{nat-to-bv}}\,({\tt{1}}, {\rm{length}}\,({\it{x\/}})\index{length})\index{nat-to-bv})))\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  lessp-bv-x-1-means \\ \index{lessp-bv-x-1-means}
\=\+(({\rm{length}}\,({\it{x\/}})\index{length} $=$ {\it{size\/}}) $\wedge$ {\rm{bvp}}\,({\it{x\/}})\index{bvp} $\wedge$ ({\tt{1}} $<$ {\it{size\/}})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{lessp-bv}}\,({\it{x\/}}, {\rm{nat-to-bv}}\,({\tt{1}}, {\it{size\/}})\index{nat-to-bv})\index{lessp-bv} $=$ {\rm{all-zeros}}\,({\it{x\/}})\index{all-zeros})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  nat-to-bv-not-numberp \\ \index{nat-to-bv-not-numberp}
({\it{n\/}} $\not\in\;${\bf{N}}${}$) $\rightarrow$ ({\rm{nat-to-bv}}\,({\it{n\/}}, {\it{size\/}})\index{nat-to-bv} $=$ {\rm{nat-to-bv}}\,({\tt{0}}, {\it{size\/}})\index{nat-to-bv})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  all-zeros-nat-to-bv-1 \\ \index{all-zeros-nat-to-bv-1}
({\it{size\/}} $\not\simeq {\tt{0}}$) $\rightarrow$ ({\rm{all-zeros}}\,({\rm{nat-to-bv}}\,({\it{n\/}}, {\it{size\/}})\index{nat-to-bv})\index{all-zeros} $=$ ({\it{n\/}} $\simeq {\tt{0}}$))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  get-when-lessp-bv-2 \\ \index{get-when-lessp-bv-2}
\=\+(\=\+{\rm{good-state-of-size}}\,({\it{state\/}}, {\it{size\/}})\index{good-state-of-size} \\ 
$\wedge$$\;\;\;\;$({\tt{1}} $<$ {\it{size\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{z\/}} $<$ {\rm{length}}\,({\it{state\/}})\index{length}) \\ 
$\wedge$$\;\;\;\;$({\rm{number-with-at-least}}\,({\it{state\/}}, {\tt{2}}, {\it{size\/}})\index{number-with-at-least} $=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;${\rm{bvp}}\,({\it{x\/}})\index{bvp} \\ 
$\wedge$$\;\;\;\;$({\rm{length}}\,({\it{x\/}})\index{length} $=$ {\it{size\/}}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{lessp-bv}}\,({\it{x\/}}, {\rm{get}}\,({\it{z\/}}, {\it{state\/}})\index{get})\index{lessp-bv} \\ 
$=$$\;\;\;\;$({\rm{all-zeros}}\,({\it{x\/}})\index{all-zeros} $\wedge$ ({\rm{get}}\,({\it{z\/}}, {\it{state\/}})\index{get} $=$ {\rm{nat-to-bv}}\,({\tt{1}}, {\it{size\/}})\index{nat-to-bv})))\-\-
\end{tabbing}


\begin{verbatim};; replacement rule version
\end{verbatim}\begin{tabbing}{\sc Theorem}:  find-high-out-of-sync-reasonable2 \\ \index{find-high-out-of-sync-reasonable!2}
\=\+({\rm{listp}}\,({\it{state\/}}) $\wedge$ {\rm{good-state-of-size}}\,({\it{state\/}}, {\it{size\/}})\index{good-state-of-size}) \\ 
$\rightarrow$$\;\;\;\;$(({\rm{find-high-out-of-sync}}\,({\it{state\/}})\index{find-high-out-of-sync} $<$ {\rm{length}}\,({\it{state\/}})\index{length}) $=$ {\bf{t}})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  xor-bv-0 \\ \index{xor-bv-0}
\=\+(({\rm{length}}\,({\it{x\/}})\index{length} $=$ {\it{size\/}}) $\wedge$ {\rm{bvp}}\,({\it{x\/}})\index{bvp}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{xor-bv}}\,({\rm{nat-to-bv}}\,({\tt{0}}, {\it{size\/}})\index{nat-to-bv}, {\it{x\/}})\index{xor-bv} $=$ {\it{x\/}}) \\ 
$\wedge$$\;\;\;\;$({\rm{xor-bv}}\,({\it{x\/}}, {\rm{nat-to-bv}}\,({\tt{0}}, {\it{size\/}})\index{nat-to-bv})\index{xor-bv} $=$ {\it{x\/}}))\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  lessp-bv-to-nat-get-col-with-at-least \\ \index{lessp-bv-to-nat-get-col-with-at!-least}
\=\+(\=\+{\rm{good-state-of-size}}\,({\it{state\/}}, {\it{size\/}})\index{good-state-of-size} \\ 
$\wedge$$\;\;\;\;$({\it{n\/}} $<$ {\rm{exp}}\,({\tt{2}}, {\it{size\/}})\index{exp}) \\ 
$\wedge$$\;\;\;\;$({\tt{1}} $<$ {\it{size\/}}) \\ 
$\wedge$$\;\;\;\;$({\rm{number-with-at-least}}\,({\it{state\/}}, {\it{n\/}}, {\it{size\/}})\index{number-with-at-least} $\not\simeq {\tt{0}}$))\- \\ 
$\rightarrow$$\;\;\;\;$(({\rm{bv-to-nat}}\,({\rm{get}}\,({\rm{col-with-at-least}}\,({\it{state\/}}, {\it{n\/}}, {\it{size\/}})\index{col-with-at-least}, {\it{state\/}})\index{get})\index{bv-to-nat} $<$ {\it{n\/}}) $=$ {\bf{f}})\-
\end{tabbing}

\begin{verbatim};; needed?
\end{verbatim}\begin{tabbing}{\sc Theorem}:  lessp-get-exp-2-size \\ \index{lessp-get-exp-2-size}
\=\+({\rm{good-state-of-size}}\,({\it{state\/}}, {\it{size\/}})\index{good-state-of-size} $\wedge$ ({\it{z\/}} $<$ {\rm{length}}\,({\it{state\/}})\index{length})) \\ 
$\rightarrow$$\;\;\;\;$(({\rm{bv-to-nat}}\,({\rm{get}}\,({\it{z\/}}, {\it{state\/}})\index{get})\index{bv-to-nat} $<$ {\rm{exp}}\,({\tt{2}}, {\it{size\/}})\index{exp}) $=$ {\bf{t}})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  equal-remainder-sub1-0 \\ \index{equal-remainder-sub1-0}
((({\it{x\/}} $-\;1$) ${}${\bf{mod}}${}$ {\it{p\/}}) $=$ {\tt{0}}) $=$ (({\it{x\/}} $\simeq {\tt{0}}$) $\vee$ ({\it{p\/}} $=$ {\tt{1}}) $\vee$ (({\it{x\/}} ${}${\bf{mod}}${}$ {\it{p\/}}) $=$ {\tt{1}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  lessp-1-rewrite \\ \index{lessp-1-rewrite}
({\tt{1}} $<$ {\it{x\/}}) $=$ (({\it{x\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{x\/}} $\not=$ {\tt{0}}) $\wedge$ ({\it{x\/}} $\not=$ {\tt{1}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  numberp-col-with-at-least \\ \index{numberp-col-with-at-least}
({\rm{col-with-at-least}}\,({\it{state\/}}, {\it{n\/}}, {\it{size\/}})\index{col-with-at-least} $\in\;${\bf{N}}${}$) $=$ {\rm{listp}}\,({\it{state\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  equal-remainder-2-special \\ \index{equal-remainder-2-special}
\=\+(((({\it{x\/}} ${}${\bf{mod}}${}$ {\tt{2}}) $=$ {\it{y\/}}) $\wedge$ ({\it{y\/}} $=$ {\tt{1}})) $\rightarrow$ (({\it{x\/}} ${}${\bf{mod}}${}$ {\tt{2}}) $\not=$ {\tt{0}})) \\ 
$\wedge$$\;\;\;\;$(((({\it{x\/}} ${}${\bf{mod}}${}$ {\tt{2}}) $\not=$ {\it{y\/}}) $\wedge$ ({\it{y\/}} $=$ {\tt{1}})) $\rightarrow$ ((({\it{x\/}} ${}${\bf{mod}}${}$ {\tt{2}}) $=$ {\tt{0}}) $=$ {\bf{t}}))\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  listp-fix-xor-bv \\ \index{listp-fix-xor-bv}
{\rm{listp}}\,({\rm{fix-xor-bv}}\,({\it{x\/}})\index{fix-xor-bv}) $=$ {\rm{listp}}\,({\it{x\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  lessp-length-x-length-xor-bvs-put-x \\ \index{lessp-length-x-length-xor-bvs-p!ut-x}
({\rm{length}}\,({\it{x\/}})\index{length} $<$ {\rm{length}}\,({\rm{xor-bvs}}\,({\rm{put}}\,({\it{z\/}}, {\it{x\/}}, {\it{state\/}})\index{put})\index{xor-bvs})\index{length}) $=$ {\bf{f}}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  length-xor-bvs-put \\ \index{length-xor-bvs-put}
\=\+(\=\+{\rm{good-state-of-size}}\,({\it{state\/}}, {\it{size\/}})\index{good-state-of-size} \\ 
$\wedge$$\;\;\;\;${\rm{listp}}\,({\it{state\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{z\/}} $<$ {\rm{length}}\,({\it{state\/}})\index{length}) \\ 
$\wedge$$\;\;\;\;$({\rm{length}}\,({\it{x\/}})\index{length} $=$ {\it{size\/}}))\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{length}}\,({\rm{xor-bvs}}\,({\rm{put}}\,({\it{z\/}}, {\it{x\/}}, {\it{state\/}})\index{put})\index{xor-bvs})\index{length} $=$ {\it{size\/}})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  lessp-1-length \\ \index{lessp-1-length}
(({\it{n\/}} $<$ {\rm{length}}\,({\it{x\/}})\index{length}) $\wedge$ ({\it{n\/}} $\not\simeq {\tt{0}}$)) $\rightarrow$ {\rm{listp}}\,({\rm{cdr}}\,({\it{x\/}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  all-zeros-get-col-with-at-least \\ \index{all-zeros-get-col-with-at-least}
\=\+(\=\+{\rm{good-state-of-size}}\,({\it{state\/}}, {\it{size\/}})\index{good-state-of-size} \\ 
$\wedge$$\;\;\;\;$({\tt{1}} $<$ {\it{size\/}}) \\ 
$\wedge$$\;\;\;\;$({\tt{1}} $<$ {\rm{length}}\,({\it{state\/}})\index{length}) \\ 
$\wedge$$\;\;\;\;$({\it{n\/}} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;$({\rm{number-with-at-least}}\,({\it{state\/}}, {\it{n\/}}, {\it{size\/}})\index{number-with-at-least} $\not\simeq {\tt{0}}$))\- \\ 
$\rightarrow$$\;\;\;\;$($\neg$ {\rm{all-zeros}}\,({\rm{get}}\,({\rm{col-with-at-least}}\,({\it{state\/}}, {\it{n\/}}, {\it{size\/}})\index{col-with-at-least}, {\it{state\/}})\index{get})\index{all-zeros})\-
\end{tabbing}

\begin{verbatim};; these dinosaurs aren't needed any more
\end{verbatim}
\noindent{\sc Event}:   Disable equal-bit-1.

\addvspace{18pt}

\noindent{\sc Event}:   Disable silly-listp-cdr.

\addvspace{18pt}

\begin{verbatim};; this takes too much time and isn't needed often
\end{verbatim}
\noindent{\sc Event}:   Disable nat-to-bv-is-all-ones.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  equal-remainder-sub1-x-2-special \\ \index{equal-remainder-sub1-x-2-specia!l}
((({\it{x\/}} $-\;1$) ${}${\bf{mod}}${}$ {\tt{2}}) $=$ {\tt{1}}) $=$ (({\it{x\/}} $\not\simeq {\tt{0}}$) $\wedge$ (({\it{x\/}} ${}${\bf{mod}}${}$ {\tt{2}}) $=$ {\tt{0}}))
\end{tabbing}


\begin{verbatim};;;;;;
;;;;;;
;; The big lemmas about NIM

\end{verbatim}\begin{tabbing}{\sc Theorem}:  smart-moves-from-not-loser \\ \index{smart-moves-from-not-loser}
\=\+(\=\+($\neg$ {\rm{loser-state}}\,({\it{state\/}}, {\it{size\/}})\index{loser-state}) \\ 
$\wedge$$\;\;\;\;${\rm{good-state-of-size}}\,({\it{state\/}}, {\it{size\/}})\index{good-state-of-size} \\ 
$\wedge$$\;\;\;\;$({\tt{1}} $<$ {\rm{length}}\,({\it{state\/}})\index{length}) \\ 
$\wedge$$\;\;\;\;$({\tt{1}} $<$ {\it{size\/}}) \\ 
$\wedge$$\;\;\;\;$({\rm{number-with-at-least}}\,({\it{state\/}}, {\tt{1}}, {\it{size\/}})\index{number-with-at-least} $\not=$ {\tt{0}}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{loser-state}}\,({\rm{apply-move}}\,({\rm{smart-move}}\,({\it{state\/}}, {\it{size\/}})\index{smart-move}, {\it{state\/}})\index{apply-move}, {\it{size\/}})\index{loser-state}\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{stupid-move} \\  
\=\+{\rm{stupid-move}}\,({\it{state\/}}, {\it{size\/}})\index{stupid-move} \\ 
$=$$\;\;\;\;$\=\+{\bf let }\=\+{\it{pile\/}}{\bf $\;$ be$\;\;$}{\rm{col-with-at-least}}\,({\it{state\/}}, {\tt{1}}, {\it{size\/}})\index{col-with-at-least}\- \\ 
{\bf in} \\ 
{\rm{cons}}\,({\it{pile\/}}, {\rm{nat-to-bv}}\,({\rm{bv-to-nat}}\,({\rm{get}}\,({\it{pile\/}}, {\it{state\/}})\index{get})\index{bv-to-nat} $-\;1$, {\it{size\/}})\index{nat-to-bv})$\;${\bf  endlet}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{computer-move} \\  
\=\+{\rm{computer-move}}\,({\it{state\/}}, {\it{size\/}})\index{computer-move} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{loser-state}}\,({\it{state\/}}, {\it{size\/}})\index{loser-state}$\;\;${\bf then }{\rm{stupid-move}}\,({\it{state\/}}, {\it{size\/}})\index{stupid-move} \\ 
{\bf else }{\rm{smart-move}}\,({\it{state\/}}, {\it{size\/}})\index{smart-move}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  smart-move-is-a-move \\ \index{smart-move-is-a-move}
\=\+(\=\+{\rm{good-state-of-size}}\,({\it{state\/}}, {\it{size\/}})\index{good-state-of-size} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{loser-state}}\,({\it{state\/}}, {\it{size\/}})\index{loser-state}) \\ 
$\wedge$$\;\;\;\;$({\tt{1}} $<$ {\it{size\/}}) \\ 
$\wedge$$\;\;\;\;$({\tt{1}} $<$ {\rm{length}}\,({\it{state\/}})\index{length}) \\ 
$\wedge$$\;\;\;\;$({\tt{0}} $<$ {\rm{number-with-at-least}}\,({\it{state\/}}, {\tt{1}}, {\it{size\/}})\index{number-with-at-least}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{movep}}\,({\rm{smart-move}}\,({\it{state\/}}, {\it{size\/}})\index{smart-move}, {\it{state\/}}, {\it{size\/}})\index{movep}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  moves-from-loser \\ \index{moves-from-loser}
\=\+(\=\+{\rm{loser-state}}\,({\it{state\/}}, {\it{size\/}})\index{loser-state} \\ 
$\wedge$$\;\;\;\;$({\tt{1}} $<$ {\it{size\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{good-state-of-size}}\,({\it{state\/}}, {\it{size\/}})\index{good-state-of-size} \\ 
$\wedge$$\;\;\;\;${\rm{movep}}\,({\it{move\/}}, {\it{state\/}}, {\it{size\/}})\index{movep})\- \\ 
$\rightarrow$$\;\;\;\;$($\neg$ {\rm{loser-state}}\,({\rm{apply-move}}\,({\it{move\/}}, {\it{state\/}})\index{apply-move}, {\it{size\/}})\index{loser-state})\-
\end{tabbing}




\begin{verbatim};;;; put together big lemmas in one theorem about "game"

\end{verbatim}\begin{tabbing}{\sc Conservative Axiom}:  a-move-intro \\ \index{a-move-intro}
\=\+(\=\+({\rm{number-with-at-least}}\,({\it{state\/}}, {\tt{1}}, {\it{size\/}})\index{number-with-at-least} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;$({\tt{1}} $<$ {\it{size\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{good-state-of-size}}\,({\it{state\/}}, {\it{size\/}})\index{good-state-of-size})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{movep}}\,({\rm{a-move}}\,({\it{state\/}}, {\it{size\/}})\index{a-move}, {\it{state\/}}, {\it{size\/}})\index{movep}\-
\end{tabbing}\noindent Simultaneously, we introduce the new function symbol {\it a-move\/}.

\begin{tabbing}{\sc Definition}:\index{reasonable-game-statep} \\  
\=\+{\rm{reasonable-game-statep}}\,({\it{state\/}}, {\it{size\/}})\index{reasonable-game-statep} \\ 
$=$$\;\;\;\;$(\=\+{\rm{good-state-of-size}}\,({\it{state\/}}, {\it{size\/}})\index{good-state-of-size} \\ 
$\wedge$$\;\;\;\;$({\tt{1}} $<$ {\it{size\/}}) \\ 
$\wedge$$\;\;\;\;$({\tt{1}} $<$ {\rm{length}}\,({\it{state\/}})\index{length}))\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{sum-matches} \\  
\=\+{\rm{sum-matches}}\,({\it{state\/}})\index{sum-matches} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{state\/}}) \\ 
{\bf then }{\rm{bv-to-nat}}\,({\rm{car}}\,({\it{state\/}}))\index{bv-to-nat} $+$ {\rm{sum-matches}}\,({\rm{cdr}}\,({\it{state\/}}))\index{sum-matches} \\ 
{\bf else }{\tt{0}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  equal-x-nat-to-bv-0 \\ \index{equal-x-nat-to-bv-0}
({\rm{bvp}}\,({\it{x\/}})\index{bvp} $\wedge$ {\rm{all-zeros}}\,({\it{x\/}})\index{all-zeros}) $\rightarrow$ (({\it{x\/}} $=$ {\rm{nat-to-bv}}\,({\tt{0}}, {\rm{length}}\,({\it{x\/}})\index{length})\index{nat-to-bv}) $=$ {\bf{t}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  get-from-zeros \\ \index{get-from-zeros}
\=\+(\=\+{\rm{good-state-of-size}}\,({\it{z\/}}, {\it{size\/}})\index{good-state-of-size} \\ 
$\wedge$$\;\;\;\;$({\it{size\/}} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;$({\rm{number-with-at-least}}\,({\it{z\/}}, {\tt{1}}, {\it{size\/}})\index{number-with-at-least} $=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$({\it{d\/}} $<$ {\rm{length}}\,({\it{z\/}})\index{length}))\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{get}}\,({\it{d\/}}, {\it{z\/}})\index{get} $=$ {\rm{nat-to-bv}}\,({\tt{0}}, {\it{size\/}})\index{nat-to-bv})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  lessp-sum-matches-member \\ \index{lessp-sum-matches-member}
\=\+({\it{place\/}} $<$ {\rm{length}}\,({\it{state\/}})\index{length}) \\ 
$\rightarrow$$\;\;\;\;$({\rm{sum-matches}}\,({\it{state\/}})\index{sum-matches} $\not<$ {\rm{bv-to-nat}}\,({\rm{get}}\,({\it{place\/}}, {\it{state\/}})\index{get})\index{bv-to-nat})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  sum-matches-put \\ \index{sum-matches-put}
\=\+({\it{place\/}} $<$ {\rm{length}}\,({\it{state\/}})\index{length}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{sum-matches}}\,({\rm{put}}\,({\it{place\/}}, {\it{v\/}}, {\it{state\/}})\index{put})\index{sum-matches} \\ 
$=$$\;\;\;\;$(\=\+({\rm{sum-matches}}\,({\it{state\/}})\index{sum-matches} $-$ {\rm{bv-to-nat}}\,({\rm{get}}\,({\it{place\/}}, {\it{state\/}})\index{get})\index{bv-to-nat}) \\ 
$+$$\;\;\;\;${\rm{bv-to-nat}}\,({\it{v\/}})\index{bv-to-nat})\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  lessp-not-all-zeros \\ \index{lessp-not-all-zeros}
(($\neg$ {\rm{all-zeros}}\,({\it{x\/}})\index{all-zeros}) $\wedge$ {\rm{bvp}}\,({\it{x\/}})\index{bvp} $\wedge$ {\rm{listp}}\,({\it{x\/}})) $\rightarrow$ ({\tt{0}} $<$ {\rm{bv-to-nat}}\,({\it{x\/}})\index{bv-to-nat})
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{game-ends-recursion} \\  
\=\+{\rm{game-ends-recursion}}\,({\it{move\/}}, {\it{state\/}}, {\it{size\/}})\index{game-ends-recursion} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{state\/}}) $\wedge$ ({\rm{car}}\,({\it{move\/}}) $\not\simeq {\tt{0}}$) \\ 
{\bf then }{\rm{game-ends-recursion}}\,(\=\+{\rm{cons}}\,({\rm{car}}\,({\it{move\/}}) $-\;1$, {\rm{cdr}}\,({\it{move\/}})), \\ 
{\rm{cdr}}\,({\it{state\/}}), \\ 
{\it{size\/}})\-\index{game-ends-recursion} \\ 
{\bf else }{\bf{t}}$\;${\bf  endif}\-\-
\end{tabbing}
    
\begin{tabbing}{\sc Theorem}:  game-ends \\ \index{game-ends}
\=\+(\=\+({\rm{number-with-at-least}}\,({\it{state\/}}, {\tt{1}}, {\it{size\/}})\index{number-with-at-least} $\not=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;${\rm{good-state-of-size}}\,({\it{state\/}}, {\it{size\/}})\index{good-state-of-size} \\ 
$\wedge$$\;\;\;\;$({\it{size\/}} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;${\rm{movep}}\,({\it{move\/}}, {\it{state\/}}, {\it{size\/}})\index{movep})\- \\ 
$\rightarrow$$\;\;\;\;$(({\rm{sum-matches}}\,({\rm{apply-move}}\,({\it{move\/}}, {\it{state\/}})\index{apply-move})\index{sum-matches} $<$ {\rm{sum-matches}}\,({\it{state\/}})\index{sum-matches}) $=$ {\bf{t}})\-
\end{tabbing}


\noindent{\sc Event}:   Disable apply-move.

\addvspace{18pt}

\noindent{\sc Event}:   Disable smart-move.

\addvspace{18pt}

\noindent{\sc Event}:   Disable stupid-move.

\addvspace{18pt}

\begin{tabbing}{\sc Definition}:\index{game} \\  
\=\+{\rm{game}}\,({\it{good-player-turn\/}}, {\it{state\/}}, {\it{size\/}})\index{game} \\ 
$=$$\;\;\;\;$\=\+{\bf if }$\neg$ {\rm{reasonable-game-statep}}\,({\it{state\/}}, {\it{size\/}})\index{reasonable-game-statep}$\;\;${\bf then }{\bf{f}} \\ 
{\bf elseif }{\rm{number-with-at-least}}\,({\it{state\/}}, {\tt{1}}, {\it{size\/}})\index{number-with-at-least} $=$ {\tt{0}} \\ 
{\bf then }{\it{good-player-turn\/}} \\ 
{\bf else }\=\+{\bf let }\=\+{\it{move\/}}{\bf $\;$ be$\;\;$}\=\+{\bf if }{\it{good-player-turn\/}} \\ 
{\bf then }{\rm{computer-move}}\,({\it{state\/}}, {\it{size\/}})\index{computer-move} \\ 
{\bf else }{\rm{a-move}}\,({\it{state\/}}, {\it{size\/}})\index{a-move}$\;${\bf  endif}\-\- \\ 
{\bf in} \\ 
\=\+{\bf if }$\neg$ {\rm{movep}}\,({\it{move\/}}, {\it{state\/}}, {\it{size\/}})\index{movep}$\;\;${\bf then }{\bf{f}} \\ 
{\bf else }{\rm{game}}\,(\=\+$\neg$ {\it{good-player-turn\/}}, \\ 
{\rm{apply-move}}\,({\it{move\/}}, {\it{state\/}})\index{apply-move}, \\ 
{\it{size\/}})\-\index{game}$\;${\bf  endif}\-$\;${\bf  endlet}\-$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  transitivity-of-lessp-bv \\ \index{transitivity-of-lessp-bv}
\=\+(\=\+{\rm{lessp-bv}}\,({\it{x\/}}, {\it{y\/}})\index{lessp-bv} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{lessp-bv}}\,({\it{z\/}}, {\it{y\/}})\index{lessp-bv}) \\ 
$\wedge$$\;\;\;\;$({\rm{length}}\,({\it{x\/}})\index{length} $=$ {\rm{length}}\,({\it{y\/}})\index{length}) \\ 
$\wedge$$\;\;\;\;$({\rm{length}}\,({\it{y\/}})\index{length} $=$ {\rm{length}}\,({\it{z\/}})\index{length}) \\ 
$\wedge$$\;\;\;\;${\rm{bvp}}\,({\it{x\/}})\index{bvp} \\ 
$\wedge$$\;\;\;\;${\rm{bvp}}\,({\it{y\/}})\index{bvp} \\ 
$\wedge$$\;\;\;\;${\rm{bvp}}\,({\it{z\/}})\index{bvp})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{lessp-bv}}\,({\it{x\/}}, {\it{z\/}})\index{lessp-bv}\-
\end{tabbing}


\begin{tabbing}{\sc Theorem}:  nat-to-bv-size-1 \\ \index{nat-to-bv-size-1}
\=\+{\rm{nat-to-bv}}\,({\it{x\/}}, {\tt{1}})\index{nat-to-bv} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{x\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\tt{'}}{\tt{(}}{\tt{0}}{\tt{)}} \\ 
{\bf else }{\tt{'}}{\tt{(}}{\tt{1}}{\tt{)}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  lessp-bv-nat-to-bv-nat-to-bv-2 \\ \index{lessp-bv-nat-to-bv-nat-to-bv-2}
({\it{x\/}} $\not<$ {\it{y\/}}) $\rightarrow$ ($\neg$ {\rm{lessp-bv}}\,({\rm{nat-to-bv}}\,({\it{x\/}}, {\it{size\/}})\index{nat-to-bv}, {\rm{nat-to-bv}}\,({\it{y\/}}, {\it{size\/}})\index{nat-to-bv})\index{lessp-bv})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  lessp-bv-of-larger \\ \index{lessp-bv-of-larger}
\=\+({\rm{lessp-bv}}\,({\it{v\/}}, {\rm{nat-to-bv}}\,({\it{x\/}}, {\it{a\/}})\index{nat-to-bv})\index{lessp-bv} $\wedge$ ({\rm{length}}\,({\it{v\/}})\index{length} $=$ {\it{a\/}}) $\wedge$ {\rm{bvp}}\,({\it{v\/}})\index{bvp} $\wedge$ ({\it{y\/}} $\not<$ {\it{x\/}})) \\ 
$\rightarrow$$\;\;\;\;${\rm{lessp-bv}}\,({\it{v\/}}, {\rm{nat-to-bv}}\,({\it{y\/}}, {\it{a\/}})\index{nat-to-bv})\index{lessp-bv}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  lessp-number-with-at-least-x-y \\ \index{lessp-number-with-at-least-x-y}
\=\+(({\it{y\/}} $\not<$ {\it{x\/}}) $\wedge$ {\rm{good-state-of-size}}\,({\it{state\/}}, {\it{size\/}})\index{good-state-of-size}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{number-with-at-least}}\,({\it{state\/}}, {\it{x\/}}, {\it{size\/}})\index{number-with-at-least} \\ 
$\not<$$\;\;\;\;${\rm{number-with-at-least}}\,({\it{state\/}}, {\it{y\/}}, {\it{size\/}})\index{number-with-at-least})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  number-with-at-least-x-y \\ \index{number-with-at-least-x-y}
\=\+(\=\+({\rm{number-with-at-least}}\,({\it{state\/}}, {\it{x\/}}, {\it{size\/}})\index{number-with-at-least} $=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$({\it{y\/}} $\not<$ {\it{x\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{good-state-of-size}}\,({\it{state\/}}, {\it{size\/}})\index{good-state-of-size})\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{number-with-at-least}}\,({\it{state\/}}, {\it{y\/}}, {\it{size\/}})\index{number-with-at-least} $=$ {\tt{0}})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  listp-cdr-put \\ \index{listp-cdr-put}
{\rm{listp}}\,({\rm{cdr}}\,({\it{state\/}})) $\rightarrow$ {\rm{listp}}\,({\rm{cdr}}\,({\rm{put}}\,({\it{x\/}}, {\it{v\/}}, {\it{state\/}})\index{put}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  listp-cdr-apply-move \\ \index{listp-cdr-apply-move}
({\rm{listp}}\,({\rm{cdr}}\,({\it{state\/}})) $\wedge$ {\rm{listp}}\,({\it{state\/}})) $\rightarrow$ {\rm{listp}}\,({\rm{cdr}}\,({\rm{apply-move}}\,({\it{move\/}}, {\it{state\/}})\index{apply-move}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  good-state-of-size-apply-move \\ \index{good-state-of-size-apply-move}
\=\+({\rm{movep}}\,({\it{move\/}}, {\it{state\/}}, {\it{size\/}})\index{movep} $\wedge$ {\rm{good-state-of-size}}\,({\it{state\/}}, {\it{size\/}})\index{good-state-of-size}) \\ 
$\rightarrow$$\;\;\;\;${\rm{good-state-of-size}}\,({\rm{apply-move}}\,({\it{move\/}}, {\it{state\/}})\index{apply-move}, {\it{size\/}})\index{good-state-of-size}\-
\end{tabbing}


\begin{verbatim};;;; THE GAME CORRECTNESS LEMMA
\end{verbatim}\begin{tabbing}{\sc Theorem}:  computer-always-wins \\ \index{computer-always-wins}
\=\+(\=\+({\it{good-playerp\/}} $=$ ($\neg$ {\rm{loser-state}}\,({\it{state\/}}, {\it{size\/}})\index{loser-state})) \\ 
$\wedge$$\;\;\;\;${\rm{reasonable-game-statep}}\,({\it{state\/}}, {\it{size\/}})\index{reasonable-game-statep})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{game}}\,({\it{good-playerp\/}}, {\it{state\/}}, {\it{size\/}})\index{game}\-
\end{tabbing}

\begin{verbatim};;;;;;
;;;;;;
;;; Let's run an example to watch the game.  We'll need to 
;;; instantiate the dumb player's strategy to really do this,
;;; and we'll define some functions to relate bit vector states
;;; to integers.

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{nat-to-bv-state} \\  
\=\+{\rm{nat-to-bv-state}}\,({\it{state\/}}, {\it{size\/}})\index{nat-to-bv-state} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{state\/}}) \\ 
{\bf then }{\rm{cons}}\,({\rm{nat-to-bv}}\,({\rm{car}}\,({\it{state\/}}), {\it{size\/}})\index{nat-to-bv}, {\rm{nat-to-bv-state}}\,({\rm{cdr}}\,({\it{state\/}}), {\it{size\/}})\index{nat-to-bv-state}) \\ 
{\bf else }{\bf{nil}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{bv-to-nat-state} \\  
\=\+{\rm{bv-to-nat-state}}\,({\it{state\/}})\index{bv-to-nat-state} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{state\/}}) \\ 
{\bf then }{\rm{cons}}\,({\rm{bv-to-nat}}\,({\rm{car}}\,({\it{state\/}}))\index{bv-to-nat}, {\rm{bv-to-nat-state}}\,({\rm{cdr}}\,({\it{state\/}}))\index{bv-to-nat-state}) \\ 
{\bf else }{\bf{nil}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{verbatim};; a particular game where the other player uses the stupid strategy
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{game-with-stupid-move} \\  
\=\+{\rm{game-with-stupid-move}}\,({\it{good-player-turn\/}}, {\it{state\/}}, {\it{size\/}})\index{game-with-stupid-move} \\ 
$=$$\;\;\;\;$\=\+{\bf if }$\neg$ {\rm{reasonable-game-statep}}\,({\it{state\/}}, {\it{size\/}})\index{reasonable-game-statep}$\;\;${\bf then }{\bf{f}} \\ 
{\bf elseif }{\rm{number-with-at-least}}\,({\it{state\/}}, {\tt{1}}, {\it{size\/}})\index{number-with-at-least} $=$ {\tt{0}} \\ 
{\bf then }{\it{good-player-turn\/}} \\ 
{\bf else }\=\+{\bf let }\=\+{\it{move\/}}{\bf $\;$ be$\;\;$}\=\+{\bf if }{\it{good-player-turn\/}} \\ 
{\bf then }{\rm{computer-move}}\,({\it{state\/}}, {\it{size\/}})\index{computer-move} \\ 
{\bf else }{\rm{stupid-move}}\,({\it{state\/}}, {\it{size\/}})\index{stupid-move}$\;${\bf  endif}\-\- \\ 
{\bf in} \\ 
\=\+{\bf if }$\neg$ {\rm{movep}}\,({\it{move\/}}, {\it{state\/}}, {\it{size\/}})\index{movep}$\;\;${\bf then }{\bf{f}} \\ 
{\bf else }{\rm{game-with-stupid-move}}\,(\=\+$\neg$ {\it{good-player-turn\/}}, \\ 
{\rm{apply-move}}\,(\=\+{\it{move\/}}, \\ 
{\it{state\/}})\-\index{apply-move}, \\ 
{\it{size\/}})\-\index{game-with-stupid-move}$\;${\bf  endif}\-$\;${\bf  endlet}\-$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  movep-stupid-move \\ \index{movep-stupid-move}
\=\+(\=\+({\rm{number-with-at-least}}\,({\it{state\/}}, {\tt{1}}, {\it{size\/}})\index{number-with-at-least} $\not=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$({\tt{1}} $<$ {\it{size\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{good-state-of-size}}\,({\it{state\/}}, {\it{size\/}})\index{good-state-of-size})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{movep}}\,({\rm{stupid-move}}\,({\it{state\/}}, {\it{size\/}})\index{stupid-move}, {\it{state\/}}, {\it{size\/}})\index{movep}\-
\end{tabbing}


\begin{tabbing}{\sc Theorem}:  game-with-stupid-is-game \\ \index{game-with-stupid-is-game}
\=\+(\=\+({\it{good-playerp\/}} $=$ ($\neg$ {\rm{loser-state}}\,({\it{state\/}}, {\it{size\/}})\index{loser-state})) \\ 
$\wedge$$\;\;\;\;${\rm{reasonable-game-statep}}\,({\it{state\/}}, {\it{size\/}})\index{reasonable-game-statep})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{game-with-stupid-move}}\,({\it{good-playerp\/}}, {\it{state\/}}, {\it{size\/}})\index{game-with-stupid-move}\-
\end{tabbing}


%\end{list}
\printindex
\end{document}
