From b7755d9d452f59494b3071e95df178bf1fd6246b Mon Sep 17 00:00:00 2001 From: Ben Caldwell Date: Wed, 7 Feb 2024 13:56:02 -0600 Subject: [PATCH] Migrated ViCaR out of VyZX, added build system separated examples. --- .github/workflows/coq-action.yml | 30 ++ .gitignore | 162 +++++++ .lia.cache | Bin 0 -> 524302 bytes .vscode/settings.json | 15 + Makefile | 31 ++ README.md | 44 ++ ViCaR/Classes/BraidedMonoidal.v | 20 + ViCaR/Classes/Category.v | 80 ++++ ViCaR/Classes/CategoryTypeclass.v | 9 + ViCaR/Classes/CompactClosed.v | 28 ++ ViCaR/Classes/Dagger.v | 22 + ViCaR/Classes/DaggerBraidedMonoidal.v | 14 + ViCaR/Classes/DaggerMonoidal.v | 28 ++ ViCaR/Classes/DaggerSymmetricMonoidal.v | 16 + ViCaR/Classes/GeneralLemmas.v | 37 ++ ViCaR/Classes/Monoidal.v | 77 ++++ ViCaR/Classes/SymmetricMonoidal.v | 11 + ViCaR/dune | 4 + _CoqProject | 2 + coq-vicar.opam | 33 ++ dune-project | 21 + examples/ZXExample.v | 578 ++++++++++++++++++++++++ examples/dune | 3 + 23 files changed, 1265 insertions(+) create mode 100644 .github/workflows/coq-action.yml create mode 100644 .gitignore create mode 100644 .lia.cache create mode 100644 .vscode/settings.json create mode 100644 Makefile create mode 100644 README.md create mode 100644 ViCaR/Classes/BraidedMonoidal.v create mode 100644 ViCaR/Classes/Category.v create mode 100644 ViCaR/Classes/CategoryTypeclass.v create mode 100644 ViCaR/Classes/CompactClosed.v create mode 100644 ViCaR/Classes/Dagger.v create mode 100644 ViCaR/Classes/DaggerBraidedMonoidal.v create mode 100644 ViCaR/Classes/DaggerMonoidal.v create mode 100644 ViCaR/Classes/DaggerSymmetricMonoidal.v create mode 100644 ViCaR/Classes/GeneralLemmas.v create mode 100644 ViCaR/Classes/Monoidal.v create mode 100644 ViCaR/Classes/SymmetricMonoidal.v create mode 100644 ViCaR/dune create mode 100644 _CoqProject create mode 100644 coq-vicar.opam create mode 100644 dune-project create mode 100644 examples/ZXExample.v create mode 100644 examples/dune diff --git a/.github/workflows/coq-action.yml b/.github/workflows/coq-action.yml new file mode 100644 index 0000000..c334a3e --- /dev/null +++ b/.github/workflows/coq-action.yml @@ -0,0 +1,30 @@ +name: Coq Build + +on: + push: + branches: ['main'] + pull_request: + branches: ['**'] # for all submitted Pull Requests + +jobs: + build: + runs-on: ubuntu-latest + strategy: + matrix: + coq_version: + - '8.14' + - '8.15' + - '8.16' + - '8.17' + - 'dev' + ocaml_version: + - 'default' + fail-fast: false # don't stop jobs if one fails + steps: + - uses: actions/checkout@v3 + - uses: coq-community/docker-coq-action@v1 + with: + opam_file: 'coq-vicar.opam' + coq_version: ${{ matrix.coq_version }} + ocaml_version: ${{ matrix.ocaml_version }} + diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..8995ff1 --- /dev/null +++ b/.gitignore @@ -0,0 +1,162 @@ + +# Created by https://www.toptal.com/developers/gitignore/api/coq,emacs,macos,windows +# Edit at https://www.toptal.com/developers/gitignore?templates=coq,emacs,macos,windows + +### Coq ### +.*.aux +.*.d +*.a +*.cma +*.cmi +*.cmo +*.cmx +*.cmxa +*.cmxs +*.glob +*.ml.d +*.ml4.d +*.mlg.d +*.mli.d +*.mllib.d +*.mlpack.d +*.native +*.o +*.v.d +*.vio +*.vo +*.vok +*.vos +.coq-native +.csdp.cache +.lia.cache +.nia.cache +.nlia.cache +.nra.cache +csdp.cache +lia.cache +nia.cache +nlia.cache +nra.cache +native_compute_profile_*.data + +# generated timing files +*.timing.diff +*.v.after-timing +*.v.before-timing +*.v.timing +time-of-build-after.log +time-of-build-before.log +time-of-build-both.log +time-of-build-pretty.log + +### Emacs ### +# -*- mode: gitignore; -*- +*~ +\#*\# +/.emacs.desktop +/.emacs.desktop.lock +*.elc +auto-save-list +tramp +.\#* + +# Org-mode +.org-id-locations +*_archive + +# flymake-mode +*_flymake.* + +# eshell files +/eshell/history +/eshell/lastdir + +# elpa packages +/elpa/ + +# reftex files +*.rel + +# AUCTeX auto folder +/auto/ + +# cask packages +.cask/ +dist/ + +# Flycheck +flycheck_*.el + +# server auth directory +/server/ + +# projectiles files +.projectile + +# directory configuration +.dir-locals.el + +# network security +/network-security.data + + +### macOS ### +# General +.DS_Store +.AppleDouble +.LSOverride + +# Icon must end with two \r +Icon + + +# Thumbnails +._* + +# Files that might appear in the root of a volume +.DocumentRevisions-V100 +.fseventsd +.Spotlight-V100 +.TemporaryItems +.Trashes +.VolumeIcon.icns +.com.apple.timemachine.donotpresent + +# Directories potentially created on remote AFP share +.AppleDB +.AppleDesktop +Network Trash Folder +Temporary Items +.apdisk + +### Windows ### +# Windows thumbnail cache files +Thumbs.db +Thumbs.db:encryptable +ehthumbs.db +ehthumbs_vista.db + +# Dump file +*.stackdump + +# Folder config file +[Dd]esktop.ini + +# Recycle Bin used on file shares +$RECYCLE.BIN/ + +# Windows Installer files +*.cab +*.msi +*.msix +*.msm +*.msp + +# Windows shortcuts +*.lnk + +# End of https://www.toptal.com/developers/gitignore/api/coq,emacs,macos,windows + +_build + +settings.json \ No newline at end of file diff --git a/.lia.cache b/.lia.cache new file mode 100644 index 0000000000000000000000000000000000000000..0ecc033cc88f30cd5e92fe987af29835065da4ad GIT binary patch literal 524302 zcmeEP2bf${+1}Z`1EDAM-b?5SUFwA1dyyi9UZtael+dIon4qADK!SpFLBxgvQUn1J zL{tz31XL8og8D0>|NDOBoLgsScW0B`?CkU0yK_%J-}ipylzZ+LC!DlQSJ%d`&b8!| z4_$cG%@1^Sb&bZ=gKKtPQ>WfNVM5Pl|I@!lQk$8AcZfoluK;O8_A;lE_T#^eyLk&_v`oChak`M3&itKk+3lFaLQQCc`E zojNt%rXdvBcGRLI!|tKjeJoUx9B2OI!Gr;Tp zn7DS0oMv+Y70En%`-gWliY*9`3AJWciuKI^IGIeH3AMKQ(Wf6bYJpf?7lKm9^6Cq| z+UZz2qh~O{8pl8Ijf+yMs;zR@AD?Q7(50E+edxdcoWn@AP`d?h$dPQ|lDF{|i_K!> zs(n%<|Gs53V9EC0hGZ8D7609>pBOy1ekr0HslN*b?^HE-jU8Ut@M1#?{mp40$gRBk zK$JFm=tG1m&_-20lo+>#zWjd^TNITfW_5IMk@tZaG}zkI62EIMVKB zsIPl@Rj4qUz&NWbL#a7nS(3SUo5$j&*|d?FNW?4|jMj2KeItf7Yfh83S<1S+t)Hnz zEZpW6lsAz~Zd2hp1+;J4E>83ZDdVWnjt^V77+8qEl&a%Erer@GTja-qKJ@_Q&lJZm z@^G4VUk2Uo<5i>`5^I06w3A>TQY&4Hw3|P)d68zcTbXoNmABQ4wA-Kw?Y4DFFmI_( zA(%^SQV@v_^&G}$bi)@zTBhBE=jMFYaJNERahEKl^Ms3LDUL;$07qeWdi`d&0k7-* zC)31hAMhZ@BGaRD#G9Frx8^@~@?j*_3%fY-zKK_FQY(^~k=T?-=fqZsxUh+dXr84g zUCTHIQ?d?mMa-JKjZafub=k(*93pA)Ce_$9KJxG7a>>FDNZ0NXtCD=Ir<0bQ;t4r) za7`$+qau?T>cYl;i|x0)iR`lNC0sIEDuS)``b19(QInZ~a))ofmQRAM0?J(nxZT04 z2szMSn4lI&sX%UyQUV2AOFn6=4EPpinnknJL&)+C$E6rrfr~B}C2KLqI$D{Pqz{Ta zm_Dv#N2tj!Wyl^Hhx{MZUsA5G8A*FG%g#y0)+VRLOz4GHH^~~}tJ5Lk3h5>mkd9sG zJBGatKtXD}M|c$}h=%6nQi9yf<|C8l*qb&b8C%H0#rtFp-o|ArGYJxUY^L4JQ;?Z< zHVVLpz*FhST_n@ztyOA|(_F}LlINFHXZVvgMJm70nkDp1x9Uox=UMkW`-IW60eapK zTKG`D>I{lG8VWY9x+4H99`fbqk z4PHgMN{5jn3Lk{Llo;# z?9_*xq#XHiAH%nJ6-kO(wDw?+JS5_E*r|X%lGJ40Mt(%^uZw>H+)bZe!EB{6cDtVlm~NSR1&1Q?bbe9(vSmgqoB{} zY8$Mw1X>Y<&FV=>&O+b@XVx9189PGTF{!1sR^l zxixNrF*l2X-I87DTAK|YP-c4e*c+sM6O19niJ?{@(;??RbBd8^H$dt8AQ4vUYws7y zr1a5ylAutOXtc_ZDTM}9*JQK$H0A6vUJ3w(3}JsZS&`9njBQCEnb2m~@yjtKBy@q4 zQI}&1=}{TUl^mzPg;**2C5EcfC9?8?s%_W}GP}hSd;QA@J)c>IOF-yL@`PrsLQlB` zB3PiiXni1ZvK;zVPc%bi;xvP-TIIW;ffL_W5H$fuj=E_vnb z7aFNH1gY)@nV#j9CzT0l);bv1((uHN2{bV^x0j-7GC$)Mv=#~86b%Z_6#_WzbrL}d zr;$S$DV4X0rWW+Xn;F(H9mNXGnBtcci=h)WzX^tq{7F;PW;dDG%bJUGm2Q=rx*Cmh zPP~5`qv)ETD8~p7^BUO{6&4Bmf~=K|^3}hi-Ch2)4{u;(+zw>C2PFIzuOb}P#MG(CGlv<0;#RCuVihgfWiL$UC+k@;C^0S`Rr`v& zIjKmu584BNm(AxR_!zG@Il=9=bNKf;$MYsmBJ+5(`Ccdf0 zpP?Cqwu`6o1lo>G(Kfw4g<{wB^rqhsB%n$wS)~Emg2-MKgZd#ySdGG3n;6ti26~2W zmm^rM7?F%_jJxG6dk?j?J!twp(DSdniZo@Pm7FP)B{k2ycvb$8J-yJhboZrFc=mtZ z@paP(nBCy!%kGPL6)7xrgo;ET2x$>ylvm?Mw9H|sEY5LA7BCBmY$e~YJ|$U0*(GpW zBZb^`tgsE3X+zwQJqidJuh_G#&}dH@#3~-{y`s}7BsHK)g7+%*a*jhRv^<$|m1qX+wP?<=hs+%p#^=XS3m0eyqk|S#0olJ~uux`w?Gj zjd?H&9xeHMo1dR|3_ph~Mym64)Oo1o?=r~x!_Hn!8Y>O{ST0lf$ar3?&?5fmeV z+KSq1iAD**fMc_crbgff-Vi~4UV4xWX?8N|$%7A>7!i~rA8h^uzs!c?*Rfu@^;XJ9 z_~{Et&wraUSFaUU|Z?6cmv%SE^N#L>Z+qrb2x(1l7%sh(IDd>%K6q zT4f_hxhcu&NKu#$K^W;5O0k^$hjCF0#A8C!QTXK}BO&QQMqgo?J3v~Qlz*aCoW?1O zJ6qUTm_4Uvx8cxiKc6tCsfeRN*q=Z>0GZv(L9bcNMgI zm=U*XJe0DeIcpmyQjY)lAwC|Z|M>t={U=@{odMC^G2IJjnMeU)MMwvyUWo2b^zc{y z-uVvk%|PL=fx4xmCd2QD&>elHt}2W`T9WmnE3Gn0HAnZXASsqidN$!z1zgk0)aUM| z4sp*AorW&56uz%r$ckAyH1xzk=JZ#L)5uwu8R4?sO2Udkg%HA{``o!cZieMSzyn(V zy0Na^UGkcbkRs3{!UI83;MM;cQlmbFhcBZMD!#xYtP69(-~{5rI6@fa;|NCO89y+1 z^zMZg7DuXiogWZ38e1(p`C()0b71SjVCmDmic&w4*{WQPLJJlH0+&TKfPmCA1x6SV z_IWrANDow~fMRe?Su`5k&%O1Qtub0UCpWM>)e($J3i3OY2LA0(@8yif8jkDxETgBT z>C-BszZc0E6#mm8%oKi+qg5I`o3hcE`|{hmjM4vwM6U}QKAKliqC1SvOLXsyR)Cls zr~$txiw-pw-!){!8j>dhkK=s8^C8UmUN-cgJ}-M2Ucd_jS+= zd+fV!<5kpxC?Vy(w;S_lly(ww#d6wU0(wLZ=-H zLfnxaC%ofMLXJw>@0{Kgz#7<)+#SM9rR5b=x!NijuDB1=Xe_bGX78C4yaR4FV9yrd zRph3iKyKh`N`tk>c>!th_9KZ(ehE=Y?hTEboAQBhs^F&Wq>U1x=w&YFpTgbwr`!zu z6K;NV(71VL;9TTp9Gx0BD@USL7OI4?B|*h8XZ962S=-(1`D=W0@Xb($??Rx@;Wd(B zplHi0#!CPaniP$7!~$nmr-ed5Y{`(ma!K;*CBTSYY_*shQ$>y&jibkX?OP_q6Q}kHK?E#xOZ0x_r4XvTIJq3`|o?2aqm8G??2!iUXjB@xH*gsG}bWVXZRr=vNZo8vh3D>55?F+q{aR zD5g|y5Xza_o|cPZ?~1g9nKzd)^Q%Q>em5{KGBb`6jhPiA!U}WS+>UZIIDXRu-H39= zZwc`I$Gk=|?_2YXOE`U98K-Y8a{6l}oQ|WvYO$>x_ZMBL4Cl${gFdvM+grZvj@PNW z@8nfv^vJQd{bux4WsLUezvz7>ca$*t8zHPIqYL9CAOCQ`B!7*@iLd_qV`hc1*`y0A z%iYKE>hLu3hn_6`BSAIfAdJ)S+Z|%DxxMogMMP(dc@co(imTPi9v!l%AcA>VU3q$g zGmKq)F$Em!p2DlhF0@Thq*VYXR_{n1xAsfdHepw#70pRqL5rSw$d&6F3!ecC7Xka8 z;x&?4=uo9VnMTFXa*$l5CQQxojzZX~TjciB#-?K)ymS2&mlp+xxx4a*MJ}T`Db*4M z72&2_g1+g;>Nd!@l4`HC;+iqjh2>oCeQa7Hy1kEXrVE!3J%3NPo|p`7rj9#YR)!ca zZMp&I3}e{VW+3{?*1SZ!I#yQ*r?`Ff6gQ|ZfP*VQMqlMsl+%%8P|M}CcWpdi4pvMB zx2l4jx8ggA>K5+1`_yP0bJ^kFHKqIoxK959qtE6wl9}Dw0A|3f?YFyBTk($%8qaVB zK-X`f!nn2kP2j?)XfN@R02+nY(E;mbvUle>Xbe6&pF#9Mj%qCv&Tzkvj?#=g%BOP>K|k z*Aft~v!{42zT$>JP)eGbPH2RZLU=HDh;yPM-v_kHNG0o$5Mg_bl;r+CCh|C;*tqZp ztYq-bv3!s&$xSvpX6b~L_p-?hQQn+J=|MkP=1`=^|cvA_+-M7`2m}A21FH^;{?wV*;3}gM4`2LPjR7oW$PG z1146DSk==O2s~C4)ZaSbxz7h_(>ivAZr}@ z>plETt=$2p$3dh2@hZ|uF{}5?ODz#qC_eWM-pZ4Fupg!yq-Z#Ql~H9x%Kxzb7HXyI#g=sw$`bpXbGI^&L2S2L<)v>MBIh^ra2Y6lS)S6Y zRe&cq!b8-1|EbJVxKhPb+K3btS~3zyKS&2AHEI_$rWmd8qJ+G|_B?3ye4bV&Ujj;y zOQ#3OXMaEwn;+w&dxaKG3kAhLS+)>j=SmAo#w)FqGY%8MSA{f7oIz4bFgt;od{?|6 z(%*$v(|U~cNNdxko@P~xaZN{D5D=R7Rt$@@8%OVZ&_YJkZ9vqAKv3@Zd1r(Y70gq) za7qF*KIH}=l}O=~@v8cqXHCm{mN+sl zCA+pCt?WE`Z@6G<6;l~nSo-vtbYW(w6jf$t(2TStlG5zZDNR?ZJ{7F~Cb-ZwImLxh zV9m{hZdRoZZ?8&hrYTpY*^-IT7m0gk48gwQYkNC4XxF|8pkqa+@?AmFU%hCN)Y+`{ z()iKj#=N}o)UTjPjT=idBBw39cS66lykseiCnn$>SKPRxEf$vP=+0Vw88?FO%_7{T zl#-qP$_=N#a>M9vM<+m2w9Jj`td(hBUZHS@>YK(~-&w#I@!8#<#w5 zWV_G+ckBmWdcnws_pjw-fa^fE>+)n1qJZC7`cFLvRP6e=HQow`ACo85{;t=I2 ze+j9F9o(86Kbw9o!4!!Jy^`ORF3Tx%5D;t|S@G*Q_f;gXbQGjR#F-w!hBO+D(Ql;> zmA|G+QUl&{pqrA^%RDPoRDC7@5y=)g$RMw#>Ozo-D~cJHPHZISKj=zP5(0^MGs4-S zos!V#hAcKFQgZs+h9ccZMU8`&Nw$*%p#*f=42hX!pj)x$#j^}_y8v{2_q_V-BXn6{ zbPB)joFCBNI0lTsQ~y6+v8 zyPaV}+$Tj7@x)mks$y$P=%^gelat?1C@G8YRHmG$`TqCTxkl#AL1vom*LW3WTj)7L z$t)tE=*Le*OR2}2qU@|&9_JGx$AGfmhii%xWxMCApe&)QRyM_2;M4+@`wJTP1w2a- z4@;>$Eo+U+lz`}QOp|wr3^ZOclWfh~wp!K>*|J!d@ZKd{h!JlhwMToy1f=Ef6HB8Z z-ilvI$b}toOeAiy$5{i^9x*CKbn00&M{2!Oqoge=h2O9cQNOd@vgD(N?OnkEZXEjy zuObIfLXaeC0&P^fVkN9{0Zd^6CrdE*n2j=;A}0+#|1F0bi_`)bvU))yD|vbHU$O~r zn^|)F+{zm!RYt07pS3-unwRC6#S#OM9Ph36p#lbQ@pFRt66E_JHs)Hp z%ja4RrpRU(35yuLOgPYO3e3t5>GS|r zfLr8ZbI-+!wnHY*MbQ#U#hW?&6BWTWsB*7DS`%I?k|%$yh((`mnXK1RsG&V5^eE28 z807P99xM=<5ORyOxSU}=FTp7a|0~R0$a_CKoOZ=_rj(8V?{L0zm9Pj8wCWxwR^T1x zd7XFC<%O)9XsGfos2`#Bik?~$+gVWPle^5SJvXZ4-S*0~o%A1uYf+u;(-QAY`xx&& z;+#x#NDu(kqe8o>{H3vh13E|HYd1zQp}!qWjvlV#lyrCox+)j9QG#zzYT&y9Ar{LK z!L6?r7`Mt&>50}pCG+XAwaGd5+uM*PGs7yV+)P4B=Is5v4jgm5(_Vh86q&#s`z!J) zGC`Oplpy;}S2=;%EDefGz`49xCIsCD0xp_Pk0~S)=?? z84SQ7Yu!h8n1In08S+u#IuO7o!p}KE@5s3%NReo!QU-jsz!KeCUv4={tVHH*QQG^% zkGjo2u!eQjuHS)AaJ0JjE%HhLtIcR;Goru@f2~DcUFb|I@aoFuyuu83PJHeP;*(z0 z5u0AV87xTD3S}nwRb-4vPN;1}*qeT+y4D%ff?J%`f7EsdFZy|3Hk}A|@d&R4cy-tXIda3}#t8J1 zFz_UL!j%ka>Xsca>71)fOi1@9LGv-ZigXtV5m~`roxEEXMaV6byol#HO>wsaXcG;9jZ#;U!K2L9X#0&d#QmP@*2h zbQEGzgOXHPMj^!StF;RX<4x-KLAy3H3`wLyACkz!xz+=9lrQ%FNZhA9PCMf=fttgR zBsS(&@01Ycp5Q20iYO{c<`f8@W`s|Na-TzuI=P-ahQ}AB%toVj;ENX+=f;6^Q!%+% zv9S`_%{4J!5|bRU-H6p;i;~6WVI(DL8^adZH%5$c3|U-Cl+Or6E-+$c)d(Tb%UPe1 z_KguO2hS6{UD5#QWxUzEi*23JIfBxqMV4&q6!>M6G5A&b^=pKm7itBz8jYPNZT)Yf z<5{5Nt3dyzyecFBm_UWSAM`v8>pZAzloA)e!eLQD(-eWYW0ieaBHb=o(OU_#8_76j znmPNJPe)RIvk9LUO2rt1rJyaf&PYo6W%MjrYeZQS4FiJHvYFd-`KMdOX*0kE*-Ce_ z8C##8GM6^v<))S|ww!O3Nyd}iz>{wQ+c;LCRybCHtwQJQ7HB%HH@0aDJ?v zqB;s37W~N2nY1UZ>F(_GqdWaDTCP%5E_9AyLW>a~v>fjEVbTD#RXVPYZl%+C&pGz@ zvm`GEo&Ny^b0n{hk`WUZCTOXDn$miJuSyli1Szev=buhHU$sv6LeMrl;$XB1yoyW` zofFj!Tb)4#?W?S6_>`dZ(#$BqBYT^&1>gzc_NIcFTFDl_0h{uLY*U$(HNl9c(Q?eT z7KW+v>iJpUC85W1`)sY$7+fPU2f;OxxJhOytWNbzl1~Q$1k%VwL1~@|C4!#Pl+2kfSug45Uhb6SP0;aG^^%I)4}t}XLK=cxGiCxLu%JNEs0EU5 zI9z52T;MeHU?#bzWF}d-fgHwF=}PVlU__zSL(+BDruj|~g^TY55lEb2kWhE|JbO~- z^-_Dv!sUXN;er`4Wj||DRDUZ&$KW`Zz~#B1sLgvq0n@ZyuX(vsk{3Yuw_1Qp+4$9v zQi3H~*Li>WSKHsx{Q)3kBG7RfucAWfAjC|n$T`^**o`FxQ!-Zw0%FXqX&?w|LndG( z51U8RsgrO{bO~%;_S#imwN{1A+g|RJc_623H1 z0;tU4)LFCjx|cg8`7;3ZhXAOe#SvXo0t_)wnPr=xl}dp}&9v1lJDWe+y%>PB6F{^z zuMUvJZBb#*x;g^^QVKgkFoS=Te8=Uo1Uf-a6?M_e5jt-HI&bs_oie3Tjh!6+;O<;A zxkbnTU!rZa$?Ca{NOz|QnbwV2bI3f_1TrspToE#FM##Jf$oz4TA+y8_tN9e=f1qX7 zhlar})SlLMp$?cOwkz zWTGtTWp<^xp6ILX2uS$BU?E|?FP!}yo0f$xka@Nhpc7Uo>Vysw3<*QW@eJ_z$zZ`_ zkB@KU@Ti%SxiH|da1kD8i#B4UI}}BDv_2=&Tzm9&C>!AMMhoyL@hCB-Ewv%^G?(6T zPCKECA9t_q4Nx4ws{@QmUt%D@@UaHG#I{eC1(^JypD?MO=cvZd@q6v;_`w#y+E&2M z2E2;+>DZk%*qs!9+CF<9@biln@KZHUHn~x%Y6M!1m5#n-Q`@of8-QhLEbilf_is92 zNhzBlw-^|3@oX9wm29qDm)T<1ty|DGObI3l=JpT!=qU?9LpBt*SY2Qe8j}~WRVUk%D2ri4A#$ek<`_jPpz3}Ic zY?0p`#~{b=UZy5e(%y9AM<4n9WSZZ7*Y0y{llVrTB_ZE?zzM{z)Slgn^4;P0baVv! z2m);L0eftwvTq=e>B@?cW~EPX!dD)4)No#cLx)9p6;ac%3YDm7eO@A^I+_kY`-mFs zC5))4bPb9T6=>nS#GVKJ#8*ZC24G+#PY+hYdS>YWBQ;c*9(ynP2nDQvwHpe%{%67T zV(1ot!K%E9P(aO{Jr&~BrMx>K3eOzStyxKL8w4#Kw~_{(E0~+oM<`%ns1L)Nf$qWgQiI_O9#ihj*0v<(Q4^dAW1@PvDwX_3PLubp`VUF7U# z4awnEclqn%HaDiw{d#o40j&TVM9}c${os@-wl7a`7g9Rrmmbqzp&C$&(*q&SLEi zTl})~arLD`(UoAEc8a-BesRx$D?$5|+%ad}ohIGQAltpXiljqn+Fc<}Ae{u~KIp*8 z(VRdeobqfF1pJ(XMrv84bV!T$TG1(fIs_-^DHk+ONU(tgMXJd!CEa#ffiTU#Q($MA ze$b*=?17;jhgvAAv6l3ibepdI-nNFi<=cw7WFa9EURl+q8Np{J*quG`TWQ+04|Wh@ z5$Mr5+Ra3`o4E1{KD1c|xcdUcl^XA+-b7Y}BO|UUc;(cc&~V|jP%TCIS;nO|r6VD$ zhzVyjQw^yCmDiRw&gRGoFEaX3!;-r6J#=v!lfzSD?5App@cLnwdhncUK~W2+&9n{m zU}N^3*Lv6lcG>n4E*UKq;T?XjFWL}!e?J-ClpA~MxfdDbRsrRBHuxR9ijV{S1y$*B z6!9@i2^8#X4kl$EU_h?r@ov7BC-y^7xu%vBUI~vSX-YK+cxRZlrHHrPQaIYjehc=@ zHkj2o!lK0VWbABmS}Xx|Yju;nmGqm^?YKguq0tz-+o`sJhLcoXUk3Fa;Z>xdNNDU7 z8z4b$WAj3rG{+teHyB&UQguE!3Bf+$ACIUlr{GT3e>4lp{HOzY=<7*%LftdGyj0~E z>ThA6P}p0AxhjYj4qpH2&RZ)YyZ!=to(o#yMXlO?d3w4$s-sa!NUbh*enD*$`nMQ6 zS$1j!f`h*j*oDA#B4$MiNFU-2DYmr^v*exaw@{*-mW*Nr9DfTIQZmtK9DBgKvzurx z0Yc!k*xK#9@`OMcD8xzoPP0?sIpCibAt{3p4LP%{C&a@#V5d?eVMSAKU6 zL)mcmIaFc084$ViA%c1u6NBux!ROfH&U^jK8v6oi-vQFz<5d(-5l6X!-f1~CSV@$_ zPci9=zytum3LVo@L+HNCi{0gRA`iWCGk>QM}G(%Dx zb%U6TV~qM#=!#LNY{b@Be9lupZAiTs1b+*2dDxWLy?09lFG#x6Yc_LgRX3WMMC;<5*)3t=mYz@*oDye46CS)_(mZ~=U!mLcytn<}9jXkj0U9W;QTkAOavaZpq5Ec>WtQ@A)AdsZ^l zVHP&c{iU6X%(4=1INTBcP;9zHTTehVk9UlbGV0zkn?raMZ_53B)AdaB2WhRXCkXeC zw-{7`x<2Ah8Im)~nF_DLIwci4zLnR^F|@OYp`rYTl~ z6RdCCC$Afg&42d5tS0AJ_~^nHExXU-)#3D1A-ywD`EUhcF}Wd_az;hgB{wj7T8LHz zm$UvG##tQjQqKAxSb`t6%KFB7_Z{BHFr&d;No4RTH#$J=?Z12`MBOt6`G%< z=RrhTieHdJ_ruUCNGSqapA-_f`=mI@*`Gd#Qp=dBMWbtNZ z&#W3W9C~c?{OZEE#}HhCVLZ`_zI`kV7=r7Se4L%WgtyB=Y{^WZx&YA-G#bZUJjTEE z#c!{?1L_~ctLSS8VdKp`4<)hj#py2fc#JWI|HM5i%(@z1Jbf~j{aA%Ju5==w#)#Xo zUbcH^PkNbHl5Fp;Vc4A@)$VO7k~Xn?iaVM|q&SJmPT}n|uhQGeIuU+8Be~QG>bpyA zEyX`=xNr!+(aw-t2D$y5fZbu`u~(b0OaZ%o3szy_w7alyirSSyG66d!nN{16?xC=< z!>|%5A*Tuq%S`>r^h1$_HYLH?z!T2h;zncCSzy#_U=rSr@7}5?S0js2aiKz`NKxwZ zvo<3j8a=x&vPGU`xRjcpmBGPApZolh#*+)clRtnTALLc!iO5F0c_UT21sst2Ue=O_ zi>@0~jud9;amOkMHv;vPO6T)|jRhDi6;YJ24W8d+yLU zDU-o&v6GzRXf{hHS;VY{)Fs6jVg=BkpZh~DW*K9ZtvPGRETL8^QC_PCY1QF(@_(p` zd6M_hld>7YdTkC%Qm>5;EX`2DR6^EzX2cxIIQ*5ZlZD6v7#TxlUEg;WM<2eiS(^mp z{g77?eNMs@`Xs1C890@#<@`64Rtpq;K5H;DqVLa+zQ0$ZuP2~yR2$Hj(`^BFRiM=L z1mIyiY;~Mkrf%+q!`6qMH+XdbXd6$GNfaORxLvYD(L}|Pe41&l;_b8GEB=GBCaCrh zl#mE*yiHG~_)mxBe=1=)dw}IU-hu31oIWYV{=;&WyDo58!Xno$1SEgSs|ZUFPz~0w zUq@5D*osvq&}_(!U!M$+%fs?oCcKWf8$z0)2h0Bj%q5k$oHwMw7~VKN-Hr8Xm!7kN z>B{Q>%B#A%lG%85Kr*BEKH9t$3Jf#Rve&qPzJVZ_)pmxo#6OqPZncXYrra$aRIPMn> z2Q9Q{?Hp*)mv|LHD@KVliJDY`W@ZnQy0I+=-eBk`La|>lK;Bz|5KEmDwkZrIXzKxx zvzIi9Ag|XJ4r!JMI2e$gEgvu0Ua8}*|IEFnQ290*w$mp|@akZ*pJVSL3U4tK-ciDG zM^owB@!eRbtD{XzWXHE(a2SL)sc+TtGfyNv%wj92JM!_qBPj80d#wFHl%a2t(nKQ_w2 zcs{_0d8eLV@G62){7>}S1qz*&pqbevEe>0p?aEccvsW;--|Q1-FY)$r1e-J{1;)1- z|ECz=6pYi=9W4Q4MunO~I?v0=FHBAT9>~O2u4FQ=4l-Te44c6cq4*kauSY!Q@%lH$ z|2@Vx#p|5Gz>leP0+tGCmJd3s|HG#uXw?I#_6@3H%ER;J(@{8Px6RWM@Ep*81+St6 zh*qK^8bR(Y@iJ`YxY*dYc>6;{cwPeDWBmIuzNrMvAJDx>r39=L(ySJc(YpjR_jRjd z^9XkND30ukDa&Mn60rPzH`xA}Zs`8nC*Yajt$?1tb|k=UKwBgrx()c%|7`-q?=N`! zWdv~^;Xvj)NVi*yB~h;r7Xuyoxv#0wYICQ%lgy>_wC1ZShsw zh|}lUs23s*^EiEz@xP7nO>jD-=FzJ3b5Z9)KbNUps_pXdd=XU8qmJBtoH^;=0`ReI zJHbxWq+}=RNCbXAhL3H8_|t^&GZDghi2sW5ug3Uh5Fhf}6{M z9nfb0(A?}$F&~1&BW|<9j0N;h2-u%Sz~%w{8^-@G#y11>u-WLa&EuoiF%7#Z0Ew4j zdpJpV?$oJwPngiN+5hy9uOf5++0txr8#U|z09kB>O%dzL1$gPZBLHf7;xscyZ^&s$ zk)rApA02#^DnHrldg8bz)2R9o5Op4}BC1fGHXu$dNYKpeu+CUDHvqfcMpPAyra`LQ zHw4lE(g`OXceClLJ)x@(1EN01tAi>ZuFpinpc#y{?S6Dy8f%9FXIJwoVr?YaMd*Z@250f^k;hpFf~+c#dNin%O17QL8jN*ibh30mxZw)@2TrV|eV7S99@u`bi|y$%-JrW4zbMW_RH zp2BugQ53k9yaY8=k$1vZc5>t$2;`j()P09n5qao=cDFOD82CJcHj~aM7Ql(k$JC=tQ3n-lsvb_{^GZ$L>q7zN+;tL0|FkP{P*n#>mI~HO_`j-I9 z-q&uEMiv*RaZ+2)1w|z~65U8D(Y6@$BA5HMv@@ghWVQcTu0g4@=6LDv|23Vp8gv#u zD%EowuMV>MIW!)D7}{}_wbK~d3;4lVxjiLk<&H$V*N-XZVUD44ZKLydMXySiEtZ_? zu)69Y`N{=`tONb>X)+J(0#0j4&#NG0F$TB%O$VfH{VNwNdBC4Oon^K;exQ`7t$@>5 zZv!R1$*ZW5fh_A=^G|-DRdWj&222goGMUj|xCmbtvl(HB6wTR~|9o&ugVEnWJi=&y zUPaC|F)<87K8iI(hcJCB*%KB|jf;cKv*rB3{#y7F*b=)_5kYxhS=^L~DYYxY0}ExyYW zUohB1`n!G&=4`{O!ysc&_&NcXnBw}XZaAlbux)%`BFHJYAb{}0)kE2L`7-RF=;Y5^ zpX-E$FEqYjL8$9#@C25=dxaujq^3}vq1;6#G=)MF<8%RiZZt6&%^S`Dlt`Bt5dnTc znO(|fTa`IhFNSZx@C|v}I1|b3_sKREBm{~#{k&olzR@S5aj+AW8N(^d66I%$%EL!B z9TJ^oIgkM@me$)>J*20BG18RJu-L2PK1}U-=43-HhN;n1zA(_(>E#QaHh$~@etZq4 z;VoWyez0z-E@u@GmZ7Gb$=KjEHkZq2pDl`CQ%*>I@B5~K{z)%iNL1yu zUm)Z`k&sbc39&zHG4gP#J)lNyiV6pamF+)Hc16>!@X!o15b*`ZUXQMNFy$DkbUx_W z9nBA}?E^Z09W=%#Y-;c1=^VM{n3nz~D6~N9(X44+-sab6rKn_}>z6E@lRE^hssc+B z%pN%l)@O2l^E25f7XwVE0F(ZPO`6#I2jWb00<*9q?Sa1?(*l7enD*KX97<=Rh->JS$#cWT( z3o5*JEGg)xF8lqvE;WXJ4AS!onAzafVQ6bMq6Ig$6+hKEMwTr9##28vmfYRd)dgkN z4Og}M^dd_{lH_LEkn`qAJ)`LmBN$8Oq}0(h4QV3)lf@Yc=ZOE7aqBDY15CDru3nLo zMg#*n*Lb12Z5h73=H00njj@~(Ol}se22w9kSdKtl+vUXKV|#v90b{b1<5h%UCC#j|Ni62_*_bgOOkXtLb`HX4TY&x@D#6-SndQ6Jzy5VD%`l`F38t zs9x)!G^xXCvZ8;i1`Hw;gs~v0LV_Tn^ync2&a)CWT2N%P%*H+Y$|U0}mL_V;f~Wkd zXmLoUwP+(mq(-Pc1q&}W@im@^vbxeGIJq7vU{IAt#v_r`n?jO%kmL?e(vp>Z0tF>c zrb-J!E?VbBM*pIBAxB*$uMYwkgu?jWEYmU+1bsxEK|wl*Pb8$2tpqK=hApJ+E<|!l zJPGx|ji(r1D8qcG4D2l|5rfqxsY@$1mfMmKZmR zsOA>DoR-Nrrdg}#L~v<7*-Z0pUX1n`9W<+K`evdtn5Fp2fVv+iSd^}i*;1qS;v9`a z7I#GQr?@0vN}&T~XP|%w14$M{t$?g;o~Od5Z6IqEdIC_ow_^@`?OO9`xXorR_%qM& zDrz`ER0n)EGn4cSd?H#m5aiQf3kbUmA~9ouD88QSQ6jiHqv9!}VgoZwFEZPYdE=RW zNGS5*8C37R&geI@gQ3R4Z=L#paUaK>b$u6{@8*@~ek>1qWLh%H+AT^2t&nbY)**!s zq`oo%grU-{T8G^D#>ae`5Ql!$mImFS_Pa}7`~(`b#5CE3yUqaAg3myw6Pdu0znx8Z2!zG2N=eV0LCT*UoY?~VhqRu9Asq!&9bmypEkJQ@fXcLb%p@IRSVN+Sc5sU z_$k!m4n<5vhxm*GV~+L*Ddi-6Lik5Q zI3t7%^jY{o>o3b6`3R(vq)GwS6_S?hdd?IjwfmyAmSXO{bV&R73?hG``5_n_{$i2*jGu6{!_{MRa|iS)cGxWD#9IWBiMmq8p8) z&X|8T(;lmW@A!I759Tm?4xd{5z60t<)$(4^lw?-?26CeWSo_KbwB8ic0vWZT**qp} zNK1==jKNo9|Any5+P| zwGqisHNug`WzSO64ZqG+HW{sRTG{0Lx7dLD1J6RNz##bnW1m7S!N7w0uP|Cr7a@uL z;6Khlj{EoAmm7qz{aude#Y=xZ4;CThfHCMOpfct`^sYrmjp5yPn4~pE=(xb710bi> z^ac>XTfPT_mL@>Q%#Qvm2`vU$i2TEHOQUh-ge`guZeswq^#Qfzd3E4scBD`G3JT;h zYLVRgMOk~}?-wE6)U39l?MkO5`iffYA=dCPa;lmN5LGSqEMtG1Ew^$Ks1!>jsDW-7 z_1b>t8cycdALEP6f6wvWg^&h4nVZ&1LxY# zk?zF-qHO`7&3Sb|1W!->)*+^EqBoSAV-_z7$_Zd@qF&m7nS+1xksVC&bOAHtffrb+ zo-swtbR43|NpBuCjKd&Xr~x9TXnjij9XiVEuD+$6;m|$W4APds#g-jh^hcAlbEGvu z1XSpZ5*U;OMfh+x5sGSTRo{3w(;ssJCtCv}>+ve$q~o~IckE4r%pjypQGRBIJmhcL ztDVKb^f?xiE1tweU9$b}*ZZwvq-ROY)y?14Rmaw!`dmefL>q%_oFSmy9^orag>7cn zMK>1%8lO&)xj7rO=md@pU<#9OByDgvd=fbfg%IUqADvj9oULL?@^-3ztwW0QTw1w| zv=HuPq!L;Jgv59})N7;V&VvNdL}{2eRm!f{mXQR@#Rm2=hoo?>aG}#!?=?vg^C5ea zyydw{LM=%C@kXgxV2?B3G|l=?Xx2aDZ0v`56{QA=g=9)llbV2wFuTnVEPmiN0^SBG zNX_R`aGMcQ^V?MY%C0s^&GIO%URzPiER&jbCBgbbMrx|@A7m<69+e1ArG0qKUtDeC zfVUoNpNA+c%Bv#|U~kxyENV9?z8uw59B4I?TY0-(=Jfe4tEmssD-ozkYE_VvWUgdP z=b#AJ*inZgw?N;g+ssC}Vele!Z7F$Yu*8ImGW8l)bJ4`m@L)CTHEt@e*RZSH8)(L* zbpFMWT7qRp6@#hKSO5J^pEEybLHI!!Zzq4?RfMq9OzCOV?f5~;JcZ+wB<%+Ygs(z8 z_J0v*$>#%)BPNBj6+j0ne3EFO5Po;CAiS_3)Q&bRgYe3d07on3AYA#riNLst1Jeu4 zEqi70MKQ1fn^b8U9|w@H{)aK9@cAX#haf5VW=(QxM_P#Q(l=EQ?)%gV3V#r!1=W4a z7lB2}RJWpeRIwtGPx(-TTSd|~#nx3c)vG?%%a1kcweGN ztJglzx-c~bb%hlvkq}ynF@LPjW7vPaIrfp*NDsB>N-XrI&rCL>m{tl90rvmgVK&(o=1j>vk4XzLs zLcjZl%MLUrX;wi0FHreE;#E}p9q9Mb&+p@~7Z87}7l{8XK>Xz<5P!Q8;(s43h_59G zUZ)!3TSx+&a!AAjNmQN9_Affdn~H$qy_Y1V0#Pj}I?v8|SlLlB-=uF(Y)w2mV+ebH zw^gsG@8WS!FXHh?5D#p1tn_|Twb|r8M@lwQg5z^fQL6ePI2>!#Yn$Q@SF22Lc9I0U6a=SNUn;INtB01mR}3^f zRnzDSN3As20{M@Fn7QtK^9qxvMPP>Bgc*9AS4W<}=Yh!+6?MfNZq(p9t<-F>0){|7{NLY#3?gS^vUYAWmA!Tkux63SFiC5)e1S=OA_o;kh97uT#VnF%3!H9^nKKS z&Qp)ram3wMLtu`@7NVzk6$PdGC>k-k(HOmQmg;vF;(xigRqKsKM?yLUU{^#^(a_f$kcBc)}c>* z`^V6NPIO+(#von-qe!$wsjrG`Rl;QfU-)?hN8#|?&N*VLiU9TpZ${L+5==I z&01Ium4wlmBaI8IPCreRri~JM|DFwh8&D2BVM|3*{fklWrJ{^`={`kTYg3zUk*}Is zqYqeNy(+?U+Z@e_jAhXC+x+y?*ENjd^cFc^@3$~yzb#@EO&8)QtE`uWHU2bHK$xB) zaONh#M)NkWMcQaT9M4{cQPUR%jM~}kC~f0nRogVfsC@v>DxYW&QjFU7yijWR9!#2_ z*yH)B6i}u!Mt_m28e{~u1fx9NEcs~)h{5V4e!N+LZyPX5Fjje55n_h9a_m|%`Ntda zSpUdMUp74AUFq7%z~Vi;I(U?|(U$Nidg&s<;bPt{&CL3Ws#ewYS;k(&+qIrV<=i1RqEulBd12mWDnFt31gFGuQ$?`|uJNdV?cN%|_Hocaq&-;VrC6v<-YO zmxJ%mtnIHUgvHkU4^j16EfqJ2=&LZ-Rpz}FGk)%*iw`#B-V5a30o1O|tAkusn-{ow z&zbSGt2tog0$n&x0!VVvkH17)CQqXkqEVCQfV6x)AkMZ65IP#^e-sl*JDjq3IAa?0&f2* z12s1z&{ZClifjX{t9;*5S2-fo-|Aj-)QA3RsN@;3KxWUQygI0C-Tm#$EEdo)eNm~l z!JKza@zTH{SvACO<}H?wrlLKj zPsu-eiYK42$YHJFG736+f#b3qV}>ifS5WvX;*SQstQ_KUhi6}3 z&2YH`^yOjDm6!7>>dOu;)B3WlQ>8v-Byh>NYvvyzBBp@~C@$3(C;5j2_6V_g7k=(G zgV+`_{fwy*dig3;=MzxxQID$h?OZY(P(8_OjTV~ zOu3F@9?wBA?t1Ee8yFbR1{kMe3bMwl14bPi4~rch1IJyNIaGM10TV;~SMMP6l=9z^ z7XxF6{URv0I^Z+kHc)O4P@V+scmuB@D3Ms~gO2rWs;T1~_HoGE24z^>8aG2g8R6s* z%ZB)r;37+2<9lB5PIe8aRCoW6R}o?8MrJ<7Epm3dYkGsB%#qHIbjgCeEu0y&B+JNr zZNj~n0I!c{^ht7ZA7-*{SO6C4PR!_O_#^&{IQt!{=ck4)yThX{LRjR*(?Ym2JrL!{le%|I7s&^CysGxE7`oBm6VKso@eO^T%Nb8Uz#j=Di86|V1n_d9I;!MIf zRFkDcR-xs}3Iv|yL{ggW(kG$WM$EKHSAH zaMq)KL9`iL(Kz+Xr~l9xyE_=m4N%y_T>EXFv1|ebF}wI^<1cPiwgtCQY{~4JSeiZBMU)W> zY3~wlR}Ny0@UZtj9mx06lkusd*0-V%yos;tp%}QLc~O?Pt&%-Lt9-vQOFU3Rjp#@C z6QhDVO97YO%J2uJXS<)+bf<+1uVZq2MG0l$Y%*8v>A2oHc2L-Ovb>+5(}GYQctXQnlm5ltu_&jzz3seKUCB<3$J@r-8z;_0k;MB%QjP z%y_{;^g7EiLgN?Sagb2O_Tm1-M90|!+7-#ns-=%YNF82W$kZQq;^)cy8OC0nC-Yhx z-Qy-}Z;<&ukob?h@??&sNnNPbxY-2L3HOAteJWk7-<+6Gno|`A*D{*#lY|U-4w%lr zP=YP^*)qy$U4*pQqJvT_a8ip|DkZh_Fw|y(dyzKy5+{RELz;nxN1COgSIl>IT*5z)Xr zGa>QgI{ABP&nkL&tcrS49M2@{Gc^wriFHefTQb~V@8<6vy+n!L(-pP0Q1o=X5#oux zi3OTT4*SNaz&<(Mxxj?ydQYUS7yFas`cyh0tSze3ri%9|8NO%@ONBELT4Oi#EILC} zMEa3Kc34WW)Ikd}g;egZyl9mffz4e`H~k(mW4vkhVG;6jGl}C&Z|x1RS>y8aRH< zrsB9oqXN5;K~(ZC6Z|6wjz;&N&pyi(^N+#wxxw%Uc@>$S0kCmbYH)lafiesA%<2t^ zJTV0k1E?PooAS_%isBWOhdSrM8q9@p=9-Gg2is&9%Ji2twJKpKymBc;BrM+S^P-2P z8RyeolJ8^(f;^q6PpHCmgi;v+mmmtdS$hCjn4%;~oDH!#q*Rm#AL(jRV_>Q@8|nrd zP$kr^>U}mdCE^tClfQZAMaF43OSQG2`x9OrPEQX`0|gNYuDTTw#E2rIN>^9xK>(u* zJZDg5|F)%&e}utDe|fThh#YGrwetair+HPt06DbX254?EWMlOaaS8VCY7$9@0QUqm zRP-@tIO6xlT{wj9rBj=!tQ#_`zme_QjbYpHww>yV;0&ZP?o%Q1X8(O|Q}lRn2Bb+r z`%Bz;CabJ2X#Z3_oZb}4Pp(IbYn(JwlAG~3Ev0WQ)x8M5%TlEv5lcjILgS`RLMFK? z6KU-mh)8~8u^G%sw4V^i2kNCNUE(^V1Ye9Q53X3?%O(y$Tq;@hY12oTMX${VtMeOP zMIZ_Wg(@5x8xVz4bNVBDjdO*xR}RF*Bj-?r0Fg5gIMG6Wuj-lAdat9Qv@S*&sB?Xg z(WZT`b{`A7ZXey3oyp#C0R@x6fNLWPa1?m*MdgR%4=aDhn*PG=-EgfS%9c>+H3( zfeBMkH2|syMyF@K4wx`(8GJA)4i#~Prbw*ZD6u8;Aep31lt|>VdoALjlxh$1L zmY&G)CmYRN5)JIR&b#*7cumTN4hjaX6nf;aY}?Bv@4_zIB4D|2$i-d`XC`X z8RjW-i9`#?4dte$&FJA~EeXpyQrmr>xey~ZR2QMV| z9MQp#x(Xz3n6~LJeptxodHX_CJ2~Biku&1)T}a?PB}2JXBAIgQw+8zI>-nQgR|%pD z$MZCuyeT58e)7eRsQH1Ym4K!S{}+8wt*+{V)J0I#wh}M5js?tFKr-=e-o6?Ulfz2# zFykMM@v2F4sRoWHoN9J}XBo0(61C3|2;W3B>&tWcirifgQ<8l$ zuRQ5N;3$XAf*kz=69i4}IaJdhF(Z9rQRNnwvhifj6EvMm^S#IeTRmz5bQ8D;HuB`= z?oW2OI8`)e(`}EYHr$JZiV}RomzQ6PYEf9gHB!;9YJolU%(G@O{hVUnHs>DYr+4lH z=A8mdc?+)+=FLo&(pJX8OaSPf*pj#M%zbj5Eef;G;;&CJ|A3joMu=ckWE?hBeD|R> zR>YF*8mlg&z%6DS0pA|12F~(sz z5{HU9+W_@A`%@GBu*=N=qCEki6M1z&WM-rtAR^jE#CS2lYKKFwcUX<2LF4o_g@o1J zybbR`KXi#3xEl^)4iF+LOuL(G`=8(v>9n2&9sv+7s3ll8SHUrD#0Mjq!L$9^&ocFfV{7 z&!MiubBuq!AzmM2Y^JHy$1d}#Regk6@|0`6l6eCu~PcwUL@g*q#Kr z3h!Gdb7?Z7SSFtqRD>*&X`{p}kCb>z%{%28#xa=R%1W}E(iyU8HZ|H=q7|?oU1qJB z!B$7`%imKI_292wisJBBFVzf1jyM(KY#pl;BE(yEsV&P?_AE+^saSkB0j;?=ki)yL zWhdWb>?4R}JJ}Y~24(Nlt1{@Xp2(;YR~pbFoKTtd{LkBmCA-G~L5Bc6T*E!Jh#>SY zf+mv1*)P=W;Kz756X2&Xrvn&er+FMoKvJXYsr@cAO*9%fS`QdnmRAQyYWn-6hoBhF zr*^oIxADO-{LX`X&pL#r=6Z)?2|?9RH1{iz{vS2@<{YRN6d5V z$#%v=HxBxcNtr!>lRb(!=~ygqpf`(!B*P3Tc_m`tDBpURQaC}`G#U%6bj%Z`YZe2B zwgG+`ygC@NmBVC+X`ATdWbI9h)%3SZeFpj#Bjf941Wv;`0Y@MwzPu+&llG3-3s6Y<2&8KZy zQS9$3qESmI16qX%ADM6P*|BJ}5$waAFkHf{1g4RFfJ7HW7!pdGl9`~Bnox}JN2i}X zrOwkx0W2+BD;_Og>+`2n8^aijDOf_i#xJbbYis&!msgIWLlVxI*J~4Ud&w#`)EJU0 zd?UsZ$g6+&(`g`21Bln;RRppSg8lCm$iraIVq2D{LX!P&N`iV~(sj!Wc7LBi-i!t9%Mo5&roA z-JG3IZe?1$vMYk{m5^+vLpa}2s@FDXhVX4A$@WErR}96)<0zk~ktpDGx0^2hmFn;w z=j7Z1dpQ=*TMmH%VVlM?4iWB#1IB`BG6fUVCzLQP$&%ilw zP>R!BEP`y6{Sq^Bz`MW5&xb;*Gp*!9z4l?bpHLLB{*4pF#VQq?<}npnN`tFJFz(d? zw@yF)3#*%YqGT2#`CF7R_m@Ili=?2~77t zATTdLSn$?Ya#PW4p+~ChdYz_{lp}rY(*}XLKPw72qNvO|J)2GS^Pw&<8;dlA&4*PW)?$4Nt58UVNCue`mB zv6lJcDaTG-CT{Dk*Jg<+&?n!F83j{xpWL8aLt#oiFFKRDWWiz(=Xq&T1|%VeK7XxC z2$nNy??F1`DoThLeRNgHl%0P}`wt-d&_9f5s4i=yy{u#q9W22FzSo7FrsNH zdsXJE%C42BuV@6vLtCA^qYLH&ux~$yeY>AmQ83-e_io=LQAMt~`o4>cg77wP_*74YkxKq6!q62H44N?TW#@Wrvt~AG7fG^P zpKMewpx<}V^&IrC0`%CWm`vnV1bt@&G*x$L4DbCg0-JBQU?Dz#FKACJ&u)1w&c~peOlS~W5@!W-=En8Y?t4{wHS^zgEKsVQ(dTkED(_Asdpn-dPscFY%;66Z-9N129&->BE9o&xq z+_wVQTk|S{+l{9ZpxLyRq#WsP{}2H8>jd|k5xO~WC*jLNHuF1Z(B=^g_1b#Ppv~_@ z)@$1qp7$rx!h2cuPw?tMJFU0-;iM05XxqAj2m>+ay1ib* zIqW6tjP=@5CPMYv@?lcnMJ8lG){+&C2?FaaJj(4_tfyWJPE8;8^;Y^UE*zDT)5Onb zp_QIexsOy58iVW?#c{)5Jm%tf0K^ezS=V>xRTM|@0zjhPElp5-qiWM4CZOTfGP1w1=^DmE$kRBT7)AW0OY5kF+li{olR*v40g zBet}dz~WeE+a%SZI8GE^bK-WTAI6DBtI}Fl zMwPUI^0?5O?>%ouY!c)VM?2L|=GBqM0gmI^ERUw@z%j_vP+pnL%d2lIsMl7hkk|Et zyoS$Oi~NeV_ZKIqbkKDPi!b31WWUa!$ZOl=a+3u%ak)Gna=9vG633Uq z?9;Fh3d|II9*d41`A=0Rg8)sPF^ofduWDWZ*9zjbeuV&T8B%Q5R{=air0b|=0(iP4 zIkV3KNC&i3l*+?nVxKt~`=KRWgjR+Ky#?|46|bTQf!T_Q&g(&j`lc_Aw?Tvk@%13E za$qk+a|5Hgk`0W zVzs_no9#qcc4#In;r;Qvu#}q;!GA=4N*wfORaAxN#!Q}tUfhKB?s5s*8{?}bF}A|N zk@c;L64deHW+E?cKoYcSkdJW{60}K3v3Xx5=pd1xgPTdvNs{E0Hu`HWN=*k;QE)VQ zxVt=s0RD)9_KVVX(EZ!k$KQKsuQ+DH*6!q&9cfG3tA6bA10sgwY{r1ZaGfAzAE*$+ ztwV|(`YMJ;iHsf7ObpMIBxe=Hu!$i{iA6?QvJ#VzN*x6B!FoL{K^!vSdr`?NMG5K* zncQA=&f2nXA?01cC4+n{S0O>;LW*_!DnSD|x@0gVXzMpFTF%By_zIsK;`25n=-Jk?4Bm4M`L8)53TOP91!> zeQ$o;u_S~J`E$>Onk-o)mI7@+_aK)GYqFjonAh&vL zVb~^aE~wX*=&L`qp=8^**`PffanP>W=Sul-FN{9ZLN`A8Z!-uOYsk4DH$oI{?1)0z zAoOF*(Gdl4=F$qY8A-Ua0#XN}H}LtHO6dBq!6EF=`oAQ!7!*T%t@7Z1&XSgap8@|< zc@J;k=B0i1Ao~y5A($F(6qya~uB{&W$ zd8{Z6ok7BkTwKUV!yukqJ0NKoqzxj2FAWvD>S0sdBWpBvx@xae)o%362T8#?L-G=@ zj-;gRMn8rU&DaZ@0=-i4FmK|+7d<)J}bAL&byVsP0+I^(|j%}G%8I*r8C@cqteozsb-9CQB(%;HIo5}${_8MZ$`0}MJ0ecCkY}%YcMDrkbJ*rR63F}6G;k(N(1^rO@3qHaGloWsJ%phVxTW(jJf$0 z7ZiG59H%_Wt0*X)af%B{OPipYDaaO0${>1QXhFR;un*PbMP;pqFL$@~<=%o>`0 zt^&3!D%;P|wZGYvWAKL6a(KJygSrby5B{dSdC9^(AvvP@B(IMAr7hr$U*duGn+o}dc!(Z! zW!U#EF%+<2aMoe#_N`=0lr~i*xVPvS!;w=1UxYryM4@L}m?BKa)p7DmedVGkbjD3? zidq^s5pr#G2HPnL_1eHbZOL_AypKLv=H@bc9@_ds|3^3?7Q3kciUhK zpU>%D3bM5!ua11BP0e&$6>6s#B?J15PF{!x>HPQBg{T)9sf44~O(O0qN@j=kdIXkQN&QA?RH% zOUllBC~aLBse%zC2T^@E%7mgekcru%k{BgJtJ1GvFAAln7DNR72@&}h)UVpb;|8eSz$-l9fh=bipw-ccYQ zu$7f&(_1tO3*WeU8p)iOf^kUJE+V-zHgTgctY6<4;z;i2kOSb{=(eA3WOGZHSE@Y; z6raVbgXFYM?#E!Ff3vJ3MfLUq*eY+O#PKKw#SouBUFPY}q(RQ_(451o2=a~(@9MfG zAHD-}du2n$`qSj)4nPR1WBPwr;HbS8cwaSnt=`qubt$y@X}t0vxA!zez1bVS*ro>$ zvYuW$!1LS;9NqADPrz&LB-cdZ1Sb5-Ji?G{MW!9g+bWvCQU~%R8)#ZlaPc-x5R`1E zky2H%t39x^y+aNATPU}+Cx@ici-(mQXVr#Rmo@kd*{RrQ?7qn{|7XP68pOdFMYX^1 z$`c2Cl#ICblRzmX3@&{@hP{joB*}p2gO6bNFwF;trNg<4)a?Ov zF9Bsw;#H(Bg+p-EcjOsiljYFarJXy;3hetzysc~qP?$#G@i-xXG-6JE8Su6>3Nm@J zODJ_u3ufqk_FI5=a4Nkb>{zQd2fWh_c;|j|@Ar%}qd=O=K$g>a%%F)T1ApGu?O0Mik?^ehp6&6t>m6ggT3MS83ewt3{dW}#6 zkkBa6ka3FZlH1(4iP3yk6W3BpAu`&MxJnPoDcz#HrYO;pz>;JJN&MO)4bD=5O_iUK z*i^WS?3jI4f7HnHEr{wofFoYG>%P4bl1YM6L}GC>U^-5tp0kLA$EGE-o1oIhBB>ME zUuMb#5+O){Tw}fTWOY8SX@#tvE<~LWsXp0U(~H83H$7)9(o7Va!&6+CqSL)In<*c&%} z>1q^8lSaIszS}$J7(>4Vykj>}H}KwF@Qlz9X~~ok%}_AsW8g`0wi}o@;U^qUKEc?_ z4U-@kC{4%E7#Uf7W0A#oR7Kp1fvYxmu}I>PAUCz`>8ae%x_ zi6nlCTtaI#CQmDPhm@?6z>+X9aq3Mfiz1uM*;we#lO8v&V(zr-f8glHd3Cs2#?_nv zs*ZA_0BVY5arvv_A(-IwkN?Z~6?G?Bm42c;F8YIiIp?kb=UxWacH~vUIYW@Ccec|! z|Ih(}u6eU5Es`vvF45vtG)o!|V_qG5uExkUg7R_gBSmhUB1y7^7Pd9hZ<{X6DW>Ip zQ1b}+;!We+2u@M!c#<et3n<0p?Y`8pU}dJr7y=9TA?m1tFFOrP&J|ych<@)BfY?R3%q?LM;?KOSmg7y?>MDF0I$dfrLR*`Rw zWjbRLeg#KG8h?%!?#wqLGD^CS78o^>&$5_nGE|pXwSr$}?5z#;%ovW2HyQ`MJoPan z{P$q4u+P8y+r09G2d$*9u{x=}EyNc-n8&zg=*>E8?|MdhejwJ`Ov}yQOLKf8MyL{R z<}tcsEsG&>4o1j&OsMDtBQWbb&3>bFJe_S%R-Kful}qO%Et0F5{Bu>LznQVOV-JKxeHYCA53eF)(HCNY&aiZ=ojgs(qvue1T6{vsA2KCa zPCkH#Ql4(B>4n_!W<1^3c_QKzrZ3CZ zp5DaRFXwpL*#Cv~KWPs1P+C+I`W{4DkV1mwwOK|68Gj3Jx21B5 zK3i^~bKL#D0Sv&LY4^#z@(e)zXn?fBn&JW=m2-gX@%SNe$!OL%FK_b~=m$1P#$`35 z=Rp~!*v1EJuE!EK;BCWPF)TrHFmeaY5CuSfnG_u0C>AL=%$}I7sMka^%56%T53HP= z2w~c36@cXPK@QT4Kz&eatoHUCBTBSenWmy=M{PCV9uqG$xj7PSgDL8somY`J-*OSjQr2SNGuD|UsE zpvlgj(iIOG1La0eB6$?EC9k;RIpZ^5QQNqyt7mRr9X^`|g=ztabAF$xWkh@e$z%*; zN)SO;2X&NufqAbFiZUot^}p|6>|M~Wu0Uz8O4KA(VpFE)nA2$8VD1urjT zNVo?`m<`f?J+BTD28@JgL51-kc1oeqd{y$jZvw5BbMISk_`EUlQ?Q)xfQg6k>M*hy zBU555cFWCJi@YlxiK%dj_}b0HkMg#_1s^@s*z`2y4V>z}l~)Oy(r&4^Wa{sjA31x_ zHz-v-d`@r3LJWH$&Z-WumR0x2R-8?XX@ZoWY3^vc5|%8AaBHKXJnW>!?aJDAcP*Ey zPjX30^GAiq@urQ9qcKSuRILs^KAx`d@(c&B@+ir7oySqjCO6rWOB%!OMi_N9T8O7_ zrpcxe49BnB&_mnt0`vR~Hzx&28&!YuTgJbo^k~pbtu-PCpXccP28;TM-ACcjU55t8?KDQ$2!Z2K(F4SD8&^In>a}jW*)1A$^ z#=C}A8O2=32C{Lmrs%y-yZ%l2XLQ0pX|$$zTvI%mW8|KP%pR z-10@Y5Yk){sY=N~ zS>UB26aOOnSTq`74Ybija)cXLcX#WZH36nbTiii-6-A;Hlj`{CA zKQqo<3eNouTx;-Zg>%X&ZC#3St_V~mwPkf_a#;V1}CK`qFW+jdnX7kM+J5V!5x1g(@SOdzCL?5P3SXrl?g zru&MeGr8Bm`z1M6YJc+Te~dvez%{((!ng5zYRwqr959{a1|;xENjD6Pu#nbg1BC~^ z!lbI*U)55Md`vk4zD+XTC^ry5GfY-U8Iw!ZwgQX^NT+CZp}5%$0xK4w?iaOlx$6vl zn^%^-sNj<1LA@@q=2t&r7=UW6Ee8R8lUD}=VC}##fC8=#Zb;4~eHPI$GmVl&{F7 z@|vSp?@6+lqXti^or zFdUNlA^IxBQWg}nHbmQDz2e|YbcLk3GfguC2ulC9CkkD7R1#J?Y$aT#jwr0YEbZ|=FLCEb=cV(>TLB}i6F=QSGH za*yX@9nuWg;FRjzDOJ=SENZXNs*qu#W{6BT;xoDV=Qv)SPp4bas0mM#{7K@%Mh`}P z%GTGrlfC{;)fhGn36f`eVC{6k{0Yaa2e%KyJ z`Cs>*`|J}>-F#c+TFCz2c(uZI^Mi zMGE%=z(jZ*$tFfP2HTbZwb~nKaol5;Y?3Wb5)gYz?p;X3lJ|p{^B|4G5K5GO*p{J> zz7J61%FTl&4CX&cg5cnASS8Z9pR+SB zX_?-AtyLTNd&a-5(#UE-_GpO zVmH!BHIR^3NDA63C50QE*?#Jq>5Rue5^wJ)r^@j7KSb4QwV?~hRM7O+$al@3(8>hra_H|js`n=7&dl+}Tz2MivN;NLiVX0|DV0-g|E7HK9WY5Fqs4 zLob2|sE{Cv4S7Kk5erg8Q4mECP((mQL<9u>2!eY=o;HEi?0>GdB9%d`l!G@W?T^k5QSvV5ryLhVP`Se-^|Oq z$gQ+k5ce|QUF8e}l>P(eSX9aWD1fpQi2fKI6;R3qN+Nv1QVL@X3qTAiBG82hVWK%9 zL-r8!Tp!u$&xuZtVu<*2bW~z47BkVEIBQe@z9hp-+zCkY9eItW$OzUSP;5npD_pkS zyQ&nd?&p8A8E?(0K_mYyt3&}K7^}8 zT=odq`b$Q3@qN8qbqBCu50qY*J{B?YRaO9_rFXELmMM`}y@U9S@p_^a_@;cH&8e8N z^f4~!hHU4ATTn6fSCS7D#kV`qXc*QvW+D~;Fyr)`&rFh*t8}g`ZfNZ%Cs@CTuEEWu zee_Z6zzcFEO(@S~^RiAf#mEz;%HqmAByIF7>sV#)5I-$B{+zgG1zjwwKgca!cj4cx zsFBU5fXso1lp(`h{wN~2yXbx#4RONGn%Emcv#X5 zL<5sz7xS76O$svU?22`bS};p_QOss;F{T@WbD<3)R4bUpyyAtJ>3ejYI@b7hg0h>T zVB8&69Ci{KD&qUO6`xJ#j&=OFq$7ZhHnXi7 z=vf<&!rwP*oN9H6WHq0@)7f+4u`GGsf7Vdc?E})(MS7g@On<_UAW$0( zSq*$_I}kuC+!+$hWVp*g%y`h8K<4h$jprGoaJvL>!wv=gAJS35O_2X_-tVu)g?kK2EV-09 zEiT@(lKz*bm0U>kkQU2ps_Z#}*Fs;o=s<qPyV7`E}cqk`6yE+kLe=Gz&m7pRD52yT-aX{2((p3ti{GDtk8B@|1Ad zf7r?|C@wDsE^owZV?IJh9+#C9*R?oGVm9M0qcU$k6?S2pOBu2l(u=}+uizqIS=nPXKFutwqlGhaze%Ad0#jC()5dROJ`8=oj`lrpmIJKoQ`*==8t7?BIx|YaT#H zg`C#7@#H|G70 z8ZYeV8e#j#{`2U_1Eq3;T6BVX3MwsY8o#cgvwqX(7_tq&{>3{LQ&=k)?FT#^Oh<*O zjvb;_9P9G*Oc8j>^`+NZZR2$nItv0i6960RqS(Jf9y*l|)RGT0G{Etzihwx^oz7Y_ z(|@1*;F)I%R{H0~yg%&J7Gu}8__aJ%VCRw`unetcNA1n@FWGrv*sPO>QHGf@NGN9t zdv+yqd_poBjnx-sW|liiRO31tWTzYw+@YC&()9R^ADTkh4S#J&$mFBQ{B#b~Lu_)H z6E3o0do56F;|cHcsq}5RwYXHd32s@7XhCo-(ih5@NmowkwP**bwt)-6N%GHDWUK^o93 z%ZNtgp&rpb>%G5%@&z-Q`eq+7q6X7aE8GN>nLvuA;tS|+R~iry?5^B}d?5tI*UR{+ zc{`TT))_?}-znMdqDy{^iFgK!+V(hY4F@GbHa%r;XgBp*MB6!{nqGTDi$rSC*zOQ1 z?2;La6sB5u=ua1MZC#sR!%qEMgFE0)4WXyn76Svfj2qWK_Cxv8!60q`{eX~)xf53| zSpsWJ>33`mb0RWqh=W}e!5z%e8gASn2c;I7O->E*#kHhgwP<(#+%w0W4q;z> zdBDuDaq_b%a7D-+B)fF-62Dtc?b31J76!p2OmBy{F*v;9c?r=-N>MA|b z|3pOHi!T0$c6T(Z_Kf%n`d*9r1lF}^Hlr;Ev!gVD>#!R>Lx$^M&M{?pk}t?TGtHDp zc*vMPEUhHm3M5<@1YDJlJPFw)Og?aJv4P{PRc8v#KtY4p?Mx9L%5e@0NQlXM?5;jt zOv3ne&G)8}=U`HB6DF8074-U!J9CclQb`5fP{%47IhGQqh)$kj|e_n3Dvv)M#`$lYoX{qS_K(&ZoK@sBFzMNyf!R8rL4c)oWxTP^x?e+M4 z%*%7za`AxI7SdM_^xqCHoAsTR=-{c6!tFjgk6 z?#4S-AxzMXJ;~vblB>0`JiHtHq7tP%_ZY#PF>bXZHbKZ8su8E9X>;3+=p{aOp~#`!>#X35JX3a@{f1` zmSiD1vWV8;uy{#wmt@-vgv*L{(&y*r&YCqnxMC@kg7-g*=OAOL@cVVmB8qRUe~XpX0P^Z&xAw9BPFG@MAi%Lco*b8hL)X zU2Z7u4GG>?!$)40s2(PYCjoxBW~bavA#SW?XcH zo~JvQtp%mo?K@iaet~8eA#+>6WG6$FDDPS-^tzBZbPKt(IEr8N=&@Y^VQkM z>nYx~A?UpH3x&VzhmTHG;Xe-HuL!~anT|^MB?>>IV~vIsSp!PYNZ}EQY#&P<(3a#3 zP}b*u_l~nv($~U{z6&X1T}xkhU5m9Cl?o?|5mMnD2sgw`8DFK)^iGGr@vsQ3?=sNy zi*V&*I`Z^n>zaI!%v2$fElWg*Z(=^_H0Os&)~syxJ|aW#^N>CwhtQTJm$7@Io{_nO z`+ju1ua#Si%UV~;+JMTUm$urn*hu4-jE`(D*Pu48cchNdM7O|$^an~pkw=;&{&k}H z#Z@#fn- zzifG_o9o@BnYm&npPZ7+++y@{G$fJaEHg?p?X{iCM{ptbuKeLw+< z%~2w3_Zg3+BM(qy=I784dbY*@#Rk)m^I|3|J#CC02>lyFA1mU6+LlX_W@72)$u z;On+FFrn))g`NIU7$Dx&Ei2Wq@j-G8H+k}*05zRSuAG4#?u;TYF!$nLmzrN(#cAeO z8iUi~LtMb66R8+HF4fsIr-5Ow0d!G3ULK%h8UwT#qip?(KpX~gHf}=jjmF=r?oU7M zmOT%k`yL$?d`p2Z!ycVUD(qYI@f}g92D}MG;=3i+y_D-`HkTnV&f=ORJHAn&_@^I8 zHI!BRgA1IC_!qKEqMKqECd_K2cb9Q0LH8so)7)jMXrbP14%T_EP5@u1w+kRo*LlnI zpAHxYV#=o1_nobZ{x&H3JHQgm_ljZSvJ;sTq3}17TVqAfS!ZESgqbp3IB+#E6@Sj+ z*+DVqk}hQY4a)URo6EFu3flOAh8-HFjPx>Pp}}B^7x8EbK3}g-s2y{gLism<@_m3Y zwiSt++E&CgvsEq}Qv=3TeMpN#GPABzT^5wJiMe6jkN7?Tef*0I!bAp|HU5L<`jb&V z*$_UJ4|a5F5k8u!g;<2;dI0A~E`I)Zo5Q)mueKevN@JBhtNZ4R^Aen!AkOh37{14| z8HA;A{twOdZzHoV;hX~Pd53<}9>Dpsk8N$hD-_q>@}2)Y+{ z(Jk(B9ugBq7p;HJGklWMU{#c3(qM!Wy(*G0e_hWB_ z=ndfheme5luY8c1(+6Sf*P@RwzUOxEEg%;3FV3k;I;kP_uj57k7B2b==Mg7UanqXJ z{$dUk6ya6%L>-S`lRwF4$bFe>g)#b`(*E@kVMmm`Mr%YDu809BbUr{tu%hW&^skc$ zyQ*q8&ccd{-bTvzD8Cb`gjs+ov5-RvmoUq5>KG?AM3_yygxS^-#sk}?xzM)7@Y5y8 zBJY%7B^Qxtoh>4rs@3-@tjw=rVK6NqzAR6ssxQ#SbN~i=2|@TEnYtIb6q3G2YT$i` zEH0JumMKJ~WxZ5dqj@S7cP+dqH(bn{5={|5Yr&_dzN3ANUxESm0{w^3Q89o--|>W) zvKTbn1qRYL{blFF<_pTeta-b|q-1 z@(%#-ztE9~I9urC18v+yz^4k^10p4OOkIRH^^d8SJi7yASCiAuU$y9?PHG6|G#f7; zwBKlmVeacf1bm`USDn0}c*+Y~t1b8wi1G|bay1y(m(}S~jGQJRD{?Jd}w7p{fB48fgfB!3VQzr14BJ4ms-3C4QhxCdvTV!Xw6&?FwvT|sK`_32%O>IVtc^NXkU)~ zJyZX_V)%Jr_$gp`IvsiST4A^iZXPU#!_@t>>zzV=#l6k3%WN0o%MPrv%iLd1>&oG zd8eN$cCRnSE~;3$*R8tOt%mJ_*zMl@a`8#pp0zt<$X#cTA8e(_rKle5J+U<%d97O^ zw~g6Q!vMJoJ(n{w>l_I@`sta4V&me)BYs|AfPI8uG{k?2=d7M0&tYQiTVoZ&j{?Jg z0Ddo}Bah+AuWrMyE)B!o^BlT}VFTBKS>ELI1_2%PiG!|kDh}?zeD}AGJW*iYKRaMf zbDEx`qk?%U4l*ggGUhb7iqwsYba57V=kPCtZvd%;Z2Yx{{a~3MRUf>E%}Z8b^%b8x z)v*E(ff}dKk*5cmtMb8H^}(4Q!*gDD=k!RaWP!c;v=}relK%zF2qt-oOHL8Ycbod? zW(xC%VFexs#LuRqf;s8$j%SFJ1#{~mo0+2kVds;#hYrbp1_WUoRM}p=pGNp*Uy3$T zgk#QjgsFM)H|fYDymIH;aOcbNb9xowJ?_ec{3X)un|y3gL;4wGK+=l-Yt}l6EZ0kkEm@_D@~y`6}84sIB}IW-*j z3{$8>2}rPyokWGD!jI7%o{;Brg2jB}=P2zjZd&m&5f2t*&&hiI=!KsBcymBNWwnD3 z`Dyc0ZTLL)Y4QO9OJBIcw3I&m78^6kngzT(CCmOP1cZ3qr0rttd&O->SvJ<NyVO*fcobJDN#^_RSlE zTgfI5gY&He;X%6l!}5Ic#5{4BZ~P>sJ>{mg4TQ<_#&tDN%R(dU0^_t39Rmg1=qAly z0l^CdNau?rqAz1Xj7Z6W2I8Vfx;aVWr80&Xk`X!Z#X>2oBz{9BJT4_?vGFXWJ@2Nq zjt$)0%qFo84$isure5FY@oj(B9CCmct|dQ|qe3cMlCvd{op~*f2RXNrY;W%bIixfY zJXdiLkrS=*S4w-;P3sbJMlSZ(^VRq~3!Q`cdwoBlBd>ERfEhhURMT9xW#`AY-_$42o%KIV-klw(>@taZtUqYO(*S8+C*>)=SgYd$idmwWB z>l=|3yVfUBdWu#+73KCzE8yE4^m9&OLrkxSAvm)##d&&DXS}F;(mbX(04v*K)}Wkg zX)*N9Hd~C{Fb)|oI8UNrx+EX^#*IBCQQrR>?{9u_LmjHW=q^XgcYHfR&*EnIWn2#W zL3ih-e#eOu-ri=#48KAPy=R(y>Tgf)U>Qvn|wdL2HbjQXFA-a*|i6P>h^1b<# zwntVwrAS40p+<&8TtT@PlOhGuT(BytW~88Z7Tejn7`OuY*Lt%0@+&G=40JV~II#jk*em6^ z5-Z`#0S^oU&~sq(LP019Xji~&_o|Q|Q%DU(K&Pp3% z&Hm@VKcC9&XE5yZLT2BiqmmngQZ;YJD^n#4HE^-mA8SBx3PCvagW}JUTDyj|8=5*% zi)^v*rdy=mh|@+LlJW5>(?B?)NI$TOe7|gBQaN4$&5F^wzC-A!OX&o~2)2*k|Na7`^nyo9)@7vov8s@YB6OfX)u+<>8Sh*kfRx5)ahPc9U%chh zb_1j=?uJsgD9*$V;tdq0lxAM?N#A#r;&!3$6SBqOq-`MMqI2sdA7YlxkcEzHnV~El z(6~t3pYCy)erNHZ3!6yBh99LfJzz4%U%_Rrsuc0YH{FHB6MN?V57E znZo#{ULQRn*CvIN_%*8S->v>mmCw!m0W#F05zfV=!|Ut)ci-z0)jQ&E0K!>x{aA)gFE@9_`|D;Y%6i* zt?5D??UXCAj`NmbYk}`FT({fA#g)B;XHoY!hUTO(Rnx}S3lu*V- z^4xe@J2n}QqdJ*l^x3&VLc^0HLDL-lXviLTHWq&GFo zgzjv@Ho|Jtli?emtIwf2`x5;rjK9Jp#$QA!pXGW{D~T44Z@|fcLLys2CPqamY8vww zRKJI`NaeRl`#q)ofp6evGxvEcVQmkHzWC0j28$_A{nTY&d!{*<7(%H8dXCEDwEnkD=Pm0-}&&Z_ndX6 z_Y}ims-lhvYmeY$O%keWmkzniBsBYY7YJ-nGpu(ZISu6s<;H_bOp0|eKVlG)f3>QTnj%WldQgNwnS~NrNf1_^kfzm?w z=9P}f!%By)IMZHnUb;b%2I(~IaJ!@RBDVP3A`E|M5>?3!)36El#!!;H{Egh~ozLET zOBFFXSJ7$^FU7b#Gty_KPS!9Ja&X#rB2aR?_%C}Z{ab&LK(*sL{L0#bj1 zj=birB;ORhRjU!UK9hFDoRk@=43OzYXbQDdtb1|lR?BrSf4yu^3pks_5%?y%eECBa z_^%=G1tDwG|_=Ykc~XvY`jcSU>a1Q$7$~*mo{;A(r{~qkGx^V4fw&oH(`W$PM!# z6&@%)LU|#9loMQ*m>`w1#E=HfhU-3Iu8Ti|UsvQ=GJw-xGI+%m2@K6Qf&VQ6|Jxd{ zB{5#wLuPK+J1<=#u=Wz0Alc!yl^r6gJ6l;yLEE&bA3n)u~M2oxhmjDX$ z`7^+**B739n@bdwm_rqv4nW>YM+M4hafzUGeJ-OzAzMRqh9|IU5ylaP_!mIf&ythe z-Hso}$wxYaUHos{JANwwI$BUiuUjLue&7J@o&Njyxod{otn}eN6$`;XRs35*!>yu{}sOw#gny zKI4PrD+Q2@-=%i=U%*1s1_;!_>Vk#NyNqPcy^6M8-}XQM_d^Bhh5+i?0O&@VXe z%EWR|%C3^18zK47$d{RRMf%9Dg5uklF0#z@GUN4P&`cK@7xBaK{JGqKoIH*7vEpl0 z5Ki5`p{>8y;-l8k*8e10AJgCZcBdmxW?W2n<*9FY8ga>~Jsjs;Yb8~qcg$fPjR|lr zNIw^rk-_ZRr&y=B^7TfJC`G5htY-_^m->y;CEG zcp$32PgWu#G72wR5s@Pn#xa^07_Cp6;j@BSxlljDb50|MnMh5&-haXu=2u&J6l90J zZ2PfDqyLt??6@knK7;1e0mAEnW`bH#Z$z=N+yjiar0-h`-Kd$QT9R2?es3WWH)`_1 zoHBERnE|nPZZH}XcQ{9hI6b};zbBf*cWan?>Ykh{B@1~n7A_%$l*>&iQ=rITGU z{eUvvWu9evuZLSaVB@~7|9mdi5=Hl2EdcCa6G~&{5hH3Cd9SUO2OwHe8x>+yNsHvV zI!FUyZ0-o0C`|&|UI4fgecz=JfU3_E?D01)q=_k!0>F=30A7Uqeafki0Psqjg+6!T z?*-tusk+~70KlJ8ru$53)8k%a@8G5@31u6d0a(HfY5XP^ci88r61WqRT z44dlpx$pVgpHz<{P#*mp(nzv?$>4~LN&|4D%>*|jd}CB?53^4{>H@_&@} zK|@q}VP;jNAPa9+xas0+6js{;R(k_dC)1IK6&^}!2d>}|II=_4?(X_rlt0Y;-F9Hr z*icL3r(pGz4^}S~!OAE!kFuk&Y_i+47X!p`fEq$9VwU19ViNbMz47ctGtG+iVph`udIog{g~=I%!_(G&axcZ)$v9et;9XK9axB_06VE8S$mHWK#E2cn7;thJaH$BKg8QVxqqbaJGvNtrg5YR zodHR%c^-ad8hZl2(Sny*XTRVCBP7`A@i%${ezdfk#vW&5d3XU>i)bZ6Em{QNH0bXV z0vEhw;SCjms{n!PLHY5KSAZ1)jb0;>G__-OAp)t8AJWH`iZHByPm)*L~lSc~Z0xwUBN3?}Q*KR(<^5EPw;MIzY0q7S{nz9q8= zO7tu}LOh37k$#}y6uR)xYB=#tU#Ny}*|+8Jbd&sYof+}QT%IWVl|^c}Twke%Z|fvV zpBq%Ni(!MFr#425xgSNZR6~K@^*SUwGs&2dV0RBtYsdEx;aQrqeCbLyrC0fN1f}!C z=ib1w^GX}(#Hk2#5Ju2zlrNzpD-1kw(&G5W&&5jDeUy$$@Ffa95hh_Hg&EetfDANXVC1 zEab%Ifou%h%*2AWE?1+GDJ+1k>;C@Cydt5#SuQ4^VSxQ@qq4?5On;JAJ;o-{uT%6F zD_0v6;9vUk2hrJ8Ou!fb`kyrdoMxt>EV=3}b1VF2xtM^$&!9@9P-f~A0nVa|fqA(L zKYBR~_l_8TUobeOs|L&u_CZ-^kY`ZE1YA^VRJ2|{V~Gp4QUuO&F@d2)AYpZ8hzacV z?VDaxC+9u5vMVC0gq;cc0tKqGbmhCo4Rj}W z>ChT$${Nf>*x7wCuTsJd&s2>icuX`FDkCnc?bzTasWN%4qy^=fY~GaOlP9E0Y&uuw zr_x40=YQIusawZSNRHnp&KDXo;4LR+j(Rt{o&Uz+3W+xXiBa%*F}t$QGrJOXsvtok zWtr&PwOWD%GGC20j6X*o=-{S&V{ypzy`xCabZ~Lwrm!O00LHR?uoo-O2v(j;W2L^s z?Gs;7>oPBZP={WiU82@5(hUp=+{EFod?kY~XqGg7IL@7DhExPGRYJUwRFUHBxw2=- z7CZiUl~ar=Bvu&O89@b7!9&#vyBkikgJMSBaO3zOqj_Sla^U>NDN1Vum%`>5Y|oZ! zDb2$VgLhugVJ<>frU$fDoAvJ<8gT0U>%r6 zb+&up=HnD5O9Li50U|rnk%tM;O~MPmb`R#?Dr^=9Y&HR8Fh8V!%?dWGDLc?F&^t&8VG*0Xu@s+2>C@NFlQvAVbp_x1u8t z84yN26aI#4ou`wpl|iyTB_Pn#fC;G|t5zDBs(O8%yU+cCLWdTV9|+i-M@I#n0Z6}n zU#0};2sKH2#InafsUhwvIVtxf-8$*?#J>nBp5KXL`a^Syhpkm703*e;&QWXYP(dFS z{zUr#StrqvM_1(n#ik?Ol&?Ij@D+j)6s>PlLY(zq;dn`hY_$E?Rc{fp4g;z_PDh2T zPQ9e8KV*Cab(RR7&_dD+a}?1xj6aoAQQuEgl=GVF=M%VFFGo0b><9}pmJ<4 zj8IDu18&vtkq)2@kGJU-rM1j@XMIjb%%Xo6BcbwQTJvIt9~M@h=T~p3N4qSrFcH>< zHuIaD*9sLDTEjvs9&OhZ0Eha@bz;X{eay*%oakvFXHnRaKhlv$4tprcN9C*N7^geP znfNL_g`2eD81u%JW)VEO5WmBwwKM3*i`>Xq9!uxY+2@6qZ$@o7ECscxtMhEUGafB5 z%AQ$;+>QC3Y1&VZXE-Rxtb0$~Pt&v#yEPuJotKnxAq?$Ix@mXyD^iXHra8aq)*zjz z!|W1Agol#KDb>Tx68|N6IPTP;+LEkS^5srpoNj?xHK5C{R=PSOG+u1<+7XOO6y6C7m-FC^cZhTTY47hLQ=i zZ$~ZKsE7&MbCwYwfeCp5q`9At zya|E)SOhF$K!9`uzn``ujiBzt|J&*N_Y?f5 zVISWwxgMlk4=1@ytK)R%EP1C_Sh5!$rxxwQkBrCivE&HOa#WrrVWVM8OPC3T912|) zI3F@!91dOJ?e8eX@IK8xtSqSEf9;ftVg&EjS5E@_4*t7CF}VZZCi!4w#xH@7RPk4| zmmyhGULsX6eoym#Xr>xZPy2S$@!IKLq2QsYa4kB#h=QkcmNR;mf~16u%b(Y{$sv2 znw9L<2D2}6t}<>C7)Ni##`sxnVxDnEL5hH?aJWY5AT3bSZorXcoZCw)k#SgV%=dl1 z0ptFq`Q8pQZbYvzZhxlJfklivp0k{oXIzK9wc;qD5HrB9K(r*A+o9YV3r)REDR&Vl zhcyYctLUgGM@%ZW*ES3&$B-Vyp9_GkL~EmJ-EbZaBG#fYNe<-V&{(R^icA#EOtcWP zaCu2lss4w(pA0+D&1=yV{yeORh^KLusa+vr-diftJ(g$Wt@biYkgKvadV9SPmyR?0iTJh%>xMzDaMbTmC0*8NW*(|4V3>VN)%l zE$(X(_P96HRWziZ9ho{O=FWVp@kPWukh2_=C#IhohFMuMnDhLr@CK>ZZ#eZY z%F8{#OKh)HTZ)c~mk@W!{X!~nm_}C^`+fWwCw$B?c0tauaFU~YjNOxOwRaI?59cgL zw$9kF&l@JJkLSrbGJ(fm`}CnowIe|_Oo^*)Pe-0=i8h92(8AxubO&ZPc_lKtmH{3QNu zxckRmRsMYh0|~#uAi|AwRQ!YRO70y}i9I@O&Pbh;Kk+6A<67qUwFKu_D#_73ehp1{ zCQBfq$O-38J5nivUDEpIhItx8N1h^8FRfR`+I&$8VAlx9OwDLz{uM5d|3x4FN#LI& zNR0_Hdy=Dj1nK68L7?{*G9+Z1!f9DfNp5osV%TEi&bd<=whb7z7}&Kw9Tmd}Z$mo{ zR}Pa>Q-kTD{zf0KCp^h8DSn^QKTOiQ$D_@0r&=_&$dQ}CS$4}iat6dH=gj`_0pCe1 z@&dzbBBpt7>pM;4+Pb#!#!4;_EBZUUyFb#ACl@la7-WQ|8glFYkXt$AO07U)sLl#O zi6V-$ND@m*`hq?BPk;B{%9vd>Cb1#R(S{Xc0IrhzM6HgP^&VqHXBtnErcc%)+U;Iv z{zIwC_!uon5i6Flb;c>>)3)#Bj*#ugh3;QuqK@S($G2*tLdL`}qL^e%mxA>!obEMN z%(KI`zgU;U_S0*cMuTJ9(UIp_s)^JUsD{6~Is8=)&&qQ9d>mWI%dutJ<=9qCplymc zX6N_Yurqw5f}ORLL_Wt%lZv`cOr8RA1&Z~ZCO2@-U)->q8a3>{#d94G2H6g-$Ogfe z+{dC4%NWxthlHtBWK^}bqZqiD&6)nkKYDYm&(z_~4%~le+0^aCh3-;B!vi?WocB3OtLuBUGt9oNR^)T=TGQiBiSa-&| zQn$eE0C;lqj8oENFfp}E4VTxV_T%mH%xRxP^r^M)SRa7eA?@C9>P^Tw1|kO za+cFuCE}3!ocnHj&eF=iOToXjz`e8SsQ3qAmfW|a63ZCxLOF>tG~Z+@R=3u$F|ykq zZkExB=!vL&|CrUdUA@gk9Es?t>RkkTE*RQk6N^6kyW%y#0N2o6NrI^ z=}6s9??t}T)URCjn2#KsoS;7)T6j^#}qO3Y|e6S-hT}nII)91l5mPY!R%0X>qlxwj4U;$KO}BoD9#9 zM##^iBhQwqr`GAT$P(GoEzhtcwhWs=1XvNj4M{p+!Su4cy_91}zF+MJ|9n}QcnFxd z2v~?|l(lUtCX(GMw~t08mNB&FSQE#t&`1Nl_MJV`A=?Z{>Xx==W4zwq+U!&Yu@f%7u z+B=Ab&hZ+|+Rhc(h#Gbi1hyfUYu99`$wrld>a!zX_|oanc}HYgJ*f(+WhQ2B+%B0W zF;fmGBGYl4<%B$$Lbk?QvSLrOfG;Trv0-r`-jaPgXWcjTwMYF8C|C9II_={TiOcXT z%b{Fq(pX27Ti8pvW!t6P*374Eizv4@XW2JTxdQV8nuHm}9113f2t-$f(|pAd<(A*^ zcbln|qs0fb(iHod*LKQVxr%a~Qm)moN;%X@O^WV_TJw0RwOG5<+KhR#MG>{ebCz98 zr&c3l80Jxsw_bvYX(XPVbksWcD9@Heu>UOt`d^_V&ogA!E;<-zCYo3%R2z>p-gsna zc$Qig*AdT#OYozJC2YfrZJduWdYN{?j^1X=^OQ7wAkD8pm@m^&kp?QFax;K$WXR;kq-Sz6fjTi&>RzuE|v=p=F6rO8Lv|~%W16|uR_w8vEvi> z`_BKGV@Bn+Rc@PLTcB-%5Gl7U$Bb1iGcY&G%Z$x!jxE#7*pXqsa}hJ_W;?CTiE4@& z`~Knkt1B}eM~CKPBSy@&1RVndw~QOtKlVfU(^rq{$^Zrs;*LS< z_G=oF;#vK@f7AxEXbd68m~|~5uennf7w%7_zI%(ff8_Brq* z5aB3t3LA!t7*JU$JPm&<6r|fVR|RC5CdFOvVyIRf*K9@ z?xR_8FD`IJs3yeOE#BEFvqXWKZ_J9Jf2W(&&2-yj zH{;?5*Zs}q-%>u~eF4$G!R3gKJfABcau)C*f%Nv@>V}JfsB}1`i7gXy zY#wL1x@~~Xd)OTNrrCTDQ}vJ{HlNH{PHmmdS^79E^>zHrVEehpt#yDh>@ir(DPY$d zbW{u@uvH7*lELCyH0YZI<+!(lW!Crr_t0rmTYFHNdq*;{U}*85^gwE~Mn*8s;wuKEQE^v`4ze^pEI@ShF_q|3 z4M>H>=kp_6SVVN6?MTkr5kZK_Dz^8DQ!}9L6-{cvh`sk6Q z6Wps2Bz?mfS@h8lzVx!(i@M%Yy4z z$*81HP9i=h7E!aQMy^F$Su=)Rp1kwfv2hxJOonv7w4pnMPY%IbTYRR;FtT1~2J0jD zymG3NY5=4<7=#MMeJW3K*7hV5?zBdz)hu1GVWF2$*z`gPh1aym=z;KSsNP3b#HU~! zh6u;T&%bWVCI^;@1@7rPP44EB2hFpR^7d!o?Fr!R+jI=%<}Fpc?Uc7r>oaA9r(H&` zXZeb~+q{g%4pGYJozjdRs;x(TG_n@5aIIMI$|6TMoaQSoIY-Ps{frI1sm!KrP3His zX}85?^31L}lAX>-Bxd*MLQeK2+aHN(m)kp8=I$EcHa1*TZXc57_R(DBV~gTE?QL#K zb~W7@G}M*fUtY;}8p!rh5G}CbTSc~BAsb+p2*Z5ifMu`FacGx}`&p_@ z4v-OSQ!<{ECgYh*#N4fQ;SRN}plde(1Gb zGR|Uwp~ZK&^Gziq7Gn0{eZ8}-LdQVW!GzOT?lj+4qpby`>(*jS+_L?N^zBk^Q)}I5 zJvN1%bR5%0Yw@mnwST*(?caW^C9w5~w3QjpOiHOm$8whATeW{h-ev<&wdm4@p`(BY z9PVlcE90vM^*ndja;a04@&|zO^THWkn~pr?jn`GJA|*i1q^n4o9;5iPowac7l74qf z>3ssE#|Vp({-`wRPvXj+QbhXhyq4R?DAPx6&;#B6l2320q{DoH2s7>D+v%uCN6adB z51&@*;b=E(F~ zG>3G)Wg=}l)s2!!R|y`Gu1RfkS{$ZtYo7}{6nH~1n7yqzjy9F1dekDjL4iJOss@tf zV$OI;J`_{5uW~}8MkcY?C>E!N%&Gr;$d20FWEGghL^K@Th2~ObJi}% z2y^x{=Iqqr&smwZ=b4sATs`Q9ZBJIN&Iu2eyw|VMk>_gF>Fl)ANn9<%gDr=v?Y)Gt zU9PTfnYd2CzK*pywoY?(XC@*X*f3WQieqv^lW3xjSFHo3AHrUiGnoWy1Q_# zfE@@urACmYcIYj%v|UPD=WYpOOY^R|!dA+Zi(ut;frZ0sJ!>~qOd(tk?buQQBWA5B zzhyBZWIIggFE~~towZO@v8Y&UmXdqWH{a=Ocx2m4&c0u$+4n9&?vKEL;l1PscP(#27 z+_Dyp;?D)@GBws{Lg{45)Ys)Whne(%9A-v?FM^ZIE(-2n+1B#OLE(wtu2>coO|Yof z_gLffGnHKTfm|10D+2VLX7g;XT=khc?K72VZo1_Of;7WqJA$&P<@3o5cZ!)+Y`kdj ztZ2u|KrgN=uM!Gx?aTLAMX7DJ9iSH)tedx+6}3C1Ht}YdhC|p+4wG$v$|8Lsb&FZw zVB3KO4t?9aC$|CVjMGwe-`efI5$Vbp(?dClFwD2^jvp}T+JCuU;;*(gs<59r%(bY6 zjqiG&bVvMZqIqr4=5S(1z{-uJBX8-9bSu&gHR*iaFtEb7B1}I>tCfXcOsZkBwQKK_ zDqd!#Thx8r5~P|9gj$%6JgJP#SdD5odwN`xpZ0|`De6IU_v^}8NG%@8i)`Y#==(fa zO@sf)u0=6Y7pJ5pQ|G70n{qZ;`MbJP+`3ZS26W9v+2W*(8LUF%9px%K!N5TBfkdi8 zyuX$?U4GIFQ0e`%lvM5*0hL&W`)C@@9c)I~MnI-v8;~lsLW`=__Pg%5kx7zng_4uO zU`tzDgp@|94!lELS{QFZudiM|>gdBhRAyoOM}8;lonY3T6|>4`R;w|Wau}4FV@wa# z=3C|xsRj>^D|}BAS|*D zY%5sj(JwMyNv?Pi0>fgC9T_dAilWsqg4G6o$?Cg!9ZFhHiZQo{H*hQ;maST|w4)Ta z3tclITbz`kmhWJ>DlvMZqt)`6c!*lQbDUcY?SO-6AlIPaxlnojFb!zhJ+NOuYSjy_ ztVLA-Bnf(=HA92m$kZSJa>nhS*i6Z@4#60l7e*M0IN|+5u&ds;x!i_3E_Ztwob;j)P3cq7;MIz~S=~$;YqE zMj7?`!M8nrmojMz+{9JkA|6CXo=HagadTK3QFXw$=V4b-DD|*|RNtYX-Jj{Gs0XN3u@A?@ z)S?=jo!QmA06eOIeWYB{YuZ*WG;Nz$!!_2qFYaTF-_AD2Zsz8LLCVf3+t&DZi03}t zK|G#t*QZ`r9)A@)rmc4DqS? z908(o*{x7JR1+fgoR@v&B_;I_LF!2$^^?9&9H8u_s8@tGV=5e#I*YtEG86o(D>149;`Ze9aUX4$_uAsM3T^Q?YiYL)*y7aU zdL6Y>d!0AlSvR|pE%s4`N$XEAtDN@O{F(17lLlZKcZXU05gmEcXdEl)dsTyuDJFeE ze@)MtMz^clYP7e2N!?oahg;SAP(-WMouX(RI|VEw*BN5xxUF!59=suOqGPaOulEeO1_ zsfT?L!|!A0@Czzs8DU6C|BYoEbI`UQC_}K(A8$7CO<1;X<{47?h_ir?*bzf!vH_Gr z;}!0W1&v<#5+70Z99gl|-~ZN{%F$1QqhrC(Yv`yrN_ML^Cwq$p@kU#_6`1LWyJNim z=h}t-=a$yHgrDk-tL|xYOl;l%Ebtu3fE9U`#mQkJ(sd!9)OSONr2DP#=J%AO%fi)s z8gAx;bmU1|brCytHHr3RjAj;)^d%sdZZl->tdqK>|uHHu_jfCyh!hgE?K82hfrEq6KC; zB?0PHX3^K8jSHE9>G;t16w1Nyq1SxvZ*yQmeygF#V)IpCXp(N4&*a$DaAGJWa6V-6 z$n`w$)I;x3Zr%lMo`v0KVmk8NL`fiCOOb%q^rb73zxmo4Nb7Kti1 zF}2*w&24NBEE6r4n*p8}<`pLwrMlY*n$nX0As$kWK&gC*epst#9mzx$}6LixqOrH~&1kRV^bT9~kb!hNS5KCQC9cJ*wK-}bbJh7t;)~POjS*AT)Wk}(->e$@FPmCn3uA1R5AY_f9EXoe z3lWaIz!Pu&{F_QG+IO=Ci?t9Pd8<`XtJ7XpS=2HrE|Cbnb$5+kN8V!-1JY$vFJP90 zTOmGJ<`qzn=@cs6geoRnec1_0Dn!ov<^!Qtrz20Q$`$N%x+IaRjPbAnQVrLsSc6Kc zV$Ot(5RooSNS}cuv$gA6^KPLG+W`z)3hb)WQ8A48Ftp=S1x)JJqP339Qxg-ChY^#! zwyAZ3ov_+p?^S})2Ac0E@&rq~5VVqsX4qI*HQrSIcvAtvy0wjD2eS^Qk6LjRlt>Qd2+aA z`){w4`lg4jn%I7zY^Hc!uqMn$VNZyz_cN)%Wr2%)r>SRk%$yI8QOED6;NvOa;)irp zd?aX=+q0q)hiU8rRUd-=eFm4Q1%x9u;?GASNokl`?1UDjhSPl2;d4ant(X1hjY{l^ zAU0kRTibw+Jh7`D-7FmGXJWViT02}0_@qs66T9*C8nKI+9cG}ApM2YTeg0LRTU`ma zF$mWWvdu+DML4p1)?uYkQODbgP#HbCVhvRrf}Lw;Mnavv%BnXjq4oixMuSWU{?~TM z6ADjXbrq9oAT!qtE8=?Fud~C&Ir}vH1^@y*%p$uKPV;(=Xr%L}KJc#6ji!by0;;V^ zM@2V6V7WcPR->49e5Iou)>CW1=%Lzt$DNNYsrkt04ymzzLMaKK0~W-h?d95La??Xc$z;pQ5lsL3gX@ zvcUa(rzu*o(&bxhs{A_!{M!WF!(P0#v-12ix=cE`x-qKNS**cQfQc8u&lr0;vUa2I zqj}4ccscq$MpmDrP^13n>^k(Z9zK%u)8h^JC(jRyw|0udHp`TK7y6ixEl$diKy8do zmZ=h~g_92?QuSj)tLgId9Oo888w{6cNT?_6z;*7{qAlFA*1@`yglvP#z(#{b1ymAK z=3|F7az$(lm+UVxdzL78=5J@ODFta4sAWLEadcD^BzDen6l{9k}dc%UI@N zu>XwA1mds1$^HEpc`gq)RwI% zM+7OilT{YwY;eg5CZKHNsx$eBgc@lVeKS{rL1Q z@RYGfCph&wl^S)X0_h>-i^U4@(?_G^92uZp4}Nu|vSuV$^9~sEA{`ZL2;=2;m|6`* zlw)X8b8Ck?J3>G=rl^=EUT!6PFojraMg%$kmCt@s2-5dQ5abb%<1#w(1VQGiQzTvr zac6igbLw@1G$uf+Ah)PD`z*G7;v+2V8*w90e;*xr#Iqv>*c%@TV&_wFKLMa7 zbZ`>m`DAQ#0sfc1FkTwn)_A3qPe!GzMjva?$6BfK)Jf*C*0JIp%k zwCA;G%K(Fa-NB^`b>`a~_Zek8?^8sxmJ9pQuJ zGO5-;)~nUxEO`AX#)6-RcKsV7ixcR`w=2X&5{_ehGG_6SF+hUC*%b)JtjtGMBMcKD z%*n;;$r4m^PVJAB(h-7j!`-EFOrU-ByP)?V{Uzu<()`j25;Uc%mZ7M(8eEinG4f~7 zd!@8x9=(8YpqG*BNhGhnCA2T_!?$%#X@p^w5x;^&=B6Vr6(b3*a;k|r1@2XgLW!46 zl@hN&(pyPOArH$+(IxPv(u&+P$%iW5oh1?Fc)WrcB9zHS46IU)Fu$4<%0gec5{b&_xdYzAAG};T>@kl*SG<<#I zt?u1Q8+0@pbO4P>{ev5`4ceS9%RHW!usF()QFI9>H1EtZeuWZ#XBKzZPSHnq^P5Bl zsn3~pig%q^=d{n6Wj#TiG2;GWkNoRWZMTKdZeK>5eTj~ly4|cUVIH%AF<^s@NxS~3 z)|zYeZ(O3Sh0(APGtg2*-J5c)rKT@qu^{1e-;-qSg;~5DQh+m4PR3{q42y2X)U1 zXDMYB`p|Hal!f2xCFJ*Yp{S^M2W2tec~|p;e|eoyTyj`Ke5#-LF*9$B(@RHu8%p4}bj;d9K$9QuNFqK>{U4k^ z+qQT{6qnfq0!+Pr-t&umsPLYKmVFD*rsXNedYhHhEGHo zv-m~|xkTA>DX-oXFnrrj1|50AG4MV;vkQ>*5AenOxeQ2mwO0Gy2|B?#nhZHnR|{dp zzWMWVGE!0b;3-lq&dEjrrBY^XDY;D#acFmIa7K?s#R}9BPXopnmFe3k-=?Z^2*C!`eru{{<2jHs zo>R084=PyYf%6}g`jb6PQ-apWWzMWg1+A?Gt?wq9XJyTytK}WW|vBo%l&) zwd?iecDd?3mCNTL7c7?PL&vS}xV&5dio~#_Tp<)=^t@zA>>O+iJF)RxNJ-lmjUz8c z3Gi$2kF>Z(V5mq|6016z1M9G*unp*%jod5D{b2)$3``IpmUF;a2z$u(NbJKB-gB9HH~zRGI={Q4KTbs8OcepT}F$%}AClRxZpd8eMINShdB$?P#KRZ)EstfC1e`_qwURV6B)sDO5IL97qLZc7tv%FpEuI)(>+Wr+)$ z6H%r3SVS4cry@!@^3AZQ1rhCe&6Q@b@q1v=|G=Ot>BzH)MMO$fd}+cBPO)yLnOdT5 z$@RsLBoK}73uvlbC!X=rlxdlC56ig2GiV#Dcx`hdE^lMG(Pnhn7U}Zjm)usz3%K2q z53Zwkyg({rU3k8gapBp6Hv-{Sk7@P~`|XxAM4@TqNtnlXjFD!dyR!yDg|u_vR{0Kn z8fGI^0D0wMer|n@ygbvLG3qqWara|Jkl%zLvCBl?g>>WvX)BWmG9D@IOFd#FC)JG6 z_rkfD_CZD1RZ?9+nyGZDB=h9lgc#`23#g1OrMzwE`*x{|QqQh4xf2=kH?E55e6g^O zGj-)#Vfaks!)fQ5Uvw{;O=mS+j6k+mkW-S!*Ke#NrJfB0d5=C#UXYK31*xhNV-@xK zj^|yai$$a9kRV0Xcc!C~APcuxf)MdF5UTL;F#P(8!medG-W!zTqaw%p`XjczU(MRt z5Y(?Bq}Axi3kns|ei)O^Qp*rTQW@5g|z*wFK@xk}B{KNkweRR8A}J(T>Qzd{SSN&x}cN)2yE^#tx#hY`2wL zCsL4Bp2+-V zJXGfT8$|@uW@N*Ip^!YPl*l{!l^n#eD58J&kK7=5&mEYWh7V9Z4(6Elwb?zRi$w~q(O6iFaY1@*#g>CbKbc=e0PsH%m_THV!T14z7`TmKp@;4^du$;%5HkR za!L@fYC9CPt~8A58Tr9N9VZQ%h(MZ++Ck^E;hR?=tc7AL5V}H_2jSa^={Cd}2t-hm zk^$8LccgzT7C-`dug>eZ>r}@xh@i2#WX?LIAcTSR-@v4$ijRBm3Q;u`rDLK0l&fH zB!F~=QkH)><#Qd-08?MDovkwe8Dt(q-e03*AZNKMnYSx*V@(-*=y9>dGJ@ul-%M=8 zEqM(5D5zI+l2*x+F5PhM^-Wljw!gqG(0$L)QAxHbHnW?P5ShPaeKee8@nKvuFVk&H$y!OGYhZz*pVK#d?Q?(;7ef+X{<00s5-%(r8G)As_MJpWCGj#O?uZy) zN$v?I$gVXjVar((T)n>N(<61iguaQODP|`2-$sW=Xxeqaog5&lu{EotOrmSU>KCega!%+KT(HJ~fB#8-FQmMdrX@iWgXwjSc< z8vh?X^#Ee+59o zzk`lE;E-8hokE2IjuXkdb0A>a1UsD2V=rK(K))z19xo{=qciZJrZN|=MfuiAl^buG z&ChMSJ>|47?J(kz`lJA-v&C2}$p_cbhQ?WRHZ;!Vo6tC_h8xk^TIL<+gkPs%%aqm(Os@#k@K3pj#e{HmM$<`4sJ($Wi>m1QtV(R?sTf1o1| zIJ6Y^*bJuRDHL#(hI0XzXgHGhx9T2k7XQ$Yh!D$d8~@xug;Dz}lflB2J13MKh%$tt z+a~n<8{O}9DNx||Z&N0vyhk7JJIS>u7W~!sd1S2}rK{1m5O7e3(pj61JPvSk?YVQU z&4*G<(wMzEq$(UsX({cfEke~CU_)^F?!^uI7@K)kQlVqd|C|h zq45v-(X?F^EK36{y8`3{yE9_K+{D`+Cpawij!<||{3NK4l>rpeso zO;F)>PLEVYxM$ixvdLQvneOZkTE~FONQ*afp>12mozRQ0Rpj zJJcktS`_go?P6jiP>bf|Rtm*$1zPKj;$&pmQRv7U>iORuQ#GluEsR>SuPDUs19oP*Mj%u>U~6Z~pf2QN1*v z=P32%mDWy$Q}Y{Cy=V)t63gf-xzgxJ*DM+W#*^sY2hc}WU$KB#FdnNZN~oET9u@r= zeG(FRTGXa|Si-`@@P$4AaMe8kNJaDFM^LkWIP#C*rnb0&` z(4fB^9SgvGmX5q?L2Xq|)Ff(eoKtyEiz=&gHU%{CQaA&+8t()JrJOCKE}JQuL8DgC zds9q&*Ynye)Z8$E_|QmAl8i|+jzb#+jgD8SYOyolx!`k>+Q%BFF_9PLsYQvnPxfc$ zz7-xM>8DGJ(wX>4`gjT-)SmIH`0=a@n$(B|z0D~8J2zR8Nz2(H7&L!aC!I6-WxkO+ zzsvJqm|H=H-DV=}aNBpc+q~^#3t$Rc zRP-N6M;=oEpjS8XdH%>c=Tzxg$l3{}t}}9DopPgr3oD%%vsCCbTFXVu-6oTRsfSWI z9y2*w!4%=eb_V0$cI5qTBw##9Y{wun483m+OhSXAS8XO&X(*$=}8mGva3iR|;;Ntwpo* zC#`Yd9Iw&2c`eEUK?%Q&G@ZnTN^SCMUw&BOhqdq#Vqg6?(2<89YRVPk57dyH4ds}g z=NxJOepd3v2E$N71o1Dz@cVrM{9dMOUoqf%7eCB25_U6F(@1L3NTh$zW$f*K;rY8M z_RtH6J_g+Vf{qG%U>4iNq3H<_Q0@tXjD~5AY0m1nKhw43p|J*g6F>gXF{C`I&mI~j z!>l6xKaD`vTFlk24o%m>o6kS07+eDw+z$BLnT|XLk-2i}XtufOOJ~im zIe7`kB&eXzd*lcYY0Lw z3T@Y5vx8p$oT6xZpy)&(2s@_rf4)M|fNHX)oj4yD+75)Zg`xy2OnJlm8Szu%`gmSX zAbN#9{rV@Zcaq%vEqsZ^*Rs#-wTOc+j1BdFk&ZmRP%yvY%7(*9LYO>F@8Cpr$QQIobD{sFv-{!#0!N3gmnCU+|j~i5m?<%*hJg%I_H5eALL)`q=#f{gVLE)s0muMh9?E_ja zGX)!tIrxrAjxyREfZB_W3RFfJHSK1p3NUdfnd{YVu%Scryy2q92L@xUyvPb0IIE0C zT|4_z4sLb>X7->XkDJO#A`fM-f>a&i=J9UhW{r)PTTpRB(@8G@W*(;_j2n#@u(PO} zZE+<{O`Z9b>{00{Bcx&F{w=hAS&^$>$jk=4edMz&8z z$#zd97l@-NWm$gW?3;<$DKS8#*Am4Wrh%9UMO-?*8{Q6!oD-zP-T7Zq*Ax(^h=fpg zcWoX6(X6fF{Jce#eVW)z@Dd;zSjuE)1525=9GeB{nc%2t6=?^>23Ny2m^Kj}#e$6M zf?TBm5n*=0VdTf5yvMEpoEtQooDwAPebo!TWO_aFpjD9(`yH|U6|e(}s^cYt zq?N7`Yf-)9(*^I`u;j_~94i~XV3FIM0a&1dvr0}EUt z_^g#CMHK%|k-}gkq|iz1#-VuSN|LMuP6A&AInJ@#2zrWhDcmr{%!fvK?^Z2Zx(jIB za*rilG@b(_24?=?;p8b2hMHY~^*Q5ZS>Q*|TepheSw#@Fbm4D*opPSW`MjSqi+DhGeFE5PRT;}5UA zW&ADHA^tpD@)h)(mmBv>7nyh?NdK#Jb6<<*_ak#@MW(D{D_UX|h}(pt(*?*};o0jSRGo=A<2-M?>PfSgRz^>H@Q_J# zd5u2)jt^EMI(c?M5%Em|VgS*_AbUwZ_Uc4?%*fjEvOl z2c2`MK_Sf`KLNV2>QV~|O}JaSxPu>8v>4(pO9RVI0DO@?Xys@D3V9_m?*L~qg)ulv zLAIbDgYwd=T7(tl=vox2&0-9Gdf z`$;AETPo5|L}c1lG=+I0bI!gA5IZz4=w9b@`nD#G}hXm9RH8#IHEBI0w%0aFi{#T%Y!qWD@KlBgv zSC>E$m;>YiMfOzsxBen99^hCUX5cA0DsT|MJJuK}f)hA^42uyqh4GBM zk}x}5paQq%m4sLWuaZcM88=IXh3qd9{E16#W44_9F9g31G{Q(a@`7iUCm*6CDnk($ z7>Yp_dpOb(S~q5)zz`uk>~_b4pI0jp0T0;Srhh3q@_4AMgnc0#8F%A4*p4YHfALw^ z5k?-gFR?zJo{*oMJ16Bj<71?!-8jWq7fE~t6bWbAs|6^KaRY2c_I-;ClSJ}@8qVxa zE2wAQ%`)n{PcESr0-c2jE=1qWbmW1N=m`E+DGKQarF}e+TUz*o28%@4h;-HK`|P^m z3o6?CA=-H%)*sSQiMA=zA7p$Z^^Xe!plFHYMBp5q?d0y$rY<>Ig^MxpBH>mFy)}j2 z6XIR))-w)Jdku#@!nD`;aykOsCAE{p8CXBhB(uK20kG9B@L;#y>}|-BvhRjxa@l>P zb*9&6H3~32E!BjeGzCNqHChedIfWY#AC#j1thrOI?=sxc6jYoW6UZc`uHr{aikG$kflR*Ci ziGg^9C%-9x9Mr8AzRLjq9svGF06P{r#hyh@ED36a1n@J{+#W_nY#`2Xv=A4-f68JS zqQ?7f6*!XhTAP@{+RO_0wGE)x_XB=QlfG@E*qb8TVA2J;{T@inowioG|MLr*9bR4m zs-FO&5sHsJq4)~b7Py_EniU+kCO+Ig*aKAVgBh6E&YNbApQc>TSml!N#?_|EIAq0T zX+>b}A!y&50ZfhnPf#vQAXe+zqXgL40DSYz^C$uE z_C+BGhLP|jU2=5Xz=|PCd+yJg4?gvT`uopK_eg%*G#nLvMl$9 zq#xe^zc;0d#Yei$pc{G83LLuJdi?mV=0kIlZ!ZP>QT*xjwb;c~WuiVgD)3Jio!G_I z5t_ZY3+BOf^L^cboeVoBSavj_{u^Wo0^czSh9vZ#z5ZjbF|dCUuzvuM#{#GL)I982 zGSp^?*UzV_ZY}}cc5@l_*ZN_9vuV6`VgI-n_RpGP6WG6+f;~u(2(6p2U&p|D1NZ*8 zqZ);+O!{_Qqb?bR08I$)qb@z+Q>x|v47j7C8)F)5e0&9WV7MJ`s0FwO-J+infqtGr zOwKLRcUKrB^Ns)F zu%Fyb*pJ`&>R+j{|EKyk7X$VeSFi`BOlKFM!7tOvKmv5A<)#(bcc<9}p3=zzVi!>2N8!U7-Fy{7neMG>UMoGQYqJz3g zgjK$KiB8|{!-CA{QIOzMbW}tDy1VTEtNtV@vr54SDPa8vRxm>}e9xxlaq$-t-OFcN z?(Sw_9((mYrr4|d)RDg5)WCSGu@_WlqP%!Mc&#&?s71Rr2Xjw&KXLB^iNQD!^?(=q z_=AQ4V?v z6#brt0sC481OhfL&>Lh4LLTZRHAma@iNS=^-hb-%+C2aZqC3HYgXpMiL7TQ9qc~OZ zi9%N;sONIN&=8D_WjOH>FDJ08Nf}n5jWAFl;JujkAzdOu_4)#jF0NSbUldq>8#sTF zjy%>uj4A@uI0DoG)`wskL|wwI)+^pIhk^Cq0PAM}>Fepp!x}9j{jn+#godyI($;4K4Hc}h-G&drU{}>b?_^(ArMS-rl{k=*7vLW=UX8If@>P}-dY3srn zmgmnEoNQtqlIRZft44V?GwiUV23nw|?_$z-V>ULL2Vvmr7y}0_u-4T6K?*FsN7KY-=a7iEx7P}onW+lu zy-fPVra;}$YcF(UcDnCC^Zs+1$b;R(;z@K=i0_(z9vsN(`3|j6VnxRK$`01Eb5l73 z?Tk~4ws5kA^}HL)^u;<4GnBy2IPjx8*7Ikay@ZQ;>XjZqM;`T15taL%=y@~0p>_8? zi29xnSqkcxW;ie7z}buX^*GxGPPQ=W-7zd5>JKoeKe!y!FZYk_KcOBw&0fG#`uGAm z@~E%8o2I-QLPoDo&Ci5r8Vp$p)<-jlmvunw#X7wKhR(u8=*C! z;X8ABwpngAB|<;k`#$V6R>S|A$IY+Qe~Jhp_0L4;@yYrbA~cx2AVgS%5x$s%a4!*7 z=WJ^_*}_EF#sGZ>zxThlN#CzIA_V)iLAPJKyxG`}oF-y0bz!2yFn0tJo^-1_=^ z#SHbI4E7;tR6CN6ycw$4S2p{CUf6J(L?`^DH!ap8-F`LPJEs>d)}paZ@zd>n`wZ3L zhM(AgwHZU@=Z%uBATgK}NC*%vXefz^lP`YJF!6jaaU-zsY&!BxtQ^7=6RU~c&ctq^ z;#$nHbsUa)P31P6Z96Ah*i^dxA0HKuH&i^?QnAw!?jT(f>sWA$AO{0h)k9^X<)pJ_ zT%ZPW3(#^7P;wqRDq6M~lVkU^xv7Og1KHcljD&-|ADIgfAz_!-_oQSGSLCWdLS_vg zjNR>%4XdzJwQmD33jb@>l2z#9ZckYcvTEqvPG<}VUvtLpW!C%ofA{2PEb-oX}Qy#AJP}Vd3~QjXurnPM#M=ypHHNsrs#%w%fHAaG8_03W<6k_T$W1~|)Lp;s_P*)0ZMA4V z$*p+&|Mspt$co~OzuoQS5LZ!SBzQy+BVr^7L_<`Zs8PXN3-1sV6igI8J6cqCrYkU~vUunV$C^yYKBTFn{#C zH+_8F{e8dh>#uuyrqeZYhJE*8a9Ac$3MR_ zI7ZMBnC&fl3IIG5s7^|}ju8{=!OS5U-Pd$~2Xr0JP_v+o70hYfAd3SH{L5k1i zwEdGp9;C3z<*VcDBoH_XKOVScnb}4-GR+6+VI5OeswI62mh?gR0V64tAZ?nrZ8k;* zQXNML_gm|PviT?;`usp2#Sa0&qbTH2jJ9~bOzF|;BFUEhdWQh4%A~RpD}T*L@x_xn z2B|IXf-UX@g0U6I4a%dqbQl!34g2hBTDtM#1fq3^fLIMZLXE8Tmh{vn-Ma#3w{T&> zreDEn87(Nx`@>2fxQhVV?I`4di-wfuH}Q1KXZ-CgRX-0<7jUaB!r?J~0j>$SQ$AVt zx>{U1tCGHCcL9YGxG-={{;FxA8@!Ed5o-jrL&&cR_}M4?*#J+UFdqKTpbudiqko8Pto&liu!vqd}sX@8(pfo`sN(CTiT zFGcrf70A3UTH|m7>U4X{IKKAm9he?#1wAb+@Nvv@uOmwh8da04BnI^|5J}$H^p9^h z%{&5{xg)f44+?qB1kcK8L_?<$g__y--dIL4YaF&9irI+wM0>870h}iqS#5)HVZlO8 zD@Y)h)w8U$IwvsK&Ks=YhGtRQn! zA1lz0+lIb~)^nvO^o?|Q2(5`#PbwTz3KGbvI^pP(Ref5q^Q`5!7)9{R&UNM0ryNP@ z8cBMfK7FunA~UAcI2S_ZB#n4kzb^GDbb!oBD!_G;9MGYF+G!N2!?y_#3)Y&65#2s{BGU{Q*I~K?NGHG!e0q)#Sb9mLokAY4 zr3FqozC|kr4A`yeD1l}GHh{)>m8*FF7XkL>*~>fB!oCX&`#iu}9(`nP^0vFjJ+(I0 z-cn;%RUbe)g!rni#6^=fD$v{Z#}n;=c$)1f}_6*W% zZ0v0Y(!1wv#P+=q^|~lrZTD|*DLD{HBgKt(UAjs~ioar{_zgyi`zVwO)O=sOKP!;T z6N0Z-_d9I~Ks&gjFq@C?|GDv_4gYwW!iy{A_d`ohsh8m&@_W3YAe3A8nhg~4R=u3Crre?}dBWPiFk9gN5IPT^w#-N89Y7{tOl|vH9-YX{OH_DJ z#>=|29yORQLvZ0lT=YwllSCJkW;C6_MF6TfpUHFam>&}KO80+M<^`$_$4(E495 zqq6{hu~7}LTN65G%ozT@+RoQtJAVpqcshkVI?<)_am&{BxTTkI8XDT`nBoQfTa?SX zxD>@zMA0R$ooBdS4_vPUrhh;ok83DFX>}7^7cG@w=n(ba{4eGA!K3qD#&!4XubSsV z-_|rEpfw@n%SlFL)Q?*J>%G*d&j$Ffg}dLnS-Eyha!r$fAt<8e%AqdKc|p~AG%Wd6p8IEnva$6Q&Z{v6vOYvyRSJ)tY78G zN~Q8ygfl2);m3NET*L|BnHNCm2HI?jZg!xXD4O;A!TN2X$^oFbGr|N4LCQ2W19hIS zfy4kIvD<;W>yeF>;V3#7fqsVvNuYQX9sI8oBJIv7=xlh=419WUrcWM+swYojA)933j}4oXqv zk0KwIE@8dU{-DgsS_ze(rvJI*d4BCP?S^aAxu|^q-CbpADJx4is7>EjWJwQu=as3# z^p=s0WtX$|SEn1DrRP2mqHZi*#-%EwzEhtl1DG3kU8Ty|Y_cgs? zPR+6#zPnuRK>A86!SUDIomcs7+AQX$->OB*&y(Kz<0j?j6!7y|@DkI(mURXEWDce| zD?KIJh)*FEE!<9ckU}aKK-y;nlx|P26fv#S9fZ{VwKv2CbbGv@t+vL0-;WlE_wY}lJJH^ zz;vF7$zO~#wYLdg{yO*?7`k2%g4wAK?I)~IvB!|2Anr*|Zw1!3XQ>%yc2 zIsj4uke7mV%nCWil;v=Z`wHD0CAqYa72(QGmom)M)U!q5@0!zIPkxk@P3%^CKldvaa>P@H~n|BUQ*4w9-6lbS~r?PUh_)fC4eH3 zi3kO2-$#;)lJUo)e?)QVVe)A!CfQjLUy9>MmQmY^2_LIKuNpKFu35deL5#MFXRPrZ?toG^rI@m#9|l79h@SjP!>KMBh_>7l8dC-$W84r zcbh5K?QXkyLf+FI>IvGLbeh>uRorhWrZjPi$R&7mP1@ekLfDvFuQqX<266lZ!~RAJ zd2t}KKe{uI2YW4ZL#bIi)8$jzHqUIiy(wX&j|G?p?H=2(@hNf82;>f<%j6WXlsHb3 z>Jv%uKM{v{phUtf8;ip%n^-fO?|{q5r~*)L;Z`AEmpC5MRbC+`o`QT@uKS;nK@pt-+|r?Ln8lL;xf3A3{@}D$bFt zUaZD*Hz#G3f+N35w2l>8Q`594ot4p@EwyLyk5m-CRGUWs&Eb+!+8i#f=w@Rw7a}i~ zoCS@*1U$_jZxdEL^43nD+M@m-_a>E1#E)~fD| zx_9APmE2!oooH+CKPcoShibBn=cu9yAKI?)X9NxNdTg$*R9iRFcNhp>9$s%P2e-R>l9_I3>2WB$SZ{6P=%a}rt$9O5iN{+NyqVv+FNM4)(PVE#XI0`>#!cl6 zFyMX<7^!r;o*PP+ovmF2LS6gBni7-96{Ex5-GO;>@zMtzPrne;JXWKa!O2BbCe~=q zI>Us-jkKi?PWpx>fjru9t=!??4H_>kW|`bhIqnp`lZ}ZzOPq~}l*LJknkK5iG79e~ z2IT;mD7xl9lg|-(w4Mkfipg->qZIP;Fl0zsB~I;S;_wcHIQL*zL_1o-ptMAE!WBB1 z8D^Aw6Hm6pwBfK=N=!|)JhDeqA|_i|il$7Kq)wfXu#$+lOiVnolvRM@E@Y19;3bOM7vbzB=jMQy`ks6tq z8^SFGnQK?(r9j46?X>Bf%y%LtU@?t;Fdb4#49?J8C}Fi5M@7cxQKb7lnc|W8 B × A; + inv_braiding {A B : C} : B × A ~> A × B; + braiding_inv_compose {A B : C} : braiding ∘ inv_braiding ≃ c_identity (A × B); + inv_braiding_compose {A B : C} : inv_braiding ∘ braiding ≃ c_identity (B × A); + + hexagon_1 {A B M : C} : + (braiding ⊗ c_identity M) ∘ associator ∘ (c_identity B ⊗ braiding) + ≃ associator ∘ (@braiding A (B × M)) ∘ associator; + + hexagon_2 {A B M : C} : (inv_braiding ⊗ c_identity M) ∘ associator ∘ (c_identity B ⊗ inv_braiding) + ≃ associator ∘ (@inv_braiding (B × M) A) ∘ associator; +}. + +Local Close Scope Cat. \ No newline at end of file diff --git a/ViCaR/Classes/Category.v b/ViCaR/Classes/Category.v new file mode 100644 index 0000000..f756e32 --- /dev/null +++ b/ViCaR/Classes/Category.v @@ -0,0 +1,80 @@ +Require Import Setoid. + +Declare Scope Cat_scope. +Delimit Scope Cat_scope with Cat. +Local Open Scope Cat. + +Reserved Notation "A ~> B" (at level 50). +Reserved Notation "f ≃ g" (at level 60). +Reserved Notation "A ≅ B" (at level 60). + +(* + Might use these to abstract out the equality relations. + + Definition relation (A : Type) := A -> A -> Prop. + Definition reflexive {A : Type} (R : relation A) := + forall a : A, R a a. + Definition transitive {A: Type} (R: relation A) := + forall a b c : A, (R a b) -> (R b c) -> (R a c). + Definition symmetric {A: Type} (R: relation A) := + forall a b : A, (R a b) -> (R b a). + Definition equivalence {A : Type} (R : relation A) := + (reflexive R) /\ (symmetric R) /\ (transitive R). +*) + +Class Category (C : Type) : Type := { + morphism : C -> C -> Type + where "A ~> B" := (morphism A B); + + equiv {A B : C} (f g : A ~> B) : Prop + where "f ≃ g" := (equiv f g) : Cat_scope; + equiv_symm {A B : C} {f g : A ~> B} : + f ≃ g -> g ≃ f; + equiv_trans {A B : C} {f g h : A ~> B} : + f ≃ g -> g ≃ h -> f ≃ h; + equiv_refl {A B : C} {f : A ~> B} : + f ≃ f; + + obj_equiv (A B : C) : Prop + where "A ≅ B" := (obj_equiv A B); + obj_equiv_symm {A B : C} : + A ≅ B -> B ≅ A; + obj_equiv_trans {A B M : C} : + A ≅ B -> B ≅ M -> A ≅ M; + obj_equiv_refl {A : C} : + A ≅ A; + + c_identity (A : C) : A ~> A; + + compose {A B M : C} : + (A ~> B) -> (B ~> M) -> (A ~> M); + compose_compat {A B M : C} : + forall (f g : A ~> B), f ≃ g -> + forall (h j : B ~> M), h ≃ j -> + compose f h ≃ compose g j; + + left_unit {A B : C} {f : A ~> B} : compose (c_identity A) f ≃ f; + right_unit {A B : C} {f : A ~> B} : compose f (c_identity B) ≃ f; + assoc {A B M N : C} + {f : A ~> B} {g : B ~> M} {h : M ~> N} : + compose (compose f g) h ≃ compose f (compose g h); +}. + +Add Parametric Relation {C : Type} {Cat : Category C} + (n m : C) : (morphism n m) (equiv) + reflexivity proved by (@equiv_refl C Cat n m) + symmetry proved by (@equiv_symm C Cat n m) + transitivity proved by (@equiv_trans C Cat n m) + as prop_equiv_rel. + +Add Parametric Morphism {C : Type} {Cat : Category C} (n o m : C) : compose + with signature (@equiv C Cat n m) ==> (@equiv C Cat m o) ==> + equiv as compose_mor. +Proof. apply compose_compat; assumption. Qed. + +Notation "A ~> B" := (morphism A B) : Cat_scope. +Notation "f ≃ g" := (equiv f g) : Cat_scope. (* \simeq *) +Notation "A ≅ B" := (obj_equiv A B) : Cat_scope. (* \cong *) +Infix "∘" := compose (at level 40, left associativity) : Cat_scope. (* \circ *) + +Local Close Scope Cat. \ No newline at end of file diff --git a/ViCaR/Classes/CategoryTypeclass.v b/ViCaR/Classes/CategoryTypeclass.v new file mode 100644 index 0000000..51197f3 --- /dev/null +++ b/ViCaR/Classes/CategoryTypeclass.v @@ -0,0 +1,9 @@ +Require Export Category. +Require Export Monoidal. +Require Export BraidedMonoidal. +Require Export SymmetricMonoidal. +Require Export Dagger. +Require Export DaggerMonoidal. +Require Export CompactClosed. +Require Export DaggerBraidedMonoidal. +Require Export DaggerSymmetricMonoidal. \ No newline at end of file diff --git a/ViCaR/Classes/CompactClosed.v b/ViCaR/Classes/CompactClosed.v new file mode 100644 index 0000000..1a966eb --- /dev/null +++ b/ViCaR/Classes/CompactClosed.v @@ -0,0 +1,28 @@ +Require Import Category. +Require Import Monoidal. +Require Import BraidedMonoidal. +Require Import SymmetricMonoidal. + +Local Open Scope Cat. + +Reserved Notation "A ★" (at level 0). + +(* A compact closed category is a right autonomous symmetric monoidal category *) +Class CompactClosedCategory (C : Type) `{SymmetricMonoidalCategory C} : Type := { + dual (A : C) : C + where "A ★" := (dual A); + unit {A : C} : I ~> A ★ × A; + counit {A : C} : A × A ★ ~> I; + + triangle_1 {A : C} : + inv_right_unitor ∘ (c_identity A ⊗ unit) ∘ inv_associator + ∘ (counit ⊗ c_identity A) ∘ left_unitor ≃ c_identity A; + + triangle_2 {A : C} : + inv_left_unitor ∘ (unit ⊗ c_identity A ★) ∘ associator + ∘ (c_identity A ★ ⊗ counit) ∘ right_unitor ≃ c_identity A ★; +}. + +Notation "A ★" := (dual A) : Cat_scope. + +Local Close Scope Cat. diff --git a/ViCaR/Classes/Dagger.v b/ViCaR/Classes/Dagger.v new file mode 100644 index 0000000..391ab78 --- /dev/null +++ b/ViCaR/Classes/Dagger.v @@ -0,0 +1,22 @@ +Require Import Category. + +Local Open Scope Cat. + +Reserved Notation "f †" (at level 0). + +Class DaggerCategory (C : Type) `{Category C} : Type := { + adjoint {A B : C} (f : A ~> B) : B ~> A + where "f †" := (adjoint f); + + involutive {A B : C} {f : A ~> B} : f † † ≃ f; + + preserves_id {A : C} : (c_identity A) † ≃ c_identity A; + + contravariant {A B M : C} {f : A ~> B} {g : B ~> M} : + (f ∘ g) † ≃ g † ∘ f †; +}. + +Notation "f †" := (adjoint f) : Cat_scope. (* \dag *) + + +Local Close Scope Cat. diff --git a/ViCaR/Classes/DaggerBraidedMonoidal.v b/ViCaR/Classes/DaggerBraidedMonoidal.v new file mode 100644 index 0000000..7ca1dd8 --- /dev/null +++ b/ViCaR/Classes/DaggerBraidedMonoidal.v @@ -0,0 +1,14 @@ +Require Import Category. +Require Import Dagger. +Require Import Monoidal. +Require Import BraidedMonoidal. +Require Import DaggerMonoidal. + +Local Open Scope Cat. + +Class DaggerBraidedMonoidalCategory (C : Type) + `{!Category C} `{!DaggerCategory C} `{!MonoidalCategory C} + `{!DaggerMonoidalCategory C} `{!BraidedMonoidalCategory C} : Type := {}. + + +Local Close Scope Cat. \ No newline at end of file diff --git a/ViCaR/Classes/DaggerMonoidal.v b/ViCaR/Classes/DaggerMonoidal.v new file mode 100644 index 0000000..6465359 --- /dev/null +++ b/ViCaR/Classes/DaggerMonoidal.v @@ -0,0 +1,28 @@ +Require Import Category. +Require Import Dagger. +Require Import Monoidal. + +Local Open Scope Cat. + +Class DaggerMonoidalCategory (C : Type) + `{!Category C} `{!DaggerCategory C} `{!MonoidalCategory C} : Type := { + dagger_compat {A B M N : C} {f : A ~> M} {g : B ~> N} : + f † ⊗ g † ≃ (f ⊗ g) †; + + associator_unitary_r {A B M : C} : + associator ∘ associator † ≃ c_identity (A × B × M); + associator_unitary_l {A B M : C} : + associator † ∘ associator ≃ c_identity (A × (B × M)); + + left_unitor_unitary_r {A : C} : + left_unitor ∘ left_unitor † ≃ c_identity (I × A); + left_unitor_unitary_l {A : C} : + left_unitor † ∘ left_unitor ≃ c_identity A; + + right_unitor_unitary_r {A : C} : + right_unitor ∘ right_unitor † ≃ c_identity (A × I); + right_unitor_unitary_l {A : C} : + right_unitor † ∘ right_unitor ≃ c_identity A; +}. + +Local Close Scope Cat. diff --git a/ViCaR/Classes/DaggerSymmetricMonoidal.v b/ViCaR/Classes/DaggerSymmetricMonoidal.v new file mode 100644 index 0000000..07f5dc9 --- /dev/null +++ b/ViCaR/Classes/DaggerSymmetricMonoidal.v @@ -0,0 +1,16 @@ +Require Import Category. +Require Import Dagger. +Require Import Monoidal. +Require Import BraidedMonoidal. +Require Import DaggerMonoidal. +Require Import SymmetricMonoidal. + +Local Open Scope Cat. + +Class DaggerSymmetricMonoidalCategory (C : Type) + `{!Category C} `{!DaggerCategory C} `{!MonoidalCategory C} + `{!DaggerMonoidalCategory C} `{!BraidedMonoidalCategory C} + `{!SymmetricMonoidalCategory C}: Type := {}. + + +Local Close Scope Cat. \ No newline at end of file diff --git a/ViCaR/Classes/GeneralLemmas.v b/ViCaR/Classes/GeneralLemmas.v new file mode 100644 index 0000000..7de0640 --- /dev/null +++ b/ViCaR/Classes/GeneralLemmas.v @@ -0,0 +1,37 @@ +Require Import Category. +Require Import Monoidal. + +Local Open Scope Cat. + +Lemma compose_simplify_general : forall {C : Type} {Cat : Category C} + {A B M : C} (f1 f3 : A ~> B) (f2 f4 : B ~> M), + f1 ≃ f3 -> f2 ≃ f4 -> (f1 ∘ f2) ≃ (f3 ∘ f4). +Proof. + intros. + rewrite H, H0. + reflexivity. +Qed. + +Lemma stack_simplify_general : forall {C : Type} + {Cat : Category C} {MonCat : MonoidalCategory C} + {A B M N : C} (f1 f3 : A ~> B) (f2 f4 : M ~> N), + f1 ≃ f3 -> f2 ≃ f4 -> (f1 ⊗ f2) ≃ (f3 ⊗ f4). +Proof. + intros. + rewrite H, H0. + reflexivity. +Qed. + +Lemma nwire_stack_compose_topleft_general : forall {C : Type} + {Cat : Category C} {MonCat : MonoidalCategory C} + {topIn botIn topOut botOut : C} + (f0 : botIn ~> botOut) (f1 : topIn ~> topOut), + ((c_identity topIn) ⊗ f0) ∘ (f1 ⊗ (c_identity botOut)) ≃ (f1 ⊗ f0). +Proof. + intros. + rewrite <- bifunctor_comp. + rewrite left_unit; rewrite right_unit. + easy. +Qed. + +Local Close Scope Cat. diff --git a/ViCaR/Classes/Monoidal.v b/ViCaR/Classes/Monoidal.v new file mode 100644 index 0000000..9caad41 --- /dev/null +++ b/ViCaR/Classes/Monoidal.v @@ -0,0 +1,77 @@ +Require Import Category. +Require Import Setoid. + +Local Open Scope Cat. + +Class MonoidalCategory (C : Type) `{Category C} : Type := { + tensor : C -> C -> C; + I : C; + + tensor_morph {A B M N : C} : + (A ~> M) -> (B ~> N) -> (tensor A B) ~> (tensor M N); + tensor_morph_compat {A B M N : C} : + forall (f g : A ~> B), f ≃ g -> + forall (h j : M ~> N), h ≃ j -> + tensor_morph f h ≃ tensor_morph g j; + + (* These are all isomorphisms *) + associator {A B M : C} : tensor (tensor A B) M ~> tensor A (tensor B M); + inv_associator {A B M : C} : tensor A (tensor B M) ~> tensor (tensor A B) M; + associator_inv_compose {A B M : C} : associator ∘ inv_associator + ≃ c_identity (tensor (tensor A B) M); + inv_associator_compose {A B M : C} : inv_associator ∘ associator + ≃ c_identity (tensor A (tensor B M)); + + left_unitor {A : C} : tensor I A ~> A; + inv_left_unitor {A : C} : A ~> tensor I A; + left_inv_compose {A : C} : + left_unitor ∘ inv_left_unitor ≃ c_identity (tensor I A); + inv_left_compose {A : C} : + inv_left_unitor ∘ left_unitor ≃ c_identity A; + + right_unitor {A : C} : tensor A I ~> A; + inv_right_unitor {A : C} : A ~> tensor A I; + right_inv_compose {A : C} : + right_unitor ∘ inv_right_unitor ≃ c_identity (tensor A I); + inv_right_compose {A : C} : + inv_right_unitor ∘ right_unitor ≃ c_identity A; + + bifunctor_id {A B : C} : + tensor_morph (c_identity A) (c_identity B) ≃ c_identity (tensor A B); + bifunctor_comp {A B M N P Q : C} + {f : A ~> B} {g : B ~> M} + {h : N ~> P} {k : P ~> Q} : + tensor_morph (f ∘ g) (h ∘ k) ≃ (tensor_morph f h) ∘ (tensor_morph g k); + + (* Coherence conditions for α, λ, ρ *) + associator_cohere {A B M N P Q : C} + {f : A ~> B} {g : M ~> N} {h : P ~> Q} : + associator ∘ (tensor_morph f (tensor_morph g h)) ≃ (tensor_morph (tensor_morph f g) h) ∘ associator; + left_unitor_cohere {A B : C} {f : A ~> B} : + left_unitor ∘ f ≃ (tensor_morph (c_identity I) f) ∘ left_unitor; + right_unitor_cohere {A B : C} {f : A ~> B} : + right_unitor ∘ f ≃ (tensor_morph f (c_identity I)) ∘ right_unitor; + + (* Commutative diagrams *) + triangle {A B : C} : + associator ∘ (tensor_morph (c_identity A) left_unitor) + ≃ tensor_morph right_unitor (c_identity B); + pentagon {A B M N : C} : + (tensor_morph associator (c_identity N)) ∘ associator ∘ (tensor_morph (c_identity A) associator) + ≃ @associator (tensor A B) M N ∘ associator; +}. + +Infix "×" := tensor (at level 40, left associativity) : Cat_scope. (* \times *) +Infix "⊗" := tensor_morph (at level 40, left associativity) : Cat_scope. (* \otimes *) + +Add Parametric Morphism {C : Type} + {Cat : Category C} (MonCat : MonoidalCategory C) + (n0 m0 n1 m1 : C) : tensor_morph + with signature + (@Category.equiv C Cat n0 m0) ==> + (@Category.equiv C Cat n1 m1) ==> + Category.equiv as stack_mor. +Proof. apply tensor_morph_compat; assumption. Qed. + + +Local Close Scope Cat. diff --git a/ViCaR/Classes/SymmetricMonoidal.v b/ViCaR/Classes/SymmetricMonoidal.v new file mode 100644 index 0000000..801a761 --- /dev/null +++ b/ViCaR/Classes/SymmetricMonoidal.v @@ -0,0 +1,11 @@ +Require Import Category. +Require Import Monoidal. +Require Import BraidedMonoidal. + +Local Open Scope Cat. + +Class SymmetricMonoidalCategory (C : Type) `{BraidedMonoidalCategory C} : Type := { + symmetry {A B : C} : (@braiding C H H0 H1 A B) ≃ inv_braiding; +}. + +Local Close Scope Cat. diff --git a/ViCaR/dune b/ViCaR/dune new file mode 100644 index 0000000..ad28400 --- /dev/null +++ b/ViCaR/dune @@ -0,0 +1,4 @@ +(include_subdirs qualified) +(coq.theory + (name ViCaR) + (package coq-vicar)) diff --git a/_CoqProject b/_CoqProject new file mode 100644 index 0000000..be3d169 --- /dev/null +++ b/_CoqProject @@ -0,0 +1,2 @@ +-R _build/default/examples/ Examples +-R _build/default/ViCaR ViCaR \ No newline at end of file diff --git a/coq-vicar.opam b/coq-vicar.opam new file mode 100644 index 0000000..b630cfb --- /dev/null +++ b/coq-vicar.opam @@ -0,0 +1,33 @@ +# This file is generated by dune, edit dune-project instead +opam-version: "2.0" +version: "0.1.0" +synopsis: "Coq library reasoning about categorical string diagrams" +description: """ +inQWIRE's ViCaR is a library for reasoning about + categorical string diagrams +""" +maintainer: ["inQWIRE Developers"] +authors: ["inQWIRE"] +license: "MIT" +homepage: "https://github.com/inQWIRE/ViCaR" +bug-reports: "https://github.com/inQWIRE/ViCaR/issues" +depends: [ + "dune" {>= "2.8"} + "coq" {>= "8.12"} + "odoc" {with-doc} +] +build: [ + ["dune" "subst"] {dev} + [ + "dune" + "build" + "-p" + name + "-j" + jobs + "@install" + "@runtest" {with-test} + "@doc" {with-doc} + ] +] +dev-repo: "git+https://github.com/inQWIRE/ViCaR.git" diff --git a/dune-project b/dune-project new file mode 100644 index 0000000..a57ea96 --- /dev/null +++ b/dune-project @@ -0,0 +1,21 @@ +(lang dune 2.8) +(name coq-vicar) +(version 0.1.0) +(using coq 0.2) + +(generate_opam_files true) + +(license MIT) +(authors "inQWIRE") +(maintainers "inQWIRE Developers") +(source (github inQWIRE/ViCaR)) + +(package + (name coq-vicar) + (synopsis "Coq library reasoning about categorical string diagrams") + (description "\| inQWIRE's ViCaR is a library for reasoning about + "\| categorical string diagrams + ) + + (depends + (coq (>= 8.12)))) diff --git a/examples/ZXExample.v b/examples/ZXExample.v new file mode 100644 index 0000000..3d8b82a --- /dev/null +++ b/examples/ZXExample.v @@ -0,0 +1,578 @@ +From VyZX Require Import CoreData. +From VyZX Require Import CoreRules. +From VyZX Require Import PermutationRules. +From ViCaR Require Export CategoryTypeclass. + +#[export] Instance ZXCategory : Category nat := { + morphism := ZX; + + equiv := @proportional; + equiv_symm := @proportional_symm; + equiv_trans := @proportional_trans; + equiv_refl := @proportional_refl; + + obj_equiv := eq; + obj_equiv_symm := @eq_sym nat; + obj_equiv_trans := @eq_trans nat; + obj_equiv_refl := @eq_refl nat; + + c_identity n := n_wire n; + + compose := @Compose; + compose_compat := @Proportional.compose_compat; + + left_unit _ _ := nwire_removal_l; + right_unit _ _ := nwire_removal_r; + assoc := @ComposeRules.compose_assoc; +}. + +Definition zx_associator {n m o} := + let l := (n + m + o)%nat in + let r := (n + (m + o))%nat in + let assoc := Nat.add_assoc n m o in + cast l r (eq_refl l) assoc (n_wire l). + +Definition zx_inv_associator {n m o} := + let l := (n + (m + o))%nat in + let r := (n + m + o)%nat in + let assoc := Nat.add_assoc n m o in + cast l r (eq_refl l) (eq_sym assoc) (n_wire l). + +Lemma zx_associator_inv_compose : forall {n m o}, + zx_associator ⟷ zx_inv_associator ∝ n_wire (n + m + o). +Proof. + intros. + unfold zx_associator. unfold zx_inv_associator. + rewrite cast_compose_r. + cleanup_zx. simpl_casts. + reflexivity. +Qed. + +Lemma zx_inv_associator_compose : forall {n m o}, + zx_inv_associator ⟷ zx_associator ∝ n_wire (n + (m + o)). +Proof. + intros. + unfold zx_associator. unfold zx_inv_associator. + rewrite cast_compose_l. + cleanup_zx. simpl_casts. + reflexivity. +Qed. + +Lemma zx_associator_cohere : forall {n m o p q r} + (zx0 : ZX n m) (zx1 : ZX o p) (zx2 : ZX q r), + zx_associator ⟷ (zx0 ↕ (zx1 ↕ zx2)) + ∝ (zx0 ↕ zx1 ↕ zx2) ⟷ zx_associator. +Proof. + intros. + unfold zx_associator. + repeat rewrite cast_compose_r. + simpl_casts. cleanup_zx. + rewrite cast_compose_l. + cleanup_zx. simpl_casts. + rewrite stack_assoc. + reflexivity. +Qed. + +Definition zx_left_unitor {n} := + cast (0 + n) n (Nat.add_0_l n) (eq_refl n) (n_wire n). + +Definition zx_inv_left_unitor {n} := + cast n (0 + n) (eq_refl n) (Nat.add_0_l n) (n_wire n). + +Lemma zx_left_inv_compose : forall {n}, + zx_left_unitor ⟷ zx_inv_left_unitor ∝ n_wire (0 + n). +Proof. + intros. + unfold zx_left_unitor. unfold zx_inv_left_unitor. + simpl_casts. cleanup_zx. reflexivity. +Qed. + +Lemma zx_inv_left_compose : forall {n}, + zx_inv_left_unitor ⟷ zx_left_unitor ∝ n_wire n. +Proof. + intros. + unfold zx_left_unitor. unfold zx_inv_left_unitor. + simpl_casts. cleanup_zx. reflexivity. +Qed. + +Lemma zx_left_unitor_cohere : forall {n m} (zx : ZX n m), + zx_left_unitor ⟷ zx ∝ (n_wire 0) ↕ zx ⟷ zx_left_unitor. +Proof. + intros. + unfold zx_left_unitor. + simpl_casts. + rewrite nwire_removal_l. + rewrite stack_empty_l. + rewrite nwire_removal_r. + reflexivity. +Qed. + +Definition zx_right_unitor {n} := + cast (n + 0) n (Nat.add_0_r n) (eq_refl n) (n_wire n). + +Definition zx_inv_right_unitor {n} := + cast n (n + 0) (eq_refl n) (Nat.add_0_r n) (n_wire n). + +Lemma zx_right_inv_compose : forall {n}, + zx_right_unitor ⟷ zx_inv_right_unitor ∝ n_wire (n + 0). +Proof. + intros. + unfold zx_right_unitor. unfold zx_inv_right_unitor. + rewrite cast_compose_l. + cleanup_zx. simpl_casts. reflexivity. +Qed. + +Lemma zx_inv_right_compose : forall {n}, + zx_inv_right_unitor ⟷ zx_right_unitor ∝ n_wire n. +Proof. + intros. + unfold zx_right_unitor. unfold zx_inv_right_unitor. + rewrite cast_compose_r. + cleanup_zx. simpl_casts. reflexivity. +Qed. + +Lemma zx_right_unitor_cohere : forall {n m} (zx : ZX n m), + zx_right_unitor ⟷ zx ∝ zx ↕ (n_wire 0) ⟷ zx_right_unitor. +Proof. + intros. + unfold zx_right_unitor; cleanup_zx. + rewrite <- cast_compose_mid_contract. + cleanup_zx. + rewrite cast_compose_l; simpl_casts. + rewrite nwire_removal_l. + reflexivity. + Unshelve. all: easy. +Qed. + +Lemma zx_triangle_lemma : forall {n m}, + zx_associator ⟷ (n_wire n ↕ zx_left_unitor) ∝ + zx_right_unitor ↕ n_wire m. +Proof. + intros. + unfold zx_associator. + unfold zx_right_unitor. + unfold zx_left_unitor. + simpl_casts. + repeat rewrite n_wire_stack. + cleanup_zx. + simpl_casts. + reflexivity. +Qed. + +Lemma zx_pentagon_lemma : forall {n m o p}, + (zx_associator ↕ n_wire p) ⟷ zx_associator ⟷ (n_wire n ↕ zx_associator) + ∝ (@zx_associator (n + m) o p) ⟷ zx_associator. +Proof. + intros. + unfold zx_associator. + simpl_casts. + repeat rewrite n_wire_stack. + repeat rewrite cast_compose_l. + repeat rewrite cast_compose_r. + cleanup_zx; simpl_casts; reflexivity. +Qed. + +#[export] Instance ZXMonoidalCategory : MonoidalCategory nat := { + tensor := Nat.add; + I := 0; + + tensor_morph _ _ _ _ := Stack; + tensor_morph_compat := stack_compat; + + associator := @zx_associator; + inv_associator := @zx_inv_associator; + associator_inv_compose := @zx_associator_inv_compose; + inv_associator_compose := @zx_inv_associator_compose; + + left_unitor := @zx_left_unitor; + inv_left_unitor := @zx_inv_left_unitor; + left_inv_compose := @zx_left_inv_compose; + inv_left_compose := @zx_inv_left_compose; + + right_unitor := @zx_right_unitor; + inv_right_unitor := @zx_inv_right_unitor; + right_inv_compose := @zx_right_inv_compose; + inv_right_compose := @zx_inv_right_compose; + + bifunctor_id := n_wire_stack; + bifunctor_comp := @stack_compose_distr; + + associator_cohere := @zx_associator_cohere; + left_unitor_cohere := @zx_left_unitor_cohere; + right_unitor_cohere := @zx_right_unitor_cohere; + + triangle := @zx_triangle_lemma; + pentagon := @zx_pentagon_lemma; +}. + +Definition zx_braiding {n m} := + let l := (n + m)%nat in + let r := (m + n)%nat in + cast l r (eq_refl l) (Nat.add_comm m n) (n_top_to_bottom n m). + +Definition zx_inv_braiding {n m} := + let l := (m + n)%nat in + let r := (n + m)%nat in + cast l r (eq_refl l) (Nat.add_comm n m) (n_bottom_to_top n m). + +Definition n_compose_bot n m := n_compose n (bottom_to_top m). +Definition n_compose_top n m := n_compose n (top_to_bottom m). + +Lemma zx_braiding_inv_compose : forall {n m}, + zx_braiding ⟷ zx_inv_braiding ∝ n_wire (n + m). +Proof. + intros. + unfold zx_braiding. unfold zx_inv_braiding. + unfold n_top_to_bottom. + unfold n_bottom_to_top. + rewrite cast_compose_mid. + simpl_casts. + fold (n_compose_bot n (m + n)). + rewrite cast_fn_eq_dim. + rewrite n_compose_top_compose_bottom. + reflexivity. + Unshelve. + all: rewrite (Nat.add_comm n m); easy. +Qed. + +Lemma zx_inv_braiding_compose : forall {n m}, + zx_inv_braiding ⟷ zx_braiding ∝ n_wire (m + n). +Proof. + intros. + unfold zx_braiding. unfold zx_inv_braiding. + unfold n_top_to_bottom. + unfold n_bottom_to_top. + rewrite cast_compose_mid. + simpl_casts. + fold (n_compose_top n (n + m)). + rewrite cast_fn_eq_dim. + rewrite n_compose_bottom_compose_top. + reflexivity. + Unshelve. + all: rewrite (Nat.add_comm n m); easy. +Qed. + +Lemma n_top_to_bottom_split : forall {n m o o'} prf1 prf2 prf3 prf4, + n_top_to_bottom n m ↕ n_wire o + ⟷ cast (n + m + o) o' prf1 prf2 (n_wire m ↕ n_top_to_bottom n o) + ∝ cast (n + m + o) o' prf3 prf4 (n_top_to_bottom n (m + o)). +Proof. + intros. unfold n_top_to_bottom. subst. + apply prop_of_equal_perm. + all: auto with zxperm_db. + cleanup_perm_of_zx; auto with zxperm_db. + rewrite stack_perms_idn_f. + unfold Basics.compose, rotr. + apply functional_extensionality; intros. + bdestruct_all; simpl in *; try lia. + all: solve_simple_mod_eqns. +Admitted. + +Lemma hexagon_lemma_1 : forall {n m o}, + (zx_braiding ↕ n_wire o) ⟷ zx_associator ⟷ (n_wire m ↕ zx_braiding) + ∝ zx_associator ⟷ (@zx_braiding n (m + o)) ⟷ zx_associator. +Proof. + intros. + unfold zx_braiding. unfold zx_associator. + simpl_casts. + rewrite cast_compose_l. simpl_casts. + rewrite compose_assoc. + rewrite cast_compose_l. simpl_casts. + cleanup_zx. simpl_casts. + rewrite cast_compose_l. + simpl_casts. cleanup_zx. + rewrite cast_compose_l. simpl_casts. + rewrite (cast_compose_r _ _ _ (n_wire (m + o + n))). + cleanup_zx. simpl_casts. + rewrite n_top_to_bottom_split. + reflexivity. +Qed. + +Lemma n_bottom_to_top_split : forall {n m o o'} prf1 prf2 prf3 prf4, + n_bottom_to_top m n ↕ n_wire o + ⟷ cast (n + m + o) o' prf1 prf2 (n_wire m ↕ n_bottom_to_top o n) + ∝ cast (n + m + o) o' prf3 prf4 (n_bottom_to_top (m + o) n). +Proof. + intros. unfold n_bottom_to_top. subst. + apply prop_of_equal_perm. + all: auto with zxperm_db. + cleanup_perm_of_zx. + rewrite stack_perms_idn_f. + unfold Basics.compose, rotl. + apply functional_extensionality; intros. + bdestruct_all; simpl in *; try lia. + all: solve_simple_mod_eqns. + auto with zxperm_db. +Qed. + +Lemma hexagon_lemma_2 : forall {n m o}, + (zx_inv_braiding ↕ n_wire o) ⟷ zx_associator ⟷ (n_wire m ↕ zx_inv_braiding) + ∝ zx_associator ⟷ (@zx_inv_braiding (m + o) n) ⟷ zx_associator. +Proof. + intros. + unfold zx_inv_braiding. unfold zx_associator. + simpl_casts. + rewrite cast_compose_l. simpl_casts. + rewrite compose_assoc. + rewrite cast_compose_l. simpl_casts. + cleanup_zx. simpl_casts. + rewrite cast_compose_l. + simpl_casts. cleanup_zx. + rewrite cast_compose_l. simpl_casts. + rewrite (cast_compose_r _ _ _ (n_wire (m + o + n))). + cleanup_zx. simpl_casts. + rewrite n_bottom_to_top_split. + reflexivity. +Qed. + +#[export] Instance ZXBraidedMonoidalCategory : BraidedMonoidalCategory nat := { + braiding := @zx_braiding; + inv_braiding := @zx_inv_braiding; + braiding_inv_compose := @zx_braiding_inv_compose; + inv_braiding_compose := @zx_inv_braiding_compose; + + hexagon_1 := @hexagon_lemma_1; + hexagon_2 := @hexagon_lemma_2; +}. + +Lemma n_top_to_bottom_is_bottom_to_top : forall {n m}, + n_top_to_bottom n m ∝ n_bottom_to_top m n. +Proof. + unfold n_bottom_to_top. + unfold bottom_to_top. + unfold n_top_to_bottom. + induction n. + - intros. + rewrite n_compose_0. + simpl. + rewrite <- n_compose_transpose. + rewrite n_compose_n_top_to_bottom. + rewrite n_wire_transpose. + reflexivity. + - intros. + rewrite n_compose_grow_l. + assert ((S n + m)%nat = (n + S m)%nat) by lia. + assert (top_to_bottom (S n + m) + ∝ cast (S n + m) (S n + m) H H (top_to_bottom (n + S m))) + by (rewrite cast_fn_eq_dim; reflexivity). + rewrite H0. + rewrite cast_n_compose. + rewrite IHn. + rewrite <- cast_n_compose. + rewrite <- H0. + rewrite n_compose_grow_l. + rewrite <- cast_transpose. + rewrite <- H0. + fold (bottom_to_top (S n + m)). + rewrite <- compose_assoc. + rewrite top_to_bottom_to_top. cleanup_zx. + reflexivity. +Qed. + +Lemma braiding_symmetry : forall n m, + @zx_braiding n m ∝ @zx_inv_braiding m n. +Proof. + intros. + unfold zx_braiding. unfold zx_inv_braiding. + apply cast_compat. + rewrite n_top_to_bottom_is_bottom_to_top. + reflexivity. +Qed. + +#[export] Instance ZXSymmetricMonoidalCategory : SymmetricMonoidalCategory nat := { + symmetry := braiding_symmetry; +}. + +Lemma nwire_adjoint : forall n, (n_wire n) †%ZX ∝ n_wire n. +Proof. + intros. + induction n; try easy. + - intros. + unfold ZXCore.adjoint. + simpl. + unfold ZXCore.adjoint in IHn. + rewrite IHn. + reflexivity. +Qed. + +Lemma compose_adjoint : forall {n m o} + (zx0 : ZX n m) (zx1 : ZX m o), + (zx0 ⟷ zx1) †%ZX ∝ zx1 †%ZX ⟷ zx0 †%ZX. +Proof. + intros; easy. +Qed. + +#[export] Instance ZXDaggerCategory : DaggerCategory nat := { + adjoint := @ZXCore.adjoint; + involutive := @Proportional.adjoint_involutive; + preserves_id := nwire_adjoint; + contravariant := @compose_adjoint; +}. + +Lemma zx_dagger_compat : forall {n n' m m'} + (zx0: ZX n m) (zx1 : ZX n' m'), + zx0 †%ZX ↕ zx1 †%ZX ∝ (zx0 ↕ zx1) †%ZX. +Proof. + intros. + unfold ZXCore.adjoint. + simpl. + reflexivity. +Qed. + +Lemma zx_associator_unitary_r : forall {n m o}, + zx_associator ⟷ zx_associator †%ZX ∝ n_wire (n + m + o). +Proof. + intros. + unfold zx_associator. + rewrite cast_adj. + rewrite nwire_adjoint. + rewrite cast_compose_mid. + simpl_casts. + rewrite nwire_removal_r. + reflexivity. + Unshelve. all: lia. +Qed. + +Lemma zx_associator_unitary_l : forall {n m o}, + zx_associator †%ZX ⟷ zx_associator ∝ n_wire (n + (m + o)). +Proof. + intros. + unfold zx_associator. + rewrite cast_adj. + rewrite nwire_adjoint. + rewrite cast_compose_mid. + simpl_casts. + rewrite nwire_removal_r. + reflexivity. + Unshelve. all: lia. +Qed. + +Lemma zx_left_unitor_unitary_r : forall {n}, + zx_left_unitor ⟷ zx_left_unitor †%ZX ∝ n_wire (0 + n). +Proof. + intros. unfold zx_left_unitor. + simpl_casts. cleanup_zx. + rewrite nwire_adjoint. + reflexivity. +Qed. + +Lemma zx_left_unitor_unitary_l : forall {n}, + zx_left_unitor †%ZX ⟷ zx_left_unitor ∝ n_wire n. +Proof. + intros. unfold zx_left_unitor. + simpl_casts. cleanup_zx. + rewrite nwire_adjoint. + reflexivity. +Qed. + +Lemma zx_right_unitor_unitary_r : forall {n}, + zx_right_unitor ⟷ zx_right_unitor †%ZX ∝ n_wire (n + 0). +Proof. + intros. unfold zx_right_unitor. + rewrite cast_compose_mid. simpl_casts. + rewrite nwire_adjoint. + cleanup_zx. + rewrite cast_n_wire. + reflexivity. + Unshelve. all: lia. +Qed. + +Lemma zx_right_unitor_unitary_l : forall {n}, + zx_right_unitor †%ZX ⟷ zx_right_unitor ∝ n_wire n. +Proof. + intros. unfold zx_right_unitor. + rewrite cast_compose_mid. simpl_casts. + rewrite nwire_adjoint. + cleanup_zx. + reflexivity. + Unshelve. all: lia. +Qed. + +Lemma n_yank_l : forall n {prf1 prf2}, + cast n (n + n + n) prf1 prf2 (n_wire n ↕ n_cap n) + ⟷ (n_cup n ↕ n_wire n) ∝ n_wire n. +Proof. + induction n. + - intros. + rewrite n_cap_0_empty. + rewrite n_cup_0_empty. + simpl_casts. + cleanup_zx. simpl. + simpl_casts. cleanup_zx. + easy. + - intros. +Admitted. + +Lemma n_yank_r : forall n {prf1 prf2 prf3 prf4}, + cast n n prf3 prf4 (cast n (n + (n + n)) prf1 prf2 (n_cap n ↕ n_wire n) + ⟷ (n_wire n ↕ n_cup n)) ∝ n_wire n. +Proof. + induction n. + - intros. + rewrite n_cap_0_empty. + rewrite n_cup_0_empty. + simpl_casts. + cleanup_zx. simpl. + simpl_casts. cleanup_zx. + easy. + - intros. +Admitted. + +Lemma zx_triangle_1 : forall n, + zx_inv_right_unitor ⟷ (n_wire n ↕ n_cap n) ⟷ zx_inv_associator + ⟷ (n_cup n ↕ n_wire n) ⟷ zx_left_unitor ∝ n_wire n. +Proof. + intros. + unfold zx_inv_right_unitor. + unfold zx_inv_associator. + unfold zx_left_unitor. + simpl_casts. cleanup_zx. + rewrite cast_compose_l. + simpl_casts. cleanup_zx. + rewrite cast_compose_r. + cleanup_zx. simpl_casts. + rewrite n_yank_l. + reflexivity. +Qed. + +Lemma zx_triangle_2 : forall n, + zx_inv_left_unitor ⟷ (n_cap n ↕ n_wire n) ⟷ zx_associator + ⟷ (n_wire n ↕ n_cup n) ⟷ zx_right_unitor ∝ n_wire n. +Proof. + intros. + unfold zx_inv_left_unitor. + unfold zx_associator. + unfold zx_right_unitor. + simpl_casts. cleanup_zx. + rewrite cast_compose_r. + simpl_casts. cleanup_zx. + rewrite cast_compose_r. + simpl_casts. cleanup_zx. + rewrite n_yank_r. + reflexivity. +Qed. + +#[export] Instance ZXCompactClosedCategory : CompactClosedCategory nat := { + dual n := n; + unit n := n_cap n; + counit n := n_cup n; + triangle_1 := zx_triangle_1; + triangle_2 := zx_triangle_2; +}. + + + +#[export] Instance ZXDaggerMonoidalCategory : DaggerMonoidalCategory nat := { + dagger_compat := @zx_dagger_compat; + + associator_unitary_r := @zx_associator_unitary_r; + associator_unitary_l := @zx_associator_unitary_l; + left_unitor_unitary_r := @zx_left_unitor_unitary_r; + left_unitor_unitary_l := @zx_left_unitor_unitary_l; + right_unitor_unitary_r := @zx_right_unitor_unitary_r; + right_unitor_unitary_l := @zx_right_unitor_unitary_l; +}. + +#[export] Instance ZXDaggerBraidedMonoidalCategory : DaggerBraidedMonoidalCategory nat := {}. + +#[export] Instance ZXDaggerSymmetricMonoidalCategory : DaggerSymmetricMonoidalCategory nat := {}. \ No newline at end of file diff --git a/examples/dune b/examples/dune new file mode 100644 index 0000000..d6c6e29 --- /dev/null +++ b/examples/dune @@ -0,0 +1,3 @@ +(coq.theory + (name Examples) + (theories ViCaR)) \ No newline at end of file