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

\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$}}
\renewcommand{\symbol}[1]{\mbox{\it {#1}}}
\newcommand{\scriptsym}[1]{\mbox{\scriptsize \it {#1}}}
\newcommand{\function}[1]{\mbox{\it {#1}} \,}

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

\def\BigA{\mbox{\bf A}}
\def\BigT{\mbox{\bf T}}

\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{\symbol{ok}}
\def\tmes{\function{mes}}
\def\tchg{\function{chg}}
\def\tquo{\function{quo}}
\def\tin{\function{in}}
\def\tout{\function{out}}
\def\tfwd{\function{fwd}}
\def\tbwd{\function{bwd}}

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

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

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

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

\section{The $\symbol{Cstat}$ State Transition Model}

     $\Delta$ is a finite set of symbols:
\begin{eqnarray*}
\Delta & = & \{ \delta_{ij} \suchthat 3 \leq i < 6 \land 0 \leq j < 4 \} \cup
  \\ & & \{ \delta_{ij} \suchthat 0 \leq i < 4 \land 3 \leq j < 6 \} \cup
  \\ & & \{ \epsilon_{ij} \suchthat 0 \leq i < 6 \land 0 \leq j < 4 \} \cup
  \\ & & \{ \epsilon_{ij} \suchthat 0 \leq i < 4 \land 0 \leq j < 6 \}
\end{eqnarray*}
It's convenient to introduce a finite state transition model on $\Delta$.
This model has alphabet
\begin{eqnarray*}
    \BigA^\Delta & = & \{
       \begin{array}[t]{l}
	 c^O, c^I, c_-^I, q^O, q^I, i^O, i^I, \\
	 \overline{c}^O, \overline{c}^I, \overline{c}_-^I, \overline{q}^O,
	 \overline{q}^I, \overline{i}^O, \overline{i}^I \, \, \}
       \end{array}
\end{eqnarray*}
The transition function $\BigT^\Delta$ is given in figure \ref{Tdelta}.
In this diagram, all arcs are directed from left to right, or top to bottom.

\begin{figure}

\begin{center}

\begin{picture}(150, 200)(-10, -50)

\put( 13, 135){$q^I$}
\put( 38, 135){$i^O$}
\put( 63, 135){$i^I$}
\put( 88, 135){$c^O$}
\put(113, 135){$c^I$}
\put(113, 135){$c^I$}
\put(138, 135){$q^O$}

\put(-12, 112){$\overline{q}^I$}
\put(-12,  87){$\overline{i}^O$}
\put(-12,  62){$\overline{i}^I$}
\put(-12,  37){$\overline{c}^O$}
\put(-12,  12){$\overline{c}^I$}
\put(-12,  12){$\overline{c}^I$}
\put(-12, -17){$\overline{q}^O$}

\put(  0,   0){$\delta_{05}$}
\put( 25,   0){$\delta_{15}$}
\put( 50,   0){$\delta_{25}$}
\put( 75,   0){$\delta_{35}$}
\put(  0,  25){$\delta_{04}$}
\put( 25,  25){$\delta_{14}$}
\put( 50,  25){$\delta_{24}$}
\put( 75,  25){$\delta_{34}$}
\put(  0,  50){$\delta_{03}$}
\put( 25,  50){$\delta_{13}$}
\put( 50,  50){$\delta_{23}$}
\put( 75,  50){$\delta_{33}$}
\put(100,  50){$\delta_{43}$}
\put(125,  50){$\delta_{53}$}
\put( 75,  75){$\delta_{32}$}
\put(100,  75){$\delta_{42}$}
\put(125,  75){$\delta_{52}$}
\put( 75, 100){$\delta_{31}$}
\put(100, 100){$\delta_{41}$}
\put(125, 100){$\delta_{51}$}
\put( 75, 125){$\delta_{30}$}
\put(100, 125){$\delta_{40}$}
\put(125, 125){$\delta_{50}$}

\multiput(75, 50)(0, 25){4}{\multiput(13, 3)(25, 0){2}{\line(1,0){10}}}
\multiput(75, 50)(0, 25){3}{\multiput(4, 20)(25, 0){3}{\line(0,-1){10}}}

\multiput(0, 0)(0, 25){3}{\multiput(13, 3)(25, 0){3}{\line(1,0){10}}}
\multiput(0, 0)(0, 25){2}{\multiput(4, 20)(25, 0){4}{\line(0,-1){10}}}

\put(100,  25){$\epsilon_{00}$}
\put(88, 28){\vector(1,0){10}}
\put(104, 45){\vector(0,-1){10}}

\put(150,  50){$\delta_{03}$}
\put(138, 53){\vector(1,0){10}}

\put( 75, -25){$\delta_{30}$}
\put( 79, -5){\vector(0,-1){10}}

\end{picture}

\end{center}

\begin{center}

\begin{picture}(150, 200)(-10, -50)

\put( 13, 135){$\overline{c}_-^I$}
\put( 38, 135){$i^O$}
\put( 63, 135){$i^I$}
\put( 88, 135){$c^O$}
\put(113, 135){$c^I$}
\put(138, 135){$q^O$}

\put(-12, 112){$c_-^I$}
\put(-12,  87){$\overline{i}^O$}
\put(-12,  62){$\overline{i}^I$}
\put(-12,  37){$\overline{c}^O$}
\put(-12,  12){$\overline{c}^I$}
\put(-12, -17){$\overline{q}^O$}

\put(  0,   0){$\epsilon_{05}$}
\put( 25,   0){$\epsilon_{15}$}
\put( 50,   0){$\epsilon_{25}$}
\put( 75,   0){$\epsilon_{35}$}
\put(  0,  25){$\epsilon_{04}$}
\put( 25,  25){$\epsilon_{14}$}
\put( 50,  25){$\epsilon_{24}$}
\put( 75,  25){$\epsilon_{34}$}
\put(  0,  50){$\epsilon_{03}$}
\put( 25,  50){$\epsilon_{13}$}
\put( 50,  50){$\epsilon_{23}$}
\put( 75,  50){$\epsilon_{33}$}
\put(100,  50){$\epsilon_{43}$}
\put(125,  50){$\epsilon_{53}$}
\put(  0,  75){$\epsilon_{02}$}
\put( 25,  75){$\epsilon_{12}$}
\put( 50,  75){$\epsilon_{22}$}
\put( 75,  75){$\epsilon_{32}$}
\put(100,  75){$\epsilon_{42}$}
\put(125,  75){$\epsilon_{52}$}
\put(  0, 100){$\epsilon_{01}$}
\put( 25, 100){$\epsilon_{11}$}
\put( 50, 100){$\epsilon_{21}$}
\put( 75, 100){$\epsilon_{31}$}
\put(100, 100){$\epsilon_{41}$}
\put(125, 100){$\epsilon_{51}$}
\put(  0, 125){$\epsilon_{00}$}
\put( 25, 125){$\epsilon_{10}$}
\put( 50, 125){$\epsilon_{20}$}
\put( 75, 125){$\epsilon_{30}$}
\put(100, 125){$\epsilon_{40}$}
\put(125, 125){$\epsilon_{50}$}

\multiput(0, 50)(0, 25){4}{\multiput(13, 3)(25, 0){5}{\line(1,0){10}}}
\multiput(0, 50)(0, 25){3}{\multiput(4, 20)(25, 0){6}{\line(0,-1){10}}}

\multiput(0,  0)(0, 25){6}{\multiput(13, 3)(25, 0){3}{\line(1,0){10}}}
\multiput(0,  0)(0, 25){5}{\multiput(4, 20)(25, 0){4}{\line(0,-1){10}}}

\put(100,  25){$\epsilon_{00}$}
\put(88, 28){\vector(1,0){10}}
\put(104, 45){\vector(0,-1){10}}

\put(150,  50){$\delta_{03}$}
\put(138, 53){\vector(1,0){10}}

\put( 75, -25){$\delta_{30}$}
\put( 79, -5){\vector(0,-1){10}}

\end{picture}

\end{center}

\caption{\label{Tdelta} The $\Delta$ state transition function}

\end{figure}

     The transition model describing the history of a channel is an
``augmented'' version of this finite state model.
The state space $\symbol{Cstat}$ is a subset of
\begin{eqnarray*}
  \Delta & \times &
  \symbol{Ports}_\perp \times \symbol{Ports} \times \symbol{Ports}_\perp \times
  \symbol{Values}_\perp \times \\ & &
  \symbol{Ports}_\perp \times \symbol{Ports} \times \symbol{Ports}_\perp \times
  \symbol{Values}_\perp,
\end{eqnarray*}
namely
\begin{eqnarray*}
  \symbol{Cstat} & = &
    \{(d, P_-, P, P_+, u, Q_-, Q, Q_+, v) \suchthat \\ &&
    \, \, 
       ((d = \delta_{ij} \lor d = \epsilon_{ij}) \Rightarrow \\ &&
       \quad \quad (\begin{array}[t]{l}
	(i < 3 \Rightarrow P_- \in \symbol{Ports}) \land \\
	(4 \leq i \Rightarrow P_+ \in \symbol{Ports}) \land \\
	((i = 0) \lor (i = 2) \lor (i = 4)) \Rightarrow
			       u \in \symbol{Values}) \land \\
	(j < 3 \Rightarrow (Q_- \in \symbol{Ports}) \land \\
	(4 \leq j \Rightarrow (Q_+ \in \symbol{Ports}) \land \\
	((j = 0) \lor (j = 2) \lor (j = 4)) \Rightarrow
			       v \in \symbol{Values}) \, \, ))\land
	\end{array} \\ &&
    \, \, (d = \epsilon_{0j} \Rightarrow Q_- \in \symbol{Ports}) \land \\ &&
    \, \, (d = \epsilon_{i0} \Rightarrow P_- \in \symbol{Ports}) \}.
\end{eqnarray*}

The restrictions ensure that various fields don't
take the undefined value $\perp$ in various states---necessary
in the definition of the transition function.

%\begin{eqnarray*}
%  \symbol{Cstat} & = &
%    \{(d, P_-, P, P_+, G_-, G, u, Q_-, Q, Q_+, H_-, H, v) \suchthat \\ &&
%    \, \, 
%       ((d = \delta_{ij} \lor d = \epsilon_{ij}) \Rightarrow \\ &&
%       \quad \quad (\begin{array}[t]{l}
%	(i < 3 \Rightarrow (P_- \in \symbol{Ports} \land
%		 G_- \in \symbol{Halfs} )) \land \\
%	(4 \leq i \Rightarrow (P_+ \in \symbol{Ports} \land
%		 G \in \symbol{Halfs} )) \land \\
%	(j < 3 \Rightarrow (Q_- \in \symbol{Ports} \land
%		 H_- \in \symbol{Halfs} )))) \land \\
%	(4 \leq j \Rightarrow (Q_+ \in \symbol{Ports} \land
%		 H \in \symbol{Halfs} \, \, ))\land
%	\end{array} \\ &&
%    \, \, d = \epsilon_{ji} \Rightarrow
%       (\begin{array}[t]{l}
%	(i = 0 \Rightarrow (Q_- \in \symbol{Ports} \land H_- \in Halfs)) \land \\
%	(j = 0 \Rightarrow (P_- \in \symbol{Ports} \land G_- \in Halfs))\, \,) \land 
%	\end{array} \\ &&
%    \, \, (\exists S_P \cdot \exists S_Q \cdot
%       S_P \cap S_Q = \emptyset \land \\ &&
%       \quad ((d = \delta_{ij} \lor d = \epsilon_{ij}) \Rightarrow \\ &&
%       \quad \quad (\begin{array}[t]{l}
%	(i < 2 \Rightarrow ( P_- \not= P \land
%		  S_P = \{P_-, P\})) \land \\
%	(2 <= i < 4 \Rightarrow ( S_P = \{P\})) \land \\
%	(4 \leq i \Rightarrow (P_+ \not= P \land S_P = \{P, P_+\})) \land \\
%	(j < 2 \Rightarrow ( Q_- \not= Q \land
%		  S_Q = \{Q_-, Q\})) \land \\
%	(2 <= j < 4 \Rightarrow ( S_Q = \{Q\})) \land \\
%	(4 \leq j \Rightarrow (Q_+ \not= Q \land S_Q = \{Q, Q_+\})) \, \, ))) \}
%	\end{array}
%\end{eqnarray*}
%
%The complicated restrictions ensure that various fields don't
%take the undefined value $\perp$ in various states---necessary
%in the definition of the transition function---and that various
%port fields take distinct values.  The latter conditions
%will be needed for setting
%up the bisimulation with the port-oriented description.  It isn't
%essential to put these constraints in the definition of the state
%space---they could appear alternatively
%in the definition of the domain for the bisimulation.
%This would simplify the definition of the $\symbol{Cstat}$ at the
%price, obviously, of complicating the definition of the bisimulation.

     The alphabet of a $\symbol{Cstat}$ system associated with
$C \in \symbol{Chans}$ is
\begin{eqnarray*}
    \BigA^{\scriptsym{Cstat}}_C & = & \{
       \begin{array}[t]{ll}
		(\any, \any)^O.\tmes (E, \any), \\
		(\any, \any)^O.\tmes (\overline{E}, \any), \\
		(\any, \any)^O.\tini (E, \any, \any), &
		(\any, \any)^I.\tini (E, \any, \any), \\
		(\any, \any)^O.\tini (\overline{E}, \any, \any), &
		(\any, \any)^I.\tini (\overline{E}, \any, \any), \\
		(\any, \any)^O.\tchg (E, \any, \any), &
		(\any, \any)^I.\tchg (E, \any, \any), \\
		(\any, \any)^O.\tchg (\overline{E}, \any, \any), &
		(\any, \any)^I.\tchg (\overline{E}, \any, \any), \\
		(\any, \any)^O.\tquo (E, \any), &
		(\any, \any)^I.\tquo (E, \any), \\
		(\any, \any)^O.\tquo (\overline{E}, \any), &
		(\any, \any)^I.\tquo (\overline{E}, \any) \, \, \}.
       \end{array}
\end{eqnarray*}
where $E = \tout (C)$, $\overline{E} = \tin (C)$.

The transition function is
\begin{eqnarray*}
\lefteqn{\BigT^{\scriptsym{Cstat}}_C (d, P^-, P, P^+, u,
				       Q^-, Q, Q^+, v) = } \\ &&
\{ ((Q, P)^O.\tmes (E, \any) \mapsto
   (d, P^-, P, P^+, u, Q^-, Q, Q^+, v)) \suchthat \\ &&
   \hspace{2in} (d = \delta_{3i} \lor d = \epsilon_{3i}) \land 0
		 \leq i < 5 \} \cup \\ &&
\{ ((Q^+, P)^O.\tmes (\overline{E}, \any) \mapsto
   (d, P^-, P, P^+, u, Q^-, Q, Q^+, v)) \suchthat \\ &&
   \hspace{2in} d = \delta_{35} \lor d = \epsilon_{35} \} \cup \\ &&
\{ ((Q, P)^O.\tchg (E, {P^+}', u') \mapsto
   (d', P^-, P, {P^+}', u', Q^-, Q, Q^+, v)) \suchthat \\ &&
   \hspace{2in} (c^O \mapsto d') \in \BigT^\Delta (d) \land
		 d' \not = \epsilon_{00}\} \cup \\ &&
\{ ((Q, P)^O.\tchg (E, {P^+}', u') \mapsto
   (d', P, {P^+}', \perp, v, Q, Q^+, \perp, u')) \suchthat \\ &&
   \hspace{2in} (c^O \mapsto d') \in \BigT^\Delta (d) \land
		 d' = \epsilon_{00}\} \cup \\ &&
\{ ((Q, P)^I.\tchg (E, P^+, u) \mapsto
   (d', P^-, P, P^+, \perp, Q^-, Q, Q^+, v)) \suchthat \\ &&
   \hspace{2in} (c^I \mapsto d') \in \BigT^\Delta (d) \} \cup \\ &&
\{ ((Q^-, P^-)^I.\tchg (E, P, v) \mapsto
   (d', P^-, P, P^+, u, Q^-, Q, Q^+, \perp)) \suchthat \\ &&
   \hspace{2in} (c_-^I \mapsto d') \in \BigT^\Delta (d) \} \cup \\ &&
\{ ((P, Q)^O.\tquo (E, u') \mapsto
   (d', P, P^+, \perp, u', Q^-, Q, Q^+, v)) \suchthat \\ &&
   \hspace{2in} (q^O \mapsto d') \in \BigT^\Delta (d) \} \cup \\ &&
\{ ((P^-, Q)^I.\tquo (E, u) \mapsto
   (d', P^-, P, P^+, \perp, Q^-, Q, Q^+, v)) \suchthat \\ &&
   \hspace{2in} (q^I \mapsto d') \in \BigT^\Delta (d) \} \cup \\ &&
\{ ((P, P^-)^O.\tini (E, Q, u') \mapsto
   (d', P^-, P, P^+, u', Q^-, Q, Q^+, v)) \suchthat \\ &&
   \hspace{2in} (i^O \mapsto d') \in \BigT^\Delta (d) \} \cup \\ &&
\{ ((P, P^-)^I.\tini (E, Q, u) \mapsto
   (d', P^-, P, P^+, \perp, Q^-, Q, Q^+, v)) \suchthat \\ &&
   \hspace{2in} (i^I \mapsto d') \in \BigT^\Delta (d) \} \cup \\ &&
\{ ((P, Q)^O.\tmes (\overline{E}, \any) \mapsto
   (d, P^-, P, P^+, u, Q^-, Q, Q^+, v)) \suchthat \\ &&
   \hspace{2in} (d = \delta_{j3} \lor d = \epsilon_{j3}) \land
		 0 \leq j < 5 \} \cup \\ &&
\{ ((P^+, Q)^O.\tmes (\overline{E}, \any) \mapsto
   (d, P^-, P, P^+, u, Q^-, Q, Q^+, v)) \suchthat \\ &&
   \hspace{2in} d = \delta_{53} \lor d = \epsilon_{53} \} \cup \\ &&
\{ ((P, Q)^O.\tchg (\overline{E}, {Q^+}', v') \mapsto
   (d', P^-, P, P^+, u, Q^-, Q, {Q^+}', v')) \suchthat \\ &&
   \hspace{2in} (\overline{c}^O \mapsto d') \in \BigT^\Delta (d) \land
		 d' \not = \epsilon_{00}\} \cup \\ &&
\{ ((P, Q)^O.\tchg (\overline{E}, {Q^+}', v') \mapsto
   (d', P, P^+, \perp, v', Q, {Q^+}', \perp, u)) \suchthat \\ &&
   \hspace{2in} (\overline{c}^O \mapsto d') \in \BigT^\Delta (d) \land
		 d' = \epsilon_{00}\} \cup \\ &&
\{ ((P, Q)^I.\tchg (\overline{E}, Q^+, v) \mapsto
   (d', P^-, P, P^+, u, Q^-, Q, Q^+, \perp)) \suchthat \\ &&
   \hspace{2in} (\overline{c}^I \mapsto d') \in \BigT^\Delta (d) \} \cup \\ &&
\{ ((P^-, Q^-)^I.\tchg (\overline{E}, Q, u) \mapsto
   (d', P^-, P, P^+, \perp, Q^-, Q, Q^+, v)) \suchthat \\ &&
   \hspace{2in} (\overline{c}_-^I \mapsto d') \in \BigT^\Delta (d) \} \cup \\ &&
\{ ((Q, P)^O.\tquo (\overline{E}, v') \mapsto
   (d', P^-, P, P^+, u, Q, Q^+, \perp, v')) \suchthat \\ &&
   \hspace{2in} (\overline{q}^O \mapsto d') \in \BigT^\Delta (d) \} \cup \\ &&
\{ ((Q^-, P)^I.\tquo (\overline{E}, v) \mapsto
   (d', P^-, P, P^+, u, Q^-, Q, Q^+, \perp)) \suchthat \\ &&
   \hspace{2in} (\overline{q}^I \mapsto d') \in \BigT^\Delta (d) \} \cup \\ &&
\{ ((Q, Q^-)^O.\tini (\overline{E}, P, v') \mapsto
   (d', P^-, P, P^+, u, Q^-, Q, Q^+, v')) \suchthat \\ &&
   \hspace{2in} (\overline{i}^O \mapsto d') \in \BigT^\Delta (d) \} \cup \\ &&
\{ ((Q, Q^-)^I.\tini (\overline{E}, P, v) \mapsto
   (d', P^-, P, P^+, u, Q^-, Q, Q^+, \perp)) \suchthat \\ &&
   \hspace{2in} (\overline{i}^I \mapsto d') \in \BigT^\Delta (d) \}.
\end{eqnarray*}

The elements of the bisimulation between the $\symbol{Cstat}$ system
and the $\symbol{Pstat}$, $\symbol{Mstat}$ system are the partial functions
$\widetilde{p}^s$, $\widetilde{m}^s$.
these functions are defined in the tables of figures
\ref{ptilda} and \ref{mtilda}.
Here, $\eta$ means $\delta$ {\em or} $\epsilon$.
In figure \ref{ptilda}, $i$ and $j$ run from $0$ to $4$;
in figure \ref{mtilda} they run from $0$ to $5$.

\begin{figure}

\begin{center}

\begin{tabular}{|c|c|c|c|}
\hline
$ d $ &
$\widetilde{p}^s (P^-)$ &
$\widetilde{p}^s (P)$ &
$\widetilde{p}^s (P^+)$ \\
\hline
\hline
$ \epsilon_{0j} $ &
$ \pi_2 (E, Q^-, P) $ &
$ \pi_0 $ &
\\
\hline
$ \delta_{0j} $ &
$ \pi_2 (E, Q, P) $ &
$ \pi_0 $ &
\\
\hline
$ \eta_{1j} $ &
$ \pi_3 (E, Q, P) $ &
$ \pi_0 $ &
\\
$ \eta_{2j} $ &
&
$ \pi_0 $ &
\\
$ \eta_{3j} $ &
&
$ \pi_1 (E, Q) $ &
\\
$ \eta_{4j} $ &
&
$ \pi_2 (E, Q, P^+) $ &
$ \pi_0 $ \\
$ \eta_{5j} $ &
&
$ \pi_2 (E, Q, P^+) $ &
$ \pi_0 $ \\
\hline
\hline
$ \epsilon_{05} $ &
$ \pi_2 (E, Q^-, P) $ &
$ \pi_0' (Q^+, Q) $ &
\\
\hline
$ \delta_{05} $ &
$ \pi_2 (E, Q, P) $ &
$ \pi_0' (Q^+, Q) $ &
\\
\hline
$ \eta_{15} $ &
$ \pi_3 (E, Q, P) $ &
$ \pi_0' (Q^+, Q) $ &
\\
$ \eta_{25} $ &
&
$ \pi_0' (Q^+, Q) $ &
\\
$ \eta_{35} $ &
&
$ \pi_1' (E, Q^+, Q) $ &
\\
\hline
\end{tabular}

\end{center}

\begin{center}

\begin{tabular}{|c|c|c|c|}
\hline
$ d $ &
$\widetilde{p}^s (Q^-)$ &
$\widetilde{p}^s (Q)$ &
$\widetilde{p}^s (Q^+)$ \\
\hline
\hline
$ \epsilon_{i0} $ &
$ \pi_2 (\overline{E}, P^-, Q) $ &
$ \pi_0 $ &
\\
\hline
$ \delta_{i0} $ &
$ \pi_2 (\overline{E}, P, Q) $ &
$ \pi_0 $ &
\\
\hline
$ \eta_{i1} $ &
$ \pi_3 (\overline{E}, P, Q) $ &
$ \pi_0 $ &
\\
$ \eta_{i2} $ &
&
$ \pi_0 $ &
\\
$ \eta_{i3} $ &
&
$ \pi_1 (\overline{E}, P) $ &
\\
$ \eta_{i4} $ &
&
$ \pi_2 (\overline{E}, P, Q^+) $ &
$ \pi_0 $ \\
$ \eta_{i5} $ &
&
$ \pi_2 (\overline{E}, P, Q^+) $ &
$ \pi_0 $ \\
\hline
\hline
$ \epsilon_{50} $ &
$ \pi_2 (\overline{E}, P^-, Q) $ &
$ \pi_0' (P^+, P) $ &
\\
\hline
$ \delta_{50} $ &
$ \pi_2 (\overline{E}, P, Q) $ &
$ \pi_0' (P^+, P) $ &
\\
\hline
$ \eta_{51} $ &
$ \pi_3 (\overline{E}, P, Q) $ &
$ \pi_0' (P^+, P) $ &
\\
$ \eta_{52} $ &
&
$ \pi_0' (P^+, P) $ &
\\
$ \eta_{53} $ &
&
$ \pi_1' (\overline{E}, P^+, P) $ &
\\
\hline
\end{tabular}

\end{center}

\caption{\label{ptilda} The partial function $\widetilde{p}^s$
for $s = (d, P^-, P, P^+, u, Q^-, Q, Q^+, v)$}

\end{figure}

\begin{figure}

\begin{center}

\begin{tabular}{|c|c|c|c|c|}
\hline
$ d $ &
$\widetilde{m}^s (P^-, Q^-)$ &
$\widetilde{m}^s (P^-, Q)$ &
$\widetilde{m}^s (P, P^-)$ &
$\widetilde{m}^s (Q, P)$ \\
\hline
\hline
$ \epsilon_{0j} $ &
$ \langle \tchg (\overline{E}, Q, u) \rangle $ &
 &
 &
 \\
\hline
$ \delta_{0j} $ &
 &
$ \langle \tquo (E, u) \rangle $ &
 &
 \\
\hline
$ \eta_{1j} $ &
 &
 &
$ \langle \rangle $ &
 \\
$ \eta_{2j} $ &
 &
 &
$ \langle \tini (E, Q, u) \rangle $ &
 \\
$ \eta_{3j} $ &
 &
 &
 &
$ \langle \rangle $ \\
$ \eta_{4j} $ &
 &
 &
 &
$ \langle \tchg (E, P^+, u) \rangle $ \\
$ \eta_{5j} $ &
 &
 &
 &
 \\
\hline
\end{tabular}

\end{center}

\begin{center}

\begin{tabular}{|c|c|c|c|c|}
\hline
$ d $ &
$\widetilde{m}^s (Q^-, P^-)$ &
$\widetilde{m}^s (Q^-, P)$ &
$\widetilde{m}^s (Q, Q^-)$ &
$\widetilde{m}^s (P, Q)$ \\
\hline
\hline
$ \epsilon_{i0} $ &
$ \langle \tchg (E, P, v) \rangle $ &
 &
 &
 \\
\hline
$ \delta_{i0} $ &
&
$ \langle \tquo (\overline{E}, v) \rangle $ &
 &
 \\
\hline
$ \eta_{i1} $ &
 &
 &
$ \langle \rangle $ &
 \\
$ \eta_{i2} $ &
 &
 &
$ \langle \tini (\overline{E}, P, v) \rangle $ &
 \\
$ \eta_{i3} $ &
 &
 &
 &
$ \langle \rangle $ \\
$ \eta_{i4} $ &
 &
 &
 &
$ \langle \tchg (\overline{E}, Q^+, v) \rangle $ \\
$ \eta_{i5} $ &
 &
 &
 &
 \\
\hline
\end{tabular}

\end{center}

\caption{\label{mtilda} The partial function $\widetilde{m}^s$
for $s = (d, P^-, P, P^+, u, Q^-, Q, Q^+, v)$}

\end{figure}

%\begin{figure}
%
%\begin{center}
%
%\begin{tabular}{|c|c|c|c|c|c|}
%\hline
%$ d $ &
%$\widetilde{m}^s (P^-, Q^-)$ &
%$\widetilde{m}^s (P^-, Q)$ &
%$\widetilde{m}^s (P, P^-)$ &
%$\widetilde{m}^s (Q, P)$ &
%$\widetilde{m}^s (P^+, Q)$ \\
%\hline
%\hline
%$ \epsilon_{0j} $ &
%$ \langle \tchg (\overline{E}, Q, u) \rangle $ &
% &
% &
% &
% \\
%\hline
%$ \delta_{0j} $ &
% &
%$ \langle \tquo (E, u) \rangle $ &
% &
% &
% \\
%\hline
%$ \eta_{1j} $ &
% &
% &
%$ \langle \rangle $ &
% &
% \\
%$ \eta_{2j} $ &
% &
% &
%$ \langle \tini (E, Q, u) \rangle $ &
% &
% \\
%$ \eta_{3j} $ &
% &
% &
% &
%$ \langle \rangle $ &
% \\
%$ \eta_{4j} $ &
% &
% &
% &
%$ \langle \tchg (E, P^+, u) \rangle $ &
% \\
%$ \eta_{5j} $ &
% &
% &
% &
% &
%$ \langle \rangle $ \\
%\hline
%\end{tabular}
%
%\end{center}
%
%\begin{center}
%
%\begin{tabular}{|c|c|c|c|c|c|}
%\hline
%$ d $ &
%$\widetilde{m}^s (Q^-, P^-)$ &
%$\widetilde{m}^s (Q^-, P)$ &
%$\widetilde{m}^s (Q, Q^-)$ &
%$\widetilde{m}^s (P, Q)$ &
%$\widetilde{m}^s (Q^+, P)$ \\
%\hline
%\hline
%$ \epsilon_{i0} $ &
%$ \langle \tchg (E, P, v) \rangle $ &
% &
% &
% &
% \\
%\hline
%$ \delta_{i0} $ &
%&
%$ \langle \tquo (\overline{E}, v) \rangle $ &
% &
% &
% \\
%\hline
%$ \eta_{i1} $ &
% &
% &
%$ \langle \rangle $ &
% &
% \\
%$ \eta_{i2} $ &
% &
% &
%$ \langle \tini (\overline{E}, P, v) \rangle $ &
% &
% \\
%$ \eta_{i3} $ &
% &
% &
% &
%$ \langle \rangle $ &
% \\
%$ \eta_{i4} $ &
% &
% &
% &
%$ \langle \tchg (\overline{E}, Q^+, v) \rangle $ &
% \\
%$ \eta_{i5} $ &
% &
% &
% &
% &
%$ \langle \rangle $ \\
%\hline
%\end{tabular}
%
%\end{center}
%
%\caption{\label{mtilda} The partial function $\widetilde{m}^s$
%for $s = (d, P^-, P, P^+, u, Q^-, Q, Q^+, v)$}
%
%\end{figure}

\end{document}

