summaryrefslogtreecommitdiff
path: root/macros/latex/contrib/zed-csp
diff options
context:
space:
mode:
authorNorbert Preining <norbert@preining.info>2019-09-02 13:46:59 +0900
committerNorbert Preining <norbert@preining.info>2019-09-02 13:46:59 +0900
commite0c6872cf40896c7be36b11dcc744620f10adf1d (patch)
tree60335e10d2f4354b0674ec22d7b53f0f8abee672 /macros/latex/contrib/zed-csp
Initial commit
Diffstat (limited to 'macros/latex/contrib/zed-csp')
-rw-r--r--macros/latex/contrib/zed-csp/csp2e.pdfbin0 -> 112501 bytes
-rw-r--r--macros/latex/contrib/zed-csp/csp2e.tex381
-rw-r--r--macros/latex/contrib/zed-csp/zed-csp.sty789
-rw-r--r--macros/latex/contrib/zed-csp/zed2e.pdfbin0 -> 147037 bytes
-rw-r--r--macros/latex/contrib/zed-csp/zed2e.tex774
5 files changed, 1944 insertions, 0 deletions
diff --git a/macros/latex/contrib/zed-csp/csp2e.pdf b/macros/latex/contrib/zed-csp/csp2e.pdf
new file mode 100644
index 0000000000..557e7d7045
--- /dev/null
+++ b/macros/latex/contrib/zed-csp/csp2e.pdf
Binary files differ
diff --git a/macros/latex/contrib/zed-csp/csp2e.tex b/macros/latex/contrib/zed-csp/csp2e.tex
new file mode 100644
index 0000000000..880eedf08f
--- /dev/null
+++ b/macros/latex/contrib/zed-csp/csp2e.tex
@@ -0,0 +1,381 @@
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+% csp2e.tex -> hack guide to zed-csp.sty
+
+% (c) Jim Davies September 1994 >> Version 0 <<
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\documentclass[12pt]{article}
+
+% \usepackage[yy]{lucbr}
+
+% Uncomment the above line if you have the Lucida fonts and want to
+% use them to set csp. Note that you may have to change the [yy]
+% option if you are not using the Y&Y font naming convention.
+
+\usepackage{zed-csp}
+
+\advance\textwidth 30mm
+\advance\oddsidemargin -15mm
+\advance\evensidemargin -15mm
+\advance\textheight 35mm
+\advance\topmargin -20mm
+
+\begin{document} \thispagestyle{empty}
+
+\def\AMS{%
+ $\cal{A}$
+ \kern-.5em\lower.5ex\hbox{$\cal{M}$}\kern-.125em$\cal{S}$}
+
+\parindent 0pt
+\parskip 10pt
+
+{\huge\bf Setting real-time CSP}
+
+\vskip 2mm
+
+{\Large Jim Davies}
+
+\vskip 8mm
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\section{Introduction}
+
+The language and models of CSP have undergone a gradual evolution
+since the publication of the first CSP textbook---Hoare's {\sl
+Communicating Sequential Processes\/} (Prentice-Hall, 1985). The
+forthcoming text on real-time CSP will provide for some
+degree of standardisation.
+
+In parallel, we hope to provide a standard set of macros for setting
+documents which use CSP notation. This will allow users to exchange
+documents in electronic form, and will form part of the user interface
+to the language tools.
+
+The macros are defined by a style file called \verb|zed-csp.sty|.
+This should work with \LaTeXe. Inquiries, suggestions, or complaints
+should be addressed to
+
+\begin{center}
+ {\tt Jim.Davies@comlab.ox.ac.uk}.
+\end{center}
+
+Note that this is a fairly quick fix of the style to enable myself and
+others to use the improved facilities offered by the new version of
+\LaTeX. It has not been rigorously tested, although it seems to work
+for me.
+
+\section{Symbols}
+
+We can divide the symbols used into three separate classes: symbols
+for the language itself, symbols used in the definition of the
+semantics, and symbols used in the specification language.
+
+\subsection{The language of real-time CSP}
+
+The operators of real-time CSP are set using macros of the same name.
+The macros for atomic operators begin with an uppercase letter; the
+same is true for those representing indexed versions of parallel and
+choice operators. All other macros are lowercase throughout. Some
+operators accept optional arguments, but no argument is compulsory.
+
+When an operator with an optional argument appears within an optional
+argument, \LaTeX may require assistance if it is to parse the
+expression correctly. In these circumstances, we use an extra pair of
+braces to delimit the process expression: e.g.,
+\begin{center}
+ \verb|\Ftf[{P \parallel[A] Q}]|.
+\end{center}
+
+\begin{tabular}{p{2in}p{1.5in}c} \\ \\
+bottom & \verb|\Bottom| & $ \Bottom $ \\[1ex]
+stop & \verb|\Stop| & $ \Stop $ \\[1ex]
+skip & \verb|\Skip| & $ \Skip $ \\[1ex]
+wait & \verb|\Wait| & $ \Wait $ \\[1ex]
+prefix & \verb|\then| & $ \then $ \\[1ex]
+external choice & \verb|\extchoice| & $ \extchoice $ \\[1ex]
+internal choice & \verb|\intchoice| & $ \intchoice $ \\[1ex]
+hiding & \verb|\hide| & $ \hide $ \\[1ex]
+parallel & \verb|\parallel[A][B]|& $ \parallel[A][B] $\\[1ex]
+interleaving & \verb|\interleave| & $ \interleave $ \\[1ex]
+sharing & \verb|\parallel[C]| & $ \parallel[C] $ \\[1ex]
+recursion & \verb|\mu X \spot P| & $ \mu X \spot P $ \\[1ex]
+timeout & \verb|\timeout[t]| & $\timeout[t]$\\[1ex]
+transfer & \verb|\transfer[t]| & $\transfer[t]$\\[1ex]
+interrupt & \verb|\interrupt| & $\interrupt$ \\[1ex]
+timer & \verb|\at| & $\at$ \\[1ex]
+indexed external choice & \verb|\Extchoice| & $ \Extchoice $ \\[1ex]
+indexed internal choice & \verb|\Intchoice| & $ \Intchoice $ \\[1ex]
+indexed alphabet parallel & \verb|\Parallel| & $ \Parallel $ \\[1ex]
+indexed interleaving & \verb|\Interleave| & $ \Interleave $
+\end{tabular}
+
+\subsection{Parallel combinations}
+
+There are several ways to denote the parallel combination of
+two processes in CSP. Firstly, we can describe the set of events upon
+which they must cooperate: e.g., in the process
+\[
+P \parallel[C] Q
+\]
+components $P$ and $Q$ must cooperate upon every event from the shared
+set $C$. Alternatively, we can declare two alphabets
+\begin{eqnarray*}
+\alpha P & = & A \\
+\alpha Q & = & B
+\end{eqnarray*}
+and write
+\[
+P \parallel Q
+\]
+to denote the parallel combination in which $P$ and $Q$ must cooperate
+upon every event in the intersection of their alphabets. Finally, we
+can add explicit alphabet information to the parallel operator: e.g.,
+\[
+P \parallel[A][B] Q
+\]
+is equivalent to the above parallel combination, given the values
+chosen for $\alpha P$ and $\alpha Q$.
+
+\subsection{Delays and timers}
+
+We write $\Wait t ; P$ to denote the process which will delay for time
+$t$ before behaving as $P$. The wait process is a delayed form of
+termination $\Skip$: i.e.,
+\begin{eqnarray*}
+\Wait 0 & = & \Skip
+\end{eqnarray*}
+To model a nondeterministic delay, we can use an internal choice
+operator indexed by a range of time values:
+\[
+\Intchoice_{t \in [t_1,t_2)} \Wait t
+\]
+A convenient abbreviation for this involves overloading the $\Wait$
+operator: e.g.,
+\[
+\Wait [t_1,t_2)
+\]
+abbreviates the above choice.
+
+External events in a process description are performed in cooperation
+with the environment of that process. It is therefore quite likely
+that an external event will not occur as soon as the process is ready.
+The time elapsed between the offer of an event and its occurrence can
+influence future behaviour; the rest of the process description should
+be allowed to refer to this time.
+
+Accordingly, real-time CSP includes a timer construct, or
+`passage-of-time' operator. We write
+\[
+a \at t \then P \qquad \qquad \hbox{\verb|a \at t \then P|}
+\]
+to denote a process which is initially ready to engage in event $a$.
+The time variable $t$ is assigned the relative time at which $a$
+occurs. This is the same as the elapsed time between control being
+passed to this process---at which point the offer of $a$ is made---and
+the event $a$ actually occuring.
+
+A useful extension to this, which adds nothing to the expressivity of
+the language but can make for more intelligible process descriptions,
+is the offer timeout. We write
+\[
+a \at t \{ d \} \then P \qquad \qquad
+\hbox{\verb|a \at t \{ d \} \then P|}
+\]
+to denote a process which offers to perform $a$, and will store the
+time of occurrence in $t$, but will withdraw the offer if it has not
+been accepted by time $d$. (This form of timeout was suggested
+by Guy Leduc for his version of timed LOTOS.)
+
+\section{Mathematical language}
+
+The semantic models of CSP come with a great deal of notational
+baggage. We need to define operators to project information out of
+traces, refusals, and timed failures. There is also a specification
+language based upon the timed semantics, and the names used for the
+models themselves.
+
+\subsection{Logic, sets, and sequences}
+
+\begin{tabular}{c@{\hspace{0.55in}}c@{\hspace{0.55in}}c} \\
+\begin{tabular}[t]{@{}lc}
+\verb|\defs| & $ \defs $ \\[0.6ex]
+\verb|\mu| & $ \mu $ \\[0.6ex]
+\verb|\lambda| & $ \lambda $ \\[0.6ex]
+\verb|\exists| & $ \exists $ \\[0.6ex]
+\verb|\forall| & $ \forall $ \\[0.6ex]
+\verb|\spot| & $ \spot $ \\[0.6ex]
+\verb|\nat| & $ \nat $ \\[0.6ex]
+\verb|\num| & $ \num $ \\[0.6ex]
+\verb|\rat| & $ \rat $ \\[0.6ex]
+\verb|\real| & $ \real $ \\[0.6ex]
+\verb|\seq| & $ \seq $
+\end{tabular} &
+\begin{tabular}[t]{lc}
+\verb|\land| & $ \land $ \\[0.6ex]
+\verb|\lor| & $ \lor $ \\[0.6ex]
+\verb|\Land| & $ \Land $ \\[0.6ex]
+\verb|\Lor| & $ \Lor $ \\[0.6ex]
+\verb|\lnot| & $\lnot $ \\[0.6ex]
+\verb|\implies| & $ \implies $ \\[0.6ex]
+\verb|\iff| & $ \iff $ \\[0.6ex]
+\verb|\upto| & $\upto$ \\[0.6ex]
+\verb|\le| & $ \le $ \\[0.6ex]
+\verb|\ge| & $ \ge $ \\[0.6ex]
+\verb|\project| & $ \project $
+\end{tabular} &
+\begin{tabular}[t]{lc}
+\verb|\power| & $ \power $ \\[0.6ex]
+\verb|\finset| & $ \finset $ \\[0.6ex]
+\verb|\cross| & $ \cross $ \\[0.6ex]
+\verb|\union| & $ \union $ \\[0.6ex]
+\verb|\inter| & $ \inter $ \\[0.6ex]
+\verb|\Union| & $ \Union $ \\[0.6ex]
+\verb|\Inter| & $ \Inter $ \\[0.6ex]
+\verb|\dom| & $ \dom$ \\[0.6ex]
+\verb|\ran| & $ \ran$ \\[0.6ex]
+\verb|\emptyset| & $\emptyset$ \\[0.6ex]
+\verb|\set{x}| & $ \set{x} $
+\end{tabular}
+\end{tabular}
+
+\subsection{Operators on traces}
+
+\begin{tabular}{p{1.95in}p{1.75in}c} \\
+empty trace & \verb|\nil| & $\nil $ \\[0.6ex]
+trace & \verb|\trace{e_1,e_2}| & $\trace{e_1,e_2}$\\[0.6ex]
+catenation of traces & \verb|\cat| & $\cat $ \\[0.6ex]
+count & \verb|\cnt| & $\cnt $ \\[0.6ex]
+during & \verb|\during| & $\during $ \\[0.6ex]
+tick event & \verb|\tick| & $\tick$ \\[0.6ex]
+subsequence & \verb|\subseq| & $\subseq$ \\[0.6ex]
+data values & \verb|\data| & $\data$
+\end{tabular}
+
+\subsection{Projection functions}
+
+\begin{tabular}{p{1.95in}p{1.75in}l} \\
+ begin & \verb|\Begin | & $\Begin$ \\[0.4ex]
+ end & \verb|\End | & $\End $ \\[0.4ex]
+ head & \verb|\Head | & $\Head $ \\[0.4ex]
+ first & \verb|\First | & $\First$ \\[0.4ex]
+ tail & \verb|\Tail | & $\Tail $ \\[0.4ex]
+ front & \verb|\Front | & $\Front$ \\[0.4ex]
+ last & \verb|\Last | & $\Last $ \\[0.4ex]
+ times & \verb|\Times | & $\Times$ \\[0.4ex]
+ events & \verb|\Events | & $\Events$ \\[0.4ex]
+\end{tabular}
+
+$\Times$ and $\Events$ are projection functions from timed traces to
+sequences of times and sequences of events respectively. $\Head$ and
+$\Tail$ may be applied to any sequence. $\Begin$ and $\End$ may be
+applied to timed traces and timed refusals. $\First$ is a synonym for
+$\Head$. $\Front$ is the dual of $\Tail$. $\Last$ is the dual of
+$\Head$.
+
+To denote the set of events mentioned in a timed or untimed trace or
+refusal, we prefix the name of the object with $\alpha$. For example,
+the set of events mentioned in the timed trace $s$ would be written
+$\alpha s$. Earlier version of real-time CSP did this using the
+$\sigma$ operator to avoid confusion with process alphabets. Where
+there is scope for confusion, we suggest that this practice is
+continued.
+
+\subsection{Semantic functions, models, and spaces}
+
+In {\sl Advanced CSP}, we use long names for the semantic functions:
+
+\begin{tabular}{p{1.95in}p{1.75in}l} \\
+semantics & \verb|\Semantics| & $\Semantics$ \\
+traces & \verb|\Traces| & $\Traces$ \\
+failures & \verb|\Failures| & $\Failures$ \\
+timed failures & \verb|\TimedFailures| & $\TimedFailures$ \\
+divergences & \verb|\Divergences| & $\Divergences$ \\
+infinites & \verb|\Infinites| & $\Infinites$
+\end{tabular}
+
+Any semantic function macro can be given an optional argument. This
+will be set within semantic brackets: e.g., \verb|\Traces[P]| yields
+$\Traces[P]$. To obtain the semantic brackets alone, use the
+\verb|\semb| macro; this takes a single compulsory argument.
+Alternatively, the macros \verb|\leftsemb| and \verb|\rightsemb|
+produce left and right semantic brackets respectively.
+
+In theoretical papers, we often need to refer to several models,
+functions, and associated spaces. To make things easier on ourselves,
+we adopt short names for these mathematical objects, using subscripts
+to identify the model concerned. For example, the objects associated
+with the timed failures model are all subscripted with $TF$.
+
+The models themselves have macros beginning \verb|\M|:
+
+\begin{tabular}{p{2.4in}p{1.1in}l} \\
+traces & \verb|\Mut| & $ \Mut $ \\
+failures & \verb|\Muf| & $ \Muf $ \\
+failures-divergences & \verb|\Mufd| & $ \Mufd $ \\
+timed failures & \verb|\Mtf| & $ \Mtf $ \\
+timed failures-stability & \verb|\Mtfs| & $ \Mtfs $ \\
+timed infinite & \verb|\Mti| & $ \Mti $
+\end{tabular}
+
+The matching semantic functions use \verb|\F| instead---e.g.,
+\verb|\Fut| for untimed traces---and the observation spaces use
+\verb|\S|.
+
+\subsection{Refinement and satisfaction}
+
+The satisfaction notation employed in Hoare's {\sl Communicating
+Sequential Processes} has been retained. We also have a refinement
+relation between processes, possibly indexed by the name of the model
+concerned.
+
+The satisfaction relation is set as follows: \verb|P \sat S| produces
+$P \sat S$. The refinement relation is produced by \verb|\lessdet| (or
+\verb|refinedby|, a synonymbol).
+
+\subsection{Specifications}
+
+To capture timing constraints at the level of the semantic models, we
+use a number of specification `macros'. These are set using \LaTeX\
+macros which begin with an `m' (for macro) and are then capitalised.
+\par
+\begin{tabular}{p{1.95in}p{1.75in}l} \\
+internal & \verb|\mInternal | & $ \mInternal $ \\[0.4ex]
+refuses & \verb|\mRef | & $ \mRef $ \\[0.4ex]
+at & \verb|\mAt | & $ \mAt $ \\[0.4ex]
+live & \verb|\mLive | & $ \mLive $ \\[0.4ex]
+open & \verb|\mOpen | & $ \mOpen $ \\[0.4ex]
+from & \verb|\mFrom | & $ \mFrom $ \\[0.4ex]
+until & \verb|\mUntil | & $ \mUntil $ \\[0.4ex]
+live from & \verb|\mLiveFrom | & $ \mLiveFrom $ \\[0.4ex]
+open from & \verb|\mOpenFrom | & $ \mOpenFrom $ \\[0.4ex]
+name of last & \verb|\mNameOfLast| & $ \mNameOfLast $ \\[0.4ex]
+before & \verb|\mBefore | & $ \mBefore $ \\[0.4ex]
+after & \verb|\mAfter | & $ \mAfter $ \\[0.4ex]
+time of last & \verb|\mTimeOfLast| & $ \mTimeOfLast $ \\[0.4ex]
+\end{tabular}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\section{Discussion}
+
+\subsection{Dependencies}
+
+You must have the AMS fonts available, and the {\tt amsfonts}
+installation must have been performed for \LaTeXe. This requires the
+{\tt mfnfss} package; it takes about twenty seconds.
+
+\subsection{CSP and Z}
+
+You may have problems if you try to use the {\tt zed-csp} package with
+{\tt fuzz} or any style package that uses the AMS fonts. The good
+news is that you shouldn't need them. All of the AMS symbols are
+defined in the {\tt zed-csp} package, using the standard names.
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\end{document}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
diff --git a/macros/latex/contrib/zed-csp/zed-csp.sty b/macros/latex/contrib/zed-csp/zed-csp.sty
new file mode 100644
index 0000000000..c89ce59eda
--- /dev/null
+++ b/macros/latex/contrib/zed-csp/zed-csp.sty
@@ -0,0 +1,789 @@
+%
+% >>> zed-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 `zed-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 `zed-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
+
+% >>> date and version <<<
+
+\def\fileversion{0c}
+\def\filedate{95/01/11}
+\def\docdate {95/01/11}
+
+\NeedsTeXFormat{LaTeX2e}
+
+\ProvidesPackage{zed-csp}[{%
+ \filedate\space\fileversion\space zed-csp package}]
+
+% >>> fonts and symbols <<<
+
+% We declare a new math version. For convenience, I have chosen the
+% same name as that used in oz.sty. The following code is based upon
+% the work of Paul King, Sebastian Rahtz, and Mike Spivey. Alan
+% Jeffrey's influence is everywhere.
+
+\@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\because{\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}
+ }
+
+% A macro name has been chosen for each of the symbols in the AMS
+% fonts. There is no need to load any other AMS package in order to
+% access these symbols.
+
+% >>> fuzz <<<
+
+% This is the standard fuzz setup, apart from the oz style change to
+% the setmcodes macro.
+
+\def\@setmcodes#1#2#3{{\count0=#1 \count1=#3
+ \loop \global\mathcode\count0=\count1 \ifnum \count0<#2
+ \advance\count0 by1 \advance\count1 by1 \repeat}}
+\@setmcodes{`A}{`Z}{"7\hexnumber@\symitalics41}%
+\@setmcodes{`a}{`z}{"7\hexnumber@\symitalics61}%
+
+\def~{\ifmmode\,\else\penalty\@M\ \fi}
+
+\let\@mc=\mathchardef \mathcode`\;="8000 {\catcode`\;=\active
+ \gdef;{\semicolon\;}} \@mc\semicolon="603B
+
+\def\strut@op#1{\mathop{\mathstrut{#1}}\nolimits}
+
+\def\_{\leavevmode \ifmmode\else\kern0.06em\fi \vbox{\hrule
+ width0.5em}}
+
+\mathcode`\"="8000 \def\@kwote#1"{\hbox{\it #1}} {\catcode`\"=\active
+ \global\let"=\@kwote}
+
+\mathchardef\spot="320F
+\mathcode`\@=\spot
+\mathcode`\|=\mid
+
+\def\bsup#1 \esup{^{#1}}
+
+\def\inrel#1{\mathrel{\underline{#1}}}
+
+\newdimen\zedindent \zedindent=\leftmargini%
+\newdimen\zedleftsep \zedleftsep=1em%
+\newdimen\zedtab \zedtab=2em%
+\newdimen\zedbar \zedbar=6em%
+\newskip\zedskip \zedskip=0.5\baselineskip plus0.333333\baselineskip%
+ minus0.333333\baselineskip%
+\def\zedsize{}%
+
+\newcount\interzedlinepenalty \interzedlinepenalty=10000%
+\newcount\preboxpenalty \preboxpenalty=0%
+\newif\ifzt@p \zt@pfalse%
+
+\def\@jot{0.5\zedskip}
+
+\def\@narrow{\advance\linewidth by-\zedindent}
+
+\def\@zrulefill{\leaders\hrule height\arrayrulewidth\hfill}
+
+\def\@topline#1{\hbox to\linewidth{%
+ \vrule height\arrayrulewidth width\arrayrulewidth
+ \vrule height0pt depth\@jot width0pt
+ \hbox to\zedleftsep{\@zrulefill\thinspace}%
+ #1\thinspace\@zrulefill}}
+
+\def\@zedline{\omit \vrule height\arrayrulewidth width\linewidth \cr}
+
+\def\where{\@zskip\@jot
+ \omit \vrule height\arrayrulewidth width\zedbar \cr
+ \@zskip\@jot}
+
+\def\also{\crcr \noalign{\penalty\interdisplaylinepenalty
+ \vskip\zedskip}}
+\def\@zskip#1{\crcr \omit \vrule height#1 width\arrayrulewidth \cr}
+\def\@zlign{\tabskip\z@skip\everycr{}}
+
+\let\tie=\t
+\def\t#1{\afterassignment\@t\count@=#1}
+\def\@t{\hskip\count@\zedtab}
+
+\def\@setzsize{\let\next=\@nomath\def\@nomath##1{}%
+ \skip0=\abovedisplayskip\skip1=\belowdisplayskip
+ \zedsize \let\@nomath=\next
+ \abovedisplayskip=\skip0\belowdisplayskip=\skip1}
+
+\def\@zed{\ifvmode\@zleavevmode\fi
+ $$\global\zt@ptrue
+ \@setzsize
+ \advance\linewidth by-\zedindent
+ \advance\displayindent by\zedindent
+ \def\\{\crcr}% Must have \def and not \let for nested alignments.
+ \let\par=\relax
+ \tabskip=0pt}
+
+\def\@znoskip{\offinterlineskip
+ \everycr={\noalign{\ifzt@p \global\zt@pfalse
+ \ifdim\prevdepth>-1000pt \skip0=\normalbaselineskip
+ \advance\skip0by-\prevdepth \advance\skip0by-\ht\strutbox
+ \ifdim\skip0<\normallineskiplimit \vskip\normallineskip
+ \else \vskip\skip0 \fi\fi
+ \else \penalty\interzedlinepenalty \fi}}}
+
+\def\zed{\@zed\@znoskip\halign to\linewidth\bgroup
+ \strut$\@zlign##$\hfil \tabskip=0pt plus1fil\cr}
+\def\endzed{\crcr\egroup$$\global\@ignoretrue}
+
+\def\[{\begingroup\zed}
+\def\]{\crcr\egroup$$\endgroup\ignorespaces}
+
+\def\axdef{\def\also{\@zskip\zedskip}%
+ \predisplaypenalty=\preboxpenalty
+ \@zed\@znoskip \halign to\linewidth\bgroup
+ \strut \vrule width\arrayrulewidth \hskip\zedleftsep
+ $\@zlign##$\hfil \tabskip=0pt plus1fil\cr}
+\let\endaxdef=\endzed
+
+\def\schema#1{\@ifnextchar[{\@schema{#1}}{\@nschema{#1}}}
+\def\@schema#1[#2]{\@nschema{#1[#2]}}
+\def\@nschema#1{\@narrow\axdef \omit\@topline{$\strut#1$}\cr}
+\def\endschema{\@zskip\@jot \@zedline \endzed}
+
+\@namedef{schema*}{\@narrow\axdef \@zedline \@zskip\@jot}
+\expandafter\let\csname endschema*\endcsname=\endschema
+
+\def\gendef{\@ifnextchar[{\@gendef}{\@ngendef}}
+\def\@gendef[#1]{\@narrow\axdef \omit \setbox0=\hbox{$\strut[#1]$}%
+ \rlap{\raise\doublerulesep\@topline{\hskip\wd0}}\@topline{\box0}\cr}
+\def\@ngendef{\@narrow\axdef \@zedline \omit \hbox to\linewidth{\vrule
+ height\doublerulesep width\arrayrulewidth \@zrulefill}\cr
+ \@zskip\@jot
+ }
+\let\endgendef=\endschema
+
+\def\argue{\@zed \interzedlinepenalty=\interdisplaylinepenalty
+ \openup\@jot \halign to\linewidth\bgroup
+ \strut$\@zlign##$\hfil \tabskip=0pt plus1fil
+ &\hbox to0pt{\hss[\@zlign##\unskip]}\tabskip=0pt\cr
+ \noalign{\vskip-\@jot}}
+\let\endargue=\endzed
+
+\def\because#1{\noalign{\vskip-\jot}&#1\cr}
+
+\def\syntax{\@zed\@znoskip \halign\bgroup
+ \strut$\@zlign##$\hfil &\hfil$\@zlign{}##{}$\hfil
+ &$\@zlign##$\hfil\cr}
+\let\endsyntax=\endzed
+
+\def\infrule{\@zed\@znoskip \halign\bgroup
+ \strut\quad$\@zlign##$\quad\hfil&\quad\@zlign##\hfil\cr}
+\let\endinfrule=\endzed
+
+\def\derive{\crcr \noalign{\vskip\@jot} \omit\@zrulefill
+ \@ifnextchar[{\@xderive}{\@yderive}}
+\def\@xderive[#1]{&$\smash{\lower 0.5ex\hbox{$[\;#1\;]$}}$\cr
+ \noalign{\vskip\@jot}}
+\def\@yderive{\cr \noalign{\vskip\@jot}}
+
+\def\@zleavevmode{\if@inlabel \indent
+ \else\if@noskipsec \indent
+ \else\if@nobreak \global\@nobreakfalse
+ \everypar={}\abovedisplayskip=0pt\fi
+ {\parskip=0pt\noindent}\fi\fi}
+
+% From now on, we must depart from the text of fuzz, as we do not have
+% the oxsy symbol font at our disposal. We must choose symbols from
+% the AMS or Lucida fonts to compensate for our loss. Sadly, this
+% means a number of conditional definitions. I have tried to maintain
+% the order of definitions used in fuzz2.sty, rather than factor the
+% font-dependent ones out.
+
+\let\xlambda=\lambda \let\xmu=\mu
+\let\xforall=\forall \let\xexists=\exists
+
+\def \bind {\mathrel{\leadsto}}
+\def \bindsto {\mathrel{\leadsto}}
+
+\@ifpackageloaded{lucbr}{%
+ \def \lblot {{\langle}\mkern -5mu{|}}
+ \def \rblot {{|}\mkern -5mu{\rangle}}
+ }{%
+ \def \lblot {{\langle}\mkern -3.5mu{|}}
+ \def \rblot {{|}\mkern -3.5mu{\rangle}}
+ }
+
+\let\lbind=\lblot
+\let\rbind=\rblot
+
+\def \defs {\mathrel{\widehat=}}
+\def \power {\strut@op{\bbold P}}
+\let \cross \times
+\def \lambda {\strut@op{\xlambda}}
+\def \mu {\strut@op{\xmu}}
+\@ifpackageloaded{lucbr}{}{
+ \def\ldbrack{{[}\mkern-2mu{[}}
+ \def\rdbrack{{]}\mkern-2mu{]}}}
+\let \lbag \ldbrack
+\let \rbag \rdbrack
+\def \lnot {\neg\;}
+\def \land {\mathrel{\wedge}}
+\def \lor {\mathrel{\vee}}
+\let \implies \Rightarrow
+\let \iff \Leftrightarrow
+\def \forall {\strut@op{\xforall}}
+\def \exists {\strut@op{\xexists}}
+\def \hide {\mathrel{\backslash}}
+\@ifpackageloaded{lucbr}{%
+ \DeclareMathSymbol{\project}{3}{arrows}{"75}}{%
+ \DeclareMathSymbol{\project}{\mathrel}{AMSa}{"16}}
+\def \pre {{\mathrm{pre}}\;}
+\def \semi {\mathrel{\comp}}
+\def \ldata {\langle\!\langle}
+\def \rdata {\rangle\!\rangle}
+\let \shows \vdash
+\def \pipe {\mathord>\!\!\mathord>}
+\def \LET {{\mathbf{let}}\;}
+\def \IF {{\mathbf{if}}\;}
+\def \THEN {\mathrel{\mathbf{then}}}
+\def \ELSE {\mathrel{\mathbf{else}}}
+
+\let \rel \leftrightarrow
+\def \dom {\mathop{\mathrm{dom}}}
+\def \ran {\mathop{\mathrm{ran}}}
+\def \id {\mathop{\mathrm{id}}}
+\@ifpackageloaded{lucbr}{%
+ \def\comp{\mathrel{\raise 0.66ex\hbox{\oalign{\hfil%
+ $\scriptscriptstyle\mathsf{o}$\hfil%
+ \cr\hfil$\scriptscriptstyle\mathsf{9}$\hfil}}}}
+ \DeclareMathSymbol{\dres}{\mathbin}{letters}{"2F}
+ \DeclareMathSymbol{\rres}{\mathbin}{letters}{"2E}}{%
+ \def\comp{\mathbin{\raise 0.6ex\hbox{\small\oalign{\hfil%
+ $\scriptscriptstyle\mathrm{o}$\hfil%
+ \cr\hfil$\scriptscriptstyle\mathrm{9}$\hfil}}}}
+ \DeclareMathSymbol{\dres}{\mathbin}{AMSa}{"43}
+ \DeclareMathSymbol{\rres}{\mathbin}{AMSa}{"42}
+ }
+\def \ndres {\mathbin{\rlap{\raise.05ex\hbox{$-$}}{\dres}}}
+\def \nrres {\mathbin{\rlap{\raise.05ex\hbox{$-$}}{\rres}}}
+\def \inv {^\sim}
+\def \limg {(\!|}
+\def \rimg {|\!)}
+
+\def\@p#1{\mathrel{\ooalign{\hfil$\mapstochar\mkern
+ 5mu$\hfil\cr$#1$}}}
+\def \pfun {\@p\fun}
+\let \fun \rightarrow
+\let \inj \rightarrowtail
+\@ifpackageloaded{lucbr}{%
+ \DeclareMathSymbol{\pinj}{3}{arrows}{"92}
+ \def \surj {\mathrel{\ooalign{$\fun$\hfil\cr$\mkern3mu\fun$}}}
+ \def \bij {\mathrel{\ooalign{$\inj$\hfil\cr$\mkern4mu\fun$}}}}{%
+ \def \pinj {\@p\inj}
+ \def \surj {\mathrel{\ooalign{$\fun$\hfil\cr$\mkern4mu\fun$}}}
+ \def \bij {\mathrel{\ooalign{$\inj$\hfil\cr$\mkern5mu\fun$}}}}
+\def \psurj {\@p\surj}
+\def \nat {{\bbold N}}
+\def \num {{\bbold Z}}
+\def \div {\mathbin{\mathsf{div}}}
+\def \mod {\mathbin{\mathsf{mod}}}
+\def \upto {\mathbin{\ldotp\ldotp}}
+\def \plus {^+}
+\def \star {^*}
+\def \finset {\strut@op{{\bbold F}}}
+\def\@f#1{\mathrel{\ooalign{\hfil$\mapstochar\mkern 3mu
+ \mapstochar\mkern 5mu$\hfil\cr$#1$}}}
+\def \ffun {\@f\fun}
+\def \finj {\@f\inj}
+\def \seq {\mathop{\mathrm{seq}}}
+\def \iseq {\mathop{\mathrm{iseq}}}
+\def \cat {\mathbin{\raise 0.8ex\hbox{$\smallfrown$}}}
+\def \filter {\mathbin{\project}}
+\def \dcat {\mathop{\cat/}}
+\def \bag {\mathop{\mathrm{bag}}}
+\def \bcount {\mathbin{\sharp}}
+\def \inbag {\mathrel{\mathrm{in}}}
+\let \subbageq \sqsubseteq
+\def \disjoint {{\mathsf{disjoint}}\;}
+\def \partition {\mathrel{\mathsf{partition}}}
+\def \prefix {\mathrel{\mathsf{prefix}}}
+\def \suffix {\mathrel{\mathsf{suffix}}}
+\def \inseq {\mathrel{\mathsf{in}}}
+\def \extract {\mathrel{\upharpoonleft}}
+
+\def \uminus@sym{\setbox0=\hbox{$\cup$}\rlap{\hbox
+ to\wd0{\hss\raise0.3ex\hbox{$\scriptscriptstyle{-}$}\hss}}\box0}
+\def \uminus {\mathrel{\uminus@sym}}
+
+% If you are not using csp notation, then feel free to uncomment the
+% following:
+
+% \endinput
+
+
+% >>> 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 {\strut@op{\mathrm{begin}}}
+\def \End {\strut@op{\mathrm{end}}}
+\def \Head {\strut@op{\mathrm{head}}}
+\def \First {\strut@op{\mathrm{first}}}
+\def \Tail {\strut@op{\mathrm{tail}}}
+\def \Front {\strut@op{\mathrm{front}}}
+\def \Last {\strut@op{\mathrm{last}}}
+\def \Times {\strut@op{\mathrm{times}}}
+\def \Events {\strut@op{\mathrm{events}}}
+\def \Reverse {\strut@op{\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 \Chaos {{Chaos}}
+\def \Stop {{Stop}}
+\def \Skip {{Skip}}
+\def \Wait {\strut@op{{Wait}}}
+\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]{\,\ldbrack #1 \rdbrack}
+\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{{\ldbrack #1 \rdbrack}}
+
+% 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
diff --git a/macros/latex/contrib/zed-csp/zed2e.pdf b/macros/latex/contrib/zed-csp/zed2e.pdf
new file mode 100644
index 0000000000..0f6daf8654
--- /dev/null
+++ b/macros/latex/contrib/zed-csp/zed2e.pdf
Binary files differ
diff --git a/macros/latex/contrib/zed-csp/zed2e.tex b/macros/latex/contrib/zed-csp/zed2e.tex
new file mode 100644
index 0000000000..ae6a4d41e6
--- /dev/null
+++ b/macros/latex/contrib/zed-csp/zed2e.tex
@@ -0,0 +1,774 @@
+% STOLEN VERSION of ``zguide.tex'' 11th December 1990
+% Copyright (C) J. M. Spivey 1990
+
+% The zed style option and its documentation may be freely copied,
+% distributed and used for any purpose except direct commercial gain,
+% provided that they are copied and distributed as a whole and without
+% modification. The author accepts no liablility for their accuracy or
+% fitness for any purpose.
+
+\documentclass{article}
+
+\usepackage{zed-csp}
+
+\def\fuzz{{\large\it f\kern0.1em}{\normalsize\sc uzz}}
+\let\Fuzz=\fuzz
+\def\ZRM{{\rm ZRM}}
+
+\makeatletter % Oh-ho: here comes some more lark's vomit ...
+
+\def\demo{\par\vbox\bgroup\begingroup\quote}
+\def\gives{\endquote\endgroup\egroup}
+\def\enddemo{\global\@ignoretrue}
+
+% Try doing this in pure LaTeX without `visual formatting'!
+\def\symtab{\setbox0=\vbox\bgroup \def\\{\cr}
+ \halign\bgroup\strut$##$\hfil&\quad##\hfil\cr}
+\def\endsymtab{\crcr\egroup\egroup
+ \dimen0=\ht0 \divide\dimen0 by2 \advance\dimen0 by\ht\strutbox
+ \splittopskip=\ht\strutbox \vbadness=10000
+ \predisplaypenalty=0
+ $$\halign{##\cr\hbox to\linewidth{%
+ \valign{##\vfil\cr
+ \setbox1=\vsplit0 to\dimen0 \unvbox1\cr
+ \noalign{\hfil}\unvbox0\cr
+ \noalign{\hfil}}}\cr
+ \noalign{\prevdepth=\dp\strutbox}}$$
+ \global\@ignoretrue}
+
+\makeatother % Sanity is restored
+
+\begin{document}
+
+\title{A guide to the {\tt zed} style option}
+\author{Mike Spivey}
+\date{December 1990}
+\maketitle
+
+\section{Introduction}
+
+This document is a guide to the version of the {\tt zed} style option
+for \LaTeX\ dated 11th December 1990. This new version of the style
+option is fully compatible with the {\tt fuzz} style option
+distributed with the my \fuzz\ type-checker for Z, but uses two fonts
+from the AMS in place of the special Z font distributed with
+\fuzz. Some of the symbols have been cobbled together by combining
+two or more characters, but the results are good enough for rough
+drafts. The style option requires the `old' AMS fonts, and will not at
+present work with Sli\TeX\ or the Sch\"opf-Mittelbach font selection
+scheme.
+
+The rest of this guide is mostly extracted from the manual for \fuzz,
+and it assumes a basic knowledge of \LaTeX. I have not removed some
+information about how the \fuzz\ type-checker treats various
+constructs, in case you later want to type-check a document you have
+formatted with the {\tt zed} style option. For information about the
+\fuzz\ package and how to order it, see the end of this guide.
+
+This guide and the {\tt zed} style option itself may be freely copied,
+distributed and used for any purpose except direct commercial gain,
+provided that they are copied and distributed as a whole and without
+modification. The author accepts no liablility for their accuracy or
+fitness for any purpose.
+
+\section{Loading the {\tt zed} style option}
+
+Every \LaTeX\ document should begin with a \verb/\documentstyle/
+command. If the document contains a Z specification, this command
+should include the style option \verb/zed/. For example:
+\begin{quote}
+ \verb/\documentstyle[12pt,zed]{article}/
+\end{quote}
+Including \verb/zed/ as a style option loads macros from the file
+\verb/zed.sty/ and also loads four fonts of extra mathematical symbols
+called \verb/msxm9/, \verb/msym9/, \verb/msxm10/, and \verb/msym10/.
+Your \LaTeX\ installation must have these fonts for the \verb/zed/
+style option to work; if it doesn't, or they are in the wrong place to
+be found by \TeX, then you will get an error message like this:
+\begin{quote}
+ \verb/! Font \ninsxm=msxm9 not loadable .../
+\end{quote}
+The \verb/zed/ style option can be used with any of the standard
+\LaTeX\ styles, and it can appear either before or after the type-size
+option if one is used. It can be combined with most of the standard
+style options, but it should not be combined with \verb/fleqn/,
+because {\tt zed} already makes provision for setting mathematics
+flush left. At present, \verb/zed/ does not work with Sli\TeX.
+
+\section{Making boxes}
+
+To print a schema, use the \verb/schema/ environment. Here is an
+example, showing first the input, then the output from \LaTeX:
+\begin{demo}
+\begin{verbatim}
+\begin{schema}{PhoneDB}
+ known: \power NAME \\ phone: NAME \pfun PHONE
+\where
+ known = \dom phone
+\end{schema}
+\end{verbatim}
+\gives
+\begin{schema}{PhoneDB}
+ known: \power NAME \\ phone: NAME \pfun PHONE
+\where
+ known = \dom phone
+\end{schema}
+\end{demo}
+The name of the schema appears as an argument to the environment, and
+the horizontal dividing line between declarations and predicates is
+indicated by \verb/\where/. Successive lines in the declaration and
+predicate parts are separated by the command \verb/\\/. In this
+example, the Z symbols `$\power$', `$\pfun$' and `$\dom$' have been
+entered as the commands \verb/\power/, \verb/\pfun/ and \verb/\dom/:
+for a complete list of these commands, see Section~\ref{s:symtabs}
+below.
+
+Like the \verb/displaymath/ environment of \LaTeX, the \verb/schema/
+environment (and the others we shall come to in a moment) can appear
+in the middle of a paragraph, and ordinarily should have no blank
+lines either before or after it. Blank lines before the environment
+are ignored, but blank lines afterwards cause the following text to
+begin a new paragraph.
+
+For a schema without a predicate part, the command \verb/\where/ is
+simply omitted, as in the following example:
+\begin{demo}
+\begin{verbatim}
+\begin{schema}{Document[CHAR]}
+ left, right: \seq CHAR
+\end{schema}
+\end{verbatim}
+\gives
+\begin{schema}{Document[CHAR]}
+ left, right: \seq CHAR
+\end{schema}
+\end{demo}
+This example also shows how to set schemas with generic parameters.
+
+For axiomatic descriptions, the \verb/axdef/ environment is used.
+Here is an example:
+\begin{demo}
+\begin{verbatim}
+\begin{axdef}
+ limit: \nat
+\where
+ limit \leq 65535
+\end{axdef}
+\end{verbatim}
+\gives
+\begin{axdef}
+ limit: \nat
+\where
+ limit \leq 65535
+\end{axdef}
+\end{demo}
+In both kinds of box, predicates and declarations can be split between
+lines before or after infixed symbols, as shown in the following
+example:
+\begin{demo}
+\begin{verbatim}
+\begin{axdef}
+ policy: \power_1 RESOURCE \fun RESOURCE
+\where
+ \forall S: \power_1 RESOURCE @ \\
+\t1 policy(S) \in S
+\end{axdef}
+\end{verbatim}
+\gives
+\begin{axdef}
+ policy: \power_1 RESOURCE \fun RESOURCE
+\where
+ \forall S: \power_1 RESOURCE @ \\
+\t1 policy(S) \in S
+\end{axdef}
+\end{demo}
+The strange hint \verb/\t1/ in this example makes the corresponding
+line in the output have one helping of indentation. As things get
+more nested, you can say \verb/\t2/, \verb/\t3/, and so on. But if
+you should ever get beyond \verb/t9/, you'll need to use braces around
+the argument: \verb/\t{10}/, and you'd better look for some way to
+simplify your specification!
+
+This system of tab stops is a little crude, but it is easier to use
+than the alternatives, and usually gives acceptable results. The
+\verb/\t/$n$ commands are completely ignored by the type-checker,
+so you are free to use them as you like to improve the look of your
+specification. The size of `helping' you get with
+\verb/\t/$n$ is a style parameter \verb/\zedindent/, and the default
+is 2em.
+
+For generic definitions, there's the \verb/gendef/ environment: for
+example,
+\begin{demo}
+\begin{verbatim}
+\begin{gendef}[X,Y]
+ first: X \cross Y \fun X
+\where
+ \forall x: X; y: Y @ \\
+\t1 first(x,y) = x
+\end{gendef}
+\end{verbatim}
+\gives
+\begin{gendef}[X,Y]
+ first: X \cross Y \fun X
+\where
+ \forall x: X; y: Y @ \\
+\t1 first(x,y) = x
+\end{gendef}
+\end{demo}
+In this environment, the formal generic parmeters are an optional
+argument. Omitting this argument results in a box with a solid double
+bar at the top, which can be used for uniquely defining non-generic
+constants.
+
+If a schema or other box contains more than one predicate below the
+line, it often looks better to add a small vertical space between
+them. This can be done with the command \verb/\also/:
+\begin{demo}
+\begin{verbatim}
+\begin{schema}{AddPhone}
+ \Delta PhoneDB \\ name?: NAME \\ number?: PHONE
+\where
+ name? \notin known
+\also
+ phone' = phone \oplus \{name? \mapsto number?\}
+\end{schema}
+\end{verbatim}
+\gives
+\begin{schema}{AddPhone}
+ \Delta PhoneDB \\ name?: NAME \\ number?: PHONE
+\where
+ name? \notin known
+\also
+ phone' = phone \oplus \{name? \mapsto number?\}
+\end{schema}
+\end{demo}
+
+Some Z paragraphs do not appear in boxes, and for these the \verb/zed/
+environment is used:
+\begin{demo}
+\begin{verbatim}
+\begin{zed}
+ [NAME, DATE]
+\also
+ REPORT ::= ok | unknown \ldata NAME \rdata
+\also
+ \exists n: NAME @ \\
+\t1 birthday(n) \in December.
+\end{zed}
+\end{verbatim}
+\gives
+\begin{zed}
+ [NAME, DATE]
+\also
+ REPORT ::= ok | unknown \ldata NAME \rdata
+\also
+ \exists n: NAME @ \\
+\t1 birthday(n) \in December.
+\end{zed}
+\end{demo}
+This environment should be used for basic type definitions,
+constraints, abbreviation definitions, free type definitions, and the
+horizontal form of schema definitions. As the example illustrates, a
+full stop or comma is allowed just before the closing \verb/\end/
+command of any of the Z environments, if that suits your taste (or is
+forced on you by a publisher's house rules). This punctuation is
+ignored by the type-checker.
+
+For large free type definitions, the \verb/syntax/ environment
+provides a useful alternative to the \verb/zed/ environment, as the
+following example suggests:
+\begin{demo}
+\begin{verbatim}
+\begin{syntax}
+ OP & ::= & plus | minus | times | divide
+\also
+ EXP & ::= & const \ldata \nat \rdata \\
+ & | & binop \ldata OP \cross EXP \cross EXP \rdata
+\end{syntax}
+\end{verbatim}
+\gives
+\begin{syntax}
+ OP & ::= & plus | minus | times | divide
+\also
+ EXP & ::= & const \ldata \nat \rdata \\ & | & binop \ldata OP
+\cross EXP \cross EXP \rdata
+\end{syntax}
+\end{demo}
+Just as in the \verb/eqnarray/ environment of \LaTeX, the fields are
+separated by \verb/&/ characters, and these are ignored by the
+type-checker.
+
+\section{Inside the boxes}\label{s:symtabs}
+
+The first thing to notice about the text inside the boxes is that
+multi-character identifiers look better than they do with ordinary
+\LaTeX: instead of $\mit specifications$, you get $specifications$.
+The letters are not spread apart, and ligatures like $fi$ are used.
+This is achieved by an adjustment to the way \TeX\ treats letters in
+mathematical formulas, and no special commands are needed in the input
+file. Embedded underline characters can be set with the \verb/\_/
+command, which is also used for dummy arguments of operators:
+\verb/not\_known/ gives $not\_known$, and \verb/\_ + \_/ gives
+$\_ + \_$~.
+
+The various special symbols of the Z language and library have
+mnemonic names. Some of these names are the same as in ordinary
+\LaTeX, and some symbols have new names more suggestive of their
+meaning in Z. The spaces inserted around the symbols have been
+adjusted to make them look better in Z specifications.
+
+A few symbols have two names, reflecting two different uses for the
+symbol in Z. The symbol $\semi$ is called \verb/\semi/ when it is used
+as an operation on schemas, and \verb/\comp/ when it is used for
+composition of relations. The symbol $\hide$ is called \verb/\hide/ as
+the hiding operator of the schema calculus, and \verb/\setminus/ for
+the set difference operator. The symbol $\project$ is called
+\verb/project/ as the schema projection operator, and \verb/\filter/
+for filtering of sequences. The spaces around the schema operations
+are a little larger, and the type-checker recognizes each name only in
+the appropriate context.
+
+For most symbols, two attributes are of interest: the syntactic class
+({\sf In-Fun}, \dots) assigned to it by the type-checker, and the kind
+of symbol \LaTeX\ generates from it. The first of these affects the
+parsing of an expression containing the symbol, and the second affects
+the way spaces will be inserted when the expression is printed. In the
+description below, `thin', `medium' and `thick' spaces are the same as
+those produced by the \LaTeX\ commands \verb/\,/ and \verb/\:/ and
+\verb/\;/ respectively.
+
+Here are the mnemonics for the basic elements of the Z language:
+\begin{symtab}
+ \power & \verb/\power/ \\
+ \cross & \verb/\cross/ \\
+ \in & \verb/\in/ \\
+ | & \verb/|/ or \verb/\mid/ \\
+ @ & \verb/@/ or \verb/\spot/ \\
+ \theta & \verb/\theta/ \\
+ \lambda & \verb/\lambda/ \\
+ \mu & \verb/\mu/ \\
+ \Delta & \verb/\Delta/ \\
+ \Xi & \verb/\Xi/ \\
+ \defs & \verb/\defs/
+\end{symtab}
+The operators of propositional logic and the schema calculus are as
+follows. Many of these names are already defined by \LaTeX, but the
+spacing is often adjusted to make them look better in Z
+specifications.
+\begin{symtab}
+ \lnot & \verb/\lnot/ \\
+ \land & \verb/\land/ \\
+ \lor & \verb/\lor/ \\
+ \implies & \verb/\implies/ \\
+ \iff & \verb/\iff/ \\
+ \forall & \verb/\forall/ \\
+ \exists & \verb/\exists/ \\
+ \exists_1 & \verb/\exists_1/ \\
+ \hide & \verb/\hide/ \\
+ \project & \verb/\project/ \\
+ \pre & \verb/\pre/ \\
+ \semi & \verb/\semi/
+\end{symtab}
+Here are the various sorts of fancy brackets:
+\begin{symtab}
+ \{\ldots\} & \verb/\{ ... \}/ \\
+ \langle\ldots\rangle & \verb/\langle ... \rangle/ \\
+ \lbag\ldots\rbag & \verb/\lbag ... \rbag/ \\
+ \ldata\ldots\rdata & \verb/\ldata ... \rdata/ \\
+ \ldots\limg\ldots\rimg & \verb/... \limg ... \rimg/
+\end{symtab}
+Those are all the symbols `built-in' to the Z language; now for the
+symbols defined as part of the mathematical tool-kit. First come the
+symbols which are not defined as infix operators, etc.:
+\begin{symtab}
+ \empty & \verb/\empty/ \\
+ \bigcup & \verb/\bigcup/ \\
+ \bigcap & \verb/\bigcap/ \\
+ \dom & \verb/\dom/ \\
+ \ran & \verb/\ran/ \\
+ \nat & \verb/\nat/ \\
+ \num & \verb/\num/ \\
+ \nat_1 & \verb/\nat_1/ \\
+ \# & \verb/\#/ \\
+ \dcat & \verb/\dcat/
+\end{symtab}
+Here are the infix function symbols; they are defined in \LaTeX\ as
+binary operators, so medium spaces are inserted automatically. The
+type-checker recognizes them as of class {\sf In-Fun}. Each symbol is
+shown with its priority:
+\begin{symtab}
+ \mapsto & \verb/\mapsto/\quad\hfill 1 \\
+ \upto & \verb/\upto/\quad\hfill 2 \\
+ + & \verb/+/\quad\hfill 3 \\
+ - & \verb/-/\quad\hfill 3 \\
+ \cup & \verb/\cup/\quad\hfill 3 \\
+ \setminus & \verb/\setminus/\quad\hfill 3 \\
+ \cat & \verb/\cat/\quad\hfill 3 \\
+ \uplus & \verb/\uplus/\quad\hfill 3 \\
+ * & \verb/*/\quad\hfill 4 \\
+ \div & \verb/\div/\quad\hfill 4 \\
+ \mod & \verb/\mod/\quad\hfill 4 \\
+ \cap & \verb/\cap/\quad\hfill 4 \\
+ \comp & \verb/\comp/\quad\hfill 4 \\
+ \circ & \verb/\circ/\quad\hfill 4 \\
+ \filter & \verb/\filter/\quad\hfill 4 \\
+ \oplus & \verb/\oplus/\quad\hfill 5 \\
+ \dres & \verb/\dres/\quad\hfill 6 \\
+ \rres & \verb/\rres/\quad\hfill 6 \\
+ \ndres & \verb/\ndres/\quad\hfill 6 \\
+ \nrres & \verb/\nrres/\quad\hfill 6
+\end{symtab}
+The postfix function symbols (class {\sf Post-Fun}) all produce
+superscripts:
+\begin{symtab}
+ \inv & \verb/\inv/ \\
+ \plus & \verb/\plus/ \\
+ \star & \verb/\star/ \\
+ \bsup n \esup & \verb/\bsup n \esup/
+\end{symtab}
+As an example, \verb/R \star/ is printed as $R \star$. For iteration,
+the commands \verb/\bsup ... \esup/ should be used: for example,
+\verb/R \bsup n \esup/ is printed as $R \bsup n \esup$. The
+type-checker regards this formula as equivalent to $iter~n~R$, as
+explained on page 112 of the \ZRM.
+
+The infix relation symbols (class {\sf In-Rel}) are defined in
+\LaTeX\ as relations, so thick spaces are inserted around them
+automatically:
+\begin{symtab}
+ \neq & \verb/\neq/ \\
+ \notin & \verb/\notin/ \\
+ \subseteq & \verb/\subseteq/ \\
+ \subset & \verb/\subset/ \\
+ < & \verb/</ \\
+ > & \verb/>/ \\
+ \leq & \verb/\leq/ \\
+ \geq & \verb/\geq/ \\
+ \partition & \verb/\partition/ \\
+ \inbag & \verb/\inbag/ \\
+\end{symtab}
+There is only one prefix relation symbol (class {\sf Pre-Rel}). It
+separates itself from an argument with a thick space:
+\begin{symtab}
+ \disjoint & \verb/\disjoint/
+\end{symtab}
+The infix generic symbols are seen by \LaTeX\ as relation symbols, so
+they are surrounded by thick spaces. Of course, the type-checker
+itself assigns them class {\sf In-Gen}:
+\begin{symtab}
+ \rel & \verb/\rel/ \\
+ \pfun & \verb/\pfun/ \\
+ \fun & \verb/\fun/ \\
+ \pinj & \verb/\pinj/ \\
+ \inj & \verb/\inj/ \\
+ \psurj & \verb/\psurj/ \\
+ \surj & \verb/\surj/ \\
+ \bij & \verb/\bij/ \\
+ \ffun & \verb/\ffun/ \\
+ \finj & \verb/\finj/
+\end{symtab}
+Prefix generic symbols are assigned class {\sf Pre-Gen} by the
+type-checker; in \LaTeX, they are defined as operator symbols, so that
+a thin space is inserted between the symbol and a following generic
+parameter:
+\begin{symtab}
+ \power_1 & \verb/\power_1/ \\
+ \id & \verb/\id/ \\
+ \finset & \verb/\finset/ \\
+ \finset_1 & \verb/\finset_1/ \\
+ \seq & \verb/\seq/ \\
+ \seq_1 & \verb/\seq_1/ \\
+ \iseq & \verb/\iseq/ \\
+ \bag &
+\verb/\bag/
+\end{symtab}
+
+\section{Fine points}
+
+In math mode, which is used for type-setting the contents of Z boxes,
+\TeX\ ignores all space characters in the input file. The spaces which
+appear between elements of a mathematical formula are determined by
+\TeX\ itself, working from information about the symbols in the
+formula. Although this information has been adjusted in the {\tt zed}
+style option to make Z texts look as balanced as possible, there are
+one or two situations in which \TeX\ needs a little help.
+
+Special care is needed when function application is indicated by
+juxtaposing two identifiers, as in the expression $rev~words$. This
+expression should be typed as %
+\verb/rev~words/. Typing just %
+\verb/rev words/ results in the output $rev words$, since \TeX\ ignores the
+space separating the two identifiers. In a formula, the character
+%
+\verb/~/ inserts the same amount of space as the \LaTeX\ %
+\verb/\,/
+command, but it looks better in the input file. The type-checker
+completely ignores both the %
+\verb/~/ character and the \LaTeX\ spacing
+commands, except that it issues a warning if it finds that a needed
+one is missing, for example, between two identifiers. It is not
+necessary to separate symbols like %
+\verb/\dom/ and %
+\verb/\ran/ from
+their arguments with a %
+\verb/~/, because \TeX\ inserts the right
+amount of space automatically. For example, the input %
+\verb/\dom f/
+produces $\dom f$.
+
+It is good style also to insert small spaces inside the braces of a
+set comprehension, as in this example:
+\begin{demo}
+%
+\verb/\{~x: \nat | x \leq 10 @ x * x~\}/
+\gives
+\[\{~x: \nat | x \leq 10 @ x * x~\}\]
+\end{demo}
+This helps to distinguish it visually from a set display, which should
+not have the space:
+\begin{demo}
+%
+\verb/\{1, 2, 3\}/
+\gives
+\[\{1, 2, 3\}\]
+\end{demo}
+The space symbol %
+\verb/~/ is ignored by the type-checker, so this is
+purely a matter of appearance. It also looks better if you add small
+spaces inside the square brackets of `horizontal' schema texts.
+
+\TeX\ also needs help when a binary operator appears at the end of a
+line, as in the following example:
+\begin{demo}
+\begin{verbatim}
+\begin{zed}
+ directory' = directory \cup {} \\
+\t3 \{new\_name? \mapsto new\_number?\}
+\end{zed}
+\end{verbatim}
+\gives
+\begin{zed}
+ directory' = directory \cup {} \\
+\t3 \{new\_name? \mapsto new\_number?\}
+\end{zed}
+\end{demo}
+\TeX\ will not recognize %
+\verb/\cup/ as a binary operator and insert
+the correct space unless it is surrounded by two operands, so the
+dummy operand %
+\verb/{}/ has been inserted: this is ignored by the
+type-checker. This problem affects only binary operators; relation
+signs do not need to be surrounded by arguments to be recognized by
+\TeX.
+
+\section{Bits and pieces}
+
+Specification documents often contain mathematical text which does not
+form part of the specification proper. This section describes some
+environments for setting various kinds of mathematics; they are
+provided for convenience, and they are all ignored by the
+type-checker. Besides these environments for making displays, run-in
+mathematics can be set with the usual %
+\verb/math/ environment, or with
+the commands %
+\verb/$ ... $/ or \hbox{%
+\verb/\( ... \)/}. All the Z
+symbols listed in Section~\ref{s:symtabs} can be used with these
+commands.
+
+The simplest display environment is provided by the commands
+%
+\verb/\[ ... \]/. This form acts just like %
+\verb/\begin{zed} ... \end{zed}/, except that the contents are ignored by the
+type-checker. Here is an example:
+\begin{demo}
+\begin{verbatim}
+\[
+ \exists PhoneDB @ \\
+\t1 known = \empty
+\]
+\end{verbatim}
+\gives
+\[
+ \exists PhoneDB @ \\
+\t1 known = \empty
+\]
+\end{demo}
+These commands generalize the standard \LaTeX\ commands with the same
+name, because the displayed material can be several lines. Note,
+however, that the contents are set as text style rather than display
+style mathematics.
+
+A schema box with no name is generated by the %
+\verb/schema*/
+environment:
+\begin{demo}
+\begin{verbatim}
+\begin{schema*}
+ x, y: \nat
+\where
+ x > y
+\end{schema*}
+\end{verbatim}
+\gives
+\begin{schema*}
+ x, y: \nat
+\where
+ x > y
+\end{schema*}
+\end{demo}
+This form is often useful for showing the result of expanding a
+complex schema-expression.
+
+Another kind of mathematical display is provided by the %
+\verb/argue/
+environment. This is like the %
+\verb/zed/ environment, but the
+separation between lines is increased a little, and page breaks may
+occur between lines. The intended use is for arguments like this:
+\begin{demo}
+\begin{verbatim}
+\begin{argue}
+ S \dres (T \dres R) \\
+\t1 = \id S \comp \id T \comp R \\
+\t1 = \id (S \cap T) \comp R & law about $\id$ \\
+\t1 = (S \cap T) \dres R.
+\end{argue}
+\end{verbatim}
+\gives
+\begin{argue}
+ S \dres (T \dres R) \\
+\t1 = \id S \comp \id T \comp R \\
+\t1 = \id (S \cap T) \comp R & law about $\id$ \\
+\t1 = (S \cap T) \dres R.
+\end{argue}
+\end{demo}
+When the left-hand side is long, I find this style better than the
+\LaTeX\ %
+\verb/eqnarray/ style, which wastes a lot of space. The second
+field on each line is optional. Again, the %
+\verb/argue/ environment is
+ignored by the type-checker.
+
+Finally, there is the %
+\verb/infrule/ environment, used for inference
+rules:
+\begin{demo}
+\begin{verbatim}
+\begin{infrule}
+ \Gamma \shows P
+\derive[x \notin freevars(\Gamma)]
+ \Gamma \shows \forall x @ P
+\end{infrule}
+\end{verbatim}
+\gives
+\begin{infrule}
+ \Gamma \shows P
+\derive[x \notin freevars(\Gamma)]
+ \Gamma \shows \forall x \spot P
+\end{infrule}
+\end{demo}
+The horizontal line is generated by %
+\verb/\derive/; the optional
+argument is a side-condition of the rule.
+
+\section{Style parameters}
+
+A few style parameters affect the way Z text is set out; they can be
+changed at any time if your taste doesn't match mine.
+
+\begin{description}
+\item[\tt\string\zedindent] The indentation for mathematical text.
+ By default, this is the same as %
+\verb|\leftmargini|, the indentation
+ used for list environments.
+\item[\tt\string\zedleftsep] The space between the vertical line on the left
+ of schemas, etc., and the maths inside. The default is 1em.
+\item[\tt\string\zedtab] The unit of indentation used by %
+\verb|\t|. The default
+ is 2em.
+\item[\tt\string\zedbar] The length of the horizontal bar in the middle of a
+ schema. The default is 6em.
+\item[\tt\string\zedskip] The vertical space inserted by
+ %
+\verb/\also/. By default, this is the same as that inserted by
+ %
+\verb/\medskip/.
+\end{description}
+
+\newpage
+\section{The fuzz package}
+
+The \fuzz\ package consists of two parts -- a style option compatible
+with the {\tt zed} style option described here, and an analysis and
+checking program. Using \fuzz\ together with \LaTeX, you can:
+\begin{itemize}
+\item Input Z specifications as ordinary ASCII files.
+\item Process them for laser printing or photo-typesetting.
+\item Check them for conformance with the Z language rules.
+\item Produce a listing showing the schemas in the specification with
+ components and their types.
+\end{itemize}
+The \fuzz\ analysis program works on the same ASCII file as \LaTeX; it
+extracts the formal text and checks it for conformance with the rules
+of the Z language, producing clear error messages. Analysis of a
+1300-line specification takes about 7 seconds on a SUN 3/75.
+
+The \fuzz\ distribution contains the \LaTeX\ style option, a special
+font of Z symbols, object code for the analysis program, a library
+containing the standard mathematical tool-kit, and some example
+specifications. To use \fuzz, you will need to have \LaTeX\ installed
+on your machine, but everything else you need is included. \fuzz\ is
+currently available under `no-nonsense' licence conditions for the IBM
+PC and other DOS machines, and for the SUN 3 and SUN 4 under SUN UNIX.
+The PC version can also be used on the PS/2. We are willing to
+produce versions for other machines according to demand.
+
+\newpage
+\thispagestyle{empty}
+\section*{Ordering information}
+
+You can order the \fuzz\ package either by cutting out the coupon
+below and sending it with your payment, or by sending an official
+order -- we will send an invoice. Please send all orders to the
+address below. Technical enquiries can be sent to Mike Spivey at the
+same address, or by E-mail to {\tt mike@uk.ac.oxford.prg} .
+
+\vfill
+{\center\large\bf \Fuzz\ package: order form\par}
+\bigskip
+\noindent To: Mrs.\ A. Spivey, 34, Westlands Grove, Stockton Lane,
+\hfil\break\hphantom{To: }York, YO3 0EF, England.
+\par\bigskip
+\newdimen\x \setbox0=\hbox{Telephone:} \x=\wd0
+\begingroup
+\baselineskip=24pt
+\def\addrline#1{\hbox to\linewidth{\hbox to\x{#1\hfil}\qquad\hrulefill}}
+\addrline{Name:}
+\addrline{Address:}
+\addrline{}
+\addrline{}
+\addrline{Telephone:}
+\endgroup
+\bigskip
+\noindent Please send [\qquad] copies of the \fuzz\ package for the
+following machines:
+\par\bigskip
+\halign{\hskip\x\qquad#\hfil\qquad&#\qquad\hfil&#\hfil\cr
+ [\quad]& SUN 3 version: Cartridge tape& \pounds 300\cr
+ \noalign{\medskip}
+ [\quad]& SUN 4 version: 3.5in disk& \pounds 275\cr
+ \noalign{\medskip}
+ [\quad]& SUN 4 version: Cartridge tape& \pounds 300\cr
+ \noalign{\medskip}
+ [\quad]& IBM PC version: 5.25in disk& \pounds 200\cr
+ \noalign{\medskip}
+ [\quad]& IBM PC version: 3.5in disk& \pounds 200\cr}
+\bigskip
+\noindent I enclose a cheque for \pounds [\qquad], payable to
+Dr.\ J. M.~Spivey.
+\par\bigskip\noindent
+Signed:
+\par\bigskip
+\end{document}