From 7e4a3687efb20aa9a88b4b7924660ba38980d60e Mon Sep 17 00:00:00 2001
From: sneeker
Date: Wed, 23 Sep 2026 01:30:00 +0200
Subject: [PATCH] add(named): the paper measure with machine checked
counterexamples to its invariants (M5 metatheory)
---
README.md | 30 +-
graphs/dependency-M1.dot | 71 ++
graphs/dependency-M1.png | Bin 0 -> 158535 bytes
graphs/dependency-M1.svg | 473 ++++++++
graphs/dependency-M2.dot | 115 ++
graphs/dependency-M2.png | Bin 0 -> 270508 bytes
graphs/dependency-M2.svg | 827 +++++++++++++
graphs/dependency-M3.dot | 52 +
graphs/dependency-M3.png | Bin 0 -> 103923 bytes
graphs/dependency-M3.svg | 329 ++++++
graphs/dependency-M4.dot | 19 +
graphs/dependency-M4.png | Bin 0 -> 28602 bytes
graphs/dependency-M4.svg | 80 ++
graphs/dependency-M5.dot | 126 ++
graphs/dependency-M5.png | Bin 0 -> 362500 bytes
graphs/dependency-M5.svg | 914 +++++++++++++++
graphs/dependency-overview.dot | 20 +
graphs/dependency-overview.png | Bin 0 -> 18200 bytes
graphs/dependency-overview.svg | 68 ++
graphs/dependency.dot | 268 -----
graphs/dependency.png | Bin 764351 -> 0 bytes
graphs/dependency.svg | 2007 --------------------------------
graphs/dune | 21 +-
graphs/index.txt | 107 +-
graphs/reduction.dot | 32 +-
graphs/reduction.png | Bin 29263 -> 28895 bytes
graphs/reduction.svg | 72 +-
graphs/rules.dot | 26 +-
graphs/rules.png | Bin 44541 -> 38567 bytes
graphs/rules.svg | 78 +-
graphs/theorems.json | 429 ++++++-
scripts/audit.sh | 2 +-
scripts/gen_graphs.py | 239 ++--
theory/NamedMeasure.v | 230 ++++
34 files changed, 4067 insertions(+), 2568 deletions(-)
create mode 100644 graphs/dependency-M1.dot
create mode 100644 graphs/dependency-M1.png
create mode 100644 graphs/dependency-M1.svg
create mode 100644 graphs/dependency-M2.dot
create mode 100644 graphs/dependency-M2.png
create mode 100644 graphs/dependency-M2.svg
create mode 100644 graphs/dependency-M3.dot
create mode 100644 graphs/dependency-M3.png
create mode 100644 graphs/dependency-M3.svg
create mode 100644 graphs/dependency-M4.dot
create mode 100644 graphs/dependency-M4.png
create mode 100644 graphs/dependency-M4.svg
create mode 100644 graphs/dependency-M5.dot
create mode 100644 graphs/dependency-M5.png
create mode 100644 graphs/dependency-M5.svg
create mode 100644 graphs/dependency-overview.dot
create mode 100644 graphs/dependency-overview.png
create mode 100644 graphs/dependency-overview.svg
delete mode 100644 graphs/dependency.dot
delete mode 100644 graphs/dependency.png
delete mode 100644 graphs/dependency.svg
create mode 100644 theory/NamedMeasure.v
diff --git a/README.md b/README.md
index 408c869..a86203c 100644
--- a/README.md
+++ b/README.md
@@ -2,14 +2,36 @@ This was (mostly) me being bored in a Monday evening and in an attempt to formal
## Graphs
-The dependency graph covers the six milestones and every edge runs from a dependency to the result that uses it while the node colour encodes the status proved or stated or planned or blocked:
+The dependency graphs are drawn in black and white and split by milestone. Every edge runs from a dependency to the result that uses it. A box is a result named after a paper statement, an ellipse is a supporting result, and a dashed box labelled with a milestone is a result defined in another diagram. The overview gives the shape of the whole development:
-
+

+
+The details are then one diagram per milestone:
+
+### M1, binding and reduction
+
+
+
+### M2, metatheory and checks
+
+
+
+### M3, subsystem
+
+
+
+### M4, parallel reduction
+
+
+
+### M5, metaterms and the named calculus
+
+
The rule sketch gives the transition system generated by the rules B and Gc and R:
-
+
The reduction graph gives the bounded reduct set of the term that applies the duplicating identity to a variable with every edge labelled by its rule and with the normal form marked:
-
+
diff --git a/graphs/dependency-M1.dot b/graphs/dependency-M1.dot
new file mode 100644
index 0000000..226b1e9
--- /dev/null
+++ b/graphs/dependency-M1.dot
@@ -0,0 +1,71 @@
+digraph deps {
+ rankdir=LR;
+ bgcolor="#ffffff";
+ splines=polyline;
+ concentrate=true;
+ nodesep=0.2;
+ ranksep=0.9;
+ node [fontname=Inter, fontsize=9];
+ edge [fontname=Inter, fontsize=8, color="#000000", fontcolor="#000000", arrowsize=0.6, penwidth=0.8];
+ graph [fontname=Inter, fontsize=12, labelloc=t, fontcolor="#000000", label=<Theorem dependencies M1, 33 results>];
+ close_rec_fvar [label="close_rec_fvar", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="close_rec_fvar theory/Binding.v proved"];
+ close_rec_fvs [label="close_rec_fvs", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="close_rec_fvs theory/Binding.v proved"];
+ close_rec_notin [label="close_rec_notin", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="close_rec_notin theory/Binding.v proved"];
+ fvs_lift [label="fvs_lift", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="fvs_lift theory/Binding.v proved"];
+ lift_0_lc [label="lift_0_lc", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="lift_0_lc theory/Binding.v proved"];
+ lift_lc [label="lift_lc", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="lift_lc theory/Binding.v proved"];
+ open_close [label="open_close", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="open_close theory/Binding.v proved"];
+ open_rec_bvar [label="open_rec_bvar", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="open_rec_bvar theory/Binding.v proved"];
+ open_rec_bvar_neq [label="open_rec_bvar_neq", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="open_rec_bvar_neq theory/Binding.v proved"];
+ open_rec_fvs [label="open_rec_fvs", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="open_rec_fvs theory/Binding.v proved"];
+ open_rec_occurs_false [label="open_rec_occurs_false", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="open_rec_occurs_false theory/Binding.v proved"];
+ subst_fvar_other [label="subst_fvar_other", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="subst_fvar_other theory/Binding.v proved"];
+ subst_fvar_self [label="subst_fvar_self", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="subst_fvar_self theory/Binding.v proved"];
+ subst_fvs [label="subst_fvs", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="subst_fvs theory/Binding.v proved"];
+ at_ctx_comp [label="at_ctx_comp", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="at_ctx_comp theory/Reduction.v proved"];
+ has_red_f [label="has_red_f", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="has_red_f theory/Reduction.v proved"];
+ has_red_spec [label="has_red_spec", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="has_red_spec theory/Reduction.v proved"];
+ nf_dec [label="nf_dec", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="nf_dec theory/Reduction.v proved"];
+ nf_iff_steps_nil [label="nf_iff_steps_nil", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="nf_iff_steps_nil theory/Reduction.v proved"];
+ normal_form_iff_nf [label="normal_form_iff_nf", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="normal_form_iff_nf theory/Reduction.v proved"];
+ plug_comp [label="plug_comp", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="plug_comp theory/Reduction.v proved"];
+ positions_at [label="positions_at", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="positions_at theory/Reduction.v proved"];
+ positions_comp [label="positions_comp", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="positions_comp theory/Reduction.v proved"];
+ positions_hole [label="positions_hole", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="positions_hole theory/Reduction.v proved"];
+ red1_dec [label="red1_dec", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="red1_dec theory/Reduction.v proved"];
+ root_steps_complete [label="root_steps_complete", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="root_steps_complete theory/Reduction.v proved"];
+ root_steps_in_steps [label="root_steps_in_steps", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="root_steps_in_steps theory/Reduction.v proved"];
+ root_steps_sound [label="root_steps_sound", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="root_steps_sound theory/Reduction.v proved"];
+ steps_complete [label="steps_complete", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="steps_complete theory/Reduction.v proved"];
+ steps_sound [label="steps_sound", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="steps_sound theory/Reduction.v proved"];
+ steps_sound_red1 [label="steps_sound_red1", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="steps_sound_red1 theory/Reduction.v proved"];
+ zdecs_complete [label="zdecs_complete", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="zdecs_complete theory/Reduction.v proved"];
+ zdecs_sound [label="zdecs_sound", shape=ellipse, style="filled", fillcolor="#ffffff", color="#000000", penwidth=1.0, fontcolor="#000000", tooltip="zdecs_sound theory/Reduction.v proved"];
+ lift_lc -> lift_0_lc;
+ fvs_lift -> open_rec_fvs;
+ open_rec_bvar -> open_rec_fvs;
+ open_rec_bvar_neq -> open_rec_fvs;
+ open_rec_bvar -> open_close;
+ lift_0_lc -> subst_fvar_self;
+ close_rec_fvs -> subst_fvs;
+ open_rec_fvs -> subst_fvs;
+ zdecs_sound -> root_steps_sound;
+ zdecs_complete -> root_steps_complete;
+ positions_at -> steps_sound;
+ root_steps_sound -> steps_sound;
+ steps_sound -> steps_sound_red1;
+ positions_hole -> root_steps_in_steps;
+ at_ctx_comp -> steps_complete;
+ plug_comp -> steps_complete;
+ positions_comp -> steps_complete;
+ root_steps_complete -> steps_complete;
+ root_steps_in_steps -> steps_complete;
+ has_red_f -> has_red_spec;
+ steps_complete -> has_red_spec;
+ steps_sound -> has_red_spec;
+ has_red_spec -> red1_dec;
+ steps_complete -> nf_iff_steps_nil;
+ steps_sound_red1 -> nf_iff_steps_nil;
+ nf_iff_steps_nil -> normal_form_iff_nf;
+ nf_iff_steps_nil -> nf_dec;
+}
diff --git a/graphs/dependency-M1.png b/graphs/dependency-M1.png
new file mode 100644
index 0000000000000000000000000000000000000000..2decc03920b628a65c5b2cc5e048f4a91ebec431
GIT binary patch
literal 158535
zcmbTec{tYJy9N9RC6y>clOal9AyP@klu{^}6%kU#kjOlhgph=a2+17Em@#A0q)Z`W
zMIuDV_^wTL&Uvr*ueWnuztcDMJfF|r_rC9SueI*&d*ZnKD*6rd6bfb4(IaxI6bh{}
zg+iTAw-kTEx4-^0{@+qVMR_^OJo&!|MF}Ak3K!+5oUFP-rcBrdw
z=ToQ=q2J8>GTD%Jk}Bkow$3nP@aI^zYFeCrdhT`dR{a9|K}Kd~b;DVFr0|6{v4QrY>45Px
z|Ci!ghi|O&WE0YRpb~dj?BeI^>LXamL{=lR5s4hreQ`m<&zEst587+la`nox)k`Rk
zl@ItK?=QQkE*g^RuB*U7Qq)0F)5#8@$Zy1KIR
z`OBB|YquS*xZL5oE$~Dd!@hm{Ca1oq*JYb)nV6Y%zq-3i`{}t=lrwLmq?)r#*KXKt
za^j2Y_mC8=bZ&9+XN{3E*lP9Zg)LVP!VWxt@#2V!OLxU`n~$$vtz=+es2q1Ma_Il^
z#oMSlaI=8G%GVKlt0VW>o;i0;(;_-zua)6Ydl4Ny{Q+57Dgi;kod#tzmj;?M<)X}+
z9vgHNyV5Z*EFCr*>%Ozo=v|u5UYqD9q4e2qf1%-4tCFra_a!EO6b!vfP>xoZ*vQIy
z?Pv(Euch5UGn3D1&Z?*9-<~lx_TFdvbw575WPVQKLVMwIDJdzXJHk}1)8lFN-y_1q
zeegg%W8XfU(9)9kVPIE~`jK3yna){~oxMj=N~&_=%=o}ZlaEin=;XHM+xA}UXuT(v
z<0nGdzkfev{KqGMe9?j9#~E^Ra_&gGif3hIF>-RQ-n(~iW>IXoq1Jd|p-sQH|6s7Oquc2PLaz9=yIeV&c?*YZj}NA(mQ4Kk
zv^LkN>8!M_Ze&Nn`5COgoXgN@8~X>fY(bva+6?-QB9O$M)>mWAl6TtxWn)bB(b{
z{~V3Ugrp=s9N^xxmbAX2G+(2XSHHh}{mT2|?2|RqckkW}HNh*{XuPrQDx;N^m5r%)
z-FEDrde^?2cklB3=*Y3ui9zTsp*(;6`WPdP>?DGRhH?NqK+D6!Gm=*uo0=*>VZ67;
zT+^T<)b8^OrWmbsy#ooy@6%{#Xi#~OsO#!)NU_Qu`kp*$tMhT9vb9x5cm7wCe)u!D
zHHHfKX5tuit)qLlvpQj4%T$$iDgXW7b?D~E?l=F3`JH@Z%ZC8?GiijR*sXvs1a
za~ew&>oquXgzna@Tf<89K&(GLW_A4mRBRP$04r-3IH&$e7-0rGRQnR+Ty~0IzLQSpw
z)>cJpocPpJ+4KP$_G}*%Ou86_^R-z>Xmx*oKl$WNggAnQy~uguu%V&hUDw<3!{<)5
z=32>LyeNVLre;yZOy4V2Z1U+X?*
zMK6>;j~A|V?dk5W_|3G!pB`BsuV1>1)5XJm?zeo~<=6N2tdn*TqwGI!~qQi}u3xlwkyefB1O1cIFa3
zKECdqVZD8Iaos;(hVt*c`1uHB|G9I#kCdbJEIRhSwlFa89Bj=!$Q$zfH
zHDx0`)m^>4%eHOXCh7Q-MnOTrD$B~TecV>((~zR+hCOC9%a$$M8F%ZJs;{Y%8TT?2
z`3ARzVy}`UZr8sh@ay}=M%Jc;gam4bJ<%pH8~0wg-E!E%LV&_0DXFX5RP5?(^RcDn
zlrF=nRe~ckJ5E1i<}X#x?!YNatuQ`z?6vBy#FP}Cty^hLO-ECKn}+svzGqfgzNFgt(`)oj1*dMGWsOHd-@#T?rw3@wGKdD=c=Os+wBm
zm)PpDoV)r~DSbwJ_GIt9kh^_ous|GT1TUsn5`5Az`BrsB1<^gA8rTgM6DBo1W{gM$P#tNZP^E+y4YGNEmzvf*Y;_-;_Ks
z{S5D+Iqu5m)c*PFSHIf2y1LLer=l*~xG~~nd@A2Z;82OpvolW`)X*v!Qtf?nzw!&BmfAtXWfsRdS@3C4(CQ`B
z)KnBtPtW0Bzi5ZeKBvaVf01w&H0y5O{yt8AwarK5TY+v?W@csyt9IVE@&0tzU0
zoi;?$Y|b#a;&6T(Ptc7YXuSCpb8y+EZ|`X-oqc_DyLLU@o~sguWB2^|bE@OVkF)&v
zj(>X4hhejfjK1#W>2XVP?t=sc1yc%#BAnQU{P7sgUs1_7(=B=O^l7b>jGmVELuF-U
zA^RDPnuUBEnYA|+TN-leR^V6?RBse!-|L7g0CrDMnZKLr;I2aajf=#EW}%wNvS&CKMp
zPnbp}Ezu}oDazerW5Hs4Jt&9`>8tYBsZ*y&5xRP9)kb=8adG1utx!qtUe9aSuAQ;8
z6a+?6xfveLMger9KcKFzp5Kcs^Qc)FaG~;-a+D-fVNsDcaFO5l8#ivyP`sW!bIKGA
z6Vl%?*59Dm*N_r^NBQK*le)RawX8NBtb(U-h)n?}w*6?u364RKdqqY@-f8;y@i$R|@0TS9jGe6mLFwjoH~PU9adWs-Py{LcTDUvHeV%iXtX}
zE!|?5^>5z1xfv32P)TX!WBroAzCIHIxMgOBsqgKzV(4s;Bp_FAer|SiNDbqfHQep%
z67@^m@*GCE$HvBzi#jgX;BWwdco!E-Q@H;7j}FkK6p1cb(6;IEX#-Q!DbC-y^ns*eZ7fM?&n^|=>59YBYGSkd}Antbd0SYO?`
zeHXU?!7ws1dY~fl$jERmUAlA<~Wg1%A&HVf+^`lt=WHDBv67)__PIlIWZ2JQuB9s`DO%L0VRP-xK($Ndxnvza0
zna*}uL`0+_A|J>v&hC37Mep=`CxC`E-&btiwv9(jY@HX^gOg9snE)5vUB70{8m#IP
zib-88?Ik-q{?M4+EWdO#f4qBlV&u^gO-;@20R6|h`PlGH|MBs~I8XdA9@kL^sQuAi
zv;r9DPDBLHwr$JY+}tRXg9ppkgiC1M-X|=4;?=&zZe`=!XqoB{3CaeBhF-kK?iJRV
zkMIsz+HtlH5X~H~WZbrCO}a+$1#`wlV<`56J)g|82ex$o5ly1#{6IQBXLbs=DS@NJwx<$d%i-nQfebJDxmwQc(>Q
zc0yHk3FXCE5fgLsgFra%jL${=HXNm}UScHB(X1z<>n~5ZBI~Dl=`ppFeX+NfkA_
zVVz#Qel3{uxNqV>4D!$t%I-aTVjewO3W!cVhc~3Cm3lLR6Th64GaXLR0{ze}UoLz0
z?3UQrSjLSTbq3rG4Y~11{wxY9im1G3U1*UM)@|4ji)>pt7jf@iEVkf;rsm`EV&C@5
zD4W-PeUY$fy1Tn?-n{8?^(svvkju!(NOuo@4+y|5CB=@ihi)n{*d;kR`GkgscTSEd
zI#bH&)2I8seUk+9v(Uqca
zX56$%V6L*V(s!EtV|{(j!-o$G3k!P$2Qyu|bg7~)*1PgJN)5j7I#1OCJ~TsT+=CVV
z+}le{`T6rFL0sq}G8rQxBLxD_2Kf7vTnEyCY2!wJq`ORQejFeGcO0eiwzf?qa6>~`
zQq$665)!lyrgNx#3c;RbWC){a=i0J`Mmbvg(4|Ye$tN%|c>)6P2ni{->7PE$j#BXM
z!-uv0x4aL%T)Jw*e*6(C1=fH?-iMV{?8}!gF-b`$Q{8cH6B84ebtarfvWE+(DChvt
z5Ba`&rDUUSj<_KIji;WRoK#&=a7aGa%*3R$xq02O2vKjmH#mcLsV8@l$1N*cf|@hb
z9nZVC(aDNoMH7`D@T|JeE-gn=z$%hv7$3+LQgg=4jDE!me?#}LU%!$L&$rez{&rMU
zAaV_WrGI5~XXhD7Fgr*Y%P6}|-_tZUHfH4HTuVz692gkTJ`q3h28EdksTe#>53p+Y
z`7hr-By_J{hn$QLyeoF#10EAQWEfLdTKYgP=IP@jN=g;z^%>W%_r+QR)A`m02M5!w
zUd@)k{O;X5#*$HFggT%Z?UN^C@PfdCw}v0sEIZP5dA|
zT2jv%jR?FgVV>~U^PDGkAfNh^4DNxzJe6&>m35gv>+ph5&f`j(Ea#_!b|N$4
z`Q#!*Ex}!E4YU|~AHO1j3i$}XVy6=4*pzpPh**Dl$+AhtZ4)|5yoSfMYfGQm57J9W
zNC4KAzj?!eQ=uxKwiD+!&wg;j4*lYlx>8@)l*LwjpHzwC*%YCVN
z@uC#(O8Nr)MZ^TxjvWjD7Q#Ds%91BBGNRtNabuQcE9<#)=Tzk%+al(X{ydkh<|uvp
zb~S>)VRCpgKr0mme<9=P(<=c1s|E%K>wxNB)YKe}ytla8eQEV?yG@;(#3dyqGcFJ5
zMM^od=I7^UWM)2pAbUmFR?
zG^)$B(l6FiPeG~eMw2!C^Jf{lA?w~Z?4Q4U0Ru(%>6zU@6kx()0VxIVRdKF1G%~Uo
zY}un*C4xT;fDG)^7vnrOIa#Li1GW}q)zX5?L)Qul
zB#=yjPp>oa96p19Ky}TmXZn5v)J~+B%@PD`^{?+u24~KAfUh%{nH<4;1&ebOC6twy
z+n_&oaCCf*9v!^1c6DhY?=3w!!&O&?lvXMwZ*#leXzk+QC*PcBrSWrCO
z)wnpGr7PE+7c;vz`)qm9
zvONqu{Obt%Nc$gczJxsB;-Wlz_G}U)r?AVU_1KS35tp6Pd-Mt&Jn?$n!(HXWPt>Y?B^cXRQBoVD-KO}4#&oZ6
z^YCPve&Dre%VRY9-PcxgGN3JH
zt?y4l4azGh=mDG)yZmDlAlu0A-e@DBPGM2eFmaBB??<1-7lj1ao!jA7E>tqJWYwxw
z0;jU*9zT9u$WwS#uh_-6!)MX*?Ij$
zDKwg!`AyEgrzh2qPX#`-D_AqEPt~qlx9&`Bm>_9vO-%kH#59;#9lY#{Gh$Hw
z??_zUagBl94<`wH%3W`@C6xcRZ#SGA?jncbc(imtR@QECV+N%jRDhGW{;qS;c{9tA
zF~piR2uOr(240SwGE_Ny0W=0DlC1UJes2XXy$V1KEUAp2C<1xMpv9OR`=H#_-R*_y
zG=sGg)dGF)0;(p;q^wpO@oIdH~#R
zl5%1e6%|#LkKHcrFw7-AJ+KS=f^$#3VZ#Phd2U}iFON`ut!^JqxBV%aX&H{A=iV3{
z)d&Oq4EWxKKPG5{@X3Mf5(@18i(k{9+j9A%o4PtPa>Z(pu5E>mA>JRv%@7ahxhnx(
z$oV^KYPSXFNTsADe1UI-(`fhDv;eDyBfo)x1Y4$`1MOJZF>~qg%O
z$|tuzIFTbbJiHpDbB0kh!_0WAm3GD%&-&m$X(%drPvr-&zFqHP4mRglZp1l_4^%r)
zcfbhW>>F!zjG0?8BsiE#U%z9o(*;s#PCrwB?W^!4JG(MSX6`zkzN@R;XQ)u-mZqK_
z$Kk+DzS!kRiOUR-s#N8-clAcQS9ww|+hWyY2~u5XDAheFDD4UF@yP4bw48A;BRgF0R0yppJ^BooBt7!Ue`dt}e6Be!FRVp`)0~q%b=2
ztH^T->^|)=UaY=%i1)K+Qxc{+{YEK%AWXX2i=2rN
zF*Wv$8jVsC&!2=OrOJOeDoWgr9>|C!yyUcFY;0`kR(e8|rJrw$cJYD~!`jNh&K`hc
zLef9U9q-@2rxZThHHj(-Zr%%N*6*#NfvkH_Ae9P9r>D;Gt7woq0Hf8QTA*pc*OroZ
z*meF5v-5G&R-!KA_h;~k*4Eag*ir2ZC6ETJ?d-gPeL#Z*wzaigY=!i|%&TR~i9LVeQGrck(4fu1Tf0B$3oUv6ef;{lX>R(5*MTyh)G+qJp}Dj_M4e)
z7r*@DMq#0((p?eSiJ=a15ru1_`5qCmal_sV
zx)#okgXhnlEk##=m9Io)tjo7OzjD0@4N-VJM5cw5!EW3g3=NM@L=a#4-nfc1>|pR?
z9zSLPXgquVyjH8T2r1>}=0;#t8X9>U1R#!#4YslYo*Z&=a`GLNupeL?^3(goA?q$!ck7MTR(jd}3^zlWE?xgS-ln|fGA8%OwRPzCy{)D-Q4bS%=~+%M(C|uYslfDUdF&BDw=bub+K)U
zorpZK0>S}3ijQ-4&hq_qD_1ge2C++M-jQ)HM%SMKKoEoV>&`*(AP!ci`@9
zczo>m%Uadlqeuq+gWKr5pj2{_oMb#c%ZnquO>E!PD!%5wUVwcX<`L?)fUvX_FF^PQ
z4$u6!A?colzKtX&dV35uoF`I6QZ_Y@{WuI$8{L?-(HL($;vYKD(F*BNv(_J}8
z1k3p~Qxh}ZBCuqS9zA;G$Pvb-_=JS;kB31MdC$*HlyvtX(CIB(b67@$IHXRsfvDYr
zTuz4;{>!*p7&+^+K^yic0G>U{dtF|BFe5uV?P>Km@B0rQXpw#lNT9TfF6Nh_T(>Zn
zHy_XvS5#M*zkmPaRI7%X8h_)XfPer8qjTkdj?MI`R`St{GTBR}Q
z;Kbx)Zb`{aC{`(#WQ_Tyq*TTv9!PJ}F-}ZMia~WRB%8L80aT%IL0Gs8@kW
zY6*nb1bivOA@T=|2sb%+=n(D8moF##Q_|n%+4QKkDjYq^6b^kX7~1Q(?J3bOlV9#^
z$Tmtz1y`Xi_ImlBa-?xYPqLxD9_-!00|yRd=jfa`;Q`2Ph;{%pRv8-8ijC1E{ovaU
zI5>!bCk{loc7qTA!YoI=u7fPQZvA=#Fq}v`GS-NDG{0=Mksvuh#en;`-G^23XI-bD
zraAwGMY&c@FAV9=rUZI}(d^VO;Pu1)tb!B@uuM|@vGd8?($XBL?&x*W8|{i022f{FesV>1H#Cgga!dNS|@UrPSm2=1JIZlO!_`P-6npi&jZPGKb{7Z
zePv7IhYwe9902{%{VW?ftnU5Nyo5XSTgmqA5%D-qlc>k7?@aXs@|IEr7dqe?4E8Spz*@
z^oXKj`D&S&6J0s@U&ilE={`k8u9*cjCC5Q^K`(_4BZt&Oj3NTMc^R)n$vXhNltCl7
zFK*`*A8(xL_0-#&mOQn&xw(K|;X0k%3*M2Dx(n+!*c>J8>IZXBX=7tf%fIpvuH-N)
zuDkrzeF--Cz)iBy%s+olPKZiLNkQD{UAO&tQd|3W^ESi?8X}Z%1HmoJ-zg&A=)0Y8N7YaAV0!GAD81+cUnG_*|$
z;}sQ!lZpwb%_Aqr-rEwmg=_O>Dx5)9`2^I14ddhEC^X!p3x!n(rB*#T`aR9kr3bJJ
zRaI4hLZ3gMB~0GwXP5YL16rIctPBB+n)7Y9VSTqBZ#u9Dg~r0d8vMFVK|T-xKuAbv
zY^bB;R7-tB!y(8h*;$7gjIfx*V+6+d0Zy*nCZ}aTM@LD}A{0Bp_NZ1TY0$5@vFqHc
zo8k)DAyW$*C~DbK`ug=MVhr0ty_i)R6l=Fck1|t0t3=73`l;)k5ExVI=G+ttn
zABE0uUny;!BR$2yz#!wv6CxMX
z-oJ9Q|540AA8u?32>{ggdYeA>X@X`ieN){8m3POE9jetaPTLVUguOv;MU*nlv{Pv9
z{xpN(#y&usY;EAcXNnAQM@Nq3c
zdS%`#>hf%iNCoacqW*Tvwrxg`U&Wlq1?HwZ=F6(84)-5f+${BZ-DH;VLAEL6^WnZa
zo*V0SEGdJ~Ji15g;
zRLCum4T)iZ7gt~xTudU4lfQp=p{wvlKK&mi;sn2cf;Tb#Ay08{-%gLjOV#-JwExVE
zOOlZaAM6Js4O;p!z^I@ZpW}ePdwO0OKM~{(sS!4Q$&52yR#{1F`}LJ)e*QkQNCK{amw_SSK>FvMM04Wq^7j!Z6IUc}W;eo2v9Pp6-LWJq1sz--ZUK0c
z`0NCx+)+AVBj88vx&pjlgrAU>3)w9`@Nl*|mMPP1)`|E~z=M^~{2nzhGxLK4XnXay
z^JDm+fZj-k!-4jODqw`Zz+q-`C%SC9yGp!va*IT*)7$zfvhMu+4l>8##4)0RaG^^ecmngbO9?8eigzp112v>lLz`u)T>#TnLDu-
zWZ`fq=#L#cMl7(T$Hh4$O@WDAjI4lw0AXa`
zfrrV&qmmp2>D&wQs;;i?aGg9Sv1TlgTMzfbMSG2;S3=5;jCcZx0PS5REII1@4AqUr
z1ZEcT?6jmHGgKOAFa}6fz^16}Qowvy&@vuC%IbUDg__8)Aaq8
z1)e#meJ$!QVMrJ_rElP*><3;2+kXZ8IAPR5p8>~1KT!8WeIon@5(()LQOMxh*c|wu
z{l$x3P(SN;{>iH^Rb~7Vyg_u@z|A#){-1+`1FGjCcsGO{hR>|ru={#=nAUzq8iHz~
zqM`_#1G(mltY-uwZr!ePD*<4tHs;)X2%f6qKqPW^l#F}e;eZX~(Dk(!Nf1&U=uZ}!
zTz}$F{Q0+0#88-b@e4hX-2qOB=Z{^&o=6Z~=sS>GZRwXTMt3rQzt%`rBKS`S2ZvHn
z(txY7pixfcSoi|T##wa~ldnL_^q-wl&7nhwx?l|?FN~HDg^L<(JfVA$@QL@(s_{T}
zBTk~t*H`PwVFr*Y$B~UmOuWv(F8%FC0J2WQR&|9%t
zk+mM{75PDz;a+T`pjNEHb3-(v1?ba0bt=~M!z0Ni{+pqp-l#<6xD#{j9~BO=2*m@j
zjLfy55e>Do1INgoIKfCx0=S4+ECtx2N_kG#3Qog6tm0!wgi5+U!WNzqForZlEc^X?
zGhP4@g=&8QQC(N;>a4A!Lv&MgbP&s)G&gG#poFhSZ-Kfc^P{6A2(1X})dOrkSr8lp
zJPP=j9d>79&B7xh{9$*9|epah{vmw_s<7o~uRnhx$RT)c
z-o2X{=doKKuodEl%83&c@V;0CR{s5H5uu1BzOoOwb<29VQ#Mtn%kzjY6r}FU>_k$Q6X0bN+@5RkaShYfR_MNTZIfb4j}sj=wB#Yz^(0RdWx|c3R
zfU5uwrp%-#LNGm*O3~52-O$wJ1E&^9(d~1+TPNi9@bB8Cw(0eHPR<~-Ql!mTzI=K2
zYECTRi&wAYz=33T^HSjKV4bD{I8A8oQ>JXaV3L3p*t&J=qGu)izc&Gik+sV%WlrGw|@@Tuf|>$HHGZ{y$%9u*nhg
zE_T%Naf`T9i|&qyF+E@dIl+t8qXjo-?KmFS?N-fM?INc=Bq8$1
z2OeSfS^V05E;4(Q*#5r0z5=+Ih_G9Dc_AtM`SCiv9A$iXJ7~BE(0*j*XVm)t`;)^j
z4?l6mJIoV2i1Cop+FHebKl53b_V^WrYz2o0HMr7;@$pCheJmaM*1jTQ!39^s0azL)
zPXA{|m?B59ob4N7I6nw8a%Wc;m9w++zZV+JQIhSa!8572xk;0ZvUcqifD}A6H`)lo
zV=5^D8rx^qRwJ98nA8aa)=-B_pMu;#&My47Fx=H;7#t-2BpscN@S}S{StI4KW@qCe
zg7k0}g<;m8oSp`Ih34YV8~fY9vsky$3HcTsH4`)Q)#@P59~D=5xCEZwdUS#SqKsa
z=gwV2U-ul7AjAel)El?0{j9Q#gmHX)y1?+;`*_vrMORg9i}`{FjRkOWto0hN=OvIRnVhnEG%>dPxdE6skqelj*2*ufsOyE
zTG?xfKQ0|#Uk=RPH8>bRS`hR|#KW>UP4h0(NS=IVSXh`zLoy4*f`@^+#D9sTHUjKS
z>LPp^SE8diQ4CP?DUj-k4;WpzEE+wcL%*mg(w|_|&A+%64ce7O$fwdT_GjA`Mvu18
zEkSu%1uFv@D^@i9a)=+&bU+P@1E~)qh9?MOM-1#nv&yq^m{TshP*y$H!u|fzQ+K*
z9h}Y^>=LXCNIlga`~fk`AftB_B(3=KHoCC)tITQva3On~0hrFa^li<(-KIqE>xLl!
zki)xv#4HV+5X5x@gaE<77*G;+8Z&{oT%Z^5{#8wlCxQkOMvCA8j{VynXOb&^X`vhu
zUk4x_K?h_xk@k^u
z6MCD@i)=$?1s74^Rd^>a{b*Z{G${vXS^Y@+OEmOMn>O7*M|JeyXD(m(Ou}vxA{kaE
zm{_}j;7R6&j3;21
zm!YJC3EZ@g+m3m$Ufo)UgrL3+vss4kA08zFGC|Yedt<>bt5!P=*$uX^5Cb+~GH7lO
z^xul?NiSh4&4eN1)t#Nxpv(WpJ@@hvl%Ql=aDh8v03yc*O+*EZH}QdT={2>r<=Dj$
z^x)n2BM?Y;>VuOl@EK$v39G>O@1d$hXp`15GHEn`q$3kMs_7WatnB6`oI?
zh*Sk}uEr4Eg0)3k7NTRubl`+u{t1_3Nky28>khKQSm@YSEIl96@W)mBm2F
zOZY%25Yz!i71gg*J7@Lt@etKQzEW7p0!q{aLI=u3^ys6Y_7
z>uU@zhVUNCu=psV1hpCUgge`h
zR&W?er$~j9LJX=vN1LEOL;m0+&H=Dmlu~fABb99WBs0U=OoR)>=1#*3I!qSD;n3x|
z&lfkp#or=F7qNU0atIzNrO{CVAjcN00FQ{sla`iLJ~*-nTZAtW_!}?DvLqeeC)5w3
z7N&uiQ!P3uJ~XmK7MYtFRVMiaGW>Ixw#d9LIba|yv6NqOp2Cn7DdWxod7%Q+kHPov
zla467B@n7Kk@Pv;CaFlTi*x3O8AzDI`U0jX9vD%@^wcH-Pl?SAoDRA)J(nLyz!``{
zba+%0ViTx~ljngm6D6h;1d;!*U(kyPeGadyJfOu+xD59?Ix6l#b^-qBc@fOh(0J}x
zaLrl5B@rkGHxF3bKUwa`FZIm;W0`o^&RU_8)Ny;bhwH!&g0}4(`1lkg*rCv<67YVJ
zFphvZTuK3*mDM&YGucT^WED==F(z;x*0WP~FiMozaKbE539|<2+;Eogc69DDBg@b<
z(o*h7I*LGEqELuS05+^3h_X};d$xVQx%r^quRTz62whFdz_ID;>r)?(PrM0pA0a;7
z-RI5BpYqn4jm*}=+yhu8?P?|JxQBe%&*lh0Ky?ZiKanKI^zcEG@
z3@cAyZ~*QjR`aJY$8=vLK6aR_e^aN>fL=k*r)eIs=NpnUaZqZe>k0mgB`U;HowF&@
z(j8ID4QQwsWEqD+`*UM763nz#e)?h1djOIcXUMBJwes2j*9$OcoV^PYgqVZ`8BS(t
ze_m85z1S880*=|722F+@d3$KdZg@;s!r}Fq4=QpFs{QRYQ$63u6?*(uY^>aSQ}N7;
z0*~oVH@@5Q>Tub)^6{v6f_(M!^OV^g!4
z`c0Pu*5~&(Xar3UHd>}U{{GuVx9Qp0pzpt(q*YFxY8lAnkY}X9s7Q_7tHy_^sVI*2
z1U4Lj_ABuxQ)UZ?CCJr(MT-Y7Mefne2}ztE7@7gI2vtw~au7(K3~k)7p&Qie6Oms>
ziN^&vk_VnwXlK<>W-#D15d_!&)lP6)lW@rq-`uNvdsZM$Uq_Y0c?@G=ISf}M0*SQ-
zoy=j|DAtq3Xs%-u6X}MEr*{CIMMyRF0Q-^A^v6ayqC^zLr2}BR(NA7!{tN18Gts1Z
z6GH;9=Aj)%XsiiK>F_-*_Z{Zhh&DtBV^b9u~gVtf&14lYg=Xl(#XYqb)Kw*h
z`K&?7Cno<)EePxE?e)QNlhXPKEZ*@5+L+@8~g4orA-AQQ7ELjsG1
zE_>tmJT$({Wyo>XWKi<(VLx{7d!``pF*R$#R>`+;EdwYmhtb!2D+B+CeS%lN@GsiN`I287%3yLzijM0A5Eb&$Zj)Whyzd=Ug1i3ujT;rfNR@%yTIP+ZvM_|BJ*oKj
zDWu8ZuGQs>C?uBG
z;iEJY9|PJMm#J?F+PN3lVRxDLW%r3X;OZ)c`FRAfA8L>vd%~eSIJ@Bet%3$G_;)RD
z?LzE6JVEp(Y>FY`Qp|m>u-T?hpJX(o61e(k$c$d#2SZqygFv7ffw?vOQ>VH283Ieu
zpGTG;SQ`SS&E&8_X3sk#h@QmOOvau;)IkrZ46KjEi6GJnv}{JSqlSMvKkj`7(w=Iqu)5P?Jx2r9sKTJq4LQTUc)EbF<
zeJ}!DBi4N>XU%~>w8z*cZPfk(5l|Ok`V8<8bP(Vmi-8dc4h!S8&$7pEP!Xp;<`oEg
zfw>?;Sa-NiurEYJ(>XFvk7P)uV(jd)|7DlEw{Z_k1%s?y{TiGJ;(8-QEbOpEWnZ#n
zNhe%is4|&7e7DQW4$Q#yMlNt56$wlO1|Ygi=4XYVm-5;diXLU8!MR)t@B-)=@b@eF
zKBo1&RO2?wMVMjO?RtH^I*~Il*mP4Np3F&0qilm^^JC9EmXels2%C(&vl5j9@No@V
zKWqWvSPAk$H)I60iJ0$Hw6*`U|15gw=+WgJE~Bf6_6rYu=EC?JIH+CLIP!M?f$g7!
z5uS8CkPk7hT#88t^fK$jFPZpsq(4ngriTHY@Sfz-{Usa&Aam+Q
zpTMsG;#MI-9>m0WLULs%@~Ee$Y_0Tl(Z`4Ya;*mBw~@K&A^*R4DvF~Pv>ydlyZy)y
zV6Uu4x)0SiHX33faXP9YNy2Ns1l5NaM%aJlqk|@7D9Cs+N|3y{bw+z&*sRFQIq^lvQ6FW!fO%P$Aj>~Xj2t$yW
zDT@RJO9d@{$)l9uMZ~a77N7Dxu=ZSc_07_Llz45xN0W
z^W{nJDtP@;(3mQ^x+^J!f`XkJ6SQP3
z49JQMTw>Y=$b1M`2K1Rvcemm0IVN4ys;Ma_cs{Nz#lfbcAdg>r
z^oaKv?!tg9b7`P>H*idGz2tpeaNa+dzpRplzeWmhx>YsO*d
z*AOGgFl=o-_a>6>??X+U7a)xBVBdc!Dkz^_kc|Nn%8-)>{_t&M4hw(7(rhS21(WhB
zs;XpoA~SAr@TRVZV5r!fw4%p{kr}-q;KAQ;mE6kn_mpr{l80cHch(7T0+&rZ1HkNk
zFi-x?V~KoZWga@Td@xf7>jMOT2C(B_)_;T(&lGH^Hr9{`UW&K@L7EDmd$sOwN~)WG
zdi>-7SY)}k+M_a@Hwzr~Ga;mO#K0Br%c
zF2QjGvfdB$G;kyc;)53y^y86YRJa)A?@HR8U3fHc22i|Y!~(7IwJTSsiOd~1c3s+a
zip=68Gn$SrJN*YYUS0@~gDP5D)fj&A$6Ygqu&{$S3uzAK7(0rMo|k!iA703
z#iwdP!zfq4>^4X*fFe>uAg*3#Kg#?6ne@cD7hfbC4~&WJ6Q@tFLN0)C!
zML|;*15*Qqg2Vt`0b?FU55)D_8|eH(C{LwvS|pdH9e9J}nFq;NAva%u}Aw*1nF)kLxlX
z;73G!#FqlEDkv&aQ6Mk(wdL=k5QY97e6tv_f_sq6hmm>#uf!qTXM~1|3jOF#PTqyh
zkh*V2Hsc;2JY}#RJqP(pR7$wSF;=Ld`H13yPa&BLK<&b(XEiUC+1c;&ZvBRvY^n^G
zPCivf&a+T0ly(@Vkh=^(egL>oQILh*H_wsVFR-+
zyFJtp&6#EF&0^GScoBkc-@b~7xz3(&`lzz9JQ#OC#bC&}P)*yQGgILGTZxz?N(LBQ
z&8z)L#`5yZ0QoVCOFWStkE}d)v!)UO94bDhjDw@2gTTFhw1nhiaQ-~G(gt%iWf(RP
zDjZ&dvr*|NvOsn8*^rze6+o_~0a$}~2X(X@*xq{d>oE$Myn-_p)H|_@e)Ky5TLP=l
z4sh-M*hy~Gh`kruZnET~jXP*(w})V9V3;y^jZlz*Z~jAlJGDC`mN?O%bipP%k>-
zQuM!ba4cHD_trl@AN?Z{qwbKwbrkc|ih+(28E_J0I3Pc~7sG<2_916kgXfq5#2_^l
zX)N&NO9ezF@p1sucwinC1Y8WtQPawWKp#^guQ?ln04D@E0P%B(oho=9Z0~c(pLkv}
zH-aM!M+&cfy?lLB6Av_Fn9^>s6hmG^CG>_)Qdn3>;3!5kA1k@ufF6x;xh~wUQx0Rw
zPGnk@QT6{@Kg?JUanmiqobe6f@&eQ#MHXxY8BarpMSL=t!$AqVmbmZx_wT{r^)R0E
z!Vd<6A);FWeUYYAQc|*|LcxS!yI6*6sM~e=P}LT$o-4R4M7%P{3&hnAb*3C30)S?#
zeZ{$y&
zyI}(y`QmnWz8i>RVGwk7qJsxA9^4k>iO@K7e*OB0F}w=F#ly|LWFC%5Yq(SZ705^d
z8es6l%n}Q8pDOatQQH!6deOG?5V{Z26R}GG2g4Wj91Nkcb8yaHY&~RWBD@iO6VH1P
zhXvZ!%_CbDS`)*Fo0ypAQ+rg3nhqxgF79I!tc9olgs$!lRNFd{EMtPkK(E^1x-#4W
zVuT)*cuR04NpoG4B91DtP=Wnm03%FhroCua5a;*fMHSoZBoaen&oj(c7Ekr_
zIMu|h104>&rG~EY^@zs`+|@ITi`a;Tidb2J&3(atk?R!(9AZ-*Kd#cTD)NSbfwUQj
zt=P~1{ok5@D<+MJhTJttI6oWM9?30eD79D&)9}h}jBF2MUV$5m5R4xVLq!v~f`x0U
zk$NGT2bocW`yH_3SBViE?&iY?tPybE-PuigMn@;-$^9TiU_ca+D=n;wezCT@PMlWJ
z(#>HZH(ddEjes;VM9UX@Rt#gAU*FvKhwwo#)9sa(mH7S)hY>@l%Z4z$O%A!w`@?GF
z%bubEjbjBggngK`B?3~aPA&tk{#avYzI-7z?XQ!bXA=$#0Z`C}yP&9GytAyf);~O9
z{tC!mm)T!U+9hsM;HSxV6pp@;U@ty<{C^iYftS*ma4X`5f>OkQj_Z#cF60`l0tYs4
z1;*Yy1137gwGP13IJtn4ape%Od
zgr!O6HoMLJCV~(TS{0B-P>p|Nfd0V^9;8W!AWyDb!GLt&YUxP|(wU(=&Itieq%$iR
z$8Axu@L3RFI9AgW*?w|r>d9``rGU;37#c%cy%g@6!toY!40Ip9aN%)tom^a892t*$
z6)nRF&~5dLI+Bc;fipu-7>n$r(aWlc9Vb&Mmc
z&FT_JVCeh(7bjkibP-X>EF2Jj7*mks4IBoun=;T}VlM93fc9V+8mOIC?UKx_tlYSW
z1LTCE{F(;*A<^EG)cv5@XZ3GBgp36^SPet@M>AW$E{JP*`YK>^;x9JDh&HH{56JkP
zaLr-iXVA;9lXl5#4qn(YW)`8=ZL#CMNIJy&>^3tZPo_vGk?T)JzO2JwJ%q|2(A);N
z&uwzJe05!LhtEb>m2t@iDGDn$imrrik|sKV7L{?$8ZYpjIW3WCgMb}ytsOdcY!yHn
z_TGDLcA6Yta>Wsfu#T(o!qqe?&Sl6{Euny=D>gg`+Pkr~<(8?sb!$BMYgjI)X)uzwn
zftu_#J-8R`GdcdiFM{Iw@ED-+xC-g$0WO_9)N8g1H+39<6ORlnvL;-7fLS}#Lk`5`
z;r;tP{&ZK&^vJ5J4zL{(Ba}^NDHUWFwE;2qF!VC4J9Mu@&Ev);YXf4j=GeqXX^0v*R)x&Lb>q)z!Y62z-Uh><6LLXH@
zKLfG(0QRy*#7QNhl)&0d9778XXToceR{l>nko7_md_0M5IR7BZ>zoY?8z(0i%nnRs
zu+ca@t!gfIl>qNTCWQATgp~aJc@ZjDTyk>1Z%}S=F$b_oH6*b*F#P0B)03lc348ewYAtN|?Uhg>Gnu4eR=hF!!Wo~anPr-!de%y`}$SJd<
z`qE;}3xA1;c1>S)uj`5XXk<#t1u)Ti{NQx%}$sfv0cZ;o=jLDM-pj0DzsM>U^tu
z9>#cWTy;UZ8#p9+!wOMWaj4z6d4}?L2?H#&Z@GV^*clWnQX*5
zVbo4*{1%+E!Z1gNzJDGCYOf6GVYwN#a`qSRiB{xzmJ1PY#mxsUavu&4
zTa%kgAkdE5h9-bXBHIdIEHVAS5>sAPwG_Po#RJ|dagWOQojUjeJq{Rc^EkUv%19{-o66zIhcJ$eCSUMPP!ansPcQ+R~?}aPK0L?Zg
zQb<<|!)4I@9s&wKhbUtP^(ycO#zrVOYOkFxK;Q8NDG-yFw+^iN>kU^(m?u*2D-TVO
zdze8W3otn9+)Lv^Z0BKV1QE@!5
zqXMF5ePPFdwsxQ`e=V6R!R6@`DENb+Q=Kd9|6
zBTXb`5&$jG-cl$~Z
z6<`9}4ib(GA$o)3L?nJJvvPA
zY2t=q2pag-6Q@pX2j5GNBN`Ggio1vDA(FGu$lm-k7tN6(iT5}`;R2snYx!#YEBdRl
zM3p$=cwY{W*hS9y`J@2B7^4>&sJ516C0vyd`BExC8E);qL>ut;Cs+wO3XprErI
zD;OA9DRi(MD@Sg_Rd7(!9lI@~8ljZqecarNb*mP!UA45^%r65uIeLOv(JEcss0_$~
zA%G>rz4WB%?15nWR`NKq8!DM#0ZkLK1}uHQo2F3&$V4+-yid~METN*1+o^ozypWx!
zDOh5%-_RFGHAa>Ka}6d2R!*=l@UA_vL9Y$SJ0~i$bHUC+0hz{YmiFeC*5JRPeP(rPY72lQOG@G<+w4bG&(&A
z=?#+*bP%l*6B8*EVr0uPYr^RJ_%o+l*pof`Xa*36xErn%bRceNppo?e)+a`55E&T2
zdvQSmMuvRJ_VaazAs<;PtXh|#(p0y|Z;(fM7R<(w}WGH=#)m}woPz~%k8X7*HB
z$deh@bUDbRy!vXYs%E#ooB9M-wg2@3aGKlxf;plz`pe4MUDzF$pEcVcpe-W=qj7Cm
z&ESJ=a1oHq>(G1uG8u)=zwz-F;+W90h^boR!sG#dAFF(pmMMGz(F$uR_T74=T)!z7{&z_AMD_$;ST(byWyQIpVwO!nf!bd$T4
zV8Gj*THXtYVOD|=lJvEUmz0LKIw0{7^Bd?4YiOJZQi!0#!L5)*Ruc?@ts|fT|zs#ie+QuCHIOVg4)zY5jzz+s|nYlov9m9T^#k?gsSTN~|#Ew->HC#gL}(
z*%ypAHtkzO(l#gAX~
zcTZGXNESgL>HiFrqkwInJrkmwk-A#IP>_(
z;7Yyh2+#CxWI`}K17-3)K5W_$agM-Cre24WkXPQ?6V%ke7
z+f+T!yuprqT~>L->{sPAyvG%i{#3(q&u?8z9eX_>A03Wr6r73KKjEJ`55QH_<=QZO
z^6vgyqdU%O0RaIjhX7>ydmgye5Y!@yl>!}^B|JH)$n9q#`}PS&c>5ru3z9vOM;j6xmz4w8lGl@tw{5pG&YyV%K~X?1}A=A(}+u
zJS~PaLJO1otz?D9jYI2tRBk&223V|P>j@7!ckA}*WbB{dezRUtr->2WtZEnGV>D~k
z>OyePyyb`u+kc;h2_vBSx~?s1Hf-42y@xHN7S=07T$rYB@#4^
zz9MV7_Z^?j)Lq
zO4z^GHtxCN#+?CZ;_^CZYCz5pld7n&{vS-l-nag%U@Xn}fYqq9Yq_s;p8!lMvLGlZ
zD1Lw{)TQO}!-V*sFOKgiR$-L27vi3Fi@=Bx#6F47MyOdDKP6#3T)Na%14GK8j?H{H
zw_WZP1cD`6wruGMNj|k-y&7E1Xq0=5pKfmx{_|J|1$UuJ6d}n#sDGF=f3xSKv#fUg
zU_ADDYU;|0BWC4e`YCtL+hXA>kte7a4#0r~5Tma9f9@gF*D{p?*#R3JHD*l4b!W-8
zka+?;0hA0azRQ!?G*5K7Nb5*bv%g@he|svTUz+ow!}L6A+T2hPdHF4{SBmQx3KA_*
z2uq&cL&`F;!>9=p9*-H)DxwH^Nj3l!U2>m9miBd1tQ4UDpN&0V7er}q0ngK
z5xss#J2VbsZf#vfZ{Y~1{D&1BSbMC5PvH$EU6^p_>=IIYGOx{>UMAi@A)KuaGKVB)
zQXd0hgrMG82fHr!CCF^UqD2>w-fa@wVhKp;E`bDLet5IdU(&c(xGzN00-xA-W)m&8
z7RoS)@(XC{f4{wz+UA6f;Bhqxjj|>HNnVURKde@`o$?bh?E!XnD;T<~5NxKQay-8@
zbJDI|JM2b3gnWDq|DlW{VIHJg@jVkGnc%Olor1TLl~d@h3+uo1~Vcfbt@KZ0>mE|P4Cdf3UjF0b5d{L#GEX9u7pk(OW_
zy&Aa}!qQ#v-F@4rdV6(wJ7_z_F@o#mGeBE~-IVN>C!;ch^g0JWV!W&%g#+if!r!xF
zm8faKB}Q-8?nj7GVN|dS5JmA^aFTyotp4UVI7BERA_EtEiRh|pY7f_e*y54NmTB^y
zYl&f&XKETM*)rIB1_V?Bn<&g62Xz;`1^zgbUfs*XFkBy)!{6Wg(2Wa%@%aUAg0>Wm
z!j}*V%-CXsWlv@ZiP6MR1J01>_YNKzzhWPc9W%xZ*Zlzl2Izt_e^k@I2mdSO7Ty&h
z<>O{Hf~Zxu$)^Yd+d=g|LUDwU@t?O7!M4-rxJ{StKGI#5+0*&ychX?)Au1w+chNVjPhJcn64j
zkK66mdj(oVT(l*Zm)?}0f_}v9!B7q&QE|=LO#d}&79#9dq{MgYbxPh`qIng4o3JNQ
zUNwmF@;up&mUqa=x#eNd@q#$Xw^>Kk;sk8_11=k%{bh6;iZ~#ZvppI)n*U
z>4tb>90yryP>a0$WN2tWd7(JbWA{KXn^((jrSbW+?g$zHRdaB8n>PI^`t$~YJ!G^g
zoPh?l7$sWR&hS8qx^iI
zdcrGL?*ZrFIVksD0sk#qPVk>?v1Z}I{PH~EWuOxDcroo~5Z-l~s7G`&ym``>o_+gX
zBt@*`1{b0a6J)^OFamp
z@ab;vrU(`={B_vgB<0rCtH_xPQi4oIBqX=fLycj??mYFA+-U8+H;k49h+_)rUtD1{HV~Yf+WhPioUsUQgLm9a3>d%Y7U-SbyBva4+G5$5T;p_K2A
zIlWFN%599oqN%NUCK|~^P`Q8X0c0)^)*4=>OOY`K!{(O|4*g?iSDf;Id*?`ICdnW=
zcKf#S^Vj}=Eo{3XHv-55>
z&UXz~G2LT<#BOs21Is~IsG3=VSnlfbt3W~qozYZK!4@V)%HEJ)sEq>uS3E>UBJLF6
z7$3=MwbgqBA`Orh1FsE3xqjT+E^GY=FHg?QE(;ELV)mCjh0u^8MSy8ZT~~@Z6e&`K
z`OjTXYn-uVa1$)y%2iwRfGCA6&HP6pfDpQ8;k21`N=@=+b>{sr#ZT+rOAnUZS<0_}
z?OIu1_!~#8)N}#W6Wd}K@;8$%XVa#lT}p2Y2`P%*jcoYnjn+SV1fB*47(A?5e;jy)JYjV@
zXLfehb{qX|!vk-~9;&
zoqx+sj||!m;IL!#5ZhHn9<|yKLLIBpW7oj?khaKV|8lpwvwp({i9~cch(k0m#h>4L
zLw)eSM%Aic{ev_W(oz8k9~rcV>`!-F$N(Mi4j$E!`+KEUeGt02-s4&I_C-}UFAop<
z_+fxgKiyvcr4kPfh*i4*L@G~;x^)W!*&yN!J+Q5^bleW>8yM!7I)GrB3|1sO5BeC|)YvLR2h&{#V
zIJ4X}Jl@^|I0PfA>z-$PHL#J==+do&$j)-Crz9772c@J@4BG}5|8E){^hfduMpC9eFkDJBG1k(^BT<%g3CZvZdG97-
z8@x7;m4PZ|&&$!dEa5?4y=qI+3agc~|5nGW65LCM3`_R59l!C$bC-yMHe9`yEP$H4^C*tKxZ;S_X)$kKzP$H(@EH!9qdFW&F!=HL@)<`W+Gs$C1IuSf
zxI0o?2d-XS)9&val7J&q6HeAriR^f-Q7EfjNv*fX6s88tDLv
zR=a-xOWE*>d_?eKEAppwyePE|jwG(%inlopnNIin^`GNSGp
zVV1ClM1_pd3B)BywcBgJR3Pb}hDZ>?l
znS4T&Q6cUyS+Yik2Ykkxt$WSPjdx5)lDh7X6kDwV0OEX{u_O@SveHB3r`m43WOtDjb4iSQssw<@y>S3*W0w#Jvc)In?V<2WYd=#nGe`chq
zmC=VINntPFd2L&>WlIwb6hL!#?bwlDO)TA>WT;5Q9>o$J{yok{t!}7oMql&+zTzvZ
zF0pgn!;FXBJGOg1`M34;#36w>bL+g&IRgHXo8|g%ak8>c_E!1YyU<$Io*A~30=IY
ze-F$w;Y^1N9B4^}kIV9>KFQz%S4JF1v)vg0i>kpNEESUX+N5B1kFmzj`f6_qu#)S*t=?nNu$T3cbmA|J~`!h`V3i9(_FNkUEnoO@<`SM#;SO7
zu-OYx#Smux@<@Zp=ot6K(lv3d(U#BTFFpeKYjaIQ$@?uW7pBgffK~@4^+9&D-H}CzBVzK9|nB0@x~x~`$n5j6HBK|2}_+hE;%YO%4=lC
zm~qZ7k7teK+|ma~j6+kW9aYSsXf&2%9r3wkk9$*<3W(O4%A%vu8Ws59JCLDy?L$BA
z2MSIp?K8G>lRS1trni1Ht56XG?lN)1Hez5nga)q*XKLTnj}L%@K+kl`N6bnp1eWR~
zGh$SQ(g}NxUz%4v=3{kJb-}F&q?yN%QJ)4&Y8n#mJ0srRyv}b`4T)~D{f67wFzU}kDVf&o
z1klggyT{XmVEvEekB6qz?`9ztaCJJF>O3ydJva4Up4QW+-?EeAe+?rNsZplCLjsr|
zq6vkE;40kq&I4faIyTPbpY!V4*utOQRH&t+IDB~EftP1d#Zy=y<1WGb0}42I!RQbgp^xZM9~0akUv4e`#M0U1YKU0fbD==6{{
z%Ai-5|2t5DdO|QT+t)Qm`1R`ruFQ$K<;#S(5#E;$hAwpmBhBsgs*=tZQkN+c_uTl?
zUrtns%k_GG=-BPZ+Y7CZ1q?hk?)JVLce`J1v1H=ni7jJ_EOIOX6VS|gQ)){5rGX84
z_pjMdUoYFx#82B$jX{UlucBj-(?1s$8!#!AQt=|DuG*m-0ZE6$<
zaPcb=gq0A7L&y8XCWpJ6Q3;AnVSL6cE>-FBjzra*;w~eK
z_Iu0J!87oqva8pRrk{scz04O#KB>-cmhC09@R|0
z;4#t8!s7Vmh0cH&u-7ueRUn67;R9SmOZUiWC4)8qAdl0ER0>7!e5ryvPoDczfDYM`
zU`tA1uH82g$z^@d>`LmlgT&>U9}RWc4-1x
z8AKCB>1#E)u;q=RX;A+1{fnA9bd4)IcG{VIjtC+%qeV(sg0&
zBBczmO;ZUPi>=mf_0zxNZr=3mnEo;UvuZ6L9vbNb#bJ?hbF9!s-XgBD5ttgcFezMFU28r)-nD?%cU#u=Elu~?p
z)ru917*Lpviam${$LTHg`zO5a+SGhK+8U0HVeQ_46Q{?f5J0q(T~oWL@qQC%!WC#(%Khwh!#%kbTQm6mj&(5B&%w=lkU@)OaUVeb_}
z3WoVl_&)kDXvmPGN4MZ;Cci1hvh;m1XhOc~+P3A^%ds{N4y$;p5dmQ7Hj-1rw`oiR
z5v;+lmLF6-a0c;fln*eztt0nmah_yPs*QNmcW35hSK+C$RCf_sHYX>`4O{ixS{<(5
z+)b86@0gl5xLp4B#O1Pp)w(niTojI*xB?V2fv(K47|9uy%ccn<#IW-6U>05CQ*NzG-DL(^jS3{r
zm*zwj=JOyPT#R7G@#?zzwms5n2R1Rk->Ts^ggiQq-<
z?q7-@4YJExgtRP&cbOhAF*wa6Z717a)DTSh^BUIY&0dXy7J@`ZSQ*)iJoWB3yff-?t
zQ>jHPi0KD7INYfIk(q9$=+xRqx;6(~%-dg%%?s6?>I6BI^L*r2Y~Oxe6I9v7q=1E^
z)|4^W=kSd9o-`fW=cso|aup*F`c{iy1}Gt64S-BK`WDBF%gcZK<(2#5VsS-$$Yss1
zKvrvwpA$fB+IY7MzAp%&I>R`WE#xi`>6~yfoBphJjRRp}Wi%Z}Z^uRV6R8DB;V{1U
zKBmFsuznF=HU{e!qQ)=JNqA{qfv2`J@7eX@;mW-!3QKunWq|pN2I#yfNzczX)+G4U
zsVW-0;jfp0)61@m^3k2@c_1NpvB{sNPXa
zKNe$*9^0o<)%}VXD8V2DKw)lLyS6tsu33o!$f`JD;$4AHZEKISCcMe)R8B!W9kuri
zF?H|#Q#(W|5l}(GUWYn^rmWtuVF?@=(N^#a)u2EI1&kXlvX=s8LlYVaePlXbGeLxr
z*cpxP=4%B?i#S9>f8;`WK1YnN>U)sim0uzvq6pwZ-V9`|GM46b8*DYUH238kiANOQ
zg-NmYSdt}%J0w*X18RcLtNj<8E#*_6d-S^
zPj#Mx1n$%+5*Y#hFY5UGhc~t9VfVD*Qr}Th|1m8&;oB`Cge)#;0o9b&6h!9yoKWS^
zNBEW%jG8;rpfDw>IT&OaH}hV*rCxj15av^O?V85V5zG4#c!^XujJ*&T?2+gCC
zUxV;>=r}3_cA3rRpo#fsQx`w-fQ|jC(>sfmD&@n!rq^D=cF&^p)wbnodGa3%Ly&;T
zo+AQd#FK13@N`Ag^yo>@ToxygBcyw2Zp^jbrfWU7xRKE%6b=8-wrY5V-K)EbH<-?U
z9H#t)EU*CT!fNbEC0D*MuTbVNpp1rII6;dxZK^DbJ%G2VCM!HedrCOcZqCfW7peAkXFn)v8k%<-vo3Jn@Ws+l1gwgp$yt}TwPBZ7n`Ttq&j-%y{JneYQhHc*
z=0r4`@!pnnrlDHYZG~O;-&ux~DF$PCOsn;oZ`Azw96yOLrWSSgG%17#cAUGjMLDiL
zv8F2(o#qzr+(|MwPNMs%0)@J5=gtBm`g`=4Y!VW4<<>3rq?MMOQvbU4*06Hi6@yQ7Vs(2{An&taFt}k1K?%j9bk|w7ua%jwq
z+UNbrUYZhq8y8%Pa&PbCpYqYx${bqv$;|ffVjlV%nwl7#?ZroKNO1`Js3rH@nFRn7
zQ%#n67DQPfYFS*jbZ;;fJdsQTuk3FXrD1@QP$z&}-*f(T51@BRbgEgnmk>jaVB>at
zJYn^2VL(>p5rju-|7foH>1R}G(@%(DBF0d5O*2_Gc@(p(nwH`#n>KEIW5$0*p(IpI
zTPutc131nr7Z&$ULc5Qd~{^yJ~aQED644X?Jid)?)i@ME)|p6
zISL%njcvQ^%V4d|`BevYk!sO(?`G78hOh*!#^@;zD&Koggu
z_s!BGE>RMXa&}$>5H|I0r~gF?2dS-8obo_4Y+xTdJ6Iz-{6+(tBcdYqpAMj;q}3$(@17rVgZ$;XdB+^
z$xT?l7c3xDd5$O2k5ZGGGM8ZxLV)m-nd8jBv^q2)G8m)n(X^v|tZ9(MooI6B6V0at
zQgRfg?Hdy{lP%ITk4O$n8ylM)cJCCfu!A1+Yrc-AySmx7uj4)WAn2#E5gyqEKQH;<
zyooIV$oL8wXypS~+U5@Z5+>2d(MX?@8qn8rxFhl)>1wD@JH1~#21?#;P^;Rx&tGH?
zXZ~56labo=PiX40S=AIrT}k-ifXhXyfO^PF1^F>7#@3W}FKay}^C3&ndhdffKS2q?(L2|Jz7K#PeNgr6i5s&LWXFr<`n
zs{*r%43d|xN>FCL&Fa-#dbShE1-^@Ocmc@#LS*ywZ{O5H6AYNTD(L3s#*qo@U2(H-
z)S+x%mxgFnWRcdCQ>o_99?#uif7-nyAPecTEBSYS^*0*HrvldGHeP+IEfmD5E#$-m
zkc*2}&&^xoO5yG2qv1@ZM%gA95uH%S^?PJxGG3i{oDS&deelXK+|_@Hqt>LKIB{YW
z9Tq}W95_du32<$kgg)@VZ91Ixlp26E95ErQ*;$FwQa^<_Y%rgRhwU^ZSb6
z$rd@08T{yl1f9;n5ri-?)JVPJC*Js$_#fF)`CWzv1oOiXS{bXJW=+);%v-#3<#UKC
z@O*rHz}&I{ClFQ
zG)O6c1G-3iVVy6nJl8hSbCLED!cGa<;ofkM3v#-t$Q&^PLCdiK_JEQ`3!kWS)gAMl
zCAP%@2wq4_Tq2gn+jqJF@Uei+)vEAlk0=G#WN!-wv``Izf~G>Fq4PmJ8Twz~Sg8$0
zNETXZ1sYO=p7xI^A=s)2%)=+2ZOrQ1xI<1v$B_%2nDqoIeoilEJaqG}ZyY|xzI{kN
zXOA{x+Grt9-jU3ZKjjM_OvZH>aDZb+Z!Mm$GbJR$*5_#@WZBHeI#MHbE{+eg*iOal
zr8+H6`|z449;~O)(8C5`nw|03BLfr#(}dHjiEs%KXFda%do8aL5Xd$dA0O-e
z)%#C78ThkQ$&!l^#(<{ri%P0@YCNVVv(Y>du8DjKXtStsgZti^HjRhKpX%HDyG1*6
z7%HS5KhE0nxPk+sG@?TOlL2?A8yKYNPN(GrUeb7LRjPF%fy4q&9uaFNqdG^tpEdGy
zS%u22KnFJgPMNa%JWJp_68mhX@0W~>F&M6A
zUfRaFI?Cu(WE%>IO*AcI^d>1i9y#-AM;kN)b7-6qXWxWeh=Ol@wgu9lXsofC13G!Q
zZ6K3=-ZHlG5|@m>e>TP1;~YG5@dF(`zjGNk?yxh~Ti#)Z50Ao8>|Eps2lV?b$KR{B
z;A^4zv%kGBpEbAlo5K9uOV_WjJR7xl@6vamM_C@Zb;0XNS}jAbe)mRC
zb(GHE`cShc>s^bQ7M#VJj!H`a^L?WqGYb80)B^@xc*!Hq%vzAIKw%d4l!78nO-FR4
zt#e9Oga#?{@R*Xl{r&sleX}=g+}M^qxtz?52_P}e>dBb#6q5IH(4`gD*@m$*B3&S8d#{JGYrh@L5}T+81%Rt>7!L*gADpCX9YKYf1H
zn;N3%v0GqV&H%kycnZXixZ5@|F}7_TlsH^R{%xU{W}_+dE!z>@IgvCvgTKRIlWim<4r@YmvUExd+0m_H(`(QVAW7i0Dq!Lx3)n@Md$=
zH39|?t-Fg$eFiKww}D1q9_11g)T=k2=x(6(>Y8(;J6^;E*LS2(8yD8p#Ka`Bc>u6I
zM<2VZBT;cYVZAXXr!zOSt6I5o`1|x@>w1$+fY1zb{_bB2FrOPI40*+{t?Xyb&Hm`+
znQi#_4F6UrGMtzs%K0a3^fd3=GGOzi5As@pLQz_Vv6J%EdfYaA_q48%
z^@$TY@>&=CDv1=^HSFnz7Ue5cXyehbf;Vrf)?a^F=bfpFb4K?zOtOtzanWypH)+~A
z>L7Ch0E+B}qF>4fAw?r)iB3JblSjSQu2oe{ki{kLjmplb3M9Xj9{Y26_Uq!uy*x%{
zea!kE`Y!iIq`+~Ap5r6zkJq)fJDc)%`BuEyGjqNzcPm;i^VqZSm1kXQ9M-xIUKwg;
zYt#wc#X@(-QekTuA(s*`vjAB^!xwKxjHhE@D)Fsdw`H7hi3n*O0DTt`R_A-obK5-c
z%wKVHo$$%j`M~ZcxgU<7j7|L7{Y-eLragFCoH|}%*4~O`
zYPoqlOnkwCz+46~`%bUi9Io>s9L78UocOMNhHRSXBY;aw4bQ-#qg8u9Nm3$0y$ido++WS()EI
zxMZ3JEtI+KAI(Rj4`G;tF!z&QXUxVd^IEIDpQB!B#PtBHfxv|%|INo|4}*>LDq
zTfeps=h;MnY8=h|0LH!&Ax%uPJ}a`@#$LR*coPz{)4Q6{UpO>)vY{Gcw(HEA#eYPl
zaTTMCFK2IsY*U$Voe{o5&ziWL-7`9?Z(ERH442ncMv^@Zum}soz)co24|dLKPqI1v
zA6&G5Wm=_aNT2G`2E79ZPh9hurnvjCVVhFS6%+ajduwhDQI)85BPQBKQ
zthTYwv!+I!oEWt`Hu1rm-m4YODPGeXhtwv59N}9Z0LN8ie+^-MoigE3W4nT{ZhRr6
zt%QnOyLPS89K~64fHFOA@>nG*@k;Iz}a|-W2H+EA8yR|>D;x9#D|l5ZyIi1qqtVa
zeF5Vo{aN-1w!D^6)bt4ui?m4W#4AZsTM!Y7n3`Zs>}1zl0i;H$6ZdkAVsM2-UDF*A
zr`A`>vW?dzu97_htDulr@>VE{&9HW^_$*Q*Hr_RS*Z;HtTDQAo)v6nIRUfo{n3HuZ
zBG>DCYib{oG(Oq+Xp2W5dXYVHTB|n>oID1yoDtHiC|b35Z#}Xn#RU8U=4Dq$?9QTV
zBg&K;=cRcWl+>Wqr{&dNhAWK@cMG5BIcG(7t5{|+Ws4`Q5Km>zhIn`sFo1Ci`}c~m)Q}YO+Ez?xzC)Rm+sb42
z?k8^J-=#Nf&>-R+We`X*;C^_!TK=Bx`#KLsMF7=*o(r}OVc7GahI6tqGq;C@rLVnS
zj719_sUtMlqV>OS6SmT0X!09y${Kc>|E|EGLHFB)e*|r!=<1C0k?25cSIA3`9$pjb>Dn7rW#lP!{gaGoV@p+Cb^{qfhKcApW4f(6`e
zQ`v+K@Req@uPzAWH-C1dDK4kT{htg%M+K05J6h&!O@?1c8WuONpUOmj<4!dcGA*#No$9*|vbc#PRwlrwmxEq~J;))wHza<(kaTEu`WkP9x
zVvygL#J}-(!U6hvg)qDs$!xJ7f)fJYeC;|KjSr973zA~<_rN*}SutWJM@!;2NbD`U
z*shkAg4}rjk>9d1O!;tB6k4_$dA8H+_A-IMAu&ISd-r!vJaf%3Fe&8zgw|4m7m|JI
z)~#+I(jE`&)VO}rrq*=B6uXJTGwe|tv3!uuZAFKSkLd*r=v3t0xjFYn^B<8<$fKYu
zOK^JkNId-;;h>C_W~sSXj^_f0?0{p>80T$1Dq5}}tK9m>)TJCcbw)BTk+kZrZgVC0IB*Pi=iH4OtDaW;(U<5WwioxU_zuT%_tTw5P8+zEKu3~B
zcsHMLCZi67sTo~2QB+g@e9k_D0MX-2oyOr=k$oC(@yp%M=@z5O=pXvV9hU5
zL7w!D2@WwFHgxFa8SC1-+k0}euySfsaHujrM(nd{M!g~TEs3lzJw;Y|_8NeA`3!y!-?2-JKn{zR
zts9N`3n&J&0s+xuMo+IxMbvfDqz`uA4*`@*++5TDxk4vh&ktgJ$mE2Z;Ho8=eJ&vX
zK}{%AJJ?(QtO=(O%cS_TQzN@|+x=)oxPLAyxblXy5f9t8bB$&G#v4#GiP4EA(1#DF
z{19QrU-L@I0bG%Poyox;3zsY05dN_+FduAovxfw#W(r)TYLxuu-
zEQXgmI_@Dy=o2lo|
zr&r*Er_7@iYTqrf#8E~fu!%@e=Xczj8ZGay@(l+AR|IaTG&3J|z%g_q@@?XHPBsaS
zQ%^0b`c*;GU3HF43@Uwh9_z&n6rkyen~l9$?O^ii{=1;ZwYLH$2d=~AXpRxvV@lvD
zp`sGa#-rlB{0|bs%Rs+r3JsK5#vBK0`G3c%URtW=Ge6if&FBMI+zHLQH!j2q*T4mn
zMOi>sbAH7iI@IhlACUwaRUaDb=L~)WjC&s&*=gRdYp%wYJsQqtqzlkZ*r9eh>EmHx
zSOx4)SP!t|-pL6pjJd3h@<^DyHCXiY(Ar}rez7ssx}x28a-x=!Lmarnej;2x|k+*+>5|5dZ1X!*F)fq`uQ%*YQ493)3=#oJZHz
zI##0WiTeKj#4hKn#0(5o2zmha`H@ZWAab>YiVrDPUT)pJdtaM5Vp-ty>O>J)DacI;
ztoApDbZh}P8E*lR3BnwoJozuB$FA}``{s;I2qOc+Io5VoMY*N{0m)!^{lH#RVauo;WBgf@K5`|S-H^~JL1E@x~dWGT&KSKvxG8oH=z
zvrz_gc-waE^41+URrV7NoTEUTrjgxtJvvm?dh<
z&Zz7_SeKB!7DkNw@B@1JFsr)sjwryWaztpuJr~?Y^p(nfiy6M9_K#(WNEz=mDZ(05u_v)Rfoc6%rbH5qXK0wg^V0)Pj(CZeAg2DJw@b
zNdrnF;{%4_QhJ!&T`|eB^J>^IX{nH
zAf^~lq&T$+-*}42D#K`cAZ`2kG^@R|XTZ`0{9=>ME9674QGlc?zXGqE%)ca~!<|cvGhAw3#pGas;e$nzZMlgVmk!6C<
z23KxjB7Kw;b=-C2BIRIIv?ei64bZ*d%GhK{$PGsEa53R~0rztOFjyEXA;@7%?Ug-~Kx5-$aHYIcJRqcf#@4wwObxgaI}WhcFIeOt(ytxx+mZ`EpD
z%1{US_RB06XjqPPRPYM{svm~+urLD(;AVkN6+t+7j`=TZFR#R%uzK>gLkbfHu#Ozb
z?_fx0zOd<%2j@_X7%p+t&Owp$5X{QDl0Z=IPBU5ct2ZUD^0|08mLN!`C!8Gk)P(5&j=@TrN-CCLOlm={PyF5kSlg#0Tmkw0?Vy=0ngT>MjrHJS&pKU5`7)cT&C
zhCtnt2W9#Qh)I_u9SUh;)E^<{=FMFl9JcJVw#->U1DU67DN*7A&0IRbtMld6ruMP#
zjnUUhL<3T5Lis2IVS=Ld(K9_)XkrtS2et^*5C;HoO5pf_pg@k)h|kWWgkme5)j?@!
zw&oQG?eGF_m$|3uQY*?wTfxKpcd
zpXQ)$2L>WBbm7@SU1Az5TCR9gWQlr9cDSFN5$@OTo~oKpOCk*CFoJYDq0zrI}iQ!URsP2+yAvW29Zg
zVsd%b(iDp916Ztb~mw6=RywV_l%i#}~L15m(F1
zfIfEYKkg-sm)6=799Dt}b>(OM(Ql&)J>hHJaXVw^#Z<&lK__OD7385pmSj#-ponZc
zXHf)6+)T|1i?p3sR;|v*K!i5(vY{DLGLwJ|rORPT!UZdzQgx!##{urYE!#mwiqQc?
ztRBzd;1D+0cD!qem}rO|#4DYdrKFZnc|qJ=R_uBH(#SzzHeaAp#IEL|0yv!^0Lnk32~;Wl-2Y+
zj5b!Q&S3hIa#2v0AOIaqo?(taL(>dG-7wRYxhYZ^`6NIKI^5f_f+ZWW$&|;Prt!fm
zLCBm}1S9N{ARE#$@#NT%C>J$a^=BTON8^nW80snHQx2O7)BbN@t*EhR`X+%r4*mo{5}l`C3TI~MO-%1U*iE?fR4kPMoQ%{b)WKY
zF=JPG`!Jc2#26-Wnfd6^Rldu06+}eZq3+6-?P|_#Bu6uorN=xfP*P{~x
zVp9u@o7@x6hEI^nlfK;z-~GtbDBJ(mC^M=*pF-+6urD({1`72+2;?uu?R`@MOa{`x
z$=M3uDM`cSE{O=88wU@$oGyHtiN9xljy%Tl*364*5KFTMj4bfLg%B{^rXd^_Qfdnp
z>*<)(nHY8hzNlc~!Y^o-^fy7HkgH3@f>NHlH_$Pu(|AZ?P#P`z&@V?LV?fuZRmJQu
zTM)Nt64?Pb-1Ay?jSh1PawH>PN_$3c_m(XPiHb|H#t7}lTHm5r#O-wfF`<#Y9Posm-
z3*;#P7-8^1`=WG*2X_*{O67?Fj{|2$BP&xKjgb=hTpd1-7ExjnQ8T#zuFdJcGN(xl
zL#}~}mByb})SLvlvT9o+N?<*^ht0284@Oc)iDinSn*KuTC8W01Oo6$1Wca;#G{&O7
z+f0m~Pi?~;JkdA%K1&;LCP%}DK&Cq#F4=*l;)VHJl9FRobu4O1OMnN749RaYvj@jk
z5zB9dnb2}AettwsDSt$nWop#8Rl$bTJHW=K0KBsMNw2u|my5Qg0-FK>SFO{$YFhun
zd(>PC6g4%GqBTBq-gJ^x=p00(`c@A<%kzp0^1QNOY@$z=0K3=kV3H_-NES{(^ZiD^XD7z
z$)zr48f9YGbOsU{-!v$J4Hn%u6A}g2)B&lZK;aZTwT+e
zv`t>+Sn15H^o4Gz+Ll6uTD@kCQ}LVJ69n5IZ(rMwk!@y1zqu&p!4ZFC^lRO``2zCy
z!vPjsK&GCsZww0rD67Sod#x-V?_rZfC^PnA%%OnHY8hQU66$2Kdmh)GJ^YYM_Qr#9};!Ng!2R1aWw#Hc4g8op)AexAe>&I#~&3AwRu
zMxZRY1%T@%Xv4=huIIqZhV8E>_JyRP==bbdb%qAgK71=`y30oTbnjL!r&>(c7*mHi
z)c*x}-ZlAMC1N@w+GJ!=Q*GN3np1&jD+6GfrEJ8huR+jm7OMbnO#<%1Kok{_1}Dj2
zY9inXG+2rckAb>(q|_6q4CTY|y0=Vi+URq{rAyrjLt!n=shCzUtrHD!Of7|bWNNdP
z7toU;uem(0=I!YonV;(NlnxqH=5+}?#x?D<)i9^UOQ%s_%3L|6FC?8O3#(X#SRo8|$O2Ds?xMzlz6jF)v^xBk4d_)_MY^5oltu4hE`
zbw2#glOnnp9bAOpo-f4cT6}uNMV@t}9UrO~+o-64XMR|}X3cr-*rOc>IYZ3TGrhTr
zZgt-6FFkvBFg5Q@)Q^~78A!Zsiao6u!;6@yb>UFQZ|1&QWWeT=vZRU1u(!iPfChpo
z!5xPWug<>RjK^paOi!bkWsVYv#-*FK!KI26HBB>6gYmNK`i&b|U$oin^-!G6_>hmB
z#`0F}+6&DF4WyWjZ-biX(V>eNys*J}UQ>=8S&hE(NH-H580>C%Eztj|*N2dQOUsw;urVGj^
zBA`n3>PGagEGqfW;e#864!`8!&WPfqS#2T6n}ed;Y{$$AUyqHN3)CoKX;)@e5bsw(
z1lU*SjCh6sZf1oJ%y9p>8SLgefGZZcV+HCCIuTJRk(LMe58AH-3v>a
z=8nYvO7n0WRWPAyd~SW!;@dgRq$9^pof~mL=}Hq*hVhd$vB|7}B|3X~it{A(hd8NP
z?gt+8@Ws~maMh-|(uSs6x^WhSfUf8O5THth+Cd`u@&ybtE28x!;8O$(j^JF4Y<@pF
zdRyL!Z-#7bNCu)YuZ!!XFv
zi+8~zov3>Owx^2rR?yOE
zaDgRNhhsTUcr7lVr@8aKFki-ddU=%xr7g|ZpkpdnsE|^+hM;*CkDT5yLKoj5*3fhz
z==hD}Gv7lM!r(<8pSf?@vYtLo>Wx7;AoVwx8ohZK4JSO+mXx9VKtogeyewDx?pEv$
z{tV-~-Dom{*-0SYlYE7ZGVOyLcR!g+c|)X_&*tl}YuU6YcZkpjcSa7Oh0=J990$?d
z3CMQ{Sg9ZWGWQ?!#FmCGZp6!Yr+2(1y}RG#`1xngwvJg;=B^PW)|a#`I+eU;_e9%2
zdrd)E?5zuZ%81;9y5AeNRDD06Iic$BS8PwUEMGY^{Tc+MGm!?C9Es?q5!r_4Z|Jh~
zcR&86@plaM<=C7!)r+ls{pTg^-ZQr^)k4_lYZW5r_ARQPY*^#ZPaYTO@SZ(G^inGL
z_>o#ePQmB%%)-C)=Sj$GA-Be?2;nWgeRkGj<*HSWUge-FpbA7@u`*Z%?QHpH?ksZboJ9Q$|qM_CKFA
zr{(WYTBA49A`qn*FwRFFfC(Do^%c}k9y{huJ@>E-k*p8Mhn&0UED(5TavKl=l7$X09thnv6eV|cj$X8-qf&w5u%v%hpsu*dNJb4P5?M>J90~0UxP3BO5d&2i
zjEKx9(5plxYI3Y7N5Z(ID_h=
z)7~IXvce=?A@%YF?qWJ>Es$j`oMNW(0u4OLvGF$R2aZzlbL&=Mtf*#HEf?Ff38l2Wu6WqB6OVS`*wWU
z?m~J@y?@yeh&AfP^#=_TQ$T&I#Eh|Rk*5AS#p1JYb-n+3ZeP5R*b8(0cq-s{mXsFhexZ3YIV``G)ivniyh&je$xO3UZ&I#r^$tNcY+k2RKO&rMSR@kR?
zR=M9FsMU=o-+tpobRY$3yoJm>c(7s2M)3dj9GoPE%r8Q(ePW+^DZb07rsckw24)PH
z`(-fpm%@4~@8hQ9O*J
z->tq_XwzL2s4lt!-(kjHnt=}LRNR6UZP2GLAowcOc=sn2-;e?InexZ
z?gFoXCFR}cA1*V%u&dSXs{^e1=d-WBUB!FDt)G6m^P=GK
zfkm#CE6@`u#~Mto^gZj_)oXSCK6z_KzoganCqJY#xv;!^
z!^0?<80>T+rE=@WS{#V5TpL`j+W_0|G_3Qn`#v@aUg`5pA)e1J-J0lLN|%s
z{H^D)wGQ;=sL2BhIHXuP-O`{{V=+%$-9;l8)$O0Sm<{ICb(-ZgUiRCzRR2(61?15J
z0ws5E2hHg0rz^fw8vi?|XX~d!SRF;=AnZlInyNVfv=j1#!6NG0>vQG0WgjhVO@82`
zKxh>W8!E33lIJ#}5|Kf$K#$t_^DGu4BS(zUVi|tgrda++V0Lr5P8NOXh4S7CH`!R+
z$ftnZw-}v`Now}6IDuo%Dg*f@$;^VMr;wmanVehz>PHo5M*7Zr`(ivENA5`r1&g6?
zXiknlS%U3yc&enMZ40alB)+yBu*VA|o9J>x*R#vEeue$1N6eV6@1aDSay
zaqaG=b!`HT>+_%bSPnMxZ}r%Za18J#eut<;c!EogxqElb$;w>sK{oZ@mt1CLrhO!|
zIwJL7@XQQwBTGe^JqLQ>I;Iw6r<#mQ?iXou@=k}?mu^fD`nEXWZ7|4u@|&p)h2
z;DIWT<7M#UuXE!kP4XRac20Afy;_YtVM6b!n2Qgl|Dv11ORLG3L;uwC{->T5QRiqV
z3ToM~kgt#h$_^Guab43#U)^k4zrD7v`{O_>vo2H&7o3_C$wnKWX__M^Dx4wcPA=CT
zxA~w84geBPfRY7xHEz_%Jk=+Iz*cwI945>8@Cpx*5Ktp;je9yS-*L*XVpbqIJL1~6
z(i3{^?bs=;Q{%>~h6U_<*C7SQpXrxa_Y-=s-v*Q&i9N=)K)=;G3NVJ7t)^Z;az2^9fUPhV`@^uD8dH{PD`tU7f}Vc*m<
z%Gy*@T#OL(GzPa}#7jTc6RWL)%=lzT*zfNcnHD{h!OW@ogL|w3h}yGY+~z?tcx*
zOp*wJd6qUT2qNvhWs9`$k6VAB4tsLeqatv83?PeXxnj+=V~5x&1G111m(!QJa<8kH
z4<8wqF_;9zr`puuKDyCGvB_6#gDEwldJjqahX?5(UtUR4`&&m{<6MgPY5)G|Q
z#Jc$?Ngf#mx1OH%(gh&@;K(RZm8yEd9{AROe5iz|AfyJvp0T;qV+KrQD+aR3Ym(D4
zg)?x46rWVmc+AL<0cfCb$Dmt8p>MlK^xtSBtbi*dndjPas~@zwg?-%af!K2DxB
zki_R9Mj)lW=GN*qV9Ri7nhH%v5M0(6J$-oWEDR?!cHg?&t3bFK`NTBpaew;J@bKNC
z`|2&EVZ
zfRTtuKjB)!Ca(MtkgEQu&QU~AO!iFlj$HhvqC?SArR3IP5Dn1JDxrlzK_mAM*)YJi
zH%mxpN&+G`fU3haScBh=-q-J~PwkAJwT-3!3MqXGO(WNJ+uprD5++QeBBJ2jl;YdD
z=BS7oIGZCd8fM;r7x>`538lpGiWT=PU$v?m6;zyc_`BDsseQ6?Y`6}tb-B4Tr&7^r
zaxEgpaS+u3mAC}MG_Mgcvny_CIXjTXjb7%3EYO&yp`p;i2D$&ETb#c8W*dQ=;Nyg*
zVic6!APV&6k29x`nboTzVFlUoI}V|
zRk8@^ZEs6cLVyAvmrXimJk!N!K~|@;nb#SXcgw-VR^0~NOPT&%1pt$7!&dKmw_(j1
zpqm0DCpcu%@8hI_y8ZGD*5D|W|6TVM2C|6Iz7QS)xR8^@f5-37UK0#JB_}owPck07
z;M%M6Fqg3T!R33V9RL^yf4_j|!jz2EVFWvk!ivDaKKZ8mEZe^Z+1SK1GAPHiB4Rz5
z-Mq!;85v6m0LWe+8Lb^(hzf
zwp;#SY(RJ#HOB#nfO1skrA9t+b;HhHMM5CWI(3x$gVsyUCw)GKe2$A6&-z&dd0mM&
zrl1(=yK;O_;CwmLFcc1!FPkALk!il}SPOJp_SK_hMP{#v{xU$Z=4bJ~Q76RnsbzkV#2KfTn-jB{|UwkPxng0==F7Dt(eq15VkYaO
zUsi~{f|o0?K#`KkBfm5h94mwc^0P7egKlp!jDOQxY0SD;mQx^qZ705ivW4mgY0d
z_J9_)J9hChM3TgzpWUvU^_0vLpPnkuaW7)3CEGE`8ex<#xQ`=xv=}!s?t`!v@RJsC
zIj~eEs{8$Avn7G+@bmZz(#VQp0Hjo9v@4nYk}32T-Fl-jZ}5i&q`92$QMqRad~QV{
z0Y!+=t_Z?aE+y)g3$^=SyLwg1De7};YiqS3S}u#}1EEz;>L6Ge0n-=?hxgw#``u)2
z(uH;!_9fA!+J@;XU%D`@CO;N9^khUnmze)32Ij@L9^R8$Mj}^j4oW(|SW2J1fiud&
zE@)g3U5Wuq*?(kZF+;wwNo41<}KUke8I!?wBKgM3nLgCutij9|-mlA>(o+$IZp2Z@%?pm*$6J}Cs7Et&We;yPy
zmSO?z%dFt!Q<#)Ve@8*dMwc^jLmLgf_0#y93KgU!SY7!sBZFPaqO{d}2R|U_*t23m
zCQL}yWt)Js91DTvX}9;bF{`jbwr1M8LXjo!0ZcF+8LfE#lE8DA83_$JQr~GjUOS+;
zsYyHiIyzajr>fsh(ZLR-1@9&Vu32N56*$nq0I-wVoBu`HUBEzq0Oe`RxSZUdDNQBu
zlauSBMT>|S)GfD1By!%i^dMhT!)4w~#%-e6LoYZ-1C5o^OXhs5#B-Nb!89*^VvAde
z)Wa%|FQkemge?MJbz@%-?P%*K5$`&=k+OqRCAs<-VAU?JR_kU|CRQ
zmOaRBG;Y_JxOg7AYlL6Kh2gJUxF?aBudDug(<%2H+rKUku4HSGg7GpEG?gi5a&xkj
zyr|IPjaH1WqajkMLghQi0SPW%=O5SQx86w5C)0XO8Nj@&@0k#!0JV(Zf
zzu*FKy!!dxdc*B^rrW#j%;(^KpfZrYms`Vle}k53iTCfX4|%wf#HhyFDi^qmFS=18l3Zw_I{8
z-mpV|FJ6(>iy(7fQ@_rhQ+~iL5;cP1%4r8Pgm|N6bBa(V