This is TeX, Version 3.14159 (Web2C 7.4.5) (format=latex 2006.8.25)  29 DEC 2006 11:55
**page
(./page.tex
LaTeX2e <2001/06/01>
Babel <v3.7h> and hyphenation patterns for american, french, german, ngerman, d
anish, nohyphenation, loaded.
(/usr/share/texmf/tex/latex/base/article.cls
Document Class: article 2001/04/21 v1.4e Standard LaTeX document class
(/usr/share/texmf/tex/latex/base/fleqn.clo
File: fleqn.clo 1998/08/17 v1.1c Standard LaTeX option (flush left equations)
\mathindent=\dimen102
)
(/usr/share/texmf/tex/latex/base/size10.clo
File: size10.clo 2001/04/21 v1.4e Standard LaTeX file (size option)
)
\c@part=\count79
\c@section=\count80
\c@subsection=\count81
\c@subsubsection=\count82
\c@paragraph=\count83
\c@subparagraph=\count84
\c@figure=\count85
\c@table=\count86
\abovecaptionskip=\skip41
\belowcaptionskip=\skip42
\bibindent=\dimen103
) (./lgwinclude.tex)
(/usr/share/texmf/tex/latex/base/latexsym.sty
Package: latexsym 1998/08/17 v2.2e Standard LaTeX package (lasy symbols)
\symlasy=\mathgroup4
LaTeX Font Info:    Overwriting symbol font `lasy' in version `bold'
(Font)                  U/lasy/m/n --> U/lasy/b/n on input line 42.
)
(/usr/share/texmf/tex/latex/base/makeidx.sty
Package: makeidx 2000/03/29 v1.0m Standard LaTeX package
)
\bracketwidth=\skip43
LaTeX Font Info:    External font `cmex10' loaded for size
(Font)              <7> on input line 23.
LaTeX Font Info:    External font `cmex10' loaded for size
(Font)              <5> on input line 23.
LaTeX Font Info:    Try loading font information for U+lasy on input line 23.

(/usr/share/texmf/tex/latex/base/ulasy.fd
File: ulasy.fd 1998/08/17 v2.2e LaTeX symbol font definitions
)
(/usr/share/texmf/tex/latex/graphics/lscape.sty
Package: lscape 2000/10/22 v3.01 Landscape Pages (DPC)

(/usr/share/texmf/tex/latex/graphics/graphics.sty
Package: graphics 2001/07/07 v1.0n Standard LaTeX Graphics (DPC,SPQR)

(/usr/share/texmf/tex/latex/graphics/trig.sty
Package: trig 1999/03/16 v1.09 sin cos tan (DPC)
)
(/usr/share/texmf/tex/latex/config/graphics.cfg
File: graphics.cfg 2001/08/31 v1.1 graphics configuration of teTeX/TeXLive
)
Package graphics Info: Driver file: dvips.def on input line 80.

(/usr/share/texmf/tex/latex/graphics/dvips.def
File: dvips.def 1999/02/16 v3.0i Driver-dependant file (DPC,SPQR)
)))
(/usr/share/texmf/tex/latex/tools/multicol.sty
Package: multicol 2000/07/10 v1.5z multicolumn formatting (FMi)
\c@tracingmulticols=\count87
\mult@box=\box26
\multicol@leftmargin=\dimen104
\c@unbalance=\count88
\c@collectmore=\count89
\doublecol@number=\count90
\multicoltolerance=\count91
\multicolpretolerance=\count92
\full@width=\dimen105
\page@free=\dimen106
\premulticols=\dimen107
\postmulticols=\dimen108
\multicolsep=\skip44
\multicolbaselineskip=\skip45
\partial@page=\box27
\last@line=\box28
\mult@rightbox=\box29
\mult@grightbox=\box30
\mult@gfirstbox=\box31
\mult@firstbox=\box32
\@tempa=\box33
\@tempa=\box34
\@tempa=\box35
\@tempa=\box36
\@tempa=\box37
\@tempa=\box38
\@tempa=\box39
\@tempa=\box40
\@tempa=\box41
\@tempa=\box42
\@tempa=\box43
\@tempa=\box44
\@tempa=\box45
\@tempa=\box46
\@tempa=\box47
\@tempa=\box48
\@tempa=\box49
\c@columnbadness=\count93
\c@finalcolumnbadness=\count94
\last@try=\dimen109
\multicolovershoot=\dimen110
\multicolundershoot=\dimen111
\mult@nat@firstbox=\box50
\colbreak@box=\box51
)
(/usr/share/texmf/tex/latex/misc/float.sty
Package: float 2001/11/08 v1.3d Float enhancements (AL)
\c@float@type=\count95
\float@exts=\toks14
\float@box=\box52
\@float@everytoks=\toks15
\@floatcapt=\box53
)
(/usr/share/texmf/tex/latex/base/inputenc.sty
Package: inputenc 2001/07/10 v0.99a Input encoding file 

(/usr/share/texmf/tex/latex/base/latin1.def
File: latin1.def 2001/07/10 v0.99a Input encoding file 
))
(/usr/share/texmf/tex/latex/graphics/graphicx.sty
Package: graphicx 1999/02/16 v1.0f Enhanced LaTeX Graphics (DPC,SPQR)

(/usr/share/texmf/tex/latex/graphics/keyval.sty
Package: keyval 1999/03/16 v1.13 key=value parser (DPC)
\KV@toks@=\toks16
)
\Gin@req@height=\dimen112
\Gin@req@width=\dimen113
)
(/usr/share/texmf/tex/latex/tools/verbatim.sty
Package: verbatim 2001/03/12 v1.5p LaTeX2e package for verbatim enhancements
\every@verbatim=\toks17
\verbatim@line=\toks18
\verbatim@in@stream=\read1
)
(/usr/share/texmf/tex/generic/babel/babel.sty
Package: babel 2001/03/01 v3.7h The Babel package

(/usr/share/texmf/tex/generic/babel/danish.ldf
Language: danish 2001/01/30 v1.3n Danish support from the babel system

(/usr/share/texmf/tex/generic/babel/babel.def
File: babel.def 2001/03/01 v3.7h Babel common definitions
\babel@savecnt=\count96
\U@D=\dimen114
)
Package babel Info: Making " an active character on input line 62.
))
(/usr/share/texmf/tex/latex/base/graphpap.sty
Package: graphpap 1994/08/09 v1.0c Standard LaTeX graphpap package (LL)
)
(/usr/share/texmf/tex/latex/hyperref/hyperref.sty
Package: hyperref 2003/01/22 v6.73n Hypertext links for LaTeX
\@linkdim=\dimen115
\Hy@linkcounter=\count97
\Hy@pagecounter=\count98

(/usr/share/texmf/tex/latex/hyperref/pd1enc.def
File: pd1enc.def 2003/01/22 v6.73n Hyperref: PDFDocEncoding definition (HO)
)
(/usr/share/texmf/tex/latex/config/hyperref.cfg
File: hyperref.cfg 2002/06/06 v1.2 hyperref configuration of TeXLive and teTeX
)
Package hyperref Info: Hyper figures OFF on input line 1792.
Package hyperref Info: Link nesting OFF on input line 1797.
Package hyperref Info: Hyper index ON on input line 1800.
Package hyperref Info: Plain pages ON on input line 1805.
Package hyperref Info: Backreferencing OFF on input line 1812.

Implicit mode ON; LaTeX internals redefined
Package hyperref Info: Bookmarks ON on input line 1916.
(/usr/share/texmf/tex/latex/html/url.sty
Package: url 1999/03/02  ver 1.4  Verb mode for urls, email addresses, and file
 names
)
LaTeX Info: Redefining \url on input line 2055.
\Fld@menulength=\count99
\Field@Width=\dimen116
\Fld@charsize=\dimen117
\Choice@toks=\toks19
\Field@toks=\toks20
Package hyperref Info: Hyper figures OFF on input line 2513.
Package hyperref Info: Link nesting OFF on input line 2518.
Package hyperref Info: Hyper index ON on input line 2521.
Package hyperref Info: backreferencing OFF on input line 2528.
Package hyperref Info: Link coloring OFF on input line 2533.
\c@Item=\count100
\c@Hfootnote=\count101
)
*hyperref using driver hdvipdfm*
(/usr/share/texmf/tex/latex/hyperref/hdvipdfm.def
File: hdvipdfm.def 2003/01/22 v6.73n Hyperref driver for dvipdfm
\pdfm@box=\box54
\Fld@listcount=\count102
\@outlinefile=\write3
)
Package hyperref Info: Option `colorlinks' set `false' on input line 42.
\outex=\write4
\toktex=\toks21
\openout4 = `page.otx'.

\outest=\write5
\openout5 = `page.tst'.

 (./page.aux)
\openout1 = `page.aux'.

LaTeX Font Info:    Checking defaults for OML/cmm/m/it on input line 73.
LaTeX Font Info:    ... okay on input line 73.
LaTeX Font Info:    Checking defaults for T1/cmr/m/n on input line 73.
LaTeX Font Info:    ... okay on input line 73.
LaTeX Font Info:    Checking defaults for OT1/cmr/m/n on input line 73.
LaTeX Font Info:    ... okay on input line 73.
LaTeX Font Info:    Checking defaults for OMS/cmsy/m/n on input line 73.
LaTeX Font Info:    ... okay on input line 73.
LaTeX Font Info:    Checking defaults for OMX/cmex/m/n on input line 73.
LaTeX Font Info:    ... okay on input line 73.
LaTeX Font Info:    Checking defaults for U/cmr/m/n on input line 73.
LaTeX Font Info:    ... okay on input line 73.
LaTeX Font Info:    Checking defaults for PD1/pdf/m/n on input line 73.
LaTeX Font Info:    ... okay on input line 73.
Package hyperref Info: Link coloring OFF on input line 73.

(/usr/share/texmf/tex/latex/hyperref/nameref.sty
Package: nameref 2001/01/27 v2.19 Cross-referencing by name of section
\c@section@level=\count103
)
LaTeX Info: Redefining \ref on input line 73.
LaTeX Info: Redefining \pageref on input line 73.
 (./page.out) (./page.out)
\openout3 = `page.out'.


Overfull \hbox (15.86766pt too wide) in paragraph at lines 85--102
[]$\OT1/cmr/m/n/10 [SystemQ[]ToNegatedDoubleImply: ^^E\OMS/cmsy/m/n/10 A\OML/cm
m/m/it/10 ; \OMS/cmsy/m/n/10 B\OML/cmm/m/it/10 ; \OMS/cmsy/m/n/10 C\OT1/cmr/m/n
/10 : \OMS/cmsy/m/n/10 A ` B ` [] \OT1/cmr/m/n/10 (\OMS/cmsy/m/n/10 C\OT1/cmr/m
/n/10 )n \OMS/cmsy/m/n/10 ` [] \OT1/cmr/m/n/10 ((\OMS/cmsy/m/n/10 A )|
 []

\lgwproofline=\count104
\lgwproofline=\count105

Overfull \hbox (10.82487pt too wide) in paragraph at lines 626--639
[]$\OT1/cmr/m/n/10 [SystemQ[]RemoveDoubleNeg(Consequent): ^^E\OMS/cmsy/m/n/10 A
\OML/cmm/m/it/10 ; \OMS/cmsy/m/n/10 B\OT1/cmr/m/n/10 : \OMS/cmsy/m/n/10 A ) [] 
\OT1/cmr/m/n/10 ([] (\OMS/cmsy/m/n/10 B\OT1/cmr/m/n/10 )n)n \OMS/cmsy/m/n/10 `|

 []

\lgwproofline=\count106
[1

]
\lgwproofline=\count107
\lgwproofline=\count108

Underfull \hbox (badness 10000) in paragraph at lines 1197--1197
[]$[] \OT1/cmr/m/n/10 (\OMS/cmsy/m/n/10 8\OT1/cmr/m/n/10 V[]: [] (\OMS/cmsy/m/n
/10 A\OT1/cmr/m/n/10 )n)n \OMS/cmsy/m/n/10 )
 []

\lgwproofline=\count109

Overfull \hbox (34.08434pt too wide) in paragraph at lines 1511--1529
[]$\OT1/cmr/m/n/10 [SystemQ[]AddNegatedAll: ^^EV[]\OML/cmm/m/it/10 ; \OMS/cmsy/
m/n/10 A\OML/cmm/m/it/10 ; \OMS/cmsy/m/n/10 B\OT1/cmr/m/n/10 : \OMS/cmsy/m/n/10
 B ) A ` [] \OT1/cmr/m/n/10 (\OMS/cmsy/m/n/10 8\OT1/cmr/m/n/10 V[]: \OMS/cmsy/m
/n/10 A\OT1/cmr/m/n/10 )n \OMS/cmsy/m/n/10 ) [] \OT1/cmr/m/n/10 (\OMS/cmsy/m/n/
10 8\OT1/cmr/m/n/10 V[]: \OMS/cmsy/m/n/10 B\OT1/cmr/m/n/10 )n]$ |
 []

\lgwproofline=\count110
\lgwproofline=\count111

Underfull \hbox (badness 10000) in paragraph at lines 1779--1779
[]$[] \OT1/cmr/m/n/10 (\OMS/cmsy/m/n/10 8\OT1/cmr/m/n/10 V[]: [] (\OMS/cmsy/m/n
/10 8\OT1/cmr/m/n/10 V[]: \OMS/cmsy/m/n/10 A\OT1/cmr/m/n/10 )n)n \OMS/cmsy/m/n/
10 )
 []


Underfull \hbox (badness 10000) in paragraph at lines 1803--1803
[]$\OMS/cmsy/m/n/10 9\OT1/cmr/m/n/10 V[]: \OMS/cmsy/m/n/10 8\OT1/cmr/m/n/10 V[]
: \OMS/cmsy/m/n/10 A )
 []


Underfull \hbox (badness 10000) in paragraph at lines 1839--1839
[]$\OMS/cmsy/m/n/10 9\OT1/cmr/m/n/10 V[]: \OMS/cmsy/m/n/10 8\OT1/cmr/m/n/10 V[]
: \OMS/cmsy/m/n/10 A )
 []


Overfull \hbox (13.72299pt too wide) in paragraph at lines 1875--1875
[]$[] \OT1/cmr/m/n/10 (\OMS/cmsy/m/n/10 8\OT1/cmr/m/n/10 V[]: [] (\OMS/cmsy/m/n
/10 8\OT1/cmr/m/n/10 V[]: \OMS/cmsy/m/n/10 9\OT1/cmr/m/n/10 V[]: [] (\OMS/cmsy/
m/n/10 A\OT1/cmr/m/n/10 )n)n)n \OMS/cmsy/m/n/10 )|
 []


Underfull \hbox (badness 10000) in paragraph at lines 1905--1905
[]$\OMS/cmsy/m/n/10 9\OT1/cmr/m/n/10 V[]: \OMS/cmsy/m/n/10 8\OT1/cmr/m/n/10 V[]
: \OMS/cmsy/m/n/10 9\OT1/cmr/m/n/10 V[]: [] (\OMS/cmsy/m/n/10 A\OT1/cmr/m/n/10 
)n \OMS/cmsy/m/n/10 )
 []


Overfull \hbox (0.94527pt too wide) in paragraph at lines 1905--1905
[] \OT1/cmr/m/n/10 (\OMS/cmsy/m/n/10 8\OT1/cmr/m/n/10 V[]: [] (\OMS/cmsy/m/n/10
 8\OT1/cmr/m/n/10 V[]: \OMS/cmsy/m/n/10 9\OT1/cmr/m/n/10 V[]: [] (\OMS/cmsy/m/n
/10 A\OT1/cmr/m/n/10 )n)n)n$|
 []


Underfull \hbox (badness 10000) in paragraph at lines 1945--1945
[]$\OMS/cmsy/m/n/10 9\OT1/cmr/m/n/10 V[]: \OMS/cmsy/m/n/10 8\OT1/cmr/m/n/10 V[]
: \OMS/cmsy/m/n/10 9\OT1/cmr/m/n/10 V[]: [] (\OMS/cmsy/m/n/10 A\OT1/cmr/m/n/10 
)n \OMS/cmsy/m/n/10 )
 []

[2]
\lgwproofline=\count112
\lgwproofline=\count113
\lgwproofline=\count114
\lgwproofline=\count115
 [3]
\lgwproofline=\count116

Overfull \hbox (25.33882pt too wide) in paragraph at lines 2845--2862
[]$\OT1/cmr/m/n/10 [SystemQ[]SameExp(Base): ^^E\OMS/cmsy/m/n/10 N\OML/cmm/m/it/
10 ; \OMS/cmsy/m/n/10 X\OT1/cmr/m/n/10 : \OMS/cmsy/m/n/10 8N\OT1/cmr/m/n/10 : (
0 = \OMS/cmsy/m/n/10 N ) X\OT1/cmr/m/n/10 (exp)0 = \OMS/cmsy/m/n/10 X\OT1/cmr/m
/n/10 (exp)\OMS/cmsy/m/n/10 N\OT1/cmr/m/n/10 )]$ |
 []

\lgwproofline=\count117

Overfull \hbox (4.84pt too wide) in paragraph at lines 3133--3167
[]$\OT1/cmr/m/n/10 [SystemQ[]SameExp(Indu): ^^E\OMS/cmsy/m/n/10 M\OML/cmm/m/it/
10 ; \OMS/cmsy/m/n/10 N\OML/cmm/m/it/10 ; \OMS/cmsy/m/n/10 X\OT1/cmr/m/n/10 : \
OMS/cmsy/m/n/10 8N\OT1/cmr/m/n/10 : (\OMS/cmsy/m/n/10 M \OT1/cmr/m/n/10 = \OMS/
cmsy/m/n/10 N ) X\OT1/cmr/m/n/10 (exp)\OMS/cmsy/m/n/10 M \OT1/cmr/m/n/10 =|
 []

\lgwproofline=\count118

Underfull \hbox (badness 3291) in paragraph at lines 3299--3299
[]$\OMS/cmsy/m/n/10 X\OT1/cmr/m/n/10 (exp)((\OMS/cmsy/m/n/10 M \OT1/cmr/m/n/10 
+ 1)) = (\OMS/cmsy/m/n/10 X ^^C
 []


Underfull \hbox (badness 2600) in paragraph at lines 3356--3356
[]$\OMS/cmsy/m/n/10 M \OT1/cmr/m/n/10 = ((\OMS/cmsy/m/n/10 M \OT1/cmr/m/n/10 + 
1) \OMS/cmsy/m/n/10 ^^@ \OT1/cmr/m/n/10 1) \OMS/cmsy/m/n/10 )
 []


Underfull \hbox (badness 4660) in paragraph at lines 3418--3418
[]$\OMS/cmsy/m/n/10 X\OT1/cmr/m/n/10 (exp)(((\OMS/cmsy/m/n/10 M \OT1/cmr/m/n/10
 + 1) \OMS/cmsy/m/n/10 ^^@ \OT1/cmr/m/n/10 1)) =
 []


Underfull \hbox (badness 6348) in paragraph at lines 3567--3567
[]$\OT1/cmr/m/n/10 (\OMS/cmsy/m/n/10 X ^^C X\OT1/cmr/m/n/10 (exp)\OMS/cmsy/m/n/
10 M\OT1/cmr/m/n/10 ) = (\OMS/cmsy/m/n/10 X ^^C
 []


Underfull \hbox (badness 5519) in paragraph at lines 3649--3649
[]$\OT1/cmr/m/n/10 (\OMS/cmsy/m/n/10 X ^^C X\OT1/cmr/m/n/10 (exp)((\OMS/cmsy/m/
n/10 N ^^@ \OT1/cmr/m/n/10 1))) =
 []


Underfull \hbox (badness 6125) in paragraph at lines 3831--3831
[]$\OMS/cmsy/m/n/10 8N\OT1/cmr/m/n/10 : ((\OMS/cmsy/m/n/10 M \OT1/cmr/m/n/10 + 
1) = \OMS/cmsy/m/n/10 N )
 []


Underfull \hbox (badness 1454) in paragraph at lines 3896--3896
\OMS/cmsy/m/n/10 N ) X\OT1/cmr/m/n/10 (exp)((\OMS/cmsy/m/n/10 M \OT1/cmr/m/n/10
 + 1)) =
 []

[4]
\lgwproofline=\count119

Underfull \hbox (badness 1454) in paragraph at lines 4055--4055
\OMS/cmsy/m/n/10 N ) X\OT1/cmr/m/n/10 (exp)((\OMS/cmsy/m/n/10 M \OT1/cmr/m/n/10
 + 1)) =
 []


Underfull \hbox (badness 1365) in paragraph at lines 4114--4114
[]$\OMS/cmsy/m/n/10 M \OT1/cmr/m/n/10 = \OMS/cmsy/m/n/10 N ) X\OT1/cmr/m/n/10 (
exp)\OMS/cmsy/m/n/10 M \OT1/cmr/m/n/10 =
 []

\lgwproofline=\count120

Underfull \hbox (badness 3291) in paragraph at lines 4284--4284
[]$\OMS/cmsy/m/n/10 X\OT1/cmr/m/n/10 (exp)((\OMS/cmsy/m/n/10 M \OT1/cmr/m/n/10 
+ 1)) = (\OMS/cmsy/m/n/10 X ^^C
 []


Underfull \hbox (badness 6348) in paragraph at lines 4362--4362
[]$\OT1/cmr/m/n/10 (\OMS/cmsy/m/n/10 X ^^C X\OT1/cmr/m/n/10 (exp)\OMS/cmsy/m/n/
10 M\OT1/cmr/m/n/10 ) = (\OMS/cmsy/m/n/10 X ^^C
 []


Underfull \hbox (badness 3291) in paragraph at lines 4427--4427
[]$\OMS/cmsy/m/n/10 X\OT1/cmr/m/n/10 (exp)((\OMS/cmsy/m/n/10 M \OT1/cmr/m/n/10 
+ 1)) = (\OMS/cmsy/m/n/10 X ^^C
 []

[5]
\lgwproofline=\count121

Underfull \hbox (badness 1210) in paragraph at lines 4680--4680
[]$\OT1/cmr/m/n/10 (\OMS/cmsy/m/n/10 X ^^C \OT1/cmr/m/n/10 ((\OMS/cmsy/m/n/10 Z
 ^^C \OT1/cmr/m/n/10 (\OMS/cmsy/m/n/10 ^^@\OT1/cmr/m/n/10 1)))) = (\OMS/cmsy/m/
n/10 X ^^C
 []

\lgwproofline=\count122
[6]
\lgwproofline=\count123

Underfull \hbox (badness 3000) in paragraph at lines 5530--5530
[]$\OT1/cmr/m/n/10 (\OMS/cmsy/m/n/10 ^^@\OT1/cmr/m/n/10 u((1\OML/cmm/m/it/10 =\
OT1/cmr/m/n/10 2 \OMS/cmsy/m/n/10 ^^C \OT1/cmr/m/n/10 ((\OMS/cmsy/m/n/10 X \OT1
/cmr/m/n/10 + \OMS/cmsy/m/n/10 Y\OT1/cmr/m/n/10 ))))) =
 []

[7]
\lgwproofline=\count124
\lgwproofline=\count125

Underfull \hbox (badness 3291) in paragraph at lines 6364--6364
[]$\OMS/cmsy/m/n/10 X\OT1/cmr/m/n/10 (exp)((\OMS/cmsy/m/n/10 M \OT1/cmr/m/n/10 
+ 1)) = (\OMS/cmsy/m/n/10 X ^^C
 []


Underfull \hbox (badness 3364) in paragraph at lines 6545--6545
[]$\OT1/cmr/m/n/10 0 \OML/cmm/m/it/10 < \OMS/cmsy/m/n/10 X\OT1/cmr/m/n/10 (exp)
\OMS/cmsy/m/n/10 M ) \OT1/cmr/m/n/10 0 \OML/cmm/m/it/10 <
 []

\lgwproofline=\count126

Underfull \hbox (badness 3364) in paragraph at lines 6684--6684
[]$\OT1/cmr/m/n/10 0 \OML/cmm/m/it/10 < \OMS/cmsy/m/n/10 X\OT1/cmr/m/n/10 (exp)
\OMS/cmsy/m/n/10 M ) \OT1/cmr/m/n/10 0 \OML/cmm/m/it/10 <
 []

[8]
\lgwproofline=\count127
\lgwproofline=\count128
\lgwproofline=\count129

Underfull \hbox (badness 2326) in paragraph at lines 7274--7274
[]$\OT1/cmr/m/n/10 0 = N[] \OMS/cmsy/m/n/10 ) \OT1/cmr/m/n/10 BS(\OMS/cmsy/m/n/
10 M\OML/cmm/m/it/10 ; \OT1/cmr/m/n/10 0) =
 []


Overfull \hbox (28.10127pt too wide) in paragraph at lines 7358--7394
[]$\OT1/cmr/m/n/10 [SystemQ[]SameBS(2)(Indu): ^^E\OMS/cmsy/m/n/10 M\OML/cmm/m/i
t/10 ; \OT1/cmr/m/n/10 N[]\OML/cmm/m/it/10 ; \OT1/cmr/m/n/10 N[]: \OMS/cmsy/m/n
/10 8\OT1/cmr/m/n/10 N[]: (N[] = N[] \OMS/cmsy/m/n/10 ) \OT1/cmr/m/n/10 BS(\OMS
/cmsy/m/n/10 M\OML/cmm/m/it/10 ; \OT1/cmr/m/n/10 N[]) =|
 []

\lgwproofline=\count130

Underfull \hbox (badness 10000) in paragraph at lines 7466--7466
[]$\OMS/cmsy/m/n/10 8\OT1/cmr/m/n/10 N[]: (N[] = N[] \OMS/cmsy/m/n/10 )
 []


Underfull \hbox (badness 7133) in paragraph at lines 7466--7466
\OT1/cmr/m/n/10 BS(\OMS/cmsy/m/n/10 M\OML/cmm/m/it/10 ; \OT1/cmr/m/n/10 N[]) = 
BS(\OMS/cmsy/m/n/10 M\OML/cmm/m/it/10 ; \OT1/cmr/m/n/10 N[]))$
 []


Underfull \hbox (badness 10000) in paragraph at lines 7535--7535
[]$\OT1/cmr/m/n/10 BS(\OMS/cmsy/m/n/10 M\OML/cmm/m/it/10 ; \OT1/cmr/m/n/10 (N[]
 + 1)) =
 []


Underfull \hbox (badness 2608) in paragraph at lines 7592--7592
[]$\OT1/cmr/m/n/10 N[] = ((N[] + 1) \OMS/cmsy/m/n/10 ^^@ \OT1/cmr/m/n/10 1) \OM
S/cmsy/m/n/10 )
 []


Underfull \hbox (badness 6188) in paragraph at lines 7654--7654
[]$\OT1/cmr/m/n/10 BS(\OMS/cmsy/m/n/10 M\OML/cmm/m/it/10 ; \OT1/cmr/m/n/10 ((N[
] + 1) \OMS/cmsy/m/n/10 ^^@ \OT1/cmr/m/n/10 1)) =
 []


Underfull \hbox (badness 3989) in paragraph at lines 7704--7704
\OT1/cmr/m/n/10 BS(\OMS/cmsy/m/n/10 M\OML/cmm/m/it/10 ; \OT1/cmr/m/n/10 ((N[] +
 1) \OMS/cmsy/m/n/10 ^^@ \OT1/cmr/m/n/10 1))) =
 []


Underfull \hbox (badness 10000) in paragraph at lines 7947--7947
[]$\OT1/cmr/m/n/10 (1\OML/cmm/m/it/10 =\OT1/cmr/m/n/10 2(exp)((\OMS/cmsy/m/n/10
 M \OT1/cmr/m/n/10 + ((N[] +
 []


Underfull \hbox (badness 1281) in paragraph at lines 7947--7947
\OT1/cmr/m/n/10 1)))) + BS(\OMS/cmsy/m/n/10 M\OML/cmm/m/it/10 ; \OT1/cmr/m/n/10
 (N[] \OMS/cmsy/m/n/10 ^^@ \OT1/cmr/m/n/10 1))) =
 []


Underfull \hbox (badness 10000) in paragraph at lines 7947--7947
\OT1/cmr/m/n/10 (1\OML/cmm/m/it/10 =\OT1/cmr/m/n/10 2(exp)((\OMS/cmsy/m/n/10 M 
\OT1/cmr/m/n/10 + N[])) +
 []


Underfull \hbox (badness 10000) in paragraph at lines 8039--8039
[]$\OT1/cmr/m/n/10 (1\OML/cmm/m/it/10 =\OT1/cmr/m/n/10 2(exp)((\OMS/cmsy/m/n/10
 M \OT1/cmr/m/n/10 + N[])) +
 []


Underfull \hbox (badness 10000) in paragraph at lines 8142--8142
[]$\OMS/cmsy/m/n/10 8\OT1/cmr/m/n/10 N[]: (N[] = N[] \OMS/cmsy/m/n/10 )
 []


Underfull \hbox (badness 10000) in paragraph at lines 8142--8142
\OT1/cmr/m/n/10 (N[] + 1) = N[] \OMS/cmsy/m/n/10 )
 []


Underfull \hbox (badness 10000) in paragraph at lines 8162--8162
[]$\OMS/cmsy/m/n/10 8\OT1/cmr/m/n/10 N[]: (N[] = N[] \OMS/cmsy/m/n/10 )
 []


Underfull \hbox (badness 7133) in paragraph at lines 8162--8162
\OT1/cmr/m/n/10 BS(\OMS/cmsy/m/n/10 M\OML/cmm/m/it/10 ; \OT1/cmr/m/n/10 N[]) = 
BS(\OMS/cmsy/m/n/10 M\OML/cmm/m/it/10 ; \OT1/cmr/m/n/10 N[]))$
 []


Underfull \hbox (badness 4316) in paragraph at lines 8231--8231
[]$\OMS/cmsy/m/n/10 8\OT1/cmr/m/n/10 N[]: ((N[] + 1) = N[] \OMS/cmsy/m/n/10 )
 []


Underfull \hbox (badness 10000) in paragraph at lines 8298--8298
[]$\OMS/cmsy/m/n/10 8\OT1/cmr/m/n/10 N[]: (N[] = N[] \OMS/cmsy/m/n/10 )
 []


Underfull \hbox (badness 4316) in paragraph at lines 8298--8298
\OMS/cmsy/m/n/10 8\OT1/cmr/m/n/10 N[]: ((N[] + 1) = N[] \OMS/cmsy/m/n/10 )
 []

[9] [10]
Overfull \hbox (24.69348pt too wide) in paragraph at lines 8353--8369
[]$\OT1/cmr/m/n/10 [SystemQ[]SameBS(2): ^^E\OMS/cmsy/m/n/10 M\OML/cmm/m/it/10 ;
 \OT1/cmr/m/n/10 N[]\OML/cmm/m/it/10 ; \OT1/cmr/m/n/10 N[]: N[] = N[] \OMS/cmsy
/m/n/10 ` \OT1/cmr/m/n/10 BS(\OMS/cmsy/m/n/10 M\OML/cmm/m/it/10 ; \OT1/cmr/m/n/
10 N[]) = BS(\OMS/cmsy/m/n/10 M\OML/cmm/m/it/10 ; \OT1/cmr/m/n/10 N[])]$ |
 []

\lgwproofline=\count131

Underfull \hbox (badness 10000) in paragraph at lines 8463--8463
[]$\OMS/cmsy/m/n/10 8\OT1/cmr/m/n/10 N[]: (N[] = N[] \OMS/cmsy/m/n/10 )
 []


Underfull \hbox (badness 4316) in paragraph at lines 8463--8463
\OMS/cmsy/m/n/10 8\OT1/cmr/m/n/10 N[]: ((N[] + 1) = N[] \OMS/cmsy/m/n/10 )
 []


Underfull \hbox (badness 10000) in paragraph at lines 8499--8499
[]$\OMS/cmsy/m/n/10 8\OT1/cmr/m/n/10 N[]: (N[] = N[] \OMS/cmsy/m/n/10 )
 []


Underfull \hbox (badness 7133) in paragraph at lines 8499--8499
\OT1/cmr/m/n/10 BS(\OMS/cmsy/m/n/10 M\OML/cmm/m/it/10 ; \OT1/cmr/m/n/10 N[]) = 
BS(\OMS/cmsy/m/n/10 M\OML/cmm/m/it/10 ; \OT1/cmr/m/n/10 N[]))$
 []

\lgwproofline=\count132

Overfull \hbox (2.78476pt too wide) in paragraph at lines 8903--8927
[]$\OT1/cmr/m/n/10 [SystemQ[]BS(+1): ^^E\OMS/cmsy/m/n/10 M\OML/cmm/m/it/10 ; \O
MS/cmsy/m/n/10 N\OT1/cmr/m/n/10 : BS(\OMS/cmsy/m/n/10 M\OML/cmm/m/it/10 ; \OT1/
cmr/m/n/10 (\OMS/cmsy/m/n/10 N \OT1/cmr/m/n/10 + 1)) = (1\OML/cmm/m/it/10 =\OT1
/cmr/m/n/10 2(exp)(((\OMS/cmsy/m/n/10 M \OT1/cmr/m/n/10 + \OMS/cmsy/m/n/10 N\OT
1/cmr/m/n/10 ) +|
 []

\lgwproofline=\count133

Underfull \hbox (badness 10000) in paragraph at lines 9004--9004
[]$\OT1/cmr/m/n/10 BS(\OMS/cmsy/m/n/10 M\OML/cmm/m/it/10 ; \OT1/cmr/m/n/10 (\OM
S/cmsy/m/n/10 N \OT1/cmr/m/n/10 + 1)) =
 []


Underfull \hbox (badness 7814) in paragraph at lines 9174--9174
[]$\OT1/cmr/m/n/10 BS(\OMS/cmsy/m/n/10 M\OML/cmm/m/it/10 ; \OT1/cmr/m/n/10 ((\O
MS/cmsy/m/n/10 N \OT1/cmr/m/n/10 + 1) \OMS/cmsy/m/n/10 ^^@ \OT1/cmr/m/n/10 1)) 
=
 []


Underfull \hbox (badness 5217) in paragraph at lines 9228--9228
\OT1/cmr/m/n/10 BS(\OMS/cmsy/m/n/10 M\OML/cmm/m/it/10 ; \OT1/cmr/m/n/10 ((\OMS/
cmsy/m/n/10 N \OT1/cmr/m/n/10 + 1) \OMS/cmsy/m/n/10 ^^@ \OT1/cmr/m/n/10 1))) =
 []


Underfull \hbox (badness 10000) in paragraph at lines 9268--9268
[]$\OT1/cmr/m/n/10 BS(\OMS/cmsy/m/n/10 M\OML/cmm/m/it/10 ; \OT1/cmr/m/n/10 (\OM
S/cmsy/m/n/10 N \OT1/cmr/m/n/10 + 1)) =
 []

[11]
Overfull \hbox (25.47186pt too wide) in paragraph at lines 9324--9346
[]$\OT1/cmr/m/n/10 [SystemQ[]BSbound(Exact)(Base): ^^E\OMS/cmsy/m/n/10 M\OT1/cm
r/m/n/10 : (BS((\OMS/cmsy/m/n/10 M \OT1/cmr/m/n/10 + 1)\OML/cmm/m/it/10 ; \OT1/
cmr/m/n/10 0) + 1\OML/cmm/m/it/10 =\OT1/cmr/m/n/10 2(exp)(((\OMS/cmsy/m/n/10 M 
\OT1/cmr/m/n/10 +|
 []

\lgwproofline=\count134

Underfull \hbox (badness 10000) in paragraph at lines 9387--9387
[]$\OT1/cmr/m/n/10 BS((\OMS/cmsy/m/n/10 M \OT1/cmr/m/n/10 + 1)\OML/cmm/m/it/10 
; \OT1/cmr/m/n/10 0) =
 []


Underfull \hbox (badness 4518) in paragraph at lines 9442--9442
[]$\OT1/cmr/m/n/10 BS((\OMS/cmsy/m/n/10 M \OT1/cmr/m/n/10 + 1)\OML/cmm/m/it/10 
; \OT1/cmr/m/n/10 0) = (1\OML/cmm/m/it/10 =\OT1/cmr/m/n/10 2 \OMS/cmsy/m/n/10 ^
^C
 []


Underfull \hbox (badness 1997) in paragraph at lines 9494--9494
[]$\OT1/cmr/m/n/10 1\OML/cmm/m/it/10 =\OT1/cmr/m/n/10 2(exp)(((\OMS/cmsy/m/n/10
 M \OT1/cmr/m/n/10 + 1) + 0)) =
 []


Underfull \hbox (badness 10000) in paragraph at lines 9577--9577
[]$\OT1/cmr/m/n/10 (BS((\OMS/cmsy/m/n/10 M \OT1/cmr/m/n/10 + 1)\OML/cmm/m/it/10
 ; \OT1/cmr/m/n/10 0) +
 []


Underfull \hbox (badness 1028) in paragraph at lines 9577--9577
\OT1/cmr/m/n/10 1\OML/cmm/m/it/10 =\OT1/cmr/m/n/10 2(exp)(((\OMS/cmsy/m/n/10 M 
\OT1/cmr/m/n/10 + 1) + 0))) =
 []


Underfull \hbox (badness 1430) in paragraph at lines 9577--9577
\OT1/cmr/m/n/10 ((1\OML/cmm/m/it/10 =\OT1/cmr/m/n/10 2 \OMS/cmsy/m/n/10 ^^C \OT
1/cmr/m/n/10 1\OML/cmm/m/it/10 =\OT1/cmr/m/n/10 2(exp)\OMS/cmsy/m/n/10 M\OT1/cm
r/m/n/10 ) + (1\OML/cmm/m/it/10 =\OT1/cmr/m/n/10 2 \OMS/cmsy/m/n/10 ^^C
 []


Underfull \hbox (badness 1430) in paragraph at lines 9600--9600
[]$\OT1/cmr/m/n/10 ((1\OML/cmm/m/it/10 =\OT1/cmr/m/n/10 2 \OMS/cmsy/m/n/10 ^^C 
\OT1/cmr/m/n/10 1\OML/cmm/m/it/10 =\OT1/cmr/m/n/10 2(exp)\OMS/cmsy/m/n/10 M\OT1
/cmr/m/n/10 ) + (1\OML/cmm/m/it/10 =\OT1/cmr/m/n/10 2 \OMS/cmsy/m/n/10 ^^C
 []


Underfull \hbox (badness 10000) in paragraph at lines 9639--9639
[]$\OT1/cmr/m/n/10 (BS((\OMS/cmsy/m/n/10 M \OT1/cmr/m/n/10 + 1)\OML/cmm/m/it/10
 ; \OT1/cmr/m/n/10 0) +
 []


Underfull \hbox (badness 1028) in paragraph at lines 9639--9639
\OT1/cmr/m/n/10 1\OML/cmm/m/it/10 =\OT1/cmr/m/n/10 2(exp)(((\OMS/cmsy/m/n/10 M 
\OT1/cmr/m/n/10 + 1) + 0))) =
 []


Overfull \hbox (44.0788pt too wide) in paragraph at lines 9695--9738
[]$\OT1/cmr/m/n/10 [SystemQ[]BSbound(Exact)(Indu): ^^E\OMS/cmsy/m/n/10 M\OML/cm
m/m/it/10 ; \OMS/cmsy/m/n/10 N\OT1/cmr/m/n/10 : (BS((\OMS/cmsy/m/n/10 M \OT1/cm
r/m/n/10 + 1)\OML/cmm/m/it/10 ; \OMS/cmsy/m/n/10 N\OT1/cmr/m/n/10 ) + 1\OML/cmm
/m/it/10 =\OT1/cmr/m/n/10 2(exp)(((\OMS/cmsy/m/n/10 M \OT1/cmr/m/n/10 +|
 []

\lgwproofline=\count135

Underfull \hbox (badness 10000) in paragraph at lines 9792--9792
[]$\OT1/cmr/m/n/10 (BS((\OMS/cmsy/m/n/10 M \OT1/cmr/m/n/10 + 1)\OML/cmm/m/it/10
 ; \OMS/cmsy/m/n/10 N\OT1/cmr/m/n/10 ) +
 []


Underfull \hbox (badness 7814) in paragraph at lines 9827--9827
[]$\OT1/cmr/m/n/10 BS((\OMS/cmsy/m/n/10 M \OT1/cmr/m/n/10 + 1)\OML/cmm/m/it/10 
; \OT1/cmr/m/n/10 (\OMS/cmsy/m/n/10 N \OT1/cmr/m/n/10 + 1)) =
 []


Underfull \hbox (badness 10000) in paragraph at lines 9890--9890
[]$\OT1/cmr/m/n/10 (BS((\OMS/cmsy/m/n/10 M \OT1/cmr/m/n/10 + 1)\OML/cmm/m/it/10
 ; \OT1/cmr/m/n/10 (\OMS/cmsy/m/n/10 N \OT1/cmr/m/n/10 + 1)) +
 []


Underfull \hbox (badness 2158) in paragraph at lines 9890--9890
\OT1/cmr/m/n/10 1\OML/cmm/m/it/10 =\OT1/cmr/m/n/10 2(exp)((((\OMS/cmsy/m/n/10 M
 \OT1/cmr/m/n/10 + 1) + \OMS/cmsy/m/n/10 N\OT1/cmr/m/n/10 ) +
 []


Underfull \hbox (badness 10000) in paragraph at lines 10006--10006
\OT1/cmr/m/n/10 1)) + BS((\OMS/cmsy/m/n/10 M \OT1/cmr/m/n/10 + 1)\OML/cmm/m/it/
10 ; \OMS/cmsy/m/n/10 N\OT1/cmr/m/n/10 )) +
 []


Underfull \hbox (badness 2158) in paragraph at lines 10006--10006
\OT1/cmr/m/n/10 1\OML/cmm/m/it/10 =\OT1/cmr/m/n/10 2(exp)((((\OMS/cmsy/m/n/10 M
 \OT1/cmr/m/n/10 + 1) + \OMS/cmsy/m/n/10 N\OT1/cmr/m/n/10 ) +
 []


Underfull \hbox (badness 10000) in paragraph at lines 10104--10104
\OT1/cmr/m/n/10 1)) + 1\OML/cmm/m/it/10 =\OT1/cmr/m/n/10 2(exp)((((\OMS/cmsy/m/
n/10 M \OT1/cmr/m/n/10 +
 []


Underfull \hbox (badness 2189) in paragraph at lines 10104--10104
\OT1/cmr/m/n/10 1) + \OMS/cmsy/m/n/10 N\OT1/cmr/m/n/10 ) + 1))) = ((1\OML/cmm/m
/it/10 =\OT1/cmr/m/n/10 2 \OMS/cmsy/m/n/10 ^^C
 []


Underfull \hbox (badness 1259) in paragraph at lines 10145--10145
[]$\OT1/cmr/m/n/10 ((1\OML/cmm/m/it/10 =\OT1/cmr/m/n/10 2 \OMS/cmsy/m/n/10 ^^C 
\OT1/cmr/m/n/10 1\OML/cmm/m/it/10 =\OT1/cmr/m/n/10 2(exp)(((\OMS/cmsy/m/n/10 M 
\OT1/cmr/m/n/10 + 1) +
 []


Underfull \hbox (badness 10000) in paragraph at lines 10257--10257
[]$\OT1/cmr/m/n/10 ((BS((\OMS/cmsy/m/n/10 M \OT1/cmr/m/n/10 + 1)\OML/cmm/m/it/1
0 ; \OMS/cmsy/m/n/10 N\OT1/cmr/m/n/10 ) +
 []


Underfull \hbox (badness 2158) in paragraph at lines 10257--10257
\OT1/cmr/m/n/10 1\OML/cmm/m/it/10 =\OT1/cmr/m/n/10 2(exp)((((\OMS/cmsy/m/n/10 M
 \OT1/cmr/m/n/10 + 1) + \OMS/cmsy/m/n/10 N\OT1/cmr/m/n/10 ) +
 []


Underfull \hbox (badness 1102) in paragraph at lines 10257--10257
\OT1/cmr/m/n/10 1))) + 1\OML/cmm/m/it/10 =\OT1/cmr/m/n/10 2(exp)((((\OMS/cmsy/m
/n/10 M \OT1/cmr/m/n/10 + 1) +
 []


Underfull \hbox (badness 10000) in paragraph at lines 10312--10312
[]$\OT1/cmr/m/n/10 (BS((\OMS/cmsy/m/n/10 M \OT1/cmr/m/n/10 + 1)\OML/cmm/m/it/10
 ; \OT1/cmr/m/n/10 (\OMS/cmsy/m/n/10 N \OT1/cmr/m/n/10 + 1)) +
 []


Underfull \hbox (badness 2158) in paragraph at lines 10312--10312
\OT1/cmr/m/n/10 1\OML/cmm/m/it/10 =\OT1/cmr/m/n/10 2(exp)((((\OMS/cmsy/m/n/10 M
 \OT1/cmr/m/n/10 + 1) + \OMS/cmsy/m/n/10 N\OT1/cmr/m/n/10 ) +
 []


Underfull \hbox (badness 10000) in paragraph at lines 10386--10386
[]$\OT1/cmr/m/n/10 (BS((\OMS/cmsy/m/n/10 M \OT1/cmr/m/n/10 + 1)\OML/cmm/m/it/10
 ; \OMS/cmsy/m/n/10 N\OT1/cmr/m/n/10 ) +
 []


Underfull \hbox (badness 5970) in paragraph at lines 10386--10386
\OT1/cmr/m/n/10 1\OML/cmm/m/it/10 =\OT1/cmr/m/n/10 2(exp)\OMS/cmsy/m/n/10 M ) \
OT1/cmr/m/n/10 (BS((\OMS/cmsy/m/n/10 M \OT1/cmr/m/n/10 +
 []

[12] [13]
Overfull \hbox (16.02316pt too wide) in paragraph at lines 10441--10464
[]$\OT1/cmr/m/n/10 [SystemQ[]BSbound(Exact): ^^E\OMS/cmsy/m/n/10 M\OML/cmm/m/it
/10 ; \OMS/cmsy/m/n/10 N\OT1/cmr/m/n/10 : (BS((\OMS/cmsy/m/n/10 M \OT1/cmr/m/n/
10 + 1)\OML/cmm/m/it/10 ; \OMS/cmsy/m/n/10 N\OT1/cmr/m/n/10 ) + 1\OML/cmm/m/it/
10 =\OT1/cmr/m/n/10 2(exp)(((\OMS/cmsy/m/n/10 M \OT1/cmr/m/n/10 +|
 []

\lgwproofline=\count136

Underfull \hbox (badness 10000) in paragraph at lines 10512--10512
[]$\OT1/cmr/m/n/10 (BS((\OMS/cmsy/m/n/10 M \OT1/cmr/m/n/10 + 1)\OML/cmm/m/it/10
 ; \OT1/cmr/m/n/10 0) +
 []


Underfull \hbox (badness 1028) in paragraph at lines 10512--10512
\OT1/cmr/m/n/10 1\OML/cmm/m/it/10 =\OT1/cmr/m/n/10 2(exp)(((\OMS/cmsy/m/n/10 M 
\OT1/cmr/m/n/10 + 1) + 0))) =
 []


Underfull \hbox (badness 10000) in paragraph at lines 10560--10560
[]$\OT1/cmr/m/n/10 (BS((\OMS/cmsy/m/n/10 M \OT1/cmr/m/n/10 + 1)\OML/cmm/m/it/10
 ; \OMS/cmsy/m/n/10 N\OT1/cmr/m/n/10 ) +
 []


Underfull \hbox (badness 5970) in paragraph at lines 10560--10560
\OT1/cmr/m/n/10 1\OML/cmm/m/it/10 =\OT1/cmr/m/n/10 2(exp)\OMS/cmsy/m/n/10 M ) \
OT1/cmr/m/n/10 (BS((\OMS/cmsy/m/n/10 M \OT1/cmr/m/n/10 +
 []


Underfull \hbox (badness 10000) in paragraph at lines 10599--10599
[]$\OT1/cmr/m/n/10 (BS((\OMS/cmsy/m/n/10 M \OT1/cmr/m/n/10 + 1)\OML/cmm/m/it/10
 ; \OMS/cmsy/m/n/10 N\OT1/cmr/m/n/10 ) +
 []

\lgwproofline=\count137

Underfull \hbox (badness 10000) in paragraph at lines 10716--10716
[]$\OT1/cmr/m/n/10 (BS((\OMS/cmsy/m/n/10 M \OT1/cmr/m/n/10 + 1)\OML/cmm/m/it/10
 ; \OMS/cmsy/m/n/10 N\OT1/cmr/m/n/10 ) +
 []

\lgwproofline=\count138
[14]
Overfull \hbox (29.36043pt too wide) in paragraph at lines 11261--11280
[]$\OT1/cmr/m/n/10 [SystemQ[]UStelescope(Zero)(Exact): ^^E\OMS/cmsy/m/n/10 M\OT
1/cmr/m/n/10 : UStelescope(\OMS/cmsy/m/n/10 M\OML/cmm/m/it/10 ; \OT1/cmr/m/n/10
 0) = \OMS/cmsy/m/n/10 j\OT1/cmr/m/n/10 (us[\OMS/cmsy/m/n/10 M\OT1/cmr/m/n/10 ]
 \OMS/cmsy/m/n/10 ^^@|
 []

\lgwproofline=\count139

Overfull \hbox (66.61514pt too wide) in paragraph at lines 11397--11415
[]$\OT1/cmr/m/n/10 [SystemQ[]SameTelescope(2)(Base): ^^E\OMS/cmsy/m/n/10 M\OML/
cmm/m/it/10 ; \OT1/cmr/m/n/10 N[]: \OMS/cmsy/m/n/10 8\OT1/cmr/m/n/10 N[]: (0 = 
N[] \OMS/cmsy/m/n/10 ) \OT1/cmr/m/n/10 UStelescope(\OMS/cmsy/m/n/10 M\OML/cmm/m
/it/10 ; \OT1/cmr/m/n/10 0) =|
 []

\lgwproofline=\count140

Underfull \hbox (badness 10000) in paragraph at lines 11506--11506
[]$\OT1/cmr/m/n/10 UStelescope(\OMS/cmsy/m/n/10 M\OML/cmm/m/it/10 ; \OT1/cmr/m/
n/10 N[]) =
 []


Underfull \hbox (badness 10000) in paragraph at lines 11506--11506
\OMS/cmsy/m/n/10 j\OT1/cmr/m/n/10 (us[\OMS/cmsy/m/n/10 M\OT1/cmr/m/n/10 ] \OMS/
cmsy/m/n/10 ^^@ \OT1/cmr/m/n/10 us[(\OMS/cmsy/m/n/10 M \OT1/cmr/m/n/10 + 1)])\O
MS/cmsy/m/n/10 j$
 []


Underfull \hbox (badness 3118) in paragraph at lines 11537--11537
[]$\OMS/cmsy/m/n/10 j\OT1/cmr/m/n/10 (us[\OMS/cmsy/m/n/10 M\OT1/cmr/m/n/10 ] \O
MS/cmsy/m/n/10 ^^@ \OT1/cmr/m/n/10 us[(\OMS/cmsy/m/n/10 M \OT1/cmr/m/n/10 + 1)]
)\OMS/cmsy/m/n/10 j \OT1/cmr/m/n/10 =
 []


Underfull \hbox (badness 10000) in paragraph at lines 11591--11591
[]$\OT1/cmr/m/n/10 UStelescope(\OMS/cmsy/m/n/10 M\OML/cmm/m/it/10 ; \OT1/cmr/m/
n/10 0) =
 []


Underfull \hbox (badness 10000) in paragraph at lines 11666--11666
[]$\OMS/cmsy/m/n/10 8\OT1/cmr/m/n/10 N[]: (0 = N[] \OMS/cmsy/m/n/10 )
 []


Underfull \hbox (badness 10000) in paragraph at lines 11666--11666
\OT1/cmr/m/n/10 UStelescope(\OMS/cmsy/m/n/10 M\OML/cmm/m/it/10 ; \OT1/cmr/m/n/1
0 0) =
 []


Overfull \hbox (60.33258pt too wide) in paragraph at lines 11721--11755
\OT1/cmr/m/n/10 UStelescope(\OMS/cmsy/m/n/10 M\OML/cmm/m/it/10 ; \OT1/cmr/m/n/1
0 N[]) = UStelescope(\OMS/cmsy/m/n/10 M\OML/cmm/m/it/10 ; \OT1/cmr/m/n/10 N[]))
 \OMS/cmsy/m/n/10 ) 8\OT1/cmr/m/n/10 N[]: ((N[] + 1) = N[] \OMS/cmsy/m/n/10 ) \
OT1/cmr/m/n/10 UStelescope(\OMS/cmsy/m/n/10 M\OML/cmm/m/it/10 ; \OT1/cmr/m/n/10
 (N[] +|
 []

\lgwproofline=\count141

Underfull \hbox (badness 10000) in paragraph at lines 11826--11826
[]$\OMS/cmsy/m/n/10 8\OT1/cmr/m/n/10 N[]: (N[] = N[] \OMS/cmsy/m/n/10 )
 []


Underfull \hbox (badness 10000) in paragraph at lines 11826--11826
\OT1/cmr/m/n/10 UStelescope(\OMS/cmsy/m/n/10 M\OML/cmm/m/it/10 ; \OT1/cmr/m/n/1
0 N[]) =
 []


Underfull \hbox (badness 2165) in paragraph at lines 11905--11905
[]$\OT1/cmr/m/n/10 UStelescope(\OMS/cmsy/m/n/10 M\OML/cmm/m/it/10 ; \OT1/cmr/m/
n/10 (N[] + 1)) =
 []


Underfull \hbox (badness 10000) in paragraph at lines 11905--11905
\OT1/cmr/m/n/10 (\OMS/cmsy/m/n/10 j\OT1/cmr/m/n/10 (us[(\OMS/cmsy/m/n/10 M \OT1
/cmr/m/n/10 + ((N[] + 1)))] \OMS/cmsy/m/n/10 ^^@
 []


Underfull \hbox (badness 2608) in paragraph at lines 11962--11962
[]$\OT1/cmr/m/n/10 N[] = ((N[] + 1) \OMS/cmsy/m/n/10 ^^@ \OT1/cmr/m/n/10 1) \OM
S/cmsy/m/n/10 )
 []


Underfull \hbox (badness 10000) in paragraph at lines 11962--11962
\OT1/cmr/m/n/10 UStelescope(\OMS/cmsy/m/n/10 M\OML/cmm/m/it/10 ; \OT1/cmr/m/n/1
0 N[]) =
 []


Underfull \hbox (badness 10000) in paragraph at lines 11996--11996
[]$\OT1/cmr/m/n/10 UStelescope(\OMS/cmsy/m/n/10 M\OML/cmm/m/it/10 ; \OT1/cmr/m/
n/10 N[]) =
 []


Underfull \hbox (badness 10000) in paragraph at lines 12024--12024
[]$\OT1/cmr/m/n/10 UStelescope(\OMS/cmsy/m/n/10 M\OML/cmm/m/it/10 ; \OT1/cmr/m/
n/10 ((N[] + 1) \OMS/cmsy/m/n/10 ^^@
 []


Underfull \hbox (badness 10000) in paragraph at lines 12079--12079
[]$\OT1/cmr/m/n/10 N[] = (N[] \OMS/cmsy/m/n/10 ^^@ \OT1/cmr/m/n/10 1) \OMS/cmsy
/m/n/10 )
 []


Underfull \hbox (badness 10000) in paragraph at lines 12079--12079
\OT1/cmr/m/n/10 UStelescope(\OMS/cmsy/m/n/10 M\OML/cmm/m/it/10 ; \OT1/cmr/m/n/1
0 N[]) =
 []


Underfull \hbox (badness 10000) in paragraph at lines 12079--12079
\OT1/cmr/m/n/10 UStelescope(\OMS/cmsy/m/n/10 M\OML/cmm/m/it/10 ; \OT1/cmr/m/n/1
0 (N[] \OMS/cmsy/m/n/10 ^^@ \OT1/cmr/m/n/10 1))$
 []


Underfull \hbox (badness 10000) in paragraph at lines 12111--12111
[]$\OT1/cmr/m/n/10 UStelescope(\OMS/cmsy/m/n/10 M\OML/cmm/m/it/10 ; \OT1/cmr/m/
n/10 N[]) =
 []


Underfull \hbox (badness 10000) in paragraph at lines 12111--12111
\OT1/cmr/m/n/10 UStelescope(\OMS/cmsy/m/n/10 M\OML/cmm/m/it/10 ; \OT1/cmr/m/n/1
0 (N[] \OMS/cmsy/m/n/10 ^^@ \OT1/cmr/m/n/10 1))$
 []


Underfull \hbox (badness 10000) in paragraph at lines 12147--12147
[]$\OT1/cmr/m/n/10 UStelescope(\OMS/cmsy/m/n/10 M\OML/cmm/m/it/10 ; \OT1/cmr/m/
n/10 ((N[] + 1) \OMS/cmsy/m/n/10 ^^@
 []


Underfull \hbox (badness 10000) in paragraph at lines 12364--12364
[]$\OT1/cmr/m/n/10 (\OMS/cmsy/m/n/10 j\OT1/cmr/m/n/10 (us[(\OMS/cmsy/m/n/10 M \
OT1/cmr/m/n/10 + ((N[] + 1)))] \OMS/cmsy/m/n/10 ^^@
 []


Underfull \hbox (badness 10000) in paragraph at lines 12364--12364
\OT1/cmr/m/n/10 UStelescope(\OMS/cmsy/m/n/10 M\OML/cmm/m/it/10 ; \OT1/cmr/m/n/1
0 ((N[] + 1) \OMS/cmsy/m/n/10 ^^@
 []


Underfull \hbox (badness 3250) in paragraph at lines 12364--12364
\OT1/cmr/m/n/10 1))) = (\OMS/cmsy/m/n/10 j\OT1/cmr/m/n/10 (us[(\OMS/cmsy/m/n/10
 M \OT1/cmr/m/n/10 + N[])] \OMS/cmsy/m/n/10 ^^@
 []


Underfull \hbox (badness 10000) in paragraph at lines 12364--12364
\OT1/cmr/m/n/10 us[(\OMS/cmsy/m/n/10 M \OT1/cmr/m/n/10 + ((N[] + 1)))])\OMS/cms
y/m/n/10 j \OT1/cmr/m/n/10 +
 []


Underfull \hbox (badness 10000) in paragraph at lines 12432--12432
[]$\OT1/cmr/m/n/10 UStelescope(\OMS/cmsy/m/n/10 M\OML/cmm/m/it/10 ; \OT1/cmr/m/
n/10 N[]) =
 []


Underfull \hbox (badness 2165) in paragraph at lines 12511--12511
[]$\OT1/cmr/m/n/10 UStelescope(\OMS/cmsy/m/n/10 M\OML/cmm/m/it/10 ; \OT1/cmr/m/
n/10 (N[] + 1)) =
 []


Underfull \hbox (badness 10000) in paragraph at lines 12564--12564
[]$\OMS/cmsy/m/n/10 8\OT1/cmr/m/n/10 N[]: (N[] = N[] \OMS/cmsy/m/n/10 )
 []


Underfull \hbox (badness 10000) in paragraph at lines 12564--12564
\OT1/cmr/m/n/10 UStelescope(\OMS/cmsy/m/n/10 M\OML/cmm/m/it/10 ; \OT1/cmr/m/n/1
0 N[]) =
 []


Underfull \hbox (badness 10000) in paragraph at lines 12564--12564
\OT1/cmr/m/n/10 UStelescope(\OMS/cmsy/m/n/10 M\OML/cmm/m/it/10 ; \OT1/cmr/m/n/1
0 N[])) \OMS/cmsy/m/n/10 )
 []


Underfull \hbox (badness 10000) in paragraph at lines 12564--12564
\OT1/cmr/m/n/10 (N[] + 1) = N[] \OMS/cmsy/m/n/10 )
 []


Underfull \hbox (badness 2165) in paragraph at lines 12564--12564
\OT1/cmr/m/n/10 UStelescope(\OMS/cmsy/m/n/10 M\OML/cmm/m/it/10 ; \OT1/cmr/m/n/1
0 (N[] + 1)) =
 []


Underfull \hbox (badness 10000) in paragraph at lines 12583--12583
[]$\OMS/cmsy/m/n/10 8\OT1/cmr/m/n/10 N[]: (N[] = N[] \OMS/cmsy/m/n/10 )
 []


Underfull \hbox (badness 10000) in paragraph at lines 12583--12583
\OT1/cmr/m/n/10 UStelescope(\OMS/cmsy/m/n/10 M\OML/cmm/m/it/10 ; \OT1/cmr/m/n/1
0 N[]) =
 []


Underfull \hbox (badness 10000) in paragraph at lines 12619--12619
[]$\OT1/cmr/m/n/10 (N[] + 1) = N[] \OMS/cmsy/m/n/10 )
 []


Underfull \hbox (badness 2165) in paragraph at lines 12619--12619
\OT1/cmr/m/n/10 UStelescope(\OMS/cmsy/m/n/10 M\OML/cmm/m/it/10 ; \OT1/cmr/m/n/1
0 (N[] + 1)) =
 []


Underfull \hbox (badness 4316) in paragraph at lines 12651--12651
[]$\OMS/cmsy/m/n/10 8\OT1/cmr/m/n/10 N[]: ((N[] + 1) = N[] \OMS/cmsy/m/n/10 )
 []


Underfull \hbox (badness 2165) in paragraph at lines 12651--12651
\OT1/cmr/m/n/10 UStelescope(\OMS/cmsy/m/n/10 M\OML/cmm/m/it/10 ; \OT1/cmr/m/n/1
0 (N[] + 1)) =
 []


Underfull \hbox (badness 10000) in paragraph at lines 12716--12716
[]$\OMS/cmsy/m/n/10 8\OT1/cmr/m/n/10 N[]: (N[] = N[] \OMS/cmsy/m/n/10 )
 []


Underfull \hbox (badness 10000) in paragraph at lines 12716--12716
\OT1/cmr/m/n/10 UStelescope(\OMS/cmsy/m/n/10 M\OML/cmm/m/it/10 ; \OT1/cmr/m/n/1
0 N[]) =
 []


Underfull \hbox (badness 10000) in paragraph at lines 12716--12716
\OT1/cmr/m/n/10 UStelescope(\OMS/cmsy/m/n/10 M\OML/cmm/m/it/10 ; \OT1/cmr/m/n/1
0 N[])) \OMS/cmsy/m/n/10 )
 []


Underfull \hbox (badness 4316) in paragraph at lines 12716--12716
\OMS/cmsy/m/n/10 8\OT1/cmr/m/n/10 N[]: ((N[] + 1) = N[] \OMS/cmsy/m/n/10 )
 []


Underfull \hbox (badness 2165) in paragraph at lines 12716--12716
\OT1/cmr/m/n/10 UStelescope(\OMS/cmsy/m/n/10 M\OML/cmm/m/it/10 ; \OT1/cmr/m/n/1
0 (N[] + 1)) =
 []

[15] [16]
Overfull \hbox (39.00397pt too wide) in paragraph at lines 12771--12787
[]$\OT1/cmr/m/n/10 [SystemQ[]SameTelescope(2): ^^E\OMS/cmsy/m/n/10 M\OML/cmm/m/
it/10 ; \OT1/cmr/m/n/10 N[]\OML/cmm/m/it/10 ; \OT1/cmr/m/n/10 N[]: N[] = N[] \O
MS/cmsy/m/n/10 ` \OT1/cmr/m/n/10 UStelescope(\OMS/cmsy/m/n/10 M\OML/cmm/m/it/10
 ; \OT1/cmr/m/n/10 N[]) =|
 []

\lgwproofline=\count142

Underfull \hbox (badness 10000) in paragraph at lines 12841--12841
[]$\OMS/cmsy/m/n/10 8\OT1/cmr/m/n/10 N[]: (0 = N[] \OMS/cmsy/m/n/10 )
 []


Underfull \hbox (badness 10000) in paragraph at lines 12841--12841
\OT1/cmr/m/n/10 UStelescope(\OMS/cmsy/m/n/10 M\OML/cmm/m/it/10 ; \OT1/cmr/m/n/1
0 0) =
 []


Underfull \hbox (badness 10000) in paragraph at lines 12879--12879
[]$\OMS/cmsy/m/n/10 8\OT1/cmr/m/n/10 N[]: (N[] = N[] \OMS/cmsy/m/n/10 )
 []


Underfull \hbox (badness 10000) in paragraph at lines 12879--12879
\OT1/cmr/m/n/10 UStelescope(\OMS/cmsy/m/n/10 M\OML/cmm/m/it/10 ; \OT1/cmr/m/n/1
0 N[]) =
 []


Underfull \hbox (badness 10000) in paragraph at lines 12879--12879
\OT1/cmr/m/n/10 UStelescope(\OMS/cmsy/m/n/10 M\OML/cmm/m/it/10 ; \OT1/cmr/m/n/1
0 N[])) \OMS/cmsy/m/n/10 )
 []


Underfull \hbox (badness 4316) in paragraph at lines 12879--12879
\OMS/cmsy/m/n/10 8\OT1/cmr/m/n/10 N[]: ((N[] + 1) = N[] \OMS/cmsy/m/n/10 )
 []


Underfull \hbox (badness 2165) in paragraph at lines 12879--12879
\OT1/cmr/m/n/10 UStelescope(\OMS/cmsy/m/n/10 M\OML/cmm/m/it/10 ; \OT1/cmr/m/n/1
0 (N[] + 1)) =
 []


Underfull \hbox (badness 10000) in paragraph at lines 12914--12914
[]$\OMS/cmsy/m/n/10 8\OT1/cmr/m/n/10 N[]: (N[] = N[] \OMS/cmsy/m/n/10 )
 []


Underfull \hbox (badness 10000) in paragraph at lines 12914--12914
\OT1/cmr/m/n/10 UStelescope(\OMS/cmsy/m/n/10 M\OML/cmm/m/it/10 ; \OT1/cmr/m/n/1
0 N[]) =
 []


Underfull \hbox (badness 10000) in paragraph at lines 12941--12941
[]$\OT1/cmr/m/n/10 N[] = N[] \OMS/cmsy/m/n/10 )
 []


Underfull \hbox (badness 10000) in paragraph at lines 12941--12941
\OT1/cmr/m/n/10 UStelescope(\OMS/cmsy/m/n/10 M\OML/cmm/m/it/10 ; \OT1/cmr/m/n/1
0 N[]) =
 []


Underfull \hbox (badness 10000) in paragraph at lines 12970--12970
[]$\OT1/cmr/m/n/10 UStelescope(\OMS/cmsy/m/n/10 M\OML/cmm/m/it/10 ; \OT1/cmr/m/
n/10 N[]) =
 []

[17]
\lgwproofline=\count143

Underfull \hbox (badness 3118) in paragraph at lines 13241--13241
[]$\OMS/cmsy/m/n/10 j\OT1/cmr/m/n/10 (us[\OMS/cmsy/m/n/10 M\OT1/cmr/m/n/10 ] \O
MS/cmsy/m/n/10 ^^@ \OT1/cmr/m/n/10 us[(\OMS/cmsy/m/n/10 M \OT1/cmr/m/n/10 + 1)]
)\OMS/cmsy/m/n/10 j \OT1/cmr/m/n/10 =
 []


Underfull \hbox (badness 10000) in paragraph at lines 13348--13348
[]$\OMS/cmsy/m/n/10 j\OT1/cmr/m/n/10 (us[\OMS/cmsy/m/n/10 M\OT1/cmr/m/n/10 ] \O
MS/cmsy/m/n/10 ^^@ \OT1/cmr/m/n/10 us[(\OMS/cmsy/m/n/10 M \OT1/cmr/m/n/10 + ((0
 +
 []


Overfull \hbox (11.63414pt too wide) in paragraph at lines 13403--13446
[]$\OT1/cmr/m/n/10 [SystemQ[]TelescopeNumerical(Indu): ^^E\OMS/cmsy/m/n/10 M\OM
L/cmm/m/it/10 ; \OMS/cmsy/m/n/10 N\OT1/cmr/m/n/10 : \OMS/cmsy/m/n/10 j\OT1/cmr/
m/n/10 (us[\OMS/cmsy/m/n/10 M\OT1/cmr/m/n/10 ] \OMS/cmsy/m/n/10 ^^@ \OT1/cmr/m/
n/10 us[(\OMS/cmsy/m/n/10 M \OT1/cmr/m/n/10 + ((\OMS/cmsy/m/n/10 N \OT1/cmr/m/n
/10 +|
 []

\lgwproofline=\count144

Underfull \hbox (badness 10000) in paragraph at lines 13500--13500
[]$\OMS/cmsy/m/n/10 j\OT1/cmr/m/n/10 (us[\OMS/cmsy/m/n/10 M\OT1/cmr/m/n/10 ] \O
MS/cmsy/m/n/10 ^^@ \OT1/cmr/m/n/10 us[(\OMS/cmsy/m/n/10 M \OT1/cmr/m/n/10 + ((\
OMS/cmsy/m/n/10 N \OT1/cmr/m/n/10 +
 []


Underfull \hbox (badness 3428) in paragraph at lines 13567--13567
[]$\OT1/cmr/m/n/10 UStelescope(\OMS/cmsy/m/n/10 M\OML/cmm/m/it/10 ; \OT1/cmr/m/
n/10 (\OMS/cmsy/m/n/10 N \OT1/cmr/m/n/10 + 1)) =
 []


Underfull \hbox (badness 10000) in paragraph at lines 13567--13567
\OT1/cmr/m/n/10 (\OMS/cmsy/m/n/10 j\OT1/cmr/m/n/10 (us[(\OMS/cmsy/m/n/10 M \OT1
/cmr/m/n/10 + ((\OMS/cmsy/m/n/10 N \OT1/cmr/m/n/10 + 1)))] \OMS/cmsy/m/n/10 ^^@

 []


Underfull \hbox (badness 10000) in paragraph at lines 13707--13707
[]$\OT1/cmr/m/n/10 (\OMS/cmsy/m/n/10 j\OT1/cmr/m/n/10 (us[(\OMS/cmsy/m/n/10 M \
OT1/cmr/m/n/10 + ((\OMS/cmsy/m/n/10 N \OT1/cmr/m/n/10 + 1)))] \OMS/cmsy/m/n/10 
^^@
 []


Underfull \hbox (badness 10000) in paragraph at lines 13707--13707
\OT1/cmr/m/n/10 UStelescope(\OMS/cmsy/m/n/10 M\OML/cmm/m/it/10 ; \OT1/cmr/m/n/1
0 ((\OMS/cmsy/m/n/10 N \OT1/cmr/m/n/10 + 1) \OMS/cmsy/m/n/10 ^^@
 []


Underfull \hbox (badness 3428) in paragraph at lines 13760--13760
[]$\OT1/cmr/m/n/10 UStelescope(\OMS/cmsy/m/n/10 M\OML/cmm/m/it/10 ; \OT1/cmr/m/
n/10 (\OMS/cmsy/m/n/10 N \OT1/cmr/m/n/10 + 1)) =
 []


Underfull \hbox (badness 10000) in paragraph at lines 13760--13760
\OT1/cmr/m/n/10 (\OMS/cmsy/m/n/10 j\OT1/cmr/m/n/10 (us[(\OMS/cmsy/m/n/10 M \OT1
/cmr/m/n/10 + ((\OMS/cmsy/m/n/10 N \OT1/cmr/m/n/10 + 1)))] \OMS/cmsy/m/n/10 ^^@

 []


Underfull \hbox (badness 10000) in paragraph at lines 13807--13807
[]$\OT1/cmr/m/n/10 (\OMS/cmsy/m/n/10 j\OT1/cmr/m/n/10 (us[(\OMS/cmsy/m/n/10 M \
OT1/cmr/m/n/10 + ((\OMS/cmsy/m/n/10 N \OT1/cmr/m/n/10 + 1)))] \OMS/cmsy/m/n/10 
^^@
 []


Underfull \hbox (badness 10000) in paragraph at lines 13807--13807
\OT1/cmr/m/n/10 UStelescope(\OMS/cmsy/m/n/10 M\OML/cmm/m/it/10 ; \OMS/cmsy/m/n/
10 N\OT1/cmr/m/n/10 )) =
 []


Underfull \hbox (badness 10000) in paragraph at lines 13807--13807
\OT1/cmr/m/n/10 UStelescope(\OMS/cmsy/m/n/10 M\OML/cmm/m/it/10 ; \OT1/cmr/m/n/1
0 (\OMS/cmsy/m/n/10 N \OT1/cmr/m/n/10 + 1))$
 []


Underfull \hbox (badness 1990) in paragraph at lines 13883--13883
\OT1/cmr/m/n/10 us[(\OMS/cmsy/m/n/10 M \OT1/cmr/m/n/10 + ((\OMS/cmsy/m/n/10 N \
OT1/cmr/m/n/10 + 1)))])\OMS/cmsy/m/n/10 j\OT1/cmr/m/n/10 ) \OML/cmm/m/it/10 <\O
T1/cmr/m/n/10 =
 []


Underfull \hbox (badness 10000) in paragraph at lines 13883--13883
\OT1/cmr/m/n/10 (\OMS/cmsy/m/n/10 j\OT1/cmr/m/n/10 (us[(\OMS/cmsy/m/n/10 M \OT1
/cmr/m/n/10 + ((\OMS/cmsy/m/n/10 N \OT1/cmr/m/n/10 + 1)))] \OMS/cmsy/m/n/10 ^^@

 []


Underfull \hbox (badness 1990) in paragraph at lines 13946--13946
\OT1/cmr/m/n/10 us[(\OMS/cmsy/m/n/10 M \OT1/cmr/m/n/10 + ((\OMS/cmsy/m/n/10 N \
OT1/cmr/m/n/10 + 1)))])\OMS/cmsy/m/n/10 j\OT1/cmr/m/n/10 ) \OML/cmm/m/it/10 <\O
T1/cmr/m/n/10 =
 []


Underfull \hbox (badness 5431) in paragraph at lines 14026--14026
\OT1/cmr/m/n/10 us[(\OMS/cmsy/m/n/10 M \OT1/cmr/m/n/10 + ((\OMS/cmsy/m/n/10 N \
OT1/cmr/m/n/10 + 1)))])\OMS/cmsy/m/n/10 j\OT1/cmr/m/n/10 ) =
 []


Underfull \hbox (badness 4872) in paragraph at lines 14026--14026
\OT1/cmr/m/n/10 (\OMS/cmsy/m/n/10 j\OT1/cmr/m/n/10 (us[\OMS/cmsy/m/n/10 M\OT1/c
mr/m/n/10 ] \OMS/cmsy/m/n/10 ^^@ \OT1/cmr/m/n/10 us[(\OMS/cmsy/m/n/10 M \OT1/cm
r/m/n/10 + ((\OMS/cmsy/m/n/10 N \OT1/cmr/m/n/10 +
 []


Underfull \hbox (badness 4872) in paragraph at lines 14089--14089
[]$\OT1/cmr/m/n/10 (\OMS/cmsy/m/n/10 j\OT1/cmr/m/n/10 (us[\OMS/cmsy/m/n/10 M\OT
1/cmr/m/n/10 ] \OMS/cmsy/m/n/10 ^^@ \OT1/cmr/m/n/10 us[(\OMS/cmsy/m/n/10 M \OT1
/cmr/m/n/10 + ((\OMS/cmsy/m/n/10 N \OT1/cmr/m/n/10 +
 []


Overfull \hbox (5.19675pt too wide) in paragraph at lines 14100--14100
[][]$\OT1/cmr/m/n/10 insertMiddleTerm(Numerical)[] \OMS/cmsy/m/n/10 ^^] |
 []


Underfull \hbox (badness 10000) in paragraph at lines 14193--14193
[]$\OMS/cmsy/m/n/10 j\OT1/cmr/m/n/10 (us[\OMS/cmsy/m/n/10 M\OT1/cmr/m/n/10 ] \O
MS/cmsy/m/n/10 ^^@ \OT1/cmr/m/n/10 us[(\OMS/cmsy/m/n/10 M \OT1/cmr/m/n/10 +
 []


Underfull \hbox (badness 10000) in paragraph at lines 14193--14193
\OT1/cmr/m/n/10 (((\OMS/cmsy/m/n/10 N \OT1/cmr/m/n/10 + 1) + 1)))])\OMS/cmsy/m/
n/10 j \OML/cmm/m/it/10 <\OT1/cmr/m/n/10 =
 []


Underfull \hbox (badness 10000) in paragraph at lines 14193--14193
\OT1/cmr/m/n/10 UStelescope(\OMS/cmsy/m/n/10 M\OML/cmm/m/it/10 ; \OT1/cmr/m/n/1
0 (\OMS/cmsy/m/n/10 N \OT1/cmr/m/n/10 + 1))$
 []


Underfull \hbox (badness 10000) in paragraph at lines 14267--14267
[]$\OMS/cmsy/m/n/10 j\OT1/cmr/m/n/10 (us[\OMS/cmsy/m/n/10 M\OT1/cmr/m/n/10 ] \O
MS/cmsy/m/n/10 ^^@ \OT1/cmr/m/n/10 us[(\OMS/cmsy/m/n/10 M \OT1/cmr/m/n/10 +
 []


Underfull \hbox (badness 10000) in paragraph at lines 14267--14267
\OT1/cmr/m/n/10 ((\OMS/cmsy/m/n/10 N \OT1/cmr/m/n/10 + 1)))])\OMS/cmsy/m/n/10 j
 \OML/cmm/m/it/10 <\OT1/cmr/m/n/10 =
 []


Underfull \hbox (badness 10000) in paragraph at lines 14267--14267
\OT1/cmr/m/n/10 UStelescope(\OMS/cmsy/m/n/10 M\OML/cmm/m/it/10 ; \OMS/cmsy/m/n/
10 N\OT1/cmr/m/n/10 ) \OMS/cmsy/m/n/10 )
 []


Underfull \hbox (badness 10000) in paragraph at lines 14267--14267
\OMS/cmsy/m/n/10 j\OT1/cmr/m/n/10 (us[\OMS/cmsy/m/n/10 M\OT1/cmr/m/n/10 ] \OMS/
cmsy/m/n/10 ^^@ \OT1/cmr/m/n/10 us[(\OMS/cmsy/m/n/10 M \OT1/cmr/m/n/10 +
 []


Underfull \hbox (badness 10000) in paragraph at lines 14267--14267
\OT1/cmr/m/n/10 (((\OMS/cmsy/m/n/10 N \OT1/cmr/m/n/10 + 1) + 1)))])\OMS/cmsy/m/
n/10 j \OML/cmm/m/it/10 <\OT1/cmr/m/n/10 =
 []


Underfull \hbox (badness 10000) in paragraph at lines 14267--14267
\OT1/cmr/m/n/10 UStelescope(\OMS/cmsy/m/n/10 M\OML/cmm/m/it/10 ; \OT1/cmr/m/n/1
0 (\OMS/cmsy/m/n/10 N \OT1/cmr/m/n/10 + 1))$
 []

[18] [19]
\lgwproofline=\count145

Underfull \hbox (badness 10000) in paragraph at lines 14392--14392
[]$\OMS/cmsy/m/n/10 j\OT1/cmr/m/n/10 (us[\OMS/cmsy/m/n/10 M\OT1/cmr/m/n/10 ] \O
MS/cmsy/m/n/10 ^^@ \OT1/cmr/m/n/10 us[(\OMS/cmsy/m/n/10 M \OT1/cmr/m/n/10 + ((0
 +
 []


Underfull \hbox (badness 10000) in paragraph at lines 14440--14440
[]$\OMS/cmsy/m/n/10 j\OT1/cmr/m/n/10 (us[\OMS/cmsy/m/n/10 M\OT1/cmr/m/n/10 ] \O
MS/cmsy/m/n/10 ^^@ \OT1/cmr/m/n/10 us[(\OMS/cmsy/m/n/10 M \OT1/cmr/m/n/10 +
 []


Underfull \hbox (badness 10000) in paragraph at lines 14440--14440
\OT1/cmr/m/n/10 ((\OMS/cmsy/m/n/10 N \OT1/cmr/m/n/10 + 1)))])\OMS/cmsy/m/n/10 j
 \OML/cmm/m/it/10 <\OT1/cmr/m/n/10 =
 []


Underfull \hbox (badness 10000) in paragraph at lines 14440--14440
\OT1/cmr/m/n/10 UStelescope(\OMS/cmsy/m/n/10 M\OML/cmm/m/it/10 ; \OMS/cmsy/m/n/
10 N\OT1/cmr/m/n/10 ) \OMS/cmsy/m/n/10 )
 []


Underfull \hbox (badness 10000) in paragraph at lines 14440--14440
\OMS/cmsy/m/n/10 j\OT1/cmr/m/n/10 (us[\OMS/cmsy/m/n/10 M\OT1/cmr/m/n/10 ] \OMS/
cmsy/m/n/10 ^^@ \OT1/cmr/m/n/10 us[(\OMS/cmsy/m/n/10 M \OT1/cmr/m/n/10 +
 []


Underfull \hbox (badness 10000) in paragraph at lines 14440--14440
\OT1/cmr/m/n/10 (((\OMS/cmsy/m/n/10 N \OT1/cmr/m/n/10 + 1) + 1)))])\OMS/cmsy/m/
n/10 j \OML/cmm/m/it/10 <\OT1/cmr/m/n/10 =
 []


Underfull \hbox (badness 10000) in paragraph at lines 14440--14440
\OT1/cmr/m/n/10 UStelescope(\OMS/cmsy/m/n/10 M\OML/cmm/m/it/10 ; \OT1/cmr/m/n/1
0 (\OMS/cmsy/m/n/10 N \OT1/cmr/m/n/10 + 1))$
 []


Underfull \hbox (badness 10000) in paragraph at lines 14479--14479
[]$\OMS/cmsy/m/n/10 j\OT1/cmr/m/n/10 (us[\OMS/cmsy/m/n/10 M\OT1/cmr/m/n/10 ] \O
MS/cmsy/m/n/10 ^^@ \OT1/cmr/m/n/10 us[(\OMS/cmsy/m/n/10 M \OT1/cmr/m/n/10 + ((\
OMS/cmsy/m/n/10 N \OT1/cmr/m/n/10 +
 []

\lgwproofline=\count146

Overfull \hbox (1.88902pt too wide) in paragraph at lines 14748--14765
[]$\OT1/cmr/m/n/10 [SystemQ[]x = x + (y \OMS/cmsy/m/n/10 ^^@ \OT1/cmr/m/n/10 y)
(R): ^^EFX\OML/cmm/m/it/10 ; \OT1/cmr/m/n/10 FY: R(FX) = R(FX) + +(R(FY) +|
 []

\lgwproofline=\count147
[20]
\lgwproofline=\count148

Underfull \hbox (badness 3396) in paragraph at lines 15069--15069
[]$\OT1/cmr/m/n/10 R(FX) + +R(FY) + +(\OMS/cmsy/m/n/10 ^^@ ^^@
 []


Underfull \hbox (badness 10000) in paragraph at lines 15069--15069
\OT1/cmr/m/n/10 R(FY)) == R(FX) +
 []


Underfull \hbox (badness 1635) in paragraph at lines 15102--15102
[]$\OT1/cmr/m/n/10 R(FX) + +(R(FY) + +(\OMS/cmsy/m/n/10 ^^@ ^^@
 []


Underfull \hbox (badness 10000) in paragraph at lines 15102--15102
\OT1/cmr/m/n/10 R(FY))) == R(FX) +
 []


Underfull \hbox (badness 10000) in paragraph at lines 15102--15102
\OT1/cmr/m/n/10 +R(FY) + +(\OMS/cmsy/m/n/10 ^^@ ^^@ \OT1/cmr/m/n/10 R(FY))$
 []


Overfull \hbox (15.72237pt too wide) in paragraph at lines 15194--15219
[]$\OT1/cmr/m/n/10 [SystemQ[]Three2twoTerms(R): ^^EFX\OML/cmm/m/it/10 ; \OT1/cm
r/m/n/10 FY\OML/cmm/m/it/10 ; \OT1/cmr/m/n/10 FZ\OML/cmm/m/it/10 ; \OT1/cmr/m/n
/10 FU: R(FY) + +R(FZ) ==|
 []

\lgwproofline=\count149

Underfull \hbox (badness 10000) in paragraph at lines 15283--15283
[]$\OT1/cmr/m/n/10 R(FX) + +(R(FY) +
 []


Overfull \hbox (21.88911pt too wide) in paragraph at lines 15396--15417
[]$\OT1/cmr/m/n/10 [SystemQ[]PositiveToRight(Less)(R): ^^EFX\OML/cmm/m/it/10 ; 
\OT1/cmr/m/n/10 FY\OML/cmm/m/it/10 ; \OT1/cmr/m/n/10 FZ: R(FX) + +R(FY) \OML/cm
m/m/it/10 <<|
 []

\lgwproofline=\count150

Underfull \hbox (badness 3396) in paragraph at lines 15481--15481
[]$\OT1/cmr/m/n/10 R(FX) + +R(FY) + +(\OMS/cmsy/m/n/10 ^^@ ^^@
 []


Underfull \hbox (badness 3396) in paragraph at lines 15529--15529
[]$\OT1/cmr/m/n/10 R(FX) + +R(FY) + +(\OMS/cmsy/m/n/10 ^^@ ^^@
 []

\lgwproofline=\count151

Underfull \hbox (badness 10000) in paragraph at lines 15763--15763
[]$\OT1/cmr/m/n/10 R(FX) + +(R(FZ) +
 []


Underfull \hbox (badness 10000) in paragraph at lines 15763--15763
\OT1/cmr/m/n/10 +R(FY)) == R(FX) +
 []

[21]
\lgwproofline=\count152

Overfull \hbox (15.38913pt too wide) in paragraph at lines 16008--16029
[]$\OT1/cmr/m/n/10 [SystemQ[]PositiveToRight(Eq)(R): ^^EFX\OML/cmm/m/it/10 ; \O
T1/cmr/m/n/10 FY\OML/cmm/m/it/10 ; \OT1/cmr/m/n/10 FZ: R(FX) + +R(FY) ==|
 []

\lgwproofline=\count153

Underfull \hbox (badness 3396) in paragraph at lines 16093--16093
[]$\OT1/cmr/m/n/10 R(FX) + +R(FY) + +(\OMS/cmsy/m/n/10 ^^@ ^^@
 []


Overfull \hbox (24.16693pt too wide) in paragraph at lines 16202--16227
[]$\OT1/cmr/m/n/10 [SystemQ[]SubtractEquations(R): ^^EFX\OML/cmm/m/it/10 ; \OT1
/cmr/m/n/10 FY\OML/cmm/m/it/10 ; \OT1/cmr/m/n/10 FZ\OML/cmm/m/it/10 ; \OT1/cmr/
m/n/10 FU: R(FX) + +R(FZ) ==|
 []

\lgwproofline=\count154

Underfull \hbox (badness 4242) in paragraph at lines 16308--16308
[]$\OT1/cmr/m/n/10 R(FX) + +R(FZ) + +(\OMS/cmsy/m/n/10 ^^@ ^^@
 []


Underfull \hbox (badness 1635) in paragraph at lines 16431--16431
[]$\OT1/cmr/m/n/10 R(FY) + +(R(FU) + +(\OMS/cmsy/m/n/10 ^^@ ^^@
 []


Underfull \hbox (badness 3396) in paragraph at lines 16458--16458
[]$\OT1/cmr/m/n/10 R(FY) + +R(FU) + +(\OMS/cmsy/m/n/10 ^^@ ^^@
 []


Underfull \hbox (badness 10000) in paragraph at lines 16458--16458
\OT1/cmr/m/n/10 R(FZ)) == R(FY) +
 []


Underfull \hbox (badness 6332) in paragraph at lines 16458--16458
\OT1/cmr/m/n/10 +(R(FU) + +(\OMS/cmsy/m/n/10 ^^@ ^^@ \OT1/cmr/m/n/10 R(FZ)))$
 []


Underfull \hbox (badness 3396) in paragraph at lines 16514--16514
[]$\OT1/cmr/m/n/10 R(FY) + +R(FU) + +(\OMS/cmsy/m/n/10 ^^@ ^^@
 []

[22]
Overfull \hbox (9.36113pt too wide) in paragraph at lines 16626--16646
[]$\OT1/cmr/m/n/10 [SystemQ[]NeqAddition(R): ^^EFX\OML/cmm/m/it/10 ; \OT1/cmr/m
/n/10 FY\OML/cmm/m/it/10 ; \OT1/cmr/m/n/10 FZ: R(FX) \OMS/cmsy/m/n/10 6\OT1/cmr
/m/n/10 = R(FY) \OMS/cmsy/m/n/10 ` \OT1/cmr/m/n/10 R(FX) +|
 []

\lgwproofline=\count155

Underfull \hbox (badness 10000) in paragraph at lines 16840--16840
[]$\OT1/cmr/m/n/10 R(FX) \OMS/cmsy/m/n/10 6\OT1/cmr/m/n/10 = R(FY) \OMS/cmsy/m/
n/10 )
 []


Overfull \hbox (34.02792pt too wide) in paragraph at lines 16975--16992
[]$\OT1/cmr/m/n/10 [SystemQ[]PositiveToRight(Less)(1term)(R): ^^EFX\OML/cmm/m/i
t/10 ; \OT1/cmr/m/n/10 FY: R(FX) \OML/cmm/m/it/10 << \OT1/cmr/m/n/10 R(FY) \OMS
/cmsy/m/n/10 `|
 []

\lgwproofline=\count156
[23]
Overfull \hbox (13.88527pt too wide) in paragraph at lines 17174--17192
[]$\OT1/cmr/m/n/10 [SystemQ[]To!! ==: ^^E\OMS/cmsy/m/n/10 M\OML/cmm/m/it/10 ; \
OMS/cmsy/m/n/10 N\OML/cmm/m/it/10 ; ^^O; \OT1/cmr/m/n/10 FX\OML/cmm/m/it/10 ; \
OT1/cmr/m/n/10 FY: [] (SF(FX\OML/cmm/m/it/10 ; \OT1/cmr/m/n/10 FY))n \OMS/cmsy/
m/n/10 ` \OT1/cmr/m/n/10 R(FX)!! ==|
 []

\lgwproofline=\count157

Underfull \hbox (badness 10000) in paragraph at lines 17306--17306
[]$\OT1/cmr/m/n/10 R(FX) == R(FY) \OMS/cmsy/m/n/10 )
 []

\lgwproofline=\count158

Overfull \hbox (15.18718pt too wide) in paragraph at lines 17599--17639
[]$\OT1/cmr/m/n/10 [SystemQ[]LessNeq(F)(Helper): ^^E\OMS/cmsy/m/n/10 M\OML/cmm/
m/it/10 ; \OMS/cmsy/m/n/10 N\OML/cmm/m/it/10 ; ^^O; \OT1/cmr/m/n/10 FX\OML/cmm/
m/it/10 ; \OT1/cmr/m/n/10 FY: \OMS/cmsy/m/n/10 8M\OT1/cmr/m/n/10 : 0 \OML/cmm/m
/it/10 < ^^O [] \OT1/cmr/m/n/10 (\OMS/cmsy/m/n/10 N \OML/cmm/m/it/10 <\OT1/cmr/
m/n/10 =|
 []

\lgwproofline=\count159

Underfull \hbox (badness 1342) in paragraph at lines 17727--17727
[]$\OT1/cmr/m/n/10 0 \OML/cmm/m/it/10 < ^^O [] \OT1/cmr/m/n/10 (\OMS/cmsy/m/n/1
0 N \OML/cmm/m/it/10 <\OT1/cmr/m/n/10 = \OMS/cmsy/m/n/10 N )
 []


Underfull \hbox (badness 1515) in paragraph at lines 17775--17775
[]$\OMS/cmsy/m/n/10 N \OML/cmm/m/it/10 <\OT1/cmr/m/n/10 = \OMS/cmsy/m/n/10 N ) 
\OT1/cmr/m/n/10 FX[\OMS/cmsy/m/n/10 N\OT1/cmr/m/n/10 ] \OML/cmm/m/it/10 <\OT1/c
mr/m/n/10 =
 []


Underfull \hbox (badness 10000) in paragraph at lines 17874--17874
[]$\OT1/cmr/m/n/10 (FY[\OMS/cmsy/m/n/10 N\OT1/cmr/m/n/10 ] \OMS/cmsy/m/n/10 ^^@
 \OT1/cmr/m/n/10 FX[\OMS/cmsy/m/n/10 N\OT1/cmr/m/n/10 ]) \OML/cmm/m/it/10 <\OT1
/cmr/m/n/10 =
 []

[24]
Overfull \hbox (23.6179pt too wide) in paragraph at lines 18167--18183
[]$\OT1/cmr/m/n/10 [SystemQ[]LessNeq(F): ^^E\OMS/cmsy/m/n/10 M\OML/cmm/m/it/10 
; \OMS/cmsy/m/n/10 N\OML/cmm/m/it/10 ; ^^O; \OT1/cmr/m/n/10 FX\OML/cmm/m/it/10 
; \OT1/cmr/m/n/10 FY: FX \OML/cmm/m/it/10 <[] \OT1/cmr/m/n/10 FY \OMS/cmsy/m/n/
10 ` [] \OT1/cmr/m/n/10 (SF(FX\OML/cmm/m/it/10 ; \OT1/cmr/m/n/10 FY))n]$ |
 []

\lgwproofline=\count160

Underfull \hbox (badness 1629) in paragraph at lines 18258--18258
\OT1/cmr/m/n/10 (\OT1/cmr/m/it/10 n \OML/cmm/m/it/10 <\OT1/cmr/m/n/10 = \OT1/cm
r/m/it/10 m \OMS/cmsy/m/n/10 ) \OT1/cmr/m/n/10 FX[\OT1/cmr/m/it/10 m\OT1/cmr/m/
n/10 ] \OML/cmm/m/it/10 <\OT1/cmr/m/n/10 =
 []


Underfull \hbox (badness 10000) in paragraph at lines 18573--18573
[]$[] \OT1/cmr/m/n/10 (\OMS/cmsy/m/n/10 8\OT1/cmr/m/n/10 (EPob): \OMS/cmsy/m/n/
10 9\OT1/cmr/m/it/10 n\OT1/cmr/m/n/10 : \OMS/cmsy/m/n/10 8\OT1/cmr/m/it/10 m\OT
1/cmr/m/n/10 : (0 \OML/cmm/m/it/10 <
 []


Underfull \hbox (badness 2671) in paragraph at lines 18573--18573
\OT1/cmr/m/n/10 (EPob) \OMS/cmsy/m/n/10 ) \OT1/cmr/m/it/10 n \OML/cmm/m/it/10 <
\OT1/cmr/m/n/10 = \OT1/cmr/m/it/10 m \OMS/cmsy/m/n/10 )
 []

[25]
\lgwproofline=\count161
\lgwproofline=\count162
\lgwproofline=\count163

Overfull \hbox (14.69684pt too wide) in paragraph at lines 19083--19083
[][]$\OT1/cmr/m/n/10 PositiveToRight(Less)(1term)(R) \U/lasy/m/n/10 ^^C |
 []


Underfull \hbox (badness 1635) in paragraph at lines 19117--19117
[]$\OT1/cmr/m/n/10 R(FX) + +(R(FY) + +(\OMS/cmsy/m/n/10 ^^@ ^^@
 []


Underfull \hbox (badness 6110) in paragraph at lines 19143--19143
[]$\OT1/cmr/m/n/10 R(FY) + +(\OMS/cmsy/m/n/10 ^^@ ^^@ \OT1/cmr/m/n/10 R(FX)) +
 []


Underfull \hbox (badness 3396) in paragraph at lines 19191--19191
[]$\OT1/cmr/m/n/10 R(FY) + +R(FX) + +(\OMS/cmsy/m/n/10 ^^@ ^^@
 []


Underfull \hbox (badness 1635) in paragraph at lines 19231--19231
[]$\OT1/cmr/m/n/10 R(FX) + +(R(FY) + +(\OMS/cmsy/m/n/10 ^^@ ^^@
 []


Underfull \hbox (badness 1635) in paragraph at lines 19271--19271
\OT1/cmr/m/n/10 R(FX) + +(R(FY) + +(\OMS/cmsy/m/n/10 ^^@ ^^@
 []


Underfull \hbox (badness 5667) in paragraph at lines 19304--19304
[]$\OMS/cmsy/m/n/10 9\OT1/cmr/m/n/10 FEP: 00 \OML/cmm/m/it/10 << \OT1/cmr/m/n/1
0 R(FEP) []
 []


Underfull \hbox (badness 10000) in paragraph at lines 19359--19359
[]$\OT1/cmr/m/n/10 R(FX) \OML/cmm/m/it/10 << \OT1/cmr/m/n/10 R(FY) \OMS/cmsy/m/
n/10 )
 []


Underfull \hbox (badness 5667) in paragraph at lines 19359--19359
\OMS/cmsy/m/n/10 9\OT1/cmr/m/n/10 FEP: 00 \OML/cmm/m/it/10 << \OT1/cmr/m/n/10 R
(FEP) []
 []


Underfull \hbox (badness 10000) in paragraph at lines 19436--19436
\OT1/cmr/m/n/10 R(FX) + +R(FEP) ==
 []


Underfull \hbox (badness 1337) in paragraph at lines 19466--19466
[]$[] \OT1/cmr/m/n/10 (\OMS/cmsy/m/n/10 9\OT1/cmr/m/n/10 FEP: 00 \OML/cmm/m/it/
10 << \OT1/cmr/m/n/10 R(FEP) []
 []


Underfull \hbox (badness 10000) in paragraph at lines 19466--19466
\OT1/cmr/m/n/10 R(FX) + +R(FEP) ==
 []

[26]
Overfull \hbox (27.41667pt too wide) in paragraph at lines 19574--19593
[]$\OT1/cmr/m/n/10 [SystemQ[]LeqNeqLess(R): ^^EFX\OML/cmm/m/it/10 ; \OT1/cmr/m/
n/10 FY: R(FX) \OML/cmm/m/it/10 <<\OT1/cmr/m/n/10 == R(FY) \OMS/cmsy/m/n/10 ` \
OT1/cmr/m/n/10 R(FX)!! ==|
 []

\lgwproofline=\count164

Underfull \hbox (badness 4765) in paragraph at lines 19771--19771
[]$\OT1/cmr/m/n/10 R(FX) \OML/cmm/m/it/10 <<\OT1/cmr/m/n/10 == R(FY) \OMS/cmsy/
m/n/10 )
 []


Underfull \hbox (badness 10000) in paragraph at lines 19771--19771
\OT1/cmr/m/n/10 R(FX)!! == R(FY) \OMS/cmsy/m/n/10 )
 []


Underfull \hbox (badness 4765) in paragraph at lines 19771--19771
\OT1/cmr/m/n/10 R(FY) \OML/cmm/m/it/10 <<\OT1/cmr/m/n/10 == R(FX) \OMS/cmsy/m/n
/10 )
 []


Underfull \hbox (badness 4765) in paragraph at lines 19834--19834
[]$\OT1/cmr/m/n/10 R(FY) \OML/cmm/m/it/10 <<\OT1/cmr/m/n/10 == R(FX) \OMS/cmsy/
m/n/10 )
 []


Overfull \hbox (37.69447pt too wide) in paragraph at lines 19934--19954
[]$\OT1/cmr/m/n/10 [SystemQ[]SubLeqLeft(R): ^^EFX\OML/cmm/m/it/10 ; \OT1/cmr/m/
n/10 FY\OML/cmm/m/it/10 ; \OT1/cmr/m/n/10 FZ: R(FX) == R(FY) \OMS/cmsy/m/n/10 `
 \OT1/cmr/m/n/10 R(FX) \OML/cmm/m/it/10 <<\OT1/cmr/m/n/10 ==|
 []

\lgwproofline=\count165
[27]
Overfull \hbox (22.88898pt too wide) in paragraph at lines 20125--20145
[]$\OT1/cmr/m/n/10 [SystemQ[]LeqLessTransitivity(R): ^^EFX\OML/cmm/m/it/10 ; \O
T1/cmr/m/n/10 FY\OML/cmm/m/it/10 ; \OT1/cmr/m/n/10 FZ: R(FX) \OML/cmm/m/it/10 <
<\OT1/cmr/m/n/10 == R(FY) \OMS/cmsy/m/n/10 `|
 []

\lgwproofline=\count166

Underfull \hbox (badness 4765) in paragraph at lines 20395--20395
[]$\OT1/cmr/m/n/10 R(FX) \OML/cmm/m/it/10 <<\OT1/cmr/m/n/10 == R(FY) \OMS/cmsy/
m/n/10 )
 []


Underfull \hbox (badness 10000) in paragraph at lines 20395--20395
\OT1/cmr/m/n/10 R(FY) \OML/cmm/m/it/10 << \OT1/cmr/m/n/10 R(FZ) \OMS/cmsy/m/n/1
0 )
 []


Underfull \hbox (badness 10000) in paragraph at lines 20395--20395
\OT1/cmr/m/n/10 R(FX) == R(FZ) \OMS/cmsy/m/n/10 )
 []


Underfull \hbox (badness 10000) in paragraph at lines 20457--20457
[]$\OT1/cmr/m/n/10 R(FX) == R(FZ) \OMS/cmsy/m/n/10 )
 []


Overfull \hbox (7.41682pt too wide) in paragraph at lines 20615--20636
[]$\OT1/cmr/m/n/10 [SystemQ[]NegativeToLeft(Eq)(R): ^^EFX\OML/cmm/m/it/10 ; \OT
1/cmr/m/n/10 FY\OML/cmm/m/it/10 ; \OT1/cmr/m/n/10 FZ: R(FX) == R(FY) +|
 []

\lgwproofline=\count167

Underfull \hbox (badness 7344) in paragraph at lines 20726--20726
[]$\OT1/cmr/m/n/10 R(FY) + +(\OMS/cmsy/m/n/10 ^^@ ^^@ \OT1/cmr/m/n/10 R(FZ)) +
 []


Underfull \hbox (badness 4242) in paragraph at lines 20774--20774
[]$\OT1/cmr/m/n/10 R(FY) + +R(FZ) + +(\OMS/cmsy/m/n/10 ^^@ ^^@
 []

[28]
\lgwproofline=\count168

Underfull \hbox (badness 6110) in paragraph at lines 20952--20952
[]$\OT1/cmr/m/n/10 R(FX) + +(\OMS/cmsy/m/n/10 ^^@ ^^@ \OT1/cmr/m/n/10 R(FY)) +
 []


Underfull \hbox (badness 6110) in paragraph at lines 20978--20978
[]$\OT1/cmr/m/n/10 R(FX) + +(\OMS/cmsy/m/n/10 ^^@ ^^@ \OT1/cmr/m/n/10 R(FY)) +
 []


Underfull \hbox (badness 10000) in paragraph at lines 20978--20978
\OT1/cmr/m/n/10 +R(FY) == R(FX) +
 []


Underfull \hbox (badness 10000) in paragraph at lines 20978--20978
\OT1/cmr/m/n/10 +R(FY) + +(\OMS/cmsy/m/n/10 ^^@ ^^@ \OT1/cmr/m/n/10 R(FY))$
 []


Underfull \hbox (badness 3396) in paragraph at lines 21026--21026
[]$\OT1/cmr/m/n/10 R(FX) + +R(FY) + +(\OMS/cmsy/m/n/10 ^^@ ^^@
 []


Underfull \hbox (badness 6110) in paragraph at lines 21059--21059
[]$\OT1/cmr/m/n/10 R(FX) + +(\OMS/cmsy/m/n/10 ^^@ ^^@ \OT1/cmr/m/n/10 R(FY)) +
 []


Overfull \hbox (22.1944pt too wide) in paragraph at lines 21144--21159
[]$\OT1/cmr/m/n/10 [SystemQ[]!! == Symmetry: ^^EFX\OML/cmm/m/it/10 ; \OT1/cmr/m
/n/10 FY: R(FX)!! == R(FY) \OMS/cmsy/m/n/10 ` \OT1/cmr/m/n/10 R(FY)!! ==|
 []

\lgwproofline=\count169

Underfull \hbox (badness 10000) in paragraph at lines 21269--21269
[]$\OT1/cmr/m/n/10 R(FY) == R(FX) \OMS/cmsy/m/n/10 )
 []

\lgwproofline=\count170

Underfull \hbox (badness 6110) in paragraph at lines 21452--21452
[]$\OT1/cmr/m/n/10 R(FX) + +(\OMS/cmsy/m/n/10 ^^@ ^^@ \OT1/cmr/m/n/10 R(FY)) +
 []


Underfull \hbox (badness 3396) in paragraph at lines 21499--21499
[]$\OT1/cmr/m/n/10 R(FX) + +R(FY) + +(\OMS/cmsy/m/n/10 ^^@ ^^@
 []

[29]
Overfull \hbox (7.05592pt too wide) in paragraph at lines 21590--21607
[]$\OT1/cmr/m/n/10 [SystemQ[]NegativeToRight(Eq)(1term)(R): ^^EFX\OML/cmm/m/it/
10 ; \OT1/cmr/m/n/10 FY: R(FX) + +(\OMS/cmsy/m/n/10 ^^@ ^^@|
 []

\lgwproofline=\count171
\lgwproofline=\count172

Underfull \hbox (badness 5771) in paragraph at lines 21838--21838
\OT1/cmr/m/n/10 R(FX))) == (\OMS/cmsy/m/n/10 ^^@ ^^@ \OT1/cmr/m/n/10 (\OMS/cmsy
/m/n/10 ^^@ ^^@
 []


Overfull \hbox (11.89131pt too wide) in paragraph at lines 21918--21918
[][]$\OT1/cmr/m/n/10 NegativeToRight(Eq)(1term)(R) \U/lasy/m/n/10 ^^C |
 []

\lgwproofline=\count173
[30]
Overfull \hbox (41.80586pt too wide) in paragraph at lines 22309--22334
[]$\OT1/cmr/m/n/10 [SystemQ[]SubtractEquationsLeft(R): ^^EFX\OML/cmm/m/it/10 ; 
\OT1/cmr/m/n/10 FY\OML/cmm/m/it/10 ; \OT1/cmr/m/n/10 FZ\OML/cmm/m/it/10 ; \OT1/
cmr/m/n/10 FU: R(FX) + +R(FZ) ==|
 []

\lgwproofline=\count174

Overfull \hbox (25.77783pt too wide) in paragraph at lines 22544--22561
[]$\OT1/cmr/m/n/10 [SystemQ[]EqNegated(R): ^^EFX\OML/cmm/m/it/10 ; \OT1/cmr/m/n
/10 FY: R(FX) == R(FY) \OMS/cmsy/m/n/10 ` \OT1/cmr/m/n/10 (\OMS/cmsy/m/n/10 ^^@
 ^^@ \OT1/cmr/m/n/10 R(FX)) ==|
 []

\lgwproofline=\count175
\lgwproofline=\count176

Underfull \hbox (badness 2512) in paragraph at lines 23051--23051
[] \OT1/cmr/m/n/10 ((\OMS/cmsy/m/n/10 ^^@ ^^@ \OT1/cmr/m/n/10 R(FX)) == (\OMS/c
msy/m/n/10 ^^@ ^^@
 []


Underfull \hbox (badness 7963) in paragraph at lines 23100--23100
[]$\OT1/cmr/m/n/10 (\OMS/cmsy/m/n/10 ^^@ ^^@ \OT1/cmr/m/n/10 R(FX)) == (\OMS/cm
sy/m/n/10 ^^@ ^^@
 []


Underfull \hbox (badness 2512) in paragraph at lines 23125--23125
[]$[] \OT1/cmr/m/n/10 ((\OMS/cmsy/m/n/10 ^^@ ^^@ \OT1/cmr/m/n/10 R(FX)) == (\OM
S/cmsy/m/n/10 ^^@ ^^@
 []

[31]
Overfull \hbox (42.97224pt too wide) in paragraph at lines 23185--23205
[]$\OT1/cmr/m/n/10 [SystemQ[]SubLeqRight(R): ^^EFX\OML/cmm/m/it/10 ; \OT1/cmr/m
/n/10 FY\OML/cmm/m/it/10 ; \OT1/cmr/m/n/10 FZ: R(FX) == R(FY) \OMS/cmsy/m/n/10 
` \OT1/cmr/m/n/10 R(FZ) \OML/cmm/m/it/10 <<\OT1/cmr/m/n/10 ==|
 []

\lgwproofline=\count177
\lgwproofline=\count178

Underfull \hbox (badness 1221) in paragraph at lines 23479--23479
[]$\OT1/cmr/m/n/10 00 \OML/cmm/m/it/10 <<\OT1/cmr/m/n/10 == R(FY) + +(\OMS/cmsy
/m/n/10 ^^@ ^^@
 []


Underfull \hbox (badness 2057) in paragraph at lines 23531--23531
[]$\OT1/cmr/m/n/10 00 \OML/cmm/m/it/10 <<\OT1/cmr/m/n/10 == (\OMS/cmsy/m/n/10 ^
^@ ^^@ \OT1/cmr/m/n/10 R(FX)) +
 []


Underfull \hbox (badness 1337) in paragraph at lines 23561--23561
[]$\OT1/cmr/m/n/10 00 + +(\OMS/cmsy/m/n/10 ^^@ ^^@ \OT1/cmr/m/n/10 R(FY)) \OML/
cmm/m/it/10 <<\OT1/cmr/m/n/10 ==
 []


Underfull \hbox (badness 1668) in paragraph at lines 23667--23667
[]$\OT1/cmr/m/n/10 (\OMS/cmsy/m/n/10 ^^@ ^^@ \OT1/cmr/m/n/10 R(FY)) \OML/cmm/m/
it/10 <<\OT1/cmr/m/n/10 == (\OMS/cmsy/m/n/10 ^^@ ^^@
 []


Underfull \hbox (badness 1635) in paragraph at lines 23667--23667
\OT1/cmr/m/n/10 R(FX)) + +R(FY) + +(\OMS/cmsy/m/n/10 ^^@ ^^@
 []


Underfull \hbox (badness 1668) in paragraph at lines 23696--23696
[]$\OT1/cmr/m/n/10 (\OMS/cmsy/m/n/10 ^^@ ^^@ \OT1/cmr/m/n/10 R(FY)) \OML/cmm/m/
it/10 <<\OT1/cmr/m/n/10 == (\OMS/cmsy/m/n/10 ^^@ ^^@
 []

[32]
Overfull \hbox (32.27782pt too wide) in paragraph at lines 23754--23771
[]$\OT1/cmr/m/n/10 [SystemQ[]LessNegated(R): ^^EFX\OML/cmm/m/it/10 ; \OT1/cmr/m
/n/10 FY: R(FX) \OML/cmm/m/it/10 << \OT1/cmr/m/n/10 R(FY) \OMS/cmsy/m/n/10 ` \O
T1/cmr/m/n/10 (\OMS/cmsy/m/n/10 ^^@ ^^@ \OT1/cmr/m/n/10 R(FY)) \OML/cmm/m/it/10
 <<|
 []

\lgwproofline=\count179

Underfull \hbox (badness 1668) in paragraph at lines 23849--23849
[]$\OT1/cmr/m/n/10 (\OMS/cmsy/m/n/10 ^^@ ^^@ \OT1/cmr/m/n/10 R(FY)) \OML/cmm/m/
it/10 <<\OT1/cmr/m/n/10 == (\OMS/cmsy/m/n/10 ^^@ ^^@
 []

\lgwproofline=\count180
\lgwproofline=\count181

Overfull \hbox (36.88899pt too wide) in paragraph at lines 24296--24311
[]$\OT1/cmr/m/n/10 [SystemQ[]LeqTotality(R): ^^EFX\OML/cmm/m/it/10 ; \OT1/cmr/m
/n/10 FY: R(FX) \OML/cmm/m/it/10 <<\OT1/cmr/m/n/10 == R(FY) [] R(FY) \OML/cmm/m
/it/10 <<\OT1/cmr/m/n/10 ==|
 []

\lgwproofline=\count182

Underfull \hbox (badness 6510) in paragraph at lines 24470--24470
[]$\OT1/cmr/m/n/10 R(FX) \OML/cmm/m/it/10 <<\OT1/cmr/m/n/10 == R(FY) []
 []

[33]
\lgwproofline=\count183

Underfull \hbox (badness 6510) in paragraph at lines 24610--24610
[]$\OT1/cmr/m/n/10 R(FX) \OML/cmm/m/it/10 <<\OT1/cmr/m/n/10 == R(FY) []
 []


Overfull \hbox (23.83333pt too wide) in paragraph at lines 24697--24713
[]$\OT1/cmr/m/n/10 [SystemQ[]FromLess(R): ^^EFX\OML/cmm/m/it/10 ; \OT1/cmr/m/n/
10 FY: R(FX) \OML/cmm/m/it/10 << \OT1/cmr/m/n/10 R(FY) \OMS/cmsy/m/n/10 ` [] \O
T1/cmr/m/n/10 (R(FY) \OML/cmm/m/it/10 <<\OT1/cmr/m/n/10 ==|
 []

\lgwproofline=\count184

Underfull \hbox (badness 10000) in paragraph at lines 24919--24919
[]$\OT1/cmr/m/n/10 R(FX) \OML/cmm/m/it/10 << \OT1/cmr/m/n/10 R(FY) \OMS/cmsy/m/
n/10 )
 []


Underfull \hbox (badness 4765) in paragraph at lines 24919--24919
\OT1/cmr/m/n/10 R(FY) \OML/cmm/m/it/10 <<\OT1/cmr/m/n/10 == R(FX) \OMS/cmsy/m/n
/10 )
 []


Underfull \hbox (badness 4765) in paragraph at lines 24964--24964
[]$\OT1/cmr/m/n/10 R(FY) \OML/cmm/m/it/10 <<\OT1/cmr/m/n/10 == R(FX) \OMS/cmsy/
m/n/10 )
 []

\lgwproofline=\count185
[34]
\lgwproofline=\count186

Overfull \hbox (33.05566pt too wide) in paragraph at lines 25611--25625
[]$\OT1/cmr/m/n/10 [SystemQ[]NonnegativeNumerical(R): ^^EFX: 00 \OML/cmm/m/it/1
0 <<\OT1/cmr/m/n/10 == R(FX) \OMS/cmsy/m/n/10 ` j\OT1/cmr/m/n/10 rR(FX)\OMS/cms
y/m/n/10 j \OT1/cmr/m/n/10 =|
 []

\lgwproofline=\count187
\lgwproofline=\count188

Underfull \hbox (badness 1983) in paragraph at lines 26097--26097
[]$\OT1/cmr/m/n/10 SF(FX\OML/cmm/m/it/10 ; \OT1/cmr/m/n/10 FY) \OMS/cmsy/m/n/10
 ) \OT1/cmr/m/n/10 R(FX) \OML/cmm/m/it/10 <<
 []

[35]
\lgwproofline=\count189

Overfull \hbox (9.1667pt too wide) in paragraph at lines 26385--26400
[]$\OT1/cmr/m/n/10 [SystemQ[]NegativeNumerical(R): ^^EFX: R(FX) \OML/cmm/m/it/1
0 << \OT1/cmr/m/n/10 00 \OMS/cmsy/m/n/10 ` j\OT1/cmr/m/n/10 rR(FX)\OMS/cmsy/m/n
/10 j \OT1/cmr/m/n/10 ==|
 []

\lgwproofline=\count190
[36]
\lgwproofline=\count191

Underfull \hbox (badness 3668) in paragraph at lines 27122--27122
[]$[] \OT1/cmr/m/n/10 (00 \OML/cmm/m/it/10 <<\OT1/cmr/m/n/10 == R(FX))n \OMS/cm
sy/m/n/10 )
 []


Overfull \hbox (10.41672pt too wide) in paragraph at lines 27206--27219
[]$\OT1/cmr/m/n/10 [SystemQ[]PositiveNegated(R): ^^EFX: 00 \OML/cmm/m/it/10 << 
\OT1/cmr/m/n/10 R(FX) \OMS/cmsy/m/n/10 ` \OT1/cmr/m/n/10 (\OMS/cmsy/m/n/10 ^^@ 
^^@ \OT1/cmr/m/n/10 R(FX)) \OML/cmm/m/it/10 <<|
 []

\lgwproofline=\count192

Overfull \hbox (2.47227pt too wide) in paragraph at lines 27369--27394
[]$\OT1/cmr/m/n/10 [SystemQ[]AddEquations(R): ^^EFX\OML/cmm/m/it/10 ; \OT1/cmr/
m/n/10 FY\OML/cmm/m/it/10 ; \OT1/cmr/m/n/10 FZ\OML/cmm/m/it/10 ; \OT1/cmr/m/n/1
0 FU: R(FX) == R(FY) \OMS/cmsy/m/n/10 `|
 []

\lgwproofline=\count193
[37]
Overfull \hbox (21.80594pt too wide) in paragraph at lines 27578--27601
[]$\OT1/cmr/m/n/10 [SystemQ[]DistributionOut(R): ^^EFX\OML/cmm/m/it/10 ; \OT1/c
mr/m/n/10 FY\OML/cmm/m/it/10 ; \OT1/cmr/m/n/10 FZ: R(FX) \OMS/cmsy/m/n/10 ^^C ^
^C\OT1/cmr/m/n/10 R(FY) + +R(FX) \OMS/cmsy/m/n/10 ^^C|
 []

\lgwproofline=\count194
\lgwproofline=\count195

Underfull \hbox (badness 1275) in paragraph at lines 27840--27840
[]$\OT1/cmr/m/n/10 R(FX) \OMS/cmsy/m/n/10 ^^C ^^C\OT1/cmr/m/n/10 00 + +R(FX) ==

 []


Underfull \hbox (badness 1275) in paragraph at lines 27983--27983
[]$\OT1/cmr/m/n/10 R(FX) \OMS/cmsy/m/n/10 ^^C ^^C\OT1/cmr/m/n/10 00 + +R(FX) ==

 []

\lgwproofline=\count196

Underfull \hbox (badness 1173) in paragraph at lines 28124--28124
\OT1/cmr/m/n/10 R(FX)) == R(FX) \OMS/cmsy/m/n/10 ^^C ^^C\OT1/cmr/m/n/10 00 +
 []


Underfull \hbox (badness 1275) in paragraph at lines 28178--28178
[]$\OT1/cmr/m/n/10 R(FX) \OMS/cmsy/m/n/10 ^^C ^^C\OT1/cmr/m/n/10 00 + +R(FX) ==

 []

[38]
\lgwproofline=\count197
\lgwproofline=\count198
 [39]
\lgwproofline=\count199

Underfull \hbox (badness 10000) in paragraph at lines 29087--29087
[]$\OT1/cmr/m/n/10 (\OMS/cmsy/m/n/10 ^^@ ^^@ \OT1/cmr/m/n/10 R(FX)) + +(\OMS/cm
sy/m/n/10 ^^@ ^^@
 []


Underfull \hbox (badness 10000) in paragraph at lines 29135--29135
[]$\OT1/cmr/m/n/10 (\OMS/cmsy/m/n/10 ^^@ ^^@ \OT1/cmr/m/n/10 01) \OMS/cmsy/m/n/
10 ^^C ^^C\OT1/cmr/m/n/10 (R(FX) +
 []


Underfull \hbox (badness 10000) in paragraph at lines 29176--29176
[]$\OT1/cmr/m/n/10 (\OMS/cmsy/m/n/10 ^^@ ^^@ \OT1/cmr/m/n/10 R(FX)) + +(\OMS/cm
sy/m/n/10 ^^@ ^^@
 []


Overfull \hbox (8.38889pt too wide) in paragraph at lines 29232--29251
[]$\OT1/cmr/m/n/10 [SystemQ[]LessTotality(R): ^^EFX\OML/cmm/m/it/10 ; \OT1/cmr/
m/n/10 FY: R(FX) \OML/cmm/m/it/10 << \OT1/cmr/m/n/10 R(FY) [] R(FX) ==|
 []

\lgwproofline=\count200

Underfull \hbox (badness 2418) in paragraph at lines 29429--29429
[]$[] \OT1/cmr/m/n/10 (R(FX) \OML/cmm/m/it/10 << \OT1/cmr/m/n/10 R(FY))n \OMS/c
msy/m/n/10 )
 []


Underfull \hbox (badness 10000) in paragraph at lines 29429--29429
\OT1/cmr/m/n/10 R(FX)!! == R(FY) \OMS/cmsy/m/n/10 )
 []


Underfull \hbox (badness 10000) in paragraph at lines 29458--29458
[]$\OT1/cmr/m/n/10 R(FX) \OML/cmm/m/it/10 << \OT1/cmr/m/n/10 R(FY) []
 []


Underfull \hbox (badness 10000) in paragraph at lines 29458--29458
\OT1/cmr/m/n/10 R(FX) == R(FY) []
 []


Overfull \hbox (32.08339pt too wide) in paragraph at lines 29514--29531
[]$\OT1/cmr/m/n/10 [SystemQ[]SameNumerical(R): ^^EFX\OML/cmm/m/it/10 ; \OT1/cmr
/m/n/10 FY: R(FX) == R(FY) \OMS/cmsy/m/n/10 ` j\OT1/cmr/m/n/10 rR(FX)\OMS/cmsy/
m/n/10 j \OT1/cmr/m/n/10 ==|
 []

[40]
\lgwproofline=\count201

Underfull \hbox (badness 10000) in paragraph at lines 30014--30014
[]$\OT1/cmr/m/n/10 00 \OML/cmm/m/it/10 <<\OT1/cmr/m/n/10 == R(FX) \OMS/cmsy/m/n
/10 )
 []


Underfull \hbox (badness 10000) in paragraph at lines 30014--30014
\OT1/cmr/m/n/10 R(FX) == R(FY) \OMS/cmsy/m/n/10 )
 []


Underfull \hbox (badness 3668) in paragraph at lines 30046--30046
[]$[] \OT1/cmr/m/n/10 (00 \OML/cmm/m/it/10 <<\OT1/cmr/m/n/10 == R(FX))n \OMS/cm
sy/m/n/10 )
 []


Underfull \hbox (badness 10000) in paragraph at lines 30046--30046
\OT1/cmr/m/n/10 R(FX) == R(FY) \OMS/cmsy/m/n/10 )
 []


Underfull \hbox (badness 10000) in paragraph at lines 30080--30080
[]$\OT1/cmr/m/n/10 R(FX) == R(FY) \OMS/cmsy/m/n/10 )
 []


Overfull \hbox (25.13927pt too wide) in paragraph at lines 30165--30184
[]$\OT1/cmr/m/n/10 [SystemQ[]MinusNegated(R): ^^EFX\OML/cmm/m/it/10 ; \OT1/cmr/
m/n/10 FY: (\OMS/cmsy/m/n/10 ^^@ ^^@ \OT1/cmr/m/n/10 (R(FX) + +(\OMS/cmsy/m/n/1
0 ^^@ ^^@ \OT1/cmr/m/n/10 R(FY)))) ==|
 []

\lgwproofline=\count202

Underfull \hbox (badness 10000) in paragraph at lines 30361--30361
[]$\OT1/cmr/m/n/10 (\OMS/cmsy/m/n/10 ^^@ ^^@ \OT1/cmr/m/n/10 ((\OMS/cmsy/m/n/10
 ^^@ ^^@ \OT1/cmr/m/n/10 R(FY)) +
 []


Underfull \hbox (badness 10000) in paragraph at lines 30432--30432
[]$\OT1/cmr/m/n/10 (\OMS/cmsy/m/n/10 ^^@ ^^@ \OT1/cmr/m/n/10 (R(FX) + +(\OMS/cm
sy/m/n/10 ^^@ ^^@
 []

[41]
Overfull \hbox (5.47224pt too wide) in paragraph at lines 30490--30504
[]$\OT1/cmr/m/n/10 [SystemQ[]PositiveNumerical(R): ^^EFX: 00 \OML/cmm/m/it/10 <
< \OT1/cmr/m/n/10 R(FX) \OMS/cmsy/m/n/10 ` j\OT1/cmr/m/n/10 rR(FX)\OMS/cmsy/m/n
/10 j \OT1/cmr/m/n/10 ==|
 []

\lgwproofline=\count203

Overfull \hbox (5.55562pt too wide) in paragraph at lines 30632--30648
[]$\OT1/cmr/m/n/10 [SystemQ[]SignNumerical(+)(R): ^^EFX: 00 \OML/cmm/m/it/10 <<
 \OT1/cmr/m/n/10 R(FX) \OMS/cmsy/m/n/10 ` j\OT1/cmr/m/n/10 rR(FX)\OMS/cmsy/m/n/
10 j \OT1/cmr/m/n/10 ==|
 []

\lgwproofline=\count204
\lgwproofline=\count205

Underfull \hbox (badness 4378) in paragraph at lines 31054--31054
[]$\OMS/cmsy/m/n/10 j\OT1/cmr/m/n/10 r(\OMS/cmsy/m/n/10 ^^@ ^^@ \OT1/cmr/m/n/10
 (\OMS/cmsy/m/n/10 ^^@ ^^@ \OT1/cmr/m/n/10 R(FX)))\OMS/cmsy/m/n/10 j \OT1/cmr/m
/n/10 ==
 []

[42]
Overfull \hbox (29.19478pt too wide) in paragraph at lines 31580--31599
[]$\OT1/cmr/m/n/10 [SystemQ[]NumericalDi^^Kerence(R): ^^EFX\OML/cmm/m/it/10 ; \
OT1/cmr/m/n/10 FY: \OMS/cmsy/m/n/10 j\OT1/cmr/m/n/10 rR(FX) + +(\OMS/cmsy/m/n/1
0 ^^@ ^^@ \OT1/cmr/m/n/10 R(FY))\OMS/cmsy/m/n/10 j \OT1/cmr/m/n/10 ==|
 []

\lgwproofline=\count206

Underfull \hbox (badness 10000) in paragraph at lines 31668--31668
[]$\OT1/cmr/m/n/10 (\OMS/cmsy/m/n/10 ^^@ ^^@ \OT1/cmr/m/n/10 (R(FX) + +(\OMS/cm
sy/m/n/10 ^^@ ^^@
 []


Underfull \hbox (badness 10000) in paragraph at lines 31700--31700
[]$\OMS/cmsy/m/n/10 j\OT1/cmr/m/n/10 r(\OMS/cmsy/m/n/10 ^^@ ^^@ \OT1/cmr/m/n/10
 (R(FX) + +(\OMS/cmsy/m/n/10 ^^@ ^^@
 []


Underfull \hbox (badness 6944) in paragraph at lines 31700--31700
\OT1/cmr/m/n/10 R(FY))))\OMS/cmsy/m/n/10 j \OT1/cmr/m/n/10 == \OMS/cmsy/m/n/10 
j\OT1/cmr/m/n/10 rR(FY) +
 []

[43]
\lgwproofline=\count207

Underfull \hbox (badness 10000) in paragraph at lines 32039--32039
[]$\OT1/cmr/m/n/10 00 \OML/cmm/m/it/10 <<\OT1/cmr/m/n/10 == R(FX) \OMS/cmsy/m/n
/10 )
 []


Underfull \hbox (badness 10000) in paragraph at lines 32039--32039
\OT1/cmr/m/n/10 R(FX) \OML/cmm/m/it/10 <<\OT1/cmr/m/n/10 == \OMS/cmsy/m/n/10 j\
OT1/cmr/m/n/10 rR(FX)\OMS/cmsy/m/n/10 j$
 []


Underfull \hbox (badness 10000) in paragraph at lines 32065--32065
[]$\OT1/cmr/m/n/10 R(FX) \OML/cmm/m/it/10 <<\OT1/cmr/m/n/10 == 00 \OMS/cmsy/m/n
/10 )
 []


Underfull \hbox (badness 10000) in paragraph at lines 32065--32065
\OT1/cmr/m/n/10 R(FX) \OML/cmm/m/it/10 <<\OT1/cmr/m/n/10 == \OMS/cmsy/m/n/10 j\
OT1/cmr/m/n/10 rR(FX)\OMS/cmsy/m/n/10 j$
 []


LaTeX Warning: Command \O invalid in math mode on input line 34693.


LaTeX Warning: Command \O invalid in math mode on input line 34711.


LaTeX Warning: Command \O invalid in math mode on input line 34821.


LaTeX Warning: Command \O invalid in math mode on input line 34823.


LaTeX Warning: Command \O invalid in math mode on input line 34825.


LaTeX Warning: Command \O invalid in math mode on input line 34827.


LaTeX Warning: Command \O invalid in math mode on input line 34829.


LaTeX Warning: Command \O invalid in math mode on input line 34869.


LaTeX Warning: Command \O invalid in math mode on input line 34871.

[44] [45] [46] [47] [48] [49] [50] [51] [52] [53] [54] [55] [56] [57] [58]
[59] [60] [61] [62] [63] [64]
Overfull \hbox (18.54926pt too wide) in paragraph at lines 41211--41218
[]$\OT1/cmr/m/n/10 [NonreciprocalToRight(Eq)(1term)(R) [] []NonreciprocalToRigh
t(Eq)(1  []term)(R)[]]$ |
 []

[65]
Overfull \hbox (2.3269pt too wide) in paragraph at lines 41293--41300
[]$\OT1/cmr/m/n/10 [ReciprocalToRight(Less)(1term)(R) [] []ReciprocalToRight(Le
ss)(1  []term)(R)[]]$ |
 []

[66]
Overfull \hbox (1.77153pt too wide) in paragraph at lines 41421--41427
[]$\OT1/cmr/m/n/10 [USlimitIsLeastUpperBound(Helper) [] []USlimitIsLeastUpperBo
und(Helper)[]]$ |
 []

[67] (./page.aux) ) 
Here is how much of TeX's memory you used:
 2718 strings out of 95835
 36117 string characters out of 1195527
 205290 words of memory out of 1000001
 5617 multiletter control sequences out of 10000+50000
 7607 words of font info for 29 fonts, out of 500000 for 1000
 28 hyphenation exceptions out of 1000
 25i,9n,36p,203b,245s stack positions out of 1500i,500n,5000p,200000b,5000s

Output written on page.dvi (67 pages, 246712 bytes).