From bf18f8060540d130ab08375dd88c9b33085a8771 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Tue, 16 Apr 2024 15:31:25 -0400
Subject: [PATCH] Initial

---
 .DS_Store                   | Bin 0 -> 6148 bytes
 .github/workflows/build.yml |  78 +++++++
 .gitignore                  |  10 +
 .lake/lakefile.olean        | Bin 0 -> 72872 bytes
 .lake/lakefile.olean.trace  |   4 +
 HepLean.lean                |   0
 lake-manifest.json          |  68 ++++++
 lakefile.lean               |  14 ++
 lean-toolchain              |   1 +
 scripts/lint-style.py       | 454 ++++++++++++++++++++++++++++++++++++
 scripts/lint-style.sh       |  37 +++
 11 files changed, 666 insertions(+)
 create mode 100644 .DS_Store
 create mode 100644 .github/workflows/build.yml
 create mode 100644 .gitignore
 create mode 100644 .lake/lakefile.olean
 create mode 100644 .lake/lakefile.olean.trace
 create mode 100644 HepLean.lean
 create mode 100644 lake-manifest.json
 create mode 100644 lakefile.lean
 create mode 100644 lean-toolchain
 create mode 100644 scripts/lint-style.py
 create mode 100644 scripts/lint-style.sh

diff --git a/.DS_Store b/.DS_Store
new file mode 100644
index 0000000000000000000000000000000000000000..23f45740b758d6d9086545ae868263442b61f3e6
GIT binary patch
literal 6148
zcmeHK%}&BV5S|5;5@NzZ6ONmBB?|b1#!G|v0@mn34N^;_v33b9av&r<>kIiLK94iI
zi&4>&i7{j*nfaFaX**w=T?PO|dmJ<XDgfZ166Q*1z7dL(E=bOL@`yrTV*q3DgXA{y
z)j~Eq{v!kQ?uxJlcMw7fAKsse=y8jXz%7h0IK*(`Pm-Y@DIX&*{xAxYv|fJ|xqM+|
zwdfR`vUBYX)Wl1B={RZkMwj&KOsUA9uY3M^*q?MO>&Gfidtuxk>4GrmW6IS<7zb+7
zR^vEGbggFsPRS{CE7j?=*=p5f<6v)Alheayy(V{e_Ghz_v$45-blSa-9%A)GkB#3W
zevn$$EY9H>7hk%1^hR-{;yaAYtLE8^%m6dM3@jxBcC&NJOW7Sa#SAb5zhQv(2Z>7P
zTFeaUtpkl70T2u5)`DxAC8$PPbS-8EF@hpYDWWMAcEk{-9R1SfxfU~nrW}MFK7_rq
zuoH^VcgO2Xoesh^$d(yk20k-DvmZ)@&i|92=YO5Vh8bW6mXiTd=y;tr_GZu4g)Zr=
um8dtUB$SsKd@sR;K8i7yj^Zk+7W7M6Ai5SagXlrwKLVNtHq5}EGVlhd6H?3o

literal 0
HcmV?d00001

diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
new file mode 100644
index 0000000..dc92017
--- /dev/null
+++ b/.github/workflows/build.yml
@@ -0,0 +1,78 @@
+
+on: 
+  push: 
+
+name: continuous integration
+
+jobs: 
+  doc_lint: 
+    name: doc lint 
+    runs-on: ubuntu-latest
+    steps: 
+
+      - uses: actions/checkout@v4
+
+      - name: Install elan
+        run: |
+          set -o pipefail
+          curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y
+          ~/.elan/bin/lean --version
+          echo "$HOME/.elan/bin" >> $GITHUB_PATH
+
+      - name: check versions
+        run: |
+          lean --version
+          lake --version
+      
+      - name: check ls 
+        run: |
+          ls -a
+      
+      - name: build cache
+        run: |
+          lake build cache
+
+      - name: build HepLean
+        id: build
+        uses: liskin/gh-problem-matcher-wrap@v3
+        with:
+          linters: gcc
+          run: |
+            bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build -KCI | tee stdout.log"
+      
+      - name: lint HepLean
+        if: ${{ always() && steps.build.outcome == 'success' || steps.build.outcome == 'failure' }}
+        id: lint
+        uses: liskin/gh-problem-matcher-wrap@v3
+        with:
+          linters: gcc
+          run: env LEAN_ABORT_ON_PANIC=1 lake exe runLinter HepLean
+
+  style_lint: 
+    name: Lint style
+    runs-on: ubuntu-latest
+    steps:
+      - name: cleanup
+        run: |
+          find . -name . -o -prune -exec rm -rf -- {} +
+
+      - uses: actions/checkout@v4
+
+      # Run the case checker action
+      - name: Check Case Sensitivity
+        uses: credfeto/action-case-checker@v1.3.0
+
+      - name: Look for ignored files
+        uses: credfeto/action-no-ignored-files@v1.1.0
+
+      - name: install Python
+        if: ${{ 'ubuntu-latest' == 'ubuntu-latest' }}
+        uses: actions/setup-python@v5
+        with:
+          python-version: 3.8
+
+      - name: lint
+        run: |
+          chmod u+x scripts/lint-style.sh
+          ./scripts/lint-style.sh
+
diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..485c481
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1,10 @@
+/build
+/lake-packages/*
+.lake/packages/aesop/
+.lake/packages/Cli/
+.lake/packages/importGraph/
+.lake/packages/mathlib/
+.lake/packages/proofwidgets/
+.lake/packages/Qq/
+.lake/packages/std/
+.lake/build
\ No newline at end of file
diff --git a/.lake/lakefile.olean b/.lake/lakefile.olean
new file mode 100644
index 0000000000000000000000000000000000000000..c39b45f73287d9c2846e2224b679e79058697134
GIT binary patch
literal 72872
zcmbq+30zgx7w!cwdYy4fw6v?1Q4V1_U|C*s!Xd>R!l48a1!cG~6qXgKDUDKT(quP>
zBF)0gr2Y-4Wt0u1Rx~M<DVi3QDOTD$>+J8l?7IQ=y?6ZmT%5hu`qr?Av-dv3O-oLQ
zOAYEfD?TA|R==5j;%D}XjO*RISN|FDas6h^?9;1XWJG+wUh(~B^ooz~6X&pwn;tyf
z*x|^&;AWdjNsz;FGDQBc4pOH&b&N<&%EX@zw<9>nlC=*HaPnt0*;Mjf$M#YfW+5e_
zTuG__&xAiZZf*i)b$lOi(uTg?D0%bp*F;9}OKQhI9t;rDT*y^u^5REB$dS5mKHVD^
zKR0f+-xn#?{Rt0Jd3$#I@JmA)KK`rl1+S6(VI8EzogSZ@mXR=XdLPBM{};R%;ADet
zUU2N0^A^AOq6nPPzxa$y%e^Z!INQGh;FN%t-##|w&l!y>iDy-{eUQ>m`qwK00v6Hz
z3kz29{&k|q{yT@adrPE*ABA$-^S$->saDMojT653&wP?L5QcR`C3r_$E!F;8&ucF5
zLOVaQ>Vt$qw}^n?&`(k`uYGMK^`GDs0;d!-tND=kLR;7ST_l9>sHftg-|h>$Pl^~g
zyO;3K<hM6HEp66xTg=9x9S`uHyXwA2X5YH)58}{YQq%8#B8WrxI~RDl*Yqi$zV(mU
zA|m`E!|zUAu6gs*(5oL3zW7Z$q^7<8B8Wrq*#4@3+kE6B7i`!xaDa#iKinCZrysA}
z^7sp<o82dTvB!2qO1u8{q_t2zzC_?UH^1`tL(Yva(O$k`Z|$zjuJ|{6`6k+9Jfv(_
z(^Y>^6(hpdp~qJS+~-G*I{$^|U$BR>bIF$usN;o)sJyJqnto_`*|;11_E64t^}?9H
z;<93I`$_m>kN%RfKcvKECMGA%5HZ_tOV&Q}fp=rV7lre0Ui6|AiXX)&=eW_qy{FU3
z(H(k_UvBu3IC1C2+p-T0C!g(>aeV*k1&6owI`}U6?)riCUT}9+&@(CSf61pl<9u=3
zfB*e?a$XDa*{)d6E5aHd7+Dbf3Hdn&{+th&wOHAt@*VOSAMw|Hvi89H*L>Yf_>xDq
zH_{sI?n;qVhu-eWVYgAx_>r^PKQ=}rgdf@<Fy5UPj9$O4;>(G`7kk7fW&2}0j}$>1
zdOL{*?tM>%AO59X$Z-)7evV=9!4(PdT{oULlzirw{qp1gTJ8H_{?3cZFE;ca3OY98
zWafuolF$5?V*Fd&?X8$^qNlVY-{A_3ckJi)g}t$1rN8~qKHJxh5kc{-y4>HI`W{2S
z`H#;ueIwCZMn3D0?W_I^*Sca)UNn~c97F%J3mrY~Uoyk)mwJ8ix>JAP<q?zD^z~7{
z*wjC<I=1V_=N}aQxzv|7EZOxze;o}~UJ@pM_2`hJGw0J@1j^YSy}Mq%E9UgCA>=dP
z<hN|K<7nI4_q9D&e|n1`4!!;4!S1_#n?Ig@PsJh;5q`1Z&#UK^eAIK`Ylnp|@v~o$
zvfZ-1_R<D6J>QN-D*pd||E*itqwTJty$F;uzV!M_KK(H%qbd1pFKq9B<O~Q7b=`K1
ze6OLuY0QoBd&a&yk9_8j{qy(x3VV5u&cBKLLPP)9ny_y!E$MHMtGfRj=a+{a@}>2!
z|D))iOMB3U3p>B`C$zE3$Ap(U-qh=kdydc_56YR3HgP+GzxuC<%|EC7YZF1;{~X$z
z|L}>}lIU34D>UtWzT(N<Z~U}G_~&F#Yhb#)O5nDB=EYY_`(|#SJ$IA9@nPbif`kF%
z-abG+>zn=M;d!~4*U#N^iu_nZ|HMxl%Ac9|*M9PuU+RC-cgda6{p-I;zR%FF8nWp~
z%+JpI$frL2f58)*7~FD>omGji+|ZwL=fp=_wtH=bsn2{L+`BoXV0LRa`R=BH@wea6
z`=g*M5+{+*_}M-VHrsSfdUo#-<j0!&lQK_V(eSmm$>(^({(Z@*e*O18ck*%aeTM!w
zUv3YLEBnd5{z-g{pZ)c%gFpT;=XdAT)Gs&mI~43q^*%JQ#`sMC-@1SKcaDDB-lx91
zSz!DfCYSuyV*JQy<THNyKfn94-%Q;3p5OmiL;t4OP0yt4o%aFt=|AVW886QK``7I=
zz98Rc=&$^7_?U|ISKm!O^T+=F&W~GuFJBs;D}1Xz9JeoI*59O6SPv!Qdg#V{HxaZ9
zGz#;?B2X9SS)dNgA3UJ3pgz!I&<I?geW2x_Zd|uwL4Ba*pwSrDnO`r?%R!?t4(5TD
zf>wgYqCb~{de9G;uN<C(I?zr$pgEw$pbpf72Q&w?7_=Oe^@;q~xqmP{ZN?mtkwe<C
zRaf?r6RO%<?`t=#FYCDW5-GI!&H|KE?#U^Ye<}^(*K@F5$uEJt$XI1{`r%)EDm#8Z
zTrHFz!?upU>(JoRwP(W_6PJ=8GIB^f5zvnY{b%ocK`j#37YSedu_rjz-=y_~VI3Kn
z>FN*bf5FLyem>~C1HZYa&Aqo}ijd&&dQR$}kEY$4ke;42)9)1Uih)xOT6O8s2V>(W
zb3Wk=ZK>k6u<fJqw4c`C&okPKOHE6imy(v1L1ByP{zn7%snzwCHD5i!zTS)f^&w9h
zg7fJ~Dc)rKEjT&Q_ksS{a{8KwTn}-aca|7_A1rwN1*nT3AratLfIfEdqxUjKi|^z-
zie=6<WxwhAu2w29;h>ov$86x9QkdnR+5SW~!m8a0w8JRq5kC><v>`Oq5fqf8l}o$k
zI7L0PT{i##Df2i!Gd(GFwqi>Ds9z5J`U@gmmnJUmCK49!B=t#&6X*3Nq|U6yakWMs
zKs%hC7Sj0oZ|(V&<S`oMwD)5Ak_VNx-5#7=?~woTz5CW{{17kn^FZsboiLrUf*+3Y
zm}OIbE3>a<f?@GP3ZYjDx}nXcD7~J{e2SjbQ!(;V2|eP6wo&nl91p3daIM^ut+O3Z
z9G`SM`=DMAiO^5^y8Xh69iROr*b-kJ%4t7w;DJN5EA4^TEAk7^(T}uQW8&;VL)i(U
zol5AJ_WgbQ>Tg?c9qbG{FK`^V;Mq~TtNjRedT^bhA9>~T4r=_6Na)9aUZ1q=Q_4zz
zG2;+jsfSYdlWo|~$2n~Xm3k=D$}Rkp97jo6_d{=~*3|2v68cLoPN-^l{M~&bW$h>X
z`^#%BUYQ~tgyoTKRbJj{{@C*lfJ;2lC})f!FZCIQ@<h=8j%U7PgIWJscIpxD`F7EV
zS#Ift<UrmBI_}||FNkf?I@fjAr_IbtP8brG8AmkRk09=kmjUnY4R`<h@7CM7u5!A<
z0_(eZ_@t#o5PKXKNI5<zdrDIBN;^@&Tah^G+KiYBSBb=#aMFgw#V4SF3XT{0d7$47
zf9kbwx<%U8e93E(;qUZWi+Q<lNdCgXF9ZFf*>@)_`}QIHBIKb8{3|;b?_*mLKY1M`
z<v!hYSxLz=N2bjH6!H9VN48UWoO7zhUAae}v3Jp>eb6?kC`ufOkk18u_|$NWwr9@Q
z_<0$b2`S183&)RN44h*PrfplZ@dbOeccyrTB_$_BTYHWQsT!{WIIi|8o|El|&u$-E
z&u*jQcO=Rg&!baLoF<0k*9ZL=$bGi+$a2aGKMeeA@E>?^doT7``?`mDICb(NCpIJ=
z&UZ*zPs8F;l9K0*&Ei-m@{%96%QE0}J%4=nQSCZ6C0;A}!#YS?s#C`-8*lpDgn82w
zZke7r&&$Ew;tQ_pe3hSY&~Lrp-!}60`X@zQuXon3lv{evSjgvquAlw$^TLxu_?-6z
zsUk<q;zir=r|?7ap;rX@*X^E-lofs%%GnQI`=wt9+qdwmz-RyX`PolWtMhNw&jl(j
z*3X@*ckFP&0n5%wdjV>lliG>2&XZCzGR-=$?D_K_1Kd;hjN1SD+WhVUY4M%8C}%!8
zBu!#f*zp#C&v;kQXgElZw*-8~`{bI`r}TI$z-PScpO|&G9<QrIV7#pk#T4oB+BZTh
zUrFr+c0jyC60A#XN<#GjeEnQ&5;lnQVh$YaaMSxr==P!KCklQn8+^gB{#CoL7Xisn
z0m>Qks-+QLrET*=!oe>AjmaC-igRg8KO_?ISAZYVV#8A$!=;^a{Y!jhx1OU2{l(Q0
z?HpA2*7Y~oqn%5?<@%X8=6sbtkut~AvvD)c!j*hbKM(i~@BKPxZpA0|cxu_T{#75=
zb+lm_<i^}SU=cZX+_=71fPc@^YcHm*MeCfm4N6asvll6bKkf@v9>(?D8q~AfT>m<T
z`>UiJmr~-q*H28%h?`}M8&SYX1l_!4LU5Dk#@-;li(kwODch=r$M77Ir+nxafnGJ_
zkG!IXcfE2poaz4ApvreS^c`*$-{beM+7Z-fU9{kcop6-%{(Il3{Fi_Ds<4oDI1Z3<
zJdpME=%g8g(^6+8%@$$n5WFbhC4vrKvZ;614?i9ue2JfJla%dcc5>Q`3=y&pJAUXF
zfv&slzn5;j_R>p)FF3p|kn%b{eP+U}xU6LTGGXJD1IN)x<>A})*It`FC(FN1qCP3-
zL(?<73Gv$f;0WkPgB~e$v^jrBG4Fdgvr%sOXdf$^-up2A6hE8}<NEj7;Xd|UO=K*7
zNIvw7K=Z~e^RJWSc?jbEz57^etE1Y7=#@df3Up%7_kRUf^PRES$D#g*<DUIiX)C*-
zomE~UK-Z;h`k)^4BOOjx5&D^bU4nKM4f!cME?&nrO<Wm&%yC0_vL5gP&kKF}Re*D1
z2$l6fu~shQ5%=+^XO2g_MvzjjhXyRT?k*~BDVFgj3g?fe4Wp`ky*KTNyu{&vd<-b<
zcr{#+l|$_1YUL6K_aUiwu5qL(NI!0chAVM|UW9g@mvkjXr9Mo1!jm{kpznqr{fWdm
zF@#DS(OS7BTj#tXT0Le{W1Qf;Ee|-&uIMz!`S1^43%>M|V#ALcx9z-5cydVIxNl28
z%ME`xu8^{ATGu0gJ}f)_>yi6nm9M9V&h9no<xA}Av&2PxQsT@>OG;JV*!~7Z;(D40
zoVm+4J+%4Nadr=qc=AwAf15Ww(SiD6r#VhYIo@J8lgFlpBw-6t{AT`2f!m?$(bwjO
zggquOV$ac4#Y2044iDG&YeEX4=Z4(SW4=7fia)L34=Lx(@CVhJ;r9u4{eHy)*X>&Q
z^sW~17t^nN!>=1=ALiv){0{MeUj({%{NKab5ydao11amns#kkWL_Ziy6>v86yfLo8
z^XId|7aR<296}w;`;BSob2F@G!xFR>tLNKuiOTEP?|073de8X;<MN`Mc0c@i9%@V3
z<8_{tF{R8E1a*iV;uHdJ^*=-2eBSZPI+2iiEi>$7?dUiM>cS7H0-x7`W2=Ae7=&OY
zZsv_t%b$PZDt<7I$Z!?!kauo))%jDOE%bx)9Ik(Uh<IrY{SZ5xFOhQIB=d%`-pr&l
zfA3NKhwa%1d!0ILJs36l?isXKigNn((I=b!q&<l{2mDIV74HuHn6lyzuj{0|zNgF`
zn&Qn=O;F-yToIS5xc~V2_QeIaKViFX@trX!XWTJUZ(XJPkqtimI6Sk&fBhCe^TFr5
z^%Cc?fc**93#nE=k(wQU{geT(SI4^?lN!!!&3th`mpLdMxN@7O@6VU}G8N~fLv0_S
ztoX?|$lrbN&JT2cEc6)1H&Z4>vQ10A=|8C!M}N%^e;hvGrQS5{#H|Zj?iCrqVLg#@
z-l(@BsW<vo0i5ZFH@;Qx$Ep7cj?`OdHx(!AZN;m5KNFrDXY%*Dv^0JH$!{kbcz<`_
zQC775gI5Jd>|~>y{<H`?#HKI&kO=VeLHEDADT1;Vtut@dax+0}$RY7Eo-*JpPw%{c
z)b^zd!FM{k2gbW)@5ak)Wu+hD2A_T`I`6_)bw8MAQr4ra=OO?keo!YCc<*OE_(bFr
z3;p9P`#&j@A>)8H#M+30$8n$lc>jCx+q55+Z{H{a7T;Nha@t)n@#y7nNBBYHbNt+Q
z;@<Mv7pCr}epnBc7wUiUaeN&0t+G1zpX_D+gn(@#+aCRm0q)uhyPv3VFR(A)g2(ZO
zl<hb@Avqx~LshBxoeTW}(Cbc@K9u`V(0uw`YWV%{-Z1-FI`Bgx!LI~u_UDtUEc^B$
z>ju_e`X7(1uqJ%=Vc87{?Wyt+0s8!~mRZ5ziyp66vj+6K#|qf57X|r5(810B&9A57
z<{13Hdv|`?squXVzri)XHVD!9#o*Jg$4)grQeWej8~StJdT4F~jqkWz#YO+V%KmeS
zOXIr@{$20v|F0qVXR5dBtobZ&oJqa0{$qjX9G7_hGvm73={^&VzD%|2ANmEL52svt
z-hgXg`BD;Y@tvh8w=nHv;_A7H_*3{H9`Gwc*X%qztC1FOXoSiK=LJu^e`G~tEnfC>
zQnnZA?|hU@{G|P8;N8&o;s1R7-nc`25kGk!nsVXSE?B1d>E!)h@|~Ts?0aO;56K5^
z5$N=+=RzrK(K^@ti3#56R*%wV6>6PQ1suVbby0XPm4|1_g6+8l?Uq3<68yAV&L6K|
z&zKidJwI0nh;``s@dD@VR_PBPK7AXXd-0F|F<37=I^^?_j8E#3<1+bIJhrzd`4T_v
zlj?qO0<8N{1wTGax^cq`I|n=kKmFH#?z=8|^PUN`BYyDuPyX#MT+m79$6lfG$m{=!
z@ymVZnlJn2zL75<@D8<{5FPW>uF1?N*Hs+P|C;I9c&t}xA^6S;=+U=<@4Z$mJUJv^
z^of*mJ(Y<4zpQ7&uT=3!fwYrooEQCk@8=Yiytq&v3%c!-9xI6{_E;~Zdi`*Mt=CUJ
zaN2x2`<>g9-oICDi5<=pIR7eG_KtsjCVaLN@}pYC|8S0eTv1zlb@x{BH+ik`@&?Cu
z+U-Q*;r<#auVa~M`jZGMLlPJ7ZzKXQ?Si-V7bj2bh`5~jD5tNUC*F@y+IHR@v~yvn
zt;-$Je%z2E=#_yk$Qax<2z>FA`6gxFXT>GsDy#Y@=VzgPRJ>U$o_i<l=v&{=zetqR
zzb*Gw-Aex?@0GA01G!1#*YycL2S2QF^olD1BzYo!K5$;2eCVC0KaIDi$r2Cwr1U|j
z(r(M4FXhs1U42ztpE!^HO<D2V+gg=}f&W|F@czUWegw*SeR#Zg&uQF06n~gkQs!6U
zs%_ly0?++U$4d|FJN2pfqWeKRF-v`0xjq$s5%jp9_VYK#hMub*wT&xPz+3&~$|=|P
zteP!;NIYz3q-@vG$#I#p($Z5zj)&z}PzCO5ditq6<{Y`F!LfQ7_MBSqIIkmRo-*Uo
zX9wK>hJGICqJf>pl(!l9yV$bqIEzqjVcN$Hzn${$6Y2RWgWO#Ybzga|`KfLE35!(m
z+&1mNWx=!Vju)d65A#9FxO!Rv^_+dX?VGf}Sm;ZEw7*=OH*K@2#1^vt)BVl|KhF71
z8~QEz<$fQ>`A@H$7CdLgqfvq(c`1b+^K$%-3loTM*>x~Uzm{|w?x<88v0Dkf(EcjU
z2~RFO76iWNwE;-nll%HR3aj<PAs+?0>c}5kgEc+wiyf)IWthWPtrrXV9MJo2_@QAv
zO|J#)MZ7e(jU%sGFCX$nppDCa+vwEvxIdMXaz$H5PPJYs<SRk{8nOL<A<&cfU012N
zIbL1!-X+88Yq;&;&+@k?e&{Hz#tnyF6zIw=cN}e?;l>*LLw$zqcWJo1Pjq5eN^6I=
z8aD@eKG0EXn%~$EdeZJf;SVX}#(ddchH=wT+70L5Wx#7RHGjdajc2tK7-=`It5y7L
zHxWZSv#AI_qzHQ9kc(<`Uo-VKrRoPZkcCCc`s2Q=x(!B;l=He@iNKxs<=Bz)9gC~z
zm(TEP<gPaM92)$PDDaCxE84bwxUrTed!xq^CS`ksU)DomNw+3gH|TWFbiW(}R9^N!
z-v5>hM*jUC{fb06^A-92llHZnewD+Y7|0##_Uv~}G{5YHuO&>%cEI{eO0D)t_a`5C
z(-$v$aR1>BN9j+A;m_S8>va*H98!PT;8%cNnvmYRspb#ulQvPR4)`-7z1khY^S7t)
zYgB$Ji>EFNp7pAYXz`sfC}(~)ukUvlkhVWA@UuZDEdFg&Gx#Ip4fjF%KU3Dv5vw#M
zj(o@$ffg@m7||Sh!Y?)W`yct$6{_(o4SvMv&w91c_@URTczE5-`un1$Ej4}w_#7wR
z{;<imR^ZG1KM%%H&NmBj9!<TG84X&OGZTu6o*UOG>Q&*~3%$=DetKe?(wchtoIhYc
zuMFn}(7WlU@UruYYw8taK16%b&?|@D)%oFj+ZNW;i^9B)dfC7U8>sTOwc8sPhxuyi
z6=VKh4(b3-H1r<*xN<_fyqbC?ShsMUmks?~=rz9n=iv4^HTB%k^MK}n7DF%pua{4s
z@2#nqk9A-XXc=e~^!CnN{M7}qHTAN&9zS2@AsTuS9(6t~cgwO4(KYpQu}@b88UdU{
z=*2uV;HQqBntCOu?;`ALdZ6!vUhz%me|TX;O+5$nJfJyjH_+?#Q(S+yyQW?&?iYk&
zAH4`PbdZYgg+;5TcM7ek=f-`OJkT)UL_x1v)rsYuYtf6seK*#78SYQzKrd*@p7;C%
z9L&mnTl0RWu<ZNKz$>CYbSiO<Q=7<q&2^oMOA6#ZYIcY^=Xj>ye-^tYU-ZOo6maN2
z^%FIGk(ER2=4j<&*HOQ2yB1cR^XVI|8<WPDA7s4d`xxcGUwrr0&*Cm$f34UR9IjJH
zc^|^sE1D%TatMxVu<|Dybll5(*Az|)=lf*NXp}R~vE8%$>sGPDbp$Er&C^p8vNF@-
z{Pz%Ok2rb2UB5GW)6*}kw~H-*oW+K{BOe_Om`{7bF9&^g%%cAhQ?3_|Au1m7FRypd
zt?hx-d4Fz5g1i@ykQ%RUiTU%xd6oybRq5S6o1GGVHRJK3ob&hC!5^&oeB-U%z<1_>
zPajwO`u_Jexb>gJ8__VZJ>)dLbE?J<DTID0XgBYS9mEoSU(-PSW0(H=r><WKz0jdb
zE-Sm+z08N?D+1-bJ|4UNgFot_|LV`buz$FL7Y)7ZyZ+mbZHsoL|CsGuc+!80(O$jK
zXDkIcCx%ezKgC+P^dHX|`j5!-I~$@e>oWH+6?bl{+crv>9O9peBjxtE0{I9~`WJ<B
zk>eruVzqMdFSdSQeK2pLBlQ)7ahACI1{QNEBK(kI;IaLtebOU}vcfM1pZkxqzP`6T
z>(i2}v){{p1^u>g{QEHO;qZ6fv#+|k+_Q*&I*j{G%kqXU)AU0Up+`T%UM!fZ`^oz&
zybrPS_U|qZb}IylqX7EkcMku2YCVl#V(`;aLV}$dzrx@@9{TIP5RLDOQgIP~{1+YH
zsIT$E4gR`IXTR7$<3}0%6;l#>x-@>G!GC8%Ur$4gp9?<kOU#@TpVCO<7l6-x_w~pD
z%NlEZzMsW*n9=NoiRW0)+zyiV<gaJf2$heGTk0?DFtx*Ohjm!(SFT9@L;6cJ<XS#{
zh)X`f@wdBJ@CV=5yYyWA@n&Tt(t!BG=M3_J6ZJ$@r%!K<>LfB2-&u_EASf;Se$;cC
zen>g^{&u(EvUeyeemX{~IGNWwcV$Lv`z;}E@YyadIN1CywmS>wO#P>y=7&G8vB29i
zsO-0{QA@uTnKR*JRKGsu(DP9MobGEbF8urMZ9fZ+<f9bj7N&iiirE@4UQ~k5e5}pe
zcZ#x-kI+$p`EX7zU8d)Q?=>-BpAU?32Vwjd{rpaW{pg>H&&LG0l`q2g8u)+2eP6_W
zF6%!3{@K`*eH@-@y*%g@f_lG*7*$W>bKjf$B|VqUnHS`()~|pb*KJoFnL9fed@KGs
z=OuElY*2b;hC)*R%QzlBTE!_P(hp*A?n=uJcz%riG7<bXUpKm3?+4ufB<1`|?k8Re
zqgLMh?Z*e4pz}U{@U2Z#Vnsyq%682Ct#1~LT@;)nT*a?|9_#I3qhlY|%dy$EKK<l#
zjfeO7o}`~TKKJV$xOB&V!M<w!sOtmU&5vc%a_Uv{{rd%c-g(EmDW1!|e)ymuNPM}_
z=e($IWJS|`oe$W11{U900KQdM_VH%@u)Fc6?SBdQ+=uJ)!R2#<N|l7PtF{pSZ2Hb!
zj$(BpaaBOiHAeY=x@Gd3VCV_ojdI?{Y8$jQyPn4PfX}>?&g|6FsqtgM=YGYq9?iWW
z8b1eo-mlrw`?KHcYkVL0+?O5lM%ynNR95?63_ja+SkOy7xxXm>mxIse1F}C})sFj!
z!gq`fthevu{`rObdNQBm`kV8TMC8j2y&hwpKHRum`NRM1{S2(PsTU4C5A@b{8P%f+
z;?(s@&`zo6f?hWCwk^E*;-<yaP*m)3-A=t6;1ohH^~nwS%?fMkaotWm7xXHi7xisb
zbaP)#J+9lSSAy}y9j)?Ny6*I}(7c*@T(_IghsQwgo0AdGw8*Kc$8|gPqG2x&dN*wE
z`*KTfO}$)<_w+LYdL_^+JbLJvR<SkpxZbCp2RM##D!v})_eg9VT~jXt*IVjk<2(|2
zx3wMJzKy4*9`^~TSAqGC7kVomUN+*qh?;ubC!k&l^a`MN?3b=zv~|~_hxs7&a&cY`
zy-Cxn{tFAOsmJI0spo)R*bOQ#?!q5;_%FCnm-T}=&li@gAAFdfM?;_ETQ1IZ59GSz
z)5>N2;5)<mLF}4*+ARkT?=#V^W4wyPv>T?Ci{0Wg*cCtdy*9y->ti<b2QH6EBesk`
zyzb<JzjE>iSMj=I`Bdlr#`v_X^!NmYWa0R)FU7zK+0}5>;Eg3+L_%=5<|O4jc6Rk=
zJRO2l0e#m5m52V%Y}onA|L(Ex^ILpp1j?DOq`Mx?XFOtulW9`k^G(dm^k!Uj`Q?_q
z#H<-T<I_?um#KyI8Aa<m6+Nuelq~CuqVq1t_wRc5)Etw1dSO>=Nj^((UNSAI6YWbr
zqfuT4x^~M@AAJ>mCCWJua8~Req|fg{C#tx~pSQbLL$2>dpZg1(hn<`-s(+A2d0^Xz
zKIh9(?v?Su8sBT+KlJaRBlW<yuN#*r`|MxbKgfgL18=X{%;)2jRfj|L%yA$B@`a!~
zXXpLF^<IEp9pgX+^o~y3I;8$Ni~~Nj8}}sT|G4#iTW~H*d(t1xej_{?2V$Tf1AW$6
z9?pp&RN6y<RxbUK-`Sxa^C$9Fy*Tro$}jS7p1Jon;mINO#(wC!QOUi0(RKc3g2ZnV
zU-ZQ93iuHYJ>o~<T;zC&-?3V`J$^L^^vm?y*DR2~sHz8V4cUJ4d5vP=wr+gWzw|-k
zcDMrdzuva%G5RBMm(!mZCD(NNwwE~m*yE?+pXl1-HuT)kqfHOaX+x;Q9ix>?-24s_
z_4K&KuE`f1v6~MZt|zEpq~VLK9AdXrD;K+NBOkh5$yY&8V7~V5NekG=;W{f~vXU$O
zYWMT>LGl@ma?VEwc=|c@e46&fPl+oOdR|as=HXoAc-ZY<E0?%p&m5P3UCa0Ord(b0
zp6-{aFShLV4LhzWfq4nXIeii;etEQVyM3R*FS~sie8CaBIl$p{k@@gx_#!KZ*e%k^
z?e=Bhn)O_4wCf)K{9)fq7Cfm(jt5~=RouOfZ`q~itK7gBJ@LB=endi#e#hWk<amhR
zUaegG=6AoSXZoFE*j;{C8{Vo8@VgYaUB=x0kM6gLFTRN1g^;fVrTx%pDt`JbRQwLt
z%BA1rVx2<0hQY@+QAgt9cg)C7)by>glYDN1l$&YR_pq|!Ge=lo6&O<Eg<Z?8e_x;g
zc&CE$ibvgiUVr7M<tUx7sMX#a<+OWKbzIU8LvgOlTlkH_QO@V(*G=2-5oM&E@OgR<
z<o-;1)89@cF79WLa{e_sDI=4v>2c%$=dZVZ_+f3xKZ`_0aCo1Hl-JhGwCXq21*ZV|
zC7?g_ecN-g*ACm3#dlVsobR`Ebk6jzDkPrJn^j);Uecb)hi+oL;s^aF<vcPqsruHH
z?ngB6raZp*mPfj7_($RqKeACyKjJUA=O*FFA%5f=ejIJt@ecYS{0Q)ih*OllmhIf)
z`|GU?`~#mZZ$e*1KNfkY0>9(NuWw^a!e<`bm#KWTSr`1ZZlC^<|I(4-yLEo#bfp&q
z`tcW+^sUXmZ14~NddIE0e_<%k2MrE=aW&hJ_*Z1`Z=QOf9rw_LUuN*P<^DF7ZASQ2
z;4}XCM&0jX+Y)|Qtn#1sTivnlUf#15ex$)4{K$p_ja2p7^%rCCHyv{|=fuU*_ty{i
z`-gXXWVfEbZ0duyE&BUE4s^Oc@B44~_ru$@{Du@kuMG5!o%MI{*&gw~1mjf|`0Kv!
zFoVw`S$@>H?n;r5dh}9(S~&jam?Ps<zDE8r;<0B+|F-X0T6||L${Aa^>#lA{lbxp=
z@Oj_jqV)Qulodb2!1safxu?-%eAdn4`}0`+T*!;p>Uk)JUODK@mw%hZ>Ac{xo%8wq
z{jb&QPWu+EbNq@=OZD#wTR8r4$1_9aVaB?v_l;fjfIY{y_|8O>v%lwl@=U<>HWz&Q
zad_#6{`Wb=&jRq7ht|(s)l83*{gL|Lm!4|DI7Gh$`W2uFcl_Yf`<ol(u6X5t|MB1K
z)5ZgTp2NYvIQ@?w_5SF9eiZm$jaom9*D%Qs@8j@09jWWuz4v;z(PN}7NPcpm$M4@H
zev~>~Zzl!dGro`R2y4ao&Qwpst?y-MIR1Tt3gGQsp11Jg_wFd5AE7f<{KVdVO*ak;
z;%7(+^dca)_Ns(CSr6g|b4JP>Yp*2=P7v*QfwSYnVFOP-eBH<NBj50&pjp4Kv^YYd
z!7l=x@bmsnv?YF)p*$S^{`B{YcWCwHug@yT^&9^1DSiA*gkD&J%17~6|K85IiQsb`
z!1h>w>I?qoCWIdYJ+1>5Tz=7onty)#*^qnT^A`EcndnENJRfwyH7`Eg3JDNC+bi31
zmT%P^tOtwl$1j8awtgqy*X)NBp}Y$8?Vs-mYF&-**Qfu3;v0R(HX-)IW~sbHf{r`b
zBC`$jr5&)*kn-9yT0IDBOIkSo_LvQv2}d{mxqtYH2Sh+{I3|;F4Cj3*?Xz)qyYd02
z81z8r#y!^0nHMj3mOW=B$}MdBh!{Nf75piD|2PvmTg5jiJ9V&@*N_O5Gw+|3NAJ+{
z%6f^0+{Z<|Gqrm4=hX}TEa%%(w00R11OM{C&zpNg@AKfG<?~5i14(&JRiB;Gvth^U
z&u=O4s+!zTu`_B*kw8j59EpMb{n$OrFV*wm20yz!>U-Xx&3Zm~{qR8UWp`n)o{wCN
zi{!`Nd;esOZ~ZWk!sUIh*q{%4t_$}6K84d~_%|kQE#0&0tJv`G{(3hq)BP(4pWpqO
zdZPQQntiAF-K$O8?)-}eq&+y2lz(o}3BP7urPXIh4)8tTR}{W+kzSv?E_om~dr9{b
zn*ESi=;eS$yxh7>ABSS0=L0_>czqK4lI5SjJr#rhd;Lxx_Brvt5cOUT{=Qk?eb5#G
z%DTr~mkCSOgSlKM%~A3Dea5-f7X62;2P07~g|gn`_o^vptYiJ_>&RXTfBi){2laa6
z_{x3QpMyvK9)yXD#8m`)9G@PF2->Xg<MMqD-j{s;=)fO?e9C3fuYx}Bm;bhYYujLr
zA2wI{#ru{kt}M8!p2m*^pZA-$E?(Nksqtf|-(TUZ9`NoPAsRm$eEL7?q2c-UHGaOK
z|6IGC8yjf+B7<M=!bw-TG=3TQyl;C~vq29u)c954^L>UN#x#1fk;V^8R(|ung1<V<
zo!?mFM}p7i`+Mx}-lvJij{%?0+kbrR?%<{xKO6k)Ym}Y8R)w`_rt$N^XMP*sH2yc<
zhqUY8;QzI%A~96cFEjX!Z(11NLgQC~&-OLr)zXeFHGWu%@{9Fzd`jM3t-zQ4cJuxx
zpL36dp0iuG*IVZ~0uIsR{ZIA>KIa|-y+ccye%2-@K+WFY=lxIW@j3TA=rzpx;r{cy
zHTBH<pM1`}1bQz#HGXQ_*qVCg{m(M??^KnSrr(cS6&77n&%FPc54}j}6~4S?NIOqW
zJ@fu2?_+wQH{!=b@3xPqsb}8z;C;*j=oK9pIPQFREqcRM9Ly*0W0pg2R(a@K7lhW-
zGw*-$x#qAmg*Rc$!paVTYO?PXWR8a-BI9f}@)Hexj+ePO*P&#b^=akyK4(K^mwNtq
zEJd-)-wPn0cFTdo@z>AyDm>F}m{xA@Q#PvGuGK%Cu}uT{5g)9)ikQ-W`MgdxaKHLz
zv;X-x(Jyud>TgQ_=XzZ~A9_WgefMR3#cPzr&EH4x$7Lx?zGEO?21<Sv&S^ua<U911
z>U>Dt{JjP0>G`(fZW8GCdojuS^UMBqgBQ5p^xhh<uat*!jyoN%{Qgf~7bPy!zW6C|
zMMJL;l>U|CT;zC2Toqcm#8rBh`Ybo<Gx@sV8;B?M$@@@I=_>xWb`8+KSK!R4ADEZ!
zhwq=K>nB1l7qmg}(x3IXP5(q!;tq#=0Vv}x!8vURmAK2ba*4arh}+zk=3I=Fb35z#
zv@1CrS@HY#nLQaQ&JnG5w}@<g_kUv7^65<PMPG^SB!`ZZ3!EGN3%_E}(aH8Z+GoSz
z1Is#2DR3Scl5ywp;3lc(;?I>LWF0zASf+}rMe2dsIcsiB6#m)#=`BLmq2t5?=asoD
z7QWJR`XcZ{_+1U|gEd$_<OJ*gY<BwCRs!vmz|Nkhmlj1OzHToY&xTXmd(WX+D(>G>
zJN%S8H|7WW8+(N+=kvXdZrB%muKxC`#ouh$`Q^qG_j89sa$(2+d@uLSF1+u~!%&yJ
zh7?1O`$F?x+4H0or+o;&9DL4mqEZ$&*5}ENTU8u<J}z-UVNN|X?6c)7vf55{`v+c^
z&^{M__|B4HA|g1<4Jmz$1BMX2o#X=NM0EVTk)3uX3tw<J#*-3nx<@3`AvlH5F9p4#
z`Ks$4zWcP@ABA6qa(>S?__=F;oxT22duvtfaE(RE{;z+FN^rt%Q~8So4e?IizyIw|
z28k!ak3~86+vXR(IW*+k3cnqWC!}0kPEVXS8{ybEIl%FOMmhUmK5OW@$*>b#f^xf|
zTZL<0pE3H$`}-vbKf+P3K?V41C)~dqx8cWZE8c*^@;ik4YHT-0mp!v62=gHeufB;F
znXU3LDyY*b)(Jr^{4<V!_RTs=Sn@?*a)I||gRn<df8X;Z!4e$ihm`H0`qwQ2aY}*n
z)c5-muWI`7O2M)0IIB=jd%Z8|&`x-A2%pc9v)`rUj<`l~ZGK4PJQXkVxv5jX@x+q+
z#emP}fEr!7_P$`ZLa^k{l#kxEU03pfcWH8)y-&4Xe7_)_4X3v2N;z;^o(!$r_juGT
z=Ymt)btU|E75@*e?mso&c4V30NZkCsBHP!3+wX79yvY28e{-K3dQN_SIuE#qn_YEO
zcyb7C0m_+g_rBL}A(rq<z^C0CANk{PwnIy<&T(VJOl1Rh{QkM_Q1ShF=*iPd9`_}I
z?~Fh>+r^>x7Jfhk@uLEML_;q5kMok*M#T^A+mUkrPQIIeeOhYVOwAz+FNpT?fVVQG
z<&<ZC>tXMOTYP7+;m?-kTRAM-dGmr_4*Ko0d-eUu5XXEKC!c3)I@SArh(|>v@wmZf
zJ8p7({NDN+-vd6!iB87{yx2hF$AZu2yZc3d_P#4x;Y&U^u99*bwB}d6YnzAofEV1d
zW%<*OCEP4X;wSfu_+5;LUv2tRP@b|Q{0iuCUOlDH&d$N$pUscj<}u-Ss=W1o<%8E+
z-go;?V(Dx+wart!z*)7X*&~nt5cjL#h`*c<@j0i@zx-;a-kzB+Qax|A&11@7XZE-U
zCUyGx8aM55e!zXQFH4_!E7&Jo<%jz&6({TWvC9T7s^_!WXN|YEc}^_w{)l?DYpa{*
z4Wu2$%l9w3UU|g7&wRGLvcX$<^Y`Bp*lD`xwTjPQ-fZvbN?y4i%y@1)R^E}%cZwbE
zosu?Cp*oV|qvaRB?K9m@#N8@C6Z;Lkaq*-JZ2^n#j6u1DX&>RSO*8SQUBB7j=eJk-
zFCE)akJmKuGn9PL%>G?ghlDDGv*n|<>uDKqp2!&0)i?0xNrEJHI9_vq`t9^*Q#f7;
zpWk;QztZ>al{(*(qx|PQ*wroSBgSzSKl?-=A(kC~z2yM!yO{?b_~iTP%%^{zOFss8
zssFm}M+x*;uebNScBvEjk~k{B=Qy^c|DMPYw{k$<kLdzmZVIXR#o@L*w+_+ca{}S_
zs5o=4>e3(xe9`L!y=F&NHFw~Swdi>u9}7D2w$Z(UHN6X=*T~VLg*|e>UN+?OL9cyk
z)aiPf-uckGZgBB!j&gM(_6i|i3R+O<ebWg&JARaNd^~U8qMacc-?c!+$Nkoqp8EHb
z`WinReD0TbezDIN4K#if_#9vRo;q>TrSTKN=XGHIef@_w)cCpJv;KPR+rPLG__A+W
zfckTTx)>+)-bhIKw6Xt*0hJfga~OKDI4^<Tq9d2BZsJh&jnvxvt(6!**xriJe;f-{
zo)#WYeURUe(e-kn$9YNt&Lg3>YHQZIX64jS)b^A1u&(sr+zY+c^*-L$ytJlXKE`$0
zE5dmJ^bWkTG&Hohrd~AU%<qGgL+|SEJ)>I`*3>J(b(GINxquV4Naf|aiT}oMAD!9~
zUo_@LUeFxiL_@FT>6XJ=<xxXX(Q`qb@BKI~L_dVy`&Yejf9sr@dc~OMQjhNo6+_Q)
ztY>Z;Z%w^ItP8@RpAA|Cy&e4)jXy88rd}e}lP>7TfJWS_{Qb81qyMyxuBqq4`keLP
z22LXMK04yq7v`y{7is9l;M@njpTZAxX%|sbuM+zr{H_R}8!Cg|OShCQZ11kAmkT|%
zvjUulE>`jFsqAvc`JpxSJdiWL?-B*QJC@yk;(}WItiryP`F)oh=;h7rv$jJmeilN{
zbD8oh2eb%!tqQ&y(6JUj6QO5*-=z|IdzWv1k7G8Yl=Y0ce<(cJmvjR!e2MadBTOvL
zi6K<>C9}11*_Y(+_fpT?XXfu>lYgUUpuMLccrxDedje&^ebIaR80U||uR=Nbjd~4O
zrC(3Oa+TlYPkim03|`koKhoeIpL%2#=b*xmG5Gg9a=f&@IA<Ng&o=li9iMFETub=*
z2LJlaBlmJnCj26Uf4WiC(uNA&#xDb(&lg_Qa?s938ovsBUT@lkPwU<o?Lx*K^F9yn
zD}~*s@^Z`jZLi`Q4zTw97PH=jC+(pK`HqA>>&=UEVhEM?kgJv3`}2(h+mYEGJO<yL
z8?>94k}u9<DuA21x~d0#5Weevh400EfhL|g4Yl^-<nO3c=kceH&(ZP2p&tdhA?oQh
zdV5MlIp04BjvjY|)}EY2^#bEtanaJdbo^ZC7l3~H%9oq8_U8093e<0OV!<!EehKs{
zK!<in%GKMW>j9<D_Wu0RY47XpF&uo(Z)T)+U!k=}XM|yY@9ekk(d|b;KM{0f`#%3_
z?bYcv?i)SU{S9kgs1B*0T<8^mUOgvr4coJfL;Rg@){kgPyDLF`mq3sF3Y^1)O{Cp9
z9#nad0%><1!!NVlg*FJxd+1Z$HW5?&&c}VVSm3VseoiRch4^jai>~<XfqV`q{r2IU
zHiU}bMOwLK*XbP+=$EhI`75X+aq)N1iCYz@ACeQN^!fhD$tRBm?5p!Vz{rP`-12*u
z_tN@{|2;!~=k1f=2?5XLW<!tPSKE-aemL_Yd5Zx*AGFD|zdEzOSU%VJ{Y(2-N(QGT
zCnv=Fe>}y)^RKVUfOq8cp`Y*RF#bKs$(isH<X2B>!E-&V;tmI`*C#h*>i(xc6FkX(
z49dArcGKV;gM=rC*kj)zWnZ&@LNU&3%ZcCoZdX3=CWg-6xBTZQd)rLx6r<e2w2$Ep
z;_W?6IkEU5<=}I^T6AmA)sz)}Hu#REDxO9&(<iYW#ZRucNZTtj_U~L8xz=5`rNn>w
z=K=omJEGn9>{E|&ivKw%r%z4qjQI#AZ2x`W)BnF;ylg0C#eX;W#h`cYO<SzDqaxII
zIryVLz2s$%o7Uwn*gt8oj7onr`-S)-{V@zUjy#noH)sSXeG+-;k5MR>bLnq6O_Uzx
z%yGnBKagLVUu^IBEB)&Cu?m3u`=J4YSWn`&i7$HMcP`{h3_mM0|3p>}d;EJu`61`_
zIB^EQ?R*)0(X+=d;tUUrE0*OVh(qjVYvp3s(KJv`&zIOW`2r<&i-5!DzL@Va4PUog
zsg;Xe&l&7WdyNSR^lQzD;FH9Y_Q>b%q90XqtGjLs*r)fRob!;WzQf_HN72s%KVq`d
z|6u<G)AjaT2tMa+V>%wn()W2v!RK{6>B)EMao^1L4}4z7-}vt2V7}ih{LsggUFuJH
zx#g|~m=_8^!r&*InlRd>@uR_y!aO5%%%t#!8s7^(pS%05{@33$()fAc^SQh8=PwNA
zyj1KLg3ssfx|AIFxrwG<3O=8^`}^J%)0%4hO7QvIU6+@B9n?(Yhb~j`Grv=ADtf)S
z#*Z-gv!8i9DOBS}8~oIE*{&AVd}pCCPkL}mb8g>S{mpug1p0ZP{R;1!-m+Rhq!8t-
zze|=SzuF4?GtJveq4)le+dpm11`8_v$!zz+lKvEd_EHIb_NVaWDo;9;^ka`!ZjXCs
z=uh^zW$<Y?2RQtG2<`ebeA*VfMOwK%ZW*}x_+jPQ>29X{C+>#BcMd0>)C0ex5car|
zb3QlmFUkr(66I_s^PZn@hyGkajKPmuH=qai+0Rr@+0ZN9TD*nx9r|UDw?<sdR~6#V
zhdzBR#W^vAO1>(za(lcr@?qvHDmXA-L!Vjo0Ws}%+gkCXRw$bNTKA3gLHLO%=lA$K
zw%z^<$31&IH|z_xw7+oZ<$@Bk0O#~UsKiyQmD}UFfvd-5w|j#xIAYh4uj1f$G-%h2
za*^X9b|bZNyWJbOx?RZ!*9BZ}ez^UUV;tx0eqrc~E%7TGcJe{#SCM94_p4MZxBG>G
ztNUfQFN06Jp--rMg!NUFb|X+un?fZYQChj!EjMt@^#<>MalP^C{lE8S`>^um<ab$U
z_toX60-h`6cTISIW6{xuj|IDxSCa1v_{08sa@w+%^{V+!e%F@w<=0MM{*=;I^XTv=
zRovYFJO5<$ZoB1EozM4V6U3sHAO3YnBJlo9*!*UC`ogzGO!#>y=W{!Y-y3&pMajT8
z@(aOtwNU;neeH&m(^voXjqt?}&TUCKh75_zv@wWN3Y<#N-h=*{_DbU$y~N?(04ecq
zxbAwaPL#i4PbohlLFaziX7p|K2iUiIC7xK6^SPb%9Y5_jz*S|#S^VG}@TYbb%MM3_
zcMpxI7`1Yo{4LMf_`ql0xellt@#Vc%ya9)W7ZQbdilKLKL6rYKs>SzzpP2Rh>eLqL
z1QGqvrvvLbX5qoVX-D`G;1fUb<icrer;>lJ=SaD(8=o~JlfQ~*;rQEu7kC|$>y3J2
z*6a!5i}3SN&i8`uid_E5_JrMbbCP}<*;e^U-=OC#f?gTu70V;H>+w~hyb}3&K7H;~
zjyvK%V<9EJ|K=_HV|m0g%8xttcguM6uBmpt3l5*_Amv`ojS0!g!>r$pNtj8mRJ`ne
z*}%K{*Gc>P_Q+VqxC&6tdh1ybno9(!mlE*VPI}LIF5r4y0Y2+3bNk3KT8wpm|M8Zr
zr1-gmQ|x}B+4H~m9KKS;KXiVxOP_cpWe@$0K{@mEe!o1skAolL0zVt{`M36c$$F4@
z@=?z5YWwV6(VXW?zlcFRtj8kAUwz=%eD+n%-;hwqmqBj$f)R=A+hWi4tcrv7J{_?j
zOrQ7DpJ=q7@;y)X;@Bekyq_NhobOg&9<U!Cj`Bp%@TFJx(bo;!PvZMV?>>0)r=VCB
zf#4TFkI!kYFYNJNu*NR|pZ+h%E_t^e_%h$(dms+%1LQ)!0(5H6n86LBl|BA1dVCLr
zd1m}BpUT(O->;n9$U_Z9MbG~}2d+CVj7uKqZBFPivT;OBJ-*LT)Jx%We=Hk%e|NsN
zZ4-AbdRS+hzpqdTy^*CaE#Nwc+WI_{{iXo^RzPp>f=R9T?kV+T{4uZR!jt()F7(~c
zDgW92V{lFkp)ybKYUMIdhzSbRJJ;VUj~bG6E3vKi;vZj2fj@HJn3(^L<gF1I8K2lk
zNZFPX4V)_Ihpke6wcqkq<<qyW<2dc~pq$U`waoq0z7~reX}7W9^M2z$4|M;5IT3!2
z!C%?)-vu0(gzq!>cW)SVDaQ$kgL~+tyza>Jbb3zUk3TQv!0kNjmL1RRUTDACZP{~%
zu2yk!-*U-syDLOj4)G@fe8%(Rgd+jJA04Vht-4hQ_t(T9E49Otk`toiG81j4h3Ef0
zcrS4KRCVw6=C`MOA|U?wP|lq7c_)iok+wh4;1`3wnfB!oJ%7cBvmE?h6T{zQT}wQU
zH7Z{IzWW`EmxQoQ2;U8UQCB4w+P-kNHg5XgKlMQFMB1tCyylBOe`h=v{O2#es0-^z
z_}nkb0Y5UKpbP6#_&${LI~|Vc13R-n3ZMJ*e2-~B?EbOLmGFz9Uk<u<-cymR6N~Tn
zpX1Dr5AQ!;&!1y0@&g)tbmn5#t>Al5&iClAdEkPdc;iO+vEcJP`OhEU<+dA}s^5?t
z@cEsU$?coJ-%2XqIz-=R@bB?<$!o3HHoqAB@;K#Zn`SM(Yg5hl$H)DqM%%V!==mv!
zzT<hN?`YjO;k;V(xgWLs&h8KD`fliXK<~SzYeCyu^toR(?&;h1>H4wI%K^Rj_`VTg
zwdiv{%lnCEyRPqpUNLC+Lw85<L2kW%x!?74vtN^R{c`9zUQqGxS>7v;d;GdS@8fLV
zofq(axf^;O(6N<S3)w;K`ZxHAp<8ENP#s@Lj=?{F@okGcfN%L(=X~1wPG)@K^j@~4
zWyk-!c*VfG_rb0cBi9#95dn+utUx*E#m|rXfZfy~cG#y#`5wWHtfb_bgVN&@t)B_A
zAJ$ZO{&6(CK;`YzC;z$UuY<c%U@s^J<y^;oHsM&$nO*Psko;`$`ToUYdpbwlHvUc9
zyu_0aKHsbGO&!<$ip-7nJ>fIuCEEJk<+#}iVn*T)DgsU!=%#-*%>JhLq$kODyr}%=
z`Yhvv*IOp7dgp)O2fM*vE(O-nIyj|d|9$;;$=@;$^?=WL2iIqRxz={!I3lugSpI~#
z;72U<#@>B!Ij?8J&qF!e+vWG&P{r|D;^x>)N?vMQiV9lU@z+l&@FpBTyddtAyc@(1
z@w*D;^q2F-4ZD^+V%Z5e#IHighpkijYP0&gAo?JA=DM8qc_4X7`y->@u<ykQKM{JY
z&v~Ck9r@qg_434!@N>auJ$<?Q&taYJKm7*z1>m!u*3FK2Z%o%P`w<LFKez<^7vcHC
zm7e(-eZM>=r;;~bb4c0vqXv29hiq&u@q@9u)~h)0>vG8VUfJLFqd#ZDNi=XGpdSso
zIqu5BE(=2ri6P65GaKccH{IoY&u&xThvb9L`uS_nHxJV{OFyK@;J?~)Yc|`P@XHK-
zuie)iWIK~M`0NTP*QxfrNs9&k`12C>lFCc3M`nc`YPHS{zB3BtoHu=!v*5V!<Pd)n
z!Dl@G4SqkC@rXaXW|Hz6EB+{VYX2Q!7xrBXfPYWl!}p$!Sz(7Gc`ipeZG8~txK??k
z{K^I2u|dTZ`S<qE^gLEEkKkucTCs?IPW<Lvg_P}ULR#(q(vMi+b^Pe%ouO|&TYx+T
z<)NIvi~Q-XOXd$PzIZP9&O-2+=NnH&Zqef@1)q6NO#8sUPbB_wZb8bqh~$|*o1R;F
z^w)pr%PLPV%*;5i(}r<&|B^gMp`7vEG%hy4uS&)Rxg{s>4AS$Qi*oL-cIrE3BipOA
z9}n~kAh$d`<P~lF@xTAUd0xU@&#%<+E1<{wMopKl9k1ilzUvhg-;bNdxLMC)zXbZ>
z;GevuVWu_@_WKtF{*veKOyw9O`o!n&6(4wNdcgOX5}}t1TGF@o+iXh#@q^#B>33t;
z=5&1CU%38>&H>L~l|Zio^p>ChH<^1<I=-t=#eeXZeXnv%(DC`b^f{fcS)k`H9C}fp
zdpeKY$FW7OHx(G4d7VszT*}4oj^<oLZ^u!P&xKq<;p>|?H?jQj&ufdokMA0$&+9{c
zobP~N|Kp4Q>j(o9PZi2JFMqip|93v$DeHT49WJV}zAxl@c%#Y_a}bGhwttbA^?fwT
z<=o;O?;(F!2Wep|g%i_8(em>YjqRvtWoJc;x+t1+k)n~;DOw0xIaHnJ4O6uA21TRB
zD_S-Q{2LX`jZxGw8GKOh6m?z!>YJ+0W2PyZI7iXaG)1Glih6EQG%Q`w&<sTjmMB_u
zpP~^DDp~=Worm&A6fFRC<G!mG_w_13!*GAA5;T$bcd+l04eCQZ<rw+zqSEhw-^1fl
zb{(MZrs|yE2QCj$=jBa6!4G$;b3XSMi*h~>$M5v=c?sV4E^Msy_`G98Lv>yZ8rw{r
z`{)P!;&-X}9dkGQ@qzOGB%h<<{at={!3SJEC+euD?06d~n$tkhSl~&T<a)tAN6Nk`
z^UVxzTzo>t(Ckd))aqCM=e0bqDZKY@j-7u+WtBa*k@nvevZU;1%oF3GpUey6XFV|<
z`px=a9?FqF#?SnhBR+pUqkdUmtPkdo^}u$(?`1L1%vUVz#WK%qSI9H#oB3w@Du!GH
z>VfskcI1Y?Y&ViVYkYEek>5N}DVO@<m`=)TL|j((4GHnpbtUq8eN}E&^_6t=`R|v_
z>BajP{yCh;^AP*)*Oj~nRCr>adn=@DH>qjz=6qI0Qd+9t3EjRIIF~uM{@#A6Z@1uy
z9bX-G*bYf~t(ln+pL|1H>g)u+mB2X5fLA}`yF-_zX4}&rvBNzJD+d1|<y?z%oEK)e
zbsY%bqT;8#2j{w+=yNZE^DWWW%P*D!9D<tz9Lne8T$dC57?c-+3WSuieU=&JoLAFd
z%F~X$P}BTy6$QrU#<?yh_J~VLT%PlqD&-PiEO5xr#<?yhxREH&10^n>Pb@OZ+0M=Q
z*go`n5kD%R@0Wi=#jDGSAH=1<^n>Mky$G%cIFygUxh^NTVJP>45|`s)zE*Dec$|Kb
zR-%4O5l5jWFZeF-OSEze=Opt%%6?=05KE@@$Z*2UI{HoMn<_u8daml!Z0Pb&=&uLm
z=Q<9=B`3wnB_knKh5|te?4Q}d`)^G4?XCY!{a5%BPeC1a*nUa5o{7uMOi!ATl_}$Z
zZp*Y+4%~0s{ryO3(Yhqs3;Umn*NltxPRcp@;ItI4wYQ%x`aJaUEgE=3wnsHi$z5vS
ztC9L({z*CKPD)KqN=+DKMUg=`hv4M^#|QfM1>^Fc-2LGdA|!cY|F^LHhm^Bj>E+hn
z$GJu#tpu*?Efv3jh<+)`-CDV&U*~uqpB$HQrh1MAPJYF~4Htd6)!qjZJ9#KK^UiuD
zW&cV~n3)xyG$Se5`thK^Yz4Nf65u}Y%_UhwI;w6U_8f1kIL)|-Ps;s>)U*t5LVS|d
zjBmGV$Dd^D550aOfg5&J#oR5=E~;Q2y(l;1<Moo1*Uj3j>2?Z$H^lj}>z$8WqiLtC
z4m-pp<v1XA%&wx_34KT9X<pAQ=@IcG5@@Hkb&uZOVxdR*+MX8|d5-IOhP)f=4ZYop
zJllD(CNJ%o<0EM{_ywS4n!Mn6a9*jEOS|Sh7E+Ec);Kvwy;?CWbwui{G;O%F>!0r{
zM82!?75dWLOCFdraX91mqTH;1_Ipy!-x93hD?L?OwjiiO>V<X+fHx(-{n*>yDmx$&
z5?5IrcG!PN*}jufyvYeE38~f<;5xe_!IqGKc2KP1`Xpy_@|GjF{vdp@7lm>&F5;8=
z`%!}RyI)rF(&OSY1EUM<w>iM=vZ&{xxeFTD^HQ-_REIs*J1NJt5jTjZ>d^C737j9k
z%Xqx<fi!y<milKskg`5xerY`crdPY2pRlbeFOi^yM;`Cd;nDeX#G>VIegC>3aK2n)
z{H5RgU193;dqh6qOS!eb;0TdFa9HP!%Qb$u_1!1pkye85-_WykW!^#@jz1;D*{0$W
z6Cy_(%H={XT$78i&^%bzusu*d8gf>S{fFd->pRK|Q{pM>SZ&|ZsgW<{Nsn9b@_Q@2
zQq3>P7x(0dAG*C7U*aR5{#HTXZOAcS%ttZgA`Ch5iB|x*7)?&{#dR&?r+g0N^nBU!
z-Id=guZv2Y(qGDeLwuCi=epZ0=la_$_pi^jb}aeky4sX?U9J2y%YAi}M-Hf6zNC)w
zm}_d6=XzhaD|su849r^>NrZJUf2>z2llH=S9?v-*@SOF;bB=R7=XHbUyf@Ett~+_o
z^&-!CFImnlACD8Cl<l7F*z>-MkNqN==LU_%xfe7CG!N7VS_taL8xe?K48Hg$?JN}M
zrCPb<k?UxYlYX7ML*dAIq@#Wa`K%B28_rL7o_`iS)}yIcpy^3Jr#;r67yR-7xq9_k
z-)t9QAE5ovkmbMNv7U%m^`4URKwjb$Io2=b$|09%$gy2et^{&<h8)`y<q9EJWXQ1{
zQZ65I<%S&F73Fdu=PIeLFNuSE(nQEb7;<JkaGZ=W<d|pTMFTI#kYj(O9LLiFL(Uw>
zBY{_H$gy6D=Z0LBA;<PdITz&IA6Dl@#ux4@a@?VO6y&sKWA_98Zo0G&=@;y0Y%iu=
zA8-l{yWCGS?H1Q!SNx0~jCL%Btb=};RCv;_!#+ZLHpYGKm(nie>vP{!FBiLcLjvux
zo@%pemDQNfo8z6HFYz-Eeinm@Kay9EHXcd)HQP}o<Xt<f>r>?DAL}t2a$$y?*^Xi%
z=P~5W`iz2Hq9!MK;(jypNBen@W4;()^p$~rn|3OoXSN&jx=lM(wb+sCJone>7wfyI
zU+wK9y0t3T=V3B0WxnVq=U3*u)Xaa*#|keWRP0MV5s&^Sf?sUN(H`ZZ!LQKd?EGUt
zpK($?^b=*@%zsoDRZf3QJBiRU^UwPhrk(6s>`4B3pMmnsKkp;x<+b%6`o(_3{^Z9Q
zfjB-5jK{2p2=G~NjN7b-3d9j*;L#7}wG?t*O-|~8_eB^N<?|t@*MsCI=2GRikLwr9
zvD(^4CG@!-qW`8}tS{GR)%g&=%zB_-5s=gU68VyrN}uI*QPhJY7dVU?<@I@g$Se;9
zeqcYVIet|D_iXi6%6Lnw<CZ*{`6+^2xF#p@^8OY5WPYL{$M_{K8K3$4=yG10odW2w
zK15FJ<hYc7rk$c%>`41?bPbdj94XJQqdf0oC4aWOdOlZjXUl6i<YGX@er@rFf}f+w
zNxbHIjd?AAoSs*StGsFL@$$YX^F}|+{u{PS>7Q*JbwDlxRPe-Ka~(#1V<2bx8{4FI
ze|i5@_gCWcHmY6T95=)tk$2aEFMbwWuW;xO=gT~2yB8d*y*fCrm2*qxIOh|j=J;A;
zeTMl+%x+~j7UwyjT!#t1<+mdoa*3c)F8#&_c{!JL6xR)=|D4w|j&co0+8^~;KPBK-
z8gk}(BNY7bJt_|IL-1&ycvYzHXhY8Qi|d1ILykD4Tp#!hIo1p1%3-&}kTcgCC6KE$
z<XE4?<9=7z7lHAb*GI00JcgXvzY1YD(U4<3(Jt37d77NvzZxq)*e@tw1Ua@}sTXPg
zeC~ttQZDV6_DDG|U^`~}B~ErHWjFlGz&x1wiUI#@^J?bRYv3_otgle;^9?!rO*yus
zVogr+WsW1vR|VwEeDS#pJzuqr*PgFb9?a_#?^95p_F^D!+B2_bl5ercJW#(7`VQ^7
zTbp0JK9^A5!jn9h>o($6*5a3pGvU1g>zVncUQ}7_@$>ne8u3G3kH6M9(Lc_0{#XcH
z$(zJ!?z_|9vRdrh*N0{*4*E-+hzY8kakIbEe^QaR{yuAeV!sl38Q-J6R`}VVQZD(R
z9r|4W{@Lak5s)i3@aRABxQ|hx$w}VK^*iN5zfpeb@k-vz{RjGQw%bJLpKH6#p}Yks
zewphW`c+VeU*<ZRewlf2e5>Lz`!DZHvOUmV802f@p`pT|Jnflz@IwDw^N>q<<iWgO
zLca=Y@k{z|=tase`eVlL`mXl)&GiQDghAen-<<c;UXA#nf3E#H7xIE9?ZBMJ(XYZ<
z{HkqS<n_T^*ZGY3A#q*btNfVp<}|2T-_jq<b$wlV$Oi7&=GU>1%L8Q|%>5YpTU3j`
z(hl6i&fE?{_txGH_`D<AHSM?|ujfVVlwiDM+-7^ruFH-w{?blv9d>df&m2#A9d^w1
z5A9UeVaL_?%yy#o)t)zB9r46KUeBAf>#!aQhvl3{^PK%i@@kdUSa)!q_Ww%F>rx^7
zEC&_4Qoqs0x`XpB`pf#}e30ic<<)tV^@^!y#!0<IO;7qW^;mBn@O=St_3E3~&oc1M
zeMZwy|Gv-<)&ACYJ?1(j+>m2E(SKgAqYXLo83(V&*_xcR3-f*~<$aK2-lTr)c}y+q
z{@TXDD(IWnJw7jH_V>^q1KTI<d5nD+DVO$1zetVtRX^-Jg_i?d(Gx$JKi0F4eB3{$
zoSDBw$Q4oE5|sRz>mK5kLyrE{h0ArCdEegLe_*{t{#1LO%<(|%NqsqL$)BDF;uZk+
zY}boC%7Ka<$%A>lB5p+;{+i>y;MC@qXFvMMIj%=yC=b8PeINRj13A5ZtiNl#N05zn
zQLtV4;l+Kg3eY0l&v0X(Kk^eL=L0RqesB!-GqVv#IcO>O<FFnn$ND-H>!lpfFsv(b
zxDLU*Iui5KQcw@(X=R`u%v;JpBXIpL2aV!&3^WYmaSmt+`f()MvkUbZ3mS?%7HE05
z+MOeDtI9)}R&M3D&gY*Jvb|~P#uHom^Hh-s6kbxouU~b!?&%rQUTixk=XfIJVu#PY
zlCob;Or4Qty|IvymCUzG91gL==d66d%l=|``)hX{%_1J3(<0@#o+Wt3gJyzP3Y<#N
z)3b*>GXKZoX9Z9Eb{|ynn11uQKvG`!CZ?t*#KkAZ%}7qTE<G+aJ~1IfpzK5UKL)tz
zFBScA=`}xf5&_8v_t!{?KPxNM{-E>ttdx|v^d$YY8#^y~z$*lOJon=1b3>l8-*uHZ
zI6iZ{6nj$6amOeRuI+gt%fA})4eI^B(#Q&xU-%Qu`9`!>E_o|%q2zom75#F{(Srjb
z#!eDF8P`f6Pd|A5uza=;?la1X#KGqRNvTIFa#ntVD}WnzsM=4_Cmt#F3L)=-JmVw(
z|CbWaq{OA)d=4i@^V@FEm={zT<y^n(I1(q%O={YwUG8Ie4p-+(@>tvR1GV8ZZ(iu<
z8aTYa?+YyV-!CsU%dwuL|M1hn`yysJ*KKAw?<bh$yboxW``5uno^xC(FQz>2>zL(*
zjcUqE-Z-w2n(dA_|F@L&$omatzXa5ygZrV8M*_>auS$E&GxtADdH?>Skst0CnmF9Y
zGt0S8#r8tG#mF<;lfOJf`E9ln|9*<$5BEPzyWD>;%ejAGmUEqMmUDhpqa5o-vz+Tz
zvz+rvvz+S&wh!ik^Luj~;5^yH;XKzY=X}yE_s{3Fd`i3Jd!M8(jF)cEQ1st$&<gfv
zw8Jpa2+%0dSkP?HJkSErV$f)`+eFYD(0tHB&=Syc&??Z-qpJOcgL*(?K)s;3pgzzd
z&{EI}P{*$dFAOvSGzv5pG#ixlSApw%o>p$<x6a>%NKcrZl^mBoA~mUc@+Q|+zDH2`
zoAP78<oCagKQjCU+HqH^a&!K}=lDrEUzhI%WhPm#M$};^26!d0PquAXf7m6olUs+K
z`XXQ*q`a;V9&f#|pjZxxgYQKZ183-?9o9Bo@<C@2k-YF*4y0_a*83GeQS-|R=(~Pb
zaW{8t{&VV>?FU6juAdPoH}k=H04ej5nwA=Gy&9I4DKo-=w+56w=06d*&koN&J@$($
zJJFu64tvZ4DdW06A@Do5#4iKRwkzhWymY|qF9l!n!f$Pn@;>nF<g^)a$s??<f>@JS
z<0U%Dx8o0$A2(?83FE5%eWZc?eJ06M49d+s@%}6+=lvO(=~?laS?PL?^!Awtyn1bR
zw7B!Z>wac_itDh$_Cm@$T`%9w5@qYq<ER48z{PLgaZTm)QNow}a2-L)>#bFl=4*vE
zp8HSq7toXsrmVTnyY<qu;aTmlRy;3o@<2xpAH5}K&%gfnB8zG7b!C@!*bYhA9_{aj
zSzjQm`BqV2d#nQP^K&QdUH13L2*I`6|1rd8*yH;|q_ivFm8sc+1T8TCiNGCo>VK0D
zud1+@Q)16ohdn+=P0IE=GhtSowPvin;VQEM^<D=2U6I+oS3g~Nhlq&Xu)k`LlkJF<
z{ciN&F~b0F<8wTU2F}l;|LPy&>Ru!=(ysX4C@J?TXT)XryMVOMZ0P5MKC*A^T@5yF
z=_)wlXK@{V5|@<tDQT(xch+?LD&Rafe0%FYqh{ORKNEcS@!IpieoM-Adwg2L5bG7G
zfR(o1&tia=+Bzd6=hpU5Fpk_h?9gvg_UF+_)~jmiq8-?7i-A)T_SLE_Q|j552+23E
zPo#YRab|)yJt02MdhM;+W%0KHIIa^a{)xxiE`9d?r&ftQ$x9^4&vks8nHH};tE626
z#16-2FYvxA{MWm0*h5Qb$M=6}CnarWR&v6SH2qT#x}7rM<sW-#@qfQg`;K;8RkhbM
z^G?eAN5`dS)Run_aAxP;`TPqrhNlU><e%dYDeJ*&;{=YT;%_2wazS7IWB6Y~7HzQc
zB>zQq_{(}F<#i@HJs~r5UUa(FZ0vr@{8s`m`-QA!3qQKd?$+WruZN`PNkG<N`E9){
zY3=S<?*XSv)3IMRS3L3GeG>Tu?K3I3(}>=UXNiRPpH2SjN>0kf9>0S?%5N4)6P=xw
zKF`YgIoT}){^YF}4ZUDjC%gK@Ze<;IyNCnUL26H&tn-w))|>4!l2YR`)6&mmTXglf
z!~a%s4ZHla5$QK}A1ZvY??t)UZ@7O(%InB1>s#se)yl}RX|DjdpSB-x(}<Tx?4`Z(
zI_xpOq|CD(uY9MyHrslfVgIN&KRh^pi{r~bD`+<c<z}3`Zjkc&F*G@DhUm&6_-vPX
z!0COW>ceSm-+ET~(oWcaNZH;~;^NcOj9dv`5pc>tznWh!ZQF#`?-e|$7uUaNuSR>M
zpQQA6LPC0q=*pqvdw}!r4<}BhFI-~Fh`+2)QqB*oK|DobH(d7PCIT-Pbl;JCe|_ll
zH|<ST@w>PVzj<9E<@ISuf@Lf%U7E9PgZ{I>RsnD9T_@)MenI17!aq~KX9}L-yyPSN
zl*(rm=od-OD}%4zc~tPk?`)Kt?StbCDaV^QuXkdqwfP>GI<waChV}}9d-cX)o4d9e
zeT4QZ>afRgos{FdbshI#sU#l%eE+nH>xZ!`J3RY?*MI$pLb(|a+YKq(kG6cX+YjeC
zIlwvEe(ki<19R>9f#jd#I4SGZ`l^sjFf)gxCC`*t<q&@hfKvjxv7NVN<+{7=W+!-@
z&y#XqKg+_gUrbj}e!ME+g#D-DKlaDE@Y%1O|Aq)ieMX^Nk6-*?T>O55^Umu&TQ_d`
zCDhBQMNj-=dnKix<NaTsuwAqN)9n-iZ{p<7em>>cw?_odlt20I!(i)%MRjef{8a$Q
z<+%C5)0Pw64juUI$^V|2Ab1jQB+BcGm-jbzELbx1sb;YYMNj<nLXY<;c71)a#rFI?
zlZl&G3$FOjagLPZo!9!z$n|ll)+c}EYXX9z>@e>oz`M2Q*XJiMTlJ{$#s8{0>@d%y
zY!~CQ(lX=xzo;oF$_~e;h#-}xW_ONwDgM$s5`-^)bG#$vxF@sD#Dw^{#?T>ZcAjE^
zmjn9#)Ne|fZTR_G;fw!8DA)5Z_Sla}*`Fs^-&shC7j1>l>p>-Oo;&dK#Mkp)FBHDu
zw3a`tgOu0hOdF^65nJjvELi0s67<%|#dn45*kE5~#cwalO~1KLA*KJ;>?6e*^K4%P
zpMDnrXXEB$O@f-O`$YuAZ{9Z}rT^9@jNsJjxZsuouM+g@)_Zn5e(N&({*w3|UQfkk
z`b~UN<|#faBQwpqvL&Ucxs$(fT7HT>j;FD}ot68<fLAyFlP__Iz5F`tT_6J1LCW`z
z<uY_*Qf6XWR_4%bt4~`CnhDnL?MU-d3fBK(m+iF__(jD@i~im-aij=|-B4%kadI3Y
zW&f}*e;E>|-%Nm=DBw-Grs;y4m-YLJcCzcR!~RXmejcBeI$L_UzDc6zu@HC#W3o#A
z85OskcFJq9qwDc{)3@u-N0(l^$L=oDj%c5heq>nNj_GOfvc~mSso;f$pxuM^I`0q1
z4JTa3=|>{U&Gy6bfRyVa*fAnjIo9p@fZIQ6)#p{4|5rtOWp&u&e1eqy1op-cy){k(
z)6;C%C*upPuj1^rv)PV6cR#tG_M%X3#>c#o^7<|IYO}+BkpsL(UcKVkIZKD<(oSI=
zcG&MoIo@U@SOJZ%#h3-Cw}T4cZfwwCV&^BW@b`OngWCH8=O3i(7uP3cWF)1|wie(S
z;<9~+9quQ@0I%J|3E^+GK0RLq&eYygs__EaTP|=4KojQwI&adFQ~d=``f*tuelstm
zY<Je>C@Vc9&0NX~TtJ>eT`C_#n`J%v&2!5~3193*q1>$hdLm#Qq`~UcapN%jVG+p>
z$MqcGgthCobKBAFUy79EhxsM-k3YB6_zaVcR{)$6&~c|vk6-y#=up8Ef2->7m;IfT
z?bf;uS)2F?GlwN5B+o?E>V8KwRC&4P(Cqu2S3YBJM~dIfGb!_JU5~2q0!C?-k67U4
zfS#JR_uZ)j;*;rr5z5VcGe4xvlePI|@2|(%2!ir|D!ba)rm8Sp^anVR4N%!kSZdJF
zAL=H`7>S7!=2CRBxeb`{BOC4AZb`e2mO^KU0*Trn;sn%2j1CjSL`jAOtT18|jV?OL
zi~+8qamEjZ0UaNbCc}^W-t#<Nd)NAL|2*lr_df4?-t(UKyyv5Bw%td;H|^UUSCp2W
zx5fjhpR+*Ki*{URJh=7T{i`34_r;D?xNp~k;}enNRHP#k*1XHjBP_BZ5?<2Y5e#WH
z9T~qOtMp=jiGu&5U2p&P`_XAll$*#Sm-8kf<DA&ruSo*8$Z!5dM6EAuj+1MIP03^2
z83pgcSmfN;?z(s7zSProb?!L8JcY=7t5FM?KX4^)D}K)BTfj3mY0I34FE$>N`{F0m
zlgPO233|1Atdl?Wq2O9y*4#weCkDP=pu<)0)8eTcw+gT5J)B2x`UjDIvN$bI7}O<l
zsDJTPWrw}59_rq-<PA&RfAVuZ=-0+M(<Zlwh1U%}9k}ST*@Fi^zWK5|Ao};9-0olO
zM?{XBo`5%>I4dqto&nw&7jAje`*mX*<rQ6%yPes8iIi)4bEu)yV>XV*{3XIr#%V9r
z?ra}7c%3u1)ZNr{;(5y3kVhW<iAcX%;q$g@8Gg%lNr2~k*{ay~KbBe%O4@~SjL3MV
z)`=UmcC#adx<nhL?=W~A)07>8rFZS@TDbkB+?Vz!N4dQ{Xn!K*nF|)0Un!mL<I?Vw
zql2%es`lijjYl7&oOm8NTt6UkT*>q-;paSL2t2pfocinZu_Lz$zu1L&2$AEs7L~Y=
zmHt?MlLAk1p|Z<R@ttii&YEuZU$KiD<#xNU-H2QVsS9ZBt)h&1W$L>DJPq?VR=B?(
zOwS`34~U#^tXyj`<;-w|w-<Z^z>?5~Nv|w_)C!NHx1%VxzjNM8<h*RDxhA@}H4G0N
z*PrpT5_~O}pWUq$Kc4nO+Ly?<(-{ft!e?(k9Xv7Mg2EFcWu<pKBN9dLL>|4#Pox}k
zn6dQECubCVdwY`ec0KXyYa&Pdg#JZj{u1ewC)6c&c20*Kf%`r=es+tq$!d1dSLglz
zxW4KQuItFf-vgfAr>}hPzL!Gj{xXn<pYel8KMb#qw1)MG`a5Q*di;1MaCUw$-Y-vx
z{w|c;{hR(wWWQ|e3IsCsr+>77XRP+QsXI>eZ<A-l&h#%L^$nXmY%{TQ4Da^>2fsK{
z{gB?5&PRsw=ve|~h*pATmPI;zZ9a2z#Y_y`=HAeRzAvwdT<Sk%rm|1d;0x<7K6SUH
zzu3o(a=U%#heZ0L`P2FGKUG<opU4?-sP)AS;Jak}@^WJKT&o+JcAD^g3ZCN<Jw=Z`
zyf*}ta<MPtF_Gf{^r+T4$5qMHW6HIvzPDC;4t##q;W^-&pa;JvDfdN>O1#$$#C!Sm
z2!_`z>-3ttT)Fk=2G6p(#)@+z@pmXEiE_K$X=ftyo3JP3>l{A<B{Ww1((Wnn-7vdh
zeZY5qkaAqtp?}-@FY^H+^8%bhXv`rlOI{0j+rIf>#nuZ?TWX5^;(6rJkBF?FUu*5C
z^;tU+R-Nqi8UmlwSmiu5cavZ4=kh0>*OdFBhvRxxZzmA%<vq7AdfXe$XhidcOn+(y
zPyfNmg=P9?E6$3X7|QMKNIxZVyw=P?I%KPHrko`BG{=qZhA%6uNGEbe^T?qciS(B>
ztsyht8uv-5f2JJQEM=dc_bheo`s%GG<-W*iM!CH{^b?}ZUz&1=%aYd(-q^ekA1T<s
z*&1I(-T=z&?ZkYH$o{YLzZ&xoJjN@RSuaPis#jv)g8lI`lXtRS<tVq;i}fH<9^y;3
zAR#laOnEwZOOJPL+w<M0V{%{W)$>2)`F$%xt)Z@em1lsr`t^appX-eZ$}1|#+0QR|
z<N@;{8V6LIZbm#v0#om+@|Hsi2Y{7_)n|9V!akt$i2B?OOaYxApd6S2>Pb~@0G;^W
zN(@+qbD;*#b5`LzV=u5C=KzzyD9*hN6LIdV9_ONxz)GAC8s>SUOG=MkU^C8@B!MoR
zr!atVoI5DOetb93f&J(x(1rciVPG8lmQ%3*rW3J0)dOtiz7nt)`x*wY8|(URu6qN^
zu|6CJI<RgU1EzpF)(3~U{)qLp6j0~771mJ<U<=k044|9ybj&}Kz;evHdVuwqZzO;^
z@^>flR09}8-ZuhtBmWr%>c|5|fl-Wa!$3F2g#^bN#K&G>5#mY|I0CFk|49PN(Ql-W
XSl_ptr2NBC2tVGZuxP(RH=h3+1R@-Z

literal 0
HcmV?d00001

diff --git a/.lake/lakefile.olean.trace b/.lake/lakefile.olean.trace
new file mode 100644
index 0000000..97347b1
--- /dev/null
+++ b/.lake/lakefile.olean.trace
@@ -0,0 +1,4 @@
+{"platform": "aarch64-apple-darwin",
+ "options": {},
+ "leanHash": "6fce8f7d5cd18a4419bca7fd51780c71c9b1cc5a",
+ "configHash": "5431361440021290490"}
diff --git a/HepLean.lean b/HepLean.lean
new file mode 100644
index 0000000..e69de29
diff --git a/lake-manifest.json b/lake-manifest.json
new file mode 100644
index 0000000..d333c30
--- /dev/null
+++ b/lake-manifest.json
@@ -0,0 +1,68 @@
+{"version": 7,
+ "packagesDir": ".lake/packages",
+ "packages":
+ [{"url": "https://github.com/leanprover/std4",
+   "type": "git",
+   "subDir": null,
+   "rev": "32983874c1b897d78f20d620fe92fc8fd3f06c3a",
+   "name": "std",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/quote4",
+   "type": "git",
+   "subDir": null,
+   "rev": "64365c656d5e1bffa127d2a1795f471529ee0178",
+   "name": "Qq",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/aesop",
+   "type": "git",
+   "subDir": null,
+   "rev": "5fefb40a7c9038a7150e7edd92e43b1b94c49e79",
+   "name": "aesop",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/ProofWidgets4",
+   "type": "git",
+   "subDir": null,
+   "rev": "fb65c476595a453a9b8ffc4a1cea2db3a89b9cd8",
+   "name": "proofwidgets",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v0.0.30",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover/lean4-cli",
+   "type": "git",
+   "subDir": null,
+   "rev": "be8fa79a28b8b6897dce0713ef50e89c4a0f6ef5",
+   "name": "Cli",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/import-graph.git",
+   "type": "git",
+   "subDir": null,
+   "rev": "61a79185b6582573d23bf7e17f2137cd49e7e662",
+   "name": "importGraph",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/mathlib4.git",
+   "type": "git",
+   "subDir": null,
+   "rev": "75e48397bac997131ff37a8cb76dae141f67f5e2",
+   "name": "mathlib",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": null,
+   "inherited": false,
+   "configFile": "lakefile.lean"}],
+ "name": "hep_lean",
+ "lakeDir": ".lake"}
diff --git a/lakefile.lean b/lakefile.lean
new file mode 100644
index 0000000..e0446c6
--- /dev/null
+++ b/lakefile.lean
@@ -0,0 +1,14 @@
+import Lake
+open Lake DSL
+
+package «hep_lean» {
+  -- add any package configuration options here
+}
+
+require mathlib from git
+  "https://github.com/leanprover-community/mathlib4.git"
+
+@[default_target]
+lean_lib «HepLean» {
+  -- add any library configuration options here
+}
diff --git a/lean-toolchain b/lean-toolchain
new file mode 100644
index 0000000..9ad3040
--- /dev/null
+++ b/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:v4.7.0
diff --git a/scripts/lint-style.py b/scripts/lint-style.py
new file mode 100644
index 0000000..da56552
--- /dev/null
+++ b/scripts/lint-style.py
@@ -0,0 +1,454 @@
+#!/usr/bin/env python3
+"""
+
+Taken from Mathlib4. 
+
+Lint a file or files from mathlib for style.
+
+Sample usage:
+
+    $ ./scripts/lint-style.py $(find Mathlib -name '*.lean')
+
+which will lint all of the Lean files in the specified directories.
+
+The resulting error output will contain one line for each style error
+encountered that isn't in the list of allowed / ignored style exceptions.
+
+Paths with no errors will not appear in the output, and the script will
+exit with successful return code if there are no errors encountered in
+any provided paths.
+
+Paths emitted in the output will match the paths provided on the
+command line for any files containing errors -- in particular, linting
+a relative path (like ``Mathlib/Foo/Bar.lean``) will produce errors
+that contain the relative path, whilst linting absolute paths (like
+``/root/mathlib4/Mathlib/Foo/Bar.lean``) will produce errors with the
+absolute path.
+
+This script can also be used to regenerate the list of allowed / ignored style
+exceptions by redirecting the output to ``style-exceptions.txt``. Use:
+
+    $ ./scripts/update-style-exceptions.sh
+
+to perform this update. 
+"""
+
+# TODO: This is adapted from the linter for mathlib3. It should be rewritten in Lean.
+
+from pathlib import Path
+import sys
+import re
+import shutil
+
+ERR_COP = 0 # copyright header
+ERR_MOD = 2 # module docstring
+ERR_LIN = 3 # line length
+ERR_OPT = 6 # set_option
+ERR_AUT = 7 # malformed authors list
+ERR_TAC = 9 # imported Mathlib.Tactic
+ERR_IBY = 11 # isolated by
+ERR_DOT = 12 # isolated or low focusing dot
+ERR_SEM = 13 # the substring " ;"
+ERR_WIN = 14 # Windows line endings "\r\n"
+ERR_TWS = 15 # trailing whitespace
+ERR_CLN = 16 # line starts with a colon
+ERR_IND = 17 # second line not correctly indented
+ERR_ARR = 18 # space after "←"
+ERR_NUM_LIN = 19 # file is too large
+ERR_NSP = 20 # non-terminal simp
+
+exceptions = []
+
+SCRIPTS_DIR = Path(__file__).parent.resolve()
+ROOT_DIR = SCRIPTS_DIR.parent
+
+
+with SCRIPTS_DIR.joinpath("style-exceptions.txt").open(encoding="utf-8") as f:
+    for exline in f:
+        filename, _, _, _, _, errno, *extra = exline.split()
+        path = ROOT_DIR / filename
+        if errno == "ERR_COP":
+            exceptions += [(ERR_COP, path, None)]
+        elif errno == "ERR_MOD":
+            exceptions += [(ERR_MOD, path, None)]
+        elif errno == "ERR_LIN":
+            exceptions += [(ERR_LIN, path, None)]
+        elif errno == "ERR_OPT":
+            exceptions += [(ERR_OPT, path, None)]
+        elif errno == "ERR_AUT":
+            exceptions += [(ERR_AUT, path, None)]
+        elif errno == "ERR_TAC":
+            exceptions += [(ERR_TAC, path, None)]
+        elif errno == "ERR_NUM_LIN":
+            exceptions += [(ERR_NUM_LIN, path, extra[1])]
+        else:
+            print(f"Error: unexpected errno in style-exceptions.txt: {errno}")
+            sys.exit(1)
+
+new_exceptions = False
+
+def annotate_comments(enumerate_lines):
+    """
+    Take a list of tuples of enumerated lines of the form
+    (line_number, line, ...)
+    and return a list of
+    (line_number, line, ..., True/False)
+    where lines have True attached when they are in comments.
+    """
+    nesting_depth = 0 # We're in a comment when `nesting_depth > 0`.
+    starts_in_comment = False # Whether we're in a comment when starting the line.
+    for line_nr, line, *rem in enumerate_lines:
+        # We assume multiline comments do not begin or end within single-line comments.
+        if line == "\n" or line.lstrip().startswith("--"):
+            yield line_nr, line, *rem, True
+            continue
+        # We assume that "/-/" and "-/-" never occur outside of "--" comments.
+        # We assume that we do not encounter "... -/ <term> /- ...".
+        # We also don't account for "/-" and "-/" appearing in strings.
+        starts_in_comment = (nesting_depth > 0)
+        nesting_depth = nesting_depth + line.count("/-") - line.count("-/")
+        in_comment = (starts_in_comment or line.lstrip().startswith("/-")) and \
+            (nesting_depth > 0 or line.rstrip().endswith("-/"))
+        yield line_nr, line, *rem, in_comment
+
+def annotate_strings(enumerate_lines):
+    """
+    Take a list of tuples of enumerated lines of the form
+    (line_number, line, ...)
+    and return a list of
+    (line_number, line, ..., True/False)
+    where lines have True attached when they are in strings.
+    """
+    in_string = False
+    in_comment = False
+    for line_nr, line, *rem in enumerate_lines:
+        # ignore comment markers inside string literals
+        if not in_string:
+            if "/-" in line:
+                in_comment = True
+            if "-/" in line:
+                in_comment = False
+        # ignore quotes inside comments
+        if not in_comment:
+            # crude heuristic: if the number of non-escaped quote signs is odd,
+            # we're starting / ending a string literal
+            if line.count("\"") - line.count("\\\"") % 2 == 1:
+                in_string = not in_string
+            # if there are quote signs in this line,
+            # a string literal probably begins and / or ends here,
+            # so we skip this line
+            if line.count("\"") > 0:
+                yield line_nr, line, *rem, True
+                continue
+            if in_string:
+                yield line_nr, line, *rem, True
+                continue
+        yield line_nr, line, *rem, False
+
+def set_option_check(lines, path):
+    errors = []
+    newlines = []
+    for line_nr, line, in_comment, in_string in annotate_strings(annotate_comments(lines)):
+        if line.strip().startswith('set_option') and not in_comment and not in_string:
+            option_prefix = line.strip().split(' ', 2)[1].split('.', 1)[0]
+            # forbidden options: pp, profiler, trace
+            if option_prefix in {'pp', 'profiler', 'trace'}:
+                errors += [(ERR_OPT, line_nr, path)]
+                # skip adding this line to newlines so that we suggest removal
+                continue
+        newlines.append((line_nr, line))
+    return errors, newlines
+
+def line_endings_check(lines, path):
+    errors = []
+    newlines = []
+    for line_nr, line in lines:
+        if "\r\n" in line:
+            errors += [(ERR_WIN, line_nr, path)]
+            line = line.replace("\r\n", "\n")
+        if line.endswith(" \n"):
+            errors += [(ERR_TWS, line_nr, path)]
+            line = line.rstrip() + "\n"
+        newlines.append((line_nr, line))
+    return errors, newlines
+
+def four_spaces_in_second_line(lines, path):
+    # TODO: also fix the space for all lines before ":=", right now we only fix the line after
+    # the first line break
+    errors = []
+    # We never alter the first line, as it does not occur as next_line in the iteration over the
+    # zipped lines below, hence we add it here
+    newlines = [lines[0]]
+    annotated_lines = list(annotate_comments(lines))
+    for (_, line, is_comment), (next_line_nr, next_line, _) in zip(annotated_lines,
+                                                                   annotated_lines[1:]):
+        # Check if the current line matches "(lemma|theorem) .* :"
+        new_next_line = next_line
+        if (not is_comment) and re.search(r"^(protected )?(def|lemma|theorem) (?!.*:=).*(where)?$",
+                                          line):
+            # Calculate the number of spaces before the first non-space character in the next line
+            stripped_next_line = next_line.lstrip()
+            if not (next_line == '\n' or next_line.startswith("#") or stripped_next_line.startswith("--")):
+                num_spaces = len(next_line) - len(stripped_next_line)
+                # The match with "| " could potentially match with a different usage of the same
+                # symbol, e.g. some sort of norm. In that case a space is not necessary, so
+                # looking for "| " should be enough.
+                if stripped_next_line.startswith("| ") or line.endswith("where\n"):
+                    # Check and fix if the number of leading space is not 2
+                    if num_spaces != 2:
+                        errors += [(ERR_IND, next_line_nr, path)]
+                        new_next_line = ' ' * 2 + stripped_next_line
+                # Check and fix if the number of leading spaces is not 4
+                else:
+                    if num_spaces != 4:
+                        errors += [(ERR_IND, next_line_nr, path)]
+                        new_next_line = ' ' * 4 + stripped_next_line
+        newlines.append((next_line_nr, new_next_line))
+    return errors, newlines
+
+def nonterminal_simp_check(lines, path):
+    errors = []
+    newlines = []
+    annotated_lines = list(annotate_comments(lines))
+    for (line_nr, line, is_comment), (_, next_line, _) in zip(annotated_lines,
+                                                              annotated_lines[1:]):
+        # Check if the current line matches whitespace followed by "simp"
+        new_line = line
+        # TODO it would be better to use a regex like r"^\s*simp( \[.*\])?( at .*)?$" and thereby
+        # catch all possible simp invocations. Adding this will require more initial cleanup or
+        # nolint.
+        if (not is_comment) and re.search(r"^\s*simp$", line):
+            # Calculate the number of spaces before the first non-space character in the line
+            num_spaces = len(line) - len(line.lstrip())
+            # Calculate the number of spaces before the first non-space character in the next line
+            stripped_next_line = next_line.lstrip()
+            if not (next_line == '\n' or next_line.startswith("#") or stripped_next_line.startswith("--") or "rfl" in next_line):
+                num_next_spaces = len(next_line) - len(stripped_next_line)
+                # Check if the number of leading spaces is the same
+                if num_spaces == num_next_spaces:
+                    # If so, the simp is nonterminal
+                    errors += [(ERR_NSP, line_nr, path)]
+                    new_line = line.replace("simp", "simp?")
+        newlines.append((line_nr, new_line))
+    newlines.append(lines[-1])
+    return errors, newlines
+
+def long_lines_check(lines, path):
+    errors = []
+    # TODO: find a good way to break long lines
+    # TODO: some string literals (in e.g. tactic output messages) can be excepted from this rule
+    for line_nr, line in lines:
+        if "http" in line or "#align" in line:
+            continue
+        if len(line) > 101:
+            errors += [(ERR_LIN, line_nr, path)]
+    return errors, lines
+
+def import_only_check(lines, path):
+    for _, line, is_comment in annotate_comments(lines):
+        if is_comment:
+            continue
+        imports = line.split()
+        if imports[0] == "#align_import":
+            continue
+        if imports[0] != "import":
+            return False
+    return True
+
+def regular_check(lines, path):
+    errors = []
+    copy_started = False
+    copy_done = False
+    copy_start_line_nr = 1
+    copy_lines = ""
+    for line_nr, line in lines:
+        if not copy_started and line == "\n":
+            errors += [(ERR_COP, copy_start_line_nr, path)]
+            continue
+        if not copy_started and line == "/-\n":
+            copy_started = True
+            copy_start_line_nr = line_nr
+            continue
+        if not copy_started:
+            errors += [(ERR_COP, line_nr, path)]
+        if copy_started and not copy_done:
+            copy_lines += line
+            if "Author" in line:
+                # Validating names is not a reasonable thing to do,
+                # so we just look for the two common variations:
+                # using ' and ' between names, and a '.' at the end of line.
+                if ((not line.startswith("Authors: ")) or
+                    ("  " in line) or
+                    (" and " in line) or
+                    (line[-2] == '.')):
+                    errors += [(ERR_AUT, line_nr, path)]
+            if line == "-/\n":
+                if ((not "Copyright" in copy_lines) or
+                    (not "Apache" in copy_lines) or
+                    (not "Authors: " in copy_lines)):
+                    errors += [(ERR_COP, copy_start_line_nr, path)]
+                copy_done = True
+            continue
+        if copy_done and line == "\n":
+            continue
+        words = line.split()
+        if words[0] != "import" and words[0] != "--" and words[0] != "/-!" and words[0] != "#align_import":
+            errors += [(ERR_MOD, line_nr, path)]
+            break
+        if words[0] == "/-!":
+            break
+    return errors, lines
+
+def banned_import_check(lines, path):
+    errors = []
+    for line_nr, line, is_comment in annotate_comments(lines):
+        if is_comment:
+            continue
+        imports = line.split()
+        if imports[0] != "import":
+            break
+        if imports[1] in ["Mathlib.Tactic"]:
+            errors += [(ERR_TAC, line_nr, path)]
+    return errors, lines
+
+def isolated_by_dot_semicolon_check(lines, path):
+    errors = []
+    newlines = []
+    for line_nr, line in lines:
+        if line.strip() == "by":
+            # We excuse those "by"s following a comma or ", fun ... =>", since generally hanging "by"s
+            # should not be used in the second or later arguments of a tuple/anonymous constructor
+            # See https://github.com/leanprover-community/mathlib4/pull/3825#discussion_r1186702599
+            prev_line = lines[line_nr - 2][1].rstrip()
+            if not prev_line.endswith(",") and not re.search(", fun [^,]* (=>|↦)$", prev_line):
+                errors += [(ERR_IBY, line_nr, path)]
+        if line.lstrip().startswith(". "):
+            errors += [(ERR_DOT, line_nr, path)]
+            line = line.replace(". ", "· ", 1)
+        if line.strip() in (".", "·"):
+            errors += [(ERR_DOT, line_nr, path)]
+        if " ;" in line:
+            errors += [(ERR_SEM, line_nr, path)]
+            line = line.replace(" ;", ";")
+        if line.lstrip().startswith(":"):
+            errors += [(ERR_CLN, line_nr, path)]
+        newlines.append((line_nr, line))
+    return errors, newlines
+
+def left_arrow_check(lines, path):
+    errors = []
+    newlines = []
+    for line_nr, line, is_comment, in_string in annotate_strings(annotate_comments(lines)):
+        if is_comment or in_string:
+            newlines.append((line_nr, line))
+            continue
+        # Allow "←" to be followed by "%" or "`", but not by "`(" or "``(" (since "`()" and "``()"
+        # are used for syntax quotations). Otherwise, insert a space after "←".
+        new_line = re.sub(r'←(?:(?=``?\()|(?![%`]))(\S)', r'← \1', line)
+        if new_line != line:
+            errors += [(ERR_ARR, line_nr, path)]
+        newlines.append((line_nr, new_line))
+    return errors, newlines
+
+def output_message(path, line_nr, code, msg):
+    if len(exceptions) == 0:
+        # we are generating a new exceptions file
+        # filename first, then line so that we can call "sort" on the output
+        print(f"{path} : line {line_nr} : {code} : {msg}")
+    else:
+        if code.startswith("ERR"):
+            msg_type = "error"
+        if code.startswith("WRN"):
+            msg_type = "warning"
+        # We are outputting for github. We duplicate path, line_nr and code,
+        # so that they are also visible in the plaintext output.
+        print(f"::{msg_type} file={path},line={line_nr},code={code}::{path}#L{line_nr}: {code}: {msg}")
+
+def format_errors(errors):
+    global new_exceptions
+    for errno, line_nr, path in errors:
+        if (errno, path.resolve(), None) in exceptions:
+            continue
+        new_exceptions = True
+        if errno == ERR_COP:
+            output_message(path, line_nr, "ERR_COP", "Malformed or missing copyright header")
+        if errno == ERR_MOD:
+            output_message(path, line_nr, "ERR_MOD", "Module docstring missing, or too late")
+        if errno == ERR_LIN:
+            output_message(path, line_nr, "ERR_LIN", "Line has more than 100 characters")
+        if errno == ERR_OPT:
+            output_message(path, line_nr, "ERR_OPT", "Forbidden set_option command")
+        if errno == ERR_AUT:
+            output_message(path, line_nr, "ERR_AUT", "Authors line should look like: 'Authors: Jean Dupont, Иван Иванович Иванов'")
+        if errno == ERR_TAC:
+            output_message(path, line_nr, "ERR_TAC", "Files in mathlib cannot import the whole tactic folder")
+        if errno == ERR_IBY:
+            output_message(path, line_nr, "ERR_IBY", "Line is an isolated 'by'")
+        if errno == ERR_DOT:
+            output_message(path, line_nr, "ERR_DOT", "Line is an isolated focusing dot or uses . instead of ·")
+        if errno == ERR_SEM:
+            output_message(path, line_nr, "ERR_SEM", "Line contains a space before a semicolon")
+        if errno == ERR_WIN:
+            output_message(path, line_nr, "ERR_WIN", "Windows line endings (\\r\\n) detected")
+        if errno == ERR_TWS:
+            output_message(path, line_nr, "ERR_TWS", "Trailing whitespace detected on line")
+        if errno == ERR_CLN:
+            output_message(path, line_nr, "ERR_CLN", "Put : and := before line breaks, not after")
+        if errno == ERR_IND:
+            output_message(path, line_nr, "ERR_IND", "If the theorem/def statement requires multiple lines, indent it correctly (4 spaces or 2 for `|`)")
+        if errno == ERR_ARR:
+            output_message(path, line_nr, "ERR_ARR", "Missing space after '←'.")
+        if errno == ERR_NSP:
+            output_message(path, line_nr, "ERR_NSP", "Non-terminal simp. Replace with `simp?` and use the suggested output")
+
+def lint(path, fix=False):
+    global new_exceptions
+    with path.open(encoding="utf-8", newline="") as f:
+        # We enumerate the lines so that we can report line numbers in the error messages correctly
+        # we will modify lines as we go, so we need to keep track of the original line numbers
+        lines = f.readlines()
+        enum_lines = enumerate(lines, 1)
+        newlines = enum_lines
+        for error_check in [line_endings_check,
+                            four_spaces_in_second_line,
+                            long_lines_check,
+                            isolated_by_dot_semicolon_check,
+                            set_option_check,
+                            left_arrow_check,
+                            nonterminal_simp_check]:
+            errs, newlines = error_check(newlines, path)
+            format_errors(errs)
+
+        if not import_only_check(newlines, path):
+            # Check for too long files: either longer than 1500 lines, or not covered by an exception.
+            # Each exception contains a "watermark". If the file is longer than that, we also complain.
+            if len(lines) > 1500:
+                ex = [e for e in exceptions if e[1] == path.resolve()]
+                if ex:
+                    (_ERR_NUM, _path, watermark) = list(ex)[0]
+                    assert int(watermark) > 500 # protect against parse error
+                    is_too_long = len(lines) > int(watermark)
+                else:
+                    is_too_long = True
+                if is_too_long:
+                    new_exceptions = True
+                    # add up to 200 lines of slack, so simple PRs don't trigger this right away
+                    watermark = len(lines) // 100 * 100 + 200
+                    output_message(path, 1, "ERR_NUM_LIN", f"{watermark} file contains {len(lines)} lines, try to split it up")
+            errs, newlines = regular_check(newlines, path)
+            format_errors(errs)
+            errs, newlines = banned_import_check(newlines, path)
+            format_errors(errs)
+    # if we haven't been asked to fix errors, or there are no errors or no fixes, we're done
+    if fix and new_exceptions and enum_lines != newlines:
+        path.with_name(path.name + '.bak').write_text("".join(l for _,l in newlines), encoding = "utf8")
+        shutil.move(path.with_name(path.name + '.bak'), path)
+
+fix = "--fix" in sys.argv
+argv = (arg for arg in sys.argv[1:] if arg != "--fix")
+
+for filename in argv:
+    lint(Path(filename), fix=fix)
+
+if new_exceptions:
+    exit(1)
diff --git a/scripts/lint-style.sh b/scripts/lint-style.sh
new file mode 100644
index 0000000..ff9ab08
--- /dev/null
+++ b/scripts/lint-style.sh
@@ -0,0 +1,37 @@
+#!/usr/bin/env bash
+
+set -exo pipefail
+
+# This is adapted from the linter for mathlib4.
+
+################################################################################
+
+# 1. Call the Lean file linter, implemented in Python
+
+touch scripts/style-exceptions.txt
+
+git ls-files 'HepLean/*.lean' | xargs ./scripts/lint-style.py "$@"
+
+# 2. Global checks on the mathlib repository
+
+# 2.1 Check for executable bit on Lean files
+
+executable_files="$(find . -name '*.lean' -type f \( -perm -u=x -o -perm -g=x -o -perm -o=x \))"
+
+if [[ -n "$executable_files" ]]
+then
+	echo "ERROR: The following Lean files have the executable bit set."
+	echo "$executable_files"
+	exit 1
+fi
+
+# 2.2 Check that there are no filenames with the same lower-case reduction
+
+# `uniq -D`: print all duplicate lines
+ignore_case_clashes="$(git ls-files | sort --ignore-case | uniq -D --ignore-case)"
+
+if [ -n "${ignore_case_clashes}" ]; then
+	printf $'The following files have the same lower-case form:\n\n%s\n
+Please, make sure to avoid such clashes!\n' "${ignore_case_clashes}"
+	exit 1
+fi