
%\documentstyle[11pt,zed]{csart}
%\documentstyle{csart}
\documentstyle{article}

\begin{document}

\sloppy

\newenvironment{linear}{\\ \begin{minipage}[t]{\textwidth}}{\end{minipage}}
% Prevents body from being split between pages.  Can't be used at start
% of a paragraph.  Not within an indented environment.

\newenvironment{linpar}{\begin{minipage}[t]{\textwidth}}{\end{minipage}}
% Prevents body from being split between pages.  Used at start
% of a paragraph.  Not within an indented environment.

%\newenvironment{linpar1}{\newlength{\ltormar} \setlength{\textwidth} \addtolength{\textwidth}{-\leftmargin} \begin{minipage}[t]{\ltormar}}{\end{minipage}}
% As above, but 1 level of list indentation.  Doesn't work

\def\dotdot{\mathinner{\ldotp\ldotp}}

\def\parallel{\mathinner{\,\|\,}}
\def\Parallel{\mathinner{\|}}

\def\cho#1#2#3{{\vcenter{\vbox{\hrule height.#3pt
		\hbox{\vrule width.#3pt height#2pt \kern#1pt
		\vrule width.#3pt}
		\hrule height.#3pt}}}}
\def\choi{\mathchoice\cho5{15}{48}\cho4{12}{45}\cho39{25}\cho26{21}}
\def\Choice{\mathop{\smash\choi\vphantom\sum}}

\def\choice{{\scriptstyle \Choice }}

\def\righti#1#2{{\mathclose>\llap{$#2\kern#1pt$}}}
\def\rightif{\mathchoice\righti{3}{\displaystyle|}\righti3{\textstyle|}\righti{2}{\scriptstyle|}\righti{2}{\scriptscriptstyle|}\,}
\def\lefti#1#2{{\mathopen<\llap{$#2\kern#1pt$}}}
\def\leftif{\,\mathchoice\lefti{2}{\displaystyle|}\lefti{2}{\textstyle|}\lefti{2}{\scriptstyle|}\lefti{1.5}{\scriptscriptstyle|}}

\newcommand{\proc}[1]{\mbox{\bf {#1}}}
\newcommand{\bvector}[1]{\mbox{\boldmath $#1$}}
\newcommand{\mysymbol}[1]{\mbox{\it {#1}}}
\newcommand{\function}[1]{\mbox{\it {#1}} \,}

\def\satisfies{\, \, \mbox {\bf sat}\, \,}

\def\lbag{[[}
\def\rbag{]]}

\def\ndchoice{\sqcap}
\def\suchthat{\, | \,}
\def\concat{\hat{\mbox{ }}}
\def\pling{\, ! \,}
\def\query{\, ? \,}
\def\seq{; \, \,}
\def\next{, \,}

\def\bif{\mbox{\bf if}\, \,}
\def\bthen{\, \, \mbox{\bf then}\, \,}
\def\belse{\, \, \mbox{\bf else}\, \,}

\def\bcase{\mbox{\bf case}\, \,}
\def\bof{\, \, \mbox{\bf of}\, \,}
\def\aof{\mbox{\bf of}}
\def\bwhere{\mbox{\bf where}\, \,}

\def\powset{\mbox{P}}

\def\tini{\function{ini}}
\def\tok{\mysymbol{ok}}
\def\tdat{\function{dat}}
\def\treq{\function{req}}
\def\tnew{\mysymbol{new}}
\def\tchg{\function{chg}}
\def\tquo{\function{quo}}
\def\tacs{\function{acs}}
\def\tack{\function{ack}}
\def\tmov{\function{mov}}
\def\tin{\function{in}}
\def\tout{\function{out}}

\def\interleaves{\, \, \function{interleaves}}

\def\any{\,\_\,}

\def\seqsize{\mbox{\#}}

\def\follow{\, \mbox{\^{ }} \,}
\def\flatten{\mbox{\^{ }}/ \,}

\section{External Events}

$\tdat$ transfers are followed by $\tack$ acknowledgments.
$\treq$ requests evoke the return of $\tacs$ access permissions.\\ \\
\begin{linpar}
$C.U.\tdat (e)$ \\
$U.C.\tdat (e)$ 

\begin{description}
\item[]
\begin{tabbing}
$P$  \=\kill
$C$ \> = data transfer channel. \\
$e$ \> = data value transferred.
\end{tabbing}

$C.U.\mysymbol{dat}$ is in the alphabets of 
channel end $\tout (C)$ and the user process.
$U.C.\mysymbol{dat}$ is in the alphabets of 
channel end $\tin (C)$ and the user process.
\end{description}
\end{linpar}
\ \\ \\
\noindent
\begin{linpar}
$C.U.\tack$ \\
$U.C.\tack$ 

\begin{description}
\item[]
\begin{tabbing}
$P$  \=\kill
$C$ \> = data transfer channel.
\end{tabbing}

$C.U.\mysymbol{ack}$ is in the alphabets of 
channel end $\tin (C)$ and the user process.
$U.C.\mysymbol{ack}$ is in the alphabets of 
channel end $\tout (C)$ and the user process.
\end{description}
\end{linpar}
\ \\ \\
\noindent
\begin{linpar}
$C.U.\treq$ \\
$U.C.\treq$ 

\begin{description}
\item[]
\begin{tabbing}
$P$  \=\kill
$C$ \> = access transfer channel.
\end{tabbing}

$C.U.\mysymbol{req}$ is in the alphabets of 
channel end $\tout (C)$ and the user process.
$U.C.\mysymbol{req}$ is in the alphabets of 
channel end $\tin (C)$ and the user process.
\end{description}
\end{linpar}
\ \\ \\
\noindent
\begin{linpar}
$C.U.\tacs (F)$ \\
$U.C.\tacs (F)$ 

\begin{description}
\item[]
\begin{tabbing}
$P$  \=\kill
$C$ \> = access transfer channel\\
$F$ \> = channel end, access to which is transferred.
\end{tabbing}

$C.U.\mysymbol{acs (F)}$ is in the alphabets of 
channel end $\tin (C)$ and the user process.
$U.C.\mysymbol{acs (F)}$ is in the alphabets of 
channel end $\tout (C)$ and the user process.
\end{description}
\end{linpar}


\section{Messages}

\subsection{Data Transfer Messages}

$\tack$ is an acknowledgement of a $\tdat$ message.\\ \\
\begin{linpar}
$Q.P^O.\tdat (e, C)$ \\
$Q.P^I.\tdat (e, C)$ 

\begin{description}
\item[]
\begin{tabbing}
$P$  \=\kill
$P$ \> = port associated with channel end $\tout (C)$. \\
$Q$ \> = port associated with $\tin (C)$. \\
$e$ \> = data value transferred. \\
$C$ \> = data transfer channel.
\end{tabbing}

$\mysymbol{dat}$ output is in the alphabets of 
port $P$, channel end $\tout (C)$, and the message delivery system.
$\mysymbol{dat}$ input is in the alphabets of port $Q$,
channel end $\tin (C)$, and the message delivery system.
\end{description}
\end{linpar}
\ \\ \\
\noindent
\begin{linpar}
$P.Q^O.\tack (C)$ \\
$P.Q^I.\tack (C)$ 

\begin{description}
\item[]
\begin{tabbing}
$P$  \=\kill
$P$ \> = port associated with channel end $\tout (C)$. \\
$Q$ \> = port associated with $\tin (C)$. \\
$C$ \> = data transfer channel.
\end{tabbing}

$\mysymbol{ack}$ output is in the alphabets of 
port $Q$, channel end $\tin (C)$, and the message delivery system.
$\mysymbol{ack}$ input is in the alphabets of port $P$,
channel end $\tout (C)$, and the message delivery system.
\end{description}
\end{linpar}

\subsection{Access Transfer Messages}

$\treq$ requests access to some available channel end be transferred to a
locally allocated port.  ``Acknowledgment'' of the request goes
through the control transfer messages introduced below.\\ \\
\begin{linpar}
$Q.P^O.\treq (R, C)$ \\
$Q.P^I.\treq (R, C)$ 

\begin{description}
\item[]
\begin{tabbing}
$P$  \=\kill
$P$ \> = port associated with channel end $\tout (C)$. \\
$Q$ \> = port associated with $\tin (C)$. \\
$R$ \> = recipient port, to which access will be transferred. \\
$C$ \> = data transfer channel.
\end{tabbing}

$\mysymbol{req}$ output is in the alphabets of 
ports $P$ and $R$, channel end $\tout (C)$, and the message delivery system.
$\mysymbol{req}$ input is in the alphabets of port $Q$, channel end
$\tin (C)$, and the message delivery system.
\end{description}
\end{linpar}

\subsection{Control Transfer Messages}

     The $\mysymbol{ini}$ message is sent from a port process
to its successor on termination of the former.  It carries information
needed to initialise the new port. \\ \\
\begin{linpar}
$P.S^O.\tini (E, Q, s, D)$ \\
$P.S^I.\tini (E, Q, s, D)$ 

\begin{description}
\item[]
\begin{tabbing}
$P$  \=\kill
$P$ \> = port formerly associated with channel end $E$. \\
$S$ \> = successor port to $P$. \\
$E$ \> = a channel end. \\
$Q$ \> = port associated with partner of $E$. \\
$s$ \> = value defining a set of events pending on $E$
	   at time of transfer. \\
$D$ \> = access transfer channel.
\end{tabbing}
$\mysymbol{ini}$ output is in the alphabets of channel end $E$,
port $P$, and the message delivery system.
$\mysymbol{ini}$ input is in the alphabets of channel ends $E$
and $\tout (D)$, port $S$, and the message delivery system.
\end{description}
\end{linpar}

\subsection{Port Repointing Messages}

These messages are used during transfer of access to a channel end
to inform the port associated with the {\em partner} channel end
of the move. $\tquo$ is an acknowledgement of a $\tchg$ message.\\ \\
\begin{linpar}
$Q.P^O.\tchg (E, S, D)$ \\
$Q.P^I.\tchg (E, S, D)$ 

\begin{description}
\item[]
\begin{tabbing}
$P$  \=\kill
$P$ \> = port formerly associated with channel end $E$. \\
$Q$ \> = port associated with partner of $E$. \\
$S$ \> = successor port to $P$. \\
$E$ \> = a channel end. \\
$D$ \> = access transfer channel.
\end{tabbing}
$\mysymbol{chg}$ output is in the alphabets of channel end $\tin (D)$,
port $P$, and the message delivery system.
$\mysymbol{chg}$ input is in the alphabets of port $Q$ and
the message delivery system.
\end{description}
\end{linpar}
\ \\ \\
\noindent
\begin{linpar}
$P.Q^O.\tquo (E, D)$ \\
$P.Q^I.\tquo (E, D)$ 

\begin{description}
\item[]
\begin{tabbing}
$P$  \=\kill
$P$ \> = port formerly associated with channel end $E$. \\
$Q$ \> = port associated with partner of $E$. \\
$E$ \> = a channel end. \\
$D$ \> = access transfer channel.
\end{tabbing}
$\mysymbol{quo}$ output is in the alphabets of 
port $Q$, and the message delivery system.
$\mysymbol{quo}$ input is in the alphabets of port $P$ and
the message delivery system.
\end{description}
\end{linpar}

\section{The Channel-End Process}

     Associated with each $C$-channel are an input channel-end process
and an output channel-end process.  These processes are largely formal
devices, with no unique physical location.  Their alphabets incorporate the
events of the external interface of the $C$-channel.  They are responsible
for correct sequencing of the individual messages involved in communication
on the $C$-channel.

\subsection{Output channel-end}

\begin{linpar}
     The alphabet of an output channel end process $\tout (C)$ contains \\ \\
Control transfer events

\begin{description}
\item[]
\begin{tabbing}
$\any.\any^O.\tini (\tout (C), \any, \any, \any)$ \\
$\any.\any^I.\tini (\tout (C), \any, \any, \any)$
\end{tabbing}
\end{description}

Data transfer events

\begin{description}
\item[]
\begin{tabbing}
$C.U.\tdat \any$ \\
$\any.\any^O.\tdat (\any, C)$ \\
$\any.\any^I.\tack (C)$ \\
$U.C.\tack$
\end{tabbing}
\end{description}

Access transfer events

\begin{description}
\item[]
\begin{tabbing}
$C.U.\treq$ \\
$\any.\any^O.\treq (\any, C)$ \\
$\any.\any^I.\tini (\any, \any, \any, C)$ \\
$U.C.\tacs \any$
\end{tabbing}
\end{description}
\end{linpar}
\  \\ \\
In this alphabet, the data and access transfer events together will be
called ``communication events''.  Communication events excluding
the input events on channels $\any.\any^I$ will be called ``non-input
communication events''.  The traces of $\tout (C)$ satisfy
\begin{enumerate}
\item
The trace restricted to control transfer events and non-input events
(ie, excluding input communication events) is a prefix of a sequence
built from the atomic subsequences
\begin{description}
\item[]
\begin{tabbing}
$\langle c \rangle$, where $c$ is any non-input communication event, and \\
$ \langle \any.\any^O.\tini (\tout (C), \any, s, \any) \next
\any.\any^I.\tini (\tout (C), \any, \any, \any) \rangle $
\end{tabbing}
\end{description}
\item
The trace restricted to communication events is a prefix of
a sequence built from the atomic subsequences
\begin{description}
\item[]
\begin{tabbing}
$\langle C.U.\tdat (e) \next
\any.\any^O.\tdat (e, C) \next
\any.\any^I.\tack (C) \next
U.C.\tack \rangle $, and \\
$\langle C.U.\treq \next
\any.\any^O.\treq (R, C) \next
R.\any^I.\tini (F, \any, \any, C) \next
U.C.\tacs (F) \rangle $
\end{tabbing}
\end{description}
\item
If one of the atomic subsequences in 2 is interrupted by an $\tini $
output, the $s$ field in that output contains sufficient information
to determine how to resume the subsequence at the point of interruption.
\end{enumerate}

\subsection{Input channel-end}

\begin{linpar}
     The alphabet of an input channel end process $\tin (C)$ contains \\ \\
Control transfer events

\begin{description}
\item[]
\begin{tabbing}
$\any.\any^O.\tini (\tin (C), \any, \any, \any)$ \\
$\any.\any^I.\tini (\tin (C), \any, \any, \any)$
\end{tabbing}
\end{description}

Data transfer events

\begin{description}
\item[]
\begin{tabbing}
$\any.\any^I.\tdat (\any, C)$ \\
$U.C.\tdat \any$ \\
$C.U.\tack$ \\
$\any.\any^O.\tack (C)$
\end{tabbing}
\end{description}

Access transfer events

\begin{description}
\item[]
\begin{tabbing}
$\any.\any^I.\treq (\any, C)$ \\
$U.C.\treq$ \\
$C.U.\tacs \any$ \\
$\any.\any^O.\tchg (\any, \any, C)$
\end{tabbing}
\end{description}
\end{linpar}
\  \\ \\
The traces of $\tin (C)$ satisfy
\begin{enumerate}
\item
The trace restricted to control transfer events and non-input events
(ie, excluding input communication events) is a prefix of a sequence
built from the atomic subsequences
\begin{description}
\item[]
\begin{tabbing}
$\langle c \rangle$, where $c$ is any non-input communication event, and \\
$ \langle \any.\any^O.\tini (\tin (C), \any, s, \any) \next
\any.\any^I.\tini (\tin (C), \any, \any, \any) \rangle $
\end{tabbing}
\end{description}
\item
The trace restricted to communication events is a prefix of
a sequence built from the atomic subsequences
\begin{description}
\item[]
\begin{tabbing}
$\langle \any.\any^I.\tdat (e, C) \next 
U.C.\tdat (e) \next 
C.U.\tack \next 
\any.\any^O.\tack (C) \rangle$, and \\
$\langle \any.\any^I.\treq (R, C) \next
U.C.\treq \next
C.U.\tacs (F) \next
\any.\any^O.\tchg (F, R, C) \rangle$
\end{tabbing}
\end{description}
\item
(As for output channel-end).
\end{enumerate}
%\ \\

Requirement 1 implies that the only event that can occur between
output of an $\tini $ message and its subsequent receipt is
an input communication event.  During this interval the channel
end is ``moving'', and most types of event are disabled.
Inputs from the message system cannot be disabled here, because
(as it will turn out) this
would violate the important eager readership assumption.
Requirement 3 implies that resumption of a channel-end process
after moving to a different processor doesn't depend on any miraculous
non-local transfer of information.  For example, suppose the move of
an input channel-end, implied
by insertion of an $\tini $ subsequence, occurred after reception 
of a $\tdat (e, C)$ message from the message delivery system, but
before delivery of the datum $e$ to the user process.  The $s$ field
in the $\tini $ message would have to include the value of $e$.

Eventually it will be necessary to put some further restrictions
on these traces, to avoid other forms of non-locality.

\section{The Port Process}

     A port process may be ``initialised'' or ``uninitialised''.
An initialised port is associated from the outset with some channel
end $\tout (C)$ or $\tin (C)$.  It has a partner initialised port,
associated with opposite other channel end.  An uninitialised port starts
off in the ``free pool'' of ports.  Port $P$ is allocated from this pool
when it successfully engages in a $\any.\any^O.req (P, \any)$ event.

\begin{linpar}
     The alphabet of a port process $P$ contains \\ \\
Main control thread events

\begin{description}
\item[]
\begin{tabbing}
$\any.\any^O.\treq (P, \any)$ \\
$P.\any^I.\tini \any$ \\
$\any.P^O.\tini \any$
\end{tabbing}
\end{description}

Repointing events

\begin{description}
\item[]
\begin{tabbing}
$P.\any^I.\tchg \any$ \\
$\any.P^O.\tquo \any$ \\
$\any.P^O.\tchg \any$ \\
$P.\any^I.\tquo \any$
\end{tabbing}
\end{description}

Communication events

\begin{description}
\item[]
\begin{tabbing}
$\any.P^O.\tdat \any$ \\
$P.\any^I.\tack \any$ \\
$\any.P^O.\treq \any$ \\
$P.\any^I.\tdat \any$ \\
$\any.P^O.\tack \any$ \\
$P.\any^I.\treq \any$
\end{tabbing}
\end{description}
\end{linpar}
\  \\ \\
The traces of $P$ satisfy
\begin{enumerate}
\item
The trace restricted to main thread events and $\tchg$ output events
is a prefix of some sequence
\begin{description}
\item[]
\begin{tabbing}
$ \langle
\any.P^O.\tchg (\any, R, D) \next
R.P^O.\tini (\any, \any, \any, D) \rangle $
\end{tabbing}
\end{description}
if $P$ is an initialised port, or
\begin{description}
\item[]
\begin{tabbing}
$ \langle
\any.\any^O.req (P, \any) \next
P.\any^I.\tini \any \next
\any.P^O.\tchg (\any, R, D) \next
R.P^O.\tini (\any, \any, \any, D) \rangle $
\end{tabbing}
\end{description}
if it is uninitialised.
Moreover, $\treq (P, \any)$ output can only occur as the first event of the
full trace, and $\tini$ output can only occur as the last.
\item
In the trace restricted to $\tini $ input events and
output events on the channels $\any.P^O$,
an $\tini $ event can only appear in the first position of the sequence,
and a $\tchg $ output event can only appear in the last.
(ie, no outputs are initiated before initialisation, or after initiation
of a ``move'').
\item
The trace restricted to repointing events is a prefix of
a sequence built from any number of atomic subsequences of the form
\begin{description}
\item[]
\begin{tabbing}
$ \langle
P.Q^I.\tchg (E, \any, D) \next Q.P^O.\tquo (E, D)
\rangle $
\end{tabbing}
\end{description}
terminated by {\em one} subsequence from
\begin{description}
\item[]
\begin{tabbing}
$\langle \any.P^O.\tchg \any \next 
P.\any^I.\tquo \any \rangle$, \\
$\langle \any.P^O.\tchg \any \next 
P.\any^I.\tchg \any \rangle$, or
$\langle P.\any^I.\tchg \any \next 
\any.P^O.\tchg \any \rangle$
\end{tabbing}
\end{description}
All incoming $\tchg$ messages are acknowledged.  The three
possibilities for termination embody the only slightly subtle
part of the repointing protocol.
\item
In any event from
\nopagebreak
\begin{description}
\item[]
\begin{tabbing}
$Q.P^O.\tdat \any$ \\
$Q.P^O.\tack \any$ \\
$Q.P^O.\treq \any$ \\
$Q.P^O.\tchg \any$ \\
$\any.P^O.\tini (\any, Q, \any, \any)$
\end{tabbing}
\end{description}
appearing in a trace, the $Q$ field must have the same value as the
$Q$ field in the most recent preceding event of type
\begin{description}
\item[]
\begin{tabbing}
$P.\any^I.\tchg (Q, \any)$
\end{tabbing}
\end{description}
If there is no preceding $\tchg $ input, the $Q$ field must match
either the initial value for the partner port (if $P$ is initialised),
or the value
in the trace's (compulsory)
\begin{description}
\item[]
\begin{tabbing}
$P.\any^I.\tini (\any, Q, \any, \any)$
\end{tabbing}
\end{description}
event (if it is uninitialised).  These constraints impose that communications 
are always sent to the active partner port.
\item
The trace must be constructed from
\begin{description}
\item[]
\begin{tabbing}
$\any.\any^O.\treq (P, \any)$ \\
$P.\any^I.\tini (out (C), \any, \any, \any)$ \\
$\any.P^O.\tini (out (C), \any, \any, \any)$ \\
$P.\any^I.\tchg \any$ \\
$\any.P^O.\tchg (\any, out (C), \any)$ \\
$\any.P^O.\tdat (\any, C)$ \\
$P.\any^I.\tack (C)$ \\
$\any.P^O.\treq (\any, C)$
\end{tabbing}
\end{description}
or (exclusively) from
\begin{description}
\item[]
\begin{tabbing}
$\any.\any^O.\treq (P, \any)$ \\
$P.\any^I.\tini (in (C), \any, \any, \any)$ \\
$\any.P^O.\tini (in (C), \any, \any, \any)$ \\
$P.\any^I.\tchg \any$ \\
$\any.P^O.\tchg (\any, in (C), \any)$ \\
$\any.P^I.\tdat (\any, C)$ \\
$P.\any^O.\tack (C)$ \\
$\any.P^I.\treq (\any, C)$
\end{tabbing}
\end{description}
where the value of the $C$ field is common to all events in a trace.
(MISSING quo EVENTS HERE).
If $P$ is an initialised port with channel end $\tout (C)$ the first set
is applicable; if it is initialised with $\tin (C)$ the second set applies.
A port will only support one channel end throughout its life.
(IT'S LIKELY THAT I WANT TO REMOVE SOME UNNECESSARY RESTRICTIONS ON INPUT
EVENTS).

\end{enumerate}

\section{``Solving'' the Trace Restrictions}

%     Concentrate on some $C$-channel, $C$, and suppose that,
%in its lifetime, the $i + 1$th port associated with $\tout (C)$
%is $P_i$, and the $j + 1$th port associated with $\tin (C)$ is $Q_j$.
%Define the following subsequences of $C$'s trace, restricted to
%``control thread'' $\tini$, $\tchg$ and $\tquo$ events.

%$p^1_{ij} \concat p^2_{ij} \concat p^3_{ij} \concat p^4_{ij}$ is the
%expected sequence of events
%involved in moving $\tout (C)$ from $P_i$ to $P_{i + 1}$ if $\tin (C)$
%is stationary at $Q_j$.
%If $\tout (C)$ and $\tin (C)$ move simultaneously
%from $P_i$ to $P_{i + 1}$ and $Q_j$ to $Q_{j + 1}$ respectively,
%the expected sequence is some interleave of
%$p^1_{ij} \concat \overline{p}^4_{ij}$ and
%$q^1_{ij} \concat \overline{q}^4_{ij}$.

     Suppose $C$ is some channel name, and $\bvector{P}, \bvector{Q}$
are non-empty sequences of port names,
with $n = \seqsize \bvector{P}, m = \seqsize \bvector{Q}$.
Introduce the sets of event sequences:
\begin{eqnarray*}
\cal{P}^1_{ij} (D)
	       & = & \{ \langle
	       Q_j.P_i^O.\tchg (\tout (C), P_{i + 1}, D) \rangle \} \\ 
\cal{P}^2_{ij} (D)
	       & = & \{ \langle 
	       Q_j.P_i^I.\tchg (\tout (C), P_{i + 1}, D) \rangle \} \\ 
\cal{P}^3_{ij} (D)
	       & = & \{ \langle
	       P_i.Q_j^O.\tquo (\tout (C), D) \rangle \} \\
\cal{P}^4_{ij} (D)
	       & = & \{ \langle
		 P_i.Q_j^I.\tquo (\tout (C), D) \next \\&&
		P_{i + 1}.P_i^O.\tini (\tout (C), Q_j, s, D) \next \\&&
		P_{i + 1}.P_i^I.\tini (\tout (C), Q_j, s, D) \rangle
		\suchthat s \in \mysymbol{Contexts} \}
\end{eqnarray*}
for $0 \leq i < n - 1, 0 \leq j < m$, and
\begin{eqnarray*}
\cal{Q}^1_{ij} (D)
	       & = & \{ \langle
	       P_i.Q_j^O.\tchg (\tin (C), Q_{j + 1}, D) \rangle \} \\ 
\cal{Q}^2_{ij} (D)
	       & = & \{ \langle 
	       P_i.Q_j^I.\tchg (\tin (C), Q_{j + 1}, D) \rangle \} \\ 
\cal{Q}^3_{ij} (D)
	       & = & \{ \langle
	       Q_j.P_i^O.\tquo (\tin (C), D) \rangle \} \\
\cal{Q}^4_{ij} (D)
	       & = & \{ \langle
		 Q_j.P_i^I.\tquo (\tin (C), D) \next \\&&
		Q_{j + 1}.Q_j^O.\tini (\tin (C), P_i, s, D) \next \\&&
		Q_{j + 1}.Q_j^I.\tini (\tin (C), P_i, s, D) \rangle
		\suchthat s \in \mysymbol{Contexts} \}
\end{eqnarray*}
for $0 \leq i < n, 0 \leq j < m - 1$, and
\begin{eqnarray*}
\overline{\cal{P}}^4_{ij} (D, D')
	       & = & \{ \langle
		P_i.Q_j^I.\tchg (\tin (C), Q_{j + 1}, D') \next \\&&
		P_{i + 1}.P_i^O.\tini (\tout (C), Q_{j + 1}, s, D) \next \\&&
		P_{i + 1}.P_i^I.\tini (\tout (C), Q_{j + 1}, s, D) \rangle
		\suchthat s \in \mysymbol{Contexts} \} \\
\overline{\cal{Q}}^4_{ij} (D, D')
	       & = & \{ \langle
		Q_j.P_i^I.\tchg (\tout (C), P_{i + 1}, D) \next \\&&
		Q_{j + 1}.Q_j^O.\tini (\tin (C), P_{i + 1}, s, D') \next \\&&
		Q_{j + 1}.Q_j^I.\tini (\tin (C), P_{i + 1}, s, D') \rangle
		\suchthat s \in \mysymbol{Contexts} \}
\end{eqnarray*}
for $0 \leq i < n - 1, 0 \leq j < m - 1 $.
%Some abbreviations of these for fixed $C$, $\bvector{P}$ and $\bvector{Q}$:
%\begin{displaymath}
%\begin{array}{rcl}
%\cal{P}^1_{ij} (D) & = & \cal{S}^1_{ij} (C, \bvector{P}, \bvector{Q}, D) \\
%\cal{P}^2_{ij} (D) & = & \cal{S}^2_{ij} (C, \bvector{P}, \bvector{Q}, D) \\
%\cal{P}^3_{ij} (D) & = & \cal{S}^3_{ij} (C, \bvector{P}, \bvector{Q}, D) \\
%\cal{P}^4_{ij} (D) & = & \cal{S}^4_{ij} (C, \bvector{P}, \bvector{Q}, D) \\
%\overline{\cal{P}}^4_{ij} (D) & = &
%	      \overline{\cal{S}}^4_{ij} (C, \bvector{P}, \bvector{Q}, D)
%\end{array}
%\quad \quad
%\begin{array}{rcl}
%\cal{Q}^1_{ij} (D) & = & \cal{S}^1_{ji} (C, \bvector{Q}, \bvector{P}, D) \\
%\cal{Q}^2_{ij} (D) & = & \cal{S}^2_{ji} (C, \bvector{Q}, \bvector{P}, D) \\
%\cal{Q}^3_{ij} (D) & = & \cal{S}^3_{ji} (C, \bvector{Q}, \bvector{P}, D) \\
%\cal{Q}^4_{ij} (D) & = & \cal{S}^4_{ji} (C, \bvector{Q}, \bvector{P}, D) \\
%\overline{\cal{Q}}^4_{ij} (D) & = &
%	      \overline{\cal{S}}^4_{ji} (C, \bvector{Q}, \bvector{P}, D)
%\end{array}
%\end{displaymath}
Next, define recursively
\begin{eqnarray*}
\lefteqn{\cal{A}_{ij} (D) =} \\ &&
  \left(\bigcup_{D'} \cal {A}_{i - 1, j} (D')
		      \cal {P}^3_{i - 1, j} (D')
		      \cal {P}^4_{i - 1, j} (D')
		      \cal {P}^1_{ij} (D)
		      \cal {P}^2_{ij} (D)
		  \right) \cup \\ &&
  \left(\bigcup_{D'} \cal {B}_{i, j - 1} (D')
		      \cal {Q}^3_{i, j - 1} (D')
		      ((\cal {P}^1_{ij} (D)
		      \cal {P}^2_{ij} (D)) +
		      \cal {Q}^4_{i, j - 1} (D'))
		  \right) \cup \\ &&
  \left(\bigcup_{D', D''} \cal {C}_{i - 1, j - 1} (D', D'')
		      ((\overline{\cal {P}}^4_{i - 1, j - 1} (D')
		       \cal{P}^1_{ij} (D)
		       \cal{P}^2_{ij} (D)) +
		      \overline{\cal {Q}}^4_{i - 1, j - 1} (D''))
		  \right)
\end{eqnarray*}
for $0 \leq i < n - 1, 0 \leq j < m $, and
\begin{eqnarray*}
\lefteqn{\cal{B}_{ij} (D) =} \\ &&
  \left(\bigcup_{D'} \cal {A}_{i - 1, j} (D')
		      \cal {P}^3_{i - 1, j} (D')
		      (\cal {P}^4_{i - 1, j} (D') +
		      (\cal {Q}^1_{ij} (D)
		      \cal {Q}^2_{ij} (D)))
		  \right) \cup \\ &&
  \left(\bigcup_{D'} \cal {B}_{i, j - 1} (D')
		      \cal {Q}^3_{i, j - 1} (D')
		      \cal {Q}^4_{i, j - 1} (D')
		      \cal {Q}^1_{ij} (D)
		      \cal {Q}^2_{ij} (D)
		  \right) \cup \\ &&
  \left(\bigcup_{D', D''} \cal {C}_{i - 1, j - 1} (D', D'')
		      (\overline{\cal {P}}^4_{i - 1, j - 1} (D') +
		      (\overline{\cal {Q}}^4_{i - 1, j - 1} (D'')
		       \cal{Q}^1_{ij} (D)
		       \cal{Q}^2_{ij} (D)))
		  \right)
\end{eqnarray*}
for $0 \leq i < n, 0 \leq j < m - 1 $, and
\begin{eqnarray*}
\lefteqn{\cal{C}_{ij} (D, D') =} \\ &&
  \left(\bigcup_{D''} \cal {A}_{i - 1, j} (D'')
		      \cal {P}^3_{i - 1, j} (D'')
		    ((\cal {P}^4_{i - 1, j} (D'') \cal {P}^1_{ij} (D)) +
		      \cal {Q}^1_{ij} (D'))
		  \right) \cup \\ &&
  \left(\bigcup_{D''} \cal {B}_{i, j - 1} (D'')
		      \cal {Q}^3_{i, j - 1} (D'')
		     (\cal {P}^1_{ij} (D) +
		     (\cal {Q}^4_{i, j - 1} (D'') \cal {Q}^1_{ij} (D'))
		  \right) \cup \\ &&
   \left(\bigcup_{D'', D'''} \cal {C}_{i - 1, j - 1} (D'', D''')
	  ((\overline{\cal {P}}^4_{i - 1, j - 1} (D'') \cal {P}^1_{ij} (D)) +
	   (\overline{\cal {Q}}^4_{i - 1, j - 1} (D''') \cal {Q}^1_{ij} (D')))
                 \right)
\end{eqnarray*}
for $0 \leq i < n - 1, 0 \leq j < m - 1 $.
Here, juxtaposition of sequence sets implies concatentation
of elements, and `$+$' means interleaving of elements.
The conventions:
$\cal {A}_{-1,0} = \cal {B}_{0,-1} = \cal {C}_{-1,-1} =
\cal {P}^3_{-1,i} = \cal {P}^4_{-1,i} =
\overline{\cal {P}}^4_{-1, i - 1} =
\cal {Q}^3_{i, -1} = \cal {Q}^4_{i, -1} =
\overline{\cal {Q}}^4_{i - 1, -1} =
\{ \langle \rangle \}$ for $i \geq 0$, and
$\cal {A}_{-1,i} = \cal {B}_{-1,i} = \cal {C}_{-1,i - 1} =
\cal {A}_{i, -1} = \cal {B}_{i, -1} = \cal {C}_{i - 1, -1} = \emptyset $
for $i > 0$, supply the base cases for the recurrence.

     Finally we construct:
\begin{eqnarray*}
\lefteqn{\cal{M} (C, \bvector{P}, \bvector{Q}) =} \\ &&
  \left(\bigcup_{D} \cal {A}_{i - 1, j} (D)
		      \cal {P}^3_{i - 1, j} (D)
		      \cal {P}^4_{i - 1, j} (D)
		  \right) \cup \\ &&
  \left(\bigcup_{D} \cal {B}_{i, j - 1} (D)
		      \cal {Q}^3_{i, j - 1} (D)
		      \cal {Q}^4_{i, j - 1} (D)
		  \right) \cup \\ &&
   \left(\bigcup_{D, D'} \cal {C}_{i - 1, j - 1} (D, D')
                     (\overline{\cal {P}}^4_{i - 1, j - 1} (D) +
                      \overline{\cal {Q}}^4_{i - 1, j - 1} (D'))
                 \right)
\end{eqnarray*}
where $i = n - 1, j = m - 1$.

\end{document}
