\documentclass [fleqn]{article}

\everymath{\rm}
\everydisplay{\rm}
\usepackage{latexsym}
\setlength {\overfullrule }{0mm}
%\input{lgwinclude}

\usepackage{url}
\usepackage[dvipdfm=true]{hyperref}
\usepackage{amsmath}
\usepackage{theorem}
\usepackage{amssymb}
\hypersetup{pdfpagemode=none}
\hypersetup{pdfstartpage=1}
\hypersetup{pdfstartview=FitBH}
\hypersetup{pdfpagescrop={120 80 490 680}}
\hypersetup{pdftitle=Logiweb sequent calculus}
\hypersetup{colorlinks=true}

% Save current \parindent (used by e.g. pyk display ... end display)
\newlength{\docparindent}
\setlength{\docparindent}{\parindent}

%Our extras
\newtheorem{Def}{Definition}[section]
\newtheorem{Lem}[Def]{Lemma}
\newtheorem{The}[Def]{Theorem}
\newtheorem{Cor}[Def]{Corollary}
\newtheorem{Alg}[Def]{Algorithm}
\theorembodyfont{\rmfamily} %normale bogstaver
\newtheorem{Exa}[Def]{Example}
\newtheorem{Rem}[Def]{Remark}

\begin{document}
\title{A formal proof in Group Theory}
\author{Lasse Nielsen \& Morten Ib Nielsen\\
Department of Computer Science, University of Copenhagen}
\date{\today}
\maketitle

\section{Introduction}
In this report we set out to formally prove a simple result
of Group Theory namely:
\begin{The}
Let $e$ be a neutral element of a Group $G$ then $e$ is unique. Thus
we can talk about \emph{the neutral element} of a Group $G$.
\end{The}

The theorem above is very loosely formulated. In this report we set out to
formalize the theorem and give a formal proof of it's correctness. In order to
do this we need to do a lot of other work.
First in XXTODO we define \emph{Propositional Calculus} and then in MMTODO we define \emph{First order Predicate Calculus}. Then using this we define
ZFC set theory in YYTODO and finally having set theory available we can define a Group in ZZTODO.
Then in WWTODO we restate the above theorem in a formal setting and we give a formal proof of it's
correctness.

TODO mere jalla.

\section{Propositional Calculus}
Based on mathworld\footnote{http://mathworld.wolfram.com/First-OrderLogic.html.} and thus on Kleene (2002) we define
first-order predicate calculus below. We note that the axioms 1 through 10 together with the inference rule
modus ponens constitutes the propositional calculus.

Our definitions are not excately like those found on Mathworld. The reason is that we have made
$\Rightarrow$ right associative this means that 
${\cal F} \Rightarrow {\cal G} \Rightarrow {\cal F}$ really means
${\cal F} \Rightarrow 
({\cal G} \Rightarrow {\cal F}
)$ below.

The $
[ \mathbf{Theory\ } 
\mbox{pred calc}
]$ contains the following axioms
\begin{enumerate}
\item $
[ 
\mbox{pred calc}
\mathbf{\ rule\ } 
\mbox{pc1}
\colon 
\forall {\cal F}
\colon 
\forall {\cal G}
\colon {\cal F} \Rightarrow {\cal G} \Rightarrow {\cal F}
]$

\item $
[ 
\mbox{pred calc}
\mathbf{\ rule\ } 
\mbox{pc2}
\colon 
\forall {\cal F}
\colon 
\forall {\cal G}
\colon 
\forall {\cal H}
\colon 
({\cal F} \Rightarrow {\cal G}
) \Rightarrow 
({\cal F} \Rightarrow {\cal G} \Rightarrow {\cal H}
) \Rightarrow {\cal F} \Rightarrow {\cal H}
]$

\item $
[ 
\mbox{pred calc}
\mathbf{\ rule\ } 
\mbox{pc3}
\colon 
\forall {\cal F}
\colon 
\forall {\cal G}
\colon {\cal F} \Rightarrow {\cal G} \Rightarrow {\cal F} \wedge {\cal G}
]$

\item $
[ 
\mbox{pred calc}
\mathbf{\ rule\ } 
\mbox{pc4}
\colon 
\forall {\cal F}
\colon 
\forall {\cal G}
\colon {\cal F} \Rightarrow {\cal F} \vee {\cal G}
]$

\item $
[ 
\mbox{pred calc}
\mathbf{\ rule\ } 
\mbox{pc5}
\colon 
\forall {\cal F}
\colon 
\forall {\cal G}
\colon {\cal F} \Rightarrow {\cal G} \vee {\cal F}
]$

\item $
[ 
\mbox{pred calc}
\mathbf{\ rule\ } 
\mbox{pc6}
\colon 
\forall {\cal F}
\colon 
\forall {\cal G}
\colon {\cal F} \wedge {\cal G} \Rightarrow {\cal F}
]$

\item $
[ 
\mbox{pred calc}
\mathbf{\ rule\ } 
\mbox{pc7}
\colon 
\forall {\cal F}
\colon 
\forall {\cal G}
\colon {\cal F} \wedge {\cal G} \Rightarrow {\cal G}
]$

\item $
[ 
\mbox{pred calc}
\mathbf{\ rule\ } 
\mbox{pc8}
\colon 
\forall {\cal F}
\colon 
\forall {\cal G}
\colon 
\forall {\cal H}
\colon 
({\cal F} \Rightarrow {\cal G}
) \Rightarrow 
({\cal H} \Rightarrow {\cal G}
) \Rightarrow {\cal F} \vee {\cal H} \Rightarrow {\cal G}
]$

\item $
[ 
\mbox{pred calc}
\mathbf{\ rule\ } 
\mbox{pc9}
\colon 
\forall {\cal F}
\colon 
\forall {\cal G}
\colon 
({\cal F} \Rightarrow {\cal G}
) \Rightarrow 
({\cal F} \Rightarrow \neg {\cal G}
) \Rightarrow \neg {\cal F}
]$

\item $
[ 
\mbox{pred calc}
\mathbf{\ rule\ } 
\mbox{pc10}
\colon 
\forall {\cal F}
\colon \neg \neg {\cal F} \Rightarrow {\cal F}
]$

\item $
[ 
\mbox{pred calc}
\mathbf{\ rule\ } 
\mbox{pc11}
\colon 
\forall {\cal F}
\colon 
\forall {\cal R}
\colon 
\forall {\cal X}
\colon 
\forall {\cal Y}
\colon \Pi~{\cal Y} . 
\langle {\cal F}
\,{|}{\cal X}
{:=}\,{\cal Y}
\rangle  \Rightarrow 
\langle {\cal F}
\,{|}{\cal X}
{:=}\,{\cal R}
\rangle 
]$

\item $
[ 
\mbox{pred calc}
\mathbf{\ rule\ } 
\mbox{pc11}
\colon 
\forall {\cal F}
\colon 
\forall {\cal R}
\colon 
\forall {\cal X}
\colon 
\forall {\cal Y}
\colon 
\langle {\cal F}
\,{|}{\cal X}
{:=}\,{\cal R}
\rangle  \Rightarrow \Sigma~{\cal Y} . 
\langle {\cal F}
\,{|}{\cal X}
{:=}\,{\cal Y}
\rangle 
]$
\end{enumerate}

We note that in first order predicate calculus metaiables used in functions $F$ and predicates $P$ are \emph{object metaiables}.

The only proof rule in $
[ \mathbf{Theory\ } 
\mbox{pred calc}
]$ is Modus Ponens which says
\begin{itemize}
\item $
[ 
\mbox{pred calc}
\mathbf{\ rule\ } 
\mbox{pcmp}
\colon 
\forall {\cal F}
\colon 
\forall {\cal G}
\colon {\cal F}
\vdash {\cal F} \Rightarrow {\cal G}
\vdash {\cal G}
]$

\item $
[ 
\mbox{pred calc}
\mathbf{\ rule\ } 
\mbox{pcia}
\colon 
\forall {\cal F}
\colon 
\forall {\cal G}
\colon 
\forall {\cal X}
\colon 
\forall {\cal Y}
\colon {\cal G} \Rightarrow 
\langle {\cal F}
\,{|}{\cal X}
{:=}\,{\cal Y}
\rangle 
\vdash {\cal G} \Rightarrow \Pi~{\cal Y} . 
\langle {\cal F}
\,{|}{\cal X}
{:=}\,{\cal Y}
\rangle 
]$
 
\item $
[ 
\mbox{pred calc}
\mathbf{\ rule\ } 
\mbox{pcie}
\colon 
\forall {\cal F}
\colon 
\forall {\cal G}
\colon 
\forall {\cal X}
\colon 
\forall {\cal Y}
\colon 
\langle {\cal F}
\,{|}{\cal X}
{:=}\,{\cal Y}
\rangle  \Rightarrow {\cal G}
\vdash \Sigma~{\cal Y} . 
\langle {\cal F}
\,{|}{\cal X}
{:=}\,{\cal Y}
\rangle  \Rightarrow {\cal G}
]$
\end{itemize}

\subsection{A little proof}
Below we make some small proofs just to demonstrate how to do it but also in order to test our definitions
above.

\begin{Lem}
$
[ 
\mbox{pred calc}
\mathbf{\ lemma\ } 
\mbox{trivia}
\colon 
\forall {\cal F}
\colon {\cal F} \Rightarrow {\cal F}
]$
\end{Lem}

$
\if\relax\csname lgwprooflinep\endcsname
\def\lgwprooflinep{x}
\newcount\lgwproofline
\fi
\begingroup
\def\insideproof{x}
\lgwproofline=0 
\mbox{pred calc}
\mathbf {\ proof\ of\ } 
\mbox{trivia}
\colon 
\newline \makebox [0.1\textwidth ][l]{$
\if \relax \csname lgwprooflinep\endcsname L_? \else
\global \advance \lgwproofline by 1
L\ifnum \lgwproofline <10 0\fi \number \lgwproofline
\fi 
$:}\makebox [0.4\textwidth ][l]{$Arbitrary{}\gg{}$}\quad
\parbox [t]{0.4\textwidth }{${\cal F}
$\hfill \makebox [0mm][l]{\quad ;}}
\newline \makebox [0.1\textwidth]{}%
\parbox [b]{0.4\textwidth }{\raggedright
\setlength {\parindent }{-0.1\textwidth }%
\makebox [0.1\textwidth ][l]{$
\if \relax \csname lgwprooflinep\endcsname L_a \else
\if \relax \csname lgwella\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwella {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwella \fi 
$:}$
\mbox{pc2}
{}\gg {}$}\quad
\parbox [t]{0.4\textwidth }{$
({\cal F} \Rightarrow {\cal F} \Rightarrow {\cal F}
) \Rightarrow 
({\cal F} \Rightarrow 
({\cal F} \Rightarrow {\cal F}
) \Rightarrow {\cal F}
) \Rightarrow {\cal F} \Rightarrow {\cal F}
$\hfill \makebox [0mm][l]{\quad ;}}
\newline \makebox [0.1\textwidth]{}%
\parbox [b]{0.4\textwidth }{\raggedright
\setlength {\parindent }{-0.1\textwidth }%
\makebox [0.1\textwidth ][l]{$
\if \relax \csname lgwprooflinep\endcsname L_b \else
\if \relax \csname lgwellb\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwellb {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwellb \fi 
$:}$
\mbox{pc1}
{}\gg {}$}\quad
\parbox [t]{0.4\textwidth }{${\cal F} \Rightarrow {\cal F} \Rightarrow {\cal F}
$\hfill \makebox [0mm][l]{\quad ;}}
\newline \makebox [0.1\textwidth]{}%
\parbox [b]{0.4\textwidth }{\raggedright
\setlength {\parindent }{-0.1\textwidth }%
\makebox [0.1\textwidth ][l]{$
\if \relax \csname lgwprooflinep\endcsname L_c \else
\if \relax \csname lgwellc\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwellc {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwellc \fi 
$:}$
\mbox{pcmp}
\rhd 
\if \relax \csname lgwprooflinep\endcsname L_b \else
\if \relax \csname lgwellb\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwellb {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwellb \fi 
\rhd 
\if \relax \csname lgwprooflinep\endcsname L_a \else
\if \relax \csname lgwella\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwella {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwella \fi 
{}\gg {}$}\quad
\parbox [t]{0.4\textwidth }{$
({\cal F} \Rightarrow 
({\cal F} \Rightarrow {\cal F}
) \Rightarrow {\cal F}
) \Rightarrow {\cal F} \Rightarrow {\cal F}
$\hfill \makebox [0mm][l]{\quad ;}}
\newline \makebox [0.1\textwidth]{}%
\parbox [b]{0.4\textwidth }{\raggedright
\setlength {\parindent }{-0.1\textwidth }%
\makebox [0.1\textwidth ][l]{$
\if \relax \csname lgwprooflinep\endcsname L_d \else
\if \relax \csname lgwelld\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwelld {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwelld \fi 
$:}$
\mbox{pc1}
{}\gg {}$}\quad
\parbox [t]{0.4\textwidth }{${\cal F} \Rightarrow 
({\cal F} \Rightarrow {\cal F}
) \Rightarrow {\cal F}
$\hfill \makebox [0mm][l]{\quad ;}}
\newline \makebox [0.1\textwidth]{}%
\parbox [b]{0.4\textwidth }{\raggedright
\setlength {\parindent }{-0.1\textwidth }%
\makebox [0.1\textwidth ][l]{$
\if \relax \csname lgwprooflinep\endcsname L_? \else
\global \advance \lgwproofline by 1
L\ifnum \lgwproofline <10 0\fi \number \lgwproofline
\fi 
$:}$
\mbox{pcmp}
\rhd 
\if \relax \csname lgwprooflinep\endcsname L_d \else
\if \relax \csname lgwelld\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwelld {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwelld \fi 
\rhd 
\if \relax \csname lgwprooflinep\endcsname L_c \else
\if \relax \csname lgwellc\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwellc {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwellc \fi 
{}\gg {}$}\quad
\parbox [t]{0.4\textwidth }{${\cal F} \Rightarrow {\cal F}
$\hfill \makebox [0mm][l]{\quad \makebox[0mm]{$\Box$}}}
\gdef\lgwella{\relax}
\gdef\lgwellb{\relax}
\gdef\lgwellc{\relax}
\gdef\lgwelld{\relax}
\gdef\lgwelle{\relax}
\gdef\lgwellf{\relax}
\gdef\lgwellg{\relax}
\gdef\lgwellh{\relax}
\gdef\lgwelli{\relax}
\gdef\lgwellj{\relax}
\gdef\lgwellk{\relax}
\gdef\lgwelll{\relax}
\gdef\lgwellm{\relax}
\gdef\lgwelln{\relax}
\gdef\lgwello{\relax}
\gdef\lgwellp{\relax}
\gdef\lgwellq{\relax}
\gdef\lgwellr{\relax}
\gdef\lgwells{\relax}
\gdef\lgwellt{\relax}
\gdef\lgwellu{\relax}
\gdef\lgwellv{\relax}
\gdef\lgwellw{\relax}
\gdef\lgwellx{\relax}
\gdef\lgwelly{\relax}
\gdef\lgwellz{\relax}
\gdef\lgwellbiga{\relax}
\gdef\lgwellbigb{\relax}
\gdef\lgwellbigc{\relax}
\gdef\lgwellbigd{\relax}
\gdef\lgwellbige{\relax}
\gdef\lgwellbigf{\relax}
\gdef\lgwellbigg{\relax}
\gdef\lgwellbigh{\relax}
\gdef\lgwellbigi{\relax}
\gdef\lgwellbigj{\relax}
\gdef\lgwellbigk{\relax}
\gdef\lgwellbigl{\relax}
\gdef\lgwellbigm{\relax}
\gdef\lgwellbign{\relax}
\gdef\lgwellbigo{\relax}
\gdef\lgwellbigp{\relax}
\gdef\lgwellbigq{\relax}
\gdef\lgwellbigr{\relax}
\gdef\lgwellbigs{\relax}
\gdef\lgwellbigt{\relax}
\gdef\lgwellbigu{\relax}
\gdef\lgwellbigv{\relax}
\gdef\lgwellbigw{\relax}
\gdef\lgwellbigx{\relax}
\gdef\lgwellbigy{\relax}
\gdef\lgwellbigz{\relax}
\endgroup $

\begin{Lem}
$
[ 
\mbox{pred calc}
\mathbf{\ lemma\ } 
\mbox{iatest}
\colon 
\forall {\cal Y}
\colon 
\forall {\cal G}
\colon {\cal G} \Rightarrow \Pi~{\cal Y} . {\cal Y} \Rightarrow {\cal G}
]$
\end{Lem}

$
\if\relax\csname lgwprooflinep\endcsname
\def\lgwprooflinep{x}
\newcount\lgwproofline
\fi
\begingroup
\def\insideproof{x}
\lgwproofline=0 
\mbox{pred calc}
\mathbf {\ proof\ of\ } 
\mbox{iatest}
\colon 
\newline \makebox [0.1\textwidth ][l]{$
\if \relax \csname lgwprooflinep\endcsname L_? \else
\global \advance \lgwproofline by 1
L\ifnum \lgwproofline <10 0\fi \number \lgwproofline
\fi 
$:}\makebox [0.4\textwidth ][l]{$Arbitrary{}\gg{}$}\quad
\parbox [t]{0.4\textwidth }{${\cal Y}
$\hfill \makebox [0mm][l]{\quad ;}}
\newline \makebox [0.1\textwidth ][l]{$
\if \relax \csname lgwprooflinep\endcsname L_? \else
\global \advance \lgwproofline by 1
L\ifnum \lgwproofline <10 0\fi \number \lgwproofline
\fi 
$:}\makebox [0.4\textwidth ][l]{$Arbitrary{}\gg{}$}\quad
\parbox [t]{0.4\textwidth }{${\cal G}
$\hfill \makebox [0mm][l]{\quad ;}}
\newline \makebox [0.1\textwidth]{}%
\parbox [b]{0.4\textwidth }{\raggedright
\setlength {\parindent }{-0.1\textwidth }%
\makebox [0.1\textwidth ][l]{$
\if \relax \csname lgwprooflinep\endcsname L_a \else
\if \relax \csname lgwella\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwella {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwella \fi 
$:}$
\mbox{pc1}
{}\gg {}$}\quad
\parbox [t]{0.4\textwidth }{${\cal G} \Rightarrow {\cal Y} \Rightarrow {\cal G}
$\hfill \makebox [0mm][l]{\quad ;}}
\newline \makebox [0.1\textwidth]{}%
\parbox [b]{0.4\textwidth }{\raggedright
\setlength {\parindent }{-0.1\textwidth }%
\makebox [0.1\textwidth ][l]{$
\if \relax \csname lgwprooflinep\endcsname L_? \else
\global \advance \lgwproofline by 1
L\ifnum \lgwproofline <10 0\fi \number \lgwproofline
\fi 
$:}$
\mbox{pcia}
\rhd 
\if \relax \csname lgwprooflinep\endcsname L_a \else
\if \relax \csname lgwella\endcsname
\global \advance \lgwproofline by 1
\xdef \lgwella {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline }
\fi \lgwella \fi 
{}\gg {}$}\quad
\parbox [t]{0.4\textwidth }{${\cal G} \Rightarrow \Pi~{\cal Y} . {\cal Y} \Rightarrow {\cal G}
$\hfill \makebox [0mm][l]{\quad \makebox[0mm]{$\Box$}}}
\gdef\lgwella{\relax}
\gdef\lgwellb{\relax}
\gdef\lgwellc{\relax}
\gdef\lgwelld{\relax}
\gdef\lgwelle{\relax}
\gdef\lgwellf{\relax}
\gdef\lgwellg{\relax}
\gdef\lgwellh{\relax}
\gdef\lgwelli{\relax}
\gdef\lgwellj{\relax}
\gdef\lgwellk{\relax}
\gdef\lgwelll{\relax}
\gdef\lgwellm{\relax}
\gdef\lgwelln{\relax}
\gdef\lgwello{\relax}
\gdef\lgwellp{\relax}
\gdef\lgwellq{\relax}
\gdef\lgwellr{\relax}
\gdef\lgwells{\relax}
\gdef\lgwellt{\relax}
\gdef\lgwellu{\relax}
\gdef\lgwellv{\relax}
\gdef\lgwellw{\relax}
\gdef\lgwellx{\relax}
\gdef\lgwelly{\relax}
\gdef\lgwellz{\relax}
\gdef\lgwellbiga{\relax}
\gdef\lgwellbigb{\relax}
\gdef\lgwellbigc{\relax}
\gdef\lgwellbigd{\relax}
\gdef\lgwellbige{\relax}
\gdef\lgwellbigf{\relax}
\gdef\lgwellbigg{\relax}
\gdef\lgwellbigh{\relax}
\gdef\lgwellbigi{\relax}
\gdef\lgwellbigj{\relax}
\gdef\lgwellbigk{\relax}
\gdef\lgwellbigl{\relax}
\gdef\lgwellbigm{\relax}
\gdef\lgwellbign{\relax}
\gdef\lgwellbigo{\relax}
\gdef\lgwellbigp{\relax}
\gdef\lgwellbigq{\relax}
\gdef\lgwellbigr{\relax}
\gdef\lgwellbigs{\relax}
\gdef\lgwellbigt{\relax}
\gdef\lgwellbigu{\relax}
\gdef\lgwellbigv{\relax}
\gdef\lgwellbigw{\relax}
\gdef\lgwellbigx{\relax}
\gdef\lgwellbigy{\relax}
\gdef\lgwellbigz{\relax}
\endgroup $

\section{First order predicate calculus}
%\begin{Def}[Term]
%A term is a metaiable, constant, or the result of acting on metaiables and constants by function symbols.
%\footnote{See: http://mathworld.wolfram.com/Term.html}
%\end{Def}

\section{Zermelo-Fraenkel Axioms}
Below we formally define the Zermelo-Frankel set theory.
Together with the \emph{axiom of choice} this is know
as \emph{ZFC}. Our definitions are based on those found
on mathworld.wolfram.com
$
[ \mathbf{Theory\ } 
\mbox{zfc}
]$



\begin{appendix}
\section{Pyk definitions}

\begin{flushleft}
$(
[
\ast  \Rightarrow 
\ast 
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}
\mbox {\tt \char34}
\linebreak [0]\ \hskip0em plus2.0em{}imply
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {\tt \char34}
\mbox{''}
]
\linebreak[4] 
[
\mbox{pred calc}
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}pred
\linebreak [0]\ \hskip0em plus2.0em{}calc
\mbox{''}
]
\linebreak[4] 
[
\mbox{pc1}
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}pc1
\mbox{''}
]
\linebreak[4] 
[
\mbox{pc2}
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}pc2
\mbox{''}
]
\linebreak[4] 
[
\mbox{pc3}
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}pc3
\mbox{''}
]
\linebreak[4] 
[
\mbox{pc4}
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}pc4
\mbox{''}
]
\linebreak[4] 
[
\mbox{pc5}
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}pc5
\mbox{''}
]
\linebreak[4] 
[
\mbox{pc6}
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}pc6
\mbox{''}
]
\linebreak[4] 
[
\mbox{pc7}
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}pc7
\mbox{''}
]
\linebreak[4] 
[
\mbox{pc8}
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}pc8
\mbox{''}
]
\linebreak[4] 
[
\mbox{pc9}
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}pc9
\mbox{''}
]
\linebreak[4] 
[
\mbox{pc10}
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}pc10
\mbox{''}
]
\linebreak[4] 
[
\mbox{pc11}
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}pc11
\mbox{''}
]
\linebreak[4] 
[
\mbox{pc12}
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}pc12
\mbox{''}
]
\linebreak[4] 
[
\mbox{pcmp}
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}pcmp
\mbox{''}
]
\linebreak[4] 
[
\mbox{pcia}
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}pcia
\mbox{''}
]
\linebreak[4] 
[
\mbox{pcie}
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}pcie
\mbox{''}
]
\linebreak[4] 
[\Pi~
\ast  . 
\ast 
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}forall
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {\tt \char34}
\linebreak [0]\ \hskip0em plus2.0em{}dot
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {\tt \char34}
\mbox{''}
]
\linebreak[4] 
[\Sigma~
\ast  . 
\ast 
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}exists
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {\tt \char34}
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {\tt \char34}
\mbox{''}
]
\linebreak[4] 
[\neg 
\ast 
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}lnot
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {\tt \char34}
\mbox{''}
]
\linebreak[4] 
[
\ast  \wedge 
\ast 
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}
\mbox {\tt \char34}
\linebreak [0]\ \hskip0em plus2.0em{}land
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {\tt \char34}
\mbox{''}
]
\linebreak[4] 
[
\ast  \vee 
\ast 
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}
\mbox {\tt \char34}
\linebreak [0]\ \hskip0em plus2.0em{}lor
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {\tt \char34}
\mbox{''}
]
\linebreak[4] 
[
\ast  \Leftrightarrow 
\ast 
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}
\mbox {\tt \char34}
\linebreak [0]\ \hskip0em plus2.0em{}bimply
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {\tt \char34}
\mbox{''}
]
\linebreak[4] 
[
\mbox{trivia}
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}trivia
\mbox{''}
]
\linebreak[4] 
[
\mbox{iatest}
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}iatest
\mbox{''}
]
\linebreak[4] 
[
\mbox{zfc}
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}zfc
\mbox{''}
]
\linebreak[4] 
[
\mbox{test}
\stackrel{
\mathrm{pyk}
}{\rightarrow}
\mbox{``}test
\mbox{''}
]
\linebreak[4] 
)^{\mathbf {p}}$
\end{flushleft}

\section{Tex definitions}
\begin{itemize}
\item $
[\neg 
\mathsf{x}
\stackrel {\mathrm {tex}}{=} 
\mbox{``}
\mbox {$\backslash $}neg
\linebreak [0]\ \hskip0em plus2.0em{}
\#1.
\mbox{''}
]$
\item $
[
\mathsf{x} \wedge 
\mathsf{y}
\stackrel {\mathrm {tex}}{=} 
\mbox{``}
\#1.
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}wedge
\linebreak [0]\ \hskip0em plus2.0em{}
\#2.
\mbox{''}
]$
\item $
[
\mathsf{x} \vee 
\mathsf{y}
\stackrel {\mathrm {tex}}{=} 
\mbox{``}
\#1.
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}vee
\linebreak [0]\ \hskip0em plus2.0em{}
\#2.
\mbox{''}
]$
\item $
[
\mathsf{x} \Rightarrow 
\mathsf{y}
\stackrel {\mathrm {tex}}{=} 
\mbox{``}
\#1.
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}Rightarrow
\linebreak [0]\ \hskip0em plus2.0em{}
\#2.
\mbox{''}
]$
\item $
[
\mathsf{x} \Leftrightarrow 
\mathsf{y}
\stackrel {\mathrm {tex}}{=} 
\mbox{``}
\#1.
\linebreak [0]\ \hskip0em plus2.0em{}
\mbox {$\backslash $}Leftrightarrow
\linebreak [0]\ \hskip0em plus2.0em{}
\#2.
\mbox{''}
]$
\item $
[\Pi~
\mathsf{y} . 
\mathsf {b}
\stackrel {\mathrm {tex}}{=} 
\mbox{``}
\mbox {$\backslash $}Pi
\char126 
\#1.
\linebreak [0]\ \hskip0em plus2.0em{}.
\linebreak [0]\ \hskip0em plus2.0em{}
\#2.
\mbox{''}
]$
\item $
[\Sigma~
\mathsf{y} . 
\mathsf {b}
\stackrel {\mathrm {tex}}{=} 
\mbox{``}
\mbox {$\backslash $}Sigma
\char126 
\#1.
\linebreak [0]\ \hskip0em plus2.0em{}.
\linebreak [0]\ \hskip0em plus2.0em{}
\#2.
\mbox{''}
]$
\end{itemize}

\section{Priority table}

\begin {flushleft}$
\mathbf{Priority\ table} 
\newline \mathbf {Preassociative} \newline 
[
\mbox{test}
] , \linebreak [0] 
[
\mbox{base}
] , \linebreak [0] 
[
\mbox{bracket $
\ast $ end bracket}
] , \linebreak [0] 
[
\mbox{big bracket $
\ast $ end bracket}
] , \linebreak [0] 
[
\ \$
\ast \$\linebreak[0]\ 
] , \linebreak [0] 
[
\mathbf{flush\ left\ }[ 
\ast 
]
] , \linebreak [0] 
[
\mathsf{x}
] , \linebreak [0] 
[
\mathsf{y}
] , \linebreak [0] 
[
\mathsf{z}
] , \linebreak [0] 
[
[
\ast 
\bowtie
\ast 
]
] , \linebreak [0] 
[
[
\ast 
\stackrel{
\ast 
}{\rightarrow}
\ast 
]
] , \linebreak [0] 
[
\mathrm{pyk}
] , \linebreak [0] 
[
\mathrm{tex}
] , \linebreak [0] 
[
\mathrm{name}
] , \linebreak [0] 
[
\mathrm{prio}
] , \linebreak [0] 
[
\ast 
] , \linebreak [0] 
[
\mathsf {T}
] , \linebreak [0] 
[
\mathrm {if}(
\ast 
,\linebreak [0]
\ast 
,\linebreak [0]
\ast 
)
] , \linebreak [0] 
[
[
\ast 
\stackrel {
\ast 
}{\Rightarrow }
\ast 
]
] , \linebreak [0] 
[
\mathrm {val}
] , \linebreak [0] 
[
\mathrm {claim}
] , \linebreak [0] 
[
\bot 
] , \linebreak [0] 
[
f(
\ast 
)
] , \linebreak [0] 
[
(
\ast 
){}^{I} 
] , \linebreak [0] 
[
\mathsf {F}
] , \linebreak [0] 
[
\underline {0}
] , \linebreak [0] 
[
\underline {1}
] , \linebreak [0] 
[
\underline {2}
] , \linebreak [0] 
[
\underline {3}
] , \linebreak [0] 
[
\underline {4}
] , \linebreak [0] 
[
\underline {5}
] , \linebreak [0] 
[
\underline {6}
] , \linebreak [0] 
[
\underline {7}
] , \linebreak [0] 
[
\underline {8}
] , \linebreak [0] 
[
\underline {9}
] , \linebreak [0] 
[
0
] , \linebreak [0] 
[
1
] , \linebreak [0] 
[
2
] , \linebreak [0] 
[
3
] , \linebreak [0] 
[
4
] , \linebreak [0] 
[
5
] , \linebreak [0] 
[
6
] , \linebreak [0] 
[
7
] , \linebreak [0] 
[
8
] , \linebreak [0] 
[
9
] , \linebreak [0] 
[
\mathsf {a}
] , \linebreak [0] 
[
\mathsf {b}
] , \linebreak [0] 
[
\mathsf {c}
] , \linebreak [0] 
[
\mathsf {d}
] , \linebreak [0] 
[
\mathsf {e}
] , \linebreak [0] 
[
\mathsf {f}
] , \linebreak [0] 
[
\mathsf {g}
] , \linebreak [0] 
[
\mathsf {h}
] , \linebreak [0] 
[
\mathsf {i}
] , \linebreak [0] 
[
\mathsf {j}
] , \linebreak [0] 
[
\mathsf {k}
] , \linebreak [0] 
[
\mathsf {l}
] , \linebreak [0] 
[
\mathsf {m}
] , \linebreak [0] 
[
\mathsf {n}
] , \linebreak [0] 
[
\mathsf {o}
] , \linebreak [0] 
[
\mathsf {p}
] , \linebreak [0] 
[
\mathsf {q}
] , \linebreak [0] 
[
\mathsf {r}
] , \linebreak [0] 
[
\mathsf {s}
] , \linebreak [0] 
[
\mathsf {t}
] , \linebreak [0] 
[
\mathsf {u}
] , \linebreak [0] 
[
\mathsf {v}
] , \linebreak [0] 
[
\mathsf {w}
] , \linebreak [0] 
[
(
\ast 
)^M
] , \linebreak [0] 
[
\mathrm {If}(
\ast 
,\linebreak [0]
\ast 
,\linebreak [0]
\ast 
)
] , \linebreak [0] 
[\mathrm {array}\{
\ast 
\}
\ast 
\mathrm {end\ array}
] , \linebreak [0] 
[
l
] , \linebreak [0] 
[
c
] , \linebreak [0] 
[
r
] , \linebreak [0] 
[
\mathrm {empty}
] , \linebreak [0] 
[
\langle 
\ast 
\,{|}
\ast 
{:=}\,
\ast 
\rangle 
] , \linebreak [0] 
[
{\cal M}(
\ast 
)
] , \linebreak [0] 
[
\tilde {{\cal U}}(
\ast 
)
] , \linebreak [0] 
[
{\cal U}(
\ast 
)
] , \linebreak [0] 
[
{\cal U}^M(
\ast 
)
] , \linebreak [0] 
[
\mathbf {apply}(
\ast 
,
\ast 
)
] , \linebreak [0] 
[
\mathbf {apply}_1(
\ast 
,
\ast 
)
] , \linebreak [0] 
[
identifier( 
\ast 
)
] , \linebreak [0] 
[
identifier_{1}( 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
array\mbox{-}\linebreak[0]plus( 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
array\mbox{-}\linebreak[0]remove( 
\ast 
, 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
array\mbox{-}\linebreak[0]put( 
\ast 
, 
\ast 
, 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
array\mbox{-}\linebreak[0]add( 
\ast 
, 
\ast 
, 
\ast 
, 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
bit( 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
bit_1( 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
rack
] , \linebreak [0] 
[
\mbox {\tt \char34}\mathrm {vector}\mbox {\tt \char34}
] , \linebreak [0] 
[
\mbox {\tt \char34}\mathrm {bibliography}\mbox {\tt \char34}
] , \linebreak [0] 
[
\mbox {\tt \char34}\mathrm {dictionary}\mbox {\tt \char34}
] , \linebreak [0] 
[
\mbox {\tt \char34}\mathrm {body}\mbox {\tt \char34}
] , \linebreak [0] 
[
\mbox {\tt \char34}\mathrm {codex}\mbox {\tt \char34}
] , \linebreak [0] 
[
\mbox {\tt \char34}\mathrm {expansion}\mbox {\tt \char34}
] , \linebreak [0] 
[
\mbox {\tt \char34}\mathrm {code}\mbox {\tt \char34}
] , \linebreak [0] 
[
\mbox {\tt \char34}\mathrm {cache}\mbox {\tt \char34}
] , \linebreak [0] 
[
\mbox {\tt \char34}\mathrm {diagnose}\mbox {\tt \char34}
] , \linebreak [0] 
[
\mbox {\tt \char34}\mathrm {pyk}\mbox {\tt \char34}
] , \linebreak [0] 
[
\mbox {\tt \char34}\mathrm {tex}\mbox {\tt \char34}
] , \linebreak [0] 
[
\mbox {\tt \char34}\mathrm {texname}\mbox {\tt \char34}
] , \linebreak [0] 
[
\mbox {\tt \char34}\mathrm {value}\mbox {\tt \char34}
] , \linebreak [0] 
[
\mbox {\tt \char34}\mathrm {message}\mbox {\tt \char34}
] , \linebreak [0] 
[
\mbox {\tt \char34}\mathrm {macro}\mbox {\tt \char34}
] , \linebreak [0] 
[
\mbox {\tt \char34}\mathrm {definition}\mbox {\tt \char34}
] , \linebreak [0] 
[
\mbox {\tt \char34}\mathrm {unpack}\mbox {\tt \char34}
] , \linebreak [0] 
[
\mbox {\tt \char34}\mathrm {claim}\mbox {\tt \char34}
] , \linebreak [0] 
[
\mbox {\tt \char34}\mathrm {priority}\mbox {\tt \char34}
] , \linebreak [0] 
[
\mbox {\tt \char34}\mathrm {lambda}\mbox {\tt \char34}
] , \linebreak [0] 
[
\mbox {\tt \char34}\mathrm {apply}\mbox {\tt \char34}
] , \linebreak [0] 
[
\mbox {\tt \char34}\mathrm {true}\mbox {\tt \char34}
] , \linebreak [0] 
[
\mbox {\tt \char34}\mathrm {if}\mbox {\tt \char34}
] , \linebreak [0] 
[
\mbox {\tt \char34}\mathrm {quote}\mbox {\tt \char34}
] , \linebreak [0] 
[
\mbox {\tt \char34}\mathrm {proclaim}\mbox {\tt \char34}
] , \linebreak [0] 
[
\mbox {\tt \char34}\mathrm {define}\mbox {\tt \char34}
] , \linebreak [0] 
[
\mbox {\tt \char34}\mathrm {introduce}\mbox {\tt \char34}
] , \linebreak [0] 
[
\mbox {\tt \char34}\mathrm {hide}\mbox {\tt \char34}
] , \linebreak [0] 
[
\mbox {\tt \char34}\mathrm {pre}\mbox {\tt \char34}
] , \linebreak [0] 
[
\mbox {\tt \char34}\mathrm {post}\mbox {\tt \char34}
] , \linebreak [0] 
[
{\cal E}(
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[
{\cal E}_2(
\ast 
,
\ast 
,
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[
{\cal E}_3(
\ast 
,
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[
{\cal E}_4(
\ast 
,
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[
\mathbf {lookup}(
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[
\mathbf {abstract}(
\ast 
,
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[
\lceil 
\ast 
\rceil 
] , \linebreak [0] 
[
{\cal M}(
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[
{\cal M}_2(
\ast 
,
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[
{\cal M}^*(
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[
\mathrm {macro}
] , \linebreak [0] 
[
s_0
] , \linebreak [0] 
[
\mathbf {zip}(
\ast 
,
\ast 
)
] , \linebreak [0] 
[
\mathbf {assoc}_1(
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[(
\ast 
)^{\mathbf {p}}
] , \linebreak [0] 
[
\mbox{self}
] , \linebreak [0] 
[
[
\ast 
\mathrel {\ddot {=}}
\ast 
]
] , \linebreak [0] 
[
[
\ast 
\mathrel {\dot {=}}
\ast 
]
] , \linebreak [0] 
[
[
\ast 
\mathrel {\acute {=}}
\ast 
]
] , \linebreak [0] 
[
[
\ast 
\stackrel {\mathrm {pyk}}{=} 
\ast 
]
] , \linebreak [0] 
[
[
\ast 
\stackrel {\mathrm {tex}}{=} 
\ast 
]
] , \linebreak [0] 
[
[
\ast 
\stackrel {\mathrm {name}}{=} 
\ast 
]
] , \linebreak [0] 
[
\mathbf{Priority\ table} [ 
\ast 
]
] , \linebreak [0] 
[
\tilde {{\cal M}}_1
] , \linebreak [0] 
[
\tilde {{\cal M}}_2(
\ast 
)
] , \linebreak [0] 
[
\tilde {{\cal M}}_3(
\ast 
)
] , \linebreak [0] 
[
\tilde {{\cal M}}_4(
\ast 
,
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[
\tilde {{\cal M}}(
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[
\tilde {{\cal Q}}(
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[
\tilde {{\cal Q}}_2(
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[
\tilde {{\cal Q}}_3(
\ast 
,
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[
\tilde {{\cal Q}}^*(
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[
(
\ast 
)
] , \linebreak [0] 
[
\left( 
\ast 
\right) 
] , \linebreak [0] 
[
display(
\ast 
)
] , \linebreak [0] 
[
statement(
\ast 
)
] , \linebreak [0] 
[
[
\ast 
]^{\cdot}
] , \linebreak [0] 
[
[
\ast 
]^-
] , \linebreak [0] 
[
\mathbf{aspect}( 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
\mathbf{aspect}( 
\ast 
, 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
\langle 
\ast 
\rangle 
] , \linebreak [0] 
[
\mathbf {tuple}_1( 
\ast 
) 
] , \linebreak [0] 
[
\mathbf {tuple}_2( 
\ast 
) 
] , \linebreak [0] 
[
let_2( 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
let_1( 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
[
\ast 
\stackrel {claim}{=}
\ast 
]
] , \linebreak [0] 
[
\mbox{checker}
] , \linebreak [0] 
[
\mathbf{check}( 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
\mathbf{check}_2( 
\ast 
, 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
\mathbf{check}_3( 
\ast 
, 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
\mathbf{check}^*( 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
\mathbf{check}^*_2( 
\ast 
, 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
\relax [ 
\ast 
\relax ]^{\cdot} 
] , \linebreak [0] 
[
\relax [ 
\ast 
\relax ]^{-} 
] , \linebreak [0] 
[
\relax [ 
\ast 
\relax ]^{\circ} 
] , \linebreak [0] 
[
msg
] , \linebreak [0] 
[
[
\ast 
\stackrel {msg}{=} 
\ast 
]
] , \linebreak [0] 
[
{<}stmt{>}
] , \linebreak [0] 
[
stmt
] , \linebreak [0] 
[
[
\ast 
\stackrel {stmt}{=}
\ast 
]
] , \linebreak [0] 
[
HeadNil'
] , \linebreak [0] 
[
HeadPair'
] , \linebreak [0] 
[
Transitivity'
] , \linebreak [0] 
[
{\makebox [0mm][l]{$\bot $}\,{\bot }}
] , \linebreak [0] 
[
Contra'
] , \linebreak [0] 
[
T'_{E}
] , \linebreak [0] 
[
L_{1}
] , \linebreak [0] 
[\underline{
\ast }
] , \linebreak [0] 
[{\cal A}
] , \linebreak [0] 
[{\cal B}
] , \linebreak [0] 
[{\cal C}
] , \linebreak [0] 
[{\cal D}
] , \linebreak [0] 
[{\cal E}
] , \linebreak [0] 
[{\cal F}
] , \linebreak [0] 
[{\cal G}
] , \linebreak [0] 
[{\cal H}
] , \linebreak [0] 
[{\cal I}
] , \linebreak [0] 
[{\cal J}
] , \linebreak [0] 
[{\cal K}
] , \linebreak [0] 
[{\cal L}
] , \linebreak [0] 
[{\cal M}
] , \linebreak [0] 
[{\cal N}
] , \linebreak [0] 
[{\cal O}
] , \linebreak [0] 
[{\cal P}
] , \linebreak [0] 
[{\cal Q}
] , \linebreak [0] 
[{\cal R}
] , \linebreak [0] 
[{\cal S}
] , \linebreak [0] 
[{\cal T}
] , \linebreak [0] 
[{\cal U}
] , \linebreak [0] 
[{\cal V}
] , \linebreak [0] 
[{\cal W}
] , \linebreak [0] 
[{\cal X}
] , \linebreak [0] 
[{\cal Y}
] , \linebreak [0] 
[{\cal Z}
] , \linebreak [0] 
[
\langle 
\ast 
\,{\protect\vert}
\ast 
{:=}\,
\ast 
\rangle 
] , \linebreak [0] 
[
\langle ^ { \ast } 
\ast 
\,{\protect\vert}
\ast 
{:=}\,
\ast 
\rangle 
] , \linebreak [0] 
[
\emptyset 
] , \linebreak [0] 
[
Remainder
] , \linebreak [0] 
[
( 
\ast 
)^{\bf v}
] , \linebreak [0] 
[
intro(
\ast 
,
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[
intro(
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[
error(
\ast 
,
\ast 
)
] , \linebreak [0] 
[
error_{2}(
\ast 
,
\ast 
)
] , \linebreak [0] 
[
proof( 
\ast 
, 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
proof_{2}( 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
{\cal S}(
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
{\cal S}^{I}(
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
{\cal S}^{\rhd}(
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
{\cal S}_{1}^{\rhd}(
\ast 
, 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
{\cal S}^{E}(
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
{\cal S}_{1}^{E}(
\ast 
, 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
{\cal S}^{+}(
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
{\cal S}_{1}^{+}(
\ast 
, 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
{\cal S}^{-}(
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
{\cal S}_{1}^{-}(
\ast 
, 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
{\cal S}^{\ast}(
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
{\cal S}_{1}^{\ast}(
\ast 
, 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
{\cal S}_{2}^{\ast}(
\ast 
, 
\ast 
, 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
{\cal S}^{\char64}(
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
{\cal S}_{1}^{\char64}(
\ast 
, 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
{\cal S}^{\vdash}(
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
{\cal S}_{1}^{\vdash}(
\ast 
, 
\ast 
, 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
{\cal S}^{\makebox [0mm][l]{\scriptsize $\vdash $}\,{\vdash }}(
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
{\cal S}_{1}^{\makebox [0mm][l]{\scriptsize $\vdash $}\,{\vdash }}(
\ast 
, 
\ast 
, 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
{\cal S}^{i.e.}(
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
{\cal S}_{1}^{i.e.}(
\ast 
, 
\ast 
, 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
{\cal S}_{2}^{i.e.}(
\ast 
, 
\ast 
, 
\ast 
, 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
{\cal S}^{\forall}(
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
{\cal S}_{1}^{\forall}(
\ast 
, 
\ast 
, 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
{\cal S}^{;}(
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
{\cal S}_{1}^{;}(
\ast 
, 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
{\cal S}_{2}^{;}(
\ast 
, 
\ast 
, 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
{\cal T}( 
\ast 
)
] , \linebreak [0] 
[
claims( 
\ast 
, 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
claims_2( 
\ast 
, 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
{<}proof{>}
] , \linebreak [0] 
[
proof
] , \linebreak [0] 
[
[ \mathbf{Lemma\ } 
\ast 
\colon 
\ast 
]
] , \linebreak [0] 
[
[ \mathbf{Proof\ of\ }
\ast 
\colon 
\ast 
]
] , \linebreak [0] 
[
[ 
\ast 
\mathbf{\ lemma\ } 
\ast 
\colon 
\ast 
]
] , \linebreak [0] 
[
[ 
\ast 
\mathbf{\ antilemma\ } 
\ast 
\colon 
\ast 
]
] , \linebreak [0] 
[
[ 
\ast 
\mathbf{\ rule\ } 
\ast 
\colon 
\ast 
]
] , \linebreak [0] 
[
[ 
\ast 
\mathbf{\ antirule\ } 
\ast 
\colon 
\ast 
]
] , \linebreak [0] 
[
\mbox{verifier}
] , \linebreak [0] 
[
{\cal V}_1( 
\ast 
)
] , \linebreak [0] 
[
{\cal V}_2( 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
{\cal V}_3( 
\ast 
, 
\ast 
, 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
{\cal V}_4( 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
{\cal V}_5( 
\ast 
, 
\ast 
, 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
{\cal V}_6( 
\ast 
, 
\ast 
, 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
{\cal V}_7( 
\ast 
, 
\ast 
, 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
Cut( 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
Head_{\oplus} ( 
\ast 
)
] , \linebreak [0] 
[
Tail_{\oplus} ( 
\ast 
)
] , \linebreak [0] 
[
rule_1( 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
rule( 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
Rule\ tactic
] , \linebreak [0] 
[
Plus( 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
[ \mathbf{Theory\ } 
\ast 
]
] , \linebreak [0] 
[
theory_2( 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
theory_3( 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
theory_4( 
\ast 
, 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
HeadNil''
] , \linebreak [0] 
[
HeadPair''
] , \linebreak [0] 
[
Transitivity''
] , \linebreak [0] 
[
Contra''
] , \linebreak [0] 
[
HeadNil
] , \linebreak [0] 
[
HeadPair
] , \linebreak [0] 
[
Transitivity
] , \linebreak [0] 
[
Contra
] , \linebreak [0] 
[
T_E
] , \linebreak [0] 
[
ragged\ right
] , \linebreak [0] 
[
ragged\ right\ expansion\ 
] , \linebreak [0] 
[
parm(
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[
parm^*(
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[
inst(
\ast 
,
\ast 
)
] , \linebreak [0] 
[
inst^*(
\ast 
,
\ast 
)
] , \linebreak [0] 
[
occur(
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[
occur^*(
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[
unify(
\ast 
=
\ast 
,
\ast 
)
] , \linebreak [0] 
[
unify^*(
\ast 
=
\ast 
,
\ast 
)
] , \linebreak [0] 
[
unify_2(
\ast 
=
\ast 
,
\ast 
)
] , \linebreak [0] 
[L_a
] , \linebreak [0] 
[L_b
] , \linebreak [0] 
[L_c
] , \linebreak [0] 
[L_d
] , \linebreak [0] 
[L_e
] , \linebreak [0] 
[L_f
] , \linebreak [0] 
[L_g
] , \linebreak [0] 
[L_h
] , \linebreak [0] 
[L_i
] , \linebreak [0] 
[L_j
] , \linebreak [0] 
[L_k
] , \linebreak [0] 
[L_l
] , \linebreak [0] 
[L_m
] , \linebreak [0] 
[L_n
] , \linebreak [0] 
[L_o
] , \linebreak [0] 
[L_p
] , \linebreak [0] 
[L_q
] , \linebreak [0] 
[L_r
] , \linebreak [0] 
[L_s
] , \linebreak [0] 
[L_t
] , \linebreak [0] 
[L_u
] , \linebreak [0] 
[L_v
] , \linebreak [0] 
[L_w
] , \linebreak [0] 
[L_x
] , \linebreak [0] 
[L_y
] , \linebreak [0] 
[L_z
] , \linebreak [0] 
[L_A
] , \linebreak [0] 
[L_B
] , \linebreak [0] 
[L_C
] , \linebreak [0] 
[L_D
] , \linebreak [0] 
[L_E
] , \linebreak [0] 
[L_F
] , \linebreak [0] 
[L_G
] , \linebreak [0] 
[L_H
] , \linebreak [0] 
[L_I
] , \linebreak [0] 
[L_J
] , \linebreak [0] 
[L_K
] , \linebreak [0] 
[L_L
] , \linebreak [0] 
[L_M
] , \linebreak [0] 
[L_N
] , \linebreak [0] 
[L_O
] , \linebreak [0] 
[L_P
] , \linebreak [0] 
[L_Q
] , \linebreak [0] 
[L_R
] , \linebreak [0] 
[L_S
] , \linebreak [0] 
[L_T
] , \linebreak [0] 
[L_U
] , \linebreak [0] 
[L_V
] , \linebreak [0] 
[L_W
] , \linebreak [0] 
[L_X
] , \linebreak [0] 
[L_Y
] , \linebreak [0] 
[L_Z
] , \linebreak [0] 
[L_?
] , \linebreak [0] 
[
Reflexivity
] , \linebreak [0] 
[
Reflexivity_1
] , \linebreak [0] 
[
Commutativity
] , \linebreak [0] 
[
Commutativity_1
] , \linebreak [0] 
[
{<}tactic{>}
] , \linebreak [0] 
[
tactic
] , \linebreak [0] 
[
[
\ast 
\stackrel {tactic}{=}
\ast 
]
] , \linebreak [0] 
[
{\cal P}( 
\ast 
, 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
{\cal P}^*( 
\ast 
, 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
p_0
] , \linebreak [0] 
[
conclude_1 ( 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
conclude_2 ( 
\ast 
, 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
conclude_3 ( 
\ast 
, 
\ast 
, 
\ast 
, 
\ast 
)
] , \linebreak [0] 
[
conclude_4 ( 
\ast 
, 
\ast 
)
]
; 
\newline \mathbf {Preassociative} \newline 
[
\ast 
\_\{
\ast 
\}
] , \linebreak [0] 
[
\ast 
/indexintro(
\ast 
,
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[
\ast 
/intro(
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[
\ast 
/bothintro(
\ast 
,
\ast 
,
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[
\ast 
/nameintro(
\ast 
,
\ast 
,
\ast 
,
\ast 
)
] , \linebreak [0] 
[
\ast '
] , \linebreak [0] 
[
\ast 
{[}
\ast 
{]}
] , \linebreak [0] 
[
\ast 
[ 
\ast 
{\rightarrow} 
\ast 
]
] , \linebreak [0] 
[
\ast 
[ 
\ast 
{\Rightarrow} 
\ast 
]
] , \linebreak [0] 
[
\ast 
0
] , \linebreak [0] 
[
\ast 
1
] , \linebreak [0] 
[
0 \mathrm {b}
] , \linebreak [0] 
[
\ast 
\mbox {-color}( 
\ast 
)
] , \linebreak [0] 
[
\ast 
\mbox {-color}^{\ast}( 
\ast 
)
] , \linebreak [0] 
[
\ast 
{}^H
] , \linebreak [0] 
[
\ast 
{}^T
] , \linebreak [0] 
[
\ast 
{}^U
] , \linebreak [0] 
[
\ast 
{}^h
] , \linebreak [0] 
[
\ast 
{}^t
] , \linebreak [0] 
[
\ast 
{}^s
] , \linebreak [0] 
[
\ast 
{}^c
] , \linebreak [0] 
[
\ast 
{}^d
] , \linebreak [0] 
[
\ast 
{}^a
] , \linebreak [0] 
[
\ast 
{}^C
] , \linebreak [0] 
[
\ast 
{}^M
] , \linebreak [0] 
[
\ast 
{}^B
] , \linebreak [0] 
[
\ast 
{}^{r}
] , \linebreak [0] 
[
\ast 
{}^{i}
] , \linebreak [0] 
[
\ast 
{}^{d}
] , \linebreak [0] 
[
\ast 
{}^{R}
] , \linebreak [0] 
[
\ast 
{}^{0}
] , \linebreak [0] 
[
\ast 
{}^{1}
] , \linebreak [0] 
[
\ast 
{}^{2}
] , \linebreak [0] 
[
\ast 
{}^{3}
] , \linebreak [0] 
[
\ast 
{}^{4}
] , \linebreak [0] 
[
\ast 
{}^{5}
] , \linebreak [0] 
[
\ast 
{}^{6}
] , \linebreak [0] 
[
\ast 
{}^{7}
] , \linebreak [0] 
[
\ast 
{}^{8}
] , \linebreak [0] 
[
\ast 
{}^{9}
] , \linebreak [0] 
[
\ast 
{} ^ { E }
] , \linebreak [0] 
[
\ast 
{} ^ {\cal V}
] , \linebreak [0] 
[
\ast 
{} ^ {\cal C}
] , \linebreak [0] 
[
\ast 
{} ^ {{\cal C} ^ { \ast }}
]
; 
\newline \mathbf {Preassociative} \newline 
[
\mbox{``}
\ast 
\mbox{''}
] , \linebreak [0] 
[
] , \linebreak [0] 
[
(
\ast 
)^{\bf t}
] , \linebreak [0] 
[
\mbox{string}(
\ast 
)+
\ast 
] , \linebreak [0] 
[\mbox{string}(
\ast 
)\mathrel{++}
\ast 
] , \linebreak [0] 
[
\newline 
\ast 
] , \linebreak [0] 
[
\linebreak [0]\ \hskip0em plus2.0em{}
\ast 
] , \linebreak [0] 
[!
\ast 
] , \linebreak [0] 
[
\mbox {\tt \char34}
\ast 
] , \linebreak [0] 
[
\#
\ast 
] , \linebreak [0] 
[
\$
\ast 
] , \linebreak [0] 
[
\%
\ast 
] , \linebreak [0] 
[
\&
\ast 
] , \linebreak [0] 
[
\mbox {'}
\ast 
] , \linebreak [0] 
[(
\ast 
] , \linebreak [0] 
[)
\ast 
] , \linebreak [0] 
[
{*}
\ast 
] , \linebreak [0] 
[
{+}
\ast 
] , \linebreak [0] 
[,
\ast 
] , \linebreak [0] 
[
\mbox{-}
\ast 
] , \linebreak [0] 
[.
\ast 
] , \linebreak [0] 
[/
\ast 
] , \linebreak [0] 
[0
\ast 
] , \linebreak [0] 
[1
\ast 
] , \linebreak [0] 
[2
\ast 
] , \linebreak [0] 
[3
\ast 
] , \linebreak [0] 
[4
\ast 
] , \linebreak [0] 
[5
\ast 
] , \linebreak [0] 
[6
\ast 
] , \linebreak [0] 
[7
\ast 
] , \linebreak [0] 
[8
\ast 
] , \linebreak [0] 
[9
\ast 
] , \linebreak [0] 
[
{:}
\ast 
] , \linebreak [0] 
[;
\ast 
] , \linebreak [0] 
[
{<}
\ast 
] , \linebreak [0] 
[
{=}
\ast 
] , \linebreak [0] 
[
{>}
\ast 
] , \linebreak [0] 
[?
\ast 
] , \linebreak [0] 
[@
\ast 
] , \linebreak [0] 
[A
\ast 
] , \linebreak [0] 
[B
\ast 
] , \linebreak [0] 
[C
\ast 
] , \linebreak [0] 
[D
\ast 
] , \linebreak [0] 
[E
\ast 
] , \linebreak [0] 
[F
\ast 
] , \linebreak [0] 
[G
\ast 
] , \linebreak [0] 
[H
\ast 
] , \linebreak [0] 
[I
\ast 
] , \linebreak [0] 
[J
\ast 
] , \linebreak [0] 
[K
\ast 
] , \linebreak [0] 
[L
\ast 
] , \linebreak [0] 
[M
\ast 
] , \linebreak [0] 
[N
\ast 
] , \linebreak [0] 
[O
\ast 
] , \linebreak [0] 
[P
\ast 
] , \linebreak [0] 
[Q
\ast 
] , \linebreak [0] 
[R
\ast 
] , \linebreak [0] 
[S
\ast 
] , \linebreak [0] 
[T
\ast 
] , \linebreak [0] 
[U
\ast 
] , \linebreak [0] 
[V
\ast 
] , \linebreak [0] 
[W
\ast 
] , \linebreak [0] 
[X
\ast 
] , \linebreak [0] 
[Y
\ast 
] , \linebreak [0] 
[Z
\ast 
] , \linebreak [0] 
[[
\ast 
] , \linebreak [0] 
[
\mbox {$\backslash $}
\ast 
] , \linebreak [0] 
[]
\ast 
] , \linebreak [0] 
[
{\char94}
\ast 
] , \linebreak [0] 
[
\_
\ast 
] , \linebreak [0] 
[
\mbox {`}
\ast 
] , \linebreak [0] 
[a
\ast 
] , \linebreak [0] 
[b
\ast 
] , \linebreak [0] 
[c
\ast 
] , \linebreak [0] 
[d
\ast 
] , \linebreak [0] 
[e
\ast 
] , \linebreak [0] 
[f
\ast 
] , \linebreak [0] 
[g
\ast 
] , \linebreak [0] 
[h
\ast 
] , \linebreak [0] 
[i
\ast 
] , \linebreak [0] 
[j
\ast 
] , \linebreak [0] 
[k
\ast 
] , \linebreak [0] 
[l
\ast 
] , \linebreak [0] 
[m
\ast 
] , \linebreak [0] 
[n
\ast 
] , \linebreak [0] 
[o
\ast 
] , \linebreak [0] 
[p
\ast 
] , \linebreak [0] 
[q
\ast 
] , \linebreak [0] 
[r
\ast 
] , \linebreak [0] 
[s
\ast 
] , \linebreak [0] 
[t
\ast 
] , \linebreak [0] 
[u
\ast 
] , \linebreak [0] 
[v
\ast 
] , \linebreak [0] 
[w
\ast 
] , \linebreak [0] 
[x
\ast 
] , \linebreak [0] 
[y
\ast 
] , \linebreak [0] 
[z
\ast 
] , \linebreak [0] 
[
\{
\ast 
] , \linebreak [0] 
[|
\ast 
] , \linebreak [0] 
[
\}
\ast 
] , \linebreak [0] 
[
\char126 
\ast 
] , \linebreak [0] 
[
\mathbf{Preassociative}\,
\ast 
; 
\ast 
] , \linebreak [0] 
[
\mathbf{Postassociative}\,
\ast 
; 
\ast 
] , \linebreak [0] 
[
[
\ast 
] , \linebreak [0] 
\ast 
] , \linebreak [0] 
[
\mathrm{priority} \,
\ast 
\, \mathrm{end}
] , \linebreak [0] 
[
newline\ 
\ast 
] , \linebreak [0] 
[
macro\ newline\ 
\ast 
]
; 
\newline \mathbf {Preassociative} \newline 
[
\ast 
\mathbin {\mbox {'}}
\ast 
] , \linebreak [0] 
[
\ast 
\mathbin {\mbox {`}}
\ast 
]
; 
\newline \mathbf {Preassociative} \newline 
[
\ast 
\cdot 
\ast 
] , \linebreak [0] 
[
\ast 
\cdot_0 
\ast 
]
; 
\newline \mathbf {Preassociative} \newline 
[
\ast 
+ 
\ast 
] , \linebreak [0] 
[
\ast 
\mathop{+_0} 
\ast 
] , \linebreak [0] 
[
\ast 
\mathop{+_1} 
\ast 
] , \linebreak [0] 
[
\ast 
- 
\ast 
] , \linebreak [0] 
[
\ast 
\mathop{-_0} 
\ast 
] , \linebreak [0] 
[
\ast 
\mathop{-_1} 
\ast 
]
; 
\newline \mathbf {Preassociative} \newline 
[
\ast 
\cup \{ 
\ast 
\}
] , \linebreak [0] 
[
\ast 
\cup 
\ast 
] , \linebreak [0] 
[
\ast 
\backslash \{ 
\ast 
\}
]
; 
\newline\mathbf{Postassociative} \newline 
[
\ast 
\mathrel { \dot { . \, . } }
\ast 
] , \linebreak [0] 
[
\ast 
\mathrel { \underline { \dot { . \, . } } }
\ast 
] , \linebreak [0] 
[
\ast 
\mathrel { \underline { : \, : } }
\ast 
] , \linebreak [0] 
[
\ast 
\mathrel { \underline { {+} 2 \ast } }
\ast 
] , \linebreak [0] 
[
\ast 
\mathrel { : \, : }
\ast 
] , \linebreak [0] 
[
\ast 
\mathrel { {+} 2 \ast }
\ast 
]
; 
\newline\mathbf{Postassociative} \newline 
[
\ast 
,\linebreak [0] 
\ast 
]
; 
\newline \mathbf {Preassociative} \newline 
[
\ast 
\stackrel {B}{\approx }
\ast 
] , \linebreak [0] 
[
\ast 
\stackrel {D}{\approx }
\ast 
] , \linebreak [0] 
[
\ast 
\stackrel {C}{\approx }
\ast 
] , \linebreak [0] 
[
\ast 
\stackrel {P}{\approx }
\ast 
] , \linebreak [0] 
[
\ast 
\approx 
\ast 
] , \linebreak [0] 
[
\ast 
=
\ast 
] , \linebreak [0] 
[
\ast 
\stackrel {+}{\rightarrow }
\ast 
] , \linebreak [0] 
[
\ast 
\stackrel {t}{=}
\ast 
] , \linebreak [0] 
[
\ast 
\stackrel {t^*}{=}
\ast 
] , \linebreak [0] 
[
\ast 
\stackrel{r}{=} 
\ast 
] , \linebreak [0] 
[
\ast 
\in_t 
\ast 
] , \linebreak [0] 
[
\ast 
\subseteq_T 
\ast 
] , \linebreak [0] 
[
\ast 
\stackrel{T}{=} 
\ast 
] , \linebreak [0] 
[
\ast 
\stackrel{s}{=} 
\ast 
] , \linebreak [0] 
[
\ast 
\mathrel {free\ in} 
\ast 
] , \linebreak [0] 
[
\ast 
\mathrel {free\ in}^{\ast} 
\ast 
] , \linebreak [0] 
[
\ast 
\mathrel {free\ for} 
\ast 
\mathrel {in} 
\ast 
] , \linebreak [0] 
[
\ast 
\mathrel {free\ for}^{\ast} 
\ast 
\mathrel {in} 
\ast 
] , \linebreak [0] 
[
\ast 
\in_c 
\ast 
] , \linebreak [0] 
[
\ast 
< 
\ast 
] , \linebreak [0] 
[
\ast 
<' 
\ast 
] , \linebreak [0] 
[
\ast 
\le' 
\ast 
]
; 
\newline \mathbf {Preassociative} \newline 
[
{\neg }
\ast 
]
; 
\newline \mathbf {Preassociative} \newline 
[
\ast 
\wedge 
\ast 
] , \linebreak [0] 
[
\ast 
\mathrel{\ddot{\wedge}} 
\ast 
] , \linebreak [0] 
[
\ast 
\mathrel{\tilde{\wedge}} 
\ast 
] , \linebreak [0] 
[
\ast 
\wedge_c 
\ast 
]
; 
\newline \mathbf {Preassociative} \newline 
[
\ast 
\vee 
\ast 
] , \linebreak [0] 
[
\ast 
\parallel 
\ast 
] , \linebreak [0] 
[
\ast 
\mathrel{\ddot{\vee}} 
\ast 
]
; 
\newline\mathbf{Postassociative} \newline 
[
\ast 
\mathrel{\ddot{\Rightarrow}} 
\ast 
] , \linebreak [0] 
[
\ast  \Rightarrow 
\ast 
]
; 
\newline\mathbf{Postassociative} \newline 
[
\ast 
:
\ast 
] , \linebreak [0] 
[
\ast 
\mathrel{spy}
\ast 
] , \linebreak [0] 
[
\ast 
!
\ast 
]
; 
\newline \mathbf {Preassociative} \newline 
[
\ast 
\left\{\protect \begin {array}{l}
\ast 
\\
\ast 
\protect \end {array}\right.
]
; 
\newline \mathbf {Preassociative} \newline 
[
\lambda 
\ast 
.
\ast 
] , \linebreak [0] 
[
\Lambda 
\ast 
. 
\ast 
] , \linebreak [0] 
[
\Lambda 
\ast 
] , \linebreak [0] 
[
{\bf if} \ 
\ast 
\ {\bf then} \ 
\ast 
\ {\bf else} \ 
\ast 
] , \linebreak [0] 
[
\mathbf{let\ } 
\ast 
= 
\ast 
\mathbf{\ in\ } 
\ast 
] , \linebreak [0] 
[
\mathbf{let\ } 
\ast 
\mathrel{\ddot{=}} 
\ast 
\mathrel{\ in\ } 
\ast 
]
; 
\newline \mathbf {Preassociative} \newline 
[
\ast 
{} ^ { I }
] , \linebreak [0] 
[
\ast 
{} ^ { \rhd }
] , \linebreak [0] 
[
\ast 
{} ^ { V } 
] , \linebreak [0] 
[
\ast 
{} ^ { + } 
] , \linebreak [0] 
[
\ast 
{} ^ { - } 
] , \linebreak [0] 
[
\ast 
{} ^ { \ast } 
]
; 
\newline \mathbf {Preassociative} \newline 
[
\ast 
\mathop {\char64} 
\ast 
] , \linebreak [0] 
[
\ast 
\rhd 
\ast 
] , \linebreak [0] 
[
\ast 
\mathrel {\makebox [0mm][l]{$\rhd $}\,{\rhd }} 
\ast 
] , \linebreak [0] 
[
\ast 
\gg 
\ast 
]
; 
\newline\mathbf{Postassociative} \newline 
[
\ast 
\vdash 
\ast 
] , \linebreak [0] 
[
\ast 
\mathrel {\makebox [0mm][l]{$\vdash $}\,{\vdash }} 
\ast 
] , \linebreak [0] 
[
\ast 
\mathrel {i.e.} 
\ast 
]
; 
\newline \mathbf {Preassociative} \newline 
[
\forall 
\ast 
\colon 
\ast 
]
; 
\newline\mathbf{Postassociative} \newline 
[
\ast 
\mathrel {\oplus} 
\ast 
]
; 
\newline\mathbf{Postassociative} \newline 
[
\ast 
; 
\ast 
]
; 
\newline \mathbf {Preassociative} \newline 
[
\ast 
\ proves\ 
\ast 
]
; 
\newline \mathbf {Preassociative} \newline 
[
\ast 
\mathbf{\ proof\ of\ } 
\ast 
: 
\ast 
] , \linebreak [0] 
[
Line \, 
\ast 
: 
\ast 
\gg 
\ast 
; 
\ast 
] , \linebreak [0] 
[
Last\ line \, 
\ast 
\gg 
\ast 
\,\Box
] , \linebreak [0] 
[
Line \, 
\ast 
: Premise \gg 
\ast 
;
\ast 
] , \linebreak [0] 
[
Line \, 
\ast 
: \mbox{Side-condition} \gg 
\ast 
; 
\ast 
] , \linebreak [0] 
[
Arbitrary \gg 
\ast 
;
\ast 
] , \linebreak [0] 
[
Local \gg 
\ast 
= 
\ast 
; 
\ast 
]
; 
\newline\mathbf{Postassociative} \newline 
[
\ast 
\mathrel{\mathrm{,}}
\ast 
] , \linebreak [0] 
[
\ast 
{[}
\ast 
{]}
\ast 
]
; 
\newline \mathbf {Preassociative} \newline 
[
\ast 
\& 
\ast 
]
; 
\newline \mathbf {Preassociative} \newline 
[
\ast 
\backslash \backslash 
\ast 
] , \linebreak [0] 
[
\ast 
\mathrel{linebreak[4]} 
\ast 
]
; 
\newline \mathbf {Preassociative} \newline 
[
\mbox{pred calc}
] , \linebreak [0] 
[
\mbox{pc1}
] , \linebreak [0] 
[
\mbox{pc2}
] , \linebreak [0] 
[
\mbox{pc3}
] , \linebreak [0] 
[
\mbox{pc4}
] , \linebreak [0] 
[
\mbox{pc5}
] , \linebreak [0] 
[
\mbox{pc6}
] , \linebreak [0] 
[
\mbox{pc7}
] , \linebreak [0] 
[
\mbox{pc8}
] , \linebreak [0] 
[
\mbox{pc9}
] , \linebreak [0] 
[
\mbox{pc10}
] , \linebreak [0] 
[
\mbox{pc11}
] , \linebreak [0] 
[
\mbox{pc12}
] , \linebreak [0] 
[
\mbox{pcmp}
] , \linebreak [0] 
[
\mbox{pcia}
] , \linebreak [0] 
[
\mbox{pcie}
]
; 
\newline\mathbf{Postassociative} \newline 
[\Pi~
\ast  . 
\ast 
] , \linebreak [0] 
[\Sigma~
\ast  . 
\ast 
]
; 
\newline \mathbf {Preassociative} \newline 
[\neg 
\ast 
]
; 
\newline \mathbf {Preassociative} \newline 
[
\ast  \wedge 
\ast 
]
; 
\newline \mathbf {Preassociative} \newline 
[
\ast  \vee 
\ast 
]
; 
\newline \mathbf {Preassociative} \newline 
[
\ast  \Leftrightarrow 
\ast 
]
; 
\newline \mathbf {Preassociative} \newline 
[
\mbox{trivia}
] , \linebreak [0] 
[
\mbox{iatest}
]
; 
\newline \mathbf {Preassociative} \newline 
[
\mbox{zfc}
]
; 
\mathbf{End\ table}$
\end {flushleft}
\end{appendix}

\end{document}
