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/".
17 include "nat/div_and_mod.ma".
18 include "list/list.ma".
20 inductive exadecimal : Type ≝
38 record byte : Type ≝ {
48 [ x0 ⇒ true | x1 ⇒ false | 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 ⇒ true | x2 ⇒ false | 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 ⇒ true | x3 ⇒ false
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 ⇒ true
67 | x4 ⇒ false | 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 ⇒ true | x5 ⇒ false | 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 ⇒ true | x6 ⇒ false | 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 ⇒ true | x7 ⇒ false
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 ⇒ true
92 | x8 ⇒ false | 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 ⇒ true | x9 ⇒ false | 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 ⇒ true | xA ⇒ false | 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 ⇒ true | xB ⇒ false
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 ⇒ true
117 | xC ⇒ false | 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 ⇒ true | xD ⇒ false | 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 ⇒ true | xE ⇒ false | 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 ⇒ true | xF ⇒ false ]
138 [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
139 | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
140 | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
141 | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ true ]].
145 λb,b'. eqex (bh b) (bh b') ∧ eqex (bl b) (bl b').
147 inductive cartesian_product (A,B: Type) : Type ≝
148 couple: ∀a:A.∀b:B. cartesian_product A B.
157 [ x0 ⇒ couple exadecimal bool x1 false
158 | x1 ⇒ couple exadecimal bool x2 false
159 | x2 ⇒ couple exadecimal bool x3 false
160 | x3 ⇒ couple exadecimal bool x4 false
161 | x4 ⇒ couple exadecimal bool x5 false
162 | x5 ⇒ couple exadecimal bool x6 false
163 | x6 ⇒ couple exadecimal bool x7 false
164 | x7 ⇒ couple exadecimal bool x8 false
165 | x8 ⇒ couple exadecimal bool x9 false
166 | x9 ⇒ couple exadecimal bool xA false
167 | xA ⇒ couple exadecimal bool xB false
168 | xB ⇒ couple exadecimal bool xC false
169 | xC ⇒ couple exadecimal bool xD false
170 | xD ⇒ couple exadecimal bool xE false
171 | xE ⇒ couple exadecimal bool xF false
172 | xF ⇒ couple exadecimal bool x0 true ]
175 [ x0 ⇒ couple exadecimal bool x2 false
176 | x1 ⇒ couple exadecimal bool x3 false
177 | x2 ⇒ couple exadecimal bool x4 false
178 | x3 ⇒ couple exadecimal bool x5 false
179 | x4 ⇒ couple exadecimal bool x6 false
180 | x5 ⇒ couple exadecimal bool x7 false
181 | x6 ⇒ couple exadecimal bool x8 false
182 | x7 ⇒ couple exadecimal bool x9 false
183 | x8 ⇒ couple exadecimal bool xA false
184 | x9 ⇒ couple exadecimal bool xB false
185 | xA ⇒ couple exadecimal bool xC false
186 | xB ⇒ couple exadecimal bool xD false
187 | xC ⇒ couple exadecimal bool xE false
188 | xD ⇒ couple exadecimal bool xF false
189 | xE ⇒ couple exadecimal bool x0 true
190 | xF ⇒ couple exadecimal bool x1 true ]
193 [ x0 ⇒ couple exadecimal bool x3 false
194 | x1 ⇒ couple exadecimal bool x4 false
195 | x2 ⇒ couple exadecimal bool x5 false
196 | x3 ⇒ couple exadecimal bool x6 false
197 | x4 ⇒ couple exadecimal bool x7 false
198 | x5 ⇒ couple exadecimal bool x8 false
199 | x6 ⇒ couple exadecimal bool x9 false
200 | x7 ⇒ couple exadecimal bool xA false
201 | x8 ⇒ couple exadecimal bool xB false
202 | x9 ⇒ couple exadecimal bool xC false
203 | xA ⇒ couple exadecimal bool xD false
204 | xB ⇒ couple exadecimal bool xE false
205 | xC ⇒ couple exadecimal bool xF false
206 | xD ⇒ couple exadecimal bool x0 true
207 | xE ⇒ couple exadecimal bool x1 true
208 | xF ⇒ couple exadecimal bool x2 true ]
211 [ x0 ⇒ couple exadecimal bool x4 false
212 | x1 ⇒ couple exadecimal bool x5 false
213 | x2 ⇒ couple exadecimal bool x6 false
214 | x3 ⇒ couple exadecimal bool x7 false
215 | x4 ⇒ couple exadecimal bool x8 false
216 | x5 ⇒ couple exadecimal bool x9 false
217 | x6 ⇒ couple exadecimal bool xA false
218 | x7 ⇒ couple exadecimal bool xB false
219 | x8 ⇒ couple exadecimal bool xC false
220 | x9 ⇒ couple exadecimal bool xD false
221 | xA ⇒ couple exadecimal bool xE false
222 | xB ⇒ couple exadecimal bool xF false
223 | xC ⇒ couple exadecimal bool x0 true
224 | xD ⇒ couple exadecimal bool x1 true
225 | xE ⇒ couple exadecimal bool x2 true
226 | xF ⇒ couple exadecimal bool x3 true ]
229 [ x0 ⇒ couple exadecimal bool x5 false
230 | x1 ⇒ couple exadecimal bool x6 false
231 | x2 ⇒ couple exadecimal bool x7 false
232 | x3 ⇒ couple exadecimal bool x8 false
233 | x4 ⇒ couple exadecimal bool x9 false
234 | x5 ⇒ couple exadecimal bool xA false
235 | x6 ⇒ couple exadecimal bool xB false
236 | x7 ⇒ couple exadecimal bool xC false
237 | x8 ⇒ couple exadecimal bool xD false
238 | x9 ⇒ couple exadecimal bool xE false
239 | xA ⇒ couple exadecimal bool xF false
240 | xB ⇒ couple exadecimal bool x0 true
241 | xC ⇒ couple exadecimal bool x1 true
242 | xD ⇒ couple exadecimal bool x2 true
243 | xE ⇒ couple exadecimal bool x3 true
244 | xF ⇒ couple exadecimal bool x4 true ]
247 [ x0 ⇒ couple exadecimal bool x6 false
248 | x1 ⇒ couple exadecimal bool x7 false
249 | x2 ⇒ couple exadecimal bool x8 false
250 | x3 ⇒ couple exadecimal bool x9 false
251 | x4 ⇒ couple exadecimal bool xA false
252 | x5 ⇒ couple exadecimal bool xB false
253 | x6 ⇒ couple exadecimal bool xC false
254 | x7 ⇒ couple exadecimal bool xD false
255 | x8 ⇒ couple exadecimal bool xE false
256 | x9 ⇒ couple exadecimal bool xF false
257 | xA ⇒ couple exadecimal bool x0 true
258 | xB ⇒ couple exadecimal bool x1 true
259 | xC ⇒ couple exadecimal bool x2 true
260 | xD ⇒ couple exadecimal bool x3 true
261 | xE ⇒ couple exadecimal bool x4 true
262 | xF ⇒ couple exadecimal bool x5 true ]
265 [ x0 ⇒ couple exadecimal bool x7 false
266 | x1 ⇒ couple exadecimal bool x8 false
267 | x2 ⇒ couple exadecimal bool x9 false
268 | x3 ⇒ couple exadecimal bool xA false
269 | x4 ⇒ couple exadecimal bool xB false
270 | x5 ⇒ couple exadecimal bool xC false
271 | x6 ⇒ couple exadecimal bool xD false
272 | x7 ⇒ couple exadecimal bool xE false
273 | x8 ⇒ couple exadecimal bool xF false
274 | x9 ⇒ couple exadecimal bool x0 true
275 | xA ⇒ couple exadecimal bool x1 true
276 | xB ⇒ couple exadecimal bool x2 true
277 | xC ⇒ couple exadecimal bool x3 true
278 | xD ⇒ couple exadecimal bool x4 true
279 | xE ⇒ couple exadecimal bool x5 true
280 | xF ⇒ couple exadecimal bool x6 true ]
283 [ x0 ⇒ couple exadecimal bool x8 false
284 | x1 ⇒ couple exadecimal bool x9 false
285 | x2 ⇒ couple exadecimal bool xA false
286 | x3 ⇒ couple exadecimal bool xB false
287 | x4 ⇒ couple exadecimal bool xC false
288 | x5 ⇒ couple exadecimal bool xD false
289 | x6 ⇒ couple exadecimal bool xE false
290 | x7 ⇒ couple exadecimal bool xF false
291 | x8 ⇒ couple exadecimal bool x0 true
292 | x9 ⇒ couple exadecimal bool x1 true
293 | xA ⇒ couple exadecimal bool x2 true
294 | xB ⇒ couple exadecimal bool x3 true
295 | xC ⇒ couple exadecimal bool x4 true
296 | xD ⇒ couple exadecimal bool x5 true
297 | xE ⇒ couple exadecimal bool x6 true
298 | xF ⇒ couple exadecimal bool x7 true ]
301 [ x0 ⇒ couple exadecimal bool x9 false
302 | x1 ⇒ couple exadecimal bool xA false
303 | x2 ⇒ couple exadecimal bool xB false
304 | x3 ⇒ couple exadecimal bool xC false
305 | x4 ⇒ couple exadecimal bool xD false
306 | x5 ⇒ couple exadecimal bool xE false
307 | x6 ⇒ couple exadecimal bool xF false
308 | x7 ⇒ couple exadecimal bool x0 true
309 | x8 ⇒ couple exadecimal bool x1 true
310 | x9 ⇒ couple exadecimal bool x2 true
311 | xA ⇒ couple exadecimal bool x3 true
312 | xB ⇒ couple exadecimal bool x4 true
313 | xC ⇒ couple exadecimal bool x5 true
314 | xD ⇒ couple exadecimal bool x6 true
315 | xE ⇒ couple exadecimal bool x7 true
316 | xF ⇒ couple exadecimal bool x8 true ]
319 [ x0 ⇒ couple exadecimal bool xA false
320 | x1 ⇒ couple exadecimal bool xB false
321 | x2 ⇒ couple exadecimal bool xC false
322 | x3 ⇒ couple exadecimal bool xD false
323 | x4 ⇒ couple exadecimal bool xE false
324 | x5 ⇒ couple exadecimal bool xF false
325 | x6 ⇒ couple exadecimal bool x0 true
326 | x7 ⇒ couple exadecimal bool x1 true
327 | x8 ⇒ couple exadecimal bool x2 true
328 | x9 ⇒ couple exadecimal bool x3 true
329 | xA ⇒ couple exadecimal bool x4 true
330 | xB ⇒ couple exadecimal bool x5 true
331 | xC ⇒ couple exadecimal bool x6 true
332 | xD ⇒ couple exadecimal bool x7 true
333 | xE ⇒ couple exadecimal bool x8 true
334 | xF ⇒ couple exadecimal bool x9 true ]
337 [ x0 ⇒ couple exadecimal bool xB false
338 | x1 ⇒ couple exadecimal bool xC false
339 | x2 ⇒ couple exadecimal bool xD false
340 | x3 ⇒ couple exadecimal bool xE false
341 | x4 ⇒ couple exadecimal bool xF false
342 | x5 ⇒ couple exadecimal bool x0 true
343 | x6 ⇒ couple exadecimal bool x1 true
344 | x7 ⇒ couple exadecimal bool x2 true
345 | x8 ⇒ couple exadecimal bool x3 true
346 | x9 ⇒ couple exadecimal bool x4 true
347 | xA ⇒ couple exadecimal bool x5 true
348 | xB ⇒ couple exadecimal bool x6 true
349 | xC ⇒ couple exadecimal bool x7 true
350 | xD ⇒ couple exadecimal bool x8 true
351 | xE ⇒ couple exadecimal bool x9 true
352 | xF ⇒ couple exadecimal bool xA true ]
355 [ x0 ⇒ couple exadecimal bool xC false
356 | x1 ⇒ couple exadecimal bool xD false
357 | x2 ⇒ couple exadecimal bool xE false
358 | x3 ⇒ couple exadecimal bool xF false
359 | x4 ⇒ couple exadecimal bool x0 true
360 | x5 ⇒ couple exadecimal bool x1 true
361 | x6 ⇒ couple exadecimal bool x2 true
362 | x7 ⇒ couple exadecimal bool x3 true
363 | x8 ⇒ couple exadecimal bool x4 true
364 | x9 ⇒ couple exadecimal bool x5 true
365 | xA ⇒ couple exadecimal bool x6 true
366 | xB ⇒ couple exadecimal bool x7 true
367 | xC ⇒ couple exadecimal bool x8 true
368 | xD ⇒ couple exadecimal bool x9 true
369 | xE ⇒ couple exadecimal bool xA true
370 | xF ⇒ couple exadecimal bool xB true ]
373 [ x0 ⇒ couple exadecimal bool xD false
374 | x1 ⇒ couple exadecimal bool xE false
375 | x2 ⇒ couple exadecimal bool xF false
376 | x3 ⇒ couple exadecimal bool x0 true
377 | x4 ⇒ couple exadecimal bool x1 true
378 | x5 ⇒ couple exadecimal bool x2 true
379 | x6 ⇒ couple exadecimal bool x3 true
380 | x7 ⇒ couple exadecimal bool x4 true
381 | x8 ⇒ couple exadecimal bool x5 true
382 | x9 ⇒ couple exadecimal bool x6 true
383 | xA ⇒ couple exadecimal bool x7 true
384 | xB ⇒ couple exadecimal bool x8 true
385 | xC ⇒ couple exadecimal bool x9 true
386 | xD ⇒ couple exadecimal bool xA true
387 | xE ⇒ couple exadecimal bool xB true
388 | xF ⇒ couple exadecimal bool xC true ]
391 [ x0 ⇒ couple exadecimal bool xE false
392 | x1 ⇒ couple exadecimal bool xF false
393 | x2 ⇒ couple exadecimal bool x0 true
394 | x3 ⇒ couple exadecimal bool x1 true
395 | x4 ⇒ couple exadecimal bool x2 true
396 | x5 ⇒ couple exadecimal bool x3 true
397 | x6 ⇒ couple exadecimal bool x4 true
398 | x7 ⇒ couple exadecimal bool x5 true
399 | x8 ⇒ couple exadecimal bool x6 true
400 | x9 ⇒ couple exadecimal bool x7 true
401 | xA ⇒ couple exadecimal bool x8 true
402 | xB ⇒ couple exadecimal bool x9 true
403 | xC ⇒ couple exadecimal bool xA true
404 | xD ⇒ couple exadecimal bool xB true
405 | xE ⇒ couple exadecimal bool xC true
406 | xF ⇒ couple exadecimal bool xD true ]
409 [ x0 ⇒ couple exadecimal bool xF false
410 | x1 ⇒ couple exadecimal bool x0 true
411 | x2 ⇒ couple exadecimal bool x1 true
412 | x3 ⇒ couple exadecimal bool x2 true
413 | x4 ⇒ couple exadecimal bool x3 true
414 | x5 ⇒ couple exadecimal bool x4 true
415 | x6 ⇒ couple exadecimal bool x5 true
416 | x7 ⇒ couple exadecimal bool x6 true
417 | x8 ⇒ couple exadecimal bool x7 true
418 | x9 ⇒ couple exadecimal bool x8 true
419 | xA ⇒ couple exadecimal bool x9 true
420 | xB ⇒ couple exadecimal bool xA true
421 | xC ⇒ couple exadecimal bool xB true
422 | xD ⇒ couple exadecimal bool xC true
423 | xE ⇒ couple exadecimal bool xD true
424 | xF ⇒ couple exadecimal bool xE true ]
427 [ x0 ⇒ couple exadecimal bool x0 true
428 | x1 ⇒ couple exadecimal bool x1 true
429 | x2 ⇒ couple exadecimal bool x2 true
430 | x3 ⇒ couple exadecimal bool x3 true
431 | x4 ⇒ couple exadecimal bool x4 true
432 | x5 ⇒ couple exadecimal bool x5 true
433 | x6 ⇒ couple exadecimal bool x6 true
434 | x7 ⇒ couple exadecimal bool x7 true
435 | x8 ⇒ couple exadecimal bool x8 true
436 | x9 ⇒ couple exadecimal bool x9 true
437 | xA ⇒ couple exadecimal bool xA true
438 | xB ⇒ couple exadecimal bool xB true
439 | xC ⇒ couple exadecimal bool xC true
440 | xD ⇒ couple exadecimal bool xD true
441 | xE ⇒ couple exadecimal bool xE true
442 | xF ⇒ couple exadecimal bool xF true ]
448 [ x0 ⇒ couple exadecimal bool x0 false
449 | x1 ⇒ couple exadecimal bool x1 false
450 | x2 ⇒ couple exadecimal bool x2 false
451 | x3 ⇒ couple exadecimal bool x3 false
452 | x4 ⇒ couple exadecimal bool x4 false
453 | x5 ⇒ couple exadecimal bool x5 false
454 | x6 ⇒ couple exadecimal bool x6 false
455 | x7 ⇒ couple exadecimal bool x7 false
456 | x8 ⇒ couple exadecimal bool x8 false
457 | x9 ⇒ couple exadecimal bool x9 false
458 | xA ⇒ couple exadecimal bool xA false
459 | xB ⇒ couple exadecimal bool xB false
460 | xC ⇒ couple exadecimal bool xC false
461 | xD ⇒ couple exadecimal bool xD false
462 | xE ⇒ couple exadecimal bool xE false
463 | xF ⇒ couple exadecimal bool xF false ]
466 [ x0 ⇒ couple exadecimal bool x1 false
467 | x1 ⇒ couple exadecimal bool x2 false
468 | x2 ⇒ couple exadecimal bool x3 false
469 | x3 ⇒ couple exadecimal bool x4 false
470 | x4 ⇒ couple exadecimal bool x5 false
471 | x5 ⇒ couple exadecimal bool x6 false
472 | x6 ⇒ couple exadecimal bool x7 false
473 | x7 ⇒ couple exadecimal bool x8 false
474 | x8 ⇒ couple exadecimal bool x9 false
475 | x9 ⇒ couple exadecimal bool xA false
476 | xA ⇒ couple exadecimal bool xB false
477 | xB ⇒ couple exadecimal bool xC false
478 | xC ⇒ couple exadecimal bool xD false
479 | xD ⇒ couple exadecimal bool xE false
480 | xE ⇒ couple exadecimal bool xF false
481 | xF ⇒ couple exadecimal bool x0 true ]
484 [ x0 ⇒ couple exadecimal bool x2 false
485 | x1 ⇒ couple exadecimal bool x3 false
486 | x2 ⇒ couple exadecimal bool x4 false
487 | x3 ⇒ couple exadecimal bool x5 false
488 | x4 ⇒ couple exadecimal bool x6 false
489 | x5 ⇒ couple exadecimal bool x7 false
490 | x6 ⇒ couple exadecimal bool x8 false
491 | x7 ⇒ couple exadecimal bool x9 false
492 | x8 ⇒ couple exadecimal bool xA false
493 | x9 ⇒ couple exadecimal bool xB false
494 | xA ⇒ couple exadecimal bool xC false
495 | xB ⇒ couple exadecimal bool xD false
496 | xC ⇒ couple exadecimal bool xE false
497 | xD ⇒ couple exadecimal bool xF false
498 | xE ⇒ couple exadecimal bool x0 true
499 | xF ⇒ couple exadecimal bool x1 true ]
502 [ x0 ⇒ couple exadecimal bool x3 false
503 | x1 ⇒ couple exadecimal bool x4 false
504 | x2 ⇒ couple exadecimal bool x5 false
505 | x3 ⇒ couple exadecimal bool x6 false
506 | x4 ⇒ couple exadecimal bool x7 false
507 | x5 ⇒ couple exadecimal bool x8 false
508 | x6 ⇒ couple exadecimal bool x9 false
509 | x7 ⇒ couple exadecimal bool xA false
510 | x8 ⇒ couple exadecimal bool xB false
511 | x9 ⇒ couple exadecimal bool xC false
512 | xA ⇒ couple exadecimal bool xD false
513 | xB ⇒ couple exadecimal bool xE false
514 | xC ⇒ couple exadecimal bool xF false
515 | xD ⇒ couple exadecimal bool x0 true
516 | xE ⇒ couple exadecimal bool x1 true
517 | xF ⇒ couple exadecimal bool x2 true ]
520 [ x0 ⇒ couple exadecimal bool x4 false
521 | x1 ⇒ couple exadecimal bool x5 false
522 | x2 ⇒ couple exadecimal bool x6 false
523 | x3 ⇒ couple exadecimal bool x7 false
524 | x4 ⇒ couple exadecimal bool x8 false
525 | x5 ⇒ couple exadecimal bool x9 false
526 | x6 ⇒ couple exadecimal bool xA false
527 | x7 ⇒ couple exadecimal bool xB false
528 | x8 ⇒ couple exadecimal bool xC false
529 | x9 ⇒ couple exadecimal bool xD false
530 | xA ⇒ couple exadecimal bool xE false
531 | xB ⇒ couple exadecimal bool xF false
532 | xC ⇒ couple exadecimal bool x0 true
533 | xD ⇒ couple exadecimal bool x1 true
534 | xE ⇒ couple exadecimal bool x2 true
535 | xF ⇒ couple exadecimal bool x3 true ]
538 [ x0 ⇒ couple exadecimal bool x5 false
539 | x1 ⇒ couple exadecimal bool x6 false
540 | x2 ⇒ couple exadecimal bool x7 false
541 | x3 ⇒ couple exadecimal bool x8 false
542 | x4 ⇒ couple exadecimal bool x9 false
543 | x5 ⇒ couple exadecimal bool xA false
544 | x6 ⇒ couple exadecimal bool xB false
545 | x7 ⇒ couple exadecimal bool xC false
546 | x8 ⇒ couple exadecimal bool xD false
547 | x9 ⇒ couple exadecimal bool xE false
548 | xA ⇒ couple exadecimal bool xF false
549 | xB ⇒ couple exadecimal bool x0 true
550 | xC ⇒ couple exadecimal bool x1 true
551 | xD ⇒ couple exadecimal bool x2 true
552 | xE ⇒ couple exadecimal bool x3 true
553 | xF ⇒ couple exadecimal bool x4 true ]
556 [ x0 ⇒ couple exadecimal bool x6 false
557 | x1 ⇒ couple exadecimal bool x7 false
558 | x2 ⇒ couple exadecimal bool x8 false
559 | x3 ⇒ couple exadecimal bool x9 false
560 | x4 ⇒ couple exadecimal bool xA false
561 | x5 ⇒ couple exadecimal bool xB false
562 | x6 ⇒ couple exadecimal bool xC false
563 | x7 ⇒ couple exadecimal bool xD false
564 | x8 ⇒ couple exadecimal bool xE false
565 | x9 ⇒ couple exadecimal bool xF false
566 | xA ⇒ couple exadecimal bool x0 true
567 | xB ⇒ couple exadecimal bool x1 true
568 | xC ⇒ couple exadecimal bool x2 true
569 | xD ⇒ couple exadecimal bool x3 true
570 | xE ⇒ couple exadecimal bool x4 true
571 | xF ⇒ couple exadecimal bool x5 true ]
574 [ x0 ⇒ couple exadecimal bool x7 false
575 | x1 ⇒ couple exadecimal bool x8 false
576 | x2 ⇒ couple exadecimal bool x9 false
577 | x3 ⇒ couple exadecimal bool xA false
578 | x4 ⇒ couple exadecimal bool xB false
579 | x5 ⇒ couple exadecimal bool xC false
580 | x6 ⇒ couple exadecimal bool xD false
581 | x7 ⇒ couple exadecimal bool xE false
582 | x8 ⇒ couple exadecimal bool xF false
583 | x9 ⇒ couple exadecimal bool x0 true
584 | xA ⇒ couple exadecimal bool x1 true
585 | xB ⇒ couple exadecimal bool x2 true
586 | xC ⇒ couple exadecimal bool x3 true
587 | xD ⇒ couple exadecimal bool x4 true
588 | xE ⇒ couple exadecimal bool x5 true
589 | xF ⇒ couple exadecimal bool x6 true ]
592 [ x0 ⇒ couple exadecimal bool x8 false
593 | x1 ⇒ couple exadecimal bool x9 false
594 | x2 ⇒ couple exadecimal bool xA false
595 | x3 ⇒ couple exadecimal bool xB false
596 | x4 ⇒ couple exadecimal bool xC false
597 | x5 ⇒ couple exadecimal bool xD false
598 | x6 ⇒ couple exadecimal bool xE false
599 | x7 ⇒ couple exadecimal bool xF false
600 | x8 ⇒ couple exadecimal bool x0 true
601 | x9 ⇒ couple exadecimal bool x1 true
602 | xA ⇒ couple exadecimal bool x2 true
603 | xB ⇒ couple exadecimal bool x3 true
604 | xC ⇒ couple exadecimal bool x4 true
605 | xD ⇒ couple exadecimal bool x5 true
606 | xE ⇒ couple exadecimal bool x6 true
607 | xF ⇒ couple exadecimal bool x7 true ]
610 [ x0 ⇒ couple exadecimal bool x9 false
611 | x1 ⇒ couple exadecimal bool xA false
612 | x2 ⇒ couple exadecimal bool xB false
613 | x3 ⇒ couple exadecimal bool xC false
614 | x4 ⇒ couple exadecimal bool xD false
615 | x5 ⇒ couple exadecimal bool xE false
616 | x6 ⇒ couple exadecimal bool xF false
617 | x7 ⇒ couple exadecimal bool x0 true
618 | x8 ⇒ couple exadecimal bool x1 true
619 | x9 ⇒ couple exadecimal bool x2 true
620 | xA ⇒ couple exadecimal bool x3 true
621 | xB ⇒ couple exadecimal bool x4 true
622 | xC ⇒ couple exadecimal bool x5 true
623 | xD ⇒ couple exadecimal bool x6 true
624 | xE ⇒ couple exadecimal bool x7 true
625 | xF ⇒ couple exadecimal bool x8 true ]
628 [ x0 ⇒ couple exadecimal bool xA false
629 | x1 ⇒ couple exadecimal bool xB false
630 | x2 ⇒ couple exadecimal bool xC false
631 | x3 ⇒ couple exadecimal bool xD false
632 | x4 ⇒ couple exadecimal bool xE false
633 | x5 ⇒ couple exadecimal bool xF false
634 | x6 ⇒ couple exadecimal bool x0 true
635 | x7 ⇒ couple exadecimal bool x1 true
636 | x8 ⇒ couple exadecimal bool x2 true
637 | x9 ⇒ couple exadecimal bool x3 true
638 | xA ⇒ couple exadecimal bool x4 true
639 | xB ⇒ couple exadecimal bool x5 true
640 | xC ⇒ couple exadecimal bool x6 true
641 | xD ⇒ couple exadecimal bool x7 true
642 | xE ⇒ couple exadecimal bool x8 true
643 | xF ⇒ couple exadecimal bool x9 true ]
646 [ x0 ⇒ couple exadecimal bool xB false
647 | x1 ⇒ couple exadecimal bool xC false
648 | x2 ⇒ couple exadecimal bool xD false
649 | x3 ⇒ couple exadecimal bool xE false
650 | x4 ⇒ couple exadecimal bool xF false
651 | x5 ⇒ couple exadecimal bool x0 true
652 | x6 ⇒ couple exadecimal bool x1 true
653 | x7 ⇒ couple exadecimal bool x2 true
654 | x8 ⇒ couple exadecimal bool x3 true
655 | x9 ⇒ couple exadecimal bool x4 true
656 | xA ⇒ couple exadecimal bool x5 true
657 | xB ⇒ couple exadecimal bool x6 true
658 | xC ⇒ couple exadecimal bool x7 true
659 | xD ⇒ couple exadecimal bool x8 true
660 | xE ⇒ couple exadecimal bool x9 true
661 | xF ⇒ couple exadecimal bool xA true ]
664 [ x0 ⇒ couple exadecimal bool xC false
665 | x1 ⇒ couple exadecimal bool xD false
666 | x2 ⇒ couple exadecimal bool xE false
667 | x3 ⇒ couple exadecimal bool xF false
668 | x4 ⇒ couple exadecimal bool x0 true
669 | x5 ⇒ couple exadecimal bool x1 true
670 | x6 ⇒ couple exadecimal bool x2 true
671 | x7 ⇒ couple exadecimal bool x3 true
672 | x8 ⇒ couple exadecimal bool x4 true
673 | x9 ⇒ couple exadecimal bool x5 true
674 | xA ⇒ couple exadecimal bool x6 true
675 | xB ⇒ couple exadecimal bool x7 true
676 | xC ⇒ couple exadecimal bool x8 true
677 | xD ⇒ couple exadecimal bool x9 true
678 | xE ⇒ couple exadecimal bool xA true
679 | xF ⇒ couple exadecimal bool xB true ]
682 [ x0 ⇒ couple exadecimal bool xD false
683 | x1 ⇒ couple exadecimal bool xE false
684 | x2 ⇒ couple exadecimal bool xF false
685 | x3 ⇒ couple exadecimal bool x0 true
686 | x4 ⇒ couple exadecimal bool x1 true
687 | x5 ⇒ couple exadecimal bool x2 true
688 | x6 ⇒ couple exadecimal bool x3 true
689 | x7 ⇒ couple exadecimal bool x4 true
690 | x8 ⇒ couple exadecimal bool x5 true
691 | x9 ⇒ couple exadecimal bool x6 true
692 | xA ⇒ couple exadecimal bool x7 true
693 | xB ⇒ couple exadecimal bool x8 true
694 | xC ⇒ couple exadecimal bool x9 true
695 | xD ⇒ couple exadecimal bool xA true
696 | xE ⇒ couple exadecimal bool xB true
697 | xF ⇒ couple exadecimal bool xC true ]
700 [ x0 ⇒ couple exadecimal bool xE false
701 | x1 ⇒ couple exadecimal bool xF false
702 | x2 ⇒ couple exadecimal bool x0 true
703 | x3 ⇒ couple exadecimal bool x1 true
704 | x4 ⇒ couple exadecimal bool x2 true
705 | x5 ⇒ couple exadecimal bool x3 true
706 | x6 ⇒ couple exadecimal bool x4 true
707 | x7 ⇒ couple exadecimal bool x5 true
708 | x8 ⇒ couple exadecimal bool x6 true
709 | x9 ⇒ couple exadecimal bool x7 true
710 | xA ⇒ couple exadecimal bool x8 true
711 | xB ⇒ couple exadecimal bool x9 true
712 | xC ⇒ couple exadecimal bool xA true
713 | xD ⇒ couple exadecimal bool xB true
714 | xE ⇒ couple exadecimal bool xC true
715 | xF ⇒ couple exadecimal bool xD true ]
718 [ x0 ⇒ couple exadecimal bool xF false
719 | x1 ⇒ couple exadecimal bool x0 true
720 | x2 ⇒ couple exadecimal bool x1 true
721 | x3 ⇒ couple exadecimal bool x2 true
722 | x4 ⇒ couple exadecimal bool x3 true
723 | x5 ⇒ couple exadecimal bool x4 true
724 | x6 ⇒ couple exadecimal bool x5 true
725 | x7 ⇒ couple exadecimal bool x6 true
726 | x8 ⇒ couple exadecimal bool x7 true
727 | x9 ⇒ couple exadecimal bool x8 true
728 | xA ⇒ couple exadecimal bool x9 true
729 | xB ⇒ couple exadecimal bool xA true
730 | xC ⇒ couple exadecimal bool xB true
731 | xD ⇒ couple exadecimal bool xC true
732 | xE ⇒ couple exadecimal bool xD true
733 | xF ⇒ couple exadecimal bool xE true ]
738 definition plusbyte ≝
740 match plusex (bl b1) (bl b2) c with
742 match plusex (bh b1) (bh b2) c' with
743 [ couple h c'' ⇒ couple ? ? (mk_byte h l) c'' ]].
745 alias num (instance 0) = "natural number".
746 definition nat_of_exadecimal ≝
767 coercion cic:/matita/assembly/nat_of_exadecimal.con.
769 definition nat_of_byte ≝ λb:byte. 16*(bh b) + (bl b).
771 coercion cic:/matita/assembly/nat_of_byte.con.
773 let rec exadecimal_of_nat b ≝
774 match b with [ O ⇒ x0 | S b ⇒
775 match b with [ O ⇒ x1 | S b ⇒
776 match b with [ O ⇒ x2 | S b ⇒
777 match b with [ O ⇒ x3 | S b ⇒
778 match b with [ O ⇒ x4 | S b ⇒
779 match b with [ O ⇒ x5 | S b ⇒
780 match b with [ O ⇒ x6 | S b ⇒
781 match b with [ O ⇒ x7 | S b ⇒
782 match b with [ O ⇒ x8 | S b ⇒
783 match b with [ O ⇒ x9 | S b ⇒
784 match b with [ O ⇒ xA | S b ⇒
785 match b with [ O ⇒ xB | S b ⇒
786 match b with [ O ⇒ xC | S b ⇒
787 match b with [ O ⇒ xD | S b ⇒
788 match b with [ O ⇒ xE | S b ⇒
789 match b with [ O ⇒ xF | S b ⇒ exadecimal_of_nat b ]]]]]]]]]]]]]]]].
791 definition byte_of_nat ≝
792 λn. mk_byte (exadecimal_of_nat (n / 16)) (exadecimal_of_nat n).
794 lemma byte_of_nat_nat_of_byte: ∀b. byte_of_nat (nat_of_byte b) = b.
802 lemma lt_nat_of_exadecimal_16: ∀b. nat_of_exadecimal b < 16.
809 lemma lt_nat_of_byte_256: ∀b. nat_of_byte b < 256.
812 letin H ≝ (lt_nat_of_exadecimal_16 (bh b)); clearbody H;
813 letin K ≝ (lt_nat_of_exadecimal_16 (bl b)); clearbody K;
814 unfold lt in H K ⊢ %;
815 letin H' ≝ (le_S_S_to_le ? ? H); clearbody H'; clear H;
816 letin K' ≝ (le_S_S_to_le ? ? K); clearbody K'; clear K;
818 cut (16*bh b ≤ 16*15);
819 [ letin Hf ≝ (le_plus ? ? ? ? Hcut K'); clearbody Hf;
820 simplify in Hf:(? ? %);
826 lemma le_to_lt: ∀n,m. n ≤ m → n < S m.
833 lemma exadecimal_of_nat_mod:
834 ∀n.exadecimal_of_nat n = exadecimal_of_nat (n \mod 16).
838 cases n; [ reflexivity | ];
839 cases n1; [ reflexivity | ];
840 cases n2; [ reflexivity | ];
841 cases n3; [ reflexivity | ];
842 cases n4; [ reflexivity | ];
843 cases n5; [ reflexivity | ];
844 cases n6; [ reflexivity | ];
845 cases n7; [ reflexivity | ];
846 cases n8; [ reflexivity | ];
847 cases n9; [ reflexivity | ];
848 cases n10; [ reflexivity | ];
849 cases n11; [ reflexivity | ];
850 cases n12; [ reflexivity | ];
851 cases n13; [ reflexivity | ];
852 cases n14; [ reflexivity | ];
853 cases n15; [ reflexivity | ];
854 change in ⊢ (? ? ? (? (? % ?))) with (16 + n16);
855 cut ((16 + n16) \mod 16 = n16 \mod 16);
857 simplify in ⊢ (? ? % ?);
860 change with (mod_aux (16+n16) (16+n16) 15 = n16);
863 (match leb (16+n16) 15 with
865 | false ⇒ mod_aux (15+n16) ((16+n16) - 16) 15
867 cut (leb (16+n16) 15 = false);
869 change with (mod_aux (15+n16) (16+n16-16) 15 = n16);
870 cut (16+n16-16 = n16);
871 [ rewrite > Hcut1; clear Hcut1;
880 (*lemma exadecimal_of_nat_elim:
881 ∀P:exadecimal → Prop.
882 (∀m. m < 16 → P (exadecimal_of_nat m)) →
883 ∀n. P (exadecimal_of_nat n).
885 cases n; [ apply H; autobatch | ]; clear n;
886 cases n1; [ apply H; autobatch | ]; clear n1;
887 cases n; [ apply H; autobatch | ]; clear n;
888 cases n1; [ apply H; autobatch | ]; clear n1;
889 cases n; [ apply H; autobatch | ]; clear n;
890 cases n1; [ apply H; autobatch | ]; clear n1;
891 cases n; [ apply H; autobatch | ]; clear n;
892 cases n1; [ apply H; autobatch | ]; clear n1;
893 cases n; [ apply H; autobatch | ]; clear n;
894 cases n1; [ apply H; autobatch | ]; clear n1;
895 cases n; [ apply H; autobatch | ]; clear n;
896 cases n1; [ apply H; autobatch | ]; clear n1;
897 cases n; [ apply H; autobatch | ]; clear n;
898 cases n1; [ apply H; autobatch | ]; clear n1;
899 cases n; [ apply H; autobatch | ]; clear n;
900 cases n1; [ apply H; autobatch | ]; clear n1;
906 axiom nat_of_exadecimal_exadecimal_of_nat:
907 ∀n. nat_of_exadecimal (exadecimal_of_nat n) = n \mod 16.
910 apply (exadecimal_of_nat_elim (λn.;
914 elim n 0; [ reflexivity | intro ];
915 elim n1 0; [ intros; reflexivity | intros 2 ];
916 elim n2 0; [ intros; reflexivity | intros 2 ];
917 elim n3 0; [ intros; reflexivity | intros 2 ];
918 elim n4 0; [ intros; reflexivity | intros 2 ];
919 elim n5 0; [ intros; reflexivity | intros 2 ];
920 elim n6 0; [ intros; reflexivity | intros 2 ];
921 elim n7 0; [ intros; reflexivity | intros 2 ];
922 elim n8 0; [ intros; reflexivity | intros 2 ];
923 elim n9 0; [ intros; reflexivity | intros 2 ];
924 elim n10 0; [ intros; reflexivity | intros 2 ];
925 elim n11 0; [ intros; reflexivity | intros 2 ];
926 elim n12 0; [ intros; reflexivity | intros 2 ];
927 elim n13 0; [ intros; reflexivity | intros 2 ];
928 elim n14 0; [ intros; reflexivity | intros 2 ];
929 elim n15 0; [ intros; reflexivity | intros 2 ];
933 change in ⊢ (? ? % ?) with (nat_of_exadecimal (exadecimal_of_nat n16));
937 lemma nat_of_byte_byte_of_nat: ∀n. nat_of_byte (byte_of_nat n) = n \mod 256.
941 change with (16*(exadecimal_of_nat (n/16)) + exadecimal_of_nat n = n \mod 256);
942 rewrite > nat_of_exadecimal_exadecimal_of_nat in ⊢ (? ? (? (? ? %) ?) ?);
943 rewrite > nat_of_exadecimal_exadecimal_of_nat;
947 definition nat_of_bool ≝
948 λb. match b with [ true ⇒ 1 | false ⇒ 0 ].
952 match plusex b1 b2 c with
953 [ couple r c' ⇒ b1 + b2 + nat_of_bool c = nat_of_exadecimal r + nat_of_bool c' * 16 ].
964 match plusbyte b1 b2 c with
965 [ couple r c' ⇒ b1 + b2 + nat_of_bool c = nat_of_byte r + nat_of_bool c' * 256
969 generalize in match (plusex_ok (bl b1) (bl b2) c);
970 elim (plusex (bl b1) (bl b2) c);
972 generalize in match (plusex_ok (bh b1) (bh b2) t1);
973 elim (plusex (bh b1) (bh b2) t1);
975 change in ⊢ (? ? ? (? (? % ?) ?)) with (16 * t2);
977 letin K ≝ (eq_f ? ? (λy.16*y) ? ? H1); clearbody K; clear H1;
978 rewrite > distr_times_plus in K:(? ? ? %);
979 rewrite > symmetric_times in K:(? ? ? (? ? (? ? %)));
980 rewrite < associative_times in K:(? ? ? (? ? %));
981 normalize in K:(? ? ? (? ? (? % ?)));
982 rewrite > symmetric_times in K:(? ? ? (? ? %));
983 rewrite > sym_plus in ⊢ (? ? ? (? % ?));
984 rewrite > associative_plus in ⊢ (? ? ? %);
985 letin K' ≝ (eq_f ? ? (plus t) ? ? K); clearbody K'; clear K;
986 apply transitive_eq; [3: apply K' | skip | ];
988 rewrite > sym_plus in ⊢ (? ? (? (? ? %) ?) ?);
989 rewrite > associative_plus in ⊢ (? ? (? % ?) ?);
990 rewrite > associative_plus in ⊢ (? ? % ?);
991 rewrite > associative_plus in ⊢ (? ? (? ? %) ?);
992 rewrite > associative_plus in ⊢ (? ? (? ? (? ? %)) ?);
993 rewrite > sym_plus in ⊢ (? ? (? ? (? ? (? ? %))) ?);
994 rewrite < associative_plus in ⊢ (? ? (? ? (? ? %)) ?);
995 rewrite < associative_plus in ⊢ (? ? (? ? %) ?);
996 rewrite < associative_plus in ⊢ (? ? (? ? (? % ?)) ?);
997 rewrite > H; clear H;
998 autobatch paramodulation.
1002 lemma sign_ok: ∀ n:nat. nat_of_byte (byte_of_nat n) = n \mod 256.
1003 intros; elim n; [ reflexivity | unfold byte_of_nat.
1007 definition addr ≝ nat.
1031 match eqex (bl b) x0 with
1032 [ true ⇒ mk_byte (xpred (bh b)) (xpred (bl b))
1033 | false ⇒ mk_byte (bh b) (xpred (bl b))
1036 (* Way too slow and subsumed by previous theorem
1039 match eqbyte b (mk_byte x0 x0) with
1040 [ true ⇒ nat_of_byte (bpred b) = mk_byte xF xF
1041 | false ⇒ nat_of_byte (bpred b) = pred (nat_of_byte b)].
1050 definition addr_of_byte : byte → addr ≝ λb. nat_of_byte b.
1052 coercion cic:/matita/assembly/addr_of_byte.con.
1054 inductive opcode: Type ≝
1055 ADDd: opcode (* 3 clock, 171 *)
1056 | BEQ: opcode (* 3, 55 *)
1057 | BRA: opcode (* 3, 48 *)
1058 | DECd: opcode (* 5, 58 *)
1059 | LDAi: opcode (* 2, 166 *)
1060 | LDAd: opcode (* 3, 182 *)
1061 | STAd: opcode. (* 3, 183 *)
1063 let rec cycles_of_opcode op : nat ≝
1074 definition opcodemap ≝
1075 [ couple ? ? ADDd (mk_byte xA xB);
1076 couple ? ? BEQ (mk_byte x3 x7);
1077 couple ? ? BRA (mk_byte x3 x0);
1078 couple ? ? DECd (mk_byte x3 xA);
1079 couple ? ? LDAi (mk_byte xA x6);
1080 couple ? ? LDAd (mk_byte xB x6);
1081 couple ? ? STAd (mk_byte xB x7) ].
1083 definition opcode_of_byte ≝
1091 match eqbyte n b with
1098 definition magic_of_opcode ≝
1109 definition opcodeeqb ≝
1110 λop1,op2. eqb (magic_of_opcode op1) (magic_of_opcode op2).
1112 definition byte_of_opcode : opcode → byte ≝
1116 [ nil ⇒ mk_byte x0 x0
1120 match opcodeeqb op op' with
1127 record status : Type ≝ {
1138 λf: addr → byte.λa.λv.λx.
1143 lemma update_update_a_a:
1145 update (update s a v1) a v2 b = update s a v2 b.
1153 lemma update_update_a_b:
1156 update (update s a1 v1) a2 v2 b = update (update s a2 v2) a1 v1 b.
1160 apply (bool_elim ? (eqb b a1)); intros;
1161 apply (bool_elim ? (eqb b a2)); intros;
1164 rewrite < (eqb_true_to_eq ? ? H1);
1165 apply eqb_true_to_eq;
1171 definition mmod16 ≝ λn. nat_of_byte (byte_of_nat n).
1174 λs:status. match s with [ mk_status acc pc spc zf cf mem clk ⇒
1175 let opc ≝ opcode_of_byte (mem pc) in
1176 let op1 ≝ mem (S pc) in
1177 let clk' ≝ cycles_of_opcode opc in
1178 match eqb (S clk) clk' with
1182 let res ≝ plusbyte acc (mem op1) false in (* verify carrier! *)
1183 let acc' ≝ match res with [ couple acc' _ ⇒ acc' ] in
1184 let c' ≝ match res with [ couple _ c' ⇒ c'] in
1185 mk_status acc' (2 + pc) spc
1186 (eqbyte (mk_byte x0 x0) acc') c' mem 0 (* verify carrier! *)
1191 [ true ⇒ mmod16 (2 + op1 + pc) (*\mod 256*) (* signed!!! *)
1192 (* FIXME: can't work - address truncated to 8 bits *)
1202 acc (mmod16 (2 + op1 + pc) (*\mod 256*)) (* signed!!! *)
1203 (* FIXME: same as above *)
1210 let x ≝ bpred (mem op1) in (* signed!!! *)
1211 let mem' ≝ update mem op1 x in
1212 mk_status acc (2 + pc) spc
1213 (eqbyte (mk_byte x0 x0) x) cf mem' 0 (* check zb!!! *)
1215 mk_status op1 (2 + pc) spc (eqbyte (mk_byte x0 x0) op1) cf mem 0
1218 mk_status x (2 + pc) spc (eqbyte (mk_byte x0 x0) x) cf mem 0
1220 mk_status acc (2 + pc) spc zf cf
1221 (update mem op1 acc) 0
1225 acc pc spc zf cf mem (S clk)
1228 let rec execute s n on n ≝
1231 | S n' ⇒ execute (tick s) n'
1235 ∀s,n1,n2. execute s (n1 + n2) = execute (execute s n1) n2.
1237 generalize in match s; clear s;
1245 notation "hvbox(# break a)"
1246 non associative with precedence 80
1247 for @{ 'byte_of_opcode $a }.
1248 interpretation "byte_of_opcode" 'byte_of_opcode a =
1249 (cic:/matita/assembly/byte_of_opcode.con a).
1251 definition mult_source : list byte ≝
1252 [#LDAi; mk_byte x0 x0; (* A := 0 *)
1253 #STAd; mk_byte x2 x0; (* Z := A *)
1254 #LDAd; mk_byte x1 xF; (* (l1) A := Y *)
1255 #BEQ; mk_byte x0 xA; (* if A == 0 then goto l2 *)
1256 #LDAd; mk_byte x2 x0; (* A := Z *)
1257 #DECd; mk_byte x1 xF; (* Y := Y - 1 *)
1258 #ADDd; mk_byte x1 xE; (* A += X *)
1259 #STAd; mk_byte x2 x0; (* Z := A *)
1260 #BRA; mk_byte xF x2; (* goto l1 *)
1261 #LDAd; mk_byte x2 x0].(* (l2) *)
1263 definition mult_memory ≝
1266 [ true ⇒ nth ? mult_source (mk_byte x0 x0) a
1274 definition mult_status ≝
1276 mk_status (mk_byte x0 x0) 0 0 false false (mult_memory x y) 0.
1279 ∀b. plusbyte (mk_byte x0 x0) b false = couple ? ? b false.
1287 definition plusbytenc ≝
1289 match plusbyte x y false with
1290 [couple res _ ⇒ res].
1292 definition plusbytec ≝
1294 match plusbyte x y false with
1297 lemma plusbytenc_O_x:
1298 ∀x. plusbytenc (mk_byte x0 x0) x = x.
1301 rewrite > plusbyte_O_x;
1305 (*axiom mod_plus: ∀a,b,m. (a + b) \mod m = a \mod m + b \mod m.*)
1306 axiom mod_plus: \forall a1,a2,b1,b2,m.
1307 a1 \mod m = b1 \mod m \to
1308 a2 \mod m = b2 \mod m \to
1309 (a1 + a2) \mod m = (b1 + b2) \mod m.
1311 axiom eq_mod_times_n_m_m_O: ∀n,m. O < m → n * m \mod m = O.
1313 axiom eq_nat_of_byte_mod: ∀b. nat_of_byte b = nat_of_byte b \mod 256.
1315 theorem plusbytenc_ok:
1316 ∀b1,b2:byte. nat_of_byte (plusbytenc b1 b2) = (b1 + b2) \mod 256.
1319 generalize in match (plusbyte_ok b1 b2 false);
1320 elim (plusbyte b1 b2 false);
1322 change with (nat_of_byte t = (b1 + b2) \mod 256);
1323 rewrite < plus_n_O in H;
1324 rewrite > H; clear H;
1325 letin K ≝ (eq_nat_of_byte_mod t); clearbody K;
1326 rewrite > K in ⊢ (? ? % ?);
1327 letin K' ≝ (eq_mod_times_n_m_m_O (nat_of_bool t1) 256 ?); clearbody K';
1329 | cut (O = O \mod 256);
1330 [ rewrite > Hcut in K':(? ? ? %);
1331 rewrite > K in K:(? ? % ?);
1332 rewrite > (mod_plus ? ? ? ? ? K K') in ⊢ (? ? ? %);
1333 rewrite < plus_n_O;reflexivity
1334 |simplify;reflexivity]]
1339 let s ≝ execute (mult_status (mk_byte x0 x0) (mk_byte x0 x0)) i in
1340 pc s = 20 ∧ mem s 32 = byte_of_nat 0.
1348 let x ≝ mk_byte x0 x0 in
1349 let y ≝ mk_byte x0 x2 in
1350 let i ≝ 14 + 23 * nat_of_byte y in
1351 let s ≝ execute (mult_status x y) i in
1352 pc s = 20 ∧ mem s 32 = plusbytenc x x.
1360 let y ≝ mk_byte x0 x1 in
1361 let i ≝ 14 + 23 * nat_of_byte y in
1362 let s ≝ execute (mult_status x y) i in
1363 pc s = 20 ∧ mem s 32 = x.
1367 | change in ⊢ (? ? % ?) with (plusbytenc (mk_byte x0 x0) x);
1368 rewrite > plusbytenc_O_x;
1375 let y ≝ mk_byte x0 x2 in
1376 let i ≝ 14 + 23 * nat_of_byte y in
1377 let s ≝ execute (mult_status x y) i in
1378 pc s = 20 ∧ mem s 32 = plusbytenc x x.
1382 | change in ⊢ (? ? % ?) with
1383 (plusbytenc (plusbytenc (mk_byte x0 x0) x) x);
1384 rewrite > plusbytenc_O_x;
1389 theorem lt_trans: ∀x,y,z. x < y → y < z → x < z.
1402 (∀a. mem s a = mem s' a) →
1406 lemma eq_eqex_S_x0_false:
1407 ∀n. n < 15 → eqex x0 (exadecimal_of_nat (S n)) = false.
1409 cases n 0; [ intro; simplify; reflexivity | clear n];
1410 cases n1 0; [ intro; simplify; reflexivity | clear n1];
1411 cases n 0; [ intro; simplify; reflexivity | clear n];
1412 cases n1 0; [ intro; simplify; reflexivity | clear n1];
1413 cases n 0; [ intro; simplify; reflexivity | clear n];
1414 cases n1 0; [ intro; simplify; reflexivity | clear n1];
1415 cases n 0; [ intro; simplify; reflexivity | clear n];
1416 cases n1 0; [ intro; simplify; reflexivity | clear n1];
1417 cases n 0; [ intro; simplify; reflexivity | clear n];
1418 cases n1 0; [ intro; simplify; reflexivity | clear n1];
1419 cases n 0; [ intro; simplify; reflexivity | clear n];
1420 cases n1 0; [ intro; simplify; reflexivity | clear n1];
1421 cases n 0; [ intro; simplify; reflexivity | clear n];
1422 cases n1 0; [ intro; simplify; reflexivity | clear n1];
1423 cases n 0; [ intro; simplify; reflexivity | clear n];
1427 [ elim (not_le_Sn_O ? Hcut)
1428 | do 15 (apply le_S_S_to_le);
1433 lemma leq_m_n_to_eq_div_n_m_S: ∀n,m:nat. 0 < m → m ≤ n → ∃z. n/m = S z.
1436 apply (ex_intro ? ? (div_aux (pred n) (n-m) (pred m)));
1441 clear Hcut; clear H2; clear H; (*clear m;*)
1443 unfold in ⊢ (? ? % ?);
1445 [ elim Hcut; clear Hcut;
1447 rewrite > H; clear m;
1448 change in ⊢ (? ? % ?) with
1449 (match leb (S a1) a with
1451 | false ⇒ S (div_aux a1 ((S a1) - S a) a)]);
1453 [ apply (leb_elim (S a1) a);
1463 | elim H1; autobatch
1469 lemma eq_eqbyte_x0_x0_byte_of_nat_S_false:
1470 ∀b. b < 255 → eqbyte (mk_byte x0 x0) (byte_of_nat (S b)) = false.
1473 cut (b < 15 ∨ b ≥ 15);
1476 change in ⊢ (? ? (? ? %) ?) with (eqex x0 (exadecimal_of_nat (S b)));
1477 rewrite > eq_eqex_S_x0_false;
1478 [ elim (eqex (bh (mk_byte x0 x0))
1479 (bh (mk_byte (exadecimal_of_nat (S b/16)) (exadecimal_of_nat (S b)))));simplify;
1481 alias id "andb_sym" = "cic:/matita/nat/propr_div_mod_lt_le_totient1_aux/andb_sym.con".
1488 change in ⊢ (? ? (? % ?) ?) with (eqex x0 (exadecimal_of_nat (S b/16)));
1489 letin K ≝ (leq_m_n_to_eq_div_n_m_S (S b) 16 ? ?);
1497 rewrite > eq_eqex_S_x0_false;
1502 clear H2; clear a; clear H1; clear Hcut;
1503 elim daemon (* trivial arithmetic property over <= and div *)
1511 lemma eq_bpred_S_a_a:
1512 ∀a. a < 255 → bpred (byte_of_nat (S a)) = byte_of_nat a.
1516 cut (a \mod 16 = 15 ∨ a \mod 16 < 15);
1525 lemma plusbyteenc_S:
1526 ∀x:byte.∀n.plusbytenc (byte_of_nat (x*n)) x = byte_of_nat (x * S n).
1528 rewrite < byte_of_nat_nat_of_byte;
1529 rewrite > (plusbytenc_ok (byte_of_nat (x*n)) x);
1541 lemma eq_plusbytec_x0_x0_x_false:
1542 ∀x.plusbytec (mk_byte x0 x0) x = false.
1550 lemma loop_invariant':
1551 ∀x,y:byte.∀j:nat. j ≤ y →
1552 execute (mult_status x y) (5 + 23*j)
1554 mk_status (byte_of_nat (x * j)) 4 0 (eqbyte (mk_byte x0 x0) (byte_of_nat (x*j)))
1555 (plusbytec (byte_of_nat (x*pred j)) x)
1556 (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (y - j))) 32
1557 (byte_of_nat (x * j)))
1561 [ do 2 (rewrite < times_n_O);
1563 [1,2,3,4,7: normalize; reflexivity
1564 | rewrite > eq_plusbytec_x0_x0_x_false;
1570 | cut (5 + 23 * S n = 5 + 23 * n + 23);
1571 [ letin K ≝ (breakpoint (mult_status x y) (5 + 23 * n) 23); clearbody K;
1572 letin H' ≝ (H ?); clearbody H'; clear H;
1574 | letin xxx ≝ (eq_f ? ? (λz. execute (mult_status x y) z) ? ? Hcut); clearbody xxx;
1578 apply (transitive_eq ? ? ? ? K);
1582 cut (∃z.y-n=S z ∧ z < 255);
1583 [ elim Hcut; clear Hcut;
1586 (* instruction LDAd *)
1589 (mk_status (byte_of_nat (x*n)) 4 O
1590 (eqbyte (mk_byte x0 x0) (byte_of_nat (x*n)))
1591 (plusbytec (byte_of_nat (x*pred n)) x)
1592 (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (S a))) 32
1593 (byte_of_nat (x*n))) O)
1595 normalize in K:(? ? (? ? %) ?);
1596 apply transitive_eq; [2: apply K | skip | ]; clear K;
1597 whd in ⊢ (? ? (? % ?) ?);
1598 normalize in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
1599 change in ⊢ (? ? (? (? % ? ? ? ? ? ?) ?) ?)
1600 with (byte_of_nat (S a));
1601 change in ⊢ (? ? (? (? ? ? ? (? ? %) ? ? ?) ?) ?) with
1602 (byte_of_nat (S a));
1603 (* instruction BEQ *)
1606 (mk_status (byte_of_nat (S a)) 6 O
1607 (eqbyte (mk_byte x0 x0) (byte_of_nat (S a)))
1608 (plusbytec (byte_of_nat (x*pred n)) x)
1609 (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (S a))) 32
1610 (byte_of_nat (x*n))) O)
1612 normalize in K:(? ? (? ? %) ?);
1613 apply transitive_eq; [2: apply K | skip | ]; clear K;
1614 whd in ⊢ (? ? (? % ?) ?);
1615 letin K ≝ (eq_eqbyte_x0_x0_byte_of_nat_S_false ? H3); clearbody K;
1616 rewrite > K; clear K;
1617 simplify in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
1618 (* instruction LDAd *)
1621 (mk_status (byte_of_nat (S a)) 8 O
1622 (eqbyte (mk_byte x0 x0) (byte_of_nat (S a)))
1623 (plusbytec (byte_of_nat (x*pred n)) x)
1624 (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (S a))) 32
1625 (byte_of_nat (x*n))) O)
1627 normalize in K:(? ? (? ? %) ?);
1628 apply transitive_eq; [2: apply K | skip | ]; clear K;
1629 whd in ⊢ (? ? (? % ?) ?);
1630 change in ⊢ (? ? (? (? % ? ? ? ? ? ?) ?) ?) with (byte_of_nat (x*n));
1631 normalize in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
1632 change in ⊢ (? ? (? (? ? ? ? % ? ? ?) ?) ?) with (eqbyte (mk_byte x0 x0) (byte_of_nat (x*n)));
1633 (* instruction DECd *)
1636 (mk_status (byte_of_nat (x*n)) 10 O
1637 (eqbyte (mk_byte x0 x0) (byte_of_nat (x*n)))
1638 (plusbytec (byte_of_nat (x*pred n)) x)
1639 (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (S a))) 32
1640 (byte_of_nat (x*n))) O)
1642 normalize in K:(? ? (? ? %) ?);
1643 apply transitive_eq; [2: apply K | skip | ]; clear K;
1644 whd in ⊢ (? ? (? % ?) ?);
1645 change in ⊢ (? ? (? (? ? ? ? (? ? %) ? ? ?) ?) ?) with (bpred (byte_of_nat (S a)));
1646 rewrite > (eq_bpred_S_a_a ? H3);
1647 normalize in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
1648 normalize in ⊢ (? ? (? (? ? ? ? ? ? (? ? % ?) ?) ?) ?);
1650 [2: elim daemon | ];
1651 rewrite < Hcut; clear Hcut; clear H3; clear H2; clear a;
1652 (* instruction ADDd *)
1655 (mk_status (byte_of_nat (x*n)) 12
1656 O (eqbyte (mk_byte x0 x0) (byte_of_nat (y-S n)))
1657 (plusbytec (byte_of_nat (x*pred n)) x)
1659 (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (S (y-S n))))
1660 32 (byte_of_nat (x*n))) 31
1661 (byte_of_nat (y-S n))) O)
1663 normalize in K:(? ? (? ? %) ?);
1664 apply transitive_eq; [2: apply K | skip | ]; clear K;
1665 whd in ⊢ (? ? (? % ?) ?);
1666 change in ⊢ (? ? (? (? % ? ? ? ? ? ?) ?) ?) with
1667 (plusbytenc (byte_of_nat (x*n)) x);
1668 change in ⊢ (? ? (? (? ? ? ? (? ? %) ? ? ?) ?) ?) with
1669 (plusbytenc (byte_of_nat (x*n)) x);
1670 normalize in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
1671 change in ⊢ (? ? (? (? ? ? ? ? % ? ?) ?) ?)
1672 with (plusbytec (byte_of_nat (x*n)) x);
1673 rewrite > plusbyteenc_S;
1674 (* instruction STAd *)
1677 (mk_status (byte_of_nat (x*S n)) 14 O
1678 (eqbyte (mk_byte x0 x0) (byte_of_nat (x*S n)))
1679 (plusbytec (byte_of_nat (x*n)) x)
1681 (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (S (y-S n))))
1682 32 (byte_of_nat (x*n))) 31
1683 (byte_of_nat (y-S n))) O)
1685 normalize in K:(? ? (? ? %) ?);
1686 apply transitive_eq; [2: apply K | skip | ]; clear K;
1687 whd in ⊢ (? ? (? % ?) ?);
1688 normalize in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
1689 (* instruction BRA *)
1691 normalize in ⊢ (? ? (? ? % ? ? ? ? ?) ?);
1694 [1,2,3,4,7: normalize; reflexivity
1695 | change with (plusbytec (byte_of_nat (x*n)) x =
1696 plusbytec (byte_of_nat (x*n)) x);
1704 [ rewrite < (minus_S_S y n);
1706 | letin K ≝ (lt_nat_of_byte_256 y); clearbody K;
1707 letin K' ≝ (lt_minus_m y (S n) ? ?); clearbody K';
1713 | rewrite > associative_plus;
1714 autobatch paramodulation
1721 let i ≝ 14 + 23 * y in
1722 execute (mult_status x y) i =
1723 mk_status (byte_of_nat (x*y)) 20 0
1724 (eqbyte (mk_byte x0 x0) (byte_of_nat (x*y)))
1725 (plusbytec (byte_of_nat (x*pred y)) x)
1727 (update (mult_memory x y) 31 (mk_byte x0 x0))
1728 32 (byte_of_nat (x*y)))
1731 cut (14 + 23 * y = 5 + 23*y + 9);
1732 [2: autobatch paramodulation;
1733 | rewrite > Hcut; (* clear Hcut; *)
1734 rewrite > (breakpoint (mult_status x y) (5 + 23*y) 9);
1735 rewrite > loop_invariant';
1737 | rewrite < minus_n_n;
1739 [1,2,3,4,5,7: normalize; reflexivity