1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 set "baseuri" "cic:/matita/assembly/exadecimal/".
17 include "assembly/extra.ma".
19 inductive exadecimal : Type ≝
42 [ x0 ⇒ true | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
43 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
44 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
45 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
48 [ x0 ⇒ false | x1 ⇒ true | x2 ⇒ false | x3 ⇒ false
49 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
50 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
51 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
54 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ true | x3 ⇒ false
55 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
56 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
57 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
60 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ true
61 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
62 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
63 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
66 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
67 | x4 ⇒ true | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
68 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
69 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
72 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
73 | x4 ⇒ false | x5 ⇒ true | x6 ⇒ false | x7 ⇒ false
74 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
75 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
78 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
79 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ true | x7 ⇒ false
80 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
81 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
84 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
85 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ true
86 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
87 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
90 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
91 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
92 | x8 ⇒ true | x9 ⇒ false | xA ⇒ false | xB ⇒ false
93 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
96 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
97 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
98 | x8 ⇒ false | x9 ⇒ true | xA ⇒ false | xB ⇒ false
99 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
102 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
103 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
104 | x8 ⇒ false | x9 ⇒ false | xA ⇒ true | xB ⇒ false
105 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
108 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
109 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
110 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ true
111 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
114 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
115 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
116 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
117 | xC ⇒ true | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
120 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
121 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
122 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
123 | xC ⇒ false | xD ⇒ true | xE ⇒ false | xF ⇒ false ]
126 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
127 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
128 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
129 | xC ⇒ false | xD ⇒ false | xE ⇒ true | xF ⇒ false ]
132 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
133 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
134 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
135 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ true ]].
144 [ x0 ⇒ couple exadecimal bool x1 false
145 | x1 ⇒ couple exadecimal bool x2 false
146 | x2 ⇒ couple exadecimal bool x3 false
147 | x3 ⇒ couple exadecimal bool x4 false
148 | x4 ⇒ couple exadecimal bool x5 false
149 | x5 ⇒ couple exadecimal bool x6 false
150 | x6 ⇒ couple exadecimal bool x7 false
151 | x7 ⇒ couple exadecimal bool x8 false
152 | x8 ⇒ couple exadecimal bool x9 false
153 | x9 ⇒ couple exadecimal bool xA false
154 | xA ⇒ couple exadecimal bool xB false
155 | xB ⇒ couple exadecimal bool xC false
156 | xC ⇒ couple exadecimal bool xD false
157 | xD ⇒ couple exadecimal bool xE false
158 | xE ⇒ couple exadecimal bool xF false
159 | xF ⇒ couple exadecimal bool x0 true ]
162 [ x0 ⇒ couple exadecimal bool x2 false
163 | x1 ⇒ couple exadecimal bool x3 false
164 | x2 ⇒ couple exadecimal bool x4 false
165 | x3 ⇒ couple exadecimal bool x5 false
166 | x4 ⇒ couple exadecimal bool x6 false
167 | x5 ⇒ couple exadecimal bool x7 false
168 | x6 ⇒ couple exadecimal bool x8 false
169 | x7 ⇒ couple exadecimal bool x9 false
170 | x8 ⇒ couple exadecimal bool xA false
171 | x9 ⇒ couple exadecimal bool xB false
172 | xA ⇒ couple exadecimal bool xC false
173 | xB ⇒ couple exadecimal bool xD false
174 | xC ⇒ couple exadecimal bool xE false
175 | xD ⇒ couple exadecimal bool xF false
176 | xE ⇒ couple exadecimal bool x0 true
177 | xF ⇒ couple exadecimal bool x1 true ]
180 [ x0 ⇒ couple exadecimal bool x3 false
181 | x1 ⇒ couple exadecimal bool x4 false
182 | x2 ⇒ couple exadecimal bool x5 false
183 | x3 ⇒ couple exadecimal bool x6 false
184 | x4 ⇒ couple exadecimal bool x7 false
185 | x5 ⇒ couple exadecimal bool x8 false
186 | x6 ⇒ couple exadecimal bool x9 false
187 | x7 ⇒ couple exadecimal bool xA false
188 | x8 ⇒ couple exadecimal bool xB false
189 | x9 ⇒ couple exadecimal bool xC false
190 | xA ⇒ couple exadecimal bool xD false
191 | xB ⇒ couple exadecimal bool xE false
192 | xC ⇒ couple exadecimal bool xF false
193 | xD ⇒ couple exadecimal bool x0 true
194 | xE ⇒ couple exadecimal bool x1 true
195 | xF ⇒ couple exadecimal bool x2 true ]
198 [ x0 ⇒ couple exadecimal bool x4 false
199 | x1 ⇒ couple exadecimal bool x5 false
200 | x2 ⇒ couple exadecimal bool x6 false
201 | x3 ⇒ couple exadecimal bool x7 false
202 | x4 ⇒ couple exadecimal bool x8 false
203 | x5 ⇒ couple exadecimal bool x9 false
204 | x6 ⇒ couple exadecimal bool xA false
205 | x7 ⇒ couple exadecimal bool xB false
206 | x8 ⇒ couple exadecimal bool xC false
207 | x9 ⇒ couple exadecimal bool xD false
208 | xA ⇒ couple exadecimal bool xE false
209 | xB ⇒ couple exadecimal bool xF false
210 | xC ⇒ couple exadecimal bool x0 true
211 | xD ⇒ couple exadecimal bool x1 true
212 | xE ⇒ couple exadecimal bool x2 true
213 | xF ⇒ couple exadecimal bool x3 true ]
216 [ x0 ⇒ couple exadecimal bool x5 false
217 | x1 ⇒ couple exadecimal bool x6 false
218 | x2 ⇒ couple exadecimal bool x7 false
219 | x3 ⇒ couple exadecimal bool x8 false
220 | x4 ⇒ couple exadecimal bool x9 false
221 | x5 ⇒ couple exadecimal bool xA false
222 | x6 ⇒ couple exadecimal bool xB false
223 | x7 ⇒ couple exadecimal bool xC false
224 | x8 ⇒ couple exadecimal bool xD false
225 | x9 ⇒ couple exadecimal bool xE false
226 | xA ⇒ couple exadecimal bool xF false
227 | xB ⇒ couple exadecimal bool x0 true
228 | xC ⇒ couple exadecimal bool x1 true
229 | xD ⇒ couple exadecimal bool x2 true
230 | xE ⇒ couple exadecimal bool x3 true
231 | xF ⇒ couple exadecimal bool x4 true ]
234 [ x0 ⇒ couple exadecimal bool x6 false
235 | x1 ⇒ couple exadecimal bool x7 false
236 | x2 ⇒ couple exadecimal bool x8 false
237 | x3 ⇒ couple exadecimal bool x9 false
238 | x4 ⇒ couple exadecimal bool xA false
239 | x5 ⇒ couple exadecimal bool xB false
240 | x6 ⇒ couple exadecimal bool xC false
241 | x7 ⇒ couple exadecimal bool xD false
242 | x8 ⇒ couple exadecimal bool xE false
243 | x9 ⇒ couple exadecimal bool xF false
244 | xA ⇒ couple exadecimal bool x0 true
245 | xB ⇒ couple exadecimal bool x1 true
246 | xC ⇒ couple exadecimal bool x2 true
247 | xD ⇒ couple exadecimal bool x3 true
248 | xE ⇒ couple exadecimal bool x4 true
249 | xF ⇒ couple exadecimal bool x5 true ]
252 [ x0 ⇒ couple exadecimal bool x7 false
253 | x1 ⇒ couple exadecimal bool x8 false
254 | x2 ⇒ couple exadecimal bool x9 false
255 | x3 ⇒ couple exadecimal bool xA false
256 | x4 ⇒ couple exadecimal bool xB false
257 | x5 ⇒ couple exadecimal bool xC false
258 | x6 ⇒ couple exadecimal bool xD false
259 | x7 ⇒ couple exadecimal bool xE false
260 | x8 ⇒ couple exadecimal bool xF false
261 | x9 ⇒ couple exadecimal bool x0 true
262 | xA ⇒ couple exadecimal bool x1 true
263 | xB ⇒ couple exadecimal bool x2 true
264 | xC ⇒ couple exadecimal bool x3 true
265 | xD ⇒ couple exadecimal bool x4 true
266 | xE ⇒ couple exadecimal bool x5 true
267 | xF ⇒ couple exadecimal bool x6 true ]
270 [ x0 ⇒ couple exadecimal bool x8 false
271 | x1 ⇒ couple exadecimal bool x9 false
272 | x2 ⇒ couple exadecimal bool xA false
273 | x3 ⇒ couple exadecimal bool xB false
274 | x4 ⇒ couple exadecimal bool xC false
275 | x5 ⇒ couple exadecimal bool xD false
276 | x6 ⇒ couple exadecimal bool xE false
277 | x7 ⇒ couple exadecimal bool xF false
278 | x8 ⇒ couple exadecimal bool x0 true
279 | x9 ⇒ couple exadecimal bool x1 true
280 | xA ⇒ couple exadecimal bool x2 true
281 | xB ⇒ couple exadecimal bool x3 true
282 | xC ⇒ couple exadecimal bool x4 true
283 | xD ⇒ couple exadecimal bool x5 true
284 | xE ⇒ couple exadecimal bool x6 true
285 | xF ⇒ couple exadecimal bool x7 true ]
288 [ x0 ⇒ couple exadecimal bool x9 false
289 | x1 ⇒ couple exadecimal bool xA false
290 | x2 ⇒ couple exadecimal bool xB false
291 | x3 ⇒ couple exadecimal bool xC false
292 | x4 ⇒ couple exadecimal bool xD false
293 | x5 ⇒ couple exadecimal bool xE false
294 | x6 ⇒ couple exadecimal bool xF false
295 | x7 ⇒ couple exadecimal bool x0 true
296 | x8 ⇒ couple exadecimal bool x1 true
297 | x9 ⇒ couple exadecimal bool x2 true
298 | xA ⇒ couple exadecimal bool x3 true
299 | xB ⇒ couple exadecimal bool x4 true
300 | xC ⇒ couple exadecimal bool x5 true
301 | xD ⇒ couple exadecimal bool x6 true
302 | xE ⇒ couple exadecimal bool x7 true
303 | xF ⇒ couple exadecimal bool x8 true ]
306 [ x0 ⇒ couple exadecimal bool xA false
307 | x1 ⇒ couple exadecimal bool xB false
308 | x2 ⇒ couple exadecimal bool xC false
309 | x3 ⇒ couple exadecimal bool xD false
310 | x4 ⇒ couple exadecimal bool xE false
311 | x5 ⇒ couple exadecimal bool xF false
312 | x6 ⇒ couple exadecimal bool x0 true
313 | x7 ⇒ couple exadecimal bool x1 true
314 | x8 ⇒ couple exadecimal bool x2 true
315 | x9 ⇒ couple exadecimal bool x3 true
316 | xA ⇒ couple exadecimal bool x4 true
317 | xB ⇒ couple exadecimal bool x5 true
318 | xC ⇒ couple exadecimal bool x6 true
319 | xD ⇒ couple exadecimal bool x7 true
320 | xE ⇒ couple exadecimal bool x8 true
321 | xF ⇒ couple exadecimal bool x9 true ]
324 [ x0 ⇒ couple exadecimal bool xB false
325 | x1 ⇒ couple exadecimal bool xC false
326 | x2 ⇒ couple exadecimal bool xD false
327 | x3 ⇒ couple exadecimal bool xE false
328 | x4 ⇒ couple exadecimal bool xF false
329 | x5 ⇒ couple exadecimal bool x0 true
330 | x6 ⇒ couple exadecimal bool x1 true
331 | x7 ⇒ couple exadecimal bool x2 true
332 | x8 ⇒ couple exadecimal bool x3 true
333 | x9 ⇒ couple exadecimal bool x4 true
334 | xA ⇒ couple exadecimal bool x5 true
335 | xB ⇒ couple exadecimal bool x6 true
336 | xC ⇒ couple exadecimal bool x7 true
337 | xD ⇒ couple exadecimal bool x8 true
338 | xE ⇒ couple exadecimal bool x9 true
339 | xF ⇒ couple exadecimal bool xA true ]
342 [ x0 ⇒ couple exadecimal bool xC false
343 | x1 ⇒ couple exadecimal bool xD false
344 | x2 ⇒ couple exadecimal bool xE false
345 | x3 ⇒ couple exadecimal bool xF false
346 | x4 ⇒ couple exadecimal bool x0 true
347 | x5 ⇒ couple exadecimal bool x1 true
348 | x6 ⇒ couple exadecimal bool x2 true
349 | x7 ⇒ couple exadecimal bool x3 true
350 | x8 ⇒ couple exadecimal bool x4 true
351 | x9 ⇒ couple exadecimal bool x5 true
352 | xA ⇒ couple exadecimal bool x6 true
353 | xB ⇒ couple exadecimal bool x7 true
354 | xC ⇒ couple exadecimal bool x8 true
355 | xD ⇒ couple exadecimal bool x9 true
356 | xE ⇒ couple exadecimal bool xA true
357 | xF ⇒ couple exadecimal bool xB true ]
360 [ x0 ⇒ couple exadecimal bool xD false
361 | x1 ⇒ couple exadecimal bool xE false
362 | x2 ⇒ couple exadecimal bool xF false
363 | x3 ⇒ couple exadecimal bool x0 true
364 | x4 ⇒ couple exadecimal bool x1 true
365 | x5 ⇒ couple exadecimal bool x2 true
366 | x6 ⇒ couple exadecimal bool x3 true
367 | x7 ⇒ couple exadecimal bool x4 true
368 | x8 ⇒ couple exadecimal bool x5 true
369 | x9 ⇒ couple exadecimal bool x6 true
370 | xA ⇒ couple exadecimal bool x7 true
371 | xB ⇒ couple exadecimal bool x8 true
372 | xC ⇒ couple exadecimal bool x9 true
373 | xD ⇒ couple exadecimal bool xA true
374 | xE ⇒ couple exadecimal bool xB true
375 | xF ⇒ couple exadecimal bool xC true ]
378 [ x0 ⇒ couple exadecimal bool xE false
379 | x1 ⇒ couple exadecimal bool xF false
380 | x2 ⇒ couple exadecimal bool x0 true
381 | x3 ⇒ couple exadecimal bool x1 true
382 | x4 ⇒ couple exadecimal bool x2 true
383 | x5 ⇒ couple exadecimal bool x3 true
384 | x6 ⇒ couple exadecimal bool x4 true
385 | x7 ⇒ couple exadecimal bool x5 true
386 | x8 ⇒ couple exadecimal bool x6 true
387 | x9 ⇒ couple exadecimal bool x7 true
388 | xA ⇒ couple exadecimal bool x8 true
389 | xB ⇒ couple exadecimal bool x9 true
390 | xC ⇒ couple exadecimal bool xA true
391 | xD ⇒ couple exadecimal bool xB true
392 | xE ⇒ couple exadecimal bool xC true
393 | xF ⇒ couple exadecimal bool xD true ]
396 [ x0 ⇒ couple exadecimal bool xF false
397 | x1 ⇒ couple exadecimal bool x0 true
398 | x2 ⇒ couple exadecimal bool x1 true
399 | x3 ⇒ couple exadecimal bool x2 true
400 | x4 ⇒ couple exadecimal bool x3 true
401 | x5 ⇒ couple exadecimal bool x4 true
402 | x6 ⇒ couple exadecimal bool x5 true
403 | x7 ⇒ couple exadecimal bool x6 true
404 | x8 ⇒ couple exadecimal bool x7 true
405 | x9 ⇒ couple exadecimal bool x8 true
406 | xA ⇒ couple exadecimal bool x9 true
407 | xB ⇒ couple exadecimal bool xA true
408 | xC ⇒ couple exadecimal bool xB true
409 | xD ⇒ couple exadecimal bool xC true
410 | xE ⇒ couple exadecimal bool xD true
411 | xF ⇒ couple exadecimal bool xE true ]
414 [ x0 ⇒ couple exadecimal bool x0 true
415 | x1 ⇒ couple exadecimal bool x1 true
416 | x2 ⇒ couple exadecimal bool x2 true
417 | x3 ⇒ couple exadecimal bool x3 true
418 | x4 ⇒ couple exadecimal bool x4 true
419 | x5 ⇒ couple exadecimal bool x5 true
420 | x6 ⇒ couple exadecimal bool x6 true
421 | x7 ⇒ couple exadecimal bool x7 true
422 | x8 ⇒ couple exadecimal bool x8 true
423 | x9 ⇒ couple exadecimal bool x9 true
424 | xA ⇒ couple exadecimal bool xA true
425 | xB ⇒ couple exadecimal bool xB true
426 | xC ⇒ couple exadecimal bool xC true
427 | xD ⇒ couple exadecimal bool xD true
428 | xE ⇒ couple exadecimal bool xE true
429 | xF ⇒ couple exadecimal bool xF true ]
435 [ x0 ⇒ couple exadecimal bool x0 false
436 | x1 ⇒ couple exadecimal bool x1 false
437 | x2 ⇒ couple exadecimal bool x2 false
438 | x3 ⇒ couple exadecimal bool x3 false
439 | x4 ⇒ couple exadecimal bool x4 false
440 | x5 ⇒ couple exadecimal bool x5 false
441 | x6 ⇒ couple exadecimal bool x6 false
442 | x7 ⇒ couple exadecimal bool x7 false
443 | x8 ⇒ couple exadecimal bool x8 false
444 | x9 ⇒ couple exadecimal bool x9 false
445 | xA ⇒ couple exadecimal bool xA false
446 | xB ⇒ couple exadecimal bool xB false
447 | xC ⇒ couple exadecimal bool xC false
448 | xD ⇒ couple exadecimal bool xD false
449 | xE ⇒ couple exadecimal bool xE false
450 | xF ⇒ couple exadecimal bool xF false ]
453 [ x0 ⇒ couple exadecimal bool x1 false
454 | x1 ⇒ couple exadecimal bool x2 false
455 | x2 ⇒ couple exadecimal bool x3 false
456 | x3 ⇒ couple exadecimal bool x4 false
457 | x4 ⇒ couple exadecimal bool x5 false
458 | x5 ⇒ couple exadecimal bool x6 false
459 | x6 ⇒ couple exadecimal bool x7 false
460 | x7 ⇒ couple exadecimal bool x8 false
461 | x8 ⇒ couple exadecimal bool x9 false
462 | x9 ⇒ couple exadecimal bool xA false
463 | xA ⇒ couple exadecimal bool xB false
464 | xB ⇒ couple exadecimal bool xC false
465 | xC ⇒ couple exadecimal bool xD false
466 | xD ⇒ couple exadecimal bool xE false
467 | xE ⇒ couple exadecimal bool xF false
468 | xF ⇒ couple exadecimal bool x0 true ]
471 [ x0 ⇒ couple exadecimal bool x2 false
472 | x1 ⇒ couple exadecimal bool x3 false
473 | x2 ⇒ couple exadecimal bool x4 false
474 | x3 ⇒ couple exadecimal bool x5 false
475 | x4 ⇒ couple exadecimal bool x6 false
476 | x5 ⇒ couple exadecimal bool x7 false
477 | x6 ⇒ couple exadecimal bool x8 false
478 | x7 ⇒ couple exadecimal bool x9 false
479 | x8 ⇒ couple exadecimal bool xA false
480 | x9 ⇒ couple exadecimal bool xB false
481 | xA ⇒ couple exadecimal bool xC false
482 | xB ⇒ couple exadecimal bool xD false
483 | xC ⇒ couple exadecimal bool xE false
484 | xD ⇒ couple exadecimal bool xF false
485 | xE ⇒ couple exadecimal bool x0 true
486 | xF ⇒ couple exadecimal bool x1 true ]
489 [ x0 ⇒ couple exadecimal bool x3 false
490 | x1 ⇒ couple exadecimal bool x4 false
491 | x2 ⇒ couple exadecimal bool x5 false
492 | x3 ⇒ couple exadecimal bool x6 false
493 | x4 ⇒ couple exadecimal bool x7 false
494 | x5 ⇒ couple exadecimal bool x8 false
495 | x6 ⇒ couple exadecimal bool x9 false
496 | x7 ⇒ couple exadecimal bool xA false
497 | x8 ⇒ couple exadecimal bool xB false
498 | x9 ⇒ couple exadecimal bool xC false
499 | xA ⇒ couple exadecimal bool xD false
500 | xB ⇒ couple exadecimal bool xE false
501 | xC ⇒ couple exadecimal bool xF false
502 | xD ⇒ couple exadecimal bool x0 true
503 | xE ⇒ couple exadecimal bool x1 true
504 | xF ⇒ couple exadecimal bool x2 true ]
507 [ x0 ⇒ couple exadecimal bool x4 false
508 | x1 ⇒ couple exadecimal bool x5 false
509 | x2 ⇒ couple exadecimal bool x6 false
510 | x3 ⇒ couple exadecimal bool x7 false
511 | x4 ⇒ couple exadecimal bool x8 false
512 | x5 ⇒ couple exadecimal bool x9 false
513 | x6 ⇒ couple exadecimal bool xA false
514 | x7 ⇒ couple exadecimal bool xB false
515 | x8 ⇒ couple exadecimal bool xC false
516 | x9 ⇒ couple exadecimal bool xD false
517 | xA ⇒ couple exadecimal bool xE false
518 | xB ⇒ couple exadecimal bool xF false
519 | xC ⇒ couple exadecimal bool x0 true
520 | xD ⇒ couple exadecimal bool x1 true
521 | xE ⇒ couple exadecimal bool x2 true
522 | xF ⇒ couple exadecimal bool x3 true ]
525 [ x0 ⇒ couple exadecimal bool x5 false
526 | x1 ⇒ couple exadecimal bool x6 false
527 | x2 ⇒ couple exadecimal bool x7 false
528 | x3 ⇒ couple exadecimal bool x8 false
529 | x4 ⇒ couple exadecimal bool x9 false
530 | x5 ⇒ couple exadecimal bool xA false
531 | x6 ⇒ couple exadecimal bool xB false
532 | x7 ⇒ couple exadecimal bool xC false
533 | x8 ⇒ couple exadecimal bool xD false
534 | x9 ⇒ couple exadecimal bool xE false
535 | xA ⇒ couple exadecimal bool xF false
536 | xB ⇒ couple exadecimal bool x0 true
537 | xC ⇒ couple exadecimal bool x1 true
538 | xD ⇒ couple exadecimal bool x2 true
539 | xE ⇒ couple exadecimal bool x3 true
540 | xF ⇒ couple exadecimal bool x4 true ]
543 [ x0 ⇒ couple exadecimal bool x6 false
544 | x1 ⇒ couple exadecimal bool x7 false
545 | x2 ⇒ couple exadecimal bool x8 false
546 | x3 ⇒ couple exadecimal bool x9 false
547 | x4 ⇒ couple exadecimal bool xA false
548 | x5 ⇒ couple exadecimal bool xB false
549 | x6 ⇒ couple exadecimal bool xC false
550 | x7 ⇒ couple exadecimal bool xD false
551 | x8 ⇒ couple exadecimal bool xE false
552 | x9 ⇒ couple exadecimal bool xF false
553 | xA ⇒ couple exadecimal bool x0 true
554 | xB ⇒ couple exadecimal bool x1 true
555 | xC ⇒ couple exadecimal bool x2 true
556 | xD ⇒ couple exadecimal bool x3 true
557 | xE ⇒ couple exadecimal bool x4 true
558 | xF ⇒ couple exadecimal bool x5 true ]
561 [ x0 ⇒ couple exadecimal bool x7 false
562 | x1 ⇒ couple exadecimal bool x8 false
563 | x2 ⇒ couple exadecimal bool x9 false
564 | x3 ⇒ couple exadecimal bool xA false
565 | x4 ⇒ couple exadecimal bool xB false
566 | x5 ⇒ couple exadecimal bool xC false
567 | x6 ⇒ couple exadecimal bool xD false
568 | x7 ⇒ couple exadecimal bool xE false
569 | x8 ⇒ couple exadecimal bool xF false
570 | x9 ⇒ couple exadecimal bool x0 true
571 | xA ⇒ couple exadecimal bool x1 true
572 | xB ⇒ couple exadecimal bool x2 true
573 | xC ⇒ couple exadecimal bool x3 true
574 | xD ⇒ couple exadecimal bool x4 true
575 | xE ⇒ couple exadecimal bool x5 true
576 | xF ⇒ couple exadecimal bool x6 true ]
579 [ x0 ⇒ couple exadecimal bool x8 false
580 | x1 ⇒ couple exadecimal bool x9 false
581 | x2 ⇒ couple exadecimal bool xA false
582 | x3 ⇒ couple exadecimal bool xB false
583 | x4 ⇒ couple exadecimal bool xC false
584 | x5 ⇒ couple exadecimal bool xD false
585 | x6 ⇒ couple exadecimal bool xE false
586 | x7 ⇒ couple exadecimal bool xF false
587 | x8 ⇒ couple exadecimal bool x0 true
588 | x9 ⇒ couple exadecimal bool x1 true
589 | xA ⇒ couple exadecimal bool x2 true
590 | xB ⇒ couple exadecimal bool x3 true
591 | xC ⇒ couple exadecimal bool x4 true
592 | xD ⇒ couple exadecimal bool x5 true
593 | xE ⇒ couple exadecimal bool x6 true
594 | xF ⇒ couple exadecimal bool x7 true ]
597 [ x0 ⇒ couple exadecimal bool x9 false
598 | x1 ⇒ couple exadecimal bool xA false
599 | x2 ⇒ couple exadecimal bool xB false
600 | x3 ⇒ couple exadecimal bool xC false
601 | x4 ⇒ couple exadecimal bool xD false
602 | x5 ⇒ couple exadecimal bool xE false
603 | x6 ⇒ couple exadecimal bool xF false
604 | x7 ⇒ couple exadecimal bool x0 true
605 | x8 ⇒ couple exadecimal bool x1 true
606 | x9 ⇒ couple exadecimal bool x2 true
607 | xA ⇒ couple exadecimal bool x3 true
608 | xB ⇒ couple exadecimal bool x4 true
609 | xC ⇒ couple exadecimal bool x5 true
610 | xD ⇒ couple exadecimal bool x6 true
611 | xE ⇒ couple exadecimal bool x7 true
612 | xF ⇒ couple exadecimal bool x8 true ]
615 [ x0 ⇒ couple exadecimal bool xA false
616 | x1 ⇒ couple exadecimal bool xB false
617 | x2 ⇒ couple exadecimal bool xC false
618 | x3 ⇒ couple exadecimal bool xD false
619 | x4 ⇒ couple exadecimal bool xE false
620 | x5 ⇒ couple exadecimal bool xF false
621 | x6 ⇒ couple exadecimal bool x0 true
622 | x7 ⇒ couple exadecimal bool x1 true
623 | x8 ⇒ couple exadecimal bool x2 true
624 | x9 ⇒ couple exadecimal bool x3 true
625 | xA ⇒ couple exadecimal bool x4 true
626 | xB ⇒ couple exadecimal bool x5 true
627 | xC ⇒ couple exadecimal bool x6 true
628 | xD ⇒ couple exadecimal bool x7 true
629 | xE ⇒ couple exadecimal bool x8 true
630 | xF ⇒ couple exadecimal bool x9 true ]
633 [ x0 ⇒ couple exadecimal bool xB false
634 | x1 ⇒ couple exadecimal bool xC false
635 | x2 ⇒ couple exadecimal bool xD false
636 | x3 ⇒ couple exadecimal bool xE false
637 | x4 ⇒ couple exadecimal bool xF false
638 | x5 ⇒ couple exadecimal bool x0 true
639 | x6 ⇒ couple exadecimal bool x1 true
640 | x7 ⇒ couple exadecimal bool x2 true
641 | x8 ⇒ couple exadecimal bool x3 true
642 | x9 ⇒ couple exadecimal bool x4 true
643 | xA ⇒ couple exadecimal bool x5 true
644 | xB ⇒ couple exadecimal bool x6 true
645 | xC ⇒ couple exadecimal bool x7 true
646 | xD ⇒ couple exadecimal bool x8 true
647 | xE ⇒ couple exadecimal bool x9 true
648 | xF ⇒ couple exadecimal bool xA true ]
651 [ x0 ⇒ couple exadecimal bool xC false
652 | x1 ⇒ couple exadecimal bool xD false
653 | x2 ⇒ couple exadecimal bool xE false
654 | x3 ⇒ couple exadecimal bool xF false
655 | x4 ⇒ couple exadecimal bool x0 true
656 | x5 ⇒ couple exadecimal bool x1 true
657 | x6 ⇒ couple exadecimal bool x2 true
658 | x7 ⇒ couple exadecimal bool x3 true
659 | x8 ⇒ couple exadecimal bool x4 true
660 | x9 ⇒ couple exadecimal bool x5 true
661 | xA ⇒ couple exadecimal bool x6 true
662 | xB ⇒ couple exadecimal bool x7 true
663 | xC ⇒ couple exadecimal bool x8 true
664 | xD ⇒ couple exadecimal bool x9 true
665 | xE ⇒ couple exadecimal bool xA true
666 | xF ⇒ couple exadecimal bool xB true ]
669 [ x0 ⇒ couple exadecimal bool xD false
670 | x1 ⇒ couple exadecimal bool xE false
671 | x2 ⇒ couple exadecimal bool xF false
672 | x3 ⇒ couple exadecimal bool x0 true
673 | x4 ⇒ couple exadecimal bool x1 true
674 | x5 ⇒ couple exadecimal bool x2 true
675 | x6 ⇒ couple exadecimal bool x3 true
676 | x7 ⇒ couple exadecimal bool x4 true
677 | x8 ⇒ couple exadecimal bool x5 true
678 | x9 ⇒ couple exadecimal bool x6 true
679 | xA ⇒ couple exadecimal bool x7 true
680 | xB ⇒ couple exadecimal bool x8 true
681 | xC ⇒ couple exadecimal bool x9 true
682 | xD ⇒ couple exadecimal bool xA true
683 | xE ⇒ couple exadecimal bool xB true
684 | xF ⇒ couple exadecimal bool xC true ]
687 [ x0 ⇒ couple exadecimal bool xE false
688 | x1 ⇒ couple exadecimal bool xF false
689 | x2 ⇒ couple exadecimal bool x0 true
690 | x3 ⇒ couple exadecimal bool x1 true
691 | x4 ⇒ couple exadecimal bool x2 true
692 | x5 ⇒ couple exadecimal bool x3 true
693 | x6 ⇒ couple exadecimal bool x4 true
694 | x7 ⇒ couple exadecimal bool x5 true
695 | x8 ⇒ couple exadecimal bool x6 true
696 | x9 ⇒ couple exadecimal bool x7 true
697 | xA ⇒ couple exadecimal bool x8 true
698 | xB ⇒ couple exadecimal bool x9 true
699 | xC ⇒ couple exadecimal bool xA true
700 | xD ⇒ couple exadecimal bool xB true
701 | xE ⇒ couple exadecimal bool xC true
702 | xF ⇒ couple exadecimal bool xD true ]
705 [ x0 ⇒ couple exadecimal bool xF false
706 | x1 ⇒ couple exadecimal bool x0 true
707 | x2 ⇒ couple exadecimal bool x1 true
708 | x3 ⇒ couple exadecimal bool x2 true
709 | x4 ⇒ couple exadecimal bool x3 true
710 | x5 ⇒ couple exadecimal bool x4 true
711 | x6 ⇒ couple exadecimal bool x5 true
712 | x7 ⇒ couple exadecimal bool x6 true
713 | x8 ⇒ couple exadecimal bool x7 true
714 | x9 ⇒ couple exadecimal bool x8 true
715 | xA ⇒ couple exadecimal bool x9 true
716 | xB ⇒ couple exadecimal bool xA true
717 | xC ⇒ couple exadecimal bool xB true
718 | xD ⇒ couple exadecimal bool xC true
719 | xE ⇒ couple exadecimal bool xD true
720 | xF ⇒ couple exadecimal bool xE true ]
725 definition nat_of_exadecimal ≝
746 coercion cic:/matita/assembly/exadecimal/nat_of_exadecimal.con.
748 let rec exadecimal_of_nat b ≝
749 match b with [ O ⇒ x0 | S b ⇒
750 match b with [ O ⇒ x1 | S b ⇒
751 match b with [ O ⇒ x2 | S b ⇒
752 match b with [ O ⇒ x3 | S b ⇒
753 match b with [ O ⇒ x4 | S b ⇒
754 match b with [ O ⇒ x5 | S b ⇒
755 match b with [ O ⇒ x6 | S b ⇒
756 match b with [ O ⇒ x7 | S b ⇒
757 match b with [ O ⇒ x8 | S b ⇒
758 match b with [ O ⇒ x9 | S b ⇒
759 match b with [ O ⇒ xA | S b ⇒
760 match b with [ O ⇒ xB | S b ⇒
761 match b with [ O ⇒ xC | S b ⇒
762 match b with [ O ⇒ xD | S b ⇒
763 match b with [ O ⇒ xE | S b ⇒
764 match b with [ O ⇒ xF | S b ⇒ exadecimal_of_nat b ]]]]]]]]]]]]]]]].
766 lemma lt_nat_of_exadecimal_16: ∀b. nat_of_exadecimal b < 16.
771 |*: repeat (apply lt_to_lt_S_S)
776 lemma exadecimal_of_nat_mod:
777 ∀n.exadecimal_of_nat n = exadecimal_of_nat (n \mod 16).
779 apply (nat_elim1 n); intro;
780 cases m; [ intro; reflexivity | ];
781 cases n1; [ intro; reflexivity | ];
782 cases n2; [ intro; reflexivity | ];
783 cases n3; [ intro; reflexivity | ];
784 cases n4; [ intro; reflexivity | ];
785 cases n5; [ intro; reflexivity | ];
786 cases n6; [ intro; reflexivity | ];
787 cases n7; [ intro; reflexivity | ];
788 cases n8; [ intro; reflexivity | ];
789 cases n9; [ intro; reflexivity | ];
790 cases n10; [ intro; reflexivity | ];
791 cases n11; [ intro; reflexivity | ];
792 cases n12; [ intro; reflexivity | ];
793 cases n13; [ intro; reflexivity | ];
794 cases n14; [ intro; reflexivity | ];
795 cases n15; [ intro; reflexivity | ];
797 change in ⊢ (? ? % ?) with (exadecimal_of_nat n16);
798 change in ⊢ (? ? ? (? (? % ?))) with (16 + n16);
800 change in ⊢ (? ? ? (? (? % ?))) with (n16 \mod 16);
809 lemma nat_of_exadecimal_exadecimal_of_nat:
810 ∀n. nat_of_exadecimal (exadecimal_of_nat n) = n \mod 16.
812 rewrite > exadecimal_of_nat_mod;
813 generalize in match (lt_mod_m_m n 16 ?); [2: autobatch | ]
814 generalize in match (n \mod 16); intro;
815 cases n1; [ intro; reflexivity | ];
816 cases n2; [ intro; reflexivity | ];
817 cases n3; [ intro; reflexivity | ];
818 cases n4; [ intro; reflexivity | ];
819 cases n5; [ intro; reflexivity | ];
820 cases n6; [ intro; reflexivity | ];
821 cases n7; [ intro; reflexivity | ];
822 cases n8; [ intro; reflexivity | ];
823 cases n9; [ intro; reflexivity | ];
824 cases n10; [ intro; reflexivity | ];
825 cases n11 [ intro; reflexivity | ];
826 cases n12; [ intro; reflexivity | ];
827 cases n13; [ intro; reflexivity | ];
828 cases n14; [ intro; reflexivity | ];
829 cases n15; [ intro; reflexivity | ];
830 cases n16; [ intro; reflexivity | ];
839 lemma exadecimal_of_nat_nat_of_exadecimal:
840 ∀b.exadecimal_of_nat (nat_of_exadecimal b) = b.
848 match plusex b1 b2 c with
849 [ couple r c' ⇒ b1 + b2 + nat_of_bool c = nat_of_exadecimal r + nat_of_bool c' * 16 ].
851 elim b1; (elim b2; (elim c; normalize; reflexivity)).
874 lemma eq_eqex_S_x0_false:
875 ∀n. n < 15 → eqex x0 (exadecimal_of_nat (S n)) = false.
877 cases n 0; [ intro; simplify; reflexivity | clear n];
878 cases n1 0; [ intro; simplify; reflexivity | clear n1];
879 cases n 0; [ intro; simplify; reflexivity | clear n];
880 cases n1 0; [ intro; simplify; reflexivity | clear n1];
881 cases n 0; [ intro; simplify; reflexivity | clear n];
882 cases n1 0; [ intro; simplify; reflexivity | clear n1];
883 cases n 0; [ intro; simplify; reflexivity | clear n];
884 cases n1 0; [ intro; simplify; reflexivity | clear n1];
885 cases n 0; [ intro; simplify; reflexivity | clear n];
886 cases n1 0; [ intro; simplify; reflexivity | clear n1];
887 cases n 0; [ intro; simplify; reflexivity | clear n];
888 cases n1 0; [ intro; simplify; reflexivity | clear n1];
889 cases n 0; [ intro; simplify; reflexivity | clear n];
890 cases n1 0; [ intro; simplify; reflexivity | clear n1];
891 cases n 0; [ intro; simplify; reflexivity | clear n];
895 [ elim (not_le_Sn_O ? Hcut)
896 | do 15 (apply le_S_S_to_le);
901 lemma eqex_true_to_eq: ∀b,b'. eqex b b' = true → b=b'.
907 first [ reflexivity | destruct H ].
910 lemma eqex_false_to_not_eq: ∀b,b'. eqex b b' = false → b ≠ b'.
922 lemma xpred_S: ∀b. xpred (exadecimal_of_nat (S b)) = exadecimal_of_nat b.
924 rewrite > exadecimal_of_nat_mod;
925 rewrite > exadecimal_of_nat_mod in ⊢ (? ? ? %);