%!PS-Adobe-2.0 %%Creator: dvips 5.47 Copyright 1986-91 Radical Eye Software %%Title: w-book.dvi %%Pages: 10 1 %%BoundingBox: 0 0 612 792 %%EndComments %%BeginProcSet: tex.pro /TeXDict 200 dict def TeXDict begin /N /def load def /B{bind def}N /S /exch load def /X{S N}B /TR /translate load N /isls false N /vsize 10 N /@rigin{ isls{[0 1 -1 0 0 0]concat}if 72 Resolution div 72 VResolution div neg scale Resolution VResolution vsize neg mul TR matrix currentmatrix dup dup 4 get round 4 exch put dup dup 5 get round 5 exch put setmatrix}N /@letter{/vsize 10 N}B /@landscape{/isls true N /vsize -1 N}B /@a4{/vsize 10.6929133858 N}B /@a3{ /vsize 15.5531 N}B /@ledger{/vsize 16 N}B /@legal{/vsize 13 N}B /@manualfeed{ statusdict /manualfeed true put}B /@copies{/#copies X}B /FMat[1 0 0 -1 0 0]N /FBB[0 0 0 0]N /nn 0 N /IE 0 N /ctr 0 N /df-tail{/nn 8 dict N nn begin /FontType 3 N /FontMatrix fntrx N /FontBBox FBB N string /base X array /BitMaps X /BuildChar{CharBuilder}N /Encoding IE N end dup{/foo setfont}2 array copy cvx N load 0 nn put /ctr 0 N[}B /df{/sf 1 N /fntrx FMat N df-tail} B /dfs{div /sf X /fntrx[sf 0 0 sf neg 0 0]N df-tail}B /E{pop nn dup definefont setfont}B /ch-width{ch-data dup length 5 sub get}B /ch-height{ch-data dup length 4 sub get}B /ch-xoff{128 ch-data dup length 3 sub get sub}B /ch-yoff{ ch-data dup length 2 sub get 127 sub}B /ch-dx{ch-data dup length 1 sub get}B /ch-image{ch-data dup type /stringtype ne{ctr get /ctr ctr 1 add N}if}B /id 0 N /rw 0 N /rc 0 N /gp 0 N /cp 0 N /G 0 N /sf 0 N /CharBuilder{save 3 1 roll S dup /base get 2 index get S /BitMaps get S get /ch-data X pop /ctr 0 N ch-dx 0 ch-xoff ch-yoff ch-height sub ch-xoff ch-width add ch-yoff setcachedevice ch-width ch-height true[1 0 0 -1 -.1 ch-xoff sub ch-yoff .1 add]{ch-image} imagemask restore}B /D{/cc X dup type /stringtype ne{]}if nn /base get cc ctr put nn /BitMaps get S ctr S sf 1 ne{dup dup length 1 sub dup 2 index S get sf div put}if put /ctr ctr 1 add N}B /I{cc 1 add D}B /bop{userdict /bop-hook known{bop-hook}if /SI save N @rigin 0 0 moveto}N /eop{clear SI restore showpage userdict /eop-hook known{eop-hook}if}N /@start{userdict /start-hook known{start-hook}if /VResolution X /Resolution X 1000 div /DVImag X /IE 256 array N 0 1 255{IE S 1 string dup 0 3 index put cvn put}for}N /p /show load N /RMat[1 0 0 -1 0 0]N /BDot 260 string N /rulex 0 N /ruley 0 N /v{/ruley X /rulex X V}B /V statusdict begin /product where{pop product dup length 7 ge{0 7 getinterval(Display)eq}{pop false}ifelse}{false}ifelse end{{gsave TR -.1 -.1 TR 1 1 scale rulex ruley false RMat{BDot}imagemask grestore}}{{gsave TR -.1 -.1 TR rulex ruley scale 1 1 false RMat{BDot}imagemask grestore}}ifelse B /a{ moveto}B /delta 0 N /tail{dup /delta X 0 rmoveto}B /M{S p delta add tail}B /b{ S p tail}B /c{-4 M}B /d{-3 M}B /e{-2 M}B /f{-1 M}B /g{0 M}B /h{1 M}B /i{2 M}B /j{3 M}B /k{4 M}B /w{0 rmoveto}B /l{p -4 w}B /m{p -3 w}B /n{p -2 w}B /o{p -1 w }B /q{p 1 w}B /r{p 2 w}B /s{p 3 w}B /t{p 4 w}B /x{0 S rmoveto}B /y{3 2 roll p a}B /bos{/SS save N}B /eos{clear SS restore}B end %%EndProcSet TeXDict begin 1000 300 300 @start /Fa 1 108 df<3C000C000C00180018001800187031 903230340038007F00618061906190C1A0C0C00C117E9010>107 D E /Fb 8 126 df57 D<007C007C007C007C007C007C007C007C007C007C007C007C007C007C007C 007C007C007C007C007C007C007C007C00F800F800F800F001F001E003C007C007800F001E007C 00F000C0000E25798025>59 D61 D I<0001F8000FF8003FF800FFF801FFF803FE0007E0000F80001E0000380000700000600000E000 00C00000150E818413>122 DII<000018000038 0000300000700000E00003C0000F80003F0003FE00FFFC00FFF800FFE000FF8000FC0000150E81 8D13>I E /Fc 1 51 df<7FFFFFC0FFFFFFE0C0000060C0000060C0000060C0000060C0000060 C0000060C0000060C0000060C0000060C0000060C0000060C0000060C0000060C0000060C00000 60C0000060C0000060C0000060C0000060C0000060C0000060C0000060C0000060FFFFFFE0FFFF FFE01B1B7B9E25>50 D E /Fd 7 122 df<07001880304060404080FF00C000C000C0008000C0 40C08043003C000A0E7B8D10>101 D<030706000000000000384C4C4C8C181818303262622438 08177D960B>105 D<3E0C0C0C0C181818183030303060606060C0D0D0D0D06007177C9609>108 D<387044984708460C8C180C180C180C18183018311861186230263038100E7D8D14>110 D<078018C0304060606060C060C060C06080C080C08180C10046003C000B0E7B8D12>I<1C7022 88230C230C460C060C060C060C0C180C180C100C301A601B8018001800300030003000FC000E14 7E8D12>I<1C0826184618461886300C300C300C30186018601860186008C007C000C000807180 730066003C000D147D8D11>121 D E /Fe 1 47 df<40E04003037D8209>46 D E /Ff 3 67 df<03000700FF0007000700070007000700070007000700070007000700070007 0007000700070007007FF00C157E9412>49 D<001000003800003800003800005C00005C00005C 00008E00008E00008E0001070001070003078002038002038007FFC00401C00401C00800E00800 E01800E03800F0FE03FE17177F961A>65 DI E /Fg 6 111 df<0000C00000C00001C00001C00003C000 05C00005E00008E00008E00010E00020E00020E00040E000C0E00080E001FFF001007002007004 0070040070080070180070FE03FE17177F961A>65 D<07FFF800E00E00E00700E00300E00301C0 0301C00701C00701C00E03803C03FFF003FFF003803C07001C07000E07000E07000E0E001C0E00 1C0E00380E00701C01E0FFFF0018177F961B>I<0300038003000000000000000000000000001C 002400460046008C000C0018001800180031003100320032001C0009177F960C>105 D<00180038001000000000000000000000000001C0022004300430086000600060006000C000C0 00C000C001800180018001806300E300C60078000D1D80960E>I<1F0006000600060006000C00 0C000C000C00181C1866188E190C32003C003F00318060C060C460C460C8C0C8C0700F177E9612 >I<383C0044C6004702004602008E06000C06000C06000C0C00180C00180C4018184018188030 0880300F00120E7F8D15>110 D E /Fh 6 109 df0 D<020002000200C218F2783AE00F800F803AE0F278C2180200020002000D0E7E8E12>3 D<0400020008000100080001001000008020000040FFFFFFF8FFFFFFF820000040100000800800 010008000100040002001D0C7D8D23>36 D<060F0F0E1E1E1C3C383830707060E0C04008117F91 0A>48 D<000FFFF0003FFFF000C300600103000003070000060700000406000000060000000E00 00000C0000000C0000001FFC00001FF800001800000030000000300000006000000060000000C0 000000C0000071800000FF0000007C0000001C17809619>70 D<020006000F001F802640C63006 000600060006000600060006000600060006000600060006000600060006000600060006000600 0600C63026401F800F00060002000C217D9812>108 D E /Fi 19 117 df<000FF000007FFC00 01F80E0003E01F0007C03F000F803F000F803F000F801E000F800C000F8000000F8000000F8000 000F800000FFFFFF00FFFFFF000F801F000F801F000F801F000F801F000F801F000F801F000F80 1F000F801F000F801F000F801F000F801F000F801F000F801F000F801F000F801F000F801F000F 801F000F801F007FF0FFE07FF0FFE01B237FA21F>12 D<00180000780001F800FFF800FFF80001 F80001F80001F80001F80001F80001F80001F80001F80001F80001F80001F80001F80001F80001 F80001F80001F80001F80001F80001F80001F80001F80001F80001F80001F80001F8007FFFE07F FFE013207C9F1C>49 D<03FC000FFF003C1FC07007E07C07F0FE03F0FE03F8FE03F8FE01F87C01 F83803F80003F80003F00003F00007E00007C0000F80001F00003E0000380000700000E01801C0 180380180700180E00380FFFF01FFFF03FFFF07FFFF0FFFFF0FFFFF015207D9F1C>I<00FE0007 FFC00F07E01E03F03F03F03F81F83F81F83F81F81F03F81F03F00003F00003E00007C0001F8001 FE0001FF000007C00001F00001F80000FC0000FC3C00FE7E00FEFF00FEFF00FEFF00FEFF00FC7E 01FC7801F81E07F00FFFC001FE0017207E9F1C>I<0000E00001E00003E00003E00007E0000FE0 001FE0001FE00037E00077E000E7E001C7E00187E00307E00707E00E07E00C07E01807E03807E0 7007E0E007E0FFFFFEFFFFFE0007E00007E00007E00007E00007E00007E00007E000FFFE00FFFE 17207E9F1C>I<1000201E01E01FFFC01FFF801FFF001FFE001FF8001BC0001800001800001800 0018000019FC001FFF001E0FC01807E01803E00003F00003F00003F80003F83803F87C03F8FE03 F8FE03F8FC03F0FC03F07007E03007C01C1F800FFF0003F80015207D9F1C>I<387CFEFEFE7C38 0000000000000000387CFEFEFE7C3807167C9510>58 D68 D80 D<7FFFFFFF807FFFFFFF807E03F80F807803F807807003F803806003F80180E003F801C0E003F8 01C0C003F800C0C003F800C0C003F800C0C003F800C00003F800000003F800000003F800000003 F800000003F800000003F800000003F800000003F800000003F800000003F800000003F8000000 03F800000003F800000003F800000003F800000003F800000003F800000003F800000003F80000 0003F8000003FFFFF80003FFFFF80022227EA127>84 D<00FE0007FF800F87C01E01E03E01F07C 00F07C00F8FC00F8FC00F8FFFFF8FFFFF8FC0000FC0000FC00007C00007C00007E00003E00181F 00300FC07003FFC000FF0015167E951A>101 D<003F8000FFC001E3E003C7E007C7E00F87E00F 83C00F80000F80000F80000F80000F80000F8000FFFC00FFFC000F80000F80000F80000F80000F 80000F80000F80000F80000F80000F80000F80000F80000F80000F80000F80000F80000F80000F 80007FF8007FF80013237FA211>I104 D<1C003F007F007F007F003F001C000000000000000000000000000000FF00FF 001F001F001F001F001F001F001F001F001F001F001F001F001F001F001F001F001F001F00FFE0 FFE00B247EA310>I109 DI<00FE0007FFC00F83E01E00F03E00F87C007C7C007C 7C007CFC007EFC007EFC007EFC007EFC007EFC007EFC007E7C007C7C007C3E00F81F01F00F83E0 07FFC000FE0017167E951C>I114 D<0180000180000180000180000380000380000780000780000F80003F80 00FFFF00FFFF000F80000F80000F80000F80000F80000F80000F80000F80000F80000F80000F80 000F81800F81800F81800F81800F81800F830007C30003FE0000F80011207F9F16>116 D E /Fj 19 121 df<70F8F8F87005057C840E>58 D<70F8FCFC7404040404080810102040060F 7C840E>I<0000001800000078000001E00000078000001E00000078000003E000000F8000003C 000000F0000003C000000F0000003C000000F0000000F00000003C0000000F00000003C0000000 F00000003C0000000F80000003E0000000780000001E0000000780000001E00000007800000018 1D1C7C9926>I<000080000180000180000300000300000300000600000600000600000C00000C 00000C0000180000180000180000300000300000300000600000600000600000C00000C00000C0 000180000180000180000180000300000300000300000600000600000600000C00000C00000C00 00180000180000180000300000300000300000600000600000600000C00000C00000C000001131 7DA418>II<00000080000000018000000001C000000003C000000003C000000007C0000000 0BC00000000BC000000013C000000033C000000023C000000043C000000043E000000081E00000 0181E000000101E000000201E000000201E000000401E000000C01E000000801E000001001E000 001FFFF000002000F000006000F000004000F000008000F000008000F000010000F000030000F0 00020000F000040000F8000C0000F8001E0000F800FF800FFF8021237EA225>65 D<007FFFF8000007800F00000780078000078003C0000F0001C0000F0001C0000F0001E0000F00 01E0001E0001C0001E0003C0001E0003C0001E000780003C000F00003C001E00003C003C00003C 01F000007FFFE00000780078000078003C000078001E0000F0001E0000F0000E0000F0000F0000 F0000F0001E0001E0001E0001E0001E0001E0001E0003C0003C0003C0003C000780003C000F000 03C001C00007C00F8000FFFFFC000023227EA125>I<007FFFF8000007801E0000078007000007 800380000F0001C0000F0001C0000F0000E0000F0000E0001E0000E0001E0000F0001E0000F000 1E0000F0003C0000F0003C0000F0003C0000F0003C0000F000780001E000780001E000780001E0 00780001E000F00003C000F00003C000F000038000F000078001E000070001E0000E0001E0001E 0001E0001C0003C000380003C000700003C000E00003C003800007C00E0000FFFFF8000024227E A128>68 D<00007F00400003C0C080000E002180001C0013800070000F8000E000070001C00007 00038000070007000007000F000002000E000002001E000002003C000002003C00000400780000 000078000000007800000000F000000000F000000000F000000000F000000000F0003FFF00E000 00F000E00000F000E00000F000E00001E000F00001E000F00001E000700001E000700003C00038 0003C000180007C0000C0009C00006001180000380E08000007F00000022247DA226>71 D<007FFE000007C0000007800000078000000F0000000F0000000F0000000F0000001E0000001E 0000001E0000001E0000003C0000003C0000003C0000003C000000780000007800000078000000 78000000F0000000F0000000F0001000F0001001E0002001E0002001E0004001E0004003C000C0 03C0008003C0018003C0078007C01F00FFFFFF001C227EA121>76 D<007FC00001FF0007C00003 E00007C00005E00007C00005E00009E0000BC00009E0000BC00009E00013C00009E00023C00011 E00027800011E00047800011E00047800011E00087800021E0010F000020F0010F000020F0020F 000020F0040F000040F0041E000040F0081E000040F0081E000040F0101E000080F0203C000080 78203C00008078403C00008078803C0001007880780001007900780001007900780001007A0078 0002007C00F00002007C00F00002003800F00006003800F0000F003001F000FFE0203FFF003022 7EA12F>I<007FFFF0000007801C000007800F000007800700000F000380000F000380000F0003 80000F000380001E000780001E000780001E000780001E000F00003C000F00003C001E00003C00 3C00003C007000007801E000007FFF00000078000000007800000000F000000000F000000000F0 00000000F000000001E000000001E000000001E000000001E000000003C000000003C000000003 C000000003C000000007C0000000FFFC00000021227EA11F>80 D<1FFFFFFE1E01E00E1801E006 3001E0062003C0062003C0064003C0044003C00440078004800780048007800400078000000F00 00000F0000000F0000000F0000001E0000001E0000001E0000001E0000003C0000003C0000003C 0000003C00000078000000780000007800000078000000F0000000F0000000F0000000F0000001 F00000FFFFC0001F227EA11D>84 D86 D<00F0000FE00000E00000E00000E00001C00001C00001C00001C000038000038000038000 0380000700000700F00703080704380E08780E10780E20300E40001C80001F00001FC0001C7000 383800383800381C00381C10703820703820703820701840E00C8060070015237DA219>107 D<3C07E01F00461830618047201880C087401D00E087801E00E087801C00E087001C00E00E0038 01C00E003801C00E003801C00E003801C01C007003801C007003801C007007001C007007043800 E007083800E00E083800E00E083800E006107001C006203000C003C026157E942B>109 D<3C07C04618604720308740388780388700388700380E00700E00700E00700E00701C00E01C00 E01C01C01C01C13801C23803823803823801847001883000F018157E941D>I<1E001818230038 3C4380383E4380701E8380700E83807006870070060700E0040E00E0040E00E0040E00E0041C01 C0081C01C0081C01C0081C01C0101C01C0101C01C0201C03C0400C04C0C00708E10001F03E001F 157E9423>119 D<01E0F006310C081A1C101A3C201C3C201C18201C0000380000380000380000 380000700000700000700000700860E010F0E010F0E020E170404230803C1F0016157E941C>I E /Fk 38 122 df<00000FE0000030180000E01C0001C03C0001803C0003803800038000000380 000007000000070000000700000007000000070000000E000000FFFFE0000E00E0000E00E0000E 01C0001C01C0001C01C0001C01C0001C0380001C03800038038000380380003807000038070000 3807000070070800700E1000700E1000700E1000700E2000E0062000E003C000E0000000E00000 00C0000001C0000001C0000071800000F1800000F3000000620000003C0000001E2D82A21B>12 D45 D<000FC000106000603800801800801C01001C02201E02101E 04101E04101E04101E08203C08203C0840380840780880F00700E00001C0000300000600001800 00200000C0000100000200000400100800301000202000605F80C063FFC040FF80807F00801E00 17227CA019>50 D<0000030000000300000007000000070000000F0000000F0000001F0000002F 0000002F0000004F0000004F800000878000008780000107800002078000020780000407800004 07800008078000080780001007800030078000200780007FFF80004007C0008007C0008003C001 0003C0030003C0020003C0040003C0040003C00C0003C03C0007C0FF003FFC1E237DA224>65 D<00007F00800003808100000E00630000380027000070001F0000E0000E0001C0000E00038000 0E000700000E000F000004000E000004001E000004003C000004003C0000080078000000007800 0000007800000000F000000000F000000000F000000000F000000000F000000000E000000000E0 00002000E000002000E000004000E000004000F000008000700000800070000100003800020000 18000400001C0008000006003000000381C0000000FE000000212479A223>67 D<00FFFFFF80000F000780000F000180000F000180001E000180001E000180001E000100001E00 0100003C000100003C000100003C010100003C0100000078020000007802000000780600000078 0E000000FFFC000000F00C000000F00C000000F00C000001E008000001E008000001E008040001 E000080003C000080003C000080003C000100003C000100007800020000780006000078000C000 078001C0000F8007C000FFFFFF800021227DA121>69 D<00FFFFFF000F000F000F0003000F0003 001E0003001E0003001E0002001E0002003C0002003C0002003C0102003C010000780200007802 000078060000780E0000FFFC0000F00C0000F00C0000F00C0001E0080001E0080001E0080001E0 000003C0000003C0000003C0000003C00000078000000780000007800000078000000F800000FF FC000020227DA120>I<00FFF8000F00000F00000F00001E00001E00001E00001E00003C00003C 00003C00003C0000780000780000780000780000F00000F00000F00000F00001E00001E00001E0 0001E00003C00003C00003C00003C0000780000780000780000780000F8000FFF80015227DA113 >73 D<00FFFC00000F8000000F0000000F0000001E0000001E0000001E0000001E0000003C0000 003C0000003C0000003C00000078000000780000007800000078000000F0000000F0000000F000 0000F0000001E0000001E0000001E0002001E0002003C0004003C0004003C0008003C000800780 0180078001000780030007800F000F803E00FFFFFE001B227DA11F>76 D<00FF000FFC000F8001 E0000F800180000FC000800013C001000013C001000011E001000011E001000021E002000020F0 02000020F002000020F0020000407804000040780400004078040000403C040000803C08000080 3E080000801E080000801E080001001F100001000F100001000F10000100079000020007A00002 0007A000020003E000020003E000040003C000040001C000040001C0000C0001C0001E00008000 FFC000800026227DA124>78 D<00FFFFE0000F0038000F001E000F000E001E0007001E0007001E 0007001E0007003C000F003C000F003C000F003C001E0078001E0078003C00780078007800E000 F003C000FFFE0000F0000000F0000001E0000001E0000001E0000001E0000003C0000003C00000 03C0000003C00000078000000780000007800000078000000F800000FFF8000020227DA121>80 D<00FFFFC0000F0070000F003C000F001C001E000E001E000E001E000F001E000F003C001E003C 001E003C001E003C003C0078003800780070007801E00078078000FFFC0000F00E0000F0070000 F0038001E003C001E003C001E003C001E003C003C0078003C0078003C0078003C0078007800F00 07800F0107800F01078007020F800702FFF8038C000000F020237DA124>82 D<0001F020000E0C40001802C0003001C0006001C000E0018000C0018001C0018001C0018003C0 010003C0010003C0000003C0000003E0000001F8000001FF000000FFE000007FF000001FF80000 03FC0000007C0000003C0000001E0000001E0000001E0020001C0020001C0020001C0020001800 6000380060003000700060007000C000C8018000C607000081FC00001B247DA21B>I<1FFFFFF8 1E03C0381803C0183003C01820078018200780184007801040078010400F0010800F0010800F00 10000F0000001E0000001E0000001E0000001E0000003C0000003C0000003C0000003C00000078 000000780000007800000078000000F0000000F0000000F0000000F0000001E0000001E0000001 E0000001E0000003E00000FFFF00001D2277A123>I86 DI<00F8C0 0185C00705C00E03800E03801C03803C0380380700780700780700780700F00E00F00E00F00E00 F00E10F01C20701C20703C20305C40308C400F078014157B9419>97 D<007E0001C10003018007 03800E07801C07803C0000380000780000780000780000F00000F00000F00000F00000F0010070 0100700200300C001830000FC00011157B9416>99 D<00003C0003F80000380000380000380000 700000700000700000700000E00000E00000E00000E00001C000F9C00185C00705C00E03800E03 801C03803C0380380700780700780700780700F00E00F00E00F00E00F00E10F01C20701C20703C 20305C40308C400F078016237BA219>I<00F803840E021C023C0238027804F018FFE0F000F000 E000E000E000E000E002E0026004701830600F800F157A9416>I<00003E0000470000CF00018F 000186000380000380000380000700000700000700000700000700000E0000FFF0000E00000E00 000E00001C00001C00001C00001C00001C00003800003800003800003800003800007000007000 00700000700000700000E00000E00000E00000E00000C00001C00001C000718000F18000F30000 6200003C0000182D82A20F>I<001F180030B800E0B801C07001C0700380700780700700E00F00 E00F00E00F00E01E01C01E01C01E01C01E01C01E03800E03800E0780060B8006170001E7000007 00000700000E00000E00000E00701C00F01800F0300060E0003F8000151F7E9416>I<00F0000F E00000E00000E00000E00001C00001C00001C00001C00003800003800003800003800007000007 1F0007218007C0C00F00E00F00E00E00E00E00E01C01C01C01C01C01C01C01C038038038038038 0380380704700708700E08700E10700610E006206003C016237DA219>I<00C001E001C001C000 0000000000000000000000000000001C002300430043008700870087000E000E001C001C001C00 380038003840708070807080710032001C000B217BA00F>I<00F0000FE00000E00000E00000E0 0001C00001C00001C00001C0000380000380000380000380000700000701E0070210070C700E10 F00E10F00E20600E40001D80001E00001FC0001C7000383800383800381C00381C207038407038 40703840701880E01880600F0014237DA216>107 D<01E01FC001C001C001C003800380038003 8007000700070007000E000E000E000E001C001C001C001C003800380038003800700070007000 7100E200E200E200E200640038000B237CA20C>I<1C0F80F8002610C10C004760660600878078 07008780780700870070070087007007000E00E00E000E00E00E000E00E00E000E00E00E001C01 C01C001C01C01C001C01C01C001C01C03820380380384038038070403803807080380380308070 070031003003001E0023157B9428>I<1C0F002631C04740C08780E08780E08700E08700E00E01 C00E01C00E01C00E01C01C03801C03801C03801C0704380708380E08380E103806107006203003 C016157B941B>I<007E0001C3000381800701C00E01C01C01E03C01E03801E07801E07801E078 01E0F003C0F003C0F00380F00780700700700E00700C0030180018700007C00013157B9419>I< 01C1F002621804741C08780C08700E08700E08701E00E01E00E01E00E01E00E01E01C03C01C03C 01C03C01C07803807003807003C0E003C1C0072380071E000700000700000E00000E00000E0000 0E00001C00001C00001C0000FFC000171F7F9419>I<1C1F002620804741C08783C08703C08701 808700000E00000E00000E00000E00001C00001C00001C00001C00003800003800003800003800 0070000030000012157B9415>114 D<00FC000183000200800401800C03800C03000C00000F00 000FF00007FC0003FE00003E00000F00000700700700F00600F00600E004004008002030001FC0 0011157D9414>I<00C001C001C001C001C003800380038003800700FFF8070007000E000E000E 000E001C001C001C001C003800380038003810702070207040708031001E000D1F7C9E10>I<1E 00602300E04380E04381C08381C08701C08701C00703800E03800E03800E03801C07001C07001C 07001C07081C0E10180E101C0E101C1E200C262007C3C015157B941A>I<1E03802307C04387C0 4383C08381C08700C08700C00700800E00800E00800E00801C01001C01001C01001C02001C0200 1C04001C08001C08000C300003C00012157B9416>I<1E0060E02300E1F04380E1F04381C0F083 81C0708701C0308701C030070380200E0380200E0380200E0380201C0700401C0700401C070040 1C0700801C0700801C0701001C0F01000C0F020006138C0003E0F0001C157B9420>I<03C1E004 6210083470103CF02038F020386020380000700000700000700000700000E00000E00000E00000 E02061C040F1C040F1C080E2C100446200383C0014157D9416>I<1E00302300704380704380E0 8380E08700E08700E00701C00E01C00E01C00E01C01C03801C03801C03801C03801C07001C0700 1C07001C0F000C3E0003CE00000E00000E00001C00601C00F03800F03000E0600080C000438000 3E0000141F7B9418>I E /Fl 51 128 df<60F0F0701010101020204080040C7C830C>44 DI<60F0F06004047C830C>I<03C00C301818300C300C700E60066006E0 07E007E007E007E007E007E007E007E007E007E007E007E00760066006700E300C300C18180C30 07E0101D7E9B15>48 D<030007003F00C700070007000700070007000700070007000700070007 00070007000700070007000700070007000700070007000F80FFF80D1C7C9B15>I<07C0183020 1C400C400EF00FF80FF807F8077007000F000E000E001C001C00380070006000C0018003000601 0C01180110023FFE7FFEFFFE101C7E9B15>I<07E01830201C201C781E780E781E381E001C001C 00180030006007E00030001C001C000E000F000F700FF80FF80FF80FF00E401C201C183007E010 1D7E9B15>I<300C3FF83FF03FC020002000200020002000200023E024302818301C200E000E00 0F000F000F600FF00FF00FF00F800E401E401C2038187007C0101D7E9B15>53 D<00F0030C06040C0E181E301E300C700070006000E3E0E430E818F00CF00EE006E007E007E007 E007E007600760077006300E300C18180C3003E0101D7E9B15>I<03E00C301008200C20066006 600660067006780C3E083FB01FE007F007F818FC307E601E600FC007C003C003C003C003600260 04300C1C1007E0101D7E9B15>56 D<60F0F0600000000000000000000060F0F06004127C910C> 58 D<000600000006000000060000000F0000000F0000000F0000001780000017800000178000 0023C0000023C0000023C0000041E0000041E0000041E0000080F0000080F0000180F800010078 0001FFF80003007C0002003C0002003C0006003E0004001E0004001E000C001F001E001F00FF80 FFF01C1D7F9C1F>65 DI<001F808000E061800180198007000780 0E0003801C0003801C00018038000180780000807800008070000080F0000000F0000000F00000 00F0000000F0000000F0000000F0000000F0000000700000807800008078000080380000801C00 01001C0001000E000200070004000180080000E03000001FC000191E7E9C1E>II70 D<001F808000E0618001801980070007800E0003801C0003801C00018038 000180780000807800008070000080F0000000F0000000F0000000F0000000F0000000F0000000 F000FFF0F0000F80700007807800078078000780380007801C0007801C0007800E00078007000B 800180118000E06080001F80001C1E7E9C21>I73 D76 DII<003F800000E0E0000380380007001C000E000E001C0007003C00 078038000380780003C0780003C0700001C0F00001E0F00001E0F00001E0F00001E0F00001E0F0 0001E0F00001E0F00001E0700001C0780003C0780003C0380003803C0007801C0007000E000E00 07001C000380380000E0E000003F80001B1E7E9C20>II82 D<07E0801C1980300580700380600180E00180E00080E00080E00080F00000F800007C00 007FC0003FF8001FFE0007FF0000FF80000F800007C00003C00001C08001C08001C08001C0C001 80C00180E00300D00200CC0C0083F800121E7E9C17>I<7FFFFFC0700F01C0600F00C0400F0040 400F0040C00F0020800F0020800F0020800F0020000F0000000F0000000F0000000F0000000F00 00000F0000000F0000000F0000000F0000000F0000000F0000000F0000000F0000000F0000000F 0000000F0000000F0000001F800003FFFC001B1C7F9B1E>II87 D<1FC000307000783800781C 00301C00001C00001C0001FC000F1C00381C00701C00601C00E01C40E01C40E01C40603C40304E 801F870012127E9115>97 DI<07E00C3018783078703060 00E000E000E000E000E000E00060007004300418080C3007C00E127E9112>I<003F0000070000 070000070000070000070000070000070000070000070000070003E7000C1700180F0030070070 0700600700E00700E00700E00700E00700E00700E00700600700700700300700180F000C370007 C7E0131D7E9C17>I<03E00C301818300C700E6006E006FFFEE000E000E000E000600070023002 18040C1803E00F127F9112>I<00F8018C071E061E0E0C0E000E000E000E000E000E00FFE00E00 0E000E000E000E000E000E000E000E000E000E000E000E000E000E000E007FE00F1D809C0D>I< FC00001C00001C00001C00001C00001C00001C00001C00001C00001C00001C00001C7C001C8700 1D03001E03801C03801C03801C03801C03801C03801C03801C03801C03801C03801C03801C0380 1C03801C0380FF9FF0141D7F9C17>104 D<18003C003C00180000000000000000000000000000 00FC001C001C001C001C001C001C001C001C001C001C001C001C001C001C001C001C00FF80091D 7F9C0C>I107 DIII<03F0000E1C00180600300300700380600180E001C0E001C0E001C0 E001C0E001C0E001C06001807003803003001806000E1C0003F00012127F9115>II114 D<1F9030704030C010C010E010F8007F803FE00FF000F880388018C018C018E0 10D0608FC00D127F9110>I<04000400040004000C000C001C003C00FFE01C001C001C001C001C 001C001C001C001C001C101C101C101C101C100C100E2003C00C1A7F9910>IIII<7F 8FF00F03800F030007020003840001C80001D80000F00000700000780000F800009C00010E0002 0E000607000403801E07C0FF0FF81512809116>II<6060F0F0F0F060600C047C 9C15>127 D E /Fm 3 123 df<040004000400C460E4E03F800E003F80E4E0C460040004000400 0B0D7E8D11>3 D<0C000C000C000C000C000C00FFC0FFC00C000C000C000C000C000C000C000C 000C000C000C000C000C000C000C000C000C000C000A1A7E9310>121 D<0C000C000C000C000C 000C00FFC00C000C000C000C000C000C0000000C000C000C000C000C00FFC0FFC00C000C000C00 0C000C000A1A7E9310>I E /Fn 10 107 df0 D<000FFFFC007FFFFC01F0000003800000060000000C0000001800000030000000300000006000 000060000000C0000000C0000000C0000000C0000000C0000000C0000000C00000006000000060 0000003000000030000000180000000C000000060000000380000001F00000007FFFFC000FFFFC 00000000000000000000000000000000000000000000000000000000000000007FFFFFFC7FFFFF FC1E277C9F27>18 D21 D<0000C00000000000C000000000018000000000030000 0000000300000000000600000000000C00000000001800000000003FFFFFFFE0007FFFFFFFE001 C0000000000700000000003E0000000000F800000000003C00000000000F000000000003800000 000000C000000000007FFFFFFFE0003FFFFFFFE0001C00000000000C0000000000060000000000 03000000000001800000000001800000000000C00000000000C00000002B1C7D9932>40 D<0000006000000000006000000000003000000000001800000000001800000000000C00000000 00060000000000030000FFFFFFFF8000FFFFFFFFC000000000007000000000001C00000000000F 800000000003E0000000000780000000001E00000000003800000000006000FFFFFFFFC000FFFF FFFF80000000000700000000000600000000000C00000000001800000000003000000000003000 000000006000000000006000002B1C7D9932>I<001FFF007FFF01E0000380000600000C000018 0000300000300000600000600000600000C00000C00000FFFFFFFFFFFFC00000C0000060000060 00006000003000003000001800000C000006000003800001E000007FFF001FFF181E7C9A21>50 D<00000300000300000600000600000C00000C0000180000180000300000300000600000600000 C00000C00000C0000180000180000300000300000600000600000C00000C000018000018000030 0000300000600000600000C00000C0000180000180000300000300000300000600000600000C00 000C0000180000180000300000300000600000600000C00000400000183079A300>54 D<40000010C0000030600000606000006060000060300000C0300000C0300000C0180001801800 01800C0003000C0003000C00030007FFFE0007FFFE0003000C0003000C0003000C000180180001 8018000180180000C0300000C030000060600000606000006060000030C0000030C00000198000 0019800000198000000F0000000F0000000F000000060000000600001C2480A21D>56 D<00001FFFFE0000FFFFFF0003FFFFFF000F1E000C00181E000800701E000000E01C000000E01C 000001C03C00000100380000000038000000007800000000780000000070000000007000000000 F000000000FFFF000000FFFE000001FFFC000001C000000003C000000003800000000380000000 070000000007000000000F000000000E000000000E000000001C000000201C0000007038000000 F838000000FC700000007FC00000003F800000001E0000000028247FA124>70 D106 D E /Fo 80 125 df<001F83E000706E3000C07C 780180F8780380F078070070000700700007007000070070000700700007007000070070000700 700007007000FFFFFFC00700700007007000070070000700700007007000070070000700700007 007000070070000700700007007000070070000700700007007000070070000700700007007000 07007000070078007FE3FF801D2380A21C>11 D<001FC0000070200000C0100001803800038078 00070078000700300007000000070000000700000007000000070000000700000007000000FFFF F80007007800070038000700380007003800070038000700380007003800070038000700380007 003800070038000700380007003800070038000700380007003800070038000700380007003800 7FE1FF80192380A21B>I<001FD8000070380000C0780001807800038078000700380007003800 07003800070038000700380007003800070038000700380007003800FFFFF80007003800070038 000700380007003800070038000700380007003800070038000700380007003800070038000700 3800070038000700380007003800070038000700380007003800070038007FF3FF80192380A21B >I<000FC07F00007031C08000E00B004001801E00E003803E01E007003C01E007001C00C00700 1C000007001C000007001C000007001C000007001C000007001C000007001C0000FFFFFFFFE007 001C01E007001C00E007001C00E007001C00E007001C00E007001C00E007001C00E007001C00E0 07001C00E007001C00E007001C00E007001C00E007001C00E007001C00E007001C00E007001C00 E007001C00E007001C00E007001C00E07FF1FFCFFE272380A229>I<7038F87CFC7EFC7E743A04 020402040204020804080410081008201040200F0F7EA218>34 D<70F8FCFC7404040404080810 102040060F7CA20E>39 D<00200040008001000300060004000C000C0018001800300030003000 7000600060006000E000E000E000E000E000E000E000E000E000E000E000E000E000E000600060 0060007000300030003000180018000C000C0004000600030001000080004000200B327CA413> I<800040002000100018000C000400060006000300030001800180018001C000C000C000C000E0 00E000E000E000E000E000E000E000E000E000E000E000E000E000C000C000C001C00180018001 80030003000600060004000C00180010002000400080000B327DA413>I<000180000001800000 018000000180000001800000018000000180000001800000018000000180000001800000018000 00018000000180000001800000018000FFFFFFFEFFFFFFFE000180000001800000018000000180 000001800000018000000180000001800000018000000180000001800000018000000180000001 800000018000000180001F227D9C26>43 D<70F8FCFC7404040404080810102040060F7C840E> II<70F8F8F87005057C840E>I<00008000018000018000030000030000 0300000600000600000600000C00000C00000C0000180000180000180000300000300000300000 600000600000600000C00000C00000C00001800001800001800001800003000003000003000006 00000600000600000C00000C00000C000018000018000018000030000030000030000060000060 0000600000C00000C00000C0000011317DA418>I<01F000071C000C0600180300380380380380 7001C07001C07001C07001C0F001E0F001E0F001E0F001E0F001E0F001E0F001E0F001E0F001E0 F001E0F001E0F001E0F001E0F001E07001C07001C07001C07803C03803803803801C07000C0600 071C0001F00013227EA018>I<008003800F80F380038003800380038003800380038003800380 03800380038003800380038003800380038003800380038003800380038003800380038007C0FF FE0F217CA018>I<03F0000C1C001007002007804003C04003C08003E0F003E0F801E0F801E0F8 01E02003E00003E00003C00003C0000780000700000E00001C0000180000300000600000C00001 80000100000200200400200800201800603000403FFFC07FFFC0FFFFC013217EA018>I<03F800 0C1E001007002007804007C07807C07803C07807C03807C0000780000780000700000F00000E00 00380003F000001C00000F000007800007800003C00003C00003E02003E07003E0F803E0F803E0 F003C04003C0400780200780100F000C1C0003F00013227EA018>I<000200000600000E00000E 00001E00001E00002E00004E00004E00008E00008E00010E00020E00020E00040E00040E00080E 00100E00100E00200E00200E00400E00800E00FFFFF8000E00000E00000E00000E00000E00000E 00000E00001F0001FFF015217FA018>I<1000801E07001FFF001FFE001FF80013E00010000010 000010000010000010000010000010F800130E001407001803801003800001C00001C00001E000 01E00001E00001E07001E0F001E0F001E0E001C08001C04003C04003802007001006000C1C0003 F00013227EA018>I<007E0001C1000300800601C00E03C01C03C0180180380000380000780000 700000700000F0F800F30C00F40600F40300F80380F801C0F001C0F001E0F001E0F001E0F001E0 F001E07001E07001E07001E03801C03801C01803801C03000C0600070C0001F00013227EA018> I<4000006000007FFFE07FFFC07FFFC0400080C001008001008002008002000004000008000008 0000100000300000200000600000600000600000E00000C00000C00001C00001C00001C00001C0 0003C00003C00003C00003C00003C00003C00003C00003C00001800013237DA118>I<01F80006 0E000803001001802001802000C06000C06000C06000C07000C07801803E01003F02001FC4000F F80003F80003FC00067F00083F80100F803007C06001C06000E0C000E0C00060C00060C00060C0 00606000406000C03000801803000E0E0003F00013227EA018>I<01F000060C000C0600180700 380380700380700380F001C0F001C0F001C0F001E0F001E0F001E0F001E0F001E07001E07003E0 3803E01805E00C05E00619E003E1E00001C00001C00001C0000380000380300300780700780600 700C002018001030000FC00013227EA018>I<70F8F8F870000000000000000000000070F8F8F8 7005157C940E>I61 D<07E01838201C400E800FF00FF00F F00F000F000E001C00380030006000C000C0008000800180010001000100010001000100000000 00000000000000038007C007C007C0038010237DA217>63 D<0001800000018000000180000003 C0000003C0000003C0000005E0000005E000000DF0000008F0000008F0000010F8000010780000 10780000203C0000203C0000203C0000401E0000401E0000401E0000800F0000800F0000FFFF00 0100078001000780030007C0020003C0020003C0040003E0040001E0040001E00C0000F00C0000 F03E0001F8FF800FFF20237EA225>65 DI<0007E0100038183000E0063001C00170038000F0070000F00E0000701E0000701C0000 303C0000303C0000307C0000107800001078000010F8000000F8000000F8000000F8000000F800 0000F8000000F8000000F800000078000000780000107C0000103C0000103C0000101C0000201E 0000200E000040070000400380008001C0010000E0020000381C000007E0001C247DA223>IIII<00 07F008003C0C1800E0021801C001B8038000F8070000780F0000381E0000381E0000183C000018 3C0000187C0000087800000878000008F8000000F8000000F8000000F8000000F8000000F80000 00F8000000F8001FFF780000F8780000787C0000783C0000783C0000781E0000781E0000780F00 007807000078038000B801C000B800E00318003C0C080007F00020247DA226>III<03FFF0001F00000F00000F00000F00000F00000F0000 0F00000F00000F00000F00000F00000F00000F00000F00000F00000F00000F00000F00000F0000 0F00000F00000F00000F00000F00000F00700F00F80F00F80F00F80E00F01E00401C0020380018 700007C00014237EA119>IIIII<000FE00000783C0000E00E 0003C00780078003C00F0001E00E0000E01E0000F03C0000783C0000787C00007C7C00007C7800 003C7800003CF800003EF800003EF800003EF800003EF800003EF800003EF800003EF800003EF8 00003E7800003C7C00007C7C00007C3C0000783E0000F81E0000F00F0001E00F0001E0078003C0 03C0078000E00E0000783C00000FE0001F247DA226>II<000FE00000783C0000E00E0003C00780078003C00F0001E00E0000E01E 0000F03E0000F83C0000787C00007C7C00007C7800003C7800003CF800003EF800003EF800003E F800003EF800003EF800003EF800003EF800003EF800003E7800003C7C00007C7C00007C3C0000 783C0000781E0380F00E0420E00F0801E0078813C003C8178000E80E00007C3C02000FEC020000 0C0200000C0200000E0600000F0E000007FC000007FC000007F8000003F8000001E01F2D7DA226 >II<03F0200C0C601802603001 E07000E0600060E00060E00060E00020E00020E00020F00000F000007800007F00003FF0001FFE 000FFF0003FF80003FC00007E00001E00000F00000F0000070800070800070800070800070C000 60C00060E000C0F000C0C80180C6070081FC0014247DA21B>I<7FFFFFF8780780786007801840 0780084007800840078008C007800C800780048007800480078004800780040007800000078000 000780000007800000078000000780000007800000078000000780000007800000078000000780 00000780000007800000078000000780000007800000078000000780000007800000078000000F C00003FFFF001E227EA123>I86 DI<7FF807FF0007E001F80003C000E00003 E000C00001E000800000F001000000F80300000078020000007C040000003E0C0000001E080000 001F100000000FB000000007A000000007C000000003E000000001E000000001F000000003F800 00000278000000047C0000000C3E000000081E000000101F000000300F80000020078000004007 C00000C003E000008001E000010001F000030000F000070000F8001F8001FC00FFE007FFC02222 7FA125>I91 D<08041008201020104020402080408040 80408040B85CFC7EFC7E7C3E381C0F0F7AA218>II<0F E0001838003C0C003C0E0018070000070000070000070000FF0007C7001E07003C070078070070 0700F00708F00708F00708F00F087817083C23900FC1E015157E9418>97 D<0E0000FE00001E00000E00000E00000E00000E00000E00000E00000E00000E00000E00000E00 000E00000E1F000E61C00E80600F00300E00380E003C0E001C0E001E0E001E0E001E0E001E0E00 1E0E001E0E001E0E001C0E003C0E00380F00700C80600C41C0083F0017237FA21B>I<01FE0007 03000C07801C0780380300780000700000F00000F00000F00000F00000F00000F00000F0000070 00007800403800401C00800C010007060001F80012157E9416>I<0000E0000FE00001E00000E0 0000E00000E00000E00000E00000E00000E00000E00000E00000E00000E001F8E00704E00C02E0 1C01E03800E07800E07000E0F000E0F000E0F000E0F000E0F000E0F000E0F000E07000E07800E0 3800E01801E00C02E0070CF001F0FE17237EA21B>I<01FC000707000C03801C01C03801C07801 E07000E0F000E0FFFFE0F00000F00000F00000F00000F000007000007800203800201C00400E00 8007030000FC0013157F9416>I<003C00C6018F038F030F070007000700070007000700070007 000700FFF807000700070007000700070007000700070007000700070007000700070007000700 070007807FF8102380A20F>I<00007001F198071E180E0E181C07001C07003C07803C07803C07 803C07801C07001C07000E0E000F1C0019F0001000001000001800001800001FFE000FFFC00FFF E03800F0600030400018C00018C00018C000186000306000303800E00E038003FE0015217F9518 >I<0E0000FE00001E00000E00000E00000E00000E00000E00000E00000E00000E00000E00000E 00000E00000E1F800E60C00E80E00F00700F00700E00700E00700E00700E00700E00700E00700E 00700E00700E00700E00700E00700E00700E00700E00700E0070FFE7FF18237FA21B>I<1C001E 003E001E001C00000000000000000000000000000000000E00FE001E000E000E000E000E000E00 0E000E000E000E000E000E000E000E000E000E000E000E00FFC00A227FA10E>I<01C003E003E0 03E001C00000000000000000000000000000000001E00FE001E000E000E000E000E000E000E000 E000E000E000E000E000E000E000E000E000E000E000E000E000E000E000E000E060E0F0C0F180 61803E000B2C82A10F>I<0E0000FE00001E00000E00000E00000E00000E00000E00000E00000E 00000E00000E00000E00000E00000E03FC0E01F00E01C00E01800E02000E04000E08000E10000E 38000EF8000F1C000E1E000E0E000E07000E07800E03C00E01C00E01E00E00F00E00F8FFE3FE17 237FA21A>I<0E00FE001E000E000E000E000E000E000E000E000E000E000E000E000E000E000E 000E000E000E000E000E000E000E000E000E000E000E000E000E000E000E000E000E00FFE00B23 7FA20E>I<0E1FC07F00FE60E183801E807201C00F003C00E00F003C00E00E003800E00E003800 E00E003800E00E003800E00E003800E00E003800E00E003800E00E003800E00E003800E00E0038 00E00E003800E00E003800E00E003800E00E003800E00E003800E0FFE3FF8FFE27157F942A>I< 0E1F80FE60C01E80E00F00700F00700E00700E00700E00700E00700E00700E00700E00700E0070 0E00700E00700E00700E00700E00700E00700E0070FFE7FF18157F941B>I<01FC000707000C01 801800C03800E0700070700070F00078F00078F00078F00078F00078F00078F000787000707800 F03800E01C01C00E038007070001FC0015157F9418>I<0E1F00FE61C00E80600F00700E00380E 003C0E001C0E001E0E001E0E001E0E001E0E001E0E001E0E001E0E003C0E003C0E00380F00700E 80E00E41C00E3F000E00000E00000E00000E00000E00000E00000E00000E00000E0000FFE00017 1F7F941B>I<01F8200704600E02601C01603801E07800E07800E0F000E0F000E0F000E0F000E0 F000E0F000E0F000E07000E07800E03801E01C01E00C02E0070CE001F0E00000E00000E00000E0 0000E00000E00000E00000E00000E00000E0000FFE171F7E941A>I<0E3CFE461E8F0F0F0F060F 000E000E000E000E000E000E000E000E000E000E000E000E000E000F00FFF010157F9413>I<0F 8830786018C018C008C008E008F0007F803FE00FF001F8003C801C800C800CC00CC008E018D030 8FC00E157E9413>I<02000200020002000600060006000E001E003E00FFF80E000E000E000E00 0E000E000E000E000E000E000E000E040E040E040E040E040E040708030801F00E1F7F9E13>I< 0E0070FE07F01E00F00E00700E00700E00700E00700E00700E00700E00700E00700E00700E0070 0E00700E00700E00700E00F00E00F006017003827800FC7F18157F941B>IIIII<3FFFC0380380300780200700600E00401C00403C0040380000700000 E00001E00001C0000380400700400F00400E00C01C0080380080780180700780FFFF8012157F94 16>III E /Fp 28 122 df<0001E0000003E000000FE000007FE0001FFFE000FFFFE000FFBFE000E03FE000003FE00000 3FE000003FE000003FE000003FE000003FE000003FE000003FE000003FE000003FE000003FE000 003FE000003FE000003FE000003FE000003FE000003FE000003FE000003FE000003FE000003FE0 00003FE000003FE000003FE000003FE000003FE000003FE000003FE000003FE000003FE000003F E000003FE000003FE000003FE000003FE0007FFFFFF07FFFFFF07FFFFFF01C2E7AAD29>49 D<003FF00001FFFE0007FFFF800FC07FE01E001FF03C000FF87F0007FC7F8007FEFFC007FEFFC0 03FEFFC003FFFFC003FF7F8003FF7F8003FF3F0003FF000003FF000003FE000003FE000007FC00 0007FC00000FF800000FF000001FE000001FC000003F8000007F000000FE000001F8000001F000 0003E00000078007000F0007001E0007003C000F0078000E00F0000E01C0001E03FFFFFE07FFFF FE0FFFFFFE1FFFFFFE3FFFFFFE7FFFFFFCFFFFFFFCFFFFFFFCFFFFFFFC202E7CAD29>I<000FFC 0000007FFF800001F01FE00003C00FF000070007F8000FE007FC000FF007FC001FF007FE001FF8 07FE001FF807FE001FF807FE001FF807FE000FF007FC0007E007FC00018007FC0000000FF80000 000FF00000001FE00000001FC00000007F8000001FFE0000001FFC0000001FFF800000001FF000 000007F800000003FC00000003FE00000003FF00000001FF80000001FF800E0001FFC03F8001FF C07FC001FFC07FC001FFC0FFE001FFC0FFE001FFC0FFE001FF80FFE001FF80FFC003FF007F8003 FF003F0003FE001F0007FC000FE01FF80007FFFFE00001FFFF8000001FFC0000222E7DAD29>I< 000003FF80018000003FFFF003800001FFFFFC0F800007FF007F1F80001FF8000FBF80003FE000 03FF8000FF800000FF8001FF0000007F8003FE0000003F8007FC0000003F8007FC0000001F800F F80000001F801FF80000000F801FF00000000F803FF000000007803FF000000007807FF0000000 07807FE000000007807FE000000000007FE00000000000FFE00000000000FFE00000000000FFE0 0000000000FFE00000000000FFE00000000000FFE00000000000FFE00000000000FFE000000000 00FFE000000000007FE000000000007FE000000000007FE000000000007FF000000003803FF000 000003803FF000000003801FF000000003801FF800000007800FF8000000070007FC0000000700 07FC0000000E0003FE0000001E0001FF0000003C0000FF8000007800003FE00000F000001FF800 03E0000007FF003F80000001FFFFFE000000003FFFF80000000003FF80000031317BB03C>67 D73 D<00000FFE0000000000FFFFE000000007FFFFFC0000001FFC07FF000000 3FE000FF800000FF80003FE00001FF00001FF00003FE00000FF80007FC000007FC0007FC000007 FC000FF8000003FE001FF8000003FF001FF0000001FF003FF0000001FF803FF0000001FF803FF0 000001FF807FE0000000FFC07FE0000000FFC07FE0000000FFC0FFE0000000FFE0FFE0000000FF E0FFE0000000FFE0FFE0000000FFE0FFE0000000FFE0FFE0000000FFE0FFE0000000FFE0FFE000 0000FFE0FFE0000000FFE0FFE0000000FFE0FFE0000000FFE07FE0000000FFC07FE0000000FFC0 7FF0000001FFC07FF0000001FFC03FF0000001FF803FF0000001FF801FF8000003FF001FF80000 03FF000FFC000007FE000FFC000007FE0007FE00000FFC0003FF00001FF80001FF80003FF00000 FFC0007FE000003FE000FF8000001FFC07FF00000007FFFFFC00000000FFFFE0000000000FFE00 000033317BB03E>79 DI82 D<3FFFFFFFFFFF003FFFFFFFFFFF003FFFFFFFFFFF003FE00FFC01FF007F00 0FFC003F807E000FFC001F807C000FFC000F8078000FFC00078078000FFC00078070000FFC0003 8070000FFC00038070000FFC00038070000FFC000380E0000FFC0001C0E0000FFC0001C0E0000F FC0001C0E0000FFC0001C000000FFC00000000000FFC00000000000FFC00000000000FFC000000 00000FFC00000000000FFC00000000000FFC00000000000FFC00000000000FFC00000000000FFC 00000000000FFC00000000000FFC00000000000FFC00000000000FFC00000000000FFC00000000 000FFC00000000000FFC00000000000FFC00000000000FFC00000000000FFC00000000000FFC00 000000000FFC00000000000FFC00000000000FFC00000000000FFC00000000000FFC0000000000 0FFC00000000000FFC000000007FFFFFFF8000007FFFFFFF8000007FFFFFFF800032307DAF39> 84 D87 D<007FF8000003FFFF000007FFFFC0000FE01FE0001FF007F0001FF003F8001FF003FC001FF001 FE000FE001FE0007C001FE00010001FE00000001FE00000001FE000001FFFE00003FFFFE0001FF F1FE0007FE01FE000FF001FE001FC001FE003F8001FE007F8001FE00FF0001FE00FF0001FE00FF 0001FE00FF0001FE00FF0003FE007F8003FE007FC00EFE003FF03CFF000FFFF87FF807FFF03FF8 00FF800FF825207E9F28>97 D<0007FF00007FFFE000FFFFF003FC03F807F007FC0FE007FC1FE0 07FC3FC007FC3FC003F87FC001F07F8000407F800000FF800000FF800000FF800000FF800000FF 800000FF800000FF800000FF8000007F8000007FC000007FC000003FC0000E3FE0000E1FE0001C 0FF0001C07F8007803FF01F000FFFFE0007FFF800007FC001F207D9F25>99 D<00000007E0000003FFE0000003FFE0000003FFE00000003FE00000001FE00000001FE0000000 1FE00000001FE00000001FE00000001FE00000001FE00000001FE00000001FE00000001FE00000 001FE00000001FE00000001FE0000FF81FE0007FFF1FE001FFFFDFE003FE03FFE007F800FFE00F E0003FE01FE0001FE03FC0001FE03FC0001FE07F80001FE07F80001FE07F80001FE0FF80001FE0 FF80001FE0FF80001FE0FF80001FE0FF80001FE0FF80001FE0FF80001FE0FF80001FE07F80001F E07F80001FE07F80001FE03FC0001FE03FC0001FE01FC0003FE00FE0007FE007F001FFE003FC07 DFF001FFFF9FFF007FFE1FFF000FF01FFF28327DB12E>I<0007FC0000003FFF800000FFFFE000 03FC07F00007F801F8000FE000FC001FE0007E003FC0007E003FC0003F007FC0003F007F80003F 007F80003F80FF80003F80FF80003F80FFFFFFFF80FFFFFFFF80FFFFFFFF80FF80000000FF8000 0000FF800000007F800000007F800000003FC00000003FC00003801FC00003801FE00007800FF0 000F0007F8001E0003FE00FC0000FFFFF800003FFFE0000003FF000021207E9F26>I<0000FF00 0007FFC0001FFFE0003FC7F0007F0FF800FE0FF801FE0FF801FC0FF803FC07F003FC03E003FC01 C003FC000003FC000003FC000003FC000003FC000003FC000003FC0000FFFFF800FFFFF800FFFF F80003FC000003FC000003FC000003FC000003FC000003FC000003FC000003FC000003FC000003 FC000003FC000003FC000003FC000003FC000003FC000003FC000003FC000003FC000003FC0000 03FC000003FC000003FC000003FC000003FC000003FC000003FC00007FFFF0007FFFF0007FFFF0 001D327EB119>I<01F800000000FFF800000000FFF800000000FFF8000000000FF80000000007 F80000000007F80000000007F80000000007F80000000007F80000000007F80000000007F80000 000007F80000000007F80000000007F80000000007F80000000007F80000000007F80000000007 F807F8000007F83FFF000007F87FFF800007F8F03FC00007F9C01FE00007FB000FE00007FE000F F00007FE000FF00007FC000FF00007FC000FF00007F8000FF00007F8000FF00007F8000FF00007 F8000FF00007F8000FF00007F8000FF00007F8000FF00007F8000FF00007F8000FF00007F8000F F00007F8000FF00007F8000FF00007F8000FF00007F8000FF00007F8000FF00007F8000FF00007 F8000FF00007F8000FF00007F8000FF000FFFFC1FFFF80FFFFC1FFFF80FFFFC1FFFF8029327DB1 2E>104 D<03C0000FF0000FF0001FF8001FF8001FFC001FF8001FF8000FF0000FF00003C00000 000000000000000000000000000000000000000000000001F800FFF800FFF800FFF8000FF80007 F80007F80007F80007F80007F80007F80007F80007F80007F80007F80007F80007F80007F80007 F80007F80007F80007F80007F80007F80007F80007F80007F80007F80007F800FFFF80FFFF80FF FF8011337DB217>I<01F800FFF800FFF800FFF8000FF80007F80007F80007F80007F80007F800 07F80007F80007F80007F80007F80007F80007F80007F80007F80007F80007F80007F80007F800 07F80007F80007F80007F80007F80007F80007F80007F80007F80007F80007F80007F80007F800 07F80007F80007F80007F80007F80007F80007F80007F80007F80007F80007F800FFFFC0FFFFC0 FFFFC012327DB117>108 D<03F007F8000FF000FFF03FFF007FFE00FFF07FFF80FFFF00FFF0F0 3FC1E07F800FF1C01FE3803FC007F3000FE6001FC007F6000FFC001FE007FE000FFC001FE007FC 000FF8001FE007FC000FF8001FE007F8000FF0001FE007F8000FF0001FE007F8000FF0001FE007 F8000FF0001FE007F8000FF0001FE007F8000FF0001FE007F8000FF0001FE007F8000FF0001FE0 07F8000FF0001FE007F8000FF0001FE007F8000FF0001FE007F8000FF0001FE007F8000FF0001F E007F8000FF0001FE007F8000FF0001FE007F8000FF0001FE007F8000FF0001FE007F8000FF000 1FE007F8000FF0001FE0FFFFC1FFFF83FFFFFFFFC1FFFF83FFFFFFFFC1FFFF83FFFF40207D9F45 >I<03F007F80000FFF03FFF0000FFF07FFF8000FFF0F03FC0000FF1C01FE00007F3000FE00007 F6000FF00007FE000FF00007FC000FF00007FC000FF00007F8000FF00007F8000FF00007F8000F F00007F8000FF00007F8000FF00007F8000FF00007F8000FF00007F8000FF00007F8000FF00007 F8000FF00007F8000FF00007F8000FF00007F8000FF00007F8000FF00007F8000FF00007F8000F F00007F8000FF00007F8000FF00007F8000FF000FFFFC1FFFF80FFFFC1FFFF80FFFFC1FFFF8029 207D9F2E>I<0007FE0000003FFFC00000FFFFF00003FC03FC0007F000FE000FE0007F001FC000 3F803FC0003FC03FC0003FC07F80001FE07F80001FE07F80001FE0FF80001FF0FF80001FF0FF80 001FF0FF80001FF0FF80001FF0FF80001FF0FF80001FF0FF80001FF07F80001FE07F80001FE07F 80001FE03FC0003FC03FC0003FC01FE0007F800FE0007F0007F801FE0003FE07FC0001FFFFF800 003FFFC0000007FE000024207E9F29>I<03F03F00FFF07FC0FFF1FFE0FFF3C7F00FF38FF807F7 0FF807F60FF807FE0FF807FC07F007FC03E007FC008007F8000007F8000007F8000007F8000007 F8000007F8000007F8000007F8000007F8000007F8000007F8000007F8000007F8000007F80000 07F8000007F8000007F8000007F80000FFFFE000FFFFE000FFFFE0001D207E9F22>114 D<00FF870007FFEF001FFFFF003F007F003C001F0078000F00F8000700F8000700F8000700FC00 0700FF000000FFF800007FFFC0003FFFF0003FFFFC000FFFFE0007FFFF0001FFFF80001FFF8000 00FFC000001FC060000FC0E00007C0E00007C0F00007C0F8000780F8000F80FE000F00FF803E00 FFFFFC00F3FFF800C07FC0001A207D9F21>I<0038000038000038000038000038000078000078 0000780000F80000F80001F80003F80007F8001FF800FFFFFEFFFFFEFFFFFE07F80007F80007F8 0007F80007F80007F80007F80007F80007F80007F80007F80007F80007F80007F80007F80007F8 0007F80707F80707F80707F80707F80707F80707F80703F80E03FC0E01FE1C00FFF8007FF0000F E0182E7EAD20>I<01F80003F000FFF801FFF000FFF801FFF000FFF801FFF0000FF8001FF00007 F8000FF00007F8000FF00007F8000FF00007F8000FF00007F8000FF00007F8000FF00007F8000F F00007F8000FF00007F8000FF00007F8000FF00007F8000FF00007F8000FF00007F8000FF00007 F8000FF00007F8000FF00007F8000FF00007F8000FF00007F8000FF00007F8000FF00007F8001F F00007F8001FF00003F8003FF00003F8006FF00001FE03CFF80000FFFF8FFF80007FFF0FFF8000 0FFC0FFF8029207D9F2E>III121 D E /Fq 1 71 df<00007FFFE00003FFFFF0000E3801E000303800C0006078000000E078000001C07000000180 7000000000F000000000F000000000E000000000E000000001E000000001C000000001C0000000 03FFF8000003FFF000000380000000070000000007000000000F000000000E000000000E000000 001C000000001C0000000038000000003800000030700000007870000000FCC00000007F800000 003E0000000024207F9E21>70 D E /Fr 5 120 df<0000780003F80000700000700000700000 700000E00000E00000E00000E00001C00001C000F1C00389C00707800E03801C03803C03803807 00780700780700780700F00E00F00E00F00E00F00E20F01C40F01C40703C40705C40308C800F07 0015207C9F17>100 D<01E0000FE00001C00001C00001C00001C0000380000380000380000380 00070000070000071E000763000E81800F01C00E01C00E01C01C03801C03801C03801C03803807 00380700380700380E10700E20700C20701C20700C40E00CC060070014207D9F17>104 D<00C001E001E001C000000000000000000000000000000E003300230043804300470087000E00 0E000E001C001C001C003840388030807080310033001C000B1F7C9E0E>I<018001C003800380 0380038007000700FFF007000E000E000E000E001C001C001C001C003800380038003820704070 407080708031001E000C1C7C9B0F>116 D<0E00C1C03300E3C02301C3E04381C1E04301C0E047 01C060870380400E0380400E0380400E0380401C0700801C0700801C0700801C0701001C070100 1C0602001C0F02000C0F04000E13080003E1F0001B147C931E>119 D E /Fs 41 122 df<003F0000E0C001C0C00381E00701E00701E00700000700000700000700000700 00070000FFFFE00700E00700E00700E00700E00700E00700E00700E00700E00700E00700E00700 E00700E00700E00700E00700E00700E00700E00700E07FC3FE1720809F19>12 D<0020004000800100020006000C000C00180018003000300030007000600060006000E000E000 E000E000E000E000E000E000E000E000E000E0006000600060007000300030003000180018000C 000C000600020001000080004000200B2E7DA112>40 D<800040002000100008000C0006000600 0300030001800180018001C000C000C000C000E000E000E000E000E000E000E000E000E000E000 E000E000C000C000C001C001800180018003000300060006000C00080010002000400080000B2E 7DA112>I<70F8FCFC74040404080810102040060E7C840D>44 D<70F8F8F87005057C840D>46 D<70F8F8F8700000000000000000000070F8F8F87005147C930D>58 D<7FFFFFE0FFFFFFF00000 000000000000000000000000000000000000000000000000000000000000FFFFFFF07FFFFFE01C 0C7D9023>61 D<000100000003800000038000000380000007C0000007C0000007C0000009E000 0009E0000009E0000010F0000010F0000010F00000207800002078000020780000403C0000403C 0000403C0000801E0000801E0000FFFE0001000F0001000F0001000F0002000780020007800200 0780040003C00E0003C01F0007E0FFC03FFE1F207F9F22>65 D<000FC040007030C001C009C003 8005C0070003C00E0001C01E0000C01C0000C03C0000C07C0000407C00004078000040F8000000 F8000000F8000000F8000000F8000000F8000000F8000000F8000000F8000000780000007C0000 407C0000403C0000401C0000401E0000800E000080070001000380020001C0040000703800000F C0001A217D9F21>67 D69 DI< FFFC0FC00780078007800780078007800780078007800780078007800780078007800780078007 800780078007800780078007800780078007800FC0FFFC0E1F7F9E10>73 D78 D80 D<07E0800C1980100780300380600180600180E00180E00080E00080E00080F00000F000007800 007F00003FF0001FFC000FFE0003FF00001F800007800003C00003C00001C08001C08001C08001 C08001C0C00180C00380E00300F00600CE0C0081F80012217D9F19>83 D<7FFFFFE0780F01E060 0F0060400F0020400F0020C00F0030800F0010800F0010800F0010800F0010000F0000000F0000 000F0000000F0000000F0000000F0000000F0000000F0000000F0000000F0000000F0000000F00 00000F0000000F0000000F0000000F0000000F0000000F0000000F0000001F800007FFFE001C1F 7E9E21>I<7FF83FF80FE00FC007C0070003C0020001E0040001F00C0000F0080000781000007C 1000003C2000003E4000001E4000000F8000000F8000000780000003C0000007E0000005E00000 09F0000018F8000010780000207C0000603C0000401E0000801F0001800F0001000780020007C0 070003C01F8007E0FFE01FFE1F1F7F9E22>88 D<1FE000303000781800781C00300E00000E0000 0E00000E0000FE00078E001E0E00380E00780E00F00E10F00E10F00E10F01E10781E103867200F 83C014147E9317>97 D<0E0000FE00000E00000E00000E00000E00000E00000E00000E00000E00 000E00000E00000E3E000EC3800F01C00F00E00E00E00E00700E00700E00780E00780E00780E00 780E00780E00780E00700E00700E00E00F00E00D01C00CC300083E0015207F9F19>I<03F80E0C 1C1E381E380C70007000F000F000F000F000F000F00070007000380138011C020E0C03F010147E 9314>I<000380003F800003800003800003800003800003800003800003800003800003800003 8003E380061B801C0780380380380380700380700380F00380F00380F00380F00380F00380F003 807003807003803803803807801C07800E1B8003E3F815207E9F19>I<03F0000E1C001C0E0038 0700380700700700700380F00380F00380FFFF80F00000F00000F0000070000070000038008018 00800C010007060001F80011147F9314>I<007C00C6018F038F07060700070007000700070007 000700FFF007000700070007000700070007000700070007000700070007000700070007000700 07007FF01020809F0E>I<0000E003E3300E3C301C1C30380E00780F00780F00780F00780F0078 0F00380E001C1C001E380033E0002000002000003000003000003FFE001FFF800FFFC03001E060 0070C00030C00030C00030C000306000603000C01C038003FC00141F7F9417>I<0E0000FE0000 0E00000E00000E00000E00000E00000E00000E00000E00000E00000E00000E3E000E43000E8180 0F01C00F01C00E01C00E01C00E01C00E01C00E01C00E01C00E01C00E01C00E01C00E01C00E01C0 0E01C00E01C00E01C0FFE7FC16207F9F19>I<1C001E003E001E001C0000000000000000000000 00000E007E000E000E000E000E000E000E000E000E000E000E000E000E000E000E000E000E000E 00FFC00A1F809E0C>I<0E0000FE00000E00000E00000E00000E00000E00000E00000E00000E00 000E00000E00000E0FF00E03C00E03000E02000E04000E08000E10000E30000E70000EF8000F38 000E1C000E1E000E0E000E07000E07800E03800E03C00E03E0FFCFF815207F9F18>107 D<0E00FE000E000E000E000E000E000E000E000E000E000E000E000E000E000E000E000E000E00 0E000E000E000E000E000E000E000E000E000E000E000E00FFE00B20809F0C>I<0E1F01F000FE 618618000E81C81C000F00F00E000F00F00E000E00E00E000E00E00E000E00E00E000E00E00E00 0E00E00E000E00E00E000E00E00E000E00E00E000E00E00E000E00E00E000E00E00E000E00E00E 000E00E00E000E00E00E00FFE7FE7FE023147F9326>I<0E3E00FE43000E81800F01C00F01C00E 01C00E01C00E01C00E01C00E01C00E01C00E01C00E01C00E01C00E01C00E01C00E01C00E01C00E 01C0FFE7FC16147F9319>I<01F800070E001C03803801C03801C07000E07000E0F000F0F000F0 F000F0F000F0F000F0F000F07000E07000E03801C03801C01C0380070E0001F80014147F9317> I<0E3E00FEC3800F01C00F00E00E00E00E00F00E00700E00780E00780E00780E00780E00780E00 780E00700E00F00E00E00F01E00F01C00EC3000E3E000E00000E00000E00000E00000E00000E00 000E00000E0000FFE000151D7F9319>I<03E0800619801C05803C0780380380780380700380F0 0380F00380F00380F00380F00380F003807003807803803803803807801C0B800E138003E38000 0380000380000380000380000380000380000380000380003FF8151D7E9318>I<0E78FE8C0F1E 0F1E0F0C0E000E000E000E000E000E000E000E000E000E000E000E000E000E00FFE00F147F9312 >I<1F9030704030C010C010C010E00078007F803FE00FF00070803880188018C018C018E030D0 608F800D147E9312>I<020002000200060006000E000E003E00FFF80E000E000E000E000E000E 000E000E000E000E000E000E080E080E080E080E080610031001E00D1C7F9B12>I<0E01C0FE1F C00E01C00E01C00E01C00E01C00E01C00E01C00E01C00E01C00E01C00E01C00E01C00E01C00E01 C00E01C00E03C00603C0030DC001F1FC16147F9319>III<7FC3FC0F01E00701C007018003810001C200 00E40000EC00007800003800003C00007C00004E000087000107000303800201C00601E01E01E0 FF07FE1714809318>II E /Ft 7 117 df<0000E000000000E000000001F000000001F000000001F000000003F800000003F80000 0006FC00000006FC0000000EFE0000000C7E0000000C7E000000183F000000183F000000303F80 0000301F800000701FC00000600FC00000600FC00000C007E00000FFFFE00001FFFFF000018003 F000018003F000030001F800030001F800060001FC00060000FC000E0000FE00FFE00FFFE0FFE0 0FFFE0231F7E9E28>65 D<07FC001FFF003F0F803F07C03F03E03F03E00C03E00003E0007FE007 FBE01F03E03C03E07C03E0F803E0F803E0F803E0FC05E07E0DE03FF8FE0FE07E17147F9319>97 DI<01FE0007FF801F0FC03E0FC03E 0FC07C0FC07C0300FC0000FC0000FC0000FC0000FC0000FC00007C00007E00003E00603F00C01F 81C007FF0001FC0013147E9317>I114 D<0FE63FFE701E600EE006E006F800FFC07FF83FFC1FFE03FE001FC007C007E007F0 06F81EFFFCC7F010147E9315>I<01800180018003800380038007800F803F80FFFCFFFC0F800F 800F800F800F800F800F800F800F800F800F860F860F860F860F8607CC03F801F00F1D7F9C14> I E /Fu 40 122 df<78FCFCFEFE7A02020202040404081010204007127B8511>44 D<00100000700001F0000FF000FEF000F0F00000F00000F00000F00000F00000F00000F00000F0 0000F00000F00000F00000F00000F00000F00000F00000F00000F00000F00000F00000F00000F0 0000F00000F00000F00000F00000F00000F00000F00000F00000F00000F00000F00001F8007FFF E07FFFE013287BA71E>49 D<007F000003FFC0000701F0000C00F80010007C001C007C003E007E 003E003E003E003E001E003E000C007E0000007C0000007C00000078000000F0000000E0000001 C0000007000000FF00000001E0000000F0000000780000003C0000003E0000001F0000001F0000 001F8000001F8030001F8078001F80FC001F80FC001F80FC001F00F8001F0040003F0040003E00 30007C001800F8000F01F00003FFC000007F000019297EA71E>51 D<00006000000060000000E0 000001E0000001E0000003E0000003E0000005E0000009E0000009E0000011E0000021E0000021 E0000041E0000081E0000081E0000101E0000201E0000201E0000401E0000801E0000801E00010 01E0003001E0002001E0004001E000C001E000FFFFFF80FFFFFF800001E0000001E0000001E000 0001E0000001E0000001E0000001E0000001E0000003F000007FFF80007FFF8019287EA71E>I< 1800181F00F01FFFE01FFFC01FFF801FFF0011F800100000100000100000100000100000100000 100000100000107E001183801600C01800E010007000007800003C00003C00003C00003E00003E 00003E70003EF8003EF8003EF8003EF8003C80003C40007C4000782000783000F01801E00E07C0 07FF0001FC0017297DA71E>I<007F000001FFC0000381F000060078000C003C001C001C001800 0E0038000E0038000E0038000E003C000E003C000E003E001C001F8018001FC038000FF0600007 F8C00003FF800001FF0000007FC00000FFE000030FF8000603FC001C01FE0038007E0030003F00 70000F0070000780E0000780E0000380E0000380E0000380E0000380F000030070000700780006 0038000C001E0038000F80F00003FFE000007F000019297EA71E>56 D<00001800000000180000 000018000000003C000000003C000000003C000000007E000000007E00000000FF000000009F00 0000009F000000011F800000010F800000010F8000000207C000000207C000000207C000000403 E000000403E000000403E000000801F000000801F000001801F800001000F800001000F8000020 00FC000020007C00003FFFFC00007FFFFE000040003E000040003E000080001F000080001F0000 80001F000100000F800100000F800100000F8002000007C007000007C01F80000FE0FFF000FFFF FFF000FFFF282A7EA92D>65 D<0000FF00100007FFE030001FC07830003E000C7000F80006F001 F00003F003E00001F007C00000F00F800000700F800000701F000000303F000000303E00000030 3E000000107E000000107E000000107C00000000FC00000000FC00000000FC00000000FC000000 00FC00000000FC00000000FC00000000FC00000000FC000000007C000000007E000000007E0000 00103E000000103E000000103F000000101F000000200F800000200F8000006007C000004003E0 00008001F000018000F8000300003E000E00001FC038000007FFE0000000FF8000242B7DA92B> 67 DI72 DI<03FFFF03FFFF0007E00003E00003E00003E00003E00003E000 03E00003E00003E00003E00003E00003E00003E00003E00003E00003E00003E00003E00003E000 03E00003E00003E00003E00003E00003E00003E00003E00003E00003E03003E07803E0FC03E0FC 03E0FC03C0F807C0400780200F00300E000C3C0003F000182A7DA81F>I78 D80 D82 D<00FE010003FF83000F81E3001E0037003C001F0038000F0078 00070070000700F0000300F0000300F0000300F0000100F8000100F8000100FC0000007C000000 7F0000003FE000001FFF00000FFFE00007FFF80003FFFC00007FFE000007FF0000007F0000001F 8000000F80000007C0000007C0800003C0800003C0800003C0800003C0C00003C0C0000380C000 0380E0000780F0000700F8000E00EE001C00C3C07800C1FFF000803FC0001A2B7DA921>I85 D 89 D<01FC00000E0780001001C0003C00E0003E00F0003E0078001C0078000800780000007800 0000780000007800007FF80003E078000F8078001F0078003E0078007C00780078007820F80078 20F8007820F8007820F800F8207C00F8203C013C401F063FC007F80F001B1A7E991E>97 D<007F8001C0700780080F003C1E007C3C007C3C00387C0010780000F80000F80000F80000F800 00F80000F80000F80000F800007800007C00003C00043C00041E00080F001007802001C0C0007F 00161A7E991B>99 D<00000F000001FF000001FF0000001F0000000F0000000F0000000F000000 0F0000000F0000000F0000000F0000000F0000000F0000000F0000000F0000000F00003F0F0001 C0CF0003802F000F001F001E001F001C000F003C000F007C000F0078000F0078000F00F8000F00 F8000F00F8000F00F8000F00F8000F00F8000F00F8000F0078000F0078000F003C000F003C000F 001E001F000E002F0007004F8001C18FF8007E0FF81D2A7EA921>I<007E0003C3800700E00E00 F01C00703C00783C003878003C78003CF8003CF8003CFFFFFCF80000F80000F80000F80000F800 007800007C00003C00043C00041E00080E001007002001C0C0007F00161A7E991B>I<001F0000 70C000E1E001C3E003C3E00381C007808007800007800007800007800007800007800007800007 8000078000FFFE00FFFE0007800007800007800007800007800007800007800007800007800007 800007800007800007800007800007800007800007800007800007800007800007800007C000FF FE00FFFE00132A7FA912>I<0000078001FC1840070721C00E03C1C01E03C0803C01E0003C01E0 007C01F0007C01F0007C01F0007C01F0007C01F0003C01E0003C01E0001E03C0000E0380001707 000011FC0000300000003000000030000000380000001C0000001FFFC0000FFFF80007FFFC001C 003E0030000F007000070060000380E0000380E0000380E0000380E00003807000070070000700 38000E000C0018000780F00000FF80001A287E9A1E>I<07800000FF800000FF8000000F800000 078000000780000007800000078000000780000007800000078000000780000007800000078000 0007800000078000000783F800078C1C0007900E0007A0070007A0078007C0078007C007800780 078007800780078007800780078007800780078007800780078007800780078007800780078007 800780078007800780078007800780078007800780078007800780FFFCFFFCFFFCFFFC1E2A7FA9 21>I<07000F801F801F800F80070000000000000000000000000000000000000007807F807F80 0F8007800780078007800780078007800780078007800780078007800780078007800780078007 800780FFF8FFF80D297FA811>I<007800FC00FC00FC00FC007800000000000000000000000000 0000000000007C07FC07FC007C003C003C003C003C003C003C003C003C003C003C003C003C003C 003C003C003C003C003C003C003C003C003C003C003C003C003C003C003C7038F838F870F07060 C01F800E3582A812>I<07800000FF800000FF8000000F80000007800000078000000780000007 800000078000000780000007800000078000000780000007800000078000000780000007807FF0 07807FF007801F8007801C00078018000780200007804000078080000781000007820000078700 00079F800007A7800007C7C0000783E0000781E0000781F0000780F8000780780007807C000780 3E0007801E0007801F0007801F80FFFC7FF8FFFC7FF81D2A7FA920>I<0780FF80FF800F800780 078007800780078007800780078007800780078007800780078007800780078007800780078007 80078007800780078007800780078007800780078007800780078007800780FFFCFFFC0E2A7FA9 11>I<0781F800FC00FF860E030700FF98070C03800FA0079003C007A003D001E007C003E001E0 07C003E001E0078003C001E0078003C001E0078003C001E0078003C001E0078003C001E0078003 C001E0078003C001E0078003C001E0078003C001E0078003C001E0078003C001E0078003C001E0 078003C001E0078003C001E0078003C001E0078003C001E0078003C001E0FFFC7FFE3FFFFFFC7F FE3FFF301A7F9933>I<0783F800FF8C1C00FF900E000FA0070007A0078007C0078007C0078007 800780078007800780078007800780078007800780078007800780078007800780078007800780 07800780078007800780078007800780078007800780078007800780FFFCFFFCFFFCFFFC1E1A7F 9921>I<007F000001C1C000070070000E0038001C001C003C001E003C001E0078000F0078000F 00F8000F80F8000F80F8000F80F8000F80F8000F80F8000F80F8000F80F8000F8078000F007800 0F003C001E003C001E001E003C000E0038000700700001C1C000007F0000191A7E991E>I<0783 F000FF8C1C00FFB00F0007A0078007C003C0078003E0078001E0078001F0078001F0078000F807 8000F8078000F8078000F8078000F8078000F8078000F8078000F0078001F0078001F0078001E0 078003C007C003C007C0078007A00E0007983C000787E000078000000780000007800000078000 00078000000780000007800000078000000780000007800000FFFC0000FFFC00001D267F9921> I<0787C0FF98E0FF91F00FA1F007C1F007C0E007C0000780000780000780000780000780000780 0007800007800007800007800007800007800007800007800007800007800007C000FFFE00FFFE 00141A7F9917>114 D<07F8401C06C03001C06000C06000C0E00040E00040F00040F800007E00 007FF0003FFE000FFF0003FF80003FC00007C08001E08001E0C000E0C000E0C000E0E000C0F001 C0F80180C4070083F800131A7E9918>I<00800000800000800000800001800001800001800003 80000380000780000F80001FFF80FFFF8007800007800007800007800007800007800007800007 800007800007800007800007800007800007804007804007804007804007804007804007804003 C08001C08000E100003E0012257FA417>I<07800780FF80FF80FF80FF800F800F800780078007 800780078007800780078007800780078007800780078007800780078007800780078007800780 078007800780078007800780078007800780078007800F8007800F800380178001C027C000E047 FC003F87FC1E1A7F9921>III121 D E /Fv 3 123 df<01800180018001804182F18F399C0FF003C003C00FF0399CF18F41820180 01800180018010127E9215>3 D<02000700070007000700070007000200020002007270FFF872 700200020007000700070007000700070007000700070007000700070007000700070007000700 0200020002000200020002000D267E9C12>121 D<02000700070007000700020002004210FFF8 FFF802000200020007000700070007000200000002000700070007000700020002000200FFF8FF F8421002000200070007000700070002000D257E9C12>I E /Fw 24 120 df<7FFFFFFFFFE0FFFFFFFFFFF0FFFFFFFFFFF07FFFFFFFFFE000000000000000000000000000 000000000000000000000000000000000000000000000000000000000000000000000000000000 00000000000000007FFFFFFFFFE0FFFFFFFFFFF0FFFFFFFFFFF07FFFFFFFFFE02C127C9735>61 D<000003800000000007C00000000007C0000000000FE0000000000FE0000000000FE000000000 1FF0000000001FF0000000003FF8000000003FF8000000003FF80000000073FC0000000073FC00 000000F3FE00000000E1FE00000000E1FE00000001C0FF00000001C0FF00000003C0FF80000003 807F80000007807FC0000007003FC0000007003FC000000E003FE000000E001FE000001E001FF0 00001C000FF000001FFFFFF000003FFFFFF800003FFFFFF80000780007FC0000700003FC000070 0003FC0000E00001FE0000E00001FE0001E00001FF0001C00000FF0001C00000FF00FFFE001FFF FEFFFE001FFFFEFFFE001FFFFE2F297EA834>65 D<00003FF001800003FFFE0380000FFFFF8780 003FF007DF8000FF8001FF8001FE00007F8003FC00003F8007F000001F800FF000000F801FE000 0007801FE0000007803FC0000007803FC0000003807FC0000003807F80000003807F8000000000 FF8000000000FF8000000000FF8000000000FF8000000000FF8000000000FF8000000000FF8000 000000FF8000000000FF80000000007F80000000007F80000000007FC0000003803FC000000380 3FC0000003801FE0000003801FE0000007000FF00000070007F000000E0003FC00001E0001FE00 003C0000FF8000F800003FF007E000000FFFFFC0000003FFFF000000003FF8000029297CA832> 67 DII< FFFFFCFFFFFCFFFFFC01FE0001FE0001FE0001FE0001FE0001FE0001FE0001FE0001FE0001FE00 01FE0001FE0001FE0001FE0001FE0001FE0001FE0001FE0001FE0001FE0001FE0001FE0001FE00 01FE0001FE0001FE0001FE0001FE0001FE0001FE0001FE0001FE0001FE0001FE0001FE00FFFFFC FFFFFCFFFFFC16297EA81A>73 D78 D<0000FFE000000007FFFC0000003FC07F8000007F001FC00001FC0007F00003F80003F80007F0 0001FC000FF00001FE001FE00000FF001FE00000FF003FC000007F803FC000007F807FC000007F C07F8000003FC07F8000003FC07F8000003FC0FF8000003FE0FF8000003FE0FF8000003FE0FF80 00003FE0FF8000003FE0FF8000003FE0FF8000003FE0FF8000003FE0FF8000003FE0FF8000003F E07F8000003FC07FC000007FC07FC000007FC03FC000007F803FC000007F801FE00000FF001FE0 0000FF000FF00001FE0007F00001FC0003F80003F80001FC0007F00000FF001FE000003FC07F80 00000FFFFE00000000FFE000002B297CA834>II<007F 806003FFF0E007FFF9E00F807FE01F001FE03E0007E07C0003E07C0001E0FC0001E0FC0001E0FC 0000E0FE0000E0FE0000E0FF000000FFC000007FFE00007FFFE0003FFFFC001FFFFE000FFFFF80 07FFFFC003FFFFE000FFFFE00007FFF000007FF000000FF8000007F8000003F8600001F8E00001 F8E00001F8E00001F8F00001F0F00001F0F80003F0FC0003E0FF0007C0FFE01F80F3FFFF00E0FF FE00C01FF0001D297CA826>83 D<7FFFFFFFFFC07FFFFFFFFFC07FFFFFFFFFC07F803FC03FC07E 003FC007C078003FC003C078003FC003C070003FC001C0F0003FC001E0F0003FC001E0E0003FC0 00E0E0003FC000E0E0003FC000E0E0003FC000E0E0003FC000E000003FC0000000003FC0000000 003FC0000000003FC0000000003FC0000000003FC0000000003FC0000000003FC0000000003FC0 000000003FC0000000003FC0000000003FC0000000003FC0000000003FC0000000003FC0000000 003FC0000000003FC0000000003FC0000000003FC0000000003FC0000000003FC0000000003FC0 0000007FFFFFE000007FFFFFE000007FFFFFE0002B287EA730>I<01FF800007FFF0000F81F800 1FC07E001FC07E001FC03F000F803F8007003F8000003F8000003F8000003F80000FFF8000FFFF 8007FC3F800FE03F803F803F803F003F807F003F80FE003F80FE003F80FE003F80FE003F807E00 7F807F00DF803F839FFC0FFF0FFC01FC03FC1E1B7E9A21>97 D<00003FF80000003FF80000003F F800000003F800000003F800000003F800000003F800000003F800000003F800000003F8000000 03F800000003F800000003F800000003F800000003F800001FE3F80000FFFBF80003F03FF80007 E00FF8000FC007F8001F8003F8003F8003F8007F0003F8007F0003F8007F0003F800FF0003F800 FF0003F800FF0003F800FF0003F800FF0003F800FF0003F800FF0003F8007F0003F8007F0003F8 007F0003F8003F8003F8001F8003F8000F8007F80007C00FF80003F03BFF8000FFF3FF80003FC3 FF80212A7EA926>100 D<003FE00001FFF80003F07E0007C01F000F801F801F800F803F800FC0 7F000FC07F0007C07F0007E0FF0007E0FF0007E0FFFFFFE0FFFFFFE0FF000000FF000000FF0000 007F0000007F0000007F0000003F8000E01F8000E00FC001C007E0038003F81F0000FFFE00001F F0001B1B7E9A20>I<0007F0003FFC00FE3E01F87F03F87F03F07F07F07F07F03E07F00007F000 07F00007F00007F00007F00007F000FFFFC0FFFFC0FFFFC007F00007F00007F00007F00007F000 07F00007F00007F00007F00007F00007F00007F00007F00007F00007F00007F00007F00007F000 07F00007F00007F0007FFF807FFF807FFF80182A7EA915>I104 D<07000FC01FE03FE03FE03FE01FE00FC007000000000000000000000000 000000FFE0FFE0FFE00FE00FE00FE00FE00FE00FE00FE00FE00FE00FE00FE00FE00FE00FE00FE0 0FE00FE00FE00FE00FE00FE0FFFEFFFEFFFE0F2B7DAA14>I109 DI<003FE00001FFFC0003F07E000FC01F801F800FC03F800FE03F 0007E07F0007F07F0007F07F0007F0FF0007F8FF0007F8FF0007F8FF0007F8FF0007F8FF0007F8 FF0007F8FF0007F87F0007F07F0007F03F800FE03F800FE01F800FC00FC01F8007F07F0001FFFC 00003FE0001D1B7E9A22>I114 D<03FE300FFFF01E03F03800F0700070 F00070F00070F80070FC0000FFE0007FFE007FFF803FFFE01FFFF007FFF800FFF80003FC0000FC 60007CE0003CF0003CF00038F80038FC0070FF01E0F7FFC0C1FF00161B7E9A1B>I<0070000070 0000700000700000F00000F00000F00001F00003F00003F00007F0001FFFF0FFFFF0FFFFF007F0 0007F00007F00007F00007F00007F00007F00007F00007F00007F00007F00007F00007F00007F0 3807F03807F03807F03807F03807F03803F03803F87001F86000FFC0001F8015267FA51B>I119 D E end %%EndProlog %%BeginSetup %%Feature: *Resolution 300 TeXDict begin %%EndSetup %%Page: 1 1 bop 160 214 a Fw(On)22 b(IP)h(=)h(PSP)-6 b(A)n(CE)23 b(and)h(Theorems)e(with) f(Narro)n(w)j(Pro)r(ofs)1789 192 y Fv(\003)261 362 y Fu(Juris)c(Hartmanis)135 b(Ric)n(hard)20 b(Chang)1214 340 y Fv(y)1352 362 y Fu(Desh)e(Ranjan)1688 340 y Fv(z)771 436 y Fu(P)n(ank)m(a)s(j)i(Rohatgi)282 560 y(Departmen)n(t)f (of)h(Computer)f(Science,)f(Cornell)h(Univ)n(ersit)n(y)581 620 y(Ithaca,)f(New)i(Y)-5 b(ork)20 b(14853,)f(USA)875 858 y Ft(Abstract)265 942 y Fs(It)f(has)h(b)q(een)g(sho)o(wn)f(that)f(the)i (class)f(of)g(languages)g(with)h(in)o(teractiv)o(e)g(pro)q(ofs,)f(IP)l(,)197 998 y(is)k(exactly)h(the)f(class)g(PSP)l(A)o(CE.)41 b(This)22 b(surprising)i(result)e(elegan)o(tly)h(places)g(IP)f(in)197 1055 y(the)e(standard)g(classi\014cation)i(of)d(feasible)j(computations.)35 b(F)l(urthermore,)20 b(the)g(IP)i(=)197 1111 y(PSP)l(A)o(CE)f(result)g(rev)o (eals)g(some)g(v)o(ery)g(in)o(teresting)g(and)g(unsusp)q(ected)i(prop)q (erties)e(of)197 1168 y(mathematical)15 b(pro)q(ofs.)265 1224 y(In)20 b(this)g(column)g(w)o(e)g(de\014ne)g(the)g Fr(width)j Fs(of)c(a)h(pro)q(of)f(in)h(a)f(formal)g(system)g Fq(F)24 b Fs(and)197 1281 y(sho)o(w)d(that)g(it)h(is)g(an)g(in)o(tuitiv)o(ely)h (satisfying)f(and)g(robust)g(de\014nition.)41 b(Then,)23 b(using)197 1337 y(the)18 b(IP)f(=)g(PSP)l(A)o(CE)g(result,)h(it)g(is)g(seen)g(that)f (the)h(width)g(of)f(a)g(pro)q(of)h(\(as)f(opp)q(osed)h(to)197 1394 y(the)c(length\))h(determines)g(ho)o(w)f(quic)o(kly)h(one)f(can)h(giv)o (e)f(o)o(v)o(erwhelming)h(evidence)h(that)d(a)197 1450 y(theorem)i(is)h(pro)o (v)m(able)f(without)h(sho)o(wing)f(the)g(full)i(pro)q(of.)75 1616 y Fp(1)83 b(On)27 b(Pro)r(ofs)h(and)g(In)n(teractiv)n(e)e(Pro)r(ofs)75 1726 y Fo(A)17 b(mathematician)d(has)19 b(the)e(most)f(con\014dence)h(in)g (the)g(truth)h(of)g(a)f(theorem)f(when)i(he/she)f(is)75 1786 y(giv)o(en)g(a)h(complete)d(pro)q(of)k(of)f(the)f(theorem)f(in)h(a)h(trusted) g(formal)f(system.)23 b(Let)18 b Fn(F)k Fo(b)q(e)c(suc)o(h)g(a)75 1846 y(formal)13 b(system)f(in)h(whic)o(h)g(the)h(correctness)f(of)h(a)h(pro) q(of)f(can)g(b)q(e)g(c)o(hec)o(k)o(ed)e(b)o(y)h(a)h(v)o(eri\014er)e(in)i(p)q (oly-)75 1906 y(nomial)e(time.)18 b(The)c(class)g(NP)f(clearly)g(captures)g (all)g(the)h(theorems)e(whic)o(h)h(ha)o(v)o(e)g(p)q(olynomially)75 1967 y(long)18 b(pro)q(ofs.)28 b(The)17 b(NP)35 b(=?)17 b(P)h(question)g(is)g (the)f(question)h(ab)q(out)h(the)f(quan)o(titativ)o(e)e(compu-)75 2027 y(tational)f(di\013erence)f(b)q(et)o(w)o(een)h(\014nding)g(a)h(pro)q(of) g(of)f(a)h(theorem)d(and)j(c)o(hec)o(king)e(the)g(correctness)75 2087 y(of)j(a)f(giv)o(en)g(pro)q(of.)148 2147 y(Some)k(y)o(ears)h(ago,)j (theoretical)c(computer)g(scien)o(tists)g(ask)o(ed)i(whether)f(it)g(is)g(p)q (ossible)h(to)75 2207 y(giv)o(e)13 b(con)o(vincing)g(evidence)f(that)i(a)h (theorem)d(is)i(pro)o(v)m(able)g(in)f Fn(F)19 b Fo(without)14 b(sho)o(wing)h(a)f(complete)p 75 2251 720 2 v 131 2282 a Fm(\003)150 2297 y Fl(This)g(researc)o(h)h(w)o(as)f(supp)q(orted)h(in)f(part)g(b)o(y)f (NSF)i(Researc)o(h)g(Gran)o(t)e(CCR)g(88-23053.)132 2332 y Fm(y)150 2347 y Fl(Supp)q(orted)g(in)e(part)h(b)o(y)g(an)f(IBM)i(Graduate)f (F)m(ello)o(wship.)k(Curren)o(t)c(Address:)19 b(Departmen)o(t)11 b(of)h(Computer)75 2397 y(Science,)j(Univ)o(ersit)o(y)f(of)f(Maryland,)g (Baltimore)f(Coun)o(t)o(y)h(Campus,)g(Baltimore,)e(MD)j(21228,)e(USA.)132 2432 y Fm(z)150 2447 y Fl(Curren)o(t)i(Address:)19 b(Max)13 b(Plank)g(Institut)g(f)q(\177)-22 b(ur)13 b(Informatik,)e(Im)g(Stadt)o(w)o (ald,)h(W)h(6600)f(Saarbr)q(\177)-22 b(uc)o(k)o(en,)14 b(Ger-)75 2497 y(man)o(y)m(.)j(On)e(lea)o(v)o(e)f(from)f(Departmen)o(t)h(of)g(Computer) g(Science,)h(New)g(Mexico)g(State)g(Univ)o(ersit)o(y)m(,)e(Las)i(Cruces,)75 2547 y(NM)f(88003,)e(USA.)p eop %%Page: 2 2 bop 75 42 a Fo(pro)q(of.)22 b(Clearly)l(,)13 b(if)g(w)o(e)h(do)h(not)f(giv)o (e)f(a)i(complete)c(pro)q(of)16 b(to)e(a)h(v)o(eri\014er)d(\(that)j(do)q(es)f (not)h(ha)o(v)o(e)e(the)75 102 y(p)q(o)o(w)o(er)h(or)h(time)d(to)j(generate)f (and)h(c)o(hec)o(k)d(the)j(pro)q(of)s(\),)g(then)g(w)o(e)e(cannot)i(exp)q (ect)f(the)g(v)o(eri\014er)f(to)75 162 y(b)q(e)j(completely)d(con)o(vinced)h (that)i(the)g(theorem)e(is)i(pro)o(v)m(able.)21 b(This)16 b(led)f(to)h(a)g(v) o(ery)f(fascinating)75 222 y(problem:)k(ho)o(w)d(can)g(a)g(v)o(eri\014er)d(b) q(e)j(con)o(vinced)e(with)h(high)h(probabilit)o(y)e(that)i(a)g(giv)o(en)f (theorem)75 282 y(is)h(pro)o(v)m(able)g(without)h(seeing)f(the)g(whole)g(pro) q(of)s(?)23 b(and)17 b(ho)o(w)g(rapidly)e(can)i(this)f(b)q(e)g(done?)148 342 y(This)g(problem)e(has)i(b)q(een)f(form)o(ulated)f(and)i(extensiv)o(ely)d (studied)i(in)g(terms)f(of)i Fk(inter)n(active)75 403 y(pr)n(oto)n(c)n(ols)27 b Fo([Gol89)q(].)44 b(Informally)l(,)24 b(an)g(in)o(teractiv)o(e)e(proto)q (col)j(consists)g(of)f(a)h Fk(Pr)n(over)k Fo(and)c(a)75 463 y Fk(V)l(eri\014er)p Fo(.)41 b(The)23 b(Pro)o(v)o(er)e(is)i(an)g(all)f(p)q(o) o(w)o(erful)g(T)l(uring)h(Mac)o(hine)e(\(TM\))i(and)g(the)f(V)l(eri\014er)f (is)75 523 y(a)h(TM)f(whic)o(h)f(op)q(erates)i(in)f(time)f(p)q(olynomial)g (in)h(the)g(length)g(of)g(the)g(input.)36 b(In)21 b(addition,)75 583 y(the)d(V)l(eri\014er)e(has)j(a)f(random)g(source)g(\(e.g.,)f(a)h(fair)g (coin\))g(not)g(visible)f(to)h(the)g(Pro)o(v)o(er.)26 b(In)17 b(the)75 643 y(b)q(eginning)22 b(of)g(the)g(in)o(teractiv)o(e)d(proto)q(col)k (the)e(Pro)o(v)o(er)g(and)h(the)g(V)l(eri\014er)e(receiv)o(e)g(the)h(same)75 704 y(input)i(string.)41 b(Then,)24 b(the)f(Pro)o(v)o(er)f(tries)g(to)h(con)o (vince)e(the)i(V)l(eri\014er,)f(through)i(a)g(series)e(of)75 764 y(queries)17 b(and)h(answ)o(ers,)g(that)g(the)g(input)g(string)g(b)q (elongs)g(to)g(a)g(giv)o(en)f(language.)27 b(The)18 b(Pro)o(v)o(er)75 824 y(succeeds)e(if)g(the)g(V)l(eri\014er)f(accepts)h(with)h(probabilit)o(y)e (greater)i(than)g(2)p Fj(=)p Fo(3.)23 b(The)17 b(probabilit)o(y)e(is)75 884 y(computed)k(o)o(v)o(er)g(all)h(p)q(ossible)h(coin)f(tosses)h(made)e(b)o (y)h(the)g(V)l(eri\014er.)31 b(Ho)o(w)o(ev)o(er,)20 b(the)g(V)l(eri\014er)75 944 y(m)o(ust)15 b(guard)j(against)f(imp)q(osters)f(masquerading)g(as)h(the)f (real)g(Pro)o(v)o(er.)21 b(That)c(is,)f(the)h(V)l(eri\014er)75 1005 y(m)o(ust)c(not)h(b)q(e)h(con)o(vinced)d(to)j(accept)f(a)g(string)g(not) h(in)f(the)g(language)h(with)f(probabilit)o(y)f(greater)75 1065 y(than)k(1)p Fj(=)p Fo(3|ev)o(en)f(if)g(the)g(Pro)o(v)o(er)f(lies.)75 1157 y Fi(De\014nition)h Fo(Let)h Fj(V)28 b Fo(b)q(e)17 b(a)g(probabilistic)f (p)q(olynomial)f(time)g(TM)h(and)i(let)e Fj(P)24 b Fo(b)q(e)17 b(an)g(arbitrary)75 1217 y(TM.)12 b Fj(P)20 b Fo(and)14 b Fj(V)24 b Fo(share)13 b(the)g(same)f(input)g(tap)q(e)i(and)f(comm)o(unicate)c(via)k (a)g(comm)o(unication)d(tap)q(e.)75 1278 y Fj(P)23 b Fo(and)17 b Fj(V)28 b Fo(form)15 b(an)i(in)o(teractiv)o(e)d(proto)q(col)j(for)f(a)h (language)g Fj(L)f Fo(if)135 1376 y(1.)24 b Fj(x)13 b Fn(2)i Fj(L)f Fo(=)-8 b Fn(\))15 b Fo(Prob[)i Fj(P)7 b Fo(-)p Fj(V)28 b Fo(accepts)16 b Fj(x)g Fo(])f Fj(>)f Fo(2)p Fj(=)p Fo(3.)135 1477 y(2.)24 b Fj(x)13 b Fn(62)i Fj(L)f Fo(=)-8 b Fn(\))15 b(8)p Fj(P)495 1459 y Fh(\003)514 1477 y Fo(,)h(Prob[)g Fj(P)715 1459 y Fh(\003)735 1477 y Fo(-)p Fj(V)28 b Fo(accepts)16 b Fj(x)g Fo(])g Fj(<)d Fo(1)p Fj(=)p Fo(3.)75 1576 y(A)k(language)h Fj(L)g Fo(is)f(in)g(IP)h(if)f(there)f(exist)h Fj(P)25 b Fo(and)18 b Fj(V)28 b Fo(whic)o(h)17 b(form)g(an)h(in)o(teractiv)o(e)d(proto)q(col)j (for)75 1636 y Fj(L)p Fo(.)148 1729 y(Clearly)l(,)c(IP)h(con)o(tains)g(all)f (NP)h(languages,)h(b)q(ecause)f(in)g(p)q(olynomial)f(time)f(the)i(Pro)o(v)o (er)f(can)75 1789 y(giv)o(e)19 b(the)g(V)l(eri\014er)f(the)h(en)o(tire)f(pro) q(of.)32 b(In)20 b(suc)o(h)f(a)h(proto)q(col,)h(the)e(V)l(eri\014er)f(cannot) i(b)q(e)g(fo)q(oled)75 1849 y(and)h(nev)o(er)d(accepts)i(a)h(string)f(not)g (in)g(the)g(language.)33 b(T)l(o)21 b(illustrate)e(ho)o(w)h(randomness)g(can) 75 1909 y(generalize)12 b(the)g(concept)h(of)g(a)g(pro)q(of,)h(w)o(e)f(lo)q (ok)g(at)h(an)f(in)o(teractiv)o(e)d(proto)q(col)k(for)f(a)h(language)g(not)75 1970 y(kno)o(wn)h(to)f(b)q(e)h(in)f(NP.)g(Consider)h(GNI,)e(the)h(set)h(of)f (pairs)h(of)g(graphs)h(that)e(are)h(not)g(isomorphic.)75 2030 y(GNI)f(is)h(kno)o(wn)h(to)f(b)q(e)g(in)g(co-NP)g(and)g(b)q(eliev)o(ed)f(not) h(to)g(b)q(e)h(in)e(NP.)h(Ho)o(w)o(ev)o(er,)e(GNI)h(do)q(es)i(ha)o(v)o(e)75 2090 y(an)f(in)o(teractiv)o(e)d(proto)q(col)j([GMW86].)21 b(F)l(or)14 b(small)f(graphs,)i(the)g(V)l(eri\014er)d(can)j(easily)f(determine)75 2150 y(if)f(the)g(t)o(w)o(o)h(graphs)g(are)g(not)g(isomorphic.)19 b(F)l(or)14 b(su\016cien)o(tly)d(large)j(graphs,)h(the)e(V)l(eri\014er)f (solicits)75 2210 y(help)k(from)f(the)h(Pro)o(v)o(er)f(to)i(sho)o(w)g(that)f Fj(G)860 2217 y Fg(i)891 2210 y Fo(and)h Fj(G)1024 2217 y Fg(j)1059 2210 y Fo(are)f(not)h(isomorphic,)e(as)h(follo)o(ws:)135 2309 y(1.)24 b(The)11 b(V)l(eri\014er)f(randomly)g(selects)h Fj(G)857 2316 y Fg(i)883 2309 y Fo(or)h Fj(G)976 2316 y Fg(j)1006 2309 y Fo(and)g(a)f(random)g(p)q(erm)o(utation)g(of)g(the)g(selected)197 2369 y(graph.)23 b(This)17 b(pro)q(cess)g(is)g(indep)q(enden)o(tly)e(rep)q (eated)i Fj(n)f Fo(times,)f(where)h Fj(n)h Fo(is)f(the)h(n)o(um)o(b)q(er)197 2430 y(of)g(v)o(ertices)f(in)h Fj(G)527 2437 y Fg(j)546 2430 y Fo(.)24 b(If)17 b(the)g(graphs)h(do)g(not)g(ha)o(v)o(e)e(the)h(same)f(n)o (um)o(b)q(er)g(of)h(v)o(ertices,)f(they)197 2490 y(are)23 b(clearly)f(not)h (isomorphic.)41 b(This)23 b(sequence)f(of)i Fj(n)f Fo(randomly)f(c)o(hosen,)i (randomly)197 2550 y(p)q(erm)o(uted)19 b(graphs)k(is)e(sen)o(t)g(to)g(the)g (Pro)o(v)o(er.)36 b(Recall)20 b(that)h(the)g(Pro)o(v)o(er)g(has)h(not)f(seen) p eop %%Page: 3 3 bop 197 42 a Fo(the)16 b(V)l(eri\014er's)e(random)i(bits.)21 b(This)16 b(assumption)g(is)g(not)g(necessary)l(,)f(but)i(simpli\014es)c(the) 197 102 y(exp)q(osition.)135 203 y(2.)24 b(The)13 b(V)l(eri\014er)e(asks)j (the)f(Pro)o(v)o(er)f(to)h(determine,)e(for)i(eac)o(h)f(graph)i(in)f(the)g (sequence,)f(whic)o(h)197 264 y(graph,)22 b Fj(G)392 271 y Fg(i)428 264 y Fo(or)f Fj(G)530 271 y Fg(j)548 264 y Fo(,)h(w)o(as)f(the)f (one)h(selected.)34 b(If)20 b(the)g(Pro)o(v)o(er)g(answ)o(ers)h(all)g(the)f (queries)197 324 y(correctly)l(,)14 b(then)i(the)g(V)l(eri\014er)f(accepts.) 75 425 y(Supp)q(ose)k(the)f(t)o(w)o(o)g(original)g(graphs)h(are)f(not)h (isomorphic.)25 b(Then,)19 b(only)f(one)g(of)g(the)g(original)75 486 y(graphs)g(is)f(isomorphic)f(to)i(the)f(p)q(erm)o(uted)e(graph.)25 b(The)17 b(Pro)o(v)o(er)g(simply)e(answ)o(ers)j(b)o(y)e(pic)o(king)75 546 y(that)i(graph.)27 b(If)18 b(the)f(graphs)i(are)f(isomorphic,)f(then)g (the)h(Pro)o(v)o(er)f(has)i(at)f(b)q(est)g(a)h(2)1664 528 y Fh(\000)p Fg(n)1733 546 y Fo(c)o(hance)75 606 y(of)e(answ)o(ering)g(all)g Fj(n)g Fo(questions)g(correctly)l(.)k(Th)o(us,)c(the)g(V)l(eri\014er)e (cannot)j(b)q(e)f(fo)q(oled)g(with)g(high)75 666 y(probabilit)o(y)l(.)j (Therefore,)c(GNI)f Fn(2)i Fo(IP)l(.)148 726 y(Note)12 b(that)g(GNI)f(is)h(b) q(eliev)o(ed)d(to)k(b)q(e)f(incomplete)d(for)j(co-NP.)20 b(So,)12 b(the)g(preceding)f(discussion)75 787 y(do)q(es)23 b(not)g(sho)o(w)g(that)f (co-NP)j Fn(\022)f Fo(IP.)39 b(F)l(or)22 b(a)h(while,)f(it)g(w)o(as)h(b)q (eliev)o(ed)d(that)j(co-NP)f(is)h(not)75 847 y(con)o(tained)12 b(in)g(IP)l(,)f(b)q(ecause)h(there)g(are)g(oracle)g(w)o(orlds)g(where)g (co-NP)i Fn(6\022)f Fo(IP)f([FS88)q(].)19 b(In)12 b(fact,)g(the)75 907 y(computational)19 b(p)q(o)o(w)o(er)h(of)g(in)o(teractiv)o(e)d(proto)q (cols)k(w)o(as)f(not)g(fully)f(appreciated)g(un)o(til)g(Lund,)75 967 y(F)l(ortno)o(w,)j(Karlo\013)f(and)g(Nisan)f([LFKN90])g(sho)o(w)o(ed)h (that)g(IP)f(actually)g(con)o(tains)g(the)g(en)o(tire)75 1027 y(P)o(olynomial)12 b(Hierarc)o(h)o(y)l(.)18 b(This)13 b(result)g(then)h(led)e (Shamir)h([Sha90])g(to)h(completely)d(c)o(haracterize)75 1088 y(IP)16 b(b)o(y)g(sho)o(wing)h(that)814 1148 y(IP)c(=)h(PSP)l(A)o(CE)p Fj(:)75 1235 y Fo(Babai,)j(F)l(ortno)o(w)h(and)g(Lund)h([BFL90])e(c)o (haracterized)f(the)h(computational)g(p)q(o)o(w)o(er)g(of)h(m)o(ulti-)75 1295 y(pro)o(v)o(er)d(in)o(teractiv)o(e)f(proto)q(cols)818 1355 y(MIP)f(=)h(NEXP)p Fj(:)75 1443 y Fo(In)f(b)q(oth)g(cases,)h(it)e(is)h (in)o(teresting)e(to)j(see)e(that)h(in)o(teractiv)o(e)e(pro)q(of)j(systems)d (pro)o(vide)h(alternativ)o(e)75 1503 y(de\014nitions)23 b(of)h(classic)e (complexit)o(y)e(classes.)43 b(Th)o(us,)25 b(they)d(\014t)i(v)o(ery)e(nicely) f(in)i(the)g(o)o(v)o(erall)75 1563 y(classi\014cation)f(of)h(feasible)e (computations.)39 b(F)l(urthermore,)21 b(b)q(oth)i(of)g(these)f(problems)f (ha)o(v)o(e)75 1623 y(con)o(tradictory)16 b(relativizations)f([FS88].)21 b(That)c(is,)e(there)h(exist)f(oracles)i Fj(A)e Fo(and)i Fj(B)i Fo(suc)o(h)d(that)530 1733 y(IP)581 1715 y Ff(A)623 1733 y Fo(=)e(PSP)l(A)o(CE)868 1712 y Fg(A)929 1733 y Fo(and)33 b(IP)1091 1715 y Ff(B)1132 1733 y Fn(6)p Fo(=)13 b(PSP)l(A)o(CE)1376 1712 y Fg(B)1407 1733 y Fj(;)75 1843 y Fo(and)18 b(similarly)d(for)j(the)g(m) o(ulti-pro)o(v)o(er)c(case.)26 b(Th)o(us,)18 b(these)f(results)h(pro)o(vide)e (the)i(\014rst)g Fk(natur)n(al)75 1903 y Fo(coun)o(terexamples)h(to)k(the)e (b)q(elief)g(that)h(problems)e(with)i(con)o(tradictory)f(relativizations)g (are)75 1963 y(b)q(ey)o(ond)13 b(our)h(pro)q(of)h(tec)o(hniques.)j(The)c(IP)f (=)h(PSP)l(A)o(CE)f(result)g(also)h(pro)o(vides)f(a)g(v)o(ery)f(dramatic)75 2024 y(coun)o(terexample)k(to)j(the)f(already)g(battered)h(Random)f(Oracle)g (Hyp)q(othesis.)28 b(In)18 b([HCRR90],)75 2084 y(w)o(e)e(sho)o(w)o(ed)g(that) 644 2144 y(Prob)748 2151 y Fg(A)776 2144 y Fo([)g(IP)857 2126 y Ff(A)899 2144 y Fn(6)p Fo(=)e(PSP)l(A)o(CE)1144 2123 y Fg(A)1189 2144 y Fo(])f(=)h(1)p Fj(:)75 2310 y Fp(2)83 b(On)27 b(Theorems)g(with)g(P)n (olynomially)f(Wide)i(Pro)r(ofs)75 2420 y Fo(In)16 b(this)g(section,)g(w)o(e) g(de\014ne)g(the)g(notion)h(of)g(the)f Fk(width)k Fo(of)d(a)g(pro)q(of)g(of)g (a)g(theorem)d(in)i(a)h(formal)75 2480 y(system.)22 b(The)16 b(notion)i(of)f(\\formal)f(system")g(go)q(es)i(bac)o(k)e(to)h(Hilb)q(ert)f (who)h(w)o(an)o(ted)g(to)g(dev)o(elop)75 2540 y(a)e(complete)c(system)i(to)i (formalize)d(all)h(of)i(mathematics.)i(There)d(are)g(sev)o(eral)g(equiv)m (alen)o(t)e(w)o(a)o(ys)p eop %%Page: 4 4 bop 530 498 3 166 v 366 499 165 3 v 365 498 3 166 v 366 334 165 3 v 699 719 3 664 v 700 57 885 3 v 718 121 a Fe(.)-8 b(.)721 120 y(.)h(.)724 119 y(.)g(.)728 118 y(.)f(.)h(.)733 117 y(.)f(.)736 116 y(.)h(.)739 115 y(.)g(.)743 114 y(.)f(.)h(.)748 113 y(.)e(.)e(.)744 112 y(.)h(.)f(.)739 111 y(.)h(.)736 110 y(.)f(.)733 109 y(.)g(.)g(.)728 108 y(.)g(.)724 107 y(.)h(.)f(.)719 106 y(.)h(.)p 588 113 165 3 v 586 220 3 109 v 588 222 165 3 v 718 230 a(.)719 229 y(.)j(.)723 228 y(.)f(.)h(.)728 227 y(.)f(.)731 226 y(.)h(.)734 225 y(.)g(.)g(.)739 224 y(.)g(.)743 223 y(.)f(.)h(.)748 222 y(.)e(.)e(.)744 221 y(.)h(.)741 220 y(.)f(.)h(.)736 219 y(.)f(.)733 218 y(.)g(.)g(.)728 217 y(.)g(.)724 216 y(.)h(.)721 215 y(.)f(.)h(.)p 447 333 3 169 v 449 166 139 3 v 700 166 874 3 v 700 278 818 3 v 700 391 484 3 v 700 499 331 3 v 700 612 233 3 v 804 57 a(.)804 59 y(.)804 60 y(.)804 62 y(.)804 64 y(.)804 65 y(.)804 67 y(.)804 69 y(.)804 70 y(.)804 72 y(.)804 87 y(.)804 89 y(.)804 90 y(.)804 92 y(.)804 94 y(.)804 95 y(.)804 97 y(.)804 99 y(.)804 100 y(.)804 102 y(.)804 117 y(.)804 119 y(.)804 120 y(.)804 122 y(.)804 124 y(.)804 125 y(.)804 127 y(.)804 129 y(.)804 130 y(.)804 132 y(.)804 147 y(.)804 149 y(.)804 150 y(.)804 152 y(.)804 154 y(.)804 155 y(.)804 157 y(.)804 159 y(.)804 160 y(.)804 162 y(.)804 177 y(.)804 179 y(.)804 180 y(.)804 182 y(.)804 184 y(.)804 185 y(.)804 187 y(.)804 189 y(.)804 190 y(.)804 192 y(.)804 207 y(.)804 209 y(.)804 210 y(.)804 212 y(.)804 214 y(.)804 215 y(.)804 217 y(.)804 219 y(.)804 220 y(.)804 222 y(.)804 237 y(.)804 239 y(.)804 240 y(.)804 242 y(.)804 244 y(.)804 245 y(.)804 247 y(.)804 249 y(.)804 250 y(.)804 252 y(.)804 267 y(.)804 269 y(.)804 270 y(.)804 272 y(.)804 274 y(.)804 275 y(.)804 277 y(.)804 279 y(.)804 280 y(.)804 282 y(.)804 297 y(.)804 299 y(.)804 300 y(.)804 302 y(.)804 304 y(.)804 305 y(.)804 307 y(.)804 309 y(.)804 310 y(.)804 312 y(.)804 327 y(.)804 329 y(.)804 330 y(.)804 332 y(.)804 334 y(.)804 335 y(.)804 337 y(.)804 339 y(.)804 340 y(.)804 342 y(.)804 357 y(.)804 359 y(.)804 360 y(.)804 362 y(.)804 364 y(.)804 365 y(.)804 367 y(.)804 369 y(.)804 370 y(.)804 372 y(.)804 387 y(.)804 389 y(.)804 390 y(.)804 392 y(.)804 394 y(.)804 395 y(.)804 397 y(.)804 399 y(.)804 400 y(.)804 402 y(.)804 417 y(.)804 419 y(.)804 420 y(.)804 422 y(.)804 424 y(.)804 425 y(.)804 427 y(.)804 429 y(.)804 430 y(.)804 432 y(.)804 447 y(.)804 449 y(.)804 450 y(.)804 452 y(.)804 454 y(.)804 455 y(.)804 457 y(.)804 459 y(.)804 460 y(.)804 462 y(.)804 477 y(.)804 479 y(.)804 480 y(.)804 482 y(.)804 484 y(.)804 485 y(.)804 487 y(.)804 489 y(.)804 490 y(.)804 492 y(.)804 507 y(.)804 509 y(.)804 510 y(.)804 512 y(.)804 514 y(.)804 515 y(.)804 517 y(.)804 519 y(.)804 520 y(.)804 522 y(.)804 537 y(.)804 539 y(.)804 540 y(.)804 542 y(.)804 544 y(.)804 545 y(.)804 547 y(.)804 549 y(.)804 550 y(.)804 552 y(.)804 567 y(.)804 569 y(.)804 570 y(.)804 572 y(.)804 574 y(.)804 575 y(.)804 577 y(.)804 579 y(.)804 580 y(.)804 582 y(.)804 597 y(.)804 599 y(.)804 600 y(.)804 602 y(.)804 604 y(.)804 605 y(.)804 607 y(.)804 609 y(.)804 610 y(.)804 612 y(.)804 627 y(.)804 629 y(.)804 630 y(.)804 632 y(.)804 634 y(.)804 635 y(.)804 637 y(.)804 639 y(.)804 640 y(.)804 642 y(.)804 657 y(.)804 659 y(.)804 660 y(.)804 662 y(.)804 664 y(.)804 665 y(.)804 667 y(.)804 669 y(.)804 670 y(.)804 672 y(.)804 687 y(.)804 689 y(.)804 690 y(.)804 692 y(.)804 694 y(.)917 57 y(.)917 59 y(.)917 60 y(.)917 62 y(.)917 64 y(.)917 65 y(.)917 67 y(.)917 69 y(.)917 70 y(.)917 72 y(.)917 87 y(.)917 89 y(.)917 90 y(.)917 92 y(.)917 94 y(.)917 95 y(.)917 97 y(.)917 99 y(.)917 100 y(.)917 102 y(.)917 117 y(.)917 119 y(.)917 120 y(.)917 122 y(.)917 124 y(.)917 125 y(.)917 127 y(.)917 129 y(.)917 130 y(.)917 132 y(.)917 147 y(.)917 149 y(.)917 150 y(.)917 152 y(.)917 154 y(.)917 155 y(.)917 157 y(.)917 159 y(.)917 160 y(.)917 162 y(.)917 177 y(.)917 179 y(.)917 180 y(.)917 182 y(.)917 184 y(.)917 185 y(.)917 187 y(.)917 189 y(.)917 190 y(.)917 192 y(.)917 207 y(.)917 209 y(.)917 210 y(.)917 212 y(.)917 214 y(.)917 215 y(.)917 217 y(.)917 219 y(.)917 220 y(.)917 222 y(.)917 237 y(.)917 239 y(.)917 240 y(.)917 242 y(.)917 244 y(.)917 245 y(.)917 247 y(.)917 249 y(.)917 250 y(.)917 252 y(.)917 267 y(.)917 269 y(.)917 270 y(.)917 272 y(.)917 274 y(.)917 275 y(.)917 277 y(.)917 279 y(.)917 280 y(.)917 282 y(.)917 297 y(.)917 299 y(.)917 300 y(.)917 302 y(.)917 304 y(.)917 305 y(.)917 307 y(.)917 309 y(.)917 310 y(.)917 312 y(.)917 327 y(.)917 329 y(.)917 330 y(.)917 332 y(.)917 334 y(.)917 335 y(.)917 337 y(.)917 339 y(.)917 340 y(.)917 342 y(.)917 357 y(.)917 359 y(.)917 360 y(.)917 362 y(.)917 364 y(.)917 365 y(.)917 367 y(.)917 369 y(.)917 370 y(.)917 372 y(.)917 387 y(.)917 389 y(.)917 390 y(.)917 392 y(.)917 394 y(.)917 395 y(.)917 397 y(.)917 399 y(.)917 400 y(.)917 402 y(.)917 417 y(.)917 419 y(.)917 420 y(.)917 422 y(.)917 424 y(.)917 425 y(.)917 427 y(.)917 429 y(.)917 430 y(.)917 432 y(.)917 447 y(.)917 449 y(.)917 450 y(.)917 452 y(.)917 454 y(.)917 455 y(.)917 457 y(.)917 459 y(.)917 460 y(.)917 462 y(.)917 477 y(.)917 479 y(.)917 480 y(.)917 482 y(.)917 484 y(.)917 485 y(.)917 487 y(.)917 489 y(.)917 490 y(.)917 492 y(.)917 507 y(.)917 509 y(.)917 510 y(.)917 512 y(.)917 514 y(.)917 515 y(.)917 517 y(.)917 519 y(.)917 520 y(.)917 522 y(.)917 537 y(.)917 539 y(.)917 540 y(.)917 542 y(.)917 544 y(.)917 545 y(.)917 547 y(.)917 549 y(.)917 550 y(.)917 552 y(.)917 567 y(.)917 569 y(.)917 570 y(.)917 572 y(.)917 574 y(.)917 575 y(.)917 577 y(.)917 579 y(.)917 580 y(.)917 582 y(.)917 597 y(.)917 599 y(.)917 600 y(.)917 602 y(.)917 604 y(.)917 605 y(.)917 607 y(.)917 609 y(.)917 610 y(.)917 612 y(.)917 627 y(.)917 629 y(.)917 630 y(.)917 632 y(.)917 634 y(.)917 635 y(.)917 637 y(.)1026 57 y(.)1026 59 y(.)1026 60 y(.)1026 62 y(.)1026 64 y(.)1026 65 y(.)1026 67 y(.)1026 69 y(.)1026 70 y(.)1026 72 y(.)1026 87 y(.)1026 89 y(.)1026 90 y(.)1026 92 y(.)1026 94 y(.)1026 95 y(.)1026 97 y(.)1026 99 y(.)1026 100 y(.)1026 102 y(.)1026 117 y(.)1026 119 y(.)1026 120 y(.)1026 122 y(.)1026 124 y(.)1026 125 y(.)1026 127 y(.)1026 129 y(.)1026 130 y(.)1026 132 y(.)1026 147 y(.)1026 149 y(.)1026 150 y(.)1026 152 y(.)1026 154 y(.)1026 155 y(.)1026 157 y(.)1026 159 y(.)1026 160 y(.)1026 162 y(.)1026 177 y(.)1026 179 y(.)1026 180 y(.)1026 182 y(.)1026 184 y(.)1026 185 y(.)1026 187 y(.)1026 189 y(.)1026 190 y(.)1026 192 y(.)1026 207 y(.)1026 209 y(.)1026 210 y(.)1026 212 y(.)1026 214 y(.)1026 215 y(.)1026 217 y(.)1026 219 y(.)1026 220 y(.)1026 222 y(.)1026 237 y(.)1026 239 y(.)1026 240 y(.)1026 242 y(.)1026 244 y(.)1026 245 y(.)1026 247 y(.)1026 249 y(.)1026 250 y(.)1026 252 y(.)1026 267 y(.)1026 269 y(.)1026 270 y(.)1026 272 y(.)1026 274 y(.)1026 275 y(.)1026 277 y(.)1026 279 y(.)1026 280 y(.)1026 282 y(.)1026 297 y(.)1026 299 y(.)1026 300 y(.)1026 302 y(.)1026 304 y(.)1026 305 y(.)1026 307 y(.)1026 309 y(.)1026 310 y(.)1026 312 y(.)1026 327 y(.)1026 329 y(.)1026 330 y(.)1026 332 y(.)1026 334 y(.)1026 335 y(.)1026 337 y(.)1026 339 y(.)1026 340 y(.)1026 342 y(.)1026 357 y(.)1026 359 y(.)1026 360 y(.)1026 362 y(.)1026 364 y(.)1026 365 y(.)1026 367 y(.)1026 369 y(.)1026 370 y(.)1026 372 y(.)1026 387 y(.)1026 389 y(.)1026 390 y(.)1026 392 y(.)1026 394 y(.)1026 395 y(.)1026 397 y(.)1026 399 y(.)1026 400 y(.)1026 402 y(.)1026 417 y(.)1026 419 y(.)1026 420 y(.)1026 422 y(.)1026 424 y(.)1026 425 y(.)1026 427 y(.)1026 429 y(.)1026 430 y(.)1026 432 y(.)1026 447 y(.)1026 449 y(.)1026 450 y(.)1026 452 y(.)1026 454 y(.)1026 455 y(.)1026 457 y(.)1026 459 y(.)1026 460 y(.)1026 462 y(.)1026 477 y(.)1026 479 y(.)1026 480 y(.)1026 482 y(.)1026 484 y(.)1026 485 y(.)1026 487 y(.)1026 489 y(.)1026 490 y(.)1026 492 y(.)1138 57 y(.)1138 59 y(.)1138 60 y(.)1138 62 y(.)1138 64 y(.)1138 65 y(.)1138 67 y(.)1138 69 y(.)1138 70 y(.)1138 72 y(.)1138 87 y(.)1138 89 y(.)1138 90 y(.)1138 92 y(.)1138 94 y(.)1138 95 y(.)1138 97 y(.)1138 99 y(.)1138 100 y(.)1138 102 y(.)1138 117 y(.)1138 119 y(.)1138 120 y(.)1138 122 y(.)1138 124 y(.)1138 125 y(.)1138 127 y(.)1138 129 y(.)1138 130 y(.)1138 132 y(.)1138 147 y(.)1138 149 y(.)1138 150 y(.)1138 152 y(.)1138 154 y(.)1138 155 y(.)1138 157 y(.)1138 159 y(.)1138 160 y(.)1138 162 y(.)1138 177 y(.)1138 179 y(.)1138 180 y(.)1138 182 y(.)1138 184 y(.)1138 185 y(.)1138 187 y(.)1138 189 y(.)1138 190 y(.)1138 192 y(.)1138 207 y(.)1138 209 y(.)1138 210 y(.)1138 212 y(.)1138 214 y(.)1138 215 y(.)1138 217 y(.)1138 219 y(.)1138 220 y(.)1138 222 y(.)1138 237 y(.)1138 239 y(.)1138 240 y(.)1138 242 y(.)1138 244 y(.)1138 245 y(.)1138 247 y(.)1138 249 y(.)1138 250 y(.)1138 252 y(.)1138 267 y(.)1138 269 y(.)1138 270 y(.)1138 272 y(.)1138 274 y(.)1138 275 y(.)1138 277 y(.)1138 279 y(.)1138 280 y(.)1138 282 y(.)1138 297 y(.)1138 299 y(.)1138 300 y(.)1138 302 y(.)1138 304 y(.)1138 305 y(.)1138 307 y(.)1138 309 y(.)1138 310 y(.)1138 312 y(.)1138 327 y(.)1138 329 y(.)1138 330 y(.)1138 332 y(.)1138 334 y(.)1138 335 y(.)1138 337 y(.)1138 339 y(.)1138 340 y(.)1138 342 y(.)1138 357 y(.)1138 359 y(.)1138 360 y(.)1138 362 y(.)1138 364 y(.)1138 365 y(.)1138 367 y(.)1138 369 y(.)1138 370 y(.)1138 372 y(.)1138 387 y(.)1138 389 y(.)1138 390 y(.)1138 392 y(.)1138 394 y(.)1138 395 y(.)1138 397 y(.)1138 399 y(.)1138 400 y(.)1138 402 y(.)1251 57 y(.)1251 59 y(.)1251 60 y(.)1251 62 y(.)1251 64 y(.)1251 65 y(.)1251 67 y(.)1251 69 y(.)1251 70 y(.)1251 72 y(.)1251 87 y(.)1251 89 y(.)1251 90 y(.)1251 92 y(.)1251 94 y(.)1251 95 y(.)1251 97 y(.)1251 99 y(.)1251 100 y(.)1251 102 y(.)1251 117 y(.)1251 119 y(.)1251 120 y(.)1251 122 y(.)1251 124 y(.)1251 125 y(.)1251 127 y(.)1251 129 y(.)1251 130 y(.)1251 132 y(.)1251 147 y(.)1251 149 y(.)1251 150 y(.)1251 152 y(.)1251 154 y(.)1251 155 y(.)1251 157 y(.)1251 159 y(.)1251 160 y(.)1251 162 y(.)1251 177 y(.)1251 179 y(.)1251 180 y(.)1251 182 y(.)1251 184 y(.)1251 185 y(.)1251 187 y(.)1251 189 y(.)1251 190 y(.)1251 192 y(.)1251 207 y(.)1251 209 y(.)1251 210 y(.)1251 212 y(.)1251 214 y(.)1251 215 y(.)1251 217 y(.)1251 219 y(.)1251 220 y(.)1251 222 y(.)1251 237 y(.)1251 239 y(.)1251 240 y(.)1251 242 y(.)1251 244 y(.)1251 245 y(.)1251 247 y(.)1251 249 y(.)1251 250 y(.)1251 252 y(.)1251 267 y(.)1251 269 y(.)1251 270 y(.)1251 272 y(.)1251 274 y(.)1251 275 y(.)1251 277 y(.)1251 279 y(.)1251 280 y(.)1251 282 y(.)1251 297 y(.)1251 299 y(.)1251 300 y(.)1251 302 y(.)1251 304 y(.)1251 305 y(.)1251 307 y(.)1251 309 y(.)1251 310 y(.)1251 312 y(.)1251 327 y(.)1251 329 y(.)1251 330 y(.)1251 332 y(.)1251 334 y(.)1251 335 y(.)1251 337 y(.)1251 339 y(.)1251 340 y(.)1251 342 y(.)1251 357 y(.)1251 359 y(.)1251 360 y(.)1359 57 y(.)1359 59 y(.)1359 60 y(.)1359 62 y(.)1359 64 y(.)1359 65 y(.)1359 67 y(.)1359 69 y(.)1359 70 y(.)1359 72 y(.)1359 87 y(.)1359 89 y(.)1359 90 y(.)1359 92 y(.)1359 94 y(.)1359 95 y(.)1359 97 y(.)1359 99 y(.)1359 100 y(.)1359 102 y(.)1359 117 y(.)1359 119 y(.)1359 120 y(.)1359 122 y(.)1359 124 y(.)1359 125 y(.)1359 127 y(.)1359 129 y(.)1359 130 y(.)1359 132 y(.)1359 147 y(.)1359 149 y(.)1359 150 y(.)1359 152 y(.)1359 154 y(.)1359 155 y(.)1359 157 y(.)1359 159 y(.)1359 160 y(.)1359 162 y(.)1359 177 y(.)1359 179 y(.)1359 180 y(.)1359 182 y(.)1359 184 y(.)1359 185 y(.)1359 187 y(.)1359 189 y(.)1359 190 y(.)1359 192 y(.)1359 207 y(.)1359 209 y(.)1359 210 y(.)1359 212 y(.)1359 214 y(.)1359 215 y(.)1359 217 y(.)1359 219 y(.)1359 220 y(.)1359 222 y(.)1359 237 y(.)1359 239 y(.)1359 240 y(.)1359 242 y(.)1359 244 y(.)1359 245 y(.)1359 247 y(.)1359 249 y(.)1359 250 y(.)1359 252 y(.)1359 267 y(.)1359 269 y(.)1359 270 y(.)1359 272 y(.)1359 274 y(.)1359 275 y(.)1359 277 y(.)1359 279 y(.)1359 280 y(.)1359 282 y(.)1359 297 y(.)1359 299 y(.)1359 300 y(.)1359 302 y(.)1359 304 y(.)1359 305 y(.)1359 307 y(.)1359 309 y(.)1359 310 y(.)1359 312 y(.)1472 57 y(.)1472 59 y(.)1472 60 y(.)1472 62 y(.)1472 64 y(.)1472 65 y(.)1472 67 y(.)1472 69 y(.)1472 70 y(.)1472 72 y(.)1472 87 y(.)1472 89 y(.)1472 90 y(.)1472 92 y(.)1472 94 y(.)1472 95 y(.)1472 97 y(.)1472 99 y(.)1472 100 y(.)1472 102 y(.)1472 117 y(.)1472 119 y(.)1472 120 y(.)1472 122 y(.)1472 124 y(.)1472 125 y(.)1472 127 y(.)1472 129 y(.)1472 130 y(.)1472 132 y(.)1472 147 y(.)1472 149 y(.)1472 150 y(.)1472 152 y(.)1472 154 y(.)1472 155 y(.)1472 157 y(.)1472 159 y(.)1472 160 y(.)1472 162 y(.)1472 177 y(.)1472 179 y(.)1472 180 y(.)1472 182 y(.)1472 184 y(.)1472 185 y(.)1472 187 y(.)1472 189 y(.)1472 190 y(.)1472 192 y(.)1472 207 y(.)1472 209 y(.)1472 210 y(.)1472 212 y(.)1472 214 y(.)1472 215 y(.)1472 217 y(.)1472 219 y(.)1472 220 y(.)1472 222 y(.)1472 237 y(.)1472 239 y(.)1472 240 y(.)1472 242 y(.)1472 244 y(.)1472 245 y(.)1472 247 y(.)1472 249 y(.)1472 250 y(.)1472 252 y(.)1472 267 y(.)1472 269 y(.)1472 270 y(.)1472 272 y(.)1472 274 y(.)1472 275 y(.)1472 277 y(.)1472 279 y(.)1472 280 y(.)1472 282 y(.)1472 297 y(.)1472 299 y(.)1472 300 y(.)1472 302 y(.)1472 304 y(.)1580 57 y(.)1580 59 y(.)1580 61 y(.)1580 62 y(.)1580 64 y(.)1579 66 y(.)1579 67 y(.)1579 69 y(.)h(.)1579 71 y(.)1579 73 y(.)1578 75 y(.)1578 77 y(.)1578 79 y(.)1578 80 y(.)g(.)1577 82 y(.)1577 84 y(.)1577 86 y(.)1577 88 y(.)1576 90 y(.)1576 92 y(.)g(.)1576 93 y(.)1576 95 y(.)1575 97 y(.)1575 99 y(.)1575 101 y(.)1575 102 y(.)g(.)1574 104 y(.)1574 106 y(.)1574 107 y(.)1574 109 y(.)1573 111 y(.)1573 113 y(.)g(.)1573 114 y(.)1573 116 y(.)1572 118 y(.)1572 119 y(.)1572 121 y(.)1572 122 y(.)g(.)1571 124 y(.)1571 126 y(.)1571 128 y(.)1570 130 y(.)1570 132 y(.)g(.)1570 134 y(.)1570 136 y(.)1569 137 y(.)1569 139 y(.)1569 141 y(.)g(.)1568 143 y(.)1568 145 y(.)1568 146 y(.)1567 148 y(.)1567 150 y(.)g(.)1567 152 y(.)1566 153 y(.)1566 155 y(.)1566 157 y(.)1565 158 y(.)g(.)1565 161 y(.)1564 163 y(.)1564 165 y(.)1564 167 y(.)g(.)1563 169 y(.)1563 170 y(.)1562 172 y(.)1562 174 y(.)g(.)1561 176 y(.)1561 178 y(.)1561 179 y(.)1560 181 y(.)1560 183 y(.)1559 184 y(.)1559 186 y(.)1559 187 y(.)1558 189 y(.)g(.)1558 191 y(.)1557 192 y(.)1557 194 y(.)1556 196 y(.)1556 198 y(.)1555 199 y(.)1555 201 y(.)1554 203 y(.)g(.)1554 204 y(.)1553 206 y(.)1553 208 y(.)1552 210 y(.)1551 212 y(.)1551 213 y(.)1550 215 y(.)g(.)1550 217 y(.)1549 218 y(.)1548 220 y(.)1548 222 y(.)1547 223 y(.)1546 225 y(.)1546 227 y(.)g(.)1545 228 y(.)1544 230 y(.)1544 232 y(.)1543 234 y(.)1542 235 y(.)1541 237 y(.)g(.)1540 239 y(.)1540 240 y(.)1539 242 y(.)1538 243 y(.)1537 245 y(.)1536 247 y(.)g(.)1535 248 y(.)1535 250 y(.)1534 251 y(.)1533 253 y(.)1532 254 y(.)1531 256 y(.)g(.)1530 257 y(.)1529 259 y(.)1528 261 y(.)1527 262 y(.)1525 264 y(.)g(.)1524 265 y(.)1523 266 y(.)1522 268 y(.)1521 269 y(.)1520 270 y(.)1519 272 y(.)1517 273 y(.)1516 274 y(.)1515 276 y(.)1514 277 y(.)1513 278 y(.)g(.)1511 280 y(.)1510 281 y(.)1509 282 y(.)1507 283 y(.)1506 284 y(.)1505 285 y(.)g(.)1503 286 y(.)1502 287 y(.)1500 288 y(.)1499 289 y(.)1497 290 y(.)1495 291 y(.)g(.)1494 292 y(.)1492 293 y(.)f(.)1489 294 y(.)1488 295 y(.)1486 296 y(.)g(.)h(.)1483 297 y(.)1482 298 y(.)1480 299 y(.)e(.)1477 300 y(.)1475 301 y(.)h(.)h(.)1472 302 y(.)e(.)1468 303 y(.)1467 304 y(.)g(.)1463 305 y(.)h(.)h(.)1460 306 y(.)e(.)1456 307 y(.)g(.)1453 308 y(.)g(.)1449 309 y(.)i(.)e(.)1446 310 y(.)g(.)g(.)1441 311 y(.)g(.)1438 312 y(.)g(.)i(.)e(.)1433 313 y(.)g(.)1429 314 y(.)h(.)f(.)1424 315 y(.)h(.)h(.)e(.)1420 316 y(.)g(.)g(.)1415 317 y(.)g(.)g(.)1410 318 y(.)i(.)e(.)g(.)1404 319 y(.)g(.)1400 320 y(.)h(.)f(.)i(.)e(.)1393 321 y(.)g(.)h(.)1388 322 y(.)f(.)g(.)i(.)1382 323 y(.)f(.)f(.)1377 324 y(.)h(.)f(.)1372 325 y(.)i(.)e(.)h(.)1367 326 y(.)g(.)f(.)1362 327 y(.)h(.)h(.)e(.)1357 328 y(.)h(.)f(.)1352 329 y(.)h(.)h(.)1349 330 y(.)e(.)1346 331 y(.)g(.)h(.)1341 332 y(.)h(.)e(.)1338 333 y(.)1336 334 y(.)g(.)1333 335 y(.)i(.)e(.)1330 336 y(.)g(.)1326 337 y(.)h(.)1323 338 y(.)h(.)e(.)1320 339 y(.)g(.)1316 340 y(.)h(.)1313 341 y(.)g(.)h(.)1310 342 y(.)1308 343 y(.)e(.)1304 344 y(.)h(.)1301 345 y(.)1299 346 y(.)h(.)f(.)1296 347 y(.)f(.)1292 348 y(.)h(.)1289 349 y(.)1287 350 y(.)g(.)h(.)1284 351 y(.)e(.)1280 352 y(.)1279 353 y(.)g(.)1275 354 y(.)g(.)1272 355 y(.)i(.)1270 356 y(.)e(.)1267 357 y(.)g(.)1263 358 y(.)1262 359 y(.)g(.)1259 360 y(.)g(.)i(.)1255 361 y(.)1253 362 y(.)e(.)1249 363 y(.)i(.)1248 364 y(.)e(.)1244 365 y(.)1242 366 y(.)i(.)e(.)1238 367 y(.)1236 368 y(.)g(.)i(.)1232 369 y(.)1230 370 y(.)1229 371 y(.)e(.)i(.)1225 372 y(.)1223 373 y(.)e(.)1219 374 y(.)i(.)1217 375 y(.)1215 376 y(.)e(.)1211 377 y(.)i(.)1210 378 y(.)e(.)1206 379 y(.)1205 380 y(.)g(.)1202 381 y(.)1200 382 y(.)g(.)1197 383 y(.)i(.)1195 384 y(.)e(.)1192 385 y(.)g(.)1188 386 y(.)1187 387 y(.)g(.)1184 388 y(.)1182 389 y(.)i(.)e(.)1179 390 y(.)1177 391 y(.)h(.)1174 392 y(.)1173 393 y(.)f(.)1170 394 y(.)1168 395 y(.)i(.)f(.)1165 396 y(.)1163 397 y(.)g(.)1160 398 y(.)1158 399 y(.)1157 400 y(.)f(.)i(.)1154 401 y(.)1152 402 y(.)1150 403 y(.)1148 404 y(.)f(.)1145 405 y(.)1143 406 y(.)h(.)1142 407 y(.)1140 408 y(.)f(.)1137 409 y(.)1136 410 y(.)1134 411 y(.)1132 412 y(.)h(.)1131 413 y(.)e(.)1128 414 y(.)1126 415 y(.)1125 416 y(.)1123 417 y(.)i(.)1122 418 y(.)1120 419 y(.)1119 420 y(.)1118 421 y(.)1116 422 y(.)1115 423 y(.)1113 424 y(.)1112 425 y(.)1111 426 y(.)1109 427 y(.)g(.)1108 428 y(.)1106 429 y(.)1105 430 y(.)1103 431 y(.)1102 432 y(.)g(.)1100 433 y(.)1099 435 y(.)1097 436 y(.)1096 437 y(.)1095 438 y(.)1093 439 y(.)g(.)1092 440 y(.)1091 441 y(.)1089 443 y(.)1088 444 y(.)1086 445 y(.)1085 446 y(.)g(.)1084 447 y(.)1083 448 y(.)1081 450 y(.)1080 451 y(.)1079 452 y(.)1078 453 y(.)1076 454 y(.)g(.)1075 455 y(.)1074 456 y(.)1073 457 y(.)1071 458 y(.)1070 460 y(.)1069 461 y(.)1068 462 y(.)g(.)1066 463 y(.)1065 464 y(.)1064 465 y(.)1062 466 y(.)1061 468 y(.)1060 469 y(.)1059 470 y(.)g(.)1057 471 y(.)1056 472 y(.)1055 473 y(.)1054 475 y(.)1052 476 y(.)1051 477 y(.)1050 478 y(.)g(.)1049 479 y(.)1047 480 y(.)1046 482 y(.)1045 483 y(.)1044 484 y(.)1042 485 y(.)1041 486 y(.)g(.)1040 488 y(.)1039 489 y(.)1038 490 y(.)1036 491 y(.)1035 492 y(.)1034 493 y(.)1033 494 y(.)g(.)1032 496 y(.)1030 497 y(.)1029 498 y(.)1028 500 y(.)1026 501 y(.)1025 502 y(.)g(.)1024 504 y(.)1023 505 y(.)1021 506 y(.)1020 507 y(.)1019 508 y(.)1018 510 y(.)1017 511 y(.)1015 512 y(.)1014 513 y(.)1013 515 y(.)1012 516 y(.)1011 517 y(.)g(.)1009 518 y(.)1008 520 y(.)1007 521 y(.)1006 522 y(.)1005 523 y(.)1004 525 y(.)1003 526 y(.)1002 527 y(.)1000 528 y(.)999 530 y(.)g(.)998 531 y(.)997 532 y(.)996 533 y(.)995 535 y(.)993 536 y(.)992 537 y(.)991 539 y(.)990 540 y(.)989 541 y(.)988 542 y(.)987 544 y(.)g(.)985 545 y(.)984 547 y(.)983 548 y(.)982 550 y(.)981 551 y(.)980 553 y(.)g(.)979 554 y(.)978 555 y(.)977 557 y(.)975 558 y(.)974 560 y(.)973 561 y(.)972 562 y(.)g(.)971 564 y(.)970 565 y(.)969 567 y(.)968 568 y(.)967 570 y(.)966 571 y(.)965 573 y(.)g(.)964 574 y(.)963 576 y(.)962 577 y(.)960 579 y(.)959 581 y(.)958 582 y(.)957 584 y(.)g(.)956 585 y(.)955 586 y(.)954 588 y(.)953 589 y(.)952 591 y(.)951 592 y(.)950 594 y(.)949 595 y(.)g(.)948 596 y(.)947 598 y(.)946 599 y(.)945 601 y(.)944 602 y(.)943 604 y(.)942 605 y(.)941 606 y(.)g(.)940 608 y(.)939 609 y(.)938 611 y(.)937 612 y(.)936 614 y(.)935 615 y(.)934 616 y(.)933 618 y(.)g(.)932 619 y(.)931 621 y(.)930 622 y(.)929 623 y(.)928 625 y(.)927 626 y(.)926 627 y(.)925 629 y(.)g(.)923 630 y(.)922 632 y(.)921 633 y(.)920 634 y(.)919 635 y(.)918 637 y(.)917 638 y(.)916 639 y(.)g(.)915 641 y(.)914 642 y(.)913 644 y(.)911 645 y(.)910 647 y(.)909 648 y(.)908 650 y(.)g(.)907 651 y(.)906 652 y(.)904 653 y(.)903 655 y(.)902 656 y(.)901 657 y(.)900 659 y(.)g(.)898 660 y(.)897 661 y(.)896 662 y(.)895 663 y(.)894 665 y(.)893 666 y(.)892 667 y(.)g(.)890 668 y(.)889 669 y(.)887 670 y(.)886 672 y(.)885 673 y(.)883 674 y(.)g(.)882 675 y(.)880 676 y(.)879 677 y(.)877 678 y(.)876 680 y(.)g(.)e(.)872 681 y(.)871 682 y(.)869 683 y(.)868 684 y(.)866 685 y(.)864 686 y(.)h(.)h(.)861 687 y(.)860 688 y(.)858 689 y(.)e(.)855 690 y(.)853 691 y(.)h(.)850 692 y(.)848 693 y(.)h(.)f(.)845 694 y(.)f(.)842 695 y(.)g(.)i(.)839 696 y(.)837 697 y(.)e(.)834 698 y(.)g(.)i(.)830 699 y(.)f(.)827 700 y(.)f(.)h(.)822 701 y(.)h(.)f(.)819 702 y(.)f(.)h(.)814 703 y(.)f(.)i(.)810 704 y(.)f(.)f(.)805 705 y(.)g(.)801 706 y(.)i(.)f(.)f(.)796 707 y(.)g(.)h(.)791 708 y(.)f(.)i(.)e(.)786 709 y(.)g(.)g(.)780 710 y(.)g(.)g(.)i(.)f(.)773 711 y(.)f(.)g(.)h(.)766 712 y(.)f(.)h(.)h(.)e(.)g(.)758 713 y(.)g(.)g(.)h(.)751 714 y(.)f(.)h(.)h(.)e(.)744 715 y(.)g(.)g(.)i(.)738 716 y(.)e(.)g(.)g(.)i(.)730 717 y(.)e(.)g(.)h(.)f(.)i(.)721 718 y(.)e(.)h(.)f(.)714 719 y(.)i(.)e(.)h(.)f(.)g(.)g(.)i(.)703 720 y(.)e(.)g(.)g(.)695 721 y(.)423 436 y Fw(D)263 875 y Fo(Figure)15 b(1:)22 b(A)16 b(DF)-5 b(A)15 b(pro)q(of)j(c)o(hec)o(k)o(er)13 b(reading)k(adjacen)o(t)f (lines)f(of)i(the)f(pro)q(of.)p 166 935 1634 2 v 75 1060 a(of)h(de\014ning)g (what)h(one)f(means)f(b)o(y)g(\\formal)h(system.")22 b(The)17 b(most)f(common)f(one)i(sa)o(ys)g(that)h(a)75 1120 y(formal)d(system)g(is)h (a)h(set)f(of)h(axioms)e(and)i(a)g(set)f(of)g(recursiv)o(e)f(rules)h(for)g (obtaining)h(new)g(state-)75 1180 y(men)o(ts)c(from)i(the)g(axioms.)k(All)14 b(the)h(axioms)f(and)i(the)f(statemen)o(ts)f(obtained)h(b)o(y)g(the)g(rep)q (eated)75 1240 y(application)22 b(of)h(these)e(rules)h(are)g(the)g(theorems)f (of)i(the)f(formal)f(system.)38 b(The)22 b(pro)q(of)h(of)g(a)75 1300 y(theorem)18 b(is)h(the)h(do)q(cumen)o(tation)e(of)i(ho)o(w)g(the)g (theorem)e(w)o(as)i(deriv)o(e)e(using)i(the)f(systematic)75 1361 y(application)f(of)g(rules)f(to)h(the)g(axioms)e(and)j(other)e (theorems.)25 b(The)18 b(notion)g(of)g(theorems)e(and)75 1421 y(pro)q(ofs)j(is)f(cen)o(tral)f(to)h(the)f(concept)h(of)g(a)g(formal)f (system.)24 b(The)18 b(idea)g(b)q(ehind)f(restricting)g(the)75 1481 y(rules)g(to)g(b)q(e)h(recursiv)o(e)d(is)j(that)f(one)h(w)o(an)o(ts)f (the)g(pro)q(of-c)o(hec)o(king)g(to)h(b)q(e)f(recursiv)o(e.)23 b(Although)75 1541 y(the)16 b(rules)h(are)g(only)f(restricted)g(to)h(b)q(e)g (recursiv)o(e,)d(they)j(are)f(exp)q(ected)g(to)h(b)q(e)g(fairly)f(simple)e (so)75 1601 y(the)g(pro)q(ofs)i(of)f(the)f(theorems)f(can)i(b)q(e)f(c)o(hec)o (k)o(ed)f(and)i(understo)q(o)q(d)h(with)e(ease.)21 b(In)14 b(what)h(follo)o(ws)75 1662 y(w)o(e)e(giv)o(e)f(an)i(equiv)m(alen)o(t)e (de\014nition)g(of)i(\\formal)f(system")f(whic)o(h)g(renders)h(pro)q(of-c)o (hec)o(king)g(v)o(ery)75 1722 y(simple.)27 b(This)19 b(formal)f(system)f(is)i (b)q(etter)g(suited)f(for)i(de\014ning)f(measures)f(of)h(computational)75 1782 y(complexit)o(y)e(on)k(pro)q(ofs)g(in)f(a)g(formal)f(system.)32 b(\(This)20 b(is)g(analogous)i(to)f(the)f(fact)g(that)h(T)l(ur-)75 1842 y(ing)e(mac)o(hines)f(are)h(b)q(etter)g(suited)g(for)h(the)f(study)h(of) g(computational)e(complexit)o(y)e(than)k(the)75 1902 y(Lam)o(b)q(da)c (Calculus,)g(ev)o(en)f(though)i(b)q(oth)h(are)e(mo)q(dels)f(of)i(computable)d (functions.\))148 1963 y(W)l(e)d(de\014ne)f(a)i(formal)e(system)f(to)i(b)q(e) g(a)h(set)e(of)i(pro)q(ofs)g(and)f(a)h(corresp)q(onding)g(set)f(of)g (theorems.)75 2023 y(The)16 b(k)o(ey)e(concept)h(in)h(the)f(de\014nition)g (of)h(\\formal)f(system")g(is)g(ho)o(w)h(a)g(pro)q(of)h(is)f(presen)o(ted)e (and)75 2083 y(v)o(eri\014ed.)27 b(In)18 b(our)h(\014rst)g(de\014nition)f(of) h(\\formal)f(system")g(w)o(e)g(insist)g(that)h(the)g(pro)q(of)h(m)o(ust)d(b)q (e)75 2143 y(presen)o(ted)f(as)h(a)g(sequence)f(of)g(horizon)o(tal)h(lines)f (written)g(on)h(a)g(t)o(w)o(o)f(dimensional)f(page.)23 b(Eac)o(h)75 2203 y(line)c(is)h(a)g(string)g(o)o(v)o(er)f(a)h(\014xed)g(alphab)q(et)g(and) h(is)f(written)f(in)h(a)g(left-justi\014ed)f(form)g(directly)75 2264 y(b)q(elo)o(w)i(the)g(preceding)f(line.)34 b(Moreo)o(v)o(er,)20 b(w)o(e)h(insist)f(that)i(the)e(pro)q(of)i(can)g(b)q(e)f(c)o(hec)o(k)o(ed)d (b)o(y)j(a)75 2324 y(deterministic)15 b(\014nite)i(automaton)h(\(DF)-5 b(A\))17 b(in)h(the)g(follo)o(wing)f(w)o(a)o(y)l(.)26 b(The)18 b(DF)-5 b(A)17 b(pro)q(of)j(c)o(hec)o(k)o(er)75 2384 y(starts)13 b(at)g(the)f(top-left)h(corner)f(of)h(the)f(page)h(and)g(reads)g(t)o(w)o(o)f (adjacen)o(t)h(sym)o(b)q(ols)e(at)i(a)g(time)d(from)75 2444 y(the)16 b(\014rst)g(t)o(w)o(o)g(lines)f(of)h(the)g(pro)q(of.)22 b(The)16 b(DF)-5 b(A)16 b(scans)g(the)g(input)g(in)g(an)g(oblivious)g (manner|it)75 2504 y(reads)f(the)g(\014rst)g(t)o(w)o(o)g(lines,)e(scanning)j (from)d(left)h(to)i(righ)o(t,)e(and)h(returns)g(to)g(the)g(left)f(margin)g (to)p eop %%Page: 5 5 bop 75 42 a Fo(read)16 b(the)f(second)h(and)g(third)f(lines,)f(left)h(to)h (righ)o(t,)f(and)h(so)g(forth.)21 b(\(See)15 b(Figure)g(1.\))22 b(When)15 b(the)75 102 y(DF)-5 b(A)16 b(reac)o(hes)f(the)i(b)q(ottom)f(righ)o (t)g(corner,)g(it)f(accepts)i(or)f(rejects.)21 b(The)c(pro)q(ofs)g(of)g(the)f (formal)75 162 y(system)g(are)h(exactly)f(those)i(sequences)e(of)i(lines)e (accepted)h(b)o(y)g(the)g(DF)-5 b(A)16 b(pro)q(of)j(c)o(hec)o(k)o(er,)14 b(and)75 222 y(the)f(theorems)g(of)h(the)f(formal)g(system)f(are)i(the)f (\014rst)h(lines)f(of)h(the)g(pro)q(ofs.)21 b(That)15 b(is,)e(w)o(e)h(assume) 75 282 y(that)j(all)e(pro)q(ofs)j(start)f(with)f(the)g(statemen)o(t)e(of)j(a) g(theorem)d(and)j(end)f(with)g(\\Q.E.D.")148 342 y(Let)c Fn(F)17 b Fo(b)q(e)c(a)f(formal)f(system)g(and)i Fj(D)821 349 y Fh(F)864 342 y Fo(b)q(e)f(the)g(corresp)q(onding)h(pro)q(of)h(c)o(hec)o(k)o(er,)c(as)j (describ)q(ed)75 403 y(ab)q(o)o(v)o(e.)75 495 y Fi(De\014nition)j Fo(The)g Fk(width)21 b Fo(of)c(a)g(pro)q(of)h(in)f Fn(F)k Fo(is)c(the)f (width)h(of)g(the)f(longest)i(line.)j(The)c Fk(width)k Fo(of)75 555 y(a)c(theorem)d Fj(T)23 b Fo(in)15 b Fn(F)5 b Fo(,)16 b(written)g Fk(width)t Fo(\()p Fj(D)831 562 y Fh(F)862 555 y Fj(;)8 b(T)f Fo(\))o(,)16 b(is)f(the)h(width)g(of)h(the)f(narro)o(w)o(est)g(pro)q(of)h(of) g Fj(T)22 b Fo(in)75 615 y Fn(F)5 b Fo(.)75 708 y Fi(De\014nition)15 b Fo(W)l(e)h(sa)o(y)g(that)g(a)h(language)g Fj(L)f Fo(is)g(in)f(PWT,)h(that)h (is,)e Fj(L)i Fo(is)e(a)i(set)f(of)g Fk(p)n(olynomial)r(ly-)75 768 y(wide)i(the)n(or)n(ems)t Fo(,)d(if)h(there)g(exist)f(a)i Fj(k)e Fn(\025)f Fo(1)j(and)g(a)f(formal)f(system)g Fn(F)5 b Fo(,)16 b(suc)o(h)g(that)300 873 y Fj(T)k Fn(2)14 b Fj(L)28 b Fn(\()-8 b(\))27 b Fj(T)c Fo(is)16 b(a)h(theorem)d(in)i Fn(F)21 b Fo(and)c Fk(width)t Fo(\()p Fj(D)1292 880 y Fh(F)1323 873 y Fj(;)8 b(T)f Fo(\))13 b Fj(<)h Fn(j)p Fj(T)7 b Fn(j)1529 853 y Fg(k)1560 873 y Fo(+)k Fj(k)r(:)148 978 y Fo(A)o(t)16 b(\014rst)g(glance,)g(our)h(de\014nition)f(of)h(\\formal)e(system")h(ma)o(y)e (seem)h(to)q(o)j(restrictiv)o(e.)h(After)75 1039 y(all,)h(the)h(DF)-5 b(A)19 b(pro)q(of)j(c)o(hec)o(k)o(er)17 b(cannot)k(ev)o(en)f(v)o(erify)e(if)i (the)g(statemen)o(t)f(of)h(the)g(theorem)f(has)75 1099 y(balanced)g(paren)o (theses.)30 b(Ho)o(w)o(ev)o(er,)17 b(the)i(DF)-5 b(A)19 b(pro)q(of)h(c)o(hec) o(k)o(er)c(can)k(v)o(erify)d(a)i(pro)q(of)i(that)e(the)75 1159 y(theorem)11 b(has)j(balanced)f(paren)o(theses.)20 b(W)l(e)13 b(claim)e(that)i(our)h(de\014nition)f(of)g(\\formal)f(system")g(is)75 1219 y(robust)17 b(b)o(y)f(sho)o(wing)h(that)f(replacing)g(the)g(DF)-5 b(A)15 b(pro)q(of)j(c)o(hec)o(k)o(er)c(with)i(more)f(p)q(o)o(w)o(erful)g (devices)75 1279 y(do)q(es)i(not)g(c)o(hange)f(the)g(class)g(PWT.)148 1340 y(In)e(our)g(de\014nition)f(of)h(a)h(formal)d(system)g(with)i(a)g(DF)-5 b(A)13 b(pro)q(of)i(c)o(hec)o(k)o(er,)d(w)o(e)h(tried)g(to)h(capture)75 1400 y(the)f(idea)f(that)h(it)g(should)g(b)q(e)g(\\easy")h(to)f(c)o(hec)o(k)e (if)h(one)h(line)f(of)h(the)g(pro)q(of)g(follo)o(ws)g(another.)21 b(This)75 1460 y(notion)f(of)g(\\easy")g(can)g(b)q(e)g(extended)f(to)h (recognition)f(in)g(p)q(olynomial)g(time.)29 b(F)l(or)20 b(example,)75 1520 y(let)15 b(the)h(v)o(eri\014er)f(b)q(e)h(a)h(T)l(uring)f(mac)o(hine)e (with)i(a)h(separate)f(w)o(ork)g(tap)q(e.)22 b(The)16 b(size)g(of)g(the)g(w)o (ork)75 1580 y(tap)q(e)j(is)e(b)q(ounded)i(b)o(y)f(a)g(p)q(olynomial)f(in)h (the)g(size)f(of)h(the)g(theorem.)25 b(The)18 b(v)o(eri\014er)e(still)h (scans)75 1641 y(the)h(pro)q(of)i(obliviously)l(,)e(but)h(no)o(w)g(it)f(can)h (cop)o(y)f(the)g(lines)g(of)h(the)g(pro)q(of)g(on)o(to)g(its)g(w)o(ork)g(tap) q(e)75 1701 y(and)h(sp)q(end)g(an)g(additional)g(amoun)o(t)f(of)g(time)f(\(p) q(olynomial)g(in)h(the)g(length)h(of)g(the)f(line)f(it)h(is)75 1761 y(reading\))14 b(to)f(c)o(hec)o(k)f(the)h(pro)q(of.)22 b(After)12 b(this)i(allotted)f(time,)e(the)i(v)o(eri\014er)f(con)o(tin)o(ues) h(to)h(read)f(the)75 1821 y(pro)q(of)j(obliviously)l(.)k(Let)15 b(PWT)665 1828 y Fd(p)n(oly)746 1821 y Fo(b)q(e)g(de\014ned)g(as)h(ab)q(o)o (v)o(e,)f(replacing)g(the)g(DF)-5 b(A)14 b(pro)q(of)j(c)o(hec)o(k)o(er)75 1881 y(b)o(y)g(a)g(p)q(olynomial)f(time)g(pro)q(of)i(c)o(hec)o(k)o(er.)k(W)l (e)17 b(sho)o(w)h(that)f(the)g(more)f(p)q(o)o(w)o(erful)h(pro)q(of)i(c)o(hec) o(k)o(er)75 1942 y(do)q(es)e(not)g(c)o(hange)f(the)g(class)g(of)h(p)q (olynomially)d(wide)i(theorems.)75 2050 y Fi(Theorem)h(1)24 b Fo(PWT)14 b(=)g(PWT)668 2057 y Fd(p)n(oly)734 2050 y Fo(.)75 2159 y Fi(Pro)r(of:)46 b Fo(Clearly)l(,)15 b(PWT)f Fn(\022)g Fo(PWT)755 2166 y Fd(p)n(oly)821 2159 y Fo(.)22 b(T)l(o)16 b(see)g(that)h(PWT)1232 2166 y Fd(p)n(oly)1311 2159 y Fn(\022)d Fo(PWT,)i(let)g Fj(L)e Fn(2)g Fo(PWT)1795 2166 y Fd(p)n(oly)1861 2159 y Fo(.)75 2219 y(Then,)i(there)g(is)g(a)g(formal)f(system)g Fn(F)21 b Fo(and)c(a)g(T)l(uring)f(mac)o(hine)e Fj(M)1334 2226 y Fh(F)1381 2219 y Fo(suc)o(h)i(that)297 2324 y Fj(T)k Fn(2)14 b Fj(L)28 b Fn(\()-8 b(\))27 b Fj(T)22 b Fo(is)17 b(a)f(theorem)f(in)h Fn(F)21 b Fo(and)c Fk(width)t Fo(\()p Fj(M)1296 2331 y Fh(F)1326 2324 y Fj(;)8 b(T)f Fo(\))13 b Fj(<)h Fn(j)p Fj(T)7 b Fn(j)1532 2304 y Fg(k)1564 2324 y Fo(+)k Fj(k)r(:)75 2430 y Fo(W)l(e)21 b(can)g(construct)g(a)g(new)g(formal)f(system)f Fn(F)992 2409 y Fh(0)1025 2430 y Fo(where)h(the)h(pro)q(ofs)h(can)g(b)q(e)f(v)o(eri\014ed)e (b)o(y)i(an)75 2490 y(oblivious)15 b(\014nite)f(automaton.)22 b(T)l(o)15 b(do)h(this,)f(simply)e(annotate)j(the)f(pro)q(ofs)h(in)f Fn(F)20 b Fo(b)o(y)15 b(inserting,)75 2550 y(b)q(et)o(w)o(een)21 b(the)g(lines,)h(the)g(instan)o(taneous)g(descriptions)g(\(ID\))f(of)h(the)g (computation)f(of)h Fj(M)1831 2557 y Fh(F)1861 2550 y Fo(.)p eop %%Page: 6 6 bop 75 42 a Fo(Since)19 b(the)g(ID's)h(c)o(hange)f(only)h(near)g(the)f(tap)q (e)i(heads,)f(a)h(\014nite)e(automaton)h(that)g(has)g Fj(M)1811 49 y Fh(F)1842 42 y Fo('s)75 102 y(transition)c(table)g(can)h(v)o(erify)d (that)j Fj(M)797 109 y Fh(F)844 102 y Fo(accepted)f(the)g(pro)q(of.)22 b(Th)o(us,)16 b Fj(L)e Fn(2)g Fo(PWT.)184 b Fc(2)148 226 y Fo(Ev)o(en)17 b(the)g(concept)g(of)h(explicit)d(lines)h(are)i(not)g(essen)o (tial)e(in)h(these)g(de\014nitions.)25 b(Consider)75 286 y(a)18 b(formal)e(system)g(whose)i(pro)q(ofs)g(are)g(presen)o(ted)e(as)i(a)g(single) f(line)f(and)i(the)f(pro)q(of)h(c)o(hec)o(k)o(er)d(is)75 347 y(a)h(t)o(w)o(o-headed)f(\014nite)f(automaton,)i(scanning)f(the)g(pro)q(of)i (from)d(left)g(to)i(righ)o(t.)k(Here)14 b(the)h(width)75 407 y(of)20 b(the)g(pro)q(of)g(is)g(the)g(maxim)n(um)c(separation)k(of)g(the)g (heads.)32 b(De\014ne)20 b(PWT)1548 414 y Ff(1)p Fh(\000)p Fd(line)1674 407 y Fo(to)g(b)q(e)g(the)75 467 y(class)f(of)f(languages)i(con) o(taining)e(p)q(olynomially)f(wide)h(theorems)f(under)i(this)f(new)g (de\014nition)75 527 y(of)f(width.)k(Again,)16 b(this)g(mo)q(del)f(yields)g (the)h(same)f(class)h(PWT.)75 641 y Fi(Theorem)h(2)24 b Fo(PWT)14 b(=)g(PWT)668 648 y Ff(1)p Fh(\000)p Fd(line)774 641 y Fo(.)75 754 y Fi(Pro)r(of:)49 b Fo(Let)17 b Fj(L)e Fn(2)g Fo(PWT.)24 b(Let)17 b Fn(F)k Fo(and)d Fj(D)897 761 y Fh(F)945 754 y Fo(b)q(e)f(the)f (formal)g(system)f(and)j(the)f(pro)q(of)h(c)o(hec)o(k)o(er)75 814 y(for)j(the)f(language)h Fj(L)p Fo(.)34 b(T)l(o)21 b(giv)o(e)e(a)i (one-dimensional)e(pro)q(of)j(that)f Fj(T)27 b Fn(2)21 b Fj(L)p Fo(,)g(simply)d(tak)o(e)i(the)75 874 y(t)o(w)o(o-dimensional)e(pro)q(of)j (and)f(concatenate)f(the)h(lines)e(to)i(form)f(one)h(long)g(line.)30 b(A)19 b(DF)-5 b(A)19 b Fj(D)1863 856 y Fh(0)75 935 y Fo(with)13 b(t)o(w)o(o)g(heads)h(can)f(sim)o(ulate)e Fj(D)722 942 y Fh(F)766 935 y Fo(reading)i(t)o(w)o(o)g(adjacen)o(t)g(sym)o(b)q(ols)f(of)i(the)f(t)o (w)o(o)g(dimensional)75 995 y(pro)q(of)21 b(b)o(y)e(k)o(eeping)f(the)h(t)o(w) o(o)g(heads)h(in)f(the)h(correct)e(p)q(ositions)j(along)f(the)f(single-line)f (pro)q(of.)75 1055 y(Since)12 b Fj(D)239 1062 y Fh(F)282 1055 y Fo(reads)h(sym)o(b)q(ols)f(only)g(from)g(adjacen)o(t)g(lines,)g Fj(D)1158 1037 y Fh(0)1183 1055 y Fo(can)h(sim)o(ulate)d Fj(D)1499 1062 y Fh(F)1543 1055 y Fo(without)j(mo)o(ving)75 1115 y(its)j(heads)h (further)f(apart)h(than)g(the)f(width)g(of)g(the)g(original)g(pro)q(of.)23 b(So,)16 b Fj(L)e Fn(2)g Fo(PWT)1665 1122 y Ff(1)p Fh(\000)p Fd(line)1771 1115 y Fo(.)148 1175 y(On)j(the)g(other)g(hand,)h(if)e Fj(L)f Fn(2)h Fo(PWT)840 1182 y Ff(1)p Fh(\000)p Fd(line)947 1175 y Fo(,)g(then)h(for)g(an)o(y)g Fj(T)22 b Fn(2)15 b Fj(L)p Fo(,)i(let)g Fj(w)h Fo(b)q(e)f(the)g(width)g(of)75 1236 y(the)d(pro)q(of)i (of)e Fj(T)7 b Fo(.)20 b(T)l(o)15 b(giv)o(e)f(a)h(t)o(w)o(o-dimensional)d (pro)q(of)k(that)f Fj(T)20 b Fn(2)14 b Fj(L)p Fo(,)h(simply)d(divide)h(the)h (single-)75 1296 y(line)f(pro)q(of)i(in)o(to)e(segmen)o(ts)g(of)h(length)g Fj(w)h Fo(and)g(arrange)f(the)g(segmen)o(ts)f(in)o(to)g(a)i(t)o(w)o (o-dimensional)75 1356 y(pro)q(of)j(b)o(y)f(listing)f(the)h(segmen)o(ts)e (one)i(b)q(elo)o(w)g(the)g(other.)23 b(A)17 b(p)q(olynomial)f(time)e(pro)q (of)19 b(c)o(hec)o(k)o(er)75 1416 y Fj(M)j Fo(can)16 b(sim)o(ulate)e(the)i(t) o(w)o(o-headed)g(DF)-5 b(A,)15 b Fj(D)q Fo(,)i(reading)f(a)h(single-line)e (pro)q(of,)i(b)q(ecause)f Fj(M)22 b Fo(can)75 1476 y(record)15 b(the)g(last)g(t)o(w)o(o)g(lines)g(of)g(the)g(pro)q(of)i(in)d(its)h(w)o(ork)h (tap)q(e.)21 b(Since)14 b Fj(D)j Fo(nev)o(er)d(mo)o(v)o(es)g(its)h(heads)75 1537 y(greater)d(than)h Fj(w)g Fo(tap)q(e)f(cells)f(apart,)i Fj(M)k Fo(only)12 b(needs)g(the)g(last)g(t)o(w)o(o)g(lines)f(of)h(the)g(t)o (w)o(o-dimensional)75 1597 y(pro)q(of)17 b(to)g(sim)o(ulate)d Fj(D)q Fo(.)22 b(Th)o(us,)16 b(PWT)789 1604 y Ff(1)p Fh(\000)p Fd(line)909 1597 y Fn(\022)d Fo(PWT)1080 1604 y Fd(p)n(oly)1160 1597 y Fn(\022)g Fo(PWT.)478 b Fc(2)148 1721 y Fo(Finally)l(,)14 b(in)h(b)q(oth)h(mo)q(dels)e(with)h(\014nite)g(automata)g(v)o(eri\014ers,)f (w)o(e)h(can)g(allo)o(w)g(the)g(v)o(eri\014er)f(to)75 1781 y(ha)o(v)o(e)19 b(freer)g(mo)o(v)o(eme)o(n)o(ts.)30 b(In)19 b(the)h(t)o(w)o(o)g(dimensional)e(case,)i(w)o(e)g(can)g(remo)o(v)o(e)d(the)j (restriction)75 1842 y(that)15 b(the)g(v)o(eri\014er)e(m)o(ust)h(read)h(the)f (pro)q(of)i(in)f(an)g(oblivious)g(manner)f(and)h(allo)o(w)g(it)f(to)i(mo)o(v) o(e)c(up,)75 1902 y(do)o(wn,)j(left)e(or)h(righ)o(t)g(at)h(an)o(y)f(time.)k (De\014ne)c(PWT)1017 1910 y Fh($)-30 b(l)1064 1902 y Fo(to)15 b(b)q(e)f(the)g(class)g(of)h(languages)g(con)o(taining)75 1962 y(p)q(olynomially)f(wide)i(theorems)f(under)h(this)g(non-oblivious)h(DF)-5 b(A)16 b(v)o(eri\014er)e(mo)q(del.)75 2075 y Fi(Theorem)j(3)24 b Fo(PWT)14 b(=)g(PWT)668 2083 y Fh($)-30 b(l)701 2075 y Fo(.)75 2189 y Fi(Pro)r(of:)53 b Fo(Clearly)l(,)17 b(PWT)g Fn(\022)f Fo(PWT)769 2197 y Fh($)-30 b(l)803 2189 y Fo(.)26 b(T)l(o)18 b(see)f(that)i(PWT)1222 2197 y Fh($)-30 b(l)1272 2189 y Fn(\022)16 b Fo(PWT,)i(note)g(that)h(the)e(non-)75 2249 y(oblivious)f(DF)-5 b(A)15 b(pro)q(of)i(c)o(hec)o(k)o(er)c(is)j(deterministic,)c(so)17 b(it)f(cannot)g(b)q(e)g(in)g(the)g(same)f(state)h(when)75 2309 y(it)i(revisits)g(a)h(lo)q(cation)g(in)g(the)f(t)o(w)o(o)h(dimensional)e (page.)29 b(If)18 b(it)h(do)q(es,)g(it)g(will)e(lo)q(op)j(and)f(nev)o(er)75 2369 y(accept)14 b(the)h(pro)q(of.)21 b(Since)14 b(the)h(n)o(um)o(b)q(er)e (of)h(states)i(is)e(constan)o(t,)h(the)g(DF)-5 b(A)13 b(can)i(only)g(visit)f (eac)o(h)75 2430 y(lo)q(cation)21 b(a)f(constan)o(t)h(n)o(um)o(b)q(er)d(of)i (times.)31 b(Th)o(us,)21 b(to)g(con)o(v)o(ert)e(a)h(pro)q(of)i(for)e(a)h (non-oblivious)75 2490 y(DF)-5 b(A)15 b(v)o(eri\014er)g(in)o(to)g(one)i(that) f(an)h(oblivious)e(DF)-5 b(A)16 b(pro)q(of)h(v)o(eri\014er)d(can)i(c)o(hec)o (k,)e(one)i(simply)e(has)75 2550 y(to)j(include,)d(at)j(eac)o(h)e(lo)q (cation)i(on)f(the)g(page,)g(a)h(list)f(describing)f(state)h(and)h(direction) e(of)i(head)p eop %%Page: 7 7 bop 75 42 a Fo(mo)o(v)o(em)o(en)o(t)11 b(of)k(the)g(non-oblivious)g(DF)-5 b(A)13 b(during)i(eac)o(h)f(visit)g(to)h(that)g(lo)q(cation.)21 b(The)14 b(oblivious)75 102 y(DF)-5 b(A)14 b(pro)q(of)i(c)o(hec)o(k)o(er)c (can)j(v)o(erify)e(that)j(the)e(list)g(at)i(eac)o(h)e(lo)q(cation)h(is)g (consisten)o(t)f(with)h(the)f(lists)75 162 y(at)h(neigh)o(b)q(oring)h(lo)q (cations,)f(b)q(ecause)g(there)g(is)g(only)f(a)i(constan)o(t)f(n)o(um)o(b)q (er)f(of)h(p)q(ossible)g(lists.)20 b(It)75 222 y(can)e(also)h(v)o(erify)d (that)j(the)f(non-oblivious)g(DF)-5 b(A)18 b(en)o(tered)e(the)i(pro)q(of)i (at)e(the)g(top)g(left)g(corner,)75 282 y(and)f(accepted)e(in)h(the)g(b)q (ottom)g(righ)o(t)g(corner.)21 b(Hence,)15 b(PWT)1246 290 y Fh($)-30 b(l)1293 282 y Fn(\022)14 b Fo(PWT.)344 b Fc(2)148 407 y Fo(Similarly)l(,)22 b(for)i(the)g(formal)f(system)f(where)h(the)h(pro)q (of)h(is)e(presen)o(ted)g(in)h(one)g(line)e(and)75 467 y(the)c(v)o(eri\014er) f(is)h(a)g(t)o(w)o(o-headed)h(\014nite)e(automaton,)i(w)o(e)f(can)g(allo)o(w) g(b)q(oth)h(heads)g(to)g(mo)o(v)o(e)d(left)75 527 y(and)i(righ)o(t.)24 b(De\014ne)18 b(PWT)582 534 y Fh($)637 527 y Fo(to)g(b)q(e)f(the)h(class)f (of)h(languages)h(con)o(taining)e(p)q(olynomially)e(wide)75 587 y(theorems)g(under)h(this)g(new)g(de\014nition)g(of)h(width.)75 702 y Fi(Theorem)g(4)24 b Fo(PWT)14 b(=)g(PWT)668 709 y Fh($)705 702 y Fo(.)75 816 y Fi(Pro)r(of:)71 b Fo(By)22 b(Theorem)e(2,)k(PWT)g Fn(\022)g Fo(PWT)977 823 y Ff(1)p Fh(\000)p Fd(line)1107 816 y Fn(\022)g Fo(PWT)1289 823 y Fh($)1326 816 y Fo(.)39 b(F)l(or)22 b(an)o(y)g(language)h Fj(L)f Fo(in)75 876 y(PWT)194 883 y Fh($)231 876 y Fo(,)16 b(let)g Fn(F)21 b Fo(and)c Fj(D)524 883 y Fh(F)572 876 y Fo(b)q(e)g(the)f(formal)g(system)f(and)i(the)f(t)o(w)o(o-headed)h(DF)-5 b(A)16 b(pro)q(of)i(c)o(hec)o(k)o(er)75 936 y(for)h Fn(F)t Fo(.)28 b(Supp)q(ose)19 b Fj(D)467 943 y Fh(F)517 936 y Fo(is)f(c)o(hec)o (king)f(if)h(a)g(string)h Fj(x)f Fo(is)g(a)h(pro)q(of)h(in)e Fn(F)t Fo(.)28 b(Let)18 b Fj(w)i Fo(b)q(e)f(the)f(greatest)75 996 y(distance)k(separating)i(the)e(t)o(w)o(o)h(tap)q(e)g(heads)g(of)g Fj(D)1063 1003 y Fh(F)1116 996 y Fo(while)f(v)o(erifying)f Fj(x)p Fo(.)40 b(A)22 b(deterministic)75 1056 y(T)l(uring)c(mac)o(hine)e Fj(M)23 b Fo(with)18 b(one)g(input)g(head)g(and)g(a)h(separate)f(w)o(ork)g (tap)q(e)g(can)g(sim)o(ulate)e Fj(D)1844 1063 y Fh(F)75 1117 y Fo(using)k(no)g(more)e(than)i(log)9 b Fj(w)21 b Fo(tap)q(e)f(cells)e(on)i (its)f(w)o(ork)h(tap)q(e.)31 b Fj(M)25 b Fo(will)18 b(simply)f(use)j(the)f(w) o(ork)75 1177 y(tap)q(e)f(to)g(k)o(eep)f(trac)o(k)g(of)h(the)g(distance)f(b)q (et)o(w)o(een)g(the)g(t)o(w)o(o)h(tap)q(e)g(heads)g(of)h Fj(D)1535 1184 y Fh(F)1566 1177 y Fo(.)25 b(Since)17 b Fj(M)23 b Fo(has)75 1237 y(only)d(p)q(olynomially)d(man)o(y)i(w)o(ork)g(tap)q(e)i (con\014gurations,)g(it)f(can)g(only)f(visit)g(eac)o(h)g(sym)o(b)q(ol)g(of)75 1297 y Fj(x)f Fo(p)q(olynomially)f(man)o(y)g(times)g(without)i(lo)q(oping.)29 b(Then,)18 b(as)i(in)e(the)g(pro)q(ofs)i(of)f(Theorems)f(2)75 1357 y(and)g(3,)f(w)o(e)g(can)h(con)o(v)o(ert)e(the)h(one)g(line)f(pro)q(of)j (in)o(to)d(a)i(t)o(w)o(o)f(dimensional)f(pro)q(of)i(and)g(annotate)75 1418 y(the)e(pro)q(of)i(with)e Fj(M)5 b Fo('s)17 b(crossing)g(sequence.)k (This)c(will)e(c)o(hange)i(the)f(width)h(of)g(the)f(pro)q(of)i(b)o(y)e(at)75 1478 y(most)j(a)i(p)q(olynomial.)31 b(Also,)20 b(since)f(the)h(depth)g(of)g (eac)o(h)g(crossing)g(sequence)f(is)h(p)q(olynomial,)75 1538 y(an)k(oblivious)f(p)q(olynomial)g(time)e(pro)q(of)k(c)o(hec)o(k)o(er)c(can)j (v)o(erify)e(that)i(the)f(crossing)h(sequence)75 1598 y(at)d(eac)o(h)f(lo)q (cation)i(is)e(consisten)o(t)g(with)h(the)g(crossing)g(sequences)f(of)h(its)f (neigh)o(b)q(ors.)36 b(Hence,)75 1658 y(PWT)194 1665 y Fh($)245 1658 y Fn(\022)13 b Fo(PWT)416 1665 y Fd(p)n(oly)496 1658 y Fn(\022)g Fo(PWT.)1158 b Fc(2)148 1756 y Fo(As)20 b(the)f(reader)g(ma)o(y)g (ha)o(v)o(e)f(susp)q(ected,)j(there)e(is)g(a)h(go)q(o)q(d)i(reason)e(wh)o(y)g (all)f(these)g(classes)75 1816 y(turn)g(out)h(to)g(b)q(e)f(PWT.)h(The)f (reason)h(is)f(that)h(the)f(v)o(eri\014ers)f(in)h(these)g(formal)f(systems)g (ha)o(v)o(e)75 1876 y(enough)e(p)q(o)o(w)o(er)g(to)g(c)o(hec)o(k)e(v)m(alid)h (computations.)21 b(Hence,)14 b(restricting)h(the)g(width)h(of)f(the)h(pro)q (of)75 1937 y(to)g(b)q(e)f(p)q(olynomial)f(in)h(the)h(size)e(of)i(the)f (theorem)f(is)h(equiv)m(alen)o(t)f(to)h(restricting)g(the)g(size)g(of)g(the) 75 1997 y(instan)o(taneous)h(descriptions)f(of)h(a)g(T)l(uring)f(mac)o(hine)e (computation)i(to)h(b)q(e)f(p)q(olynomial)f(in)h(the)75 2057 y(size)g(of)i(the)f(input)g(string.)21 b(But,)16 b(this)g(is)g(just)g(PSP)l (A)o(CE)q(.)21 b(\(See)15 b([Fis69])h(for)h(related)e(results.\))75 2171 y Fi(Theorem)i(5)24 b Fo(PWT)14 b(=)g(PSP)l(A)o(CE.)75 2285 y Fi(Pro)r(of:)57 b Fo(Let)19 b Fj(L)g Fn(2)f Fo(PWT.)30 b(Then,)19 b(using)g(our)h(\014rst)f(de\014nition)f(of)i(\\formal)e(system",) g(there)75 2346 y(exist)d(a)i(constan)o(t)g Fj(k)h Fo(and)f(a)g(formal)e (system)f(with)j(a)f(DF)-5 b(A)16 b(pro)q(of)h(c)o(hec)o(k)o(er,)c Fj(D)1541 2353 y Fh(F)1572 2346 y Fo(,)j(suc)o(h)g(that)300 2456 y Fj(T)k Fn(2)14 b Fj(L)28 b Fn(\()-8 b(\))27 b Fj(T)c Fo(is)16 b(a)h(theorem)d(in)i Fn(F)21 b Fo(and)c Fk(width)t Fo(\()p Fj(D)1292 2463 y Fh(F)1323 2456 y Fj(;)8 b(T)f Fo(\))13 b Fj(<)h Fn(j)p Fj(T)7 b Fn(j)1529 2435 y Fg(k)1560 2456 y Fo(+)k Fj(k)r(:)p eop %%Page: 8 8 bop 75 42 a Fo(On)17 b(input)g Fj(T)7 b Fo(,)16 b(a)i(nondeterministic)c(T)l (uring)k(mac)o(hine)c Fj(M)23 b Fo(can)17 b(guess)h(a)f(width)g Fj(m)p Fo(,)g(guess)h(suc-)75 102 y(cessiv)o(e)d(lines)g(of)i(length)f Fj(m)p Fo(,)f(and)i(use)f Fj(D)840 109 y Fh(F)888 102 y Fo(to)g(c)o(hec)o(k)f (if)h(the)g(lines)f(form)g(a)i(pro)q(of)g(of)g Fj(T)23 b Fo(in)15 b Fn(F)5 b Fo(.)22 b(If)75 162 y(suc)o(h)16 b(a)h(pro)q(of)g(is)f(found,)g Fj(M)22 b Fo(accepts.)f(Clearly)l(,)682 263 y Fj(T)f Fn(2)14 b Fj(L)28 b Fn(\()-8 b(\))27 b Fj(M)5 b Fo(\()p Fj(T)i Fo(\))16 b(accepts)p Fj(:)75 363 y Fo(Since)f(NPSP)l(A)o(CE)f Fn(\022)f Fo(PSP)l(A)o(CE,)j Fj(L)e Fn(2)g Fo(PSP)l(A)o(CE.)148 424 y(Con)o(v)o(ersely) l(,)23 b(supp)q(ose)g(that)g Fj(L)i Fn(2)g Fo(PSP)l(A)o(CE.)41 b(Then,)24 b(there)e(is)g(a)h(T)l(uring)g(mac)o(hine)e Fj(M)75 484 y Fo(whic)o(h)14 b(recognizes)g Fj(L)p Fo(.)21 b(W)l(e)14 b(can)h(de\014ne)f(a)h(formal)e(pro)q(of)j(system)d(that)i(uses)g(the)f (instan)o(taneous)75 544 y(descriptions)k(\(ID\))g(of)h Fj(M)24 b Fo(as)19 b(the)f(lines)g(of)h(a)g(pro)q(of.)29 b(Since)17 b(the)i(ID's)f(only)g(c)o(hange)h(near)f(the)75 604 y(tap)q(e)13 b(head,)g(a)g(DF)-5 b(A)12 b(can)h(c)o(hec)o(k)e(if)h(one)h(ID)f(follo)o(ws)h (another)g(according)g(to)g(the)f(transition)h(table)75 664 y(of)j Fj(M)5 b Fo(.)22 b(Moreo)o(v)o(er,)14 b(the)i(length)f(of)h(the)g (ID's)g(are)f(p)q(olynomial)g(in)h(the)f(size)g(of)h(the)g(input)g(string)75 725 y Fj(T)7 b Fo(,)21 b(so)g(the)f(width)h(of)f(the)h(pro)q(of)g(is)g(p)q (olynomial)e(in)h Fn(j)p Fj(T)7 b Fn(j)p Fo(.)33 b(Th)o(us,)22 b(there)e(is)g(a)h(formal)e(system)75 785 y(whic)o(h)d(pro)o(v)o(es)f (exactly)g(the)h(strings)h(in)f Fj(L)g Fo(using)h(p)q(olynomially-wide)d(pro) q(ofs.)23 b(So,)780 886 y(PWT)14 b(=)g(PSP)l(A)o(CE)p Fj(:)1822 986 y Fc(2)148 1111 y Fo(Note)i(that)g(the)g(role)f(of)i Fk(p)n(olynomial)k Fo(width)16 b(w)o(as)g(not)h(essen)o(tial)e(in)g(pro)o(ving)h(these)g (results.)75 1171 y(W)l(e)c(can)g(easily)g(de\014ne)g(Exp)q(onen)o(tially)f (Wide)h(Theorems)f(and)i(sho)o(w)g(similar)d(robustness)j(prop-)75 1231 y(erties.)21 b(These)c(observ)m(ations)g(sho)o(w)g(that)g(the)f (de\014nition)g(of)h(the)g(width)f(of)h(a)g(pro)q(of)g(is)g(robust,)75 1291 y(and)f(w)o(e)f(b)q(eliev)o(e)f(it)h(prop)q(erly)g(captures)h(the)f(in)o (tuitiv)o(e)e(idea)i(of)h(width.)21 b(In)15 b(essence,)g(the)g(width)75 1352 y(of)g(a)f(pro)q(of)i(quan)o(ti\014es)d(ho)o(w)i(m)o(uc)o(h)d (information)h(a)i(v)o(eri\014er)e(needs)h(c)o(hec)o(k)e(a)j(pro)q(of)g(and)g (ho)o(w)g(far)75 1412 y(this)h(information)f(can)i(b)q(e)f(separated)h(in)f (the)g(pro)q(of.)75 1577 y Fp(3)83 b(Conclusion)148 1686 y Fo(F)l(rom)15 b(the)h(previous)g(consideration,)g(w)o(e)g(see)g(that)721 1787 y(IP)e(=)g(PSP)l(A)o(CE)g(=)f(PWT)p Fj(:)75 1888 y Fo(Recall)21 b(that)i(NP)g(is)f(the)g(class)h(of)g(languages)h(with)e(p)q(olynomially)f (long)i(pro)q(ofs.)41 b(PWT)23 b(is)75 1948 y(the)16 b(class)g(of)h (languages)h(with)e(p)q(olynomially)e(wide)i(pro)q(ofs)i(whose)f(length)f(ma) o(y)e(not)j(b)q(e)g(p)q(oly-)75 2008 y(nomially)22 b(b)q(ounded.)44 b(By)24 b(comparing)f(IP)g(and)h(PWT)h(w)o(e)e(can)h(see)f(ho)o(w)i(in)o (teraction)d(and)75 2068 y(probabilistic)15 b(acceptance)h(can)g(shorten)h (the)f(amoun)o(t)g(of)g(time)e(required)h(to)i(c)o(hec)o(k)d(a)j(pro)q(of.) 148 2129 y(F)l(or)j(example,)d(if)i(NP)g Fn(6)p Fo(=)g(PSP)l(A)o(CE,)g(then)g (there)g(are)h(formal)e(systems)g(where)h(all)g(of)g(the)75 2189 y(theorems)f(ha)o(v)o(e)g(p)q(olynomial)g(width,)i(but)f(some)f(of)i (the)f(pro)q(ofs)h(ha)o(v)o(e)e(lengths)i(that)f(are)h(not)75 2249 y(b)q(ounded)12 b(b)o(y)f(an)o(y)g(p)q(olynomial)f(\(in)g(the)h(size)f (of)i(the)f(theorem\).)18 b(Th)o(us,)12 b(in)e(these)h(formal)f(systems)75 2309 y(the)16 b(pro)q(of)i(cannot)g(alw)o(a)o(ys)e(b)q(e)h(presen)o(ted)f(in) g(p)q(olynomial)g(time.)k(Ho)o(w)o(ev)o(er,)15 b(one)i(can)g(presen)o(t)75 2369 y(a)g(probabilistic)e(pro)q(of)j(in)e(p)q(olynomial)f(time,)f(b)q (ecause)j(IP)d(=)g(PSP)l(A)o(CE.)22 b(If)15 b(NP)f Fn(6)p Fo(=)g(PSP)l(A)o (CE,)75 2430 y(then)i(the)g(whole)g(range)h(of)g(languages)g(in)f(PSP)l(A)o (CE)11 b Fn(\000)g Fo(NP)16 b(are)g(of)h(this)f(t)o(yp)q(e.)148 2490 y(Note)j(that)g(the)g(languages)i(in)e(PSP)l(A)o(CE)g(ma)o(y)e(require)h (exp)q(onen)o(tially)g(long)h(pro)q(ofs.)32 b(So)75 2550 y(if)16 b(PSP)l(A)o(CE)d Fn(6)p Fo(=)h(NEXP,)h(then)h(there)g(are)g(languages)i(whic) o(h)d(ha)o(v)o(e)g(exp)q(onen)o(tially)g(long)i(pro)q(ofs)p eop %%Page: 9 9 bop 94 673 16 4 v 125 673 V 155 673 V 186 673 V 217 673 V 248 673 V 279 673 V 309 673 V 340 673 V 371 673 V 402 673 V 432 673 V 463 673 V 494 673 V 525 673 V 555 673 V 586 673 V 617 673 V 648 673 V 678 673 V 94 635 V 125 635 V 155 635 V 186 635 V 217 635 V 248 635 V 279 635 V 309 635 V 340 635 V 371 635 V 402 635 V 432 635 V 463 635 V 494 635 V 525 635 V 555 635 V 586 635 V 617 635 V 648 635 V 678 635 V 94 598 V 125 598 V 155 598 V 186 598 V 217 598 V 248 598 V 279 598 V 309 598 V 340 598 V 371 598 V 402 598 V 432 598 V 463 598 V 494 598 V 525 598 V 555 598 V 586 598 V 617 598 V 648 598 V 678 598 V 94 560 V 125 560 V 155 560 V 186 560 V 217 560 V 248 560 V 279 560 V 309 560 V 340 560 V 371 560 V 402 560 V 432 560 V 463 560 V 494 560 V 525 560 V 555 560 V 586 560 V 617 560 V 648 560 V 678 560 V 94 523 V 125 523 V 155 523 V 186 523 V 217 523 V 248 523 V 279 523 V 309 523 V 340 523 V 371 523 V 402 523 V 432 523 V 463 523 V 494 523 V 525 523 V 555 523 V 586 523 V 617 523 V 648 523 V 678 523 V 94 485 V 125 485 V 155 485 V 186 485 V 217 485 V 248 485 V 279 485 V 309 485 V 340 485 V 371 485 V 402 485 V 432 485 V 463 485 V 494 485 V 525 485 V 555 485 V 586 485 V 617 485 V 648 485 V 678 485 V 94 448 V 125 448 V 155 448 V 186 448 V 217 448 V 248 448 V 279 448 V 309 448 V 340 448 V 371 448 V 402 448 V 432 448 V 463 448 V 494 448 V 525 448 V 555 448 V 586 448 V 617 448 V 648 448 V 678 448 V 94 410 V 125 410 V 155 410 V 186 410 V 217 410 V 248 410 V 279 410 V 309 410 V 340 410 V 371 410 V 402 410 V 432 410 V 463 410 V 494 410 V 525 410 V 555 410 V 586 410 V 617 410 V 648 410 V 678 410 V 94 373 V 125 373 V 155 373 V 186 373 V 217 373 V 248 373 V 279 373 V 309 373 V 340 373 V 371 373 V 402 373 V 432 373 V 463 373 V 494 373 V 525 373 V 555 373 V 586 373 V 617 373 V 648 373 V 678 373 V 94 335 V 125 335 V 155 335 V 186 335 V 217 335 V 248 335 V 279 335 V 309 335 V 340 335 V 371 335 V 402 335 V 432 335 V 463 335 V 494 335 V 525 335 V 555 335 V 586 335 V 617 335 V 648 335 V 678 335 V 94 298 V 125 298 V 155 298 V 186 298 V 217 298 V 248 298 V 279 298 V 309 298 V 340 298 V 371 298 V 402 298 V 432 298 V 463 298 V 494 298 V 525 298 V 555 298 V 586 298 V 617 298 V 648 298 V 678 298 V 94 260 V 125 260 V 155 260 V 186 260 V 217 260 V 248 260 V 279 260 V 309 260 V 340 260 V 371 260 V 402 260 V 432 260 V 463 260 V 494 260 V 525 260 V 555 260 V 586 260 V 617 260 V 648 260 V 678 260 V 94 223 V 125 223 V 155 223 V 186 223 V 217 223 V 248 223 V 279 223 V 309 223 V 340 223 V 371 223 V 402 223 V 432 223 V 463 223 V 494 223 V 525 223 V 555 223 V 586 223 V 617 223 V 648 223 V 678 223 V 94 185 V 125 185 V 155 185 V 186 185 V 217 185 V 248 185 V 279 185 V 309 185 V 340 185 V 371 185 V 402 185 V 432 185 V 463 185 V 494 185 V 525 185 V 555 185 V 586 185 V 617 185 V 648 185 V 678 185 V 94 148 V 125 148 V 155 148 V 186 148 V 217 148 V 248 148 V 279 148 V 309 148 V 340 148 V 371 148 V 402 148 V 432 148 V 463 148 V 494 148 V 525 148 V 555 148 V 586 148 V 617 148 V 648 148 V 678 148 V 1440 107 307 4 v 1440 407 4 300 v 1744 407 V 1440 410 307 4 v 915 107 V 915 707 4 600 v 1219 707 V 915 710 307 4 v 91 107 607 4 v 91 707 4 600 v 694 707 V 91 710 607 4 v 919 148 16 4 v 950 148 V 982 148 V 1013 148 V 1045 148 V 1077 148 V 1108 148 V 1140 148 V 1171 148 V 1203 148 V 919 185 V 950 185 V 982 185 V 1013 185 V 1045 185 V 1077 185 V 1108 185 V 1140 185 V 1171 185 V 1203 185 V 919 223 V 950 223 V 982 223 V 1013 223 V 1045 223 V 1077 223 V 1108 223 V 1140 223 V 1171 223 V 1203 223 V 919 260 V 950 260 V 982 260 V 1013 260 V 1045 260 V 1077 260 V 1108 260 V 1140 260 V 1171 260 V 1203 260 V 919 298 V 950 298 V 982 298 V 1013 298 V 1045 298 V 1077 298 V 1108 298 V 1140 298 V 1171 298 V 1203 298 V 919 335 V 950 335 V 982 335 V 1013 335 V 1045 335 V 1077 335 V 1108 335 V 1140 335 V 1171 335 V 1203 335 V 919 373 V 950 373 V 982 373 V 1013 373 V 1045 373 V 1077 373 V 1108 373 V 1140 373 V 1171 373 V 1203 373 V 919 410 V 950 410 V 982 410 V 1013 410 V 1045 410 V 1077 410 V 1108 410 V 1140 410 V 1171 410 V 1203 410 V 919 448 V 950 448 V 982 448 V 1013 448 V 1045 448 V 1077 448 V 1108 448 V 1140 448 V 1171 448 V 1203 448 V 919 485 V 950 485 V 982 485 V 1013 485 V 1045 485 V 1077 485 V 1108 485 V 1140 485 V 1171 485 V 1203 485 V 919 523 V 950 523 V 982 523 V 1013 523 V 1045 523 V 1077 523 V 1108 523 V 1140 523 V 1171 523 V 1203 523 V 919 560 V 950 560 V 982 560 V 1013 560 V 1045 560 V 1077 560 V 1108 560 V 1140 560 V 1171 560 V 1203 560 V 919 598 V 950 598 V 982 598 V 1013 598 V 1045 598 V 1077 598 V 1108 598 V 1140 598 V 1171 598 V 1203 598 V 919 635 V 950 635 V 982 635 V 1013 635 V 1045 635 V 1077 635 V 1108 635 V 1140 635 V 1171 635 V 1203 635 V 919 673 V 950 673 V 982 673 V 1013 673 V 1045 673 V 1077 673 V 1108 673 V 1140 673 V 1171 673 V 1203 673 V 1444 148 V 1475 148 V 1507 148 V 1538 148 V 1570 148 V 1601 148 V 1633 148 V 1665 148 V 1696 148 V 1728 148 V 1444 185 V 1475 185 V 1507 185 V 1538 185 V 1570 185 V 1601 185 V 1633 185 V 1665 185 V 1696 185 V 1728 185 V 1444 223 V 1475 223 V 1507 223 V 1538 223 V 1570 223 V 1601 223 V 1633 223 V 1665 223 V 1696 223 V 1728 223 V 1444 260 V 1475 260 V 1507 260 V 1538 260 V 1570 260 V 1601 260 V 1633 260 V 1665 260 V 1696 260 V 1728 260 V 1444 298 V 1475 298 V 1507 298 V 1538 298 V 1570 298 V 1601 298 V 1633 298 V 1665 298 V 1696 298 V 1728 298 V 1444 335 V 1475 335 V 1507 335 V 1538 335 V 1570 335 V 1601 335 V 1633 335 V 1665 335 V 1696 335 V 1728 335 V 1444 373 V 1475 373 V 1507 373 V 1538 373 V 1570 373 V 1601 373 V 1633 373 V 1665 373 V 1696 373 V 1728 373 V 94 764 a Fb(|)p 113 764 263 5 v 263 w({z)p 414 764 V 263 w(})806 409 y Fo(2)830 391 y Fg(n)851 379 y Fa(k)736 110 y Fb(9)736 147 y(>)736 160 y(>)736 172 y(>)736 184 y(>)736 197 y(>)736 209 y(>)736 222 y(>)736 234 y(>)736 247 y(>)736 259 y(>)736 272 y(>)736 284 y(>)736 297 y(>)736 309 y(>)736 321 y(>)736 334 y(>)736 346 y(>)736 359 y(=)736 434 y(>)736 446 y(>)736 458 y(>)736 471 y(>)736 483 y(>)736 496 y(>)736 508 y(>)736 521 y(>)736 533 y(>)736 546 y(>)736 558 y(>)736 571 y(>)736 583 y(>)736 595 y(>)736 608 y(>)736 620 y(>)736 633 y(>)736 645 y(;)360 840 y Fo(2)384 822 y Fg(n)405 810 y Fa(k)94 34 y Fs(NEXP:)1331 409 y Fo(2)1355 391 y Fg(n)1376 379 y Fa(k)1261 110 y Fb(9)1261 147 y(>)1261 160 y(>)1261 172 y(>)1261 184 y(>)1261 197 y(>)1261 209 y(>)1261 222 y(>)1261 234 y(>)1261 247 y(>)1261 259 y(>)1261 272 y(>)1261 284 y(>)1261 297 y(>)1261 309 y(>)1261 321 y(>)1261 334 y(>)1261 346 y(>)1261 359 y(=)1261 434 y(>)1261 446 y(>)1261 458 y(>)1261 471 y(>)1261 483 y(>)1261 496 y(>)1261 508 y(>)1261 521 y(>)1261 533 y(>)1261 546 y(>)1261 558 y(>)1261 571 y(>)1261 583 y(>)1261 595 y(>)1261 608 y(>)1261 620 y(>)1261 633 y(>)1261 645 y(;)919 764 y(|)p 938 764 113 5 v 113 w({z)p 1089 764 V 113 w(})1044 840 y Fj(n)1073 822 y Fg(k)919 34 y Fs(PSP)l(A)o(CE:)1856 259 y Fj(n)1885 241 y Fg(k)1786 109 y Fb(9)1786 147 y(>)1786 159 y(>)1786 172 y(>)1786 184 y(>)1786 196 y(>)1786 209 y(=)1786 284 y(>)1786 296 y(>)1786 309 y(>)1786 321 y(>)1786 333 y(>)1786 346 y(;)1444 464 y(|)p 1463 464 V 113 w({z)p 1614 464 V 113 w(})1568 540 y Fj(n)1597 522 y Fg(k)1444 34 y Fs(NP:)186 995 y Fo(Figure)15 b(2:)22 b(The)16 b(shap)q(es)i(of)e(pro)q(ofs)i(for)e (languages)i(in)e(NEXP)l(,)f(PSP)l(A)o(CE)h(and)h(NP.)p 166 1056 1634 2 v 75 1180 a(that)f(do)h(not)f(ha)o(v)o(e)f(\(pro)q(of)i (systems\))e(with)g(p)q(olynomially)f(wide)i(pro)q(ofs.)22 b(Figure)16 b(2)g(illustrates)75 1240 y(the)g(v)m(arious)h(shap)q(es)g(of)g (these)f(pro)q(ofs.)148 1301 y(W)l(e)h(b)q(eliev)o(e)e(that)i(these)g (results,)f(in)h(particular)f(the)h(IP)e(=)g(PSP)l(A)o(CE)i(result)f(in)h (the)f(IP)f(=)75 1361 y(PWT)d(in)o(terpretation,)f(rev)o(eal)f(new)h(and)h (in)o(teresting)e(insigh)o(ts)h(ab)q(out)i(the)e(quan)o(titativ)o(e)f(nature) 75 1421 y(of)15 b(mathematical)d(pro)q(ofs)k(and)f(th)o(us)g(ab)q(out)h(the)e (fundamen)o(tal)f(nature)i(of)g(mathematics.)j(The)75 1481 y(t)o(w)o(o)12 b(dimensional)e(shap)q(e)j(of)g(the)e(pro)q(of)j(determines)9 b(ho)o(w)k(rapidly)e(one)h(can)h(giv)o(e)e(o)o(v)o(erwhelming)75 1541 y(evidence)17 b(that)j(there)f(is)g(a)g(pro)q(of)i(without)e(sho)o(wing) h(the)f(whole)g(pro)q(of.)32 b(In)o(tuitiv)o(ely)l(,)16 b(this)j(is)75 1602 y(b)q(ecause)k(the)f(width)h(of)g(the)g(pro)q(of)h(re\015ects)e(the)g (maxim)o(um)c(distance)23 b(that)g(separates)g(the)75 1662 y(critical)15 b(pieces)g(of)h(the)g(pro)q(of)i(whic)o(h)d(are)i(used)f(to)g (v)o(erify)f(the)h(correctness)g(of)g(the)g(pro)q(of.)148 1722 y(W)l(e)d(are)g(impressed)f(b)o(y)h(the)g(rapid)g(dev)o(elopmen)o(t)d(of)j (the)g(theory)h(of)f(in)o(teractiv)o(e)e(pro)q(ofs)j(and)75 1782 y(deligh)o(ted)k(b)o(y)g(the)h(researc)o(h)g(culminating)e(in)i(the)f (IP)h(=)g(PSP)l(A)o(CE)g(result.)29 b(IP)18 b(=)h(PSP)l(A)o(CE)75 1842 y(is)e(indeed)f(a)h(b)q(eautiful)g(result)f(con)o(tributing)h(to)g(the)g (elegance)f(and)h(relev)m(ance)f(of)h(complexit)o(y)75 1902 y(theory)f(and)h(leading)f(to)h(new)f(insigh)o(ts)g(in)g(the)g(quan)o (titativ)o(e)e(nature)j(of)f(mathematics.)75 2069 y Fp(References)75 2178 y Fo([BFL90])71 b(L.)18 b(Babai,)f(L.)h(F)l(ortno)o(w,)g(and)g(C.)f (Lund.)27 b(Non-deterministic)14 b(exp)q(onen)o(tial)j(time)319 2239 y(has)g(t)o(w)o(o-pro)o(v)o(er)g(in)o(teractiv)o(e)d(proto)q(cols.)24 b(In)17 b Fk(Pr)n(o)n(c)n(e)n(e)n(dings)g(of)h(the)g(IEEE)g(Symp)n(o-)319 2299 y(sium)f(on)h(F)l(oundations)g(of)f(Computer)h(Scienc)n(e)p Fo(,)f(pages)g(16{25,)h(1990.)75 2400 y([Fis69])103 b(M.)12 b(J.)g(Fisc)o(her.)i(Tw)o(o)f(c)o(haracterizations)f(of)h(the)f(con)o(text)g (sensitiv)o(e)f(languages.)16 b(In)319 2461 y Fk(IEEE)k(Confer)n(enc)n(e)g(R) n(e)n(c)n(or)n(d)e(of)i(the)g(Symp)n(osium)g(on)g(Switching)i(and)e(A)o (utomata)319 2521 y(The)n(ory)p Fo(,)14 b(pages)k(149{156,)g(1969.)p eop %%Page: 10 10 bop 75 42 a Fo([FS88])109 b(L.)24 b(F)l(ortno)o(w)h(and)g(M.)f(Sipser.)45 b(Are)23 b(there)h(in)o(teractiv)o(e)e(proto)q(cols)j(for)g(co-NP)319 102 y(languages?)j Fk(Information)17 b(Pr)n(o)n(c)n(essing)g(L)n(etters)p Fo(,)f(28\(5\):249{251,)j(August)e(1988.)75 203 y([GMW86])35 b(O.)22 b(Goldreic)o(h,)g(S.)f(Micali,)h(and)h(A.)e(Widgerson.)39 b(Pro)q(ofs)24 b(that)f(yield)d(nothing)319 264 y(but)14 b(their)g(v)m (alidit)o(y)f(and)i(a)g(metho)q(dology)f(of)h(cryptographic)f(proto)q(col)h (design.)j(In)319 324 y Fk(Pr)n(o)n(c)n(e)n(e)n(dings)12 b(of)h(the)h(IEEE)g (Symp)n(osium)e(on)i(F)l(oundations)g(of)f(Computer)h(Scienc)n(e)p Fo(,)319 384 y(pages)j(174{187,)h(1986.)75 486 y([Gol89])92 b(S.)18 b(Goldw)o(asser.)29 b(In)o(teractiv)o(e)16 b(pro)q(of)j(systems.)27 b(In)18 b Fk(Computational)i(Complexity)319 546 y(The)n(ory)p Fo(,)i(Pro)q(ceedings)g(of)g(Symp)q(osia)g(in)f(Applied)g(Mathematics,)g(V)l (olume)f(38,)319 606 y(pages)d(108{128.)h(American)c(Mathematical)g(So)q (ciet)o(y)l(,)h(1989.)75 708 y([HCRR90])24 b(J.)d(Hartmanis,)h(R.)f(Chang,)j (D.)d(Ranjan,)j(and)e(P)l(.)f(Rohatgi.)39 b(Structural)21 b(com-)319 768 y(plexit)o(y)15 b(theory:)21 b(Recen)o(t)16 b(surprises.)22 b(In)17 b Fk(Pr)n(o)n(c)n(e)n(e)n(dings)f(of)i(the)h(2nd)f(Sc)n(andinavian) 319 828 y(Workshop)13 b(on)g(A)o(lgorithm)h(The)n(ory)p Fo(,)d(v)o(olume)f (447)j(of)f Fk(L)n(e)n(ctur)n(e)h(Notes)h(in)g(Computer)319 888 y(Scienc)n(e)p Fo(,)k(pages)f(1{12.)g(Springer-V)l(erlag,)e(1990.)75 990 y([LFKN90])31 b(C.)20 b(Lund,)h(L.)f(F)l(ortno)o(w,)g(H.)f(Karlo\013,)i (and)g(N.)e(Nisan.)32 b(Algebraic)18 b(metho)q(ds)i(for)319 1050 y(in)o(teractiv)o(e)i(pro)q(of)j(systems.)44 b(In)24 b Fk(Pr)n(o)n(c)n(e)n(e)n(dings)g(of)h(the)g(IEEE)g(Symp)n(osium)f(on)319 1110 y(F)l(oundations)18 b(of)f(Computer)h(Scienc)n(e)p Fo(,)f(pages)g(2{10,) h(1990.)75 1212 y([Sha90])90 b(A.)19 b(Shamir.)30 b(IP)19 b(=)h(PSP)l(A)o (CE.)31 b(In)20 b Fk(Pr)n(o)n(c)n(e)n(e)n(dings)f(of)h(the)i(IEEE)e(Symp)n (osium)g(on)319 1272 y(F)l(oundations)e(of)f(Computer)h(Scienc)n(e)p Fo(,)f(pages)g(11{15,)h(1990.)p eop %%Trailer end userdict /end-hook known{end-hook}if %%EOF