\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 Computational Logic, Inc.  All Rights Reserved.

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

 NO WARRANTY

 Computational Logic, Inc. 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 Computational Logic, Inc. 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}
\noindent{\sc Event}:   Start with the initial {\bf nqthm} theory.

\addvspace{18pt}


\begin{verbatim}; A Mechanical Checking of a Theorem About a Card Trick

;  Robert S. Boyer, May 22, 1991

; This is a formalization, in the Nqthm logic, of a card trick theorem
; that de Bruijn taught Huet, Huet taught Moore, and Moore taught me.
; Mine differs from a treatment of the same problem by Moore in that
; he uses oracles to simulate shuffling, whereas I use a merge
; predicate.

; Here is Moore's statement of the trick:

   ; Suppose you have a deck of cards of even length.  Suppose the cards
   ; alternate between red ones and black ones.  Cut the deck into two
   ; piles, a and b.  Shuffle a and b together.  Then the following is
   ; true of the shuffled deck.  If the bottom-most cards in a and b are
   ; of different color, then when the cards of the shuffled deck are
   ; taken from the top in adjacent pairs, each pair contains a card of
   ; each color.  On the other hand, if the bottom-most cards in a and b
   ; are the same color, the above pairing property holds after rotating
   ; the shuffled deck by one card, i.e., moving the bottom card to the
   ; top.

#| For other references see

The Gilbreath Tick: A Case Study in Axiomatization and Proof Development in the
COQ Proof Assistant, Gerard Huet, Technical Report 1511, INRIA, September,
1991.

M. Gardner, Mathematical Recreation Column, Scientific American, Aug. 1960.,
p. 149, vol. 203, no. 2.

N. Gilbreath, Magnetic Colors, The Linking Ring, 38(5), 1958, p. 60.

|#



; Now on to my formalization.  We first define the six functions
; needed in the statement of the theorem.  The main, all encompassing,
; theorem is stated at the very end, and is named ``all''.

; Intuitively, we imagine that cards are arbitrary objects, but
; numbers are ``red'' and nonnumbers are ``black.''

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{opposite-color} \\  
{\rm{opposite-color}}\,({\it{x\/}}, {\it{y\/}})\index{opposite-color} $=$ ((({\it{x\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{y\/}} $\not\in\;${\bf{N}}${}$)) $\vee$ (({\it{y\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{x\/}} $\not\in\;${\bf{N}}${}$)))
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{alternating-colors} \\  
\=\+{\rm{alternating-colors}}\,({\it{x\/}})\index{alternating-colors} \\ 
$=$$\;\;\;\;$\=\+{\bf if }({\it{x\/}} $\simeq\;${{\bf{nil}}}${}$) $\vee$ ({\rm{cdr}}\,({\it{x\/}}) $\simeq\;${{\bf{nil}}}${}$)$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }\=\+{\rm{opposite-color}}\,({\rm{car}}\,({\it{x\/}}), {\rm{cadr}}\,({\it{x\/}}))\index{opposite-color} \\ 
$\wedge$$\;\;\;\;${\rm{alternating-colors}}\,({\rm{cdr}}\,({\it{x\/}}))\index{alternating-colors}\-$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{paired-colors} \\  
\=\+{\rm{paired-colors}}\,({\it{x\/}})\index{paired-colors} \\ 
$=$$\;\;\;\;$\=\+{\bf if }({\it{x\/}} $\simeq\;${{\bf{nil}}}${}$) $\vee$ ({\rm{cdr}}\,({\it{x\/}}) $\simeq\;${{\bf{nil}}}${}$)$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }{\rm{opposite-color}}\,({\rm{car}}\,({\it{x\/}}), {\rm{cadr}}\,({\it{x\/}}))\index{opposite-color} $\wedge$ {\rm{paired-colors}}\,({\rm{cddr}}\,({\it{x\/}}))\index{paired-colors}$\;${\bf  endif}\-\-
\end{tabbing}

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

\begin{tabbing}{\sc Definition}:\index{shufflep} \\  
\=\+{\rm{shufflep}}\,({\it{x\/}}, {\it{y\/}}, {\it{z\/}})\index{shufflep} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{z\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }({\it{x\/}} $=$ {\bf{nil}}) $\wedge$ ({\it{y\/}} $=$ {\bf{nil}}) $\wedge$ ({\it{z\/}} $=$ {\bf{nil}}) \\ 
{\bf elseif }{\it{x\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }({\it{x\/}} $=$ {\bf{nil}}) $\wedge$ ({\it{y\/}} $=$ {\it{z\/}}) $\wedge$ {\rm{plistp}}\,({\it{y\/}})\index{plistp} \\ 
{\bf elseif }{\it{y\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }({\it{y\/}} $=$ {\bf{nil}}) $\wedge$ ({\it{x\/}} $=$ {\it{z\/}}) $\wedge$ {\rm{plistp}}\,({\it{x\/}})\index{plistp} \\ 
{\bf else }\=\+(({\rm{car}}\,({\it{x\/}}) $=$ {\rm{car}}\,({\it{z\/}})) $\wedge$ {\rm{shufflep}}\,({\rm{cdr}}\,({\it{x\/}}), {\it{y\/}}, {\rm{cdr}}\,({\it{z\/}}))\index{shufflep}) \\ 
$\vee$$\;\;\;\;$(({\rm{car}}\,({\it{y\/}}) $=$ {\rm{car}}\,({\it{z\/}})) $\wedge$ {\rm{shufflep}}\,({\it{x\/}}, {\rm{cdr}}\,({\it{y\/}}), {\rm{cdr}}\,({\it{z\/}}))\index{shufflep})\-$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{even-length} \\  
\=\+{\rm{even-length}}\,({\it{l\/}})\index{even-length} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{l\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\bf{t}} \\ 
{\bf elseif }{\rm{cdr}}\,({\it{l\/}}) $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\bf{f}} \\ 
{\bf else }{\rm{even-length}}\,({\rm{cddr}}\,({\it{l\/}}))\index{even-length}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{verbatim};;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

; That ends the definitions needed to state the final theorem ``all,'' given
; at the end of this file.

; We now proceed to develop 17 auxiliary lemmas to help prove
; ``all.''

\end{verbatim}\begin{tabbing}{\sc Theorem}:  al-$>$pp \\ \index{al-$>$pp}
{\rm{alternating-colors}}\,({\it{x\/}})\index{alternating-colors} $\rightarrow$ {\rm{paired-colors}}\,({\it{x\/}})\index{paired-colors}
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{silly} \\  
\=\+{\rm{silly}}\,({\it{x\/}}, {\it{y\/}}, {\it{z\/}})\index{silly} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{z\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }{\rm{list}}\,(\=\+{\rm{silly}}\,({\rm{cddr}}\,({\it{x\/}}), {\it{y\/}}, {\rm{cddr}}\,({\it{z\/}}))\index{silly}, \\ 
{\rm{silly}}\,({\rm{cdr}}\,({\it{x\/}}), {\rm{cdr}}\,({\it{y\/}}), {\rm{cddr}}\,({\it{z\/}}))\index{silly}, \\ 
{\rm{silly}}\,({\it{x\/}}, {\rm{cddr}}\,({\it{y\/}}), {\rm{cddr}}\,({\it{z\/}}))\index{silly})\-$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  main \\ \index{main}
\=\+(\=\+{\rm{shufflep}}\,({\it{x\/}}, {\it{y\/}}, {\it{z\/}})\index{shufflep} \\ 
$\wedge$$\;\;\;\;${\rm{alternating-colors}}\,({\it{x\/}})\index{alternating-colors} \\ 
$\wedge$$\;\;\;\;${\rm{alternating-colors}}\,({\it{y\/}})\index{alternating-colors} \\ 
$\wedge$$\;\;\;\;${\rm{listp}}\,({\it{x\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{listp}}\,({\it{y\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{opposite-color}}\,({\rm{car}}\,({\it{x\/}}), {\rm{car}}\,({\it{y\/}}))\index{opposite-color})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{paired-colors}}\,({\it{z\/}})\index{paired-colors}\-
\end{tabbing}

\begin{verbatim}; The closer to a gensym is the name of a lemma, the more boring and
; obvious it is.  As usual in such Nqthm proofs, these tedious lemmas
; are conceived by carefully reading failed Nqthm proofs rather than
; by thinking ahead.  The idea is to prove only those things which are
; suggested by Nqthm failures.

\end{verbatim}\begin{tabbing}{\sc Theorem}:  f2 \\ \index{f2}
({\rm{plistp}}\,({\it{d\/}})\index{plistp} $\wedge$ {\rm{plistp}}\,({\it{c\/}})\index{plistp}) $\rightarrow$ {\rm{shufflep}}\,({\it{c\/}}, {\it{d\/}}, {\rm{append}}\,({\it{c\/}}, {\it{d\/}}))\index{shufflep}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  f3 \\ \index{f3}
({\rm{plistp}}\,({\it{d\/}})\index{plistp} $\wedge$ {\rm{plistp}}\,({\it{c\/}})\index{plistp}) $\rightarrow$ {\rm{shufflep}}\,({\it{c\/}}, {\it{d\/}}, {\rm{append}}\,({\it{d\/}}, {\it{c\/}}))\index{shufflep}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  cdr-append \\ \index{cdr-append}
\=\+{\rm{cdr}}\,({\rm{append}}\,({\it{c\/}}, {\it{d\/}})) \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{c\/}})$\;\;${\bf then }{\rm{append}}\,({\rm{cdr}}\,({\it{c\/}}), {\it{d\/}}) \\ 
{\bf else }{\rm{cdr}}\,({\it{d\/}})$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  f4 \\ \index{f4}
({\rm{plistp}}\,({\it{w\/}})\index{plistp} $\wedge$ {\rm{shufflep}}\,({\it{x\/}}, {\it{y\/}}, {\it{z\/}})\index{shufflep}) $\rightarrow$ {\rm{shufflep}}\,({\it{x\/}}, {\rm{append}}\,({\it{y\/}}, {\it{w\/}}), {\rm{append}}\,({\it{z\/}}, {\it{w\/}}))\index{shufflep}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  f5 \\ \index{f5}
({\rm{plistp}}\,({\it{w\/}})\index{plistp} $\wedge$ {\rm{shufflep}}\,({\it{x\/}}, {\it{y\/}}, {\it{z\/}})\index{shufflep}) $\rightarrow$ {\rm{shufflep}}\,({\rm{append}}\,({\it{x\/}}, {\it{w\/}}), {\it{y\/}}, {\rm{append}}\,({\it{z\/}}, {\it{w\/}}))\index{shufflep}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  trick \\ \index{trick}
\=\+({\rm{listp}}\,({\it{x\/}}) $\wedge$ {\rm{listp}}\,({\it{y\/}}) $\wedge$ {\rm{shufflep}}\,({\it{x\/}}, {\it{y\/}}, {\it{z\/}})\index{shufflep}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{shufflep}}\,({\rm{append}}\,({\rm{cdr}}\,({\it{x\/}}), {\rm{list}}\,({\rm{car}}\,({\it{x\/}}))), {\it{y\/}}, {\rm{append}}\,({\rm{cdr}}\,({\it{z\/}}), {\rm{list}}\,({\rm{car}}\,({\it{z\/}}))))\index{shufflep} \\ 
$\vee$$\;\;\;\;${\rm{shufflep}}\,(\=\+{\it{x\/}}, \\ 
{\rm{append}}\,({\rm{cdr}}\,({\it{y\/}}), {\rm{list}}\,({\rm{car}}\,({\it{y\/}}))), \\ 
{\rm{append}}\,({\rm{cdr}}\,({\it{z\/}}), {\rm{list}}\,({\rm{car}}\,({\it{z\/}}))))\-\index{shufflep})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  car-append \\ \index{car-append}
\=\+{\rm{car}}\,({\rm{append}}\,({\it{x\/}}, {\it{y\/}})) \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{x\/}})$\;\;${\bf then }{\rm{car}}\,({\it{x\/}}) \\ 
{\bf else }{\rm{car}}\,({\it{y\/}})$\;${\bf  endif}\-\-
\end{tabbing}
               
\begin{tabbing}{\sc Theorem}:  f12 \\ \index{f12}
\=\+({\rm{alternating-colors}}\,({\rm{append}}\,({\it{c\/}}, {\rm{list}}\,({\it{d\/}})))\index{alternating-colors} $\wedge$ ($\neg$ {\rm{opposite-color}}\,({\it{d\/}}, {\it{e\/}})\index{opposite-color})) \\ 
$\rightarrow$$\;\;\;\;${\rm{alternating-colors}}\,({\rm{append}}\,({\it{c\/}}, {\rm{list}}\,({\it{e\/}})))\index{alternating-colors}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  f6 \\ \index{f6}
\=\+({\rm{listp}}\,({\it{l\/}}) $\wedge$ {\rm{even-length}}\,({\it{l\/}})\index{even-length} $\wedge$ {\rm{alternating-colors}}\,({\it{l\/}})\index{alternating-colors}) \\ 
$\rightarrow$$\;\;\;\;${\rm{alternating-colors}}\,({\rm{append}}\,({\rm{cdr}}\,({\it{l\/}}), {\rm{list}}\,({\rm{car}}\,({\it{l\/}}))))\index{alternating-colors}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  g19 \\ \index{g19}
\=\+({\rm{alternating-colors}}\,({\it{c\/}})\index{alternating-colors} $\wedge$ ({\rm{car}}\,({\it{c\/}}) $\in\;${\bf{N}}${}$) $\wedge$ {\rm{even-length}}\,({\it{c\/}})\index{even-length} $\wedge$ ({\it{v\/}} $\in\;${\bf{N}}${}$)) \\ 
$\rightarrow$$\;\;\;\;${\rm{alternating-colors}}\,({\rm{append}}\,({\it{c\/}}, {\rm{list}}\,({\it{v\/}})))\index{alternating-colors}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  g20 \\ \index{g20}
\=\+({\rm{alternating-colors}}\,({\it{c\/}})\index{alternating-colors} $\wedge$ ({\rm{car}}\,({\it{c\/}}) $\not\in\;${\bf{N}}${}$) $\wedge$ {\rm{even-length}}\,({\it{c\/}})\index{even-length} $\wedge$ ({\it{v\/}} $\not\in\;${\bf{N}}${}$)) \\ 
$\rightarrow$$\;\;\;\;${\rm{alternating-colors}}\,({\rm{append}}\,({\it{c\/}}, {\rm{list}}\,({\it{v\/}})))\index{alternating-colors}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  fap \\ \index{fap}
\=\+(\=\+{\rm{shufflep}}\,({\it{x\/}}, {\it{y\/}}, {\it{z\/}})\index{shufflep} \\ 
$\wedge$$\;\;\;\;${\rm{alternating-colors}}\,({\it{x\/}})\index{alternating-colors} \\ 
$\wedge$$\;\;\;\;${\rm{alternating-colors}}\,({\it{y\/}})\index{alternating-colors} \\ 
$\wedge$$\;\;\;\;${\rm{even-length}}\,({\it{x\/}})\index{even-length} \\ 
$\wedge$$\;\;\;\;${\rm{even-length}}\,({\it{y\/}})\index{even-length} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{opposite-color}}\,({\rm{car}}\,({\it{x\/}}), {\rm{car}}\,({\it{y\/}}))\index{opposite-color}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{paired-colors}}\,({\rm{append}}\,({\rm{cdr}}\,({\it{z\/}}), {\rm{list}}\,({\rm{car}}\,({\it{z\/}}))))\index{paired-colors}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  al2 \\ \index{al2}
\=\+(\=\+{\rm{alternating-colors}}\,({\rm{append}}\,({\it{x\/}}, {\it{y\/}}))\index{alternating-colors} \\ 
$\wedge$$\;\;\;\;${\rm{even-length}}\,({\rm{append}}\,({\it{x\/}}, {\it{y\/}}))\index{even-length} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{opposite-color}}\,({\rm{car}}\,({\it{x\/}}), {\rm{car}}\,({\it{y\/}}))\index{opposite-color}))\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{even-length}}\,({\it{x\/}})\index{even-length} $\wedge$ {\rm{even-length}}\,({\it{y\/}})\index{even-length})\-
\end{tabbing}
                
\begin{tabbing}{\sc Theorem}:  g16 \\ \index{g16}
($\neg$ {\rm{alternating-colors}}\,({\it{x\/}})\index{alternating-colors}) $\rightarrow$ ($\neg$ {\rm{alternating-colors}}\,({\rm{append}}\,({\it{x\/}}, {\it{y\/}}))\index{alternating-colors})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  g17 \\ \index{g17}
($\neg$ {\rm{alternating-colors}}\,({\it{y\/}})\index{alternating-colors}) $\rightarrow$ ($\neg$ {\rm{alternating-colors}}\,({\rm{append}}\,({\it{x\/}}, {\it{y\/}}))\index{alternating-colors})
\end{tabbing}

\begin{verbatim};;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

; That ends the intermediate development of auxiliary lemmas.  We are now
; ready for the main result.

\end{verbatim}\begin{tabbing}{\sc Theorem}:  all \\ \index{all}
\=\+(\=\+{\rm{alternating-colors}}\,({\rm{append}}\,({\it{x\/}}, {\it{y\/}}))\index{alternating-colors} \\ 
$\wedge$$\;\;\;\;${\rm{even-length}}\,({\rm{append}}\,({\it{x\/}}, {\it{y\/}}))\index{even-length} \\ 
$\wedge$$\;\;\;\;${\rm{shufflep}}\,({\it{x\/}}, {\it{y\/}}, {\it{z\/}})\index{shufflep} \\ 
$\wedge$$\;\;\;\;${\rm{listp}}\,({\it{x\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{listp}}\,({\it{y\/}}))\- \\ 
$\rightarrow$$\;\;\;\;$\=\+{\bf if }{\rm{opposite-color}}\,({\rm{car}}\,({\it{x\/}}), {\rm{car}}\,({\it{y\/}}))\index{opposite-color}$\;\;${\bf then }{\rm{paired-colors}}\,({\it{z\/}})\index{paired-colors} \\ 
{\bf else }{\rm{paired-colors}}\,({\rm{append}}\,({\rm{cdr}}\,({\it{z\/}}), {\rm{list}}\,({\rm{car}}\,({\it{z\/}}))))\index{paired-colors}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{verbatim}; To run this list of events takes about 1 hour of cpu time on a
; Sun-3/280.  To develop this list of events took about 15 hours of
; work.
\end{verbatim}
%\end{list}
\printindex
\end{document}
