1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
|
or_assoc: forall A B C : Prop, (A \/ B) \/ C <-> A \/ B \/ C
and_assoc: forall A B C : Prop, (A /\ B) /\ C <-> A /\ B /\ C
eq_trans_assoc:
forall [A : Type] [x y z t : A] (e : x = y) (e' : y = z) (e'' : z = t),
eq_trans e (eq_trans e' e'') = eq_trans (eq_trans e e') e''
plus_O_n: forall n : nat, 0 + n = n
plus_n_O: forall n : nat, n = n + 0
plus_n_Sm: forall n m : nat, S (n + m) = n + S m
plus_Sn_m: forall n m : nat, S n + m = S (n + m)
mult_n_Sm: forall n m : nat, n * m + n = n * S m
f_equal2_plus:
forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 + x2 = y1 + y2
nat_rect_plus:
forall (n m : nat) {A : Type} (f : A -> A) (x : A),
nat_rect (fun _ : nat => A) x (fun _ : nat => f) (n + m) =
nat_rect (fun _ : nat => A)
(nat_rect (fun _ : nat => A) x (fun _ : nat => f) m)
(fun _ : nat => f) n
Nat.bitwise: (bool -> bool -> bool) -> nat -> nat -> nat -> nat
Number.internal_number_dec_bl:
forall x y : Number.number, Number.number_beq x y = true -> x = y
Number.internal_signed_int_dec_bl1:
forall x y : Number.signed_int, Number.signed_int_beq x y = true -> x = y
Number.internal_uint_dec_bl1:
forall x y : Number.uint, Number.uint_beq x y = true -> x = y
Hexadecimal.internal_hexadecimal_dec_bl:
forall x y : Hexadecimal.hexadecimal,
Hexadecimal.hexadecimal_beq x y = true -> x = y
Hexadecimal.internal_signed_int_dec_bl0:
forall x y : Hexadecimal.signed_int,
Hexadecimal.signed_int_beq x y = true -> x = y
Decimal.internal_decimal_dec_bl:
forall x y : Decimal.decimal, Decimal.decimal_beq x y = true -> x = y
Decimal.internal_signed_int_dec_bl:
forall x y : Decimal.signed_int, Decimal.signed_int_beq x y = true -> x = y
Byte.of_bits:
bool * (bool * (bool * (bool * (bool * (bool * (bool * bool)))))) ->
Byte.byte
Byte.to_bits_of_bits:
forall
b : bool * (bool * (bool * (bool * (bool * (bool * (bool * bool)))))),
Byte.to_bits (Byte.of_bits b) = b
Number.internal_number_dec_lb:
forall x y : Number.number, x = y -> Number.number_beq x y = true
Number.internal_uint_dec_lb1:
forall x y : Number.uint, x = y -> Number.uint_beq x y = true
Number.internal_signed_int_dec_lb1:
forall x y : Number.signed_int, x = y -> Number.signed_int_beq x y = true
Decimal.internal_signed_int_dec_lb:
forall x y : Decimal.signed_int, x = y -> Decimal.signed_int_beq x y = true
Hexadecimal.internal_hexadecimal_dec_lb:
forall x y : Hexadecimal.hexadecimal,
x = y -> Hexadecimal.hexadecimal_beq x y = true
Hexadecimal.internal_signed_int_dec_lb0:
forall x y : Hexadecimal.signed_int,
x = y -> Hexadecimal.signed_int_beq x y = true
Decimal.internal_decimal_dec_lb:
forall x y : Decimal.decimal, x = y -> Decimal.decimal_beq x y = true
Byte.to_bits:
Byte.byte ->
bool * (bool * (bool * (bool * (bool * (bool * (bool * bool))))))
Hexadecimal.internal_uint_dec_bl0:
forall x : Hexadecimal.uint,
(fun x0 : Hexadecimal.uint =>
forall y : Hexadecimal.uint, Hexadecimal.uint_beq x0 y = true -> x0 = y) x
Decimal.internal_uint_dec_lb:
forall x : Decimal.uint,
(fun x0 : Decimal.uint =>
forall y : Decimal.uint, x0 = y -> Decimal.uint_beq x0 y = true) x
Decimal.internal_uint_dec_bl:
forall x : Decimal.uint,
(fun x0 : Decimal.uint =>
forall y : Decimal.uint, Decimal.uint_beq x0 y = true -> x0 = y) x
Hexadecimal.internal_uint_dec_lb0:
forall x : Hexadecimal.uint,
(fun x0 : Hexadecimal.uint =>
forall y : Hexadecimal.uint, x0 = y -> Hexadecimal.uint_beq x0 y = true) x
andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true
andb_true_intro:
forall [b1 b2 : bool], b1 = true /\ b2 = true -> (b1 && b2)%bool = true
Byte.to_bits_of_bits:
forall
b : bool * (bool * (bool * (bool * (bool * (bool * (bool * bool)))))),
Byte.to_bits (Byte.of_bits b) = b
bool_choice:
forall [S : Set] [R1 R2 : S -> Prop],
(forall x : S, {R1 x} + {R2 x}) ->
{f : S -> bool | forall x : S, f x = true /\ R1 x \/ f x = false /\ R2 x}
Nat.two: nat
Nat.zero: nat
Nat.one: nat
Nat.succ: nat -> nat
Nat.log2: nat -> nat
Nat.sqrt: nat -> nat
Nat.square: nat -> nat
Nat.double: nat -> nat
Nat.pred: nat -> nat
Nat.ldiff: nat -> nat -> nat
Nat.tail_mul: nat -> nat -> nat
Nat.land: nat -> nat -> nat
Nat.div: nat -> nat -> nat
Nat.modulo: nat -> nat -> nat
Nat.lor: nat -> nat -> nat
Nat.lxor: nat -> nat -> nat
Nat.of_hex_uint: Hexadecimal.uint -> nat
Nat.of_uint: Decimal.uint -> nat
Nat.of_num_uint: Number.uint -> nat
length: forall [A : Type], list A -> nat
plus_n_O: forall n : nat, n = n + 0
plus_O_n: forall n : nat, 0 + n = n
plus_n_Sm: forall n m : nat, S (n + m) = n + S m
plus_Sn_m: forall n m : nat, S n + m = S (n + m)
mult_n_Sm: forall n m : nat, n * m + n = n * S m
Nat.land_comm: forall a b : nat, Nat.land a b = Nat.land b a
Nat.lor_comm: forall a b : nat, Nat.lor a b = Nat.lor b a
Nat.lxor_comm: forall a b : nat, Nat.lxor a b = Nat.lxor b a
Nat.lcm_comm: forall a b : nat, Nat.lcm a b = Nat.lcm b a
Nat.min_comm: forall n m : nat, Nat.min n m = Nat.min m n
Nat.gcd_comm: forall n m : nat, Nat.gcd n m = Nat.gcd m n
Bool.xorb_comm: forall b b' : bool, xorb b b' = xorb b' b
Nat.max_comm: forall n m : nat, Nat.max n m = Nat.max m n
Nat.mul_comm: forall n m : nat, n * m = m * n
Nat.add_comm: forall n m : nat, n + m = m + n
Bool.orb_comm: forall b1 b2 : bool, (b1 || b2)%bool = (b2 || b1)%bool
Bool.andb_comm: forall b1 b2 : bool, (b1 && b2)%bool = (b2 && b1)%bool
Nat.eqb_sym: forall x y : nat, (x =? y) = (y =? x)
Nat.bit0_eqb: forall a : nat, Nat.testbit a 0 = (a mod 2 =? 1)
Nat.Div0.div_exact: forall a b : nat, a = b * (a / b) <-> a mod b = 0
Nat.land_ones: forall a n : nat, Nat.land a (Nat.ones n) = a mod 2 ^ n
Nat.testbit_spec':
forall a n : nat, Nat.b2n (Nat.testbit a n) = (a / 2 ^ n) mod 2
Nat.pow_div_l:
forall a b c : nat, b <> 0 -> a mod b = 0 -> (a / b) ^ c = a ^ c / b ^ c
Nat.testbit_eqb: forall a n : nat, Nat.testbit a n = ((a / 2 ^ n) mod 2 =? 1)
Nat.testbit_false:
forall a n : nat, Nat.testbit a n = false <-> (a / 2 ^ n) mod 2 = 0
Nat.testbit_true:
forall a n : nat, Nat.testbit a n = true <-> (a / 2 ^ n) mod 2 = 1
Nat.bit0_eqb: forall a : nat, Nat.testbit a 0 = (a mod 2 =? 1)
Nat.Div0.div_exact: forall a b : nat, a = b * (a / b) <-> a mod b = 0
Nat.land_ones: forall a n : nat, Nat.land a (Nat.ones n) = a mod 2 ^ n
Nat.testbit_spec':
forall a n : nat, Nat.b2n (Nat.testbit a n) = (a / 2 ^ n) mod 2
Nat.pow_div_l:
forall a b c : nat, b <> 0 -> a mod b = 0 -> (a / b) ^ c = a ^ c / b ^ c
Nat.testbit_eqb: forall a n : nat, Nat.testbit a n = ((a / 2 ^ n) mod 2 =? 1)
Nat.testbit_false:
forall a n : nat, Nat.testbit a n = false <-> (a / 2 ^ n) mod 2 = 0
Nat.testbit_true:
forall a n : nat, Nat.testbit a n = true <-> (a / 2 ^ n) mod 2 = 1
|
