\documentclass[]{article}
%\usepackage[]{}
\usepackage{html}


\begin{document}

        \title{
        The Mutilated Checkerboard in Set Theory
}
\author{
        John McCarthy\\Computer Science Department\\Stanford University\\jmc@cs.stanford.edu
        \\http://www-formal.stanford.edu/jmc/   % insert author(s) here
}
\date{\today}   % optional

\maketitle


        An 8 by 8 checkerboard with two diagonally opposite squares removed 
cannot be covered by dominoes each of which covers two rectilinearly 
adjacent squares.  We present a set theory description of the 
proposition and an informal proof that the covering is impossible.  
While no present system that I know of will accept either the formal 
description or the proof, I claim that both should be admitted in any 
\emph{heavy duty set theory}.\footnote{The Mizar proof checker
  accepts the definitions essentially as they are, but the first proof
  in Mizar is 400 lines.}  

We have the definitions

\begin{equation}
        Board = Z8 \times Z8,
        \label{board}
\end{equation}

\begin{equation}
        mutilated\mbox{-}board = Board - \{(0,0),(7,7)\},
        \label{mutilated1}
\end{equation}


\begin{equation}
        \begin{array}{l}
                domino\mbox{-}on\mbox{-}board(x) \equiv (x \subset Board) \land card(x) =2  \\
        \land (\forall x1\ x2)(x = \{x1,x2\}
%       \land (\forall x1\ x2)(x1 \not= x2 \land x1 \in x \land x2 \in x \\
                \rightarrow adjacent(x1,x2))
        \end{array}
        \label{domino}
\end{equation}
%
and
       
\begin{equation}
        \begin{array}{l}
                adjacent(x1,x2) \equiv |c(x1,1) - c(x2,1)| =1 \\
                 \land c(x1,2) = c(x2,2) \\
                \lor |c(x1,2) - c(x2,2)| =1 \land c(x1,1) = c(x2,1).
        \end{array}
        \label{adjacent}
\end{equation}
%
If we are willing to be slightly tricky, we can write more compactly
        
\begin{equation}
      adjacent(x1,x2) \equiv |c(x1,1) - c(x2,1)| + |c(x1,2) - c(x2,2)| = 1,
        \label{adjacent1}
\end{equation}
%
but then the proof might not be so obvious to the program.


Next we have.

\begin{equation}
\begin{array}{l}
                partial\mbox{-}covering(z)  \\
                 \equiv (\forall x)(x \in z \rightarrow
        domino\mbox{-}on\mbox{-}board(x))
  \\
        \land (\forall x\ y)(x \in z \land y \in z \rightarrow x = y \lor x \cap 
        y = \{\})
\end{array}
        \label{covering}
\end{equation}

                
                                        \noindent \textbf{Theorem}: 
\begin{equation}
        \lnot (\exists z)(partial\mbox{-}covering(z) \land \bigcup z
        = mutilated\mbox{-}board)
        \label{theorem}
\end{equation}

\noindent \textbf{Proof:}

We define

\begin{equation}
        x \in Board \rightarrow color(x) = rem(c(x,1) + c(x,2),2)
        \label{color}
\end{equation}



\begin{equation}
\begin{array}{l}
        domino\mbox{-}on\mbox{-}board (x) \rightarrow \\
         (\exists u\ v)(u \in x 
        \land v \in x \land color(u) = 0 \land color(v) = 1),
\end{array}      
        \label{colordomino}
\end{equation}

\begin{equation}
        \begin{array}{l}
                partial\mbox{-}covering(z) \rightarrow  \\
                card(\{u \in \bigcup z|color(u) =0\}) \\
                =       card(\{u \in \bigcup z|color(u) =1\}),
        \end{array}
                \label{eqcolor}
\end{equation}


\begin{equation}
\begin{array}{l}
         card(\{u \in mutilated\mbox{-}board|color(u) = 0\}) \\
        \not= card(\{u \in mutilated\mbox{-}board|color(u) = 1\}),
\end{array}
        \label{mutilated}
\end{equation}
%
and finally

\begin{equation}
        \lnot (\exists z)(partial\mbox{-}covering(z)\ \ \land\ \ 
        mutilated\mbox{-}board = \bigcup z)
        \label{theorem-again}
\end{equation}

\noindent \textbf{Q.E.D.}
        

\end{document}