Computer Science Department
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
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.