\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 kvanti}

\hypersetup{colorlinks=true}

\everymath{\rm}

\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 kvanti$}}

\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}{510}
\newlength{\aritylength}
\settowidth{\aritylength}{99}
\vspace{2ex}
\makebox[\idlength][r]{0}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm kvanti$

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

\makebox[\idlength][r]{2}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm UniqueMember(Type)$

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

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

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

\makebox[\idlength][r]{6}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm Qclosed(Addition)$

\makebox[\idlength][r]{7}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm Qclosed(Multiplication)$

\makebox[\idlength][r]{8}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm FromCartProd(1)$

\makebox[\idlength][r]{9}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
\mbox{1rule fromCartProd(2)}$

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

\makebox[\idlength][r]{11}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm cartProd(\ast
)$

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

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

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

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

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

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

\makebox[\idlength][r]{18}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm (\cdots{})$

\makebox[\idlength][r]{19}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm \texttt{Objekt-var}$

\makebox[\idlength][r]{20}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm \texttt{Ex-var}$

\makebox[\idlength][r]{21}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm \texttt{Ph-var}$

\makebox[\idlength][r]{22}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm \texttt{V\ae{}rdi}$

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

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

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

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

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

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

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

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

\makebox[\idlength][r]{31}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{3}%
\makebox[0.5em]{}%
$\rm Dedu_{s}(\ast
,\ast
,\ast
)$

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

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

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

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

\makebox[\idlength][r]{36}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{4}%
\makebox[0.5em]{}%
$\rm 
Dedu_4^*(\ast
,\ast
,\ast
,\ast
)$

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

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

\makebox[\idlength][r]{39}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{4}%
\makebox[0.5em]{}%
$\rm 
Dedu_6^*(\ast
,\ast
,\ast
,\ast
)$

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

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

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

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

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

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

\makebox[\idlength][r]{46}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm Ex_{10}$

\makebox[\idlength][r]{47}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm Ex_{20}$

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

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

\makebox[\idlength][r]{50}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{4}%
\makebox[0.5em]{}%
$\rm \langle \ast
{\equiv} \ast
| \ast
{:==} \ast
\rangle_{Ex} $

\makebox[\idlength][r]{51}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{4}%
\makebox[0.5em]{}%
$\rm \langle \ast
{\equiv}^0 \ast
| \ast
{:==} \ast
\rangle_{Ex} $

\makebox[\idlength][r]{52}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{4}%
\makebox[0.5em]{}%
$\rm \langle \ast
{\equiv}^1 \ast
| \ast
{:==} \ast
\rangle_{Ex} $

\makebox[\idlength][r]{53}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{4}%
\makebox[0.5em]{}%
$\rm \langle \ast
{\equiv}^* \ast
| \ast
{:==} \ast
\rangle_{Ex} $

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

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

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

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

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

\makebox[\idlength][r]{59}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{4}%
\makebox[0.5em]{}%
$\rm \langle \ast
{\equiv} \ast
| \ast
{:==} \ast
\rangle_{Ph} $

\makebox[\idlength][r]{60}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{4}%
\makebox[0.5em]{}%
$\rm \langle \ast
{\equiv}^0 \ast
| \ast
{:==} \ast
\rangle_{Ph} $

\makebox[\idlength][r]{61}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{4}%
\makebox[0.5em]{}%
$\rm \langle \ast
{\equiv}^1 \ast
| \ast
{:==} \ast
\rangle_{Ph} $

\makebox[\idlength][r]{62}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{4}%
\makebox[0.5em]{}%
$\rm \langle \ast
{\equiv}^* \ast
| \ast
{:==} \ast
\rangle_{Ph} $

\makebox[\idlength][r]{63}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{4}%
\makebox[0.5em]{}%
$\rm \langle \ast
{\equiv} \ast
| \ast
{:==} \ast
\rangle_{Me}$

\makebox[\idlength][r]{64}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{4}%
\makebox[0.5em]{}%
$\rm \langle \ast
{\equiv}^1 \ast
| \ast
{:==} \ast
\rangle_{Me} $

\makebox[\idlength][r]{65}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{4}%
\makebox[0.5em]{}%
$\rm \langle \ast
{\equiv}^* \ast
| \ast
{:==} \ast
\rangle_{Me} $

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

\makebox[\idlength][r]{117}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm (Switch)HelperPowerIsSub$

\makebox[\idlength][r]{118}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm (Switch)PowerIsSub$

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

\makebox[\idlength][r]{120}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm HelperToSetEquality(t)$

\makebox[\idlength][r]{121}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm ToSetEquality(t)$

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

\makebox[\idlength][r]{139}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm ==\!{}Symmetry$

\makebox[\idlength][r]{140}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm Helper\!{}==\!{}Transitivity$

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

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

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

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

\makebox[\idlength][r]{145}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm Helper(2)PairSubset$

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

\makebox[\idlength][r]{164}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm Helper(2)NoneEqNecessary$

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

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

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

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

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

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

\makebox[\idlength][r]{171}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm Union(BS/R)subset$

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

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

\makebox[\idlength][r]{174}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm (x1)$

\makebox[\idlength][r]{175}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm (x2)$

\makebox[\idlength][r]{176}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm (y1)$

\makebox[\idlength][r]{177}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm (y2)$

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

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

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

\makebox[\idlength][r]{181}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm (v4)$

\makebox[\idlength][r]{182}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm (v2n)$

\makebox[\idlength][r]{183}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm (m1)$

\makebox[\idlength][r]{184}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm (m2)$

\makebox[\idlength][r]{185}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm (n1)$

\makebox[\idlength][r]{186}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm (n2)$

\makebox[\idlength][r]{187}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm (n3)$

\makebox[\idlength][r]{188}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm (\epsilon)$

\makebox[\idlength][r]{189}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm (\epsilon)_{1}$

\makebox[\idlength][r]{190}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm (\epsilon 2)$

\makebox[\idlength][r]{191}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm (fep)$

\makebox[\idlength][r]{192}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm (fx)$

\makebox[\idlength][r]{193}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm (fy)$

\makebox[\idlength][r]{194}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm (fz)$

\makebox[\idlength][r]{195}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm (fu)$

\makebox[\idlength][r]{196}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm (fv)$

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

\makebox[\idlength][r]{198}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm (rx)$

\makebox[\idlength][r]{199}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm (ry)$

\makebox[\idlength][r]{200}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm (rz)$

\makebox[\idlength][r]{201}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm (ru)$

\makebox[\idlength][r]{202}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm (sx)$

\makebox[\idlength][r]{203}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm (sx1)$

\makebox[\idlength][r]{204}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm (sy)$

\makebox[\idlength][r]{205}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm (sy1)$

\makebox[\idlength][r]{206}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm (sz)$

\makebox[\idlength][r]{207}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm (sz1)$

\makebox[\idlength][r]{208}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm (su)$

\makebox[\idlength][r]{209}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm (su1)$

\makebox[\idlength][r]{210}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm (fxs)$

\makebox[\idlength][r]{211}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm (fys)$

\makebox[\idlength][r]{212}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm (crs1)$

\makebox[\idlength][r]{213}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm (f1)$

\makebox[\idlength][r]{214}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm (f2)$

\makebox[\idlength][r]{215}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm (f3)$

\makebox[\idlength][r]{216}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm (f4)$

\makebox[\idlength][r]{217}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm (op1)$

\makebox[\idlength][r]{218}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm (op2)$

\makebox[\idlength][r]{219}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm (r1)$

\makebox[\idlength][r]{220}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm (s1)$

\makebox[\idlength][r]{221}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm (s2)$

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

\makebox[\idlength][r]{250}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm (SX)$

\makebox[\idlength][r]{251}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm (SX1)$

\makebox[\idlength][r]{252}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm (SY)$

\makebox[\idlength][r]{253}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm (SY1)$

\makebox[\idlength][r]{254}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm (SZ)$

\makebox[\idlength][r]{255}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm (SZ1)$

\makebox[\idlength][r]{256}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm (SU)$

\makebox[\idlength][r]{257}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm (SU1)$

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

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

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

\makebox[\idlength][r]{261}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm (F2)$

\makebox[\idlength][r]{262}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm (F3)$

\makebox[\idlength][r]{263}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm (F4)$

\makebox[\idlength][r]{264}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm (OP1)$

\makebox[\idlength][r]{265}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm (OP2)$

\makebox[\idlength][r]{266}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm (R1)$

\makebox[\idlength][r]{267}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm (S1)$

\makebox[\idlength][r]{268}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm (S2)$

\makebox[\idlength][r]{269}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm (EPob)$

\makebox[\idlength][r]{270}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm (CRS1ob)$

\makebox[\idlength][r]{271}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm (F1ob)$

\makebox[\idlength][r]{272}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm (F2ob)$

\makebox[\idlength][r]{273}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm (F3ob)$

\makebox[\idlength][r]{274}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm (F4ob)$

\makebox[\idlength][r]{275}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm (N1ob)$

\makebox[\idlength][r]{276}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm (N2ob)$

\makebox[\idlength][r]{277}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm (OP1ob)$

\makebox[\idlength][r]{278}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm (OP2ob)$

\makebox[\idlength][r]{279}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm (R1ob)$

\makebox[\idlength][r]{280}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm (S1ob)$

\makebox[\idlength][r]{281}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm (S2ob)$

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

\makebox[\idlength][r]{300}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm (-1)$

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

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

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

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

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

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

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

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

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

\makebox[\idlength][r]{310}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm (--01)$

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

\makebox[\idlength][r]{312}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 01//02$

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

\makebox[\idlength][r]{314}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm PlusAssociativity(R)XX$

\makebox[\idlength][r]{315}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm Plus0(R)$

\makebox[\idlength][r]{316}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm Negative(R)$

\makebox[\idlength][r]{317}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm Times1(R)$

\makebox[\idlength][r]{318}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm lessAddition(R)$

\makebox[\idlength][r]{319}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm PlusCommutativity(R)$

\makebox[\idlength][r]{320}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm LeqAntisymmetry(R)$

\makebox[\idlength][r]{321}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm LeqTransitivity(R)$

\makebox[\idlength][r]{322}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm leqAddition(R)$

\makebox[\idlength][r]{323}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm Distribution(R)$

\makebox[\idlength][r]{324}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm A4(Axiom)$

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

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

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

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

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

\makebox[\idlength][r]{330}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm QisClosed(Reciprocal)(Imply)$

\makebox[\idlength][r]{331}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm QisClosed(Reciprocal)$

\makebox[\idlength][r]{332}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm QisClosed(Negative)(Imply)$

\makebox[\idlength][r]{333}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm QisClosed(Negative)$

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

\makebox[\idlength][r]{350}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
\mbox{lemma eqLeq(R)}$

\makebox[\idlength][r]{351}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm TimesAssociativity(R)$

\makebox[\idlength][r]{352}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm TimesCommutativity(R)$

\makebox[\idlength][r]{353}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm (Adgic)SameR$

\makebox[\idlength][r]{354}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm Separation2formula(1)$

\makebox[\idlength][r]{355}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm Separation2formula(2)$

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

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

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

\makebox[\idlength][r]{359}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm From==$

\makebox[\idlength][r]{360}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm To==$

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

\makebox[\idlength][r]{362}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm PlusR(Sym)$

\makebox[\idlength][r]{363}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm ReciprocalR(Axiom)$

\makebox[\idlength][r]{364}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm LessMinus1(N)$

\makebox[\idlength][r]{365}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm Nonnegative(N)$

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

\makebox[\idlength][r]{367}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm NextXS(UpperBound)$

\makebox[\idlength][r]{368}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm NextXS(NoUpperBound)$

\makebox[\idlength][r]{369}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm NextUS(UpperBound)$

\makebox[\idlength][r]{370}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm NextUS(NoUpperBound)$

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

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

\makebox[\idlength][r]{373}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm ExpZero(R)$

\makebox[\idlength][r]{374}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm ExpPositive(R)$

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

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

\makebox[\idlength][r]{377}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm UStelescope(Zero)$

\makebox[\idlength][r]{378}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm UStelescope(Positive)$

\makebox[\idlength][r]{379}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm EqAddition(R)$

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

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

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

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

\makebox[\idlength][r]{384}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 0not1(R)$

\makebox[\idlength][r]{385}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm ExpUnbounded(R)$

\makebox[\idlength][r]{386}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm FromLeq(Advanced)(N)$

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

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

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

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

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

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

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

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

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

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

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

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

\makebox[\idlength][r]{399}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm MemberOfSeries(Imply)$

\makebox[\idlength][r]{400}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm JoinConjuncts(2conditions)$

\makebox[\idlength][r]{401}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
\mbox{prop lemma imply negation}$

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

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

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

\makebox[\idlength][r]{405}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm FromNegated(2*Imply)$

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

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

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

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

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

\makebox[\idlength][r]{411}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm From2*2Disjuncts$

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

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

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

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

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

\makebox[\idlength][r]{417}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm LessLeq(R)$

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

\makebox[\idlength][r]{419}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm memberOfSeries(Type)$

\makebox[\idlength][r]{420}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm  \ast
 (exp) \ast$

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

\makebox[\idlength][r]{440}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm 01//Macro(\ast
)$

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

\makebox[\idlength][r]{463}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm \langle \ast
,\ast
\rangle$

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

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

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

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

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

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

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

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

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

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

\makebox[\idlength][r]{474}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{3}%
\makebox[0.5em]{}%
$\rm [\ast
 \mathrel{\in} \ast
]_{\ast
}$

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

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

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

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

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

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

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

\makebox[\idlength][r]{482}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm \ast
-_{f}\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]{2}%
\makebox[0.5em]{}%
$\rm R(\ast
) -- R(\ast
)$

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

\makebox[\idlength][r]{503}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{1}%
\makebox[0.5em]{}%
$\rm \dot{\neg}\,(\ast
)n$

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

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

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

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

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

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

\makebox[\idlength][r]{510}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{2}%
\makebox[0.5em]{}%
$\rm  \{ ph \mathrel{\in} \ast
\mid \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-12-15.UTC:00:19:10.164930} = 
\href {http://www.diku.dk/~grue/logiweb/20060417/logiweb/doc/misc/time.html}{MJD-54084.TAI:00:19:43.164930} = 
\href {http://www.diku.dk/~grue/logiweb/20060417/logiweb/doc/misc/time.html}{LGT-4672858783164930e-6}
}

\end{document}

