From 6813754dce16fba5c517be4eef9ea95552f262e0 Mon Sep 17 00:00:00 2001 From: MARCHE Claude Date: Tue, 1 Oct 2024 15:38:42 +0200 Subject: [PATCH] clarify ghost and non-ghost for reals and ufloats --- examples/numeric/add_sqrt.mlw | 8 +- examples/numeric/add_sqrt/why3session.xml | 12 +- examples/numeric/add_sqrt/why3shapes.gz | Bin 460 -> 462 bytes examples/numeric/add_sub_mul.mlw | 16 +- examples/numeric/add_sub_mul/why3session.xml | 360 ++++++------ examples/numeric/add_sub_mul/why3shapes.gz | Bin 5239 -> 5243 bytes examples/numeric/addition.mlw | 8 +- examples/numeric/addition/why3session.xml | 164 +++--- examples/numeric/addition/why3shapes.gz | Bin 2774 -> 2779 bytes examples/numeric/exp_log.mlw | 16 +- examples/numeric/exp_log/why3session.xml | 252 ++++----- examples/numeric/exp_log/why3shapes.gz | Bin 5456 -> 5459 bytes examples/numeric/lse.mlw | 34 +- examples/numeric/lse/why3session.xml | 347 ++++++------ examples/numeric/lse/why3shapes.gz | Bin 9702 -> 9742 bytes examples/numeric/multiplication.mlw | 8 +- examples/numeric/multiplication/why3session.xml | 188 +++---- examples/numeric/multiplication/why3shapes.gz | Bin 3443 -> 3446 bytes examples/numeric/sin_cos.mlw | 22 +- examples/numeric/sin_cos/why3session.xml | 710 ++++++++++++------------ examples/numeric/sin_cos/why3shapes.gz | Bin 15516 -> 15513 bytes examples/numeric/substraction.mlw | 8 +- examples/numeric/substraction/why3session.xml | 168 +++--- examples/numeric/substraction/why3shapes.gz | Bin 2796 -> 2785 bytes examples/numeric/sum.mlw | 12 +- examples/regtests.sh | 1 + examples/stdlib/ufloat/why3session.xml | 339 +++++------ examples/stdlib/ufloat/why3shapes.gz | Bin 13223 -> 13561 bytes stdlib/real.mlw | 2 +- stdlib/ufloat.mlw | 42 +- 30 files changed, 1372 insertions(+), 1345 deletions(-) rewrite examples/numeric/add_sqrt/why3shapes.gz (100%) rewrite examples/numeric/add_sub_mul/why3shapes.gz (100%) rewrite examples/numeric/addition/why3shapes.gz (100%) rewrite examples/numeric/exp_log/why3shapes.gz (100%) rewrite examples/numeric/lse/why3shapes.gz (100%) rewrite examples/numeric/multiplication/why3shapes.gz (100%) rewrite examples/numeric/sin_cos/why3shapes.gz (99%) rewrite examples/numeric/substraction/why3shapes.gz (100%) rewrite examples/stdlib/ufloat/why3shapes.gz (99%) diff --git a/examples/numeric/add_sqrt.mlw b/examples/numeric/add_sqrt.mlw index 9e18b129b..d44207ecc 100644 --- a/examples/numeric/add_sqrt.mlw +++ b/examples/numeric/add_sqrt.mlw @@ -6,9 +6,9 @@ module AdditionSqrtSingle use ieee_float.RoundingMode use real.Square - function usqrt (x:usingle) : usingle + val function usqrt (x:usingle) : usingle - let ghost add_sqrt (a b : usingle) + let add_sqrt (a b : usingle) ensures { let exact = (to_real a +. to_real (usqrt b)) in abs (to_real result -. exact) <=. eps *. abs exact @@ -24,9 +24,9 @@ module AdditionSqrtDouble use ieee_float.RoundingMode use real.Square - function usqrt (x:udouble) : udouble + val function usqrt (x:udouble) : udouble - let ghost add_sqrt (a b : udouble) + let add_sqrt (a b : udouble) ensures { let exact = (to_real a +. to_real (usqrt b)) in abs (to_real result -. exact) <=. eps *. abs exact diff --git a/examples/numeric/add_sqrt/why3session.xml b/examples/numeric/add_sqrt/why3session.xml index 55f1fc006..e0d19a71e 100644 --- a/examples/numeric/add_sqrt/why3session.xml +++ b/examples/numeric/add_sqrt/why3session.xml @@ -12,16 +12,16 @@ - + - + - + @@ -37,16 +37,16 @@ abs (to_real result -. t) <=. (eps *. abs t)"> - + - + - + diff --git a/examples/numeric/add_sqrt/why3shapes.gz b/examples/numeric/add_sqrt/why3shapes.gz dissimilarity index 100% index 3db264e4362db0fb99c85cb9572e079cb467fe66..73b3efee8d2481c29670f914bb13a821c190ddb3 100644 GIT binary patch literal 462 zcwPa{0Wtm`iwFP!00000|Ampkj?^#=hVOlf9${9DoWyn#1ScdkhduYYa$-lUH0%s* z2l4o%qh%Q+Sfn0O=g${^&YRu1e37#)<9C~v$J5jMk;mQJK|Xxkih$Dpe_0+7@htE@blDA~wf@kbQtqEBL6X!PU}Qwcb>) z>ZF-kQ;MyM`hulf#j9mYY?2ytj7C@+07kHe;sdvw{MFJNH%Gl;jN%wwBo1B(gt|ii zf41~BCJU;l)%y?&_7RrgJ!R|2NY9o4rYW&6)*nPFBDEqplJsLxR9-B90z9|NT}lH0 E071dqlmGw# literal 460 zcwPa_0Wsh41|<`lz!wR3(*EO7tYi9QNGTrIJ)|VcZ$J zd&Hk_rdih!bcGO_%IlZ+y}a3t%NIS{GJdytc|1M6ALF=tJLrdxd)2(?yS=WbhuQR~ zvn`k7I)U!?YUky8Ji)!*{Z{D9*Jb%OubKy47MoYAV>``XFGqdF_*J8uJO6Xxzy0lp zmi5+X8w}^uvX;|ReOx>K-~OLyinq-1mbusQM}!IQC+dQ`{RES{@9Wq6^Duq7)-Y_7D=LrFVM_JI{1N0lBO(H zC0g(#t~6&J6KICYZNvi%4H$CuNjXZ8QZ*FnW-ausvhvlb%Zl?3L;=KG>8VndVihGg z6Oov^m)m3{jWCodn35*zLAjA{lD#0n=5`hKk-Ff-Vd!XRm|UtX5JCmXp>321&XEOc z#d`Ei8OV@{m~%()VWX_I*QE?%t(h-Q6M*@ITaRqAQPMRCy2iaO$fXjH%Z@QqlaeDo zQwFWk^@=oGM)+FEqzPXHg6gXe1EL?LirOryYCuG0{{SQ CAm=*( diff --git a/examples/numeric/add_sub_mul.mlw b/examples/numeric/add_sub_mul.mlw index 902f19e88..f1bd00614 100644 --- a/examples/numeric/add_sub_mul.mlw +++ b/examples/numeric/add_sub_mul.mlw @@ -4,7 +4,7 @@ module AddSubMulSingle use ufloat.USingle use ufloat.USingleLemmas - let ghost example1 (a b c d : usingle) + let example1 (a b c d : usingle) ensures { let exact = (to_real a +. to_real b -. to_real c) *. to_real d in let exact_abs = abs ((abs (to_real a +. to_real b) +. abs (to_real c)) *. to_real d) in @@ -12,7 +12,7 @@ module AddSubMulSingle } = (a ++. b --. c) **. d - let ghost determinant (a b c d : usingle) + let determinant (a b c d : usingle) ensures { let t1 = to_real a *. to_real d in let t2 = to_real b *. to_real c in @@ -21,7 +21,7 @@ module AddSubMulSingle } = (a **. d --. b **. c) - let ghost square_norm (a b c : usingle) + let square_norm (a b c : usingle) ensures { let t1 = to_real a *. to_real a in let t2 = to_real b *. to_real b in @@ -34,7 +34,7 @@ module AddSubMulSingle } = (a **. a ++. b **. b ++. c **. c) - let ghost example2 (a b c : usingle) + let example2 (a b c : usingle) ensures { let t = 1.0 +. eps in let t1 = eps +. (eps *. t) in @@ -53,7 +53,7 @@ module AddSubMulDouble use ufloat.UDouble use ufloat.UDoubleLemmas - let ghost example1 (a b c d : udouble) + let example1 (a b c d : udouble) ensures { let exact = (to_real a +. to_real b -. to_real c) *. to_real d in let exact_abs = abs ((abs (to_real a +. to_real b) +. abs (to_real c)) *. to_real d) in @@ -61,7 +61,7 @@ module AddSubMulDouble } = (a ++. b --. c) **. d - let ghost determinant (a b c d : udouble) + let determinant (a b c d : udouble) ensures { let t1 = to_real a *. to_real d in let t2 = to_real b *. to_real c in @@ -70,7 +70,7 @@ module AddSubMulDouble } = (a **. d --. b **. c) - let ghost square_norm (a b c : udouble) + let square_norm (a b c : udouble) ensures { let t1 = to_real a *. to_real a in let t2 = to_real b *. to_real b in @@ -83,7 +83,7 @@ module AddSubMulDouble } = (a **. a ++. b **. b ++. c **. c) - let ghost example2 (a b c : udouble) + let example2 (a b c : udouble) ensures { let t = 1.0 +. eps in let t1 = eps +. (eps *. t) in diff --git a/examples/numeric/add_sub_mul/why3session.xml b/examples/numeric/add_sub_mul/why3session.xml index 298b5ac8c..e4869a51a 100644 --- a/examples/numeric/add_sub_mul/why3session.xml +++ b/examples/numeric/add_sub_mul/why3session.xml @@ -48,77 +48,77 @@ abs (to_real result -. ((t6 -. t1) *. t)) - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + @@ -144,10 +144,10 @@ abs (to_real result -. (t1 -. t)) - + - + @@ -155,43 +155,43 @@ abs (to_real result -. (t1 -. t)) - + - + - + - + - + - + - + - + - + - + - + @@ -240,10 +240,10 @@ abs (to_real result -. ((t6 +. t5) +. t4)) - + - + @@ -251,38 +251,38 @@ abs (to_real result -. ((t6 +. t5) +. t4)) - + - + - + - + - + - + - + - + - + - + @@ -290,43 +290,43 @@ abs (to_real result -. ((t6 +. t5) +. t4)) - + - + - + - + - + - + - + - + - + - + - + @@ -379,46 +379,46 @@ abs (to_real result -. (t2 +. t2)) - + - + - + - + - + - + - + - + - + - + - + - + @@ -446,79 +446,79 @@ abs (to_real result -. (t2 +. t2)) - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + @@ -567,77 +567,77 @@ abs (to_real result -. ((t6 -. t1) *. t)) - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + @@ -663,10 +663,10 @@ abs (to_real result -. (t3 -. t)) - + - + @@ -674,43 +674,43 @@ abs (to_real result -. (t3 -. t)) - + - + - + - + - + - + - + - + - + - + - + @@ -759,10 +759,10 @@ abs (to_real result -. ((t9 +. t8) +. t7)) - + - + @@ -770,38 +770,38 @@ abs (to_real result -. ((t9 +. t8) +. t7)) - + - + - + - + - + - + - + - + - + - + @@ -809,43 +809,43 @@ abs (to_real result -. ((t9 +. t8) +. t7)) - + - + - + - + - + - + - + - + - + - + - + @@ -898,46 +898,46 @@ abs (to_real result -. (t7 +. t7)) - + - + - + - + - + - + - + - + - + - + - + - + @@ -965,79 +965,79 @@ abs (to_real result -. (t7 +. t7)) - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + diff --git a/examples/numeric/add_sub_mul/why3shapes.gz b/examples/numeric/add_sub_mul/why3shapes.gz dissimilarity index 100% index 96a2d89af561811a5aec13b655193a050c8b8504..41210f06dda52f6a4a083a26494481776a3092d0 100644 GIT binary patch literal 5243 zcwPZ}6ol&^iwFP!00000|LvMfj~mHyh4=gwy|guukne}#yE0&C!8NxR`Gg0Ukz{p` zVgGx7QN`w?n`ET+i zf8LaT{oAKf>SOu%sXTrC`}a|PE5H20Tcws?j&GI2t6DyMD&yPZ@}bKSoAUTLzCVrr zFu#8P{g2z^pL6=S=k>7TP5E2-$l9MX)XsmpxW5^pRp|6fcerQC_pb0Yu=@E=XDB*m zLBRBVJpS?9Q~5x8&ePg2ZumL;(_MRbk(}p8AFy>?$~hWdym=0eHRNs(o~Pv$*~^RL zgJ0+8UC+6Ew~Kgqefb6apDxqlY4Uerr+4adUU%-ej>GGnm!IO!+>wKw+r_g>JG(Rd z?`3J*eOh*5`BQJN^|1_EC?I`k*B5MAq@1 za$w)SK0dXtU;3|4DCngX@6xNqa)8gT^x>5`yt40I?AiTJ7JGKj?WB@vl7B z)4n3jK7tkL^{`LYck=$Xi*^?pl1xx>`o_ZuSpU*@KkRhdr!;W({*fqFQuw$inOjIf z2tvvGZhftH=0FO4JdN+a|N5nTdAh+16;i@MfT~$SueNOCp$cZNX;*DcNVPA z+O;zUy!QV2o92c#ubNDzwB2d9)BgH8k0F2VI?v?$=;_TBxz|_ZUTxXjYWA~ed|qG2 zo!{=_v-T6@pS53amri2^#=!?X{^uVY=-RiZzMfA8ez(opQf z*-x)V6+bd8yV8}vG4Z_esf)wR*O%{`K>Q!)@7Sf@`H=tLxjQf2_ax}0{e1HScg9^B zEM8jZ3mfp>vOQAxJ!^k2Vs0h)*0pm7`?FGd%?aFG$#oZS>od1=ExdbX1>ofUeUNui z(4AXawdJCci~Gsav2VV))9v~CUdjC%P!N$mA7+Yj9~2S+UuFKu@%y^kqM%2e-ES0G zbv@fbT}s>=@*gwunuh(k=#$p4kBsgeS39+ zW;Pq6)0{RmTT&ijmQ+(JeMDWV?GdZ%hfHJlM}#Z)UGSyP3V6deqv7($OUsS~E(yXysmNlZ$K3+B8#l z&c$T4O^v78ILu7ea4)mTy^-V`Mzg+Y>xz|2#aeAl(^+n%Hfg9{{2WTPK8j8y_u{e+ zDp<{0rre1z71d~}+o?i`ooy*n<-Mx5Res3>-6q=-vhAjunrBmL2CWsV_u2;)iz3Kx zlApR-=Ur*BRcCDUIT~BE;m6wKfnhUa(SAnFeR9!Frs_`RP_0H&?bF8{dr+x1R7!d?uQuZxqm6Y|J)A7m= z<$IemwbGSY4tY7jsh!Gx7Q<U*VbEu?Qm7uNmD#REZ&4`V?XMS!H1s`bTOslF6=c6fe=HczY2)m)}FixWUPt5#X zL2A~JoX$y)F*S^!^Yqqs!t-=($yeA!>ZPUWOHw+KPN3(2s`5d{nL=F3P--k#3f<|V zi~@9~IAv8fv!)90&DfW<)U2Z<0*Kbb=vr-Z)8$U>8QY2W>A~91)@)o?uBtGBDZkRJ zC7A$fLoc&Y=yF4=H@#6^!4(C>YSp2u-eDmAtJOs}SfHhdl4?|X@NAd8P`|NzH@b%< zdeM$3lQ)o%@6i{|-G^8sRp~NI(hW|rPO8Y*x1+Q~4d<%uvxlOgCn`+vHKxseBt=uZ z+)DzBF`k821|`uRU=5Cdpk-?l=sd$3VLud-qewmwRQFxVVXIcUG61; zK;C&@J4wl**akC@Q(vRzf5=t>{U);?Xs(9XTC7TW?+tk##nfI~T=Ee%Sv81B=~Cgh zR!DwOQwPp?#93;WsCZ{o8NM1o+C1ng6{_{NRz=y2o*>eNGwurVAygg^o73!|St$dM z0>PG^ot64EX%j;B35aGnN$N8ITTN9`7s1aI7xV};jO3;QLzP`Zz=oSV*rF0G^S55n zC{SyNm4;T>t-r5Z%Ba_k^4#|N)IyG%Y@@ICQJ$`mzW5h$0l)Y~Y@CAp!aSgKWK z6ji9;z^=O@@lz$vILDqF3v?tm2->D;0oav^1ccI~tqFo-8B?OdhNH_aK>l8tGy=e# zRBNY_p=LKIyw5hj9i=78K_;nY6EYRtVwg4O6wx{eF$5#&weIaGEm0hh?FB0Lxs(|| zvvau`lZp$|dcWLD0>NFbaCC#+C*-d}^N1?2Oi;QJUbFt~C@oPG?*vG&g;pVFBjOSV zb*!R?KFxA33A9*-+yc3@Er8hCVY8wk?r2?aOV+{$ic~NZm_zH83CfA6gxpdsx@0LR z8#lET9OHzh_eFPCl$#1c zMqYy#j)kl^36Cp)=!;5Hnl^1LTk;cE2LE%07$;vx?_HJVF*{*Fk3d6`j_1o+2tHS* zt-)haB=|8TR#?NSx1+Q~4I3g^j9DX}7^gw80m7L^I<6FG&P}fE3S%m zSQC-1A$05XCQzJsvgkSt-lFr^2pF^}kiolhN)Gqd$}9z!7?V-6r#PyEyE8mU6;EMN zXYV{F5HVo;S+W@}z(W@E8!>8-=+sgs&fR%Tcs*!SH{30p&{MDzr1dV$ROZ5H4!DMa z@r#rjh9r-S1Wn#3lTya7)`c*H4WJz>GBFGaTr*TesXH}AIwwlL5|FS<#I#xoOCA#q zEsPkV#gZj*!|#V+J_pVE63&a7!&eShV$`_N(BKe~TUwVJ22QG1GcANzbDR;quf~T- zF1X{!#jrr1H<9frG_K)SW@-2eJJAUlk3c9^9JEiHR3ds_T?xro3Xly{><+~fR`5_MCQ$B$mBZ~LuNpG2^1#+Pb4)oBi|?3X5xm(1kO$gr z;PhCx11bqq#46Z$RBo~Vpw4rKvFk}zwVk2jd2pf81Hhsd`(LGB5>>`8@n@XQ$}jlJ zVw7ju+ka4ugLNX;1`t)muJT+gbi^*H)&7qFcxvy3lQ*(cIrUg+2cVv^m<{ruV@=z{b8#6ChW&xEilFrGseiyEWq3ivb!gi^SsbV^DfI zWjVs^sSa#=<}uXRRLDc8P&{XDtMdzJ1QCCs>o0WudFX1+aon_nIQE`=!Ap=hC2O+= zno~R`%(@QM^FOTWRCWG!a0^$|L80w+>s1%uZxa~y|gzoWP*#?c; zHG!xDV;F5RQpOlkM2o_Re6USLckS`XfL3-{L-(}p+PA4n-_N4T2;Jof=Ch*1XI%&p zHpsga#pmp2Q59&S_L!fj@eHMC@T+51v>QoJyUwC$&8$(?4Ei)6&ka&HbgwnJCew&@ z7FCJ^8r@EZZ|D>R6--9PpdF(FbI-G=Om~*))oC9pEP(OpvD&I}VQR7cT5XawlrqU^ z(MZ(|#CGC-W;U7X^$T54h9kffbTqNeru9(9n}lJSCFy0523=%UOG6QGxE(JWqoED} zJJ8N!Z5#<3E@CvY&&|6zYSYkRrnl7^_c+aB?KVbIY8_`T-hwu-7&5{Ao0_WEbruBx zBVgqGcxuO9a}@YG1rP>J!dU6T*f58hWGVxW3l)py33hhz8bw< z@inY@T4zzxSX12^Bkg>^E=6EqNN$W)n!I%u#Yd-et`D7L)>%V^%`6hZehi*-okdL- zv}nViqbUMvm3bEBq*61`|2m6m1Hy;kl=U>nWgt-k$53QMGOb!?Q9m#9_a#+T+~afw zxYKS%C_H-W)1yVD&;@(cyH$Q8Q#3cO9%fN8&G4FrmyW1#ICSgM z1Hy46kn&w;QEx^qv#8NL#|TQ34DcLn7X2{;{Dmbw_QE}`p(H5jS3$-9~ z0NlP?XHm2?uF5}3RK<<#=@6UBD7mI-WUFDFMbWDCEX7BDyQkW8!`>v*0N8Nr1TWqh zg+B|(Zs-=;4LFq875r-0n2I%;g){C7Dp(+_WJ|UCkZ9ftBt+8_&?M7LSZ7hAj3N`a z>PDQnsG#vqQu<^r;zbU#sDfTY)tIX2#R{h8S^ms2SMejI<1EUGsY06ju!9atvAJ1H z<<<$n`?Q}$bvHXr9n?SN%L-L#}OFFo+9yZHk2l#HXU5Yza^RQN4uXz z@qo;3sZmI*dt`9Ixc6EVY^Ze>Ww21KBlo?OfO@OY2idaY8gi1>S=5_R%PfkvnH(&mBOa)6*8`PM8L4Kwqa9{Za97}jNNdCY z(6obapAEG&JLNIfS=5_R%PdMk9>c1|b=kNHR8Aj-gI6xn{_A289Ryny+{U6& z>As)}!h)>RQdqHe%}z{TzN)h<%M405 zQXjN7MLTV)fd-~WT3RseFpGjr$oWKiX}Ayrk1Mja;iYlVZXFA$x1*L>l$@pYo=pq` z#akd=tJCm%DKro1FpI+FH!42)B%1DG^>I+78aL|E2e;0m3NmkHp2A5r90E-oO@{^? z)CqoYokdOB$c_<&OoO8H!X;M@k=)w>`?_@&b=NT!C(>mnHAzjEkX`2K8HsJ7!6)l1 z>b_&ro_^FwLs?OkSV)``H!MT(q8H!d{05pDF4MPge%NOj6=s|ZV&Ul)tvSr1WWVCW z8puUel)K?L(!}>u-e|hj}a#=Ud)7nx7g33 zkliR>cT;txW*S?N3@l{CiTT%kofa5{T}HHM9|3qwgD!(5T1^j{ZHeo&z{7Jm@9GM8 z#^PY@3KfttEhi07U#A7B<6SH@0%y>|YiV-}ei|^LHEI1S+W0Uyc$!=~uLg2@i^&J1 zI0J~{7yFN~O5_W7gQCzEl36;nNTU|#h~xRI=mAcxvK2yh2nxMd;lSZ%kiH*?;0_S& zCGVLk^{7am1{OCIQge8}#r}s(D+REUD7lW5yKmyE@L}``%U3u7*M+GFgO-5Y4g`B)7#quSWJ7hEK3wNcN;-MMVruGETV$=*6%uhUJz`MBOV)9SpxP6PI$DJRi1t}9V>F#Xg1eSj?0aIHmv!=Qb*?wB^7rOpJ z*Pn+jm_5L^=nTHT1@J&)6tE!G;y?6$7Ijw?G-|!UU1JwZ*BE=+G5Mz`Xv9#<_e4J2 z86{up`aH>8M9Y#x28SCsIZRb|E<8_}?up8}_nPrebR}54is((>kQ~|v*UWwvMe{wA zmamk-y2@O`_Tl}CbQ*Z$!z@Y-;M2faFIgd0(n!RR5={l!N#i(+`d{_aigfcp006H4 BWeorT literal 5239 zcwPZ_6o~5|iwFP!00000|LvPgk6Xufh3EVgJxpX+sP`kt9R&z9=rN}k^+XKVmLkbP z^6&HQI&3!CO|mInIfKBq)J^j2Q>SV_)>?bh{-<{jU;d+f8ebm%YkdCl%g5jUaXYZE5;W?*|d)f~t-j%@ z1xcpQ1r2p5;uz2eHec0>0y6o4zd)~+K_1??7xHotBVDI+v?9$%u z4S&6C?eXB2eON#B;}!oro}cRR#IcXBJn*>I;@8okk1x{q$7UkWx9sg_J$}|lCi%w9 zdR|ik_UYr7ukGXS{gBzK*?K3NJzH~y@E=*>@te=_ zxKED)F(fUo!=peAIc6UB?ol9TulD-icl&=6QSdPSyZrX)*P$;)U2v+b3c3)Wr{JEr z=#tU3@{+adR>{{nL7|VY5vM-I1%{VW`x zx7Ts+ANTQz`!VuQ+^-*3r?Dl*Q3rha&p!z0-+%x3`8R7K!0NYt&^im zL$P;f?_P~6zGql=r7M49;(6t+i^I&R;-HuE^UWLX zw7WD|ytL65GT>Xw_8G$O+55L<%q<7sx^}K$f0RqFDS?|ixvm0k-E-U5g1cu@08Bot z1HB7_?%itD)350j<$L3g?6*{UXVC+t7BAsWw&P zgHa!J-qoU2PNk|mtd3SYWkSf&R@3UxRzK(uI_-R&I(Fq|4727uf~vI#J*Ir(QWmSY ztG>)Onob_0IeW?}%^p)$CK=W2gZ-fOuH~e>N?lcxn;BEF=U#kG%?EAOkhRoKyJTx^ zwz^b%9laV((%5>Brg^7X%j}AZ-fN!;o3bfXH%uNT#aPSiEqj(yyO4tQbCw)^ENCYjIemhfX>8U`^DvIj_3G%rBG4ndDAWH;`?@?7Ps~fFMo$S+w$u2bsS(+G{T`Y0T&`38^cwJJ>vO8maD%NC) zv$i|kwKt@LNwao2sgJP}BQu9B+%8sbM`mOdb8)6L6=F7R2D09CZ-Sq8S@|F6`MZoP z8^;qZxZ0A7!TS+RAUmy56p0w=u+yRI5U4RS&}grCGot5YGvr))U1caWMu2#z8zXt0 zgNZidgE@*J37u|ZD{HA)XD!>xl$z^$lBAtNB>cz_B-RwpArd;WkN6n%LkSoCmVtITi6=~nL(qiSQu2?)^l|VK(see+g_h_4Hl-yct z88(in$sm_GM`4HBicQwu*%F)>y0@*gSPh+v2O?FPO zwc=W8eB4y>=i@*wv`qu#Km;YCq;x(@nErSRXH4qlwh}O zt+kv|u*wv@0B%@>iq#{6SF=G!QTW&5TapmNnTe~f#Cj64kb0ozE%HOGh*PzNsCm3; zYt$NMC+Si#F~es9eIL?&Mk#mH$3Ub=hP*) zo!-I9y&De4sxS{_mvtI;psuIyD}kKZX+sG)P%2IX&LjPFEj9$7scqI1D|=st zI3$uNr8ZNTsnwNg-tI>6X(R+8?kvFW5S@J(|{y`goXXui2pkpEWuGtt;Q>Go{|BO9^ zreR7C>Z@46loC~G>|koWl5sa$>NP^<=qR*xY6cFez+dV^g`$`I=h5O()igAiTBEm` zPSH~-eC%sn@*lvqP#+ajwaZ8dnk!4%Bd4qfO;=Wv-C!Gtj*uy)Xq2)Y)B;)~NYIzQ z{BcH#LKgm^NeLV@C4-AJ7199$7X+$3eWkS=N4hdc^VO3An808NUIX&Mt|&_gX$nx? zQgSnEh@9jL)QIae3EjD}l14J(uk89OyZ*fFDmJA7LL*Qb4W__fGN^B_yK8fZFTB6g zszvQ|REVvh63U7EQx#=H8>b?KBv#>0s~JioF)fW$s%185kCcrxS2Q#<3L6>SXGI2= zEG>&DYkCrzM9?3W_w*B{3;lUiN;i`4)rTg70dfW0h7tORa74B;Gij?W>!^%KZ*FOugl!MAs8L6Tp-QGVOe*6BZ392d z=uJ}_hgsCBxbp`;ZDQSE(UETf|9?(hDxKkW>He+t_ANI?$phO&>{y#0d*kEo75Y_9UR$W>GTMFvv(6 z*+5r36S~#L-T+xzkrK99ltE-QdP%YnDMigy)Fe{gX{4YoYMVv=_sID zI!|Rgtbsb0aw2{EHj4^ys0jZslrWGM{|=Y^AehDUe4ItqQB4PuVnUzeO>W2(eTggw z=(XorRGVHoKlm4T@HFlz>e+xPMN>Y~ILx8|5M(PHEEUfhkScAWvO@|UwSJgI1&Nx> zNvv=&jRtVV{+n=Rrr5SwRI*BWnkkm26_R~n4!z{`rgY2U) zbW2Wp-=-#zrKar-6`;3SR5gY^HZ@dL@-llEwAeC3fw3Lk=r)Ub(`wD46cyKDd1vTC*tM=)EC1B(S1#sbq~1_7VmdHpb&DD%%Rfl@Jid$ay^o zeveT_4;N=Mw^`JiR%;ejWVC1f=t}EsLGg+3LGXElN<%0eXHk)gg?)!kKm{6P3Zzbo zWJMvhZ5D;Ah^NXZ@Jy&JoXWDwhXJp*7PeW`G#&W&5V3_G3~hlUIx42I%wZPwmera?N#6sirk24|9$x^p zWF}-&`v8ECvnT?Sm4)%pG%}vHiFo={>!51X`hv;n9k7jVmeG(U?8QRWj!>aQ>nt|p zZ5BoU5Q>PrjF2FRB~FSMscI0uROvR0x+_e$$wULdApUHyGNs8~dtJ$E&YQMb)V*OE zxyA_1fj;<2MbY_a$YBC~VLi;En%5Io>u zO@Q(+i)ur-5IqMLwqo22^bLa2b7!n*gdg~9fC^})} za|E2BxLl?*ezuGzinc3%m=HjAHR-Rtu#>aXnjE4%)* z?8+S#93TQ)#RuIWmU^W>U~L40*``eQSs_IIj6}GAybbXRT22RNR-w}M^^XsCT1j&n z3H_`HVXsl`#^h>MMa+1zb|a(vtQ-xm(Ln}1aH6FI - + - + - + - + - + - + - + - + - + - + - + - + @@ -112,38 +112,38 @@ abs (to_real result -. ((t4 +. t1) +. (t +. t3))) - + - + - + - + - + - + - + - + - + - + @@ -155,77 +155,77 @@ abs (to_real result -. ((t4 +. t1) +. (t +. t3))) - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + @@ -253,36 +253,36 @@ abs (to_real result -. (t2 +. t)) - + - + - + - + - + - + - + - + - + - + @@ -292,7 +292,7 @@ abs (to_real result -. (t2 +. t)) - + @@ -336,38 +336,38 @@ abs (to_real result -. ((t4 +. t1) +. (t +. t3))) - + - + - + - + - + - + - + - + - + - + @@ -379,7 +379,7 @@ abs (to_real result -. ((t4 +. t1) +. (t +. t3))) - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + diff --git a/examples/numeric/addition/why3shapes.gz b/examples/numeric/addition/why3shapes.gz dissimilarity index 100% index 0bb1f70bf87d4a828539803345fe7cb1c4099795..2739e809010ecf9c5764081c201c27710fb3c5e0 100644 GIT binary patch literal 2779 zcwPb93MBO(iwFP!00000|J9dEZ(O+%h4=SYXqniE!S^G`tO5jHXx-ZZSw$iSJYz$0 z0_5N4<83{$mMM@7kA7Ki`b@vAuoEtJd4w$5-uP)!UnQZG67nKe}wOwcFcq^JVDO{B-ln zzdp9_Ifd8XJV?yD&t{mdeg6FMKUbe`#xEak$L+<_;oNhv z-+%ge-r3V`aDO=AojyMt|5LjexBvS1Wlz$5qU2&=_lEDD^7X5@?<_g_#EJFh8{uBu zM(o2D=OJ9OII(&@l7l;#Z##Q%``<^)gT3U#!Jd46{X~S<=bm1FRjwb%`I{YUY;7N% ze|rv)cJ}mDwztopZokNPc?ZZ^bg&JoRKetmYGg;Kbs4HhpryoEZJa=f^7v3%Mc--P;W2lO3bT$=JPX`Yw%%0)Ch7s*Q< zKhqA6v0u;&=gjy#n$D)#OY-o0(Dqe{?w98S=%qaRqd0wZ;5pv?jny}^b_mS0eQ^2H zqtP+$Jkmqh|JwV`6Kv{=HZWJ;T7`?CB!T4>mjz)f0;8e&rul;Y4%&j;Nm3NoP;~>?xc*#q0mY89$Jt zYf^qxbk-dTPwwu?EU{)%_q#oRJh)(%PDhi0TD^{G2otTo15 z+4t6NF?uJpSu=w)quu3wvnnBY4ynt^Y{tjhXU=?Hj5pGqH#wVTo4BGqU-|cL(=wv3 zVVW4cv({?2&U(|`4Bd}Z*vf1^#hhxaBcza%W!*z6Nep-^Be=B_W-atA-p8K2m4Sn% zMAM7r?vl&7Viq=6s;1v3^|ug2sl)X$$z_r0=A0OnS2WT|ip7uO zb4n$|45fEi1dZ>Zhn9 zL=BWiG^!zVH;S${S)j0Gt0pvGi7iz#h6Zsd)nZGxVbESX?(9 z-Jm;b;pL9#(ngQ7Ngs8&m7Me%wV6aKcI{zDG-P3WuFW;C-hiZ9NCPyYYFcW2$KmT4 zwN$2$twT!1Q@0${PYM$(jp+AQv}tS8H#@S78cOm-_v9~t84Iq8-K)Gx*u~G;C*)S6 z(?R1T=*M(5X@J?42bVT#P+bA+l?*tEX*MrCK|LBWr&B{0H#f&BYNBgQtuq+s>?Efn zRFI)-FIxfN^v2AdRmQ?z51G!*6fNaAMp`G@4HClZMCE*hou;l1fs#g)7E@V}cV;WI z;c+ez4y81eNJ_{GU{iz89 z6o+4QFZQZrj`Z+o!rK(5&=0OS=quUO$wpa*nX%Vr@HQ|An2QxA$+mK%HIiV+qgC0w z+U}e06ZV~>lGY_a9vnG}<22V$Qf;K?33{*|EL5rs=rzd&=`Lx(x&W%CGOvM91d(hz# zsZ$(crLDo1bZ2wP=%I%9@CiK@miaEJU zkFd>@XM`A>X{e16Q8AIRMjI0z0NvTV$B;eq9D0k8BBf3E)C)r>X6KG<9x~Ief&a-6 zYt@j`ENU1!CLxOA-jdd-;c`L4qYGgslum_J+v36uQ|{n-J);o;O%D*I2|Z0ZhaL`v z;hdBKHFkYsK;V=zJi?4SDjl!Pxc)xpes)F&1O zux^P5v=1rq{LhwAY5WjYR(E|;CLP$;_{TB{s#ef3v;=bn=_PmiBn5uXOG@)+mKtfe z-03HgPDT1rpJ++Y6vM#|AJ|w8p*TSid0G1Os87(MVIdT);F}`D;NUv!+TOO1#!;V` zhLmPnpi_NdYBO`vY9wbQPhK4LNuj4eUuL`r{a)b(l1rAEo(S|KqNRX%bROVhk~#%> zlW7rpo#@=ucSJ)a5D}Wn>x8JZ-~gJbrQ`!c(cdB3pzz4QA0E{OLMcM5f&0Zwu9Lkx zeX>sP2q~si@6k92R$^($a^s8N5xtz!oan}!kt#7YL7hf3CqW_=cSKL?0f15v{s@fY z<{GYuBnH1xvm@Hb?Br%>M+H}SbvWXxN?Uk}p*s#=&&b9Wm$D2<@*$1O*C@^lL|7&o zyBzfiV`uuXdXKvhLN=N;x{wY9bzAqXj{2mb8_{Q_0R#(g7UUT>vWfO}OQjt3NnLUq z`N+(J^`ZSCix8lF?qY4^qdrlT57d@tXQD)2BZYc4bjf6<1$)#dK?E^U!Crxwv=J=8 zKqBQOb*ek+6V#P$3w4Nl9OOwQH|6FTW{13w`UH4;sU7)S1Fhw_9+3q+H=YS_oRGVr z=i0Xb7N@UmsE+CkDF%#)^*G&8pM-(tGQPPqy1*7(#MaeCN>>eF@u*K;RHi=|I*qYK zKzX7fQ)4(}l)D@Biop1--RTozh@BzEC1sdF_tO7tiss8SMt;yIE~fw}s;o;kfScTs z9r*xt9on}?eKMfOXvHIxXA-6zcSX%}`3R2G9rXz}fiBZF*pnp($j73gJ2_jL*I}51Kpb6XX(~A)Ip~N|M4>V`-<>m>E?c^a+>G hnI|J3iNSpz(lrCIJn77ynMjZNx(+aI6w zM^3@#Zywa#yF1t2qIY+n{&RD8-+%kK@B53VwUeiH>%-dB?)cMj!-pN7aqgwqAC^9z zclNd#JRFYjPT!Bm|DyMO|Hr20SPjgDKK zhj7W_#OmcpcD!@nc6P_>|3}LmUGiZ^C(Cc2iSYK^)7vNI`iY#sS+Rz#>CySO=K#^O zwvk7zC%|_y zpJjV?JNnnM`{!hj8?`O+5B>iB^Zouq)&0jd8|17ruIQ5|_W%Fw@)H3acK@C*Uh>3F zo}T4a`&KMn$Ehd%_%xmw1Sb|hvgxw}=EUeLpC1D~d%HL=P7iy@^$pAR=1>)^lZWp?+mjMKJf07rYkBl%ar)@MOT7D))i<-Y^O$Mt;F8m$p=0pP-)Stp&n$=RDfdkeS!i!**AN4H4%rs#-w8E<@e zb5rb*JF2}~{CZG<@fLsUv)_g1RN%6xGI(4qwd|6$Hlk8fQAs0Ow0c9~J^3ZZ+(&TH zTN*mV_huwHz^IO%0^g9lCtgy@oT4AKv!$x|ITx#GlpI?hk#6Wc(bA=0$zZmTbCjsD zv*glybh#Ie)5^eYpF)DcNnr)>?lJdyBm4W3x#TxM`VRFHI*P8HS)^b20QPu zm0Kz$S87rtpSX1L!<+BHw;0J)$8#r`^%hI=BHc~5hg!EtY$2Gh%}a;bOhoOe5k_B0 zk}_QDjBvdRrP!ziMq$Y*rLHMx<)XPy*S&bE*gs_-D~#fz#g#@#OOMHCbuNdh*-H({ zTxip)w8ZS#G?vbDVe_s=HgZlK&tL>b`4x@2>&OafHpn5yoI_7cNPLh8*QQSeMNVub zQ%6M3k)@EClaNR-13K0s&k6?Qyw8w87!i#`fyFtLsv&cvZ3E3jMC?^dL4vYy=mp`^ z7&X<}5&>*)M6*EQ5a z(?Q{-S{W2ZWfUQd!i5v|1rjC4$T3eVT9TMFiPWjFCz|MMy=is@ND&{A5y}hGh&YaH z_>o46)teb0prI8jzRi@RMLVU&H4JHRwpz#~lnPXIW8ZZ{bkPb7Rhh6^Drn*#rI|BLA+SgQ@b0!`CyKd2tQR2QXwvXDiVYSk4A2ZAEAO;u5J) zE)>+rxzb-_7rRmPZ!kBb+irZrZ;W=I{$ zg^^l`0vhpJCbT##;uyFDeZ|VT8N%t1D8sqYht)iDN@a;nWK5!Qh=3%e;jyClR4mj` z{X7vcMc>vOxWthp!>b^QDpbOLC`O$px&Uz7UvkaKdAkt`#%IS!CT)s=WBtGd`- zY}9M*6+GQAv<=PYl{Li%Rgt*OrfrFlsiECgHfL$z=Ty5vf&knZ*%GLe;=r}&`<2Z>KH7_q zIR>YKdg4G&B{y7FQfuwN<|Tot16tcd0L>=03~munK7uCN*c{ZHG5tb=p$9GTq-r`yysF{m`cwpCkO(xu!g zs7GC)fFzhe`}FLSVU$`*8+cyL2;5evVbC^!v0!S}hKbt=Rg9{stop?3^pC?-v%Y!- z&0%mhsH@&)UXS_&AVS-r*hPAS*nti$v#)a!4Vbr&`o!y~CX@kfOm4vhguG+#9HpnO1~maPb+$$PpC%-CB|Iy1!B;Ht%GK?Kw$u& ztcVT~>KJ+$zLnY0P>>C62KLWGS>iUXUd;$8g2f!5kes*$O-)s}VI=tEz4}d`h)>Bt zrPUWOeiO7et_zs7!#nls4QA6P87cIcaxDeb4V`ks19aQ05UA*&Pin@Gptg}QvnnVq z;S$JWGX4mxn?8Xyz&#)|h;tk8$5DrH6-F^}dDFV-6LpZaRHcmS2PFb!4Ri|OmH=6^ zatZVa_y!vRP7d*66NB{4=?m*NHn@s76a0XH$+$1~;$ zE@SC{3S3WeMfD=+-9R^>Ib4xb59nSG-ha?1MKEA_PRuGux5E%YGX@oL9-qgiJg&2P zy@X-j6KK_UAzZA$7|f%W1m%V)jpds@nOq98ijZp!3eB2Ab$XA1!VIMokNTw5Abxm` cSdRM_a?YN+6Km@s^--Vv7fLgpVh - + - + - + - + - + - + - + - + - + @@ -91,62 +91,62 @@ abs (to_real result -. (t4 +. t3)) - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + @@ -155,7 +155,7 @@ abs (to_real result -. (t4 +. t3)) - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + @@ -261,7 +261,7 @@ abs (to_real result -. t) - + - + - + - + - + - + - + - + - + - + @@ -327,7 +327,7 @@ abs (to_real result -. t) - + - + - + - + - + - + - + - + - + - + @@ -396,10 +396,10 @@ abs (to_real result -. t) - + - + - + - + - + - + - + - + - + @@ -478,62 +478,62 @@ abs (to_real result -. (t4 +. t3)) - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + @@ -542,7 +542,7 @@ abs (to_real result -. (t4 +. t3)) - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + @@ -648,7 +648,7 @@ abs (to_real result -. t) - + - + - + - + - + - + - + - + - + - + @@ -714,7 +714,7 @@ abs (to_real result -. t) - + - + - + - + - + - + - + - + - + - + diff --git a/examples/numeric/exp_log/why3shapes.gz b/examples/numeric/exp_log/why3shapes.gz dissimilarity index 100% index 342a58515b9396e2de0d80b61e4316be1b087a6a..d3ec649482de105f3c92eeab335c05574b0d0db4 100644 GIT binary patch literal 5459 zcwPZh6|CwXiwFP!00000|IM09Z(PZdh4=auT+Vc(HTjIp9M}tE0HX|O&8?Bo83VE< zi1I-C_w!}3M6#H-Zn4#rdw{mPN!E=U5gBpfoQ(RnpKk8{Cx7gBH~-r|-Tm#uKmPMZ zZhrdrH~9~Le4F2Y`0u~=PoF+~s`~9m)zzQoZ>u`~_v0TQKU?oU?|=T`1NYD5a+iO3 zn?HZ}>!+UIA3u>le*E;|%kA;w-~PZ)KfldC-GBc4_YY2-oBvDx!^3+YKK$ngN6oI6 zX5U5g%}0Iw>A}8!;^EWZK3d%JN(kHk(zg&MGed7a ze(LqZKic0uQ~Ot{^4xo zar##zWa|jlOl*DXm*WTd*9pt=f4qIs5iZ8QJ%6!`?(X`h&%ND@51;=2&-eLNV%(1G z(S-{!K8E%Jzkk1@_^od4!0_G?e|=h;uY|ELYRj+J+VWWxm)i2{ep~Jhq3;cSE4%xr z{`ET>@aty8uUg2LL)s4Hcj~uS&-{0}xpwpBZ!bUab^Etxli@WS{$u{s@BaDzbN>0~ zw|fY-mFdk>`DX6zHUw|x{O7l)&p+|;RO27-=AT}k(le6}8Tokks^$2@U$CFqTYu|* zMdoh(@&D%|w{k1*ez^DV*0WlFb**|n>-_oGln0+b{_FTG`pvxg_~GvJt~9vS$DHVJ ztL4|^Q-}M1$?@sPKfgmxZ{7MU|BjH}%~rnE<~H(^`O9Y9=1hj`OZr^zyYnEV)t|PM zvEuz|`~B)XlFL$(Xr3rg_wF`s8jNRd%Y|^{MbXGsF!JtJHs37g2XHwOe-?@V^PAiM znxyxpf60IU_`d5c#Wykexu|*(`aY#nyGAZZ!2M^gg4T{`+Wyej4QSZDpE&*Yfsy_3 zT717cg;(=+IlA+Cc2)=HDDpxRPr>Bz66chcmwf2|V}N_EeP{Vz))ChW`C0j14}a&+ zPmyE)ldBfF^5TC@(qDA=YqnqX*kwuc3V~gB;Wsd@7l-)5d|c%P*Anvmu{;pRdq()9 zJ$d(nbnIoG;aESPocQV6*qFb1eBTAHe>(o4&q&sHCvUQ;BUgNqJnep<6I*%XxSn&p z-<{pvbImyE(IsN`y+rTF(k-(^w>EFxH#ZP-tX!vH=K1HhHcStHd%wTA`u4G(-#%%i z^UEtLYd*C7iSIFbx^ddI`?AThhWju}%=s``K6&pkVV;{6As->qJS$o(!WMVg9&Hm(3l!EN{80#qS4?yY*XpZ@=}Fdp-i} zm2%Y!+;6VopW^rKihtMgLz90qars3TQ0C?DzJ@a!F1!F~wED47^YHD87h%mcpRb1Y zG!NS`E`9QX6IcP~dtdTy*ZuDTo!5+a8+TqW*cW5ZlkdyOX8+!!&$BoEEAYo{eL2To z{Bq8l?7a%&O03#Q4^a)If1Dzr&=pa>ev9?6x zlbC^>q^!{`#v825Hqs8=UYx5xwW3@}Br5u%WAyyldvd2f=LED2in+AICDfpsn z!$9g@cZb`lyKF-aBiuN3u<4-vj*Y5I$X*SiFx(m&bjFRKIsC^q4Fe$YWdyh?A?Pes^;-K=fGN-fE z`!+~N(Zkbj-S$wENu=jpx?bg!nHCK~FMekI|stwJ7b(7k$Yp!I4LmgJ@ zD7v{ynPp={D0o6tsVQ}|apiQx)Y44JBe)oBFPshyE!s8B;ha)(rCK{h<=imRx?{%GS$#Y-Lv6n7N5Dx8rrD)l3v z>#V%5M;liv{xzyqO43R+r~{x?P}P{MOQAAGw>6g2*Z4ht@;7q7Nnn z5ZbpgyH+K7R9k$tOa+@q^d&hfJ(V~@vfdwi*xGBD1}+x5K8{gHaxSTKFV50Wt^{?o zajk1!A+xVxqm0%up-V2k#_pP}DUac#G*!jir}fILc?}zxwz15npljx&V~>gPkesO? zZkA)`*(;rwYcY%nW;U(U4J1YvMjZ|0b?kPW=J&Pnt1OT{{D_RX8ck;ObS7w35wC1_ zCn|A`2{7`thXo`byi~@X%>Hf71^S?ba3kvAH;ICsfFYm@wiNqm{lVm8{W%~0Z<&wNWGL!kE&jrv&sxnmLITnG~jm( z@G{4IZ16T~T&k(?zbrOdJESHzi^=O91Ij^H8Kw{)hHdi0Wv`SpBBG{)KYE~c48#g1 z=`eCCTAb7Y41?(*fX3RHexf})IjGccvO$J+Jun7h>B&RLlp{8iPm^fJ11L)3eaiS| zd#gOuU6GxJKJK#Hv}T_=s9gRa7P z9yDb@B~4eyLGIGtDU9M_%vQm6Q!0}Mv|yGktQEw!U%)dWez2u4A|X%vMngjysth+gC4R}HHcrpxiF4g z#JjyT=s`0V3zeDz0KX?H=7_SZUK@KFbvym!;DMGA>4<ZEI7E(((&!OK8>h6S$yV%wM$5LhRuWY~=<+HMkhin0@JlqMMcL6pV2#Y0+ z*<>pdkxX!{=wM*J3WN@F2!1PzE)jw#a0*_#WIr+(ip1RWLAlJv>c~fyAIz=~*%@Y&PBGhNt$`%yTDt2as@97fE$BT9;!_{addRCQ zLwor2Y^6Ei$;HsK7)ACh_|T{Vnnt}z*d;hpo|ixylsxO9F2rM3$(I8KtV@Tc}l}*fP#7! zI2Xj_NT((4S;(Vmn2s*}~Tc4^AR`SeYG<3=Ad?Ar1404|{F|kj2nnMS~RWNMICxMx8O!Y;V(G{zI#Gq?nh3&@f{jX~ih0~+2l zG>`H$>{{s5wKK5bOnD&iw=w;hFqP6hnubq@H8)b{1nV*5P;sfNhrY68xnM`|#Iab{CYO}QE#F8HG? zHx3@I#91^(72_tO`~|gW8V&2z(;NQf*~q}F3!J_aEjIh?2^-I>ym#l!h|(3K}vN_ zLW82{W76}g0(#`N-MZypjFjMm*Z^awU6aR0h*#H#=qGZK&Y^O3?P zHS_Ya&0Cn1x9<5DBWUBCTD8H2L1z_jRjGrnD-3Zp^43NFVuV4%VIok_XoLZN4s?Tz z=ppR%`qoYVVgzOzGIKk&+-eV#)Kz1;M6ffg{x@a;>&5``0>2h(t8|n6Kt!GvbkPC>h=hU36PF zbc+$`8S#h!v_;IAn=)Ua6=oYSyS&V?=vY=Hw*q^PVLDKuFRH_x+0< z#e_^mWGmH+fMT4`L@~{)ill?zy6|6-Bzj}TGLXn`8$(-DW3Ew>U^nNj8~?SJhY1!0 zFLr7wvI2vh+p1#wm}tFq<-eYhXSxb-&V;iAAq8RiENFX+C~Pr~fFKF;`mshg^46{YniCg&MqQ3hy@QQR zii}my%#JuBTi5 zrc}1>{(nq*U&TlRQ))>zlNpd8oG`yXRO({N4=z@;iW0DLpBEffn% ztmZ0P3xIVRQV+94U{f*i&dqlg6$;qVqfF}f^kfVEYCavvGu zGJ;KG;*x@7sktjF#iwNtu+g!3svmewNlafoD#=uq3C2jCSJ2NF0gHtUiy;rpC1_0# z8oKRLL)JM>eYLP`0yaoz>;+Li1g;wxF^Cw?F){+@#?3CPfOUQwuk=*58fA(QY#p84 zx`+EKL}grd0UMY;vK@^5sx-VcctcpG=Q+I5?6NEa77O^U=6D^B{&E^wOim@2X6KsC zs%0Cnk}6M0>4FM_*TFdx4>Na14}C~5W?2WUr)dHz9N_iErc_D~oiqNTz5V#LxRXJ-?)am}<*~{tvLw5`#Ed6T5HdNP+w}rx-@?)?)7Ovd?w` ztCWiK_R%;7YKdVexM4I=<4{m}^t81USSd^H4a!7wBFJ*g&JR=&(UcL)IBgcpZiCP7 z)P#&IXDT9ML=#UTgciIq_eAh)EwD*y$07yzB6h@v*VcfBu*fwj3RiAV@w?dBD%vmo`nONU(`aQoQW46K7^OuP+sfbVmX zRgOVJGltV$L6f&u18aF(JAlZTP?ji-UaQryk1%30zSXd`8(8OPLp+kvkPXzv1ANU! zUs^Q1yPzMJ18Y^;YAtyWz2LZ&jxe3y2r9a!0xy4d`?ujfkP_j~)u2A-8oDS*Kn3+G z$6MC*zzQ2ZSsi^tYf|}O-z>0KA5+oWvt{D49g7T8O3Qm&I+QxN3 zu+icTc&te>BUeFd=xnQ?6@|`^rL7x+HJ90UGH0#PkXEm$F+oxnj-}fa$GRd|NBF?& zK|6Vd2P2n})0sKmi&idbS$70$Rd%0)4{(nHe=e?51oJW&3NybI5jU3v>!CE50AfTj zaw7;6OXoU>q(UfcXXO+V_g%h85J#aedH}fCWD%w z&(H(lqs%3^bx*K?HgjZXnRC?HNs5eSj!-cYnnbfM3fAsQ&I37!%}hOH0qArLFidS5 zLfCF@3Rdc_(#ZJVOKSsenpK??p@{Zr-jZ&v3Rd8fI8)LU<1oaiWPVp9;#|;FN!s2O ztRQXz(!J$6zpXlA@i8FOlrb(LgPlAq3tk;BbfzUkwm}CQb72gL)9`F^LXGROt_wEQ z7{Kl4lPz>TiD@3Gpt$q=R+I_rzF=*3DtL5ryp@JzJ4%#^RQzO^DeJs04AxGa7m%WQ z^wQ=q*0hHtg+L=Lifr8&tQBF4Z!KhPKxzmU)d+eq(IKxr*o~FJ3cn3Lf(}&>G?XE| znnSU)sh`B%$8~40HVDG2M5c|IbF@$Ns|x5d9_R|~30~}3$u0L81rIbZbJTgKqT^to zT24i;TZ5IGXsu&{*;aZBGcLA~M+{^ol2o;>4OW&lnN@1X@02$amR+WB!lra7$1xUj2b}az7FDZ*MK|{ z)S89#@ApMkb$3-qR%WZ+8n10ws;W#TgF!yN7tH_o;pXmt(#Ljp^S|xW-ESZM`PUnF z^TS`>q`&?AHogDw-~VWzK7II9`0Yn(^vn3R(DL`kA0MwRcb~Vff4JayPs(@cr?=_z zhktx(>HTs=`uOqFhcCCw<@Z0}(~ob{569~-zkhJz(){1k-yWX(aPhAXj>@K&vhAYW z`^d|u2m5^H;rX|Z7T3JuN3WPR-MatznqT<+Uw2HUujkj}(=}7+>zjF97lz(^{M5>af7ahV zBlmZ*^3sE|M7;cAHCLy5*V1-x*K-RWk zj>OtkKP?yHj}w-q|9tzbEu4(q-+wiY?(W*B&#m6{51)Sj*ZcG;Yg}L1qYGEo__(xZ z`2FW?#UFKZ1BSP@`0IIYz7obht1Q3nmF1IFTr113+hw`cgkHMzwdii|`qvj0;Mdg^ zziJ|1U()(Q{-k<)^~k@-&AFOazrB9L*Y$5NI>T!?{B!!$?*8@ubNcbew_6Cd7U|Vp zxi|NA9fDV5{^Q%z^=Cewa{S}n`04o}y)gL@k&kz;nvUQ70o#$iwYT~Wk-N3a|Hm!2 z?$*8g?%uzf_iFxXFMB?7`ur{Ff$Nt)mV2S!y`@{&e!xgZ@cp#r0JJ6WlVTJtv{bGS8`oS zVl`(9RNvi(RfFNeZFglk?pdpGYm0I3Zr$pW-Q@;cUx~d~iT(A>?SBo@d(*z8-#@-@ zyr%dDCO;Kb&qCjGDz$0kiUi!gXBV_KMAQ03Uss@E{e0r|?E@qGd2fB+9KzjrU0>a0 zKfB0-OB8vgiE}V{Jj6N0pEgTk)NdR{_;0|K1Yu2D`zdT^Wc9^ z(4V#WbF`mz+jU9v3JcqJ;SVsbXD{)Y@z~`BdjWa*S{{hwkr94xPu@Kv99xk`b1a`v zPW*7+HpW+v&%5IF56cI>AXzUC-e6M;S3CvwcwEpFJZr(Ew(XLm=g83sMNM$BGH z^u90Mk~O-udg{J9ff#LNpMuHL>(?es55K+No?P8u_T$^LLb^P>LS~Jd)~|Sp(bI|3 zrrqatmU+1ky+kgX$#mt#1FkrF-MuF*c|9<5D}GUkubkd*?do}iHaB4{P@6X#@kmyW z5TCP(>(wXaX%pBNscyC!}5m;T`1g!gUpS$6Up73tV?`O5Qr@igf77A=W$Nv-N zzs@QVv9o5hA27t#?xv^gYVl*^(ObJV_qJC+ZqcG8t6xL+N^pX2xDh=0@a zLy_N`xc;CkDD(Vh@8Qgf3(r6rrtb?i4{ujI3v2d#-d);x9M;!3)yXqf zF(y$g%_qSvT`jAU)S6jjxm6Er4lJt%yul+&5b5HD4Lff&ccMU=Gr4r5bTIM2cEd)? zwkgF*){rvwVp4+vvbDG1sN9G-n6P7mVul~A9S`L!p~lEvixe&)R9F6^?cIA-ZiNh8R<-HDxZQ zSHv`Wsn++Fe76!88?v*O6v$LDurdA(?Af_SIR??1OB-upw{63QRK1v*tiX%T-b7oP z=@wB6QNv@PmG#xgMd%L$a zh#_~0@Ly|arYIw6S|?Nwd1vb>&GxdS_Y!T)lBJsHwc`JxTw3a_wi?qgV|H9oRTso% zpPHcDZ1>gX)JsKt#HlP*vlErEl@^{OPrHFPk#c2^Dg-8l&d18z*`1cG<7%*-IpZ&d z73o?S?s$Z_FKdyVY$XkmlbRN4&(b`quGt=o^U|^T$1K@F0EeOhTBvJ4(*{gM-WBOw z#RH5gEjD&CUP^EYaF{E0LTtjCikK1skk0!U7aKbn{~Foad$mab&qhr!L2C0z8K*f~ zS3^msz1`aypKL`qoIzS>q>;8xEHDJ2ZQ1)%n(bvt(i9sz^|jmJ7~YT~aa{MYpm7|t z)$F*!(PUO+cLp-H5*4kB*$1s+yYgaV4_jX$vaex-t8c*|JFq*gpnOEV*eKQ&MFVxq zTK0O)E7-{347J1>OAp=$P>l>EL+>)#hSC-=GCP&08ninjTG)wF_1>F`DlUZlBkrgE zz1MzQ$u-mzeV1lhRg(>)icB#Pa3JnPCH9yAXIo3iqf1l*lR?siRKyB904=b@(ZQ~! zsOycZOSzWj2-q62&8%pCpKyyOJNeY;kA`y%Un+cXq+N~^v4Z=yP|>xxRkAyWHL!)51bDT zB>%XCty=iQ1|$a{nOMF zis6*Xo5|=<#e=j{H^8srIzf*>lZ7w}JuG^{%7y^|p@N!qGfFaWMNu08!(%_1cv%{a zH5&$+jiEzCjxt8eHCma2D_~h2-Rr0VtZo$~2SMckiNSKY+ms0Cn8ktHG(+js>aH8e zYLLu8Ac)K!DnZnEl(%is2JFr~C~d+@a$^t0gted zv3#&Z(?^K|>uk_0UR!73EQ+HZgz=|qI7r{fJvITNMmt=Hq%K|encu3ifr3-;U z8t4@_Xk6)0my-r(H+=w0f(M|V0gX8t4S_81In)Y(rhf0krV-CW3l~55Vjwg)v~6_g zVqh91cL4_HH{B?KMHS#|nn~7zUE8XjnzPQPvh+C@HhrLy62z55i;X;r94Hr&qF7C; zeSroSw=6UW01!54Rt<LH~gDCP|8K9VU}=8 zs_m>mSLA{8VN`b(;fTrz6kG(G%}3hf_mVRL=El7XW$4I{L{Sh5?${}l^i*QoHNw>@ zgFTX3l%HPpn>ilA2uwYr$DAgr~s%+ zwjzC0muVos*x6`K_^@SxQC3NVH3@Kq1k6AMP;w6*tC`v(K5Q6a^!p6{Qis~Es3{nN z4Cy^Ll~m1ASz$92PMsT>B$^ajsK7#X9xBxbpSzy$VZ#DgpMlWNoPt*`)zy%2H<$xTE1Kric+%QVxxJm77ELNw-x+0wzk?CCWa~J^Gsui`Ut-%e z;#}4aRSbwnf}4PzHI6}jX37x1j|cq0J*`iO8I*@ZQWn5InW5EdQG*U3G3(h0|8#GH z6p3BKI3F0Ys0@W}29fF70GQJe|6~F359!F&psaz8xj5{fTQU=I^s;uwKN%6Q4UlnP zz@d>3>+?r^o#BjsR>Shk_BA~)r0=Yh{yICklN-mNMSFW#DZEh7(#GET07~Vj07vWEiKrgdk?{a;_oPS z5EIbNwszD%8DY&(7eg`EZc_0L=ELkEY!8Z@*?t0f-+^J!rrls98h4W>`$#q$}tB^B&d06d?j5Jkkz$O+f^r9N~%5+S-Bt zWQ0&K9f0Y@v^`FbI13;jql(?v?JzD5OGA%Yn6Rc_N*#G!HMUc7*2{MM1ZSCy;`-JyZjI@Fd+`-fl+l)XD z13JfC`cbpL&fM4*z^F=$5iW>LFEdnN5sGnu3TIn$0LC54pC!DH{*=qda?NsZY|bAT0I z0`UVTf_xxAVYLSB4lE6{iCQ>zzKavPxm*(%Ma4f{BB!qE$d36ZBvmYQOwEf)z>H!; zF{K80uLi=d0?jK33N%2F+)JNE0rOT4LI+Obzz)Yb2e>bYBPe$&P?!1s6^IQBz&ex$ zfV8%89H9i}9C5Q)(136n2X9*F7Po~q&bw0cuC)X$ht@@i?&yrW>^Q6tNWVP^Se-pB?4tIRATC0Ac8ZY&2&8SRUP) zdvN1r1*GX|q_9~Rf7}94%@pKsKzl48JRFRzxqy7jI7KbfOkkyxC9qpmMZ{jFaj-om zUIP9jtl@b0_jD*Q7kH{R7nnlVAat{;z11+@ZShd|O{S^9N+_yl8*Cph3TYLPs1Ut@ zwl=9ltW9HqxjYH#1+_?wgaV%gQ6~*hmMqSpUZ%Og3gV-(eGcGmfY<`O%46_3Mz^_u zCQpNbxxh_tqQ2N@$LR{hC3+}SZORb^4vb!z49rI0#qx?1s0FBwCYwV=ZGx-&2tv3v z8kqYignaS=-5koJLkLyV)CV9(F($XPHXE3YK*En#E}RBPTt){I59tC~W&v0^J`4xu zI|psFt)${0lSX^8ts+rlVQ&W|zdZe$^BN(boD&d!ycCh0f#Y~E1f>EqbRG}P$}M=w zrsY!bP$YPzqGS_t0evhdndbv@LYQ$>DjnTQWE|0tiF=Z272v7G%maeiL<5sy4^jmd zZ5<>%%ECtzM?(wQ%@cw-76~;`(S0Cd$F#|_fqX?wLcsdO&m)4_3rG-PT&Yr^H%nHe zH=0h1WRa{K<{81hC}JSCXJSLcrk3f8^Nnm2uv0_;a=(H>&&1!S^ z=YX3gY=8o39{VxE0U<)b(Qd~ZC$UqV2L&@|7FVFpLW20ntwp0HjbbA-Sl5DIofOPz z4*AWs8W1aXDbx z1!+d(3n3fkiNRd#4vm-8Ah}}%TBu2a;zwo&u_fH&#bzuFZir5MOlZmlg$7>H+IT0b z1HojT8O%EZyc+s38tfwaI5;C5Q*z=;RYR*ogOy6H5DeTD>IHuV?w~j<3SA5G^LU_g zIW?HcX3o&mj2`ZRmeyk#Ty<0{d6Q3r$!!w~june1$r8{x%JLR8@V~IrXj+-)26LH$ z8f7%HaSjuzN#GTb*de3WLj 0 then sum_of_fun_le_sum_of_abs_fun f a (b-1) - let rec ghost function usum_rec (f : int -> usingle) (a b:int) : usingle + let rec function usum_rec (f : int -> usingle) (a b:int) : usingle requires { 0 <= b - a } variant { b - a } ensures { abs (to_real result -. sum (real_fun f) a b) <=. sum (abs_real_fun f) a b *. (eps *. from_int (b-a)) } - = if b - a <= 0 then u0 else if b - a = 1 then f (b-1) else usum_rec f a (b-1) ++. f (b-1) + = if b - a <= 0 then uzero else if b - a = 1 then f (b-1) else usum_rec f a (b-1) ++. f (b-1) constant log_error:real axiom log_error_bounds : 0. <=. log_error <=. 1. @@ -92,7 +92,7 @@ module LSE let ghost function exp_of_f (f: int -> usingle) = (fun i -> exp ((real_fun f) i)) - let ghost lse (f : int -> usingle) (n:int) : usingle + let lse (f : int -> usingle) (n:int) : usingle requires { 0 < n < 8388608 } ensures { let exact = log(sum (exp_of_f f) 0 n) in @@ -110,7 +110,7 @@ module LSE sum_single_error_propagation s f' exact_f' exact_f' (abs_real_fun f') n (eps *. from_int n) 0. exp_error 0.; assert { abs (to_real s -. sum (exact_f') 0 n) - <=. (exp_error +. (from_int n *. eps) *. (1.0 +. exp_error)) *. + <=. (exp_error +. (from_int n *. eps) *. (1.0 +. exp_error)) *. (sum (exact_f') 0 n) }; usum_strictly_pos f' 0 n; @@ -139,7 +139,7 @@ module SLSE constant g_error:real = exp_error +. (exp (a_eps *. ((2. *. a_max +. 1.) *. (2. *. a_max +. 1.)) +. 1.5 *. eta) -. 1.) *. (1. +. exp_error) (* TODO: Instead bound a_max and prove a lemma on g_error_bound *) - axiom g_error_bound : g_error <=. 0x1p-2 + lemma g_error_bound : g_error <=. 0x1p-2 let ghost function exact_g (x y mu:usingle) : real = @@ -148,10 +148,10 @@ module SLSE lemma compat_order_mult1 : forall x y z. 0. <=. z -> x <=. y -> x *. z <=. y *. z lemma compat_order_mult2 : forall x y z. 0. <=. z -> x <=. y -> z *. x <=. z *. y - let ghost function g (x y mu : usingle) = - exp_approx ((--.((x ++. mu --. y) **. (x ++. mu --. y))) ///. u2) + let function g (x y mu : usingle) = + exp_approx ((--.((x ++. mu --. y) **. (x ++. mu --. y))) ///. utwo) - lemma g_pos : + lemma g_pos : forall x y mu. 0. <. to_real (g x y mu) let lemma error_of_g (x y mu : usingle) @@ -167,7 +167,7 @@ module SLSE let t' = 2. *. a_max +. 1. in let lemma err () ensures { - exact_g x y mu *. (exp_error +. (exp((eps +. (4. *. (eps +. eps *. eps)) *. (1. +. eps)) + exact_g x y mu *. (exp_error +. (exp((eps +. (4. *. (eps +. eps *. eps)) *. (1. +. eps)) *. ((t *. t) /. (to_real u2)) +. (eta /. to_real u2 +. eta)) -. 1.) *. (1. +. exp_error)) <=. exact_g x y mu *. (exp_error +. (exp(a_eps *. (t' *. t') +. 1.5 *. eta) -. 1.) *. (1. +. exp_error)) } @@ -175,12 +175,12 @@ module SLSE compat_order_mult1 t t' t; compat_order_mult2 t t' t'; assert { - exp((eps +. (4. *. (eps +. eps *. eps)) *. (1. +. eps)) + exp((eps +. (4. *. (eps +. eps *. eps)) *. (1. +. eps)) *. ((t *. t) /. (to_real u2)) +. (eta /. to_real u2 +. eta)) <=. exp(a_eps *. (t' *. t') +. 1.5 *. eta) }; - compat_order_mult2 - (exp_error +. (exp((eps +. (4. *. (eps +. eps *. eps)) *. (1. +. eps)) + compat_order_mult2 + (exp_error +. (exp((eps +. (4. *. (eps +. eps *. eps)) *. (1. +. eps)) *. ((t *. t) /. (to_real u2)) +. (eta /. to_real u2 +. eta)) -. 1.) *. (1. +. exp_error)) (exp_error +. (exp(a_eps *. (t' *. t') +. 1.5 *. eta) -. 1.) *. (1. +. exp_error)) (exact_g x y mu); @@ -195,12 +195,12 @@ module SLSE }; (* We call the strategy on the following assertion *) assert { abs (to_real ret -. exact_g x y mu) <=. (exact_g x y mu) *. g_error } - + let ghost function exact_f (a:int -> usingle) (mu : usingle) (n i : int) : real = log2(sum (fun j -> exact_g (a i) (a j) mu) 0 n) - let ghost function f (a:int -> usingle) (mu : usingle) (n i : int) : usingle + let function f (a:int -> usingle) (mu : usingle) (n i : int) : usingle requires { 0 <= i < n <= max_size } requires { forall k. 0 <= k < n -> abs (to_real (a k)) <=. a_max } requires { 0. <=. to_real mu <=. 1. } @@ -210,7 +210,7 @@ module SLSE -. log2 (1. -. (g_error +. from_int n *. eps *. (1. +. g_error))) *. (1. +. log2_error) } = - let ghost function g' = (fun j -> if 0 <= j < n then g (a i) (a j) mu else u1) in + let function g' = (fun j -> if 0 <= j < n then g (a i) (a j) mu else uone) in let ghost function exact_g' = (fun j -> exact_g (a i) (a j) mu) in let s = usum_rec g' 0 n in sum_single_error_propagation s g' exact_g' exact_g' (abs_real_fun g') n (eps *. from_int n) 0. g_error 0.; @@ -224,7 +224,7 @@ module SLSE lt_compat_order_mult_l (g_error +. (eps *. from_int n) *. (1.0 +. g_error)) 1. (sum exact_g' 0 n); log2_approx (s) - let ghost function slse (a:int -> usingle) (mu : usingle) (n : int) : usingle + let function slse (a:int -> usingle) (mu : usingle) (n : int) : usingle requires { 0 < n <= max_size } requires { forall i. 0 <= i < n -> abs (to_real (a i)) <=. a_max } requires { 0. <=. to_real mu <=. 1. } @@ -237,7 +237,7 @@ module SLSE *. from_int n *. (1. +. eps *. from_int n) } = - let function f' = (fun i -> if 0 <= i < n then f a mu n i else u0) in + let function f' = (fun i -> if 0 <= i < n then f a mu n i else uzero) in let function exact_f' = (fun i -> exact_f a mu n i) in let function exact_f'' = (fun i -> abs (exact_f a mu n i)) in assert { diff --git a/examples/numeric/lse/why3session.xml b/examples/numeric/lse/why3session.xml index 7662670a2..86cddad29 100644 --- a/examples/numeric/lse/why3session.xml +++ b/examples/numeric/lse/why3session.xml @@ -4,38 +4,38 @@ - - + - + + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + @@ -103,81 +103,81 @@ abs (to_real result -. (sum (real_fun f) a t1 +. t2)) - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + + + - + - + - + - - + + - + - - + - + - - + + - + - + - + - + - + - + - + - + - + - + - + - + - + + + + - + - + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - - - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - - - + - + - + @@ -596,10 +595,10 @@ abs (to_real ret -. t8) - + - + @@ -608,41 +607,41 @@ abs (to_real ret -. t8) - + - + - + - + - + - + - + - + - + @@ -651,16 +650,16 @@ abs (to_real ret -. t8) - + - + - + - + - + - + - + - + - + - + - + - + @@ -735,13 +734,13 @@ abs (to_real result -. t3) - + - + - + @@ -752,36 +751,36 @@ abs (to_real result -. t3) - + - + - + - + - + - + - + - + @@ -790,36 +789,36 @@ abs (to_real result -. t3) - + - + - + - + - + - + - + - + @@ -830,12 +829,12 @@ abs (to_real result -. t3) - + - + diff --git a/examples/numeric/lse/why3shapes.gz b/examples/numeric/lse/why3shapes.gz dissimilarity index 100% index 584b3b78b118f78029234db1f3cfb2e40ce4e1ba..f1695ad58dea60f23f2acf274af4e1b846a0e1dc 100644 GIT binary patch literal 9742 zcwPYxCh^%HiwFP!00000|LuKSj~h9b=DUAIzInF{yLi7W+5;PlO~^o^_hq41gI9NA zTu!eu-CH%ke!oLTghEnCDP_v#>cOB(&WIp+Zah3UGNS+6FIV^f2w%(n)j!L(``f!O z|KrMB{qo;mgulIg6GFTX_uqdD-%9xWv3~!uW^29{?Gc(jZa@BT`*3)WSsr9=@Lzbn z7Kw*{Tg$}W14LqY;?^A3{en8Q+unrho3$H;edyzEZo_r>d|$%<`S!gGkJj?0_x>;& zdHrJjKd-mkH=FDl`3n_v#PG|TJr*}DCpHp!4h9{lkoox8e3nz5V^_^~;Xp z<@Yb&?@Jy!Pt9+)o42NKCZes&MZmnvW5)D5kUKr=W8Uo$)9((qFM!xVE5`N(+1~Ao zwa?ih(N3*9;vHuiM0_U=#f0w=dNu@o5_{5_Mz-H@)_V z++UTi-W;O*fK=$;S4SpiB#>HP9aX|*)@Mi(pFnLhwAABKie7~K`||CfWU|S>eg7QJ z6w6wz^_;r3If2!+qDQlV1zT@wY ztoipRuG>3t(Bkx_ovFdY@cyu!y%W@UH(0*+2aRVZ{*E{OxswMWilOmN4oYzVAm5i# zgRBlhmP6y6njnvE1(8=%+f!|mrHsd83u04x~9xQt`a)+|1b&)V?9qHn9w*lW1jB)f%8&Ln-G88c&zJ5`D`}*+5$5t(% z+!d%_%-Em^h)Xbre?uga5omFF-Mdb)GOlmw(e3nT4gqbq5721RwdNQnt(#os``L)8 z+Yvw6+{55`W|VAj#628w2}c~pfTuNwVb=3u)5D#S)AJ7_TjLYIG~6E;?#Z2ync=kb z|JI(FdEa-`Q#9!dT(nvV^%9ayXuBH9DT3p!LBik3g0?%DJU$}%Fk;!UdBa2cZF=sI zp&A*3G&&h-B!la%0?hrxx7+ma`HzoZ@9tmhuZfLen#=L=ZjZ`q3fuo0a@!{7MEQMR z5+K%iBT9}J1nfZ+x0s# z`K>&+>3%)YOooMuZXgx%qpDT-lALtTFh}bPCgA0o&FoJzD`Xho;$cV+AM4970ts~} zi46wj%b|+GOEkXQjKAGBg!7gm9UTg4i?G&wHe$^W!CH4!2w%Fc%!`6wmZQ~7_L+#*^s zO2;Q=CY=K_v@fIs9bdP;_%qV^>zf}j$xG2Y~e}wEQ zl%NW|__GMQSro@<(%rJGuNUOI)nSXFKT*6?liMX}%_uNELi5n!X*6Tt6K7zK{8)`~ zUiHySr69cne=KU~gs78`U#O|Jmav#nI3RSBdYbCGqs`GuJ1 z*Q0M3a_-Ol=*XKetG~V$Xdg0oVW+?C`qwwD0RHAH2g1LHx5MSQ6WZ(I=p%3F*VLM? zIUlMZeg8vtEu!5J+jm3kv{$-jeZOM76@ANMszu%qFaiWMy;*lCb`2QYAhsdQ0nDlm zWXnHw?m;J(Ym;n0twZ-+MW)4kJ$2PBKO4*Xv=ywjy6Wq8lxJEH5C89Oa>=*%9~zI{Ei}`%k*K4zJ1Jk~_m++5-4J{PsQkv3pA(F-5%`w68frZB=lEI9%N&BQmS# zjvGP0{z@~=Xpd-@Vqu^OFj}4Hc6r^q&X`{NjY`mt5ly|jp&xO#=4Q>sQ1GHAMP(tb z`u34oQ%^B8vDU;kO^x|!8b2+C^Pjp{X9@7w@_Ps$e+$3wH~cYc*ai37_uhYVKc*5} z(<}~7vL`k;?-Fa5Cr`9E5NABhXR%G!$q)}J!+Bt~MKwq$JiHv23Ei|mFNfBt@2tzq zO`n(32FEOL?x#e4X@*n`A;sq8$c~Z6-LDho&9u-UJcr2U59xM;D|{TlHcAMggdyYv z^NI`ZviJ*&;Y?beCzxN~3{msz z#`VVZZ0yI(?3~hR@UnwEUUhSDXwbWtdeK#5=TP2R zy8X0+hnrqoJe@@O$>eRxce4mc%#XX*M|&(z#tCpQXqEO1`>WZcjhXRR#I$l=PgBhs{mB**JUw8i zww>M%Ujm5zcz^pJW$D%HK;CR*l&+`a)Z)6I7ytAUNN>aUyDtSc{vEwu(#J`%F^2dPs=B?#{;vs?duP>eEE#gK0DNv*l9!Fk1+O$ zANtLl+HTV^??%%60brjkwS{x-U1uqvF65$Hd~((FNA|xB(#o8@Ghe5yB%N zH}6Ja3~a_1418wK4-fzQTsi!GdevY9W?@G5Y5Lm}ROa9d1serAQwJBIY>*r~1uSMO z;+OsRe*2pP$KEAg2K8z@n=ZBwr_cHvIKuyF_Xz)|BS-i@J$i)y)BFhk&tBLkzo0!A z>H#X2WP70N>)!jo(f^++lqGPp!`0&}?kBx2aFGAQ@|g*7QBJR(BB4pRKU5~iUP6G) zoj9kPbJ?WtcAUaj51ytY#CCdY7D*lxIWvBbs2!x;<@RPL-#9emd#>R1(z@8|^~)0X z+cSLdwS}?Usq?W`qwA?Hqa0toKSt?R$1{j++2G04-hi~lgSnu1`@0W5EVu=FygRSc zCl~zE>j~VC?l;>ymy>L6%itKrlh}0AnaOC85hN%x^u$EyQL)NNWT$e6E2?#mtVhM&M4bt z2#i~_Roe>l*R%yY#XNbmm?!s2c7t}CS)t2p1cwBVMzpfjP$_HQg3z-rdf^y+i_z^2 zrrqR>_PTwPu6>%Kf2Csle9GT;KA%Ee-Va^3zi2@pTnN+W7v_b$_r3A`tQCL%ohn}c zKKDp7O3`rO(EgACZP;)dHpbKcn{B2el5giFhc8TUcRPF~Y4mFZcOUrdqZ9Awf5Tz_ zcHp0TdLu&ct-@)YKf4}a&x?-rdTa6W1^8bpMR+z#N;h#f0b5v$pej8M8HQ<|via{sYNu zGq)+Z3UkO(&)lupxLaW#{nX7dJN$^L{!vWN1HQi?d1rjKXW@fFFZbyG({z6Mb3i|l zpmRQeB<#K@>EV%;X@7z+edVK~ zVR1j9*FuLcoBFjGU-qwk`<<#fhFw$r$Db%%>UmtchOdp-u1Ze0#DME;0n?x-NO+st zeO7K}WXrWt3nZ&f^06ZFzl#^{~$xZghWx%|z2 zvGX~4!Dje~A|gU}B6iB-TC9zp%HyKl{nB_D?m+8yX?(fQ2#NwhJm_=-q0tA+;sUJ= z1gF0Pts_hWm<^Vh!7|tFQ!Ml$p7xa&EpE2L!`_IW^3#S79h1dxTL-qbxm4dO67doAVWCPaB{)_dXczb@0WJ8HNkJ5^5zd z0@r*c7=hATkfMx9S_6_Tx4c%)F~7+%r%Ws|>MMzU`V>fB2F! zIY4qJ(UhcO8TK(1#sLP3td*!1u#9w2XoBQVfs~??)?1otEm;aFSrs)@1(U$55d=xH zQy{5qL-J9ESaMWF7{@V>J_oG3#6#mw@{{D0A!F#2XOX!A0YzgoH%ZvYwGggBI!T}Y zijZQ_wwO?L!UFLyR6d3nb=5_C3w3C7r%r*yOJFR)IE7@hiaCHtOrzBdEh&wws;ML2?lAW~rtck%J2_26x1ljTwZ1CBGILM1nz)qq}R%4BD zws>ERs7^vzS+F&yly!3AO8J#?D`i*8tQ0IW2FjHZE5%oek@@GYVyQ696g)uWiJNR8 zajUH>2t}{7Uukz7MlKc<6wlyYf>5kfnTxKT=@3;izPk{y(tM@aaZuKB;h8F&9Fa62 z$aCpckOF>5qyPs)fKGxXl|W#fj8sWwEqpaer%&RO9YkMzA`LL&5hWhf1WFwD1(y26U*EkuSiZ)B!O>WhK-q zGw;1;VpUvm2GwNhh4mo7BZe>~S_c?bF)f9Zg%yLC`pSxx>!jjHd zGa$2icXY~#ix5Xx?Lw9%^BiK(0k#WzS6oBs#?f{GfT_+|AGAjJ5i+6$88C|or8o~( z*+MZ9TiFAnvqa=kwSWK_b8W0MvLxjJ&WJXe9|I6`c8)t>bU8@wC7d|Y0G3_EVsga2 z6OX{qpdSnfC~;Ofn}8`Zu({4KD7VNoUrw!@To?;y&t$d;8(`H8;vN4#K1W+W3uE( z$S|uqw#d|*Q=wIFu+&4+?VQXS21sSJP8W~^YEt>cKRA|Tn0z(=AyxhR#o{usn27L&K`d8mhTLFxkcLwHYDX+FohQMHFr*6@zV!4v3YIwsiq1Y7A+wiG3BW?pFIBhq+Yp_m?v8_oy{kch_& z--;#9kmWMlI%6%sx=I&)j1{IX2Dpucby6#=md_n%2aJ3Wd9R0uhNE?fdG9%bgXH1$ z0?RE-fkBx1ONuGLILtEau_#PZQ9@ zAf)<2`PkXfTVoJWXG|N!3ZC%*v|ugHeSv~4E-)UJ?Npe#7Rqvv-^e5_k{gcMfvYLLBA)hQ)Q~g5 z%0j_ZLRx{)-Nd93X?p=DAt>P~>4{*W#X3j$*Nhkm$!{tuh3Eymzp=uV2G*YqmMO-( zlt>nB#yX)26zphFlI2L%Ndha`lRzhq0EOpDl|Tmb869FF*(LA4GhxHp zrXmbNM5uv7+NM)M0#zt=)>!vVAEX#ypCVo8frg@%g2W;g1oT$H`8t)O2*^+gp7v+K zq$*s{2r`s{q9(_JMy9|WPtg?_RC99LoduJa=J1md>84J?OKuSAreF(7jDb6~<;CRO0`SQdzgtaHrx;1EkQIMiS%0^$0+ zIeHXkqw_BS6E=x#K-2}zMgDF&(?QbryDr|Ggm z#wU2MOIgu*=V#6la=c=)PbP=N3?>TkB1@PT{DV-X(RrRc;d~v|V`f1j)7K)yCPn3{ zfE(~e%0_4VoemSs7E=Od*)r{XVN5U>PU8`3N}2tJ&hy|_WC__J@IxG!3KX=!s(X*% zhC`^ybhzi~s0R1&{R~d7koJen5lT={Y?<(-c9`ecyNXDH62FvqMC@ryshF}P;h!{O zGS*?9XO}^e(}`S&qg_Fd_|PNP71<%2M#wl+^M5kPC}Kz=mf!>;SqgIml?t6f+Qdaw zo%8d&+>aoW${EQBfQ%XngqYDJ69bb-0$`TA0cGbol%PgQvWR5WQOUA%exCV6E~kwwlADNBKSrZ7 z@^D1`h(>J?d~)$;x?~@rIKrxAEzhzbo0Wzu&$adz_CQSG$eG~-s{%wKTt-S8cy$74 ztn>^k)x%54ZkpA3rkR<_U2sek4CxyZ8VJRVp zj6uPfCIKco%=3&M9VStt((VKDgD7eyX(E&W&2WRdhqvchs9=yFE9)~$0*L}unxYai zWl<#zc3(~6JnLjivOywA0>27EK&FVy!Lx!`MXA!Qo<0wzhc+o@bm3MA6TNp;Cai;k z{IvSG37O9fn;(TcrVMAoMaT%Q4GX3~wF(k(o0!vN6nL=xXam>hS*Zdm>@m?fR+F`b zy1EpUPzCCrnH=W-y!9Wcuwip4x>$~N5UJ2arKd)443Hm_MAs2Ts zNCeV?(dH)OSKMHLfiR5R8?2Rg@bXav1kOz8;DXF#OPwV3@>ksXm0)IZut0VJtEj9D zbetik!h;A1yQM4~xcjCrH|TBLh7Ut$t;T)bCAd!8kW>&1uHAB24a+37D42{jDSJK0 z(htJ15R%nTKoS7Fc=%9EhO((BV=Lrl;qC;Bsg<0qdnOXbv*N`er#JBZ+#sZ=<5dttcFv(djNPCi&c?OoEu;znC zEXS)#a4a<%&T3*xSTCGvSe$(>79HRN5@W1bh)im2aUn~t6hwI29258a0;nSVSkX07 zyc_9|6xo?rvrSn#I*Qj(u?wJrqb*1)crH5YwhdRb&I!?afU!=jqjK&NTt&@{)Cp=< zs<+Y^*n$98Q7shR*sct6kl}MMQQ5!n7z@0#&xy)y)+JnJVc!=hdvhs#Ng=Z{ zoEJj|9hr8CSxP#8E+P_03KIn#*Yoy*SRJR+84S4yP?C+McngtNh*2g4?&NlnTwfS# zr9&Z9{FYdJ+9B^m9ERXqYUG73%Z^oE7;DVPI;vzMQ}#>&S&=?fVPI}Fa|5s9!dQ_5 zVKR-?+67!{VFcpq0J(`kERWPQR)wfe_Tr)U7seXsZGqxN%#6<972(JpF{Tg(G24?@!Puo& zjtCyX9ejGl-<(ZVNa-T%ZDKXp(y{VOOPJ2SI*3&n?vU7@+=+v_Fqoug~x^+NlrDocCo-@nA!&d`u$tvh#!e|*UZ>Qjm zF_lzgtulCIra4NiDCZHySxdWW%B+MU)b>C?>kzsKhzlu{$=+ws3~nM~vl`o3UxDs| zx(`$dI>>HB%671sN?8F{j#Tb0NmlyMlmnET&ci zIbBFp#zDR+ZPY3kOOIgmO6>8;VKs6w3KlHO&@cqSh-o6Pbl}k<4E7qaYVJs$JMr8~ z#PP+z_&b;)X9V(m=@`POATyBAD?oxj4+|0#2XPq%XKt&+lqlv)$UGrC^3e=f)HC(V zI_R#|)iRmrXb(ImymW%y%&_@oz+#?A0i@8uk`JGQIMo zJhw@gL1!*HjYf+Fvz#<%fy5g(r_YVq8BfpkIm~uUY#Wd8yr0HD;QrB zv_>=>GPAubc|nAjJqK%oa79ILd{UTDcufSr!o%q3sXlo@oJ{5zLWD(=j8l%D4Z4+J z8A~<$c9K;{lB<38s+W}hBVy%&E8;F?;XPF=ZL(Ih8oZ!y5Ii51&ql+C(z{WRkr5uN z0Qp+1HJVEA4NqKM1RcvtqyS!Eq>-pG*q4G(nS%&KZLAAX(T`t*yGn|r)i->Ro zhk}^s5%$2I`HqfVYTis#8QBEvGri9N4GA1MaYjl&**9n1fh%z-_5xy1W*xG81&Kxl cZA4ZRwTQ(S7u}p%+)Xd_9Fc4?VAwdeYpSrTliMO=a2RKmo;1SwP=@c>*Mz254R788=2)s<_7^(>%hAVE(aoi8+fp*$&;rM3lhGrjnyPMl^9X{We@PEI3FT!|j)P`}@`Fmz~AS z?_a*(mpnW?-F~}$du!}w`q?^MB+R=qW<7ofai?p&&AT08`q|<83nX^fit+w}ZtwQh z+6U~AYNxw9>K%s}LVPFl#AxpbdN=F$t5vDIMDxdga`Fs-W(S4NY4^`^OY6Y z;n%O9|G0w9{&ss`?iaaF(l1j~=9Sx*D#sLM9p#4$t>lPVxt@2|U|->8aq zP1+m!O*#;IUkB|P{vCAi;qOEDx1SrX^}K~1n~5_e7o)rA9%noojEVfp{L&y4#2m%j zZ85*q7%e?C7=63VwxwEfQd4WQwrjUNaQ)KKxJ`FqfBGa!0c1?xJ9Hca)3M*@k@2E5_D4_rUt!m#K(>@%4-H+t-Ib zKDG)0<*Q)*V%7};K3t+>_%}on8Tg9J>;C8jk#T%Wmu{y^a|*b3`v7w$TWj%fvbrfk zzMr+29y<~qTT~bV&Pd*>rKI<#heS*sbx3Uuy0TH1`xp z$j5M+_kU~G%>3DR^rUFo7dUA35qe5U@}KQ!D4__BvqlMjC->RT;P3dz9=`uM-0`(7_`yFP@@=JZxvncAHLnDhtGd}{Cao)Vt-C-9MfEnk3aUPz9zK(*U;Ox zI4A1w`;r1N$D2@cJRo9kx?W}+8=Z$6f>rNY*dcH5ZeHC|*TY@CHv4zY^?L+UTy8L7 z_}h-(k;`u-xy|F(lg#8;sL%#cp+Blrg)hlT=L~Z+zu*F1uG!50G`B*I@hvWf^zgC1 z3?q?HhcejUP`(^0B)r7UcboRN+m3L4XUIZ_BHALYHJ`Ou^Fy@O-4w!?ZY%Rb;Fo0_ z8g{D`FG)qqsls$?Cso)b{ccWfR|`X(U{MiEwTUfaYccPvI6`baMv!LKlS0H0?cVKn ztxNXm&51)c5brSi^_wo}84Z^NI3O92*REu1d9d5^sAMNJToQnEC?_4tWjMENNXuor zFNdsaZUKkNT3-g6UY;#ojImoY8D7mhz9`eIZZbW1fY_!IxY&M=_OYtlg2c<>&RF&G z(&OSTg|~O3wH=ITVZZUanFHKz+*ywIdb_s^SGNGqZi8KN+dX)iGKLF7fLa{MCun$q z(u~orMwiRXLy=&XKZN^*q$1oulA@er>rXJA6H3L~(st&P%=`V>qPQpf?uA`Ie8{l7 zm-}&(XvrxZADEeT4vf&gk`6rhx;=|Oqny9K`4NM>#C~kNNup0Phyy)2*wKwHmiqg& zZZ1fFMC=JlP+?yDSpwZGs^c{6Zh6+%3;Nx9V5>uaqI#(yw=2?`5imU>^YFmaWJbd$ zj=-Gxu>#|~>Z6xRL3)S&Sk%x9x!_uV81g3}dN~pYo6^u5T$`PZc@))Csq8q{LobWA zrJ}WPNZxu0lFkgN1gFRXH)^_}N0#)|OSM!7kb^2dj70?B24<^-&@Sy25caOVqtdjr z4M^H?Cj|~E!|Yrrb>0lZQl2{H+hUjcCXZCZt4FMBBC%*U za~9LGpKa+f+mOSR-N*KUX1g^u;B1EX2erK2a)3*svpMdIgBCZKV>eN+A81 zi>%wpFVu;CJjRA0=lUU-^*TifA3g_H__DEs?HSU#S>RMPIC#YLPcYj0nL@Z`PfPU4zCp ziERpV0<&rZ`SMS__mC6QwQ08R(4q5gBGY8Po*vaLKO1ZMv;wTQ9@W=v`_42W#1xQk z?>{!at$KnH=~eRY`Szc5a2;NgyQN@;zf}GIJ^c1P{IPrbU0`^6DQMqngxad!3URoy zOAcgK%^jD2e*Kk3nbFG7uDrs)3gEE1$nEgDKRWC1+HcH()`@7?-3|SyZ)Z7gp9{9}*8F^xUi!CCy6pKUvmulH?t>M=LF*rDAPr&!s1kKbnB-MGc=EOUC= zHonbMm+#ZYd7NSE3&Nbl@?;KMgT0ZG#{BW{`sfpjT0DX71-;UqV}CWXuyH`f!@ZGO z_V_>2y=_f`cCazn{c$>v^u@{TOsSp8^sv0k^)%>q;o$TyX9m04yQngLq~uE;NRVhp4W}BzSSJ+Q_9pGU959?>9#6>;5dWwc7<^E8e z9DB(CK6mOlot)cE`Xa|E{p#Rp+9GVH%VtsJF^MzdXNKBF+1=jW>|`5DGg12-|YOlcl|ZXp5U~A@TNi9eh{_ z3v_vRT&GVe_@&nmxF6p?kZP?|KbXINpyp?zAxWh7s=Ylh_GYcb4gFg61P>UTO`ok= zOLs%Rxl(TEnSHI$ix)#3!H#tV`~L6a3kdz%gn-{Jj?U;)#>Z!{L%Fr`%cTfK8_2KG z=IE;jLv`c8Tm5FOTTY_c^twKd$JY;9O=NL&`*#^ed8Zh#7L;hv#_P>&7JT8+rI!S@ z8mU>*Fm_8}b1yVg_2MHp1~p78N(DTz7q+(@!1m(P^T zuir0clx;8s+AaF3ZG-u1`huN8o;+H}lY8a5!Me??$YnN)LxM*wT2X4KlC^I==-DHB zVY7R~=ypcaZgNI@-M%%~K0VRDLNR_GW zyZHMbRPXwac|@8?iW>*E<_{UrrWz*R~`i4s+iXKwd;ZQyxv$}zNE>xA62O`y4-c4H(eK-`iaoXS^q3d z|K+0lmL9-qiT#W6pWnmh+lN1{{_)4xyN7?2``hLBvd`-1Hs3#|hYNx|){(8oKeZE0 zf=2{j`fkck6Z(LBG-c)=8d(SyTXXZQ7;%<}C(d75;{F*Qc{w&@i`mYlM{VcZF=lJn z%uy-n{tpzhjohZ*D$F5IJ&Uzs6KjQi^gA}k{O}{L`bTwoj`se7;+^qLo`tUkz1)-k zPqX>uZ~gp4fzJ85k+A!!q>D#pru_-Z{Fx#xYVD9mIMMf?yk>LCr(hnAe1~Sc$aSnx zH+ynUZb#l9spsc^%V|*;uP>~NNfAF&3&*-Y?E5gA&1jpP#9m)UCj$?+7Jf1J@z?)K zx{_=y`EDO1zo@RHSWCI2D=Gg)bamlrH8;~G6S99PwQMQ}bJO29`x7SSftD9Fwr0>v z#>W4mT7CJrIV>(F^g`(H*;2nY<6Hi5H8Y%?mc;M-q_`x(l&W8`olO^i&%c?d+GqLS+N!3=3Uel^kUovWIk>i5VWVLNYsjnDKOHQ;3B|9mEHu~ni>_aE zr$eeTG8R=Xj2Eq~O^};0gR^Lb8lL8S#o5yu)S9@A$yr-+^-&0;nH0rI3k4|4M|sSO z>lIf+FRCjx8kv-^UMS`>!%Q%|Vya~o!o0Jswo5V4NqRU$GSThqE(#fK(B%af!P!g3#OG0@o zLarFUEQ;kKU}RcSKY++GR066O?27Q>igcD9%x zlgq)o;yeU35Xq#_D7jN8MFc9JoX){kTXmAw8RnA+iPz$SXq5aZlyX+Qlq8ksur6Js zt~_yJa&n};rOhIUs?c0X(5skluq~!UY?SyZlvpv5!wRgEUKkj^WGQ)* zK-XBoWTSMFJ^d9a8Ln8;uENQ{Ylxzw#ayn&N4O57R2w^Wl09MCVf=~}CBP>Ht}u&v z^*r(zbri#FInB&vjNEDyQ*g?#WHom=3LR3`R&b?9&vDZ1gH;BuJuj9ST2*(?Fy8LkBTcbO}5La!;jHVTF^GNari%SIVuFT`99t@XTl^S4ylDUn!XG3(rE- zwqn3&*7#UFIt!PA4gypNd8PeIyW=z*s|EI*1VoS`V7itR3Z|Zk(OKqu2oWpISDGCs zWzojNDI@B{F0K%7|c7So!}U<0v}aMCR%!>)k@3L ziKbXXipgsO7cRIip7U%nMpH-!E2YuX7$tKGF?dP~KNXk^2_e;#DyvJ`Rxe71ProvJ zWgej+5nx@GF>}Y0k~LQ;I5WyhmpGz7S%4A8X~6Q}!~qyQSVvieGR{a%&_H`1^OaF6 zBN2gU78son!wsTO4!|A8l$0}YO$bMkpF~b~6hG#(BM|4Iqc4fuN z@|9&P1L54tz(CB(=oeWiuv1EwtV?#jYa|3G8DWTsA+u^_xt8 z2uCPt;DI~qJ%gtKCSoglpf#qc<&_~82qQ38l7;0P=L!&AA)TT%KSm%!YQ~u?K!OOq zS}Dg^LQ-f1&|4=U9-#qSb^=YU)|GGtI+KFJ;6gfun>1cdt(;uqk9lshiLw?xm4b~j%ORJ!8loguUOY|-`bp#=67n5{S1$`h)IJ&`p!3)PGy^Sl5;+rKY&pw{>B^9O zIEQ>TNrXa{fypI>XwJl`{{?PJ0U+PRPdVQ>jJdaTX8@^QDM{ ztjsjT1zm>h0hk*#b8=U!Dja?nZY!f}+M56`FT6y4gK=mm-rG~D0pBD6Kdb~&Ee+R% z6gL>;l?c7T`_!nplY3emf&gMn0nqYJU@(F=a1q&-WJ_t({HfHqLFOcb)G=qwg93D^ zVRcAU;ccypqm7&~uyA)sz>|}Tyba@3!Eq$aQGkI210SvU4AYC02W3^^lmZiQ=SJ(I zjFAE!+Nv_nvoj`#HHc{u$s$C}z=*&>p(T^FGdWd*(2eYsA$?`$1q0W}QjOfOXyDfk zU?E_W#Tj88f)t$j_H0h@A`ZqaG3E{cQgL_#WY-ugNG{s5NWjPES+tl3$PdY7Ad!Xn z3s(?j2v28+bQ;)}QwL{_FpbGe2*k6PjrS698YzFmz$Ik#6eT$2`LiZMW{wVkJRk@T zYJ@g5P(;R=Vy-n2d(E7N^1a3^N7@i2I9VSPCPPAe=GOP_=&d$@r^qm^EAX+j)vfN@aeUc;!8OvNx{B)MU!3Wp`&qybwr26yTf{l)N5b%DwYJ7fT@0DTfO z62M7YK)Dj4t5zZQ7$FHXampP|A(i2KmD5bvShb+S4u;3*ToiYRMvWA-CLSkc12Pi{ z;aGh#u5(R1p5Cw&0IBdXo7_46mk@M z3KC2JEeWK}YoZ(<(I5DsaLXs@PABOBeG=ti8ZJ2^+yX;JB%NMVB#c25h~n^8T$qz- z1`a<8;NYDBbanz!*GeS?l17u!?a@NcB#ZpKa+nQ|@T|oY%02+rMKL*h(=Fx+WRcAf zP+`FXPus$zb6E-a{a77yyfme{^Q8qM2qhzJcUg!Uk$L!1FfBQ9O~w0IJ&iPwUcfv} zmRuoR1R^|gnTiOJqv4@8Pb*pfok<&z3-JI5MaxLPN1XAlB9XNSkH)o{BIdlW;Uj28$ADs;Mmt|(BnTTiO??(k zs{UFa6cD14H`g^llbCHHB_6FIWWhDREX^k8&!?G+E7l^%M9vrqO6fuN|WR~o2C@T06-d6k#%GwKDAb)iP`y}1`w{)Su`CYMzkUnC6V1C%M6)S6Opx> z7E5~H*;zC-JXFX5U@BRvzyRHZ8cI;nY6Z{LJWfl>h=HDlPVHihvD z0UJQ4WY{Eg(ZniCvBF9#0clgMz31mej~^hWt+8k%c-b1Rr9!|^K2b!HN@pj#qnGCe zP7Jh8Mn#W)105s%gO73mYc{#;tJ^q{^CtZdaZXMkCvyeZR%RqMOaek7?TS|M%K1R^ zya4heX!2sU*Oe7`d9Ib9X^OxBjE2N0G2UsOH}*e*=D)_|v{}SdH1b)*p~5sP!W86{ zvC;e!VH6qx}pX^Hvj83hkuDCR9wfT*4Bd9E4Wgvv6=9(|4?3q&b0d#au% zZF~O7|xc!?%N^ghU%gaRVZ&H|b<0f;w*P<1Y}M=It5B98_LL-dqZ!{m`S6`5EW zJk)vK$!De&z?Us4Cd;7)g+PbE?*j0N^NprB&pXjvtjQ$7>HBDvmeJ?}3?B(y7JY{5 zGd-S^!YbBA26>lL032u+DHmRrz#4Hd@9F?G$^uT4w7?#D9E}og*3GE9leS`>q&qHxGIG9zEF$ht|l+m7_ zis}?f3W+usz&;B+H=3HLJX&(Ar!@S`v{}$*ri^T+z@uYG6hmO$ThI)A z78e_V!-AnjQiP`{Fw>EPB5^cGZj#K?;6Hb00B{t`i104arV8LRpWs{JtZ0j(YZX(+ zW=#B3N5@*)cbH4{h%3&Uj2Vb@1$IpUCNxH9=J<1%V75Dv5os{bGt4au4<`&HYHhG7 z^t}wv=VPFFtE1MKiz3v>g=WfR42&|KNj`0Pcs{GDffNHmhBs9^mfkgUr`p5d4HdR$x_dNefm= zK^S8_a(U9)v$(im8H>1NU~#end|2Q&Fi@^CWg8b~p2-EH4@)ziHalU4=-?^%@=Tk= za-m(h2u$3w3$Tg~t`nJuFU;h~Y3WG`fQlkCK%elPmGc*1RUFM68G^R9t@$9;7u;c> zWZ*9Aft9@gD`mA14nP7RE}%amXSix5V*xLx`s#!igASj=DOIE(5|Bg7is|aJ$T+no zfKfrFL?-U#g_s%I03vDa(yPR?%m_$Md0#UR$S<3p^Xh^O0nzFIirA2G^O!?rL8Vl6 zY{_;NeRmD_`a=A)35+(#)F^XJ)md6&;lQLJD`>Ut!9hj>PUeDKC6Fof=2W0f6AG}J zuuw_a3E&sg)^r5zNVq6h>RiR8`&u}FI4uyPU69gC zI5B4{QXWcmb?3@2%#|`epbo%l0gM?F&<9{sMP8|LEU_2V+@&=fK$;g76~|0r7BI(1 z@2y}#Ai?oHN%Z!@Tr)?{BC<1|;1F^GLo}wP*F>9-d&=+Kg}J)mxImKNc#Xlru%u$v z7uwJbU*v4(>MzU{b|iQe68RT7L7S!G32-GO&2{W0D8bmpZMc{y5D)344rCWlGOhC$ z+M_@(AdEBT@^66Kk^^B58AnlvyNzeo<6W z8AzHT=|}=NjZmOq^mCI`g7#`bD*ShdYE*zNwaSEm2*9c>?RG#aV>6>I-n6Gx(5pwB z-wMJg6%HD}QXT{7HeWsL*6-86qTbpR4UgDNEeg!LvS4Pe5Q2$UT= zMi51aac4IYb^Hu|`Wz-fdqC7AQ>E1`Zi~!OIizC15l)rRnW*P6@j_Sck-9ob8{v_( z8X#jvyYCFrFxi=i=P?l`N&pbR9HnbO;_INkq+^YqP_b%EK<-&gvW53DR7zBEn$^Xk zsr>JO9f9Ul?e6TEOpswE;KNAo00Go`K%$5$u`f#j-B6@6R|ScU&6) zr&7=#+9t!Q9=OP7jtb*&;xe(QijPQwayCW?0AR(u@*@}h+_9&wxvZWUdMH`$aF^GZY2GTjtXu`k|I!f^oF$-o6BL+fD228IUKAjij^@Zv!P@S$8 z`f{8$k~#(8VJj68;oU}F^eW-=_&FN|G6C)*V@SS{ry4JqPV^!Rl7HFwi3{=r^-LRP zd2%(mXp}-66yV2UfvQy&XD;XY45Oue$tii-2By4{Ra8$49e|S#VSdN`JfEQ!Fhs{- zdOpVJRfd5VFX6v4h3E#5h2$4hDKa_*@XwQR$BqX+=-YMLP=WCsD7}Siw+~b&xu?TQ!gT;EIM!*U69!_mn~AD#uLrSe4fuOY1+)0 z0e)Silrk^?3X`OwsV`jWWyuRN3=HT~L?o`oV-%6tIB(D%Xd9roztkiy%+nweOIux* zTDT}JOZ3(YA~gn;syYq*(hL96JeO689)AiO8X)nQwkc>lu z3Iu7SKsJngLP~`h?@C37H@&(DJF2Esu9z+c0TuQbS*)N5u<2CHZ9A|~m<;sRrr8frfoY8)9UM(`l-aCJ(aRWYciXm)g+C491My%CZvPzX&E`|WE_@%lB oNTM<2qDA&8E2md1>FosC7sqSR1Nc$$Qlt0(0p^Mg;n=SL0L+Zj - + - + - + - + - + - + - + - + - + - + - + - + - + @@ -189,46 +189,46 @@ abs (to_real result -. t15) - + - + - + - + - + - + - + - + - + - + - + - + @@ -253,87 +253,87 @@ abs (to_real result -. t15) - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + @@ -379,51 +379,51 @@ abs (to_real result -. t4) - + - + - + - + - + - + - + - + - + - + - + - + - + @@ -524,46 +524,46 @@ abs (to_real result -. t15) - + - + - + - + - + - + - + - + - + - + - + - + @@ -588,87 +588,87 @@ abs (to_real result -. t15) - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + diff --git a/examples/numeric/multiplication/why3shapes.gz b/examples/numeric/multiplication/why3shapes.gz dissimilarity index 100% index 12ee0dabb2c0a95d80cae58a482c0cc334766b42..e47dd67e96a2abd1eb425f03b04cea1088aa1299 100644 GIT binary patch literal 3446 zcwPZ^4To$jEmZ*2;h}3$A-BamCtD4PjicK~pVQdUEqR6VssC-1ky>X-dbbWRI&wShOum08V?mvC`>91G*>iW-1 z{@eE-axVAzFCX&5mmltW{+zF`d6Y}OetMJ-S0#V-Rr@epp@j=*IfuK_3l2oZI^|Kg{3L=iAkG^SJi)$=!D! zsvNdG$KG(z3kyA7JS}kKiPz@a@ADzAdwR$(M(^3!>3&x~{tx}NKiuVu{NMU&XW!|G zot_gNzxL+YcIN3AJ6WHooiGviHw^8}PTibwz|HAtZcdMS^9+h-@}d7b*N6Q+x2-ax zJo;xJfX!%|esB9c@sBpLzg%v=+&|PWKebN}(B(^e*tuPJV`&V|EsK+0TK48N`*!MZ zB~NeO?A*=d7u?IW*{*T?KbGC!C)-{@w-29gKYxNw+58Xv?(WOo{SPJIf2xzEPUz_Z zvU+C!2WMS|!>{bNZ-KggyUXUE-{O}8l#jOh>|p0M-;S=%ikJ2a@$&5WJ&)tP_QTaU zFTIY9PImXSp_988mDBMg=Z7Boqdjf*`0nhn+DnIPub=c85RS9+G*@5bkJGciwb0Xw zucmc-2V{=dxjt5k?*PMBblbDtzrDye>9XJImpA#Noo@aTX1dVsMO2^N?uB+IUCt|R zdT#eVDt+gR?M%OQDr#OQrIU{0%@F)*^u3x|uZ_Ktm9LMzET=9_v|m91?+M)gmCNma zkLv!eZPs^gvtGK*H$D3+)_jj2-`#3|%fNU_o!|GAe}Lj!1;sACoXb1Av)s%-`>!bJ zm+7#64A=!Mr-9!;jPqgKKXltoIQoL(XRp6bu`{cUY(vM7)T8y8i0@>bN}ciV&1sN! zdbQS%>zsU~IXL?1vR(9n=4B3eF!Sg7@#5k1d(H7{539rY{b05ry2pX_8w7*qK5Y)+fchtE;l{A z$tES4RiP?3k!BjQJohqa0ZhY@o`r`#g zf)RW7Mw{YGFU?jPLbP2>9i}x=cAW{cs+4Fjnj7 zD6Or}txI4cOmqynIgBhufqbe%r0W)vSFx8;lr6ypZ^ATkONxn?axjWOjoMqlS-mFw zrZhts`Nam8Q;orn5l3uw)SzADz?`8CsThSNC2frEp&8=pT5=W(;r|pu({XM*UN)1h zL8Or`buE0Eh>JzbTT?sx2zIbWHwclpj8{*dmeD$!KXIR!z*Ya%`*x zL&A1jE8f6T_e$D|ZrK4W9IVwM-nceW@Iw^_bsIfI(Z1_aT1jI%E-j%sC8jsij584c zvDQ#b7^{S+);Pq4eQ1ksof*TIVnKrCUu&^|`D9lZy=gRIq@%925&cYRd#}OCAe^d* zF14GqhtbH!`9e}Ft=kI!ti#ByNa*-uREha;tXuGguugz$ybH35%Nn z$Gw1GI*e2&H|1`Co9VFf8s!t?M;uW=16K3puTWDFa|f z8OCRFDJwk$4xWZ_DWO1;#sZ9Lk~1m$QAV$s_y(II>uSzGN*d6kWMr*e(8Cf$p4L=L zb~C%QUm#seq2Nq2qMRoin>swmY?+|W6=m^}w1Q0itQ^ijdd`(n2`SX4>bfuewv|k) z5WP%Rh??Y~kOc~WskRh>*T+hBdY!HcfG%;eVpD)As{k`Hzx7&?z|+uBC7Wh~0K+TQ zizT$&*Oe%ItgDs1Eb3o56FWSmRZ<|Z`Iro4X7oG~u?8hp&7HfY`NCOp7s$fZ5ZrJT z-+HQ!)v(zb>={Xu27vE8&c34ndNHVnSSqYJht}Mgi4p5i0~YTMexP1w>TdBpvjPjN z)njR~x%NyHbBfivSg16X6l9ZdVw5?ZQ47&6WWOKXd1$e)CuE2n#WxgzU#;XqE2FZN z2=kNk91-ReAA2T$;*9Jpx<)SpanMJJF1l1}Md8$xoE8h3jFss%V;00ua*mUh9>h9g z>JznlObr{U*3-%^95#}3oyZUa?Yxt008--I-G#OmhROPliIneV${Y*f30yz?%wQ>& zy0X@pSwvKh73X+E0UWAR>quB(U9nj?owvF*i<0yXaZsd;1DLH$onc|?378ahdQ^AT zk&(f8pLACdkvG^RI#8hmV#|AV7Z3^#jZ@|y{!;{MmN|jQds@Lx@ikK)b!1VEG>P6$ zcEfQLCtp!KW3TSuyHYb5O<@8F;;o^m7=E)m6E}4SQ-DKs5#fmy05r)1X2PQ;M>p28 z^rq1)O9ZG*ePK-)UMi%JEmhg^FgF=vUzXySL_GTZupVmjFx1es387NNVGZfxNF7Zi zQ8xo2R&iHGFOgQEDv-36r8$Rz6{&f#^1IzDBT@8j~%pHGnu$ zYNm&jhHka1&~rbiJMri+8!MvEiPc@((1Op14a%D8`AOYrN(i)V9MThMR0axlMA`_C zUPoQ;)twF%iw3AE7B-|#k)jR`$gMd$x45c1r!pFaCTPmO&X!V1T_vPT^^HQask=-c zL)S8FBu20uNGUOMTBHcBkWJk=ay?R44XsN`#;B;04T_ovEAOF>xVZ5)!>Nun20ZL6u5%;Y2{WeDJK!KG{>m7LZxP7*j9 zfJsF4&`BcH>XW)dS_d#0P*aqsM*r;tHNw&S%#TH5Q+I|0qvIZCNUPjHILN7c`8=h)O;j#EzP0&Hdz%wk|%W^GE)PFDwY zmknO-4KgL7OEz_fcq!!iXvUJ@ zg?^Yk!X2nQ2SK$>-QgTRBl?WPy&Qxu;X9ded!}S((`aBGUr7P}c7e)CHtP ziK7BEzo|PLplR4LT1^k%XLC(c5{1kb5-M%#4w~yU4xEpQg}yD5$WxIS4ivZE)Lle# z>qx&HDjiNz^hlhK?m>hiD*2%9WL8^)04fQ%&{I_!sYrK^234kngSx|k1>8)TLd0NY Y(gz)f*d}I9*C%!NUwzM+M{6tq02oBB$^ZZW literal 3443 zcwPZ>4UF<1iwFP!00000|LvGdZyd)Jh4=F-xJ+n7s9Wy};#Gh^3$ABt)DsaPTLei5 z$-mE6-Seb5fpY;33<-H3={V8wq<70n#>g{HH zdHC_?&-`$I|M@>R_YeKYPmlfa#l7pv)v{4lAMRCGi{0VT?#JT_7reOq==kb!zq7l= zV81zsJ-t8O{$Mf>{C$4tk3WBYT0*!FV}0?Ud&3Wxe18^)`R|PRdbQr{_r5*5`|d-P zgWL1j8v%M@qy5EkgOfo@tojn&q^GZI@p z7dn0I&9iOI@fcfKeoaW$&a7vM5!})x&o}8 z+5drA*Y)974%@c?UB5kK^S|E`mqRO`xccm1mz-}WR~N-g`-OOUcKn{lsjvNTH7-l9 zQ=>EQjt-sOy{Mc{7rFdsk00&m?CIUbW3`tK*IqyAvqm_r&huJ*5kJn){?s-{l4oYVe#hWSk)!p}MX}$LBjjDY8*~@b3+Cuvk5b&PF?OwUw{`X+_ zcez>L>1Msw%{L?aEB1U(9N#@^f6I+=ES=x?lz%kEx7rlj^l~k4?bdQL|J!{G z>-|1wA88JOK3=w~KG3|30Z(TBz1?3toqw-6eeG!p82>(*HHmKjVEM+vzxxMve~;~@ zd~StA>5G1CCGdAfVY%3fU*gOg&r+(@5-K&Vm*k}V16dx(;X&NpPg{S;t|Xq^9SinZ ziEj15_@aq9S??sl7rq>wTA0%td$@AX>p}eUG9Y~GM<>zS$erHZsrfxh)Zv5F9Zz>3 zs{9>)mutIquYai8Y~mPB={`#DRV3POoz^C5pNvmos2lMg#cd=NJ6y0WTB}AIB^70o zQ%Z~pRmP3jk771m2Vb)uBeyV;v!mJGy^6(+l2eX1@=^50IctkHxeez>8ESZiS+Xj} zWQ@zxN;VRd3RMqNlPKj(492jAC_JpA>S@Jn-=sV5*ijj!OH|hP7@{i8XVbmA(I2lc z5{yc-B3coJtd&$D1f#aV0d>fuskstns)&pblrdP?QFJNYMPsdwSy$gMGaDl=HY2`_ zs9g^^)=g~Fb+;K+S|!rD6{l6nYB-C_ zDW%av)6>XrI99Qm#AF-_PT5+;D~grfT$gDSHqla3Dy29idq0w%8(Qm{9X5w37{%*W z^4%tW??kY5XR>nL60zbE!3C5tN}H5;O|kM&HCF;*vW=w=l?vq(&64Dq!Q^W6!DI=+ zjnG|+xew2YO;lZmU20}2h-RQvr)tW|SHar%s>CW!xYND{XMuGUn~co?b3qd~rq)&@x>h>5u#V2)yseY|ltSn@ zXu^iKMrv)4M5S%7Zjhx~dMvbuk7ZiWJda-WK3Zjo*jpm)v5&kQ*0>Gm7kiAh zbo^JjI)b7pxfHAS)h7b137n5R zmDw<)zO-cA)ZuG&*|Z)M6`RRx9lG~U@>;23X`?rdW*gNMQ=+WHFr`I~MiUW+9B5kx z#Ib9m%&934KZGKpI*Kn|)fS7mMkxEzMwz1Vl+_5)0Q0sQr-7yz+h|3#v9ys8XKTBb zIJ)Vy1Qv!;BNrp^*3w4wR8B5?XPj!ydu;$aGl->`HSE_mnr=Iu2C7|1a92iavZ;tI zAhZ;JO+h+QJu6?4yb$d0O`C4LE?Dc~^wMiWUC|d> zON}mQC#2YmcLJJP{v;QcEYB3`l%1Witi-yI8M;k}lye-KPRdKsEEOR@SjdL8jLe!I zwotCANU~1RnHa`RFe$WFT`Jiqnph=rm7>qlMk%GSuLe}~3<6kWQiHJKu)dlA+_~7z z$Z1;nO$YdBLC?%JIY3Bw$l{8=obBGF#)X}=21O*+Id>(x2u*rPP+xLffbgureTIs3b0#o&~`PnX@M7q_lj~1Wg41I3!o$wWP#_V zoF<|HGSL-k02u7Fve#w(D_7#g-D+wFbLiUzJ(9E-G&tc&$@JW9qT^(P>e29fP(f^T zk~62w&OkRyvS%iN5NI+0hf-C7{@Gc1KQn71*tXQpER4cipdj8CT!Q4YMH2{s-Asb+ zr(xQ#wiRcCkHA39+4o62Bjf^1CqL6<)TU=RgKa&(hMZby!Z~u0tSUP%SRq$hK}ccv z96*Rf3s^AQXaZT30+H2>tkFQe2W%nb4v5~CT|ou6A?1LQ+Hm> zFscR<0RUu$hi>4@p+o`THSE+~YYipTDL1+!0t;on0pb=%tC6im-FZ_Zw2)JUu!s#5 z4%~oU!pXptRoyjPpm@gtlE;^>QcDQLKo3~uq_66Zyk+fa%E~FiJa@>A`V~W2()bH4 zy=gRQ31%ti2ec~sMscQu90c@yLqIf?=}Jqe9@h|Gy;v%D=7Tc>&KjS)D;-TRwGpiq8p$evRuI6s+AD# zsBoWjLa}-(O^|QV(4g8k7yY8{qDPeyKu5+<<=&tss4ZaLk)ESf-ucvB!} zhXRc78Nvxgn-A&^X^Y%Rsz%fFr~|K2=>u?y(V-8I>W*NtT1R@J7L82oPG+V;G^g=p zr|$aDHfuLK(;BouZvax6+Jy6rolU~gv#edW$qXYMYKsx1 zqIi6OQ!UE97VxskPTk=~fn5;mSs)eVYD)|V-nEGiX;pVP1`8UPqcQn6=u2l0IVxrV z;MJ_^&H~8}wcle>CX5(t06}C#K}#_u?bIFO6`f7KIFnJ4u5LgNNWh5B%(SXI*N1J; z2r3i7EKGZasw8#MI^z! z2?}rSpzbKU1Z z4%IMXFtfXqR&_T}gf@Y_#W8_G$yMm02KWO+MXOcay=k?mJEqov`Wk7@B9I>%H3Y_k zf#3~Ob?()j6C_&69XZmG=hJ{7N7)g6ZkJ5&o zs%6Sgi6MJccf`C>)KO(Oa;>Er<&n53h~A+dS#{fWR@OzLgig)|nhmK%NrSM{J?L4l zS9RBOuFwm01z(~-+ngtiHLfr$$ikJVJCk%3nt@RsSwx#oVZ%_KnXTBotm=-Dnuco~ z;)%2mb5Ny*Ksf~$f!POjmnbHN*jBU3umqHukwBGEjJl1X9@HH*lbB{p;S`o3C+jJ( V6&^FA3>}W@?!V!&4=!sg004C(r#=7x diff --git a/examples/numeric/sin_cos.mlw b/examples/numeric/sin_cos.mlw index 60dabacd7..679f794f1 100644 --- a/examples/numeric/sin_cos.mlw +++ b/examples/numeric/sin_cos.mlw @@ -33,7 +33,7 @@ module SinCosSingle } - let ghost sin_simple_example (a b :usingle) + let sin_simple_example (a b :usingle) requires { abs (to_real a) <=. 0.25 *. sin_max } requires { abs (to_real b) <=. 0.25 *. sin_max } ensures { @@ -44,7 +44,7 @@ module SinCosSingle } = sin_approx(a ++. b) - let ghost cos_simple_example (a b :usingle) + let cos_simple_example (a b :usingle) requires { abs (to_real a) <=. 0.25 *. cos_max } requires { abs (to_real b) <=. 0.25 *. cos_max } ensures { @@ -56,7 +56,7 @@ module SinCosSingle = cos_approx(a --. b) (* Example from the report *) - let ghost r_cos_theta (r theta : usingle) + let r_cos_theta (r theta : usingle) (ghost r_exact theta_exact r_err theta_err :real) requires { cos_max >=. 3.1416 } requires { 0.0 <=. to_real r <=. 1.0 } @@ -80,7 +80,7 @@ module SinCosSingle lemma cos_square_plus_sine_square : forall x. cos x *. cos x +. sin x *. sin x = 1. - let ghost cos_and_sine_example (a :usingle) + let cos_and_sine_example (a :usingle) requires { abs (to_real a) <=. sin_max } requires { abs (to_real a) <=. cos_max } ensures { @@ -109,7 +109,7 @@ val exact_cte (x:real) : usingle (* Kinematics example *) -let ghost kinematics (theta1 theta2:usingle) +let kinematics (theta1 theta2:usingle) requires { abs (to_real theta1) <=. 0.25 *. sin_max } requires { abs (to_real theta2) <=. 0.25 *. sin_max } ensures { @@ -136,7 +136,7 @@ let ghost kinematics (theta1 theta2:usingle) (* Raytracer example *) -let ghost raytracer (theta phi nx ny nz:usingle) +let raytracer (theta phi nx ny nz:usingle) requires { abs (to_real phi) <=. sin_max } requires { abs (to_real phi) <=. cos_max } requires { abs (to_real theta) <=. sin_max } @@ -218,7 +218,7 @@ module SinCosDouble } - let ghost sin_simple_example (a b :udouble) + let sin_simple_example (a b :udouble) requires { abs (to_real a) <=. 0.25 *. sin_max } requires { abs (to_real b) <=. 0.25 *. sin_max } ensures { @@ -229,7 +229,7 @@ module SinCosDouble } = sin_approx(a ++. b) - let ghost cos_simple_example (a b :udouble) + let cos_simple_example (a b :udouble) requires { abs (to_real a) <=. 0.25 *. cos_max } requires { abs (to_real b) <=. 0.25 *. cos_max } ensures { @@ -240,7 +240,7 @@ module SinCosDouble } = cos_approx(a --. b) - let ghost cos_and_sine_example (a :udouble) + let cos_and_sine_example (a :udouble) requires { abs (to_real a) <=. sin_max } requires { abs (to_real a) <=. cos_max } ensures { @@ -268,7 +268,7 @@ val exact_cte (x:real) : udouble (* Kinematics example *) -let ghost kinematics (theta1 theta2:udouble) +let kinematics (theta1 theta2:udouble) requires { abs (to_real theta1) <=. 0.25 *. sin_max } requires { abs (to_real theta2) <=. 0.25 *. sin_max } ensures { @@ -295,7 +295,7 @@ let ghost kinematics (theta1 theta2:udouble) (* Raytracer example *) -let ghost raytracer (theta phi nx ny nz:udouble) +let raytracer (theta phi nx ny nz:udouble) requires { abs (to_real phi) <=. sin_max } requires { abs (to_real phi) <=. cos_max } requires { abs (to_real theta) <=. sin_max } diff --git a/examples/numeric/sin_cos/why3session.xml b/examples/numeric/sin_cos/why3session.xml index d36dc9d93..06f7473a9 100644 --- a/examples/numeric/sin_cos/why3session.xml +++ b/examples/numeric/sin_cos/why3session.xml @@ -13,7 +13,7 @@ - + - + - + - + - + - + - + - + - + @@ -76,7 +76,7 @@ abs (to_real result -. t1) - + - + - + - + - + - + - + - + - + @@ -139,7 +139,7 @@ abs (to_real result -. t1) - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + @@ -437,74 +437,74 @@ abs (to_real result -. (t6 +. t5)) - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + @@ -513,10 +513,10 @@ abs (to_real result -. (t6 +. t5)) - + - + - + - + - + - + - + - + - + - + - + - + - + @@ -668,7 +668,7 @@ abs (to_real result -. (t7 +. t9)) - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + @@ -787,19 +787,19 @@ abs (to_real result -. (t7 +. t9)) - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + @@ -1132,69 +1132,69 @@ abs (to_real result -. ((t18 +. t13) +. t17)) - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + @@ -1266,110 +1266,110 @@ abs (to_real result -. ((t18 +. t13) +. t17)) - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + @@ -1380,7 +1380,7 @@ abs (to_real result -. ((t18 +. t13) +. t17)) - + - + - + - + - + - + - + - + - + @@ -1443,7 +1443,7 @@ abs (to_real result -. t1) - + - + - + - + - + - + - + - + - + @@ -1506,27 +1506,27 @@ abs (to_real result -. t1) - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + @@ -1690,74 +1690,74 @@ abs (to_real result -. (t6 +. t5)) - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + @@ -1768,10 +1768,10 @@ abs (to_real result -. (t6 +. t5)) - + - + - + - + - + - + - + - + - + - + - + - + - + @@ -1923,7 +1923,7 @@ abs (to_real result -. (t7 +. t9)) - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + @@ -2042,19 +2042,19 @@ abs (to_real result -. (t7 +. t9)) - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + @@ -2387,69 +2387,69 @@ abs (to_real result -. ((t18 +. t13) +. t17)) - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + @@ -2521,110 +2521,110 @@ abs (to_real result -. ((t18 +. t13) +. t17)) - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + diff --git a/examples/numeric/sin_cos/why3shapes.gz b/examples/numeric/sin_cos/why3shapes.gz dissimilarity index 99% index 1894e8027e76187076ced07c0c5d0eba9768d5ac..7633796acb2aadbaf31ccc24d46ddf3719af0e37 100644 GIT binary patch delta 15391 zcwPY?JmABed6{{T8h`yn45kM#1~94t0rQrxjabpfc!Q)nXzSO{cSvR?$s{vLs;cB} z>$b0|GK+CyJInXQa`@lgzWMOa_;X{4@v6eUOxA(vN*U#}tEq!vu|NJW_o~C+;ZNV4)PFnnGbeG9f4_N5F1YAhVPfH_ zAHO;MZ}x3(`16OKe);|9`j7gr$Uh&%i`A%-Ha+#-cfHTNdEi!i@yJcFerQLLuq(Ut z*;+-NO*E{KOHVQy$O7Fh9ZPK(jKQpdy^uF14*JA*L( z)9lfE!!WOHc@S=%+SamzetfNIOU=1;?=MyRwt+cR`}@(ny`Rt7yq<;c#>PL!Fe863 zTYsN8(AdA7!`fSvd>?UP9W z8b43^=!kUqr~lJQqZahz-TuLNH&T**1%GBVHt!Za;337H58}8vALS!$ooJ|jM&*I9 zk8(`~PM#;I!>pLA`<*yRF?8ZmVASZ7JZnKe^M=1OOU>++!k_?4yw2&#ZkfyJ?4A5O zjv~O=?%l~PLVP!Y?`KMP58}%Q5MQ2A;bMIfs%n2&`inTJlj;5flNjOIA8w%VNq_$^ zM$adC|MBZ{y>vAU(GR0QeNt1AV&R$VAAeY55*POI{vZ6;0qOtkI;tlz{M#>{okaid zP}`5+)L(x8_{TrGt(K)Vs?{xuM^Jpc!ElD*_ckHo!*$@_x}kgsJn{C zkfDhKQsphYP{VIcf*HwMa z*gdzr8`E8zoXK=N@YRnWnTWbKmX9Bqui!mvWV$Q-b9HGh{69CoZSCa0uVq};f%yp5 zj8?40>2rziAKB9m=l<-_?AaaYAauJM+1T|LZS;Stb#5BH=g^`5P_w^h)hE}j0$xAH z@kA#-(*Bd{{=GhOGWh#>s7~P&;@f`d@$m$rC|!$6!HbdS!gt#Lt{*@=w`Drd)`@o)g;=(3 zH<-73ch$OgP`v(#t5m!dBUQgI1Gnn&Ni6S_h;bl(-mRH;C%;&yf5|Fc-)RHCxapAb zx%xW+b~t*zTK)JiSp2p80}tOh1Ke%bES)!Ac~otBl;Qgzc_?-B=;~I@ZP|xIvQl5X z9xu7>;B<|bRjz*y#od;wNwq_X$L$-5UTTyc8YR~Daz?*?dviMKDrJ1cc>1T=$K~bH zp_R*DKVI=3)wViF-!300n7X#5Zx*beqU%ou31DYNFw%oXt%HJ+s2b=S_ zEqe*CII;td+F0XXXjGqN$ZnX?xC^rpTI<7aa{TMMJCGDN?qGJs?Z(N@ntbE;m#zpc zKKopgV+SK++&*pY$JAs7{omT5*XYS-%+3q-WMtXXkJE^~NxQc^xNvay<>zR;_cZG8 zKHGQ+7$FbX=lyRHhfjFzk-Urkp3*K z>_7XH=?5TxYtP==M(h14{Y-DS#VEEsGuZ4T-{2yeYZU3!**DwJN-7@ zNzcabW(9pZ+V4gqH~L*aw8--kVz1ksEP4I} z`tR3&m2P}Gck4&|NiOdJO)gnH$BxM9vZ(*=6#CW?O!!3OrqOw1(K5T(FgvMJZ)lf( z&@O##mmbFOq;4|juifWaxGUJa z;E??Kuko+nt}QzM`mfbJC={E1T)tw|H)rwN^U-}sLSHYxtrD~0xk)G1MreiUPxs0< z-x;6v`A(&mU)IkFERXXVm3}KDa- zZ+K?e0kErE_-=)bZ$5H7Mz%;QHMKA4TrZ61?A={D-LCFx`h+|5fe2s@yn5b$^Pa@- zkJ#cKZ~CR}WRuIAZc!g}OMjelJS-=EgO_ovy% z3zq)W9Va{gwvJFf4ad$#5?^@_;L}U(0eo5mey^}#{rbZ?cNTXm{L2jKbBxz^7xig< z4`50BhG&+^^f|Q6zWb~-{ZBUyYx6v2FBvIvq zmF_JB^LmrxWq+dGX9DkkuXyssW5~!JUT|Um^9j}GI>u)mv%gTRedq$ZWNYdq-FQ^G zoPBbtTYP`1`=Rd!?|HJeN0L|<+s5LzRC;4c)Z=`p0m8 z>~a&i3xBT8+aKvsy>xR%-6+kn&Vg=m}vpC(7ojqs&V%| z?dsmA24@V*MJX@B4=Dc~;sdo}fY9_`zue9x|XC*{X_ zchbY#_Dugnci#<{&dvE5aek)zTF>yKyN_EoiQsbp1Z^ym2^D*ZKH|i6&aT%O&BmJb7IXuyF`nVAbeOgqeai7H2K8dY* z#D9HS!7tkL$S>j-G--xkrr)4Vi-l$YX8O&n(7L$WG81fZR{U!Ygz=?wef{+cIrv7m z^8GbxKq-&u160RB*Y91pyE8f7nZo zj$X^$H2;U~{=Ghe85`y4_x&47_1vMXSoz6aiwEy98YlMen89sU2zFVMvS z&C+BY=e=06&bW#q`l?5j%vMZSDp?BXaSxRI3ys3xKmH&7-^)3eAC9@aAND%drFqJx+HXI@f)k@rRfeBEgo6&T%5cl zGt=FBDb9Jy%qn8<9_mwKb&%wwrt5pplROYff6{dCSQ+RJZzS*^)g%*_I(O^Gdv9ZT zL2LAV>m2m&td=IDNm-hJlBDeCY^nky)Idv!SX_I&htKk54Xbqi%qR9yea^^doh ze`I8<-Ls2c>Dqj`*x-A6K0|}Wq{01Lp6G^>*=vJoZOudm9=GK^AAPguGx_Fp`wAz1 zV!r1y`DQ57ZMVd6&dKXn;=1Fb&aPXmC!zFf3oXM=&w116?ETrv58q8@agphn{)g@f zpMHrQpOd1A3TQc6x#P9Iei`k$;>eu}f9GequhmsRKMOkW>fYjV=Un=Ap>C+*`s__D z!=i$@E*%aZhhWC*e3$sJvfODeHC|dWSsFCAOM{ztZ-yn*rG*f4S(6=VxmoTMv&X|i zpH`MTFMYa>*n>Xd!OhE^YRz;t@yIVPciNlf&dE1u(_*3da_8imS)p}tw`EpHf5M)X zPuR(@zG=H$o5~I!HD}?(k72n}a*EC_pJ(@xU+sqfUk>>%N;%{r=lJHEq>~gS`(kBt zK87frHd!@tu9-mgjZ#laKG`Spq@UE2d=lRz0GKA6j3iC*6nzj?lOt=QZ`!3d;mJSI zlbaNhQtM!aZRDvc6|yTWwHjmge?p3u-YD@T!;=&@CCU1LwosMHxDbSn#aa=nq=W`j zd?WFkUn*H08Sk{yg>sQznW~!zGFcg$C)t;zrIOk<(}JZaY!=F>>QS=^O(mtOtG+Ag zmP*E~s}o-M=!%m{i0Dbh;gfd_p3R9w?xoD@xf5UE}Y*MkAYDg%d zTGbZj1sy8MmK1AojR#1p<+4r4Qc)ZO92>QytW6rjK}RSjqdl~B5}V!5oWRBRHM0c|zZ(7`EH7=VVV$mBXzQhvFtE5Q~DWF-8Mu(~v* zT5?S~D@j?w^(tB}f16`XUJ>S^`i$o59HG)GT8y@A#-8h4DXvseqGjpfc`N*E@{NQv zL?suvn${I}D?_a;d`u7_R123BG2W)tma_0J!92RMVWrtQBwZrGlngh>fx2C z3hJ7@q8^B=E>+Mqn?a>GH6J6(*8-)lb(eY z7%p_(kYvXhe_HaUS#J@TLZB8ccfvuG-zPQ&=`E2eMRP1q_+O+ZF|-kJS$5IN>D^*8 zds;vP3!i1sNCYvfgOe8F9v-msmrm^#TX`OgNUCKH{>c);vd{1vS=wqlYj<+DSPRdA z&{?8(E>)kBuNc~>6}}cSY1V8Lc8m3J(G`d&6$5`=e}aH#@~t!thXZd>S*+bZWhx-x zi6o(4kq|iH0!b72j!FoiG4mkU{Zm#$f;vMFB4uheDv7{|NMI$0-A8BG2I}D-C~=r0{*K+s|`Z3&=N!Ih(gYq5H-3f^Si~$6p{_q0|99f zR90S8e^?!&J%CM8oqx3Z6|4}vRnf3maskc(e4R2kKLLzZC3@GnS1NE*HKjqnJa7nN zFXb#6@Lq}@_{t87aA4A4{JI8Na{#0(IW`{TtP#fn6-y7Ypt%RMtd+oV62RDFz7j%Z zmEL4h4mjK9E{IsWe}DxbN=+8rLbNDSfR<^-e-Yj(U8U^Ay4_+U$U_bi=oYF4fD$F( z7dh0EO|{y0V(Cw!4&4wslZ+^);L;#wN*9jI49yYfa_Gju?e`0@MZhB?G?0-?pj-e%fdJFs zf7wgQVF)}2f<(y4!mf-3YcUG`+YwldpaLZUfQ>_>JP_5GqIx)P5X~5}(3rI5Dxd;c zIL#)9(0(KgXCTZNgVca~fLj9eFb3s8pM(zDym9`?(Ufo4lvPzg@YyR{G=i8Gf_#8N zMZm;2!94{#F9plB=}}f1XeWuxkK#TzDeE|IUhPK*+2d(0XYxSEg6i zAOPoNpmjkFMdfnoY-_~yg3p2MARM}!9R~q;#u{qkicyZ#ssJFs3M_6b{ALD@MxQ}@ z5{5s5FA6mX(D!6igNd>PDo}YLgscZnjOlx?m@hC1c>ka{ED|_i1)pjNw~|RQXh$cYx$1 z$8sC$PULb$N8yIOI-BVR z3rkXAp5RlXMQ=2e7y+-U0MKWMWQW%MhEWnS3hRUs*?YKW$FT$6hkT)uROz6p-!S*! zc@pGK0d^_iLhwU|i6iWTY+8&|s!pEG$$6_X3=jE3k9TI+-R*;Kd(Tb-yC$H^dA|3Q*A~pEB%T zC)R=HldUk_9AZC8e;fQFJdcWAw#xfT08%n&ZDMK&WuQib2io8iGwdKZ0d^VTqv5)M zYJD=c6-B~^&QJRd9x=EoG*6q)iJ&|(A&yaygxMtRyG0zo0RyQjNf+xKMyEI}Bj87^ zMhFL2oBHq*HrR&JiQ|?tK-?Mj29?sHc!RKSWer`74;!@6fB0Y;6k15IaHB!=5eAzE z5i_poKm*p?0u#vt_=fDd&PDCu@gdRG92&5qZv*_@f?PpXBPQHs0AT2(0fi_fIGalF zDYf=SYW*a&x97=Q^+bMP;U={Sz9g&*3s=XX|YXM=oZFeku~wA5YQJWMT0MtrG*-LVJd7B2AydP zw+$s3D;#M9-vLblKOhe)>l~`w*fJp`LKJTnW&}~Ae@SORF=;BJSeg2LQn9gRylYfI z;)Ib&>ly`EA)+%z4G};1et%B*ZNhYe1l3BE)oBNRrqMT3b!fgRW&5}x>^5OGG~<#$ z-=Le|x-b)jpX7nb85;Lv)(P3tvS33&Fe?~t;MWRjSb!EYa20%Q9$Mx$s)ki905nvE zHbMj>e?YRs@6E~5uX;;C8z(@!CVfbed7%{WnZSPlOM!z6i1e^hwn-KkJeWeD+TaSv z7~wS8A~DA;Bv$5Qn&KO7aQ83t~HvD%D040F^B!qHBfs@Bqpj0(79D z(PL#y=^dKdCM*@-c&QjL)dp{Qm(t}Nq*T0fJ-7|EaZ;;yB{oEXtU&6l=CuHfAHrfH ze|t7gxltG*R|aS4&Qri^d;EmHSO)~;f)f1!3As^owO5I^<^#e}Mu3E}@CFh|0tW(B z?2m_R)VE{;Fj@tDvOu&LD;vOmLW6a|MqTZNZS;yI~xgJf7l~jwN-bs zwwSS`G#}?gK($&n>s+QBJ+N0VY@_3VnrieA;jg*|C4x>goEF7h_~KTY2Qe1P20En^aW)kIRfW&h7FC3b7dE?%93iy^G?6VygljMXr!>PUmwmFLnXWNh z+HVjRyMxIwG@E%3Do0lxFW5@002gB~j7x@%0)sC$)c|q{VT#wxe~bgLQVlLQg(QYv z8nHtrC_OMftoCwFe}_MiJqt*6a}F2=P3L0tHlxmw>bFB_GkcoKls>XIm`OG~TVNstRdTZA}f3 z-uOdpwhe?9Tn#`XIdBHhj#zXl1>F%nkL>Jkx8$mGDgs0ye`6fj0n5^qmtJ$!=r;{O z36EHc%^-jdAQ58>nktRq9VBobSY^z8JTpgZ5V}?fC{wrubIig5zw@c=Vm(x%^fBBV zu|cr(0+`4rJd$!1STX_?c$YdS2Zcd*VDLeMsli}sFZqzx z*-G%nxjFBYe;2}ARYR0~nyA&(pZ2y#R0C+l3J2SupjCrQMd%Q~!wA_~06F#B>wlsK zM+Y8=@TntE6L^zHaMua`UkWlUmwpHSfZXO1A`=QIgeTz&B2)$G#MlU4RqN;Oh%eGm zHyJ2dsBJN!06Ao((1)0lhcaL7`iKQ8t94W${}uMke|{({j6Gj^2s}{b>W_|$c1Q*; zBSNA15)!ytWW*|oPg#P14bqQ96(+gBdWNHSgr>O)JIT5Mqw7r6Q)m;8NCwrHfL6H% zcw;VP2B3)3@Av^`H`RD?#J2r8jFs<*z+x(Bky7BlfeEspVgJG&!Hq767HokTM&>Ap ze^}iaB@knmo1j7Rkv6|r5U+*+7#+o6je}3lu$WvW4|@jLXv50lpQphf{d`=@)@U0a zDUk~9(@??ODIoPYY}@VkNsh0+hCpD%k%R<5fN5BQ?;z=@-`I6WhQcZd9;l6XE&_>q zXB!#tlL(4I!qLU94_Tn<_5}qTzGljef3Q*uZ)#Tf>SkTI_@hIfqfsre>2872!1r6j z=k`2b>$E~sAHm%bFC9#TpNpzNmS&pLFybP>&K;bp>ph1%;-TRn_@XqdIc5b~+frfp z;Q-27Au)L9BM2`N`p!2c;Xi>9Qnn3V6v10*YI5*N>WE~%pyq%xd=ysrBD7+we-ya_ zH5Cw}zRgGMrL+RwWBbGKTIo~4V7FRZ?TFkk&PTkR^$G4+DUT@2ceQNbGvJ7}uE0J+ zk4W7SZ&!g1lg!q8s8~u8R1VV!Dh}H0Dbi(a=FlpNQ6&iY5TBC<*ziFKsIU`GBDS1o z(I1K61q3z#8bJfA$u>DSk0_e7f01<4ZMar`2;*r?odE%YGFTr=sN|uG7#GB@IOH$z zhd8(f_c2oGrb1wT0l%RPaGB-%@%;fbNk?=V?J=BW0W?czZ%h>q!BGV5`R;9hms`>y z3BACmB>i0INca1M1L6>@c?=7{6f74A`xcP4jU^UfWk*`+oD7j%eN2Rg{0< zRg?t&16~4d<>5kGXc=O8KQtQa>e+`L847T2A1F(VXmtQ$Uh$db=!^5EcDs#(T_3VQ zOj@ng7EQ|YaV5$upO47$e;q)1^+$(12YVrFO*GNU2uu@+5049LB%HOVeVo-t=8>Rf zxk4+n=iP4$eieC#C0f238HaWskt~F2>@qvYX0U!z;n{lKZl%ojX0={l(`y3yV4l%43;uSS`Ko_C20N5wQe?Hd)%+Px;18lvY zJ%3~@YEcnZZY%r`=U)m{vd^zdiOi?uFKFWsE+`qAOhy-i%d=4-{v`!)Q;Bqr!qJ=3 z5#M36K{(7_%ECxPe;ZyD6P7F|rb(*T5PxXzMn@>K;UrZE=CwQOSxjb_;8Gqe+#m5B zsXN!8B(Iwb%py}P1)we?Cg7~q{)q4Je7P-qt-xp_FQ8OvO@enOGCrSY@Q5YyRTWpP z6vDL}_+)@0tsI5QnK$}-hB6$n7&u~U5l{Fo41z!fK&o9PeOmJ7wL5ytV z#5fsY#b(e7f2S$0XJ>0g0Fq?T1CVWV8n&epo)kKdV%!+z>w3b3Lw=fo*MUp)T?{RYp@Q8%i=40{uc+1V=P0EF4BL1o%ij&+Jpqww+B zBD_?8%@K=;Mn>};N|)>lw@ zAJEa%e@t<3b~zHT2Oq+|o1Lu|xE@(5LTNNLK}FDu4AU#nF&M%^cDCZZVD!$LIv$Eg zu*L#XU>ivnwOPx~W}tjv?tEQYw=9iP32>}9R|}knF!!>v5h!Cq^wfMe$puVKf$vRL z@u7v3%f0MuSz}E3FghTPkKO7zxD0TF3r!X!fA3{y%e>GpLJQ7&MHyX{Ny!E=;9R=T zDYTaK3-}s9gf9q1*%DYgfj9XC=8LhV{y65Av=f4FEj8<*+5HOY zT6(pl6@^mZC_%CSceUdr3e~j`cr}pD^{x~T#q*V1i-^ygD9t8l22|On5D`Z1XJ@lH ze+788)?!PbGe(2|3(xl)D$DK4u4HGE;6c_~9R!RufpLTUgbW-Bo(PPtdLFxyP%frc zHB_s>NVBwv6jo;*t&A4i2ie&OiXr)it*gK~-Kw5|tPE!*8^k@x&gOJ55zZTNBL&Wg z6DekR0f6)ZPb(i}XS3em|5_~qkxNp_e^3!jAy|kKp-9E~N-zqug(k&kHWe>}aF!49 z8d1ZQ#5a~>3gc`g)8kZ_Sw1Qpie{zm4yaZO>;ZEEDW9b(nXb8bUau}1ILb(wYolNU zhR(yFY!HS3alCPye=x};&PiXk3yjXCASL=Ie}U$K-n8Jg z_sF+v1%*CchS?zyPR=)2brr2}axw<32Z2W5jbFCcqBv|M#3fqkkQHxsb4kyV)EEgIk?Eg2bPnK4*pMa zT4fFVgjh8!l72CHDj7%=e<14#+{wpaT;LpAe3C6`a_0-6+XZGm@c@MeeUwZY06|Dr zK3ommtnHdkX1h%IfTDG3lqEXe5c4Rs?3#m9qay3z8+KW961*1VlgX8gslcDEl5imY z!U)-~iTFJuNxVwYVg}-YQ40(!m==BwCBoe#8nSBaa9}{U+O2VI*@0mOPQO}#P-L^E zcADe&c<$<$oxCbLzKx}vc6FD1pf;JZL7z-Q^^~TV4(KPHb zX93a&>c)6me^dYo4b=o8P11V`qMfhPZ4Z60JQyI~ulAIz1gP_zLC^9Pbwt%Oa^Hou zEr=7SDcFv4HgnDt5{>indp^cl{h46wqXYtAP9;7ljZhzjl~!25g~D5u$XtXAO78P-}Hz`bs8^UKL{e9G#>Dx`ZR4eh;Xe4EUpId_ODbV=lL153D;;+{r*r_8v-y=oi<6od?Eh*zl zlbnDq46x*(9MLfE{C*pS=R7#&%}w`hyie4UX~kmXX7MGS$96eIK9VtAaC$BL){e6u%MMHAp3D!;gf zLhj@6dfJ&kc7+Ip9ZvYDm(gQiQ)5 zuE(zCIGApYMsgV_FvAzXRUt@{_MF_of8w|DAluDU85%$-VwROHWC-&m!TKyOp~Ukm zh*neGO!YkRh6A5QY%FV;Hc30S}a!SE{rtg{siL#qdgZ6>J8 zT3)<|d9jej@5v!!0g6-69+0VT*Orj}T%I#422w7AxYoqEY%vF}O9SfoWq9pzKARcA zNqhqqXbtg-lg3Br6_njVEGFQhf9acal)$YEP#9crYprm`*T%=6(Zia2?e}+AGucc+ z9~9m4+mO68oGih$0?pv{3C?~wY;CWmvH5F+zRG8tJ>W?QvNnFDl@PF^SYxVuf}{85 zn{*0DEILohRKZz|MI=7v%df@*q-}KO;*Y0I@Fp^d6Q{DU0`3L4*MRZ1f1)s-@p00c zNhsy`0$>M{(jX-?e)E{)spgFA2_erjFZ4p9)M^5oA3221Vk1T=3Zn^rsQIe@vH?2IOS6EMQae zd_N0>g%7j`PP9mYUzdgd7t0B0CSwbh8WKMprR1!(=tw11fDNN1@~hcsCPJu5Omh_c zE@=tcUK?lAa=drWX>#wUqM6{F3PGHQhu>#tG4YAtImrq8`Org_kMqz>7u!hiJ12$V z^-9c?D;VYs%2;@He?M$WLNoDjkrTB;>3G{50z#~wPxut&D@TMK8EB@YF$634L{_!k z1Il>AM^RF8%=3VodDYMff1kjp{pB+C&ej5QC51Q% zg@RY(^Bo9F$s#^^z#q3G-^_HK9mXg4=zW1fX?{5&-_ll+^VGStC)v!TwIFAlh?qB$ z5cx7E4XfIN?(*@r+{e;wnPw)f<+P#_2(6}o@GAI_D_;Y|ytSML9=I)8!~{r|)Scnc z#gw37u(H|!e{PupQ@xUDM~<1Pm4SHW?yZFdK95o+N6|1phub@+fl<4y44Oso(29a! zZh)p|0BM~9p9UZDXl~0cGmS1aV{YJal0+DVW7QQL$$-@Q+`S%_#csO(G8tQ5bC1>< z;2v-+Fi{_gF9{fagUtY~x7~=EG9}I)$}fwO9{96~ebvw_{F*0JHEvP8u2A=DScY-&DXX5>4~v1s4-51o6TxzsFP=;oRn1P!rMtV#ZD& znqZuO$(9<8wJnj%#3hp8J0~R|t}4Efs=?YUzc3_aBaPXaMP_;~p;^Q+ zP6vgye`;BT2NZFjZ;tHwD&O`LGLyxyT$)jQTr)U=F9Y#O#-;9k#~}@wSGVPlnM@qN z{(zI3fU%g;CHSwoc|M)qa_!Y&WAd2k)J5P93#UjF_;@PkvT`DM0m>oIVP|)1eIQDJ zAaDx&<{|{H5)}!RTBKlxGt}EIJiWM~QOG=1e>qovS);Q23V{TCQ%M$^^3c}Z{`N&I z4T2C`h%iF{v;4k4Riy+Z&wL6k_RIF$QpHTy@QJe&Hcrh65@exZXrXD@I&QVznI~ql zkl?$teEbq^T><@dB{+4*Da?)aqf~nPK?tN7Fn19fr_Cur@!~pX@#IrlVF;AlGQ>;* zeXNK3kaEdnDXt2C!Pk8lZalrZ37ZTsK^6={t?pzEPHMb>znS`7Q)r|NLkpcd|@Jl)>bP7}*COo82f8U<{ zWnv7RM$%e@bWT>zCl9m7phB~h<1|bcN3-86@M(QMw8IfMyTofUD)CFY6LevCOYFwH zFVmxLf$0NWIWUJ%O;1*{LuDXW^`Ab2@|f7cu?%Yr+njbAkd%#rv7e_hsG0sdQC@O+rk?aB2r zF*ONvm-(nSLYZX1l=$$3HT;q@%x5olw-1xSc*ie5B5ho7TBL|TX)tdgHm`?hw%dmV z^gJ>)%5W_@7DP9%c$tY`q9UEXtb*)cvT%G{#xkeY2yTrp*72cuFwEHae+csB=JHOl zfnQxvfNuj3WFx0FNOtIMxr?A_M{<`55DA*^Fjc;nBy*O+hAMN=4d@S@cRMn>O!lV0 zcqtKPEQ<`N9stqL!yd@CY%bG< zL8dpHfd?obrbeQBS2-b zmnNU8!f|6|w7G6g43o;CXJLg&ze0$mNOv*CB%lY6!>~Og%f!-j)<8`BLJ!QJ<7mcbRGSTge_y${CmqW~ccmacPRgK8 zq{6v2d}|JKrz(`KH;HYzSSGDCsye>B)R5sOjnyEd{*>A zDX2jQO*3CHFq}0@4yS#$Wnr0U1m=ie@al^#ItT9xd%TBJQnyYQ}=$5%A1P32HA<-mV9Np9mB^G zec%hi60wXpU{t<t462GK+CyJInXQa`@lgzIp%8_l}z zkB6!&yY%FI*yfdtBwjl`?pUn9zwZhyKk-d`|GvKaP|KV4+q+->>*si+mcBdpD;nnN zoA~?hKmYLtgMatSPw(sdzP1&y_gZ~_yzjPiY1r=;*wH=wl{IN*2oGm*YttVzcU)y( z;9l zT0Rr}XeLhj@9WJyf0B>=7@ir4{qcvnR~`NifBJlq&wuP^PU1v=zj=%nT=cClvGCN7 z-<)-e=xCaI3v|2-2yxMGqSF6HIHU#YttVz zcU{aZ~ih zQqIlepDSkF$s0>O|2}?x`tZF7_uC|7_0K;JZCAN>JDP3Q&kY^Q&&O}IzS%E3`hJC5 zI|?n?elO?US?0S-nR|M5d2oNbr-OCz?q7D!xb`h|eVwnn^L2qeN2di~h9R)L9r2UG z&yzYjA|3we|8!EQ1^sy5KN!y=CFxgSMt@`TyyyWBDfWC2$IbabkF<57q3Q*d2f{wk znhKmePf&+hF<19HaUwBv;!Fz;%dI0h1j0zX)BdDtRVd*d8Bu~2g3ru2!XMebX!YB2^7-l`6 z=>Fr^=X&XK7@{9Wf%+t;BE`Zp*FXNS#w0H6e5{Je{Ou++R1-k%ebrq^AW5WtyqiG=MvvPvZo!+{l%f#i#yOk=yo@< zvFoqe=>Jsf+%$SGp+o!+%~M z5&Ke`oWX~o$#<&WV_?^+cUsbk^ul$-(+A`~A0L$$v1SKKaEu{cBcf`%Y{4#Z8Bd&(+@vu*1>w)#}HG z!Q!vwA9(oA8Q^ZaX6d}~%A<1AqYU2%$wR4|M_0FMZp%I#l9l@6^?1p32d8U1Raza2 zyDgQIYKIb!+cy%u)F?GHO04bWjDG$0=5*9m%J_)!^iQ*o%gd!hE0@21ykz1%s%>?U zzFj_0Fm-K9-!3kW&iZ$+*2^#JzI=I52Q)kUZMktPmA_rO4mRg;TlNw@vi_eB<|*t_UqY`%;r=2P0$DK5g#D z)MN(z-`b(i(UVV@omc9~$g-y&rxAOTc5iub;o$D;&(V1AY1H9;w(%M;f)3c|?3WiE zy{j8|QL)S6Voylk5G-C%srCf>KZBah0m9xkd{wc(f{MM8{w%HRzxb2x2Oxjvp1rk= z*85ZXiQaCDQEYi;x>2xC3->pBZ|e@}$V=DuXV9mU?YHbMn-lKjZnyY`M^53==6>yT zTy1|NQ=hV^YWMv+hLvV^xJeNH5@4EUbj10bp86O&BK3R`o@fwIj%b^ALLatE>bUxF}IS(5ql=R7yW@)=HNHz zwz(rLauK?ymp5&H3~tVyT2aEw9@n@%{r1poS|M?X9);XB)$&H)l&LfMKnZ<^gNu6p#yVQerscXB`Foq|2n;Bqf z&t<8TchbT9-=BW1zr+te<@dL14Zr{Mr}Oj6f6Vi1HWQb1TXuD8hlM>HwM%>MF7wdj z#7^IkZy)X44bP2s?>2w$@@#1Lbu{h@pWe*54#~ZCpJ(B&VEu|i^6S6Gzka*6==|%y zR`;M#Z2EEeic#O3#c$6?_aO;=z5KRH%!cPComd;86{bJkE8l!)eAeeXm0o^XKPRv} z&TCZq@l;Qr-OqQwz_8A+`TYw2GDG?j<8{La#vPaq&l;;=6u*DrnPmsSu5RJG6*j*4 z$oY}J_U`67LA-4_`(kxUr=`AsI9|&!VP-#@CVzImXK#^3hqh(5S9`F*AYV+YXX~VU z=KF%{cNcsVxj#wpesA(0qI$!0A8!3uwfm}epH=PFHQ=);;Zn_iMy;HMm`_*JHO2h( zkMXbTyycH|-tvFP?BkuYbIadec*`H>yG-40>uB(g*#RYdvBpPN0QM(tgb#hbQ|aZG zeFwiFcm-rXCf1*N?&}K->)dMZR`{10(w7*o8(*=u{{R_t-m=%VA1k&@m6m$6;hDP^ zXg_y|e5nh!U*q1(#l3_3&S&fR+vURT4cqN){QjR;&wGE~llc7+TioMKzqFlfa(UA& z>VvLn>yRASGyZDaU(~oCOx>4L>{-{A!S~1Uuj}CZ<2v~MIQw|P(jU9yWar=35z5Em z*x5+pXWj$&_*#1aAJ>52XIQZQ{KGnT7I!QB%M9sDjMsJ-^>KXcbEBm9vyrM=JPp}@)McQt(H#o z^3_%fUXOIIt~YMcy<^3eSLMDqPu#Kq^2w{4FX?|V7C`3LwUe)FC$G46vUUIB1=2r$ zjZH5Unj9Iq4YJ`s5Td&QG49z#a<@QMrjpH8Sg)iJ*4nEi!f?L!yP zC0mmxvg1+da`w?wxA^{2_e1tSt_4ovG`ik}Ph@7}bb64W?nJs5sz%TE7n=CrSzJH4 z{*iy{A8$hOX>^0Cdv@`<-St_y*x>c>c4;t88r&xv^z(3WveyRtxrcu~54qrRt95Md#;mR` zb*G7+{r+)lZ2a|K!~LKBhARJx z8oFu!^^f8H*ySd27kVep^WVGYFEaaIKIr&CEqm{^8iyxlwT{ZI)ZEv}HzU=^^>sHT z&!0bxF8M9*DSVLm(tv6E#z^PGBwt}yfS(?3C!7T?VfC)L%h0-OexB4c$FV#x(*l2b zp?k|KRO9Y_+||90%iUW7j9vFu*B&0J;kp(sDd8vU;C&Tb)44Ud2 zEc^mK_~UTT8oxhKs*|#p8ZRw*JMMqInU6U?xKW?DjmzMK8|f#t%;AZm>El`~^l4F< z#(ff7`y{sN5%*~YzbMZmzldMZq#1sheuFkG7McN=={K`N>*8+9Ot8gS@vk`$#+T03 z_17!p;2Yi2_t&VU<$S~VF?`gVn;1X(%iqA!#S{*9$-?od{&{A901hqnW$x!v9v(_p0c>BkMh zph>|yBy>)ta;)*@oVwLVSt2Af8Mb9U-Sp6h5+ok$D z8$GAV-KE9q-=A~rtmH!*+FRvAFmruvN)Kl2Etom8p)ujO;Tz(d%xv=1#YGQG(;YBc zvgElqx+F7G-Fqp{dCK%EV(%X6Q(|?HXduiA$cl z_2a#_vAm)+`o47*`ggM9rrGnz{n!fFfQ^SerG7Vcw?6*0(AES4l`EiOmd?I}XC2y||=iZ)=I`1c4pTBOQ%!!Ka zAG!YV7L$LBY_)rK(JNh>Pm2w{x92l7SWFt+zvao@P%?9Euv=R*p}^y|yyv5C_IxJa zoNiy?#81rkd?w!vWxDN_ILCCMJ>gTYvEy@+ZlVH;Mk{x`*4HniT~{2rQ{jL7O!u|C3g~A+1zz1-T<)Apzb@1b zHC&&)sbyGH(ATBI;o}g@c%APOA6Aw-&85amOD0Q$`gUn>^X|>Cgu1j4qAzQ*LoGMU zonrQQSm@Kra_6N_*AaWrCp@@$xl^v0u5vu`%gdeSX1R0n4cfF=XujMz`DRvVUEFP% z6_S6jXXO)iGOTZ!F4v|s!$-wgIPqgx?j%mp+2!->KJu&G@W17d|EiRO7CFZ^-`HG} zlN4IZwvku4h*qtJR^jR8z8eI0>6dwqC^$ z-h?OrYX;Bia99Ce+{}6{ni4$*9zt zud<}pm9$GGt$HE* zqA1_DmX=ClI4~V>mRT85DSJ=SQZv^1AbpYNIu{E!C&*S~bie?q<^pJ_(oNJ9ywXl| zg~d|IV7w!fk}u9{hxuq(2%Rv}R#8rUwPtZ*l8#bkVWPlDYZq!wzGhaUm@&g#aKf!lwn@UUGd zYl_N7$(*b(PB~1g%b3^_WrQ+X#RH_|a#>h@aaM&;oJ-DoBQkpHq58EJt6f)?mdm1X zLJDJ&OdeCAvh=A~hk^2$icVcwv0OGfDHL3YsMdRh!Up51Vp0?WG}^N&NxxiHz(UYx zWlarA6r;RqUcwK$7Okbu;-r6DE?d2}Rm$X)k&QCy)lwQbBmrIrB|X=>QXK6w$rf!v zl3i{s!Z*TyI#^+ex`nQ|T^nj0TS}OqLZSxZL036AOVxYWdsjBB)JrAi7FDdCib*0S z7i<1N*gTx5W%ne4$6)7bpr1AmdcCHeP%jBrlUgirQdQ|(OIEV# zhAFF#-dOu&&D=4Dnu6VV#hD~k3aWodtk@wPS5;JhLl*Bp1kLX_VpmN2wBs8ouSw$*~41#^{33lWoR zcxbKKE!NoFf)pAK-Meb4l9=gGH7rfDhv~%1-D1&W?-7y_zLOMH+ZL3?d}N!19IV~a zZm}77AZoY`MHOKJz7G-CYatLGqHJ9p(_#PEN`RwM;8Trm2#J548rW2AHa_^+#dEWN z%HW%Him(9KLyJDx2ml6friu+En9g0A{Zr-<8f60DsR>G9U6UFi(xmJvuv3Vg*!@!` zix6n4Rv1>8fU0or2{mb0Kaim520`o=t1Y@J;J$Rz(niu1aa==d@xQ7<2OwDH-m!%` zX(%p2v}>(t5TJho`&Yg;^g?w0(d<_+3P2rI0P|*`x#+44S|$KfLUd0_^saNSRJc${ z6fw3y6R=zY!nDGb%3um`a8QH;lSZkC>Lb7%{ESI1!JLJu7LX7QT+*Pq2ei!9l$Em* z5G4d+&`9XNYEdwjWONL%X1CayeTI5j_(;0J%lO^>!v<4w!_5v&yCffHcHF zG_=?Z?~pS5TkXTX+3y@xAp@N0K*n;B8OjE<3Lhpaa8-642(tVAg7d)g=&vPkEtf-z z(o1kT8H#@d9#uo&IS?d3P%}l~q(UkRm1GDKd=mI82;nFWk@7%PbIItO0~u8f$H_tt zPOV|?fb-GzA+#R|!@;L40>B8ogz=uCd1i9p!4`o}+8gViteegYRNR4-e(Swp8KB zTCr#c{+&OeqD;fJA{2p?c9()nmh zPDU{8@=m1A1f6>GfI9`mplW|03j_y%)#R>U8|Di*1Cn4-NeizTG205n zKt9z>P@_)HhWQFg3ea_hKnPw0xB<)+q%1K+4bHDRIp*`pi7D1(IpjsyZpt7WO2KWw zg#f{-f$4oNFQ>y6xe$Uctaqm#0~(? z&33)>8|K~v9)O%y2_Z?T0{Q^dpM-x41@)SObAMhoYrd3QjdyiH=$@;C|s9X1c|~lp-i_MZfr8fMxPcAu37}s)Rr3L~V!} z86HTnIZ%Y*OAX`#A`*DdhL?XjyQ%jZ{GtYU5(J+ZEDvu>1`t+SSeSE0rrrZ>aEc72 z5%#ND|@Mq}tEg29FqQ0#`$v08#;931Ha@@m!hQn=0$4$> z3@Q)27*>Tg5}?Dx0u)nKx7ZxE*amxJ_)u>&%EeZI%`4oSh`=9Oci4X=Y|us{;Z?N; zw1k6)L|u4z9Y7--s}*^`np0Dre2SFnuah?iWT z&enp+nnqO;=<4;LntLLVY*U6rnd-1yWjMlp)uqfZwaGsqqei0*Vj#&p!os3vvVS ztYqepas?4ZWJwC1B8Y!XDlmf}fky>zfr(`q9$r`$6TQ@MFd&Ep&=6gL>gG_L>~?q* z3*ZegbzfMrB0@!_1jZ1i2Ff~s6Bnpk$f|WHmz3BhELPD#tKq(y_r(P*;Qkaw1vo6I zK7axcZ4>5+qIdmr4X>6eC5+4trm6s;eaG2}HnvO^Knsn-8dK|- zI*E-fOHtX{AO@%oO;lP~0@MH)78S-a2=m*7VG>OMX10YeTuPfnz=#&U-^d87@3%G0 zHer@LMS;QhwmXwjEr2l8Q$!JD(xn%swh4m+gLjq`tmI8_AHdK>;yoD)N*`J;%x)7V zWI!JcTp1z;o(_K%d;$J8iz15a*NaHFjj93muAyW>kcCCL0*F-LPYT+JFy)4ovTfs! zMyV)y5t4zU#i$ztN-e?XEBNqvi}!OkOJjs%0;@(;f`Xamp!N!`H~NCC&C~M;q0@)NVIF zG+nw4er*b`ekYxZv!P$H@2z~JaUyy;P<_z|ku)PRB!E;R+n{K!<^EiQ+-L#@_{J&| z4FaB4h*t&TgRfrmnTx?~NV!cI;uW;tG!UMmg_5u*L>UW^=0TWq?uBifRFH4Pcmyqn z*+pQ^i70;wz$)WaX+HGhwo#Y_?oooFhpW;MG&V9^R82R8)j9~$|y8H5A!WRMKFumCyZ9gV%t2^DuvX2{_reY@=$p%I~Tc0k9vz7zUmr zV}96vw?CLJE!!#(F%m)o1@thcm@U+djL?y}q!PXR5F7m(nUXYkXF#OGus10PD#n{Y z2n+~Zee3jR_qPPKuvrtIi}6xs>usxmVl~@X=zI{#ZdVZPg9M2X1sVoe7@7$w2UoK* zzJh5Nd&_6}wiro+uIW0)iC+7aNxZ-z~s%Tqt>UTIvZnSv7x&(jJY-!T*%6TRDIJl;k3utn0 zRdS<=G8t%&PZ|O&H}>F3)n*7pyS8R}i;^47^F@U@1O$|9!T1Jm#G6>H0*QOoKv;j< zFbNxVHwg_(*AkSl0k1g-Y870gdWG=k1{AZ=aUiS%KT4YcBXw0e*;)ZW5{$uT+Z#gI zsA`CwpqVHR!&VK*iVp!K;@wn{s&^N@xRvHXtw36ZwuuyPfNR*8ffI(GEO5s5!e+OU z&}thzh0y(N2Dz&uzSu9Y`2XeeMUMiQE_8M<&E;&em ze_p+-&DpLoT-t9CrUBO#iuzhx@gDex_miuw0JLxurW3{`!$yI;X^Vhg3I%^B30|Q} zSK%4~8sREz8G5P34w)@eVuy_}2VCUk0s(v+;3r)PHKqRCD&}9)PRZWs?(7=olyb5S zUe`Ovr>$V)h^3v%26;fTaw6uSHSj_dNr9r7D5Qp>>A-f{OQr*o9XW?_@Bwr01E1hP z{87M`k&-OFw|^&IMY2378R36AF%roF;W{B$w?e?^64O_U)IGd5_JCw70IaLb*#ab& zOoqL6v9`f5a+5vKGvpVI(ix!Y_j3^^%WhU2YYA0Kicpa%yL~ zQ*#&$-~}Lu+=FKAkIZ0`)gi)!pt9E5HUddVAR|#F7j56>&i;1KV9kF4yi^b*XN15A z&_tyKOWFci^mJDrnL$1@8H|DJMJP%V`iFlBY>tmidDH8LK4OE=X0UUm;LIxJD11s7 zk7z*XEKp!rV&G7 zHM)R&45M*G>kv!%fO&rg+Yk*#n5qoMkq1>4LYQ>M&->NcD?X?K6SR^~A{c?GRLwX( zK2!U%ibsax)f%i)!{mvKxoX*Jo2yN}`zC0TJzF|5!U*a~@LixNZ3uyy0+!EwKAk`e zhRY=Sh%XWdsFtt(fLnuY%jWsexNIb9Nk-rS?2~!mRe{>n#H%8S< z4hJN|lr1G-48B8AK?@PSI0hiPsOV!qBIZb&O8^uSfLpri1^^GA6oBAEjU~p=`qdY6 z#3#L$8LC=+l#YLQ_%--(MUYaNEbt*EjWOw4dpUqL;T%XqFrYOO_&LBmNsRavZ5+Y{))?F1I84M~NQ)B$bQvZGkv4!!)&h`lMtgp}|^d&(_$6mBl|# zgFzWcRRCNvh~=OV2qqCc*=JB$J9wodbC(KVAp;6meDl=vf%pt>$6OP>wU=v;3`KQ_ z(|l{wfzXTC-R}_yiow=Y1-E#x>q8dEi(e%$(*%EebJjbLHBj4v;1XgAFrr@i5ic!6c6`Mpps@t~05yiw(1wrWp*Q^ks6FDLHA{t- zxR5w*V{obj{^Aqesw&yD3VQ_MIU&6Ri{*=e4vdg*rvf8@lMA$+)MYhu|7dVVgPNOZ zf=7SbRL9rin9pIHbAN=H>>&d$w#Zue*ht_NaKx&rl`?`T6U9NVk9a#zl8?ScnHwLm z=ew9v@yb^U=!B(S@)2+6D=`H(2z<$h*b*Pi;~6b{m%-6xZRXG_3Z@UHf5NDSyP1Dil%psKTAur(KK_s$0vVJDj8i1I9O# z6^sypzzEx;4tK=Dt$;wsckP82oEgDH2d)ol#i=p`TGo~gjHE$309W<7YKMo51L zr)cojWv~`^WSpCmUU|MI>5OI%SG|EB(S#bcDZQUohwLzOwhhnwBEWQ-Ff`~qV>>>H zGVEHqBU<-$73JS|6$O26aL!Nz>A@&GAGx<^xYsK4HThmE4h@Au;I;ykN0R_&1JE~x zY6NlN!-H45K4gJ1@aB;33_CSZybgaUqLNTUfmPOvKRV<&U>X*Ul+~dRrGb#cn|4=6 zqyy+1a5iO#f-@+B!$vUM82TFt0DgZWUXiutGf;n^+%;FB zlj7yaQaRBKFR1kT><_JhfmX&QVv9+5T@e8!XHm#}%pYd%FKFWsE|6YlB{=t!D3O{3 zljTJ_;!ANrWbJ~I4&j*+f%ciU*p{o#q6Qd!17e2mpT0Gw&SwY)86$#4n` zq4=Q>@k}_he_C`P#1ZWhNv3}i@FY%TFEZdw zcY|@*r#`f!Y^!Qbz&d>6O9D35rg>%1W-GvyYQMj(j_!oBbLJdZqD4fNTzS7US40BQ zfUE05cD9fLh-tG?3RmIY`0{yy`;0Ph8Vp*@&gKBBIR%RnVET%;5)peer+9F-w(}{0 zr-js3sltGZ$CDNW$U1-Gw7jzLhJpz}we{?528s{FBV2~BQC1iQ_?lZuDT780yP}J^ zxS-Vqremvs50$`UA!#XLnI$NMp1hu&Ev3X4(_IwKSz-AyP$~jN$yGi9-Xnpfl4wy* zBy{0BNpOLpy9%U0g85uiy_1~{#+;JN9j$i~_CK9-)|E41KkW+1Xl*IdFZs^QO=~ z1oWH|gaP!%az1x>o7N3;!k%1JU6R*ML{WJ=&+yHcc%9M3sc9fwhz>qh$wb{l5ukz~ zsY+?kk$g8h8<2l#p;&>GoYi2=(s^0I3c!gJ1pB+$*|G+%Fp1~Mq^Kod{*GB24YPyD zw3MCAOND?1{#k5b=m(I-hpfD|Qo`ESva@l{M4!+tS(<_!!&+cwl(Pa3u_4{d&Q`#0 zsI?mS@?q%GlzFrgAXZ8jv%Z&|Er1B90uGyl6}2|Tf5LytrrE1>YIG+%TLtM(v5<&x z5ym^9L_pk%0ggaq{$6%AI1eZs=lB5&t{9+#7K8*WXn{2Pi`Hw|*|G=%rkVt7L?Q;j z=+RioY1aTsY`B-5O(nho27PrAgPRMCJpxn0q|f!P6xUHon<|XOI$69j0Gm>X z#D1q3*(ZOMTg%QyrPxBeM-qz2(PM@jTNK!N%dK0+TFcI6nL|jy+F^a7fQGYgOT;TD z_RM3Ko1BDb-YPE|bg}T2eJ2gV5uh{ZkA9GyO;7~)0_ifqBL;pO+T2viyblw6Di5-= z!5y0@dC4^yXa^#$wivtuV{!sB@gO@JSg*m*pmKi%Y4~Muc>GV-79d9|%lS&Am~|Lv ziPMKxgIXGyR5VOWGmuhF>om?*G6m4hSEFTZfQzBaUaFVsoalSGL&YfsESZLA& z7^OLwaBP92w~DigMC54UB_}s1JJxG-k zxPD=(%xM-qdd#iuHHmgegd-`?K|Y$&l5c;oC8zjGXyi-iB)emdlCOMhmZ(d#O0$Wh z>k6Qe1XLIfhmVKHD2B`~+Xeb8tmgGaKsSZ{^X>g6C11ah)$4Apfa&pOfwfo{tn-#J zia`|Dh#q`~Mkh3~<{_`ej%mrnd#!;_=<7_nN@DyZIsKzi^_=u&yFeEJYE|%T@_c_q zMK?jb;^IKugQ0FofLEe63rrdz1-uu;j=zkKQ;V4KEhLix<^6 z=P;iVC)Z`})E$-P)vPZk(0fW5jK%QX2J~8HrBmbk?F~4O&a0+hOdfDt3%Wt=0-t=M zs48E_5DH*Tq<(XD&lJD7JWK&ZG);d9w@|?vqmo1*-x1-V-^_G-oEJhkU*B(;v%eGs z(F_w7d@tBwhO@Y)liA^HWGqEc;bjn^4R5L?_#SfE^D*!;_=a89tdgl@!21;_3EXru zUV6zMT!Cry9rt@iGK2L4%aY^-pwMzlI!8{T20|J6`hK5PV@Izo`m90}k~4qP5=VJK zA$gUgNWRai==ZqTB7Ls-$2;M9VGJBh1U|{?q=0YivuN!R7!_kX;BNuf#TPPC;{7H7 z2?4xD9ZYn4;*eD)2ytl5C~dPEk_EsUIpSi@2{xsB4~Q?H48A|HCqNB0`~3lx80WO3aYL=O5u zP(wbLU7p*+y;Q3e`kRUg8Wap(TLP8Aui1_;`d#=YRVzboB9_FP$h=i(eUpU`FsImO z;@RV~rS>Mr25uQV2$B#mWgnVwQYlV7&d~H*U&}n1X zV}5{MK(UJRUqLYwpOSy|P#Ow+VsF^H413hOWX|yu8mt5S-`keG;q|n@Z*wS$&d7Zi z)|Qpm{4f=T!1>_&Er`DKL^Yb2wK@}weU!i#p-X1ogJ_^YrugD}y7d*R@{i(nS)b9Nz;NO0!fHmx!kEib#};5Fa2QvG?()dV?{fd>4*tibFvAD0!{@@XS@ zYQXlGDcsMFGhKf-R29<$iv`eErUa^)^FK(dR2I_RPmMD@2PFYnYm=&Ayf|@c)Xpet z(QRO`{*={fUYtpI<6=3b3OWMl%Ouo;ha_Pc(hP}&R+HjP(3+{4`J3fbO%>QGy2zL4 zfC70Duipt<&4@Eara~0HkC}7T7NJKeEBHpO6^OoK$ohY?c3F739PPoiQUl}7d<+QO zAtC-m&K=0>#dmMaPdqv2As4;?g90~W^re)A?|x@fi;wQ!E&f+&P~wz+uEFce*f^_e zto-5(tvOj$ck8c%B@gAuYJo$dg0EoKUA*HPkmDihfOWN_p$IPeo5LRmFvUGp;yGyItZYJ7E0K0`3c4W6@$$9`9 zTLm1cJ|B`@O?5ME6FhBj#&D7e!~>7k8IdjQx@0ZN{X92Q5@>9a{Kh8Ft3^z=I41!p zTY&RS=6;f!$%ylD$rk!?w!G2pmEmOzYm$=5aP5H8{u-_}1sWMaLJ{Nzyl4zAldlQ^jNd_k zs4s>*E?Z2wf+6T61ELe=Ug-=b&qUS|)4bs@!fLLX={XG8T2Yx_mm^AY{5Aw~rg(mb z9D>m0HpXX^MBPi^96)|){B}XZ2_}D~qzXQxvh1DbYKoePtKytRAo`BC_4(|-;cYo~ z?R+(Ga4xI)X(sE7AgU3Q6>Ed)lwjfdK!YqopG5>KXEy!VL!mpNbSA>YK?unu+H0`^GSH1C2@5Be?OwHEIA+ z%U-}qD!xrn+|49EU+Xnc2VIomEiXZ^6TNCFcm`# zFRFIro|(+H<=qyjI&>dV*)+{(jZ5XXfC2I5%jKq*7Aud4)uIKMgyw&|GZJB&H$nq1 zgJhU&84hD^OF1)9Ex7vR5ZqbUF~1` z1@Yv|j$|_vy=|J)sx(AqFgLhSPU~O+_a(n7R}8rqHl3oKfT9S8&L`X&(0XkM8^!X8 zUjo@Jx<5~_F>}?5VCWFxU9YK5#RJ7JC;tQA*Fa9MJS{%+{Zp$t+r+gN+1YOBB0a+ zKLa`qNTz}HIn(OqTTm0BaQ=dCDyOW_PF@P;%XZL*$gh&?7dW>il9?cDeruZGldbRp z2(Bgbi+P+?UL}8JhPO~}&muD!T-ZNsseAvBQUyMX)5^hPMQi!!?bXrj9$`Ks%!wKJ z`i2KI!Eahy$xFWh?0zta-SGi7gr+&mxyy|NhvhW5KwV7}-;wTF>$c=Eldz-FF2+R> z0Rad>+u(~UCUY(;28UhP+22}lHCTayt_ei&?iLQ?{SbeEXH%9tEk^bu`vks>VaER%pnO;fP`VwG(rrufFx~mr zaONCzlZ4I!1)2|jMBovVL*@&R8&3`IdxqZkq^?gn^>iGaA- z1YYR3ydDRi}=Ji8xwU)s0y!N(&&L_@>3qQth)-wR;=er(%hNdE_ z7d~RhZ=(kr)0}1jOp*$a7%;Tid{=YQf6zT2a{_q^ieIFY9Ov1tCBW&J;lks#1TYh` zRcwD-_>bR-%Gd8$3!<(X=oBMfc4mK>uzhF~-_)|UIO5k60E&a|SJ8a)!pe)I+3yu9 zT(2@B#LPEVr3azFRGRESF*Q6-!H#e4aJDPKi)-g;+ieuZ76oUngCq?uNv^@eWRa||8kXGivu%l9rZJd=G1VF% z8W(`;oaTMBpm}%DxS_SXeHcQxPy9YX8#2G_0|pX-ojl*i2lBnHg6v4i-L}inllV)VCK|&j zIJ={_0g=pWDv{5}+Z1+Wc9|}&}!d(`{?0QA6*AGgM0ig)#^bsKrSrowzuf{a(T7 zR4BHX8^7Yk%fjz^ln&jnhF^Q$+u81kbG*MJl(wc+&hHdcX?%H5`NAjRdSbmTQ_E!8 zm6Hnds~dB$fp2tmFT(LSeK5>o{6Eo-d)qI6ogSSVx-&U0a zN$ZDTH&%ERxGxZ848{QTnOCcz1{vI}8Ni(&s~z&2>>dIkISzuCCUhNE3^PuAQw#G) z**LQ^Da#Z*D}Hx#DZt_~@H%z{hmb`YBklQBN82;9OqC3hL{b1?Xl;KaC3!1eWCvf& z*8+OcyM04boP{bj&aIbC3BU<~ga#@Ph|InZJ==1zOq`_9U?l+kkyB0pfaJ&t2^g3I zFAV7cwum4&5IPZ1+?=y%c!)nL*C$RSy*OACo;b$mft9?Bk*p6^%g$r zg$N|vkZy3dUoZf(A{cKUvgDbAzJZkRK|m?shlUl>ZTVLwVwK7K(%>2}ut3l{yW$zt zuzS;kS!_$bGCkX(LIwrqx4FTinF7L>Wl)*Vox7ASTeSQ4QxoDXXVSI}v7OtkV?&$= Z#l$#p+L0mc%7Go={}11bFO+;T0RT+m+G+p* diff --git a/examples/numeric/substraction.mlw b/examples/numeric/substraction.mlw index 8e5b1dac9..1dc89b7c6 100644 --- a/examples/numeric/substraction.mlw +++ b/examples/numeric/substraction.mlw @@ -4,7 +4,7 @@ module SubstractionSingle use ufloat.USingle use ufloat.USingleLemmas - let ghost substraction_errors_basic (a b c : usingle) + let substraction_errors_basic (a b c : usingle) ensures { let exact = to_real a -. to_real b -. to_real c in let exact_abs = abs (to_real a) +. abs (to_real b) +. abs (to_real c) in @@ -12,7 +12,7 @@ module SubstractionSingle } = a --. b --. c - let ghost substraction_errors (a b c d e f : usingle) + let substraction_errors (a b c d e f : usingle) ensures { let exact = (to_real a -. to_real b -. to_real c) -. (to_real d -. (to_real e -. to_real f)) in @@ -29,7 +29,7 @@ module SubstractionDouble use ufloat.UDouble use ufloat.UDoubleLemmas - let ghost substraction_errors_basic (a b c : udouble) + let substraction_errors_basic (a b c : udouble) ensures { let exact = to_real a -. to_real b -. to_real c in let exact_abs = abs (to_real a) +. abs (to_real b) +. abs (to_real c) in @@ -37,7 +37,7 @@ module SubstractionDouble } = a --. b --. c - let ghost substraction_errors (a b c d e f : udouble) + let substraction_errors (a b c d e f : udouble) ensures { let exact = (to_real a -. to_real b -. to_real c) -. (to_real d -. (to_real e -. to_real f)) in diff --git a/examples/numeric/substraction/why3session.xml b/examples/numeric/substraction/why3session.xml index f172c0f4a..8b041256c 100644 --- a/examples/numeric/substraction/why3session.xml +++ b/examples/numeric/substraction/why3session.xml @@ -26,46 +26,46 @@ abs (to_real result -. (t2 -. t)) - + - + - + - + - + - + - + - + - + - + - + - + @@ -106,41 +106,41 @@ abs (to_real result -. ((t4 -. t1) -. (t -. t3))) - + - + - + - + - + - + - + - + - + - + - + @@ -152,77 +152,77 @@ abs (to_real result -. ((t4 -. t1) -. (t -. t3))) - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + @@ -250,36 +250,36 @@ abs (to_real result -. (t2 -. t)) - + - + - + - + - + - + - + - + - + - + @@ -289,7 +289,7 @@ abs (to_real result -. (t2 -. t)) - + @@ -330,41 +330,41 @@ abs (to_real result -. ((t4 -. t1) -. (t -. t3))) - + - + - + - + - + - + - + - + - + - + - + @@ -376,7 +376,7 @@ abs (to_real result -. ((t4 -. t1) -. (t -. t3))) - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + diff --git a/examples/numeric/substraction/why3shapes.gz b/examples/numeric/substraction/why3shapes.gz dissimilarity index 100% index 9148b3fbe8a27c3c6d1a01b1d70b9bc3c72c56c9..3851dcfa25fbb878c2c1ef73c65dddd15ade05c4 100644 GIT binary patch literal 2785 zcwPbF3Lf%mu$Sp^8Z(7Lw+l2t?uc*cg> z6Ci(|!`pgvdsxcH^`}Xzo&v)KFwIA_}&rUyTk59e5d*A%a;oC2rMC{t(;CEl$ZszB^Uw-@4 z{>UyrynlV85#E0Z9(L`^mrwt>`EuvKd_4H!;%?*QXOA#kgFITeXeRw_DJ#W9CBKLGDhdrHq{q~s(Z_hKm{pPs-M9<%CSi{ov zl>86p0BL7$-*kKT<@4d|`24GV{EDHyl+8Y#CxVVVJkjG5Uy;cEY#8w6(>K2T{x4jS z*6lvtE`aZ4Jm^?&ZgsvS@|aZ z|9@ouL_znfe@_`NWnw2!&+@CiR*ScJ`jJ0A&1b~mB;t=O`mD&D1pO}Or$W!(F7AK2 z*-NP(v20KIp1wU>nO&;SUM}_sv2X^lZyCv6D&sPiPp9KmsK0eVf1r#@nOrkG*Uri_ zL-Kqj*Cu{u7M^Oq;2F-D@ntlfDcY-j_)fHab3_l1=OT11kN#PlJ|*xH@BS|8)voOo zy0(dzoNf&-!{?Rmb^A>ZuNy^fU)sl|h8NP=^Q->lauaS(3OO+~Pmh;b>+R9-=stqe zNjn~YuJ%JOFtDG!UBvmG^mkP~PeAjnW^|Dtwdy}&_J$s9{|C2r5u1B|M z`O(!8?+f1e{w*xSN8!=&-QvIZPB7i#XM5Ite8~y!c4llLj^@S_oIa+6$gR6aO(A%^ zq4dq&6PKtZbvVMSKJ+xg#_Az&jnqN~jtoXiJ)= zNUWU-39-v`EERTLb5m7E(o*ZNES@B{+|8_oTGvVlqarmKHbq0C4BK zgYHUCT`RYQq7CJh$c$@rt=KiqstAfZ(=ubp)e^TjB&9qg zL~s-L5r?{zB3f2ZzAk7;keOX)a7GVu=p`lT>^XA@))7>$TdAR{o?Gc$nisU9x`=A1 zqenGi1l1kt43>Lg!4e6WF&YscrHGTNCfgye6AS_UYfe3-mH{TUZk*UAWez~s5i|=C z#f8xInnJjpVd+Z`#bk3-hY=GnJeeouuu0{1VL75D|g0c>(Z8*4q zYwrs2OwfS39b&yQDkw#eK38D2g2S_q1jv97s3j_9IG}X&CnqH2kWaWNn5d4y9gj0&4HpTGxV&-3GY_}n61Vqe*#a`MkI&=T+dKt z>7n*kG7?F+Ti*MVQ9zuqULzteP=y2F0w0}lV9{&2_a|@$0>U+zoCcW%hHQZvM^$>y zn}GuI87DNj1Hu_(<{C-TgbQhLi8b}3Kj~v|DEL*7j>((_>V@>7`*83%9sSAV4zB|b zn&DY$$DR@HcMYL(9LbOVBp{*G0Dh=XSuQ%rvdjyaT$MK}*cF}>a0`Hl=9$AxpwR$7 zgRgnFeDo)MS(>zjt%ibjq0_CDRHuNqkm^06J%A)&-)92>O%MTS1LOgOG{^M$hG-D8 zBopvB0E&w0%(yi~&;-T=oW3C%mx}_j70h$MxC2#iehdc*l@yQh=ube-*ohKroT&>W z9PS*=gXqHg9U*pAkS~IOXeMBXFz#VCa_LK+ajlSf^e5M>1hV$*u|{v5D-0s;Nhkud z4>MUdQGh>*IP0o~dZ3JxOjA}i5}Hp5BU(VqYeK7Fwf%zFm8;y^KJ2*+IYl<)ls46ckh84f&a zjo@$&#(=$Jm?t0oiK|9c+!MlN9B0Rct>CU^4W(aT_;6IFKEXpUzD&4bftz8b zAf|QWrF(w@Fpb6Zu(P-b(7Lh-NSC3wlyg7&lS~Edf;3k3f?T3zBnNke3tkWgkf<(61gL{7cYu-8HVJT9Q4K&gm_ot92 zSWHvf9B~?cbRJhm1qFjcULc?za8HV9UDAg_BVcOo{RwcoY>0nbPf zJpuCfIejlhkuoLGGeUqEhHx)gtggqYQ>Xv(;b#9YyYKs(fA@#|m%HEob`x$s{B^Ov z|NP0U?Cqyd_U-PMhi+f(Cp_b`(~s=-YQTKRU5kY`^ah-+H?lcMre*{?-1- zDIY(*eNd%O_ta^z`}?o|xw(Jnzkb>G{l(Mj$}PxE``^EQTZ{BqsCqH1N5fAq#riDo`S;^m*pn0ICvT*C(M{!} zi}RE&S)5qCp2^Pb=E z*xB2&YA^S9`)~E`xAx^5hW1i4J3S8s6?uH(Zt_;|jAuI14`i_@n7UgO>Gtlq5JPO#V3<>gP0 zhL&;XneJr$%a5-sMXo>E>D-1F!r8eu^~>cV+@2(IB5Ixh4vXS`pHZc*}0)v?

RD8Gi_MimAE&i|1veVa;;Ia&&RtgnrE?LrEO6jh}YCgCkW8AQQW?9t5 z5}Qbf+?@m-y_aAukAV5I2s8hg-BL;zqq$C!qsG!grCwUgwO5JV!VQ0BUbOe@ER%VG zpXjN0ZoO7xmmT>$t!OD2d-g+;#!6C*317xqU9TZgsW<+!TfC3MVT0h2rw1u!AlRNG0IeHYF@=c?ZE^_VG#rzQG=3`)Tq)k zd}d0Tf=ZQnT)fVxbzd2NgGQgS4*@N0g)=kCoGij9UFRuirACUjY4eV9DGGqG=sMOWZygNDhccQVh=@pPaV#A!sn=5d2AUNSL#j2_ zk$M7b41^~k$hv)p&&WVOds%8m*geXqmH^K-YKT=zX#j5M!A*zWFKAn}8m$Ei>XEn~ z&MNt!4G^appm&Rj8>U52w7`-|qM95j0W7E!O{{ueLdU<5fj%{AQCu4si!Kc{M4M-A zIW4ISEu*65!@D$p<430?K8quSGD{K{5-lD;9Z5@dA`uMfSVuBRiFBapLmXRG=Lb7q zRzypTS*wpW=ZvZn25le(51Zm!SrJ`aPsPRPbHmc8nt|drFi7MIiqls_Q%g04P_hKg z-5b?fbHo6J#0aje5WC8#MASN(6pEArx7aY1n0k$tt4diBeU+ygqxhaZck`s$0$x(g zATuh%Wu5&Ci;I9&VNYHIYw#Fw;Lc#>F&>52F3%PY=c+Hg0M{)7`JhFh1>q&9okEy} z4~tdIMFgX1A9J_}FyN7EsBjK)L=T-VMkL}fJ*0|ohyZ|845f~{u z{FuDMTw*{fXfH`jGc?BwQ7CF7QR-Yw!)OVtUK63^4l^)Mq{Y`ZvN<%85`bbwhsVST zYLmIh3c%Gcbxc@yATJcT<(z7ptXmmOki}+com&Db;EN$6(BT-QsY)6cOdlOQukQRi zqT>Ca!vW-oj<_b~*q4!ns3WoHz0YoKqbxb*n6h9+1T+!3(a-@R!GIw@U8@jgCmp)4 zK8m3N*k_jJ)_^B%1G}xS3kH#aq7nu+aB7@^zSJ8NISxK{34U5#iR$YrQHw|J+7no& zQTLc^)F2qp9s;jP=4-871HJ_l0|t*c+8AV+#32YbN`jRqP)Pv&L^iA+sf-0O42bic zh%jAoCEk@)2{|VaST8J^IAE&-v{;(VpgO-1`DAHm_Dnv(1(-Q{j8hhX&E*lXdviGG zlNm{@F*lrolQAaUISnB927uaO)l3GCKr3cD^sJ>-PZEe-%GeMT5BdZx$EX6t_};tb z3ivz)a*l`#2IrtpYEw{!nzk}Yn{yly5~O7VeX+ zmJXq!Ax|BEo#sk4%`2M=HfxXFLE04M<`5$wG|lKnu)qu$&=ye1$c}1gjV_ z22F-^ItYdquVZNzf>nds++DEYb^-FpJwgH$G1H82xLyY)qo;MkkOlS8IeOiZTdvD4$44A2Fp&O$^jb% z60zh~wAM|ZB;defy%e4@WNI^y9;>k!RRph|;F1o50UeKIh96}u;5yb=_7hG(dEEG8^L?93I>g1QS6~ZL{tm%SMJ)aHC`4>A(WEbU^f6Ymj|V^q><+ZpTi{n6D8M&FRBOAv|b(vv;`ntGZtx`iUx)=+)`Hf}UP z#o)H-lQ7%t!1SPL(1S;PL7&N|q``$AH+_;J8=K(*rxY6M$pJS%M29=Yz;#_VePZ6G zJT{yGMOstOP}xebXmaIxZVSAf1ATgz6BT5Vj7}88EH9=@SJjWJSQZMncG- znTEjt=PItLfZS1^V9yjZS8>Nd=;A3sz2Xwkz+w>KdDAD^4OMglcgF<5#?Zm@I)>?n z=0E6d|Bk45Kj=X4LlWSw(y(YPGs*Ys+ z9Q6qls9-DFlpg5fz-Z&}qN3OYEwoLa%*#S+Q_bP3jAa++KtU@G++dn+*W@cveU;Ia zNx1pwydCxi2? usingle) (n:int) : usingle + let rec usum_rec (f : int -> usingle) (n:int) : usingle requires { 0 <= n } variant { n } ensures { abs (to_real result -. sum (real_fun f) 0 n) <=. sum (abs_real_fun f) 0 n *. (eps *. from_int n) } - = if n = 0 then u0 else usum_rec f (n-1) ++. f (n-1) + = if n = 0 then uzero else usum_rec f (n-1) ++. f (n-1) function exact_f : int -> real function f' : int -> real @@ -49,7 +49,7 @@ module SumSingle constant f_cst_err:real (* We use the propagation on sum to prove the postcondition *) - let ghost function example1 (f : int -> usingle) (n : int) : usingle + let function example1 (f : int -> usingle) (n : int) : usingle requires { 0 <= n } requires { forall i. abs (to_real (f i) -. exact_f i) <=. f' i *. f_rel_err } ensures { @@ -95,13 +95,13 @@ module SumDouble !s (* We use the propagation lemma on IEEE addition to prove the postcondition *) - let rec ghost usum_rec (f : int -> udouble) (n:int) : udouble + let rec usum_rec (f : int -> udouble) (n:int) : udouble requires { 0 <= n } variant { n } ensures { abs (to_real result -. sum (real_fun f) 0 n) <=. sum (abs_real_fun f) 0 n *. (eps *. from_int n) } - = if n = 0 then u0 else usum_rec f (n-1) ++. f (n-1) + = if n = 0 then uzero else usum_rec f (n-1) ++. f (n-1) function exact_f : int -> real function f' : int -> real @@ -110,7 +110,7 @@ module SumDouble constant f_cst_err:real (* We use the propagation on sum to prove the postcondition *) - let ghost function example1 (f : int -> udouble) (n : int) : udouble + let function example1 (f : int -> udouble) (n : int) : udouble requires { 0 <= n } requires { forall i. abs (to_real (f i) -. exact_f i) <=. f' i *. f_rel_err } ensures { diff --git a/examples/regtests.sh b/examples/regtests.sh index e40b575e1..17e20cc5f 100755 --- a/examples/regtests.sh +++ b/examples/regtests.sh @@ -94,6 +94,7 @@ run_dir verifythis_2016_matrix_multiplication "-L verifythis_2016_matrix_multipl run_dir WP_revisited "" run_dir prover "-L prover --warn-off=unused_variable" run_dir multiprecision "-L multiprecision" +run_dir numeric "" echo "" echo "Score on ported programs : $success/$total" diff --git a/examples/stdlib/ufloat/why3session.xml b/examples/stdlib/ufloat/why3session.xml index d36f9d349..0df63c2d9 100644 --- a/examples/stdlib/ufloat/why3session.xml +++ b/examples/stdlib/ufloat/why3session.xml @@ -2,12 +2,13 @@ - + - + + @@ -20,31 +21,33 @@ - + + - + - + - + - + - + - + + - + @@ -101,12 +104,12 @@ - + - + @@ -173,7 +176,7 @@ - + @@ -299,284 +302,299 @@ - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + + + + + + + + + + + + + + + + + - + - + - + - + - - + - + @@ -587,280 +605,279 @@ - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + diff --git a/examples/stdlib/ufloat/why3shapes.gz b/examples/stdlib/ufloat/why3shapes.gz dissimilarity index 99% index 7b78e70508a0ba02a29451435397d38b4ea8041c..56cec9b64299af992e7118172e241d505c449f05 100644 GIT binary patch literal 13561 zcwPbdGzQBbiwFP!00000|LuKQj~u(P=DU7Hzj;Q2B<{=L9>a~n2;G3-3k(MJDsc4( zIF=5yc%=L5=Zj?Sm04X?-K}c_*FLST$|Qrq*n?{`VK*xA5)rhc6}k9zNF(A3uFNuu#8z{(JlQZhSaz`29c1m(Pj4`Gb|^^Ut43 z;>VA_{lCxjnA78bdlSkZU;9?K_}asvr|s>xu=Vy^z}w&6gb=@m*KY>c2OnNdU-mpTB>~;eY@2e;w?5{D+pNR#MsvB9L}`(3^ZPJPFglQ8m5NPD=u zO#qiH$9uq8vVy1&dcOoKEb$4yW~wI}?AhymJk^mz+nKpO1rU&C+s)mz?1s0reVRObG#lcmSkzSl&s{P7>;3+Oj` z6CTshySVNF-K2a68C-M=aFZ_J#Wr;oO?v7qM|RW5(^H`qf(%g-YDrM>o_%vcVPtaxwe@7S=(-my4GL6e_iIjOyKg4CBfL_OCAx19K942UO0u#vl z@bT-1@*|{g1qlBo{N*6oLGptXjsD%ocj$<=w{sE-z9kV2)F2n_TkE_d9gF!LBO?Ta zni$g|(|zobx!*x%Pm%^)G>El8U=mNfAVE1s!h+@p;d>u_U#+83i#DP&7kh}roQ0$<3N^~DjLO3EQQIsYJlENT%Uj9Im zFr-#}I)j&!+|ax}f63*`hxGaHe}r!%1l}Mpg7D`{Aczjckj?!7(!Z~sfcTSD{?Ukl z-xa?;e_7b;ALHvLpB=QZ=>Y1_=DbfBW|i z+yv)U_ul|*2cz)wcIfuH`|rW_{Rl6@*RSQvH>B)OJB>Akei^yWoc>6zGs!!W>q&`p zAz4O{{Sdp5U;Od;>$mjzQ~tQYS*Vikk`w&ufFccV01u+Q>5}n-zCGD*oFO37P$Kx$EXB!nr^N7pboRe7^h)7*VJjs~d&TLTs zYWOBcTL!=S?L+zUWnr*>9+|M8OB2=!#fP7GykWwAj<1`{bkN48Jt#P-JploLnLZ4# zmS*wiTn>Lu$})EQIZES?As{~@a&0P)L1~Xf6CGBfPF_2H{8auG=Q0?S=iusc zr0MIR3OmrQm5agiH5ematFIeme)Z;>-at>L#?bLbK<`=uh_D9HR_N>zcuJ z&1c#6>fq_CCqvvnP@N|@xUL00_`%cWAF%^7ku%y0tcKv7g`!{cL;VyMBv(ieXW{8`aK`1Q@$;e17rG z9S_di;QV-SJ`K*FW$E+7;*L* zix#crkCm$}KmM4yz3jht|Mn^V1S4+rcs2AGyS{$2(|g$e>m3Rj^+3i5>am~)g}iJ| ze?Hmc^$=YicY3|*w~g&4fN?LB;Jn(K*6IFy$U9!Wd5|*aA=CS@hW^mu0t4DPFgal=a&u(z)B~6nmp?Qrp;^_1G&Dq^fh~uelN00})tZeT)?(j#|8XZZXkwZPkuo%&W{N18n_h})QQ+Dzr zynQnfe0;iGndL8LbvQp4@BU-Tia4^F{wqGeeG~qpZwoAG&+)+Tr)8eD0zCydi}h%} zc-8h^dxHP|`EPSPPhj6Qolo?*_eQ(Msztj4Bw%~|ZemB{ADVCpRrMF@LOy$eAcpA*=5T?RF}lz$Hbu=r;qLTh|`0jtrOAqPF$zP>%9}a zb?@=-dm7@vsqBKipO5|??@8;;d;HfmQt$EK9Gmxt*1f0Q{lm!3MMG@J#yNy~c#JLS z;15d&e@Hs`h$m+oyyx3iVczy2Hrft4yJWvOX1^HOFZO0HCicq%mG98v$DIALXTR(U z!eq~W-ipI!qj%+DV1KI@q(-_c7koW$B4_NMShJ7Zoc)|_@c%qoJv_`z0{YFLjiht( zIArlRV#jXH?CqPaS2J@q#%%PZ>oSSPPUqXPbJza$L+uyi3@-fjn=v0>w(i^AE{U+! z_QhlHcoYR*&|dP7`CedXoBmsk_e}AFta%WPV|70Xvk$P3=6pRI#E|r_+y`(l2Ys-^ z;?T-PY#0eXSqZ+YBCz|N?I$}yHi2rhh7J9}6VSR-=L8xKqs%sxL%+DWhwfa&yXoyU zY#=A09+ph|_i8D|%eS|K-nOr8s7=BlGSX`^xHJ*yIf0!;y=oj%)AHIPxLGeWb>3<& z8RAldATH2E@vJ7{I!qo(ht1gPwC;+_m2QpOV?Z@+5Tgcf!8lT3v8BV}S1R#<_t|PJ z&e3D>FRI95OOrWUhzVzx>hjRzEESrK_8i)LEiR9y#&*bjTBR3(^qGoyjNjv+HT@vH zItAuPvljs@-;7|NUAHIX&(`jt>1p*Q!2go^ja*}`;61Oue*A=P^sgG=bW2<1?|*#z z`Jp?&wrHO|(-txPYi1jD-BQ@J8P>P`OQ@JC{_RUPZ7+KCq=_CL)sNjCIDVlQD1b-t zwu9DA(ezNmYy3YZj<5I~0yRmjeSYze@a1Fp^z9~>^reKarN^f0(0~3&Fg{L?=1AiC zh$KF*k;J0~k}p1fTTt-(-vJ_o&+StWhQ2pIec$$S+&28&zak*R=|5oinP&D|=&P9j z^rd|L{`{)lcpL_LS7w;<|ch`N~w%E$qp2-3!0)B^m4M)3GW!2Q744yvcK zTqJMp2o8F6{r$V~BRwSGwzFex4ujaWZ|!JK8~=Vl;Qhz&F8uzrg#Yv9dl??yudx!W zVI|lcE5Qb=@TtwETgGA&R#TN6=(DHQ!vPC2@zb95R?+T8Cn`rdStd7jT5o!{8l9>B z?ziwIyn5BP%ki`|%H?-RxYe;ide^)G&Il}5FPtzSRISA*2HPUHMG*|^K~Q#4tZ zG_PoK63}|Oo3q-b!)jvNM3~jUEwtq2n?870kzgEc?6^{vvEypuBmTdhrT32$@n67& z`^O92ufg(CGj@BGvHaEZ>I3dyJm$2if2j)HUaPdXzsjrp8d16Z&tcqCS^I0W{`TT{ z4%>=qk1C96r)#-y=e0**ilcV=$Y~kp}hk4?=G61O3$On{M}a(5T(_wu;r2 ziPKlpOU6^dnhqMduF$*LKTOj!cvII|9{>uw@Vr(_vV?X$%i+xKU;GocFoa zOxW94ttp|kv~nGy{Yz?i`?S=V!FstGwNY#OKDR{;=f&%l05p12cIi%|JR-TAz<}dw z0w+)=lo|_X4+f+=GA>^oBdoebE48S}S=MXoc8^B4!QEe=@w#20p;uRC*p`F9YnitztR9K&|a1`vBg)jr0?R} zbm*bilm3f5Y#-L>FtkgPpsEWXDN0T^!N~!woHu^rWE$AHPQ&S}n1g zZwLn8#$R?|>1vMW8TFQKb&(xgXlZA8-axFxYk4R`ETxT`=}?29MXK2u2T*N!D0R9u zWt>@usUOBXA_O1r$|1yQ%C=ok@|xH(-L1mieVfwjcB2v(XCQrg!fg)j%qh|Om%DaK ziyNLESkn0Q0=lH@vQ~4c!+fd4Vx{o*eo5E+C0(~wVS}#Q4L9l9t@FKnxmxENqOjSE z$pP(UH!t7x$BTAb^w(e94m*Uep9bC*x-Wj&7|%s!K^)qd6jWIWmjgWhqC> zv}Q*QG~LK(3A+L-&(`|-J;d)qMx3cOzm&i_Pkw{c4W;dHk+_Lw&kn$C%xWvu#S=J z(g-zue++-l;QWyWJ|JPU=^RVi&YgY#v`W3C^zxL-D*SWHx661>%;LR{()UYBZ-#MO zl-_Q5E~VQF^cj~#ZFK$p^WUfymCDYcH7HbNI@~L=ZqZesw*A{_F>rRT%Ep~m>#F$E zR~#*lUiFxqJ^SNr?QN`X_t5Xh*qHSQW54Qp^TwtH_})xx5w&;aucsEnfLDxml5jKL zFX^}D`||B|^PcJ90DcmoW8s&rG+T~0AJ_q#@!5&0b?NCYI>lPsq4ur2knVPe{s*aO zkOk$b`@3R7UgI2Vzi2u1|ik!#hbV<(pJ#ubZ!pq6I4Q7*^JJx}--aK&jut{CD*|Dj| ztvFj*)$QX3mzdQJRF3TGY}l*De8{rSX?N1L9=*So3YS_}-=9d(!&O*XPB@KEPoZA58IsH~2FTxMyXSH4z6 zJvO#WqTcTjb=yi_LDWq^+eF}?17Q5}|xSic;#hulD-f}`~ z5HB~{JbKbAd}denoz~5N9-L=qGatc;+kbjVTj}+yO&G7Pfbr^Sru)x0^dK8gLA!nP zx{S77P1bdir7Pz!fg(`Gqn4UHi4u-GCJ{Wm0>|oTTWc?dOmV}4ZzJ% z>}R#T!}gTwaC*}B)1{A>MDQMZGRi4$UcAFP&GUq1$Etm-mO)wZ@*Brt$s^YqZVhV z+5-6gES8YgGq^(41`zWJujy@NcV&Ye57*ma#PQki1|ne&Zf>HjJ=o=*<&0(rs|ebH zTC;I_XlSw!Guzxb8shz?mNblKqa0zrz+hWn>CGCIQPqfE7pdCgiMXP{{X~OJExD8i z+dwvHFmL&nKn*|C@1H_FI6k|u!wri(wUe;fy&ZT{hYLIK`BS?W0UvwNQ`0{kT({Ky zYH{y}6Wd@#13M2z&+oMwwZlzJxb0Y&AKi@@6A2Ovp9V+x{qN0-&92P&Q}@2RdtvR! zTk99yaN$$`yT5qk(=N%+xP7EUq8@4Y2HvxqKW6i&N3-Z&c5evQ?B0)0iLEdlC*C7E zqIDsrM+96Vb3LXf88v(P>dm7^-82ln1Raz8)c|>c#9+5~25nt8hMq@P({y)DKD3f9 zP;rt(-;5X?TvxB?7Jo*?x29^|l+N|c{xE&_eC%KkZuAHQtLv^?_W}Ab%=JJ=L)@=q zW`ubmsPG!k(lY$|3xFNGq~D5u_tM+G0UY|1!JyBkw-{c&8*IlhYM#$flaEBr^MhA} zjHKUl)YJ?$HA78JsJ%z`_oE?bhOfO@WKhm-`p70H^X`keEO|>L#dX6V&f+w=E_xJb2R+Yew@1(+tEiGg#)`;?kUpy#BN6(fvZiCT?wd z^9#9kKjRi(aEmXf#y7cj+-3mPQJBvt%-`Lg;FjpQCDz;$1GmHsmH@Z@8h#tx>R@HN z!!qkX*6K-NNUpj+*4ll17sjJCbS{bh9_#dE+GSdRov&K{7|-7P*o(efhquc82DnsXae*{9O(1Q?(@e_|7hp1R*#0f>qq+&*kiMe z$Fpbjoj$Ibj*kg}S@)mgoI9-6FOUA1`~zlm2M(?No`ucr`SZIyk7BnE(Y>MF`4HQq zLmsC4W$)<*N^g4}zMHGy%f6QUVevST&~Ms=3st<=ihs3HhaG`mK+O{d`+_My){^Z| za0~ONFq{_-cfV&TH{ua^-cDnt2g4$TcikI1AEAFs&;9!O`l#D;jWC0(`k8IU#m_J^ zy33Z1T65MuI{J7!`?KzRxEZ6pqx&U!`y(Wr!zj@otl*~m4jaX}df)xiZ~{W_yFSy< zk{+`rx9llwxYfNhuY9C%|mTydHF#&NJe+toDN5}cVqv{9RHU&{!cK+|BBY^ z41wAbregtKWsf7po@u=IejmY^rQk@`-mOEHy_M^OZGD#Vbi38G2}2S|{V;Q2<{ zJ83QjnoY5iS*9>+Q(+yPQ&I`3AhorK8^!LVzmx7lxL!-8MXlhOmdq$tgBh;8pl`^P5D;H|!;1L0t5oaG6 zmC?~lupIp~cd8lzHmjl>Y^WwUXbFPvK>*#r8<#ZXM+7BvDc-@4XBd$LN76x%4*(I; zK{O>uU=1V?)}th5YLf5;Ua`;tQ4hoMmK$kwwl;w#762st5G1ig9<1^m9DNojF13hN zW~Zfx(ShbgXmkRS&cmyyo-)Rs1mZ9yD2ww7@RBOrSCgRvFgt>KGZE)B9G$Y|K{&~^ zGZEu^>%EIwSK*AvazUTdpn~94S_obgp;}!tgQ7&Plu&?Z?V3cVp(!D_g1hJNkI<(Y zva~+I?8RC_ket-qpo@C|j)QB^67pQ5gr(%X8keoq8LFlY@63fg4^)OF3$Q!Id)PZG zD+@YiW1TQwMd3S8>?}|cmdBZ7$b};$fk!aR76;SLF;7=Jlfuu11~r8!F-(t8N{LBt zas@jPpd>im4lzXl&w&;rn8qqhdjjntP?2Q^R|ZdGIje>2q}3My1ksq3vU;I8Y!kvU z1R5M3D@qr1Q8$j?dGW%R90il6V$f8bbnwLRp>Qnd4l>a!9LVDCEO=qHws1YL=Uhvv zlFY(a3%?+A$-eU)*7uFkPUFb?MrZctJ8#wFnD~C>jx2(wXO~Jn2@4xt!YTU=aibxGu!JO2Y>R zo?#(_$k8FV?C?>GF7OLAfDuI+gCGxXOK|X~YV!ZihpvlW_hPjc7ov7>U{LH_nDW-b zv#6Lo^t|h3HaZr;HG*3(9VRbC3-7F%^-^1_Rdk~3Xt(>qJgdMBthbR>!xlj}GXgaW zw_YVoCG~Z?-J$5BSZx?AHFz38Qp6bW>=8B_WbL~9QxG(Sp;U_55npg24J#nG1tMDc z0zU`=_6^7*x)}UVIHlp9EP~w}BLX2Moz!r9S|GJx2)LMf5fERLSP->mxOn3s(gMbo zF;}9EL3h%m@4UM6@|mvbEp{oHhyb3&47Jffn8nUH&?p_~ zu183jRfr56oB(Vgk&2WQ5VlEa5tz0fcGZhPFTg^Nln?9+GS}j>4_Z4Z5Q*m2i)Q3z zy*$jMMQ9FlKzRU1%!T+pb7TfVW!JHvBW!MTnD?YS)asBRq?F%a;3zYLo+y|jC@YA7 z$eXfE-giK1p<_wNu}mcW&@54CM5Zt>n^%PBdwB%A7{|cDbL}$_tO^2)bkZ^88eMS6 zDY`%InWObq=3HTc3;Y&`kVcc?A{1<>90|hps%J%H?kFel-1C}KfWXUu+!gdC58sH= zus!aL02uNMFNd6uA%V6WxwzCoxnQ;>-hjABMnF?ap8HPG!c;+(eBcPvG@^2_FxiyA z6S$tx39#sV0H>q|skgNY2=Jp4kOMLg3)4}Oq2LjLIKyXQ4;Af>r1%?Gv*KxvWP# zz!MS;H1Rok1i?j@0@C>AWw{g&F&wHCjg6){D`iALCY3W%#OMsg10$;><-QN$ln}p~ zfMgx|Q4zC(0EqAm*`4HJzeiS`1uZ8Ix8;y-mf&C-ghe(iG?>KU8%xt5Nx11VAr=vm z1T5r3ur&ql1?h6o96W>H%rG~KvV8T#tb*Mgj#;lBq0orC>UXrd0}Ul{gb3gTsY)khSIjFQy?@$Ucx+1-RG37+6Kf znMEfh5rx=7AqQ+DIiX+;g?yzra?*V#cia)#ET?r4m_HbI9bvP$jW#2Oua+YkF~HKW z&CakR1v!L9@EkLzg-MTKjTZrm1kJ<^C;n>8Tmy(EAbuMVvj%n~Q=VR3DcZuh5o>Ei znBkiGX!S6h3JYA}pDNi+jm{u2d_Ekc$*H%P8kErVTb~6}Xdg48dZaT2VV$NmD+9zr zMH1mG?>OB3xRY=U?1G8WGiVW`l`D}U*n%fxOUzJeWUP1GQ5@_@f~--9^dUwHVu|#D zm*T5us>{j{^tU7lyfO2n3Ewd-y zRc6q2mV2=73eXk7NDlPJ00bfmD6dHj5gM%|GFtuXLHjG%#{vR&1h@iGJ_3}AY|;uzD{G>C08XhF{1UQwh+T!Lj@#ziT9R(K2PGW=bT5K)Fh+=$qz&33S4OVJd7;fIk3>-32qde50lMd1 z2VD?RDaf1fv`Ec7gV&MOniOF}ZI=ym$|Jluh2;p(=vq{PBGAfFFe1G3;fjjnpN9;mfFv#yl$dQY@qju97$* zK=LxCj=9jc9=N@VDAB}XYehtfjKe1;5Q8L*pdMa1!*TZ8CT*DWc~}sLRL+ncOBPZU zC1ewX2q3#pv0vC0*Fc7hff}>}MnM*>v(O@UbwYybG4Xz*<~rb@1iWd6B9p8|(76Q3 zZGh;}qG7yQEANHyT?iaO38G2|dk`hENtUA!Fl)t|KEY{A^jDAJQ=&Cqr2moW>X;0s zD4yZEJe;>`OAdYC$BdJi&&4~KX$=d6_$b2l1_d>s)x*TvIO0jha@BLVuYx#9K-(gP zIPflxY2(!1uW*^Nf>QV25XTHO9!nKfs?4fFUSUqoed9kBKFh>lSf+~Oof=4E-6a# zgrdQd7s1p4E)~YlI)>;!X)aTyts{@LsDgN%U*Q@*>MVG+SY9;pN^1gi0vtfN0*VIw zk3p6?hH`TeOi2YZlo3HBG+9o{gR@Ui35#e2jO_OR37B6_E&>S+lglHm=xM|biH`Sq zgFYe*cy(~JT8LOYU);`Jh|^AZsN0@vVAGIR$fGg;Umkc?Z(m`GTnfRP19 zq2u9UrtZK+QVRoxtj$Rz%rNEEQIP`z8^k?Iwt#_(CIml!{!+pegoJo8#*nMDiYcXv zjMdQsSI1m&1>B6hiYMe~f`Wcw=!{-Y@W>p=vEny^YG@>YiQ~=z#sUdRf*0hj=9;K4 zqd-f;12VbKkTn5rv+BIhfYT{bPeHN`U6rPGYwhl^|!ft4<>G9Ct|)Jlu# zjz_1_M4E@0y$?GIutdOoCMBv-+QXYlL@7!j{X=5X7)}gw7r_nD8=pdqx(Fzdjanh* zs>pXZuSLp^=~Os%1#C-|FwP*Z^-{rFYMZ$WxzM^{R8(}P01P%B`mhZ^XvSfvk?lH_ zk&7aTj~1rPFbJe)BlD@WN$Q3a)lLyYJ1~*WA-f2y+wrOuLV%AP&Lf0sWh=<&;9Lkd zL;ql}kdO=HavY|~dtYJGxFqY*Ek+1MFzrQfZ3Z`dw`c&^u)NF(6%qWTkc081gG;4S z7s7?1NEw-Cu-U?CS!HSUJbG!Ebcik+Tz@fKxYPtsz^(R3Tw=76cAi0OWSlx9_G?UM zJ@CsBN49T^!?)yU`-sC)B1LdoAxT8wq#L1iKgMOSc@13|9(_d%S!_0KC2gYq}XT<=6jA-9iYVL`wmLe8vD-ep6zc_6lw zB|suO3TqHT_cliPhSUj|4o24)Ehr}!Ft<9=u4IIfL1LeEi%PV(7%tKxBQy6bP@$ag z;8{gBDUm}Xk<{)+7yvW?sP$3O$&guF_LAiA|Yy~Z2)dXE{VfkjP+FZ30wE~Ut*B2J+yBsKz(ddvvwRl(nuW6xp?pykAQZ&C zK^x$T7%3^&ZOjV`Mj7-o?ong;U=g~Ym4qi29{;(DJSS4|i>W$}bFuvDF>C-(C{>Q| zRnT8#0W}9mibVRELv8aB%lSNFJP#vE^+Ygz!YK})g>b%PH1p9Rqv{0I0-lwR8pmab z0gQB|+X$WZL_(P*%Rwiwt|f$4Kgn1zW%&A10wVfK%L15OE(j@9)X4qdh`hU#l#p0= zo{%|Ma1It1hA4!?ufbPZ+7)w#a@vk54t*V9IUw#JaCRs$Z8@wsdo%~ebL8ak(AiN9 zqAsykiaP1RpoRufXDcoV6V4TcKXN*fU{oO+@WO(;+tcqz{j zG{7MiB+oDr1`aF)AE!A!<*0}!VR?}2z&SeEtwtb1O;rg*mm+nwLNF)zF;6(Eqk|%d zh8*%L3xVgl@?=tW#VHl?OnPW^_XHy<0ZBn}E`t*lLsyRoBPH+Q#9&oFXSS~Cb1A~5&^s&1m1_ece(6d3d)>t`4l zAvVGzTa^*nlP8ZXNT?Jh%#e>Zm*LGbjGUZA`bSGVIV#%Aa8wc^WJNe7EfN4S?8xT( z;dM{?=U_az4Sh<^Q@tlGZF7YTI%Pz7h56DEK{EPbPdqZFO;riTC7n$aT+*I$Mqp}L z;U)MsGJl4Vv)0uxZSY=EaY%(vq#(-)#%!g9*UqnsXBuAWppv)6Cm|wS2I4-iy^V#I zU~9j~0)Npkc!D$EuxTGE5klr_y-Z7G@Pm15(grjSRGz zgdiFJQ%D#Y zRDi~#sh3r&2vwOWQp59tP$7bX*4d2AvM@NPbXm1ZKyr)3$sj2J2dL}|p&}Oun<7~w ze_geTbP!(ckaEC(S1u3~A)}$yz$(3}r4jn#k`fM$p*=3|8EiIvg0DhEkb~sGBE4u} zuc=n?v{&L&jHH3a)#?y9GM6a2Q$mOy^ra;wnt`%XBfe)PIyy0@b7rvwxEN)0?!jII zx>Rp7T#`s$Y6k8b7lVhGY4~pzV-Nb8dJnEV2SGzBTp|$gG6iHjwCPqE64f5-tEyEp z^u6kkDtFaWVR)#3tyu=?t1V?B$ko*0uAVpPH&W5AdiAa zxxT^#Qd+r^n*QpSU@1fl;e&z6_ptjSKdQn+QcbW=zSLThgpfo;;W9uF={&i5bcKnc zFq0v;M0lU+Xp~MRU_h`S(G3MpQDFiDP2i9%(@CEy3ax@vc%4j}dWt_)g$ejt$>MPl zrQ;FCG%_URA<`i!-Pf2uQN@Q)FwT-f@nEUcLn&!|q}o(E92n(OSD17M{SmIH0>4ZL z^EI+xqf*d{4vX{0RG0`;GF%?x(5@I@d!ZsJ!eAoCbv%&G=0_DKh#3o`rR`!ufFp*f zW>F;=GFA}r#Y-woU?RMc&S$vr;1Jq+g9xf3yhA8ve7(5B#Ka_Y_C+Zq4phbpMroxj zt(KRnucxUz(}!KVG=mpWv)<0(tN3?v=gas@YQAj*e@5_ zsf6&ddPOVi9H20r3h5AFiKUX<>e4k8CQxled<79UZMGw0p{-n|MRrU%x>n}O3X_EJ z1Gyub86HGL6z1uaxb#v8SCqe|!o&m$gCY`D##u1keI;;Sh?qixXsfF$Of(NHOM*t_ z0v2DO|InR`&=j4)V7Xgif&d?RG9@P-kv^B6Di)|V6h6IZt*)ss(OyeLS%|=Ex3Njb z6s@2lV-J(y)U_2R8ul~>;U%3;Wz}*pBQp`GegW8~$5fb5T^wG}2ZRDM~}! zAIQ~O>Cz@}I62!B=K2Z~FW`-<$_^F{*1<|gRR?ffR?3_udvt|~kCE<55h@z0$_j}V zVdykJWT%RN3FrqaOhTozONM-YOp5LiQWc4ThnEy7X?snDiKMG#L_{EK9pZtkL0a9N zkmm)#V7|7(q&T2RD{Iy}cnCw+`oIZATK3S^ktmz9DonH}bWVgL0fiVj*q$1p%E}}g zl@8_F3KJKRt0G{8mI)K_kJ1t$Zd)(m**vDgBq5+iCa$Fqnr;PvKq25w6$xWvFyEN` z`4uLnD`5*%>&$bg5FUihbZtWM(IeA&Y=wywbS4|Ni!Q>V;#)_{F^&qW9HIxH0VhQgB zTdH#sPE>@!NJkN^z@gdtR23%7RH~Yfl{Nz4A%b!OQM*#X=C0uS2`fxOh6vNSWN!_J zKk`UcjDo}pj0d*0oiOTj?(UMIAbXG6GaDBJFcLX@v=^V0N&Gouh}P zPF!1vI0uQvx=%+r}nh99*}H?wA3TdwSuK8 zgsvKffjf=FE2ihEFhSrHkn{^M(nJwT4&5G#qBGYuS~|4n6x}Sw+se|@SC~)%uuncSmkibS(bYs6{@%wF ztY`-i+xGvHR$3SsFs*4_Uho2a)HcTCk~BVPY4W($Psfg)wz`B-`7w-v@?=G`7gX6w zMHdC>pPaV(pL}FkvnkmXjrJ!W9pR3k^$xmqD$s#)2j=q-DEuoTileRmC&vIoBfda#?|Jk{oM@|1 z(~&a+F@QZg+UkFD3=lo*OxM2v0ST)anaM~AMUGH60}uD)TmAnZD>z-Tx$OV|!37#3 literal 13223 zcwPagGg!(ab!eZRmGj1>0)I@xS5;VZGP2%dwuuq|Ajxwx4VBYU%!3&^7((< znY-8j{Z;raeE;(CYYD%HFZJW6&)@ef)URLu**<Bs=02>y3s#wjzmL8jUwf#LVfoX)Q*@x;fF?S|t~Y7jLb}TN4l|_aX6Qy+z>9V6 z%$oGvnfL6*p2w#`%@i4`B-EUt;*oyH&;|I1pGoV9Dt-F==eKF(Y){Z;j(W?qqzNasr^QRTb!jyDZ zoZwf76lHirxEJkBSB&rV{YkjPFj3Uc;YOkKAWbNHJ~UPX?t%ZaS3MkYXRmwiJRd2? z{mm_BofK&EftIN|C$}^(kw6Y~k~6!X_@MsP@J$|k8RF{qkLByvnZx>dBJw88@+^HzsGk9&LbuAiRl>6tg0slYQ0 zt_|fWByF*1IO9TLX+pmzc!LEoRyFYVYZ*Cr8{rP+cV0yRHR3_`%f= z;h}wO{@ad>1%%&>IA)=cXxvCZ7(F}_b9C)dPoG$cPm}n22FDF_^<8d6`G*BU-CCPA z*-v-|INRR%4sNziF-*#Lz1j(pKx1ct&(FTO-$5>WHp9@O#*%QrynS~u*a>w!1$Kma;LC!h zQ326(p(-~cJc;Kt_)^K*>kWv7T5SsBL|+Z;0C3#;eh5h|6}Uod6Tlh%N#lopdUc-A z@g|Bc_mRVXjA1gOOZmG=z3$UYFURWSM|l5kWccCfd}fxvn(V{*IeYgXV^zda&GcXK z`Te`_AAMU;No$UK{xDASv>E6z!I{lR^VzGm_S!T2_b>mL(s_dVuIY53$IvV7ny6;& z_RxU!{=0!4^}lb*y(b=!^bVuuB&ONW9dp0$#i5Bd~6#-EH zk$>#gLOxzR`inZ4C?0q6eu_AA=D)33m=4IzC2UVRj zhaWSCYMef|-(pUWik419TRU-`886pP@YX%z-$&|V&uQBQdz|+Ei1%dm<`MsOjnpIl zn^N<*Z{R)e9?latRSmJC8<#NZd>?Dt!Ov?4Kc^l1KqqG_vghkwVcK>tR@x3WI~Tt= z7QZ-%Uu=zDjN+Gj+P*`RA5-zmUi`A#5GH%^^R_u`(tEc(4B~J51*wtlwhO+UHjxwY zkD}QoZYqAxR^)#fug-Tf(SUyOXQk*IBMy1|mE5tLGkgDT?bXDc9db7M(t(Vsu>pL4 z0PfnqJ=cEL&k(}jzB|<8^VWU4`#BTV+P-=U9Z%xGD_TqbFCWjUwV#P`D(M#}66M^6Fd_VaK@(HvzYgo`9 zA_2`ibwQxfaM0OCa_A>Fx5%BUcsIPQh7IMY)Wei%|6a}2c>eZ&u-o>vb+yVkWJY@F z2InpUkR#ej)~gO(YMNe~B{$27rY>4dHA7tM5X2RhC|=Yh+(yY0`LLQ>owi+Zz0oac zdkU&%4dP(IYdDTfSghHw_?1RH(0#EPi%aZS{1-K3v1ZAf&D4amYi)UexX6Siy}g7r z-%87qxv`!ypEl`PB7LDD9@FXyJoyX0)KA^&H-4c##*RnvzQfbb&-D1hTl_yJj<5I~0yRmjeSY=t;p?aH z`TJci>1zq!N>4`z(0~3!I6jS!rsU!IfjoR3$-|c!d9OZwpK#FWvL@kidsidZ6eFjpnz|?^*uK*YfSp-@pImPn3iuhcEQ%OF#C1J7VrYLR^p# zH%N%uzEVPMcUPl+5oD9_a6=)=^-Jvoxf^h7?iAiYe#Te z{|^HJkDtPa@cXwC{_od6%kc1FNtIxYD#4~y2{urLPi-vSbQK$^8h68iKU>y29Hbyu zKCVr#ZO&Z*qHQN9x5FKPmW$hMFV48n?ziwYym`}>#qqQ?%H?@%FR@ z#Dto|mY(V6zP3Q}N4FPfu{HHgPvdetQ;_+~0c4ABZ|2ON@~{!SDv{~Vy;bhd_bMI_ zWQ*Jd!(N{l*pFe~(mJBaDc6q(1ONEFkd}S<`Vk8ENBBn=_d-s^)B1eVkp4K@#niv} zxwZwWJ#29O5Z?@1+kg(^TNUG`)KBqbxpjHLlaq*+!(AQKCLb09TW7*#uiMN@Ucc*; zgar!@y&V7-#&Q5$4E#XO80B1yw;7~-{dTR^|<=P`WN>(F5X{j zLie{C?ftKcD!)cm?*DTH_gvoo7OTI%I$t@%94)cN}#qkz|siid7Tww>Zfne2N)X#4d>*QglG z>T{Gq{XPdFSL6XWHTkC7Jss3*_r1+lb=$$|tLZi4xp0jKid?s$yZJv1(=>eJ7V~!A zsJ(WCs_S9RA@0XRuYA=R?%8m2%HlciYpaQ}x4v3aB5UsDIzs!G)bRd!xii7_deLj+ z*7$wuiyFL#buZ12r{ zU$$=dWpoSK{Y4pX+eI0AaW#f*bvY`}eYY8dCJEkjOZ(k={^T|vHoyA?Mf`7Mqz!P^ zJD*KO_AK8ZwEOle9l(t2`Sv9?`)cO=oqZb*H}rPWf06t3L)m;721pyleQb+;BTZ_s zai@^%B&o&=LK= zh=qF14_}D6wsA8aUJx`%H95-wuFVghj<=&6M%Gd4hdz%O!4G%h5aBdr+pZybOJW)C zP~q;O4e4#WIf;u4h(0~wHU@X$kZAtP-8!V%O-^T~G=9B;&iOjulR39xJ~v{qFnIeg z=j+3quj{6;!q@eNt9pgKv%8 zSHG-}m*v%AGN{ejwprR~ecC-CF&;e}pvJ?-Gi38~$wz07=ZAV1ogSt*CpUUsV3sE^ zO)faNfVlh1#(RGu^Cs4ET4sGgGR?&nWy$M*jiaSw8TEQmMv-1!LixNpS{=uf2QM?G z1r=NOSBmZcEZq|2*9S`1N_E#C^&ggl+Y3WC@*EAQT`NR4#n8P}LsBi;8CBO^*u{p= z;+WXw!Aq&>)|)A*b4^;3c_8e1VrHwzQXV+dnjJOJbT?NYLGC+2Q~DC-zOLn4}fYYqE%vsU*rI6XEQ z+utw!dAkzr$eUAcHd1@+%NOrYM!nl`9TVA=5o-MY6!}~r`6CNFqhXWb9BbOf-F*MD zMm^{B{4~lU{d4oT^L$TC^1Y7J4|7hhrg3YWUT=6Qr`rtl1(!jsfd2mFAJmGr#7?m_ zEVP?+xIbjsqT6ZO)^Eqjz{&k7D|c5dcfX&$%4l}Ps;A`Q(H}2suTyouMSkDM%BT-G zws%*r-pn*Z-@A!5ruL!y?bu@I@P^(_GHxRKIscY&pTE6r+!H$-(2pu~to*WV!Ip;` z4(ve9;n|7Z>C)4kbBeXL!ydQp;<@_`{_mxtPG+1Z@bf(Y>|voZbW>dqe-V*wN{&#O z**3H3rn6z6nV!PV_nPquzf8L`?-5TQCu5wuGkX#K4Z^mBHoZA;DZClC*Dsc)H+sRM z+5YycW)EIWj~0x4IK#+?Ek>^2xp*ZbH!f~mW8{V-5WOc5=fi;5hyybVIBFyoesgtO z`!$a9n2aOODW-1l>JHEOPH{A{4R)=$&+DnV&VM!sB=%~U0#^D!(Ba_;TK3BBmD(%U z8V{Gq~R&w17< z?@s#GqxZLR;aczN`;!NHxbjNNk*34bQ{?Qm-fOYfrnMf7LCd{XO9wm3WUr~oQW}Kf zl70ZX^sxkNM=Tc-+`JhfoSowDUM%cZ^C|4i&1yU0pXl0{M?8I;jCQ_Cy5h!H@NW>d zEyhWIE8?8-Uacb1Q%&eeSseAa&eOiEel3`K>}=;ueb{2^x|h6xsjGReuXX#47H_*d*%s3becQtYZS2xZXCk_^$AKSRiUfF^thm~ zH+Z^Ue|h%isbL|wc-e7YDr&@SXKBA&=#uiX;t{>as|jwh7A zes?KJZ|Artv}}41B551!*kxS7pe5Q%`hHkM+r81(_1Y(b5cGVG)aZlubnOA99`SUN zbN0ohS-Z>$Pd6|xbaXE2t~b7TevtYSft!%nk7|8|?K#ci^q?QcL9gd(R}6X`!KH(y zW6|VR@M|U6!_z~3xNJf1mI+_qepUpp!Sycg&Di4ndfOcN_9*6}SA+CiBg)ZSfur z@qX1T8pV@djwqi}VAqY4Xj_spp6La@t}4@>&cp=|9!4IlTFJFMSVywTgEb{hU%qup z_T}4(sp08CQI{>~-O|+h_A^skgPWTgwYb34X2`ckF~_tV!40N1pqLJL$!{yWs~PO! zaJ?ORJUkoTKqbuHOI+9f$Ok4gfP{WV)&(ERm9iLpx;f6_` z+G$vKKL?)G;bIPa{@iXvz{egbHA1Uydiza(r-u_uB%&dirktl+9`JVkim~4fzwx8H z;bI(EV&U@;-v0b&i%s1X7=P*BbayE%19NNls_Q6x?tk~!hJ4;+;mNy0x{m9SovzS2 zxxHgTd!10;J?@?nmdV{6pA%b9hha9d{&EdP6Xp!v-9p6%%O{WDyt}E7RWt1+f6Tf! z1I}5;gBLyOt^uudI?Zy%VQsoz*a%%@;v^}nInc6q-M&FL`?Dp!HC5B5biQWtC)~T| z2LQWw2hU8nI&j^<2kgf60ORa(bw22>q~`Gmv#!@~(_ ziC$V_DJ?NbOH6PHNbB$6w;>!3{PxDGpa1|8-j>t`p-~4im-nR}$X$hkDu{kp4Nm z?3|bF-;!(Ve%TLGX}|8b51*&xL=Cs9ephN!FMucXdi2-e&-mqEP2ezJ{0kU=!i`)p zZ`(25WhzFfHjSq$r*1PVFo%YbbrRRS6e0dP+rFxiPR{h9U zv$Yo(8Qo|~2XQ%TA02(XpZsxeKHQto-qG!Yy!|N(&f&4>&lYggeTM_%Ts?OGG@3xr zV+S*KE$IQ9Jm~k849ZTU8(@j<RpTl#1U>2QJ7JTs2_}c#- za-i;tSa5Ax@;1HftmdTlF9A>KfP8?<=0sJ%NFq<)SU7>DO zNM8bPK<@Xt1)1HtDS(H6N2+K5XUadx&9tqh-Q zLv#4&+R)_VSv)9_Hru=kkxPl%H^#tRh>;s9RJ1M{?+R1pPVMAQ?D&qoVj?MPJgY{T zWUN(AIvzu|f*EdDyz@J^vpciXJ%CH1YVHHD@mv(pN|v>dCYw|pvv*wWxZH8H<~z=2 zup#isIgl5{mY$K56pUS+LD@Ti4PqC}>+DylG1O>|b-JE3+0+!1H+XzrNvi3^>5R-p#XxbaGw zkg~6g-wC%9b|=hE==0c&)InF6mvto-Wwke6WDllr8I!7alI?`Q6kDjZ@RYOwuaXzZ z2@c6hCpARHqr8)1C;7#+2`{A7(UhQ+;-#wOqhLOxrnM%5HmH-l6k9Q1xu{8^Dz3s9 ztCY~DBwwl%#g#j0chc;nz8GO;3W{n%PR_?Ds^cYA7QHWm!vyZ6-${1`!X&ayR>Tau z39Lks@f%8BEAuQCeW&ZT&34M~l-nu0Q)Z|1PN`Q_ z8ylQAQDq}-VU-u=7*tTCqCJ!uP+IP^*l9ik6fW14Y^*_=q(oqv^USzHYEp9L;ZB1e zdZ*PAFfb+x*Caa;y#?2mf&btNE}(!1cgF9md?i(8P8(mj%StQmb#c(_oE2K-obL>n zqjp9Ra>EI~Vbq28)QfdSv6O0t)`kdO$rzKeOa$q`PuGF#QyAbJ6i`5jfinn5m83lj z$yG0{u&Kjf&LEKjqKMJ5m{P9MfUTxDu3V^@Lq;7EdmazO13*tI4>))Z1rG!O2NGunR6PCPTBGxoaEY>i2l9x-bJmea7JV~4Eo9sK_#s93}*_oYg{p(uyk(f@w@jS-sF4z6n`c4u%J&qI5wQb!Xkq`B%PV zgji`1YYWmUiBOBc!Vp*h4mNe8fTz_v3t3pLEkY0cIoDFEB(w0EJWdo)WkjD&XPoUoy7r`A z(9Be=imZsDk@F{=d9KQnZFTM0*j@))f(!^<(g7o4VBi@ZGKd_J*_nh{xC{`N=PYsy{ zuoO84B720-23tFDa|(loGL&is*unxwn$8N?Z9#}uz90@lfnA5>DIf;_6HaM_CtH2Z zF(MJ_5>A9YE%+U3VWe3c6+kE@BF%#tq2lmRX#r=;m@Co7ph-Kt*m=J5>{T{8Y6MM( zn3-4!+QKM&00V?65~@Ls?arH>*E_FvUXHNI6$cgZD0wIk;Kh^-7f1P0&?brw*6+L< zK@?P!F<%4AnMX=KK%U`}mCT`>jK+;3ehCKcODb8UIMH(#kZ@Z>v6vZyfmNq4cBGpO z`6iREN)Ze-kB1v}DN!nn6g9(QG>B!fiwj*Jgt~)3Il(Hl1+h&~GA|=Im;y33DJ^o+ z2B8*ENU`Bmg6AnhazW-=eD*A_HtAef~(?>CuTVBY!jQ$8RN9(Q3xx)Dtge(sIj3y&GpxV;% zzz{ALkQGU}qjCU6Ca*aK=(-FAtYU$Jd&d;ss6B>8?hDmLfb(#i9GNGt8hioC1*0wT zj-yWGC=@vrzCBR1@KUfMA2>2Jjf5N`Og1IR1W_lD@^ap}e@=xA%4Vx(7!X1w#1>F= zSa^++4CRf;!J*VP)zo1S=dd6PgX}P7EjiV+g(KTX#t4?^7*XRA(**s%x>0&~74IzUDAzkAmpd-iGmFY2^+hUxdObm*xzEWX|1G){u*SCl%TfEE z5jadK8XHY@R?3K6Oe$xjh|w8J1rDM@-4B;`23tbvYJ!2fNMDhzf&obG4Edep;kpl^ zx(HiN91+W*(k#KjH3*AB7)3u=gs@ne1xcb!T!^uVkR))S6oRiQ@PDY3gXWMKLS}}$ zQ9z~mGm8qggW5~LKO&h#utVNZg2#Z6Rv_o<0uqlkn$a0zjf%}7V*AYI8+h{Y=_i8y35ls_6b`=08LpX+=I8NLc;JfoRLO5@0K;b^ z<|9CwoO+L`!3j;j#YH%U_Aw)&M#7ruthK9;cD&WV(S;v#Ay&nF7bHEL9c&573iMm~ zh&o0k6x@x`mQedEhK@u)A=k|%BFISTkQ6&))e@r8HYwGk6*r(p${4JLpN)w@C~>*O*jg_9-D!0(JEwiBdXW zL3M=lr>H#Ot4hO+y+C;eH<2Sl_eBTfepc#ankPfqdJRsIXeuV4Bm@fz0x*&QtqjTt zWH5014JWwiX-S1&j8_62RhRUsI;7}`4;kv}HL8MWl+O*Xx*D&DP)dXnMazUH@#MAB z@SZXxh03u-8n3U$TRn%xB86ZmgNqOr&K$nNJA`1EQ|g4vz3Gvwo0tNUH9RJSm8y@X zM8%xu$drXaaja6mV$!;~Muxx?bo59#OVpwuK~gCcfhshp>iY@y8!#g|L!AXyqf$UB zU6Aj@pffG9AaydfU!%DVIhCu3MTpKKL4$)q^2vNeXsrdAPr6$g@0IvbAtANYG{-1i z&I-=nXfkVQosNAD-e%`-?n6n*;F6JmCMqqn<;9{pbuoMBPi=EOJ?vBZL477=K^;}m z8=PG788s}jj*R@>W!ADp|15oFB`iZ3sF3ubj7PPB%#U2Gg>T5dP1_7G&(R+eI}bIG z+0kSYr&(_3u_raCDRuMjf+k+Pzhx{*C}liSh%SRfJa&l4(s*XzKkfwAJH$P7APztY z!BrQOew6(Nohqlb#fY+)7b8_yZb4J=9ufKq#zxC>FnEO!BN{%W@7Lf&Oj8ckGHrFW@PR0SVh~7> zLx7^`F0KeJ@WU^{=Xf^OSONW~APINpIFU?6O_I5b(1OeBa2B{9O-o@xAzL;|!|!K9 zGo37g#dksg8Ep>XW(J6&MKd_>V3V*Y)liet&V~pPGnkIp6ehQghy^}wtAZv3CXt-e z775{zwkK2p$r~T!Nr7(R6R;U|zwc(~{$BSYGIix}@ zh*A~Nrew~LxHrK9A9okyOfm5SD@rOsXN;wZ?n)snNR&Xnn?VQRSL0QPxzWTT8LO~- z$R;|GT`bO;V2gl&fsi)bh&7>biCP2+8M3nouaAmH_?VD!30Yj+6td_wZ4D<^!WD*c z*4N@n-iC5l)Zg0XZEw3;~ zT6WcxH6piH48MaMFc8X3!a2FdCi>-oqmo$(iwrARc6oS6_{nNv3EKIeVv)k{Skys)HucVV5Q6 zhSyw;S20Tbd_{$ipo5U3a*3p+91Q2RHla(~Bfp+-WMZDjl58kQjEi&7CYq&z<)vV9 zx415p==-=5H|j6V92FuVA$_+9Be`nYq*&43H{9$d+zzFru^Qzp{DY$zbWR@JloDy% znCPv6-`qhe2nUo|MZ_`KoHxd#9JNUj=AxVbR`i@8$%mL8+Qe#(;rP1EChD38a0wsADq$ zGGIicK=Kk3JRv2Y-Jmt#wQ9s^*@!!XR|i_tDF#`ErMQ3&iqjC1C>l|>b_4HzZor*1 zM_IyXgQhNtA#aXIZe@x{<7rJ;SRk~7$e%@4wJIDBO>{AGCoNStCc<1{4M_Dmr)yOI zL!W`q&>mNI5q`LWY#d^Y&PWC;IAMdMLdQ`8%xc3=`*{Ip^ppDXoC2A%HiGlWkTfbp zV>og~$z$be9E-cT4|EY}THh*W98}Fhij+zy6Oq8DmZ2EG7|-qfNy-6`U9hZuji{)| z!5Ww;Ei;5RS0pU(S@xuUd}J6FG~bAVq*ywSS}d^$$AwBFw}Q}$XX#5IIf{}t`tTAs zQV-g|>Sz*PG0T{|6COaG_Ic}z5F!;OU*`@MwUSnB1%-jMiKTE?ISJy@Pabx3=b;d>B5g6_6^c0D~?kJXxD1Y!rJL!uyK7cvE; z?WKww+O8AffWz@;>M_~O>D+>Gfq6|upiYQl(00$DAa)$%v-T=bTW8Lz4}$irD}^*& z(<-A2K6BYAp@Y&n`Ha1yU_+m%3b?fz_HCrrweo;u9x5rqL3+ z(mdLTk`ht?izv#Fp~BJv{0zKzOd|#Mxnz!q$o)|{rhud$gGTvG+nf-*69O$%j%H{T z1$rjo#8YLQIh5G2e>i#CbBCIW>npbnSY+P{As68(Am3sI6|3?*z?n$}O}}c}fYeSP z>ktv%$S~9GA3`o_;U+m0+FiG8z+?umqp3*G!3duU%R#sPZBeVW#l}P3Px>_a2d_2kw}7q?$O?|ZJ;P?Or_vtEeGws zW|e7wzI4gMr}e0BS$MB>G{`A|3bH8UjS!hB)T2l}m@0nY^DWy3fDw6_35*V6d9M{B zIR=0V1Z2DDCk(lD+kit+2~3fuS!jcs=r()VC{TPLs;RMyo3{-Z<1}oTxuksY)v^TF zqax}mmtt+s^U|e$cw1MIlE;)7a%N|};B-#4luQ$S{!Y>oQ@_-YG=cU;dxjz$2?9)v zX40jk{SmN+fW|ZnGA{MYVma+Gf{EAStfb>;C@x*J2zN4vYnS>x4O$zTRF6tAM`t0r zBNIL(Sh~JtsXtca&1jq~N^2e@yfjL5T8)B(gn({c>K8FFL|9vRlHGw6xO&A@2-Pq| zdwuItztv7l#bZWskxNF3nxmj2Dvl-8hvn9#ep(4++9;Y1d(ldh32ULoaFFBD9&n$PM~9iMrUta>JLf*Eps%J2705fsKE+{pR*9He8N(Hi4vuD z5s1j52>h}TVJaAaM?xOMla~5{IitLm@NWpjC}oN_g`-a9I@xH$Q+?(QqnH}XIkplfmaPX%2o@S1GDHz zI>S}cG|A(ibE!YF(rth>;GR~T&WS0FbS?!$8#wuMFZCC?1Rx}fP>0fs&iY1ebupS0&$ z*=v^i5trbgdF9|KvM`fOr8CjhY7?Zarxy&@mimiRrXYu|y0B`!LsFf5bHy*g)-G3x|%ADz!zx}szVc5Ke2wrvOJPu!D6ULH<2N-Yz6I|2;I5v+V3U5cB#L3 zQ8@BL%eY1|Taqm{NYpSQanvmif|RRE{XDrO67B0$h&yyyMU0X(4ubJWFRxwdN6;0S zP85VHX;*q=G9ZzchR*kTebZ7uof1saRU|ZUfCYg887e%WMW%*=K;OF5pJ*$bViGAw zr1a5JC`&;V6karhTbBB>36=I%7VZ+0z@JgJO86%M&lkYY8<+YyodKp*Q0Ow9rxT>x zxx(RO8I52Nu-aVew>c_LQ-LB1tBOEo&NxzAN}>fa(OZ`KQPFXZOeI0ILR)amq!O*H zs?s?(ck5DrFetW_Oo4gWiL}{ykrb>LSt62y^A>ypH*M6V-4c~k8k-!VUJ;(yh>RwB zdFxVtDkdr}YRwsST8?ynF3}YRsLx@+^(jmJNuh$IJr8v4MWKD^ihO1Yg@vGaf#CJY zrG6ysbdK4g0?P_x4JNu;;V^hco!3uyU%4b-C9E(S$XPqiBd0k~cyE{y{C{Tg)}{Ug z3r9eKtdmfPD^P=M=pceca1XKGy40_XfaH0ApJOO81kxUqr7ry`oEtD+C zI+#RwNJ`Moj_QM>C3A$vTbKIbxe=y|j?fnAJ@h3@56&XR;P5K03H=F6{Rlj&ifRLM zo(Z^mmt?dxO1Q*~%=0Nr{YW94K>cqrsMD%S1a;|9)hdku-_DcWyb@0oTFwvyY0X@N zJy}cH?Np@$%Dpw*zSIx(Fr|1|kN}~4@(~#p%3#_WVGRnAr!Ms~slaY4yAx?jqacB& zGw26}Z-5WQ0LplhLyH@Z3xNwT58H zdt}d%&ubNO)=8NViqx7v+fu)=vM@w4ABqde=-@vfsi?_^Af-#sxztYyHgZG>ZKIx0&VP)nj4@Zh45QpRK=oRcxgYoaYGhUZ`Ew@xMLH3}`x=t>$z7shz$ zbKw~e;>#@cQ= 0.0 then x else -x + let function abs(x : real) : real = if x >= 0.0 then x else -x lemma Abs_le: forall x y:real. abs x <= y <-> -y <= x <= y diff --git a/stdlib/ufloat.mlw b/stdlib/ufloat.mlw index f39c98726..9bc50365f 100644 --- a/stdlib/ufloat.mlw +++ b/stdlib/ufloat.mlw @@ -13,11 +13,20 @@ module UFloat type t - function uround mode real : t - function to_real t : real - function of_int int : t + val function uround mode real : t + val function to_real t : real + val function of_int int : t axiom to_real_of_int : forall x [of_int x]. to_real (of_int x) = from_int x + val function uzero : t + axiom uzero_spec : to_real uzero = 0.0 + + val function uone : t + axiom uone_spec : to_real uone = 1.0 + + val function utwo : t + axiom utwo_spec : to_real utwo = 2.0 + constant eps:real constant eta:real axiom eps_bounds : 0. <. eps <. 1. @@ -27,7 +36,7 @@ module UFloat meta "inline:no" function eps meta "inline:no" function eta - let ghost function uadd (x y:t) : t + let function uadd (x y:t) : t (* TODO: Do we want the two first assertions in our context ? We only use them to prove the addition lemma *) ensures { abs (to_real result -. (to_real x +. to_real y)) <=. abs (to_real x) } @@ -38,7 +47,7 @@ module UFloat } = uround RNE (to_real x +. to_real y) - let ghost function usub (x y:t) : t + let function usub (x y:t) : t (* TODO: Do we want the two first assertions in our context ? We only use them to prove the addition lemma *) ensures { abs (to_real result -. (to_real x -. to_real y)) <=. abs (to_real x) } @@ -49,14 +58,14 @@ module UFloat } = uround RNE (to_real x -. to_real y) - let ghost function umul (x y:t) : t + let function umul (x y:t) : t ensures { abs (to_real result -. (to_real x *. to_real y)) <=. abs (to_real x *. to_real y) *. eps +. eta } = uround RNE (to_real x *. to_real y) - let ghost function udiv (x y:t) : t + let function udiv (x y:t) : t requires { to_real y <> 0. } ensures { abs (to_real result -. (to_real x /. to_real y)) @@ -64,29 +73,29 @@ module UFloat } = uround RNE (to_real x /. to_real y) - let ghost function uminus (x:t) : t + let function uminus (x:t) : t ensures { to_real result = -. (to_real x) } = uround RNE (-. (to_real x)) predicate is_exact (uop : t -> t -> t) (x y :t) (* Exact division but can still underflow, giving eta as error *) - let ghost function udiv_exact (x y:t) : t + let function udiv_exact (x y:t) : t requires { to_real y <> 0. } requires { is_exact udiv x y } ensures { abs (to_real result -. (to_real x /. to_real y)) <=. eta } = uround RNE (to_real x /. to_real y) (** Infix operators *) - let ghost function ( ++. ) (x:t) (y:t) : t = uadd x y - let ghost function ( --. ) (x:t) (y:t) : t = usub x y - let ghost function ( **. ) (x:t) (y:t) : t = umul x y + let function ( ++. ) (x:t) (y:t) : t = uadd x y + let function ( --. ) (x:t) (y:t) : t = usub x y + let function ( **. ) (x:t) (y:t) : t = umul x y (* Why3 doesn't support abbreviations so we need to add the requires *) - let ghost function ( //. ) (x:t) (y:t) : t + let function ( //. ) (x:t) (y:t) : t requires { to_real y <> 0. } = udiv x y - let ghost function ( --._ ) (x:t) : t = uminus x - let ghost function ( ///. ) (x:t) (y:t) : t + let function ( --._ ) (x:t) : t = uminus x + let function ( ///. ) (x:t) (y:t) : t requires { to_real y <> 0. } requires { is_exact udiv x y } = udiv_exact x y @@ -708,7 +717,8 @@ module USingleLemmas div_order_compat2 (to_real x_f) (x +. x_rel *. x_factor +. x_abs) (to_real y_f); (* TODO: Prove this somehow *) assert { - forall x y. x /. y <=. abs x /. abs y + forall x y. y <> 0.0 -> x /. y <=. abs x /. abs y + by abs (x /. y) = abs (x *. inv y) = abs x *. abs (inv y) = abs x *. inv (abs y) = abs x /. abs y }; assert { (x -. x_rel *. x_factor -. x_abs) /. to_real y_f -- 2.11.4.GIT