%% This is file `czt.sty',
%% generated with the docstrip utility.
%%
%% The original source files were:
%%
%% czt.dtx  (with options: `package')
%%
%% This is a generated file
%%
%% Copyright (C) 2008 Leo Freitas.
%% University of York All rights reserved.
%%
%% This is a generated file for Standard Z within the
%% Community Z Tools (CZT). It is based on the Object Z
%% package distribution.  Permission is granted to to
%% customize the declarations in this file to serve the
%% needs of your installation.  However, no permission
%% is granted to distribute a modified version of this
%% file under its original name.
%%
\def\fileversion{v.1.4}
\def\filedate{2015/07/23}
\def\filedesc{Standard Z style file by the Community Z Tools}

\NeedsTeXFormat{LaTeX2e}[1999/12/01]
\ProvidesPackage{czt}
    [\filedate\space\fileversion\space \filedesc]
\message{`\filedesc'\space \fileversion\space <\filedate>}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Design guidelines:
%   1) keep it minimal + simple + consistent
%   2) for machine readable Standard Z only
%   3) identify code sources (when different)
%   4) normalise definitions for consistency
%   5) complete missing cases (use common sense)
%   6) keep it well documented, but not verbose
%   7) follow order of definitions from Z Standard document
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Package options - zed.sty (old version of zed-csp.sty)        %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                                                               %

% create conditionals for each option available, init=false
\newif\if@lucida@    \@lucida@false
\newif\if@color@     \@color@false
\newif\if@mathit@    \@mathit@false
\newif\if@mathrm@    \@mathrm@false
\newif\if@tkkeyword@ \@tkkeyword@false

\newif\if@cntglobally@ \@cntglobally@false
\newif\if@cntbychapter@ \@cntbychapter@false
\newif\if@cntbysection@ \@cntbysection@false

% declare what each option actually do - colour=synonym(color)
\DeclareOption{lucida}{\PackageInfo{czt}{'lucidda' option chosen} \@lucida@true}
\DeclareOption{color}{\PackageInfo{czt}{'color' option chosen} \@color@true}
\DeclareOption{colour}{\PackageInfo{czt}{'color' option chosen} \@color@true}
\DeclareOption{mathit}{\PackageInfo{czt}{'mathit' option chosen} \@mathit@true \@mathrm@false}
\DeclareOption{mathrm}{\PackageInfo{czt}{'mathrm' option chosen} \@mathit@false \@mathrm@true}
\DeclareOption{tkkeyword}{\PackageInfo{czt}{'tkkeyword' option chosen} \@tkkeyword@true}

% way to handle paragraph counting
\DeclareOption{cntglobally}{\PackageInfo{czt}{'cntglobally' option chosen} \@cntglobally@true  \@cntbychapter@false \@cntbysection@false}
\DeclareOption{cntbychapter}{\PackageInfo{czt}{'cntbychapter' option chosen} \@cntglobally@false \@cntbychapter@true  \@cntbysection@false}
\DeclareOption{cntbysection}{\PackageInfo{czt}{'cntbysection' option chosen} \@cntglobally@false \@cntbychapter@false \@cntbysection@true}

% default option as using math italics for mathcode names.
%\ExecuteOptions{mathit,cntglobally}
\ProcessOptions\relax

% if Lucida Bright is chosen, then load the package with necessary dependencies
\if@lucida@
  \@ifpackageloaded{lucidabr}{%
      \PackageInfo{czt}{Lucida Bright already loaded}
    }{%
      \PackageInfo{czt}{Loading Lucida Bright with `expert' and `altbullet' options.\MessageBreak %
          We also require the `texnansi' package}
      \RequirePackage{texnansi}
      \RequirePackage[expert,altbullet]{lucidabr}
    }
\else
   \PackageInfo{czt}{AMS fonts selected with default options}
\fi

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Treating colours                                              %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                                                               %

% If colouring is available
\if@color@
  \PackageInfo{czt}{Rendering Z math mode with colours}

  % check whether to load color package or not
  \@ifpackageloaded{color}{%
        \relax
  }{%
        \PackageInfo{czt}{Package `color' loaded with `dvipsnames' \MessageBreak and `usenames' options}
        \RequirePackage[dvipsnames,usenames]{color}
  }

  % define some nice colours to use within Z declarations
  %
  %\definecolor{ZedBoxColor}{cmyk}{0.99,0,0.52,0}
  \definecolor{ZedBoxColor}{cmyk}{1,1,0,0}
  \definecolor{AnnotationColor}{cmyk}{0.98,0.13,0,0.43}
  \definecolor{ZedColor}{cmyk}{0.50,1,0,0}
  % add more color here if needed

  \PackageInfo{czt}{Z colours defined as:\MessageBreak%
    \space\space ZedBoxColor\space\space\space\space\space                = cmyk(   1,   1,0,   0) \MessageBreak%
    \space\space AnnotationColor                                          = cmyk(0.98,0.13,0,0.43) \MessageBreak%
    \space\space ZedColor\space\space\space\space\space\space\space\space = cmyk(0.50,   1,0,   0) \MessageBreak%
  }

\else
  \PackageInfo{czt}{Rendering Z math mode in monochrome.}
  % if color is loaded do nothing, otherwise redefine \color as empty
  \@ifpackageloaded{color}{\relax}{\def\color#1{\relax}}%
\fi

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Some needed markers used in some symbols - font independant   %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                                                               %

% horizontal raised bar: used for negated \dres\rres
\def\zmark@hbar#1{\rlap{\raise.0001ex\hbox{$-$}}{#1}}

% vertical raised bar: used for partial and finite markings. #1=symbol
\def\zmark@pvbar#1{\ooalign{\hfil$\mapstochar\mkern 5mu$\hfil\cr$#1$}}
\def\zmark@fvbar#1{\ooalign{\hfil$\mapstochar\mkern 3mu\mapstochar\mkern 5mu$\hfil\cr$#1$}}

% doubled arrow function symbols. symbol = #1/#3; space delta = #2
% surjection (#1=\fun, #2=4mu, #3=\fun); bijection (#1=\inj, #2=5mu, #3=\fun)
\def\zmark@darrow#1#2#3{\ooalign{$#1$\hfil\cr$\mkern#3mu#2$}}

%                                                               %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Loading mathematical symbols from AMS/Lucuida fonts           %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                                                               %

% declares the math version for fonts as czt
\DeclareMathVersion{czt}
\PackageInfo{czt}{Creating `czt' math version}

% Selects St. Mary's Road symbol package font
\DeclareSymbolFont{stmry}{U}{stmry}{m}{n}

% Specify aliases for mathematical operator categories
\DeclareSymbolFontAlphabet{\mathrm}{operators}
\DeclareSymbolFontAlphabet{\mathit}{letters}
\DeclareSymbolFontAlphabet{\mathcal}{symbols}

% Some math alphabet defaults regardless of the chosen font
\SetMathAlphabet{\mathrm}{czt}{\encodingdefault}{\rmdefault}{m}{n}%
\SetMathAlphabet{\mathbf}{czt}{\encodingdefault}{\rmdefault}{bx}{n}%
\SetMathAlphabet{\mathsf}{czt}{\encodingdefault}{\sfdefault}{m}{n}%

% set symbol font italics for both Lucida and AMS fonts
% this changes the behaviour of \symitalics
\DeclareSymbolFont{italics}{\encodingdefault}{\rmdefault}{m}{it}%
\DeclareSymbolFontAlphabet{\zit}{italics}

% Saved symbols with other names
\let\mathemptyset=\emptyset % save old \emptyset set version
\let\mathdiv=\div           % save the math division symbol
\let\mathstar=\star         % save old \star version

% Loading symbols conditionally to Lucida Bright / AMS .
%
% To allow independent conditional loading of fonts, we
% follow the name convention: \zsym@XXX for all needed
% symbols. Equal symbols in both fonts appear at the end.
%
\@ifpackageloaded{lucidabr}{%
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  % Lucida Bright font setup                                      %
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  %                                                               %
    \PackageInfo{czt}{Loading Lucida Bright font symbols for Z}

    % Encodings from lucidabr.sty
    %
    \DeclareSymbolFont{arrows}{LMR}{hlcm}{m}{n} %arrows     =LMR/hlcm/m/n
    \DeclareSymbolFont{letters}{OML}{hlcm}{m}{n} %letters    =OML/hlcm/m/n ; % mathupright= in lucida@expert mode
    \DeclareSymbolFont{symbols}{OMS}{hlcy}{m}{n} %symbols    =OMS/hlcy/m/n
    %operators=\operator@encoding/\rmdefault/m/n
    %         =OT1-T1-LY1 / ?? / m /n
    %largesymbols=OMX/hlcv/m/n

    % Mathematical alphabet in lucidabr - \mathbb = math. blackboard bold
    \DeclareSymbolFontAlphabet{\mathbb}{arrows}

    % Math symbols declaration within Lucida Bright

    %%%%%%%%%%%%%%%%% A.2.4.1 - Greek alphabet treated as operators %

    % Or should this be largesymbols / mathupright (see lucidabr.sty)?
    \DeclareMathSymbol{\zsym@Delta}{\mathord}{letters}{"01}%
    \DeclareMathSymbol{\zsym@Xi}{\mathord}{letters}{"04}%
    \DeclareMathSymbol{\zsym@theta}{\mathord}{letters}{"12}%
    \DeclareMathSymbol{\zsym@lambda}{\mathord}{letters}{"15}%
    \DeclareMathSymbol{\zsym@mu}{\mathord}{letters}{"16}%

    %%%%%%%%%%%%%%%%% A.2.4.2 - Other letter characters             %
    % Other special letters
    \DeclareMathSymbol{\zsym@arithmos}{\mathord}{arrows}{"41}%
    \DeclareMathSymbol{\zsym@nat}{\mathord}{arrows}{"4E}%
    \DeclareMathSymbol{\zsym@power}{\mathord}{arrows}{"50}%
    \def \zsym@arithmos {\mathbb A}
    \def \zsym@nat      {\mathbb N}
    \def \zsym@power    {\mathbb P}

    % Other Greek letters
    % Or should this be largesymbols / mathupright (see lucidabr.sty)?
    \DeclareMathSymbol{\zsym@alpha}{\mathord}{letters}{"0B}%
    \DeclareMathSymbol{\zsym@beta}{\mathord}{letters}{"0C}%
    \DeclareMathSymbol{\zsym@gamma}{\mathord}{letters}{"0D}%
    \DeclareMathSymbol{\zsym@delta}{\mathord}{letters}{"0E}%
    \DeclareMathSymbol{\zsym@epsilon}{\mathord}{letters}{"0F}%
    \DeclareMathSymbol{\zsym@zeta}{\mathord}{letters}{"10}%
    \DeclareMathSymbol{\zsym@eta}{\mathord}{letters}{"11}%
    \DeclareMathSymbol{\zsym@iota}{\mathord}{letters}{"13}%
    \DeclareMathSymbol{\zsym@kappa}{\mathord}{letters}{"14}%
    \DeclareMathSymbol{\zsym@nu}{\mathord}{letters}{"17}%
    \DeclareMathSymbol{\zsym@xi}{\mathord}{letters}{"18}%
    \DeclareMathSymbol{\zsym@pi}{\mathord}{letters}{"19}%
    \DeclareMathSymbol{\zsym@rho}{\mathord}{letters}{"1A}%
    \DeclareMathSymbol{\zsym@sigma}{\mathord}{letters}{"1B}%
    \DeclareMathSymbol{\zsym@tau}{\mathord}{letters}{"1C}%
    \DeclareMathSymbol{\zsym@upsilon}{\mathord}{letters}{"1D}%
    \DeclareMathSymbol{\zsym@phi}{\mathord}{letters}{"1E}%
    \DeclareMathSymbol{\zsym@chi}{\mathord}{letters}{"1F}%
    \DeclareMathSymbol{\zsym@psi}{\mathord}{letters}{"20}%
    \DeclareMathSymbol{\zsym@omega}{\mathord}{letters}{"21}%
    \DeclareMathSymbol{\zsym@Gamma}{\mathord}{letters}{"00}%
    \DeclareMathSymbol{\zsym@Theta}{\mathord}{letters}{"02}%
    \DeclareMathSymbol{\zsym@Lambda}{\mathord}{letters}{"03}%
    \DeclareMathSymbol{\zsym@Pi}{\mathord}{letters}{"05}%
    \DeclareMathSymbol{\zsym@Sigma}{\mathord}{letters}{"06}%
    \DeclareMathSymbol{\zsym@Upsilon}{\mathord}{letters}{"07}%
    \DeclareMathSymbol{\zsym@Phi}{\mathord}{letters}{"08}%
    \DeclareMathSymbol{\zsym@Psi}{\mathord}{letters}{"09}%
    \DeclareMathSymbol{\zsym@Omega}{\mathord}{letters}{"0A}%

    %%%%%%%%%%%%%%%%% A.2.4.3 - Special characters                  %
    %\def \zsym@langle  no need to redefine?
    %\def \zsym@rangle  no need to redefine?
    \def \zsym@lblot    {{\langle}\mkern -5mu{|}}
    \def \zsym@rblot    {{|}\mkern -5mu{\rangle}}
    \def \zsym@ldata    {\langle\!\langle}
    \def \zsym@rdata    {\rangle\!\rangle}
    \DeclareMathSymbol{\zsym@spot}{\mathrel}{symbols}{"0F}%
    \DeclareMathSymbol{\zsym@in}{\mathrel}{symbols}{"32}%

    %%%%%%%%%%%%%%%%% A.2.4.4 - symbol characters predicate logic   %
    % Generic Z operators
    \DeclareMathSymbol{\zsym@vdash}{\mathord}{symbols}{"60}%
    \DeclareMathSymbol{\zsym@cross}{\mathbin}{symbols}{"02}%

    % Schema operators defined as slightly bigger with \z@Bigbinop
    \DeclareMathSymbol{\zsym@solidus}{\mathbin}{symbols}{"6E}% %{letters}{"D8}%
    \DeclareMathSymbol{\zsym@pipe}{\mathrel}{symbols}{"1D}%
    %\def \zsym@comp       {\raise 0.66ex\hbox{\oalign{\hfil$\scriptscriptstyle%
    %                       \mathrm{o}$\hfil\cr\hfil$\scriptscriptstyle\mathrm{9}$\hfil}}}
    \def \zsym@typecolon  {\raise 0.66ex\hbox{\oalign{\hfil$\scriptscriptstyle%
                           \mathrm{o}$\hfil\cr\hfil$\scriptscriptstyle\mathrm{o}$\hfil}}}%
    \DeclareMathSymbol{\zsym@comp}{\mathbin}{stmry}{"23}%

    % Predicate and propositional Logic operators - \mathrel please.
    % Both oz.sty and zed.sty \implies and \iff were not \mathstrut.
    % Adjust the original quantifiers as prefix ops with \mathstrut.
    %
    %\def \zsym@not {\neg\;}
    \DeclareMathSymbol{\zsym@not}{\mathop}{symbols}{"3A}%
    \DeclareMathSymbol{\zsym@and}{\mathrel}{symbols}{"5E}%
    \DeclareMathSymbol{\zsym@or}{\mathrel}{symbols}{"5F}%
    \DeclareMathSymbol{\zsym@implies}{\mathrel}{symbols}{"29}%
    \DeclareMathSymbol{\zsym@iff}{\mathrel}{symbols}{"2C}%
    \DeclareMathSymbol{\zsym@forall}{\mathrel}{symbols}{"38}%
    \DeclareMathSymbol{\zsym@exists}{\mathrel}{symbols}{"39}%

    %%%%%%%%%%%%%%%%% A.2.4.5 - core words (keywords)               %
    %
    % no need to change

    \DeclareMathSymbol{\zseqcat}{\mathbin}{letters}{"5F}%  why "operators"?
    \DeclareMathSymbol{\zupharpoonright}{\mathbin}{arrows}{"75}%
    \DeclareMathSymbol{\zupharpoonleft}{\mathbin}{arrows}{"76}%
    \DeclareMathSymbol{\zdres}{\mathbin}{letters}{"2F}%
    \DeclareMathSymbol{\zrres}{\mathbin}{letters}{"2E}%
    \DeclareMathSymbol{\zemptyset}{\mathord}{symbols}{"3B}%
    \DeclareMathSymbol{\zinj}{\mathbin}{arrows}{"29}%
    \let \zsym@upharpoonright \zupharpoonright

    % slightly raised concatenation operator given as a \mathcar
    \def \zmark@cat {\raise 0.8ex\hbox{$\mathchar\zseqcat$}}

    %%%%%%%%%%%%%%%%% A.2.5.1 - set toolkit symbols                 %
    \DeclareMathSymbol{\zsym@rel}{\mathbin}{arrows}{"21}%  or {symbols}{"24}
    \DeclareMathSymbol{\zsym@fun}{\mathbin}{symbols}{"21}%
    \def \zsym@notin    {\not\in}
    %\DeclareMathSymbol{\zsym@notin}{\mathbin}{arrows}{"1D}%
    \DeclareMathSymbol{\zsym@neq}{\mathrel}{arrows}{"94}%
    \def \zsym@emptyset {\zemptyset}
    \DeclareMathSymbol{\zsym@subseteq}{\mathrel}{symbols}{"12}%
    \DeclareMathSymbol{\zsym@subset}{\mathrel}{symbols}{"13}%
    \DeclareMathSymbol{\zsym@cup}{\mathbin}{symbols}{"5B}%
    \DeclareMathSymbol{\zsym@cap}{\mathbin}{symbols}{"5C}%
    \DeclareMathSymbol{\zsym@setminus}{\mathbin}{symbols}{"6E}%
    \DeclareMathSymbol{\zsym@symdiff}{\mathbin}{symbols}{"0E}%
    \DeclareMathSymbol{\zsym@bigcup}{\mathop}{symbols}{"5B}%
    \DeclareMathSymbol{\zsym@bigcap}{\mathop}{symbols}{"5C}%
    \def \zsym@finset   {\mathbb F}

    %%%%%%%%%%%%%%%%% A.2.5.2 - relation toolkit symbols            %

    \DeclareMathSymbol{\zsym@mapsto}{\mathbin}{arrows}{"2C}%
    \def \zsym@dom    {dom}
    \def \zsym@ran    {ran}
    \def \zsym@id     {id}
    \DeclareMathSymbol{\zsym@circ}{\mathbin}{arrows}{"0E}%
    \let \zsym@dres   \zdres
    \let \zsym@rres   \zrres
    \def \zsym@ndres  {\zmark@hbar{\zsym@dres}}
    \def \zsym@nrres  {\zmark@hbar{\zsym@rres}}
    \DeclareMathSymbol{\zsym@inv}{\mathord}{symbols}{"18}%
    %\def \zsym@limg   {(\mskip-3.5mu|}
    %\def \zsym@rimg   {|\mskip-5mu)}
    \DeclareMathSymbol{\zsym@limg}{\mathopen}{stmry}{"4C}% \llparenthesis in stmaryrd.sty
    \DeclareMathSymbol{\zsym@rimg}{\mathopen}{stmry}{"4D}% \rrparenthesis

    \DeclareMathSymbol{\zsym@oplus}{\mathbin}{arrows}{"2C}%
    \DeclareMathSymbol{\zsym@plus}{\mathbin}{arrows}{"2C}%
    \DeclareMathSymbol{\zsym@star}{\mathbin}{arrows}{"2C}%

    %%%%%%%%%%%%%%%%% A.2.5.3 - function toolkit symbols            %

    % The same as in for AMS
    \def \zsym@pfun      {\zmark@pvbar{\zsym@fun}}
    \def \zsym@inj       {\zinj}
    \def \zsym@pinj      {\zmark@pvbar{\zsym@inj}}
    \def \zsym@surj      {\zmark@darrow{\zsym@fun}{\zsym@fun}{4}}
    \def \zsym@bij       {\zmark@darrow{\zsym@inj}{\zsym@fun}{5}}
    \def \zsym@psurj     {\zmark@pvbar{\zsym@surj}}
    \def \zsym@ffun      {\zmark@fvbar{\zsym@fun}}
    \def \zsym@finj      {\zmark@fvbar{\zsym@inj}}
    \def \zsym@disjoint  {disjoint}
    \def \zsym@partition {partition}

    %%%%%%%%%%%%%%%%% A.2.5.4 - number toolkit symbols              %

    \def \zsym@num         {\mathbb Z}
    \DeclareMathSymbol{\zsym@negate}{\mathop}{arrows}{"2D}%
    \DeclareMathSymbol{\zsym@leq}{\mathrel}{symbols}{"14}%
    \DeclareMathSymbol{\zsym@geq}{\mathrel}{symbols}{"15}%
    \def \zsym@div         {div}
    \def \zsym@mod         {mod}
    \DeclareMathSymbol{\zsym@miuns}{\mathbin}{symbols}{"00}%
    \DeclareMathSymbol{\zsym@sum}{\mathbin}{symbols}{"82}%
    \DeclareMathSymbol{\zsym@mult}{\mathbin}{symbols}{"03}%
    \DeclareMathSymbol{\zsym@lessthan}{\mathrel}{letters}{"3C}%
    \DeclareMathSymbol{\zsym@greaterthan}{\mathrel}{letters}{"3E}%

    %%%%%%%%%%%%%%%%% A.2.5.5 - sequence toolkit symbols            %

    \def \zsym@upto    {\ldotp\ldotp}
    \DeclareMathSymbol{\zsym@hash}{\mathop}{arrows}{"17}%
    \def \zsym@seq     {seq}
    \def \zsym@iseq    {iseq}
    %\langle
    %\rangle
    \def \zsym@cat     {\zmark@cat}
    \def \zsym@extract {\zupharpoonleft}
    \def \zsym@filter  {\zupharpoonright}
    \def \zsym@prefix  {prefix}
    \def \zsym@suffix  {suffix}
    \def \zsym@infix   {infix}
    \def \zsym@dcat    {{\zsym@cat}/}

    % mathematical delimiters that can be used for box drawings
    % (see LaTeX2e Font Selection guide @ fntguide.pdf).
    \DeclareMathDelimiter{\zboxulcorner}{\mathopen}{arrows}{"5B}{arrows}{"5B}
    \DeclareMathDelimiter{\zboxurcorner}{\mathclose}{arrows}{"71}{arrows}{"5C}
    \DeclareMathDelimiter{\zboxllcorner}{\mathopen}{arrows}{"5D}{arrows}{"5D}
    \DeclareMathDelimiter{\zboxlrcorner}{\mathclose}{arrows}{"5E}{arrows}{"5E}
}{%
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  % AMS font setup                                                %
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  %                                                               %

    \PackageInfo{czt}{Loading AMS font symbols for Z}

    % Load msama10 msamb10 font (AMS font dependencies): AMSa, AMSb
    \DeclareSymbolFont{AMSa}{U}{msa}{m}{n}
    \DeclareSymbolFont{AMSb}{U}{msb}{m}{n}

    % Mathematical alphabet in AMSb - \mathbb = math. blackboard bold
    \DeclareSymbolFontAlphabet{\mathbb}{AMSb}

    %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    % Symbols selected from the AMS font                            %
    %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

    \DeclareMathSymbol{\zseqcat}{\mathbin}{AMSa}{"61}         % \frown
    \DeclareMathSymbol{\zupharpoonright}{\mathbin}{AMSa}{"16} % \upharpoonright
    \DeclareMathSymbol{\zupharpoonleft}{\mathbin}{AMSa}{"18}  % \upharpoonleft
    \DeclareMathSymbol{\zdres}{\mathbin}{AMSa}{"43}           % \lhd
    \DeclareMathSymbol{\zrres}{\mathbin}{AMSa}{"42}           % \rhd
    \DeclareMathSymbol{\zemptyset}{\mathord}{AMSb}{"3F}       % \varnothing; similar to original \emptyset
    \DeclareMathSymbol{\zinj}{\mathrel}{AMSa}{"1A}            % \rightarrowtail

    % Font dependant marker: slightly raised concatenation operator given as a \mathcar
    \def \zmark@cat {\raise 0.8ex\hbox{$\mathchar\zseqcat$}}
    % oz.sty option seems to use \mathchar, which nicely selects
    % and AMS font Unicode character (see LaTeX for \mathcar)

    %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    % Standard Z symbols and mathematical toolkit                   %
    %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    %
    % NOTE: Some of these symbols resemble those coming
    %       from the fonts OML/cmm/n/it or OMS/cmsy/m/n
    %       (similar rendering names aside each symbol)
    %       - see tex/latex/base/fontmath.ltx
    %       The synonyms may be useful if AMS is not present?
    %
    %%%%%%%%%%%%%%%%% A.2.4.1 - Greek alphabet treated as operators %
    \let \zsym@Delta    \Delta
    \let \zsym@Xi       \Xi
    \let \zsym@theta    \theta
    \let \zsym@lambda   \lambda
    \let \zsym@mu       \mu

    %%%%%%%%%%%%%%%%% A.2.4.2 - Other letter characters             %
    % Other special letters
    \def \zsym@arithmos {\mathbb A}
    \def \zsym@nat      {\mathbb N}
    \def \zsym@power    {\mathbb P}

    % Other Greek letters
    \let \zsym@alpha    \alpha
    \let \zsym@beta     \beta
    \let \zsym@gamma    \gamma
    \let \zsym@delta    \delta
    \let \zsym@epsilon  \epsilon
    \let \zsym@zeta     \zeta
    \let \zsym@eta      \eta
    \let \zsym@iota     \iota
    \let \zsym@kappa    \kappa
    \let \zsym@nu       \nu
    \let \zsym@xi       \xi
    \let \zsym@pi       \pi
    \let \zsym@rho      \rho
    \let \zsym@sigma    \sigma
    \let \zsym@tau      \tau
    \let \zsym@upsilon  \upsilon
    \let \zsym@phi      \phi
    \let \zsym@chi      \chi
    \let \zsym@psi      \psi
    \let \zsym@omega    \omega
    \let \zsym@Gamma    \Gamma
    \let \zsym@Theta    \Theta
    \let \zsym@Lambda   \Lambda
    \let \zsym@Pi       \Pi
    \let \zsym@Sigma    \Sigma
    \let \zsym@Upsilon  \Upsilon
    \let \zsym@Phi      \Phi
    \let \zsym@Psi      \Psi
    \let \zsym@Omega    \Omega

    %%%%%%%%%%%%%%%%% A.2.4.3 - Special characters                  %
    %\def \zsym@langle  no need to redefine?
    %\def \zsym@rangle  no need to redefine?
    \def \zsym@lblot    {{\langle}\mkern -3.5mu{|}}
    \def \zsym@rblot    {{|}\mkern -3.5mu{\rangle}}
    \def \zsym@ldata    {\langle\!\langle}
    \def \zsym@rdata    {\rangle\!\rangle}
    \let \zsym@spot     \bullet
    \let \zsym@in       \in

    %%%%%%%%%%%%%%%%% A.2.4.4 - symbol characters predicate logic   %

    % Generic Z operators
    \let \zsym@vdash    \vdash
    \let \zsym@cross    \times

    % Schema operators defined as slightly bigger with \z@Bigbinop
    \let \zsym@solidus        \backslash
    \let \zsym@upharpoonright \zupharpoonright
    \def \zsym@pipe           {\mathord>\!\!\mathord>}

    %   oz.sty has a nicer (without \small) fcn composition symbol.
    %    It is defined as an `o' sitting on the top of a `9'.
    %   zed-csp.sty differentiate the heights whenever in Lucida Bright.
    %   To allow room for greater flexibility, do not surround it with any \zXXXop.
    %\def \zsym@comp       {\raise 0.6ex\hbox{\oalign{\hfil$\scriptscriptstyle%
    %                       \mathrm{o}$\hfil\cr\hfil$\scriptscriptstyle\mathrm{9}$\hfil}}}
    \def \zsym@typecolon  {\raise 0.6ex\hbox{\oalign{\hfil$\scriptscriptstyle%
                           \mathrm{o}$\hfil\cr\hfil$\scriptscriptstyle\mathrm{o}$\hfil}}}%
    \DeclareMathSymbol{\zsym@comp}{\mathbin}{stmry}{"23}%

    % Predicate logic
    \def \zsym@not      {\neg\;}
    \let \zsym@and      \wedge
    \let \zsym@or       \vee
    \let \zsym@implies  \Rightarrow
    \let \zsym@iff      \Leftrightarrow
    \let \zsym@forall   \forall
    \let \zsym@exists   \exists

    %%%%%%%%%%%%%%%%% A.2.5.1 - set toolkit symbols                 %
    \let \zsym@rel      \leftrightarrow
    \let \zsym@fun      \rightarrow
    \def \zsym@notin    {\not\in}
    \let \zsym@neq      \neq
    \def \zsym@emptyset {\zemptyset}
    \let \zsym@subseteq \subseteq
    \let \zsym@subset   \subset
    \let \zsym@cup      \cup
    \let \zsym@cap      \cap
    \let \zsym@setminus \setminus
    \let \zsym@symdiff  \ominus
    \let \zsym@bigcup   \bigcup
    \let \zsym@bigcap   \bigcap
    \def \zsym@finset   {\mathbb F}

    %%%%%%%%%%%%%%%%% A.2.5.2 - relation toolkit symbols            %
    \let \zsym@mapsto \mapsto
    \def \zsym@dom    {dom}
    \def \zsym@ran    {ran}
    \def \zsym@id     {id}
    \let \zsym@circ   \circ
    \let \zsym@dres   \zdres
    \let \zsym@rres   \zrres
    \def \zsym@ndres  {\zmark@hbar{\zsym@dres}}
    \def \zsym@nrres  {\zmark@hbar{\zsym@rres}}
    \let \zsym@inv    \sim
    %\def \zsym@limg   {(\mskip-3.5mu|}
    %\def \zsym@rimg   {|\mskip-5mu)}
    \DeclareMathSymbol{\zsym@limg}{\mathopen}{stmry}{"4C}% \llparenthesis in stmaryrd.sty
    \DeclareMathSymbol{\zsym@rimg}{\mathopen}{stmry}{"4D}% \rrparenthesis

    \let \zsym@oplus  \oplus
    \let \zsym@plus   +
    \let \zsym@star   *

    %%%%%%%%%%%%%%%%% A.2.5.3 - function toolkit symbols            %
    \def \zsym@pfun      {\zmark@pvbar{\zsym@fun}}
    \let \zsym@inj       \zinj
    \def \zsym@pinj      {\zmark@pvbar{\zsym@inj}}
    \def \zsym@surj      {\zmark@darrow{\zsym@fun}{\zsym@fun}{4}} % lucida has 3 here
    \def \zsym@bij       {\zmark@darrow{\zsym@inj}{\zsym@fun}{5}} % lucida has 4 here
    \def \zsym@psurj     {\zmark@pvbar{\zsym@surj}}
    \def \zsym@ffun      {\zmark@fvbar{\zsym@fun}}
    \def \zsym@finj      {\zmark@fvbar{\zsym@inj}}
    \def \zsym@disjoint  {disjoint}
    \def \zsym@partition {partition}

    %%%%%%%%%%%%%%%%% A.2.5.4 - number toolkit symbols              %
    \def \zsym@num         {\mathbb Z}
    \def \zsym@negate      {\mathrm{-}}
    \let \zsym@leq         \leq
    \let \zsym@geq         \geq
    \def \zsym@div         {div}
    \def \zsym@mod         {mod}
%    \def \zsym@miuns       {-}
%    \def \zsym@sum         {+}
%    \def \zsym@mult        {*}
%    \def \zsym@lessthan    {<}
%    \def \zsym@greaterthan {>}

    %%%%%%%%%%%%%%%%% A.2.5.5 - sequence toolkit symbols            %
    \def \zsym@upto    {\ldotp\ldotp}
    \let \zsym@hash    \#
    \def \zsym@seq     {seq}
    \def \zsym@iseq    {iseq}
    %\langle
    %\rangle
    \def \zsym@cat     {\zmark@cat}
    \let \zsym@extract \zupharpoonleft
    \let \zsym@filter  \zupharpoonright
    \def \zsym@prefix  {prefix}
    \def \zsym@suffix  {suffix}
    \def \zsym@infix   {infix}
    \def \zsym@dcat    {{\zsym@cat}/}

    % mathematical delimiters that can be used for box drawings
    % (see LaTeX2e Font Selection guide @ fntguide.pdf).
    \DeclareMathDelimiter{\zboxulcorner}{\mathopen}{AMSa}{"70}{AMSa}{"70}
    \DeclareMathDelimiter{\zboxurcorner}{\mathclose}{AMSa}{"71}{AMSa}{"71}
    \DeclareMathDelimiter{\zboxllcorner}{\mathopen}{AMSa}{"78}{AMSa}{"78}
    \DeclareMathDelimiter{\zboxlrcorner}{\mathclose}{AMSa}{"79}{AMSa}{"79}
}
% sets the math version
\mathversion{czt}%
\PackageInfo{czt}{Current math version set to `czt'}

% changes the rendering of A-Z and a-z in specialised italics when in math mode.
%
% Quite elaborated loop that changes the rendering
% (\mathcode) of #1 to that of #3 until 1# >= #2.
%
% setmcodes(#1 % original mathcode
%           #2 % upto threshold
%           #3 % mathcode to substitute)
% begin
%   var c0, c1 : Register;
%   c0 = &#1; c1 = &#3                % fetch value of #1/#3 in c0/c1
%   change_mcode(c0, c1);             % make math code for c0 the value of c1
%   while (c0 < &#2) do               % while c0 has not reached value of #2
%   begin
%     c0++; c1++;                     % increment the values of source/target
%     changeg_mcode(c0, c1);          % make math code for c0 the value of c1
%   end
%                                     % all chars from #1..#2 changed to #3
%                                     % incremented one by one.
% end
%
% called as: setmcodes{ }{ }{italics} % makes A-Z and a-z italic in math mode
%
% fuzz.sty has same code but calls with: \@setmcodes{`A}{`Z}{"7441}
% blend from: zed-csp.sty, soz.sty, oz.sty, fuzz.sty
%
% OBS: This is used in all Z styles. It seems to be originally from struktxf.sty
%
\def\@setmcodes#1#2#3{%
    {\count0=#1 \count1=#3%
    \loop \global\mathcode\count0=\count1%
    \ifnum \count0<#2%
    \advance\count0 by1 \advance\count1 by1%
    \repeat}}
\def\z@mathit%
{%
    \@setmcodes{`A}{`Z}{"7\hexnumber@\symitalics41}%
    \@setmcodes{`a}{`z}{"7\hexnumber@\symitalics61}%
}
\def\z@mathrm%
{%
    \@setmcodes{`A}{`Z}{"7141}
    \@setmcodes{`a}{`z}{"7161}
}

% Depending on package options, load the right encoding.
% Or else, raise a warning and use math italics as default.
\if@mathrm@
  \PackageInfo{czt}{Setting math code for letters as Roman}
  \z@mathrm
\else
  \if@mathit@
    \PackageInfo{czt}{Setting math code for letters as Italics}
    \z@mathit
  \else
    \PackageWarning{czt}{%
      Could not resolve math code for letters.\MessageBreak%
      Default could not be found. Using Italics}
    \z@mathit
  \fi
\fi

%                                                               %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Z definition counters                                         %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                                                               %

% Flag used to switch command counting on/off, default=on
\newif\ifCountDefs

\CountDefstrue
\PackageInfo{czt}{Counting Z declarations? \ifCountDefs YES \else NO \fi}

% Low-level TeX register used to define what to count; started from 1 (instead of 0) because thought of cause of bug; but it wasn't so go bakc to 0; now with debug info too.
% 1 = unboxed para  (e.g. \begin{zed})
% 2 = axdef		(e.g. \begin{axdef})
% 3 = gendef	(e.g. \begin{gendef})
% 4 = schemas	(e.g. \begin{schema})
% 5 = gen schemas  (e.g. \begin{schema})
% 6 = theorems   (e.g. \begin{theorem})
% 7 = proofs (e.g. \begin{zproof})
% 99= nothing  
\newcount\@zcountingwhat
\@zcountingwhat=99

% Few counters used to calculate number of definitions used.
% Reset is controlled by flag/option, default is "cntglobally".
% Stared versions of environments, which are not parsed, are not counted.
% We do not care about parsing rules here (i.e., incorrect specs
% are going to be counted incorrectly).
%
% We have local and global counters. Global counters accumulate decls
% from the whole documents.
%
% Z paragraphs         | Keywords used for counting
%  unboxed items       |  \begin{zed}, \begin{theorem}
%  axiomatic def.      |  \begin{axdef}
%  gen. axdef          |  \begin{gendef}
%  schemas             |  \begin{schema}{NAME}
%  gen. schemas        |  \begin{schema}[X]{NAME}
%
% Counters:
%  a) number of unboxed items: given set, freetype, abbreviation, conjectures, op. templates.
%  b) number of axiomatic definitions
%  c) number of generic axiomatic definitions
%  d) number of schemas
%  e) number of generic schemas
%  f) number of theorems
% g) number of proofs
%  h) total number of Z declarations
\newcounter{cntZunboxed}      %a) local
\newcounter{cntZaxdef}        %b) local
\newcounter{cntZgendef}       %c) local
\newcounter{cntZschema}       %d) local
\newcounter{cntZgenschema}    %e) local
\newcounter{cntZtheorem}    %f) local
\newcounter{cntZproof}    %g) local
\newcounter{cntZdecl}         %h) local
\newcounter{cntZunknown}  % bug? / double-check

\newcounter{cntZtotunboxed}   %a) global
\newcounter{cntZtotaxdef}     %b) global
\newcounter{cntZtotgendef}    %c) global
\newcounter{cntZtotschema}    %d) global
\newcounter{cntZtotgenschema} %e) global
\newcounter{cntZtottheorem}    %f) global
\newcounter{cntZtotproof}    %g) global
\newcounter{cntZtotdecl}      %h) global
\newcounter{cntZtotunknown}  % bug? / double-check

% update the reseting rationale based on package options.
% maybe put this code at the \DeclareOption part (?)
\if@cntbychapter@
  \@addtoreset{cntZunboxed}{chapter}
  \@addtoreset{cntZaxdef}{chapter}
  \@addtoreset{cntZgendef}{chapter}
  \@addtoreset{cntZschema}{chapter}
  \@addtoreset{cntZgenschema}{chapter}
  \@addtoreset{cntZtheorem}{chapter}
  \@addtoreset{cntZproof}{chapter}
  \@addtoreset{cntZdecl}{chapter}
  \@addtoreset{cntZunknown}{chapter}

  \renewcommand{\thecntZunboxed}{\arabic{cntZunboxed} unboxed \ifnum \arabic{cntZaxdef} = 1 item \else items \fi in Chapter~\thechapter}
  \renewcommand{\thecntZaxdef}{\arabic{cntZaxdef} axiomatic \ifnum \arabic{cntZaxdef} = 1 definition \else definitions \fi in Chapter~\thechapter}
  \renewcommand{\thecntZgendef}{\arabic{cntZgendef} generic axiomatic \ifnum \arabic{cntZaxdef} = 1 definition \else definitions \fi in Chapter~\thechapter}
  \renewcommand{\thecntZschema}{\arabic{cntZschema} \ifnum \arabic{cntZaxdef} = 1 schema \else schemas \fi in Chapter~\thechapter}
  \renewcommand{\thecntZgenschema}{\arabic{cntZgenschema} generic \ifnum \arabic{cntZaxdef} = 1 schema \else schemas \fi in Chapter~\thechapter}
  \renewcommand{\thecntZtheorem}{\arabic{cntZtheorem} theorems  in Chapter~\thechapter}
  \renewcommand{\thecntZtheorem}{\arabic{cntZproof} proofs  in Chapter~\thechapter}
  \renewcommand{\thecntZdecl}{\arabic{cntZdecl} in Chapter~\thechapter}
\else
  \if@cntbysection@
    \@addtoreset{cntZunboxed}{section}
    \@addtoreset{cntZaxdef}{section}
    \@addtoreset{cntZgendef}{section}
    \@addtoreset{cntZschema}{section}
    \@addtoreset{cntZgenschema}{section}
    \@addtoreset{cntZtheorem}{section}
    \@addtoreset{cntZproof}{section}
    \@addtoreset{cntZdecl}{section}
	  \@addtoreset{cntZunknown}{section}

    \renewcommand{\thecntZunboxed}{\arabic{cntZunboxed} unboxed \ifnum \arabic{cntZaxdef} = 1 item \else items \fi in Section~\thesection}
    \renewcommand{\thecntZaxdef}{\arabic{cntZaxdef} axiomatic \ifnum \arabic{cntZaxdef} = 1 definition \else definitions \fi in Section~\thesection}
    \renewcommand{\thecntZgendef}{\arabic{cntZgendef} generic axiomatic \ifnum \arabic{cntZaxdef} = 1 definition \else definitions \fi in Section~\thesection}
    \renewcommand{\thecntZschema}{\arabic{cntZschema} \ifnum \arabic{cntZaxdef} = 1 schema \else schemas \fi in Section~\thesection}
    \renewcommand{\thecntZgenschema}{\arabic{cntZgenschema} generic \ifnum \arabic{cntZaxdef} = 1 schema \else schemas \fi in Section~\thesection}
  \renewcommand{\thecntZtheorem}{\arabic{cntZtheorem} theorems  in Section~\thesection}
  \renewcommand{\thecntZtheorem}{\arabic{cntZproof} proofs in Section~\thesection}
    \renewcommand{\thecntZdecl}{\arabic{cntZdecl} in Section~\thesection}
  \fi
  %\else \if@cntglobally@ \relax \fi
\fi

\def\zcountingwhat{%
       \ifnum \@zcountingwhat = 1
           unboxed
       \else
          \ifnum \@zcountingwhat = 2
             axdef
          \else
             \ifnum \@zcountingwhat = 3
                gendef
             \else
                \ifnum \@zcountingwhat = 4
                  schema
                \else
                   \ifnum \@zcountingwhat = 5
                      genschema
                   \else
                     \ifnum \@zcountingwhat = 6
                        theorem
                      \else
                     \ifnum \@zcountingwhat = 7
                        proof
                      \else
                      	\ifnum \@zcountingwhat = 99
							nothing
					\else
                       %don't count at all but debug?
                          unknown?
                       \fi
                     \fi
                   \fi
                \fi
             \fi
          \fi
       \fi
       \fi
}
% counts the appropriate Z paragraph with correct
% dependant counter reseting according to the rule
% chosen by the package option given.
\def\@countZGlobal{\stepcounter{cntZdecl}\stepcounter{cntZtotdecl}}
\def\@countZPara{%
   \ifCountDefs
		\PackageWarning{czt}{Counting  \zcountingwhat}
       \ifnum \@zcountingwhat = 1
          %unboxed para code...
          \stepcounter{cntZunboxed}
          \stepcounter{cntZtotunboxed}
          \@countZGlobal
       \else
          \ifnum \@zcountingwhat = 2
             %axdef code...
             \stepcounter{cntZaxdef}
             \stepcounter{cntZtotaxdef}
             \@countZGlobal
          \else
             \ifnum \@zcountingwhat = 3
                %gendef code...
                \stepcounter{cntZgendef}
                \stepcounter{cntZtotgendef}
                \@countZGlobal
             \else
                \ifnum \@zcountingwhat = 4
                   %schemas code...
                   \stepcounter{cntZschema}
                   \stepcounter{cntZtotschema}
                   \@countZGlobal
                \else
                   \ifnum \@zcountingwhat = 5
                      %gen schemas code...
                      \stepcounter{cntZgenschema}
                      \stepcounter{cntZtotgenschema}
                      \@countZGlobal
                   \else
                     \ifnum \@zcountingwhat = 6
                        %theorem code...
                        \stepcounter{cntZtheorem}
                        \stepcounter{cntZtottheorem}
                        \@countZGlobal
                      \else
                     \ifnum \@zcountingwhat = 7
                        %proof code...
                        \stepcounter{cntZproof}
                        \stepcounter{cntZtotproof}
                        \@countZGlobal
                      \else
                      	\ifnum \@zcountingwhat = 99
							\relax
					\else
                       %don't count at all but debug?
                          \stepcounter{cntZunknown}
                          \stepcounter{cntZtotunknown}
                       \fi
                     \fi
                   \fi
                \fi
             \fi
          \fi
       \fi
       \fi
   \else
      \relax
   \fi
}

% Count hard new lines within Z definitions: not ideal but without complex boolean ifs then this a solution
\def\@countZHNL{%
   \ifCountDefs
       \ifnum \@zcountingwhat = 1
       	  % zed unboxed item
          \@countZPara
       \else
          \ifnum \@zcountingwhat = 2
             %axdef code...
	          \@countZPara
          \else
             \ifnum \@zcountingwhat = 3
                %gendef code...
	              \@countZPara
             \else
                \ifnum \@zcountingwhat = 4
                   %schemas code...
                   \relax
                \else
                   \ifnum \@zcountingwhat = 5
                      %gen schemas code...
			          \@countZPara
                   \else
                     \ifnum \@zcountingwhat = 6
                        %theorem code...
                        \relax
                      \else
                     \ifnum \@zcountingwhat = 7
                        %proof code...
                        \relax
                      \else
                      	\ifnum \@zcountingwhat = 99
							\relax
					\else
                       %don't count at all but debug?
                          \stepcounter{cntZunknown}
                          \stepcounter{cntZtotunknown}
                       \fi
                     \fi
                   \fi
                \fi
             \fi
          \fi
       \fi
       \fi
   \else
      \relax
   \fi
}

\def\ZDeclTblInfoGlobal{%
                    \hline
                    \textbf{Z Declarations}   & \textbf{Total} \\
                    \hline
                    Unboxed items           & \arabic{cntZtotunboxed} \\
                    \hline
                    Axiomatic definitions   & \arabic{cntZtotaxdef} \\
                    \hline
                    Generic axiomatic defs. & \arabic{cntZtotgendef} \\
                    \hline
                    Schemas                 & \arabic{cntZtotschema} \\
                    \hline
                    Generic schemas         & \arabic{cntZtotgenschema} \\
                    \hline
                    Theorems         & \arabic{cntZtottheorem} \\
                    \hline
                    Proofs         & \arabic{cntZtotproof} \\
                    \hline
                    \textbf{Total}          & \textbf{\arabic{cntZtotdecl}} \\
                    \hline
                    \hline
                    \textbf{Unknown?} & \textbf{\arabic{cntZtotunknown}} \\
                    \hline
}
\def \@cntpart {\if@cntbychapter@ Chapter \else \if@cntbysection@ Section \else ??? \fi \fi}
\def\ZDeclTblInfoBy{%
                    \hline
                    \textbf{Z Declarations}   & \textbf{This \@cntpart}       & \textbf{Globally} \\
                    \hline
                    Unboxed items           & \arabic{cntZunboxed}           & \arabic{cntZtotunboxed} \\
                    \hline
                    Axiomatic definitions   & \arabic{cntZaxdef}             & \arabic{cntZtotaxdef} \\
                    \hline
                    Generic axiomatic defs. & \arabic{cntZgendef}            & \arabic{cntZtotgendef} \\
                    \hline
                    Schemas                 & \arabic{cntZschema}            & \arabic{cntZtotschema} \\
                    \hline
                    Generic schemas         & \arabic{cntZgenschema}         & \arabic{cntZtotgenschema} \\
                    \hline
                    Theorems         & \arabic{cntZtheorem}         & \arabic{cntZtottheorem} \\
                    \hline
                    Proofs         & \arabic{cntZproof}         & \arabic{cntZtotproof} \\
                    \hline
                    \textbf{Total}          & \textbf{\arabic{cntZdecl}} & \textbf{\arabic{cntZtotdecl}} \\
                    \hline
                    \hline
                    \textbf{Unknown?} & \textbf{\arabic{cntZunknown}} & \textbf{\arabic{cntZtotunknown}} \\
                    \hline
}

\def \ZDeclSummary {%
   \ifCountDefs
      \begin{table}[ht]
        \begin{center}
            \if@cntglobally@
                \begin{tabular}{|l|r|}
                		\ZDeclTblInfoGlobal
                \end{tabular}
            \else
                \begin{tabular}{|l|c|c|}
					\ZDeclTblInfoBy
                \end{tabular}
            \fi
        \end{center}
        \if@cntglobally@
           \caption{Summary of all Z declarations.}\label{tbl:zdecl:global}
        \else
          \if@cntbychapter@
             \caption{Summary of Z declarations for Chapter~\thechapter.}\label{tbl:zdecl:\thechapter}
          \else
            \if@cntbysection@
               \caption{Summary of Z declarations for Section~\thesection.}\label{tbl:zdecl:\thesection}
            \fi
          \fi
        \fi
      \end{table}
   \else
      \relax
   \fi
}

%                                                               %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Z registers: skip, dimen, tab, etc                            %
% blend: oz.sty, soz.sty, ltcadiz.sty, zed-csp.sty, fuzz.sty    %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                                                               %

%%%%%%%%%% new registers                                        %

% dimen used to:
\newdimen\big@size          % 1) calculate the increase on \z@XXXop modifiers
\newdimen\zedtab            % 2) define the tab stop (\tn) increment
\newdimen\zedindent         % 3) controls how to indent new lines within z para mode
\newdimen\zedleftsep        % 4) determinsed how far within a topline letters should appear(?)
\newdimen\zedbar            % 5) length horizontal bar in z box drawings
%\newdimen\zedlinethickness  % 6) thinkness of z box drawins lines    - oz.sty only? TODO: add behaviour if needed
%\newdimen\zedcornerheight   % 7) height of corners in z box drawings - oz.sty only?

% counter used to:
\newcount\interzedlinepenalty
\newcount\preboxpenalty
\newcount\forcepagepenalty

% skip used to:
\newskip\zedskip            % 1) amount of vertical space inserted by \also

% LaTeX conditional used to:
\newif\ifzt@p               % 1) determines whether LaTeX is in z paragraph mode

%%%%%%%%%% registers initialisation                             %

% initialisation of dimens
\zedtab=2em%
\zedindent=\leftmargini
\zedleftsep=1em
\zedbar=6em                  % oz.sty = 8em
%\zedlinethickness=0.4pt
%\zedcornerheight=0pt

% initialisation of counters
\interzedlinepenalty=10000   %never break
\preboxpenalty=0             %break easily
\forcepagepenalty=-10000     %always break
\interdisplaylinepenalty=100 %break sometimes

% initialisation of skips
\zedskip=0.5\baselineskip%
         plus0.333333\baselineskip%
         minus0.333333\baselineskip%
% \zedskip=\medskipamount from fuzz.sty

% initialisation of if-flags (LaTeX conditionals)
\zt@pfalse

\PackageInfo{czt}{%
    Initialising Z registers with default values.\MessageBreak
    \space\space\space\protect\zedtab=\the\zedtab \MessageBreak%
    \space\space\space\protect\zedindent=\the\zedindent=\protect\leftmargini \MessageBreak%
    \space\space\space\protect\zedleftsep=\the\zedleftsep \MessageBreak%
    \space\space\space\protect\zedbar=\the\zedbar \MessageBreak %
    \MessageBreak
    \space\space\space\protect\interzedlinepenalty=\the\interzedlinepenalty \MessageBreak%never break
    \space\space\space\protect\preboxpenalty=\the\preboxpenalty \MessageBreak%break easily
    \space\space\space\protect\forcepagepenalty=\the\forcepagepenalty\MessageBreak%always break
    \space\space\space\protect\interdisplaylinepenalty=\the\interdisplaylinepenalty \MessageBreak%break sometimes
    \MessageBreak
    \space\space\space\protect\zedskip=\the\zedskip \MessageBreak%
    \space\space\space\protect\zt@p=\ifzt@p true \else false \fi\MessageBreak%
    \space\space\space\protect\CountDefstrue=\ifCountDefs true \else false \fi%
}

%                                                               %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Z spaces, skips, tabs, etc (using the Z registers)            %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                                                               %

% Tab stops from \t1 to \t9 - relative to \zedtab
\let\tie=\t
\def\t#1{\afterassignment\@t\count@=#1}
\def\@t{\hskip\count@\zedtab}

%\def\t#1{\hskip #1\zedtab}

% Small vertical space within z paragraph mode - relative to \zedskip
\def\@also{\crcr \noalign{\penalty\interdisplaylinepenalty\vskip\zedskip}}
\def\also{\@countZHNL\@also}

% varied spacing based in \also - from oz.sty
\def\@Also{\@also\@also}
\def\@ALSO{\@Also\@Also}
\def\Also{\@countZHNL\@Also}
\def\ALSO{\@countZHNL\@Also\@Also}

% forces a page break within z paragraph mode
\def\znewpage{\@also\noalign{\penalty\forcepagepenalty}\@also}

% forces a formula break within z paragraph mode.
% varied relative spacing added before/after it.
\def\zbreak{\@also\noalign{\penalty\interdisplaylinepenalty\vskip-\zedskip}\@also}
\def\zBreak{\@also\noalign{\penalty\interdisplaylinepenalty}\@also}
\def\ZBREAK{\@Also\noalign{\penalty\interdisplaylinepenalty}\@Also}

\PackageInfo{czt}{Setting up Standard Z skipping and breaking}

%                                                               %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Basic definitions for Z box drawings - mostly from zed-csp.sty%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                                                               %

%%%%%%%%%% indent, sizes, skips, padding, new line behaviour    %

% various indentation levels depending on the vertical placement
% to be called whenever within vertical mode (\ifvmode = true)
\def\@zleavevmode{%
  \if@inlabel
    \indent
  \else
    \if@noskipsec
      \indent
    \else
      \if@nobreak
         \global\@nobreakfalse \everypar={}\abovedisplayskip=0pt
      \fi
      {\parskip=0pt\noindent}
    \fi
  \fi}
%\def\@zleavevmode{\if@inlabel \indent
%  \else\if@noskipsec \indent
%  \else\if@nobreak \global\@nobreakfalse
%  \everypar={}\abovedisplayskip=0pt\fi
%  {\parskip=0pt\noindent}\fi\fi}

% nested (dynamic) command definition to change skip sizes.
% it first saves the display skips; changes it; then restores
% the skips back. This is done incrementally.
\def\z@size{}%
\def\@setzsize{%
  \let\next=\@nomath%
  \def\@nomath##1{}%
  \skip0=\abovedisplayskip\skip1=\belowdisplayskip
  \z@size
  \let\@nomath=\next
  \abovedisplayskip=\skip0\belowdisplayskip=\skip1}

% code that affects the size of Z symbols within formulas without
% actually affecting the surrounding text. e.g., \zedsize{\large}
% (see ozguide.pdf, p. 7).
\def\zedsize#1{\def\z@size{#1}}

% changes the behaviour of new line so that appropriate
% skip and side bar is added. if within z paragraph mode \zt@p = false
\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}}}

% a relative bit of \zedskip
\def\@jot{0.5\zedskip}

% fill a line with appropriate width
\def\@zrulefill{\leaders\hrule height\arrayrulewidth\hfill}

% creates a particular skip after new lines? - (old) zed.sty
\def\@zskip#1{\crcr \omit \hbox{\color{ZedBoxColor}\vrule height#1%
    width\arrayrulewidth} \cr}
%\def\@zskip#1{\crcr \omit \vrule height#1 width\arrayrulewidth \cr} zed-csp.sty


% add a tabskip for each new line (?)
\def\@zlign{\tabskip\z@skip\everycr{}}

%%%%%%%%%% individual line drawing                              %

% creates a top line for schema and other boxes with specific width.
% then creates an \hbox relative to \zedleftsep filled with appropriate spacing.
% #1 = possible name or generic parameters to be added
\def\@topline#1{\hbox to\linewidth{%
    \color{ZedBoxColor}%
    \vrule height\arrayrulewidth width\arrayrulewidth
    \vrule height0pt depth\@jot width0pt
    \hbox to\zedleftsep{\@zrulefill\thinspace}%
    {\color{ZedColor}#1}\thinspace\@zrulefill}}

% creates a line of sorts. - used (old) zed.sty
\def\@zedline{\omit\hbox to 0pt{\color{ZedBoxColor}\vrule
    height\arrayrulewidth width\linewidth\hss} \cr}
%\def\@zedline{\omit \vrule height\arrayrulewidth width\linewidth \cr} zed-csp.sty

% creates a narrow line with \zedindent width
\def\@narrow{\advance\linewidth by-\zedindent}

%                                                               %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Z boxes drawings + paragraph markers + box rendering          %
% - mostly from zed-csp.sty (few things from oz.sty)            %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                                                               %

%%%%%%%%%% basic ZEDCHAR definition                             %

% 1) adds appropriate spacing if in vertical mode
% 2) enters "zed" paragraph mode - \zt@p flag = true
% 3) change skip sizes
% 4) thickens line by negative \zedindent (?)
% 5) increased display indent (?)
% 6) fix new lines and tab stopping
\def\@@zed{\ifvmode\@zleavevmode\fi
  $$\global\zt@ptrue
  \@setzsize
  \advance\linewidth by-\zedindent
  \advance\displayindent by\zedindent
  % Count this declaration
  \@countZPara
  % Must have \def and not \let for nested alignments.
  % Also, count extra definitions at each "\\", whenever within
  % a unboxed paragraph. Changed "\also" accordingly.
  \def\\{\crcr \@countZHNL}
  \let\par=\relax
  \tabskip=0pt}

\def\@zed{%
  \@@zed\@znoskip\halign to\linewidth\bgroup
  {\strut$\color{ZedColor}\@zlign##$}\hfil \tabskip=0pt plus1fil\cr}

%%%%%%%%%% \begin{zed}\end{zed} definition                      %

% corresponds to "ZEDCHAR" markup in LaTeX for horizontal para
%
% 1) enters z paragraph mode, which sets \zt@p = true
% 2) changes \cr behaviour to pad next line with spaces, which flips \zt@p = false
% 3) changes the tabskip (\zling) for each tabskip (?)
% 4) restores tabskip after the new line (\cr)     (?)
\def\zed{%
% 1 = unboxed para  (e.g. \begin{zed})
  \@zcountingwhat=1    % sets the kind of counter to addto, 1=unboxed para
  \@zed}

% corresponds to "ENDCHAR" markup in LaTeX
%
% 1) restores paragraph and group balancing (i.e., leaves z mode)
% 2) \@ignoretrue makes sure there are no trailing spaces after \end{zed}
\def\endzed{\crcr\egroup$$\global\@ignoretrue}

% stared version which is ignored by the parser.
% - don't count it, set \@zcountingwhat=99
\@namedef{zed*}{\@zcountingwhat=99 \@zed}
\expandafter\let\csname endzed*\endcsname=\endzed

% change displaymath environment to behave just like \begin{zed}\end{zed}
\def\[{\begingroup \@zcountingwhat=99 \@zed}
\def\]{\crcr\egroup$$\endgroup\ignorespaces}

% corresponds to "ZEDCHAR" markup in LaTeX for section headers

% zsection environment
\let\zsection=\@zed
\let\endzsection=\endzed

% z named conjecture or theorem environment
%
% 1) if theorem is followed by "[" - std z has no ability or label
%\def\theorem#1{\@ifnextchar[{\@theorem{#1}}{\@@theorem{#1}}} % ]
%\def\@theorem#1[#2]{\@@theorem{#1 $[#2]$}}
%
% 2) just puts the theorem in a bold name
\def\@ability{\relax}

\def\theorem#1{\@ifnextchar[{\@theorem{#1}}{\@@theorem{#1}}}
\def\@theorem#1[#2]{\@@theorem{#1 $[#2]$}}
\def\@@theorem#1{%
% 6 = theorems   (e.g. \begin{theorem})
  \@zcountingwhat=6    % sets the kind of counter to addto, 0=unboxed para
  \@@zed\@znoskip\halign to\linewidth\bgroup%
  {\strut$\color{ZedColor}\@zlign\hskip\zedleftsep##$}\hfil \tabskip=0pt plus1fil\crcr
\hskip -\zedleftsep\hbox{\bf theorem \rm \@ability {\color{ZedColor}#1}}\cr}
%\def\@ability{\relax} % don't follow why z-eves needed this command here. = no need.

% synonym for \endzed - could not add colour to the theorem's body :-(
%\def\endtheorem{\color{ZedColor}\endzed}
\let\endtheorem=\endzed

%%%%%%%%%% \begin{axdef}\end{axdef} definition                  %

% TODO: create a general command for entering zed paragraph mode

% corresponds to "AXCHAR" markup in LaTeX
%
% 1) enters z paragraph mode with \@@zed
% 2) changes the behaviour of padding and new lines, just
%    like in \zed but with a side line displayed
% 3) ???
\def\@axdef{%
  \def\also{\@zskip\zedskip}%
  \predisplaypenalty=\preboxpenalty
  \@@zed\@znoskip \halign to\linewidth\bgroup
    \strut{\color{ZedBoxColor}\vrule width\arrayrulewidth} \hskip\zedleftsep
    {$\color{ZedColor}\@zlign##$}\hfil \tabskip=0pt plus1fil\cr}
\def\axdef{%
% 2 = axdef		(e.g. \begin{axdef})
  \@zcountingwhat=2    % sets the kind of counter to addto, 2=axdef para
  \@axdef}

% synonym for \endzed
\let\endaxdef=\endzed

% stared version which is ignored by the parser.
% 99= nothing  
\@namedef{axdef*}{\@zcountingwhat=99 \@axdef}
\expandafter\let\csname endaxdef*\endcsname=\endaxdef

%%%%%%%%%% \begin{schema}{NAME}[X]\end{schema} definition       %

% corresponds to "SCHCHAR" markup in LaTeX
%
% 1) check to see if \begin{schema}?#1 is followed by "["
% 2) if it is, we have a generic schema, in which case
%    \@@nschema{#1[#2]} is called, where #1=name, #2=formals
% 3) otherwise, \@@nschema{#1} is called, where #1=name
% 4) \@@nschema draws a narrow \axdef with the name #1 in the middle

% 4 = schemas	(e.g. \begin{schema})
% 5 = gen schemas  (e.g. \begin{schema})
\def\schema#1{\@ifnextchar[{\@zcountingwhat=5 \@@schema{#1}} {\@zcountingwhat=4 \@@nschema{#1}}}
\def\@schema#1{\@zcountingwhat=99 \@ifnextchar[{\@@schema{#1}}{\@@nschema{#1}}}
\def\@@schema#1[#2]{\@@nschema{#1[#2]}}
\def\@@nschema#1{\@narrow\@axdef \omit\@topline{$\strut#1$}\cr}

% just like \endzed but with a final underline to close
% the schema box, right after restoring the skip mode.
\def\endschema{\@zskip\@jot \@zedline \endzed}

% for schemas without name, use \begin{plainschema}
% it is ignored by the parser
\def\plainschema{\@narrow \@zcountingwhat=99 \@axdef \@zedline \@zskip\@jot}
\let\endplainschema=\endschema

% similarly, one could use the stared version of the
% schema environment, which accepts name and/or generic
% formals, but is ignored by the parser.
\@namedef{schema*}{\@schema} % don't count those
\expandafter\let\csname endschema*\endcsname=\endschema

%%%%%%%%%% \begin{gendef}[X]\end{gendef} definition             %

% corresponds to "AXCHAR GENCHAR" markup in LaTeX
%
% 1) check to see if \begin{gendef}?#1 is followed by "["
% 2) if it is, we have a generic axdef with generic formals,
%    in which case \@@ngendef is called to draw double lines
% 3) otherwise, \@@gendef is called to draw double lines but
%    with the generic formals given
% 4) lines are draw similarly to \axdef but doubled

  % 3 = gendef	(e.g. \begin{gendef})
\def\gendef{\@zcountingwhat=3 \@ifnextchar[{\@@gendef}{\@@ngendef}}
\def\@gendef{\@zcountingwhat=99 \@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
  }


% synonym for \endschema
\let\endgendef=\endschema

% stared version which is ignored by the parser.
\@namedef{gendef*}{\@gendef} % don't count it
\expandafter\let\csname endgendef*\endcsname=\endgendef

%%%%%%%%%% \where separator definition                          %

% draws the |- line separating declarations from predicates (zed.sty)
\def\where{\@zskip\@jot
  \omit\hbox{\color{ZedBoxColor}\vrule height\arrayrulewidth width\zedbar} \cr
  \@zskip\@jot}
%\def\where{\@zskip\@jot            zed-csp.sty
%  \omit \vrule height\arrayrulewidth width\zedbar \cr
%  \@zskip\@jot}

\PackageInfo{czt}{Setting up Standard Z LaTeX environments}

%                                                               %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Basic definitions for Z symbols.                              %
% Mathematical operators classes - Add \mathstrut for boxing    %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                                                               %

% The spacing chosen for the math operators should reflect
% their precedences, as defined using the Markup directives.
% That is, function, generic, and schema operators bind
% tighter than relation and predicate logic operators.
% The former are to be \mathbin, whereas the latter are to
% be \mathrel (thanks to Ian Toyn's clarification on the
% CZT mail thread of 24/09/2008).
%
% SUMMARY: Function, generic, schema op = \mathbin
%          Relation, predicate logic op = \mathrel
%
% Core symbols and keywords have fixed precedences, and we
% wrap them accordingly. Markup directives have their fixture
% hinting which spacing should they have. For the list of
% core symbols precedence see ISOZ Table 31 p.37.
%
% \z@op     = general operator given with \nolimits
% \z@preop  = prefix operator spacing  - Zprechar  / Zpreword
% \z@postop = postfix operator spacing - Zpostchar / Zpostword
% \z@relop  = infix operator  spacing  - Zinchar   / Zinword (\;)
% \z@binop  = infix operator  spacing  - Zinchar   / Zinword (\:)
% \z@ordop  = ordinary char spacing    - Zchar     / Zword
%
% IMPORTANT:
%
% User defined \LaTeX{} commands used as markup directives
% should take these spacing rules into account, hence wrap
% it with the proper \zXXop.
%
% For that, we provide equivalent macro names without @ so
% that users specifying new commands for markup directives
% can add the appropriate spacing rule.
% (see LaTeX Companion 2nd Ed Table 8.7, p.525)
%
% We need the original commands with the \z@ prefix as this is
% used for slightly increasing/decreasing their size.
%
% LATEX DETAILS:
%
% The use of \nolimits is important for mathematical symbols used
% as keywords as it finely control typesetting and raise errors.
% For the user command form of \z@op, one should refer to \keyword
% (see LaTeX Companion 2nd Ed p.492, 903)
%
% The use of \mathstrut is important only when the symbol may
% appear within other symbols (e.g., \sqrt{y} vs. \sqrt{\mathstrut y}).
% For the Z operators, we tried to compromise between consistency
% and simplicity.
%
% That is, some operators were already relation/binary and we avoided
% redefining them just to add the \mathstrut. For these cases where
% we did not add \mathstrut, a note is added.
% TODO: this is experimental check if need to add everywhere.
%
\def\z@op#1{\mathstrut{#1}}
\def\z@preop#1{\mathop{\z@op{#1}}\nolimits}
\def\z@postop#1{\mathop{\z@op{#1}}\nolimits}
\def\z@relop#1{\mathrel{\mathstrut{#1}}}
\def\z@binop#1{\mathbin{\mathstrut{#1}}}
\def\z@ordop#1{\mathord{#1}}
\def\z@openop#1{\mathopen{#1}}
\def\z@closeop#1{\mathclose{#1}}
\let\zpreop=\z@preop
\let\zpostop=\z@postop
\let\zbinop=\z@binop
\let\zrelop=\z@relop
\let\zordop=\z@ordop
\let\zopenop=\z@openop
\let\zcloseop=\z@closeop

% these operators are reused with increased/reduced size.
% for that we provide increasing/reducing macros for them.
% they come from oz.sty
%
% the (weird) algorithm that calculates the increment based on \big@size
\def\bBigg@#1#2{%
\mbox{\ifcase#1\or\large\or\Large\or\LARGE\or\small\or\footnotesize\fi
$#2$}\nulldelimiterspace\z@ \m@th}
\addto@hook\every@math@size{\setbox\z@\vbox{\hbox{$($}\kern\z@}%
  \big@size 1.2\ht\z@}
%
% each relative increment
\def\zBIG{\bBigg@{3}}
\def\zBig{\bBigg@{2}}
\def\zbig{\bBigg@{1}}
\def\zsmall{\bBigg@{4}}
\def\zSmall{\bBigg@{5}}
%
% and their version with varied sizes
\def\z@bigpreop#1{\z@preop{\zbig{#1}}}
\def\z@bigpostop#1{\z@postp{\zbig{#1}}}
\def\z@bigbinop#1{\z@binop{\zbig{#1}}}
\def\z@bigrelop#1{\z@relop{\zbig{#1}}}
%
\def\z@Bigpreop#1{\z@preop{\zBig{#1}}}
\def\z@Bigpostop#1{\z@postp{\zBig{#1}}}
\def\z@Bigbinop#1{\z@binop{\zBig{#1}}}
\def\z@Bigrelop#1{\z@relop{\zBig{#1}}}
%
\def\z@smallpreop#1{\z@preop{\zsmall{#1}}}
\def\z@smallpostop#1{\z@postp{\zsmall{#1}}}
\def\z@smallbinop#1{\z@binop{\zsmall{#1}}}
\def\z@smallrelop#1{\z@relop{\zsmall{#1}}}

\PackageInfo{czt}{Setting up Standard Z basic symbols}

%                                                               %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Z core characters and words (ISOZ A.2.4)                      %
% adjustment to spacing and boxing + added consistently         %
% normalised names to \zsym@XXX to simplify diff. font loading  %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                                                               %

%%%%%%%%%%%%%%%%% A.2.4.1 - Greek alphabet treated as operators %

% Save the original symbols - use before adjusting \mathstrut
\def \Delta      {\zordop{\zsym@Delta}}
\def \Xi         {\zordop{\zsym@Xi}}
\def \theta      {\zpreop{\zsym@theta}}
\def \lambda     {\zpreop{\zsym@lambda}}
\def \mu         {\zpreop{\zsym@mu}}

%%%%%%%%%%%%%%%%% A.2.4.2 - Other letter characters             %

% blackboard bold letters + power set is a primitive prefix operator
\def \arithmos   {\zordop{\zsym@arithmos}}
\def \nat        {\zordop{\zsym@nat}}
\def \power      {\zpreop{\zsym@power}}

% Being Zchar, these Greek letters should be surrounded
% by \zordop. As they are already \mathord, the only
% difference is because of a missing \mathstrut.
% Yet, for when conditionally loading symbols from different
% fonts, it is useful to have meta symbols like all others.
%
\def \alpha    {\zordop{\zsym@alpha}}
\def \beta     {\zordop{\zsym@beta}}
\def \gamma    {\zordop{\zsym@gamma}}
\def \delta    {\zordop{\zsym@delta}}
\def \epsilon  {\zordop{\zsym@epsilon}}
\def \zeta     {\zordop{\zsym@zeta}}
\def \eta      {\zordop{\zsym@eta}}
\def \iota     {\zordop{\zsym@iota}}
\def \kappa    {\zordop{\zsym@kappa}}
\def \nu       {\zordop{\zsym@nu}}
\def \xi       {\zordop{\zsym@xi}}
\def \pi       {\zordop{\zsym@pi}}
\def \rho      {\zordop{\zsym@rho}}
\def \sigma    {\zordop{\zsym@sigma}}
\def \tau      {\zordop{\zsym@tau}}
\def \upsilon  {\zordop{\zsym@upsilon}}
\def \phi      {\zordop{\zsym@phi}}
\def \chi      {\zordop{\zsym@chi}}
\def \psi      {\zordop{\zsym@psi}}
\def \omega    {\zordop{\zsym@omega}}
\def \Gamma    {\zordop{\zsym@Gamma}}
\def \Theta    {\zordop{\zsym@Theta}}
\def \Lambda   {\zordop{\zsym@Lambda}}
\def \Pi       {\zordop{\zsym@Pi}}
\def \Sigma    {\zordop{\zsym@Sigma}}
\def \Upsilon  {\zordop{\zsym@Upsilon}}
\def \Phi      {\zordop{\zsym@Phi}}
\def \Psi      {\zordop{\zsym@Psi}}
\def \Omega    {\zordop{\zsym@Omega}}

\PackageInfo{czt}{Setting up Standard Z Greek and other letters}

%%%%%%%%%%%%%%%%% A.2.4.3 - Special characters                  %

% Underscore redefined - used oz.sty width + zed-csp \ifmmode
%\def\_{\leavevmode \vbox{\hrule width0.4em}}
\def\_{\leavevmode \ifmmode\else\kern0.06em\fi \vbox{\hrule width0.5em}}

% Make free type ampersand spacing nicely
\let\zamp=\&
\def\&{\ifmmode \;\zbinop{\zamp} \else ~\zamp~ \fi}

% Hard space redefined - used zed-csp.sty
% in math mode ~=\, ; outside, it is "\@M\ "
% TODO: find out what \@M means!
\def~{\ifmmode\,\else\penalty\@M\ \fi}

% additional Z brackets: bindings + free type constructors
% they are not \zordop because \langle is \mathopen/close
\def \lblot {\zsym@lblot}
\def \rblot {\zsym@rblot}
\def \ldata {\zsym@ldata}
\def \rdata {\zsym@rdata}
%\langle
%\rangle

% Fat spot: used for separating predicates and expressions
\def \spot {\zrelop{\zsym@spot}}

% Set membership with added \mathstrut
\def\in   {\zrelop{\zsym@in}}

% Treat ``@'' treated as \spot and ``|'' as \mid
% That is, make then space as function operators
%
\mathcode`\|=\mid
\mathchardef\semicolon="603B
\mathcode`\;="8000                           % makes ; active in math mode
{\catcode`\;=\active \gdef;{\semicolon\;}}
\mathcode`\@="8000                           % makes @ active in math mode
{\catcode`\@=\active \gdef@{\spot}}

% zed-csp.sty had this for quotes, needed?
\def\@kwote#1"{\hbox{\mathit{#1}}}
\mathcode`\"="8000                           % makes " active in math mode
{\catcode`\"=\active \global\let"=\@kwote}

\PackageInfo{czt}{Setting up Standard Z bracket symbols}

\PackageInfo{czt}{Marking \protect\mid, \protect\semicolon,
    and \protect\spot \MessageBreak %
    as \MessageBreak active in math mode}

%%%%%%%%%%%%%%%%% A.2.4.4 - symbol characters predicate logic   %
%
% Redefine logical ops as relational rather than binary ops.
% That is because function, schema and generic operators bind
% tighter than relation and predicate logic operators. Thus,
% the former needs to be \mathbin, whereas the latter are \mathrel.

% Generic Z operators
\def \vdash      {\zpreop{\zsym@vdash}}
\def \cross      {\zbinop{\zsym@cross}}

% Schema operators defined as slightly bigger with \z@Bigbinop
\def \hide      {\zrelop{\z@Bigbinop{\zsym@solidus}}}
\def \project   {\zrelop{\z@Bigbinop{\zsym@upharpoonright}}}
\def \semi      {\zrelop{\z@Bigbinop{\zsym@comp}}}
\def \pipe      {\zrelop{\z@bigbinop{\zsym@pipe}}}
\def \typecolon {\zrelop{\z@bigbinop{\zsym@typecolon}}}

% Z schema renaming or predicate substitution as an operator
% rather than a core symbol. \rename is not in the standard,
% (came from oz.sty). The advantage here is that one could
% have better rendering of complex expression because of the
% use of \left[ instead of just `['.
%
% TODO: discuss if it is worth making it a markup directive?
%
%\def\zfor     {/}  % solidus char
%\def\z@rename*[#1/#2]{\left[#1 \over #2\right]}
%\def\z@@rename[#1/#2]{\left[#1 \zfor #2\right]}
%\def\rename{\@ifnextchar*{\z@rename}{\z@@rename}}

% Predicate and propositional Logic operators - \mathrel please.
%
\def \lnot     {\zordop{\zsym@not}}
\def \land     {\zrelop{\zsym@and}}
\def \lor      {\zrelop{\zsym@or}}
\def \implies  {\zrelop{\zsym@implies}}
\def \iff      {\zrelop{\zsym@iff}}
\def \forall   {\zpreop{\zsym@forall}}
\def \exists   {\zpreop{\zsym@exists}}

\PackageInfo{czt}{Setting up Standard Z predicate logic symbols}

%%%%%%%%%%%%%%%%% A.2.4.5 - core words (keywords)               %
%
% A \z@word     is a function-like operator (see \z@op) with \nolimits.
% A \z@boldword is a boldface \z@word.
% A \zword      is a roman string (within a \mbox) \z@word.
% A \zkeyword   is a boldface roman string (within a \mbox) \z@word.
%
% \zword    is for defining toolkit symbols, as in \dom, \seq, etc.
% \zkeyword is for language keywords. For Z they are the Z Std keywords.
% \ztoolkit is either \zword or \zkeyword depending on the \@tkkeyword@ option
%
% Toolkit builders are encouraged to use \ztoolkit for their markup directives.
% Language extension style files should use \zkeyword for new keywords.
% For infix or prefix keywords, just insert the appropriate \zXXXop
%
\def\z@word#1{\z@op{#1}}
\def\z@boldword#1{\z@word{\textbf{#1}}}

% To avoid mixed fonts in default theorem-like environments,
% remove \mbox and use \mathrm alone, Leo, 17/06/2010.
%\def\zword#1{\z@word{\mbox{\textrm{#1}}}}
%\def\zkeyword#1{\z@word{\mbox{\textrm{\textbf{#1}}}}}
\def\zword#1{\z@word{\mathrm{#1}}}
\def\zkeyword#1{\z@word{\mathrm{\mathbf{#1}}}}
\def\ztoolkit#1{\if@tkkeyword@ \zkeyword{#1} \else \zword{#1} \fi}

% Z keywords - scattered in the ZStd. They are collected
% in full at "net.sourceforge.czt.parser.z.ZKeyword.java"
%
% sections
\def \SECTION	{\zpreop{\zkeyword{section}}}
\def \parents	{\zpreop{\zkeyword{parents}}}
%
% if-then-else
\def \IF	    {\zpreop{\zkeyword{if}}}
\def \THEN	    {\zbinop{\zkeyword{then}}}
\def \ELSE	    {\zbinop{\zkeyword{else}}}
%
% let
\def \LET	    {\zpreop{\zkeyword{let}}}
%
% boolean values - used in ZStd in the Z logic only
% can be used by users that want to define \bool as
% the free type "\bool ::= \false | \true".
\def \true	    {\zordop{\zkeyword{true}}}
\def \false	    {\zordop{\zkeyword{false}}}
%
% operator template keywords
\def \function	{\zpreop{\zkeyword{function}}}
\def \relation	{\zpreop{\zkeyword{relation}}}
\def \generic	{\zpreop{\zkeyword{generic}}}
\def \leftassoc	{\zbinop{\zkeyword{leftassoc}}}
\def \rightassoc{\zbinop{\zkeyword{rightassoc}}}
%
% schema precondition
\def \pre       {\zpreop{\zkeyword{pre}}}
%
% being a Zinword expression, \listarg is \zbinop
% \varg is a synonym for \_ in operator templates
\def \listarg	{\zbinop{\zkeyword{,,}}}
\def \varg      {\zbinop{\zkeyword{\_}}}

\PackageInfo{czt}{Setting up Standard Z keywords}

%                                                               %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Z mathematical toolkit characters and words (ISOZ A.2.5)      %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                                                               %

\PackageInfo{czt}{\space\space Loading prelude\space\space\space\space\space\space\space\space\space\space symbols}

% NOTE: adjustment to spacing (\mathrel/bin) and boxing (\mathstrut)
%
% Spacing of operator templates and toolkit characters:
%
% \zbinop = Function (F) or Generic (G)
% \zrelop = Relation (R)
%
% \zordop = Zchar or Zword (D)       (unless these are used)
% \zpreop = Zprechar or Zpreword (O) (for operator templates)
%
% TODO: Discuss... [wait to see how it renders]
% Shall I really rename all these already relational
% operators just to add \mathstrut to then?

%%%%%%%%%%%%%%%%% A.2.5.1 - set toolkit symbols                 %
\def \rel      {\zbinop{\zsym@rel}}       % G
\def \fun      {\zbinop{\zsym@fun}}       % G
\def \notin    {\zbinop{\zsym@notin}}     % R
\def \neq      {\zrelop{\zsym@neq}}       % R
\def \emptyset {\zordop{\zsym@emptyset}}  % D
\def \subseteq {\zrelop{\zsym@subseteq}}  % R
\def \subset   {\zrelop{\zsym@subset}}    % R
\def \cup      {\zbinop{\zsym@cup}}       % F
\def \cap      {\zbinop{\zsym@cap}}       % F
\def \setminus {\zbinop{\zsym@setminus}}  % F
\def \symdiff  {\zbinop{\zsym@symdiff}}   % F
\def \bigcup   {\zpreop{\zsym@bigcup}}    % O
\def \bigcap   {\zpreop{\zsym@bigcap}}    % O
\def \finset   {\zpreop{\zsym@finset}}    % O

\PackageInfo{czt}{\space\space Loading set\space\space\space\space\space\space toolkit symbols}

%%%%%%%%%%%%%%%%% A.2.5.2 - relation toolkit symbols            %

% superscript maths is aligned/spaced differently
% hence no change (see LaTeX Companion 8.7.5 p.505)
%
% NOTE: ISOZ A.2.5.2 does not add wordglue to \inv! TODO: check std bug?

\def \mapsto {\zbinop{\zsym@mapsto}}         % F
\def \dom    {\zpreop{\ztoolkit{\zsym@dom}}} % O
\def \ran    {\zpreop{\ztoolkit{\zsym@ran}}} % O
\def \id     {\zpreop{\ztoolkit{\zsym@id}}}  % G
\def \comp   {\zbinop{\zsym@comp}}           % F
\def \circ   {\zbinop{\zsym@circ}}           % F
\def \dres   {\zbinop{\zsym@dres}}           % F
\def \rres   {\zbinop{\zsym@rres}}           % F
\def \ndres  {\zbinop{\zsym@ndres}}          % F
\def \nrres  {\zbinop{\zsym@nrres}}          % F
\def \inv    {\zpostop{^\zsym@inv}}          % F - ZStd alternative should be {^\zsym@inv}
\def \limg   {\zbinop{\zsym@limg}}           % F
\def \rimg   {\zpostop{\zsym@rimg}}          % F - it's a Zposchar!
\def \oplus  {\zbinop{\zsym@oplus}}          % F
\def \plus   {\zpostop{^\zsym@plus}}         % F - superscripts spaces differently
\def \star	 {\zpostop{^\zsym@star}}         % F

\PackageInfo{czt}{\space\space Loading relation toolkit symbols}

%%%%%%%%%%%%%%%%% A.2.5.3 - function toolkit symbols            %

\def \pfun      {\zbinop{\zsym@pfun}}                 % G
\def \inj       {\zbinop{\zsym@inj}}                  % G
\def \pinj      {\zbinop{\zsym@pinj}}                 % G
\def \surj      {\zbinop{\zsym@surj}}                 % G
\def \bij       {\zbinop{\zsym@bij}}                  % G
\def \psurj     {\zbinop{\zsym@surj}}                 % G
\def \ffun      {\zbinop{\zsym@ffun}}                 % G
\def \finj      {\zbinop{\zsym@finj}}                 % G
\def \disjoint  {\zpreop{\ztoolkit{\zsym@disjoint}}}  % G
\def \partition {\zbinop{\ztoolkit{\zsym@partition}}} % G

\PackageInfo{czt}{\space\space Loading function toolkit symbols}

%%%%%%%%%%%%%%%%% A.2.5.4 - number toolkit symbols              %

\def\num    {\zordop{\zsym@num}}            % D
\def\negate {\zpreop{\zsym@negate}}         % F
\def\leq    {\zrelop{\zsym@leq}}            % R
\def\geq    {\zrelop{\zsym@geq}}            % R
\def\div    {\zbinop{\ztoolkit{\zsym@div}}} % F
\def\mod    {\zbinop{\ztoolkit{\zsym@mod}}} % F
%\def-{\zbinop{\zsym@miuns}}                 % F
%\def+{\zbinop{\zsym@sum}}                   % F
%\def*{\zbinop{\zsym@mult}}                  % F
%\def<{\zrelop{\zsym@lessthan}}              % R
%\def>{\zrelop{\zsym@greaterthan}}           % R

\PackageInfo{czt}{\space\space Loading number\space\space\space toolkit symbols}

%%%%%%%%%%%%%%%%% A.2.5.5 - sequence toolkit symbols            %

% NOTE: As with \{ and \}, I am not redefining \langle and \rangle
%       Also, \# is not being given as a \zpreop - # is low level
%       and I don't know how to "influence" its spacing in \#
%
% MINOR: R~^{~n~} : hard spaces are mandatory for parsing
%
% Relational iteration, as in R~^{~n~}, have superscripts and
% a prefix operator. R alone will be treated as \mathord (rather
% than \mathop), and I do not know how to accommodate that :-(

\def \upto    {\zbinop{\zsym@upto}}                  % F
\def \seq     {\zpreop{\ztoolkit{seq}}}              % G
\def \iseq    {\zpreop{\ztoolkit{iseq}}}             % G
\def \cat     {\zbinop{\zsym@cat}}                   % F
\def \extract {\zbinop{\zsym@extract}}               % F
\def \filter  {\zbinop{\zsym@filter}}                % F
\def \prefix  {\zbinop{\ztoolkit{\zsym@prefix}}}     % R
\def \suffix  {\zbinop{\ztoolkit{\zsym@suffix}}}     % R
\def \infix   {\zbinop{\ztoolkit{\zsym@infix}}}      % R
\def \dcat    {\zpreop{\zsym@dcat}}                  % D
%\langle                                             % F
%\rangle                                             % F
\def\#{\zpreop{\zsym@hash}}                          % F

\PackageInfo{czt}{\space\space Loading sequence toolkit symbols}

%%%%%%%%%%%%%%%%% B.9 - standard toolkit                        %

\PackageInfo{czt}{\space\space Loading standard toolkit symbols completed}

%%%%%%%%%%%%%%%%% refinement toolkit                        %

\def\zastate {\zkeyword{Z\_Abs\_St}}
\def\zcstate {\zkeyword{Z\_Con\_St}}
\def\zastinit {\zkeyword{Z\_Abs\_Init}}
\def\zcstinit {\zkeyword{Z\_Con\_Init}}
\def\zretrieve {\zkeyword{Z\_Retr}}
\def\zfsrefines {\zpreop{\zkeyword{Z\_FS\_Refines}}}

\PackageInfo{czt}{\space\space Loading Z state refinement toolkit symbols completed}

%                                                               %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Few extra helpful commands                                    %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                                                               %

% users referring to this file in their \LaTeX
\def\cztstylefile {\texttt{czt.sty}}

% macro for block alignment of paragraphs - from (old) zed.sty
\def\zedblock{\@ifnextchar[{\@zedblock}{\@zedblock[t]}}
\def\@zedblock[#1]{\array[#1]{@{}l@{}}}
\let\endzedblock=\endarray

%                                                               %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newif\ifshowLabels
\showLabelstrue

\def\Label#1{\ifshowLabels \mbox{$\ldata$\,#1\,$\rdata$} \\ \fi}

\newif\ifshowzproofs
\showzproofstrue
%%
%% the showzproofsfalse code is mostly copied from Latex's verbatim
%% the \let\0... stuff is needed to put the ignore macro after the \fi
%% -- otherwise the \fi gets ignored!
%%
\def\zproof{\ifshowzproofs% 
% 7 = proofs (e.g. \begin{zproof})
 \@zcountingwhat=7% sets the kind of counter to addto, 0=unboxed para
 \@@zed\@znoskip\let\par=\cr\obeylines\@vobeyspaces\halign to\linewidth\bgroup
\strut$\@zlign##$\hfil \tabskip=0pt plus1fil\crcr
\hskip -\zedleftsep\hbox{\bf proof} \let\0\relax
\else \let\do\@makeother \dospecials \let\0\ignore@zproof \fi \0}
\def\endzproof{\ifshowzproofs\crcr\vrule width.6em height.6em depth.1em\crcr\egroup$$\global\@ignoretrue\par\fi}

\begingroup \catcode `|=0 \catcode `[= 1
\catcode`]=2 \catcode `\{=12 \catcode `\}=12
\catcode`\\=12 |long|gdef|ignore@zproof#1\end{zproof}[|end[zproof]]
|endgroup

%\def\[{\begingroup\zed}
%\def\]{\crcr\egroup$$\endgroup\ignorespaces}

\def\proof{\crcr \hskip -\zedleftsep\mbox{\bf proof} \crcr }

\let\latexbegin\begin
\def\begin{\long\def\@ability{\relax}\@ifnextchar[{\x@begin}{\latexbegin}} % ]
\def\x@begin[#1]{\long\def\@ability{#1\ }\latexbegin}


\def \defs {\mathrel{\widehat=}}
\def \bind      {\mathrel{\leadsto}}
\def \bindsto   {\mathrel{\leadsto}}
\let\lbind=\lblot
\let\rbind=\rblot


\endinput
%%
%% End of file `czt.sty'.