A new proof of the wellfoundednes of the multiset ordering

• To: types@cis.upenn.edu
• Subject: A new proof of the wellfoundednes of the multiset ordering
• From: Tobias.Nipkow@informatik.tu-muenchen.de
• Date: Mon, 12 Oct 1998 16:31:40 +0200
• Sender: Tobias Nipkow <nipkow@informatik.tu-muenchen.de>

Dear colleagues,

Attached you find a new(?) proof of the wellfoundednes of the multiset
ordering due to Wilfried Buchholz. Salient features:
- it is completely inductive and does not involve classical reasoning (in
contrast to the proof by Dershowitz and Manna);
- it is a joy for theorem provers (it takes about 40 lines in Isabelle/HOL).

I would be interested to hear if this proof is known in the literature.

Tobias

%!PS-Adobe-2.0
%%Creator: dvipsk 5.58f Copyright 1986, 1994 Radical Eye Software
%%Title: multiset.dvi
%%Pages: 2
%%PageOrder: Ascend
%%BoundingBox: 0 0 596 842
%%DocumentPaperSizes: a4
%%EndComments
%DVIPSCommandLine: dvips multiset.dvi -o multiset.ps
%DVIPSParameters: dpi=600, compressed, comments removed
%DVIPSSource:  TeX output 1998.10.12:1306
%%BeginProcSet: texc.pro
/TeXDict 250 dict def TeXDict begin /N{def}def /B{bind def}N /S{exch}N
/X{S N}B /TR{translate}N /isls false N /vsize 11 72 mul N /hsize 8.5 72
mul N /landplus90{false}def /@rigin{isls{[0 landplus90{1 -1}{-1 1}
ifelse 0 0 0]concat}if 72 Resolution div 72 VResolution div neg scale
isls{landplus90{VResolution 72 div vsize mul 0 exch}{Resolution -72 div
hsize mul 0}ifelse TR}if Resolution VResolution vsize -72 div 1 add mul
TR[matrix currentmatrix{dup dup round sub abs 0.00001 lt{round}if}
forall round exch round exch]setmatrix}N /@landscape{/isls true 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 sub]/id ch-image N /rw ch-width 7 add 8 idiv string N /rc 0 N /gp 0 N
/cp 0 N{rc 0 ne{rc 1 sub /rc X rw}{G}ifelse}imagemask restore}B /G{{id
gp get /gp gp 1 add N dup 18 mod S 18 idiv pl S get exec}loop}B /adv{cp
add /cp X}B /chg{rw cp id gp 4 index getinterval putinterval dup gp add
/gp X adv}B /nd{/cp 0 N rw exit}B /lsh{rw cp 2 copy get dup 0 eq{pop 1}{
dup 255 eq{pop 254}{dup dup add 255 and S 1 and or}ifelse}ifelse put 1
adv}B /rsh{rw cp 2 copy get dup 0 eq{pop 128}{dup 255 eq{pop 127}{dup 2
idiv S 128 and or}ifelse}ifelse put 1 adv}B /clr{rw cp 2 index string
putinterval adv}B /set{rw cp fillstr 0 4 index getinterval putinterval
adv}B /fillstr 18 string 0 1 17{2 copy 255 put pop}for N /pl[{adv 1 chg}
{adv 1 chg nd}{1 add chg}{1 add chg nd}{adv lsh}{adv lsh nd}{adv rsh}{
adv rsh nd}{1 add adv}{/rc X nd}{1 add set}{1 add clr}{adv 2 chg}{adv 2
chg nd}{pop nd}]dup{bind pop}forall N /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 /V matrix currentmatrix dup 1 get dup mul exch 0 get dup mul
add .99 lt{/QV}{/RV}ifelse load def pop pop}N /eop{SI restore userdict
/eop-hook known{eop-hook}if showpage}N /@start{userdict /start-hook
known{start-hook}if pop /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
65781.76 div /vsize X 65781.76 div /hsize X}N /p{show}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
{}B /RV statusdict begin /product where{pop product dup length 7 ge{0 7
getinterval dup(Display)eq exch 0 4 getinterval(NeXT)eq or}{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 /QV{gsave newpath transform
round exch round exch itransform moveto rulex 0 rlineto 0 ruley neg
rlineto rulex neg 0 rlineto fill grestore}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{SS restore}B end
%%EndProcSet
TeXDict begin 39158280 55380996 1000 600 600 (multiset.dvi)
@start /Fa 1 51 df<007FB812E0B912F0A300F0CAFCB3B3A8B9FCA36C17E0343478B8
44>50 D E /Fb 20 117 df<120FEA3FC0127FA212FFA31380EA7F00123C0A0A77891C>
46 D<49B648B6FC495DA2D9000390C7000313004B5D4B5DA2180714074B5DA2180F140F
4B5DA2181F141F4B5DA2183F143F4B5DA2187F147F4B5DA218FF91B8FC96C7FCA292C712
015B4A5DA2170313034A5DA2170713074A5DA2170F130F4A5DA2171F131F4A5DA2173F13
3F4A5DA2017F157FA24A5D496C4A7EB66CB67EA3483E7BBD44>72
D<49B6FC5BA2D9000313005D5DA314075DA3140F5DA3141F5DA3143F5DA3147F5DA314FF
92C7FCA35B5CA313035CA313075CA3130F5CA3131F5CA3133F5CA2137FA25C497EB67EA3
283E7BBD23>I<49B612C0A25FD9000390C8FC5D5DA314075DA3140F5DA3141F5DA3143F
5DA3147F5DA314FF92C9FCA35B5CA313035C18C0EF01E0010716C05C17031880130F4A14
0718005F131F4A141EA2173E013F5D4A14FC1601017F4A5A16074A131F01FFECFFF0B8FC
A25F333E7BBD39>76 D<49B5933807FFFC496062D90003F0FC00505ADBBF805E1A771AEF
1407033F923801CFE0A2F1039F020FEE071F020E606F6C140E1A3F021E161C021C04385B
A2F1707F143C023804E090C7FCF001C0629126780FE0495A02705FF00700F00E0114F002
E0031C5BA2F03803010116704A6C6C5D18E019070103ED01C00280DA03805BA294380700
0F13070200020E5C5FDB03F8141F495D010E4B5CA24D133F131E011CDAF9C05CEEFB8019
7F013C6DB4C7FC013895C8FC5E01784A5C13F8486C4A5CD807FE4C7EB500F04948B512FE
16E01500563E7BBD52>I<147E49B47E903907C1C38090391F80EFC090383F00FF017E13
7F4914804848133F485AA248481400120F5B001F5C157E485AA215FE007F5C90C7FCA214
01485C5AA21403EDF0385AA21407EDE078020F1370127C021F13F0007E013F13E0003E13
7FECF3E1261F01E313C03A0F8781E3803A03FF00FF00D800FC133E252977A72E>97
D<EB1FC0EA0FFF5CA2EA003FA291C7FCA25BA2137EA213FEA25BA21201A25BA21203A25B
147E3907F1FF809038F783E09038EF01F013FE390FF800F8A24913FC49137C485A157E5B
15FE123FA290C7FCA248130115FC127EA2140300FE14F85AA2EC07F0A215E048130F15C0
141F15800078EB3F00127C147E003C5B383E01F8381E03E06C485A6CB4C7FCEA01F81F40
76BE2A>I<EC1FC0ECFFF0903803F03C903807C01E90381F800E90383F000F017E133F49
13FF485A485A000714FE5B000F14FC48481300A2485AA3127F90C8FCA35A5AA648140300
7E1407150F151E003E143C15786C14F0EC03E0390F800F803903E07E003801FFF838003F
C0202977A72A>I<EE3F80ED1FFF1700A2ED007FA2167EA216FEA25EA21501A25EA21503
A25EA21507A25E147E903801FF8F903807C1CF90391F80EFC090383F00FF017E137F5B48
486D5A485AA2485A000F92C7FC5B001F5CA24848137EA215FE127F90C75AA214015A485C
A2140316384814F0A21407167891380FE070127C021F13F0007E013F5B003E137FECF3E1
261F01E35B3A0F8781E3802703FF00FFC7FCD800FC133E294077BE2E>I<EC3F80903801
FFE0903807E0F890381F803CEB3E0001FC131E485A485A12074848133E49133C121F4848
137C15F8EC03F0397F000FE0ECFF809038FFFC00B512C048C8FCA45AA61506150E151E00
7C143C15786C14F0EC01E06CEB07C0390F801F003807C0FC3801FFF038007F801F2976A7
2A>I<167C4BB4FC923807C78092380F83C0ED1F87161FED3F3FA2157EA21780EE0E004B
C7FCA414015DA414035DA30103B512F8A390260007E0C7FCA3140F5DA5141F5DA4143F92
C8FCA45C147EA414FE5CA413015CA4495AA4495AA4495A121E127F5C12FF49C9FCA2EAFE
1EEAF83C1270EA7878EA3FE0EA0F802A5383BF1C>I<EC03F0EC0FFC91383E0E1C9138FC
077E903901F003FE1303903807E001D90FC013FCEB1F80A2EB3F004914F8137E01FE1303
A2484814F0A2150712034914E0A2150F12074914C0A2151FA216805B153F1203ED7F006D
5BA200015B0000495A9038F80F7E90387C1EFEEB1FF8903807E0FC90C7FC1401A25DA214
03A25D001C1307007F5C48130F5D4A5A4AC7FC48137E00F85B387C03F0381FFFC0D803FE
C8FC273B7CA72A>I<EB01FC13FF5CA21303A25CA21307A25CA2130FA25CA2131FA25CA2
133FA291C8FCEC03F890387F0FFE91383E0F80D97E7813C0ECE007D9FFC013E014801400
A2485A5BA25B0003140F16C05BA20007141F16805BA2000F143F16005B5D001F147EEDFE
074913FCA2003F0101130FEDF80E1300161E48ECF01CA2007E1538A200FE1570020013E0
48EC7FC00038EC1F0028407ABE2E>I<1478EB01FCA21303A314F8EB00E01400AD137C48
B4FC38038F80EA0707000E13C0121E121CEA3C0F1238A2EA781F00701380A2EAF03F1400
12005B137E13FE5BA212015BA212035B1438120713E0000F1378EBC070A214F0EB80E0A2
EB81C01383148038078700EA03FEEA00F8163E79BC1C>I<EB01FC13FF5CA21303A25CA2
1307A25CA2130FA25CA2131FA25CA2133FA291C8FCED03E049EB0FF8ED3C3C017EEB707C
EDE1FC9038FE01C1EC03839038FC0703140E0001011C13F891383800E049481300146000
0313E0EBF9C0EBF78001FEC8FC1207EBFFE0EBE7F8EBE0FE000F137F6E7EEBC01F81001F
130F16701380A2003F15F0021F13E001001380A248148116C0007EEB0F83168000FE1487
9138078F0048EB03FE0038EB00F826407ABE2A>107 D<EB07F0EA03FF14E0A2EA000FA2
14C0A2131FA21480A2133FA21400A25BA2137EA213FEA25BA21201A25BA21203A25BA212
07A25BA2120FA25BA2121FA25BA2123FA290C7FCA25A1307127EA2EAFE0F130E12FCA213
1E131CA2EA7C381378EA3C70EA1FE0EA0780144079BE17>I<D801F0D93F80137F3D07FC
01FFE003FFC03D0F3E07C1F80F83F03D0E1F0F00FC1E01F8001E011C90387C3800001C49
D97E707F003C01F05C0038157F4A5C26783FC05C12704A91C7FC91C7127E00F003FE1301
494A5CEA007EA20301140301FE5F495CA203031407000160495C180F03075D0003051F13
E0494A1480A2030FEC3F810007F001C0495CA2031F91383E0380120F494AEC0700A2033F
150E001FEF1E1C4991C7EA0FF80007C7000EEC03E0432979A74A>I<D801F0EB3F803A07
FC01FFE03A0F3E07C1F83A0E1F0F00FC001E011C137C001C49137E003C13F012385C3878
3FC012705C91C7FC00F015FE495CEA007EA2150101FE5C5BA2150300015D5B15075E0003
020F13704914C0A2031F13F00007ED80E05B1681EE01C0120F49EC0380A2EE0700001FEC
0F0E49EB07FC0007C7EA01F02C2979A733>I<EC1FC0ECFFF8903803F07C90380FC01FEB
1F8090393F000F80017E14C0491307484814E0485A12075B000F15F0485AA2485AA2ED0F
E0127F90C7FCA2151F4815C05AA2ED3F80A2ED7F00A248147E007C5C007E13015D4A5A00
3E495A6C495A4A5A260F803EC7FC3807C0FC3801FFF038003F80242977A72E>I<EB01C0
EB03F01307A25CA2130FA25CA2131FA25CA2133FA291C7FCA2007FB51280B6FC1500D800
7EC7FC13FEA25BA21201A25BA21203A25BA21207A25BA2120FA25BA2121F141C1380A200
3F133C1438EB0078147014F05C495AEA1F03495A6C48C7FCEA07FCEA01F0193A78B81E>
116 D E /Fc 4 118 df<137CEA0FFCA21200A213F8A21201A213F0A21203A213E0A212
07A213C0A2120FA21380A2121FA21300A25AA2123EA2127EA2127CA2EAFC08131812F8A2
1338133012F01370EAF860EA78E0EA3FC0EA0F000E2F7DAD15>108
D<27078007F0137E3C1FE01FFC03FF803C18F0781F0783E03B3878E00F1E01263079C001
B87F26707F8013B00060010013F001FE14E000E015C0485A4914800081021F130300015F
491400A200034A13076049133E170F0007027EEC8080188149017C131F1801000F02FCEB
3F03053E130049495C180E001F0101EC1E0C183C010049EB0FF0000E6D48EB03E0391F7E
9D3E>I<130E131FA25BA2133EA2137EA2137CA213FCA2B512F8A23801F800A25BA21203
A25BA21207A25BA2120FA25BA2001F1310143013001470146014E0381E01C0EB0380381F
0700EA0F0EEA07FCEA01F0152B7EA919>116 D<EA01E0D807F8130ED80E3C131FD81C3E
5B0038143E12301270D8607E137ED8E07C137C12C013FC484813FC00005C12015B140100
035C13E0A2020313200007ECE06013C0A216E0020713C00003EB0FC09038E01FC191383B
E1803901F071E33A007FE0FF0090381F803C231F7E9D29>I E /Fd
26 127 df<007FB512F8B612FCA46C14F81E067C9927>45 D<121EEA7F80A2EAFFC0A4EA
7F80A2EA1E000A0A728927>I<1538157C15FCA2140115F8140315F0140715E0140F15C0
141F1580143F1500A25C147E14FE5C13015C13035C13075C130F5CA2131F5C133F91C7FC
5B137E13FE5B12015B12035BA212075B120F5B121F5B123F90C8FC5A127E12FE5AA25A12
781E3A7CB327>I<14FF010713C0011F13F04913F890B5FC48EB81FC3803FE0113F8EA07
F0EA0FE09038C000F8001F1400485A90C8FCA25A127EEB0FF838FE3FFE48B51280B612C0
15E09038F80FF09038E007F890388001FC90C7FC15FE48147E157F153FA3127EA3127F6C
147F157E6C6C13FE9038C001FC120F9038F007F83907F81FF06CB512E06C14C06C148090
383FFE00EB0FF820307DAE27>54 D<3803FFC0000F13F04813FC4813FF811380EC1FC038
1F000F000480C71207A2EB0FFF137F0003B5FC120F5A383FFC07EA7FC0130012FE5AA46C
130F007F131FEBC0FF6CB612806C15C07E000313F1C69038807F8022207C9F27>97
D<EA7FE0487EA3127F1203A914FF01F313C090B512F08181EC81FE49C67E49EB3F804913
1F16C049130FA216E01507A6150F16C07F151F6DEB3F80157F6DEBFF009038FF83FEECFF
FC5D5D01F313C02601E0FEC7FC232E7FAD27>I<EB0FFF017F13C048B512E04814F05A38
0FF807EA1FE0393FC003E0903880008048C8FC127EA212FE5AA67E127EA2007F14F0393F
8001F813C0381FE003390FF80FF06CB5FC6C14E06C14C06C6C1300EB0FF81D207B9F27>
I<EC3FF04A7EA3143F1401A9EB0FE1EB7FFD48B5FC5A5A380FF83F381FE00F383FC007EB
8003EA7F00007E1301A212FE5AA67E007E1303A2127F6C1307EB800F381FE01F380FF03F
6CB612C06C15E06C13FD38007FF9D91FE013C0232E7EAD27>I<EB0FF8EB3FFE90B51280
000314C04814E0390FFC0FF0391FE003F8EBC001D83F8013FC48C7FC127E157E12FEB612
FEA415FC00FCC8FC7E127E127F6C143C6D137E6C7E01F013FE390FFC07FC6CB5FC000114
F86C14F0013F13C0903807FE001F207D9F27>I<EC1FF0ECFFF84913FC4913FE5BEB0FF0
14C0011F137CEC8000A6007FB512F0B612F8A36C14F039001F8000B3A4003FB512C04814
E0A36C14C01F2E7EAD27>I<153F90391FC0FF80D97FF313C048B612E05A4814EF390FF0
7F873A1FC01FC3C0EDC000EB800F48486C7EA66C6C485AEBC01FA2390FF07F8090B5C7FC
5C485BEB7FF0EB1FC090C9FCA27F6CB5FC15E015F84814FE4880EB8001007EC7EA3F8000
7C140F00FC15C0481407A46C140F007C1580007F143F6C6CEB7F009038F807FF6CB55A00
0714F86C5CC614C0D90FFCC7FC23337EA027>I<EA7FE0487EA3127F1203A9147F9038F1
FFC001F713F090B5FC8114C1EC01FCEBFE005B5BA25BB03A7FFF83FFE0B500C713F0A36C
018313E0242E7FAD27>I<130F497E497EA46D5A6DC7FC90C8FCA7383FFF80487FA37EEA
000FB3A4007FB512F0B6FC15F815F07E1D2F7BAE27>I<EA7FE07F12FF127FA21201A991
383FFFC04A13E0A36E13C0913803F8004A5A4A5A4A5A4A5A02FFC7FCEBF1FEEBF3FCEBF7
F8EBFFFC8080143F496C7E496C7E01F87FEBF0076E7E6E7E816E7E157E3A7FFFC1FFF002
C313F8B512E36C13C316F0252E80AD27>107 D<387FFF80B57EA37EEA000FB3B2007FB5
12F8B612FCA36C14F81E2E7CAD27>I<397F07C01F3AFF9FF07FC09039FFF9FFE091B57E
7E3A0FFC7FF1F89038F03FC001E0138001C01300A3EB803EB03A7FF0FFC3FF486C01E313
8001F913E701F813E36C4801C313002920819F27>I<387FE07F39FFF1FFC001F713F090
B5FC6C80000313C1EC01FCEBFE005B5BA25BB03A7FFF83FFE0B500C713F0A36C018313E0
24207F9F27>I<EB1FE0EB7FF83801FFFE487F481480390FF03FC0391FC00FE0393F8007
F0EB00034814F8007E1301A248EB00FCA76C1301007E14F8A2007F1303393F8007F0A239
1FE01FE0390FF03FC06CB512806C14006C5B38007FF8EB1FE01E207C9F27>I<387FE0FF
D8FFF313C090B512F0816C800003EB81FE49C67E49EB3F8049131F16C049130FA216E015
07A6150F16C07F151F6DEB3F80157F6DEBFF009038FF83FEECFFFC5D5D01F313C0D9F0FE
C7FC91C8FCAC387FFF80B57EA36C5B23317F9F27>I<397FFC03FC39FFFE0FFF023F1380
4A13C0007F90B5FC39007FFE1F14F89138F00F809138E002004AC7FC5CA291C8FCA2137E
AD007FB57EB67EA36C5C22207E9F27>114 D<9038FFF3800007EBFFC0121F5A5AEB803F
38FC000F5AA2EC07806C90C7FCEA7F8013FC383FFFF06C13FC000713FF00011480D8000F
13C09038003FE014070078EB03F000FC1301A27E14036CEB07E0EBE01F90B512C0158015
0000FB13FC38707FF01C207B9F27>I<133C137EA8007FB512F0B612F8A36C14F0D8007E
C7FCAE1518157EA415FE6D13FC1483ECFFF86D13F06D13E0010313C0010013001F297EA8
27>I<397FE01FF8486C487EA3007F131F00031300B21401A21403EBFC0F6CB612E016F0
7EEB3FFE90390FF87FE024207F9F27>I<3A7FFE07FFE000FF15F06D5A497E007F15E03A
0F80001F00A36D5B0007143EA414F0EBC1F83903E3FC7CA4EBE79EA200011478A301F713
F8A2EBFF0F6C5CA3EBFE0790387C03E024207F9F27>119 D<001FB512FE4814FFA49038
0001FEEC03FCEC07F8EC0FF0001EEB1FE0C7EA3FC0EC7F80ECFF00495A495A495AEB1FE0
495A495A49C7FC485A4848131E4848133F485A485A485A485AB7FCA46C14FE20207E9F27
>122 D<3901F003803903FC07C0000F130F381FFE1F393FFF7F80397FBFFF0038FE1FFE
486C5A00F813F0387003E01A0A7AAD27>126 D E /Fe 31 128 df<123C127EB4FCA213
80A2127F123D1201A412031300A25A1206120E120C121C5A5A126009177A8715>44
D<B512F0A514057F921A>I<B512FEA3000113006C5AB3B3A7487EB512FEA317337EB21C>
73 D<B512FEA3D803FEC9FC6C5AB3A9EE0180A416031700A45EA25E5E5E5E16FE000314
07B7FCA329337DB230>76 D<D8FFFC923801FFF86D5DA20003EFFE00D801BFED06FCA3D9
9F80140CA2D98FC01418A3D987E01430A2D983F01460A3D981F814C0A3D980FCEB0180A2
027EEB0300A36E1306A26E6C5AA36E6C5AA36E6C5AA26E6C5AA36E6C5AA3913800FD80A2
037FC7FCA3486C133ED80FF04B7EB5011C90387FFFF8A33D337CB246>I<D8FFFE91381F
FFF87F80C6030013006E143CD9DFE01418EBCFF0A2EBC7F8EBC3FCA2EBC1FEEBC0FF6E7E
A26E7E6E7EA26E7E6E7E6E7EA26E7E6E7EA2ED7F80ED3FC0ED1FE0A2ED0FF0ED07F8A2ED
03FCED01FEED00FFA2EE7F98EE3FD8A2EE1FF8160F1607A216031601A2486C1400D807F8
1578B500C01438A2171835337EB23A>I<007FB712FEA390398007F001D87C00EC003E00
78161E0070160EA20060160600E01607A3481603A6C71500B3AB4A7E011FB512FCA33033
7DB237>84 D<B500FE90381FFFF8A3000190C813006C48153C1718B3AF1738017F1530A2
17706D6C1460011F15E06E495A010F14036D6C495A6D6C49C7FCD901FC131E6DB413FC91
383FFFF0020F13C0020190C8FC35357EB23A>I<EB7F803803FFF0380F80FC381C003E00
3F133F6D6C7E6E7EA26E7EEA1F00C7FCA4EB01FF131FEBFF873803FC07EA0FF0EA1FC0EA
3F80127F13004815C05AA3140FA26C131F6C133B3A3F8071F180391FC1E1FF2607FFC013
003900FE003C22237DA126>97 D<EA03F012FFA312071203AEEC3F80ECFFE09038F3C0F8
9038F7007E01FE7F49EB1F8049EB0FC05BED07E016F0A2150316F8AA16F0150716E0A2ED
0FC07F6DEB1F8001ECEB3F0001CF137C90388381F8903801FFE0C76CC7FC25357EB32B>
I<EB07F8EB3FFF9038FC07C03901F000E03903E003F03807C007120FEA1F80123F903800
03E04890C7FCA2127E12FEAA127FA26C14187F001F14386D1330000F14706C6C13E03903
F001C03900FC0F8090383FFE00EB07F01D237EA122>I<153FEC0FFFA3EC007F81AEEB07
F0EB3FFCEBFC0F3901F003BF3907E001FF48487E48487F8148C7FCA25A127E12FEAA127E
127FA27E6C6C5BA26C6C5B6C6C4813803A03F007BFFC3900F81E3FEB3FFCD90FE0130026
357DB32B>I<EB0FE0EB7FFCEBF83F3903F00F80D807E013C0390FC007E0381F800315F0
EA3F0014014814F8127EA212FEA2B6FCA248C8FCA5127E127FA26C1418A26C6C1338000F
14306D13706C6C13E03901F003C03900FC0F00EB3FFEEB07F01D237EA122>I<EB01FCEB
07FF90381F078090383E0FC0EB7C1F13FCEA01F8A20003EB070049C7FCACB512F0A3D803
F0C7FCB3A7487E387FFFE0A31A357FB417>I<151F90391FC07F809039FFF8E3C03901F0
7FC73907E03F033A0FC01F83809039800F8000001F80EB00074880A66C5CEB800F000F5C
EBC01F6C6C48C7FCEBF07C380EFFF8380C1FC0001CC9FCA3121EA2121F380FFFFEECFFC0
6C14F06C14FC4880381F0001003EEB007F4880ED1F8048140FA56C141F007C15006C143E
6C5C390FC001F83903F007E0C6B51280D91FFCC7FC22337EA126>I<EA03F012FFA31207
1203AEEC1FC0EC7FF09038F1E0FC9038F3807C9038F7007E13FE497FA25BA25BB3486CEB
7F80B538C7FFFCA326347EB32B>I<EA0780EA0FC0EA1FE0A4EA0FC0EA0780C7FCAAEA07
E012FFA3120F1207B3A6EA0FF0B5FCA310337EB215>I<EA03F012FFA312071203AF9138
03FFE0A36E1300EC00F8EC01E05D4A5A020FC7FC141C5C5C14F0EBF3F8EBF7FC13FEEBFC
7EEBF87F496C7E141F6E7E8114076E7E8114016E7E81486CEBFF80B500C313F0A324347E
B329>107 D<EA07E012FFA3120F1207B3B3A7EA0FF0B5FCA310347EB315>I<2703F01FE0
13FF00FF90267FF80313C0903BF1E07C0F03E0903BF3803E1C01F02807F7003F387FD803
FE1470496D486C7EA2495CA2495CB3486C496C487EB53BC7FFFE3FFFF0A33C217EA041>
I<3903F01FC000FFEB7FF09038F1E0FC9038F3807C3907F7007EEA03FE497FA25BA25BB3
486CEB7F80B538C7FFFCA326217EA02B>I<EB07F0EB3FFE9038FC1F803901F007C03903
C001E000078048486C7E48C7127CA248147E003E143E007E143FA300FE1580A8007E1500
A36C147EA26C147C6D13FC6C6C485A00075C3903F007E03900FC1F80D93FFEC7FCEB07F0
21237EA126>I<3903F03F8000FFEBFFE09038F3C0F89038F7007ED807FE7F6C48EB1F80
4914C049130F16E0ED07F0A3ED03F8A9150716F0A216E0150F16C06D131F6DEB3F801600
01FF13FC9038F381F89038F1FFE0D9F07FC7FC91C8FCAA487EB512C0A325307EA02B>I<
3803E07C38FFE1FF9038E38F809038E71FC0EA07EEEA03ECA29038FC0F8049C7FCA35BB2
487EB512E0A31A217FA01E>114 D<EBFF06000713CE381F00FE003C133E48131E140E5A
1406A27EA200FE90C7FC6C7EEA7FFC383FFFC014F0000F7F6C7FC67FEB0FFF1300EC3F80
00C0131F140F6C1307A37E15006C5B6C130E6C5B38F7807838E1FFE038C07F8019237EA1
1E>I<1330A51370A313F0A21201A212031207381FFFFEB5FCA23803F000AF1403A81407
3801F806A23800FC0EEB7E1CEB1FF8EB07E0182F7FAD1E>I<D803F0133F00FFEB0FFFA3
0007EB007F000380B35DA35D12016D4813800000903803BFFC90387E073FEB1FFED907F8
130026227EA02B>I<B5EBFFF0A3D80FF0EB3F800007EC1F000003140E150C6D131C0001
1418A26C6C5BA26D1370017E1360137F6D5BA290381F8180A214C3010F90C7FCA2EB07E6
A214FE6D5AA26D5AA36D5AA2146024217E9F29>I<B53A1FFF81FFF0A33C07F801FC003F
8001F049EB1E0000030100141C816C6C017C1318A26D017E1338000002FE1330A290267E
01FF5B159F168090263F030F5BA216C0903A1F8607C180A202C613E390260FCC0390C7FC
A2D907FC13F6ECF80116FE6D486C5AA36D481378A36D48133034217F9F37>I<B53801FF
F8A32603FE0013806C48EB7C0000001478017E1370017F5B90383F81C090381F8380D90F
C3C7FCEB07E614FE6D5A6D5A6D7E80805B9038039F809038071FC09038060FE0EB0C0790
381C03F0496C7E01707FEBF000000180000FECFF8026FFFC0313FCA326207F9F29>I<00
1C1370387F01FC00FF13FEA4007F13FC381C0070170879B226>127
D E /Ff 3 52 df<13E01201120712FF12F91201B3A7487EB512C0A212217AA01E>49
D<EA01FC3807FF80381C0FC0383003E0386001F0EB00F812F86C13FCA2147C1278003013
FCC7FC14F8A2EB01F0EB03E014C0EB0780EB0F00131E13385B5B3801C00CEA0380380600
185A5A383FFFF85AB512F0A216217CA01E>I<13FF000313C0380F03E0381C00F014F800
3E13FC147CA2001E13FC120CC712F8A2EB01F0EB03E0EB0FC03801FF00A2380003E0EB00
F01478147C143E143F1230127812FCA2143E48137E0060137C003813F8381E03F0380FFF
C00001130018227DA01E>I E /Fg 12 104 df<EB0FFCEB3FFF90B512C0000314F04880
488048804880A2481580A3B712C0AA6C1580A36C1500A26C5C6C5C6C5C6C5CC614C0013F
90C7FCEB0FFC22227BA72D>15 D<EF01E0841700841878187C84A284727E727E85180372
7E007FB912FCBA7E856C85CCEA07E0737EF101FCF1007FF21FC0F20FF8F203FFA2F20FF8
F21FC0F27F00F101FCF103F04F5A007FBA1280BBC7FC616C60CBEA01F04E5A1807614E5A
4EC8FC183EA260187818F86017016050327BAF5B>41 D<03F015F0A20201824B15780203
167C4B153C0207163E4A488192C97E4A83023E707E023C1603027C834A707E49B97E4984
49844984013FCBEA0FC0017E727E49727ED803F8F001FCD80FE0F0007FD83FC0F13FC0B4
CDEA0FF0A2D83FC0F13FC0D80FE0F17F00D803F8F001FCC66CF003F0017E4E5A6D4E5A01
0FBAC7FC6D606D606D60D900F8C9EA01F0027C4C5A023C5F023E16076E4C5A6E94C8FC6F
5D6E6C153E0203163C6F157C020116786F15F802005EA254327DAF5B>44
D<0207B512E0023F14F049B6FC4915E0D90FFCC8FCEB1FE0017FC9FC13FEEA01F8485A48
5A5B485A121F90CAFC123EA25AA21278A212F8A25AA2B812E017F0A217E000F0CAFCA27E
A21278A2127CA27EA27E7F120F6C7E7F6C7E6C7EEA00FE137FEB1FE0EB0FFC0103B612E0
6D15F0EB003F020714E02C3678B13D>50 D<0060EE018000F0EE03C06C1607A200781780
007C160FA2003C1700003E5EA26C163EA26C163C6D157CA2000716786D15F8A26C6C4A5A
A200015E6D140390B7FC6C5EA3017CC7EA0F80A2013C92C7FC013E5CA2011E141E011F14
3EA26D6C5BA2010714786E13F8A26D6C485AA201015CECF003A201005CECF807A291387C
0F80A2023C90C8FCEC3E1FA2EC1E1EEC1F3EA2EC0FFCA26E5AA36E5AA36E5A6E5A324180
BE33>56 D<007FB612FEB8FCA27EC9120FB3A7001FB7FC127FA3C9120FB3A8007FB7FCB8
FCA26C15FE283F7BBE33>I<1518153CA2157CA2903803FC7890380FFFF8EB3E07903878
01F0EBF0004848487ED803C07FD807807FA2390F0003EFA248ECCF80001EEB07C7003E15
C01587A2140F007E15E0007C1403A2141FA2141E00FC013E13F0A2143CA2147CA21478A2
14F8A214F01301A214E0A21303A214C0A21307A21480D87C0F14E0A21400007E14075BA2
D83E1E14C0A2133E001FEC0F80133CD80F7C1400A2495B0007141E00035C00015C4913F8
3900F801E03901FE07C090B5C7FCEBE3FCD803E0C8FCA25BA26C5A244D7CC52D>59
D<0438198004F81801030119030303190770180F1D1FF53F00A2030761706064525A1C07
A24B6C170F1C1F525A030E187F7017FD031E6DED01F91CFB031CEF03F3983807E3F89226
3C3FC0ED0FC3F31F830338EF3F03F37E079238781FE009FC5B0370EE01F8F203F09226F0
0FF0EC07E003E093380FC00FF21F800201173F4B6C6C03005B1A7E02035F03806D495A04
034A48131F02074C5A03004B5A706C131F020E4C5A4FC75B021E6E13FE021C6D495AF083
F84ADB87F0143F94387FCFE00278EDDFC002706EB45A96C8FC4A6E5A6001016F5A49485D
0030705A267C07805DD87F0F6F5AB5C890C9EBE1C094CA13E749F3FF80491C00F41FFC49
1BF06C48F20FC0D81FE097C8FCEA078062457DBF6D>77 D<0060EE018000F0EE03C0B3B3
A36C1607A200781780007C160FA26CEE1F00003F5E6C6C157E6C6C5DD807F0EC03F8D803
FCEC0FF06CB4EC3FE03B007FF003FF80011FB548C7FC010714F8010114E09026001FFEC8
FC32397BB63D>91 D<15C04A7E4A7EA24A7EA34A7EA2EC1F3EA2EC3E1FA2EC3C0F027C7F
A24A6C7EA249486C7EA2ECE001010380A249486C7EA24948137CA249C77EA2011E141E01
3E141FA2496E7EA2496E7EA2491403000182A248486E7EA248486E7EA2491578000F167C
A248C97EA2003E82A2003C82007C1780A248EE07C0A24816030060EE018032397BB63D>
94 D<153FEC03FFEC0FE0EC3F80EC7E00495A5C495AA2495AB3AA130F5C131F495A91C7
FC13FEEA03F8EA7FE048C8FCEA7FE0EA03F8EA00FE133F806D7E130F801307B3AA6D7EA2
6D7E80EB007EEC3F80EC0FE0EC03FFEC003F205B7AC32D>102 D<12FCEAFFC0EA07F0EA
01FCEA007E6D7E131F6D7EA26D7EB3AA801303806D7E1300147FEC1FC0EC07FEEC00FFEC
07FEEC1FC0EC7F0014FC1301495A5C13075CB3AA495AA2495A133F017EC7FC485AEA07F0
EAFFC000FCC8FC205B7AC32D>I E /Fh 25 120 df<B612E0A91B097F9823>45
D<EA0FC0EA1FE0EA3FF0EA7FF8EAFFFCA6EA7FF8EA3FF0EA1FE0EA0FC00E0E798D1D>I<
140F143F5C495A130F48B5FCB6FCA313F7EAFE071200B3B3A8007FB612F0A5243C78BB34
>49 D<903803FF80013F13F890B512FE00036E7E4881260FF80F7F261FC0037F4848C67F
486C6D7E6D6D7E487E6D6D7EA26F1380A46C5A6C5A6C5A0007C7FCC8FC4B1300A25E153F
5E4B5AA24B5A5E4A5B4A5B4A48C7FC5D4A5AEC1FE04A5A4A5A9139FF000F80EB01FC495A
4948EB1F00495AEB1F8049C7FC017E5C5B48B7FC485D5A5A5A5A5AB7FC5EA4293C7BBB34
>I<903801FFE0010F13FE013F6D7E90B612E04801817F3A03FC007FF8D807F06D7E82D8
0FFC131F6D80121F7FA56C5A5E6C48133FD801F05CC8FC4B5A5E4B5A4A5B020F5B902607
FFFEC7FC15F815FEEDFFC0D9000113F06E6C7E6F7E6F7E6F7E1780A26F13C0A217E0EA0F
C0487E487E487E487EA317C0A25D491580127F49491300D83FC0495A6C6C495A3A0FFE01
FFF86CB65A6C5DC61580013F49C7FC010313E02B3D7CBB34>I<ED01F815031507A2150F
151F153FA2157F15FF5C5CA25C5CEC1FBFEC3F3F143E147C14FCEB01F814F0EB03E01307
EB0FC0EB1F801400133E137E5B485A5B485A1207485A5B48C7FC5A127E5AB812F8A5C838
7FF800AA49B612F8A52D3C7DBB34>I<B712E0A526003FFEC9FCB3AD183EA4187E187CA4
18FCA21701A2EF03F8A21707170F171F177FEE01FF160FB9FC18F0A4373E7DBD3F>76
D<B812F017FF18C018F018FC26003FFCC77FEF1FFF7113807113C07113E0A27113F0A319
F8A819F0A34D13E019C05F4D1380053F1300EFFFFE91B712F860188005FCC7FC4ACAFCB3
A4B77EA53D3E7DBD47>80 D<003FB912FCA5903BFE003FFE003FD87FF0EE0FFE01C01603
49160190C71500197E127EA2007C183EA400FC183F48181FA5C81600B3AF010FB712F8A5
403D7CBC49>84 D<903807FFC0013F13F848B6FC48812607FE037F260FF8007F6DEB3FF0
486C806F7EA36F7EA26C5A6C5AEA01E0C8FC153F91B5FC130F137F3901FFFE0F4813E000
0F1380381FFE00485A5B485A12FF5BA4151F7F007F143F6D90387BFF806C6C01FB13FE39
1FFF07F36CEBFFE100031480C6EC003FD91FF890C7FC2F2B7DA933>97
D<EC7FF00107B5FC011F14C0017F14E09039FFF01FF0489038800FF848EB001F4848EB3F
FC120F485AA2485AA2007FEC1FF849EB0FF0ED03C000FF91C7FCAB127F7FA3003F153E7F
001F157E6C6C147C6C6C14FC91388001F86C9038C003F0C69038F81FE06DB512C0011F14
800107EBFE009038007FF0272B7DA92E>99 D<EE07F8ED07FFA5ED003F161FAFEC7FF090
3807FFFE011FEBFF9F017F14DF9039FFF01FFF48EBC00348EB00014848EB007F485A001F
153F5B123FA2127F5BA212FFAA127FA37F123FA26C6C147F120F6D14FF6C6C01037F6C6D
48EBFFE06CEBF03F6C6CB512BF6D143F010713FC010001E0EBE00033407DBE3A>I<ECFF
F0010713FE011F6D7E017F809039FFE07FE0489038801FF048496C7E48486D7E48486D7E
121F491301003F81A2485A6F1380A212FFA290B7FCA401F0C9FCA5127FA27F123FEE0F80
6C7E161F6C6C15006C6C5C6C6D137E6C9038E001FC6C9038F80FF8013FB55A6D14C00103
91C7FC9038007FF8292B7DA930>I<EC07FE91387FFF8049B512C0010714E090390FFE3F
F0EB1FF090393FE07FF8EB7FC013FF1480A2489038003FF0ED1FE0ED0FC092C7FCAAB612
E0A500010180C7FCB3AC007FEBFF80A525407DBF20>I<13FFB5FCA512077EAFED1FF8ED
FFFE02036D7E4A80DA0FE07F91381F007F023C805C4A6D7E5CA25CA35CB3A4B5D8FE0FB5
12E0A5333F7CBE3A>104 D<EA01F8487E487E487E481380A66C13006C5A6C5A6C5AC8FC
A913FFB5FCA512077EB3ABB512F8A515407CBF1D>I<13FFB5FCA512077EB3B3AFB512FC
A5163F7CBE1D>108 D<01FFD91FF8ECFFC0B590B5010713F80203DAC01F13FE4A6E487F
DA0FE09026F07F077F91261F003FEBF8010007013EDAF9F0806C0178ECFBC04A6DB4486C
7FA24A92C7FC4A5CA34A5CB3A4B5D8FE07B5D8F03FEBFF80A551297CA858>I<01FFEB1F
F8B5EBFFFE02036D7E4A80DA0FE07F91381F007F0007013C806C5B4A6D7E5CA25CA35CB3
A4B5D8FE0FB512E0A533297CA83A>I<EC7FF0903803FFFE011FEBFFC0017F14F09039FF
E03FF8489038800FFC3A03FE0003FE48486D7E000F168048486D13C0A2003F16E049147F
007F16F0A400FF16F8AA007F16F0A46C6CECFFE0A2001F16C06C6C491380A26C6C491300
3A03FF800FFE6C9038E03FFC6C6CB512F0011F14C0010791C7FC9038007FF02D2B7DA934
>I<01FFEBFFE0B5000713FC021FEBFF80027F80DAFF8113F09139FC007FF8000301F06D
7E4A6D7E4A130F4A6D7E1880A27013C0A38218E0AA4C13C0A318805E18005E6E5C6E495A
6E495A02FCEBFFF0DAFF035B92B55A029F91C7FC028713FC028113C00280C9FCACB512FE
A5333B7DA83A>I<3901FE01FE00FF903807FF804A13E04A13F0EC3F1F91387C3FF80007
13F8000313F0EBFFE0A29138C01FF0ED0FE091388007C092C7FCA391C8FCB3A2B6FCA525
297DA82B>114 D<EB07C0A5130FA4131FA3133F137FA213FF5A1207001FEBFFFEB6FCA4
0001EBC000B3151FA96CEBE03EA2017F137EECF8FC90383FFFF86D13F0010713E0010013
80203B7EB929>116 D<D9FF80EB0FF8B5EB0FFFA50007EC007F6C153FB3A5167FA316FF
6C5C4B7F6C903AC007DFFFE09138F01F9F6DB5121F6D13FE010F13F8010101E0EBE00033
2A7CA83A>I<B53CFC3FFFFC03FFFEA50003D980009039C0000F806E161F6C037F15006E
496C5B6C183E836E48157E017F177C6E486D13FC013F02EF5C83DAFC071401011F02C75C
DAFE0FEBFE03010F02835C17FFDAFF1F14076D02015C03BF148F6DD9BE005C18CF03FE14
DF6D49017F90C7FC18FF6D496D5AA36E486D5AA26E486D5AA36E486D5AA26E486D5A4728
7EA74C>119 D E /Fi 14 122 df<121EEA7F80A2EAFFC0A4EA7F80A2EA1E000A0A7989
19>58 D<121EEA7F8012FF13C0A213E0A3127FEA1E601200A413E013C0A3120113801203
13005A120E5A1218123812300B1C798919>I<183818FC1703EF0FF8EF3FE0EFFF809338
03FE00EE0FF8EE3FE0EEFF80DB03FEC7FCED0FF8ED3FE0EDFF80DA03FEC8FCEC0FF8EC3F
E0ECFF80D903FEC9FCEB0FF8EB3FE0EBFF80D803FECAFCEA0FF8EA3FE0EA7F8000FECBFC
A2EA7F80EA3FE0EA0FF8EA03FEC66C7EEB3FE0EB0FF8EB03FE903800FF80EC3FE0EC0FF8
EC03FE913800FF80ED3FE0ED0FF8ED03FE923800FF80EE3FE0EE0FF8EE03FE933800FF80
EF3FE0EF0FF8EF03FC17001838363678B147>I<17075F84171FA2173F177FA217FFA25E
5EA24C6C7EA2EE0E3F161E161C1638A21670A216E0ED01C084ED0380171FED07005D150E
5DA25D157815705D844A5A170F4A5A4AC7FC92B6FC5CA2021CC7120F143C14384A81A24A
140713015C495AA249C8FC5B130E131E4982137C13FED807FFED1FFEB500F00107B512FC
A219F83E417DC044>65 D<49B600C090387FFFF896B5FC5FD900010180C7000F130093C8
13F84B16E01A804FC7FC0203163C4B15F84E5AF003C002074B5A4B021FC8FC183E187802
0F5D4BEB03E0EF07804DC9FC021F143E4B5B17F04C5A023F1307EDC00F4C7E163F027FEB
FFF8ED81EFED83CF92388F87FC9138FF9F0792383C03FE15784B6C7E4913E0158092C77F
5C01036F7E5C717EA213074A6E7EA2717E130F4A6E7EA284011F15035C717E133F855C49
6C4A13E0B600E0017F13FFA34D3E7DBD4D>75 D<49B56C93B512C050148062D90001F180
00704B90C7FC03DF5F1A0E1A1D1403039FEE39FC1A711A739126078FE015E3030F5FF101
C3F10387140F020E93380707F0A2F10E0F021E161C91261C07F05E1938F1701F143C0238
04E05BA2953801C03F0278ED038091267003F85EF00700060E137F14F002E04B91C8FCA2
4E5B01015E4A6C6C5D60943801C00113030280DA03805BA294380700030107150E91C700
FE5D5F1907495D010E4B5CA24D130F011E6E5A011C60705A013C171F017C92C7FC01FE02
7E5DD803FF4D7EB500FC017C017FB512E0167804385E5A3E7CBD58>77
D<49B56C49B512F81BF0A290C76D9039000FFE004AEE03F0705D735A03DF150302037F03
8F5E82190791380787FC030793C7FC1503705C140F91260E01FF140EA26F151E021E8002
1C017F141C83193C023C6D7E02381638161F711378147802706D6C1370A2040714F002F0
804A01035C8318010101EC01FF4A5E82188313034A91387FC380A2EF3FC7010716E791C8
001F90C8FC18F718FF4981010E5E1707A2131E011C6F5AA2013C1501137C01FE6F5AEA03
FFB512FC187818704D3E7DBD49>I<49B712F018FF19C0D9000190C76C7EF00FF84BEC03
FC1801020382727E5DA214071A805DA2140F4E13005DA2021F5E18034B5D1807023F5E4E
5A4B4A5A4E5A027F4B5A06FEC7FC4BEB03FCEF3FF091B712C005FCC8FC92CBFCA25BA25C
A21303A25CA21307A25CA2130FA25CA2131FA25CA2133FA25C497EB612E0A3413E7DBD3A
>80 D<DB07FC1338ED3FFF92B5EAC070913A03F807F0F091390FE000F9DA1F80137F4AC7
EA3FE0027E141F5C4948140F4A15C001031507495AA2010F16805CA3011F1600A38094C7
FC808014FE90380FFFC015FC6DEBFFC016F86D14FE6D806D81023F800207801400030F7F
1500163F707E160F1607A2160312075A5F120EA2001E15075FA24C5A123E003F4B5AA26D
4AC7FC007F157E6D5C6D495AD87DF0495AD8F8FCEB0FE090393F803F8027F01FFFFEC8FC
D8E00713F839C0007FC035427BBF38>83 D<B6017FB5D88007B51280A24A1A0000030180
010101E0C7EA7FF049C80180EC1FC0000194C85B99C7FC1B1E1B1C63A2634C7F634C1501
63DC077F4A5A160F6D020E4BC8FC161C6C190E1638620470153C04F0153804E05DED01C0
62DB03807F4F5A922607003F130362030E4BC9FC151EDA801C150E5D017F5F5D614B1578
028116704B5DEC8380F0C1C00287C713E1F0E380028EEC1FE796CAFC029C15EE14BC02F8
15FC5C013F5E5C605C604A5D91C8FC60133E95CBFC013C81170E59407BBD56>87
D<EC1F80ECFFE0903903F0707090390FC039F890381F801D90383F000F017E5C5B000114
07485A48485CA2485A001F140F5E485AA2151F007F5D5BA2153F00FF92C7FC90C7FCA25D
92387E03805AA215FEEDFC07007E0101140014035E6C0107130E140E3A1F801C7C1C000F
13783A07C1F03E383A01FFC01FF03A007F0007C029297DA730>97
D<EB1FC0EA0FFF5CA2EA003FA291C8FCA25BA2137EA213FEA25BA21201A25BA21203A25B
EC3F800007EBFFE09038F3C1F849C67E01FE137E4848133E49133F5B491480001F141F5B
5BED3FC0123FA290C7FCA248147F1680127EA215FF00FE15005AA24A5AA25D1403485C14
07007C5C4A5A5D003C495A003E49C7FC001E137E6C13F8380783F03803FFC0C648C8FC22
407CBE27>I<D901F8133FD907FEEBFFE0903A1E0F83C0F0903A3807C780F890397003CF
0301E013FED801C0EBFC071203018013F8D8070015F0EE01C0000E4AC7FCA2001E1307A2
C75BA2140F5DA3141F5DA3143F92380001C0A34A1303001E1680003F017E1307267F80FE
14005ED8FF81141ED901DF131CD8FE035C3A7C078F80F03A3C0F07C1E03A1FFC03FF8027
07F0007EC7FC2D297EA734>120 D<137C48B4EC03802603C7C0EB0FC0EA0703000F7F00
0E151F001C168013071238163FD8780F150000705BA2D8F01F5C4A137E1200133F91C712
FE5E5B137E150113FE495CA2150300015D5BA215075EA2150F151F00005D6D133F017C13
7F017E13FF90393F03DF8090380FFF1FEB01FC90C7123F93C7FCA25DD80380137ED80FE0
13FE001F5C4A5AA24848485A4A5A6CC6485A001C495A001E49C8FC000E137C380781F038
03FFC0C648C9FC2A3B7EA72D>I E /Fj 22 118 df<157815FC14031407141F14FF130F
0007B5FCB6FCA2147F13F0EAF800C7FCB3B3B3A6007FB712FEA52F4E76CD43>49
D<EC3FFE0103B512E0010F14FC013F14FF90B712C048D9C07F7F2703FE000F13F8D807F8
01037FD80FE06D7F48486D7F48488001F01680486C6E13C07F486C6E13E07FA27013F0A5
6C5AA26C5AEA0FF0EA03C0C914E05EA218C05E1880A24C13005F4C5A4B5B5F4B5B5F4B5B
4B90C7FC4B5A5E4B5AED7FE04B5A4A5B4A48C8FC4A5A5D4A48EB01F04A5AEC3F804AC7FC
02FEEC03E0495A495A495A495AD91F80140749C8FC013E150F017FB7FC90B812C05A5A5A
5A5A5A5AB9FC1880A4344E79CD43>I<91380FFFC091B512FC0107ECFF80011F15E09026
3FF8077F9026FF800113FC4848C76C7ED803F86E7E491680D807FC8048B416C080486D15
E0A4805CA36C17C06C5B6C90C75AD801FC1680C9FC4C13005FA24C5A4B5B4B5B4B13C04B
5BDBFFFEC7FC91B512F816E016FCEEFF80DA000713E0030113F89238007FFE707E701380
7013C018E07013F0A218F8A27013FCA218FEA2EA03E0EA0FF8487E487E487EB57EA318FC
A25E18F891C7FC6C17F0495C6C4816E001F04A13C06C484A1380D80FF84A13006CB44A5A
6CD9F0075BC690B612F06D5D011F1580010302FCC7FCD9001F1380374F7ACD43>I<B912
F0F0FF8019F819FF1AC0D8000701F0C714F0060F7F060113FE727F737F737F85737F87A2
737FA387A863A2616363A24F5B4F5B4F90C8FC4F5A06035B060F13F095B512C092B8C9FC
19F819E019F89226F0000313FE9439007FFF80727F727F727F727F727F8684A28684A787
A71D1C75133EA38575137E73157C7513FC731401B86C6D9038F803F807039038FE07F073
90B512E0736C14C0080F1400CEEA7FFC5F537CD164>82 D<003FBC1280A59126C0003F90
38C0007F49C71607D87FF8060113C001E08449197F49193F90C8171FA2007E1A0FA3007C
1A07A500FC1BE0481A03A6C994C7FCB3B3AC91B912F0A553517BD05E>84
D<B700FC017FB600FE91B612F0A5D8003F01C0C8001F01E0C9EBF8006F71EE0FC06D7161
876F1C1F6D7196C7FC6F8373606D1E3E6F836D7160876F1CFC6D666F4B801F016D66704A
806E525A88704A17076E059F5F70021F80080F160F6E6570023F806EDC3E074CC8FC8870
027E5F6EDC7C03163E7002FC804F6C167E6E1C7C700101814F6C16FC6E745B7001031701
6E4C6D5D060716C00580496D14036F63DDC00F16E04F6D14076F07F05BDDE01F170F6F92
C76C5D1DF8DDF03E6E141F6F98C9FCDDF87E16FC067C6E5C6FF1FE3EDDFCFC177E6F4A6E
147C1DFFDDFFF06E14FC6F62A24E816F62A270496F5BA24E817061A295C97E7061A27048
7090CAFCA37048705AA24D1601040360A27048705A84537DD18B>87
D<EC7FFF0107B512F0013F14FE90B77E48D9E00F7F2703FE000113F0486C6D7F6EEB3FFC
48826E131F83707FA36C496D7FA26C90C7FC6C5AC9FCA6037FB5FC020FB6FC91B7FC0107
1487013FEBF0074913803901FFFC004813F0485B485B485B4890C7FC5A5BA2485AA45EA2
6D5C007F151D163D6C6C02797F6C6D01F113F86C9026C003E1EBFFE06C9026F81FC014F0
6C90B5487EC6ED001F011F01FC010713E0010101E090C8FC3C387CB641>97
D<913801FFF8021FEBFF8091B612F0010315FC010F9038C00FFE903A1FFE0001FFD97FFC
491380D9FFF05B4817C048495B5C5A485BA2486F138091C7FC486F1300705A4892C8FC5B
A312FFAD127F7FA27EA2EF03E06C7F17076C6D15C07E6E140F6CEE1F806C6DEC3F006C6D
147ED97FFE5C6D6CEB03F8010F9038E01FF0010390B55A01001580023F49C7FC020113E0
33387CB63C>99 D<4DB47E0407B5FCA5EE001F1707B3A4913801FFE0021F13FC91B6FC01
0315C7010F9038E03FE74990380007F7D97FFC0101B5FC49487F4849143F484980485B83
485B5A91C8FC5AA3485AA412FFAC127FA36C7EA37EA26C7F5F6C6D5C7E6C6D5C6C6D49B5
FC6D6C4914E0D93FFED90FEFEBFF80903A0FFFC07FCF6D90B5128F0101ECFE0FD9003F13
F8020301C049C7FC41547CD24B>I<913803FFC0023F13FC49B6FC010715C04901817F90
3A3FFC007FF849486D7E49486D7E4849130F48496D7E48178048497F18C0488191C7FC48
17E0A248815B18F0A212FFA490B8FCA318E049CAFCA6127FA27F7EA218E06CEE01F06E14
037E6C6DEC07E0A26C6DEC0FC06C6D141F6C6DEC3F806D6CECFF00D91FFEEB03FE903A0F
FFC03FF8010390B55A010015C0021F49C7FC020113F034387CB63D>I<ED3FFC0203B5FC
020F14C0023F14E09139FFF81FF0499038C03FF849EB807F49903800FFFC495A495AA249
5AA2EE7FF8495AEE3FF0EE0FC093C7FCAEB712E0A526007FF8C8FCB3B3A7007FB512FEA5
2E547CD329>I<EB3FF0B5FCA51203C6FCB3A4EE1FFC93B512C0030314F0030F8092391F
E07FFC92393F001FFE037C8003F07FDAF1E081ECF3C0DAF7807F8502FFC7FC5CA25CA45C
B3ACB6D8F807B612C0A542537BD24B>104 D<137F497E000313E0487FA2487FA76C5BA2
6C5BC613806DC7FC90C8FCADEB3FF0B5FCA512017EB3B3A6B612E0A51B547BD325>I<EB
3FF0B5FCA512017EB3B3B3B1B612F0A51C537BD225>108 D<D93FF0D91FFCEDFFE0B591
B500C0010713FE030302F0011F6D7E030F6E017F8092271FE07FFCD9FF037F922A3F001F
FE01F8007F0003027C9126FF03E080C602F06DD90780137FDAF1E0038FC77FDAF3C0159E
DAF7806D01BC143F07FC8102FFC75C4A5EA24A5EA44A5EB3ACB6D8F807B6D8C03FB512FE
A567367BB570>I<D93FF0EB1FFCB591B512C0030314F0030F8092391FE07FFC92393F00
1FFE0003027C80C602F07FDAF1E081ECF3C0DAF7807F8502FFC7FC5CA25CA45CB3ACB6D8
F807B612C0A542367BB54B>I<913801FFE0021F13FE91B612C0010315F0010F9038807F
FC903A1FFC000FFED97FF86D6C7E49486D7F48496D7F48496D7F4A147F48834890C86C7E
A24883A248486F7EA3007F1880A400FF18C0AC007F1880A3003F18006D5DA26C5FA26C5F
6E147F6C5F6C6D4A5A6C6D495B6C6D495B6D6C495BD93FFE011F90C7FC903A0FFF807FFC
6D90B55A010015C0023F91C8FC020113E03A387CB643>I<903A3FF001FFE0B5010F13FE
033FEBFFC092B612F002F301017F913AF7F8007FFE0003D9FFE0EB1FFFC602806D7F92C7
6C7F4A824A6E7F4A6E7FA2717FA285187F85A4721380AC1A0060A36118FFA2615F616E4A
5BA26E4A5B6E4A5B6F495B6F4990C7FC03F0EBFFFC9126FBFE075B02F8B612E06F148003
1F01FCC8FC030313C092CBFCB1B612F8A5414D7BB54B>I<90397FE003FEB590380FFF80
033F13E04B13F09238FE1FF89139E1F83FFC0003D9E3E013FEC6ECC07FECE78014EF1500
14EE02FEEB3FFC5CEE1FF8EE0FF04A90C7FCA55CB3AAB612FCA52F367CB537>114
D<903903FFF00F013FEBFE1F90B7FC120348EB003FD80FF81307D81FE0130148487F4980
127F90C87EA24881A27FA27F01F091C7FC13FCEBFFC06C13FF15F86C14FF16C06C15F06C
816C816C81C681013F1580010F15C01300020714E0EC003F030713F015010078EC007F00
F8153F161F7E160FA27E17E07E6D141F17C07F6DEC3F8001F8EC7F0001FEEB01FE9039FF
C00FFC6DB55AD8FC1F14E0D8F807148048C601F8C7FC2C387CB635>I<143EA6147EA414
FEA21301A313031307A2130F131F133F13FF5A000F90B6FCB8FCA426003FFEC8FCB3A9EE
07C0AB011FEC0F8080A26DEC1F0015806DEBC03E6DEBF0FC6DEBFFF86D6C5B021F5B0203
13802A4D7ECB34>I<D93FF8913801FFC0B50207B5FCA50003ED001FC61607B3AE5FA35F
A2017F5D173B177B6D6C14F3DC01E313F06D6CD907C3EBFFC0903A0FFFC03F836D90B512
03010114FE6D6C13F8020701E091C7FC42377BB54B>I E /Fk 4
52 df<EB3FC0EBFFF03803E07C48487E48487E497E001EEB0780A2003E14C0A248EB03E0
A500FC14F0B0007C14E0A3007E1307003E14C0A36CEB0F806C14006D5A3807C03E3803F0
FC3800FFF0EB3FC01C2D7DAB23>48 D<130C133C137CEA03FC12FFEAFC7C1200B3B113FE
387FFFFEA2172C7AAB23>I<EB7F803801FFF0380780FC380E003F48EB1F8048EB0FC05A
0060EB07E012F000FC14F07E1403A3007C1307C7FCA215E0140F15C0141F1580EC3F0014
7E147C5C495A495A495A495A011EC7FC5B5B4913305B485A4848136048C7FC000E14E000
1FB5FC5A4814C0B6FCA21C2C7DAB23>I<EB3FC03801FFF03807C0FC380E007E487FEC1F
80003F14C0A2EB800F1300A2000C131FC7FC1580A2EC3F00143E5C5CEB03F0EBFFC014F0
EB00FC143FEC1F8015C0140F15E0A2EC07F0A21238127C12FEA3EC0FE012F8006014C000
70131F6C1480001EEB3F00380780FC3801FFF038007FC01C2D7DAB23>I
E /Fl 55 123 df<4AB4EB0FE0021F9038E03FFC913A7F00F8FC1ED901FC90383FF03FD9
07F090397FE07F80494801FF13FF4948485BD93F805C137F0200ED7F00EF003E01FE6D91
C7FC82ADB97EA3C648C76CC8FCB3AE486C4A7E007FD9FC3FEBFF80A339407FBF35>11
D<EC03FE91383FFF809138FE03E0903903F800F0D90FE013384948137C90393F8001FE90
387F00035B5BA2485A6F5AED007093C7FCAA16FEB7FCA33901FC000315011500B3AC486C
497EB5D8F87F13FCA32E407EBF33>I<1430147014E0EB01C0EB03801307EB0F00131E13
3E133C5B13F85B12015B1203A2485AA2120F5BA2121F90C7FCA25AA3123E127EA6127C12
FCB2127C127EA6123E123FA37EA27F120FA27F1207A26C7EA212017F12007F13787F133E
131E7FEB07801303EB01C0EB00E014701430145A77C323>40 D<12C07E12707E7E121E7E
6C7E7F12036C7E7F12007F1378137CA27FA2133F7FA21480130FA214C0A3130714E0A613
0314F0B214E01307A614C0130FA31480A2131F1400A25B133EA25BA2137813F85B12015B
485A12075B48C7FC121E121C5A5A5A5A145A7BC323>I<121EEA7F8012FF13C0A213E0A3
127FEA1E601200A413E013C0A312011380120313005A120E5A1218123812300B1C798919
>44 D<B512FEA617067F961E>I<121EEA7F80A2EAFFC0A4EA7F80A2EA1E000A0A798919>
I<EB01C013031307131F137FEA07FFB5FC139FEAF81F1200B3B3ACEB7FF0B612F8A31D3D
78BC2D>49 D<EB07FC90383FFF8090B512E03903F01FF83907C007FC390F0001FE001E6D
7E001C1580003CEC7FC05AED3FE01270B4FC6DEB1FF07FA56C5A6CC7FC120CC813E0153F
A216C0157F168015FF16004A5A5D4A5A4A5A5D4A5A4A5A4AC7FC147E147C5C495A495A49
5A495A49C71270133E133C5B4914E0485A485A485A48C7120148B6FCA25A4815C0B7FCA3
243D7CBC2D>I<EB07FC90383FFF809038F80FE03901E003F839078001FCD80F007F000E
6D7E001E1580D81F80137F486C14C07FA27F5BA2121F6C5AC8138015FF1600A24A5AA24A
5A5DEC07E04A5A023FC7FCEB1FFCECFF809038000FE0EC07F86E7E6E7E6E7E1680ED7FC0
A216E0153FA216F0A2120C123F487E487EA316E0A249137F6CC713C01278EDFF807E6C49
13006C495A3907C007FC3903F80FF0C6B55A013F1380D907F8C7FC243F7CBC2D>I<1238
123C123F90B612FCA316F85A16F016E00078C712010070EC03C0ED078016005D48141E15
1C153C5DC8127015F04A5A5D14034A5A92C7FC5C141EA25CA2147C147814F8A213015C13
03A31307A3130F5CA2131FA6133FAA6D5A0107C8FC26407BBD2D>55
D<EB03FCEB1FFF90387E07C09038FC03F048486C7E48486C7E4848137C000F147E484813
7F81003F15805B007F15C0A2151F12FF16E0A516F0A5127F153FA36C7EA2001F147F120F
6C6C13FF6D13DF000313013900F8039F90387E0F1FD91FFE13E0EB07F090C7FCA2ED3FC0
A41680157FD80F801400487E486C13FEA24A5A5D49485AEB8007391E000FE0001F495A26
0FC07FC7FC3803FFFE6C13F838003FC0243F7CBC2D>57 D<121EEA7F80A2EAFFC0A4EA7F
80A2EA1E00C7FCB3121EEA7F80A2EAFFC0A4EA7F80A2EA1E000A2779A619>I<121EEA7F
80A2EAFFC0A4EA7F80A2EA1E00C7FCB3121E127FEAFF80A213C0A4127F121E1200A41201
1380A3120313005A1206120E120C121C5A1230A20A3979A619>I<007FB912E0BA12F0A2
6C18E0CDFCAE007FB912E0BA12F0A26C18E03C167BA147>61 D<15074B7EA34B7EA34B7E
A34B7EA34B7E15E7A2913801C7FC15C3A291380381FEA34AC67EA3020E6D7EA34A6D7EA3
4A6D7EA34A6D7EA34A6D7EA349486D7E91B6FCA249819138800001A249C87EA24982010E
157FA2011E82011C153FA2013C820138151FA2017882170F13FC00034C7ED80FFF4B7EB5
00F0010FB512F8A33D417DC044>65 D<B712FCEEFF8017F00001903980000FF86C6CC7EA
03FE707E701380EF7FC0EF3FE0A2EF1FF0A218F8A3170F171FA318F0A2EF3FE0177F18C0
EFFF804C1300EE03FCEE0FF8EE7FE091B6C7FC17E091C7EA07FCEE01FE933800FF80EF7F
C0EF3FE0EF1FF018F8170F18FC1707A218FEA718FC170FA2EF1FF818F0173FEF7FE0EFFF
C00403138048486C90380FFE00B85A17E094C7FC373E7DBD40>I<B91280A300019038C0
00036C6C48EB007FEF1FC0170F1707A21703A31701A4EF00E0A21638A31800A31678A216
F81501150791B5FCA3EC8007150115001678A21638A693C8FCAF3801FFE0B612F0A3333E
7DBD3B>70 D<DB3FE0130C912603FFFE131C021F9038FF803C913A7FF00FC07C9139FF00
01F0D903FC90380078FC4948143DD91FE0141F4948140F4948140701FF15034890C8FC49
1501485A000716005B000F177C5B001F173CA2485AA2181C127FA25B95C7FC12FFAB041F
B512F0127FA26D9139000FFE00EF03FC123FA27F121FA26C7EA212077F12036C7E7F6C7F
6D6C14076D7E6D6C140FD907F8141ED903FEEC3C7C902600FF80EBF83C913A7FF007F01C
021FB5EAC00C020391C8FC9138003FF03C427BBF47>I<B6D8C01FB512F8A3000101E0C7
383FFC0026007F80EC0FF0B3A691B7FCA30280C7120FB3A92601FFE0EC3FFCB6D8C01FB5
12F8A33D3E7DBD44>I<B612F0A3C6EBF000EB3FC0B3B3B2EBFFF0B612F0A31C3E7EBD21>
I<011FB512FCA3D9000713006E5A1401B3B3A6123FEA7F80EAFFC0A44A5A1380D87F005B
007C130700385C003C495A6C495A6C495A2603E07EC7FC3800FFF8EB3FC026407CBD2F>
I<B612F8A3000101E0C9FC38007F80B3B0EF0380A517071800A45FA35FA25F5F5F4C5A16
0748486C133FB8FCA3313E7DBD39>76 D<B500C093B512C0A300016D4BEBE000D8007F18
80D977F0ED03BFA3D973F8ED073FA3D971FC150EA2D970FE151CA3027F1538A36E6C1470
A36E6C14E0A26E6CEB01C0A36E6CEB0380A36E6CEB0700A26E6C130EA36E6C5BA3037F5B
A26F6C5AA36F6C5AA392380FE1C0A3923807F380A26FB4C7FCA36F5AA213F8486C6D5AD8
07FFEFFFE0B500F80178017FEBFFC0A34A3E7CBD53>I<B56C91B512F88080D8007F0307
13006EEC01FC6E6E5A1870EB77FCEB73FEA2EB71FF01707FA26E7E6E7EA26E7E6E7EA26E
7E6E7EA26E7E6E7FA26F7E6F7EA26F7E6F7EA26F7E6F7EA26F7E6F1380A2EE7FC0EE3FE0
A2EE1FF0EE0FF8A2EE07FCEE03FEA2EE01FF7013F0A2177F173FA2171F170FA2170701F8
1503487ED807FF1501B500F81400A218703D3E7DBD44>I<B712F8EEFF8017E000019039
C0003FF86C6C48EB07FCEE01FE707EEF7F80EF3FC018E0A2EF1FF0A218F8A818F0A2EF3F
E0A218C0EF7F80EFFF004C5AEE07FCEE3FF091B612C04CC7FC0280C9FCB3A73801FFE0B6
12C0A3353E7DBD3E>80 D<B712C016FCEEFF800001D9C00013E06C6C48EB1FF0EE07FCEE
01FE707E84717EA2717EA284A760177F606017FF95C7FCEE01FCEE07F8EE1FE0EEFF8091
B500FCC8FC16F091388001FCED003FEE1FC0707E707E83160383160183A383A484A4F0C0
04190EA28218E0057F131E2601FFE0161CB600C0EB3FF094381FF83805071370CA3801FF
E09438003F803F407DBD43>82 D<003FB91280A3903AF0007FE001018090393FC0003F48
C7ED1FC0007E1707127C00781703A300701701A548EF00E0A5C81600B3B14B7E4B7E0107
B612FEA33B3D7DBC42>84 D<B500FE017FB5D88007B5FCA3000301C0010101E0C713F86C
90C849EC3FE07148EC0F807E7215006E143F017F190E84A26D6C60A24D7E6D6C60A2EFE7
F86D6C60A2933801C3FC6E18F001076104037F6E0281140101036104077F17006D6C4D5A
A2040EEB7F806D6C4DC7FCA24CEB3FC0DA7F80160EA24CEB1FE003C0161E023F171C0478
14F0DBE070010F133C021F173804F014F84C1307DA0FF05EA2DBF1C0EB03FCDA07F95EA2
DBFB80EB01FEDA03FF6F5AA293C8FCA26E5FA24B157F020094C8FCA24B81037C153EA203
78151E0338151C58407EBD5D>87 D<EAFFFCA4EAF000B3B3B3B3ABEAFFFCA40E5B77C319
>91 D<EAFFFCA4EA003CB3B3B3B3ABEAFFFCA40E5B7FC319>93 D<EB0FF8EBFFFE3903F0
1F8039078007E0000F6D7E9038E001F8D81FF07F6E7EA3157F6C5AEA0380C8FCA4EC1FFF
0103B5FC90381FF87FEB7F803801FC00EA07F8EA0FE0485A485AA248C7FCEE038012FEA3
15FFA3007F5BEC03BF3B3F80071F8700261FC00E13CF3A07F03C0FFE3A01FFF807FC3A00
3FC001F0292A7DA82D>97 D<EA01FC12FFA3120712031201B1EC03FC91381FFF8091387C
07E09039FDE001F09039FFC000FC4A137E91C77E49158049141F17C0EE0FE0A217F0A216
0717F8AA17F0A2160FA217E0161F17C06D1580EE3F006D5C6E13FE9039F3C001F89039F1
E003F09039E0780FC09026C03FFFC7FCC7EA07F82D407EBE33>I<49B4FC010F13E09038
3F00F8017C131E4848131F4848137F0007ECFF80485A5B121FA24848EB7F00151C007F91
C7FCA290C9FC5AAB6C7EA3003FEC01C07F001F140316806C6C13076C6C14000003140E6C
6C131E6C6C137890383F01F090380FFFC0D901FEC7FC222A7DA828>I<ED01FC15FFA315
0715031501B114FF010713E190381F80F990387E003D49131FD803F81307485A49130348
481301121F123F5B127FA290C7FCA25AAA7E7FA2123FA26C7E000F14037F000714076C6C
497E6C6C497ED8007C017913F890383F01F190380FFFC1903A01FE01FC002D407DBE33>
I<EB01FE90380FFFC090383F03F09038FC01F848486C7E4848137E48487F000F15804913
1F001F15C04848130FA2127F16E090C7FCA25AA290B6FCA290C9FCA67EA27F123F16E06C
7E1501000F15C06C6C13036DEB07806C6C1400C66C131E017E5B90381F80F8903807FFE0
010090C7FC232A7EA828>I<EC1FC0EC7FF8903801F83C903807E07E90380FC0FFEB1FC1
EB3F811401137FEC00FE01FE137C1500AEB6FCA3C648C7FCB3AE487E007F13FFA320407E
BF1C>I<167C903903F801FF903A1FFF078F8090397E0FDE1F9038F803F83803F001A23B
07E000FC0600000F6EC7FC49137E001F147FA8000F147E6D13FE00075C6C6C485AA23901
F803E03903FE0FC026071FFFC8FCEB03F80006CAFC120EA3120FA27F7F6CB512E015FE6C
6E7E6C15E06C810003813A0FC0001FFC48C7EA01FE003E140048157E825A82A46C5D007C
153E007E157E6C5D6C6C495A6C6C495AD803F0EB0FC0D800FE017FC7FC90383FFFFC0103
13C0293D7EA82D>I<EA01FC12FFA3120712031201B1EC01FE913807FFC091381E07E091
387803F09138E001F8D9FDC07F148001FF6D7E91C7FCA25BA25BB3A6486C497EB5D8F87F
13FCA32E3F7DBE33>I<EA01E0EA07F8A2487EA46C5AA2EA01E0C8FCACEA01FC127FA312
0712031201B3AC487EB512F0A3143E7DBD1A>I<EA01FC12FFA3120712031201B292B512
80A392383FFC0016E0168093C7FC153C5D5D4A5AEC07C04A5A4AC8FC143E147F4A7E13FD
9038FFDFC0EC9FE0140F496C7E01FC7F496C7E1401816E7E81826F7E151F826F7EA28248
6C14FEB539F07FFFE0A32B3F7EBE30>107 D<EA01FC12FFA3120712031201B3B3B1487E
B512F8A3153F7DBE1A>I<2701F801FE14FF00FF902707FFC00313E0913B1E07E00F03F0
913B7803F03C01F80007903BE001F87000FC2603F9C06D487F000101805C01FBD900FF14
7F91C75B13FF4992C7FCA2495CB3A6486C496CECFF80B5D8F87FD9FC3F13FEA347287DA7
4C>I<3901F801FE00FF903807FFC091381E07E091387803F000079038E001F82603F9C0
7F0001138001FB6D7E91C7FC13FF5BA25BB3A6486C497EB5D8F87F13FCA32E287DA733>
I<14FF010713E090381F81F890387E007E01F8131F4848EB0F804848EB07C04848EB03E0
000F15F04848EB01F8A2003F15FCA248C812FEA44815FFA96C15FEA36C6CEB01FCA3001F
15F86C6CEB03F0A26C6CEB07E06C6CEB0FC06C6CEB1F80D8007EEB7E0090383F81FC9038
0FFFF0010090C7FC282A7EA82D>I<3901FC03FC00FF90381FFF8091387C0FE09039FDE0
03F03A03FFC001FC6C496C7E91C7127F49EC3F805BEE1FC017E0A2EE0FF0A3EE07F8AAEE
0FF0A4EE1FE0A2EE3FC06D1580EE7F007F6E13FE9138C001F89039FDE007F09039FC780F
C0DA3FFFC7FCEC07F891C9FCAD487EB512F8A32D3A7EA733>I<02FF131C0107EBC03C90
381F80F090397F00387C01FC131CD803F8130E4848EB0FFC150748481303121F485A1501
485AA448C7FCAA6C7EA36C7EA2001F14036C7E15076C6C130F6C7E6C6C133DD8007E1379
90383F81F190380FFFC1903801FE0190C7FCAD4B7E92B512F8A32D3A7DA730>I<3901F8
07E000FFEB1FF8EC787CECE1FE3807F9C100031381EA01FB1401EC00FC01FF1330491300
A35BB3A5487EB512FEA31F287EA724>I<90383FC0603901FFF8E03807C03F381F000F00
3E1307003C1303127C0078130112F81400A27E7E7E6D1300EA7FF8EBFFC06C13F86C13FE
6C7F6C1480000114C0D8003F13E0010313F0EB001FEC0FF800E01303A214017E1400A27E
15F07E14016C14E06CEB03C0903880078039F3E01F0038E0FFFC38C01FE01D2A7DA824>
I<131CA6133CA4137CA213FCA2120112031207001FB512C0B6FCA2D801FCC7FCB3A215E0
A912009038FE01C0A2EB7F03013F138090381F8700EB07FEEB01F81B397EB723>I<D801
FC14FE00FF147FA3000714030003140100011400B3A51501A31503120015076DEB06FF01
7E010E13806D4913FC90381FC078903807FFE00100903880FE002E297DA733>I<B539E0
0FFFE0A32707FE000313006C48EB00FC5E00015D7F00005DA26D13016D5CA26D6C485AA2
ECC007011F91C7FCA290380FE00EA2ECF01E0107131CA26D6C5AA2ECFC7801011370A2EC
FEF001005BA2EC7FC0A36E5AA26EC8FCA3140E2B287EA630>I<B53BC3FFFE03FFF8A329
0FFE003FE00013C06C486D48EB3F806C4817006D010F141E00016F131C15076D163C0000
4A6C1338A2017F5E4B7E151DD93F805DED3DFC1538D91FC04A5AED78FE9238707E03D90F
E0017F5BEDE03F02F0140701070387C7FC9138F1C01F02F9148F010315CE9138FB800F02
FF14DE6D15FCED00076D5DA24A1303027E5CA2027C1301023C5C023813003D287EA642>
I<B539E00FFFE0A32707FE000313006C48EB01FC6F5A00015D7F00005DA2017F495AA2EC
8003013F5CA26D6C48C7FCA26E5A010F130EA26D6C5AA2ECF83C01031338A26D6C5AA2EC
FEF001005BA2EC7FC0A36E5AA36EC8FCA2140EA2141E141C143C1438A214780018137012
7EB45BA2495AA248485AD87E07C9FCEA780EEA3C3CEA1FF8EA07E02B3A7EA630>121
D<001FB61280A2EBE0000180140049485A001E495A121C4A5A003C495A141F00385C4A5A
147F5D4AC7FCC6485AA2495A495A130F5C495A90393FC00380A2EB7F80EBFF005A5B4848
13071207491400485A48485BA248485B4848137F00FF495A90B6FCA221277EA628>I
E /Fm 12 117 df<121EEA7F8012FF13C0A213E0A3127FEA1E601200A413E013C0A31201
1380120313005A1206120E5A5A5A12600B1D78891B>44 D<143014F013011303131F13FF
B5FC13E713071200B3B3B0497E497E007FB6FCA3204278C131>49
D<EB03FE90381FFFC0017F13F03901F80FFC3903C001FE48486C7E000EC7EA7F8048EC3F
C0ED1FE04815F00030140F007015F800601407126CB415FC7F7F1503A46C4813076CC7FC
C8FC16F8A2150F16F0151F16E0A2ED3FC0ED7F8016005D5D4A5A4A5A4A5A5D4A5A4A5A4A
C7FC147C5C5C495A495A495A49C7120C131E5B013814185B5B485A4848143848C8123000
0E1570001FB612F0A25A5AB712E0A326427BC131>I<14FF010713E0011F13F890387F00
FE01FC133FD801F0EB1F804848EB0FC049EB07E00007EC03F048481301A290C713F84814
00A47FA26D130116F07F6C6CEB03E013FC6C6CEB07C09039FF800F806C9038C01F006CEB
F03EECF87839007FFEF090383FFFC07F01077F6D13F8497F90381E7FFFD97C1F1380496C
13C02601E00313E048486C13F000079038007FF84848EB3FFC48C7120F003EEC07FE1501
48140016FF167F48153FA2161FA56C151E007C153EA2007E153C003E157C6C15F86DEB01
F06C6CEB03E06C6CEB07C0D803F8EB1F80C6B4EBFF0090383FFFFC010F13F00101138028
447CC131>56 D<14FF010713E0011F13F890387F80FC9038FC007E48487F4848EB1F8048
48EB0FC0000FEC07E0485AED03F0485A16F8007F140190C713FCA25AA216FE1500A516FF
A46C5CA36C7E5D121F7F000F5C6C6C1306150E6C6C5B6C6C5BD8007C5B90383F01E09039
0FFF80FE903801FE0090C8FC150116FCA4ED03F8A216F0D80F801307486C14E0486C130F
16C0ED1F80A249EB3F0049137E001EC75A001C495A000F495A3907E01FE06CB51280C649
C7FCEB1FF028447CC131>I<ED1FFC4AB512C0913907F007F091391F8000FC027EC7123F
D901F8EC0FC049486E7E49486E7E49486E7E49486E7E49C9127E017E8201FE834848707E
4848707EA24848707EA2000F84491603001F84A24848707EA3007F84A24982A300FF1980
AD6C6C4C1300A4003F606D1603A2001F60A26C6C4C5AA26C6C4C5AA20003606D161F6C6C
4C5A000060017F4CC7FC6E5D013F5E6D6C4A5AD907E0EC03F06D6C4A5AD901FCEC1FC0D9
007E4AC8FCDA1F8013FC913907F007F00201B512C09126001FFCC9FC41487BC54C>79
D<EA01FC12FFA3120712031201B3EC03FC91380FFF8091383C07E091387001F89039FDE0
007E02807F01FFEC1F8091C713C049EC0FE049140717F0A2EE03F8A217FCA2160117FEAB
17FC1603A217F8A2EE07F0A26DEC0FE017C06D141F01FBEC3F80D9F380EB7E00D9E1C05B
9039E0F001F89039C03C07E09039801FFF80C7D803FCC7FC2F467DC436>98
D<EC7F80903803FFF090380FC07C90383F000F01FCEB03804848EB01C00003140F4848EB
1FE049133F120F485AA2485AED1FC0007FEC070092C7FCA290C9FC5AAB7E7FA2123F1630
7F001F15706C6C146016E06C6C14C06C6C13010001EC03806C6CEB0700013F131E90381F
C078903807FFF001001380242E7DAC2B>I<EB01FE903807FFC090381F03F090387E00FC
49137E48487F485A4848EB1F80000F15C049130F121F484814E01507A2007F15F090C7FC
A25AA390B6FCA290C9FCA67EA27FA2123F16306C7E1670000F15606D14E06C6C14C00003
14016C6CEB03806C6CEB0700013E131E90381F80F8903803FFE0010090C7FC242E7DAC2B
>101 D<EC7F80903803FFF090380FC0FC90383E001F496D7E496D7E48486D7E48486D7E
48486D7E000F81A24848147E003F157FA290C87E481680A44816C0AA6C1680A26D147F00
3F1600A2001F157E6D14FE000F5D6D130100075D6C6C495A6C6C495A6C6C495A013E49C7
FC90381FC0FE903807FFF89038007F802A2E7DAC31>111 D<3903F803F000FFEB1FFCEC
3C3EEC707F0007EBE0FF3803F9C000015B13FBEC007E153C01FF13005BA45BB3A748B4FC
B512FEA3202C7DAB26>114 D<1306A5130EA4131EA3133E137EA213FE12011207001FB5
12F0B6FCA2C648C7FCB3A4150CAA017E131C017F1318A26D133890381F8030ECC0709038
07E0E0903801FFC09038007F001E3E7EBC26>116 D E /Fn 20 119
df<170FA34D7EA24D7EA34D7EA34D7EA34C7F17DFA29338039FFC178FA29338070FFE17
07040F7FEE0E03A2041E80EE1C01A2043C80EE3800A24C80187FA24C80183FA24B488018
1F0303814C130FA203078193C71207A24B81030E80A24B8284A24B8284A24B82197F03F0
824B153FA20201834B151FA202038392B8FCA24A83A292C91207020E8385A24A8485023C
84023882A20278840270177FA202F0844A173FA24948841A1FA24948841A0FA249CB7F1A
074985865B496C85497E48486C4D7F000F01F8051F13F0B60407B612F0A45C657DE463>
65 D<B712C0A4C66CEB8000D91FFEC7FC6D5AB3B3B3B3AE497E90387FFF80B712C0A422
627AE12F>73 D<B500FC071FB51280A36E61C6F58000013F51C7FCD91DFFF177FCA2011C
6D18E7A36E6CEF01C7A36E6CEF0387A36E6CEF0707A26E6C170EA36E6C171CA36E6C1738
A36E6C1770A26E6D16E0A36F6CED01C0A36F6CED0380A36F6CED0700A26F6C150EA36F6C
5DA36F6C5DA36F6C5DA26F6D5CA3706C495AA3706C495AA3706C49C7FCA2706C130EA370
6C5BA3706C5BA3706C5BA3706D5AA294387FC1C0A394383FE380A3DD1FF7C8FCA3EF0FFE
A2013E6F5AA2137F715A2601FFC04F7E000701F896383FFF80B66C6D48023FB61280A371
5A696278E17A>77 D<933801FFE0043F13FF4BB612E003079038003FF8DB1FF0EB03FEDB
7FC0903800FF804A48C8EA3FE0DA03FCED0FF0DA0FF0ED03FC4A486F7E4A486F7E4A4870
7E4ACA6C7E4948717E4948717E4948717E4948717E4948717E013F854A83017F86494872
7EA24890CC6C7EA24848737EA24848737EA2000F87491907001F87A34848737EA4007F1C
80A24985A400FF1CC0AF6C6C4F1380A5003F1C006D61A3001F63A26D190F000F63A26C6C
4F5AA36C6C4F5AA26C6D4E5A6C636E18FF017F626D6C4D90C7FC6E5F011F616D6C4D5A6D
6C4D5A0103616E171F6D6C4D5A6D6D4C5ADA3FC04CC8FCDA1FF0ED03FE6E6C4B5A6E6C4B
5ADA01FFED3FE09126007FC0ECFF80DB1FF0D903FEC9FCDB07FFEB3FF8030190B512E0DB
003F91CAFC040113E05A667AE367>79 D<B912C018FEF0FFC019F0C601FCC813FCD93FF8
ED0FFF011F04037F06007FF13FF0737E737E1907737E86731380A27313C0A31BE01A7FA2
1BF0A91BE0A21AFF1BC0A34F13801B00614F5A624F5A4F5AF17FE04F5A060390C7FCF01F
FE943801FFF891B812E096C8FC18F802F8CCFCB3B3A4497E90B5FCB7FCA44C6279E15A>
I<B600FC0207B600E00203B512FCA4000191C9000F01F8C9003F13C026007FFC040301E0
040F13006D487049EE07FC7A5A73725A131F696E717E010F67A26E721603010767A26E4D
7E6D54C7FCA2876D6DDB01CF170EA2876FDB0387171E6D1E1CA26F92260703FF163C027F
1D38A26F030F80023FDC0E015FA26F031E80021FDC1C005FA2886E6C4B017F4B5AA36F4B
6D6C1403020765A26F03F06E14076E4C011F93C8FCA2700101816E4C010F150EA2886E6D
494801075DA37049C76C6C143C037F1B38A27049701378033F020E6E1570A270011E8203
1F021C6E5DA2896F6C49037F495AA21DF07049033F1303030763A2704992381FF8076F98
C9FCA2058117FC6F4A030F130EA205C317FE6F4A03075BA21DFFDC7FE7C96C5BA305FE70
13F8043F61A37048705BA37048715AA37048715AA34D171F040396CAFCA24D830401180E
86647FE189>87 D<4AB47E020F13F8023F13FE9139FF007F80D903FCEB07E0D907F0EB01
F0D91FE0EB007849488049488049C87E48485D4915FF00034B138048485CA2485AA2485A
A2003F6F130049EC007C94C7FC127FA35B12FFAD127F7FA4123F7FA2001FEE01C07F000F
16036D168012076C6C15076D160000015E6C6C151E6D6C5C6D6C5C6D6C5CD90FF8495AD9
03FCEB07C0903A00FF803F8091263FFFFEC7FC020F13F80201138032417CBF3A>99
D<181EEF3FFEEE07FFA4EE000F1703A21701B3AAEDFF80020F13F8023F13FE9139FF803F
81903A03FC0007C14948EB01E1D91FE0EB00F94948147D4948143D49C8121F4848150F49
1507120348481503491501120F121F5BA2123F5B127FA45B12FFAD127F7FA3123FA27F12
1FA26C6C1503A26C6C150712036D150F6C6C151F0000163D137F6D6CECF9FF6D6CEB01F1
D90FF0D903C113C06D6CD90F81EBFF80D901FFEB7F019039007FFFFC021F13E002010100
91C7FC41657CE349>I<EC03FE91381FFFE091B512F8903901FE03FE903A07F0007F8049
486D7ED93FC06D7E49C76C7E496E7E49140348488148481401000782491400000F828348
5A1880123F49153FA2007F17C0A35BA212FF90B8FCA30180CAFCA9127F7FA3123FA27F12
1FEF01C06C7E17036C6C1680A26C6C15070001EE0F006D150E6C6C151E6D6C5C6D6C5C6D
6C5CD907F0EB03E0D903FC495A902700FF803FC7FC91383FFFFC020F13F0020113803241
7CBF3A>I<ED0FF0ED7FFC4AB5FC913907F81F8091390FE00FC091381FC03F91393F807F
E0EC7F005C495A5C0103EC3FC0A24948EB0F0093C7FCA2495AB3A5B712F0A426000FF0C8
FCB3B3B0497EEB3FFE003FB6FCA42B657EE428>I<EB03C0EA07FFB5FCA41201EA007FA2
133FB3AAEE7FE0923803FFFC030F13FFDB3F0013C00378EB1FE04B6D7EDAC1C06D7EDAC3
808002C7C7120302CE81170114DC14D802F86E7E5CA35CA35CB3B3496C4A7F496C4A7FB6
D8F003B612C0A442647DE349>104 D<133C13FF487F487FA66C5B6C90C7FC133C90C8FC
B3A2EB03C0EA07FF127FA41201EA007FA2133FB3B3AC497E497EB612E0A41B5F7DDE23>
I<EB03C0EA07FFB5FCA41201EA007FA2133FB3B3B3B3AD497E497EB612F0A41C647DE323
>108 D<D903C0EB7FE0D807FF903803FFFCB5010F13FFDB3F0013C00378EB1FE04B6D7E
0001D9C1C06D7E27007FC3808002C7C71203D93FCE81170114DC14D802F86E7E5CA35CA3
5CB3B3496C4A7F496C4A7FB6D8F003B612C0A4423F7DBE49>110
D<EDFF80020F13F8023F13FE9139FF007F80D903FCEB1FE0D907F0EB07F0D90FC0EB01F8
D93F80EB00FE49C8127F017E81496F7E48486F7E00038349150700078348486F7EA2001F
83491501A2003F83A348486F7EA400FF1880AC007F1800A26D5DA2003F5FA36C6C4B5AA3
6C6C4B5A00075FA26C6C4B5A6C6C4B5AA26C6C4B5A017F4BC7FC6D6C14FE6D6C495AD90F
F0EB07F8D903FCEB1FE0D900FFEB7F806EB5C8FC020F13F8020113C039417CBF42>I<90
39078003F8D807FFEB0FFFB5013F13C092387C0FE0913881F01F9238E03FF00001EB8380
39007F8700148FEB3F8E029CEB1FE0EE0FC00298EB030002B890C7FCA214B014F0A25CA5
5CB3B0497EEBFFF8B612FCA42C3F7CBE33>114 D<9139FFE00180010FEBFC03017FEBFF
073A01FF001FCFD803F8EB03EFD807E0EB01FF48487F4848147F48C8123F003E151F007E
150F127CA200FC1507A316037EA27E7F6C7E6D91C7FC13F8EA3FFE381FFFF06CEBFF806C
14F86C14FF6C15C06C6C14F0011F80010714FED9007F7F02031480DA003F13C015030300
13E0167F00E0ED1FF0160F17F86C15071603A36C1501A37EA26C16F016037E17E06D1407
6DEC0FC06D1580D8FDF0141FD8F8F8EC7F00013E14FC3AF01FC00FF80107B512E0D8E001
148027C0003FF8C7FC2D417DBF34>I<1438A71478A414F8A31301A31303A21307130F13
1FA2137F13FF1203000F90B6FCB8FCA3260007F8C8FCB3AE17E0AE6D6CEB01C0A316036D
6C148016076D6C14006E6C5A91383FC01E91381FF07C6EB45A020313E09138007F802B59
7FD733>I<D903C0150FD807FFED1FFFB50203B5FCA40001ED0007D8007F1501A2013F81
B3B25FA35FA35F011F15066E140E5F130F6E4A7F01075D6D6C494813E0D901FE4948EBFF
C0903A00FFC01F8091393FFFFE00020F13F8020001C0EC800042407DBE49>I<B66C49B5
12E0A4000101F8C8387FFE0026007FE0ED1FF819E0013F705A61131F6E93C7FC130F180E
6E151E0107161C8001035EA26E157801011670806D5EA26F1301027F5DA26E6C495AA26F
1307021F92C8FCA26E6C130EA26F131E0207141CA26F133C020314388102015CA26F13F0
6E5C168092387F81C0A216C3033F5B16E3DB1FE7C9FCA216FF6F5AA26F5AA36F5AA26F5A
A36F5A433F7FBD46>I E end
%%EndProlog
%%BeginSetup
%%Feature: *Resolution 600dpi
TeXDict begin
%%PaperSize: a4

%%EndSetup
%%Page: 1 1
1 0 bop 451 912 a Fn(An)44 b(Inductiv)l(e)h(Pro)t(of)e(of)f(the)i(W)-11
b(ellfoundedness)45 b(of)e(the)1447 1095 y(Multiset)i(Order)1512
1551 y Fm(Octob)s(er)32 b(12,)h(1998)523 1900 y Fl(The)38
b(follo)m(wing)f(note)i(presen)m(ts)f(an)h(inductiv)m(e)e(pro)s(of)g
(of)i(the)f(w)m(ellfoundedness)382 2013 y(of)f(the)g(m)m(ultiset)f
(order)g(due)h(to)g(Wilfried)e(Buc)m(hholz)2279 1980
y Fk(1)2355 2013 y Fl(comm)m(unicated)i(to)g(me)3198
1980 y Fk(2)3275 2013 y Fl(b)m(y)382 2126 y(Ralph)29
b(Matthes)976 2093 y Fk(3)1017 2126 y Fl(.)40 b(All)29
b(t)m(yp)s(os)i(are)f(en)m(tirely)g(mine.)382 2413 y
Fj(1)135 b(W)-11 b(ellfounded)45 b(part)382 2616 y Fl(Giv)m(en)35
b(a)h(binary)e(relation)g Fi(<)i Fl(on)f(a)h(set)g Fi(S)5
b Fl(,)37 b(the)e(subset)g Fi(W)48 b Fl(of)36 b Fi(S)k
Fl(called)35 b(the)g Fh(w)m(ell-)382 2728 y(founded)g(part)30
b Fl(of)h Fi(S)k Fl(w.r.t.)c Fi(<)f Fl(is)f(de\014ned)g(inductiv)m(ely)
f(as)j(follo)m(ws)e([1)q(]:)1584 2914 y Fg(8)p Fi(y)f(<)d(x:)30
b(y)e Fg(2)d Fi(W)p 1584 2954 585 4 v 1746 3038 a(x)g
Fg(2)g Fi(W)382 3204 y Fl(The)39 b(corresp)s(onding)e(induction)f
(principle)g(easily)i(yields)g(the)h(principle)d(of)46
b Fh(w)m(ell-)382 3317 y(founded)35 b(part)g(induction)p
Fl(:)1239 3503 y Fg(8)p Fi(x)25 b Fg(2)f Fi(W)m(:)31
b Fl(\()p Fg(8)p Fi(y)d(<)d(x:)31 b(P)13 b Fl(\()p Fi(y)s
Fl(\)\))26 b Fg(\))f Fi(P)13 b Fl(\()p Fi(x)p Fl(\))p
1239 3543 1275 4 v 1603 3626 a Fg(8)p Fi(x)25 b Fg(2)g
Fi(W)m(:)31 b(P)13 b Fl(\()p Fi(x)p Fl(\))382 3812 y(It)30
b(also)h(follo)m(ws)e(that)i Fi(<)f Fl(is)g(w)m(ellfounded)e(i\013)h
Fi(W)38 b Fl(=)25 b Fi(S)5 b Fl(.)382 4098 y Fj(2)135
b(The)44 b(pro)t(of)382 4301 y Fl(Let)32 b Fi(<)f Fl(b)s(e)f(a)i(w)m
(ellfounded)d(relation)h(on)i(a)f(set)h Fi(A)p Fl(,)g(and)f(let)g
Fg(M)p Fl(\()p Fi(A)p Fl(\))h(b)s(e)f(the)g(set)h(of)g(all)382
4414 y(\014nite)26 b(m)m(ultisets)h(o)m(v)m(er)i Fi(A)p
Fl(.)40 b(W)-8 b(e)28 b(use)f(set-notation)i(for)e(m)m(ultisets.)39
b(The)27 b(letters)h Fi(a)f Fl(and)382 4527 y Fi(b)37
b Fl(range)h(o)m(v)m(er)g(A;)g Fi(K)7 b Fl(,)38 b Fi(M)47
b Fl(and)37 b Fi(N)47 b Fl(range)38 b(o)m(v)m(er)g Fg(M)p
Fl(\()p Fi(A)p Fl(\).)62 b(W)-8 b(e)38 b(de\014ne)f(the)g(follo)m(wing)
p 382 4611 1196 4 v 486 4665 a Ff(1)520 4697 y Fe(Mathematisc)n(hes)195
b(Institut,)235 b(Ludwig-Maximilians-Univ)n(ersit\177)-38
b(at)195 b(M)r(\177)-41 b(unc)n(hen,)382 4788 y Fd
(www.mathematik.uni-muenchen.de)q(/~ga)q(dmin)q(6/pro)q(fess)q(oren)q
(/buch)q(holz)486 4848 y Ff(2)520 4879 y Fe(T)-6 b(obias)78
b(Nipk)n(o)n(w,)90 b(Institut)77 b(f)r(\177)-41 b(ur)78
b(Informatik,)90 b(T)-6 b(ec)n(hnisc)n(he)77 b(Univ)n(ersit\177)-38
b(at)77 b(M)r(\177)-41 b(unc)n(hen,)382 4971 y Fd
(www.in.tum.de/~nipkow)486 5030 y Ff(3)520 5062 y Fe(Institut)168
b(f)r(\177)-41 b(ur)170 b(Informatik,)204 b(Ludwig-Maximilians-Univ)n
(ersit\177)-38 b(at)169 b(M)r(\177)-41 b(unc)n(hen,)382
5153 y Fd(www.tcs.informatik.uni-muenche)q(n.de)q(/~ma)q(tthes)1854
5652 y Fl(1)p eop
%%Page: 2 2
2 1 bop 382 548 a Fl(abbreviations:)709 713 y Fi(M)36
b(<)24 b(a)84 b Fg(,)e(8)p Fi(b)25 b Fg(2)g Fi(M)5 b(:)31
b(b)25 b(<)g(a)519 851 y(N)36 b(<)699 866 y Fc(mul)q(t)878
851 y Fi(M)94 b Fg(,)82 b(9)p Fi(M)1372 865 y Fk(0)1412
851 y Fi(;)15 b(a;)g(K)q(:)32 b(M)j Fl(=)25 b Fi(M)1982
865 y Fk(0)2042 851 y Fg([)20 b(f)p Fi(a)p Fg(g)h(^)f
Fi(N)35 b Fl(=)25 b Fi(M)2655 865 y Fk(0)2715 851 y Fg([)19
b Fi(K)27 b Fg(^)20 b Fi(K)32 b(<)25 b(a)878 988 y(W)106
b Fl(=)92 b(the)31 b(w)m(ellfounded)d(part)i(of)h Fg(M)p
Fl(\()p Fi(A)p Fl(\))g(w.r.t.)g Fi(<)2783 1003 y Fc(mul)q(t)382
1161 y Fh(Lemma)i(2.1)46 b Fb(If)26 b Fg(8)p Fi(b)f(<)g(a:)i
Fg(8)p Fi(M)35 b Fg(2)25 b Fi(W)m(:)i(M)17 b Fg([)7 b(f)p
Fi(b)p Fg(g)26 b(2)f Fi(W)39 b Fb(and)28 b Fi(M)2525
1175 y Fk(0)2590 1161 y Fg(2)d Fi(W)39 b Fb(and)27 b
Fg(8)p Fi(M)35 b(<)3216 1176 y Fc(mul)q(t)382 1274 y
Fi(M)470 1288 y Fk(0)510 1274 y Fi(:)d(M)f Fg([)19 b(f)p
Fi(a)p Fg(g)27 b(2)d Fi(W)46 b Fb(then)33 b Fi(M)1438
1288 y Fk(0)1497 1274 y Fg([)20 b(f)p Fi(a)p Fg(g)26
b(2)f Fi(W)13 b Fb(.)382 1466 y Fh(Pro)s(of)90 b Fl(b)m(y)42
b(de\014nition)d(of)i Fi(W)13 b Fl(.)74 b(Let)42 b Fi(N)54
b(<)1962 1481 y Fc(mul)q(t)2161 1466 y Fi(M)2249 1480
y Fk(0)2316 1466 y Fg([)27 b(f)p Fi(a)p Fg(g)p Fl(.)75
b(W)-8 b(e)43 b(need)e(to)i(pro)m(v)m(e)382 1579 y Fi(N)35
b Fg(2)25 b Fi(W)13 b Fl(.)40 b(There)30 b(are)h(t)m(w)m(o)g(p)s
(ossibilities)26 b(wh)m(y)k Fi(N)35 b(<)2186 1594 y Fc(mul)q(t)2366
1579 y Fi(M)2454 1593 y Fk(0)2514 1579 y Fg([)20 b(f)p
Fi(a)p Fg(g)31 b Fl(holds:)518 1734 y Fg(\017)46 b Fl(If)32
b Fi(N)37 b Fl(=)28 b Fi(M)j Fg([)21 b(f)p Fi(a)p Fg(g)32
b Fl(for)g(some)g Fi(M)38 b(<)1849 1749 y Fc(mul)q(t)2031
1734 y Fi(M)2119 1748 y Fk(0)2190 1734 y Fl(then)32 b
Fi(N)38 b Fg(2)27 b Fi(W)44 b Fl(follo)m(ws)31 b(from)g(the)609
1846 y(third)e(assumption.)518 2021 y Fg(\017)46 b Fl(If)26
b Fi(N)36 b Fl(=)25 b Fi(M)989 2035 y Fk(0)1041 2021
y Fg([)13 b Fi(K)33 b Fl(for)26 b(some)h Fi(K)32 b(<)25
b(a)i Fl(then)f Fi(N)35 b Fg(2)25 b Fi(W)39 b Fl(follo)m(ws)26
b(from)g(the)h(\014rst)f(t)m(w)m(o)609 2134 y(assumptions)j(b)m(y)h
(induction)e(on)i(the)h(size)f(of)h Fi(K)7 b Fl(.)3303
2289 y Fa(2)382 2462 y Fh(Lemma)33 b(2.2)46 b Fb(If)24
b Fg(8)p Fi(b)g(<)h(a:)g Fg(8)p Fi(M)35 b Fg(2)25 b Fi(W)m(:)f(M)12
b Fg([)r(f)p Fi(b)p Fg(g)26 b(2)f Fi(W)37 b Fb(then)24
b Fg(8)p Fi(M)35 b Fg(2)25 b Fi(W)m(:)g(M)12 b Fg([)r(f)p
Fi(a)p Fg(g)25 b(2)g Fi(W)13 b Fb(.)382 2653 y Fh(Pro)s(of)66
b Fl(F)-8 b(rom)31 b(Lemma)f(2.1)i(b)m(y)e(w)m(ellfounded)e(part)i
(induction.)668 b Fa(2)382 2826 y Fh(Lemma)33 b(2.3)46
b Fg(8)p Fi(M)35 b Fg(2)24 b Fi(W)m(:)33 b(M)e Fg([)20
b(f)p Fi(a)p Fg(g)26 b(2)f Fi(W)13 b Fb(.)382 3018 y
Fh(Pro)s(of)66 b Fl(F)-8 b(rom)31 b(Lemma)f(2.2)i(b)m(y)e(w)m
(ellfounded)e(induction)g(on)i Fi(a)p Fl(.)663 b Fa(2)382
3191 y Fh(Theorem)34 b(2.4)46 b Fi(M)35 b Fg(2)25 b Fi(W)13
b Fb(.)382 3382 y Fh(Pro)s(of)67 b Fl(b)m(y)30 b(induction)f(on)h(the)h
(size)g(of)f Fi(M)10 b Fl(.)42 b(The)30 b(base)h(case)h
Fg(;)26 b(2)f Fi(W)43 b Fl(holds)30 b(b)s(ecause)382
3495 y(there)g(is)g(no)g Fi(N)35 b(<)1011 3510 y Fc(mul)q(t)1191
3495 y Fg(;)p Fl(.)41 b(Lemma)31 b(2.3)g(co)m(v)m(ers)h(the)f
(induction)d(step.)480 b Fa(2)382 3681 y Fl(Th)m(us)29
b(w)m(e)i(kno)m(w)f(that)h Fi(<)1251 3696 y Fc(mul)q(t)1436
3681 y Fl(is)f(w)m(ellfounded)e(on)i(all)f(of)i Fg(M)p
Fl(\()p Fi(A)p Fl(\).)382 3962 y Fj(3)135 b(T)-11 b(ermination)382
4165 y Fl(As)42 b(is)g(w)m(ell)f(kno)m(wn,)k(w)m(ellfoundedness)40
b(is)h(classically)g(equiv)-5 b(alen)m(t)42 b(with)f(termina-)382
4277 y(tion,)48 b(i.e.)d(the)g(absence)h(of)f(in\014nite)d(descending)i
(c)m(hains.)84 b(T)-8 b(aking)44 b(the)i(classical)382
4390 y(p)s(ersp)s(ectiv)m(e,)34 b(w)m(e)h(can)f(turn)g(things)f(around)
g(and)g(de\014ne)h Fi(W)46 b Fl(as)35 b(the)f(set)h(of)f(all)f(ter-)382
4503 y(minating)39 b(elemen)m(ts)i(of)f Fi(S)5 b Fl(.)71
b(No)m(w)41 b(w)m(ellfounded)d(part)i(induction)e(is)i(simply)e(go)s(o)
s(d)382 4616 y(old)33 b(w)m(ellfounded)e(induction,)h(and)h(the)h
(inductiv)m(e)e(c)m(haracterization)j(of)f Fi(W)46 b
Fl(is)33 b(no)m(w)382 4729 y(a)e(consequence)g(of)f(this)g(direct)f
(de\014nition)f(of)j Fi(W)13 b Fl(.)382 5009 y Fj(References)382
5212 y Fl([1])46 b(P)-8 b(.)28 b(Aczel.)36 b(An)27 b(in)m(tro)s
(duction)e(to)j(inductiv)m(e)e(de\014nitions.)33 b(In)27
b(J.)g(Barwise,)h(editor,)523 5325 y Fb(Handb)-5 b(o)g(ok)35
b(of)e(Mathematic)-5 b(al)34 b(L)-5 b(o)g(gic)p Fl(.)32
b(North-Holland,)d(1977.)1854 5652 y(2)p eop
%%Trailer
end
userdict /end-hook known{end-hook}if
%%EOF

• Prev: Book: "Theorem Proving with the Real Numbers"
• Next: Re: A new proof of the wellfoundednes of the multiset ordering
• Index(es):
  • Main
  • Thread