\documentstyle[11pt]{article}
\begin{document}
\bibliographystyle{plain}
%                  \font\Bbb=msbm10   wrt    \bf N  -> \Bbb N
\title{\bf The Mutilated Chessboard Problem - \em checked by Mizar}
\author{Grzegorz Bancerek\thanks{Institute of Mathematics, Polish 
Academy of Science, Warsaw,
e-mail: \ \ \ \ \ \ \ \break\tt bancerek@impan.gov.pl .}}
\date{}
\maketitle

\abstract{The problem presented by John McCarthy during his lecture
"Heavy duty set theory"\footnote{In this Report see: {\em The Mutilated 
Checkerboard in Set Theory} by John McCarthy.} has been resolved here.
The final version of that article has been made with the
commitment of Andrzej Trybulec.
 
Proofs have been written in Mizar language and were checked
by PC Mizar system. In this paper only definitions and theorems
are published apart from proofs (this is the so called `mizar
abstract'). Then it has been automatically translated into
English. The format of this article is exactly the same as
in journal {\em Formalized Mathematics}.}

\begin{quotation}
\noindent \small MML Identifier: {\tt M\_\hskip.5ptBOARD}.
\end{quotation}
\vskip 20pt
\def\mizleftcart{\mathopen{[\!:}}
\def\mizrightcart{\mathclose{:\!]}}
\def\es{{\mathchoice{}{}{\,}{\,}}}
\def\biginterline{\vskip2pt}
\noindent The articles \cite{TARSKI.ABS},
\cite{INT_1.ABS},
\cite{NAT_1.ABS},
\cite{BOOLE.ABS},
\cite{RELAT_1.ABS},
\cite{FUNCT_1.ABS},
\cite{FINSEQ_1.ABS},
\cite{FINSET_1.ABS},
\cite{MCART_1.ABS},
\cite{DOMAIN_1.ABS},
\cite{ANAL_1.ABS},
\cite{BINARITH.ABS},
\cite{WELLORD2.ABS},
and \cite{CARD_1.ABS} provide the notation and terminology  for this paper.


We
follow a convention:
$x$,
$z$
will be sets,
$i$,
$j$,
$k$
will be natural numbers, and
$u$,
$v$
will be elements of $\mizleftcart\,{\bf N}, \allowbreak\,{\bf
 N}\,\mizrightcart$.

One can prove the following proposition
\par\biginterline
\begin{description}
\item[{\makebox[30pt][r]{(1)\hspace{5pt}}}]
\tolerance=9999
% ExpSize = 32
If
$( i \es\mathbin{\rm mod}\es k) + ( j \es\mathbin{\rm mod}\es k) < k, $
then
$( i + j) \es\mathbin{\rm mod}\es k = ( i \es\mathbin{\rm mod}\es k) + ( j
\es\mathbin{\rm mod}\es k). $
\end{description}

Set ${\it Board} = \mizleftcart\,\mathop{\rm Seg} 8, \allowbreak\,\mathop{\rm
 Seg} 8\,\mizrightcart$
and
${\it MBoard} = {\it Board} \setminus \{\lbrack 1,1\rbrack, \lbrack
 8,8\rbrack\}$.


Let
$x$
be an element of $\mizleftcart\,{\bf N}, \allowbreak\,{\bf N}\,\mizrightcart$.
Then
${ x_{\bf 1}}$ and
${ x_{\bf 2}}$
are natural numbers.

Let
${x_{1}}$,
${x_{2}}$
be elements of $\mizleftcart\,{\bf N}, \allowbreak\,{\bf N}\,\mizrightcart$.
We say that
${x_{1}}$
is adjacent to ${x_{2}}$
if and only if:
\begin{description}
\item[{\makebox[30pt][r]{(Def.1)\hspace{5pt}}}]
\tolerance=9999
$\vert {( {x_{1}})_{\bf 1}} - {( {x_{2}})_{\bf 1}} \vert = 1$
 and
${( {x_{1}})_{\bf 2}} = {( {x_{2}})_{\bf 2}}$
 or
$\vert {( {x_{1}})_{\bf 2}} - {( {x_{2}})_{\bf 2}} \vert = 1$
 and
${( {x_{1}})_{\bf 1}} = {( {x_{2}})_{\bf 1}}. $
\end{description}

Let
$x$
be a set.
We say that
$x$
is domino-on-board
if and only if:
\begin{description}
\item[{\makebox[30pt][r]{(Def.2)\hspace{5pt}}}]
\tolerance=9999
$x \subseteq {\it Board}$
 and
$\overline{\overline{\kern1pt x \kern1pt}} = 2$
 and for all elements ${x_{1}}$,
${x_{2}}$
of $\mizleftcart\,{\bf N}, \allowbreak\,{\bf N}\,\mizrightcart$
such that
${x_{1}} \neq {x_{2}}$
 and
${x_{1}} \in x$
 and
${x_{2}} \in x$
holds
${x_{1}}$
is adjacent to ${x_{2}}$.
\end{description}

Let
$z$
be a set.
We say that
$z$
is partial-covering
if and only if the conditions (Def.3) are satisfied.
\begin{description}
\item[{\makebox[30pt][r]{(Def.3)\hspace{5pt}}}]
\tolerance=9999
\indent\quad\llap{ (i)\quad}
For every set $x$
such that
$x \in z$
holds
$x$
is domino-on-board, and
\par
\indent\quad\llap{ (ii)\quad}
for all sets $x$,
$y$
such that
$x \in z$
 and
$y \in z$
holds
$x = y$
 or
$x \cap y = \emptyset. $
\par
\end{description}

Let
$z$
be an element of $\mizleftcart\,{\bf N}, \allowbreak\,{\bf N}\,\mizrightcart$.
The functor
$\mathop{\rm color}( z)$
yielding a natural number
is defined by:
\begin{description}
\item[{\makebox[30pt][r]{(Def.4)\hspace{5pt}}}]
\tolerance=9999
$\mathop{\rm color}( z) = ({ z_{\bf 1}} + { z_{\bf 2}}) \es\mathbin{\rm mod}\es
 2.
$
\end{description}

The following three propositions are true:
\par\biginterline
\begin{description}
\item[{\makebox[30pt][r]{(2)\hspace{5pt}}}]
\tolerance=9999
% ExpSize = 128
Let
$z$
be a set. Suppose
$z$
is partial-covering. Let
$x$
be a set. Suppose
$x \in z.  $
Then there exist elements ${x_{1}}$,
${x_{2}}$
of $\mizleftcart\,{\bf N}, \allowbreak\,{\bf N}\,\mizrightcart$
such that
$x = \lbrace {x_{1}},  {x_{2}} \rbrace$
 and
$\mathop{\rm color}( {x_{1}}) = 0$
 and
$\mathop{\rm color}( {x_{2}}) = 1. $
\item[{\makebox[30pt][r]{(3)\hspace{5pt}}}]
\tolerance=9999
% ExpSize = 79
For every set $z$
such that
$z$
is partial-covering holds
$\{u:  u \in \bigcup z\ \land\ \mathop{\rm color}( u) = 0\} \approx \{v:
v \in \bigcup z\ \land\ \mathop{\rm color}( v) = 1\}. $
\item[{\makebox[30pt][r]{(4)\hspace{5pt}}}]
\tolerance=9999
% ExpSize = 45
It is not true that there exists a set $z$
such that
$z$
is partial-covering and
$\bigcup z = {\it MBoard}$.
\end{description}


\begin{thebibliography}{10}

\bibitem{CARD_1.ABS}
Grzegorz Bancerek.
\newblock Cardinal numbers.
\newblock {\it Formalized Mathematics}, 1({\bf 2}):377--382, 1990.

\bibitem{NAT_1.ABS}
Grzegorz Bancerek.
\newblock The fundamental properties of natural numbers.
\newblock {\it Formalized Mathematics}, 1({\bf 1}):41--46, 1990.

\bibitem{WELLORD2.ABS}
Grzegorz Bancerek.
\newblock Zermelo theorem and axiom of choice.
\newblock {\it Formalized Mathematics}, 1({\bf 2}):265--267, 1990.

\bibitem{FINSEQ_1.ABS}
Grzegorz Bancerek and Krzysztof Hryniewiecki.
\newblock Segments of natural numbers and finite sequences.
\newblock {\it Formalized Mathematics}, 1({\bf 1}):107--114, 1990.

\bibitem{FUNCT_1.ABS}
Czes{\l}aw Byli{\'n}ski.
\newblock Functions and their basic properties.
\newblock {\it Formalized Mathematics}, 1({\bf 1}):55--65, 1990.

\bibitem{FINSET_1.ABS}
Agata Darmochwa{\l}.
\newblock Finite sets.
\newblock {\it Formalized Mathematics}, 1({\bf 1}):165--167, 1990.

\bibitem{BINARITH.ABS}
Takaya Nishiyama and Yasuho Mizuhara.
\newblock Binary arithmetics.
\newblock {\it Formalized Mathematics}, 4({\bf 1}):83--86, 1993.

\bibitem{ANAL_1.ABS}
Jan Popio{\l}ek.
\newblock Some properties of functions modul and signum.
\newblock {\it Formalized Mathematics}, 1({\bf 2}):263--264, 1990.

\bibitem{DOMAIN_1.ABS}
Andrzej Trybulec.
\newblock Domains and their {C}artesian products.
\newblock {\it Formalized Mathematics}, 1({\bf 1}):115--122, 1990.

\bibitem{TARSKI.ABS}
Andrzej Trybulec.
\newblock Tarski {G}rothendieck set theory.
\newblock {\it Formalized Mathematics}, 1({\bf 1}):9--11, 1990.

\bibitem{MCART_1.ABS}
Andrzej Trybulec.
\newblock Tuples, projections and {C}artesian products.
\newblock {\it Formalized Mathematics}, 1({\bf 1}):97--105, 1990.

\bibitem{INT_1.ABS}
Micha{\l}~J. Trybulec.
\newblock Integers.
\newblock {\it Formalized Mathematics}, 1({\bf 3}):501--505, 1990.

\bibitem{BOOLE.ABS}
Zinaida Trybulec and Halina
 {\'{S}}wi{{\hbox{\ooalign{\hbox{e}\crcr\kern.23em\raise-1.28ex\hbox{`}}}}}czkow
 ska.
\newblock Boolean properties of sets.
\newblock {\it Formalized Mathematics}, 1({\bf 1}):17--23, 1990.

\bibitem{RELAT_1.ABS}
Edmund Woronowicz.
\newblock Relations and their basic properties.
\newblock {\it Formalized Mathematics}, 1({\bf 1}):73--83, 1990.

\end{thebibliography}

\end{document}