From 72c977ea42d5b1086af91b86716cb95127e2ade5 Mon Sep 17 00:00:00 2001 From: Jean-Christophe Filliatre Date: Thu, 31 Mar 2016 11:34:21 +0200 Subject: [PATCH] stdlib/list: updated proof session --- examples/stdlib/list/why3session.xml | 14 +++++++++----- examples/stdlib/list/why3shapes.gz | Bin 4102 -> 4139 bytes 2 files changed, 9 insertions(+), 5 deletions(-) diff --git a/examples/stdlib/list/why3session.xml b/examples/stdlib/list/why3session.xml index 92316eb05..c909080c4 100644 --- a/examples/stdlib/list/why3session.xml +++ b/examples/stdlib/list/why3session.xml @@ -7,8 +7,9 @@ + - + @@ -33,10 +34,13 @@ - - - - + + + + + + + diff --git a/examples/stdlib/list/why3shapes.gz b/examples/stdlib/list/why3shapes.gz index 648c49a5b75e2ab096ff0256ab428b0980db0103..369582641160840ab073518f63fd036e7757e271 100644 GIT binary patch delta 4113 zcmV+s5bp1WAgdsMABzY8000000RO#PNv|9?lD_*_ynCYoGJ;DGup4MJMnGNc!vJ+{ z1UI(;ZI;x7`T6s)mP}?<)_Zztjb*^f%47tCv3@~Pn#6c6Elab>X$`4Z+qp%bYi^pJ z^zDcK_J5!L_KUu2AAbM(ucImE%}=E;SLZcbL#fxyQnhh^$SF&#w&~M9_UQE2x9|4e zAMRcf2LI#ZhcCzD5wk_o%95QDL`%sSPlkPADOEX3xeEEq@ifIB*Pk1asY%R1JLJtJ zdzYNAC6#79{zP-jlfi{Wk^ z{`|Tz)?df+cKuSlX+pIN*RCb_GPK}aa9tcf?aB7rY?#CDn%?{bAE_am))6{IQgRlq z%<3qAn9M%pDQCQr^(L=OI{0mNgu|}x-s~#mx7j=P6*=pSvcW1eJJ-0lnAEUMs_c`9 zC(m1-A*>F6U*7!%xeg0C{JLZb(odh;c>HUzlNGm=>av@B{k6O|p1()zk71V>?s#^ zRCvFq33^F~wAJD9QkIA0sLRgEzyTdevnZKN9u+M|cd?|PR!ZD=mlN?LcQ}3AUF7&elQ{z+mz(G`BEv;uPAIBEHs%hSdc7^<8>3x+ zENSNYfVd2*UTiNWTGLV1kON{6q)!Te-LsQvRj=c`S@S)qdq_H){g#fA@^0w(`rv2x zZ=?a{NsV2IH56ZnU2VNbpfBIz1+g6Iw=0;qK!;5XfR9?@C`di*N*2&-ZvaCDcoI0u zT*1prj8-6X^v{j-Z!Vzb7_P(I-7p6Sp8!rkIxIE<+ZhEm2EZK%r4;HN4x)Ju#ff%y zu@eKt*?%2YtQM2v11*1XV93;aXfXsIr~vbD&8TBqkl)HTFZwVIJf$;Dnj~uQO36?+ zjQ>L|wI>oJQoqaDT{-(b&iw59c^2XHm4I-N!WHgDNKw*V79U5xX_5iU9LHAUO_AOP z=DBX06*ba?^27rvWkh|g)%KKq@2zSw7EQ+JqHa*$D_Gw_zA%5&`tz%qHax>_^@eodROBU{U0(ckTGMLCpVua7J`DIo^pOil#-MoP8UJ1D$*$65guCX5^qSO862 zfqLBN>w9KL5+mKi-g_>42={)}9hhA#vTPmBxV3*J-+~AJvOR|a>>jdD^2twYoD&oPXTZByEkP8T{u8N9S|y#!_Qs(GW}Rd(N_o@@(f68F;Axiv?lu z4@iG@%|}iw!#y?Zy3n`re&AUv@vFM0iSnEKCqz@nvSLQ@0hsdLR@Tk{hpC{l@A~0` z(mHe{Ef#Lx`(h0PBGhhsi+yZvE3@dX*FEOycWy zhe%Cff31>p5JeF2(;dy>b^D>01Z0fYRqKXh5=FWel zwg$C86vinN5i(;7>e7jm9Szms#Pep=vI}%!d18oSM(AsMcC{gH*;5zbcUU?>I6zoE zapZxc&y~pCa^$7;Tlbj`gD4#3Of=Bk4N*YOT1NkUqcJ=5@a_^euA?E7f%1^DRSW#Y zlXPu~QcuJCuEyI@dpF&e8b{|^10{cSkI4a(p&9DIN}$CR=H&jzn44A&+N)8_BIodw z%hO1(z~engaZ)XWBb%Vf;VOhs(J=Ope!w)RfWPMxPJH63>2Q9CGoLW=IovVv$8=(1 zA=O0+Yme#jgj%&SO3TwWRhq0J7bJ<`h-G985(G%9)J>iucvisSl?u4qbk%>6li~1En6Yu!i^9<2}i#mj5 zalVr8_`5|#-Vaqd)N`=ztKb`F$bhZrRtoA-Po=2!zMB9jV=7rc+LwDaeA2vIBlEkRx(q$zceLks^k_R8y-|Onpr@^Rn{zDzB&hRWTA(+@Bx&k0(RE6T6 z9^3fah5b=R4k*3I4#vbBMYKBSJSu*Rp%0;#hVkcL&P8zfWjDW0IURoyWm_~|Q4@fu zIQQafR(0N@pYdrerKdtTl@f_AXF<>Dkv58{I)Vpq1`^Y8ULiziJ^7jj6HfTy9 zcFu7`bRrWUKQq0qK9J?iV`L{59RLiD8fK1~LLT_!5Il5sM>o%|caKym$j^mA(_y zH}c;lx*Bb_A&wd@DR@^a`VB;6cY@~4_MP1P5=*O*s@jZX30Psg%9Nf)T z{br`(0h3Lkfjvu4Hl|`cZ~=D-HFo>7&*<=io$n_iMmz;Eh#`MCCe#7s<~l%nFg3_J z(IXx6YG~SZ5ZW^|&G2s<zEe=cBCUf7OcGfuM>DRHpdU?J@jW$nc^gf8C3a4>aY-~inO8lOD zhg8&+t%w-*6}^-}r!w~ZJnD~gvsJ%6-yzX;6jnCUNk)J3PSR2tmKArp7x#R=dtm4L ziF)oXRH0Z?MP(U>ERIn*DF`xPHLu8b?npl%NUTEvY2FK3N&^gwG!Gz)CIls1ddsiK zcRxm;1mtW5?QP+TrYqP4uk0MN8cW>U(^}a7EFGonO>pY7=Uj4jc3fK0khGAY*dA0v zo*;;MKHq=+7%{UK0}Q~~sv8$fVs#vSguK}aQ<*N*e)#wMe|{`w`0%(C*|MvJ4FgO@ zVz^>#2C1EbC1grt<~y|;((Sd{&8NfOdtNWs4iJorT5Zb_Apu;f0m4?mi;Bvt*1ARD zE$8V0im!@MNnBV|0e0bv_39hK6RI#~eIQqYKEZ2*-%yZ)`~c;&Qi+#`1p z2r7StK#5Z7me9JTMy zXK9xG`N1l6@<|abE|2XWc(xhWLgASi;p>0*l()}oUrGC8ca(u3z8^RTwlCR?^Ck%n z?S5hfM9R%_tv*?o(G`4ZpWpxc>-lInpHNiyQ5u3j={SpobL8MlO-1@L`UFuH%5eiM zClei#M=q_}2t7x%hm?36Z%X269y+XCXv+mnrH-3MF);c}89hFdp*4h>fJk5FUpIf{ zFAp1@Z+?}`=No566`C-~ zNaLOsPRlXQRkZoG&CHP@9ExupoBXxrVqqOr4`|I|uI}$S-W+{S7YpWi1Qx99!zp2v z6sc$}p2OHP)7F%Q?>KLcx6T`(ixz)*vJ4HhogoCM*JhOL4^Q*yRWfg4DNPzP|lXw#zyEdOaSR_ld7V$J;aId2GT6 zR3C}paW+$hZ8K^irGO{_W+=!J|M@JZ^s&drU)Y4}7G&76@f$XW9UkMp)vuGP4;w*0 zR{X$`4Z+qp%bYi^pJ z^!>;F{=c98_M`sRKK}acUq@5SPwz@$uFh+=hElJYrE24UkW-deZPTZJ?9u7Z?|<8S zf4F-|82pb{yrY125?T|N@ z>|JucmQggSXN`6(=V8l47N&9je2Y@lWqk>&h|KPSky| zY^1klUFe>FEu`d?N&BsRXdl0QJt?kz`26jE-dQEenVTsBC1jx#ieuMo@!Y7`mG~p3 zw`0yvAKO)iAC7h`!&=T!GKZF`FO9|95*r(B-*b}N4uzh9&Va#Dcz*j;Ly~Hw;X&bF*le$ z`}D#(x7=P_FNV8y`19+=SbrVM+x1KJrU}(9T)URw%g};z!F6%`v?tpyvtbUqYx?OO ze58hKT8HZvNy%B;BCDfdGW(FHn0+JbO;ar+EvIevv=$(a@HATgH>pD zu5odHF{xpjRM{sHPoB3vLs%XDy}bJiat#)8_<4y^($8Poc>HUzlNG=H29f{s(}#An za4f_uBCu6TO}!s+2$ga+68{mQcSXg2 zB8NsLQSn~j8PTYXtyq8n?_xSS8g+c(aIXL)rt;2*!hs8!nrqzTbnYfQNUL%_c?XU`hj>J2ZG90V7C zu>qE(-b0Ha_&^1ihigV1(}Mg~UcKnUH1L$pG-;Bk!7C+0-7x+OwbY(SkVyS5XLsf7 z_c-&j>*ra7(^mq*K?+y68zDtWcUgQK`KCz*EOQ)NjW z)Z!Z^dxc&XZmUXn)J6W?P( zo{Ncqc+uej7?I`V3LHD9uyVeCP_1mPQ%z`Q=1g5ZxoSjH%F-0gvI`dVsH%kA=YIK( ztT*;Ky?3vmbtl@xme4PRd{4;NF{epaYY3O@(QQ&J(E%pa9)N!=00O=;iedLbf|CI}st>6L8u<7EiFSz>802ohx>ErdPm@*7pZvDp z_X&+!)9%r~nG#|k&g4YUZ=_Uvy@SH5cdQjqVZz7(fd$aS6{yFJzP@L6Br(!G?7io* zhj8yl-GSM~BFom@j9XiO@-2AaFWYk{Kwi{5T3z3OzM}Yzcl}d8e{LV^O@lUlIUC{n z<5aZJ>9-1o70oVC;(r&f0+iSv(} znxw6fG=smcaCAQBZY(uM77ek~zUM5fD9?6Ik%5;AuvicV|A1tF*L>u}GTc+ct_!`6 z_XE#biQm*cO_ZeR4oxy}P4_-Z-PgmW z_nVz~4xDp5!ewlKbP2tM#$J=8Qd0#u2gEO93;#*Ke){qa=={<)plLk6INHC%a)Ze^ zZ4T@LtbneqLfe#*(Pq^rbVsL9kLs|LJ9dX>*@;b9u19L+9wIe`{k2NYK@>s6Pj@tj z+X=A5tclqo??4SNiYh{Mm^+hy+8WdXQ5dI8M97RSs7ohK zb~IFj6VIDf%P!D`<%uDR8KJN3+0}-)Wlvpz-(l$l;Q(Rv#E}P%K35`l%aNDXZ{24) z45Dz9GtoeEH$(wBYZ?9bjmGTI!*7?caUBhr43vkIty-kRU)(rEc;R!LtGmZ&bkDrmK#BoD@eu0=Z<98`=VoXhIb-HTz}O z0YG-oW9=-_f4m(WC8X z^hSw)f}XbOZO*kc7Dw zDkTzK&VruPBW)B@bp#LK3?#r0k81Gih4R-6<*ygYY|xZI?409>=tL%z2p{DU&2com z<$p116h71ACU9Y)r*? z-~#RvYV7uDpV8q3JKs-4jCcxS5JPZ(OsE6M&2@nEU}}(cqDMOB)zGx-Ahc&_n&ICz z$N_`U`6cHpi!E8w__xO*wKW)DcCzLFuRxWJ#!`&&#wG!L&*-xNxl1Stun;Eu{#hcy zG^(f^q?*+kO3|Qnw`K-pY7-#ciZOWyKd8{(RZK*HQWR5aV0P9AXmF%GG(A>-(N-;* zLkIV!e5as>MOp_Fm?W}Rj%HjXK}i6_U-R7?InVjdO{8zhcYado+wz^I5Q8m9-af(G zYRV-6HbPyp&H2t!8f~7?=zS1N6;9)<*w~1CmH0>U9a2$OwjyHKSM*W_oyyqr z^Qb@0%~pMVzC)txD6Hc`8p&vX-bq?2!?NOf2ruQk2X?-nsORoN6^b=gRF-kb;uw{a zf*=D{^M-uqj`SUZ#5xp^=Dnb$G{CS(^8m7FLQuk`xBP~D_k9FPK+aas-WINCx`Ivc z%FZ#XvBbSSt%d#1(oxFZ1gAcG&LwAO$E76=NedZ@?Ljr<34)mC^WFD<5i@%+zyO@B zx^clIR>#pt$eW!omFYt3$A5qL=ciJJ506WcExTISFu-IahAYNqklHC&LZ&okzSFuP z-Ck?md^+sC=k;>y0KurJ)wUcF62PSzAZ!J^sHnVZty=`%a{hh2=FqKiHP$F~Z0MnC zCjy!x&c^jlVZG(}h{e2rfCobkJKuTz&eMX>RE-Nr;{>VTj}ZD;n4<{Vdsfm13wnHo z0VPI4X^008AXR4H}OC+0Ztqfxif?JCW=PcDv(y-D01FnV!cf47|1Uap6#-qGMIylK8F$W70iOG?mb_ZfL1BlDS-5qAOA*r8|`)3og9be3k>pC7DJC!ZA2;_}%3 zfoGd>Efk)a5x#zZPkH;i_La0hc1IZq;`@PfVEdBIIB$~R(C#NzK&0F(*XomX8C}8W z_T|IBznzbU^9eS}D zc~e$#LF)Uj-`;;L+vOa7z8(+F`^49w