From 8f3cd1d9d50a4f9fe70b9310cf080b6178a4bdd0 Mon Sep 17 00:00:00 2001 From: Arne Keller Date: Mon, 15 Jan 2024 10:39:42 +0100 Subject: [PATCH 1/4] Extend HowToTaclet with a quick example --- docs/devel/HowToTaclet.md | 52 +++++++++++++++++++++++++++++++++++++-- 1 file changed, 50 insertions(+), 2 deletions(-) diff --git a/docs/devel/HowToTaclet.md b/docs/devel/HowToTaclet.md index d7997f5..50e06c3 100644 --- a/docs/devel/HowToTaclet.md +++ b/docs/devel/HowToTaclet.md @@ -19,8 +19,8 @@ system. In particular, the following topics are discussed: The standard location for `.key` files containing taclets is in the `key.core` project, location `resources/de/uka/ilkd/key/proof/rules` (*note*: unless stated -otherwise, all locations in this article are relative to `key.core`). The file -`standardRules.key` lists all the taclet files that are are loaded as defaults +otherwise, all locations in this article are relative to the main source root of `key.core`). +The file `standardRules.key` lists all the taclet files that are are loaded as defaults when starting KeY with the Java profile. New taclets can be added to either of the existing files listed there (if they fit into the scope), or can be added to a new file which is then referred to in `standardRules.key`. @@ -36,6 +36,54 @@ Taclets can be added to "rule sets" which are used, e.g., by strategy heuristics. Default rule sets are defined in the file `resources/de/uka/ilkd/key/proof/rules/ruleSetDeclarations.key`. +### Quick example + +Consider the definition of `cut_direct` below (part of `propRule.key`). + +``` +\schemaVariables { + \formula cutFormula; +} + +\rules { + cut_direct { + \find(cutFormula) + \sameUpdateLevel + "CUT: #cutFormula TRUE" [main]: + \replacewith(true) \add(cutFormula ==>); + "CUT: #cutFormula FALSE": + \replacewith(false) \add( ==> cutFormula) + \heuristics(cut_direct) + }; +} +``` + +First, we need to define the variables we want to use in the taclet. +This is the `\schemaVariables` block at the start of the `.key` file. +We only require a single `\formula` type schema variable called `cutFormula`. + +Then, we define the actual taclets in this file by creating a `\rules` block. +For the purposes of this example, we limit ourselves to the cut_direct taclet. +`propRule.key` contains many more taclets. +The `\rules` block contains the taclet definitions, each of which begins with the name of the taclet +("cut_direct"), creating a new block defined by curly brackets and a semicolon at the end. + +Since the `\find(...)` part of the taclet definition does not contain a `==>`, the `cut_direct` taclet finds (matches) a sub-term anywhere in a sequent formula. +The `\sameUpdateLevel` essentially ensures it doesn't match under an update application. + +The taclet creates two new branches, which are defined directly afterwards. +The first branch is labeled "CUT: #cutFormula TRUE". +In this branch, the found sub-term is replaced with true (`\replacewith(true)`), and the found sub-term is added as a new sequent formula to the antecedent: `\add(cutFormula ==>)`. + +A particular branch of the taclet can be tagged by enclosing the tag in brackets. +The first branch in this example is tagged with "main". +This tag must be written after the label. + +The second branch of the taclet is labeled "CUT: #cutFormula FALSE". +In this branch, the found sub-term is replaced with false (`\replacewith(false)`), and the found sub-term is added as a new sequent formula to the succedent: `\add( ==> cutFormula)`. + +Finally, the taclet is added to the `cut_direct` heuristics group. + ## How to extend the taclet language !!! danger From 7ad42a5036daa09ec9b776a61686a99af213ffce Mon Sep 17 00:00:00 2001 From: Arne Keller Date: Tue, 16 Jan 2024 09:57:27 +0100 Subject: [PATCH 2/4] Document linearized proof tree --- docs/user/ProofTreeLinearMode.md | 17 +++++++++++++++++ docs/user/ProofTreeLinearMode_enable.png | Bin 0 -> 50945 bytes docs/user/ProofTreeLinearMode_example.png | Bin 0 -> 23841 bytes docs/user/ProofTreeLinearMode_example2.png | Bin 0 -> 29239 bytes docs/user/UiFeatures/index.md | 3 ++- mkdocs.yml | 1 + 6 files changed, 20 insertions(+), 1 deletion(-) create mode 100644 docs/user/ProofTreeLinearMode.md create mode 100644 docs/user/ProofTreeLinearMode_enable.png create mode 100644 docs/user/ProofTreeLinearMode_example.png create mode 100644 docs/user/ProofTreeLinearMode_example2.png diff --git a/docs/user/ProofTreeLinearMode.md b/docs/user/ProofTreeLinearMode.md new file mode 100644 index 0000000..5d033e5 --- /dev/null +++ b/docs/user/ProofTreeLinearMode.md @@ -0,0 +1,17 @@ +# Proof Tree: linearized symbolic execution + +In the proof tree settings, you can enable the "Linearize Proof Tree" option. + +![Screenshot of option](ProofTreeLinearMode_enable.png) + +## Effect when enabled + +For symbolic execution steps, the "Normal Execution" branch will (visually) continue on the parent branch. See the screenshot below for a quick example. +The exceptional case branches (e.g. Null Reference, Index Out of Bounds) are therefore placed above the steps of the Normal Execution branch. + +![Screenshot of tree with option enabled](ProofTreeLinearMode_example.png) + +Additionally, the TRUE branch of cut_direct applications will visually continue on the parent branch. +This mechanism may be extended further by other taclets tagging their "main" created branch. + +![Screenshot of tree with cut_direct](ProofTreeLinearMode_example2.png) \ No newline at end of file diff --git a/docs/user/ProofTreeLinearMode_enable.png b/docs/user/ProofTreeLinearMode_enable.png new file mode 100644 index 0000000000000000000000000000000000000000..11bd9ed898aa223ca703f8c61756156e0fbc51b3 GIT binary patch literal 50945 zcmaI-cQjnz7e9=TZgfNRU>G%`_iohDTN2T`=ru}oM(-_pZ%GhD5Ya^^hy>Al5WSaC zo}2gg^Zl*$d;WM9*1BWvJ?EZ%c6sgB**ivCQ<)Ht1`h-R5h7F+bU`2tFbIUEfQt?M z$EnAI68PX|FE6icZ)F7n`OanhkWhi^&K72TB!Ogid_SjPhzPmE^nERoMyy*BP%E(_^1)Na3H4&Cb-dJxZk=Z-nu37b@2OM zClO|z#qxxLXeeeQcHul8nM8jZ&yi!2m!QP_xhBa77Lpqx8u#$5v*43ZvNhwoM>VOt zug%|->XR>FVK-Knv`S;$zV(-zxh$y_zGccI?GLYel=QuY9&S3<%pXUR{Y<{ z_pO?O)%Y)v2>~xlbs!U&{F#{w3{=oj^f-kS9gZ|+tr(D)y0w!f65N>0pfsw?QJTsY z6*(%2ML^ywxkemh=UBqxPh4+^x>`*%5}top51<#o z)9B~pJvdI$m#pe?d6WB zl~|DXJO41#m-AwaE-6v`fi*`iN21X9ise_ua|q^IV0lr=yA>?2E?Q1gN>f?NSZ*Ah zU%{)RZBf}i>o!8`@dD$-L~YAr%cyR@7vrZM(tSQEz2>}Bu?kFb`1ttbaeY@UrnPZ) z)H_}|J*&L60@?8kmnSE12?+_yre}3vFOO_`EEq}BXNtMIFjYRU8rnTi9at~!>r^U*N_=#6cK&g3alxL}wX6GHK}$<3PeNL{LaCH*msPId=kPFI&Bu?! zSGTuxGXm=9|BZhoq29Bwuwa1Z=jEk9NlE!@$IF^KTU|AcaWvEb6(Iexv$M0Zp+Uf- z#n@O42Fbg8)4r}A7H?UvlAD_wfRf&2g%*x`a?>Ob9cE9QE-lgj-*K(j|7>mTTwHip zhY&=-;iIPp@uszGRa2_9wY8J5XrGU@wL2>-A$gjWBwvjMa=%Z)zAU;3<85tiF>8b^ zA68yo`dBa_%{Oy>(uM?2S&Nqs@f&*Wtm+L0SKTJ&=V^1J5K?BQrjtWM;3T$3cvxAO z|E-7j8Tofx&(tsJ4d)^vB9idWZEalr7QX5grnR2!Qw~4Y*O`|i4-XI1lu9i^7xujo z@AW79`>`KNfsI$nK{^RPAwZH0ugzN$CvkpnLaeNimPAG296z89OiewSa%hZ^Qf49* zmy{$IvLH8y{5NHnzD^zEEwTJ{LOaUG{t4bU(SrJYhB9k*{bTJ+qP0Cs94xzTIZ{r% z=a`Bl;&vmc91}H;QJCnVFcQcK#wTlB4k#2lWK@9BZ2U@}SM}otD%9syiidyFx4;9b zL%+_4l?OGIe=|WtlVw$+g&#wTq#1?29PaHIu%_`*6Ga8>&h78lU^z7A1dX|(@U0tO z2A-b=ALcdu{HaHqG=SfEUl$J2`RjHuBPU|*!`bC&OWG^pOGc$x+O z?(dJhH#wiL+XjJ1Ah=*8rlf-FRK8~i4vUkI&x}Yr&ac~#O1_T;stYIrEpX`=80MFj z3Z#^q=bt70sGg*Z%lsPj<1pvOjhx=V7XaHK%^8XlWVJAlN7*HsY7M9u~$2r z2}<9z);d~Rz%&7OK@aEWuN|A`SpjVhI$C-q$j?EJHy2qZ#)3zDkM?kLW0)|a^X1;H z5Pmcjs)z#$NtPvr9FYsL0`_~Y7b`3xvcJ7O*!jBld6hVaN;u&+*NyXrdpXG>`z4y+ zm2v@NVj9XX%({DOW%f2UdWm)0Iy>#U(Lm;{q)hP8kmQgEaS4f^r0*AS|H(5NgoO@A zr}&`z{;HNBUo$Ef4J5132ayp_da6MRsnec&^SQmf3ciUAqZ$L*POp#i?2^*9E>|!8gJeLm{zTv>!Vj#%x!+%+p`m?Z z4Q6;83=dm=S6wYA0iECXUhK}I1)Lf#xZq>n8Xn^NZ^qdOl+E48PV3Pt7#UG@2CrX* z)755C^}LSl+(#a1SrSIrRr&!UIX}N9H+JXN-vy8tBh2?x`KUY#{#e;pwjC%Qn>|!npLHyJg2uYY;ZaD|b|$=VR*0VA-s;yRi^kH5n0` zAqRL^(qoyRg+2Cw%L5Y^08#)$f0*PKv9IjxdqhIT9@o%xb2iu7c^hjqBknu~ZyvvP z+TuP~!XVT~Vlqhhos@yW&92LTY=I4chgCW(r1Q}3gM1DqpG6WRWpsa&arv|^>3&0J zX4*QRe|?4cDdnf>ND2wq8_gDAh3UU|;VJOXXLRe8A5yiQ-mkoQy!>(eb(M%}a)(0$ zm~dM7FhcRKAbl_x{1rXTyYAshK9PdTD;%$!9}~s$EKi?mxGa9{BLs8;iK&&*fuy6N z+TOb&imMlCf_}W0G;mfrOf-*L9FavtL_lb0 z9F)i>fBtNNf&e9737sVB97*OCbtq$jd8ICx-93SwF_3VJDQ?n(!D^my#*IIPk(e^n zi0J5OlBjP`At9j!5)epMxN8j3HiNO)`Fu~(E@8Hff(u~K9Xs40sjgCnel`=w9_wk zc8lAn#wAZAULfAp)NKBr{b76Jfn4wo*PlSH5s}an%$K zbon4r?%e)KtB2Bz$LWXIej!WC*XPcq&S0=Kuv=`7GaobFy<`8MrhE z)pU>OWer*?DwVPgNc|XQ{hTCc*Pvp5LEPsz4zrgKqmSx*)ArXiO1t6KaHgC^cQIj$ zRO`dr2AeH{I4{?M&AuvJur!_A#G{0@wKeOlvHbtZ)cfi3=hp6DCC~i) hu;sV$g z^ojv0w|m#EBR+1XcBxYIQ|n*g38DPGElLLXcHo*32wMNU0DQv>&L>Y;Bqfdayj#i1 z$*<0^wtti=kKCay`zWVts#0H=)g%)=R_(JznW(DXQ@B21|MIbLvpOqloja*{x~{I`O}wUz(jjGp>mZi z+T@DYdVXFoi|;u?-y@OR+pkWkafs z?bL)_9%^xadp(yp2HXKm>3?~Uo$R*vo6o)`fmUP~2_`G!Xl!isIRE>s06^97FcEpU zhsUQ#v=`-at1&xu+lF__iFC!MN;=MTkY9r-%q+~z@&^ko%&%X+p43%NqR*I^(0>2! zT{5kROP02Ic_{&n!o}h8I2qnQ!&Fk4;82<-MRo+Da`L@uja!)Jn_V-d18)qJ$qfb1 zw~to8*?y}^O@-XmnB{sKU=z{3)1%mK(@7_Whus^;Bqhxxc6fq+y)|s{C|6Ka%sw0+ z8X~R2!l%f3SkKPRmMs2fzOG2jz+@w3d_hLzuU)W( zMMXu8MBr26g2|_d;BX^1Q95zU!TfX``}6^qYNVXJCu8(F53(=wVgUhGe`lzk~J za2UAkb1-#CNq?|#IqLCeG*4{&^5xijQQ|P1Z-@R5cbBJ`9zN~BuBc?EsW^xtx{kWI zoN|SoC%0j^VT{qR^jMg2;Q3Smh;dx%GLJ_-N5u7DB-yahA$tq{i%PYX8vzt;&8o#%%?_whF^R%rmlY3(Cv2=Q^6CIX@EHoCsyIkKvmrg#=*VWH$@G2|wtBYn6DIFy4Z#GGKZq&UUaI+Pgbq3uBLmnG_egy?)=6H;lcm@4$ z^?4jHi|dokL@H!VmxjpV#vjqn`e&m@$+U}G7-8vXny)%L>HLQD#=#5HHybgy1(B*M=!l{8hC-Dv1>JC!9%7kW z5{pk|!5A1UVnM&&=~SaE-)7?ZD$F-IJDPTm9_?x|2FRR-x*jqF-==I_Q(YFy z-Kk->1`gJv&VFh+4x{qBQD*wqXZJT385dlsZnnut3>+d^@*et#Xq?sIC$(PlBFh1u zb)H*es^d|gmW$r_$xcGAPmNeHMyg4j3^E%>B@PKGLSU&*D(H7Y&vAJO*83>Uyow{;sYG1p1SrK^ z*K=JvsP~pTWk46l^c!$em+ecNnzy|7_bAtCb2n@P;?lOPED={zUW*<~;kY+3|w zT@Qt3jLGtRmi$~6bDvc`$Fe^@8R6N|`}FcO%#P-L?s32C>^z^apHAt`jStSX|)@N zfj}vqN{1RD%Si9_iX2az#aa#~$21fTOV%Q%AV53oJKvqb0r9qgma(5(jbSysx6sa# z@)usl6iMl67?)N{aS!-a65k9_V?+TeUsyja>yaTDe{xcMw0nBDP8+!RdPYpKMJ^os zv;9j%*j<360wn(8Ngpch4)shF7xAYR-od;&=)?>dCFjO2J$3>n+#2@@Jmb#oBhS~Au%Q1X31;V}WF(GaU7b73WJ-;lwVo*)L1#B+{vY^?qKDg{ZP z0>4l|i|b5hj!}RpL$o8a2%qwsaI8j++P=l84)vwKtG25#Y_$BUM;>%9k~B~fZQ11$ zBbVolZ7)gYw4RR}9`XBk(v=mUWGb?uLh126AICpWR@->)lxKd8;FTKwgE$%=`1+u( z($gD5rt=YOXQNAavf-;-r|r*@c1hTmdYR%`G}u5`m$QCnYb#YT6Lfbz47t?ZR%H>H~A#?1;9RfY(yY23K}0vbRJ>@CCk-O$y)g-zXKBY2Z|HvjLc8X{r7 zC2j+ceI^j)bO=}~E`o7`B!Zz&iZVcCP-eJq^;;CRetk8hVguW!%Zw{)`q-DmfM*lX z9{FpJd7ic-IIqnxd6U)p+xP1LDnkcW7XX9ao$HW80;&bc;>?FeY#jfYuGv zPFcyM@2}Ro%MfWNk+k3Q#K`a&<2Y{Im~AB+64{jK)Y$Mq;R0byeXfD1i-c3jt8=3e z9aG!XsSB!M8Zvnj9E~L^fuF_NCldI^Z)0J<$3^^8yPSM~(ehAQ2v|UaS#u2N zv>-i)Oow)pZp5lZn+NqAo5=Dpt z1O|ywLC0Vk7K7qmPXJ(p!eBJ>%c#2bYPQmCh|A-oHH9qD(7R-Ui=C+|%K0(16#O1m zF%b&e)Bi}n6uG1$WO{s`4q=)37-c6Jnb7^4wsnLGaB()gNc-C@sx5!c< z!4l8uwVfkYRH%R}>fnU*T35ezH~8XaVU4Gc2@@-D zB&L@X1!>9Lea^Lj5f45yH{1vt2JmK5)Hjx7iZB4~dK8X64`-o``2D4W5O=O+s~~Q& zKlU7{QJ27ruj!zr{Ify>@v%I}CFqvKU;v$k4qq~6=i;>faM@wG9B-ITe ztuQ7K<6y=Ey8L&yS1@`Wqo()(^ug#$n8ChP;j)X&0T`kY%mk%S%;??ii=#9;)M`4+ zyt}QrsIQQ1Oyv2Fa=bLNpI`#puz>&Rv=qyOr31mzsN;8_x#7<^l|+%tdOJxlzxgWRUcS1)M#(Dy_=_AI%GE8jW0z2Eiy=V=z*VOTCE zv2omA*}q)OIo8L1(v`-ysWAKw=u(6dmpJQ{y=sfwF6D}8ajf3YrI;P;36ATIB*a@c&MV^oi0 zyUc8d*~Mw|+<>9_ckvFv!`j8*f6*a51Ga6C8)jZ~6I@t#_K7|$RQK`t4Y*gA?2Wdz zm^rsMg_D5x=8a7>K|#`D$1JlrGbKGf#?<-UbX1kYe(l90au-;N3M{gW2~1GX`-sfW zxrltg3SmuJ6E+fK#|jIzhpM3k-|eMzpYqL#80pGdN?GvuKB+S_s^6KqzI*HaqVeJd z3XkcZY*W)=d4!^FE1(7u(zK61j`tkQRM6v`NfY7kz^iT>INQbGFcsiOfhlE!G(sLP zj1iX!Y{!r2Qta0~ZC(!Yce~!qWOlORvtY&LkOu~Y{RgLKu0=X%!e_c%`787&9u0k+b}7xn8DTh*qq9OVh1?S{tjN z3r3iCmp3`jV`GKct5>ZvDO7*@TWMmAO^(6R8vJL__18Pnm<;zgg#E8E^ovu(f{aSe z-AXty5H#iQUfeY+NfrW;PN0wLCshNF-eN2)Jr&jl>^%F!`;B~`rT1rf0PeDp{##e~ zhSTOH-sSLzY`>8g)dt;gv6SU(+MG<`&rkcbnTF&c23`(5NU$85`Iv`HbKvW~5uVOG zg(3FYyUwe%xb7LV;O`ab@q5V^*RXwt(J3uU!NZW3rV8&KK0HiEZ+)9%1wyfl+tG^L z%u=ORAyF*a^pu61=5rFerx06%-I?0uml_ZQLn*Up(qUfwxea_N%bc%mTh5bZ2YYm9&<8-1x2s% zanW~~7jUrmFTXh>GtqkFsEFex>tbOA(I&0lim4x>=|pgYfY9qwT#Y(t<$1O6rQY*9#=uE`C9#qEGeKeasJvHU;=M7r)9G60_@zej_yg21UDO1IVOO}$c zX=ZIIhTYWOxEiLPUb}Uu%u_sB*#7li@8g(SCO4sFO0eRgKrU<{;Pm^o3Wz}(W+s-P z2Vih{NG@5II|;_U-AfNA@0;imq z8brYERQX9k`f|Z@?;9xXL%{J`ANy;9c!Iyay5O3lP2l~l-CnD%0GtA^EN@o5?_0iT z7KtDrVL3pZ0olOOcTemDfMTfg)muZ^72FrgNByDg)i$P%=KEr9uashOq^aL|eY#~u zddcNXIyr!=DU-j?#ckG;D@3a@(b<& zPjf!d&AX#-jL{R4s>Qa7g^XSqTJaV4r9+r61Nkk^&q}RI>Ak2-c_1`$@FQ@Iei%f@ zcC-aQ-0Q1iV@v=!U11YlDcbTQu3-1)yx1`+)x4K{LASnEBx+ugLlsK!cYY7X;fMN5 za`6#^pcT~jmaF^O^SGqIt*fU-O};GQ{=`PhqFZ@lo?)ClUxQl4h{4hLe7wU6TWJL_ zP(O^o)YdPh=)USc7h5q%dNvL7OkIWOyjKr*M?C2EYE}cn-Ep;6x0ci=#e0B~X;*+rlnSd*|zj}OWkb!l}zWhzI+lRz&Si{2TsD9?q z+{8Ov`4bzGOwm-?REjN&p+GJLW1q9_AOGwy1<}J+7y!8*oNOK;`5A8!Iy=kDc~oyl z!f4D)#~q3mewaqdRS9gdAa=d=fC%6Ys03eWXQan}eZ6~<@PW%1`Z17fig=xX{#o_6 zfWldZm#yA4FZiP)#v5-escV?3cQf~IlR*TEq*R-KP7zv=qX19thBlRd?&tf_wY3(c z3m`O)y^`zp=IQ|&q-W}7c5lw5a$+ywm9(Wjqo9xTfD!gm4m z=c0D4ZK7-T@*&H~}# zk{#Nft}!A}+673BVrzpLo|$VXn!EduQp<6`WEy70K$(ky$oK#0bJbSbBSc*R%iUs{ zc!@529EW&3TMJ?ekT-C$Ouws$WF+2Z{sx07Q%_vm$zr49izZT2+qF}b01F`0$3J2N zBZ{o*mcy{{1E}-aqhPX3zlkXs^GUl|`dxdcV_+(<9ToKYN&;yt4(i^^6WTQDkYNaI zy>U6uC8Kie{hpP!Siknst+|@92hr#{_{BhFXvillTX2+CRj4K))5Kz-7bOb_FI{#T1o4PBS!B*JsE^X1QnT7Csd z8W2_8;E6hmZ|1}498PPB>(q*KmrnWU8OgNtZpC^E&qA;(G;Qk%bV z=zT-10EC_D1q)Ts>|hvek~3Qi&o>wX0gMZ8I3@)v_NTU(gn&-j9uI8!YB*A7Eoa~_ z1-&4j%9R_a;~7^DfLOXzzTn?=+W)NBkaG|2U11du0(S5-zTY$BLR5cEf@R9tJzuJM zf_km>@ALJ7t00JD;xVRTN*gx>@&wzJAr?V&d`yY~vB2~VCHv2W|BrxXWqM@! zEa*;ohvO!s|91ZEv|ldtkYb2~k(b_YM{dV%zm;^f4J&Eq9FrFnk92HuO;cngq`P(G}cgI zm+5l6J9h#_dchsRJLv?iK?^v`h=Vu-V~;M}bA{DoRqSQexrDOW06q4Td^Xk`G!ZCZ z;k&mHX_%<%tUG1`*8P9zdc`80vN-Tp@Ko^6Hkp@_47o6J)8Ij}t&02YTuHk*-aS9L zsIol&6_XX}!edw{(U1lk3$DR$oxHf0I2_B67z#Zy-QIWsgA7`BYG2bd5D%}aJlf#Z z?W|0pMy_y*U`)guXY-tLzT%xo_ci+O^BpUi2EOWDL8vL^>Y$TASfy@r6!|k z6DcRqDAIYn*5}7nWGO3|I4Arh6?`#{qbBHx`FqnF^{(OF!`lxJw#2RXOyE8W%WsVM z%}Z|_-DYhv#ai~8<_+FwB|%V(|3P6G)L&nMCHzSH&l@)G7S+1(TAY##Qq`H@^ZPi! zGJ$ju0IvV&+W(JhL<<7F>hldp(h$!uE*E{THGy9x)#om{^#mFrPSN`0G6f3LVNCD4 zhL(r3%}MEh)Z~9Du^p1F+w^%So!Snnr4gS6T#Y^cVK*YIWg^?EK%5-R#n~I!H(Vqa z4w)&8;LI+}^IOWUaRHbk`@=%NnU@N~hppB_kllOyrv}q=>-+SRKD)+*O^S z!?OwC9BAbmu?#^h7KM|gPI+BCgG|B8RRazZx}BqO?Mn9qlu7QVP^ zS86^c*ROa^^yFCm#{gWk`u9)}l1TA+U+=In;L)ESdZDVj5jcy@(e(gXmU+-64s`3poNGZ;Wl3N7Aoa=@)gK2scFoe%e|FV=Kq zq1XVsw?@Z);^eO;iX9J-;-3~|cAL$qqhPQLn46>mmLj#l;gz=?Q=i_?=9 z!t@tQ&3n8+svYt$#8$XrnAXm(9y|)AK1&dUq2UKConmlpCZCF~v~N!oW5fzYk}b=; zd@qfS6mjQYxuZ1w zzq$p`ZKggh z32QCPsvXmnB`I=6T)jJ87rvw%Aq`S_EqigXwNp2Z0}htj{lkSErxl_JEwFEu1|g={ zr9q_Sj}^fqR4CGM+8J*EBfa)xOk>sPX;}UHv&Kl|ukx30_woBTd*LT*!FJx{b8i;E zzSebMv0($B1ut1Fy?i=b%TV+TAAl((w=TBU=n;m3f44HcaetI1Ne>?f$qZ_5)A&B68mzBSl6(xr zl=6dqDby~X5cIgO#aTpB&l2y}YTSd>xjLrgF$aTos9s$m{J3x;m@N^B1XDgQswNV4CK)wACj z=(jw7$DPNVD9K20fJE1SGrqbD$cK>s+c{@q<(RRNYE4-gEcB9CcLWtv8L}gRc4)0A zihmc2i3-KQSvyuO>mAP(8E5&wjGjtw8pr?#lo}Ql*1IGK3q2$ad_uH9c8A-Sg`5N2 z@u`WMpLz@9^THr%4A#gl?GQWuXIVewiKP@YLFa_{=Lr1=;M7^ELRL{Wb-m?cr8^ws z2ym7XwY5?14_I&2Fi0`wV8!Aon7DHHbXYw0o)D_h01w__hr#gG45Nx=D_SUaAsQh| z_=8x199ZN!cqr^%v_iw07W$qj3A4WWAwuMeAG?<>Ro0gTRqT7Ui~Rfj7)j|DXR$55 zfHVL6PCKVgwq%8u8GH~JYzAGu3YZQ$Nb!93PcCxwb>g}VAJ4lmh)GaSBcAJeq`GYk zrW9EXB(nFAstI9Zq&wqE3`;IkaIGUUd{do{Z%OaNY;t|_q-oFta~zNEqSZqk@(M|q z#;9}SM*}5KM+Fur`GA6|CdV1>X~(cotG~bA%hB9OfJmDssw8VM=%|vt3SyCyu&Lbc z1hgmWkgPXJ&PZ+OMfY64>}b;qBFprny1vKwT96Q*+ zzU04IlNifB3uKkVvwdXnBmKY0SNT6U0vA#@R^o`DqKX-L zj|h9Q6qBv|p0#aTX7g>CWD}{SDU=z>Ue~FG+yA&A1g4KXC|W`BLx`;)nPATz{^(~3 z52WyDNrd^t2^0Y>`S!Zbw&FblJPS*VG8~&Qc7xu0lbJ7NUpq|1xlaHg58-U%SP+0> z>e{jh<-la|RN5l4tiJa@ksZ{k5A_fSj&n1kv~jN}%&*5W+G5X?J3HXm=i@8)dYNh{ z;H(%1^-N8cL9~3b{sR*O8*H_c&}zNY0VWFbSq{t$EqEjk7W<&>a_qp{$Y6@uL&`{F z3T9J?>JG2V!GxhDfzD;!cGIi}+}&ZJ1}0?9VNuorNHo>f)$0~oz0ce?-ZJG-@; z@7V%TvuTW^z4IQmNX_1-k$(`sfO-j&KpG(jII4 zqR;zo?S^$V#f`S&i3S|f)<^%T=Q^6@k0c)q4GP2Qqr*b_8gbnqv9FEs;53Yaz92>s z7<(y_t!DY}R27uuSA?gh`jQaUD`H97U*R{ruXk_GcRAGLAOQyYih*ULszA+vpdo+{ z|Bez8p=imTk`G0O0+Ki-ii6#M6FJ}0WI!t|FN!4!0 z;vppKPZhRKn$n)4PyLjFZ1;Zv-(Pk<>LwJa22X~c zgEX-VgKpF&D!w-r=`)H%PxPaA3l=>y+^8COn3ZTvem5x^U;2m?;hRE9s()#k4$Z+U zFS9l%TEY!8q4KkUzcYylWBe15tiovm3p0(0%~6T9_`5A0RJT4;vcD%vz}))D;UMZe zjPE{kYjN>gR{)(IU9NNigQS=ER^Yh5ZI|D}xS!1ZL(}+D1_}HX*|_fDdxA`nfVX*HAZnB`sPuMO-)UV8lz^02T}6>?%x>#Y z{G1ru;}c_76dpc)AK_DG0dI_N(<8t82(I;b8*$CwkpA@}jhAPin=vpnObrc1n_XVE zBUZ^<3To5*rtX1%f%q*LBp_AB$)%m5-EG zWP5n8rl+SAgXP}(`Uy*<#~&L5Qq3K42)cIEl- z$#wYv7X;LFyx5wY{DVdJIf(IdbF*4dP>?oj_m0;GPoQ(6M80U>QIw9Tetv&15DZ1K zLaSNPJl#ldamr3kPB0ezU%!5Kb8}PH*=hDRGZO>x;g36=OG0Ae@Zex{?UoH(G?sN$ z#?s1;w5>|9FNr>TvoFpJYoVn9HdC8hR=r2*cl(>^#}6`(+pDbK`wUnhE^{T5JRWv~ z9~9iXQ^c5QLohHH%r7JqK}nB0OzZ@awY9Af6cijhIQY1?zYoThL(x##$hM}XrR|0O z_j;177T(^|%jC?#dPzsD-w(HeO0VUt8#%6&CaV*q z9`@s^(zu16jZHJYMeDI{D}zb9IGf!V)yA*)?kxd+n)6G)@+-BRJ??MQ=_D%tmd0z| zb=f;O^ei{rm^e5)6Ar@S6A}=bnndV<&iKDbKG*8JeEB{|Ehjg37K02h9XN;;+E$92 zqpGGBxYXR#^qd-bbMr;X{`Ny+#wBev~nisz+7;`T`#G8A!& z1lZv;jRrEBsi~il#=H{wo;xneQm>95)=BH1eCdMAlKQne#RpDi!$ z^d>Mc&_q{Pmt>=g6q%9nNPSc8tzM_x<<->}buF!`_5OaP&!PVIo5_zKDSfkTK)ASk z1d38se0(lt_VPOu(R9fB8Dw{!rgLHuK8jJrE!HV6(Pf80YLu8sNy&jrFM7FB{lD!Y zJx)O)?gF#fv$MDG!#P52kn+Fw`vrwbwKoEaWp7rDz70-oOn z_!Dtw#-*vij-a$?`XGid%xv}KBaa_-#_Z&SZ~l%X!w?Wy01*T@J!HFLNKjgaqPZPi zDVFMVN^xK@tyIJhy5{dzpFY>~PoOcDg~GNggtI0Y9bV6d+ipiOlxs}8@@FTr@Dhd% zSx<6M#90&V>9YdIM+578p)$O3O5x%b<69;*&ut&}z17HsQIkecmE<8zFwe|gP$jjY z84`v_Wn67YCW-4S;1-D;Snu#J&}2h*>%YDJczEeQy?BQvi_3-zl@nomsCgcT8vQcu zCB7eu=@Zgvz-7ROZ!TN>b7#ehpJ3~h`p6>x6Zi)3mR<|nyA|7Xp3!Q~jtRJ)gw;*7SR7N>w?O-wV zDeTD*bUA@dG0bDhr1LlJn(}-VqZVDZ z2%_XM9_^mbU8z^dsg_ikB+4=13dj?M5UsrnM76_E2cN z_lZj^D>8-S63z4bT1zsy->LW>f4%2EmTCO)3MpmwBOHbZ!)#aozC1{-U-b;#(<(zX zfKt=ya18IFnoWht^?#otOU(Z*=RNT?A#BGf!cWV?1 z5vJe|Sbxl=d(__TqiJMB8v&6#jVjWiZLv5oKKT+RDJ}iU*P^qQu3-H=Pz>Am$05`% z$d3e$8-wJc0H2XEGOSdghd%SlTQ6M88x+eNfh?A^sQi zT94AR{si$N2||Fyk^XOSW8U80)dqt=<*t~R*fbs zXYXl|fkhWK&{o}|;GQHnvRmGGWFSTgY4HzjI1wb$;T3VBx1t9`<5xh#pv26dKdduW zPukEPJTy9v_ZW?hjVHdO@;)}zTL}%rZ)GPBQ4=BJ7^HPh!AO`R4o=L}|Q2uoOMjTH=d~SgzH8Sv- zMe!%vBU1qZ0keWaNo;Rb5-ga^sS`6}b?oKI;|JE1mH+=qc1XecwBNvX84O!8uQq^8 zR&&NH&kMA6BNK~^jl~m?k#Q|4(ieDg6`cqwIObl69^0$F{rPAqf>!72tVjVbM^Ee* z(>%v`)T&QuX(`x;Uew3YaU^8RSN#7cIm{TqU9+Yf&1=(V^B2Xy1EoEW5GRBm=a|{y zOvSCO^TI~zm_$#O6UfaP4gQ6|NX% zn}`J0iWoga5NN<;eK|<@{^LhsP{H-4A}$mL;b(+c1DjN7sQThV)rSx7AibKQPqpyW z)YQ0*qomorbQl;IDp%lbF_bJhJ4s>TnuTwZRT%5DrfxAUl+JXaY>fJNkCYch=mFpc zXVK=1vXk`GQdg&1nR`z{j@E)Fh*bY8x_C0XDk>={I8@i#Iudx2cO5`Nr*k?IP6Ahf zS*yUdf0Dp`2k#Fnf!4;Kv$HYGw1zR265{A#AO8wI-QC%-*p%sjYX+fzCw0FR4F(GQy6+qvjO0cWA?y@B!PhOL{f*W@kDNPR+6I>(ChT%WWqPD?vKy3 z7@;@U*JAJ2fd)@U+NSdKquUe4e-A)_2&2vfl~6z*ds2*m&9HX+Bvsy!N-!W8mgnai zpjtdUJgnzmt~aIri5T`z!U{b}f&oQ&QYO&sZdV8CkzPP-6D8YRQ$AzXObELQ(kL#to zYbyCbf#w{J`T<8f(ZkzgNpbN{G6R-;o&f=Qkd!V?p+y70MQS)YR$T_rP-tjs-s`83 z1W4PrQc5#Bl%I}X83QSeJ$lB8e+h>3%a_?2S&}j`my1z!2Y^c#l-k|i=51+d`2&=- zu=4PXJGr{%KB!q)S*53G{1ljxfW`u76_roY2Q+ME=jIC7_m~9d97{12svOC5Zjklw z6n6<-C60XiPaokh$vYH-|JKhph9v#R%ag-KM@s3b?89MoR!>tR3^-;}&zMvFo5hyS%NaS-JZMB?#_@e6M~+ zr)h1B5@)Gjh3({3pD2tPjM&0aJhcIniiJ6ej0Wg^qT9fCvqn2 z1XJb&b!ThEnvYv^hBl5-WVXXU#GEi#kJ(ug9D>f3N5VLKB6Tj4O*VNPy^!|a?A#Ib zpp-hXzK-m4;P5H9bmsBAJTfQ~83bxQ3*zLF7sOAa-F2hYnWHG=rYd{1M zzA&&sonMN_(!Te##=GF^c?H-rb3akKR88cwmok|nFH{->sd}4;_xH5!Cl6<5a<{;F(>U)zI ztsf`S?KC>dAnqDi-jSo0CV4Z^#BrnXzz9l48-8C8I_VT(t2c=E@;mTosWXtDjz4oG zd0e(U4M`2LQd+P$>`W9;x?#>x8z+U_dW-oH_5HVR)9>Nigx6 zVV?=XvMrHuu)WYPOfQ(uGDQ4CS51-16iGj+l~ZkwhCAyUoVj)U^8} z%xOb|jt(#q-+o`|!kQDI;R&E_nH9{i;Bp2|?Ha+<{+Os*Zm9wR6}54lT(<$qsAZ!e z8Ufk}Ai3t5o0UgDb_1E;vqNLbq*qDWdHVvFf*!1UkqH;rF|J_Jho`{Md>AE{sZN=C}f zYF7Sipn9~iOGRP$`PTYy;bjS;gm)A;FQ<);e&~`hFN(3Hp^m1CwzOnYiWMQjcum@d zxmLm+Ykp7?+M{F}NgHihhM!vqHRs=)1mFhE$F7?q!FYxvfLR*AHJSQEgkg z$^gw92Q$76G}Dw0hrx^*jZ;Hd;>LBh_YQSTb^afw-aDS^@c;imIN^|W5|wputn5)X z$390Qlq7qEY_j(VB^<{{*+P`PWhQ%5*0J{{d!O@r_5Qp+pYQML&)j%j<8{5R=kt0z z?oU2#GTWCgU$XmwIjG;JMohd!684n%4-(OAxxG`oCq;Zce{apb!HLhYLDg%>JgZ_) za-gj(ti)-s!3Yy%Xl$%HRs)!<1Joild+OjB>@mO2x|wPl8y|lbWmWd0U*Tv^40+h5lm|CB;k~0{NR<_|+=YTYX zy&qETBBK-M<&HGQ%-^5n{^@m#@$DbCn>8#oPG9A7fQbFkj}oW7hNaGy9;5{2oP(Vm zdtVC&WT7ssHM-&OAKPKh>qGOgoEMf66O`F?tEWx)FUZiy=$WhLVq2&2OYUsQ^`m!# z5pe3)%8Eh@d=08RDv;#|V|zd+PeBJEWU5g6TH16ltqZRgCFwCy;rR4)s)a)*0#u4s z5>cn!c?u`6P<6#G9RKoFFqfL8KuR~ObQ!6GPC-*2|9^eNU2SE!>MW;%TW!u5t$qj8 z)Ymh#k5p^Rw@7NPz=Mk5%@Vekbn^Rig@JZsc{ZV7K(P?fNpaveM-O=JW2_(0E^ zlL!T&4q@tqTJ@DT|7D=%lHq5Y9JHU|f6>dAq{2TA4-ftJtQ$cIk1^UV-SPPmx&0k$ zogS46w#wRYz%!3zi zn17pETDBDy7k`G!$jZ9-t7O@sV6itw)`{u}8XFt)7@q_Ihs5Ym`=w5|c~&7aj&wZD zDFoDYS-POwbPPFVF_2HV7zvQ{QZznq`!NYHt07y}o*PnT=EHv)_`mB^ zE7$@KY3XzKlk_qMW~x4M5sUpU9od z&9VQ+iN>0qlfy7!+AwM|*oQYinyxe(rnKH8s{cA&MsU zkWErwd^61-+R`eD9y4cWbVy)gOvXOit55hS?DoG4#Q!|bTnZdGd8*w`O8NY`Z)ga; z0h~(J)YLcyOCNB*{Yghp&-1Wj3u$a(G8YX8BHJe#A6|ESYUBWp-9D{=5#V1B6UauT zoE#mYQ{3ine0(kvJBrJiDl&7-ima|YJw0{Wnn9?{dqQwCd;7kpAwVc$cg=F=jx)C4 zPD5oS?QJPL2ZsknMn+-89N~vR9{lUM?1Bo)nDlG*;lV-qU1nxY$pCu8aejXO)s+<$ ztrx&}#f8NJI-TZgW{lzOaCw{s@cA`>v?H0R|O#&n+W^;cZ><&w(DRCJzeCr0L}r`NB> zyaVZhOd;Wg3^UcF9OPnbe4OC6(xoUQBP~sG3^nFjS~#_n9lxFNvgw6=#!RpO%Xh;2 zN9TT+wg)Nw1rurNxoueN=e`L?N5^~AIHi9FkXyi(Xzt>o{b%bKrFjKNjjl97+b@_h znYd0}OIRVA7qP~u`P7ikPPK@Wm$`F$Um{K!`uObHB5Bye;Tj*|R~Of2p2Mrn#fm@* zKCb9eXZ7^*6K!{O_nJN*G1@sAp6TZ8eK)9}N5Y0QZNYhhe~zzutN0&!=jdoT&yhrm zX<}2TBh^d8usckZjb_~6)aiU+AVy~5+l*uE!D!IYT~>(Y8a*8yTwDLei#WlPY6JfL ztE;}(Nepl^p{SCkxin2RB`D(&@I}7!vDqpf0|vA8o&N4C2i%v!=E&AJsMgMmW)J#f zQ8j3TaY@&T>$fI-K6Rmt!8PF8rkx)1MBt+eH?8?Q)4U@k|mN$oQpqhY>0A z=$?S`SnvL^(_=~4`4Nz-g96rN)Zw99`QF*r?~CWYyW(X&xBJatX4t zzd@kUUHw+k40EP4@V*P?av|45aBYDBSKr%j-JO|XIt_ANyuY`!U&{+$I5`=^M6Wdx zQJ|cM0>w}h6B9vq>J^|8lAp@{Z))yfgpklKRnbqb_=AI1QCNn?gZQs(kYEHNsRUp} z;ee2~S_(imS$XX4>^R&(wGek``>c!F4F3E{u#+eUih1_2+-QpGuR2o`C@1u1<`_NJ z*w|QSfJ3wdh<~RmR6;U>7)NK<4hvjrBTuQ*dh|fo8yf|iR6<`_mX$0%p13sv@R|od z2Lg;5b~gV8^Xr^_prQtKfp(rUg3g!PPXGQzyY6=T^x_+Udw}q0ryzVXJWHpb%l`yO znV35|#_Y%>RIn`*qk@7o6rt<#G^mN0ncKh<---_#91Pr^nc8|bN=M=hW$B5S^&@?U z3r%Mu^PztKK69OnLz`GZ#X~fo`u%oRui$&JdPX+*HlgfO+R12*A5TucM3LTgk5rCT zJ92&kKK5)V{AC>%-|n>2=vcfni@hUcy7S=Fz|MH=^Wi0vTc0p~O>$bqB7p+9e1c$v z9(sOpL4$`M2d(6=#oT0rw7@eV^A(PO_K%LcF^9Tn*7lKN%Lqw<0Ro=$fwR1m$*bFKjb z>djyK-=2NHGLcN+B^d#fMa>pto+~_Z6$#JdtQm>g2cmut%mrSa>=bRD<)t|G%=#TZ zcHfag_&vdW->k3Z-~F*wtPJf}?~27I{}i(LC7bi;+8}@Px*}7~y)&J9^#v%-gvc zpg@D0Rl>~9v{pNtiLtB1=8_L1TAT4Z9A}@h|P|WCL>raJ2@SR|l zOt3x=Cd^W@#%907E(`|d)CmC1Dc~h&`|tf>7Og{Yz}aBwn?l~5-PLnM82Go(oFI?ezgMO1ifno2T;MngA(b~Kk}Nwv`|uJ+a3PHelXP2M&M{qReLL;SxaI@s0<9gCQ*0Ra zYEC9Hm1cqliv;Gz`L+E@jcKSd6t=IkJrC_rFMwC-hZ9hFFXsl>rR+iP z^6)`o94+W!q&y(KDgM&+XutW{cp}2y>P62ffmiLHTHZR<+vtWRcoeK)1; zQ}Efz?LL63-8}5SE8YiF>iD}kVnewEHLtlO6SN@H2pH9Z+Y(;Qg>eq@g)B`uHK&<4 zvq3-wONwI5jtU@urU}8<444+SPX|w*B^~(d_!IC2@G7xE`2H$oKlEM|!nF86&YX31 zOpebtHKE@&>qUw*pcn%_NB-c+5Y6MuF7{Z7JVVt!n6vP`H+T?^3E4WQ(y#__VtS?C zpUxRj6h9Vj4F_N#bQ?8K7|QKzrVdwVMWWR$%inqP9GyK0fT*MX@?>9JqpWI=PY+6My1wW71sw%q0B_ zbAr_bFasp0JNH`}ody<{C>MR{p7E)U|KFmiROL*B!^s7nGlO;jm9k~-BUs!PNyaNZ zlOJCD=EdahaMrp~S`=aP6@V3psM1$vj0z53){X-^$}V2>(!*YA10%|}{*216{(Q6f z>Y!H*1tdAMZ`X;}5YKzIh(0>K(K6F{9PoV1#S`=7+1xW*4or*HO$8n1U6su+UcHYO zjex!!O^QF2&$0cVXC?i&wLv7akcuG8(9qatq{bf=blATq{QqHup#onYXWkE4|8Z+AKnP2RzKb29(%*nd>yF?-^cZy)+!GXrF^PRSU2JN9tiyUd-v{P!{Lll zZ@B9Le`2}lfCT%T!+D?RU|$n};3zDbkZ#WlG-^vHCWerYaXsCBHsVLU)qF+BtiQe| zgj9?;@m|l0*cKBUQZ$|eC^+30)G4R3*GIp-o!=e~%FpHbpUcVmN5NQU;{Z2Yt~drp zmSI7&Lb^{WW&NcGMZ>`G-ki$>_%EwjPbTZK@%N_e{>R$G%`sp9-@`?gT1Bi>3`p_r zOv~0@Gd_Kf4L@NK zYvtclY*g<$-V0zaCIxW*7_j!4a^xe?r-O2re66B9aD_io=VcL?ev|{2tT49!Gyd-{ zDr;HfQOSQMBRpJF4prI=#{30LrLUNjy)2o89=OX;w~^WL-7FcZdv56Rw!j1h43hX0 z_idFjdU8Ys;Q8i5`AbC!n_2~8EI0fwcWNp^K(Pl_HBJINCrbGYZ3aeopc}~$v_Pz) zK*~>B!vJYCk(%X`Yr@>f5To2gx9f}J=tHj5(sBahr^#jx>XGP9ExB_`=Ebw@D1ma@ zSH|hamPb2F0l7bRdT0JYf)4l!4>OmsOurJ9>h>BA2ew!?*6JfB6B?}T8O4kVc!1pm{-0$eM32j~^*$I%=B1c}wb zi`5h-A0R92v&qBo?!wqLTdj{c?(@ag1N`#$lBS;Dl*}^8?r2~&{ojOz!6)wQ|IyXz z*Ob3L+6L6c5=l(a5ftXcR7CVoRsxA>JNfyHx@THJ!}qU$YsvT12^iYIx=ErpHf(iI zdHezFQ;QNMrrK%F@e3l9g8bDeZ0zj9B=9gv3x|QF+)Fml!{;P<7qAH-*dS}EZknzNO9#sVE!I>bizg^T z%UE+x1*7kxdv079)9{uW8!e{GreuD?k*Eq9#9x5H0A{?D&m23uTqLvNCl}|~n|=1& z=ouU2pLm@ui{h-&%}xROxq)TCj%u9n6(ZI8E#~;pU&P*$Sf)w=ZVI|93C5#@Rk~?jmjj5JF#+{3l^LGoofe}a>ib{HN zx|ltZ=cm%^h6Q0@kRId8^!l$xgVM<69nk?02$o&F2^S zi-Ol>f%VeB04XHUeB2~>9D(>8471$9R&iiJLT;kqj!}0u$nhRYnQqfvQaXne!~20w zbAnM#0UN_=EGo|LqqMd*O9rpFhUqf=4p3vtfE)Bn8cD(4ACv6B9bi>>ei;H94H{gm ziXeb3O=Mb7zv+w4j#cPu?NWek)SmS@0;1}{2SPa?5R9I|i*IBeCH~~*>753wvc?Z0 zA2cyLzo>IvDMN#$Yl(cG?W%@u)@bAO=lBe*{lzTi@kf_?&06qa!4tmk*`K2KYX;9y ziU#_LfB$I_IY!*G(=r zOhVxrkq6xtMvTcP06He6di&TrFDc+^zjL-%_~Pno1IZnVG%w6w;KRMbbUA4agpaO0 zJj74eC_w%<&52`OD9j;k{`>9pd~fSUPiKAi9yj%;_ZoEXe9PpkeHN;}v_)Y)D38Aq zjsp|@1$5@KV`;f4T%m9&bNf@dc?@3>!$W)If7nScwCVT_!r&k3{X0~ko7j;On5ov;HLRDJyn)w&UZ&UJdz;sl>gTG_dSp1iT;=+jc)XI}hJSMHY zalm6V+JiCE(Y4A3Ems55dw)hv=FY`?KeO>2FFVp++sR*Vb)%q3kFURI#`2n;0sCUZ zRlD2$(Wi`fL5hyGLB-DC@sxuf0Q#n0CdK5F<}+puq8KyLqMoa*4;tRAG={?F?4?8T z@8Ix9!ht$wPtruMXBBG^px88GVceGihw0kk!EbNfA|HJ`f`1@rdK?s7OAIQxW%_B( zPT`)Bla!%l5?KMSd?qBnh6Cb$PUNFLcuXnL+4+fE{I3e>^P8d!6*JL)xJrkNE}Sxa zFhhYjNDGf8m)Xjw>e~wkb!cVmk5|s+gGxH?gneUG%_6LP?bV9l9ylv14ld>`ufq&5 z2ngk!oy;5eE-xPgDqdx$vAjIoMW1}Iu3>NMOhmo*QHjO6iIxQBZwY>vArI$fXw6#O zaG=h+9JO|KQeZen(p<-Cde9gLPNIx9OeM}KX}Z|VL4)0O`WWm&r6lMuLFWdMbchFU zw&7+2sgg(na%#k4@_WLOF^-lujW%q2veDE0?_B{X&ONw(BxpE`eC_5zj+sZfM=#4<0Gat|{ckx)Ymdp;HO@-F=VhRSA@RNIAex2sMDOql8($#}~$iefLtsGQj$NX%*M%8z24Prtmvm9o+%Dm#$L1n;wm4)Yg{2roE- zutTiqKLa*|yDbeZei!dy3|l8F!EI*NJ!oFZt zEbwA%8@kJF9%{vp1`np(1&i`-Du32&=Zo?^d;FF;A=Z30O;jn{etosNA&7BZ6dysxo^EmJE_SJ8Ha8K0uGFagA`^CggbRxVPqdUMAt2 zQ8m^$xwh-pzef_~yZger1n;}IcUlwBJXe0}k*LSjnTz1hSsc+ac5kvw6f@+Q5dbo| zXiu6wY^&%de}E)JTTM$i2#^Q+0JOuwgCgq}DzB0=$WY0d*In`DRV>NEgB_(4-UOQ~ zTcK5^G4;q0?+0AughCr%-G@I19y18qX^}oX^%X?f6jAkv1Wip+=We_UAasqNZf0A_ zpPNo$!QD-@LRnmKI>^(UuLJNthFj`#CTreJoG5)76t_Y>!zg}1!!pi3)SilEu9N0$ zQAqF)32DkxO%++JmxH$PpRbMB8-7GHO>@Sk2=5}Mq7yY&UD}mIo@`RD{WBBj;3P%G zj0g5b;8F#@CKWgS`(U-$<9NJncmkJMUt+aj@5_gDkVsK};7;LENroi2zmX2OO>v3! z3ItJH>SkZpO^iKBe(#mh52tk`g;2O_cHk1766%H-;lYQb{BPhd6WQSek?k$EOtyc7 zC4+8v5#tC$7Drx-q{2b)q)oVl=jc3UOSYm@H0e#+dg67+fD?UjCAcc z&6!Yy)btBt;|AEB!S?Ea)~7a_nE4s|H8w6bRO>7zO#W)Wqg)IKeNNk0Fknux1@|U@ zS

OqVHzezm{(}=N8mF)BCfQcPO2w#E+R5U$C!CqmLl=uB|w)lvV#lDbZU}`DF~J zz!2nT*{xTeMm6q<0l#`0_mxHL3M;M%m59BVe(lTeWX}h^X|0Yym+N2 zdX#l{zG@BzF;janG2!bnoPXK(HK;CT&aDqRQZ^Q2aQU%Hh4cZ9DjOI}iW&;Xz!Tac z)2x%BH&AyxU5l$4lWKrRq5k(Mn18K21KH{%fBw6?azGB!=jKP%aA~|aL~Ngi9DX>IFg zVn$F5$=1Ye=Xt8o`wk_m|2rc9Bot`d?3gFgf@WzbLQ%TrkDyneiM=3u*d4Dm#MZif z`i8j*QB9P4IE8F>rePeLS6I8339qhykQ3+)Yi;tTP$NyY{Uu+-za_zPlwnbI z5N0mzx=b3M6=?%E0PDcaL*}@@z#zkPaiqxv5Gqcs$SS}+y3rh|N`!f03(Ul%J{&fX z0B7a+*R15zYNyfeF^G2e{i@p4g7IRWw62`w*3?J0I87NJ7--C9QZ>#x|pyk z7(|hbC=+Ch2{RgqoiR{g&ZApa3L>5#HB0gE)Jl~QwqFNjeB*Z={E@Zb$3dT(`*o5)=*&)8>@X;}go6p|;RD4N&?3dPG3PsP$S&^dM;Y{um(BDlHP+-256 z1LWTkJlQbp=K!*@=@~iBkPBijR3GUl&m>l)iPys0qIeA;sKrU_dqH1ZUvWDLRqK9Y zm}&BVnexerQgn(-r}JH-=9D}Da*C(RD{10|uvff%RjOfe9!k+eZyQ@6psT;s_NHhk zNc2+7Lqj8aWxmZqnolt#g*=E+8v(tyrKJC4=iTqJcS6OR=J%!BuX(R(hGuu^m18F; zUKeKYbjpYAWi$bvQeJIGbxfGXClM=y*t9UA8q%PN6oAFJC+)ykdZXtC2X%#}lGCWjgsR%t8c~->9eGlk|Dq*EN z9xBjn>RNhZ@0Ht4h8|HtM-$O7#5Rx)xyg7b3o}ZhVq_=An%)eWwxQDHZsO}pC~S;i z3GhNdQ;EWm$)TOhz8bam@GNWpvsu4dI<(s2AIZ_{UaFSQl$fEqfILQgyWP1Oyyr0r zg9c_=!%h*XTJSYzPs{`?vI;|VB-1f;5&4k}l(Km~L)h#cBPi$H#aC4~GanlhE2

%l}G%p_Rk=T)CNH2E$;0k->yG(XR5kGPyx0?^;wj| zq@}4n#K6Tv`0ia3X(-!;ED&Cj#>^cTX1wbNa;>`^-dZR zDYXFKnpMK7RXMTI7Df2yNdWgb_OBm75$JADC1`3j<@#t}bO+*z*5$S%X@$n6eP_!a zM^;=YytLhT=mI;L>>seo1zFIy`x^SoHMMc6-q?-4)e^-3>6bkeBWxi23zC-%#5FXy z;v|`46Zft%+TGiq+903+|E%+$lS~2XGp1HIMbO6^XzqgedctGEki5nEz35o<=NVNP zD#KU!{}vo}4bF;~Ug`a4D`o4SM#@~>znNR~#sd{+<7@}3y!0{M+McZNQ~^{=ZJ5w9I;lyx!(b)Nz4P&Lh4&02*5rx|*I*hg7r^I41_9{Z1yW`?WU0ripZR zlEN&+Oh4Q~1d*YB5S3wAI`vQ;* z9VCUCfp7Iv98dzIgH!@K_ime^tB9BxIu1Vg2j?*w)jEGe*A-`0zmf=9-MM2xp6z9qt%n#yxGTNQ!uIgyLQBqh+lU6 z_o7I=^I7&q@GTIDFpTM%gfzG=Ek4ZS^61?;@lY4*Zvg_er<7R)O;vNYM;(6w8Wp3v zVP0b{YPAcCZv31GE0=GgKvaCN#ADd+3$}4J+x-9k{OV$> zL_8hHfFVRQLVZfCKQBCW9oDsZ6w4yd46FWv2i2VrWlO^$J0}|?e{)UjH{N>t0Vx2Q zBp3vd?Xpx^#|Pdlv*-k2`CAO*?yi1SgmT)*ALQ8YsJ-f|5a#nR4)Qs_Fy#lJ?&#OX z{oNs;_6u91%2ku=j$Z67!o(%l{~WOM@!jk#0cRRO-D@J7K>R!#7s>V9-ucnpr#~ z9w!E9aP_P#n_lzUUtEGspg{ElT28I5e!~MGwZls50df=3*`>hz)e^+H@$T@Ldab2- zE_S)2vfDFNptn-K&^dGgNkA!&MzmFRfTw|=LkPbvIMn0Y+P#Od#@H?5Bm2e?uEF}D44yjs<5t+gEP#zmCrp*tes{N1 z3Im1-wAvO|RZe9@Ib4So{7!}cyoBg=z5CCp6OTV%EngP*{XxDzq(n8moG?eA&wP_j zf1^W$p&`?e4ap;%-5*FN+qRcH&cekD{(OPdpcDUro7lA}A8D z#l#xD`<_TD#o9R(;YfF(@=J-MMDL2iPabJ5P8=xYq%aDxn>N}a;8&D8gG>E;O#4bH zL0yuX2L(OBz^AXK=00+q+o?js^WZ=R4DwaZC86C`02P7++mnCN{xC|fP1zmFa)aq}_5dKU&89kVAcpWM? zg)?l3@h_}?J4p&Fj@=fnsXAh$nsn^gNUQAZ0y{JbbN4LyeHEzZD|V{+BD?GIBiG|y z^S~z!W%3*q@0|+^5+pOl;2o4rRmImrTpa`FK!JTiZ+Vb2<(o~{i;eOJqWNEj^9)#e zTxi{9G)KzaUw3xndpwN11-S#uj8IU(Ee13UyiXHK3_>4b@HJHW1Yx0Y=dJ@;Yp(Hs z*J_~`5~yyX1Ns9Hk2mAYV*S^QfX|^%E0ttk1#)B%IAr$Xv1~V)=XU}>`>mire!2d= z2h=nzn(0ij!_`EtO>3#Efs`fyIU#>f;^TSD;q9H1OqNaEYP*`wSx@1n)lQkG*kRG# zmL@5tp$dEcKbs%djvlY5U8kPXAr%L`s(Lmv>K~$>Bz4^>ez!%F9QQy}Pp#;2m0Tp{ ztrg^M8OPS2+7~R8(Dz$3V&kkV>^uJ(L%7C%VgRBR#z-Ow6=;(~7#yUUeLs>#^EZl| zq80`b``!{Oll3>K9|~8)a2bTojnon)`omd4EEKgyq?~ebYe#C>3&KAIL|r4h2A8kB zD?8+VBc^U-#(5m!vhPxX1Xe45{COP82TmXI>k-$qPx<1&CKpM}s+9pkUW+ufa6T!~ zTonbaVm#i&_)_1ck-FM5XoF)so^N_m%-wd|tr)`exIL~@_38L-q=%nAMuQ&?dJvcw z##Oz2pj%=w0Zdw<1*g$i@t_CohtA9a^XV|gBgtJ77o19hOY#WD16aAJf9*Uk?*9Tt zkW{!W5}JJ8hDx0pCjv-gL(o^sAdyn!t(~x;w^9T=%HU+8ysNwvc*D`iqqwh+#R^+~ zlb)ID-NHY|KJQ)9=bEh;dL#B@^Bz+tKmyR=7UyI&^Lew_2H7wB;)n3BcW5ab#C+MK zNgraKV&XXf9b4_JGkMNegFh+`C%QRk+8tjqjthGO2IkZ`ku08ZBrt=$zzi~DTB?18 z#yCu!#%UZjH$zJUiB|y(^X80C3IIH~nStBAF`_4aMWShOnIet9L5-ypC*NxgEdJ!G^8)o$t|Z~GqWS-YvTb#$q-?@G_gEq3T$i&gf>HvaJaHsPzg5-9 zp2%x}h)rqKieu4WPG$}i_fHzc?L3x8Ezhq^Y)vY5`~)kNJ|XbH-APlQAVGmke)JyO z!|IPgp*A*SYFJKYDGJZ4rqU%6XM)oI3{B=&#+L{Hlj)BRQ@<7iDwr)#Js>de{Lj+< zH!$~5`O)r>iTce*SFAtv&V5ad9XLdeXi5it6DNJ_(XR#FCT0s;Y>Rzo9e(*ne6cSi zvT-h{d&@H~uy_chLwdMsm)sn$AWX_|9M zxt03@2lHG%@Sev<9m^2`37wJvH2uxo-07vv>LXU{_GLIVItA|Fk>y)*(Ip)zA}_k;vo4Hq|s9I(e^F; z4|aUYV_+&ZwsD=rJ5?)@HBHW6%0sn!r%Q#`mf-n(gBS#p+|l)NEGF%PbP>0%;F96z zYcMMR4~w1ol)^{7dcy7ROQQnc19x}B;ccI7$7xoMj##r_o;zlxVx`>6^V5WtfBR25 zj$grl-X+}ae%730O+^6d<0ri(Qct02$BZTiH)uFD?1$H#q}mv30hmck{#yFuIZ^bS zdOa?yV-%Z(I(+#m+XB1V!>Ag73Bz91ScUIXpfE!I_}+6Zj8IACs`Xr47}gtN_ZVu^ zb!AMr8T_VM2?}zbkNW+MKD&z#NKDG0MY&TB3)khgO93+RqSc*Yt5nU6w_RbsoDxjX zVUfIe;7lQE=fc>~z`t`1@Hb0Uwatk$i$|Ian2SmyBw9$?_@nGfZeo|A66$6A-x`@( zo*@xCLQO61=sXVKojN7`_093KiJ63;VeLFE76wVYuy`!QIwHU90G>Gg@Vx%tZm*m* z!m<^@g0Lv;eek95HIuexJr#C~*@YDSU?8XEPUTnuQyDC=qiN=JCO(YiYJTov({T~i zLr-N~wL-x0_tbNtlxkelNrmH=1$@ex>E;v^6$Ckf!cott$5u3&sq_@q) z?*&+7+Zq;W2Uvv2R;~tqJ659h`1}fpza_)xYcA$KXku9;Ddu>4NqYQxZH5u&A>HMf%=Lt1 z;zv!go=EiOCp^zsEP8}iq;J2F3O>y!DN{Cz@3^WN*Q)p5IbLGw7vBK{QVeZw3f>+v zTxf%9-)BwMw*v_WdEe6=wk6bw%CB1QpcH|aSfogMlMC{^WOm|>&(-u=KmF>QxQTi5 z+}Va!V2whgQYj^)M5znF+MNkX(CNK}LvHV$qT!@mQGGs=f>n1<%fHezxGZ(3@)%#x z-hYrqOK?WuIpWsnbCj|=yi4;}6;OSS{+Oi<*_UzOq;+1bU{aL!m5U{WIM7ZCE$#$T-aB)3yYe6t{X?d; zskGG+RW~gUA-rxOOF+o&h~3wChQm2y`JI!haVkvaUaq;qCy#^w^jl93iufslF1||6 z_-|-RhWWb?5jgXwC1Ce3FMQ`@%qigL%XcvoGrAR(E)8>f*xSiJh!ir7Jqpx1y`Zsy zje{hB9P!iA)rxvXaM#RL4|#Y2psT<0Qbt!!sVBGtWt3(wY+Y>cHwNt(j(U{s@ZJCZ zso4iZy(%E~#rP=BrYSnG^CBw|+)9k_BY_iu?g}=`;wnG)z3#soU1Dd^`MP~c8h<@b zM?)Fsrbk37(O|E9aURO?y8_Od@n5KVTYr4q=|Jj_YIEVw) z7Z7dq#Gd~*OXK+n8gSk_=NT8qg8RE^%Joz4TmV7lTzUd0Xd#{l-Jfry1x1()iY%~% zDkpL>?ri;r@0ti%AL!H3C*v+Do!qZPJ%1TgHr!XQN#r-golysIJq|Bgs=K;+N6_k!?` zUoJE|(gf`V;!Ql&p`;E^`niI4iaw4zBFHZ1Njav_de;v!p_+-eGs3jp;3U)D+Oec9 zB&pAPij4>Na^8?yi!ue}x-`<4ICu=8k>PXBuw(DI^)P>r1<&CWmavXHyE;Kk9t#$E zgtrODjOF{Hk3OM+)W+L7ZFm2wUZ-gJp=N!7luL=wS2vcVe_zwbbbAngKEF*992J;^ zOFC>WKmIkn4pcp`cu|BKUu%|aN<29(VYy!Yu1p%p_1UdHz1~3n`ncrB)jOnOpVt2* z5V1U{v*QxH9r+dhtP|g~f0z+iyT9Xve@hxP_tSDgYG>P zY<+(;E-#btPS5GcSy@n>U`)%t?^72&u#5T;53fb z=fR?Q#{=8I9cO36bXDHe#$l>-|6q0W52U!6KuekSd<2lk5K;psG}ZJRL;AyLBHf&Q*0$xf8rK~kMhDeJ%gd-s~1HHZ(8)^b92j{OwBZyBtB8l%rM%&#M% zuMEMfPnrYB{etgQ{^!f`Ka*URuJTtTTo4!9STX*Xoh;jVr_<$jGnfKeMIMHD%3}lN zQ&H3o;O1t_;by%}qsp zl|d#Mm&#MeIz!Bl%E!GKw@BU(iZ;$V)RC~5-v_lfW7R& z>f%Ex!vC;xiAwLXyl+tYqNJ&p%-fY&(R?*{x|ZRRiR-M*=Lyak_M?dqjXmdIzx>$f z{3)J@6nq#_(TVGLK{9aBIUyhPhfZ@lf1I^k%LfMk#n4=Xo4vX?UE5^PN1 zW~xre&mJG*u1Mi#4*%2t!pK*zC15g{k&8^+`Qm4DN--B1Nw-PM4QLLc1@ z&qdy1B@IC{u|d@Txx>}P|Kl!+3nKw!+|O%(A58lE?!T26*#5b}lUPuhEj3T?JMc|^ z88&D%t|>%x#4oP5QD5+ya@$BmN(ThuLctbg$Uy&B6?dUIT~7|`vx2U>g7oB<lx!stBTa%qOpPC0X(TY_nF_H6o(VE(f-KNiaaku|xc3jxLS6_1+v9aBK z{eq`_w}jmo9hF2JaB=}WuFPLkQ zinN#(`r!&S_dCW%#Jp=)Ta6hMfwL3w6{5aA`%;5;Yd()Vj<-jpeQ|kCf|p7Re)z;* ze@~LRZ9(6)MTSwAxBK$nz>GqaR3D$f+7jBRZ3rP~bLaeiQAn_<;)meBq^o8cAO`7` z#EF=94)#Dki)e*MJ+!J`~3 zmy-q*6QVF`9vINX68}9I!EiiU*PWyJaQpV{+2QQ-^KbEkD*fMsIzW$w)Ybd#dLf+5}a4|QO z8w<~5(bJDyLYRQMSjo^}D?exRJIDJfgDc4zJ#33r(Wjn3O`BJfms{hhKfGief>`nAsMXOM?ZI>M6E7@I{L_nX(_C7O z6q`^msCGGPtw|2Xi0wHQRU5C>spP(zF3AwD;-6VBtSA4wQ5K1lM^ zg(+Sra4YF3v;M{{U!8LRJN62|u7h4uC79GY6R^S0-v`iAf18Wd+z%x|UIR+jLNbsa zDeg;^$?xWMz)(W}SFJ^YFD;0_MK}MVswhX>unfvXDMHVx)1^HJV6`&) zGA-8cF#|Xn0?RM#y&=WJcb6mqeKQ%st|;I?1mCx;B1P}Mj0Uvns9 zlWnV?kKdJvJ76n8C<*@yG35|BQxh7;P(^6M{?EN5l2gKER+j|Zt!pb5kc9zKv1{K# z7e9P@;PAggjf<6Uf3$3U1LftpBv7&BTyaI=)%iN+t>0;!$6S?fj7Rc=m*1RgATrjz zk9C*R{qwRnk@M%5a+g?p*@^WR<5X!^-xKOCZG2k@n;TD}l2^-+4Ke{KhJP{V$89`+XlmH&aL#tI1<^VDms(!_22J(p_(R_YDQ<_u z70J@A5mO`~jB~!1GC6_~cH_p4ydOWXHNg*Gvn}7%7uDr}$ni?dhpo*4x1&555NLgK zQ(dYVkX3n7BUJf#J=m_fVNV-P5R@&v9G>h(`1OwnHMvIugRLqm1tx}bcDv24EAP=@ zEH3{z)f(W@F_4>Q1&XLcoka+#>OV4nuA32LsBFTHR=UISiB&B;Khx!IiTqC?5g( zWCiD1fxfe{9DL>w{m#w~LiHDQUcbcZne`T_QK=$InuB!L`W9(dMz1j_q82kG|aKdcs}kvB?tMl^o1zH*UEnS zQVo}pfBgs4!?%D!N1#xw zxqs5AzK)g_kjwKc`%>6cXm8mRD53?mwBYAuve#FQ1&)QwHAA}sqymrr(EN0b^}R>v zb)$voEDos9`zZY&fQCoh$8h03Eet{m4!&K2!v(NHSUVz|szRM0gEjm>$dnTxlOZ)< z+*$L8L7on%)ogg-MbAX$3129yXRzW&%}epk={Im`dJi|qT)OY=S*yjo55lXYzx8u( zcPzoJ_{y!wok%J3tx(L)IW;z>%NV*Yf12(kBT7m9(vu+OJIfX?{)%y&d*#N|ajO$~ z{}fAr{rjZGPJhr=vXw3uDHxuYmm8IcL4L9re$*Q{9Ui8HIZbVBWZDW*O3)sWo6YQ0`Sjopt|1RE#Jd! z{JUpC1Q_1u#R<5$(?=u)2LfeMKc&fp*$9?}*|HdN@o(YtuXEzShND<4_9h#gwe1W+ zOibJdfWR9rfMV94I$?{BN7tuwzPoXNI|6%FmKoSwT6ehsdGv1un?}H|ikx7^JqDOk z=M7(sxV724^M3LhG-!jp(HgI3cZ(%z`%P_QsY9riv9g_-zF+D1y{(DHRSjLS%byPC z4DQxwjD+_X?3&#Y!9VXIua2@iM=Odp z=FTjLhmWg_EL5jQbf>k7war9B3H%;PnWr7`@2SOsIkBK89~M%myfogy=Q9SKJ_;C# zAVZ>~^(l3`=>dn-P1qy8xNH^`P;a?{u5vSrC%fjWcdQ1Nx39lnjBb*wzZ0O(a18jh zqk+Aqmg#==Oz&a#O!N?!DZhK!oV*mO)Fcqx(ifLTsuyt4^%V%}5^)OS+rMA~q3}0^ zcb;ElJXFy4^S?nuiUwzpqDV#Mawq{aW{~xCioSp8HI590m{1=47A+D$T!iN~3#2(M zZ@ukwCGln#sptw{P~6+`;vq*VQa2FQzIY6306x%?gXRt&D{a~@(~o^Gc-hmCJLpr3IjVlby%*L~wl&7_w+d zr73J?!T!}(ISvehm@2wKT9|^?OgAW29QX4zQYC265pVCn?s;0U$2UZ#Qz5c<&NhjR zOW$80O0rqz)FE=i`i8bFnH+uB`Yyx0fGdPM!-L2fMr?5T;Cky~bW1J8c@88tvPLcY zFuR=fX^Z$VAg2lX`l~-hymPwt!!g|>5r!AHQP1%<@Sp1cY9>%ccB*AGt-`sFI0k<% zQaFeE#Sh{V(6B^bp@18j=H~Ij#}vbOd$FYG-m7qY01}fKO*PpSW5oj0u`oIdM+n(B zGy~@@%il8JZ==CT=u&JVk;BzZ1H3lj{?h+f*IP!#5p-?4$lyK@APGSScL@%IGq@xW z+%-7CU4y%Y;1EJ^ch?|6gS)%Cb2`uSe&2c5I_q@(nVz1RuG%G2)wTD1anag5@&*AF z0XUFfZKa(};7fw*NN;txx1^R>S=e!Sn2h0-!XbYc^$ex9qq)_xyqWLN2H#@J_`#j( ztn5iQe5k~s63xVl&#qAzz(^qnH7E>hqO1I}J8+ROv>@{z>=UE$)OiJ$*T7~k7Ov58 zdSXV|Tc08W{SJXcJ?lk6r3ULLf9q&`0dV%f9N4R=kP1#N8m_kD3~z`MF6iD^trvZ- z+KJ&FuhI1+Qxgcy6A{q~>{^bo>RW95!Y9;QoeY?m5VyEif2zGqztyJ(@l>+;G=JyY z@7!EU)QDJ+2&ISdU$Yh}WdQYqm3;+QO}V#E77WoSgl>kJfAHOW@PpAIJZPJ z_7}!RRNeb@50QoItx0gmxrT1#vG$QlXAkz7Wz1g6UQ>36df9;b2z6Ex0n726}1+J7tLf<+@z?x5_(w zUT4&L((DW{|BegDL;KT^$0!RnYB6k z2CPcj-Y7EKXh_3myh6N4SC>EQ9<=NwC2Bhw_}(f&gQZnW2VTGeO)ocZ~ai{j-$ivz(ju$gCXtwTF;fG!m6Tl|r2%l?rj?*?J1;MQs15JxwKW zdj5#abU$nR&dbL3=9MC3*@^PwCu6Gj4SkGxeX^D&Z__#M-aKea*KP9z4FPZ zAMRg~k?l_~vDxeVsl-MebKUV^nmIR-Ur1PY&yoU7BET%btjmW% zCSbYkbovNgC9j$`hdlPX%6_j{#z?90mFNQ2;2xBv01%$hY=kJVL0ZavHVm^w3R{it*!muOc z5U#HM*`jYDxL`c(M(ml`U%#5xjCUXqN1-OblQgCOF;3;0*Ne!t3hw*il_oQ0XW zIhh5z6*;+NCU!s}h9=oQ;I)m{>8gJvB$3+YTry|sibx7d`Ig5PG1=jm-L94RxzZSF_ zh6N)M#)N2OXM&SAczh1)pz+LB*nDtsFvSY1rYNMJvWY5}y9rZb(kwWb7v~bmk0cjP zM!65=_lPQ4SX;FHA4by*sPFRNL$l>ynriDgj%6a881hwIiE;g0Ao_YWUXB}vfF_4V z)(zykVG8u0o~hA62WTb^Mw0M>t>_YPJNn+pbad4LB)vqKn6B=-1eAmyJbf|m1o|K$ zNOJoqxCZN6LaVRk#U7(-fVJY{qK+Q|qup}Qdw@p=6WdJ!9h;xGxg5Po_MwrZu`cyi z^)WW4QkO3Yk}vXW6d9u#KiUX$@Yh3th>mBKWdUneV}`=V=xA)90}%T$uRs;;yWca& zzi7XP0{;NLIHcsgw+3o{!j!ie(?0nxS7&)MN@UR3Aj9sjsX!Bd4N9TSM7fn$nV5r8 z`dK@fXpX(-Hx?`q0bia_b@7;um^r-x-y-D%@7zwoPwVf1+D_3CjNU;Vs_PvGs8s1)AT~!|LIqkv3 zfYC~ZfDhQT!H?1CtBBO1L`&@C1aykv=#Q~(Jvfi8tgP~VCSQqu(~doh)^ zVa0FK0-{wlo7FuI%qLop*L$7Eyk6wVo12^8uCK3aVnMpTYXF0!3^;yVSbhF%k8&o0 z953;*Kn(RG@%zMZEG7F=ydhnlCG10vRfJy?Z6aR(^cz{kU_X0aI}7?9{<$e`YN8(t;8LRIIQ9fduVwzikR z44gFUZQp@H4!TBI!}d>LU4IjSfF#7f&P}0^MI?jnYgm9HF5SiEK*A+Fe(X_Qg99&U zF$$OINPZGE`Q0L`bzD$Oiy%!GpyJ!mY*1(d==7VGwY2E$|L$w!z3OJ@?Rf*YE)xqX z(R0Wwug5uXvb3c4=v!wzCJ+)5qWQWS-&H*!3g&vsH&#OE!}2PF7mwr=NpH}mf3h=u zgwy%AZUgG_hibm!jTdY5xQE5b)@7@Hpa5kF>+^KOPVjvzl9L%Ip zsr|Q)yPsF`-=gB;zoOs%g} zu#Hd6%+Sh#i9-^DYtcXP>vshdBoN0y*yip_vJ97^E_V)&x~09Qiqsm6*c`(1O91&) z3A8l)t)N)0c+h+beLOjN^mE5V*i=0LYWYv!@hcr19Q+6in0RUOxdH|qlz3%z^=-y4 z(b*#stCSJtA_U|WP2xWk(x(za3 zJns1eAZctsqwsxms=TmpKoA+vmFg73vmJ;O=X&Zbeo2r7m#wstu{tPdeWCyadlAw+ zcTbs+%rPCgb8hz|kZ@LnBDSh2cE>r~@PZ;w&yCSCL`ZqNg&^fYUDHt@Cd%jgg<__f4`}`$WQ7l_IF#hK`(sm zhGVepJJ|=&C7>SuoXhke{QSn z%ff4D!&?UqIn43-^2_!j{d}LCKAfZE8^X?{pd_rtD5hw#ho`&*(9jhTJlhwOf^+W= zG6+wBWpg2&Bur=-e#42+1q!%?`ud_E1V|^X7`Q7Er%>F%fxQo9F|A^G!N(T}HnGk% zpOONI;`dNZ$l8COVHKo7Ieb zYurUYMsFe#)ig2g2*f2q(mh+3JV%N2F`!$PZ{H(LkY1K6@uy6f;naP~Yie$rQWKgN zPqlKNUML!7J#T1e&?reuV475Dzg-eB?af}qS-xmDPkMDurb`pa4r80se4MiBc#8(= zB64F}`*`1CQ7r4@qNE{WHh^x5GJE>4wPpG!tUWE;#>`hTq^S85gytOEL1|(*4((%m zIWi^pPl{D4V(*FPJvE%3mLqKDI}wnfUgY~jWpci|+wXEuLM zB_M@c@E<2&>+RsE?v)Y-q$Kxo8e|puUQs_nX+rP3aMaEwcJ*B|YOjoZKxC4u)Cz{)`i4!R+SCBm&d$zK)xqj&Hq{P6W}2Rk@*nX*UjR8#q+jf< zj(2PEloW(#O^$C(n6@0CO)`Xpeuhn`Sfww!UU@ix!4x@zpa^(M7Z zo0M!4=9#P992ycU!b}ndIc}b~Z{;QOjdu!&Cf!(hSvhJP>=bfr{hmBtrIaJwc(2c- zXX4jl^YMuolj#@JEI!d(LCsb{|A#gdTfynL^``do1VE3LHIs3B>Xq&d3gq!}`-DEe z?f4tW;^UkAFa$}w_m-FhY-An|F}LaB15fVv%OQ(iOw`fC`zshogkd`7d)wH5Q5YoO zNIHYSn|pk_mA^u~w)EG;b1>>j{X!fIY?%!69_bS54&iVHE6tPrgS0YB>pq_`ii)LX zJv$5rd;Z8IOgaOUo80fCx{4zQFFB!ZJMS>Qv zBG|=poKhhC!bYSTf270hm`Am=;SD(NB)$7?BsF6*5T5vYA6kF2@?RcrlsCHyKNl@L zoVwp!qbN1kFZ-UedQUX2JnYKtZSvCp_pnUZH4F?Qf?ylEN`M#a{>Av}% z5{0HRTh+&RsCuRj8Svn)sL&OitUeS+Ot3~BeXlU(h7az?QZK(QOyN4hC*hRadiR)> z+?PA)uSR+U)zj*O(2x~oQL%wEYvGr*7;K?tx4+(J`}M~cDeW#<-ZxDTmkU|V1+2bj zXup040J_V+gWPbKe9cg$u!hD)RlC;x#XOcghIZw# zdt~a0>lJ9+SF)Y{DVI4Qo7_Lwpaj)lik&W2_6=SQ!$c@^ZtbtjKn+W4OdA_{QGE!E z8d-mmmijq%d@jVh@yJ3%TW)&|;@NyNayZv$IWo6&%~{6?M|t8Kxp~i0LvjMj$RRDe z4SY44wQvVdn6@$FNd2dlL0TE4Bf7*X#py#lTJM<}-3cv!st!!1zP%X>bUWa$u-*ZAu43TteB8R_iNWnh-r z*yEY~9M@*$NYcTkZoapA<1hT@%uv1+ly>NbY!6KX{sw{abXsH*^KoZKKd9{_chuQK zq^-N>f%y*aLNim~M1+kPlN-$%OdQ#62tGYgDs?H~6^rw^sr|t#o)Z{=5{yAA{XM2F z=rBZxi-@i(xFPJv3VJ2}kWCJ8%5Qf2kgmB27Uq+)eD$(J9rzKtpk;G9AHZ@FaweVE7w|443BV(}$lA)?IjZXxCp6mrd$-iz^GT^ zb!DaHL5nKin7Cm6Mj$w!=xs|oz3NdU^M5UgVh6Tw#P{C*buZq5sU)B04N)%1^QN4@ z;EpE@nQoC0$r4~#?0QEFQ}_<5Qw;L7 z@G-nbTO;j)oa(GbdD9j+&HCo!th{-TW-VliU2{bp(s#;J5CF8>Uot?`RSx1r!*%`D zK>FFTGHK*C_{YclFkHN~nCTzg(%QoV*NO?+OZG)Qw{=JP=gBQ!!>wLw@g5Hix%C75 zI}!}Wpd;JCBE2$5!mQhUdm_4qd{?LJEWYyv?LU5+?VnM4xkaXdPVav&H?~0D1RFlK z@5_$Ugnw2^LtUI~s8Wm2;=&}Teq;6tOM=~3`AanV$wlU;7#F?oce{hgL}<6o+6%NO6UMO&fx20ul4AAF z``*Wa5g>(??~OOi;7ji{0ly3BQ*m#v-)&wG{yVMVpka^whmIZ0lW`?lrBAd$$`ED9 zBP|OnEA^YG=sy~*dgY0-`I-AP2{MhXt?%b+v`RY}GQ>6w{Yfh{Q~=TZra zYHwdS4%QC{DgzjY#)gJiH^DL&p0SkQ8=X%fE?HSw`C6qubl{1-n#H9hihODFAudz2 z8T(asqFLE|)xo-9vxM5(_m}?f*|j6E0g7dhZT*e0(x;zk#h+7#wjc!PuLUG)wG(_4F9JsiAKhZ<6 zoD4t%CPmwX=DXNG(F*}$^|;i7$RsY4si~=P`T5l1ktC#~MY>omfP8M@J)ovr5wQa& zK=F=pZF?JeL-oqV)pgi9^;l{ZpxeDWQqvE8%)|MCW@x>OXk}hSXye^IAf5GVAw)~Q)0dzF0-Gp-F*T&_PFl{tC@i4f5FX_%;|K84$aek@1f5G1-rdgak8g z*0GW4cUoGS86X#&_@y?~G693?7hDF3o64b25J1CPw_XSWCTYuN>Tt<@%6w|vH?rAk z0wj_LMgCWYG$CG3SG4Fd5ui>3HZ}lv5vxdfHzQLbKT931Fo<{L(V96aY80lGpvuM0 zZWwm3x%s2j$Hr!uiJ3VSARJaVG{7EUaUxFX<*ydW9O4E{Bp{Oq&UXxWz$3?(94w*BBpsj7>9-L<1*49KyKfd3!#%6;J{ok_j&65;yw(c` z9yL$@DX>eCxqP=@etv9R(%yX}<*RsjoaWBkt2lnGN5;PaNi@nkA)cTF$NPi`uHd{@ zx|a-iSW*($;zZ)u@!;G{|eUP@~O-5QQ|G z0-jL8OT&1frMZluk+}@MW&xoqa(Mdp4i2wVJ?!U*O@F*fx=P;&m#a}Pe$|ZFe~!3A zs%Yi)c`E4Q)S|%hO|KDqFwWw85fT3-WE0k^IqL>0ijk|)KY#kk;Tup5Vx;sj3JUQfL&w=v``7ovB7S-untLE5*|lh653Y~`zkXM$e*&1!k@?KUfj-l z1#w~Sd+G4={AJ@C=A?W%xy#Bcuzb@u&e|ukJHxMLsW&9?Ew_@Ko*e~BgD9(T9?&NFclH|*K9 zmzI-MJNzR)qq_XDPh$#^QOS4+>ATJ|`2thhN+)qZmWd6zs2Bx|7hhBi9-X|?wtl0y z-O=H}_c?XGuU?#CJZWNnTM1p_S=HV271A|MPuI2C0S}EvP`6A9Oxh|#pkIFUr@-`2wT5-Dgmw=UCTu<~<%&vTbc zTawM~W?_Ie1Q5#YiKR1aJ9iQnVuH|RV`D=EX^kIVW(97Ri^A!`ed+WV;3dGAYla_! zD3z6A?^~z{5YA%>jNM_fn>p|~s^XS$szrsOQMtc5$a;EiVUhPC`kk!yhbJ@{=`J2b zU-$|x>vVZE2U>SB-H*M^M(3+{yi!O1`s3TNr}H=jA`L@DBO%MGaDJc!-|8 z#_etcRd|T|Neee!b}dfQO8PwsNR|Dbx$Ga^5kp+LvZ7^TNl=$h?wPb3&AN#bX6#Zi zx69Ywb~5@c3$$cU-%p#^yb z`lA40PySQCPT$(mv?n|?xh%zchu6Cd9S5#K_v3*sM!HL&w@25yyFa39c0%9kpQ#1nEw;Gh-In)+G96#I=l{yO z!AaraQ0nFNe{rsOD(Q!&LO@=#53jz`%yShVQ)DqBLW5ph$v&I+O2vWZ<3+$--bkAe zyq#iNvHzCuTB2$+FgB1^zZ9tA{y6(+t;?oRY&Axuy}F`^37n*8TxJ-;8q?h?0a(Bo z70vAU#ehWIPIbw3Wc%@Nj*0(OOlP3AQ_ZuODu3)#@yQih>wOzp*y3h98i%j*R&gV0 z=sy*G27mH5HLjRd}5%d91gapRYzK+JwoQ%FXza6u=VtDN0~1m&5#bm-NfxT@veFwLXO& zu{=TUbWgu~)PNmMsidF(V}g>1X`GDcd))?~kdq|k?|fe}bI6iN@$?m+99Wb|_voo8 z(U9gjg`3K=3`?PVqf(!RRJVTIYo{cYapoSWB2y3WW@XvpK)yZ+CeFRTjkOx^7J;rC zG+b{{DfK9T<-wQJRe9ysM8vBCt@p`)8LN==%haZp^$)z`mWXdeaEo9ihz(2OZ0Xy}s;< zsM)#Qj@%LAe$=1Y?4z&-nE;sp!+5q}KRk53yC#V<*L(b;pt!m?Hq34|c`yyT3|pi} zPa*|c3yt0Cv;LZdg`fn_@iTuuj+K?b7e3G8r;?~3L*lQ7@yeVsr{?@#U4@fNOG}!7 zYs~d&)(hNBcdZI3zz-%%wE6D+6J2Jt1-=X3ZHGGtp2_t=!o2(6ZDjtN+&JP_-Q@oB zjy(7gxbeRPT*mAMg2?_maR1Lmd7vKurT<*~KVK)7j?d;*b$Xq65K$SqT25` z3C>TY%uT2~(9neB8khBJ7w@U0J|rTBGaS2Te=-;&+RY2!4DlOOc@F+4PA z&)*>ODDf2*XYtm3k+1Pw-tp3)5ZT|KD<}qSd4e3;WyD^kH*>=tWZ%y6EhYYy=0i$q zx%VxRx8Nm@5gu3>5*2Has?&?2cOE&Qbv+!nN$uc=yTuHWB@PwpK2+F_$cANQw zlYw6noL20arLocU!A#}*VpeCcMu~0v*2k9DfSLbCyg1^F-EvVM`5B24bG-7i8@^N5 zKT`yG(4e{X@D@F*uIM6bwjoBYxMA7Sps9^jd}jX2@YxQ2bo6u}uZ4v$71@}_ch^;V zr&LA~JmTt$cZuJcA##UGkgUYj2ylDB|HKi52>*bq=Fc4K!q#|378HA z_q?h3De--B%)+Wr42eozB_hbJQ=1F@EbtjV*Vp8blZ9DSWb!C;7n;|E`1G}5TfObqHPzDMUvH)o8^@*XcR~00S7;7n zdgQ!+9>T)VZ`|AOy`yH~5x`D%v?w0@^Z40+I3-P_n=cby>eM)7M0O_U)IJn{*TN~> zyEHC)OBuuzSG;2~Hv5GmQ`AQ{^IKEt=nXfQrFXPqpS<_s$jG>k-N~UU&NR1mJP38! zLCC|r(%_&Q7rJx#f&5xjM%q@G<}NACJ63HXW%GdLnmuIpxPSJ&P5FG2$JDG>hal@6 zM;3Yyhti)fH+o)1_Cd$iN9NW}TV|?LJck81$6@FEHdcdTE!sW0?h7l6u3?Naq#@Ws ztKV@Gav#Cd$EbCDjq-i5UsCLTb&fSS#~bV~3{mz*rY#B0imxh)u4JC}c?!NJWmqfl ziC=wrgyfLKg93=E{A1swEqwHPcE^+HHTzOj-At4_?Pm{t(fmHlw$=8RqPD8ibl#N6 zbRO=ptCGMJH6UN%0OD^Bp9!NZ7Ts3o9zEyiLE_u{fbB*06dN;Y_ zxmCC+?wzTjA$fhI&Pk3d{xRUVbZgZ>J?iE1udAdPB^4FlBx-qGy|d@3sv?N8E?j(TtbZt~uQoOH+489%ZfpD=N0+n-SKV8D z=S4tf)lY*}a=jmMpyHzL2Ne%l!sFnua6iMI+_^K)gZ=ERKYV0&0Yu*{wo7D$4^~yL ze^%Yz*q068p1A2O2M%(p4{JWJZ|6&QFinHF^}eU4p}wOoS%SB&Rss_%8($;`zQYV? zr9oThtt8;gKeRQ+@jOnvJbGu>@;f0d>z)zqc~l8JNG;PZ_+T-T>W`{a@JvIG@ZC-j zUZ)yl6$fE^P@ZHVPtfrgwhsBI56b#@jN`fUqUHRm&!LkH zhu+SnN>i&kIhY^;+#X*-w*&bY`SZ0^1ceX1)1dkoj!gs1`k7yffS*#sD#Oh?wmT$a zY3HKx=FgH%3z^&OQft=5UHXIIj(g^X&&ZdNR{uP?daA(iFH{GTW?UKYl)tu~u+<+d z;Wr-07sQgOd0-W$SxY!+XfA>wrj7wrnnheN5tL31a=Ka)!L^5}=c%Z@rn62EK#6w7 zn(NEPT6AgqZL?UFw<&~{R{!eJ9Q48IQ}v#E)rw{l19#tG21M(;s;{Y(RvSlsjDb$2_c)u}UL((6vx?*#~Q{yX6)OcijwhOH(ZXu_bF4yF?yjnT0 zeRXa#NA8by_d!i@usg*B^(#zoxZqTDv&U6Hc+kGDAG0K-441j>Khn`Bu~W;O-oHv02q(X6Bcs(F9{Fsdpb3BYRR3gpa}vW4wTnSE(?!hH`Yl_=y^Ox zx9K{-;YZ!lgVrhC0Vsv1mQJTx>@pJsZSy%*nZU{ET+!YBUYp@tWAE1u5y5N_tWer&v^Iq zMIIU42Coa2lWKSVHxT8Q!Ef-PwKb%p6Ka+0W>JiCQ1>mhH?WE;1CWgs6V*xC58KD# zo0ujZY!U`FUrsZQIKG6-N5|80EKi<8Ta|ri%gAv|yYT-l_m|a$ToD9MxLtgXYesUD z!w)lG7{FU@mE@gOsmg?P!s|xnvot`#7ZTnpB7r3k&?4X<%5r-LNq1Q#@;k236eO@c z-Q+9ZF_+{f*l|QP>ilV>QoB5fOFVp0k;j`I@eG=yIUJGXM5{+1IGP^Ndv5!)@8)N% zjX+~CsM~4eePS(pmf%j1A;h=KqM#6vB2%3~IybEHIlPp-w;AZ)l`bUj41DuhmR|Dg z{i-#xce*82L!}|s>)rs6lSExVv|wyf9**h3iR!tk5@&7#dnxPWU4_X<>qyOw!HF2^ za@1IZ{Z7>RZH?;()66C1q0J`iSml>_?f$qOs_K> zZ9TEyzGcO@x*)sK@VJP<+USZ?OI?mb^4y~~W8FpLMuV@W??~j{_1%;+hsoNzr+1`6 zp`<;P*^_}=@$Z=`xhN#ILPQi{j%+`TFW;XD7kg&JZ1yIf739M$$B{#^i((V)s$-O! zz1fAp6WDfVCd)m!~7fP{^T(Nw~to`;4^{Tx? zX7JL(BgfihrOcl5~)W-!yZ9_;Ss`A%)d$^AD`sXsrK z!6*29K7pr`H<_EnyiHA7`CMt!Hw1Jbv%{MCp8K@9Dq0^-3gUvl>qQ~~Fml6akpQ1* z@8j3MhtRO&gBvC=$svIZnxVbxj+*TaOh7CQ3^!$fL}o`R?yls5L6bJxEYZ5>)z(ET zG?v|_Wipf;E!wz$W7Y< zM4+;qoX)7oNDz5W{5e2|RT7y#J*|k;gMiT>Fwj3^YW*7-PL_wX(KXrU_4Ny3irhvvIT!8;j^1&w z=ZL5N==!-}I#qN`f`x?As3+m-U_J>CLrPXeps01~ptgJCzZhv@ay(e*yYr zL;eU-8de|$()xLoUuC7z?$J}n4)L4wwMW5=A{s+;b7|5&U_^!P~>*dy0B- zFhm9@6lm*I4Ia%D+^2A{z=Jk?GjnhSJkIZ2UM8iXrLC-}=*Z)djg+F=0T_H8pKBc> z7mlPD{|pbWU0!}Pr1N!D&|yij24iDm?+#{s1@`1X2>$8^qd+SY{(F1N3&2s=ZXR;{ zZax%GU8W1X2?+`LHTC&i^9>URcBzZ(?#)03xahsJtR5IWc$RMJ!1+uC4;9n}K@F0@ zZ9&s$!NFe6R&}>!`@k|DiWhNueC#@AVbqd44h~I9D!+_;DQA0sm3lnKw78U%!-b}+ zOBy{lA8zP=hjD$=9yq%gY3O!KHMy^CQR{GdqyIthb=0R52r=f@6w0LFtR-7%K~ias zRFgBPfIx(7K7x^rO_W5PQP2UAl#~=MCUV+Vy$$&L$taC~5A$n8a7)YY$49}Xp*w~o zbj5;%;b^J6oQrxB@cEq}hHXgqS&9R%fIxx*!jZHXG()l4F!kFvkxC8g!e_JURIJF~ z8=^D`{=;U*oUy}Zq7r#3kzAO714$~%&f5rYM!dOEB8MG* zDA9XSumtnotgY3jYnM)oZaS(>9*E?ef@C~?oY6)@`R~uN6vT{W^T83F_Pm%~CLD&& z&aZsu1+r4=s@O2gF_vy{=#I(+ka%7-(~CLe*Re?GqBc291+er4xATN&!|V$p2<0&) zAY-ac$|NwG_qCIv-@apV1Rhxg)BMP$DiAbxXn0S-lk!nE;RasxctEHzbE5mkXXmL6 zL!?6yS5a#2wCgdPBoI{6yP&(ATov}6OcH!Kl`B%>BcTt$1k9W)IFiAEJNl0eJrI?d>&kG~)%31N+T>z#jMq zZEY)VZth5wYpouG)@^cFB=VUZ<7W8rQ0eaQe29?`lT$FI-` zh=?c&?o&QQ4!O{v$NSd8?2{?0euJKY*m6)Bi}4{=(;bQZ%jD!onVS?=@Z*j&Br-CR z*bng8?n67(MSgU|)%yo@g%Q7f`-Rfb&283A^qahr(nCpmH46m;F2*D8!szX7!vhO? zLAeOTUQ7A(V}502+>=_`*Z;}h;LdPbIrmt!gm4NIc-?_0eJ3oaua8W!D^L0kUW+5u zFtV=bdUI{>uhP%rA+0p)48)F$9sTeyxW00E$iE;gKxCkV#iVm!atEmokpIw#t{5}$ z?#v=xeddt(kHHbHb15mnVQ$qo&;{E~30dVhdq+p3ofW|8CGe$Ni95}i($K|4ol+E) z0s;<_2xxeNO1zRfKVL6;D5dk;HYlloipRdR{Ut98W*@LVlEI8Pw){*x^DDR?pKX%G z?esOPJ|sOO15anZOb8CxlGW+nIJqj-9#UZ<%&S)Fc*wvCtu*SLDih)DcxVgCO9C(}KRxY-PSOnHY)*MxuRk+?T%lvR~?6@cFn2Yl8^i;t6rDT6_S$!x4P}Te7 zSW-BFkz`&X2p5b7)a*x6R{ipx!t#q`)TDcSV6nW zn7mL>sifQaCRKa0Eevk%@TJDGb|&rn@(14Gh{?ykAwo0}9@3^QTnOL;ulh@VjcM*n zIWuxGj;0O5w%<)NzJKnVts>sHh;>Z_wW`JEi-(9H!1ng;X#Zzzaf|-eF z_9Wu>hFAO1;pF7xrj7rg*P(Q}i+up@FMD@)_qoZL8LAFzLm z7fGfWpIHv|Py<^Ip)cI&BB$2*RW&tw;b(?xW`z%3lqw-^l_QSlX?pn#n^dtq$ zj7F%8M5AnMY^zn*ezia#RK(5u*@O@PWjVAIf_k2cD2n$BiQ(c@=h1ue^VsL4+Gb1} zJwC&4Sy?kQltHmDpmKB1QA3~$JO>3(EoNj z)U)R5rY6~Kl45jC>y|?`S}?zWKqax}i8mk^a)qV!0%zd;+18eOz(n;W=YLup;L2k2 iR*t=fPz?1<`}AGwJcoslq8b()aL7n1N|cEi1pGf|O@V3v literal 0 HcmV?d00001 diff --git a/docs/user/ProofTreeLinearMode_example.png b/docs/user/ProofTreeLinearMode_example.png new file mode 100644 index 0000000000000000000000000000000000000000..07627fd86aa9ca66f74a4e15e0a78b9500a7fac8 GIT binary patch literal 23841 zcma%i1ymeevn?b90>Rw|f(K`ChoHgTA;{nw+$BKJ!QCym1$T$Ro!}DO-Tgtn|G)QN z_uci@Tfj{9^r1O@x@zxTRfk}CS#cx;d;};cC?tt5B8pH@Z$K~hzQ*#hMCR4bdfk5I)7SxG-ukrI-v1rU<+yO{TVQP|)WQ=j%r& zd39W9XP)(+F{jr_u21u>E7z_Wb90X)_Xq6BZRWIXd405VqmLd!?@9bo+wumyiYz02 zeSM!@mFv{h)p0vII#{D|F<#F`;>P@AbSHKvqP~9eZ-X2{4)GFpn9W^I0VR0o&HEe z^SSd)5r)g2=QltQt9s>RhkpU;QasmrP0dx$MSk0D@P};JOa1d4(sNVY)vnMt_Wf6~ zaV4Q0W^N9!J|x$ehNZ;3Wk^qRJ@1kcSy2Oy<)U#Uz72 zDH?DL_O!HNi8|k_C+p8U+7RRk-oK~dN(BTmej~f*zvYlaKd=c?`=&Bf@J>Y5+AnUj z$ug+1^RnBN6vb1n2$}302!veB5h7hcaz~jNuzoN4K^kx-y9^|TM?Rj;N`I}fqhNYK zgDOA?N}NI;uZ%hv)VNP6`{q- ze5DHF)B_`){&rXD4nh%i!uI6Xg@jAIyQ1~v2?IM!3cdFUe%=o4P8VK8$<;M^-!3Od z)Zq@cpfk5TJDBzdn5aA3t8a0`5t4o!P1F; z03*wvJE7^VL%L%kn8ud=*yyl1AO`2NZee&>t{BL*B4FX%geGvXsLJNZq-dm;LlOA{ z2g(5F4AhWv6Z6+q2nPNG3B|k_)Hz<8i=$sixTw?Z#b=nuSJ3L}gd`@F%Fi-&FgUuU(OLz75 z>Iz&N@BVSxOFZpbdM#kS()HE}g#$+FcPeaUgHxfR?3AHeHQDv4lo>fjN)z*{A+_Y< z8}7z;=;_YB*V;U2=;iWPhlYzsk^^W?)Base96&o>^>XiqW|pu?Nl9#E zvEID z=RjJglnmPpb8mC8yqyG%SovFAF~*gY&1of z8nJ-KcmY3lCCDi$r@=P>@MGEsP;F0)LlYE$vRnOkyuMEji#PunR2=u-ik;FqaiByM z5N>ZNkB*BImNs9Ibf7>{a)VrrRRx&0Ww|a>N`OI1q_1blpZA<{hJ2TOK6GR#v#@LO zNm(Y8tmY%Q?l3($h9L=SiS>p-Qt-1JMBrY3(wpQ194GK>&_h|-t`-I2CHVfs-5j%? z687CT-pkx`vT$kjW|(N_N5bM>2`v~HToHhorqkPeDbAVjEoLZ{?g_)wr@=F=Vz(lM z9I(R@QF&3$^ZxmihPqBkB1n5M!=uCufcg2mq>iIkyY~+x?{B$FB`lZ%WDt4cZ|0H& zbbR8!Xx3=zm?tG#F-NZGsrtuecx@|x9ghqNtMxag$R3Q?x@gpreyT*RSuU*^pl>Uq z3!!~8&<{@TwUA|7h%Im>bRT`YkNn;8d6nC&P(qv2$#?d?DC#!x$!1_J5w%hMIURoW zT3#k3hje7*j?vv216>riU0-|3QBA2A<-v)LnvR-G1A{zBgl_7~9{M|-5@f~nl8>SM zvt<(UpYcRtqEN-Yk4vBhXG&pz`m8BceWUW()pT$v&71B6?U$}2efWWGID7m6*KH%* z^sZ)>{Wu+a5ocXDwsnG;$qzC#0}F)sih%ZhpfbmrrwcvAW#$5>XQj4EcWTIr{m zv9q|LKw@@ao-Y0#-DJ@nQJBYF_FRLF2p$wFsC(A#se&J1z5Fw}gq4DdCssqd6cRp& zpM*p+bjM96=bko=O<4 zcn8&u3%s)N_P=P9BRTSff(il}SZ;di2<*AHA!Fh*gN?MTYZ}FIusF)zLJ5M=K;5`d zP#+;LqY$B>48XW=|2cyCd+tRvzFh4^LjH5w2bT<@8vjS@l3lf^bhLPEMKjmjdAU9I zj;F4WbRqYm89$BC%Zj76TbGB{584O!{uo5ZR61^&r;iJp7I*xah^R|M*@5i^jlZHunSM;iASnoI#BNvBzFW*-6-bhw|*yR+4A$rx%T)K;yuSGBQ58cUC5pP0ji& z%Ho|d!?hyd5Pt17x;fB1`Z%)4lgWpqQ^Hhk6dtC9k&cwsf0e3uRA*sEi#xYIO_n)C zXZg)$>O1rb;UDh0jdItx=@^Xhr?hic%Xvl5O$PewUYE7F!ny2udx6VaD<-(0Tz)c zIHKW6auNv~BV)Ks`lXkKZmy7L9Z;yGP~?a5ppkEo76c_V@y$4TZBjYaU=rPy>L+sS zcegBq)e?YoAFSWR--apODU73d$ySxK3B5P3MO`>d0L(+cp!EQwYSbmU1&$E~`dQ%GrBd zqYL2|pW+hsVEsdu_p}SOR!y#K1Jlc=#_yMSek}gbQQ*LpYQ~lysr(hnwuG~trRQHb zQxhzWMWc2>sni(i~ zpg)5MBfEcGsq6-3zxN`uA{2{;K+gAT5`=O40yl?;JxtFLRhMWSk5*|K>7p}R>{f+; zaJwzPy_?^9cru1Wii5dAT$qq&Nj%24qbQg1pnJL8@l zMIdWO>4e~!!vB3<$WJR2dPt7CWUU!|+@b$a>L^+DFzMW;}#=PwyvSdmcJTK|R-@%XgOdWhIw4m5K5`wLyG!}of zDoo7gsixB-=p8TzV1<$62^cX2CvmpL4jyEj!&-S9R1_G6*JxohdJ*<$P;`-8(|tG)hi)FEYSM{%r~^R9}J54#(W_t`cA>Wes03roL5XOGxnTrHw#Et zmAou|%S)fOaN05NmpZ~P`cR4bppxF)u!)Y4x24YwLF`=%&d0-u5)zwM@WRIc$6aDf zd6|ErMVF1TH)mvVYs}o`O&BT~8dL^DXRgmy>#+ii?ZtHGCblRHR>}hNR-sy#;)kND zAG@D!KJ0QsjS)o{oZj&f4mb4uzyN}gD?6Pp_$9*#ZPpjsq#aBFB`HWow@(h0EYWkU zr)H^X?p5T%Hha84H=^Xc%|HHP>dr{p5d&WQpUpk++4C=(&V%Pt1T~$|7Hz>v{B6|| zF=pm7;nX~`_Nzk3ZO1E}1G5-A8+?NANq|@KJ+m$ElGx*Z>1io%u@&kcNv5FfbE!z; z0bC`tf|p{3qH@d*LQ{t`DOG2k)8rbLFZQu^Cr!r0R5HfzC4qV5#_wh0`PAJ$Q@c-A zwmW`#$v($TSg!GqhP%9k;XdK0PRx{%fUXm4**r^31+t z&sT3127m%q6&AK3S7FHOlJ$wM(d&URvsl2;I$uItZ)@uO3tW}6eNzt=tE8y1w)L6I z{MNiB-5&J=EzV-Ms)LC`T%}3tE$WL!r=(5KftBW(Q{u^A@p!7Q0z4kc9m%)`p9QEO zl^gQ>(d&>kfd4Qo%mR+GCruoP50`hXpSV2};EGQw2Do__=(u>w3l@(~uHEc?bEbBd znn$vZUcIPVY4yo^gycc_P2RQ&A24r8ARczlB+=rc%8T31d1Ngu{WI&yRp-J2fisUi zojcuXvjI0`pl&7U*1ISjy|(2rs$m($#g)`7HiyqFUC69y}3kdK+ z0h8srp?}zTXw$W9$9I@FlehpCC6D|(l41VeD{vPCV0Bdp_~rV@X=#f+47craF(+eb z4>HEyIJPJ}XqvMkOCNWgKvJLbcew71P>b3}xk{SWT@%B}g~4nFou5HKW4o`vu|c`_ z)`S@&LxaFG3_h+vS$6A-CpY4T9)wH^BS{ukXLJz!x@iHsWg9OfpfTG^pY0vxXiSk3 z!$aqdsx>PCc0ci5k>~pr2XLC98$rz}Zj+z=&0SI&9o{wXQ|&aXD`PTmgEZw!HOHM3 zM90dCDXLJ9GapOMTFeWnZ++z3Q@=JaOSjuDr`^6?6@@F|8QE~@QKymIh{2|54(w5Q zp9dzpvU^~H ztEJyuXGkyDM_lVAB5Y8==myu?ls!Xl+1o}ba*s>8@Q4%@^q2V2U#j@h z>Al!vW5V$5(vH$S&#`Cj+^V);GxsGkJXj5?n3_^1@_w*&YvnvCD+|J+2xR#=SV|Bv zU1AmxS1gbQJE|vMh77g2=G1uyt1$W-dr)(0*6rO{XZL$q%?i)Vd18!|M65RrL3=OGJC5m8UgXZpu7qN*52CgTH{ zagScJTU<|K#d;~5(|%x#CGJ8Dgrn9*Up#HvFR@{pS2At{V{#>r?&~vi(V3QIY(%mw zVmNi78yI>X{GQ)!8VARnYH^=6cfXIqJcsu_QEQ%%%< zv4peH_3)CeRs`-MKiuBlo^k#RTs>vCuNoh0_D2=^0`6ar^yjsZKe}LeIef{@U%s{| z{$+jvOT3nr{@*p+m$Cm8?*1A;O5l~?Za8yQ3`$FN6~HuNB!CFnF}v&ZHxZ^s3Z}o+`Pc{+(ch2bQC2gW(Dr=oS%|j*inp`#1PXy2icB!n=Yv^ z1#e{;I^}59a2Gmcj47E=%(EhR++`~-GI88KL2gP#BFV;n1S?b zEqpeoM!GPv=@;!DEGT&9&432BQ$^nW8ZRbTp5a$s2HasDv3Mxjyht7_x8ie)m3Hw# z$JGC-yx&SP?8Cb0D?Fi^&}BTQ`!=<96vpSA3%h_upwFBUx`#=r(`c+r^ zmf7eOZR^sZcmIb`D&4zR4XFQutpp2+W8L2aa-0ze7kYga7BB}n1p5{Dxipe>5IOsB!CKnvu{Ij(CNMfsR zob^g{#8@7K_MmBmN(ZH}x{#G)=FglXX;j;`l6GXrv~B6HQh?+T7EJ*igzg&vU53Qy zVs6M&O!)lQ%Gl#DP)vf~q^hcKpopo`zMpZE$W-Ey6{>i7u)&fP(n!ZSawO5g$>x@@ zV~=o>j~ino`8O(1B)}?WxN4m}LotK`soiBk8qHW6LHG7jT)Djk(YoU6#pZ)x2fkc) z{_HX%sV7hAz|S3Gu$+y|4q6geAZeMVr2H}a1*7Ejx6 zNETZB_(C2u=-Q%~8p2Rfk^tLg3;#T8G_b#amt~7UGXJZb)IeBAVF?UW%D}sS>)Bxq zVXf&re&js+o8Z3w3289aLE`WY7r|_too`9i+(WB3{W>={Xz7j?d0#LCt7AKZj?&zQ zhKglEA~;R-IY9LWF>EXP&9|^L;@hmUg$Ntxw2!opYS^t?p;jk2gf#D}`#r`7u%1!Y zJ~c1k=J?k;^NqpC>4{Ijvm4#ac?_giGGFhV5L}9;4t^&Hudx7`?CAd`t&wY^gbk6) zZcxz)5P1=>*r3K04IVE}{iwN}&1=6GzznYN76bn!Hz|z8lHo#)Nkm#TZ*HXYj&N-N z)IiUn|0Pm(dNF-`%}~W9!p4tawA4@8+Nbc-5xbwsOt7|+sZ1x_-)N1*`Ucx5sq#St zQ(BY9;;jpYRq9*L_*@4BXd&`vK`9e{up?KTO>W~C4NL~Ah>&8n-yp=0F9;tX^XF_{ zyv6cBNURj?PL3@Jd6B#q&p-XTUXtJ+2Ap)tR$-~ zl)knWE1*Rn$0?2<^S<;6chcU@&HaIYk^cH0f1(6Z9vuy+)6$9o7XZM>>jQtZ`g>~8)>>t6!;hnQYw z_us~ARs6M^__sX%YP^z^yUWghGmpSRoH+Cgd%cW!&cvO3>L{~W$#=GAJfIu?_3QGd z>xzU(+PIw*bz6AR=z0Vn1Qei9e4rqT;2PQlQh3t5Ey!Z_daJZa+O#cg`1wHvvxvca zxVSpq(uH?|&ql2wc_16w%k%)YLi8w_<{x0uSx~YgOG0H1X;6UUO0th1ni>Y%9Q(*z zf2+KJ>aoQCF3YfC@1>|NU*&q)DDBmx0~q|0El>5GL8sm(UhU`b$^(d zVgDupUHxAL9Mw6$POWK52T{z7>kr+N5cIg17jhMe$$^X2{&yjUGJ*!a!9^_}4geJ9m#_s$zq_Zxy62oIRny|J*i=uC*nnXD#y= z(aCwh11DGJD!j!28Vk+&)$A*Sfrnm{Z1(Lo7Yu*V<3$=mTgmTFi!l3n%a494jjH>>1MqC;z? zAH^3lv<9g8#Nr;f@pVWc^&?iGW9DecpL02Ej2e!(7`)w|-6PrF!n7U%V)hbQ;PjFc>shxS==N~}la%M8 zv}z9mK{+SZATavc@}(dK?{|O(P9I-F#FbZ1;*s-oII*m{VeKNX>fh*UdS0NFL^k=7 zKv}PmqEwZKr&{*pfY0j(XyAs54PAiWClKLN)1tFT0_|hj(hBp zRO2Q-up7N#PxWpwywz^Ny!MX;+Lf66#SB~}hSJOk$dAYZp-pEYs*W;HH!he<6D}4O3Q{imjF{l4e*>Hol>rJRi|3+V`k8(2Kqn##Eyo@oUvweRWZ(^nUpd_GtSwN) zX`=pACl70U#=sj=yK|whmfL}T^Moul9~|eAjn=j%A%0}LOf39F9YJxu&otW7!~4es zaHOtaXi?^?fQ&cIP zG`uGPs5l{l91vth#SR6js=~-{89qp=c1kwRHjKZ>Y*(Kl;vm0AT7Qbg`cACD{imz? zw#HbwmG zhsT0I^1>{v3^lgZRb3;cXx|y1Q#5!6*2s5JW85287k8z$js{4LkDZo}H-g36h}AP3 z$RM?6Vjy?kyK*D@-=Lw3W*TsYs;A&vICo1+TExID#Jkmzcy{mkYG0Im8-wxMu9Ahy zkOX|Q6BoYdf}(D91N4lG(omhyh+AWuxqU3qfga|g=i!MP-%D2YiZhAbvtgV!NgTTJbBZ}!bq_&4 zaEQC(BWm^+y%iJ6-vb&Od=(Sx1ghHb^%cz`fGiLQ5TCcKA$VJDlkZgm=Sn!xK=hPH z#$u-SmV2$Tvxl^1oBzT)atP5WZt(=u(=qc6a7!)Ta(3VXFJrtViZ2{sQb{*{!=4@A z<`*a`6(DAemf{g|BBz^O=4^52^}u$FeBj>{L%h^FE3?7Zow)0|R36p8N0BjJtOG@4 zeN;JScUB6U}ctF*dM!7@^ly7O>ZLEz2!HvkQ!%fL%I-J<0LGCHA9LZr;J zx8EMUP4(w|o&-`!+|Duawb-_YiEVl%*wI#ya>`Vs0<1@x^Kn`D%J*KpAsCTNaJ^G0 zhfD*I;dwqV+g$fp!HNemPISG@wyA3@@Cal9mH(GZG=VEJroH^-Hi3}%6V&uEhpn8$ zIT6ouX7=aa<(3v!yk1*EIQvb_!^}zPs%X?^1&m<-knRr^JK5Dt{qi&jWT-{)%;HT8BLpI3K}|SFksIkv|i4GG5LZ2D8QdGHCKsApBxUHWC5)U&nFov ziEaA8`n@#sUYm5%h>olUYqLl-i+F0~9GN32Gs+5))Bqgxt(IQ-Dvwu zTa3fCY&MLV*ws8P{g>h49yrx29?QX?a z(M9h22zluy&OU@!tUejXVH?wq8!Kq1imE!tpVekeQygC}QGqVXibBt-7p-PG-(k-w z+SjZK1~xtjjH+Mi2$ZcoNOP57_fV0W^)%7|uA1Y3XqQ%!Rofv;2(8mUgnJ~Nxi-G# zQ`_6OBqux3x=xmW=$cceRZ|%ED*@cQX?OGxut_ORb)(9}U3wZ23JM5GjK2On;x&v3 z+M;EK5IG&GnM>y4dxEKJ0U;35*f zKSTel_3UAYu?gK*>=Y>{wOS{~N9tw%f-E{2r$8mu565{hudU~ohAfKe7r*893z=c~ zrSp`<5kjOr)f;0I!AB4=n-CcKKl-aLEmxq}%O`(-@87*xD1!q5@0En|jLWbV`-qUe zK8$Z$hR)H_#?dmBBk4nil{`&VO;tQBR4m2WGR|a3tYbmOf~RPoeFLPKpmjUc$RXEc zD54awId~EV*<#AsxVi;F1qC9Q3czgNY}SxBzGGw8UhW4NBv;j6$?5gBuG5sfGj-~$ ze?R^%EiblS;Z|>qSu&YSnV7+G;(BUXQjo1;U2NA?)l|@a@ErY>0XiQdxwx2EHQSRj zD3ftZfdw$||8#`;j4A>-!of>va%W{Mn_f*_US=Z{RjKE(G^BJH|IHaIC%ceV!WiM4 z!NEe&)N$xnYJaQ4?VM+yz~FFb+)c)*B|Up8i7?o9c|B!pzs6fZ$is<7aN1QiDw z(fEQjRYlfOG$G1G*V0tv4wUZ2$_-iwz8{0YOFVeRg@yWy^|o|ht74{^$W@Lb8P&`t zYH>8|^ycZ!T$i;6EF_OVg7}#5!xFzrR4k#`{4HF0*JriMg89QBePSvq2*va zJ?}~TTi&N`rH$=v`-J*PrbAX+iyMI9P+*_406Bkq22fW=$d&{o<9$8NVh*C0`Gj-J zJKz4t$V9=k1)Q`z&A(sni~)8J)ReiC?Y?6Y*&HV2SF+ZXVUml>qNTpX4fjBXp;~`hqS#9I1CLw`;PF zu|i_5Ze-&(P8FLi`CIz0JG?ULu(Ag0qVKB1kHH2;j$oX((H|--zAV&`Wt^)H3A)|x zjqeWohe=cB3-utG{$40ORj49^w*P}!Sw4uQgbMT7@PMd)HcuwSx-XH;ac`=h#Lzkt zSn2?W#{y((h@800VS;NDHO`$MVKxRGvw9=uu-hT|Xd*WQLb&ccD?@1unj?Ena_DZl z%T|5gWPWp+(?cB3SU&*_^Kxto$sLd31SK~lA9TG-t(@14XKdz4_YzL5D)c$uG)kR6 zMfO8{k{)Rce_Ip6H<{6k${iJVkHFV-L%n$ zZC-Q8K(ytSC@y@Gv%i>H2EDq7{~R1KalT==;i>I*CF}m-@=d{9r@GCDs;j}p#E<5Hx}U$UCH&ddnJv#}ws`8nM*zvO1o1Vd~ZOPkd3- zJ!kT5f2Wx8@&F#s=5#F%JYC9-4mh0zx#~jnx4x4DN^OMk&a;aHk^MS+Oq@{~lSvaB zvLf-Z;I4Ac;V*Xr#xK(F2xGom6X}x!>YAc~hrHqE6Bw7fT$oTt3@c-sxvbm8#$8|D z>aWyh@d-qsKGK#{(r{+EK4>WvN{4ohnLy8DfDo`6GJs?ZzL9@E`uh37UmS%qu!j}X ztl%8FHL>yU&9RRJ8BKe+T1&tBOv#}k9RmY0(!20W)0E8E06bmOq^XQt$D z-c}YQ_dJ8E^!6+6qo7AqQj)v((GfFmkkqf~$>(RR24m+holHDFZQrs=%5{t9Zzcgh zqrya0xRZebQHZxX;E2f!m@;Ns-WZ+YtNij0N~5f_>uPAs?X9=eF5AtJV%PD1$v*ZHp*9k&j{4qDRdIg( z*=mdY;c<)YYBcyt!r(@X1}txOy}}X|H{oP^C&S?W1G;&wjX4Ah&{$&Rji{by=SDn zD>aeuisZ}0Hb+O}3@eq-S7oc8ii8Fg8k%oq+}vHqazo()G8KNte*)YYE9*AL^kC?c zPFenJ5_fKXbBD%a#RWG&(4bXjMI<+sy*_KkSHpvG!qO9IR}GfR%~hUinm_6fWk}gNAWaD=TX}vP^e;N!f;eZ+eUKm;13d5Eo1)^`hpSlO#k5Xk-9r2aSVpb)&@SCI=;sm(O2XrBt9n=0F9dxWcx}3-za@w-7ai-Gr&zn~f z-?L^<-lLzLIVeWx2&*twc{;&Br|TrQ7P?ay8d!{r?Z{^UiE?b;ELh=hR{!KbYBn}! zyQQT>`@P@~!Z`QwYUUOQ9Sqqo4OQ)R0e);iZ3?K?;W^{7=|TLNP)?M#EIr$2Xh);0 zogH7rEhhIY$`DZ;=A>m>S4dz)x8>(Z-ijR(k&g_LCy!ADghE@ec$1RORG`(R(+h&m zRGD|FjEw73;m){*Cnk2&j)VmXbF2`s?HG??Doy^H5cKZk*Y@J3@U4!b__sEJ2H{>A z2Wtp4j2owOpFZ$cSkz}i?Wr)YAV9WjlqIp^2DKm{_#mpK-*spE3rT;h^fm${l~Wb! zPv)d{=&HEJX0r*(at^B1-|9Qxv6rjH@Ri~~peN@dy@~dJ2su%S{@6Poo zP@4#1yVC#s9YBB3qfs*0w=V696-O~Q6v~9oeEdGFehq(@EKDR1GY9I*S5zd?^W@Z4 za_b8=u``WU6aBn8q;Y(SBl(s`&Y<*{V!aXj+c0d(<07FRnTkC+kR;avRiK`i8TGrG zFS>g^p8Z@9z?7waN!<^Pd!rX>$Fq>an?$X=iU$Iolqw5zT(J#*)53mLSM+~VfMpT< z8;+T+DV(yXj%lRn*7&Dt9?JkvZ1;nhwShpqNFskSmJtHf-fwBjcPV&LmA?Lepw=dJ zP#gws<$}*1SkA*)8_R^RFg+YAeyS8%69`Vx?&Ik*aN0hm_MSNNPRx@8|SG~6mu`p&#l*=GuthjJNqWRyI78ZN09MkE*@McSZ zg?6oG#gk0YA5F3m(>l?Vfkfm%Frnq*&-fu2fo6zh7VP!l?5`;Ud!KS#P0zUW5fQ^VXL(kE@yR^`d; z*-3+q?#68j8y8E;PkOI;_vmXQ6;eQ6NN;NOooC&Kaz6> z{rRK!rllz-RA#*>&^<7{rRkk8s=82@PqjSZqvi!AOhf-SS1*K3zdmB2E;xC=z#HD#@ zyUu36<#xp5k1O^oOL9|HxvV5qw49Gc>~XpR*Mlm?%ECH^Z}Q=^xfD#Tew|zSSn_6m zFt#)j7=~+m&Yb%^Wx3ZNfwZu4lGU3ytZgA$VlKeq1fP3_8vGb`kyMpoQFM`uJeQCP zTKpacJ{5aoywNw5_!16c%y}dR09}aufCTZOR79VvA-2w1NKGX8I$*7Ma_P(>yM-lP z9EUd~_8=x!lTlGSvS)tEasV?hxPloHxI9@|sJMEUBiiVRwzvuT8Wa~Cv)xz4v^r?W_@&hNY5g+v%dF>@y# zL1Xk6DAx>(m%W5hlARNdMXjgIc#ouc@nE0U6^&Q??m<<<*AZrSIX!oPbGH|36sjjo zf3L-N*pho}^h5VRBT07>Vo?p;NEaXOYSUb>SzTc*xKM@g#*qEERN%*BZQI^K_{cTI z*5M88J{Ikd6qB(P)S;;Zb7c-l(Rn%bet7HX2gtH?e`5%ZXJO7I#SE}4b$jv?9~yC5 zyb0u09Yt1j1)`k)@k2qMqH31to)?7>GJ2+o1UYl`O6j(^waA(WPgJI$Woq{u&CPzl z*>B1^-|yX_(D)gC{kWi}McyLoB9B5SaEweSxY$X@K>I~h(?tm_9knz=5|wm(Ses3S6T$O3|Ai(Tp1~0s`?Y!zdpKNrm-qQ?$G8~ zeS97tjPpccGLMfW+HcCW>3X1R?G4ExXvWi%GTSoc1u*g3I->6mp}TKI<2V!(%66LR z5QEZ$HT98-RJrJjBNob%?AXKngY=}iQFt9F-Na=!Vua)BQ}r5Nvw*Ae*RM1QRr?MrT7xtRU9X3s;aejF6E_li#0(# zr6|!m7>l8b10kklZ)4;PwvSPI&l0bh6ib;SNIbmFS*TWzpDB}SCa`_`W<4taiq>Y7 z@LFUpo*+}H==G{V21AJpcx$oEz3Ee!i}c|qsgxwWqt6jUvi(yD4Z0j>!auD|-n6W@ ztrZ>Uk$HGmQCZca=%1f&u6n+JE5J~iRH**gq<6ae($G{AEo=hccML(<+|C#cpF7QR zF6Cv$7jmAMzOFKzgmWd5fW1&n&l=3c)4%MyWzK>iMTspW}4{CV^QM%?psC+$!1 zV%;@IfO*bdn3J9MpXzAqPBCc>E_m-}yLitwh=W$rXC9KSitisIuGpeVEnhByci$9Q z0r_yCi7R!I;ngF+_YlE*al`VkdmC(NI)7RBoiE3`%P;(q(I(IPk28jS!)b>cCb_1GrK$rRX4Pd<;qu7|3P2bK^jbwX9;_oXIv#R>O;@B`VEjqRf zFR--{`)zf|Y`}cU#d_qhRN>k^Ow%(F1@19k{F&O9alhtC_wSM!A{P8dbulx()I?~? zG@6}oLwQ$J5;-5Zd_x}bj$teHjr?fiXSuTl{lbmS?U>^);h5wr88Deqd<>$YhxIV_T)F-U>{kOb6R^|V(Uez@8Z5RlyHf>F9U@Ziahk49Q6rc(Wt!@}^gkvmgyIdU#G;n{|EKi>nY&T(2 z*W-j;SzDM#cy~&TKKgEZIPyOJtg_^KZu^@&_RZE=&QDD~9h$mN-RhtPrE<->M{=@-in0@SmFSH`ZuL^OPWz{mMxE(JR-;w4S&WmsCmfpvHTVv!&4<_}rXop=rc9 za*h|^RUOYk_dFbf@|>9QSVRyd0avIv&W~~k-Oxb))EFP!(YC%F@#IhS)RnSYnEz>+ zHF*2^gz;e`OWgJD8Mfk6IribXokIBe%AV+S^Zbu|;#)KUyXxKu7dqZBH?_)dEs-i9 zx6?&N;`LSW^gl`4q_@@T(8@H|lxNw;_74lsFaN3ZS>>wOlN zq9vwd-R2?LdH6gS7RmDO*np;a1*XzW3R=C>LDD+e9j2^h@Ofyfl0BJzQKA~z?+ZR! zh<+ASZ5X^i?AvJ}JKrmA?{nCC9B%erO0rMq;_bQ};@e){FZh{JDIlCzx;jO_db&@~ z?q$ypN0zs?Z~h~90<9cg|Dawz;>5voA`7J_o66h${V~MQ?*2fLccFsfvJs}>f$#Q@ z2)1rucu$w=aL}mz*uLUzpHe^g5h>At&PXZ~;Th>2t_YBF+*=4>20TXpVhJo%h$Q{s5bG_Jr{)Ij}X5%UUh&o!tiob=T?AddCp=Fu*gVEk)ib z7pB(j>Oi_r&+i3*&mvO44XEHK4GM|2^ty3*gD=BWK_M1-6oc$}v#~SczdjyLA3T%G zw3XjId5;C5o0nZ{Kx9y<7NTOJ{Ox^LB8O|t6J8KY@Upkrj_pwV%B);J^7=iO-9{g- zdl~LNe&0ny$z|PV{qay;4NeTyCqNH3QFr@cNsOsdRYSCQ@Of|D$%s6gQ%s$bAq>cf zPRUXysiD}%7}`IcfG`3#%+ZFbGkSgp7c@@!2D6Q1tywnJFZldhHKKuY*omIfUf_8% zOtQ>d?7|P@OA1kr@~UzbF}QFd@j6oM2Mn(JN8L z{yw5N@q#dq8;W!x;!-QH{)3!WAPnSg72h~rxL|Rl+iSYnu^>Ir>`|Y= ziQ&VI9KnR6BL>8OL6=3vlbAp3i@4lT@@j$KwIbDb;Q5XF`&v6AFM~<4gokH-$&Rt# z8aovCBBV>B{E|JX)9jEtP5A=FkTV|Chyz0#4`PvIx9|b*qhF zyb8(><1w0{9vWP;)Mh<@B>a}vnqokfZFbM~hOtMT9SaYdkHS_8-a$#<3>484!)X6h z;oDEc7$592sNS4pE7zIm#E&n^|Hk78rI5aeRIt3sj$HH=g-NX z3Z?P7QB?lcg6)ciYuyPHn~#>hJkulJOJvK$P`kdrdMHQA9xI6$mmQz$|Ec4=qv3qQ zzK;YEQdnY_)$K-S)###k(My7`dW|50AVlxIM(-tLwdf-3uHJi%-up&d;*sC`ocFKy zz5lt-T<6T3xn}OU=00jCmx2Wx%4A+`ED{q^U#TfuvG;3 zf`L_p6c}p8;RrGb$C0@&H_P!5A{W`pPM58SxE5&6B$PalZ0k}9zr(xKp%v&tci z&62r(p^Kkj^^!Do^)=jGL1p?khe$ck z0$QvP$m2d{`#c7yKwgPnh!Eb`*oZk;$Y8D6_^?BRnB2?k&lvxU%*X6ZP}bE9-A*?*rxdNc zh+d`4bX0I1OzQmvq>8sKWnil-VXl^qC}4T06B_q4@BwMCIN73Xs?fSzpveO>A?2X) zBr@@*?d9#OyQ*_^bK$55o#OaN#_EC$|ljz&|_L*{2 zxU}Vk81JKEvA=lxB8!D>nlmb9F;?t$BaFgu?b@amb;pF)A&7OmF@~kTj zXm58s69-oBz4BVfP0wSN6U|SoJr9>K8fy&^-%Qs2CZd&I3Mo>_s{I_0lC@O>nXA~m z(1!`0zVV}jpYe{@%VZ=a0XajM!0lRf%)bD>znXhXO=_tV{F=GMl2IR*@9C?T zPHf#b(CR*4jp86P%lV(sRelE7th96Vfv5El)_ybXv~B5fkc_l8sALVVa;ZhlvB&lo z<*a!lN3aMD4kk&ydb%Tt@;tLBr#f!3{u$Mr7jEqA*vBz@QtHRW+B%+J!u`->Yehd9 zUZh1I8lw136%gaPm`Rif+!Eey( zIfze>mRYzsHBTjt8F>?SQ(QiBlWnPLnjH)Cm!g0A07Sj&s2mo&1!1uYjw{D6u#zBl z`)TcmZxs1bVV}X2ymF3Z9B)?oLsNO`aWhF1h&=YvPI@JNdgCzQTR%B58oz}~S1P0n zC*5Ju_f5yig?jMt#L);NBrDjY$YHByysKTWgvYcYrdlF+?DbD?jh@u%16Qxe84Wvn zvnVF3m`M11gMaMJ4sd_n`$*^Gk(r_7Qg^F8bMV!w;0U;}kSd1qJa(dlj~*_+c5nV0 zJ;R>xhKK=U!dy-kmhE`r2g&3VC_T&uJPlcy5_%5K(98 zCn2kcdD2!^{`s5i*O015L^3w4q3@99N+ds+rM%OOPjz27izy7neokeqIW-$Q#&a6i zkMrgaop~=%m1!&IWxzY>6TW1??s;%HK(I5eNz?c=?Mkg}7}%ISE?dz~_5-Vt)f7*Z zZV@yz_=d#8QuNY1pBUitBSC9K(bZiru5Y5`8eTF9D)FrSRGL&PRFv;#IDiJpCHf@E z%!YBWVMnH(tE2wc2a?{@`at6>y>2!1X=thVA~m3N6i4b-U-YuHlN!PZK< z(H~xB0_#5tJ{;jRUBN5fy<4f{<5XOlPUq`fjv_hW4IP*NrTm&h|C2mgCLU(Ij@z=% z_i;0xKn7D7%=2kXO?Hi`_^4*C%Zo__KY75T6eGot0489v(gMvS6omzE7G zNvDwXn13cC4Vp1T*M|k=v4>5tc~4qlTqL!2@flm7FmC<`J=+3dR(uJ<^5O0Ff=@Be zAD%BHo=Gx;%0)tl6nT@+L_VD0MA!RTgT`DBpEaV-zn@vF8_aT>ds_j>at3@TQxw#A zerV=uJqnH@OHf#t)+?bgsUf|b{mNs-_6(p~1>l7~eQ+O-0WP^w&UsaJ?caFfZ^*L0 zzAu*h24$MTjB}$p#qX*IJWx_LYS#A67F6g>WD-s3m#?9oEJe=CDvxYjrCpM}PhXmF zy1Tnyl{n|foJtMkZ`gC)c-&Be+gOP}fV)2V$0F!zB5fl)c&uNcwp7<3b7%t}Wl1Ke z01f2ld#IVP5ssV3AnDHbXKay<)9x^zbjGLza}aH7kIUZFqyau{@ja;wjSC0JUxb=h zT$4xiAG;c7fuFZSln#ia8$JrEyQS8RJzaa@*j<30zA4a)mMFKFoNOVrEEa+QMJ?%x z#ILKq0pB{I%Mu(F^Ci@Tz1rMFgA2oZ0t?(uajvfZ@BA9XBPvhnNPV}MDI=;hJ({!1 zh0!xR_94hIZ`OUnt&LwBhAc(+C&x(paa~^}44ZX@n1`#}JuSG1^H7aE&G(q`mQN?A zg!wtCJCBKK<@V01t7G54;ask0ovzX2fQLX)wS%>>pnI+I0pOpgX)OH+^fSb7if zZoaMU`w&cMs79v1q_llgEdlFdv`4hrR?oEbG?jhj!G~9+ns+DxK*;^=o-Zb@aS^xB z`u^r_x~+{v@ek%K6^Yjvn@LXt_^MwZ)xyuiqNCX>&_R@EZ7ET*aTgIyrU zhFZ(=9aN$_?5dw;#&&clQ^Il09gwTI@cIxGpZ5$Io&OA2Zsm;kYl8gGU97_vgn^MU z9Of8OJ6(?JJtZY2MW&jo z-WkZ@;jp{X|D(w9U$VY7jC4H<2QIubr~+y2XK+k0wG z{$DG8j$%td4X0$67kp{DdVFRuB@5b8)SnSF-j~KjC|k_FMQ6GqN6~}&EbnNchSM+B zs>hfsPbc?&^FR(1-jL{&SA4^S=bHndmBW@ez$sbacH^=2lk0iCUa%DtgS$|WkjV-Z z0}~wk6i`82b%aR88naUpyH11Yf{+#+RvJuI1v4-O-`?0p3b{K)?&uw`8RN+uVYp5dzzy zJneM#{7}VNn`8mojX?W!ES0%U33=FK?avMLW_kV<}uW`>3y+)1bGg>E}@zAfB-I&fPT^oA}WVDXe&Ru-=s#in#4M zV|H=^N9CE`x22LQdutlXhfBAa)0lmnUc*6c-p5n}C?$+7Q#2OEzcmp|%}6y{UPEpL zDKzHp{$5{d6Hh&s1CMlMy0 zKwU59m9NPqTKtqE%&t${(n-@G;t zn@_4->H8^MZzAU6)TY%kbp{tV9W}*|g}4Mp^xy=C*DvK`43~!AZZ(JaAZgOK!v%SI zdt)p`H&)F=;}+J*I5B8DwB{l)C?KMcq|w+fAdie?BzNiv;Jq1xY;MNq4WjW;2(Dqs zr|Ov&>;eSf-+{%E;$YaM?B%6#p!Xci!j>uu#~smPaX1v<9`WG)4>>C*|MDe^zgZ?h zZrrN^n+6B=Doa1w3YVw++B&6nagw2?`FVMP?4`$hV!jlPA#oPLEpv*`z)e!VBO0Gt ze?Cc)6Y?T?WUb&u3-P?Qm;e$c`oqX~FmQ`A-2S=jj=B}G(R#JQ_W7Wx752DDBoN1l zs|q6{e69V^4M*g?K4A{HA&{6VT`6gg7}0TD$22}cV_B9!f!jA)63>&9e7N`?Z6?c4 zBwVPoR{Y(ng}DA@Mz=FvE@~=;O<1DliSqd?2^F!S!U~;eIx(fnXR*CAWCdN?w<)j^ z$*#Uh<*Wr0v)`%P-KMAac~gWg)ffIY@7nfUZozb9B$Y@yyAn^kmBpf#B4PM3Rf94L z5j&ZY+D(A8%8^4K^B3x8+LujAlF;7?&2WrMA+S2YVgCjR9Ca6zgd;zfknl^X?e$Fy z5B-+C=jBnEQ11s>W?J~}23B{|5+=)0dL7yv#>z&0r*(V%j2cn|&Ek+Kw>`f^O->ca z4{IDV!;nqh5r`Iz2N&Ofq7pRTo;-7GqR|M{nlMI79C^iPtRmy{xvItT_T_E!ZVbgM z}bo9e+75kusx$o5mPu(bE!c6BbUK{sYKY>cd=P%@8c?xcp=k!g~F6kDJLKa z?i8Cs_2r>f-IgQE{E=gtM&ozkoN<6HXG{O7z5Bh)t8oP}2wYjq>kpBaRlSY?xMb_$ zmrvc^=X7wz#C>2)6k2+8ybk=>^{4x!&^!vKG+t0_Vc=7i?_GM0#MuRy;G3t4+y%xWK&JsLHb zDKb{5k}_GSUCf2~nxLA$44;rdjWW6D*B<ec8RGnAJ^rdF}m-)PlH1n{c#_!~Z z%`jaogxh^zev9Eoz+CH6Fn|+F8dnArSxmiJYsBah)U;}OJ%w3)Y*H8kG!7Lwh0qUvm*a0*Oz}nctcC1#kOjs`d39GsNbtBe z&ojK1rZnCWp7c?+DE}p$jW^UCY2Ib`e!O<#V>0B+dP8fRtPJ6jG22|veQHtYr(}6O zJ-xp7aRrdSEa2j&rryplsP2JTy!+gZd`73Tr0}8&cMd7+A3SQlXBLTQTGKGB6-*wZ ztkiPLPh~H~hJnpukl$mvC-KHzcO0LPx5`}XVRXaaw_C5W`yftUcgP8#(Ds8hD=>wt zA(cGbVH1g8MPG_95jg>~Wzt%D(WpgBXjqikPaq$%--^ZciIvtHBdM!oo~vFjGT#=e zFl-F0gn_G{DBA_TJ>&iO`613{s4HdP)ZR*W4?i!rrRzqQyw#-v98lZn*`k9CGxUjV zjM~f(RIQ|-h;`jy$q)kPf4{-MzKf5&p&5JOy{>E-8pe#=LK%q-Rf_EpTs7vK9#Ekv zd5;{$JjXZrdnMdes~|$*)_^55>rq3lbqiOh3p=qwW6stk8=;EZaK`{~&@P_lpY(yA zxmt##Lo+RXYUlx%LQ`>U8Ixz0X!5<{8qR$xp>V&oU5|U)lkWV~CvNoS{}SeR7q0=~ zQJX?AN1fA7Wl;}7x%KI6$+ouewT#&hF_yr$+-TLAM^(RBR*1(@XzGRxEpJa^vo@#c zZdIPRnPGba7P{Mfyf8u#Tv?uT=GS#Gc0|`II%$r_Wa(p;5z)mDbCMlE(eijBaqC8A zQJB^2-az2xdFRM4FaQA3<60CGXAh=hV>S{nfe7vh2R9fo@WDFsnuXxcXx6>3K)yB! z`U$J*KLb)?VDi-TvUg``o%)4jIO+4P{YUQ7W>EAtav@O(=N;Bgtk0CjKO`T2qlmZS zYwJh5D>O4jIW7s(pb!5{nb!Ejh!lyy(LS}4fmmIZ^dIry@yzV7DBzb(Zmgq|+K^dQ zwMZeDNcJD690~-CCEl*i2J5N9L}ckc|ujVl(dq(Z;%vLPOEC>reqE$yT;3Psl&4`M+vTu%ZF;pej7= zBzD}IC-Kj@Ovvsk{@3Wg_gw&j{x>oIOi!3mfAQ@^Xy+SBKkD2a(BUY_smoSMzYX{w D5v*pT literal 0 HcmV?d00001 diff --git a/docs/user/ProofTreeLinearMode_example2.png b/docs/user/ProofTreeLinearMode_example2.png new file mode 100644 index 0000000000000000000000000000000000000000..a075c36276a7a0dcd98d33697361e6328e53f538 GIT binary patch literal 29239 zcmb5VWl$YK*Di`AxVyu~-QC?a5P}n6;}+cAed7+n-Q5#( zFP~(4XlR&{`roGg8mmRD16DY&sk3Io94Je!&T^m}TboP{;MHac2*H9wT|A)*O@|_C?k|L9w|x60nZWVQFjA z@iZHe08)sE6KF%$Mj59g-m*FkftlU5`$ZoKD2P|f{pQ&}rxhAVdp=6&D`AUj))t?n z$V&b~WlBI>Y}>?)%qMEHOqxt0L(48K@;77Kl^J-5+}< zQsK2_A=>-KEKkEHTi38uBhU0c8QQN;rr)dp^}>z6Fj#w26aU@^e_|ctFhFy1raQo8YZ*cXY&zi71AM3g?#?<} zw;4ZU$hsvwSbib2v2I1fP>+7=x5;V#v$^ENFOof3Ov{p+BG#(`w6SRtwFGK z19(XZKD$85u=2dVWrB}J%}Ljq%t+H9*a02 zGnaFZ`9)SqiHpQ?VVDj*j`0(e7&dNwmY(s()$i_m$1ljDXJ!Uvd%c@g+Oqe=Es3}+LA0Tx-I=-QI_A(F5i`RqZUqRb66V3p|~oE=7KdJISEiYE&Typ;c%#SNga ztFN->i)h-EI(|%A%Lv5KnVWUqepf-ZO=%!8`Y;!;&dJ%Qvh(@M zVV5o8OU(~vwm@u!0$DZ?AAy%TN2@P|Zn!oXnqaj!^HvL8jOtuzKu8tr zIP?&vFD)Ycqs%yg^;azmJqrTP7}A;~QIFhukR65qgFlQ8Y-6>-gOEsADOca+kvcwL zCB?^i++Cx^H@QkmbnA1oqE|qQfvc8~Q9z6r2ULmlk0x>R=1>0;#O@BZkGb$ML zE+szkyv5asGI`+?FA&~qq8Q|CL2=&b z(r#V)0i7~nJbiOE3tZsshf%L z!78ITCyR(&#(j(50x>b<#x)l@H4($H1lG$hAXKd^Xn-DMKA!wXOXkur7MkZ&O8ezy4ElsZy`j!?! znHuicqcTG2so}%f9rQ@Q4_BhnkKSd8ntDS!W|9v=KC~g8hd5Ank{jbN2$Ek3Xz5Yd z{Njl~(;QP0GMH?H{s=*4ijJ=bn`s89jO~!rxkC3%TgR^A4o@C#pFS5~@#*~xEehz6 z_S*Wof*2RCwhGBgdFered@9@(F1F=Oji`Nt@Hw!2YW7)3iU`g&+%`@MTXvL|szZ3I zP=WgXV&pA{ilo4}75aX!>9R;?5oJ*{R*@XxwYwhq^jT{oS)D|qda{JJ-aIvDX953> zmy1MV_dIerr8PFZ(4QU2lJTf|>yVFTY9rGUTa5cGI+`5;^A%s%rYiq1x({o8Tw_Ui zG6Sisacq0W-+?ry$oCcgMF$G#GZb|fla^7cE}UB?j?*O`@Y9O(_E)&GwGedE8PY48 z?p927@#{+zp5pn|+PfFANKf=u091JUo}TidDTdm~{oywCjObdnlqLIb`tbsHAEsQy z{)%FbnpY6Tb3<${ehp;3)@zoUP7%lLce(c9cw=Mfw*0e}*wtPO>Gn2u@^ZAbyhBbG zQtAHj)6TP_q3AyTNY|L&8H(UE@uW%fa*$MwDp@Ikk`RTbvftmhL3`>j1x25N%=JEw z$d~E!VDJ4P%~GB2I6d&lYj*;)+vHNvfb?TJcii^vTz~x=#9-GdM5dYgVlGX`U1UfW zT4>GFo1!!ztTo@)LCE6^^|3)?$z`K^tluAkgKyl46sA}DelpA6&XN7;zOw|i0XBQr z>CFF)K}q#V*>z>p<~}qM55( z{>CyAC1rKh-x!H|e8qDsh5G?ZyfM1}@|Raf{Uv&IWw7Y+88aDC8mQET5E5PZr;p)z zVx~6_d54FX;&c!jLlfoqP&o=Bn2 zz3zOW^x8D(S-L(r{6iixUzaB_F-G}5viX3I>0bQp+nG9m#vHnaf5piB{@2!@a5q1? z-@twsxKH9>aWK>eQ842_C=m=A@cn-+yTSZSU(yyvT!eNt$Q9vDQr$VF;8 zlkcz9LYBtdPxD`C(Zspy%DzcYJ;rnrYCRpK%vW+#tvQ^~i-l;hct$_O{z)%jOdroS2p}e450Y(xZdwa*WDbRH7$8!I+;qk5FSSp^fh0UoaF` zD`Jd)?s_l!)tr@Z2FWk~vm4vsN+gZpQ&xCu0TCbCX!AwfgR>Vqj0f!5dHRmSqn*TKl`H8 zwM~rVaDgT2m*k+rms6{F8`pJyJx&>|}e{Ksgb6g6Ji=lwj|cmY1qd ztD3F0Ief6bDVc{DO{L(_l~aTqa{EZj`4u_dzM0I>(j`z19B*H47rLH1O%y54y^fe# z9c(8g?|6jo8vJBpyCZ(e4XBiBReaieXA}8@uM{U$n8u!(0NQ&d8Z}q9z@&FZHoe!q zdy32!gC04S>_$nRa`>TRV&lntP#zqOumVcPslR%fCeDe-^^q|1C*R%_S=GtBQMI$;A8`ruV-< zl52y%4_kJ_;4wD8w6V2rRJk?3n$FIeOdi3lfAsV#p2#BuDy&LGAAqJ)|MX3#KoZvH zMfZ}1ZfJQLPnxX(08sU@MLr26l&ybF=7UcHW3ad=~!+0e8I%6~b%O_FM4G#Oxo;w&eqOQUyLilg z%0prBe4dm#U(qVqsrIN>3mVTOt1;eR1;yJvO^%n-@#|VZz(7{r^BPAd4O)3F;^=#* z`h}~`!PMGM*(VNDvBs)7qm1I!txBbfT%2;?k!-O6moI#UV?K)3$I?-Mgn;tJjR4Y* zj^oiEF{QN=t!2cQUVx;%=P$Ha%r6IU9;>YmX4XfClanPu`h@#AwE0*OS+9wfb_)TI z2e)AG#t500b&jD^$Epm@HyqdB<##J5Ol);xC4W5CB}V{uI*7Bk8+$Dn>11QG&lM*` zBl(;NZEQ0rDKx-=wlS*Rk9bDVm%t3ET*cSWqba5^Ju$M<<;m!JOcW3Q<*sZBFx;KF zJ3LFlo5=;445D!)v$Q7AqR<{%FhyuwewbY>v%5SKJWo zqt{>QnV~xl*oyB}=e_uj8XC57SWp89?aruYH-b_y^MN9)9NOS^$ztwlwAyJc_dE+8 z6G0{hG{?P#A8+fI4;F!1*>ur**ddIGb$pqgp-HAU^=^3wuyuM9%!RDS_A>`@@nWonHxf|2tU#ae`Hu{{@Z zYk`q?yAz->qL*NhFn}Hq-``)qv#FNgM41?D<1Kw2uD(e=u?~5YPU-!E6w76$Ne0~G zsuX#~9OZfK9cIAaH7lz1Gf-*FDF{cOWGc@A#Ssfg#}IJAorv_)nly0V-sr8p0wnmK ze$Huq&zs*~VG16&On)~&w-L`r+U7;7Yqm#hW~z*`P$P~eM||#${2Aqw)hj`eK#UOd zmt4z0fKoD;7+Rv!Jsb)#vNtg-5{~~f`6vBgd8+7>@1*S~EPppM8<71B(r|EcVDC78 za*SToo=gbD$zQ#qHobJJ zR6pL{al5ouGQb`5qvBWS6nvHSu~nkqy|P-YR~Yh=ajqy(t|9^GdbK{-Nv^?iGvF2_ zMLI5f{;h;DoVbQIY!WVOsjdB0Fq3@r%Ekf_Jf@Gcs`Lxf2m%ftjU7T<8XS%afF}Fc z5ekk5K|*{yg7{AZ2?7GHZ5x?SnH)m2iTifUAqWDwc@wz}VJuw;$sc3_fVDYF-@&%1 z{rY=p)qMgE9|ABWjF?n9KHw#h+vWX2FJc=fPi0~{%xyG_RY(o$Y};=N zpgqI*S5Sopfm^kh)DL zka8KfB6Tm%<9Gy$b9b2Ux3BUg{(uz)LqPb0-f=h1Dk?x zD+2K3(w&taaY+DWB%x_6)4BS9a5~=A{&NRkGOHiOb2%|d?1G2Sq)cWcALs$c zC8Fav?vaHj*$(Abw1go z+!~4kbVf_`U|*e)pW$wyzLat;;bZi2$UE3xTBREka{#ljOIP`NZcM^zsk~WClFZ({ zpP7a)`!1bK(s5yKcBZ6k0Dt`DBL{8;Aw zgRl=%6ckry;!OBxB8V83Zd{&n@TXWA^3cttWw~eWX}#o{8(lyCE$s``pWv% zI9Wvo4fx-hzdYCI9V2_bTdHDwdy>kH#a&izkT>1#VS-{++NjqBzP$%CCd&+t7lzWx z@!CuH`)Psid5sXrJ^enLC;o>zU>y18&(@W5~$<<%4Ut-)*E5I%3SHv)&z zH()b`$EUReWM@8hPz)st45Usr;(E9I;XxFTYA%^)P@mY)LTG7OUhtxWO$_CSzy~4q zg9uih;PC7??{-j3F@trQvEWPYsTp(1{GTTvC?E`{o7FP>Egy%*ui5B}kzRdZtI(s? znU-ZepI|iT^rhVoKJ>vvYuO9`Z#lqTfmbX7_bHN7{q zt&l?6KRF#R<41bS#G0}F7TUS?5*K^!9qF^I#OM379F!yCDd`e`p36bPGXWy6iqn;r z9!CITwnwEp!J}TnOeLbnKAiKepX`qt5<8EVS^m;-ok;F2B7G=zb|X2e{@SRkhyxPJ z@t-CKEGVe3NHZo4M$fvp>?b#kldtzSv%v{g&0Z1MSiz_DtkkFFlaKdvm4ZtrQlZRe z=0o{Q&Jh60vSV(XOUWA&?QrM;8+bi&&1`k6!!tEwjZ5zZrp78|FN7X4QIr~H?m~qB=9|~o3MWfU@Az_AdsFUXTr0Q;CGv_*oKshar|!gR z<5YbLj!bcGf*5rKkJs3n!?QA;XYsR#(58_AqW0@2IPJfkqQ+oj*Hl!`q_9Q5WMTl~ zL#0jH;g3~Wv2!^vAb>KJ&s|&3MO(6B{UA%}f*go#J?Ts)B+y?pZdK?+@kcj%=nR=U zpMoMhIvObU9U`)y{7I@Trq!MVu&EEOe(Gbqyp}0=A1yVg8QfqAEkI^Q^Q`s8S4pD} z-&?6~Rb7iQX-D!H;MywqM1Le9 z`al|NEb=YkhE{2bGkPZkzMKO$Uk*G(E%@%b|(w#1l z5s9+y&(PdwiiHQQ_m{$)0!J3aCS6(*G(+L~ziq$5%0GXh7L)+QrJjfqXGIPGhHC|d zu=d7+Phyq1EyW)io#EmS@vDSI8$B^oVFvKwwNDt#DumOj%#Y(WI|YAURq$%$(IqXJ zGk*=Eib18J8hWktWz&c@M3Rx^QSvD+Q>2EsI9tAQMm}C7OvZa zOGye@nv+LkP$O02ja&;R6AIMQCS+w=2?Mi#b9M^{VB4}29k=5;@xaDUEMVce}FWARE%FZhbXoEnvgJMPpuB5vH+l(a)SRL83o zvf(X))&9enXZMQ$zz6Tys+;PxiwbY{?cuWpykT9sL~3Sj6a-7hi1^Q)F&!vs!-u>@ z#Y@)Kba(!O8lcn!wB8uRvk$_|w$|TnR?39dS#JVqNi)PL-`xDMPbmZ%56{+cJf{Vf z3p9X^5QFq=S?BN^&>y%Id*Og0-k9(h4vhN7lheQ4n$mxNu-NKea1+L+J@zr}k|!v| z|Hbxwpu54_alN`dhYlYT1&cG3C|a=`_(ex{#h=-$tpy%L3G7=6Z~1*3f;uai_Y8fr zmzw~oIg-btRcDlFlJ{d-c?NCUT5fc=_6uU$4p>*F9Jw@wwtpQdl8@oiltiMFXCW^x zFDu3~P6-I6q%rq9O9=6CnipQ%&e@UQ*f6hpm6>RCaFX8C}@ln?nHGS0s$-+U|OuIp49e6!e0uT~Pb$l5Mo+;SSglZF`{&gBm z#(wNhyZ9wu!P?OpjiK*{Gd74lAwMp!23bI%FQWFUv$F9}u+fTWkke7_2 zYY*bH_wF2(cJ4fRe^@)J)eD4jxzX;KM>;OlZ;388Y<>CG7`unka&9am8us!F?}8VU z!;~fi8{tHLXvgp7#3RJ6lLVuyuWo8NnM92TT`k=LI2$R7Ykm(i!rEpI=;KN>`2a@4t8UhSkwOBK6QP znak?4(4#C5>aR^&C%QRu+cLt8G)J2Hz8J*5c%}(CY+P&||Hd12Go8cEL}Y4>3CM#n z@bH3hc#i$yZcl!U^9E~ZBl{ah6y~@+Id7i#E81jNEbh@tMhr);jIkYWjMD`37}xP> z;eRCag=w~1)2VgJYN;U|iX|@itHsAh6H3y6^5gnoOQY7l|HicQP(KGCKvKG4*MeG@ zWpA!oSn%#~EJhvrcsT;90z%TZXss`y#!=@wk*D?w%9_1Yz>FX-O5g1aR(*@@j@o%> zRKNomz(l{zg_B^alp`l+aa6{}6ifTVO4p$EZlw3d5~8s4DJubbu_nxE8p+eE8_IRH zR}H_k$Z$F9j0kn{Asiv)-S@gg$5e~c1rg?$9?zJ#vZo_Fx%@S3Jks&*h;=x%M*Gga zrCW#JH=ng<-1~`to<3%HO;L5NdW29&??<`2thT=yzo6k|)q5zZg)EgVMu&X!fRVBz-_Z^ew4OOC=midPz8g1cx z;-*n|W7bFYGHsE4YV)6e?;@m0g>PMcQp|-TAgw!x+dp&XcgDfG(2)GjXbHP#Nc;QH zbp&OD`&eI=9!^&RUcjm^c*D@g6#&psQVLp{MGfT3KjMQ|xRS11W71l9Qsi^8wK5{) z2Qm0PUl>SFhG$*{=Oq-&4`hn+R)%4~I-?!JX6p}U+z5Azvgu2oB*5Q&N4!>B?eLgl z-0ih74!*EB*sQT0Wk5$nj6y-2UCsQV|0Eeh@pgl3S8`%xHiY()e-NKPH+jDu4u4gA z+5cK-EuFAxEY_G#aKyu%%{R-BoHB@Hm_8Q5aIn-v8)`L(=J}Qu8fZY=F0Q$d@62Jm zKmypilH(qb-rUm8aJ+r4<2@8CJMc5oS%Da1GIKh#JevNZhJ8qR#gLV ze4EPKriHL%Frtjk5t){)*S8LOhuv7NaYCWtS9-oH1oa2vjfW@`x^*eMK>%Kv_?0hk}V;ZErIC9 z!e0a4WJ8^I>*FaES#g}I8I=>)wDVOEhzq;w2ou(f_0@xoyW5DbrU1IUNHyLwO5~1f zhrC_fpWjB$61l-u*yS#6F#^Kcw$|(bWeD_A*!6aP5%E!FpgD?Gy^z35u2^y&)f@A^pR|n^lMtU=_+-HIJ``m(p4m$o_ixv2-PY95%c1Ig zjf{DDc}bTJeP~_&x{=+Wxl3Kv640aL(y|DedP&jh+%aY<{E}p!rFq?@AKHh4!?7U) z24IOW6qjWl;BmJWz4dy1>96OG>&SJmw)JC294s-;hS*eOS}t}--m2Hh*bFEr1#~~~ zWq1*!lF01vcx8Iq>X%97%e$;h_`wCs(42cM=<8V|cQcE!3wR0PNzw zkt#!I<2OlY3a->moe9?ap*y-5SfkG6TVQTJwaO5F$8qNB4^l(g}yg}~QA_K>+#PXqx@si#2<+piaOEkWjdnVpe&TLwv|*fQ;b zZwFOj>8oTQt3FaW9I(JGmmfUqm%LZ^6iSla{=*%j#deTiBf@WuZUK?PD*EVl!{YQ=uOV1vVQ|K4V`F1LUt*6I5w4-(w{ZywJ#imlxQ zURFG(emqx$?(thfe68Dk+R_F}yY5^3yFRt*)mGW*Ksycgq!L4M7zC-R|JowLZ?D4x?Sl|aL~QK9OJGuQQw;z_*_WADioGh3NHrCWlX?q zk`!I=fFf8Xj%05y)v)+fckRaXr836-oc7v_r%>;A6d+G>aBS;)F_db538ThY?qj^% zT0tqn-v}=`==I-RmP-eS7&W_)f?Xg;k}RX~v>pu2c|r+z9>LMs;?uvp)ysdvpK?`N zLX+WdoJ%C(q1ORTmK@)?z3dsRh7VF^S`5&rc__rr8TX2>WSmM}nx8BnDV8;glYSGQ z|B?0danj;Y{Mv(30;k=>{BiTiGv3<7(LiQZt1pE8y>(u<75atjxF3E>qxr!Yo>8F+ zC2_H{71wkH8&2D+t4b#>B-?Zx+&t^f+ueb>N72FIGs%=xa*El6s?PxYl~JF9s-sE% zYay3?&w9#p5vtg=PSsEW>?!ntf_&|dOo2df#SBYtMQuaP_r&&3Vg}hbfYJ3&SJG)@ z;y3`rf6x#R1(NdqPv!pvh5v<&aDo4bMedRKJTS!2B*6nh>MUW1m+F7SKuh;T za-MNz7CL{%%`>az6OowM;~F)K{CLS#yErEy{?{gq68_CC4oYsvufsLO@G>Lv)^9}V zt-L{1X@Z#*^Niv+AMo^;{g$)V!BP{e_{fCMqG^A%5w1Jdy%;|4e&2h0HuKMX4$4R2x)DLL=h96St z)GDm5BDXS-1|v2bvnG}i2;=%_U5#1KpXzg?^2SEpZ8eQvudkWmd$#m0%z|G30l{4c zog9jD9KB!*2tTQL{gEEZv^w6cIoylK)(6*Vur~qEntClKazj=SA5eXL%k{d%52*fQ zt_gSMvDt>TRb?AVR--;1r}0pe4>519!6zJxH~UYan#J`<@*37OUYKlG_B*eoqvcnn(=IMtY{14*!z~B2In>BFU zu7*0^;JAr;M#e{Fv|hzbUXaf|mONb%*T`|w!;flfdH#=AR^>iSzs%(1d_B8;T8%g@PO#g6SzwM<{XWG8yNv?GbonAN*Eq2D$64iN&GtXX8a>WM+f5OB~+-K4ZqBdi)w=HP!ImLly<$Yyx95*PG7l~i@Y)) z{!XZe6ZW%A5%Bz`X1VXU-XQ?J@Tx7|Ty&ijwCZ*Dgw@jj95;*$3BeYnZh&(0!!`f; zM3i$6`)URahc9!+e3_YfEgG;dO?wdcR7-II892Ro)FrL~=s^MG3i~`gj(c0pSC5Wo z@|2OWlWW>FOdyGoAd6jRvAXF`Gzp^PkI(^=;#eZhuF<@n7~29@p}yj_5#csmRcBqn zWvm2Mb3lV}=rXg^-Iwl+<fp=>Mn+$<&P zxWDVyQxvZf8$&NZLL{0xeq?rM z*CL5Unp)VW=ymt8T+95aXy6Ls8Ir9D$XBHbz6px1BOckuWH_`x9~f4w(~HB!XyKTh zj;XqY!Z3}lYM0$pLc1zcFELm*8t?CyOmIww)3&O|(lb`ZMHIYOpz)c5e?$>!Tbj8K zL%UKFZH=obf%d@-12K%eJpT3-w1usG(gf6qyP077RM9xGqeiS^D%PKkU%?R<(M9US zWflnC-4$i*uyRY`0$6rqogFW}--dJ)nipbze4Z0jnVsguMp!2(4ui(Q$G?uS@U0re zrT3ag8cT8vCqF`VEcU5`hR;ak4GlGTduNUDaP3@S6_=QdmOXOOnF%{JUo>IzM`hR} zs4&JjrUKan1#9T%jr%y&zH@`=?!NABcsc0nTTpN%<6b##J*YiX4W~<+dbn&lM9<;V z7nJC}ymRtE(@85P9?jdK!I_q^Y~{j-{XYW^Bt1AO4^&RXw&^Zn4A=g8Bqb$@Z|^!V zZTukIdOl@D36SRu+TXR$nPnxz6_S7`ZJM;%Hqr{aBM`T`c2q?Xtk=wkyaGl7m$W?* zvQs^N~fk?6E}J&C^sIIUdJ@l2yu@>`ULd$cs8M`Lw0b~SJ)uA z>F^N~ug3zlwL*l)TLf*Zn9L@PMfIA<;H>&YbQ~Wo^v8WTZCRoI2WB6w2kYh+WzzIF z?}Z|P4cPts;Ja;`lilFeB98TdWqEpSEq3E?^x_fN`>c#%HUNWCK>+TWj*>`2tk%kF zZgNL9Hu1QgHlh9vJI;OfFx*}lK;>#LRwI#ynF$sBPbf=KOA`(3^k<0RVB1!0tT?sx zuhnaH@Ov1B(GB|DeIi9}>nAe-h0z^ecl~nT<635}-J2VXoS&`016wMLuO}*(~ zzJ@pyAKs9uAq*dA&?!*G7sqjTztJV~nxv6kAN&b#CN?<{EuuG}Lb97}+O9tw<+=Q4 z;HELXKZ3DtS{_IL;IkST@P3l34`8Wi_AZha5odjVoIgJw~z}(3uKlw&Q zr5bp-i`!jy);s1;1SGG)0z|1Ovo1{p3_sfeeDe25@(5S!PWUrLl?IB+eeRe?jszxl zE5tQD5<@B(cgk_uRqxN6bL_Gta}i5ekGd@qug9 z94H6Zwx{jv^{R+3`PCR92BJLKZ1C5UAxFiBQ@iT@vWE4&IPMd?%b-3@qsH_#4|xZ2 zCSf826!dC+?&@0p0u$_Ww_te)J;%BvV`cY}7+3j?&R8Rp56;5()Xt4iDeaEX7UXw8?CHXy&_8(KJ<`-tXu-PfjlQ(<8JrmjJ@qS$HD8%cnyF zwYsY@aTN3qWQc40COmJfsGo05?CI@)f+#2`9*0EU#Nys0DDiuw0nma0 zjOTwNIqA~CC|ztx=Q-C4M=bWO);w)l%%L|ZbMyK@WSiu!Q zbh7b8Ie3Pil9dph3UXq+KZz>HhFW}JEiDzV zK6&d^hrSfv8N}-G-LssG>w4S7@YB9}N#C-Fsqxqs-Xd>aPv}E`zRrm z`5y&A8@oR8qtFAfKgw6|$1JMxQ2_sjEfv@NUqpMz#k3iFu1tq*bdY)SLv7=MccF__ za?-TcdisoBLQIxsm0`ZwDwq7YYA$ud{THbc8BQ*K5?{er;e7EnBrhsR)@_#xVuzXi zpBfy0z-G*rO5bKM)sb{16M8`SpF!d-L=QbS6wgk3g&lEaUZjsQ#?lB#7)^Y) z)>+`mUtXDGwR?cq7ff+tZUU84pYKm9IzI)6a+O~yyOgsaJTUdj`IHs|V9JZsH4O z9$&5>F!1_P1s?x~BwB9|CXJ&ehX4(10b(AUQz*klgkpKDny7!A!#W``rJ#RX3ivwi z{cYOg=ZCwltQXZ$oh57B%omR;UR*B;byAf3$JTBtmI56Pu8ZbQwN*0aNPev=0@37F z7O{g+i!t({owvqp4O8z2vCrKB!p4*S?ReVnzigSPhEe;T4Lv!ZpO7+eBUbY8NkmA^ zyRE%41ieP}&Ly(U9^&cA)PBT48z_70ZNT~LP^Y2jjXgR;@OrCblq z@^Joit(Z_0#8a3qTWa-wVuqPRwp_GhJ*ME?i&F3dkT}<8wu{x zes&c1AP732HE6W8iO%u0&1fVZoS=k68%8h~_z~9JSZXfn67=M~di?R%N0jMgi{5*N z#hv1zT&6VFACA(Y=WLk<03%|Zo(Fki*d9MBR-x5=LLE(Y-FRODPE)i64-b_7mT9-G zrT?h%@Mk!=%6hhbn@i%z4=CX6Th{)DcwSbbXteoBCrQ4)_dCma%~Y8Fk}UA_*TCPN zbmuluf`x~(4^6?!Y{BaZ+7+bpLfS$e^SKId6b#upT96g~^ymQ_c@es-o@I#`g+x0L%c z38>iE^z zh1^DrmkQSn4SDlYgijF>^>U=Vy~$d9(qdFzJ>tYW43l1_iEO$H_2xduk@A0Vhh=Wk z;kb>Q&1JTMA;n*;f9fVP*PDhm+gTigOZ2-nKZ5Z)+YdKI)b@x@b>MzG;#7&Zn?HZ{ zAdZGTp&}e13=0HR%vdyXhNiWXgdGhcEoKfNUd18hx%SoY7D(|`%VX3(tZ;i02qhXa zkNgdP>1L9i5C+o2X&?CsOmGpf9RUp@5dEU~|6UJQTK~nmmJA(1b9}a%J!wnUK#zz- z&}Qq=pm>kDn^jlt4>aj3rJw;O>LBqwZHqGD-679fnk0H1R)6&3wd>PF9tutI5BVFwIvn00K7VoZfK|KV(&klbRU^hiCUG_Uq0Kd z_)#OaVED&K-1B2yR*@Uw z;o;#g3UU-3Xr}!()ngW6Vim(LI{(!vk)t~JAs;s*f5W#s8kD@Pic>_n8<&Po{qdD= zE4>_ez?8`ccD`t&Grz8)j>9heI`aE8f~2TS{|PsqrX)CT#=`cZ-cJr(K=}QSeVomB z+ffK(Oc~>@mTx2L$87KsuRP1|y8j8-rDuGtl3l5;7k@TR4p*ZglSc<<^ae}y6wrXo z$(dmoLGx$?UAE2R){BaOPevTPDD=q3=3K{#4X`&AmIM9KXZJbgSN|VuLu4{xBQF(+ zH$EmTV*e|=t0L@6wvMN{{NiKbdIlny4+OBOg+nLD6fJ3vtuGq8TsKN(|8yv#BF}6t6P{UyK4y@ZQ?YIwmN5h#4T2d)naS# zO#|{HdG1$y>9GqjaKcS_l1cz&Nsi6!*sTA+XuHZ}cBHx1JlkD-L?gGCahUU?FwC6K zZ=TsV-m-wdu!+uFLSm*Ap=J_7%$~;k_;ohSs!4#|!H<&eP%ik5#mkL^_^VN^(Mv65 zx?&1E0A4#>3{)E=uO%W}N?xH+&ZUZQRkvWwgabKx6@e{g-IQ-zTKQFnfmT5qSfNp< z0VmM!PXGl;PAOK82j=FuKLyY@nocYl1tLWV_c-m7a?mI{Qct!Wu-|tp$dtAfMNr$& zB>~P2hhkutc8;HL-ql!CtYronTE{Jz-Y(LV&5ErTmR**;ra(fsBZr~N89qO?zO+r) zWme~)@6#dj^w{$RFwMu(=+HK<@pi>~${#d{%zI7VXck;_d%hN4^RLq|pZ8^A0k4UC zB&3iOr)a1Wh#r@pw|%U%CMSJBLY-lJAunqiv)6AiTHcaTL#_+9$+)4Er7M3$4n^bh z801lzrWb{iad}GZ^hG|)v`h<`7|h2K4f(w;oF+uyW?aj%G)1GR`R7VCw>G!iuPQ9( z=;u{b--AmyB`VAXOJgs&wU3?|D4V-rls8J9l-ttx4J*;tFtLd-em>nY)pOa^_{J4m zw0JbKc-oyrnTZiiqvx_{Q`^-mbnk583dPea^R;)!0a@mUr7(esLe??V8w+}B$mCcnh1pNa zI_0>D6mtXmAfc`>c*m;M*`4Xbj30D1^37SD%>D``@a*^0n~|(&z(Axxq>sDe101_3 z2-2Sn69_>Dh7bk8vqPZ$tA1*O@rC;BqH8BZ*CXRk_H3sRe<0pJFaEmZl z`b_in=!}(%{Ky}U-OZ@52nm&10yeY> z5;RUH3NSppLVQXmgN6`;fe2Lm=lqW<^*`tTuQ>Shm|4@m)AFIq`9N{bYnJQVr2}$1 zgMkr_$md0Z%_B^|4(OM9oAO!txJnrffjdnDW$lixVt;W-CbMU3GSglad#-* z;u4BG6n7`MoY3!lzkBX|&R;iw>?eEn%&b}Ol36>+e)F>w#wKau;gp~~$0m*9XiCc@ zwPJeY6$`fgnWmI4-lO4=KMuk9Hm^C5q#xp2^vTV0JDm7~;ZAR-;P>j{cpXDM0@IMV zh2jq_7TAa5HdK5}LLWb+gwNcKFR|$G<;5RwB_TmAyB)0B!b*HsMq3}J)IVRsn7p)l zbTk>GQ)`_X8{n^OXlgr?^xcRvr&br|!%h}+yx?We&?8^6pGt{Cv_@H1A7O)#VIKt0 zk5-#C^x%g9-{7MYcC_6dtx3(TbXknfm=Z=#)Z%TS6)kcM`aW%y!?dGTx|H}mw}<@c$J8>{T9MhoN~$qerPFWR>W-Y>Uq#-}b0zD!7;ZX- z2(^ib8wfzfZ3-mj`2;Om&j`0N;&hbdqMLBKPtsfvJ7;^BYL5BBJ>J;i$bN9fEi+Uq z@3ZSDFGJC=mckcCKyr>*oMM{o<)FK?x)VOq<1pMvAY{DyYR0#hMD%9Mm&Y*fjhu?H zNZZ@DZ?TEC*@nLq{4h$p_ZBqZWhfff32WHUE8uVQiX|{5*r{*sl&`QjOx0Hz-~SvL zPE=KqY6cP|&B_b1vXUwD{+c)59wiXJqH=RF0~MqcbmQl*5}W0$s&1C-hph zEf%tJ1eP2X>)zD6duYKAxWh=6N(fWMP4@Abxxc)-twQA0A3LkzgF5CV`69-c#=QfQ z^C15qN+f=TyjiJADa%Gaj;A~j7F*Cgku?*w)cYX!{d|IEsT34inlyl5BF(bbry(8;sN@lHI|Ck=HgvcouBuY4PY7VA_x zk8w(X_H2yH6fO4q^QuJ*;|tPt7}&Cmv-5V7(;Pn`Ng+88M6ToCJ>uy3uj{W^NpiPS zXfvt{ltQ7f9$?wV&%}l+PrzQ6Nl*4egy-G-4@bQe0=(XBB(*`==h5?6MQ}Pq6&FVM>DYkJF7zXfu0mDLMtXdmlwZZ@M=#A= z^iHss^h>^5y(Q1gy?7vYz~^f+{q|EwPSqOzdI$#TgK!7DaHW!yaEJ5cQ(nAB@E&57 z`9Sw*)Jt}95C)Q1Wh@RdcK-2%-1N5cS?xfX4F2zQ_3yTI%7FBRJb;ZGqBrkmJV-7+ z9XAtfw`IHkihQ7BVamnLYqf5FrL-=AuwMf{U0x6dZhj}zyDvoEyWY-6@M(omFy&Mo zI6npZ3FzkoFzuISxmV8fe!Qxd8E!h*F(jd=D?x&Vh-hVC&Iqz>L!9%A)a+XJWneycTRSBBF z|1Rg9DHr4gr}?Rk6X>?R@gs$#FoAkLToA^~@kEc}70y(W zSe|7twMwJCm{hn7P`urwK5OCdo6;Ng1@KVIkP5SxEDn*CJUyIeUJ?kG;rPxs*pre^!6DYt|(lv+)SbKiY~{+iW7 zn2YsE)dhjBM7v%-V6CZq+;&DQ=wxh>Ka)E6`jY7i*_3gE#Xj2ZTD|&RjZ6=O*tD} zCoXb$T-DEX&>iqAkQaxbN_An?R>cC35G_jVlmb{Qk_bb9;`oI(8M%-mroW4ypE6N}rX;w(arW0&{{cJz5k`3XD)WC7 z8~ZARPdomP(Wv$M==6wlw;$EX_>s*g)n2%@x3$FR>20!Dyh5wSQsa z-)nf8-p4prlXITp&#n#U=zrZLXZdI}nZxF*_oB{T$&_=%OUGLcXvNZ6)Tm~8f^Ei2 z^U?-I&{TCS*=fy=MzYU(>P|%cGt^#^104Vn_uaXRY@Dg%XSZq*!aWzikWW`W?e1YtAKTzt&=pHRsa9=IVc(#oh25G z_lG2cyw%ypfw0(^#1)OOv0)h<}{vIojF|Sl|+7kI!!?S%Ma2GTNaU@+9B5l)F*T?8?9A zvh4=x?YN!H@(OtgXIDsPc#O!O2_Eg>7|d_9%5OZkY1AP!D60Y0(K8-DC2HjS-ealb zY}TjJh7H7axjuca_BavNo{b>ww-Mj;$9eUtMj+72I5Ekpa>hyHqBd8%m1ED|IHa;M zo#X`Sm6gXoQr-1;stvS8Kg{OoabWehj=rOVr{Lu1MJ4|OPeaN|ks7vhFH|?mvEyMx z=65P*^3&gdqcb3D)nPL(?D{?6=257eR|f-zh1)HrgGmf~(_zofVH;(!Q0yHCdomRl zV&SpNj9fI$G2Q%JbeVj+&eN5#fS^Q&i1}yuWE$RbnMhjKLvI=4qot~{VRGINz%{^F zues&uvOmZrZjAo{Yx@~OPh&FDFQq+cHlGT-SCS;Oho;20sZ=Y3uJ>?)Yct z8n1rnm>rI*zNf7-vg0bUL5FEx9CPVd>ad7x=(k`k|E$&o1M+Pp%pzRLk#XEa6S57= z?37r=r(Br2*WiK>-WYGh5nyvC`4< zrB;%{YUvntwmkmmi`wj{OGuJ5Mh?gCX1cF5UOL+0-N_++YH#S5gqV|F$5<$XvKyQ9 z-8r2uX6XkgQO=vr-Z>BN&3f`UA~D7CKVyl?gI^=S3ys(m>FS+KdSRG&88DccnawEs zr)O+GL-i_I`<-xqws+y+J8@_Z81rUO%51)}knSjJ{?RHSj0*)Sk(~P|L*g35aa)aC zJtQV$ia*FYWLnt1faVda=BWJ>y`tA^FR)3$Du)0}x4)*XrHC9<3dL979msRn50CPj4d;)r>*8Gq!AU%_G(KnK+ zH>&nHeba@cpMDWEvZVL?N&D0$AaHh)-qqYopyyie&{?@9MyMLri?z0jj)B4UI{zI$ z2S;*HGD2l*P7!$&{eZXYf^*dMLHVNqj*6JD2GC(JGW`Bgz)wjW+Z6s*1A3S34-zV( zM5zt*MGZW32Pl%MV8Lq(<6$LQZyr#KG* z>M~Bkd~5)0nbmopl07BiH`JCBIzs$j35np1sdU*XBEJD~?9Df|C9_!^sjaYdHNBy3 zy%x{ie%o=W$` zF6v3knM3$%G|L2jei>}AJS$9Vs)GCnoW{5NcC`1) zqf1%lsSZAMc;=@&*Umg%YqE@ErtECvaUB zumI8-m~cBzL&f}hRtkna$WUb>>#;aRQK+xK|BoEHg7dwz4Pp;cI+-$d$NX#n)b_$1 zqZ&o8&m=7k|!Vs@C4wXq(<6|a zIh6wXp})}U6Aj^GiJrRjsSQ)c`ExPMuZr!W=r7Qoqq|=%!Of3?a{`&6$SMePP3g04 z)mCJbiMQD5U(&}5i)w=c(7!;RAir9I@3|G|stx4(7Evo0MKIoe#1d8MiGcAL+}clH z#iO_qT5<{5mmfN|M*C~E%xppKfGhXqY`~+6B2?-2z@-s7)RXR3Sv&#QJp7OLZ-`KB z@nN7P!#2u&N(>Dvb6RycK7!B_YVAsv!pO}tk*Q(F^$AfLH*G9tl|5YF8?(C~R8xds z+;gCAHwp%2B8u8qUli%$LKDf3pX&mOl{Ihd704yZ%;y{65}Z@!^5xkZb&KZc)P|KzX7_*GPtV8JodppK}`x%DdVQE(5}6K_?1e!#*In%eTn1M)My3%$AP z$Oya30cI|ndh8)&4&+{6Fq9`bieJ4qtbLSJhNA{k2tK0~T{NEme1wupKqwlZo=88i zI#LL-c_X74*HiSYf^zufh)n=%E)(yH`^#iQJ0Mr{G_lR@7qqf*tN>oZuUaUn!5FM` zi(z<&Hi7x|5L=$8b$4Rua*F^4Ld$#iQYbbTW$ZA0eYw+P?++`Det3DVlX3nWPo; zmJ=E&$7sUtNe*j+#ae}ar!)wbLvpmt54`T&pRI=0=SjcHd3DA&jwH_#oZtyNOJpzV z;%*Po(%wA#4IeXg4YrW`oiOE00GojRUsuh+kd~AH&KU%-t*1L8@jOK>7*(TnjyOE~>RHZ!i zGG=mv>1wz@oU68^yoS4TIYCX=V+WH6oP1^;V=5>wAK@EfQ=KfwsDvsa9CX-Rn|g~O z!G2S~%*tz7v90fqKXI4pjec)F&O{zDn%vhbwCvq?!?Sa}3^%X#7&0hq2exA{-3nTv zX6BE~p6R%=eB)xI3e*ik z==$HQfgd5zn$3G~qu^0!!TIXbGW!IGM53yS3@yUU@|+OGIyy>T z@PHyIrcQFaDhxxv^$sifM%7)d8Rf%o&lEe@$mVH%)>mIBa|^8dH} zIE_-HoCuung~P*l|9tXf^ZPZlx_Gt~=8`XxUgRQJO$KZP;Z}cC_BDSuX^dQT)=@A8Q7a(qD@pzaa%yV zMAWZXCWxlT*-}P7{-wl+_)dEgwaFXgy5|Rhx;JE-Qq%A#V<+Uikk5JUz7K%IWgjKA z9fJNduoxm{gnYhqW?{)*@wm6NE)foLg;d)os|01&p7E04UCYV(LTTHHP-S3Yva^<=;rf_}XHul;0>*i;-VbXy{dH<7wgIBDMN-WPh0AFa}OzqNiVTUpzEG%hdV0 z)*RmZV=(ao!XX*l#+4rQVYG9pXaGfy!MEm;jD!qg_Z-s6cVJfmKCdL#Xvr zLL>evHr{0+t$kcbFs`UsX z3*ujXr(ia*?AkB4Tw~0ii{*{w12Hz#S?3sV-*d93l)sVw!c6&z6hyul>m)4C7gSJ0 z8+{fOXq!vzL!dxbIAJ8)*^p4-bdg@n@Dt7m+^@-rcWq3N(JjoC0J@UQa%Yk%F3Sfi z^^PC9MXTCv!Uo~EY}gkvJO!^X8d)Q@h|CH70JZhEI%tIFVC_IlJ~YWG-m7y>@o?2`{VlnisJ#4J~-Y* z0gf-)IdOMG;*8ODyP2q7OyJ~*^wd2p@+c%=7}XC^xE1C*~f*E|&42P19Cp&=dX6!V-AgVYot%NLGMK zYBnm>7^wFwG&W$l61kY0c>Z{cR^SVS(5fa?%E_{c%_44yg|G=jry9qWW}Gpbfa0Fnt#XOtubK5m^uOlAXp4Oj5D-qGX4+5q zW{?D1YnZE|IYYKV@oL_has5b;bYz77yYgM3&F>0gp3P8EJ>~-Q#ZM_eK4_KdMX$0L zK3C;0aikKos5h`k+uG;DT>3nJn`*Ot4ygF?*q-oYudZrahfxcU0c#P&6@mk%ADO&hH=n_ zk`?LJOx3S}p1o)qfi@c^pM!m?j|N*kd*}kBcZBQ}8q9YbJ;|wO>D^yy$|3>-XYuh$ z$S2W^HaGj(K6f6S6qf>ababiIA-9JN3}Q^L5@P)jmkH`D`1@VCe>bSd`%c8w2*U=U zjkW{eo|H&>o%~Q)jx>3_tywlULEYxZtwRQ*+X(M|iylprJSfnlFpI$r{K7XS*t(g( zd{EIhiw;BDJZ3uigZVy@%yv)n)p483vP#{(~jy#`KezwQf92)DwQ$dYdP;B`#IqlBdoi>Dny1)Malu4b44^ zxx^FceHSl}czG8G)ARO3)U;aUITe|Id0I@nH80!F);pKE$5?!s!Ve-oKHHa%>a5A~ z)|#0Xp}4g!h877!F-~hBIYpKH7VLqsH%Kp;_80W~B1M-XPjxb>O*e~cW0C|OB1+2F zrtyer$F>@!+cmX$vRSBDSg&da9;4Fh@bbb-o8`=OQTcvZ^pI&siZ%mEve)ml#KgWZ zJCm8LIS=|Yw{>C`Rn&RX55ySuAlBxC=~I}*pioglU$3D>Hx^d>XZYGBI+>*66aR=P z)>pOk%6V`DuTB5+MtL=YanxklMUj2@Ss=p!!c(NpVTL`{p&DrZZ6hUXYuRkJKEoyBo^&ERrm)y3Gw+k z#tRct#^8nXo33PcX3#XK&g)z zSnKXpMQ&XaLQZ31TGlDN6Y@dYdxi{Q7mi5Q*mrWfo6>@2h%bVLhkhhJ%Iw=y% zA3b<}9wabxYc1v`eUpvfRD=&fRNW)_6FnwdHm^s2O5E4rE}{9Xk86hMjc&T%zvMeT;plC0x*CK{fPJRDn8(y^iGy}p=Y`B9X@3Ih6MRh_r!d6;`I2~=&kqq2fOc))l|P(1KHNt zd{{arR&dm|G>ADXj&9sTr;kfkg!dF@+;8zTI!v&UP;#mC+DL9F=yuRV^rz`UFv9xY z_g@kRp#f1%;q&npejO|godMh%-c5Ottt5>)c)p^P5jt*xN$Y(PUc?zV!?Rx_)ocKx zs{ome3VZa^dhXN1-)vGt3v%3sBr!$VV!T|56cET%_=0GyIE8Ku8C(r` z7!|r5-kV)0&(JuSpRTq!S@I>q$uj+@dS`jC{iz~Xy1a>c_>g$TwzS_+yQbtaH+pi0 zHwn+;`>FPV|F(SWAFCK{yKO(wq0bFY#VFe8sI#=eV^4v>Q_FIDsusMpMwz7neLpIgkT5>}S@a=_z};SSzVA<;7{$J6U zK)Zv>rZBScTSvJP){O#j|Fl#u^9w1v+~dcHxJfWjM}?xSFBPdp0A*fpsDN(s7K`Uc z$4LEZr8$S@@0H%KDK6mB>F0aW<;Dm&YsPmVNAP(s<}50rysX6W5EF`?ZdNO+CTpH( zn5Uqc;&iSdE`rBUr553$W3SdP?2i3>%Lt2Rf9<8lP z1n6U^8+h2sM6Hl{yAVX{Ftke^!gQP|%KD*-`=V$wbSP@p;7ZZpo;P|4RyR@WSs?0w z1fop zjP+{Pe4J3HF%EGCMW9kSImH^uY>Q9ztMiE{$lym-H8ND`F5P!_?cZGQV&eu^HDQph zBs(@VbvN$W&X|>>Vk3c5g&4?L4S>7b`+)f6UQ#o!56^sEWO(8dLDN;Qs zB*n#(7f^Ty_fvW%UGF!ublO8QwPn3lRzBsI^fNnXN83eLXa<;@rNdWpQUG=h--+bl zXqQU~7AMtH*^V&w!Ke8Jw!rRxJM)R*)y9R(T?lK4x_B)cipa3eG|n?6UV_xZ$5v5G zZJO+qoCkb|x<$XeZ>-_l5PtN+ZNvT2NG)P;#+O_lx1brkv z25;^Ij*}gb$=MfK>HkKaZT8}mw%SQH6c~gbkrD^htVI--Thnl3x4Dn*{(QFVPt*6Z zhTvXXuG((}vwFTg+x|HswUrFRLMk|0v*pMhtas_slDm?;1K@cI%Tbu)d!`|F%Z^wv zY$h8jHurwGqk%prT0(Br6a*fmyrXEaNb2d@mQ+0IJUk*k2v9 zGPkH#z>@RAR<%f*8HJV41&;14%G|eZAk}f(Jpb0btg0v&vM~gzL1~rWr-w6o6UvPU zw|s6&0fQP-LTpJ5&y&P&@oL=&%JNCW=^`SEqjOJd8vU4c8^T$?UNw8j8~M4j?_(5B zHpL<;c0#jOUjNDpU5|K_<^@)?cGA%LDF3bHTG*xSW=tPl*6yXAN)***p5XZ2T5=7< zzQ5~s@s^o0@g^BLI^3Y!8I@`ByBpcK#ie9h6Lmxgk;nOXAb~52Yggr7IptawRbd$3 z!h-UM%p+czM;5tsMO@xvPvjfOE}soQlZWYB{u=%cLI7W1wo;$Lp;J;QP`zJ0k{j|g z7z`HLEtPmr>5rFVzc_e^k&4yI6!(1#qmc+i(RUsEP_~Y7%ks>B482=Ww#7jgTC9L?kWw##>C*Jx?gB#R!m5a^Bi>YWuDTG8CBKv z{vnZT^_ZAfqt8x=%~uO97phc&@(hdg4urpd&~sHQx9sAq1|+&~;tcU^H>BL~@vrZ0 zizefmr13#$mNIcr=Ffe}>MynCgjS9gQJxWx7Ww{Yb7yI$ZUI%6c$C*q$KKYy1q{mW z%~Yc(ykTv=o1(tinn$zUkdc=a(TMtt<$UX-dU6LjINx{G_QY{tqEIo_Q`ywTJ>RcK zYKivE{M1Jy4yAFzrHHx_8-Ows1T#ZVUs_VI75)cf)&C?X_)A^z>@)ZrYSoPZ%E^&^ z)!XBl!6}+?ULS;;ElVPC@`LJv9*J^u0{vk}sr20%M2`=i-EFw0%1*;MB1xba5s_=5Tjm^Lb6h+E+Zo z2fHf;?!Eb% zCmy`EIk_^b0n|&f7`TR=5zushv(uhzR&v`X`yAjc_>32~8S!-Wd4bBZIHUry|gYWMqJq{GpWDFei2f7=1-0y;;XtAe4qWAi@ zT%Ah0(_pW?!q5JAzJ{=bw<{?LP?R-My$pAb2-eFwCqtgUys+=%J}-RQ&3>?D)NcO) zgnUf*%XlqAYiiP`Wvy1<4W7r*oXuOe?J6{8$-^LsqBDiKzmN%tu<|pRPR8*Q%noG! z5N&cQ`DO~)7tz=(X5F0h{Vi67blYWFx|i{u^Wt?&ON-24>(7{bY{h}nqk)tVD4WA@ zI1sgC6}+ot7%2JOQJcL`r@g_9E64qV(#4US8wF7vKAzDx(Fcq)`t@V?P_+qqUEEc+ z{JLy@HizcWy*MGW+=W;i3Z@;(zhLA*y=nU6O8JRc0k}?TaD8Mfux*SDd}f#k zs{pN?qk8?5epw~sPfv13Y)iKWq!HclT z77&?&4$;ThpU%+B2>t=| zcQm{bSk6yQD-PeNEGLxDmHTcdOYM2QF3k@{MJP5VxUp=C?0>j_nHx}gApU5%{Cba% zCHY25QD-P6{Kd!27216s96jNyX56SejS)P$&SzH?Xlq>`4Pp%+BFGdA-ZS>ZTIXN6 zkkMo(&Im?h*+z!KP5{@*oTST+H#6N@7d5&&Hc)W7>m= zTN$f%kMY3U%f#>*ooiEXb7&q-hzLJAQG?27>cvhbypU+g^tb!r;421DJtR+h${V~? zl!njC$AHud&T%@5m*TwXNC8)M-m})CzFD(rRt|&;6YUP+(OH<@&bFn3(RTubr=R zVucmeJM&t52iE$iE~M!`X6D$BS$coJc5)IIm&mg4=Ip^p<@_LIlvnhtcHu*ykToctlX~(}iW_IUoLXlk0kX%r7Z)=nagb zO*(c?d&n{fhLW3X)+VctWjzFRNCH`d_f|Je6uS4cKpv-s7g>*bEjF*CiPN?4g3^JR zBTvU3wSq!|aQdfe;*Hk*X{ZG6R_R>3Teh`696$fumcn>I2+H$-A~U`BnuG^;mi}6=M6NExgeikhJktS9kBI5a)%^rsZ&R zsyy1WA$+t-fWAoJ8bT&zJF-{qyW|`KFu1kX_psv6+hIf3 z{+c!VM&j0<>5KXD80)~YrKxw&#H>A3;<0mTj8I<^)6~wQC}Jo=*2FM0z?2px9>4G`GWF4Yb>R6YHdN~?%ZM9!=i2lIVbMj8J0E&!n zG+!Z8lvP>P&_Mh3(}t4*2G$Eax19z9k-JlI49K*sEJxw0G3=&GsSai@dFcr?*f%G0 z)_>a??CcFV=vm#)rZf~XpoY$S%ZBOf|7MbKx2EQT>JT!A&qeQyh=Lkv|J=1fcr(&rcX3%)F2n3LL;nmiMj2&379&oe`d&**^UE=Z^om2F~*C zbhgyN=kzZB<16$HN!xiJx;S14siA`4J3t|N{;`Wgb^9sX$Uh_KJ0Hjb_0C0~FR;&{ Qe+UU9Ev_I|DPk1(Uy}b8ga7~l literal 0 HcmV?d00001 diff --git a/docs/user/UiFeatures/index.md b/docs/user/UiFeatures/index.md index dcc3dc6..026e78d 100644 --- a/docs/user/UiFeatures/index.md +++ b/docs/user/UiFeatures/index.md @@ -1,4 +1,5 @@ - [Exploration](../Exploration) - [Node Differences](../NodeDiff) - [Proof Slicing](../ProofSlicing) -- [Proof Caching](../ProofCaching) \ No newline at end of file +- [Proof Caching](../ProofCaching) +- [Proof Tree: linearized symbolic execution](../ProofTreeLinearMode) \ No newline at end of file diff --git a/mkdocs.yml b/mkdocs.yml index deea199..4445edd 100644 --- a/mkdocs.yml +++ b/mkdocs.yml @@ -111,6 +111,7 @@ nav: - user/NodeDiff.md - user/ProofSlicing/index.md - user/ProofCaching/index.md + - user/ProofTreeLinearMode.md - Languages: - user/JMLGrammar.md - user/KeyGrammar.md From 2f04ab489ce8c57515e33ed9521bb6436b17ddcb Mon Sep 17 00:00:00 2001 From: Arne Keller Date: Thu, 18 Jan 2024 16:15:31 +0100 Subject: [PATCH 3/4] Docs for proof caching disable + new action --- docs/user/ProofCaching/index.md | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/docs/user/ProofCaching/index.md b/docs/user/ProofCaching/index.md index ab6a189..3ca071b 100644 --- a/docs/user/ProofCaching/index.md +++ b/docs/user/ProofCaching/index.md @@ -39,6 +39,12 @@ Without condition 1, the replay may fail. In KeY's settings dialog, enable the Proof Caching extension. You can toggle the automatic search for references in the "Proof Caching" section (on by default). +### Enabling/disabling the functionality + +In the toolbar, a new Proof Caching toggle button is added. +In the options menu, a Proof Caching checkbox is synchronized to the same state. +When these are not activated, the automated reference search is disabled. + ## Automated reference search When running the auto pilot or a strategy macro, KeY will automatically search for references @@ -53,6 +59,11 @@ Right-click on an open goal in the proof tree and select "close by reference". If a matching branch is found, the goal will be closed. Otherwise, a dialog with an error message will open. +## Re-opening cached proof branches + +It is possible to re-open proof goals closed by the cache. +To do so, just activate the "Re-open cached goal" context menu entry on the goal you wish to re-open. + ## Copying referenced proof steps In the status line, a button indicates whether cached goals are present: From f89bcad7ebebf19519a42399e256eb32ea6ce83e Mon Sep 17 00:00:00 2001 From: Arne Keller Date: Mon, 29 Jan 2024 12:40:41 +0100 Subject: [PATCH 4/4] Document effect of tagging a branch 'main' --- docs/devel/HowToTaclet.md | 3 ++- docs/user/ProofTreeLinearMode.md | 2 +- docs/user/UiFeatures/index.md | 2 +- 3 files changed, 4 insertions(+), 3 deletions(-) diff --git a/docs/devel/HowToTaclet.md b/docs/devel/HowToTaclet.md index 50e06c3..6852bc6 100644 --- a/docs/devel/HowToTaclet.md +++ b/docs/devel/HowToTaclet.md @@ -76,8 +76,9 @@ The first branch is labeled "CUT: #cutFormula TRUE". In this branch, the found sub-term is replaced with true (`\replacewith(true)`), and the found sub-term is added as a new sequent formula to the antecedent: `\add(cutFormula ==>)`. A particular branch of the taclet can be tagged by enclosing the tag in brackets. +This tag must be written after the branch label. The first branch in this example is tagged with "main". -This tag must be written after the label. +This particular value causes the branch to be visually continued on the parent branch if [the linearized Proof Tree mode](../../user/ProofTreeLinearMode/) is active. The second branch of the taclet is labeled "CUT: #cutFormula FALSE". In this branch, the found sub-term is replaced with false (`\replacewith(false)`), and the found sub-term is added as a new sequent formula to the succedent: `\add( ==> cutFormula)`. diff --git a/docs/user/ProofTreeLinearMode.md b/docs/user/ProofTreeLinearMode.md index 5d033e5..b70057a 100644 --- a/docs/user/ProofTreeLinearMode.md +++ b/docs/user/ProofTreeLinearMode.md @@ -1,4 +1,4 @@ -# Proof Tree: linearized symbolic execution +# Proof Tree: linearized mode In the proof tree settings, you can enable the "Linearize Proof Tree" option. diff --git a/docs/user/UiFeatures/index.md b/docs/user/UiFeatures/index.md index 026e78d..d70a409 100644 --- a/docs/user/UiFeatures/index.md +++ b/docs/user/UiFeatures/index.md @@ -2,4 +2,4 @@ - [Node Differences](../NodeDiff) - [Proof Slicing](../ProofSlicing) - [Proof Caching](../ProofCaching) -- [Proof Tree: linearized symbolic execution](../ProofTreeLinearMode) \ No newline at end of file +- [Proof Tree: linearized mode](../ProofTreeLinearMode) \ No newline at end of file