**
John McCarthy Computer Science Department Stanford University jmc@cs.stanford.edu
http://www-formal.stanford.edu/jmc/ **

**February 28, 1996
**

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
*heavy duty set theory*.

We have the definitions

and

If we are willing to be slightly tricky, we can write more compactly

but then the proof might not be so obvious to the program.

Next we have.

**Theorem**:

**Proof:**

We define

and finally

**Q.E.D.**

Wed Feb 28 19:43:17 PST 1996