forall (xy : ptrofs) (m : Z),
0 < m ->
(m | Ptrofs.modulus) ->
Ptrofs.unsigned x mod m = 0 ->
Ptrofs.unsigned y mod m = 0 ->
Ptrofs.signed (Ptrofs.mul x y) mod m = 0
forall (xy : ptrofs) (m : Z),
0 < m ->
(m | Ptrofs.modulus) ->
Ptrofs.unsigned x mod m = 0 ->
Ptrofs.unsigned y mod m = 0 ->
Ptrofs.signed (Ptrofs.mul x y) mod m = 0
x, y:ptrofs
m:Z
H:0 < m
H0:(m | Ptrofs.modulus)
H1:Ptrofs.unsigned x mod m = 0
H2:Ptrofs.unsigned y mod m = 0
Ptrofs.signed (Ptrofs.mul x y) mod m = 0
x, y:ptrofs
m:Z
H:0 < m
H0:(m | Ptrofs.modulus)
H1:Ptrofs.unsigned x mod m = 0
H2:Ptrofs.unsigned y mod m = 0
Ptrofs.signed
(Ptrofs.repr (Ptrofs.unsigned x * Ptrofs.unsigned y))
mod m = 0
x, y:ptrofs
m:Z
H:0 < m
H0:(m | Ptrofs.modulus)
H1:Ptrofs.unsigned x mod m = 0
H2:Ptrofs.unsigned y mod m = 0
(if
zlt
((Ptrofs.unsigned x * Ptrofs.unsigned y)
mod Ptrofs.modulus) Ptrofs.half_modulus
then
(Ptrofs.unsigned x * Ptrofs.unsigned y)
mod Ptrofs.modulus
else
(Ptrofs.unsigned x * Ptrofs.unsigned y)
mod Ptrofs.modulus - Ptrofs.modulus) mod m = 0
repeatmatch goal with
| [ _ : _ |- context[if?xthen _ else _] ] => destruct x
| [ _ : _ |- context[_ mod Ptrofs.modulus mod m] ] =>
rewrite <- Zmod_div_mod; trylia; tryassumptionend; try(crush; lia); ptrofs_mod_tac m.Qed.
forall (xy : ptrofs) (m : Z),
0 < m ->
(m | Ptrofs.modulus) ->
Ptrofs.unsigned x mod m = 0 ->
Ptrofs.unsigned y mod m = 0 ->
Ptrofs.unsigned (Ptrofs.add x y) mod m = 0
forall (xy : ptrofs) (m : Z),
0 < m ->
(m | Ptrofs.modulus) ->
Ptrofs.unsigned x mod m = 0 ->
Ptrofs.unsigned y mod m = 0 ->
Ptrofs.unsigned (Ptrofs.add x y) mod m = 0
x, y:ptrofs
m:Z
H:0 < m
H0:(m | Ptrofs.modulus)
H1:Ptrofs.unsigned x mod m = 0
H2:Ptrofs.unsigned y mod m = 0
Ptrofs.unsigned (Ptrofs.add x y) mod m = 0
x, y:ptrofs
m:Z
H:0 < m
H0:(m | Ptrofs.modulus)
H1:Ptrofs.unsigned x mod m = 0
H2:Ptrofs.unsigned y mod m = 0
Ptrofs.unsigned
(Ptrofs.repr (Ptrofs.unsigned x + Ptrofs.unsigned y))
mod m = 0
x, y:ptrofs
m:Z
H:0 < m
H0:(m | Ptrofs.modulus)
H1:Ptrofs.unsigned x mod m = 0
H2:Ptrofs.unsigned y mod m = 0
((Ptrofs.unsigned x + Ptrofs.unsigned y)
mod Ptrofs.modulus) mod m = 0
repeatmatch goal with
| [ _ : _ |- context[if?xthen _ else _] ] => destruct x
| [ _ : _ |- context[_ mod Ptrofs.modulus mod m] ] =>
rewrite <- Zmod_div_mod; trylia; tryassumptionend; try (crush; lia); ptrofs_mod_tac m.Qed.
forallxy : ptrofs,
0 < Ptrofs.unsigned x ->
Ptrofs.unsigned y mod Ptrofs.unsigned x = 0 ->
Ptrofs.mul x (Ptrofs.divu y x) = y
forallxy : ptrofs,
0 < Ptrofs.unsigned x ->
Ptrofs.unsigned y mod Ptrofs.unsigned x = 0 ->
Ptrofs.mul x (Ptrofs.divu y x) = y
x, y:ptrofs
H:0 < Ptrofs.unsigned x
H0:Ptrofs.unsigned y mod Ptrofs.unsigned x = 0
Ptrofs.mul x (Ptrofs.divu y x) = y
x, y:ptrofs
H:0 < Ptrofs.unsigned x
H0:Ptrofs.unsigned y mod Ptrofs.unsigned x = 0
x <> Ptrofs.zero
x, y:ptrofs
H:0 < Ptrofs.unsigned x
H0:Ptrofs.unsigned y mod Ptrofs.unsigned x = 0
H1:x <> Ptrofs.zero
Ptrofs.mul x (Ptrofs.divu y x) = y
x, y:ptrofs
H:0 < Ptrofs.unsigned x
H0:Ptrofs.unsigned y mod Ptrofs.unsigned x = 0
x <> Ptrofs.zero
x, y:ptrofs
H:0 < Ptrofs.unsigned x
H0:Ptrofs.unsigned y mod Ptrofs.unsigned x = 0
H1:x = Ptrofs.zero
False
x, y:ptrofs
H:0 < Ptrofs.unsigned Ptrofs.zero
H0:Ptrofs.unsigned y mod Ptrofs.unsigned x = 0
H1:x = Ptrofs.zero
False
x, y:ptrofs
H:0 < 0
H0:Ptrofs.unsigned y mod Ptrofs.unsigned x = 0
H1:x = Ptrofs.zero
False
lia.
x, y:ptrofs
H:0 < Ptrofs.unsigned x
H0:Ptrofs.unsigned y mod Ptrofs.unsigned x = 0
H1:x <> Ptrofs.zero
Ptrofs.mul x (Ptrofs.divu y x) = y
x, y:ptrofs
H:0 < Ptrofs.unsigned x
H0:Ptrofs.unsigned y mod Ptrofs.unsigned x = 0
H1:x <> Ptrofs.zero
H2:y =
Ptrofs.add (Ptrofs.mul (Ptrofs.divu y x) x)
(Ptrofs.modu y x)
Ptrofs.mul x (Ptrofs.divu y x) = y
x, y:ptrofs
H:0 < Ptrofs.unsigned x
H0:Ptrofs.unsigned y mod Ptrofs.unsigned x = 0
H1:x <> Ptrofs.zero
H2:y =
Ptrofs.add (Ptrofs.mul (Ptrofs.divu y x) x)
(Ptrofs.repr
(Ptrofs.unsigned y mod Ptrofs.unsigned x))
Ptrofs.mul x (Ptrofs.divu y x) = y
x, y:ptrofs
H:0 < Ptrofs.unsigned x
H0:Ptrofs.unsigned y mod Ptrofs.unsigned x = 0
H1:x <> Ptrofs.zero
H2:y =
Ptrofs.add (Ptrofs.mul (Ptrofs.divu y x) x)
(Ptrofs.repr 0)
Ptrofs.mul x (Ptrofs.divu y x) = y
x, y:ptrofs
H:0 < Ptrofs.unsigned x
H0:Ptrofs.unsigned y mod Ptrofs.unsigned x = 0
H1:x <> Ptrofs.zero
H2:y =
Ptrofs.add (Ptrofs.mul (Ptrofs.divu y x) x)
Ptrofs.zero
Ptrofs.mul x (Ptrofs.divu y x) = y
x, y:ptrofs
H:0 < Ptrofs.unsigned x
H0:Ptrofs.unsigned y mod Ptrofs.unsigned x = 0
H1:x <> Ptrofs.zero
H2:y = Ptrofs.mul (Ptrofs.divu y x) x
Ptrofs.mul x (Ptrofs.divu y x) = y
x, y:ptrofs
H:0 < Ptrofs.unsigned x
H0:Ptrofs.unsigned y mod Ptrofs.unsigned x = 0
H1:x <> Ptrofs.zero
H2:y = Ptrofs.mul (Ptrofs.divu y x) x
Ptrofs.mul (Ptrofs.divu y x) x = y
congruence.Qed.
forallxy : ptrofs,
0 < Ptrofs.unsigned y ->
Ptrofs.unsigned x <= Ptrofs.max_unsigned ->
Ptrofs.unsigned (Ptrofs.divu x y) =
Ptrofs.unsigned x / Ptrofs.unsigned y
forallxy : ptrofs,
0 < Ptrofs.unsigned y ->
Ptrofs.unsigned x <= Ptrofs.max_unsigned ->
Ptrofs.unsigned (Ptrofs.divu x y) =
Ptrofs.unsigned x / Ptrofs.unsigned y
x, y:ptrofs
H:0 < Ptrofs.unsigned y
H0:Ptrofs.unsigned x <= Ptrofs.max_unsigned
Ptrofs.unsigned (Ptrofs.divu x y) =
Ptrofs.unsigned x / Ptrofs.unsigned y
x, y:ptrofs
H:0 < Ptrofs.unsigned y
H0:Ptrofs.unsigned x <= Ptrofs.max_unsigned
Ptrofs.unsigned
(Ptrofs.repr (Ptrofs.unsigned x / Ptrofs.unsigned y)) =
Ptrofs.unsigned x / Ptrofs.unsigned y
x, y:ptrofs
H:0 < Ptrofs.unsigned y
H0:Ptrofs.unsigned x <= Ptrofs.max_unsigned
0 <= Ptrofs.unsigned x / Ptrofs.unsigned y <=
Ptrofs.max_unsigned
x, y:ptrofs
H:0 < Ptrofs.unsigned y
H0:Ptrofs.unsigned x <= Ptrofs.max_unsigned
0 <= Ptrofs.unsigned x / Ptrofs.unsigned y
x, y:ptrofs
H:0 < Ptrofs.unsigned y
H0:Ptrofs.unsigned x <= Ptrofs.max_unsigned
Ptrofs.unsigned x / Ptrofs.unsigned y <=
Ptrofs.max_unsigned
x, y:ptrofs
H:0 < Ptrofs.unsigned y
H0:Ptrofs.unsigned x <= Ptrofs.max_unsigned
0 <= Ptrofs.unsigned x
x, y:ptrofs
H:0 < Ptrofs.unsigned y
H0:Ptrofs.unsigned x <= Ptrofs.max_unsigned
Ptrofs.unsigned x / Ptrofs.unsigned y <=
Ptrofs.max_unsigned
x, y:ptrofs
H:0 < Ptrofs.unsigned y
H0:Ptrofs.unsigned x <= Ptrofs.max_unsigned
Ptrofs.unsigned x / Ptrofs.unsigned y <=
Ptrofs.max_unsigned
x, y:ptrofs
H:0 < Ptrofs.unsigned y
H0:Ptrofs.unsigned x <= Ptrofs.max_unsigned
Ptrofs.unsigned x <=
Ptrofs.unsigned y * Ptrofs.max_unsigned
eapply Z.le_trans.
x, y:ptrofs
H:0 < Ptrofs.unsigned y
H0:Ptrofs.unsigned x <= Ptrofs.max_unsigned
Ptrofs.max_unsigned <=
Ptrofs.unsigned y * Ptrofs.max_unsigned
x, y:ptrofs
H:0 < Ptrofs.unsigned y
H0:Ptrofs.unsigned x <= Ptrofs.max_unsigned
Ptrofs.max_unsigned <=
Ptrofs.max_unsigned * Ptrofs.unsigned y
apply Z.le_mul_diag_r; crush.Qed.
forallxy : ptrofs,
Ptrofs.mul x y =
Ptrofs.repr (Ptrofs.unsigned x * Ptrofs.unsigned y)
forallxy : ptrofs,
Ptrofs.mul x y =
Ptrofs.repr (Ptrofs.unsigned x * Ptrofs.unsigned y)
x, y:ptrofs
Ptrofs.repr (Ptrofs.unsigned x * Ptrofs.unsigned y) =
Ptrofs.repr (Ptrofs.unsigned x * Ptrofs.unsigned y)
x, y:ptrofs
Ptrofs.eqm (Ptrofs.unsigned x * Ptrofs.unsigned y)
(Ptrofs.unsigned x * Ptrofs.unsigned y)
apply Ptrofs.eqm_mult; exists0; lia.Qed.
forallx : ptrofs,
0 <= Ptrofs.signed x ->
Ptrofs.signed x = Ptrofs.unsigned x
forallx : ptrofs,
0 <= Ptrofs.signed x ->
Ptrofs.signed x = Ptrofs.unsigned x
x:ptrofs
H:0 <= Ptrofs.signed x
Ptrofs.signed x = Ptrofs.unsigned x
x:ptrofs
H:0 <= Ptrofs.signed x
Ptrofs.signed x =
(if Ptrofs.lt x Ptrofs.zero
then Ptrofs.signed x + Ptrofs.modulus
else Ptrofs.signed x)
x:ptrofs
H:0 <= Ptrofs.signed x
EQ:Ptrofs.lt x Ptrofs.zero = true
Ptrofs.signed x = Ptrofs.signed x + Ptrofs.modulus
forall (n : Integers.int) (i : Z),
0 <= i < Byte.zwordsize ->
Byte.testbit (byte1 n) i = testbit n i
forall (n : Integers.int) (i : Z),
0 <= i < Byte.zwordsize ->
Byte.testbit (byte1 n) i = testbit n i
n:Integers.int
i:Z
H:0 <= i < Byte.zwordsize
Byte.testbit (byte1 n) i = testbit n i
n:Integers.int
i:Z
H:0 <= i < Byte.zwordsize
Byte.testbit (Byte.repr (unsigned n)) i = testbit n i
rewrite Byte.testbit_repr; auto.Qed.
forall (n : Integers.int) (i : Z),
0 <= i < Byte.zwordsize ->
Byte.testbit (byte2 n) i =
testbit n (i + Byte.zwordsize)
forall (n : Integers.int) (i : Z),
0 <= i < Byte.zwordsize ->
Byte.testbit (byte2 n) i =
testbit n (i + Byte.zwordsize)
n:Integers.int
i:Z
H:0 <= i < Byte.zwordsize
Byte.testbit (byte2 n) i =
testbit n (i + Byte.zwordsize)
n:Integers.int
i:Z
H:0 <= i < Byte.zwordsize
Byte.testbit
(Byte.repr (unsigned (shru n (repr Byte.zwordsize))))
i = testbit n (i + Byte.zwordsize)
n:Integers.int
i:Z
H:0 <= i < Byte.zwordsize
Z.testbit (unsigned (shru n (repr Byte.zwordsize))) i =
testbit n (i + Byte.zwordsize)
n:Integers.int
i:Z
H:0 <= i < Byte.zwordsize
H0:zwordsize = 4 * Byte.zwordsize
Z.testbit (unsigned (shru n (repr Byte.zwordsize))) i =
testbit n (i + Byte.zwordsize)
n:Integers.int
i:Z
H:0 <= i < Byte.zwordsize
H0:zwordsize = 4 * Byte.zwordsize
testbit (shru n (repr Byte.zwordsize)) i =
testbit n (i + Byte.zwordsize)
n:Integers.int
i:Z
H:0 <= i < Byte.zwordsize
H0:zwordsize = 4 * Byte.zwordsize
(if zlt (i + unsigned (repr Byte.zwordsize)) zwordsize
then testbit n (i + unsigned (repr Byte.zwordsize))
else false) = testbit n (i + Byte.zwordsize)
n:Integers.int
i:Z
H:0 <= i < Byte.zwordsize
H0:zwordsize = 4 * Byte.zwordsize
0 <= i < zwordsize
n:Integers.int
i:Z
H:0 <= i < Byte.zwordsize
H0:zwordsize = 4 * Byte.zwordsize
(if zlt (i + Byte.zwordsize) zwordsize
then testbit n (i + Byte.zwordsize)
else false) = testbit n (i + Byte.zwordsize)
n:Integers.int
i:Z
H:0 <= i < Byte.zwordsize
H0:zwordsize = 4 * Byte.zwordsize
0 <= i < zwordsize
n:Integers.int
i:Z
H:0 <= i < Byte.zwordsize
H0:zwordsize = 4 * Byte.zwordsize
i + Byte.zwordsize < zwordsize
n:Integers.int
i:Z
H:0 <= i < Byte.zwordsize
H0:zwordsize = 4 * Byte.zwordsize
0 <= i < zwordsize
omegais deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
n:Integers.int
i:Z
H:0 <= i < Byte.zwordsize
H0:zwordsize = 4 * Byte.zwordsize
0 <= i < zwordsize
omegais deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
Qed.
forall (n : Integers.int) (i : Z),
0 <= i < Byte.zwordsize ->
Byte.testbit (byte3 n) i =
testbit n (i + 2 * Byte.zwordsize)
forall (n : Integers.int) (i : Z),
0 <= i < Byte.zwordsize ->
Byte.testbit (byte3 n) i =
testbit n (i + 2 * Byte.zwordsize)
n:Integers.int
i:Z
H:0 <= i < Byte.zwordsize
Byte.testbit (byte3 n) i =
testbit n (i + 2 * Byte.zwordsize)
n:Integers.int
i:Z
H:0 <= i < Byte.zwordsize
Byte.testbit
(Byte.repr
(unsigned (shru n (repr (2 * Byte.zwordsize)))))
i = testbit n (i + 2 * Byte.zwordsize)
n:Integers.int
i:Z
H:0 <= i < Byte.zwordsize
Z.testbit
(unsigned (shru n (repr (2 * Byte.zwordsize)))) i =
testbit n (i + 2 * Byte.zwordsize)
n:Integers.int
i:Z
H:0 <= i < Byte.zwordsize
H0:zwordsize = 4 * Byte.zwordsize
Z.testbit
(unsigned (shru n (repr (2 * Byte.zwordsize)))) i =
testbit n (i + 2 * Byte.zwordsize)
n:Integers.int
i:Z
H:0 <= i < Byte.zwordsize
H0:zwordsize = 4 * Byte.zwordsize
testbit (shru n (repr (2 * Byte.zwordsize))) i =
testbit n (i + 2 * Byte.zwordsize)
n:Integers.int
i:Z
H:0 <= i < Byte.zwordsize
H0:zwordsize = 4 * Byte.zwordsize
(if
zlt (i + unsigned (repr (2 * Byte.zwordsize)))
zwordsize
then
testbit n (i + unsigned (repr (2 * Byte.zwordsize)))
else false) = testbit n (i + 2 * Byte.zwordsize)
n:Integers.int
i:Z
H:0 <= i < Byte.zwordsize
H0:zwordsize = 4 * Byte.zwordsize
0 <= i < zwordsize
n:Integers.int
i:Z
H:0 <= i < Byte.zwordsize
H0:zwordsize = 4 * Byte.zwordsize
(if zlt (i + 2 * Byte.zwordsize) zwordsize
then testbit n (i + 2 * Byte.zwordsize)
else false) = testbit n (i + 2 * Byte.zwordsize)
n:Integers.int
i:Z
H:0 <= i < Byte.zwordsize
H0:zwordsize = 4 * Byte.zwordsize
0 <= i < zwordsize
n:Integers.int
i:Z
H:0 <= i < Byte.zwordsize
H0:zwordsize = 4 * Byte.zwordsize
i + 2 * Byte.zwordsize < zwordsize
n:Integers.int
i:Z
H:0 <= i < Byte.zwordsize
H0:zwordsize = 4 * Byte.zwordsize
0 <= i < zwordsize
omegais deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
n:Integers.int
i:Z
H:0 <= i < Byte.zwordsize
H0:zwordsize = 4 * Byte.zwordsize
0 <= i < zwordsize
omegais deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
Qed.
forall (n : Integers.int) (i : Z),
0 <= i < Byte.zwordsize ->
Byte.testbit (byte4 n) i =
testbit n (i + 3 * Byte.zwordsize)
forall (n : Integers.int) (i : Z),
0 <= i < Byte.zwordsize ->
Byte.testbit (byte4 n) i =
testbit n (i + 3 * Byte.zwordsize)
n:Integers.int
i:Z
H:0 <= i < Byte.zwordsize
Byte.testbit (byte4 n) i =
testbit n (i + 3 * Byte.zwordsize)
n:Integers.int
i:Z
H:0 <= i < Byte.zwordsize
Byte.testbit
(Byte.repr
(unsigned (shru n (repr (3 * Byte.zwordsize)))))
i = testbit n (i + 3 * Byte.zwordsize)
n:Integers.int
i:Z
H:0 <= i < Byte.zwordsize
Z.testbit
(unsigned (shru n (repr (3 * Byte.zwordsize)))) i =
testbit n (i + 3 * Byte.zwordsize)
n:Integers.int
i:Z
H:0 <= i < Byte.zwordsize
H0:zwordsize = 4 * Byte.zwordsize
Z.testbit
(unsigned (shru n (repr (3 * Byte.zwordsize)))) i =
testbit n (i + 3 * Byte.zwordsize)
n:Integers.int
i:Z
H:0 <= i < Byte.zwordsize
H0:zwordsize = 4 * Byte.zwordsize
testbit (shru n (repr (3 * Byte.zwordsize))) i =
testbit n (i + 3 * Byte.zwordsize)
n:Integers.int
i:Z
H:0 <= i < Byte.zwordsize
H0:zwordsize = 4 * Byte.zwordsize
(if
zlt (i + unsigned (repr (3 * Byte.zwordsize)))
zwordsize
then
testbit n (i + unsigned (repr (3 * Byte.zwordsize)))
else false) = testbit n (i + 3 * Byte.zwordsize)
n:Integers.int
i:Z
H:0 <= i < Byte.zwordsize
H0:zwordsize = 4 * Byte.zwordsize
0 <= i < zwordsize
n:Integers.int
i:Z
H:0 <= i < Byte.zwordsize
H0:zwordsize = 4 * Byte.zwordsize
(if zlt (i + 3 * Byte.zwordsize) zwordsize
then testbit n (i + 3 * Byte.zwordsize)
else false) = testbit n (i + 3 * Byte.zwordsize)
n:Integers.int
i:Z
H:0 <= i < Byte.zwordsize
H0:zwordsize = 4 * Byte.zwordsize
0 <= i < zwordsize
n:Integers.int
i:Z
H:0 <= i < Byte.zwordsize
H0:zwordsize = 4 * Byte.zwordsize
i + 3 * Byte.zwordsize < zwordsize
n:Integers.int
i:Z
H:0 <= i < Byte.zwordsize
H0:zwordsize = 4 * Byte.zwordsize
0 <= i < zwordsize
omegais deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
n:Integers.int
i:Z
H:0 <= i < Byte.zwordsize
H0:zwordsize = 4 * Byte.zwordsize
0 <= i < zwordsize
omegais deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
Qed.
forall (b4b3b2b1 : byte) (i : Z),
0 <= i < zwordsize ->
testbit (ofbytes b4 b3 b2 b1) i =
(if zlt i Byte.zwordsize
then Byte.testbit b1 i
elseif zlt i (2 * Byte.zwordsize)
then Byte.testbit b2 (i - Byte.zwordsize)
elseif zlt i (3 * Byte.zwordsize)
then Byte.testbit b2 (i - 2 * Byte.zwordsize)
else Byte.testbit b2 (i - 3 * Byte.zwordsize))
forall (b4b3b2b1 : byte) (i : Z),
0 <= i < zwordsize ->
testbit (ofbytes b4 b3 b2 b1) i =
(if zlt i Byte.zwordsize
then Byte.testbit b1 i
elseif zlt i (2 * Byte.zwordsize)
then Byte.testbit b2 (i - Byte.zwordsize)
elseif zlt i (3 * Byte.zwordsize)
then Byte.testbit b2 (i - 2 * Byte.zwordsize)
else Byte.testbit b2 (i - 3 * Byte.zwordsize))
b4, b3, b2, b1:byte
i:Z
H:0 <= i < zwordsize
testbit (ofbytes b4 b3 b2 b1) i =
(if zlt i Byte.zwordsize
then Byte.testbit b1 i
elseif zlt i (2 * Byte.zwordsize)
then Byte.testbit b2 (i - Byte.zwordsize)
elseif zlt i (3 * Byte.zwordsize)
then Byte.testbit b2 (i - 2 * Byte.zwordsize)
else Byte.testbit b2 (i - 3 * Byte.zwordsize))
b4, b3, b2, b1:byte
i:Z
H:0 <= i < zwordsize
testbit
(or
(shl (repr (Byte.unsigned b4))
(repr (3 * Byte.zwordsize)))
(or
(shl (repr (Byte.unsigned b3))
(repr (2 * Byte.zwordsize)))
(or
(shl (repr (Byte.unsigned b2))
(repr Byte.zwordsize))
(repr (Byte.unsigned b1))))) i =
(if zlt i Byte.zwordsize
then Byte.testbit b1 i
elseif zlt i (2 * Byte.zwordsize)
then Byte.testbit b2 (i - Byte.zwordsize)
elseif zlt i (3 * Byte.zwordsize)
then Byte.testbit b2 (i - 2 * Byte.zwordsize)
else Byte.testbit b2 (i - 3 * Byte.zwordsize))
b4, b3, b2, b1:byte
i:Z
H:0 <= i < zwordsize
testbit
(shl (repr (Byte.unsigned b4))
(repr (3 * Byte.zwordsize))) i
|| (testbit
(shl (repr (Byte.unsigned b3))
(repr (2 * Byte.zwordsize))) i
|| (testbit
(shl (repr (Byte.unsigned b2))
(repr Byte.zwordsize)) i
|| testbit (repr (Byte.unsigned b1)) i)) =
(if zlt i Byte.zwordsize
then Byte.testbit b1 i
elseif zlt i (2 * Byte.zwordsize)
then Byte.testbit b2 (i - Byte.zwordsize)
elseif zlt i (3 * Byte.zwordsize)
then Byte.testbit b2 (i - 2 * Byte.zwordsize)
else Byte.testbit b2 (i - 3 * Byte.zwordsize))
b4, b3, b2, b1:byte
i:Z
H:0 <= i < zwordsize
(if zlt i (unsigned (repr (3 * Byte.zwordsize)))
then false
else
testbit (repr (Byte.unsigned b4))
(i - unsigned (repr (3 * Byte.zwordsize))))
|| ((if zlt i (unsigned (repr (2 * Byte.zwordsize)))
then false
else
testbit (repr (Byte.unsigned b3))
(i - unsigned (repr (2 * Byte.zwordsize))))
|| ((if zlt i (unsigned (repr Byte.zwordsize))
then false
else
testbit (repr (Byte.unsigned b2))
(i - unsigned (repr Byte.zwordsize)))
|| testbit (repr (Byte.unsigned b1)) i)) =
(if zlt i Byte.zwordsize
then Byte.testbit b1 i
elseif zlt i (2 * Byte.zwordsize)
then Byte.testbit b2 (i - Byte.zwordsize)
elseif zlt i (3 * Byte.zwordsize)
then Byte.testbit b2 (i - 2 * Byte.zwordsize)
else Byte.testbit b2 (i - 3 * Byte.zwordsize))
b4, b3, b2, b1:byte
i:Z
H:0 <= i < zwordsize
(if zlt i (unsigned (repr (3 * Byte.zwordsize)))
then false
else
testbit (repr (Byte.unsigned b4))
(i - unsigned (repr (3 * Byte.zwordsize))))
|| ((if zlt i (unsigned (repr (2 * Byte.zwordsize)))
then false
else
testbit (repr (Byte.unsigned b3))
(i - unsigned (repr (2 * Byte.zwordsize))))
|| ((if zlt i Byte.zwordsize
then false
else
testbit (repr (Byte.unsigned b2))
(i - Byte.zwordsize))
|| testbit (repr (Byte.unsigned b1)) i)) =
(if zlt i Byte.zwordsize
then Byte.testbit b1 i
elseif zlt i (2 * Byte.zwordsize)
then Byte.testbit b2 (i - Byte.zwordsize)
elseif zlt i (3 * Byte.zwordsize)
then Byte.testbit b2 (i - 2 * Byte.zwordsize)
else Byte.testbit b2 (i - 3 * Byte.zwordsize))
b4, b3, b2, b1:byte
i:Z
H:0 <= i < zwordsize
(if zlt i (unsigned (repr (3 * Byte.zwordsize)))
then false
else
testbit (repr (Byte.unsigned b4))
(i - unsigned (repr (3 * Byte.zwordsize))))
|| ((if zlt i (2 * Byte.zwordsize)
then false
else
testbit (repr (Byte.unsigned b3))
(i - 2 * Byte.zwordsize))
|| ((if zlt i Byte.zwordsize
then false
else
testbit (repr (Byte.unsigned b2))
(i - Byte.zwordsize))
|| testbit (repr (Byte.unsigned b1)) i)) =
(if zlt i Byte.zwordsize
then Byte.testbit b1 i
elseif zlt i (2 * Byte.zwordsize)
then Byte.testbit b2 (i - Byte.zwordsize)
elseif zlt i (3 * Byte.zwordsize)
then Byte.testbit b2 (i - 2 * Byte.zwordsize)
else Byte.testbit b2 (i - 3 * Byte.zwordsize))
b4, b3, b2, b1:byte
i:Z
H:0 <= i < zwordsize
(if zlt i (3 * Byte.zwordsize)
then false
else
testbit (repr (Byte.unsigned b4))
(i - 3 * Byte.zwordsize))
|| ((if zlt i (2 * Byte.zwordsize)
then false
else
testbit (repr (Byte.unsigned b3))
(i - 2 * Byte.zwordsize))
|| ((if zlt i Byte.zwordsize
then false
else
testbit (repr (Byte.unsigned b2))
(i - Byte.zwordsize))
|| testbit (repr (Byte.unsigned b1)) i)) =
(if zlt i Byte.zwordsize
then Byte.testbit b1 i
elseif zlt i (2 * Byte.zwordsize)
then Byte.testbit b2 (i - Byte.zwordsize)
elseif zlt i (3 * Byte.zwordsize)
then Byte.testbit b2 (i - 2 * Byte.zwordsize)
else Byte.testbit b2 (i - 3 * Byte.zwordsize))
b4, b3, b2, b1:byte
i:Z
H:0 <= i < zwordsize
H0:zwordsize = 4 * Byte.zwordsize
(if zlt i (3 * Byte.zwordsize)
then false
else
testbit (repr (Byte.unsigned b4))
(i - 3 * Byte.zwordsize))
|| ((if zlt i (2 * Byte.zwordsize)
then false
else
testbit (repr (Byte.unsigned b3))
(i - 2 * Byte.zwordsize))
|| ((if zlt i Byte.zwordsize
then false
else
testbit (repr (Byte.unsigned b2))
(i - Byte.zwordsize))
|| testbit (repr (Byte.unsigned b1)) i)) =
(if zlt i Byte.zwordsize
then Byte.testbit b1 i
elseif zlt i (2 * Byte.zwordsize)
then Byte.testbit b2 (i - Byte.zwordsize)
elseif zlt i (3 * Byte.zwordsize)
then Byte.testbit b2 (i - 2 * Byte.zwordsize)
else Byte.testbit b2 (i - 3 * Byte.zwordsize))
b4, b3, b2, b1:byte
i:Z
H:0 <= i < zwordsize
H0:zwordsize = 4 * Byte.zwordsize
l:i < Byte.zwordsize
(if zlt i (3 * Byte.zwordsize)
then false
else
testbit (repr (Byte.unsigned b4))
(i - 3 * Byte.zwordsize))
|| ((if zlt i (2 * Byte.zwordsize)
then false
else
testbit (repr (Byte.unsigned b3))
(i - 2 * Byte.zwordsize))
|| (false || testbit (repr (Byte.unsigned b1)) i)) =
Byte.testbit b1 i
b4, b3, b2, b1:byte
i:Z
H:0 <= i < zwordsize
H0:zwordsize = 4 * Byte.zwordsize
g:i >= Byte.zwordsize
(if zlt i (3 * Byte.zwordsize)
then false
else
testbit (repr (Byte.unsigned b4))
(i - 3 * Byte.zwordsize))
|| ((if zlt i (2 * Byte.zwordsize)
then false
else
testbit (repr (Byte.unsigned b3))
(i - 2 * Byte.zwordsize))
|| (testbit (repr (Byte.unsigned b2))
(i - Byte.zwordsize)
|| testbit (repr (Byte.unsigned b1)) i)) =
(if zlt i (2 * Byte.zwordsize)
then Byte.testbit b2 (i - Byte.zwordsize)
elseif zlt i (3 * Byte.zwordsize)
then Byte.testbit b2 (i - 2 * Byte.zwordsize)
else Byte.testbit b2 (i - 3 * Byte.zwordsize))
b4, b3, b2, b1:byte
i:Z
H:0 <= i < zwordsize
H0:zwordsize = 4 * Byte.zwordsize
l:i < Byte.zwordsize
(if zlt i (3 * Byte.zwordsize)
then false
else
Z.testbit (Byte.unsigned b4)
(i - 3 * Byte.zwordsize))
|| ((if zlt i (2 * Byte.zwordsize)
then false
else
testbit (repr (Byte.unsigned b3))
(i - 2 * Byte.zwordsize))
|| (false || testbit (repr (Byte.unsigned b1)) i)) =
Byte.testbit b1 i
b4, b3, b2, b1:byte
i:Z
H:0 <= i < zwordsize
H0:zwordsize = 4 * Byte.zwordsize
l:i < Byte.zwordsize
0 <= i - 3 * Byte.zwordsize < zwordsize
b4, b3, b2, b1:byte
i:Z
H:0 <= i < zwordsize
H0:zwordsize = 4 * Byte.zwordsize
g:i >= Byte.zwordsize
(if zlt i (3 * Byte.zwordsize)
then false
else
testbit (repr (Byte.unsigned b4))
(i - 3 * Byte.zwordsize))
|| ((if zlt i (2 * Byte.zwordsize)
then false
else
testbit (repr (Byte.unsigned b3))
(i - 2 * Byte.zwordsize))
|| (testbit (repr (Byte.unsigned b2))
(i - Byte.zwordsize)
|| testbit (repr (Byte.unsigned b1)) i)) =
(if zlt i (2 * Byte.zwordsize)
then Byte.testbit b2 (i - Byte.zwordsize)
elseif zlt i (3 * Byte.zwordsize)
then Byte.testbit b2 (i - 2 * Byte.zwordsize)
else Byte.testbit b2 (i - 3 * Byte.zwordsize))
Abort.
forallxy : Integers.int,
signed x >= 0 -> signed y >= 0 -> divs x y = divu x y
forallxy : Integers.int,
signed x >= 0 -> signed y >= 0 -> divs x y = divu x y
forallxy : Integers.int,
signed x >= 0 ->
signed y >= 0 ->
repr (signed x ÷ signed y) =
repr (unsigned x / unsigned y)
x, y:Integers.int
H:signed x >= 0
H0:signed y >= 0
repr (signed x ÷ signed y) =
repr (unsigned x / unsigned y)
forallx : Integers.int,
unsigned x <> 2147483648 ->
signed (neg x) = - signed x
forallx : Integers.int,
unsigned x <> 2147483648 ->
signed (neg x) = - signed x
x:Integers.int
Hhalf:unsigned x <> 2147483648
signed (neg x) = - signed x
x:Integers.int
Hhalf:unsigned x <> 2147483648
signed (neg x) = - signed x
x:Integers.int
Hhalf:unsigned x <> 2147483648
(if zlt (unsigned (neg x)) half_modulus
then unsigned (neg x)
else unsigned (neg x) - modulus) =
-
(if zlt (unsigned x) half_modulus
then unsigned x
else unsigned x - modulus)
x:Integers.int
Hhalf:unsigned x <> 2147483648
(if zlt (Z_mod_modulus (- unsigned x)) half_modulus
then Z_mod_modulus (- unsigned x)
else Z_mod_modulus (- unsigned x) - modulus) =
-
(if zlt (unsigned x) half_modulus
then unsigned x
else unsigned x - modulus)
x:Integers.int
Hhalf:unsigned x <> 2147483648
(if zlt (- unsigned x mod modulus) half_modulus
then - unsigned x mod modulus
else - unsigned x mod modulus - modulus) =
-
(if zlt (unsigned x) half_modulus
then unsigned x
else unsigned x - modulus)
x:Integers.int
Hhalf:unsigned x <> 2147483648
(if zlt (- unsigned x mod 4294967296) half_modulus
then - unsigned x mod 4294967296else - unsigned x mod 4294967296 - 4294967296) =
-
(if zlt (unsigned x) half_modulus
then unsigned x
else unsigned x - 4294967296)
x:Integers.int
Hhalf:unsigned x <> 2147483648
(if zlt (- unsigned x mod 4294967296) 2147483648then - unsigned x mod 4294967296else - unsigned x mod 4294967296 - 4294967296) =
-
(if zlt (unsigned x) 2147483648then unsigned x
else unsigned x - 4294967296)
x:Integers.int
Hhalf:unsigned x <> 2147483648
l:- unsigned x mod 4294967296 < 2147483648
l0:unsigned x < 2147483648
- unsigned x mod 4294967296 = - unsigned x
x:Integers.int
Hhalf:unsigned x <> 2147483648
l:- unsigned x mod 4294967296 < 2147483648
g:unsigned x >= 2147483648
- unsigned x mod 4294967296 =
- (unsigned x - 4294967296)
x:Integers.int
Hhalf:unsigned x <> 2147483648
g:- unsigned x mod 4294967296 >= 2147483648
l:unsigned x < 2147483648
- unsigned x mod 4294967296 - 4294967296 =
- unsigned x
x:Integers.int
Hhalf:unsigned x <> 2147483648
g:- unsigned x mod 4294967296 >= 2147483648
g0:unsigned x >= 2147483648
- unsigned x mod 4294967296 - 4294967296 =
- (unsigned x - 4294967296)
x:Integers.int
Hhalf:unsigned x <> 2147483648
l:- unsigned x mod 4294967296 < 2147483648
l0:unsigned x < 2147483648
- unsigned x mod 4294967296 = - unsigned x
x:Integers.int
Hhalf:unsigned x <> 2147483648
l:- unsigned x mod 4294967296 < 2147483648
l0:unsigned x < 2147483648
e:unsigned x = 0
- unsigned x mod 4294967296 = - unsigned x
x:Integers.int
Hhalf:unsigned x <> 2147483648
l:- unsigned x mod 4294967296 < 2147483648
l0:unsigned x < 2147483648
n:unsigned x <> 0
- unsigned x mod 4294967296 = - unsigned x
x:Integers.int
Hhalf:unsigned x <> 2147483648
l:- unsigned x mod 4294967296 < 2147483648
l0:unsigned x < 2147483648
e:unsigned x = 0
- unsigned x mod 4294967296 = - unsigned x
x:Integers.int
Hhalf:unsigned x <> 2147483648
l:- unsigned x mod 4294967296 < 2147483648
l0:unsigned x < 2147483648
e:unsigned x = 0
- 0 mod 4294967296 = - 0
auto.
x:Integers.int
Hhalf:unsigned x <> 2147483648
l:- unsigned x mod 4294967296 < 2147483648
l0:unsigned x < 2147483648
n:unsigned x <> 0
- unsigned x mod 4294967296 = - unsigned x
x:Integers.int
Hhalf:unsigned x <> 2147483648
l:- unsigned x mod 4294967296 < 2147483648
l0:unsigned x < 2147483648
n:unsigned x <> 0
H:4294967296 <> 0 ->
unsigned x mod 4294967296 <> 0 ->
- unsigned x mod 4294967296 =
4294967296 - unsigned x mod 4294967296
- unsigned x mod 4294967296 = - unsigned x
x:Integers.int
Hhalf:unsigned x <> 2147483648
l:- unsigned x mod 4294967296 < 2147483648
l0:unsigned x < 2147483648
n:unsigned x <> 0
H:4294967296 <> 0 ->
unsigned x mod 4294967296 <> 0 ->
- unsigned x mod 4294967296 =
4294967296 - unsigned x mod 4294967296
H0:4294967296 <> 0
- unsigned x mod 4294967296 = - unsigned x
x:Integers.int
Hhalf:unsigned x <> 2147483648
l:- unsigned x mod 4294967296 < 2147483648
l0:unsigned x < 2147483648
n:unsigned x <> 0
H:4294967296 <> 0 ->
unsigned x mod 4294967296 <> 0 ->
- unsigned x mod 4294967296 =
4294967296 - unsigned x mod 4294967296
H0:- unsigned x mod 4294967296 =
4294967296 - unsigned x mod 4294967296
- unsigned x mod 4294967296 = - unsigned x
x:Integers.int
Hhalf:unsigned x <> 2147483648
l:- unsigned x mod 4294967296 < 2147483648
l0:unsigned x < 2147483648
n:unsigned x <> 0
H:4294967296 <> 0 ->
unsigned x mod 4294967296 <> 0 ->
- unsigned x mod 4294967296 =
4294967296 - unsigned x mod 4294967296
H0:4294967296 <> 0
unsigned x mod 4294967296 <> 0
x:Integers.int
Hhalf:unsigned x <> 2147483648
l:4294967296 - unsigned x mod 4294967296 <
2147483648
l0:unsigned x < 2147483648
n:unsigned x <> 0
H:4294967296 <> 0 ->
unsigned x mod 4294967296 <> 0 ->
- unsigned x mod 4294967296 =
4294967296 - unsigned x mod 4294967296
H0:- unsigned x mod 4294967296 =
4294967296 - unsigned x mod 4294967296
- unsigned x mod 4294967296 = - unsigned x
x:Integers.int
Hhalf:unsigned x <> 2147483648
l:- unsigned x mod 4294967296 < 2147483648
l0:unsigned x < 2147483648
n:unsigned x <> 0
H:4294967296 <> 0 ->
unsigned x mod 4294967296 <> 0 ->
- unsigned x mod 4294967296 =
4294967296 - unsigned x mod 4294967296
H0:4294967296 <> 0
unsigned x mod 4294967296 <> 0
x:Integers.int
Hhalf:unsigned x <> 2147483648
l:4294967296 - unsigned x mod 4294967296 <
2147483648
l0:unsigned x < 2147483648
n:unsigned x <> 0
H:4294967296 <> 0 ->
unsigned x mod 4294967296 <> 0 ->
- unsigned x mod 4294967296 =
4294967296 - unsigned x mod 4294967296
H0:- unsigned x mod 4294967296 =
4294967296 - unsigned x mod 4294967296
H1:0 <= unsigned x < 4294967296 ->
unsigned x mod 4294967296 = unsigned x
- unsigned x mod 4294967296 = - unsigned x
x:Integers.int
Hhalf:unsigned x <> 2147483648
l:- unsigned x mod 4294967296 < 2147483648
l0:unsigned x < 2147483648
n:unsigned x <> 0
H:4294967296 <> 0 ->
unsigned x mod 4294967296 <> 0 ->
- unsigned x mod 4294967296 =
4294967296 - unsigned x mod 4294967296
H0:4294967296 <> 0
unsigned x mod 4294967296 <> 0
x:Integers.int
Hhalf:unsigned x <> 2147483648
l:4294967296 - unsigned x mod 4294967296 <
2147483648
l0:unsigned x < 2147483648
n:unsigned x <> 0
H:4294967296 <> 0 ->
unsigned x mod 4294967296 <> 0 ->
- unsigned x mod 4294967296 =
4294967296 - unsigned x mod 4294967296
H0:- unsigned x mod 4294967296 =
4294967296 - unsigned x mod 4294967296
H1:0 <= unsigned x < 4294967296 ->
unsigned x mod 4294967296 = unsigned x
0 <= unsigned x < 4294967296
x:Integers.int
Hhalf:unsigned x <> 2147483648
l:4294967296 - unsigned x mod 4294967296 <
2147483648
l0:unsigned x < 2147483648
n:unsigned x <> 0
H:4294967296 <> 0 ->
unsigned x mod 4294967296 <> 0 ->
- unsigned x mod 4294967296 =
4294967296 - unsigned x mod 4294967296
H0:- unsigned x mod 4294967296 =
4294967296 - unsigned x mod 4294967296
H1:0 <= unsigned x < 4294967296 ->
unsigned x mod 4294967296 = unsigned x
H2:0 <= unsigned x < 4294967296
- unsigned x mod 4294967296 = - unsigned x
x:Integers.int
Hhalf:unsigned x <> 2147483648
l:- unsigned x mod 4294967296 < 2147483648
l0:unsigned x < 2147483648
n:unsigned x <> 0
H:4294967296 <> 0 ->
unsigned x mod 4294967296 <> 0 ->
- unsigned x mod 4294967296 =
4294967296 - unsigned x mod 4294967296
H0:4294967296 <> 0
unsigned x mod 4294967296 <> 0
x:Integers.int
Hhalf:unsigned x <> 2147483648
l:4294967296 - unsigned x mod 4294967296 <
2147483648
l0:unsigned x < 2147483648
n:unsigned x <> 0
H:4294967296 <> 0 ->
unsigned x mod 4294967296 <> 0 ->
- unsigned x mod 4294967296 =
4294967296 - unsigned x mod 4294967296
H0:- unsigned x mod 4294967296 =
4294967296 - unsigned x mod 4294967296
H1:0 <= unsigned x < 4294967296 ->
unsigned x mod 4294967296 = unsigned x
H2:0 <= unsigned x <= max_unsigned
0 <= unsigned x < 4294967296
x:Integers.int
Hhalf:unsigned x <> 2147483648
l:4294967296 - unsigned x mod 4294967296 <
2147483648
l0:unsigned x < 2147483648
n:unsigned x <> 0
H:4294967296 <> 0 ->
unsigned x mod 4294967296 <> 0 ->
- unsigned x mod 4294967296 =
4294967296 - unsigned x mod 4294967296
H0:- unsigned x mod 4294967296 =
4294967296 - unsigned x mod 4294967296
H1:0 <= unsigned x < 4294967296 ->
unsigned x mod 4294967296 = unsigned x
H2:0 <= unsigned x < 4294967296
- unsigned x mod 4294967296 = - unsigned x
x:Integers.int
Hhalf:unsigned x <> 2147483648
l:- unsigned x mod 4294967296 < 2147483648
l0:unsigned x < 2147483648
n:unsigned x <> 0
H:4294967296 <> 0 ->
unsigned x mod 4294967296 <> 0 ->
- unsigned x mod 4294967296 =
4294967296 - unsigned x mod 4294967296
H0:4294967296 <> 0
unsigned x mod 4294967296 <> 0
x:Integers.int
Hhalf:unsigned x <> 2147483648
l:4294967296 - unsigned x mod 4294967296 <
2147483648
l0:unsigned x < 2147483648
n:unsigned x <> 0
H:4294967296 <> 0 ->
unsigned x mod 4294967296 <> 0 ->
- unsigned x mod 4294967296 =
4294967296 - unsigned x mod 4294967296
H0:- unsigned x mod 4294967296 =
4294967296 - unsigned x mod 4294967296
H1:0 <= unsigned x < 4294967296 ->
unsigned x mod 4294967296 = unsigned x
H2:0 <= unsigned x < 4294967296
- unsigned x mod 4294967296 = - unsigned x
x:Integers.int
Hhalf:unsigned x <> 2147483648
l:- unsigned x mod 4294967296 < 2147483648
l0:unsigned x < 2147483648
n:unsigned x <> 0
H:4294967296 <> 0 ->
unsigned x mod 4294967296 <> 0 ->
- unsigned x mod 4294967296 =
4294967296 - unsigned x mod 4294967296
H0:4294967296 <> 0
unsigned x mod 4294967296 <> 0
x:Integers.int
Hhalf:unsigned x <> 2147483648
l:4294967296 - unsigned x mod 4294967296 <
2147483648
l0:unsigned x < 2147483648
n:unsigned x <> 0
H:4294967296 <> 0 ->
unsigned x mod 4294967296 <> 0 ->
- unsigned x mod 4294967296 =
4294967296 - unsigned x mod 4294967296
H0:- unsigned x mod 4294967296 =
4294967296 - unsigned x mod 4294967296
H1:0 <= unsigned x < 4294967296 ->
unsigned x mod 4294967296 = unsigned x
H2:unsigned x mod 4294967296 = unsigned x
- unsigned x mod 4294967296 = - unsigned x
x:Integers.int
Hhalf:unsigned x <> 2147483648
l:- unsigned x mod 4294967296 < 2147483648
l0:unsigned x < 2147483648
n:unsigned x <> 0
H:4294967296 <> 0 ->
unsigned x mod 4294967296 <> 0 ->
- unsigned x mod 4294967296 =
4294967296 - unsigned x mod 4294967296
H0:4294967296 <> 0
unsigned x mod 4294967296 <> 0
x:Integers.int
Hhalf:unsigned x <> 2147483648
l:4294967296 - unsigned x < 2147483648
l0:unsigned x < 2147483648
n:unsigned x <> 0
H:4294967296 <> 0 ->
unsigned x mod 4294967296 <> 0 ->
- unsigned x mod 4294967296 =
4294967296 - unsigned x mod 4294967296
H0:- unsigned x mod 4294967296 =
4294967296 - unsigned x mod 4294967296
H1:0 <= unsigned x < 4294967296 ->
unsigned x mod 4294967296 = unsigned x
H2:unsigned x mod 4294967296 = unsigned x
- unsigned x mod 4294967296 = - unsigned x
x:Integers.int
Hhalf:unsigned x <> 2147483648
l:- unsigned x mod 4294967296 < 2147483648
l0:unsigned x < 2147483648
n:unsigned x <> 0
H:4294967296 <> 0 ->
unsigned x mod 4294967296 <> 0 ->
- unsigned x mod 4294967296 =
4294967296 - unsigned x mod 4294967296
H0:4294967296 <> 0
unsigned x mod 4294967296 <> 0
x:Integers.int
Hhalf:unsigned x <> 2147483648
l:- unsigned x mod 4294967296 < 2147483648
l0:unsigned x < 2147483648
n:unsigned x <> 0
H:4294967296 <> 0 ->
unsigned x mod 4294967296 <> 0 ->
- unsigned x mod 4294967296 =
4294967296 - unsigned x mod 4294967296
H0:4294967296 <> 0
unsigned x mod 4294967296 <> 0
x:Integers.int
Hhalf:unsigned x <> 2147483648
l:- unsigned x mod 4294967296 < 2147483648
l0:unsigned x < 2147483648
n:unsigned x <> 0
H:4294967296 <> 0 ->
unsigned x mod 4294967296 <> 0 ->
- unsigned x mod 4294967296 =
4294967296 - unsigned x mod 4294967296
H0:4294967296 <> 0
unsigned x <> 0
x:Integers.int
Hhalf:unsigned x <> 2147483648
l:- unsigned x mod 4294967296 < 2147483648
l0:unsigned x < 2147483648
n:unsigned x <> 0
H:4294967296 <> 0 ->
unsigned x mod 4294967296 <> 0 ->
- unsigned x mod 4294967296 =
4294967296 - unsigned x mod 4294967296
H0:4294967296 <> 0
0 <= unsigned x < 4294967296
x:Integers.int
Hhalf:unsigned x <> 2147483648
l:- unsigned x mod 4294967296 < 2147483648
l0:unsigned x < 2147483648
n:unsigned x <> 0
H:4294967296 <> 0 ->
unsigned x mod 4294967296 <> 0 ->
- unsigned x mod 4294967296 =
4294967296 - unsigned x mod 4294967296
H0:4294967296 <> 0
0 <= unsigned x < 4294967296
x:Integers.int
Hhalf:unsigned x <> 2147483648
l:- unsigned x mod 4294967296 < 2147483648
l0:unsigned x < 2147483648
n:unsigned x <> 0
H:4294967296 <> 0 ->
unsigned x mod 4294967296 <> 0 ->
- unsigned x mod 4294967296 =
4294967296 - unsigned x mod 4294967296
H0:4294967296 <> 0
H1:0 <= unsigned x <= max_unsigned
0 <= unsigned x < 4294967296
lia.
x:Integers.int
Hhalf:unsigned x <> 2147483648
l:- unsigned x mod 4294967296 < 2147483648
g:unsigned x >= 2147483648
- unsigned x mod 4294967296 =
- (unsigned x - 4294967296)
x:Integers.int
Hhalf:unsigned x <> 2147483648
l:- unsigned x mod 4294967296 < 2147483648
g:unsigned x >= 2147483648
e:unsigned x = 0
- unsigned x mod 4294967296 =
- (unsigned x - 4294967296)
x:Integers.int
Hhalf:unsigned x <> 2147483648
l:- unsigned x mod 4294967296 < 2147483648
g:unsigned x >= 2147483648
n:unsigned x <> 0
- unsigned x mod 4294967296 =
- (unsigned x - 4294967296)
x:Integers.int
Hhalf:unsigned x <> 2147483648
l:- unsigned x mod 4294967296 < 2147483648
g:unsigned x >= 2147483648
e:unsigned x = 0
- unsigned x mod 4294967296 =
- (unsigned x - 4294967296)
lia.
x:Integers.int
Hhalf:unsigned x <> 2147483648
l:- unsigned x mod 4294967296 < 2147483648
g:unsigned x >= 2147483648
n:unsigned x <> 0
- unsigned x mod 4294967296 =
- (unsigned x - 4294967296)
x:Integers.int
Hhalf:unsigned x <> 2147483648
l:- unsigned x mod 4294967296 < 2147483648
g:unsigned x >= 2147483648
n:unsigned x <> 0
4294967296 - unsigned x mod 4294967296 =
- (unsigned x - 4294967296)
x:Integers.int
Hhalf:unsigned x <> 2147483648
l:- unsigned x mod 4294967296 < 2147483648
g:unsigned x >= 2147483648
n:unsigned x <> 0
unsigned x mod 4294967296 <> 0
x:Integers.int
Hhalf:unsigned x <> 2147483648
l:- unsigned x mod 4294967296 < 2147483648
g:unsigned x >= 2147483648
n:unsigned x <> 0
4294967296 - unsigned x mod 4294967296 =
- unsigned x + 4294967296
x:Integers.int
Hhalf:unsigned x <> 2147483648
l:- unsigned x mod 4294967296 < 2147483648
g:unsigned x >= 2147483648
n:unsigned x <> 0
unsigned x mod 4294967296 <> 0
x:Integers.int
Hhalf:unsigned x <> 2147483648
l:- unsigned x mod 4294967296 < 2147483648
g:unsigned x >= 2147483648
n:unsigned x <> 0
4294967296 - unsigned x = - unsigned x + 4294967296
x:Integers.int
Hhalf:unsigned x <> 2147483648
l:- unsigned x mod 4294967296 < 2147483648
g:unsigned x >= 2147483648
n:unsigned x <> 0
0 <= unsigned x < 4294967296
x:Integers.int
Hhalf:unsigned x <> 2147483648
l:- unsigned x mod 4294967296 < 2147483648
g:unsigned x >= 2147483648
n:unsigned x <> 0
unsigned x mod 4294967296 <> 0
x:Integers.int
Hhalf:unsigned x <> 2147483648
l:- unsigned x mod 4294967296 < 2147483648
g:unsigned x >= 2147483648
n:unsigned x <> 0
0 <= unsigned x < 4294967296
x:Integers.int
Hhalf:unsigned x <> 2147483648
l:- unsigned x mod 4294967296 < 2147483648
g:unsigned x >= 2147483648
n:unsigned x <> 0
unsigned x mod 4294967296 <> 0
x:Integers.int
Hhalf:unsigned x <> 2147483648
l:- unsigned x mod 4294967296 < 2147483648
g:unsigned x >= 2147483648
n:unsigned x <> 0
H:0 <= unsigned x <= max_unsigned
0 <= unsigned x < 4294967296
x:Integers.int
Hhalf:unsigned x <> 2147483648
l:- unsigned x mod 4294967296 < 2147483648
g:unsigned x >= 2147483648
n:unsigned x <> 0
unsigned x mod 4294967296 <> 0
x:Integers.int
Hhalf:unsigned x <> 2147483648
l:- unsigned x mod 4294967296 < 2147483648
g:unsigned x >= 2147483648
n:unsigned x <> 0
unsigned x mod 4294967296 <> 0
x:Integers.int
Hhalf:unsigned x <> 2147483648
l:- unsigned x mod 4294967296 < 2147483648
g:unsigned x >= 2147483648
n:unsigned x <> 0
unsigned x <> 0
x:Integers.int
Hhalf:unsigned x <> 2147483648
l:- unsigned x mod 4294967296 < 2147483648
g:unsigned x >= 2147483648
n:unsigned x <> 0
0 <= unsigned x < 4294967296
x:Integers.int
Hhalf:unsigned x <> 2147483648
l:- unsigned x mod 4294967296 < 2147483648
g:unsigned x >= 2147483648
n:unsigned x <> 0
0 <= unsigned x < 4294967296
x:Integers.int
Hhalf:unsigned x <> 2147483648
l:- unsigned x mod 4294967296 < 2147483648
g:unsigned x >= 2147483648
n:unsigned x <> 0
H:0 <= unsigned x <= max_unsigned
0 <= unsigned x < 4294967296
simplify; lia.
x:Integers.int
Hhalf:unsigned x <> 2147483648
g:- unsigned x mod 4294967296 >= 2147483648
l:unsigned x < 2147483648
- unsigned x mod 4294967296 - 4294967296 =
- unsigned x
x:Integers.int
Hhalf:unsigned x <> 2147483648
g:- unsigned x mod 4294967296 >= 2147483648
l:unsigned x < 2147483648
e:unsigned x = 0
- unsigned x mod 4294967296 - 4294967296 =
- unsigned x
x:Integers.int
Hhalf:unsigned x <> 2147483648
g:- unsigned x mod 4294967296 >= 2147483648
l:unsigned x < 2147483648
n:unsigned x <> 0
- unsigned x mod 4294967296 - 4294967296 =
- unsigned x
x:Integers.int
Hhalf:unsigned x <> 2147483648
g:- unsigned x mod 4294967296 >= 2147483648
l:unsigned x < 2147483648
e:unsigned x = 0
- unsigned x mod 4294967296 - 4294967296 =
- unsigned x
x:Integers.int
Hhalf:0 <> 2147483648
g:- 0 mod 4294967296 >= 2147483648
l:0 < 2147483648
e:unsigned x = 0
- 0 mod 4294967296 - 4294967296 = - 0
x:Integers.int
Hhalf:0 <> 2147483648
g:0 mod 4294967296 >= 2147483648
l:0 < 2147483648
e:unsigned x = 0
0 mod 4294967296 - 4294967296 = 0
x:Integers.int
Hhalf:0 <> 2147483648
g:0 >= 2147483648
l:0 < 2147483648
e:unsigned x = 0
0 mod 4294967296 - 4294967296 = 0
lia.
x:Integers.int
Hhalf:unsigned x <> 2147483648
g:- unsigned x mod 4294967296 >= 2147483648
l:unsigned x < 2147483648
n:unsigned x <> 0
- unsigned x mod 4294967296 - 4294967296 =
- unsigned x
x:Integers.int
Hhalf:unsigned x <> 2147483648
g:- unsigned x mod 4294967296 >= 2147483648
l:unsigned x < 2147483648
n:unsigned x <> 0
4294967296 - unsigned x mod 4294967296 - 4294967296 =
- unsigned x
x:Integers.int
Hhalf:unsigned x <> 2147483648
g:- unsigned x mod 4294967296 >= 2147483648
l:unsigned x < 2147483648
n:unsigned x <> 0
unsigned x mod 4294967296 <> 0
x:Integers.int
Hhalf:unsigned x <> 2147483648
g:- unsigned x mod 4294967296 >= 2147483648
l:unsigned x < 2147483648
n:unsigned x <> 0
4294967296 - unsigned x - 4294967296 = - unsigned x
x:Integers.int
Hhalf:unsigned x <> 2147483648
g:- unsigned x mod 4294967296 >= 2147483648
l:unsigned x < 2147483648
n:unsigned x <> 0
0 <= unsigned x < 4294967296
x:Integers.int
Hhalf:unsigned x <> 2147483648
g:- unsigned x mod 4294967296 >= 2147483648
l:unsigned x < 2147483648
n:unsigned x <> 0
unsigned x mod 4294967296 <> 0
x:Integers.int
Hhalf:unsigned x <> 2147483648
g:- unsigned x mod 4294967296 >= 2147483648
l:unsigned x < 2147483648
n:unsigned x <> 0
0 <= unsigned x < 4294967296
x:Integers.int
Hhalf:unsigned x <> 2147483648
g:- unsigned x mod 4294967296 >= 2147483648
l:unsigned x < 2147483648
n:unsigned x <> 0
unsigned x mod 4294967296 <> 0
x:Integers.int
Hhalf:unsigned x <> 2147483648
g:- unsigned x mod 4294967296 >= 2147483648
l:unsigned x < 2147483648
n:unsigned x <> 0
H:0 <= unsigned x <= max_unsigned
0 <= unsigned x < 4294967296
x:Integers.int
Hhalf:unsigned x <> 2147483648
g:- unsigned x mod 4294967296 >= 2147483648
l:unsigned x < 2147483648
n:unsigned x <> 0
unsigned x mod 4294967296 <> 0
x:Integers.int
Hhalf:unsigned x <> 2147483648
g:- unsigned x mod 4294967296 >= 2147483648
l:unsigned x < 2147483648
n:unsigned x <> 0
unsigned x mod 4294967296 <> 0
x:Integers.int
Hhalf:unsigned x <> 2147483648
g:- unsigned x mod 4294967296 >= 2147483648
l:unsigned x < 2147483648
n:unsigned x <> 0
unsigned x <> 0
x:Integers.int
Hhalf:unsigned x <> 2147483648
g:- unsigned x mod 4294967296 >= 2147483648
l:unsigned x < 2147483648
n:unsigned x <> 0
0 <= unsigned x < 4294967296
x:Integers.int
Hhalf:unsigned x <> 2147483648
g:- unsigned x mod 4294967296 >= 2147483648
l:unsigned x < 2147483648
n:unsigned x <> 0
0 <= unsigned x < 4294967296
x:Integers.int
Hhalf:unsigned x <> 2147483648
g:- unsigned x mod 4294967296 >= 2147483648
l:unsigned x < 2147483648
n:unsigned x <> 0
H:0 <= unsigned x <= max_unsigned
0 <= unsigned x < 4294967296
lia.
x:Integers.int
Hhalf:unsigned x <> 2147483648
g:- unsigned x mod 4294967296 >= 2147483648
g0:unsigned x >= 2147483648
- unsigned x mod 4294967296 - 4294967296 =
- (unsigned x - 4294967296)
x:Integers.int
Hhalf:unsigned x <> 2147483648
g:- unsigned x mod 4294967296 >= 2147483648
g0:unsigned x >= 2147483648
e:unsigned x = 0
- unsigned x mod 4294967296 - 4294967296 =
- (unsigned x - 4294967296)
x:Integers.int
Hhalf:unsigned x <> 2147483648
g:- unsigned x mod 4294967296 >= 2147483648
g0:unsigned x >= 2147483648
n:unsigned x <> 0
- unsigned x mod 4294967296 - 4294967296 =
- (unsigned x - 4294967296)
x:Integers.int
Hhalf:unsigned x <> 2147483648
g:- unsigned x mod 4294967296 >= 2147483648
g0:unsigned x >= 2147483648
e:unsigned x = 0
- unsigned x mod 4294967296 - 4294967296 =
- (unsigned x - 4294967296)
lia.
x:Integers.int
Hhalf:unsigned x <> 2147483648
g:- unsigned x mod 4294967296 >= 2147483648
g0:unsigned x >= 2147483648
n:unsigned x <> 0
- unsigned x mod 4294967296 - 4294967296 =
- (unsigned x - 4294967296)
x:Integers.int
Hhalf:unsigned x <> 2147483648
g:4294967296 - unsigned x mod 4294967296 >=
2147483648
g0:unsigned x >= 2147483648
n:unsigned x <> 0
- unsigned x mod 4294967296 - 4294967296 =
- (unsigned x - 4294967296)
x:Integers.int
Hhalf:unsigned x <> 2147483648
g:- unsigned x mod 4294967296 >= 2147483648
g0:unsigned x >= 2147483648
n:unsigned x <> 0
unsigned x mod 4294967296 <> 0
x:Integers.int
Hhalf:unsigned x <> 2147483648
g:4294967296 - unsigned x >= 2147483648
g0:unsigned x >= 2147483648
n:unsigned x <> 0
- unsigned x mod 4294967296 - 4294967296 =
- (unsigned x - 4294967296)
x:Integers.int
Hhalf:unsigned x <> 2147483648
g:4294967296 - unsigned x mod 4294967296 >=
2147483648
g0:unsigned x >= 2147483648
n:unsigned x <> 0
0 <= unsigned x < 4294967296
x:Integers.int
Hhalf:unsigned x <> 2147483648
g:- unsigned x mod 4294967296 >= 2147483648
g0:unsigned x >= 2147483648
n:unsigned x <> 0
unsigned x mod 4294967296 <> 0
x:Integers.int
Hhalf:unsigned x <> 2147483648
g:4294967296 - unsigned x >= 2147483648
g0:unsigned x >= 2147483648
n:unsigned x <> 0
H:unsigned x < 2147483648
- unsigned x mod 4294967296 - 4294967296 =
- (unsigned x - 4294967296)
x:Integers.int
Hhalf:unsigned x <> 2147483648
g:4294967296 - unsigned x mod 4294967296 >=
2147483648
g0:unsigned x >= 2147483648
n:unsigned x <> 0
0 <= unsigned x < 4294967296
x:Integers.int
Hhalf:unsigned x <> 2147483648
g:- unsigned x mod 4294967296 >= 2147483648
g0:unsigned x >= 2147483648
n:unsigned x <> 0
unsigned x mod 4294967296 <> 0
x:Integers.int
Hhalf:unsigned x <> 2147483648
g:4294967296 - unsigned x mod 4294967296 >=
2147483648
g0:unsigned x >= 2147483648
n:unsigned x <> 0
0 <= unsigned x < 4294967296
x:Integers.int
Hhalf:unsigned x <> 2147483648
g:- unsigned x mod 4294967296 >= 2147483648
g0:unsigned x >= 2147483648
n:unsigned x <> 0
unsigned x mod 4294967296 <> 0
x:Integers.int
Hhalf:unsigned x <> 2147483648
g:4294967296 - unsigned x mod 4294967296 >=
2147483648
g0:unsigned x >= 2147483648
n:unsigned x <> 0
H:0 <= unsigned x <= max_unsigned
0 <= unsigned x < 4294967296
x:Integers.int
Hhalf:unsigned x <> 2147483648
g:- unsigned x mod 4294967296 >= 2147483648
g0:unsigned x >= 2147483648
n:unsigned x <> 0
unsigned x mod 4294967296 <> 0
x:Integers.int
Hhalf:unsigned x <> 2147483648
g:4294967296 - unsigned x mod 4294967296 >=
2147483648
g0:unsigned x >= 2147483648
n:unsigned x <> 0
H:0 <= unsigned x <= 4294967295
0 <= unsigned x < 4294967296
x:Integers.int
Hhalf:unsigned x <> 2147483648
g:- unsigned x mod 4294967296 >= 2147483648
g0:unsigned x >= 2147483648
n:unsigned x <> 0
unsigned x mod 4294967296 <> 0
x:Integers.int
Hhalf:unsigned x <> 2147483648
g:- unsigned x mod 4294967296 >= 2147483648
g0:unsigned x >= 2147483648
n:unsigned x <> 0
unsigned x mod 4294967296 <> 0
x:Integers.int
Hhalf:unsigned x <> 2147483648
g:- unsigned x mod 4294967296 >= 2147483648
g0:unsigned x >= 2147483648
n:unsigned x <> 0
unsigned x <> 0
x:Integers.int
Hhalf:unsigned x <> 2147483648
g:- unsigned x mod 4294967296 >= 2147483648
g0:unsigned x >= 2147483648
n:unsigned x <> 0
0 <= unsigned x < 4294967296
x:Integers.int
Hhalf:unsigned x <> 2147483648
g:- unsigned x mod 4294967296 >= 2147483648
g0:unsigned x >= 2147483648
n:unsigned x <> 0
0 <= unsigned x < 4294967296
x:Integers.int
Hhalf:unsigned x <> 2147483648
g:- unsigned x mod 4294967296 >= 2147483648
g0:unsigned x >= 2147483648
n:unsigned x <> 0
H:0 <= unsigned x <= max_unsigned
0 <= unsigned x < 4294967296
x:Integers.int
Hhalf:unsigned x <> 2147483648
g:- unsigned x mod 4294967296 >= 2147483648
g0:unsigned x >= 2147483648
n:unsigned x <> 0
H:0 <= unsigned x <= 4294967295
0 <= unsigned x < 4294967296
lia.Qed.
forallxy : Integers.int,
unsigned x <> 2147483648 ->
neg (divs x y) = divs (neg x) y
forallxy : Integers.int,
unsigned x <> 2147483648 ->
neg (divs x y) = divs (neg x) y
x, y:Integers.int
Hhalf:unsigned x <> 2147483648
neg (divs x y) = divs (neg x) y
x, y:Integers.int
Hhalf:unsigned x <> 2147483648
repr (- unsigned (repr (signed x ÷ signed y))) =
repr (signed (repr (- unsigned x)) ÷ signed y)
x, y:Integers.int
Hhalf:unsigned x <> 2147483648
x':=signed x:Z
repr (- unsigned (repr (x' ÷ signed y))) =
repr (signed (repr (- unsigned x)) ÷ signed y)
g:match2 ^ unsigned y with
| 0 => 0
| Z.pos p => Zbits.P_mod_two_p p wordsize
| Z.neg p =>
if zeq (Zbits.P_mod_two_p p wordsize) 0then0else modulus - Zbits.P_mod_two_p p wordsize
end >= 4294967296 / 2
match Z.shiftl 1 (unsigned y) with
| 0 => 0
| Z.pos p => Zbits.P_mod_two_p p wordsize
| Z.neg p =>
if zeq (Zbits.P_mod_two_p p wordsize) 0then0else modulus - Zbits.P_mod_two_p p wordsize
end - 4294967296 >= 0
y:Integers.int
H:unsigned y <= 30
Heqz:2 ^ unsigned y = 0
g:0 >= 4294967296 / 2
match Z.shiftl 1 (unsigned y) with
| 0 => 0
| Z.pos p => Zbits.P_mod_two_p p wordsize
| Z.neg p =>
if zeq (Zbits.P_mod_two_p p wordsize) 0then0else modulus - Zbits.P_mod_two_p p wordsize
end - 4294967296 >= 0
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.pos p
g:Zbits.P_mod_two_p p wordsize >= 4294967296 / 2
match Z.shiftl 1 (unsigned y) with
| 0 => 0
| Z.pos p => Zbits.P_mod_two_p p wordsize
| Z.neg p =>
if zeq (Zbits.P_mod_two_p p wordsize) 0then0else modulus - Zbits.P_mod_two_p p wordsize
end - 4294967296 >= 0
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.neg p
g:(if zeq (Zbits.P_mod_two_p p wordsize) 0then0else modulus - Zbits.P_mod_two_p p wordsize) >=
4294967296 / 2
match Z.shiftl 1 (unsigned y) with
| 0 => 0
| Z.pos p => Zbits.P_mod_two_p p wordsize
| Z.neg p =>
if zeq (Zbits.P_mod_two_p p wordsize) 0then0else modulus - Zbits.P_mod_two_p p wordsize
end - 4294967296 >= 0
y:Integers.int
H:unsigned y <= 30
Heqz:2 ^ unsigned y = 0
g:4294967296 / 2 <= 0
match Z.shiftl 1 (unsigned y) with
| 0 => 0
| Z.pos p => Zbits.P_mod_two_p p wordsize
| Z.neg p =>
if zeq (Zbits.P_mod_two_p p wordsize) 0then0else modulus - Zbits.P_mod_two_p p wordsize
end - 4294967296 >= 0
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.pos p
g:Zbits.P_mod_two_p p wordsize >= 4294967296 / 2
match Z.shiftl 1 (unsigned y) with
| 0 => 0
| Z.pos p => Zbits.P_mod_two_p p wordsize
| Z.neg p =>
if zeq (Zbits.P_mod_two_p p wordsize) 0then0else modulus - Zbits.P_mod_two_p p wordsize
end - 4294967296 >= 0
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.neg p
g:(if zeq (Zbits.P_mod_two_p p wordsize) 0then0else modulus - Zbits.P_mod_two_p p wordsize) >=
4294967296 / 2
match Z.shiftl 1 (unsigned y) with
| 0 => 0
| Z.pos p => Zbits.P_mod_two_p p wordsize
| Z.neg p =>
if zeq (Zbits.P_mod_two_p p wordsize) 0then0else modulus - Zbits.P_mod_two_p p wordsize
end - 4294967296 >= 0
y:Integers.int
H:unsigned y <= 30
Heqz:2 ^ unsigned y = 0
g:4294967296 / 2 <= 0
False
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.pos p
g:Zbits.P_mod_two_p p wordsize >= 4294967296 / 2
match Z.shiftl 1 (unsigned y) with
| 0 => 0
| Z.pos p => Zbits.P_mod_two_p p wordsize
| Z.neg p =>
if zeq (Zbits.P_mod_two_p p wordsize) 0then0else modulus - Zbits.P_mod_two_p p wordsize
end - 4294967296 >= 0
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.neg p
g:(if zeq (Zbits.P_mod_two_p p wordsize) 0then0else modulus - Zbits.P_mod_two_p p wordsize) >=
4294967296 / 2
match Z.shiftl 1 (unsigned y) with
| 0 => 0
| Z.pos p => Zbits.P_mod_two_p p wordsize
| Z.neg p =>
if zeq (Zbits.P_mod_two_p p wordsize) 0then0else modulus - Zbits.P_mod_two_p p wordsize
end - 4294967296 >= 0
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.pos p
g:Zbits.P_mod_two_p p wordsize >= 4294967296 / 2
match Z.shiftl 1 (unsigned y) with
| 0 => 0
| Z.pos p => Zbits.P_mod_two_p p wordsize
| Z.neg p =>
if zeq (Zbits.P_mod_two_p p wordsize) 0then0else modulus - Zbits.P_mod_two_p p wordsize
end - 4294967296 >= 0
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.neg p
g:(if zeq (Zbits.P_mod_two_p p wordsize) 0then0else modulus - Zbits.P_mod_two_p p wordsize) >=
4294967296 / 2
match Z.shiftl 1 (unsigned y) with
| 0 => 0
| Z.pos p => Zbits.P_mod_two_p p wordsize
| Z.neg p =>
if zeq (Zbits.P_mod_two_p p wordsize) 0then0else modulus - Zbits.P_mod_two_p p wordsize
end - 4294967296 >= 0
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.pos p
g:Zbits.P_mod_two_p p wordsize >= 4294967296 / 2
match2 ^ unsigned y with
| 0 => 0
| Z.pos p => Zbits.P_mod_two_p p wordsize
| Z.neg p =>
if zeq (Zbits.P_mod_two_p p wordsize) 0then0else modulus - Zbits.P_mod_two_p p wordsize
end - 4294967296 >= 0
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.neg p
g:(if zeq (Zbits.P_mod_two_p p wordsize) 0then0else modulus - Zbits.P_mod_two_p p wordsize) >=
4294967296 / 2
match Z.shiftl 1 (unsigned y) with
| 0 => 0
| Z.pos p => Zbits.P_mod_two_p p wordsize
| Z.neg p =>
if zeq (Zbits.P_mod_two_p p wordsize) 0then0else modulus - Zbits.P_mod_two_p p wordsize
end - 4294967296 >= 0
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.pos p
g:Zbits.P_mod_two_p p wordsize >= 4294967296 / 2
Zbits.P_mod_two_p p wordsize - 4294967296 >= 0
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.neg p
g:(if zeq (Zbits.P_mod_two_p p wordsize) 0then0else modulus - Zbits.P_mod_two_p p wordsize) >=
4294967296 / 2
match Z.shiftl 1 (unsigned y) with
| 0 => 0
| Z.pos p => Zbits.P_mod_two_p p wordsize
| Z.neg p =>
if zeq (Zbits.P_mod_two_p p wordsize) 0then0else modulus - Zbits.P_mod_two_p p wordsize
end - 4294967296 >= 0
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.pos p
g:Zbits.P_mod_two_p p Wordsize_32.wordsize >=
4294967296 / 2
Zbits.P_mod_two_p p Wordsize_32.wordsize - 4294967296 >=
0
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.neg p
g:(if zeq (Zbits.P_mod_two_p p wordsize) 0then0else modulus - Zbits.P_mod_two_p p wordsize) >=
4294967296 / 2
match Z.shiftl 1 (unsigned y) with
| 0 => 0
| Z.pos p => Zbits.P_mod_two_p p wordsize
| Z.neg p =>
if zeq (Zbits.P_mod_two_p p wordsize) 0then0else modulus - Zbits.P_mod_two_p p wordsize
end - 4294967296 >= 0
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.pos p
g:Zbits.P_mod_two_p p 32 >= 4294967296 / 2
Zbits.P_mod_two_p p 32 - 4294967296 >= 0
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.neg p
g:(if zeq (Zbits.P_mod_two_p p wordsize) 0then0else modulus - Zbits.P_mod_two_p p wordsize) >=
4294967296 / 2
match Z.shiftl 1 (unsigned y) with
| 0 => 0
| Z.pos p => Zbits.P_mod_two_p p wordsize
| Z.neg p =>
if zeq (Zbits.P_mod_two_p p wordsize) 0then0else modulus - Zbits.P_mod_two_p p wordsize
end - 4294967296 >= 0
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.pos p
g:Z.pos p mod two_power_nat 32 >= 4294967296 / 2
Z.pos p mod two_power_nat 32 - 4294967296 >= 0
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.neg p
g:(if zeq (Zbits.P_mod_two_p p wordsize) 0then0else modulus - Zbits.P_mod_two_p p wordsize) >=
4294967296 / 2
match Z.shiftl 1 (unsigned y) with
| 0 => 0
| Z.pos p => Zbits.P_mod_two_p p wordsize
| Z.neg p =>
if zeq (Zbits.P_mod_two_p p wordsize) 0then0else modulus - Zbits.P_mod_two_p p wordsize
end - 4294967296 >= 0
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.pos p
g:Z.pos p mod two_power_nat 32 >= 2147483648
Z.pos p mod two_power_nat 32 - 4294967296 >= 0
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.neg p
g:(if zeq (Zbits.P_mod_two_p p wordsize) 0then0else modulus - Zbits.P_mod_two_p p wordsize) >=
4294967296 / 2
match Z.shiftl 1 (unsigned y) with
| 0 => 0
| Z.pos p => Zbits.P_mod_two_p p wordsize
| Z.neg p =>
if zeq (Zbits.P_mod_two_p p wordsize) 0then0else modulus - Zbits.P_mod_two_p p wordsize
end - 4294967296 >= 0
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.pos p
g:2 ^ unsigned y mod two_power_nat 32 >= 2147483648
Z.pos p mod two_power_nat 32 - 4294967296 >= 0
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.neg p
g:(if zeq (Zbits.P_mod_two_p p wordsize) 0then0else modulus - Zbits.P_mod_two_p p wordsize) >=
4294967296 / 2
match Z.shiftl 1 (unsigned y) with
| 0 => 0
| Z.pos p => Zbits.P_mod_two_p p wordsize
| Z.neg p =>
if zeq (Zbits.P_mod_two_p p wordsize) 0then0else modulus - Zbits.P_mod_two_p p wordsize
end - 4294967296 >= 0
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.pos p
g:2 ^ unsigned y >= 2147483648
Z.pos p mod two_power_nat 32 - 4294967296 >= 0
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.pos p
g:2 ^ unsigned y mod two_power_nat 32 >= 2147483648
0 <= 2 ^ unsigned y < two_power_nat 32
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.neg p
g:(if zeq (Zbits.P_mod_two_p p wordsize) 0then0else modulus - Zbits.P_mod_two_p p wordsize) >=
4294967296 / 2
match Z.shiftl 1 (unsigned y) with
| 0 => 0
| Z.pos p => Zbits.P_mod_two_p p wordsize
| Z.neg p =>
if zeq (Zbits.P_mod_two_p p wordsize) 0then0else modulus - Zbits.P_mod_two_p p wordsize
end - 4294967296 >= 0
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.pos p
g:2 ^ unsigned y >= 2 ^ 31
Z.pos p mod two_power_nat 32 - 4294967296 >= 0
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.pos p
g:2 ^ unsigned y >= 2147483648
2 ^ 31 = 2147483648
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.pos p
g:2 ^ unsigned y mod two_power_nat 32 >= 2147483648
0 <= 2 ^ unsigned y < two_power_nat 32
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.neg p
g:(if zeq (Zbits.P_mod_two_p p wordsize) 0then0else modulus - Zbits.P_mod_two_p p wordsize) >=
4294967296 / 2
match Z.shiftl 1 (unsigned y) with
| 0 => 0
| Z.pos p => Zbits.P_mod_two_p p wordsize
| Z.neg p =>
if zeq (Zbits.P_mod_two_p p wordsize) 0then0else modulus - Zbits.P_mod_two_p p wordsize
end - 4294967296 >= 0
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.pos p
g:2 ^ unsigned y >= 2 ^ 31
H0:0 < 2 ->
unsigned y <= 30 -> 2 ^ unsigned y <= 2 ^ 30
Z.pos p mod two_power_nat 32 - 4294967296 >= 0
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.pos p
g:2 ^ unsigned y >= 2147483648
2 ^ 31 = 2147483648
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.pos p
g:2 ^ unsigned y mod two_power_nat 32 >= 2147483648
0 <= 2 ^ unsigned y < two_power_nat 32
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.neg p
g:(if zeq (Zbits.P_mod_two_p p wordsize) 0then0else modulus - Zbits.P_mod_two_p p wordsize) >=
4294967296 / 2
match Z.shiftl 1 (unsigned y) with
| 0 => 0
| Z.pos p => Zbits.P_mod_two_p p wordsize
| Z.neg p =>
if zeq (Zbits.P_mod_two_p p wordsize) 0then0else modulus - Zbits.P_mod_two_p p wordsize
end - 4294967296 >= 0
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.pos p
g:2 ^ 31 <= 2 ^ unsigned y
H0:0 < 2 ->
unsigned y <= 30 -> 2 ^ unsigned y <= 2 ^ 30
Z.pos p mod two_power_nat 32 - 4294967296 >= 0
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.pos p
g:2 ^ unsigned y >= 2147483648
2 ^ 31 = 2147483648
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.pos p
g:2 ^ unsigned y mod two_power_nat 32 >= 2147483648
0 <= 2 ^ unsigned y < two_power_nat 32
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.neg p
g:(if zeq (Zbits.P_mod_two_p p wordsize) 0then0else modulus - Zbits.P_mod_two_p p wordsize) >=
4294967296 / 2
match Z.shiftl 1 (unsigned y) with
| 0 => 0
| Z.pos p => Zbits.P_mod_two_p p wordsize
| Z.neg p =>
if zeq (Zbits.P_mod_two_p p wordsize) 0then0else modulus - Zbits.P_mod_two_p p wordsize
end - 4294967296 >= 0
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.pos p
g:2 ^ 31 <= 2 ^ unsigned y
H0:0 < 2 ->
unsigned y <= 30 -> 2 ^ unsigned y <= 2 ^ 30
H1:0 < 2
Z.pos p mod two_power_nat 32 - 4294967296 >= 0
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.pos p
g:2 ^ unsigned y >= 2147483648
2 ^ 31 = 2147483648
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.pos p
g:2 ^ unsigned y mod two_power_nat 32 >= 2147483648
0 <= 2 ^ unsigned y < two_power_nat 32
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.neg p
g:(if zeq (Zbits.P_mod_two_p p wordsize) 0then0else modulus - Zbits.P_mod_two_p p wordsize) >=
4294967296 / 2
match Z.shiftl 1 (unsigned y) with
| 0 => 0
| Z.pos p => Zbits.P_mod_two_p p wordsize
| Z.neg p =>
if zeq (Zbits.P_mod_two_p p wordsize) 0then0else modulus - Zbits.P_mod_two_p p wordsize
end - 4294967296 >= 0
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.pos p
g:2 ^ 31 <= 2 ^ unsigned y
H0:0 < 2 ->
unsigned y <= 30 -> 2 ^ unsigned y <= 2 ^ 30
H1:2 ^ unsigned y <= 2 ^ 30
Z.pos p mod two_power_nat 32 - 4294967296 >= 0
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.pos p
g:2 ^ 31 <= 2 ^ unsigned y
H0:0 < 2 ->
unsigned y <= 30 -> 2 ^ unsigned y <= 2 ^ 30
H1:0 < 2
unsigned y <= 30
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.pos p
g:2 ^ unsigned y >= 2147483648
2 ^ 31 = 2147483648
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.pos p
g:2 ^ unsigned y mod two_power_nat 32 >= 2147483648
0 <= 2 ^ unsigned y < two_power_nat 32
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.neg p
g:(if zeq (Zbits.P_mod_two_p p wordsize) 0then0else modulus - Zbits.P_mod_two_p p wordsize) >=
4294967296 / 2
match Z.shiftl 1 (unsigned y) with
| 0 => 0
| Z.pos p => Zbits.P_mod_two_p p wordsize
| Z.neg p =>
if zeq (Zbits.P_mod_two_p p wordsize) 0then0else modulus - Zbits.P_mod_two_p p wordsize
end - 4294967296 >= 0
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.pos p
g:2 ^ 31 <= 2 ^ unsigned y
H0:0 < 2 ->
unsigned y <= 30 -> 2 ^ unsigned y <= 2 ^ 30
H1:0 < 2
unsigned y <= 30
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.pos p
g:2 ^ unsigned y >= 2147483648
2 ^ 31 = 2147483648
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.pos p
g:2 ^ unsigned y mod two_power_nat 32 >= 2147483648
0 <= 2 ^ unsigned y < two_power_nat 32
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.neg p
g:(if zeq (Zbits.P_mod_two_p p wordsize) 0then0else modulus - Zbits.P_mod_two_p p wordsize) >=
4294967296 / 2
match Z.shiftl 1 (unsigned y) with
| 0 => 0
| Z.pos p => Zbits.P_mod_two_p p wordsize
| Z.neg p =>
if zeq (Zbits.P_mod_two_p p wordsize) 0then0else modulus - Zbits.P_mod_two_p p wordsize
end - 4294967296 >= 0
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.pos p
g:2 ^ unsigned y >= 2147483648
2 ^ 31 = 2147483648
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.pos p
g:2 ^ unsigned y mod two_power_nat 32 >= 2147483648
0 <= 2 ^ unsigned y < two_power_nat 32
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.neg p
g:(if zeq (Zbits.P_mod_two_p p wordsize) 0then0else modulus - Zbits.P_mod_two_p p wordsize) >=
4294967296 / 2
match Z.shiftl 1 (unsigned y) with
| 0 => 0
| Z.pos p => Zbits.P_mod_two_p p wordsize
| Z.neg p =>
if zeq (Zbits.P_mod_two_p p wordsize) 0then0else modulus - Zbits.P_mod_two_p p wordsize
end - 4294967296 >= 0
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.pos p
g:2 ^ unsigned y mod two_power_nat 32 >= 2147483648
0 <= 2 ^ unsigned y < two_power_nat 32
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.neg p
g:(if zeq (Zbits.P_mod_two_p p wordsize) 0then0else modulus - Zbits.P_mod_two_p p wordsize) >=
4294967296 / 2
match Z.shiftl 1 (unsigned y) with
| 0 => 0
| Z.pos p => Zbits.P_mod_two_p p wordsize
| Z.neg p =>
if zeq (Zbits.P_mod_two_p p wordsize) 0then0else modulus - Zbits.P_mod_two_p p wordsize
end - 4294967296 >= 0
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.pos p
g:2 ^ unsigned y mod two_power_nat 32 >= 2147483648
0 <= 2 ^ unsigned y
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.pos p
g:2 ^ unsigned y mod two_power_nat 32 >= 2147483648
2 ^ unsigned y < two_power_nat 32
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.neg p
g:(if zeq (Zbits.P_mod_two_p p wordsize) 0then0else modulus - Zbits.P_mod_two_p p wordsize) >=
4294967296 / 2
match Z.shiftl 1 (unsigned y) with
| 0 => 0
| Z.pos p => Zbits.P_mod_two_p p wordsize
| Z.neg p =>
if zeq (Zbits.P_mod_two_p p wordsize) 0then0else modulus - Zbits.P_mod_two_p p wordsize
end - 4294967296 >= 0
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.pos p
g:2 ^ unsigned y mod two_power_nat 32 >= 2147483648
2 ^ unsigned y < two_power_nat 32
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.neg p
g:(if zeq (Zbits.P_mod_two_p p wordsize) 0then0else modulus - Zbits.P_mod_two_p p wordsize) >=
4294967296 / 2
match Z.shiftl 1 (unsigned y) with
| 0 => 0
| Z.pos p => Zbits.P_mod_two_p p wordsize
| Z.neg p =>
if zeq (Zbits.P_mod_two_p p wordsize) 0then0else modulus - Zbits.P_mod_two_p p wordsize
end - 4294967296 >= 0
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.pos p
g:2 ^ unsigned y mod two_power_nat 32 >= 2147483648
2 ^ unsigned y < 2 ^ Z.of_nat 32
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.neg p
g:(if zeq (Zbits.P_mod_two_p p wordsize) 0then0else modulus - Zbits.P_mod_two_p p wordsize) >=
4294967296 / 2
match Z.shiftl 1 (unsigned y) with
| 0 => 0
| Z.pos p => Zbits.P_mod_two_p p wordsize
| Z.neg p =>
if zeq (Zbits.P_mod_two_p p wordsize) 0then0else modulus - Zbits.P_mod_two_p p wordsize
end - 4294967296 >= 0
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.neg p
g:(if zeq (Zbits.P_mod_two_p p wordsize) 0then0else modulus - Zbits.P_mod_two_p p wordsize) >=
4294967296 / 2
match Z.shiftl 1 (unsigned y) with
| 0 => 0
| Z.pos p => Zbits.P_mod_two_p p wordsize
| Z.neg p =>
if zeq (Zbits.P_mod_two_p p wordsize) 0then0else modulus - Zbits.P_mod_two_p p wordsize
end - 4294967296 >= 0
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.neg p
g:(if zeq (Zbits.P_mod_two_p p wordsize) 0then0else modulus - Zbits.P_mod_two_p p wordsize) >=
4294967296 / 2
H0:Z.neg p < 0
match Z.shiftl 1 (unsigned y) with
| 0 => 0
| Z.pos p => Zbits.P_mod_two_p p wordsize
| Z.neg p =>
if zeq (Zbits.P_mod_two_p p wordsize) 0then0else modulus - Zbits.P_mod_two_p p wordsize
end - 4294967296 >= 0
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.neg p
g:(if zeq (Zbits.P_mod_two_p p wordsize) 0then0else modulus - Zbits.P_mod_two_p p wordsize) >=
4294967296 / 2
H0:Z.neg p < 0
H1:0 <= 2 -> 0 <= 2 ^ unsigned y
match Z.shiftl 1 (unsigned y) with
| 0 => 0
| Z.pos p => Zbits.P_mod_two_p p wordsize
| Z.neg p =>
if zeq (Zbits.P_mod_two_p p wordsize) 0then0else modulus - Zbits.P_mod_two_p p wordsize
end - 4294967296 >= 0
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.neg p
g:(if zeq (Zbits.P_mod_two_p p wordsize) 0then0else modulus - Zbits.P_mod_two_p p wordsize) >=
4294967296 / 2
H0:2 ^ unsigned y < 0
H1:0 <= 2 -> 0 <= 2 ^ unsigned y
match Z.shiftl 1 (unsigned y) with
| 0 => 0
| Z.pos p => Zbits.P_mod_two_p p wordsize
| Z.neg p =>
if zeq (Zbits.P_mod_two_p p wordsize) 0then0else modulus - Zbits.P_mod_two_p p wordsize
end - 4294967296 >= 0
lia.Qed.
forally : Integers.int,
unsigned y <= 30 -> is_power2 (shl one y) = Some y
forally : Integers.int,
unsigned y <= 30 -> is_power2 (shl one y) = Some y
y:Integers.int
H:unsigned y <= 30
is_power2 (shl one y) = Some y
y:Integers.int
H:unsigned y <= 30
match
Zbits.Z_is_power2
(unsigned
(repr (Z.shiftl (unsigned one) (unsigned y))))
with
| Some i => Some (repr i)
| None => None
end = Some y
y:Integers.int
H:unsigned y <= 30
z:Z
Heqo:Zbits.Z_is_power2
(unsigned
(repr
(Z.shiftl (unsigned one) (unsigned y)))) =
Some z