| Name | Conclusion | Link |
|---|---|---|
| natural-bits_1 | is_bits [] | link to proof |
| natural-bits_2 | ~bit_hd 0 | link to proof |
| natural-bits_3 | bit_hd 1 | link to proof |
| natural-bits_4 | bit_to_num F = 0 | link to proof |
| natural-bits_5 | bits_to_num [] = 0 | link to proof |
| natural-bits_6 | bit_tl 0 = 0 | link to proof |
| natural-bits_7 | bit_width 0 = 0 | link to proof |
| natural-bits_8 | num_to_bits 0 = [] | link to proof |
| natural-bits_9 | !n. is_bits (num_to_bits n) | link to proof |
| natural-bits_10 | ~bit_hd 2 | link to proof |
| natural-bits_11 | bit_to_num T = 1 | link to proof |
| natural-bits_12 | bit_tl 1 = 0 | link to proof |
| natural-bits_13 | !i. ~bit_nth 0 i | link to proof |
| natural-bits_14 | bit_width 1 = 1 | link to proof |
| natural-bits_15 | !b. bit_hd (bit_to_num b) <=> b | link to proof |
| natural-bits_16 | !b. bit_tl (bit_to_num b) = 0 | link to proof |
| natural-bits_17 | !n. bit_hd n <=> ODD n | link to proof |
| natural-bits_18 | !n. bits_to_num (num_to_bits n) = n | link to proof |
| natural-bits_19 | !n. bit_and 0 n = 0 | link to proof |
| natural-bits_20 | !n. bit_and n 0 = 0 | link to proof |
| natural-bits_21 | !n. bit_and n n = n | link to proof |
| natural-bits_22 | !n. bit_append [] n = n | link to proof |
| natural-bits_23 | !k. bit_bound 0 k = 0 | link to proof |
| natural-bits_24 | !n. bit_bound n 0 = 0 | link to proof |
| natural-bits_25 | !n. bit_or 0 n = n | link to proof |
| natural-bits_26 | !n. bit_or n 0 = n | link to proof |
| natural-bits_27 | !n. bit_or n n = n | link to proof |
| natural-bits_28 | !k. bit_shl 0 k = 0 | link to proof |
| natural-bits_29 | !n. bit_shl n 0 = n | link to proof |
| natural-bits_30 | !k. bit_shr 0 k = 0 | link to proof |
| natural-bits_31 | !n. bit_shr n 0 = n | link to proof |
| natural-bits_32 | !n. num_to_bitvec n 0 = [] | link to proof |
| natural-bits_33 | num_to_bits 1 = [T] | link to proof |
| natural-bits_34 | !b. bit_to_num b < 2 | link to proof |
| natural-bits_35 | !b. bit_width (bit_to_num b) = bit_to_num b | link to proof |
| natural-bits_36 | !b. bit_cons b 0 = bit_to_num b | link to proof |
| natural-bits_37 | !n. bit_nth n 0 <=> bit_hd n | link to proof |
| natural-bits_38 | !n. LENGTH (num_to_bits n) = bit_width n | link to proof |
| natural-bits_39 | !k. bits_to_num (REPLICATE F k) = 0 | link to proof |
| natural-bits_40 | !n. bit_bound n (bit_width n) = n | link to proof |
| natural-bits_41 | !n. bit_shr n (bit_width n) = 0 | link to proof |
| natural-bits_42 | !l. bits_to_num l = bit_append l 0 | link to proof |
| natural-bits_43 | !l. bit_width (bits_to_num l) <= LENGTH l | link to proof |
| natural-bits_44 | !m n. m <= bit_or m n | link to proof |
| natural-bits_45 | !m n. n <= bit_or m n | link to proof |
| natural-bits_46 | !m n. bit_and m n <= m | link to proof |
| natural-bits_47 | !m n. bit_and m n <= n | link to proof |
| natural-bits_48 | !n k. bit_bound n k <= n | link to proof |
| natural-bits_49 | !b. bit_to_num b = 0 <=> ~b | link to proof |
| natural-bits_50 | !b. bits_to_num [b] = bit_to_num b | link to proof |
| natural-bits_51 | !b. bit_to_num b = 1 <=> b | link to proof |
| natural-bits_52 | !n. ~bit_hd (2 * n) | link to proof |
| natural-bits_53 | !n. bit_tl n = bit_shr n 1 | link to proof |
| natural-bits_54 | !n. num_to_bits n = num_to_bitvec n (bit_width n) | link to proof |
| natural-bits_55 | !n. bit_hd (SUC n) <=> ~bit_hd n | link to proof |
| natural-bits_56 | !k. num_to_bitvec 0 k = REPLICATE F k | link to proof |
| natural-bits_57 | !n. bit_shr n 1 = bit_tl n | link to proof |
| natural-bits_58 | !n. bit_cons (bit_hd n) (bit_tl n) = n | link to proof |
| natural-bits_59 | !h t. bit_hd (bit_cons h t) <=> h | link to proof |
| natural-bits_60 | !h t. bit_tl (bit_cons h t) = t | link to proof |
| natural-bits_61 | !n k. LENGTH (num_to_bitvec n k) = k | link to proof |
| natural-bits_62 | !n k. bit_width (bit_bound n k) <= k | link to proof |
| natural-bits_63 | !b. bit_to_num b = (if b then 1 else 0) | link to proof |
| natural-bits_64 | !n. ?h t. n = bit_cons h t | link to proof |
| natural-bits_65 | !n. n < 2 EXP bit_width n | link to proof |
| natural-bits_66 | !n. bit_tl n = n DIV 2 | link to proof |
| natural-bits_67 | !n. bit_nth (bit_tl n) = bit_nth n o SUC | link to proof |
| natural-bits_68 | !n. bit_width n = 0 <=> n = 0 | link to proof |
| natural-bits_69 | !n. num_to_bits n = [] <=> n = 0 | link to proof |
| natural-bits_70 | !n. SUC (bit_cons F n) = bit_cons T n | link to proof |
| natural-bits_71 | !n. bit_bound n 1 = bit_to_num (bit_hd n) | link to proof |
| natural-bits_72 | !l. is_bits l <=> NULL l \/ LAST l | link to proof |
| natural-bits_73 | !l. is_bits l <=> num_to_bits (bits_to_num l) = l | link to proof |
| natural-bits_74 | !l. bits_to_num l = 0 <=> ALL (~) l | link to proof |
| natural-bits_75 | !m n. bit_and m n = bit_and n m | link to proof |
| natural-bits_76 | !m n. bit_or m n = bit_or n m | link to proof |
| natural-bits_77 | !m n. MAX m n <= bit_or m n | link to proof |
| natural-bits_78 | !m n. bit_and m n <= MIN m n | link to proof |
| natural-bits_79 | !n k. bit_bound (bit_shl n k) k = 0 | link to proof |
| natural-bits_80 | !n k. bit_shr (bit_bound n k) k = 0 | link to proof |
| natural-bits_81 | !n k. bit_shr (bit_shl n k) k = n | link to proof |
| natural-bits_82 | !b. bit_to_num b MOD 2 = bit_to_num b | link to proof |
| natural-bits_83 | !n. bit_to_num (bit_hd n) = n MOD 2 | link to proof |
| natural-bits_84 | !n. bit_cons F n = 2 * n | link to proof |
| natural-bits_85 | !n. SUC (bit_cons T n) = bit_cons F (SUC n) | link to proof |
| natural-bits_86 | !l. is_bits l <=> bit_width (bits_to_num l) = LENGTH l | link to proof |
| natural-bits_87 | !l. bits_to_num l < 2 EXP LENGTH l | link to proof |
| natural-bits_88 | !h t. bit_width (bit_cons h t) <= SUC (bit_width t) | link to proof |
| natural-bits_89 | !n i. bit_nth n i <=> bit_hd (bit_shr n i) | link to proof |
| natural-bits_90 | !n k. bit_shr n k = funpow bit_tl k n | link to proof |
| natural-bits_91 | !n i. bit_nth n i ==> i < bit_width n | link to proof |
| natural-bits_92 | !n k. bits_to_num (num_to_bitvec n k) = bit_bound n k | link to proof |
| natural-bits_93 | !n. (!i. ~bit_nth n i) <=> n = 0 | link to proof |
| natural-bits_94 | !n. (!i. ~bit_nth n i) ==> n = 0 | link to proof |
| natural-bits_95 | !l n. bit_append l n = foldr bit_cons n l | link to proof |
| natural-bits_96 | !n. bit_shl n 1 = 2 * n | link to proof |
| natural-bits_97 | !k. bit_shl 1 k = 2 EXP k | link to proof |
| natural-bits_98 | !k. bit_width (bit_shl 1 k) = k + 1 | link to proof |
| natural-bits_99 | !b1 b2. bit_to_num b1 = bit_to_num b2 <=> b1 <=> b2 | link to proof |
| natural-bits_100 | !h t. bits_to_num (CONS h t) = bit_cons h (bits_to_num t) | link to proof |
| natural-bits_101 | !n k. bit_shl n k = funpow (bit_cons F) k n | link to proof |
| natural-bits_102 | !n1 n2. n1 <= n2 ==> bit_width n1 <= bit_width n2 | link to proof |
| natural-bits_103 | !n i. bit_nth n (SUC i) <=> bit_nth (bit_tl n) i | link to proof |
| natural-bits_104 | !n k. bit_shr n (SUC k) = bit_tl (bit_shr n k) | link to proof |
| natural-bits_105 | !n k. bit_shr n (SUC k) = bit_shr (bit_tl n) k | link to proof |
| natural-bits_106 | !n k. bit_width (bit_shl n k) <= bit_width n + k | link to proof |
| natural-bits_107 | !k n. bit_shl n k = 0 <=> n = 0 | link to proof |
| natural-bits_108 | !n k. bit_bound (bit_bound n k) k = bit_bound n k | link to proof |
| natural-bits_109 | !n k. num_to_bitvec (bit_bound n k) k = num_to_bitvec n k | link to proof |
| natural-bits_110 | !k. bit_width (2 EXP k - 1) = k | link to proof |
| natural-bits_111 | !b1 b2. bit_to_num b1 < bit_to_num b2 <=> ~b1 /\ b2 | link to proof |
| natural-bits_112 | !b1 b2. bit_to_num b1 <= bit_to_num b2 <=> ~b1 \/ b2 | link to proof |
| natural-bits_113 | !b k. is_bits (REPLICATE b k) <=> k = 0 \/ b | link to proof |
| natural-bits_114 | !q n. bit_cmp q n 0 <=> q /\ n = 0 | link to proof |
| natural-bits_115 | !n k. num_to_bitvec n k = MAP (bit_nth n) (interval 0 k) | link to proof |
| natural-bits_116 | !n1 n2. bit_hd (n1 * n2) <=> bit_hd n1 /\ bit_hd n2 | link to proof |
| natural-bits_117 | !m n. bit_hd (bit_and m n) <=> bit_hd m /\ bit_hd n | link to proof |
| natural-bits_118 | !m n. bit_hd (bit_or m n) <=> bit_hd m \/ bit_hd n | link to proof |
| natural-bits_119 | !m n. bit_tl (bit_and m n) = bit_and (bit_tl m) (bit_tl n) | link to proof |
| natural-bits_120 | !m n. bit_tl (bit_or m n) = bit_or (bit_tl m) (bit_tl n) | link to proof |
| natural-bits_121 | !m n. bit_width (MAX m n) = MAX (bit_width m) (bit_width n) | link to proof |
| natural-bits_122 | !n k. bit_shl n (SUC k) = bit_cons F (bit_shl n k) | link to proof |
| natural-bits_123 | !n k. bit_shl n (SUC k) = bit_shl (bit_cons F n) k | link to proof |
| natural-bits_124 | !m n. bit_width (m * n) <= bit_width m + bit_width n | link to proof |
| natural-bits_125 | !n k. bit_bound n k = n <=> bit_width n <= k | link to proof |
| natural-bits_126 | !n k. bit_shr n k = 0 <=> bit_width n <= k | link to proof |
| natural-bits_127 | !n i. i < n ==> (?r. random_uniform n r = i) | link to proof |
| natural-bits_128 | !n. bit_cons T n = 1 + 2 * n | link to proof |
| natural-bits_129 | !q n. bit_cmp q 0 n <=> q \/ ~(n = 0) | link to proof |
| natural-bits_130 | !h t. is_bits (CONS h t) <=> (if NULL t then h else is_bits t) | link to proof |
| natural-bits_131 | !n k. bit_bound n k = n - bit_shl (bit_shr n k) k | link to proof |
| natural-bits_132 | !n k. bit_bound n k = n MOD 2 EXP k | link to proof |
| natural-bits_133 | !n k. bit_shl n k = 2 EXP k * n | link to proof |
| natural-bits_134 | !n k. bit_shr n k = n DIV 2 EXP k | link to proof |
| natural-bits_135 | !n1 n2. bit_hd (n1 + n2) <=> ~(bit_hd n1 <=> bit_hd n2) | link to proof |
| natural-bits_136 | !n1 n2. bit_tl (n1 + bit_cons F n2) = bit_tl n1 + n2 | link to proof |
| natural-bits_137 | !m n. bit_or m n + bit_and m n = m + n | link to proof |
| natural-bits_138 | !n k. bit_bound n k + bit_shl (bit_shr n k) k = n | link to proof |
| natural-bits_139 | !n. random_uniform n = (\r. let w = bit_width (n - 1) in random_uniform_loop n w r) | link to proof |
| natural-bits_140 | !k. bits_to_num (REPLICATE T k) = 2 EXP k - 1 | link to proof |
| natural-bits_141 | !h t. bit_cons h t = bit_to_num h + 2 * t | link to proof |
| natural-bits_142 | !h t. bit_cons h t = 0 <=> ~h /\ t = 0 | link to proof |
| natural-bits_143 | !h t. bit_cons h t = 1 <=> h /\ t = 0 | link to proof |
| natural-bits_144 | !n k. bit_width n <= k <=> n < 2 EXP k | link to proof |
| natural-bits_145 | !n k. bit_bound n (SUC k) = bit_cons (bit_hd n) (bit_bound (bit_tl n) k) | link to proof |
| natural-bits_146 | !n k. num_to_bitvec n (SUC k) = CONS (bit_hd n) (num_to_bitvec (bit_tl n) k) | link to proof |
| natural-bits_147 | !h t1 t2. bit_cons h t1 < bit_cons h t2 <=> t1 < t2 | link to proof |
| natural-bits_148 | !h t1 t2. bit_cons h t1 <= bit_cons h t2 <=> t1 <= t2 | link to proof |
| natural-bits_149 | !h t n. bit_append (CONS h t) n = bit_cons h (bit_append t n) | link to proof |
| natural-bits_150 | !n k i. bit_nth n (k + i) <=> bit_nth (bit_shr n k) i | link to proof |
| natural-bits_151 | !n k1 k2. bit_shl n (k1 + k2) = bit_shl (bit_shl n k1) k2 | link to proof |
| natural-bits_152 | !n k1 k2. bit_shr n (k1 + k2) = bit_shr (bit_shr n k1) k2 | link to proof |
| natural-bits_153 | !n j k. bit_bound (bit_bound n j) k = bit_bound n (MIN j k) | link to proof |
| natural-bits_154 | !k n1 n2. bit_shl (n1 * n2) k = n1 * bit_shl n2 k | link to proof |
| natural-bits_155 | !k n1 n2. bit_shl n1 k = bit_shl n2 k <=> n1 = n2 | link to proof |
| natural-bits_156 | !k n1 n2. bit_shl n1 k <= bit_shl n2 k <=> n1 <= n2 | link to proof |
| natural-bits_157 | !n1 n2 k. bit_bound (n1 + bit_shl n2 k) k = bit_bound n1 k | link to proof |
| natural-bits_158 | !m n. (!i. bit_nth m i <=> bit_nth n i) ==> m = n | link to proof |
| natural-bits_159 | !n. bit_width n = (if n = 0 then 0 else bit_width (bit_tl n) + 1) | link to proof |
| natural-bits_160 | !n. num_to_bits n = (if n = 0 then [] else CONS (bit_hd n) (num_to_bits (bit_tl n))) | link to proof |
| natural-bits_161 | !h t. ~(t = 0) ==> bit_width (bit_cons h t) = SUC (bit_width t) | link to proof |
| natural-bits_162 | !m n. bit_width (m + n) <= MAX (bit_width m) (bit_width n) + 1 | link to proof |
| natural-bits_163 | !m n. bit_or m n = 0 <=> m = 0 /\ n = 0 | link to proof |
| natural-bits_164 | !l i. bit_nth (bits_to_num l) i <=> i < LENGTH l /\ nth l i | link to proof |
| natural-bits_165 | !l k. k <= LENGTH l ==> num_to_bitvec (bits_to_num l) k = take k l | link to proof |
| natural-bits_166 | !l k. num_to_bitvec (bits_to_num l) (LENGTH l + k) = APPEND l (REPLICATE F k) | link to proof |
| natural-bits_167 | !l1 l2. bits_to_num (APPEND l1 l2) = bits_to_num l1 + bit_shl (bits_to_num l2) (LENGTH l1) | link to proof |
| natural-bits_168 | !n r. random_uniform n r = (let w = bit_width (n - 1) in random_uniform_loop n w r) | link to proof |
| natural-bits_169 | !h1 h2 t1 t2. t1 < t2 ==> bit_cons h1 t1 < bit_cons h2 t2 | link to proof |
| natural-bits_170 | !h t. bits_to_num (CONS h t) = 0 <=> ~h /\ bits_to_num t = 0 | link to proof |
| natural-bits_171 | !n k. ~(n = 0) ==> bit_width (bit_shl n k) = bit_width n + k | link to proof |
| natural-bits_172 | !n k. bit_and n (2 EXP k - 1) = bit_bound n k | link to proof |
| natural-bits_173 | !h1 h2 t. bit_cons h1 t < bit_cons h2 t <=> bit_to_num h1 < bit_to_num h2 | link to proof |
| natural-bits_174 | !h1 h2 t. bit_cons h1 t <= bit_cons h2 t <=> bit_to_num h1 <= bit_to_num h2 | link to proof |
| natural-bits_175 | !q m n. bit_cmp q m n <=> (if q then m <= n else m < n) | link to proof |
| natural-bits_176 | !m n i. bit_nth (bit_and m n) i <=> bit_nth m i /\ bit_nth n i | link to proof |
| natural-bits_177 | !n i k. bit_nth (bit_bound n k) i <=> i < k /\ bit_nth n i | link to proof |
| natural-bits_178 | !m n i. bit_nth (bit_or m n) i <=> bit_nth m i \/ bit_nth n i | link to proof |
| natural-bits_179 | !m n k. bit_bound (bit_and m n) k = bit_and (bit_bound m k) (bit_bound n k) | link to proof |
| natural-bits_180 | !m n k. bit_bound (bit_or m n) k = bit_or (bit_bound m k) (bit_bound n k) | link to proof |
| natural-bits_181 | !k n1 n2. bit_shl (n1 + n2) k = bit_shl n1 k + bit_shl n2 k | link to proof |
| natural-bits_182 | !n j k. bit_width n <= j + k ==> bit_width (bit_shr n k) <= j | link to proof |
| natural-bits_183 | !n j k. bit_bound (bit_shl n k) (j + k) = bit_shl (bit_bound n j) k | link to proof |
| natural-bits_184 | !n1 n2 k. bit_shr (n1 + bit_shl n2 k) k = bit_shr n1 k + n2 | link to proof |
| natural-bits_185 | !n j k. bit_shr (bit_bound n (j + k)) k = bit_bound (bit_shr n k) j | link to proof |
| natural-bits_186 | !n. bit_width n = (if n = 0 then 0 else log 2 n + 1) | link to proof |
| natural-bits_187 | !n k. bit_bound n (SUC k) = bit_bound n k + bit_shl (bit_to_num (bit_nth n k)) k | link to proof |
| natural-bits_188 | !l k. bit_bound (bits_to_num l) k = bits_to_num (if LENGTH l <= k then l else take k l) | link to proof |
| natural-bits_189 | !l k. bit_shr (bits_to_num l) k = (if LENGTH l <= k then 0 else bits_to_num (drop k l)) | link to proof |
| natural-bits_190 | !m n k. num_to_bitvec (bit_and m n) k = zipwith (/\) (num_to_bitvec m k) (num_to_bitvec n k) | link to proof |
| natural-bits_191 | !m n k. num_to_bitvec (bit_or m n) k = zipwith (\/) (num_to_bitvec m k) (num_to_bitvec n k) | link to proof |
| natural-bits_192 | !n i. i < n ==> (?r. random_uniform_loop n (bit_width (n - 1)) r = i) | link to proof |
| natural-bits_193 | !p. p 0 /\ (!h t. p t ==> p (bit_cons h t)) ==> (!n. p n) | link to proof |
| natural-bits_194 | !n k i. bit_nth (bit_shl n k) i <=> k <= i /\ bit_nth n (i - k) | link to proof |
| natural-bits_195 | !m n k. bit_bound (bit_bound m k * bit_bound n k) k = bit_bound (m * n) k | link to proof |
| natural-bits_196 | !m n k. bit_bound (bit_bound m k + bit_bound n k) k = bit_bound (m + n) k | link to proof |
| natural-bits_197 | !h1 h2 t1 t2. bit_cons h1 t1 = bit_cons h2 t2 <=> (h1 <=> h2) /\ t1 = t2 | link to proof |
| natural-bits_198 | !h1 h2 t1 t2. bit_and (bit_cons h1 t1) (bit_cons h2 t2) = bit_cons (h1 /\ h2) (bit_and t1 t2) | link to proof |
| natural-bits_199 | !h1 h2 t1 t2. bit_or (bit_cons h1 t1) (bit_cons h2 t2) = bit_cons (h1 \/ h2) (bit_or t1 t2) | link to proof |
| natural-bits_200 | !m n p k. m = n + bit_shl p k ==> bit_bound m k = bit_bound n k | link to proof |
| natural-bits_201 | !p. p 0 /\ (!n. ~(n = 0) /\ p (bit_tl n) ==> p n) ==> (!n. p n) | link to proof |
| natural-bits_202 | !n k. num_to_bitvec n k = (if k = 0 then [] else CONS (bit_hd n) (num_to_bitvec (bit_tl n) (k - 1))) | link to proof |
| natural-bits_203 | !m n j k. bit_width (bit_bound m k + bit_shl n k) <= j + k <=> bit_width n <= j | link to proof |
| natural-bits_204 | !m n. bit_and m n = bits_to_num (MAP (\i. bit_nth m i /\ bit_nth n i) (interval 0 (MIN (bit_width m) (bit_width n)))) | link to proof |
| natural-bits_205 | !m n. bit_or m n = bits_to_num (MAP (\i. bit_nth m i \/ bit_nth n i) (interval 0 (MAX (bit_width m) (bit_width n)))) | link to proof |
| natural-bits_206 | !l k. num_to_bitvec (bits_to_num l) k = (if LENGTH l <= k then APPEND l (REPLICATE F (k - LENGTH l)) else take k l) | link to proof |
| natural-bits_207 | !h1 h2 t1 t2. bit_cons h1 t1 < bit_cons h2 t2 <=> t1 < t2 \/ t1 = t2 /\ bit_to_num h1 < bit_to_num h2 | link to proof |
| natural-bits_208 | !h1 h2 t1 t2. bit_cons h1 t1 <= bit_cons h2 t2 <=> t1 < t2 \/ t1 = t2 /\ bit_to_num h1 <= bit_to_num h2 | link to proof |
| natural-bits_209 | !q h1 h2 t1 t2. bit_cmp q (bit_cons h1 t1) (bit_cons h2 t2) <=> bit_cmp (~h1 /\ h2 \/ ~(h1 /\ ~h2) /\ q) t1 t2 | link to proof |
| natural-bits_210 | !n w r. random_uniform_loop n w r = (let r1,r2 = split_random r in let l = random_bits w r1 in let m = bits_to_num l in if m < n then m else random_uniform_loop n w r2) | link to proof |