bitvectors: more proofs

examples/bitvectors/bitvector/bitvector_BitVector_nth_from_int2c_plus_pow2_1.v

 (* This file is generated by Why3's Coq 8.4 driver *)
 (* Beware! Only edit allowed sections below    *)
 Require Import BuiltIn.
-Require Import ZOdiv.
 Require BuiltIn.
 Require bool.Bool.
 Require int.Int.
 Require int.Abs.
-Require int.ComputerDivision.
+Require int.EuclideanDivision.
 
 Parameter pow2: Z -> Z.
 
@@ -150,15 +149,26 @@ Axiom pow2_62 : ((pow2 62%Z) = 4611686018427387904%Z).
 
 Axiom pow2_63 : ((pow2 63%Z) = 9223372036854775808%Z).
 
-Axiom Div_pow : forall (x:Z) (i:Z), (((pow2 (i - 1%Z)%Z) <= x)%Z /\
-  (x < (pow2 i))%Z) -> ((ZOdiv x (pow2 (i - 1%Z)%Z)) = 1%Z).
+Axiom Div_double : forall (x:Z) (y:Z), (((0%Z < y)%Z /\ (y <= x)%Z) /\
+  (x < (2%Z * y)%Z)%Z) -> ((int.EuclideanDivision.div x y) = 1%Z).
 
-Axiom Div_pow2 : forall (x:Z) (i:Z), (((-(pow2 i))%Z <= x)%Z /\
-  (x < (-(pow2 (i - 1%Z)%Z))%Z)%Z) ->
-  ((ZOdiv x (pow2 (i - 1%Z)%Z)) = (-2%Z)%Z).
+Axiom Div_pow : forall (x:Z) (i:Z), (0%Z < i)%Z ->
+  ((((pow2 (i - 1%Z)%Z) <= x)%Z /\ (x < (pow2 i))%Z) ->
+  ((int.EuclideanDivision.div x (pow2 (i - 1%Z)%Z)) = 1%Z)).
 
-Axiom Mod_pow2_gen : forall (x:Z) (i:Z) (k:Z), ((0%Z <= k)%Z /\ (k < i)%Z) ->
-  ((ZOmod (ZOdiv (x + (pow2 i))%Z (pow2 k)) 2%Z) = (ZOmod (ZOdiv x (pow2 k)) 2%Z)).
+Axiom Div_double_neg : forall (x:Z) (y:Z), (((((-2%Z)%Z * y)%Z <= x)%Z /\
+  (x < (-y)%Z)%Z) /\ ((-y)%Z < 0%Z)%Z) -> ((int.EuclideanDivision.div x
+  y) = (-2%Z)%Z).
+
+Axiom Div_pow2 : forall (x:Z) (i:Z), (0%Z < i)%Z ->
+  ((((-(pow2 i))%Z <= x)%Z /\ (x < (-(pow2 (i - 1%Z)%Z))%Z)%Z) ->
+  ((int.EuclideanDivision.div x (pow2 (i - 1%Z)%Z)) = (-2%Z)%Z)).
+
+Axiom Mod_pow2_gen : forall (x:Z) (i:Z) (k:Z), (0%Z <= x)%Z ->
+  (((0%Z <= k)%Z /\ (k < i)%Z) ->
+  ((int.EuclideanDivision.mod1 (int.EuclideanDivision.div (x + (pow2 i))%Z
+  (pow2 k)) 2%Z) = (int.EuclideanDivision.mod1 (int.EuclideanDivision.div x
+  (pow2 k)) 2%Z))).
 
 Parameter size: Z.
 
@@ -287,18 +297,19 @@ Axiom to_nat_sub_footprint : forall (b1:bv) (b2:bv) (j:Z) (i:Z),
 Parameter from_int: Z -> bv.
 
 Axiom nth_from_int_high_even : forall (n:Z) (i:Z), (((i < size)%Z /\
-  (0%Z <= i)%Z) /\ ((ZOmod (ZOdiv n (pow2 i)) 2%Z) = 0%Z)) ->
-  ((nth (from_int n) i) = false).
+  (0%Z <= i)%Z) /\ ((int.EuclideanDivision.mod1 (int.EuclideanDivision.div n
+  (pow2 i)) 2%Z) = 0%Z)) -> ((nth (from_int n) i) = false).
 
 Axiom nth_from_int_high_odd : forall (n:Z) (i:Z), (((i < size)%Z /\
-  (0%Z <= i)%Z) /\ ~ ((ZOmod (ZOdiv n (pow2 i)) 2%Z) = 0%Z)) ->
-  ((nth (from_int n) i) = true).
+  (0%Z <= i)%Z) /\
+  ~ ((int.EuclideanDivision.mod1 (int.EuclideanDivision.div n (pow2 i))
+  2%Z) = 0%Z)) -> ((nth (from_int n) i) = true).
 
-Axiom nth_from_int_low_even : forall (n:Z), ((ZOmod n 2%Z) = 0%Z) ->
-  ((nth (from_int n) 0%Z) = false).
+Axiom nth_from_int_low_even : forall (n:Z), ((int.EuclideanDivision.mod1 n
+  2%Z) = 0%Z) -> ((nth (from_int n) 0%Z) = false).
 
-Axiom nth_from_int_low_odd : forall (n:Z), (~ ((ZOmod n 2%Z) = 0%Z)) ->
-  ((nth (from_int n) 0%Z) = true).
+Axiom nth_from_int_low_odd : forall (n:Z), (~ ((int.EuclideanDivision.mod1 n
+  2%Z) = 0%Z)) -> ((nth (from_int n) 0%Z) = true).
 
 Axiom nth_from_int_0 : forall (i:Z), ((i < size)%Z /\ (0%Z <= i)%Z) ->
   ((nth (from_int 0%Z) i) = false).
@@ -313,19 +324,20 @@ Axiom nth_sign_negative : forall (n:Z), (n < 0%Z)%Z -> ((nth (from_int2c n)
 
 Axiom nth_from_int2c_high_even : forall (n:Z) (i:Z),
   (((i < (size - 1%Z)%Z)%Z /\ (0%Z <= i)%Z) /\
-  ((ZOmod (ZOdiv n (pow2 i)) 2%Z) = 0%Z)) -> ((nth (from_int2c n)
-  i) = false).
+  ((int.EuclideanDivision.mod1 (int.EuclideanDivision.div n (pow2 i))
+  2%Z) = 0%Z)) -> ((nth (from_int2c n) i) = false).
 
 Axiom nth_from_int2c_high_odd : forall (n:Z) (i:Z),
   (((i < (size - 1%Z)%Z)%Z /\ (0%Z <= i)%Z) /\
-  ~ ((ZOmod (ZOdiv n (pow2 i)) 2%Z) = 0%Z)) -> ((nth (from_int2c n)
-  i) = true).
+  ~ ((int.EuclideanDivision.mod1 (int.EuclideanDivision.div n (pow2 i))
+  2%Z) = 0%Z)) -> ((nth (from_int2c n) i) = true).
 
-Axiom nth_from_int2c_low_even : forall (n:Z), ((ZOmod n 2%Z) = 0%Z) ->
-  ((nth (from_int2c n) 0%Z) = false).
+Axiom nth_from_int2c_low_even : forall (n:Z), ((int.EuclideanDivision.mod1 n
+  2%Z) = 0%Z) -> ((nth (from_int2c n) 0%Z) = false).
 
-Axiom nth_from_int2c_low_odd : forall (n:Z), (~ ((ZOmod n 2%Z) = 0%Z)) ->
-  ((nth (from_int2c n) 0%Z) = true).
+Axiom nth_from_int2c_low_odd : forall (n:Z),
+  (~ ((int.EuclideanDivision.mod1 n 2%Z) = 0%Z)) -> ((nth (from_int2c n)
+  0%Z) = true).
 
 Axiom nth_from_int2c_0 : forall (i:Z), ((i < size)%Z /\ (0%Z <= i)%Z) ->
   ((nth (from_int2c 0%Z) i) = false).
@@ -341,8 +353,8 @@ Theorem nth_from_int2c_plus_pow2 : forall (x:Z) (k:Z) (i:Z),
 (* intros x k i ((h1,h2),h3). *)
 
 intros x k i (h1 & h2).
-assert (h: ZOmod (ZOdiv x (pow2 k)) 2 = 0 \/
-           ZOmod (ZOdiv x (pow2 k)) 2 <> 0) 
+assert (h: int.EuclideanDivision.mod1 (int.EuclideanDivision.div x (pow2 k)) 2 = 0 \/
+           int.EuclideanDivision.mod1 (int.EuclideanDivision.div x (pow2 k)) 2 <> 0) 
   by omega.
 destruct h.
 rewrite nth_from_int2c_high_even; intuition.

examples/bitvectors/double/why3session.xml

@@ -50,7 +50,7 @@
     name="nth_one1"
     locfile="../double.why"
     loclnum="73" loccnumb="8" loccnume="16"
-    sum="64b742f26230c95a6f017247e361064e"
+    sum="52d8a3fb72c7fbd67b6242f14de4ec07"
     proved="true"
     expanded="true"
     shape="ainfix =anthaoneV0aFalseIainfix <=V0c51Aainfix <=c0V0F">
@@ -75,7 +75,7 @@
     name="nth_one2"
     locfile="../double.why"
     loclnum="74" loccnumb="8" loccnume="16"
-    sum="84a85185c5147202068cebe22848d18f"
+    sum="5d9e03517d2cc0bf19926e772b281575"
     proved="true"
     expanded="true"
     shape="ainfix =anthaoneV0aTrueIainfix <=V0c61Aainfix <=c52V0F">
@@ -100,7 +100,7 @@
     name="nth_one3"
     locfile="../double.why"
     loclnum="75" loccnumb="8" loccnume="16"
-    sum="3fa54a156946495d247aa0b4e5d2308b"
+    sum="f5f820393566394effd1eecae3fa8ef8"
     proved="true"
     expanded="false"
     shape="ainfix =anthaoneV0aFalseIainfix <=V0c63Aainfix <=c62V0F">
@@ -117,7 +117,7 @@
     name="sign_one"
     locfile="../double.why"
     loclnum="77" loccnumb="8" loccnume="16"
-    sum="be9ca7041b727df4ca7493d2af0cd4c6"
+    sum="c88fd3753e8153b90619ca7be5ed1117"
     proved="true"
     expanded="false"
     shape="ainfix =asignaoneaFalse">
@@ -166,7 +166,7 @@
     name="exp_one"
     locfile="../double.why"
     loclnum="78" loccnumb="8" loccnume="15"
-    sum="a95859f4aee7c4d050a5a4db5dd9c1fd"
+    sum="62a94560121b0bf05e66471064063151"
     proved="true"
     expanded="false"
     shape="ainfix =aexpaonec1023">
@@ -192,7 +192,7 @@
     name="mantissa_one"
     locfile="../double.why"
     loclnum="79" loccnumb="8" loccnume="20"
-    sum="1e2b71c93f02723b910f5b0520c73873"
+    sum="8f958039e1df42ec82b32367fcd739c7"
     proved="true"
     expanded="false"
     shape="ainfix =amantissaaonec0">
@@ -225,7 +225,7 @@
     name="double_value_of_1"
     locfile="../double.why"
     loclnum="81" loccnumb="8" loccnume="25"
-    sum="ad540400343cee2ffb0b8a07d70165cf"
+    sum="8058d2bf7c95995fe09bb6908781d19f"
     proved="true"
     expanded="false"
     shape="ainfix =adouble_of_bv64aonec1.0">

examples/bitvectors/neg_as_xor/why3session.xml

@@ -35,7 +35,7 @@
     name="Nth_j"
     locfile="../neg_as_xor.why"
     loclnum="13" loccnumb="8" loccnume="13"
-    sum="34b383120a6c9582c26cf0005c710a92"
+    sum="6c8374d08ad76160b6097f0c92f918f8"
     proved="true"
     expanded="true"
     shape="ainfix =anthajV0aFalseIainfix <=V0c62Aainfix <=c0V0F">
@@ -60,7 +60,7 @@
     name="sign_of_j"
     locfile="../neg_as_xor.why"
     loclnum="15" loccnumb="8" loccnume="17"
-    sum="8874135905e94507fde3c62c691db581"
+    sum="1760b20625d63815ec0aa452d6ad34d1"
     proved="true"
     expanded="false"
     shape="ainfix =asignajaTrue">
@@ -77,7 +77,7 @@
     name="mantissa_of_j"
     locfile="../neg_as_xor.why"
     loclnum="16" loccnumb="8" loccnume="21"
-    sum="7a9b27b0536d17d854cf27f8234d761b"
+    sum="a3e5fd7d3642b40f5cc15957027b57c3"
     proved="true"
     expanded="false"
     shape="ainfix =amantissaajc0">
@@ -103,14 +103,14 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="3.10"/>
+     <result status="valid" time="2.68"/>
     </proof>
    </goal>
    <goal
     name="exp_of_j"
     locfile="../neg_as_xor.why"
     loclnum="17" loccnumb="8" loccnume="16"
-    sum="d30d723f5c789d43e3644685e0f09ad3"
+    sum="3b531125475692b4d418a663a72c1838"
     proved="true"
     expanded="false"
     shape="ainfix =aexpajc0">
@@ -143,7 +143,7 @@
     name="int_of_bv"
     locfile="../neg_as_xor.why"
     loclnum="18" loccnumb="8" loccnume="17"
-    sum="a5352ad948c731bc7e1b1d044870bb95"
+    sum="65a13df3701b2fbbbaf06857bd5fece6"
     proved="true"
     expanded="false"
     shape="ainfix =adouble_of_bv64ajc0.0">
@@ -176,7 +176,7 @@
     name="MainResultBits"
     locfile="../neg_as_xor.why"
     loclnum="20" loccnumb="8" loccnume="22"
-    sum="52f645e44bf665a7bc0953d0ab22cbec"
+    sum="be8ed15fd950211d237c83c4aa76424a"
     proved="true"
     expanded="false"
     shape="ainfix =anthabw_xorV0ajV1anthV0V1Iainfix &lt;V1c63Aainfix &lt;=c0V1FF">
@@ -193,7 +193,7 @@
     name="MainResultSign"
     locfile="../neg_as_xor.why"
     loclnum="23" loccnumb="8" loccnume="22"
-    sum="84408f58ca669e966ac3dd0e8e26c501"
+    sum="634a2fb3ae42a2e5996ab58a4428682c"
     proved="true"
     expanded="false"
     shape="ainfix =anthabw_xorV0ajc63anotbanthV0c63F">
@@ -210,7 +210,7 @@
     name="Sign_of_xor_j"
     locfile="../neg_as_xor.why"
     loclnum="25" loccnumb="8" loccnume="21"
-    sum="8e35e7b3978720fcffa4654f4d40a8bb"
+    sum="083892c9a58aff7b918bc3d5aca51d8e"
     proved="true"
     expanded="false"
     shape="ainfix =asignabw_xorV0ajanotbasignV0F">
@@ -243,7 +243,7 @@
     name="Exp_of_xor_j"
     locfile="../neg_as_xor.why"
     loclnum="27" loccnumb="8" loccnume="20"
-    sum="bd2a20ad78883a9b246d819dfc050046"
+    sum="e23bdb76d6bcfd9e06cfe30f4eea16e7"
     proved="true"
     expanded="false"
     shape="ainfix =aexpabw_xorV0ajaexpV0F">
@@ -276,7 +276,7 @@
     name="Mantissa_of_xor_j"
     locfile="../neg_as_xor.why"
     loclnum="29" loccnumb="8" loccnume="25"
-    sum="ce1ceaaaf0b5d079ac350e484e3a5051"
+    sum="6294006381c02dc3f9556ae437087baa"
     proved="true"
     expanded="false"
     shape="ainfix =amantissaabw_xorV0ajamantissaV0F">
@@ -309,7 +309,7 @@
     name="MainResultZero"
     locfile="../neg_as_xor.why"
     loclnum="31" loccnumb="8" loccnume="22"
-    sum="e71da47a4d26e5f9bb78680af2110e9d"
+    sum="f6fbb4d35e0473dc1e92b447b37a3189"
     proved="true"
     expanded="false"
     shape="ainfix =adouble_of_bv64abw_xorV0ajaprefix -.adouble_of_bv64V0Iainfix =amantissaV0c0Aainfix =c0aexpV0F">
@@ -342,7 +342,7 @@
     name="sign_neg"
     locfile="../neg_as_xor.why"
     loclnum="34" loccnumb="8" loccnume="16"
-    sum="1a8d522bc703c9be8a1629374fd9d762"
+    sum="e4ee54c231d60fa6ef6184307c4a30c3"
     proved="true"
     expanded="false"
     shape="ainfix =asign_valueanotbasignV0aprefix -.asign_valueasignV0F">
@@ -359,7 +359,7 @@
     name="MainResult"
     locfile="../neg_as_xor.why"
     loclnum="36" loccnumb="8" loccnume="18"
-    sum="172f68d15ea46e505257c40efb1e8b07"
+    sum="6826df4299dee21a669e748d7738a8c4"
     proved="true"
     expanded="true"
     shape="ainfix =adouble_of_bv64abw_xorV0ajaprefix -.adouble_of_bv64V0Iainfix &lt;aexpV0c2047Aainfix &lt;c0aexpV0F">

examples/bitvectors/power2/power2_Pow2int_Mod_pow2_gen_1.v

+(* This file is generated by Why3's Coq 8.4 driver *)
+(* Beware! Only edit allowed sections below    *)
+Require Import BuiltIn.
+Require BuiltIn.
+Require int.Int.
+Require int.Abs.
+Require int.EuclideanDivision.
+
+Parameter pow2: Z -> Z.
+
+Axiom Power_0 : ((pow2 0%Z) = 1%Z).
+
+Axiom Power_s : forall (n:Z), (0%Z <= n)%Z ->
+  ((pow2 (n + 1%Z)%Z) = (2%Z * (pow2 n))%Z).
+
+Axiom Power_1 : ((pow2 1%Z) = 2%Z).
+
+Axiom Power_sum : forall (n:Z) (m:Z), ((0%Z <= n)%Z /\ (0%Z <= m)%Z) ->
+  ((pow2 (n + m)%Z) = ((pow2 n) * (pow2 m))%Z).
+
+Axiom pow2pos : forall (i:Z), (0%Z <= i)%Z -> (0%Z < (pow2 i))%Z.
+
+Axiom pow2_0 : ((pow2 0%Z) = 1%Z).
+
+Axiom pow2_1 : ((pow2 1%Z) = 2%Z).
+
+Axiom pow2_2 : ((pow2 2%Z) = 4%Z).
+
+Axiom pow2_3 : ((pow2 3%Z) = 8%Z).
+
+Axiom pow2_4 : ((pow2 4%Z) = 16%Z).
+
+Axiom pow2_5 : ((pow2 5%Z) = 32%Z).
+
+Axiom pow2_6 : ((pow2 6%Z) = 64%Z).
+
+Axiom pow2_7 : ((pow2 7%Z) = 128%Z).
+
+Axiom pow2_8 : ((pow2 8%Z) = 256%Z).
+
+Axiom pow2_9 : ((pow2 9%Z) = 512%Z).
+
+Axiom pow2_10 : ((pow2 10%Z) = 1024%Z).
+
+Axiom pow2_11 : ((pow2 11%Z) = 2048%Z).
+
+Axiom pow2_12 : ((pow2 12%Z) = 4096%Z).
+
+Axiom pow2_13 : ((pow2 13%Z) = 8192%Z).
+
+Axiom pow2_14 : ((pow2 14%Z) = 16384%Z).
+
+Axiom pow2_15 : ((pow2 15%Z) = 32768%Z).
+
+Axiom pow2_16 : ((pow2 16%Z) = 65536%Z).
+
+Axiom pow2_17 : ((pow2 17%Z) = 131072%Z).
+
+Axiom pow2_18 : ((pow2 18%Z) = 262144%Z).
+
+Axiom pow2_19 : ((pow2 19%Z) = 524288%Z).
+
+Axiom pow2_20 : ((pow2 20%Z) = 1048576%Z).
+
+Axiom pow2_21 : ((pow2 21%Z) = 2097152%Z).
+
+Axiom pow2_22 : ((pow2 22%Z) = 4194304%Z).
+
+Axiom pow2_23 : ((pow2 23%Z) = 8388608%Z).
+
+Axiom pow2_24 : ((pow2 24%Z) = 16777216%Z).
+
+Axiom pow2_25 : ((pow2 25%Z) = 33554432%Z).
+
+Axiom pow2_26 : ((pow2 26%Z) = 67108864%Z).
+
+Axiom pow2_27 : ((pow2 27%Z) = 134217728%Z).
+
+Axiom pow2_28 : ((pow2 28%Z) = 268435456%Z).
+
+Axiom pow2_29 : ((pow2 29%Z) = 536870912%Z).
+
+Axiom pow2_30 : ((pow2 30%Z) = 1073741824%Z).
+
+Axiom pow2_31 : ((pow2 31%Z) = 2147483648%Z).
+
+Axiom pow2_32 : ((pow2 32%Z) = 4294967296%Z).
+
+Axiom pow2_33 : ((pow2 33%Z) = 8589934592%Z).
+
+Axiom pow2_34 : ((pow2 34%Z) = 17179869184%Z).
+
+Axiom pow2_35 : ((pow2 35%Z) = 34359738368%Z).
+
+Axiom pow2_36 : ((pow2 36%Z) = 68719476736%Z).
+
+Axiom pow2_37 : ((pow2 37%Z) = 137438953472%Z).
+
+Axiom pow2_38 : ((pow2 38%Z) = 274877906944%Z).
+
+Axiom pow2_39 : ((pow2 39%Z) = 549755813888%Z).
+
+Axiom pow2_40 : ((pow2 40%Z) = 1099511627776%Z).
+
+Axiom pow2_41 : ((pow2 41%Z) = 2199023255552%Z).
+
+Axiom pow2_42 : ((pow2 42%Z) = 4398046511104%Z).
+
+Axiom pow2_43 : ((pow2 43%Z) = 8796093022208%Z).
+
+Axiom pow2_44 : ((pow2 44%Z) = 17592186044416%Z).
+
+Axiom pow2_45 : ((pow2 45%Z) = 35184372088832%Z).
+
+Axiom pow2_46 : ((pow2 46%Z) = 70368744177664%Z).
+
+Axiom pow2_47 : ((pow2 47%Z) = 140737488355328%Z).
+
+Axiom pow2_48 : ((pow2 48%Z) = 281474976710656%Z).
+
+Axiom pow2_49 : ((pow2 49%Z) = 562949953421312%Z).
+
+Axiom pow2_50 : ((pow2 50%Z) = 1125899906842624%Z).
+
+Axiom pow2_51 : ((pow2 51%Z) = 2251799813685248%Z).
+
+Axiom pow2_52 : ((pow2 52%Z) = 4503599627370496%Z).
+
+Axiom pow2_53 : ((pow2 53%Z) = 9007199254740992%Z).
+
+Axiom pow2_54 : ((pow2 54%Z) = 18014398509481984%Z).
+
+Axiom pow2_55 : ((pow2 55%Z) = 36028797018963968%Z).
+
+Axiom pow2_56 : ((pow2 56%Z) = 72057594037927936%Z).
+
+Axiom pow2_57 : ((pow2 57%Z) = 144115188075855872%Z).
+
+Axiom pow2_58 : ((pow2 58%Z) = 288230376151711744%Z).
+
+Axiom pow2_59 : ((pow2 59%Z) = 576460752303423488%Z).
+
+Axiom pow2_60 : ((pow2 60%Z) = 1152921504606846976%Z).
+
+Axiom pow2_61 : ((pow2 61%Z) = 2305843009213693952%Z).
+
+Axiom pow2_62 : ((pow2 62%Z) = 4611686018427387904%Z).
+
+Axiom pow2_63 : ((pow2 63%Z) = 9223372036854775808%Z).
+
+Axiom Div_double : forall (x:Z) (y:Z), (((0%Z < y)%Z /\ (y <= x)%Z) /\
+  (x < (2%Z * y)%Z)%Z) -> ((int.EuclideanDivision.div x y) = 1%Z).
+
+Axiom Div_pow : forall (x:Z) (i:Z), (0%Z < i)%Z ->
+  ((((pow2 (i - 1%Z)%Z) <= x)%Z /\ (x < (pow2 i))%Z) ->
+  ((int.EuclideanDivision.div x (pow2 (i - 1%Z)%Z)) = 1%Z)).
+
+Axiom Div_double_neg : forall (x:Z) (y:Z), (((((-2%Z)%Z * y)%Z <= x)%Z /\
+  (x < (-y)%Z)%Z) /\ ((-y)%Z < 0%Z)%Z) -> ((int.EuclideanDivision.div x
+  y) = (-2%Z)%Z).
+
+Axiom Div_pow2 : forall (x:Z) (i:Z), (0%Z < i)%Z ->
+  ((((-(pow2 i))%Z <= x)%Z /\ (x < (-(pow2 (i - 1%Z)%Z))%Z)%Z) ->
+  ((int.EuclideanDivision.div x (pow2 (i - 1%Z)%Z)) = (-2%Z)%Z)).
+
+Open Scope Z_scope.
+
+Require Import Why3.
+Ltac ae := why3 "alt-ergo" timelimit 3.
+
+
+(* Why3 goal *)
+Theorem Mod_pow2_gen : forall (x:Z) (i:Z) (k:Z), ((0%Z <= k)%Z /\
+  (k < i)%Z) ->
+  ((int.EuclideanDivision.mod1 (int.EuclideanDivision.div (x + (pow2 i))%Z
+  (pow2 k)) 2%Z) = (int.EuclideanDivision.mod1 (int.EuclideanDivision.div x
+  (pow2 k)) 2%Z)).
+(* intros x i k (h1,h2). *)
+intros x i k (h1,h2).
+replace (x + pow2 i) with (pow2 k*pow2(i-k)+x).
+  2:ae.
+rewrite int.EuclideanDivision.Div_mult.
+  2:ae.
+replace (pow2 (i-k)) with (2*pow2(i-k-1)).
+  2:ae.
+ae.
+Qed.
+
+

examples/bitvectors/power2/why3session.xml

@@ -37,14 +37,6 @@
   id="8"
   name="Z3"
   version="3.2"/>
- <prover
-  id="9"
-  name="Z3"
-  version="4.2"/>
- <prover
-  id="10"
-  name="Z3"
-  version="4.3.1"/>
  <file
   name="../power2.why"
   verified="false"
@@ -3232,7 +3224,7 @@
     name="Div_double"
     locfile="../power2.why"
     loclnum="113" loccnumb="8" loccnume="18"
-    sum="54ca81fd8dd2cc7b0616dbb62374c1dc"
+    sum="6f01a44c48ae3d43c3c4f83b1d870e98"
     proved="false"
     expanded="true"
     shape="ainfix =adivV0V1c1Iainfix &lt;V0ainfix *c2V1Aainfix &lt;=V1V0Aainfix &lt;c0V1F">
@@ -3241,9 +3233,9 @@
     name="Div_pow"
     locfile="../power2.why"
     loclnum="116" loccnumb="8" loccnume="15"
-    sum="38721ee10b8925bf9da7fdd92bfcadad"
+    sum="94c0d831a4dcda27b2e02ffd748efbcf"
     proved="true"
-    expanded="true"
+    expanded="false"
     shape="ainfix =adivV0apow2ainfix -V1c1c1Iainfix &lt;V0apow2V1Aainfix &lt;=apow2ainfix -V1c1V0Iainfix &gt;V1c0F">
     <proof
      prover="0"
@@ -3259,7 +3251,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.26"/>
+     <result status="valid" time="0.27"/>
     </proof>
     <proof
      prover="2"
@@ -3290,7 +3282,7 @@
     name="Div_double_neg"
     locfile="../power2.why"
     loclnum="119" loccnumb="8" loccnume="22"
-    sum="973e29204b30d40a7bab41c85eb8f9ff"
+    sum="abb5d03ab24579b6ee213167c0a3133c"
     proved="false"
     expanded="true"
     shape="ainfix =adivV0V1aprefix -c2Iainfix &lt;aprefix -V1c0Aainfix &lt;V0aprefix -V1Aainfix &lt;=ainfix *aprefix -c2V1V0F">
@@ -3299,9 +3291,9 @@
     name="Div_pow2"
     locfile="../power2.why"
     loclnum="122" loccnumb="8" loccnume="16"
-    sum="cf96a17cbeab4ecc0a75f7fc5fc09ad3"
+    sum="2c89cfc95fa863dc50eff7a69b9fa7c8"
     proved="true"
-    expanded="true"
+    expanded="false"
     shape="ainfix =adivV0apow2ainfix -V1c1aprefix -c2Iainfix &lt;V0aprefix -apow2ainfix -V1c1Aainfix &lt;=aprefix -apow2V1V0Iainfix &gt;V1c0F">
     <proof
      prover="0"
@@ -3309,7 +3301,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.13"/>
+     <result status="valid" time="0.21"/>
     </proof>
     <proof
      prover="1"
@@ -3317,7 +3309,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.08"/>
+     <result status="valid" time="0.11"/>
     </proof>
     <proof
      prover="2"
@@ -3348,81 +3340,18 @@
     name="Mod_pow2_gen"
     locfile="../power2.why"
     loclnum="129" loccnumb="8" loccnume="20"
-    sum="b227e85b4b94596b025f86278ff9ea72"
-    proved="false"
+    sum="a7a76c1f697e0c3aa10ef9e6d6a80fc0"
+    proved="true"
     expanded="true"
     shape="ainfix =amodadivainfix +V0apow2V1apow2V2c2amodadivV0apow2V2c2Iainfix &lt;V2V1Aainfix &lt;=c0V2F">
     <proof
-     prover="0"
-     timelimit="5"
-     memlimit="1000"
-     obsolete="false"
-     archived="false">
-     <result status="timeout" time="5.13"/>
-    </proof>
-    <proof
-     prover="1"
-     timelimit="5"
-     memlimit="1000"
-     obsolete="false"
-     archived="false">
-     <result status="timeout" time="4.99"/>
-    </proof>
-    <proof
-     prover="2"
-     timelimit="5"
-     memlimit="1000"
-     obsolete="false"
-     archived="false">
-     <result status="unknown" time="0.42"/>
-    </proof>
-    <proof
-     prover="3"
-     timelimit="5"
-     memlimit="1000"
-     obsolete="false"
-     archived="false">
-     <result status="timeout" time="5.12"/>
-    </proof>
-    <proof
-     prover="4"
-     timelimit="5"
-     memlimit="1000"
-     obsolete="false"
-     archived="false">
-     <result status="timeout" time="5.13"/>
-    </proof>
-    <proof
-     prover="7"
-     timelimit="5"
-     memlimit="1000"
-     obsolete="false"
-     archived="false">
-     <result status="timeout" time="5.15"/>
-    </proof>
-    <proof
-     prover="8"
-     timelimit="5"
-     memlimit="1000"