%PDF-1.4 % 3 0 obj << /pgfprgb [/Pattern /DeviceRGB] >> endobj 8 0 obj << /S /GoTo /D (Outline0.1) >> endobj 11 0 obj (The Model Checking Modulo Theories Environment) endobj 12 0 obj << /S /GoTo /D (Outline0.2) >> endobj 15 0 obj (Automating Termination) endobj 16 0 obj << /S /GoTo /D [17 0 R /Fit ] >> endobj 41 0 obj << /Length 1215 /Filter /FlateDecode >> stream xXKo7WTH@p)#)\4rJzp%նkIqc^.fJ&@l#x+äe7 ;|:z䒥n.X:wZeB04"0Pj5찳=:7F"KKz0ŕwJ1L aHkA'Q9ԧ?$Bl"x GsN|@O0o>_@}9E$#`<+}$4JSAg[SPD}$ c1ґ!/.ÂYJd+}Cs(EAjj[M(BNHEZwңpbe3TȔ>oWۥk}Uy`Qa1`4"`Vn>G0\+2/VKjzZlsEN0svYuNe"Åi{DXڒ}^)Z8v-w{l>]t ۻ{^[,k]˦;zzrH@]p1:URJ.$pQQSul=((*ُrA?7I+._é|WS&\:VAuE W
k)9ϲ}E4ڦD6د<$ Km 4M
m`IBK IsAŎeVgw&gcbǏ*/F \x0i;0ǒ{~{EܶXEsqf7wZSs;O$vZIE9u./I8Mڬ+-cSJ&=i?,٫+=6mq[%2]e`>R9%*ワY'c}w.-$.lzT1t<ƇH1rpE3>؍G1<@#Omz_{PJa<;m N~;6X+$4(?/1y
endstream
endobj
17 0 obj <<
/Type /Page
/Contents 41 0 R
/Resources 40 0 R
/MediaBox [0 0 362.835 272.126]
/Trans << /S /R >>
/Parent 47 0 R
/Annots [ 19 0 R 20 0 R 21 0 R 22 0 R 23 0 R 24 0 R 25 0 R 26 0 R 27 0 R 28 0 R 29 0 R 30 0 R 31 0 R 32 0 R 33 0 R 34 0 R 35 0 R 36 0 R 37 0 R 38 0 R 39 0 R ]
>> endobj
19 0 obj <<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/N/C[.5 .5 .5]
/Rect [233.913 11.157 241.883 20.621]
/A << /S /GoTo /D (Navigation1) >>
>> endobj
20 0 obj <<
/Type /Annot
/Border[0 0 0]/H/N/C[1 0 0]
/Rect [239.891 11.157 249.853 20.621]
/Subtype/Link/A<>
>> endobj
21 0 obj <<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/N/C[.5 .5 .5]
/Rect [247.861 11.157 255.831 20.621]
/A << /S /GoTo /D (Navigation2) >>
>> endobj
22 0 obj <<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/N/C[.5 .5 .5]
/Rect [254.946 11.157 261.92 20.621]
/A << /S /GoTo /D (Navigation1) >>
>> endobj
23 0 obj <<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/N/C[.5 .5 .5]
/Rect [259.927 11.157 266.901 20.621]
/A << /S /GoTo /D (Navigation1) >>
>> endobj
24 0 obj <<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/N/C[.5 .5 .5]
/Rect [264.909 11.157 271.883 20.621]
/A << /S /GoTo /D (Navigation1) >>
>> endobj
25 0 obj <<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/N/C[.5 .5 .5]
/Rect [269.89 11.157 276.864 20.621]
/A << /S /GoTo /D (Navigation2) >>
>> endobj
26 0 obj <<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/N/C[.5 .5 .5]
/Rect [275.979 11.157 282.953 20.621]
/A << /S /GoTo /D (Navigation1) >>
>> endobj
27 0 obj <<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/N/C[.5 .5 .5]
/Rect [280.96 11.157 287.934 20.621]
/A << /S /GoTo /D (Navigation1) >>
>> endobj
28 0 obj <<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/N/C[.5 .5 .5]
/Rect [285.942 11.157 292.916 20.621]
/A << /S /GoTo /D (Navigation1) >>
>> endobj
29 0 obj <<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/N/C[.5 .5 .5]
/Rect [290.923 11.157 297.897 20.621]
/A << /S /GoTo /D (Navigation2) >>
>> endobj
30 0 obj <<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/N/C[.5 .5 .5]
/Rect [297.012 11.157 303.986 20.621]
/A << /S /GoTo /D (Navigation1) >>
>> endobj
31 0 obj <<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/N/C[.5 .5 .5]
/Rect [301.994 11.157 308.967 20.621]
/A << /S /GoTo /D (Navigation1) >>
>> endobj
32 0 obj <<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/N/C[.5 .5 .5]
/Rect [306.975 11.157 313.949 20.621]
/A << /S /GoTo /D (Navigation1) >>
>> endobj
33 0 obj <<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/N/C[.5 .5 .5]
/Rect [311.956 11.157 318.93 20.621]
/A << /S /GoTo /D (Navigation2) >>
>> endobj
34 0 obj <<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/N/C[.5 .5 .5]
/Rect [318.045 11.157 329.004 20.621]
/A << /S /GoTo /D (Navigation1) >>
>> endobj
35 0 obj <<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/N/C[.5 .5 .5]
/Rect [327.012 11.157 339.963 20.621]
/A << /S /GoTo /D (Navigation89) >>
>> endobj
36 0 obj <<
/Type /Annot
/Border[0 0 0]/H/N/C[1 0 0]
/Rect [339.078 11.157 348.045 20.621]
/Subtype/Link/A<>
>> endobj
37 0 obj <<
/Type /Annot
/Border[0 0 0]/H/N/C[1 0 0]
/Rect [346.052 11.157 354.022 20.621]
/Subtype/Link/A<>
>> endobj
38 0 obj <<
/Type /Annot
/Border[0 0 0]/H/N/C[1 0 0]
/Rect [352.03 11.157 360.996 20.621]
/Subtype/Link/A<>
>> endobj
39 0 obj <<
/Type /Annot
/Subtype /Link
/Border[0 0 0]/H/N/C[.5 .5 .5]
/Rect [144.715 0.8 218.114 8.382]
/A << /S /GoTo /D (Navigation89) >>
>> endobj
42 0 obj <<
/D [17 0 R /XYZ 10.909 261.966 null]
>> endobj
45 0 obj <<
/D [17 0 R /XYZ 351.926 0 null]
>> endobj
46 0 obj <<
/D [17 0 R /XYZ 351.926 0 null]
>> endobj
40 0 obj <<
/ColorSpace 3 0 R /Pattern 2 0 R /ExtGState 1 0 R
/Font << /F50 43 0 R /F53 44 0 R >>
/ProcSet [ /PDF /Text ]
>> endobj
77 0 obj <<
/Length 1257
/Filter /FlateDecode
>>
stream
xXKs7WԑK|ؤq&S#˶4v$U$5aZC
#Bsj"p
\
n)'g5Kkr|U[~;`BRA4dݑрlщ$"/b)^"F a8'3/e%i?NF:4IO!I:,Y&Oṽ%GP@Ml(P &Z0ڶue%{