%
% >>> csp.sty <<< 
%
% (c) Jim Davies, January 1995

% You may copy and distribute this file freely.  Any queries and
% complaints should be forwarded to Jim.Davies@comlab.ox.ac.uk.

% If you make any changes to this file, please do not distribute
% the results under the name `csp.sty'.  

% >>> information <<<

% This is a LaTeX2e package for typesetting Z and CSP notation.  It
% employs the standard (JMS) set of macros, but uses the AMS fonts in
% place of `oxsy'.  You will need the tfm and fd files for the `A' and
% `B' symbol fonts installed.  This requires (1) the AMSFONTS package
% and (2) the MFNFSS package for LaTeX2e.  

% If you have the Lucida Bright font set from Y&Y, then you can use
% that instead.  In this case, you have only to load `lucbr' (from the
% PSNFSS package) before `csp'.  

% >>> changes <<<

% version 0  (Sep 94): first attempt
% version 0a (Oct 94): fixed error in definition of \cat
% version 0b (Nov 94): added composite for \uminus 
% version 0c (Jan 95): removed definition of \emptyset 
% version 1 (Aug 96): removed fuzz and symbol stuff BPM

% >>> date and version <<<

\def\fileversion{1}
\def\filedate{96/08/29} 
\def\docdate {96/08/29}

\NeedsTeXFormat{LaTeX2e}
\RequirePackage{oz}
%\RequirePackage{ams-chars}

\ProvidesPackage{csp}[{%
  \filedate\space\fileversion\space csp package}]

% >>> copied from ams-chars.sty <<<

\@ifpackageloaded{lucbr}{}{%
  \DeclareMathVersion{zed}
  \SetMathAlphabet{\mathrm}{zed}{\encodingdefault}{\rmdefault}{m}{n}%
  \SetMathAlphabet{\mathbf}{zed}{\encodingdefault}{\rmdefault}{bx}{n}%
  \SetMathAlphabet{\mathsf}{zed}{\encodingdefault}{\sfdefault}{m}{n}%
  \DeclareSymbolFont{italics}{\encodingdefault}{\rmdefault}{m}{it}%
  \DeclareSymbolFontAlphabet{\mathrm}{operators}
  \DeclareSymbolFontAlphabet{\mathit}{letters}
  \DeclareSymbolFontAlphabet{\mathcal}{symbols}
  \DeclareSymbolFontAlphabet{\zedit}{italics}
  \DeclareSymbolFont{lasy}{U}{lasy}{m}{n}
  \DeclareSymbolFont{AMSa}{U}{msa}{m}{n}
  \DeclareSymbolFont{AMSb}{U}{msb}{m}{n}
  \let\mho\undefined
  \let\Join\undefined
  \let\Box\undefined
  \let\Diamond\undefined
  \let\leadsto\undefined
  \let\sqsubset\undefined
  \let\sqsupset\undefined
  \let\lhd\undefined
  \let\unlhd\undefined
  \let\rhd\undefined
  \let\unrhd\undefined
  \DeclareMathSymbol{\mho}{\mathord}{lasy}{"30}
  \DeclareMathSymbol{\Join}{\mathrel}{lasy}{"31}
  \DeclareMathSymbol{\Box}{\mathord}{lasy}{"32}
  \DeclareMathSymbol{\Diamond}{\mathord}{lasy}{"33}
  \DeclareMathSymbol{\leadsto}{\mathrel}{lasy}{"3B}
  \DeclareMathSymbol{\sqsubset}{\mathrel}{lasy}{"3C}
  \DeclareMathSymbol{\sqsupset}{\mathrel}{lasy}{"3D}
  \DeclareMathSymbol{\lhd}{\mathrel}{lasy}{"01}
  \DeclareMathSymbol{\unlhd}{\mathrel}{lasy}{"02}
  \DeclareMathSymbol{\rhd}{\mathrel}{lasy}{"03}
  \DeclareMathSymbol{\unrhd}{\mathrel}{lasy}{"04}
  \DeclareSymbolFontAlphabet{\bbold}{AMSb}
  \mathversion{zed}
  }

\@ifpackageloaded{lucbr}{%
  \DeclareMathSymbol{\doublebarwedge}{\mathbin}{symbols}{"D4}
  \DeclareMathSymbol{\lll}{\mathrel}{letters}{"DE}
  \DeclareMathSymbol{\ggg}{\mathrel}{letters}{"DF} 
  \DeclareMathSymbol{\eth}{\mathrel}{operators}{"F0}
  }{%
  \let\rightleftharpoons\undefined
  \let\angle\undefined
  \DeclareMathSymbol\boxdot{\mathbin}{AMSa}{"00}
  \DeclareMathSymbol\boxplus{\mathbin}{AMSa}{"01}
  \DeclareMathSymbol\boxtimes{\mathbin}{AMSa}{"02}
  \DeclareMathSymbol\square{\mathord}{AMSa}{"03}
  \DeclareMathSymbol\blacksquare{\mathord}{AMSa}{"04}
  \DeclareMathSymbol\centerdot{\mathbin}{AMSa}{"05}
  \DeclareMathSymbol\lozenge{\mathord}{AMSa}{"06}
  \DeclareMathSymbol\blacklozenge{\mathord}{AMSa}{"07}
  \DeclareMathSymbol\circlearrowright{\mathrel}{AMSa}{"08}
  \DeclareMathSymbol\circlearrowleft{\mathrel}{AMSa}{"09}
  \DeclareMathSymbol\rightleftharpoons{\mathrel}{AMSa}{"0A}
  \DeclareMathSymbol\leftrightharpoons{\mathrel}{AMSa}{"0B}
  \DeclareMathSymbol\boxminus{\mathbin}{AMSa}{"0C}
  \DeclareMathSymbol\Vdash{\mathrel}{AMSa}{"0D}
  \DeclareMathSymbol\Vvdash{\mathrel}{AMSa}{"0E}
  \DeclareMathSymbol\vDash{\mathrel}{AMSa}{"0F}
  \DeclareMathSymbol\twoheadrightarrow{\mathrel}{AMSa}{"10}
  \DeclareMathSymbol\twoheadleftarrow{\mathrel}{AMSa}{"11}
  \DeclareMathSymbol\leftleftarrows{\mathrel}{AMSa}{"12}
  \DeclareMathSymbol\rightrightarrows{\mathrel}{AMSa}{"13}
  \DeclareMathSymbol\upuparrows{\mathrel}{AMSa}{"14}
  \DeclareMathSymbol\downdownarrows{\mathrel}{AMSa}{"15}
  \DeclareMathSymbol\upharpoonright{\mathrel}{AMSa}{"16}
  \DeclareMathSymbol\downharpoonright{\mathrel}{AMSa}{"17}
  \DeclareMathSymbol\upharpoonleft{\mathrel}{AMSa}{"18}
  \DeclareMathSymbol\downharpoonleft{\mathrel}{AMSa}{"19}
  \DeclareMathSymbol\rightarrowtail{\mathrel}{AMSa}{"1A}
  \DeclareMathSymbol\leftarrowtail{\mathrel}{AMSa}{"1B}
  \DeclareMathSymbol\leftrightarrows{\mathrel}{AMSa}{"1C}
  \DeclareMathSymbol\rightleftarrows{\mathrel}{AMSa}{"1D}
  \DeclareMathSymbol\Lsh{\mathrel}{AMSa}{"1E}
  \DeclareMathSymbol\Rsh{\mathrel}{AMSa}{"1F}
  \DeclareMathSymbol\rightsquigarrow{\mathrel}{AMSa}{"20}
  \DeclareMathSymbol\leftrightsquigarrow{\mathrel}{AMSa}{"21}
  \DeclareMathSymbol\looparrowleft{\mathrel}{AMSa}{"22}
  \DeclareMathSymbol\looparrowright{\mathrel}{AMSa}{"23}
  \DeclareMathSymbol\circeq{\mathrel}{AMSa}{"24}
  \DeclareMathSymbol\succsim{\mathrel}{AMSa}{"25}
  \DeclareMathSymbol\gtrsim{\mathrel}{AMSa}{"26}
  \DeclareMathSymbol\gtrapprox{\mathrel}{AMSa}{"27}
  \DeclareMathSymbol\multimap{\mathrel}{AMSa}{"28}
  \DeclareMathSymbol\therefore{\mathrel}{AMSa}{"29}
  \DeclareMathSymbol\amsbecause{\mathrel}{AMSa}{"2A}
  \DeclareMathSymbol\doteqdot{\mathrel}{AMSa}{"2B}
  \DeclareMathSymbol\triangleq{\mathrel}{AMSa}{"2C}
  \DeclareMathSymbol\precsim{\mathrel}{AMSa}{"2D}
  \DeclareMathSymbol\lesssim{\mathrel}{AMSa}{"2E}
  \DeclareMathSymbol\lessapprox{\mathrel}{AMSa}{"2F}
  \DeclareMathSymbol\eqslantless{\mathrel}{AMSa}{"30}
  \DeclareMathSymbol\eqslantgtr{\mathrel}{AMSa}{"31}
  \DeclareMathSymbol\curlyeqprec{\mathrel}{AMSa}{"32}
  \DeclareMathSymbol\curlyeqsucc{\mathrel}{AMSa}{"33}
  \DeclareMathSymbol\preccurlyeq{\mathrel}{AMSa}{"34}
  \DeclareMathSymbol\leqq{\mathrel}{AMSa}{"35}
  \DeclareMathSymbol\leqslant{\mathrel}{AMSa}{"36}
  \DeclareMathSymbol\lessgtr{\mathrel}{AMSa}{"37}
  \DeclareMathSymbol\backprime{\mathord}{AMSa}{"38}
  \DeclareMathSymbol\risingdotseq{\mathrel}{AMSa}{"3A}
  \DeclareMathSymbol\fallingdotseq{\mathrel}{AMSa}{"3B}
  \DeclareMathSymbol\succcurlyeq{\mathrel}{AMSa}{"3C}
  \DeclareMathSymbol\geqq{\mathrel}{AMSa}{"3D}
  \DeclareMathSymbol\geqslant{\mathrel}{AMSa}{"3E}
  \DeclareMathSymbol\gtrless{\mathrel}{AMSa}{"3F}
  \DeclareMathSymbol\sqsubset{\mathrel}{AMSa}{"40}
  \DeclareMathSymbol\sqsupset{\mathrel}{AMSa}{"41}
  \DeclareMathSymbol\vartriangleright{\mathrel}{AMSa}{"42}
  \DeclareMathSymbol\vartriangleleft{\mathrel}{AMSa}{"43}
  \DeclareMathSymbol\trianglerighteq{\mathrel}{AMSa}{"44}
  \DeclareMathSymbol\trianglelefteq{\mathrel}{AMSa}{"45}
  \DeclareMathSymbol\bigstar{\mathord}{AMSa}{"46}
  \DeclareMathSymbol\between{\mathrel}{AMSa}{"47}
  \DeclareMathSymbol\blacktriangledown{\mathord}{AMSa}{"48}
  \DeclareMathSymbol\blacktriangleright{\mathrel}{AMSa}{"49}
  \DeclareMathSymbol\blacktriangleleft{\mathrel}{AMSa}{"4A}
  \DeclareMathSymbol\vartriangle{\mathord}{AMSa}{"4D}
  \DeclareMathSymbol\blacktriangle{\mathord}{AMSa}{"4E}
  \DeclareMathSymbol\triangledown{\mathord}{AMSa}{"4F}
  \DeclareMathSymbol\eqcirc{\mathrel}{AMSa}{"50}
  \DeclareMathSymbol\lesseqgtr{\mathrel}{AMSa}{"51}
  \DeclareMathSymbol\gtreqless{\mathrel}{AMSa}{"52}
  \DeclareMathSymbol\lesseqqgtr{\mathrel}{AMSa}{"53}
  \DeclareMathSymbol\gtreqqless{\mathrel}{AMSa}{"54}
  \DeclareMathSymbol\Rrightarrow{\mathrel}{AMSa}{"56}
  \DeclareMathSymbol\Lleftarrow{\mathrel}{AMSa}{"57}
  \DeclareMathSymbol\veebar{\mathbin}{AMSa}{"59}
  \DeclareMathSymbol\barwedge{\mathbin}{AMSa}{"5A}
  \DeclareMathSymbol\doublebarwedge{\mathbin}{AMSa}{"5B}
  \DeclareMathSymbol\angle{\mathord}{AMSa}{"5C}
  \DeclareMathSymbol\measuredangle{\mathord}{AMSa}{"5D}
  \DeclareMathSymbol\sphericalangle{\mathord}{AMSa}{"5E}
  \DeclareMathSymbol\varpropto{\mathrel}{AMSa}{"5F}
  \DeclareMathSymbol\smallsmile{\mathrel}{AMSa}{"60}
  \DeclareMathSymbol\smallfrown{\mathrel}{AMSa}{"61}
  \DeclareMathSymbol\Subset{\mathrel}{AMSa}{"62}
  \DeclareMathSymbol\Supset{\mathrel}{AMSa}{"63}
  \DeclareMathSymbol\Cup{\mathbin}{AMSa}{"64}
  \DeclareMathSymbol\Cap{\mathbin}{AMSa}{"65}
  \DeclareMathSymbol\curlywedge{\mathbin}{AMSa}{"66}
  \DeclareMathSymbol\curlyvee{\mathbin}{AMSa}{"67}
  \DeclareMathSymbol\leftthreetimes{\mathbin}{AMSa}{"68}
  \DeclareMathSymbol\rightthreetimes{\mathbin}{AMSa}{"69}
  \DeclareMathSymbol\subseteqq{\mathrel}{AMSa}{"6A}
  \DeclareMathSymbol\supseteqq{\mathrel}{AMSa}{"6B}
  \DeclareMathSymbol\bumpeq{\mathrel}{AMSa}{"6C}
  \DeclareMathSymbol\Bumpeq{\mathrel}{AMSa}{"6D}
  \DeclareMathSymbol\lll{\mathrel}{AMSa}{"6E}
  \DeclareMathSymbol\ggg{\mathrel}{AMSa}{"6F}
  \DeclareMathDelimiter\ulcorner{4}{AMSa}{"70}{AMSa}{"70}
  \DeclareMathDelimiter\urcorner{5}{AMSa}{"71}{AMSa}{"71}
  \DeclareMathDelimiter\llcorner{4}{AMSa}{"78}{AMSa}{"78}
  \DeclareMathDelimiter\lrcorner{5}{AMSa}{"79}{AMSa}{"79}
  \xdef\yen      {\noexpand\mathhexbox\hexnumber@\symAMSa 55 }
  \xdef\checkmark{\noexpand\mathhexbox\hexnumber@\symAMSa 58 }
  \xdef\circledR {\noexpand\mathhexbox\hexnumber@\symAMSa 72 }
  \xdef\maltese  {\noexpand\mathhexbox\hexnumber@\symAMSa 7A }
  \DeclareMathSymbol\circledS{\mathord}{AMSa}{"73}
  \DeclareMathSymbol\pitchfork{\mathrel}{AMSa}{"74}
  \DeclareMathSymbol\dotplus{\mathbin}{AMSa}{"75}
  \DeclareMathSymbol\backsim{\mathrel}{AMSa}{"76}
  \DeclareMathSymbol\backsimeq{\mathrel}{AMSa}{"77}
  \DeclareMathSymbol\complement{\mathord}{AMSa}{"7B}
  \DeclareMathSymbol\intercal{\mathbin}{AMSa}{"7C}
  \DeclareMathSymbol\circledcirc{\mathbin}{AMSa}{"7D}
  \DeclareMathSymbol\circledast{\mathbin}{AMSa}{"7E}
  \DeclareMathSymbol\circleddash{\mathbin}{AMSa}{"7F}
  \DeclareMathSymbol\lvertneqq{\mathrel}{AMSb}{"00}
  \DeclareMathSymbol\gvertneqq{\mathrel}{AMSb}{"01}
  \DeclareMathSymbol\nleq{\mathrel}{AMSb}{"02}
  \DeclareMathSymbol\ngeq{\mathrel}{AMSb}{"03}
  \DeclareMathSymbol\nless{\mathrel}{AMSb}{"04}
  \DeclareMathSymbol\ngtr{\mathrel}{AMSb}{"05}
  \DeclareMathSymbol\nprec{\mathrel}{AMSb}{"06}
  \DeclareMathSymbol\nsucc{\mathrel}{AMSb}{"07}
  \DeclareMathSymbol\lneqq{\mathrel}{AMSb}{"08}
  \DeclareMathSymbol\gneqq{\mathrel}{AMSb}{"09}
  \DeclareMathSymbol\nleqslant{\mathrel}{AMSb}{"0A}
  \DeclareMathSymbol\ngeqslant{\mathrel}{AMSb}{"0B}
  \DeclareMathSymbol\lneq{\mathrel}{AMSb}{"0C}
  \DeclareMathSymbol\gneq{\mathrel}{AMSb}{"0D}
  \DeclareMathSymbol\npreceq{\mathrel}{AMSb}{"0E}
  \DeclareMathSymbol\nsucceq{\mathrel}{AMSb}{"0F}
  \DeclareMathSymbol\precnsim{\mathrel}{AMSb}{"10}
  \DeclareMathSymbol\succnsim{\mathrel}{AMSb}{"11}
  \DeclareMathSymbol\lnsim{\mathrel}{AMSb}{"12}
  \DeclareMathSymbol\gnsim{\mathrel}{AMSb}{"13}
  \DeclareMathSymbol\nleqq{\mathrel}{AMSb}{"14}
  \DeclareMathSymbol\ngeqq{\mathrel}{AMSb}{"15}
  \DeclareMathSymbol\precneqq{\mathrel}{AMSb}{"16}
  \DeclareMathSymbol\succneqq{\mathrel}{AMSb}{"17}
  \DeclareMathSymbol\precnapprox{\mathrel}{AMSb}{"18}
  \DeclareMathSymbol\succnapprox{\mathrel}{AMSb}{"19}
  \DeclareMathSymbol\lnapprox{\mathrel}{AMSb}{"1A}
  \DeclareMathSymbol\gnapprox{\mathrel}{AMSb}{"1B}
  \DeclareMathSymbol\nsim{\mathrel}{AMSb}{"1C}
  \DeclareMathSymbol\ncong{\mathrel}{AMSb}{"1D}
  \DeclareMathSymbol\varsubsetneq{\mathrel}{AMSb}{"20} 
  \DeclareMathSymbol\varsupsetneq{\mathrel}{AMSb}{"21}
  \DeclareMathSymbol\nsubseteqq{\mathrel}{AMSb}{"22}
  \DeclareMathSymbol\nsupseteqq{\mathrel}{AMSb}{"23}
  \DeclareMathSymbol\subsetneqq{\mathrel}{AMSb}{"24}
  \DeclareMathSymbol\supsetneqq{\mathrel}{AMSb}{"25}
  \DeclareMathSymbol\varsubsetneqq{\mathrel}{AMSb}{"26}
  \DeclareMathSymbol\varsupsetneqq{\mathrel}{AMSb}{"27}
  \DeclareMathSymbol\subsetneq{\mathrel}{AMSb}{"28}
  \DeclareMathSymbol\supsetneq{\mathrel}{AMSb}{"29}
  \DeclareMathSymbol\nsubseteq{\mathrel}{AMSb}{"2A}
  \DeclareMathSymbol\nsupseteq{\mathrel}{AMSb}{"2B}
  \DeclareMathSymbol\nparallel{\mathrel}{AMSb}{"2C}
  \DeclareMathSymbol\nmid{\mathrel}{AMSb}{"2D}
  \DeclareMathSymbol\nshortmid{\mathrel}{AMSb}{"2E}
  \DeclareMathSymbol\nshortparallel{\mathrel}{AMSb}{"2F}
  \DeclareMathSymbol\nvdash{\mathrel}{AMSb}{"30}
  \DeclareMathSymbol\nVdash{\mathrel}{AMSb}{"31}
  \DeclareMathSymbol\nvDash{\mathrel}{AMSb}{"32}
  \DeclareMathSymbol\nVDash{\mathrel}{AMSb}{"33}
  \DeclareMathSymbol\ntrianglerighteq{\mathrel}{AMSb}{"34}
  \DeclareMathSymbol\ntrianglelefteq{\mathrel}{AMSb}{"35}
  \DeclareMathSymbol\ntriangleleft{\mathrel}{AMSb}{"36}
  \DeclareMathSymbol\ntriangleright{\mathrel}{AMSb}{"37}
  \DeclareMathSymbol\nleftarrow{\mathrel}{AMSb}{"38}
  \DeclareMathSymbol\nrightarrow{\mathrel}{AMSb}{"39}
  \DeclareMathSymbol\nLeftarrow{\mathrel}{AMSb}{"3A}
  \DeclareMathSymbol\nRightarrow{\mathrel}{AMSb}{"3B}
  \DeclareMathSymbol\nLeftrightarrow{\mathrel}{AMSb}{"3C}
  \DeclareMathSymbol\nleftrightarrow{\mathrel}{AMSb}{"3D}
  \DeclareMathSymbol\divideontimes{\mathbin}{AMSb}{"3E}
  \DeclareMathSymbol\varnothing{\mathord}{AMSb}{"3F}
  \DeclareMathSymbol\mho{\mathord}{AMSb}{"66}
  \DeclareMathSymbol\eth{\mathord}{AMSb}{"67}
  \DeclareMathSymbol\eqsim{\mathrel}{AMSb}{"68}
  \DeclareMathSymbol\beth{\mathord}{AMSb}{"69}
  \DeclareMathSymbol\gimel{\mathord}{AMSb}{"6A}
  \DeclareMathSymbol\daleth{\mathord}{AMSb}{"6B}
  \DeclareMathSymbol\lessdot{\mathrel}{AMSb}{"6C}
  \DeclareMathSymbol\gtrdot{\mathrel}{AMSb}{"6D}
  \DeclareMathSymbol\ltimes{\mathbin}{AMSb}{"6E}
  \DeclareMathSymbol\rtimes{\mathbin}{AMSb}{"6F}
  \DeclareMathSymbol\shortmid{\mathrel}{AMSb}{"70}
  \DeclareMathSymbol\shortparallel{\mathrel}{AMSb}{"71}
  \DeclareMathSymbol\smallsetminus{\mathbin}{AMSb}{"72}
  \DeclareMathSymbol\thicksim{\mathrel}{AMSb}{"73}
  \DeclareMathSymbol\thickapprox{\mathrel}{AMSb}{"74}
  \DeclareMathSymbol\approxeq{\mathrel}{AMSb}{"75}
  \DeclareMathSymbol\succapprox{\mathrel}{AMSb}{"76}
  \DeclareMathSymbol\precapprox{\mathrel}{AMSb}{"77}
  \DeclareMathSymbol\curvearrowleft{\mathrel}{AMSb}{"78}
  \DeclareMathSymbol\curvearrowright{\mathrel}{AMSb}{"79}
  \DeclareMathSymbol\digamma{\mathord}{AMSb}{"7A}
  \DeclareMathSymbol\varkappa{\mathord}{AMSb}{"7B}
  \DeclareMathSymbol\hslash{\mathord}{AMSb}{"7D}
  \DeclareMathSymbol\hbar{\mathord}{AMSb}{"7E}
  \DeclareMathSymbol\backepsilon{\mathrel}{AMSb}{"7F}
  }

% copied from oz.sty <<<

% >>> csp <<< 

% We require the following mathematical symbols and aliases when
% specifying and reasoning about the behaviour of CSP processes. 

\let \Inter     \bigcap                   
\let \Land      \bigwedge                 
\let \Lor       \bigvee                   
\let \Union     \bigcup                   
\let \inter     \cap                          
\def \nin       {\not\in}
\let \union     \cup                          
\def \rat       {{\bbold Q}}
\def \real      {{\bbold R}}
\def \cnt       {\mathrel{\downarrow}}
\def \data      {\mathrel{\Downarrow}}
\def \during    {\mathrel{\uparrow}}
\def \nil       {\trace{}}                       
\def \clause    {\Bigm{|}}      
\def \contig    {\mathrel{\mathbf{in}}}
\def \trace#1{\langle #1\rangle}          
\def \set#1{\{#1\}}                       
\let \ge        \geqslant
\let \le        \leqslant
\@ifpackageloaded{lucbr}{%
  \DeclareMathSymbol{\tick}{0}{arrows}{"AC}
  }{
  \DeclareMathSymbol{\tick}{0}{AMSa}{"58}
  }

\let \subseq    \preccurlyeq

% We define a number of useful macros for projecting information from
% a timed or untimed observation. 

\def \Begin     {\@myop{\mathrm{begin}}}
\def \End       {\@myop{\mathrm{end}}}
\def \Head      {\@myop{\mathrm{head}}}
\def \First     {\@myop{\mathrm{first}}}
\def \Tail      {\@myop{\mathrm{tail}}}
\def \Front     {\@myop{\mathrm{front}}}
\def \Last      {\@myop{\mathrm{last}}}
\def \Times     {\@myop{\mathrm{times}}}
\def \Events    {\@myop{\mathrm{events}}}
\def \Reverse   {\@myop{\mathrm{reverse}}}

% We define a number of useful macros for specification purposes. 

\def\@PreMacro#1{\mathop{\mbox{\sffamily #1}}}
\def\@InMacro#1{\mathrel{\mbox{\sffamily #1}}}
\def\@@InMacro#1^#2{\;\mbox{\sffamily #1}^{#2}\;}
\def\@SupInMacro#1{\@ifnextchar^{\@@InMacro{#1}}{\@InMacro{#1}}}

\def \mInternal         {\@PreMacro{internal}}
\def \mRef              {\@InMacro{ref}}
\def \mAt               {\@SupInMacro{at}}
\def \mLive             {\@SupInMacro{live}}
\def \mOpen             {\@SupInMacro{open}}
\def \mFrom             {\@InMacro{from}}
\def \mUntil            {\@InMacro{until}}
\def \mLiveFrom         {\@InMacro{live from}}
\def \mOpenFrom         {\@InMacro{open from}}
\def \mNameOfLast       {\@InMacro{name of last}}
\def \mBefore           {\@InMacro{before}}
\def \mAfter            {\@InMacro{after}}
\def \mTimeOfLast       {\@InMacro{time of last}}

% We define a conditional syntax for processes.  This is an expression
% conditional, and should not be confused with the command conditional
% of programming languages.  That is, if the boolean condition is
% true, then the expression under consideration is equal to the
% expression in the first branch. 

\def \If        {\mathrel{\hbox{if}}}
\def \Then      {\mathrel{\hbox{then}}}
\def \Otherwise {\mathrel{\hbox{otherwise}}}
\def \Else      {\mathrel{\hbox{else}}}
\def \Fi        {\mathrel{\hbox{fi}}}

% In defining macros to set the syntax of real-time CSP, some symbols
% are used more than once.  For ease of understanding, we define these
% symbols as internal macros. 

\def \csp@at    {\hbox{\it @}}
\def \csp@bar   {\mathord{\mid}}
\def \csp@chain {\mathord{\gg}}
\def \csp@ext   {\mathord{\Box}}
\def \csp@int   {\mathord{\sqcap}}
\def \csp@par   {\mathord{\xparallel}}

\def \csp@interrupt {\mathord{\triangle}}
\def \csp@timeout   {\mathord{\triangleright}}

\@ifpackageloaded{lucbr}{%
  \def \csp@leftpar   {\csp@bar\mkern -3mu{[}}
  \def \csp@rightpar  {{]}\mkern -3mu\csp@bar}
  \def \csp@interleave {\csp@bar\mkern-2mu\csp@bar\mkern-2mu\csp@bar}
  \DeclareMathSymbol{\csp@transfer}{0}{arrows}{"93}
  }{
  \def \csp@leftpar   {\csp@bar{[}}
  \def \csp@rightpar  {{]}\csp@bar}
  \def \csp@interleave {\csp@bar\csp@bar\csp@bar}  
  \def \csp@transfer {\mathord{\swarrow}}
  }

% We define a quick hack to magnify the indexed forms of the choice
% and parallel composition operators.  It seems to work okay. 

\def\indexed@op#1{%
  \mathop{\vcenter{\hbox{\Large$\mathstrut#1$}}}\nolimits}

% We are now ready to define the macros used for setting the syntax of
% real-time CSP.  Notice that the LaTeX version of \parallel *must* be
% saved as \xparallel at this point. 

\let\xparallel \parallel 

\def \Bottom    {\mathord{\perp}}
\def\Init{I\!\mbox{\footnotesize\emph{NIT}}}

\def \Chaos     {C\!\mbox{\footnotesize\emph{HOAS}}}
\def \Stop      {S\!\mbox{\footnotesize\emph{TOP}}}
\def \Skip      {S\!\mbox{\footnotesize\emph{KIP}}}
\def \Div       {D\!\mbox{\footnotesize\emph{IV}}}
\def \Wait      {\@myop{W\!\mbox{\footnotesize\emph{AIT}}}}
\def \at        {\mathord{\csp@at}}
\def \then      {\@ifnextchar[{\@then}{\mathrel{\rightarrow}}}
\def \@then[#1]{\buildrel #1\over\rightarrow}
\def \barchoice {\mathrel{\csp@bar}}
\def \intchoice {\mathrel{\csp@int}}
\def \extchoice {\mathrel{\csp@ext}}
\def \interrupt {\mathrel{\csp@interrupt}}
\def \timeout   {\@ifnextchar[{\@timeout}{\mathrel{\csp@timeout}}}
\def \@timeout[#1]{\mathrel{\csp@timeout\{#1\}}}
\def \transfer  {\@ifnextchar[{\@transfer}{\mathrel{\csp@transfer}}}
\def \@transfer[#1]{\mathrel{\csp@transfer\{#1\}}}
\def \parallel  {\@ifnextchar[{\@parallel}{\mathrel{\csp@par}}}
\def \@parallel[#1]{\@ifnextchar[{\@@parallel[#1]}{%
                {\mathrel{\,\csp@leftpar\,{#1}\,\csp@rightpar\,}}}}
\def \@@parallel[#1][#2]{\mathrel{\,\csp@leftpar\,{#1}\,
                \csp@bar\,{#2}\,\csp@rightpar\,}}
\def \interleave{\mathrel{\csp@interleave}}
\def \chain     {\mathrel{\csp@chain}}
\def \Intchoice {\indexed@op{\csp@int}}
\def \Extchoice {\indexed@op{\csp@ext}}
\def \Parallel  {\indexed@op{\csp@par}}
\def \Interleave{\indexed@op{\csp@interleave}}

\def \@semapp[#1]{\,\lbag #1 \rbag}
\def \sem@fun#1{{#1}\@ifnextchar[{\@semapp}{}}
\def \Semantics         {\sem@fun{semantics}}
\def \Traces            {\sem@fun{traces}}
\def \Failures          {\sem@fun{failures}}
\def \TimedTraces       {\sem@fun{timed\,traces}}
\def \TimedFailures     {\sem@fun{timed\,failures}}
\def \Divergences       {\sem@fun{divergences}}
\def \Infinites         {\sem@fun{infinites}}

\def \lessdet{\@ifnextchar[{\@lessdet}{\mathrel\sqsubseteq}}
\def \@lessdet[#1]{\@ifnextchar[{\lessdet@two[#1]}{\lessdet@one[#1]}}
\def \lessdet@one[#1]{\mathrel{\sqsubseteq_{#1}}}
\def \lessdet@two[#1][#2]{%
        \mathrel{{\vphantom{\sqsubseteq}}_{#1}{\sqsubseteq}_{#2}}}

\let \refinedby \lessdet

\def \sat       {\mathrel{\mbox{\bf sat}}}
\def \semb#1{{\lbag #1 \rbag}}

% The following symbols have been used by researchers at Oxford to
% denote the various semantic models, spaces, and functions.  

\def\UT{UT}     \def\TE{TE}     \def\TT{TT}     
\def\RT{RT}     \def\TR{TR}     \def\TI{TI}                
\def\TTi{\TT^i} \def\TTw{\TT^\omega} \def\TRu{\TR^u}            

\def\@obsmodel#1{{\cal{O}}_{#1}}
\def\@obsspace#1{{\cal{S}}_{#1}}
\def\@semmodel#1{{\cal{M}}_{#1}}
\def\@semfunct#1{{\cal{F}}_{#1}\@ifnextchar[{\@semapp}{}}

\def\Out    {\@obsmodel{UT}}    \def\Sut    {\@obsspace{UT}}
\def\Ouf    {\@obsmodel{UF}}    \def\Suf    {\@obsspace{UF}}
\def\Oufd   {\@obsmodel{UFD}}   \def\Sufd   {\@obsspace{UFD}}
\def\Otf    {\@obsmodel{TF}}    \def\Stf    {\@obsspace{TF}}
\def\Otfs   {\@obsmodel{TFS}}   \def\Stfs   {\@obsspace{TFS}}
\def\Oti    {\@obsmodel{TI}}    \def\Sti    {\@obsspace{TI}}

\def\Mut    {\@semmodel{UT}}    \def\Fut    {\@semfunct{UT}}
\def\Muf    {\@semmodel{UF}}    \def\Fuf    {\@semfunct{UF}}
\def\Mufd   {\@semmodel{UFD}}   \def\Fufd   {\@semfunct{UFD}}
\def\Mtf    {\@semmodel{TF}}    \def\Ftf    {\@semfunct{TF}}
\def\Mtfs   {\@semmodel{TFS}}   \def\Ftfs   {\@semfunct{TFS}}
\def\Mti    {\@semmodel{TI}}    \def\Fti    {\@semfunct{TI}}

\endinput
