]> matita.cs.unibo.it Git - helm.git/blob - matita/library/assembly/assembly.ma
0. less nice solution by Enrico reverted
[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 alias num (instance 0) = "natural number".
148 definition nat_of_exadecimal ≝
149  λb.
150   match b with
151    [ x0 ⇒ 0
152    | x1 ⇒ 1
153    | x2 ⇒ 2
154    | x3 ⇒ 3
155    | x4 ⇒ 4
156    | x5 ⇒ 5
157    | x6 ⇒ 6
158    | x7 ⇒ 7
159    | x8 ⇒ 8
160    | x9 ⇒ 9
161    | xA ⇒ 10
162    | xB ⇒ 11
163    | xC ⇒ 12
164    | xD ⇒ 13
165    | xE ⇒ 14
166    | xF ⇒ 15
167    ].
168
169 coercion cic:/matita/assembly/nat_of_exadecimal.con.
170
171 definition nat_of_byte ≝ λb:byte. 16*(bh b) + (bl b).
172
173 coercion cic:/matita/assembly/nat_of_byte.con.
174
175 let rec exadecimal_of_nat b ≝
176   match b with [ O ⇒ x0 | S b ⇒
177   match b with [ O ⇒ x1 | S b ⇒
178   match b with [ O ⇒ x2 | S b ⇒ 
179   match b with [ O ⇒ x3 | S b ⇒ 
180   match b with [ O ⇒ x4 | S b ⇒ 
181   match b with [ O ⇒ x5 | S b ⇒ 
182   match b with [ O ⇒ x6 | S b ⇒ 
183   match b with [ O ⇒ x7 | S b ⇒ 
184   match b with [ O ⇒ x8 | S b ⇒ 
185   match b with [ O ⇒ x9 | S b ⇒ 
186   match b with [ O ⇒ xA | S b ⇒ 
187   match b with [ O ⇒ xB | S b ⇒ 
188   match b with [ O ⇒ xC | S b ⇒ 
189   match b with [ O ⇒ xD | S b ⇒ 
190   match b with [ O ⇒ xE | S b ⇒ 
191   match b with [ O ⇒ xF | S b ⇒ exadecimal_of_nat b ]]]]]]]]]]]]]]]]. 
192
193 definition byte_of_nat ≝
194  λn. mk_byte (exadecimal_of_nat (n / 16)) (exadecimal_of_nat n).
195
196 lemma byte_of_nat_nat_of_byte: ∀b. byte_of_nat (nat_of_byte b) = b.
197  intros;
198  elim b;
199  elim e;
200  elim e1;
201  reflexivity.
202 qed.
203
204 notation "14" non associative with precedence 80 for @{ 'x14 }.
205 interpretation "natural number" 'x14 = 
206 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
207 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
208 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
209 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
210 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
211 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
212 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
213 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
214 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
215 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
216 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
217 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
218 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
219 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
220 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/1)))))))))))))))).
221
222 notation "22" non associative with precedence 80 for @{ 'x22 }.
223 interpretation "natural number" 'x22 = 
224 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
225 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
226 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
227 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
228 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
229 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
230 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
231 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
232 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
233 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
234 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
235 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
236 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
237 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
238 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
239 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
240 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
241 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
242 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
243 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
244 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
245 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
246 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/1)))))))))))))))))))))))).
247  
248 notation "256" non associative with precedence 80 for @{ 'x256 }.
249 interpretation "natural number" 'x256 = 
250 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
251 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
252 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
253 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
254 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
255 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
256 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
257 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
258 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
259 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
260 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
261 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
262 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
263 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
264 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
265 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
266 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
267 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
268 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
269 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
270 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
271 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
272 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
273 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
274 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
275 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
276 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
277 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
278 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
279 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
280 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
281 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
282 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
283 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
284 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
285 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
286 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
287 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
288 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
289 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
290 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
291 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
292 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
293 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
294 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
295 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
296 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
297 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
298 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
299 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
300 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
301 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
302 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
303 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
304 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
305 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
306 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
307 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
308 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
309 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
310 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
311 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
312 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
313 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
314 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
315 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
316 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
317 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
318 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
319 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
320 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
321 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
322 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
323 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
324 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
325 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
326 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
327 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
328 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
329 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
330 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
331 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
332 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
333 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
334 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
335 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
336 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
337 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
338 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
339 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
340 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
341 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
342 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
343 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
344 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
345 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
346 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
347 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
348 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
349 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
350 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
351 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
352 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
353 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
354 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
355 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
356 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
357 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
358 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
359 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
360 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
361 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
362 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
363 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
364 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
365 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
366 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
367 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
368 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
369 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
370 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
371 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
372 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
373 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
374 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
375 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
376 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
377 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
378 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
379 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
380 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
381 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
382 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
383 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
384 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
385 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
386 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
387 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
388 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
389 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
390 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
391 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
392 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
393 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
394 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
395 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
396 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
397 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
398 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
399 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
400 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
401 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
402 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
403 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
404 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
405 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
406 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
407 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
408 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
409 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
410 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
411 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
412 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
413 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
414 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
415 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
416 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
417 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
418 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
419 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
420 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
421 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
422 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
423 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
424 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
425 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
426 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
427 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
428 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
429 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
430 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
431 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
432 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
433 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
434 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
435 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
436 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
437 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
438 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
439 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
440 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
441 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
442 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
443 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
444 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
445 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
446 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
447 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
448 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
449 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
450 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
451 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
452 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
453 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
454 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
455 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
456 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
457 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
458 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
459 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
460 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
461 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
462 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
463 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
464 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
465 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
466 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
467 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
468 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
469 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
470 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
471 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
472 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
473 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
474 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
475 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
476 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
477 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
478 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
479 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
480 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
481 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
482 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
483 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
484 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
485 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
486 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
487 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
488 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
489 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
490 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
491 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
492 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
493 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
494 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
495 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
496 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
497 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
498 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
499 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
500 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
501 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
502 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
503 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/1) 
504 ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
505 ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
506 ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
507 )))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))).
508
509 (*
510 lemma sign_ok: ∀ n:nat. nat_of_byte (byte_of_nat n) = n \mod 256.
511  intros; elim n; [ reflexivity | unfold byte_of_nat. 
512 qed.
513 *)
514
515 definition addr ≝ nat.
516
517 definition xpred ≝
518  λb.
519   match b with
520    [ x0 ⇒ xF
521    | x1 ⇒ x0
522    | x2 ⇒ x1
523    | x3 ⇒ x2
524    | x4 ⇒ x3
525    | x5 ⇒ x4
526    | x6 ⇒ x5
527    | x7 ⇒ x6
528    | x8 ⇒ x7
529    | x9 ⇒ x8
530    | xA ⇒ x9
531    | xB ⇒ xA
532    | xC ⇒ xB
533    | xD ⇒ xC
534    | xE ⇒ xD
535    | xF ⇒ xE ].
536
537 definition bpred ≝
538  λb.
539   match eqex (bl b) x0 with
540    [ true ⇒ mk_byte (xpred (bh b)) (xpred (bl b))
541    | false ⇒ mk_byte (bh b) (xpred (bl b))
542    ]. 
543
544 (* Way too slow and subsumed by previous theorem
545 lemma bpred_pred:
546  ∀b.
547   match eqbyte b (mk_byte x0 x0) with
548    [ true ⇒ nat_of_byte (bpred b) = mk_byte xF xF
549    | false ⇒ nat_of_byte (bpred b) = pred (nat_of_byte b)].
550  intros;
551  elim b;
552  elim e;
553  elim e1;
554  reflexivity.
555 qed.
556 *)
557
558 definition addr_of_byte : byte → addr ≝ λb. nat_of_byte b.
559
560 coercion cic:/matita/assembly/addr_of_byte.con.
561
562 inductive opcode: Type ≝
563    ADDd: opcode  (* 3 clock, 171 *)
564  | BEQ: opcode   (* 3, 55 *)
565  | BRA: opcode   (* 3, 48 *)
566  | DECd: opcode  (* 5, 58 *)
567  | LDAi: opcode  (* 2, 166 *)
568  | LDAd: opcode  (* 3, 182 *)
569  | STAd: opcode. (* 3, 183 *)
570
571 let rec cycles_of_opcode op : nat ≝
572  match op with
573   [ ADDd ⇒ 3
574   | BEQ ⇒ 3
575   | BRA ⇒ 3
576   | DECd ⇒ 5
577   | LDAi ⇒ 2
578   | LDAd ⇒ 3
579   | STAd ⇒ 3
580   ].
581
582 inductive cartesian_product (A,B: Type) : Type ≝
583  couple: ∀a:A.∀b:B. cartesian_product A B.
584
585 definition opcodemap ≝
586  [ couple ? ? ADDd (mk_byte xA xB);
587    couple ? ? BEQ (mk_byte x3 x7);
588    couple ? ? BRA (mk_byte x3 x0);
589    couple ? ? DECd (mk_byte x3 xA);
590    couple ? ? LDAi (mk_byte xA x6);
591    couple ? ? LDAd (mk_byte xB x6);
592    couple ? ? STAd (mk_byte xB x7) ].
593
594 definition opcode_of_byte ≝
595  λb.
596   let rec aux l ≝
597    match l with
598     [ nil ⇒ ADDd
599     | cons c tl ⇒
600        match c with
601         [ couple op n ⇒
602            match eqbyte n b with
603             [ true ⇒ op
604             | false ⇒ aux tl
605             ]]]
606   in
607    aux opcodemap.
608
609 definition magic_of_opcode ≝
610  λop1.
611   match op1 with
612    [ ADDd ⇒ 0
613    | BEQ ⇒  1 
614    | BRA ⇒  2
615    | DECd ⇒ 3
616    | LDAi ⇒ 4
617    | LDAd ⇒ 5
618    | STAd ⇒ 6 ].
619    
620 definition opcodeeqb ≝
621  λop1,op2. eqb (magic_of_opcode op1) (magic_of_opcode op2).
622
623 definition byte_of_opcode : opcode → byte ≝
624  λop.
625   let rec aux l ≝
626    match l with
627     [ nil ⇒ mk_byte x0 x0
628     | cons c tl ⇒
629        match c with
630         [ couple op' n ⇒
631            match opcodeeqb op op' with
632             [ true ⇒ n
633             | false ⇒ aux tl
634             ]]]
635   in
636    aux opcodemap.
637
638 record status : Type ≝ {
639   acc : byte;
640   pc  : addr;
641   spc : addr;
642   zf  : bool;
643   cf  : bool;
644   mem : addr → byte;
645   clk : nat
646 }.
647
648 definition update ≝
649  λf: addr → byte.λa.λv.λx.
650   match eqb x a with
651    [ true ⇒ v
652    | false ⇒ f x ].
653
654 definition mmod16 ≝ λn. nat_of_byte (byte_of_nat n).
655
656 definition tick ≝
657  λs:status.
658   (* fetch *)
659   let opc ≝ opcode_of_byte (mem s (pc s)) in
660   let op1 ≝ mem s (S (pc s)) in
661   let clk' ≝ cycles_of_opcode opc in
662   match eqb (S (clk s)) clk' with
663    [ true ⇒
664       match opc with
665        [ ADDd ⇒
666           let x ≝ nat_of_byte (mem s op1) in
667           let acc' ≝ acc s + x in (* signed!!! *)
668            mk_status (byte_of_nat acc') (2 + pc s) (spc s)
669             (eqb O acc') (cf s) (mem s) 0
670        | BEQ ⇒
671           mk_status
672            (acc s)
673            (match zf s with
674              [ true ⇒ mmod16 (2 + op1 + pc s) (*\mod 256*)   (* signed!!! *)
675              | false ⇒ 2 + pc s
676              ])
677            (spc s)
678            (zf s)
679            (cf s)
680            (mem s)
681            0
682        | BRA ⇒
683           mk_status
684            (acc s) (mmod16 (2 + op1 + pc s) (*\mod 256*)) (* signed!!! *)
685            (spc s)
686            (zf s)
687            (cf s)
688            (mem s)
689            0
690        | DECd ⇒
691           let x ≝ bpred (mem s op1) in (* signed!!! *)
692           let mem' ≝ update (mem s) op1 x in
693            mk_status (acc s) (2 + pc s) (spc s)
694             (eqb O x) (cf s) mem' 0 (* check zb!!! *)
695        | LDAi ⇒
696           mk_status op1 (2 + pc s) (spc s) (eqb O op1) (cf s) (mem s) 0
697        | LDAd ⇒
698           let x ≝ mem s op1 in
699            mk_status x (2 + pc s) (spc s) (eqb O x) (cf s) (mem s) 0
700        | STAd ⇒
701           mk_status (acc s) (2 + pc s) (spc s) (zf s) (cf s)
702            (update (mem s) op1 (acc s)) 0
703        ]
704    | false ⇒
705        mk_status
706         (acc s) (pc s) (spc s) (zf s) (cf s) (mem s) (S (clk s))
707    ].
708
709 let rec execute s n on n ≝
710  match n with
711   [ O ⇒ s
712   | S n' ⇒ execute (tick s) n'
713   ].
714   
715 lemma foo: ∀s,n. execute s (S n) = execute (tick s) n.
716  intros; reflexivity.
717 qed.
718
719 notation "hvbox(# break a)"
720   non associative with precedence 80
721 for @{ 'byte_of_opcode $a }.
722 interpretation "byte_of_opcode" 'byte_of_opcode a =
723  (cic:/matita/assembly/byte_of_opcode.con a).
724
725 definition mult_source : list byte ≝
726   [#LDAi; mk_byte x0 x0; (* A := 0 *)
727    #STAd; mk_byte x2 x0; (* Z := A *)
728    #LDAd; mk_byte x1 xF; (* (l1) A := Y *)
729    #BEQ;  mk_byte x0 xA; (* if A == 0 then goto l2 *)
730    #LDAd; mk_byte x2 x0; (* A := Z *)
731    #DECd; mk_byte x1 xF; (* Y := Y - 1 *)
732    #ADDd; mk_byte x1 xE; (* A += X *)
733    #STAd; mk_byte x2 x0; (* Z := A *)
734    #BRA;  mk_byte xF x2; (* goto l1 *)
735    #LDAd; mk_byte x2 x0].(* (l2) *)
736
737 definition mult_status ≝
738  λx,y.
739   mk_status (mk_byte x0 x0) 0 0 false false
740    (λa:addr.
741      match leb a 29 with
742       [ true ⇒ nth ? mult_source (mk_byte x0 x0) a
743       | false ⇒
744          match eqb a 30 with
745           [ true ⇒ x
746           | false ⇒ y
747           ]
748       ]) 0.
749
750 (*
751 lemma foobar:
752  ∀x.
753   let y ≝ mk_byte x0 x1 in
754   let i ≝ 14 + 23 * nat_of_byte y in
755   let s ≝ execute (mult_status x y) i in
756    pc s = 20 ∧ mem s 32 = x.
757  intros;
758  letin w ≝ 22;
759  letin opc ≝ (let s ≝ execute (mult_status x y) w in opcode_of_byte (mem s (pc s))); whd in opc;
760  letin acc' ≝ (acc (execute (mult_status x y) w)); change in acc' with (byte_of_nat x);
761  letin z ≝ (let s ≝ (execute (mult_status x y) w) in mem s 32); whd in z;
762  letin x ≝ (let s ≝ (execute (mult_status x y) w) in mem s 30); whd in x;
763  (*letin xxx ≝ (byte_of_nat (x+y)); normalize in xxx;*)
764  split;
765   [ normalize; reflexivity
766   | change with (byte_of_nat x = x);
767  normalize;
768  split;
769   [ reflexivity
770   | change with (byte_of_nat (x + 0));
771  letin www ≝ (nat_of_byte (byte_of_nat 260)); whd in www;
772  letin xxx ≝ (260 \mod 256); reduce in xxx;
773  letin xxx ≝ ((18 + 242) \mod 256);
774  whd in xxx;
775  letin pc' ≝ (pc s);
776  normalize in pc';
777  letin opcode ≝ (let s ≝ s in opcode_of_byte (mem s (pc s)));
778  normalize in opcode;
779  csc.
780  split;
781  reduce in s;
782  reflexivity.
783 qed.
784
785 lemma goo1:
786  ∀x,y.
787   let i ≝ 14 + 23 * nat_of_byte y in
788   let s ≝ execute (mult_status x y) i in
789    pc s = 22 ∧ mem s 32 = byte_of_nat (nat_of_byte x * nat_of_byte y).
790  intros;
791 qed.
792
793 lemma goo: True.
794  letin s0 ≝ mult_status;
795  letin pc0 ≝ (pc s0); 
796  reduce in pc0;
797  letin i0 ≝ (opcode_of_byte (mem s0 pc0));
798  reduce in i0;
799  
800  letin s1 ≝ (execute s0 (cycles_of_opcode i0));
801  letin pc1 ≝ (pc s1);
802  reduce in pc1;
803  letin i1 ≝ (opcode_of_byte (mem s1 pc1));
804  reduce in i1;
805
806  letin s2 ≝ (execute s1 (cycles_of_opcode i1));
807  letin pc2 ≝ (pc s2);
808  reduce in pc2;
809  letin i2 ≝ (opcode_of_byte (mem s2 pc2));
810  reduce in i2;
811
812  letin s3 ≝ (execute s2 (cycles_of_opcode i2));
813  letin pc3 ≝ (pc s3);
814  reduce in pc3;
815  letin i3 ≝ (opcode_of_byte (mem s3 pc3));
816  reduce in i3;
817  letin zf3 ≝ (zf s3);
818  reduce in zf3;
819
820  letin s4 ≝ (execute s3 (cycles_of_opcode i3));
821  letin pc4 ≝ (pc s4);
822  reduce in pc4;
823  letin i4 ≝ (opcode_of_byte (mem s4 pc4));
824  reduce in i4;
825
826  letin s5 ≝ (execute s4 (cycles_of_opcode i4));
827  letin pc5 ≝ (pc s5);
828  reduce in pc5;
829  letin i5 ≝ (opcode_of_byte (mem s5 pc5));
830  reduce in i5;
831  
832  letin s6 ≝ (execute s5 (cycles_of_opcode i5));
833  letin pc6 ≝ (pc s6);
834  reduce in pc6;
835  letin i6 ≝ (opcode_of_byte (mem s6 pc6));
836  reduce in i6;
837  
838  letin s7 ≝ (execute s6 (cycles_of_opcode i6));
839  letin pc7 ≝ (pc s7);
840  reduce in pc7;
841  letin i7 ≝ (opcode_of_byte (mem s7 pc7));
842  reduce in i7;
843  
844  letin s8 ≝ (execute s7 (cycles_of_opcode i7));
845  letin pc8 ≝ (pc s8);
846  reduce in pc8;
847  letin i8 ≝ (opcode_of_byte (mem s8 pc8));
848  reduce in i8;
849
850  letin s9 ≝ (execute s8 (cycles_of_opcode i8));
851  letin pc9 ≝ (pc s9);
852  reduce in pc9;
853  letin i9 ≝ (opcode_of_byte (mem s9 pc9));
854  reduce in i9;
855  
856  exact I.
857 qed.
858 *)