%!PS-Adobe-2.0
%%Creator: dvipsk 5.66a Copyright 1986-97 Radical Eye Software (www.radicaleye.com)
%%Title: completeness.dvi
%%Pages: 6
%%PageOrder: Ascend
%%BoundingBox: 0 0 612 792
%%DocumentFonts: CMR12 CMTT10 CMSY7 CMSY10 CMTT8 CMBSY10 CMBX10 CMR5
%%+ CMR10 CMSY8 LASYB10 CMR7
%%EndComments
%DVIPSCommandLine: dvips completeness.dvi
%DVIPSParameters: dpi=600
%DVIPSSource: TeX output 2000.06.28:0931
%%BeginProcSet: tex.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]{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 /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 false[(Display)(NeXT)
(LaserWriter 16/600)]{dup length product length le{dup length product
exch 0 exch getinterval eq{pop true exit}if}{pop}ifelse}forall}{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
%%BeginProcSet: texps.pro
%!
TeXDict begin /rf{findfont dup length 1 add dict begin{1 index /FID ne 2
index /UniqueID ne and{def}{pop pop}ifelse}forall[1 index 0 6 -1 roll
exec 0 exch 5 -1 roll VResolution Resolution div mul neg 0 0]/Metrics
exch def dict begin Encoding{exch dup type /integertype ne{pop pop 1 sub
dup 0 le{pop}{[}ifelse}{FontMatrix 0 get div Metrics 0 get div def}
ifelse}forall Metrics /Metrics currentdict end def[2 index currentdict
end definefont 3 -1 roll makefont /setfont cvx]cvx def}def /ObliqueSlant
{dup sin S cos div neg}B /SlantFont{4 index mul add}def /ExtendFont{3 -1
roll mul exch}def /ReEncodeFont{/Encoding exch def}def end
%%EndProcSet
%%BeginFont: CMR7
%!PS-AdobeFont-1.1: CMR7 1.0
%%CreationDate: 1991 Aug 20 16:39:21
% Copyright (C) 1997 American Mathematical Society. All Rights Reserved.
11 dict begin
/FontInfo 7 dict dup begin
/version (1.0) readonly def
/Notice (Copyright (C) 1997 American Mathematical Society. All Rights Reserved) readonly def
/FullName (CMR7) readonly def
/FamilyName (Computer Modern) readonly def
/Weight (Medium) readonly def
/ItalicAngle 0 def
/isFixedPitch false def
end readonly def
/FontName /CMR7 def
/PaintType 0 def
/FontType 1 def
/FontMatrix [0.001 0 0 0.001 0 0] readonly def
/Encoding 256 array
0 1 255 {1 index exch /.notdef put} for
dup 43 /plus put
readonly def
/FontBBox{-27 -250 1122 750}readonly def
/UniqueID 5000790 def
currentdict end
currentfile eexec
9b9c1569015f2c1d2bf560f4c0d52257bacdd6500abda5ed9835f6a016cfc8f0
0b6c052ed76a87856b50f4d80dfaeb508c97f8281f3f88b17e4d3b90c0f65ec3
79791aacdc162a66cbbc5be2f53aad8de72dd113b55a022fbfee658cb95f5bb3
2ba0357b5e050fddf264a07470bef1c52119b6fbd5c77ebed964ac5a2bbec9d8
b3e48ae5bb003a63d545774b922b9d5ff6b0066ece43645a131879b032137d6d
823385fe55f3402d557fd3b448685940729e6e22f4be0e08c6505cba868f7950
93f556b64b808dd710eb936d3ac83e5783b5f7e56d363a59a026a5619a357d21
c4e77bea121eb24b09027d1aad93158edf912940e91cd2f17922b35885894644
7773730bb19af9e70453e1b78d5edc123b273a979891d6d5e624f4a388f3897e
13b045e34b4ee2f5e4fc5e996d3549640010c671de14d18b0b3cd300e57dac03
22e59bfbf7b29422230870f5897fcfaad4b50c7c1c58edcd119218163d6f6e56
25ccb882db7b6d09a1586508e8cb642a11c29a46915e4a96e282079cb21922c1
c2e360b487a45302fd22ec8c5fab63e54b5e844d4b17ca2fff37c69c366dd72a
d02922c14c0932f65ed03e4219c117962edbad2dcdeaa9c10ce8af38a4ae52e2
b377245b0be19a77d6c936e7530cc4d0b78d0cc4a92698fa2870fa54f2d8503e
2d17b3d52fb2febb09f2b2af0c2a1892039ebe19a690098799a858e3d39631bd
6925a154d161df3918074ada6bd52baddd0adc3f07e2d9f15e27cbf7fe8b98c4
07205c811121fa91e059f2f99322fed63f359ac9da97aec383f067f23e5de331
51e80f0a88ab50fe8fdae4a5de93c1ae2fdca06150b37246140c0e87cb2325a6
0d2349162ae3ac93144eee1e665a1289105318fdfe86b6e76251cb25adc967d3
d0b97fe5e279e1161736ab22b4ca510b964342383a840defd38f96a7280e6ac1
34e48d740607ff2e7804164a16d47735864db847c97335e6d4215cb99911a1ec
015a3edaac1f28fedd56d2467130d07bae9416c15f0827d27c6c79f59054282a
418c12c157c91223a829947f47592f7cafd93ca182b25a73a9419127e3b12a9e
5167ac3963f2b019b338ac46d63880f94dda4b538835884d2a5538c85528d6bd
977f844d32b43b0e48caed5a4bdabcefe71695d69ca784dc64b133e0a1ad75f6
c55499b6157e9c9fe0a4116b869671d467a70ac26288407c06c5438405d242a2
2bfcfa67fc5350d355986b8ffd1e18d973f2cf2042fdc530b7305c199d70174c
b41fbaa1e51a936b61238b8f78ff346b7d7e2ee7e6cae91c116f11df51285fd6
45d9ff3362850205a0f4de7498b68f0716a3dcff3b8f6037f253186228923ac4
13aa11df2377e398c58ff868054c79873198b2a98c11a5c287353dadd960b7fd
9ee645980be3247225fdf3b35a006657577b804712dcbd9d5d4ee3b1d659186f
3cf54baab9c0d7f29749e383ae6dda7d1493232ad338c15706c3e220e2301bf3
97996025e6448065fcf5f42b60e9b5cf49a0754ec07f1d9f0f48eea1356d4c99
de
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
cleartomark
%%EndFont
%%BeginFont: LASYB10
%!PS-AdobeFont-1.1: LASYB10 1.00
%%CreationDate: 1992 Oct 23 20:19:19
% Copyright (C) 1997 American Mathematical Society. All Rights Reserved.
11 dict begin
/FontInfo 7 dict dup begin
/version (1.00) readonly def
/Notice (Copyright (C) 1997 American Mathematical Society. All Rights Reserved) readonly def
/FullName (LASYB10) readonly def
/FamilyName (LaTeX) readonly def
/Weight (Bold) readonly def
/ItalicAngle -14.035 def
/isFixedPitch false def
end readonly def
/FontName /LASYB10 def
/PaintType 0 def
/FontType 1 def
/FontMatrix [0.001 0 0 0.001 0 0] readonly def
/Encoding 256 array
0 1 255 {1 index exch /.notdef put} for
dup 50 /a50 put
dup 51 /a51 put
dup 59 /a59 put
readonly def
/FontBBox{-29 -219 1086 697}readonly def
/UniqueID 5011950 def
currentdict end
currentfile eexec
80347982ab3942d930e069a70d0d48311d725e830d1c76fba12e12486e989c98
74c2b527f0925722787027f44470d484262c360cdfdddf3657533a57bb16f730
48bfbbfcb73a650484015441fdc837add94ac8fbd2022e3ec8f115d4b4bb7b7f
15388f22cc6198efe768bd9fceb3446ee4a8dc27d6cd152485384ef5f59381ff
da43f2d20c8fb08aa27ab2015b774db10dacfdcd33e60f178c461553146ab427
bdd7da12534ba078ad3d78041490e255e7bea26ee642aef010c9bda4efe5f68a
908b64df8a52bf05c5af6317d887e45ccf36a8dcd827096c7adac5cac39661b0
998fd6418f316a6756eb874d1e22ea875621d689d84924ba14836ff946d3b62c
39625025b68b0a2bf41ef0f89edee9c0785dedc5698e99695578d0de4648a0a1
632d9c8f99867829211d911138d78a645bbba26e47378eaae2d43df7f3153301
d45a2a4dbcac308dfdffa623fb03b0ae4bff93bc4c60a6273d70e4860d379e2a
75653dae82da757424e970527b3bb2ba29beccaef62031abc96dcaaa43e3c084
1294723a49ace2e235e813dbbc22b1e709c0f3fff2f130bec1e97a70ef2d742d
5342676c9c8b9da59419dccc233ec79e6269fe193975fa7d32c82007ed307e2b
8aef65a1ef5641d2501aed1513e0f04036e92e4d541733be29f31346b395e83f
0de2f9f18c1f1c5cb7883f7ef17790a939bfb1309e284f7c6827b0792b525417
82f3f64a3c3a727a93e26f837de3ddf2b541c125283d63def8611ec17e0d2f3e
94688339a1b5f810dee37f77c6fbd891ff00f7758517cfc535db0d1418deb55d
9c083b4228bc1b071c171e77095457e0c9d7fa4d114a97f12a15b18afca263da
39d8af8a3d3ef2c827355b4cdb1e4268026ba0039179298513b26077f1a69a06
f230e4707a7c7ac822b18e1b05f2e629b4ce72bbcf59d25280e19bfc2396c096
4bcdd6639be8532a38d32addd4f138315fd1b50ec74c0055d4e210781900c85b
cc8dd9c7dd53434840a4f69f5768c64d932ee77de3c6a40a9f0b8d4d3415222b
8b81071a62ae4fac43c576e589c2e771dec549839f29047871da39fed8cfbfa5
654253963ea9efa3e406c55bbd1d75e0689cda9bb4281fc558529d3a83a7bc94
f1749f78d8f9136ce581d6ab3c8b78ff8cbb539f565456d213d7e31193bb28b4
744677f351194fd160af192021d1a28f9aaf38c8247a2e5c6ddd1af20f1c67f5
fe24a775e2818c4b7bc1397816cf8ad4a8a856963390fbdaab8c8b73913b6fb4
39498953ec6eeca359dcd6c251b6073c49dc53d1793362545318382bfe02c9ff
3ef5e68c9f741c9e6ca6cb20ed7740b41574ff64641d0958a245d73ed57b2a6b
f208d24c9165fc1666e41741923940c7445d3f9f823f1cf66bfe40cb20567069
4e9835c08fbaaf116ee43e414fc30cbcd3ea4143a35e4b6399496fe1b684c589
9188df28084070514c7d9013fddc33d3a26b7ef97f3f0fc570ab9f7ec6a9ae7f
b6b211d313acbadf6bb543079e4dce1cf9537aebe80a044db4e78c8f71671d9c
89ac7ff9b1f3ccbad79fdab1c879444029a0b80bdb6a14eba0d2d8e27b72f642
a2e3e13cdbdd1ea794b8add636a786f0985f2757cd7abd1b138effa7810cacf6
2cf41e8cfd004ad40ea619b83f71aa00260f37bce6e6b0ef468f8866b493bbfe
27051e4200ce1ebf9be4ba364f785201fa49899fdc6624925a1d94f8b07b7599
094c31bf415824958a169a81ec4cc2bb1ad52b3b2db9bac1ad7519e45d3b0c33
8ccfbe4efef1cb7de91199a81dba6cd2e44604bcd936e7f1620c68f6e6dec8fe
528f1893009fce58a4625f8d30ff948b1870a54ea7bc78d258267809a69159b6
a6d043de65317571ebcfbce2430c8e76564eef1e48426d80962584e656ad5ea5
8a11ca8070a700e4aa1080ee0585ac8f408cfbdd73dfc26bfd4111d6b048125e
d07d37995d91f5e265
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
cleartomark
%%EndFont
%%BeginFont: CMSY8
%!PS-AdobeFont-1.1: CMSY8 1.0
%%CreationDate: 1991 Aug 15 07:22:10
% Copyright (C) 1997 American Mathematical Society. All Rights Reserved.
11 dict begin
/FontInfo 7 dict dup begin
/version (1.0) readonly def
/Notice (Copyright (C) 1997 American Mathematical Society. All Rights Reserved) readonly def
/FullName (CMSY8) readonly def
/FamilyName (Computer Modern) readonly def
/Weight (Medium) readonly def
/ItalicAngle -14.035 def
/isFixedPitch false def
end readonly def
/FontName /CMSY8 def
/PaintType 0 def
/FontType 1 def
/FontMatrix [0.001 0 0 0.001 0 0] readonly def
/Encoding 256 array
0 1 255 {1 index exch /.notdef put} for
dup 58 /logicalnot put
readonly def
/FontBBox{-30 -955 1185 779}readonly def
/UniqueID 5000818 def
currentdict end
currentfile eexec
9b9c1569015f2c1d2bf560f4c0d52257bac8ced9b09a275ab231194ecf829352
05826f4e975dcecec72b2cf3a18899ccde1fd935d09d813b096cc6b83cdf4f23
b9a60db41f9976ac333263c908dcefcdbd4c8402ed00a36e7487634d089fd45a
f4a38a56a4412c3b0baffaeb717bf0de9ffb7a8460bf475a6718b0c73c571145
d026957276530530a2fbefc6c8f059084178f5ab59e11b66566ca5ba42b1911a
5d7f1bf343015eece988b7a93bce0c7aa61344d48aed9c92c8698d4b7c9951c8
7d103f2414b39e1437f9d2e50c4ee5f218f2e6716926a79ea978f13b1f855345
191dd7d31d8f82c2e3343c7a5894d95bdc492c28226834efcb5c12fea36ac5cc
430e0aa604961e34888adf6c1f3954cbc2498e225d953cf5685852162346f474
5a2a7087d5d7ad486de16d2ca8e15cee26e012671ba3bdc7d95cc8c98bb774f5
08625e968aee27ff7d1a06e63bcfb5aa4876c3f8f13b30ccccee73c3caf4e70d
98e6ed2f422dbb4950bf789680e064150995941a9f4dd68a575949847a7d012b
b910bf03a7a227d51386469ec9ef415f3bb849d30411890d9dbb7f6f84670fe8
8416f71bdab3874138a93b02a7716b10a7be24518850bf2359abfe10738d29dc
4b1505d2f6fb9f899155f85de8b0e454327c4cacf3e0859686a63352adbd27fe
4ffd3d5df3e167731ee61929c2ab0fe185aa504b05ff647eb08de5f42b316efe
123264e8ce1a3ad3a1fd8d9d17c992d7f0344726b33f565c83aaee447847eb91
7b7495e1adec87bd907995f6026879c3053d77adf7893e2052c8f0fcdd913009
0c3dd7b477904bf957a9a84899dd5a6131c7c2344279ef72b290d6383c8f3178
24e1ccdb7d7011604458e6
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
cleartomark
%%EndFont
%%BeginFont: CMR10
%!PS-AdobeFont-1.1: CMR10 1.00B
%%CreationDate: 1992 Feb 19 19:54:52
% Copyright (C) 1997 American Mathematical Society. All Rights Reserved.
11 dict begin
/FontInfo 7 dict dup begin
/version (1.00B) readonly def
/Notice (Copyright (C) 1997 American Mathematical Society. All Rights Reserved) readonly def
/FullName (CMR10) readonly def
/FamilyName (Computer Modern) readonly def
/Weight (Medium) readonly def
/ItalicAngle 0 def
/isFixedPitch false def
end readonly def
/FontName /CMR10 def
/PaintType 0 def
/FontType 1 def
/FontMatrix [0.001 0 0 0.001 0 0] readonly def
/Encoding 256 array
0 1 255 {1 index exch /.notdef put} for
dup 5 /Pi put
dup 8 /Phi put
dup 61 /equal put
readonly def
/FontBBox{-251 -250 1009 969}readonly def
/UniqueID 5000793 def
currentdict end
currentfile eexec
8053514d28ec28da1630165fab262882d3fca78881823c5537fe6c3dda8ee5b8
97e17cb027f5c73fdbb56b0a7c25fc3512b55fe8f3acfbffcc7f4a382d8299cc
8fd37d3cea49dabdca92847af0560b404ef71134b0f3d99934fc9d0b4e602011
b9cfb856c23f958f3c5a2fbe0ef8587d1f5774879c324e51fcb22888b74f2415
50d7401eb990d4f3a7af635198422283cac1b6cd446ddbcbd915db9bff88844e
784c6bf7389803d9450b0c21756a017306457c7e62c1d269f306bd3402e266de
fc3b5e7d8a8d2f5bf0fe6ddd40d07391df4fad4a6018dce29a2b8f692b29f202
3a7c0e66de8ed85c14f1f8492167357f51a7e84cc5d92e0fee4d81cf7fbc8de5
2d2e7bb57142033993f9c08c315abade8dbc4a732e84e142d3bee51557910e12
cd8aa37c459a5e6b7f5269f59078aba3be4641a11ac48d0b625c8325b38ec08e
4c9e5e7fed976a5650d99d82114f449b9ca14c4ec957702295a39a93ef93f618
99b8ea06b092c3c1e503e6e436e0a9fa22576c8930ab3dc8c20f5d82b69cddf8
ff4dacfa9c54bed5a3aa3ea5b129fe96be632843b9b6bc91b615581a985db56b
1e01ca60ee69ca92cf5c0882ece62edad3e106d835348822400f0b66af658f2a
e56ed08f8b0010571807009b73ab12a8cf14ca6c71f03c2a48c500f9d62266af
154a6375ff600d9bac3f05ce34142d6867a79581c533176bb2f3117336671e2e
44638a97167e2ea9644e31ea16c2ad2990ea33c54001e0c8156e6de8ab6a4d40
a7137ba275f39589fea2e2db8256adc103d6f9cc038037a47e8fd469c5f98a5e
3c15bd4ace40d340018b1cff7d1ed8abb0ac57b5b5a2c20a51957b96c453edb7
dae5affd91a46d938fe0a13363001d844ded4323f1ee6d30012aea19b024a552
315505535c85dc26bad31e09c50e6512802976d298c4e90d0044c362e6bf3ab3
62a454ee93de25ce54411090c29e9d75c80ce26a84404bd9de3aee0e3f921ac5
87f907572b8354a5c3165eea7e8b2ba4e4f834663063e9a307d8ff6f8b61acd8
799bc105cddcf8f95f2160494fc01f7ec3effb95de571b8d7f27a2f9ad203c09
cd4cffd98a119a507460e7fef5c910405e877aa1f8da68d1272e59e3adccef8d
82e692b3229926fbe621080b7831a2ee248948dd3ae55082a939f02875a7a0eb
7ae7d50270a576fbdfde7109c670f51be75b80b6fe3045ea50e2121022b473d0
d3fea17e9d1a4bbf6c305043243b45392b6235029f5b43a5a2eb1bdd1028b383
bd30fd563602daecd2904708559b0121700b751adc27f868f6d1aa7228789bd1
2766d0d120de4827922d175ea200550aa6169093cd7d0a3301a23bcbf802a762
df99cc7eac2cda1e1279f4ce30ac5250715d1126d5ea31972bdcc61423d69cf5
cb2e9f26b30215e5e894b75b7a3a3b1112b539298f5a3a0cf2d24886c94269a6
23e5c0b7a9433a7829ef51f89ef4810da9cc3ed7c0097449721ee95f5e96535f
562d769886f55e61cb03688d72223e7fe2c4a6cbdda42f5c8a6854ffd6a6b32f
77cd719b7e3538aeaad6c3e45508849a665eadb591ec0ada1d7903e8ad608f87
98778535ca3c0c2673b9135b5c1c0cf19ca455e95eda6ae504c5bf786eb45c2f
a6e47e2288515d52d1a8ee6b3582ab4b89ef390222bf7d68aac95a63f09a08d2
4e35a7ad0df64f96b4aa2a856256e5dd50543e0d5809cdfe1bcbdcb7c88e6984
6f81f72614391f295b213e516c3b45431651ecf66b9252a26ab6a3618e811214
c9ac7c7db9701ef2e067e1972bbfd6b7d83c51801b9a6d0600891e9bda40bf16
e08d727289fe918138da7fa061f853bcb1be05ee4426c61bec614e780266a306
6f7e0a160b23b3c498281ec949b4bd3d68e1d952b697ac777d2a83b7e8123782
d174968c2409cec25e5b7981c2ac87140873c24f792eb576325b23250cadf61f
3a3f9256a43eaaa9aedc27ba10ea97b55d728bafc72523f65c56165eaf9f07fb
a7e7dfaa1f569361c1308341e1f175eadeebfd9f96adbdb585fa072e6b4b89ca
705618f9597107231e794e4430550629dac97ee9317c74c22c11f7ecd11aeee7
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
cleartomark
%%EndFont
%%BeginFont: CMR5
%!PS-AdobeFont-1.1: CMR5 1.00B
%%CreationDate: 1992 Feb 19 19:55:02
% Copyright (C) 1997 American Mathematical Society. All Rights Reserved.
11 dict begin
/FontInfo 7 dict dup begin
/version (1.00B) readonly def
/Notice (Copyright (C) 1997 American Mathematical Society. All Rights Reserved) readonly def
/FullName (CMR5) readonly def
/FamilyName (Computer Modern) readonly def
/Weight (Medium) readonly def
/ItalicAngle 0 def
/isFixedPitch false def
end readonly def
/FontName /CMR5 def
/PaintType 0 def
/FontType 1 def
/FontMatrix [0.001 0 0 0.001 0 0] readonly def
/Encoding 256 array
0 1 255 {1 index exch /.notdef put} for
dup 1 /Delta put
readonly def
/FontBBox{-341 -250 1304 965}readonly def
/UniqueID 5000788 def
currentdict end
currentfile eexec
8053514d28ec28da1630165fab262882d3fca78881823c5537fe6c3dda8ee5b8
97e17cb027f5c73fdbb56b0a7c25fc3512b55fe8f3acfbffcc7f4a382d8299cc
8fd37d3cea49dabdca92847af0560b404ef71134b0f3d99934fc9d0b4e602011
b9cfb856c23f958f3c5a2fbe0ef8587d1f5774879c324e51fcb22888b74f2415
50d7401eb990d4f3a7af635198422283cac1b6cd446ddbcbd915db9bff88844e
784c6bf7389803d9450b0c21756a017306457c7e62c1d269f306bd3402e266de
fc3b5e7d8a8d2f5bf0fe6ddd40d07391df4fad4a6018dce29a2b8f692b29f202
3a7c0e66de8ed85c14f1f8492167357f51a7e84cc5d92e0fee4a71813d2ffb26
445026f89b4787516ecd1afc78f8bd19e91e9ccc9402e8c36d2449c1ff850a8a
f61165aac3fe931332dd28e261b91b05edd18f44ea7d58a8f35fe88493b64aad
6bfac3a0136215fc2f4ca8e91d70c5010e6f4013e6d63b44f6fb00afdbd7cdb4
5ec5b1d9736f45cefc8a0124b815987cebd81bbe0d44dedb2d5ef37923b3d551
abb6a1cefca7868fc7bf3814ef7d7b6b1ae6e869cb77aa29e3d90b12b0dc3ff6
ec945922b5899bbf2f12e92731486d2ef1230c528bf8d7e0ae09ad7632a38966
5963de49d1ef3d65bc483e4a577b927c940f5e121169ba52f6576c85793e5fd7
7f5863c488e55bdefd5d8b2514795533aabbc12e7f51816c7e1484f1c441aa9a
66a5dc77158e79cd6692d299b95e8058b35e771a6972d2b5eb1cd6d2bb8e835d
361a6eac0c90c906aea1cd75c4412a1339dc1439f93e59917311bf20af4f2bc8
bba5a4626f75f28a47d4595c37f4019df480d9385975159142618e22e964f019
d88125210e2ef21d65baf500adf802297b24eebbf4e93c617a613f856bd0d45f
e17a9480980ef83950bdb8ebf208c895ebc4a7132f0765b7c19a332ebbf8a3c9
ab65063a42e19ca9d43dec3de7aba46b9a5d24fb93d615c0a1726ab7e31c378e
ab77150858535b91362ab0e2b968dee1c539964126d937f9d4980ccefa92bc81
b054996a65a13995c9c9d819ff05511cfc89cbfe67447c940405001d61be633b
b771eff383fc6977ec06af30f981504260de7b9ec97359974734f495ac073935
fb30e3700679092ef5d971b6b2da0e15960f2391fa6b63c33e7f56b4a9b86951
1d3686a5e8e613a69a0add8b8c73b127ddcd397a48d785079e786d24b31bb502
0850037529377f7d1ed88ee66c914ca096a2b67bf402a2cf5cfbb44ff8c84c09
8fc6e1dbf42f16a855ebf9e4f158bf206fa717b693663fadcdf49dc29d3e430b
1b266d08172d13837a9248e7da44b9f6cc4ef0871ebc090728d88951ac4a8e23
b90b7651cf9a6660c771ec3b8f19a81cf375e5a8c6d79166254fd4ae85eeb28e
f4c3ca0c006abf646d4b088aeb02e6a2cad1fcd44717a6712bac6c14db6fea67
8b70cb994e69d3e34bf3205dc88aeff446edb9a993b196dc2b4ddefee82c480a
0080c9acfb1e70fae37006d10306afa8c1e2b6ac64fea43bb7cd45b289aac6df
d9b6104c7a09831cc0b9f5707e7b41991b358ede8d4f88b73c81a87ff69e04d3
357da19262bf
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
cleartomark
%%EndFont
%%BeginFont: CMBX10
%!PS-AdobeFont-1.1: CMBX10 1.00B
%%CreationDate: 1992 Feb 19 19:54:06
% Copyright (C) 1997 American Mathematical Society. All Rights Reserved.
11 dict begin
/FontInfo 7 dict dup begin
/version (1.00B) readonly def
/Notice (Copyright (C) 1997 American Mathematical Society. All Rights Reserved) readonly def
/FullName (CMBX10) readonly def
/FamilyName (Computer Modern) readonly def
/Weight (Bold) readonly def
/ItalicAngle 0 def
/isFixedPitch false def
end readonly def
/FontName /CMBX10 def
/PaintType 0 def
/FontType 1 def
/FontMatrix [0.001 0 0 0.001 0 0] readonly def
/Encoding 256 array
0 1 255 {1 index exch /.notdef put} for
dup 61 /equal put
readonly def
/FontBBox{-301 -250 1164 946}readonly def
/UniqueID 5000768 def
currentdict end
currentfile eexec
8053514d28ec28da1630165fab262882d3fca78881823c5537fe6c3dda8ee5b8
97e17cb027f5c73fdbb56b0a7c25fc3512b55fe8f3acfbffcc7f4a382d8299cc
8fd37d3cea49dabdca92847af0560b404ef71134b0f3d99934fc9d0b4e602011
b9cfb856c23f958f3c5a2fbe0ef8587d1f5774879c324e51fcb22888b74f2415
50d7401eb990d4f3a7af635198422283cac1b6cd446ddbcbd915db9bff88844e
784c6bf7389803d9450b0c21756a017306462c563d51ece66fcc9c831843ecae
1fefc1a232e2724f7baee428ae03aadb95c3035345c15e9922fe49e1f2cfc980
237316572dbc57064edac9b0db8913a5e2d45e97e19a91435ccf8adfc835b585
48e74b291446d689c7f2f8c4325e8356e974ae30c3e2977477baeaa33d141fb7
80f59351e84bfc88c87b3a4a1d25e168b9d134554f6a581378c7d2d6eca8ac09
045cc3a5e0ed86f147133f094029e3483bebc81cfde69942cf645ea20d0a2b64
5140ccc2f9cb4a3d969f4b0a79cd3329b440dfcff5285494406f3dd08d804c86
df191e57232f6f1f83df6430f214e03fa5412b1e13d83c60c52a698bc9a38159
19a64162af7b83a9468fae9507c6cb55ea80df8c696dfbc3296c663902d77e89
a181502627281181ac8624f65be9de5fb32f056cc7dd7cbc7366a91717b5892a
34ef6b441871c6993da3a81afc9bf70ff3842a21a29c0e49da1ccba37dd6b920
2702db510b8b1109acf4c27ee8d676bdbd16abe189f34a9b61532eb777457698
cee0561838eaab2d3939c5093afbb215bac433d1918c739b62566906bb2187f3
378521fb52e70c18886e1aa15f53a1f8a169528cf2ddd54c203613ff88e619f2
6c9c50c2c3b8b8c868a88afab1dc8472e7b6f3f992a161723a3c0904865a7c42
3281601eee91f35222c4a71f343739f102eb43145a47e4fac3bd666e4c114a90
5950618ecb1bdc29f90f6ebed1d8325fe6b52e14a8870e9b4bb088e585c71b91
493c12845a101937e3473ac5e9ae24f7c358f7d9e8e9b20ec9e6ce4429b55ae8
aa69952af43d57f7451969ccac33dafe647bbc3ea5e0682fbfb59a389ae2391e
4609fd282e9a80eff3e96c2127cf5db56c6e9ea66aefdbe92e688671555403b8
10033d58cc39146c1a8508b3d5edfa25f24d78b1419264f16ae7aa81d8a8fcb5
e12e301e15ff1254590f50b94eb38efe5ce0e77ab149905b11ba173ce62e6fa0
30f62e730d0f438b571a026814cb7b91e12f4f9471c3ded0188a660d995da909
c6da23895076901dc6f1252df8c4c08657e835dc2f40eb6cee2da576017803f2
e3da299a1fe54e30023dd44d6133562f44e6ffd70cbb5ab3d430ecb5ea7c959b
909324635638daf49e18f9f3c2ea3c10442c64e6928fb74e3cdabf29ae502938
87eb119f15549e0a39b234a42a1c3a5e9220d098e9777eaf381dbd4bcbacdf0e
dcff5dbcbb38161d6e5b2775653303ac55a6924ac20fa4958e13e9fd5d70f854
e5c4ffa3a5769148de1520592a2adc54dfef33ab1d5a03c7e81a1e09afc0ae9d
7d3dce4bf0199d4c3c20ecf6330fb0cd390e08a88d73cbe6d4f468b8b64d2315
2fa3f94946
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
cleartomark
%%EndFont
%%BeginFont: CMBSY10
%!PS-AdobeFont-1.1: CMBSY10 1.00
%%CreationDate: 1992 Jul 23 21:21:18
% Copyright (C) 1997 American Mathematical Society. All Rights Reserved.
11 dict begin
/FontInfo 7 dict dup begin
/version (1.00) readonly def
/Notice (Copyright (C) 1997 American Mathematical Society. All Rights Reserved) readonly def
/FullName (CMBSY10) readonly def
/FamilyName (Computer Modern) readonly def
/Weight (Bold) readonly def
/ItalicAngle -14.035 def
/isFixedPitch false def
end readonly def
/FontName /CMBSY10 def
/PaintType 0 def
/FontType 1 def
/FontMatrix [0.001 0 0 0.001 0 0] readonly def
/Encoding 256 array
0 1 255 {1 index exch /.notdef put} for
dup 56 /universal put
dup 57 /existential put
dup 96 /turnstileleft put
dup 106 /bar put
readonly def
/FontBBox{-27 -940 1332 825}readonly def
/UniqueID 5000762 def
currentdict end
currentfile eexec
80347982ab3942d930e069a70d0d48311d7190fa2d133a583138f76695558e7a
e9348d37cac6651806d08527c1bb4a062a4835ac37784cc39ad8841404e438b4
d52d3901e47a1de4f7924e0fb3daf442499175bab1226edf692a4956739f8828
e80592f450c5d5c22ac88bcfbe9748f61d18243a16f4a4467f084e8e2be46ef4
7fc51c3a8199e3cda62ff9c4fb73956dab8b6683d2156377808cb35026073e80
523f59a30d195fcf9b9fce4ffafc691c7bbdc230332e4e15db130d783c5d60b3
4fa0c677b6fc914a4213ae7799999a2d0021fd62c387d3bb675576611b2ec495
a9caa4ef4a1bf07cf81eafedfce403b646248cf8361b876f5c8d87de5fcc236f
2b2f12c78a15541fa8126c733d02cf50fe3dfb4fa7697d214dac2976bf91bc19
25c44f6936d68343d88dd537315a255cb7fc437bac2edb80f1fedfb4969ccde2
833a78ed57203109de46d94ee67e9d14d007992d2b9eabe7849bfbd36d1dd5de
5610f8e81efba96bffe4771de37e4b90ab0fa5d00300e3061eaf81cfea33be39
4d62e8f0c0aa19ebe3828f6fde9e61b73c470cef9b4d7a6787b150ff08f15a83
ed6b0acf36782e41acca43713187dd752c77547e2528d18dc4134fa3be0437e0
410f753832c5a527637c0036f79decaa84d1336c08eb69278ec4cc6521f89d17
554615b1b9116bfd0206cf7a1df3f28001205ae025f815296036c964a2021b70
f0337f2f2a90c1470b16ed8e150bfc7e005bd2ea03ad6bfe9d6b5a3c65b14e6c
be22923c1eb4580708cfef29efdf90e536a526e574800e33e8da7df629c95160
7d35f46dee446052fe9d16b548e706ed1cd2134dacf1de546eb986db5dcb2720
3cdb731c7cd3dcdb09fc306c72e30b6ac4ba92e01172b6b7c3ab05eefc76f18b
88634a00cda21f9aa8b49697f29a3a933ecf906ecbbc18dd666400ba4a5cee1f
93a7c2b839d974432d0870b95bae5aab09bfdbdc34239645738efa9614940fde
e7a133e719de5158aebf878bfd7fbb18ab3ed796980110cc963a15e698f86115
9d6bacf7eaa215c7fe350c691b0197e44771431566e5cea887ffc56f020cfc7a
0e65beec65e69680575f81eaa9650a9c6b3afe7dfd807eb036cb2ed43f20fa78
0b0461d49b390febb576278c2d035db9241f2bc72af8bbd9bc2fb50feb5528e2
db1bec31c35b4ec55650dd3a52e6762f69aa5bf59af7e1fe94beaf457a4eabde
02b8a2e15bce0bcc8ecc6b98eb661458b1918bcaddab085699260195cf9abc2a
29beaa5bbfccf4d87cf98fcb085450c62401f94957f0e57a36a6d7ecf803ae8d
1718232634195160de87543dbe0f3937781b9573be3941b63b850bb1bf8256a2
4e09a9e72c9d2779b77b11c68410a57f58f58a406a48cc96313e7a8bdbc4ad76
6d9415f1cb536b474d969c21010346e47a32a59ed9866e4d784464556514fb7d
b2968201de08caa464fd4aea49e1f621670a12673de9920ea23bd3a2ea4f189d
0fdaefe5e16915748f21f4910c273cd8201d8601a1456241b22d7e510b7332a9
f936d6a1c21f614cef8930ab4d06ec535c74080c418e343ee2a237958a9ac4ed
0708b223eeae1950d246ea56634be01c6ef4adb9241fb309f61eb08546077df4
cd55a64d931af1ece352e61a1af01c5bf7c2bed4441aef17cde3e1640c26846f
baed384621256b01a0ffb1db652400179add9e8d063561256b89708a2e10aba7
b7ddc1a84f94d999e9895a7b9cc5c80319086fec1385b2d553fb7e0c40a52d14
0c7de748ed3a0f2c8eb2a968c40a8272ac92d693d287b1d96d6a899f37bd38fe
6d11f8d0533ad0bbc3dc03f0cb6a133bd6222b232185f0480017bd4de922b88c
7e6b1277fa2a933e56a3cc07aabe952155bf5ef18e5c88da3544ff78f4a43439
c194de1b6878e5f64ffb468822c678ad0c3baa01b038a2867aac502fbba17f8b
02500ffb373afc2b1f
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
cleartomark
%%EndFont
%%BeginFont: CMTT8
%!PS-AdobeFont-1.1: CMTT8 1.0
%%CreationDate: 1991 Aug 20 16:46:05
% Copyright (C) 1997 American Mathematical Society. All Rights Reserved.
11 dict begin
/FontInfo 7 dict dup begin
/version (1.0) readonly def
/Notice (Copyright (C) 1997 American Mathematical Society. All Rights Reserved) readonly def
/FullName (CMTT8) readonly def
/FamilyName (Computer Modern) readonly def
/Weight (Medium) readonly def
/ItalicAngle 0 def
/isFixedPitch true def
end readonly def
/FontName /CMTT8 def
/PaintType 0 def
/FontType 1 def
/FontMatrix [0.001 0 0 0.001 0 0] readonly def
/Encoding 256 array
0 1 255 {1 index exch /.notdef put} for
dup 48 /zero put
dup 49 /one put
dup 50 /two put
dup 51 /three put
dup 80 /P put
dup 102 /f put
dup 103 /g put
dup 105 /i put
dup 107 /k put
dup 110 /n put
readonly def
/FontBBox{-5 -232 545 699}readonly def
/UniqueID 5000830 def
currentdict end
currentfile eexec
9b9c1569015f2c1d2bf560f4c0d52257bacdd6500abda5ed9835f6a016cfc8f0
0b6c052ed76a87856b50f4d80dfaeb508c97f8281f3f88b17e4d3b90c0f65ec3
79791aacdc162a66cbbc5be2f53aad8de72dd113b55a022fbfee658cb95f5bb3
2ba0357b5e050fddf264a07470bef1c52119b6fbd5c77ebed964ac5a2bbec9d8
b3e48ae5bb003a63d545774b922b9d5ff6b0066ece43645a131879b032137d6d
823385fe55f3402d557fd3b4486be533de8dbe3ccd493ef4c9656d5d5b76d531
9e704539dd76b065f45e6d6f62ec499c9ab91923a364237ef75e1d62d52df3a9
43713cbc63b16c1880feedd1633766248fed9d060ff709951f2ec84ecdc06bbd
9cc4a865e1f275455525e5ac7e2e6289615e98cf7ce3763b6914d3a4c5b75b29
b8043dbd898ccd5be448064cf1af2f80f969a44b4f9b801c42f6d6a6d0c3ff42
e0b1cff748c1fc49b598eadde0c2802dd591c54b802ffd24cb7a7639295713d5
4e639514ac78460672c9c51742ae2014e4137ba4303051c06f686395aaef86c9
9d7f9a97009436c2ff55b770de3e80cef0d53f4df46aacecc21632c0c676e2f5
ca7bb101a239a0ff67ebd37a6b8c4c8246dc2c90b759dc03fb26bde8f134f552
23ef3d6496aa0c4a2d7b6398de6e6a0474ee1b0d78b2d865614609f1db92fc56
4ab5921078b4944e11a2162902f0e04f4b29448aaa22b4ea92fac48f8dc47535
d717dc7acd08b25d391c97c6c540ae0a98be5d6a8da564ab73e8b5d3b5e1989d
6e25c3a35ea44d596b5fd6b2373b30de7d59c1831245edb76d6a67816ab91a80
a27a6597c6dfd274db8b3e45cb01aedee59ba6efa1428e41ed557f051012a389
9b195ea44a4e4d0067398d9d40ea26195efbffd2cf785540bbeb8964f6391361
904fa5e187e4af3baeb4e8cbe7558fb7049c94a1769a2ff0b44f679bf6f14d8a
974bb8bdc735d5a9798c89d7d81176ba98dc22dddf6766acd52020e3ddcbc94b
71ad8a336dbe9262f302d8e8d5ced4481b19a586e1d73d0138ab0b732226185e
8cfb8408890ecb590f032a5633352c42df62a7dd1a3cb4fb12083709edc26146
f31161bae67a54aa5b41ca7af61b515c100b38a01b77f831245a013f804584b7
bb764dab019978bf8edeeb17bc57930c37f4b1e9d770cb1162fb3f1628dfc9f1
31690d1ad193a3bc10f6172418f4e77096e34682a6d0201d291b1d6dc1b20bd5
446e2f6644a228afc3d3229b0beedcdcdc6b1d51322d1dd80a1f7d0e014f13f3
4905de263819c895b6ffdfd1810d997bf449d72fdaf53e42ae884b459222fcb1
47de80aaa4932db234dc648cceb5582c0541cee4354536c14ef4fe242d4d0311
accf6f03b8a6641cc1bce8477990495024f30c953b421ee5c66a643838867a0b
7fd7ef168595b570422eeba0d70e614a2abe79348c7b7db49d99838f617c128c
872644e094bb124260a45438d23764b6a8fdbe76e8ff3fd8336da4e04f57a115
e53b213b203b6a0438a094381ac3ba062ed1020eb26730d143c349120a644584
1e049040afe662e16392d2bed5aa34d8e60290b835975e73c77f373daf0e9427
dd3ae8cf53fbc42db6bf9f9e5dec1c4dd80d528a230772938b839587e894d7fd
fd5979c06c87a1e5b4c2ade4fb806b216b65113923bd5967be2b04bc2c64e195
bfe83d00c6977b21cb2e20ffc9266e15acf9ba7164e6e8eec3170003ae201c5b
99b59f1056ef2f1d0a722e80dbeb41eae7687222ca1eeb4a349eef8c9c3ec6bd
8581dfa76f4532e97f590af884f2b855266f572bf644063a7cfc8cc773ef2d5e
507519e06cd7d0fb450f9f4d1fff6d53f39b2f3f2d0cb60575fec98095eda074
ec4cfff554d12226918e25cb53f6581a55693751a411447632b172939c81ccc7
3c77eb2a185df572898afb508214dff6dc8c259b1d3213b4e4d36f45bc3bf6cb
07a0b40e60b7c41857817d79470f27fc5e01165f849932fae5249d1191ccae48
4aed537866e84cf0dd95be80fefcbd1e394bf9d8d27cb7d910bd43a4f080bbcb
12f789c9d87dd62c6d68f5e67b26d738aa00835452203a3e05c5ee8c257ab689
3ba6998817076457840f2b7c195426c0cddf7fe8a7c90b21ba729043ad5aaf49
8c56bcdb9bd5b0869075f5096d71a64324342e69d8040e5fb0cf9153a700aa2c
249f6d5d2f5b77309c7f7f265646448b173aa49d733d82a97eb5cb0003fbc857
05df5818ba4042ddaa0cb2d6be2957882b6e0b0e100564caf9de1431e1d0ae15
adefd457565482f7f6a3a30e44efda7500dfa66295a7ca117902beebea8f2ff3
3584d2b4f6c327201e6d1f1f22866c7bf0a5bd11d8b7d747f84e63586537033d
c7fa68d51b5a3e0a2ff169b6d234864a987d6b7d2a9f2612be598d4b7e145247
be9a30c4db62cd00bf6edb714fde90d1ce7a106e54a5c7b5a985a35d89764c65
87e3208c47367ad150e64953dab1369fbb848a2d4e2fa97d241c4edb8217ff35
9692b8e42d34306eaa45ef4f90a672f1358e202eaaae9ebf5e5636fb3fcbed22
149624f6ca95a96c6155d6100ecd9bfcace4a3f1b2a9ea2e6d3831e8bc47bbee
9659dfaf24e9e5d8ff3fe9062ebb5718c3e482dbe18dbeef92b21b2c84a12227
3b012ec9f4afa4f2a81ab6f349a2a288fb5b52bb28e15346b4e315ac3abd45e1
a0fb92f9b8dcb0e12eaf0cdfebe318f36d47ebfbb6c7eaadc66ce9db243a67d3
f22065f831851f81488cbdc82a3e8de6469d42e9d2dfbde18ddf7d93aaac50c7
957e3be6dcab0a7b01fbd0f9c3cbfa6907d9697f74878dd8a1591bcc4a354882
c607898e2d49470a31ba5f9c83a79d6398d0fb4eec4d4214a8d8a86350d29d80
e25067e3b613d2111c5716fbc09a3bc39b7b67c3aa780cee28e5166c69501dfc
dfb0016c09ea69d97e69edd099a09d00975bad510554661f5bec3e2d6576d08a
365d8ed80f3281ac2fe7370ec70a9176879eb89ef74d57bb5ed8e39dce2bd417
2b788f7cb83be09bdd7231facfeac5f0f279d70e04bf659287e5866dd1a04227
393de3f6a950d764900a5eb0e5df8aca84ba88e99559536a02543fb0861b568b
36a394b39cf15247bed86ca8d2267a686202976b6fb3c9917072a755b68de374
3068ab171d050e09ffcdf232cbe633ade6a1f64521a87efa520d0cabc5331731
f56dbec52f8b3c054d149f1a3891808f936957d9e6bf43ece0428ebbf11f642e
8ec4dce87534a857b4597c94f15de43a4a8bc20d67be2485c7f362d95fcb6212
35ca83c0ed283787c7ec0be9f5439ad71ccfe67c807e7f0d3d5d841d84ddec06
3f2fc9e48f96f85540a80f5027de5bb53382d62bddd8f9d4f62076ea4e579016
31d9a3bc8e7c01e711be44011b5736d86bd7896c29d1e718eff432ab9c9b6685
7b03fc89802247aea3cc6c883b3b047f16916ad121117bb5b89b2647fb9ebee5
5083fb01b99b824aecd5a0a9ee8cd50099d44b43318a99a047f0489463ef6d63
047ac47f31c197d765604d6a6d6ef631c93820a9afa83d2cfd3be01f9d2a1b63
5ff156b28e6aab3f100826ae0140b538a0b3
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
cleartomark
%%EndFont
%%BeginFont: CMSY10
%!PS-AdobeFont-1.1: CMSY10 1.0
%%CreationDate: 1991 Aug 15 07:20:57
% Copyright (C) 1997 American Mathematical Society. All Rights Reserved.
11 dict begin
/FontInfo 7 dict dup begin
/version (1.0) readonly def
/Notice (Copyright (C) 1997 American Mathematical Society. All Rights Reserved) readonly def
/FullName (CMSY10) readonly def
/FamilyName (Computer Modern) readonly def
/Weight (Medium) readonly def
/ItalicAngle -14.035 def
/isFixedPitch false def
end readonly def
/FontName /CMSY10 def
/PaintType 0 def
/FontType 1 def
/FontMatrix [0.001 0 0 0.001 0 0] readonly def
/Encoding 256 array
0 1 255 {1 index exch /.notdef put} for
dup 17 /equivalence put
dup 21 /greaterequal put
dup 41 /arrowdblright put
dup 50 /element put
dup 94 /logicaland put
dup 95 /logicalor put
readonly def
/FontBBox{-29 -960 1116 775}readonly def
/UniqueID 5000820 def
currentdict end
currentfile eexec
9b9c1569015f2c1d2bf560f4c0d52257bac8ced9b09a275ab231194ecf829352
05826f4e975dcecec72b2cf3a18899ccde1fd935d09d813b096cc6b83cdf4f23
b9a60db41f9976ac333263c908dcefcdbd4c8402ed00a36e7487634d089fd45a
f4a38a56a4412c3b0baffaeb717bf0de9ffb7a8460bf475a6718b0c73c571145
d026957276530530a2fbefc6c8f67052788e6703bb5ee49533870bca1f113ad8
3750d597b842d8d96c423ba1273ddd32f3a54a912a443fcd44f7c3a6fe3956b0
aa1e784aaec6fce08dae0c76da9d0a3eba57b98a6233d9e9f0c3f00fcc6b2c6a
9ba23af389e6dfff4efec3de05d6276c6be417703ce508377f25960ef4ed83b4
9b01b873f3a639ce00f356229b6477a081933fef3bb80e2b9dffa7f75567b1fa
4d739b772f8d674e567534c6c5bbf1cf615372be20b18472f7aa58be8c216dbd
df81cc0a86b6d8318ca68fe22c8af13b54d7576fe4ca5a7af9005ea5cc4edb79
c0ab668e4fec4b7f5a9eb5f0e4c088cd818ecc4feb4b40ec8bd2981bf2336074
b64c43046fe6e8a202c241f339425066bbc9f56c37232c6210cf7904a0503c50
4027a8b09757f77fcadee6c45ba649b9adbb873ad9bbefb3f1cd94b5ee8eaf68
9c49d1d2cf03321f6a59fad140085590083e97fe493ea75681ccb3c1f52a8c85
9e9bdcf12ab1121511676adca513069ece719f99ed8cb583a0b2072464fee23e
a96511c74900e44c1bba4dff1a60072a6f6e3901480d6b554b8128f00cec14f7
b51ab8a27c368a022565f54b2dbb3f3ed0ddfc47225f6dbbbcd27483e2fd7126
3a728648b22728f7ef9c1bb863ebc7f069da04c6a7d26fe37fe0bceb1346c391
4040de167b35f29e72a5675938a5a4e4b3efdebb1a183ffebb6578a94642e8d5
0d84abc350e234c6ea432dac9bf9daca52279b38b49571943eae50bade15879d
e8b2eac7969be429343e5f42110c2f08dbf1aa86327ff26d3c2b766bf5b3d6bf
93e2473f2a2cda207291bc24d5a3fc7d89c1501c46c15a4a610703bf324e1b4f
89afb22706335b2f32fc8d7c5a0dfd6cb911257c90acf6875aa15d91905cf672
32ec40e163a79af232d19b4130bbe10edb953553e451abd19cd01804ed4bd0b7
4bce816ba28ccda864ee6ce96f1cf9f76f7f18cc3951e15614bf680e74980d7b
d077389cefedd6e14cca8e7ce05ca59c8147b716f4e9f4e20e1685593335c25a
5660a2d23b7138d41b23954c96d9899198e495a0fd10f890d3c0c76ed2b2d202
ad1e77c977fef06cf6173cdded120eea05fe38d414b1fbe5cb01d685b7895cd9
ceca509b255587948dd502b7f1d3a9b2b06942d5773cc2c253083c1f07ce6f67
14bd0d8d6c7047d11b45732ff7f543ed5399766dc367ea79033af318fc2656e9
9f914a2485d0a623513e964a6cce42bf532509ea91ab31cbd22f62d58df2d8d4
2f9f11fe2c942aa1af8bed899d3f8fa07f4b2f43bddde7d6b15d9431313b2e69
1047e8d67dff71bd92b3b79cffce13e4f004fdeb4440e80edf299ad4246c2976
2808024c202d91a669e2203e1911ee6a8a09087d6f7ea9869684b07bf181e9d9
75bfd3c86caca058e2122b0a5bc318c2a1d05d7f5a43892776f7ffa98b8c2242
bff854d35c4b63f11c3e7c52c12a2fd5d63d8a8448fe72c66ca9ab6c700f033b
a65597d561c27c596b28a9fcd97ae79a2114f826855e219b6c7e72d2b835e9c0
9140bd60cc4b20e83b2462b1d5746b2deed62cdd78a4f485a6ecf036dc43634c
7b7afbc0a71f09c68797313631f4d20cf511a18b9fb9326d7caad35b4057edac
3dbd4f6f2a76374522157860f5ddb4e9276b1a2b521e1415504f82ef24ff389b
766fbe437fa4932e362512660d2e6e784ee82559cebbbe94ba943bf63ac1e806
6388715e26f7852cb7dc3ff2a7f62b4774c0727e91ce6a06b4eb7a97d1c94d43
8f0b419693556a93b615c927debe95296b
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
cleartomark
%%EndFont
%%BeginFont: CMSY7
%!PS-AdobeFont-1.1: CMSY7 1.0
%%CreationDate: 1991 Aug 15 07:21:52
% Copyright (C) 1997 American Mathematical Society. All Rights Reserved.
11 dict begin
/FontInfo 7 dict dup begin
/version (1.0) readonly def
/Notice (Copyright (C) 1997 American Mathematical Society. All Rights Reserved) readonly def
/FullName (CMSY7) readonly def
/FamilyName (Computer Modern) readonly def
/Weight (Medium) readonly def
/ItalicAngle -14.035 def
/isFixedPitch false def
end readonly def
/FontName /CMSY7 def
/PaintType 0 def
/FontType 1 def
/FontMatrix [0.001 0 0 0.001 0 0] readonly def
/Encoding 256 array
0 1 255 {1 index exch /.notdef put} for
dup 48 /prime put
readonly def
/FontBBox{-15 -951 1252 782}readonly def
/UniqueID 5000817 def
currentdict end
currentfile eexec
9b9c1569015f2c1d2bf560f4c0d52257bac8ced9b09a275ab231194ecf829352
05826f4e975dcecec72b2cf3a18899ccde1fd935d09d813b096cc6b83cdf4f23
b9a60db41f9976ac333263c908dcefcdbd4c8402ed00a36e7487634d089fd45a
f4a38a56a4412c3b0baffaeb717bf0de9ffb7a8460bf475a6718b0c73c571145
d026957276530530a2fbefc6c8f73e9b697ddc0351763500e23c4d170ea8a2d2
75ad0b6b23097f02fa803c1f46f9ac10fe0e527c431b11b1b9a50e874896cca6
17fe3e255960846bc319ca68b9b930a45d5d0fc36b352c3443ab6f7793b38d2c
7fb9c409ab7980ead55e9f8f6b83c70088d1fa6d7f2214da8928e40b96334ad2
72d1b5db9d1355a579b26a8dac21f021e393d7d837a95deb8de92ed818a8b80b
98ee9cdd8a3c57ad7d6eb7a82f43eaa6ec520eefa7302e750edc4b495f70bba2
24a2182eec37f1a1c5dc8e20973007150237daa6bf03d498826777eeebe09014
ebfe05a8731e1a421cfc513d47d673e3d94d805f5d0668ffa265e0962cb5a75a
4a93d9b872c2d3ac4391eedd46c6cae184e1af981f95ce213181b697819ba31f
f3e3ed201f4914426e805de77334e00eed5adea5f5d61825725d49fa68a47dff
c7dff4d05cf6f360d8527294e94f599911c9b1c6ee95a83babcb7b57d31308bf
2640919d126b479a8eea2b7131aaf0903d6b3f9519ece17464f3d605fee01d6e
3e58fc4c89f6b777941084ca85af30f25e654413f4375bc8cb6a1a646f67e625
fc908b99cc334b2fdce43d5fb1cfc6818380ec001b2cd1512737559d840e7314
38f466bcd2a38f39407a24126b5740c84b061f1e16f5e2a86e4861655d1ce449
244d642b6101c0b80b742dcae02855
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
cleartomark
%%EndFont
%%BeginFont: CMTT10
%!PS-AdobeFont-1.1: CMTT10 1.00B
%%CreationDate: 1992 Apr 26 10:42:42
% Copyright (C) 1997 American Mathematical Society. All Rights Reserved.
11 dict begin
/FontInfo 7 dict dup begin
/version (1.00B) readonly def
/Notice (Copyright (C) 1997 American Mathematical Society. All Rights Reserved) readonly def
/FullName (CMTT10) readonly def
/FamilyName (Computer Modern) readonly def
/Weight (Medium) readonly def
/ItalicAngle 0 def
/isFixedPitch true def
end readonly def
/FontName /CMTT10 def
/PaintType 0 def
/FontType 1 def
/FontMatrix [0.001 0 0 0.001 0 0] readonly def
/Encoding 256 array
0 1 255 {1 index exch /.notdef put} for
dup 34 /quotedbl put
dup 40 /parenleft put
dup 41 /parenright put
dup 42 /asterisk put
dup 43 /plus put
dup 44 /comma put
dup 45 /hyphen put
dup 46 /period put
dup 47 /slash put
dup 48 /zero put
dup 49 /one put
dup 50 /two put
dup 51 /three put
dup 53 /five put
dup 55 /seven put
dup 58 /colon put
dup 60 /less put
dup 61 /equal put
dup 62 /greater put
dup 63 /question put
dup 65 /A put
dup 66 /B put
dup 67 /C put
dup 68 /D put
dup 69 /E put
dup 70 /F put
dup 71 /G put
dup 72 /H put
dup 73 /I put
dup 75 /K put
dup 76 /L put
dup 77 /M put
dup 78 /N put
dup 79 /O put
dup 80 /P put
dup 81 /Q put
dup 82 /R put
dup 83 /S put
dup 84 /T put
dup 85 /U put
dup 86 /V put
dup 87 /W put
dup 91 /bracketleft put
dup 93 /bracketright put
dup 97 /a put
dup 98 /b put
dup 99 /c put
dup 100 /d put
dup 101 /e put
dup 102 /f put
dup 103 /g put
dup 104 /h put
dup 105 /i put
dup 106 /j put
dup 107 /k put
dup 108 /l put
dup 109 /m put
dup 110 /n put
dup 111 /o put
dup 112 /p put
dup 113 /q put
dup 114 /r put
dup 115 /s put
dup 116 /t put
dup 117 /u put
dup 118 /v put
dup 119 /w put
dup 120 /x put
dup 121 /y put
dup 122 /z put
dup 123 /braceleft put
dup 125 /braceright put
readonly def
/FontBBox{-4 -235 731 800}readonly def
/UniqueID 5000832 def
currentdict end
currentfile eexec
8053514d28ec28da1630165fab262882d3fca78881823c5537fe6c3dda8ee5b8
97e17cb027f5c73fdbb56b0a7c25fc3512b55fe8f3acfbffcc7f4a382d8299cc
8fd37d3cea49dabdca92847af0560b404ef71134b0f3d99934fc9d0b4e602011
b9cfb856c23f958f3c5a2fbe0ef8587d1f5774879c324e51fcb22888b74f2415
50d7401eb990d4f3a7af635198422283cac1b6cd446ddbcbd915db9bff88844e
784c6bf7389803d9450b0c21756a017306462c563d51ecefaacd079732f12c29
315e4b9623a5752c6f1d8145869e120d910b2644887cea7e30b15676a92537c2
9d3aa80dc30082aba94b40990b82fb1a877e805e0c8c48f61e9f2edac05b944e
e4d8084ec1d5cc517aaeec5b3ea379dd011eeb454cecab3ad2443c887c582789
72355673e503affe0394fc7db31de364e4f56c24033c7df2265c56445ec63a1d
5695a6041ea1b94407e1cdb7c5635603a4fd047e6edcaeb2d0da6c9e0e9396d5
1a4a58e8fdc1578730f992435560a6e2d3e3687703ee2f78f5896389ac8470bc
806169eb01762e89b6dc9adf857ead656620e2589aae722c37a2ed7a2941c360
b067ee34d8d5ca3bf68db725614d936bcb207781f4d4ec2ac67b13a5ad161f3f
059add7b5e3d904831e31c20c04546fae83ca93a35989e65c201756888f727b9
7e5313c9870ec96e4cec3901ea03a5c744754485e7d169bbc98bf872d0796e18
9d43b712950c3786257d8be06ab6080b9d9392313298327549a8a41c00a2cea3
690b4a333e45aa815a64facae1c2b44640860b8b8687afbefdbd5b4a541a7251
4ee7d3e0752af3e96a88c95d31fa16d34ba2f02fdb0088b165844f02611c734a
dbcc2037bf741fdea7e8bcdc130c70c33772f777d8bcddf4611db99001ccff14
d7af2bb05defc3480bdab312a0eff2f375afb4e0df2f803c594b7c93f71ca4af
861ae1711932fef19bfe2f9b7adb69d68e5a70ea4d1a3d5bd85231b16993f65e
fb37a0a823f0542f8c2340a073dc1be4a8347f9d3068a6435cd8278b0db1809e
8af9664c2c989b9f16873c009449b6284b85da4dee11c96a05ba83292f0edbd9
2cf674aad6ac1a5ff966ffc37e88a66048deed053565b55ef6bdb8c2f2f67832
f8939a32442ea54f13d003494d6350a2864b427a9126a9c26a031909fe53fa84
63b80c3ffd536c9a5dd29ceb03148dbc24c0033ae3542e26551168a474b72c73
a7e2c34e90c8b7c4125d8657cd89e0449b5969f05212e64175cce0f9faa61069
ed82a8ef9276f14e2a08d8dc7e5a15f1707902c2b2f41cb1fafaa593385c2ea4
1499e485ac557d0d505dd37049f7ca9d303d4839275a1522489af3cae4c8d3d8
0584cea580c00d8f7ce736b638014d8afd7fdc438ebe18f2c93050178d27e8ae
fe411dbda894ff8b1e900a07731e233c3fc33767a273b314e40004fe183cb5f1
bdb61a8d2270041c64032c0d0b191c1bc79f85b5c21d32b401c7a7369b5b0dca
42a8f4c16e56a032966fa060f47cfbb83fab0ca27e46f19c8febbda62c68cb35
baa9123e654c0e7edfcdd65cb88d0c8dd1e541d7205e6fe25b51cd9f07dafdf0
8d0c7757cd1b60d9c0430da8219c7fff22b331a40597f94e6852c0c39aba5151
b2fb2918ab02ecb5f4a367a7c3d4ce20f0038c7f34226a371ca80cb2014953bb
6790bd4b0b79c7dc2b9b2a53bf03cb2edd00b6a0fce95affbe03f0054c880d38
0be72fd087949024da3e3e034c52472c7ffbc00af56cbbb845f90718ee525941
dd68aef18d0d1b01c3771b76d10b7b94233d669f520d114deaccd0a65d951270
c9e4dff5e2a56bea407ffd439459cafc7d32f25ed1ecfae51d121cd24e5cc208
bc7372d1c0a39a30df00924bf40e3ca8953a4d172f508d816924c7f8c74ef3af
3cac2447d35e50d23e951d099b3b371754d66338fda91ad154489f4507531bd1
b76760dc2b7ee450c9735cfc7b12af3bb609f75d8c15d0f09a4f830e69873453
70114e64f4dbc578560ecd976b5dceb6b3df755aac88e8b3cb9b405908a3f613
b863e8f9dbc268b8b753444a73e48a3c555f4ea05c62656b5d49a47af5ea563d
7b55a5a5e600dbfc8b9fc56e6d57e8aa7de31b2bc8db63d36a78fda37775f9cb
a4943c0a0fb2c68663444db13e3b19dcc6b9053221ae1e12e51dd91a5dd885c4
f1c12acf2861062c9a5c01d1db784146a0ff7cc6b6e6dd5ac1b227f181be78a2
87f0496a3bcd73dcbe3237c7a317f016de8236e5733b011d53ae3cbbe32669e7
80691b03ac2c50ab1c6b9622915ba8ab3915b58130ba99fd2feab474b7839309
08b12d96ed9376fa70f93061817348764bc6b17681ca492b04841422a20d7484
7971a3db6823461b324cfb0fb48e7063d700b3e6d1c428e448847a53d0780934
bcf1a11959adfc88e4e81a25efd6d27b339230675f6db389e1ddb296d9051cc5
43ad0e55f051ee604a3dd8bcf8d7d650370cc8d06e8293a39487b5abc74c9bba
5af14e88db84f9a3828a1d38e402b726cc0ebd3e6c3052b8db26511511159ec4
3b30af2749f53550435ffc8b52196aada719642fd88202ae528f73ff52fd7fc3
3c02dae44ac264639ad701600b3b042dbf883c8873713a4c45a96b5aa1047652
524523a14fd815d986cc812c3f6d461f8a96dab65c2100786d3244b0231246a9
7758b3a5a8f00898c3d3489464d6c5eaf00c5749d578f2a835bb54bdbf1613a0
df693fe805449a227dd1939a76b1164b7495d0a8953a7755fb72c656ba20a4c6
d0cf1c27242734369948616e5ccb01659c6c45a79a21d2ae5d08ddc7b46ad2f4
1bec1a378af006133682ec4468ba8f5808062e831bd2d803f8bbfc24ca23e0bf
4825cab3200be5fb78108b38ec9f0b1d429340160ba600d3b9833bfeefb1858f
4eafff06598a3ad91804d7d9c176bd4d0e873f31852d7b064fe598e619f53e06
02866bbda3a5aeedd9da286b48ae940b6f7d7db1b8fe72294fef48f9d83fba4b
c8411d79d5241a65bdc4174343ab39c33d42dd26a61a8f1f3e688b37708e68a5
5132e75b65e9b2d17c0536595637eafc93870fdc87355aecd4622b78b247a107
9ef4ad766eea276788938c29a5e55eceffb845bd56b741dea11a946d8aa4bfaf
58f54b35ad9f123116681236eae673e9bb4725505c94822bf1d307085324b4a8
afd3d3feae8d707591a3f740ef01a1767ae83f02cb62b7d8b58bebfa452e30b9
16cc5498954f6ffe157a4ac19e7395270411ab320f0ff7b55ecb2b6f98e555aa
0e674e8ffda484178f436bc91647632a1a8d463d29d731346668baeef5628018
63ff5ba82a84e7bde298d381b38d38c731bafacc3389f5644bb0bbc6096b44c4
1a3b94622022150fb1e8b5e515eb992fdfb05e9adffe9257069547dcb0edc643
e51b30b24f4baf669dce6855ae3c019e874f263995e33cf623ba2890ddd0d9e3
685f93ce883c2dafefbcffae9740bf793e15e469f48e8fd7eacef8979d1e0b12
aa1daf4154ec632d1fad80013a4bb2b726ac41e76fbb1b69ff91a7f8e9f91741
fa543ae830d8d6453354c298fe337b642aaba25c766bbd3025ebc97194921266
133134a573ed63fbddcf8bcab76d049b726f75120120078da5bdd0429641be63
a98277121f3548e0596aa0cd254b923c39ad82be9a959c2f933c02ccdefed449
3b28a44806e001a3c62acdd8af68f8aefcc6b2eea639a971fc700bf52fbf32c4
da1be8c9a6f33c203552ab98ab9e407f7e9f203e6a90738d7e5c14b4474bd504
ba01b622ede4ddc5cfab5bccb6342624dcb766b395a01d936e25c78203bdd057
49ee01971bac4a675a644ada0cdac1a32e2aa2a836c00e2822830cfabf42ff6b
6f631b8ac5ad8bc80dc4390f24a3588d01fbdedf599c3c4d1a8be03d5a6003dd
6d8fc99e91aa373f6c6c959683e336a086f0018e4b825486d5abf16b17f7ddb1
95c39507094362b6669b88219ffcef112b3ef76176179e9d6ea6c2e2d2e98464
d76d9e5c5d8486ec69d08c9cb4aa52dc3dae00270c2888a6e5dd2525e904fa48
beb531a076030372a73e7712db0bb4e540d5805e8367ceb3de8c4e7b045269a8
480e407f1cde6e60f70476d3160ed63ff74ed0741aeed0847c3918560c2bfd65
897fcfcfaf480c3615da8d0f83742f79584e1f122fcd20d53bdf1fcca9818c8e
74f8ea956c6091a8ba2ae302cd8731941fd6d24893a6a2196039cd1e8cc7c589
a94eebe8e01909200f0b8a4bb73b4f5b63773bb43d2c10a76403a99ddec94b4e
7daa253621d64548a50dd2d92ea33e98458bda7b7926eb9cf0b5fe39ce8e8485
35f782c52c126c1f6824d8edcab4e1bf608f1874a2c4f792eee5c434b07b0db6
43011eb5c8b02f70e5c5ce8977d79eaf27052bd64a8613d5db4f66105104399b
74515e31b622db45e200f93fe8c92145f11eba9a573f45b5f2ecae7097aa2907
a4c7cddbb69a1bd1aff7e53cc9774542eb1847a3ed9b6c94830f86fc117abcb3
d8d5c404c5942acec8005a05ea5c2997d5431242b5336890a4e99c6c1be3eeb4
5d61a6d792b2cfbeae4f6776ff85d6bc2b70bf3554b90732333dfda22ba6d6de
7d5e49eee37e08a547c3eaecb851e28c4e457a90472bc134b5c56dd3b5f9ba94
f358cac49841e78d0a1bd9b0798fca8291f335289d78d24e07a7254739956538
f3d389b797d2b270d4f7a2e88f017fcb04c8f9c103f6578c2c3c843704b2fb07
232e726427400b172b8220918ee3396a64cc6401ebcfd214e0db6dcac1fb8a1a
c3bbb9dce29627e193f3b144ff04431405791e9b1c19d78f7872a9a86337b421
29d191d72e49fc6ee238c2d13457b067d036f74be4d5095a7e02be956612f69b
6cfb5acf87763d888c11a756a908755484c4956366330c9712e7650429d32c6c
e4d2cd1d5b1bde966be1ba782c6019c4f78bcdf326e4ecbb79b4f1ba5a8903f3
8fbdd3890fb36006496da1a3ca3699366a50804284ea693b51f1629965d41672
d16886f44ba55cf726ffabe96eedc044d50dc1d12aac7f2e22ac4d8adf11a523
ef5d1e1865678fecf430d87892cbfeaccf77d7dbdbda9ae9e0dd7cce9c2f8350
ad19cfdb69b4addbe4fec77da30f544e84782ab329975e60dd3e11e9805ec0d5
7e6604b84961c68e5f19f8bb303b1b69b36a64aac500984e902be9107ba92a19
8112080169a75c2ac23422bb4ffa5ac6860e8f85339ec1783ce832d31691d46e
06954b2f68a55f117cad91a7e7366a0e0876241e02bc8e04e2f7a199497d1aa4
ae42e61ea1ccf6d40727b3ab65f5f1d741160076366dc0b859ac8fa20745d32a
5b27ab89e964b0d2837a2ffc1ef708e21fcfa984e298bb48a91d332fb8db6a3b
0f2c76156893a76f53c6c1d1595b6fe650da2f7d803502a7118db4484adde271
33455c76fee29bfdd43c762999d2f1953977b9f514db96e303ece594dd924945
17d3c439038c87d7e1602c94702098dcf34c063c8df4325d7974d2b48c53cb64
a7d39ba9301548a3dda5fd25b50835c5abdc06c24a7290b4b77d94a504ca6e2f
9aeeb678164a24a377f4c0126197c968504852080f5fdc805a8125bd7bc701ec
6a211324c39dcb1c5752c1e24e492486ad37013180accfc861474c45a5f0d993
00e71d04568128fdefc88ea7531b5ed09b7d1bd06f99c5d62a43739e9d887aea
3e4845e47a3da39c061c6b04ff661fb5aee552ec4a96d446d699c9db2d7c58be
997021d6ea816bd8d7d5037214030566dbc7a04de7b76d7f73c552fa56742ae1
8ea5c89a3435dc8f1ad9ee20ad549093b505e4b375bb1d4f8febfca65e121f69
35d0cceeb4764c1122f822a53f249f61100ac9565e9b91753b271884e97279fe
4351b0ad028a5932529c3099fb2a08009bef2b83eedc3604a65ee657e4b6ef9b
5d94b4049c7bf50cbd51a05c7052988f4ee4a7b0da976455e1d46cf442f7ff93
c59cf10b3cb7a4b6036f94d73e347291843d6f2d0d6678629fad461ba4360361
d93dcd2d4d5855cf78e140b3e6446d253e006c396d88c3f8be42be5d90205261
a8599f6e1e0314069e05c6779b3634878402b80f1110df74b9bdfc71369aba16
5a758ce5628992375fa2d40530b38688835f57628a544711147bbd1ae65b4301
1f9bea152d22d5fd1f5d6ca0315ef5f1d1b87f429603b2ee7a7ed514f230667c
c3e8b5f93bc858abc8a2934e48ffa095b10f07a1b92a09034d6fa81d3c65f4fb
36a8da964f13d93600d8db91e43552a642d9892eee16c90af97270ac28d6a35c
f4b74f23f068c75e8fd8807e5baf09089074927b834b161b962177c5ab8a3306
3e84c2ed899cbeb1576abf4f303659c28d7bb2e639be7031ebddb41501d0767a
a6282f394629b5b2214273af6538b781880d574e713f66be48c2e5cfd8a4712c
85dc1a5046679454f5c08a2a0e52d98905652a3958b864042a9a0d234bdb7093
9e5139475a70c862f671b59111c98c0fad49398db451d656645b1c6dfde0d50a
c07cda4bcc270658f5d65ced55b2699da70201d0aed473a2ab87f5c57b2c19cb
13c7e58a557e848cdaa46090ea1cdc781eeb3babc88c6639a38cf2424facd102
f95b720bb621bbc1240d4ae565ddbead3c8f236fca933c8006a6853177432f9e
4fb1155b903d4d60cf5285e1552388f1af6c4691a5065a5ca77ef0181fb1087d
b837ac89e2f8f8899d53324544d90da95c7e5c2c2ea0880804e7eface447aa6c
937b771048a3fd3704f109f452b33b56e5573d30ebd890965aa539a80a2e0d0d
6eb8a58e0dcaef39af0353705e56b8b60e831f2a344c13339a2784b3d88a87ea
140b2b3222f5fb2f1c0a47396075deabee37c860818833ac2d122d178c8981f9
506edd20127120a5235c56c4193ef8432c9c0382f0f98d808c80e498ceaaa8e6
867ca742f212a1080f98c9c6044c8b3714f711f6be993add29902f6f4eab8c7a
379025b3b2848a28bf72efd6f15c6ebf6b5689692c5a41ddf1faede16a1e2e3d
bcc28e0981d478e1af92e8b0e9ef42103c8f9cb62846f1c5c85707d83b4b75dd
991dcebb5dc2271abaff4cd922e0a25b36e70d42194dec4ffd0068aa87b97f09
3411fca57f0a58604c3f339d9f5653a172ebd263f57c75b2a57766d2ad01c862
965333d5393ea76f5ccc9f9517efc7636b17b58506114b79c27925fe4cc01677
114064016c75233a063f3cf177f01e8f9be2d66ad3568e4ff82b85a8a0e11aab
e1c36986cad554abf00dc8f0aedac7ae7eb8064200c95d4a2fcfef7042409a7c
ee6d977ad2646ca7f9ab9aa8f11037283eece173d77bf8ced4682c5a3ecb8a55
bccdb9524debeac26fad035987d7fa39d3aeb710a8636da6a2ab31425ca740fb
ae4b33722b68c458ea3bf5bed7471d4f6aa1378466434e0017604b4d9a446f35
aad4809e9e169d9047748f22aef44657fad62625e90273460477285d0a86c1aa
f2173f9e7ac61329621d72a0d0b3fddc914295be1e54f6ec763f664b6e65cbc2
fc8aede647b4304284d1047b021940b8afc76ee994bfe3313f36ba0da7c0b709
1915cf378f6c589f09596bbd6eb203e0282201a8181f657a0d5b12c931b5ddd6
233925693def6c753f77c931a1ec70c3e31aaa622d32b27a8099a83fc05e5d3b
9fbe725e6c9fa53ffcadb3913207b1b6064082450c2939a372e17daaa9b289ba
c4aee2137a34f9f8028fa55844ee5b735812018dd2e3ad04a85f012f3037fbcc
e4a5101bca0cc3c98c73508fc905b849aad84d120541cf4fc8c01116fdc051af
d1e85e2c16909308b189043001d6cda538afd37282c5ab51c0585cf1e3d0909e
8953bcedd12a4133c8a464971c1c124ffe3b3ad42b6bbe91981518a7bb5bf223
a918e2242a03bae331dbbb7e54b60865d74970c63a3a646243722993fe1f7e7e
080d4dfd1af17bb0452d855faf5351573f0f8e3d93bf2c8702a8c4c2085bbec9
a1a8a1bc9936618de5a6be967dc42c3f5912da9be2f2d22af1ecaed5ce5f44e2
866df3811f0e0e2b3b5490bfe6ac8a210a7e47ccca3d0d1629cfb4c4b0e884a7
02309948c01912e48d697cd3b842453e456c75a245c7d7a446ff10a43c502f73
0621018bf5baea052e0c1be7cb674e482423d5c0911b698bbb00a1f2f357aca2
a74391db557e43dd11ed52c78c7c9dc444609de850b40758894cd96570e3df61
cf8581203353bcc5eb168b4e7e4bbcb4ddafa476d63f2b982ddf12487a486b45
dbe7a0b4974d13c4236cd0e223d0756d7c257b4aa00e94058bc051841a91a480
d6d0eddde82eb988db6274e0f29cea7a5958d9128f658c628fd0cb1f0db3d300
17b4d77bd2fceb61d71a6a95170c45398f00fd26a9e159741ca8b7e1c6030d45
f2a624b310e904b516f79dd6f39677913a80dc17558c1e5669aee7762e3784a2
0fce5e639064791d44738b0d8035123c9b753b3da2dbb98839b4211ee7b3d0c3
141d1e616567d4a98230c1c56661d94b8ff1e7a4f5cd587dccc9c96c27c63fe9
bf53a33ee9da738f26eb23761ae8c69afdf38b8a8c49b841d96b5d06a1f35cf4
8c1215b10c3084eb0f126fab97f436f6885633e29e2cb869b92020a9519e7964
edc3f27d105827552a37871628900f900029da1c0fe996a08dd27a4250b2adda
a35524b2000f342c2e0690b92676af7e2eb82bd19f858420a88013f5c3a480d9
3d91d46ede929080f48b84a6ce64776a3b11c61d10cd09783e11da8f3d784ea6
d3ba27a20f5693051a15dc3a02115abc63bf36aac55dc8e920f70bb580e1e973
c0829e625dddffd41e2afa85b4e41858ac0bd94eb6b0eea35e44c5cc808b5600
33ce448101e3fb8e24640844a91f4a24c6ef294f909d08a84790584ee80a7196
f5437ebecac65dd310fa73b6e214f3f5fe4c321c30ea33b1bb58aeb6ab48a944
595f56a4a3b6e76d304d7d8083437526838074e3573805c2b39fb15a5f7db01f
23ffd60e6eaebe43d7f6f6df2d4e744ffaed25a0a194aeac06461ded1ea61669
c925c8ce577b6a6dfe1e5a824744aab5ac5379d5b3c4688d6a50211e752755e9
9f1c90d81084284414b07d5ef23f1d9210ecbc9bc516072648865dbbb12adef3
ae7e53521f3e9b99d18e4e28a42cfa13468b06f06f9d4778a1670bea3118cbb3
cd29db109d893a7585b250e0b8b73de06ac639d39879c1a26e82092b9aa2272e
b3a19cc305f7ed9804e1d808af5f490f28a4e329086d2be7df8ddafcc445f417
36219605481798a7f6aa9a490c359074a6a2e58bf0b68727f798ac8a0df54a99
9f8417c7b85d4870cf6a7588a5d5b49e4a99a19419eebd4480c50d344ff80417
aa158403ad3b646c52df0e555dd0d5efece905acbc65443919a4f16ed3cc6f7c
9483616cb6b0d6a93fadfe9ce7ad1c6da0147e2b19c40f7f596b8eb076ea0178
716ce353f6d7ffbb5d16efaa55ae9f31f925705261313dff7e20afc4bc74ce0a
f748b8ac31288649b3ffa14276323e98f8e24247408ccbfea24482b47c327c69
0476173a022065abe7c055d8e8668af65265867ad1b0fcbe26096312134c0433
282b66a750cd433e23fbd08162205addd2e66f5ac7ab5b7e356519f80221a5ed
442a64e338f907127d79aa6f0d60f901c3279616578c87e9b04649169d2d342e
5b18c3e801467b1ebe9e619373f0f8a13ba0949e3bee9268e7c76ebc9a6b9f07
2640f3d651cf449e7ad3c04ea81b9af2fb8de694852e91b53595558e937696ce
54c0b61214342e5a4897078a42c7203bf9eca194325d88dc11b61e3a31806d8f
01687a4e0418127c9be93ac8a3d3091986fe740cb7eea4d0ea6970e1d7bb2029
73f683e7b6bb966c2adae61352ded408276fe4e07a84514686a071ac60bd6535
fdcbbc3bb0da56bfeeff6fff7c6fa6af09d5cb110ca95c7fdbca4505f5cd332e
7a8d82cbe641422fb978e2a23040fd83a263925854a32fcea12a43b590fe4382
660ec18a5eac419bc6411817101344c6f404683edf8f4bec52114b77fcf9ab17
9dd0fd23909ef5b12ba5b15cdec5352858597a96c240925f01be6c026bc86790
6f1e890f1d507030291a279bdec533ee7f95c017a52b75e16d4b6cc7a3ce6a04
2de6828e82ffee4caa666a83b34da47e62bbb7744b19a5d4808d544eb4340045
2e723c83610a95df83728bec5b50b5cfae9859edf267a8bea11cc7496f087dc8
955f1f834c0af7a5ab9cb69fe89aabb812d241e75e14bc6c9b126d7eb09b17e6
89218a6a171d8142cf1a3b813fa4876bb7c444d502f51d609536661686505a3f
f6f12a31a7fa88fae5c5b4601e58200f7e36ead1fa8eec35fce98e50a559af6c
eb5575d81902d8881df0319bf2265c0534916347e01063450817e9333f836274
5ca167375fcafc8d1d6f5a9efb1ba34dd482eb029d1287c54494b69efd47edd8
8529c9dcf3eeaa257f70c5772289b48f69266c42c7943261bacb38e3a8fad7eb
e95fead299c23e597a18164ee19933c6eefdd6b35d39c00ad3c523515f6b9a2e
2f064922f52b279dc1f8cd9bf396d3ad63db923d1b7d8ab51ba663b70bbcd80f
09d2a1a3086ad8227cb17202a65b090e81bfb00888d0ea564981027411c6d4af
c8cfa71c0df856331137423f8fd030f2555a524a638baaff1b71bc9d99bc6336
ba20d2501140f5e47b40d393e0d9186a9a6c2ea50f72dc73658b4004561b4808
882d0e2a4e6ba50a56d130c8f88967411b2a1d8973bc4f2eea84921ba6e7376a
d19c4a124c196f1b46953a33e32a407cb9406e8e63a39d28f696e93e0aa32dea
2e80d558b41d7d4cd0fbab5e4ddbb5f58f1b63811610d384601b7a3784828bed
c9591dd57b576ce5c1c43af1f595dea577f692df71445a70090fb8dfb0833532
abf54a581dc37eba9a0842977732931f45ef4d5c3815d1cf600560e04e91ad17
e47a92fdbc55c2322fe4bda54b8185b97dae3ab626b188fe27e5d3cceb6e5f25
5bfb59b42c46a43979976760325e5fa482d15fb377dfdb62548d2d27e22924c6
c7fb929abfcf81d021446627f6503e83487a3789549edf16097217e4bc62e5f7
a93e19b55484b8b453b1d5332bb0102ccd3e5ef00c8b6c3df0d80755ddf6f450
054423d9122b7a40e22b3fae41b8c1eb7b0004c20d2ffbc0737d537216799996
4d47200a0b349cbdf9be151aaa932688fa3bc241088758c70f32912a5cae8795
76e055aad3f76a254874873b73e9373f92105da9fdc2251584b6491dfdbcc58e
aba6e1e137cb6845672e19f68db0e9ea5070ab2efb5c07cc33b98fa1ee879792
b2c0932781894235d7fb97361821c299c8083799db5ba25b408bf2b3052c138a
29bab9950fabf08055032855700b5026a077845a8c69345844bad2b3ebd0adbd
9ade7f3a757ed59ff7279d04db76f1aa0a6e5a854265234dd32b671d418e4efd
8fc612f42ba748af77c01e863cbb626721b8911cf7cb37c69236fc8da5f4ce87
71a350b7c033029d8f2e4062482e44f7f04dbfe2e9549b05c4a6603ba3a26605
9a7728dd6207e96a51d5ab3cae8be6c3cde9290ced507c3bee293cf366a54cd8
6b669b7b26e0ad8774a9a83dab5d42f494b018ed240d38cb44b26155ee7c18d5
b49a2ae5cd44baad218e22bb1d79add079e9018faac195ff01466b74961e8777
e3dc7f4178697956dde9097594d11587b911b2e6d78a77d41e100b33bc1f3aae
45d1675d82dd7af6cc7a96d98c341183deebf8d2232930863701137f0b058272
a5accdd57dc1f9a7e815c4463eafee156617a7d8e64f2488a0ef2875477e6f7f
eae47e2ca012fda746927b07573ef22c79f80f5ffa2844b6249facd49cc61235
0e2a6e5ead8470c31c89d47682a40acdedd6f3bd96611d56d84d54f1e9f4a114
74813dbc86d6bc9fdf27b4f02e521f66f58c5484d2b598ab42a221f109e1ba46
7430a79e2486b8aafd69eac2c6ce8d6fa8b41472134357fba71e0c47baccf499
a4170e4bb0cff38dafa6fdf63b5de6567c803b3c2dfa98c390457a230936314f
6e37f08a7ea73f853dcd91b77514580c9601d9ab0d79b5ad5cefaa1e197fa530
f09649172eabb2659005b61233c50cd7445420df57a2acb7cb9fd0d46fd0cc97
b5465ac37393900f009eda5877fac6809393695937cb57862c62c9555fbbd218
f539bf7c1af8e438eb96e88cfd1a81b0e37f6bdd455deda7018d75a385b79385
b7cd27a7749f468c8847c43d520f71fc19da41652049720a3669ef4f352b2009
9a197504692772f2e89084614dc29db10354fff16e4851629e9e23268aa77408
8e1d1d52fab96acdb49fbd9666e0bd769b99a5459d514f478d738062d62cd7b9
78300482e82f537a712ab7c34fa3da1791a6300bd7368eb6beda466aa185544b
1ea1896c9a8850fc06524594335f61b244e58832825f94040d107f2e6c499866
c273d2e0eb60d4ff877bdb5242f8f150405ee92b182695be15d760abf075f697
f91ee3b7baeabde4f55235d44b1ede0c002da626566cd17c10ac65a6ba6b010d
c968cf19e2ae7a081e8b7dbc50fb07fa002f43e20f50d2adc03fe99c9db173db
ab58c4e0f0973f5501d360d0e1d6b4aebabfa7ec2d8dcb1af6ace9747ca0d291
c4adb8cd0d4efbb3d927e5a47ab863ef3ea8e3389c34a73c909a29f834a22bfc
b3d20fbab176c98ad687b1237931c48fe796993480bf6a0429a445438c86eb4b
51399c0a78ccf5b385931f4b59478235dc89efca2c6bc499369a3dff493a288c
bf0ba9dc3771caeeada9a3fcfea45ced81f965250936650f111cd255666859b9
b2b020f76672d88408f431c573f0ff2d703dc88d6323aa5c2cd3b9056b17d9ab
a00981fb71ee93e51dd4c8c5af288a4d4d1b2e9c01d15a77841d3123141c9d29
c2859264800b78bee5cfc2bda268e7c33645c8733187e7218f23b33bb635331d
17be92ffd95ae27e5d6a7d008cc8696709de013fb9ac73ce9425d5627b7a1f67
5cf5e63a0c9a1b83678225d2775554105c42a83e22046839a8c186ad603e379f
46e0a84cfe43c7d8b0401b0a319aae509a4249b23df02f2ad141afb122d7f4bc
9e378998c8d181821c41d00091750af428f800914f0daee6c08b80b58b105b74
cea39d4556bf38ee3a6e827a877326407ca27e98ae2ca1305fb0c5b8d0363370
9f1fdb2524d46cac837a67771da819f3cede81c6ed7a2012c2691d316c8266df
6052f67ea0c4475316c95f98592a38d999561ff8d7de7abd0e840bc09547cf0a
87163f6a2ed705107877eb5c52e7e178546e37fd0db657e8ddc0d8eb9b89582a
504d855e76e76d466494080339ced91dcb8a0a765c182daaa734462f559c35fa
dc6a869c0c90dfada97f7a17a9bdf4ae6e7f63d7d62fb8aebf39a56d0b9fc012
813d27b1a4c97ad5fefd645cce0b7e1633f34b2cf819581f8c5e442efbf11619
6d516aef98b96e7447e90a6c436e0fac81097226c75a199324e2df1838c7156b
e223cc5f2a00ba8e74367fea539a67bf5fff55a8cb10ed0547f2451d2fbbc8f1
d367825c3dd79900e2799aaf773cb0257f01f5dbff1900a554e365c00db8fc32
e8a6d33e9487b21f9e4c57ed4951546e5ac0c0d27dd8eafd9c80959f4e8b6a29
4727401318359974f6d7c8c87262568eeb6ed4f431711420fce7603160c16ab5
b5086536152579520747f93072c9fdb4605cbe39ffcad3b574603019afb3b1cf
e868adf0ffff5a92fd069117f51e6f7dc5336cafe91151e40e9a70e78fb1a713
df5bede0eaf8e1ac87409b458005312b7570781954969aeee3c6d876bd272355
b7efdd723621650b4e718fd1399933d7457d4fe49e7b7f007383442ebed9fb07
a46f1c98a5d1f13bcc361703d460b4b176707b1ea10b2f1528e898e9212f269c
40407b55212307ff5a6bcde7fde9dcd1e007aaed46dc7674c2a18aeaa0b3058d
8c99ce5567e62bfefea597bd904621d319cb36e9aa08b392c6b245e74bbd2166
dce18dff49cc8e8c87cee7907bde13ed1628cb2de9d38a17b1d5477cdcad4526
e08f820ddf52bcab86031b97f6d93dc8221827a4c9a1582405016e2112a64165
63ee4bc60c5c17584fe0b9935bdc41159813e043f0ab07f8fdd5d6b6864dacbc
7fd5ce7fce0835e5d9fc0d9ea62a0d5577c4e5cf0f91e495525e23df8fc26e6c
183f7123486f057258e3ddd4bc505165e7634483a13af94ea4352d597c45e27c
ddf645d0ae0ec702b7faac0e54b33087808b873ec95445754371f2de1b7cf8aa
4157bb6248c7aefc3e08dca1ab7aae211f26558720f5b62009a9454abd4650ca
6f7e28cf5546a2a9ea00af815bfe78888098ed57ed7fd754df72645a9bd08042
ccf430595d75ad890fb4b0c0c8b5be79ec280694512bf91ea0966d6146a7053d
d842c496334a6ce3ec0c1c76bbe4a75aa2f5adcc233e53021fc66edb3e95a4b3
2b34bd75a507b72bc86ef6eea04baeb90af7075ba18e7c1ede93182cee86ebed
33490b8d04b9fa9aa45b22368b8dd03c853c572d84c5e302f315a72dbb1d8825
15c4d8dbb54298142820ab6d4ea23c5a2318c4d7f9f09d640b3dadbf3ea86371
c4e099b81ac104d2388dacf5986032b6e29687f68a02b7ca8eaf683e62b42c32
e91f031dfe614ea80a36f4dbb291e880694d9a0eb7f4e809bc60abb13801e822
1868d7d7f4ed9eaa72322cbd15d1a6bd9b359f4fd877a4320699e48bf0184383
7fa5d62896870f5392b87776e369c67fceeafcee45c694dbd8a1ea0c4d41184f
11cfdd85babeb744d7b5d771c9e074e50cc91ddfdf0ee817eb0983cd4a7a5b8e
91a06ab16af248d86a83ee984ba62942f5bbe6c10c247dfdbcac344fc32f262b
644abe752d32b72d249b01e76b300c4149fc65ebdaedad86db5965b74b811dd3
c27dffbaa0ad8871669539369358b2b2d28bf59a21490d6c918e81b605110d55
7e895528cbd3b0ab69095146702b483b96cb421529982f9e2d58c7eab0acaa76
78e7ea34b422c50ff7b54d7f6658161a60cb127230735e2a6ab04b09eeb2b039
68c79ad7cd8b7c9e3c47b4be6e3168e5d6f12d8db764fcd92b6cb6d0ef846f2d
63fb15952a40f257576dcdba15d7417c84be62e6ecad3794927807d9123926a8
74bf77f789fdfec84b2d8b2eff29e84a755d793d869f26c2a4b6f4999ad70e6c
8f158a251633e836df3d300db1ccc78eb3d9c86e5a6c413bf95de046cb1975e3
35b100e4b87027b724a7a80b9618b0cc671e56f173bdece8b96fa06815073a6e
17f000b0c38ef2a9b135e0146d91ab99fa6122a3d5ef7c8fbe788971eec3588b
1df041eeaf515981895abeed057a4df522d25e72ee74bd7fc7d7e992f046e93a
fdcd48fed8deacc6608fd2356efcf07f4bf650eec30a75d2650efb9bb96f95f0
d226f514d89611dc53152bd3ed4646c1c009b0ad90abc596b71c218f4905d762
abea63698d634f171c0906f31ef7bf61a3aa84e148fc7243ca7c8ebf227a2bc9
8f815baccbea90e329a295c1ed8a5d47d070b4635c5981b287ebe99c18a93920
100f7d22915fb000b7f2216d291a5f17353cd0dce4ba62fae79b46c442776bce
a5c680e917af255d7b78ba96d271afbc06ca15980ba0026f825e7348be929e4e
370f0c8367cd641d261d990f436c6d2e4d239b2b825abfdf16fcbd4b8598c6ba
c644895b5f76cd7583540130893c521bf23c9532c66b3307f340faa12faa63a8
435ec331e4d96a8d64e642d7cc98d3e155dfb59e537e8a3c1946318605a221f2
d64c67a1ef6268a8c27602ada8e633a9e504ad0f1d2b5691e65c04ff02484051
8db5071f3def9e539874d9d1c7d7273e5f4e6f5b55be8ea732965513d62466b7
de32204864ef365fe16bc5f549c46b8db73fbd62c73b2d46a39ad66e32b3ee6f
4307a517a1a859d7dbf4bae29f887d3a7896885d7fed9eae2ec8e0aae6406118
fe5b95ae5b58345d2a9b72a70f64c9800c57920a528f16b275e261d2a274cd32
f2708191831252275cde9b843c4538091fcf85976e1a6f28ba5cc25093b821b6
2f34d5386fe16738fec129ce5febbf5166f9b80a0f942864c02caede10f94be9
d01fb9a078a8187f58a9d53fc78526433266ffb50a87093c289f5b0264627fac
1815bfb943a8673f95d2de6604953e3d52faf95bf7560f99ced7620c55049f2e
f72835fc3873bf1c860eeb2b931826ecd2efbfdbaba1000929f7372519497086
35578c2e595cea101b2eb7064eaa804c8fb9f4c529cc74a2864227663cd0a97e
036511f8edc02e2774976ae6078eea540d49594a989d398552e77b936088b0e6
83f48a8c73bee08a2c424613b2dfb331ba770fab58047e6ac8df4256ac394254
1ae84d02cfd4368db50841479b52a12ea26fbbae5e947e33c229ea599f836d27
72ca39d8facdcf00fcce2a788be9132c0bee8712103d2cccad2fe59358552422
a6daf5aac31dfa04b6106c4d2b6bcb92e4879ae789488cb8860c796ddf1c2e18
38b2f475c2d5062be2ed2218702cf0e1e054c5748e5db03d3328aa209c0ac009
acd0a907947fbc3c96ad237cdca093e1b34ded6b8c0b92270dfb4dbbe7aca169
8c8d62dd8609a31b573313174546e5a705753f1661b67bab5782a4095ada3138
681b61ddf12b0424c48ac3c53f52567156a44c9aa9f4d49febfbef9222056e29
eda6cc95e0e0fa39f08473503b4fe03e8be8e2c601d99eb3662e149eb14d9f0e
c4ccd7b120963c058a57c181e004b7ed7a21e4a480e9af9844a47b13d0ab4da0
c23edf0e9708131f2ba446847b4e11e22dfad9e6993efbc9a72445c5ba94d6c2
8a1e424057a5555bb15c85c3bc2408d0815a139e2021c5d52db65c2f81c8418b
c7f6091b3dae15b3c0f7646f3f8add5282e84d363da33655fa30a055dccb16ae
12cf3e836f64e9c8c562e5a6acb22ee5a7d914dacd3532b2179f3299488a3e17
17faecb3bc1df0cb0ec46364130f7986a401f5ff40cab5f5639addd11753a5f5
b30b77321074305d86fbb91f6d48e8c61e69e9947802b01b0c0297d289ffef17
52127e82b4cda5d2dc2f852fe9a88e2db1f6d8556391f16d31f3777d0227f413
8efa2806
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
cleartomark
%%EndFont
%%BeginFont: CMR12
%!PS-AdobeFont-1.1: CMR12 1.0
%%CreationDate: 1991 Aug 20 16:38:05
% Copyright (C) 1997 American Mathematical Society. All Rights Reserved.
11 dict begin
/FontInfo 7 dict dup begin
/version (1.0) readonly def
/Notice (Copyright (C) 1997 American Mathematical Society. All Rights Reserved) readonly def
/FullName (CMR12) readonly def
/FamilyName (Computer Modern) readonly def
/Weight (Medium) readonly def
/ItalicAngle 0 def
/isFixedPitch false def
end readonly def
/FontName /CMR12 def
/PaintType 0 def
/FontType 1 def
/FontMatrix [0.001 0 0 0.001 0 0] readonly def
/Encoding 256 array
0 1 255 {1 index exch /.notdef put} for
dup 49 /one put
dup 50 /two put
dup 51 /three put
dup 52 /four put
dup 53 /five put
dup 54 /six put
readonly def
/FontBBox{-34 -251 988 750}readonly def
/UniqueID 5000794 def
currentdict end
currentfile eexec
9b9c1569015f2c1d2bf560f4c0d52257bacdd6500abda5ed9835f6a016cfc8f0
0b6c052ed76a87856b50f4d80dfaeb508c97f8281f3f88b17e4d3b90c0f65ec3
79791aacdc162a66cbbc5be2f53aad8de72dd113b55a022fbfee658cb95f5bb3
2ba0357b5e050fddf264a07470bef1c52119b6fbd5c77ebed964ac5a2bbec9d8
b3e48ae5bb003a63d545774b922b9d5ff6b0066ece43645a131879b032137d6d
823385fe55f3402d557fd3b4486858b2a4b5a0cc2e1bf4e2a4a0e748483c3bcf
5de47cc5260a3a967cac70a7a35b88b54315191d0423b4065c7a432987938c6b
edad3b72ad63c2918b6e5a2017457e0d4ebc204a520640fd7c4d05e35ea5486f
a43d0e970787203855daccb1ed0b16325828b13b7c767a1a58c87902f0546ea5
404440fa6526975783c2d7a9572b8e5d5176bac598b8960609f49016aebf3763
89c1adfe6a1ffc0c53b3acd9d168ec3a278fd4f1d9b085dc2df701346c9d0887
3d230a161692b42a45bb5da343b4edd839dd60685a59aaa49fc65cd8e2ad2a9c
5cab953495172a1a9f40d5f38e922443a519dd96f667201a408bd1d89e35f4ab
98e2f68c3366efc14b5afe1018d9c845d808d4f8e07ea8168518a171ab4d6e21
70eeac099eb7ef46eb9781384da1fac3b3133bb718bc80082eaea88759745188
f266b31d0c7e791d633f16ed94e05517a32163e74cbd96dc5db066f2a5313d6d
7f09465608cb404613e0f058073af000e5bdfafbbf9da0c0d5c02a3447f2cdc1
f56481901e34265c26d331ac3f85bdcbc7c51ef9eddf2b9c189c5253f8e74282
d6f053d7d183ae17ea175e5ebc401e67d21a9fea139cbbf3bb1358c713a75843
b39a69aa2b1a7b975f53ff22d1dc3bdf7acd17afa1da21568310c68241b31d3d
03bf404bd30baf9cc19c75b958bce7155f03cb0cfe2cae0327aad4b603284a51
7c26de75b8c6f6aaa9debe4aec08ca4b646d787a9dfac85b2c01760e9c6c6162
fbbc67dbd0796831e00c477d8e23c375ffab46d289be9d2328aec2b7534ae4cd
d782ec2453e7787f6e6b4537b46c01545cba6f90b8e9a1bccac1937bceeaa5e7
8e9f368ce067a0a31da98bfbb545be555a7270f0031fadd4f9b186629e5d2c5f
d264f8f24cd5a1c0f68399ff4b29fd77c4a54d82965234164717f36bfc620394
0fb15bb43ce60e206d2cb6754e95342956e0b20f41d34e72d5380fa042f9d8c5
64a1f8d0fad35bb3f461d64fe0bbd1c7733e838df9c6e6c39126ddf7342cf189
aa65d3700111adce8e186357ecdfa25b75ea72b4f1a7e30db223e66dcf9bae75
98e44d82f8043bac9a87ecf0e14f7e1ccbf20b2638df6e86f553a59ef16decad
b5395fbb90c8dd8e87434917d6fc049acea4b2d1bc2d56f19fea590faa905653
4e840ffa84cb0cceec749b7180f13cfd51905036b69a1e50d10a060af632691a
db52f7c25943d20da602ff67945e76a13a77277b3fc40316719654d6cbd8223c
acac14692094c0eb91094d4ced56a6ba2b8932cc4a262bba6b2c4eb32f9dfd33
dbb2f8f70b7b00fdb0436b2cfa982d7fe8de16d522f35b428f6b7c7d1b610510
0dcd911ac928a8e41d781796361cec2dc2869df3b0dd3fb790268a62a26bd6d4
215258c574e9f0d2317f1a3061610efbf08c38b1f2c4ff76291c9e50e21e20e4
5fc5679a030c1a21bfb96fd700391a89416a2c959518f9bd499b92345a62d547
7e594460c020719eb66176d79605a2b3c5c774cb02388955b2ace8d6c23f4c41
6b9b4289e05aa577c7706c8b9f522f8ef8cd39c72f297091487a25478b4baaf2
b9889d7992d6f5bc1a0a97a8976fcfd24d70b881f5411eb7674b76422be335ca
9bae18466d27727fe2a69edd00e6d81bfa3a3ed178b8e56bd8a876229d458740
d20ff3903923f5297340922120eb6f351f2ea54602b3824041547b9c274ecbd2
b9ee0f32c5af6a6e2c21e3ed45c9a7df84e2b7f5c5f297983fccec81f360a2c7
46e82174e59ea72bec0db7f93b7206ab6000100b1d6ed22237a8ee5cb9a16d73
bec03244aa4b497c8f4f57c5a98b65555afa4256d5b22c5ddea04688652e468d
8ac2c3f63875d2698deee28c00e3b9ba3f4bd451ca5ac80d3e7b49b2aa336afc
0e4bfc04140d1bd99955a30710712e8b16a57b10da52ccc7b0f80606b78d641d
497b8a8f7a40144d7578ace295446b2b5dfa1635f6fce36eff7555ce24f3da5f
35e2272502cab61e58bed3c7a9331c091eaf57c9264ad7d429aab4097741baf5
bccfd28d88ec9622c9326d31d0eb86d1e0bbab44d8f67d46fa7412033d544571
86b45ac5bfad756447e2e7a098b8679406757f39c056b35d6a20c665739c5f04
1406200f2d40baf392a2f5bd93e4d1836f8285139e3fd1c08719c66f0081fe43
1e5b56aa4f666c5bd09571aae875d53a4bf73a14ea89f994c9f095feeb40fd87
16e6c65215bfda1d1d691d5a4edb1467a4cae45cd568a7f18f2b31e54f635a3d
1587df708933b807c5862f4782d7c9d36467a68328b45934adb1c6582f5862b3
d5f44c7b62401b0f2845a1283064fc5b6308b28a59c8e6ef51e44d43b3df8f67
73c562a1e119e0750153bb79b3a62cd876f5d5cdc01474e5d0bb8f4a48bc4466
ea73bbb1040bd01affd200a3c86534bfd7fa69f09dfa81046225c5a8c8f53a03
0a3968f721c3a21dd0f9fe44c72b6eafa3da5c9e211a6b1ad68ebf7b9256fc34
6c16950d58cf3af15d107875efc5ffab531577356b5a20fe4b5967c6ac6f872c
57883ceb64dda199cb
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
cleartomark
%%EndFont
TeXDict begin 40258431 52099146 1000 600 600 (completeness.dvi)
@start /Fa 212[51 43[{}1 58.1154 /CMR7 rf /Fb 196[95
7[67 65 50[{}3 83.022 /LASYB10 rf /Fc 197[47 58[{}1 66.4176
/CMSY8 rf /Fd 194[65 52[60 2[62 5[{}3 83.022 /CMR10 rf
/Fe 254[46 1[{}1 41.511 /CMR5 rf /Ff 194[74 61[{}1 83.022
/CMBX10 rf /Fg 149[27 9[58 38[53 53 56[{}4 83.022 /CMBSY10
rf /Fh 145[31 2[31 1[31 1[31 31 21[31 28[31 31 31 31
48[{}10 58.1154 /CMTT8 rf /Fi 160[55 55 43[55 8[83 19[65
3[65 17[{}6 83.022 /CMSY10 rf /Fj 207[19 48[{}1 58.1154
/CMSY7 rf /Fk 130[44 1[44 44 44 44 44 44 44 44 44 44
44 44 44 44 44 44 44 44 44 44 44 44 44 44 44 44 44 3[44
1[44 3[44 44 44 44 44 44 44 44 44 44 44 44 44 1[44 44
44 44 44 44 44 44 44 1[44 44 44 44 1[44 2[44 1[44 1[44
44 44 44 44 44 44 44 44 44 44 44 5[44 34[{}72 83.022
/CMTT10 rf /Fl 201[59 59 59 59 59 59 49[{}6 119.552 /CMR12
rf end
%%EndProlog
%%BeginSetup
%%Feature: *Resolution 600dpi
TeXDict begin
%%EndSetup
%%Page: 1 1
1 0 bop 3603 -177 115 4 v 3603 -50 4 127 v 3631 -75 a
Fl(1)p 3715 -50 V 3603 -47 115 4 v 448 -42 a Fk(A)43
b(COMPLETENESS)c(THEOREM)i(FOR)h(TLA)448 108 y(Preface:)f(A)i(Quick)e
(Introduction)e(to)k(TLA)448 183 y(-----------------)o(--)o(---)o(--)o
(---)o(--)o(--)o(---)o(--)o(-)448 332 y(Here)638 302
y Fj(0)666 332 y Fk(s)g(a)h(quick)d(and)h(dirty)g(informal)e
(definition)g(and)i(semantics)e(for)i(TLA.)448 432 y(A)h(more)f
(precise)f(one)h(is)h(given)f(later.)84 b(If)43 b(you)g(are)f(already)f
(familiar)448 531 y(with)h(the)h(new,)f(improved)e(TLA)i(\(defined)e(a)
k(little)d(differently)e(than)j(in)448 631 y(SRC)h(Report)e(No.)h(57\))
g(you)h(can)f(skip)g(to)h(the)f(Introduction.)448 780
y(Values:)448 855 y(I)h(assume)f(a)h(set)f(of)h(values,)e(big)h(enough)
f(to)i(contain)d(all)j(the)f(constants)448 955 y(of)h(interest.)84
b(It)42 b(includes)f(the)h(values)f(1,)i(TRUE,)e(NAT)i(\(the)f(set)g
(of)h(all)448 1054 y(naturals\),)d({n)d Fi(2)h Fk(NAT)k(:)h(n)g(a)h
(prime},)c(etc.)448 1204 y(State,)h(Variable:)448 1303
y(A)i(variable)e(is)i(something)c(that)j(assigns)f(a)i(value)f(to)g
(every)g(state.)85 b(I)43 b(let)448 1403 y(s.x,)f(denote)f(the)i(value)
e(state)h(s)h(assigns)e(to)h(variable)f(s.)86 b(Or)43
b(maybe)e(a)448 1503 y(state)h(s)h(is)g(something)d(that)i(assigns)e(a)
j(value)f(s.x)g(to)h(a)g(variable)d(x.)448 1602 y(Take)i(your)g(pick.)
448 1752 y(State)g(Function:)448 1851 y(An)h(expression)d(made)h(from)h
(variables)e(and)j(constants,)c(such)j(as)h(x)2977 1821
y Fh(2)3055 1851 y Fk(+)g(3*y.)448 1951 y(A)g(state)f(function)e(f)j
(assigns)e(a)i(value)f(s.f)g(to)h(every)e(state)h(s.)86
b(For)448 2032 y(example,)623 2181 y(s.\(x)799 2151 y
Fh(2)876 2181 y Fk(+3*y\))41 b(=)i(\(s.x\))1444 2151
y Fh(2)1521 2181 y Fk(+)g(3*\(s.y\).)448 2331 y(Predicate:)448
2405 y(A)g(boolean-valued)38 b(state)k(function--for)c(example,)928
2505 y(x)972 2475 y Fh(2)1050 2505 y Fk(<)43 b(3*y)448
2654 y(Action:)448 2729 y(A)g(Boolean)e(expression)f(involving)f
(variables,)h(primed)h(variables)f(and)448 2829 y(constants--for)e
(example,)i(x)k(+)f(1)g(<)g(2*y)1989 2799 y Fj(0)2017
2829 y Fk(.)87 b(An)43 b(action)e(maps)h(pairs)f(of)448
2928 y(states)g(to)i(Booleans.)84 b(Letting)40 b(s.A.t)i(denote)f(the)h
(value)g(that)g(action)f(A)448 3028 y(assigns)g(to)i(the)f(pair)g
(\(s,t\),)f(I)i(define)535 3177 y(s.\(x)f(+)i(1)f(<)g(2*y)1161
3147 y Fj(0)1189 3177 y Fk(\).t)86 b(=)43 b(\(s.x\))f(+)h(1)g(<)87
b(2*\(t.y\))448 3327 y(In)43 b(other)f(words,)f(the)h(unprimed)e
(variables)g(talk)i(about)g(the)g(left-hand)448 3426
y(state,)f(and)i(the)f(primed)f(variables)f(talk)i(about)g(the)g
(right-hand)d(state.)448 3526 y(Think)j(of)h(s.A.t)e(=)i(TRUE)f(as)h
(meaning)e(that)h(an)g(A-step)f(can)i(take)f(state)f(s)i(to)448
3626 y(state)f(t.)86 b(An)43 b(action)e(is)i(valid,)e(written)h
Fg(j)-16 b Ff(=)44 b Fk(A,)f(iff)f(s.A.t)g(is)h(true)f(for)448
3725 y(all)h(states)e(s)i(and)f(t.)448 3875 y(Enabled\(A\):)448
3951 y(For)h(any)f(action)f(A,)i(the)f(predicate)e(Enabled\(A\))g(is)i
(defined)f(by)579 4065 y(s.Enabled\(A\))1167 4018 y Fe(\001)1157
4065 y Fd(=)50 b Fg(9)39 b Fk(t)k(:)g(s.A.t)448 4214
y(f)506 4184 y Fj(0)535 4214 y Fk(=f:)448 4289 y(For)g(any)f(state)g
(function)e(f,)j(the)f(action)f(f)2119 4259 y Fj(0)2148
4289 y Fk(=f,)i(which)e(is)i(sometimes)448 4389 y(written)e
(Unchanged\(f\),)d(is)43 b(defined)e(by)535 4502 y(s.\(f)725
4472 y Fj(0)753 4502 y Fk(=f\).t)1079 4455 y Fe(\001)1070
4502 y Fd(=)98 b Fk(\(t.f\))41 b(=)j(\(s.f\))448 4726
y([A])580 4738 y Fh(f)614 4726 y Fk(:)448 4808 y(The)f(action)e([A])
1060 4820 y Fh(f)1137 4808 y Fk(is)i(defined)e(by)579
4922 y([A])711 4934 y Fh(f)809 4875 y Fe(\001)800 4922
y Fd(=)54 b Fk(A)59 b Fi(_)h Fk(\(f)1239 4892 y Fj(0)1268
4922 y Fk(=f\))448 5022 y(An)43 b([A])711 5034 y Fh(f)788
5022 y Fk(step)f(is)h(either)e(an)i(A)g(step)f(or)h(leaves)e(f)i
(unchanged.)448 5246 y()580 5258 y Fh(f)614 5246 y
Fk(:)448 5328 y(The)g(action)e()1060 5340 y Fh(f)1137
5328 y Fk(is)i(defined)e(by)579 5441 y()711 5453 y
Fh(f)809 5394 y Fe(\001)800 5441 y Fd(=)52 b Fc(:)o Fk([)n
Fc(:)n Fk(A])1138 5453 y Fh(f)p eop
%%Page: 2 2
2 1 bop 3603 -177 115 4 v 3603 -50 4 127 v 3631 -75 a
Fl(2)p 3715 -50 V 3603 -47 115 4 v 448 -42 a Fk(It)43
b(equals)e(A)59 b Fi(^)h Fk(\(f)1204 -72 y Fj(0)1233
-42 y Fk(=)-44 b(/)o(f\).)86 b(An)43 b()1757 -30 y
Fh(f)1835 -42 y Fk(step)e(is)i(an)g(A)g(step)f(that)g(changes)f(f.)448
183 y(The)i(Raw)f(Logic:)448 282 y(A)h(Raw)g(Logic)e(formula)g(is)i
(any)f(formula)f(made)h(from)g(actions)e(using)448 382
y(logical)h(operators)f(and)i(the)h(unary)52 b Fb(2)j
Fk(operator--for)38 b(example)623 531 y(A)59 b Fi(_)71
b Fb(2)11 b Fk(\(B)58 b Fi(^)71 b Fb(2)10 b Fc(:)f Fb(2)g
Fc(:)o Fk(A\))448 681 y(where)42 b(A)h(and)f(B)i(are)e(actions.)84
b(A)43 b(Raw)f(Logic)g(formula)e(is)j(a)g(Boolean-valued)448
780 y(function)e(on)h(infinite)f(sequences)e(of)k(states.)85
b(An)42 b(infinite)f(sequence)f(of)448 880 y(states)h(is)i(called)e(a)i
(BEHAVIOR.)84 b(An)43 b(action)e(A)i(is)g(interpreted)c(as)j(the)448
980 y(temporal)f(formula)f(asserting)g(that)i(first)g(step)g(of)g(the)h
(behavior)d(is)j(an)f(A)448 1079 y(step.)85 b(The)43
b(formula)52 b Fb(2)11 b Fk(A)43 b(asserts)d(that)i(every)g(step)g(is)h
(an)f(A)i(step.)85 b(In)448 1179 y(general,)41 b(let)h(s)1059
1191 y Fh(0)1094 1179 y Fk(,)h(s)1225 1191 y Fh(1)1259
1179 y Fk(,)h(...)87 b Fg(j)-16 b Ff(=)44 b Fk(F)f(denote)e(the)i
(value)e(that)h(formula)f(F)448 1279 y(assigns)g(to)i(the)f(sequence)e
(s)1538 1291 y Fh(0)1573 1279 y Fk(,)j(s)1704 1291 y
Fh(1)1739 1279 y Fk(,)g(....)85 b(The)43 b(semantics)d(of)i(Raw)h
(Logic)448 1378 y(formulas)e(is)h(defined)f(as)i(follows,)d(where)i(A)h
(is)g(any)f(action)f(and)h(F)h(and)g(G)448 1478 y(are)g(any)f
(formulas:)579 1636 y(s)623 1648 y Fh(0)658 1636 y Fk(,)h(s)789
1648 y Fh(1)823 1636 y Fk(,)h(s)955 1648 y Fh(2)989 1636
y Fk(,)f(...)h Fg(j)-16 b Ff(=)45 b Fk(A)1533 1589 y
Fe(\001)1524 1636 y Fd(=)54 b Fk(s)1687 1648 y Fh(0)1722
1636 y Fk(.A.s)1898 1648 y Fh(1)579 1736 y Fk(s)623 1748
y Fh(0)658 1736 y Fk(,)43 b(s)789 1748 y Fh(1)823 1736
y Fk(,)h(s)955 1748 y Fh(2)989 1736 y Fk(,)f(...)h Fg(j)-16
b Ff(=)56 b Fb(2)11 b Fk(F)774 1802 y Fe(\001)765 1849
y Fd(=)49 b Fg(8)39 b Fk(n)33 b Fi(\025)g Fk(0)43 b(:)g(s)1364
1861 y Fh(n)1399 1849 y Fk(,)g(s)1530 1861 y Fh(n)p Fa(+)p
Fh(1)1646 1849 y Fk(,)g(s)1777 1861 y Fh(n)p Fa(+)p Fh(2)1894
1849 y Fk(,)g(...)h Fg(j)-16 b Ff(=)44 b Fk(F)579 1963
y(s)623 1975 y Fh(0)658 1963 y Fk(,)f(s)789 1975 y Fh(1)823
1963 y Fk(,)h(s)955 1975 y Fh(2)989 1963 y Fk(,)f(...)h
Fg(j)-16 b Ff(=)43 b Fc(:)n Fk(F)1577 1916 y Fe(\001)1567
1963 y Fd(=)96 b Fc(:)o Fk(\(s)1862 1975 y Fh(0)1896
1963 y Fk(,)43 b(s)2027 1975 y Fh(1)2062 1963 y Fk(,)g(s)2193
1975 y Fh(2)2228 1963 y Fk(,)g(...)g Fg(j)-16 b Ff(=)45
b Fk(F\))579 2076 y(s)623 2088 y Fh(0)658 2076 y Fk(,)e(s)789
2088 y Fh(1)823 2076 y Fk(,)h(s)955 2088 y Fh(2)989 2076
y Fk(,)f(...)h Fg(j)-16 b Ff(=)45 b Fk(F)59 b Fi(_)g
Fk(G)1707 2029 y Fe(\001)1698 2076 y Fd(=)54 b Fk(etc.)448
2226 y(A)43 b(formula)e(F)i(is)g(valid,)e(written)h Fg(j)-16
b Ff(=)45 b Fk(F,)d(iff)h(it)g(is)f(true)g(for)h(all)448
2306 y(behaviors.)448 2530 y(TLA:)448 2605 y(The)g(Raw)f(Logic)g(is)g
(wonderfully)d(simple,)i(but)h(it)h(is)g(too)f(expressive.)83
b(It)448 2705 y(allows)41 b(you)i(to)g(assert)e(that)h(something)d(is)k
(true)f(of)h(the)f(next)g(state,)448 2804 y(which)g(ruins)f(any)i
(effort)e(to)i(heierarchically)37 b(refine)k(programs.)83
b(We)448 2904 y(define)41 b(TLA)i(to)g(be)f(the)h(subset)e(of)h(Raw)h
(Logic)e(formulas)g(obtained)f(by)448 3004 y(application)f(of)54
b Fb(2)h Fk(and)42 b(logical)f(operators)f(starting)g(not)i(from)g
(arbitrary)448 3103 y(actions,)f(but)h(from)g(predicates)d(and)k
(actions)d(of)j(the)f(form)g([A])2890 3115 y Fh(f)2924
3103 y Fk(.)87 b(For)448 3184 y(example:)623 3333 y(P)45
b Fi(\))f Fc(:)9 b Fb(2)h Fc(:)f Fb(2)i Fk([A])1234 3345
y Fh(f)1327 3333 y Fi(_)71 b Fb(2)11 b Fk(\(Q)45 b Fi(\))57
b Fb(2)11 b Fk([B])2010 3345 y Fh(g)2044 3333 y Fk(\))448
3483 y(Observe)41 b(that)53 b Fb(2)11 b Fk([A])1234 3495
y Fh(f)1311 3483 y Fk(asserts)41 b(that)h(every)g(step)g(is)g(either)f
(an)i(A)g(step)448 3582 y(or)g(else)f(leaves)f(f)i(unchanged.)448
3732 y(As)g(is)g(usual)e(in)i(temporal)d(logic,)h(we)i(define)51
b Fb(3)j Fk(and)38 b Fb(;)i Fk(by)546 3890 y Fb(3)10
b Fk(F)731 3843 y Fe(\001)721 3890 y Fd(=)53 b Fc(:)9
b Fb(2)h Fc(:)n Fk(F)535 4004 y(F)40 b Fb(;)f Fk(G)861
3956 y Fe(\001)852 4004 y Fd(=)66 b Fb(2)11 b Fk(\(F)44
b Fi(\))57 b Fb(2)11 b Fk(G\))448 4153 y(The)43 b(Raw)f(formula)51
b Fb(3)10 b Fk(A)43 b(is)g(a)g(TLA)f(formulas)f(iff)h(A)h(is)g(a)g
(predicate)d(or)j(an)448 4253 y(action)e(of)i(the)g(form)51
b Fb(3)11 b Fk()1496 4265 y Fh(f)1529 4253 y Fk(.)448
4402 y(Technical)40 b(point.)85 b(Since)53 b Fb(2)11
b Fk(F)59 b Fi(^)71 b Fb(2)11 b Fk(G)43 b(=)54 b Fb(2)11
b Fk(\(F)59 b Fi(^)h Fk(G\))42 b(holds)g(for)g(any)h(F)g(and)448
4502 y(G,)g(it)681 4472 y Fj(0)710 4502 y Fk(s)g(convenient)c(to)k(let)
g(TLA)f(include)f(formulas)f(of)j(the)f(form)460 4601
y Fb(2)10 b Fk(\(P)59 b Fi(^)71 b Fb(2)11 b Fk([A])1016
4613 y Fh(f)1050 4601 y Fk(\))43 b(where)f(P)h(is)g(a)g(predicate.)448
4825 y(Introduction)448 4900 y(------------)448 5050
y(This)f(is)h(a)g(relative)d(completeness)f(proof)j(for)g(TLA,)g(a)h
(la)g(Cook.)85 b(It)43 b(is)448 5149 y(not)g(a)g(completeness)38
b(result)k(for)g(all)g(of)h(TLA,)f(just)g(for)g(the)h(class)e(of)448
5249 y(formulas)g(that)h(one)g(is)h(interested)c(in)k(proving.)84
b(The)42 b(formulas)e(we)3078 5219 y Fj(0)3107 5249 y
Fk(re)448 5349 y(interested)g(in)j(are)f(of)h(the)f(form)579
5498 y(Program)h Fi(\))j Fk(Property)p eop
%%Page: 3 3
3 2 bop 3603 -177 115 4 v 3603 -50 4 127 v 3631 -75 a
Fl(3)p 3715 -50 V 3603 -47 115 4 v 448 33 a Fk(A)43 b(Program)e(has)i
(the)f(form)535 183 y(P)60 b Fi(^)71 b Fb(2)11 b Fk([A])973
195 y Fh(f)1066 183 y Fi(^)60 b Fk(Fairness)448 332 y(for)43
b(P)g(a)g(predicate.)83 b(So)43 b(far,)f(all)g(the)g(Fairness)f
(conditions)e(have)448 432 y(have)j(been)g(conjunctions)d(of)k(the)f
(form)g(SF)2062 444 y Fh(f)2096 432 y Fk(\(B\))g(or)h(WF)2489
444 y Fh(f)2523 432 y Fk(\(B\),)f(where)448 531 y(B)h(implies)e(A)i
(and)535 690 y(WF)623 702 y Fh(f)658 690 y Fk(\(B\))853
643 y Fe(\001)843 690 y Fd(=)66 b Fb(2)21 b(3)10 b Fk()1269
702 y Fh(f)1362 690 y Fi(_)71 b Fb(2)21 b(3)9 b Fc(:)n
Fk(Enabled\()2179 702 y Fh(f)2210 690 y Fk(\))535
803 y(SF)623 815 y Fh(f)658 803 y Fk(\(B\))853 756 y
Fe(\001)843 803 y Fd(=)66 b Fb(2)21 b(3)10 b Fk()1269
815 y Fh(f)1362 803 y Fi(_)70 b Fb(3)22 b(2)9 b Fc(:)n
Fk(Enabled\()2179 815 y Fh(f)2210 803 y Fk(\))448
953 y(The)43 b(theorem)d(allows)h(the)i(more)f(general)e(class)i(of)h
(programs)d(in)j(which)448 1052 y(Fairness)e(is)h(the)h(conjunction)c
(of)j(formulas)f(of)i(the)f(form)590 1202 y Fb(2)21 b(3)9
b Fc(:)n Fk(TACT)58 b Fi(_)70 b Fb(3)21 b(2)11 b Fk(TACT)86
b(or)54 b Fb(2)21 b(3)8 b Fc(:)n Fk(TACT)58 b Fi(_)71
b Fb(2)21 b(3)10 b Fk(TACT,)448 1351 y(where)42 b(TACT)g(denotes)e(any)
j(formula)d(of)j(the)g(form)f(Q)59 b Fi(^)g Fk([B])2672
1363 y Fh(g)2706 1351 y Fk(,)43 b(so)e Fc(:)o Fk(TACT)h(is)448
1451 y(a)h(formula)e(of)i(the)f(form)g(Q)59 b Fi(_)h
Fk()1757 1463 y Fh(g)1791 1451 y Fk(.)87 b(The)42
b(Fairness)e(formula)h(must)448 1550 y(satisfy)g(the)h(additional)e
(requirement)f(that)j(program)e(is)j(machine)e(closed,)448
1650 y(meaning)g(that)h(for)g(any)h(safety)e(property)f(S:)535
1799 y(If)k Fg(j)-16 b Ff(=)45 b Fk(\(P)59 b Fi(^)71
b Fb(2)11 b Fk([A])1278 1811 y Fh(f)1371 1799 y Fi(^)60
b Fk(Fairness\))42 b Fi(\))j Fk(S)535 1899 y(then)f Fg(j)-16
b Ff(=)44 b Fk(\(P)59 b Fi(^)71 b Fb(2)11 b Fk([A])1365
1911 y Fh(f)1399 1899 y Fk(\))45 b Fi(\))h Fk(S)448 2048
y(\(The)c(theorem)f(requires)f(this)i(only)g(when)g(S)h(is)g(of)g(the)f
(form)53 b Fb(2)11 b Fk(TACT.\))448 2148 y(Machine)41
b(closure,)f(which)i(was)g(called)f("feasibility")d(by)43
b(Apt,)f(Francez,)448 2248 y(and)h(Katz,)e(is)i(a)g(reasonable)d
(requirement)f(for)j(any)g(fairness)f(condition.)448
2347 y(It)i(can)f(be)h(argued)e(that)h(a)h(condition)d(not)j
(satisfying)c(it)k(is)g(not)f(a)448 2447 y(fairness)f(condition,)e
(since)j(it)g(can)1858 2417 y Fj(0)1887 2447 y Fk(t)h(be)g(implemented)
c(by)j(a)i(memory-less)448 2528 y(scheduler.)448 2677
y(The)f(Property)d(can)i(have)g(any)h(of)f(the)h(following)d(forms:)535
2826 y(Predicate)547 2926 y Fb(2)11 b Fk(Predicate)535
3026 y(Predicate)36 b Fb(;)k Fk(Predicate)535 3125 y(GeneralProgram)448
3275 y(where)i(a)h(GeneralProgram)38 b(is)43 b(like)e(a)j(Program,)c
(except)h(without)g(the)448 3374 y(machine-closure)d(requirement)h(on)j
(its)h(fairness)d(condition.)83 b(The)42 b(absence)448
3474 y(of)h(this)f(requirement)d(is)k(important,)c(for)k(the)f
(following)e(reason.)84 b(To)448 3574 y(prove)42 b(that)g(program)31
b Fd(\005)1320 3586 y Fh(1)1399 3574 y Fk(implements)39
b(program)31 b Fd(\005)2270 3586 y Fh(2)2305 3574 y Fk(,)44
b(one)e(proves)439 3673 y Fd(\005)492 3685 y Fh(1)573
3673 y Fi(\))37 b Fd(\010)745 3685 y Fh(2)780 3673 y
Fk(,)43 b(where)33 b Fd(\010)1172 3685 y Fh(2)1251 3673
y Fk(is)43 b(obtained)d(from)32 b Fd(\005)2035 3685 y
Fh(2)2114 3673 y Fk(by)448 3773 y(substituting)39 b(state)i(functions)f
(for)j(variables.)83 b(This)42 b(substitution)448 3873
y(preserves)e(the)j(form)e(of)i(the)g(formula)31 b Fd(\005)1974
3885 y Fh(2)2009 3873 y Fk(,)43 b(but)f(can)h(destroy)448
3953 y(machine-closure.)448 4103 y(Proving)e(relative)f(completeness)f
(for)j(safety)f(properties)f(in)j(TLA)f(is)448 4202 y(pretty)f(much)h
(the)h(same)f(as)g(proving)f(it)i(for)f(the)h(Floyd/Hoare)c(method.)84
b(The)448 4302 y(completeness)39 b(results)i(for)h(Hoare)1772
4272 y Fj(0)1799 4302 y Fk(s)i(method)d(assumes)f(the)j(expressibility)
448 4401 y(of)g(the)f(predicate)e(sp\(S,)i(P\))h(for)f(program)f
(statements)e(S)k(and)g(predicates)448 4501 y(P,)g(where)f(sp)g(is)h
(the)f(strongest)e(postcondition)f(operator.)83 b(Assuming)40
b(such)448 4601 y(predicates)g(for)i(arbitrary)e(statements)f(S,)k
(which)f(include)e(loops)i(or)448 4700 y(recursion,)e(is)j(equivalent)c
(to)k(assuming)d(the)i(expressibility)c(of)43 b(sp\(A,)e(P\))448
4800 y(and)i(sin\(A,)e(P\))i(for)f(atomic)f(actions)g(A,)h(where)g(sin)
g(is)h(the)f(strongest)448 4900 y(invariant)e(operator.)448
5049 y(Proving)h(relative)f(completeness)f(for)j(liveness)f(is)h
(somewhat)f(trickier.)448 5149 y(It)i(requires)d(induction)g(over)i
(well-founded)d(sets.)85 b(Taking)41 b(a)i(simple,)448
5248 y(intuitive)d(approach)g(leads)i(to)h(a)g(result)e(whose)h
(practical)d(interest)i(is)448 5348 y(rather)g(doubtful.)84
b(For)42 b(example,)e(Mann)i(and)h(Pnueli)e(\("Completing)d(the)448
5448 y(Temporal)j(Picture"\))e(use)k(the)f(axiom)g(of)g(choice)g(to)g
(pull)g(a)h(well-founded)p eop
%%Page: 4 4
4 3 bop 3603 -177 115 4 v 3603 -50 4 127 v 3631 -75 a
Fl(4)p 3715 -50 V 3603 -47 115 4 v 448 -42 a Fk(ordering)41
b(on)h(the)h(state)e(space)h(out)g(of)h(a)g(hat.)86 b(Such)41
b(a)j(construction)448 58 y(requires)d(the)h(assumption)d(that)j(every)
g(semantic)e(predicate)g(is)448 158 y(syntactically)f(expressible.)448
307 y(Getting)i(the)h(precise)f(expressibility)d(assumptions,)g(and)43
b(avoiding)448 407 y(mistakes,)d(required)g(a)k(careful)c(formal)h
(exposition.)448 631 y(The)i(Assumptions)448 706 y(---------------)448
780 y(In)g(relative)d(completeness)f(results)i(for)h(Hoare)g(logic,)f
(one)h(assumes)f(a)448 880 y(complete)g(system)g(for)h(reasoning)e
(about)h(predicates.)83 b(In)43 b(TLA,)f(all)g(the)448
980 y(serious)f(reasoning)f(is)j(in)f(the)h(domain)e(of)i(actions.)83
b(So,)43 b(we)g(assume)e(a)448 1079 y(complete)g(system)g(for)h
(reasoning)e(about)h(actions.)84 b(More)42 b(precisely,)448
1179 y(letting)55 b Fg(`)k Fk(denote)41 b(provability,)d(we)43
b(assume)e(a)j(set)e(ACT)g(of)h(expressible)448 1279
y(actions)e(such)h(that)g(\()q Fg(j)-16 b Ff(=)44 b Fk(A\))h
Fi(\))h Fk(\()14 b Fg(`)58 b Fk(A\))43 b(for)f(any)h(action)e(A)i(in)g
(ACT.)e(There)448 1378 y(are)i(various)d(simple)h(assumptions)e(about)j
(ACT--such)e(as)j(its)f(being)f(closed)448 1478 y(under)h(boolean)f
(operations.)82 b(Let)42 b(PRED)g(denote)g(the)g(set)g(consisting)e(of)
448 1577 y(all)j(predicates)c(in)k(ACT)f(\(remember)e(that)i(a)h
(predicate)d(is)j(an)g(action)e(that)448 1677 y(doesn)682
1647 y Fj(0)710 1677 y Fk(t)i(mention)e(unprimed)f(variables\).)83
b(The)42 b(least)f(reasonable)448 1777 y(assumption)f(is)j(that)e(for)i
(any)f(P)h(in)g(PRED)f(and)g(A)i(in)e(ACT,)g(sin\(A,)f(P\))i(and)448
1876 y(sp\(A,)f(P\))h(are)f(in)h(PRED.)e(Of)i(course,)e(this)h
(assumption)d(is)k(what)f(really)448 1976 y(puts)g(the)h("relative")c
(in)k("relative)d(completeness".)448 2125 y(The)j(relatively)c
(complete)h(logical)h(system)g(consists)f(of)j(the)g(following:)448
2275 y(1.)g(The)f(usual)g(assortment)d(of)k(simple)e(propositional)d
(temporal)j(logic)579 2374 y(rules)h(and)g(axioms)f(that)h(you)1684
2344 y Fj(0)1712 2374 y Fk(d)h(expect,)e(since)h(TLA)g(includes)579
2474 y(simple)f(temporal)f(logic)i(\(the)g(logic)f(that)2207
2444 y Fj(0)2235 2474 y Fk(s)j(the)e(same)g(as)h(the)f(Raw)579
2574 y(Logic)g(except)f(starting)f(with)i(predicates,)d(not)j
(arbitrary)e(actions\).)448 2723 y(2.)j(An)g(induction)d(principle,)f
(which)j(is)g(what)g(you)2381 2693 y Fj(0)2410 2723 y
Fk(d)h(expect)e(for)h(any)579 2823 y(relatively)e(complete)g(system)h
(for)h(proving)f(temporal)f(logic)579 2922 y(liveness)g(properties.)448
3072 y(3.)j(The)f(two)h(TLA)f(axioms:)724 3221 y Fg(`)59
b Fk(\()11 b Fb(2)f Fk(P)33 b Fi(\021)g Fk(P)59 b Fi(^)71
b Fb(2)11 b Fk([P)45 b Fi(\))g Fk(P)1770 3191 y Fj(0)1799
3221 y Fk(])1843 3233 y Fh(P)1878 3221 y Fk(\))724 3371
y Fg(`)15 b Fk(\(A)45 b Fi(\))h Fk(B\))88 b Fi(\))104
b Fg(`)14 b Fk(\()d Fb(2)g Fk(A)45 b Fi(\))57 b Fb(2)11
b Fk(B\))579 3520 y(where)42 b(P)h(is)g(a)g(predicate,)c(and)j(A)i(and)
e(B)h(are)g(actions)d(of)j(the)f(form)579 3620 y(P)59
b Fi(^)h Fk([A])929 3632 y Fh(f)963 3620 y Fk(.)448 3769
y(The)43 b(axioms)e(of)i(3)g(are)f(the)g(only)g(ones)g(that)g(mention)f
(actions.)84 b(The)42 b(axioms)448 3869 y(of)h(1)g(only)f(mention)f
(arbitrary)f(formulas,)g(and)i(the)g(induction)e(principle)448
3968 y(of)j(2)g(talks)f(only)g(about)f(predicates.)83
b(These)41 b(axioms)g(are)i(actually)d(valid)448 4068
y(for)j(the)f(Raw)g(logic,)f(and)i(in)g(that)e(logic)h(the)g(second)f
(axiom)h(of)h(3)448 4168 y(is)g(a)g(special)e(case)h(of)h(the)f(axiom)
681 4317 y Fg(`)58 b Fk(\(F)45 b Fi(\))h Fk(G\))88 b
Fi(\))104 b Fg(`)58 b Fk(\()11 b Fb(2)g Fk(F)45 b Fi(\))57
b Fb(2)11 b Fk(G\))448 4467 y(from)42 b(1,)h(for)f(arbitrary)e
(formulas)g(F)k(and)e(G.)h(However,)d([A])2716 4479 y
Fh(f)2795 4467 y Fi(\))46 b Fk([B])3056 4479 y Fh(g)448
4566 y Fk(isn)594 4536 y Fj(0)623 4566 y Fk(t)d(a)g(TLA)f(formula)f
(\(it)1466 4536 y Fj(0)1494 4566 y Fk(s)j(a)f(formula)d(in)j(the)g
(logic)e(of)i(actions,)d(but)448 4666 y(not)j(in)f(TLA\),)g(so)h(the)f
(second)f(axiom)h(of)g(3)i(is)e(needed)f(if)i(you)g(want)e(to)i(do)448
4765 y(all)g(your)f(reasoning)d(completely)h(within)h(TLA.)448
4915 y(The)i(induction)d(axiom)h(2)i(is)g(tricky)e(enough)g(to)i(be)g
(worth)e(mentioning.)83 b(To)448 5015 y(get)43 b(it)f(right,)g(we)g
(first)g(have)g(to)g(generalize)e(everything)f(to)k(include)448
5114 y(logical)e(variables.)83 b(If)43 b(you)f(want)g(to)h(describe)d
(an)j(n-process)d(algorithm)448 5214 y(with)i(a)h(TLA)g(formula,)d(for)
i(an)h(arbitrary)d(but)i(fixed)g(n,)h(then)f(n)h(is)f(a)448
5313 y(logical)f(variable)f(of)j(the)f(formula.)84 b(A)43
b(logical)e(variable)f(represents)g(an)448 5413 y(unspecified)f(value)j
(that)g(is)h(the)f(same)g(for)g(all)h(states)e(of)h(a)i(behavior.)448
5513 y(In)f(the)f(semantics)e(of)j(actions)e(and)h(TLA)g(formulas,)e
(Booleans)h(have)g(to)i(be)p eop
%%Page: 5 5
5 4 bop 3603 -177 115 4 v 3603 -50 4 127 v 3631 -75 a
Fl(5)p 3715 -50 V 3603 -47 115 4 v 448 -42 a Fk(replaced)41
b(by)h(Boolean-valued)c(formulas)i(involving)g(logical)h(variables.)448
58 y(\(Formally,)f(Booleans)g(become)h(boolean-valued)d(functions)i(on)
448 158 y(interpretations,)d(where)42 b(an)h(interpretation)37
b(is)43 b(an)g(assignment)c(of)k(values)448 257 y(to)g(all)f(logical)f
(variables.\))e(Logical)i(variables)f(pop)i(up)h(all)f(the)g(time)448
357 y(when)g(you)h(use)f(TLA)g(in)h(practice.)83 b(For)43
b(example,)d(if)j(you)f(have)g(a)448 457 y(distributed)d(algorithm)h
(with)i(a)h(set)g(Node)f(of)g(nodes,)f(then)h(Node)g(is)h(a)448
556 y(logical)e(variable.)83 b(In)43 b(fact,)f(if)g(you)h(go)g(really)e
(overboard)f(in)448 656 y(formalism--as)f(you)j(must)g(to)h(verify)e
(things)g(mechanically--th)o(en)448 756 y(everything)f(that)1118
725 y Fj(0)1146 756 y Fk(s)j(not)f(a)h(program)e(variable)f(\(the)i
(kind)g(of)h(variable)d(I)448 855 y(first)i(talked)f(about\))g(or)i(a)g
(logical)e(operator)f(is)j(a)g(logical)e(variable.)448
955 y(In)i(the)f(expression)e(x)j(+)g(3,)g(the)f(+)h(and)g(the)f(3)h
(are)g(logical)d(variables.)83 b(We)448 1054 y(just)42
b(happen)f(to)i(have)f(a)h(lot)g(of)f(axioms)f(about)h(the)g(logical)f
(variables)f(+)448 1154 y(and)j(3,)f(such)g(as)h(1+1+1)f(=)h(3,)g
(while)e(we)i(have)f(just)g(a)h(few)f(axioms)f(about)h(the)448
1254 y(logical)f(variable)f(n)j(\(for)f(example)f(n)c
Fi(2)h Fk(NAT,)k(n)i(>)f(0\).)448 1403 y(But,)f(I)h(digress.)84
b(I)43 b(was)g(talking)d(about)i(the)g(induction)e(principle.)83
b(An)448 1503 y(induction)40 b(principle)g(involves)g(induction)g(over)
i(a)h(well-founded)c(ordering)448 1602 y(on)k(a)g(set.)86
b(Intuitively,)38 b(a)44 b(well-founded)38 b(ordering)i(on)j(a)g(set)g
(S)g(is)g(a)448 1702 y(relation)e(>)i(such)f(that)g(there)f(does)h(not)
g(exist)g(an)h(infinite)d(sequence)448 1802 y(c)492 1814
y Fh(1)571 1802 y Fk(>)j(c)702 1814 y Fh(2)780 1802 y
Fk(>)g(c)911 1814 y Fh(3)989 1802 y Fk(>)g(...)86 b(.)h(More)42
b(precisely,)579 1951 y(Well-Founded\(>,)37 b(S\))731
2017 y Fe(\001)721 2064 y Fd(=)53 b Fc(:)37 b Fg(8)i
Fk(i)k(:)g(\(i)37 b Fi(2)h Fk(NAT\))44 b Fi(\))1359 2164
y Fg(9)39 b Fk(c)1495 2176 y Fh(i)1573 2164 y Fk(:)k(\(c)1748
2176 y Fh(i)1820 2164 y Fi(2)38 b Fk(S\))59 b Fi(^)h
Fk(\(c)2263 2176 y Fh(i)2340 2164 y Fk(>)44 b(c)2472
2176 y Fh(i)p Fa(+)p Fh(1)2588 2164 y Fk(\))448 2314
y(But,)e(what)g(does)g(this)g(formula)f(mean?)85 b(For)42
b(me,)h(the)f(most)g(sensible)e(way)i(to)448 2413 y(interpret)e(it)j
(as)g(a)g(logical)e(formula)f(is)j(to)g(rewrite)d(it)j(as)579
2563 y(Well-Founded\(v)38 b(>)43 b(w,)g(S\))731 2629
y Fe(\001)721 2676 y Fd(=)93 b Fg(8)39 b Fk(c)44 b(:)d
Fc(:)c Fg(8)i Fk(i)k(:)g(\(i)37 b Fi(2)h Fk(NAT\))44
b Fi(\))1799 2776 y Fk(\(c\(i\))36 b Fi(2)i Fk(S\))59
b Fi(^)h Fk(\(c\(i\))41 b(>)i(c\(i+1\)\))448 2925 y(where)f(v)h(>)g(w)g
(is)g(a)g(formula)e(with)h(free)g(logical)f(variables)e(v)44
b(and)e(w,)h(and)448 3025 y(\(c\(i\))f(>)h(ci+1\)\))e(is)i(the)f
(formula)f(obtained)f(by)j(substituting)c(c\(i\))i(for)i(v)448
3124 y(and)g(c\(i+1\))e(for)h(w)h(in)g(the)f(formula)f(v)i(>)g(w.)87
b(This)42 b(is)g(a)i(higher-order)448 3224 y(formula,)d(involving)e
(quantification)f(over)k(a)h(function)e(symbol)g(c.)448
3373 y(The)i(completeness)38 b(result)j(requires,)f(as)j(an)g
(assumption,)c(that)j(if)g(the)448 3473 y(formulas)f("v)h(>)i(w")e(and)
h("v)37 b Fi(2)h Fk(S")k(are)h(expressible,)38 b(then)448
3573 y(Well-Founded\(v)g(>)43 b(w,)g(S\))g(is)g(provable)d(if)j(it)2207
3543 y Fj(0)2235 3573 y Fk(s)h(true.)85 b(I)43 b(think)e(that)h(if)448
3672 y(you)h(look)f(closely)e(at)j(Manna)f(and)g(Pnueli)2034
3642 y Fj(0)2061 3672 y Fk(s)h(paper,)e(you)2599 3642
y Fj(0)2628 3672 y Fk(ll)h(find)g(that)g(they)448 3772
y(are)h(implicitly)c(assuming)h(this)i(for)h(any)f(formula)f("v)h(>)i
(w"--not)c(just)i(for)448 3872 y(an)h(expressible)c(one.)448
4021 y(Anyway,)i(the)h(actual)f(temporal)g(induction)f(principle)f
(looks)j(as)h(follows,)448 4121 y(where)f(P\(w\))g(denotes)e(a)k
(formula)c(containing)g(w)j(as)g(free)f(logical)448 4220
y(variables,)e(P\(v\))i(denotes)e(the)j(result)e(of)i(substituting)38
b(v)43 b(for)g(w,)f(and)h(F)448 4320 y(is)g(an)g(arbitrary)d(temporal)g
(formula.)623 4469 y(If)57 b Fg(`)c(9)39 b Fk(w)f Fi(2)g
Fk(S)753 4569 y(w)44 b(not)e(free)g(in)h(F)768 4669 y
Fg(`)58 b Fk(Well-Founded\(>,)38 b(S\))768 4768 y Fg(`)58
b Fk(\(F)h Fi(^)h Fk(w)37 b Fi(2)h Fk(S)1017 4868 y Fi(\))46
b Fk(\(P\(w\))37 b Fb(;)e Fg(9)k Fk(v)k(:)g(\(v)37 b
Fi(2)h Fk(S\))59 b Fi(^)h Fk(\(w)43 b(>)g(v\))59 b Fi(^)g
Fk(P\(v\)\)\))623 4967 y(then)d Fg(`)h Fc(:)n Fk(F)448
5117 y(I)506 5087 y Fj(0)535 5117 y Fk(ve)43 b(actually)e(lied)g(a)j
(bit.)85 b(I)43 b(assume)e(this)h(rule)g(when)g(w)h(is)g(a)g(k-tuple)
448 5217 y(of)g(distinct)d(logical)h(variables,)e(and)k(I)g(assume)e
(the)h(provability)d(only)j(of)448 5316 y(Well-Founded\(v)c(>)43
b(w,)g(VAL)1452 5286 y Fh(k)1486 5316 y Fk(\),)g(where)e(v)i(>)g(w)h
(is)e(an)h(expressible)c(formula)448 5416 y(and)k(VAL)755
5386 y Fh(k)832 5416 y Fk(denotes)e(the)h(set)g(of)h(k-tuples)d(of)j
(values.)84 b(I)44 b(could)d(have)h(done)p eop
%%Page: 6 6
6 5 bop 3603 -177 115 4 v 3603 -50 4 127 v 3631 -75 a
Fl(6)p 3715 -50 V 3603 -47 115 4 v 448 -42 a Fk(it)43
b(the)f(other)g(way)g(by)h(making)e(a)i(few)g(more)f(expressibility)448
58 y(assumptions--such)37 b(as)43 b(assuming)d(that)i("v)37
b Fi(2)h Fk(VAL)2324 28 y Fh(k)2358 58 y Fk(")43 b(is)448
158 y(expressible--but)37 b(I)43 b(think)f(that)g(would)f(have)h(been)g
(a)h(little)f(more)448 238 y(complicated.)p eop
%%Trailer
end
userdict /end-hook known{end-hook}if
%%EOF