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

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

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

Definition: put (place, value, state) = if place ≃ 0 then cons (value, cdr (state))

else cons (car (state), put (place − 1, value, cdr (state))) endif

Definition: get (place, state) = if place ≃ 0 then car (state)

else get (place − 1, cdr (state)) endif

Theorem: get-put get (a1 , put (a2 , value, state)) = if fix (a1 ) = fix (a2 ) then value

else get (a1 , state) endif

Definition: length (list) = if listp (list) then 1 + length (cdr (list))

else 0 endif

Event: Introduce the function symbol bv-size of 0 arguments.

Definition: bitp (bit) = ((bit = 0) ∨ (bit = 1))

Definition: bvp (bv) = if listp (bv) then bitp (car (bv)) ∧ bvp (cdr (bv))

else bv = nil endif Definition: bvsp (bvs) = if listp (bvs) then bvp (car (bvs)) ∧ bvsp (cdr (bvs))

else bvs = nil endif

Definition: good-state-of-size (state, size) = if listp (state)

then bvp (car (state))

∧ (length (car (state)) = fix (size)) ∧ good-state-of-size (cdr (state), size)

else state = nil endif

Definition: good-state (state) = good-state-of-size (state, bv-size)

Definition: lessp-bv (bv1 , bv2 ) = if listp (bv1 ) ∧ listp (bv2 )

then (car (bv1 ) < car (bv2 ))

∨ ((car (bv1 ) = car (bv2 )) ∧ lessp-bv (cdr (bv1 ), cdr (bv2 ))) else f endif

;; high order bit first

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

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

;; most significant bit first

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

then (car (bv) ∗ exp (2, length (cdr (bv)))) + bv-to-nat (cdr (bv))

else 0 endif

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

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

else exp (2, size) − 1 endif Theorem: lessp-bv-length bvp (x) → (bv-to-nat (x) < exp (2, length (x)))

Theorem: lessp-bv-to-nat-bv-to-nat ((length (x) = length (y)) ∧ bvp (x) ∧ bvp (y)) → ((bv-to-nat (x) < bv-to-nat (y)) = lessp-bv (x, y))

Theorem: lessp-bv-nat-to-bv-nat-to-bv ((x < exp (2, size)) ∧ (y < exp (2, size))) → (lessp-bv (nat-to-bv (x, size), nat-to-bv (y, size)) = (x < y))

;; return the number of columns with value at least min

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

then if ¬ lessp-bv (car (state), nat-to-bv (min, size))

then 1 + number-with-at-least (cdr (state), min, size) else number-with-at-least (cdr (state), min, size) endif

else 0 endif

;; return a column number with value at least min

Definition: col-with-at-least (state, min, size) = if listp (state)

then if ¬ lessp-bv (car (state), nat-to-bv (min, size)) then 0 else 1 + col-with-at-least (cdr (state), min, size) endif

else f endif

Definition: xor (bit1 , bit2 ) = if (bit1 ≃ 0) = (bit2 ≃ 0) then 0

else 1 endif

Definition: xor-bv (bv1 , bv2 ) = if listp (bv1 ) ∧ listp (bv2 )

then cons (xor (car (bv1 ), car (bv2 )), xor-bv (cdr (bv1 ), cdr (bv2 ))) else nil endif

Definition: fix-bit (x) = if x ≃ 0 then 0

else 1 endif Definition: fix-xor-bv (bv) = if listp (bv) then cons (fix-bit (car (bv)), fix-xor-bv (cdr (bv)))

else nil endif

Definition: xor-bvs (bvs) = if listp (bvs)

then if listp (cdr (bvs)) then xor-bv (car (bvs), xor-bvs (cdr (bvs)))

else fix-xor-bv (car (bvs)) endif else nil endif

Theorem: bvp-fix-xor-bv bvp (fix-xor-bv (x))

Theorem: bvp-fix-xor-bv-identity bvp (x) → (fix-xor-bv (x) = x)

Theorem: commutativity-of-xor xor (a, b) = xor (b, a)

Theorem: associativity-of-xor xor (xor (a, b), c) = xor (a, xor (b, c))

Theorem: commutativity2-of-xor xor (c, xor (a, b)) = xor (a, xor (c, b))

Theorem: commutativity-of-xor-bv xor-bv (a, b) = xor-bv (b, a)

Theorem: associativity-of-xor-bv xor-bv (xor-bv (a, b), c) = xor-bv (a, xor-bv (b, c))

Theorem: commutativity2-of-xor-bv xor-bv (c, xor-bv (a, b)) = xor-bv (a, xor-bv (c, b))

;; return number of first vector with high bit on

Definition: high-bit-on (bvs) = if listp (bvs)

then if caar (bvs) = 1 then 0

else 1 + high-bit-on (cdr (bvs)) endif else f endif Definition: delete-pile (place, state) = if ¬ listp (state) then state

elseif place ≃ 0 then cdr (state)

else cons (car (state), delete-pile (place − 1, cdr (state))) endif

Definition: delete-high-bits (state) = if listp (state) then cons (cdar (state), delete-high-bits (cdr (state)))

else nil endif

Theorem: find-high-out-of-sync-rewrite (listp (state) ∧ listp (car (state))) → (length (car (delete-high-bits (state))) < length (car (state)))

Definition: find-high-out-of-sync (state) = if listp (state)

then if listp (car (state))

then if car (xor-bvs (state)) = 1 then high-bit-on (state)

else find-high-out-of-sync (delete-high-bits (state)) endif else f endif

else f endif

Definition: smart-move (state, size) = if number-with-at-least (state, 2, size) = 0

then cons (col-with-at-least (state, 1, size), nat-to-bv (0, size))

elseif number-with-at-least (state, 2, size) = 1 then cons (col-with-at-least (state, 2, size),

if (number-with-at-least (state, 1, size) mod 2) = 0 then nat-to-bv (0, size) else nat-to-bv (1, size) endif) else let badcol be find-high-out-of-sync (state)

in

cons (badcol, xor-bvs (delete-pile (badcol, state))) endlet endif

Definition: apply-move (move, state) = put (car (move), cdr (move), state)

Definition: all-zeros (bv) = if listp (bv) then (car (bv) = 0) ∧ all-zeros (cdr (bv))

else t endif Definition: loser-state (state, size) = (((number-with-at-least (state, 2, size) = 0)

∧ ((number-with-at-least (state, 1, size) mod 2) = 1)) ∨ ((0 < number-with-at-least (state, 2, size))

∧ all-zeros (xor-bvs (state))))

Definition: movep (move, state, size) = (lessp-bv (cdr (move), get (car (move), state))

∧ (length (cdr (move)) = size)

∧ bvp (cdr (move))

∧ (car (move) < length (state)))

;; the column of place has a 1 bit at the highest position
;; whose xors are not 0

Definition: high-bit-out-of-sync (place, state) = if listp (state)

then if listp (car (state))

then ((car (get (place, state)) = 1) ∧ (car (xor-bvs (state)) = 1)) ∨ ((car (xor-bvs (state)) = 0)

∧ high-bit-out-of-sync (place,

delete-high-bits (state)))

else f endif else f endif

Definition: lessp-when-high-bit-recursion (state, size) = if size ≃ 0 then t

else lessp-when-high-bit-recursion (delete-high-bits (state), size − 1) endif

Theorem: equal-length-0 (length (x) = 0) = (¬ listp (x))

Theorem: equal-length-1 (length (x) = 1) = (listp (x) ∧ (¬ listp (cdr (x))))

Theorem: good-state-of-size-delete-high-bits good-state-of-size (state, 1 + x) → good-state-of-size (delete-high-bits (state), x)

Theorem: high-bit-out-of-sync-empty (good-state-of-size (state, size) ∧ (size ≃ 0)) → (¬ high-bit-out-of-sync (place, state))

Theorem: get-of-bad-place (place ≮ length (state)) → (get (place, state) = 0)

Theorem: listp-delete-high-bits listp (delete-high-bits (x)) = listp (x)

Definition: bv-not (x) = if x = 0 then 1

else 0 endif

Theorem: bvp-xor-bv bvp (xor-bv (x, y))

Theorem: bvp-xor-bvs bvp (xor-bvs (state))

Theorem: equal-bitp-simplify (bitp (x) ∧ (x ≠ 0)) → ((x = y) = (y = 1))

;; make all bit equality constants into 0

Theorem: equal-bit-1 bitp (x) → ((x = 1) = (x ≠ 0))

Theorem: bitp-car-bvp bvp (x) → bitp (car (x))

Theorem: good-state-of-size-means-bvsp good-state-of-size (state, size) → bvsp (state)

Theorem: listp-xor-bv listp (xor-bv (x, y)) = (listp (x) ∧ listp (y))

Theorem: listp-xor-bvs good-state-of-size (state, size) → (listp (xor-bvs (state)) = (listp (state) ∧ (0 < size)))

Theorem: bvp-get good-state-of-size (state, size) → (bvp (get (place, state)) = (place < length (state)))

Theorem: listp-get good-state-of-size (state, size) → (listp (get (place, state))

= ((place < length (state)) ∧ (0 < size)))

Theorem: car-xor-bv (listp (x) ∧ listp (y)) → (car (xor-bv (x, y)) = xor (car (x), car (y)))

Definition: lessp-bv-recursion (list, size) = if size ≃ 0 then t

else lessp-bv-recursion (cdr (list), size − 1) endif

Definition: firstn (list, n) = if ¬ listp (list) then list

elseif n ≃ 0 then nil

else cons (car (list), firstn (cdr (list), n − 1)) endif

Definition: min (x, y) = if x < y then fix (x)

else fix (y) endif

Theorem: xor-bv-inverse xor-bv (a, xor-bv (a, b)) = firstn (fix-xor-bv (b), min (length (a), length (b)))

Theorem: xor-bv-fix-xor-bv (xor-bv (fix-xor-bv (x), y) = xor-bv (x, y)) ∧ (xor-bv (y, fix-xor-bv (x)) = xor-bv (y, x))

Theorem: firstn-noop (x ≮ length (list)) → (firstn (list, x) = list)

Theorem: xor-bvs-delete-high-bits good-state-of-size (state, size) → (xor-bvs (delete-high-bits (state))

= if (¬ listp (state)) ∨ (1 ≮ size) then nil else cdr (xor-bvs (state)) endif)

Theorem: length-xor-bvs good-state-of-size (state, size) → (length (xor-bvs (state))

= if listp (state) then fix (size)

else 0 endif)

Theorem: listp-delete-pile listp (delete-pile (place, state)) = (listp (state) ∧ (¬ ((place ≃ 0) ∧ (¬ listp (cdr (state))))))

Theorem: xor-bvs-delete-pile (good-state-of-size (state, size) ∧ (place < length (state))) → (xor-bvs (delete-pile (place, state))

= if 1 < length (state)

then xor-bv (get (place, state), xor-bvs (state)) else nil endif)

Theorem: listp-delete-pile-delete-high-bits listp (delete-pile (place, delete-high-bits (state))) = listp (delete-pile (place, state))

Theorem: get-delete-high-bits get (place, delete-high-bits (state)) = cdr (get (place, state))

Theorem: delete-pile-delete-high-bits delete-pile (place, delete-high-bits (state)) = delete-high-bits (delete-pile (place, state))

Theorem: good-state-of-size-delete-pile good-state-of-size (state, size) → good-state-of-size (delete-pile (place, state), size)

Theorem: silly-listp-cdr (1 < length (x)) → listp (cdr (x))

Theorem: numberp-car-bv bvp (bv) → (car (bv) ∈ N)

Theorem: length-delete-high-bits length (delete-high-bits (x)) = length (x)

;; special version to help with free variable problem of next lemma

Theorem: xor-bvs-delete-high-bits-2 ((size ≠ 0) ∧ good-state-of-size (state, size)) → (xor-bvs (delete-high-bits (state))

= if (¬ listp (state)) ∨ (1 ≮ size) then nil else cdr (xor-bvs (state)) endif)

Theorem: lessp-when-high-bit-out-of-sync-helper (good-state-of-size (state, size) ∧ (place < length (state)) ∧ (1 < length (state)) ∧ high-bit-out-of-sync (place, state)) → lessp-bv (xor-bvs (delete-pile (place, state)), get (place, state))

Event: Disable xor-bvs-delete-high-bits-2.

Theorem: high-bit-out-of-sync-trivial (place ≮ length (state)) → (¬ high-bit-out-of-sync (place, state))

Theorem: lessp-when-high-bit-out-of-sync (good-state-of-size (state, size) ∧ (1 < length (state)) ∧ high-bit-out-of-sync (place, state)) → lessp-bv (xor-bvs (delete-pile (place, state)), get (place, state))

Theorem: bitp-car-xor-bvs bitp (car (xor-bvs (bvs)))

Theorem: high-bit-on-works ((car (xor-bvs (state)) = 1) ∧ bvsp (state)) → (car (get (high-bit-on (state), state)) = 1)

Theorem: all-zeros-length-1 (length (x) = 1) → (all-zeros (x) = (car (x) = 0))

Theorem: all-zeros-xor-bvs-simple (good-state-of-size (state, size) ∧ (size < 2)) → (all-zeros (xor-bvs (state))

= ((size ≃ 0) ∨ (¬ listp (state)) ∨ (car (xor-bvs (state)) = 0)))

Theorem: find-high-out-of-sync-works ((¬ all-zeros (xor-bvs (state))) ∧ good-state-of-size (state, size)) → high-bit-out-of-sync (find-high-out-of-sync (state), state)

Theorem: bvp-nat-to-bv bvp (nat-to-bv (nat, size))

Theorem: silly-lessp-sub1-exp-length ((nat ≮ exp (2, length (bv))) ∧ bvp (bv)) → (nat ≮ bv-to-nat (bv))

Definition: all-ones (size) = if size ≃ 0 then nil

else cons (1, all-ones (size − 1)) endif

Theorem: nat-to-bv-is-all-ones (nat ≮ exp (2, size)) → (nat-to-bv (nat, size) = all-ones (size))

Theorem: length-all-ones length (all-ones (size)) = fix (size)

Theorem: bvp-all-ones bvp (all-ones (size))

Theorem: lessp-bv-all-ones-arg1 bvp (bv) → (¬ lessp-bv (all-ones (size), bv))

Theorem: lessp-bv-all-ones-arg2 ((length (bv) = size) ∧ bvp (bv)) → (lessp-bv (bv, all-ones (size))

= (bv-to-nat (bv) < (exp (2, size) − 1)))

Theorem: lessp-bv-nat-to-bv ((length (bv) = fix (size)) ∧ (nat < exp (2, size)) ∧ bvp (bv)) → ((lessp-bv (nat-to-bv (nat, size), bv) = (nat < bv-to-nat (bv)))

∧ (lessp-bv (bv, nat-to-bv (nat, size)) = (bv-to-nat (bv) < nat)))

Theorem: length-car-state good-state-of-size (state, size) → (length (car (state))

= if listp (state) then fix (size)

else 0 endif)

Theorem: bvp-car (bvsp (x) ∧ listp (x)) → bvp (car (x))

Theorem: lessp-bv-zero (zero ≃ 0) → (¬ lessp-bv (x, nat-to-bv (zero, size)))

Theorem: number-with-at-least-zero (zero ≃ 0) → (number-with-at-least (bv, zero, size) = length (bv))

Theorem: lessp-1-exp (1 < exp (x, y)) = ((1 < x) ∧ (y ≄ 0))

Theorem: lessp-x-exp-x-y (x < exp (x, y)) = (((x ≃ 0) ∧ (y ≃ 0)) ∨ ((1 < x) ∧ (1 < y)))

Theorem: lessp-bv-col-get-with-at-least ((x < y) ∧ (y < exp (2, size)) ∧ good-state-of-size (state, size) ∧ (number-with-at-least (state, y, size) ≄ 0)) → lessp-bv (nat-to-bv (x, size), get (col-with-at-least (state, y, size), state))

Theorem: lessp-1-x-means-not-zerop-x (1 < x) → (x ≄ 0)

Theorem: length-xor-bvs-delete-pile ((1 < length (state)) ∧ good-state-of-size (state, size)) → (length (xor-bvs (delete-pile (n, state))) = fix (size))

Theorem: high-bit-on-reasonable ((car (xor-bvs (state)) = 1) ∧ good-state-of-size (state, size)) → (high-bit-on (state) < length (state))

Theorem: find-high-out-of-sync-reasonable (listp (state) ∧ good-state-of-size (state, size)) → (find-high-out-of-sync (state) < length (state))

Theorem: col-with-at-least-reasonable ((number-with-at-least (state, n, size) ≄ 0) ∧ good-state-of-size (state, size)) → (col-with-at-least (state, n, size) < length (state))

Theorem: lessp-length (n < length (state)) → listp (state)

Event: Disable equal-bitp-simplify.

Theorem: listp-nat-to-bv listp (nat-to-bv (n, size)) = (size ≄ 0)

Theorem: number-with-at-least-simple (good-state-of-size (state, size) ∧ (size ≃ 0)) → (number-with-at-least (state, n, size) = length (state))

Theorem: bitp-car bvp (bv) → bitp (car (bv))

Theorem: car-xor-bv-better car (xor-bv (x, y)) = if listp (x) ∧ listp (y) then xor (car (x), car (y))

else 0 endif

Theorem: xor-bv-inverse-2 xor-bv (b, xor-bv (a, a)) = firstn (fix-xor-bv (b), min (length (a), length (b)))

Theorem: length-fix-xor-bv length (fix-xor-bv (x)) = length (x)

Theorem: xor-bvs-put (good-state-of-size (state, size) ∧ (length (value) = size) ∧ (place < length (state))) → (xor-bvs (put (place, value, state))

= xor-bv (get (place, state), xor-bv (value, xor-bvs (state))))

Definition: triple-cdr-induction (a, b, c) = if listp (a) ∧ listp (b) ∧ listp (c)

then triple-cdr-induction (cdr (a), cdr (b), cdr (c))

else t endif

Theorem: all-zeros-xor-bv-identity ((length (a) = length (b)) ∧ (length (b) = length (c)) ∧ all-zeros (c)) → (all-zeros (xor-bv (a, xor-bv (b, c)))

= (fix-xor-bv (a) = fix-xor-bv (b)))

Theorem: length-get (good-state-of-size (state, size) ∧ (place < length (state))) → (length (get (place, state)) = fix (size))

Theorem: all-zeros-xor-bvs-put (all-zeros (xor-bvs (state)) ∧ good-state-of-size (state, size) ∧ (length (value) = size) ∧ (place < length (state))) → (all-zeros (xor-bvs (put (place, value, state)))

= (fix-xor-bv (value) = get (place, state)))

Theorem: lessp-bv-x-x ¬ lessp-bv (x, x)

Theorem: put-get (x < length (state)) → (put (x, get (x, state), state) = state)

Theorem: get-means-number-with-at-least ((¬ lessp-bv (get (x, state), nat-to-bv (n, size))) ∧ (x < length (state))) → (number-with-at-least (state, n, size) ≠ 0)

Theorem: number-with-at-least-put ((p < length (state)) ∧ good-state-of-size (state, size) ∧ (length (v) = size)) → (number-with-at-least (put (p, v, state), n, size)

= if lessp-bv (get (p, state), nat-to-bv (n, size)) then if lessp-bv (v, nat-to-bv (n, size))

then number-with-at-least (state, n, size)

else 1 + number-with-at-least (state, n, size) endif elseif lessp-bv (v, nat-to-bv (n, size)) then number-with-at-least (state, n, size) − 1 else number-with-at-least (state, n, size) endif)

Theorem: all-zeros-xor-bvs-when-lone-big-simple (good-state-of-size (state, 1) ∧ (number-with-at-least (state, 1, 1) = 1)) → (car (xor-bvs (state)) = 1)

Theorem: plus-exp-2-x-exp-2-x (exp (2, x) + exp (2, x)) = exp (2, 1 + x)

Theorem: lessp-exp-exp (exp (x, y) < exp (x, z)) = if x ≃ 0 then (y ≄ 0) ∧ (z ≃ 0)

else (x ≠ 1) ∧ (y < z) endif

Theorem: nat-to-bv-exp (n ≮ size) → (nat-to-bv (exp (2, n), size) = all-ones (size))

Theorem: bv-to-nat-all-zeros bvp (bv) → ((bv-to-nat (bv) = 0) = all-zeros (bv))

Theorem: lessp-bv-to-nat-1 bvp (bv) → ((bv-to-nat (bv) < 1) = all-zeros (bv))

Theorem: car-nat-to-bv-exp (n < size) → (car (nat-to-bv (exp (2, n), size))

= if (1 + n) = size then 1 else 0 endif)

;; let's disable some time wasters

Event: Disable equal-bitp-simplify.

Event: Disable all-zeros-xor-bvs-when-lone-big-simple.

Event: Disable high-bit-on-reasonable.

Event: Disable find-high-out-of-sync-reasonable.

Theorem: all-zeros-firstn-difference (bvp (x) ∧ (length (x) = size) ∧ (n < size)) → (lessp-bv (x, nat-to-bv (exp (2, n), size))

= all-zeros (firstn (x, size − n)))

Theorem: all-zeros-xor-bv (bvp (a) ∧ bvp (b) ∧ (length (a) = length (b))) → (all-zeros (xor-bv (a, b)) = (a = b))

Theorem: lessp-bv-nat-to-bv-1 ((length (x) = size) ∧ bvp (x)) → (lessp-bv (x, nat-to-bv (1, size)) = ((0 < size) ∧ all-zeros (x)))

Definition: double-length-induction (x, y) = if listp (x) ∧ listp (y) then double-length-induction (cdr (x), cdr (y))

else t endif

Theorem: all-zeros-equal (bvp (a) ∧ bvp (b) ∧ all-zeros (a) ∧ all-zeros (b)) → ((a = b) = (length (a) = length (b)))

Event: Disable all-zeros-equal.

Theorem: all-zeros-xor-bvs (good-state-of-size (z, size) ∧ (number-with-at-least (z, 1, size) = 0)) → all-zeros (xor-bvs (z))

Theorem: length-firstn length (firstn (list, size)) = min (length (list), size)

Theorem: length-xor-bv length (xor-bv (a, b)) = min (length (a), length (b))

Theorem: firstn-xor-bv firstn (xor-bv (a, b), size) = xor-bv (firstn (a, size), firstn (b, size))

Theorem: all-zeros-xor-bvs-firstn (good-state-of-size (z, size) ∧ (n < size) ∧ (number-with-at-least (z, exp (2, n), size) = 0)) → all-zeros (firstn (xor-bvs (z), size − n))

Theorem: all-zeros-if-firstn-zeros all-zeros (x) → all-zeros (firstn (x, size))

Theorem: good-state-of-size-length-xor-bvs good-state-of-size (z, length (xor-bvs (z))) = good-state-of-size (z, length (car (z)))

Theorem: bvp-firstn bvp (x) → bvp (firstn (x, size))

Theorem: number-with-at-least-exp-2 (good-state-of-size (state, size) ∧ (n < size) ∧ all-zeros (firstn (xor-bvs (state), size − n))) → (number-with-at-least (state, exp (2, n), size) ≠ 1)

Theorem: number-with-at-least-2 (good-state-of-size (state, size) ∧ (1 < size) ∧ all-zeros (xor-bvs (state))) → (number-with-at-least (state, 2, size) ≠ 1)

Theorem: lessp-bv-all-zeros (all-zeros (x) ∧ (length (x) = length (y)) ∧ bvp (x) ∧ bvp (y)) → ((lessp-bv (x, y) = (¬ all-zeros (y))) ∧ (¬ lessp-bv (y, x)))

Theorem: number-with-at-least-means-get (good-state-of-size (state, size) ∧ (z < length (state)) ∧ (number-with-at-least (state, n, size) = 0)) → ((bv-to-nat (get (z, state)) < n) = t)

Theorem: remainder-sub1-hack ((x mod y) = p) → (((x − 1) mod y)

= if x ≃ 0 then 0 elseif p ≃ 0 then y − 1 else p − 1 endif)

;; ought to be using more up-to-date naturals library!

Theorem: equal-times-x ((y ∗ x) = x) = ((x = 0) ∨ ((x ∈ N) ∧ (y = 1)))

Theorem: equal-times-x-2 ((x ∗ y) = x) = ((x = 0) ∨ ((x ∈ N) ∧ (y = 1)))

Theorem: equal-exp-x-x (exp (x, y) = x) = ((x = 1) ∨ ((x = 0) ∧ (y ≄ 0)) ∨ ((x ∈ N) ∧ (y = 1)))

Theorem: lessp-bv-2-means (bvp (x) ∧ (1 < length (x))) → (lessp-bv (x, nat-to-bv (2, length (x)))

= (all-zeros (x) ∨ (x = nat-to-bv (1, length (x)))))

Theorem: lessp-bv-x-1-means ((length (x) = size) ∧ bvp (x) ∧ (1 < size)) → (lessp-bv (x, nat-to-bv (1, size)) = all-zeros (x))

Theorem: nat-to-bv-not-numberp (n ∉ N) → (nat-to-bv (n, size) = nat-to-bv (0, size))

Theorem: all-zeros-nat-to-bv-1 (size ≄ 0) → (all-zeros (nat-to-bv (n, size)) = (n ≃ 0))

Theorem: get-when-lessp-bv-2 (good-state-of-size (state, size) ∧ (1 < size) ∧ (z < length (state)) ∧ (number-with-at-least (state, 2, size) = 0) ∧ bvp (x) ∧ (length (x) = size)) → (lessp-bv (x, get (z, state))

= (all-zeros (x) ∧ (get (z, state) = nat-to-bv (1, size))))

;; replacement rule version

Theorem: find-high-out-of-sync-reasonable2 (listp (state) ∧ good-state-of-size (state, size)) → ((find-high-out-of-sync (state) < length (state)) = t)

Theorem: xor-bv-0 ((length (x) = size) ∧ bvp (x)) → ((xor-bv (nat-to-bv (0, size), x) = x)

∧ (xor-bv (x, nat-to-bv (0, size)) = x))

Theorem: lessp-bv-to-nat-get-col-with-at-least (good-state-of-size (state, size) ∧ (n < exp (2, size)) ∧ (1 < size) ∧ (number-with-at-least (state, n, size) ≄ 0)) → ((bv-to-nat (get (col-with-at-least (state, n, size), state)) < n) = f)

;; needed?

Theorem: lessp-get-exp-2-size (good-state-of-size (state, size) ∧ (z < length (state))) → ((bv-to-nat (get (z, state)) < exp (2, size)) = t)

Theorem: equal-remainder-sub1-0 (((x − 1) mod p) = 0) = ((x ≃ 0) ∨ (p = 1) ∨ ((x mod p) = 1))

Theorem: lessp-1-rewrite (1 < x) = ((x ∈ N) ∧ (x ≠ 0) ∧ (x ≠ 1))

Theorem: numberp-col-with-at-least (col-with-at-least (state, n, size) ∈ N) = listp (state)

Theorem: equal-remainder-2-special ((((x mod 2) = y) ∧ (y = 1)) → ((x mod 2) ≠ 0)) ∧ ((((x mod 2) ≠ y) ∧ (y = 1)) → (((x mod 2) = 0) = t))

Theorem: listp-fix-xor-bv listp (fix-xor-bv (x)) = listp (x)

Theorem: lessp-length-x-length-xor-bvs-put-x (length (x) < length (xor-bvs (put (z, x, state)))) = f

Theorem: length-xor-bvs-put (good-state-of-size (state, size) ∧ listp (state) ∧ (z < length (state)) ∧ (length (x) = size)) → (length (xor-bvs (put (z, x, state))) = size)

Theorem: lessp-1-length ((n < length (x)) ∧ (n ≄ 0)) → listp (cdr (x))

Theorem: all-zeros-get-col-with-at-least (good-state-of-size (state, size) ∧ (1 < size) ∧ (1 < length (state)) ∧ (n ≄ 0) ∧ (number-with-at-least (state, n, size) ≄ 0)) → (¬ all-zeros (get (col-with-at-least (state, n, size), state)))

;; these dinosaurs aren't needed any more

Event: Disable equal-bit-1.

Event: Disable silly-listp-cdr.

;; this takes too much time and isn't needed often

Event: Disable nat-to-bv-is-all-ones.

Theorem: equal-remainder-sub1-x-2-special (((x − 1) mod 2) = 1) = ((x ≄ 0) ∧ ((x mod 2) = 0))

;;;;;;
;;;;;;
;; The big lemmas about NIM

Theorem: smart-moves-from-not-loser ((¬ loser-state (state, size)) ∧ good-state-of-size (state, size) ∧ (1 < length (state)) ∧ (1 < size) ∧ (number-with-at-least (state, 1, size) ≠ 0)) → loser-state (apply-move (smart-move (state, size), state), size)

Definition: stupid-move (state, size) = let pile be col-with-at-least (state, 1, size)

in

cons (pile, nat-to-bv (bv-to-nat (get (pile, state)) − 1, size)) endlet

Definition: computer-move (state, size) = if loser-state (state, size) then stupid-move (state, size)

else smart-move (state, size) endif

Theorem: smart-move-is-a-move (good-state-of-size (state, size) ∧ (¬ loser-state (state, size)) ∧ (1 < size) ∧ (1 < length (state)) ∧ (0 < number-with-at-least (state, 1, size))) → movep (smart-move (state, size), state, size)

Theorem: moves-from-loser (loser-state (state, size) ∧ (1 < size) ∧ good-state-of-size (state, size) ∧ movep (move, state, size)) → (¬ loser-state (apply-move (move, state), size))

;;;; put together big lemmas in one theorem about "game"

Conservative Axiom: a-move-intro ((number-with-at-least (state, 1, size) ≄ 0) ∧ (1 < size) ∧ good-state-of-size (state, size)) → movep (a-move (state, size), state, size)

Simultaneously, we introduce the new function symbol a-move.

Definition: reasonable-game-statep (state, size) = (good-state-of-size (state, size)

∧ (1 < size)

∧ (1 < length (state)))

Definition: sum-matches (state) = if listp (state)

then bv-to-nat (car (state)) + sum-matches (cdr (state))

else 0 endif

Theorem: equal-x-nat-to-bv-0 (bvp (x) ∧ all-zeros (x)) → ((x = nat-to-bv (0, length (x))) = t)

Theorem: get-from-zeros (good-state-of-size (z, size) ∧ (size ≄ 0) ∧ (number-with-at-least (z, 1, size) = 0) ∧ (d < length (z))) → (get (d, z) = nat-to-bv (0, size))

Theorem: lessp-sum-matches-member (place < length (state)) → (sum-matches (state) ≮ bv-to-nat (get (place, state)))

Theorem: sum-matches-put (place < length (state)) → (sum-matches (put (place, v, state))

= ((sum-matches (state) − bv-to-nat (get (place, state))) + bv-to-nat (v)))

Theorem: lessp-not-all-zeros ((¬ all-zeros (x)) ∧ bvp (x) ∧ listp (x)) → (0 < bv-to-nat (x))

Definition: game-ends-recursion (move, state, size) = if listp (state) ∧ (car (move) ≄ 0)

then game-ends-recursion (cons (car (move) − 1, cdr (move)), cdr (state), size)

else t endif

Theorem: game-ends ((number-with-at-least (state, 1, size) ≠ 0) ∧ good-state-of-size (state, size) ∧ (size ≄ 0) ∧ movep (move, state, size)) → ((sum-matches (apply-move (move, state)) < sum-matches (state)) = t)

Event: Disable apply-move.

Event: Disable smart-move.

Event: Disable stupid-move.

Definition: game (good-player-turn, state, size) = if ¬ reasonable-game-statep (state, size) then f

elseif number-with-at-least (state, 1, size) = 0

then good-player-turn

else let move be if good-player-turn then computer-move (state, size) else a-move (state, size) endif

in

if ¬ movep (move, state, size) then f else game (¬ good-player-turn,

apply-move (move, state), size) endif endlet endif Theorem: transitivity-of-lessp-bv (lessp-bv (x, y) ∧ (¬ lessp-bv (z, y)) ∧ (length (x) = length (y)) ∧ (length (y) = length (z)) ∧ bvp (x) ∧ bvp (y) ∧ bvp (z)) → lessp-bv (x, z)

Theorem: nat-to-bv-size-1 nat-to-bv (x, 1) = if x ≃ 0 then '(0)

else '(1) endif

Theorem: lessp-bv-nat-to-bv-nat-to-bv-2 (x ≮ y) → (¬ lessp-bv (nat-to-bv (x, size), nat-to-bv (y, size)))

Theorem: lessp-bv-of-larger (lessp-bv (v, nat-to-bv (x, a)) ∧ (length (v) = a) ∧ bvp (v) ∧ (y ≮ x)) → lessp-bv (v, nat-to-bv (y, a))

Theorem: lessp-number-with-at-least-x-y ((y ≮ x) ∧ good-state-of-size (state, size)) → (number-with-at-least (state, x, size)

≮ number-with-at-least (state, y, size))

Theorem: number-with-at-least-x-y ((number-with-at-least (state, x, size) = 0) ∧ (y ≮ x) ∧ good-state-of-size (state, size)) → (number-with-at-least (state, y, size) = 0)

Theorem: listp-cdr-put listp (cdr (state)) → listp (cdr (put (x, v, state)))

Theorem: listp-cdr-apply-move (listp (cdr (state)) ∧ listp (state)) → listp (cdr (apply-move (move, state)))

Theorem: good-state-of-size-apply-move (movep (move, state, size) ∧ good-state-of-size (state, size)) → good-state-of-size (apply-move (move, state), size)

;;;; THE GAME CORRECTNESS LEMMA

Theorem: computer-always-wins ((good-playerp = (¬ loser-state (state, size))) ∧ reasonable-game-statep (state, size)) → game (good-playerp, state, size)

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

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

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

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

then cons (bv-to-nat (car (state)), bv-to-nat-state (cdr (state)))

else nil endif

;; a particular game where the other player uses the stupid strategy

Definition: game-with-stupid-move (good-player-turn, state, size) = if ¬ reasonable-game-statep (state, size) then f

elseif number-with-at-least (state, 1, size) = 0

then good-player-turn

else let move be if good-player-turn then computer-move (state, size) else stupid-move (state, size) endif

in

if ¬ movep (move, state, size) then f

else game-with-stupid-move (¬ good-player-turn,

apply-move (move,

state),

size) endif endlet endif

Theorem: movep-stupid-move ((number-with-at-least (state, 1, size) ≠ 0) ∧ (1 < size) ∧ good-state-of-size (state, size)) → movep (stupid-move (state, size), state, size)

Theorem: game-with-stupid-is-game ((good-playerp = (¬ loser-state (state, size))) ∧ reasonable-game-statep (state, size)) → game-with-stupid-move (good-playerp, state, size)

Index

a-move, 23, 24 a-move-intro, 23 all-ones, 13, 14, 17 all-zeros, 8, 9, 13, 16–21, 23, 24 all-zeros-equal, 18 all-zeros-firstn-difference, 18 all-zeros-get-col-with-at-least, 21 all-zeros-if-firstn-zeros, 18 all-zeros-length-1, 13 all-zeros-nat-to-bv-1, 20 all-zeros-xor-bv, 18 all-zeros-xor-bv-identity, 16 all-zeros-xor-bvs, 18 all-zeros-xor-bvs-firstn, 18 all-zeros-xor-bvs-put, 16 all-zeros-xor-bvs-simple, 13 all-zeros-xor-bvs-when-lone-big

-simple, 17 apply-move, 8, 22–26 associativity-of-xor, 7 associativity-of-xor-bv, 7

bitp, 4, 10, 13, 15 bitp-car, 15 bitp-car-bvp, 10 bitp-car-xor-bvs, 13 bv-not, 10 bv-size, 4, 5 bv-to-nat, 5, 6, 13, 14, 17, 19–24, 26 bv-to-nat-all-zeros, 17 bv-to-nat-nat-to-bv, 5 bv-to-nat-state, 26 bvp, 4–7, 9, 10, 12–15, 17–20, 23–25 bvp-all-ones, 14 bvp-car, 14 bvp-firstn, 19 bvp-fix-xor-bv, 7 bvp-fix-xor-bv-identity, 7 bvp-get, 10 bvp-nat-to-bv, 13 bvp-xor-bv, 10 bvp-xor-bvs, 10 bvsp, 5, 10, 13, 14

car-nat-to-bv-exp, 17

car-xor-bv, 11

car-xor-bv-better, 15

col-with-at-least, 6, 8, 14, 15, 20–22 col-with-at-least-reasonable, 15 commutativity-of-xor, 7 commutativity-of-xor-bv, 7 commutativity2-of-xor, 7 commutativity2-of-xor-bv, 7 computer-always-wins, 26 computer-move, 22, 24, 26

delete-high-bits, 8–12 delete-pile, 8, 12, 13, 15 delete-pile-delete-high-bits, 12 double-length-induction, 18

equal-bit-1, 10

equal-bitp-simplify, 10 equal-exp-x-x, 20 equal-length-0, 9 equal-length-1, 9 equal-remainder-2-special, 21 equal-remainder-sub1-0, 21 equal-remainder-sub1-x-2-specia

l, 22 equal-times-x, 19 equal-times-x-2, 19 equal-x-nat-to-bv-0, 23 exp, 5, 6, 13, 14, 17–21

find-high-out-of-sync, 8, 13, 15, 20 find-high-out-of-sync-reasonable, 15

2, 20 find-high-out-of-sync-rewrite, 8 find-high-out-of-sync-works, 13 firstn, 11, 15, 18, 19 firstn-noop, 11 firstn-xor-bv, 18 fix-bit, 6, 7 fix-xor-bv, 7, 11, 15, 16, 21

game, 24, 26 game-ends, 24 game-ends-recursion, 24 game-with-stupid-is-game, 27 game-with-stupid-move, 26, 27 get, 4, 9–14, 16, 17, 19–24 get-delete-high-bits, 12 get-from-zeros, 23 get-means-number-with-at-least, 16 get-of-bad-place, 10 get-put, 4 get-when-lessp-bv-2, 20 good-state, 5 good-state-of-size, 5, 9–26 good-state-of-size-apply-move, 25 good-state-of-size-delete-high-

bits, 9 good-state-of-size-delete-pile, 12 good-state-of-size-length-xor-bv

s, 19 good-state-of-size-means-bvsp, 10

high-bit-on, 7, 8, 13, 15 high-bit-on-reasonable, 15 high-bit-on-works, 13 high-bit-out-of-sync, 9, 10, 12, 13 high-bit-out-of-sync-empty, 10 high-bit-out-of-sync-trivial, 13

length, 4–6, 8–16, 18–25 length-all-ones, 14 length-car-state, 14 length-delete-high-bits, 12 length-firstn, 18 length-fix-xor-bv, 15 length-get, 16 length-nat-to-bv, 5 length-xor-bv, 18 length-xor-bvs, 11 length-xor-bvs-delete-pile, 15 length-xor-bvs-put, 21 lessp-1-exp, 14 lessp-1-length, 21 lessp-1-rewrite, 21 lessp-1-x-means-not-zerop-x, 15 lessp-bv, 5, 6, 9, 12–14, 16–20, 25 lessp-bv-2-means, 20 lessp-bv-all-ones-arg1, 14 lessp-bv-all-ones-arg2, 14 lessp-bv-all-zeros, 19 lessp-bv-col-get-with-at-least, 14 lessp-bv-length, 6 lessp-bv-nat-to-bv, 14 lessp-bv-nat-to-bv-1, 18 lessp-bv-nat-to-bv-nat-to-bv, 6 lessp-bv-nat-to-bv-nat-to-bv-2, 25 lessp-bv-of-larger, 25 lessp-bv-recursion, 11 lessp-bv-to-nat-1, 17 lessp-bv-to-nat-bv-to-nat, 6 lessp-bv-to-nat-get-col-with-at

-least, 20 lessp-bv-x-1-means, 20 lessp-bv-x-x, 16 lessp-bv-zero, 14 lessp-exp-exp, 17 lessp-get-exp-2-size, 21 lessp-length, 15 lessp-length-x-length-xor-bvs-p

ut-x, 21 lessp-not-all-zeros, 24 lessp-number-with-at-least-x-y, 25 lessp-sum-matches-member, 23 lessp-when-high-bit-out-of-sync, 13

-helper, 12 lessp-when-high-bit-recursion, 9 lessp-x-exp-x-y, 14 listp-cdr-apply-move, 25 listp-cdr-put, 25 listp-delete-high-bits, 10 listp-delete-pile, 12 listp-delete-pile-delete-high-bit

s, 12 listp-fix-xor-bv, 21 listp-get, 11 listp-nat-to-bv, 15 listp-xor-bv, 10 listp-xor-bvs, 10 loser-state, 9, 22, 23, 26, 27

min, 11, 15, 18 movep, 9, 22–26 movep-stupid-move, 26 moves-from-loser, 23

nat-to-bv, 5, 6, 8, 13–18, 20, 22, 23,

25, 26 nat-to-bv-exp, 17 nat-to-bv-is-all-ones, 13 nat-to-bv-not-numberp, 20 nat-to-bv-size-1, 25 nat-to-bv-state, 26 number-with-at-least, 6, 8, 9, 14–26 number-with-at-least-2, 19 number-with-at-least-exp-2, 19 number-with-at-least-means-get, 19 number-with-at-least-put, 16 number-with-at-least-simple, 15 number-with-at-least-x-y, 25 number-with-at-least-zero, 14 numberp-car-bv, 12 numberp-col-with-at-least, 21

plus-exp-2-x-exp-2-x, 17 put, 4, 8, 16, 21, 24, 25 put-get, 16

reasonable-game-statep, 23, 24, 26,

27 remainder-sub1-hack, 19

silly-lessp-sub1-exp-length, 13 silly-listp-cdr, 12 smart-move, 8, 22 smart-move-is-a-move, 22 smart-moves-from-not-loser, 22 stupid-move, 22, 26 sum-matches, 23, 24 sum-matches-put, 24 transitivity-of-lessp-bv, 25 triple-cdr-induction, 16

xor, 6, 7, 11, 15

xor-bv, 6, 7, 10–12, 15, 16, 18, 20 xor-bv-0, 20 xor-bv-fix-xor-bv, 11 xor-bv-inverse, 11 xor-bv-inverse-2, 15 xor-bvs, 7–13, 15–19, 21 xor-bvs-delete-high-bits, 11 xor-bvs-delete-high-bits-2, 12 xor-bvs-delete-pile, 12 xor-bvs-put, 16