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

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

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

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

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

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

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

\makebox[\idlength][r]{5}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm (A)to(~E~)(Imply)$

\makebox[\idlength][r]{6}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm (E)to(~A~)(Imply)$

\makebox[\idlength][r]{7}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm (E~)to(~A)(Imply)$

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

\makebox[\idlength][r]{23}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm PositiveToRight(Eq)$

\makebox[\idlength][r]{24}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm PositiveToLeft(Eq)$

\makebox[\idlength][r]{25}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm PositiveToLeft(Eq)(1 term)$

\makebox[\idlength][r]{26}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm NegativeToLeft(Eq)$

\makebox[\idlength][r]{27}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm NonreciprocalToRight(Eq)(1 term)$

\makebox[\idlength][r]{28}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm DistributionOut(Minus)$

\makebox[\idlength][r]{29}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm PositiveToRight(Eq)(1 term)$

\makebox[\idlength][r]{30}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm SameSeries(NumDiff)$

\makebox[\idlength][r]{31}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm PlusAssociativity(4 terms)$

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

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

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

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

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

\makebox[\idlength][r]{37}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm NegativeToRight(Neq)(1 term)$

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

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

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

\makebox[\idlength][r]{41}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm SwitchTerms(x<=y-z)$

\makebox[\idlength][r]{42}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm NegativeToLeft(Less)(1 term)$

\makebox[\idlength][r]{43}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm (+1)IsPositive(N)$

\makebox[\idlength][r]{44}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm (1/2)(x+y)-x=(1/2)(y-x)$

\makebox[\idlength][r]{45}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm y-(1/2)(x+y)=(1/2)(y-x)$

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

\makebox[\idlength][r]{47}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm SameExp(Base)$

\makebox[\idlength][r]{48}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm SameExp(Indu)$

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

\makebox[\idlength][r]{50}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm Exp(+1)$

\makebox[\idlength][r]{51}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm PositiveBase(Base)$

\makebox[\idlength][r]{52}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm PositiveBase(Indu)$

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

\makebox[\idlength][r]{54}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm BSzero(Exact)$

\makebox[\idlength][r]{55}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm SameBS(2)(Base)$

\makebox[\idlength][r]{56}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm SameBS(2)(Indu)$

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

\makebox[\idlength][r]{58}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm BS(+1)$

\makebox[\idlength][r]{59}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm BSbound(Exact)(Base)$

\makebox[\idlength][r]{60}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm BSbound(Exact)(Indu)$

\makebox[\idlength][r]{61}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm BSbound(Exact)$

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

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

\makebox[\idlength][r]{64}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm SameTelescope(2)(Base)$

\makebox[\idlength][r]{65}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm SameTelescope(2)(Indu)$

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

\makebox[\idlength][r]{67}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm UStelescope(+1)$

\makebox[\idlength][r]{68}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm TelescopeNumerical(Base)$

\makebox[\idlength][r]{69}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm TelescopeNumerical(Indu)$

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

\makebox[\idlength][r]{71}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm TelescopeBound(Base)$

\makebox[\idlength][r]{72}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm TelescopeBound(Indu)$

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

\makebox[\idlength][r]{74}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm LessNeq(F)(Helper)$

\makebox[\idlength][r]{75}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm LessNeq(F)$

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

\makebox[\idlength][r]{77}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm IntervalSize(Base)$

\makebox[\idlength][r]{78}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm IntervalSize(Indu)$

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

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

\makebox[\idlength][r]{81}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
\mbox{lemma USdecreasing(+1)}$

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

\makebox[\idlength][r]{83}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm CloseUS(n+1)$

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

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

\makebox[\idlength][r]{86}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm IntroExist(Helper)$

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

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

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

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

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

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

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

\makebox[\idlength][r]{94}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm AddExist(Helper1)$

\makebox[\idlength][r]{95}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm AddExist(Helper2)$

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

\makebox[\idlength][r]{97}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm AddExist(SimpleAnt)$

\makebox[\idlength][r]{98}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm AddExist(Simple)$

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

\makebox[\idlength][r]{119}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm PositiveToRight(Leq)$

\makebox[\idlength][r]{120}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm PositiveToRight(Leq)(1 term)$

\makebox[\idlength][r]{121}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
\mbox{lemma negativeToRight(Leq)}$

\makebox[\idlength][r]{122}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm PositiveToLeft(Leq)$

\makebox[\idlength][r]{123}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm negativeToLeft(Leq)$

\makebox[\idlength][r]{124}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm negativeToLeft(Leq)(1 term)$

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

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

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

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

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

\makebox[\idlength][r]{130}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm AddEquations(Leq)$

\makebox[\idlength][r]{131}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm MultiplyEquations(Leq)$

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

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

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

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

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

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

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

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

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

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

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

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

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

\makebox[\idlength][r]{145}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm SwitchTerms(x<y-z)$

\makebox[\idlength][r]{146}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm SwitchTerms(x-y<z)$

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

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

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

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

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

\makebox[\idlength][r]{152}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm PositiveToRight(Less)$

\makebox[\idlength][r]{153}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm PositiveToLeft(Less)$

\makebox[\idlength][r]{154}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm NegativeToLeft(Less)$

\makebox[\idlength][r]{155}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm NegativeToRight(Less)$

\makebox[\idlength][r]{156}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm AddEquations(Less)$

\makebox[\idlength][r]{157}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm AddEquations(LeqLess)$

\makebox[\idlength][r]{158}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm reciprocalToLeft(Less)$

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

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

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

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

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

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

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

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

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

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

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

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

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

\makebox[\idlength][r]{172}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 0<=|x|$

\makebox[\idlength][r]{173}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm x<=|x|$

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

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

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

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

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

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

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

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

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

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

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

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

\makebox[\idlength][r]{186}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm splitNumericalSum(+-small)$

\makebox[\idlength][r]{187}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm splitNumericalSum(+-big)$

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

\makebox[\idlength][r]{189}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm splitNumericalSum(-+)$

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

\makebox[\idlength][r]{205}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm x+y=zBackwards$

\makebox[\idlength][r]{206}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm x*y=zBackwards$

\makebox[\idlength][r]{207}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm x=x+(y-y)$

\makebox[\idlength][r]{208}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm x=x+y-y$

\makebox[\idlength][r]{209}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm x=x*y*(1/y)$

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

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

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

\makebox[\idlength][r]{213}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm x*0+x=x$

\makebox[\idlength][r]{214}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm x*0=0$

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

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

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

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

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

\makebox[\idlength][r]{220}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm (-1)*(-1)+(-1)*1=0$

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

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

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

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

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

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

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

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

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

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

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

\makebox[\idlength][r]{232}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm -x-y=-(x+y)$

\makebox[\idlength][r]{233}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm -x*y=-(x*y)$

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

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

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

\makebox[\idlength][r]{237}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm f2R(Plus)$

\makebox[\idlength][r]{238}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm f2R(Times)$

\makebox[\idlength][r]{239}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm <<TransitivityHelper(Q)$

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

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

\makebox[\idlength][r]{242}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm <<==AntisymmetryHelper(Q)$

\makebox[\idlength][r]{243}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm FromNot<f(Weak)(Helper)$

\makebox[\idlength][r]{244}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm FromNot<f(Weak)$

\makebox[\idlength][r]{245}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm FromNot<f(Strong)(Helper2)$

\makebox[\idlength][r]{246}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm FromNot<f(Strong)(Helper)$

\makebox[\idlength][r]{247}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm FromNot<f(Strong)$

\makebox[\idlength][r]{248}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm fromNotSameF(Strongest)(Helper2)$

\makebox[\idlength][r]{249}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm fromNotSameF(Strongest)(Helper)$

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

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

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

\makebox[\idlength][r]{253}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm FromNot<<$

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

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

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

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

\makebox[\idlength][r]{258}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm FromNotLess(F)$

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

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

\makebox[\idlength][r]{261}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm Fpart-Bounded(Base)$

\makebox[\idlength][r]{262}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm Fpart-Bounded(InduHelper)$

\makebox[\idlength][r]{263}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm Fpart-Bounded(Indu)$

\makebox[\idlength][r]{264}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm Fpart-Bounded$

\makebox[\idlength][r]{265}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm F-Bounded(Helper)$

\makebox[\idlength][r]{266}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm F-Bounded$

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

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

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

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

\makebox[\idlength][r]{271}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm x*0=0(F)$

\makebox[\idlength][r]{272}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm x*0=0(R)$

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

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

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

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

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

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

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

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

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

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

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

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

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

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

\makebox[\idlength][r]{287}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm (Eventually=f)2sameF(Helper)$

\makebox[\idlength][r]{288}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm (Eventually=f)2sameF$

\makebox[\idlength][r]{289}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm FromNotSameF(Strong)(Helper2)$

\makebox[\idlength][r]{290}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm FromNotSameF(Strong)(Helper)$

\makebox[\idlength][r]{291}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm FromNotSameF(Strong)$

\makebox[\idlength][r]{292}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm SameFreciprocal(Helper)$

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

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

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

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

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

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

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

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

\makebox[\idlength][r]{301}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm PositiveToRight(Less)(1 term)$

\makebox[\idlength][r]{302}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm (A~)to(~E)$

\makebox[\idlength][r]{303}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 
\mbox{lemma ==Transitivity4}$

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

\makebox[\idlength][r]{305}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm x=x+(y-y)(R)$

\makebox[\idlength][r]{306}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm x=x+y-y(R)$

\makebox[\idlength][r]{307}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm PositiveToRight(Eq)(R)$

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

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

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

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

\makebox[\idlength][r]{312}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm PositiveToRight(Less)(R)$

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

\makebox[\idlength][r]{314}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm PositiveToRight(Less)(1 term)(R)$

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

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

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

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

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

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

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

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

\makebox[\idlength][r]{323}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm NegativeToRight(Eq)(1 term)(R)$

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

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

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

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

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

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

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

\makebox[\idlength][r]{331}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm -0=0(R)$

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

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

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

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

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

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

\makebox[\idlength][r]{338}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 0<=|x|(R)$

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

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

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

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

\makebox[\idlength][r]{343}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm x*0+x=x(R)$

\makebox[\idlength][r]{344}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm x*0=0(R)(fff)$

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

\makebox[\idlength][r]{346}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm Times(-1)Left(R)$

\makebox[\idlength][r]{347}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm -x-y=-(x+y)(R)$

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

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

\makebox[\idlength][r]{350}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm SignNumerical(+)(R)$

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

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

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

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

\makebox[\idlength][r]{355}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm x<=|x|(R)$

\makebox[\idlength][r]{356}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm USlimitIsUpperBound(Helper)$

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

\makebox[\idlength][r]{358}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm (-1)*(-1)+(-1)*1=0(R)$

\makebox[\idlength][r]{359}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm (-1)*(-1)=1(R)$

\makebox[\idlength][r]{360}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 0<1Helper(R)$

\makebox[\idlength][r]{361}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 0<1(R)$

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

\makebox[\idlength][r]{363}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm PositiveBase(R)(Base)$

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

\makebox[\idlength][r]{365}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm x=x*y*(1/y)(R)$

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

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

\makebox[\idlength][r]{368}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 0<2(R)$

\makebox[\idlength][r]{369}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm SameExp(R)(Base)$

\makebox[\idlength][r]{370}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm SameExp(R)(Indu)$

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

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

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

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

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

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

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

\makebox[\idlength][r]{378}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 0<1/2(R)$

\makebox[\idlength][r]{379}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm PositiveToRight(Eq)(1 term)(R)$

\makebox[\idlength][r]{380}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm Exp(+1)(R)$

\makebox[\idlength][r]{381}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm PositiveBase(R)(Indu)$

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

\makebox[\idlength][r]{383}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm -x*y=-(x*y)(R)$

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

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

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

\makebox[\idlength][r]{387}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm x+x=2*x(R)$

\makebox[\idlength][r]{388}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm (1/2)x+(1/2)x=x(R)$

\makebox[\idlength][r]{389}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm DistributionOut(Minus)(R)$

\makebox[\idlength][r]{390}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm (1/2)(x+y)-x=(1/2)(y-x)(R)$

\makebox[\idlength][r]{391}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm IntervalSize(R)(Base)$

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

\makebox[\idlength][r]{393}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm NegativeToLeft(Less)(R)$

\makebox[\idlength][r]{394}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm NegativeToLeft(Less)(1 term)(R)$

\makebox[\idlength][r]{395}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm y-(1/2)(x+y)=(1/2)(y-x)(R)$

\makebox[\idlength][r]{396}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm IntervalSize(R)(Indu)$

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

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

\makebox[\idlength][r]{399}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm USdecreasing(+1)(R)$

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

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

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

\makebox[\idlength][r]{403}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 1<=x+1(N)$

\makebox[\idlength][r]{404}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm NonzeroProduct(2)(R)$

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

\makebox[\idlength][r]{406}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm NonreciprocalToRight(Eq)(1 term)(R)$

\makebox[\idlength][r]{407}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm ExpNonzero(Base)$

\makebox[\idlength][r]{408}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm ExpNonzero(Indu)$

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

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

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

\makebox[\idlength][r]{412}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm HalfBase(Base)$

\makebox[\idlength][r]{413}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm HalfBase(Indu)$

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

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

\makebox[\idlength][r]{416}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm x*y=zBackwards(R)$

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

\makebox[\idlength][r]{418}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm ReciprocalToRight(Less)(R)$

\makebox[\idlength][r]{419}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm ReciprocalToRight(Less)(1 term)(R)$

\makebox[\idlength][r]{420}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm NonreciprocalToLeft(Less)(R)$

\makebox[\idlength][r]{421}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm 1<x*y(R)$

\makebox[\idlength][r]{422}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm SwitchFactors(1/x<y)(R)$

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

\makebox[\idlength][r]{424}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm IntervalSize(anyPositive)$

\makebox[\idlength][r]{425}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm USdecreasing(+n)(Base)$

\makebox[\idlength][r]{426}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm USdecreasing(+n)(Indu)$

\makebox[\idlength][r]{427}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm USdecreasing(+n)$

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

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

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

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

\makebox[\idlength][r]{432}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm SubtractEquations(Less)(R)$

\makebox[\idlength][r]{433}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm SubtractEquationsLeft(Less)(R)$

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

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

\makebox[\idlength][r]{436}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm RemoveDoubleNeg(Consequent)$

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

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

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

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

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

\makebox[\idlength][r]{442}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm USlimitIsLeastUpperBound(Helper)$

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

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

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

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

\makebox[\idlength][r]{447}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm ysFClose(Helper)$

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

\makebox[\idlength][r]{449}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm ysFCauchy(Helper)$

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

\makebox[\idlength][r]{465}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm FromOrderedPair(TwoLevels)$

\makebox[\idlength][r]{466}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm ToCartProd(Helper)$

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

\makebox[\idlength][r]{468}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm NonreciprocalToRight(Eq)$

\makebox[\idlength][r]{469}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm NonreciprocalToLeft(Eq)(1 term)$

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

\makebox[\idlength][r]{497}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm To=f(Subset)(Helper)$

\makebox[\idlength][r]{498}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm To=f(Subset)$

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

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

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

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

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

\makebox[\idlength][r]{504}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm -x+(1/2)x=-(1/2)x$

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

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

\makebox[\idlength][r]{507}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm |x-x|=0$

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

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

\makebox[\idlength][r]{510}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm (1/3)x+(1/3)x=(2/3)x$

\makebox[\idlength][r]{511}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm (2/3)x+(1/3)x=x$

\makebox[\idlength][r]{512}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm -x+(2/3)x=-(1/3)x$

\makebox[\idlength][r]{513}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm -(1/3)x-(1/3)x=-(2/3)x$

\makebox[\idlength][r]{514}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm -x+(1/3)x=-(2/3)x$

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

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

\makebox[\idlength][r]{517}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm SubLessLeft(F)$

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

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

\makebox[\idlength][r]{520}%
\makebox[0.5em]{}%
\makebox[\aritylength][r]{0}%
\makebox[0.5em]{}%
$\rm SubLessRight(F)$

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

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

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

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

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

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

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

\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-08.UTC:16:16:16.345569} = 
\href {http://www.diku.dk/~grue/logiweb/20060417/logiweb/doc/misc/time.html}{MJD-54077.TAI:16:16:49.345569} = 
\href {http://www.diku.dk/~grue/logiweb/20060417/logiweb/doc/misc/time.html}{LGT-4672311409345569e-6}
}

\end{document}

