\documentclass [fleqn]{article}

\setlength {\overfullrule }{1mm}

\usepackage{latexsym}

\setlength{\parindent}{0em}

\setlength{\parskip}{1ex}

\usepackage{graphicx}

\usepackage[dvipdfm=true]{hyperref}

\hypersetup{pdfpagemode=none}

\hypersetup{pdfstartpage=1}

\hypersetup{pdfstartview=FitBH}

\hypersetup{pdfpagescrop={120 130 490 730}}

\hypersetup{pdftitle=Logiweb dictionary of base}

\hypersetup{colorlinks=true}

\everymath{\rm}

\hyperbaseurl{http://www.diku.dk/cgi-bin/cginetd/grue/relay/go/01674B61AE95731A9E053A161BB72EB60438989941D88AEFC2F389A20806/2/dictionary/tex/page.tex}

\begin {document}\raggedright

\makebox [0mm][l]{\makebox [\linewidth ][r]{\includegraphics [0mm,18.5mm][16.5mm,19mm]{/home/disk07/grue/logiweb/20060417/html/logiweb/doc/logiweb.eps}}}%
{\bf {\Large Logiweb dictionary of $\rm 
\mbox{base}$}}

\vspace {12.5mm}

\href {../index.html}{Up}
\href {http://www.diku.dk/~grue/logiweb/20060417/logiweb/doc/browser/dictionary/index.html}{Help}


\newlength{\idlength}
\settowidth{\idlength}{609}
\newlength{\aritylength}
\settowidth{\aritylength}{99}
\vspace{2ex}
\makebox[\idlength][r]{0}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
\mbox{base}$

\makebox[\idlength][r]{1}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm 
[\ast
\bowtie\ast
]$

\makebox[\idlength][r]{2}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm 
\mbox{``}\ast
\mbox{''}$

\makebox[\idlength][r]{3}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm $

\makebox[\idlength][r]{4}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm \ast
\mathrel{\mathrm{,}}\ast$

\makebox[\idlength][r]{5}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{3}%
\makebox[0.5em]{}%
$\rm \ast
{[}\ast
{]}\ast$

\makebox[\idlength][r]{6}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm 
\mathbf{Preassociative}\,\ast
; \ast$

\makebox[\idlength][r]{7}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm 
\mathbf{Postassociative}\,\ast
; \ast$

\makebox[\idlength][r]{8}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm 
[\ast
] , \linebreak [0] \ast$

\makebox[\idlength][r]{9}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm 
\mathrm{priority} \,\ast
\, \mathrm{end}$

\makebox[\idlength][r]{10}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm 
\newline \ast$

\makebox[\idlength][r]{11}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
\ast $

\makebox[\idlength][r]{12}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm 
(\ast
)^{\bf t}$

\makebox[\idlength][r]{13}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm 
\mbox{string}(\ast
)+\ast$

\makebox[\idlength][r]{14}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm \mbox{string}(\ast
)\mathrel{++}\ast$

\makebox[\idlength][r]{15}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
\mathrm{pyk}$

\makebox[\idlength][r]{16}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{3}%
\makebox[0.5em]{}%
$\rm 
[\ast
\stackrel{\ast
}{\rightarrow}\ast
]$

\makebox[\idlength][r]{17}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm \ast
\mathrel{linebreak[4]} \ast$

\makebox[\idlength][r]{18}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm 
\mbox{bracket $\ast$ end bracket}$

\makebox[\idlength][r]{19}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm 
\mbox{big bracket $\ast$ end bracket}$

\makebox[\idlength][r]{20}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm 
\ \$\ast\$\linebreak[0]\ $

\makebox[\idlength][r]{21}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm 
\mathbf{flush\ left\ }[ \ast
]$

\makebox[\idlength][r]{22}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
\mathsf{x}$

\makebox[\idlength][r]{23}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
\mathsf{y}$

\makebox[\idlength][r]{24}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
\mathsf{z}$

\makebox[\idlength][r]{25}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
\mathrm{tex}$

\makebox[\idlength][r]{26}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
\mathrm{name}$

\makebox[\idlength][r]{27}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
\mathrm{prio}$

\makebox[\idlength][r]{28}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
\mathsf {T}$

\makebox[\idlength][r]{29}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{3}%
\makebox[0.5em]{}%
$\rm 
\mathrm {if}(\ast
,\linebreak [0]\ast
,\linebreak [0]\ast
)$

\makebox[\idlength][r]{30}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{3}%
\makebox[0.5em]{}%
$\rm 
[\ast
\stackrel {\ast
}{\Rightarrow }\ast
]$

\makebox[\idlength][r]{31}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
\mathrm {val}$

\makebox[\idlength][r]{32}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm 
\linebreak [0]\ \hskip0em plus2.0em{}\ast$

\makebox[\idlength][r]{33}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm !\ast$

\makebox[\idlength][r]{34}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm 
\mbox {\tt \char34}\ast$

\makebox[\idlength][r]{35}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm 
\#\ast$

\makebox[\idlength][r]{36}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm 
\$\ast$

\makebox[\idlength][r]{37}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm 
\%\ast$

\makebox[\idlength][r]{38}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm 
\&\ast$

\makebox[\idlength][r]{39}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm 
\mbox {'}\ast$

\makebox[\idlength][r]{40}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm (\ast$

\makebox[\idlength][r]{41}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm )\ast$

\makebox[\idlength][r]{42}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm 
{*}\ast$

\makebox[\idlength][r]{43}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm 
{+}\ast$

\makebox[\idlength][r]{44}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm ,\ast$

\makebox[\idlength][r]{45}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm 
\mbox{-}\ast$

\makebox[\idlength][r]{46}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm .\ast$

\makebox[\idlength][r]{47}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm /\ast$

\makebox[\idlength][r]{48}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm 0\ast$

\makebox[\idlength][r]{49}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm 1\ast$

\makebox[\idlength][r]{50}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm 2\ast$

\makebox[\idlength][r]{51}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm 3\ast$

\makebox[\idlength][r]{52}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm 4\ast$

\makebox[\idlength][r]{53}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm 5\ast$

\makebox[\idlength][r]{54}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm 6\ast$

\makebox[\idlength][r]{55}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm 7\ast$

\makebox[\idlength][r]{56}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm 8\ast$

\makebox[\idlength][r]{57}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm 9\ast$

\makebox[\idlength][r]{58}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm 
{:}\ast$

\makebox[\idlength][r]{59}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm ;\ast$

\makebox[\idlength][r]{60}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm 
{<}\ast$

\makebox[\idlength][r]{61}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm 
{=}\ast$

\makebox[\idlength][r]{62}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm 
{>}\ast$

\makebox[\idlength][r]{63}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm ?\ast$

\makebox[\idlength][r]{64}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm @\ast$

\makebox[\idlength][r]{65}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm A\ast$

\makebox[\idlength][r]{66}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm B\ast$

\makebox[\idlength][r]{67}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm C\ast$

\makebox[\idlength][r]{68}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm D\ast$

\makebox[\idlength][r]{69}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm E\ast$

\makebox[\idlength][r]{70}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm F\ast$

\makebox[\idlength][r]{71}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm G\ast$

\makebox[\idlength][r]{72}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm H\ast$

\makebox[\idlength][r]{73}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm I\ast$

\makebox[\idlength][r]{74}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm J\ast$

\makebox[\idlength][r]{75}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm K\ast$

\makebox[\idlength][r]{76}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm L\ast$

\makebox[\idlength][r]{77}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm M\ast$

\makebox[\idlength][r]{78}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm N\ast$

\makebox[\idlength][r]{79}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm O\ast$

\makebox[\idlength][r]{80}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm P\ast$

\makebox[\idlength][r]{81}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm Q\ast$

\makebox[\idlength][r]{82}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm R\ast$

\makebox[\idlength][r]{83}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm S\ast$

\makebox[\idlength][r]{84}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm T\ast$

\makebox[\idlength][r]{85}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm U\ast$

\makebox[\idlength][r]{86}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm V\ast$

\makebox[\idlength][r]{87}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm W\ast$

\makebox[\idlength][r]{88}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm X\ast$

\makebox[\idlength][r]{89}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm Y\ast$

\makebox[\idlength][r]{90}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm Z\ast$

\makebox[\idlength][r]{91}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm [\ast$

\makebox[\idlength][r]{92}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm 
\mbox {$\backslash $}\ast$

\makebox[\idlength][r]{93}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm ]\ast$

\makebox[\idlength][r]{94}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm 
{\char94}\ast$

\makebox[\idlength][r]{95}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm 
\_\ast$

\makebox[\idlength][r]{96}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm 
\mbox {`}\ast$

\makebox[\idlength][r]{97}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm a\ast$

\makebox[\idlength][r]{98}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm b\ast$

\makebox[\idlength][r]{99}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm c\ast$

\makebox[\idlength][r]{100}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm d\ast$

\makebox[\idlength][r]{101}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm e\ast$

\makebox[\idlength][r]{102}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm f\ast$

\makebox[\idlength][r]{103}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm g\ast$

\makebox[\idlength][r]{104}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm h\ast$

\makebox[\idlength][r]{105}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm i\ast$

\makebox[\idlength][r]{106}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm j\ast$

\makebox[\idlength][r]{107}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm k\ast$

\makebox[\idlength][r]{108}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm l\ast$

\makebox[\idlength][r]{109}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm m\ast$

\makebox[\idlength][r]{110}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm n\ast$

\makebox[\idlength][r]{111}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm o\ast$

\makebox[\idlength][r]{112}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm p\ast$

\makebox[\idlength][r]{113}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm q\ast$

\makebox[\idlength][r]{114}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm r\ast$

\makebox[\idlength][r]{115}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm s\ast$

\makebox[\idlength][r]{116}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm t\ast$

\makebox[\idlength][r]{117}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm u\ast$

\makebox[\idlength][r]{118}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm v\ast$

\makebox[\idlength][r]{119}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm w\ast$

\makebox[\idlength][r]{120}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm x\ast$

\makebox[\idlength][r]{121}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm y\ast$

\makebox[\idlength][r]{122}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm z\ast$

\makebox[\idlength][r]{123}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm 
\{\ast$

\makebox[\idlength][r]{124}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm |\ast$

\makebox[\idlength][r]{125}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm 
\}\ast$

\makebox[\idlength][r]{126}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm 
\char126 \ast$

\makebox[\idlength][r]{127}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
\mathrm {claim}$

\makebox[\idlength][r]{128}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
\bot $

\makebox[\idlength][r]{129}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm 
f(\ast
)$

\makebox[\idlength][r]{130}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm 
(\ast
){}^{I} $

\makebox[\idlength][r]{131}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
\mathsf {F}$

\makebox[\idlength][r]{132}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
\underline {0}$

\makebox[\idlength][r]{133}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
\underline {1}$

\makebox[\idlength][r]{134}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
\underline {2}$

\makebox[\idlength][r]{135}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
\underline {3}$

\makebox[\idlength][r]{136}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
\underline {4}$

\makebox[\idlength][r]{137}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
\underline {5}$

\makebox[\idlength][r]{138}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
\underline {6}$

\makebox[\idlength][r]{139}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
\underline {7}$

\makebox[\idlength][r]{140}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
\underline {8}$

\makebox[\idlength][r]{141}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
\underline {9}$

\makebox[\idlength][r]{142}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
0$

\makebox[\idlength][r]{143}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
1$

\makebox[\idlength][r]{144}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
2$

\makebox[\idlength][r]{145}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
3$

\makebox[\idlength][r]{146}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
4$

\makebox[\idlength][r]{147}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
5$

\makebox[\idlength][r]{148}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
6$

\makebox[\idlength][r]{149}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
7$

\makebox[\idlength][r]{150}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
8$

\makebox[\idlength][r]{151}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
9$

\makebox[\idlength][r]{152}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
\mathsf {a}$

\makebox[\idlength][r]{153}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
\mathsf {b}$

\makebox[\idlength][r]{154}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
\mathsf {c}$

\makebox[\idlength][r]{155}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
\mathsf {d}$

\makebox[\idlength][r]{156}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
\mathsf {e}$

\makebox[\idlength][r]{157}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
\mathsf {f}$

\makebox[\idlength][r]{158}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
\mathsf {g}$

\makebox[\idlength][r]{159}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
\mathsf {h}$

\makebox[\idlength][r]{160}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
\mathsf {i}$

\makebox[\idlength][r]{161}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
\mathsf {j}$

\makebox[\idlength][r]{162}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
\mathsf {k}$

\makebox[\idlength][r]{163}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
\mathsf {l}$

\makebox[\idlength][r]{164}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
\mathsf {m}$

\makebox[\idlength][r]{165}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
\mathsf {n}$

\makebox[\idlength][r]{166}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
\mathsf {o}$

\makebox[\idlength][r]{167}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
\mathsf {p}$

\makebox[\idlength][r]{168}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
\mathsf {q}$

\makebox[\idlength][r]{169}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
\mathsf {r}$

\makebox[\idlength][r]{170}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
\mathsf {s}$

\makebox[\idlength][r]{171}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
\mathsf {t}$

\makebox[\idlength][r]{172}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
\mathsf {u}$

\makebox[\idlength][r]{173}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
\mathsf {v}$

\makebox[\idlength][r]{174}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
\mathsf {w}$

\makebox[\idlength][r]{175}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm 
(\ast
)^M$

\makebox[\idlength][r]{176}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{3}%
\makebox[0.5em]{}%
$\rm 
\mathrm {If}(\ast
,\linebreak [0]\ast
,\linebreak [0]\ast
)$

\makebox[\idlength][r]{177}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm \mathrm {array}\{\ast
\}\ast
\mathrm {end\ array}$

\makebox[\idlength][r]{178}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
l$

\makebox[\idlength][r]{179}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
c$

\makebox[\idlength][r]{180}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
r$

\makebox[\idlength][r]{181}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
\mathrm {empty}$

\makebox[\idlength][r]{182}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{3}%
\makebox[0.5em]{}%
$\rm 
\langle \ast
\,{|}\ast
{:=}\,\ast
\rangle $

\makebox[\idlength][r]{183}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm 
{\cal M}(\ast
)$

\makebox[\idlength][r]{184}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm 
\tilde {{\cal U}}(\ast
)$

\makebox[\idlength][r]{185}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm 
{\cal U}(\ast
)$

\makebox[\idlength][r]{186}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm 
{\cal U}^M(\ast
)$

\makebox[\idlength][r]{187}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm 
\mathbf {apply}(\ast
,\ast
)$

\makebox[\idlength][r]{188}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm 
\mathbf {apply}_1(\ast
,\ast
)$

\makebox[\idlength][r]{189}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm 
identifier( \ast
)$

\makebox[\idlength][r]{190}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm 
identifier_{1}( \ast
, \ast
)$

\makebox[\idlength][r]{191}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm 
array\mbox{-}\linebreak[0]plus( \ast
, \ast
)$

\makebox[\idlength][r]{192}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{3}%
\makebox[0.5em]{}%
$\rm 
array\mbox{-}\linebreak[0]remove( \ast
, \ast
, \ast
)$

\makebox[\idlength][r]{193}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{4}%
\makebox[0.5em]{}%
$\rm 
array\mbox{-}\linebreak[0]put( \ast
, \ast
, \ast
, \ast
)$

\makebox[\idlength][r]{194}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{5}%
\makebox[0.5em]{}%
$\rm 
array\mbox{-}\linebreak[0]add( \ast
, \ast
, \ast
, \ast
, \ast
)$

\makebox[\idlength][r]{195}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm 
bit( \ast
, \ast
)$

\makebox[\idlength][r]{196}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm 
bit_1( \ast
, \ast
)$

\makebox[\idlength][r]{197}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
rack$

\makebox[\idlength][r]{198}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
\mbox {\tt \char34}\mathrm {vector}\mbox {\tt \char34}$

\makebox[\idlength][r]{199}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
\mbox {\tt \char34}\mathrm {bibliography}\mbox {\tt \char34}$

\makebox[\idlength][r]{200}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
\mbox {\tt \char34}\mathrm {dictionary}\mbox {\tt \char34}$

\makebox[\idlength][r]{201}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
\mbox {\tt \char34}\mathrm {body}\mbox {\tt \char34}$

\makebox[\idlength][r]{202}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
\mbox {\tt \char34}\mathrm {codex}\mbox {\tt \char34}$

\makebox[\idlength][r]{203}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
\mbox {\tt \char34}\mathrm {expansion}\mbox {\tt \char34}$

\makebox[\idlength][r]{204}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
\mbox {\tt \char34}\mathrm {code}\mbox {\tt \char34}$

\makebox[\idlength][r]{205}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
\mbox {\tt \char34}\mathrm {cache}\mbox {\tt \char34}$

\makebox[\idlength][r]{206}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
\mbox {\tt \char34}\mathrm {diagnose}\mbox {\tt \char34}$

\makebox[\idlength][r]{207}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
\mbox {\tt \char34}\mathrm {pyk}\mbox {\tt \char34}$

\makebox[\idlength][r]{208}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
\mbox {\tt \char34}\mathrm {tex}\mbox {\tt \char34}$

\makebox[\idlength][r]{209}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
\mbox {\tt \char34}\mathrm {texname}\mbox {\tt \char34}$

\makebox[\idlength][r]{210}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
\mbox {\tt \char34}\mathrm {value}\mbox {\tt \char34}$

\makebox[\idlength][r]{211}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
\mbox {\tt \char34}\mathrm {message}\mbox {\tt \char34}$

\makebox[\idlength][r]{212}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
\mbox {\tt \char34}\mathrm {macro}\mbox {\tt \char34}$

\makebox[\idlength][r]{213}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
\mbox {\tt \char34}\mathrm {definition}\mbox {\tt \char34}$

\makebox[\idlength][r]{214}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
\mbox {\tt \char34}\mathrm {unpack}\mbox {\tt \char34}$

\makebox[\idlength][r]{215}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
\mbox {\tt \char34}\mathrm {claim}\mbox {\tt \char34}$

\makebox[\idlength][r]{216}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
\mbox {\tt \char34}\mathrm {priority}\mbox {\tt \char34}$

\makebox[\idlength][r]{217}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
\mbox {\tt \char34}\mathrm {lambda}\mbox {\tt \char34}$

\makebox[\idlength][r]{218}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
\mbox {\tt \char34}\mathrm {apply}\mbox {\tt \char34}$

\makebox[\idlength][r]{219}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
\mbox {\tt \char34}\mathrm {true}\mbox {\tt \char34}$

\makebox[\idlength][r]{220}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
\mbox {\tt \char34}\mathrm {if}\mbox {\tt \char34}$

\makebox[\idlength][r]{221}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
\mbox {\tt \char34}\mathrm {quote}\mbox {\tt \char34}$

\makebox[\idlength][r]{222}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
\mbox {\tt \char34}\mathrm {proclaim}\mbox {\tt \char34}$

\makebox[\idlength][r]{223}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
\mbox {\tt \char34}\mathrm {define}\mbox {\tt \char34}$

\makebox[\idlength][r]{224}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
\mbox {\tt \char34}\mathrm {introduce}\mbox {\tt \char34}$

\makebox[\idlength][r]{225}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
\mbox {\tt \char34}\mathrm {hide}\mbox {\tt \char34}$

\makebox[\idlength][r]{226}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
\mbox {\tt \char34}\mathrm {pre}\mbox {\tt \char34}$

\makebox[\idlength][r]{227}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
\mbox {\tt \char34}\mathrm {post}\mbox {\tt \char34}$

\makebox[\idlength][r]{228}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{3}%
\makebox[0.5em]{}%
$\rm 
{\cal E}(\ast
,\ast
,\ast
)$

\makebox[\idlength][r]{229}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{5}%
\makebox[0.5em]{}%
$\rm 
{\cal E}_2(\ast
,\ast
,\ast
,\ast
,\ast
)$

\makebox[\idlength][r]{230}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{4}%
\makebox[0.5em]{}%
$\rm 
{\cal E}_3(\ast
,\ast
,\ast
,\ast
)$

\makebox[\idlength][r]{231}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{4}%
\makebox[0.5em]{}%
$\rm 
{\cal E}_4(\ast
,\ast
,\ast
,\ast
)$

\makebox[\idlength][r]{232}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{3}%
\makebox[0.5em]{}%
$\rm 
\mathbf {lookup}(\ast
,\ast
,\ast
)$

\makebox[\idlength][r]{233}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{4}%
\makebox[0.5em]{}%
$\rm 
\mathbf {abstract}(\ast
,\ast
,\ast
,\ast
)$

\makebox[\idlength][r]{234}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm 
\lceil \ast
\rceil $

\makebox[\idlength][r]{235}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{3}%
\makebox[0.5em]{}%
$\rm 
{\cal M}(\ast
,\ast
,\ast
)$

\makebox[\idlength][r]{236}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{4}%
\makebox[0.5em]{}%
$\rm 
{\cal M}_2(\ast
,\ast
,\ast
,\ast
)$

\makebox[\idlength][r]{237}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{3}%
\makebox[0.5em]{}%
$\rm 
{\cal M}^*(\ast
,\ast
,\ast
)$

\makebox[\idlength][r]{238}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
\mathrm {macro}$

\makebox[\idlength][r]{239}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
s_0$

\makebox[\idlength][r]{240}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm 
\mathbf {zip}(\ast
,\ast
)$

\makebox[\idlength][r]{241}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{3}%
\makebox[0.5em]{}%
$\rm 
\mathbf {assoc}_1(\ast
,\ast
,\ast
)$

\makebox[\idlength][r]{242}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm (\ast
)^{\mathbf {p}}$

\makebox[\idlength][r]{243}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
\mbox{self}$

\makebox[\idlength][r]{244}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm 
[\ast
\mathrel {\ddot {=}}\ast
]$

\makebox[\idlength][r]{245}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm 
[\ast
\mathrel {\dot {=}}\ast
]$

\makebox[\idlength][r]{246}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm 
[\ast
\mathrel {\acute {=}}\ast
]$

\makebox[\idlength][r]{247}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm 
[\ast
\stackrel {\mathrm {pyk}}{=} \ast
]$

\makebox[\idlength][r]{248}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm 
[\ast
\stackrel {\mathrm {tex}}{=} \ast
]$

\makebox[\idlength][r]{249}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm 
[\ast
\stackrel {\mathrm {name}}{=} \ast
]$

\makebox[\idlength][r]{250}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm 
\mathbf{Priority\ table} [ \ast
]$

\makebox[\idlength][r]{251}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
\tilde {{\cal M}}_1$

\makebox[\idlength][r]{252}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm 
\tilde {{\cal M}}_2(\ast
)$

\makebox[\idlength][r]{253}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm 
\tilde {{\cal M}}_3(\ast
)$

\makebox[\idlength][r]{254}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{4}%
\makebox[0.5em]{}%
$\rm 
\tilde {{\cal M}}_4(\ast
,\ast
,\ast
,\ast
)$

\makebox[\idlength][r]{255}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{3}%
\makebox[0.5em]{}%
$\rm 
\tilde {{\cal M}}(\ast
,\ast
,\ast
)$

\makebox[\idlength][r]{256}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{3}%
\makebox[0.5em]{}%
$\rm 
\tilde {{\cal Q}}(\ast
,\ast
,\ast
)$

\makebox[\idlength][r]{257}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{3}%
\makebox[0.5em]{}%
$\rm 
\tilde {{\cal Q}}_2(\ast
,\ast
,\ast
)$

\makebox[\idlength][r]{258}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{4}%
\makebox[0.5em]{}%
$\rm 
\tilde {{\cal Q}}_3(\ast
,\ast
,\ast
,\ast
)$

\makebox[\idlength][r]{259}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{3}%
\makebox[0.5em]{}%
$\rm 
\tilde {{\cal Q}}^*(\ast
,\ast
,\ast
)$

\makebox[\idlength][r]{260}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm 
(\ast
)$

\makebox[\idlength][r]{261}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm 
\left( \ast
\right) $

\makebox[\idlength][r]{262}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm 
display(\ast
)$

\makebox[\idlength][r]{263}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm 
statement(\ast
)$

\makebox[\idlength][r]{264}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm 
[\ast
]^{\cdot}$

\makebox[\idlength][r]{265}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm 
[\ast
]^-$

\makebox[\idlength][r]{266}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm 
\mathbf{aspect}( \ast
, \ast
)$

\makebox[\idlength][r]{267}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{3}%
\makebox[0.5em]{}%
$\rm 
\mathbf{aspect}( \ast
, \ast
, \ast
)$

\makebox[\idlength][r]{268}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm 
\langle \ast
\rangle $

\makebox[\idlength][r]{269}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm 
\mathbf {tuple}_1( \ast
) $

\makebox[\idlength][r]{270}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm 
\mathbf {tuple}_2( \ast
) $

\makebox[\idlength][r]{271}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm 
let_2( \ast
, \ast
)$

\makebox[\idlength][r]{272}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm 
let_1( \ast
, \ast
)$

\makebox[\idlength][r]{273}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm 
[\ast
\stackrel {claim}{=}\ast
]$

\makebox[\idlength][r]{274}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
\mbox{checker}$

\makebox[\idlength][r]{275}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm 
\mathbf{check}( \ast
, \ast
)$

\makebox[\idlength][r]{276}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{3}%
\makebox[0.5em]{}%
$\rm 
\mathbf{check}_2( \ast
, \ast
, \ast
)$

\makebox[\idlength][r]{277}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{3}%
\makebox[0.5em]{}%
$\rm 
\mathbf{check}_3( \ast
, \ast
, \ast
)$

\makebox[\idlength][r]{278}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm 
\mathbf{check}^*( \ast
, \ast
)$

\makebox[\idlength][r]{279}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{3}%
\makebox[0.5em]{}%
$\rm 
\mathbf{check}^*_2( \ast
, \ast
, \ast
)$

\makebox[\idlength][r]{280}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm 
\relax [ \ast
\relax ]^{\cdot} $

\makebox[\idlength][r]{281}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm 
\relax [ \ast
\relax ]^{-} $

\makebox[\idlength][r]{282}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm 
\relax [ \ast
\relax ]^{\circ} $

\makebox[\idlength][r]{283}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
msg$

\makebox[\idlength][r]{284}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm 
[\ast
\stackrel {msg}{=} \ast
]$

\makebox[\idlength][r]{285}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
{<}stmt{>}$

\makebox[\idlength][r]{286}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
stmt$

\makebox[\idlength][r]{287}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm 
[\ast
\stackrel {stmt}{=}\ast
]$

\makebox[\idlength][r]{288}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
HeadNil'$

\makebox[\idlength][r]{289}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
HeadPair'$

\makebox[\idlength][r]{290}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
Transitivity'$

\makebox[\idlength][r]{291}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
{\makebox [0mm][l]{$\bot $}\,{\bot }}$

\makebox[\idlength][r]{292}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
Contra'$

\makebox[\idlength][r]{293}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
T'_{E}$

\makebox[\idlength][r]{294}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
L_{1}$

\makebox[\idlength][r]{295}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm \underline{\ast}$

\makebox[\idlength][r]{296}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm {\cal A}$

\makebox[\idlength][r]{297}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm {\cal B}$

\makebox[\idlength][r]{298}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm {\cal C}$

\makebox[\idlength][r]{299}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm {\cal D}$

\makebox[\idlength][r]{300}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm {\cal E}$

\makebox[\idlength][r]{301}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm {\cal F}$

\makebox[\idlength][r]{302}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm {\cal G}$

\makebox[\idlength][r]{303}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm {\cal H}$

\makebox[\idlength][r]{304}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm {\cal I}$

\makebox[\idlength][r]{305}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm {\cal J}$

\makebox[\idlength][r]{306}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm {\cal K}$

\makebox[\idlength][r]{307}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm {\cal L}$

\makebox[\idlength][r]{308}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm {\cal M}$

\makebox[\idlength][r]{309}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm {\cal N}$

\makebox[\idlength][r]{310}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm {\cal O}$

\makebox[\idlength][r]{311}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm {\cal P}$

\makebox[\idlength][r]{312}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm {\cal Q}$

\makebox[\idlength][r]{313}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm {\cal R}$

\makebox[\idlength][r]{314}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm {\cal S}$

\makebox[\idlength][r]{315}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm {\cal T}$

\makebox[\idlength][r]{316}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm {\cal U}$

\makebox[\idlength][r]{317}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm {\cal V}$

\makebox[\idlength][r]{318}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm {\cal W}$

\makebox[\idlength][r]{319}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm {\cal X}$

\makebox[\idlength][r]{320}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm {\cal Y}$

\makebox[\idlength][r]{321}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm {\cal Z}$

\makebox[\idlength][r]{322}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{3}%
\makebox[0.5em]{}%
$\rm 
\langle \ast
\,{\protect\vert}\ast
{:=}\,\ast
\rangle $

\makebox[\idlength][r]{323}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{3}%
\makebox[0.5em]{}%
$\rm 
\langle ^ { \ast } \ast
\,{\protect\vert}\ast
{:=}\,\ast
\rangle $

\makebox[\idlength][r]{324}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
\emptyset $

\makebox[\idlength][r]{325}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
Remainder$

\makebox[\idlength][r]{326}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm 
( \ast
)^{\bf v}$

\makebox[\idlength][r]{327}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{4}%
\makebox[0.5em]{}%
$\rm 
intro(\ast
,\ast
,\ast
,\ast
)$

\makebox[\idlength][r]{328}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{3}%
\makebox[0.5em]{}%
$\rm 
intro(\ast
,\ast
,\ast
)$

\makebox[\idlength][r]{329}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm 
error(\ast
,\ast
)$

\makebox[\idlength][r]{330}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm 
error_{2}(\ast
,\ast
)$

\makebox[\idlength][r]{331}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{3}%
\makebox[0.5em]{}%
$\rm 
proof( \ast
, \ast
, \ast
)$

\makebox[\idlength][r]{332}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm 
proof_{2}( \ast
, \ast
)$

\makebox[\idlength][r]{333}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm 
{\cal S}(\ast
, \ast
)$

\makebox[\idlength][r]{334}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm 
{\cal S}^{I}(\ast
, \ast
)$

\makebox[\idlength][r]{335}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm 
{\cal S}^{\rhd}(\ast
, \ast
)$

\makebox[\idlength][r]{336}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{3}%
\makebox[0.5em]{}%
$\rm 
{\cal S}_{1}^{\rhd}(\ast
, \ast
, \ast
)$

\makebox[\idlength][r]{337}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm 
{\cal S}^{E}(\ast
, \ast
)$

\makebox[\idlength][r]{338}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{3}%
\makebox[0.5em]{}%
$\rm 
{\cal S}_{1}^{E}(\ast
, \ast
, \ast
)$

\makebox[\idlength][r]{339}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm 
{\cal S}^{+}(\ast
, \ast
)$

\makebox[\idlength][r]{340}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{3}%
\makebox[0.5em]{}%
$\rm 
{\cal S}_{1}^{+}(\ast
, \ast
, \ast
)$

\makebox[\idlength][r]{341}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm 
{\cal S}^{-}(\ast
, \ast
)$

\makebox[\idlength][r]{342}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{3}%
\makebox[0.5em]{}%
$\rm 
{\cal S}_{1}^{-}(\ast
, \ast
, \ast
)$

\makebox[\idlength][r]{343}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm 
{\cal S}^{\ast}(\ast
, \ast
)$

\makebox[\idlength][r]{344}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{3}%
\makebox[0.5em]{}%
$\rm 
{\cal S}_{1}^{\ast}(\ast
, \ast
, \ast
)$

\makebox[\idlength][r]{345}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{4}%
\makebox[0.5em]{}%
$\rm 
{\cal S}_{2}^{\ast}(\ast
, \ast
, \ast
, \ast
)$

\makebox[\idlength][r]{346}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm 
{\cal S}^{\char64}(\ast
, \ast
)$

\makebox[\idlength][r]{347}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{3}%
\makebox[0.5em]{}%
$\rm 
{\cal S}_{1}^{\char64}(\ast
, \ast
, \ast
)$

\makebox[\idlength][r]{348}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm 
{\cal S}^{\vdash}(\ast
, \ast
)$

\makebox[\idlength][r]{349}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{4}%
\makebox[0.5em]{}%
$\rm 
{\cal S}_{1}^{\vdash}(\ast
, \ast
, \ast
, \ast
)$

\makebox[\idlength][r]{350}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm 
{\cal S}^{\makebox [0mm][l]{\scriptsize $\vdash $}\,{\vdash }}(\ast
, \ast
)$

\makebox[\idlength][r]{351}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{4}%
\makebox[0.5em]{}%
$\rm 
{\cal S}_{1}^{\makebox [0mm][l]{\scriptsize $\vdash $}\,{\vdash }}(\ast
, \ast
, \ast
, \ast
)$

\makebox[\idlength][r]{352}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm 
{\cal S}^{i.e.}(\ast
, \ast
)$

\makebox[\idlength][r]{353}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{4}%
\makebox[0.5em]{}%
$\rm 
{\cal S}_{1}^{i.e.}(\ast
, \ast
, \ast
, \ast
)$

\makebox[\idlength][r]{354}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{5}%
\makebox[0.5em]{}%
$\rm 
{\cal S}_{2}^{i.e.}(\ast
, \ast
, \ast
, \ast
, \ast
)$

\makebox[\idlength][r]{355}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm 
{\cal S}^{\forall}(\ast
, \ast
)$

\makebox[\idlength][r]{356}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{4}%
\makebox[0.5em]{}%
$\rm 
{\cal S}_{1}^{\forall}(\ast
, \ast
, \ast
, \ast
)$

\makebox[\idlength][r]{357}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm 
{\cal S}^{;}(\ast
, \ast
)$

\makebox[\idlength][r]{358}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{3}%
\makebox[0.5em]{}%
$\rm 
{\cal S}_{1}^{;}(\ast
, \ast
, \ast
)$

\makebox[\idlength][r]{359}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{4}%
\makebox[0.5em]{}%
$\rm 
{\cal S}_{2}^{;}(\ast
, \ast
, \ast
, \ast
)$

\makebox[\idlength][r]{360}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm 
{\cal T}( \ast
)$

\makebox[\idlength][r]{361}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{3}%
\makebox[0.5em]{}%
$\rm 
claims( \ast
, \ast
, \ast
)$

\makebox[\idlength][r]{362}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{3}%
\makebox[0.5em]{}%
$\rm 
claims_2( \ast
, \ast
, \ast
)$

\makebox[\idlength][r]{363}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
{<}proof{>}$

\makebox[\idlength][r]{364}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
proof$

\makebox[\idlength][r]{365}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm 
[ \mathbf{Lemma\ } \ast
\colon \ast
]$

\makebox[\idlength][r]{366}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm 
[ \mathbf{Proof\ of\ }\ast
\colon \ast
]$

\makebox[\idlength][r]{367}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{3}%
\makebox[0.5em]{}%
$\rm 
[ \ast
\mathbf{\ lemma\ } \ast
\colon \ast
]$

\makebox[\idlength][r]{368}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{3}%
\makebox[0.5em]{}%
$\rm 
[ \ast
\mathbf{\ antilemma\ } \ast
\colon \ast
]$

\makebox[\idlength][r]{369}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{3}%
\makebox[0.5em]{}%
$\rm 
[ \ast
\mathbf{\ rule\ } \ast
\colon \ast
]$

\makebox[\idlength][r]{370}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{3}%
\makebox[0.5em]{}%
$\rm 
[ \ast
\mathbf{\ antirule\ } \ast
\colon \ast
]$

\makebox[\idlength][r]{371}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
\mbox{verifier}$

\makebox[\idlength][r]{372}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm 
{\cal V}_1( \ast
)$

\makebox[\idlength][r]{373}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm 
{\cal V}_2( \ast
, \ast
)$

\makebox[\idlength][r]{374}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{4}%
\makebox[0.5em]{}%
$\rm 
{\cal V}_3( \ast
, \ast
, \ast
, \ast
)$

\makebox[\idlength][r]{375}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm 
{\cal V}_4( \ast
, \ast
)$

\makebox[\idlength][r]{376}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{4}%
\makebox[0.5em]{}%
$\rm 
{\cal V}_5( \ast
, \ast
, \ast
, \ast
)$

\makebox[\idlength][r]{377}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{4}%
\makebox[0.5em]{}%
$\rm 
{\cal V}_6( \ast
, \ast
, \ast
, \ast
)$

\makebox[\idlength][r]{378}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{4}%
\makebox[0.5em]{}%
$\rm 
{\cal V}_7( \ast
, \ast
, \ast
, \ast
)$

\makebox[\idlength][r]{379}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm 
Cut( \ast
, \ast
)$

\makebox[\idlength][r]{380}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm 
Head_{\oplus} ( \ast
)$

\makebox[\idlength][r]{381}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm 
Tail_{\oplus} ( \ast
)$

\makebox[\idlength][r]{382}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm 
rule_1( \ast
, \ast
)$

\makebox[\idlength][r]{383}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm 
rule( \ast
, \ast
)$

\makebox[\idlength][r]{384}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
Rule\ tactic$

\makebox[\idlength][r]{385}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm 
Plus( \ast
, \ast
)$

\makebox[\idlength][r]{386}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm 
[ \mathbf{Theory\ } \ast
]$

\makebox[\idlength][r]{387}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm 
theory_2( \ast
, \ast
)$

\makebox[\idlength][r]{388}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm 
theory_3( \ast
, \ast
)$

\makebox[\idlength][r]{389}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{3}%
\makebox[0.5em]{}%
$\rm 
theory_4( \ast
, \ast
, \ast
)$

\makebox[\idlength][r]{390}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
HeadNil''$

\makebox[\idlength][r]{391}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
HeadPair''$

\makebox[\idlength][r]{392}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
Transitivity''$

\makebox[\idlength][r]{393}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
Contra''$

\makebox[\idlength][r]{394}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
HeadNil$

\makebox[\idlength][r]{395}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
HeadPair$

\makebox[\idlength][r]{396}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
Transitivity$

\makebox[\idlength][r]{397}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
Contra$

\makebox[\idlength][r]{398}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
T_E$

\makebox[\idlength][r]{399}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
ragged\ right$

\makebox[\idlength][r]{400}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
ragged\ right\ expansion\ $

\makebox[\idlength][r]{401}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{3}%
\makebox[0.5em]{}%
$\rm 
parm(\ast
,\ast
,\ast
)$

\makebox[\idlength][r]{402}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{3}%
\makebox[0.5em]{}%
$\rm 
parm^*(\ast
,\ast
,\ast
)$

\makebox[\idlength][r]{403}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm 
inst(\ast
,\ast
)$

\makebox[\idlength][r]{404}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm 
inst^*(\ast
,\ast
)$

\makebox[\idlength][r]{405}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{3}%
\makebox[0.5em]{}%
$\rm 
occur(\ast
,\ast
,\ast
)$

\makebox[\idlength][r]{406}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{3}%
\makebox[0.5em]{}%
$\rm 
occur^*(\ast
,\ast
,\ast
)$

\makebox[\idlength][r]{407}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{3}%
\makebox[0.5em]{}%
$\rm 
unify(\ast
=\ast
,\ast
)$

\makebox[\idlength][r]{408}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{3}%
\makebox[0.5em]{}%
$\rm 
unify^*(\ast
=\ast
,\ast
)$

\makebox[\idlength][r]{409}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{3}%
\makebox[0.5em]{}%
$\rm 
unify_2(\ast
=\ast
,\ast
)$

\makebox[\idlength][r]{410}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm L_a$

\makebox[\idlength][r]{411}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm L_b$

\makebox[\idlength][r]{412}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm L_c$

\makebox[\idlength][r]{413}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm L_d$

\makebox[\idlength][r]{414}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm L_e$

\makebox[\idlength][r]{415}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm L_f$

\makebox[\idlength][r]{416}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm L_g$

\makebox[\idlength][r]{417}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm L_h$

\makebox[\idlength][r]{418}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm L_i$

\makebox[\idlength][r]{419}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm L_j$

\makebox[\idlength][r]{420}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm L_k$

\makebox[\idlength][r]{421}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm L_l$

\makebox[\idlength][r]{422}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm L_m$

\makebox[\idlength][r]{423}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm L_n$

\makebox[\idlength][r]{424}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm L_o$

\makebox[\idlength][r]{425}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm L_p$

\makebox[\idlength][r]{426}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm L_q$

\makebox[\idlength][r]{427}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm L_r$

\makebox[\idlength][r]{428}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm L_s$

\makebox[\idlength][r]{429}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm L_t$

\makebox[\idlength][r]{430}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm L_u$

\makebox[\idlength][r]{431}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm L_v$

\makebox[\idlength][r]{432}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm L_w$

\makebox[\idlength][r]{433}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm L_x$

\makebox[\idlength][r]{434}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm L_y$

\makebox[\idlength][r]{435}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm L_z$

\makebox[\idlength][r]{436}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm L_A$

\makebox[\idlength][r]{437}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm L_B$

\makebox[\idlength][r]{438}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm L_C$

\makebox[\idlength][r]{439}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm L_D$

\makebox[\idlength][r]{440}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm L_E$

\makebox[\idlength][r]{441}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm L_F$

\makebox[\idlength][r]{442}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm L_G$

\makebox[\idlength][r]{443}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm L_H$

\makebox[\idlength][r]{444}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm L_I$

\makebox[\idlength][r]{445}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm L_J$

\makebox[\idlength][r]{446}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm L_K$

\makebox[\idlength][r]{447}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm L_L$

\makebox[\idlength][r]{448}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm L_M$

\makebox[\idlength][r]{449}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm L_N$

\makebox[\idlength][r]{450}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm L_O$

\makebox[\idlength][r]{451}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm L_P$

\makebox[\idlength][r]{452}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm L_Q$

\makebox[\idlength][r]{453}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm L_R$

\makebox[\idlength][r]{454}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm L_S$

\makebox[\idlength][r]{455}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm L_T$

\makebox[\idlength][r]{456}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm L_U$

\makebox[\idlength][r]{457}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm L_V$

\makebox[\idlength][r]{458}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm L_W$

\makebox[\idlength][r]{459}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm L_X$

\makebox[\idlength][r]{460}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm L_Y$

\makebox[\idlength][r]{461}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm L_Z$

\makebox[\idlength][r]{462}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm L_?$

\makebox[\idlength][r]{463}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
Reflexivity$

\makebox[\idlength][r]{464}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
Reflexivity_1$

\makebox[\idlength][r]{465}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
Commutativity$

\makebox[\idlength][r]{466}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
Commutativity_1$

\makebox[\idlength][r]{467}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
{<}tactic{>}$

\makebox[\idlength][r]{468}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
tactic$

\makebox[\idlength][r]{469}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm 
[\ast
\stackrel {tactic}{=}\ast
]$

\makebox[\idlength][r]{470}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{3}%
\makebox[0.5em]{}%
$\rm 
{\cal P}( \ast
, \ast
, \ast
)$

\makebox[\idlength][r]{471}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{3}%
\makebox[0.5em]{}%
$\rm 
{\cal P}^*( \ast
, \ast
, \ast
)$

\makebox[\idlength][r]{472}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
p_0$

\makebox[\idlength][r]{473}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm 
conclude_1 ( \ast
, \ast
)$

\makebox[\idlength][r]{474}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{3}%
\makebox[0.5em]{}%
$\rm 
conclude_2 ( \ast
, \ast
, \ast
)$

\makebox[\idlength][r]{475}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{4}%
\makebox[0.5em]{}%
$\rm 
conclude_3 ( \ast
, \ast
, \ast
, \ast
)$

\makebox[\idlength][r]{476}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm 
conclude_4 ( \ast
, \ast
)$

\makebox[\idlength][r]{477}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm \ast
\_\{\ast
\}$

\makebox[\idlength][r]{478}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{5}%
\makebox[0.5em]{}%
$\rm \ast
/indexintro(\ast
,\ast
,\ast
,\ast
)$

\makebox[\idlength][r]{479}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{4}%
\makebox[0.5em]{}%
$\rm \ast
/intro(\ast
,\ast
,\ast
)$

\makebox[\idlength][r]{480}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{6}%
\makebox[0.5em]{}%
$\rm \ast
/bothintro(\ast
,\ast
,\ast
,\ast
,\ast
)$

\makebox[\idlength][r]{481}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{5}%
\makebox[0.5em]{}%
$\rm \ast
/nameintro(\ast
,\ast
,\ast
,\ast
)$

\makebox[\idlength][r]{482}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm \ast'$

\makebox[\idlength][r]{483}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm \ast
{[}\ast
{]}$

\makebox[\idlength][r]{484}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{3}%
\makebox[0.5em]{}%
$\rm \ast
[ \ast
{\rightarrow} \ast
]$

\makebox[\idlength][r]{485}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{3}%
\makebox[0.5em]{}%
$\rm \ast
[ \ast
{\Rightarrow} \ast
]$

\makebox[\idlength][r]{486}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm \ast
0$

\makebox[\idlength][r]{487}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm \ast
1$

\makebox[\idlength][r]{488}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
0 \mathrm {b}$

\makebox[\idlength][r]{489}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm \ast
\mbox {-color}( \ast
)$

\makebox[\idlength][r]{490}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm \ast
\mbox {-color}^{\ast}( \ast
)$

\makebox[\idlength][r]{491}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm \ast
{}^H$

\makebox[\idlength][r]{492}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm \ast
{}^T$

\makebox[\idlength][r]{493}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm \ast
{}^U$

\makebox[\idlength][r]{494}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm \ast
{}^h$

\makebox[\idlength][r]{495}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm \ast
{}^t$

\makebox[\idlength][r]{496}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm \ast
{}^s$

\makebox[\idlength][r]{497}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm \ast
{}^c$

\makebox[\idlength][r]{498}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm \ast
{}^d$

\makebox[\idlength][r]{499}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm \ast
{}^a$

\makebox[\idlength][r]{500}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm \ast
{}^C$

\makebox[\idlength][r]{501}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm \ast
{}^M$

\makebox[\idlength][r]{502}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm \ast
{}^B$

\makebox[\idlength][r]{503}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm \ast
{}^{r}$

\makebox[\idlength][r]{504}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm \ast
{}^{i}$

\makebox[\idlength][r]{505}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm \ast
{}^{d}$

\makebox[\idlength][r]{506}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm \ast
{}^{R}$

\makebox[\idlength][r]{507}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm \ast
{}^{0}$

\makebox[\idlength][r]{508}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm \ast
{}^{1}$

\makebox[\idlength][r]{509}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm \ast
{}^{2}$

\makebox[\idlength][r]{510}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm \ast
{}^{3}$

\makebox[\idlength][r]{511}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm \ast
{}^{4}$

\makebox[\idlength][r]{512}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm \ast
{}^{5}$

\makebox[\idlength][r]{513}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm \ast
{}^{6}$

\makebox[\idlength][r]{514}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm \ast
{}^{7}$

\makebox[\idlength][r]{515}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm \ast
{}^{8}$

\makebox[\idlength][r]{516}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm \ast
{}^{9}$

\makebox[\idlength][r]{517}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm \ast
{} ^ { E }$

\makebox[\idlength][r]{518}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm \ast
{} ^ {\cal V}$

\makebox[\idlength][r]{519}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm \ast
{} ^ {\cal C}$

\makebox[\idlength][r]{520}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm \ast
{} ^ {{\cal C} ^ { \ast }}$

\makebox[\idlength][r]{521}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm 
newline\ \ast$

\makebox[\idlength][r]{522}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm 
macro\ newline\ \ast$

\makebox[\idlength][r]{523}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm \ast
\mathbin {\mbox {'}}\ast$

\makebox[\idlength][r]{524}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm \ast
\mathbin {\mbox {`}}\ast$

\makebox[\idlength][r]{525}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm \ast
\cdot \ast$

\makebox[\idlength][r]{526}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm \ast
\cdot_0 \ast$

\makebox[\idlength][r]{527}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm \ast
+ \ast$

\makebox[\idlength][r]{528}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm \ast
\mathop{+_0} \ast$

\makebox[\idlength][r]{529}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm \ast
\mathop{+_1} \ast$

\makebox[\idlength][r]{530}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm \ast
- \ast$

\makebox[\idlength][r]{531}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm \ast
\mathop{-_0} \ast$

\makebox[\idlength][r]{532}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm \ast
\mathop{-_1} \ast$

\makebox[\idlength][r]{533}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm \ast
\cup \{ \ast
\}$

\makebox[\idlength][r]{534}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm \ast
\cup \ast$

\makebox[\idlength][r]{535}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm \ast
\backslash \{ \ast
\}$

\makebox[\idlength][r]{536}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm \ast
\mathrel { \dot { . \, . } }\ast$

\makebox[\idlength][r]{537}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm \ast
\mathrel { \underline { \dot { . \, . } } }\ast$

\makebox[\idlength][r]{538}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm \ast
\mathrel { \underline { : \, : } }\ast$

\makebox[\idlength][r]{539}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm \ast
\mathrel { \underline { {+} 2 \ast } }\ast$

\makebox[\idlength][r]{540}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm \ast
\mathrel { : \, : }\ast$

\makebox[\idlength][r]{541}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm \ast
\mathrel { {+} 2 \ast }\ast$

\makebox[\idlength][r]{542}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm \ast
,\linebreak [0] \ast$

\makebox[\idlength][r]{543}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm \ast
\stackrel {B}{\approx }\ast$

\makebox[\idlength][r]{544}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm \ast
\stackrel {D}{\approx }\ast$

\makebox[\idlength][r]{545}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm \ast
\stackrel {C}{\approx }\ast$

\makebox[\idlength][r]{546}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm \ast
\stackrel {P}{\approx }\ast$

\makebox[\idlength][r]{547}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm \ast
\approx \ast$

\makebox[\idlength][r]{548}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm \ast
=\ast$

\makebox[\idlength][r]{549}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm \ast
\stackrel {+}{\rightarrow }\ast$

\makebox[\idlength][r]{550}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm \ast
\stackrel {t}{=}\ast$

\makebox[\idlength][r]{551}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm \ast
\stackrel {t^*}{=}\ast$

\makebox[\idlength][r]{552}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm \ast
\stackrel{r}{=} \ast$

\makebox[\idlength][r]{553}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm \ast
\in_t \ast$

\makebox[\idlength][r]{554}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm \ast
\subseteq_T \ast$

\makebox[\idlength][r]{555}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm \ast
\stackrel{T}{=} \ast$

\makebox[\idlength][r]{556}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm \ast
\stackrel{s}{=} \ast$

\makebox[\idlength][r]{557}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm \ast
\mathrel {free\ in} \ast$

\makebox[\idlength][r]{558}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm \ast
\mathrel {free\ in}^{\ast} \ast$

\makebox[\idlength][r]{559}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{3}%
\makebox[0.5em]{}%
$\rm \ast
\mathrel {free\ for} \ast
\mathrel {in} \ast$

\makebox[\idlength][r]{560}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{3}%
\makebox[0.5em]{}%
$\rm \ast
\mathrel {free\ for}^{\ast} \ast
\mathrel {in} \ast$

\makebox[\idlength][r]{561}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm \ast
\in_c \ast$

\makebox[\idlength][r]{562}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm \ast
< \ast$

\makebox[\idlength][r]{563}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm \ast
<' \ast$

\makebox[\idlength][r]{564}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm \ast
\le' \ast$

\makebox[\idlength][r]{565}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm 
{\neg }\ast$

\makebox[\idlength][r]{566}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm \ast
\wedge \ast$

\makebox[\idlength][r]{567}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm \ast
\mathrel{\ddot{\wedge}} \ast$

\makebox[\idlength][r]{568}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm \ast
\mathrel{\tilde{\wedge}} \ast$

\makebox[\idlength][r]{569}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm \ast
\wedge_c \ast$

\makebox[\idlength][r]{570}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm \ast
\vee \ast$

\makebox[\idlength][r]{571}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm \ast
\parallel \ast$

\makebox[\idlength][r]{572}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm \ast
\mathrel{\ddot{\vee}} \ast$

\makebox[\idlength][r]{573}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm \ast
\mathrel{\ddot{\Rightarrow}} \ast$

\makebox[\idlength][r]{574}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm \ast
:\ast$

\makebox[\idlength][r]{575}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm \ast
\mathrel{spy}\ast$

\makebox[\idlength][r]{576}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm \ast
!\ast$

\makebox[\idlength][r]{577}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{3}%
\makebox[0.5em]{}%
$\rm \ast
\left\{\protect \begin {array}{l}\ast
\\\ast
\protect \end {array}\right.$

\makebox[\idlength][r]{578}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm 
\lambda \ast
.\ast$

\makebox[\idlength][r]{579}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm 
\Lambda \ast
. \ast$

\makebox[\idlength][r]{580}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm 
\Lambda \ast$

\makebox[\idlength][r]{581}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{3}%
\makebox[0.5em]{}%
$\rm 
{\bf if} \ \ast
\ {\bf then} \ \ast
\ {\bf else} \ \ast$

\makebox[\idlength][r]{582}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{3}%
\makebox[0.5em]{}%
$\rm 
\mathbf{let\ } \ast
= \ast
\mathbf{\ in\ } \ast$

\makebox[\idlength][r]{583}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{3}%
\makebox[0.5em]{}%
$\rm 
\mathbf{let\ } \ast
\mathrel{\ddot{=}} \ast
\mathrel{\ in\ } \ast$

\makebox[\idlength][r]{584}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm \ast
{} ^ { I }$

\makebox[\idlength][r]{585}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm \ast
{} ^ { \rhd }$

\makebox[\idlength][r]{586}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm \ast
{} ^ { V } $

\makebox[\idlength][r]{587}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm \ast
{} ^ { + } $

\makebox[\idlength][r]{588}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm \ast
{} ^ { - } $

\makebox[\idlength][r]{589}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm \ast
{} ^ { \ast } $

\makebox[\idlength][r]{590}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm \ast
\mathop {\char64} \ast$

\makebox[\idlength][r]{591}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm \ast
\rhd \ast$

\makebox[\idlength][r]{592}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm \ast
\mathrel {\makebox [0mm][l]{$\rhd $}\,{\rhd }} \ast$

\makebox[\idlength][r]{593}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm \ast
\gg \ast$

\makebox[\idlength][r]{594}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm \ast
\vdash \ast$

\makebox[\idlength][r]{595}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm \ast
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} \ast$

\makebox[\idlength][r]{596}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm \ast
\mathrel {i.e.} \ast$

\makebox[\idlength][r]{597}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm 
\forall \ast
\colon \ast$

\makebox[\idlength][r]{598}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm \ast
\mathrel {\oplus} \ast$

\makebox[\idlength][r]{599}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm \ast
; \ast$

\makebox[\idlength][r]{600}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm \ast
\ proves\ \ast$

\makebox[\idlength][r]{601}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{3}%
\makebox[0.5em]{}%
$\rm \ast
\mathbf{\ proof\ of\ } \ast
: \ast$

\makebox[\idlength][r]{602}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{4}%
\makebox[0.5em]{}%
$\rm 
Line \, \ast
: \ast
\gg \ast
; \ast$

\makebox[\idlength][r]{603}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm 
Last\ line \, \ast
\gg \ast
\,\Box$

\makebox[\idlength][r]{604}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{3}%
\makebox[0.5em]{}%
$\rm 
Line \, \ast
: Premise \gg \ast
;\ast$

\makebox[\idlength][r]{605}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{3}%
\makebox[0.5em]{}%
$\rm 
Line \, \ast
: \mbox{Side-condition} \gg \ast
; \ast$

\makebox[\idlength][r]{606}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm 
Arbitrary \gg \ast
;\ast$

\makebox[\idlength][r]{607}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{3}%
\makebox[0.5em]{}%
$\rm 
Local \gg \ast
= \ast
; \ast$

\makebox[\idlength][r]{608}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm \ast
\& \ast$

\makebox[\idlength][r]{609}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm \ast
\backslash \backslash \ast$

\vspace{2ex}

{\em \href {http://www.diku.dk/~grue/logiweb/20060417/logiweb/doc/compiler/index.html}{The pyk compiler},
version 0.grue.20060417+
by
\href {http://www.diku.dk/~grue/index.html}{Klaus Grue}\\
\href {http://www.diku.dk/~grue/logiweb/20060417/logiweb/doc/misc/time.html}{GRD-2006-05-04.UTC:15:30:23.702808} = 
\href {http://www.diku.dk/~grue/logiweb/20060417/logiweb/doc/misc/time.html}{MJD-53859.TAI:15:30:56.702808} = 
\href {http://www.diku.dk/~grue/logiweb/20060417/logiweb/doc/misc/time.html}{LGT-4653473456702808e-6}
}

\end{document}

