From 307099b1cb525c282f4618babbfd2f81a80ed89e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 2 Jan 2014 12:13:26 -0800 Subject: [PATCH] refactor(builtin/Nat): cleanup all proofs using calculational proof style Signed-off-by: Leonardo de Moura --- src/builtin/Nat.lean | 148 +++++++++++++++++--------------------- src/builtin/obj/Nat.olean | Bin 20456 -> 15338 bytes 2 files changed, 65 insertions(+), 83 deletions(-) diff --git a/src/builtin/Nat.lean b/src/builtin/Nat.lean index 3509b2abf1..577019274a 100644 --- a/src/builtin/Nat.lean +++ b/src/builtin/Nat.lean @@ -41,135 +41,117 @@ Theorem ZeroNeOne : 0 ≠ 1 := Trivial. Theorem ZeroPlus (a : Nat) : 0 + a = a := Induction (show 0 + 0 = 0, Trivial) (λ (n : Nat) (Hi : 0 + n = n), - let L1 : 0 + (n + 1) = (0 + n) + 1 := PlusSucc 0 n - in show 0 + (n + 1) = n + 1, Subst L1 Hi) + calc 0 + (n + 1) = (0 + n) + 1 : PlusSucc 0 n + ... = n + 1 : { Hi }) a. Theorem SuccPlus (a b : Nat) : (a + 1) + b = (a + b) + 1 -:= Induction (show (a + 1) + 0 = (a + 0) + 1, - (Subst (PlusZero (a + 1)) (Symm (PlusZero a)))) +:= Induction (calc (a + 1) + 0 = a + 1 : PlusZero (a + 1) + ... = (a + 0) + 1 : { Symm (PlusZero a) }) (λ (n : Nat) (Hi : (a + 1) + n = (a + n) + 1), - let L1 : (a + 1) + (n + 1) = ((a + 1) + n) + 1 := PlusSucc (a + 1) n, - L2 : (a + 1) + (n + 1) = ((a + n) + 1) + 1 := Subst L1 Hi, - L3 : (a + n) + 1 = a + (n + 1) := Symm (PlusSucc a n) - in show (a + 1) + (n + 1) = (a + (n + 1)) + 1, Subst L2 L3) + calc (a + 1) + (n + 1) = ((a + 1) + n) + 1 : PlusSucc (a + 1) n + ... = ((a + n) + 1) + 1 : { Hi } + ... = (a + (n + 1)) + 1 : { show (a + n) + 1 = a + (n + 1), Symm (PlusSucc a n) }) b. Theorem PlusComm (a b : Nat) : a + b = b + a -:= Induction (show a + 0 = 0 + a, - let L1 : a + 0 = a := PlusZero a, - L2 : a = 0 + a := Symm (ZeroPlus a) - in Trans L1 L2) +:= Induction (calc a + 0 = a : PlusZero a + ... = 0 + a : Symm (ZeroPlus a)) (λ (n : Nat) (Hi : a + n = n + a), - let L1 : a + (n + 1) = (a + n) + 1 := PlusSucc a n, - L2 : a + (n + 1) = (n + a) + 1 := Subst L1 Hi, - L3 : (n + a) + 1 = (n + 1) + a := Symm (SuccPlus n a) - in show a + (n + 1) = (n + 1) + a, Trans L2 L3) + calc a + (n + 1) = (a + n) + 1 : PlusSucc a n + ... = (n + a) + 1 : { Hi } + ... = (n + 1) + a : Symm (SuccPlus n a)) b. Theorem PlusAssoc (a b c : Nat) : a + (b + c) = (a + b) + c -:= Induction (show 0 + (b + c) = (0 + b) + c, - Subst (ZeroPlus (b + c)) (Symm (ZeroPlus b))) +:= Induction (calc 0 + (b + c) = b + c : ZeroPlus (b + c) + ... = (0 + b) + c : { Symm (ZeroPlus b) }) (λ (n : Nat) (Hi : n + (b + c) = (n + b) + c), - let L1 : (n + 1) + (b + c) = (n + (b + c)) + 1 := SuccPlus n (b + c), - L2 : (n + 1) + (b + c) = ((n + b) + c) + 1 := Subst L1 Hi, - L3 : ((n + b) + 1) + c = ((n + b) + c) + 1 := SuccPlus (n + b) c, - L4 : (n + b) + 1 = (n + 1) + b := Symm (SuccPlus n b), - L5 : ((n + 1) + b) + c = ((n + b) + c) + 1 := Subst L3 L4, - L6 : ((n + b) + c) + 1 = ((n + 1) + b) + c := Symm L5 - in show (n + 1) + (b + c) = ((n + 1) + b) + c, Trans L2 L6) + calc (n + 1) + (b + c) = (n + (b + c)) + 1 : SuccPlus n (b + c) + ... = ((n + b) + c) + 1 : { Hi } + ... = ((n + b) + 1) + c : Symm (SuccPlus (n + b) c) + ... = ((n + 1) + b) + c : { show (n + b) + 1 = (n + 1) + b, Symm (SuccPlus n b) }) a. Theorem ZeroMul (a : Nat) : 0 * a = 0 := Induction (show 0 * 0 = 0, Trivial) (λ (n : Nat) (Hi : 0 * n = 0), - let L1 : 0 * (n + 1) = (0 * n) + 0 := MulSucc 0 n, - L2 : 0 * (n + 1) = 0 + 0 := Subst L1 Hi - in show 0 * (n + 1) = 0, L2) + calc 0 * (n + 1) = (0 * n) + 0 : MulSucc 0 n + ... = 0 + 0 : { Hi } + ... = 0 : Trivial) a. Theorem SuccMul (a b : Nat) : (a + 1) * b = a * b + b -:= Induction (show (a + 1) * 0 = a * 0 + 0, - Trans (MulZero (a + 1)) (Symm (Subst (PlusZero (a * 0)) (MulZero a)))) +:= Induction (calc (a + 1) * 0 = 0 : MulZero (a + 1) + ... = a * 0 : Symm (MulZero a) + ... = a * 0 + 0 : Symm (PlusZero (a * 0))) (λ (n : Nat) (Hi : (a + 1) * n = a * n + n), - let L1 : (a + 1) * (n + 1) = (a + 1) * n + (a + 1) := MulSucc (a + 1) n, - L2 : (a + 1) * (n + 1) = a * n + n + (a + 1) := Subst L1 Hi, - L3 : a * n + n + (a + 1) = a * n + n + a + 1 := PlusAssoc (a * n + n) a 1, - L4 : a * n + n + a = a * n + (n + a) := Symm (PlusAssoc (a * n) n a), - L5 : a * n + n + (a + 1) = a * n + (n + a) + 1 := Subst L3 L4, - L6 : a * n + n + (a + 1) = a * n + (a + n) + 1 := Subst L5 (PlusComm n a), - L7 : a * n + (a + n) = a * n + a + n := PlusAssoc (a * n) a n, - L8 : a * n + n + (a + 1) = a * n + a + n + 1 := Subst L6 L7, - L9 : a * n + a = a * (n + 1) := Symm (MulSucc a n), - L10 : a * n + n + (a + 1) = a * (n + 1) + n + 1 := Subst L8 L9, - L11 : a * (n + 1) + n + 1 = a * (n + 1) + (n + 1) := Symm (PlusAssoc (a * (n + 1)) n 1) - in show (a + 1) * (n + 1) = a * (n + 1) + (n + 1), - Trans (Trans L2 L10) L11) + calc (a + 1) * (n + 1) = (a + 1) * n + (a + 1) : MulSucc (a + 1) n + ... = a * n + n + (a + 1) : { Hi } + ... = a * n + n + a + 1 : PlusAssoc (a * n + n) a 1 + ... = a * n + (n + a) + 1 : { show a * n + n + a = a * n + (n + a), Symm (PlusAssoc (a * n) n a) } + ... = a * n + (a + n) + 1 : { PlusComm n a } + ... = a * n + a + n + 1 : { PlusAssoc (a * n) a n } + ... = a * (n + 1) + n + 1 : { Symm (MulSucc a n) } + ... = a * (n + 1) + (n + 1) : Symm (PlusAssoc (a * (n + 1)) n 1)) b. Theorem OneMul (a : Nat) : 1 * a = a := Induction (show 1 * 0 = 0, Trivial) (λ (n : Nat) (Hi : 1 * n = n), - let L1 : 1 * (n + 1) = 1 * n + 1 := MulSucc 1 n - in show 1 * (n + 1) = n + 1, Subst L1 Hi) + calc 1 * (n + 1) = 1 * n + 1 : MulSucc 1 n + ... = n + 1 : { Hi }) a. Theorem MulOne (a : Nat) : a * 1 = a := Induction (show 0 * 1 = 0, Trivial) (λ (n : Nat) (Hi : n * 1 = n), - let L1 : (n + 1) * 1 = n * 1 + 1 := SuccMul n 1 - in show (n + 1) * 1 = n + 1, Subst L1 Hi) + calc (n + 1) * 1 = n * 1 + 1 : SuccMul n 1 + ... = n + 1 : { Hi }) a. Theorem MulComm (a b : Nat) : a * b = b * a -:= Induction (show a * 0 = 0 * a, Trans (MulZero a) (Symm (ZeroMul a))) +:= Induction (calc a * 0 = 0 : MulZero a + ... = 0 * a : Symm (ZeroMul a)) (λ (n : Nat) (Hi : a * n = n * a), - let L1 : a * (n + 1) = a * n + a := MulSucc a n, - L2 : (n + 1) * a = n * a + a := SuccMul n a, - L3 : (n + 1) * a = a * n + a := Subst L2 (Symm Hi) - in show a * (n + 1) = (n + 1) * a, Trans L1 (Symm L3)) + calc a * (n + 1) = a * n + a : MulSucc a n + ... = n * a + a : { Hi } + ... = (n + 1) * a : Symm (SuccMul n a)) b. Theorem Distribute (a b c : Nat) : a * (b + c) = a * b + a * c -:= Induction (let L1 : 0 * (b + c) = 0 := ZeroMul (b + c), - L2 : 0 * b + 0 * c = 0 + 0 := Subst (Subst (Refl (0 * b + 0 * c)) (ZeroMul b)) (ZeroMul c), - L3 : 0 + 0 = 0 := Trivial - in show 0 * (b + c) = 0 * b + 0 * c, Trans L1 (Symm (Trans L2 L3))) +:= Induction (calc 0 * (b + c) = 0 : ZeroMul (b + c) + ... = 0 + 0 : Trivial + ... = 0 * b + 0 : { Symm (ZeroMul b) } + ... = 0 * b + 0 * c : { Symm (ZeroMul c) }) (λ (n : Nat) (Hi : n * (b + c) = n * b + n * c), - let L1 : (n + 1) * (b + c) = n * (b + c) + (b + c) := SuccMul n (b + c), - L2 : (n + 1) * (b + c) = n * b + n * c + (b + c) := Subst L1 Hi, - L3 : n * b + n * c + (b + c) = n * b + n * c + b + c := PlusAssoc (n * b + n * c) b c, - L4 : n * b + n * c + b = n * b + (n * c + b) := Symm (PlusAssoc (n * b) (n * c) b), - L5 : n * b + n * c + b = n * b + (b + n * c) := Subst L4 (PlusComm (n * c) b), - L6 : n * b + (b + n * c) = n * b + b + n * c := PlusAssoc (n * b) b (n * c), - L7 : n * b + (b + n * c) = (n + 1) * b + n * c := Subst L6 (Symm (SuccMul n b)), - L8 : n * b + n * c + b = (n + 1) * b + n * c := Trans L5 L7, - L9 : n * b + n * c + (b + c) = (n + 1) * b + n * c + c := Subst L3 L8, - L10 : (n + 1) * b + n * c + c = (n + 1) * b + (n * c + c) := Symm (PlusAssoc ((n + 1) * b) (n * c) c), - L11 : (n + 1) * b + n * c + c = (n + 1) * b + (n + 1) * c := Subst L10 (Symm (SuccMul n c)), - L12 : n * b + n * c + (b + c) = (n + 1) * b + (n + 1) * c := Trans L9 L11 - in show (n + 1) * (b + c) = (n + 1) * b + (n + 1) * c, - Trans L2 L12) + calc (n + 1) * (b + c) = n * (b + c) + (b + c) : SuccMul n (b + c) + ... = n * b + n * c + (b + c) : { Hi } + ... = n * b + n * c + b + c : PlusAssoc (n * b + n * c) b c + ... = n * b + (n * c + b) + c : { Symm (PlusAssoc (n * b) (n * c) b) } + ... = n * b + (b + n * c) + c : { PlusComm (n * c) b } + ... = n * b + b + n * c + c : { PlusAssoc (n * b) b (n * c) } + ... = (n + 1) * b + n * c + c : { Symm (SuccMul n b) } + ... = (n + 1) * b + (n * c + c) : Symm (PlusAssoc ((n + 1) * b) (n * c) c) + ... = (n + 1) * b + (n + 1) * c : { Symm (SuccMul n c) }) a. Theorem Distribute2 (a b c : Nat) : (a + b) * c = a * c + b * c -:= let L1 : (a + b) * c = c * (a + b) := MulComm (a + b) c, - L2 : c * (a + b) = c * a + c * b := Distribute c a b, - L3 : (a + b) * c = c * a + c * b := Trans L1 L2 - in Subst (Subst L3 (MulComm c a)) (MulComm c b). +:= calc (a + b) * c = c * (a + b) : MulComm (a + b) c + ... = c * a + c * b : Distribute c a b + ... = a * c + c * b : { MulComm c a } + ... = a * c + b * c : { MulComm c b }. Theorem MulAssoc (a b c : Nat) : a * (b * c) = a * b * c -:= Induction (let L1 : 0 * (b * c) = 0 := ZeroMul (b * c), - L2 : 0 * b * c = 0 * c := Subst (Refl (0 * b * c)) (ZeroMul b), - L3 : 0 * c = 0 := ZeroMul c - in show 0 * (b * c) = 0 * b * c, Trans L1 (Symm (Trans L2 L3))) +:= Induction (calc 0 * (b * c) = 0 : ZeroMul (b * c) + ... = 0 * c : Symm (ZeroMul c) + ... = (0 * b) * c : { Symm (ZeroMul b) }) (λ (n : Nat) (Hi : n * (b * c) = n * b * c), - let L1 : (n + 1) * (b * c) = n * (b * c) + (b * c) := SuccMul n (b * c), - L2 : (n + 1) * (b * c) = n * b * c + (b * c) := Subst L1 Hi, - L3 : n * b * c + (b * c) = (n * b + b) * c := Symm (Distribute2 (n * b) b c), - L4 : n * b * c + (b * c) = (n + 1) * b * c := Subst L3 (Symm (SuccMul n b)) - in show (n + 1) * (b * c) = (n + 1) * b * c, Trans L2 L4) + calc (n + 1) * (b * c) = n * (b * c) + (b * c) : SuccMul n (b * c) + ... = n * b * c + (b * c) : { Hi } + ... = (n * b + b) * c : Symm (Distribute2 (n * b) b c) + ... = (n + 1) * b * c : { Symm (SuccMul n b) }) a. SetOpaque ge true. diff --git a/src/builtin/obj/Nat.olean b/src/builtin/obj/Nat.olean index b5e571a5fc51c926cf7e764c3e5c1c989a3d3f08..44c6d2416cce9061c15c760f98fabaf7df387a19 100644 GIT binary patch literal 15338 zcmb_jTZ~;*8Qy!JedY`X5JIISf&$ZNz&fFW;bH`0FCYaegjNMg0@KbZojN_I&V`FH zh|mOy5)%oCKFABi%aaC4AAAOlnkFh0BnA_dCw!_J^cS-)&n;!e?zxq$muJQP;Yzk` zaba#bE8aTxbXLfe?W+rmD+_}?{gtdUaFSay-^1oTbMy1r?%~SZ%EEAf33;)FGq<79 zsfiw0U5rFOMbR4|TGm7z;X3Fw*Jinsx*Ve2`p{cXJa5K!_77$yO}ek2O%!v%jEQ1D z=DMz8`*67EP|!M!U95hD)lDe7P({qVuIf6^g07j2D8BW?3&O*Xk_mu%iz`h`&gK|( ze-zcTSv`x@siGLTXk?^w7U<;URHt)|(RXI1`tEDgcRrANRI&lp^I82Et5Ya9sPRqO zt~1)sG1?a9t#ts}Oyu)eO=uUzH!}CH=SHuhr#5EW9?VJz_x7wFIIwGQ*y4q_ZJ8); z%%+Q?|FtYD7+-Ntht6SU&YB*{)!A$sxSvL`1%d^o-5Nko_Hp*)mHOKjSC{YVFAc4J z1(>0Gs4uJp8dsYR3+(hje|sZN9zzBbv|l3O?WH%&I6UA-TFJTqBsP50EELGRD;3NmSaBma=#!jjo;~(!Dv(yPE zaSD;%;v${rdk^_MgYS0tZyofJQ3IqDerBw*W?h!;U0S$*Vb1LpwTZ|QYf9{|j)$q- zAzRJWQ1RGiru>$yTRez%Hj~Uo?=hWwTCsd+_`pp6!J|w4c^Ps5q825uEC+=Dz9IXck(M8xg9wd}@fp9CI2*PBkQ(vV%U z{C7C9YT3s2V8}!0Y{q8}LpO&YbDrzS=TMWqzuMlgwe1+X#bl03zrE$F(~##q$y{?} z?^2Bf%<0t|0l&)XE>_z&F;I~`DncquYU_}s|5ni@-Hf&G2`e9{xp7^-DzdIyj!z0a zCE{11H-BpEMzKz+4Jjuij5UA^D=r!INlY2z43K>x7Ow3gkZ`A(`;|@6Q!<*Y8X}`G z_cunh)3!Ds%x*g$bmc!|TNmrEAfA~pG#osT;K`M2j3jmf<0r(H&r8%@M}C6H zwdCElygY2WT<3326bFEkzuB0^g&JWqT6^WGfC}lBTZqN#Zmr(R>gYT-+pK_!5>-V5 zWyl0v#(kQruw_eMk)nmPD}#d}-(wJy8AOtCXHj;{{Vz^W(*a`E2EyyyDhG<%Dtr^O z&LCu6|Maq(;J`^&P=7QpwwZvTlhfr~oj=N@7>|k3n z05<*oIwqycJH%smza?Ejv{O^SFcUirQ)rNGD2jo&U z(6IL!@wql(QKy##Qvm`+9|A+q_Q)MZX#0Nu%RocbS-u zLRhGAKC-|WjKwi_5y2Q|a2^kSYH#hpG*<^91I*cgrZhm@J@{ki^D~NKr`%;lt9{DZO+Aiq;3c zcs3!pwpo;zd%uFgl+F>h)y@aja4P?w%ow@ziAR-e;-BUP0h9hwi<0ppJxB=#Gl`CR zSoA{l19r9~nc*P5R=(^cu3}oGWfg3hBbUsM6C~(&0c7k+f&jRH*(Er=WIcgPRR%B#deL z`Ir01EV}(oV?4R}`>O*d)8+R#sd7n-b)SA=l6=yU%!lAIC$d<>4kI_{*>F+z7q9i- z`z>iEn)xIp=rE4*C!lq_?*j1=@gg&SuNR$pmDi=5G9|q5ZQ`(~99BMVKN_Og_aOny z@@Zw~npr8Ip;Zg4dXwr97@_L|>^z6e0}fpCJ3H zl61|ie2s05=t+pD5p8+RU!H1=tvr7zOR<9l7ohYMtA|-_h_`$ zasbkIiU2yo6b_m+bVJ<>V;sF4;>7Dt*G>$gRhi}AwUfL#!^OQ+RwY>$K6<4(O0bZN zhf<{vz-pr!5PS``_YA@Qku)MOguzz)>wjcTT z3*CMGEq`}kV-}n1x=CmgA=)bMLDhEI%ka&$?ml`8uM~atD66A0-aH8ye4|yeO56dw zC73MxeR8~PHE5{~c5(Q+1Wv&1aMB~6r;0+bkOvldBCFOQ1|Ey@^I;E*u_wbC6SXvi z0rVTQNlYhR92XX-@;#n>a9I0(15m$%;=2mznpyWzwlxKxtZe|0_<<{m+NytMjDCCT zsBO7``z8#59bUDMAUck5h=xY2{I_{_I4SwULiYt%sk3^1O?#0E{P;8?6%=V2sT;$l zqdnXr>??J%DjHD~La=@Brw?Nz7)$#BCPS}~UWujS7To`l`!*w!B*c39JOFzV& z3i!@gK<*y0-y83;szVC+{`vu%uq1rWYZEr?&0dVHi`yipfTypUp|R7rfO!Ij8%F@j z)Oc3h2Fk^?^CFg@3i~dIDF&n-7Qv*#HJ4$M*oL|IU%bbmk){|INYaioMOB#4 zXvhVxO6BhRNh<#xr2bah#7MIyXo58I>@)Pu320_}0c8#QCjNsmnd|y`-FiUQK5tx@ za4h#OAfC0z^)gJo3tGZtgn6?6K?7tAhy#$A&AG2}E((dAhUsL@`=EL;iciL2>Ro`@ zMZ>en<@RNXe>myw^baS!ozrew?S+_nmfRUVe^Q8(s7Sf$3YHryz7XBpNvEx9^?p_v z3;P`Lp_FkA`EQ7fqhvIK!JVQ|XUTeu+AywnZ{t+i7zL$r1m*op?L*#II*6J-MUPOO z=tQ@^NV5;emJ^tKiwJFLNE{R<>tx9(OS2=Gp(@LI6?bZ)&Uo2~;Z!Exg4B;FKZ+T5 zZu1mt)EmAcMKFRZvwJ1c4~gTbv&wPzF0k!8cDBqaqGc0Zsx=CpPa7dFIMxl_M zLRorB11Otnr%gP=gkFbCP%W+zP!*&04`Y>hS`kc}D$GJNLscG4&Ol@PdqD-}q9LTA zZVzt4ixk{*hfc*Eb@C3msw^8q29gr7&&*z^xQ7LoC7HkgUP>kpCqDDJq*R#UWNN&@ zDp#3kRPStvSJ@<9Elw`hLXV!qWO3`!xvX@}tmpo2HP@E=+fmbUf7xkT?k_L%>j(2U I;O~3?3pmuZJOBUy literal 20456 zcmbtcTdW;b8J?NF&)(_n4*!GRFnsd3MN>6@Iie6VoVH1W5PovJdluxA;DmbuJ8NTn*X0!GqdL) zf$6&Zm+!xEirgX5skU{2=lFq&JsEJ z$+;VyPJ#5)>U@dx3XN`=X?{Y})Q^}=hUe4yb*xZcg zrD}YYw(E_ycN%STv(`EY+Cs_iVKaiAWv3JOZ{N-Cpr_uQ?7lbYg1CQZ_1LkS7Cvv~ zg}80)W&4uJEE{|wNixP)oYSFmn3>aNL~?aHnS|UAGTKy_u8{I>FVI|PG0y`|Q>;e9sN;zp+WH3R;B@*7gT-E;7`C&l21V_g00k7q+ zL;9IAQVMEDDkM}$2j_ZjT9{ou#?sKsZnJ&~tI$RDXtLQtbt7|*azPjFJ|ST2q}eh4 z@vbpTo#G@;A<|o2q|@~9-9FFYy90w;7Y4|v1*8=I*=C(J?Xv9f(%cv4W?Zc(Fd|E= zDP@0kyqMe_QfjV&imz>9%5P0ZvU|}_wnf|+J)^v1+49|sU)naf_nxJ}@-m8S8nIa1 zd911EV_dUNTkg&gxVKJ%ReQ^Hy{6dxG9pi7f6BJYYNFX3@(_B`HCU$lvLFy{VvNJc zRF)lDJ-Y0QCjL1mENDIkZA_kQ1pRCAI2XA9qd!qa9rS;yeRPv&atFz>WH(O^tf+Ew zg!TVIq)$Z$CsCRVn@Ns(tBHR%ki5X=9yarwLXXzPS)~FQi9b~8k`)FiFSZGe$_y6x z$VWE#ac{*GA$$UQl5GIuiwpX%<8d908*Yi0M-~NxZt})vD*1rf5@_-pTU?ra`P3;A zB`@HQf8z0apl64qLl=#z3^~}~RgZNnt6WzqN~%ZL2k0HoYP}lM7bt1_W@CGhN-Brp z%8IqEGP?zh;0Xp+V_^9YB%ZerWXlF|UH4x)O2N?-M=`&#T^4{Uof0wN#llUuYTtE} z^eW7-7P_)?%TM&Og-wXM8f z6sltIRB2C}fuv2SdO+57|D^|1fR%-*gY80vGhcd4#n9m6+IQ1Qx&VcyyfSimjYWO^ zG$n^dHN0~ zYN~@}VmlP8z+{(mdKROZfHT4~ldb7lnRbM7)v@{q*qC%)&Byh4khE zdkRYYG0e5nU$9R+c(gorfV9q+m35L@)bC;6kr5r|!62XX)sVb+pafWt*|pnMA)%m^ zg%faCLKS5WDx@MBSsY}h)og1ZC>4(MWfkCNlk`;(wX9-v!H8esWfMXHqf(O>!4s;N z#~_{-Jh$)%#txvzHxna*}LkWfAhr5g=?mQV>iknPQfFma^EqQ=50O z*|tiV{a?hFEoZ!Bs!hCnF;UR5DW=}YWMO^Kd|`KnBxhjFY}2A3mFlxrK$a|pP_>j! zRGYlcc0$zvkJ&)Z4y6n|=#fgrTNpZ8aAsxkQrf&UIS}#|Bd;<-Vd%73c-OJ(%^#kD zQD|zan~EwHHZZbW`D$LqKx>7-FVI3vjaY5Q@}R{?Y6`lFVJZ2(_PIz+g?2KN>`6uk zkLIJDiYb&vnlE$qiD985K`2e!N_LrrWoVq=uWme8(ksOSn}RA-Ig`4f${9+S&64bk zXK^Zf1@ncH+;s!lD-PdBYw@X!uxG$-cPs2_uFTmdh8YYYsLu-{mhu4PZ;>R7zQp;a zyZ`|gS>Fm!4XoaLslYii`#0#N5;)7=2{ z#MwWT#VR*cN&tG=khH1IDxzP&4tZk~TCFfpD_zA7YlH)pS&@yRRVKKetO4NWI`30b zw75_hYALGu=^yuY?&{MX{>xF7b+lc$>5A=g|8@e3PPEuNyCA$9IPg#BWDEBPrCy)^ zgT8n&s*`ZwRu#o9qiANl9ngcP zp&KeY_cg3)l0K}8Q1UyEXy0{{&Ufe)+OmdVsE}~n^|*6sk|cR{;r_0aUH;Xw^K6u6 zDm}QLVr7_5X0a3?PSFdCu;*De@eQK$Y@38sUG(RLN=@8d>8|J7I7wv&{N6i}1y#|u z2XM0?2T_1=5Rb#|zs_If$h8FnotFx=lG7MJT#-dElctI&lSQLtko3!+A?+{Z5RLx! zPXgi1uvlIu?XcsYu`etG@r?hz;%CU< z;8eWt8oOk{+e^n_sevQ=Af3qv6VANY1R)iXR71Lm(OW>}IXP7pYC=8fNbRm|P=l&_ zxynZE=)Pb3#vLS`Vr+s(>MsEml3WFX!yf|B3MnGr{9Mvo$>Kz75a!wW=*X=&X!L>Mn$417=dl(Y%Ta50nMXY(!GG%Z?N%!}l z_XnDrxkvOc{G3ay9d!qNBS*~@xkj7GYt<>OIIqhTPW?4?>W$!Wpr@n#K8F5yU6?8v zMMQm=Xb~+IO10SbjopTpXb5pFA)NpR9WtiMCJ>eXYTtE}5fbHjeQlk?h)AVQP>Kwy zz%lQFxR^zh(0!+H8c_hW1JEbJ@t7SByKqjs7l}#Nu{%(-hSq_FejQh2>+0f3VC$4H z1fD|LL{!y@lt>`JPp>6*>uEC|iVHWpBm1PUqg-qV>&QXS=V6?#cvFcSwO-{+cuT1? zb`@=^Addyakv9vbl>}=d+mUjZ`*k8k>%q7XSUn};wVlN`6kGw76?sH_8`Kp=63Zkz zUd>^BgOhHLPwUY4$0y^HNE-~?Pc3L297g&T0~8GR6+mI+X(Pe}Zv%Dkp&|%+3S4{( zGPMMRr58H)1E13STzM^rGpjOl-P{ia7bUgaZ*?HK`m;?Jgnw7=HqrJW<{xkC*E%t1 zRH`H@RDn*tSM`$N;lPG`n#WXsQ{V(+Y7LgDzT#U1G)v zEuI9-=frfls9`YLUL!@IYf?jF6oT$8l?jOmgq5d>#{CG*Otnc3)fY0Lpbz50gh`Fw zE(HR`y*(t%Q=_*likd27R@?!uBRc51N$)O5X-bWnUl{aOB6aiw#VJyeOpp&j-3prz zv)MLr!UTVbzo?6-6Z)cb-Flm7nO4=LnBlY$WrW>(GCL|U?S5trY>CiBk8 zEaj_Q5=He-ApIj4TBn?mT-bMv2f{dk)Fh%60}wwFE7WcxrbmR-$_Im(N$8PTZ#4)5 z2VEkM{8D)D-15rO+|kvQ!e-&`h5MWQXaD}D%F1AF$K<432Eg2r3q9H-D}qsd%;D*8 zV)MJ&{2rTatBAP)Gn&j9i^dAdE+l^lZoqfc+T%p{*%ArqG%m#LNvHv0qE1(@Igi2f zg4&}nBmSb(kN7_-mWN~ZwF<414Qs+{b!7dIL#OFquNbg#^!K2jG-<E$KL-`by<>Hlpj7lR)5fF zvz>bm;*t^rTw-W!uB=hJ4|OV*Kk$B}ED?iO%OIa!3@~YVb~wJCEGCfO+1zg z>hj^eoC9)MooKb&xz@C>D3)4k7M9pY3Od$a#EV%%!6)m4{RRL&Q)oPcJ*TOBnXF!t zrjmwjP#I+pGBA9UsT>a;E4-Mv4TAEbHse*eX3xO(pX+k?< zX^gEXg!9fzK#fp0+PT1~p|K@GekU;Z%F@&+W0wgZxp+Ai9qvb;g!U)w8w`FgHG1Cp zvCY>D1IVC&lRV0@$)kQxQxd~h*qFsl=Bb2{*(%MXl)=U&8F5+J(uN#-ej7cf5>+i- zD2H1;t@dvS(ki6VW`MhD}3;r5*VFB z6V>SDXAtvUf_-rZBf^gtrqB9ApRnS%Te9KbT+~(e+exHUZHbJH`N}2`(nRfs)&!wi zlyI1*IV9kJJs-Ofcq1b)v%gpljqV|QaAw7eoB)iRVn4~q2My)`J;AW~8&~Q#=qvaX zqMckrcS8j-@jP~%em;ZEAR!Oc!a^WG{WFZ|O z_I^CRYD+0Tjg6g#<0~$j3XX?Z!iZogc76h>LuksX7om*dlMs}wZ&72{3?#}PIBfJk z&==W55Q442&6QItv(aB3TSMbjr`S@jQKCR7X*u>(g_?Shx^h#MJg_~D7nU_`h zt!SK}oQ{h1DJWHuXp_F0YsrZ#O|{4nrKiVvB(QVIprfWb-M;5Ews5YWVNpWob>RE#eq|f4yr$AV5W& z3Z>biTL-0Iu?QHZGF^j6mXD#I4iUeJYgMc**^Fg*ii3DG-k|#R1Ufp#h^2wHPYotU z${h-6h4|_ zpyC6uu~g&((c_UMH_ErDiN_ma?`0`CI+-_G<`%Zx=Vn1OqWh+a^FZ?hyKuV1*QV|f zhPXOfIu=9O*6