From 41badd75386a1fb811ef7fe6a950c17b6c93a564 Mon Sep 17 00:00:00 2001 From: Claude Marche Date: Mon, 16 May 2011 21:44:27 +0200 Subject: [PATCH] Coq proofs for power --- .../programs/isqrt/isqrt.mlw_M_WP_isqrt_1.v | 45 --------------- .../programs/isqrt/isqrt.mlw_M_WP_main_1.v | 36 ------------ .../programs/isqrt/isqrt.mlw_M_WP_main_2.v | 39 ------------- examples/programs/isqrt/project.db | Bin 19456 -> 0 bytes .../power/power.mlw_Power_Power_mult_1.v | 6 +- .../power/power.mlw_Power_Power_mult_2.v | 44 --------------- .../power/power.mlw_Power_Power_sum_1.v | 6 +- .../power/power.mlw_Power_Power_sum_2.v | 53 ------------------ examples/programs/power/project.db | Bin 15360 -> 0 bytes examples/programs/power/why3session.xml | 14 +++-- 10 files changed, 20 insertions(+), 223 deletions(-) delete mode 100644 examples/programs/isqrt/isqrt.mlw_M_WP_isqrt_1.v delete mode 100644 examples/programs/isqrt/isqrt.mlw_M_WP_main_1.v delete mode 100644 examples/programs/isqrt/isqrt.mlw_M_WP_main_2.v delete mode 100644 examples/programs/isqrt/project.db delete mode 100644 examples/programs/power/power.mlw_Power_Power_mult_2.v delete mode 100644 examples/programs/power/power.mlw_Power_Power_sum_2.v delete mode 100644 examples/programs/power/project.db diff --git a/examples/programs/isqrt/isqrt.mlw_M_WP_isqrt_1.v b/examples/programs/isqrt/isqrt.mlw_M_WP_isqrt_1.v deleted file mode 100644 index 53a060231..000000000 --- a/examples/programs/isqrt/isqrt.mlw_M_WP_isqrt_1.v +++ /dev/null @@ -1,45 +0,0 @@ -(* Beware! Only edit allowed sections below *) -(* This file is generated by Why3's Coq driver *) -Require Import ZArith. -Require Import Rbase. -Parameter ghost : forall (a:Type), Type. - -Definition unit := unit. - -Parameter ignore: forall (a:Type), a -> unit. - -Implicit Arguments ignore. - -Parameter label_ : Type. - -Parameter at1: forall (a:Type), a -> label_ -> a. - -Implicit Arguments at1. - -Parameter old: forall (a:Type), a -> a. - -Implicit Arguments old. - -Parameter ref : forall (a:Type), Type. - -Definition sqr(x:Z): Z := (x * x)%Z. - -Theorem WP_isqrt : forall (x:Z), (0%Z <= x)%Z -> forall (result:Z), - (result = 0%Z) -> forall (result1:Z), (result1 = 1%Z) -> - (((0%Z <= result)%Z /\ (((sqr result) <= x)%Z /\ - (result1 = (sqr (result + 1%Z)%Z)))) -> forall (sum:Z), forall (count:Z), - ((0%Z <= count)%Z /\ (((sqr count) <= x)%Z /\ - (sum = (sqr (count + 1%Z)%Z)))) -> forall (result2:Z), (result2 = sum) -> - ((result2 <= x)%Z -> forall (result3:Z), (result3 = count) -> - forall (count1:Z), (count1 = (result3 + 1%Z)%Z) -> forall (result4:Z), - (result4 = sum) -> forall (result5:Z), (result5 = count1) -> - forall (sum1:Z), (sum1 = ((result4 + (2%Z * result5)%Z)%Z + 1%Z)%Z) -> - (((0%Z <= count1)%Z /\ (((sqr count1) <= x)%Z /\ - (sum1 = (sqr (count1 + 1%Z)%Z)))) -> (0%Z <= (x - count)%Z)%Z))). -(* YOU MAY EDIT THE PROOF BELOW *) -intros. - -Qed. -(* DO NOT EDIT BELOW *) - - diff --git a/examples/programs/isqrt/isqrt.mlw_M_WP_main_1.v b/examples/programs/isqrt/isqrt.mlw_M_WP_main_1.v deleted file mode 100644 index 64131d076..000000000 --- a/examples/programs/isqrt/isqrt.mlw_M_WP_main_1.v +++ /dev/null @@ -1,36 +0,0 @@ -(* Beware! Only edit allowed sections below *) -(* This file is generated by Why3's Coq driver *) -Require Import ZArith. -Require Import Rbase. -Parameter ghost : forall (a:Type), Type. - -Definition unit := unit. - -Parameter ignore: forall (a:Type), a -> unit. - -Implicit Arguments ignore. - -Parameter label_ : Type. - -Parameter at1: forall (a:Type), a -> label_ -> a. - -Implicit Arguments at1. - -Parameter old: forall (a:Type), a -> a. - -Implicit Arguments old. - -Parameter ref : forall (a:Type), Type. - -Definition sqr(x:Z): Z := (x * x)%Z. - -Theorem WP_main : (0%Z <= 17%Z)%Z /\ forall (result:Z), ((0%Z <= result)%Z /\ - (((sqr result) <= 17%Z)%Z /\ (17%Z < (sqr (result + 1%Z)%Z))%Z)) -> - (result = 4%Z). -(* YOU MAY EDIT THE PROOF BELOW *) -intros. - -Qed. -(* DO NOT EDIT BELOW *) - - diff --git a/examples/programs/isqrt/isqrt.mlw_M_WP_main_2.v b/examples/programs/isqrt/isqrt.mlw_M_WP_main_2.v deleted file mode 100644 index 9bbadd484..000000000 --- a/examples/programs/isqrt/isqrt.mlw_M_WP_main_2.v +++ /dev/null @@ -1,39 +0,0 @@ -(* Beware! Only edit allowed sections below *) -(* This file is generated by Why3's Coq driver *) -Require Import ZArith. -Require Import Rbase. -Parameter ghost : forall (a:Type), Type. - -Definition unit := unit. - -Parameter ignore: forall (a:Type), a -> unit. - -Implicit Arguments ignore. - -Parameter label_ : Type. - -Parameter at1: forall (a:Type), a -> label_ -> a. - -Implicit Arguments at1. - -Parameter old: forall (a:Type), a -> a. - -Implicit Arguments old. - -Parameter ref : forall (a:Type), Type. - -Definition sqr(x:Z): Z := (x * x)%Z. - -Theorem WP_main : (0%Z <= 17%Z)%Z -> forall (result:Z), ((0%Z <= result)%Z /\ - (((sqr result) <= 17%Z)%Z /\ (17%Z < (sqr (result + 1%Z)%Z))%Z)) -> - (result = 4%Z). -(* YOU MAY EDIT THE PROOF BELOW *) -intros. -assert (h:(result < 4 \/ result = 4 \/ result > 4)%Z) by omega. -destruct h as [h1|[h2|h3]]; auto. - - -Qed. -(* DO NOT EDIT BELOW *) - - diff --git a/examples/programs/isqrt/project.db b/examples/programs/isqrt/project.db deleted file mode 100644 index 7d3758ee97aced863c9974289daf67546540d5a8..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 19456 zcmeHPU2Gi19iQ3p-Pul@FCUnYm>i`Ln>c2^c6JvC!HHcOK?0_=rHTsrP>D*YLWowNQYb3rfl~TFDQZDNLjBL(jlJi! z$WfI7$z7t`+uzP_=0E@Wf6eZlKX>DGGxMgF&CVUw^EH8b5XR{0S`8s@GirbJ!70u` z`Oi7H__1V(S~~? zfsdsIdMgAC-Kvit*XzmzZPiESx0|_JXSdVwh?PnNt-ni@dk7j#W>2gl1P!|et2{WV z&m28|WG1__f(be&xjhk0|GyuRf04hEKapq1W8{bA{*UFvyFzs}a29A_utK)s`8j>8 z-Ym*zW{=eeHk8TeG7t}zprJW6Z|08aBh$y{W@oedRDTcIh~e|?X0Fml$Pm7DRv)QP zuJ*_hj>`$40P{QnZ<{pX+xcm(Qzr_Ta4cc<9Zz$a1zeb%XM z`md}fTd~XTjr3nGllAy6QL2zZ4C%jTH8{O%K~2j%un0Wz~=w1|DWlL-ko1p11$}#As6B$_s6+=^Ml=c^Ia?HYT#_r zz=n<1|4Fm>Ur*j8|L*Ps&ZhP6&h>26z&Z)DUV9O|t=VAr|0Vnc!cTb2`?B{6IdwK_ zYAzj zwHx;D**mfSQ0>~OL$!&62d>|<4~ToG_8k~&wLPYfn%aS>n+}ZL;FX8AZNrBeW7SW< zKGICr&54udSYno)lD5&8T^zApjsbJ@W>Oj22I7;MW2rfn8xSOHo%XbPI=FAojR&Vd z?8&K{TGN@f{n(bZ>-R06p}jP^FxXQW8Xd(8x*>A=o%Qy!Qk%f-*J>l}=bfo<8D~k2 z3#C$J=n9ZZG-ka*J3FU#xV(}U+MBd#qy1800uAj9kar;ezl_K~$ZO&5{fOLxr{Lq6^h*0H zLqkJ&VQVAyHy(L5-UiwteFLhE*h6Pwz0ook%*%b1q2Xb?Fx^Zst>>)ndF$%7!5j+l z*tWZ~vk_Zu?Z7T;kJVaWPLM-o$feuxJu?kKmOUI^c3No@YuUxxNITG(l=hBtuBEFU zmMV?0T76#6pR6y=VK%PM9x?C@)K)1nHa`QE22?HAjhPf`i*#Don}x>$t2EZ~o{7fX z8qc*GZ@q2vXh5}*WsKe4K>xZY4+e~t}e)4ET#<6Ar zvRGG*E^O&-tjEI1reU-{)o;(w_5QYbEW7BkcTT(SH>V~W8t2-N9oKW_So5~Oo78CY z`5)8(@0>|)-Wgp9abp>VUO)Z`1$ZK;(`0Yu&xp)j(GRXMhIQ!qfkY$Hy<5 zsh^meA3u8J4(tCL&=rV0MIIyx+3vmV{o4DwchK8{|Av2#zl5joI`krX7@dGd?Jv2Z z0$Ym<_hLjof5UXMM<$d`wF$CNDIJEwhYx9($sh?>B4gnrvEH(_0Luf`Q9W~PT>62K zGEI1v@q{K>tfhc=NmHey$QVarU4bNwib9scP+agdOl2e^=pfT3qDn`xKw@oy#Dxl} zO4F34I;D~e!F3SRltv(_2|^fYO@YMxh{i!2&@}VYAdNyl%%~PHDG*OeUm}0Nk}iTd z;U!J5AP86xMzL>V$^sQ+Nh}TJhDFpQNd&ajE6`|2Da`^9CuRwY!;CSS$w-G<_&P}= zh2$zrvwB||Et1^$q4uLhNFStS0ZVC26UI#zCP~7O>@TvyI8m{mBs7qL^i`7iTnShQ ztpi^snW0Gb6%;%LQ!Q0g;^?|L_uUC6$%z0*;`~OnVKl060{Z=%`z!Khl$Z5 zhQ-KWu1HpjET0LTi8xX;4MG#eL6pQSPC3}i24tn!bnF&yHU^oRaxt|40 z!b*pU4naavWHD`Yz>K0YlmRuN09zJdTY!Mwm@Gidv#d>f;pccQKLKy>{g6g1i9sid zC6v)L0YXUQh|&OYY$?MnO2Z+!)IOJ4N;L=LGdxNem|q~M5j;{nMb`hAtH@^6~@#AX#h5u1mGfuX&x~OZgGB*)q%TjEV4Rq_w$OZ4s2?u$m+nR z&MmS|Z&R0_V_Dn5I?9Vy&&C`7G=~Ht6%!DdAd+jyj5_j#i6V%;knK=dwcJtQmfE=~ zi+u^vj6qC^sWJ&OCd(ksLm)OHOpzM2%!`59lV_StLFZfxsZnYs^X~QbdFSC*@Q?94z7jSHPoW3?8~<0*$<)6n6CYPl24vENhKhtk zwt&bQz)TE;CkjamQk4=b@q9?05;8#wAr11qNTNt+3Q0Ecjna~bNb!|;G7EGpLNJmr zWKbd4q9QOXO@fHYB#3>a*h)M>71ReBaz7U-1Ivdvn?@o9d6l9@a-`@=Jg#Ey+k~2m zOc|LmNJg20AfHeURZT#Vx@;vL^BH($q9AEyVJ6bl$TZD@)H)vxs7+eqmS+=x-;zGF zkOm1&4dm_&de9<-xSpsCiVw&sG(>WHk;OtkqqgixIke|A%S>VfL;w+nngy z{UBp)E3!^MmVc>b*?78?Cs+sZbaVw;2k~^o$+$FH2k~@kk<~#wy`;$MAf8@aWOWcv zKV4*!Ar!=?G-i=bOe%!|MFgotVn=~=`mK<>(vsR^R0nHyMUi#-wGx**0aq>R zPr^1RRZ>BK)38JF!5kpub8aF7Wp5lI5fw-R;%g$q#6XEdMHoXWf?Z9@V@3lWXJLp$ zSRipspdyW7e;_g%Nysz|(sHO^V~RvjAhE=kS(L^w43tigi5P4;mEutG`>UyX+w32Vz z>(Jgj+UL+dD}x)Y-=X~=+Rk4-XkXtRSk*-Fz$)kgRad)4tMeTWICLP7u5oCemm6lS zL;G{+DD=YwBEd%wscQzdhfK$Q`2nx z_UbvV?=^Wj&UNToJF%9+b`Q1C!)xt`FYGw}gFp1|=x{`vL8dtjc-~^y@SFcdO>T7P zx*R%yx1eG47J+a7UE|#hx&QaxYhH;&q(rVK7vVpWyUDlUF9Q6^+XTN0eiq+>-@qC_ zhVR4I5`!PYedsOp7T)4LY>ywJf&MSMuI_eCH9w4&9>p}W1DV+0PJ$f3A;g@bqG%&>ZuL$9`I%T#dnatBZ5`ta(_FLqQf zb60nia&{g%beA;(=cboBbQ1o!#3Cvkx+`zD=R0)09o4z%CWo%I+Iy%KDmFWGT@Ll$ zLwkza^S-;1PND5Ew1vY;3g7CwpRi&(QAQlPE02ykba!rwWD}}D_ti0XaaV5b;X>mp zGSzW+buxFgy3L^z7Im83?$F)&wmTfUGjAExp;y@zay>AI?zE`0PVUgF^KFGgCvq!< Ss>;EWIk@UObhkxY9sdUq(+@oW diff --git a/examples/programs/power/power.mlw_Power_Power_mult_1.v b/examples/programs/power/power.mlw_Power_Power_mult_1.v index 201a2b5fa..b93242742 100644 --- a/examples/programs/power/power.mlw_Power_Power_mult_1.v +++ b/examples/programs/power/power.mlw_Power_Power_mult_1.v @@ -1,22 +1,26 @@ -(* Beware! Only edit allowed sections below *) (* This file is generated by Why3's Coq driver *) +(* Beware! Only edit allowed sections below *) Require Import ZArith. Require Import Rbase. Definition unit := unit. Parameter ignore: forall (a:Type), a -> unit. + Implicit Arguments ignore. Parameter label_ : Type. Parameter at1: forall (a:Type), a -> label_ -> a. + Implicit Arguments at1. Parameter old: forall (a:Type), a -> a. + Implicit Arguments old. Parameter power: Z -> Z -> Z. + Axiom Power_0 : forall (x:Z), ((power x 0%Z) = 1%Z). Axiom Power_s : forall (x:Z) (n:Z), (0%Z < n)%Z -> ((power x diff --git a/examples/programs/power/power.mlw_Power_Power_mult_2.v b/examples/programs/power/power.mlw_Power_Power_mult_2.v deleted file mode 100644 index a3f2258f0..000000000 --- a/examples/programs/power/power.mlw_Power_Power_mult_2.v +++ /dev/null @@ -1,44 +0,0 @@ -(* Beware! Only edit allowed sections below *) -(* This file is generated by Why3's Coq driver *) -Require Import ZArith. -Require Import Rbase. -Parameter ghost : forall (a:Type), Type. - -Definition unit := unit. - -Parameter ignore: forall (a:Type), a -> unit. - -Implicit Arguments ignore. - -Parameter label_ : Type. - -Parameter at1: forall (a:Type), a -> label_ -> a. - -Implicit Arguments at1. - -Parameter old: forall (a:Type), a -> a. - -Implicit Arguments old. - -Parameter power: Z -> Z -> Z. - - -Axiom Power_0 : forall (x:Z), ((power x 0%Z) = 1%Z). - -Axiom Power_s : forall (x:Z) (n:Z), (0%Z < n)%Z -> ((power x - n) = (x * (power x (n - 1%Z)%Z))%Z). - -Axiom Power_1 : forall (x:Z), ((power x 1%Z) = x). - -Axiom Power_sum : forall (x:Z) (n:Z) (m:Z), (0%Z <= n)%Z -> ((0%Z <= m)%Z -> - ((power x (n + m)%Z) = ((power x n) * (power x m))%Z)). - -Theorem Power_mult : forall (x:Z) (n:Z) (m:Z), (0%Z <= n)%Z -> - ((0%Z <= m)%Z -> ((power x (n * m)%Z) = (power (power x n) m))). -(* YOU MAY EDIT THE PROOF BELOW *) -admit. - -Qed. -(* DO NOT EDIT BELOW *) - - diff --git a/examples/programs/power/power.mlw_Power_Power_sum_1.v b/examples/programs/power/power.mlw_Power_Power_sum_1.v index 1b92571bb..b6280e815 100644 --- a/examples/programs/power/power.mlw_Power_Power_sum_1.v +++ b/examples/programs/power/power.mlw_Power_Power_sum_1.v @@ -1,22 +1,26 @@ -(* Beware! Only edit allowed sections below *) (* This file is generated by Why3's Coq driver *) +(* Beware! Only edit allowed sections below *) Require Import ZArith. Require Import Rbase. Definition unit := unit. Parameter ignore: forall (a:Type), a -> unit. + Implicit Arguments ignore. Parameter label_ : Type. Parameter at1: forall (a:Type), a -> label_ -> a. + Implicit Arguments at1. Parameter old: forall (a:Type), a -> a. + Implicit Arguments old. Parameter power: Z -> Z -> Z. + Axiom Power_0 : forall (x:Z), ((power x 0%Z) = 1%Z). Axiom Power_s : forall (x:Z) (n:Z), (0%Z < n)%Z -> ((power x diff --git a/examples/programs/power/power.mlw_Power_Power_sum_2.v b/examples/programs/power/power.mlw_Power_Power_sum_2.v deleted file mode 100644 index de2b20c4e..000000000 --- a/examples/programs/power/power.mlw_Power_Power_sum_2.v +++ /dev/null @@ -1,53 +0,0 @@ -(* Beware! Only edit allowed sections below *) -(* This file is generated by Why3's Coq driver *) -Require Import ZArith. -Require Import Rbase. -Parameter ghost : forall (a:Type), Type. - -Definition unit := unit. - -Parameter ignore: forall (a:Type), a -> unit. - -Implicit Arguments ignore. - -Parameter label_ : Type. - -Parameter at1: forall (a:Type), a -> label_ -> a. - -Implicit Arguments at1. - -Parameter old: forall (a:Type), a -> a. - -Implicit Arguments old. - -Parameter power: Z -> Z -> Z. - - -Axiom Power_0 : forall (x:Z), ((power x 0%Z) = 1%Z). - -Axiom Power_s : forall (x:Z) (n:Z), (0%Z < n)%Z -> ((power x - n) = (x * (power x (n - 1%Z)%Z))%Z). - -Axiom Power_1 : forall (x:Z), ((power x 1%Z) = x). - -Theorem Power_sum : forall (x:Z) (n:Z) (m:Z), (0%Z <= n)%Z -> - ((0%Z <= m)%Z -> ((power x (n + m)%Z) = ((power x n) * (power x m))%Z)). -(* YOU MAY EDIT THE PROOF BELOW *) -intros x n m Hn Hm. -generalize Hm. -pattern m. -apply Z_lt_induction; auto. -intros n0 Hind Hn0. -assert (h:(n0 = 0 \/ n0 > 0)%Z) by omega. -destruct h. -subst n0; rewrite Power_0; ring_simplify (n+0)%Z; ring. -rewrite Power_s; auto with zarith. -replace (n+n0-1)%Z with (n+(n0-1))%Z by omega. -rewrite Hind; auto with zarith. -rewrite (Power_s x n0). -ring. -omega. -Qed. -(* DO NOT EDIT BELOW *) - - diff --git a/examples/programs/power/project.db b/examples/programs/power/project.db deleted file mode 100644 index 68991aea77a709abe7b57b9fc996757520770b5c..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 15360 zcmeHNU2Ggj9iNZ8J^TEb_|hXmZa0D|w(OeyoZS^Fi5-r}C3chGsEt%OW_D-OQ*2*y zdv-o}x|Y5nA)zAR0TuBfq&~nCqEad(sv?90hzFz+34!2&Z&86-6p0sRc5m(7%ZJk! zTDd#2cXxjCpa0DNH#7U6o&SC6?CDmQt6{sdLA$C6N&rG|LRA3(FN*(c8WtIt0kY2- z_|C_&tcd?B3r3RLoiYVdFi%pDPb@jwKguVx5DcqSY+sW_c7kN*q%ff97{8gX$zjNKn$k*_7%DQ zEBH$Qzm5Nle~W*GZ{qKYY>^5E3I^U42Bs=_4t6_qGfFn)t@dUF4=Q+e0EAOzA;_vE!pC{XXc0eFX!32FCGG zxV!w}82mms0!I-30q)^vu!cW@kKmWkHu?fCp?{*!qBqcw(G$o*FQbRy-_Q{JH5`Fo zgU`ba_|!h*^ofUtMDPQ`%5^MaAjg06_G@2!X68Tq8WjgBJo(ZyLP0nYYdA+n&WRJx@w106e^;H&)@jNsqfW3SNlMUVsT7! z{HN8&FMsQeYOS84P@*p;vIu}jGqj8BLz!&BA3EJa5$D6Wm9@UU#*+x-Ekrsz;cxTd6Nxs1Sx4_jaVhUBTV zgJOw(>|o4Zc?Zqv#XBgHvZr2~5yJQ@U_#dEry5FyN=Q)g!({YDVKOY0w6v^970SQ= zB8rw_AH9m?O#NLgw&R`6)M#r%PSi|nZlZ|IrGrx33kKc~42)06@BcD<9l+O-j-E$< z#Mj;rcJD76FTqOv@L|}~yOgc-6Tfx5i9);QHT zr=B^tys~)ig8IqE1$FWK+LOzxqT)(pb#1;cyGb{=y4HAlZT1XO>T`4OLflq#MSMr{ zX2h>-@lBr(WO1(bfx;Q7a$eM&{WPxB=S25$Yct^2G7X9z_OqqFrt_=IXU{i8w?E!^ zx^GTX>XDM_ldFRk%A(ocRH;&*orOIbcR7Eup3jwY9nP1jGx_|3(Kk?Mm&RVXT&aIl z^vaB_zKfi+DGw`mV<9h+V3DGl!9udUa!O6vH0B|hdkrUSnf?9L+XsYJ=kkKmdw1&mElT#dK&hc ziHqsSS<`syXs)po74Ksycm2Uy?90lAQ?EU*_Q6a?E-1p6&cWweaYqJ%!von$u3H0z z>P#MZuwKd&<&0#yd)VD+%&SqCcDJG(8`>;tuXFJW)c#gvzS|Nz4Y6xEJRmsIh250$gk87T#2O+1r!)(nqsTR1*G91S>JWKOkur#)p4wt($AYRD0t+`D19gXOoXSt4P zQ_6)Zur#`t4##C7Gku5px?|GNC(JVp;`=^x^g#Da3oMQ7rGprTV+XdSxfb=z&~Zt? zbaUOH^c4K2ekd}bH{b6l>u-0?k1n4vKz)IzW{yq6A(+hNEE3p~T; zu3=JQT8wj3rz8wqE3m=R&|W%BPAtKP#+YM@LDo5O17hk1A)NWT#eA?-*-MAPZDKjD z<(MAxY=<)6wGGb+84bmqcw%goy>#fhYuPTRM0d5&5fj7?sqXroX$GNf^H2jP%2J27 z0ui|TMCHN?OAm?33}P9foDe4U94qvQZTh|r?2^>*p#crlC00n8Zt7xIGb3<030+O& zj5vlch5!r8YDZT@q%MgR%NVigQqQHtAg*U|-R3ss8W-eQp-UX@GGHQE>yh1B;u}LJ z#Bs%R@dF|0`k`e8KBo?0b|~rQK!>u@2X`y!0imW~k$Q5ac~lHYV2NoG_`2t~lrxa{ z|C<2cyyp@x3JL}a2HtxNoSc-a{l2bO4?TytwioDOU>cgu88`G$I2r1bfD*#M{{WDp B20j1) diff --git a/examples/programs/power/why3session.xml b/examples/programs/power/why3session.xml index 85efebccc..df00d4bcd 100644 --- a/examples/programs/power/why3session.xml +++ b/examples/programs/power/why3session.xml @@ -1,8 +1,8 @@ - + - + @@ -17,7 +17,10 @@ - + + + + @@ -31,7 +34,10 @@ - + + + + -- GitLab