\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 Sakthi Subramanian.  All Rights Reserved.

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

 NO WARRANTY

 Sakthi Subramanian 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 Sakthi Subramanian 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.

|#

\end{verbatim} \newpage
 \begin{center}
 \Large
 A Mechanically Checked Proof of the \\
 Mutilated Checkerboard Theorem \\[1in]
 \large
 Sakthi Subramanian
 \end{center} \newpage

 
 Here is a formalization of the nxn mutilated checkerboard problem using Bob
 Boyer's representation. I later learnt that Herb Simon uses a 
 similar trick in
 discussing a solution to a ``Cube-brick problem''. Our formalization allows
 us to prove by induction that every sequence of
 domino-placements leads to a state in which the number of covered black
 and white squares are equal. However, in the mutilated board the number of
 black and white squares are not equal and hence it cannot be covered 
 completely. An
 interesting feature is the definition of the color predicates in terms of 
 the representation of the squares. White squares are those whose coordinates
 sum up to an even number and black squares are those whose coordinates
 sum upto an odd number.
 We prove the theorem for a nxn board using mathematical induction. 

 REPRESENTATION:

 We label the squares by their coordinates with (0,0) being
 the upper left hand corner and (n,n) being the diagonally opposite
 square.  Thus, there are n+1 rows and columns in the board. If n=7, we are
 talking about the usual 8x8 checkerboard with the rows and columns numbered
 from 0 through 7. More generally, when n is odd, the number of rows and 
 columns is even and vice versa. We use [0..m, 0..n] as  our notation for
 a  board whose rows are numbered from 0 through m and whose 
 columns are numbered from 0 through n.


\noindent{\sc Event}:   Start with the initial {\bf nqthm} theory.

\addvspace{18pt}

 A square is represented by a pair {\rm{cons}}\,({\it{x\/}}, {\it{y\/}}) where {\it{x\/}} and {\it{y\/}} are its 
 coordinates.

\begin{tabbing}{\sc Definition}:\index{squarep} \\  
{\rm{squarep}}\,({\it{x\/}})\index{squarep} $=$ ({\rm{listp}}\,({\it{x\/}}) $\wedge$ ({\rm{car}}\,({\it{x\/}}) $\in\;${\bf{N}}${}$) $\wedge$ ({\rm{cdr}}\,({\it{x\/}}) $\in\;${\bf{N}}${}$))
\end{tabbing}

 A domino is a pair of adjacent squares. 
 Two squares are adjacent if one of their coordinates is the same and the
 other coordinate differs by one. Our predicate is true provided the 
 sum of the coordinates of the first argument is less than that of 
 the second argument. Thus, our definition is asymmetric but this will do:
 there is no loss of generality.


\begin{tabbing}{\sc Definition}:\index{adjp} \\  
\=\+{\rm{adjp}}\,({\it{s1\/}}, {\it{s2\/}})\index{adjp} \\ 
$=$$\;\;\;\;$(\=\+(({\rm{car}}\,({\it{s1\/}}) $=$ {\rm{car}}\,({\it{s2\/}})) $\wedge$ (({\tt{1}} $+$ {\rm{cdr}}\,({\it{s1\/}})) $=$ {\rm{cdr}}\,({\it{s2\/}}))) \\ 
$\vee$$\;\;\;\;$(({\rm{cdr}}\,({\it{s1\/}}) $=$ {\rm{cdr}}\,({\it{s2\/}})) $\wedge$ (({\tt{1}} $+$ {\rm{car}}\,({\it{s1\/}})) $=$ {\rm{car}}\,({\it{s2\/}}))))\-\-
\end{tabbing}

 A square {\it{x\/}} in a [0..n,0..n] board is a pair of coordinates each 
 less than or equal to n.

\begin{tabbing}{\sc Definition}:\index{squarenp} \\  
{\rm{squarenp}}\,({\it{x\/}}, {\it{n\/}})\index{squarenp} $=$ ({\rm{squarep}}\,({\it{x\/}})\index{squarep} $\wedge$ ({\rm{car}}\,({\it{x\/}}) $\leq$ {\it{n\/}}) $\wedge$ ({\rm{cdr}}\,({\it{x\/}}) $\leq$ {\it{n\/}}))
\end{tabbing}

 Dominoes are adjacent pairs of squares that fall within the board.

\begin{tabbing}{\sc Definition}:\index{dominop} \\  
\=\+{\rm{dominop}}\,({\it{x\/}}, {\it{n\/}})\index{dominop} \\ 
$=$$\;\;\;\;$({\rm{squarenp}}\,({\rm{car}}\,({\it{x\/}}), {\it{n\/}})\index{squarenp} $\wedge$ {\rm{squarenp}}\,({\rm{cdr}}\,({\it{x\/}}), {\it{n\/}})\index{squarenp} $\wedge$ {\rm{adjp}}\,({\rm{car}}\,({\it{x\/}}), {\rm{cdr}}\,({\it{x\/}}))\index{adjp})\-
\end{tabbing}

 Square-listp recognizes a list of squares.

\begin{tabbing}{\sc Definition}:\index{square-listp} \\  
\=\+{\rm{square-listp}}\,({\it{x\/}})\index{square-listp} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{x\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }{\rm{squarep}}\,({\rm{car}}\,({\it{x\/}}))\index{squarep} $\wedge$ {\rm{square-listp}}\,({\rm{cdr}}\,({\it{x\/}}))\index{square-listp}$\;${\bf  endif}\-\-
\end{tabbing}


 A board state is a list of covered squares.

\begin{tabbing}{\sc Definition}:\index{board-statep}$\;\;$
{\rm{board-statep}}\,({\it{x\/}})\index{board-statep} $=$ {\rm{square-listp}}\,({\it{x\/}})\index{square-listp}
\end{tabbing}

 Having modeled all possible states of all possible checkerboards
 let us move on to actions.
 There is exactly one action: place a domino with the
 preconditions that the squares of the domino should not be already covered.
 We don't have to check if the dominoes fall within the board because the
 dominop definition takes care of it. 

 The state got as a result of placing a domino {\it{x\/}} on a board in state {\it{s\/}} 
 is given by the following function. If the preconditions of the action
 are not satisfied then it returns a non-board-statep whose car 
 is {\tt{'}}{\tt{failed}}.
 This ``error'' state
 is returned  when other actions are performed on it. Thus, a legal domino
 placement action is one that results in a board state.

\begin{tabbing}{\sc Definition}:\index{res-place} \\  
\=\+{\rm{res-place}}\,({\it{x\/}}, {\it{s\/}})\index{res-place} \\ 
$=$$\;\;\;\;$\=\+{\bf if }({\rm{car}}\,({\it{x\/}}) $\in$ {\it{s\/}}) $\vee$ ({\rm{cdr}}\,({\it{x\/}}) $\in$ {\it{s\/}}) \\ 
{\bf then }{\rm{list}}\,({\tt{'}}{\tt{failed}}, {\tt{'}}{\tt{place}}, {\it{x\/}}, {\it{s\/}}) \\ 
{\bf else }{\rm{cons}}\,({\rm{car}}\,({\it{x\/}}), {\rm{cons}}\,({\rm{cdr}}\,({\it{x\/}}), {\it{s\/}}))$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{result} \\  
\=\+{\rm{result}}\,({\it{a\/}}, {\it{s\/}})\index{result} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{car}}\,({\it{s\/}}) $=$ {\tt{'}}{\tt{failed}}$\;\;${\bf then }{\it{s\/}} \\ 
{\bf else }{\rm{res-place}}\,({\rm{cadr}}\,({\it{a\/}}), {\it{s\/}})\index{res-place}$\;${\bf  endif}\-\-
\end{tabbing}

 The state got from {\it{s\/}} as a result of executing a list of 
 actions {\it{l\/}} is given 
 by the following function.

\begin{tabbing}{\sc Definition}:\index{resultlist} \\  
\=\+{\rm{resultlist}}\,({\it{l\/}}, {\it{s\/}})\index{resultlist} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{l\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\it{s\/}} \\ 
{\bf else }{\rm{resultlist}}\,({\rm{cdr}}\,({\it{l\/}}), {\rm{result}}\,({\rm{car}}\,({\it{l\/}}), {\it{s\/}})\index{result})\index{resultlist}$\;${\bf  endif}\-\-
\end{tabbing}

 A constructor for the action is given below.

\begin{tabbing}{\sc Definition}:\index{place}$\;\;$
{\rm{place}}\,({\it{x\/}})\index{place} $=$ {\rm{list}}\,({\tt{'}}{\tt{place}}, {\it{x\/}})
\end{tabbing}

 The following are predicates on domino-placement actions and 
 sequences of them.

\begin{tabbing}{\sc Definition}:\index{placep}$\;\;$
{\rm{placep}}\,({\it{x\/}}, {\it{n\/}})\index{placep} $=$ {\rm{dominop}}\,({\rm{cadr}}\,({\it{x\/}}), {\it{n\/}})\index{dominop}
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{place-planp} \\  
\=\+{\rm{place-planp}}\,({\it{x\/}}, {\it{n\/}})\index{place-planp} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{x\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }{\rm{placep}}\,({\rm{car}}\,({\it{x\/}}), {\it{n\/}})\index{placep} $\wedge$ {\rm{place-planp}}\,({\rm{cdr}}\,({\it{x\/}}), {\it{n\/}})\index{place-planp}$\;${\bf  endif}\-\-
\end{tabbing}

 To express the theorem, we need a predicate on states in which all squares
 except the corner squares (0,0) and (n,n) are covered.
 We write functions to generate the set of all squares on the board and then
 delete the two corner squares from the set.

 Make-row constructs the set of all squares in the row numbered {\it{m\/}} from 
 columns {\tt{0}} through {\it{n\/}}.

\begin{tabbing}{\sc Definition}:\index{make-row} \\  
\=\+{\rm{make-row}}\,({\it{m\/}}, {\it{n\/}})\index{make-row} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{n\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\rm{list}}\,({\rm{cons}}\,({\it{m\/}}, {\tt{0}})) \\ 
{\bf else }{\rm{append}}\,({\rm{make-row}}\,({\it{m\/}}, {\it{n\/}} $-\;1$)\index{make-row}, {\rm{list}}\,({\rm{cons}}\,({\it{m\/}}, {\it{n\/}})))$\;${\bf  endif}\-\-
\end{tabbing}

 Make-all-rows constructs the set of squares in rows {\tt{0}} through {\it{m\/}} and 
 columns {\tt{0}} through {\it{n\/}}.

\begin{tabbing}{\sc Definition}:\index{make-all-rows} \\  
\=\+{\rm{make-all-rows}}\,({\it{m\/}}, {\it{n\/}})\index{make-all-rows} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{m\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\rm{make-row}}\,({\tt{0}}, {\it{n\/}})\index{make-row} \\ 
{\bf else }{\rm{append}}\,({\rm{make-all-rows}}\,({\it{m\/}} $-\;1$, {\it{n\/}})\index{make-all-rows}, {\rm{make-row}}\,({\it{m\/}}, {\it{n\/}})\index{make-row})$\;${\bf  endif}\-\-
\end{tabbing}

 The following function deletes the first occurrence of {\it{x\/}} in {\it{l\/}}.

\begin{tabbing}{\sc Definition}:\index{delete} \\  
\=\+{\rm{delete}}\,({\it{x\/}}, {\it{l\/}})\index{delete} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{l\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\it{l\/}} \\ 
{\bf elseif }{\it{x\/}} $=$ {\rm{car}}\,({\it{l\/}})$\;\;${\bf then }{\rm{cdr}}\,({\it{l\/}}) \\ 
{\bf else }{\rm{cons}}\,({\rm{car}}\,({\it{l\/}}), {\rm{delete}}\,({\it{x\/}}, {\rm{cdr}}\,({\it{l\/}}))\index{delete})$\;${\bf  endif}\-\-
\end{tabbing}

 A mutilated [0..n,0..n] board includes all squares in rows 
 0 through {\it{n\/}} except the squares {\tt{'}}{\tt{(}}{\tt{0}}{\tt{ .\ }}{\tt{0}}{\tt{)}} and {\rm{cons}}\,({\it{n\/}}, {\it{n\/}}).

\begin{tabbing}{\sc Definition}:\index{mutilated-board} \\  
\=\+{\rm{mutilated-board}}\,({\it{n\/}})\index{mutilated-board} \\ 
$=$$\;\;\;\;${\rm{delete}}\,({\rm{cons}}\,({\it{n\/}}, {\it{n\/}}), {\rm{delete}}\,({\tt{'}}{\tt{(}}{\tt{0}}{\tt{ .\ }}{\tt{0}}{\tt{)}}, {\rm{make-all-rows}}\,({\it{n\/}}, {\it{n\/}})\index{make-all-rows})\index{delete})\index{delete}\-
\end{tabbing}


\begin{tabbing}{\sc Definition}:\index{set-equal} \\  
\=\+{\rm{set-equal}}\,({\it{l1\/}}, {\it{l2\/}})\index{set-equal} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{l1\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\it{l2\/}} $\simeq\;${{\bf{nil}}}${}$ \\ 
{\bf else }\=\+({\rm{car}}\,({\it{l1\/}}) $\in$ {\it{l2\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{set-equal}}\,({\rm{cdr}}\,({\it{l1\/}}), {\rm{delete}}\,({\rm{car}}\,({\it{l1\/}}), {\it{l2\/}})\index{delete})\index{set-equal}\-$\;${\bf  endif}\-\-
\end{tabbing}

 A state in which all squares of the mutilated [0..n,0..n] board are
 covered is given by the following predicate.

\begin{tabbing}{\sc Definition}:\index{all-covered-except-cornerp} \\  
{\rm{all-covered-except-cornerp}}\,({\it{x\/}}, {\it{n\/}})\index{all-covered-except-cornerp} $=$ {\rm{set-equal}}\,({\it{x\/}}, {\rm{mutilated-board}}\,({\it{n\/}})\index{mutilated-board})\index{set-equal}
\end{tabbing}

 A white square is one whose coordinates add up to an even number. Otherwise
 it is a black square. Predicates on white and black squares are given
 below.

\begin{tabbing}{\sc Definition}:\index{oddp}$\;\;$
{\rm{oddp}}\,({\it{x\/}})\index{oddp} $=$ (({\it{x\/}} ${}${\bf{mod}}${}$ {\tt{2}}) $=$ {\tt{1}})
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{whitep}$\;\;$
{\rm{whitep}}\,({\it{x\/}})\index{whitep} $=$ ((({\rm{car}}\,({\it{x\/}}) $+$ {\rm{cdr}}\,({\it{x\/}})) ${}${\bf{mod}}${}$ {\tt{2}}) $=$ {\tt{0}})
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{blackp}$\;\;$
{\rm{blackp}}\,({\it{x\/}})\index{blackp} $=$ ((({\rm{car}}\,({\it{x\/}}) $+$ {\rm{cdr}}\,({\it{x\/}})) ${}${\bf{mod}}${}$ {\tt{2}}) $=$ {\tt{1}})
\end{tabbing}

 The following functions compute the number of white and black squares
 in a state.

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

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

 THE PROOF.

 What is the impossibility argument? In the desired state the number
 of covered white squares is not equal to number of covered black
 squares.  Every placement operation covers exactly one white square
 and one black square.  Thus, all states reachable starting with a
 state in which there are no dominoes on the board have an equal
 number of covered white and black squares. Ergo the desired state is
 unachievable.


 First we show that {\rm{make-all-rows}}\,({\it{n\/}}, {\it{n\/}})\index{make-all-rows} 
 has an equal number of white and
 black squares when {\it{n\/}} is odd (theorem eq-bw-board1) and 
 that the number of white
 squares = number of black squares + 1 when {\it{n\/}} is even (theorem
 white-one-plus-black2). 
 The lemmas appearing before them were needed for the proofs.

\begin{tabbing}{\sc Theorem}:  add-before-sub1 \\ \index{add-before-sub1}
({\it{x\/}} $\geq$ {\tt{2}}) $\rightarrow$ (($1\;+$ ({\it{x\/}} $-$ {\tt{2}})) $=$ (($1\;+$ {\it{x\/}}) $-$ {\tt{2}}))
\end{tabbing}

 Odd numbers succeed even numbers.

\begin{tabbing}{\sc Theorem}:  odd-succeed-even1 \\ \index{odd-succeed-even1}
(({\it{n\/}} ${}${\bf{mod}}${}$ {\tt{2}}) $=$ {\tt{0}}) $\rightarrow$ ((($1\;+$ {\it{n\/}}) ${}${\bf{mod}}${}$ {\tt{2}}) $=$ {\tt{1}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  move-1-out \\ \index{move-1-out}
({\it{m\/}} $+$ ($1\;+$ {\it{n\/}})) $=$ ($1\;+$ ({\it{m\/}} $+$ {\it{n\/}}))
\end{tabbing}

 If a square is white then the next square is black.

\begin{tabbing}{\sc Theorem}:  black-follows-white1 \\ \index{black-follows-white1}
{\rm{whitep}}\,({\rm{cons}}\,({\it{m\/}}, {\it{n\/}}))\index{whitep} $\rightarrow$ {\rm{blackp}}\,({\rm{cons}}\,({\it{m\/}}, $1\;+$ {\it{n\/}}))\index{blackp}
\end{tabbing}	     

 Even numbers succeed odd numbers.

\begin{tabbing}{\sc Theorem}:  even-succeed-odd1 \\ \index{even-succeed-odd1}
(({\it{n\/}} ${}${\bf{mod}}${}$ {\tt{2}}) $=$ {\tt{1}}) $\rightarrow$ ((($1\;+$ {\it{n\/}}) ${}${\bf{mod}}${}$ {\tt{2}}) $=$ {\tt{0}})
\end{tabbing}

 The square next to a  black square is white.

\begin{tabbing}{\sc Theorem}:  white-follows-black1 \\ \index{white-follows-black1}
{\rm{blackp}}\,({\rm{cons}}\,({\it{m\/}}, {\it{n\/}}))\index{blackp} $\rightarrow$ {\rm{whitep}}\,({\rm{cons}}\,({\it{m\/}}, $1\;+$ {\it{n\/}}))\index{whitep}
\end{tabbing}


\begin{tabbing}{\sc Theorem}:  odd-even1 \\ \index{odd-even1}
(({\it{n\/}} ${}${\bf{mod}}${}$ {\tt{2}}) $\not=$ {\tt{0}}) $\rightarrow$ (({\it{n\/}} ${}${\bf{mod}}${}$ {\tt{2}}) $=$ {\tt{1}})
\end{tabbing}

 The following is the base case of the lemma that the number of 
 white squares  equals the number of black
 squares in a row with an even number of squares.

\begin{tabbing}{\sc Theorem}:  expand-make-row1 \\ \index{expand-make-row1}
{\rm{make-row}}\,({\it{m\/}}, {\tt{1}})\index{make-row} $=$ {\rm{list}}\,({\rm{cons}}\,({\it{m\/}}, {\tt{0}}), {\rm{cons}}\,({\it{m\/}}, {\tt{1}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  equal-bw-row-base0 \\ \index{equal-bw-row-base0}
{\rm{nwhite}}\,({\rm{make-row}}\,({\it{m\/}}, {\tt{1}})\index{make-row})\index{nwhite} $=$ {\rm{nblack}}\,({\rm{make-row}}\,({\it{m\/}}, {\tt{1}})\index{make-row})\index{nblack}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  t5 \\ \index{t5}
(({\it{y\/}} ${}${\bf{mod}}${}$ {\tt{2}}) $\not=$ {\tt{1}}) $\rightarrow$ ((($1\;+$ {\it{y\/}}) ${}${\bf{mod}}${}$ {\tt{2}}) $=$ {\tt{1}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  append-assoc \\ \index{append-assoc}
{\rm{append}}\,({\rm{append}}\,({\it{l1\/}}, {\it{l2\/}}), {\it{l3\/}}) $=$ {\rm{append}}\,({\it{l1\/}}, {\rm{append}}\,({\it{l2\/}}, {\it{l3\/}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  t6 \\ \index{t6}
\=\+({\it{n\/}} $\geq$ {\tt{2}}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{make-row}}\,({\it{m\/}}, {\it{n\/}})\index{make-row} \\ 
$=$$\;\;\;\;${\rm{append}}\,({\rm{make-row}}\,({\it{m\/}}, {\it{n\/}} $-$ {\tt{2}})\index{make-row}, {\rm{list}}\,({\rm{cons}}\,({\it{m\/}}, {\it{n\/}} $-\;1$), {\rm{cons}}\,({\it{m\/}}, {\it{n\/}}))))\-\-
\end{tabbing}

 The number of white/black squares obtained on appending two lists is the
 sum of the number of white/black squares of the individual lists.

\begin{tabbing}{\sc Theorem}:  nwhite-append1 \\ \index{nwhite-append1}
{\rm{nwhite}}\,({\rm{append}}\,({\it{l1\/}}, {\it{l2\/}}))\index{nwhite} $=$ ({\rm{nwhite}}\,({\it{l1\/}})\index{nwhite} $+$ {\rm{nwhite}}\,({\it{l2\/}})\index{nwhite})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  nblack-append1 \\ \index{nblack-append1}
{\rm{nblack}}\,({\rm{append}}\,({\it{l1\/}}, {\it{l2\/}}))\index{nblack} $=$ ({\rm{nblack}}\,({\it{l1\/}})\index{nblack} $+$ {\rm{nblack}}\,({\it{l2\/}})\index{nblack})
\end{tabbing}


 In each row of a chess board [0..m,0..n] where n is odd, the number
 of black squares is equal to the number of white squares.

\begin{tabbing}{\sc Theorem}:  equal-bw-row1 \\ \index{equal-bw-row1}
{\rm{oddp}}\,({\it{n\/}})\index{oddp} $\rightarrow$ ({\rm{nwhite}}\,({\rm{make-row}}\,({\it{m\/}}, {\it{n\/}})\index{make-row})\index{nwhite} $=$ {\rm{nblack}}\,({\rm{make-row}}\,({\it{m\/}}, {\it{n\/}})\index{make-row})\index{nblack})
\end{tabbing}


 In an entire [0..m,0..n] board, n odd, 
 there are an equal number of white and black squares.

\begin{tabbing}{\sc Theorem}:  eq-bw-board1 \\ \index{eq-bw-board1}
{\rm{oddp}}\,({\it{n\/}})\index{oddp} $\rightarrow$ ({\rm{nwhite}}\,({\rm{make-all-rows}}\,({\it{m\/}}, {\it{n\/}})\index{make-all-rows})\index{nwhite} $=$ {\rm{nblack}}\,({\rm{make-all-rows}}\,({\it{m\/}}, {\it{n\/}})\index{make-all-rows})\index{nblack})
\end{tabbing}

 Instantiating {\it{m\/}} as {\it{n\/}} in the above we get the following.

\begin{tabbing}{\sc Theorem}:  eq-bw-board \\ \index{eq-bw-board}
{\rm{oddp}}\,({\it{n\/}})\index{oddp} $\rightarrow$ ({\rm{nwhite}}\,({\rm{make-all-rows}}\,({\it{n\/}}, {\it{n\/}})\index{make-all-rows})\index{nwhite} $=$ {\rm{nblack}}\,({\rm{make-all-rows}}\,({\it{n\/}}, {\it{n\/}})\index{make-all-rows})\index{nblack})
\end{tabbing}

 Now we prove that the number of white
 squares = number of black squares + 1 in a board with an odd number of
 rows and columns (theorem white-one-plus-black2). The following are
 intermediate lemmas needed for the proof.
 

\begin{tabbing}{\sc Definition}:\index{evenp}$\;\;$
{\rm{evenp}}\,({\it{x\/}})\index{evenp} $=$ (({\it{x\/}} ${}${\bf{mod}}${}$ {\tt{2}}) $=$ {\tt{0}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  zero-ident \\ \index{zero-ident}
({\it{m\/}} $+$ {\tt{0}}) $=$ {\rm{fix}}\,({\it{m\/}})
\end{tabbing}

 The number of white squares of an even numbered row with an odd number
 of columns is equal to the number of black squares + 1.

\begin{tabbing}{\sc Theorem}:  white-one-plus-black \\ \index{white-one-plus-black}
\=\+({\rm{evenp}}\,({\it{m\/}})\index{evenp} $\wedge$ {\rm{evenp}}\,({\it{n\/}})\index{evenp}) \\ 
$\rightarrow$$\;\;\;\;$({\rm{nwhite}}\,({\rm{make-row}}\,({\it{m\/}}, {\it{n\/}})\index{make-row})\index{nwhite} $=$ ($1\;+$ {\rm{nblack}}\,({\rm{make-row}}\,({\it{m\/}}, {\it{n\/}})\index{make-row})\index{nblack}))\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  black-one-plus-white \\ \index{black-one-plus-white}
\=\+({\rm{oddp}}\,({\it{m\/}})\index{oddp} $\wedge$ {\rm{evenp}}\,({\it{n\/}})\index{evenp}) \\ 
$\rightarrow$$\;\;\;\;$({\rm{nblack}}\,({\rm{make-row}}\,({\it{m\/}}, {\it{n\/}})\index{make-row})\index{nblack} $=$ ($1\;+$ {\rm{nwhite}}\,({\rm{make-row}}\,({\it{m\/}}, {\it{n\/}})\index{make-row})\index{nwhite}))\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  l13 \\ \index{l13}
{\rm{make-all-rows}}\,({\tt{1}}, {\it{n\/}})\index{make-all-rows} $=$ {\rm{append}}\,({\rm{make-row}}\,({\tt{0}}, {\it{n\/}})\index{make-row}, {\rm{make-row}}\,({\tt{1}}, {\it{n\/}})\index{make-row})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  l14 \\ \index{l14}
{\rm{evenp}}\,({\it{n\/}})\index{evenp} $\rightarrow$ ({\rm{nwhite}}\,({\rm{make-all-rows}}\,({\tt{1}}, {\it{n\/}})\index{make-all-rows})\index{nwhite} $=$ {\rm{nblack}}\,({\rm{make-all-rows}}\,({\tt{1}}, {\it{n\/}})\index{make-all-rows})\index{nblack})
\end{tabbing}


\begin{tabbing}{\sc Theorem}:  base2 \\ \index{base2}
\=\+({\rm{nwhite}}\,({\rm{make-row}}\,({\tt{0}}, {\it{n\/}})\index{make-row})\index{nwhite} $+$ {\rm{nwhite}}\,({\rm{make-row}}\,({\tt{1}}, {\it{n\/}})\index{make-row})\index{nwhite}) \\ 
$=$$\;\;\;\;$({\rm{nblack}}\,({\rm{make-row}}\,({\tt{0}}, {\it{n\/}})\index{make-row})\index{nblack} $+$ {\rm{nblack}}\,({\rm{make-row}}\,({\tt{1}}, {\it{n\/}})\index{make-row})\index{nblack})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  l15 \\ \index{l15}
\=\+({\it{m\/}} $>$ {\tt{0}}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{nwhite}}\,({\rm{make-row}}\,({\it{m\/}} $-\;1$, {\it{n\/}})\index{make-row})\index{nwhite} $+$ {\rm{nwhite}}\,({\rm{make-row}}\,({\it{m\/}}, {\it{n\/}})\index{make-row})\index{nwhite}) \\ 
$=$$\;\;\;\;$({\rm{nblack}}\,({\rm{make-row}}\,({\it{m\/}} $-\;1$, {\it{n\/}})\index{make-row})\index{nblack} $+$ {\rm{nblack}}\,({\rm{make-row}}\,({\it{m\/}}, {\it{n\/}})\index{make-row})\index{nblack}))\-\-
\end{tabbing}


\begin{tabbing}{\sc Theorem}:  t61 \\ \index{t61}
\=\+({\it{m\/}} $\geq$ {\tt{2}}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{make-all-rows}}\,({\it{m\/}}, {\it{n\/}})\index{make-all-rows} \\ 
$=$$\;\;\;\;${\rm{append}}\,(\=\+{\rm{make-all-rows}}\,({\it{m\/}} $-$ {\tt{2}}, {\it{n\/}})\index{make-all-rows}, \\ 
{\rm{append}}\,({\rm{make-row}}\,({\it{m\/}} $-\;1$, {\it{n\/}})\index{make-row}, {\rm{make-row}}\,({\it{m\/}}, {\it{n\/}})\index{make-row}))\-)\-\-
\end{tabbing}


\begin{tabbing}{\sc Theorem}:  l16 \\ \index{l16}
\=\+(({\it{x1\/}} $+$ {\it{y1\/}} $+$ {\it{z1\/}}) $=$ ({\it{x1\/}} $+$ {\it{y2\/}} $+$ {\it{z2\/}})) \\ 
$=$$\;\;\;\;$(({\it{y1\/}} $+$ {\it{z1\/}}) $=$ ({\it{y2\/}} $+$ {\it{z2\/}}))\-
\end{tabbing}

 In a [0..m,0..n] checkerboard in which {\it{m\/}} is odd, the number of
 black squares is equal to the number of white squares.

\begin{tabbing}{\sc Theorem}:  eq-bw-board2 \\ \index{eq-bw-board2}
{\rm{oddp}}\,({\it{m\/}})\index{oddp} $\rightarrow$ ({\rm{nwhite}}\,({\rm{make-all-rows}}\,({\it{m\/}}, {\it{n\/}})\index{make-all-rows})\index{nwhite} $=$ {\rm{nblack}}\,({\rm{make-all-rows}}\,({\it{m\/}}, {\it{n\/}})\index{make-all-rows})\index{nblack})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  l17 \\ \index{l17}
({\rm{evenp}}\,({\it{m\/}})\index{evenp} $\wedge$ ({\it{m\/}} $>$ {\tt{0}})) $\rightarrow$ ((({\it{m\/}} $-\;1$) ${}${\bf{mod}}${}$ {\tt{2}}) $=$ {\tt{1}})
\end{tabbing}

 The following function is introduced to force Nqthm
 to chose the appropriate induction scheme for theorem white-one-plus-black2.
 A hint to induct on {\it{m\/}} according to the recursive structure of f1
 was given.

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

 If the number of rows and columns of a checkerboard is odd then
 the number of white squares in the board is 1 greater than the number of
 black squares.

\begin{tabbing}{\sc Theorem}:  white-one-plus-black2 \\ \index{white-one-plus-black2}
\=\+({\rm{evenp}}\,({\it{m\/}})\index{evenp} $\wedge$ {\rm{evenp}}\,({\it{n\/}})\index{evenp}) \\ 
$\rightarrow$$\;\;\;\;$({\rm{nwhite}}\,({\rm{make-all-rows}}\,({\it{m\/}}, {\it{n\/}})\index{make-all-rows})\index{nwhite} $=$ ($1\;+$ {\rm{nblack}}\,({\rm{make-all-rows}}\,({\it{m\/}}, {\it{n\/}})\index{make-all-rows})\index{nblack}))\-
\end{tabbing}


 Having established that the number of white squares is equal to the
 number of black squares in a board with an even number of rows and columns
 and that the number of white squares is 1 greater than the number of black
 squares in a board with an odd number of rows and columns, we would
 like to show that in a mutilated board the number of white squares
 is less than the number of black squares.
 This is proved as theorem mut3 below. The lemmas preceding it are
 intermediate lemmas needed for the proof.

\begin{tabbing}{\sc Theorem}:  t7 \\ \index{t7}
({\it{n\/}} $\in\;${\bf{N}}${}$) $\rightarrow$ ({\rm{cons}}\,({\it{m\/}}, {\it{n\/}}) $\in$ {\rm{make-row}}\,({\it{m\/}}, {\it{n\/}})\index{make-row})
\end{tabbing}   


\begin{tabbing}{\sc Theorem}:  t8 \\ \index{t8}
({\it{x\/}} $\in$ {\it{l2\/}}) $\rightarrow$ ({\it{x\/}} $\in$ {\rm{append}}\,({\it{l1\/}}, {\it{l2\/}}))
\end{tabbing}


\begin{tabbing}{\sc Theorem}:  m1 \\ \index{m1}
(({\it{n\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{m\/}} $\in\;${\bf{N}}${}$)) $\rightarrow$ ({\rm{cons}}\,({\it{m\/}}, {\it{n\/}}) $\in$ {\rm{make-all-rows}}\,({\it{m\/}}, {\it{n\/}})\index{make-all-rows})
\end{tabbing}

 If we delete a white square from a list then the number of white squares
 in the new list is less than that in the old list.

\begin{tabbing}{\sc Theorem}:  white-delete \\ \index{white-delete}
(({\it{x\/}} $\in$ {\it{l\/}}) $\wedge$ {\rm{whitep}}\,({\it{x\/}})\index{whitep}) $\rightarrow$ ({\rm{nwhite}}\,({\rm{delete}}\,({\it{x\/}}, {\it{l\/}})\index{delete})\index{nwhite} $<$ {\rm{nwhite}}\,({\it{l\/}})\index{nwhite})
\end{tabbing}

 The (n,n) square is white.

\begin{tabbing}{\sc Theorem}:  white1 \\ \index{white1}
{\rm{whitep}}\,({\rm{cons}}\,({\it{n\/}}, {\it{n\/}}))\index{whitep}
\end{tabbing}

 Deleting a white square does not change the number of black squares.

\begin{tabbing}{\sc Theorem}:  black-same1 \\ \index{black-same1}
{\rm{whitep}}\,({\it{x\/}})\index{whitep} $\rightarrow$ ({\rm{nblack}}\,({\rm{delete}}\,({\it{x\/}}, {\it{l\/}})\index{delete})\index{nblack} $=$ {\rm{nblack}}\,({\it{l\/}})\index{nblack})
\end{tabbing}

 Deleting {\tt{'}}{\tt{(}}{\tt{0}} {\tt{.\ }}{\tt{0}}{\tt{)}} and {\rm{cons}}\,({\it{n\/}}, {\it{n\/}}) does not change the number of black
 squares in a list since both of them are white.

\begin{tabbing}{\sc Theorem}:  black-del1 \\ \index{black-del1}
{\rm{nblack}}\,({\rm{delete}}\,({\rm{cons}}\,({\it{n\/}}, {\it{n\/}}), {\rm{delete}}\,({\tt{'}}{\tt{(}}{\tt{0}}{\tt{ .\ }}{\tt{0}}{\tt{)}}, {\it{x\/}})\index{delete})\index{delete})\index{nblack} $=$ {\rm{nblack}}\,({\it{x\/}})\index{nblack}
\end{tabbing}


\begin{tabbing}{\sc Theorem}:  mut-l2 \\ \index{mut-l2}
{\rm{oddp}}\,({\it{n\/}})\index{oddp} $\rightarrow$ ({\it{n\/}} $\not=$ {\tt{0}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  mem-del1 \\ \index{mem-del1}
(({\it{x\/}} $\in$ {\it{l\/}}) $\wedge$ ({\it{x\/}} $\not=$ {\it{y\/}})) $\rightarrow$ ({\it{x\/}} $\in$ {\rm{delete}}\,({\it{y\/}}, {\it{l\/}})\index{delete})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  m2 \\ \index{m2}
{\tt{'}}{\tt{(}}{\tt{0}}{\tt{ .\ }}{\tt{0}}{\tt{)}} $\in$ {\rm{make-all-rows}}\,({\it{m\/}}, {\it{n\/}})\index{make-all-rows}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  mut-l1 \\ \index{mut-l1}
{\rm{oddp}}\,({\it{n\/}})\index{oddp} $\rightarrow$ ({\rm{cons}}\,({\it{n\/}}, {\it{n\/}}) $\in$ {\rm{delete}}\,({\tt{'}}{\tt{(}}{\tt{0}}{\tt{ .\ }}{\tt{0}}{\tt{)}}, {\rm{make-all-rows}}\,({\it{n\/}}, {\it{n\/}})\index{make-all-rows})\index{delete})
\end{tabbing}



 In a mutilated board with an even number of rows and
 columns the number of white squares is less than the number of black
 squares.

\begin{tabbing}{\sc Theorem}:  mut1 \\ \index{mut1}
({\rm{oddp}}\,({\it{n\/}})\index{oddp} $\wedge$ ({\it{x\/}} $=$ {\rm{mutilated-board}}\,({\it{n\/}})\index{mutilated-board})) $\rightarrow$ ({\rm{nwhite}}\,({\it{x\/}})\index{nwhite} $<$ {\rm{nblack}}\,({\it{x\/}})\index{nblack})
\end{tabbing}

 In a mutilated board with an odd number of rows and columns,
 the number of white squares is less than the number
 of black squares.

\begin{tabbing}{\sc Theorem}:  mut2 \\ \index{mut2}
\=\+({\rm{evenp}}\,({\it{n\/}})\index{evenp} $\wedge$ ({\it{x\/}} $=$ {\rm{mutilated-board}}\,({\it{n\/}})\index{mutilated-board}) $\wedge$ ({\it{n\/}} $>$ {\tt{0}})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{nwhite}}\,({\it{x\/}})\index{nwhite} $<$ {\rm{nblack}}\,({\it{x\/}})\index{nblack})\-
\end{tabbing}

 In any mutilated board the number of white squares is less than the number
 of black squares.

\begin{tabbing}{\sc Theorem}:  mut3 \\ \index{mut3}
(({\it{x\/}} $=$ {\rm{mutilated-board}}\,({\it{n\/}})\index{mutilated-board}) $\wedge$ ({\it{n\/}} $>$ {\tt{0}})) $\rightarrow$ ({\rm{nwhite}}\,({\it{x\/}})\index{nwhite} $<$ {\rm{nblack}}\,({\it{x\/}})\index{nblack})
\end{tabbing}

 The following shows what a mutilated board looks like for n = 7.

\begin{tabbing}{\sc Theorem}:  mutboard7 \\ \index{mutboard7}
\=\+{\rm{mutilated-board}}\,({\tt{7}})\index{mutilated-board} \\ 
$=$$\;\;\;\;${\tt{'}}{\tt{(}}\=\+{\tt{(}}{\tt{0}}{\tt{ .\ }}{\tt{1}}{\tt{)}} \\ 
{\tt{(}}{\tt{0}}{\tt{ .\ }}{\tt{2}}{\tt{)}} \\ 
{\tt{(}}{\tt{0}}{\tt{ .\ }}{\tt{3}}{\tt{)}} \\ 
{\tt{(}}{\tt{0}}{\tt{ .\ }}{\tt{4}}{\tt{)}} \\ 
{\tt{(}}{\tt{0}}{\tt{ .\ }}{\tt{5}}{\tt{)}} \\ 
{\tt{(}}{\tt{0}}{\tt{ .\ }}{\tt{6}}{\tt{)}} \\ 
{\tt{(}}{\tt{0}}{\tt{ .\ }}{\tt{7}}{\tt{)}} \\ 
{\tt{(}}{\tt{1}}{\tt{ .\ }}{\tt{0}}{\tt{)}} \\ 
{\tt{(}}{\tt{1}}{\tt{ .\ }}{\tt{1}}{\tt{)}} \\ 
{\tt{(}}{\tt{1}}{\tt{ .\ }}{\tt{2}}{\tt{)}} \\ 
{\tt{(}}{\tt{1}}{\tt{ .\ }}{\tt{3}}{\tt{)}} \\ 
{\tt{(}}{\tt{1}}{\tt{ .\ }}{\tt{4}}{\tt{)}} \\ 
{\tt{(}}{\tt{1}}{\tt{ .\ }}{\tt{5}}{\tt{)}} \\ 
{\tt{(}}{\tt{1}}{\tt{ .\ }}{\tt{6}}{\tt{)}} \\ 
{\tt{(}}{\tt{1}}{\tt{ .\ }}{\tt{7}}{\tt{)}} \\ 
{\tt{(}}{\tt{2}}{\tt{ .\ }}{\tt{0}}{\tt{)}} \\ 
{\tt{(}}{\tt{2}}{\tt{ .\ }}{\tt{1}}{\tt{)}} \\ 
{\tt{(}}{\tt{2}}{\tt{ .\ }}{\tt{2}}{\tt{)}} \\ 
{\tt{(}}{\tt{2}}{\tt{ .\ }}{\tt{3}}{\tt{)}} \\ 
{\tt{(}}{\tt{2}}{\tt{ .\ }}{\tt{4}}{\tt{)}} \\ 
{\tt{(}}{\tt{2}}{\tt{ .\ }}{\tt{5}}{\tt{)}} \\ 
{\tt{(}}{\tt{2}}{\tt{ .\ }}{\tt{6}}{\tt{)}} \\ 
{\tt{(}}{\tt{2}}{\tt{ .\ }}{\tt{7}}{\tt{)}} \\ 
{\tt{(}}{\tt{3}}{\tt{ .\ }}{\tt{0}}{\tt{)}} \\ 
{\tt{(}}{\tt{3}}{\tt{ .\ }}{\tt{1}}{\tt{)}} \\ 
{\tt{(}}{\tt{3}}{\tt{ .\ }}{\tt{2}}{\tt{)}} \\ 
{\tt{(}}{\tt{3}}{\tt{ .\ }}{\tt{3}}{\tt{)}} \\ 
{\tt{(}}{\tt{3}}{\tt{ .\ }}{\tt{4}}{\tt{)}} \\ 
{\tt{(}}{\tt{3}}{\tt{ .\ }}{\tt{5}}{\tt{)}} \\ 
{\tt{(}}{\tt{3}}{\tt{ .\ }}{\tt{6}}{\tt{)}} \\ 
{\tt{(}}{\tt{3}}{\tt{ .\ }}{\tt{7}}{\tt{)}} \\ 
{\tt{(}}{\tt{4}}{\tt{ .\ }}{\tt{0}}{\tt{)}} \\ 
{\tt{(}}{\tt{4}}{\tt{ .\ }}{\tt{1}}{\tt{)}} \\ 
{\tt{(}}{\tt{4}}{\tt{ .\ }}{\tt{2}}{\tt{)}} \\ 
{\tt{(}}{\tt{4}}{\tt{ .\ }}{\tt{3}}{\tt{)}} \\ 
{\tt{(}}{\tt{4}}{\tt{ .\ }}{\tt{4}}{\tt{)}} \\ 
{\tt{(}}{\tt{4}}{\tt{ .\ }}{\tt{5}}{\tt{)}} \\ 
{\tt{(}}{\tt{4}}{\tt{ .\ }}{\tt{6}}{\tt{)}} \\ 
{\tt{(}}{\tt{4}}{\tt{ .\ }}{\tt{7}}{\tt{)}} \\ 
{\tt{(}}{\tt{5}}{\tt{ .\ }}{\tt{0}}{\tt{)}} \\ 
{\tt{(}}{\tt{5}}{\tt{ .\ }}{\tt{1}}{\tt{)}} \\ 
{\tt{(}}{\tt{5}}{\tt{ .\ }}{\tt{2}}{\tt{)}} \\ 
{\tt{(}}{\tt{5}}{\tt{ .\ }}{\tt{3}}{\tt{)}} \\ 
{\tt{(}}{\tt{5}}{\tt{ .\ }}{\tt{4}}{\tt{)}} \\ 
{\tt{(}}{\tt{5}}{\tt{ .\ }}{\tt{5}}{\tt{)}} \\ 
{\tt{(}}{\tt{5}}{\tt{ .\ }}{\tt{6}}{\tt{)}} \\ 
{\tt{(}}{\tt{5}}{\tt{ .\ }}{\tt{7}}{\tt{)}} \\ 
{\tt{(}}{\tt{6}}{\tt{ .\ }}{\tt{0}}{\tt{)}} \\ 
{\tt{(}}{\tt{6}}{\tt{ .\ }}{\tt{1}}{\tt{)}} \\ 
{\tt{(}}{\tt{6}}{\tt{ .\ }}{\tt{2}}{\tt{)}} \\ 
{\tt{(}}{\tt{6}}{\tt{ .\ }}{\tt{3}}{\tt{)}} \\ 
{\tt{(}}{\tt{6}}{\tt{ .\ }}{\tt{4}}{\tt{)}} \\ 
{\tt{(}}{\tt{6}}{\tt{ .\ }}{\tt{5}}{\tt{)}} \\ 
{\tt{(}}{\tt{6}}{\tt{ .\ }}{\tt{6}}{\tt{)}} \\ 
{\tt{(}}{\tt{6}}{\tt{ .\ }}{\tt{7}}{\tt{)}} \\ 
{\tt{(}}{\tt{7}}{\tt{ .\ }}{\tt{0}}{\tt{)}} \\ 
{\tt{(}}{\tt{7}}{\tt{ .\ }}{\tt{1}}{\tt{)}} \\ 
{\tt{(}}{\tt{7}}{\tt{ .\ }}{\tt{2}}{\tt{)}} \\ 
{\tt{(}}{\tt{7}}{\tt{ .\ }}{\tt{3}}{\tt{)}} \\ 
{\tt{(}}{\tt{7}}{\tt{ .\ }}{\tt{4}}{\tt{)}} \\ 
{\tt{(}}{\tt{7}}{\tt{ .\ }}{\tt{5}}{\tt{)}} \\ 
{\tt{(}}{\tt{7}}{\tt{ .\ }}{\tt{6}}{\tt{)}}{\tt{)}}\-\-
\end{tabbing}

 We will now use mut3 to show that in all states satisfying
 all-covered-except-cornerp the number of white squares is
 less than the number of black squares. This is proved as theorem
 unequal3 below. We need some more lemmas for
 the proof because all-covered-except-cornerp checks for set equality
 by deleting squares in two given lists.

 Deleting a non-white element from a list of white squares does not alter
 the number of white squares.

\begin{tabbing}{\sc Theorem}:  white-same1 \\ \index{white-same1}
($\neg$ {\rm{whitep}}\,({\it{x\/}})\index{whitep}) $\rightarrow$ ({\rm{nwhite}}\,({\rm{delete}}\,({\it{x\/}}, {\it{l\/}})\index{delete})\index{nwhite} $=$ {\rm{nwhite}}\,({\it{l\/}})\index{nwhite})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  white-del1 \\ \index{white-del1}
(({\it{x\/}} $\in$ {\it{l\/}}) $\wedge$ {\rm{whitep}}\,({\it{x\/}})\index{whitep}) $\rightarrow$ ({\rm{nwhite}}\,({\it{l\/}})\index{nwhite} $=$ ({\tt{1}} $+$ {\rm{nwhite}}\,({\rm{delete}}\,({\it{x\/}}, {\it{l\/}})\index{delete})\index{nwhite}))
\end{tabbing}

 If two sets of squares are equal then the number of white/black squares in 
 them are equal.

\begin{tabbing}{\sc Theorem}:  nwhite-eq1 \\ \index{nwhite-eq1}
{\rm{set-equal}}\,({\it{l1\/}}, {\it{l2\/}})\index{set-equal} $\rightarrow$ ({\rm{nwhite}}\,({\it{l1\/}})\index{nwhite} $=$ {\rm{nwhite}}\,({\it{l2\/}})\index{nwhite})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  black-same2 \\ \index{black-same2}
($\neg$ {\rm{blackp}}\,({\it{x\/}})\index{blackp}) $\rightarrow$ ({\rm{nblack}}\,({\rm{delete}}\,({\it{x\/}}, {\it{l\/}})\index{delete})\index{nblack} $=$ {\rm{nblack}}\,({\it{l\/}})\index{nblack})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  black-del2 \\ \index{black-del2}
(({\it{x\/}} $\in$ {\it{l\/}}) $\wedge$ {\rm{blackp}}\,({\it{x\/}})\index{blackp}) $\rightarrow$ ({\rm{nblack}}\,({\it{l\/}})\index{nblack} $=$ ({\tt{1}} $+$ {\rm{nblack}}\,({\rm{delete}}\,({\it{x\/}}, {\it{l\/}})\index{delete})\index{nblack}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  nblack-eq1 \\ \index{nblack-eq1}
{\rm{set-equal}}\,({\it{l1\/}}, {\it{l2\/}})\index{set-equal} $\rightarrow$ ({\rm{nblack}}\,({\it{l1\/}})\index{nblack} $=$ {\rm{nblack}}\,({\it{l2\/}})\index{nblack})
\end{tabbing}


 If all the squares except the corner ones are covered in a board state
 then the number of white squares covered is less than the number of
 covered black squares.

\begin{tabbing}{\sc Theorem}:  unequal1 \\ \index{unequal1}
\=\+(\=\+{\rm{evenp}}\,({\it{n\/}})\index{evenp} \\ 
$\wedge$$\;\;\;\;$({\it{n\/}} $>$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;${\rm{board-statep}}\,({\it{x\/}})\index{board-statep} \\ 
$\wedge$$\;\;\;\;${\rm{all-covered-except-cornerp}}\,({\it{x\/}}, {\it{n\/}})\index{all-covered-except-cornerp})\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{nwhite}}\,({\it{x\/}})\index{nwhite} $<$ {\rm{nblack}}\,({\it{x\/}})\index{nblack})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  unequal2 \\ \index{unequal2}
\=\+({\rm{oddp}}\,({\it{n\/}})\index{oddp} $\wedge$ {\rm{board-statep}}\,({\it{x\/}})\index{board-statep} $\wedge$ {\rm{all-covered-except-cornerp}}\,({\it{x\/}}, {\it{n\/}})\index{all-covered-except-cornerp}) \\ 
$\rightarrow$$\;\;\;\;$({\rm{nwhite}}\,({\it{x\/}})\index{nwhite} $<$ {\rm{nblack}}\,({\it{x\/}})\index{nblack})\-
\end{tabbing}


\begin{tabbing}{\sc Theorem}:  unequal3 \\ \index{unequal3}
\=\+(({\it{n\/}} $>$ {\tt{0}}) $\wedge$ {\rm{board-statep}}\,({\it{x\/}})\index{board-statep} $\wedge$ {\rm{all-covered-except-cornerp}}\,({\it{x\/}}, {\it{n\/}})\index{all-covered-except-cornerp}) \\ 
$\rightarrow$$\;\;\;\;$({\rm{nwhite}}\,({\it{x\/}})\index{nwhite} $<$ {\rm{nblack}}\,({\it{x\/}})\index{nblack})\-
\end{tabbing}


 Now we want to show that the number of covered white squares is equal to
 the number of covered black squares in every state that arises starting
 with an initial state when there are no dominoes on the board.
 This is proved as theorem bcequal1. This in turn uses theorem bw-equal2
 which says that the number of covered black and white squares remain
 equal when a domino is placed on a board legally. 

 First we need some more number theory: If the sum of two numbers is 
 even then 
 adding one to one of the
 numbers will make the sum odd and vice versa.

\begin{tabbing}{\sc Theorem}:  t10 \\ \index{t10}
(({\tt{1}} $+$ {\it{w\/}}) $+$ {\it{z\/}}) $=$ ($1\;+$ ({\it{w\/}} $+$ {\it{z\/}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  t11 \\ \index{t11}
({\it{x\/}} $+$ {\tt{1}} $+$ {\it{y\/}}) $=$ ($1\;+$ ({\it{x\/}} $+$ {\it{y\/}}))
\end{tabbing}


 A domino covers exactly one white square and one black square.

\begin{tabbing}{\sc Theorem}:  domino-white1 \\ \index{domino-white1}
\=\+{\rm{dominop}}\,({\it{x\/}}, {\it{n\/}})\index{dominop} \\ 
$\rightarrow$$\;\;\;\;$({\rm{nwhite}}\,({\rm{cons}}\,({\rm{car}}\,({\it{x\/}}), {\rm{cons}}\,({\rm{cdr}}\,({\it{x\/}}), {\it{y\/}})))\index{nwhite} $=$ ({\tt{1}} $+$ {\rm{nwhite}}\,({\it{y\/}})\index{nwhite}))\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  domino-black1 \\ \index{domino-black1}
\=\+{\rm{dominop}}\,({\it{x\/}}, {\it{n\/}})\index{dominop} \\ 
$\rightarrow$$\;\;\;\;$({\rm{nblack}}\,({\rm{cons}}\,({\rm{car}}\,({\it{x\/}}), {\rm{cons}}\,({\rm{cdr}}\,({\it{x\/}}), {\it{y\/}})))\index{nblack} $=$ ({\tt{1}} $+$ {\rm{nblack}}\,({\it{y\/}})\index{nblack}))\-
\end{tabbing}

 If a domino is placed on a board then the new
 board state will have the two squares under the domino covered.

\begin{tabbing}{\sc Theorem}:  place-dom1 \\ \index{place-dom1}
\=\+({\rm{board-statep}}\,({\it{s\/}})\index{board-statep} $\wedge$ {\rm{placep}}\,({\it{a\/}}, {\it{n\/}})\index{placep} $\wedge$ {\rm{board-statep}}\,({\rm{result}}\,({\it{a\/}}, {\it{s\/}})\index{result})\index{board-statep}) \\ 
$\rightarrow$$\;\;\;\;$({\rm{result}}\,({\it{a\/}}, {\it{s\/}})\index{result} $=$ {\rm{cons}}\,({\rm{caadr}}\,({\it{a\/}}), {\rm{cons}}\,({\rm{cdadr}}\,({\it{a\/}}), {\it{s\/}})))\-
\end{tabbing}


 If the number of covered black and white squares in a state are
 equal then they remain the same after a legal domino placement.

\begin{tabbing}{\sc Theorem}:  bw-equal2 \\ \index{bw-equal2}
\=\+(\=\+{\rm{board-statep}}\,({\it{s\/}})\index{board-statep} \\ 
$\wedge$$\;\;\;\;$({\rm{nwhite}}\,({\it{s\/}})\index{nwhite} $=$ {\rm{nblack}}\,({\it{s\/}})\index{nblack}) \\ 
$\wedge$$\;\;\;\;${\rm{placep}}\,({\it{a\/}}, {\it{n\/}})\index{placep} \\ 
$\wedge$$\;\;\;\;${\rm{board-statep}}\,({\rm{result}}\,({\it{a\/}}, {\it{s\/}})\index{result})\index{board-statep})\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{nwhite}}\,({\rm{result}}\,({\it{a\/}}, {\it{s\/}})\index{result})\index{nwhite} $=$ {\rm{nblack}}\,({\rm{result}}\,({\it{a\/}}, {\it{s\/}})\index{result})\index{nblack})\-
\end{tabbing}


 The following lemmas are need to show that if
 the number of covered white and black squares are equal in a state 
 then they will
 remain equal after every legal sequence of domino-placement actions.

 First we  prove that executing an action sequence in an error state 
 results in the error state.

\begin{tabbing}{\sc Theorem}:  failed-state1 \\ \index{failed-state1}
({\rm{car}}\,({\it{s\/}}) $=$ {\tt{'}}{\tt{failed}}) $\rightarrow$ ({\rm{car}}\,({\rm{resultlist}}\,({\it{p\/}}, {\it{s\/}})\index{resultlist}) $=$ {\tt{'}}{\tt{failed}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  res2 \\ \index{res2}
\=\+({\rm{board-statep}}\,({\it{s\/}})\index{board-statep} $\wedge$ {\rm{placep}}\,({\it{a\/}}, {\it{n\/}})\index{placep} $\wedge$ ($\neg$ {\rm{board-statep}}\,({\rm{result}}\,({\it{a\/}}, {\it{s\/}})\index{result})\index{board-statep})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{car}}\,({\rm{result}}\,({\it{a\/}}, {\it{s\/}})\index{result}) $=$ {\tt{'}}{\tt{failed}})\-
\end{tabbing}


\begin{tabbing}{\sc Theorem}:  s1 \\ \index{s1}
({\rm{car}}\,({\it{s\/}}) $=$ {\tt{'}}{\tt{failed}}) $\rightarrow$ ($\neg$ {\rm{board-statep}}\,({\it{s\/}})\index{board-statep})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  res3 \\ \index{res3}
\=\+(\=\+{\rm{board-statep}}\,({\it{s\/}})\index{board-statep} \\ 
$\wedge$$\;\;\;\;${\rm{place-planp}}\,({\it{p\/}}, {\it{n\/}})\index{place-planp} \\ 
$\wedge$$\;\;\;\;${\rm{listp}}\,({\it{p\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{board-statep}}\,({\rm{resultlist}}\,({\it{p\/}}, {\it{s\/}})\index{resultlist})\index{board-statep})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{board-statep}}\,({\rm{result}}\,({\rm{car}}\,({\it{p\/}}), {\it{s\/}})\index{result})\index{board-statep}\-
\end{tabbing}


 The following function is used to force the prover to choose the correct
 induction scheme for the theorem bcequal1.

\begin{tabbing}{\sc Definition}:\index{foo} \\  
\=\+{\rm{foo}}\,({\it{s\/}}, {\it{p\/}})\index{foo} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{p\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\bf{nil}} \\ 
{\bf else }{\rm{foo}}\,({\rm{result}}\,({\rm{car}}\,({\it{p\/}}), {\it{s\/}})\index{result}, {\rm{cdr}}\,({\it{p\/}}))\index{foo}$\;${\bf  endif}\-\-
\end{tabbing}

 If the number of covered white and black squares is equal in a state and
 a sequence of legal domino placement operations is executed then the number
 of covered white and black squares would be equal in the resulting state.

\begin{tabbing}{\sc Theorem}:  bcequal1 \\ \index{bcequal1}
\=\+(\=\+{\rm{board-statep}}\,({\it{s\/}})\index{board-statep} \\ 
$\wedge$$\;\;\;\;$({\rm{nwhite}}\,({\it{s\/}})\index{nwhite} $=$ {\rm{nblack}}\,({\it{s\/}})\index{nblack}) \\ 
$\wedge$$\;\;\;\;${\rm{place-planp}}\,({\it{p\/}}, {\it{n\/}})\index{place-planp} \\ 
$\wedge$$\;\;\;\;${\rm{board-statep}}\,({\rm{resultlist}}\,({\it{p\/}}, {\it{s\/}})\index{resultlist})\index{board-statep})\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{nwhite}}\,({\rm{resultlist}}\,({\it{p\/}}, {\it{s\/}})\index{resultlist})\index{nwhite} $=$ {\rm{nblack}}\,({\rm{resultlist}}\,({\it{p\/}}, {\it{s\/}})\index{resultlist})\index{nblack})\-
\end{tabbing}

 The final theorem:
 Starting with an initial state {\it{s\/}} of an [0..n,0..n] board, {\it{n\/}} 
 greater than 0,
 in which there are no covered squares there
 is no sequence of actions that will result in a state in which 
 all the squares except (0,0) and (n,n) are covered.

\begin{tabbing}{\sc Theorem}:  tough-nut \\ \index{tough-nut}
\=\+(\=\+{\rm{place-planp}}\,({\it{p\/}}, {\it{n\/}})\index{place-planp} \\ 
$\wedge$$\;\;\;\;$({\it{n\/}} $>$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$({\it{s1\/}} $=$ {\rm{resultlist}}\,({\it{p\/}}, {\bf{nil}})\index{resultlist}) \\ 
$\wedge$$\;\;\;\;${\rm{board-statep}}\,({\it{s1\/}})\index{board-statep})\- \\ 
$\rightarrow$$\;\;\;\;$($\neg$ {\rm{all-covered-except-cornerp}}\,({\it{s1\/}}, {\it{n\/}})\index{all-covered-except-cornerp})\-
\end{tabbing}



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