1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* ********************************************************************** *)
16 (* Progetto FreeScale *)
18 (* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *)
19 (* Cosimo Oliboni, oliboni@cs.unibo.it *)
21 (* ********************************************************************** *)
23 include "freescale/opcode_base_lemmas_instrmode1.ma".
25 (* ********************************************** *)
26 (* MATTONI BASE PER DEFINIRE LE TABELLE DELLE MCU *)
27 (* ********************************************** *)
29 nlemma symmetric_eqim : symmetricT instr_mode bool eq_im.
32 ##[ ##1: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
33 ##| ##2: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
34 ##| ##3: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
35 ##| ##4: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
36 ##| ##5: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
37 ##| ##6: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
38 ##| ##7: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
39 ##| ##8: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
40 ##| ##9: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
41 ##| ##10: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
42 ##| ##11: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
43 ##| ##12: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
44 ##| ##13: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
45 ##| ##14: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
46 ##| ##15: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
47 ##| ##16: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
48 ##| ##17: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
49 ##| ##18: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
50 ##| ##19: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
51 ##| ##20: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
52 ##| ##21: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
53 ##| ##22: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
54 ##| ##23: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
55 ##| ##24: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
56 ##| ##25: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
57 ##| ##26: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
58 ##| ##27: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
59 ##| ##28: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
60 ##| ##29: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
61 ##| ##30: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
62 ##| ##31: ncases i2; #n1;
64 nchange with (eq_oct n2 n1 = eq_oct n1 n2);
65 nrewrite > (symmetric_eqoct n1 n2);
66 ##| ##32,33,34: #n2; nnormalize
68 nnormalize; napply refl_eq
69 ##| ##32: ncases i2; #n1;
71 nchange with (eq_oct n2 n1 = eq_oct n1 n2);
72 nrewrite > (symmetric_eqoct n1 n2);
73 ##| ##31,33,34: #n2; nnormalize
75 nnormalize; napply refl_eq
76 ##| ##33: ncases i2; #n1;
78 nchange with (eq_ex n2 n1 = eq_ex n1 n2);
79 nrewrite > (symmetric_eqex n1 n2);
80 ##| ##31,32,34: #n2; nnormalize
82 nnormalize; napply refl_eq
83 ##| ##34: ncases i2; #n1;
85 nchange with (eq_bit n2 n1 = eq_bit n1 n2);
86 nrewrite > (symmetric_eqbit n1 n2);
87 ##| ##31,32,33: #n2; nnormalize
89 nnormalize; napply refl_eq
93 nlemma eqim_to_eq1 : ∀i2.eq_im MODE_INH i2 = true → MODE_INH = i2.
94 #i2; ncases i2; nnormalize;
95 ##[ ##1: #H; napply refl_eq
96 ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
97 ##| ##*: #H; napply (bool_destruct … H)
101 nlemma eqim_to_eq2 : ∀i2.eq_im MODE_INHA i2 = true → MODE_INHA = i2.
102 #i2; ncases i2; nnormalize;
103 ##[ ##2: #H; napply refl_eq
104 ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
105 ##| ##*: #H; napply (bool_destruct … H)
109 nlemma eqim_to_eq3 : ∀i2.eq_im MODE_INHX i2 = true → MODE_INHX = i2.
110 #i2; ncases i2; nnormalize;
111 ##[ ##3: #H; napply refl_eq
112 ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
113 ##| ##*: #H; napply (bool_destruct … H)
117 nlemma eqim_to_eq4 : ∀i2.eq_im MODE_INHH i2 = true → MODE_INHH = i2.
118 #i2; ncases i2; nnormalize;
119 ##[ ##4: #H; napply refl_eq
120 ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
121 ##| ##*: #H; napply (bool_destruct … H)
125 nlemma eqim_to_eq5 : ∀i2.eq_im MODE_INHX0ADD i2 = true → MODE_INHX0ADD = i2.
126 #i2; ncases i2; nnormalize;
127 ##[ ##5: #H; napply refl_eq
128 ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
129 ##| ##*: #H; napply (bool_destruct … H)
133 nlemma eqim_to_eq6 : ∀i2.eq_im MODE_INHX1ADD i2 = true → MODE_INHX1ADD = i2.
134 #i2; ncases i2; nnormalize;
135 ##[ ##6: #H; napply refl_eq
136 ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
137 ##| ##*: #H; napply (bool_destruct … H)
141 nlemma eqim_to_eq7 : ∀i2.eq_im MODE_INHX2ADD i2 = true → MODE_INHX2ADD = i2.
142 #i2; ncases i2; nnormalize;
143 ##[ ##7: #H; napply refl_eq
144 ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
145 ##| ##*: #H; napply (bool_destruct … H)
149 nlemma eqim_to_eq8 : ∀i2.eq_im MODE_IMM1 i2 = true → MODE_IMM1 = i2.
150 #i2; ncases i2; nnormalize;
151 ##[ ##8: #H; napply refl_eq
152 ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
153 ##| ##*: #H; napply (bool_destruct … H)
157 nlemma eqim_to_eq9 : ∀i2.eq_im MODE_IMM1EXT i2 = true → MODE_IMM1EXT = i2.
158 #i2; ncases i2; nnormalize;
159 ##[ ##9: #H; napply refl_eq
160 ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
161 ##| ##*: #H; napply (bool_destruct … H)
165 nlemma eqim_to_eq10 : ∀i2.eq_im MODE_IMM2 i2 = true → MODE_IMM2 = i2.
166 #i2; ncases i2; nnormalize;
167 ##[ ##10: #H; napply refl_eq
168 ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
169 ##| ##*: #H; napply (bool_destruct … H)
173 nlemma eqim_to_eq11 : ∀i2.eq_im MODE_DIR1 i2 = true → MODE_DIR1 = i2.
174 #i2; ncases i2; nnormalize;
175 ##[ ##11: #H; napply refl_eq
176 ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
177 ##| ##*: #H; napply (bool_destruct … H)
181 nlemma eqim_to_eq12 : ∀i2.eq_im MODE_DIR2 i2 = true → MODE_DIR2 = i2.
182 #i2; ncases i2; nnormalize;
183 ##[ ##12: #H; napply refl_eq
184 ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
185 ##| ##*: #H; napply (bool_destruct … H)
189 nlemma eqim_to_eq13 : ∀i2.eq_im MODE_IX0 i2 = true → MODE_IX0 = i2.
190 #i2; ncases i2; nnormalize;
191 ##[ ##13: #H; napply refl_eq
192 ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
193 ##| ##*: #H; napply (bool_destruct … H)
197 nlemma eqim_to_eq14 : ∀i2.eq_im MODE_IX1 i2 = true → MODE_IX1 = i2.
198 #i2; ncases i2; nnormalize;
199 ##[ ##14: #H; napply refl_eq
200 ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
201 ##| ##*: #H; napply (bool_destruct … H)
205 nlemma eqim_to_eq15 : ∀i2.eq_im MODE_IX2 i2 = true → MODE_IX2 = i2.
206 #i2; ncases i2; nnormalize;
207 ##[ ##15: #H; napply refl_eq
208 ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
209 ##| ##*: #H; napply (bool_destruct … H)
213 nlemma eqim_to_eq16 : ∀i2.eq_im MODE_SP1 i2 = true → MODE_SP1 = i2.
214 #i2; ncases i2; nnormalize;
215 ##[ ##16: #H; napply refl_eq
216 ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
217 ##| ##*: #H; napply (bool_destruct … H)
221 nlemma eqim_to_eq17 : ∀i2.eq_im MODE_SP2 i2 = true → MODE_SP2 = i2.
222 #i2; ncases i2; nnormalize;
223 ##[ ##17: #H; napply refl_eq
224 ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
225 ##| ##*: #H; napply (bool_destruct … H)
229 nlemma eqim_to_eq18 : ∀i2.eq_im MODE_DIR1_to_DIR1 i2 = true → MODE_DIR1_to_DIR1 = i2.
230 #i2; ncases i2; nnormalize;
231 ##[ ##18: #H; napply refl_eq
232 ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
233 ##| ##*: #H; napply (bool_destruct … H)
237 nlemma eqim_to_eq19 : ∀i2.eq_im MODE_IMM1_to_DIR1 i2 = true → MODE_IMM1_to_DIR1 = i2.
238 #i2; ncases i2; nnormalize;
239 ##[ ##19: #H; napply refl_eq
240 ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
241 ##| ##*: #H; napply (bool_destruct … H)
245 nlemma eqim_to_eq20 : ∀i2.eq_im MODE_IX0p_to_DIR1 i2 = true → MODE_IX0p_to_DIR1 = i2.
246 #i2; ncases i2; nnormalize;
247 ##[ ##20: #H; napply refl_eq
248 ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
249 ##| ##*: #H; napply (bool_destruct … H)
253 nlemma eqim_to_eq21 : ∀i2.eq_im MODE_DIR1_to_IX0p i2 = true → MODE_DIR1_to_IX0p = i2.
254 #i2; ncases i2; nnormalize;
255 ##[ ##21: #H; napply refl_eq
256 ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
257 ##| ##*: #H; napply (bool_destruct … H)
261 nlemma eqim_to_eq22 : ∀i2.eq_im MODE_INHA_and_IMM1 i2 = true → MODE_INHA_and_IMM1 = i2.
262 #i2; ncases i2; nnormalize;
263 ##[ ##22: #H; napply refl_eq
264 ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
265 ##| ##*: #H; napply (bool_destruct … H)
269 nlemma eqim_to_eq23 : ∀i2.eq_im MODE_INHX_and_IMM1 i2 = true → MODE_INHX_and_IMM1 = i2.
270 #i2; ncases i2; nnormalize;
271 ##[ ##23: #H; napply refl_eq
272 ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
273 ##| ##*: #H; napply (bool_destruct … H)
277 nlemma eqim_to_eq24 : ∀i2.eq_im MODE_IMM1_and_IMM1 i2 = true → MODE_IMM1_and_IMM1 = i2.
278 #i2; ncases i2; nnormalize;
279 ##[ ##24: #H; napply refl_eq
280 ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
281 ##| ##*: #H; napply (bool_destruct … H)
285 nlemma eqim_to_eq25 : ∀i2.eq_im MODE_DIR1_and_IMM1 i2 = true → MODE_DIR1_and_IMM1 = i2.
286 #i2; ncases i2; nnormalize;
287 ##[ ##25: #H; napply refl_eq
288 ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
289 ##| ##*: #H; napply (bool_destruct … H)
293 nlemma eqim_to_eq26 : ∀i2.eq_im MODE_IX0_and_IMM1 i2 = true → MODE_IX0_and_IMM1 = i2.
294 #i2; ncases i2; nnormalize;
295 ##[ ##26: #H; napply refl_eq
296 ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
297 ##| ##*: #H; napply (bool_destruct … H)
301 nlemma eqim_to_eq27 : ∀i2.eq_im MODE_IX0p_and_IMM1 i2 = true → MODE_IX0p_and_IMM1 = i2.
302 #i2; ncases i2; nnormalize;
303 ##[ ##27: #H; napply refl_eq
304 ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
305 ##| ##*: #H; napply (bool_destruct … H)
309 nlemma eqim_to_eq28 : ∀i2.eq_im MODE_IX1_and_IMM1 i2 = true → MODE_IX1_and_IMM1 = i2.
310 #i2; ncases i2; nnormalize;
311 ##[ ##28: #H; napply refl_eq
312 ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
313 ##| ##*: #H; napply (bool_destruct … H)
317 nlemma eqim_to_eq29 : ∀i2.eq_im MODE_IX1p_and_IMM1 i2 = true → MODE_IX1p_and_IMM1 = i2.
318 #i2; ncases i2; nnormalize;
319 ##[ ##29: #H; napply refl_eq
320 ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
321 ##| ##*: #H; napply (bool_destruct … H)
325 nlemma eqim_to_eq30 : ∀i2.eq_im MODE_SP1_and_IMM1 i2 = true → MODE_SP1_and_IMM1 = i2.
326 #i2; ncases i2; nnormalize;
327 ##[ ##30: #H; napply refl_eq
328 ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
329 ##| ##*: #H; napply (bool_destruct … H)
333 nlemma eqim_to_eq31 : ∀n1,i2.eq_im (MODE_DIRn n1) i2 = true → MODE_DIRn n1 = i2.
336 nchange in H:(%) with (eq_oct n1 n2 = true);
337 nrewrite > (eqoct_to_eq … H);
339 ##| ##32,33,34: nnormalize; #n2; #H; napply (bool_destruct … H)
340 ##| ##*: nnormalize; #H; napply (bool_destruct … H)
344 nlemma eqim_to_eq32 : ∀n1,i2.eq_im (MODE_DIRn_and_IMM1 n1) i2 = true → MODE_DIRn_and_IMM1 n1 = i2.
347 nchange in H:(%) with (eq_oct n1 n2 = true);
348 nrewrite > (eqoct_to_eq … H);
350 ##| ##31,33,34: nnormalize; #n2; #H; napply (bool_destruct … H)
351 ##| ##*: nnormalize; #H; napply (bool_destruct … H)
355 nlemma eqim_to_eq33 : ∀n1,i2.eq_im (MODE_TNY n1) i2 = true → MODE_TNY n1 = i2.
358 nchange in H:(%) with (eq_ex n1 n2 = true);
359 nrewrite > (eqex_to_eq … H);
361 ##| ##31,32,34: nnormalize; #n2; #H; napply (bool_destruct … H)
362 ##| ##*: nnormalize; #H; napply (bool_destruct … H)
366 nlemma eqim_to_eq34 : ∀n1,i2.eq_im (MODE_SRT n1) i2 = true → MODE_SRT n1 = i2.
369 nchange in H:(%) with (eq_bit n1 n2 = true);
370 nrewrite > (eqbit_to_eq … H);
372 ##| ##31,32,33: nnormalize; #n2; #H; napply (bool_destruct … H)
373 ##| ##*: nnormalize; #H; napply (bool_destruct … H)
377 nlemma eqim_to_eq : ∀i1,i2.eq_im i1 i2 = true → i1 = i2.
379 ##[ ##1: napply eqim_to_eq1 ##| ##2: napply eqim_to_eq2
380 ##| ##3: napply eqim_to_eq3 ##| ##4: napply eqim_to_eq4
381 ##| ##5: napply eqim_to_eq5 ##| ##6: napply eqim_to_eq6
382 ##| ##7: napply eqim_to_eq7 ##| ##8: napply eqim_to_eq8
383 ##| ##9: napply eqim_to_eq9 ##| ##10: napply eqim_to_eq10
384 ##| ##11: napply eqim_to_eq11 ##| ##12: napply eqim_to_eq12
385 ##| ##13: napply eqim_to_eq13 ##| ##14: napply eqim_to_eq14
386 ##| ##15: napply eqim_to_eq15 ##| ##16: napply eqim_to_eq16
387 ##| ##17: napply eqim_to_eq17 ##| ##18: napply eqim_to_eq18
388 ##| ##19: napply eqim_to_eq19 ##| ##20: napply eqim_to_eq20
389 ##| ##21: napply eqim_to_eq21 ##| ##22: napply eqim_to_eq22
390 ##| ##23: napply eqim_to_eq23 ##| ##24: napply eqim_to_eq24
391 ##| ##25: napply eqim_to_eq25 ##| ##26: napply eqim_to_eq26
392 ##| ##27: napply eqim_to_eq27 ##| ##28: napply eqim_to_eq28
393 ##| ##29: napply eqim_to_eq29 ##| ##30: napply eqim_to_eq30
394 ##| ##31: napply eqim_to_eq31 ##| ##32: napply eqim_to_eq32
395 ##| ##33: napply eqim_to_eq33 ##| ##34: napply eqim_to_eq34
399 nlemma eq_to_eqim1 : ∀i2.MODE_INH = i2 → eq_im MODE_INH i2 = true.
400 #t2; ncases t2; nnormalize;
401 ##[ ##1: #H; napply refl_eq
402 ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct … H)
403 ##| ##*: #H; napply (instr_mode_destruct … H)
407 nlemma eq_to_eqim2 : ∀i2.MODE_INHA = i2 → eq_im MODE_INHA i2 = true.
408 #t2; ncases t2; nnormalize;
409 ##[ ##2: #H; napply refl_eq
410 ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct … H)
411 ##| ##*: #H; napply (instr_mode_destruct … H)
415 nlemma eq_to_eqim3 : ∀i2.MODE_INHX = i2 → eq_im MODE_INHX i2 = true.
416 #t2; ncases t2; nnormalize;
417 ##[ ##3: #H; napply refl_eq
418 ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct … H)
419 ##| ##*: #H; napply (instr_mode_destruct … H)
423 nlemma eq_to_eqim4 : ∀i2.MODE_INHH = i2 → eq_im MODE_INHH i2 = true.
424 #t2; ncases t2; nnormalize;
425 ##[ ##4: #H; napply refl_eq
426 ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct … H)
427 ##| ##*: #H; napply (instr_mode_destruct … H)
431 nlemma eq_to_eqim5 : ∀i2.MODE_INHX0ADD = i2 → eq_im MODE_INHX0ADD i2 = true.
432 #t2; ncases t2; nnormalize;
433 ##[ ##5: #H; napply refl_eq
434 ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct … H)
435 ##| ##*: #H; napply (instr_mode_destruct … H)
439 nlemma eq_to_eqim6 : ∀i2.MODE_INHX1ADD = i2 → eq_im MODE_INHX1ADD i2 = true.
440 #t2; ncases t2; nnormalize;
441 ##[ ##6: #H; napply refl_eq
442 ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct … H)
443 ##| ##*: #H; napply (instr_mode_destruct … H)
447 nlemma eq_to_eqim7 : ∀i2.MODE_INHX2ADD = i2 → eq_im MODE_INHX2ADD i2 = true.
448 #t2; ncases t2; nnormalize;
449 ##[ ##7: #H; napply refl_eq
450 ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct … H)
451 ##| ##*: #H; napply (instr_mode_destruct … H)
455 nlemma eq_to_eqim8 : ∀i2.MODE_IMM1 = i2 → eq_im MODE_IMM1 i2 = true.
456 #t2; ncases t2; nnormalize;
457 ##[ ##8: #H; napply refl_eq
458 ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct … H)
459 ##| ##*: #H; napply (instr_mode_destruct … H)
463 nlemma eq_to_eqim9 : ∀i2.MODE_IMM1EXT = i2 → eq_im MODE_IMM1EXT i2 = true.
464 #t2; ncases t2; nnormalize;
465 ##[ ##9: #H; napply refl_eq
466 ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct … H)
467 ##| ##*: #H; napply (instr_mode_destruct … H)
471 nlemma eq_to_eqim10 : ∀i2.MODE_IMM2 = i2 → eq_im MODE_IMM2 i2 = true.
472 #t2; ncases t2; nnormalize;
473 ##[ ##10: #H; napply refl_eq
474 ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct … H)
475 ##| ##*: #H; napply (instr_mode_destruct … H)
479 nlemma eq_to_eqim11 : ∀i2.MODE_DIR1 = i2 → eq_im MODE_DIR1 i2 = true.
480 #t2; ncases t2; nnormalize;
481 ##[ ##11: #H; napply refl_eq
482 ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct … H)
483 ##| ##*: #H; napply (instr_mode_destruct … H)
487 nlemma eq_to_eqim12 : ∀i2.MODE_DIR2 = i2 → eq_im MODE_DIR2 i2 = true.
488 #t2; ncases t2; nnormalize;
489 ##[ ##12: #H; napply refl_eq
490 ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct … H)
491 ##| ##*: #H; napply (instr_mode_destruct … H)
495 nlemma eq_to_eqim13 : ∀i2.MODE_IX0 = i2 → eq_im MODE_IX0 i2 = true.
496 #t2; ncases t2; nnormalize;
497 ##[ ##13: #H; napply refl_eq
498 ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct … H)
499 ##| ##*: #H; napply (instr_mode_destruct … H)
503 nlemma eq_to_eqim14 : ∀i2.MODE_IX1 = i2 → eq_im MODE_IX1 i2 = true.
504 #t2; ncases t2; nnormalize;
505 ##[ ##14: #H; napply refl_eq
506 ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct … H)
507 ##| ##*: #H; napply (instr_mode_destruct … H)
511 nlemma eq_to_eqim15 : ∀i2.MODE_IX2 = i2 → eq_im MODE_IX2 i2 = true.
512 #t2; ncases t2; nnormalize;
513 ##[ ##15: #H; napply refl_eq
514 ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct … H)
515 ##| ##*: #H; napply (instr_mode_destruct … H)
519 nlemma eq_to_eqim16 : ∀i2.MODE_SP1 = i2 → eq_im MODE_SP1 i2 = true.
520 #t2; ncases t2; nnormalize;
521 ##[ ##16: #H; napply refl_eq
522 ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct … H)
523 ##| ##*: #H; napply (instr_mode_destruct … H)
527 nlemma eq_to_eqim17 : ∀i2.MODE_SP2 = i2 → eq_im MODE_SP2 i2 = true.
528 #t2; ncases t2; nnormalize;
529 ##[ ##17: #H; napply refl_eq
530 ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct … H)
531 ##| ##*: #H; napply (instr_mode_destruct … H)
535 nlemma eq_to_eqim18 : ∀i2.MODE_DIR1_to_DIR1 = i2 → eq_im MODE_DIR1_to_DIR1 i2 = true.
536 #t2; ncases t2; nnormalize;
537 ##[ ##18: #H; napply refl_eq
538 ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct … H)
539 ##| ##*: #H; napply (instr_mode_destruct … H)
543 nlemma eq_to_eqim19 : ∀i2.MODE_IMM1_to_DIR1 = i2 → eq_im MODE_IMM1_to_DIR1 i2 = true.
544 #t2; ncases t2; nnormalize;
545 ##[ ##19: #H; napply refl_eq
546 ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct … H)
547 ##| ##*: #H; napply (instr_mode_destruct … H)
551 nlemma eq_to_eqim20 : ∀i2.MODE_IX0p_to_DIR1 = i2 → eq_im MODE_IX0p_to_DIR1 i2 = true.
552 #t2; ncases t2; nnormalize;
553 ##[ ##20: #H; napply refl_eq
554 ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct … H)
555 ##| ##*: #H; napply (instr_mode_destruct … H)
559 nlemma eq_to_eqim21 : ∀i2.MODE_DIR1_to_IX0p = i2 → eq_im MODE_DIR1_to_IX0p i2 = true.
560 #t2; ncases t2; nnormalize;
561 ##[ ##21: #H; napply refl_eq
562 ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct … H)
563 ##| ##*: #H; napply (instr_mode_destruct … H)
567 nlemma eq_to_eqim22 : ∀i2.MODE_INHA_and_IMM1 = i2 → eq_im MODE_INHA_and_IMM1 i2 = true.
568 #t2; ncases t2; nnormalize;
569 ##[ ##22: #H; napply refl_eq
570 ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct … H)
571 ##| ##*: #H; napply (instr_mode_destruct … H)
575 nlemma eq_to_eqim23 : ∀i2.MODE_INHX_and_IMM1 = i2 → eq_im MODE_INHX_and_IMM1 i2 = true.
576 #t2; ncases t2; nnormalize;
577 ##[ ##23: #H; napply refl_eq
578 ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct … H)
579 ##| ##*: #H; napply (instr_mode_destruct … H)
583 nlemma eq_to_eqim24 : ∀i2.MODE_IMM1_and_IMM1 = i2 → eq_im MODE_IMM1_and_IMM1 i2 = true.
584 #t2; ncases t2; nnormalize;
585 ##[ ##24: #H; napply refl_eq
586 ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct … H)
587 ##| ##*: #H; napply (instr_mode_destruct … H)
591 nlemma eq_to_eqim25 : ∀i2.MODE_DIR1_and_IMM1 = i2 → eq_im MODE_DIR1_and_IMM1 i2 = true.
592 #t2; ncases t2; nnormalize;
593 ##[ ##25: #H; napply refl_eq
594 ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct … H)
595 ##| ##*: #H; napply (instr_mode_destruct … H)
599 nlemma eq_to_eqim26 : ∀i2.MODE_IX0_and_IMM1 = i2 → eq_im MODE_IX0_and_IMM1 i2 = true.
600 #t2; ncases t2; nnormalize;
601 ##[ ##26: #H; napply refl_eq
602 ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct … H)
603 ##| ##*: #H; napply (instr_mode_destruct … H)
607 nlemma eq_to_eqim27 : ∀i2.MODE_IX0p_and_IMM1 = i2 → eq_im MODE_IX0p_and_IMM1 i2 = true.
608 #t2; ncases t2; nnormalize;
609 ##[ ##27: #H; napply refl_eq
610 ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct … H)
611 ##| ##*: #H; napply (instr_mode_destruct … H)
615 nlemma eq_to_eqim28 : ∀i2.MODE_IX1_and_IMM1 = i2 → eq_im MODE_IX1_and_IMM1 i2 = true.
616 #t2; ncases t2; nnormalize;
617 ##[ ##28: #H; napply refl_eq
618 ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct … H)
619 ##| ##*: #H; napply (instr_mode_destruct … H)
623 nlemma eq_to_eqim29 : ∀i2.MODE_IX1p_and_IMM1 = i2 → eq_im MODE_IX1p_and_IMM1 i2 = true.
624 #t2; ncases t2; nnormalize;
625 ##[ ##29: #H; napply refl_eq
626 ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct … H)
627 ##| ##*: #H; napply (instr_mode_destruct … H)
631 nlemma eq_to_eqim30 : ∀i2.MODE_SP1_and_IMM1 = i2 → eq_im MODE_SP1_and_IMM1 i2 = true.
632 #t2; ncases t2; nnormalize;
633 ##[ ##30: #H; napply refl_eq
634 ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct … H)
635 ##| ##*: #H; napply (instr_mode_destruct … H)
639 nlemma eq_to_eqim31 : ∀n1,i2.MODE_DIRn n1 = i2 → eq_im (MODE_DIRn n1) i2 = true.
642 nchange with (eq_oct n1 n2 = true);
643 nrewrite > (instr_mode_destruct_MODE_DIRn … H);
644 nrewrite > (eq_to_eqoct n2 n2 (refl_eq …));
646 ##| ##32,33,34: #n; #H; nnormalize; napply (instr_mode_destruct … H)
647 ##| ##*: #H; nnormalize; napply (instr_mode_destruct … H)
651 nlemma eq_to_eqim32 : ∀n1,i2.MODE_DIRn_and_IMM1 n1 = i2 → eq_im (MODE_DIRn_and_IMM1 n1) i2 = true.
654 nchange with (eq_oct n1 n2 = true);
655 nrewrite > (instr_mode_destruct_MODE_DIRn_and_IMM1 … H);
656 nrewrite > (eq_to_eqoct n2 n2 (refl_eq …));
658 ##| ##31,33,34: #n; #H; nnormalize; napply (instr_mode_destruct … H)
659 ##| ##*: #H; nnormalize; napply (instr_mode_destruct … H)
663 nlemma eq_to_eqim33 : ∀n1,i2.MODE_TNY n1 = i2 → eq_im (MODE_TNY n1) i2 = true.
666 nchange with (eq_ex n1 n2 = true);
667 nrewrite > (instr_mode_destruct_MODE_TNY … H);
668 nrewrite > (eq_to_eqex n2 n2 (refl_eq …));
670 ##| ##31,32,34: #n; #H; nnormalize; napply (instr_mode_destruct … H)
671 ##| ##*: #H; nnormalize; napply (instr_mode_destruct … H)
675 nlemma eq_to_eqim34 : ∀n1,i2.MODE_SRT n1 = i2 → eq_im (MODE_SRT n1) i2 = true.
678 nchange with (eq_bit n1 n2 = true);
679 nrewrite > (instr_mode_destruct_MODE_SRT … H);
680 nrewrite > (eq_to_eqbit n2 n2 (refl_eq …));
682 ##| ##31,32,33: #n; #H; nnormalize; napply (instr_mode_destruct … H)
683 ##| ##*: #H; nnormalize; napply (instr_mode_destruct … H)
687 nlemma eq_to_eqim : ∀i1,i2.i1 = i2 → eq_im i1 i2 = true.
689 ##[ ##1: napply eq_to_eqim1 ##| ##2: napply eq_to_eqim2
690 ##| ##3: napply eq_to_eqim3 ##| ##4: napply eq_to_eqim4
691 ##| ##5: napply eq_to_eqim5 ##| ##6: napply eq_to_eqim6
692 ##| ##7: napply eq_to_eqim7 ##| ##8: napply eq_to_eqim8
693 ##| ##9: napply eq_to_eqim9 ##| ##10: napply eq_to_eqim10
694 ##| ##11: napply eq_to_eqim11 ##| ##12: napply eq_to_eqim12
695 ##| ##13: napply eq_to_eqim13 ##| ##14: napply eq_to_eqim14
696 ##| ##15: napply eq_to_eqim15 ##| ##16: napply eq_to_eqim16
697 ##| ##17: napply eq_to_eqim17 ##| ##18: napply eq_to_eqim18
698 ##| ##19: napply eq_to_eqim19 ##| ##20: napply eq_to_eqim20
699 ##| ##21: napply eq_to_eqim21 ##| ##22: napply eq_to_eqim22
700 ##| ##23: napply eq_to_eqim23 ##| ##24: napply eq_to_eqim24
701 ##| ##25: napply eq_to_eqim25 ##| ##26: napply eq_to_eqim26
702 ##| ##27: napply eq_to_eqim27 ##| ##28: napply eq_to_eqim28
703 ##| ##29: napply eq_to_eqim29 ##| ##30: napply eq_to_eqim30
704 ##| ##31: napply eq_to_eqim31 ##| ##32: napply eq_to_eqim32
705 ##| ##33: napply eq_to_eqim33 ##| ##34: napply eq_to_eqim34