\special{!/magscale false def}
% ALL_11.TEX
%==============================================================================

%==============================================================================
% PARAM.1
\magnification=\magstep1
\pageno=0
%==============================================================================



%==============================================================================
% FONTS.2
\font\huge=cmbx10 scaled\magstep2
\font\xbold=cmbx10 scaled\magstep1
\font\cbold=cmsy10 scaled\magstep1
\font\mbold=cmmi10 scaled\magstep1
\font\sub=cmbx10
\font\small=cmr7
\font\plg=cmtt10
\font\plgt=cmtt10 at 10truept
%==============================================================================



%==============================================================================
% TITLES.3
\count5=0
\count6=1
\count7=1
\count8=1
\def\proof{\medskip\noindent{\bf Proof.\ }}
\def\qed{\hfill\smallskip
         \line{\hfill\vrule height 1.8ex width 2ex depth +.2ex
               \ \ \ \ \ \ }\bigskip}
\def\remark{\medskip\noindent{\bf Remark.}}
\def\abstract#1\par{\noindent{\sub Abstract.} #1 \par}
\def\equ(#1){\csname e#1\endcsname}
\def\clm(#1){\csname c#1\endcsname}
\def\equation(#1){\eqno\tag(#1)}
\def\tag(#1){(\number\count5.
              \number\count6)
    \expandafter\xdef\csname e#1\endcsname{(\number\count5.\number\count6)}
    \global\advance\count6 by 1}
\def\claim #1(#2) #3\par{
    \vskip.1in\medbreak\noindent
    {\bf #1\ \number\count5.\number\count7.\ }{\sl #3}\par
    \expandafter\xdef\csname c#2\endcsname{#1~\number\count5.\number\count7}
    \global\advance\count7 by 1
    \ifdim\lastskip<\medskipamount
    \removelastskip\penalty55\medskip\fi}
\def\section#1\par{\vskip0pt plus.3\vsize\penalty-75
    \vskip0pt plus -.3\vsize\bigskip\bigskip
    \global\advance\count5 by 1
    \message{#1}\leftline
     {\xbold \number\count5.\ #1}
    \count6=1
    \count7=1
    \count8=1
    \nobreak\smallskip\noindent}
\def\subsection#1\par{\vskip0pt plus.2\vsize\penalty-75
    \vskip0pt plus -.2\vsize\bigskip\bigskip
    \message{#1}\leftline{\sub
    \number\count5.\number\count8.\ #1}
    \global\advance\count8 by 1
    \nobreak\smallskip\noindent}
%==============================================================================



%==============================================================================
% MACROS.15

\footline{\ifnum\pageno=0\hss\else\hss\tenrm\folio\hss\fi}
\let\cl=\centerline
\def\mean{{\rm I\kern-.18em E}}
\def\natural{{\rm I\kern-.18em N}}
\def\integer{{\rm Z\kern-.32em Z}}
\def\real{{\rm I\kern-.2em R}}
\def\complex{\kern.1em{\raise.47ex\hbox{
            $\scriptscriptstyle |$}}\kern-.40em{\rm C}}
\def\I{|\hskip-0.08em |\hskip-0.08em |}
\def\Id{{\rm I}}
\def\Int{\int\limits_{-\infty}^\infty\!}
\def\HT{_{\scriptscriptstyle HT}}
\def\UV{_{\scriptscriptstyle UV}}
\def\IR{_{\scriptscriptstyle IR}}
\def\AA{{\cal A}}
\def\BB{{\cal B}}
\def\CC{{\cal C}}
\def\DD{{\cal D}}
\def\EE{{\cal E}}
\def\FF{{\cal F}}
\def\GG{{\cal G}}
\def\HH{{\cal H}}
\def\II{{\cal I}}
\def\JJ{{\cal J}}
\def\KK{{\cal K}}
\def\LL{{\cal L}}
\def\MM{{\cal M}}
\def\NN{{\cal N}}
\def\OO{{\cal O}}
\def\PP{{\cal P}}
\def\QQ{{\cal Q}}
\def\RR{{\cal R}}
\def\SS{{\cal S}}
\def\TT{{\cal T}}
\def\UU{{\cal U}}
\def\VV{{\cal V}}
\def\WW{{\cal W}}
\def\XX{{\cal X}}
\def\YY{{\cal Y}}
\def\ZZ{{\cal Z}}
\def\std{{\rm std}}

\def\...{{$\cdot\cdot\cdot$}}

\def\pro{
    \bgroup
    \smallskip
    \noindent
    \plg
    \catcode`_=11
    \catcode`~=11
    \catcode`@=11
    \catcode`&=11
    \obeylines
    \obeyspaces
}
\def\log{
 \smallskip
 \write3{  }
 \write3{  }
 \noindent
 \egroup
}

\def\logc{
 \smallskip
 \noindent
 \egroup
}

\def\p${\bgroup\plg\catcode`_=11\catcode`~=11}
\def\l${\egroup}

\def\prolog#1{
 \write3{#1}
 {\ }#1
}

\def\t #1{{\hbox{\plg#1}}}
%==============================================================================



%==============================================================================
% PSDUMP.TEX
% TeX macros for dumping included Postscript to files.
% Adapted from Knuth's \answer macro in the TeXbook.
% Requires Plain TeX.  Maybe other flavors will work too?
% Jamie Stephens, jamies@math.utexas.edu, 28 Nov 94

\def\endofps{EndOfTheIncludedPostscriptMagicCookie}
\chardef\other=12
\newwrite\psdumphandle
\outer\def\psdump#1{\par\medbreak
  \immediate\openout\psdumphandle=#1
  \copytoblankline}
\def\copytoblankline{\begingroup\setupcopy\copypsline}
\def\setupcopy{\def\do##1{\catcode`##1=\other}\dospecials
  \catcode`\\=\other \obeylines}
{\obeylines \gdef\copypsline#1
  {\def\next{#1}%
  \ifx\next\endofps\let\next=\endgroup %
  \else\immediate\write\psdumphandle{\next} \let\next=\copypsline\fi\next}}
\outer\def\closepsdump{
  \immediate\closeout\psdumphandle}

% EXAMPLE (remove the leading % signs to make it work):
%
%\psdump{example.ps}These three lines
%are going be dumped "as is"
%to the file example.ps
%EndOfTheIncludedPostscriptMagicCookie
%\closepsdump
%==============================================================================



%==============================================================================
% PHI_FG.PS
\psdump{phi_fg.ps}%!
/jpedict 250 dict def jpedict begin
/Cou /Times-Roman findfont 50.000000 scalefont def
/Sym /Symbol      findfont 50.000000 scalefont def
/lw{0.700000 setlinewidth}def
/ll{3.000000 setlinewidth}def
newpath
-0.240000 0.240000 scale
90 rotate
1 setlinecap
/r{moveto 0 1 rlineto stroke}def
/m{moveto}def
/l{lineto}def
/s{stroke}def
0 0 m
lw
1.000000 1.000000 scale
295 -59 m
295 649 l
s
-59 295 m
649 295 l
s
295 1181 m
295 1535 l
s
-59 1181 m
720 1181 l
s
ll
153 -59 m
155 -58 l
157 -57 l
159 -56 l
160 -56 l
162 -55 l
164 -54 l
166 -54 l
167 -53 l
169 -52 l
171 -51 l
173 -51 l
174 -50 l
176 -49 l
178 -49 l
180 -48 l
181 -47 l
183 -47 l
185 -46 l
187 -45 l
188 -44 l
190 -44 l
192 -43 l
194 -42 l
195 -42 l
197 -41 l
199 -40 l
200 -39 l
202 -39 l
204 -38 l
206 -37 l
207 -37 l
209 -36 l
211 -35 l
212 -34 l
214 -34 l
216 -33 l
218 -32 l
219 -32 l
221 -31 l
223 -30 l
224 -29 l
226 -29 l
228 -28 l
229 -27 l
231 -27 l
233 -26 l
235 -25 l
236 -25 l
238 -24 l
240 -23 l
241 -22 l
243 -22 l
245 -21 l
246 -20 l
248 -20 l
250 -19 l
251 -18 l
253 -17 l
255 -17 l
256 -16 l
258 -15 l
259 -15 l
261 -14 l
263 -13 l
264 -12 l
266 -12 l
268 -11 l
269 -10 l
271 -10 l
273 -9 l
274 -8 l
276 -8 l
277 -7 l
279 -6 l
281 -5 l
282 -5 l
284 -4 l
285 -3 l
287 -3 l
289 -2 l
290 -1 l
292 0 l
293 0 l
295 0 l
297 1 l
298 1 l
300 2 l
301 3 l
303 4 l
305 4 l
306 5 l
308 6 l
309 6 l
311 7 l
312 8 l
314 8 l
316 9 l
317 10 l
319 11 l
320 11 l
322 12 l
323 13 l
325 13 l
326 14 l
328 15 l
329 16 l
331 16 l
332 17 l
334 18 l
335 18 l
337 19 l
339 20 l
340 21 l
342 21 l
343 22 l
345 23 l
346 23 l
348 24 l
349 25 l
351 25 l
352 26 l
354 27 l
355 28 l
356 28 l
358 29 l
359 30 l
361 30 l
362 31 l
364 32 l
365 33 l
367 33 l
368 34 l
370 35 l
371 35 l
373 36 l
374 37 l
375 38 l
377 38 l
378 39 l
380 40 l
381 40 l
383 41 l
384 42 l
385 42 l
387 43 l
388 44 l
390 45 l
391 45 l
392 46 l
394 47 l
395 47 l
397 48 l
398 49 l
399 50 l
401 50 l
402 51 l
404 52 l
405 52 l
406 53 l
408 54 l
409 55 l
410 55 l
412 56 l
413 57 l
414 57 l
416 58 l
417 59 l
418 59 l
420 60 l
421 61 l
422 62 l
424 62 l
425 63 l
426 64 l
428 64 l
429 65 l
430 66 l
432 67 l
433 67 l
434 68 l
436 69 l
437 69 l
438 70 l
439 71 l
441 72 l
442 72 l
443 73 l
445 74 l
446 74 l
447 75 l
448 76 l
450 77 l
451 77 l
452 78 l
453 79 l
455 79 l
456 80 l
457 81 l
458 81 l
459 82 l
461 83 l
462 84 l
463 84 l
464 85 l
466 86 l
467 86 l
468 87 l
469 88 l
470 89 l
472 89 l
473 90 l
474 91 l
475 91 l
476 92 l
477 93 l
479 94 l
480 94 l
481 95 l
482 96 l
483 96 l
484 97 l
486 98 l
487 98 l
488 99 l
489 100 l
490 101 l
491 101 l
492 102 l
494 103 l
495 103 l
496 104 l
497 105 l
498 106 l
499 106 l
500 107 l
501 108 l
502 108 l
503 109 l
505 110 l
506 111 l
507 111 l
508 112 l
509 113 l
510 113 l
511 114 l
512 115 l
513 115 l
514 116 l
515 117 l
516 118 l
517 118 l
518 119 l
519 120 l
520 120 l
521 121 l
522 122 l
s
522 122 m
523 123 l
524 123 l
525 124 l
526 125 l
527 125 l
528 126 l
529 127 l
530 128 l
531 128 l
532 129 l
533 130 l
534 130 l
535 131 l
536 132 l
537 132 l
538 133 l
539 134 l
540 135 l
541 135 l
542 136 l
543 137 l
544 137 l
545 138 l
546 139 l
547 140 l
548 140 l
549 141 l
549 142 l
550 142 l
551 143 l
552 144 l
553 145 l
554 145 l
555 146 l
556 147 l
557 147 l
557 148 l
558 149 l
559 149 l
560 150 l
561 151 l
562 152 l
563 152 l
563 153 l
564 154 l
565 154 l
566 155 l
567 156 l
568 157 l
568 157 l
569 158 l
570 159 l
571 159 l
572 160 l
573 161 l
573 162 l
574 162 l
575 163 l
576 164 l
577 164 l
577 165 l
578 166 l
579 167 l
580 167 l
580 168 l
581 169 l
582 169 l
583 170 l
583 171 l
584 171 l
585 172 l
586 173 l
586 174 l
587 174 l
588 175 l
588 176 l
589 176 l
590 177 l
591 178 l
591 179 l
592 179 l
593 180 l
593 181 l
594 181 l
595 182 l
595 183 l
596 184 l
597 184 l
597 185 l
598 186 l
599 186 l
599 187 l
600 188 l
601 188 l
601 189 l
602 190 l
603 191 l
603 191 l
604 192 l
604 193 l
605 193 l
606 194 l
606 195 l
607 196 l
607 196 l
608 197 l
609 198 l
609 198 l
610 199 l
610 200 l
611 201 l
612 201 l
612 202 l
613 203 l
613 203 l
614 204 l
614 205 l
615 205 l
615 206 l
616 207 l
616 208 l
617 208 l
618 209 l
618 210 l
619 210 l
619 211 l
620 212 l
620 213 l
621 213 l
621 214 l
622 215 l
622 215 l
623 216 l
623 217 l
623 218 l
624 218 l
624 219 l
625 220 l
625 220 l
626 221 l
626 222 l
627 222 l
627 223 l
628 224 l
628 225 l
628 225 l
629 226 l
629 227 l
630 227 l
630 228 l
630 229 l
631 230 l
631 230 l
632 231 l
632 232 l
632 232 l
633 233 l
633 234 l
633 235 l
634 235 l
634 236 l
635 237 l
635 237 l
635 238 l
636 239 l
636 239 l
636 240 l
637 241 l
637 242 l
637 242 l
638 243 l
638 244 l
638 244 l
639 245 l
639 246 l
639 247 l
639 247 l
640 248 l
640 249 l
640 249 l
641 250 l
641 251 l
641 252 l
641 252 l
642 253 l
642 254 l
642 254 l
642 255 l
643 256 l
643 257 l
643 257 l
643 258 l
643 259 l
644 259 l
644 260 l
644 261 l
644 261 l
645 262 l
645 263 l
645 264 l
645 264 l
645 265 l
645 266 l
646 266 l
646 267 l
646 268 l
646 269 l
646 269 l
646 270 l
647 271 l
647 271 l
647 272 l
647 273 l
647 274 l
647 274 l
647 275 l
648 276 l
648 276 l
648 277 l
648 278 l
648 278 l
648 279 l
648 280 l
648 281 l
648 281 l
648 282 l
648 283 l
649 283 l
649 284 l
649 285 l
649 286 l
649 286 l
649 287 l
649 288 l
649 288 l
649 289 l
649 290 l
649 291 l
649 291 l
649 292 l
649 293 l
649 293 l
649 294 l
649 295 l
649 295 l
649 296 l
649 297 l
649 298 l
649 298 l
649 299 l
649 300 l
649 300 l
649 301 l
649 302 l
649 303 l
649 303 l
s
649 303 m
649 304 l
649 305 l
649 305 l
649 306 l
648 307 l
648 308 l
648 308 l
648 309 l
648 310 l
648 310 l
648 311 l
648 312 l
648 312 l
648 313 l
648 314 l
647 315 l
647 315 l
647 316 l
647 317 l
647 317 l
647 318 l
647 319 l
646 320 l
646 320 l
646 321 l
646 322 l
646 322 l
646 323 l
645 324 l
645 325 l
645 325 l
645 326 l
645 327 l
645 327 l
644 328 l
644 329 l
644 329 l
644 330 l
643 331 l
643 332 l
643 332 l
643 333 l
643 334 l
642 334 l
642 335 l
642 336 l
642 337 l
641 337 l
641 338 l
641 339 l
641 339 l
640 340 l
640 341 l
640 342 l
639 342 l
639 343 l
639 344 l
639 344 l
638 345 l
638 346 l
638 347 l
637 347 l
637 348 l
637 349 l
636 349 l
636 350 l
636 351 l
635 351 l
635 352 l
635 353 l
634 354 l
634 354 l
633 355 l
633 356 l
633 356 l
632 357 l
632 358 l
632 359 l
631 359 l
631 360 l
630 361 l
630 361 l
630 362 l
629 363 l
629 364 l
628 364 l
628 365 l
628 366 l
627 366 l
627 367 l
626 368 l
626 368 l
625 369 l
625 370 l
624 371 l
624 371 l
623 372 l
623 373 l
623 373 l
622 374 l
622 375 l
621 376 l
621 376 l
620 377 l
620 378 l
619 378 l
619 379 l
618 380 l
618 381 l
617 381 l
616 382 l
616 383 l
615 383 l
615 384 l
614 385 l
614 385 l
613 386 l
613 387 l
612 388 l
612 388 l
611 389 l
610 390 l
610 390 l
609 391 l
609 392 l
608 393 l
607 393 l
607 394 l
606 395 l
606 395 l
605 396 l
604 397 l
604 398 l
603 398 l
603 399 l
602 400 l
601 400 l
601 401 l
600 402 l
599 402 l
599 403 l
598 404 l
597 405 l
597 405 l
596 406 l
595 407 l
595 407 l
594 408 l
593 409 l
593 410 l
592 410 l
591 411 l
591 412 l
590 412 l
589 413 l
588 414 l
588 415 l
587 415 l
586 416 l
586 417 l
585 417 l
584 418 l
583 419 l
583 419 l
582 420 l
581 421 l
580 422 l
580 422 l
579 423 l
578 424 l
577 424 l
577 425 l
576 426 l
575 427 l
574 427 l
573 428 l
573 429 l
572 429 l
571 430 l
570 431 l
569 432 l
568 432 l
568 433 l
567 434 l
566 434 l
565 435 l
564 436 l
563 437 l
563 437 l
562 438 l
561 439 l
560 439 l
559 440 l
558 441 l
557 441 l
557 442 l
556 443 l
555 444 l
554 444 l
553 445 l
552 446 l
551 446 l
550 447 l
549 448 l
549 449 l
548 449 l
547 450 l
546 451 l
545 451 l
544 452 l
543 453 l
542 454 l
541 454 l
540 455 l
539 456 l
538 456 l
537 457 l
536 458 l
535 458 l
534 459 l
533 460 l
532 461 l
531 461 l
530 462 l
529 463 l
528 463 l
527 464 l
526 465 l
525 466 l
524 466 l
523 467 l
522 468 l
521 468 l
520 469 l
519 470 l
518 471 l
517 471 l
516 472 l
515 473 l
514 473 l
513 474 l
512 475 l
511 475 l
510 476 l
509 477 l
508 478 l
507 478 l
506 479 l
505 480 l
503 480 l
502 481 l
501 482 l
500 483 l
499 483 l
498 484 l
497 485 l
s
497 485 m
496 485 l
495 486 l
494 487 l
492 488 l
491 488 l
490 489 l
489 490 l
488 490 l
487 491 l
486 492 l
484 492 l
483 493 l
482 494 l
481 495 l
480 495 l
479 496 l
477 497 l
476 497 l
475 498 l
474 499 l
473 500 l
472 500 l
470 501 l
469 502 l
468 502 l
467 503 l
466 504 l
464 505 l
463 505 l
462 506 l
461 507 l
459 507 l
458 508 l
457 509 l
456 509 l
455 510 l
453 511 l
452 512 l
451 512 l
450 513 l
448 514 l
447 514 l
446 515 l
445 516 l
443 517 l
442 517 l
441 518 l
439 519 l
438 519 l
437 520 l
436 521 l
434 522 l
433 522 l
432 523 l
430 524 l
429 524 l
428 525 l
426 526 l
425 527 l
424 527 l
422 528 l
421 529 l
420 529 l
418 530 l
417 531 l
416 531 l
414 532 l
413 533 l
412 534 l
410 534 l
409 535 l
408 536 l
406 536 l
405 537 l
404 538 l
402 539 l
401 539 l
399 540 l
398 541 l
397 541 l
395 542 l
394 543 l
392 544 l
391 544 l
390 545 l
388 546 l
387 546 l
385 547 l
384 548 l
383 548 l
381 549 l
380 550 l
378 551 l
377 551 l
375 552 l
374 553 l
373 553 l
371 554 l
370 555 l
368 556 l
367 556 l
365 557 l
364 558 l
362 558 l
361 559 l
359 560 l
358 561 l
356 561 l
355 562 l
354 563 l
352 563 l
351 564 l
349 565 l
348 565 l
346 566 l
345 567 l
343 568 l
342 568 l
340 569 l
339 570 l
337 570 l
335 571 l
334 572 l
332 573 l
331 573 l
329 574 l
328 575 l
326 575 l
325 576 l
323 577 l
322 578 l
320 578 l
319 579 l
317 580 l
316 580 l
314 581 l
312 582 l
311 582 l
309 583 l
308 584 l
306 585 l
305 585 l
303 586 l
301 587 l
300 587 l
298 588 l
297 589 l
295 590 l
293 590 l
292 591 l
290 592 l
289 592 l
287 593 l
285 594 l
284 595 l
282 595 l
281 596 l
279 597 l
277 597 l
276 598 l
274 599 l
273 599 l
271 600 l
269 601 l
268 602 l
266 602 l
264 603 l
263 604 l
261 604 l
259 605 l
258 606 l
256 607 l
255 607 l
253 608 l
251 609 l
250 609 l
248 610 l
246 611 l
245 612 l
243 612 l
241 613 l
240 614 l
238 614 l
236 615 l
235 616 l
233 617 l
231 617 l
229 618 l
228 619 l
226 619 l
224 620 l
223 621 l
221 621 l
219 622 l
218 623 l
216 624 l
214 624 l
212 625 l
211 626 l
209 626 l
207 627 l
206 628 l
204 629 l
202 629 l
200 630 l
199 631 l
197 631 l
195 632 l
194 633 l
192 634 l
190 634 l
188 635 l
187 636 l
185 636 l
183 637 l
181 638 l
180 638 l
178 639 l
176 640 l
174 641 l
173 641 l
171 642 l
169 643 l
167 643 l
166 644 l
164 645 l
162 646 l
160 646 l
159 647 l
157 648 l
155 648 l
153 649 l
s
lw
649 -59 m
649 649 l
s
-59 649 m
649 649 l
s
-59 649 m
-59 -59 l
s
-59 -59 m
649 -59 l
s
ll
649 1181 m
649 1181 l
648 1181 l
648 1182 l
647 1182 l
647 1182 l
646 1183 l
646 1183 l
645 1183 l
645 1184 l
645 1184 l
644 1184 l
644 1185 l
643 1185 l
643 1186 l
642 1186 l
642 1186 l
641 1187 l
641 1187 l
641 1187 l
640 1188 l
640 1188 l
639 1188 l
639 1189 l
638 1189 l
638 1189 l
637 1190 l
637 1190 l
636 1191 l
636 1191 l
636 1191 l
635 1192 l
635 1192 l
634 1192 l
634 1193 l
633 1193 l
633 1193 l
632 1194 l
632 1194 l
632 1194 l
631 1195 l
631 1195 l
630 1195 l
630 1196 l
629 1196 l
629 1197 l
628 1197 l
628 1197 l
628 1198 l
627 1198 l
627 1198 l
626 1199 l
626 1199 l
625 1199 l
625 1200 l
624 1200 l
624 1200 l
623 1201 l
623 1201 l
623 1202 l
622 1202 l
622 1202 l
621 1203 l
621 1203 l
620 1203 l
620 1204 l
619 1204 l
619 1204 l
619 1205 l
618 1205 l
618 1205 l
617 1206 l
617 1206 l
616 1206 l
616 1207 l
615 1207 l
615 1208 l
615 1208 l
614 1208 l
614 1209 l
613 1209 l
613 1209 l
612 1210 l
612 1210 l
611 1210 l
611 1211 l
611 1211 l
610 1211 l
610 1212 l
609 1212 l
609 1212 l
608 1213 l
608 1213 l
607 1214 l
607 1214 l
606 1214 l
606 1215 l
606 1215 l
605 1215 l
605 1216 l
604 1216 l
604 1216 l
603 1217 l
603 1217 l
602 1217 l
602 1218 l
602 1218 l
601 1219 l
601 1219 l
600 1219 l
600 1220 l
599 1220 l
599 1220 l
598 1221 l
598 1221 l
598 1221 l
597 1222 l
597 1222 l
596 1222 l
596 1223 l
595 1223 l
595 1223 l
594 1224 l
594 1224 l
594 1225 l
593 1225 l
593 1225 l
592 1226 l
592 1226 l
591 1226 l
591 1227 l
590 1227 l
590 1227 l
590 1228 l
589 1228 l
589 1228 l
588 1229 l
588 1229 l
587 1229 l
587 1230 l
586 1230 l
586 1231 l
586 1231 l
585 1231 l
585 1232 l
584 1232 l
584 1232 l
583 1233 l
583 1233 l
582 1233 l
582 1234 l
582 1234 l
581 1234 l
581 1235 l
580 1235 l
580 1236 l
579 1236 l
579 1236 l
579 1237 l
578 1237 l
578 1237 l
577 1238 l
577 1238 l
576 1238 l
576 1239 l
575 1239 l
575 1239 l
575 1240 l
574 1240 l
574 1240 l
573 1241 l
573 1241 l
572 1242 l
572 1242 l
571 1242 l
571 1243 l
571 1243 l
570 1243 l
570 1244 l
569 1244 l
569 1244 l
568 1245 l
568 1245 l
567 1245 l
567 1246 l
567 1246 l
566 1247 l
566 1247 l
565 1247 l
565 1248 l
564 1248 l
564 1248 l
563 1249 l
563 1249 l
563 1249 l
562 1250 l
562 1250 l
561 1250 l
561 1251 l
560 1251 l
560 1251 l
560 1252 l
559 1252 l
559 1253 l
558 1253 l
558 1253 l
557 1254 l
557 1254 l
556 1254 l
556 1255 l
556 1255 l
555 1255 l
555 1256 l
554 1256 l
554 1256 l
553 1257 l
553 1257 l
552 1257 l
552 1258 l
552 1258 l
551 1259 l
551 1259 l
550 1259 l
550 1260 l
549 1260 l
549 1260 l
549 1261 l
548 1261 l
548 1261 l
547 1262 l
547 1262 l
546 1262 l
546 1263 l
545 1263 l
545 1264 l
545 1264 l
544 1264 l
544 1265 l
543 1265 l
543 1265 l
542 1266 l
542 1266 l
542 1266 l
541 1267 l
541 1267 l
540 1267 l
540 1268 l
539 1268 l
539 1268 l
538 1269 l
538 1269 l
538 1270 l
537 1270 l
537 1270 l
536 1271 l
536 1271 l
535 1271 l
s
535 1271 m
535 1272 l
535 1272 l
534 1272 l
534 1273 l
533 1273 l
533 1273 l
532 1274 l
532 1274 l
531 1274 l
531 1275 l
531 1275 l
530 1276 l
530 1276 l
529 1276 l
529 1277 l
528 1277 l
528 1277 l
528 1278 l
527 1278 l
527 1278 l
526 1279 l
526 1279 l
525 1279 l
525 1280 l
525 1280 l
524 1281 l
524 1281 l
523 1281 l
523 1282 l
522 1282 l
522 1282 l
521 1283 l
521 1283 l
521 1283 l
520 1284 l
520 1284 l
519 1284 l
519 1285 l
518 1285 l
518 1285 l
518 1286 l
517 1286 l
517 1287 l
516 1287 l
516 1287 l
515 1288 l
515 1288 l
515 1288 l
514 1289 l
514 1289 l
513 1289 l
513 1290 l
512 1290 l
512 1290 l
511 1291 l
511 1291 l
511 1292 l
510 1292 l
510 1292 l
509 1293 l
509 1293 l
508 1293 l
508 1294 l
508 1294 l
507 1294 l
507 1295 l
506 1295 l
506 1295 l
505 1296 l
505 1296 l
505 1296 l
504 1297 l
504 1297 l
503 1298 l
503 1298 l
502 1298 l
502 1299 l
502 1299 l
501 1299 l
501 1300 l
500 1300 l
500 1300 l
499 1301 l
499 1301 l
498 1301 l
498 1302 l
498 1302 l
497 1302 l
497 1303 l
496 1303 l
496 1304 l
495 1304 l
495 1304 l
495 1305 l
494 1305 l
494 1305 l
493 1306 l
493 1306 l
492 1306 l
492 1307 l
492 1307 l
491 1307 l
491 1308 l
490 1308 l
490 1309 l
489 1309 l
489 1309 l
489 1310 l
488 1310 l
488 1310 l
487 1311 l
487 1311 l
486 1311 l
486 1312 l
486 1312 l
485 1312 l
485 1313 l
484 1313 l
484 1313 l
483 1314 l
483 1314 l
483 1315 l
482 1315 l
482 1315 l
481 1316 l
481 1316 l
480 1316 l
480 1317 l
480 1317 l
479 1317 l
479 1318 l
478 1318 l
478 1318 l
477 1319 l
477 1319 l
477 1319 l
476 1320 l
476 1320 l
475 1321 l
475 1321 l
474 1321 l
474 1322 l
474 1322 l
473 1322 l
473 1323 l
472 1323 l
472 1323 l
471 1324 l
471 1324 l
471 1324 l
470 1325 l
470 1325 l
469 1326 l
469 1326 l
468 1326 l
468 1327 l
468 1327 l
467 1327 l
467 1328 l
466 1328 l
466 1328 l
465 1329 l
465 1329 l
465 1329 l
464 1330 l
464 1330 l
463 1330 l
463 1331 l
462 1331 l
462 1332 l
462 1332 l
461 1332 l
461 1333 l
460 1333 l
460 1333 l
459 1334 l
459 1334 l
459 1334 l
458 1335 l
458 1335 l
457 1335 l
457 1336 l
456 1336 l
456 1337 l
456 1337 l
455 1337 l
455 1338 l
454 1338 l
454 1338 l
454 1339 l
453 1339 l
453 1339 l
452 1340 l
452 1340 l
451 1340 l
451 1341 l
451 1341 l
450 1341 l
450 1342 l
449 1342 l
449 1343 l
448 1343 l
448 1343 l
448 1344 l
447 1344 l
447 1344 l
446 1345 l
446 1345 l
445 1345 l
445 1346 l
445 1346 l
444 1346 l
444 1347 l
443 1347 l
443 1347 l
442 1348 l
442 1348 l
442 1349 l
441 1349 l
441 1349 l
440 1350 l
440 1350 l
440 1350 l
439 1351 l
439 1351 l
438 1351 l
438 1352 l
437 1352 l
437 1352 l
437 1353 l
436 1353 l
436 1354 l
435 1354 l
435 1354 l
434 1355 l
434 1355 l
434 1355 l
433 1356 l
433 1356 l
432 1356 l
432 1357 l
432 1357 l
431 1357 l
431 1358 l
430 1358 l
430 1358 l
429 1359 l
429 1359 l
429 1360 l
428 1360 l
428 1360 l
427 1361 l
427 1361 l
426 1361 l
426 1362 l
426 1362 l
s
426 1362 m
425 1362 l
425 1363 l
424 1363 l
424 1363 l
424 1364 l
423 1364 l
423 1364 l
422 1365 l
422 1365 l
421 1366 l
421 1366 l
421 1366 l
420 1367 l
420 1367 l
419 1367 l
419 1368 l
418 1368 l
418 1368 l
418 1369 l
417 1369 l
417 1369 l
416 1370 l
416 1370 l
416 1371 l
415 1371 l
415 1371 l
414 1372 l
414 1372 l
413 1372 l
413 1373 l
413 1373 l
412 1373 l
412 1374 l
411 1374 l
411 1374 l
411 1375 l
410 1375 l
410 1375 l
409 1376 l
409 1376 l
408 1377 l
408 1377 l
408 1377 l
407 1378 l
407 1378 l
406 1378 l
406 1379 l
405 1379 l
405 1379 l
405 1380 l
404 1380 l
404 1380 l
403 1381 l
403 1381 l
403 1382 l
402 1382 l
402 1382 l
401 1383 l
401 1383 l
400 1383 l
400 1384 l
400 1384 l
399 1384 l
399 1385 l
398 1385 l
398 1385 l
398 1386 l
397 1386 l
397 1386 l
396 1387 l
396 1387 l
395 1388 l
395 1388 l
395 1388 l
394 1389 l
394 1389 l
393 1389 l
393 1390 l
393 1390 l
392 1390 l
392 1391 l
391 1391 l
391 1391 l
391 1392 l
390 1392 l
390 1392 l
389 1393 l
389 1393 l
388 1394 l
388 1394 l
388 1394 l
387 1395 l
387 1395 l
386 1395 l
386 1396 l
386 1396 l
385 1396 l
385 1397 l
384 1397 l
384 1397 l
383 1398 l
383 1398 l
383 1399 l
382 1399 l
382 1399 l
381 1400 l
381 1400 l
381 1400 l
380 1401 l
380 1401 l
379 1401 l
379 1402 l
379 1402 l
378 1402 l
378 1403 l
377 1403 l
377 1403 l
376 1404 l
376 1404 l
376 1405 l
375 1405 l
375 1405 l
374 1406 l
374 1406 l
374 1406 l
373 1407 l
373 1407 l
372 1407 l
372 1408 l
371 1408 l
371 1408 l
371 1409 l
370 1409 l
370 1409 l
369 1410 l
369 1410 l
369 1411 l
368 1411 l
368 1411 l
367 1412 l
367 1412 l
367 1412 l
366 1413 l
366 1413 l
365 1413 l
365 1414 l
365 1414 l
364 1414 l
364 1415 l
363 1415 l
363 1416 l
362 1416 l
362 1416 l
362 1417 l
361 1417 l
361 1417 l
360 1418 l
360 1418 l
360 1418 l
359 1419 l
359 1419 l
358 1419 l
358 1420 l
358 1420 l
357 1420 l
357 1421 l
356 1421 l
356 1422 l
355 1422 l
355 1422 l
355 1423 l
354 1423 l
354 1423 l
353 1424 l
353 1424 l
353 1424 l
352 1425 l
352 1425 l
351 1425 l
351 1426 l
351 1426 l
350 1427 l
350 1427 l
349 1427 l
349 1428 l
349 1428 l
348 1428 l
348 1429 l
347 1429 l
347 1429 l
347 1430 l
346 1430 l
346 1430 l
345 1431 l
345 1431 l
344 1431 l
344 1432 l
344 1432 l
343 1433 l
343 1433 l
342 1433 l
342 1434 l
342 1434 l
341 1434 l
341 1435 l
340 1435 l
340 1435 l
340 1436 l
339 1436 l
339 1436 l
338 1437 l
338 1437 l
338 1437 l
337 1438 l
337 1438 l
336 1439 l
336 1439 l
336 1439 l
335 1440 l
335 1440 l
334 1440 l
334 1441 l
334 1441 l
333 1441 l
333 1442 l
332 1442 l
332 1442 l
331 1443 l
331 1443 l
331 1444 l
330 1444 l
330 1444 l
329 1445 l
329 1445 l
329 1445 l
328 1446 l
328 1446 l
327 1446 l
327 1447 l
327 1447 l
326 1447 l
326 1448 l
325 1448 l
325 1448 l
325 1449 l
324 1449 l
324 1450 l
323 1450 l
323 1450 l
323 1451 l
322 1451 l
322 1451 l
321 1452 l
321 1452 l
321 1452 l
320 1453 l
s
320 1453 m
320 1453 l
319 1453 l
319 1454 l
319 1454 l
318 1454 l
318 1455 l
317 1455 l
317 1456 l
317 1456 l
316 1456 l
316 1457 l
315 1457 l
315 1457 l
315 1458 l
314 1458 l
314 1458 l
313 1459 l
313 1459 l
313 1459 l
312 1460 l
312 1460 l
311 1461 l
311 1461 l
311 1461 l
310 1462 l
310 1462 l
309 1462 l
309 1463 l
309 1463 l
308 1463 l
308 1464 l
307 1464 l
307 1464 l
307 1465 l
306 1465 l
306 1465 l
305 1466 l
305 1466 l
305 1467 l
304 1467 l
304 1467 l
303 1468 l
303 1468 l
303 1468 l
302 1469 l
302 1469 l
301 1469 l
301 1470 l
301 1470 l
300 1470 l
300 1471 l
299 1471 l
299 1472 l
299 1472 l
298 1472 l
298 1473 l
297 1473 l
297 1473 l
297 1474 l
296 1474 l
296 1474 l
295 1475 l
295 1475 l
295 1475 l
294 1476 l
294 1476 l
293 1476 l
293 1477 l
293 1477 l
292 1478 l
292 1478 l
291 1478 l
291 1479 l
291 1479 l
290 1479 l
290 1480 l
289 1480 l
289 1480 l
289 1481 l
288 1481 l
288 1481 l
287 1482 l
287 1482 l
287 1482 l
286 1483 l
286 1483 l
285 1484 l
285 1484 l
285 1484 l
284 1485 l
284 1485 l
283 1485 l
283 1486 l
283 1486 l
282 1486 l
282 1487 l
281 1487 l
281 1487 l
281 1488 l
280 1488 l
280 1489 l
279 1489 l
279 1489 l
279 1490 l
278 1490 l
278 1490 l
277 1491 l
277 1491 l
277 1491 l
276 1492 l
276 1492 l
276 1492 l
275 1493 l
275 1493 l
274 1493 l
274 1494 l
274 1494 l
273 1495 l
273 1495 l
272 1495 l
272 1496 l
272 1496 l
271 1496 l
271 1497 l
270 1497 l
270 1497 l
270 1498 l
269 1498 l
269 1498 l
268 1499 l
268 1499 l
268 1499 l
267 1500 l
267 1500 l
266 1501 l
266 1501 l
266 1501 l
265 1502 l
265 1502 l
264 1502 l
264 1503 l
264 1503 l
263 1503 l
263 1504 l
263 1504 l
262 1504 l
262 1505 l
261 1505 l
261 1506 l
261 1506 l
260 1506 l
260 1507 l
259 1507 l
259 1507 l
259 1508 l
258 1508 l
258 1508 l
257 1509 l
257 1509 l
257 1509 l
256 1510 l
256 1510 l
255 1510 l
255 1511 l
255 1511 l
254 1512 l
254 1512 l
254 1512 l
253 1513 l
253 1513 l
252 1513 l
252 1514 l
252 1514 l
251 1514 l
251 1515 l
250 1515 l
250 1515 l
250 1516 l
249 1516 l
249 1517 l
248 1517 l
248 1517 l
248 1518 l
247 1518 l
247 1518 l
247 1519 l
246 1519 l
246 1519 l
245 1520 l
245 1520 l
245 1520 l
244 1521 l
244 1521 l
243 1521 l
243 1522 l
243 1522 l
242 1523 l
242 1523 l
241 1523 l
241 1524 l
241 1524 l
240 1524 l
240 1525 l
240 1525 l
239 1525 l
239 1526 l
238 1526 l
238 1526 l
238 1527 l
237 1527 l
237 1527 l
236 1528 l
236 1528 l
236 1529 l
235 1529 l
235 1529 l
235 1530 l
234 1530 l
234 1530 l
233 1531 l
233 1531 l
233 1531 l
232 1532 l
232 1532 l
231 1532 l
231 1533 l
231 1533 l
230 1534 l
230 1534 l
229 1534 l
229 1535 l
229 1535 l
s
720 1181 m
720 1181 l
720 1181 l
719 1182 l
719 1182 l
719 1182 l
719 1183 l
719 1183 l
719 1183 l
718 1184 l
718 1184 l
718 1184 l
718 1185 l
718 1185 l
718 1186 l
717 1186 l
717 1186 l
717 1187 l
717 1187 l
717 1187 l
717 1188 l
716 1188 l
716 1188 l
716 1189 l
716 1189 l
716 1189 l
715 1190 l
715 1190 l
715 1191 l
715 1191 l
715 1191 l
715 1192 l
714 1192 l
714 1192 l
714 1193 l
714 1193 l
714 1193 l
714 1194 l
713 1194 l
713 1194 l
713 1195 l
713 1195 l
713 1195 l
713 1196 l
712 1196 l
712 1197 l
712 1197 l
712 1197 l
712 1198 l
712 1198 l
711 1198 l
711 1199 l
711 1199 l
711 1199 l
711 1200 l
711 1200 l
710 1200 l
710 1201 l
710 1201 l
710 1202 l
710 1202 l
710 1202 l
709 1203 l
709 1203 l
709 1203 l
709 1204 l
709 1204 l
708 1204 l
708 1205 l
708 1205 l
708 1205 l
708 1206 l
708 1206 l
707 1206 l
707 1207 l
707 1207 l
707 1208 l
707 1208 l
707 1208 l
706 1209 l
706 1209 l
706 1209 l
706 1210 l
706 1210 l
706 1210 l
705 1211 l
705 1211 l
705 1211 l
705 1212 l
705 1212 l
705 1212 l
704 1213 l
704 1213 l
704 1214 l
704 1214 l
704 1214 l
704 1215 l
703 1215 l
703 1215 l
703 1216 l
703 1216 l
703 1216 l
703 1217 l
702 1217 l
702 1217 l
702 1218 l
702 1218 l
702 1219 l
702 1219 l
701 1219 l
701 1220 l
701 1220 l
701 1220 l
701 1221 l
701 1221 l
700 1221 l
700 1222 l
700 1222 l
700 1222 l
700 1223 l
700 1223 l
699 1223 l
699 1224 l
699 1224 l
699 1225 l
699 1225 l
699 1225 l
698 1226 l
698 1226 l
698 1226 l
698 1227 l
698 1227 l
697 1227 l
697 1228 l
697 1228 l
697 1228 l
697 1229 l
697 1229 l
696 1229 l
696 1230 l
696 1230 l
696 1231 l
696 1231 l
696 1231 l
695 1232 l
695 1232 l
695 1232 l
695 1233 l
695 1233 l
695 1233 l
694 1234 l
694 1234 l
694 1234 l
694 1235 l
694 1235 l
694 1236 l
693 1236 l
693 1236 l
693 1237 l
693 1237 l
693 1237 l
693 1238 l
692 1238 l
692 1238 l
692 1239 l
692 1239 l
692 1239 l
692 1240 l
691 1240 l
691 1240 l
691 1241 l
691 1241 l
691 1242 l
691 1242 l
690 1242 l
690 1243 l
690 1243 l
690 1243 l
690 1244 l
690 1244 l
689 1244 l
689 1245 l
689 1245 l
689 1245 l
689 1246 l
689 1246 l
688 1247 l
688 1247 l
688 1247 l
688 1248 l
688 1248 l
688 1248 l
687 1249 l
687 1249 l
687 1249 l
687 1250 l
687 1250 l
687 1250 l
687 1251 l
686 1251 l
686 1251 l
686 1252 l
686 1252 l
686 1253 l
686 1253 l
685 1253 l
685 1254 l
685 1254 l
685 1254 l
685 1255 l
685 1255 l
684 1255 l
684 1256 l
684 1256 l
684 1256 l
684 1257 l
684 1257 l
683 1257 l
683 1258 l
683 1258 l
683 1259 l
683 1259 l
683 1259 l
682 1260 l
682 1260 l
682 1260 l
682 1261 l
682 1261 l
682 1261 l
681 1262 l
681 1262 l
681 1262 l
681 1263 l
681 1263 l
681 1264 l
680 1264 l
680 1264 l
680 1265 l
680 1265 l
680 1265 l
680 1266 l
679 1266 l
679 1266 l
679 1267 l
679 1267 l
679 1267 l
679 1268 l
678 1268 l
678 1268 l
678 1269 l
678 1269 l
678 1270 l
678 1270 l
677 1270 l
677 1271 l
677 1271 l
677 1271 l
s
677 1271 m
677 1272 l
677 1272 l
676 1272 l
676 1273 l
676 1273 l
676 1273 l
676 1274 l
676 1274 l
676 1274 l
675 1275 l
675 1275 l
675 1276 l
675 1276 l
675 1276 l
675 1277 l
674 1277 l
674 1277 l
674 1278 l
674 1278 l
674 1278 l
674 1279 l
673 1279 l
673 1279 l
673 1280 l
673 1280 l
673 1281 l
673 1281 l
672 1281 l
672 1282 l
672 1282 l
672 1282 l
672 1283 l
672 1283 l
671 1283 l
671 1284 l
671 1284 l
671 1284 l
671 1285 l
671 1285 l
670 1285 l
670 1286 l
670 1286 l
670 1287 l
670 1287 l
670 1287 l
670 1288 l
669 1288 l
669 1288 l
669 1289 l
669 1289 l
669 1289 l
669 1290 l
668 1290 l
668 1290 l
668 1291 l
668 1291 l
668 1292 l
668 1292 l
667 1292 l
667 1293 l
667 1293 l
667 1293 l
667 1294 l
667 1294 l
666 1294 l
666 1295 l
666 1295 l
666 1295 l
666 1296 l
666 1296 l
665 1296 l
665 1297 l
665 1297 l
665 1298 l
665 1298 l
665 1298 l
665 1299 l
664 1299 l
664 1299 l
664 1300 l
664 1300 l
664 1300 l
664 1301 l
663 1301 l
663 1301 l
663 1302 l
663 1302 l
663 1302 l
663 1303 l
662 1303 l
662 1304 l
662 1304 l
662 1304 l
662 1305 l
662 1305 l
662 1305 l
661 1306 l
661 1306 l
661 1306 l
661 1307 l
661 1307 l
661 1307 l
660 1308 l
660 1308 l
660 1309 l
660 1309 l
660 1309 l
660 1310 l
659 1310 l
659 1310 l
659 1311 l
659 1311 l
659 1311 l
659 1312 l
658 1312 l
658 1312 l
658 1313 l
658 1313 l
658 1313 l
658 1314 l
658 1314 l
657 1315 l
657 1315 l
657 1315 l
657 1316 l
657 1316 l
657 1316 l
656 1317 l
656 1317 l
656 1317 l
656 1318 l
656 1318 l
656 1318 l
655 1319 l
655 1319 l
655 1319 l
655 1320 l
655 1320 l
655 1321 l
655 1321 l
654 1321 l
654 1322 l
654 1322 l
654 1322 l
654 1323 l
654 1323 l
653 1323 l
653 1324 l
653 1324 l
653 1324 l
653 1325 l
653 1325 l
652 1326 l
652 1326 l
652 1326 l
652 1327 l
652 1327 l
652 1327 l
652 1328 l
651 1328 l
651 1328 l
651 1329 l
651 1329 l
651 1329 l
651 1330 l
650 1330 l
650 1330 l
650 1331 l
650 1331 l
650 1332 l
650 1332 l
649 1332 l
649 1333 l
649 1333 l
649 1333 l
649 1334 l
649 1334 l
649 1334 l
648 1335 l
648 1335 l
648 1335 l
648 1336 l
648 1336 l
648 1337 l
647 1337 l
647 1337 l
647 1338 l
647 1338 l
647 1338 l
647 1339 l
647 1339 l
646 1339 l
646 1340 l
646 1340 l
646 1340 l
646 1341 l
646 1341 l
645 1341 l
645 1342 l
645 1342 l
645 1343 l
645 1343 l
645 1343 l
645 1344 l
644 1344 l
644 1344 l
644 1345 l
644 1345 l
644 1345 l
644 1346 l
643 1346 l
643 1346 l
643 1347 l
643 1347 l
643 1347 l
643 1348 l
642 1348 l
642 1349 l
642 1349 l
642 1349 l
642 1350 l
642 1350 l
642 1350 l
641 1351 l
641 1351 l
641 1351 l
641 1352 l
641 1352 l
641 1352 l
640 1353 l
640 1353 l
640 1354 l
640 1354 l
640 1354 l
640 1355 l
640 1355 l
639 1355 l
639 1356 l
639 1356 l
639 1356 l
639 1357 l
639 1357 l
638 1357 l
638 1358 l
638 1358 l
638 1358 l
638 1359 l
638 1359 l
638 1360 l
637 1360 l
637 1360 l
637 1361 l
637 1361 l
637 1361 l
637 1362 l
636 1362 l
s
636 1362 m
636 1362 l
636 1363 l
636 1363 l
636 1363 l
636 1364 l
636 1364 l
635 1364 l
635 1365 l
635 1365 l
635 1366 l
635 1366 l
635 1366 l
634 1367 l
634 1367 l
634 1367 l
634 1368 l
634 1368 l
634 1368 l
634 1369 l
633 1369 l
633 1369 l
633 1370 l
633 1370 l
633 1371 l
633 1371 l
632 1371 l
632 1372 l
632 1372 l
632 1372 l
632 1373 l
632 1373 l
632 1373 l
631 1374 l
631 1374 l
631 1374 l
631 1375 l
631 1375 l
631 1375 l
631 1376 l
630 1376 l
630 1377 l
630 1377 l
630 1377 l
630 1378 l
630 1378 l
629 1378 l
629 1379 l
629 1379 l
629 1379 l
629 1380 l
629 1380 l
629 1380 l
628 1381 l
628 1381 l
628 1382 l
628 1382 l
628 1382 l
628 1383 l
627 1383 l
627 1383 l
627 1384 l
627 1384 l
627 1384 l
627 1385 l
627 1385 l
626 1385 l
626 1386 l
626 1386 l
626 1386 l
626 1387 l
626 1387 l
626 1388 l
625 1388 l
625 1388 l
625 1389 l
625 1389 l
625 1389 l
625 1390 l
624 1390 l
624 1390 l
624 1391 l
624 1391 l
624 1391 l
624 1392 l
624 1392 l
623 1392 l
623 1393 l
623 1393 l
623 1394 l
623 1394 l
623 1394 l
623 1395 l
622 1395 l
622 1395 l
622 1396 l
622 1396 l
622 1396 l
622 1397 l
621 1397 l
621 1397 l
621 1398 l
621 1398 l
621 1399 l
621 1399 l
621 1399 l
620 1400 l
620 1400 l
620 1400 l
620 1401 l
620 1401 l
620 1401 l
620 1402 l
619 1402 l
619 1402 l
619 1403 l
619 1403 l
619 1403 l
619 1404 l
618 1404 l
618 1405 l
618 1405 l
618 1405 l
618 1406 l
618 1406 l
618 1406 l
617 1407 l
617 1407 l
617 1407 l
617 1408 l
617 1408 l
617 1408 l
617 1409 l
616 1409 l
616 1409 l
616 1410 l
616 1410 l
616 1411 l
616 1411 l
616 1411 l
615 1412 l
615 1412 l
615 1412 l
615 1413 l
615 1413 l
615 1413 l
614 1414 l
614 1414 l
614 1414 l
614 1415 l
614 1415 l
614 1416 l
614 1416 l
613 1416 l
613 1417 l
613 1417 l
613 1417 l
613 1418 l
613 1418 l
613 1418 l
612 1419 l
612 1419 l
612 1419 l
612 1420 l
612 1420 l
612 1420 l
612 1421 l
611 1421 l
611 1422 l
611 1422 l
611 1422 l
611 1423 l
611 1423 l
610 1423 l
610 1424 l
610 1424 l
610 1424 l
610 1425 l
610 1425 l
610 1425 l
609 1426 l
609 1426 l
609 1427 l
609 1427 l
609 1427 l
609 1428 l
609 1428 l
608 1428 l
608 1429 l
608 1429 l
608 1429 l
608 1430 l
608 1430 l
608 1430 l
607 1431 l
607 1431 l
607 1431 l
607 1432 l
607 1432 l
607 1433 l
607 1433 l
606 1433 l
606 1434 l
606 1434 l
606 1434 l
606 1435 l
606 1435 l
606 1435 l
605 1436 l
605 1436 l
605 1436 l
605 1437 l
605 1437 l
605 1437 l
604 1438 l
604 1438 l
604 1439 l
604 1439 l
604 1439 l
604 1440 l
604 1440 l
603 1440 l
603 1441 l
603 1441 l
603 1441 l
603 1442 l
603 1442 l
603 1442 l
602 1443 l
602 1443 l
602 1444 l
602 1444 l
602 1444 l
602 1445 l
602 1445 l
601 1445 l
601 1446 l
601 1446 l
601 1446 l
601 1447 l
601 1447 l
601 1447 l
600 1448 l
600 1448 l
600 1448 l
600 1449 l
600 1449 l
600 1450 l
600 1450 l
599 1450 l
599 1451 l
599 1451 l
599 1451 l
599 1452 l
599 1452 l
599 1452 l
598 1453 l
s
598 1453 m
598 1453 l
598 1453 l
598 1454 l
598 1454 l
598 1454 l
598 1455 l
597 1455 l
597 1456 l
597 1456 l
597 1456 l
597 1457 l
597 1457 l
597 1457 l
596 1458 l
596 1458 l
596 1458 l
596 1459 l
596 1459 l
596 1459 l
596 1460 l
595 1460 l
595 1461 l
595 1461 l
595 1461 l
595 1462 l
595 1462 l
595 1462 l
594 1463 l
594 1463 l
594 1463 l
594 1464 l
594 1464 l
594 1464 l
594 1465 l
593 1465 l
593 1465 l
593 1466 l
593 1466 l
593 1467 l
593 1467 l
593 1467 l
592 1468 l
592 1468 l
592 1468 l
592 1469 l
592 1469 l
592 1469 l
592 1470 l
591 1470 l
591 1470 l
591 1471 l
591 1471 l
591 1472 l
591 1472 l
591 1472 l
590 1473 l
590 1473 l
590 1473 l
590 1474 l
590 1474 l
590 1474 l
590 1475 l
589 1475 l
589 1475 l
589 1476 l
589 1476 l
589 1476 l
589 1477 l
589 1477 l
588 1478 l
588 1478 l
588 1478 l
588 1479 l
588 1479 l
588 1479 l
588 1480 l
587 1480 l
587 1480 l
587 1481 l
587 1481 l
587 1481 l
587 1482 l
587 1482 l
586 1482 l
586 1483 l
586 1483 l
586 1484 l
586 1484 l
586 1484 l
586 1485 l
585 1485 l
585 1485 l
585 1486 l
585 1486 l
585 1486 l
585 1487 l
585 1487 l
584 1487 l
584 1488 l
584 1488 l
584 1489 l
584 1489 l
584 1489 l
584 1490 l
584 1490 l
583 1490 l
583 1491 l
583 1491 l
583 1491 l
583 1492 l
583 1492 l
583 1492 l
582 1493 l
582 1493 l
582 1493 l
582 1494 l
582 1494 l
582 1495 l
582 1495 l
581 1495 l
581 1496 l
581 1496 l
581 1496 l
581 1497 l
581 1497 l
581 1497 l
580 1498 l
580 1498 l
580 1498 l
580 1499 l
580 1499 l
580 1499 l
580 1500 l
579 1500 l
579 1501 l
579 1501 l
579 1501 l
579 1502 l
579 1502 l
579 1502 l
578 1503 l
578 1503 l
578 1503 l
578 1504 l
578 1504 l
578 1504 l
578 1505 l
578 1505 l
577 1506 l
577 1506 l
577 1506 l
577 1507 l
577 1507 l
577 1507 l
577 1508 l
576 1508 l
576 1508 l
576 1509 l
576 1509 l
576 1509 l
576 1510 l
576 1510 l
575 1510 l
575 1511 l
575 1511 l
575 1512 l
575 1512 l
575 1512 l
575 1513 l
574 1513 l
574 1513 l
574 1514 l
574 1514 l
574 1514 l
574 1515 l
574 1515 l
574 1515 l
573 1516 l
573 1516 l
573 1517 l
573 1517 l
573 1517 l
573 1518 l
573 1518 l
572 1518 l
572 1519 l
572 1519 l
572 1519 l
572 1520 l
572 1520 l
572 1520 l
571 1521 l
571 1521 l
571 1521 l
571 1522 l
571 1522 l
571 1523 l
571 1523 l
571 1523 l
570 1524 l
570 1524 l
570 1524 l
570 1525 l
570 1525 l
570 1525 l
570 1526 l
569 1526 l
569 1526 l
569 1527 l
569 1527 l
569 1527 l
569 1528 l
569 1528 l
568 1529 l
568 1529 l
568 1529 l
568 1530 l
568 1530 l
568 1530 l
568 1531 l
568 1531 l
567 1531 l
567 1532 l
567 1532 l
567 1532 l
567 1533 l
567 1533 l
567 1534 l
566 1534 l
566 1534 l
566 1535 l
566 1535 l
s
lw
[20 20] 10 setdash
295 1181 m
295 1181 l
295 1181 l
296 1182 l
296 1182 l
297 1182 l
297 1183 l
297 1183 l
298 1183 l
298 1184 l
298 1184 l
299 1184 l
299 1185 l
299 1185 l
300 1186 l
300 1186 l
300 1186 l
301 1187 l
301 1187 l
302 1187 l
302 1188 l
302 1188 l
303 1188 l
303 1189 l
303 1189 l
304 1189 l
304 1190 l
304 1190 l
305 1191 l
305 1191 l
305 1191 l
306 1192 l
306 1192 l
306 1192 l
307 1193 l
307 1193 l
308 1193 l
308 1194 l
308 1194 l
309 1194 l
309 1195 l
309 1195 l
310 1195 l
310 1196 l
310 1196 l
311 1197 l
311 1197 l
311 1197 l
312 1198 l
312 1198 l
312 1198 l
313 1199 l
313 1199 l
314 1199 l
314 1200 l
314 1200 l
315 1200 l
315 1201 l
315 1201 l
316 1202 l
316 1202 l
316 1202 l
317 1203 l
317 1203 l
317 1203 l
318 1204 l
318 1204 l
319 1204 l
319 1205 l
319 1205 l
320 1205 l
320 1206 l
320 1206 l
321 1206 l
321 1207 l
321 1207 l
322 1208 l
322 1208 l
322 1208 l
323 1209 l
323 1209 l
323 1209 l
324 1210 l
324 1210 l
325 1210 l
325 1211 l
325 1211 l
326 1211 l
326 1212 l
326 1212 l
327 1212 l
327 1213 l
327 1213 l
328 1214 l
328 1214 l
328 1214 l
329 1215 l
329 1215 l
329 1215 l
330 1216 l
330 1216 l
331 1216 l
331 1217 l
331 1217 l
332 1217 l
332 1218 l
332 1218 l
333 1219 l
333 1219 l
333 1219 l
334 1220 l
334 1220 l
334 1220 l
335 1221 l
335 1221 l
336 1221 l
336 1222 l
336 1222 l
337 1222 l
337 1223 l
337 1223 l
338 1223 l
338 1224 l
338 1224 l
339 1225 l
339 1225 l
339 1225 l
340 1226 l
340 1226 l
340 1226 l
341 1227 l
341 1227 l
342 1227 l
342 1228 l
342 1228 l
343 1228 l
343 1229 l
343 1229 l
344 1229 l
344 1230 l
344 1230 l
345 1231 l
345 1231 l
345 1231 l
346 1232 l
346 1232 l
347 1232 l
347 1233 l
347 1233 l
348 1233 l
348 1234 l
348 1234 l
349 1234 l
349 1235 l
349 1235 l
350 1236 l
350 1236 l
350 1236 l
351 1237 l
351 1237 l
351 1237 l
352 1238 l
352 1238 l
353 1238 l
353 1239 l
353 1239 l
354 1239 l
354 1240 l
354 1240 l
355 1240 l
355 1241 l
355 1241 l
356 1242 l
356 1242 l
356 1242 l
357 1243 l
357 1243 l
357 1243 l
358 1244 l
358 1244 l
359 1244 l
359 1245 l
359 1245 l
360 1245 l
360 1246 l
360 1246 l
361 1247 l
361 1247 l
361 1247 l
362 1248 l
362 1248 l
362 1248 l
363 1249 l
363 1249 l
364 1249 l
364 1250 l
364 1250 l
365 1250 l
365 1251 l
365 1251 l
366 1251 l
366 1252 l
366 1252 l
367 1253 l
367 1253 l
367 1253 l
368 1254 l
368 1254 l
368 1254 l
369 1255 l
369 1255 l
370 1255 l
370 1256 l
370 1256 l
371 1256 l
371 1257 l
371 1257 l
372 1257 l
372 1258 l
372 1258 l
373 1259 l
373 1259 l
373 1259 l
374 1260 l
374 1260 l
374 1260 l
375 1261 l
375 1261 l
376 1261 l
376 1262 l
376 1262 l
377 1262 l
377 1263 l
377 1263 l
378 1264 l
378 1264 l
378 1264 l
379 1265 l
379 1265 l
379 1265 l
380 1266 l
380 1266 l
381 1266 l
381 1267 l
381 1267 l
382 1267 l
382 1268 l
382 1268 l
383 1268 l
383 1269 l
383 1269 l
384 1270 l
384 1270 l
384 1270 l
385 1271 l
385 1271 l
385 1271 l
s
385 1271 m
386 1272 l
386 1272 l
387 1272 l
387 1273 l
387 1273 l
388 1273 l
388 1274 l
388 1274 l
389 1274 l
389 1275 l
389 1275 l
390 1276 l
390 1276 l
390 1276 l
391 1277 l
391 1277 l
392 1277 l
392 1278 l
392 1278 l
393 1278 l
393 1279 l
393 1279 l
394 1279 l
394 1280 l
394 1280 l
395 1281 l
395 1281 l
395 1281 l
396 1282 l
396 1282 l
396 1282 l
397 1283 l
397 1283 l
398 1283 l
398 1284 l
398 1284 l
399 1284 l
399 1285 l
399 1285 l
400 1285 l
400 1286 l
400 1286 l
401 1287 l
401 1287 l
401 1287 l
402 1288 l
402 1288 l
402 1288 l
403 1289 l
403 1289 l
404 1289 l
404 1290 l
404 1290 l
405 1290 l
405 1291 l
405 1291 l
406 1292 l
406 1292 l
406 1292 l
407 1293 l
407 1293 l
407 1293 l
408 1294 l
408 1294 l
409 1294 l
409 1295 l
409 1295 l
410 1295 l
410 1296 l
410 1296 l
411 1296 l
411 1297 l
411 1297 l
412 1298 l
412 1298 l
412 1298 l
413 1299 l
413 1299 l
413 1299 l
414 1300 l
414 1300 l
415 1300 l
415 1301 l
415 1301 l
416 1301 l
416 1302 l
416 1302 l
417 1302 l
417 1303 l
417 1303 l
418 1304 l
418 1304 l
418 1304 l
419 1305 l
419 1305 l
419 1305 l
420 1306 l
420 1306 l
421 1306 l
421 1307 l
421 1307 l
422 1307 l
422 1308 l
422 1308 l
423 1309 l
423 1309 l
423 1309 l
424 1310 l
424 1310 l
424 1310 l
425 1311 l
425 1311 l
426 1311 l
426 1312 l
426 1312 l
427 1312 l
427 1313 l
427 1313 l
428 1313 l
428 1314 l
428 1314 l
429 1315 l
429 1315 l
429 1315 l
430 1316 l
430 1316 l
430 1316 l
431 1317 l
431 1317 l
432 1317 l
432 1318 l
432 1318 l
433 1318 l
433 1319 l
433 1319 l
434 1319 l
434 1320 l
434 1320 l
435 1321 l
435 1321 l
435 1321 l
436 1322 l
436 1322 l
437 1322 l
437 1323 l
437 1323 l
438 1323 l
438 1324 l
438 1324 l
439 1324 l
439 1325 l
439 1325 l
440 1326 l
440 1326 l
440 1326 l
441 1327 l
441 1327 l
441 1327 l
442 1328 l
442 1328 l
443 1328 l
443 1329 l
443 1329 l
444 1329 l
444 1330 l
444 1330 l
445 1330 l
445 1331 l
445 1331 l
446 1332 l
446 1332 l
446 1332 l
447 1333 l
447 1333 l
447 1333 l
448 1334 l
448 1334 l
449 1334 l
449 1335 l
449 1335 l
450 1335 l
450 1336 l
450 1336 l
451 1337 l
451 1337 l
451 1337 l
452 1338 l
452 1338 l
452 1338 l
453 1339 l
453 1339 l
454 1339 l
454 1340 l
454 1340 l
455 1340 l
455 1341 l
455 1341 l
456 1341 l
456 1342 l
456 1342 l
457 1343 l
457 1343 l
457 1343 l
458 1344 l
458 1344 l
458 1344 l
459 1345 l
459 1345 l
460 1345 l
460 1346 l
460 1346 l
461 1346 l
461 1347 l
461 1347 l
462 1347 l
462 1348 l
462 1348 l
463 1349 l
463 1349 l
463 1349 l
464 1350 l
464 1350 l
464 1350 l
465 1351 l
465 1351 l
466 1351 l
466 1352 l
466 1352 l
467 1352 l
467 1353 l
467 1353 l
468 1354 l
468 1354 l
468 1354 l
469 1355 l
469 1355 l
469 1355 l
470 1356 l
470 1356 l
471 1356 l
471 1357 l
471 1357 l
472 1357 l
472 1358 l
472 1358 l
473 1358 l
473 1359 l
473 1359 l
474 1360 l
474 1360 l
474 1360 l
475 1361 l
475 1361 l
475 1361 l
476 1362 l
476 1362 l
s
476 1362 m
477 1362 l
477 1363 l
477 1363 l
478 1363 l
478 1364 l
478 1364 l
479 1364 l
479 1365 l
479 1365 l
480 1366 l
480 1366 l
480 1366 l
481 1367 l
481 1367 l
482 1367 l
482 1368 l
482 1368 l
483 1368 l
483 1369 l
483 1369 l
484 1369 l
484 1370 l
484 1370 l
485 1371 l
485 1371 l
485 1371 l
486 1372 l
486 1372 l
486 1372 l
487 1373 l
487 1373 l
488 1373 l
488 1374 l
488 1374 l
489 1374 l
489 1375 l
489 1375 l
490 1375 l
490 1376 l
490 1376 l
491 1377 l
491 1377 l
491 1377 l
492 1378 l
492 1378 l
492 1378 l
493 1379 l
493 1379 l
494 1379 l
494 1380 l
494 1380 l
495 1380 l
495 1381 l
495 1381 l
496 1382 l
496 1382 l
496 1382 l
497 1383 l
497 1383 l
497 1383 l
498 1384 l
498 1384 l
499 1384 l
499 1385 l
499 1385 l
500 1385 l
500 1386 l
500 1386 l
501 1386 l
501 1387 l
501 1387 l
502 1388 l
502 1388 l
502 1388 l
503 1389 l
503 1389 l
503 1389 l
504 1390 l
504 1390 l
505 1390 l
505 1391 l
505 1391 l
506 1391 l
506 1392 l
506 1392 l
507 1392 l
507 1393 l
507 1393 l
508 1394 l
508 1394 l
508 1394 l
509 1395 l
509 1395 l
509 1395 l
510 1396 l
510 1396 l
511 1396 l
511 1397 l
511 1397 l
512 1397 l
512 1398 l
512 1398 l
513 1399 l
513 1399 l
513 1399 l
514 1400 l
514 1400 l
514 1400 l
515 1401 l
515 1401 l
516 1401 l
516 1402 l
516 1402 l
517 1402 l
517 1403 l
517 1403 l
518 1403 l
518 1404 l
518 1404 l
519 1405 l
519 1405 l
519 1405 l
520 1406 l
520 1406 l
520 1406 l
521 1407 l
521 1407 l
522 1407 l
522 1408 l
522 1408 l
523 1408 l
523 1409 l
523 1409 l
524 1409 l
524 1410 l
524 1410 l
525 1411 l
525 1411 l
525 1411 l
526 1412 l
526 1412 l
527 1412 l
527 1413 l
527 1413 l
528 1413 l
528 1414 l
528 1414 l
529 1414 l
529 1415 l
529 1415 l
530 1416 l
530 1416 l
530 1416 l
531 1417 l
531 1417 l
531 1417 l
532 1418 l
532 1418 l
533 1418 l
533 1419 l
533 1419 l
534 1419 l
534 1420 l
534 1420 l
535 1420 l
535 1421 l
535 1421 l
536 1422 l
536 1422 l
536 1422 l
537 1423 l
537 1423 l
537 1423 l
538 1424 l
538 1424 l
539 1424 l
539 1425 l
539 1425 l
540 1425 l
540 1426 l
540 1426 l
541 1427 l
541 1427 l
541 1427 l
542 1428 l
542 1428 l
542 1428 l
543 1429 l
543 1429 l
544 1429 l
544 1430 l
544 1430 l
545 1430 l
545 1431 l
545 1431 l
546 1431 l
546 1432 l
546 1432 l
547 1433 l
547 1433 l
547 1433 l
548 1434 l
548 1434 l
548 1434 l
549 1435 l
549 1435 l
550 1435 l
550 1436 l
550 1436 l
551 1436 l
551 1437 l
551 1437 l
552 1437 l
552 1438 l
552 1438 l
553 1439 l
553 1439 l
553 1439 l
554 1440 l
554 1440 l
554 1440 l
555 1441 l
555 1441 l
556 1441 l
556 1442 l
556 1442 l
557 1442 l
557 1443 l
557 1443 l
558 1444 l
558 1444 l
558 1444 l
559 1445 l
559 1445 l
559 1445 l
560 1446 l
560 1446 l
561 1446 l
561 1447 l
561 1447 l
562 1447 l
562 1448 l
562 1448 l
563 1448 l
563 1449 l
563 1449 l
564 1450 l
564 1450 l
564 1450 l
565 1451 l
565 1451 l
565 1451 l
566 1452 l
566 1452 l
567 1452 l
567 1453 l
s
567 1453 m
567 1453 l
568 1453 l
568 1454 l
568 1454 l
569 1454 l
569 1455 l
569 1455 l
570 1456 l
570 1456 l
570 1456 l
571 1457 l
571 1457 l
572 1457 l
572 1458 l
572 1458 l
573 1458 l
573 1459 l
573 1459 l
574 1459 l
574 1460 l
574 1460 l
575 1461 l
575 1461 l
575 1461 l
576 1462 l
576 1462 l
576 1462 l
577 1463 l
577 1463 l
578 1463 l
578 1464 l
578 1464 l
579 1464 l
579 1465 l
579 1465 l
580 1465 l
580 1466 l
580 1466 l
581 1467 l
581 1467 l
581 1467 l
582 1468 l
582 1468 l
582 1468 l
583 1469 l
583 1469 l
584 1469 l
584 1470 l
584 1470 l
585 1470 l
585 1471 l
585 1471 l
586 1472 l
586 1472 l
586 1472 l
587 1473 l
587 1473 l
587 1473 l
588 1474 l
588 1474 l
589 1474 l
589 1475 l
589 1475 l
590 1475 l
590 1476 l
590 1476 l
591 1476 l
591 1477 l
591 1477 l
592 1478 l
592 1478 l
592 1478 l
593 1479 l
593 1479 l
593 1479 l
594 1480 l
594 1480 l
595 1480 l
595 1481 l
595 1481 l
596 1481 l
596 1482 l
596 1482 l
597 1482 l
597 1483 l
597 1483 l
598 1484 l
598 1484 l
598 1484 l
599 1485 l
599 1485 l
599 1485 l
600 1486 l
600 1486 l
601 1486 l
601 1487 l
601 1487 l
602 1487 l
602 1488 l
602 1488 l
603 1489 l
603 1489 l
603 1489 l
604 1490 l
604 1490 l
604 1490 l
605 1491 l
605 1491 l
606 1491 l
606 1492 l
606 1492 l
607 1492 l
607 1493 l
607 1493 l
608 1493 l
608 1494 l
608 1494 l
609 1495 l
609 1495 l
609 1495 l
610 1496 l
610 1496 l
610 1496 l
611 1497 l
611 1497 l
612 1497 l
612 1498 l
612 1498 l
613 1498 l
613 1499 l
613 1499 l
614 1499 l
614 1500 l
614 1500 l
615 1501 l
615 1501 l
615 1501 l
616 1502 l
616 1502 l
617 1502 l
617 1503 l
617 1503 l
618 1503 l
618 1504 l
618 1504 l
619 1504 l
619 1505 l
619 1505 l
620 1506 l
620 1506 l
620 1506 l
621 1507 l
621 1507 l
621 1507 l
622 1508 l
622 1508 l
623 1508 l
623 1509 l
623 1509 l
624 1509 l
624 1510 l
624 1510 l
625 1510 l
625 1511 l
625 1511 l
626 1512 l
626 1512 l
626 1512 l
627 1513 l
627 1513 l
627 1513 l
628 1514 l
628 1514 l
629 1514 l
629 1515 l
629 1515 l
630 1515 l
630 1516 l
630 1516 l
631 1517 l
631 1517 l
631 1517 l
632 1518 l
632 1518 l
632 1518 l
633 1519 l
633 1519 l
634 1519 l
634 1520 l
634 1520 l
635 1520 l
635 1521 l
635 1521 l
636 1521 l
636 1522 l
636 1522 l
637 1523 l
637 1523 l
637 1523 l
638 1524 l
638 1524 l
638 1524 l
639 1525 l
639 1525 l
640 1525 l
640 1526 l
640 1526 l
641 1526 l
641 1527 l
641 1527 l
642 1527 l
642 1528 l
642 1528 l
643 1529 l
643 1529 l
643 1529 l
644 1530 l
644 1530 l
644 1530 l
645 1531 l
645 1531 l
646 1531 l
646 1532 l
646 1532 l
647 1532 l
647 1533 l
647 1533 l
648 1534 l
648 1534 l
648 1534 l
649 1535 l
649 1535 l
s
590 1181 m
590 1476 l
s
590 1476 m
295 1476 l
s
590 1228 m
295 1228 l
s
[] 0 setdash
649 1181 m
649 1535 l
s
-59 1535 m
649 1535 l
s
-59 1535 m
-59 1181 l
s
stroke
end
EndOfTheIncludedPostscriptMagicCookie
\closepsdump
%==============================================================================


%==============================================================================
% PHI_FG.TEX
\psdump{phi_fg.tex}%paperxsize:12.000
%paperysize: 5.000
\def\point#1 #2 #3 {\rlap{\kern #1 truecm
\raise #2 truecm \hbox{#3}}}
\def\spot{{\kern
-0.2em\lower.55ex\hbox{$\bullet$}}}
\def\clap#1{{\setbox0=\hbox{#1}\dimen0
=\wd0\divide\dimen0
by 2\hskip-\dimen0\box0}}
\def\dlap#1{{\setbox0=\hbox{#1}\dimen0
=\ht0\divide\dimen0
by 1\raise-\dimen0\box0}}
\def\ulap#1{{\setbox0=\hbox{#1}\dimen0
=\ht0\divide\dimen0
by 1\raise\dimen0\box0}}
\def\nlap#1{{\setbox0=\hbox{#1}\dimen0
=\ht0\divide\dimen0
by 2\raise-\dimen0\box0}}
\smash{\hbox{
\point       3.35       4.30 {$\phi$}
\point       3.90       2.10 {$1$}
\point      11.40       2.10 {$1$}
\point       9.30       2.10 {$\lambda^2$}
\point      10.10       4.45 {$f$}
\point       9.75       6.00 {$g$}
\point       8.70       4.85 {$1$}
}}
EndOfTheIncludedPostscriptMagicCookie
\closepsdump
%==============================================================================



%==============================================================================
% S_RANGE.PS
\psdump{s_range.ps}%!
/jpedict 250 dict def jpedict begin
/Cou /Times-Roman findfont 50.000000 scalefont def
/Sym /Symbol      findfont 50.000000 scalefont def
/lw{0.700000 setlinewidth}def
/ll{3.000000 setlinewidth}def
newpath
-0.240000 0.240000 scale
90 rotate
1 setlinecap
/r{moveto 0 1 rlineto stroke}def
/m{moveto}def
/l{lineto}def
/s{stroke}def
0 0 m
lw
1.000000 1.000000 scale
177 0 m
177 1653 l
s
159 60 m
194 60 l
s
177 1653 m
170 1630 l
s
177 1653 m
184 1630 l
s
lw
newpath
203 360 m
203 1172 l
150 1172 l
150 360 l
203 360 l
closepath
0.800000 setgray
eofill
0.0 setgray
ll
177 180 m
177 1382 l
s
159 180 m
194 180 l
s
159 1382 m
194 1382 l
s
159 511 m
194 511 l
s
lw
stroke
end
EndOfTheIncludedPostscriptMagicCookie
\closepsdump
%==============================================================================



%==============================================================================
% S_RANGE.TEX
\psdump{s_range.tex}%paperxsize:14.000
%paperysize: 3.000
\def\point#1 #2 #3 {\rlap{\kern #1 truecm
\raise #2 truecm \hbox{#3}}}
\def\spot{{\kern
-0.2em\lower.55ex\hbox{$\bullet$}}}
\def\clap#1{{\setbox0=\hbox{#1}\dimen0
=\wd0\divide\dimen0
by 2\hskip-\dimen0\box0}}
\def\dlap#1{{\setbox0=\hbox{#1}\dimen0
=\ht0\divide\dimen0
by 1\raise-\dimen0\box0}}
\def\ulap#1{{\setbox0=\hbox{#1}\dimen0
=\ht0\divide\dimen0
by 1\raise\dimen0\box0}}
\def\nlap#1{{\setbox0=\hbox{#1}\dimen0
=\ht0\divide\dimen0
by 2\raise-\dimen0\box0}}
\smash{\hbox{
\point      13.20       1.10 {$\real$}
\point       1.85       0.80 {$2^{-500}$}
\point       8.53       0.80 {$2^{500}$}
\point       0.18       0.80 {$2^{-1022}$}
\point      10.01       0.80 {$(1-2^{-53})2^{1024}$}
\point       3.23       0.80 {$1$}
\point      -0.59       0.80 {$0$}
\point       2.05       2.25 {$\scriptfont0=\tenrm
\overbrace{\hbox to 5.7cm{}}
^{\rm positive\ part\ of\ safe\ range}$}
\point       0.53       0.45 {$\scriptfont0=\tenrm
\underbrace{\hbox to 8.5cm{}}
_{\rm positive\ representable\ numbers}$}
}}
EndOfTheIncludedPostscriptMagicCookie
\closepsdump
%==============================================================================



%==============================================================================
% FIGTEX2.TEX
%%%%%%%%%%%%%%%%%%%%
%  WITH COUNTER
%%%%%%%%%%%%%%%%%%%%%

\newdimen\texpscorrection
\texpscorrection=0truecm %must be 0.15truecm in ps_fonts
\font\eightrm=cmr8
\def \eightpoint{\rm}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% macros  for cross reference %%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%
%% defining the symbolic value
%%
\def\ifff(#1,#2,#3){\ifundefined{#1#2}
\expandafter\xdef\csname #1#2\endcsname{#3}\else
\write16{!!!!!doubly defined #1,#2}\fi}
\def\NEWDEF #1,#2,#3 {\ifff({#1},{#2},{#3})}
%%
%%  referring to something
%%
\def\ifundefined#1{\expandafter\ifx\csname#1\endcsname\relax}
%=============postscript=======
%figure psfile height (in cm) width (in cm) caption  (will be centered)
\newcount\FIGUREcount \FIGUREcount=0
\newskip\ttglue
\newdimen\figcenter
\def\figure #1 #2 #3 #4\cr{\null\ifundefined{fig#1}\global
\advance\FIGUREcount by 1\NEWDEF fig,#1,{Fig.~\number\FIGUREcount}\fi
\write16{ FIG \number\FIGUREcount: #1}
{\goodbreak\figcenter=\hsize\relax
\advance\figcenter by -#3truecm
\divide\figcenter by 2
\midinsert\vskip #2truecm\noindent\hskip\figcenter
\special{psfile=#1}\vskip 0.8truecm\noindent \vbox{\eightpoint\noindent
{\bf\fig(#1)}: #4}\endinsert}}
%figurewithtex psfile texfile height (in cm) width (in cm) caption  (will be centered)
\def\figurewithtex #1 #2 #3 #4 #5\cr{\null\ifundefined{fig#1}\global
\advance\FIGUREcount by 1\NEWDEF fig,#1,{Fig.~\number\FIGUREcount}\fi
\write16{ FIG \number\FIGUREcount: #1}
{\goodbreak\figcenter=\hsize\relax
\advance\figcenter by -#4truecm
\divide\figcenter by 2

%\midinsert
\bigskip\vbox{

\vskip #3truecm\noindent\hskip\figcenter
\special{psfile=#1}{\hskip\texpscorrection\input #2 }\vskip 0.8truecm\noindent \vbox{\eightpoint\noindent
{\bf\fig(#1)}: #5}

}\bigbreak
%\endinsert

}}
\def\fig(#1){\ifundefined{fig#1}\global
\advance\FIGUREcount by 1\NEWDEF fig,#1,{Fig.~\number\FIGUREcount}
\fi
\csname fig#1\endcsname\relax}
%==============================================================================



%==============================================================================
% ABSTRACT.5
\vskip.4in
\cl{{\huge Computer--Assisted Proofs in Analysis and}}
\cl{{\huge Programming in Logic: A Case Study}}
\vskip.6in
\cl{Hans Koch
\footnote{$\!\!^1$}
{{\small Supported in Part by the
National Science Foundation under Grant No. DMS--9103590,
and by the Texas Advanced Research Program under Grant No. ARP--035.}}}
\cl{Department of Mathematics, University of Texas at Austin}
\cl{Austin, TX 78712}
\vskip.25in
\cl{Alain Schenkel$^2$, Peter Wittwer
\footnote{$\!\!^2$}
{{\small Supported in Part by the
Swiss National Science Foundation.}}}
\cl{D\'epartement de Physique Th\'eorique, Universit\'e de Gen\`eve}
\cl{Gen\`eve, CH 1211}
\vskip.8in
\abstract
In this paper we present a computer--assisted proof of the existence of a
solution for the Feigenbaum equation
$\varphi(x)={1\over\lambda}\varphi(\varphi(\lambda x)).$
There exist by now various such proofs in
the literature. Although the one presented here
is new, the main purpose of
this paper is not to provide yet another version,
but to give an easy--to--read and
self contained introduction to the technique of
computer--assisted proofs in analysis.
Our proof is written in Prolog
({\bf Pro}gramming in {\bf log}ic), a programming language which we found
to be well suited for this purpose.
In this paper we also give an introduction to Prolog,
so that even a reader
without prior exposure to programming should be
able to verify the correctness of the proof.
\par\vfill\eject
%==============================================================================



%==============================================================================

\leftline{\xbold Table of Contents}
\bigskip

\item{}
 {{\bf1. Introduction}\hfill 2}
\bigskip

\item{}
 {{\bf2. Prolog}\hfill 5}
\itemitem{}
 {2.1. The Syntax of Prolog Terms \hfill 5}
\smallskip

\itemitem{}
 {2.2. The Operator Syntax for Prolog Terms \hfill 6}
\smallskip

\itemitem{}
 {2.3. The List Notation \hfill 8}
\smallskip

\itemitem{}
 {2.4. The Syntax of Prolog Programs \hfill 8}
\smallskip

\itemitem{}
 {2.5. Matching Terms \hfill 9}
\smallskip

\itemitem{}
 {2.6. Program Execution \hfill 10}
\smallskip

\itemitem{}
 {2.7. Built--in Predicates \hfill 11}
\smallskip

\itemitem{}
 {2.8. Syntax Used in the Proof \hfill 13}
\bigskip

\item{}
 {{\bf3. 64bit IEEE Arithmetic and Rounding }\hfill 13}
\bigskip

\item{}
 {{\bf4. Interval Analysis } \hfill 18}
\bigskip

\item{}
 {{\bf5. Elementary Operations with Real Numbers }\hfill 19}
\bigskip

\item{}
 {{\bf6. The Contraction Mapping Principle } \hfill 22}
\bigskip

\item{}
 {{\bf7. Bounds Involving Polynomials} \hfill 23}
\bigskip

\item{}
 {{\bf8. Approximate Computations with Polynomials} \hfill 26}
\bigskip

\item{}
 {{\bf9. Bounds Involving Analytic Functions} \hfill 29}
\bigskip

\item{}
 {{\bf10. The Schr\"oder Equation} \hfill 34}
\bigskip

\item{}
 {{\bf11. Bounds on Maps and Operators} \hfill 37}
\bigskip

\item{}
 {{\bf12. Derivatives   } \hfill 39}
\bigskip

\item{}
 {{\bf13. General Clauses } \hfill 42}
\itemitem{}
 {13.1. Differences, Quotients, and Powers \hfill 43}
\smallskip

\itemitem{}
 {13.2. Expression Evaluation \hfill 44}
\smallskip

\itemitem{}
 {13.3. Sorting Numbers \hfill 45}
\bigskip

\item{}
 {{\bf14. Proving the Theorem  } \hfill 45}
\bigskip

\item{}
 {{\bf15. Appendix: Running the Program } \hfill 47}
\bigskip

\leftline{\bf Acknowledgements}
\medskip

\leftline{\bf References}




\par\vfill\eject
%==============================================================================



%==============================================================================
\openout3=proof.pl
%==============================================================================



%==============================================================================
%PROOF.59
\section Introduction

The aim of this paper is to give a self contained introduction
to the technique of computer--assisted proofs in analysis.
We center our discussion around a proof
of the existence of a function $\varphi$
that satisfies, for some real number $\lambda$, the Feigenbaum equation
$$
\varphi(x)={1\over\lambda}\varphi(\varphi(\lambda x))
\equation(1)
$$
on the interval $|x|<\sqrt{2.7}$.
Our solution $\varphi=\phi$ of this equation
is even, has a quadratic maximum at $x=0$,
vanishes at $x=1$,
and extends analytically to the complex domain $|x^2-1|<1.7$.
The graph of this function is depicted in Fig.1.
%------------------------ Fig.1---------------------------------------
\vskip 1.0truecm
\figurewithtex  phi_fg.ps phi_fg.tex 5 12 Graphs of the function
$\phi$ and of the corresponding functions $f$ and $g$\cr
\vskip 0.0truecm
%------------------------ Fig.1---------------------------------------
We note that the existence of solutions to \equ(1) is well known;
see [La1\... La4] for computer--assisted proofs
and [E] for other methods and a review on the subject.
The proof presented here is new, but as mentioned above,
this is not the main point of this paper.
For convenience later on,
we shall now reformulate the Feigenbaum problem.

One of the basic properties of equation \equ(1) is its scale invariance.
That is, if $\varphi$ is a solution, then ${1\over s}\varphi(s \cdot )$
is again a solution, for any real number $s\not=0$.
The following normalization condition will be imposed
to break this scale invariance:
$$
\varphi(1)=0.
\equation(1a)
$$
We note that
by setting $x=1$ in \equ(1), we obtain from \equ(1a)
the implicit equation
$\varphi(\varphi(\lambda))=0$
for the scaling factor $\lambda.$

Considering now only even $\varphi$'s,
we can write $\varphi(x)=f(x^2)$ for some function $f$.
In this case, equation \equ(1) becomes equivalent to the pair of equations
$$
f(z)={1\over\lambda}f(g(z)),
\equation(2)
$$
$$
g(z)=f(\lambda^2 z)^2,
\equation(3)
$$
and the condition \equ(1a) becomes $f(1)=0$.
The graphs of the functions $f$ and $g$ which correspond to
the solution $\phi$ are shown in Fig.1.

If $x=1$ is the only zero of $f$ in the domain of interest, then
$f(1)=0$ implies,
together with equations \equ(2) and \equ(3), the additional
normalization conditions
$g(1)=1$, $f(\lambda^2)^2=1$, and $g^\prime(1)=\lambda$,
where $g^\prime$ denotes the first derivative of $g.$

In what follows, we restrict our search for solutions of
\equ(2) and \equ(3) to functions $f$ and $g$
which are analytic on the disk $|z-1|<1.7$,
and which satisfy all of the normalization conditions mentioned above.
To this end,
it is convenient to change coordinates and to choose
$x=1$ as the new origin.
Define two functions $F$ and $G$ by setting
$F(z)=f(1+z)$ and $G(z)=g(1+z)-1.$
Then the equations \equ(2) and \equ(3) can be rewritten as
$$
F(z)={1\over\lambda}F(G(z)),
\equation(4)
$$
$$
G(z)=F(-1+\lambda^2+\lambda^2 z)^2-1,
\equation(5)
$$
and the normalization conditions become
$$
F(0)=0,\ \ F(-1+\lambda^2)^2=1,\ \ G(0)=0,\ \ G^\prime(0)=\lambda.
\equation(6)
$$
Equation
\equ(4) is known as the Schr\"oder equation.
It is of some interest on its own, since the solution $F$
conjugates the function $G$ to its linear part; formally
$F(G(F^{-1}(z)))=\lambda z.$

\claim Definition(bbb) Let $\BB$ be the Banach space of all analytic
functions $H$, $H(z)=\sum_{i\ge0}H_i\ z^i$, from the disk
$$
\Omega=\{z\in\complex|\ |z|<D\}
\equation(7)
$$
of radius
$$
D=1.7
\equation(7a)
$$
to the complex plane, which have real Taylor coefficients $H_i$
and a finite norm
$$
\|H\|=\sum_{i\ge0}|H_i|\ {D}^i .
\equation(8)
$$
Furthermore, define $\BB_0$ to be the subspace
of all functions in $\BB$ that vanish at $z=0.$

In this paper we prove the following.

\claim Theorem(1) There exist functions $F$ and $G$ in $\BB_0$,
and a negative real number $\lambda$,
such that for every $z\in\Omega$,
the values $G(z)$ and $-1+\lambda^2+\lambda^2z$ are in $\Omega$,
and the equations \equ(4), \equ(5), and \equ(6) are satisfied.

Our proof of \clm(1) uses estimates that have been carried out
by a computer, and that can be verified by other computers.
The necessary computer program is included
and will be discussed in detail in the following sections.
We conclude this introduction with some remarks
concerning our choice of programming language, etc.
Other computer--assisted proofs and an extensive list of
papers on interval methods can be found in the references
[C, CC, EKW1\... EKW2, EW1\... EW2, FS, FL, KP, KW1\... KW7, La1\... La4,
Lla, LLo, LR1\... LR3, M, MM, Ra, Se1\... Se2, St] and [XSC], respectively.

Unfortunately, computer--assisted proofs are usually very hard to read.
The computer programs tend to be
lengthy, even for relatively simple problems,
and it is often tedious
to verify that mathematical expressions
are correctly represented by their programmed versions.
This is because the syntax of traditional programming
languages like ADA, Basic, C, C++, Fortran, Modula2, Pascal etc.
is quite different from the syntax that mathematicians are used to,
and because in these programming languages,
memory allocation,
control structures and the like
make up most of the programs.
As a consequence, the
simplicity of the ideas underlying
computer--assisted proofs is often
lost along the way.

There have been attempts to improve this situation, e.g.
by adding syntactic features to a language like Pascal [EMO, XSC].
In this paper we propose to use
the programming language
Prolog ({\bf Pro}gramming in {\bf log}ic).
Prolog allows for a syntax
close to the one that mathematicians are used to. In addition,
Prolog does not require writing
code for memory allocation etc.

Most computer--assisted proofs in analysis rely on the contraction mapping
principle for proving the existence of solutions to equations in Banach
spaces, i.e., equations are written in the form of a fixed point problem
for an appropriate operator $\RR.$
This requires, among other things, an estimate on the norm
of the (Fr\'echet) derivative of $\RR.$
Traditionally, a considerable fraction of the program is taken up
by the parts devoted to such estimates.
With Prolog, however,
it becomes natural to have the program generate these parts,
by applying the chain rule of differentiation to the operator $\RR$,
which is usually composed of several ``building blocks.''

Prolog has been in use for many years now.
In spite of that, it did not gain much
popularity outside the Artificial Intelligence community,
mainly because, until not too long ago, efficient implementations
of the language were sparse and
did not offer reasonable support for floating point arithmetic.
More recently, good implementations
which do support decent floating point arithmetic
have become widely available, so that the interested reader
should be able to find
a Prolog system which can be used to verify our proof.

In this paper we use Prolog
for all the advantages it offers for our type of application.
We do not claim in any way that
Prolog is the ``perfect programming language.'' Indeed, Prolog is
in many respects far from being perfect, and
has, like any other language, its strong and its weak
points. We do feel, however, that
the main ideas which lead to the development of
Prolog will play a role in the
future of programming, and we would like to
bring some of these ideas to the reader's attention.

This paper has been prepared by using the
\TeX$\!$ text processing system.
Those readers who have the corresponding .tex file
can run it through the \TeX compiler.
This will produce, along with
the usual .dvi file, a file named proof.pl containing the
extraction of the Prolog lines which make up the main part of our proof.

%==============================================================================
% PRO.53D
\section Prolog

At the time of this writing
there exists no official standard for Prolog.
Many of the better implementation, however,
adhere to
a {\it de facto} standard, known under the name of
Edinburgh Prolog, which is described e.g. in [CM].
Most implementations also offer some additional features
that go beyond the Edinburgh ``standard''.
For reasons of compatibility,
we chose
not to use such features here,
with one exception:
we use floating point arithmetic,
and we require that it be implemented as
64 bit arithmetic according to the IEEE standard,
which will be described in Section 3.

There is one part of the Prolog syntax, the operator notation
(see Subsection 2.2),
that is not entirely standardized
within Edinburgh Prolog.
A consequence which is relevant here
is that the so called precedence
classes (certain positive integers) of predefined operators
may vary from one implementation to the next.
Thus, some readers may have to modify the program
in order to get it to behave as intended on their Prolog systems.
The necessary changes are minor and are described below.

We note that these issues can be ignored by the reader
who is willing to believe that we actually ran our program
once with positive outcome.
In this case, it suffices to verify the correctness of the program
in order to check the proof.
Everything that is needed for this step ---
the program and a description of the Prolog syntax that was used to write it
--- is provided in this paper.

Our program was developed, for the most part, by using LPA--Prolog [LPA].
It was run with LPA--Prolog on a ``80486'' personal computer,
and with SICStus Prolog [SP] on various Unix workstations.
The running time was between 5 and 30 minutes,
depending on the system used.

We continue this section with an introduction to Prolog.
No additional knowledge of programming,
beyond what is presented below,
will be necessary to follow the rest of this paper.
Should the reader prefer to learn about Prolog first from another source,
the classic textbook [CM] is still a very good starting point.
Possible continuations include the textbook [SS],
or the book [Ro] which also gives a rather extensive list
of Prolog implementations and references for further reading.
In what follows, items related to Prolog will be highlighted
using \p$this_special_font\l$.

\subsection The Syntax of Prolog Terms

In Prolog, a program consists of data,
and there is a single data structure, the term.
In order to define its syntax,
we introduce the notion of atoms, variables, and numbers:

$i)$ An atom is one of the following four: $(1)$ a finite sequence of
alphanumeric or underscore characters, i.e.,
characters chosen from
\pro
 a b c d e f g h i j k l m n o p q r s t u v w x y z

 A B C D E F G H I J K L M N O P Q R S T U V W X Y Z

 0 1 2 3 4 5 6 7 8 9 0 _
\logc
starting with a lower case letter;
$(2)$ any finite sequence of characters chosen from
\pro
 +  -  *  /  .  ~  ?  :  <  >  =  \^  @  \#  \$  \&
\logc
$(3)$ the exclamation mark, the semicolon, or the pair of square
brackets, i.e.,
\pro
 !  ;   []
\logc
$(4)$ an ``arbitrary'' sequence of ``arbitrary'' characters in single quotes.
We shall not specify here the meanings of ``arbitrary.''
In what follows, the only (important)
instance of this case will be the atom \p$','.\l$
\smallskip

$ii)$ A variable is a finite sequence of
alphanumeric or underscore characters,
starting with an upper case letter or an underscore.
Variables starting with an underscore are called anonymous.
\smallskip

$iii)$ A number is any sufficiently small nonnegative integer,
written in base ten ``everyday notation,'' using numeric characters.
The meaning
of ``sufficiently small'' depends on the Prolog implementation
and typically stands for ``smaller than $2^{31}.$''

As mentioned in the introduction,
our proof requires a Prolog implementation that provides
64bit IEEE floating point
arithmetic. Most Prologs that provide such numbers also
allow to use ``them'' as syntactic elements. Since we have no need for
using such numbers on a syntactic level,
we stick, as far as the syntax is concerned, with the Edinburgh definition.

Prolog terms are now defined inductively as follows.
A Prolog term comprises a functor and zero, one, or more arguments.
The arguments, if there are any, can be
either variables, numbers, or again Prolog terms.
A functor is characterized by its name (an atom)
and its arity (the number of arguments).
We will refer to a functor with name \p$funtor_name\l$ and arity \t{N}
by using the customary symbol \p$functor_name/N\l$.

The standard syntax for a prolog term
with functor \p$functor_name/N\l$,
in the cases $\t{N}=0,1,2,$ \... is
(the etc.\--dots \... are not to be confused with the Prolog atom
\t{...})
\pro
functor_name
functor_name(First_argument)
functor_name(First_argument, Second_argument)
functor_name(First_argument, Second_argument, \..., Last_argument)
\logc
Here, \p$functor_name\l$ stands for any legal Prolog atom.
Arguments have to be separated by commas, but space characters can
be added before and after each argument to enhance readability.
No white space is allowed between the atom
\p$functor_name\l$ and the opening bracket.

\subsection The Operator Syntax for Prolog Terms

One fact about Prolog that is of practical importance
is that it provides
an alternative syntax for
terms with one or two arguments: such terms
can be written in operator notation.
The functor becomes an operator, and, depending on whether this operator
is declared as
postfix (type \p$xf\l$ or \p$yf\l$),
prefix (type \p$fx\l$ or \p$fy\l$),
or infix (type \p$xfx\l${,} \p$yfx\l${,} \p$xfy\l${,} or \p$yfy\l$),
its name is written after the argument, before the argument,
or between the first and the second argument.

Many operators are already known to standard Prolog.
The following is a complete list of all those predeclared operators
which are used in this paper.
Each entry has the form of a declaration \t{op(P,Type,Name)},
specifying the precedence class, the type,
and the name of the operator.
\pro
op(1200,fx,:-)
op(1200,xfx,:-)
op(1000,xfy,',')
op( 700,xfx,=)
op( 700,xfx,=..)
op( 700,xfx,is)
op( 700,xfx,<)
op( 700,xfx,>)
op( 700,xfx,=<)
op( 700,xfx,>=)
op( 500,yfx,+)
op( 500,yfx,-)
op( 500,fx ,-)
op( 400,yfx,*)
op( 400,yfx,/)
\logc
The precedence classes specify how
a term like
\pro
2+3*4
\logc
has to be interpreted. According to the declarations listed above,
it has to be read as \p$+(2,*(3,4)).\l$
The type \p$yfx\l$ indicates that the operator is
left associative, which means e.g. that
\pro
2/3*4
\logc
is equivalent to \p${*(/(2,3),4)}\l$ and not to \p${/(2,*(3,4)).}\l$
The operator notation of the last term is
\pro
2/ (3*4)
\logc
i.e., we can always use parentheses to overrule the given
associativity rules or operator precedence.
The space between the operator name \t{/} and
the opening parentheses is necessary here
(in contrast to the standard syntax for terms)
in order to avoid possible ambiguities.
Thus, we shall always put such spaces, even though most
Prolog compilers do not insist on that.
Parentheses can also be used redundantly
(as we often do in our program)
to encapsulate arguments for better readability, e.g.,
\t{2/3*4} may be written as \t{(2/3)*4}.

More generally, a letter \p$x\l$ or \p$y\l$ in the \p$Type\l$
of an operator \p$given/N\l$ specifies what kind of argument
can be used at the corresponding position in a term with this operator.
Restrictions apply (only) if the argument is also a term
written in operator notation, without enclosing parentheses.
In this case, an \p$x\l$ indicates that the precedence class of the
argument--operator has to be lower (a smaller integer)
than that of \p$given/N\l$. A \p$y\l$ is less restrictive
and allows the two precedence classes to be equal as well.

We note that the only purpose of precedence classes
is to define an order among (classes of) operators,
i.e., the absolute size of these numbers is of no importance.
For this reason, the precedence class values of predefined
operators vary, unfortunately,
from one implementation of Prolog to another
(though usually not their ordering).
Thus, the reader who wishes to run our program
should compare the precedence class of predefined operators with
the ones listed above .
In case the values do not all agree, some
of the lines in the program part presented in Subsection 2.8
below may have to be adapted accordingly.

We shall not present the syntax rules for general
expressions involving operators in any more detail.
The reader is warned, however, that
without such specifications (which are missing in
most dialects of Prolog)
general expressions
involving operators can be ambiguous.
We avoid this problem by using only operator expressions
which can be translated to the original Prolog syntax
by applying just
the associativity rules and precedence class rules explained above.



\subsection The List Notation

Prolog offers, besides the operator notation,
additional ``syntactic sugar''
for certain terms with the functor \p$./2\l$. Namely, terms of
the form
\pro
.(Term, Again)
\logc
where \p$Term\l$ is an arbitrary Prolog term, and where
\p$Again\l$ is either the atom \p$[]\l$ or of the form
\p$ .(Term, Again)\l${,}
can be written in list notation.
For example
\pro
[1,2,3]
\logc
is just a simpler way of writing
\pro
.(1, .(2, .(3,[])))
\logc
and general lists are defined analogously.
In this context the atom \p$[]\l$ is called the empty list.
Another piece of notation, which defines
\p$[X|T]\l$ to be the same as \p$ .(X,T)\l${,}
provides a convenient way of adding a term at the beginning of a list.
In particular, if \p$T\l$ stands for the list \p$[Y,Z]\l$
then \p$[X|T]\l$ is identical to \p$[X,Y,Z]\l${.}
There is an analogous way of prepending two or more terms to a list.
For example, \p$[X,Y|T]\l$ is defined as \p$ .(X,.(Y,T))\l${,}
which implies e.g. that
\p$[1,2|[3,4]]\l$ is the same as \p$[1,2,3,4]\l${.}
We note that
\p$[a]\l$ is equivalent  to
\p$[a|[]]\l${,} but not to
\p$[a,[]].\l$ The latter is a list with two elements;
it is syntactically equivalent to
\p$.(a, .([],[]))\l$.

\subsection The Syntax of Prolog Programs

Syntactically,
a Prolog program is a sequence of Prolog terms, each followed by a
full stop and a line feed character.
(Most versions of Prolog will allow
``layout'' characters different from line feed.)
Such a term in a program is called a clause.
If the functor of a clause
is the infix operator \p$:-/2\l${,}
then we call the clause a non unit clause.
Otherwise, it will be called a unit clause,
unless its functor is the prefix operator \t{:-/1},
in which case it is called a headless clause.
There are restrictions
(which have been partly eliminated in some newer Prolog dialects)
on the type of terms
that can be used as clauses.
In particular,
the first argument of \t{:-/2} in a non unit clause has to be a term,
i.e., it cannot be a variable or a number,
and the functor of this term is not allowed to be one of the operators
\p$:-/1\l${,} \p$:-/2\l${,} and \t{','/2}{.}
The following is a Prolog program:
\pro
head.
head :- body.
\logc
It consists of a unit clause and a non unit clause.
The first argument of \p$:-/2\l$ in a non unit clause
is called the
head of the clause, and the second argument is called the body.
Unit clauses have a head only.

Given a program,
we define a predicate to be the set
of all clauses whose heads have the same functor,
and we (mis)use this functor
to refer to the corresponding predicate.
Thus, the above example program defines one predicate: \p$head/0.\l$

Below we will see that the operator \t{','/2} has a special
meaning in non unit clauses of the form
\p$A :- B0 ',' B1 ',' \... \l$
and in headless clauses of the form
\p$:- B0 ',' B1 ',' \... \l$.
For better readability, Prolog
allows for the quotes to be suppressed in these cases, i.e.,
one can simply write
\p$A :- B0,B1,\... \l$ and
\p$:- B0,B1,\... \l${.}

\subsection Matching Terms

Assume that \t{T1} is some Prolog term that does not contain any
variables. A term \t{T2} is said to match
\t{T1} if it is the same term, or
if it contains variables that can be chosen
(by instantiating them to numbers or to
Prolog terms not containing variables)
in such a way that it becomes the same term.

According to this rule,
the term \t{i(1,2)} is matched by \t{i(1,2)} and \t{i(X,Y)},
but not by \t{i(0,1)}.
The term \t{i(X,X)} does not match the term
\t{i(1,2)}, since there is no choice of the variable
\t{X} which makes the two terms identical.
On the other hand, the term \p$i(_,_)\l$ does match the term
\t{i(1,2)}, since every anonymous variable
is defined to be independent of any other variable.

The matching relation is symmetric. That is,
if \t{T2} matches \t{T1} then \t{T1} matches \t{T2}.
In general, matching is defined recursively as follows:
\medskip
\item{i)}
If \t{X} is an uninstantiated variable and
\t{T} is instantiated to
a term or a (representable) number, then
\t{X} matches \t{T} and \t{X} becomes instantiated to
whatever \t{T} is.
If \t{X} and \t{Y} are both uninstantiated variables then
\t{X} matches \t{Y}, and \t{X} and \t{Y} become synonyms for the same
(uninstantiated) variable.
An anonymous variable matches anything (that is syntactically correct).

\item{ii)}
Two Prolog terms match if they have the same functor name
and the same number of arguments,
and if corresponding arguments match.

\medskip\noindent
For example,
the term \t{f(X,i(1,Y))} matches the term \t{f(Y,i(X,1))} but not
\t{f(Y,i(X,2))}.
Also, according to the above definition, \t{X} matches \t{f(X)},
but \t{i(1,X)} does not match \t{i(X,f(X))}.

\subsection Program Execution

In this section we give an informal account of
how a Prolog program is ``executed.''
As explained earlier, the intention is
not to give a complete description of Prolog,
but only to provide enough information so that the reader
can check the correctness of our program.

Prolog, as a programming system, is not just the language
whose syntax we have introduced
above, but it is this language together with an
``inference engine'' that does some sort of reasoning,
as will now be described.
There is a way of making Prolog look at a file
(in our case the file proof.pl)
that contains a program.
How this is done precisely is of no importance
for the moment.
It suffices to know that Prolog starts to look at such a file
from the top.
In particular, since the various parts of our program
will be presented in the order they appear in the file proof.pl,
we can imagine Prolog to be watching over our shoulders
and reading along, as we go over each of these parts.
If Prolog encounters a unit clause or a non unit clause,
it does nothing except ``memorizing'' the clause by adding it to
the bottom of some (internal) list, also called the database.

The idea is that Prolog acquires knowledge by adding clauses to its
database.
Roughly speaking, a unit clause \t{H} declares a fact ``\t{H} is true'',
and a non unit clause \p$H:-B\l$ is a rule
``\t{H} is true if \t{B} is true'' that can be used to infer new facts
from facts that are already known. Such an inference is started
when Prolog encounters a headless clause.

A headless clause \p$:-G\l$
is interpreted as an instruction to ``satisfy \t{G}''.
In this context, \t{G} is also called a goal.
When Prolog encounters such a headless clause,
it tries to satisfy \t{G} (in a way to be explained)
by using the clauses that are already in the database.
If this is impossible, Prolog
stops and communicates to the user some sort of error message.
Otherwise,
Prolog continues reading the program until it reaches the
next headless clause, or until it arrives at the end of the
file containing the program, in which case it also stops and communicates
to the user that it has been successfully building up a database.
(If required one can then ask Prolog to look at another file
containing more clauses, etc.)

We now explain how Prolog tries to satisfy a goal \t{G}.
First, we note that there are two possible outcomes:
either \t{G} is satisfied, or else it fails.
A satisfied goal is interpreted as a true statement.
By contrast,
a failed goal should not be interpreted as a false statement,
but rather as a statement whose truth value is not determined
by the facts and rules contained in the database.

Assume now that \t{G} is a goal whose functor is not \t{','/2}.
In its attempt to satisfy this goal,
Prolog starts at the beginning of the database
and checks, one clause after another,
whether or not \t{G} matches the head of the clause
(in the sense explained in Subjection 2.5).
If Prolog finds a unit clause \t{H} that
matches \t{G}, then the goal \t{G} is satisfied.
Alternatively, if Prolog gets to a non unit clause \p$H:-B\l$
whose head \t{H} matches \t{G},
then it tries to satisfy the goal \t{B}
(possibly with some of its
variables being instantiated through the matching with \t{H}),
and if \t{B} becomes true then so does \t{G}.
To satisfy \t{B}, Prolog proceeds recursively.
In particular, if the functor of \t{B} is not \t{','/2},
then the database is searched (again from the top)
for a clause whose head matches \t{B}, etc.
If \t{B} fails, then Prolog backtracks and
tries to satisfy \t{G} in a different way,
by continuing its search of the database
with the clauses following \p$H:-B\l${,}
in the same state as it would have been
in the case where \t{G} did not match \t{H}.
Should Prolog arrive at the end of the database,
with all clauses checked and none of them satisfying \t{G},
then the goal \t{G} fails.

We note that by matching the goal \t{G} with the head of
a clause \t{C} in the database, Prolog makes a choice:
\t{C} becomes the first clause used
in the current attempt to prove (satisfy) \t{G}.
Before making this choice, Prolog saves all the information
needed to be able to backtrack to the same pre--choice state.
Prolog will backtrack to this state later
if no proof of \t{G} can be found that starts with \t{C},
or if such a proof was found but an alternative proof is needed.
In both of these cases, Prolog tries to satisfy \t{G} in a different way,
by continuing its search of the database
with the clauses following \t{C}. From this point on,
the above--mentioned pre--choice state is no longer available
for backtracking, since both choices (using \t{C}, or skipping \t{C})
have already been tried.

Consider now the case where the goal is of the form \t{G1','G2}.
The operator \t{','/2} corresponds to the logical ``and''.
But as a goal, \t{G1','G2} should be read as ``\t{G1} and then \t{G2}''.
Thus, in order to satisfy \t{G1','G2},
Prolog has to satisfy first \t{G1} and then \t{G2}.
Assume now that \t{G1} was found to be true.
The next step is to satisfy the goal \t{G2}.
Here, it is important to note that some variables in \t{G2}
may be instantiated as a result of matches from previous steps.
Thus, if \t{G2} fails at this point, then Prolog will
consider alternative ways of satisfying \t{G1},
by backtracking to the most recently saved state available
and proceeding as described above.
Each time Prolog finds a new proof for \t{G1},
it tries again to satisfy \t{G2},
and if this succeeds then \t{G1','G2} is true.
The goal \t{G1','G2} will fail only if \t{G1} fails,
or if \t{G2} fails after each proof of \t{G1}.


\subsection  Built--in Predicates.

Besides predeclared operators, Prolog also includes a set of
predefined predicates.
The following is a complete list of all built--in predicated
that are used in our program:
\pro
=/2
=../2
is/2
>/2
</2
=</2
>=/2
asserta/1
op/3
write/1
nl/0
!/0
\logc
We note that the list in Subsection 2.2 contains
some additional operators that are not mentioned here.
Those operators have a special meaning only on a syntactic level.

Some built--in predicates are provided for convenience only
(\t{=/2} is of this type),
i.e., they could also be defined by the user.
The others
are not predicates in the sense
defined in Subsection 2.4.
Some of them behave
just like ordinary predicates, from the point of view of program
execution, but include features
that the user could not implement
(\t{=../2} is of this type), or
not implement easily
(\t{is/2}, \t{</2}, \t{>/2}, \t{=</2} and \t{>=/2}
are of this type). Still others
(like \t{asserta/1}, \t{op/3}, \t{write/1}, \t{nl/0} and \t{!/0})
make goals that are
always satisfied, but that have side--effects.
We now explain the semantics of each of these predicates.
\smallskip\noindent
\t{=/2} behaves as if defined as \t{X=X}, i.e., it simply matches two terms.
\smallskip\noindent
\t{=../2} allows one to decompose
a given term \t{T} into its functor and its arguments.
If \t{L} is an uninstantiated variable and
\t{T} is instantiated to \p$functor_name(Arg1, Arg2, \...)\l$,
then \t{T =..L} is satisfied and \t{L} gets instantiated to the
Prolog list \p$[functor_name, Arg1, Arg2, \...]\l$.
\smallskip\noindent
\t{is/2} evaluates arithmetic expressions.
If \t{X} is an uninstantiated variable,
and if \t{T} is a number (or representable number, see Section 3)
or a Prolog term whose functor is
one of the basic arithmetic operators
(unary minus, addition, subtraction, multiplication, and division)
and whose arguments are (variables instantiated to)
either numbers or again terms of the same form,
then \t{X is T} is satisfied, and \t{X} gets instantiated to the
(approximate, in the sense of Section 3) evaluation of the
arithmetic expression \t{T}.
\smallskip\noindent
\t{X > Y} is satisfied if the variables \t{X} and \t{Y} are
instantiated to numbers
(any representable number in the sense of Section 3 is allowed here),
and if \t{X} is greater than \t{Y}.
The situation is analogous for goals with
the predicates \t{</2}, \t{>=/2} and \t{=</2}, which implement
the order relations ``less than'',
``greater than or equal'', and ``less than or equal'', respectively.
\smallskip\noindent
\t{asserta(T)} is satisfied if \t{T} is a Prolog term that
can be interpreted as a clause. This clause is then added
at the beginning of the Prolog database.
\smallskip\noindent
\t{op(P,Type,Name)} is satisfied if \t{P} is a positive integer less than
the precedence class of \p$:-/1\l$ and \p$:-/2\l${,}
if \t{Type} is one of the atoms
\t{xf}, \t{yf}, \t{fx}, \t{fy}, \t{xfx}, \t{xfy}, \t{yfx} or \t{yfy},
and if \t{Name} is any atom (except for names of
predefined operators). As a side--effect, the Prolog syntax is changed:
the atom \t{Name} is considered to be the name
of an operator with precedence class
\t{P} and of associativity type \t{Type},
as explained in Subsection 2.2.
\smallskip\noindent
\t{write(A)} is satisfied if \t{A} is an atom. As a side--effect,
\t{A} is written to the current output stream (e.g. the terminal).
\smallskip\noindent
\t{nl} is always satisfied, and it has the side--effect
of writing a newline character to the current output stream.
\smallskip\noindent
\t{!} (read ``cut'') always succeeds, and as a side--effect,
it commits Prolog to all the choices made since the parent goal
was unified with the head of the clause containing the cut.
Our programs uses cuts only to help the Prolog system
economize memory usage; it runs correctly even if all cuts are removed.
Thus, when reading our program, the reader can safely ignore the cuts.
(See [CM, R, SS] for an introduction to the
cut predicate and [Llo] for a possibility of defining its semantics.)


\subsection Syntax Used in the Proof

Any line that is highlighted in \p$this_special_font\l$
and appears in ``display style'', i.e.
\pro
like_this
\logc
is part of our program from now on.
To begin with, we declare a few operators which will allow
us to write the rest of the program in a
syntax that is close to the familiar notation of mathematics:
\pro
\prolog{:-op(700,xfx,is_a_safe_upper_bound_on).}
\prolog{:-op(700,xfx,is_a_safe_lower_bound_on).}
\prolog{:-op(700,xfx,enlarges).}
\prolog{:-op(700,xfx,contains).}
\prolog{:-op(700,xfx,approximates).}
\prolog{:-op(700,xfx,lt).}
\prolog{:-op(600,xfy,of).}
\prolog{:-op(500,xfx,at).}
\prolog{:-op(300,yfx,o).}
\prolog{:-op(200,xf,inverse).}
\prolog{:-op(200,xfx,**).}
\log
Later on, we will define predicates associated with
the first six operators declared in this list. The operators
\t{at/2}{,}
\t{of/2}{,}
\t{o/2}{,}
\t{inverse/1}{,} and
\t{**/2}{,}
are used for syntactic convenience only.




%==============================================================================
% IEEE.55a
\section 64bit IEEE Arithmetic and Rounding

The 64bit IEEE standard for floating point arithmetic
[IEEE] specifies two things:
a format for floating point numbers, and
rules concerning rounding after the operations
$+,$ $-,$ $*$ and $/$.

Unfortunately, the IEEE standard comes in several flavors.
In the present context, this means that the semantics
of the predicate \t{is/2} may differ from one Prolog system
to the next, even if both comply with ``the'' IEEE standard.
In our program we avoid this problem by restricting \t{is/2}
to a domain where all versions of the standard agree.

In 64bit IEEE arithmetic, a number is represented with 64 bits
of memory: 1 bit for the sign of the number, 11 bits for an exponent,
and 52 bits for a significand.
There is a convention which identifies the state of a bit
with the integers zero and one, e.g.,
any given state of the 11 exponent bits
determines, via the base 2 representation for nonnegative integers,
an integer $e$ in the range $0\le e\le 2047$.
A real number $r$ is now associated with any bit pattern of 64 bits
for which $0<e<2047$, and $r$ is defined by the equation
$$
r=\pm 1.m\ 2^{e-({2^{10}-1})},
\equation(88)
$$
where $+$ or $-$ is chosen according to whether the sign bit is zero or one,
and where $m$ is a base 2 significand given by the sequence
of zeros and ones associated with the 52 significand bits.
In addition, the bit pattern consisting of 64 zeros
is used to represent $r=0$.

\claim Definition(8888) A real number $r$ is called representable
if it is either zero, or if it can be written in the form \equ(88),
subject to the above--mentioned restrictions on $e$ and $m$.
The set of all representable numbers will be denoted by $\RR$.


\noindent {\bf Remark.} On many systems, integers between $-2^{31}$
and $2^{31}-1$ are represented in the ``32bit two's complement format'',
and not in the 64bit IEEE floating point format.
However, since all
these integers are representable numbers, too,
and since 64bit IEEE arithmetic computes without rounding errors with
these integers,
there will be no need for distinguishing
the two internal representations, and we will not make any mention of it
anymore.

\medskip
We note that the smallest and largest positive representable numbers are
$2^{-1022}\approx 2.2\cdot10^{-308}$ and
$(2-2^{-52})\cdot 2^{1023}=$
$(1-2^{-53})\cdot 2^{1024}\approx 1.8\cdot10^{308}$, respectively.
Other ``interesting'' numbers are
the smallest representable number larger than one,
$1+2^{-52},$
and the next nearest neighbor in $\RR$ to the left of one,
$1-2^{-52}.$

In what follows, a number described by the 64bit IEEE standard
will be referred to as ``IEEE number''.
This includes not only what we call here representable numbers,
but (among others) also some additional numbers between $\pm 2^{-1022}$,
associated with bit patterns for which $e=0$.

Besides defining a number format, the IEEE standard also
specifies the precision to which arithmetic computations
have to be carried out.
Let $r_1$ and $r_2$ be two arbitrary IEEE numbers,
and let $\#$ be any of $+,$ $-,$ $*,$ or $/.$
If $r_1\#r_2$ is not an IEEE number,
but not larger or smaller than every IEEE number (case of an overflow),
then the approximate result computed for $r_1\#r_2$ is guaranteed to be
either the largest IEEE number smaller than $r_1\#r_2$,
or the smallest IEEE number larger than $r_1\#r_2$.
If $r_1\#r_2$ is an IEEE number,
then the IEEE standard prescribes that the
computed result for $r_1\#r_2$ be exact.
In particular, the computed result is exact
if either $r_1=0$, or if $r_2=0$ and $\#$ is not division.
Also, if we avoid overflow or underflow (see below),
then multiplication and division
of a representable number by two
are always carried out exactly, since,
in terms of the representation \equ(88),
this just corresponds to increasing or decreasing $e$ by one.
The IEEE standard also requires that the tests
$r_1=r_2,$ $r_1<r_2,$ $r_1>r_2,$ $r_1\le r_2,$ and $r_1\ge r_2$
be implemented correctly.

One of the problems of floating point arithmetic, besides overflow,
is the so called ``silent underflow to zero.''
For example, if $r$ is a sufficiently small positive IEEE number,
then a computer conforming with the IEEE standard
can approximate $r*r$ by zero.
This behavior is usually not considered a problem,
and typically no execution error is raised
(whence the expression silent underflow).
But there are cases where it is important to know
whether the result of an arithmetic operation is really zero
or just very close to zero.
Below, we will restrict our usage of IEEE numbers
to a subset for which neither underflow nor overflow can occur.

For convenience later on,
we define now two predicates,
\p$negative_power_of_two/2\l$ and
\p$positive_power_of_two/2\l$,
for computing integer powers of two within the representable range.
We start with the case of negative powers.
The desired effect is that if \t{N} is a given integer,
then \p$negative_power_of_two(X,N)\l$ becomes true as a goal
if and only if $0\le\t{N}\le 1022$
and $\t{X}=2^\t{-N}.$
Our definition of \p$negative_power_of_two/2\l$
starts with the true statement
$\t{1}=2^\t{0},$
\pro
\prolog{negative_power_of_two(1,0):-}
\prolog{ !.}
\log
The other cases are covered recursively by the clause
\pro
\prolog{negative_power_of_two(X,N):-}
\prolog{ N>0,}
\prolog{ N=<1022,}
\prolog{ M is N-1,}
\prolog{ negative_power_of_two(Y,M),}
\prolog{ X is Y/2,}
\prolog{ !.}
\log
where we first check that \t{N}
is within the allowed range, then compute
$2^\t{-(N-1)},$ and then divide the result by two.
The predicate \p$positive_powers_of_two\l$ can now be defined
by using the fact that $2^\t{N}=1/2^\t{-N}$,
\pro
\prolog{positive_power_of_two(X,N):-}
\prolog{ negative_power_of_two(Y,N),}
\prolog{ X is 1/Y,}
\prolog{ !.}
\log

In order to avoid any kind of difficulties related to underflow and overflow,
and to make our program compatible
with every version of the 64bit IEEE standard,
we will check explicitly that arithmetic operations
are carried out within a (somewhat arbitrary) ``safe range''.

\claim Definition(ssss) We define the safe range $\SS$ to be the set
$$
\SS=\bigl\{r\in\RR|\
2^{-500}<|r|<2^{500}\bigr\}\cup\{0\},
\equation(ss)
$$
where $\RR$ is the set of representable numbers defined above.

%------------------------ Fig.1---------------------------------------
\vskip 0.5truecm
\figurewithtex s_range.ps s_range.tex 3 14 Positive representable numbers and
positive part of safe range\cr
\vskip 0.0truecm
%------------------------ Fig.1---------------------------------------
In Prolog we define the positive (part of the) safe range with
a predicate that makes \p$lower_bound_on_positive_safe_range(X)\l$
true if and only if \t{X} is $2^{-500}$, and
a predicate that makes \p$upper_bound_on_positive_safe_range(X)\l$
true if and only if \t{X} is $2^{500}.$
In order to avoid having to compute $2^{\pm 500}$ each time
one of these predicates is used,
we will define them in the form \p$:-B,asserta(H)\l$
instead of \p$H:-B\l$.
This is done as follows:
\pro
\prolog{:- negative_power_of_two(X,500),}
\prolog{   asserta(lower_bound_on_positive_safe_range(X)).}
\log
We note that this is the first place where Prolog
encounters a headless clause.
Prolog starts by trying to satisfy the goal
\p$negative_power_of_two(X,500)\l${.}
This succeeds, while \t{X} is being instantiated to $2^{-500}.$
Then the clause \p$lower_bound_on_positive_safe_range(X)\l$,
where \t{X} is now equal to $2^{-500},$
is prepended to the internal database.
This defines a predicate \p$lower_bound_on_positive_safe_range/1\l$.
Similarly,
\pro
\prolog{:- positive_power_of_two(X,500),}
\prolog{   asserta(upper_bound_on_positive_safe_range(X)).}
\log

In what follows, $r_1$ and $r_2$
denote fixed but arbitrary numbers in the safe range,
except in a division $r_1/r_2$, where we exclude $r_2=0$.
In addition, a ``computation'' will always refer to
a computation carried out by
a given but arbitrary system that conforms to the 64bit IEEE standard.
These restrictions guarantee e.g. that no underflow or overflow occurs
in the computation of $r_1\#r_2$,
and that the result always has the correct sign (plus, minus, or zero).

Assume now that $r_1\#r_2$ is nonzero.
Then the computation of $r=r_1\#r_2$ yields
a nonzero representable number $r_c$ which is
not necessarily in the safe range,
but which can still be multiplied by $u=1+2^{-52}$ and $d=1-2^{-52},$
without causing underflow or overflow.
Let $r^>_c$ and $r^<_c$ be the
representable numbers obtained from a computation
of the product $r^>=r_c*x$ and $r^<=r_c*y,$ respectively,
where $(x,y)=(u,d)$ if $r_c$ is positive,
and $(x,y)=(d,u)$ if $r_c$ is negative.
By using the IEEE specifications given above,
it is easy to verify that
$r_c^<$ is either the nearest or next nearest neighbor
in $\RR$ to the left of $r_c,$
and that
$r_c^>$ is either the nearest or next nearest neighbor
in $\RR$ to the right of $r_c.$
As a result, we have $r_c^< < r < r_c^>.$

\claim Definition(foo) Given a representable number $x$,
we say that a representable number $t$ is a safe upper bound on $x$
if either $t=x=0$, or if there exists a number $s\in\SS$,
with the same sign as $x$, such that $x<t\le s$;
and we say that $t$ is a safe lower bound on $x$
if either $t=x=0$, or if there exists a number $s\in\SS$,
with the same sign as $x$, such that $s\le t<x$.

Below, whenever we compute $r_c^<$ and $r_c^>$,
we will also verify that these numbers are
safe lower and upper bounds, respectively, on the number $r_c$.
These two properties together imply that both $r_c^<$ and $r_c^>$
are in the safe range.

This shows that (and how)
it is possible to compute bounds on the result of an arithmetic
operation using IEEE floating point arithmetic.
In order to implement these ideas in Prolog,
we first define two
predicates \p$up/1\l$ and \p$down/1\l${,}
such that \p$up(Up)\l$ is true for
{\p$Up\l$}$=1+2^{-52},$
\pro
\prolog{:- negative_power_of_two(X,52),}
\prolog{   Up is 1+X,}
\prolog{   asserta(up(Up)).}
\log
and \p$down(Down)\l$ is true with
{\p$Down\l$}$=1-2^{-52},$
\pro
\prolog{:- negative_power_of_two(X,52),}
\prolog{   Down is 1-X,}
\prolog{   asserta(down(Down)).}
\log
Let now $r_c=\t{Y1}$ be a nonzero representable number
obtained from a computation of $r=r_1\#r_2$
with $r_1$ and $r_2$ in the safe range.
Then the upper bound $r_c^>$ on $r$, which was described above,
can be computed by using the following predicate
which makes \p$Y2 is_a_safe_upper_bound_on Y1\l$ true
if \t{Y2} is equal to $r_c^>$ and a safe upper bound on \t{Y1}.
The case of positive \t{Y1} is covered by the clause
\pro
\prolog{Y2 is_a_safe_upper_bound_on Y1:-}
\prolog{ Y1>0,}
\prolog{ up(Up),}
\prolog{ Y2 is Up*Y1,}
\prolog{ upper_bound_on_positive_safe_range(U),}
\prolog{ Y2<U,}
\prolog{ !.}
\log
and the following applies if \t{Y1} is negative:
\pro
\prolog{Y2 is_a_safe_upper_bound_on Y1:-}
\prolog{ Y1<0,}
\prolog{ down(Down),}
\prolog{ Y2 is Down*Y1,}
\prolog{ lower_bound_on_positive_safe_range(L),}
\prolog{ Lm is -L,}
\prolog{ Y2<Lm,}
\prolog{ !.}
\log
According to the \clm(ssss) we also have to add a clause like
\pro
\prolog{Z is_a_safe_upper_bound_on Z:-}
\prolog{ Z>=0,}
\prolog{ Z=<0,}
\prolog{ !.}
\log
Similarly, the predicate
\p$is_a_safe_lower_bound_on/2\l$
is used to compute the number $r_c^<$
and to perform the indicated check.
It can be expressed easily in terms of the predicate
\p$is_a_safe_upper_bound_on/2\l$ as follows:
\pro
\prolog{X2 is_a_safe_lower_bound_on X1:-}
\prolog{ Y1 is -X1,}
\prolog{ Y2 is_a_safe_upper_bound_on Y1,}
\prolog{ X2 is -Y2,}
\prolog{ !.}
\log


%==============================================================================
% INT.55g
\section Interval Analysis

In this section we will describe in general terms
the type of bounds that are used in computer--assisted proofs.
The description is independent of the other parts of the paper,
but not vice versa: we will refer to this section
for the definition of a ``bound on a map''
and for the notion of ``standard sets''.

Given any set $\Sigma$, denote by $\PP(\Sigma)$
the set of all subsets of $\Sigma$.
Let now $\Sigma$ and $\Sigma^\prime$ be two sets,
and let $f$ and $g$ be maps from
$\DD_f\subseteq\PP(\Sigma)$ and $\DD_g\subseteq\PP(\Sigma)$,
respectively, to $\PP(\Sigma^\prime)$.

\claim Definition(331) We say that $g$ is a bound on $f$,
in symbols $g\ge f$,
if $\DD_f\supseteq \DD_g,$ and if $f(S)\subseteq g(S)$ for all $S\in\DD_g\,$.

Bounds of this type have some general properties which make it
possible to estimate complicated maps in terms of simpler ones,
and to ``mechanize'' such estimates. In particular, if
$g=g_1\circ g_2$ (composition)
is well defined, with $g_1\ge f_1$ and $g_2\ge f_2,$
then $f=f_1\circ f_2$ is well defined and $g$ is a bound on $f$.

In order to implement this idea in practice,
we need to be able to verify that bounds can be composed,
i.e., that the range of one bound is contained in the domain of the next.
With this in mind we adopt the following procedure:
\medskip

\item{a)} Given $\Sigma$ and $\Sigma^\prime,$ we specify
 two collections of sets,
 $$\std(\Sigma)\subset{\cal P}(\Sigma),\quad
 \std(\Sigma^\prime)\subset{\cal P}(\Sigma^\prime).
 \equation(324)$$
\item{b)} Given a map
 $$f\colon\;\PP(\Sigma)\supseteq\DD_f
 \to \PP(\Sigma^\prime)\,,\equation(325)$$
 we construct a bound on $f$ within the class of maps
 $$g\colon\;\std(\Sigma)\supseteq\DD_g
 \to\std(\Sigma^\prime)\,.\equation(326)$$

\medskip
\noindent
The elements of $\std(\Sigma)$ will be referred to
as the standard sets for $\Sigma$.
Unless specified otherwise, the standard sets for a Cartesian product
$\Sigma\times\Sigma^\prime$ will be defined by setting
$$
\std(\Sigma\times\Sigma^\prime)=\std(\Sigma)\times\std(\Sigma^\prime).
\equation(146)
$$

In most of our applications, the primary object of interest
is not a map on power sets, but a map $\varphi$
from some subset $\DD_\varphi$ of $\Sigma$ to $\Sigma^\prime$.
In this case, the indicated procedure is applied
after we lift $\varphi$ in the canonical way to a set map $f$
with domain $\DD_f=\PP(\DD_\varphi)$, by setting
$$
f(S)=\{s^\prime\in\Sigma^\prime\;|\
s^\prime=\varphi(s){\rm~for~some~} s\in S\}
\equation(147)
$$
for every $S\in\DD_f.$
By definition, a map $g$ is a bound on $f$ if and only if
$S\in\DD_f$ and $f(S)\subseteq g(S)$, for all $S\in\DD_g\,$.
Here, the latter holds if and only if
$s\in\DD_\varphi$ and $\varphi(s)\in g(S)$, whenever $s\in S\in\DD_g\,$.

In this paper, a bound $g$ on
$f\colon\;\PP(\Sigma)\supseteq\DD_f\to \PP(\Sigma^\prime)$
will be specified in Prolog
by means of clauses for a predicate \p$contains/2\l$.
The definition will be such that if $\t{S}\in\std(\Sigma)$, then
\p$G contains f(S)\l$ is true if and only if \t{S} is in the domain of $g$
and \t{G}$=g(\t{S}).$


\section Elementary Operations with Real Numbers

In this section we introduce a systematic way
of computing ``with real numbers''.
Following the procedure outlined in Section 4, we start by
defining the standard sets for $\real.$

\claim Definition(real) $\std(\real)$ is defined to be the collection
of all closed real intervals \t{i(X,Y)} of the form
$$
\t{i(X,Y)}=\{r\in\real\;|\ \t{X}\le r\le\t{Y}\},
\equation(329)
$$
with $\t{X}\le\t{Y}$ elements of $\SS.$

Consider now the function unary minus which maps
a real number $r\in\real$ to its negative $-r$.
The canonical lift of this map to $\PP(\real)$ associates
to any given $I\in\PP(\real)$ the set
$$
-(I)=\{r\in\real\;|\ r=-x {\rm~for~some~} x\in I\}.
\equation(432)
$$
A bound $g$, in the sense of Section 4, on the lifted unary minus
is obtained by setting $\DD_g=\std(\real)$ and defining
$g(I)=-(I)$ for all sets $I\in\DD_g$.
The following clause for \p$contains/2\l$ implements this definition,
i.e., for any given standard set \t{I},
the goal \p$I1 contains -I\l$ becomes true if and only if $\t{I1}=g(\t{I})$.
\pro
\prolog{i(X1,Y1) contains -i(X,Y):-}
\prolog{ X1 is -Y,}
\prolog{ Y1 is -X,}
\prolog{ !.}
\log
Here, we have used that if $r$ is a safe number then so is $-r$,
and that the computation of $-r$ from $r$ is done exactly.

Our second bound is on the absolute value function.
Let \p$i(P,Q)\l$ be a fixed but arbitrary standard set for $\real$.
It is easy to check that the following holds
independently of whether this set contains zero,
or only positive numbers, or only negative numbers:
if \t{X} is the largest of the numbers zero, \t{P} and \t{-Q},
and if \t{Y} is the negative of the smallest of the same three numbers,
then \p$i(X,Y)\l$ is a standard set that contains
the absolute value $|r|$ of any number $r$ in \p$i(P,Q)\l$.
In Prolog, this fact is stated by the clause
\pro
\prolog{i(X,Y) contains abs(i(P,Q)):-}
\prolog{ N is -Q,}
\prolog{ sort_numbers([0,P,N],[R,_,X]),}
\prolog{ Y is -R,}
\prolog{ !.}
\log
where \t{0} is the number zero.
The predicate \p$sort_numbers/2\l$ used here is defined in Subsection 13.3.
If \t{L1} is a list of numbers,
then \p$sort_numbers(L1,L2)\l$ is satisfied if and only if
\t{L2} matches the list which is obtained by sorting
the members of \t{L1} in increasing order.
As in the case of the unary minus,
the given clause for \p$contains/2\l$ defines a bound
with domain $\std(\real)$
on the (set map associated with the) function considered.

The bounds to be defined next deal with
functions of the form $\varphi((r_1,r_2))=r_1\#r_2$,
where $\#$ is one of the binary operators $+,$ $*,$ or $/.$
One of the things that distinguishes these functions
from the ones discussed so far is
that they need not be evaluated exactly on the computer,
even if $r_1$ and $r_2$ are in $\SS$, as we shall now assume.
However, as far as bounds are concerned,
it is sufficient to find an interval \p$i(X1,Y1)\l$
that contains $r_1\#r_2$, given an interval \p$i(X,Y)\l$
that contains the computed value for $r_1\#r_2$.
The following predicate \t{enlarges/2} serves this purpose:
\pro
\prolog{i(X1,Y1) enlarges i(X,Y):-}
\prolog{ X1 is_a_safe_lower_bound_on X,}
\prolog{ Y1 is_a_safe_upper_bound_on Y,}
\prolog{ !.}
\log
To be more precise, if \t{X}$\le$\t{Y} are given representable numbers
(not necessarily in the safe range),
then \p$i(X1,Y1) enlarges i(X,Y)\l$ is satisfied
if and only if the indicated safe lower bound \t{X1}
and safe upper bound \t{Y1} can be found,
in which case \p$i(X1,Y1)\l$ is a standard set
with the above--mentioned property, as explained in Section 3.
A typical application of \t{enlarges/2} is given in the next clause.

Consider now the sum function from $\real\times\real$ to $\real$.
The corresponding set map assigns to a pair $(I_2,I_3)$
in $\PP(\real)\times\PP(\real)$ the set
$$
I_2+I_3=\{r\in\real\;|\ r=x+y {\rm~for~some~} x\in I_2\ , y\in I_3\}
\equation(22)
$$
in $\PP(\real)$. The following clause defines a bound on this map:
\pro
\prolog{i(X1,Y1) contains i(X2,Y2)+i(X3,Y3):-}
\prolog{ X is X2+X3,}
\prolog{ Y is Y2+Y3,}
\prolog{ i(X1,Y1) enlarges i(X,Y),}
\prolog{ !.}
\log
As indicated in Section 4, the domain of this bound
is the set of all pairs $(\t{I2},\t{I3})$
in $\std(\real)\times\std(\real)$ for which \p$I1 contains I2+I3\l$
is true. In this case, the domain is determined by the
predicate \t{enlarges/2} which is used
in order to compensate for possible rounding errors
introduced by \t{is/2}, and to make sure that
the returned result \t{I1} is again a standard set.

The same description applies to our bound on the product
of (sets of) real numbers,
if $+$ is replaced by $*$. The bound itself is defined as follows:
\pro
\prolog{i(X1,Y1) contains i(X2,Y2)*i(X3,Y3):-}
\prolog{ A is X2*X3,}
\prolog{ B is X2*Y3,}
\prolog{ C is Y2*X3,}
\prolog{ D is Y2*Y3,}
\prolog{ sort_numbers([A,B,C,D],[X,_,_,Y]),}
\prolog{ i(X1,Y1) enlarges i(X,Y),}
\prolog{ !.}
\log
Here, we have used that the product of two standard sets $I_2$ and $I_3$
is an interval, and that the endpoints of this interval
can be computed as the maximum and minimum of four
products made up from the endpoints of the intervals $I_2$ and $I_3$.
As in the case of the absolute value function,
we find the maximum and the minimum by sorting.

We note that the difference function can be defined
in terms of the sum and the unary minus.
Since bounds can be composed (in the sense of Section 4),
it suffices to give a general rule for this case.
Such general rules are given in Subsection 13.1.
An analogous remark applies to the quotient function.

This brings us to the function ``inverse'' which
maps a real number $r$ in $\DD=\real\setminus\{0\}$ to $1/r$.
Its lift to $\PP(\DD)$ is defined by setting
$$
I {\rm \ inverse}=\{r\in\real\;|\ r=1/x {\rm~for~some~} x\in I\},
\equation(inverse)
$$
for every $I\in\PP(\DD)$.
A bound on this map is defined by the following clause:
\pro
\prolog{i(X1,Y1) contains (i(X2,Y2) inverse):-}
\prolog{ P is X2*Y2,}
\prolog{ P>0,}
\prolog{ X is 1/Y2,}
\prolog{ Y is 1/X2,}
\prolog{ i(X1,Y1) enlarges i(X,Y),}
\prolog{ !.}
\log
The purpose of the condition \t{P}$>$\t{0}
is to restrict the domain of this bound
to standard sets that do not contain the number zero.

Finally, we consider the function that maps a real number $r$
to $r^\t{N}$, where \t{N} is some (sufficiently small) non--negative integer.
By convention, $r^0=1$ for all $r$.
The lift to $\PP(\real)$ of this function can be obtained
by composing $I\mapsto[I,\t{i(1,1)}]$ with the \t{N}--th
iterate $\t{f}^\t{N}$ of the map $\t{f}: [I,J]\mapsto[I,I*J]$,
followed by the projection $[I,J]\mapsto J$.
In order to get a bound on $\t{f}^\t{N}$,
it suffices to give here a bound on the map \t{f},
such as the one defined by
\pro
\prolog{[I,J1] contains f of [I,J] :-}
\prolog{ J1 contains I*J,}
\prolog{ !.}
\log
The rest is taken care of by a general clause for powers (iterates)
of a map, given in Subsection 13.1.
A bound on $I\mapsto I^\t{N}$ can now be defined as follows:
\pro
\prolog{i(Xn,Yn) contains i(X,Y)**N:-}
\prolog{ [_,i(Xn,Yn)] contains f**N of [i(X,Y),i(1,1)],}
\prolog{ !.}
\log

This completes our discussion of the basic operations on
the standard sets for $\real.$
The next step will be to
establish bounds for operations on polynomials, which are the simplest
functions in the Banach space $\BB.$
However, in order to motivate our choices,
we first reformulate the proof of \clm(1) as a fixed point problem,
so that it will become clear what operations are needed.




%==============================================================================

% CMP_POLY.55b
\section The Contraction Mapping Principle

We prove the existence of a solution to
\equ(1) by applying the contraction mapping principle
to an operator $\RR$ which has the desired solution as a fixed point.
The operator $\RR$ will be defined on an open ball
$$
U_\beta(G_0)=\{G\in\BB_0\;|\ \|G-G_0\|<\beta\}
\equation(156)
$$
of radius $\beta=2^{-18},$
centered at some polynomial $G_0\in\BB_0$ to be chosen later on.
In Prolog, $\beta$ is specified by the clause
\pro
\prolog{radius_of_ball_in_function_space(Beta):-}
\prolog{ negative_power_of_two(Beta,18).}
\log

Let now $G$ be a fixed but arbitrary function in $U_\beta(G_0).$
Then $\RR(G)$ is defined through the following sequence of steps:

\item{i)} Find a solution of the Schr\"oder equation \equ(4)
$$
F(z)-{1\over\lambda}F(G(z))=0,
\equation(135)
$$
where $\lambda=G'(0).$ This equation will be solved
by an iterative procedure (see Section 10).
The result is a one--parameter family of solutions $F=c\FF$,
and we will see that $\FF$ lies in $\BB_0$
and that $c$ can be chosen such that $F(-1+\lambda^2)=1$.

\item{ii)} Compose $\FF$ with the function
$z\mapsto -1+\lambda^2+\lambda^2 z$ to obtain $F_1$,
$$
F_1(z)=\FF(-1+\lambda^2+\lambda^2 z).
\equation(145)
$$
We will show that $F_1$ is an element of $\BB.$

\item{iii)} Define $F_2$ to be the square of $F_1,$
$$
F_2(z)=F_1(z)^2.
\equation(115)
$$

\item{iv)} Normalize $F_2$ according to \equ(5) and \equ(6), by setting
$$
F_3(z)=F_2(z)/F_2(0)-1.
\equation(114  )
$$
This function $F_3$ may seem like a natural candidate for $\RR(G)$,
since $F_3=G$ would imply that the functions $F= c\FF$
and $G$ have the properties described in \clm(1).
However, the map $G\mapsto F_3$ is not a contraction:
it has ``one unstable direction'' which is roughly parallel
to the identity function. We thus add the following step:

\item{v)} Let $\widetilde\lambda={F_3}^\prime(0)$ and define
$\RR(G)$ by the equation
$$
\RR(G)(z)=F_3(z)+1.72(\lambda-\widetilde\lambda)z.
\equation(113)
$$

The value $1.72$ has been found empirically;
see also the footnote in Section 12.
In Prolog we define (a standard set containing) this number
with the predicate \p$contraction_factor/1\l${,}
\pro
\prolog{contraction_factor(X):-}
\prolog{ X contains i(172,172)/i(100,100).}
\log
We note that if $G$ is a fixed point of $\RR$,
then equation \equ(113) implies that
$\lambda=\widetilde\lambda+1.72(\lambda-\widetilde\lambda)$.
As a consequence we have $\widetilde\lambda=\lambda$, and thus $G=F_3$.
This in turn implies that the functions $F$
and $G$ have the properties described in \clm(1).

The remaining part of this paper will be devoted to the proof
of the following theorem, which implies \clm(1).

\claim Theorem(2) There exist two positive real numbers
$\rho<1$ and $\varepsilon<(1-\rho)\beta$,
and a polynomial $G_0\in\BB_0$ of degree nine (all three defined below),
such that the following holds.
The operator $\RR$ is well defined and continuously differentiable
as a map from $U_\beta(G_0)$ to $\BB_0$,
and at any given point $G\in U_\beta(G_0)$,
the operator norm of its derivative $D\RR(G)$ is bounded by $\rho$,
$$
\|D\RR(G)\|\le\rho \quad(\approx 0.94)\;.
\equation(111)
$$
Furthermore, $\RR(G_0)$ lies within distance $\varepsilon$ of $G_0$,
$$
\|\RR(G_0)-G_0\|\le\varepsilon \quad (\approx 1.3\cdot 10^{-7})\;.
\equation(112)
$$

By the contraction mapping principle, this theorem implies
that $\RR$ has a fixed point $G^*$ in $U_\beta(G_0)$, and that
$$
\|G^*-G_0\|\le{\varepsilon\over 1-\rho }.
\equation(19)
$$


\section Bounds Involving Polynomials

Let $V$ be the vector space of polynomials
over the real numbers.
In this section we define bounds on
maps from $V,$
or from $V\times V,$
to $V$ or to $\real.$
Following the procedure outline in Section 4, we start by
defining the standard sets for $V.$

\claim Definition(stv) We define $\std(V)$ to be the collection
of all sets \t{p([I0,I1,\...])} of the form
$$
\t{p([I0,I1,\...])}=
\{p\in V\,|\; p(x)=p_0+p_1\cdot x+{\cdot\cdot\cdot}\ ,\ \
p_0\in\t{I0},\ p_1\in\t{I1},\ {\cdot\cdot\cdot}\ \}\ ,
\equation(v41)
$$
with \t{[I0,I1,\...]} any finite list of elements
of $\std(\real).$ For the set containing only the polynomial
$p\equiv0$ we also use the notation \t{p([])}.

We note that our program will use these standard sets only
to represent polynomials of degree $18$ or less.
Thus, the reader may think of $V$ as being restricted accordingly.

Our first bound involving polynomials deals with the map ``unary minus''.
The negative of the zero polynomial
is the zero polynomial,
\pro
\prolog{p([]) contains -p([]):-}
\prolog{ !.}
\log
The other cases are covered by the clause
\pro
\prolog{p([H1|T1]) contains -p([H2|T2]):-}
\prolog{ H1 contains -H2,}
\prolog{ p(T1) contains -p(T2),}
\prolog{ !.}
\log
Namely, let $p: x\mapsto c+x\cdot q(x)$ be an element of the standard set
\p$p([H2|T2]).\l$
Then $c$ and $q$ are elements
of the standard sets \t{H2} and \p$p(T2)\l$, respectively.
The bound is based on the identity
$-p(x)=(-c)+x\cdot(-q(x)),$ i.e., \t{H1} contains $-c$ and
\t{p(T1)} contains the polynomial $-q.$

Similarly, our bound on the (lifted) multiplication
of a polynomial with a real number is based
on the identity
$r\cdot p(x)=$$r\cdot(c+x\cdot q(x))=$$(r\cdot c)+x\cdot(r\cdot q(x)).$
The zero polynomial multiplied by a number is equal
to the zero polynomial,
\pro
\prolog{p([]) contains i(_,_)*p([]):-}
\prolog{ !.}
\log
The remaining cases are dealt with by the clause
%
\footnote{$\ \! ^{*)}$}{
We use here the notation \p$i(X,Y)\l$
and not simply \t{I}, or similar,
in order to avoid that this argument matches
terms for which it is not intended, such as \p$p(T)\l$,
which would result in the clause being applied wrongly
to the product of two polynomials.
Our general strategy is to use the most elegant notation that
does not lead to a conflict
between different clauses of the same predicate.}
%
\pro
\prolog{p([H1|T1]) contains i(X,Y)*p([H2|T2]):-}
\prolog{ H1 contains i(X,Y)*H2,}
\prolog{ p(T1) contains i(X,Y)*p(T2),}
\prolog{ !.}
\log

The bound on the
addition of two polynomials is again very similar.
But there are two possible final stages
in the recursive evaluation of \p$p(L2)+p(L3)\l$.
If the list \t{L2} contains at least as many coefficients
as the list \t{L3}, then we will end up
with the zero polynomial in the second argument of the sum,
\pro
\prolog{p(L) contains p(L)+p([]):-}
\prolog{ !.}
\log
Otherwise, the recursion will terminate with the zero polynomial
in the first argument,
\pro
\prolog{p(L) contains p([])+p(L):-}
\prolog{ !.}
\log
If none of the arguments matches \p$p([])\l$,
then the following clause is used:
\pro
\prolog{p([H1|T1]) contains p([H2|T2])+p([H3|T3]):-}
\prolog{ H1 contains H2+H3,}
\prolog{ p(T1) contains p(T2)+p(T3),}
\prolog{ !.}
\log

In order to bound the product of two polynomials,
we will inductively reduce the first factor until
the zero polynomial is reached and the clause
\pro
\prolog{p([]) contains p([])*p(_):-}
\prolog{ !.}
\log
applies. The reduction procedure is based on the fact that
$(c+x\cdot q(x))\cdot h(x)=c \cdot h(x) + x\cdot(q(x)\cdot h(x)).$
The corresponding clause is
\pro
\prolog{p(L1) contains p([H2|T2])*p(L2):-}
\prolog{ p(L) contains p(T2)*p(L2),}
\prolog{ p(L1) contains H2*p(L2)+p([i(0,0)|L]),}
\prolog{ !.}
\log
We note that none of the clauses defined so far
applies to a goal of the form \p$A contains B*C+Q\l$.
This ``problem'' can be solved by reducing the given goal to
\p$P contains B*C, A contains P+Q\l$.
General clauses that carry out such reductions are given in Subsection 13.2.

Another operation which will be needed later
assigns to a polynomial its $\t{N}+1$st Taylor coefficient.
The zero polynomial has all coefficients equal to zero,
\pro
\prolog{i(0,0) contains coeff(_) of p([]):-}
\prolog{ !.}
\log
In the other cases, a bound for the map $p\mapsto p(0)$ is given by
\pro
\prolog{C contains coeff(0) of p([C|_]):-}
\prolog{ !.}
\log
and the higher coefficients are covered recursively by the clause
\pro
\prolog{C contains coeff(N) of p([_|T]):-}
\prolog{ M is N-1,}
\prolog{ C contains coeff(M) of p(T),}
\prolog{ !.}
\log
Next, we consider the derivative of polynomials.
For the zero polynomial we have
\pro
\prolog{p([]) contains der(p([])):-}
\prolog{ !.}
\log
In order to handle the other cases in a reasonably efficient way,
let us introduce the operator $\t{b}=x{d\over dx}$.
By using the bound on $\t{b}+\t{0}\equiv\t{b}$ given below,
we can complete our bound on the derivative as follows:
\pro
\prolog{p(T) contains der(p(L)):-}
\prolog{ p([_|T]) contains (b+0) of p(L),}
\prolog{ !.}
\log
Consider now the sum of \t{b} and \t{N} times the identity,
in symbols \p$b+N\l$, which maps
a monomial $m_k$ of degree $k$ to $(k+\t{N})m_k\,,$ for every $k\ge 0$.
Here, \t{N} is any (sufficiently small) non--negative integer.
Independently of \t{N}, the zero polynomial is mapped to itself by \p$b+N\l$,
\pro
\prolog{p([]) contains (b+_) of p([]):-}
\prolog{ !.}
\log
In the remaining cases, the following clause applies:
\pro
\prolog{p([H1|T1]) contains (b+N) of p([H2|T2]):-}
\prolog{ H1 contains i(N,N)*H2,}
\prolog{ M is N+1,}
\prolog{ p(T1) contains (b+M) of p(T2),}
\prolog{ !.}
\log
Namely, if $p(x)=c+x\cdot q(x)$ then
$((\t{b}+\t{N})p)(x)=\t{N}c+x\cdot((\t{b}+\t{N}+1)q)(x)$.

Finally, we will give a bound on the norm functional on $V$,
which assigns to a polynomial $p$ with coefficients
$p_0,p_1,\ldots,p_n$ the number
$$
\|p\|=\sum_{i=0}^n|p_i|\cdot D^i,
\equation(18)
$$
where $D=1.7$ is the radius of the common domain of analyticity
for functions in $\BB$, as specified in \clm(bbb).
In Prolog, we define a standard set containing $D$
with the predicate \p$domain/1\l$,
\pro
\prolog{domain(D):-}
\prolog{ D contains i(17,17)/i(10,10),}
\prolog{ !.}
\log
The norm of the zero polynomial is zero
\pro
\prolog{i(0,0) contains norm(p([])):-}
\prolog{ !.}
\log
and the remaining cases are covered by the clause
\pro
\prolog{i(0,Y) contains norm(p([H|T])):-}
\prolog{ domain(D),}
\prolog{ i(_,Y) contains abs(H)+D*norm(p(T)),}
\prolog{ !.}
\log
We note that this bound could be ``improved''
by substituting \p$i(X,Y)\l$ for both \p$i(_,Y)\l$ and \p$i(0,Y)\l$
in the last clause.
But for convenience later on,
we ignore lower bounds on the norm of polynomials
and replace them by the trivial lower bound $\t{X}=\t{0}$.


%==============================================================================
% APPROX.56a
\section Approximate Computations with Polynomials

In this section we develop the tools for computing
approximate solutions of the Schr\"oder equation \equ(135),
and of a generalized version of this equation (see below)
which includes an inhomogeneous term.
These approximate solutions will be used later
as input to a procedure that constructs the real solutions.

Consider now the inhomogeneous Schr\"oder equation
$$
F(z)-{1\over\lambda}F(G(z))=J(z),
\equation(hpi)
$$
where $G$ and $J$ are given functions, with $G(0)=J(0)=J^\prime(0)=0$,
and where $\lambda=G^\prime(0)$.
If we define an operator $j(G,F)$ by setting
$$
j(G,J)(F)=J+{1\over\lambda}F\circ G,
\equation(h2)
$$
then the equation \equ(hpi) can be written in the form $F=j(G,J)(F)$.
This suggests that a solution may be obtained by iteration,
e.g. by taking the limit as $n\to\infty$ of the functions
$$
f_n=j(G,J)^n(J+\kappa I)=
\sum_{i=0}^n{1\over\lambda^i}\ \!J\circ G^i
+{\kappa\over\lambda^n}G^n.
\equation(hpi1)
$$
Here, $G^i$ denotes the $i$--fold composition of $G$ with itself,
$I$ is the identity function $I(z)=z$,
and $\kappa$ is an arbitrary constant (as the equation for $F$ is affine).
In Section 10 we will show that under suitable assumptions on $G$ and $J$,
the functions $f_n$ converge in $\BB_0$ to a solution of \equ(hpi).
Thus, $f_n$ is a natural candidate for an approximate solution
of the (inhomogeneous) Schr\"oder equation, if $n$ is large.

Our goal in this section is to compute $f_n$ approximately,
in the case where $G$ and $J$ are polynomials.
To this end, we can freely combine bounds from previous sections
with steps that only produce approximate results.

In particular, we may collapse any interval \p$i(X,Y)\l$
to an interval of length zero,
centered near the arithmetic mean of \t{X} and \t{Y}.
To carry this out for every coefficient--interval
in a set of polynomials, we will use the predicate \p$collapse/2\l$
defined by
\pro
\prolog{collapse(p([i(X,Y)|T1]),p([i(Z,Z)|T2])):-}
\prolog{ Z is (X+Y)/2,}
\prolog{ collapse(p(T1),p(T2)),}
\prolog{ !.}
\log
where the recursion ends with the zero polynomial
\pro
\prolog{collapse(p([]),p([])):-}
\prolog{ !.}
\log
Another useful approximation splits a polynomial $p$
into a polynomial $q$ of degree $\le\t{N}$ and a remainder $r$,
according to the equation $p(x)=q(x)+x^\t{N+1}\cdot r(x),$
and then discards $r$.
The splitting is implemented with a predicate \p$split/4\l$
whose first, third, and fourth argument
is for the set containing $p$, $q$, and $r$, respectively.
We simply take the list of coefficients from the first argument,
say of length $l_p\,$, and split it into a ``head''
of length $l_q=\max(l_p,\t{N}+1)$ and a tail of length $l_r=l_p-l_q\,$.
This is done recursively by using the clause
\pro
\prolog{split(p([H|T1]),N,p([H|T2]),p(L)):-}
\prolog{ N>=0,}
\prolog{ M is N-1,}
\prolog{ split(p(T1),M,p(T2),p(L)),}
\prolog{ !.}
\log
provided that $l_q$ is nonzero.
Otherwise the following clause applies,
which is also reached at the end of the recursion:
\pro
\prolog{split(p(L),_,p([]),p(L)):-}
\prolog{ !.}
\log

The two approximation steps will now be combined.
For reasons that will become clear later,
we choose the degree \t{N} for the above--mentioned truncation
to be equal to $9$. In Prolog,
\pro
\prolog{degree(9).}
\log
The following clause specifies a way of collapsing
a set of polynomials \p$p(L2)\l$
into a set \p$p(L1)\l$ that contains a single
polynomial of degree $\le 9$:
\pro
\prolog{p(L1) approximates p(L2):-}
\prolog{ degree(N),}
\prolog{ split(p(L2),N,p(L3),_),}
\prolog{ collapse(p(L3),p(L1)),}
\prolog{ !.}
\log

As a first step towards a numerical computation of $f_n\,,$
we implement the composition of two polynomials $p$ and $r$.
Let $p(x)=c+x\cdot q(x)$.
Then $(p\circ r)(x)=c+r(x)\cdot(q\circ r)(x),$
and this expression can be used to
(compute as well as to) approximate $p\circ r$.
Namely,
\pro
\prolog{p(L1) approximates p([H|T]) o p(L2):-}
\prolog{ p(L3) approximates p(T) o p(L2),}
\prolog{ p(L4) contains p([H])+p(L3)*p(L2),}
\prolog{ p(L1) approximates p(L4),}
\prolog{ !.}
\log
where \t{H} contains $c,$ \t{p(T)} contains $q,$ and
\t{p(L2)} contains $r.$
The recursion ends with the composition of the zero polynomial
with an arbitrary polynomial,
\pro
\prolog{p([]) approximates p([]) o p(_):-}
\prolog{ !.}
\log
Next, we approximate the image of a polynomial $F$
under map $j(G,J)$. By following the definition \equ(h2), we set
\pro
\prolog{p(Fh) approximates j(p(G),p(J)) of p(F):-}
\prolog{ p(Fg) approximates p(F) o p(G),}
\prolog{ p(F1) contains p(J)+ p(Fg)/ (coeff(1) of p(G)),}
\prolog{ p(Fh) approximates p(F1),}
\prolog{ !.}
\log
Eventually, this approximate version of $j(G,J)$
needs to be iterated, according to \equ(hpi1).
But this can be done by using a general clause given in Subsection 13.1.

In the case where $J\equiv 0$,
we can increase precision and efficiency
by choosing $n=2^m$ and $\kappa=\lambda^n$,
so that $f_n=q^m(G)$,
where $q$ is the operator defined by the equation
$$
q(G)=G\circ G.
\equation(comp)
$$
Again, it suffices to define an approximation for the operator $q$,
\pro
\prolog{p(F) approximates q of p(G):-}
\prolog{ p(F) approximates p(G) o p(G),}
\prolog{ !.}
\log



%==============================================================================
% ANALYTIC.55b
\section Bounds Involving Analytic Functions

The bounds defined in this section involve functions in the space $\BB$.
We start by introducing the standard sets for this space.

\claim Definition(stb) $\std(\BB)$ is defined to be the collection of
all sets \p$f(P,e(G,H))\l$ of the form
$$
\t{f(P,e(G,H))}=\{F\in\BB|F(z)=p(z)+z\cdot g(z)+
z^{10}\cdot h(z),\ p\in \t{P},\|g\|\in \t{G},\|h\|\in \t{H}\},
\equation(41)
$$
with $\t{P}\in\std(V),$ and \t{G}, \t{H} intervals in $\std(\real)$
with lower boundaries equal to zero (as we have no need for nontrivial
lower bounds on norms).

In what follows, if a function $F\in\BB$ is specified as in \equ(41),
then $g$ will be referred to as the ``general error'' for $F$,
and $h$ as the ``higher order error'' for $F$.
We note that $p$ will always be of degree less than $19$,
and usually of degree less than $10$.

Given that any function in $\BB$ has a unique representation
as the sum of a polynomial of degree less than ten,
and a function $\varphi\in\BB$ with $\varphi(z)=\OO(z^{10})$,
the reader may wonder why we consider representations
with nonzero general error terms.
The reason for our choice has to do with the following fact.
Let $\psi$ be some arbitrary analytic function that maps the disk $|z|<D$
to itself, and consider the image under $\varphi\mapsto\varphi\circ\psi$
of a standard set \t{f(p([]),e(i(0,0),i(0,R)))} with $\t{R}>0$.
It is easy to show that this image is contained
in the ball $B=\{f\in\BB:\;\|f\|\le\t{R}\}$,
but not much more can be said in general.
Thus, in order to bound the set map associated with
$\varphi\mapsto\varphi\circ\psi$,
we need to find a standard set $S\subset\BB$ that contains $B$.
This can be done reasonably well with $S$ of the form
\t{f(p([C]),e(G,i(0,0)))}
(our choice of multiplying general errors with $z$
is a disadvantage here, but it turns out to be convenient later).
By contrast, bounds that use only standard sets $S$ of the form
\t{f(P,e(i(0,0),H))} are substantially weaker.
That is, if $S$ contains $B$ then $S$ also contains
functions whose norm is much larger than \t{R}.
Another solution to this problem, besides introducing general error terms,
is to use a Banach space (of analytic functions)
with a weighted sup--norm on the sequence of Taylor coefficients;
see e.g. [KW7].

Our first bound in this section is on (the set map associated with)
the norm functional on $\BB$. The domain of this bound is a subset
of $\std(\BB)$, and its range is a set of intervals in $\std(\real)$
with lower boundaries equal to zero.
By using the inequality
$$
0\le\|f\|\le\|p\|+D\cdot\|g\|+D^{10}\cdot\|h\|,
\equation(13)
$$
such a bound can be defined as follows:
\pro
\prolog{i(0,Y) contains norm(f(P,e(G,H))):-}
\prolog{ domain(D),}
\prolog{ degree(N),}
\prolog{ N1 is N+1,}
\prolog{ i(_,Y) contains norm(P)+D*G+D**N1*H,}
\prolog{ !.}
\log

We will also need bounds
for the two functionals $F\mapsto F(0)$ and $F\mapsto F^\prime(0)$.
If $F\in\BB$ is represented as in \equ(41), then $F(0)=p(0)$
and $F^\prime(0)=p^\prime(0)+g(0)$. Thus,
\pro
\prolog{S contains coeff(0) of f(P,_):-}
\prolog{ S contains coeff(0) of P,}
\prolog{ !.}
\log
and, since $|g(0)|\le\|g\|$, we have
\pro
\prolog{S contains coeff(1) of f(P,e(i(_,Y),_)):-}
\prolog{ X is -Y,}
\prolog{ S contains (coeff(1) of P)+i(X,Y),}
\prolog{ !.}
\log

The following three bounds are based on elementary properties of the norm.
The property $\|c\cdot f\|=|c|\cdot\|f\|$
applies to the multiplication of a function by a number
\pro
\prolog{f(P1,e(G1,H1)) contains i(X,Y)*f(P2,e(G2,H2)):-}
\prolog{ P1 contains i(X,Y)*P2,}
\prolog{ G1 contains abs(i(X,Y))*G2,}
\prolog{ H1 contains abs(i(X,Y))*H2,}
\prolog{ !.}
\log
as well as to the unary minus
\pro
\prolog{f(P,E) contains -f(P1,E):-}
\prolog{ P contains -P1,}
\prolog{ !.}
\log
and the triangle inequality is used when adding two functions,
\pro
\prolog{f(P1,e(G1,H1)) contains f(P2,e(G2,H2))+f(P3,e(G3,H3)):-}
\prolog{ P1 contains P2+P3,}
\prolog{ G1 contains G2+G3,}
\prolog{ H1 contains H2+H3,}
\prolog{ !.}
\log

The multiplication of two functions is slightly more complicated.
Consider functions $f_2$ and $f_3$ of the form
$$
\eqalign{
f_2(z)&=p_2(z)+z\cdot g_2(z)+z^{10}\cdot h_2(z),\cr
f_3(z)&=p_3(z)+z\cdot g_3(z)+z^{10}\cdot h_3(z),\cr
}\equation(F2)
$$
with $p_2$ and $p_3$ polynomials.
Define a polynomial $p_1$ of degree less than ten,
and a polynomial $r$, by the equation
$$
p_1(x)+x^{10}\cdot r(x)=p_2(x)\cdot p_3(x).
\equation(1sd)
$$
Then the product of $f_1$ and $f_2$ is given by the equation
$$
\eqalign{
f_2(z)\cdot f_3(z)
&=p_1(z)\cr
&+z\cdot\bigl[p_2(z)\cdot g_3(z)+g_2(z)\cdot p_3(z)
              +z\cdot g_2(z)\cdot g_3(z)\bigr]\cr
&\eqalign{
+\ \!z^{10}\cdot\bigl[
          &r(z)+
          z^{10}\cdot h_2(z)\cdot h_3(z)+
          p_2(z)\cdot h_3(z)+h_2(z)\cdot p_3(z)\cr
          &+z\cdot g_2(z)\cdot h_3(z) +z\cdot h_2(z)\cdot g_3(z)\bigr].\cr
 }
}
\equation(mult)
$$
This suggests the following bound.
We start with the multiplication of the two
sets of polynomials $\t{P2}\ni p_2$ and $\t{P3}\ni p_3\,,$
\pro
\prolog{f(P1,e(i(0,Yg),i(0,Yh))) contains f(P2,e(G2,H2))*f(P3,e(G3,H3)):-}
\prolog{ P contains P2*P3,}
\logc
which we split into $\t{P1}\ni p_1$ and $\t{R}\ni r$
according to equation \equ(1sd),
\pro
\prolog{ degree(N),}
\prolog{ split(P,N,P1,R),}
\logc
Then,
by using that
$\|f\cdot g\|\le\|f\|\cdot\|g\|$ for any two functions $f$ and $g$ in $\BB$
(this can be verified e.g. by using the Taylor expansion of $f\cdot g$),
we compute
an upper bound on the norm of the general error in \equ(mult),
\pro
\prolog{ domain(D),}
\prolog{ i(_,Yg) contains norm(P2)*G3+ G2*norm(P3)+ D* (G2*G3),}
\logc
and an upper bound on the norm of the higher order error in \equ(mult),
\pro
\prolog{ N1 is N+1,}
\prolog{ i(_,Yh) contains norm(R)+ (D**N1)*H2*H3+ norm(P2)*H3+ H2*norm(P3)}
\prolog{                         + D*G2*H3+ D*H2*G3,}
\prolog{ !.}
\log

Consider now the composition $p\circ f$
of a function $f\in\BB$ with a polynomial $p$.
This operation can be carried out recursively:
if $p(x)=c+x\cdot q(x),$ then we have
$(p\circ f)(x)=c+f(x)\cdot(q\circ f)(x)$.
In particular, if $p$ is identically zero, then so is the result,
\pro
\prolog{f(p([]),E) contains p([]) o f(_,_):-}
\prolog{ zero_error(E),}
\prolog{ !.}
\log
The predicate \p$zero_error/1\l$ used here has been introduced
for convenience. Its only clause is
\pro
\prolog{zero_error(e(i(0,0),i(0,0))).}
\log
The case of a general polynomial is covered by the clause
\pro
\prolog{f(P1,E1) contains p([H|T]) o f(P2,E2):-}
\prolog{ zero_error(E),}
\prolog{ f(P1,E1) contains f(p([H]),E)+f(P2,E2)* (p(T) o f(P2,E2)),}
\prolog{ !.}
\log
where \p$f(p([H]),E)\l$ contains the constant function $f(z)=c.$

Next, we discuss the composition of a function $f_3\in\BB$
with another function $f_2\in\BB$.
In order to ensure that $f_2\circ f_3$ is well defined,
we require that $\|f_3\|<D$. This condition implies that
$f_3$ maps the domain $|z|<D$ into itself, since
$$
\sup_{|z|<D}|f(z)|\le\|f\|,
\equation(1fghfgh)
$$
for every $f\in\BB$.
Let now $f_2$ and $f_3$ be represented in the form \equ(F2).
Then we have
$$
(f_2\circ f_3)(z)=(p_2\circ f_3)(z)+c+z\cdot g(z),
\equation(comp0)
$$
where
$$
c+z\cdot g(z)
=r(z)=
f_3(z)\cdot(g_2\circ f_3)(z)
+(f_3(z))^{10}\cdot(h_2\circ f_3)(z).
\equation(comp2)
$$
The first term on the right hand side of \equ(comp0)
is of the form discussed earlier.
For the remainder $r$ we have
$$
\|r\| \le \|f_3\|\cdot\|g_2\|+\|f_3\|^{10}\cdot \|h_2\|.
\equation(comp1)
$$
This bound can be used to estimate the constant $c$,
and the function $g$ which contributes
to the general error for $f_2\circ f_3$.
Namely, from the definition of the norm in $\BB$, we see that
$$
-\|r\|\le c\le\|r\|,
\equation(comp3)
$$
and
$$
0\le\|g\|\le\|r\|/D.
\equation(comp2)
$$
We note that this is a place where the advantage of using general errors
becomes apparent. Namely, if we
had to convert \equ(comp1) into eleven bounds (as opposed to two),
by insisting on a representation $r(x)=c_0+c_1x+\ldots+c_9x^9+x^{10}h(x)$,
then the result would be much (as opposed to slightly)
weaker than the original bound on $\|r\|$.
In Prolog, the bound on composition is now defined as follows.
By using the predicate \p$lt/2\l${,}
\pro
\prolog{i(_,Y) lt i(X,_):-}
\prolog{ Y<X,}
\prolog{ !.}
\log
which makes \t{I1 lt I2} true
if every $y\in\t{I1}$ is smaller than every $x\in\t{I2}$,
we first check that the norm of the argument corresponding
to the function $f_3$ is less than $D$,
\pro
\prolog{f(P1,E1) contains f(P2,e(G2,H2)) o f(P3,E3):-}
\prolog{ domain(D),}
\prolog{ U contains norm(f(P3,E3)),}
\prolog{ U lt D,}
\logc
Then, we use the estimate \equ(comp1)
to bound the norm of the remainder $r$,
\pro
\prolog{ degree(N),}
\prolog{ N1 is N+1,}
\prolog{ i(_,Y) contains U*G2+U**N1*H2,}
\logc
and convert the result according to \equ(comp3) and \equ(comp2)
into a bound \t{C} and a bound \t{G}
(both represented as a standard set for $\BB$),
\pro
\prolog{ X is -Y,}
\prolog{ zero_error(E),}
\prolog{ C=f(p([i(X,Y)]),E),}
\prolog{ Eg contains i(0,Y)/D,}
\prolog{ G=f(p([]),e(Eg,i(0,0))),}
\logc
At the end, the pieces are added up as in \equ(comp0),
\pro
\prolog{ f(P1,E1) contains P2 o f(P3,E3) + C + G,}
\prolog{ !.}
\log

Finally, we consider the derivative of a function $f_2\in\BB$.
Since $f_2^\prime$ is not necessarily an element of $\BB$,
we will compose $f_2^\prime$ with another function $f_3\in\BB$
whose norm is $\mu D$, with $\mu<1$.
Assume now again that $f_2$ and $f_3$ are given in the form \equ(F2).
Then
$$
(f_2^\prime\circ f_3)(z)=(p_2^\prime\circ f_3)(z)+c+z\cdot g(z),
\equation(comp0d)
$$
where
$$
c+z\cdot g(z)
=r(z)=(e_2^\prime\circ f_3)(z),
\equation(comp2d)
$$
with
$$
e_2(z)=z\cdot g_2(z)+z^{10}\cdot h_2(z).
\equation(comp2dd)
$$
In order to estimate the two terms that contribute to $e_2^\prime\circ f_3$,
let $f$ be a function in $\BB$ with $f(z)=\OO(z^j)$, where $j>0$.
Then we have the bound
$$
\|f^\prime\circ f_3\|\le\|f^\prime(\mu\ \!.\ \!)\|
\le\sup_{i\ge j}(i\ \!\mu^{i-1})\ \!\|f\|/D.
\equation(dern)
$$
The second inequality in \equ(dern) has been obtained by using the fact that
the coefficient of $z^{i-1}$ in the Taylor series for $f^\prime(\mu z)$
is $i\mu^{i-1}$ times the $i$--th Taylor coefficient of $f$.
As a result, the norm of the function $r$ in equation \equ(comp2d)
can be bounded as follows:
$$
\|r\|
\le
\sup_{i\ge1} (i\ \!\mu^{i-1})
\cdot\|g_2\|+
\sup_{i\ge10} (i\ \!\mu^{i-1})
\cdot D^9
\cdot \|h_2\|.
\equation(comp1d)
$$
An upper bound on the supremum in \equ(dern) is given by the inequality
$$
\sup_{i\ge j}(i\ \!\mu^{i-1})\le\sum_{i\ge j}\ \!i\ \mu^{i-1}=
\Bigl({j\ \!\mu^{j-1}\over1-\mu}+{\mu^j\over(1-\mu)^2}\Bigr),
\equation(sup)
$$
which is far from optimal, but easy to implement:
\pro
\prolog{i(0,X) contains sup(J,Q):-}
\prolog{ J1 is J-1,}
\prolog{ Q1 contains i(1,1)-Q,}
\prolog{ i(_,X) contains (Q**J1)*i(J,J)/Q1 + (Q**J)/ (Q1**2),}
\prolog{ !.}
\log
We are now ready to define our bound on the set map for
$(f_2,f_3)\mapsto f_2^\prime\circ f_3\,$.
The first step is to verify that $\mu<1$,
\pro
\prolog{f(P1,E1) contains der(f(P2,e(G2,H2))) o f(P3,E3):-}
\prolog{ domain(D),}
\prolog{ Mu contains norm(f(P3,E3))/D,}
\prolog{ Mu lt i(1,1),}
\logc
Then, following \equ(comp1d),
we compute a bound the norm of the error term $r$
\pro
\prolog{ degree(N),}
\prolog{ N1 is N+1,}
\prolog{ i(_,Y) contains sup(1,Mu)*G2+ sup(N1,Mu)* (D**N)*H2,}
\logc
and convert the result into a bound \t{C} and a bound \t{G},
in exactly the same way as we did in the clause for composition,
by using \equ(comp3) and \equ(comp2),
\pro
\prolog{ X is -Y,}
\prolog{ zero_error(E),}
\prolog{ C=f(p([i(X,Y)]),E),}
\prolog{ Eg contains i(0,Y)/D,}
\prolog{ G=f(p([]),e(Eg,i(0,0))),}
\logc
The last step is to add up the pieces according to equation \equ(comp0d),
\pro
\prolog{ P contains der(P2),}
\prolog{ f(P1,E1) contains P o f(P3,E3) + C + G,}
\prolog{ !.}
\log

%==============================================================================
% SCHRODER.56c
\section The Schr\"oder Equation

In this section we show how to obtain accurate bounds on solutions
of the Schr\"oder equation
$$
F(z)-{1\over\lambda}F(G(z))=J(z).
\equation(schroder)
$$
The general procedure is independent of whether
the equation is homogeneous ($J\equiv 0$) or not.
Namely, we first
compute a polynomial $F_0$ that ``solves'' the given equation
to the desired degree of accuracy,
by using the approximate methods from Section 8.
By substituting the ansatz $F=F_0+F_1$ into \equ(schroder),
we then obtain a Schr\"oder equation for $F_1\,$,
with a (small) inhomogeneous term
$$
J_1= J-\bigl(F_0-{1\over\lambda}F_0\circ G\bigr).
\equation(1222)
$$
Here, both $J_1$ and $F_1$ will be regarded as error terms, i.e.,
besides proving that the equation for $F_1$ has a solution,
we restrict ourselves to
estimating the norms of the general and higher order error
for $F_1$ in terms of the corresponding norms for $J_1$.
We start by explaining the estimates used in this last step.

Let $G$ and $J$ be given functions in $\BB_0$
such that $\lambda=G^\prime(0)$ is nonzero
and $J(z)=\OO(z^k)$, for some integer $k>1$.
Consider the corresponding sequence of functions $f_n\,$,
defined by equation \equ(hpi1) for $\kappa=0$.
Below, we will show that this sequence converges in $\BB_0\,$,
provided that
$$
(\|G\|/D)^2/\ \!|\lambda|<1.
\equation(g1)
$$
We note that this condition implies that $\|G\|<D$ and $|\lambda|<1$,
as can be seen by using the bound $|\lambda|=|G^\prime(0)|\le\|G\|/D$.
This shows e.g. that the map $j(G,J)$, defined by \equ(h2),
is continuous from $\BB_0$ to $\BB_0\,$.
Thus, if we prove that the sequence $\{f_n\}$ converges in $\BB_0\,$,
then we know that
the limit $F$ satisfies the Schr\"oder equation \equ(schroder).

Assume now that the condition \equ(g1) is satisfied,
and define two functions $H$ and $K$ in $\BB$,
by setting $H(z)=G(z)/z$ and $K(z)=J(z)/z^k$.
In addition, let $H_0(z)=1$ and
$$
H_i(z)=\prod_{j=0}^{i-1} H(G^j(z)),
\equation(1fgh)
$$
for all $i>0$. Then, by using that $G^i(z)=z\cdot H_i(z)$,
we can rewrite equation \equ(hpi1), with $\kappa=0$, in the form
$$
f_n(z)=z^k\cdot\sum_{i=0}^n{1\over\lambda^i}[H_i(z)]^k(K\circ G^i)(z).
\equation(1456)
$$
The estimate
$$
\|H_i\|\le\|H\|^i=(\|G\|/D)^i,
\equation(1ert)
$$
together with \equ(g1), now implies that the sum \equ(1456) is bounded
term by term by a convergent geometric series.
Thus, the limit $F=\lim_{n\to\infty}f_n$ exists in $\BB_0\,$, and
$$
\|F\|\le D^k\sum_{i=0}^\infty
\bigl((\|G\|/D)^k/|\lambda|\bigr)^i\|K\|
\le{\|J\|\over1-(\|G\|/D)^k/|\lambda|}.
\equation(134)
$$
Furthermore, since the Taylor coefficients of $f_n$
converge to those of $F$, we have $F(z)=\OO(z^k)$.
In what follows, we will also use the symbol $y(G)J$ in place of $F$, i.e.,
$$
y(G)J=F=\sum_{i=0}^\infty{1\over\lambda^i}\ \!J\circ G^i.
\equation(ygj)
$$

The following Prolog clause implements the norm estimate \equ(134);
it makes a goal \t{E contains norms(y(G) of J)} true only if
the Schr\"oder equation with $G\in\t{G}$ and $J\in\t{J}$
admits a solution $F\in\t{f(p([]),E)}$ of the form described above.
Here, we assume that $G\in\BB_0$
and that $J\in\BB_1=\{f\in\BB:\; f(0)=f^\prime(0)=0\}$, i.e.,
we regard \t{G} and \t{J} as standard sets for the spaces
$\BB_0$ and $\BB_1\,$, respectively.
After checking that $G$ satisfies the condition \equ(g1),
\pro
\prolog{e(Fg,Fh) contains norms(y(G) of f(Jp,e(Jg,Jh))):-}
\prolog{ L contains abs(coeff(1) of G),}
\prolog{ domain(D),}
\prolog{ X contains norm(G)/D,}
\prolog{ C contains X*X/L,}
\prolog{ C lt i(1,1),}
\logc
we split the function $J$
into a term $z\mapsto J_p(z)+z\cdot J_g(z)$ of order $z^2$,
and a higher order error $z\mapsto z^{10}\cdot J_h(z)$.
The images under $y(G)$ of the two parts
are estimated by using \equ(134) first with $k=2$,
\pro
\prolog{ Fg contains (Jg+norm(Jp)/D)/ (i(1,1)-C),}
\logc
and then with $k=10$,
\pro
\prolog{ degree(N),}
\prolog{ N1 is N+1,}
\prolog{ Fh contains Jh/ (i(1,1)-X**N1/L),}
\prolog{ !.}
\log

We are now prepared to bound the set map for $(G,J)\mapsto y(G)J$,
in the way described at the beginning of this section.
Again, this bound is restricted to (standard sets representing)
functions $G$ and $J$ that satisfy $G(0)=0$ and $J(0)=J^\prime(0)=0$.
The first step is to compute an approximate polynomial solution $F_0\,$,
\pro
\prolog{f(P1,E1) contains y(f(P2,E2)) of f(Jp,e(Jg,Jh)):-}
\prolog{ Pj approximates Jp,}
\prolog{ P1 approximates j(P2,Pj)**16 of Pj,}
\prolog{ zero_error(E),}
\prolog{ F0=f(P1,E),}
\logc
Then, a standard set is determined that contains
the function $J_1$ defined in \equ(1222),
\pro
\prolog{ L contains coeff(1) of f(P2,E2),}
\prolog{ J1 contains f(Jp,e(Jg,Jh))- (F0- (F0 o f(P2,E2))/L),}
\logc
We note that $J_1(z)=\OO(z^2)$, since $F_0(0)=0$ by construction,
and $\lambda=G^\prime(0)$.
Thus, the estimate \equ(134) can be applied to bound
the norms of the error terms for $F_1$,
\pro
\prolog{ E1 contains norms(y(f(P2,E2)) of J1),}
\prolog{ !.}
\log

Consider now the homogeneous Schr\"oder equation,
with $G$ and $\lambda$ as above.
Given a function $F_0\in\BB_0$ such that $F_0^\prime(0)=1$,
define $J_1$ by \equ(1222),
and denote by $\eta(G)$ the solution of \equ(schroder) obtained
by solving the equation $F_1-{1\over\lambda}F_1\circ G=J_1$
for $F_1=F-F_0$ as described earlier, i.e.,
$$
\eta(G)=F=F_0+y(G)\bigl(-F_0+{1\over\lambda}F_0\circ G\bigr).
\qquad\qquad (F_0^\prime(0)=1)
\equation(hdef)
$$
We note that this defines $\eta(G)$ independently of the choice of $F_0$.
Namely, if $\Delta F$ is the difference between two solutions
(of the homogeneous Schr\"oder equation) whose derivatives agree at the origin,
then $\Delta F$ is a solution that satisfies $\Delta F(z)=\OO(z^2)$,
which, as is easy to see, implies that $\Delta F\equiv 0$.

A bound on the set map associated with $\eta$ can be defined as follows:
first, we compute an approximate polynomial solution $F_0$
that satisfies $F_0^\prime(0)=1$,
\pro
\prolog{f(P1,E1) contains eta of f(P2,E2):-}
\prolog{ P approximates q**6 of P2,}
\prolog{ C contains coeff(1) of P,}
\prolog{ P1 contains P/C,}
\prolog{ zero_error(E),}
\prolog{ F0=f(P1,E),}
\logc
and then we continue as in the previous clause,
\pro
\prolog{ L contains coeff(1) of f(P2,E2),}
\prolog{ J1 contains - (F0- (F0 o f(P2,E2))/L),}
\prolog{ E1 contains norms(y(f(P2,E2)) of J1),}
\prolog{ !.}
\log




%==============================================================================
% OP.57b
\section Bounds on Maps and Operators

Our main goal in this section is to give a bound on the operator $\RR$.
Following the (informal) five--step definition given in Section 6,
we will write $\RR$ as the composition of five maps,
$\RR=k\circ n\circ s\circ c\circ h$.
Since several of these maps involve the number $\lambda=G^\prime(0)$,
we have chosen to use the space $\BB\times\real$ for intermediate results.
The direct product of a standard set \t{F} for $\BB$
with a standard set \t{I} for $\real$ will be denoted by \t{x(F,I)}.

We start with the map $h$
(solving the \underbar{h}omogeneous Schr\"oder equation)
from $\BB_0$ to $\BB\times\real$, which is defined by the equation
$$
h(G)=\left(\matrix{F\cr\lambda\cr}\right),
\equation(1fghi)
$$
where $\lambda=G^\prime(0)$,
and where $F$ is the solution of the equation $F-{1\over\lambda}F\circ G=0$,
as described in the previous section.
The corresponding bound is given by
\pro
\prolog{x(F,L) contains h of G:-}
\prolog{ F contains eta of G,}
\prolog{ L contains coeff(1) of G,}
\prolog{ !.}
\log
In this clause, \t{G} and \t{F} are considered standard sets for $\BB_0\,$,
defined as in \equ(41), but with $\BB$ replaced by $\BB_0$.

Next, we define the operator $c$ (\underbar{c}omposition) on $\BB\times\real$
by setting
$$
c\left(\matrix{F\cr\lambda\cr}\right)(z)
=\left(\matrix{F(-1+\lambda^2+\lambda^2z)\cr\lambda\cr}\right).
\equation(1fgh)
$$
Here, and in what follows, the second component $\lambda$ is being identified
with the constant map $z\mapsto\lambda$, in order to simplify notation.
A bound on $c$ is defined by the clause
\pro
\prolog{x(F1,L) contains c of x(F,L):-}
\prolog{ B contains L*L,}
\prolog{ A contains B-i(1,1),}
\prolog{ zero_error(E),}
\prolog{ F1 contains F o f(p([A,B]),E),}
\prolog{ !.}
\log
We also need the operator $s$ (\underbar{s}quaring a function),
$$
s\left(\matrix{F_1\cr\lambda\cr}\right)(z)=
\left(\matrix{F_1(z)^2\cr\lambda\cr}\right),
\equation(1fgh)
$$
and the corresponding bound
\pro
\prolog{x(F2,L) contains s of x(F1,L):-}
\prolog{ F2 contains F1*F1,}
\prolog{ !.}
\log
as well as the operator $n$ (\underbar{n}ormalization),
$$
n\left(\matrix{F_2\cr\lambda\cr}\right)(z)=
\left(\matrix{F_2(z)/F_2(0)-1\cr\lambda\cr}\right),
\equation(1hfgh)
$$
and its bound
\pro
\prolog{x(f(p([i(0,0)|P3]),E3),L) contains n of x(F2,L):-}
\prolog{ S contains coeff(0) of F2,}
\prolog{ f(p([_|P3]),E3) contains F2/S,}
\prolog{ !.}
\log
The last step in this sequence is the map $k$
(\underbar{k}ey to contraction) from $\BB_0\times\real$,
which is the range of $n$, to the space $\BB_0\,$,
$$
k\left(\matrix{F_3\cr\lambda\cr}\right)(z)=
F_3(z)+1.72\cdot(\lambda-\widetilde\lambda)\cdot z,
\equation(1dfdf)
$$
where $\widetilde\lambda=F_3^\prime(0).$
A bound on this map $k$ is given by the clause
\pro
\prolog{f(P,E3) contains k of x(f(P3,E3),L):-}
\prolog{ L3 contains coeff(1) of f(P3,E3),}
\prolog{ contraction_factor(S),}
\prolog{ B contains (L-L3)*S,}
\prolog{ P contains P3+p([i(0,0),B]),}
\prolog{ !.}
\log
This leads to the following bound on the operator $\RR$:
\pro
\prolog{G1 contains r of G:-}
\prolog{ G1 contains (k o n o s o c o h) of G,}
\prolog{ !.}
\log
where the composition of two bounds is defined by
\pro
\prolog{Z contains (F o G) of X:-}
\prolog{ Y contains G of X,}
\prolog{ Z contains F of Y,}
\prolog{ !.}
\log
Finally, to give a proper definition of the operator $\RR$,
we define its domain $\DD_\RR$ by requiring
that the condition \equ(g1) be satisfied,
that the function
$z\mapsto -1+\lambda^2+\lambda^2z$ be of norm less than $D$,
and that $F_2(0)\not=0$.


\section Derivatives

The derivative $D\RR$, if it exists, of the operator $\RR$,
maps a pair $(G,H)$ from $\DD_\RR\times\BB_0$
to the function $H_1=D\RR_GH$ in $\BB_0\,$,
where $D\RR_G$ denotes the (Fr\'echet) derivative of $\RR$ at $G$.
By the definition of $\RR$, we have
\pro
\prolog{H1 contains (d(r) at G) of H:-}
\prolog{ H1 contains (d(k o n o s o c o h) at G) of H,}
\prolog{ !.}
\log
In this section we will show that the maps $k$, $n$, $s$, $c$, and $h$
are of class $C^1$ on their domains,
and we will define bounds for their derivatives
(and thus for their tangent maps,
using the bounds from the last section).
Consequently, $\RR$ is of class $C^1$ on its domain,
and a bound for $D\RR$ is obtained by using the chain rule
\pro
\prolog{D contains (d(F o G) at X) of H:-}
\prolog{ Y contains G of X,}
\prolog{ D contains ((d(F) at Y) o (d(G) at X)) of H,}
\prolog{ !.}
\log
Here, and in what follows, we assume that the space $\BB\times\real$
has been equipped with a norm that makes the
canonical embedding of $\BB$ an isometry.

We start with the map $h$ that solves the Schr\"oder equation.
Its domain $\DD_h\subset\BB_0$ is defined by the condition \equ(g1).
On this domain, the map $G\mapsto F\circ G$ is of class $C^1$
(and even analytic) for every function $F\in\BB$.
This fact,
together with the implicit function theorem, implies that the map $h$
is $C^1$ on $\DD_h$. The derivative of $h$ at $G$ can be written as
$$
Dh_GK
=\left(\matrix{H\cr\mu\cr}\right),
\equation(t1)
$$
with $\mu=K^\prime(0)$,
and $H=y(G)J$ the solution of the equation $H-(H\circ G)/\lambda=J$,
where $J=((F^\prime\circ G)\cdot K-\mu\cdot F)/\lambda$,
and where $F$ and $\lambda$ are as in \equ(1fghi).
Our bound for $Dh$ is defined as follows:
\pro
\prolog{x(H,Mu) contains (d(h) at G) of K:-}
\prolog{ Mu contains coeff(1) of K,}
\prolog{ x(F,L) contains h of G,}
\prolog{ Fp contains der(F) o G,}
\prolog{ J contains (Fp*K-Mu*F)/L,}
\prolog{ H contains y(G) of J,}
\prolog{ !.}
\log
Next, we consider the operator $c$.
It is straightforward to check that this operator is $C^1$
on the domain defined by the condition $\|\psi\|<D$,
where $\psi(z)=-1+\lambda^2+\lambda^2z$,
and that its derivative is given by
$$
Dc_{\left(\matrix{F\cr\lambda\cr}\right)}
\left(\matrix{H\cr\mu\cr}\right)(z)=
\left(\matrix{H(\psi(z))+F^\prime(\psi(z))
\cdot(2\lambda+2\lambda z)\cdot\mu\cr\mu\cr}\right).
\equation(t2)
$$
The following defines a bound on $Dc$:
\pro
\prolog{x(H1,Mu) contains (d(c) at x(F,L)) of x(H,Mu):-}
\prolog{ B contains L*L,}
\prolog{ A contains B-i(1,1),}
\prolog{ zero_error(E),}
\prolog{ Psi=f(p([A,B]),E),}
\prolog{ Fp contains der(F) o Psi,}
\prolog{ C contains i(2,2)*L*Mu,}
\prolog{ Fh=f(p([C,C]),E),}
\prolog{ H1 contains H o Psi + Fp*Fh,}
\prolog{ !.}
\log
Squaring a function is clearly a $C^1$ operator on $\BB\times\real$.
For the derivative of $s$ we have the expression
$$
Ds_{\left(\matrix{F_1\cr\lambda\cr}\right)}
\left(\matrix{H_1\cr\mu\cr}\right)(z)=
\left(\matrix{2\ \!F_1(z)\ \!H_1(z)\cr\mu\cr}\right),
\equation(t3)
$$
and the corresponding bound is
\pro
\prolog{x(H2,Mu) contains (d(s) at x(F1,_)) of x(H1,Mu):-}
\prolog{ H2 contains i(2,2)*F1*H1,}
\prolog{ !.}
\log
The normalization operator $n$ and its derivative are
(by the chain rule, which was also used above)
well defined and continuous on the domain $F_2(0)\not=0$.
A bound on $Dn$ is obtained by using the formula
$$
Dn_{\left(\matrix{F_2\cr\lambda\cr}\right)}
\left(\matrix{H_2\cr\mu\cr}\right)(z)=
\left(\matrix{H_2(z)/F_2(0)-H_2(0)F_2(z)/{{F_2(0)}^2}\cr\mu\cr}\right),
\equation(t4)
$$
which translates to
\pro
\prolog{x(H3,Mu) contains (d(n) at x(F2,_)) of x(H2,Mu):-}
\prolog{ S contains coeff(0) of F2,}
\prolog{ T contains coeff(0) of H2,}
\prolog{ H3 contains H2/S - T*F2/ (S*S),}
\prolog{ !.}
\log
As for the operator $k$, it suffices to say that it is linear
and continuous. Thus,
\pro
\prolog{K contains (d(k) at x(_,_)) of x(H3,Mu):-}
\prolog{ K contains k of x(H3,Mu),}
\prolog{ !.}
\log
independent of the base point.
This concludes the definition of our bound for the derivative of $\RR$.

What we need now is a bound for the operator norm of $D\RR$.
We start with a rough estimate for the operator norm of $L\pi_{10}$,
where $L$ is some continuous linear operator on $\BB_0$,
and where $\pi_0,\pi_1,\ldots$ are the projections on $\BB$ defined by
$$
(\pi_jf)(z)=\sum_{n=j+1}^\infty {f^{(n)}(0)\over n!}z^n.
\equation(pijf)
$$
Denoting by $B_j$ the unit ball in the subspace $\pi_j\BB$, we have
$$
\|L\pi_j\|=\sup_{h\in B_j}\|Lh\|.
\equation(lpijnorm)
$$
Given a bound for $L$, the following clause defines an interval
\t{i(0,Yj)} in $\std(\real)$ that contains the norm \equ(lpijnorm)
in the case $j=10$:
\pro
\prolog{i(0,Yj) contains operator_norm(L o pi(J)):-}
\prolog{ degree(N),}
\prolog{ J is N+1,}
\prolog{ domain(D),}
\prolog{ Di contains D inverse,}
\prolog{ i(_,Y) contains Di**J,}
\prolog{ H=f(p([]),e(i(0,0),i(0,Y))),}
\prolog{ i(0,Yj) contains norm(L of H),}
\prolog{ write_useful_information(J,Yj),}
\prolog{ !.}
\log
In order to give the corresponding estimate in the cases $j<10$,
we will use the fact that
$$
\|L\pi_j\|=\max\{\|Lh_j\|, \|L\pi_{j+1}\|\},
\equation(lnorm)
$$
where $h_j(z)=(z/D)^j$.
This identity holds since the map $u\mapsto\sum_{j\ge 1}u_jh_j$
is an isometry from $\ell^1$ onto $\BB_0$.
The functions (basis vectors) $h_j$ can be constructed
by applying the appropriate power of the operator $\zeta$,
$$
(\zeta f)(z)=(z/D)f(z),
\equation(zeta)
$$
to the function $h_0\equiv 1$.
A bound for this operator $\zeta$ is given by the clause
\pro
\prolog{H1 contains z of H0:-}
\prolog{ domain(D),}
\prolog{ Di contains D inverse,}
\prolog{ zero_error(E),}
\prolog{ H1 contains f(p([i(0,0),Di]),E)*H0,}
\prolog{ !.}
\log
Thus, by using the identity \equ(lnorm), we have
\pro
\prolog{i(0,Y) contains operator_norm(L o pi(J)):-}
\prolog{ zero_error(E),}
\prolog{ H0=f(p([i(1,1)]),E),}
\prolog{ Hj contains (z**J) of H0,}
\prolog{ i(0,Yj) contains norm(L of Hj),}
\prolog{ write_useful_information(J,Yj),}
\prolog{ J1 is J+1,}
\prolog{ i(0,Z) contains operator_norm(L o pi(J1)),}
\prolog{ max(Y,Yj,Z),}
\prolog{ !.}
\log
where \t{Y} is the maximum of the numbers \t{Yj} and \t{Z},
according to the clause
\pro
\prolog{max(X,X,Y):-}
\prolog{ X>=Y,}
\prolog{ !.}
\log
and
\pro
\prolog{max(Y,X,Y):-}
\prolog{ Y>X,}
\prolog{ !.}
\log
We have also used the predicate
\p$write_useful_information/2\l${,} which writes
information about the
norm of the \t{J}--th basis vector to the output
(the quoted strings used here are atoms),
\pro
\prolog{write_useful_information(J,Yj):-}
\prolog{ write('norm of L(h'),write(J),write(') is approx.= '),}
\prolog{ write(Yj),nl.}
\log
Finally, the following clause defines a bound $\t{G}\mapsto\t{X}$
for the map $G\mapsto\|D\RR_G\|$, if used with \p$L=(d(r) at G)\l$:
\pro
\prolog{X contains operator_norm(L):-}
\prolog{ X contains operator_norm(L o pi(1)),}
\prolog{ !.}
\log
At this point most of the bounds which we need to prove \clm(2) have been
constructed.

We note that the operator norm of $D\RR_G$
is determined by a single ``column'' vector $D\RR_Gh_j$.
Thus, in order to get an accurate bound on $\|D\RR_G\|$,
the crucial column should be among the ones that are estimated explicitly,
and the corresponding estimate should be sufficiently accurate.
These two requirements determined to a large extent
our choice of \t{degree(N)}
%
\footnote{$\ \!^{*)}$}{The value \p$N=9\l$ has been found by trial and error.
Another quantity which has been chosen empirically,
is the domain $|z|<D$ that enters the definition of $\BB$.
Typically, increasing $D$ makes the first few of the vectors
$D\RR_Gh_i$ larger in norm, and the others smaller.
Similarly, varying the ``contraction factor''
affects the norm of these vectors, although mainly for small $i$.
Our choice of these parameters has been such as to optimize
our estimate on the norm of $D\RR_G$.}.
%
Here, it is of course useful that
(the operator $F\mapsto F\circ\psi$, and thus) the operator $D\RR_G$
is compact, for every $G$ in the domain $\DD_\RR$.


%==============================================================================
% REST.57a
\section General Clauses

In this section we have collected Prolog clauses which are necessary
for the functioning of the program, but which are of very general
nature and to some extent independent of our problem.
The reader (but not Prolog) can safely skip this
section at first reading.


\subsection Differences, Quotients, and Powers

The following clause defines a bound for the difference
of two standard sets in terms of the corresponding
bounds on the unary minus and the sum:
\pro
\prolog{X contains Y-Z:-}
\prolog{ X contains Y+ (-Z),}
\prolog{ !.}
\log
Similarly, a bound on the quotient of two standard sets
is defined by using the multiplicative inverse and the product,
\pro
\prolog{X contains Y/Z:-}
\prolog{ X contains (Z inverse)*Y,}
\prolog{ !.}
\log
In order to bound the \t{N}--th power (iterate)
of an operator \t{F}, we proceed inductively.
By definition, $\t{F}^\t{0}$ is the identity,
\pro
\prolog{X contains F**0 of X :-}
\prolog{ !.}
\log
and for positive values of \t{N} we use the fact that
$\t{F}^\t{N}(\t{X})=\t{F}^\t{N-1}(\t{F}(\t{X}))$,
\pro
\prolog{Y contains F**N of X :-}
\prolog{ M is N-1,}
\prolog{ X1 contains F of X,}
\prolog{ Y contains F**M of X1,}
\prolog{ !.}
\log
Powers are also used for approximate computations. Thus, we define
\pro
\prolog{X approximates F**0 of X :-}
\prolog{ !.}
\log
and
\pro
\prolog{Y approximates F**N of X :-}
\prolog{ M is N-1,}
\prolog{ X1 approximates F of X,}
\prolog{ Y approximates F**M of X1,}
\prolog{ !.}
\log


\subsection Expression Evaluation

Below we will define two clauses
for goals of the form \t{X contains E},
where \t{E} is a term containing at least one argument
that needs to be evaluated (as a bound)
before any of the clauses from previous sections applies.
A bound on the identity map for numbers
\pro
\prolog{i(X,Y) contains i(X,Y):-}
\prolog{ !.}
\log
or for polynomials
\pro
\prolog{p(L) contains p(L):-}
\prolog{ !.}
\log
or for functions
\pro
\prolog{f(P,E) contains f(P,E):-}
\prolog{ !.}
\log
will be used for arguments that are already standard sets.

The following clause applies to expressions \t{E} consisting
of a unary operation \t{F} applied to some other expression \t{X}:
\pro
\prolog{Y contains E:-}
\prolog{ E =.. [F,X],}
\prolog{ E1 =.. [F,S],}
\prolog{ S contains X,}
\prolog{ Y contains E1,}
\prolog{ !.}
\log
Namely, we first use the predicate \p$=../2\l$ (see Subsection 2.7)
to define a new expression \t{E1} that is identical to \t{E},
but with the subexpression \t{X} replaced by a variable \t{S}.
In the next step, \t{X} is evaluated (as a bound)
and the result is placed in \t{S}.
Now that \t{S} is a standard set,
the goal \t{Y contains E1} is handled by the clauses from previous sections.

Similarly, in the case of a binary operation we have
\pro
\prolog{Y contains E:-}
\prolog{ E =.. [F,X1,X2],}
\prolog{ E1 =.. [F,S1,S2],}
\prolog{ S1 contains X1,}
\prolog{ S2 contains X2,}
\prolog{ Y contains E1,}
\prolog{ !.}
\log
Here, one of the subexpressions \t{X1} or \t{X2}
may be a standard set,
in which case it is evaluated by using the appropriate
(bound for the) identity map defined above.


\subsection Sorting Numbers

If \t{L1} is instantiated to a list of representable numbers,
then the following clauses for \p$sort_numbers/2\l$
will make \p$sort_numbers(L1,L2)\l$ true,
with \t{L2} the list of numbers from \t{L1} sorted in increasing order.
We use sorting by insertion.
Unless the given list is empty and thus sorted,
\pro
\prolog{sort_numbers([],[]):-}
\prolog{ !.}
\log
we start by sorting the list consisting of all but the first number,
and then insert this number in the right place
\pro
\prolog{sort_numbers([H1|T1],L):-}
\prolog{ sort_numbers(T1,T2),}
\prolog{ insert_a_number(H1,T2,L),}
\prolog{ !.}
\log
by going down the already sorted part of the list, if necessary,
\pro
\prolog{insert_a_number(X,[H|T],[H|L]):-}
\prolog{ X>H,}
\prolog{ insert_a_number(X,T,L),}
\prolog{ !.}
\log
until the number can be prepended without
being in front of a smaller element
\pro
\prolog{insert_a_number(X,L,[X|L]):-}
\prolog{ !.}
\log


\section Proving the Theorem

In this section we give a proof of \clm(2),
up to trivial numerical estimates
that can be carried out by a computer.
We also define the approximate polynomial solution $G_0$
and the two numbers $\varepsilon$ and $\rho$
mentioned in \clm(2).

Given that the operator $\RR$ will be shown to be a contraction
in some neighborhood of $G_0$,
it is natural to construct $G_0$
by iterating an approximate version of $\RR$,
starting with a rough initial guess for the fixed point.
The transformation $\RR_{\rm approx}$ is defined
(on standard sets for polynomials) by the clause
\pro
\prolog{P1 approximates r of P2:-}
\prolog{ zero_error(E),}
\prolog{ f(P,_) contains r of f(P2,E),}
\prolog{ P1 approximates P,}
\prolog{ !.}
\log
We are now ready to combine the bounds from previous sections
into a \p$proof/0\l$.
Starting with an initial \t{Guess}
containing the function $z\mapsto -0.4\cdot z$,
we iterate $\RR_{\rm approx}$ thirteen times,
\pro
\prolog{proof:-}
\prolog{ I contains -i(4,4)/i(10,10),}
\prolog{ Guess=p([i(0,0),I]),}
\prolog{ P0 approximates r**13 of Guess,}
\prolog{ zero_error(E),}
\prolog{ G0=f(P0,E),}
\logc
in order to get a set \t{G0} whose single element is
the desired polynomial $G_0$.
The number $\varepsilon$ in \clm(2) is now defined to be the following
upper bound \t{Eps} on the norm of $\RR(G_0)-G_0$:
\pro
\prolog{ i(_,Eps) contains norm((r of G0)-G0),}
\prolog{ write('Epsilon is approx.='),write(Eps),nl,}
\logc
Next, we construct a standard set \t{U} containing the ball
$U_\beta(G_0)\subset\BB_0$ of radius $\beta$ centered at $G_0$,
\pro
\prolog{ radius_of_ball_in_function_space(Beta),}
\prolog{ write('Beta is approx.='),write(Beta),nl,}
\prolog{ domain(D),}
\prolog{ Ball contains i(0,Beta)/D,}
\prolog{ U=f(P0,e(Ball,i(0,0))),}
\logc
and determine an upper bound $\rho$
on the operator norm of the derivative $D\RR_G$,
for every point in the standard set \t{U},
\pro
\prolog{ i(_,Rho) contains operator_norm(d(r) at U),}
\prolog{ write('Rho is approx.='),write(Rho),nl,}
\logc
Finally, after checking the inequality
$\varepsilon<(1-\rho)\cdot\beta$,
\pro
\prolog{ i(Rhs,_) contains (i(1,1)-i(Rho,Rho))*i(Beta,Beta),}
\prolog{ Eps < Rhs,}
\logc
the proof of \clm(2) is completed.
\pro
\prolog{ write('q.e.d.'),nl,}
\prolog{ !.}
\log
With the following headless clause,
we ask Prolog to verify the \t{proof},
by going through the steps indicated above
and carrying out the corresponding numerical estimates,
as specified in the previous sections:
\pro
\prolog{:- proof.}
\log


\section Appendix: Running the Program

The reader who would like to carry out the \t{proof}
is invited to go through the following steps.
(We assume that the reader has access to the file proof.pl
containing the program. This file is produced e.g.
by running the .tex file of this paper through the \TeX compiler.)
After the Prolog system is started, the following prompt will appear:
\pro
?-
\log
At this point, it suffices to type
\pro
consult('proof.pl').
\log
and then to hit the ``return'' key.
This makes Prolog read through
the file proof.pl in the way described in Subsection 2.6.
When Prolog reaches the clause \p$:-proof\l${,}
it makes an attempt to verify the \t{proof}.
If Prolog succeeds (as it will, if it conforms to
the standards described in Sections 2 and 3)
then the program will terminate by displaying ``q.e.d.'',
and the prompt \t{?-} will return.

%REFS.4
\bigskip\noindent
\bigskip\noindent
\bigskip\noindent
{\xbold Acknowledgements}\hfill\break
P.W. and H.K. would like to thank
the Department of Mathematics at the University of Texas at Austin
and the Department of Theoretical Physics at the University of Geneva,
respectively, for their hospitality while part of this work was carried out.
We are grateful to Logic Programming Associates Ltd (LPA)
for donating a copy of their Prolog compiler,
and to Brian D. Steel at LPA for many helpful discussions.
We also thank Jan Wehr and Giampaolo d'Alessandro
for a careful reading of preliminary versions of the manuscript.

\vfill\break\eject


{\xbold References}
%\hfill\break

\item{[C]}
A.~Celletti:
{\it Construction of librational invariant tori in the spin--orbit problem}.
Journal of Applied Mathematics and Physics (ZAMP), {\bf 45}, 61 (1993).

\item{[CC]}
A.~Celletti and L.~Chierchia:
{\it Construction of Analytic KAM Surfaces and Effective Stability Bounds}.
Commun. Math. Phys., {\bf 118}, 119--161 (1988).

\item{[CM]} W.F.~Clocksin and C.S.~Mellish:
{\it Programming in Prolog}. Third, Revised and Extended Edition.
Springer--Verlag (1987).

\item{[E]}
H.~Epstein:
{\it Fixed Points of Composition Operators}.
In: Nonlinear Evolution and Chaotic Phenomena,
G.~Gallavotti and P.~Zweifel (editors).
NATO ASI Series B: Phys., {\bf 176}, 71--100 (1987).

\item{[EKW1]}
J.-P.~Eckmann, H.~Koch, and P.~Wittwer:
{\it Existence of a Fixed Point of the Doubling Transformation
for Area--Preserving Maps of the Plane}.
Phys. Rev. A, {\bf 26}, 720--722 (1982).

\item{[EKW2]}
J.-P.~Eckmann, H.~Koch and P.~Wittwer:
{\it A Computer--Assisted Proof of Universality for Area--Preserving Maps}.
Memoirs of the American Mathematical Society, {\bf  47}, 1--121 (1984).

\item{[EMO]}
J.-P.~Eckmann, A.~Malaspinas, and S.~Oliffson-Kamphorst:
{\it A software tool for analysis in function spaces}.
In: Computer Aided Proofs in Analysis, K.~Meyer and D.~Schmidt (editors).
The IMA Volumes in Mathematics, {\bf 28}, 147--166 (1991).

\item{[EW1]}
J.-P.~Eckmann and P.~Wittwer:
{\it Computer Methods and Borel Summability Applied to Feigenbaum's Equation}.
Lecture Notes in Physics, {\bf 227}.
Springer--Verlag, Berlin Heidelberg New York (1985).

\item{[EW2]}
J.-P.~Eckmann and P.~Wittwer:
{\it A complete proof of the Feigenbaum conjectures}.
J.~Stat. Phys., {\bf 46}, 455--477 (1987).

\item{[FL]}
C.~Feffermann and R.~de~la~Llave:
{\it Relativistic Stability of Matter, I}.
Revista Matem\'a\-tica Iberoamericana, {\bf 2/1,2}, 119--213 (1986).

\item{[FS]}
C.~Feffermann and L.~Seco:
{\it Aperiodicity of the Hamiltonian Flow in the Thomas--Fermi Potential}.
Revista Matem\'atica Iberoamericana, {\bf 9/3}, 409--551 (1993).

\item{[IEEE]}
{\it The IEEE Standard for Binary Floating--Point Arithmetic}.
ANSI/IEEE Std 754--1985. (Can be ordered from
IEEE Standard Board, 345 East 47th Street, New York, NY 10017, USA).

\item{[KW1]}
H.~Koch and P.~Wittwer:
{\it A Non--Gaussian Renormalization Group Fixed Point for
Hierarchical Scalar Lattice Field Theories}.
Commun. Math. Phys., {\bf 106}, 495--532 (1986).

\item{[KW2]}
H.~Koch and P.~Wittwer:
{\it Rigorous Computer--Assisted Renormalization Group Analysis}.
In: VIIIth International Congress on Mathematical Physics,
M. Mebkhout and R. S\'en\'eor (editors).
World Scientific (1986).

\item{[KW3]}
H.~Koch and P.~Wittwer:
{\it Computing Bounds on Critical Indices}.
In: Non--Linear Evolution and Chaotic Phenomena,
G.~Gallavotti and P.~Zweifel (editors).
NATO ASI Series B: Phys., {\bf 176}, 269--277 (1987).

\item{[KW4]}
H.~Koch and P.~Wittwer:
{\it The Unstable Manifold of a Nontrivial RG Fixed Point}.
Canadian Mathematical Society, Conference Proceedings, {\bf 9}, 99--105 (1988).

\item{[KW5]}
H.~Koch and P.~Wittwer:
{\it On the Renormalization Group Transformation
for Scalar Hierarchical Models}.
Commun. Math. Phys., {\bf 138}, 537--568 (1991).

\item{[KW6]}
H.~Koch and P.~Wittwer:
{\it A Nontrivial Renormalization Group Fixed Point
for the Dyson--Baker Hierarchical Model}.
Commun. Math. Phys., {\bf 164}, 627--647 (1994).

\item{[KW7]}
H.~Koch and P.~Wittwer:
{\it Bounds on the Zeros of a Renormalization Group Fixed Point}.
Preprint Austin/Geneva (1994).

\item{[KP]}
R.S.~MacKay and I.C.~Percival:
{\it Converse KAM: Theory and Practice}.
Commun. Math. Phys., {\bf 98}, 469--512 (1985).

\item{[La1]}
O.E.~Lanford:
{\it Remarks on the accumulation of period--doubling bifurcations}.
In: Mathematical Problems in Theoretical Physics.
Lecture Notes in Physics, {\bf 116}, 340--342 (1979).

\item{[La2]}
O.E.~Lanford:
{\it Computer--Assisted Proof of the Feigenbaum Conjectures}.
Bull. A.M.S. (New Series), {\bf 6}, 427--434 (1982).

\item{[La3]}
O.E.~Lanford:
{\it Computer--Assisted Proofs in Analysis}.
Physica, {\bf 124 A}, 465--470 (1984).

\item{[La4]}
O.E.~Lanford:
{\it A Shorter Proof of the Existence of the Feigenbaum Fixed Point}.
Commun. Math. Phys., {\bf 96}, 521--538 (1984).

\item{[Lla]}
R.~de~la~Llave:
{\it Computer assisted proofs of stability of matter}.
In: Computer Aided Proofs in Analysis, K.~Meyer and D.~Schmidt (editors).
The IMA Volumes in Mathematics, {\bf 28}, 116--126 (1991).

\item{[Llo]} J.W.~Lloyd:
{\it Foundations of Logic Programming}. Second, Extended Edition.
Sprin\-ger--Verlag (1987).

\item{[LPA]} Logic Programming Associates Ltd., Studio 4,
The Royal Victoria Patriotic Building, Trinity Road,
London SW18 3SX, England.

\item{[LR1]}
R.~de~la~Llave and D.~Rana:
{\it Accurate Bounds in K.A.M. Theory}.
In: VIIIth International Congress on Mathematical Physics,
M. Mebkhout and R. S\'en\'eor (editors).
World Scientific (1986).

\item{[LR2]}
R.~de~la~Llave and D.~Rana:
{\it Accurate Strategies for Small Denominator Problems}.
Bull. Amer. Math. Soc., {\bf 22}, 85-0-90 (1990).

\item{[LR3]}
R.~de~la~Llave and D.~Rana:
{\it Accurate strategies in K.A.M. problems and their implementation}.
In: Computer Aided Proofs in Analysis, K.~Meyer and D.~Schmidt (editors).
The IMA Volumes in Mathematics, {\bf 28}, 127--146 (1991).

\item{[M]}
B.D.~Mestel:
{\it A computer assisted proof of universality for cubic critical maps
of the circle with golden mean rotation number}.
Ph.D. Thesis, Math. Dept., University of Warwick (1985).

\item{[MM]}
K.~Mischaikow and M.~Mrozek:
{\it Chaos in the Lorentz Equations: A Computer--Assisted Proof}.
Bull. AMS, {\bf 32}, 66--72 (1995).

\item{[Ra]} D.~Rana:
{\it Proof of Accurate Upper and Lower Bounds for Stability Domains
in Small Denominator Problems}.
Ph.D. Thesis, Princeton University (1989).

\item{[Ro]} P.~Ross:
{\it Advanced Prolog}. Techniques and Examples.
Addison--Wesley Publishing Company (1989).

\item{[Se1]}
L.~Seco:
{\it A Lower Bounds for the Ground State Energy of Atoms}.
Thesis, Princeton University (1989).

\item{[Se2]}
L.~Seco:
{\it Computer Assisted Lower Bounds for Atomic Energies}.
In: Computer Aided Proofs in Analysis, K.~Meyer and D.~Schmidt (editors).
The IMA Volumes in Mathematics, {\bf 28}, 241--251 (1991).

\item{[SP]} Swedish Institute of Computer Science, PO Box 1263, S-164 28
Kista, Sweden.

\item{[SS]} L.~Sterling and E.~Shapiro:
{\it The Art of Prolog}. Advanced Programming Techniques.
The Massachusetts Institute of Technology (1988).

\item{[St]} A. Stirnemann:
{\it Existence of the Siegel Disc Renormalization Fixed Point}.
Nonlinearity, {\bf 7}, 959--974 (1994).

\item{[XSC]} E.~Adams and E.~Kulisch (editors):
{\it Scientific Computing with Automatic Result Verification}.
Applications in the Engineering Sciences.
Academic Press, San Diego (1993).

%==============================================================================
\closeout3
\message{*********************************************************************}
\message{regarding CURRENT VERSIONS, see the end of this TeX file}
%
% Current versions of this preprint are available by anonymous ftp from
% host: kalymnos.unige.ch   file: pub/wittwer/preprint.tex
% host: math.utexas.edu     file: pub/papers/koch/prolog.tex
%
\message{*********************************************************************}

\end




