]> matita.cs.unibo.it Git - helm.git/blob - matita/library/assembly/assembly.ma
1. status factorized out in tick
[helm.git] / matita / library / assembly / assembly.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 set "baseuri" "cic:/matita/assembly/".
16
17 include "nat/div_and_mod.ma".
18 include "list/list.ma".
19
20 inductive exadecimal : Type ≝
21    x0: exadecimal
22  | x1: exadecimal
23  | x2: exadecimal
24  | x3: exadecimal
25  | x4: exadecimal
26  | x5: exadecimal
27  | x6: exadecimal
28  | x7: exadecimal
29  | x8: exadecimal
30  | x9: exadecimal
31  | xA: exadecimal
32  | xB: exadecimal
33  | xC: exadecimal
34  | xD: exadecimal
35  | xE: exadecimal
36  | xF: exadecimal.
37  
38 record byte : Type ≝ {
39  bh: exadecimal;
40  bl: exadecimal
41 }.
42
43 definition eqex ≝
44  λb1,b2.
45   match b1 with
46    [ x0 ⇒
47        match b2 with
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 ] 
52    | x1 ⇒
53        match b2 with
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 ] 
58    | x2 ⇒
59        match b2 with
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 ] 
64    | x3 ⇒
65        match b2 with
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 ] 
70    | x4 ⇒
71        match b2 with
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 ] 
76    | x5 ⇒
77        match b2 with
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 ] 
82    | x6 ⇒
83        match b2 with
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 ] 
88    | x7 ⇒
89        match b2 with
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 ] 
94    | x8 ⇒
95        match b2 with
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 ] 
100    | x9 ⇒
101        match b2 with
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 ] 
106    | xA ⇒
107        match b2 with
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 ] 
112    | xB ⇒
113        match b2 with
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 ] 
118    | xC ⇒
119        match b2 with
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 ] 
124    | xD ⇒
125        match b2 with
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 ] 
130    | xE ⇒
131        match b2 with
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 ] 
136    | xF ⇒
137        match b2 with
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  ]]. 
142
143
144 definition eqbyte ≝
145  λb,b'. eqex (bh b) (bh b') ∧ eqex (bl b) (bl b').
146
147 inductive cartesian_product (A,B: Type) : Type ≝
148  couple: ∀a:A.∀b:B. cartesian_product A B.
149
150 definition plusex ≝
151  λb1,b2,c.
152   match c with
153    [ true ⇒
154       match b1 with
155        [ x0 ⇒
156            match b2 with
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 ] 
173        | x1 ⇒
174            match b2 with
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 ] 
191        | x2 ⇒
192            match b2 with
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 ] 
209        | x3 ⇒
210            match b2 with
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 ] 
227        | x4 ⇒
228            match b2 with
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 ] 
245        | x5 ⇒
246            match b2 with
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 ] 
263        | x6 ⇒
264            match b2 with
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 ] 
281        | x7 ⇒
282            match b2 with
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 ] 
299        | x8 ⇒
300            match b2 with
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 ] 
317        | x9 ⇒
318            match b2 with
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 ] 
335        | xA ⇒
336            match b2 with
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 ] 
353        | xB ⇒
354            match b2 with
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 ] 
371        | xC ⇒
372            match b2 with
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 ] 
389        | xD ⇒
390            match b2 with
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 ] 
407        | xE ⇒
408            match b2 with
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 ]
425        | xF ⇒
426            match b2 with
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 ] 
443        ]
444    | false ⇒
445       match b1 with
446        [ x0 ⇒
447            match b2 with
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 ] 
464        | x1 ⇒
465            match b2 with
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 ] 
482        | x2 ⇒
483            match b2 with
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 ] 
500        | x3 ⇒
501            match b2 with
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 ] 
518        | x4 ⇒
519            match b2 with
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 ] 
536        | x5 ⇒
537            match b2 with
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 ] 
554        | x6 ⇒
555            match b2 with
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 ] 
572        | x7 ⇒
573            match b2 with
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 ] 
590        | x8 ⇒
591            match b2 with
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 ] 
608        | x9 ⇒
609            match b2 with
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 ] 
626        | xA ⇒
627            match b2 with
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 ] 
644        | xB ⇒
645            match b2 with
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 ] 
662        | xC ⇒
663            match b2 with
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 ] 
680        | xD ⇒
681            match b2 with
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 ] 
698        | xE ⇒
699            match b2 with
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 ] 
716        | xF ⇒
717            match b2 with
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 ]
734        ]
735    ]
736 .
737
738 definition plusbyte ≝
739  λb1,b2,c.
740   match plusex (bl b1) (bl b2) c with
741    [ couple l c' ⇒
742       match plusex (bh b1) (bh b2) c' with
743        [ couple h c'' ⇒ couple ? ? (mk_byte h l) c'' ]].
744
745 alias num (instance 0) = "natural number".
746 definition nat_of_exadecimal ≝
747  λb.
748   match b with
749    [ x0 ⇒ 0
750    | x1 ⇒ 1
751    | x2 ⇒ 2
752    | x3 ⇒ 3
753    | x4 ⇒ 4
754    | x5 ⇒ 5
755    | x6 ⇒ 6
756    | x7 ⇒ 7
757    | x8 ⇒ 8
758    | x9 ⇒ 9
759    | xA ⇒ 10
760    | xB ⇒ 11
761    | xC ⇒ 12
762    | xD ⇒ 13
763    | xE ⇒ 14
764    | xF ⇒ 15
765    ].
766
767 coercion cic:/matita/assembly/nat_of_exadecimal.con.
768
769 definition nat_of_byte ≝ λb:byte. 16*(bh b) + (bl b).
770
771 coercion cic:/matita/assembly/nat_of_byte.con.
772
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 ]]]]]]]]]]]]]]]]. 
790
791 definition byte_of_nat ≝
792  λn. mk_byte (exadecimal_of_nat (n / 16)) (exadecimal_of_nat n).
793
794 lemma byte_of_nat_nat_of_byte: ∀b. byte_of_nat (nat_of_byte b) = b.
795  intros;
796  elim b;
797  elim e;
798  elim e1;
799  reflexivity.
800 qed.
801
802 definition nat_of_bool ≝
803  λb. match b with [ true ⇒ 1 | false ⇒ 0 ].
804
805 (* Way too slow. Handles 2^32 goals!
806 lemma plusbyte_ok:
807  ∀b1,b2,c.
808   match plusbyte b1 b2 c with
809    [ couple r c' ⇒ b1 + b2 + nat_of_bool c = nat_of_byte r + nat_of_bool c'
810    ].
811  intros;
812  elim c;
813  elim b1;
814  elim e;
815  elim e1;
816  elim b2;
817  elim e2;
818  elim e3;
819  reflexivity.
820 qed.
821 *)
822
823 notation "14" non associative with precedence 80 for @{ 'x14 }.
824 interpretation "natural number" 'x14 = 
825 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
826 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
827 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
828 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
829 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
830 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
831 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
832 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
833 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
834 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
835 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
836 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
837 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
838 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
839 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/1)))))))))))))))).
840
841 notation "22" non associative with precedence 80 for @{ 'x22 }.
842 interpretation "natural number" 'x22 = 
843 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
844 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
845 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
846 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
847 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
848 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
849 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
850 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
851 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
852 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
853 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
854 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
855 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
856 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
857 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
858 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
859 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
860 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
861 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
862 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
863 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
864 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
865 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/1)))))))))))))))))))))))).
866  
867 notation "256" non associative with precedence 80 for @{ 'x256 }.
868 interpretation "natural number" 'x256 = 
869 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
870 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
871 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
872 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
873 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
874 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
875 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
876 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
877 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
878 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
879 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
880 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
881 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
882 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
883 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
884 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
885 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
886 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
887 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
888 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
889 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
890 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
891 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
892 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
893 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
894 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
895 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
896 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
897 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
898 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
899 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
900 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
901 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
902 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
903 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
904 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
905 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
906 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
907 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
908 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
909 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
910 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
911 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
912 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
913 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
914 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
915 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
916 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
917 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
918 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
919 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
920 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
921 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
922 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
923 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
924 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
925 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
926 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
927 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
928 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
929 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
930 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
931 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
932 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
933 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
934 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
935 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
936 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
937 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
938 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
939 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
940 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
941 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
942 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
943 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
944 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
945 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
946 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
947 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
948 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
949 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
950 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
951 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
952 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
953 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
954 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
955 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
956 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
957 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
958 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
959 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
960 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
961 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
962 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
963 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
964 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
965 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
966 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
967 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
968 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
969 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
970 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
971 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
972 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
973 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
974 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
975 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
976 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
977 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
978 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
979 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
980 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
981 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
982 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
983 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
984 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
985 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
986 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
987 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
988 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
989 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
990 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
991 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
992 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
993 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
994 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
995 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
996 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
997 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
998 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
999 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1000 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1001 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1002 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1003 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1004 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1005 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1006 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1007 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1008 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1009 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1010 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1011 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1012 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1013 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1014 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1015 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1016 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1017 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1018 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1019 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1020 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1021 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1022 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1023 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1024 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1025 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1026 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1027 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1028 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1029 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1030 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1031 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1032 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1033 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1034 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1035 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1036 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1037 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1038 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1039 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1040 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1041 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1042 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1043 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1044 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1045 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1046 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1047 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1048 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1049 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1050 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1051 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1052 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1053 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1054 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1055 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1056 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1057 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1058 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1059 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1060 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1061 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1062 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1063 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1064 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1065 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1066 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1067 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1068 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1069 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1070 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1071 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1072 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1073 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1074 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1075 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1076 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1077 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1078 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1079 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1080 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1081 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1082 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1083 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1084 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1085 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1086 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1087 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1088 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1089 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1090 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1091 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1092 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1093 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1094 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1095 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1096 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1097 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1098 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1099 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1100 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1101 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1102 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1103 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1104 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1105 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1106 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1107 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1108 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1109 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1110 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1111 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1112 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1113 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1114 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1115 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1116 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1117 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1118 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1119 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1120 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1121 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
1122 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/1) 
1123 ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
1124 ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
1125 ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
1126 )))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))).
1127
1128 (*
1129 lemma sign_ok: ∀ n:nat. nat_of_byte (byte_of_nat n) = n \mod 256.
1130  intros; elim n; [ reflexivity | unfold byte_of_nat. 
1131 qed.
1132 *)
1133
1134 definition addr ≝ nat.
1135
1136 definition xpred ≝
1137  λb.
1138   match b with
1139    [ x0 ⇒ xF
1140    | x1 ⇒ x0
1141    | x2 ⇒ x1
1142    | x3 ⇒ x2
1143    | x4 ⇒ x3
1144    | x5 ⇒ x4
1145    | x6 ⇒ x5
1146    | x7 ⇒ x6
1147    | x8 ⇒ x7
1148    | x9 ⇒ x8
1149    | xA ⇒ x9
1150    | xB ⇒ xA
1151    | xC ⇒ xB
1152    | xD ⇒ xC
1153    | xE ⇒ xD
1154    | xF ⇒ xE ].
1155
1156 definition bpred ≝
1157  λb.
1158   match eqex (bl b) x0 with
1159    [ true ⇒ mk_byte (xpred (bh b)) (xpred (bl b))
1160    | false ⇒ mk_byte (bh b) (xpred (bl b))
1161    ]. 
1162
1163 (* Way too slow and subsumed by previous theorem
1164 lemma bpred_pred:
1165  ∀b.
1166   match eqbyte b (mk_byte x0 x0) with
1167    [ true ⇒ nat_of_byte (bpred b) = mk_byte xF xF
1168    | false ⇒ nat_of_byte (bpred b) = pred (nat_of_byte b)].
1169  intros;
1170  elim b;
1171  elim e;
1172  elim e1;
1173  reflexivity.
1174 qed.
1175 *)
1176
1177 definition addr_of_byte : byte → addr ≝ λb. nat_of_byte b.
1178
1179 coercion cic:/matita/assembly/addr_of_byte.con.
1180
1181 inductive opcode: Type ≝
1182    ADDd: opcode  (* 3 clock, 171 *)
1183  | BEQ: opcode   (* 3, 55 *)
1184  | BRA: opcode   (* 3, 48 *)
1185  | DECd: opcode  (* 5, 58 *)
1186  | LDAi: opcode  (* 2, 166 *)
1187  | LDAd: opcode  (* 3, 182 *)
1188  | STAd: opcode. (* 3, 183 *)
1189
1190 let rec cycles_of_opcode op : nat ≝
1191  match op with
1192   [ ADDd ⇒ 3
1193   | BEQ ⇒ 3
1194   | BRA ⇒ 3
1195   | DECd ⇒ 5
1196   | LDAi ⇒ 2
1197   | LDAd ⇒ 3
1198   | STAd ⇒ 3
1199   ].
1200
1201 definition opcodemap ≝
1202  [ couple ? ? ADDd (mk_byte xA xB);
1203    couple ? ? BEQ (mk_byte x3 x7);
1204    couple ? ? BRA (mk_byte x3 x0);
1205    couple ? ? DECd (mk_byte x3 xA);
1206    couple ? ? LDAi (mk_byte xA x6);
1207    couple ? ? LDAd (mk_byte xB x6);
1208    couple ? ? STAd (mk_byte xB x7) ].
1209
1210 definition opcode_of_byte ≝
1211  λb.
1212   let rec aux l ≝
1213    match l with
1214     [ nil ⇒ ADDd
1215     | cons c tl ⇒
1216        match c with
1217         [ couple op n ⇒
1218            match eqbyte n b with
1219             [ true ⇒ op
1220             | false ⇒ aux tl
1221             ]]]
1222   in
1223    aux opcodemap.
1224
1225 definition magic_of_opcode ≝
1226  λop1.
1227   match op1 with
1228    [ ADDd ⇒ 0
1229    | BEQ ⇒  1 
1230    | BRA ⇒  2
1231    | DECd ⇒ 3
1232    | LDAi ⇒ 4
1233    | LDAd ⇒ 5
1234    | STAd ⇒ 6 ].
1235    
1236 definition opcodeeqb ≝
1237  λop1,op2. eqb (magic_of_opcode op1) (magic_of_opcode op2).
1238
1239 definition byte_of_opcode : opcode → byte ≝
1240  λop.
1241   let rec aux l ≝
1242    match l with
1243     [ nil ⇒ mk_byte x0 x0
1244     | cons c tl ⇒
1245        match c with
1246         [ couple op' n ⇒
1247            match opcodeeqb op op' with
1248             [ true ⇒ n
1249             | false ⇒ aux tl
1250             ]]]
1251   in
1252    aux opcodemap.
1253
1254 record status : Type ≝ {
1255   acc : byte;
1256   pc  : addr;
1257   spc : addr;
1258   zf  : bool;
1259   cf  : bool;
1260   mem : addr → byte;
1261   clk : nat
1262 }.
1263
1264 definition update ≝
1265  λf: addr → byte.λa.λv.λx.
1266   match eqb x a with
1267    [ true ⇒ v
1268    | false ⇒ f x ].
1269
1270 definition mmod16 ≝ λn. nat_of_byte (byte_of_nat n).
1271
1272 definition tick ≝
1273  λs:status. match s with [ mk_status acc pc spc zf cf mem clk ⇒
1274   let opc ≝ opcode_of_byte (mem pc) in
1275   let op1 ≝ mem (S pc) in
1276   let clk' ≝ cycles_of_opcode opc in
1277   match eqb (S clk) clk' with
1278    [ true ⇒
1279       match opc with
1280        [ ADDd ⇒
1281           let res ≝ plusbyte acc (mem op1) false in (* verify carrier! *)
1282           let acc' ≝ match res with [ couple acc' _ ⇒ acc' ] in
1283           let c' ≝ match res with [ couple _ c' ⇒ c'] in
1284            mk_status acc' (2 + pc) spc
1285             (eqb O (nat_of_byte acc')) c' mem 0 (* verify carrier! *)
1286        | BEQ ⇒
1287           mk_status
1288            acc
1289            (match zf with
1290              [ true ⇒ mmod16 (2 + op1 + pc) (*\mod 256*)   (* signed!!! *)
1291              | false ⇒ 2 + pc
1292              ])
1293            spc
1294            zf
1295            cf
1296            mem
1297            0
1298        | BRA ⇒
1299           mk_status
1300            acc (mmod16 (2 + op1 + pc) (*\mod 256*)) (* signed!!! *)
1301            spc
1302            zf
1303            cf
1304            mem
1305            0
1306        | DECd ⇒
1307           let x ≝ bpred (mem op1) in (* signed!!! *)
1308           let mem' ≝ update mem op1 x in
1309            mk_status acc (2 + pc) spc
1310             (eqb O x) cf mem' 0 (* check zb!!! *)
1311        | LDAi ⇒
1312           mk_status op1 (2 + pc) spc (eqb O op1) cf mem 0
1313        | LDAd ⇒
1314           let x ≝ mem op1 in
1315            mk_status x (2 + pc) spc (eqb O x) cf mem 0
1316        | STAd ⇒
1317           mk_status acc (2 + pc) spc zf cf
1318            (update mem op1 acc) 0
1319        ]
1320    | false ⇒
1321        mk_status
1322         acc pc spc zf cf mem (S clk)
1323    ]].
1324
1325 let rec execute s n on n ≝
1326  match n with
1327   [ O ⇒ s
1328   | S n' ⇒ execute (tick s) n'
1329   ].
1330   
1331 lemma foo: ∀s,n. execute s (S n) = execute (tick s) n.
1332  intros; reflexivity.
1333 qed.
1334
1335 notation "hvbox(# break a)"
1336   non associative with precedence 80
1337 for @{ 'byte_of_opcode $a }.
1338 interpretation "byte_of_opcode" 'byte_of_opcode a =
1339  (cic:/matita/assembly/byte_of_opcode.con a).
1340
1341 definition mult_source : list byte ≝
1342   [#LDAi; mk_byte x0 x0; (* A := 0 *)
1343    #STAd; mk_byte x2 x0; (* Z := A *)
1344    #LDAd; mk_byte x1 xF; (* (l1) A := Y *)
1345    #BEQ;  mk_byte x0 xA; (* if A == 0 then goto l2 *)
1346    #LDAd; mk_byte x2 x0; (* A := Z *)
1347    #DECd; mk_byte x1 xF; (* Y := Y - 1 *)
1348    #ADDd; mk_byte x1 xE; (* A += X *)
1349    #STAd; mk_byte x2 x0; (* Z := A *)
1350    #BRA;  mk_byte xF x2; (* goto l1 *)
1351    #LDAd; mk_byte x2 x0].(* (l2) *)
1352
1353 definition mult_status ≝
1354  λx,y.
1355   mk_status (mk_byte x0 x0) 0 0 false false
1356    (λa:addr.
1357      match leb a 29 with
1358       [ true ⇒ nth ? mult_source (mk_byte x0 x0) a
1359       | false ⇒
1360          match eqb a 30 with
1361           [ true ⇒ x
1362           | false ⇒ y
1363           ]
1364       ]) 0.
1365
1366 lemma plusbyte_O_x:
1367  ∀b. plusbyte (mk_byte x0 x0) b false = couple ? ? b false.
1368  intros;
1369  elim b;
1370  elim e;
1371  elim e1;
1372  reflexivity.
1373 qed.
1374
1375 definition plusbytenc ≝
1376  λx,y.
1377   match plusbyte x y false with
1378    [couple res _ ⇒ res].
1379
1380 lemma plusbytenc_O_x:
1381  ∀x. plusbytenc (mk_byte x0 x0) x = x.
1382  intros;
1383  unfold plusbytenc;
1384  rewrite > plusbyte_O_x;
1385  reflexivity.
1386 qed.
1387
1388 lemma test_O_O:
1389   let i ≝ 14 in
1390   let s ≝ execute (mult_status (mk_byte x0 x0) (mk_byte x0 x0)) i in
1391    pc s = 20 ∧ mem s 32 = byte_of_nat 0.
1392  normalize;
1393  split;
1394  reflexivity.
1395 qed.
1396
1397
1398 lemma test_0_2:
1399   let x ≝ mk_byte x0 x0 in
1400   let y ≝ mk_byte x0 x2 in
1401   let i ≝ 14 + 23 * nat_of_byte y in
1402   let s ≝ execute (mult_status x y) i in
1403    pc s = 20 ∧ mem s 32 = plusbytenc x x.
1404  intros;
1405  split;
1406  reflexivity.
1407 qed.
1408
1409 lemma test_x_1:
1410  ∀x.
1411   let y ≝ mk_byte x0 x1 in
1412   let i ≝ 14 + 23 * nat_of_byte y in
1413   let s ≝ execute (mult_status x y) i in
1414    pc s = 20 ∧ mem s 32 = x.
1415  intros;
1416  split;
1417   [ reflexivity
1418   | change in ⊢ (? ? % ?) with (plusbytenc (mk_byte x0 x0) x);
1419     rewrite > plusbytenc_O_x;
1420     reflexivity
1421   ].
1422 qed.
1423
1424 lemma test_x_2:
1425  ∀x.
1426   let y ≝ mk_byte x0 x2 in
1427   let i ≝ 14 + 23 * nat_of_byte y in
1428   let s ≝ execute (mult_status x y) i in
1429    pc s = 20 ∧ mem s 32 = plusbytenc x x.
1430  intros;
1431  split;
1432   [ reflexivity
1433   | change in ⊢ (? ? % ?) with
1434      (plusbytenc (plusbytenc (mk_byte x0 x0) x) x);
1435     rewrite > plusbytenc_O_x;
1436     reflexivity
1437   ].
1438 qed.
1439
1440 (*
1441 lemma test_x_y:
1442  ∀x,y.
1443   let i ≝ 14 + 23 * nat_of_byte y in
1444   let s ≝ execute (mult_status x y) i in
1445    pc s = 20 ∧ mem s 32 = byte_of_nat (nat_of_byte x * nat_of_byte y).
1446  intros;
1447  
1448 qed.
1449 *)
1450
1451 (*
1452  letin w ≝ 22;
1453  letin opc ≝ (let s ≝ execute (mult_status x y) w in opcode_of_byte (mem s (pc s))); whd in opc;
1454  letin acc' ≝ (acc (execute (mult_status x y) w)); 
1455  normalize in acc';
1456  change in acc' with x;
1457  letin z ≝ (let s ≝ (execute (mult_status x y) w) in mem s 32); whd in z;
1458  letin x ≝ (let s ≝ (execute (mult_status x y) w) in mem s 30); whd in x;
1459  (*letin xxx ≝ (byte_of_nat (x+y)); normalize in xxx;*)
1460  split;
1461   [ normalize; reflexivity
1462   | change with (byte_of_nat x = x);
1463  normalize;
1464  split;
1465   [ reflexivity
1466   | change with (byte_of_nat (x + 0));
1467  letin www ≝ (nat_of_byte (byte_of_nat 260)); whd in www;
1468  letin xxx ≝ (260 \mod 256); reduce in xxx;
1469  letin xxx ≝ ((18 + 242) \mod 256);
1470  whd in xxx;
1471  letin pc' ≝ (pc s);
1472  normalize in pc';
1473  letin opcode ≝ (let s ≝ s in opcode_of_byte (mem s (pc s)));
1474  normalize in opcode;
1475  csc.
1476  split;
1477  reduce in s;
1478  reflexivity.
1479 qed.
1480
1481 lemma goo1:
1482  ∀x,y.
1483   let i ≝ 14 + 23 * nat_of_byte y in
1484   let s ≝ execute (mult_status x y) i in
1485    pc s = 22 ∧ mem s 32 = byte_of_nat (nat_of_byte x * nat_of_byte y).
1486  intros;
1487 qed.
1488
1489 lemma goo: True.
1490  letin s0 ≝ mult_status;
1491  letin pc0 ≝ (pc s0); 
1492  reduce in pc0;
1493  letin i0 ≝ (opcode_of_byte (mem s0 pc0));
1494  reduce in i0;
1495  
1496  letin s1 ≝ (execute s0 (cycles_of_opcode i0));
1497  letin pc1 ≝ (pc s1);
1498  reduce in pc1;
1499  letin i1 ≝ (opcode_of_byte (mem s1 pc1));
1500  reduce in i1;
1501
1502  letin s2 ≝ (execute s1 (cycles_of_opcode i1));
1503  letin pc2 ≝ (pc s2);
1504  reduce in pc2;
1505  letin i2 ≝ (opcode_of_byte (mem s2 pc2));
1506  reduce in i2;
1507
1508  letin s3 ≝ (execute s2 (cycles_of_opcode i2));
1509  letin pc3 ≝ (pc s3);
1510  reduce in pc3;
1511  letin i3 ≝ (opcode_of_byte (mem s3 pc3));
1512  reduce in i3;
1513  letin zf3 ≝ (zf s3);
1514  reduce in zf3;
1515
1516  letin s4 ≝ (execute s3 (cycles_of_opcode i3));
1517  letin pc4 ≝ (pc s4);
1518  reduce in pc4;
1519  letin i4 ≝ (opcode_of_byte (mem s4 pc4));
1520  reduce in i4;
1521
1522  letin s5 ≝ (execute s4 (cycles_of_opcode i4));
1523  letin pc5 ≝ (pc s5);
1524  reduce in pc5;
1525  letin i5 ≝ (opcode_of_byte (mem s5 pc5));
1526  reduce in i5;
1527  
1528  letin s6 ≝ (execute s5 (cycles_of_opcode i5));
1529  letin pc6 ≝ (pc s6);
1530  reduce in pc6;
1531  letin i6 ≝ (opcode_of_byte (mem s6 pc6));
1532  reduce in i6;
1533  
1534  letin s7 ≝ (execute s6 (cycles_of_opcode i6));
1535  letin pc7 ≝ (pc s7);
1536  reduce in pc7;
1537  letin i7 ≝ (opcode_of_byte (mem s7 pc7));
1538  reduce in i7;
1539  
1540  letin s8 ≝ (execute s7 (cycles_of_opcode i7));
1541  letin pc8 ≝ (pc s8);
1542  reduce in pc8;
1543  letin i8 ≝ (opcode_of_byte (mem s8 pc8));
1544  reduce in i8;
1545
1546  letin s9 ≝ (execute s8 (cycles_of_opcode i8));
1547  letin pc9 ≝ (pc s9);
1548  reduce in pc9;
1549  letin i9 ≝ (opcode_of_byte (mem s9 pc9));
1550  reduce in i9;
1551  
1552  exact I.
1553 qed.
1554 *)