From 02a45eae36e60b81a77110d74c9f32d032cd2807 Mon Sep 17 00:00:00 2001 From: mrwulf Date: Sat, 11 Jul 2026 20:07:20 +0200 Subject: [PATCH] =?UTF-8?q?S5.4:=20THEOREM=203=20COMPLETE=20=E2=80=94=20ex?= =?UTF-8?q?tractCons=20assembly=20+=20non-vacuity=20witness?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The paper's hardest theorem is fully kernel-checked. extractCons joins the two proven halves: extractConsNode's collision (via consRecBinding, steps 1-2) or the descent extractMTH D₀ (D₁.take n₀) (step 3, S4). - extractCons_correct: acceptance ConsRec n₀ |D₁| C ⊤ (MTH D₀) = some (MTH D₀, MTH D₁) with D₀ ≠ D₁.take n₀ (and |D₀| = n₀ ≤ |D₁|, 0 < n₀) ⇒ IsCollision of THIS function's output. Statement matches paper Thm 3 verbatim (the n₀ = 0 escape is vacuous there: [] is always the real prefix). Compiled on first attempt — the pre-verified skeleton held exactly. - extractCons_nonvacuous (queued requirement honored): on a non-rewrite input the output is provably NOT a collision — choice-proof. Cones: extractCons_correct [propext, Classical.choice, LTLAcc.sha256, Quot.sound] — single hash axiom, no collision-resistance assumed anywhere. 29 certs green. Fable statement-audit passed. LTL untouched (12 leaves, bcd15f9d). Corpus now holds kernel-checked: Lemma 1, Theorem 1, Theorem 2, Theorem 3 (+ whole-tree Lemma 2). Remaining: Prop 1 (S6), fidelity harness (S7), freeze (S8). Co-Authored-By: Claude Fable 5 --- verification/Proofs/AxiomCheck.lean | 4 ++ verification/Proofs/AxiomCheck.olean | Bin 1968 -> 2080 bytes verification/Proofs/Theorem3.lean | 67 +++++++++++++++++++++++++++ verification/Proofs/Theorem3.olean | Bin 0 -> 106440 bytes verification/check.sh | 5 +- 5 files changed, 75 insertions(+), 1 deletion(-) create mode 100644 verification/Proofs/Theorem3.lean create mode 100644 verification/Proofs/Theorem3.olean diff --git a/verification/Proofs/AxiomCheck.lean b/verification/Proofs/AxiomCheck.lean index 3d27b90..b587815 100644 --- a/verification/Proofs/AxiomCheck.lean +++ b/verification/Proofs/AxiomCheck.lean @@ -6,6 +6,7 @@ import Proofs.Descent import Proofs.Consistency import Proofs.Binding3 import Proofs.Refactor +import Proofs.Theorem3 #print axioms LTLAcc.domsep #print axioms LTLAcc.kbelow_pos #print axioms LTLAcc.kbelow_lt @@ -32,3 +33,6 @@ import Proofs.Refactor #print axioms LTLAcc.consRecBinding #print axioms LTLAcc.consRec_base_false_eq #print axioms LTLAcc.consRec_base_true_eq +#print axioms LTLAcc.extractCons +#print axioms LTLAcc.extractCons_correct +#print axioms LTLAcc.extractCons_nonvacuous diff --git a/verification/Proofs/AxiomCheck.olean b/verification/Proofs/AxiomCheck.olean index f2afdfaee821d063eb1aa938bd0c5319ac76ec33..08b26f10d2f1584d624c77da920fff9d95f0b884 100644 GIT binary patch delta 365 zcmdnMzd&F@1mla1k$udQ>zO4vLNZeGi&ArqCof=@uzbMW;6E*afx)z?Y2J>&FXaqC zAi==MAix3<2QuLR$o$3y<#A2^$n4K#z%tp2C64jL%Bv>auVsYbgV1<~F zz&hE8)s1rkl)GVaBda*$gUK^l<+&KxAWDEb4zap%DL}anY?Fo9%s306+zFEd+1x>P zu$goHfazeLe2dMkK7bu!fOClT$HHS;`XI+iFfcJRK*c4XG)NredS(y<2w?OEsBsoh abqkQxTQIOPctE|h0Xr?oumed0$Y1~|I#{3p delta 298 zcmZ1=uz`O<1Y^a<$UbJSZ=4Jez&SaR#eeb!mI%g($(*eATpcV8{?if|7*?=M4q|oV zx&Y;VV41v#)s0hu6(Z{}`6H`1W5HxjHhHcIP%)qmBQ`g#4N&d{*2zt5W}FOc5FHAW z53;#~>|i(N>VS%^V4Lj4?pFT*%5@I0{#bZSOCRJg2?izx0d}ZUpz c + | none => extractMTH D₀ (D₁.take n₀) + +/-- **Theorem 3 (Consistency soundness), explicit form**: if the + consumer's verifier accepts `C` between the pinned head `MTH D₀` + (size `n₀`) and the offered head `MTH D₁`, but `D₀` is not the real + prefix of `D₁`, then `extractCons` outputs a genuine SHA-256 + collision. -/ +theorem extractCons_correct (n₀ : Nat) (C : List Hash) (D₀ D₁ : List Bytes) + (hlen0 : D₀.length = n₀) (hn0 : 0 < n₀) (hle : n₀ ≤ D₁.length) + (hne : D₀ ≠ D₁.take n₀) + (hacc : ConsRec n₀ D₁.length C true (MTH D₀) = some (MTH D₀, MTH D₁)) : + IsCollision (extractCons n₀ C D₀ D₁).1 (extractCons n₀ C D₀ D₁).2 := by + have hbind := consRecBinding (MTH D₀) n₀ D₁.length C true D₁ + (MTH D₀) (MTH D₁) rfl hn0 hle hacc rfl + rw [extractCons] + cases hrec : extractConsNode n₀ D₁.length C true (MTH D₀) D₁ with + | some c => + rw [hrec] at hbind + exact hbind + | none => + rw [hrec] at hbind + -- hbind : MTH D₀ = MTH (D₁.take n₀); descend + have htklen : (D₁.take n₀).length = n₀ := by + rw [List.length_take]; omega + exact extractMTH_correct D₀ (D₁.take n₀) (by omega) hne hbind + +/-- Permanent non-vacuity witness: on a NON-rewrite input (the pinned + list IS the real prefix), the extractor's output is provably NOT a + collision — so the correctness conclusion is false for some inputs + and cannot be discharged by pigeonhole or choice. Uses the honest + n₀ = n base: D₀ = D₁ = [[7]], C = [], where ConsRec accepts and + extractConsNode returns none, so extractCons = extractMTH D₀ D₀ = + the equal leaf pair. -/ +theorem extractCons_nonvacuous : + ¬ IsCollision (extractCons 1 [] [([7] : List UInt8)] [([7] : List UInt8)]).1 + (extractCons 1 [] [([7] : List UInt8)] [([7] : List UInt8)]).2 := by + rw [extractCons] + have hrec : extractConsNode 1 ([([7] : List UInt8)]).length [] true + (MTH [([7] : List UInt8)]) [([7] : List UInt8)] = none := by + rw [extractConsNode]; simp + rw [hrec] + rw [extractMTH] + simp only [List.length_singleton, if_pos (by omega : (1:Nat) ≤ 1)] + intro hcol + exact hcol.1 rfl + +end LTLAcc diff --git a/verification/Proofs/Theorem3.olean b/verification/Proofs/Theorem3.olean new file mode 100644 index 0000000000000000000000000000000000000000..01527c44eb106585533fe5c59839f1340baf5a78 GIT binary patch literal 106440 zcma%kcR-ZK^Zo&cU_U#?s91wF*doywv14r5F=_+_JuGkv8Z1#XYKRq$g=h*{tf&>8`i7SKeXY1 z0VdO=?^4Q|O!41;?x3R0#bkQy4z;9a{J(8Pcr^Yrd7E5a3|_|-3_S@03v5U|SMDuo z^fENXpOXqF>CkU~QnK2Eq0@E?hv>-*IZ{vj zzj=5>Xn4e+dibw{h(42xii0=k$%}>Noa`|8%oWb`d z|JrwJ-%LhBF5SNr$T!YYJkQ2rjh_lGdP>P3#zk6E{nr#06FnkiKy-`9h^T%MkrAUp z28@gxsl_dW_P8p415OMm>-zi~N0>x!e&`|1hyVAp$pG}L(@#q{vC|KFf@K|j z$jk^46MY3BPfER-o#0S@)4n9=`}W&BNBei&I*Ix?j-_|^LJD6JJ9)1o~IWg1F4tug_QFq zY&eWF7SXPmSQ*Y%mq%I+Pb zy83pX+4CRhd&qc_#vyKgpx&^DcG>ZN#yJE3_l17i=_-F17pajGjw=LIh}g&WB*;Gs z95DK$3I~S@ZeWi&zeuUCpTBUZOZ22cJ`1#N;U&#yO?du7I7AQQM9TWmFFYbTY(zwe zqeD%fm%ECWALx@a7q=D5h-fD)Mt`nWwA22@57+-T zVh{T#W&FEY!y-q74bw)^(Vt5a^reE9xOcw5#E$(Pc`f#2qkZA?($%DoRyztTPW;Wg z3;UyfQqG@#*3pAnM8^o5_~qi22Y!Q|jIZ%^#NFqEsfYPZ$~+f64kgeN4Eb2l6_bXQ z*weSw9^nytlhED_1A1Z3^QK-ORCTD3_)sq?$G>A_&UtC@I<8FU+mioa!!q_SuS%oQ zkJ;j({2|}%BX^o8i8tq0`&Q&qaiM%5^rg?=ymjZC^eEvnu-E44(6F3(Vj!OYI;_yg zs{&TUIk>#E`M~}}TKuqsKLd1Hoj&)eS^8(3NS*Ntd3C(JJXKs4pTB5rRPYe<$n1}H z_Fw;`(HV z@+o_ZF1TJq*OLJ~7T{Mde*L~4mx5p>w1K>mS3bZ~K)cU5c8k6WZh=4P)KhojA?CW^*=Q$jTmRl> zjTK$(BsULAn5sfO!B(AYZDydGjMY(+UeWk zdCOR8O}-{Kk5tqtKky}jeo&&x5GNx7=WUEO*JJ9lgI`$0Zu&^dn6x);7qs|0?Y0z9 z{dqQd*@)mG_G zgWfFA{#9G__1br(km#53@-3+1!T5f*WY2V3DDhh+LU<%D0cdBP8a3%X=g3Jv)Jw|vwABV!w>J*@nw0LpXyk-e zA?zm^?S@XrHS_HJD)>|EaJK?a15L3W+)Q4PayP`ZTalCstfPW1#XT-J8kd`z2>9)lbFk%z=;jVkXQWi1#SmD_GPmQ zjIH2Vh(iYOS>K)+&oK}@1$kkzD8EbXDEKvVLDmoUB{s?W;Sau!V?LOy+sU{E0lYlNVzx~HvJ#v*G!=Ag;` zFf&*G!Y_8EqTN(f*?oEL@vj7vOYC9}kTTZIBO{%+KDz&Y(DS6`{`8bRzpWQN4*$_^ z=yY5~ysopv3-0a(JQj3=rEDYe8uT&u8>G&C$17^M*u(m5hrWT6;wFu>+a5{hVoz2s zd*;Wu?^TvLaCb{F6%Xb~iS~y-WuAz=iIDdN-78*s+2Ra(qY z#!v8g;PmT^&$g1fU)k^{8GPnS*%!HY5WhH&NI9RvLm55CI6M8wf}V>VXLhgqBE2j9 z@G7DF<9gP3PA8TVlk~$_lF~+J>|S;!emnaMg5I9n{y25!Ov?|1P4qFxNZFYxK1!MB ziGzF+s3o}B>V(DS3&LUG<}|b$IvrQPtCRHk>YfFhc@ba#{AKze@wb#zelxzq7Bs8J z_zLdKfAGyn`Dr!hq~L*Q=lJz})aDlFuHb&?-v++7H}78Q*jyRbN*p+ENI8E-gbmdF zaAEyQhMs^tLpGT{E3r+SHu^EAqus>$UZn9UM?e(ro(((}_>B+$UdWh9Oy@d zpMT54ToODU@_yjES!hSw!stNoG~`tfaMu>?URX5T6Z10$c--z!UAX4FDGu$!qn!IH zqaSBpr9jWW+b>=E(f#RU=}Po4ex#fi5#i2oO1xY$AaC+get*1R>hL*LS3Ay;4czR5 zcFu+|IzBXTYhk!Yj~Abai9+;Qqq?zZyfpM z?gyOyR4tnKnw}qV&>IB4ZN)oVSqQ~W)(cYB!07PM(Q>20zJ!Xs^g99i-rm`IyCts6 zm%z=bx$F(=)QdyyhzsWvDf7WN`wwGZ(hv9fo^L7t=Z~m(x!s=GpR*rdv@;JjUszXN zlXnjU&ODeo_4_G|q2vMgX*Teco-u3^$6D}A_z@3$;px9-GA9I2MmyvFLFw=RVC)1> z1J1bD{IYj5##rLcoFnC&3keNv8xb~qWXRC)=-dNf=ymQZEM-(&x)#rySikW8^NdRX z+Ue`&lssQCF48aKP0GRP7&eG(Ch3RranSdPdDu|@&RYx>+>xY?Yz%vGj!5<##-d9 z@HZ2DgRTtxhI2u1&$7y2=GD+orrp=`(g!&6>YEMYLztHm57vHCu4zNV)*~S6kZ1YniJ5@@p-heQY}X?5RVk#9G^cL9qvY*;!iqo-Y+$;78T5R zh`scklvqI5k^QxPoOXJZQ}G!+sn+p`+qbR@&ztmEbLsJid@$&>XNQ(1btuzF^yuf< z^fz~V66B=a@Xs8F|Jy-}j?7y@Fu5H5qn+^?`qKqlXBTpY}xHW zh8>Pe>|y_;%uTU}Lt*G~&cjUTd%Jt54pnZnk(Uzp49i->KiIUX&fFkn;s! zd{`r2J#K!$1A+IewyGm@OYCI6krEpal5=0=qYyl=i{LpirHvq3fdX3yx!w- ztV8L*IsWyQZ@NjJ#176=QqEUL{R)Y0VVL8rVG=jWdR0*IiOy*E{)?gC@1s2dXeZyg z1<%^+am$81R`4yX=hIe?TO8VX9_^O#Zzf|S<8Om}68N@$F}Dtr1C%^J|EUAIN48)!!|+Nt}) z#bq)ClS|@er5&J!cWepJ+fwvl71kn=&&IlB1HRz$fpV-_5~l*n6%#4<7wy9%!a_#0h#b~G5*%vW zxGzqIzHcX=EV?bAz%OwNyrYg$+N$o$~f6{u|U-THb*$3^0 zPRCWvEouV(6x=D#^Zf7%C0B>H@Ab9th`cqId}71*LF{&G7lP=N(cn z+qZI-N{34l59V&fjA^V$jZbe%msommUuv;0d7TL)TX09#ib$zMYi! z)=?w-%lk~mc3ADZs1yA*Ev%ocTZdaE6!nYrw4GImuR-EL2xobx{Gw~M8;{BquZ^0~}}nI2#D@=A5Eh+kYsNx7ano_F^f z8toVjcqRD}fc~tY7pmodnzXNwW6xvY<^;5J947CZ-cBEf6yRJh9~@53;M|sRO3#H~ z{(WgY{S|w8CPm76qb!xDg)g5CioM*AcvVwz+FH#&T;SXyoDgEkhETw*6 z)cr|7fAP=#13U)oJ0mP&haK&PPRI34(Ws92Q*ief;2EGF9P+77UcrOVZmO;PT)MIE zFnz!1jdtSJHhqRLX3{_3>!i-4^_ynv{RcyybuTINr~8b(A@kaC4G4*{YI>aclL&nu zy|b#~%3N zMeE0TjvfF#{Z}-;*lF@~hb8`_x{aesV!oAS~R^MRB$G#?!u#*Pd<&Uhq4->s!x zYo>;KIPS3=c*m^=IVLzqrVa(&Ux?6M>uRDEkust>Uibx4R#3Z{S_N-&=+GEAjz2=Vu(w zp0a+c>-UFTFzCa>!$xvUMcxbgV}aM6l+~AGuj}VHRoU3OwXQ!Aa(2)a_uSs)epBRq zFuobUGykfbp|5YIy2@|jOFh0isIRa7m>1sQE96son!dg!p-%b(A2wmp9j=dtov%Ij zj*1ACA#z-Xoi41mvCvb=XKA+&>MYC<1_L)Ip`G zg}0nk>6kvwp7m55=%;J-Rc&-XgCXw&zS9*;H{hO8;>`C21As4U?KgmXOIcs}emuv{ z3O@1gO>r7#b1XT+CUI~+_e_HP++ihrS`UBfNEwM!8roT3=I8%6)gi3p-LrtR|4U8s zt>#``Z$VApB-5y`W%j-QAm!Jllp0G|CgYp<# zQr?<4>%aCnnU0a6VGflNf9?mZ(6?gkiV|n47B4Fd5}yRL8@e6Wh0Rk-<4?ieQ-E_{ z(c}33=k!nPVGSgutwX~i21R3M;jjbGrL&>0M!&Ly_Iq}^Bz=h;-VK$%9LJe)dF$(T z_ycEsu5o9l)sPM2MpU1R>!%|^g%m)>wodIV=jpj@iPE8*O4EN zmn*FMnE^Yk;LCTl*Dbw%#^sXl6%*d=W&JetBTh-+8#LA9uuffYVEdozA+H z2|ZOezi8C0e5fPkWnNg`SN?O}@V@#)%4FxdPnF_#D)jh5E~s(QD%|_L$u7r>@K7Z2 zXIx{UC+UM@+Z&w=O%WE+!#PRHT<`vx&snBI&(&^&Z}dJI6DN9%e#}{DXMgLiZ~H+o zxuhTF4k>dD^H@(C(dWz?-$p8KPZB!(+2NfXXGNd%7mRj8x8t&(suqkt1$U1H&b+y~ z*<&K}#*lff-_apMR53A>IqWE<`nN;hAEle$xVE<3CFx7-$YehriqCuD@p-x(o{d#I z=kb`s_j9~w>jRwi=C6W_E^`dTj{xBGqe5UUSNb7%BKo(2&t5sGBj>r~T@uE{0=_u# zoeHQwj$@$P8_YZbU)ux|k9EXfckbKLf%pCCb~m1t3eJ67Ht>48h6Our9#p*CJ+V)q ze0b%-R$bof0~Ien&^cYkCl`Z(qM!SrAmBxt_pRpGv_roI>q!joPe)97!t)B_e!;5<*VG*SN5 zOc))(&&(SAy!N@TaUVEnM6(ftXsb{|pL1RZLf`fxCI9)e_sYtG>+k1szXdsSEcg>a z*X^$CFPL0nXA0U`r;fyZUQW-)bl{BBo()Bwvv!DlHgN8Do7KE#W1b1_^`Y{g;~(4l z!4;0b#DRMaQtnOqg(w?gr_=u+=({}FRyNPElgsG`^OSYAR!Y|`X6^iod723M+24Hm zo4bZHPbvR?@UJss>4$ZI``0Ded2>9^@W+0G z`{xT!E`~BkMV{v$#LMq!Qc%aenkoNdv2Xk0%I1dLLyA1_`zfC^JKCL zR_tG{-g%y+@5j8FEB~2Ce_YtqS>KPP!+t;T4Q{imrCw(P-%|3NH$SfnsmZaH{(~SF z1KP0ak43p}5}fy`3Bb**O9$~DL-L5aNLh!%qr;d+k|)kQN{61pt_vSFDQo9_qS@3! z*~$8QbXyC@o|k#%4V-!QcKXdD%w4gQdC1RS?)y4ll3}0Y5}Ak4sF3o|oefeHCvnxpcb!AA9MisZ~xt3q5}CcgNrv|GcT6 zHr>dTGoJp?mt`s3sQK1u<%R1_dIm-3)MJHw9O&J4Uk++q^2j9NGW;2Lkx zM-39UG~mp~BbmS6H~M#6Vh3}Flw;y}j^8aunn-`n_*q)3IL$2c`)S{U-4BXFvBw|n z?Bn>lD*vh89JqTH?E&Ats-Na~k0%!G%%du%lUwvWN(9b4vNn9{9BmeVy`kR@KEIj+ z%F{Q&`MG9(?kr$_i&D%L!4vW+zlfi&IQuMp5!}>9;ohKy%Er!M&IuliJoX13T4Y6W zy*|*sVBkBF>TJ~45q?gY{)Jo~drJ2&5ps-A_cHr)Jl~83ZU^mpalur59%Udd8NffT z|J?!3BeCBf_L~BfpEVYr+rm0;#NoB)IyveKCY_D5-ngLZcO^Qq%(54gJ@aE{x>LRBm1;}!&*<90K7!(rWzH1rz-zPZnqA`~Z@STMFbj?w=)o7p{*x>#slLTW*?Nfw2(zbjW9e&i=x!_Ww1GVHhwy zj(#7hcwN}^7}QxG?a9kIX}$Ao=PO6hS-1kN}n6#gJYkE0iG zJ81vUN3Li7iv9%nmjV2<5lcJi`xI}CgQ=aezfQj?Pv&#hlMNqK6+7gT`>8<4+d#Rm zvPEzIi}|Uz)%p<&d*i|1Vg1SNoZAvV<_anI(1XIF+Z*rjHl;4152n=Kub|6E^Z^>~lzCi3pS!0BI9n?AkhpWuPOxi62MzICL&-q`6s_`I#Bukya& zRp&s=yNzEZ#=I&%@z9eDnsl^J0AnEWVc(>*HA)MN#D(pqj>`XoH|yljoc85M!uBRT zLtdjN0D3~|&;MucfEG)shrW_>EQjMx#5^|z}?eP#v*G2SwOAzF!Khve$AYH#7@EFiNcRb$Wxr4-;dkj*J-{^N#jNqqp+)|*&lsTo7 zy~YdYzLPmaN*j&&(UO`Z-h5tV3RM11?0w-v(AwHf(2v;%?VK0aANlh*NXElG066DG z?5+;Z_X)%w_Df2?hK1N@hUjtH5eIz2=_BV(TaI=NShR9_62*K zbvXul-)l9l!Sklq`qJJcv@`#+-FQ8_jy$gNS!k zem@K^_*kFsK4|B8%88Lbo#K2I{Qq08@Eeq-~cxPM%$62H3<9LuVk3z!+ zhK$7P$D$`2@?PCkT-GE+4f)A0+977(W`DGEfAeTi-FY-c;t~v;*unD( zQWh1tzi|4dzYGTd`208#`g`F&F`}*XYt7*DjvB0xITXmiHyPgk8 z^t-$AyK$#}m-t?%*v&al${Nuu*LyAOKL~p2oIC!_n3D~^pq;U3C*P;#<8quo@qCH# zE3)Ii;pCP0+9A(*=zqHKE?4B0yf;j{27XXyqRCrDK;-y5%hW^p_r=~{m%D1X7utFL zmyj_x+Ec>=aBk=azU;qFZqKXX8L%q|_&a0X`!k=0CjyTFel^`PH9v5%n>BC5{W%Mb zjickz{Y`;f*tgHuy8<`j^4jxdsXI!GnjhQ;We5F1vLBJW`K6|c}(Bm6J{dH77<)4h+_p10NfN#-1D>v%#O@rMj z!2dgTEF_;6rv%{Xz;BHYt6V_CxxdLKzRlLIpcY5YLsAQz&vDDZhqv zE7~b&#a{T|`wJ$Q*cAYr^Kk$3hErV-G{LRFgD@^f zD$P2f&xbVh8wWn~`~!g;4_!a=e#p$M!Y63@UO*?-ZW({RkHyb# zjT~KNto7|3y~INUH~aKfa@=<&)oWiyFu5G#1Dwx;CRFy_r>`g0T==p^KVM>P7J0r0 z%kLfA>$j*sr{nZWm*9%rHdhMw2%2LhVe zY++c_Bu?zpr;m!qmzAz3?oEHJA?DZX;!qq;H&ByW?U*B^X~9=xC9 z{b?`Y!N6-Jwe;lLF8(l2NSQCjXV#-f+rk{C=y{h2J>`bFwc9dqP&Z)^Jsdkyj=l z)c?%ZFF7_MpAGwBfiK?s^##7aA?INUz&Rfh!Iu)`ww8HBS43YR`0e0p*LJS+ds_w1 zLObJDv2AFaejgW$ys(6*c%+PIIYs|G9ObzVzjNEQvWK?L_(CoawCC`)k$E-T6LrT1 zyiT_RYxQ+H4)r-6xc9jy-STVl?4SDxdt&YS`Z`Ga(;$D_>$?N`{)zJ3Cme8n>!B{6 z1vyK9<^SNr7QX`CD#8*!+V2ZI>eRWG1vNYw@`1qDtnetT?=w8%pAGnndU|z3H|OJfB(Pf!EO7%UvoOz*@xfY{uc$4OYDgQo(-Bl$>dyT1h=ByD^&S? z^OKbPtgV9kp`GVLKiB?iFXyA+LBKiBYR4>3*UwXUz7zw#g#o*6>+_KMd44< z59PU%9emYpFK<%VqIwWNd9IWJ{9F6(c#DRc1}eL~Fpug_8*-_LhVwp?^=9gcB^~v8 z#rt@F=&?=N^p;+)cn-jNbG|`?2)*6}LoOCH@%}qcc|Rxi^FB2Z_~fx~<-J?p&SX`3s_pmRs;?K`Xy-gx*xo!)Ul06&Gk@FIhTqfIgJ9sy-!G>`MgSumQ#1((miI-UVXaX?^eVY)`Bgl0O-cvjBhBZNZXPt;eQt z<$vEYBZBnt=X&f7yldR$l6rpmqdgGo%Jrz)RrK-YdKV17s_!njtBbD(y2mZZdFOIm%I%>o7F|J41_NFXFn=AdMA&Q^I zo&dgUb$;iuj$=iqIQnm*`sH)*v7w*0<60wl zBINiUcZCAGN^ngQ+z#9i_I00e^Md|HC%};M`YS2sq}Y?<*|Bl)rpVR407qA>Lz4 zynTW59P9but&8%*0Ko%+v)+w;_r-kPPzi1W&U5wRC#L6kUnL&)#e=VDtujC8`4o%s zOa}hEqJ26KP({Bt@HF7-y8RvGIGizTG-CGJeWvjxh5z#f=Y~G#KGPDR;<7RQ*ZOtJ z9bPXk8@SmY?HrFoJI<{|I0SbO25y2~(Ggus(jT#hxlGF3H-7uU`N4XzgWva?2z}rB z?7v}2>huroNM%3Rk2M(4#c`Go+&vRG=TYI+7k1EQvC}hB`A0kd8F_I4?G&8zg!7PrL7$H* zxNRBZkcM{pwrJaf-THXM0nY;c;l-He%pb9XxlYQt;rM(@>yZ)fP?dwgvwerNA~ zb9U60n|5I{aC0!)`8k$6-;X&bm|PNAmKC!Wami2%O_~vPe;@9(Ox%*7--% z`}Wi7iF*d{0Qftz+Q>`VxVl)~mEC;bsrA-;e?F^Od^+rN^&YNpBQ}of@bLx#`~Oy7 z)oj#14}ajapLU)~9J-NyK-A%HBIZFbJxMoa1a6q2h7+q8-M``(9~tL3;E64ie)s4S%b0_LCjsaC;v4MomGrusN*wFp;Pubz z>UB4h`mrCl-qf?NzK`%kez5=f_Juj>ek|B}z$xgccK2gf<0MI6VZ%x$gv!b2z zuJ)z={dN2Jc`ok99t^6npE>97AM(tvM*S-;)XyJMfpcA}^zF|pId?@q6FBW}+Pdjv zJ-(jN%6|H};&P>Bv|sXux=6XUj|m$Q+0Xd$GLAL!!TEk|0QBCQpFF(If|G}Vn`6*U z9~XBlG=VzA-UQ&Zx962YwOA7c_W_;)nl)-^A3dIN^cVPw$rm&EUa0s(`$<`=jYTjj zZ0JCTDMmledh0b(#V2E4|Mcf~3ofT0{%B|3e|2GFYu%4v;2hWS8@Cmp&*DccaQgY4 z%i*57pV_cK5quT=u28dxCYL`V^?Dc# zJP|b6)c^Ymn*La<>vrH~izU6HhG%iV1-xrO&32W5OCIp~HYtuiOc9aBZ$u3Z9}sT5 zMmns2Xb40c#PG|R7v7($xQ(ek{gW2sXRH(kxozSY%m0nfd76U27XylRmpJ@i=Qs4{ zOC)#`^7BzC;H!E1dU@V|3C_>UbKLs=G;B6=T<~nj@pJ1pT4p}y zToBwVM)jN2Ska|F6?>QUKyd%ss@)HKO}9?Csn0)tZZinDeO8e^oPQ$E&uvov>@Ve= z-}xzc4CE3((+}5}uID{Jx0wR`SkKh`+I!p1_@x84eD-Mvj;-iVhyU5Y`;Y%%lYU>y z`##2Z=kx=1J-&XUmH(7~_M*#dU7q)SLEyWxY*4g*Uz>q_0LLe~SKbMl{m${@eOZ&E zKVId1m)M^Iy&S)femQzWe@>AOoa48r?AqV;^G}XnHu$pM`MoF4KSe*s&ufhGb5o~+ zvHH0r$B**u!|O!o@_vvD0`fS>8$TfQc5|Ds?Je?7-4KN;^J<0pWNAz=iMfxHj+ZtmUQv9yMJ z0S^FPv}MMFw=|sdmHATs{bPA)r|9?Q{-S}hWB-VtDf&9V&k4mgRQQj(?hWKxEb^)7 zm+Q#&GacU5*Y_mgnV{eNJb#ovpZPvB^-mtwxs|TpXPoMn`X97eI!f2?2|NJQr*p_7 zy&mxW27b<}$c4pw_5BOqZy^5nPrtTeO%(s)pf?FL^}x5+_2-CuzabU)zZ0L%Vf+j| zuf5N-hJ}Q-e3=K%=jEQCDS!Xz6*c)*=0?Zf#IVEci*`OQ_quj^mY!#U!1-R-h*ohq z-q*8HzK+u0`MM=rue@Vqh&c#l?na-2`Fe`{ma z{~s;ZG}iT7#;bPrKYwXjZ(Tq8_XS_wahvz*d6b2I1A#YKRlJ^_2Ugf`1KxdbSaW?{ z;CuVb!=Q*hHr+nHx5#f#{eh65c6>!WUEUY%HqbAvmlx}Gna@+=fiL^1@0WUA z4eF`vqW|Z7)*j5^Kji5D_nBkwywZR0Z8@G9rrYoIKUVegjq$~ky8UU8qyKw0b~~)g zJN<`z9k0m2y1XyiZJ_5mWq+vqpA7x+z+>D4Ch6-A>sT`InO}^K(AO0{4`Tc>s_n0) z$1e+V)L)?DfZn?PfL=Mrf6M3T#dFv{QQwbTd z^7n^Fty_$yu|LN9*^K0cdC5ew$e{PS0B_aOUl$UQ2)0^EM0l z8VA0yGp<_nx}A-AoCN&pr!|V`b(`NK#{N${&i6v^KQmYVqcAHQiKMwNqnl)~q_wSU4{ik-Wd92GPK`s^a z+pf#+>Gsk7OyD1F+ILL1&x&@>FO~mK(sz~A$0rH#@c~};^YeR)V$pcj^YmowF9X2e z(Icgy)LPaDnOib0@!+$9Z)vH$XIYbEp632uxJ2;%*r`DzYnVPyy>Omk2jAxpJyzjRG zANSDbA{PoH9?tvzc;Iedf3-({z7dD}*JR+QPPB^V^9_k7&uw_0eQ3dM=Lc0C^8j*` zk6V8JJ6)dVHkRqi|9?il^P7HN%I{5!!~N6VD>b|8_eX({<2e2G`00lnr&o<9>wU)T zj|w_pEWm(@y&TVY=V3WLa6Ik6+ny`?nLe*Mo*BTux>9|oA zZDV}FcfU-JkF@-D32vn9<@*CacX@IsuzT00qQi)%ISX=}hZQ}|D|G#qnM$7bPa)BH zdg%A(zQB3^Q?%2zO8Wh28uSN(uip9!^K#4&*lz=VP<(QsmeZi#ROZmuS=LxF7H=jQ1zwD`x6(3IZMo`SC|@&(Y%) zLmYY7B=3SR87JwV<4F7eYBlaG?Uy+6Z&Hr&Xa>QcdK}ZyUqHi#d1tr1x)PQKiE!=<$YJfth!Y>TwH1y9IuaslH*8zJA((bAEb1eQ`vOYdmny zx&AYKeQ=(Cf$#bI8-CT-2cEClfbX{^d+YlLU$k?5IUjM-`8#Y9AL>sA-?$^i z0(AL!w5NgIU0)$eum3z>%mRM9WxmpS{pb0j1^C3BMd#}A_noKWLjOyK+)+P*rRJN{ zzCiGW_3rNSO80ux1ajy|NSk?2kY`q{~=%dT;(8LJ|699p!K5a4buI$pgjw8 z^Mipi_55IdTIMT1&lNp)R$t$EzR36$xe_ozk6$3ZhtFSS~!+iwG&44P-T`vKiPr+)a?HD!EJU4It!13!Q1MVPKX4Y*~2^8c?%JwN6? zO!ChcxG(VAKi|5`vopaHcrFL~TmEpUzdn98$Rz{6|H=MT-9E-Y9(>V$fpv8I;(7iB z`7O6g7t-~o<$*Xa6v7pl0>{wGf>f2`}b z01pH`Q|!`YJwKAsuMM~@wo#7fA3SFWME?(}Hr}lFpPZ}zijDd|)BBGHo(B4K&AR-0 zemM1G{MUZ?-7;OjB?0~c@98nTl&(JudVRt7L+qVj^!x~fe}TYfw)cC)GgiqD=Y2f< zn>=LLJzYP~0pcP5?DJ2Yzh{s`9`@ZW_Gq{+pA5M)(5)xqT=n?#93TsL)f&HPztduz z!}V7FTfSEG-3dGM>G7leoS!E+jIc8~@?{L-uVPD^lhj-ai~Pf}1V1p1j-#L+_o9Cr;kq z`O`^ZGwdKHXc7w;gx@ zo~sVe@Lb4vJNyUE{nD?svm*5U9)BN^``!(I+&;#=w8(pZqvAsU`v$dZ&+}oyO~Cy@ zV~0Iypzjx{pYd;&wPb-F|5(T|eyLUdF39-F`2gRqW&erb@7aIl`^s@G*Mia(ZbmA~BI)cT{a^Y^R-=l;VNd_E^m+VyX5_#?{fM-?Zvr5ud>eyhJzD6IkM4gK{7wUYr%lHO`u@a(`H%&C;E~El_4Uc}z4G6Jea`l_Lm%q(k^388 z^s~F}wne&qfsl^}K6~{2Uv>Yvzp;U@)auV0>h^PgL;VdW1Ps^pC+E`tN%&50T|f6X zY2f>!&6NaQKleA(zoO`nDY|}3qVk{im-_YLDP4aS^!kFY{?3P=>FY~8@Ic^i?|FB# z9)IpX*#C%>3ETDl<8$@jZ&BYI^T!4}88mx-tyq2hocb}ow#^qF>iV;&ANVoP=lOL1 z(tuljP;pr7wPT?^{=W1d_=8Gy`|0Z=*Y`k-f77;$eRTcYAJ`yYz1ZwN`uI5IVc)KM zu`PA^c*rG#R%-k>NsmAG2Wh~^@2Z%o$DjL~Ea0BD4QuuIvHxV)zj;opK)rw3@4H0B z=TXx?&9Abb^YcvJFKoJeAmnVIbIV3tdX@e0z$YxX@wi*odv^=klR@2f9_*`+PaynC z13td-(0%%Pn}zm3?1Q@eU3RIy-ddI_zqmj8?QCLoeZA%VUmD_5IrfVsy8VHWXZ<-d z=w>rL{=7e9eth1c@W*<5;vvuYA5NWIOpmXPIOxM$cjxQl=hTn<`K-gqdb<8B$^$RH zqj*JKe;RPhG8Kn`CHgngqV{kB{X?<+lZS z^o_^%A$oj$f%E?A;@mT(^!Nk<_eFl)wx<=+>w^t=AnHt^!RGmTe#Qg0;XZ3_`6GGs z{AB#%;opw|**U)NJ(>1_CbpW~SkK>B#Gm%}xYWlfukW|0-|~}+N1sDKJJ&gVzmZ~`>KWAOS3Qe zo=)~(yVK(aCVwR<oci1O-WjUv4}d)1&#JiKXjeYZmwB0*N6B+uTEYK^Z`JYaN7v^AJPx#1t%Rle zbA}lBlLFlR{G@mC`YR3MPdeK9Jyqe;N>t3J;n~3X{(;w$fz9%3xYsIWFa7y!#E_E( zfQvsV$S2DCfq&k0`_+Okr@q4=;kSXG`hvi}_M4kM3VA!&oc{>F1^m9Cao|5a_w-4= zmqP*JkHdUU1x*3}n)VaNGRMg8$Oque&pwO)UR%UpaR~0UTKUiT6{z0eUQrGA15W>c znEY1HVj3OFX*01n@K?nz2K-l=jZP}@e~4cK_}e}GWnoEgQ;zFZ@k<52Ywe%| zrE&%2Rq@LPe~G^y@8tT)P9#1)YgBwVUk*(8I)dw`;6cE7?h|pWd|7?ni~-JbpRat} z1GtWfd;)Nud)cxgCv*K0+@IqNzR$iKIaz;C!WZY1>A?NGx3^)KL_QhML9>C^>-@*v z3UJWTKc4e?tyO+znwI=~r39(`F$*fj?;Su6Gp;w*gNFe&cGnyj6i4HSD$DH((tQsn<2XCAPbg4~Cus|NY%HXp7H0;W2P?9NG z<3;=_xO>nfCC}&dA5T1z<9i5GAywOuX7f1r`xlZ9T z9+wK^eUo9+YkyBV${JF)!F$S5@sr<69soUKJ!*en`K>_?U&K!v+UaNfiq_8AE_TKP zryoV#ruEnT;Q3lI`1VepH%9k^^7Jz*t9~gRPlH?*=sM{1y7`TbeHT>Ba&=VpqlhkiCH z>J2Km@%^E$e%k+yK3_ZTBm2F2|80f*h|?82{&?y8ouXIliATHchv?@Xi8PN07}v1K z=TkneXI`a3&%}HSu7-5l;MmI>`&BdbubMuiEbC z9ZX^u_fz~_^TE?YhPeBye#9=0D}U$O20cXzKKg_9(>h%r{cYW$U8IYqFA(zapmtEx z<10V%ds(SZ`cFU{vOzPz|L!x_GoIe$RPEEbayIabN*Nc5kTU-VghYi!b&7EGY{bd=yE%5q5B~aS?@@a` zY%B~iubAKbe2%mma^_6%d#1n+_j5&={}O+1v@?%Bhz{CehB0#g$LF`@E9{zY3KXp> ze}f^%{2jO_YnTggBTji@>Z|@ZuVTP|?)lUom@i73(&rC60rXzay6@!)P#j`sD%zPR z`@X4m$OE{vo-h4y)-QfP_2svVMYeBL^Pu!$$h#y%F3YU!yS<|9 z`kK}`eTb(4Pd6#N4gTS+%S7h)`CtB^21+0EJP`a{ZkO;ckn6@u^yjW0vEZ*( zVeasPjwrtDL*_N>2lG+cX*MNdUMEAI`>+iBU*|X0bC+zii@bsT&wSxp8S&SoSmBXN z@{xM{wktnd+$=Se6SKu??0eeU*l z^LD_Z-#r8ET$k5H9;j~iSGd^8I!MYqu{y2H>96;%s=vD%f*u!bIl)o;L=WXi8UOZ< z%HXuenJ-r8X>)T?%7A_D@ITT6!;~}36`rgf_dCecazf2em+?~Q9@-!2uWAJ^_WQuDHB0_}`J{kL>h_&09e zIX`DnRJF%K-m8=KGxjC^^ISZ3Slv>lSk<${jo+Vchg@NoJwLl>ILDW94U2OLat(Yb zpANZf&`QM<{&3Uey>=_R7~d`BCKNPlxF2wS4{FuA{c5;tINxJp{?)FY_nb?x$#IGO zL6DCDov}IWi#(cqBJ4^4Ui@6Cryd&4-}7NyJ1;uglygY*2lQ6vd!LHeFL}?V<`4c~{s62qF^~%c|Cmd^FD(%Gzx;__`Uxz*Tws7xMjIeoHR?4Deqr_o7;1@Bigb!agY#)Usdo z^Tp~mmv~-ADM$Rl$92^o{E_W0O=HfIU+#Zn+>}1fO&j=yN9r*5Po%8J*8btnUs^Qg zld}%nA>XjtAB)1)6?Z(U7Co$^q&(9!K6fX-o7&va79KH3Stj~;j_diGvhVrnVkJCx z#tjh;!Tr$A-~H~s{OGdQ?SAM1+#Cd)=a)@(k9DlsluyC^ueXcRe{*^3vvphxbOG*~ z0Qs+?vKvU-zGl~>F0OWS9NkI(DZqIj)}zbYtG=w_b%*-Xf%87B`jYCq4zw-hctl~y zyJiEQDFViIv|`YmhA&FgmcQjb#4A2=5wama zbJ@ekuCb~MSzn5ww_ABOw>BlJ|A=1hyZjC)`Zake%Lcyr zONNaxYq%HM<3a1*-E+_#xWp;<_aP*M??3aXPdFYXTw-rJ{7VDhj=Xj6vmf%- zs1c6qWWi&-@u$plckhEa$GzO~tM^^CyzmFky!HtSd!*-OFmUGWoT|@{>ve#|?OHyu*`ai6o`MNBO{ zkNBL0_57;+=|RRy_Ml(A+_ zKlfX9@ZFBOVR6@R?zb|42QMoy@9h%PH))cS3Q3Iz-iya=+voNe4O9o8Vo+y zS#7uK@rgw{zsEJC(f-4FeE2>)?Jv|ZJ0I6gsndKnG-T1m_f5$r$0hTQbvgt3_qLC5 zch&H0+Ku&L|KM?B-89?|+$&AR$KyMU9j`Fsf?^f02`Mnl# z;Ct&_zoiyUKfiZ|^K@&&;o*87rb3SXhhDz*gXX`}Kkh5WbZ@Z1!(wt=GM>4=hsE=# zii2xtez9 zB01_}3USoMQxBJV>+?E@`az2(kBrpD+dT>PX9Hh;FJnOwE#3jZy^g6k%%8vGLD84E z^SK#+54gqd1tV27RlWy7E*-`4?o%tqPn`0zC=)z`c9@hOUyiO-siEoZUBpetRXd*t#Wm=E zDWhbulfYfQfzO;)yOy-g=$mg@rMFy8Q{Epq??c=!Oc-6-SPa~G|G|0~7_#&~ z7p>m${)73}z1dKI?uSL*^Ms0%52#ybuVQ+=3_v^c{dh?D4%SPNw*u!n^Zl{bo7}bj zxi98?FsD`9#5ynXaga{}-Rsk9X&y~J745Wt|0f@<_Rw(t9!MtmhBnH3%TvQWPa+Sh zDLT=kX|ue*Wt}O7SRd|p@TkeI{-eh=0P@4T-frij;fyQ&a%nxKr+(fP47pg)GbPMT z+%)+_v~%2+6)Dx;tl@UxjBDX3jRM^@oN?v2w4Kwpf?kI*Aa6RQ{7!zq+PXZNyf@lu zf4Tpn-to|Ie$T!?_~vhq>f)*4!D#3DezfWELU}cu>pT6cT6vhnda~4 z{<|s7_`|p)?p)vP(Esn~kNUf6csknY_s6Smzwf5uiNLc#*Ij$m#0>mZ>$_LFicgo2 z>w6eqWsR~Ymi>XR(v|Lu^4S%K*voyY75KneH`DTKIM??$;QP9_9$7%cxxQ0A-;bGd zbI3z374%`!zV!uP$~)J;OyF%M)_kWBaKm4ZOwxZOL+#a<+@EF@jnK2I0$^V&VKk*UvJ{j9*lj`Rcrg7wDrb?_OZ^do03)KaKpvF zOCN@QmsH5}x&Pd=bN9BtKcXPwm^)PdmiVwf z(f`;BruCkQf+{=-@_esoU&)IzxW6(~zV@6jB6LL90HsFyasG~2Chb}F^uXyx9X1Gy zJWq#tCZ5|#yCG+`oK^Ah1^x4W(Po0lCH4oPo%vv^G0>f7m4aJ=)BX}atUsMciHp2z zdi|X7H*X3%vblES7SQjK1bN24#*Uiy<1?GJC7ueL@xOWKeyvV3UO0|BMSmvnYA&kN zo;M~w+}tu|737`q_s2Xgb?U%Gy^i^uQ}*#b``5kiRMhJj>mZ*~?-=^!LJx1%m&1R^ zvko3;P{sMamEf#{Tu1H>wO8gkB6YBgQe|r1!v3i#f_8kGle(B}`n@5%=c$g9;|)zQLZh@Eb&N`R{+~d90iwXjl zI>`4-1K@|{f{M%HH6@O)UeaHQk0*#A7Z5LYu^L4Mh`LGtZ?da&f_%n6V>zZy@+KI8-+vqVcsy`o}D{#)79>j zclWxe{N}pfrcv_89~H9woK=`DgDQwo&6__Z`?YM)<3`J zF#&w*ssxYl04{Ohy#%S7GTqc696>PtZ}j7gLpt;P49lg*l%e9` z4Qg65G2@fK>UX7EqaSks+WEdk-e)e4VUpnPR^U8GJT$^(qtUV7?@Pzj~{F&lqQ=O~oq+cnawJ z57*RWJd7N8Tma0Z%rm2C42rh)iw+qQMs*Uum%jt^xAOCsrme$@&8!_GOp;%IXlK4J z{Nvi6R3PyW0?zMO&-;mQ5yKA0C3p;Q=2!F7Kg#R%CjmI?PiW|Gf9m;{Nq@oDv~&KC z_3`xro({Zx%n6Tt_W#%0m&eC=MSo9Lkyyq)_OZu4D1u^a75k_yYMY25AZq2nzt5ffJ#l96`~2Sbk9R(w_L}=W=iGD7 zJ@?$@x%1>j`?=^hH}F4e-5$!<)AV~uiXU^E^;3#4{)n#L{lD#>(9d{$L|yS7KQ&kX z^nEbr2cC{{^NyUqnEw9mAjwbb(Ls0fd)FSg#gkJ+|Kx&?)4$mN)BnI}U2^5UVxRH-TNZHIzkS&F>X(*TbI zKB-a9g|vTDeDsi>CsJ7&!cFPQk9}iO`wWa!{`_dNvQ}pYV2T}u&*3v6x52^Ls;i^N zdZs%C545A6`eAC!HqV+?h!=iv0w+HojlEEU_SXVeU6=OIKKSt%|0M25n&*kXN9$JO z_&GY|IX&bYoTKl_&xMGe!R~TFCrJ ze^1*5d3!rQ+xX+$k$nY~qGzDyrt}NVZws&PuSpVw9rWCe@>~56s)z9WMsZJmukuN9 zq<^-QAo!yoKOJT1`mLw&{Fa4!>i0e4-ua!6n_S>@?$=;i%U(RL>D-UvqKYkYJ0JJ? z;CG|k@hB&Q#ch!0mb9PrzgYKiW$I6%Ki%hu0NpA76GwSJMxmbWXVmQX=sNF5(vR%h z@{4*K?RSNIx}T8+In%cGH}mxY@zcI_<K?8z66MW>agyy?e zgfKh@IJLj*opGbMKVyOCq1=Dt$T_y}4YE%_f5MJich9uu{T1?;#7V!JngwZI^7AB4 zd0^?lBmdI#GogPZ_(}iMZx-wSs=vEN;ZD?3oVC87sT#oW!Z^Ak?OX6<%)fyQ&jG)d@ZGx7LBL-X zM|#jjuj{a#@+6O=SjaPi?o7Mribb80Ldc_aKbq2zZ)yL`+=ym$9wPcxi+Z|8KBMpQ(j^>H1A#k`KlPw{%YC;} zN#NplyKbC6&^|2|>k%X9@5ayRq_%tRI+9r`;Ria0v4P(L`de$$I+d~&l6w9j^ss_1 z7j)z9{9dax=mcJXdV2no&|%h=GQh>W5d@J`(z!y)l!OFoO_5W0ej4tQ{<^Tz+OE%t zioXaN1rIc!p3YBG)z&u|e~=kC_3w`z!n3JOj~&2C&;4;%KIYGF!FqNxwC%3`MzqYTyQxc>|tK zD+l?aUo&y;oQKj3y3K~$eamN)r(`Mok%M!4E9ior)xA*xbP8U0uHIPbMDba^XVCH) zOHX*d3H}gzKDI~dJ*MM=P26AfJ7XFj9Y>wj2WdT`M1K~ZTWkN3{F_>w=@HCuI=7EN zUfn)yTPvPdjo_pH=+wEwN}gBg+?Vp=gT-~H^Sqc1eig=XmrgZ{QGR+={;`9;=k9Yi zX}*)zc;YjN&S#yVYjratmhz9Vm(FL^_oTgH-NU+uI$!vM&S!PNHG}GF!Wd5Hv&6r1 z{;b)Y-vB-{%5D*#eqHPZf8qJ86?oAjcRLjauGm|6K5K#gHqey|3wlg>Nop(a@%o<6 zIzWH-P|W0#cA}J}$A0qnztaAxP5vq_@{{-oJRIwEE$BM^RH_Ky2U0xIeZ98f<7Nfv zUhva8zzq3cf3&h&5r$h)PxI)+_;~|D7;Xbj>wv5Kt}Nm4MC$+t=<2`K-Jj?C5X=|U zezmI2+j4&Of6{K6PjW{dZpr5p9dL^0^|x~Q`FfBG?HWLLCg{$md_FOwp5~LK%X?R$ ze&c!H06A9BKYq66mHnjyoegv~Z+85>l>LRjov7F2xz6h5-(M}wa4Yg4;n$ZQnNRzF z(cjwp(jU~{%j||`yubCp$shJptzSkn-O>%nJ4x%k=Ml!^?GI4k)qz{Bk6$0`9A>xY745?6gEOZ{nC zW`q8dUsiXhY<+qCU_318a=($Ko#_9#*sF>~<@FJMwBQ_xeh1?Qy|ZbvdsWR|;P%kO_hXm(aJzD)1?JD4cYUpVmf^Xi6|>3x3(lL`8ByDvA>>R+b!{T)m$ z=zCsrAFYA>L0rOK-`~L$fPP$!?LBI0iBgt=-uHJfnupTfrQ17|t)+gM-nd`lbbcKP z`j7u^a=ErQx#zjF@9$s)iTHg?Hu^su{5dEEF5bgpXWvCU(%+ZOZzLE?>f-vj zP*3(fX|mxBuAllb>@OqBtv72%bNveUOM@leH2UaHKds91@#F*W8&KNQmShC$U*Klc zlm4dq;h{wsPS4S;pewm-=JODS+fYx>(H*I24T>_H)>CAkeq7f!eu#geAMF?EcZ>G4 zkXinQ7y7B6NV}+iuQpk5F@WJNY9Dl#k{@MjGM*fe zX9nG7y{<+mv&V}5$_DiVuy+76rKXfiS z^alA+`1>XM!9RS^v2wvL+y7GDbAmqZ^T2{4T5kn~{Fm&1ChbqRe|?M2H;7Bnzhpn? zzuwn3yeJW(6!&d>?H7j1nsI&#D`wko9{2>`2kA@z4$8p z>T4g3hb}pv-VOU-^m88MHN7}}R52|YK_TS(+UExS-?;VoY2FO@$%?-7vbcVBx&y-pRV%0atPke7)v3nlqS(2Mt$*ibLNi}6D5J)rz& zyAfVF0R9oU3-mNUWUCfT31qki&qZnesWzh6g8;pdF6Ha|q@DD>jlA9?O7r=Ho(CB~ z*K*{g9W-7=`)1UW{4T0rd-C~#o~KwrcY5yV#WX*NxT5EFHsIM|GH%-ax@vtp z36y?_%P#S02$LUJ93mz(qgM+(sqkfcVr=Ny($eDgPfkie3$(*z2bcfxeJy z?>+syq4_y3;SmK7%tAf&$7eMb{L1?y7kDi6&OKcEDYrKtIQg@|z4GO`y>8&N4qF|+ zz9jc&BydfT^vC$B>dv9eUYaAQ^oMe>muJmndKTWlih>;fQP)-{^mx`v(1?C_7mvH`Ushd-w@CO*M{Nl_vxcmv=YfY7XATcA3h7e59sEv|t2b9F7HIUq zp7v=yP5G$m$xB*){R^DrYlEd9b{Y$I1Tb8MdOb>W=ZH2z#uxnAgQR{&;K#Rpn-J*6D|*>j2Q!&i0`8YujMPVoDQ3guI_ z=ER@mzodLs5os6sXVGl+4DKH-aI$ZH>4Tqg`|Oaf2VKQ^WwVMHWeY-oqmTSLcdXSy z7;f>A-ylEnR8fvMkalH*ZtS3i=1_*)edHf|*tlC5!!6Ly3AzV28%-<5@NkSDRfzOM z%DEcXiZh(%BO~N|d&I9V^MB#ro6>{7fA5?7xc#Ib`R|-ob(iaB1fK=vj71wSas9NY z&qi6$re?VkOg}r}m*`<{96_vXgLrHoHY^nTC0rI_@$s;KlwpM~!> zcw@}^@hasb;z@^kdM+ON&cV+GCO)FS4Zta$Q=9a9NUzQrD%Qa z@h@;2%AWgYPN4O)$G@m|pls3Tw-Eju*?@W%%9taaQ)piz__Hd=cGY3h&XPScF4Njo z;FJ&P_wH-Q&N~udlm-Y~2e}6D-xzsm63-{ZPrny#x#EN50Q1ZIR`Bosa?`Frh7&)% zx9M^D+giR3q4pi%*M52O0bhsEd_eMl91!5-^3}zp-Nb)kPK}d6to>}nl@4?hx)@pn zGhBtZCHc+DyPk9TW*_sc=dB2-?<>~-pFO{j=NXY5;O`Ps4XG=p~&`pLhT3WDuTd+a*IoS^N`D44AkLPUETPw+SiZvY4l#gdSa5en$XZ&Z2LZPeB z&k3CT_1n&Z_tngw1@JeuKc(D18N7Wn#xupk@#=5?$L%u!*O!!jGLJhqoaZYma3gT{ zvTj|ueB!qNfADKmH*TL6_1RP||6v->S9a8seZvp9PLq8~pS^beiykwk+r+f!__)+5 zA|^Z@Ky=GWG)fKbv!=;y30z7|m;x4qaukC-| z5Ur4}E+y?IeAZ`w7rrN4;5r}tX062i0cb$rIn}-8uUFN1o5}Yh{R%+$ZbKPz=)J<Qa|dSS|ih!a-8DP zh`4%ud~mZ@#jCEg^wU?Ho*w1#sz$v5WlY(L9eMw{pqCkVmHSaw_;@9LYX94RE%SK$ zR`A(ScI({qk1*!{NZ989-q!xnWy*oVKQ7`&zT0uB(MLSK9Eb~b8EM~9+mcD8SiUf8 z(Z85KlJhHC`TSu3pB4FNYnjX_K7Z(dn^CS!T+*jBlW#>m_0QdettTkI3;oS_UQ6+R z`O-!c#frckKJsgi-|&dfPcGnUlr1L3{L1Yk`^~`5Eg$|V@hk1T_IEllNlD4d8`Ppx zO%$!3crJ{0Ls{w1tqleYtyA^MCxS}RH_(E5vZ2qPedq{5obMI>eJMe&+=DA>2mP-( zpC1!-;v?*K7M1{yf(k)rO$cXQCww$?os!E^SocE{e0MQ_j#2)uWCOJ z{67u6a)r-R1wQSkPq6;Q+s^?WQeN7Bp?On1k4qid54>5x!(%)yBT-LrwYJ!hS!LO} zgvL0PloL|YMk^Qp6JPqf-;v?6zcL|r=DD(8ANx%HWit^sxu~Z;Oe$vk65Z*EhkW3) z&a3G>w2+TeH*oTI<&W?5<^I-GkbagCHNdB;}g`r%2 zI`~PyV_!V!O!5_*9@3tJN_uzVi*Yu}G$}fMR0}d%DHXpIj<;OMuQB%Nig)+aJ1NM7 z-(09y+VFhF4QUyLe+oQEt&w&ckiQzek?~oeQBnw82b}!U=95MPyw>l)9pGP{`eR$Z zKQIF)yMGV8*_QW<6*#T8Zk#)Mj_1!T=x+nvs@+{qbH7IccL2Aps_92@DDAw;DMQ_r+#UsyL^pA z2)%QFQ@mpmW6w@w|F!~3Ox_%ZJd-?b}{?@M&RLn=x8&;Ga9#r^7nKf{5q zct3ntIW}*_Vmw6xU!L@yUwMX;-zh(&{p#M&{Z9GQjQQET__~gAg~xu#rTlrjceMnb zzbJp^fi9}YvzD)tPwR%VqYZEJbxTNPX*bD_NT2hB%P)Z3aL^UG60(ZoLg<$XJQDb} zZ9VeHe@dS|q$%MSV0V`ro{`qGP@W5QuQ@p$}{ii`BL+Fza zoc#IugOkU(Ki$B|AB(;^*o&{DG*!I)VgJe;&;1b#{s_?3YfpfeU|9UZj%pqsN~UM@=;)Cy7T6ritVfrBwV< zcwU?jxxWv+yIc49S^8aJpt`EGoBX=8?fB6oLikk&obuPK;eR#d`O5&D^5f5%RvjsS z3B74=NF~kD$#LUiX~DU<74k}-+G2lN|F3027e$Z2Tpv9*Z)&!O>zNN+hjprM z+4$dh9=70Ine4b%uE#)bho+kJ1KIKZ2mi*B9l{T8$d3SBlbkKLXq_nVDAd#Qm0MR! zJ>mJr4E}V`?fLEIHGU3~i~h+1{^-Jx-IaKJV4a=|+;#F&(aH>WV*ip4yxDL5E2}VE z1>6nXW*9k??zsv5L#oR4hZ^(P_9hXt`S^*b?ma$?8A~mEd{90j|Bd|oiIwMLdY(w< zfNc%g{rNdy7Ua`8--08RGx#|godf2A?$P3kzj66$?1S@xmtQexBJY1U>gk*|zjv{< z{G2TvxJE1OO!8k}hM%*!;hzZL12>Gh%+J|qpGWy6x4HQX%6Y=Sv=62Buhm)qF<;MS zL9T)Jag~RDOu19=rvuML`Bu+oH+cWhe3B2m`XIx6p5NT4r+nYABp*J0G3q^MS6Oj34U%sO9s{@%~E(zXt8B2|Hbf`?mo6)PF;t56`9Mn9JAHly=iSu)3-3k8=6>;Ew>^ zz-3iSa{aS_M*&Y8v7|GPk0{{jz{^gyHK+Mf^e^p0BjBHJlQNrdei~o2j(hq|>~-Eh z={2SQ=^V%YQFM38=|a96?GkR;ai|gBFKTK@`w6#S?J|b%2P12F%kLW1vjda=V*Uo* zj`0WUow@j~XOE(^AD9mL#AC7Se8%&46!0vRcV^aF!1aqjeJ;v^GII;xFDUHGM?KB| z-yZ(MD}QCdue8pdc_1c$<|2=Oz^|z-{m`V|vXXrK(D;e~-mciCTKt?P3iUL;y0lJR z#>ZDa{GSfG*ki7aeEj4B&jKEwl=gtfM=t6$h@lXz)9P6OWrmG%s{V2Xk{-#Y`JMi&C z`J48S4%hysifSkoIC%I`~7stP5XFgiDys0_WX8CjF%kL(|9>q zd9c^IEDt#4%hmojit>C`0G#|edjHs)+@B%!q@6S$Jt=zm2KPreaPn7|;tg+ce^7r? z`_DQ*n919x_utUDT?_ZWh38MgUo$c2(hoFl^6Lb-__)ylcVJyK^4p91`MeSfxdzaE zu=0cXeBLmlp8BE0(+Yd3AA}z$UZ|wFNgAuX0%#O}E0J6$(>ak1a+lWpW5JZpKi(#P zI8jgj*r88e$NizIFYTpy(7k=W&5x}UwZLf|mYvbc&ev&H$k&5zcK6mrdE8K3kUutz zUon@*g#~=H4nJNcHH@#rvw@Sper!G9Dfbt}3zZZ%il;`6F^%<@%Hzffc~jOs3wu_y zN-X&)q=EDU`Dyqs&nIy|g#)L!IMKTF9v&Bwz$q@e9O==G$Aum3#)9tGVV_Ope##_% zoHI-xc)~#WMA1LU2>u+<)qi_J7(aiAMBL>8Z?ZPY#LpjSzeD4@(V?>w_p|qdI zcZ(U#zal@2_UU~|;h-Bia(F1$U)4~q2T1j?0PTi@ z?$3nG;iSJ9w=_wRFug9*=qOM+ETgZOZ&g z=M$p+bj+Voz(1)|^i#fn&Bwf*4t!IkdrkTNmHLy`H@d{1qIiGN`j^h5)_oQ+m*ccP z$i+JE)2g{$xPRPem+ViOeKUaDpATHqMB0BVrPB}|54pf2fS-yy)t%zORN!1^x1YkN7Vuk?;Sru)cHy z@7i^5d%pjVqWy1EY5%IZ8LDb*UeExK0DkeezN4!%+)-TeMFHOwZMJHGEBBy-EkP1j zg~&1;boPh$Zq+bS=9Q)JmpW9^Wr1#OQuCcPK_|u^t=*}lIbFGrI*X(!atiOG7C=tH z_l@7scAM`Z5$%}KjtynI_T#S8oFZ^~KCIJ8eI7g+v5faC-Jdc5pT4)_a5|&&$VWZ( zYo*66TkyEimymMlzQ;!&wEcm%PxnpCxDRr)#F-efRmgWhKHWFz)_CwB@`=E0z+EVB zzL!y!>#uGm+b8|s=r<^ta+=`R0Vn197~E6O@oHmi7Ev!R~O zU3QEb`XkRv>DUjF{kNK&tHbT5a~1M$=c2t&1v3AsTOj_zWVyQS)OC?0A00e1AgM?x;o%y;61b7-plW|xv2kv&y1TtjmL)rxDEK$Z5{o1{-E_X z#rMklhO#`q)up9f6yNi&ocxl=?%?~~(g7GEpb5Jf8gG1csutMIk ztisn}i*ZzVpCcRi-wB#4JkQg84#M9tKDa|;PVnb~FCXPEe+OTo1*E{~K7||j1Y^}y zuk||a5ouaWf0XOqxijf5_#;qH{dn3kwlD8T%HvU>J2ZQb*ZER9>S@2xwf+4{ydTWa zD+_c7|9Lip_d_n~sh=)?IOT8N&vYI_<9yCnyU+4G=LUZi%ADE5-sO2#6Cv%Ud8WgG z84bC95x`0Rp_TjI;QG<}mE;Fs+&qfQPX|Bgr)ioqiR3H&_}b@tzV{!R%QWlxztS&- z=dQVszxeld%{E#F_7DUL9_T_n#Y*FmYdmKsz=PCnq}>MO|HSv}#RVD#>fsO40k;C* zoE2c<`Pl%R?7GxBY6#EIX5c!k58Jk^c!KBGEa+zi-Mc>~{>=Rv1>6RF-6MB%-tP|7 z(?0Ur-X?m!PtHewyFhn+)6KqopG^HmarNxh#$LSND8H$ZXU2~GPtEhAp{?{Ejf>>7 z?F_FP7iQ3zRH4(kd@JfHuI7Dl<0!?27VUJ4o;QMMT*1ay^>sL>9@_nHJxVpWxztoNT=lQqELG(>~(zoO3#&PeD5n$z8H@$2kD1(-sbhyNAmGa zEBMJjZJWF|jOG_HFVf{$D(QE&@_anrBrd(gn+oTv!u^T^a(|fg?rp!H+aJb!7O2uo zducwLFmob3##4!S&;qCP@r@NmKjY`)df;?Eo>2AjM1DSQ1Wvy%9oA=lD&OzepqB-7 zkxzR^@pv!;&jx-n{6G($Z)m+q@$&fS$Uk|!P(0E)fAmf@NAR=cefeB?W22cln?r?d}k!j2Tt(W zkPmu}e&=VN4^&-byEGq7|M=T)`FOX3UkkdXneUwB{?h~315X;V=1V@`+bRBmYodSH z!{>Vg@`(lby${OYlB=<$S5_CheJWYRq9iAL>z0@1ef-c;Pr6f0j~`-w3+8v-b7k@nync{J+KC_bOL%6YdR@L!D}-oENBX&3REj_$Q^{zCgf zXROz@5ls*x9`vXu`)jQn@-O`cQQ-94%m}*7>_rxuvjlEIeFT1Yd)yeZiRLzeJ7HHg z=$ic(bXJW361a-&2mbNRyWi7YP!B)q)!47i+&ruuKaW;*m-f^6??2|Wljj!)#s|gM zwSOc0d3-?TdptgzKJx#$d)VvVG@VxyfBAsJF`Qo;>FuAvbxlaG` z`O$)US}zWWYUXv$LhD8HuWo9QZ~6Mj4u0~_+!_yaxPR!poBTiX&yV}?^_Qxrw43C+ zhTSRP^64HSt^X=*$?xX1{sVt*btxz8(Iu~YhDP9YkMQ!(Zyx0GwZJVXtEJtm&h>Ya zeZZr(ZVTr9n+@C!ynma3vR>m?E%l=Ks6Fn`RnAZ6y|g~K@m=?}eEe#ANq#ynxSTiO zFFrmfKJ=hlGNfBHAKymQQ+(Wf<~H;A$SEh~TR`{az>1&n^^Xem*(g&kWNEp5cGMf; zhw+Ur|G?KLwEm?2ZM83?BKN2JhPQ7fbN%eV>AbJO>Ee6&`dv%yqx^GUrzKwgFXL_h!D3kpx&GvTx@WMx ze5vgm*Y}nDr2p=%i#Krlw7`uh-#L4;0=JLO>uCI)_@K!XKK`=7N8@i+Sb>v|KRa+5 zU)SbNy~)Ry1-KLCtoIIjo!6;Quj(i5*fqs3kFVb?h#M{NGOPUh^7XqD<4+HKbk_+% zeEm-6bu>PID81}E?mx;ODvaNOKfbxm%YMiu``nvqcj5LGRFZnzK{w)H!zSGS7SuaY z#?KsFm;0Z72Sn|knjW;6&wpBjluzwj28_?(?W=(6QJxvB-NED2h<1&@+uRQy%=a%& z%KyOk*B+(f=XH9T|AD_Tc)5X}*QtQpfv-3{XEt9S*|Gj{0xx!wV$poKlt$M=1KR?v4DT&zPwZ}Fb@ zO8UMpP>_iC2-^Ln9d_`$PzqeUPc&qJ#3jA5?>Hd$P4phg4;H1j4ut)p9}C~3`-!B> z>alL8zg}?5=R{E?5AO+nci8*>0eTPYIaj0iuBC%+bHHZ}138ZOqGbWkPm0Y5Vt6j< z>0E8oioZ4lGo0Q-sSTEPrF|XwF>jyV^Go*WtCn^0_Xv@Gnt_r(X3AU7__>uE?MDDV zv2A+!AjF;U54|@m3V6TIS2Yg?uEbdp`ny@_!0Ek$Hh=ZnBA}DrlJBvkzoU|mcC)~D zz0KJ7LSQ$ir}u|PfIbiO&SJX`6h%LBdfzy9gWhoDxieHtl(H21`^ItjAnB)`-yfPD zrhb{;H;$t~|K#w1blOi4mxx#2znhi`dO;)nOYf7UbJzKGzMjtekK&Ww3plUwf;Rp} z*@EDALmtIX+5XzU0vKM{|AVDn+B*?90~wwV{s`dCmZiMj`$zAUivm7kanmcojGx|D zN%~(581XmPKMQ;$|Hy=D;X#Z)9e6Iv4|kXAU4-HJsHeEvHn{Y;5QfwHBdPt0J^uNS zx33u@?WXq65BTn5-hKpdx(BnoW7aBepBwE*fv)4nU)(Ip+Nb9{^!u9*fjejMb1lNN zz~80I&+YiR1L3*AtAFyb*L%~e9UUTFUdkZ`R95UY=sy*Z`5@qufDu5kJE94c~{qzftW z<#c}Ujn2u^5jS-jS-j#s6MVGK>|L&5Q@#(51)hWQn^sq<@OyK4gyTJIM*}W3;p=qT zhY90_&h;nzh(C7fveleFww$+r`joiSocovTk3~BrjJ7Yh z{|bEgoBy-66z9(bUk=K-XZ)XV{UTAHhw}P{hZDJf3Q$k>W!?BMjr)hrNvMC)#_q1m z^HKN+XP4X+r{YUzf zeH+hro5l5y1t0k*J>%*Yu0Oq>Bp>5r(wMb1c)rdAe-6r}ZF?W*`bDBX59N*6#k=`F zI|TX{03W-2=~sN8O!`xN%sf)NGuJPtl6QQMjeK_kk57v4$WfB6Xhc67w?Cw^H-EC> zX*tdx3%*R0ha7QU_h!RUpM&z-F3#)ReoYl``D+)nYQg2_fv*7Ny;eD!dH;o=KEx>H z>?yYMAfL~|5x3#M8$9~#FTT$&K;DQ1Uh2Xg8$XBARh4onKFf_eoWRFdCio~m)-_b$ zqWBf_A?121X>O4B9=zWmrR4L%dk=Y#+oS)q>$_?vofUJQf(N=$PxIlLZ`@gYKGZ}@ zeWMVMSFI1W@%2jta5@+7SGr6lw zd>t`b*3*1ncl^`8sZTufDb{y7%$qkuKfBJ?3sK-tN7?t^AN16>f38tZ`a@iPz7N0Ua96MSTn)YSSQmU8vOAKmuj!tVCPv!%Ta}**|89rSF9P*+ zZkgD%>m=Sjo$Ez`?&7BUkNJ8i9ra{i^^2#9@bOCXZ5HUJZChF2%YM9v(17*SivFkP z^ZiLa_-H(RUP|)`kI!7-Zj}4_?8@c&PBTW@P4~q5Ul{ua&o`7WiGP2q^fo-cqrjg9 z`DLyaJI?hd`-p#WUWWkAPxrI+-Q_;R`t;KluezU|i+1+LHhRGKPx+`P{~nm8HF5t^ zzIKDIrn$##uAjyP`;qr9U5eVx{gXxVL05g_nj_plQK%>TQ_Bun$MY?%H>m&S9Bes` z@2|7KPx=j7+3HKKUoLR!-wT677jgaafzy0k{cxl8T))EpgB>lJHjCu)HDjgyq+ewB zq%TRn$j9^yol1JS>+vU7umg z`8p#V{07ifdAQE&c?kKP;^MR^v?%vGR4%i&udAuxqs-s73ud@<-sPdp88M|#@(e4dtB%10uAOJ~g>~18^Hk_37`t_K|ATJ5W|zlC9_K1~=wK7w~s}ow$Lo8*+iG$4fik z8EHJv*9~-EBpr0MY%Q&PUNeA?`uEb%+v&W2>3L$If6arZ@_EY&ep*+Q&U`qVxAH_v?X z$88?JX5e&gsxIB$$o1C&x1t>V^g=tXzl-bxerf5~(|P~efIEQy{?*l7oW4^(TCMm{Cvhv3W?(K74#+ zV!dGn-IO|ikKys5M!gN?!o|Z%@c3|`p5m+P;96eqw~oX)4qI^f~hN7wGW?!v45OY-aI9PG!>+eE6*_Scni%VR8y6-{bW6N}xosSP)lGKm%H*PS^#i9guS=r%4oV z--Y^E$jQ(z_v&98wQrW~>75ITB>TY~}LhDBw z-!)Rs_Tv3Z`A3aB`1yKjTpC~PK6n4k?Tf{_P@OFOkXdx}b}rumejV`3RoVw~ z|I>XEYX6rJe<$(z(+oapKP5S92XEg1+={Yx)m_85e{E>r27KEavorYm#)Z7^0DkvG z;{v|EF=PI90e{@|`KNq+qXVu^k@k1qGx!=m7tvtdqXVu^X|jUfXUW2I76b71Z`WDQ z@3TY!Hv`XFSnCVA&m!($(0!9AJU_I8?s@HyR#mZ%l&eYk95@}%?`)u3TzA!+YM}G1 zS8$F)_vaT4tv#8~N2*k5r#eiQF*&BfcW?=QEpWS*SV+#IGscNI>qrZ_qPf-o%6i^?8mbF9Lf%y^xOV{!Nm2W=b(;IY2Vw6v#Rp( zZbrQ-P2$yq-x|*Sq&{>F;$v*a?2}&+55@zvb(xeC#t-lcfE@hig9N>mgcC zYk?0--E)|q%SV7eS1bAZr@eQM>reT}2>vYx_Gx+lSWr*?Yuz@aBDYTuJR9Y)B4O`y z|JqSc>*cRT^gYh=6|I+PKEJ$pe>$JfRg8L!_b-jVSghNhg;mjW`;CxK>zU$Z7izeEdf*n6krTHb{*d<;Ea3hl|3_loQgKmw zEpDIFNB_aLns+(B9k?n(`k_M8HvPGM^qx41Z}YsHJ9&Q6f=`cf|IgVIx&7IYZv@`7 z((dp1dQeOD1Mj!u=6b#!v{U>8pFHVFzgMjXX?*;7bk8Ghzq_&b`25QGcQdZP3+r&z zG)Z@FoT(4@j}z@`fm@I4xx)Qpz&RS_e{0U>e|Y{kf{*<7*7F~4@b>k(1SaMiog{vGkHjC}o(P4hqS z`HB0_y=uLu2VQm5lZLNa?-_wFZJYfeU+>X<-`v5neGBL^-oCAW)q2l~bzU~;KFn!j zsE+lXSU>vSt8{=a^49QC+L!ND2K(Ntbb-D@+#7>x=xL=XOCjI)UZr-r)cc2J>s!|3 zhy4nRp!dC3X#o9Q+rs=>+Lz_~-mA2LKBL2^UbSDoSNYQ4p|^p4__&It>v)Uz+z zS1CxueaqZI(hev1)idOGfs6aW;q1HeY~ntxA*qaPB%f17eId*6{jzjElx6-id{;@i z;R9qD=_6OP=lfCGd+pzK9Ak=!e>*yHoT*zn{rL#-oWw5zf7dY&@`F<@+^C z1b-yzvr!6uQ6J$i{hH@f-&7DNAJSL+ThI>^|4=^jW#Re1(8CRWqF2w9_HsJG-v)f7 zulUOATLTw`kZXV(qL0OQPAB-oQEx#h_(gqsfV3~ir@o>fP(Gxu__v^MDE^^*`pClb zf1yV{_=(hsZmnXF#X@qPf> zq0))|u|w}{Mla;J5$CzAUXke1uoj7xsOWPOZJUUFr}EIV@!e&A0f{Gd1jPt3}1YjeZFHo zL89RP*{D}!dp=dxZ)lr8wwz}RD){X_`n0dGV#ML^fA+kOQ0POywWhK-!%Q(~$%F)6X}r0AG5N-h!KsnUBo|?a&oLG*`)1~l$i3iDMlL| z6Js)`rf3x%LSeCh`X-GLK1oeWPD~O0H8m2(F#<&xzV#UxDI1inh6-<*#2=p3#+#zY zYR%Dc$xXDL9+YuI`P}IfH|5Z;RMH=PZO~v~tSKqkl%Q>)4Hvp8y=F>`nW89^mN-Uq zw$fpybaQ-MOkAq)Z9;k$anjhaiW|pxQ_nOu(vDW*#3)>06yYNJ zl)@`ihL<*JtcO4lD^Q}=$lPi~s3{$y9cM~RQ~sc{c0gpO#?4!{dJ$`d?(~d9nm_X9 z$?+^)Eyhhd_>;Gt|fwEe_riiwYo zOHgdahzb=UAFTkM5K`*7RArn9J74W$1xqD2Sd5I-LzAt&hASoI7$ z8K(jYO%!qaVo;71A)-WloHBeSN5@Z4vX4i?*rfO|jl_T&V@ioJDI{@;sdDV5PEHC< zQ8H&^kB;cE)MS$><%QS1=QT~Hm)~ES*KE`;pi6)61-;0lc8mins~7!8>j^4pX{?M! zaI^{n5y7BvtT_YnpnMm!(N@8XNlN4-Gmr$Z^~724O% zvt1Nr6#pg*I{I)uVj-vNH<4ipnM*x?b3n+WGgd0;%rGu7UWxinsj0~+Bu*vdWkF6Z z$^%vUXRSSZqPZXvdTX(cBD+Mr^6!`I4O!^z{{qOu1+kV|QKI6E+g+87Qg7R-FDZZ2xnv|Ss z8Y30z_F}UEx#~rT3zYUPd0(eG+aD#lv`?b4hyaw2k_pU8j`93k=tp{ILQcz7&8oc{ zP;a{+5c-k7sU*MmPfPOJ|BxI989j^j8FOO%?n?IN9AwBp6y@*4a-;AtY(eO?mtnViG2k3i>Rmk=PTjGo04+l`+oc}B>wpiDUa&PScihwBUcf0C!<&{xW{L5>4u&+fhV zT7G)+1nns&U-F~Ke(9s=Bii(Qd`nTO)V-9qwC_uQ=urwf<@~HLuM;1wSE%%r|Nr~D z&`ZP>wVTECk5B~{)|0=Cz%x-&9O{-!`$-<gAK>*pID030%mdc%+i@Ti>MA=v43U^vKIp$$3q?LfUD` zn(Z!fs`_prPkEoa%7A+Doj#%+8b4Ihe9%SNL=c_Om*i(c&KEg*mj2pf%40zzSYuF>B4i0rmN&fl$8{~6lzT4y0&=$(W5T)Zc5X!nPy?<}0IBRmf{^~<^b1-CY| zmcQ{8ek*v5ezdNplJeAmxCC==Q$j*?VKhlSNKfr5>8FP6JC^$7#?g1k4+hkW@AMIV zpgc+?#X;w2Wpx5VVJF#<2{|R!&N;Sx=#+Yb#MA$;kk9?236b$RB;#C}CW()J6MO6sqFZ`3Z8G)|Sj?Pi)Nwn0JwKEh6#*X)op-IU+$$>`0V@hR+4{_}jOv|~LbDn;IL zflrxpNbvTLF| znu+Ho6c1ESr4T6S3D0jT`FK*~N%E=QUgUpAPx&QcmN&f{`h>4} z;Xk22?du}(K2vHh5A;z!^n|z$g?#%E% z;klsKto63Hf?!lW5sjt(BtH}Mkv{Y!FaO~G&R&wI$9SjjBq!%J@?D5GqVp|<&OAQD zBmQ^#P&{N8^|m+U1L>Ctlq8?xA+L!yeLnP#^`R#{^YA`d`tDnje5x;K`+ui@PIGU4 z@}P(NHTtN0;+fi|lJuee3CHix38yk@op=0@f7CwXF&uQ6KJ=AEL(0eQ6K`42JJ*N4 zg(O!wF`trt>F|F6qgQg-OLD1$N3wd6H)&p_lJaHQ@YDPv>s5kEZ=6*3~(fH+6`ESn7`tU-&aZnFliQoXij?$5|B4 NALtxH!{~(#{|9){BANgI literal 0 HcmV?d00001 diff --git a/verification/check.sh b/verification/check.sh index 6654bd4..06f318e 100755 --- a/verification/check.sh +++ b/verification/check.sh @@ -17,7 +17,7 @@ export LEAN_MEM_MB="${LEAN_MEM_MB:-4096}" CORES="${LEAN_MAX_CORES:-0-3}" GEN_MODULES=( LTLAcc/HashExternal ) -PROOFS=( Basic Completeness Extract Descent Consistency Binding3 Refactor ) +PROOFS=( Basic Completeness Extract Descent Consistency Binding3 Refactor Theorem3 ) # Certificates and their exact expected cones (observed at first green # compile, 2026-07-10; any drift in EITHER direction is a failure). @@ -48,6 +48,9 @@ declare -A CONES=( [LTLAcc.consRecBinding]="propext, Classical.choice, LTLAcc.sha256, Quot.sound" [LTLAcc.consRec_base_false_eq]="propext, Quot.sound" [LTLAcc.consRec_base_true_eq]="propext, Quot.sound" + [LTLAcc.extractCons]="propext, LTLAcc.sha256, Quot.sound" + [LTLAcc.extractCons_correct]="propext, Classical.choice, LTLAcc.sha256, Quot.sound" + [LTLAcc.extractCons_nonvacuous]="propext, LTLAcc.sha256, Quot.sound" ) free -m | awk '/Mem:/{if($7<2048){print "FATAL: <2GB RAM available — refusing to compile"; exit 1}}'