Commit d6b6f384 authored by MARCHE Claude's avatar MARCHE Claude

Coq proofs in bitvector1

parent af9470bf
......@@ -11,72 +11,72 @@ theory Pow2int
lemma Power_1 : pow2 1 = 2
lemma Power_sum :
lemma Power_sum :
forall n m: int. n >= 0 /\ m >= 0 -> pow2 (n+m) = pow2 n * pow2 m
lemma pow2_0: pow2 0 = 1
lemma pow2_1: pow2 1 = 2
lemma pow2_2: pow2 2 = 4
lemma pow2_3: pow2 3 = 8
lemma pow2_4: pow2 4 = 16
lemma pow2_5: pow2 5 = 32
lemma pow2_6: pow2 6 = 64
lemma pow2_7: pow2 7 = 128
lemma pow2_8: pow2 8 = 256
lemma pow2_9: pow2 9 = 512
lemma pow2_10: pow2 10 = 1024
lemma pow2_11: pow2 11 = 2048
lemma pow2_12: pow2 12 = 4096
lemma pow2_13: pow2 13 = 8192
lemma pow2_14: pow2 14 = 16384
lemma pow2_15: pow2 15 = 32768
lemma pow2_16: pow2 16 = 65536
lemma pow2_17: pow2 17 = 131072
lemma pow2_18: pow2 18 = 262144
lemma pow2_19: pow2 19 = 524288
lemma pow2_20: pow2 20 = 1048576
lemma pow2_21: pow2 21 = 2097152
lemma pow2_22: pow2 22 = 4194304
lemma pow2_23: pow2 23 = 8388608
lemma pow2_24: pow2 24 = 16777216
lemma pow2_25: pow2 25 = 33554432
lemma pow2_26: pow2 26 = 67108864
lemma pow2_27: pow2 27 = 134217728
lemma pow2_28: pow2 28 = 268435456
lemma pow2_29: pow2 29 = 536870912
lemma pow2_30: pow2 30 = 1073741824
lemma pow2_31: pow2 31 = 2147483648
lemma pow2_32: pow2 32 = 4294967296
lemma pow2_33: pow2 33 = 8589934592
lemma pow2_34: pow2 34 = 17179869184
lemma pow2_35: pow2 35 = 34359738368
lemma pow2_36: pow2 36 = 68719476736
lemma pow2_37: pow2 37 = 137438953472
lemma pow2_38: pow2 38 = 274877906944
lemma pow2_39: pow2 39 = 549755813888
lemma pow2_40: pow2 40 = 1099511627776
lemma pow2_41: pow2 41 = 2199023255552
lemma pow2_42: pow2 42 = 4398046511104
lemma pow2_43: pow2 43 = 8796093022208
lemma pow2_44: pow2 44 = 17592186044416
lemma pow2_45: pow2 45 = 35184372088832
lemma pow2_46: pow2 46 = 70368744177664
lemma pow2_47: pow2 47 = 140737488355328
lemma pow2_48: pow2 48 = 281474976710656
lemma pow2_49: pow2 49 = 562949953421312
lemma pow2_50: pow2 50 = 1125899906842624
lemma pow2_51: pow2 51 = 2251799813685248
lemma pow2_52: pow2 52 = 4503599627370496
lemma pow2_53: pow2 53 = 9007199254740992
lemma pow2_54: pow2 54 = 18014398509481984
lemma pow2_55: pow2 55 = 36028797018963968
lemma pow2_56: pow2 56 = 72057594037927936
lemma pow2_57: pow2 57 = 144115188075855872
lemma pow2_58: pow2 58 = 288230376151711744
lemma pow2_59: pow2 59 = 576460752303423488
lemma pow2_60: pow2 60 = 1152921504606846976
lemma pow2_61: pow2 61 = 2305843009213693952
lemma pow2_62: pow2 62 = 4611686018427387904
lemma pow2_0: pow2 0 = 1
lemma pow2_1: pow2 1 = 2
lemma pow2_2: pow2 2 = 4
lemma pow2_3: pow2 3 = 8
lemma pow2_4: pow2 4 = 16
lemma pow2_5: pow2 5 = 32
lemma pow2_6: pow2 6 = 64
lemma pow2_7: pow2 7 = 128
lemma pow2_8: pow2 8 = 256
lemma pow2_9: pow2 9 = 512
lemma pow2_10: pow2 10 = 1024
lemma pow2_11: pow2 11 = 2048
lemma pow2_12: pow2 12 = 4096
lemma pow2_13: pow2 13 = 8192
lemma pow2_14: pow2 14 = 16384
lemma pow2_15: pow2 15 = 32768
lemma pow2_16: pow2 16 = 65536
lemma pow2_17: pow2 17 = 131072
lemma pow2_18: pow2 18 = 262144
lemma pow2_19: pow2 19 = 524288
lemma pow2_20: pow2 20 = 1048576
lemma pow2_21: pow2 21 = 2097152
lemma pow2_22: pow2 22 = 4194304
lemma pow2_23: pow2 23 = 8388608
lemma pow2_24: pow2 24 = 16777216
lemma pow2_25: pow2 25 = 33554432
lemma pow2_26: pow2 26 = 67108864
lemma pow2_27: pow2 27 = 134217728
lemma pow2_28: pow2 28 = 268435456
lemma pow2_29: pow2 29 = 536870912
lemma pow2_30: pow2 30 = 1073741824
lemma pow2_31: pow2 31 = 2147483648
lemma pow2_32: pow2 32 = 4294967296
lemma pow2_33: pow2 33 = 8589934592
lemma pow2_34: pow2 34 = 17179869184
lemma pow2_35: pow2 35 = 34359738368
lemma pow2_36: pow2 36 = 68719476736
lemma pow2_37: pow2 37 = 137438953472
lemma pow2_38: pow2 38 = 274877906944
lemma pow2_39: pow2 39 = 549755813888
lemma pow2_40: pow2 40 = 1099511627776
lemma pow2_41: pow2 41 = 2199023255552
lemma pow2_42: pow2 42 = 4398046511104
lemma pow2_43: pow2 43 = 8796093022208
lemma pow2_44: pow2 44 = 17592186044416
lemma pow2_45: pow2 45 = 35184372088832
lemma pow2_46: pow2 46 = 70368744177664
lemma pow2_47: pow2 47 = 140737488355328
lemma pow2_48: pow2 48 = 281474976710656
lemma pow2_49: pow2 49 = 562949953421312
lemma pow2_50: pow2 50 = 1125899906842624
lemma pow2_51: pow2 51 = 2251799813685248
lemma pow2_52: pow2 52 = 4503599627370496
lemma pow2_53: pow2 53 = 9007199254740992
lemma pow2_54: pow2 54 = 18014398509481984
lemma pow2_55: pow2 55 = 36028797018963968
lemma pow2_56: pow2 56 = 72057594037927936
lemma pow2_57: pow2 57 = 144115188075855872
lemma pow2_58: pow2 58 = 288230376151711744
lemma pow2_59: pow2 59 = 576460752303423488
lemma pow2_60: pow2 60 = 1152921504606846976
lemma pow2_61: pow2 61 = 2305843009213693952
lemma pow2_62: pow2 62 = 4611686018427387904
lemma pow2_63: pow2 63 = 9223372036854775808
end
......@@ -86,7 +86,7 @@ theory Pow2real
use import int.Int
use import real.RealInfix
function pow2 (i:int) : real
function pow2 (i:int) : real
axiom Power_0 : pow2 0 = 1.0
......@@ -294,7 +294,7 @@ theory BitVector
lemma to_nat_of_zero:
forall b:bv, i j:int. j >=i ->
forall b:bv, i j:int. j >=i ->
(forall k:int. j >= k >= i -> nth b k = False) ->
to_nat_sub b j i = 0
......@@ -350,13 +350,13 @@ theory BitVector
forall b:bv. nth b (size-1) = True ->
to_int_aux b (size-1) = -1
lemma to_int_zero:
forall b:bv. (forall i:int. 0 <= i <size-1-> nth b i = False)
forall b:bv. (forall i:int. 0 <= i <size-1-> nth b i = False)
-> to_int_aux b 0 = 0
lemma to_int_one:
forall b:bv. (forall i:int. 0 <= i <size-> nth b i = True)
forall b:bv. (forall i:int. 0 <= i <size-> nth b i = True)
-> to_int_aux b 0 = -1
function to_int (b:bv) : int = to_int_aux b 0
*)
......@@ -446,13 +446,13 @@ theory BV_double
use import real.FromInt
function double_of_bv64 (b:bv) : real
(* TODO: axioms
(* TODO: axioms
real represented by bv = sign . exp . mantissa
sign on bit 63
exp on bits 62..52
exp on bits 62..52
mantissa on bits 51..0
......@@ -466,7 +466,7 @@ theory BV_double
where bias = 1023, prec = 53
(e.g. the largest representable number is 2^(2046-1023) * (1+ (2^52-1)* 2^(-52)) =
2^1023 * (1 + 1 - 2^-52) = 2^1024 - 2^(1023-52) = 2^1024 - 2^971
2^1023 * (1 + 1 - 2^-52) = 2^1024 - 2^(1023-52) = 2^1024 - 2^971
)
*)
......@@ -579,9 +579,9 @@ theory TestDoubleOfInt
function const : BV64.bv = BV32_64.concat j j'
lemma sign_const: sign(const) = False
lemma exp_const: exp(const) = 1075
lemma mantissa_const_nth:
forall i:int. 0 <= i <= 30 -> BV64.nth const i = False
......@@ -606,27 +606,25 @@ theory TestDoubleOfInt
function const_as_double : real = double_of_bv64 const
lemma const_value0: const_as_double =
lemma const_value0: const_as_double =
1.0*.Pow2real.pow2 (1075 - 1023) *. (1.0 +. Pow2real.pow2 31 *. Pow2real.pow2 (-52))
lemma const_value: const_as_double = Pow2real.pow2 52 +. Pow2real.pow2 31
function jpxor(i:int): BV32.bv
axiom jxori_axiom: forall i:int. jpxor(i) = (BV32.bw_xor j' (BV32.from_int i))
function jpxor(i:int): BV32.bv = (BV32.bw_xor j' (BV32.from_int i))
function var(i:int): BV64.bv = (BV32_64.concat j (jpxor i))
lemma nth30_0:
forall x:BV32.bv, j:int. 0 <= j <31 ->
forall x:BV32.bv, j:int. 0 <= j <31 ->
(BV32.nth (BV32.bw_xor j' x) j) = (BV32.nth x j)
lemma nth30_0_var:
forall x:int, j:int. 0 <= j <31 ->
forall x:int, j:int. 0 <= j <31 ->
(BV64.nth (var x) j) = (BV32.nth (BV32.from_int x) j)
lemma nth31_var:
lemma nth31_var:
forall x:int. (BV64.nth (var x) 31) = notb (BV32.nth (BV32.from_int x) 31)
lemma nth63_32_var:
......@@ -638,10 +636,10 @@ theory TestDoubleOfInt
lemma mantissa_var_0_30:
forall x:int. (BV32.nth (BV32.from_int x) 31) = False -> BV64.to_nat_sub (var x) 30 0 = x
lemma mantissa_var_0_30_1:
forall x:int. (BV32.nth (BV32.from_int x) 31) = True -> BV64.to_nat_sub (var x) 30 0 = -x
lemma mantissa_var: forall x:int. mantissa(var(x)) = Pow2int.pow2 31 + x
lemma realx_a_mx: forall x:int. Pow2real.pow2 (1075 - 1023) *. ((Pow2real.pow2 31 +. (from_int x)) *. Pow2real.pow2 (-52)) = Pow2real.pow2 31 +. (from_int x)
......@@ -654,8 +652,8 @@ theory TestDoubleOfInt
lemma int_real_from_int:
forall x:int. from_int (Pow2int.pow2 31 + x) = Pow2real.pow2 31 +. (from_int x)
(*proved by Coq*)
lemma var_value0: forall x:int. var_as_double(x) =
(*proved by Coq*)
lemma var_value0: forall x:int. var_as_double(x) =
Pow2real.pow2 (1075 - 1023) *. (1.0 +. (from_int (Pow2int.pow2 31 + x)) *. Pow2real.pow2 (-52))
lemma var_value: forall x:int. var_as_double(x) = Pow2real.pow2 52 +. Pow2real.pow2 31 +. (from_int x)
......@@ -698,7 +696,7 @@ theory TestBv32
to_nat bvzero = 0
goal to_nat_0x0000000F:
to_nat (lsr bvone 28) = 15
to_nat (lsr bvone 28) = 15
goal to_nat_0x0000001F:
to_nat (lsr bvone 27) = 31
......
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Definition implb(x:bool) (y:bool): bool := match (x,
y) with
| (true, false) => false
| (_, _) => true
end.
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 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).
Parameter size: Z.
Parameter bv : Type.
Parameter nth: bv -> Z -> bool.
Parameter bvzero: bv.
Axiom Nth_zero : forall (n:Z), ((0%Z <= n)%Z /\ (n < size)%Z) ->
((nth bvzero n) = false).
Parameter bvone: bv.
Axiom Nth_one : forall (n:Z), ((0%Z <= n)%Z /\ (n < size)%Z) -> ((nth bvone
n) = true).
Definition eq(v1:bv) (v2:bv): Prop := forall (n:Z), ((0%Z <= n)%Z /\
(n < size)%Z) -> ((nth v1 n) = (nth v2 n)).
Axiom extensionality : forall (v1:bv) (v2:bv), (eq v1 v2) -> (v1 = v2).
Parameter bw_and: bv -> bv -> bv.
Axiom Nth_bw_and : forall (v1:bv) (v2:bv) (n:Z), ((0%Z <= n)%Z /\
(n < size)%Z) -> ((nth (bw_and v1 v2) n) = (andb (nth v1 n) (nth v2 n))).
Parameter bw_or: bv -> bv -> bv.
Axiom Nth_bw_or : forall (v1:bv) (v2:bv) (n:Z), ((0%Z <= n)%Z /\
(n < size)%Z) -> ((nth (bw_or v1 v2) n) = (orb (nth v1 n) (nth v2 n))).
Parameter bw_xor: bv -> bv -> bv.
Axiom Nth_bw_xor : forall (v1:bv) (v2:bv) (n:Z), ((0%Z <= n)%Z /\
(n < size)%Z) -> ((nth (bw_xor v1 v2) n) = (xorb (nth v1 n) (nth v2 n))).
Axiom Nth_bw_xor_v1true : forall (v1:bv) (v2:bv) (n:Z), (((0%Z <= n)%Z /\
(n < size)%Z) /\ ((nth v1 n) = true)) -> ((nth (bw_xor v1 v2)
n) = (negb (nth v2 n))).
Axiom Nth_bw_xor_v1false : forall (v1:bv) (v2:bv) (n:Z), (((0%Z <= n)%Z /\
(n < size)%Z) /\ ((nth v1 n) = false)) -> ((nth (bw_xor v1 v2)
n) = (nth v2 n)).
Axiom Nth_bw_xor_v2true : forall (v1:bv) (v2:bv) (n:Z), (((0%Z <= n)%Z /\
(n < size)%Z) /\ ((nth v2 n) = true)) -> ((nth (bw_xor v1 v2)
n) = (negb (nth v1 n))).
Axiom Nth_bw_xor_v2false : forall (v1:bv) (v2:bv) (n:Z), (((0%Z <= n)%Z /\
(n < size)%Z) /\ ((nth v2 n) = false)) -> ((nth (bw_xor v1 v2)
n) = (nth v1 n)).
Parameter bw_not: bv -> bv.
Axiom Nth_bw_not : forall (v:bv) (n:Z), ((0%Z <= n)%Z /\ (n < size)%Z) ->
((nth (bw_not v) n) = (negb (nth v n))).
Parameter lsr: bv -> Z -> bv.
Axiom lsr_nth_low : forall (b:bv) (n:Z) (s:Z), ((0%Z <= n)%Z /\
(n < size)%Z) -> ((0%Z <= s)%Z -> (((n + s)%Z < size)%Z -> ((nth (lsr b
s) n) = (nth b (n + s)%Z)))).
Axiom lsr_nth_high : forall (b:bv) (n:Z) (s:Z), ((0%Z <= n)%Z /\
(n < size)%Z) -> ((0%Z <= s)%Z -> ((size <= (n + s)%Z)%Z -> ((nth (lsr b
s) n) = false))).
Parameter asr: bv -> Z -> bv.
Axiom asr_nth_low : forall (b:bv) (n:Z) (s:Z), ((0%Z <= n)%Z /\
(n < size)%Z) -> ((0%Z <= s)%Z -> (((n + s)%Z < size)%Z -> ((nth (asr b
s) n) = (nth b (n + s)%Z)))).
Axiom asr_nth_high : forall (b:bv) (n:Z) (s:Z), ((0%Z <= n)%Z /\
(n < size)%Z) -> ((0%Z <= s)%Z -> ((size <= (n + s)%Z)%Z -> ((nth (asr b
s) n) = (nth b (size - 1%Z)%Z)))).
Parameter lsl: bv -> Z -> bv.
Axiom lsl_nth_high : forall (b:bv) (n:Z) (s:Z), ((0%Z <= n)%Z /\
(n < size)%Z) -> ((0%Z <= s)%Z -> ((0%Z <= (n - s)%Z)%Z -> ((nth (lsl b s)
n) = (nth b (n - s)%Z)))).
Axiom lsl_nth_low : forall (b:bv) (n:Z) (s:Z), ((0%Z <= n)%Z /\
(n < size)%Z) -> ((0%Z <= s)%Z -> (((n - s)%Z < 0%Z)%Z -> ((nth (lsl b s)
n) = false))).
Parameter to_nat_sub: bv -> Z -> Z -> Z.
Axiom to_nat_sub_zero : forall (b:bv) (j:Z) (i:Z), ((0%Z <= i)%Z /\
(i <= j)%Z) -> (((nth b j) = false) -> ((to_nat_sub b j i) = (to_nat_sub b
(j - 1%Z)%Z i))).
Axiom to_nat_sub_one : forall (b:bv) (j:Z) (i:Z), ((0%Z <= i)%Z /\
(i <= j)%Z) -> (((nth b j) = true) -> ((to_nat_sub b j
i) = ((pow2 (j - i)%Z) + (to_nat_sub b (j - 1%Z)%Z i))%Z)).
Axiom to_nat_sub_high : forall (b:bv) (j:Z) (i:Z), (j < i)%Z ->
((to_nat_sub b j i) = 0%Z).
(* YOU MAY EDIT THE CONTEXT BELOW *)
Open Scope Z_scope.
(* DO NOT EDIT BELOW *)
Theorem to_nat_of_zero2 : forall (b:bv) (i:Z) (j:Z), ((i <= j)%Z /\
(0%Z <= i)%Z) -> ((forall (k:Z), ((k <= j)%Z /\ (i < k)%Z) -> ((nth b
k) = false)) -> ((to_nat_sub b j 0%Z) = (to_nat_sub b i 0%Z))).
(* YOU MAY EDIT THE PROOF BELOW *)
intros b i j (Hij,Hipos).
apply Zlt_lower_bound_ind with (z:=i)
(P:=fun j =>
(forall k : Z, (k <= j) /\ (i < k) -> nth b k = false) ->
to_nat_sub b j 0 = to_nat_sub b i 0); auto.
intros x Hind Hxi.
assert (h:(i=x\/i < x)) by omega.
destruct h.
subst x; auto.
intros Hbits.
rewrite to_nat_sub_zero; auto with zarith.
(*
apply Hind.
omega.
intros; apply Hbits.
omega.
omega.
apply Hbits.
omega.
*)
Qed.
(* DO NOT EDIT BELOW *)
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Parameter pow2: Z -> R.
Axiom Power_0 : ((pow2 0%Z) = 1%R).
Axiom Power_s : forall (n:Z), (0%Z <= n)%Z ->
((pow2 (n + 1%Z)%Z) = (2%R * (pow2 n))%R).
Axiom Power_p : forall (n:Z), (n <= 0%Z)%Z ->
((pow2 (n - 1%Z)%Z) = ((05 / 10)%R * (pow2 n))%R).
Axiom Power_1 : ((pow2 1%Z) = 2%R).
Axiom Power_neg1 : ((pow2 (-1%Z)%Z) = (05 / 10)%R).
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
Theorem Power_sum : forall (n:Z) (m:Z),
((pow2 (n + m)%Z) = ((pow2 n) * (pow2 m))%R).
(* YOU MAY EDIT THE PROOF BELOW *)
Qed.
(* DO NOT EDIT BELOW *)