ࡱ> UWPQV(@ |8/ 08DTimes New RomanTT~ܖx: 0ܖDComic Sans MSnTT~ܖx: 0ܖB{h{hgLP IComic Sans MSRegularVersion 2.20Comic Sans MSBSGP4JXa:cW h1:9_)@gRNP'~O鑨WNrФ ;Qe5c#& vq5 lNSeD6,[vfXPuHܱ_<4 h<6XG nYI߃eoih`Jw5ZI`?XY ~\1Z4d$:fL_8?JteHYw^*Ō,|A<=)FI2q@W>ȆRIF;$\Tn|2` '! - ( l,BȑY)0d~@(Lb#6 [խsA`! ;8W(7x{,:<1,{R0fVK&TV2QAgZ' }tP;aK@Odb#,nд'H'rY3!4{Ӌ.P:::~BL1l-mX BĥvO`A*m Vpt3xMd8/^ ,;Th(a=yEm-ɭh|(q!M}z!՛PĽO!6Q`u_g}K.ˋ"T ǚ 6~cY:_Po4Aǔ*~2%/ǫC\[I(Lx04\'QɊw "=.E?c„;w' o,dpԷh=ve'b:ȴ;aUw GݸM6(j`';a8u #/x,Ggtin'&F9GTє"_RL6boe,s+6mhvq&ci,D~2R\W:8k8QГ.qo+ꚸ6U;,΄uMfwϳ-]|,,lIJ ~&>`*?I@ݨgtU ud @"E _tg3$6`W3P- !@p@^;0lNB@ ld'Be?e_XbɄ"0@`z8r,̜qdHGZN =r)`c/9u0~.hPݚZ?fP'oPx'$Bah6Tf5/x[) lxŭʼno-HBHD0 F\,^VCe@ ;ˆٕi夦肅_T]"uJVmQ/?X(&|[3Al p5N$ LVm!:g"睄졒x ~,iYi!JU񹷓 +)_d>)Ah>r$hg1k^v``{v+TRᶋFOM`TJݒ֫էI294r l7!k'25<ꊀȰE > _#lG [6LQ PZZQ/Q4P1 fdGCJlj 9yn@x̨cfJJIUkXq&5qb* vmWVBmt@/,J08T7V=$*q ͎ Y_*AG)mӥ5n|tBGb^ ѯsWt"1L|!ac*  fbHfM$!I58؁\Y>CsWB`*쏫=BHpt &Ju?X`LK|b ]X$ݧ'<>o-84LSs,@CRxS06NE(AJ=WٟJ- $PA N&%oC@EP~P*i˭#JC _BEU+0C9Bl2MzMж+\XO0=0Q|}tqg"A2ET@Y{]%i5(|0*3PUq[.C(fݠ5-cN3&cFNDIL nQ ʉ>˸Fr Q'uEܜ7 qaAgfgz_<0IFsЍH+4W4'16},^v#&0cCμh*.Eٷ?A#M>XxrEQѵN'G1>$do=؍k&H S,Bl{ד rzDәL4g9da4^M qpI[#wXލ<,ʦD:7$ kgFVW L{֚6H- FJ'=* pcv s?9-'vlj=(!㮀kpeO'wM0;LgR*- q7"g Y}RJ5s1㺱4pP:)0;8ΓGA`!K$cHL&t!>_ށBɞZwR2qxa21eS>_Kr%l~$ZI냏HdFէ﫠q} 65Ǜ$TLVij/PI#!$(01Ʌ2%"Dvp6M0j;gd-IPh &oX5U],O@>XrVȿE%,+(L7*96Yn61/]CEDwcesSkyO!ZPc[$T[5tQ=I;hC/P5e*BJzOӡ-[nbM6'Bȑ۫d@" />BΨcCB%KECl SXx*UlnPks2H9O JW9F񾮒,ʠ(0T31Cm"Zh4ѕtvocUgscku35_.,n-h  Int& ڴH'ڗi ?gݳlH)W~  }yR HvC9'w8O +D\g҄Uдc}0&2ɑ"D0pVd31Q#+qK@ڏB` X*P/w4}- *$ -n9м[=F2޾k^a8f`MH%E$MgtTq1eJapy*PdQ7alq@?!#ߔcǰ$fFU@`QAD))BR`SNM\DT%U8ǩDnGHqi]ܡP#VH+ uЗ½%,,g&3x=UCQ1V*]3V% "]czA>[`P%22L-j,>;jEpW :BH&<8\mɨf x;$svU.#͟gv-f8ɈL.q*取_KOrov Ge#c6ѭؤNjF`QrJGϲm\Gu6FP* {ҦS!3N#`sNɔ5(C s Wr"Hq̓dP+\^GAHS[W&x&D1)9 KX v2nx*YupF ($@t -T.͎c[zQcO}}%W Ţakk&֦Sg+´89fhTC]w)FV2z A)UJy]T+6GoS/$]SZ8~}I"bEEW2|b%^הyКlPxeG*P(ui7pP~hR? rN ks1IÈ cQȩkv*Ve2`lR 9ia 0B<TBMZ32bmK XBՆW]P i+^HK9ľ Rgx_vÍPdVgW sџh,a!4&u}n"S4ŊGF1BB` fq#q ڏ59:˳ԑ#! Ǝ\r^~2VOIOTL]9'6U#`=fn BpB`@i1onSx BN"SvEEk MF2Hw:xeqy]O֘z6Nuz|LQZ2 8~a(GLjQq>ay {3Âl-GލMe_"ur.P'.hu* &AyXH'MB5̣Ӕ -E2hz|2ǝc'8d4 mۨB@ 7VQHBE+;l혣&wv|$;MS:185`cǿȂg{|F.8\[yZY.@.wLlѶv {i]랠i5 h2j1@85<7ϕ^k"Syc'LǙ\ 1=4ioЌX鬢DYT/]'`|B-,sFӲ,$yr |=6 mE8'fU\**4O}.s RjYaQqt gglwnu)C35G n- l D*׉qqV=pE oj߰Yy7=#uΊ.b s|[a!k|ƫp3|tiLγDjyKb_>{uR2kX[@ʵT-QaѶSOX:u_Ay0s)9껚R68xuBy0dV^ ~ |?Yt'T7~ pPm'Zs`×i& ӧfex, }xީ'E!=4[gǵti! P"q*NZ@sjt ]fV`ԟjoQG< o R"}F뽞Ax[O%I $^M B% p'lLW&G?jfXo+va|ISx {(VG_?[5_ტX>xG%-zpxG$']O bB#&/q( D8W`7x&ޞS89D{4%K %iE^=tt2' vȜNdY?W/O|RwFK0dPF/@"-%Œ[ENEGiHJJp h mUznh^P&M 9 Xe2g>o؀I KGUbȪCnEqŊf32]xRW/ 4n{D{2R#TrđebPaq.h(Aw{._1䑬c`Z+§C+; E1 eP ʽ\^;&1Z"g}Dq\>ϋ>$Πd i P Ms?i==* M`W~3z.+^˿N: r 4:Qqx(~2]*N.4H C.悐 ЪS (uOXATQ!l[PŜãlH0_6`2 Hhjm6~"ֹ8HGLZLh+$DᘈY/X&Xqb kBP̈[~!&uXߵ"B8ZEUœ87ZV5+d~88(Rx8hSݎŘ^LlӣN"}mbeTae8[q?wrDz; hb!_D#w*P]I4pJoo>WUj!0}MO v.w:ZM9%X d ` y8F v'?&vKeyG\t³7Wl/]*`yuUu݋_'`QSm^Xr >xL. ]ZV( Д =?ię\/"OŜa'݃`ձ OTByȜjgX 0f ֐7^YJ $Dw-x  @R=xh"7(By 0;Jd02lE&3C}?*CÇ2Ѥ`<쩉KGŭ]A E7SypxbѠc o& M6Bz21-OC77.f3.(-C@G|sRfĄ\4a)Auh 26 {\" d'X oQ?ߛ qdU''W':#{iX cv@ss<4m.$8'-R‹GO u>c4UmX;:R@.g v茯*4a%t"}a(s@:K|&Bϟ*-IL}4? t[2 C 8Ļ'vWKRHzOJ@=a^|C;L!h I`߆4V)Au_# ?fI%)U(s-%ÂG,A<%?/ 2 ʷmrG=>lڙľuŞ\Ɠ;fW# c0+.Mg0"cL-{Le;w"8N`i v@}o܏։,w\V<(40>`aYʡQ(0m!yu,NyƘhmg.|Dbv>T!aU `bKՐȴYi?-h(`fh#/ wl@DG[dmL胸t#χFIo +տsЏJM1M} I(xٕF)HRafh^*)i%"i ~ I}EraV4]N/VJZ5N L,aoPUX-Nz9ŗ{A jO1L]x:?)/8><;3ɖi/)I˙ܷca K N2T2'#2aQ89_|ci|a܏Pq JUgb̐B.#s'Փ̂vu!P'{ՅOq81+nb):y",Xğ묪sޠ ~&B1KBP_K&Bf;7:cƻP5Nr1"o|㊘aŻTk)M,b:h X֔.(ȬS w7w$J RJO8(1Dua@n7Hg}{YQC3g,fUl̨ڌD/ 4-d<>2]ӳ}n8[*T5 MK;pc[2ul ٥OtFXb߄79$Rs `sp=g3,QsJcu Y(( iA5NT?6ځ$;xʒ~nS40 ltidp1]:]RJѵ8TDGa.Fu0pUŇ,(@=+./ 85&íGL TO~ A"hfm`wجC~<2,@zP^cA3WMٙq%qHp[1cpO 煫4${!dP[XĸVѤ}Yr>(7HrI?uRp|{yCB9O_@؝Е*"+#Z~#rEd@3a8Li#v 0IB8!$Nwz e@^dBSV)]}K)C!`"h5JXoUPQP>Lm̝d~#\F` \2:3zy}7+˔^F  0AP?nI (X)* +3F(+D8"p4l}2*wawxȅ4xy׾B๕" R1ʼ&:$Fd@A(W#WrgyO4h*hueݭ/ Vws8?C2*;yDfbs^!LػĹA8vK.WC+9^H~ * y2gcw՞ofG# ͓pi3* AB(haK Xë@BgƿD'qJ9y'hmF/gЫk*cy\"kZ4jO{i;D1AU%Mqv_CRM`L86<ٯk03&c'=R V>EO"jF0*w"T #cd0q|,{0vpb?G}b5R:$`5J]z$6= 4 0֨/*<2( 5ÁGć7xkhEmgk^ mTg/<(7xsp@zw؂+݄ D Mdsy,4A,c'EҔ?Ecx\HSw=6 )-Y!qp+XM,,X_A v]QˡUHAf4zWMgz~^hWk< M2";OqS0t ymmNS/mΗF1 ._I0'*Z]_tR8l2IOB$n[\ 4ОU$8yȔTPì6ʈ цb "ۀ *ZI-_6d7ơG+Q BXE{Wl>|(:"u6#&#sV#&3lQ j#嘼 DlF(.imnΚԈ&:Xq5cP:s`Fs,J$V ӂ@kN;cl K1.G Ryh-@C>aTku 2ʡde4$Lɛ ߲T2.Wš[uF\*e4 #G1L_Y wEa^ mw+v ł,06WZ`IZ{bM[ .˼_h^Ъmy;%SVsC{gH-J.a;_KlҢE㟓 T%gb-sݟzx ~ QcŔ wѳʰyHފhh@W$3!1$% 3J(]=SD]@O_\=c ț&āpd} Μ:a0աRܸ0.(RRT+eC]El7kV.Ae}$MSLeJ]i e3l18z%E؉AYOփ鳬rLqV3~DQfOz|DN0Z;wK)}\ eJJ 2q뙳 q-p(*zǦZ%%WΘ~*mHnZcNBl_b<6 M#U.,0j1O5 l,Vk+)'dcٓ-j>zم6?HiȐɘH 4]5kZTBΣp*AGhPd 8+zWG'=&th:^C<}HG ƐEW!2Bkh+4̗'kߡ]hJks6O1F>$Z&dl w*-Ș)UxpMQMW iIpVaTdK6|t!\ޑ' ʊ UV 0UDܦvt8BrxY5} 5n &Y}*ucZ&Y&K! kc}mro5 O) nMzY>HbC̺N (M)FBgRH)Δkn0';Qi+U; px%=@Ή*&?A*n^pGT~).lR<[ 5_ `ƚW!N2WZNlL3LWp!W 5~[DQ-9#:u%2b1p -YyaVyH>i VNOo,HZ޸0/Aq$1r\K,bi06+a$@U@FRkX{}h72-)hCt òX#;( / vtzcpɑ r|>/^Ru;S6|y| 'RfRh w+Sp#RITF8)`3G -mI,G4 َPx 3,?̟F v,Fn-Rsà`U!E`B[R`N0K0J!ٗ2+I}i ?.s!ʧ*B:&($+Ey*}6܋u>-fYvNxNǴepЉW\;}na'( ">՘0HS( Mr^Xᾊ]M:Z!YPlyL~KHAT e*Onk h& eb3&-w8S@x6+G[@hFqݲk[@P,RAALk!SPzGRlKUϘ1U7J۠(ҪP6)J#N$U.\3Y1F%p޿#uS M{Bܾ&e%,PA@(8/')Hr65s]Ԓ°ݚ#pX,zA'JcneYJS@ɂC2Z0U@ehPz@w@"&>YMzlzjO^a G-7 وCuXq +ܣw;3٤Bԝ^t~6sLqQ(1.:"RJT4_]z}7O]jӲn j^wqJp+"E/bH _E, 5n$ǒ5k`͢k *gAnR燓<BBZ\'7y-&Jd݆BJֲiiAģuP]k``rUrZH%15#\A3#Q ֊̤ ͈7k^>ut^ 0 Awi"-Wo^ ‘yVi'N<Ѻ5q˯pYHx( g$'1HC<˹ +4CB<Υ1v}B`$ꋤmMR{G TE]SXI)IE$<ބG!{~aoHt^\M9+'!G8`_VÍR)t-M>1 '@!* (BadRG@|T<K.n^n/ bysNHCT4@`No{ ߹(H$_N,7DatJج1.f$L\#$#\c>P ~99-j6-L9Xn5t?"mЭY@)r^L@J.TU^]A$(P*ubZߞk>0)C ZwB\ \RT7g@MŽj2^`]Zr(BE&a\7"=ŗǀnLv";)9"xº-`n5Dm~`9$(Y"#WEE|`Dfýw0nY=H1o 5oִo휤яfZfYꞾz/pl0>c|U(y,)jBWC\a-7D~m3A7 GPxO_xlDPH;| NPk;% *%Ҏgo;ULqx4kB.D t33+(*p F͉ʺ`PNK" A9)xJʜ&DqZ^.NDl$"HTxZR)bOu[@/, "0 }YnP  0qp( mm D KAǯ C}l1͜ ftS.,P pJ.Ag##`AMl*!h"- p4p ,F34@2 Ð;1 Ǩ`(c\-r|.@_ T7mu]jZi9ZbLPF(AbXS^@U|4/E<!77R#~ypyxy8\pk?mxd/u9`\z}TDWُ*Čٞ,i]\i$4GCj?K_~2 ~7I_Ii+ |ྒ0AO@H!-\X=3rªJڹ81wh%xa%JnɞA~r]/^,x, j(a$J{zc*xt5I" v**JXxT铑xu=m]ϻh, @R5Cd* j 1JpkeEMZ9f-IDKƐ8v<ɩC:Q{L ۥlZF`CxM.̙E^|0 %"I_?Q$A#>(J0 Dzi{dYV/0"TS˲FYV|cT D K1ƨ+>F}z4wFz~tum5@qxM6`uL C -CJYeKiŃ*Rɡ՗,yAZg#a+3]S"Q3hM,\Aؿ&bj4h',ިW`xT߀ ͙e1`U*fD39ѹbGȧiD:ңTir+"\QVP*b)AHM./PyMiaV9ۍWLn^: H&8 "EC"TʩΊ)#̕ޝ?`YDTM7zp x@TIAz*Qct /*0C/Y(5{a|h\|Yp?x^>,gXҎp '[KE)®8!*v|tT\k猖-Laa`6$4#j"sgEà v` FHjEߝ1NEAa+-i@QQ+Z)m 0"f3Ddpƍ"h*a,9%bҦxV`+ ,i6* ]er"qؾ#ZډL͒Gi`7enk.eyT@E :ض~j הF mqC_؇6! |K{@!) )g4G3#~(+7٭Wh<-K$@j$҈90v{SGf&ʮ_L%i8P8oP tiJF7Aj(jc%O:`XP6,O>B {ri j!o˟0Bx$v*iN#C=b@ PٵO4*)d}2F4\u:+ ҘӾvvЄ%kU-`*(iq1?k >5=7ء֛2ad ?VQoqy-1OD B`rIs+K쨣s%*a1!f@# s 7&ʑq=f)!@3JzFJD[X%)nڡ + y@tVŒXsu@1 Ξ!vɄID~. <7)zy!88PF87[i F猜c3JWŨR Solsu{r@Ex.iAh9Y_[(3m_Aξr[y; BB n~:z> QڱYe /'Ǝ sL Ekb7l歛.Qnk@BϺwE _7a]7J5MO@#xGwAFb뀃m}6#'j4ɶ~n*Ά3݋FZ@7F3SNK.\YM^! e3bމ}Q' K0vYu^<`|",a'!+SYݶbMVUƕ8 ,@C)5(W"\RH枂Kv ]|9<}?HiQ)˖q2$MNK̴ڰ,wSfp*dBDج' wNh`Q;;j|ELDwu/$PIbt _C)LH+͌3.vW"A07vd2 Ӧqp$ю٫YNCR^5kʒ$!YCz-; /(.*CU3n|bdn CaUMw!Ik֣ 78-&ȂȂ"#80>[?:eK?v3$1-@P#Z}؊yT<@JHe3(0ŝe" x|BܾZ3}74@EP8sdЯw@"0XE\0a #@I*ئHN-M>R\.Os>Xlg TXE-@Y\ z˙+#^†Ќv|Dh>@0%r@rG h-4SHѧr Pm+øF+'uZaDM,Ml|v.! y"o`9HywCm$$uԾn*wz<.Hj7-Y'q{(\oC4 IIOJx(Qw x`G- CAd\->Ԥ:'zM|] rVW_aH[Juog>bq3 SLս`F\X`2Z 6G^C)ߕk2E<' rYYPb=T޳pkm#f' AB!/ʝŢF`L&{gP\ ewȭAH79ml*é% w+,yCB#~?35(KvEU$hʲgط9P?ߏ? 8B AD^:oCuI{QĮM0$ZPX ^hc]D fQj#/ yl"= 1!!LP@9ۑ F΢˻M!+rjXml[KWI! .PQi]T >!={e_L<΄Rr#+IOqܺMjYC`bdx_}V$+$`q\^קkw7RLq S-e# kV.[qP!R<|$82ryZQ1ww~aDs%;p8R ;l$T:PyP$`d +S8l@ k@3APӧ.f.64k2,"kؔ˯ie;l P(V,ˁrm3%$ACYZsP(ٯ%x.HٱGUR'ѬaE S_G~Mz3|2 )+]m ᩧWi;US8:%r0-B$1Ϯ,5P0>K+to~uuB+/s1䂥@qB@=D-LgH@ Ez sOP@v+EA^x@z@mklh-Ν젉ցD}Y{W|7 .wO,WjBćݰ@+XUgn/JX&th_ jcl|[.<(ྑ@#2^NjhU A{k**@|IۊYDӯdWoIq"x;YsixL!٬.'k"2U6oxbyyM(j@+\?5ؾ9]{Ȓ}C|:#*doz1@ =8dGrhFSA҅PuHLΒ9$~dl}S_ϵ)=v$hHE4< ]lH"|nk受^4KUJ䧁[,_u'f|:.8uulo1dD>-V/kq|c@xsE< wUʍ" Iфqwh^p Qn/L &w5LV)=H+$ F(~1hdޏw k{c/Ԭ*41HQ ̛wWڬnUĝ'82(""6!hSI '~P=,EHW9I:bjO|$Xf^넰JLy^2H-86Z4L':2PJ,xп3Mm zPҢI* hEvRfD ay1X4O:Mxt‹RnN*xvw6 $uRa;f(0$'O8 &#S `p&b8S 1Η`# lV a-ȅldЦl/q`VÜ{ ,:1? ֌wBe-ځq2ցq,gp;~+IM>Rą >PDY]q3"6e0S0(ԣB6}["ذML hm57J>P!۹ SvDmc,x$x XwF:=D?N5  -SLu6hoF1 *63jTYh[ ÄO5üDrEV-[!7ED^C|}dk+H8,!ǏL݋#]F"i "*Rt* LLaRc`̼ggt9%i`3ဓDj#6{@gL/R,s/ :AʣzZ3%  o%L4W!YuF-Pш,]iOecUW{8b!GlUٴ>|@RP JTwy)bSyߘ7b7粖aוW8D]:+i^x+RPC GVGVmU LP 5qComic Sans MS BoldVersion 2.10$Comic Sans MS BoldBSGPܬAPZ5cW h1:9?~A6z]uhLԉME#hR, %,ii$ى$OgHLzlZ `#Z`֗tXiޔ-XϜ)f [Smʮ=Vo4%%$XmrA-&6W@"kJ&:MO̗ I+`n`' 'FlQu1ɼLp PkȾ;Cl]_M I=>-/A)f3*x,NujUN]8i^n<#<Ma*ս9#%<j*mq D$ØESCMOw=~+hgbZ!E4-@P12W!!!njK:R? . F < &UeQ=k&U6X& VLu[KECP/S`Q|*O?s@x9MfJbw"oԙkѰF 뇱ƽUPT*t%\ b"z"h<\,xr,-FAzR$RC96w- GRb~c9RnJ.%IJ!$-4Rw<,Azw `Sl;+CZYق.*>ȹGH2]fd?.lEP19*?vhE}S>)xd嘁 j /!@ѣ^ҍ=ABG3v UrJg9ʄBdCYD2u6y`hq,`V䆈QwG! 4Ǽ@r/Ġ'A d fd/sl}dH!!Dz\>Y~ȘINg?xڠKx5LBּTKQ'k>&VܳLo(Lޫ6^q֒Ԥ9]knM_@-p\%2T_j߷PP'C@ev1w};ܣ%?,&ƶ7Sh},UO@`kna/gҶz[-wWc.֎Z &ŷ3 @0#a ߉`y4_/ݐibxୈ$h;Γd,$JTp&-c%vd/| |2ILݔA$f6i0YeӃsZអhbBjF2zYЉv|O3)U7I;N9N"J!cC '[1)L-6I HG W2N5 HE*485䉪=D`x D L"Y+QJGS-r?u~.Je#R`4a@:03*f YS(Yja7@ʎ. #6:Q]HW .x&նyt5e.Y諳8Wؕh6$"rM3jC^!^V8L"xϴd`jda3;O'wJ*IݺJ -S5 3Q6NeSerbG(+f A4O<^s KB^TL' ~jR(2*زg 4:fܲlR@J`)@qzИ*j it_,e7KNˀN8H&O[觼YdnYH?-|D_SSН( ?,r;QNGZ/AWS9xh1,r )6$t|CjB8J0فTs@=aZp3ᰃ3$b.`5D^b{]t -뿬tHV^p0aIR&@b=$# O=t+CjÚn?yZb<ŲĶİBScyaaAN|[VŌ"dW:xhKGq* d04o}yf~a+C.C4c$+Y:hC (Y!IcZpx&N5Idk9O5<(8`G]$l(T2"$  )ATmGBJvrj ⣅لT>6fE Wa.NN{lL J'`+5@ ] r*<y5b .Ԋ&eihqԪnE6\$OlȞIi~P0,fh@?c`J(آ;}TΡ`Lc|0Tk呐PV5TE CEӧU6Cmgׄ'TB26yu`4$EСM .ғVF`#+8<.oB:c/#15KVu $!RHj|U!LNBeX&тyqr)lxhB&u(;g8KH yJ4MK89Y* m* &* wJ~>t _ӽ3䐻宍 y }}\ ӕ-x~\'/Ֆ&5Ö6~! U!*KՒHbCc[龩8q)Ml'mM& "Bk`RU6MPRl[MT|5<݀\mvkake -#N04v0 xE|I xv :0Z51xQ{heΒ`Xj hZN?M#V9pEiJ\`\,5YYս/b > US0O~WlR^sÜg5i1q+~ N h>P|9;fMlm|wwKn'd:煇 ".$ jBYvZFE gYUrFKs :NR˷*̸Pi'M`zs fM5_)fW! ^p>%J Uyxܐ ĎHol;"[r',9k=H?& DR=2- ueM!Ͻp?"M0]D"Z?JQφܸqJb{Ϛ⡂Zuw<@8М@vB''Oirz{!ϾrڣDv0A/b CݳE)f aD"ؑI߀ ۲$w3EFXZhWn3?ӂ!k`6='"^Vꢈ@ .7kq f>BS{j:^JQjNŮrc⨈/RzkArz,ĝb/b{4C9EB/G8EYA:!%{.nv=mۙ!!C>JIܧPF }'嵽Ҷng{$I 2΄,jȠKCs͢W39asg2r$I4_3qJFgn&A (Pf%/ƾcP&hG{j`eM}?ȦMdYJ1ݐP1}0_k{`G7? IҜ/ W]d0b$RZk6406㆓dtq;|: me7MYNJa QJhZÇ984٥' ={)Y !A gc5%ZXbͻNt䐛hyLJBrZE x C{4GZ`=QdpvmA`/cp\2(iT8> &Έ8 [[J;~$}6+LXF'^#70 [ TKco^% $hzfQԠTxo;q4~zͤ6$IpX!~0Uj8'6ZʂAM 6NGGcs83oLD.dрТvPD@tp#{ kA Wa)YI q ̢w!A (8YȊ:ůM?]<OCwbB [ki'@l`byV{B}0: Au?l[ hC U[94&~$l y3DRXScJ%_PҶ7DPDpϑ1µ7e`tXCluH%:-8!`\ߐe/Dd8rF@eֽC@`RKQ}QĆG>o"Mtf;g6xNPilAU] \We\k׿ 4ʙt e֝` aN.WL(sJ[4X5 `ȒY1&PӘY ]Lj"'[ ~Ow%v 0QDS0s'FG&B5iBآHxB"ۺ\A쩡6 506txcWJՄ~Ni)ňDSD356Qj!NDMP~(gJb^pY(~n9NiOfl@DN)wbD1SF[H'6*z{6sCpN}oy ?tm CƔ2Vgu&@Ēw=Q57~qxsMt]u7I#4Hj.(*' #|^@ XفhZ=`1S'(jӘt2/nog./ؑ(шRVU26JfWJM|$>dwԒuHca_/h>A A6^%t^;b`(P!`\"}R=#h w!뾯$_G)+`Z2i{Z=5Z`c@J_8RTرIU QQtFhUC8eSu<XتWtoG=̋E]82@`(KvJ DRzpz""C8lˀ)-z|}_Hb#c!(A\ϗ ]}nۊuBYIe N -iY#T;q &OEG.+iRϳPP$1:~|?&`6WU^7*kQD8S~y="Wb>͌tEp#$xū@7 Ag2E UO}@G0MoͼBE$($&6 #YO$DʐE oFOU4Jèx* Y"=&P}N&VV[ˆjԓ/,X @13H/B Gx'DA\,#$ if Le`{CǓ:xޟ}a 7 FqXQ>pL zᬌ 8yEWgxmLDKzhc` !x侮-~:5VX>7'w2:_GHWfB13FlH'Mi{[p s[e ~Z"҆[- [jq '&*s~+PI $6𔷖"?n:Muu{27C>1zp,QH fĶ\Vh@ƛ[J:~pK! 8gX$'Ȳ0N1A37l |#sڏI KGFyό$nьsfD!ʅ!X;2) C%j/+_8BŦKFOY 0(V `Zm̓  <݄~՜b2~"v1H뷕qFj|ᅒD()l m"eM o$ IՈ`6Bü=~fryT_Q˸U=2 0fqe>VHf` q,Kح7[X] BIɆsovҶɦ%Gw_hRA*ڬ:$Ku^fopzwע_@qay.r0o^z2 _pL sUL`Г/0ޣZZ:u(FsVrC&PXyQPNMgm :J4PGO75(!h-m^,SQSHO$KkݮC>9L‹;iXꄢ 6%#v`%Э7|!k[ŔpzU"WEwF>C |Hْ S!~_TźĮ-Էs"͋- 9=q":C18H8@N[Us3S5XҾ(,|!p1:^VZ<<[ /X+DV8 CwɈFf=}L1y &x,@d7|}bX^" ( .]e7qgOۥHJ ۃc. P)mg+Y*P4dݔdS?B N!v>2nAQl=RKۼ㙺N쁓ls,56y0EZ.A\,L2#6Q?|GO;٧7". 8 |<9pӨ29 [n!9y9=[߃%374@N S^R8kL2wd*'(hw* e@,fK`K'! ݅ghab DZ)`qs!f,NE74p}>˒Wn.~ A"}5,}OU uv<Ңrd? ,t*X/#۝d8h5ΖY ]Quwҍu@SbJt%>yOWA! 68580604 `Wh 1bO󹉍 ࿺Vz@'zC$-Y7yn`UL78Hi;qh}\X笞YRl[?xI Vﶗ(s?1ư kg"<8 .)3xraf ɇh>S eㄓ Am3GSLFMy@2΁Q$8;U#q YQAssHY+Hx/|h) B/ Z̠ǯ@,`/V*Og "lrۿpw>\fOi"3ѢӴiӓՒC0h1@M0X9YQ A`PKnס]-6rlC%jN`/h9Rիұ:@!.{E[FMSjC*}Xm@m= vKG!NLΰa97l4!EZ{e/OC&r$Ue[ (E-;VuB BZQ!Xޑ+SGe_k I_=1`M$J^xji~ID( BZL}B]TtN][K pINYC' 3(ÒKze%!VE<61W],}pD5U+̾%]J>Bj6& 5=g1:$p!)gpo"_.˰EDnߵ&=e/q9\,+)UP IaL^$$跁!@n (0NXI*vDjTkW:C9?NjO!$T < [›F *@0HP y6Q4QD_`7f* e8SwB+q}Kzs:i9k6ݻE] b?ykqa|f#0n%K >  x䎁ӁA\ M^'@tp;VBEwp4u&/a-c}qEs"p/yi*Ui禧pJ@:k,Ww1Iac/I=#X%"?ٔaRcL+r }p Y*]DZ0WWm==11M/3S!#~!;_9/M@-r8!" U*SI F=xp"4{uǓln? (ұE\?|uo%2f`B]z~%˼PiAW'mzuвh 9`dK-Z:j$D޷P[W +R7|!!:ɴKǞW l\bjLli0n&ouHsDa>*"y 2FU-#_z 57QшL-'(%E#}׈ Ԯy/$!üP:NW "%"+,I[>qxY?~o@K#Lbc b y9ŋ4~BUX-cu e#$k-V8]Qmd {.+$WĸD}L4<zjGbFL3 Ev0-e|f7|:"\P~Fi0ѰC$fYI.H#)$YP@=rIE4hPo!b40 =EHe7bT3^06ﲠp _TQ^ nzӶW;݇enU%Rb#gw6JJ;OFMMpaA!} -"p32eң_KK 9M$3b0[A"X¡sY(0d ,7%4I%zdlK Q T0 Zҁ OmanUR/Jl_ 20OC:6:3;UB!HQd8v*yaAFh FE:e'QѪ`spFE:XzV;e$BMSBI[(1PDS3pZ420\=#W0(0/H$:y<,r|!<$O= 65nuJג4e NQ\–T=UZlPW:7/qM0|袽6|3\D$q†8G.6 > hvGjՂ5?)gPTΩ8Sovh[je= sRJ)ˊ5w' ;@5iT4Wr&*wkS6>m.p= cMZK>XF9N N}V8vcX2紴OO}R+Y]aQ Z(<x#Dg<~ |c''džDND}"m]9@-,k.Ȉ`# sdLp\yY#LnexMj l6kf33; Skyj'co*()h&蜢LڦI٬W9uY?q RS( ghͳU[cL<ĎPRdf44q@ST$xq }sTf_$`dTL;{kɕd-o")NNMLl2uT#3pE֓+ci2BuorX~ͦԹjuN|ܻu1˼Xs0Y`hDޞet <ٓK4$A%I 5%F@KQ&;Mn^" N9:y-k`| (MP.&@`Bh*mFy]i){>6^Q$"i6%mJ;hEI$6 fihL2|_I+dq&sIi.aVpsQg>0YMNˎ-].Ϭj\̍8?lFcZH)yIwrqSd9TϪN<."ML#n]K6,eme177+J"pkpEHN!ŽvFdJ 6 AT0f}z.9JMvlq*wHj04Y96=i5er:$aRGIPi ta>پ O(4ʁ;xNA 9Ȗ \h1c7L^au55YC1w҃9DK>pḞ>`~"g2,r Zb=9N]ANSb$HJ&oO1Y # KN:NsnS=U+N? Jj2=0 (:…TR)8 ؊ 0E;$v")hۨ c2w"8 !`6$` Ta:\5r"XYu˞gd12u _5N" )8GAJ.# f@5X)_ɰuw,OCU[DB @  ̩iPg5TOfBabJf4&hhd3S e2]K)N#Ũi#c|xSR ,l(Yi jbz#G" " 1QE1ѨnHЯ]8Tп 9 >϶Y3ePt:,HE3.p&[iS^dBE8FP<-rGchQ-TRU.ڏ^ BKkFrU$ .Tyf{{(2Yaڽw>hFѱZNk(DZ~7³lbÄ0` FAk"3,20ì@"9pj0IJs0^p2t D*v SQ+o27w,l5ᆹo14 6QQ؋s" ;%m7nb 9Ey_A?mبWAB" z;Dr0&o>'e hP}܃xΰp<.q 8b;!prUg7 אn0I=HhHqH4A*(sr}Q6_WjdXK~i-*0]"<˨/fhjă.&c}ʳ%f*iRW$l׻u*\MdgA1멲 a1LdTCH+[}k%`XPD9! u?'y )󸪆 P0vN‡@M8([蕳sܪ(Ic)/oZ^g1`Ɵ͆, Na,R@{`13E7gtkD٬6ǏQ&v &La|%ĭf[`7i2Z868Q72ڂFG7vs-@\~Aj-j C'BbT_˕ud>.b$ʯ1#qx7P#FȺ#W,hC&"ϭ ! D@h 6`8XtD>@'srPg{h8p1$`J 왺N:HnqMxAei-o; 7SAUbҒ"!e3yVP7!HqȲ"DN sò"?J5pI|DCЮ|`m*+)/rύ7{1TPE9#eY#2:rQ m8ud볠,0٫Hap(Or/zېp`~1l .c6C"͈1&$aÄNs#ޒ/6mNY(۸@A:JEkkbô\7T7B8"o/îcJpŠ(ZƝDprHu3ċ-7hI  2v&E( @"H4Ebv )=IMnޣ&}@DApkvޚOWw+d[yC`}&Gjxm*}iQP h,*bY4   .^䤱mE.צqf0 D`B,FIH$,&ğPؼD [Aā-'qltm*;W>.Wdu HR=! >W,ZHvR$^2X7CUH4;Mb:j۩z5m[o{?^M8#?>8fCUZt1O Se^YHfۗdnba zA[`&` !&LÆ\?m+ҨZ-n[JK FblA33D#f<KnZ-=&3/62>ӆl Rn vh›m}q0C'KCf׃gl)HtASAb["h\ )cxCVBC(d4\0&/j4ҁUa1ahPP|aviϧߴj+!8#Ewy{k,ji"E2of @֍^0/ԙ̰k4gSzj ^U/Ebh8/#$g2P%k2V+.6t(xL&BmZOvmmb`K{׹>a] P[_E Vk]T$H y1ּAb.sI LP^x=@-(\5L'pN@H5~ͷH7o/L( -`@cTkL4 Rµe$'&qOZilTxqU.t)`xօA{jyʂaVt6z\ـ,U;ѲaXPJpnw*l#t>`1hN*Jy+ȼ9":^fP m- Ȗ /ͳ 2aنtW:| z`/X9k~,‘gyy W锱 u `Y$)L- -ܮ:;ŷ 9ا&!/Rb  LSQca%ideQb&f!+˱SӦ8TıO)> |`R9;)($I23K|0QaLчBk3%3rCj|| vjk͉.61Ã]F8U1 ]+F+D$D0[ z#C_=4>)hbyr%QL6'W!)cx'FY #V5&ܸ h4F:8эR)U "Bd!t>̋4  WH@c{W1E|鍋zYbTѪ6ԭdт"~cl_+1߽Hl0ЙFf <g7Ў2B)8 D4?m=%+; b ׅj_%U*H@ $EXg)8:ءRhnt$BP5HlR(.йq ʶbڟP]?,$DJcA $ #R j iY }m(  B' vP-0 ǝDH M@$G0oP 1Z.\8hICCJѴ̫wIW{D DArialSans MSnTT~ܖx: 0ܖ"0Dcmsy10ans MSnTT~ܖx: 0ܖ"w>w>= LP5/cmsy10Regular1.1/12-Nov-94 cmsy10BSGP<09"4`WhKw~s vh|h{f&`[ h%N#smʽqYj~5N r$%pV'LA{zF&k9EelAE).4Մ^ 0ЦT*ktFYw~`lF߫YB?'AA`VO(W(÷@..tN#W/ `9:tHg+cp#h C_mA$1/q"A5oMxxGFVZb ," ,f "lx1"!m܁'`z?z%fÎ;:%M E:R.FQ_,CfkW8TW$DoeAV'UqV8@8nrI 'i,GfyWa"9)?`;V0_EܽOLJ#n-+sO`AS$ }t&3&sD]f]Al".%TkۣZ!ާ59N2j:t C(.b|vr@bJ{[71 $(d+8YpN1OA\us[y]')])#յ{kMdKUugG79,P"x@W6 wv`Pȼafa\6c:`{&)g)w^f6D Sl(?&4qimP] ,^KؘYcӾI6EtəhEdKyAP>k}%;`e6F4QŬmȱ`JjriCDyIkټhȌ@~PRG> ᯩI|B/8COQ#Lʕf0tg1,/yUs]!Ҙbך8qO&PП (3A,^!vU`X<6TN& j{ĈA70m AF0 Ҍ S?RB~'sNPJս6n0Yte恭 ?S(/P@´rbBS^a'cɴ;nU!H{ȪqP8B B{8hF '\JZ1AiMӪP[ojAjژ+ٜɰKUߎtIiU0`JTW !!3$L4ˏ@#|]X$s⹹)"bbۖHtό>N.&'W-ð $cRĈJÉ{_ּRAiW#OlvDNIIfa'•V1!u %ڰx˶-I/胅xébR(V:^ Ĕ g i!{+d1x9,hBN+.M1Zk3 SsY~ңY؁ù4b|"L!Џapr(b5eGiؼʤҢ==~q\L/#I⫷Kjv$"\28ww6/XNI2<,}PTn 3^6jz#MWDqwRm.23lvTIaFЋPZMT $T),.ܮ*'FnI0ŴhY(9tLPh_XaƗ~xo\r̺R{D}Jم\ 7ElIfຨOOXV75tU?nAF@#%!*f#7y hq.{IPTyxۤ3&_n"y49__B9X"P.+u=L :Ʌ\( %HmLCZk[D6 [l{ f06u{'ޕ-<@̄]b ]?>.J{;a뛦9@ѻ%kZ 21;AIYodG 2"U*|mC&Q`ǜ;xJ:) 2/k Mv-#׀Pې$\ |2o5B;ImBDF)KTNB~iy8Ȱ0x0%. |Xm^W/l dt4P4!䍳izRDٯD#xTy&IkquוROc/-˹|ܮ Ɏ戌r9ͼ7+w LG0,w3=rAŐ :+:3̼ؖ&tp+uS< !AJBƨM!` %&BTxŭTj}i'NLUۀH|nWuPd~ByGu &(2_tm!9bĮvT1;X W*Ky9`VvvvˉtA%kAJksqn pa@(,4ljLf_x&#no h,:ZzZY\T@%I(@WlR/l@fk %d74:5]~ysL ?8*`7B}2AzRNl$@VBQXW7ơ<3K$wߒN{7/nw]8^8,H] !MBZDҊy%8∺sxK%A1a覮Q6plXzb ;ul;jرքo,}euhJ; 0VG*W: (z%+WcLrEWO*}rz$Y#ɢ%?~Q$w4|+ːclchS3x xᰩ]LywF5bkA|W\{mqb/]4#`hm@ۙmpR| =jjlj^n8?;ZevL>GvkFJF%wZ T=-MܬIZ^6k{u7K0فml?s,Hp"2,qygV'UH~`)؇:Ǒ݂R_(f$в kO(8W u+P{|_;Jz8[yf=ҚNᐌ&1y\aY4.*=m] %Cxz(:]O—':m\m9M1j$.QVaЁ|M3M엚;! l"-C|r0Uhoi`rwz^ bBc% CP~K.t1 +$u6#t| A4ȀϳZ:͹ KB|BC)e~+kVzˤg'p'ȴ^!,V5ȍaH`EpM؟"ju?`ex (*iH4Y=<=5=Z GjOYa(VND |3hr1ZIAX|(J|'&^ipF (Owg5a F!3ncR pg3V6J-Ϊވ,$+,}W6 0pmzʧ]7;}d5.n"Lc C7Ar@Ze(tLg6XȷlE8{>!isqa h+ āϧ PcI`@ ̹q}D1KiHgvg(^9O2jA&Uśb>h;dK#AtL & k+8C$$AԖ.U'å&QN0EPkդʣ6lQo' oh bm@L(K.)op镽O͜L4 0MЫ7?"dm>7Fy<4JO"$/ Vfɫv$ ( 2l$`rDpe*":BltNʼn.tlIhO46!Je{q/^ꧧqr@ v9]'fS2e䙔>9aPB]ueJduxozA,tJ֨*GSOi yuSy> US:I ~J6Q,H'g͒ko"H#' |tھot.}- @dԎCp8'WuQc5ōǻl NPG.EdeќLg`ZL;zr48t(+6\y) J*n "ϹrdS$<HAS.ģtnkq㴏|(F(FKbJS ز>R_`-cV9M$4=fqg8RPU]_5mQ9S *kM__A5BwO+Ea$#"@OWm~ I ѭKDtfHV^ЃAKRB"p,^LMm߂ {Bu09gS! nhk0 ˑLlb0+M3il81vp;<2)w}Nn Xf\>D Ċa @`|Lj<:OCIql(/T)FH$0 !gY;]b BWb40͉ᏔEꙆ)mKުȘ=ڠX1 2@Ki@_ [, _G*[c'h]4e=G0,Ph\N:f^xR*$|ufTqBtojA10x|Բ] ,lFEt2mT!@V¾5.%oǼ ܽ o}[. ؤUFQI9):fDjߥ\t_ $i<0ZT@gZkW–d"HUɀNO#*Mݢ"h7Fah%Bz_%7"C?iQ' ERDs"&Hl.9I [N/>lR^kDyeg5j,T4r"|X;`7q Gx{d.(32 yQ5npBn{"(x~h*Ǒ?XvnWΘWNfǯH$3,.(+:z\A }2$bxA7%-v۹C A3 mgdޛЀih hZueDW'9f Sd27ɤr0"dW^h"Pܸ%\h-~EIC/ K|!K6CהKCVra=QbCv+͟v)1"1WKQE!KPOp(j J51®“a0(Ub2P"jKb؄4wR322W@\09os:Wg/?wX Ǟ-s )Vt Ajup vq! #X X\:g(gd8H(Bמ<-PD2W#BNcdr.-bK|Z'И3,%2>MB*(\!=he&B}`:An$ƓU=wu=+c.7 xFjsۗ1efs&2؟=e~m ^`$ aEH@~,@5^I3` ؉+ ]#g5}%t (‚.NO\,fD `j-9Hτws#8 i0QYO#m>E.-a@Hˆܶl$ZPp*u * :w7X\ƝhAܷ;rzrhPS?É]ny~OBʘVUEMwjUOB"(G/f2pr"ԎՈ5}1 t`BtkG+yZ-:uZ7TC l mHzs̊ÌEV1eMl_bVbksM&`~aYrmv"U7葱o^ 2 qSG? 9,E0\mlLc^QYP!,cIS2 gB@]9ʳ/H `.I0a:f@;-o‡$p85}_"g[El.ˬ[nǦҖt ř܈DAX2EW\G'PFC2Q o5\EWj-Kץ^@,|oaȖ$QIT/ R|:/Zn] /q([`w^>~#mU݂hDbMC8봀7Y36[G{WHo9 |;gjMRBa8bΠ_J'9yM7Hzx斠គFo'Jy0UG 1!@hs-E U][|ulZ^ÓpmWQd={eA{ڔ ̬i/s#EI~y~(dK,wZVp֮J }zH2r*"!hIzp r[n)Yo_TC0Fl"ž9 VZɍŋ&6@jB̎Z)r}j̱@ĮA# 5IK|ZNY<9'xXFV׋${L9a #p93|qY`b u(ğV|g'Fe*0@3\PBT⍛U|#4H׺8aq+r-A>SK/ ~e`$9$X1&孲lg@%H:$Bߋ m}9d{Q Rl `ufe)q} +>XC5!%  QR1 GkiX{BJ> г| _0#vb2F yQ(Dp$`E{J3YI@[XwU>[qxc'ݪ'i>}C #Ĕ=%|*mHCmP@ ʋԆF|64\-wU `wym/iX̔WH3wJDC21=ѵkm  W\7{rIx5C;+=ےn^qa)K g[ ˙'ejIT^ ^0Zx׶6M2S+RqDb(M<ƈnPDЄs*>"$ C"%^w/70,K0YW2C* LйBv'Bf{J08V&j7FCT"V+9zTs_X ?20b1&0Sy5`}Z7kPOg4/hnȟ^4 qsk2& i@c3gJ X>q0;2lOf*Ic`i@'쎞PBx3( KoUy'$>m[HBvA cD[Ƶ)JL!\R3C>eI@Af4`pc%=zYY":p_D6c7JkotY=< њc7Lԛka3 WDM}s\ZbM*}ZAfvxK?X1HDN:Ӿ;ȱ:Z ^/V2&N%_rvq⢢;4+Z&j-aْl-&(%bky (H[I:f2M\bx'7+m \tT$Bs/*f-6ȃ( YaoEH7F ."p'4 6QF+O8cotX[iJUӮj>ba"uw‹Z&K.Ϟsq1'xE4oL9x#6 ?GA+ӂdòyFcx9.dT:alv/79# anTo4ɖB F $ 62w%JC |`xHx݋f禡c9l[  a0CÀx 竅H!:+(Fb5?#)}Ca!~]:-rԮ yf`g2 DO0"2-[ e! WL($3p*-FAKHdM FQWmIrIGol̑A&)EI)!>|Q xbpK~Yf x~wv]榕mI̕4O I o0t[WB| ww@y޵ J܀r7{k%N]mMz,j\Vdi'~ҦXO E(V7b\#ZHy Sx*7-"Z7U#랋/ CwqP ' cs_nWo-=sJ>b`-5㊺pqU)d+vݪGz6I۸7c%Hv|:D-֤s nA|y~SEB6 K-+2[Yc4)Ȁ}S(#js1hvΩ<a ע!ሰmڦq`!l^` p,!WcA8ZB/Q " ~""XSLE[Ki;o $ 5[^iS0k˭(9rx L@م5zT\bۈz lS oSr=|8:^ ^AL#"l8Jejz*ҒeX<~MoKۤ$ET(Rh ah d oT3 IUNީ8g,>7Lrg[w/PrcY%_nL.q 5L4% vb?( ډu'?|&^O)K$*C \2)ןfIbk։n>#K }L6"7Y%Bh^$n 4ћp$T, b*W7ֵ9epvzx-uBP"-;PA8Wy5F6և.Kk@V'ttYh%b7lZ %kl1 nŲ">g!d/ a)qf\^[cȑWB^önmPD`0ΐA=>;ba)л  Ҩ/srg$Pؖqlt9Fc׺ɇgfPRb̳Nr9ތH`Wyam3[!8ST @&yYDlƏTg>GIG|^l \8ļOďS9`,ȓun%R,"C(X5@DUq\ "rҙ-y0ee\d͂|]Į #[6 E97r }]vVƄ؞?ȗ̓L"@I`LrKq U>h%io `4ؐv+ĻhBW.+xP8=^v,X4$krO|p#O1R?[~dUv8 ,8fsK%E"pɻ-?ųrb } !O$*,(@mz݉O8w81]pP bbQIyGSB4]X::_ϟ cTX"LGa&\ϠU{r%AMn00(뽣ч,0S72 gyrT :4 y fˆYezs| 0"WD~G AOi71 ^'27'*ϼbO;˦0@搘G#D>3Ds`i (^bjS(+@0}]rr"[5h)HN\jCepp*8dkWpw+L K%vqTiVbJ&CV?P/K|Ҋea!QřViDDB A_&;DMxA((k]UXW# 'i ? /v$cX= R#[[.(&S1 1t7OvX,rj&ȪIuƗ!4V&H  j~#rI Nrp|f J! *$К8$_#tg{(((ښyHwt,7疒@q .Y0"eKG!G tcH6 F#,g2xjl;@4_+.ϴ!}R`4\Pˬq'O #ECRI.-A﫽[@WEV確Ro6F^:71h'2J1KQbJD oaEd;1:Z[:(ds66pp+pwpp`e`_`-a _ !T&0K#BF۹odp," +{%A! d'4M/joaD7EjUFhs"'"-4$MHcǫuD+1AcV[ uE-xBq:&x5܀9z6+N"p˖r帆WhUYdQmRP5gAt% ?$ 1JD֢cTW(9`@Dcmmi10ans MSnTT~ܖx: 0ܖ"88*8 LP8>zcmmi10Regular1.1/12-Nov-94 cmmi10BSGPxT*76UD -iu9'(.X^^۝[g|Xο&ɱW'9B'B7:, fyy%U>fY%ᾀQ>啡j &EleXg3|D(+Z,>]qWo]\ S'9w'$׾ 󟏱Ҏkh~ )bnt-j- 6+0i`ms'N{͈| ^LadG/27ɚ2;j?Q{"|@`75*K8,TX_ 7ulVO=0&ڴcuNy; ϜH gf)] ؐ Ӭ_ !L!0=^F<= [ 0IȀH'T+$}/PZ23s'r)q3 x k$+r%V;dV,-ْ+DcF,>Ӕ?v&ojY9"&(p(CăƹEC'A(F ̘'R2]k O*bLѴtB0ガsK:*!,01 1#DpXp] 5bq"zI#a#9Tƻ$3| 9iJ ىHh9?U ﵮ(cc{s PP,s(k),6~b&6JhWi#gn[DDhrӳsz:Y鱋XxI 1/*1تJ'<;2C  os+zU;L֧TIP>"?XucJ{\W~+(rZmje5pe`W:bم|w oC <%F1U>]\g#^$zҨ7de&Cˡf0< f|ze-3EuuY"ce4Tj^enaenp ^nsUMO-9M\u|B:Lu]p_lk9 %2 GdfDuS 8!U;Xb@{iUtDW1Ei )AMPP:>/tjC/5r $Iwiq5ɜO0uUXΝFIa#NDEsj 30^gЋ}/強S4a.$%~d#`AXW\ۻQEyPy)Pf}Yh*;yHANƠ-ą[LE?doAqzQof4RRi T~WP^ŧ´BmWCl *oCK]pV*t٦w_WÕ⿵0gWʤ6 L@8d}*}eUN0Iebts׈)9makG@a#pJy uclXW$ݍVI +ZX[ln97e@<򻛰NVgB /H41قLdPpJ.A jlm!&@He8@#@Z9LfR>tnK6ۭZQϽpd.1&E\Sym a,BW!`9KTe;Pje]} -di4-Xd2gUBp:W0?oȚ*'UeZR&O*|{}g{*<" ZmrNpVIq-E(ی*@=T*qLː@. ~_[CʧmI*E14W+metr<qeǪrwqVa:Fe>Ȕ $Ig-(F-H` t-< d s? n єE+Fc2d*$;fP.&2Dh${M4ҟ#;^&8$F+w1GxJ[]!ve)[!-a.96Qfϸ @Nak ]=&dL6rkR誝L$ N0Io1Bn֠()2]^Ia'bWv ){VIn#, @ Sψ)80tr-xRwǮ|/bƣzX7m1H+4ZһL 9THk=+ 7@I8SX i:e3nŹ~c(E=Jt)l'6 r<3Y%ƓR`T0'&%u) !֚u'ƹ0$ 3!/UM07#AՂt8 Q@G`^GRšo7 lECry@<~^OxJH홣 ۾.((㑁k=7U5kn!?5Ñ_0XxCx%Q,v$HH xj\E V-oԓ$جСGz0>Dm qhJ l7 wr9i@ 7"*]$𱓼 lElO]gUH0 k6흃Gb^&r Xxnq&u\1Dbfڅ`M"YJ$b(UH%'Y!ŦMD~RCu:a0^NH>avMEOڥ 뛰9#( Yo_voljy<ى)?6؃?Fw9sj$.?~oCЁm>w㵘nZn bE(h߮Zp]F)a"YvR*j2GhzhD] SGtg^33nnel~UkHf`,3u ;%XE ܑP6ZpӉw+&`DNgR: C$8K~sťM~ ?A ଇ c,}l -9Fimwkf'ԝF"3,@ᜄ6uIi4 2# ~f^cd~ے pvn|]EdXlAaID=ogLm}p*bw_LX#QBV5f蛢hoEЗa9Mbh-㎸ ̫ mhN顷 ;q,רs ZӠ!.H)-ӣW :,yic {xBBbtzn!y$T$)yjdU?@Oa&5|C(Rs!dOq5WA/M @HGwA *@z(ME%)j9QDU>W+ _ӴGbuS54 <0(-kY?'vuʾ/YQwQ !w"Y#P(1{ Qܿ'sxHCAvUxL4 d⍒uY+k):!8$P@4MLWEVF25E"N&fd )!q~Ba7dwlB'o]PLnbn[z|S%?I 8Gr}` uL_f-Lh<!z -, c9@!a[8,Cd&LRy</NAo/ɨ| wY9 #>p޴j!~UC&6 &MÑX =1?I!*A6TPg!fKsm+ed!kvHsó}菔B|ڢ/lU3$|YT X|BnuޯF0F *؊D-&pe߿qYdо!6/EyȨ<-^d\%ӜfuW*9XVDʉw6QK03_úւ:,Ojx& <}k#}MQ`g@=Wʋ}q0Iy!pԻ 6g܆:׭3#\ .]?^Ecd퇀Vyﹾ!^%CT9#_Z$mNU`F}(y1AԿ#(VUAPn]ʗ3'O$4Z[Kxu_2AVēƧ6b_ZDvfL[UNCgs=c(d4C8G&}PШI {5 Hi$fǂn[:X4%]^=`3 6 "-mAbX ڏk3zX C\nUQG!q4Q55+hNK(j3Qamq`wC`E@08$3O EU ӟ2*Pp2 yPӓԷbQ vګ{q 5c4!eҶV48=.|wimU 38`P D)'vw2[-C;)Ȣgx@j30&}q ;zٻ`xM}$fulBn$|Ns ;dNHe˥>cM ` 1jaqM6ͺ+TYGJ";؎UKPԀ?~ wn ('W1 Tؕ!g.耯__*6|Z`IA,V,c?c -mVa; A@,(zp=YN}_=-I̪>. _Ԑm} T% ^! R?U&y܇~JJ̡y@"OpӀ‚ 7#IM7F+Ο/U|%N7H>PT(&Uj2kQQM*yt)_HґXtީ'd6eDaJ l'xXi@vѴP8/Ƹ~H'u#{缌 Ij2f'=h/xJ)XQà6PF]Xu$PrϞ1R+鵅afD2Zv8}ze?,7*sC;d(Jzj=p~)R9Gol'T;LE0Ĕ\lL toM |^8BrY ~4\KVuR^pȻ׋: rJ~Eg#D#ɵ4n_D EX=r×FnʷJ%î0 <捘LHp#u rc!Ɇ6 [-@(1|M O@L^ _`Ǎ#zU5:?U@<{O- k+ =L>ߚT͕6i!ߠD"|uNў$HPw:q̽4٤~Ibj+a&= j:"f ó|#pR/H2S乄dRB*ŷY2t8œ ĶzD}4N@Ey$QҝO! CdR*l0WX)U/9z$aYuZ1Hi?S*gk6mVJ޴G|WuaWaG|)/=1l,Ń썗A:h`h0ILdl44پԓ(BUg ;S’MyDxwbN2BmQ\oTR tZS+ ƍ 8f[[6ԧt(1 u77AhHX}(2UXX;"Qћzo6Z!«G? EE92qyؼ/"q; 'J<2DfF`TrDAߵpBG G)z7 \pLbZ0:/RHƔWI~iI3X0X&N\!(<:UQ~j| VUtmݡ~MmTRPj8*ۋ;>Zyr4 Cf@ĉ42chndc[졪:k,@UGՔ u ٲb wQ&r|:Җ]-l:ȇ4[%J5!iF+N>6،Af,d]N 7fApܞ0 ?QUca?nX#~+=#-EG(uFPe<9mvEۡ JiFm 0 FmcC9VIp8,hOjF:L(]r" Ys/S`fDVTrTUپ(\沑xK‹)nG !YzNH\+Ԓ,#C?/sh1Vxat܌DH8U lE7;f:0ݵj\IfwG4Rqn-gV-ط(84bkKSvORrnx`.gZKD d9Lkr3 2@ ?F= F\P'2]G3|$0')@5E0 ȉuu+b \X?/AeH4PQ[Ⱦ"[~ LXWKAlRgG[Y|V|ſFFazإT%GŬ # Ѱ? _^ 4HV@*A0LMi:*PPF.uEhRձVreS:[rux(V'PhK)W8$rOZ|x.+V8$ЀXDzPdϕ5bݪhrm<P p툤uk8p5p rNa(>s/2倜FDJ גa6]ΦFFPF=r$%=jhea_ r♮_S3{͒E뵃Lp}Npdb;xdeKdRV zCoazH@I{+rȰ6;PӖqdl\tE*־ \ghr-Y*``E C(j$AʓbFZjHB;]9!Y$l6bM("(DXlr. SAnHHfu0~򪘠h RZ}1oRߧu4_FU̻B%@#>ܶH)2B7yAXV&)2v'H"VmP|cM/2?G*1<^aV3 U7tlkֱ] /E-z=&aH|+iB .( ;Se "c&n`Xt`c/ bA',\sd z.TC| u u60;HU?K J8QeՊ- UJN O:* Ť؊]:mEk gƨ2@ Jʋ+4K4b6iʑ"I:IlꠈKrn3NbyV,ig4K .ћ4"?jI\4Я}=+;ڸ<>-V8m#f_lX1ԯdQ "'`!Esya c :p0$ljlPk{/&LZSZx?.L|q?Z(DD^8 K|0a3܃' hQ"Ml,Ϊ`%1n 0’(\KX,WCH=cRvKPQS17S-P:^)&=oNFB-FLrk\x'"/W%, $3w/CSn+p )6D6XӘf*er ٮ2R2Œmp|m vv-7 yxݫS-Vcbӡ!|}CmsS08СB}‰/g2 MYCONu,'nLEy7sF*GHF1 E*g˗l "#01-X+ n ʍ`X9!3f9NZ߾uNߍKy%`(nb/|rIo;M42ps vz5 r\zAJ캲7v W·)Qa#.{=LFV"ĎcW>;vbX(1ν!Vi]?_$E_{EqRta@g :w2|^iy5:s2)'Gк!_-4g0OȕAGif&J@঺,$C@nv9T>As#2Af;&QLarPG7mС'NSMeXWv!n4hrMPܜ3RN+0tpBUR+SՄw`@pG00BXAqBԻu>YcqN`P߆ebjAZڳ>#*WɔBzaFB` LbDH"&Ai)i !8gMŵLZL[·hRi8`~߻аmt~{LUv q]:=ؾ0p.{E[:Qk@q5̙E[?5BN|?*M ,v%6ELaT>2'wĝ+;)*~UnGAa2khHkB(C"_ƒ"$/*гS8DF,~w|jR5  V Fx9WB:ćʉ6V-MvġSPѐ7(!mh,VH($c HB$Kİ@ЯB~?)W~p=`5A`CQ6pO"`M[|˔w̽+ρΓz::H[",9`ew 9)5}4 dKvh>]'60P;Z ((p}tbD 1OD'Uq#% ""^RŚDN0 XS&ŀBa[kE2tU{PݰwPӈ0'd2l,b@VKxc:@Z\l-R{:6r(]\Ruzݎ 2؂Iq7"1R2JLNa DFfAI8; AnpWN2R圿2 \H1m]BX 3b,.-ա&hGǕZR%SM,U_b|ep+*%idx\hȍ35} "Hg>ղ-; +^Wv([U(b df&WMPCB39Ds)7m sj(X7rfbej&brbAABgh9 "i) E($r\&b%B22 C5I l(8d|Ť d!q)c2(r3"JӵPoв%Mh>y7_>=έNsѳN,#q h)Uoa&G ~x,O̬q)hX .&Npi&C33o8afy@CHf)̜Ԯ GZtJe`ylL§l!)%cVp}Hh39~ .-𶣪QMOSe6Nu@mңka@?]/\LG =nk?]N=Rf͡@C9fR &ΒNx SQ5 %,ZL2=d BDi j-(R&>GH-2<^_2 a bc d f+hjln op uvw ! y 0e0e     A@  A5% 8c8c     ?1 d0u0@Ty2 NP'p<'pA)BCD|E||s " 0e@        @ABC DEEFGHIJK5%LMNOPQRSTUWYZ[ \]^_ `abN E5%  N E5%  N F   5%    !"?N@ABC DEFFGHIJK5%LMNOPQRSTUWYZ[ \]^_ `ab @b ! ʚ;[;ʚ;g4ndndx: 0pp@ <4!d!d  0T~<4dddd  0T~<4BdBd  0T~g4UdUd(Òx: 0rp pp2DEFAULTFONTSIZE10.DEFAULTWIDTH3540DEFAULTHEIGHT200<___PPT10 ``2|___PPT9^nԝwJ@hPNG  IHDR OPLTEf+tRNS0J cmPPJCmp0712Om0IDATcT` 0H)0hF(P0H' b] $IENDB`{`&@Z@?>,2/11/2004 MSR TalkO =)w]Assertion Checking over Combined Abstraction of Linear Arithmetic and Uninterpreted Functions^^ F  <Sumit Gulwani Microsoft Research, Redmond Ashish Tiwari SRI4=P>!Precision of combined abstraction *Abstract Program Model / Problem StatementLinear Arithmetic e = y | c | e1 e2 | c e Uninterpreted Functions e = y | F(e1,e2) Combination e = y | c | e1 e2 | c e | F(e1,e2)2              / R Earlier ResultsOutline[ Connection between assertion checking and unification coNP-hardness Algorithm Remarks R7 #5#8 Unification Terminology8A substitution s is a (acyclic) mapping of some variables to expressions. A substitution s1 is more general than s2 if there exists s such that s1 = s(s2). A substitution s is a unifier for an equality e1=e2 if e1[y/s(y)] = e2[y/s(y)]. Example Consider the equality F(y) = F(a) + F(b)  F(a+b-y). { y a } is a unifier for it and so is { y 1, a 1 }. The former unifier is more general than the latter. .ZZZ : 9':PrFUnification Terminology Continued & A set of unifiers {s1,& ,sk} for e1=e2 is complete if for all unifiers s of e1=e2, 9 i s.t. si is more general than s. wV3Connection between Assertion Checking & Unification An assertion e1 = e2 holds at a program point p iff the assertion Unif(e1=e2) holds at p. ] 1)Outline[ Connection between assertion checking and unification coNP-hardness Algorithm Remarks ~ 6! 7 8 /Reducing Unsatisfiability to Assertion Checking |y: boolean 3-SAT instance with m clauses IsUnsatisfiable(y) { for j=1 to m cj := 0; for i=1 to k do if (*) 8 j s.t. var i occurs positively in clause j, cj := 1; else 8 j s.t. var i occurs negatively in clause j, cj := 1; y = c1 + c2 + & + cm; Assert (y=0 y=1 & y=m-1); } ?Z'2..    6""@Encoding disjunction The check y=1 y=2 can be encoded by the assertion F(y) = F(1)+F(2)-F(3-y)). The above trick can be recursively applied to construct an assertion that encodes y=0 y=1 & y=m-1 Eg., y=0 y=1 y=2 can be encoded by encoding F(y)=F(0) F(y)=F(1)+F(2)-F(3-y)Oh1% <V !P52 Outline] Connection between assertion checking and unification coNP-hardnes Algorithm Remarks  D! ! !E  8 Assertion Checking AlgorithmBackward Analysis Perform weakest precondition computation. At each step replace the formula y by Unif(y), which is a stronger and simpler formula. Termination (reach fixpoint across loops)? Yes, because of unifier computations. This result is interesting because forward analysis (which attempts to infer invariants) does not terminate, as lattice has infinite height.t+K -+,bB Proof of Termination9At each program point, the proof obligation has the form:Outline[ Connection between assertion checking and unification coNP-hardnes Algorithm Remarks  O! P  8 <Further Connections between Assertion Checking & Unification==Can we explain the complexity results more naturally? Answer Complexity of assertion checking appears to depend on the cardinality of complete set of unifiers for equalities in the corresponding abstraction.n6ZZZ6 : M /Related work on combining abstract interpreters0/Is there an efficient analysis to reason about most assertions? Answer (PLDI 06): Given abstract interpreters for Lattice L1 (eg, linear equalities, Gulwani-Necula POPL 03) Lattice L2 (eg, uninterpreted funs, Gulwani-Necula POPL 04) Can obtain abstract interpreter for logical product of L1 & L2. Cons: Cannot reason about all assertions. Pros: Polynomial time. Can reason about conditionals.twG$0/  ,wG .b  ConclusionnAssertion checking for combination of linear arithmetic and uninterpreted functions is: coNP-hard. but decidable. We prove these (surprising!) results by establishing connections between assertion checking & unification. These results motivate logical product combination of lattices, which entail slightly imprecise, but efficient & automated reasoning (PLDI 06).6XX,< /Tx  P-6   0` ̙33` ` ff3333f` 333MMM` f` f` 3>?" dd@z?" dd@  " @ ` n?" dd@   @@``PR    @ ` ` p>>fL0 a(    6 "@  T Click to edit Master title style! !$  0 "0  RClick to edit Master text styles Second level Third level Fourth level Fifth level!     S  0 "`  @*   0 "< l   Q/17   0d "   \* ~B  Hp?"@@H  0޽h ? ̙33y___PPT10Y+D=' %= @B + Default Design0 0 @(    Nr`r` )   x*  V++VV  Nxr`r`  )  z*  V++VVd  c $ ?w  4  N~r`r`  ZF  RClick to edit Master text styles Second level Third level Fourth level Fifth level!     S  Tr`r` @   x*  V++VV  Tr`r`  @  z*  V++VVH  0~dm.F ? ̙3380___PPT10.47Lx P (    N05r`r` )   x*  V++VV  N<r`r`  )  z*  V++VV  Tdgr`r` @   x*  V++VV  T@pr`r`  @  z*  V++VVH  0~dm.F ? ̙3380___PPT10.47UC 0:L0 RJ  (   x  c $`      0p "6 ?=   R  s *\; ; \V  0޽h ?"` ̙33y___PPT10Y+D=' %= @B +.  0L0 ^V3f(  r  S @     0 ,$@ 0 Oa1 := a1+1; a2 := a2+2; b1 := F(b1); b2 := F(b2); c1 := F(2c1-c2); c2 := F(c2);0 2800 226  0+,$@ 0 8a1 := 0; a2 := 0; b1 := 1; b2 := F(1); c1 := 2; c2 := 2;N0 200 220p 22   0) h ,$@ 0 2Assert(a2=2a1); Assert(b2 = F(b1)); Assert(c2=c1);60 2#00 22L  c $FKd"  <GHOIf V RB  @ s *Dj  *B   <9? 4 0    0<wq L *.0 2    0 AQ  AFalse 0 2   0EbB\ @True 0 2L @ c $ L @ c $     < I ?"6@ NNN?N +,$D 0 Analysis over abstractions of linear arithmetic & uninterpreted functions can verify first and second assertions resp. Third assertion can be verified only over the combined abstraction.1 2                          ,2 2FH  0޽h ?O     ̙330 TIMING|36.6|49.2___PPT10h.^|+.OD<' = @B D' = @BA?%,( < +O%,( < +D' =%(D ' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*'%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*2%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*$%(Da' =4@BB BB%(D' =1:B 0.5*3>%Bstyle.opacity= B PPT<*D' =-6B image0BIE*v3=2Bopacity: 0.5 BIE<*Da' =4@BB BB%(D' =1:B 0.5*3>%Bstyle.opacity= B PPT<*D' =-6B image0BIE*v3=2Bopacity: 0.5 BIE<*Da' =4@BB BB%(D' =1:B 0.5*3>%Bstyle.opacity= B PPT<*D' =-6B image0BIE*v3=2Bopacity: 0.5 BIE<*D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*w%(D' =%(D ' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*'9%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*2P%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*$3%(Da' =4@BB BB%(D' =1:B 0.5*3>%Bstyle.opacity= B PPT<*'D' =-6B image0BIE*v3=2Bopacity: 0.5 BIE<*'Da' =4@BB BB%(D' =1:B 0.5*3>%Bstyle.opacity= B PPT<*2D' =-6B image0BIE*v3=2Bopacity: 0.5 BIE<*2Da' =4@BB BB%(D' =1:B 0.5*3>%Bstyle.opacity= B PPT<*$D' =-6B image0BIE*v3=2Bopacity: 0.5 BIE<*$D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*w%(+J  0WL0 IA51,`(  ,r , S `=@   r , S |b  8 [ *,& , 6d Q Assignment(0    , 6xiC"? [ y := e80 2Z , s *eeZ , s *e[e8 S ),I ^ , 6nb dNon-deterministic Conditional*0   , <t` = 0 Z , s *S>r , BGS|H IS|MXl , <G1HI1XW , <Dyg K*.0  f , 6M> , 6} >True0 2 , 6 ?False0 28 G  (, Q !, 6|D  wNon-deterministic Assignment(0  8X #, 6PC"? J  [ y := ?80 2Z $, s *  Z %, s * G 8 - 1,D ,, <$E: M Assertion( 0    -, 6ěC"?-  Assert(e1=e2)b0 2   Z ., s *Z /, s *H , 0޽h ? ,,,,,,,,,,#,$,#,%, -,., -,/, ̙33___PPT10i.O0N:+D=' g= @B +)#  0bL0 p7 ?(  r  S (@       #""888   . Bd ?"6@`NNN?N  @ @`v , B( ?"6@`NNN?NS  >O(n4) Gulwani-Necula (POPL  04),    @`v * B ?"6@`NNN?N S >O(n2) Gulwani-Necula (POPL  03),    @`! ( B ?"6@`NNN?N  iAssertion Checking Complexity @`  B0 ?"6@ NNN?N  W Combination   @`5   B ?"6@ NNN?NS  }Uninterpreted Functions   @`   B` ?"6@ NNN?NS ]Linear Arithmetic @`  B ?"6@ NNN?N W Abstraction   @`B  Bo ?"0@NNN?N B  <1 ?"0@NNN?N B  <1 ?"0@NNN?NS SB  <1 ?"0@NNN?N B  Bo ?"0@NNN?N B  Bo ?"0@NNN?NB  <1 ?"0@NNN?NB  Bo ?"0@NNN?N       #""8F8 <$D 0 O 6 B ?"6@ NNN?N  O(n4) Nelson-Oppen Comb,   @`7 8 B ?"6@ NNN?N S  O(n log n) Congruence Closure @`0 : B) ?"6@ NNN?N S xO(n3) Gaussian Elimination,  @`! < BL3 ?"6@ NNN?N  iDecision Procedure Complexity @`B > Bo ?"0@NNN?N B ? <1 ?"0@NNN?N B @ <1 ?"0@NNN?N SSB A <1 ?"0@NNN?N  B B Bo ?"0@NNN?N B C Bo ?"0@NNN?N  B E Bo ?"0@NNN?NI  <7 ?"6@ NNN?N L ],$D 0 kcoNP-hard! This paper 0 2  H  0޽h ? ̙33 0 TIMING|72.5|69.8___PPT10.#R ،e+D~' g= @B D9' = @BA?%,( < +O%,( < +D4' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*%(D4' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<* %(+  0WdL0 4:(  r  S *@     S S0  " (0PpH  0޽h ? ̙33___PPT10i.o`g+D=' g= @B +  03L0 64$(  4r 4 S 4R@   r 4 S  S@0  H 4 0޽h ? ̙33___PPT10i.OmH+D=' g= @B +  0L0   06 <u (  <x < c $u@   x < c $v'  Ql :&  <:&,$@ 0 < B' ?"6@ NNN?N:q&x DLet Unif(e1=e2) = y = si(y)#0 2   0 0 < BD ?"6@ NNN?N] Ai=1"0 2   < B ?"6@ NNN?N ?k"0 2   < BT ?"6@ NNN?N   ?y"0 2    < 0 j ,$D 0 P` Example Consider the equality F(y) = F(a) + F(b)  F(a+b-y). { {y a}, {y b} } is a complete set of unifiers for it. Hence, Unif(F(y) = F(a)+F(b)-F(a+b-y)) = (y=a y=b).X ;[tGH < 0޽h ? ̙33"___PPT10.OmH+MڥD' g= @B D' = @BA?%,( < +O%,( < +D' =%(Dh' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<* <%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<* <{%(+  0SL0 ~v 68(  8r 8 S 0   8 Bd @    8 04 j  ^ Example To prove, F(y) = F(a) + F(b)  F(a+b-y), you need to prove that y=a y=b is true.4\ DP-H 8 0޽h ? ̙33___PPT10i.O+D=' g= @B +  0 L0 6XF(  Xx X c $Ԫ@    X c $0  " (0PpH X 0޽h ? ̙33___PPT10i.o`g+D=' g= @B +  0L0 5($(  (r ( S \@   r ( S   H ( 0޽h ? ̙33___PPT10i.O@>)j+D=' g= @B +  0ǐL0 p4$(  r  S @   r  S W0  H  0޽h ? ̙33___PPT10i.n+D=' g= @B +  0P L0 6`F(  `x ` c $8@    ` c $0  " (0PpH ` 0޽h ? ̙33___PPT10i.o`g+D=' g= @B +  0L0 @6@$(  @r @ S `@   r @ S $0  H @ 0޽h ? ̙33___PPT10i.O+D=' g= @B +F   0QL0 E = 6 h (  hr h S @   r h S r<  t h B ?"6@ NNN?NZ   y = si(y)f0 20 0  h Bp ?"6@ NNN?NGtA Ai=1"0 2   h B ?"6@ NNN?NE? ?k"0 2   h B\ ?"6@ NNN?N' ! ?y"0 2  6  h 0 6 WDB &In each successive loop iteration, above formula becomes stronger. We prove this cannot happen indefinitely: Assign the following measure to the above formula { # of conjuncts representing unifier si | i=1 to k } Show this measure decreases in some well-founded ordering.nP2P9P;Pm 2& ;H h 0޽h ? ̙33___PPT10i.PN;'+D=' g= @B +  02L0 7F(  x  c $@     c $<0  " (0PpH  0޽h ? ̙33___PPT10i.o`g+D=' g= @B +  0OL0 `6*H5(  Hr H S )@   x H c $H*_   C|q *H #""C|q 2 H B, ?"6@ NNN?N l |q zcoNP-hard, but decidable @`" H BA ?"6@ NNN?NOl q jFinitary   @` H BJ ?"6@ NNN?Nl Oq W Combination   @`  H BT ?"6@ NNN?N g |l  gPTime @`  H B\ ?"6@ NNN?NOg l  OUnitary @`5  H B<_ ?"6@ NNN?Ng Ol  }Uninterpreted Functions   @`  H Bhp ?"6@ NNN?N b |g  gPTime @`  H B@y ?"6@ NNN?NOb g  OUnitary @` H B ?"6@ NNN?Nb Og  ]Linear Arithmetic @` H BЋ ?"6@ NNN?N C|b  V Complexity   @` H B} ?"6@ NNN?NOC b  W Cardinality   @` H B ?"6@ NNN?NCOb  W Abstraction   @`B H <o ?"0@NNN?NC|CB H 61 ?"0@NNN?Nb |b B H 61 ?"0@NNN?Ng |g B H 61 ?"0@NNN?Nl |l B H <o ?"0@NNN?Nq|qB H <o ?"0@NNN?NCqB H 61 ?"0@NNN?NOCOqB H 61 ?"0@NNN?N C qB H <o ?"0@NNN?N|C|qH H 0޽h ? ̙33___PPT10i.P@+D=' g= @B +  0 L0 6l$(  lr l S \   r l S q  H l 0޽h ? ̙33___PPT10i.CQ̪+D=' g= @B +  0L0 6P$(  Pr P S @   r P S d0  H P 0޽h ? ̙33___PPT10i.P =ȭ+D=' g= @B + 0 0 4(   d  c $w     s * ZF    H  0~dm.F ? ̙33  0 7p(  pX p C w    p S ` ZF    H p 0~dm.F ? ̙3380___PPT10.R`lgv  0 P7(  X  C w     S  ZF    H  0~dm.F ? ̙3380___PPT10.Rۉr0ӣ| w gֳ 6 4t@,G<@KeY1R9 P>ibikHm1Oh+'0 hp   PowerPoint PresentationEECS2402Microsoft PowerPoint@ybv@@P茗`RGg  ?  y--$xx--'@BComic Sans MS-. 92 !Assertion Checking over Combined ."System:-@BComic Sans MS-. ?2 !%Abstraction of Linear Arithmetic and .-@BComic Sans MS-. 2 )& Uninterpreted.-@BComic Sans MS-. 2 )W Functionse.-@BComic Sans MS-. 2 :>Sumit .-@BComic Sans MS-. 2 :NGulwani.-@BComic Sans MS-. 02 A*Microsoft Research, Redmond.-@BComic Sans MS-. 2 N?Ashish.-@BComic Sans MS-. 2 NQTiwari.-@BComic Sans MS-.  2 TKSRI.-՜.+,0\    On-screen Showon Times New RomanComic Sans MSArialcmsy10cmmi10SymbolDefault Design^Assertion Checking over Combined Abstraction of Linear Arithmetic and Uninterpreted Functions"Precision of combined abstraction+Abstract Program Model / Problem StatementEarlier ResultsOutlineUnification Terminology$Unification Terminology Continued 4Connection between Assertion Checking & UnificationOutline0Reducing Unsatisfiability to Assertion CheckingEncoding disjunctionOutlineAssertion Checking AlgorithmProof of TerminationOutline=Further Connections between Assertion Checking & Unification0Related work on combining abstract interpreters Conclusion  Fonts UsedDesign Template Slide Titles_KnEECSEECS  !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~      !"#$%&'()*+,-./012345679:;<=>?ABCDEFGIJKLMNOTRoot EntrydO)Current UserHSummaryInformation(8PowerPoint Document(onDocumentSummaryInformation8@Root EntrydO)0qXXCurrent UserGSummaryInformation(8PowerPoint Document(on      !"#$%&'()*+,-./012345679:;<=>?ABCDEFGT%_Kn Sumit GulwaniSumit Gulwani