\documentstyle{csart}

\begin{document}

\sloppy

\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\choice{\, \Box \,}

\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}} \,}
\newcommand{\setvar}[1]{\underline{#1}}
\newcommand{\infix}[1]{\,\,#1\,\,}

\newcommand{\paracc}[2]{\infix{[ #1 \sqcap #2 ]}}

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

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

\def\restrict{\rhd}

\def\Nat{\mbox{Nat}}

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

\def\ndchoice{\sqcap}
\def\Ndchoice{\ndchoice}
\def\suchthat{\, | \,}
\def\truethat{. \,\,}
\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\any{\underline{\,\,\,}}

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

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

\def\Pow{\mbox{Pow}\,\,}
\def\dom{\mbox{dom}\,\,}
\def\ran{\mbox{ran}\,\,}

\newtheorem{theorem}{Theorem}[section]
\newtheorem{definition}[theorem]{Definition}
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{corollary}[theorem]{Corollary}

\newenvironment{proof}{{\bf Proof}:}{\newline}

\title{Some CSP Proof Techniques Applied to Virtual Channel Protocols}

\author{D.B. Carpenter}
\address{Department of Electronics and Computer Science, \\
         Southampton University, \\
         Southampton, S09 5NH} 

\maketitle

%\newpage

%\tableofcontents
%\listoftables

%\newpage

\setcounter{page}{1}
\pagestyle{plain}

%\section{Message-routers and channel systems.}

%\section{Mathematical background and notation.}

\input{transition1}

\input{multx}

\input{transition2}

\input{routers}

\input{discussion}

\appendix

\input{simproof}

\begin{thebibliography}{9}

\bibitem{mail} C.A.R.~Hoare and He Jifeng, ``Design and Proof of a
Mail Service'', in ``Developments in Concurrency and Communication''
edited by C.A.R.~Hoare, Addison Wesley (1990).

\end{thebibliography}

\end{document}

