\chapter{Proof}
\label{app:proof}

This Appendix provides a proof for the entire mental image system.
{\bf You do not need to read or understand this section to use the
system.}  This is only here for the die-hard mathematicians who are
actually interested in it.

The proof will proceed as follows:

\begin{enumerate}
\item Introduce the states we will manipulate
\item Prove correctness for simple calls in simple setups
\item ...
\end{enumerate}

\section{Definitions}

A {\em mental image state\/}, $M$, consists of a location for the
designee and the position and nature of the allemande spot.

A {\em setup\/}, $S$, consists of a formation and arrangement and a
specific symmetric assignment of all eight dancers to a unique
position in the formation.

A {\em configuration\/}, $C$, consists of a setup paired with a mental
image state.

We say that a configuration is {\em correct\/} if the mental-image
formulation correctly tracks all combinations of legal dancer motions
that could get to the setup.  Note that correctness is a property of both
the actual setup and the mental-image state.

We will show that a sequence starts out correctly, that correctness is
preserved under all calls, and that the resolution rules work for
correct configurations.

In the defnitions and theorems below, keep in mind that a
configuration has some parts that describe the actual dancers (the
identities of all the people), some parts that describe the
mental-image state (location of the designee and position and nature
of the allemande spot) and one part the describes both (setup).  When
we execute a call, we manipulate all parts of the configuration.

Definition: A {\em simple setup\/} is lines-facing-in, lines-facing-out,
8-chain, or trade by, either normal or sashayed.

Definition: A {\em simple call\/} is trade by or any four-person call that
begins and ends in couples facing in or out.

We will prove the fundamental correctness theorem only for simple
calls in simple setups, and then extend it to other setups and calls
by equivalence to simple setups and calls.

Definition: A configuration with a simple setup is correct if:

\begin{itemize}
\item Case 1: The spot is \o, the designee is located in the front row,
both boys and girls are in sequence, and $B_i$ is next clockwise from
$G_{i+loc-spot}$.

Loc = where the designee is.  Spot = where the allemande spot is.
Person numbers are normal 1/2/3/4 numbering.  All arithmetic is modulo
4, considering couple 4 to be couple 0.

\item Case 2: The spot is \o, the designee is located in the back row,
both boys and girls are out of sequence, and $B_i$ is next CCW from
$G_i+loc-spot$.  \note{Make it CW from $G_i+loc-spot-1$}

\item Case 3: The spot is \x, the designee is located in the front
row, boys are in sequence, girls are out of sequence, and $B_i$ is
across from $G_i+1-spot$.

\item Case 4: The spot is \x, the designee is located in the back row,
girls are in sequence, boys are out of sequence, and $B_i$ is across
from $G_i+1-spot$.
\end{itemize}

Across from means: (picture)

Theorem: Correctness is preserved under U-turn back, 1/4 in, 1/4 out,
on each side.

Proof: These preserve the fact that the setup is simple.  The
locations of the dancers do not change.  Since the calls are \o{}s
that don't move the designee, the spot and designee (location, front
or back) don't change.

Theorem: Correctness is preserved under a call that just swpas front
and back rows, such as \call{pass thru} or \call{pass thru}$^{-1}$
from lines in/out, or sashay from 8-chain and trade by.

Proof: These preserve the simplicity of the setup.  The designee just
swaps between front and back rows.  Other than that, his location does
not change.  Since the calls are \o{}s, the spot does not move or
change its nature.

\begin{itemize}
\item Case 1: Since the designee goes to the back row, this becomes
case 2.  Both boys and girls will be out of sequence after they all
swap front and back rows.  If $B_x$ was CW from $G_y$ before, he will
be CCW from her afterwards.

\item Case 2: This goes to case 1, reversing the argument above.

\item Case 3: This goes to case 4.  Everyone's sequence changes.  Each
boy is across from the same girl before and after.

\item Case 4: This goes to case 3.  Argument is as above.
\end{itemize}

Theorem: Correctness is preserved under a call that just swaps left
and right sides in each box, that is, \call{pass thru} or \call{pass
thru}$^{-1}$ from 8-chain or trade by, or sashay from lines in/out.

Proof: These preserve the simplicity of the setup.  The locations of
the dancers swap left to right.  The allemande spot does not move or
change nature, since the calls are \o{}s.  The designee moves left
$\Leftrightarrow$ right but not forward $\Leftrightarrow$ back.  Who
is in or out of sequence is unaffected, since each sex moves
collectively in a consistent direction.

\begin{itemize}
\item Case 1: Will continue to be case 1.  If loc=0 or 2 (normal lines
in), loc will increase by 1, going to 1 or 3.  Boys will go CCW while
girls go CW.  $B_i,v$ will therefore go to being next CW from G who
was CCW original next CW from $G_{i+loc-spot}$ from that girl.  Since
girls are in sequence, that is $G_{i+1+loc-spot}$ or
$G_{i+(loc+1}-spot$.  But loc went up by 1.  If loc=1 or 3 (sasyahed
LI) loc will decrease by 1.  Apply the reverse of the argument above.

\item Case 2: Will continue to be case 2.  If loc=1 or 3 (normal LI,
remember that designee is in back) dancer action will same as for case
1 with loc=0 or 2.  Therefore, $B_i$, originally next CCW from
$G_{i+loc-spot}$ will go to being next CCW from G who was CCW from
that G.  Since G are out of sequence, that will be next lower numbered
G, that is $B_i$ will be next CCW from $G_{i+loc-spot-1}$, or
$G_{i+(loc-1)-spot}$.  But loc went down by 1.  If loc=0 or 2
(sashayed LI) loc will increase by 1.  Reverse the above argument.

\item Case 3: Will continue to be case 3.  Who is across from whom
doesn't change.  Nor does spot.  If $B_i$ is across from
$G_{i+1-spot}$ before, he will continue to be.

\item Case 4: Will continue to be case 4.  Same as case 3.
\end{itemize}