\section{Models for message-routers.}

     A message delivery system is regarded as a process which accepts
messages from a system of user processes, and delivers messages to
the user system.  A few properties are desirable {\em a priori}.
For example, the system shouldn't deliver messages which it hasn't
previously accepted---it shouldn't generate spurious messages.
Similarly, I'll assume that it doesn't duplicate messages---for
each message accepted, at most one is delivered.  Needless to say,
many useful message delivery systems don't guarantee
either of these properties.  However they do seem to be reasonable
requirements in the context of tightly-coupled MIMD systems.
It isn't difficult for hardware-assisted routing systems to
implement these specifications.

     Ignoring, for the moment only, liveness properties of the message
delivery system, the simplest structure which meets these requirements
is the {\em bag} \cite{mail}.  Assume the set of message types is
$\symbol{Values}$.  The alphabet of the bag is
\begin{displaymath}
\alpha{\symbol{Bag}} = \{\underline{v}^O \suchthat \underline{v} \in \symbol{Values}, \quad
		         \underline{v}^I \suchthat \underline{v} \in \symbol{Values} \}.
\end{displaymath}
The event $v^O$ corresponds to output of a message holding value $v$
from the user to the delivery system.  $v^I$ corresponds to it's
input (delivery of the message).  According to the discussion in
the previous paragraph any trace $\symbol{tr}$ of $\symbol{Bag}$
should satisfy
\begin{displaymath}
\forall v:\symbol{Values}. \quad \symbol{tr} \downarrow \{ v^O \} \geq
                                 \symbol{tr} \downarrow \{ v^I \}
\end{displaymath}
In fact, so far as traces are concerned, this is the strongest
specification needed to yield a workable message delivery system.
One can also give a state transition model of this trace set.
The state space is
\begin{displaymath}
\symbol{Bstat} = \symbol{Values} \rightarrow \symbol{Nat}
\end{displaymath}
A state $B$ in this space associates a non-negative value with each
message type---$B (v)$ is the number of messages of type $v$ presently
in transit.  The transition function is
\begin{eqnarray*}
T^{\scriptsym{Bstat}} (B) & = &
    \{ (\underline{v}^O \mapsto B \oplus (\underline{v} \mapsto B (\underline{v}) + 1)), \\ && \,\,\,\,
       (\underline{v}^I \mapsto B \oplus (\underline{v} \mapsto B (\underline{v}) - 1))
	     \suchthat B (\underline{v}) \neq 0 \}.
\end{eqnarray*}
The important property of this transition function is that an event $v^I$ can
only occur when there are some messages of type $v$ in transit.
The required trace set is generated from the initial state $B = 0$.
To show that this system meets the specification above, one can use
the result in section \ref{sec:TMspec} with
\begin{eqnarray*}
\dom {\cal S} & = & \{ \setvar{s} \suchthat
  \forall s \truethat s \leq \setvar{s} \Rightarrow
	      (\forall v. B_s (v) \geq 0) \} \\
{\cal S} (s) & = & B_s, \mbox{ if } s \in \dom {\cal S}
\end{eqnarray*}
where $B_s (v) = 
\symbol{s} \downarrow \{ v^O \} - \symbol{s} \downarrow \{ v^I \}$.

     This specification of the system's traces embodies the ``safety''
properties demanded in the opening paragraph of this section.
It says nothing about ``liveness''.  The ideal router would be a
deterministic process with the specified traces.  This system
would never refuse any event offered by the enviroment so long
as the event was engagable according to the trace specification.
The only events it ever refused would be those inputs corresponding
to messages which hadn't yet been sent.  It would always accept
any output, and at any time it would be prepared to deliver any
message it currently held (at least, it would deliver any such message
in bounded time, without conditions on whether
the user was refusing to input some other set of messages also in transit).
No real message delivery system has these properties because they
depend on the availability of infinite buffering.  Infinite buffering
can be approximated, up to a point, by, say, having {\em large}
buffers permanently allocated, which is costly in memory,
or by dynamically allocating memory to buffers as required, which
is costly in processor time.  This rules out such schemes out for
the purposes of this article.

     What is the minimal set of liveness properties for a useful
delivery system?  Certainly, if the delivery system is empty
(no message in transit), we would expect it to be prepared to
accept any message.  It might sometimes refuse to accept outputs
if there {\em are} messages in transit, because some buffers may have
filled up.  Secondly, if there {\em are} messages in
transit, we would expect it to be willing to deliver at least one
of them \footnote{This property may not be satisfied if the
delivery system is prone to internal deadlock.}.  However, we
will accept that delivery of some messages in transit may
be deferred pending delivery of some other messages, also
in transit, due to some internal forwarding buffers being occupied.

     These minimal requirements are embodied in the (failures model)
specification
\begin{eqnarray*}
\symbol{tr} \in \function{traces} (\symbol{Bag}) & \land &
(\bif (\forall v:\symbol{Values}. \quad \symbol{tr} \downarrow \{ v^O \} =
                                 \symbol{tr} \downarrow \{ v^I \})
\bthen \\ &&
\quad\,\,\, (\forall v:\symbol{Values}. \quad v^O \not\in \symbol{ref}) \belse \\ &&
\quad\,\,\, (\exists v:\symbol{Values}. \quad
      \symbol{tr} \downarrow \{ v^O \} >
      \symbol{tr} \downarrow \{ v^I \} \,\, \land \,\,
      v^I \not\in \symbol{ref}))
\end{eqnarray*}
This asserts that the traces of the system are those described above,
and that if there are no messages in transit, no refusal
state refuses any output event; otherwise, in any refusal state there
is (at least) one input event corresponding to a message in transit
which won't be refused.

     An acceptance transition model defining a process which
satisfies this specification
is $(\alpha \symbol{Bag}, \symbol{Bstat}, T^{\scriptsym{Bstat}}, 
W^{\scriptsym{Bstat}})$ where
\begin{displaymath}
W^{\scriptsym{Bstat}} (B) =
     \{
     \{\setvar{v}^I\} \suchthat B (\setvar{v}) > 0 \next
     \{
      \setvar{\setvar{v}}^I \suchthat B (\setvar{\setvar{v}}) > 0
     \next
     \setvar{\setvar{v}}^O
     \}
     \}
\end{displaymath}
%		\{\{\underline{v}^I\} \suchthat B (\underline{v}) > 0\} \cup
%     \{\{\underline{\underline{v}}^O\} \cup
%      \{\underline{\underline{v}}^I \suchthat B (\underline{\underline{v}}) > 0
%     \}\}
(ie, $W^{\scriptsym{Bstat}} (B)$ contains
singleton sets corresponding to each input event for which
$B (v) > 0$, and a set containing all input events satisfying the
same condition together with all output events).
This can be proven immediately using the result in section \ref{sec:ATMspec}.

\subsection{``Virtual Channels'' Implemented on a Message-Router}

     Suppose
\begin{displaymath}
\symbol{Message} = \{\setvar{c}.f.\setvar{x} \suchthat
	 \setvar{c} \in \symbol{Chans} \land \setvar{x} \in \symbol{Values}
		     \next
                     \setvar{c}.b.\setvar{x} \suchthat
	 \setvar{c} \in \symbol{Chans} \land \setvar{x} \in \symbol{Values} \}.
\end{displaymath}
Consider the following putative implementation of a virtual channel system:
\begin{displaymath}
\begin{array}{l}
\left(
\left( \begin{array}{c} \Parallel \\ c \in \symbol{Chans} \end{array} c:\symbol{OBUF} \right) \parallel
\right. \\ \left. \,\,\,\,
\left( \begin{array}{c} \Parallel \\ c \in \symbol{Chans} \end{array} c:\symbol{IBUF}  \right) \parallel
\function{BAG}
\right) \setminus H
\end{array}
\end{displaymath}
The system of input and output buffers is modelled by the TM 
$(A^{\scriptsym{IO}}, S^{\scriptsym{IO}}, T^{\scriptsym{IO}})$,
where
\def\setc{\setvar{c}}
\def\setx{\setvar{x}}
\begin{eqnarray*}
A^{\scriptsym{IO}} & = &
	\{ \setc.p.\setx \next   \setc.f.\setx^O \next
	   \setc.f.\setx^I \next \setc.q.\setx \next
	   \setc.r.\setx \next   \setc.b.\setx^O \next
	   \setc.b.\setx^I \next \setc.s.\setx \} \\
S^{\scriptsym{IO}} & = &
	(\symbol{Chans} \rightarrow S^O) \times (\symbol{Chans} \rightarrow S^I)
\end{eqnarray*}
and
\begin{eqnarray*}
\lefteqn{T^{\scriptsym{IO}} (O, I) =} \\ &&
\{
\begin{array}[t]{ll}
(\setc.p.\setx \mapsto (O \oplus \{(\setc \mapsto \alpha_1 (\setx))\}, I))
& \suchthat O (\setc) = \alpha_0, \\
(\setc.f.\setx^O \mapsto (O \oplus \{(\setc \mapsto \alpha_2)\}, I))
& \suchthat O (\setc) = \alpha_1 (\setx), \\
(\setc.f.\setx^I \mapsto (O, I \oplus \{(\setc \mapsto \alpha_1 (\setx))\}))
& \suchthat I (\setc) = \alpha_0, \\
(\setc.q.\setx \mapsto (O, I \oplus \{(\setc \mapsto \alpha_2)\}))
& \suchthat I (\setc) = \alpha_1 (\setx), \\
(\setc.r.\setx \mapsto (O, I \oplus \{(\setc \mapsto \alpha_3 (\setx))\}))
& \suchthat I (\setc) = \alpha_2, \\
(\setc.b.\setx^O \mapsto (O, I \oplus \{(\setc \mapsto \alpha_0)\}))
& \suchthat I (\setc) = \alpha_3 (\setx), \\
(\setc.b.\setx^I \mapsto (O \oplus \{(\setc \mapsto \alpha_3 (\setx))\}, I))
& \suchthat O (\setc) = \alpha_2, \\
(\setc.s.\setx \mapsto (O \oplus \{(\setc \mapsto \alpha_0)\}, I))
& \suchthat O (\setc) = \alpha_3 (\setx) \, \, \}
\end{array}
\end{eqnarray*}
The initial state is
$(\{(\any \mapsto \alpha_0)\} \next \{(\any \mapsto \alpha_0)\})$.
Hence
\begin{eqnarray*}
\lefteqn{\dom T^{\scriptsym{IO}} (O, I) =} \\ &&
\{
\begin{array}[t]{ll}
\setc.p.\setx & \suchthat O (\setc) = \alpha_0, \\
\setc.f.\setx^O & \suchthat O (\setc) = \alpha_1 (\setx), \\
\setc.f.\setx^I & \suchthat I (\setc) = \alpha_0, \\
\setc.q.\setx & \suchthat I (\setc) = \alpha_1 (\setx), \\
\setc.r.\setx & \suchthat I (\setc) = \alpha_2, \\
\setc.b.\setx^O & \suchthat I (\setc) = \alpha_3 (\setx), \\
\setc.b.\setx^I & \suchthat O (\setc) = \alpha_2, \\
\setc.s.\setx & \suchthat O (\setc) = \alpha_3 (\setx) \, \, \}.
\end{array}
\end{eqnarray*}
Now we need to calculate
$\dom T^{\scriptsym{IO}} (O, I) 
\paracc{A^{\scriptsym{IO}}}{A^{\scriptsym{BAG}}} w$
for each $w$ in the set
\begin{eqnarray*}
\lefteqn{W^{\scriptsym{BAG}} (B) =} \\ &&
\{\,\,
\{\setc.f.\setx^I\} \suchthat B (\setc.f.\setx) > 0 \next
\{\setc.b.\setx^I\} \suchthat B (\setc.b.\setx) > 0 \next
\dom T^{\scriptsym{BAG}} (B) \, \, \}.
\end{eqnarray*}
where
\begin{eqnarray*}
\lefteqn{\dom T^{\scriptsym{BAG}} (B) = } \\ &&
\{ \,\,
\setc.f.\setx^I \suchthat B (\setc.f.\setx) > 0 \next
\setc.b.\setx^I \suchthat B (\setc.b.\setx) > 0 \next
\setc.f.\setx^O \next \setc.b.\setx^O \, \, \}.
\end{eqnarray*}
The result is
\begin{eqnarray*}
\lefteqn{W^{\scriptsym{ROUT}} (O, I, B) =} \\ &&
\{
\begin{array}[t]{ll}
w^{\scriptsym{EXT}}(O, I) \cup \{\setc.f.\setx^I\} &
\suchthat B (\setc.f.\setx) > 0 \land I (\setc) = \alpha_0 \next \\
w^{\scriptsym{EXT}}(O, I) &
\suchthat B (\setc.f.\setx) > 0 \land I (\setc) \not= \alpha_0 \next \\
w^{\scriptsym{EXT}}(O, I) \cup \{\setc.b.\setx^I\} &
\suchthat B (\setc.b.\setx) > 0 \land O (\setc) = \alpha_2 \next \\
w^{\scriptsym{EXT}}(O, I) &
\suchthat B (\setc.b.\setx) > 0 \land O (\setc) \not= \alpha_2 \next \\
\dom T^{\scriptsym{ROUT}} (O, I, B) \, \, \},
\end{array}
\end{eqnarray*}
where
\begin{eqnarray*}
\lefteqn{w^{\scriptsym{EXT}} (O, I) =} \\ &&
\{
\begin{array}[t]{ll}
\setc.p.\setx & \suchthat O (\setc) = \alpha_0, \\
\setc.q.\setx & \suchthat I (\setc) = \alpha_1 (\setx), \\
\setc.r.\setx & \suchthat I (\setc) = \alpha_2, \\
\setc.s.\setx & \suchthat O (\setc) = \alpha_3 (\setx) \, \, \}
\end{array}
\end{eqnarray*}
and
\begin{eqnarray*}
\lefteqn{\dom T^{\scriptsym{ROUT}} (O, I, B) =} \\ &&
w^{\scriptsym{EXT}}(O, I) \cup
\{
\begin{array}[t]{ll}
\setc.f.\setx^I &
\suchthat B (\setc.f.\setx) > 0 \land I (\setc) = \alpha_0 \next \\
\setc.b.\setx^I &
\suchthat B (\setc.b.\setx) > 0 \land O (\setc) = \alpha_2 \next \\
\setc.f.\setx^O &
\suchthat O (\setc) = \alpha_1 (\setx) \next \\
\setc.b.\setx^O &
\suchthat I (\setc) = \alpha_3 (\setx) \, \, \}.
\end{array}
\end{eqnarray*}
Completing the definition of $T^{\scriptsym{ROUT}}$:
\begin{eqnarray*}
\lefteqn{T^{\scriptsym{ROUT}} (O, I, B) =} \\ &&
\{
\begin{array}[t]{ll}
(\setc.p.\setx \mapsto (O \oplus \{(\setc \mapsto \alpha_1 (\setx))\}, I, B))
& \suchthat O (\setc) = \alpha_0, \\
(\setc.f.\setx^O \mapsto (O \oplus \{(\setc \mapsto \alpha_2)\}, I,
B \oplus \{(\setc.f.\setx \mapsto B (\setc.f.\setx) + 1)\}))
& \suchthat O (\setc) = \alpha_1 (\setx), \\
(\setc.f.\setx^I \mapsto (O, I \oplus \{(\setc \mapsto \alpha_1 (\setx))\},
B \oplus \{(\setc.f.\setx \mapsto B (\setc.f.\setx) - 1)\}))
& \suchthat I (\setc) = \alpha_0 \land B (\setc.f.\setx) \not= 0, \\
(\setc.q.\setx \mapsto (O, I \oplus \{(\setc \mapsto \alpha_2)\}), B)
& \suchthat I (\setc) = \alpha_1 (\setx), \\
(\setc.r.\setx \mapsto (O, I \oplus \{(\setc \mapsto \alpha_3 (\setx))\}), B)
& \suchthat I (\setc) = \alpha_2, \\
(\setc.b.\setx^O \mapsto (O, I \oplus \{(\setc \mapsto \alpha_0)\},
B \oplus \{(\setc.b.\setx \mapsto B (\setc.b.\setx) + 1)\}))
& \suchthat I (\setc) = \alpha_3 (\setx), \\
(\setc.b.\setx^I \mapsto (O \oplus \{(\setc \mapsto \alpha_3 (\setx))\}, I,
B \oplus \{(\setc.b.\setx \mapsto B (\setc.b.\setx) - 1)\}))
& \suchthat O (\setc) = \alpha_2 \land B (\setc.b.\setx) \not= 0, \\
(\setc.s.\setx \mapsto (O \oplus \{(\setc \mapsto \alpha_0)\}, I, B))
& \suchthat O (\setc) = \alpha_3 (\setx) \, \, \},
\end{array}
\end{eqnarray*}
yields the ATM 
$(A^{\scriptsym{IO}}, S^{\scriptsym{IO}} \times S^{\scriptsym{BAG}},
T^{\scriptsym{ROUT}}, W^{\scriptsym{ROUT}})$ describing the combined system.

     Next, we conceal the internal events to yield an EATM.
\begin{eqnarray*}
\lefteqn{T^{\scriptsym{ROUT2}} (O, I, B) =} \\ &&
\{
\begin{array}[t]{ll}
(\setc.p.\setx \mapsto (O \oplus \{(\setc \mapsto \alpha_1 (\setx))\}, I, B))
& \suchthat O (\setc) = \alpha_0, \\
(\setc.q.\setx \mapsto (O, I \oplus \{(\setc \mapsto \alpha_2)\}), B)
& \suchthat I (\setc) = \alpha_1 (\setx), \\
(\setc.r.\setx \mapsto (O, I \oplus \{(\setc \mapsto \alpha_3 (\setx))\}), B)
& \suchthat I (\setc) = \alpha_2, \\
(\setc.s.\setx \mapsto (O \oplus \{(\setc \mapsto \alpha_0)\}, I, B))
& \suchthat O (\setc) = \alpha_3 (\setx) \, \, \},
\end{array}
\end{eqnarray*}
\begin{eqnarray*}
\lefteqn{U^{\scriptsym{ROUT2}} (O, I, B) =} \\ &&
\{
\begin{array}[t]{ll}
(O \oplus \{(\setc \mapsto \alpha_2)\}, I,
B \oplus \{(\setc.f.\setx \mapsto B (\setc.f.\setx) + 1)\})
& \suchthat O (\setc) = \alpha_1 (\setx), \\
(O, I \oplus \{(\setc \mapsto \alpha_1 (\setx))\},
B \oplus \{(\setc.f.\setx \mapsto B (\setc.f.\setx) - 1)\})
& \suchthat I (\setc) = \alpha_0 \land B (\setc.f.\setx) \not= 0, \\
(O, I \oplus \{(\setc \mapsto \alpha_0)\},
B \oplus \{(\setc.b.\setx \mapsto B (\setc.b.\setx) + 1)\})
& \suchthat I (\setc) = \alpha_3 (\setx), \\
(O \oplus \{(\setc \mapsto \alpha_3 (\setx))\}, I,
B \oplus \{(\setc.b.\setx \mapsto B (\setc.b.\setx) - 1)\})
& \suchthat O (\setc) = \alpha_2 \land B (\setc.b.\setx) \not= 0 \, \, \},
\end{array}
\end{eqnarray*}
\begin{eqnarray*}
\lefteqn{V^{\scriptsym{ROUT2}} (O, I, B) =} \\ &&
\{
\begin{array}[t]{ll}
(w^{\scriptsym{EXT}} (O, I) \next \{(O, I \oplus \{(\setc \mapsto \alpha_1 (\setx))\},
B \oplus \{(\setc.f.\setx \mapsto B (\setc.f.\setx) - 1)\}))\}
& \suchthat I (\setc) = \alpha_0 \land B (\setc.f.\setx) \not= 0, \\
(w^{\scriptsym{EXT}} (O, I) \next \emptyset)
& \suchthat I (\setc) \not= \alpha_0 \land B (\setc.f.\setx) \not= 0, \\
(w^{\scriptsym{EXT}} (O, I) \next
\{(O \oplus \{(\setc \mapsto \alpha_3 (\setx))\}, I,
B \oplus \{(\setc.b.\setx \mapsto B (\setc.b.\setx) - 1)\}))\}
& \suchthat O (\setc) = \alpha_2 \land B (\setc.b.\setx) \not= 0 \next \\
(w^{\scriptsym{EXT}} (O, I) \next \emptyset)
& \suchthat O (\setc) \not= \alpha_2 \land B (\setc.b.\setx) \not= 0 \next \\
(w^{\scriptsym{EXT}} (O, I) \next U^{\scriptsym{ROUT2}} (O, I, B)) \,\, \}.
\end{array}
\end{eqnarray*}
Finally, we have to show that the EATM
$(A^{\scriptsym{CHANS}}, S^{\scriptsym{ROUT}},
T^{\scriptsym{ROUT2}}, U^{\scriptsym{ROUT2}}), V^{\scriptsym{ROUT2}})$
simulates the TM
$(A^{\scriptsym{CHANS}}, S^{\scriptsym{CHANS}}, T^{\scriptsym{CHANS}})$.
We define the relation $G$ from 
$S^{\scriptsym{ROUT}}$ to $S^{\scriptsym{CHANS}}$ as follows:
\begin{definition}
\label{def:Gdef}
The relationship $(O, m, I, n) \infix G C$ holds iff
for any $c$ one of the following (mutually exclusive) clauses obtains
for some $x$
\begin{eqnarray}
\lefteqn{C (c) = \alpha_0 \land} \nonumber \\&&
O (c) = \alpha_0 \land (\forall y \truethat B (c.f.y) = 0) \land
I (c) = \alpha_0 \land (\forall y \truethat B (c.b.y) = 0), \\
\lefteqn{C (c) = \alpha_1 (x) \land} \nonumber \\&&
O (c) = \alpha_1 (x) \land (\forall y \truethat B (c.f.y) = 0) \land
I (c) = \alpha_0 \land (\forall y \truethat B (c.b.y) = 0), \\
\lefteqn{C (c) = \alpha_1 (x) \land} \nonumber \\&&
O (c) = \alpha_2 \land (\forall y \truethat B (c.f.y) = \delta_{xy}) \land
I (c) = \alpha_0 \land (\forall y \truethat B (c.b.y) = 0), \\
\lefteqn{C (c) = \alpha_1 (x) \land} \nonumber \\&&
O (c) = \alpha_2 \land (\forall y \truethat B (c.f.y) = 0) \land
I (c) = \alpha_1 (x) \land (\forall y \truethat B (c.b.y) = 0), \\
\lefteqn{C (c) = \alpha_2 \land} \nonumber \\&&
O (c) = \alpha_2 \land (\forall y \truethat B (c.f.y) = 0) \land
I (c) = \alpha_2 \land (\forall y \truethat B (c.b.y) = 0), \\
\lefteqn{C (c) = \alpha_3 (x) \land} \nonumber \\&&
O (c) = \alpha_2 \land (\forall y \truethat B (c.f.y) = 0) \land
I (c) = \alpha_3 (x) \land (\forall y \truethat B (c.b.y) = 0), \\
\lefteqn{C (c) = \alpha_3 (x) \land} \nonumber \\&&
O (c) = \alpha_2 \land (\forall y \truethat B (c.f.y) = 0) \land
I (c) = \alpha_0 \land (\forall y \truethat B (c.b.y) = \delta_{xy}), \\
\lefteqn{C (c) = \alpha_3 (x) \land} \nonumber \\&&
O (c) = \alpha_3 (x) \land (\forall y \truethat B (c.f.y) = 0) \land
I (c) = \alpha_0 \land (\forall y \truethat B (c.b.y) = 0)
\end{eqnarray}
\end{definition}
The first three properties needed to establish that $G$ is a
simulation are proved in exactly the same way as
in lemmas \ref{lem:xxx} to \ref{lem:yyy}.  The last lemma
needed is, assuming $(O, m, I, n) \infix G C$
\begin{lemma}
$((w, u) \in V^{\scriptsym{MUX2}} (O, m, I, n) \land u = \emptyset) \Rightarrow
(w \supset \dom T^{\scriptsym{CHANS}} (C))$.
\end{lemma}
\begin{proof}
A priori, there are five cases to consider:
\begin{enumerate}
\item
$I (c) = \alpha_0 \land B (c.f.x) \not= 0$ and
$u = \{(O, I \oplus \{(c \mapsto \alpha_1 (x))\},
B \oplus \{(c.f.x \mapsto B (c.f.x) - 1)\}))\}$.
\item
$I (c) \not= \alpha_0 \land B (c.f.x) \not= 0$ and $u = \emptyset$.
\item
$O (c) = \alpha_2 \land B (c.b.x) \not= 0 $
and $u = \{(O \oplus \{(c \mapsto \alpha_3 (x))\}, I,
\oplus \{(c.b.x \mapsto B (c.b.x) - 1)\})\}$.
\item
$ O (\setc) \not= \alpha_2 \land B (\setc.b.\setx) \not= 0 $ and
$u = \emptyset$.
\item
$u = U^{\scriptsym{ROUT2}} (O, I, B)$.
\end{enumerate}

In case 1, $u = \emptyset$ is false, so the implication is valid.

The precondition of case 2 contradicts the assumption that
$(O, I, B)$ is in the range of $G$ (none of the clauses in the
definition is consistent with this condition).  So this
case doesn't need further consideration.

Case 3 is like case 1.

Case 4 is like case 2.

In case 5 the implication is established as for lemma \ref{lem:zzz}.
\end{proof}

