Laboratoire de l'Informatique et du Parallélisme » Linear Arithmetic

\section{Further results}

\subsection{Equational theories}

\todo{Mention PVBC}

\subsection{Modal and second order theories}

\todo{Mention links with ramification/sortedness}

\section{Soundness}

\label{sect:soundness}

In this section we show that the representable functions of our theories $\arith^i$ are in $\fphi i$ (`soundness').

The main result is the following:

\begin{theorem}

	\label{thm:soundness}

	If $\arith^i$ proves $\forall \vec u^\normal . \forall \vec x^\safe . \exists y^\safe . A(\vec u ; \vec x , y)$ then there is a $\mubci{i-1}$ program $f(\vec u ; \vec x)$ such that $\Nat \models A(\vec u ; \vec x , f(\vec u ; \vec x))$.

\end{theorem}

The problem for soundness is that we have predicates, for example equality, that take safe arguments in our theory but do not formally satisfy the polychecking lemma for $\mubc$ functions, Lemma~\ref{lem:polychecking}. 

For this we will use \emph{length-bounded} witnessing argument, borrowing a similar idea from Bellantoni's work \cite{Bellantoni95}.

\begin{definition}

[Length bounded (in)equality]

%We define \emph{length-bounded equality}, $\eq(l;x,y)$ as the characteristic function of the predicate:

%\[

%x \mode l = y \mode l

%\]

%which is definable by safe recursion on $l$:

%\[

%\begin{array}{rcl}

%\eq (0 ; x,y) & \dfn & \equivfn (;\bit (0;x),\bit(0;y) ) \\

%\eq (\succ i l; x,y) & \dfn & \cond (; \eq ( u;x,y ) , 0, \equivfn (; \bit (\succ i u ; x ) , \bit (\succ i l ; y ))  )

%\end{array}

%\]

We define \emph{length-bounded inequality} as:

\[

\begin{array}{rcl}

\leqfn (0 ; x ,y) & \dfn & \cond(; \bit (0;x), 1, \bit (0;y) ) \\

\leqfn (\succ i l ; x,y) & \dfn & \orfn ( ; \cond(;\bit (\succ i l ; x) , \bit(\succ i l ; y),0 ) , \andfn (; \equivfn (\bit (\succ i l ; x) , \bit(\succ i l ; y)) , \leqfn (l;x,y ) ) )

\end{array}

\]

\end{definition}

Notice that $\leqfn (l; x,y) = 1$ just if $x \mode l \leq y \mode l$.

We can also define $\eq( l; x,y)$ as $\andfn (;\leq(l;x,y),\leq(l;y,x))$.

%\anupam{Do we need the general form of length-boundedness? E.g. the $*$ functions from Bellantoni's paper? Put above if necessary. Otherwise just add sequence manipulation functions as necessary.}

%

%Notice that $\eq$ is a polymax bounded polyomial checking function on its normal input, and so can be added to $\mubc$ without problems.

In the presence of a compatible sorting, we may easily define functions that \emph{evaluate} safe formulae in $\mubc$:

\begin{proposition}

Given a $\Sigma^\safe_i$ formula $A$ and compatible sorting $(\vec u; \vec x)$ of its variables, there is a $\mubci{i}$ program $\charfn{\vec u ;\vec x}{A} (l, \vec u ; \vec x)$ computing the characteristic function of $A (\vec u \mode l ; \vec x \mode l)$.

\end{proposition}

We will use the programs $\charfn{}{}$ in the witness functions we define below.

Let us write $\charfn{}{i}$ to denote the class of functions $\charfn{}{A}$ for $A \in \Sigma^\safe_{i}$.

For the notion of bounding polynomial below we are a little informal with bounds, using `big-oh' notation, since it will suffice just to be `sufficiently large'.

Notice that, while we refer to $b_A(l), p(l)$ etc.\ below as a `polynomial', we really mean a \emph{quasipolynomial} (which may also contain $\smsh$), i.e.\ a polynomial in the \emph{length} of $l$, as a slight abuse of notation.

\begin{definition}

	[Length bounded witness function]

	For a $\Sigma^\safe_{i}$ formula $A$ with a compatible sorting $(\vec u ; \vec x)$, we define the \emph{length-bounded witness function} $\wit{\vec u ; \vec x}{A} (l, \vec u ; \vec x , w)$ in $\bc (\charfn{}{i-1})$ and its \emph{bounding polynomial} $b_A (l)$ as follows:

	\begin{itemize}

		\item If $A$ is $\Pi^\safe_{i-1}$ then $\wit{\vec u ; \vec x}{A} (l, \vec u ; \vec x , w) \dfn \charfn{\vec u ; \vec x}{A} (l, \vec u ; \vec x )$ and we set $b_A (l) = 1$.

		\item If $A$ is $B \cor C$ then we may set $b_A = O(b_B + b_C)$ and define $		\wit{\vec u ; \vec x}{A} (l, \vec u ;\vec x , w) \dfn		\orfn ( ; \wit{\vec u ; \vec x}{B} (l, \vec u ; \vec x , \beta (b_B (l) , 0 ; w ) ) , \wit{\vec u ; \vec x}{C} (l, \vec u ; \vec x , \beta (b_C (l) , 0 ; w ) )  )$.

%		\[

%		\wit{\vec u ; \vec x}{A} (l, \vec u ;\vec x , w) 

%		\quad \dfn \quad

%		\orfn ( ; \wit{\vec u ; \vec x}{B} (l, \vec u ; \vec x , \beta (b_B (l) , 0 ; w ) ) , \wit{\vec u ; \vec x}{C} (l, \vec u ; \vec x , \beta (b_C (l) , 0 ; w ) )  )

%		\]

%		and we may set $b_A = O(b_B + b_C)$.

		\item Similarly if $A $ is $B \cand C$, but with $\andfn$ in place of $\orfn$.

%		\item If $A$ is $B \cand C$ then

%			\[

%			\wit{\vec u ; \vec x}{A} (l, \vec u ;\vec x , w) 

%			\quad \dfn \quad

%			\andfn ( ; \wit{\vec u ; \vec x}{B} (l, \vec u ; \vec x , \beta (b_B (l) , 0 ; w ) ) , \wit{\vec u ; \vec x}{C} (l, \vec u ; \vec x , \beta (b_C (l) , 0 ; w ) )  )

%			\]

%			and we may set $b_A = O(b_B + b_C)$.

		\item If $A$ is $\forall u \leq |t(\vec u;)| . B(u)$ we appeal to sharply bounded closure, Lemma~\ref{lem:sharply-bounded-recursion}, to define

		\(

		\wit{\vec u ; \vec x}{A}

		 \dfn

		\forall u \leq |t|.

		\wit{u, \vec u ; \vec x}{B(u)} (l, u, \vec u ; \vec x , \beta( b_{B(t)} (l) , u ; w ) )

		\)

		%appealing to Lemma~\ref{lem:sharply-bounded-recursion}, 

		and 

		we set 

		$b_A = O(b_{B(t)}^2 )$.

		\item Similarly if $A$ is $\exists u^\normal \leq |t(\vec u;)|. A'(u)$, but with $\exists u \leq |t|$ in place of $\forall u \leq |t|$.

		\item If $A$ is $\exists x^\safe . B(x) $ then

		\(

		\wit{\vec u ; \vec x}{A}

		\dfn 

		\wit{\vec u ; \vec x , x}{B(x)} ( l, \vec u ; \vec x , \beta( b_{B} (l) , 0;w ) , \beta (q(l) , 1 ;w ))

		\)

		where $q$ is obtained by the polychecking and bounded minimisation properties, Lemmas~\ref{lem:polychecking} and \ref{lem:bounded-minimisation}, for $\wit{\vec u ; \vec x , x}{B(x)}$.

		We may set $b_A = O(b_B + q )$.

	\end{itemize}

%	\[

%	\begin{array}{rcl}

%	\wit{\vec u ; \vec x}{A} (l, \vec u ; \vec x , w) & \dfn & \charfn{}{A} (l, \vec u ; \vec x)  \text{ if $A$ is $\Pi_i$} \\

%	\smallskip

%	\wit{\vec u ; \vec x}{A \cor B} (l,\vec u ; \vec x , \vec w^A , \vec w^B) & \dfn & \cor ( ; \wit{\vec u ; \vec x}{A} (l,\vec u ; \vec x , \vec w^A) ,\wit{\vec u ; \vec x}{B} (l,\vec u ; \vec x , \vec w^B)  )  \\

%	\smallskip

%	\wit{\vec u ; \vec x}{A \cand B} (l,\vec u ; \vec x , \vec w^A , \vec w^B) & \dfn & \cand ( ; \wit{\vec u ; \vec x}{A} (l,\vec u ; \vec x , \vec w^A) ,\wit{\vec u ; \vec x}{B} (l,\vec u ; \vec x , \vec w^B)  )  \\

%	\smallskip

%	\wit{\vec u ; \vec x}{\exists x^\safe . A(x)} (l,\vec u ; \vec x , \vec w , w) & \dfn & \wit{\vec u ; \vec x , x}{A(x)} ( l,\vec u ; \vec x , w , \vec w )

%	\\

%	\smallskip

%	\wit{\vec u ; \vec x}{\forall u \leq |t(\vec u;)| . A(x)} (l , \vec u ; \vec x, w) & \dfn & 

%	\forall u \leq |t(\vec u;)| . \wit{u , \vec u ; \vec x}{A(u)} (l, u , \vec u ; \vec x, \beta(u;w) )

%	\end{array}

%	\]

%	\anupam{need length bounding for sharply bounded quantifiers}

\end{definition}

\begin{proposition}

	\label{prop:wit-rfn}

	If, for some $w$, $\wit{\vec u ; \vec x}{A} (l, \vec u ; \vec x,w) =1$, then $A (\vec u \mode l ; \vec x \mode l)$ is true.

Conversely, if $A (\vec u \mode l ; \vec x \mode l)$ is true then there is some $w \leq b_A(l)$ such that $\wit{\vec u ; \vec x}{A} (l, \vec u ; \vec x,w) =1$.

\end{proposition}

In order to prove Thm.~\ref{thm:soundness} we need the following lemma, essentially giving an interpretation of $\arith^i$ proofs into $\mubci{i-1}$.

\begin{lemma}

		[Proof interpretation]

		\label{lem:proof-interp}

	From a typed-variable normal form $\arith^i$ proof $\pi$ of a $\Sigma^\safe_i$ sequent $\normal(\vec u), \safe(\vec x) , \Gamma  \seqar \Delta$

	there are $\bc (\charfn{}{i-1})$ functions $ f^\pi_B (\vec u ; \vec x , w)$ for $B\in\Delta$ such that

	% such that, for any $l, \vec u ; \vec x  , w$, we have:

	\[

%	\vec a^\nu = \vec u ,

%	\vec b^\sigma = \vec u, 

%	\bigwedge\limits_{A \in \Gamma} \wit{\vec u ; \vec x}{ A} (l, \vec u ; \vec x , w_A) =1

%	\ \implies \

%	\bigvee\limits_{B\in \Delta} \wit{\vec u ; \vec x}{B} (l, \vec u ; \vec x , f^\pi_B((\vec u ; \vec x )\mode l, \vec w \mode p(l))) = 1

	\begin{array}{rl}

&	\bigwedge\limits_{A \in \Gamma} \wit{\vec u ; \vec x}{ A} (l, \vec u ; \vec x , w_A \mode b_A(l)) =1 \\

\noalign{\medskip}

\implies & 	\bigvee\limits_{B\in \Delta} \wit{\vec u ; \vec x}{B} (l, \vec u ; \vec x , f^\pi_B((\vec u ; \vec x )\mode l, \vec w \mode p(l))) = 1

	\end{array}

	\]

	for some polynomial $p$.

%	\anupam{Need $\vec w \mode p(l)$ for some $p$.}

%	\anupam{$l$ may occur freely in the programs $f^\pi_B$}

\end{lemma}

Now we can prove the soundness result:

	\begin{proof}

		[Proof sketch of Thm.~\ref{thm:soundness} from Lemma~\ref{lem:proof-interp}]

		Suppose $\arith^i \proves \forall \vec u^\normal . \exists x^\safe . A(\vec u ; x)$. By inversion and Thm.~\ref{thm:normal-form} there is a $\arith^i$ proof $\pi$ of $\normal (\vec u ) \seqar \exists x^\safe. A(\vec u ; x )$ in typed variable normal form.

By Lemma~\ref{lem:proof-interp}, we have a $\mubci{i-1}$ function $f^\pi$ with $\wit{\vec u ;}{\exists x^\safe . A} (l, \vec u ; f(\vec u \mode l;)) =1$.

By the definition of $\wit{}{}$ and Prop.~\ref{prop:wit-rfn} we have that $\exists x . A(\vec u \mode l; x)$ is true just if $A(\vec u \mode l ; \beta (q(l), 1 ; f(\vec u \mode l;) ))$ is true.

Now, since all $\vec u$ are normal, we may simply set $l$ to have a longer length than all of these arguments, so the function $f(\vec u;) \dfn \beta (q(\sum \vec u), 1 ; f(\vec u \mode \sum \vec u;) ))$ suffices to finish the proof.

	\end{proof}

\documentclass[a4paper]{amsart}

\usepackage{amsmath}

\usepackage{amsthm}

\usepackage{amssymb}

\usepackage{microtype}

\usepackage[dvipsnames]{xcolor}

\usepackage{hyperref}

\bibliographystyle{plainurl}% the recommended bibstyle

\usepackage[lutzsyntax]{virginialake}

\input{ph-macros}

\title[Polynomial hierarchy in an unbounded arithmetic]{An implicit characterisation of the polynomial hierarchy in an unbounded arithmetic}

\author{Patrick Baillot}

\author{Anupam Das}

\begin{document}

\maketitle

\begin{abstract}

We consider extensions of theories based on the Bellantoni-Cook function algebra for polynomial time functions ($\fptime$) by induction principles without bounds on quantifiers. Instead, we limit quantification to `safe' arguments and show that the provably total functions are just those of the functional polynomial hierarchy ($\fph$). Our witness extraction proof relies on \emph{free-cut elimination} in the logic, making use of the \emph{witness function method}, due to Buss, rather than realisability and Dialectica approaches more common in implicit complexity. Our results closely resemble analogous ones from bounded arithmetic, only for an unbounded setting, and the proof generalises those for previous approaches characterising $\fptime$ via ramified theories. 

%\patrick{Remove: We present further comparisons to the bounded arithmetic setting and give tiered arithmetic theories analogous to the Si2 and Vi hierarchies of bounded arithmetic.} 

\end{abstract}

%\begin{abstract}

%We consider extensions of equational theories based on the Bellantoni-Cook function algebra for FPTIME by induction principles without bounds on quantifiers. Instead, we limit quantification to 'safe' variables and show that the provably total functions are just those of FPH. This closely resembles analogous results from bounded arithmetic, only for an unbounded setting, and the proof generalises those for previous approaches characterising FPTIME via the Bellantoni-Cook framework. We present further comparisons to the bounded arithmetic setting and give two-sorted arithmetic theories analogous to the Si2 and Vi hierarchies of bounded arithmetic. 

% \end{abstract}

\input{intro}

\input{preliminaries}

%\input{sequence-coding}

\input{arithmetic}

\input{soundness}

\input{completeness}

%\input{further}

\input{conclusions}

%\subparagraph*{Acknowledgements.}

%

%I want to thank \dots

%%

%% Bibliography

%%

%% Either use bibtex (recommended), 

\newpage

\bibliographystyle{alpha}

\bibliography{ph-biblio}

%% .. or use the thebibliography environment explicitely

\newpage

\appendix

\input{appendix-arithmetic}

%%\input{pv-theories}	

%\input{appendix-sequent-calculus}

%\input{appendix-soundness}

\input{appendix-completeness}

\end{document}

% VirginiaLake LaTeX macros by Alessio Guglielmi

%

% Many thanks to Ross Moore (Macquarie University) for suggestions leading 

% to \vlupdate

\NeedsTeXFormat{LaTeX2e}%

\ProvidesPackage{virginialake}[2015/08/30 v3.0]

\newif\ifvirginialakeusesxy

        \virginialakeusesxytrue

\DeclareOption{noxy}{\virginialakeusesxyfalse}%

\newif\ifvirginialakegoodsyntax

        \virginialakegoodsyntaxfalse

\DeclareOption{goodsyntax}{\virginialakegoodsyntaxtrue}%

\newif\ifvirginialakelutzsyntax

        \virginialakelutzsyntaxfalse

\DeclareOption{lutzsyntax}{\virginialakelutzsyntaxtrue}%

\ProcessOptions

\@ifclassloaded{beamer}%

               {\RequirePackage{etex}}%

               {}%

\let\circledS\undefined\RequirePackage{amssymb}%

\RequirePackage{stmaryrd}%

\RequirePackage{ifthen}%

\RequirePackage{ifpdf}%

\RequirePackage{etoolbox}%

\newif\ifvirginialakepdflatex\ifpdf\virginialakepdflatextrue\else

                                   \virginialakepdflatexfalse\fi

\@ifpackageloaded{fp-basic}%

                 {\relax}%

                 {\RequirePackage{fp-basic}\FPmessagesfalse}%

\@ifpackageloaded{xcolor}%

                 {\relax}%

                 {\RequirePackage[usenames]{xcolor}}%

\ifvirginialakeusesxy

    \ifvirginialakepdflatex

       \RequirePackage[line,arrow,curve,frame,color,crayon,pdf]{xy}%

       \newxycolor{afbackground}{0 0 0 0.12 cmyk}%

       \makeatletter\renewcommand\xywarning@[1]{\relax}\catcode`@=11

       \W@{}%

       \W@{VirginiaLake Warning: Xy-pic warnings are suppressed in PDF mode.}%

       \W@{}%

    \else

       \RequirePackage[line,arrow,curve,frame,color,crayon,ps,dvips]{xy}%

       \newxycolor@{afbackground}{0 0 0 0.12}{cmyk}{}{}%

   \fi

\fi

\newif\ifetex

\AtBeginDocument{\@ifpackageloaded{etex}{\etextrue}{\etexfalse}}%

%----------------------------------------------------------------------- IFMTARG

% Code from ifmtarg.sty, reproduced below with permission - A.G.

%

% ifmtarg.sty

%

% Provides an if-then-else command for an empty macro argument

% (empty = zero or more spaces only)

% Use as \@ifmtarg{arg1}{Code for arg1 empty}{Code for arg1 not empty}%

%

% author: Peter Wilson (CUA)

%         (now at peter.r.wilson@boeing.com)

% Copyright Peter Wilson, 1996

% Copyright Peter Wilson and Donald Arseneau, 2000

% Released under the LaTeX Project Public License

%

%% Commands by Donald Arseneau

\begingroup

\catcode`\Q=3

\long\gdef\@ifmtarg#1{\@xifmtarg#1QQ\@secondoftwo\@firstoftwo\@nil}%

\long\gdef\@xifmtarg#1#2Q#3#4#5\@nil{#4}%

\long\gdef\@ifnotmtarg#1{\@xifmtarg#1QQ\@firstofone\@gobble\@nil}%

\endgroup

%---------------------------------------------------------------- END OF IFMTARG

%------------------------------------------------------------ MACROS FOR SYMBOLS

  \newcommand\one{{\mathsf 1}}%

  \newcommand\zer{{\mathsf 0}}%

  \newcommand\fff{{\mathsf f}}%

  \newcommand\ttt{{\mathsf t}}%

  \newcommand\sw {{\mathsf s}}%

  \newcommand\me {{\mathsf m}}%

  \newcommand\iD {{\mathsf i}{\downarrow}}%

  \newcommand\iU {{\mathsf i}{  \uparrow}}%

  \newcommand\cD {{\mathsf c}{\downarrow}}%

  \newcommand\cU {{\mathsf c}{  \uparrow}}%

  \newcommand\wD {{\mathsf w}{\downarrow}}%

  \newcommand\wU {{\mathsf w}{  \uparrow}}%

  \newcommand\qD {{\mathsf q}{\downarrow}}%

  \newcommand\qU {{\mathsf q}{  \uparrow}}%

  \newcommand\BV {{\mathsf {BV}}}%

  \newcommand\SBV{{\mathsf{SBV}}}%

  \newcommand\KS {{\mathsf {KS}}}%

  \newcommand\SKS{{\mathsf{SKS}}}%

%---------------------------------------------------------------- END OF SYMBOLS

%------------------------------------------------ MACROS FOR FORMULAE/STRUCTURES

\newif\ifvlsmallops\vlsmallopsfalse

\newcommand\vlbin[1]{\ifvlsmallops\mathchoice

      {\mathbin{\raise.2ex \hbox{$\scriptstyle      #1$}}}%

      {\mathbin{\raise.2ex \hbox{$\scriptstyle      #1$}}}%

      {\mathbin{\raise.12ex\hbox{$\scriptscriptstyle#1$}}}%

      {\mathbin{           \hbox{$\scriptscriptstyle#1$}}}\else\mathbin{#1}\fi}%

\newif\ifvllinear\vllinearfalse

\newcommand{\vlor}{\ifvllinear\vlbin\varoplus\else\vlbin\vee\fi}%

\newcommand{\vlan}{\ifvllinear\vlbin\binampersand\else\vlbin\wedge\fi}%

\newcommand{\vlpa}{\vlbin\bindnasrepma}%

\newcommand{\vlte}{\vlbin\varotimes}%

\newcommand{\vlse}{\vlbin\triangleleft}%

\newcommand{\vlim}{\vlbin\to}%

\newcommand{\vlli}{\vlbin\multimap}%

\newcommand{\vlmi}{\vlbin\leftarrow}%

\newcommand{\vldi}{\vlbin\leftrightarrow}%

\newcommand{\vlne}{\vlbin\neg}%

\newcommand{\vljm}{\vlbin\supset}%

\newcommand{\vlmj}{\vlbin\subset}%

\newcommand{\vlgoodsyntax}{%

   \def\vlleftparbracket   {\ifvirginialakesmallbrackets[\else

                                       \mathopen{}\left [\fi}%

   \def\vlrightparbracket  {\ifvirginialakesmallbrackets]\else

                                                  \right]\mathclose{}\fi}%

   \let\vlleftparbracketex \vlleftparbracket

   \let\vlrightparbracketex\vlrightparbracket

   \let\vlleftparbracketcn \vlleftparbracket

   \let\vlrightparbracketcn\vlrightparbracket

   \def\vlleftcopbracket   {\ifvirginialakesmallbrackets(\else

                                       \mathopen{}\left (\fi}%

   \def\vlrightcopbracket  {\ifvirginialakesmallbrackets)\else

                                                  \right)\mathclose{}\fi}%

   \let\vlleftcopbracketex \vlleftcopbracket

   \let\vlrightcopbracketex\vlrightcopbracket

   \let\vlleftcopbracketcn \vlleftcopbracket

   \let\vlrightcopbracketcn\vlrightcopbracket

   \def\vlleftseqbracket   {\ifvirginialakesmallbrackets\langle\else

                                        \mathopen{}\left\langle\fi}%

   \def\vlrightseqbracket  {\ifvirginialakesmallbrackets\rangle\else

                                                  \right\rangle\mathclose{}\fi}%

   \let\vlleftseqbracketex \vlleftseqbracket

   \let\vlrightseqbracketex\vlrightseqbracket

   \let\vlleftseqbracketcn \vlleftseqbracket

   \let\vlrightseqbracketcn\vlrightseqbracket

   \def\vldsaaux{\ifx\vlxspacetmp\vldsa\vlx\vlx\vlx\togglexspacefalse\else

                  \iftogglexspace\vlx\else\togglexspacetrue\fi\fi}%

   \def\vldsa{\futurelet\vlxspacetmp\vldsaaux}%

   \def\vlcsaaux{\ifx\vlxspacetmp\vlcsa\vlx\vlx\vlx\togglexspacefalse\else

                  \iftogglexspace\vlx\else\togglexspacetrue\fi\fi}%

   \def\vlcsa{\futurelet\vlxspacetmp\vlcsaaux}%

   \def\vldsmaux{\ifx\vlxspacetmp\vldsm\vlx\vlx\vlx\togglexspacefalse\else

                  \iftogglexspace\vlx\else\togglexspacetrue\fi\fi}%

   \def\vldsm{\futurelet\vlxspacetmp\vldsmaux}%

   \def\vlcsmaux{\ifx\vlxspacetmp\vlcsm\vlx\vlx\vlx\togglexspacefalse\else

                  \iftogglexspace\vlx\else\togglexspacetrue\fi\fi}%

   \def\vlcsm{\futurelet\vlxspacetmp\vlcsmaux}%

   \def\vlnsmaux{\ifx\vlxspacetmp\vlnsm\vlx\vlx\vlx\togglexspacefalse\else

                  \iftogglexspace\vlx\else\togglexspacetrue\fi\fi}%

   \def\vlnsm{\futurelet\vlxspacetmp\vlnsmaux}%

   \let\vldots=\dots}%

\newcommand{\vlx}{\;}%

\newif\iftogglexspace\togglexspacetrue

\newcommand{\vlsetoperators}{%

   \def\vldsaaux{\ifx\vlxspacetmp\vldsa\vlx\vlor\vlx\togglexspacefalse\else

                  \iftogglexspace\vlor\else\togglexspacetrue\fi\fi}%

   \def\vldsa{\futurelet\vlxspacetmp\vldsaaux}%

   \def\vlcsaaux{\ifx\vlxspacetmp\vlcsa\vlx\vlan\vlx\togglexspacefalse\else

                  \iftogglexspace\vlan\else\togglexspacetrue\fi\fi}%

   \def\vlcsa{\futurelet\vlxspacetmp\vlcsaaux}%

   \def\vldsmaux{\ifx\vlxspacetmp\vldsm\vlx\vlpa\vlx\togglexspacefalse\else

                  \iftogglexspace\vlpa\else\togglexspacetrue\fi\fi}%

   \def\vldsm{\futurelet\vlxspacetmp\vldsmaux}%

   \def\vlcsmaux{\ifx\vlxspacetmp\vlcsm\vlx\vlte\vlx\togglexspacefalse\else

                  \iftogglexspace\vlte\else\togglexspacetrue\fi\fi}%

   \def\vlcsm{\futurelet\vlxspacetmp\vlcsmaux}%

   \def\vlnsmaux{\ifx\vlxspacetmp\vlnsm\vlx\vlse\vlx\togglexspacefalse\else

                  \iftogglexspace\vlse\else\togglexspacetrue\fi\fi}%

   \def\vlnsm{\futurelet\vlxspacetmp\vlnsmaux}%

   \let\vldots=\cdots}%

\newcommand{\vllutzsyntax}{%

   \def\vlleftparbracket   {\ifvirginialakesmallbrackets[\else

                                       \mathopen{}\left [\fi}%

   \def\vlrightparbracket  {\ifvirginialakesmallbrackets]\else

                                                  \right]\mathclose{}\fi}%

   \let\vlleftparbracketex \relax

   \let\vlrightparbracketex\relax

   \let\vlleftparbracketcn \{

   \let\vlrightparbracketcn\}%

   \def\vlleftcopbracket   {\ifvirginialakesmallbrackets(\else

                                       \mathopen{}\left (\fi}%

   \def\vlrightcopbracket  {\ifvirginialakesmallbrackets)\else

                                                  \right)\mathclose{}\fi}%

   \let\vlleftcopbracketex \relax

   \let\vlrightcopbracketex\relax

   \let\vlleftcopbracketcn \{

   \let\vlrightcopbracketcn\}%

   \def\vlleftseqbracket   {\ifvirginialakesmallbrackets\langle\else

                                        \mathopen{}\left\langle\fi}%

   \def\vlrightseqbracket  {\ifvirginialakesmallbrackets\rangle\else

                                                  \right\rangle\mathclose{}\fi}%

   \let\vlleftseqbracketex \relax

   \let\vlrightseqbracketex\relax

   \let\vlleftseqbracketcn \{

   \let\vlrightseqbracketcn\}%

   \vlsetoperators

   \vlsmallopstrue}%

\newcommand{\vlnogoodsyntax}{%

   \def\vlleftparbracket   {\ifvirginialakesmallbrackets(\else

                                       \mathopen{}\left (\fi}%

   \def\vlrightparbracket  {\ifvirginialakesmallbrackets)\else

                                                  \right)\mathclose{}\fi}%

   \let\vlleftparbracketex \relax

   \let\vlrightparbracketex\relax

   \let\vlleftparbracketcn \{

   \let\vlrightparbracketcn\}%

   \let\vlleftcopbracket   \vlleftparbracket

   \let\vlrightcopbracket  \vlrightparbracket

   \let\vlleftcopbracketex \relax

   \let\vlrightcopbracketex\relax

   \let\vlleftcopbracketcn \{

   \let\vlrightcopbracketcn\}%

   \let\vlleftseqbracket   \vlleftparbracket

   \let\vlrightseqbracket  \vlrightparbracket

   \let\vlleftseqbracketex \relax

   \let\vlrightseqbracketex\relax

   \let\vlleftseqbracketcn \{

   \let\vlrightseqbracketcn\}%

   \vlsetoperators}%

\ifvirginialakegoodsyntax

   \vlgoodsyntax

\else

   \ifvirginialakelutzsyntax

      \vllutzsyntax

   \else

      \vlnogoodsyntax

   \fi

\fi

\newif\ifvirginialakesmallbrackets\virginialakesmallbracketsfalse

\newcommand{\vlsmallbrackets}{\virginialakesmallbracketstrue}%

\newcommand{\vlnosmallbrackets}{\virginialakesmallbracketsfalse}%

\newcommand{\vlprepstructuresaux}{\catcode`.=\active

                                  \catcode`;=\active

                                  \catcode`[=\active

                                  \catcode`]=\active

                                  \catcode`(=\active

                                  \catcode`)=\active

                                  \catcode`<=\active

                                  \catcode`>=\active

                                  \catcode`-=\active}%

\newcommand{\lt}{<}%

\newcommand{\gt}{>}%

\let\vldot  .

\let\vlscol ;

\let\vlsqbrl[

\let\vlsqbrr]

\let\vlrobrl(

\let\vlrobrr)

\let\vlanbrl<

\let\vlanbrr>

\let\vlminus-

\newif\ifvirginialakestructuressyntax\virginialakestructuressyntaxtrue

\newcommand{\vlnostructuressyntax}{\virginialakestructuressyntaxfalse}%

\newcommand{\vlgobble}[1]{}%

{%--------------------------------------

\vlprepstructuresaux

\gdef\vlnos{\let.\vldot

            \let;\vlscol

            \let[\vlsqbrl

            \let]\vlsqbrr

            \let(\vlrobrl

            \let)\vlrobrr

            \let<\vlanbrl

            \let>\vlanbrr

            \let-\vlminus}%

\gdef\vlprepstructures{\ifvirginialakestructuressyntax

                          \vlprepstructuresaux\vlnos\fi}%

\gdef\vlparopen  {\vlleftparbracket  \bgroup\catcode`.=\active\let.\vldsa

                                            \catcode`;=\active\let;\vldsm

                                            \catcode`]=\active\let]\vlparclose}%

\gdef\vlparopenex{\vlleftparbracketex\bgroup\catcode`.=\active\let.\vldsa

                                            \catcode`;=\active\let;\vldsm\vlsbr

                                          \catcode`]=\active\let]\vlparcloseex}%

\gdef\vlparopencn{\vlleftparbracketcn\bgroup\catcode`.=\active\let.\vldsa

                                            \catcode`;=\active\let;\vldsm\vlsbr

                                          \catcode`]=\active\let]\vlparclosecn}%

\gdef\vlcopopen  {\vlleftcopbracket  \bgroup\catcode`.=\active\let.\vlcsa

                                            \catcode`;=\active\let;\vlcsm

                                            \catcode`)=\active\let)\vlcopclose}%

\gdef\vlcopopenex{\vlleftcopbracketex\bgroup\catcode`.=\active\let.\vlcsa

                                            \catcode`;=\active\let;\vlcsm\vlsbr

                                          \catcode`)=\active\let)\vlcopcloseex}%

\gdef\vlcopopencn{\vlleftcopbracketcn\bgroup\catcode`.=\active\let.\vlcsa

                                            \catcode`;=\active\let;\vlcsm\vlsbr

                                          \catcode`)=\active\let)\vlcopclosecn}%

\gdef\vlseqopen  {\vlleftseqbracket  \bgroup\catcode`;=\active\let;\vlnsm

                                            \catcode`>=\active\let>\vlseqclose}%

\gdef\vlseqopenex{\vlleftseqbracketex\bgroup\catcode`;=\active\let;\vlnsm\vlsbr

                                          \catcode`>=\active\let>\vlseqcloseex}%

\gdef\vlseqopencn{\vlleftseqbracketcn\bgroup\catcode`;=\active\let;\vlnsm\vlsbr

                                          \catcode`>=\active\let>\vlseqclosecn}%

\gdef\vls  {\catcode`[=\active\let[\vlparopenex

            \catcode`(=\active\let(\vlcopopenex

            \catcode`<=\active\let<\vlseqopenex

            \catcode`-=\active\let-\bar

            \odframefirstfalse

            \odbackgroundfirstfalse}%

\gdef\vlsbr{\catcode`[=\active\let[\vlparopen

            \catcode`(=\active\let(\vlcopopen

            \catcode`<=\active\let<\vlseqopen

            \catcode`-=\active\let-\bar

            \odframefirstfalse

            \odbackgroundfirstfalse}%

\gdef\vlscn{\catcode`[=\active\let[\vlparopencn

            \catcode`(=\active\let(\vlcopopencn

            \catcode`<=\active\let<\vlseqopencn

            \catcode`-=\active\let-\bar

            \odframefirstfalse

            \odbackgroundfirstfalse}%

\gdef\vlupdate #1{

   \expandafter\let\csname\expandafter\vlgobble\string #1vltemp\endcsname #1

   \def #1{\bgroup\vlprepstructures

     \csname\expandafter\vlgobble\string #1vlaux\endcsname}%

   \expandafter\def\csname\expandafter\vlgobble\string #1vlaux\endcsname ##1{%

      \csname\expandafter\vlgobble\string #1vltemp\endcsname{##1}\egroup}}%

}%--------------------------------------

\newcommand{\vlparclose  }{\egroup\vlrightparbracket  }%

\newcommand{\vlparcloseex}{\egroup\vlrightparbracketex}%

\newcommand{\vlparclosecn}{\egroup\vlrightparbracketcn}%

\newcommand{\vlcopclose  }{\egroup\vlrightcopbracket  }%

\newcommand{\vlcopcloseex}{\egroup\vlrightcopbracketex}%

\newcommand{\vlcopclosecn}{\egroup\vlrightcopbracketcn}%

\newcommand{\vlseqclose  }{\egroup\vlrightseqbracket  }%

\newcommand{\vlseqcloseex}{\egroup\vlrightseqbracketex}%

\newcommand{\vlseqclosecn}{\egroup\vlrightseqbracketcn}%

\newcommand{\vlhole}{\{\kern.3em\}}%

\newcommand{\vlstore}{\bgroup\vlprepstructures\afterassignment\egroup

                      \global\def\vlread}%

%----------------------------------------- END OF MACROS FOR FORMULAE/STRUCTURES

%-------------------------------------------------------- MACROS FOR DERIVATIONS

%

%                                                   +-------+--------+-------+

%                                                   |  dcl  |  dcc   |  dcr  |

%                                                   +-------+--------+-------+

%                                                       +---+        +---+

%                                                       | l |--------| m |

%                                                       +---+        +---+

%                                                             +----+

%                                                             | dc |

%                                                             +----+

%                                                   <---dl--->      <---dr--->

%

\newdimen\dercldim                                % dcl

\newdimen\derccdim                                % dcc

\newdimen\dercrdim                                % dcr

\newdimen\derdim                                  % d

\newdimen\derdldim                                % ddl

\newdimen\derdrdim                                % ddr

\newbox\derboxtwo                                 % b2

\newbox\derboxthree                               % b3

\newbox\derboxfour                                % b4

\newdimen\derquad

\newdimen\deropen

\newbox\stembox

\newcount\vlsavederboxonec

%\newcount\vlsavederdimc

\newcount\vldummycount

% THE FOLLOWING IS VERY DANGEROUS: WE ARE CREATING A 'VIRTUAL MEMORY MANAGER'

% FOR \derboxone, \derldim, \dercdim AND \derrdim, IN PARTICULAR BY USING

% \count11 AND \count14. ETEX MIGHT INTERFERE WITH THIS STUFF. START FROM 

% HERE IF YOU SEE SOMETHING ODD SUCH AS DUPLICATION OR MISPLACEMENT OF BOXES IN 

% DERIVATIONS

\newcommand{\vlderivationinitaux}{%

   \newbox\derboxone                              % b1

   \setbox\derboxone=\hbox{}%

   \vlsavederboxonec=\derboxone

%   \vlsavederdimc=\count11\advance\vlsavederdimc by1%

   \newdimen\derldim                              % dl

   \newdimen\dercdim                              % dc

   \newdimen\derrdim}%                            % dr

\newcommand{\vlderivationinit}{\bgroup

   \vlprepstructures\vlderivationinitaux}%

\newcommand{\vlderivationterm}{\egroup

   \global\chardef\derboxone=\vlsavederboxonec

   \ifetex

      \ifnum\count264>256

         \global\advance\count264 by-1

      \else

         \global\advance\count14 by-1

      \fi

   \else\global\advance\count14 by-1

   \fi

   \ifetex

      \ifnum\count261>258

         \global\advance\count261 by-3

      \else

         \ifnum\count261>257

            \global\advance\count261 by-2

            \global\advance\count11  by-1

         \else

            \ifnum\count261>256

               \global\advance\count261 by-1

               \global\advance\count11  by-2

            \else

               \global\advance\count11 by-3

            \fi

         \fi

      \fi

   \else\global\advance\count11 by-3

   \fi

%   \global\dimendef\derldim=\vlsavederdimc

%   \global\advance\vlsavederdimc by1%

%   \global\dimendef\dercdim=\vlsavederdimc

%   \global\advance\vlsavederdimc by1%

%   \global\dimendef\derrdim=\vlsavederdimc

%   \global\advance\vlsavederdimc by-2

   }%

\newcommand{\vlderivationaux}[1]{#1\vcenter{\box\derboxone}\vlderivationterm}%

\newcommand{\vlderivation}{\vlderivationinit\vlderivationaux}%

\newcommand{\vlhyaux}[1]{\global\setbox\derboxone=\hbox{#1}%

   \global\derldim=0pt%                           % dl=0

   \global\dercdim=\wd\derboxone                  % dc=wd(b1)

   \global\derrdim=0pt%                           % dr=0

   }%

\newbox\vlhybox

\newcommand{\vlhy}[1]{\global\setbox\vlhybox=\hbox{\strut$#1$}%

   \vlhyaux{\box\vlhybox}}%

\newcommand{\vlstemaux}{\dercldim=\derldim

                        \derccdim=\dercdim

                        \dercrdim=\derrdim}%

\newcommand{\vldaux}[6]{\setbox\derboxtwo=\hbox{\unhbox\derboxone}%

                                                  % b2=b1

   \setbox\derboxthree=\hbox{$#1$}%               % b3; l=wd(b3)

   \setbox\derboxfour =\hbox{$#2$}%               % b4; m=wd(b4)

   #3                                             % dl=0, dc=wd(b1), dr=0

   \derdim=\dercdim\advance\derdim by-\derccdim\divide\derdim by2%

                                                  % d=(dc-dcc)/2

   \global\derldim=\dercldim\global\advance\derldim by-\derdim

                                                  % dl=dcl-d

   \global\derrdim=\dercrdim\global\advance\derrdim by-\derdim

                                                  % dr=dcr-d

   \deropen=\fontdimen5\textfont2\divide\deropen by3%

   \setbox\derboxone=\hbox{\vbox{\offinterlineskip

         \hbox{\ifdim\derldim<0pt\kern-\derldim\fi

               \box\derboxtwo

               \ifdim\derrdim<0pt\kern-\derrdim\fi}%

         #4%

         \hbox{\ifdim\dercldim>\derldim

                  \ifdim\derldim>0pt\kern\derldim\fi

                  \else\kern\dercldim\fi

               \hbox to0pt{\hss\copy\derboxthree}%

               \vbox{\ifdim\derccdim>\dercdim\hsize=\derccdim

                                        \else\hsize=\dercdim \fi

                    #5}%

               \hbox to0pt{\copy\derboxfour\hss}%

               \ifdim\dercrdim>\derrdim

                  \ifdim\derrdim>0pt\kern\derrdim\fi

                  \else\kern\dercrdim\fi}%

         #6%

         \hbox{\ifdim\derldim>0pt\kern\derldim\fi

               \box\derboxone

               \ifdim\derrdim>0pt\kern\derrdim\fi}}}%

   \ifdim\derldim<0pt\global\derldim=0pt\fi       % dl=max(dl,0)

   \ifdim\derrdim<0pt\global\derrdim=0pt\fi       % dr=max(dr,0)

   \derdldim=\wd\derboxthree\advance\derdldim by-\dercldim

                                                  % ddl=l-dcl

   \derdrdim=\wd\derboxfour \advance\derdrdim by-\dercrdim

                                                  % ddr=m-dcr

   \ifdim\derdim<0pt%

      \ifdim\derdldim<0pt%

         \derdldim=0pt%                           % d<0, ddl<0 -> ddl=0

      \fi

      \ifdim\derdrdim<0pt%

         \derdrdim=0pt%                           % d<0, ddr<0 -> ddr=0

      \fi

   \else

      \ifdim\derldim>0pt%

         \ifdim\derdldim>-\derdim

            \advance\derdldim by\derdim           % d>=0, dl>0, ddl+d>0 -> 

         \else                                    %                    ddl=ddl+d

            \derdldim=0pt%                        % d>=0, dl>0, ddl+d<=0 ->

         \fi                                      %                        ddl=0

      \else

         \advance\derdldim by\dercldim            % d>=0, dl=0 -> ddl=ddl+dcl

      \fi

      \ifdim\derrdim>0pt%

         \ifdim\derdrdim>-\derdim

            \advance\derdrdim by\derdim           % d>=0, dr>0, ddr+d>0 -> 

         \else                                    %                    ddr=ddr+d

            \derdrdim=0pt%                        % d>=0, dr>0, ddr+d<=0 ->

         \fi                                      %                        ddr=0

      \else

         \advance\derdrdim by\dercrdim            % d>=0, dr=0 -> ddr=ddr+dcr

      \fi

   \fi

   \global\setbox\derboxone=\hbox

      {\kern\derdldim\unhbox\derboxone\kern\derdrdim}%

   \global\advance\derldim by\derdldim            % dl=dl+ddl

   \global\advance\derrdim by\derdrdim            % dr=dr+ddr

   }%

\newcommand{\vlstemraux }[4]{{#4}\vlstemaux\vldaux

   {\scriptstyle #1}%

   {\scriptstyle #2}%

   {\vlhyaux{#3}}%

   {\kern-\deropen\kern-\ht\strutbox\kern-\dp\strutbox}%

   {\hbox{$\vcenter{\vbox{\offinterlineskip

                    \hbox{$\copy\stembox$}}}$}}%

   {\kern-\deropen}}%

\newcommand{\vlstemrraux}[4]{{#4}\vlstemaux\vldaux

   {\scriptstyle #1}%

   {\scriptstyle #2}%

   {\vlhy{#3}}%

   {\kern\deropen}%

   {\hbox{\hfil}}%

   {\kern\deropen}}%

\newif\ifvlsmallleftlabels\vlsmallleftlabelstrue

\newcommand{\vlnosmallleftlabels}{\vlsmallleftlabelsfalse}%

\newcommand{\vlsmallleftlabels}{\vlsmallleftlabelstrue}%

\newcommand{\vlleftlabel }[1]{\@ifnotmtarg{#1}{\ifvlsmallleftlabels

                               \scriptstyle\fi #1\;}\relax}%

\newcommand{\vlrightlabel}[1]{\@ifnotmtarg{#1}{\;#1}\relax}%

\newdimen\vlstemheight\vlstemheight=8pt%

\newcommand{\vlvruler}{\hbox{\vrule width .6pt height \vlstemheightc sp

                             \kern1.2pt

                             \vrule width .6pt height \vlstemheightc sp}}%

\newcount\vlstemheightc

\newcommand{\vldf}[5]{\vldummycount=\vlstemheight

                      \FPmul\vlstemheightc{\the\vldummycount}{#5}%

   \setbox\stembox=\vbox to \vlstemheightc sp{\vlvruler}%

   \vlstemrraux{                }{                 }{#3              }  {%

   \vlstemraux {\vlleftlabel{#1}}{\vlrightlabel{#2}}{\kern\wd\stembox} {%

   \vlstemrraux{                }{                 }{\kern\wd\stembox}{%

   #4                                                                 }}}}%

\newcommand{\vlde}[4]{\vldf{#1}{#2}{#3}{#4}1}%

\newcommand{\vldd}[4]{\vldf{#1}{#2}{#3}{#4}2}%

\newcommand{\vlpf}[4]{\vldf{#1}{#2}{#3}%

   {\vlhyaux{\vbox to0pt{\vss\kern3pt\hrule width4.2pt\vss}}}{#4}}%

\newcommand{\vlpr}[3]{\vlpf{#1}{#2}{#3}1}%

\newcommand{\vlpd}[3]{\vlpf{#1}{#2}{#3}2}%

\newcommand{\vlproofaux}[4]{\vlderivationaux{\vlpf{#2}{#3}{#4}{#1}}}%

\newcommand{\vlproof }{\vlderivationinit\vlproofaux1}%

\newcommand{\vlproofd}{\vlderivationinit\vlproofaux2}%

\newcommand{\vlderaux}[5]{\vlderivationaux{\vldf{#2}{#3}{#4}{\vlhy{#5}}{#1}}}%

\newcommand{\vlder }{\vlderivationinit\vlderaux1}%

\newcommand{\vlderd}{\vlderivationinit\vlderaux2}%

\newcommand{\vlhruler}{\vfill\hbox to\hsize{\hrulefill}\vfill}%

\newcommand{\vlhhruler}{\vfill

                        \hbox to\hsize{\hrulefill}%

                        \kern1pt

                        \hbox to\hsize{\hrulefill}%

                        \vfill}%

\newcommand{\vlhdotter}{\vfill

   \hbox to\hsize{\cleaders\vbox to0pt{\vss

       \hbox{\kern-.35pt$.$\kern-.35pt}\vss}\hskip\hsize}\vfill}%

\newcommand{\vldsinaux}[3]{\vldaux

   {\smash{\ifvlsmallleftlabels\lower\fontdimen22\scriptfont2%

                          \else\lower\fontdimen22\textfont2\fi

                                       \hbox{$\vlleftlabel {#1}$}}}%

   {\smash{\lower\fontdimen22\textfont2\hbox{$\vlrightlabel{#2}$}}}%

   {\vlhy{#3}}%

   {\kern\deropen}%

   {\vbox to.4pt{\vlhruler}}%

   {\kern\deropen}}%

\newcommand{\vldsidaux}[3]{\vldaux

   {\smash{\ifvlsmallleftlabels\lower\fontdimen22\scriptfont2%

                          \else\lower\fontdimen22\textfont2\fi

                                       \hbox{$\vlleftlabel {#1}$}}}%

   {\smash{\lower\fontdimen22\textfont2\hbox{$\vlrightlabel{#2}$}}}%

   {\vlhy{#3}}%

   {\kern\deropen}%

   {\vbox to.4pt{\vlhdotter}}%

   {\kern\deropen}}%

\newdimen\vldsiqdimenleft

\newdimen\vldsiqdimenright

\newcommand{\vldsiqaux}[3]{\ifvlsmallleftlabels

                                \vldsiqdimenleft=\fontdimen22\scriptfont2%

                           \else\vldsiqdimenleft=\fontdimen22\textfont2\fi

                           \advance\vldsiqdimenleft  by-.7pt%

                           \vldsiqdimenright=\fontdimen22\textfont2%

                           \advance\vldsiqdimenright by-.7pt%

   \vldaux

   {\smash{\lower\vldsiqdimenleft \hbox{$\vlleftlabel {#1}$}}}%

   {\smash{\lower\vldsiqdimenright\hbox{$\vlrightlabel{#2}$}}}%

   {\vlhy{#3}}%

   {\kern\deropen\kern-.7pt}%

   {\vbox to1.8pt{\vlhhruler}}%

   {\kern\deropen\kern-.7pt}}%

\newbox\derboxin

\newdimen\derboxinwidth

\newcommand{\vliaux}[2]{#2%

   \dercldim=\derldim

   \derccdim=\dercdim

   \dercrdim=\derrdim

   \setbox\derboxin=\hbox{$#1$}%

   \derboxinwidth=1em\advance\derboxinwidth by-\wd\derboxin

   \ifdim\derboxinwidth>0pt\divide\derboxinwidth by2\else\derboxinwidth=0pt\fi}%

\newcommand{\vlin}[4]{\vliaux{#3}{#4}%

   \vldsinaux{#1}{#2}{\kern\derboxinwidth\box\derboxin\kern\derboxinwidth}}%

\newcommand{\vlid}[4]{\vliaux{#3}{#4}%

   \vldsidaux{#1}{#2}{\kern\derboxinwidth\box\derboxin\kern\derboxinwidth}}%

\newcommand{\vliq}[4]{\vliaux{#3}{#4}%

   \vldsiqaux{#1}{#2}{\kern\derboxinwidth\box\derboxin\kern\derboxinwidth}}%

\newcommand{\vliiaux}[2]{\derquad=\fontdimen6\textfont2%

   {#1}%

           \dercldim  =\derldim

           \derccdim  =\dercdim

   \setbox\derboxtwo=\hbox{\unhbox\derboxone\kern\derquad}%

   \advance\derccdim by\derrdim

   \advance\derccdim by\derquad

   {#2}%

   \setbox\derboxone=\hbox{\unhbox\derboxtwo\unhbox\derboxone}%

   \advance\derccdim by\derldim

   \advance\derccdim by\dercdim

           \dercrdim  =\derrdim}%

\newcommand{\vliin}[5]{\vliiaux{#4}{#5}\vldsinaux{#1}{#2}{#3}}%

\newcommand{\vliid}[5]{\vliiaux{#4}{#5}\vldsidaux{#1}{#2}{#3}}%

\newcommand{\vliiq}[5]{\vliiaux{#4}{#5}\vldsiqaux{#1}{#2}{#3}}%

\newcommand{\vldsauxx}{\setbox\derboxtwo=\hbox

   {\unhbox\derboxtwo\unhbox\derboxone\kern\derquad}%

   \advance\derccdim by\derldim

   \advance\derccdim by\dercdim

   \advance\derccdim by\derrdim

   \advance\derccdim by\derquad}%

\newcommand{\vldsiiiaux}[3]{\derquad=\fontdimen6\textfont2%

   {#1}%

           \dercldim  =\derldim

           \derccdim  =\dercdim

   \setbox\derboxtwo=\hbox{\unhbox\derboxone\kern\derquad}%

   \advance\derccdim by\derrdim

   \advance\derccdim by\derquad

   {#2}\vldsauxx

   {#3}%

   \setbox\derboxone=\hbox{\unhbox\derboxtwo\unhbox\derboxone}%

   \advance\derccdim by\derldim

   \advance\derccdim by\dercdim

           \dercrdim  =\derrdim}%

\newcommand{\vliiin}[6]{\vldsiiiaux{#4}{#5}{#6}\vldsinaux{#1}{#2}{#3}}%

\newcommand{\vliiid}[6]{\vldsiiiaux{#4}{#5}{#6}\vldsidaux{#1}{#2}{#3}}%

\newcommand{\vliiiq}[6]{\vldsiiiaux{#4}{#5}{#6}\vldsiqaux{#1}{#2}{#3}}%

\newcommand{\vldsiiiiaux}[4]{\derquad=\fontdimen6\textfont2%

   {#1}%

           \dercldim  =\derldim

           \derccdim  =\dercdim

   \setbox\derboxtwo=\hbox{\unhbox\derboxone\kern\derquad}%

   \advance\derccdim by\derrdim

   \advance\derccdim by\derquad

   {#2}\vldsauxx

   {#3}\vldsauxx

   {#4}%

   \setbox\derboxone=\hbox{\unhbox\derboxtwo\unhbox\derboxone}%

   \advance\derccdim by\derldim

   \advance\derccdim by\dercdim

           \dercrdim  =\derrdim}%

\newcommand{\vliiiin}[7]{\vldsiiiiaux{#4}{#5}{#6}{#7}\vldsinaux{#1}{#2}{#3}}%

\newcommand{\vliiiid}[7]{\vldsiiiiaux{#4}{#5}{#6}{#7}\vldsidaux{#1}{#2}{#3}}%

\newcommand{\vliiiiq}[7]{\vldsiiiiaux{#4}{#5}{#6}{#7}\vldsiqaux{#1}{#2}{#3}}%

\newcommand{\vldsiiiiiaux}[5]{\derquad=\fontdimen6\textfont2%

   {#1}%

           \dercldim  =\derldim

           \derccdim  =\dercdim

   \setbox\derboxtwo=\hbox{\unhbox\derboxone\kern\derquad}%

   \advance\derccdim by\derrdim

   \advance\derccdim by\derquad

   {#2}\vldsauxx

   {#3}\vldsauxx

   {#4}\vldsauxx

   {#5}%

   \setbox\derboxone=\hbox{\unhbox\derboxtwo\unhbox\derboxone}%

   \advance\derccdim by\derldim

   \advance\derccdim by\dercdim

           \dercrdim  =\derrdim}%

\newcommand{\vliiiiin}[8]{\vldsiiiiiaux{#4}{#5}{#6}{#7}{#8}%

                          \vldsinaux{#1}{#2}{#3}}%

\newcommand{\vliiiiid}[8]{\vldsiiiiiaux{#4}{#5}{#6}{#7}{#8}%

                          \vldsidaux{#1}{#2}{#3}}%

\newcommand{\vliiiiiq}[8]{\vldsiiiiiaux{#4}{#5}{#6}{#7}{#8}%

                          \vldsiqaux{#1}{#2}{#3}}%

\newcommand{\vldsiiiiiiaux}[6]{\derquad=\fontdimen6\textfont2%

   {#1}%

           \dercldim  =\derldim

           \derccdim  =\dercdim

   \setbox\derboxtwo=\hbox{\unhbox\derboxone\kern\derquad}%

   \advance\derccdim by\derrdim

   \advance\derccdim by\derquad

   {#2}\vldsauxx

   {#3}\vldsauxx

   {#4}\vldsauxx

   {#5}\vldsauxx

   {#6}%

   \setbox\derboxone=\hbox{\unhbox\derboxtwo\unhbox\derboxone}%

   \advance\derccdim by\derldim

   \advance\derccdim by\dercdim

           \dercrdim  =\derrdim}%

\newcommand{\vliiiiiin}[9]{\vldsiiiiiiaux{#4}{#5}{#6}{#7}{#8}{#9}%

                           \vldsinaux{#1}{#2}{#3}}%

\newcommand{\vliiiiiid}[9]{\vldsiiiiiiaux{#4}{#5}{#6}{#7}{#8}{#9}%

                           \vldsidaux{#1}{#2}{#3}}%

\newcommand{\vliiiiiiq}[9]{\vldsiiiiiiaux{#4}{#5}{#6}{#7}{#8}{#9}%

                           \vldsiqaux{#1}{#2}{#3}}%

\newcommand{\vlinfaux     }[4]{\vlderivationaux{\vlin  {#1}{#2}{#3}%

                                                                {\vlhy{#4}}}}%

\newcommand{\vliqfaux     }[4]{\vlderivationaux{\vliq  {#1}{#2}{#3}%

                                                                {\vlhy{#4}}}}%

\newcommand{\vlindaux     }[4]{\vlderivationaux{\vlid  {#1}{#2}{#3}%

                                                                {\vlhy{#4}}}}%

\newcommand{\vliinfaux    }[5]{\vlderivationaux{\vliin {#1}{#2}{#3}%

                                                                {\vlhy{#4}}%

                                                                {\vlhy{#5}}}}%

\newcommand{\vliidfaux    }[5]{\vlderivationaux{\vliid {#1}{#2}{#3}%

                                                                {\vlhy{#4}}%

                                                                {\vlhy{#5}}}}%

\newcommand{\vliiqfaux    }[5]{\vlderivationaux{\vliiq {#1}{#2}{#3}%

                                                                {\vlhy{#4}}%

                                                                {\vlhy{#5}}}}%

\newcommand{\vliiinfaux   }[6]{\vlderivationaux{\vliiin{#1}{#2}{#3}%

                                                                {\vlhy{#4}}%

                                                                {\vlhy{#5}}%

                                                                {\vlhy{#6}}}}%

\newcommand{\vliiidfaux   }[6]{\vlderivationaux{\vliiid{#1}{#2}{#3}%

                                                                {\vlhy{#4}}%

                                                                {\vlhy{#5}}%

                                                                {\vlhy{#6}}}}%

\newcommand{\vliiiqfaux   }[6]{\vlderivationaux{\vliiiq{#1}{#2}{#3}%

                                                                {\vlhy{#4}}%

                                                                {\vlhy{#5}}%

                                                                {\vlhy{#6}}}}%

\newcommand{\vliiiinfaux  }[7]{\vlderivationaux{\vliiiin{#1}{#2}{#3}%

                                                                {\vlhy{#4}}%

                                                                {\vlhy{#5}}%

                                                                {\vlhy{#6}}%

                                                                {\vlhy{#7}}}}%

\newcommand{\vliiiidfaux  }[7]{\vlderivationaux{\vliiiid{#1}{#2}{#3}%

                                                                {\vlhy{#4}}%

                                                                {\vlhy{#5}}%

                                                                {\vlhy{#6}}%

                                                                {\vlhy{#7}}}}%

\newcommand{\vliiiiqfaux  }[7]{\vlderivationaux{\vliiiiq{#1}{#2}{#3}%

                                                                {\vlhy{#4}}%

                                                                {\vlhy{#5}}%

                                                                {\vlhy{#6}}%

                                                                {\vlhy{#7}}}}%

\newcommand{\vliiiiinfaux }[8]{\vlderivationaux{\vliiiiin{#1}{#2}{#3}%

                                                                {\vlhy{#4}}%

                                                                {\vlhy{#5}}%

                                                                {\vlhy{#6}}%

                                                                {\vlhy{#7}}%

                                                                {\vlhy{#8}}}}%

\newcommand{\vliiiiidfaux }[8]{\vlderivationaux{\vliiiiid{#1}{#2}{#3}%

                                                                {\vlhy{#4}}%

                                                                {\vlhy{#5}}%

                                                                {\vlhy{#6}}%

                                                                {\vlhy{#7}}%

                                                                {\vlhy{#8}}}}%

\newcommand{\vliiiiiqfaux }[8]{\vlderivationaux{\vliiiiiq{#1}{#2}{#3}%

                                                                {\vlhy{#4}}%

                                                                {\vlhy{#5}}%

                                                                {\vlhy{#6}}%

                                                                {\vlhy{#7}}%

                                                                {\vlhy{#8}}}}%

\newcommand{\vliiiiiinfaux}[9]{\vlderivationaux{\vliiiiiin{#1}{#2}{#3}%

                                                                {\vlhy{#4}}%

                                                                {\vlhy{#5}}%

                                                                {\vlhy{#6}}%

                                                                {\vlhy{#7}}%

                                                                {\vlhy{#8}}%

                                                                {\vlhy{#9}}}}%

\newcommand{\vliiiiiidfaux}[9]{\vlderivationaux{\vliiiiiid{#1}{#2}{#3}%

                                                                {\vlhy{#4}}%

                                                                {\vlhy{#5}}%

                                                                {\vlhy{#6}}%

                                                                {\vlhy{#7}}%

                                                                {\vlhy{#8}}%

                                                                {\vlhy{#9}}}}%

\newcommand{\vliiiiiiqfaux}[9]{\vlderivationaux{\vliiiiiiq{#1}{#2}{#3}%

                                                                {\vlhy{#4}}%

                                                                {\vlhy{#5}}%

                                                                {\vlhy{#6}}%

                                                                {\vlhy{#7}}%

                                                                {\vlhy{#8}}%

                                                                {\vlhy{#9}}}}%

\newcommand{\vlinf     }{\vlderivationinit\vlinfaux     }%

\newcommand{\vlidf     }{\vlderivationinit\vlindaux     }%

\newcommand{\vliqf     }{\vlderivationinit\vliqfaux     }%

\newcommand{\vliinf    }{\vlderivationinit\vliinfaux    }%

\newcommand{\vliidf    }{\vlderivationinit\vliidfaux    }%

\newcommand{\vliiqf    }{\vlderivationinit\vliiqfaux    }%

\newcommand{\vliiinf   }{\vlderivationinit\vliiinfaux   }%

\newcommand{\vliiidf   }{\vlderivationinit\vliiidfaux   }%

\newcommand{\vliiiqf   }{\vlderivationinit\vliiiqfaux   }%

\newcommand{\vliiiinf  }{\vlderivationinit\vliiiinfaux  }%

\newcommand{\vliiiidf  }{\vlderivationinit\vliiiidfaux  }%

\newcommand{\vliiiiqf  }{\vlderivationinit\vliiiiqfaux  }%

\newcommand{\vliiiiinf }{\vlderivationinit\vliiiiinfaux }%

\newcommand{\vliiiiidf }{\vlderivationinit\vliiiiidfaux }%

\newcommand{\vliiiiiqf }{\vlderivationinit\vliiiiiqfaux }%

\newcommand{\vliiiiiinf}{\vlderivationinit\vliiiiiinfaux}%

\newcommand{\vliiiiiidf}{\vlderivationinit\vliiiiiidfaux}%

\newcommand{\vliiiiiiqf}{\vlderivationinit\vliiiiiiqfaux}%

\catcode`@=12

\newcommand{\vltrauxx}[5]{\vldaux

   {#1}%

   {#2}%

   {\vlhy{#3}}%

   {}%

   {\hbox{$\vcenter{\xy

          0;<\hsize,0pt>:<0pt,#4\hsize>::

          (-0.5,0.5);(0.5,0.5)**\crv{(0.1,0.6)&(-0.1,0.4)};

          (0,0)**@{-};(-0.5,0.5)**@{-};

          (0,0.273)*{\scriptstyle #5\strut}%

          \endxy}$}}%

   {\kern\deropen}}%

\catcode`\@=11

\newcommand{\vltraux}[3]{\vltrauxx{}{}{#2}{#3}{#1}}%

\newcount\vltrindc

\newdimen\vltrindd

\newcommand{\vltrlaux}[5]{\ifdim\derccdim>\dercdim\vldummycount=\derccdim

                             \else\vldummycount=\dercdim

                             \fi

                          \FPmul\vltrindc{\the\vldummycount}{0.25}%

                          \vltrindd=\vltrindc sp

                          \advance\vltrindd by-10pt%

   \vltrauxx{\scriptstyle #2\strut\kern-\vltrindd}%

            {\kern-\vltrindd\scriptstyle #3\strut}{#4}{#5}{#1}}%

\newcommand{\vltrauxxx}[2]{{#2}\vlstemaux\vldaux

   {}%

   {}%

   {\vlhy{#1}}%

   {\kern-\ht\strutbox\kern-\dp\strutbox}%

   {}%

   {}}%

\newcommand{\vltrf }[6]{\vltrauxxx{#2}%

                        {\vldsiiiaux{#3}{#4}{#5}\vltraux{#1}{}{#6}}}%

\newcommand{\vltrlf}[8]{\vltrauxxx{#4}%

                        {\vldsiiiaux{#5}{#6}{#7}\vltrlaux{#1}{#2}{#3}{}{#8}}}%

\newcommand{\vltr }[5]{\vltrf{#1}{#2}{#3}{#4}{#5}1}%

\newcommand{\vltrl}[7]{\vltrlf{#1}{#2}{#3}{#4}{#5}{#6}{#7}1}%

\newcommand{\vltreeder }[5]{\vlderivation{\vltr{#1}{#2}{\vlhy{#3}}%

                                                       {\vlhy{#4}}%

                                                       {\vlhy{#5}}}}%

\newcommand{\vltreederl}[7]{\vlderivation{\vltrl{#1}{#2}{#3}{#4}{\vlhy{#5}}%

                                                                {\vlhy{#6}}%

                                                                {\vlhy{#7}}}}%

\newcommand{\vlvdots}{\vbox to12pt{\vfil\hbox{$\smash\vdots$}}}%

%------------------------------------------------- END OF MACROS FOR DERIVATIONS

%----------------------------------------------------- MACROS FOR OPEN DEDUCTION

\newif\ifodframe          \odframetrue

\newif\ifodframefirst     \odframefirsttrue

\newif\ifodbackground     \odbackgroundfalse

\newif\ifodbackgroundfirst\odbackgroundfirsttrue

\newcount\odback

\newcount\odframe

\newcommand{\odboxed}[1]{%

   \ifnum\odback=0

      \ifnum\odframe=0

         \hbox{$\vcenter{%

         \vbox{\kern\fboxrule

         \hbox{\kern\fboxrule$#1$%

               \kern\fboxrule}%

               \kern\fboxrule}%

         }$}%

      \else

         \colorlet{currentcolor}{.}%

         {\color{currentcolor!\the\odframe}\fbox{\color{currentcolor}$#1$}}%

      \fi

   \else

      \colorlet{currentcolor}{.}%

      \fcolorbox{currentcolor!\the\odframe}{currentcolor!\the\odback}{$#1$}%

   \fi}%

\newcommand\odbox[1]{\odframe=100\setlength{\fboxsep}{2pt}%

                                 \setlength{\fboxrule}{.25pt}\odboxed{#1}}%

\newcommand{\odsetframes}{\ifodbackground\ifodbackgroundfirst

                                                   \odbackgroundfirstfalse

                                                   \odback =0%

                                                   \setlength{\fboxsep}{0pt}%

                                                   \odframe=0%

                                         \else\advance\odback by5%

                                              \odframe=\odback

                                              \ifodframe\odframe=100%

                                              \setlength{\fboxsep}{2pt}%

                                              \setlength{\fboxrule}{.25pt}%

                                              \fi

                                         \fi

                          \else\setlength{\fboxsep}{0pt}%

                          \fi

                          \ifodframe\ifodframefirst\odframefirstfalse

                                                   \odframe=0%

                                    \else          \odframe=100%

                                                   \setlength{\fboxsep}{2pt}%

                                                   \setlength{\fboxrule}{.25pt}%

                                    \fi

                          \else     \odframe=0%

                          \fi}%

\newcommand{\odderivationinit}{\bgroup

   \odsetframes

   \vlprepstructures\vlderivationinitaux}%                            % dr

\newcommand{\odderivationaux}[1]{#1\odboxed

                                 {\vcenter{\copy\derboxone}}\vlderivationterm}%

\newcommand{\od        }   {\odderivationinit\odderivationaux}%

\newcommand{\odp       }[3]{\vlpr{#1}{#3}{\vls #2}}%

\newcommand{\odP       }[3]{\vlpd{#1}{#3}{\vls #2}}%

\newcommand{\odpx      }[4]{\vlpf{#1}{#3}{\vls #2}{#4}}%

\newcommand{\odproofaux}[4]{\odderivationaux{\vlpf{#2}{#4}{\vls #3}{#1}}}%

\newcommand{\odr       }   {\odderivationinit\odproofaux1}%

\newcommand{\odR       }   {\odderivationinit\odproofaux2}%

\newcommand{\odd       }[4]{\vldf{#2}{#4}{\vls #3}{\vls #1}1}%

\newcommand{\odD       }[4]{\vldf{#2}{#4}{\vls #3}{\vls #1}2}%

\newcommand{\oddx      }[5]{\vldf{#2}{#4}{\vls #3}{\vls #1}{#5}}%

\newcommand{\odh       }[1]{\vlhy{\vls #1}}%

\newcommand{\odderaux  }[5]{\odderivationaux{\vldf{#3}{#5}{\vls #4}%

                                                    {\vlhy{\vls #2}}{#1}}}%

\newcommand{\odv       }   {\odderivationinit\odderaux1}%

\newcommand{\odV       }   {\odderivationinit\odderaux2}%

\newcommand{\odi       }[4]{\vlin{#2}{#4}{\vls #3}{\vls #1}}%

\newcommand{\odI       }[4]{\vliq{#2}{#4}{\vls #3}{\vls #1}}%

\newcommand{\odo       }[4]{\vlid{#2}{#4}{\vls #3}{\vls #1}}%

\newcommand{\odnaux    }[4]{\odderivationaux{\vlin{#2}{#4}{\vls #3}%

                                                    {\vlhy{\vls #1}}}}%

\newcommand{\odNaux    }[4]{\odderivationaux{\vliq{#2}{#4}{\vls #3}%

                                                    {\vlhy{\vls #1}}}}%

\newcommand{\odtaux    }[4]{\odderivationaux{\vlid{#2}{#4}{\vls #3}%

                                                    {\vlhy{\vls #1}}}}%

\newcommand{\odn       }   {\odderivationinit\odnaux}%

\newcommand{\odN       }   {\odderivationinit\odNaux}%

\newcommand{\odt       }   {\odderivationinit\odtaux}%

%---------------------------------------------- END OF MACROS FOR OPEN DEDUCTION

%------------------------------------------------------- MACROS FOR ATOMIC FLOWS

\catcode`@=12

\newdimen\afunitmst\afunitmst=0.01pt%

\newdimen\afelwidthmst

\newdimen\afelheightmst

\newdimen\afthickonemst

\newdimen\afthicktwomst

\newdimen\afthickthreemst

\newdimen\afthickfourmst

\newdimen\afthickfivemst

\newdimen\aflabeldistancemst

\newcommand{\afsetparamsmst}{%

\afelwidthmst      =425\afunitmst

\afelheightmst     =325\afunitmst

\afthickonemst     = 60\afunitmst

\afthicktwomst     = 40\afunitmst

\afthickthreemst   =160\afunitmst

\afthickfourmst    =120\afunitmst

\afthickfivemst    = 40\afunitmst

\aflabeldistancemst=220\afunitmst}%

\afsetparamsmst

\newdimen\afunit\afunit=0.01pt%

\newdimen\afelwidth

\newdimen\afelheight

\newdimen\afthickone

\newdimen\afthicktwo

\newdimen\afthickthree

\newdimen\afthickfour

\newdimen\afthickfive

\newdimen\aflabeldistance

\newdimen\afelwidthcur

\newdimen\afthickdouble

\newdimen\afthicksep

\newcommand{\afsetparams}{%

\afelwidth      =425\afunit

\afelheight     =325\afunit

\afthickone     = 60\afunit

\afthicktwo     = 40\afunit

\afthickthree   =160\afunit

\afthickfour    =120\afunit

\afthickfive    = 40\afunit

\aflabeldistance=220\afunit

\afthicksep     =  3\afelwidth\divide\afthicksep by10%

                             \advance\afthicksep by-\afthickfive

\afthickdouble  =\afthicksep

                 \advance\afthickdouble by2\afthickfive

\afelwidthcur   =\afelwidth}%

\afsetparams

\newbox\aftrdnbox

\newbox\aftrupbox

\newbox\afdiskbox

\newbox\afbbdbox

\newbox\afbbubox

\newbox\afbdbox

\newbox\afbubox

\newbox\afcdcbox

\newbox\afcdcmbox

\newbox\afcucbox

\newbox\afcucmbox

\newbox\afcdabox\newbox\afwdabox\newbox\afadabox

\newbox\afCdbox\newbox\afWdbox\newbox\afAdbox

\newbox\afcdnbox\newbox\afwdnbox\newbox\afadnbox

\newbox\afCdnbox

\newbox\afcuabox\newbox\afwuabox\newbox\afauabox

\newbox\afCubox\newbox\afWubox\newbox\afAubox

\newbox\afcunbox\newbox\afwunbox\newbox\afaunbox

\newbox\afCunbox

\newbox\afIubox

\newbox\afiubox

\newbox\afIdbox

\newbox\afidbox

\newbox\afinubox\newbox\afindbox 

\newbox\afDubox

\newbox\afduabox

\newbox\afDdbox

\newbox\afddabox

\newbox\afddnbox

\newbox\afdunbox

\newbox\afCudbox

\newbox\afcudabox

\newbox\afCddbox

\newbox\afcddabox

\newbox\afCudnbox

\newbox\afcudnbox

\newbox\afCddnbox