From 8e1702d2dae512361feab9be89af6f30901c97ff Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolas=20M=C3=A9ric?= Date: Mon, 4 Apr 2022 08:08:47 +0200 Subject: [PATCH 1/6] Add IDE reporting for attributes in meta-argument list --- src/DOF/Isa_DOF.thy | 27 ++++++++++++++++++++++++--- 1 file changed, 24 insertions(+), 3 deletions(-) diff --git a/src/DOF/Isa_DOF.thy b/src/DOF/Isa_DOF.thy index 9cb7611..2b79491 100644 --- a/src/DOF/Isa_DOF.thy +++ b/src/DOF/Isa_DOF.thy @@ -1244,13 +1244,34 @@ fun infer_type thy term = hd (Type_Infer_Context.infer_types (Proof_Context.init fun calc_update_term {mk_elaboration=mk_elaboration} thy cid_long (S:(string * Position.T * string * term)list) term = - let val cid_ty = cid_2_cidType cid_long thy + let val cid_ty = cid_2_cidType cid_long thy val generalize_term = Term.map_types (generalize_typ 0) fun toString t = Syntax.string_of_term (Proof_Context.init_global thy) t fun instantiate_term S t = Term_Subst.map_types_same (Term_Subst.instantiateT (TVars.make S)) (t) fun read_assn (lhs, pos:Position.T, opr, rhs) term = - let val info_opt = DOF_core.get_attribute_info cid_long (Long_Name.base_name lhs) thy + let + fun get_class_name parent_cid attribute_name pos = + let + val {attribute_decl, inherits_from, ...} = + the (DOF_core.get_doc_class_global parent_cid thy) + in + if exists (fn (binding, _, _) => Binding.name_of binding = attribute_name) + attribute_decl + then parent_cid + else + case inherits_from of + NONE => + ISA_core.err ("Attribute not defined for class: " ^ cid_long) pos + | SOME (_, parent_name) => + get_class_name parent_name attribute_name pos + end + val attr_defined_cid = get_class_name cid_long lhs pos + val {id, name, ...} = the (DOF_core.get_doc_class_global attr_defined_cid thy) + val markup = docclass_markup false cid_long id (Binding.pos_of name); + val ctxt = Context.Theory thy + val _ = Context_Position.report_generic ctxt pos markup; + val info_opt = DOF_core.get_attribute_info cid_long (Long_Name.base_name lhs) thy val (ln,lnt,lnu,lnut) = case info_opt of NONE => error ("unknown attribute >" ^((Long_Name.base_name lhs)) @@ -2008,7 +2029,7 @@ fun print_doc_items b ctxt = writeln (" type: "^cid); case vcid of NONE => () | SOME (s) => writeln (" virtual type: "^ s); - writeln (" origine: "^thy_name); + writeln (" origin: "^thy_name); writeln (" inline: "^dfg inline); writeln (" input_term: " ^ (Syntax.string_of_term From 74420a932f4d12ef18c3bfe48fff828ad9072841 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolas=20M=C3=A9ric?= Date: Thu, 7 Apr 2022 15:36:01 +0200 Subject: [PATCH 2/6] Clean up check_invariants --- src/DOF/Isa_DOF.thy | 11 ++++------- 1 file changed, 4 insertions(+), 7 deletions(-) diff --git a/src/DOF/Isa_DOF.thy b/src/DOF/Isa_DOF.thy index 2b79491..d446207 100644 --- a/src/DOF/Isa_DOF.thy +++ b/src/DOF/Isa_DOF.thy @@ -1374,14 +1374,11 @@ fun check_invariants thy oid = let val value = the (DOF_core.get_value_global oid thy) val cid = #cid (the (DOF_core.get_object_global oid thy)) - (*val _ = writeln ("cid: " ^ @{make_string} (Long_Name.base_name cid))*) fun get_all_invariants cid thy = - let val invs = #invs (the (DOF_core.get_doc_class_global cid thy)) - in case DOF_core.get_doc_class_global cid thy of - NONE => error("undefined class id for invariants: " ^ cid) - | SOME ({inherits_from=NONE, ...}) => invs - | SOME ({inherits_from=SOME(_,father), ...}) => (invs) @ (get_all_invariants father thy) - end + case DOF_core.get_doc_class_global cid thy of + NONE => error("undefined class id for invariants: " ^ cid) + | SOME ({inherits_from=NONE, invs, ...}) => invs + | SOME ({inherits_from=SOME(_,father), invs, ...}) => (invs) @ (get_all_invariants father thy) val invariants = get_all_invariants cid thy val inv_and_apply_list = let fun mk_inv_and_apply inv value thy = From a331b80095f935b8cc047cb2a9987836ac516fef Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolas=20M=C3=A9ric?= Date: Fri, 8 Apr 2022 11:33:41 +0200 Subject: [PATCH 3/6] Update images for meta arguments list attribute exploration Fix #10 --- .../document/figures/Dogfood-II-bgnd1.png | Bin 14241 -> 10508 bytes .../figures/Dogfood-III-bgnd-text_section.png | Bin 18776 -> 10790 bytes .../figures/Dogfood-IV-jumpInDocCLass.png | Bin 23999 -> 17025 bytes .../document/figures/Dogfood-V-attribute.png | Bin 16118 -> 13065 bytes 4 files changed, 0 insertions(+), 0 deletions(-) diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/figures/Dogfood-II-bgnd1.png b/examples/technical_report/Isabelle_DOF-Manual/document/figures/Dogfood-II-bgnd1.png index 528a8f0f3711b579cad3ddada975e2eb191d38d7..c8a346153f94a7777016eb2b87cb1da5a3ea1910 100755 GIT binary patch literal 10508 zcmZ`pTkyN|M@aA;PIr44{P-w zp%4Ql2F5&TC2EtHmP)$pVfOj;;i@+)l@qka{mt||!{dNRMnePd1t;r>56XA%WshIN z$K~OAZ`5U4m?GYzg*s$2CM_*3iw)um;WHK0a#`Ei$%oZh6H=6qAGV(Zpn)8p=AC-` zYk3DlVRVGmtMDk%sm}G-^mFcE0oCMfyakb=VJ}=)v-}++{2#p9>r@bryxREsyM#48 zA5#eW4$Upy122_F{IPI|A8792iMgc0CR$f#RRDoY$B36ON?z-Jh7Wh0m_<7;f4G|1 ztEtI$a|=y>KUKM)Zq7$cNehaxBlx(Van1=O?yhd;QXh$nmsu)~iPLc>FU{N}1ko~P zd3WUGr|DG0V6XM0;eX+_2e2NN1?6hl*77uHH!p}?S1fy#n6tVcO*-2~vkvS&KX7icwQwbILI4Cv3D zvv|D&BkRvfsG_n2?e;tYAV)M)r`Bv`X)B<@`jnD>$@N$kqA@-3p;^t1JTW1G$MJZ5 zHmFXoFZT51N4}4J?i}C|v0s#uRpr6`(}q?B*P8=+ghB2Ht^;$Uj#j$;y2D!tM9_+c zdr`mu-I_DyK`;i9htcK<>It?bTiAmrF4ei|h30w3!o^g6;$)cAqwM{p#PXHjH|L2a zvqf*H7Ok(mUPaH9?QYt9Z>l1rNA6?c(hlTV=ht3iHXV}QPfxgy!REXXJT;vHD zofax`R~|lLM^?KX?hqFK-X8dMH{ev|F%@D9qDESGs~GBjthR)$W{;Qt&VkAsKo-e> z==l3}=yaH37sHxAGosg7P^Y7j8L~nn> zW#m>I*-;d)#0+Ud=7e5U;T&XFv8tk+DWjYz!9PQ?cfUuU>7Z`Dh?T; zZs)6+&_89gv|Npi$8OPnMFaqh;`l+8??hGw)0&9}jowE;ZMJ7a&;XQg>5MLO0#M@{ zVeL*81P7n`eL|z?Y^Uy=R|VjI2|Yf0ho5_vUx$T|hQnBb(9n}fksU8TF>FBrJL_VG zOgpj)PTwVTj$^ygj-!yNfxjoOXS3Ew%EtX6XkiJcG!v9_kU*Onc{Pjuy{l~V2Gsh? z_c3;b1Z8|TjwtA^j|9;Qnw~#5KZI43r1)?3@iIuSaX=qDnsaPI9J)gBTz|U^djw!lZ;E0)8YI*s}IWPYhy2q1OZSw-^b+EZB z6YV+G8`lPKsYB64J&q6^S}seOOmJ%@VGVs)w*6;GWN{S~Qu#=uiyU*0xS$!HHiVB; zoSuu2$jZws(vdQcy!C2AyC&9PTMv*}=NG0}a9GA)k4<3!fj%tKS#=t0M3z%-8_?cO z`I*euSJTWVrNw}Xh$~(0=@9|x)hYKi_)ZsN*$M7%rwdSRuO$#j+J0$cS^wXdG^AaA6ym{PjIUimB$$&!KTCM+XeIi2CHh~7JCW$dD_gvGavvA;M&5oCQr#))j0bp32A#t% zTsCnXD$UL34g3^-d6iH6M#XfIPjQMoefzQI^1I}P+Q~I%g-K^>O~0QopY^oNb(U&^ ziWX(Qj-q7CW6Q={IPQ5s7+#e;eK^DJ{%4erT|3tuu_uwZm3ZDKHmxADEQC9-o5!5?p^lW z>Rq-Q^(?k8@Y=w27`~`YfFlzhU_njI z!9gWiV*-0!_U&RL+Mo&z!60V<wadnVqLJdav(;Oye_UOUbeyHJYnpJ%r0%cU#)UN}2~6gow< zc-O0*i;Ihkaof~Uo&P*YtV!UWg>%MV_7Jj@rD_e+6?klmS>L(&d--%`);VX3XxOB7 z+3J3$u%KZ?mVcY^TTK050~vdvL#{{Ia7yb)n==0XgNvLEn?*xDAJ3;rM_GMdLW?e( zu|}MW!`ohfhKhV5%ICf!WZhmm>0PQAWg)^4S(g_vI6c3SHXQ| zC#rjT^_ez48b%Bdc4a@z_jL%_7!dn4hOsWMYEUD5PU$fw63) zOw7~DW7_(j>D?-HK=zx}d|v%dwtM#{#OheH>f+BKC|XEu3bB@z=8?pv%y6$ksN5l( zK%$iR+TIx$vJBPnVNOQMgRYR}JCL@l=ZJLu8@tvZ(MXjeZZ=dh5UoY9>=Ch8gmZFPQfRo|3ad^@N0fp3zNQ7aX{i6rVcYuk6snZ{`&2th<2WGr!LzC5*6?=9Qw&bWdor(sLT$@^N!R5y zy{`uER*QdwR%&k;aeCB+lr8)n(@YM-M8QoE;>W~DQFaj;Rsx2yQ|Ed>777YRB~Sli zhd!QSA0Id9z3hlqVci^d^2K^45oHknB9lR!fYy$f5(-G8`Cjp^I{dyVBhF6ef3)ud z;%iWAQgJX@%c4Fgh7DfClvZ~%tNy#hR}13GzJ5QjLt6rTGxmlATU2npw(6&s-k#tC zkf_g%l)F)YziHK+9VR7sz8l@Vx!4qsn;e{WxiY3_M=w-1^F*KT(;-pF+=r!oSx|HK z1kgu&mQ5e^paH_g#{pBD!QI{%KA~{TvQ8&P4j!VPYBKA(56+{Jcl@}}U8L)^6^iAqc?iQ0*g)av+b@0~iNeuv~` zao_H=J9fUJ4pz6omM|X&EfymV(4|-Nu5B7a8_L0CT&mk#4_JrpuX$7O82ER+UCn)$=U4 zLjVDS6G3*j(0XN&6vXAXNsp{TZY`~{fFrff znZI=9v-)7a%HjOYnEFarU;0JV`OALsKQSV zNd$X*=0)hLxKlA3&64}lM+B#Tk0354F8&kw?sy)7nwlC2wV{SdnIS0EJ&9=e(+7OudY1be#TzWpA8H9GemjZClc*U*?z@@6XK{iGAKzo16)D@ zEfNLAI*f}FZIkBh&O&?lTk=(M8kwH=UnISJK%R z8g3*W5Bl%M2}RmIUrHOPOB>6AHvC2&rUw}YWeBTge@TIK?DxitC?>FIl=(*#?;c;V zv54Y{@pTbRoZcR5L33~&*F@gf(Rk$&s1`!|sc*gL_wJ*%yxW62^;djrMZD{QlLsy% zZ|-TJlE;?@7zi*z$yBEVMiK4zc%Jvv)n#t;mr=E`WR9r>*gkyruJnz3)cWL2Vu&B+zK%=-Y) zXGiwJ4eZ*vDj)*BE%PzOyE9$*ThG1r#pAOjKBJXfZdZ?Pa67M`puWzy^3ZrBez#wz zGBY71=CarM*<>{@vo`vJm86U`DO>LDjvML)*pE3YRYq27v1@NY8-Z>CD-1>0_o=FYyy z$=G=*efy(9yd-u7$zKr&3(mHnkLWt0NsuxAi4Hn?+z}svE>k73M08fbSN-?r%N^{B zHOBE{>>AsQJS7`ep774;Syo1ak)qzBluzl*)t!UCWvdO`cFt-5fyhgZX5Q`>-_BNY zNi~P<-(5zGcvWMKt1$E(D$w~}e1wFHw-w%`s*Fqu)KWtO=5mVfV&+%#dk9tL&w<2Y zDRr({7dfWoj=$ycAFtbc)*7>ZQ~`1OH_SgafpxS1_xP-AY+#iysD zfcS!j@ER0QP>8$B8i7E9 zww#WJPzc(G>ia{g*t4VuC4hptsBlqh;@i`#TBs`^JSC}@*fEZtd2GO?0tNVH3XYcg zxFukbPO06I!pyCh^zOM5pgyccjWG>Kna8;{iEAX<7k`3Fs$Xv6TWjr=*ko zNlxZpJXVlc0|vx)FuhFzcp(7S(g;Pwnobx%ufM>p;z<%>?!|;YgizDbU9xaR@VX$D zZs0j=dk5aBh~qo{)E{=WqztV*6PuNN;llEJ!^(=UF}S!?IPfqwo-g7=SuzXY0NEs` zcOl%Wm?Xr+z}-mV&P^)^w7j4gGE@xF1VoBS4M8ZuljEGJ3<^Fky4YF4)GR zDR?Zr0!EL&<9=I-Dkd1oyQ$b9EYFeJa_9O!u%2K17A`eRPdy>q_RbPpSt&gL zDRB2pI&sc0r`@g7KL20 zVztD_Vls%hm~)wMdb(TkY|1vV_DldgsJ|g3^D}|k4-GiSFJ8uILCYTK%K%!7JGJgb zHd5&5gru9(!Zck|8I*Fb7_s)*GZ!7{RnT+8$%}c^tmK{M(Effw3Cg=mGkIa5vWz$W zy(eYh%4EK3(!WE62_i+g@ZXVm8|ApeRYE)lgZP)P)44STwqh(ixQfN$e4C4lT30tP z2zz>o;8XSZvfyhH7t)KP=bfLpWNPUaWd^8SNwdMzv3OHMG79-|^V$x!ur`e3>GFkj z(B>DV5r*e@SgVg7DDg`GD%%J!;II#p=56c;iCV}FwBDpgx1aI4Z2V?BC1^6pbb86% zb(|$7J@N2r@>}_1tJuNJcx_4el{Na}*nKS}o8Dl~ zC@Av-Dl&nN;hLz3lxEr+3)jgHQEPXTr=V8#`8!R-`8~IzWn{~TuF~dv=JHerN(l?8 zS<<*L=_MZUA7Qf{vJOh|v2JHx9E@bdZQnHVbtF!w7BAlYWs)t=) z3xvDkSL>OYt{L~P{vodBwd^0dv20hhI%thJ@0IE}cX%vcS<5#h2Y^0hSz0B0(B4Kb z#O)VNH5TU;njboC;|2h0Go)|k)Ad%b4oQ(QuafQ%O>D(m_weJyB)m=#Wzdy=Qp3EK zawz#Isjoe1Kkr^f)$+U(HodYwheGQpSI=Npt^+T<2#$_SMEkIZ(jlj5lYj+b4zsQW3y3p>!83|&$ zQ+Ky0P2)uEl8&enKF6KRVTYjg#P8Sck~BOAIbux@uEqi^%JMSPGYr?hR7fDF{d9LY zPFAOUz*RN;_MCl!`)93ax^o!=mqTK!W#{A!g4?{Sy0Vu;>z)ICBi@+$)Ff#CtU5gT z9tM!VsOJA`zLtBsp;<3eWy@M&;G2LWUuqTm^yMcG;^m_((FAE)04o=!Q4&f44%8=#fd>M|BeF6g4onIRf1<{$Ybh_%sv(0iZlx z$V=)b`b=@?4y3RcrMbRj4nP^1Qm@umWsL4YVu8kc8}_@$2ipmSDqBsP8K0TV&CTnn z*xNwQ{1M}&AJCTV{YSADYtkxZJ)&1Q^)?beds79AvxRKmFO4(fwVayP&st0$|p|RND1-X%+f`^d(CQ-*V^vBa4Y|L zUO^$;$5!KrcpDiviJwbVT^&E!K8L>ALbp|pejD}tRqD@$YR1AQr&VAlKus5hCZOG} z9~dq)*qQTUsD};BfWIxrk+Q{Ks(xbh6!~_tKCmZ{xAL(BR!Fp8+W z*r*;{k<)(i0U1C`Fz2S1S)Hy5P0E@!&l(r?Y78p2K07Kp`3ike^{dS=64|l-Xt-+e z9kst&x7dF}1vETV`|cKkw0zk5Vq&cSO2CU*+YKsEyyuVj-KsO%qwgBX2cc;##=a)G z(o)WnO?dl>@2hZgOMlOw(f&7QqX$`>jtk!JBTJ8KLs*mTf4-EK4!X!4AL?1y-Hyk^ z{P}c_D8K0NE?EEc%l&-Q*Zn+1H&r+1fF6TBU0LiPR60b;8(l_^3CCE*iUAkZKo#RX z>vwsW)S(C`G+GV*4MJRK@V{&Inapc2BA8Zvb@!|?h=25Havcz4Tn-3O; ze@I@8sxGR+^u`(8#%-}+jEdsX%wH{#-~{2-iDARxP;6EMgx>@I4kf3Hel>EB4!buC zT@O`Cl=qw8!&}{J>`b=g_jT-$cZQV?Ir&L#AX|6Ni#%k)zuU98S|9bJh(k+!XlVM) zOTs}IZoU9r_%7dDh$F0NWTZ!?nPsRmBg}Ey}P%_mbkiVD%3}7BLj=$ z`_$OvS3{Aaac37Mr7lk|?A;yKciH1qkLTcARC;jJL-l{cIc83l9XWBk5s7JN6uV=L z*&)xHksJ=^y}LjD6L058iHw0cVf$M*sd$RD);x7gb#I z;QSIyQDwrn;8s4U^g6&w_#rhVYe~|m&E^Lt9X%fs*(u_4o$5YuP$TG<%3c60h>&Hd zB7Wqb7-2o=)D)d^I!?#)HB{``JWYH;kSJRPA;VB#opG5Eci7=YG?CX>0j)Y8fmi<& zQ(PSLmoM9`)v$g7BprL)#s<`0e~i~3x8Lw>n{Yg%p(niQmaJ^d)vZN2D~po4cdp3D zLdbBLL`BWN)S#nFuCHOSy&j!;b$9DKN(>nS0c{#LQd6M-e;FAc zZoHpnEO?O%DWRe3R$JEYJ+XTy#32*cyv+$OtIhW-8Y*I9>MADY(Dg~fM&D90w&Tin zCw2KL_I{Ms$(3IFq%Ph%WX4lgCnl?QxS=o3DvOYybbel+=<6H*q|-iDJv8uq{0U$2 z`{KSwuZhFWb;;h|y#4jHsAxX{ee~dtLo*MWpTiN=21=qcj%rHjA>>& z3{i0D$q)j5G6D1x5aVj7%?nZ8=${ZpU+Js%6aR-wpq0 z&?9*?JHrZU@rm7Iwq#kSb}?a2U0p+6g@%rf&UaPpfd2j6T?dW~zGDj*jP?{{yQ9=) z#TkPjjQWN|nKYJ)bL6}f2_yRTn~CH~AM?=Am!R=q0wmsq|EAE}+fG7T8E6T?{TWJ?&CUcJW zaZSmxxxLZ%c%u7G|6eLJCIRQ;c71i8zOc=XYe(Dd1p zi^@q$JVlv$pCJ7N9AWFIjWk2T(Jjqnh@z{D@(j#!vSS`Xd-v`yETxLS z2pzm{YEunSXQrhg0q*X2=o4gyOlq?mdFkS%q4_D?U|WnOIoQDZ^Jn{)Xrh!9yjai^ zTxfQjqM|t>MZg4s5pRya24-?hNnz<)Rov7RHt=`9Ax6?PGH0k|rF_TE?9mlG&kY49 z+UXK73ZoA2;^3hX}L0o4Vd#c233@l`^m|UEy{6l%^bB>$QuE_~KCR|5~@P32AL7%yK6@v8Kv*O@luKUGjE-=*ppuBg? z>|i&@`yvKoAqHdSjR2O~naiD;;;V6)XvXDs=lLg$w&QfidXrRcHvY}+FE`QNv6)mj zdGEjcH|12OjEr8(X&*llKP_x|@_-z|M{g~r4Z()ua`5a%@nKsZ?wf;*C`jM{k^}6G z{@L6209i?WD*0Xh*By?Lo)`l&eSV+S@yT%m2C&xv=TU@|E}OL2+Ie=yQ`fP7NH~8J z9|bvP{_8Co7VOdr7!AgA9lX?r7m*1!4nI=sw^kmbQNuAa{gP7#hRl?O$86G<1q%U^ zJl5`$vc-gZMK*9o=figJ?5m7S(CEZwhT@M{bPv#6sI^?yOfqPh^gRl!DKCPK6udyQ zF-6gTQ5->vqW_KHqfd2N zC*!rr$$9Nx}47%R*8SA-=kp9Tc0$`s}7+VRK7ty$5#u|0D0%Dc^b zUiXAQpFZE244$UivQLjP8V&*xd9O+Fwc~ZWp{E%qHf-piG%Q!7Zs$%$usK0>`;(y0 z_6`LW>;{Ikf;F{(w>$esfg%w`fs&{dSC+$0>{w#7cs?&zbmv~%9gHwUjcKeh{)fq9 zOQ|>};+h+4<@T7wt4+LC!4Wbqr`cZ~I!UbO9xF~?`xD4yr)$<-f1q@QuI89`JdG{m zQVb}fait*$(EzTZs2(N}GfGp+GnxB%X_L@^#68Pw9GORlanMA}+_8{a&@;K?UX0&0 z^9tEsx3Ek59sqP({5l{*V1*-yGHQ18msF84`V0)=B9e`w*L3O6;9BV@SSY%EXJ>-+ zGegD@dfd1~bLJ)})A4B3OBEVhI3i8?zzz7e?cAvRT7~g(H`4J~v>sAI-Wi*XFU&nn zI~n3V4R~+Y(32VRz(MjF4 zofKczJ@GJ>>1JBtxZSYu5NW$g{j$6I0^YC_ONA7)v0igu_?XDRP|;W3!4tky&yh#L z#U?sDrNkH+hR>{Ny2XkYFFlpvU=Y{Fmbkk*tmHsLd#;*+4Z+7z|^WyK9~7{e}JZ*I`b43W9=gnha!LsS#90 zm6TLWu&`7hFn0I1>*|y=X7ftQSB+*AYy|1Ktz!L?3JSp2ea1;!Tu+`2e%SL#*RRC9 z#$-gs_}SDyPZrLGipEm1AE35K0Mz?fiO=Q>k zH70_spVk{O@_CkCt$tc<47y(Mxe$2uJODt~csrv~1lAH|WND79G zdx42pk9>ajyp?$L;#o7RkK0;<#3nsklLtvK4`x^jm8C=>_8b*W7^ zZhXbU4RvsxUnqXY7N$lN#5S9z?iAhy03`4G8@>#>#MW%Fr3etq?gNmQH2G02Y9&Wf zLrBg|^zG*h)8y@~+8kgw>(-l5%>F=^(Lkf@(tX@d3TD8ET7fHz~E+O zJq(OgAzAtOsVQ8k#c*K$j>3=BmWT=MNlF^7YDon-XKKJ~G1kYDvHaV1=5enzJFOX} z8Sz}!#)SsVq)6POY`_Z}%J1m^6(Y`!4F1!Q0iJ@6?hLl{?Onq=r>v~(*&UGm^%B%j zEF>i@oxcZ*5<(22fr$nd;4K{E0A`dSn(lu-J_9?O zCZmkiqo*bNURD*xKLJNC$bU&@Y-k`LAUH`05hWm?FX4b^Ye;aw|85DgY#<=$N(*6O1xaCHLInp~ zGYczIARvjbq!b7hCTg=WW;2zf}9tT@P}NIcbud7DeKrrvy~MV z26-#wh6==!Hi=I9MZhEU32P;jgajciq_)U!9E0#Is+O8OZBmp2!EpZWF4BT8q}H%c z|Ayq9);xfPJR^(bV5MmS@^TUbW`3FabNc*gOG-XrVlpoflT&k_fbBhV^XIQf0ZJI; z0O7;b>8!Av9g{HMeO$)@J$uIqQ%?w~;bJg|NqeHL6w=9r!SGaLMX^*Ce)%&LzG17` z$5xWEIQ%(xcN&YS%>5t7oKuJ5VAFLRtUOnqktx6EtDTX<{<%JdN_qmazprEX#7g^I2_Soq8IGx6x~GJam;orH7lr|TGf)yTzzz{CUuZ0rtPmniU=b0;A=oRIkODS5csGwk z0!T7fbw;cdkt$#;m#P$<3qH%APG~9D=9rHKGD^@kcbWm3te-^#Z!whCfb8rGL?6-> zG6&RDkmELw8;%aNdjGv0iWgGXm&ZPkD;PImFa;7+yrN(xVMay0QbZM8DkM^&DnYbd zDTRena24uu6lVxlKaa4NprQP-Z{Vx2=aCQM;`yA%GI!W_YED>f;2S{~0$YLz`NOkY z45*RVL!f&>hK5EAlBox&UNTUJh=(kPOvMkk{WXF5auP>MKH*ul8m9i{h%9wG=jG0txH@M=#cRe@scKr zYm|&G3?|{Tz$;61igZe1k$4eNBg9GQ9Eli3zG1sDbijG$d!`K*nk{Kj-lfn?v`*9- zBOOB-6UQo#Y=xB$p>9ws)+v@O7C%g)5mb|36m}`Iina zIB+oEe>ouAFS}8@`FeA5qkRxFqMtyZ+CzCv{X}7hc7qB}p`(PEpI^$QLQfUi7UvP` zk;Wy{KL`7bMhm(s)+KRK6h~b}p;0wbNheRE+D*>hFFOBpUh|IS#pMOcgW&y^=iVLv z*6p@=!ZLM<`7$uRJiZ-SzD%G@u}uA>fk}8poKw}k#G&EF7_Bk9ZcHfYfa+D1uA)Pw zsEn(^K?O!dzLZZPa3OM`@0Y^@eCdWthQgA#!5!RP!9Dva`)Ld|1y(Jr1MF{Dd@Lo{4OnKl z3b;#b!>ClTGO^c48=U?jm!Z+2gQ1@?1}L5=U88&nHp-D@1!X;rtBqTcR)>bk)@tT# z-{ja4n6?Zytv<$tmWZZ|N<>Qr*`>M1S;hmC5voutfh*ZGnzTCW*qRSDQna_4@|K@g zE1N9p+^sE*#v3+lJ*T6;|Ln18&~4vP_k{3_^A3DZ4XhUK5DpgRPZ)wVwK3Im9^mlc zs&?i%eHtCzq#Qp9n$MXsn<|?U&lEqxnK+u{=kOg7T?;-}I$+u!vx{+js;)PhPX2XT3>b%YO-cNk;&dBay?DL*BL8 zCE4ZNwddpF)9PdWf%z%$nf38b8aM0{vYVh#pd- z*0Q(2pwmFm&JhyQF!&7G9rrt8I@Zg$&{^M1@BvItux4--^eJpf2t5ox@&{iZvytaO zzeK-;q={#u)vw*s)l!7n%~{b|5Jq&y3S*mr@_`#;?Oi*2Mf=cQGW2Jf)y{8jbsM{H zgWl4x$(0%o)@5UJjYUVvqjbjf+*mPTG12_UpTT&2)n@V}wa8S+L!5eU5^$2dnOsTeS&OOB@-g!K z#0rRo&|FL`Oll@hFtS0 z7xgx}4t*mH4dq*XQp5dAj2eIP2S*dFz4nsJ>-npzfh(lT-MQ16rZS0sqB2XPWp8z{ zk(j;Ub^FG+i#~N7ZP~i;I`Im#0=CL(y}IjVbf^AU{J6(B?>G+iFREr0ujS#5rG_nU zU*RGTQ^SL!oG1Q`ikph><%>0RoPNBq-rFm^rGZ)e%)ZsUg$|`xGfVve{UEG{tawfE zO-)JLN!e%y0f)_jtj$)rZen;L`SyyIy~|9k_KrDxurgN&SY> z+}V-pWMAs7`Pwhdm~!Dlb9UT@>-PK`ZHqdEin_Iwy3>oO&F#&Lu8}U!_lQ@B3;WBc zP5JiE7r}?X(a=+TLwq!zWKW$Nk#os=Td{6d_+^AloICuEXO_2<{;yLr5nF@ZzF1S9 zV(w~8`J77J-+4V;CS1=RZbhd<^&$0Tx+Xq_KVrhwLu%ySPd<(&uT!sgmhzXBZJWDP zeLSDC&f6ctX2QrX=eOj2D4t5+>JCwEm5+{&r->8BySKX%eOO;sUudt^3d-)vD8FhC zWLtnK{OAn}1M1*}1tLX1L9+o7&|z64o`y_6KQ)JZBhNlBFgHQy@n3@_`S? zI<2Aexv_QxLpqKP*4}8(7C~WIs zO2|sbLdQVF2Te#w$m3vQ#-$`8_Afc0#Y^AI_@6=kGmeOkpmn{H;^nbq4Gtx28|IgR}Ql39=xfCqiOszCTEUZm!907CiF>|u;{O$jL zzWncu|3#_!zm$v&oc~SvUtj*E>M9&BP=)uqg1VjxX zDI%!i_T^j`!T?ni!$*<=@FQ%*EEhPA^_$y=K#C)jP*hN`FhVQ@MM6^mr9nk2f&>mI z^~)tv1r;pBER=#lEXyN7_K+aH|9B>ws&{Q2*QLAP#aTW(o5*0d?b^s-zcq8onNMRj zhfNeW^sG9sFD4XLz+V_yU;vH;BJP1S!T54?#<#z z8*n8>J=|Aj15iLa*N(U+Jl}3h-v$pr$pE|}=7%QQ{M7{fFEOeOsD>iy#p`&L@t@9w zYmm!T6uY~-6kJ@Z`9M%mP^f5VqTs^W=Uq({Fy{YGzZ~NyDr*1!;+)Rs&BbcD7+EZn zmcI}iA1~DD`BFl<0qobo@Chsrz2~vG4D{1JoS|Z9Naz!~lFOqW;sf>Z)Xw+m$ z;&DWx$A^;{Vy4dlNPk)EsY9&gD9~uJ`zo8s5l5v`Dj+8(r&TfY?0Pa6tfQl2!exdw z97B*|Mlr#*Sgk88~gw1$sq#@=r$5?TLwrEe;im14tG*c9nVVEc=!hsM7#oOBk zH;<1g`$f_z#lL>3^Z_^j{K@Wov7W}m%Uje}I}~$^^+&q~pwMK%E|lSgg(TQqP880^ zGlCZ$O0t0tJ*%Q&$fPRBt?lh7&2tWaCF6%=Cj&}D1>N!Kw<4&emF|TBY+ty8&7JS% z<@IfUBrYD@9n!|e=5B;IX2cn4CQLqc{$M=CG~KwbUy1o2TjS8Y5wG)lc1UNjh({7~ z%gOhCeK6zpv5K)?uKlXpV&@+a5CBQPZpg-Hw=M8{z9eS9|AQiOdmrZST5*BDM1&Ky z&+P^Crsm&iTWTtrV5rhf1MDzTV3RnuN>@HDOuJgAb)ud#=3iwBBG$Hu?GWBHr2cE( zt&u>~;X2@{D}PtCeGFNfZ+FK%a`U$tI}T`$nEIvh{#8kIG!Qkkcy}NT|KH~SM^XSz zwvCCnxVTaVjUWD9>2nkS82&Zgayfii>8zGwPaQ4Ll$4ae+FfnGuhf%*frCp8i$cKT z#;zC|8mg4Y;T069RcYM~6Zn?ydYSzJAV6UZe-y?+E+r#V2(WTx2ZwsahL`(O@lXVU z;@DWk?@QHqvRPcJhr*Hqnx!CoR6IO9BnZUdUcG;W3Pilk0I8vZ3WGsc7=}Ww6by|P z=_Q3qsT9=abV8(?-M0k#7Ypo`AzGatth~?r2`Y`>6hprRftmg@KZDpmKwvFyv;%~j zIXO9*oX3(3Fq+*yy!U4-$~hDE|3U^rm{2=9g6MxtKLB=ev)LNQ-Q8VrZzzg+-yZlM zl=$rt8rX{&RzWc`GP1Z`89>9slll67!tOJ0J6~?{3UiVFiwF+%|6|xp);CR-OZ#%< zYN*8{SFHc&IMh#cKB3njx3Q7MoiIB+U21A-Du}~HywcQ?PuXEL4j zZbleE5}P)T_+JgdhxrX+4Fdeg{wv~m3VlfuwfY#xlv}sa?cpS-slrbi-SaG{GcTnt zW+nK%9;MQJ|3Lu*u$=i+CgXn6+nS|yiYgdZz)iVSb?84fOPB$vk*R2sK#yVmj}R$H z09Hvs!XBUTS1STGUwgude#V-1{apqs@*k%gk25;?7o>zg5e-D+v`3iq|A99YzFD8zg_nqp1Vqb9epwKm@+j$0UcSNCAAp z9_DZ!ptOpATw@%Pf#?p9>$Js)P+zbApXK_$3FOXDLSLvjUNF{+a`ukrag8NWr{vuL zoRyh`VwVf_3F&=Y{AKLopJOWZt}bs=oOD6gP7kEMdbBJ z1N8zF4mxV|rQS|OUodBnyw^gxs>O1x;oSg=yu@QyiCk9v$F9E5vuVKY$fVyCH9x~t zjfW$)w2k-!Vw1Mwz~G>wl#~=WMyXWh@$t6^_wbPE=C83SV}-9B`ekyW^4J@Bd8l;1 zZGa~?@ukFT)(fNhxmU>Sz7~31v>p{E&~<*gdhtFN#PG#;X*y^tq6$gCSS8#Df5p&X z_&}S;KY_|Y$@#BsstIH)&-HTiSG}n;G%Rdlbj061>T;u9-N)!{#XP4d8jpLE&vWo0+N4j*mmcDFm+4OEVe(PlVR#6K{nv7KXg#5Erc9QQ+@}`3M z+EdGU#tkC6>R!liW<>j!#RC~7fr%BbF`hMaXW?iuk?SStEcYqA(z&bJsE6R|atV&b zZP<9YNHuHe3Mg{Y+Y5_m6&*e;s{Y8B%e&yp-+@ z(Ymlv?2}BsDhko3uh$tZQpG!&sqs>`IldwVqu)(lAI|UkVCW?hWGmFFzWpjyG_eu? zH5h?WRD&|ZV!Nr6>@V-q2_>-*)u{c`W;O^41@g{%t+`0GV$KvC?nZI=w5FR*{B`^B zX)k8JQnLXv`sdxw+w<*QWa01g`4R*{GjB|8mh<9Wo;*7M&B6~&{RE>Up|@Stew zOT|e*-5B~_aZ)LCvH+kJ`1t_^NE>-$@_BI>f}3E+hVY=N=(ecYOW&6>rDe_9$^d-X z1Np_pg%Y0uM5TSqeQ&ah-^b0tI16Auxw*Sbd;{z}Li}%6f!Rr9+{jf;{aRf{9gatG z&oX&<99L)Oo1NOGuDDDN%6vj;-5?BR~F-m8Ukpq)BDQ`hGp_Q!I>O zE8*iSzL9r?{w~&?-I1Tv(6l+PII9#*OJ0q*-(Pp6gUZWk&RoUsp}6PDdx+nZ+MK+( zb%&AFicWh9cK%Q+0iF3CA(k>9S6ktF92c`V>XGPGin9E5ngw)fMWlV|jhOqhWdQZ% zCWgV|wB)_mWdH3_xO55&vOe}|)AMpRS1|B+n*TE~8)2scRIaA4zn_&32??pbAYe)4 z?N|Utz1_C^y;;l{TM(b?lmFu>5CC$KtDR~D4PhXDrx$<)6#(Lp_@~M)74&d;CINfr z(?!`E!OmlruMM<@OVzr7kl`??^hHp6F98cr?C1BOirwE@(->J~sCcORQ8?@-=AcDC zqEW4tzI2bym&oJ5ZRZ-q{YUqX_f#I1<`lJ0Pj0KVhJif7ngpBOb#{e?M*;?3;? z;e<{tPpI^>24fJ1EI^(JtBeN2Lu$G|w1$G27$K)!!SnnN?t!%odh!rNL+O|lW`O%2 zY9WQcYo$-Lxv=-v8hv63x5u!5E6nXR#Fm*~aE^J_hMk29yAi-W@o!+a7__c(?U~y$ z)f@qNwtGYNkSqphT5OMfw;eG}&3EoGr1PkNWtI1+8ry?*xqP&7b)71Yo<@hRQGm6lywmkb>?pnf&zOE4 z4$p_m-v0i62FF7gklmL(K$(J>=kx7WD;?7d6X4&Ab*Z%y!4RCQrX-lfYo_&^tu#X% zJRi;&d9Hduw75(d$a65aQ>)akhczd%;qHGgFuy&l*~aHkf~Of4lr#lTArFPiD=5SY zruP0SazV#y$g^CkUS%c9H)ef$e#Q!lPwXBC#46(~#QDDTl?#^Dk*zF-^~{j;X@~WZ zb5_=&m~NOsL@ZPpE23(vaadKyZ*bDdG@}Y=FA9u6b924M})v`e*?U9OoNu`quhoW#`G%p}hvly&@W#n8O#sAvfg($PQx$OST288$2 zB|543NtDVVWb)ZG5vh(kptp!(A9Pc4DmC#K3pD!a*ssY&<{7*c)(7QurXGwI_zO6J zO)E!Bio17P#|gP)_%U~kNWheT@EIhpc6obRk9`~$#LNLuOH*=F>_n^8m@6C#f096| zA9*O9NMV>*O{YLF=4-cQi5*+=)N54>fF$fqFV9Syvt`s&B7|6-a0qN%1JXn}l8k=K zI4q9l_7;EhjQwRUsmIxJ8^FA*zzj;9d#;P--Ma;h!i(dfv9)OV|8`4*n-i}_W60$4lMqd zcOz0>%SdE5Wz|VjQ+@Mp$EYQUlA* zF&_l(PA*i0)KQfdtP~s9p!)G~Akq+ns!l1gA`-i*38^v*EN*wv929fMEMWBD>pegW z2es@e8|ZVr%rYGxui$i;7&NAA{>xI1Z$4UJb}y0@E>(Z$>tTZHv2u>m z!_nLdU+^d_TEw>}g?IHE_VzsfxfnMsCDc6AO6$-z5}U`iT8Eo`xlSt+@BJ@j2gEXU zqvmE1GXm`-5tn^7+K8^n^@cArvP<|@?jJJG=8vmtZz{aad=R1rOZ|XKB2LdwRv?Du zSVpRAz-e#rs=!ZHB^7iZ0TO1nmbh=2trkH%IS80&`<@OIKNotkW3h1@23`{rDu>UJO!xVP!}UDLnnz72y~i19IAk{_8}U4I3++Cj`; z^sYk%J(X0D&+?p=yrGH3vH{BSK$QXszp0)=wLDP;vUm)5I@Thcm&5dDWYtrdhm|*c zX5Bdgcj6T>*i$p8ACuFuLaV~^Ph0&e$l`$IumB4(;9@~QcA=5O8$vcCW^rEK^P~6& zx4lYrBDJ%HO0Wk@Su{-=8S!pRil;r6Zp&+;3e~dV-EZi<4dih2BgKjb#BaGWVxP6* zX74p>q)`Kl9!WHTU7M8L#taftk_AoTeFt*Hg9?-39`x&ENqDFP@DzN7Y2c<~Oh31+ zq%v0S=f9k24?}%{~Dp{*C&eZQ-GG-wz5ppJ35Lnv!7Z0#2?i^G5> zkIAIEKxbtQaX7p?CMIURHNXi}#=b(eLaeK+>n1c5$9<;{tW^}L zSxJlv~{LfO_cUI_^|2Q)MXxv$%>6TVS&*}WHGcV5MJYOY0+<`>_7r(Uv?mj z=0)zj27YS}mpHXgXF+^1SZ9ocb~fU(NG>FI?F*kd)3hi)m8#6dFJx?Jcf@W@#kn_j zizSq+_E~R5It(jGT$y}EAhc%Kv7LmVb&5jKZ&$>^J&+DNeZhCnM>&?eh9yWcoPg|u z134^H?JJa1D;5LDkhBvfNf`lGbE1%$_tW(-!NCPzs$4BCPYnpT&T>|eU{oSH(f+i^z(G7Q9SLh`a#;@7SIYr0PmQgO^*)-yLvAN%Y_8O(6Z-D`O+K}R z0k}t#*UNITGEP~&a1XJ)un_8Wl6{M$j#?lZ{hAn;(I}`<_Iso(5ybFgVJ@3}Pj3Le{F^v=)|bDaE$n zd{TJ7`Euh{v~16z@f&@05U^*;+1y*u5}5K)E*2WW&oSp!_d-`@dZBo~dFApyt6nAE z8!ZBHvUjXX7AVKXlWB;x{EKb)_AU6;f(h-1ob+wx&VD3-A zZU(O*uz(;lAV)F@`vrT3POI_9rthbB1I!%f0$r*|UM*olIYxmn;H=^X0ko50+ZD&= zy?lQkdV=oYy^{IEm=^IeNCVrs?;}Rk-AY?LW5#~5TveJ1dIDRe=Mu>hq(>bLb{}vu zm^Y}>Q}&Qv0vv0T)~*KOX;xbM_d~6VF?D`(yJ)ZZn?tPS*I`D8noz)Mh+l=FIreIC zqgHber|MB>*Crdx_-SIU`hi#rr`H!!tX5`TUw{DX?M~2WScX7$mtuem-NsTS$rj`Ry@a~ka-lqh7-XWjJ2y-rKY zf+;Bn)EtlogaMC|we5FVuA7t`0q@jd%*Bds1xUoPnXnovI|@%oJ@Dwb8YBIcgxp^a z$vbdM#EvjcWs%9iQ8iP8ZeNh8#g|_uKnhMVs*nmeTYlrO78T3b@7=cV(ds2)&2(|)b7GCg-p6et1 zdJ&Tjm~;TyVi?fOOsaiRR!+UphpH0XqY2pmt&r}RB90s zFa1_frIMW*!lJ_fEA$t58F!BUg`Ta*F}Go)`ImGA0+8R>2RYUu{U=`&B+!+fE#rSv zH6M%Jcq%fuzHaeek|5jAWJ!<{8oW0CzS_hacd-#TaC%cvrdTl1U6p^7g>wJ z8dv-0hoEgIt1gE@>sS7VR9%{?QRP+#>1*C>rrlS`f>O`N=m)m;o|M<)f*R(eI_Fce zKHai9<60RQJ2GMg0YnM~=I}Oat{MLv-w_qbeN>wQF*sCx$jP_REM;dj7QVe_Z9zoigrj&|BQIWMC(l>D5uuZdGDiagsQxI-{qy(JD5mr1Fn2rPG zB|=X%FPQ9{Uky!iw0To!8x1x@PM@SuC}#5Tu9tS$4QqF_Z1BTjb2s~fOE9jvU9^%9 zl=S%~x$`uP03ng18vIE#hwF3;o0ia*U{8W8w^Ba7;|g#-J!DHPXv61G`5PbmcO{IT z_fS@aU2w<5+Sa&^{2X>G-{kqR{uuP#eUV6R3VjeM=iXb~t7Rq_9M(;@{$$HH^69M+ zWis9Ljq{tO^YLvcytiOvW%oRJT2y~yK70cx5t7f~(S)W{7S}yScuCaLFGuQY(aq?- z*-6l{iMxZ`bv=(0xa+95=J;yUas0dMVHirr>n=-$89>5D(2LVKa;Qc)^eEUdee1r` zwjN`|(1KHw5{gyKyJl-LG_?^(&$9{G@vmnX0w;m#7{8!xXT(g`zBu7FcUg5S!@|(&j7FBoIU6B{C7g89m6L~l& z5K7NWN605$(w0FkBHOr7#QdNfGE`Jv$|mG@XDgB%vn$kIR_kMlaAwGhW+=pB9nw%x zkH@Dq{76|dHf?V92!QlUB)(^5lbsv$^pDSB0{Z-t9QZ=z5}yR8?vJ)eo2_W{?D;uw ze7~o&6}z2d($tqbcc}qaXmSPL8Os_tbh!dPhF$0V5lL(&6Wq?5vDLpLZ{8Ng8ayy3Qr3@gq?s1G8E+Q$@oszrG38ajl9kuMdPS2atv z1eLHbQvE~~i}8_gophx2At zJymQlg^5WV^b;9bnPUzJ_%rLc&Be$sAlXP4Se~;LH4i8@9JrG3pEO_K}znf2p+%d<*#s=OE zVi0_PrkX1lMiJ8VDx`CKvzmUtx~=${xG%;jJ!bE3W#abglIe7g<9v?I3DaT8`;@DI zY?MreOTSR1oDm(Io!fBKPpP<`0<)v2QWI@koVhm5LHL9j^D`VRq8PboJ;>9*9J(`E z!nliHnBdMWwnGYaG7-a^2^b9R%N{vTgc5pKhoGrhb)n@YTr%lAkJMaevClrMD=Qk@ zr}&}Zj)0*FdRtVQOw=mBWXXfobR>=XO)hS>cQZAuZhEKYU_2=S!0Vd^5nM|;Y~)$Y zS37v`B*>#H%E)Ary*66hT5PmgI}9K&$8CZZzQqJ`(9sFfl$xn57LU=ev2D`eO*j-= z;-@1%qhhh!q%J3O%T_<`CqSa2P@`8DAw01dKD5&;lE^9Rc59tT?LJ9zp}B}r*`^{9 z6ID%9tglBXOYXGm`nH6#kk|Qy_=*B@snV{>-+oVH+*FL}&=bd6gPy6OPW2V;GrM7L zKwro{zFArZth=@Iqan0Q@PY6bvee8aYSdsCB~un1WJFZH?(1@OxWg@2zNfaH!CI`; zRhS!)Au}**w%tKkzxU%tHL;{-^1VCdr;=Ksuw8W;?em0Yd)0SdEu#}XmC*MD4yWi> z7Y;_4L*@*A5$npW(POjfv8Jge4|kYmV1&Zh3y4KofNi~o zc%V|bY8`0QsnP}!!W5tY$pwrqE1w2+LE{^UFt*Li9IFh)WUS!Ln#zK2GVhczOP_4VWk?utS+6kVibgokiT1; zHG3H^cxr>iprVEk6uh~h$@1sON;IGM{crudlwWPm%yr=PoPnI?3*~S^Sgfr1lb0|w z)%^D=pex%ODeDm%?9|`EIQk$tAc2$3QH@AQT&ct2;!wbK zms^8a7@_;4OHm1I+gNX~9FR{qRAv^5L9NqP_?47s^`*-7Bu%w>jJ^9gL*HGrD<@=z zr0IF3VbE#V6O6T$mZ}2_pQ&ihGTE4WJwX!4yrp#8H!pGPA}BfBm_$X3YKFIYjE6A# zz)I`#F&T~g)|nzi9U{H#EA_jR_@1^MiT%YQF)8K_$E+K|;Ujh#?4z(*M}Dw%(;H|7 zB2P|l9~{V87y;^iHwUFYold0oOlK^3NMXC*n&_7tayR z2Jz};jD(Pz%6G*s!PN{&<494{S_p|0Ob*79(sksFFcKUt&g+b*lQJ4b#;H3UaCCE+ zQg>G&6hjgHOwTg&;mN={Y1p-%YR2V#^9fZx?Y-0QyR7Z z=Ppr|U(THEJ?N`ZI2aMr+&opYg4vf{8N^9FS34*NE(ZMF5C^X$f#6XK$5*?!oAudz z?=aYGXVz)>h%*AkrjJEjRq;ZoWrTXg?LNHebh@oXu3TB17<6VxVTp;U60h)h#cQsY zb8*JQWomE)<@!I%H)t;xXCgwHYKYV*0fBmSjNhO87YzC%vwoUj&9lYHl-2{To>g~) zzX^q7W!T>*o|Fr=SYMx`J6WoVU9&^lKP=0w4w>}e@BlbxDaO)mm+21!G%E~Mc z3$s16_1hzDSN0X38_$eqr+t@esYG<3jwSt zX+j|Gh$|!nAGRTfHeq_;o}OY3bz`fO#3R+N*y8qhR@rl zbrUO%8*RCFLDp)mT7O9$-v#xED6+>F+8?-xg6IRD6c-m719)fWYjA}ix>iEk=%^5q zoEa!Cu>adez%C+UUF_d7=-W>~ZSs1n>vP@XZ{f3&D7L1!WU;ed1C4WQ_QAwp2 zDKRN(QUA`dj|KeDJ(6Zll&+Fk6W%9+-evNqLYvz|jEH7RC@(L+6D{sVfcc=sELend zwNl_KEF%*c&b6L~(SUc6T-Wo@Ahdvr>!u=Vif>(GE7aH}UwDa#qbb|fNGVc}5(aP1LDXOgLp+A>#;tMVnZ}5!CxjYsr z8N*(rqX89Z0X{;z6D3eqTl`oA)+5^_6!NKDd|s~kU>JzOVf>nzsVvKryAwwiucwwb zv)x)zZC*0p$8#tXj#%#qV*FN{v8-Ml_t&&ecc+!?=d(wS>ek8h_`>2+- z*g}b*EL`AeYxt~B9!3(&W%znEgrmIwqe%vf|K+S9SWGt1Ha3o!e8emA`>fzsS%Sry zEuqPD=R{(?)X=V%-`w8KENGLN&tR(MzZ7V)7xS&xT(Ax*c+{81`gRt_QE_le4vd2; z#YU;Bt6B4{#LTAkM80vaKCW7#Fxz>aRz0$Mbv^A`%HoScx~t&GtcCKVPJUmqp}dBI zJQg6A&sGyX;ADQw!_@PtOL-d7(3I2`^t!UY-ktt78jmK%^VG)%xI+<+V(e4gIG}Q4 zrI$7ruN>9Fnz@v zr9!h`qd#1~1>Ny?jQgUqZn6AWw@l3Ir?1X$7bhyaj@R3Nj-^j~DPS0nMZxm7BJ{Hk zD-WCi$Egs-Vf`*ntxi|yasORfiz4dfe(js{QU%0Pn{?!jAu|Gu^rwK)TJuKmWdeJt z^_m*`XS( zhG(sc4kF;b!9%0bAcokphnGNt=4&hlzR!(R5x_83C;Sz27${mD{7a%WS zkeq_vKz&4;K+ofbdfe%$2SCg_9{y_YJ8qRsJzWBfzE$8CKSHy<=^17etzT4uBd6G8 zNITl-+KMjdGsji(klQtwrGwVeTjeJdo8pTAG4WG)O+`ltF4FB-Zllx zf#crL{mD#TfhJu_0+`I&Qf}|N{0$I6rDADriK@j4r*=O7JZEdCq3ke!6I1QoG9f@Um+&)wsD> zk0KH#!!~DMHO?7Jn@A$E1 z4|sTdA>ok7g$d2$L_@vN@!VAeSVZ5QVDrY`{?p5K2~cJP``!0yQy!I#A)mX0)B`W_ zuIb#aRGoK9`m%J<%b|XzqF>Q!kb_)Zmu5dSf3Rc-+mb z@lJg~26ashArlaAW+)2qR8AM`{(PTaZO3Q&DYmi@pgd&g{qHKx3(V*yq40PDG5nj- z$pkDE8Wh=^YU2kaf+cb>@in$6HxJdsOT>Df=V(#9R~D;{b?d7zUTw}W6SJ(SmQM)y zJn2fx$_LGcG?AwWG**ry*udznyrMMxGQRSwW&?2CIUQOm#oaGn;ue$^`y>t<e(05IZnmdL p@bN_*FIIKqb!B}H>dJpY$auYw`V0?b{kfqmDJmyYEo2bz{{Wgk-!T9H diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/figures/Dogfood-III-bgnd-text_section.png b/examples/technical_report/Isabelle_DOF-Manual/document/figures/Dogfood-III-bgnd-text_section.png index 0773ac282950cab10f16fc7d4aaea15814ed9176..ead484ed25bedbad5e00bb2c838517854a89bf47 100755 GIT binary patch literal 10790 zcmZ{~bx<757cM+F!3h=|g1ZEFcXwSJ0t9!rU_paB1P$)4!7aGEy9Ad-?!LdT>Z`hc z+?lQI>9ciapPuP+o_@MJQbkD`6^Q@|002~383{E2fVzcT%OgTVzCRf4j6e!lD^W#J z0H}>aeldZA)XB_b)D!{0n;HNDzXQNC#1wc00B)=RaAFJqd}#oH=a|)|DggNb-c(*% z0(k%L%K5Fij+L>xj)7-l9)?f`&>0r@W;NSz6SLgQsm*9ZXU z&}1bLy^dr>rn>zEZ<+*?xW$8LF<<#%DGNC;4Ghu`m95t!`2591t}@`7b21qAy~kp z3amWyZUh_h=eFSk^q+lapOx>z8IU7~3+jrHoSb~Rs$=&Qc5~M9-O1e2^1k82rl_=Z zNr|Ee8OAysG9Uu>r7(`XQE{Q@d&3nU{LB9md~YY}elQ&g-_~ZHn}#c<1^T8l#m8-> zZzgEC-YtgY-NyMcEc`Xny5~vEPg#GKf)bu5{YK}lyDf*S7|vsjQo?fm%$flpTZ5x$ ze)Lz?zakWU-89{0`?Cz4a-bn8v4($!SJietA4O^-HTQ)4T7~m^y-@$#q;T$3IFBwp zJWGRf_<#a8w9Dbtix$%*+F$}3sqFa5v=yGFxRy^Tp17vxZ|l}}8()IWb{AMZEK0-e$x#`~ZcI!M90e0Q+ zx+ZOg-8D7&;5~)YdoXQL2nOE0RZZ_;uJI@TO?$`tWkm5%GI!kMBz8c}`H`UIsiHG; zc`^1Gazv>e(}Bx|sL2+k_Tn$SUi_uIc;|S!iWxa{NB zW;f018l7XlnuKaR#^62Vv0)^{<5ZXhLSn||mSC|FzW_S!NuS<~Hr?T3gSq_W!~EQa z;FEIa4V=$3wd`BF6;^&3F>y@DkZhzzYF6u&C$szQUlX;CIGKjgHaXQN%x5(@LBBwM zZpY6vKL}ukR;}R$>FE(vzBT@Jea4n7iMQ3yvP5>o`ot`N-}NsxQ{r1npr)Bw!R2DQ zVy+qGc(=mcs~{BVxnE~=XcwD7FfG+m2<1&^!jSCvc7q=9_$V>6OF6i^*U$_AA}qo; z4h?@!R7|SB(DPqBQ)|`(c{{ViI5ccg6uvGzz&sdQjFp7^pm|j1<#y|NoG3s3;a}|2 z{^w!knvK->d>Qvy%#&eC`?tR_SPB~E5|V}3ZcH?!J_rC{`Swuo&=NyZSY2h!W&J+b zt>dKafCnAe^0yh0q^x1-214Fgk^N_=z z@7r1neKh0Cj?A^e$Ut;lc!{2(;B^ob0Ayta;4VckzjYu1w3BhwhDYo+X~{(~yM+Vo z_U2On@DchfTfi?hj!?*S;?J;rW(gk};knl~7FOU@_x?e_>tt9}8prtP=pPFU8R$Eo z!{SOoXb@ke=NVJU5ri?3%zeg_*22EKu{J+1-^Sf_WMwJ7~S&{cIO+IBSM#ez#rAwld(HN6e zdk@7IQ}mC2Edgn{?`5!s{V;|7Da6+&Fya3#R<}#HI>brfcBdk|F{~jXq9J4US3?z1 z`$UhI-zl2g+^At9f;9t!Z8}PJoBQNT7zsSX<^8>`cueCQCrSlPb?0p<39vOV=s#E` ze}KZyL0td3lU{WHI$~KB5U_Vg#;}>C$M$DNM15?^W_)K$+k%O2=QeG4)pH0FCbJEi z(}>HUJgvdFAEb}tB3bIs$LC{3FxN3GV^bG321nFX#6qhiuZQhx7P#4cLdb&7i%)vh zxUJZ%nO4N*cfImEP%LnC&dHV~{$(de^t`qYPX=4UEK^@zWzcEXMVHmVKPX(O zI$GN5ce*`gw|&x;TJav+t+Dn(osCT_$(MdlP4544frz?^7^Q9v?SHUS_o?!&xSQca zJ-9`cg33|LNvdyMNl;m?^}b>H%|+L?GAgr5g)3xJ1Qx;%TQ$6!!*^0K8veLmiPvUT zv0V3NvooKr&0FIT)}(YkC7?19Svhpwmue1ozTN#HW_uR0JsW6OuZ*rMNvw_2B_#*q zHFXcn&vwlPK$yU%pLq66o>@ke#jGnTDJlu|;77Y|BDCS7a0S)G11*wRx%U?#a7AWUadINop_nWHXSqUF^-< zTD?*`eolFoN(K-gZq|;evAdphOa&e5CZFI^mDdi;DBu9j{ksz^t#kCK=r-43Ln^1C z>%Pbi8cAMFFVULK`0E>}2iK--5I5QG?LI6BC+R36E`@LsB-CxZzM(I3 z_IqPIWVSer?I6o1F@va4?c)9=G85E1m)jKZ6xwB5)$w$@{RavU)nAaWJF~0CQo#gR8JF18%p8$$hwy zcvUF!a^Fh3Dcx@LRVSAVax0zJR*Vb+Nod2L(eA;7&oJW>8(q<6zRGUeXG7`?fldJr@Lu5-qQ7jS=NLr6 z3$0LemhDt5{(qEE?~zk=i8y6RM5da9?&CE#ck;<^YCXDbC^~T>%t+^kLnF>ru_D6HG3Ctl=LttB&71d z9c%rrYI~eNNTN-0*?7j|JsIvog9XnNz`7^}4ahK`TCTgdxtH{K#j=Au-k7UfboGOu z`HI5ll%9NALq7q)*Jz{T`I_<>+Uinm3YM;MXmuc-tBynU)F==AvfkV_M>ErC?^a`#Cncd)-3gID2Txt5oLk*y<;Z zwc#pgvPtBXWfd{IXQjz*W#X1p=%ztHY{ze}U-SnsbuW(9*Xz>V9wQJKJNd03ad8tn zFq>f0=IO+N6a_5~fe5z`9QtnGd8tGkciAl9_A0{;c)~e!i0R?@a{n7&8Wge%ovw3y z?>2`5=G+(`=jkg1$LEumw90HK=cl0tl!erJ@PRp6M}r;-*#_nv$wr+NBA+&^RhnXfcj4u>{(y>DKI)cJG9tKNjPGWbi+vBJ>GtQ zy~D#@v7t}TVYxdK6n7H?B?Gv9d0oExQGKRR zAy5DcZj=MDfO**w7+otKZmMSX^UxucW)M~FORxNooO4(QKRO`oJ$1U0_=A;jdO87z zP~6x4&@VC4QBc6|VL$GJKY88v6K&cI-8~ION%DGm0{wc3fvhX3XyjJIA68*w*)>Xv>g%)bPXC>I%7Is_BnVemOR(xcOa*?sdTz9v3g`5Nj1d7Wo%~}0eAI8ka+v6 ztsVD<+Yg*l3+(W07yBmph})DUzgSbn-e3G5H>&dwy1H7tk{>?SzcsJ95ynQDAtn>f zC{djce;HjG;g?>%u&)S*+TjZYMgg6>^d;f$ZLLy>aKdEI=08bW4g~}ojkow zx&aq)A&RGlu?2X?zy zd4K|FPN@9evM9{W3pZ87{w(R#Uf3OI1N-oif8xoZzsnDVRil$`%)_h_>^lWLoOghP z{U7(16We{PauIbM-|n>t#oU#;Fw!g5Rb(cnL}KrS+F?_7#ZXF3;~ZW)r=eH5z|>i7q_DXJnc^v5wRH%-sT8krP4G+{TEP zCw>^K`7?(gG%6>ZSYcM@fMKCG7m?o%k%-%=6vnH1rgzMt8Qp$Ej0_`CYqOHv_vLIz zUJja8SC5|KCFTnkTW{TL_a5|ZNZl!aoH^R6_i&)5_7L=MD<~inq%Dp05fkT`+~{Bl z1s4^FKvH+5%*2tCzkcp-EV4*<1-5XpHIhOqf&rw+CbO0%Xw8^ukmqT=y21FmbX>l& z&&4t(<~^H@Qr{uj#i9(i^rUitVcfdu!u1D6`jRTTlB!axkE(B34R1XZ55{0-4n6yw zswpp~EGDgvX~DUJ!h`%gP-{;fTcxe~W89SqWm0-~@p(7E>Ru&z$uR~PdmUSjm075h z&zB9_5;6p^aI4bjlb%LKs!U82vnIUb-1h-4wro)+QS!CdD~}7+cV~}gZ>ojpR-yYy`{?(I~FElClx645ggr=vv%|9$GrT=q8E`bIw$YCW;gN5AxB9Uhy z0yR8}o#FzrVJLu(?j$eTb`()B9`6hPs%dED4?bWDSv%bCF*=#Jm`TCwVU41z3P#Wn zhN8-Hzhn48WiNBKsv(m*hqK?E&ZC3)u;UZK)m8*WcTflq5!%V=Nk-MUlCR4Av3iQ; zcZx<4*^EVL`ncsQQL%%k6QiP-c}aOv_YuTL(0 zi=pv9RFaI|ob>r=J#ba5IFyeKuqL^wZ0bBmzW;mq{i(yLriy`PP;} zFlyno9(nF2C;U^U!Y-pbH8XS3nZ*PeN{3N&ux`iAbuN8mB&PN%VQG(BPFaXUUCK@M|T<#3ZYfs-}9r0{T8LqCsk zmL~~iwmU%B-rIY2%`G?>wjgj6I=>@X1|;K)6Vs>QlY`p_3t)W2oK@A-=ThmSkGpPd z{gagX^f{3zM%osG6D&hJKhGJnnDh~+%#6dIEpMUe*&ucZGjQzUAC^3fjx6eDnxdMk z$9WZX+kXUg`4FIJVta-w_1QLW>G8RGGinob&vVAKG@UuY+wm%mXBF*RcUoh8jdzo*Zw@?#>gB2&qjM(Fp1JGU}#?Y)Sr>HT80k&r;QyXX2bH_*creY=Y3P-DNU zK@pDnMuCL>6lPfmNNCRQ(M?uwf^QpX!RL492$u^;QygbQ0ryfJV@$)ojgU16DAPR(kQCGj;?M}w1Kv|mdV6Rw^_q>U^;N!73yivglLqu9u-`xL+3O77h&Pu z^AKcy0W?8}m9lRR)tUHs+6(_^?Bi3$ZyKuaKDFY^4s$-(pFD%Iv+35V2N3z4phuI~FVS=%<3L(zvWUN6T#gwk{5CuDn+4DXDl%wV5 zgO|*!wjhBENN6awroWe$Z37I=pYOfPNyHT47g;4%mycI}5~0Au^bd3q^Q%1USR{0G zcB-bLUJmNnm|i?o^A-UZ~sYrkbxL z>xSv~j~4END(VbC+HtMN#VwSoV)?IUUr?m^?E@d4rx0Vb-@Q;6a+O}nm*fGwmbfA5 z&W-o`)5HgyUQ<(o48B8<0`IC$SfG*wOtY@@o>DSsokFUpI=3TboQ(&&YN=E(rR-bOv-Cn0`aaFn1vV=s#(wNQN z)&5BN`wUY4TrH83=9&k^b)|@dg{S9Lf?_>mlLn>+ydocd<5*iCW|J_!g&D;{WFLdl zUh=|@dD2~lKrfni0wnq15(|UcgnE25j2j&{q0FHBxO7~>i3PR4xxMvvL8#X98HSV+e*bp8aQS_dy06ST9vhB6nQl!74lM+V zxp|;Zcf%^hTGTw)g-l&R%X&kH;&dvk*$?i^O=bGz;(6y81JjpjB^P5gCFFv=RE5ta z8_|u?MYB9|qWZ*E|1P6!QELT3#H1Mh{PD5J<@vZglXLmZ~(`Yhk zslV`%QkXFaTg5fd0)g@A!gRCk#?`7p4VcsRbviRK2gK&Z^jDFyb<5v+cDlTl7S_7l zt1la9%P({%CjB965K?w4^F8Y&7ae1ju=)2}S0F+^Dcc6_GeQ5;9^Lm9xRP@hn~zi% zHQCNhEt+)up{b$^h2Q5~Pe;S(w@T7jUhSv%-@FOlh>qs7N$rvAgv zd5WP77OoU+DiK3sEE?)HB9q|=nsAlWD))a0(qo!_F!emXKiBnsb?TN-H}UZq1xv^J zHSSrb-8_h0eEj$kpetE#9w_YYBFHQ{yJ6=a{s^nfqmU)A{C;Nsewo3ubm`+4ev+;;gGX7#7tUhk>a_hwqJXAa_9u1YtloYzV5Is0|h2is)H7_(a$YOZF= zS@%sZlYpX>pgza%b7EY}vESMf8(cd%NiI-PHW?JV8m3JhQ_IiY%;DllyBLBftoQIw z<_=o5wHSGihZiD){S}zJ{FpxHEA;dN9XViSn|X&hmv_6zxVtq>!G4D+mqX;t5!wQ$ z{(ecyt`F3#C#PdaOF}cf->YaZvRTW2$XmnedVT&yxQjfU(2WRSkOa`0_$m`#704p# zJ5kqmqVh4XcG^+#m!eKHIg0fn`GWjHB_*Ey9j=OnQOW5f6Eq&?UE%iD0yw`m-cFdY zUvB-$X@UxRjJt};;_qHW@UJH9#KFE0LF~TmpD8h7ZFCBzj$H!5vcI4sG4Z|SIP!YK(IjND>`fV3kMeU2na&vx)KB`lq)Ws?G zxg;J}bA;O?vy0yNqh?)QZ8gHi_cynR&F<*pMlG<1-3jc3SGFQS{QYtH{OM_kN>J#A z=0${``BPH*#o8sc#qBHcxhmz=x!-kK)^;u!L~o&4KMg=iGEY|;EG(tsk$M;a!_`eA zNMG$br0xe9L{8<8z4Rz3xJAn1lWk0@ph7Ir)Ah!L>}-OXx)|65-cw^OJkHsxRV~Gh zyAZ2g7Ues!WW#sy@QdjYEfQ8^yOleH0{ygU)}L)d}O4)w?m)6yM*Cp6aqDUff6__e8gOR z)P`a7)W+tNmngP{Cy17*ERRf*%++)~g46b(>E#RSzq1Bw3X0DcP}i4;5|>4g$Nu$$ zD6*E+OxQCsTTu};_4RihT{|;Pj;Ld475%Z{$&!@RMaLEcwD7(IN88gQqp06hNj7$h zUY}LB&Mtrw)0_3MG7di;UjG+%Kp-F|B8wk-TK`YT*;3EVT~NC+G03avW5h~`74gQ= z7ZII!Klz>9LNEi5s zt;3iS)I|bNb}P%iCaD@JSC`D=VK3aQYHLK3NqlwR)M3O8888MYBrrxR^Dn#ZEG{)V zbL>f>gC1MS4&O3+w;h+hp=I`MJMtJP^~nW&Lu;?f0V$VTv3}Aa+KjaLM1)H-cQRhb zYrs|0YEV^`@EE4L`QZQ(ry#)jqMOdt^m_&$UwEG;`A-zo+r-TP^V((0;z16**VE=m zS9o#7(90hf+^L_g{0mDCfxw)c=f}iS9h8NZ>ftal zIjJK2^g5K(aNFkXEf`~O$5|7smz?$j(Kg5Ja{2irFg+QZF2@{UFuH?7syK1tV?z`e z0kEC`uyRNk9wJs?WRb!yVLl&I{77PC$+S{T#(#5EconYJf)zY_&&xUN>~OwxqwITf z_%cHf%^~X%Uq4h9dSCWE$6mc!L{+q`p@E%SICsF*!gr#0`Ur(jP-xpwQd86P+Q*Pd zO&G@QPov@)%dT~G*b5)@)!|gOf`SOsiyW&vh)+M0GK2-}_+P6o*V~%32k*AN!-xAX42xE%9&N(G~HzE0RuTk z0NLZx5!lW06n413VK?t;c8s{RS4QRs6eKdF@8iTZBwBKV2*fwE zE_R`sv+<1f79va2;_lb>_+`6W&6eULkGncO7iQfxA>D(kfc^43`TTGu;@(Gk^v*RC zBc?%@9VJNQg?9^*^G5g?k&!eZ1KJNO%@e3HY^zLOACd{!*(4Pc5Qc5E`!dg)W?57K z5gixbo}$3+uGG2@5GKG7&c3iRWjAm=STW+nX}z?6^ZQmGo;x>S7(3iefq^J7IrFNZ zU`pv6@G-D9G&@=0X$ntB$I?t&OUprL|v@yLrq#rA~ZNEVhBnCrMWWf^<$Cw{KXGW;SeEP zDXBtp^TX(lxG*LXJzk zxzqd#4+*X0aUhnCf@9AO$BhOofl~t&=xo*Y<8NDwHvo)QmX0=cRUe&aXaty4{SJ*v z{1LP;7pORa>-=N)p~C{2vOB z)%=UaH;*-cT`@)f9ch&GEuT(YfQS24yFY{U&EThIhWo@~EMAMf_Ao-njoXDa9$96q zJU?GF4LwQ@*P-*~-6Zl1JB2irk7qbGFdW0@Z==%xV(8RxjW`*DZ~x~l1kqO^*xMxh z3!RUGeGZ)tHrN#I^)di5zR%lQu>I?jZk@i(<%Fyq=D%;H;?vmdKm$FU_+P7JqFQy2 zj`n{sP)juE3yx*bFh)jtTX%V8Cs)MRtQdh@upNv7df|RY@wtR_*c^(f=VO2jT>7K0 z+Fp{7Kx*F}KR;kTOF(PMSmd96`iUN?3-kPk>Xaa5FE8EEj;ja<>>LsQx@Wr~vaFiO@i3{cWi?6^k|*%q&rW0eE(URl~nw_zX1a&EeTqsMi>~ePDyATRu`o@^YkdwvU-Jjji-5C zXMFq!`RIMAa+Hhm?2G9SXUV32x$gWqbmsqvrT|TZh7kB4KM`$RdE!Rlh5S_2*hAet zFUSkDyL}8^g!C+su~&MUmb4nvnnx}YKW2@00#{dvg2MUil~zBCm@23?TCFzsVOjAvXPC= z#N!WFBPN=UqR1h}<2aG$~ej$K5zh{;9* zbRJ_X3{=GFb74}}l1^-wy(}zr+qASC@KGxqiALv${SNR=8;}+r-7ZNAko7ZkmNQ^1nl@UPUoh^sz$rwmxPA;QSfnQ` ztfnXc?a$Xig&=In$jF#Nx|Y!ln8wgAx@WJmaR3j~{$qTvq%hvoc!giN)nm z6WJgk?9$ENd{bWWgaju&z_2qnJXh&%zI|BiH!R3k*|NU*^2 zdO$E7g_0e{LI}DO>Y;+N9(fmzfY`2PhP-dm_G zrD9j9{j=#CbR%6}tQxEuv(bg9x2Ac5q8$6V02Dg9Qpheu$bGop&}m$rf24cxQ9*Wm zQMpR$xSE@|TJV`UTR;kcot2%PiIszil}Ce>myeyDkCUB&m6eZ`wWD7&?EiAGb1=8I Y^!k50{7rx2gE#=Pl1dU)V#dM$2V-UG_W%F@ literal 18776 zcmZU)Wmud|(l(4UxD(t%a1HM6!QCB#ySuwvfZ*=IeX!te0fGnj!Tp`=v-j?P$H$Lh zrmya5tFEi+th1w(zDS`U5+FiAK%mG-i>p9DKtY4Q`vTy=pEoRxUm+k6tF6Vvlw`!j z$dsHNEUazKAt0oq(lX%HR9A4rr@N2h($SAXH++!Dy5Z0hQ8`61$x_iVgAv^^q#PL{ zBLms;i^u>P!asu}O$f2E>(NHY^5a8b3F$7N61cB7yf13*>zZA9n;WMEpL2Ysbe^Gv zdxmil=Z$zE=3uo8S%efNghjaO-gX18PDI`#99l6 z*Bkd6f~Z~@ErUOQ%FddH&q3BFgWy#FXLW-wY zg2T46_w7^_NhEV#UJTY#Ie#J#d8YQIV5b|nIruMqVlx()lS5@}zF-?hxWS0onACw4YJM=wDCKTRv4nw#$i}^$zCJPi~A;!9EB>c#;vJqtor^{Q-Vo>b z4LKaKdmt4WzMqeCzyOKcksK#I3~!tuj@KcT`0v-tu5lpfFxOT`lOlgu`W+sTB9lRB z3qy|yL-UA*1Ch0$eYTK)2cZEV$jP7vgG&OTlast9jCizQmqL7%0Pcb7`N(R)(D`sg zu%Cq4xsjNH>9^q8P`vxZSRlgtkXTSRLSz8Jj_9z3qGO5F#qe3eOXyh6VZQlfG|16m zI|WqI5Hk7dGm_=#birf!bmh3bsJTH*qRaXAhk~C0aUu@+(=3S81D~~smm(OAs81o` z`!Oytxe=y9UAFi=3H1;)2W}m)d@*_;@B5)IkvySbm8h_ZOTyU1Sd|UR(bb6PFg}Xb zh~VVQDlL}7snJ(rxxsS;dPhBl{w%Dpf?GvCi@lSQD&#qozahBMaK-O{TMs=K-V{MA z9G=}|!Hy;P39}n&Y;3|Jlew4aE03^`zW;fjt@HzXtXIO2$&nUxHS`iGVT?lGzDcXe zy)j{f-7ou7ba$wT0oq-8N2WG(BEpQY@!_+f#a*T?Z^wbQ1W!x@EQh%Jq2X=V2b2fQ z7mOD#Uo?LhA(=$VLyQ~%ISiBWM`ONivVt_n7#8_Vsxd5-NTxx638IrgL+UT#E_q*Z zUpb1TCYku+Fe*W7;)+z)Sl6`A(ofI5$1$uiDg4UVc4WD5`bLdXy;7M{sr@tt5e>y9G4~4Fc-yE`nHAk1%zFUmCuaj^ z+jb7;J!i{5PkYpVDnJ?_a?lY-cQ0YYFojedNP9^CK;wu5!bYXhQ^6}NEaz2Yri9MqN8PK;xe;WF(-hq>CYrWK_pHuT z)umQa!CU35hNPxgE~pf;7`xcN;Jk=hzOI(7w5)Wm`l0edy|?&HC8Tz{HmOj#+R4CF zKBe-ga&(ztsVo06r(opLsF+n2pE%Zuk%KXSF-jv%BV(z!CCI(_4(?3yY?xP^xb#cm zmxeE$Q*E`S=TPhF9c~?HHvn(>ZnJIy?_6)v8&&m!hxUeKSzJ={cM#t!t%lD85K;iSB~2ASIQPVV#BXq5gmS28V>hj=q-^B6=>VSjQ{AG0-3E<=&;`^56De$-bRJvY zr=HawnI5;EU4M7~c7MA!ym#UE+_zT-H{1yIaRM|)fEMu#hBPWN8UvCqff*4M;#YkL zW`I_`O<$2ww~>gW3jkmoc8cgl^cDRZ{?oYVY5z>v9#USIc32JK336FDGm;SIn_xe? ziO=AG^nkRCnNO+sdN$&{H7KOrh1UI_C&jJUtnLXoN-lMeGIk3o(=&IdgY zdsdIwgMRv*II0dR+>i0p?Nn#71aj_jOfvqX_d6L^hGh?BYNfu?C^7;$ylJ?(OPTSC z35r6LO6bLiylkJ@G|XI)6ha^SgXGI5*0XjCg=fiGsSGIWM+?a(rxcu));K!( zpLap!d!IB%>d>p(+UGp?($gq;dU%8m3SD^G&#IaVIer~eq zt1UH=bP~DhTpxEgq;FuX_$~IEa)n)qKyCGhrpHBmx8Ydwxc9igI3fK4U5lFUui^FO z#!bHfu@Y}{Smv1+en_iX9>as9yOw>Q(qRgcRa)5&?<#@5Dp&q$BYYs@qJ zxzk15hGOUYlgM4jXv7JLF$oTTx{n@6{7mN7L9&+v^%q(W;SEXGquL9og6CS5`*Amkah5$qPo{4v{w}fcT@VYOrM{fs{SD9Da%Z1CT z4lOE!Oc~Gg5qyS z|M~mBahiKt|FmwWqnQmbkT@xxEXx4?zxA z4*q}D|NlMtZ;$`eQv1IxS=m1SZ_EFA^6!@X%zr2FKNI@D)%sT{c)0`-`I-N-^n!?+ z`^VsjgTF^cTtv+i@=PDz7klVFK!z+-Nt8K>sT*G8+e>kj>ybh+P4Eq-+BfMWp?m-Z zAXqkqsaxhk!e6=$O12!+8>#r9cXQMsy}P@6ZG1hf=^nIldODGv#kIMf?RC9BSvy=J zmtm65q%V86+Dz&5*taXXLrMl>7{TB{N|HgMU%Hk|U0ymKuQYyI ztkKm}hfy+Uv0WJ%ACH+Ukt@T!I609cCnrDVfCpFqr>EVqwW- zj}H_7C*!ZEC}>Dk^R3tW%}+#RwbXxUfc55wh=NsMh=_vgC{I(6w{QqYzP?DoE%e_fgOpIEg3wo5TpuR?M>+(g1{`Lef)U0)a}Np?4@?7pIrFAqs*X8X-z>`9HF#pkPATfNO7O8qOI_PWQV>OUKa10JXv4fnrS7YG20 z(bIqv6%{?a+8w6F68NvQL}YXpb-2sLz9_6uDqtlUDvL4Crlh2-P{`&~YyPVKbtWIu z?QkY2o`{DcnOUz*cqryWD|a+Dt?2XpMaIhG|1LfZc=5?tSQ7jD`^%m8#;`FkjLF^0 zzT_T0T!<+g$#e!XKh5E7b(j0_k}EC)0B zjiWL80PxSL2*i*k0<;w)hekxGPJb7u0M|C*3hI&ZIRA~o2hhTwp&VHLXUM`kB0$$H z2vXMQ_;_6Ser09lKSxJ00MoLd-d>^GlV!!hB5g;S)F$uSua#;Q$y-TIzW-4;yr99b zzzTDttDT`8Kgbwd#zL@th-R7cdbm&TIA_UHL!a|;1Y%;=9&xwM?B}!klVA8kKGHSgKN>wM*cR%iDn{2%wSJfS^ zG+N&L8O3@6jWb&V10kD?2f{ra+(l885Y+2BAr+X;q{|`c3Xa|GT@v+Hx4-D=-Qfce z5DG>{q(Rr$?5QWSSWVU_~fr`-gh!GoB! z7CX7y7mzl1RXJz&8<*7uySqRHmIBuEv2!2aD+tlV1U@s0wL-^uYy3E(W8+IrC^MqCa|S4itoENBD)^mHs&$%W`K4Iuo}ZqggRa2` zUt>tG%QFdV3#dJTF_sSC{WifDokm6x;^x-!)y6Wn7)y;RRm`jXK~C(}WHl?Ad82GF zmBVuc#{G(BW|Y#9QRT$AM`$9~>X^WT3?=?qJMR_I+_xoMBNOE?~p_g&YX0u1Y zZnI~-kb#zu!u*#8-^84GpAxR%(;?+7YSSKg4@-B46UNP)B(($HU%607__ex8l?cF= zTXuVU8@DT7Z_6vaQ3pSL`RPTo&Y%QM@Ilz`oL;TmC`>L-&@c4&Q|LOY$FzCCqY~AR982>hZa>|gm>{6}1-`t#-K{y`n#-(U&#UoLv{1r>+S9N0%j7P`pXNRQ%Vyy9-g$ZvGI-+F2?;_Wx&t}GahqWeu~rb5ue~U6c<+!SNpu~56ZzM z=@DO~u5C`6{QQ=C!8tcubuaD}04r4JE_9Y(b6{WoNK|uga%oCFoZiR<0Bv(Wc(8DM zYsp&5?W#=oxVNTJ&#DjaS#^zNTK8f&hP{|VYAx@(@2&DZN7ZY4jof&$s415ki{K3+ zp1WBvTBTm~IWlAgMubYtO+PcwB&xqJHYSyUfI)v&qRCM));rv=as^35Gk-a)mn&0t zIBo~)j0wHJh+XtN*Lu1e1;bxNVo(ll6|fya;b~n~7sw-zh=_>b5?yrPf0yp{xcGh; z*w7Pjyg*xkE-g6%p)L4wDW;5iOw8k4oTv=?#aE}>8V}Yas}Tx5oB?r#VgW&9e&ZhqA}SKZ7JNXGStMvwdFvpuiM*%Fr>)y!n-wYcjY|7Nt@*EVgHZ?f@MO@-ql-?j ze>b-nE3eZ|=mUxfYw8~>KHz=c`-_zPmy6%+l>P^D8BEPO9VtJGeDPZrQL~uLS$R#N zVr5u=%G?NXJND`}fBm>xG`TA+RJ`Xw73=MBw)!#Em<9$Aa6QR|t6e}-l;C^06$FGu zJb8V-uaHV0!Sy8>8^DMDM1#CAqxW6VkB;QGT7`)w`X&0~!vmlS0voo*O;{JxUJ~ro zA59CrV~;~+rWu6?!DB)gyGKloZf@qexAZ4w zK52jJ?xR@`eHgV5w&`X#9~SG^8V!{RxcR zB+kv3$Lk@NAa($Ijcgj-?58~6LUXJ}8RUg0kn%a$Lf1T)TNFF2{E*NpGb5Vfa@Z(V zDUqEml4^)nIhe`~6OEZtk!!S^#uXy)>((KeFxvD!VGK6WZ?aOhO9o^cQ?mcs5$pP` z6FIfMVZ?9$n|mySIS;SctexA`F*FTYwxc)#jTEsf;9(n{6+w8I&1Q*VEQhDjOnKVk zwlbC)Qj3lS&&%6;bRtJD4LH2o9S?i{L57Z8zMm^Q4U}mGyJW0kS$g4 zMFfYV8xOoYPBZ_O%bGp(%jAxTdlmJDaBnQF2pm^ssWZ+^Ue4p1Bz({^PF%hxJe*#t z)vwaQRSu_oO>8k}WEl%BLHV<{R}yXv8CYnZz>;qIdl}?KLr^(H7{M|wWelMq_b|Jn z3YQ;?UZsr*F!oV(pQjvT977wT_|=<@qh;QsX+s`*e|Go7b}DsR z2DZdRrBl-CcuK#eE7q0PYM{jKY57tiFgddB_WUt^jM6_W+BM@H%9G-?!lI&dN7`aDVD#>lh zrBKJIKhk{gr}eCllYTRb6vYksfOJfunw4Z$`sYoL){)a$j!3vG?^(mmHG;s-6ZfsXJ&ka#Mq-ItoYt zO%6A*P@zirgLf6xC;<}hegq?0j_>r!BkYkCoOaasKm+0iDQm2Q*8JW7VthSRB197l#B7O zP)Mx>`9tH1=)MN_oVGO$kT4&Im_#5nrr*30i~)gmH$=ba4RuQet0&7)OeyM`F9&w+ zPU?E+j^@iGNEyb1pbGY4a^J?)_K;l&;T*cz@{Jo1H#*#6s1?66Sm3ZV$Y-&MLS*L5 zjQ0Qeny_@|o$Lu6Kc%+nV-!h)ADvI2nBq zj!YduT5z;TDBBG}Qb^bjzkFF*uo`le;sMX-^@E&I3pV5*x28sq)ai8oNGU!RVS*$K z)cW}RYvFH<62Ni>%iS5pd>7GxKuCl)!oR_t+rR`9yqnY-c^Zf1o)ahOF$V!K|F;p@ zOfts#>dgZ{Y!nD#Esh6s17kz93axEN3-!cbt7lpmxd%ZLQLnT&ni2s81tq@D(m1}^ zRCETsrnqjS(A2x`PqtrhIDF>`H?Mx0qJ#=$Jz{m5arMAeG>(|Mcqhs$gwMe2DAloKi!LP(UE ziym)os+mjMaz={yiO|i;eaobRs_@cUaKeHWhHrR8HOtFhuqCV)HG0@Z#RfROF1Qz7qu+M?8(y_ z-Szn#)^p+ve!o;+B4EbTY4k@=sE_Ago}L&81~RLf(6IXspV*mYFa_{{0MRs z>3GKda6GH1G&Wj0sj{IXFNkji2K=4gVG!w%e!uC_hbs{$IvRZUXkNh~OeI?+%f$JW zOuNegu3SJl^fY8O-ep-Pt0~->M!I&rJfw3I@x!ZVyYC{RNH{V+@-vEGFEv35#QWAK zFiL<^^^sKT^X;FgW==2QHEC{M59N|&^0Jj9IA#t@fON-_4sM5=LS%srGCJ!-dAaGjtJT$r96~&k&}}|T`>{6uPB(|kpk<_vLX`21%c1tC>FZ=9nw-*=Orpq% z_{S5r$`2MeA>G(?-LlQedJ3I|Y8oGG&9FEx@u!j?43J%&s zxhdJImT3~Si7aSg5wX!pX7K{^v8BO_wiSZ)t>{m!`<5TpukFH5BT(-&nj=XEz$H+0 z^@r)kBwsdtpYSjwIf;75?Lb3>o!F6TgCc$lCr{Mq56oXK*ZM$+sZcWUEzrJ>6RxSh z7f~4yj=Jy3q0K5PxEDWtHpYiQjQQ^WawX-5t<8u9+{JUyObOK%{LDoJ7luT6P;W+@I6L3sd!|yIZ#Mb-9-ytK>A0N`#N)oLP`{eq{L4-^$ z7R8)VC9|5UDU?AD(V+b*6U$+ zeaheg^^1+}uvV6qm%{lFeBAHPj%0)RNWl~dXZD#T<0a^s*xM**CBj0T997HGxJ7MD z`W=z_gunLTVqoB)P65IP2(WU=MQ0GCL~^VnMRg+YA)|mXv9%lUMgc(x9}(G=SB?fm z2&RIkPBCZ3t=;2Bang-ggV-s$07#wAfsEf(e=BNP&3+nqqVOXyLK$dbx4lnI5#~djtcLpzq2-syHW#FbauEDtC-YO21^nH6g=nqAlMCji#XVfBX zk_bSx5m~oM&8Ogb38f^=0imP%mNC>EUj0aU=-p3)F0b;bD*RW_^yxIq_N6d^9sssiHICf?7R66zK`c>y>Jbc}DsqwGhR!lbDVN z=tQVLLmG!V^fZF})#g-mXjJSQhKN%LhJFzg^)3THAVOQzOWNeJVNucBfKVA3rX@5tT{wT22~RZ zYS<-4GK>)UAi08~#qIHh43)*=&XCbVxK_2Jgy(gm^ge~ zP+#Q4D!EhIuj4xNEHJ=^+h}zYllf;0xD}hlF_-i4v;scs(IMX@g6&hDfS(@_wwKbD za$t@DPU@5?kPQO=V}aq%cmVQL@(k{OyB%q-{Agrl=t9BDRB1<+r^E zrKCzPRHA0sXlZ%=)-1LY%`P3lxE6MR!b}vx0c!^gY9ark^Yf#FXwEir^fQ_b&ML$^ z5jUkxYlbM(te|bsttz) z_oZM&8f^(ieOf1iiq2Y!j}NQZ;+sW2!$1QnB1^TId@Qg^6o}Obk1kK_x%-U|2Qsxv z69#=a^#vW+B1Duqx@+fKi*8ZIVm+?SX^~vd)Hj|Pg&{o!01n1(CNW+IINS5JG8$vl zgYc!boZ9Y+qal_^)+MywL-0u)CZUY8>Fy{8`Xc|;#7GJji!u=%j7KJ-m%HS;V+2Bz zqm~v21-f^yNSnMq6=R?cfAoWC(hZH%*_}cNQGO&kAoz3YL^Y8}?NF2ABlAbHx?zVlP)~d+@p)`{sb!iZ-~_twL7R zd0On&>bf?2qCm!#m1CXT`onY8$O~BLGm%TxPA^!UoZqHq|BXl6i<2qSL4W+ZP(n!< zP~@g6+1XI>Q{whwQ~eS9%y)OtjD*kjm-y3B8G`HU6M2W*N$=H$&H}sXPpv&MZuZ@7 zrrLjJhJa3g^A7xCqN68Hk&^`7B!VCJ4 zrd4m01`1<*)_@tU5?ZcQSAPtD=5RWkx7F{B4w~0kKacJ8V$Y;g^Lz}GwH%8-c`esz z4leYpM_9qH=0W=x#(V_^!`Tv#&nd@voiK1Jf5rVs$f_FK#=w{GT8%9ZR`*frfeX6P ziI`2j89RTWD4%@wztEg=~Tss9>#}C4ZANX)RU$4EaTH#23?*KUd#dcItJ?<7ht5Z zlVPlXs6cEub$ZeLgKv4KL=1`R!=)3wpdFzZo~7kT)-whM#*w^w&cE?;vhV0DZe$bq z+`0Woy^_=P8B}v_I|;mtWtJ$FG<8g%{0X6>Yq`bGPcdq2(*oOvUi8Ycq`=o5je4 zs4DS&^R!l*$P~ zSTNd0Uf62CE=3x^ADYgPB?*q9)2fe?Ay&!Pim7=q9PeKpMPa7;0RWhu$DeP>hPTIi z6*|q%vAAGOI7DY5&T^Q1i#?A&l~v|p$D-X-&%iF4n9Ad*#pP?GzfwY+%X!mfz%TCc z&Q>u*DNWRY3?@blTAn}n;{y6IVSjxpLV{g0QEN8~3^E;>@ahX54Te29m^P%zYbCa! zkFoA5Gl@D}s3>6ztYg{ZFa^f?U2dIMQb4@vwL2?SX`nD-Lk=?Qa^@0nR+rGRuQ;l21osyjp?&m=&d{Nqr-qH2z)YZXdz_QmWIj$}-Xf%CPj*G7zzz^4mRg@tx0@k-c)$=B8M``rCbM3bZOCWX;< z7tM`8J(Ca%mvBd4WEQWwKqn-dzo6q4;jhJ6Z!F06Iv zkXkVIzdehQ#}sL8TB>*Maq)3#X!;tYO6C1;F3zNGmWQ%$C>G|jIGIdp`CbF5?GOq_ z%C*uUmY^tOMD)hY3?#|gDK4F{oeRTAwlPvW52z3;bfZW-JckQI>vtZH_6wPhj%%%N z@)eOlJ-#Uvh)=qgc>2G)9K+`D;ZK}xM_jZ;rA%nt@KIC)ST^8o% z9sO#^;G?TQfq-uNUaz1cheEKR2C|=(jJh04OJ~!lGf=*g`DHuQYP;esvF$lPCrC~? z^}SnKA$v(d8l&wTMtp0d8{OP%i`IPfTU<0Qt!TURfeLmoUcUo{!}sOG$!HuJ&8bt@ zy(fVVOtT82?5Nib9}Wa~8U-DPr`;!{C+GFe8;X~bW(6vc5I9*{FAVfmM!f(i`ImF^ z=Nr+l^0}jJtwa8@MnB4nBe}7WAc@qZ*$?Q1-6BQL5_95Jd-&no8{8lBr{FTU9X6pm z;F9Z7-kd4Dn@vyV`LL*^ADR@pjeVhbG-Bb0xmcyj$G~V@MjDIPUz+a&Xh`KUDH+gY zOXKj!cnU?5DA-fseSP<#&_xFLhik1dKYVAi+03MwbD+uR!%_Ia>=06hL2#`3mlIY)DAC&Q*2V98o579;-~?dMSwja%pshrv&9Swy!7o>0Iu%`5@{Z z?J?kbR&dA#B0c2sTK)D1^AlCMG&GQr%~qS!e1&3OQh#2)R>N{yNhI^(0Gg2c<0Xi! zOTlqxkhDUx4uhgcG;EGyYViY7MVezEh9fkTVjk^O@E9<`Jg7>u4k<=B%A`Rqw(Luu zsxKT9Ld2?)Iqm5_m06fMA_PTXo>TQG{;At#FO^v)>NF^ksW?hCTASB56`Sr4{ zdVfzbc->f{ncrQQU)Cnkl>DaIL(_<)XrG&%dAegnesX^Nh9NBjC?6B{{j9@)#jSi9 zW2s1^+av0Fu`2ZCkGlX8+zk%BMTY@;hEW(W2wEylABLx9hlgU1Y^!SGPo4l8mOqr& z%WH*Ml!@!{jrPzib2MElvz%kRfb%I#810yF5C4in(8^3>)0oTEjyeXD&SxQxEI$M7 z*_+}Y?S58P-TZ$}UY*BlzXd^q{a!NkNKJE~cI@=ox+Knqouswz{OnW3RImKV$`g;_ z3z<^Buv^0!D2DlIND)@=YqBtzi-lna@r%|~+US=O*`IV!2TXb|c@ku?mFhLcwp_lV zpT6Xl2E#fJRVdgjpX0v#;y}Nn$T`NImJf2fR-uDuKz6E(%)$>c3l}a_gR_5g3wLDs z$P5!4j7n7p=VX&3N>&CEE$H+hoo^=O3hf1!^oC&D2;+rCgw1Xj4Igc%Xi4NtlLyeL zQ}n93kBC%F^ofQ!D`kREW3?oNuh0NU zB_GD%JNnbk#y%;2C#Qj0tV+`$vYF>ypV^3}01ko)6!GL>o{=dx>j$ueHjJQ&tT|=j z_Ln~ytc}rn$6`%Gr(oqp{M=G>n5Zj6YnSS*naSGdoctK`C!i7q3m95q} z<$X8zirNMv4t@c;I%)|$m_1M57z~xCeu|)JE9;6(YI2GvEh9Gk^|3Pu&xZVCg>=Ow}qes+f zY!q0o@BiVEWc`f^*)I56zx`9B1dgVJ!-D_r_`ldu!ef6KT&Z50?Th~u1x5!tlBw0@ z0L1wwm}c^Utno_55`VJ9QT{hF1a<>p;D?n;<+A{Muy$v-saMX>K^1K1 z{#>E8lRTpDZ|>imIT>Xnq?VLR-W-bBvE2{wy*$e(NZ(`CthRJhOLR_8#Kar~3RDF& zlm}lAf_oP{6lmtNy%xKO{)ZAZ7!-KK*0%zT!zRX+$f7$aIgF%1su-WJlH`cLDQQK$ zDgMnUH@}C_xp)&}>aLXDil}rO(mm4a=f%rzBrrs?$!rN`%>0cd(JwEhi3|rriB>6l zR>$|KQDHF0T@DZlO2>p(Rv1G$$P}iK#|G@Q)mLA#79(RzT;{F=NNA$Ps3f{0^PfB4 zso$5(C7z1j4a#WD+qbS7bm@ftkBBB+3m6=PN#V!zA>0$Dp7!>#8#;N+>5jhu<)+E) z%UL~|y@D9_obOj$vw-8ng5v{1wX^f{tw(oH*J}Bi>L4{iQP9ql=@25in4s4SjpsTK z$cvFuLJ;9212GHhUyk74?HWaZr16)@m1l&uK=E~dLtWqWkwCulhis_B`3bz(-jkW# zR>r>BHKu#p@=CLbbLf=ysC%Pe@L=VzPF}AD6q>tn!?=vHGrb^Dp0DDEFrHB}X<(Cx>rNwIk&V z@6LQ?2BYQ|PGnLn&^@U}*_;>$o=E#)>6>SS33h#s4qwB4Fq+sMojNs$S=ZC z)&^gPuQdxq^?5zcDSl7`+N+WOoarP%`P<2rP;-^0tZS$&Tmxj!4k%xsx5N@#U0`K% zc^D;x&^}xt%*ocKf;B&x80zqF)(f2Si4G2aE3VP?&~0-1-F9&Z+M}lsNI&2u{{kjx zu2nc}7TjDf$6nwUJKNC+(fAn}=1@= zkZ(Lddl7o?O1wMM{dDe7B6)b+zA0i3HJV$knMU2V3pY*pcg`6(``+`xK^ z{Af~WYPCtYsd_~EEy*x!*~$T^Hl{`Wp}V0v#JMQyPW{^#b4!jgd7SH+DGELb{B_d~ z!t|jeu&O1xVgS=i+FXyPTAFNEzBRcX+0tqMD5rsn7O7C-Sm=;T_l?o0&NNNhD3s6y zQ!oOzhUI-HGN)7Vy*SFm9X|_M1jcU#Wl=HUDIp8j zxs$67)OmatdCG(n--Z4lAo9vSUJv`@aIvu^vsw7+cfYr+o=N+5*)k4F#|M$XZ+r?Q zh9vn;g8jAy8@BE*i!V!y*0Do+dErooJ=`Y^Voc21vP`V8AO~sWpl-W)I;?#h$^gc^ zK)n!K!(ac4{$~^o3`5FT3?i9Op-seRHbngqDaI>5o{UQTlmccdQ84fNx^uiwX1~+1 z_mTG(UhRZ|dT_(Ky1LYOo^Bo^qj9PvFM4!S=+qJO0|VLAsx;gp=GA|CA_Ak6g#uuk zZ|dtEksgySM?d8vgs@pHRm<$0)&^KSWR4yjzp~pztXxODs9*?ltJ4i_o(D`r)*5nT zF=74I^9^>#c~7@z;{C#v@jVuWS>WT+yP|(n@SR4ER`rywq^uV8Dl{CSkXNV!0*-HUnuaJ&-dVue z7e~|(#o+HMC7@P3{#($=I=i+^9j2KoUI`zaV!#3i z*vK}?Nn@CS9(S&sIFR)vqgflG7>U~d$NCMV2e=;1#n)#;uup-V2uwH<#%71jehT8Q z$du2nRzk-M6=+~uk*K&a3qHSRsywFv-!~z${LhTqKUOQd3MG&#IzQAJbd#qeH_68l zdKBw-q5|q%AFvp7TO_ae1N6;V=&?*OPnc3NRbyJPIoWNXbqYF>&Ir75}B?|FZr(egv^Dez(d4W4F9 zov^tD5?YeR^ZvtBh!)!W%XQCZtHfq=pvL1@5l$$JGp>~B*=I{R!HJzcNDOm4%fyxI zPnnprLd)q0Iko_1EN%oMOH-I+2&lTRS!4*peH3g^2*JQALu%l9yMmLE|i2A3A5sV5o zR6iSf$UQ9kiue|o)50`j6qq_txwC- z^D}*(VzaMiE5kq%J19GeVRNx#;;K&gZksNziRy1VP2 zP8A+64_9N^M8G3D zn9TmP@relu41Po2o~>ybP*=HtZ)&7^q`Xt2N)eV48xc*W;62)JbX9cqb6(LxMPbl; zjKi1*qWuiagWR4pK7i4`u**0CrhrETOu4Q z27+laSilLrsVNM`x@M>3*NGZ=?J#cQ*6r2PU@+CVg==FzsrnvmMN{q|@Fx z^WE-;-6P&1rM)m^uJrxH*UPdVaJ#69jf-ocd=Li?Xq+h?!T7EenCjWM6*Vpa&h``k zKsK_VMbq7rl9WW06MKEStxzfuEhGjbQ5qXT8>)}_6BseJZIV7nAD9@x5PFSl3bn$I zuNPn@5W>AkdW5Ar7(B-{-`)XdfkVyFF1M{_3t@=`eSbwOuEF8|T+wzeHb}h~c})We z;6!LuN~dKbSYRtF?|UYtAou=d#5PgK^JE9!+pIW z6|+r~P3M2qn+Gq})Qj}+{f<^cEN^zdUw`&n*6z4s33WD;mXnTA1c5**jL=F%DrND8 zmUJuWwfdbZ;MpCXt~9#d9;@#aQJnfhCfh^y(H!E9a0ncxC< z&8eS2Sa|*@YAsi57hVNt+*2JIb^Y7V?#|ZK8Z8u9tHeo=Q~&a1*zN4_9m93o919ZF z2`{WX_b0M;@Co=m>#cEp&H^Q%5u?k>Sah<|ODuuxh%xZ#Ou}uXi;^6A773;C&RqsFwO+f2paM56rkBaf}AY4_Xw7A^1~=H2Uf=wu@zPb;?EIcPgPSdt)WOC$CWiXxE+* zsKg64_`nH53j<38JMe9>tjt9|T{w`j3`8_`DpvPLSwpb(bs56MNo7Y?;|5RMG6@Zu zNB-SASVBau-X8yo!(roh$wzEEV#)2cg_Dt2j>-WVCZ=10z2)H*I>qVXzxQMkxiRWj z6(Fv!z6V-}%P+UnSA?BQ#Z&6orK~J78{sEYe#W&CX^( zW2Cyb-v0|f1;F|uFxbH4|MSm3$0ge<5w|F=X4qX0nwmW3?VQN?= zFL^roEe4pB@s0sFRKD}hJ9g_vqBKF9GQL8F%$YNbC5!l|63;=yh7HBqyR!pV&YU?3 zPMA2bBm;9lo-Hi3z;dx-#R?%h6f!vXWzCw^qA6Gw(Nel}>BL~JAL!wipe2}{G3e|0 zV4cv%Y4f=nPA>J@YKN=%*vgN-iir_m1l)&!C)WApf%Q_ntiYM|xbo%86W)4+wQ*M{ zO{&=0>4n?I+ZCIak6rKoaQ+^;{xJ5N0pXF+wB|$*)tR!vqU!HMa;E@+*^-8{`O`8e_GkKlV&J7wgpdCAQ#EaM%nBl1}2W(d>fkJ_u0&Uu~ z5lR@80!i=fm62Kku$dX!2=%yxHE*E4p`5xQl*OU%>dr8u;3+6NRxy%U`s7^i{%A42!gP4X56@OvM6x|AAA+yJ0tlvZrmuABlKljWOVT&zUsyA zaNW9f1m)F;oT(Svi{UfVv13Q8BDLjNCB{Pp`WGfffDv#X0-hMuF~DOj8BRcWfe;3G zN%-*>FJ7D$Em}laQa~7IIHjTEM+bp5TPOoq$Cc}~w(`kxZJj5zsv>6bslAN7$&2Rn zqyG+VPVfcrOY2Quo*tCJCpEQxqY&*5d^uS3Ub0^-CltxyM@`G+7wHAEW}uL;Nb0}r z<@*q%9A@=OzNCK6o;|ym?Vdh;nkrSQBosf)>YxmK@x>P|HxJHyn9b|04|p!*fl6dp zJ}EGxcGdrP<+)3C292N(JIbbOq^{mFrPJRmSLINcIfNk zYes+(Nc;$ReD~dVF;E0xaz*C~Z*IA*&`f-2=a^w)_NHIEwU^i4)AjEl$?pBURal~1=U^41&O6yEQezV@YX`daAGb-AifaLk6Dh?lL~JS#7w_&B diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/figures/Dogfood-IV-jumpInDocCLass.png b/examples/technical_report/Isabelle_DOF-Manual/document/figures/Dogfood-IV-jumpInDocCLass.png index 3fe072dc1a3ac390ee91b13e30e4dd74e0bca388..a99c97cf678f5a870bc1b8bde8c409b50bf273f7 100755 GIT binary patch literal 17025 zcmZs?1ymeCyDi!{!CitT1b24}7Tnz>xCD0#!7ahv-GjRXcXtgwxI4p}{O6o|-dgv5 zvwFIwdaat7uIj4&?Y%2pNkIw~={*tv0I1Sm#8m(Q>IPEwMTCaDulm4yLQb$2qVl2u z@H-ay#TX9qncVb?iaY>#Q2{`}4*+=@buxR}3gc~7M7^cPwZU6wY3@L9yj{n3+Mgk@Ph+0XD zi>i67oMu|+sS4u{D$0&-q<>UN!qG+=iu;hq1GbkW;lY&X?@$tV3|JkEMnu{+`-<&w z-sGwUJWId1sH)T^gcltG( zgHcvDmTlA3*^lfV{X0+s02T(Fg3J-W@sYwp_psL3p2{QyQ(-mp{O~Rrk8d{;hb}I6i4i=e&4cfd@B^6JayYsu}XF^%a_J2&l5=y6V zZz2sN3lzB_u#-GXD2|ho9Z60@I*+tB?Ox0&UAVZe5m}=^N5NMcapt?=x+tgDR}NiC zb`WE?<|RS4=(&uPz6fGLzq{A}fDs0kx8YV|tU362KD1oOr&lo+Pl`Olv3QZgFH7R#RF zFU%AlOY*%7y&*)%qOI`k>$v$5?-W2u2i7zZ$_(U`(x0R3ptX9xYBdse1up7PV1M@0EHasS!;DD*h2TVlq^O?04(`~T=QZxpGYDLqp zatFxX-w#N1SQWyg{q~sNcBeADgshA|gYlal7D(GKH}-z;PWLZ+{QX6@mcZ;e`gZ@< z2l6as#&O<$b5hblHP9G~7*fqh^DYki3TwMk>^FusY?bgKEOrrRo0b-}{mNdKk0iiN z@FrTC%OpntYi=G}xDQ5q0fVg!@-a#SP?Yqy7vGe$yt3oe zMTY5`xx{{`cMv?EhX@vGIo{p|aY+<&8Bk_6AAfxT4W()=fXk~g{n%VAmS$66C}_a+ z_g$8-Zad7^*+D%Rt8Z2$3TH1n5hCQRNN7L~tE!K#S^nr55^Vs=e&d{YZhC*cva>&n zZpr9a+XIP+i^!6>JiT0L`CvIVB>*V>I(}_OdoY7;MEQU`^^sYKzg~w z-@whEZ7)n90Gs((neB$P4l^LkZIBd3&cK{3M`)YQZvr2Z=;{kYII+v&X941+?#eu)g{Yng*_Z9?` zJQAQQI( z89g?Yj1$+Nm>HXD(VB(#xqxqqTyeHfCZ=$(oLa$3gGGWJjVar1m!`I&r}x%6v-&v? zQZNBqYV4(ghLLyY(Ve*;S-om*1e|#Z0f3YWWUKN*3*zTAMwPbHmmQr8`YDMQ@Db4X zdI@4gkK!WH)WdH0YI(m9p#5ku=tl#fqoYF(=8MZK=!>h1&vtfQ^v|P)#5n=O2w{jjzcYkLbozfqdHfYg_*iisRN7lbNdEOhYvT8LL zc?f8X)H?CZ1`?8JDZH2vWPU~fx{Y!oYib5vqH<|$o=TZ7IigCU4z*lKtG469PM##+ zlK=@J=<*tQKf35+6rM;u@-OCQXS}o0@;y?D>SD)Gx)4S={7FsW3e(@p<(_{o2lVbz zQ>lo=PoXYmKAgAu&d7(z%UOWP27`|+$MNQ;g^+!O8x++E{4L)e?70!311%BIuAG|7 z%N>uCX{+B->6*Q=a$bHou*SGnN+%rri9IIT*PdfB{MIjffeARVMUZh1=@`q96*kCi zjlQ!s-m-$7+q1N#DNF?aVT)&%n(Q8AuI^v#4uQd-)pC z2^m@~abXW;2nqlMo3WCxH&j?T zJ3GT9$^=gs?~wtpk8n9vRd^yfHg_ja7N3)Ms^75iiC+qQ%ZkdVkJd25vS1MCxE_;l z{m_DiH$R-nmFTxMm^F*97VBSdlU{Rky!y$4J&gZdWU`KU`oP5e3S?u()Xp`~0|HJ2h!DCmfyaqV8ySE$!p`7EJiM z`bc?9hQ55;=UGDhsI>dd;sA!qo%`nn0CX2ue9|RwznAz`)Jc#Pi5&VB>>ZN&R-{Ks zqW_D1aiW7r(1M&fHm4bbJ0x7N$QztG^})|PBo8_05P2C~@DT&Cu^YO}EEB4<@m5hk z0d1<}bJ={7_4Te?*3>))d8%fd7GE!-gX2ee$}NAN>Y-%y%l8X>X?ySad$%$Ye|*-L zF!Rc6M*4e5ce?xs00^x5kLl-0)IE=pWJt~DE->~aWosD%gF9IM9?E%|zB_4}`?K}q zyZ58oPi2%e_U?=>vtLqC6RDrA3KxQnqGGDr3lTZ@koPoXI5i|qmVFpC-{FBO!h`A$(jFLJ?3<{PsEF+9P?UbFfpIc&=v z7TE7WE?OjSqa|14UdE$WG{OOtF#v z5PsDvi&Hv?5h2IW&qcpWWHatGBxmh={X;ED*cYz5PlW8mCjbjQT?`7!^zO<{ zK3HfVZom818UdN1x@PJ!+qTc!4y7>o{D1CO=arR3$Upm61g4PFEOq&t|Mp(@P6uyf z`J>eHGC;ohCHQ5fg}aC>yCSzpQs=qG&RT!Jx3{WsfvQzUOs?`&gE$cpap@;;pVf3SXQ5p?DE)?= zKCD9Kqqlz=UJaTriMsb=qN8hV(yGdSdW*~rnWWYtkqe0<*ZrfF?a*bOb{gj2<}Qve zsIKQkPT+p%%pqip6~m_8g+C_;XxHBGUe<)-+s_X&8+&Tq!-j-z?5fG4_c$; zZX{#O=)4gI8!{SfwkD36?%Z`r?1U1bXV)A~@!81TRq~U0anfZ3G#3;UAUZh6zrSsK z^T%xuNJ#;*W|d#sE}a3CA{LG;=T--d)s-(#=5MlpR&%Wo*c$a1~5nP#FQe7m+mbOo*jR^ca=MEGh|GCir zc_Q3VzL;09>`ODoALGHEhF3caD&tW18=*t{2fq-)A+72rP`0wHLvOR)PHqPOar zWjoa@8}dAQ$f;aK)?E|D#-=+`;fqAekv@Ik;AmJbdGOMTN)TKo9vuUd?MeAr%Rs^& zuEPd&!ZP-%ZDO)bs|!ZsRmZd-JGMuSZT0Ss+ip6$h?E3cg1Kw!>V!|(gP>#`zFPbX z!_;ZU(ipie%E+MO)7TAfEZjo|(grW^hCAb`3SMxwuf^|kg|SRQJWr{NMuCT(T0N@E zx{JvigN(vXav_h&ylHEvGK$QO>VwFk>6bwhzP!EVx(H3AS$wTdLHEl=dATLKrnMZ2 zSw+0)+t#OD(5aZ2PIm=mGBVG4)@wEuWl=%=YE@XvTFSte@bE#S-bD5_Sxvr}2Qm_X z!nl6B;yh1O?*xAyMqst;_4jRO9_o$+5YW8amnO^Rm)yyuS1m_H)NJ@pe)FViWv*#- z>6{?ut9^CfG}rm!mMzScEfnzOucxyg)y|_t|D$LaQBKwRJJi-|0g_N@07L)e3;tOL zGhq5?zDIRfc7?-^#SGg)Sbq_IjHnKzbb0Tc=4Kt32!upI1D11+S59odV3h8bJcM1q z{j1)##6MD#MtS_q!N28>`rCcI;s@3Sg+gN<;MQM6a>Glsd2Ls>4=wpWOO#OYWy|5& zIaKD%SFX}rd%b%*Fl+NwH(GP5))+i#)O{HiV;*bt(X(bm0g#+K@C|2MJUG4gX99_> zCcEH?fmfUEMt08GpbRxadnny>5A(+|=lT3KMY;D3T6aP>{!)01eehX^W$PsGA~*97 zdqbhE*GxQnD97K;@nI~0k#Y(?QysVIBg#6vtJ1gOy_f!W!7@-&d!S_FoTLo?>f+Be z;|*{8@wY^av>MLH$SBm(GG!L-+*k#%KzPB74-K!DSna;)zB|AQU{G0cR3|%^mtzx& zu{i_q_dorYH!AVd)i%~UUZ#9W_h=D5$1vB$IjG-nH#t31L}+?kKgK}E!<;)9Opm+m zyk^{FK6wRYmFY$Xd11^9!4nLn!oTWvi(a}`n}R4B$)u7a2!bQoxZc2Fb>HeX)h{tclw zwz6lM{F7%!(wJ_fwMqfT(d&vCYs+2hBj)QEWi#N=;l_*5dORQZ`i;;PxK4b%J5{{6 zsOW{y`n4#3hoMb5sJ}Uf&ubET)BUs(_XO><>DX8qCvL}wakl%L)98H#(J7VSI`yB1 z@o{{58o01c7z9rcXg;y!n31$z*`&2Y=f1IhcAkLS?jbJibH8p$W2binNkLVJl}~ya z)YNKbTTTx7+`!AmTpIpoYH1TJ=2?e;(m5AE%1o}}jupC9iZVp@s^5FrI#|-hmlyovM9Ds;~ zj1yGUPq=`mgakQ;UrTH#CtfXbulJ12p$r1|W35AFF|+Aty`ybf-WyJ9SD1- z--FJZnif8J-gz9LvE3ot-VwKxPj$G(Pfh*I^O^XoLJ*YD?1jZpGA7{Gf=bHux%+G5 z-PN9HojL%R6@1P4z_@2K+WjLbDNPc=(eZL4R$ju;@aAjHX1Rj|j*J8e2{5)`*C2OM zZ|MDjii;R>He^O8JSK#(ZDw!!tEXewlEq4oPk7+gfGjiC7zQ!NClQS{ zAKMVxU(ym?ybn5cFE+>CexxRkGWcnLp9!=uZ-0-X{pcDW4o6?+S8SqVd(nRV<9!qJ z$t%vUs~!z8M&C&D@?yGaq8gb3MPDPmUAV^5`=R_MBcq=C7rq;#&{fndOWt2nB?xnx`UtdS=}8*f%(dTv`R&Xl6dr8SU~&G~Ao+q@Vb@q0PJ3 zN7N_G)nD%cKwn{QtN^Fsc}h`nkv+#(b)&Sk94N+pn3LfmD>C5`ejXGX*PfBAU;g4v zG$<*hg^<|8GSK(8Nlp3}LH=$Q79i&3Hl>R@Xj9kzK$v2~vxWShBNIYGZp}uEzxOqq zeIm#15$xG4Jrgv&j%=e5$_KThRxh*`<~MEHF(RE(2PXgclLhOpbo&LJ2hF{d?DYw2 zGcDG@IdfPt#-jXQwMV*E2(2Kx`TH||{9D}{o-HbvZXIrqS)AHM&16Mr?6S6hcsEEm zF=Yh1H--!?;w9y=LqSB+bBLgra}=y<1BSaR$HLxrD5|z2@6Tx6;+63ZU)(%l*>(8@ zy!z*tce<@VdwYXf`RG{fA{AHfY~sR_GTXW``HRIQAj`VACMX>{3=tMO@PYBC7Q*&< zP$+SN)V>R3!M6~laQ|123^|J%<~HGv@HDUt*|+%G_0&}N2OWO2-2I37{6FX`o0Lg+ zw)&nCU}yHEiH%b+@m`P@2hJ+9=f9*b!pd7g5yMj)U4_l|0NowI-`iuF_?q$!QojFk zjRyVPSj5RM`Fs7Y^=#6Ab&}qFy$IFqo%479Z>=hCMlWIh->-nUpU-&}1IJjSl>t9q0lOALLV60;ieAOnK7!l+wdaioY z=%*399}EuW%rHOzf#z`055wZG zSLe13>|_kg1A`Rg^0jX79;WuCeEUZ`;yL>sJt*e}y#-Fx%5sR1R0RwA)E@8p1dvfF zw~g2beHA;oso9h_jMFxJy%enwnQ6e-%1{CTj^vqpmI-e{K|x8L-B}GQPibr2;T73g zs!gSo%15*r*323f^52v&w5T7z9GP^ioE#k8%&qVq0;DC{+MfO&TX)6inTIOTWxq&A zy=0SM4(e%J>4+#RD^K@>patASB_t#&XW24oSY4Ne0X29sZ=-MIPp0kJJ1EF)$&_rbnNCy34JRVCC~r`XfV-Hr_yQ!Y-lv#mSRKW+4|Qg$j3IV8Za zXl@wi4)t{&@7F)BkWAV^AT*DQs`AORU9y`%rnnObUN)m_xZ_ z8=Vk>K}^mF30{-%_e~3FZKV+28=qJr&}L@19`B>34KQFddY!a0n10Iwh$kP*hjwlq zBX`~yko)B$UBsg2)yqe^CiW{L(b@1a2-w1hJhSQ4IZWVgrMgx|-q}8O*&-Wxo_MP| zMI>{f@Tbh1s2^FNMiA`~&i}272PP}h$E+V-3*bsT+lyyGs0Y+Ahv(pxgpCW!T%3U; zanVTqH5tzb=A7E&)9xRk3J@N?F`1|}X(MZ7WJZMlL+;-;VNH#Hk+h*NhePVkkYCGY zpP%$|dZI~wIMGls1~bvXqcX$O3!Alk{zuUhem$`U8+~#bwzKWH8i_P9pdmi)6=)%% z<^>n6@P^rtzV^#Cw?%HpLS`Y{@$+YsIJU|ZuMUt=f~QaY&xr-i#Ifz_ii(%!K{?Bk z=khBz3&~0)%qG+!JKmQkVVe(;9oZ>xv&*jHu6ur0(!u|tc*~duN$2gPUz@ettVsrG1ceI9|1>4M;b=P(-7>f>`NRmpr=}R|c3aZW+uRX~q02Q*^x?0K+Ate=1*L$m17$jzYkvdFka zMSHKxuj1pE4}~9?$}^|ibdvsFeyjz6=$6>nbAHlGI>GAZ+Ca%l7*>)b#X%Y{x5X|f zT6N4oCynSm!Kz$V4s#F!jiihiBHC0b7B+^t$2s_<)fZuT4Ld;5D(?WP+^+4qA3Wq# zR#Ia5{K+jbQER1c=S_25-m59WUFA+O-9yjmdN_wd2lj)HdQJYsTgp3FWBwN3JKSJe z2E1N9&rsCDPk1l1g&%~Z;erj-^*bMU#@}HW{(e40i;E&ZlloD9YqjuQfnYo8+7Zto zt53ii&(m}EvX>ie5OzfthP?1YUv@EMf&r=m`L}z#=vZs4HI@!Q^eom*HbBQkB8QHZ6&b7w3mg?ImJ;Af z?IjU6;*@GlvCGH_$Ei9Q%>h78QIVMujvX%4;JB7&F}4IL6ckiRWjPFnk^aZQgpe}B zLEoP#ZqBDXzCb|8f#)({cUBy=Gk7t29Gh7v?6zRCL-{_EtlhdkI{@;uW#p(*7MWjs zys|!`V}o{O4*INGFc5t(Cb?XZmA1?TF zuF{B&C3y~4*iZihxr?@nlU-^HysEAljU4Fb{iP9#SXFkcYKIkNGk(!7|Mi`B45hwBJg8MVb(fO6)dS9o@ItpZl`GSWFfzP$pRH~Xk z3czE>H8~?AS&VPVcA_Siz2@;B$z+ur{hzNhPKe5-N~EuLfbNy*1chS%RfoCG%v<;3 zY0%Afv3Jqo$h)hHQA_z1$Ac|@^13V94l7ahfoYpX{~&QskG}aqJI|k+Ttx$8<+9^A z!Iza_ek%m3o3Za@R|3`gs;+yKpKwCt?wVfmPUDy#TWf5oy&!i^?} zt71Sh%mE%587UYor%FK~rJ-P=t>&}cE{k-K)e)2+b8DRbAQLV-RC*ZoP0JMoGi$U| zfd}1_0znVBf@>|?-RrvFzZvAh}>x{z}{*E6A7*9ks2E*Y4SW-En^b z0fpN$!m!wTIb_4etLD1sL=_brUj|)X^kTzK7TD>Scrj2qHtJNvmSY~8yrph@E;4Cp zSQ(m#F7MR@1fh2xcng94+BJN?tlaq>AJPHgI|6tBkcsTYGMSjf3R`o05fxi}B?ofG zGx*W7@kF&!0wwG$^+a^9d)ew7DzH3>h|tCkAo${lg#*>HH4R{GSQKm;vqb?dBHP* zhu^V^+6q1r%z`q!eTQcST5HSHuDLV_dX&rBqj@PEJ80uF8+GyX+nx_b)%!d1FRw<) zX0_-DSv53FR58Qt`YF9881JQ9Vfr3Cg1^p1*(tWaQfO9s-~7ZfIpxDhpQxmp0o1Cbt2f4Ajh@COySj#n7IPzRW=c=e z4EE^VIa5dR4>*qZ9qaq$@>`c4Ih-@Ce=j$S8k{F53A{h)yl!ESUWZF{&VgUjk~RDb zgW?FtfR3WhU+^M0I|yF4i?s$QGXKMGJ=XjmeoJK-F(9y3g&XJBl8Rm#lJ@DhTCaiN z=6dFH(kufZwUWho1plC{Wu7P~Ezu9)kb7n2;M21QCu9dR3k&}h3wW5Mjgg6e(aDy7 zTHWhn82c@?(C^;F^mC)4Qa4mL%e@5zXcyZ)^5dxBI^O+0Tev7`LtvowJ4S;Dl>q~b z&zXV-n2YdIf*0A+@Ax)flPd|6Mg_nM35k4jk@^zUMae%I3yT$2vl+b%-<4NYB^e*Y z^#0AQ>a1GDzc++K0LVX3H>t=wh4Ex*s5`!??_ZWXTonN7OU8nz=2)ZPJrggOiWv_r^O0Pz}lsU`3Iqu9|iBNiDV3sq8;S?T)Z^_fWvrSIF{ zZ{5ND5P{O~@dnr2d|_zi#X|IbKrqzR2;aqGP#x+}9UMR&d@yb$&7s|Cu`tT%jB1Y= zNAOg`+JZq9cs?|{A2D(-5=$#e4t0!Ri9euxh>NU?itp3@-!aQ3~J zJByqzt?$MP8Mlc@jwLo$KF)m*?zgj_>Yt6B?N$mpWr^(cEl+H$=h8^*{hm=_5(!gu z$>QK2viOS?0&0BGNG_3E9|J#QE7v(KHTF+WyZwkzl6MhGWmwtJ5slnC4YF#vNgLCR z71~mx!r;%KsLcDAfagnZ1y(^dwzcrXsN4bqMrYLWB?2YqK5GXYy@6M*+i~e&_Erg; z{$74x8ejA_p>( zC<%!Ke@4)CBV-A1i&qULyF5IE`JN_H3%%Xo5d2zML$Ud&GD2ljECs9rFALy~7egmF z_4k~ePcJ~3@=%D#kuK|R)f9?+9iVL^KSNNdZjG9Twc&rwB$$Q8!Z|+*w+`{GuDHJK z#H}NoFFh$(-?ORgjACbTe`_4HZ$?p7KPlCDg<tSk{lV$O`vecu%JWr7!c2b6qKn0V&w zYOKhq57AZA$T&|X64AuXNdplGw~ffGtGJk~w4cxkzPdfXK~XZa*JKhB$u-TJ#OLz|#@<&Z;H~9E}4CZW( zEbpeXNW2_HaktSY3>kI3dc*yZV)g zxPLL?74TH{pHhU*zL;LrV@2xKZz-&yBYSf@Wsz(z`NFJWia*% z4XsxvPOb^gyL_;kOLLLnH^XPw!F|lk<{^Go$$#=kgwJ0o{Urw4e{oDfc=BxZ$1HPF zCikLrB8C<{VGx01$dG$9>wREn=hrLM5P|w z%2_*ZwG;|>Z9mE0G2yg#bZhB5Zgqo_wb#EO!9 zg5J=Asu6}L>@t{!`6kq$>`CnpQ8rl9!4`^w!t3I?vZJ&WwX;ryebp@IE<>%NWN5t0 zDBRBuJqugaGb0u7WEz+^&7MpKyyZ`+9Nwz^#iG3yMvwtb}b-U2FS4 z&Yd_9IkKvn{PDMvxN0`Hp2<0dt$8o+1z4Li^t5tVQ>v|PZDASkS7?LvA?`JY&hzGE zTzxfFz15}eV9kWYPw8}%>Ra}+Nf4BGb2^Ek2As%GSU(1aDrwo3(~xObdA@iUFRUBO4a*T+9#n>AI%wA`$YHxq%?`ELtC z&WXNG3LmQ7382g}GA#FA)2Ip>ZcZ%g0~ynvM2;bd7^15s zQ?*B^(_Vv;yIMU5zRn@~_#bID=NEroc@7+X-+6$Lus;EZ6GVd!>%t%g)C^r0)(K|0 zT(|Pde;qfZqnB)w8X|UL6Fr~IAN+Yg9?iOlH&UmM@(*l-KS8)3KBfZ!9Wu_XUsl(7 z4qs0|>!OD0t{iHgkg%6sVj)NjQDJJO1)0tgmGI9uV;zs}a1U=~V?EI=muvC*QZ`64 zH!!V`9Eg%8B1`f!_8s1_-F);Zv1p)#j+KxX!*w(H>(*px+qSso|^2+>R zuYbA3Vf7Xul$qjRV)pQ0Y<-odlz~I|jV&sV$0j>duUy{KNlwq4F@Z7>nxjCd(_NAH z0irz2w=vmALGD4AFcO-Go^Ovvy_+r%4fBLWfn;`ku0iXX%&-efECA{=m zO+>xhE+pgk_4U~43;sb(cI7Msii?OyVn1!-u^MqP?t42lnL4Cy zSg6|mZJp`NAU+|laL}a~uZAHY1-KKnE_deijHY@H%FaI{3d*a5; zh-qV7Q-Q4wjObvK>MWnTc!Vtv8dkzGlO;I5K1EN`a~uvdI=tLje~@L1qC4I$C{8t#tI$#s{9@uLm58{tC91@zY9P;1QCU);fXFiPDou z-Yo6SG}Q#K<5?hmTooAFhKcB@y;XHZTEuqQ!v9N(Be|OKxb|70MWNuweJOtj@VIhn z*Wz2qNGo8lD8d_itm<&!7B?YuYv^#ECahza`Q;NRI;~^J*uX~B?8pD={mU=g4#vBF z2ee6I(lQZrEBk0fLGfi!Kn{}!nyAC=aK7`nv^XW>XiMmh48%3}N(IpoW?Hp|cv=5R z1&FYrvg3hC)DM+uW)-;w0!wD?qr;m0mEPW+|92kMrrS`(t{cxXXSPm1^zIuu%KRsk zd6(uDtb^wq_3Hsk0uXA}7dPJf))X}0)*)6-qn7`s2-GV&dXrvU-Suk4i}S#G--{v% zUT%nWCxdvMbxka-c)|Y0P`X8yx>2997441wzHQL`L5y{7YLqADms|d0z7kj*40N-A zHyphCx)f}>G8;!tsyK|{mHlU5UaPy5Qt=TnBENM9w9z&K1#=t6THRH? zM}w0ec-07@joXWO6s1MC5<^#KKtTO*?)~~UvMgNTAZn8GURis*mL62MK&Ee*>H4X@ z{S?(XYHWCivs*rHQ4ZxqSy)}HYg35Sx}cHtrLOyf1O*^MSt$9n)nco1319hOk#3;c z{l;tF>0QL1$Mh7Q#SXv;F;*N4-sFH-24mu_|}rTjd_##!=JDI4==D5B8G8Xi-8=aWtH zX1mEkz;f>7_VRr4aIaZ}1Ox0MFza9`ahQzGmp3^$q|3Bz*Y4_k0Pd&0K5IA{>iM0x zqH+`=*l*~vogR8QWB$}18bfFQXMy#V9uAP`$x2Gd(Z?*?SX{q}dtnx~IPH2mTgKPX zeXZJDx0Y$yb$oE8V2SGTCZmVVJKh2S`a(YE*P7o?u&iF7HeE~vv@@dYx(|0@euL6! zN17it+~0F7%8~Y7xSN=-^q&KH?~T*PD_P*GNHM7)V>ajG{Ie(L1tv`6(oeXOU-)8@ zg2Q(aOj&~3AFsga7N|LvLU%zsz&{i03{Db~|H%q^Bk^^=LC6p)@Y9D{Z%5M6%!#n% z$_!^7CX6A2+l}lOa)5@G9z8UmH2Nu19cBf7cNrS^`R97Sz6cNg?cC{f&RM8x;RRyF zPYA6y=RBOab|I#M5^?!Wq2GMp2}JFQCbrL4@*4U@tghum7LyeR=0Zg2{FwOU_;BKY z+QEV6+-v5I4bvU+vEW`vDhaUY@vKcM@PT)8@y&IGm>Tflf#8;n$ZC*Ydzzp#sC)m# zDQ>p3VW$tWQvkzNyKfT1J`vNb*78{mjuCI20Ur%Pi=jv?<3OR4Meo@$tAzy^QoMI- z&v!m`yQ_zTaXcFB&=ksQ@T50Bp?)j#>^u&+7IS7Kd^CnveLGpUfeAYzL|31gnEtVN z)QeCa1}aq-_b)dAb%{D}yni;{29T~#)IOh6`Xc!9-fb&(HT#T?e*|dcN?<*_O(t%1 zwE+9;XwlISHyu~lJjlv?5nazORQu@BJg>xgR0jHBjK2V4R(+Unr147}J^f=G6RUyQ zLhzV}r@069jTW2X5+LW7i9YTdl>`FX->Bpm(SF`KC8GB;w_;r_Xc0 z41#-K6nI1-f40_P4bCQbS)N9^LUoyy=gUvIpO#h#ryDYcC(MBaH|6E zKQg@VuX1QgoojDBSNWEGU(bDYgKf-|R^-KCRqT+@fM#^m@O^x#Bn=%_R45AIOMf-d zd~shFI%R?p^P08zS?bSJ6|;&gAU}tsrQ}tM!7MQ z^3?SEV#4h|$f3xoDb5{(B5;eglyyd$b&(_w~L<$?DRprFgzsDsFQVQ4ZcqSlZ(UYQH2(&R7-{LLO zi-{GZ_p#mfqG*7jL;_;bkB*N3*jDq&syC)480hJA7ayG>rl-Hfd=*zp>q&vs9XI=F z`p1U!C#~%xqJev}oZ|DTGr(7Aw~Zz#Z$Tc_X%hxE%Q{-&IiJj?QVp5phv4@fqwi?cspb4LcJKN^l!#{O?IkE%u&jRqJU)~@Wn21=~< z8WtYx7IcKS*VtVCvJkw}#?<$S-S{Q0h;=;ck%&{!MJ?VzSM^GGa6(Cyt-!$NaXr7- zo)Lxq>n{TSa~Cw=Wxq6%>BvXqKDpSqe9C*b`qx!z=DpT~F+BU5JO+Xd67@z$ik6a| zj*hnC`COL%o4$1@X&W6PEOrfGcn_I_`3XrdZ$Vab&e_rYc!o@>S^Vq2J(X1MXGXo1 zzpNi}s)njtP_-+_dSoVDJjqh^hJIm*)6I}8!t(I*q9Dni$)`q~Wfk@_}4YeVnCDrK`(4qeKaiDW?yoe+DQUAl?6aoeMi<15lEm*=I_aTCS6hOt+cpxie+52=c$P1u!3O4A0ZG~V^HlmG6BDvq@hRUAH&@nQ1TcSQx= z2T$hNy|J~m5q@gQj#%RAL{j|d2R$m|y=UKH7U45;HWt9ibem*b% zotpnO=)A<=9`!``PHnJ_HM3lhukfHumu~@|iaZ=rx5vjs-1Nz5hW?rnbqzC1uf7Wb*E zu059#4SKNfN@YG1DI_IUWTAxn(B&+Ymh||1NIlDzO>w6uZJdzH;??W&npOJwJh131 z#50a{EOPU)qur(jv3GE*l-ig1TPtKQ$)ISa_dTc-)80RD-H^_Pe%hK&p;P>S$yqMbs*^O* zztJO|mLs}|PG@6{RjU6VI+!qyA}DevQVLa_lFmk#&r1TgzVq_AsnOrvGSeAfZR$PS zkLe;Nz6omZqL&eeUf|Wj!rMsD%)42CQ~w@?d@PJ)8~}4;LuCwP_x48T0rlJ9MJ?yy z`TbY-g?R3Q=ym@;vs$EL(u&RgP0cU&9d3c=AIiqL@DVPrYKR)+RH1tme(z1Jc1k=K{9B?JnaWV+%A0rl&x1ncWom0bU$Zlx^0 z<@b3K#C`cRGr}LOFKZEcaF!+?rv%AjAc?bO74M>fXGCHgPP$Up`Z~z6G{54@981GG zM%+xjI@B|ghTOKrcD8iK6YNb{l%@ZDsw9`Uir*%o&Hq~s!#llO(^m~`H;ehZ^-X!>i#Jd>2*Vu z%pUE&jLJzIsL9OnTgU6Pw_+Z2W`DlMkFNEmIYI1$iX5I1=XsQr}%;YbZiE|xyTbq<;esv#Am44Ua zf4|xFhREmTH9m_LbQ^MI*5$pJDs<3=fCjK&wa#k9G?M0hl6eMScD@boL|W`VZmihM z?;j`C%-RmXApzg$<=2R6-RY!ucc8LPH^EC@hSMRJ9{~|PCzEkX!Y)}u{3=bVc+|D( zA4Lvsns!I4Ur*do2HBc4w_WP)4O3{i|Nf5~`_-DCVviODo08T|x*g-jeCiK%6@?m< z5%?^zDby<~@{)iJDL@d8-u#mNI`*pyvytp_Suq5(o;V+d8BUF(6yI zsQs|cyIxkGFhT3}N@dt&Ki*4gfo}>Ei;5bnppHM4!gx$+A`%Wr$qEjP^Gl*?S8JNl z_{E||-}P2ms|xqqO$`s9d&`XS#|9|@FU8n}OMS-=f={Y6fC;hHn-DS@@W7ydufs(~ zq!Xo-8{^jL#^4g181GZQY;+J%u39crx4FUR`p5K=>u=;nKF?GazVCyQNVF~kb8`W2 zpbo;H6+@^5wIMU#CS+r)Gkfc=i=Qdpp^**{XxtIoI!>^TbVZ#_N_tIpD|wb#t4U5_tw`((bo@@vz*9xAK2(07vw*A%kf6? zUSZz}*J|OBVc&kb8-Dez^L@q7=xX!jL63JMTKi-@Ut!yi&^_7<)6me6Nf*|Tugwfc zL04YEqojk;QQrF_29?4{XeHtKsIpJd<)_0u);9Ie`gZ^yJRX$^Wm0_#L{hSeNRTiYzkdj%ZJ!YVHq>&e@(KBsYM-KK^ z{<_)fC2M@8*FZ8k#Yjr%Q;m$IPau9h=ZBsm%VLC+mPQ-Lxi=u+cW=uSZZ{$SAe030~ zF>^6DzFM286l5Is&|)HR_<%Due7^j*nVOqKz2FnK;;LJj(LCduFT&Xe)qfAT9gc8ZT&JBCPC-j8i+z$^6@%8tmaJ#%ksBS8a6*J2;S0&? zh|bQ#QKK%+%?O%=2tGa_rE=9eb<3*j?z63vhQ`b&e=#?ohXl7S{r^ua;<8jQ{W>}H zwkdzkSTbWx|4%1@_xirQ*e)gD@>TjyMNl|HyPX275nD; za^1C4Zb(Ba!}IAt)pvp(`?JGVCB;~xa6($;Hty`<*=%mr&{@r#^FWvf7ZY%9+~1wh z(&5O@jw)u|!z>Zo6~1oc*h$rQOQhxX?;Y}TY5Fyj@4<~-=h)84-=s@4Z8@9fN- zX0Q5@{RnuQt{Ew0iNI!#8%)>NeUe!pHu`T^Fb#48l?F>DLfu)mt>(Av5={Zdl}uU? z8-45{UN98p+fgWM&akR}tgn|4Gai|C%WD)q*Vh zV^c?!>Aj}YC@M*p@V9uVPTq3uo)Pv~+3CFe@AK7rY|+`lZ$d~-^?|SOFwdx=H2r!V z1}W_^c=Pv%bej$m!p(iV2&oKc0__Q~-B+zF;>H`Gp93Uq=)9SurG4SU<;Ssl9Fd6~ z^}T;{{zQ|mQW?@6sB>g`?{}MQXWQ=jK~piF4rh|2`{YB+lmA1R|I}Zc;7qXWoZc5& zYGbCk^YyZKlpryP$|>Lt}&7H-)t^>({mrV zxxYK-;sIJNbzue_zM7Le)Ln*+ODcqh|06x!4*!qCdWt%BSJRL1C%ZjS}tbBE?@cnza7BU5c4X<(pl hFaH)rLvDUbW?Cg~4RJ}!1A!VCJYD@<);T3K0RVt`P@Mn( literal 23999 zcmb5VV|blg7d9F;Xqq%`oHn-Eu(545YOEC-ZEV|EvF*mTZQIVbviE+w_qopZgMTL0`ztNWc(72ELzgAq|6Slnj7=g(84TUh~BZ?2a1G0!U zbwGd@V@5V1tTJDZPkZ_z}}0RhpFx%V`D>o9Oiy4y>%C5&ieXe zvf<_V^_9|@R%Qqs3|@%cn`$SA$PK=NHB2@J8VsHxql!y{eK;3(Qc%rAg1S!1 zwu5>#H82qN@|zPH7+2yj1_?Nyi~k+gdMVED)IJw%@FMAFy{NoIjYyu?Dk)2BxnY1bS}a+IDH%*bW)G!ie|gLBkB&d|8br8IJA_O3;@RPGIJh zIYQ;>H6OoiATEf+pKx}jHW^9T3fSWq*%5&rtzc*2I&%$)pQ4NUC1xg#b}v4gK>IS- zct>sGrVRMiW*2&NT65mTFo9jqWkpb+^N}JH`G>Rk<@?ERx#!KyyahTbc(i!QzPPog z`U1I+(H)4esrqZscYI(@gm~puPE>iL%x421OVQ4wqpCjP_m!+Os6vD_P;@R#1i`gm z;ib5DTkSJBzR%KmJsD(yYR7AMZ$0d&b7cc|unaECb-N6_Lh=^oy>`7i>Un$#RHNIQ^ zb;7sGkCfFrzDkc4g53kP`Ab(lZDr7O_3;|BC z)bAa=I=x$6oC=FM%cGAD5dNJMo08VF^&fF@;(Z5ukGrQgY1dq=JL|)pP_$94LT|f! z*P-t|+@U-nKRLT0c|h@sMG);Fr@(%OqSYnQ{kl$=8EYL(FPT6*fchbTwhLAd-iEs( zW{$5}(oN7!;!9+;SXhoPF^>seL5y99T`aTcgP<}YPIOCOa6ifg>xC`==bq=D#`oJe zuwG$1ztas~pbF7(l>gDM8T z#coqRD$y1-E9Mq(76BCBE6U{a$o`xTneLbZOe5wmD<;d%%HAqq7M?1#<-ExMEL|^+ z%#tg%(bkuYF5EBdpQWB@&bUv>>^u9O!yt}@7h*%hLgPsjs2r;tKa*4I?T~Zx?pXM^ zms1cgPdZDwLb_?BzBKOyVp*xtz7gpP)u|GZ>eCd z-BFF#SgpyNyIUx(F{yC2Fw+~XTDEc>4KuB4x2)1?T2^s|agB8U`JC{xRG?YFSAaLV z2f@(NP}{zX-G#H%p6l?gzkh{daR1k2`pA!wf)SAvkzJgj-CZ7lw|kY+Bo5h1`nw6ylVY z06JYXoiUxPb)i+P)xLGp!@;A$!{X)BE8lDC%QLk-hQHDvHj*{0D&82fC?Wz9^?NsL z16*QwQ!Ow$Sk-c~-`U?=zVln#!ouqM9>F`~ntn{edKmn6)G_9}{XX4S&9?;p5CP~% z_nsH!g{Ol_&$X*lv{O{fz%|BvY9oIkA8CALTxcAU0fV7P-?FQ)>q1{+!`ep9#(#qp z>GlSQTJVFfdV_yBpU}t55e8D?Bhfj2GqA7q6rAhYWE!3MEPp zhjt2g3Z|x`C4*zgZU@yyC~+e(21yuc1M#sqwuFNOt(Zsu?MD2$4)6}BnCB+?L5w?v zGZrItCLv5FT!xoO_G1n_CnGbXvVq-usbBXU-jcwf<;2Y_zVXit#M)mh`?Ed|k4Ob( z8blk=FS0aoJ#Jp)Zpd- zY^P5rB#SN!UJYVRjmT7(dD+iHVtf7T;6p2dYo3LP?=!N~qE^&g@502wxOwqCn@G(s$bU8Ec5xVTJi56Q8uizK)sbu+dKGvH4^r_flYZWR*&RMl zIA5R5npLo>ZB_Dcy-PiAx(OT$Bs-m4mGL0I%YUlaLA_Mi-Q61{iXLoRYmM<>d02R$ zIa|ywxGJFdtkIQb0xcWxJ1`KenF9fg1Y;lF5|U4od68%oHtG1#2=<9A?Ks=W0IA)Z zH3yTQ9&BIerUa4?Nf){+Pa_l75o~cz^f(=bY(aH&=L=CP(az@7l!iT+bqSaox|EdE zNpjMI%SVbE9x#iUa*cu7%aLm!YME?@Kh5;RXbHF zNltw$3tC+RD?LM6Ckty(Tnh%q<-`fPv@o>OC3Lbdx3uMS;{Nhi2~N=U+he*fgnt#W zGvofEDkV!OUuft1QAyqLz1}UQ@3r{fmZH5;rSL$xFmWJn6$DBPrar zJ59+=yCW&{hbZ{?Y2~KVly)aeSOu})2K@%|d{BJki^MGb;po9h+o2M`Q2V-|G?{Ex z8xAGC{&~hn`nerZhO}X9N$T$+-ysqc!M<`O-XGYmCW4`UhX55dK!G?qGl+UWyln7x z3u-MQ5iVzLJuoChP*CufnxEp!-MN01y=LEACx2C;_n!K)_QOn|qM`y87Ph^?b~l1b zh1SW{m581FQ;q3#6s1PBv3HZ>X~*(1p0>7j<;d*p?99#`*Z)QV>Ss=pP>6_YxyiBj ze6trB1LGYpFRx?@yBv$bND2qL+g*9F*=#8usZ>(VjE&!)Iev#I5NrS8-#a|~fkvZN zFpgSnZDRw%)6+AB$6Y;jg;Fl-*Fv~>Eamz{u7uP5MXq`e)_?lU!2nMNR)>7ZkxK(? z5B#2-R4CzeI?J&0VKtxgdU<{%(x^2z#WVUdO^_+np^i4rmYSVWnSKnlKiyw`IO1`= zp}sj;4knXHYwzvt%?LyKf0ma&I^%MGKx=Wi?#ST(DVdVg-p)7Xa5TqYcQ_-}bLHgZ zl%u>_kN2Npi9)dUo{i0qkB{%omJwjHSyHQ*tLdqisIxSvA9e+z#tGJ^{Ko=_MBl4A zQ3(jbBO*RFY`Lwqdj|vuN8_kHto??3y5CKoFs6Ln2d1Ar-P<k*Fw}Cs z_8p26*V_}_!gqO{rM`gJuU7S<8BNZ3E=IywcbDO0CFxqQ`GYL zbqdXT`i{;{ng!RjcJQS(PlD3Y(!O-wHX)AEzun?5NA${un>#uqHu}_(4E+Avr$5k! z`ya1)dyOmIzViv+U!&*4|J)W-wOtx&ZoL9kRJrqyi?P#zJ2<7>E|eSo8N632Y#QA6?WJE1tn2)LtaZ$l&J-Tvp??O(vtCMpB`sQxtQ9rDc!FD(Q>(m?RptSC8u0;I;a@u2i6)GJT-t6tez^yje z;$7~9_LORwoo@)CiN_WO;ByOS*lZ#e(v}=AG>G-oh+3t*h)6OgF+JR5=dp5#&_SV*&L6xVC4Y}e)r~1|a zVS~-2!cJ6mR>c7*65^iivC6BTuTMY0liAuhRkq-FuG(Ar$kp;fk~E#4J}u9d3Mop4 zco&Pz6yIe^;W)M3BvE@_Jwf}hmiBIogn!tIffPyyq%5tdyNgrH$RCq4_E_AWo%6q{ z*BG1wzd8_JT^Q;kU#pInsYr7(1cv;sv;#N{v2)mQg1&kGR}q4iP|Ib%ECK(QzNqdG zWHNrbT>)T{Nmrqg4NGE1L`U z(g1CEkz_LXg2KWZLy1gt4Yt6$yajeOAlYx4_h~g(O2>q~WUo`P02iteCLpz^#XYOw zbeYc)869B*TWv9lg@UQ-ghtpAaR5`#$x5hJd|AMRiphRI>cqT>>I9Dd^OJ$^m%6Px zxDc}h)!Mx|hW(?Mfn?0=Rc9FV_ZTsiMkg!X1Cv0*l_cJq84(LMaybYB#R4Bwp&(I( zzI~i}!}qmX_4%A!u4US>_Lu6lg4bC>zE=AXfYz7#d!(5sd+C{Rf)>C5oWlUMHWxTJ z_-{R&9Mc?Rf8EZVjmJ|my`GTk$`stB{%DnKm9mEpxC0rNIXX7 z$|}#-_mKXDvYC3uE6vGEF{D>F`Y%rvm2DP_t?*g5H?&qW^Ky2J`fX0<@t^3wqdYyW zs7%Yf%vZruYu-WUNo!@tp+45FT4v!#LxOCtXLod$H;oux_>1XnfAqGKZl}>{?J^;h zk&&4y(ZJNz)xEnM`B!@*l&_s228ztnt}g3qj4!@AaPU3{5#g17s746dC|L0E1t`>3wh+ z$XK>wR=f_U+QAVKi93qy)kkORvXUwF134eCX_6VY^?w466|>~|rSUmLW=QdWSHyi9 zWCAB$D~6KXDJ={@_UCrJQQbbPUv3U}V^Ut9dCD~9eIN3QkHl-~4|OZJD^yY*;Y^`N zMUFm_C=pAZ^r)mw;f8@nQ?;{2z9J-sOsCUV3|gB5^Z7*$f^G_5^Tn|DNCZgS+KDot9R z1A<)g(l*JHhxbE+TufPC{BYTWk|#(v_xUaGcK?bg6Jxy=3zf=RS>(?Ek2lBNY`;~A z5c<7s+_9m{w4=|gWks6LoCSh*=RC1bR4j=a?HKBHn!y{Q4*8*$PI$hVXR2h=s4sI= zHm*BM7UM30Qg(2L`(u~ z!*P}I@LK@y29B-Q_7e#fYnLZV_Gfi4vkm&Y+8qY!ESD8-8){+Ymqrp8B(@6BMC^_i zoEhw0VR>J(49sLs=xSjfe z2=O3ah**KGcK`+P12Y8*WP(CM{a`=1@oWOa_{Tja1^ECpf>2Ky+$4kg>-n&|xuUQ8 zfb3ZH2DV@8HLvFKh9OKf%|ZQHCXcrg{(j1Wax3gD8ihIDxE#FIdcpDnr(K+hbo)|Y z-Dvfq`osu#f3glJB-Rw@idi`aX}izAV&367JSTCD-i?A#h??T=^~S_}W_`-J>+PrD z%-M%))z{lqLT5nGLHu3(!f4Z%6LB$+-#9P3X0KUqUShMF6Xo%L_&FSE7^AOFQsZ`S zhk(m2WJ#qw6hj4!aXDTYmRjx0xJlW%V7}l#XRX#V8P9T`IF}n4Uqs?zH(e7=yipg2Fv=ZE2d zs7T(eUsr}UJHFb%1&?=*Z-^+UbDiWAD%_shVf<@#zWpzL4j1 zwuboh+%&LX2y%w?cJGoewMO1{)O&(S4p^MkCAb!uawy_N!b81A={3DU=)ID{6vl?= zB^#y_g4L-$XrEL?-jS)4t?-3VE5-aCte!C4pXh%#*mr%CEt6icH(!-@wEK8^8&x!6 z9E-89ARJY_vrtCRX+SN1vgAD7ZV2C(#$*KbV|XFoVxrVJY`ua?TDb=lvSXuIyOZmE z+Yme&R5(w=hFA5Vj&q-!xY~+ZZ0QAHxt!Fv$~AsdiJ>JRtTPAFkvbO6Khy=GcVd3P z$x=Pxvd+E>^MO9Iu=PZp_Y7P+AUUlQF45D@prBqLmoZcX5@UZ*o2mU^Jdpou*G!(Q ze}??PH&H5?La*_5=HRid&a{78g}KI%R&LB5$VT;9rq&#=jSemEIos?TxL3()F<$!( zdY)}U$UHy2y3q`r**3h@OB94(OkajG~l%ko;*X9(wn1YcIEqL-@S`!&R` zJkrn3qQB`-Ay*&KLR@m6-S6VbRp-}v|IDf*@O_WjyV2bi-2T$(bh`{8zk9Zx>btV@ zLrS!iV2aI<2wHrlel(VH8Y4wne|sP?Uu9IllJ}WeBTf#F>~9Dsn&dTDtX756H=lWX z*8K8tm`^OMe%0(xW>Ocq=jj5 zmJGsT$iv+|{7|{vVZ8cbDE&XAQVqpe)7cpoa-%HD>+E1WFP=rKpkm@-Hii|Ylqmz24O#emN|1u1IgoJo$ zP)u|&gCAQqrRlwy3C}Ka_pRD*LD`#G?LjNO!HB~uu&GQ zG@ncsr*@)QSbxHg?Mf`xS`lhLsn*zRjN=GuUs~f;{l;-Y>P=vDh^ zNHC>BVP5QrmZ1%>pX%A+u+v8}c5G1*s84(2hYlWU4 z8gk4JXL1=lUp@(n;BdO-$jl?486)PuY;-fp>->D@oYP7w1;3eW#ltcVEyeg5)jI96#0=XNEBN3Fs7fq{W;+LDxoF|#DQ8Bn|xtFJWw%BWJB z5`A22a_MJYXS+*z@jJ^RUQi~T$15V@_I$-PcT4yc(r5&iQJE~fprkkaRQF=*HM;V6 zA-4D7T4HE`R3#s%Woq^MQgYY!YWC%kk2MT`8E=ZsLS9uiF$&ny5Tn@w2-AMN0w`bQ zUGq>LV9gY(d9}B5npgyxx4A#QfU+CijrPG&)gq(2@7+uHo|_x(4-4z#8~N|uP8Mo7 zU+(mcqFAkSZQpVfnU*apEu7f61Obh@&k?I-%(RlsZn|3A_ZH)4ngL6c(iSIE#5{L| zg6wonzdD&P+#kcD?+pj@u;;iuUsUfNJ-x=p{Mnu8v8hz>MFhJb-R=zuAUUw-$C(ynC51pgo2^<@VT> zw9d=xyW5SLYYMMtN3j@@hzH?)#8aNsto7v%dKJLsJ$f$!L3di>WMTkhEG4 z@84sFsR->aj6E-xYU!M}HxSmbTKLd|K=bEEASG~EGL4JxfCMyC#Lbb^!v#|CXVJbhpj_~Ty||=(zI6G?ogtL+hwY6>Q_(Jh)Gv^^Epjs ziv^)+m10$j5bPRNt|ia0q7J^1l^ZN_nGHS}UJSYy6v%gyKIyBE8A$XCplA+s5ZlZ(IsO!Ax;gI+oE0#s z6OBZHMNIq5v!+sX{Bql-6O8nNe0FV-r_DBSd&GePiiu>ms}o(W)$=c=;#XQk%!=%{ zOHAqqBLAfc+HpXc;_F<)jO9$tGm-sW0;j*Ui=rAi6=A!=?@vU{pTAoJaBWzKoWdk zE&fsf^!m>IL45HmZZ$X@gH4}SE;*&7F+}*peQF%a@|d{%1p~vlc;wP#%s`&hp!Ir( zNweF%W{Iu+aMn&qfAh7nKI-{5-=K96=8Fb!L*LZO$RrbI0}1?*{Pi}vlt?N2*Wchy zG=MV0>LBs+cnlH;Ryc%mU8{dN1J0s+->_aVwjRUo^J?kXAYVKbB%-TB5Z6l&CQ z2#56Hrc1ythE&%DcV2GnplYU6ASrdB#YGLc?f9n{UTk)k0P7iDc{|9Cg{OUwV-D;p z!o$NAj#EGZRT$o4@LMLzboyY>s!5#W!{tI$$g7FPcxK8b>?7K8|MB$|5#<5J(y|Um zXOJ{D4O5u6{DHAzZ<^Stf2}r$>)g%rZM0y>5I^!FGm2HK+TvPkC7QloxPzE~+TqR9 zJ=6IIwq&trW=aFx!)(~`d};A$mSgowna5n>+?!A7R-x`L>^O%qCHjU9j zi>>N>d-CDuW;Lg1f%^bVdiD{}pOAyKM;a+K3oD*u;GNNwgm;2OJiZSQxW2dh{8(q7 zc(`{M2TIlL&wcue&cML%1Mjnz@ZrbGJS{+T$~+I=vJ_LK#iC_D$*LW}gy>>JfsV6|3@p)5Hfji-8#vledtnlSD89_t{h=YzGRKWm;~w`=c>$Pm^DW2)OE( zi~B7t18qotP?eAuD-}id7qW4>clw=n2eI-}G0)Q$LTQo$`O7o`E>}~N_Lpb$&!NPd z?4?T$+}njL`l;27-I|rN_C?AirLYq^`V(DYc)VGrO1&i;6?w~eUnTYTKp6q5Jc1{w zBk5C3NzRxKhzE$-lEsh6IJVNoV~<+Jc8?#KxtSe~L;&{k@Y9RWSGTLDB>JWyD&`B1 zm%e$1ogFETh84@df1voXe&vEYhr6RPAgXlT=I{5mkNg-<$hLt&v@(c_<)QN>Bsl2z zw6A|8ixuJ)wS`9jJ$JdsX$wB%Hys-cV_wG-@?d_uf@QLnn{i4e^}x*H@0l>PG;Kh` zt{wUF4a0Kx$MBuPV#@6MTdTHbO&%^2MITo9o4f+{hnYAv)NcCmI#YEYnZO%~cxeVW zO`wt{(~n}j7D8H^@_s3+CQjr!M1gswpqo^hLkS0 zy5k70?GW3YJOxfaT%~=NYLbX^qp*-ap;FIl1tCVez3(nEKu21a`}r>_HKtk>2(Anc zrykTBwL96G90W=qLf43E3VaYph{G-rdXab~S&aKv(&_m5_1_W`+f?W=s?zXhE6vV{ zZZ&@Vn{E-7u=T(E{mF{eYsB50>}v=1;vLgI7q4hW+nSc{zjIt)!ZodcQUe%3b8s<- zD(Q;bZn;0|$n#X2=P$vKK=nV5s}vDPUF8acyJxHT8PII+gA4E{*>$cqIV!kOjnXLl zRr9rZY>tC4$InZe`QmE+>jj69?dU?LIHj=b1(8W{v>~zIvsXwd+)e(PaspH)oc4vq zHv;1lNJ#2FZnr1Am7Jm|W@;Qm)z{ z^tD}%nRsNzt!Rpd?#%XgcwqV}ELK~&O10jz-RaC+-s?%H1GqyD_bwyzM)!iTwoQoR zcrGbC^2O16LoF$9&Q@Na%t7%uldrbq-NlGPgE_Z`E`tGGTq#xmJT87W?FtjP>&Nn* z^$HQ!L^b~!X#tlXu~>L%S8gqH4!cAV8ySWYT3NSO26Q_n1xbVdqb}dLN>eEFuyrw( z_YI%lP=yyX#DD}JjiN2X8|TDFvR00aUjscdC)qyBwomeO)o3d%Nyvl>%0-C(IN`ZX z1;H4qH&zL{cnZVNpR^{>*7a{Z6d?z97NacOQn^I;2d(gtv?GQG`TUjU{0qbJ36l`w z;bRU*orf&QonZcCYvG^}*grb0+Bi(EJWR$gx{Og) zm)&LkGZ}A1Q2R248#_J!a!=KSpf3F$K%dokv$M^)hOp%YTNbm@JGJe)I0X2~e(?Fy z<*S6$w8tW#XIM;TI*)7=Ygr6O=L**Gm*nbXd})($B#Y#QW_(vQVP0?=4U3hOcZDjf zw%3YzQ-|ZZd!o|Hk((`-C~LQ8#-$&g_3mOQinhbmO@o*el^;73P1gHllhtt;(UuhV z5Zw3F9~cG{jd`Y%#%>sB@R<{RZ40%=6fH$vUlYvK3uJ;_2UEB;<2a$@xjIm>uqZrQ zI6AUwM$>tFQ@=V!;6r3vt+wV3&i9)m9SzOs1hd(`E0N`SnsmKo6z83IwEzB?=v9SM z?);04l@$Y&+h%t>!3EK@&{kGfP%tpr$|dTRWus}_AO^@I2oeU7P$rFwTrLaB<8B=W zxRrsoKeiJ}a3wZPftSo^2$q$tqqo)P3yN`M62@>&PUfMa=S?~Gi&V;>5%HJ8Kpart zGbpJLzx(j$sI+al+!)kgE24LMqT_plNv_q1!gFsBl;C1kJiz`X8`x%JQ?bz~Eo8h$ zS8umZH)d0+nKn@?o%$}rbh>eZxrEkYC82`oVSR`*aQ0x@_WbcQ+4}mxxvRJLcP9~> zo7+LQ{ULt7D#Q7!*rSwUa@|z~S)x*rv>qty4*Px);$gS|iT4TNv;{MNW30$%rCAmP z#n5}hjs+x#B%Iw}pHIW~R^0Q)lBK5KXbx(1W_(blDe{?ItJ>%Vv!#O0n_uXepJb1)(@7JmY}>A_{Huh-QkMkyg~d3Q!juHF0( zkyQOgB!&HtNXk|s+4R4nXJzk~hM7VV@2@FS8HrMxp$4Y1R}eHei)SenAw|;Z=oVbO zJTGowztR$LDga4ecquH#JC~!Pv-`%s6{YK&Rl{&7v;3axvP&Z91X7?7UIBeT?+<*VASgOiY#i_R$oq z5TFc^-MqQp+$(%krHrezJRoeN*kYAEeI<@2oztH0WfbIT-#kogZ3ih!b*qo!E_ij9 zM7G%*UMYk|l3G|^MbulwmSNO61~iDw+$>$1T6=Dcdi0Y;ocaPy<|}gtLU7Xy6o3Q! zB`F-XL7pl0bCrg{b`GMVHV#v$jK+Q`ZU19_u+BluPsr2ESI^eWs%*P9muttEV(WL< z{ao&oDia&ss9mD!<#X>Sgf93&;s;H)*Jr_@gbHmMnP7y_qcJNFxwcrvd|3wMr)4Qi zajer}RFI>FTp!ZmoKeYUz^=I0wJZ&#=a$6?Be}aLi|JysFzz1hjbEMjM$2aR6g|e^ zW~{AY?M?Q|*gGkgK4Ig1eIdYRF)b?0sZHk&{&;I#t{$h1B?6Ex;+fB026?mY<&NRq z_3Uc^@&a$}05;20*Xs$4@lyRy?xgQ{lI)r!w2UXMgv-%P|XoH{hcAG9WT&?E$?(RU?5TLJ>J z--nY_5F@g(Ethu+J#wjOZng*RzmH|a0e<-lqZn5QMSDOnb91=ZIdXI;v^1vU@{fBu zOhkRaS=fCI6%GnPqaJGCk?d*N42I0Z(`@#S{q7W5a@b86u-mcas?|VC#R?Sl5=-c zj^+7u?(f7N{*mCIWD1!8=9X%BTHy$q`>8+hjiyn$k;V0o+QR{Wg8dkQpDiFF2Nb5W zC-AuAwLV(1_k`@z=Ft;m%4W{WwKj*(nP!;He%~5OB%>K(T+CZRvSU{v&h8Cr%yqZaq#p`ppBP6<7|7b+!+bI1fs-4}_0!#9Suj6;at!%uqrFV>l#9zwZ>>e0IVT&7 zbQa7Nh-@)XxLS7xku4x+ep68<-9f2<&hKuj?!Zp#g?|gsJppcL*$G(U|>Rvn6B7E+kkmp8?d&-}$)l?C} zYd(<^t!f;(2bL>@5Z>}Q@Q}b4gqyavXUq_?EHiY?8b?)&ma?^F&>tn_*5r8|I@;MO zfZ#1c`31{GrYJU!ECY@@sXg9t`ZY+g`%r$L{HQDkHUL5(l_Rrl&I&0ZYaVP~8`@lB3>` zi+ofPu^HPrcGh^PqI6K&LP_c-4DMjQzkUUvlWKorx6Z&F&y>Rx=KySd94tB11rg#G zKgEloI+e)H+8Z zimc~`+}jWBQ)-l;^e6W!2{CwtVj>Y+T5T?(GM4?USVJZwL{^+DQ6y~jnjVTsK5J{L zilt9?hwB^JP|+grz2f8 z`l3_iC8O3A7Ju_i0(2)Skzv6Zp^XSHR~~+D`KEWZ*S&F#8P4E#=Y|}e$gU?7Iu`#c zhqVd2V<5rnCv5)UM9qVirsf!kZL^3JOVcJ5l@7JZGTe`)Qt8g-J6?&&gYqycoQ3>njqr8SuN}ce`on~umk6_BHs=ZUOJ5u;cDM+{{({mnynoDeC z?}YZ~GzumEt$haRAf|f1c$de+O{ST+DmP(;d#jj~bBNZ1Fb|=mZMPxQEQCXlme)0HF~7U?L3aZ45|yum$UO#vc%{nMkGlh!BxgEnZ>1hqtf2C-BF(3_Fe@uMp*WrJJ zXN0zIv`JakfF@?D>)`($Rv||)aKXXBC6=r%>5#6`Lp*sP`ezz;CkBAM5*TI$r;2NB zQ% zABY1|@=5*Q1)K{St!~cyR}oBti%BeIYy10wAd%tMM&9D||7aLV-{9cV(oz@Q=ejo) zCm$W{)$MKX{v>c%+UogYkj{8K3%c^hu&Evx=D&83Y#)EC7xE$dF9BzNB(8;)q$C1p zKMJq4STqgh82yjtPm$=mEkgKAM>3lgNEU;Y!0XvstGeTOvJ}|te3@lBT}W!L`HwN* z*4lfDFk%Dw?F7qGDbxPMZ2Zy9%}vrgZ=ZS-><8*++J6bE1TRRqoWAwIurOgzs&=g2 zM!!LCaBc)7cip&M^)&MD{e(d9pM??!=~c;ic*f)Zm?Dy7s&CY(he^dydc`Uft8zLdYL2#-k{a&~q` z9J6Z=FkAbf#~~XFwF4}a4L}alyLInn!jF8^VHGM zkDT{`k?$c6a2nN~z}A&5f|NH9g4pNJ==I&In0m z(n5Ae(}_Ud;qC3c2huD@#aT8vfrEzK848q-ean6El)L%E!YsyRkC~?AzFYk2+S)rF09%WQ&-#{ch#{SgPGQzyvhl z-9Xt`kNwJq9Z%`Y!(t|?(Vw?h&rZ#25C4@;t7EzsnUG`Dd|vMHTF+Rg;!9zGPD!1x zH2mRH_A`dbzCg5r$J06U&M;1>fWO0=PV-``KRAwtS8%mer+t~b$y};PB3VZK^yavZ zLBHqw(LxP|T2*7V=PTUaoQ;?1bA`Suz0rth3b(6bT+6@mN+qlT&BiOtAEPgt3z(Rg z!ScD3ppS3-9ixGQe68`}$x;LDql80?6Eey5^&SI6D2}77z3F5Au-P?vNB=Yxz~w=r z@k$d($jJ1x#(jEc*rvh$kaA}PFL1fZGxk<#efj7Cxd5%D;`gGASNJIPk`h68A0#u2%8XX&2w8+Edpp-v&H>x8K-js&lD z&e4H)vAyBrw$EkkZkwdqK}c8&QXzbi(n1aydsQ|4 zD-Ze4YZe;Q9ue*ayPi;^_aZ0+Ys5^9%xJcV1U>gKNIB2Mw;;h3tG|DCZ&_PZfaII9 zhuif5Y~u1WGlmr)?{HP;pWYqCX zyD)?W%Z2>+k4yV-UHNCvm zc?7<&m<5JRwQS~bQ50LRFZ=D@dho@znb!$bqoshKTWEzoq|Lz;xYA?9=hd}^n#;M` z<2KXzn`7Pq#zKXt2@E_cXWL`Si~eJg&;!!cMDT(P&#%} zBP}g$W8F?6>>;B4u&j+%#KqW!3bf7#91BB~O|g zX?!60ZVV1p3blC9Qq(3HeW|YAe3pK%_5Ha1{|}`ok&*eLZ}8r0TV!R6O4&f8vyVMU zDY|~J@qbZ@4k6&MVuCUpg43%1Fry(o&4HN$I^1@O;Himk+$Zk-ZLZx&iu12cMk#LF z^9?$N@9o4jX_TTje~UhS>oI3V=Sd_;#bHFo1$;rVYxidF?Ky}5&Iw`h+!-aH!Yit^ z(19Lzb&c<>w~;83)2}IBd5O{!(LyQ;mHrJEj42b50txZ1K;3vN>;XiKp?3GJx~QET z98d~JsRWy85-1hk1<{!^sDikkozYe3LR-bGNIXDCwFMfbBEoR8V|4OF>550r?PDQ? zPb}?a8XP+fc%9ol3edYxtU#l#6u0F5O=KEju2d9~_g8e_eI@&Fw;A5e++n_dcQjuG zlgerD6CWQhl*%kF5SW+8Rrw?K{<23@O}h zXbL{bI9debhn$%GH_c@YN4ANAIb0i|NU`*)SV~&<#n;GDV=`2!<8fn^SE*zJ-XPZ< z{&~0i@f!pak5GH%*()9e>wgS;%#=^K|viFfmtE;$Bh#3a_={z_n6l2RVb zSkRUN*WDx8toTC++9YYncB2Py69-~1krACF7=o5{I3Jm}O=BQWvFhRjTw)GU@>)pXm_Nzfmka2`AWktX=@@&puBUo2u_dW zr|g`4QgL6~9r>c59gkQQ_;ewW!D0@MAV)d*u0c%3B727zPK`G$u8sKT#oEn|PJhy! zvFg~UJT{Y{g2&GC-2o*EiHof(8g>`7O&nGq&v{09#j=#F*)-SVI!)JuTsb@m3d(~5 zY=WHFOc1ZVYW7n(d>GBO2G|AMWVk5Z505` zyqHX`y@fThwXcut08&b0x378SWnuB%ah;`YBi^;t(j-$`z+i)6saTa^+e_mo5((u9 z`xvX`MxYvpD>??bESi1~b>zVwekOYs2)~0=D7$NWWRTUJE$hDwd0h$?M_4Ppbg|h#lGPl!YjF+f9y5D( zDSmylis0f9x|Vp7INsHg`dF{c5&cfSp?#Rfrjapsc&2a~R-?9 zaVSU0X)s=u#)ZbrYc9OC+V5}IpQEzOxktOt)vzeWeT}R-iL(v6- z%D5u!2I7Y?st{V5y-^kq%BUzPUp4{n5OD+QU!}+lk+Z2mIE+y?QQ5f0Wb$1+olZ}8 zFs5NhL~f~FsiN4sl?l7y(!s#h6yvE5c4+0x-&XOogC=-FVFt!qK%?s}WKzx(g=|tp z%~z4IvoX_>7*ezA$jcgvCoZ1(N+k>RM~}209pJ=&DP7kjPzK_O{3(kJqyzT(7KTXD zvxKJf-hN_W5<{Wgj9`o|6-}BdZ@~Y3jUG!N@~fjZLr}t}IZ5vv+ntd1Vl^D4<^R*j zdB;=T|9!k9BOxLyBSJz_G72es?>#d!v&XS3BeFTjI>pH)E8C%yWS%%=udIVEdxeu@ z{XU1TtA6)=|8e{K>-apr&iS6#`}KOh-dBejjvD3?AIZ7^vuf^^m#%{K{=xlYOsMdK z?X#yP_UVEniXAIe1;2RKOi90^12cTVq>|bRz^;oTLB#33>G(l(r)L61qXsb}UbXS*E zS!I0z$y-&IltGYGHB)y&xOM>2DaSWb%om*giK{0)LON88sz8bD>D>VxNh`Fi{U&rcbE#}$K)OQB@Poq%qff4-z>ZrA1Oz<%%}8?+1aFxWPaGWqToJiRr~=_ z2Z)R>K6&4edvP>X-%W~LzVNQWUvrKnU)O!dKY5^y#NFF8*p;S0;VmsF#go+7^T=+v z&svXVx(CyMH^ep3qr$%L*4Jk#mH`34-$$rrT`zRcOJZ@Vd>4M1PkC)xb5yOQ0V0+p zDRFS8&7=&>MY634{yPd|leJ%w;&Zf_r@1GmJa zzLlUJvKpG^CU#N5k>Ey!Em{dCdKu!!#?M*`h}%RD?;=55sBf^!;r=eUTG{M6J;?^% zuV9D@8JtFGFwb;_l=4p!E`)|SMqlF3%i2=Q0)yDdz{r)B)-E+j$Ye%GVp?xUBg*y!EZxDGr)>knMMIbzTy)muR*qVp%8c*yVFc0ZyA-cZrWaf<4uUd6DASn|Jf$?ssh&`34B5 zWL3dSZ@^OyOTA8FZEk6?1TfkBVDVdP<)LD?nWyxUAIQ|Q&ubU!;}p&+NfsPxjRP(OGIiEiZ7Y?CdZj!&uq6~a$rQry?QaZ~0 z8BCLyiYQr7nyA|whvr#SQkchAGGH2AqFm~szhzB=!C?9!cBuG@zIvZCIwdB=_q@Ng zG(PM3xmc(>T=OJ1^u-@T7yDv1>W``GW<2~%V#fVoI&ep#KL)m;_RDRwi=iBQkgavu z-OW4eV^6SQGd~}`-)FRHBf|6-oFT#yQM&N6;F$9+Z(E@f&yY~w4=Zgr)Je(JB(<@A zh~jN~7azmW@>*fl6X~wF08(Zqvk#GY0gT|MaYo~Vuc2U~pp2O6D(Z@Hz4vL`P6L5B#i8Yq zv1SsDi)RoZfR0S46$zW!9foDjCi$;3Wx{6Q$b8FFr>Ge4y8uEwwUpFK%@BF7@~D{I z4^2$Bcb9>BcW(+u%hr1bCOMc5a>A1qfooBBG!ak%RrFsP5@-ZStpe1hT(10A!Crv? zmwoB3Mb9;Lg!>%cLLD;mC*RoEfc<1q!XpqJsRC};Ra53yTKd-5)vCt>i@DZJ5&@z# z=vQ8X367(cWE9M|GR@epKrZl7T7l&AqO$GhXc+m?0AS!e@Wl`;9d1+oB1UUlTz}h{uBu58vjB9Uhvl zSf1fMd6i!K*9tk_{Zk#R#J@ca}GJGf?U03&~Cc}a<(8FOSN#)5(7 zE#`qc$Gs>XylLUFx6n6)Dkv1Rs+&P2$$u{MH&xl&Z7*m5%HGRV+XGUd(tTjDVB(Ab zpH6HJ(8VkEx74w;zv>$AS@F*>fUl>N-F-$x{uBV84kPUe9D+gnzJx?XQB=u#e;Jgq zZ_eF5n$lBOdUjsIiJc?o>R$Yh^>%({Cae4iIl7k}%Om9K-TT0AfJ*4vl9--7N7I7O zE6pDZB@hI6XNo<~3C@0&EAP{hRfIV!)duVC z8eQ0`#zB#?(L0K5@&(#E zvGb*G?s57@k&RU@5MRVgT@jucf|FR`eO3sXf-f|N8gHI)ts(rfw__WF-_Htudw zWP?&Okxd8GODO`Fg-m+S&b=e`*J)F8zm+V!Z zHuSl0dDe~-^FG9nz}pz=q9zfuS&KlVH?NBJm3w-4dobYj(AH*CoFs&4X~#OWny5lea218x?#9HW$3V!#_*d9e1fy!5R?&*^Z`#3=ldDI$g6Y zU^EJ3$@vwi;7CP1m6RJ8`2GkZPPgGDhnth(?cY(sRggruC6YDT{*EVNIq*nb>g;6f zlITT)-`9e`Nm+`Bzi%vFOfYoo;S>lk7h3vN9_5#oF2v>7M#Xw?1O1|)Pw1<}YifE! z82WE)@jeWkwOV7we0wqV&{JCQvl$ zPgg`C?q=NNm0NKTsdy+CX8)+LTGe@?T}bkHPYUp#ynQ{*UUA4%!<_D_KN93-pDLnU zC^mi)#X7C}t(PFR!d;Q<(l;)=1kJ!_2x*aYk$(H1+2OLbLyKA0TPPL%9MF-^f*)Y$p`R#u%((_#@ z#ta&!D)suTnzViJ%Pn&pGWy_46^6Ib<>RRE^o;5yJX$r^kv}ulxUxxng^cb-?058i zDKO1}WeWOU4*BJY?hu6%Gvp;L))86A(czw`T&xL6@KK4Dxrs^9zQo(FU(H#E)TD*2(n?M1}T1FUK-WLq3F zGcz@vzy!80^wfD#>J%9$zk(0I(HS$AYeDZNkKfov7yjYdQhrXYI(hANmr6d2rS_Zi z6Vc0Rj!EHOAH-44Z4`WToYuT0fQS7%CRf{HjqLnYX5l%dOd4V~iaJx!k1^-8FF7BazXXwFum{u~HzQfABam6~k_S zQP=F2=D`QQ*IN4B+1nuGpxC{zw^%4?z>}uU2sC6Aod8F$XE|7dP`}fejuqM|6~alGF;O4$X1Uasi3Lg%F=mGsb~kCE z`CwZM6Sw-|4O|1Yc7BOwe|w---FdAVKF{p)>Gy*{di=Df+WE~7S(}N8 zIrLpFoqX;D={KstK7XLl&L{LZzReanP}q?B4ouVuoqZy{oIUMbhX(>vi#P{pIoLvA zX^lVpiM_vblpPF>Y=FwPI>2=h zVIP2s$@*&j${bYB+pYdM#I597UtD;c%Na*u)>IW1Jhi;;yuNBqTr%?QLg4*#q;90` zhjrYmMMq>K(Q~2l1pzSo8+OX|KBXxf_jW3m@^frwnkXHk69_29UOnJota7viK7Vz! zbnHt^=e6Cmw8y%@(2}%Nf^+VyjHSKt)(K0$DcvX8`Xciz! zl{td<2gPe#RF~*La8`1eh5Rd8Aezp^d>ZCOr{8|q?7iH=oul%g%3)iVJ8X+rTWrT6 z8gn~YC=hp7%vt#VD(;U}#VKX9?#;d}rvW{)r~ro*+KAr4oywsmJ!T$>CwLNUVOTLu z*qJR`GUk-(6DW_iqLc3IHLjK)C&Q<;908BFZxrz$p)*yR%am^otLD*qTl-?V>C5%z zna_FS*A5?fS)((~Y-skBe;Z-*_nl3goLZUN+6Tp`4xTW4pTsi-V}Ch)zERk=lX^rZ zAOMi#_u_sTjFGU>amz)QRE`Y0akYmb81IJ!)9w(-0SK~#$RW;^jX0;k$2#qd72Xx{` z?)PCpji^@|xEyYE-z!&*8bWOM@ia@sg+=(7S)*3N34-A9g>MWv*@Ipj9CnehS93?F zZ9=y7OpIT8HH!t}UZyCwqpn=B3!^UXWfZyb)zX9Jy%KLuCmcJm6pBy0jt=<^Rrdg{ z+}J~*ej=GVa#JF>ils8dJl>-_meAV*NT{EmpA~o_sW}IQox3xq^e&m60qBss>z(qWV|3#mX<;%l!X%;47d)xo}360Za7G}zPuihXj#ZyMlf!aZNOUE zD=iB@=hrvWeTj6_A=T5GVOaAt(BOg_4B;aBzmBuP*&Ia5AAl)u{Q~58pg_ zA^h>p@Z`nX`1C);Z9LX;vij=6TAyNvPOh9$b(eGgeS-aW&$fKf!~-Pw9BSLp)(9jhHyUQKi&O zYs`Z^d>npsc;KLoT^(-%c8F$$t!ltV3!Q`5e=T4eCDfW-2fKQRBPdzr3=HT2OcbG* z#8t2p@%%XufvI>8$Tc^Xk5P4*UW|Zf>yO&EUPo z>2ka78}dGuR#v)V|Kqm+*K@^+l0`hSFJIlNDV%(Mvf(}`_RDlp{2Cume6Ta2G^+NR z#9i4E(O~SrfZ%_9W5X?6vW)y+e&*E0o5w)W|JwdWFZ7xCkE;}v33ynhHD8wM6*GPt zA9uqvlfomhe_Y^tjsTRxz?nYf1RwI;qoSjW$O*!cf?7pHO-&77F6&kJ=FgwL*LEup z6SVT#y5xS}hXSx{jfX#K1i#uXnbrU-34y}>{rpgBMJ5PpV9n{?s|5Hv!m<$D9S4U0 zy6ud3&`Cz80CFD^XEIPk_$9>rNirMYhhsDoBcSk%b%o| cBK6N;wiZlgZOqTaQ{YEYR!yelp~chx0Bw{)8vpt02qZ`#K#<_>?gV#&yF0<%32wpNJ-F-O4#C~sb#RxRynFVX{eJA9 z?U^(8cK7Y->bli6RZn+^%FBu&zsGqG006RtxUd2MKwU%by%63(ewRJr+#nYiQ$ZO) z0H}^ade(=9{qCXvAX@aO8-&-Ac$HgPtIlV+=JxiYA!t=$}OEqnU{ z@GRi-7kTI3b?PzrS%0tWG^y>7;zdSA_B(q&6)r9*X)nG1!qSANXso z8=I{;86N$rX~A|Y%$L=y?xe4O_tUe|>_js1tztB!^^1jP+sU81Ou_d*Mw=e+K(P)+ z0YPk&7CW&HHXUExO1f913t^MaH5Eq`0u!UEZb8D{@AZCZe>yq@oxu$)8NMAx`@GCG ze>%qyP4W~;@*Mvh_TDE(gTTe&Ezq!2Jgd!goHbur}v<5x?c{w_SZ~WvRbDf(}v6X38b(b*E{@BtL2>*a-@rz8I+x_ zhvdqKey41-&)&?L%hbJeGl9UPy|+_T@mmTN<|j(g}D)Dh9lA+|MHkqv)6mWEMS zo}uG8NDr!ZU`m?Di-&7!0-;Rq`qaR#+tM=-O4ynAKGc(q3N^l*S2ULpx!}`g9kQOK z`ndjaJVYGOl}<|NPYN9Q`W#6$C^Sg1{tDJ?&Diy10|bOba&%{&>`OO)72>r=J<_+> z8vi;_rJ{;xRyAne+R5w^4f{>$<1vEAimia&dILpVc-qQkmeiaXrndSNZn-awA0^?| z*rOEfb%xn0OaO}*joSB5a1BygqM{R4_X*Ltb1jcXQ79bkJu1kG30Ie|t4HJfdhEaN z;xEdT_S9Y1kL`D_gZtw9H_3EC3n@z*>={nLIsiLnot^vEQ-xjB3D4pxf4$V<5WvWk_&9n;v{HqVFu1?@B`ON_dQ5( zhqtKcN#q~Wu|KH}!2yz&aOjM2za>W3qsz*A{7G0=z;o{e%x7-R{eREw^a_*2hx8=D zb(q5dA?i8VJO*>FRuApa^I3d+<4O{;UcEU=H~^^;kEmD9TRWmK=MP4ayigB=()QaW zTMM~6&fn)t&-3^C#H%RlO(3hFs|iM(9D)Nt{^mJ+RTjOXz<86XVpYq{e_FmIG#aaX@Qj)|Lpz|{Chy) z8Pkw?-q;%YH%fvRtO+~wukKiM{_@CN)YN9st)t#9sLvgQ&k z{pCml6B?eUPFY5$l38cTrz&AK9Qs|e^AVqV>ez$Tv&MF=>_4Rm z9$(uW9fy4yxYMkghTcmwZS-7{z*3&BY;4!ZrQdm6NNSWRV=!N#D?&mv@;AK4BNw@Ko?GJDsL|d+ zhj^rw_6Y&XxAn0E)ntu$gp2|jI2Ap}5MdNC-jXzo*b$+6f1A~Mtl9aF)1P^o)p#K* zO4P*5Gi@tr7;UcV12%EgzRE|qbum#b35AeRJ*c>$-f#->upz_?P+;EXQ7Sfhs!1T3 zk&pCmzWSODrK_~OX)l5-YU)E*^~Et>(^#f4T~G13hMJ#m4OTRxkLQ~`!CN4D9Zi(O zz_*bv*z$ao6lBEA7c1XQCX&@n!=Z%X&zf76cNSVl?PNMfuCqGo4JHG740nJH2a&k0 z?#{u0j|A&$7ouIW-Ft<2 zoyK*=6w^8mM^slmuMZ}FRU2qqSh(AgPMVE&=wmf5&1tPU?R^fPw{D&rkGU+{*xA_` z(1a6Mf7p-vFGb14Zq={LC9zxGNAY>9n)N1ha@LHyl<{7)8@@c`z~^DCJPTFozQ8xF zX9;jI<4h+EMOyn{>yZ}p9-2oHBu#g$#QM0Wn0~Q(ob-?*2&Or_avlBNF|&6kq5ONU zq^fgMnVfx{iO1d{OQt_2+7+N^-(b8F-aTl8Scew$gTL=HYfpSmnU^c$V$DqU_N)j3 zbLZ71V5UE(y1L73-cC0@g2U2Zf+|*(*4fx4j2WPo&21}f^gh9<1=D0DADr&c>NdZw z92?D_Cvj1yhZY3I;xo+vB=28^-?7P#= zSDCOLRXm}_3m6|$w(XhV73wFsioy_|9*BxoPpYRc}UL9$7UbwKX^JhU9?~cg;6HB2J#}& zNLQ~M=Omqh(#NXmeGH;aGV>p8K?eoP7iql%foh?)mOtFQ`P7YfIK*cvvhspgRA_O-H&A#h90YFbiOAUwC4d}M-ABs-TgOZ1# z%tr9Un(*Uvpb}SnP94g#m_J|!L(^bRKVzMhKE2p(FL8I5g}^#50St!QTfuqnDoLM> zPbS=DHN}#f*B#W3CwHA&A{g|GN=r|YigC!MT2UyxEo_IB0Kh;vRMRqd^)IwT?A%ym zd%2aq;WmS3?D2KZk^yi|cimm;eI}>+VHVmq@aYXS?KAL@Y=yZ6*e6ELajC%eM;kGW z#1rz%zg@k^-JEX;>*e;$HR|*fKnWPW@{Qw~BvoLI-A=&(*%+Udk*KK~S(6`#D&2jn zK{PY4fn=={4ag~kDOt%)VPss1us~Bo2#_=XzR97N@puVfVr(Qv+jiqdB% z5}a>cQ{7cJPa!ldu91sh>>vS6VC9(GL=nBp4xgElmeC|*LODp>s;cdi?_lz14P^yu zCAIPCXE$YHW(^fr=d%=r@(0Ua?yOo0R0M@ZIcrmzYo_?K8P4>uFe2LGqIUur`^T@e zrvtSM=gk@ps=bjZl7OCNo?0T)_H#1@fhHCu;H*;xR=*rU3cvB5uo^juO?6}w=u3mr zu~||a7Ka5ugzaXTtIF#OPb3i!_up`5+{Q4Git(3OPyul}b6}wzW^1z}q}8RI+v+g6 zBZ=$UgKcWDYt7E@*pYiSvX*1S59z8fBW4lbV^F=7)^0E}zR^-5ke<#;v&A5#;1KWQ zOXBvHXHYL+k3PBf6!m&5r6GxHi3FXcgr2}UgT}LUk8e-ozml{#`@Qh zZg}_xJcRIJnv$}->Ms}vhO?ezbW~JJ&-{#x)qDJdJ9`dD>Wb5eE@2_n)%aJQvV6Xr z`+1$EysIQcG#?0QXg&}T5dqyq-2w#)P`!WA{N>>IT{ColEQ^~m7ZX}7TqmTGu(Ir= zzQx8Q{sKL60cZZ)rB635h8O|DO0jafOriBN1CTAyHNqpg?{Ru z_G)Ead0c|?3A=~z+u%(c6$J8+5!7WnKdNvy6si7*M81{38MY^vz>Jyl;+mX5Cw zW(cXM;0URR-eJ5i;Ns2mi`gg2%l-;_1THDn={6N*=O4?@14M( zHTKjP2yE=RIpG0&!!zU-&Axc~#pB}nKSJCo`BT|XVC&u41eU48pKPB4M%!;n((784 zhRUz{K z7kY(@JhC4c5X2qu+d|LrNx7#&G6pS zXB}5&e|_oQ4wzYvhu4o-ABFMtr~Jdg)(Yk))=Z zHUst)9ewH|thjM;FAMA2^FnYvNkZ;C9ubvPc;8-eIP^>8tDFq7mo<_a0I8~?|_pmvU)AJxEGA!~t06%b|{(LS& z7%}rkXxs5?FEp(&P`g9lu`sDwF-yBDa}o)VsjLlKoy(&F0NbvE!tW4FKwfGt zu=Ob#uGOppm24E)HyDx%qe}=w7;CAaGB*RptP#Fd4kDL zLUWs3`z|S#<0}em6?) zq@R{#dq_!1e|^sZ>b&9H>fwPkE7H`n7eb~te#yam8?N4+MoMgZ!|yynDenLVg}>oY z5$(l=XLIzVlp@v^8Kkt-)L=D9adCv?4`c*4+bk@POj{0@`b8*!fQ++qeFzBjj)0Uq z$14I6spZYMgwbw*9r?_PA?)RPXQ2`&6{yTBm-UIwgwDH$0!pTsON8s|o3c=baB-+q z3a~a=MD3RN`)6j7y=bX%J0a+na6E}QB?+7vBA!#j>tNxQTZhrhkJGR_dqC+HZ*?h zmoSxR%u87eO>7SM!YPPC>uBmkM8$qZK)plV!yE13h~Z=XzFPH?UHzADqDvhCP*abm ziU=vd1oZmy)$8Wcuq662f(RdvFMY7QRPM;7aW499+Ar&7nA#|H6yZHN?Nl>jeiU09 z_g_ivYA#3B*OPwNF)%p(O)yed=R(8tD;pLNNcKAM!TX6z3CjTwetQ8g@N_rUK?(dQ zB!D9%w=yy72A%gx^#LWlH)KTeaf}w0y@Ti<`|(>VcG20`tMPqbH#A20l?A?V9jv_@ zhT=FHrIr)occ}dHG&TNoA0*uI_faW5?h8()I5Qh_KNLV|@-k@7euJXBZ0cWGQSvXD z8v!iB@U8@HsCRpYKYqymEnl_v$fT5WuD0RM*?99S=>eSz>6|5>;o&5y%SXpxI9c>W zw8;U!89wgq1451P!?5b$x+cy{L=^7UKW{y|hpNT`~M zl&n6eTaU@@Et(;jW%hpi^ILSl%9h_uDg0QQLgtpi{Hbnv&Dq_8cH6SxiM7c2)Oj|d%#fqIt zBpdjnsx+nk0TZ0?^>L&@c`!^4+;K=ddYbQ(uR^NX6QcC z@NKjr))Xg~yO@K#ozYz=0i_^K8LpEliq#A3JqNehV1K@S2l(QU+B47aDrqtqk4G*0? zysrWTe)UdI5>NXh$pN14qnRwA4%Dmf&TgO>@mjvYX?dd!Vc*Nq-MVX`;oh;OB3FPK z9A-!`-K0Ck+7UdJAFr*-tD2e`BG;saB&J&KMaFRiwB~JE!$O)AHYTpSqTZ`&KX24^ z3nV!3uJV0FL!0UK!XHqLXW9CE{qv7D2sHT#AY|OxIqvVDKig|u(PW}}yD2-Vs^_4- zTbfhnMxw$I5S{IGo+}9ECcizrm4y;mK3)>)e;jSmlHHr%++~$H=`XW`7Zu$&nXMeq za%Gl728{Z@Ha9JFyY205(nFtk_1u20P-9-$s10bpvVR*D8hG?^!tyfpNPTTI^SvW) zt+?tx7Nk2(I_)Jp<=$s=8Aa&c<9a-wuK&1d%-Q${wxz7>9bl?|acaZoFb+LD{EX7v z!V+S!(DYhAXfX>}CMaqJd7f;#(55te@Ie5AsBMDiChlc#{GVOHPV^0D8B8m3lX^R? z)tDdg9Vv|W8qDV!de+eCVkt&`EgQ(n?(sF|vYNiVroNCjjPWi~l>I!ZW3>%zCY(Q! zXJ*!a_HexE$fClvv$uFT;SoadK!pMvlhS$AnB`Gpj*(VIPONmTlEZ1p3!TT6&h1b&1V=H<&+_e zS&4hR2O|K)b=}Bvn2YX!-*b|1bY*8kmfXCrg6*(FfzJ~Ihx3Z=& zHy{FQx#X_wfWb!<-__&TQm>)ZUPXA*7)v4(oAJvB4NXxwIWW5hN5r#ZTaRe5qFkdU zt4~rwexFS14}OdESp{YhWK=VY-0j}L<;rFga@6r?l?vQ;EmT_7S=hGczi46v-`-ZH znI0?^&thX^fkRVXXA#r3kdRU3E7?JQGo)vluVjMhpzY@wJYB2Y z-{A0{>thm_n%gyv?;j^FN=Y6x)R?S12W@zpeB?flXBrE3l=H=rdgx$XhNC*HeA=;l zaZo?zbuZcTKNB}T>%anItcmyNt9?&3ZQzQqcp^DGs+{mXA+YV!4RUn~uODRx-!{g1 z7<5;8QPNPNS2_^4->;R@CE0T}IG}Z4DN^fbeMBnVV`dh(N_qNtq)gA{@aFG1&+O8k z!|ZauI=0emFl9b#l-LwdWRx@ngA=GA({~$#iusTj<|B6vx|FO5Y0WJY|9D0(EcHqR z5P~+?Jbq>4UbGp%xSY?y%i^-6w`tMdw`XBL;M;!hmelfod>_xEJXu zN3n+Q_sp@%72XXEMDwq4xu0t(*~^m3DCrCvJ?_Poo^-T!#iyX}Fl~x+c^EvEM~`%q z{}~VBm2}Ngl{C1UBwUiyt)Ckez3^D64SfbJoLpwA`VkIdF(jXrBl+1x_SR8Lty}HB zB0t8;6r^1A@enaOY2C!8x*lFjZ5G#hCgM^WNX7|4zwGgjb2*v5$$P6T3w(kR^iIzd zHbBGPymL)$l^(|9YiOt;jg%r9TT$nC++*hjg%Tq8dD8QS_6EdR;x0k~!q+z}zS=)7 zGIGNpHH7OY+@b~+k}|_^h=#;6f_I35pLU||R*4v66eGX736Rp=eF@4m5b%!h^}YH! z4Ub$?)yNJuF-EvddyvXf@^7+ii1N*gDLg>yReF=w1k9)a6az1W|=O3$2LFoyRq?f zPAZxcsO$?oL9PQk5;Bvngaj$scy1W2)lEX`gEhi7HACX^q7Ws;=}v=MbsEgLKI@;k ziHR{(B}a%{VKp_YYD9aEKVzOg-8AUNk;~~o`|gh`PHsdJTAepE2qQ>Jm#G!!!A#(U z4mI(jO;_C>P#t#Rw-BUw1k(}BG?JpBw_J7=!g4Fzu45Q z!3JJlzK4tJGpJ6HPAn^vHdkl$mt|(2MnnI+SKFXzV=0c&k7G*9gEH+&G;YO(FZikk z5x%f2XOr0|@@4esFwG!#aq(!Vnwwt=oO>AJVOdE@bqPpEP%tN}oewUYmWIZJ;Y%vc zQBbcpy>7wY&S!CnaBS3BH&rI{sfj&);obmr{unPCuN5v?G3hTE%7h5;uF(WowlQc` zZ`YHon^}U1ddznRnBZ5>jPJ@MyrcP0JZp^`b{@G4*R?jcobN%J;`EA|%Y!Dh!_-t& z9O-<&I`yi2N7+bjJ+98YWUcuUzK;&m@3S>=KXe>?$&psOuMLR*f)ebdDtObL+UD|J zQ1+dOu3$9%4GCIY;=IqIj^7z@DOF^XUA6F&EKXVeJhV&i3(hsPFT2e&GoO(nh0^;J z1+DL!Dk{=i!s7W}_x%RdUufWE=3m<#u~zenbTMAWR)+D}Rg0`qgK^m_kDq z4w3OfSz^LzGK~p(pyW42GZq}ofg5Yh4=Ca2N7tgpH4D;uHH$yJK8MQWbugv)6Z(*` zG!gUrH#Lb1p(peil$Ms@VB@s9J!N(oX=o(J48>zrDipJ%7J`TxYZ{YMSl(h1lmX!7 z(OiZj;a8vD=wp~QPBC5N-U?~}`hS$t(_PgcOpT3242k{OZPx#ony~&T!eE+RvlgH& zrn?!{#Is7MR6)bWh6ax3$N$8d_k`N7jp4X{)!@Sy|Co6GOq7tUqJ^b=~=@e$RJ!%<@H zK+%HeViug=nTfZux~fjmZK3)3U*76zUA~u2e;ZW2CP72TSX*@1uvh3G$o&f!5mEBm zIh1LM#cdvf0Fo20Bq67sT-TBk)u8FfK2c+R`yY{L zNlB3rvdVNZ`Gg+Tjuvdk1qY4Cbr=8sJT*K7F@xOh{-C4&po3RTn1@Ywv{1y6#IJ8H zrvz;NEG0T}ybim9r}ruLerK4M+>ZuB3^0PO2NEQO^m-%(y->*?3bUUA2oWv^o={?v z)uhQXwBnwgXU>pPYGj#3DIsh^ERj!ZrkH_y^Rm8**=GRZSo*x>h+U)_*F)@|kqd#; zF=?QAdPxddZ5}VbeO=!>r1mn;V#ZlVg%N})-H%D`RSqpI0Zis1o$XnL*sS<@N8M@* zvReWn-I^ZTkrblrjE*RMyA{Gjq%nqFrH2uW)|FO_+i@u?H;qZ=DwUR@hGRr3059^v zKujR6o|AS`WVASn8tCORZ{N;k+|{N@sf2GJj~7i59!|16CV8e83W)tEozX~o;L}LZ zN8ZQZY-hjf=Oy>6Y0!#6V+wdU%iRx)#!B znvZ9ccM3F-eA_F9zM!{OXCE|rL2OiodW}&}^Vid6F@LZ7@ZNkA&MLXC7oWSbJFTYP zr;Qt)a`ji#9G{fzB96gIk^Y;Gpw^)9ZJ+-3FYM%on889rf|^@l$!kk_S#AQ}+N)fW z{QFMeGI9vVqShQt_C0bI6n=yV-TXhtO9i3{@?U4oRgsw0u}e3((T_CH&70rK?Q2wH zSSJ|LI>;M9yx@*Cp%9arDdDy*+zPCVvV_X?84jPuU!WkSsUT1y(rvF2YjBi-cZAj+ zhrFPus*3SMv^L_0v(V>lg>(mQOM`dmH;)p-A5(9~;o&NwyKSNXg?V$$avmpVP;qE{ zKxTuc5$&JulU}@3D!yvk@vPdc%4#LugwCzjy!hE8m8*uIb!Sr1^Z4M;DxDi3mq^ZE z%J?0okK$G$UdAuQYcYKzXLWH77bPCGGw@d8`2Yk!Ny*u(;!OElEfGKQU@$i=T7-Kv zcD~HDs3GXq{Y%x+`gF$y{LT-~CBM<2ZISm%uT4x?VwQNl@Q;gT#R(Q(S__eNXU<)M zO%^zwcf01n1P>6nVFjalSgcg=l$S|_u9?sY?`cr4bEY_Q2J^b0Q;FMTKK{*2X?idr z2CA&VYIv4T*M?Ts#(ROIk)v{k4$?dC_#eogPFUo%lajGnFkCVAr^dpHU<%M}nBP|* zOKAJt)BQe%+H4UUEuqUCOLia*6?S*)2_Ljmz%)E&QoM9lyE+*2cB1t=duQtp^Xe9d)5Dfo^fT06VtCfV!oAoAZ*rus24&3J8z3RgOv43sKCfBEE z`@5NsTizse9)#JysV)h1nvn}N>$P1~KY=M{S{PqDQ(T1GECmpagQZ7xG89xqzY8?@fC7Tp|_=ywUky1G$BPI(zx zVZ)J&4r7$=UFV#~mskPT%;X$~M^j7ge=US_11cg#-P}l%@SP07?|%K$k&>d4 zXjOTO$mo)yq6jM)3(XUGezZSPI>ARMKWT|`V- z4Eb_%rz@+gto?Sjr=?^3x%*)=pph)|D&nFQ1py@(x^vSOf+C)~^7wacOyyahY6B4W z_gdv|*xy;@&!Y~B2?@KSLWQw@Xl=P=g`8p{>M2zCEu^yt&#o-DiO^} zalyI7Nqw`V@~j{ARpsvJEa#vGSM78570?APdv#N{y9+GU7do4h59IZhUhv~$0=~}| ziR(2(LS@ns(&g|`y0$EtJv=1LMenxW#leIFS6109bM*owoH9zj^aybS8q`!O7wn~7mt8t)+s?PcI@ z@N-$Yzpx)JBA_+44k3?hi2mSlKXC?&ohXi!ItGTDIkrb%jlB(Ug=FzT2bmoPo4dKz1krS-JFfAd<$D6e z<*%XUtH`nS1FzHH-X6;xzHPV(8*D|~slYs7s%_J%dgjZ?C?^m!C_4@=B%c4qp{B>L zmC~`y*E48rbN9aI!@>rD2W)t-O*|jBSCwDgknirD+cVl;Y8=NKn3Q$RohvrhVcZ99 zA_J=lp6UUho@`4=( zyZtzWwMK$Ti%Y&8jQM&mL^}#uw@v=1qV6sS2Np=UzkKoebIXd~rP?Ytq4x671%*@X z1wY!}&1AK|is@)nh}JN%j+pXJ?Bu{TuT|wkFt>9^&R>sX!cb|5izyX;jkMQ+&_)cUaXl#bU^E_jPPaVrE#2=XZfVHF3L6m- zag13^>zW4*JB89w27;dXabb16bVH~dDpkbr!}dIK$)#06~opB zYiCBYDA9Ga(8HWK;j`L`T{jz%PdhF#bt*2-MbYJ8(#APpe-YKg+SD^eX3F}T#$}7@ zfjUWH<$(G3Pdj&d=*drvRf=J+Gv$^XCU`pW-MSen!4IR9Y8{f?+=mh*WZqjW-yr_f zJKu!ZcM}gxXo@;I-+(${gU8|3=*gLX2|qM+?D0qi;^+w5R;B8$0oTSPh49CCqiM~$ z-=MC>a2&1}gV%hVsQo3XIR`LQ9TmxxX3l@@%y{qc1^l`Hzq6eXPzbsi zbaF5)_ah63Iz`Qm^YE}oTGf2BeQ>aB%mHyo%Ct0H&2+|H>cf@0@JWy?Qc$SdNUdh& z)HA!r_{+zDIfu7V2roYQ;Fe5o{Dpdv%%s{H3>KBhxoIr@M3p%VW{`?NJH|`#rzlwW zBw8ws{b1^_#%JhKnm0p_D8i7=y0U%mPrUxG)Sb*{yids_Ie3gh^Z5@(+TlG`Amu}K zG2EHf5YkthmY?XT%s&zmUzfZgDp>!oPsaPBqOXO!@=oYq?|5cPpc!vu^Q1>E@0;4!?IJK3=0T`(V`nTZZBxg zi}EZo*-(mqY+5)jCk)xTU*o*wE~&&ib|amzZ(;O%7EB%iH)}v;>L8s2%Q0cxIHI6n z{85ho>Y2ESk~>Mft3kx5yz^9uNSm>qWLQS}(C+m%rCN1B+-p(Pl9f*2_@W#-EWrPr zJ!?V;q6F>CJXODRXe~c&mKDMPsWo9YS*H1(VK_wlMDGBZuE{{7tJiQ&U9vvpYWA;F zmyKn46)@Y3ejTV-v^$+^{XYc6>d-V##Up(syUW@6M-Q7Mr5ouNZOAcBwdXBK&1p4SHoCabh` zBUIFJ?o)Hu)?KBq!jh*H=J3w+Oic`c0K}sj+F{A~eR@w(TqD9#dSVzEn^A5?a!$>tW4 z5E@f_vvGkG*&o+pVzdV%!!$Eb?k?scyZ?s<5{+CsZ2s@9)c+F%i?7gs3!{6;q{jFh zG$zFEV+;xQqO(5ykDbJFbc-Lssijo*`;(U`I@=Ww!7kE!rT-C~);G+hMnq5jWU5?1AFWb>|c9Hud! zN>nI8DQvc(4EN9P(&dlk-diol4lCZm@;4i!oL4T zO2pwhN*9y7V6_=9X>Xr;6h6<*ckn6na17^)+akPj;3o^LjLtvded_93UPAju!B}lj z5Qzo=%(SO?NH)?F?*PIPzS|D{nTFQ?3kyqv98>7|KOJb#7ZCfY!qcpd>F`O$C8FZH z7Atv;#V|ssY*`e}S)971xY$C@Jj~5OEVi%ee*&;QC*-HwAR^U!JIu4}=J%)RGC7;1 zU3+m*BwGqej%oiwe1Jnp0Dabq)htP8Bb;tJ36L37(VXW~xLxm{G zRGzpr9s?TDD|Lcn=2iqIGQ>z7!v1TI_h5Iws*zHy7!>**#1A2Wa7}}znD*#_`Vsf@ zfDAUt%xD`iq?lhALb$#JgpMlpLzAHoha3W8LW+TjT5)OGFk<4^6fT`OT6tGq$bfWm z#bO|5KM3i!+^N!T3hwvP z??nIC#Czn=aMROr_n_Q?90VbC6j5_D(swlGGPE~_TmU8pCMH@27Fq@lB?e9|Mm8>H rPHF}QE(V5!f+gSo(ZI^a$lS#3|J@+v-r(Q)6hJ~mR=DE3p5Olhp~_jM literal 16118 zcmZX5WmsHE(dJ z%FZK%Ru$;?3o*a}0IHA%3A3a8A#tcr!J|1YSKUs_Z!7EVJL_vF_#V^U$2A|p1v&;W zV5jvs!KNTJavAvL#bhjS-`@fRz&?b5!AV#|sqdp;V?!X1@xE5vdP=b5a(|g_etCX< zrFNy0AAJV~E6U+Zvzt%i0b9)$1xkPfgJsOF<&owXD}bIBk?@6{m$#n+Hp<#}1J^P_ zL!mE)TmWD^sbd&q?*!a}?>;W1laeB(22~aKj9?P}imalcNF5X9K+>PSx{5I63#!uZ z*1aHorZx6sp-9Uh-C3v~g+3j_gq!|J^Ez>SwLAjYRr~+EtzaAzAr4rP(dt(gG?-pe?J-Na)}P@;=W6^Zi2Rq7IMTBzW>jfKBNHyw`-FD($a;nYyL;4!`% z5jw+g9r8{9%!LrIs@8?3aDwG*7`Xy)9v@eWg+Exn!Ke-%)lAj1I28udb%mGi*=K#g z>fr6dO`w?74qH08a?6A@F`! z;60~sP#3)Vd-rwtWnUy{Fd{$t@1;x7@68{IGef{g9|akmriIt+iIVW1v*mDI(vcvmb`~W9d9m}R*(GGJE(4y zGgJjd= zY$?!e@dss^Z)lECtUhj`4*~tTB_>}^7>@pQ%GDo;Z_Zb|hzb|_~M}QM9`+e7-(co4e zr`qzT)h}cx@ZcV*Eg2iSCS+Wk!Q*N-Ux*LVrmvXw}f~K-)do>DXB` zv)b+08E-%AkZ+eUtgIi+V zV%$=>WO}CHO@NxPV1#xJ2*@<#Oe! zNR4w`%b+EHqC%Zcrpz)W<`J=W9zImN$1xJ@`vm_NQB-pI;G$FY~g zjjO_u=jd)|Xq9T@AYeLc{L6UBxOlqw9?t0A7(a*ipy*QIvEmNX`mjx;^Yf5nm+VO7 zvFh>7%%_2jBdQ(07^Yq&F1a0i0q4fiQ!Mfs_A%Fe&Fe3D;`$ymoTvnh)U^(m&d{GcR96#y{UpKRX zdvA|KkA&oB_XLZX&Emykq{-Du(aHCW7>uQcR=wYPFATLdZEO{6gEz@B?tzQ#CN9-0 zn@@e7((p-T>UNeT!&7wydr3odhVZJ3gV`@8F zF*--=b<=D{lD3dykVTO@=m{^!pKRdw52Hbc1$`p;Rq;BO3OcF7Y>JVEEJlt{wa!O6duYtPwyTw14EuFKlAXy`bLZ6e$K^`@T7{BjPl z@={B!HnWM(@wpNQ$PTb{X=HRWG|zNfZE4Gq^-4RuFuD-Ee@@F_S9|e!@qHDZ$4H}f zZ}gy9$Izy)0|Kd@Y7%R&AEH(HlU_LLX>GOUogR-Lo%Nidovw}@mNb+|brY0W>de1a z6dH)x3ZA#Fj5z7iRMVC$3onx_FoUp_7i-j}B2YuasVtnthwAq~rAAjqzMx_+IRv!O!en!JBVaeD-6$$FJu-t3E4U zJz{;m_)L^VrT-DBqv3Vs}GvwswjM zT0?tVii2&jr^aKCG-L9K6Y$r53$DxkA^I9kG8Zowy|!bs+s)VMdgl4m`84aFYbGtG z&X-q}PMw)2HK%4RJ2s^|4O_=^C-*CR?#pg;tLGi|J9I}Uk*n*gCmn+w?$6`1<(hJW1}_7b3@!*Vba4tcX96(s8cv+wNJO4tj{je}u2~b$Wjs zcNcS2WyLWuVmfO zq2lF!mvP*B6Z#{R;&ggV-iz|C_^Emq?NVuPZ-0U$ex!4~Bf*RHVex_XY$>ngs)UM2 zt2fgW5)|@1G!(3j6CR8V;{e_2y?{2$63GPg*W)8&=qHNI<2>WfNL{{c`Iv$XU~77>XgPw}l!JMo%gV~0q2WrMdhSaj1>_Vu3R2kTyf`bhtSa0U$QUAn2Vx`Vo`440v`C7u3f zYXc)X7fYMBxE2hI$A#7AXO>71GAtnG~H896yQ z=^2>lnV4wbX3*NZS~=*u&|2A({Eg%vJR(N+hIXbl4yM*tgun6X8(2F!@DdaMCiL&; zZ$6D&O#h=~W&giry)BUb_ZxafItKcGale7`{2t{3nYtKRsEe3d8d=%D(coiaW8(R1 z{{Q#pKZ<`qYWxSu$@VAUA20p~$V2~||3B9A_h$Vy`nFqqusrnt?mQo?S&#V^7#Pzh zNfAM1mv_e*P#%E3rGYF5DZ&7Z5C_@fDTsqg2^8cQYC>w+d^Hpl5eUFLQD8Qq6gnei z_6$GqCva+sQ$l2-oMf&i`75 zoJiM-f+GwZT;4*h@$|f|cLwoLxmIIbWhMP=u>y%Gmir&u{dSm8@02j4-Bmo#*56&9 zu4RcuVvE+B%}Sx*^{nG@JIQQJ{NK$U7baW@GqSJ%BH;6+Xx5n!sRkZRE;rc;{2^KE+7L1bffQt93I+zbci%H&VgxEGDj?WZBOV_gr$bOk0{GAL7^4%iykAle z=gMg|CHVRNkia+Q2;P_*L8nm-d8X`qeQ}3{g+;Z(t?t};J8YO?!=2&8SzelICT-ZD z@7#`ur1JNJe@fkYK7@=0P}l3;sCzA?YITsq<(!fnU-rcMsFwnICVO%H$2(gQyr%04j+?ab}z{+rlBG8hh6&1w5a z9OFB8h|xn0Bm%y=WaS1#HS`gSPf~Qae`AFP-XXXb1s5NW4jn$iWpeL z3)8{G4ATU!EpS);hZGRDqS%=A#U(Nfu(C4`1A`8>E7hwFsF)^(dR!K3PS-lK9&V1M z3#60D<>lq6)vE~G&${92tk*gKj$fkFWd+>V?44wrt`3OKW|ZU$_AYRpEv<^J>a1p!Y@aSh=x16S&8gKYaKAH!ouYLpX^_d4tA9bCnb|$EfMwW?U2bz_uE(;I zc`C~C(xi+f@Hl&?PdEDfcze)(yPBtvCpH;`fWy>=uTk*pvr0$QheP1?;5Q^g)t#e# zr*+`94GX5RBz@!Zn$bwoWE`3F{#(W+Pdb@S!N!Jx_vWYJOpb6cur(1e)$k(>$QWf^@zE6~{WsVdX?BqU%d{}iW zemP#orzlD5yR!`z^Ese?c|u^nw8iWRaqs1+h6)ubQHD2vhF#~Bn(`PVwD7A@@Vb2FqqNSY=)DbHUF+x zVZe+U-kNW^rr>DDfz)(7`dlHw^FUn0qx(v@MrmQF&Guxoy)mOj+=K`(FqiIAKm>e}-PnB}(H&bkS zG*^!CTeQR~J6~D?3FOv;8K{`()1@2hJ$6_dqFk(HviLqND-C_5?@QKkle}uEpZ{6{ zwW-_Tp#lH8zB=-FGcC_=8m~BlDDQqs(i?y$9DjNjlD^_+ z9gbux^ZQ|Q3p_MbRFm_~zN=xHN>EP_0?dy2Y8$6)3WIMHE~kNQNvhjAcpDVCd?xVZ z{giOpRHM6wQ|}w>8%t3vgrHs>_hVKCq#4MGA8(2f_x|;f!1VcYg8yna&HCHzd%VdB z{?~K^Lqpolue^d^NyMW7zcAiB*Ym?Qn$g|b>x*$LgbVRne7VTFTvPrYeMJHeNeN*PSom1g_kRo6W{TlzCO^=77f9O^BO3zy?X zR%*q3i7-+|+zL#Y`EKWWp+MNpVC&o$PakuJ?bT8>dTOl(py$O9#b#QF`PEuCjamgV zJgu*2|6CKq=7 z!gT9B;n%~7yFk954l&~^(3o#}bu+C$vkNx@rPDt6E^2!IL}4p>KFs6ueGJ7{GM86X6hZnlBkI^3e!aYv3(1ntVHbYb;S}>L6cid9Cxa2r0O)4kPxms6s>C z0|@jSGnm(1190@%$2=gOc+h%19$y>S#y`5D(81KvP6AjR9F)-P^lInW%yYXt)Blbr z6$qdV|8nT-@_Ot2O2O5{Zncbj%T7s2*;fal;gnCmGIvPSW26xgmC_Rs#kv}8LVp*D z&-=B->6rR3uf1R9ak{^8r(ax7Ga+9q)4b9@F3?@4+0JOO!?U&N)^H%IfJ&(_q=9~` z8)*W5by~5(VuAPxnOt-?(EfmJSgpU&IiNedA(W`C-TgKU33t&TPb?D174+rE*Tp4E zxl-p7W&E99?)yBoE2D+68DX4xP0zPY6twPqZrC3@UZ@Q|6Q;n#n`bs2SJw`@namZ1 zv*icz!Ru#oJInE8VW244`t89;?Yu=*vhSe~0aozQW{~ zaTm?&tv(_hCSio|uKk*@0{sm_Z^4#zJ+Bk75sXaN zI@(=UZJztWF-465O5NHRblNG(<(jPe3qDg&qL<(Op>oe#TPdOwwl*f-0>~;=p@SJs z+F5M?l+M}MSJu3@6@=tiUu{or^$onE|D>LA=I77W#;e!bpKBlG+k_VfT;kmM(55wZN1SSZ`G z1kGQ2fAgs&KIs>)G|dBh-ic$}*eD2;1DvY_rQbvzQBL8Y)Fto!;*e8$_B7S6G%mJk z-VOwM>$C}GS@DYTBbpFx4!wTnyuOazSj;PLs__uJK33t6NxHG5j*ByGQ>6Fl__Ywy z*3M&c5{1TMx1)10bR>DpcSN%3nAsUfoqSfHFqW0SX-$`hQ|neDym1uNfNER!y0PJ- z{-{pk@pibIhDGgG2U7*PpVpxTCpxWGS~lPP=4p&9V{a8%iC zM)zz3kAP6{O{H|I-F-;P`E<2ibWdV!x*xt#T0|f*@QjXmHe0+EqraXKjXePpq zs1BH%te!_4oqNAV#^cWGc2yN`Z)an6s82(u{+$|~;!n z(o{}j!Pk>ZOImGZMxSxd*B2Fm`ef=I9?fP{0>0InFuSTeEP-&C80|*+M)~RnP1s4I z>}r_b6sM9iDRpAZ5~zt2I7YAIiP1^gi3{HZ`*nO@vcR*wZ-=OnK(QHyrdR+UspZvG zcf*)%O(-u3Cg{1Xs>@7y$}JAYUI-ITQqm>J+i%z$ zzE~)&lp%S#??CyrwO4?P-^Y40OhJHUE``*cmzyg>A*#i$UKWNy zOO5fpi{Kan15hVePMDdTtOi>Edysn@IlCa{XVaD+!KViuzthJ+9fbZPbPBf2{Qh!J zZOgQ0J;?9jSM3CBI8Oosi69?xYO(_EU213%ZLIqSuxZe2&f+xw5RNsDQYv~_E%KKyz4f>XC z;p*aoC5qOw_2wUpk%w_JRhZ+xy8R4;+p$<`u%s#+$jF-I9_#G^GZLzyH2HNmn-C>G7whGgziu30ZqB!(EDH|_ZAC*wK7>~5qJtPx-h zo(cpka8y3(m!o7L6w-?cs3_Le@~0un4n&+vfIDY91;ot(}qJMHOwgigh6K>0{{kYoWW$}onc zswzXJV%UPm&Xe#c^9&rYT+vEg1dbwMYZO4)j_iJ&XcQ+!Hon8)EMySo6%=t2llMXr zAyNP-{lzC(s#1B_g(>RAM81TXHn$+ezn`t6DfkD=L{1QwW3^Dfr6{1m7IG?b_#r=&^=Ixth7DL(Uljp&K6>6HP(K&Kp+e83)}Cqn0k zTzv+DXVVQX-e)S8R}FXhrk>$q^s5j?ap*t>nn5soExl`jp1}3@Fw;j7ADN3wm~K&p ztx})@U3pTF%}Arshvm&b@QPPuu6SVyV{xr|kt@R!7@ic+_9;?(iXG^5Jc3jj^r{24 z&t0y3S<|ffIoA%o{_^A6BC*BQ>)iZ+H$2a zdmNiPrOyJwB_fa0G|4Vq%!)Bt3io9@;j7rYDS9qzNs6hlMr=|zyvp!nY3T62gP0J@ zSeoM!R2nt;4>dh-$h<~ZRgB(H!ogT!!71fXCpdukQB^v|tIsn!SI3+r8jDgmNf4un zEHt1y#yUt}?z|-yF{8slo^p|(f9;%T)_W$BE{Fi1GNRg0h)Fe2`uh)ns+j&yI6r+_ zWku_Xq;p$~i*qi`wp;kX)$nWs$O};Gp;58Y*fu8KQ~uqq^jr((la~}_j=C?egJ>1J zoNe#2V6X25=R?u9E5$1&NHNlwO;;nyOWGM`2LYzHpJIwWm_9V|CzIf)ZGeMTl?vqm zDB;{c7oNX;Fvl?ulI@|XVZ3!l?n~f9ZpGrmaLrN+A9MFr{BSIV4)7kX51vH-^i1{Ug1raFF+3Lyav5K}k5*T>-Yt;Ndhu{Q9+`YnJiG)NHMw7?zT*f08LHor zDJXk1Ebq|Q(=sxXJpu9vwnkIWh)J>GEi0HYD~fiXMoYjIr5;g?`HRnxw0Y;nz?_KW z9gU?iPWa|kX^SmhA(5VO)(or@c=uUrY!i;FK|Qd4szAVBtP+gBX~%=8iLn~p@GOOc zek>o$sz(}JSi1_e*%ys2jP)qKQ#O=&IS zn=vs+hB0Iy7zU`l@3{1!)%0cwP$g)i^ty0+wv~G13P{|d=spRX-FUEh=ES(ohEH63 zR6v;0gx*P)Uulk((YeBHe4V5>8?o&(1W)~B9JTC^j z#CJ0V57INH-Y{|KT{(SLb1_(QZDEaoKoRQjpEVzh=3pBR1dL%Xe=vMbUhqT2*7@)t z`LhQ1XBl4UVYL*-j{htK$p;qNCh`a5;QG?cpe2#mHo{n%a%0x>^PZQ)?Vf~7|5@ZamW7e|VxX9p=ff3BD}x>lP+clVJ9kWoF9Gvew_z(<$#CI^L`uyI&J`B z+kDk9J9o&!g}w@R2l`fjBpQy7@S4EmK({Q(P{r*$3WlVmC*zdAsEvybBLTp#IjL!H zF_85q2K03FnP(3%KJ@O2f%3v&3<>eiJEUWnCD$C@4Q{_%xK&mxTf06|C3Otjc!vB) zd^*)3gN{f*o3@^cz$vcqp3N2|ziNtlWDd*SRxnKNzHQz+y%c0#cOH*otldfV`1fdB z(>~;hRM}0@>LPxSj5g7x8X2kx79~12`b90oIyy+s)h30e+5FF37p|<@r$0H$5O`G@ zibJ$=OawLOZZ*sl?ipFXE_l3u_SmmH&nTAf5vX><4v)yLYrj*5T;wcl|B7E$4z+q9 zg0?u58|D=#(orRqn|>5bz6N5g*-V+O?@(8XdMFeJb+m7Bfoi2*417^80&u*bM-csP zd}sx->jY8-{l&KW2XtU>M!JWY%F0A>d;8!ZG0^ik{VrOr@EMyw!qN?sUIyCvF`0|< zl@WM9Rh#K2V36aU=Zs5yUuK~MXOj2Sap~_uqQ{is{vM1`TAHKYO-%(kL85cGxJu3C zbtasm^J}Lx+WHvx^02D>V6WUFvDq@A0{&dsmh{M=wbl^4X951tzt?%Hs- zuQ!5Ykr&up2lB~L7ea~iV~gtJNztN*ygYilu($slQ6pGe|8|$Jp1PxBQj|P*1h)h=BEe3MO^-`|eEyE=YOD!qpB6 z3EiY^gW1ZPhOjgw0$jrp5#2)Ji8S$_HzHL7M;Q2aWxy|lf9>O^=D#!lpc>u%FxCx` zo(RSVtG*mC4k)|T{LW0S7HIyw@K%QsxFH7%ocPtq$ZD=#V_5zvM{><|k zNBwU&$0^n`FH5^v2k9Ufj3*TQ?uoF>`p*y`wAA$1ge@RO-q=Y6Qx&QGE6r|4{ky<+ zm|=fmXLye21?2Si@ydzrn2Gx3us^+f`Ab-UTX()#d6A#W3^49BF6gu5Yri~DH|K{w zQWv*%^j6ma!BlM)=MK&ys^Z#TAFI(!91DoX(%>Cv1*Ox(+7|p#bm@YKfUfGB3W0rO z{9n;-a08-lscGlz8;9um&N!8v!bhA$5cxTA_hjPjTwn zLIs~L;t~ynE?xUbV+4phEs9`FbO>gwObZ)`wIhFLecHxZyRL0U9s>gr7e{9#M3){| zi)>>{wFgw$aN8yX=NVvvS^?5g|54?rVSd|!+RK%Vnt#}OD{~P-p$s;J8I?%MD;^0N z9t2KCzkDe}QS*K+ifmKbnXldg<8r%F{#Ict(or(}Lu&gfX{&MVhSHnAq5Z;{4~Nn_ zkNp{VT;S_rHftu``Bc*<75Ovm-`dV#3B(L%(n2|SVp?7HGmdxeQu13>cv39tm$dyZ zP~`>dF#>*qrqzf+zgtG(bg{nli_|2Y?yC6X4PHL`s!JA^lLwvB#kR~}Wi=T>dl-+W zbH%ieY-Y;w*lcC`%!p8LQixcs-XbOvujLY;0&e9@5OXm5adZ3tt zy`rvyNAewnTiG7qf(uV5bl7b5rybeB_`VfDrLhKjqVb3UJ+t-ea>CIklDvZlV-l(w zeO4tEXWROUORtB6);fbe&BN(E*;v)nRl{PVk^ZauJyRuM?BM$MO3I{G0+WX;TeguR zyu&)k~ z0GOCX@ZygO$#j+gvSuV#SJ!VwobETovT1C|Ua!yeu{r_*u6>8|x(LaL>hF!m(<>2= z=gTw#-!jf3Z$;QRgqh#|b>S1MSff7Z?%SW?cUpVVh=sry34HniH?_cd4CW;!<6}dkzDGiQuI!G&s zg?Dl$Q*Oj2DnzDy2u@2&Gpi2R+}()135x#3?QA8>?ffFhZoOKqflaA%lR&R7_jbEC zJ(!XQ(CnWAP-~JKtUk$&rLijl<|~0yS*%AmITD#%^|HN7HAb8(?KpDQ?W~_7onM~F z+^%O8uBN2vf81ZT?r-+-3YFk8fBA|H71a|gKh@>CW%?sKS(K+2k0G0){pDfFVY62w zylK%*qOsjggEX7l_Uicu*+kLbmBpBM5X8g=iKjD`Ee_`xEA5zqjEuGbJT!TBtJNYU zdw$~p=N;?HYzq&0phhTtki($c(yb=7rsKu9QDvKjqNy_eGON@ z%S%+H6O}AXX})4&`YWq$sh3TeHfM6C_lt%KBOQp4UpAHL>s;m9xBi|dd36e{Mz0`{ z+>^~1_bI%}R@eFcUO1prALHC+tT&XzQG4`QU&Ki$N?ndAQW5)e_Vli#Vm-Y}a1Jw#iejSgx6!o8KX* zZfj{h=zP9OP-3~nr<@~%R!xo5Gi5Z)QrC1cuj@<&_eryW5;17B9u?Q4i$SMIuDlny z<+qnMZ6B=XHd#b5(=>J(AlVD(v(@pq}>h`Qw8{W zMMpD*s9t^hn>$(#=Tni&`7&=+RHgGCQ5{#_gXj^3tJM~7N@_MDl>?jYba6t@t%0u( zEx{|f-L?Mvhx3Mk*16H_qWmhc9*LYu8YLU8QJ0Ae#@jUS*0uRJNY^7?Iq(O!Hi2-jFpXisn zt(Ypxxl%PHl?0T+j9V-e6eGqp)D7eWH5w!WG3@>xmUrqdweb-I{35B=TuJ>A_gyD5 ze!rBh=-_@Ib(aS8ayw2=S*dL95xZ4PDN{Re{d@quKrywV@J^)yAR!)|m3@gxry%1H zk*ls#M4c$LQ07(}eM57gzF5k`+e78;+qPYJN6?8PZ0N-!KF!4|*KyBlQP}6pne1Z( zCt=8|ok(Q$`og?FUTg*UL<5rDnd@CO(2w?BL!z2&BitLq(T~B#e??Woqf1wN7y&?%f|5`WZu)9+Z8Fw~Zl&4ybMq9Ilvj z27rVOFVQeSE(R_3^f#4PdkGy7R+dXHuH#XV?Dx(Bf2iov1B0e_!`V7jj&Z7sb*A66 zA4}(?o75^BfQETujtQLUX-d64XI}mvzB*ZX1CZ8X6Gee}x7yr7(KejVbaa zxEpecLEj5VNy$Om-cm*~7QjBrH8=OoTy?UQ1Qe!YBrh1L7TaM7(uAKrsQ0EGtrs_O zn`gK(UCW@RDXatxA}=}R!P;3U;g@NKDVpu zq8mHZ6Q}dZ?qj|6t3+xy^{GN$;g9X1ygs3y zVU~fc2i8ZDU6rJZ+cznvnVK}DNDyU%QEvU>s9&<|eO8sL+^?9b*!OF5f#Gh_$;*HlVBP|`G~ zQ7yf@P8gbeJdIYkNq^E*0C%6hK4K5NM%6;K{88;?C*5fJRFYQnhbtY zim8;6(j-#IXQ3wz?-yg4{mibYft>W@^0>lEq*o(WNz`a{Dhi37U1LI zy1W9&1B5G~Re^x+SNr8dJ^b02j$t^d{1hYf5`9V|KBHW$^f?W=PJ z-OFTMjQkMeF=6ladY7mh`O}WPC_1E~f#01(gO(6a31bu1tMEnMmD(sY-zT2!C94(t zK^8Lb&-b@PE$;jpCGf@T@+vgRvdo!?@()unUyKqol7P*=0xf&$i~a#QXEW4^63mAi zp46I!e(l@LK-}StZz`8ez~|+38=JGWO?vp9FCVm>f7=!TRkSYMnG#SA2Rf~yPh8@# ziD*egA*E<_gvzcmKBrxJwlbUIi$P}N#r*XYwXjBs3{4BJYerxn6Zh=;_Q_hYQ)$$8 zB0YckE6*`bmT?i6twzXjqPa+47 z@vW^iiON9(BgvOaz{H)Y0_DvK_L^-v@CDUscwYPTGecWC@MJnjZneNBw!gFjSB|i< zX24-~xS*FlSS>I-3jzAGRv!~i)dul@O;e_XUEVc}2tU%dX#*{?};f z1pOH&+$hiL_!ofH-2eI6@|CKzj5cG-Ud<^j_s0*KDESnn&;NFYr6>7(Q#V)}E=$NQ zIJQpDOx%HkGbE#-xwl{a7puSx#anOXo$!?g)#_?u4U_xd_UwQ3WC$}LT%wG)-d*hc z3-PI2ws5jDHCDB-{QDeF5JQZHAPK}RFD%8Nr)g6U})3ILH(&rLQz1fZy@&j8okE_%) z^MphGNOI4NRF7h#evdWr@^md=wqnIkE|aG;sOS7SmdHYhli2rMmM?{t~i$rRnjb`1BR*;eJ8loJKEX_tvR)8O7*d5 zV)|u;gdZ+aAz^t-+^nQ07Aq~`4VGH6 zv9Uxm1=3n>&)4k0!-wO>k%QZ{c?E~7&Y1>FIBYJ5bnKS}W4QgZjV%DGT@2kPF2V#5 z>yP{%)t8&8*OS&Plf7|0E-#P9T#!!wW?%SJ01QFlpayjy75Fa~lOj|J_9(^C-A>yr zYlrnN3|KgB>I4~A-l)^|Tk_+j##nOsmlVDy8}Q?m*4QuO>3NZx42>hr_IthK`~T}! zPJ`(IPX%NNpcnBOqnw@)yiWNW&hIZiC@Hr&ic+)Z^ND^!Eb<(~08OJ={}>xH-XC8@ zc5^xWka(h&EagxvwDi6qoaF;4LX||g{NHBaw`05dZE&WkDG%f)onS#_qua?TDU@Z= zASR-wlc|Ev5{rdx{tR3K0(nR{KDq=@z2s~NgricfKZ^JP52#Cx)8<&rMxfrP58-Es* z=TXo}He=G&Ah*P?!WS3Ul|$ig$1emX-7xufySU$qhIJCi^3}(^vXCs(Syd!pr3obO zzDmkRm`hdM^N8ZQAJ}sIn>$&@g%A?1R2+zE?>nOb;IKEwLF~xTD3%0dwYGALit=hA zN9fy@C=+WR^*8fYC%-X^gvV7u*&a6U#S=*ya8Ix2RE*iDS=^6>x@-2rO9&X z1ErvBBKOretZ^wHwVo(DI&pJNd9#v<^v4Fv<1=QV+S5tjR>2iC0=2H7RvK9jK^GVkL~TBp@w;)wX`PUOOw->luxpP3@*t2wIBjcETyX9KiQ@@DL(`Vb@Gek2#Uw82#WW443Sip=dL*J{>XH*r;=INtGS4n zGvJq2rq(mCZz%;XEZOR??0?^1PFYogmsq4 zktIdN!xMganLQZKU?w*x;*%09%6dTEDWiGw5tgcwA9rtnNo(H}L(SWt+GrD`(hh71 z|5d9l2o{Kk8$2pDl>t?ew_Ho2j%z_FIm`2SgdG1f*(fJfzHap>r{hlCe;w(ZF#@$; zB1>$yoD96BN9%jZ*P;?44I@ zw1Bn9e8zwNFT(hDhdJ|#Y{g$!(!YFj7sT64nj{VAtlBUCDnW`5Gs;^scC=6LKgIZq dgelqCD_qJNe&8ABJlNYuQdCZ)LP*c={{h^SOQ`?= From 17df6a271b9df82bb174d514ca03b32d78382cb9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolas=20M=C3=A9ric?= Date: Fri, 8 Apr 2022 12:06:28 +0200 Subject: [PATCH 4/6] Delete some TODOs, now done, in the manual --- .../technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy | 3 --- examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy | 3 --- 2 files changed, 6 deletions(-) diff --git a/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy b/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy index 40adac7..72442e0 100755 --- a/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy +++ b/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy @@ -505,9 +505,6 @@ side_by_side_figure*["hyperlinks"::side_by_side_figure,anchor="''fig:Dogfood-IV- caption2="''Exploring an attribute (hyperlinked to the class).''", relative_width2="47", src2="''figures/Dogfood-V-attribute''"]\Navigation via generated hyperlinks.\ -(* TODO: Update the images in fig:Dogfood-IV-jumpInDocCLass side_by_side_figure - to align them. This has to wait that the exploration of an attribute is again possible. - See: https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF/issues/10 *) text\ From these class definitions, \<^isadof> also automatically generated editing diff --git a/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy b/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy index 56646ed..bef34e0 100755 --- a/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy +++ b/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy @@ -1009,9 +1009,6 @@ text\ these types. They are just types declared in HOL, which are ``inhabited'' by special constant symbols carrying strings, for example of the format \<^boxed_theory_text>\@{thm }\. - % TODO: - % Update meta-types implementation explanation to the new implementation - % in repository commit 08c101c5440eee2a087068581952026e88c39f6a When HOL expressions were used to denote values of \<^boxed_theory_text>\doc_class\ instance attributes, this requires additional checks after From e3caad804b35fd9dce9662502605310fcbf8628a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolas=20M=C3=A9ric?= Date: Fri, 8 Apr 2022 12:16:04 +0200 Subject: [PATCH 5/6] Fix {Theorem, Lemma}_default_class theory attributes Fix #11 --- src/ontologies/scholarly_paper/scholarly_paper.thy | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/ontologies/scholarly_paper/scholarly_paper.thy b/src/ontologies/scholarly_paper/scholarly_paper.thy index 90692b2..fc0410c 100755 --- a/src/ontologies/scholarly_paper/scholarly_paper.thy +++ b/src/ontologies/scholarly_paper/scholarly_paper.thy @@ -305,7 +305,7 @@ val _ = {markdown = true, body = true} (fn meta_args => fn thy => let - val ddc = Config.get_global thy Definition_default_class + val ddc = Config.get_global thy Lemma_default_class val use_Lemma_default = SOME(((ddc = "") ? (K "math_content")) ddc) in Onto_Macros.enriched_formal_statement_command @@ -317,7 +317,7 @@ val _ = {markdown = true, body = true} (fn meta_args => fn thy => let - val ddc = Config.get_global thy Definition_default_class + val ddc = Config.get_global thy Theorem_default_class val use_Theorem_default = SOME(((ddc = "") ? (K "math_content")) ddc) in Onto_Macros.enriched_formal_statement_command From 1457c1cb859ef475492a51e228b1873bfdb82111 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolas=20M=C3=A9ric?= Date: Fri, 8 Apr 2022 13:04:50 +0200 Subject: [PATCH 6/6] Fix typo in upd_meta_args rail road in manual --- examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy b/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy index bef34e0..8d530b0 100755 --- a/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy +++ b/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy @@ -331,7 +331,7 @@ is currently only available in the SML API's of the kernel. symbolic evaluation using the simplifier, \nbe\ for \<^emph>\normalization by evaluation\ and \<^emph>\code\ for code generation in SML. \<^item> \upd_meta_args\ : - \<^rail>\ (obj_id ('::' class_id) ((',' attribute ('=' | '+=') HOL_term) * ))\ + \<^rail>\ (obj_id ('::' class_id) ((',' attribute (':=' | '+=') HOL_term) * ))\ \<^item> \annotated_text_element\ : \<^rail>\ ( @@{command "text*"} '[' meta_args ']' '\' formal_text '\'