From 2eb4ca283e3c817b448b88ffda581d25c4820dcc Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9on=20Gondelman?= Date: Thu, 18 Sep 2014 17:11:18 +0200 Subject: [PATCH] Fixed and proved theory list --- examples/cursor/why3session.xml | 8 +- examples/cursor/why3shapes.gz | Bin 2055 -> 2054 bytes examples/finite_tarski/why3shapes.gz | Bin 0 -> 383 bytes examples/insertion_sort_list.mlw | 4 +- examples/insertion_sort_list/why3session.xml | 9 +- examples/insertion_sort_list/why3shapes.gz | Bin 660 -> 689 bytes examples/linked_list_rev/why3session.xml | 40 +- examples/linked_list_rev/why3shapes.gz | Bin 767 -> 774 bytes examples/mergesort_list.mlw | 3 +- examples/mergesort_list/why3session.xml | 1041 +++++++++++++---- examples/mergesort_list/why3shapes.gz | Bin 6808 -> 6872 bytes examples/mergesort_queue.mlw | 3 +- examples/mergesort_queue/why3session.xml | 213 ++-- examples/mergesort_queue/why3shapes.gz | Bin 3833 -> 3833 bytes examples/sorted_list/why3session.xml | 6 +- examples/sorted_list/why3shapes.gz | Bin 187 -> 186 bytes .../stdlib/list/list_Permut_Permut_length_1.v | 156 +++ .../stdlib/list/list_Permut_Permut_length_2.v | 175 +++ examples/stdlib/list/why3session.xml | 465 ++++++++ examples/stdlib/list/why3shapes.gz | Bin 0 -> 4102 bytes examples/tower_of_hanoi.mlw | 3 +- examples/tower_of_hanoi/why3session.xml | 380 +++--- examples/tower_of_hanoi/why3shapes.gz | Bin 2203 -> 2230 bytes .../unraveling_a_card_trick/why3session.xml | 104 +- .../unraveling_a_card_trick/why3shapes.gz | Bin 3581 -> 3594 bytes examples/vstte10_aqueue/why3session.xml | 34 +- examples/vstte10_aqueue/why3shapes.gz | Bin 539 -> 542 bytes .../why3session.xml | 26 +- .../vstte12_tree_reconstruction/why3shapes.gz | Bin 3779 -> 3774 bytes theories/list.why | 49 +- 30 files changed, 2073 insertions(+), 646 deletions(-) create mode 100644 examples/finite_tarski/why3shapes.gz create mode 100644 examples/stdlib/list/list_Permut_Permut_length_1.v create mode 100644 examples/stdlib/list/list_Permut_Permut_length_2.v create mode 100644 examples/stdlib/list/why3session.xml create mode 100644 examples/stdlib/list/why3shapes.gz diff --git a/examples/cursor/why3session.xml b/examples/cursor/why3session.xml index 1a2187b72..4af148686 100644 --- a/examples/cursor/why3session.xml +++ b/examples/cursor/why3session.xml @@ -41,7 +41,7 @@ - + @@ -52,7 +52,7 @@ - + @@ -85,7 +85,7 @@ - + @@ -126,7 +126,7 @@ - + diff --git a/examples/cursor/why3shapes.gz b/examples/cursor/why3shapes.gz index 69ce22f571161d81a6825f882e56fe1e671a9f9b..e182a5d5d286695c2fe1eff201412c131a37addc 100644 GIT binary patch literal 2054 zcmV+h2>JIPiwFP!00000|Lt1KZX3rE-Rmp34=&KvRsAR+UKjxg5HP$7W*bz$Vj>FV zP_mKx_qT==$(a#JNjB}sx$;6D_RLh*yUuAc1q3cxN{EspIx5bC5o0pB45rSOvRt+0 z-?KLz$?c~;2>0!CnD<*~l+9tJ@B!^Mh5Z3)>rA=jQL^&p&4Q)B5&i ztuJ&uAL$z2zTdy-Mq5Ssb^WO>Cb$2Z+@DBWjAfs2!`8=csF_zyN22h=%j)#a=h03$ zGP1MtE7xjcBho_Q``nJIp^#b zYm{-3g{W1pWnsa^WQcso#sCFZAC!dJcw5(>Wn<$D?q`d${pj{`lB!tsNpUTbRb*=l@$BxZR5Go(T);F1 z3m#f=5;DigDU{M?lRO)4(;G0&L)XPa!uf5oh3)`xJM6+P1?^(`Bz7=g3}n&#$g?9A z)JuazwY@I$t6&2dOkTYgtU53gM@ykbg+Ccf8UT2=35%JQY1m!hu`)fN&9O3Z8h*16 zKWuT~VB*8!rrQ+XNs$v5t2^!6K}v2b9XdKJYBzwL=Wsqhp)RQ*2jAgn6F;p499M$h z;rUaNPuN3Ks6Oz*<};p>*+=^Ln+MGO=!+d}GDK6PG-DLkP|$2I)mjLWa!H7(f@gUY z@qg9sQne@{`(iPZ2`+m^g;t8MVkAU&ZubY`pJlezv~~oYTOdh$Nlwk9Q=Z_3e4{po zs+W)Lb9Bvxi#ByqY9^{OH^-KYmbA-4t)&xe0msAYiHUsLr0-)av+@Qs!CQw_QATqj z+96VGUa4F0&kf8EVs?{)O?j}Ztn30^)#yeex&)P+Jr8PMV5dFfwI4l0p@yhI$x7k9 zL(NqRR8zD$TSX6yPYKlnkG}@#vO&UHU2uKJu+=sP$Y6ns5=C^;H}f=-@(B8Q4ccXc zW(qq5Lp}O1IU_5ZM*(iWax^F>=*vBH9hmon*z3HKkrJ>fKk;6t9VuQ9Y!Zv6Zm_ch zC$a}Zw8@{lo8PXNx4NE9XR=ug(z7!g_9W}I{I{pb^Q+nvUMb*_2&J(XC=!hJF0Y^a z)4JISNByh@n*%W$NgWV0t8|6ljx?BG5oDwSxga!0Y_f48?e~}_2}JH*IIl# zn`pomF>iBUey?}xL_GFzhZhvJI3vqFN0u8ljnSw3|NoM?`$cl&LvZo3Q3 zKv$J-$1Un%4v2zkFtuRxT2$aIvx`N`j1~Ge-%j_!uhDk#rRv7y*wv^Vn;axzrYy!- zujJJeyL=1=ZryyD{hRo#j6jMsO;@U-`#K+-aAZcGj<=#0mVb+H;230#(HC%pmNDfR zQ!2?NQpT3Sg>UDW_g@@Kg3y{o12+3CwLAGsfm#e$B7|Xw$E;<~ojT}*wn^RN*Tx(Q%2#pQ2 z>=kO4`nUewzBEfWpH}7et2{ci<^GW{znn$ERLx0=oNZAOU%c`@BN543qT+a5L*F*_ z7BAURhP2BlL?J_3wJrxJr8;fLz^*A?nlzg;1^i>$@3q-_zs@9|MZ^TXN7u4Tozy;iW1#`!P zRpo`eE8aN%hRXFK0Ow=1;qCC-o6&}L%7)^Y4c$L56}XtlKj)UM_v5=s-G#BtbFRHV zJ*LI+7q-l+O8~FSWV08bBY7?8V^6wZpQD0?-Lx22={RwnYjCbM}92ZNMiyGsL^#B-k zaul0Pbdsv8skT6vVhbnE&Exp&QqCfF>Nnsb&j*iub; z@O|d-UkCM3d5zyc5x+>yTIT>*ft~_D&+Jk#3{8h)fbg_~`^O;PYi$3K0mRV<)ACOiwFP!00000|Ls~!kK0BPzWZ0`9xTw+UDXdDJ`4f~5McPU;5Df3u8xH` z8m~q+vj2XI(numXl4fjcl5utp9+OS7y59AD6mxKpYT+6pm*@y9c`$5DK`LNmw&dli zE&rUo?U3(2|Iyj|^Pl;ntbW^k=+gdxZuXbn7Bg5Zw;yCJt4(J*fc-shN5X#Uz-<@O z;;@~r>@Q*mcD|Sh`la#v<;TPAse^+8`mo_&ZdZ35VCM&`Ru^^`x{l`W_>bRb<@5UP zcC8O|X+F|5+`K&4^| ztw0?dfFlO$y!WJvqy#P)t`S=BBdsQ>wD{UoTl{5aVW}1pK}{xz*c!=bp_-b!W80W7 zIs3&LWhf>_Y~r;nEKtk_(T8FTU?6!=5^Cd}tiSNq#uwbr78m>33l2zTn_UDx zi!)rj^$xubE6f)IGIHyy|G%lqooK_#o~0Uw?5s;RljNKnIBoko|L?tDrL2YT#i+2)OSMLwYL zAQYQ8>WQz`WSH8xvO;O@VKbm0QR19^Z6NdQ4Klz&W$$l(@JpT zO7MF;e@^lldvFTX2VU5oyK^%8NS}W4h`Aqqu!C)eD7y2xcLPRZ&pgw5Y zPexGn`my~QT?;kqs&m;ZKTv`M218O18Y`%#k{WZpVgHRDnq|m%j z)jlPWZDb%NaT99v1YLg+v&mEz@Q^7Jr5dAhCm(8ts51+be=^H>A)WSu*M9U2t&n1^ z$~$7S1<(dpTPandH%(g!KP6NTJpLM_>jo)ABD5TX1h4QX7^ic_M-Y%)L(5MiDUYC^ z*PvZDXgQf26rFl&rJ}c_xInSE4uZnYW`Bmh+(Xxac|VA~E>vSBi09lWDMQmK(7yy^ z@0n9=vm+<6M?$pCpUv&BAD4H!UQB0-Sq##%Gh6n=>oxzkr^rg4vMV7b6^l6*Hb-JMk~$!0R_O}fj5L_P(Y7e;P+_HO)O<#twCo^AQv#y(cBCG? zn`EuUx3>ugY*EX0oBRBmY}ASF)Xkl{qNv3MS@bosXxKDHXZQdAOWj6;V>{|GgY|cZ zZFSxpLNm}+<=b(KdYA**x17DB0<{DzwfZb*e8@R!sR3k+`0KW`&(%)HRBjDD^U(EVPI`So{LQd@pLPCVfnXs4#!Z)CN}L_ zedj<@ViNk_ixOsIGd!bX-hZpgv2sgHp=uBtlTRrWi_#1v>$NBDU+o;4Ee)Dm(y0w* zI=16zY^TH69x(HrF*qFFC-DLnI57Qf!yOrei|H=Dvx6a{kYYZNf6|0qf1dRC%P!** zQgehQD-)CI1N6h#)I@;ZRh)fZX_F`)IDZt4_;R&ri?RIc>5_7Sn1O&@Zm5V(|GD4= zt0@H&DAcadq*feQ27Yg_XwLdmZ2MXGAt6(bZ0j%ara6Yn8 z7IOqqJ^F+#7Sf|L=;*>di^)y&;HGCrFsIBniCS)vlJU*As<1JNkC{?|#LW-CKe>O| z0lk=mmiIgjaDNm>3LY1aFuMakM)*UCKXnjyi-X+IrNdR#dKCVxxJmtj`r8b+0Nqz` z>e66Ud12ZYZyf(ZMZE}c^Re1+GyL^tw4t4{p*Utk_cu%hE++CXxn<}5_-;~nVJ!2K zYwzD4IKY-Ewuc{3&kO?N4V98`oeXS8mtF=I^&Y$^$<7(-0Rb!BH zwYAnj+3WOZg{{$JR8!As zE(G_V=MKfS0+F`D~ZV&q-dwol61i)iL5P)ZF$;@`^O;PYi$3H*jisw$bqYd lw*SCa3it1joKKD_*K_aphuD7Lg@2A;{s*RS%}Qu50043$0UH1S diff --git a/examples/finite_tarski/why3shapes.gz b/examples/finite_tarski/why3shapes.gz new file mode 100644 index 0000000000000000000000000000000000000000..1dcc90783df443af1bfe25b70772b4e17d109198 GIT binary patch literal 383 zcmV-_0f7D=iwFP!00000|8-K!YQr!Pyyq+O30l1c%^`;b1g6KmuWcC&d6XnA{rt+Y zpY%rsQ24PqIU5P zk!TpiaEQ#w1OXZlN{E)BZ3Z0E5gm$H+Ahu&qTIWFx7Tz-K{VrlsG-#4be!Q5K`}m1 z{CkjbL2(mI8)Y5uq3g+)$`~ ze6FrK>sty^kQ(G5tub9Iy-nKmNwp;HdMt;*SM#(Px%)p8{RqYDk(AY#?8ubx%{A#* z+OMujS2KnvE@PWmVgJZ=9Y3Jhf7bE@!n%Hb)qJpZuHkXjWvb!bRnI3#i3Um~%xmP! d5_MTHsV)eJOKssLD!iGER)4V)mlx*)002`7xKRKA literal 0 HcmV?d00001 diff --git a/examples/insertion_sort_list.mlw b/examples/insertion_sort_list.mlw index f659c1748..098dc9588 100644 --- a/examples/insertion_sort_list.mlw +++ b/examples/insertion_sort_list.mlw @@ -7,7 +7,9 @@ module InsertionSort predicate le elt elt clone relations.TotalPreOrder with type t = elt, predicate rel = le - clone export list.Sorted with type t = elt, predicate le = le + clone export list.Sorted with type t = elt, predicate le = le, + goal Transitive.Trans + use import list.List use import list.Permut diff --git a/examples/insertion_sort_list/why3session.xml b/examples/insertion_sort_list/why3session.xml index 7f46bc8a9..07d6ebdf1 100644 --- a/examples/insertion_sort_list/why3session.xml +++ b/examples/insertion_sort_list/why3session.xml @@ -5,7 +5,10 @@ - + + + + @@ -27,10 +30,10 @@ - + - + diff --git a/examples/insertion_sort_list/why3shapes.gz b/examples/insertion_sort_list/why3shapes.gz index b9e142ddee225f82b16caf4e70769b3bd21ef72e..d7988206be0cae0a01eacd6ee301e5edd0c2f096 100644 GIT binary patch literal 689 zcmV;i0#5xOiwFP!00000|Fu-hYFj}J-S;c}38NX!Ytcms1Pr0eyO%~17+O0x?&I^T z>%`ZoW7D+I#pS*<(vi;5QBEPKM5X|tWRO~F(UM|GHd4(i`l3^q;(ETr%RNkR{{g53 z1Gdbf8LL~b9*_K(CU{e+E$7<9^7XmT^!)Cp)~A@c z_1qMSvNXUZqf)7v8dcKD)Iwi9?w$@~x0TIdv)f+ndA&e`=ht)gCK*SI+HYukSc#6k(vx23 z1z(t-^|Jo_-l|r~M$F)QA*^*^0VgbjmxYKquO9dMW}@l+`FlnQp{1B|6SI~nqE-=6 zW|bk=Da#M1YOAZaYrpoNS9TTP6JgFCQVcKPz9iY~eRuh?pm*1KhB z0x?((1ny5*6ePuGg!;Ci_=oEL+$E7iqv(UoHYl1Ufk$Xgd zI71!YhIYu^JBpHgZLTx@4E;QpqXoDuJGlfad+#R0Z(u+*x?%`jm*px)^GvR%3#FPM z5o+qjJgN<#(5;VyyA&B--YTM0vrI9vAbbYqcD z&|L`2$Y)7ht>KU*8zrhr%I@O=&D}yQ+E9x1hX4J}Kirn-Ux5MV#ApOF-=3n@V`Hkb XKSNILlD8=OPjG$#>yJoK76u+n?O8s5 z%68m#ypUudho(1`p7iweoOlZ@_$)0~vck!$$AT^}R_9^z#ILsg`D@EhtL0{J0}TF= zH>>s5bnx@Hul&4t*>>;Y8pCKhKH}q3+h<-Z+v4x!$B+ixANey3 zaD|k|b9p{~aCq;hX2%$qK2V~}O0|S2HIP*+F8WN3O$F3VURRrKT`hI7U96Tj zd!CJ@!Qu6k9TRzuQj$x_VnOyM;xT5%oPx!R>{ldz7A9xMfr2#fF>1_3AgA6-Q^Hd4 zb`yAFXm+5;pJVL*`5{ctk%SG4P)_WH8{~%06A?q|qRCu8Xy|_+lVFn_rn;Caa!Ex) z6|AKyv$M%>UN3mLov78d@y0Inf^U=G>1Fo(S=1N}3^-V>(5NNOX5^C3o!A_aCa-I| zVl;d{f6asqoSGF7HR$qlRi%r?iHN4#Bcu5-8(ywY=$kT5_5}5XlGp;pkd;N%_eQNh zODDQf_X9@%!EC>^woZ{m0jhx7U5P0m`65bL*cGj#L+wf#v0#4mq|@IslX+jJzw1E9 zxQjk6jVYdl=8j(DrVqx@H*>czVAW-liDj~;Yg4Cy@ zedoGK0W_|$5o)7n;SiUD8MR|8A{E@RPHi3K=e@#O7t-s6bAshof5>yWzK2LJ#TTTiP1 diff --git a/examples/linked_list_rev/why3session.xml b/examples/linked_list_rev/why3session.xml index f93c744a9..caa1b4393 100644 --- a/examples/linked_list_rev/why3session.xml +++ b/examples/linked_list_rev/why3session.xml @@ -4,30 +4,26 @@ - - - - - - + + - + - + - + - + - + - - + + @@ -39,36 +35,28 @@ - - - - - + - + - + - - + - - + - - diff --git a/examples/linked_list_rev/why3shapes.gz b/examples/linked_list_rev/why3shapes.gz index d1e962d89a65b4bd1f064ca916137b9e9eb641b2..2120c3a0a968545aece529dea80fa69cf4b1eebb 100644 GIT binary patch literal 774 zcmV+h1NrjZ{s)+?ei(wKFFW;k$e!=}v`@g$CqUN#eqH006n2u4WG0VGvLFeLwBM@}N0#Z{kq(D`# zt?ABK(X7rGwqck9#$q1SCtxM1RwM!jv}B}U%S+jg{oLlm%j9Yw`Fq{%jg3yAeioGT3VJ)tTx^Fq-9gtcP?Ym!OQu`fs zS%l}{a(R~+Dqr4qbBvB5iDH4?$9;<8dt8UB4MVU)rnxy|zDM zhsfY{wLz+5cHGRFebyC=m4x+ONjz^$WBbB$zW=RftbRvfgHwT>2%Bs?D#@;<3`7#h z)m+|fgX_XhEc#2=gRUAmkV%ML&BD`O^BJbyL-;;t>LS7edg@Z`&nSWrbdBGDodnmCi-BrSZ6V z75q~6=(nKTPfbE<{z_84CpM}kTMHF20NwLu+{tFh{pC@8dGTI7{xYQg0W$U#=&lU_ E06sQ%l>h($ literal 767 zcmVh|5LOqUL^iE2eM91k@p5S<+ zu9NU$Tx-txSfi`8B_m`prA%U5g6gVsWK6f+?e4o_eBk}S<3YcM!_Vk@E)5}>5CbI? zs$7IXOF${4DTz1ruOoZSiMYni1~fG{;uN743|a%!i6gM(MJG#~uSpwXy*~lKHfKFW zAF~BC*%{V>W?z(k>zTgh6u^fXA(7S?$4v>6)PRt|M5Disr%CpQVK=@#wKu;#w_i<( z;G!f`tILd5yb%`+s>Nz1X69?8_j}Q3A9xw>udNxI|07t)6$4ddsp6tuFwYzl7YdX! z8+seqS&4q-2E{@{R_D<+JdeP004R|dIbOg diff --git a/examples/mergesort_list.mlw b/examples/mergesort_list.mlw index 5779a6faa..26b6daa07 100644 --- a/examples/mergesort_list.mlw +++ b/examples/mergesort_list.mlw @@ -15,7 +15,8 @@ module Elt type elt predicate le elt elt clone relations.TotalPreOrder with type t = elt, predicate rel = le - clone export list.Sorted with type t = elt, predicate le = le + clone export list.Sorted with type t = elt, predicate le = le, + goal Transitive.Trans end diff --git a/examples/mergesort_list/why3session.xml b/examples/mergesort_list/why3session.xml index 6215ec61d..48ff85b06 100644 --- a/examples/mergesort_list/why3session.xml +++ b/examples/mergesort_list/why3session.xml @@ -2,577 +2,1210 @@ - - - - - - - - - + + + + - + + + + - + - + - + - - + - + - + - + - + - + - + - - + + - + - - - + + + - + - + - + - - + + - + - - - - - + + + + - + - + - + - + - + - + - - - + + - + - + - - - + + + - - + + - + - + - - - + + + - - - + + - + - + - + - + - + - - - + + + - - - + + + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - - + + - - + + - + - + - + - - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - + - + - + - - + + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - - - + - + - + - - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - - + - + - + - - + - + - + - + - + - + - + - + - + - + - + @@ -583,20 +1216,20 @@ - + - + - + - + diff --git a/examples/mergesort_list/why3shapes.gz b/examples/mergesort_list/why3shapes.gz index 195f0ec7ae19cf4536a7bb9138d5c8ec34771bdb..ffcdcf718ff746ba65310330494341e420c90c31 100644 GIT binary patch literal 6872 zcmV;}8Ykr+iwFP!00000|LuL*jw8vD;Cp{Xz6%SOnVb0ms0B0%Dj)%&=Ph3se$Esi zRX3`8)I0O_YtCdGWJEB@OlB2JqFSgVBZBU3huh(HgqUW;G{D%v2^Y$?+EN8uuu@BU zh<~q7@I;UOFYf=s6Mp<53r3DLI3x(E)l>n5A~{OzsN%zi5AoOfp4c^MC&SU%JNq2eWwx#~=TgVf(3JU11%Bum^#k{0M@d z9+lanega{-D4QV2w1l^Upe({q^t{j~y|Mp*kIVJI#~-|nF%VOPMp;Vpxd3nBUZ!^1?Xt1 zRhE0ryy$F6QB36OjfoM&Ah(LH1Q$c}>mb5>sy*YHzn(Q=^wzV>&Sl?#fV?BH?8$_j z91yMp3Y&mlHhZPeOy)|)ahBvfsD$9?lLX_)n#(CV%>QwHLLF3~VY4nqmLxR=Q_xGU zK#~f)k*+Vy-lsIdq=4*;4^<+z)`Bj;s0@|%@Xz?=Q~dnojlb3R--3_(J-DDD zKgq`nKm%V}%8?i=6<3?Y9Bs75#_Ysr_wehNx+LTzZLYNr8%=UnbxiV1I(hYlY!Ty} z2o`_5agXFZugm+nu(WFvUvK%|hs-{JO;i}YO)B(~2&pJiL3AwQR<+ozz!HIVM`i1) z*p{lTxj7faS7cYPp3m*q)0vMyUkSEEx@RS@DI|rxiZ0#K2$+j&oNHcX_nCcgwS_1y zop-@=De-_Npd9^Z5Q)rQ&;W}^cP*|eyV-1)!@+0}K$9ASKisTg>@k|7`qH|5?8%!|%q!uD^8w)TQx1>Ob@Yj1vrx z?uHMj#Lj8}`6#=w!5520DUC)I+su$2cgmj*F!e-}vHG_@^#6^&{#rkmZn)2FY<}_Q zeDrht<5|ytSdwUK2)DL^(K1JTaR9`}lTTxR+|C|XJGVP0ifHqUX*8W@cAxYj?Cm^=gcUvf;%n zw(G*a9=_7^*PTS$uT%y&cmTsbx#ufxfWck>g14&54R?(PSs}?>TxO;wV8yqvF0?mg z(jBy~0$K^iD_~iyx2{12htY-RRGB1K{V`}8jE4(-s0;q<8X&XP(tNeM?YEZ_VF1Km z0Ekgz*yetUlywJ%Kx*2n5tKr-PV~;(XmkSr0-0o;S`wU^%aDTlhw2!MNf>?Ov`#6x zfZ29%nJ51EzJR!5)$&Qr##VqssyUd(Ay+kJGRX09#-37gh28X(07Ooq(C%QgmfEO6 z<5nY=S_*}VXZtwz+KNv0R;4_d1w+fu5Z*%83?nqhNVf!FXLRlKKaQpmT!1i&P)+p> zROnE2(Gf-EZ}nPo19cKt9j9qbyBO2mHoWSVm1=BBNEoaUhl&A8)~gXu(%P|0aO?1x z&;sSs)I)<{y@66=Owrb4K&7vH7%6qzaFEK;jH=#s??P5R!X~H#ZBk%1CQNYL_;Gm{5 z8EQe5N%4*$r*6G$14`c$pzILTsBtL5Y*CH2V%V{z>XTSFJ`ovWI4eP(Nqaigchj`~ z84^`^FfN}4Tn#>-vLlVFwWJwyO_LSaO!x~W>v+gFf(VHPNV6= zS2CTfHn&Bi5ZMlCkiUadMO16htJ!U#+a;%Fz_VtE!l|EJ zQt+0&&uV)*M%8f1QORy2!haPOIX+(gN-TmFjruWETC@t|+tk?hGMa44*wCE)OSh4OW_NFKKf$K=L>c=?+|p;o=xw9K(w4@s0EvRo7p}n~+I`pm;+8N^laIMcrMh;hm^l z4B)I?&zP8Rf%$%z3k$PA+YP;&1;UtGH7;1j zTxi>IJkFjoYqT_D{?q|L%Y2Y4gJl&KC=NMf)j7!q3ThdvyFi7A-C^kh)3RW{LlDyjfVJrJ`Ze{wjS=S%0*sZMCk2jZM>R__DyqYqjUpv_n zzuyP>$VsJCn#!3H8M?(~5~QfIC>!O~hdU9z!XAp1qnfEAr1ql=If-k|_PnrW3yogI zS=;80@pIVTHf{-pt8h>?(_D&4{S9Liht|qT!Tf6DaAPrQ_NH2`s|6Vvc|vuCNZm=+ z#Yj9(4fw7s>jeR?jyyw^I7U~cwUi*|SYngZe6bLmeHgPBVe)bIxuAdaasOkUBq_6J znaWz35Rbp&naji<7uM$pBdl30FnNLV1kdF#bmlNHrz@>-#_Gk%@IJu% zAG-t2NV(@8MQL24_?o#8Ne<#7g{^4I0U3_!Ew&zjKvg~L zi^inG3=$Y}bLr#99|W+JMryY(h?*|!f!P$ag)@tHYZBl91#72Jf8CfYIZ~UxH7qGr zz!)J%(@TItQp2Czi{>p~PUVY)!n&MXfT*tQ7KqHQGPwqpxF?_)(?}BQ1rkyV_(c%S znIOvS5V0$WuLHTd&RdX+RRBwJHb?Xn)VL3Jm&)CIiYD;tahXhkzA3@|D69RO0<1>E z7Qh%{ATJiY(i(bpLNrJ(6Y6WEB9I>DUMroK!sclWC?4choy4(UO;Qq zOtD#Ptig*@uQY=N=b~*{9k;qsl`)g7Q>OW>R>RI%*-bSRH_zYxDQq%9E+$9|x!1b^ z8$h(p*Imt9Dik07-4G(&YmaK*rJw zhNrt5|(WvU8arg-X3K zz{c)cs{y)ncYP%QOH}!1tfUxxRg+f?wq&HAMKzaGy}SnKT3SN(HLVB9QLvUAb&RaF zL`qsq>zrjUpN%ji(~^pyQbNcnp+O(3(+gbmb6c+g!le@l9|sU#uF-fckXs44v}RxqfYJqkD*GD~13Ft3M(Zi7+>(|tNVUu-vsjn; zx;G4Hgc@pVsY*d`s!rAUvCTT*qF=%bLi*)ejinL0mQ#tB*9^SxE;>x9#1X{<-VahL z2RP&sT@qc(B(<@r>O&h-y(O}(c_E;_lg`a)rRPfDI~`s{2Nh*5hm5s|6cybKd-bb2 z{{*QdikG+cS;Puosq%WuhGjzVx7PvQHrJ#`NIp9BT$>9jDy*Gqj}PtEfz`~swF zwHvn!Y3OJF)u^~F9F>&Kpb3UuVK$t*et(PFgNffyirdqr1h6J<-+3dwyS#PXg;G?D zuc@mjriC&VTp1PgdjZg<&|{(}ZW6wboE@d&kt=fm{jKy8;) zw05|^YmD1$^^sJSIzkMPgmQ+YW(=#3+|p%(#ngHVm{2seMWJE~Q&A%cvy*b+%D8t| zQF(@jA?0LkbzB9>6=k=YWzn@@5g?ckrZ$>YY-Pnyh`oP6iw%8^madzUXO%rvimAz9QsJfli(Xvj z40fYs@oNGAGH9ITDY+Xq#Of*exuDo&)fgA6s+Jul2%=)jiGVn3HjgT=83?$8_;wJ* zWQw(5$Pt-1QbT5|a3a*Gy7l4)doP3nW~)9vSPoDA#KH2p02v9o$zoE)>#|eruD(<% z3X99W_apyWF^_i#G>QltN6A-LBuN4R<5~#B0@iL&?)5Q`cL%71ASxQwCPU5!D}@lf znmwYfV#@s0Vju4gsH;{j;7SB)xcZ`!1$_cTF}V<2`NlDjS9%jO)GW?NaB_s!&qvP1 zoNo?tVgUB2rauOXD!j<&YAo7X)((bFj6K@(Zwhs24$kwuMn4Sq1kRk_Bn6u4}PC~pMCb@NpgA|T{ zS>>J>K~qf7ud1ahTH|=5_2>n0lHq)!mk@8C%hPl|wtg=EwKi6F%Z8)4wQ~wPrE;yG zQ=F|)0egqLqCCbBf;T8W`Ji@#RSDxRXaaI!z~oMl4O=c6rciqO=fFLZm2>poVJ3s# z_*c9X;i{37TUHc=MUAP_U!dX%bLc4~A(tqOSW;VUe>Ek9o*3JGFBk|)Mh}v#`ZER4 zJ73jGR$gjey*E6mI5uJ`x2`!7vP&s>5#pS%WWbPOZz4htO-`pk-UzPTI>?QjR}$A+ zpl4Y7B$!)_B~_G?7mb_FRF<xEhF6xovbwir{$6t#{sRBzNtP%GJ~37tT^efTu2aj(vz$^-qr>sbaL zPTkxE4o=)Zu0|eint8v8KmRz@A|5oEoITQ;lpWlHzwN*MpC`!AsQu$@?F)=W0Zmxe$I#dzs{~Jt=?Xl>A-B z*JLh#cV~6uo2o|gETy(xCD*)8jZTtl)|FsC3#~|8na@IN^q?7wblrA1%hdScnD8`i z_+8_OiAawpxP>|+zqlmm{T@bU>|e^KfA-3}pMD<3&XnQ9$RwZkWp(?28S?(`u2t}2B)ULke@0T&E%Vr}%2^rKzZ z#8A1pUQiH2fS8JKa4AQzF)(f%ne7+4M-WZRq~XSXku+BoYdv%ZlaJp%B!6$-%4P)_i|A=&B)o$>LW<$@SqNDb+_^c%|MHzDi6~GNs;VBuK@F|Ni`? z#{6F~{k_-3fBO7;n=fbk?XZ_Fgux`mCkJWj{W|Yt*ER#12~irflM6X|InLP}Xil-{$$VkT~cyzw^g*MmP7PB(@LiUhHM_p$m?jE9=~YgS!O zlBL!c_B0LR0>13{UFo@ z^~h99B_LmoH{Kt=yM1j}FO@AHvHhN{c>?=p;D=&@cd5Tqy>;1bu!xdByHtZpaz0~Q zUjqMPTi*~WJmkWjtr`aaMYn*no>I5Cs-srrqOESJ0;x2$ za4Uf`S1_txvn*Xxk>H~DDZ5_Ki>)^X==M%7R!-Y`3lr;A{Oq!iEjH>qnp9007m`c8 zYTBpJ>VtZ?pMFzTen|iG@W1uTF9)9P!Gy1(3pY-fbXs9$oR&*AV%0WMn-{%=wJvuT zd*_eWT{HSzLTSPHep*zpvA~6(yrd zC7|RQ)l6?$U^A$^Jj;3fSH_d7ij3G2dvPj(7>jyOAxSY@Y%!}Xwoe?1{Y&G@88s{n z*}{e#G>GavuvB6PYBt90M1|L%LcRq0zdFj93{xxrl(qEjk+LQAgPWm736up{0lwN11K0$_b>3h0ZhL}zfmYbPE`RATTD#1axru1)or|t#4E4%o&ZZh`b9I$X6Bcp?Q&tas zqjbg}zJ3~!crFwSOwB(_;g$+gQj7`TbC9HS3CaRy(#Z#v06jpTI3$IqwoNCq-qW%LsXB~#wz>BN$sua{Xe4RrzBuNwVC zj>!b~>0FZujpM-Yl5O(ysdSTLq+BxEiB+B{CQHt#sFF31tncSOO|@_%W|0={ajTit z6`xMwScXilpSWQ-5xXeO2~aVunH*h^D$WAAjTabPwEBAn%KK-auw!(|v|?Kjs<9 zsZ_SnL`u+K0B=(Y$*w0M9Eq4q(lVxC?X6+L2Va5-UInfQ$5tTN*x#m|p?HYLNq(DSWMtjgzJ^dD^}VkDGyvP*H{)|L`S=xK8@qiiZ{vsozCEb6W(BhaD~!4a zs1)^Ud+=9!Yd6?<8`_y!DmMqMy6mA+@~VV`C(5p|n$&E3kc6`6*?wxjpOvpMG4{=& z0)x$5d~?nv&Z^TwPGFd$%ZY29bDzU zm8z{!lIqjyIWRE@L>6n=DAqx5R(zZ7SbC<2~zezCn&OLAD9;h*@-{C=>=al+uAWf4HFn9>i_>6du8FeZ6MC!D#i`ZB#XEhQc zNe}t;66+5qem;Bi!P@P|^?TI+dp>`9+MPw9v*4@RC1{c=x(2D+DAjOi4hbH{tQeZN zW*Yf|2D;!u=cZZS#n|@-4v>fAi@9e%9Gd3*`3bYqZ1|xXQRIyGELBt$Q}U+wgD!v; zEL27I`bIq%`f+RQ61@c9NTNE6H8cUFK)LGwt2#FJ;pHJrv;BptSQ@jmip|;Hvo0lQ z-WDfH$QQ=gQFHkW&z~9J$8DwuWcGlW(KU(Y6)LtrC0*3^a>cb32n_y9D z#ON?LgN;lJg1M$rn!0)+^#0YWKHe6^$NjaK2umm>^_e2%h#~s^`gk^(qpqNAl&90m%4tAvO7Rh?BUaYFNk`n+$Y-Edf3>d35F{DghQslc2 zAL1|d%isU;+XKeO&+YMl?*8t`J-lhR6dR$r;G5z?%_WVKZ-xq&;R|~-*k<;4`%ZYjz9iB z!}e3dy23gLVF!YJ@FNI*dX#66`U!;TB5#7g(-Pha!cSG#N6!m=&>OoCc)wf^eEcpO zFydYCDaU{RcyiQUr`Uu7$WyP@II-sx#=y|g{&&D@)2|9!&K_nt)QX!5M(49}wVg8Tn z69V`w$y<{_XDP05h@P@k7t0UY!p?@rz(jhL9m&!g(@t{&V|C=FJJ1Ckdw5z z)H<@GYC+h>R4FD>Q9CF327lI8P*yg!NS4c4? zp9*{7E;@|^X{+o$vkxw|5Jt>Sacg~LCxx7==wivXy5cIQsN88`;t97 z4vxI402c6p7;^9m*%=J~?SZKwpjsk1sEx}hB%6J)x#$*X21u3Z?%DXI{_h)o{N&c^V8o_8TV(2hIE48T&~lFzWJnAkA~jm)7JVGYzJZ*-d%W6ObR z;8-X%s|IPT+^X8aCc0YJCH7*wF6`^!D?NXGl4!e?@&Jb&z>o*`e8mkg$T=WTRvi}^ z)jC(dpH@vxal=$NWISBx zLtXG+*8rKVmgcK{+I~AJ5e7i~8Gx8zJgebD>c~N;&SRyb{;JRF-Jxta=cm%>3IOD$ zM6rZ5y3myAOfr^CDbz(oO@{yuhWi=J_5_!Cupi$S5G7HHWMd4;_(E8$P@OXMom#F9 znn_-v5zINMLys1U8R59{{RCnxWM5;YR;^krsyA$Q5d#}nh4=T<{%T}cjr;g!Aon4m zJxCTl*YF^nWxY58rB9BbVp0Rzr%K*fK`IGNIR+^GkpT7CCdLvena-L3Mfubj2q5Cb zmv!a8cE~enPpA5Bn$|xMDUF48=OD#NF_1Us7*4JKI={W>*lMI2s1<|kIZ;nFYM~YobmheW^BY*?FueSgSj0e9r&Li`LdYrmq|Qxg zqAE`9y;{@VN>-8SyMHv7 z6p8_$(uhosm^pC}fM{6KVTRKJ{d@aiE-cIfZA;Xztaw8Fq-)JyIR2HxZ6Uy^zhfNmxM+FKg5pWCLR0GBUG4=yG z*;hR;@z$CQn$8%$5r`&m>DjxcvGe31f&+yb5V=L*!*tI>)^+m)<`-DkAFkM~tk{n? zmttyfvbnsPGNWHR*%H5h4Dw+Jl3MdU?n=qCF{P8Q61KqBsUp7-;r)r=iyBej5~9(4 zq>gh@hXSxw=IdXvWxXKarIA;wNmc@?`z;PE6ze>zmoB=8a^rG0W-r3z zFna!NAgwK5?){>si=Ci`(=eU31~n#BT>7dTJwTnIx(hV~1Gr|r zHB6z05!Jg?Y3N%6F;2;P)|j-PK>|Z=E`98E8)$pj-BJuDW&+6KOUepF3FK)_0_>q+ zEeiG5jmeC0%A{PPi=qNP7Mnw{p+y#xU4<9TTYEm0&k_pja&iHpy0Tj!W^Yp9n%QA; zA#%&=#VE+=BK26viy)d4LF8Ewu`7tL1G&1+TaYUkwQel26qkZ=96e@Zjr0>pHG)^e zWjr19O$qJ?S?%8xU^N=H0Ipd9#AYpu7a_9D>>XCDNu9WicYj>avQ=wXR0YRGSPT?_ zBrd3bjuBYp%Z3*hPHHC5`!_v(p>y&9etJRPhE4!(N z;_CU^KZH#tfas}3G_jKEA!P8uQAPAIrQqz{zZ*hYv?Wmk)s_{!4IWG_&`MLoD>0b6 z8MpkKpyZv)f?_H@_!gVZ(Wv!Mb8)fM!bEB@3{ z=!9}5SV`r1UD*$S&&hVIMF&l~2=6BcDm16VX1_3f82?U;q^$;W+aBB-Qsm>slK zeN7d8(LaeYtJ4zFdNs-RHh-yE!uy?Es(Z)kJ;uTjoo_BCX}JYM2_olU&4zEfDbubB zG(b~(x|kYm>S6`T&3Guaf$;&%VYuihm0%x~mC_hoD~-YVs`oROV8~oL9iS$`3#oaf z2B|95rj|vPk{mYa`Og~_C8yEqDgZRn8XGW%JsL6vl4aM+(OQxk;$cDb!2o;)^KF*M zTo|AX8I2TD`_ENw#WokbT0pi3fZ(vD$&nhMb9dKQ0x(&qMm_ip_|)v8ic2x(0#rfC zR?e>hx|EjST}|s=aulp3M;#(-Es>Je(mH1u%qJrZE#(??7jrUdpc+!{Hi*jPYCgup zG@iwn$FiNT65c8~MjIru1n|l!gfSwsB~>&O>$x==uLW`|A(z$+%mGk3XD6gqn>xLc zp&+@8>Jy;Nm4eU7r=wY{%Y5A{2GlqpBc42Sp@8B|;gF5g-ZzTcdYh(kfR}4EmPYJa zP9>gSGw{B$juK#c)wto4=~ zM^$!4U5-%E85b%Px85Ji9vRbJIl!%mFfllA!FiXAB+k}mPLiscwa0V;EOfyepnP{_ zAke%;bwE6eQ`0??il?TQjRLQq!@0E^*9)oI?13U-RznSf@nntZmCcx`p@a3>jg!?L zO#FUS+#W9_fHiUZ&Kv37W?NgN9Ogy|AW#@^* zHlpk!xt6BgbUu2u(e^W=>{E1IFZyHAb*163EjFU-6Q3`xglWF78)g6WLYQ4;%g`fi zEzGW{w@1V5M_`_q<;k2+5Sjok|Y_t~ls!?)qV9|_-{3eZ!C%5YLB)N$#hB-Pj6+$ll}Eo{`wUjAg^-2nyl zP!z;w1DM7Y$duNkidqX#A*@rni=7jAe|LbAR~rXG9qSZ*YDFz$Y#}OaUUG{Yd7zg+ zVR&~yyWd=lLFwJ^yW|Iu8cGyYUJb`8pT5RP!z*p}8EO_$2%OxF^(e%tm@6uRNwRY) zgS`v6U{PNxmmZK;&&scbUyh7D*^TZGf&ld?bgMT@McCD*|7M907;5CdaWw-2l1 zYCWnfC(LRhM#J8j1h4HJHGfmc5NHY`7>npPO;M=z==ay!Slulf0$yv;0GSe|)}sL@ zOBculKF657n&QP_#v+Xvxc1Vx3x{WJ1bNw8vff)8QMG^00kRX~90*HH#PXU~4_x$o z;+ho&QDqWQ$>Al6Nv!?~mrO2L!zIE|O}UI4!h(OU9s_DllA6JxifL$LK_$S^1r9TA6xlMB)m}sl(2JUL7V*Yb6B(PRDWjtA?r~V-PMt-S2m1Y~GZ=h0cJt}r z;K=>Mn&083nRj*g^Y>H5-(D-n*(1Fb*xoJparf;%9w0xX_VWwbg?JYdngtsuhYWEfL;L@DG5^g5|Rs>D}#dB3;Yw%DB$y9_=CSk^|o# zjyfyoHrt~bCBea{Q|b1cDl28*E3}(_YJd39=D_xiGE!@uhI@27m~5>?d4m3_V_9lB zBxoU`lT=&pt}DPXA}}?%dmITm>y|KQT01ZPIeefq?yQ3QVx0Sgqj5o7OPlVW%HBP_ zI2$N6xF*@PX25#UzgECO^mmVslYpIO`r%ZK$TJthkI5yI{FS5fmygNc<@p-VwCmQ`}itHJ0fxn{NhyIE*O;_`eJTB8TeSfuN={aL2=3WtQJal=2gXPAg| ze}r48GxCc|g5FhOWXArbJpQxSzy0uO7&}vj4rHu5mqFp3(Uyal8ge?6_oEY>_9=>#BOGw671y9VT7lFUXv z1o8=0LmtKR-TA-2x8L_9jQMbYkg)sfXKVK3y*x4ECCwwSOOwJ13xE?L$~A|D5MmYZ;XMHahLhSyeJ z3-}=z)?X6Df~2HQpk^gGX;7@^wtj&AdhqAM>B=wxE>WlfdJ_$`s!MQBp|z}hk6_DT zLFvJswg-?8j6Rb5+XE<0`n!GAX9z{*G^)xhF(*seaN|YrYa*%@#8J3FIVDTw;7IOdd+9JLR4-#&Qnwf08o(Xi^Cm;|aaD;Mr!xTGMN z-~vX~Yjq?`Rbd!R_CYKg^fffas2V;lo@ZjcW(7WrT6sXNG|yzXHk(LoW<`r4r{SG? zxR1XoE8nI6z5BoV<>x(5cW=U1(IxrT#YSXytV_rNyfRc!tD#8-Uh5@yws(Gi*){9p zAcOLePioSno-k%0U@aJ>7|3_=*I(yYgy@B!WgBh4Rz>+d5~cpWwsSa~=JD!(L0na;!T6@?H3ieu z0o1)^vb8D{o#$w`dFs_s$d^F>S4TMpfMyz~MdwR(j5=bZ%QP#} zf*ea4;d#=?jeOsNd_pZC1xSu1VeD2jGR(@IPRZAWz`yOEK z%|~wo7KK+|d19O}SKOz0Jl^ zjw$t5_L)jnEl1msR@=0{{lMU@2T(W4eV3f8LMiDUVTsurBIvIzb*aA?-K1k(*w4yF zxsmH48_gGPT-83KCP^(@8@#yW2^=)FR!)8=&W&7OgLhHk|(^hq*WIc{BGwkZ5htP40qiR()tJ-qivuE!lWNx!8??{;e4Z#bGEa za$+qOs(Kt5EjTplpFx>kD!p6%Fivmr-`P(UOsO0bM~==|PSNGaMp@C87W3VQBR`+L z`C#q#{rWxX|2@Z_9-gA^2qkl+zU%^kF}Wmaz!!40Qs^C)b{s(S)=VQ`&_Ea5>)bTU zyBPc4z#j5&eEs$8heOkxKR;krnhihfuXL8cYy$P%_+Ir#r6Bd3P{!_rtZ&r4q3^fG z=Au3#QWaZVZYFV(T*#`e#;pd!cP|eSa;U}FYJE}*uNEIHgdWdFl`t$`3HibpPt;sK zW9QF|Z@o6t13Y`c%;;*9lTKNyrVOj$Vp6EeX;O(p2&vu8aI_6psyPN$q!`K>B~fTe zJmeCIODG#Y-WJ8j{k51VLNm^hNT|KdfZACuB-P%id>9mjb@HCYk@s&|-~R(|qoc7Z GyZ`{8A~NUz diff --git a/examples/mergesort_queue.mlw b/examples/mergesort_queue.mlw index a3fe0b55f..516f572ba 100644 --- a/examples/mergesort_queue.mlw +++ b/examples/mergesort_queue.mlw @@ -16,7 +16,8 @@ module MergesortQueue type elt predicate le elt elt clone relations.TotalPreOrder with type t = elt, predicate rel = le - clone export list.Sorted with type t = elt, predicate le = le + clone export list.Sorted with type t = elt, predicate le = le, + goal Transitive.Trans let merge (q1: t elt) (q2: t elt) (q: t elt) requires { q.elts = Nil /\ sorted q1.elts /\ sorted q2.elts } diff --git a/examples/mergesort_queue/why3session.xml b/examples/mergesort_queue/why3session.xml index 525bea63e..62d0c1841 100644 --- a/examples/mergesort_queue/why3session.xml +++ b/examples/mergesort_queue/why3session.xml @@ -3,276 +3,265 @@ "http://why3.lri.fr/why3session.dtd"> - - - - - - - - - - + + + + + - - - + + + + + + - + - + - + - + - + - + - + - + - + + - + - + - + - + - + - - + - + - + - + - + - + - + - + - - + - + - + - + - + - + - + - + - + - + - + - + - - + - + - + - + - + - - + + - + + - + - + - + - + - + - - + + - - + + - + + - + - + - + - - + + - - + + - - + - - + - + - - + - - + + - + - + - + - + - - + - + - + - - - - - - + + - + - + - + - + - - + + - - + + - + - + - - + - + - + diff --git a/examples/mergesort_queue/why3shapes.gz b/examples/mergesort_queue/why3shapes.gz index 804f1a77495e27b57bebb3e38e087fb615caa15e..3efa5932ea2f57ff1967e2f9e33dfe6dbf4ea062 100644 GIT binary patch literal 3833 zcmVgH*&9Uqp~0GbT>jBq&2wUzt+jmTREY64ne?@%K8o z!G9Wm!}Qw?aQ%yLi3wxTjKPb!q9!O53D6N6U)|iqKkL^&{`q~tc=Ng4{NL4I{xaVB zYy9@*>-Sm)yy=(Ro%xT=75(v_|L6Pv4!k)C_nx6&H#h$^yJJ_~jba|db}--u-gYnz zZhTJ|pug!K^^g902-8t-bk}$1aR8cHY2fJy@6Jyz2W~zL^HIO_uCu@P^V@zg{_V@> zZ-d3(ZhpW1^tU$to-Ygo$glHXHUQsUJq&bx{p)Y@8Cu+RAWqO(9zRl^eRR6*VJlGI z5d?Q)@-R%I>y2P{0`-3IIJI^$>U8MuF4#!a=0n;x>O!P;AW{gcGVP=EycH^h!P7>n zydzbQ-97An7=u7png3x30XIZK1yAfgxH{`rhfgA)UPA;>k9P; zH-yPbLKp931-(@#GYLHgoy;W6)ZZI*VI{h?5?!T!J+u;Cw-VJMEUZMs5MD_Az3I~t zpEz>zidbX_8(HWEf4vbWq4Z(d)M&F%!tLpe4_qUT>mw@iW9Nq>F*n$xAnQrMbkswp zyOEe5Y*LTm;HD#gdwLV>Y~$7Ws9$*4wg_!*b@NNkM#dRkNt$Z$MZr>2N=`6)$ydLB z`SR!0&F6o`uQ&1Y_kMKq{pGy|mn&<^sdtpnA&P5^H8l|j&e3YGV>r0c6K&*xT?~)v zlCWt>9zr#rvIS%eB}gibNJ-aUbhk@*VwVanXF=rF<07`;eUYZvawnx^fmgeH0(c%Z z2#63ZLZjTfj9OG3_-sxgutKd@e}1j`%ja_Q{pQQ(eMhrmd!J5Xd}FqA$LF)#o(*r9 z%x-IS4;$U1L{XCS)-3lIC!bS}B^fbux#RvGy_lqBt_Htv1Xp7RZ|=Rq#S^y=^BKylDb$e6)Tb09NOFwHhhiEM zB$0caoEokpVi9$fc3P|;iZ^VT%RZZ6s#M4o=B#e0M%p_(x_Fa5Ws>I*g! z78e5gr^R7%vdQp^hEEopRdkw}N^9bUYAoH+`BXzyAEU&h!P$XK&M-Q|Xsu+x3Ytn_ zDF(hpaa~*mjmy!=y#o*~){qWR_sY^-h>VsZ8zI-PffiD6s#aNjGU0H zki?)p=B=R}&j;?S;|SZuyo0>zKn?bO)UYdS+L85m+IL%@ZJuYEI1#@~77NiiaxGg6 zh)GSG4^BJGMIV!Tz}ouYVtMc>RZ@$%$sUTE?gIkgQ;-1kj-ap;ebG+zHJW7VJb=h~k5YB+M=ciMb|MQulRIbB_%4I4vBBXf9azcvuM8tT=+M`+(XJ z0U?&eJr#hO?YT)?cX0a^D;JOP!8}I6SaQpS&4(DU`V?b}m=ojxIm6SE!_!qtU4Zn# zfE2`cLJ>%*a?Fydq$cD-_N1;T9!;@+yJQ5X%m}a)Pn@ho7h+>z2bvv6LEQ=my z1TX$>;vTbHTRpoU2^YJ39>JH!wR&n^Yi(fF%opD_^iqM zB1)r^cQHkzW--PZT1YI|f`71<=(Y003m9G_Dex(`j)oYB#)^#YAB0tNGz_9OJUc1a z|CaCKG(MWsuw=PA2M)-^Vm0iUBWLrNRGQQJ%+j3~e^PWo(nmv5&ZSAPrq*&~b)mbQ zrcnfhLqmIUS@lwOA8=*L0TGVHLM8V6Ta;5IRBu#6^a_s()!%Ea_32dermL$xWHPR; zS}i3dF15Q&6RF7px$?l|**h=5KB0=deohp`8`u}F&rLhhOGdnoPt z$yMYcdf#HL#S3E&rDU<_T#7x^=;m}rrP^o0d)fP*3{>x;4_aG@lrg2Os9byx3V-7I z?K9CZD?4%_sfnjnQp7x#iecdxg8}@QqV5kKv3XJKuEp0X);wl*Jrp1f1$|U}z}Fl^ zY#*S~`%J)&h?NppDP2vqwFG(mimM@K)UMO_5F@--y}fC{F)4)*QqEd2G?&bWDxtO3 z+d?`1WyMFV2|p9PaiZ=`xKPC4F#$ztIdExOg5w6~UMPMhv?<-sQK%(hR*qT=9PbcEHD?ay?yhU>nkZ;(D}@%ahK<4r5lL$ydD8+!7B z+$bq~(kWgF?NezlB<=h&DP&{CZC`F?^ zzjozP(0+~%hqI=T9cM2@ahy(4$3y_BO7TjUD)$SzUO+~cqYfz7Lf+Oeb$fYdisbR+K zy7i*7pfP59;&-!`BKh+RIE&NTTu^DvaZ1`OK&#p~mKs?f{J)Qv%K39gND|>JF?kOf zC}qSV1f}H6T+og?nM*nSPv>)LRa9Sv#7E(pc>J%jO*4Qet$eAmzrgE7bMO^Pt`TzS zX^FP6s4M%d0jPD)1?}q3FWMTO358wq*rJn?LTE`NI8DXXKy2hnyPCI*bAwxZj=M8G7$5gve_u5Bzvp{lc{9wi z+2NJ`j*CmSFSl(Ci@iqf<}{|q*y6p%9XK}3I8V+@2X2S=HjVRRy6J8EI(!Ttf6T!y z7NeGzl9D@->^-$JjCZ$G;rLx0S0$4RDSVL zLD$C0N5=|!e6S;X^57QUYO$ru|d}9>K9xxh1=lQ#|49j#khPAQ#a$1onguDsB~{ovO6Z-8`2iqkARe{Xz6jg zQFT1Y;I0pz==ZzDm2TZiw|>6i=-x3nlGb9cwL4kwQQ$szyA0RAXto$Fv1{y#W3pR9 zRC0voH9v7961d%p#O?RIK*rAByF=kr$4sK2B#N#(F{r2nXq8A152{sfhq7->`-1k5 z6!c6^{&|D1Eh`{&HX18!m7-L2sYr~P#tO2>6%Tb7@4}jQVJ-K-`e0Um4PR^ILyy51 z-8yo20I0`FroTM5T5DwS!Fdj18REFvjH_8S+#?y?lT7!ZyQ0xO7IOP6wAgiOBFB3+ zo!SZI!vo6;XRWKAwL|daQuNj}rlC^kgy37JgTmE4FQKR$gEnNAOCMlrXCGMYYJ-EtUUDZyblr(UW@Aa0-Uo0PIdxeoQf9GR#L;10!G2u zf13Bt_Gj3I>^}W=iB4Wuo7uablYmdP_8%=pbKVDED3b3X%Zq%?+I#9TPlFfzzjmzA zI0+Y%)C{C1Rz~qCNUmT`4}G1zQR)L;;G)&n)v7C{8?;$YmAhWm7r~Y(CLOolvTzl@ zbt_)l@J1?UEtV_|OQMpS#uOwl5eh)%QX%CE3$g4^$BrGlPd}BkDg<)cAVEx}m`O;r zNQojLb3%EL6&^Wt{!~SNcR;8dmC}ez`kjHhQd3{2!FR~v~ zAhzU;6E%pnk|av5aWz13R^9Gi&4*Qci-dr8R+PeGO)XqsG;qHLLU&Y{#*GCK3D^ar zv7oZXB9L_4acFH-)fVf4wq3{D4oVkVvh7mlMRg}sohVffO&vpPq8PjbZiKM`i6dSK zF^;YF9xj95O`aO08soS-a_lg1R3ejsaTUk}_bj{btTumoN&mHu+W@!NBjJ8%v9yv2 veQX@TFr=%~bdx|qoH{`*#61nm(0u10p^QRJt`=|hqK^I_6oV>WAdUb4bL3|N literal 3833 zcmVVyA zYKs>O7T-Qi>Gt;R8TIlq!Vkk|0!ZJ!ka=wAJEb?j3x*y17Yz zw6DMa^ZP*Q=5xRK_tl^OJivgzq;Froes6W48@pt4<}ceT(r@ka|9t=7fwu?Y&NKd( z?T`Oj;M7%{QOsl54F+N0T?fUf{w;GyB>Ce_AvO#LcEE0vH)wP$wa(~e=-qITh6gY zT386}EQEB8bm-VZXx&1{?08`zWa#ks^Uf@2p5^mj3)w$}@BNP?d>#qkuP{F2z!T2d z1U=z+Y@LA4Ci4mCJX8MIxWG9taK6gQ~dzD)lQ4I+=vd)IT;(7NIogw$n35N z)P+e%9Q54OuRoIdb)q5c3vn5-n2cqc2cR-McwSPVLuNtmhM8g*eMy0a2prG7oO z5?!|v)gdgbM8goCN&VLJ>4Z-lIeA4aGK8%xbc;W0q)8|?tT;8sSt#N5^wtNi5y$lj z6}hqV!d;-sKxNx*buA=73g(G77@Pox2+BX@gx8|>`j)%nOSJZ@WrHn+O@Q=`gM za%haHW+_gK4@8BMYAYJAe*5y}kE@%{|4LtP(&z7Xbo2fBy+-2dO9-vz)T>uimlMX2 zTlbw?TJ3cV2e*3iTRD)4;Xz%No*W3~NFiE(xwbA1pkQJz4)p71){0;e%U6*c zx6IZrreq1MO5^pXd<1wNHi%9sS_s2r`qfr|vn3JW3mK(Z=(%;n;(as*%&^L1LGL$wLG$T^t;F^sU{S9LSw#9+(?kl=%c@ z`jAuc37WKS%8OK86BhxRDYuk*M|i}mBC#BBC$^6fGo@xhQz5djsrBqUU}X*DqXm-? zLw#J#w8+uVh*sW1>uadyRUsT&Fy(m2HgwT8rc=F<52BQ*Yj_K;`wgh*HT`)KF>=YS zJH(tExz=LSP%J~tv6cKN75R&bet?QfGFofF0$vBbSisf0nN%VX=33I}0Qf}6B?nJ> z;k|S5UKUH>o9{tm5>%gEU}f>9GVjfyKQ0cFvrUFyG<-G{^LNNy4Q&mvcOK91n z>8YL$g^8Kk3=guM?OmqHMp82H1sZ;w?<~HavE}5930hggxzA^QC@YVhWK{WurF)B zC+qRFGh3f+o@bgkQ=Xk$aw!Fqe`Ikk8?PgHY#=R{1`kO+aBY2Xu{`*gDyc=>6z_|h z?g9eRV~~LU4MAZq`tp0x*Ld2VZCl6|W+>>Hpa2E}jjlurR718=8a zPY7C0)53{}=7NRyhlN^83j~USp~svpyJmA5WKpBJ2{>9|eOS_F4(_mG<>E2kna2?H zVqse@Sx1l2ye0L%pv88<1r6zO$>I4br7l2vXFy77$g%hX5nO07Fi;3NAQmXtGo4Ja ze!XM_=gbJQmKu_;EqO}?ID4;}n#x+Ck2P^@?D(9dvh9D4GpEo6p0i9_Sjn? z#|g_=(ST1Z-FfyaMHeK!J0yihp-FF;efCvbwbY=y6k6AU;-6hsy_DTMT$$<#J4Oe| zflJjjaui*qk}`;S>C-baNAdaFs49HF~TyR7@?6iz~(V=A0=Dvov&gT19WX z0Q-z8deu5$uT@jT2qjxkL%os~X|dD{LG)c$Wq%MAX|K6q;8ZJT&lIR+?93KrXz%6p zYYgwJRQrSQUJJ$2!|0^A4CbLcNKQiLuZkjVi|c>N`t1**;RFpRHH^)?njNSV4Jp=G zsCn1pk16VY=Mh_KrI)A`qPBucof`wx({Vl`@Z&h!vT5wEk;ay@-F^ZyGUFcoAIPGNl(#NX_{~&tv&5N%{mif2J z$Vnu)@eNixQDZyJlOLc^{DaV@hFoGtsR;lffMvcNSThuoUgIOD0zZEB_y0u)QKiOOo$6iNAv|}2^PR_r9ush;I3`GxIJL$lJM&)+fjym`?R=p+^Ye-L z)r!w8kaL!ocJm{?R}15WrK&}CxoWR?&&#N9xYXo~0?3{go!45g@NwngEf7 zNPk?@v9^V7%uhjZvh~$X~C7*<-i?8yg;?g6;YdORt^@mc=GF?$HrF5RMx+l-Pr}GXWl%lU!=-FYwxf*SJS~=axkwv4u6%)!dbO zQDT7-um1S*?faaS%pD#-`a55eOF&}5U8Q6^EZjV4YL&7zcNYsB$YJ$MX&+7~&0-gZ z7IF$feKx-FO0G*INX;d=nm-u_1FYQ#Hl~N;?f(1ki)QhI|$uw;K!dN3&2ACn#oX$S2GKuT7$^sui{8J=W->!Ulm z!)|G%TUhDV%|AH#?HC$KYw@kMjjRtS@Q}Nq;PsybvQiw^nUJ_Br@~a#0{E6$T;#`n zhy-sxMFNLCFOaeK|Nc-4mOk#)1i6KPY)M6AqiV|3Kzcr^db}OVp)nl_+C5OvGda1Z z4W2O8UP>-8QDav)<|bN9p5|kGOb;s_G8pf}n)hKXcfk5+R(=g%Yvkh}f-isT$l(Z3 z50i{p7;-4%`?T5vR;uKQx@hfCbGU0GN(N!b8w~9s+sKL*V>LFx}J7 ziy}t%5FmHP^^j}j1Gi|Y9ToDT<_Ak->GqH)y%i;laz1Ssr1`tj@W zPxWVHLWWPjUZRs1)h1gMl0wbIv8oTvQOW8OatjLSp51%y^EGSFsi!;*UG)Fb`fnAm zNUSwth8C-n%&AAtK{%xcx&gh%3tY7N!p^;A%aaizI8_c7Gsf-SwIS7Udy*UzhtR?I9QJ0>j;r<-2?6h|D22tETDZPw;KV#8)oKxldL%#+MX(su z)#QXhW25y|)woy>jJtKb-Jo=#rMO$lyr}Mss!Jt1^P5If-Kfb`@PyfW*O4;&(ql%iy=YSQa9YqopJ<*Oo$ro{E_$DMe4D>j2qXZT|F}{>eoe_iT%fvr#lyrex_7 vmOwTRRCjfrZek||p(HhOaS2L?G?tKJj;$t2SBocmR!9E - + - + - + diff --git a/examples/sorted_list/why3shapes.gz b/examples/sorted_list/why3shapes.gz index 55833d86b6f7b41d200ffd805c2d6a8e4065db34..d5ac3ba725ac3301519c7a2d3df3245c656272fb 100644 GIT binary patch literal 186 zcmV;r07d^FiwFP!00000|6Py43WG2ZMDP6yKOq~9iO?2A5WILQd*A2=0#&KDw4YzK z(UzW;ogLoJNI_CHoHZ;h*i<`W&7c#hjf55`s;T1+1r+^Q`#-V$Eq6Bq#i0A6!ZFaQ7m literal 187 zcmV;s07U;EiwFP!00000|6PyG3WG2ZgztR{A0eAR6KD$}2wpsuy~q4Opeogt_VKGW z+S1dqv%|MD0u0r*6)6j{ pq6`adHwa{Fz$eb!k9eLDbpN#(7j11a8@FmpjW@L7zNi=h0012dP$>Wa diff --git a/examples/stdlib/list/list_Permut_Permut_length_1.v b/examples/stdlib/list/list_Permut_Permut_length_1.v new file mode 100644 index 000000000..2e2efda0c --- /dev/null +++ b/examples/stdlib/list/list_Permut_Permut_length_1.v @@ -0,0 +1,156 @@ +(* This file is generated by Why3's Coq driver *) +(* Beware! Only edit allowed sections below *) +Require Import BuiltIn. +Require BuiltIn. +Require int.Int. + +(* Why3 assumption *) +Inductive list (a:Type) := + | Nil : list a + | Cons : a -> (list a) -> list a. +Axiom list_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (list a). +Existing Instance list_WhyType. +Implicit Arguments Nil [[a]]. +Implicit Arguments Cons [[a]]. + +Parameter num_occ: forall {a:Type} {a_WT:WhyType a}, a -> (list a) -> Z. + +Axiom num_occ_def : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (l:(list + a)), + match l with + | Nil => ((num_occ x l) = 0%Z) + | (Cons y r) => ((x = y) -> ((num_occ x l) = (1%Z + (num_occ x r))%Z)) /\ + ((~ (x = y)) -> ((num_occ x l) = (0%Z + (num_occ x r))%Z)) + end. + +(* Why3 assumption *) +Fixpoint mem {a:Type} {a_WT:WhyType a} (x:a) (l:(list a)) {struct l}: Prop := + match l with + | Nil => False + | (Cons y r) => (x = y) \/ (mem x r) + end. + +Axiom Mem_Num_Occ : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (l:(list + a)), (mem x l) <-> (0%Z < (num_occ x l))%Z. + +(* Why3 assumption *) +Fixpoint infix_plpl {a:Type} {a_WT:WhyType a} (l1:(list a)) (l2:(list + a)) {struct l1}: (list a) := + match l1 with + | Nil => l2 + | (Cons x1 r1) => (Cons x1 (infix_plpl r1 l2)) + end. + +Axiom Append_assoc : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a)) + (l2:(list a)) (l3:(list a)), ((infix_plpl l1 (infix_plpl l2 + l3)) = (infix_plpl (infix_plpl l1 l2) l3)). + +Axiom Append_l_nil : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a)), + ((infix_plpl l (Nil : (list a))) = l). + +(* Why3 assumption *) +Fixpoint length {a:Type} {a_WT:WhyType a} (l:(list a)) {struct l}: Z := + match l with + | Nil => 0%Z + | (Cons _ r) => (1%Z + (length r))%Z + end. + +Axiom Length_nonnegative : forall {a:Type} {a_WT:WhyType a}, forall (l:(list + a)), (0%Z <= (length l))%Z. + +Axiom Length_nil : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a)), + ((length l) = 0%Z) <-> (l = (Nil : (list a))). + +Axiom Append_length : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a)) + (l2:(list a)), ((length (infix_plpl l1 + l2)) = ((length l1) + (length l2))%Z). + +Axiom mem_append : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (l1:(list + a)) (l2:(list a)), (mem x (infix_plpl l1 l2)) <-> ((mem x l1) \/ (mem x + l2)). + +Axiom mem_decomp : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (l:(list + a)), (mem x l) -> exists l1:(list a), exists l2:(list a), + (l = (infix_plpl l1 (Cons x l2))). + +Axiom Append_Num_Occ : forall {a:Type} {a_WT:WhyType a}, forall (x:a) + (l1:(list a)) (l2:(list a)), ((num_occ x (infix_plpl l1 l2)) = ((num_occ x + l1) + (num_occ x l2))%Z). + +(* Why3 assumption *) +Fixpoint reverse {a:Type} {a_WT:WhyType a} (l:(list a)) {struct l}: (list + a) := + match l with + | Nil => (Nil : (list a)) + | (Cons x r) => (infix_plpl (reverse r) (Cons x (Nil : (list a)))) + end. + +Axiom reverse_append : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a)) + (l2:(list a)) (x:a), ((infix_plpl (reverse (Cons x l1)) + l2) = (infix_plpl (reverse l1) (Cons x l2))). + +Axiom reverse_cons : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a)) + (x:a), ((reverse (Cons x l)) = (infix_plpl (reverse l) (Cons x (Nil : (list + a))))). + +Axiom cons_reverse : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a)) + (x:a), ((Cons x (reverse l)) = (reverse (infix_plpl l (Cons x (Nil : (list + a)))))). + +Axiom reverse_reverse : forall {a:Type} {a_WT:WhyType a}, forall (l:(list + a)), ((reverse (reverse l)) = l). + +Axiom reverse_mem : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a)) + (x:a), (mem x l) <-> (mem x (reverse l)). + +Axiom Reverse_length : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a)), + ((length (reverse l)) = (length l)). + +Axiom reverse_num_occ : forall {a:Type} {a_WT:WhyType a}, forall (x:a) + (l:(list a)), ((num_occ x l) = (num_occ x (reverse l))). + +(* Why3 assumption *) +Definition permut {a:Type} {a_WT:WhyType a} (l1:(list a)) (l2:(list + a)): Prop := forall (x:a), ((num_occ x l1) = (num_occ x l2)). + +Axiom Permut_refl : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a)), + (permut l l). + +Axiom Permut_sym : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a)) + (l2:(list a)), (permut l1 l2) -> (permut l2 l1). + +Axiom Permut_trans : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a)) + (l2:(list a)) (l3:(list a)), (permut l1 l2) -> ((permut l2 l3) -> (permut + l1 l3)). + +Axiom Permut_cons : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (l1:(list + a)) (l2:(list a)), (permut l1 l2) -> (permut (Cons x l1) (Cons x l2)). + +Axiom Permut_swap : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (y:a) + (l:(list a)), (permut (Cons x (Cons y l)) (Cons y (Cons x l))). + +Axiom Permut_cons_append : forall {a:Type} {a_WT:WhyType a}, forall (x:a) + (l1:(list a)) (l2:(list a)), (permut (infix_plpl (Cons x l1) l2) + (infix_plpl l1 (Cons x l2))). + +Axiom Permut_assoc : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a)) + (l2:(list a)) (l3:(list a)), (permut (infix_plpl (infix_plpl l1 l2) l3) + (infix_plpl l1 (infix_plpl l2 l3))). + +Axiom Permut_append : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a)) + (l2:(list a)) (k1:(list a)) (k2:(list a)), (permut l1 k1) -> ((permut l2 + k2) -> (permut (infix_plpl l1 l2) (infix_plpl k1 k2))). + +Axiom Permut_append_swap : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list + a)) (l2:(list a)), (permut (infix_plpl l1 l2) (infix_plpl l2 l1)). + +Axiom Permut_mem : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (l1:(list + a)) (l2:(list a)), (permut l1 l2) -> ((mem x l1) -> (mem x l2)). + +(* Why3 goal *) +Theorem Permut_length : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list + a)) (l2:(list a)), (permut l1 l2) -> ((length l1) = (length l2)). +intros a a_WT l1 l2 h1. + +Qed. + diff --git a/examples/stdlib/list/list_Permut_Permut_length_2.v b/examples/stdlib/list/list_Permut_Permut_length_2.v new file mode 100644 index 000000000..f599e911d --- /dev/null +++ b/examples/stdlib/list/list_Permut_Permut_length_2.v @@ -0,0 +1,175 @@ +(* This file is generated by Why3's Coq driver *) +(* Beware! Only edit allowed sections below *) +Require Import BuiltIn. +Require BuiltIn. +Require int.Int. + +(* Why3 assumption *) +Inductive list (a:Type) := + | Nil : list a + | Cons : a -> (list a) -> list a. +Axiom list_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (list a). +Existing Instance list_WhyType. +Implicit Arguments Nil [[a]]. +Implicit Arguments Cons [[a]]. + +Parameter num_occ: forall {a:Type} {a_WT:WhyType a}, a -> (list a) -> Z. + +Axiom num_occ_def : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (l:(list + a)), + match l with + | Nil => ((num_occ x l) = 0%Z) + | (Cons y r) => ((x = y) -> ((num_occ x l) = (1%Z + (num_occ x r))%Z)) /\ + ((~ (x = y)) -> ((num_occ x l) = (0%Z + (num_occ x r))%Z)) + end. + +Axiom Num_Occ_Positive : forall {a:Type} {a_WT:WhyType a}, forall (x:a) + (l:(list a)), (0%Z <= (num_occ x l))%Z. + +(* Why3 assumption *) +Fixpoint mem {a:Type} {a_WT:WhyType a} (x:a) (l:(list a)) {struct l}: Prop := + match l with + | Nil => False + | (Cons y r) => (x = y) \/ (mem x r) + end. + +Axiom Mem_Num_Occ : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (l:(list + a)), (mem x l) <-> (0%Z < (num_occ x l))%Z. + +(* Why3 assumption *) +Fixpoint infix_plpl {a:Type} {a_WT:WhyType a} (l1:(list a)) (l2:(list + a)) {struct l1}: (list a) := + match l1 with + | Nil => l2 + | (Cons x1 r1) => (Cons x1 (infix_plpl r1 l2)) + end. + +Axiom Append_assoc : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a)) + (l2:(list a)) (l3:(list a)), ((infix_plpl l1 (infix_plpl l2 + l3)) = (infix_plpl (infix_plpl l1 l2) l3)). + +Axiom Append_l_nil : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a)), + ((infix_plpl l (Nil : (list a))) = l). + +(* Why3 assumption *) +Fixpoint length {a:Type} {a_WT:WhyType a} (l:(list a)) {struct l}: Z := + match l with + | Nil => 0%Z + | (Cons _ r) => (1%Z + (length r))%Z + end. + +Axiom Length_nonnegative : forall {a:Type} {a_WT:WhyType a}, forall (l:(list + a)), (0%Z <= (length l))%Z. + +Axiom Length_nil : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a)), + ((length l) = 0%Z) <-> (l = (Nil : (list a))). + +Axiom Append_length : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a)) + (l2:(list a)), ((length (infix_plpl l1 + l2)) = ((length l1) + (length l2))%Z). + +Axiom mem_append : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (l1:(list + a)) (l2:(list a)), (mem x (infix_plpl l1 l2)) <-> ((mem x l1) \/ (mem x + l2)). + +Axiom mem_decomp : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (l:(list + a)), (mem x l) -> exists l1:(list a), exists l2:(list a), + (l = (infix_plpl l1 (Cons x l2))). + +Axiom Append_Num_Occ : forall {a:Type} {a_WT:WhyType a}, forall (x:a) + (l1:(list a)) (l2:(list a)), ((num_occ x (infix_plpl l1 l2)) = ((num_occ x + l1) + (num_occ x l2))%Z). + +(* Why3 assumption *) +Fixpoint reverse {a:Type} {a_WT:WhyType a} (l:(list a)) {struct l}: (list + a) := + match l with + | Nil => (Nil : (list a)) + | (Cons x r) => (infix_plpl (reverse r) (Cons x (Nil : (list a)))) + end. + +Axiom reverse_append : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a)) + (l2:(list a)) (x:a), ((infix_plpl (reverse (Cons x l1)) + l2) = (infix_plpl (reverse l1) (Cons x l2))). + +Axiom reverse_cons : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a)) + (x:a), ((reverse (Cons x l)) = (infix_plpl (reverse l) (Cons x (Nil : (list + a))))). + +Axiom cons_reverse : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a)) + (x:a), ((Cons x (reverse l)) = (reverse (infix_plpl l (Cons x (Nil : (list + a)))))). + +Axiom reverse_reverse : forall {a:Type} {a_WT:WhyType a}, forall (l:(list + a)), ((reverse (reverse l)) = l). + +Axiom reverse_mem : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a)) + (x:a), (mem x l) <-> (mem x (reverse l)). + +Axiom Reverse_length : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a)), + ((length (reverse l)) = (length l)). + +Axiom reverse_num_occ : forall {a:Type} {a_WT:WhyType a}, forall (x:a) + (l:(list a)), ((num_occ x l) = (num_occ x (reverse l))). + +(* Why3 assumption *) +Definition permut {a:Type} {a_WT:WhyType a} (l1:(list a)) (l2:(list + a)): Prop := forall (x:a), ((num_occ x l1) = (num_occ x l2)). + +Axiom Permut_refl : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a)), + (permut l l). + +Axiom Permut_sym : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a)) + (l2:(list a)), (permut l1 l2) -> (permut l2 l1). + +Axiom Permut_trans : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a)) + (l2:(list a)) (l3:(list a)), (permut l1 l2) -> ((permut l2 l3) -> (permut + l1 l3)). + +Axiom Permut_cons : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (l1:(list + a)) (l2:(list a)), (permut l1 l2) -> (permut (Cons x l1) (Cons x l2)). + +Axiom Permut_swap : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (y:a) + (l:(list a)), (permut (Cons x (Cons y l)) (Cons y (Cons x l))). + +Axiom Permut_cons_append : forall {a:Type} {a_WT:WhyType a}, forall (x:a) + (l1:(list a)) (l2:(list a)), (permut (infix_plpl (Cons x l1) l2) + (infix_plpl l1 (Cons x l2))). + +Axiom Permut_assoc : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a)) + (l2:(list a)) (l3:(list a)), (permut (infix_plpl (infix_plpl l1 l2) l3) + (infix_plpl l1 (infix_plpl l2 l3))). + +Axiom Permut_append : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a)) + (l2:(list a)) (k1:(list a)) (k2:(list a)), (permut l1 k1) -> ((permut l2 + k2) -> (permut (infix_plpl l1 l2) (infix_plpl k1 k2))). + +Axiom Permut_append_swap : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list + a)) (l2:(list a)), (permut (infix_plpl l1 l2) (infix_plpl l2 l1)). + +Axiom Permut_mem : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (l1:(list + a)) (l2:(list a)), (permut l1 l2) -> ((mem x l1) -> (mem x l2)). + +(* Why3 goal *) +Theorem Permut_length : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list + a)) (l2:(list a)), (permut l1 l2) -> ((length l1) = (length l2)). +intros a a_WT l1 l2 h1. +Require Import Why3. +Ltac cvc := why3 "CVC4,1.4,". +generalize dependent l2. +induction l1; intros. +destruct l2. +trivial. +cvc. +pose (h2 := h1). +clearbody h2. +specialize (h1 a0). +assert (mem a0 l2) by cvc. +apply mem_decomp in H. +destruct H as [l3 [l4 H]]. +assert (permut l1 (infix_plpl l3 l4)). +intro. +cvc. +cvc. +Qed. + diff --git a/examples/stdlib/list/why3session.xml b/examples/stdlib/list/why3session.xml new file mode 100644 index 000000000..c7a0f64d0 --- /dev/null +++ b/examples/stdlib/list/why3session.xml @@ -0,0 +1,465 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/examples/stdlib/list/why3shapes.gz b/examples/stdlib/list/why3shapes.gz new file mode 100644 index 0000000000000000000000000000000000000000..63f07dbe5a21cb4e23f413abd929829fb4c52ba8 GIT binary patch literal 4102 zcmV+h5c%&PiwFP!00000|GisD&m1?Bz3W$e_eKL`1eYLSH_&K|fx6g-0qWWaZf*hA zVo5!i`Ssve;%Yc=Y$p{8xeL+&1#CR?(OS8#o4XIe$xkaCAZknF-{m1_P zzn}j0qyE-D{`&1-M^nsC?@D2=&TF=YQm>h%YU7YomRN1mr+@6x>Cf+f+k1bwdr27l zk53=J9*;-N7D+2hc1jQ}C1X4p_JyTXPa=w;S zn)Ub-%`KC|E|VQDN=ZL|Y2)#)#ZFfI_8Ub0&rcuP(ZaEebVOjQl$v@! z;t(q3Y$~!q)Vi6m7*PJJ4oRJhp}{MyGe~39*w&mNW6!+`a@O z3q#M2Ef)zUWa46cs=;?#LT#o>`r~@L%g(t-?qVtMh?RsA7oDKCMUO<{raG}Z6;F$s zr^5R^P0&j^q^%B*m$En{M_qJQMjh@*nnlTE@-3Mhk<(qPt?r77MGlQhqT;>4Gon!& zTd@EE-o=uFS}AegT~5T0+~M?bcah@@P38=QTyCP%hzu8rIkgytY|I@t^?F-IH%7bu zSklb(0dW~rz1Ut%w5Fr1AqT`DNS_qCXD8FD-o|;e=6h22kaRZtEgd7}-O%y%!O!mB zNCV818oLl{D83N8+Io*bKfc8${m?!@4Ep8rV1GY9Y+?X>05CWTQV+Y51@zh**H(b% zfMX2Q^D0IsZJY=A=SF%g{`@suhq=394i0`@>o6hGVX+a|$|$fY0Omj_rBLs15X~!2 zv$Knx7$DC6<2oZ)MK6vDX+kvD8dI*o5b*EJ*|WyBdc#Y+X7kTu!*y(2$F9NZ*MV{! zn3jQlT6AoHC8_t&VhBD^0p{VFQOC3(zm-=n`Y;VVr87;MBx>+V$xt_p|3fXcClVx5 zzsuQOIr}}%{OtO97UA@jfN+q)74AkzQPN!&A4k4vk^##c$5!J_k=_R8xo(>kHPVFg z!~-d1M18H*_LP0^t!gqBAb)f*Hz@B7tnVOSm}&j_)l3^6;Xj%EJ)U13-AX8HzL?_P zVr7T{Zxo#sk~48Ffm?4#2Tny^(%I$3U#B&#hWue|Qbum*Tmu@bW+T!kurZpyfG(qm z&8b$U7q$3?$zGw?h1;sqqu=8eUexr$YE|+v-m`LB$Pq`2CMhbFjNS}cmSe8!b1^0b zqxZ#CzqJ2qU%s}h*H0B?`F1VfG@_n>7A>HLIvWW`GN*GHUl_Nj18t_HmhDYbJ(e5+{$=K zb>e$W$a66f5HC7B03))TT!CZf6jsg`s+G-kstL`^oT;lPSB+>&S(>6*cEO?^Rh5wY z+%Lb8^~OG@_wE(6?nHao68eRZ?+N)j<}~SQ4dIeKx=o5DI>4mb1MqJp=dohy@!lGX zbc0-tLBgd5B6h7KS7je8XFJ+el|CtEhkmp8o$rT-A87+82a+ik{ZCBQdBf^?|vGJr?*A@x85A73ERF7X0`-0fF)DgfhYvda0B z-}d`Hp;2qvJ^D9OLJY*2oCx}jlxnYcPgUhxW4&q6rY~nB zTz{O37CQY_!LXv)rO|}LZWg|%0C)}wW$S-`V1`>4-C;2rw~5McSuGc;0_rS+y#moe5*P~`-tfP6W2jIBStJMtj7}*&Fr9+bpT+_XeQup<+ z>HTIWo&)C`k8l|qT|#f6vDYN2)Kme^0rAV&!hh1QpT2wpI={3HXd2Hij`r`c++cD} zn*+N5E1+wu&^D!Hv|05D-O(x3qdF|*j@{u|c48Bj>ycWyhe%Cff31>p5JeF2(;dy> zb^D>01Z0fYRqKXh5=FX(H2DLyG#wimKGGhzs(utED z4b|Yp^Jdku3v^+5Vu)f!=xcj+wIOcVQy1WOSUN#CKv+F--TXG|=1)Q9#aGM*n@IF+23|+a+vVM?)q9Dm&do`&~bjklxrZn`fu zj?T3PO6VSw113W=)Pt2ki!02@{r539ts1mfqnJg`;VGA=kzj$xdywL!S_nrrL6gH( z2%(~3>>quHX-)xu&nKMt#8uPb{19h8Vd8VRW8#nL#Kc0Xixk!#)8z@ZYGss`r){b< zSwk*J62TG6$QC3BkW{IgJVo%VfWsRVaJT8IBPYcXkU%ck^b<2ktgv39cK=f$;Q2iznXkwdWb40~d7&%i??`-|=^gio74Ha;WEE-B-aY zXUKr9=vE5qQBS3)^}d?`C}S#FKiZdjHhj{&TO;~1zneAB&$@cl2mG8og1X zpr@^Rn{zDzB&hRWTA(+@Bx&k0(RE6T69^3f!!hSC!2b5l92V-K6B3hku z9u>dE(1*}V!}!CG=OVcLvYTJ0oQ{aHEt;;V2|!ewd+{}^I&aa>__UVNQz4v6iA0yP zpy%{R8^u%|!2>u03GlxD8KG$jx_=QtudkqITjM|nhZ91U;z^x?C9 z8>9Df*A=kbAiL2>R+qXo+Zm{!kuhM6#w^)J@V;^W_QyD%s>MR;c0B6=>8S1(I@J6% z-LHvZkM0IC0yy{*gG&*MBXZ3`Rav}v18bGO6Vx~I-zB;lZMPwg8ZIe#S1bArL}Yh@ z=FRq<-24(ttC6bOjARK|XaH-+0Yb3>*kByo%~pLiQ}KYwrqIBir6(IxF&?;pyM!9M zecESqc)`y16A>exf*8aQ924pQa&sLZJ(wC~o#>H{c{MccItc9 z%VJBGH2&_fNNo+qmz`|+|0_^sqp=iYys=3D-!u9wK<*NX0xX2dzJHcTFpVlI2dQRt zhEg;r-L07cnc4(Mw_;4*!4E3*cNG&6pcKWF8kn8+0U8`>4^59%v{j4d(80Ya-zlhJ zk=DTkCW)+-qZwC8P!a&~*L?Rz&U3zV6X{#>ou5?twtQzP#9#}Ow@>i4nsP~ijZhbI z)2S(YbH1~bMw=%zdLP76h0{1IHZ~$(CH|3ohg8&+t%w-*6}^-}r!w~ZJnD~gvsGW8 z?~v#^3M(7wB%^sJX{ij$it8b~lKhh#vzMiR89(l3|P$@@|`=< zcL);eP(YgZf|k+%!y?TC$f5~B376jT8}i-v5hwvUTS0qUxT5I_Ho+@9$E?N@_x7|F z_CHHUDSH!~`s_KEoShw)mNXvfsqS29y{Hr6C?XfN1SC zQtyC}b?k-%Yd<|F*XXJ&9%x79g+yzu)hoWIj)3T$}S(;^key~cNd{RV<%VYZoo^8gpPTWgv*}2hM@*OE%-YNrFSWpI8BraDa!uPB{@FZ`TT|0!%h><1h>MO_r7$kyFy1t*W+I zEhr!WGi-7(nOcdOdka>$+uM`W={$4mX3z)g*c<_FOjra0m*R-qvC9z}1gY=8etZA1 zY?pKR`FcDw?-O5#jY^Dm^X4FDT0Z{_XP>>`3@3WlJ#~vGhVH2)f zkYUTlZ`d4mc#Qj2KVOfJt{aeU<`Jjo%@sIk)JAk-$gQDNqMm3^*Yrr&5BF&Q7cS>I1=TeG E0FsRjTmS$7 literal 0 HcmV?d00001 diff --git a/examples/tower_of_hanoi.mlw b/examples/tower_of_hanoi.mlw index 8af88998b..982f7b674 100644 --- a/examples/tower_of_hanoi.mlw +++ b/examples/tower_of_hanoi.mlw @@ -66,7 +66,8 @@ module Tower_of_Hanoi use import list.Length use import list.RevAppend - clone import list.RevSorted with type t = int, predicate le = (<) + clone import list.RevSorted with type t = int, predicate le = (<), + goal Transitive.Trans type tower = { mutable rod : list int; diff --git a/examples/tower_of_hanoi/why3session.xml b/examples/tower_of_hanoi/why3session.xml index 27d44d81b..2f22ac023 100644 --- a/examples/tower_of_hanoi/why3session.xml +++ b/examples/tower_of_hanoi/why3session.xml @@ -4,330 +4,334 @@ - - + + - + + - + - - - - + + + + - - - - - + + + + + - - - - - + + + + + - - - - + + + + - - - - + + + + - - - - - + + + + + - - - - + + + + - - - - - + + + + + - - - - - + + + + + - - - - + + + + - - + + - - - - - + + + + + - - - - - + + + + + - - - - - + + + + + - - - - - + + + + + - - - - - + + + + + - - - - - + + + + + - + + + + - - - + + + - + - - + + - - + + - - - - + + + + - + - - - - + + + + - - - + + + - - - + + + - + - - + + - - + + - - - + + + - + - - + + - + - + - - + + - - + + - + - - + + - - + + - - - + + + - - + + - + - - + + - - + + - - + + - - + + - + - - + + - - + + - + - + - - - - - + + + + + - - - - - + + + + + - + - - + + - - + + - + - - + + - - + + - + - - + + - - + + - + - - + + - - + + - + - - + + - - + + - + - - + + - - + + diff --git a/examples/tower_of_hanoi/why3shapes.gz b/examples/tower_of_hanoi/why3shapes.gz index 788aff54d41f06e454fde9d5688d8f823d9d4f9e..d570ed9c4c0223ef64741105f19754751572911d 100644 GIT binary patch literal 2230 zcmV;n2ub%JiwFP!00000|Lt4bY8*)tec!Lp4=iM4Trv|p3&vm&4D(p8OI{*(1V%Qp zc4j|+qiw0Hs=KSEM^d+B(+@UPUAKr6CvF)jr|f)}#ONZZN^ulxjuOQ))#9%{Cr|Om@4pW{|910faMvI1 zHwO=Q{A-AV|9-=t)33Ql3C54Y_Q-ww2S(}%D5NI6)tnnd70y*!=v*1DZnm$2{N+x+ z=xrNt_Jx7QTX68>6`;dU01tFMJp(xS5EyRm{m#oDmEiG^#zXx0eg_s1d(Rda*t;C2 zmnUBfQ!%zmz1y7O_UxDH2K@Em?4JWxnCSHYJq~fA0}K;s-FOK5g2w?L1)IDfJ-&4U zVVt5n3NBM)q+vuX9w1=a7a$EXGHU0dcjHArrQ7&%9zl~;%zoXfw0%9+J$`!_@$h@% z`0*kf5(g)^`@^o#x=0P?%+jT#*gF$fO`;tjwAQZv$agpS_Wr7Az0>?v|F(M9Yx;#1 z_2Toj>lJ@Wr&Q)=;ZLj8vOo5@Z%c%^a7;E-qc*TaUd(NBFC6Y2q{#K!DzpnUQSkW ztYL7Ll4DN*TC+T#$nvsg`S5(pyHp7@xKgE8sEIrX=IAU7vtsFo!`-|9y;%H*vN$L8 z-A8HNC&HdIIVA5`T(DY;Rzoe$I+9Zvo?hGVyk>Ygk>S_MQFwuR)L~9&-82!35|)hG z8#D?6O?)WF8y+r(|B(z|LqrMKz-h0R)0zI^_AzaQjJx)gFC?7hHJ z$f0iL_u@f2R3d{F~ESZl>xx}_n>5G)~u>KkNfcG{MBIa|8BF!aLElQFbd zluX52iexixEf8WBZ-o<6ZB=23p+>L^FE6}2884}%F4_Ra+PCULh>o1P7%6woAuaII zncTmv3C=5W%k#yK$$HFCav*KhXV^FqFxdZHggh^~(=6V;pJWd=o^D;Nmo~O){tuQq6hRK9%bO0G0U~fJW2U=MqrBxhgvxf6Y zZ~t@u`(Q1eJvvJ3=W4-0x7j}Y{pNK@m6CH}ji+-~jW&ucDsyP;T7f9=24Bu z+kE+Yas|vMY79=uidtWL^3s}gi`5Xhy5xI%mC@%r`$&Ak=(Ba=+5+U7EaODaskRhE zm3uAHbvF9E(?9;5zwFb-4Ls@$vp@=A@hJ=0d_6teq@TmjS!%)eJ70LzW(?0T!U}2$b zSHi@iwBwhXX`By}Ts^+RKfZX1JcycTIY+=Yb^W8foja?i{C8UX+@_Vu?ZkKR&F^jtlIB7>Q4?*f!3^db45Le zL;zd>j8CL2MC<8DiF)Ks+yEq$$-PF(q)2eCkPRDH0=WhJii& zeZ&q<_$Ka`=?zpi9ld27!Nz*IkNo>Ki*a@YuVm%BIfsK zmEsZRHKnw_epU1<_~4JZnkwTGVaat9N) z%-CCDJRKRmdkbV-W*MxM*KdZ5%PgCd(F!d*FByHenlO_|r`kHjjG)BuIM!GtUE(^R9-FiYt!1 z=1@0Vp%%SNW;^jNj&*UYi(}3II6y0G~f zVN>WFUNj2B!tDD5GCHJEDW>3j?8KNu4pP{HDpisl@Q#qtpMr!XV``NhkSm^QDA~Cn zmC^a6erb#RX&nCg=XUrS8DhjPPywZZ zi!`@;KmR!0WNgoj-D#4Uq{Z~5c5KPy$Bz^#YBaS>u_o6`(o(fK--6fDLk}$ny?UQ- zZu`yuu6`Y2e*fwA%RmFZ+y0FQ_bz|=ba&tC5Vu!+y*tPc_~CjoDt!3+??cbO-+Ub4 z`u+Xp;^B>d4KmQ*FZ?zA8azrceiXM?@ZleUQ>n-y5Vu~nSBybJYf02osC;#^oeJ~k zyY{)=*1^rbF!=EmH_-S5{oxT927f)hLp(SL4L5kVGx?(uVZ8L?rTg%12NqZ(p%>alB%*|f@;rPangUfEpw>9*e7-+a0~Y|l5SRaVE82_*O2V*~0D zQYwJ#u=-kOTJ4E8GWaQ~$%<;}`KobA+CzW_y$!g>U*)( zGi>Z7D8aYXg&ow`*?Bq4#nVN;UG))GBA_A&uf;C&$m2EgwiE}vswWgH%C}=i7k5$B`hqx^91x_@gK?J z&9Nf-9v}+ERFk+KH08=!YD;A`)Vf(kaw^07*EW1uGd!Qj@N4NPzCb=oQUmn@f-Xs7 z0krV$Qpz9^vAN?7j~B!LNQPGiFIHgr4oW^j?AiB*NnKN0$ygd1)Mr(nzaK@MfGiJw}f-vM^(33GV zSiMt3IRv!qs9SAHz=29-O1-cyG1Lfl;pK&wC*x%;6}6P)lR~0Y(XOhNz`n(pJS^}M zOzz*;1P?26^Yg`yXd%B@RoR;5oWP}mq}mbHbu3{q;LqayYbu})oG)0SXwnqar%mO| zHBsEu&2qJ!Hf%mU;q%yW*!0U_qeWveDF@4=+73 zDt=uSALqA)^~k-)2Pt@GA)YuBPAuwo+-cK9qc~Y&$0_J>;wknxv&+7Ew&R#PYrh~7|+;t|Gtiql~)YCByMFV8!Upw8?iKvz!@F<_3iaL4C)8OIY zYq+4%)VO|6BR}!rrAAP*Xm4RY^x&v$Hb!%6*}{`q)CF?Od*a6;G*ZSt{w;pEUP9_? zviNPJHtC>0FH(&XSUOCWAIB;og3BP9feOUzbD!@aud(bW2TFTl@{U5+CKXE!C7^E} zqTNEuOMULSqyFR|QF7v<%c+U42?JFC`;Q%#6nszfZOTQBra|vz5L<*|hM3h9DCb2C zsWs=AkU2{Bh{RrEp`_8*ApHG^9c;}1M2Ho@W+@uDg4`_0EKs-#l@?TuedVwto@2G2 z;TN`<%i3yhB`(Ip#DD5)|03omXPM#=<~NkWdClKgdT7|ax5C-S21;7dC&HxNQuyUg z$R-uUv5ds?@L=voOFY=|qqoBYKM)s}``>IxrsG}$? zWnlu}Atr*}s=NB{?On_IM=l>XOWDoseV?j6In=eMvD^s$(#Qr%4W%DcKg_Dvy$;l6= z_~s|5#g}5~nXed0v~b+~T0S~Q0O|QBESC<@9dpQX0u2m@d)9LR{Wjtr4WL^CaB?nl zGU)3;%Og%|egk@2m{p<06f|&V>QIb#6d8#$>%m6EnPqIynv`6-T9RHjfzD;uofii# zFz68{XuckAeR07&OUOAy?X@BWV&AE`;-I4Wa9Z3nio-(h`vfv-V)fk6GrOEzE){FC z1dR%dCXJ#Tc(&@@`_7k*=Zd9`sa3d5U~^@wHlCIfL=sf duKe}XRn^7hd_VABp#NUz{|`MK6lkbR008w3T2BA~ diff --git a/examples/unraveling_a_card_trick/why3session.xml b/examples/unraveling_a_card_trick/why3session.xml index bd6770d93..32a2c802e 100644 --- a/examples/unraveling_a_card_trick/why3session.xml +++ b/examples/unraveling_a_card_trick/why3session.xml @@ -2,70 +2,68 @@ - - - - + + - + - + - + - + - + - + - - + + - - + + - + - + - + - + - + - + - + - + @@ -80,34 +78,34 @@ - + - + - + - + - + - + - + @@ -125,34 +123,34 @@ - + - + - + - + - + - + - + @@ -161,13 +159,13 @@ - + - + - + @@ -179,13 +177,13 @@ - + - + - + @@ -197,7 +195,7 @@ - + @@ -210,20 +208,20 @@ - + - + - + - + @@ -231,26 +229,26 @@ - + - + - + - + - + - + diff --git a/examples/unraveling_a_card_trick/why3shapes.gz b/examples/unraveling_a_card_trick/why3shapes.gz index cf41cceabe7ef35d4625e46e37ccdaf9f7631679..e59b20e78f2905e1c49646f7ac9fe9d44a83dad3 100644 GIT binary patch literal 3594 zcmV+l4)yULiwFP!00000|Lt8(Z{s);z0a@6c?Szru~=0kFtb2ofdGA()56yUKX(Gm zcF(4JX7}fBDY0YOmK`~9r_&uBg2)m{QLi4W>PeK?$R%>U1WKIH^`0{LPF`v(F;cur zpML$L_upFj<>t4|-w&<|g^*QJ7S5Tt33R5GnolALr>E=Vf`QO#gLv!07Zs^PQC#~T6`UmRlDO01^LKAGR z_24A-N-+XEI^OhdYi@j|`=)cpl)J0s2x_xFM~6ZkLsALc`nG9a`IT&|`}FsZA3hBi zzum_JESn#)DL~g-tinoHaa%^mwZph}v}*50h&%iJL(AAO)Dm+jP#|f~+Sx@gxS_Oq zyt6yK+;r^AcDBZl9R`J%YL5X)BKhPDY!UTbt~S-z|9?!swGaRL{Obxf8@SmxBpZ{n zMiLbc!cM(_c61eTYrbldqm6Id+-#i1#Fi*XBPtoWF=RVoO5QFFQZ16*6VLl7O-s!& z*XpxxinaF=130HCyBeym$It6G8@$n~g=dJMh z7`rvbZVKa}%@M{{#?8antub~}7~4*F0^?%{liQA_iy=&C&Wrpkgu{ww;Y&7NM?;&| z9+PMS;i2r-zC#(}4Z?8;;kXxCaNR1bVyvGU1t*qY~d?@2-9^`A%Qka4~tUS+w9PS_=dH&(>fA)`GZ|fuO z)rh+_*2k}J9y0VTP!G_q^xf_m-|aT{xL@Ow#y!`sc_YC*3b2_gp6}OqO#z;wfVIgZ z3RoGYS$@s0Dd59|UmJGvvtox_6k|3(=3y*`#}hD?HO4Z9v9&29jIE5!!$fXBU8AjBNMwm9p#9yMmSC(Y+B2W5VkTn%aO@CHi%3(GTW&%!;!I` zjvXpr0CMF4@^Dee)h?Jvkcaz=SDk>|%7(4M@5;nkkn5VX>L(z#odM@SE~jJ1`uHez zcs(6E*2l*+9y!PQ`1QjM+z)8`;b|Sv-j6-gC>&kFgyxk-f{9GL&GUN}`e(HdW8v+G z>$@JM1$)2m?g5zm_Ps%Ktn52!%TmR)My>%xEQRRmw~rrxzq zKWD+@9Jdf8t2&LfAz+~rwDzWvuYSL6<>QBX^ZDlEhoi&TwByOqu|9tNew4nsN5+Rc ztg@f+?VklVL+Z5+!t?Et0~QuvR8y%y4WKil_kqyYm}RD2*6tOj-0N_sK(_An{bJph zv#xS8KZvcH8>GlhnlNz7p{HCF_eZ)J`%}C9GY!U`(<>A+{RpUa?8d3sZDrjkc3T-7 z$LDtC5x`1)>tVeZrn5|pGB_e-Y?X8o774GC?HT9*Vsdk z*%e1VaYyB@{Uo&>Zrl%I1;fIjH_9QTtUhpU#2G^EC3Q#0t>$hKu-tQK!=T#AZA+ip zx|stxjhBB+LL3La{Ov8dgS=S@K9=&<9~#2&Mka?&h-E zX<^&jW*fL1T8}*ktVA9HsQ12$aA;x3JZ8zM;c750v|4DjrWKOQ9TEt6ugD5bf<%^* zb23`-nF>q4gu+@l`nEZ$Nxi9k;NStdC+WR}4w*6+sTz-D^7nHhepzhwlD6Um(d1R} zPJ#yKoBHmNOOYCf&4ON|Y*rDY_*i3Oh zS9a}AXMSod2-k;1nN7ECELiCFwdqy?k~XcVEeumYx(_vHangN5J)HP(uIjp!%3lcg zoe&Na4l`Z`l^-~(bnPt$>JbAH_<6!h?jEyWLU=8_`c8ONe2a>x5G+$FzBbR6HZ_e} z$Yg#!PkF_W1Uq)<<&@V#((i<%O%sBJStw0IO+`2{hn8y6T!K5D&i}H&JXhhO+L&)d zmC=Kv4o*un)f)pC{&}WqTE8WQG&Qj3;i2;Mz*>woHzA1C)#M_1pIxIA9WzKW?`=tF zYx%N*XRUNCeVA~;!_C~03zmo32#>koN0_qlUO-Ab1l7k%SybqiC(6 zRL?bY#m0aZc=}Tn0v|nezCu{|_3iQtbM1r6F^)OkyE^BUO=ZCcO zIj=_V808HiT)2=g;;?rq$(!=cN~~N!8^-8n&OzI!@jhZRXnf>__i>eP7G)_ygc(EE zj>OUD9@Fq}(3njW!|X|!8>chzKzOX4PCgJ`Y<1e_FgO?<6^Rtzpo6c#5w(~nq6qQX zlk_f>5}%$s@Ca45@oAyT)2R}grNDp?prtghBm3$Jcz7Q!%Ofw4%Ymq>#qf99+< z{t~m=7J7ZN^eQ!zRIk1i9Ht;h4dg?|D5%|(`dJ@BIQcYc0e&|nFyS@-CdIrm+dH~O`Kg>h%SLTWT3uD(|28ZDTaf&lMh zA(vqGn=K3S=OSN_kTr&qDR+t~CZ+1Jxj3vTfXBWLu>YWPJ8&i*RF0Lz>8Xs1{m!)? zsLRDhNaYAVb;9hTX+zJo+g5XzorLvNuY39__ao%ldfkOQ7oOD$>RobDvGpRuayCe% zlQT)`Yt!>)@J-Fjx{wZC=<_P+<03`V5P^t1hs^9NVv!a*Lalo6RoY`ywJszk7M8q9 zmSC0u9FwmddNGe9rIn;TMK{a|m8Z_$lB0)SPE9P7dzF+6T96Taz#u8AgeG3H*&`<$ zLf-7RHQo|vDc3AHR~wm<$}s;nV2|pPx%14GW-5WlRz&hMr!2lD=zC6)w3y<}5OU1y z5PRe1lIQH{*^_}Twi4C}XLrU*Sc}~^`8N|}N!_$|iqaba)ruiduNTf%jZ^l`jk=}-jSW+eHYb)Nk0NIDnZ zp;PC9I@H*l@29(kV@Ey&@0M0O3G@mMao(I~5?nadn=zz!=eORBX+K^dcK;^85#oKnW0)JDtC8p2|tHTH$_Hg-ez+?hPIfdhH-SKVlyF5!Lk}}iIt1 zUnsFp374yn5*;M!JS;qu1z1{-Tr>sXgV40t>#N!eBtXlMhfgH1VC7VMWmIe)T50XT zUPs2^Vw=m`CO6LzD8wdY8IET&k7#aDl0mL;bqb;|zLme&%p`BuWTBJ{ z&U1%0d;?`z*V*hAb1};2mij@ISj_SwBPpP-S~Yi&R4pRpLM2<4RU$%Xw|6)AK=v+H QdI>B2A4w*A2j-9f0Nwr~b^rhX literal 3581 zcmVO86rkO^P}5a7+MF1QWqnFyHJ ziR_u==ik#3DK^O_)s!e%wt6AE*b~NmEJzy8YLnDWu>yCCs%q#hzS$$hCr%TltR-Vzq|F6yE}qQcBX0jM6=Uk!aA6dipOKWuXUQrxLjn`+4l za0T+=;oEQ9AMN&w)pwKo=j|;+6Ax3m!<0If0jx0wUWMzAf9rQ<=i#B1`B3R!hBOfF zldo3s`ufAKTWoh*3gEg_zv9DE%^2wY^Z!~g`=!jl*k2T5k1Ib9V^5a&e2o1XV?TxQ zQ053@OXKHZ?AI9kDU9u=KY{TvgwbzX)5Q=*Fy)0b3*orpS@@#0*HP2PwZ=r8KzK;I zmG6)Sd4sU-Agp_)1=gjyl^m98S}AN0)`L>El7RGox4*aRV~~@33CMNuH2g&&C;Q-$ zY9)XF@dOi)TUy!*d`Lq$5Aro>F-}1qSHyE5cXyDFH2?7UKl{(GxA_6~a_DZ3_4DhS z2M>J<)C07u@L~6jA9jm-T(9v-;hwA4$Vf1c0&L>a^Yt39DZo<{urhf>0ZYR;ORv$I z0u(3o+HjMfWjo}e7_$K~4`VSro`A8eF_tNetxOqVY-wa3#=ORur!cmgasuOH2upkc zMJB-%S#TFsWMbbJMn0ljBdk*hTdd_r2wNJMrO0G$8$>1)ncWOHLy>VfZ99Uz0OWxO z$m2yJ5B9-4f;`@Td<0P%C547-v;x8o~1`6Ui$CM9AjFI;%x#PFZ^+D3t&vE3+fr^WRy)Rp&qh z1&qQLL`NW|uFelv>FVFNt$hAeZ@%7q{&ch%TkLqUb*!IXe;m1Q{*m_K53}rheEV;K zO_O?SjqrTA_(mNH)>?cDAsZEQ(~cc$)*#?#%4MxyVM@IYJq5B=uOAobzM6EiV+G1p zDAis|$|^AjKy^-&y0+iaP1s-B?H_3n_MBRQnCM49t!+0<*=|egN4DG2z}R-5pv5EP z^01KWTac?^f`mDhM&5CEy=GUsI7})MT{??g)3sly^**T;s(AAk5P+#E^-#=p7)D6d z9Jk2+B()wo?uTFn;=-Z#$)PSt=32A;Wg}7Xq!hbPHA)Bd{hmV`2Gv$>Tl&)0#T{icq(!5_#Zn}uRFFzePKNRC<;neUopbM=QT5Wn4WtcxH>_aeTHgHQ& zh$$fuXMlQUgcV*Q!df``zBw8=q5!xcwd8<}wG;$s)To#{4@W%t`#BN6F0y(}S-B3G z$yaL5@UGQ-q6ic{LGu}loRrm67t;GAvc$uvW3?S)>b=t zYVzE$Yj-;HQ*A-KJ|xO)x@~R2Lbq>DH_RYb*BJ{tiu^eq0_QP-uS{Dp8o z2;q!xHGr!n^cr*Qj&m=K?5bka>}CaCayQI=iNI^&)epj}M#vQigKL5*hTyQ8UTYnV zV@>mUk(Z7_uw##2FY;PQ`h$=ZT$Jotjgr~KD-t@8Mjs?LE{LZ?uLb7WUCC-_GHNhy zrrIA@Z9by&%t?@DMosHgQh-wp3m*oRryJHHteL{nl9@9NYx{%eAcc!bk5FA`);#pG z0na+pHTPjc1rMFMBNZ$Uvk@Ls!H+OyqsbShJTq1)B_gFBs`u1$&qOJ9CGIu2P@f&E znEYws$`8R6hmAY5(sClmRRR-nwWuSw=n~GGE+=;rwZlS*AA%CYRLSUj;}!!|?6I^! z&CHFj#uaW)jS%?gqw^z#g zK-eTvPY!&qu5&80CuMGw&cuN5IC?rcAiT)xq^y!8KoOS{Xls&9>2z(Dd~*r(>mx1sw8dt*lLN=U~xa@ZfJ+%}wvfy!|tae6A_BEPfc=Y6s$FlXe( zlvp{d`l>BPZnc!lPQrSs);&GS{RnxsT6ZDOg=e+)D6#j*LJ1wF9&+)akt3H=meX@> zX4L*tap*#yH%T9I4xOr5iq@jTYVxhAN1yy~=u$h_2=>@itqTPc3rpT4OEP(&2+_Aj z7+dg-a;MNllaH;Pxw2kIVa2gWuNO@$lzWqutLnpW09_#oJ#$1fTA5?pAv-AH*p^p^ z^XA?YXib$+P&f^n4D`~3oYxwMb)~{#?uzxtPDG-aQx@M7^gf#RZm4szP^@N^9E`ig zeEOOT^M#%GXPks}LfM^h64oO3P4EWU$j>x{dL^cMlY6#;X`+=L|(M`qzToNa5~hqDLH5PhoG z`|J||7q+}XwrH=CNib?*4W)+~scDM@6wLnntMujfo3DTW^7-~_tK%9!91ePa<4@^R z`q#&U6$FXy)ktj;rNV}>E{QP!}X0nZ<4QkfdU8Vw$$EDfA>*G z@=nfvfR!E;4scM5I9UswRg1g4Bhs%!Ik-E*b&vEqKCpC10)EqyXy=?K+HFba!aG#z zJWz)moA>?Y?%>#w4uQL))lLGva)&r?-ZKfVJ5`%8q<8PP+Kg#GJ|K3#6W|E($4hfY z*#|YcLw(>G+#j9J{MVs&Bjo(J8e=`Y^5gY8>(+nwQJ-&XyS1-6gwTx(8& zU)bBs_d0j`^Ij!ipKNB|2&~Y$bG?T!Sb%N<)?oyc2%>~EoL}_b0I4M=KdkyK!8h?r z$)WhKHXcaAkjR{Anoqxd2E>zqT^zr#mQsgzKKGAC0ybVQpcd0 zwA3D2GOs(;#-XIzTRAp8_PO?#&$hq3V}E(i{_>V}uM3|m)oJmia^p_bhwf1_L>F*4 zVQ)^i#1wjQb!frk9xgu*m`va(r*PcOJMI?0^RvQ)Q)aRA`0&k@j$E>j3nlg`fh}g~ z!^9kk!l;71L)NMlLzYkvOw%H-Z!0ejNf}XNbsdKtSG;%G913*eRP%wnjsuKYzN7xSbf1t8Uut70ZoaRsqB7g(t=$-E%z zjr5Lu8wjh<$^7-&*1fC^LGF!^&MPflCT|y}<`z?;@qwkkbDHCVE)3=8ymY D(G(U5 diff --git a/examples/vstte10_aqueue/why3session.xml b/examples/vstte10_aqueue/why3session.xml index 96f1176c4..8c163fa3e 100644 --- a/examples/vstte10_aqueue/why3session.xml +++ b/examples/vstte10_aqueue/why3session.xml @@ -2,33 +2,33 @@ - - - - - + + + + + - - + + - - + + - - - + + + - + - - + + - - + + diff --git a/examples/vstte10_aqueue/why3shapes.gz b/examples/vstte10_aqueue/why3shapes.gz index 8a8cc477c8953a5e860e0e51f33ffa5868e54553..9c4a657444023c456fdd1e1b204fed0ec2ff7978 100644 GIT binary patch delta 528 zcmV+r0`L8s1fB$t8Gn6HhYlzT7zi-*sJkSStAW5NlC<5=pYvhao84?h(P4+g0r_aX z_b4(Db0T4Nb_ye5Mrxw;$!79OAww10j@uvA?d5rM6Cc`5+|di|_H_E)f9?uuL*4ho z<1v=S5dC_a#U!x|UO6eqdL-o~`NkU$gkH$V4zqz|t9w2o&wt;;D}oLt-fz2ocr65j z80ZCc$px`~mx4nBW4eOSfQNG`>jGE8!Bb$AkisNN5@awy1Q9DJS9M z;vE=;m?Fdle}8KIYgm-IzFIp5_1muZN8rQ`Tf#G-3AVnwX2Iq8CCFUN&=>mu;^qRN z<*Z`n)DKz)&;9UYb}UGeC90mg9mV_@(}t?2ZQC7qY^gXB_FUrNFiGLe*;0`7^HaTwVxC(&BB~G20u~gN_Yme!PQqM|9|R)h@My?N0+5ljgS3ASS=|+ zHb!us{|zoWH)dtY!db_8PX4k1W3~BM1AaHVUuhGw$E~D>nEZC3J6YR94uYPXTuNYe SvJ9$T{Rspx>SteC2mk<_(F5ZE delta 525 zcmV+o0`mQy1e*kq8Gn(Y4joVw2oPZCQFnc=1_Gx@vUNXyP8!SJ>}D&94m zr&tt2^z&^Llf*K3r6q&Nr+e}&qbX>Rm^E+=$XPY_<%E2>4}YI<+M&PSbqDuc2|6** zbLx_FV)HN)@(XT(ms1W#2~O7V3@DsjuN3qyhDb5evPeNP7fv>&rkz{4NM-8n z65vl}4@FKoxMus};?vr9*fGI5*wk*pylDK8=sgTs6qO~0WP(bPq%9($E=7Ye+Ai*a zQ3zHc#@Tc0pMTw=%+1x>F{od6y-O2lM<2GidD^wzv5YMhCjuYOF+^`YQ3y)M{>5<7CS+5r zqG-9u=4qefu1oE)-F0s@8>e#46Qdt1>yH - + @@ -52,7 +52,7 @@ - + @@ -95,7 +95,7 @@ - + @@ -110,7 +110,7 @@ - + @@ -131,18 +131,18 @@ - + - + - + - + - + @@ -165,11 +165,11 @@ - + - + @@ -224,11 +224,11 @@ - + - + diff --git a/examples/vstte12_tree_reconstruction/why3shapes.gz b/examples/vstte12_tree_reconstruction/why3shapes.gz index 1b966d1a932ac7250d7caa7f39b1f85f812674f4..979205e103e6ffda5def9a3a8fc190309369a88d 100644 GIT binary patch literal 3774 zcmV;v4ngrBiwFP!00000|Lt5`i`-Zae$TI{=N%R#ouhMsnT617L&K1LS^T=3Yo;Na zgrs*e^Y2&3b+fDNa#bbiPBIN4iCyO^eUd)u*mhtG1+6iL^Pc^){e-mc3%$%l52BfAQq^hJ-%<+eK$mh*Vg5nO$q^6`QkE> z&)QpEQ*bfOC~Ggify{1SP;xe@SWETRmTa*G9njmrS_A9dXua8})A-Wc3)SK6iwq>j zUAT&V(O|N*a0Xok1U4F0W7EE5=%Jc>K*Bad$n%(K7*`wh9#Kapd?k;6+9CdFh zJJEfuyWOP~Esqo_;P)wURTZp{SaPmT)ligWN5)+(`aSBP7gd{zkP?AOwivN;q~Iu) zSc=W1Ml+a7cRW9pmZ{9%396wq7Sw>BqXwE)L)&97QUUwz?F$vC8pW>0$l^UC8d5D5 z6s;f@OMBxGSnOTrNWOcqj_}+pC8nH=L@Wg4>>-ruQqW8)I=#AiHM<39Gc@Fi)4#tz z)y_6i-QLYNF(N&QBY6Ar)G(-fk8^6ECP&kwl5Y2sz~jL-@)ZTj()_@s(d3w|kqr2z z{1N{BzxQtnt@XRR=-}6FzYY@KotWCJ{qMnOg20)vPVS;vf<*Ie6M^zceaRne8e9ML zb8Ej2-CYBNgHlO6v4O%QkccrCP#h7s>S*h#{E=j+`*&}{o7MYwA0N`YxB0$ZFN0(# z5y6X0hBc>#=;BdB)iv0nZP2!Amwk%YO{O~@O!jlb`*7xdud*O9DykWyrU(?3@B{CQ z$>5U--qz}~9nZO}guSixlfF7*2|-1ZGgA>Otl}nX$RrfSum_`*HLKslhx_pMVI^eg zLkS=h@J@zhvM?PQ7@|a{vgWE^mWfVtWqD`fWyVk<~O$<>v=SaAc zX1>l^Tywjp+^OxoG9GQW7+ zX?Q%asH{PZg{z5IbnJ4dEPTKUa|6j*l|!y&+K@);AGpA_p3}3gxebV3fundkM6V#* zsI-bPp-3rJeHO5HLpJ#g*U)Q3cK6S7RuU;mhFvn|=8vrqENhsvN?vky()ps5oT*F+ zLz+uvXPmJrMKXevVA)46B+S&zt5-9lzZ}Y19M?L3=>NCB-2HV(1p5_$;Jk?_t+AWb z=$~GNA{9!>dRK*KausfGQ%VvjNbIxZ6Ylk@HQ{+{0&xvl{CrFhPy%K#faqFQhKeOv z&B<(eXs`sDlwonN0t2#Il6zgi_!Mkh=HL6RkC8C@_VvSWo!b6q$M1jsMK*tUbBDC;FZ(8kzu@jC^{?G*^KIq_ z9xZ6L)mrphn$Us-9PSbEi*M5I$DZBfpv@QEi@`U^6IRHBPbj)Pvh+*Qb<(@Ob&^K9%Z&RK7lUGvMS8i)5KvqGP;}< za4%8G2>&@(H4z$`4IAaTx{$$nK%)&w@)A_d%aDKeN1tm0ecQgEI;$idlSBv;3QI1o zYpAyPh%D*2PeAF}FFn3a64c5*6;o1y0$JrON~+4{SUptOooIym?nC+b@SkF>WJk9bXG?Fur7Cv<=J*z9z}9Tk^$XtVME2T7}oGc=38P{_P9xZSbmE;l2hL z1DE6@5M~#w5M>-Ulk7;GACfwbG*B?sBf9_?|QNrf@nkjyISQo1G-N9h%&U-+#a)`LL zs+7?&78`UeI#ASLS@Kx&p%gbf7}}QtC=axBm6&P{a?PI(R9dN7}imBPX|A&fgMk@9ASlcGPCU z@g27xyTDclhAI5wwfd(;=zB@Aru0weU~Z~>x7cqpVrD zMx(xI)Xyr^AIp9!v;4ve9qnd!vTJrw>K{_#J%-&xs;Sm~X-c>5YE<~8o@A%Jf`aQ% zvD|MxK8pw9`W69`!Dx1Mnp0a^(Hw2@{9yg`o~1YaH(=pZntc|W2i9LZxrVKOx6 ztDS&ebOK5|m7T%>U+D#w`)#K@9UPSHgM)I?{;cTGn!WD-p3|$D(5wCGiXH7}4QtsH z4I_lIqWwWQm?}rAPaEFd%8_@o7Q{X4=Is*&TLWS>lp*U$1Hz#J;UTdy2`1&F^Nrnw^Cyd)cM_lJ@kk@jiMeo~UcoKA~UNz#|S zlAKsY@XTbJ5tg71-}kS1o?xQT)VF{KPBbCoaX$ z$VC@xOp3Ka|5k?);Di*k#gN@%yufn`2vfzJ#eR1E3db`%1Rjk_;1QR=5t+a%*aR-o ziJ*c?DI*%Jv2ZS?Fr&{tw1=e8T=t0A)x{=UWMwa$pB>h5A_Pwy3VrEh_~{O?zr`@lqC^`}sjOW#&S|;G5xCmO znqeHq7uS#1Y(Nb+pbj>m4~p*a9VnAi|NhOPEJn2kv{xw8FU5IDjD3+v?@b6s<*3ms ziS<@P3RR`2i}R9xoI{O{@N*6~`r+`iIl(%V#W@F9C-Fl|$#508VDUM6$%uoo%EyER z7(-?)3Gz2X1eV~mp;AY1I)_XBaBynrKOLq2ILiO=iUI&F764Sv0wN)kOsI7YUU+5= z3RShC(!|?WGfZKky81Xo;cGl!HLoe(P)kROf{~)|inyT`6eS|awu)XfO6s1)*o{_6 zsGU<(Ezx--U{hu?7nhmT%aaDz7HPhuYEC@E^DU-lVm(GdO^RHJ!Q={6YYs~3O3p54 z@8>*zG7;1lyP1>na_i&w12l|I;}O0MIJAe?FNVXD zE;|f4>(QjC7`=FIcp4oWS7)wpb&n1YCCa`S9#577r2YiRrW91DkxDX(443S|nN-5W z+t)Ke_b*d*{~lvP!D@w98SPcgu~z3PITr&+%C3a2|LE2C@6mA^r;BOdfG8STb`Ftp z$vPGY2@=hGn&G($|JgA4z8p9RLaNhQ_;@7%u%0EbJ7MMRIF-MhB>V?QP5Ua(#i)6* z(hZ|U?W5tCEUEUfmEvN1Asew3c-3=N{(B7bUPY}f$cg%box>?&#PR!=C&@5?;2@(4s6Y_=KD3&X-- z+o#^Lb|vHLBytb(!DoS=QHs)rG3!)~N<}BF!3V0PNTR7g;?HWh02*uywVsbuJzZ#TZ?v9+a>HNdQr~#H*8_X-8~>t?JENB~1jk--)_}c3xar$5wBm zqtZH!>P>V-X`Plz>&2H~YRU=?+vG#Z!pJmJFjan!!2c`=S!Rh#h0 z>_=s7nl5Xf#t|)rI*--mYBXzGEP~UZu^2ANfcN37FULI}%|5%Q!-u)BN>0I1BUFay zef!ckWI_ZJwC1@t*8dycuU7^ADAu4g*+$Aa6h;LBN$2P_1=7iTvb9DPGsbKOjAby*?F$#kxSCvw37m-$vKXBKoid7u z+82Z;JNBEH`r&Ts?r@ z?%&t@KURPFt-}t&&4>4&yDv4oxqlaO`S|e9&mDB?_LVQH=t7ZQG;Bi&CDl+9}^=)o`q>us$nskrm>R}9j7Z`TcXZoV7t znlBE|x@JUi?S3lI!KulBKmm@Y1K7^%VMlUoPjqAiYQV?mZ9DIV=q{0kNm*J85LRY1Ve8X9lyOS&Gqx!-(#{^GSq_Zy9OK56?=@PA_9jTd)^GB%7Z zZ!SA=`Pz58Ll!TO94X-UDVa)Dv5!!4u8wLb#Kxg@SDSv1I@O!14TXRSl}%i%>~g^1 zFqT*f=Tf5`45d3WKa`fC?4AT^XpIFoz}L6|XWh`&*qc&-b=2%=dsO1>-V$)!*~Y%&K$)5!P#RA5*&0cQ z@5&$H@BjYzuHf3gyMs>szP+wf3GPk|ZP)yJ(3>D|rmvH$Xgfio`L>Bb`J}((A2g4x z|MY8XzYg791A|kgqA;;l#h^eU##|Jc2+C9)xvt6|NxHiK@IJg-ef;qGA$@qC@7wV* zNQM>>yvSfsb83h#9<-{u1}>U|=Bi!xDPA|2?#y7YUmMU3%w;F+_gX*bn=_^mDB7G27TJYWXtIWkB2ldI$`Y|%{U?075APpV zB9=at@VSf;qi50g=HjUolY*%dX-&;G2uB!^PBIG=46tT@aw=AY;uRaA`O4mY?aZwe z5|kO2LZDnkFdjoRx_By4N4&s~JtdeC=gYP{7Fp8Z_K8;+h3HGvoH4w0nw9xo2fKTEL^PR~uzSMYy6w6zXb3R~sl+c1kWS7+$yDUXPwyuik{J zuLh;0Yb;rf@uEWupjQe=Csl%VzAC@kPhmZBQhla2Kee+X90WHWwXz44!uWYb$>l)CJ~cl*d;@5e9R)S*cy{5dCA#P=Zj`? zrZXiBX;Z3k)>)<$(F#%m8y~%hFk7=(y_xC#_0ZNrTZNcB?%NL`?KT|^m^5t;Ji60p@u9xACn3o0kc>I;96D& zWF%P4*=)IM#i%rrHA1ff17t19y)Mf78Z0tRZCo|gD-L=UJ`ny26i9>(RT~m>awUP) zim0R*RyPl=;mytF_x+Y*B+R~l`|!_>w*T4b`(J;P#UGyBA#MAYeUrn#!0u1%1$=+TYW-ub_89s&)9cqP)9yQ;U+19F}&tIi#3xZ|6OI z%$s@8<|!yW`A}>=mX)oVaCZ~lekvvZcW;{x6EyN`Tk*@ox=^j}4mw+3yaz-phrDuG z6Olt*1c+FQ@xo`CGq`NAiid6{GGUx?*WMtT+eMP--cMZ5XI+1EnLXpO-RewI>r7*+ zMnLCG;BM+ly>z80f4wi-46Zb1j5$>*S-fsNq9l-SCph{S(f)!B@J)n|@B#cfe0cxv zzyEmGAGr}$x~?x!bo%w)|AIw1^|v>NCVu$Rsn-H}z#UB;k=%AVe@eJLr;my3sLcZL z9k(A-V5Me=dr7gT{Ez2gZmN8@c->~iN$>CTGnJs>06IT(yZHBEWU?d~;JKc8qcm2rhb9?O$~2>#Gzc%)gA6$K$dm&Y z5-n@QC=gT#UQ#TuOZT)d(&n8`>hc=XToG^Hl1;b!LracC`?O|1X-QE|r%hRPE)KBD z&p7dqYr%xBUua6vi7uh&60Oxj^2=Fu)s#= zl!S^&WomB>C zE3(ylK#xWFsDZdWMqJ1lr7x3LXJKW!*tn?7UeK~fi*9J)Bea+iTI>~QaZBRUfdNt? zK)p9L6;2$Ksib}KBAX_jsh$bzFcE?$ZVG+tWcc}RV1JKcJc-tg?36W?HRgnDN-m;( z6*`O2j>7oj{Nb7f&~O2CumF8fbXPxsGfnE>zd5wUsMY{{g){wvGc{Pp3eW{44WM;} zz{v{+m=)5@%O6h>=Oz6(M;aaB=NxVH)8S`x2kX!l=iIkXL!EH^vtA!3^^-^1steUEE9v%QIxpl zycE^XdHiG|s4re-Puk0^Z@(X)VRSbh)b|00_VD_}aCo--%UJ`ay(8J4`7YM=$Wo?7}5P{_^(a&Ce{}G8>awrN}CFi_$)kC!|#8SMs zp(wAyOBMc+VDf_zxa9wtb*New!qC1dCOXeS5;d;dSDwC?B>X2wP5Ua(#i)6<(v8oh zC`w7PwGvd)DI4!Y4!M1E0Ab>zD>GsLr>)BWh+#e<1nJn4QEb6SrsAEh;3O;8zJ0vn z|GYZCc53@x-^EUSwz62QAvl)QEvSGPD~K@1h)zz{s*G7Zqa}Z=?NQK!ZV#dshXJY+ zE7qFYqeeDbbb~jUrjUD(555@u3_c=NYBB9=r^u>Mbf%Sbxtf|aDYY6-00+y0ZI8Ve zo3X>~3wtcHM~u!V$@-Ys8Dkv9&>n~dn=NSP!s;Yw+AX%hQuXGol4gS2AH-cEJ1?%R zL#sF8QE44V^(MTcw2n)qb*n=tAtxKXEm5f!#H*;F=L&W0dzu&Hs8zKQ zj<)@%tc}xU?bA5IrBLV43tVhSK+#5y?Rz1hb1GhvLUrM1yk2h2zR=S;ZM31K6frAK zxjKltiYQICRLDlvF!#p#zrx4$tW;l(tkp4drkZSEMi5LY$kk(36^z?|FZ@I|ZDwaQ zyIX35+b`txA8xjeoXrjb8ehSN+@63n5;T2{nwSTQWiZU`D^h_pTgs@IJQ2hiToBrp z{JK=#K7l@UVZVr}Kio~79Zs~6Mo`u!4MEjdlaAJS9iwk$! mem x l1 \/ mem x l2 lemma mem_decomp: @@ -204,7 +204,7 @@ theory NthLengthAppend i < length l1 -> nth i (l1 ++ l2) = nth i l1 lemma nth_append_2: - forall l1 l2: list 'a, i: int. + forall l1 "induction" l2: list 'a, i: int. length l1 <= i -> nth i (l1 ++ l2) = nth (i - length l1) l2 end @@ -229,6 +229,11 @@ theory Reverse forall l: list 'a, x: 'a. reverse (Cons x l) = reverse l ++ Cons x Nil + + lemma cons_reverse: + forall l: list 'a, x: 'a. + Cons x (reverse l) = reverse (l ++ Cons x Nil) + lemma reverse_reverse: forall l: list 'a. reverse (reverse l) = l @@ -259,24 +264,27 @@ theory RevAppend use import Append lemma rev_append_append_l: - forall r s t: list 'a. + forall r "induction" s t: list 'a. rev_append (r ++ s) t = rev_append s (rev_append r t) - lemma rev_append_append_r: - forall r s t: list 'a. - rev_append r (s ++ t) = rev_append (rev_append s r) t + use import int.Int use import Length lemma rev_append_length: - forall s t: list 'a. + forall s "induction" t: list 'a. length (rev_append s t) = length s + length t use import Reverse lemma rev_append_def: - forall r s: list 'a. rev_append r s = reverse r ++ s + forall r "induction" s: list 'a. rev_append r s = reverse r ++ s + + + lemma rev_append_append_r: + forall r s t: list 'a. + rev_append r (s ++ t) = rev_append (rev_append s r) t end @@ -302,6 +310,7 @@ theory Sorted type t predicate le t t + clone relations.Transitive with type t = t, predicate rel = le inductive sorted (l: list t) = | Sorted_Nil: @@ -321,7 +330,7 @@ theory Sorted use import Append lemma sorted_append: - forall l1 l2: list t. + forall l1 "induction" l2: list t. (sorted l1 /\ sorted l2 /\ (forall x y: t. mem x l1 -> mem y l2 -> le x y)) <-> sorted (l1 ++ l2) @@ -333,7 +342,7 @@ end theory SortedInt use import int.Int - clone export Sorted with type t = int, predicate le = (<=) + clone export Sorted with type t = int, predicate le = (<=), goal Transitive.Trans end @@ -341,12 +350,13 @@ theory RevSorted type t predicate le t t + clone import relations.Transitive with type t = t, predicate rel = le predicate ge (x y: t) = le y x use import List - clone Sorted as Incr with type t = t, predicate le = le - clone Sorted as Decr with type t = t, predicate le = ge + clone Sorted as Incr with type t = t, predicate le = le, goal Transitive.Trans + clone Sorted as Decr with type t = t, predicate le = ge, goal Transitive.Trans predicate compat (s t: list t) = match s, t with @@ -357,12 +367,12 @@ theory RevSorted use import RevAppend lemma rev_append_sorted_incr: - forall s t: list t. + forall s "induction" t: list t. Incr.sorted (rev_append s t) <-> Decr.sorted s /\ Incr.sorted t /\ compat s t lemma rev_append_sorted_decr: - forall s t: list t. + forall s "induction" t: list t. Decr.sorted (rev_append s t) <-> Incr.sorted s /\ Decr.sorted t /\ compat t s @@ -382,6 +392,8 @@ theory NumOcc end (** number of occurrences of [x] in [l] *) + lemma Num_Occ_Positive: forall x:'a, l: list 'a. num_occ x l >= 0 + use import Mem lemma Mem_Num_Occ : @@ -390,7 +402,7 @@ theory NumOcc use import Append lemma Append_Num_Occ : - forall x: 'a, l1 l2: list 'a. + forall x: 'a, l1 "induction" l2: list 'a. num_occ x (l1 ++ l2) = num_occ x l1 + num_occ x l2 use import Reverse @@ -472,7 +484,7 @@ theory Distinct use import Append lemma distinct_append: - forall l1 l2: list 'a. + forall l1 "induction" l2: list 'a. distinct l1 -> distinct l2 -> (forall x:'a. mem x l1 -> not (mem x l2)) -> distinct (l1 ++ l2) @@ -586,7 +598,6 @@ theory ListRich use export Append use export Reverse use export RevAppend - use export Sorted use export NumOcc use export Permut -- GitLab