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: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
19 (* Ultima modifica: 05/08/2009 *)
21 (* ********************************************************************** *)
23 include "num/oct_lemmas.ma".
24 include "num/bitrigesim_lemmas.ma".
25 include "num/exadecim_lemmas.ma".
26 include "freescale/opcode_base.ma".
28 (* ********************************************** *)
29 (* MATTONI BASE PER DEFINIRE LE TABELLE DELLE MCU *)
30 (* ********************************************** *)
32 nlemma instrmode_destruct_MODE_DIRn : ∀n1,n2.MODE_DIRn n1 = MODE_DIRn n2 → n1 = n2.
34 nchange with (match MODE_DIRn n2 with [ MODE_DIRn a ⇒ n1 = a | _ ⇒ False ]);
40 nlemma instrmode_destruct_MODE_DIRn_and_IMM1 : ∀n1,n2.MODE_DIRn_and_IMM1 n1 = MODE_DIRn_and_IMM1 n2 → n1 = n2.
42 nchange with (match MODE_DIRn_and_IMM1 n2 with [ MODE_DIRn_and_IMM1 a ⇒ n1 = a | _ ⇒ False ]);
48 nlemma instrmode_destruct_MODE_TNY : ∀e1,e2.MODE_TNY e1 = MODE_TNY e2 → e1 = e2.
50 nchange with (match MODE_TNY e2 with [ MODE_TNY a ⇒ e1 = a | _ ⇒ False ]);
56 nlemma instrmode_destruct_MODE_SRT : ∀t1,t2.MODE_SRT t1 = MODE_SRT t2 → t1 = t2.
58 nchange with (match MODE_SRT t2 with [ MODE_SRT a ⇒ t1 = a | _ ⇒ False ]);
64 ndefinition instrmode_destruct_aux ≝
65 Πi1,i2.ΠP:Prop.i1 = i2 →
66 match eq_im i1 i2 with [ true ⇒ P → P | false ⇒ P ].
68 ndefinition instrmode_destruct : instrmode_destruct_aux.
73 ##[ ##31,32,33,34: #sub; nelim sub; nnormalize ##]
77 nlemma symmetric_eqim : symmetricT instr_mode bool eq_im.
80 ##[ ##1: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
81 ##| ##2: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
82 ##| ##3: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
83 ##| ##4: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
84 ##| ##5: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
85 ##| ##6: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
86 ##| ##7: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
87 ##| ##8: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
88 ##| ##9: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
89 ##| ##10: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
90 ##| ##11: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
91 ##| ##12: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
92 ##| ##13: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
93 ##| ##14: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
94 ##| ##15: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
95 ##| ##16: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
96 ##| ##17: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
97 ##| ##18: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
98 ##| ##19: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
99 ##| ##20: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
100 ##| ##21: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
101 ##| ##22: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
102 ##| ##23: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
103 ##| ##24: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
104 ##| ##25: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
105 ##| ##26: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
106 ##| ##27: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
107 ##| ##28: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
108 ##| ##29: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
109 ##| ##30: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
110 ##| ##31: ncases i2; #n1;
112 nchange with (eq_oct n2 n1 = eq_oct n1 n2);
113 nrewrite > (symmetric_eqoct n1 n2);
114 ##| ##32,33,34: #n2; nnormalize
116 nnormalize; napply refl_eq
117 ##| ##32: ncases i2; #n1;
119 nchange with (eq_oct n2 n1 = eq_oct n1 n2);
120 nrewrite > (symmetric_eqoct n1 n2);
121 ##| ##31,33,34: #n2; nnormalize
123 nnormalize; napply refl_eq
124 ##| ##33: ncases i2; #n1;
126 nchange with (eq_ex n2 n1 = eq_ex n1 n2);
127 nrewrite > (symmetric_eqex n1 n2);
128 ##| ##31,32,34: #n2; nnormalize
130 nnormalize; napply refl_eq
131 ##| ##34: ncases i2; #n1;
133 nchange with (eq_bit n2 n1 = eq_bit n1 n2);
134 nrewrite > (symmetric_eqbit n1 n2);
135 ##| ##31,32,33: #n2; nnormalize
137 nnormalize; napply refl_eq
141 nlemma eqim_to_eq1 : ∀i2.eq_im MODE_INH i2 = true → MODE_INH = i2.
142 #i2; ncases i2; nnormalize;
143 ##[ ##1: #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_eq2 : ∀i2.eq_im MODE_INHA i2 = true → MODE_INHA = i2.
150 #i2; ncases i2; nnormalize;
151 ##[ ##2: #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_eq3 : ∀i2.eq_im MODE_INHX i2 = true → MODE_INHX = i2.
158 #i2; ncases i2; nnormalize;
159 ##[ ##3: #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_eq4 : ∀i2.eq_im MODE_INHH i2 = true → MODE_INHH = i2.
166 #i2; ncases i2; nnormalize;
167 ##[ ##4: #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_eq5 : ∀i2.eq_im MODE_INHX0ADD i2 = true → MODE_INHX0ADD = i2.
174 #i2; ncases i2; nnormalize;
175 ##[ ##5: #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_eq6 : ∀i2.eq_im MODE_INHX1ADD i2 = true → MODE_INHX1ADD = i2.
182 #i2; ncases i2; nnormalize;
183 ##[ ##6: #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_eq7 : ∀i2.eq_im MODE_INHX2ADD i2 = true → MODE_INHX2ADD = i2.
190 #i2; ncases i2; nnormalize;
191 ##[ ##7: #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_eq8 : ∀i2.eq_im MODE_IMM1 i2 = true → MODE_IMM1 = i2.
198 #i2; ncases i2; nnormalize;
199 ##[ ##8: #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_eq9 : ∀i2.eq_im MODE_IMM1EXT i2 = true → MODE_IMM1EXT = i2.
206 #i2; ncases i2; nnormalize;
207 ##[ ##9: #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_eq10 : ∀i2.eq_im MODE_IMM2 i2 = true → MODE_IMM2 = i2.
214 #i2; ncases i2; nnormalize;
215 ##[ ##10: #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_eq11 : ∀i2.eq_im MODE_DIR1 i2 = true → MODE_DIR1 = i2.
222 #i2; ncases i2; nnormalize;
223 ##[ ##11: #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_eq12 : ∀i2.eq_im MODE_DIR2 i2 = true → MODE_DIR2 = i2.
230 #i2; ncases i2; nnormalize;
231 ##[ ##12: #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_eq13 : ∀i2.eq_im MODE_IX0 i2 = true → MODE_IX0 = i2.
238 #i2; ncases i2; nnormalize;
239 ##[ ##13: #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_eq14 : ∀i2.eq_im MODE_IX1 i2 = true → MODE_IX1 = i2.
246 #i2; ncases i2; nnormalize;
247 ##[ ##14: #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_eq15 : ∀i2.eq_im MODE_IX2 i2 = true → MODE_IX2 = i2.
254 #i2; ncases i2; nnormalize;
255 ##[ ##15: #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_eq16 : ∀i2.eq_im MODE_SP1 i2 = true → MODE_SP1 = i2.
262 #i2; ncases i2; nnormalize;
263 ##[ ##16: #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_eq17 : ∀i2.eq_im MODE_SP2 i2 = true → MODE_SP2 = i2.
270 #i2; ncases i2; nnormalize;
271 ##[ ##17: #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_eq18 : ∀i2.eq_im MODE_DIR1_to_DIR1 i2 = true → MODE_DIR1_to_DIR1 = i2.
278 #i2; ncases i2; nnormalize;
279 ##[ ##18: #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_eq19 : ∀i2.eq_im MODE_IMM1_to_DIR1 i2 = true → MODE_IMM1_to_DIR1 = i2.
286 #i2; ncases i2; nnormalize;
287 ##[ ##19: #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_eq20 : ∀i2.eq_im MODE_IX0p_to_DIR1 i2 = true → MODE_IX0p_to_DIR1 = i2.
294 #i2; ncases i2; nnormalize;
295 ##[ ##20: #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_eq21 : ∀i2.eq_im MODE_DIR1_to_IX0p i2 = true → MODE_DIR1_to_IX0p = i2.
302 #i2; ncases i2; nnormalize;
303 ##[ ##21: #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_eq22 : ∀i2.eq_im MODE_INHA_and_IMM1 i2 = true → MODE_INHA_and_IMM1 = i2.
310 #i2; ncases i2; nnormalize;
311 ##[ ##22: #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_eq23 : ∀i2.eq_im MODE_INHX_and_IMM1 i2 = true → MODE_INHX_and_IMM1 = i2.
318 #i2; ncases i2; nnormalize;
319 ##[ ##23: #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_eq24 : ∀i2.eq_im MODE_IMM1_and_IMM1 i2 = true → MODE_IMM1_and_IMM1 = i2.
326 #i2; ncases i2; nnormalize;
327 ##[ ##24: #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_eq25 : ∀i2.eq_im MODE_DIR1_and_IMM1 i2 = true → MODE_DIR1_and_IMM1 = i2.
334 #i2; ncases i2; nnormalize;
335 ##[ ##25: #H; napply refl_eq
336 ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
337 ##| ##*: #H; napply (bool_destruct … H)
341 nlemma eqim_to_eq26 : ∀i2.eq_im MODE_IX0_and_IMM1 i2 = true → MODE_IX0_and_IMM1 = i2.
342 #i2; ncases i2; nnormalize;
343 ##[ ##26: #H; napply refl_eq
344 ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
345 ##| ##*: #H; napply (bool_destruct … H)
349 nlemma eqim_to_eq27 : ∀i2.eq_im MODE_IX0p_and_IMM1 i2 = true → MODE_IX0p_and_IMM1 = i2.
350 #i2; ncases i2; nnormalize;
351 ##[ ##27: #H; napply refl_eq
352 ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
353 ##| ##*: #H; napply (bool_destruct … H)
357 nlemma eqim_to_eq28 : ∀i2.eq_im MODE_IX1_and_IMM1 i2 = true → MODE_IX1_and_IMM1 = i2.
358 #i2; ncases i2; nnormalize;
359 ##[ ##28: #H; napply refl_eq
360 ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
361 ##| ##*: #H; napply (bool_destruct … H)
365 nlemma eqim_to_eq29 : ∀i2.eq_im MODE_IX1p_and_IMM1 i2 = true → MODE_IX1p_and_IMM1 = i2.
366 #i2; ncases i2; nnormalize;
367 ##[ ##29: #H; napply refl_eq
368 ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
369 ##| ##*: #H; napply (bool_destruct … H)
373 nlemma eqim_to_eq30 : ∀i2.eq_im MODE_SP1_and_IMM1 i2 = true → MODE_SP1_and_IMM1 = i2.
374 #i2; ncases i2; nnormalize;
375 ##[ ##30: #H; napply refl_eq
376 ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
377 ##| ##*: #H; napply (bool_destruct … H)
381 nlemma eqim_to_eq31 : ∀n1,i2.eq_im (MODE_DIRn n1) i2 = true → MODE_DIRn n1 = i2.
384 nchange in H:(%) with (eq_oct n1 n2 = true);
385 nrewrite > (eqoct_to_eq … H);
387 ##| ##32,33,34: nnormalize; #n2; #H; napply (bool_destruct … H)
388 ##| ##*: nnormalize; #H; napply (bool_destruct … H)
392 nlemma eqim_to_eq32 : ∀n1,i2.eq_im (MODE_DIRn_and_IMM1 n1) i2 = true → MODE_DIRn_and_IMM1 n1 = i2.
395 nchange in H:(%) with (eq_oct n1 n2 = true);
396 nrewrite > (eqoct_to_eq … H);
398 ##| ##31,33,34: nnormalize; #n2; #H; napply (bool_destruct … H)
399 ##| ##*: nnormalize; #H; napply (bool_destruct … H)
403 nlemma eqim_to_eq33 : ∀n1,i2.eq_im (MODE_TNY n1) i2 = true → MODE_TNY n1 = i2.
406 nchange in H:(%) with (eq_ex n1 n2 = true);
407 nrewrite > (eqex_to_eq … H);
409 ##| ##31,32,34: nnormalize; #n2; #H; napply (bool_destruct … H)
410 ##| ##*: nnormalize; #H; napply (bool_destruct … H)
414 nlemma eqim_to_eq34 : ∀n1,i2.eq_im (MODE_SRT n1) i2 = true → MODE_SRT n1 = i2.
417 nchange in H:(%) with (eq_bit n1 n2 = true);
418 nrewrite > (eqbit_to_eq … H);
420 ##| ##31,32,33: nnormalize; #n2; #H; napply (bool_destruct … H)
421 ##| ##*: nnormalize; #H; napply (bool_destruct … H)
425 nlemma eqim_to_eq : ∀i1,i2.eq_im i1 i2 = true → i1 = i2.
427 ##[ ##1: napply eqim_to_eq1 ##| ##2: napply eqim_to_eq2
428 ##| ##3: napply eqim_to_eq3 ##| ##4: napply eqim_to_eq4
429 ##| ##5: napply eqim_to_eq5 ##| ##6: napply eqim_to_eq6
430 ##| ##7: napply eqim_to_eq7 ##| ##8: napply eqim_to_eq8
431 ##| ##9: napply eqim_to_eq9 ##| ##10: napply eqim_to_eq10
432 ##| ##11: napply eqim_to_eq11 ##| ##12: napply eqim_to_eq12
433 ##| ##13: napply eqim_to_eq13 ##| ##14: napply eqim_to_eq14
434 ##| ##15: napply eqim_to_eq15 ##| ##16: napply eqim_to_eq16
435 ##| ##17: napply eqim_to_eq17 ##| ##18: napply eqim_to_eq18
436 ##| ##19: napply eqim_to_eq19 ##| ##20: napply eqim_to_eq20
437 ##| ##21: napply eqim_to_eq21 ##| ##22: napply eqim_to_eq22
438 ##| ##23: napply eqim_to_eq23 ##| ##24: napply eqim_to_eq24
439 ##| ##25: napply eqim_to_eq25 ##| ##26: napply eqim_to_eq26
440 ##| ##27: napply eqim_to_eq27 ##| ##28: napply eqim_to_eq28
441 ##| ##29: napply eqim_to_eq29 ##| ##30: napply eqim_to_eq30
442 ##| ##31: napply eqim_to_eq31 ##| ##32: napply eqim_to_eq32
443 ##| ##33: napply eqim_to_eq33 ##| ##34: napply eqim_to_eq34
447 nlemma eq_to_eqim1 : ∀i2.MODE_INH = i2 → eq_im MODE_INH i2 = true.
448 #t2; ncases t2; nnormalize;
449 ##[ ##1: #H; napply refl_eq
450 ##| ##31,32,33,34: #n; #H; napply (instrmode_destruct … H)
451 ##| ##*: #H; napply (instrmode_destruct … H)
455 nlemma eq_to_eqim2 : ∀i2.MODE_INHA = i2 → eq_im MODE_INHA i2 = true.
456 #t2; ncases t2; nnormalize;
457 ##[ ##2: #H; napply refl_eq
458 ##| ##31,32,33,34: #n; #H; napply (instrmode_destruct … H)
459 ##| ##*: #H; napply (instrmode_destruct … H)
463 nlemma eq_to_eqim3 : ∀i2.MODE_INHX = i2 → eq_im MODE_INHX i2 = true.
464 #t2; ncases t2; nnormalize;
465 ##[ ##3: #H; napply refl_eq
466 ##| ##31,32,33,34: #n; #H; napply (instrmode_destruct … H)
467 ##| ##*: #H; napply (instrmode_destruct … H)
471 nlemma eq_to_eqim4 : ∀i2.MODE_INHH = i2 → eq_im MODE_INHH i2 = true.
472 #t2; ncases t2; nnormalize;
473 ##[ ##4: #H; napply refl_eq
474 ##| ##31,32,33,34: #n; #H; napply (instrmode_destruct … H)
475 ##| ##*: #H; napply (instrmode_destruct … H)
479 nlemma eq_to_eqim5 : ∀i2.MODE_INHX0ADD = i2 → eq_im MODE_INHX0ADD i2 = true.
480 #t2; ncases t2; nnormalize;
481 ##[ ##5: #H; napply refl_eq
482 ##| ##31,32,33,34: #n; #H; napply (instrmode_destruct … H)
483 ##| ##*: #H; napply (instrmode_destruct … H)
487 nlemma eq_to_eqim6 : ∀i2.MODE_INHX1ADD = i2 → eq_im MODE_INHX1ADD i2 = true.
488 #t2; ncases t2; nnormalize;
489 ##[ ##6: #H; napply refl_eq
490 ##| ##31,32,33,34: #n; #H; napply (instrmode_destruct … H)
491 ##| ##*: #H; napply (instrmode_destruct … H)
495 nlemma eq_to_eqim7 : ∀i2.MODE_INHX2ADD = i2 → eq_im MODE_INHX2ADD i2 = true.
496 #t2; ncases t2; nnormalize;
497 ##[ ##7: #H; napply refl_eq
498 ##| ##31,32,33,34: #n; #H; napply (instrmode_destruct … H)
499 ##| ##*: #H; napply (instrmode_destruct … H)
503 nlemma eq_to_eqim8 : ∀i2.MODE_IMM1 = i2 → eq_im MODE_IMM1 i2 = true.
504 #t2; ncases t2; nnormalize;
505 ##[ ##8: #H; napply refl_eq
506 ##| ##31,32,33,34: #n; #H; napply (instrmode_destruct … H)
507 ##| ##*: #H; napply (instrmode_destruct … H)
511 nlemma eq_to_eqim9 : ∀i2.MODE_IMM1EXT = i2 → eq_im MODE_IMM1EXT i2 = true.
512 #t2; ncases t2; nnormalize;
513 ##[ ##9: #H; napply refl_eq
514 ##| ##31,32,33,34: #n; #H; napply (instrmode_destruct … H)
515 ##| ##*: #H; napply (instrmode_destruct … H)
519 nlemma eq_to_eqim10 : ∀i2.MODE_IMM2 = i2 → eq_im MODE_IMM2 i2 = true.
520 #t2; ncases t2; nnormalize;
521 ##[ ##10: #H; napply refl_eq
522 ##| ##31,32,33,34: #n; #H; napply (instrmode_destruct … H)
523 ##| ##*: #H; napply (instrmode_destruct … H)
527 nlemma eq_to_eqim11 : ∀i2.MODE_DIR1 = i2 → eq_im MODE_DIR1 i2 = true.
528 #t2; ncases t2; nnormalize;
529 ##[ ##11: #H; napply refl_eq
530 ##| ##31,32,33,34: #n; #H; napply (instrmode_destruct … H)
531 ##| ##*: #H; napply (instrmode_destruct … H)
535 nlemma eq_to_eqim12 : ∀i2.MODE_DIR2 = i2 → eq_im MODE_DIR2 i2 = true.
536 #t2; ncases t2; nnormalize;
537 ##[ ##12: #H; napply refl_eq
538 ##| ##31,32,33,34: #n; #H; napply (instrmode_destruct … H)
539 ##| ##*: #H; napply (instrmode_destruct … H)
543 nlemma eq_to_eqim13 : ∀i2.MODE_IX0 = i2 → eq_im MODE_IX0 i2 = true.
544 #t2; ncases t2; nnormalize;
545 ##[ ##13: #H; napply refl_eq
546 ##| ##31,32,33,34: #n; #H; napply (instrmode_destruct … H)
547 ##| ##*: #H; napply (instrmode_destruct … H)
551 nlemma eq_to_eqim14 : ∀i2.MODE_IX1 = i2 → eq_im MODE_IX1 i2 = true.
552 #t2; ncases t2; nnormalize;
553 ##[ ##14: #H; napply refl_eq
554 ##| ##31,32,33,34: #n; #H; napply (instrmode_destruct … H)
555 ##| ##*: #H; napply (instrmode_destruct … H)
559 nlemma eq_to_eqim15 : ∀i2.MODE_IX2 = i2 → eq_im MODE_IX2 i2 = true.
560 #t2; ncases t2; nnormalize;
561 ##[ ##15: #H; napply refl_eq
562 ##| ##31,32,33,34: #n; #H; napply (instrmode_destruct … H)
563 ##| ##*: #H; napply (instrmode_destruct … H)
567 nlemma eq_to_eqim16 : ∀i2.MODE_SP1 = i2 → eq_im MODE_SP1 i2 = true.
568 #t2; ncases t2; nnormalize;
569 ##[ ##16: #H; napply refl_eq
570 ##| ##31,32,33,34: #n; #H; napply (instrmode_destruct … H)
571 ##| ##*: #H; napply (instrmode_destruct … H)
575 nlemma eq_to_eqim17 : ∀i2.MODE_SP2 = i2 → eq_im MODE_SP2 i2 = true.
576 #t2; ncases t2; nnormalize;
577 ##[ ##17: #H; napply refl_eq
578 ##| ##31,32,33,34: #n; #H; napply (instrmode_destruct … H)
579 ##| ##*: #H; napply (instrmode_destruct … H)
583 nlemma eq_to_eqim18 : ∀i2.MODE_DIR1_to_DIR1 = i2 → eq_im MODE_DIR1_to_DIR1 i2 = true.
584 #t2; ncases t2; nnormalize;
585 ##[ ##18: #H; napply refl_eq
586 ##| ##31,32,33,34: #n; #H; napply (instrmode_destruct … H)
587 ##| ##*: #H; napply (instrmode_destruct … H)
591 nlemma eq_to_eqim19 : ∀i2.MODE_IMM1_to_DIR1 = i2 → eq_im MODE_IMM1_to_DIR1 i2 = true.
592 #t2; ncases t2; nnormalize;
593 ##[ ##19: #H; napply refl_eq
594 ##| ##31,32,33,34: #n; #H; napply (instrmode_destruct … H)
595 ##| ##*: #H; napply (instrmode_destruct … H)
599 nlemma eq_to_eqim20 : ∀i2.MODE_IX0p_to_DIR1 = i2 → eq_im MODE_IX0p_to_DIR1 i2 = true.
600 #t2; ncases t2; nnormalize;
601 ##[ ##20: #H; napply refl_eq
602 ##| ##31,32,33,34: #n; #H; napply (instrmode_destruct … H)
603 ##| ##*: #H; napply (instrmode_destruct … H)
607 nlemma eq_to_eqim21 : ∀i2.MODE_DIR1_to_IX0p = i2 → eq_im MODE_DIR1_to_IX0p i2 = true.
608 #t2; ncases t2; nnormalize;
609 ##[ ##21: #H; napply refl_eq
610 ##| ##31,32,33,34: #n; #H; napply (instrmode_destruct … H)
611 ##| ##*: #H; napply (instrmode_destruct … H)
615 nlemma eq_to_eqim22 : ∀i2.MODE_INHA_and_IMM1 = i2 → eq_im MODE_INHA_and_IMM1 i2 = true.
616 #t2; ncases t2; nnormalize;
617 ##[ ##22: #H; napply refl_eq
618 ##| ##31,32,33,34: #n; #H; napply (instrmode_destruct … H)
619 ##| ##*: #H; napply (instrmode_destruct … H)
623 nlemma eq_to_eqim23 : ∀i2.MODE_INHX_and_IMM1 = i2 → eq_im MODE_INHX_and_IMM1 i2 = true.
624 #t2; ncases t2; nnormalize;
625 ##[ ##23: #H; napply refl_eq
626 ##| ##31,32,33,34: #n; #H; napply (instrmode_destruct … H)
627 ##| ##*: #H; napply (instrmode_destruct … H)
631 nlemma eq_to_eqim24 : ∀i2.MODE_IMM1_and_IMM1 = i2 → eq_im MODE_IMM1_and_IMM1 i2 = true.
632 #t2; ncases t2; nnormalize;
633 ##[ ##24: #H; napply refl_eq
634 ##| ##31,32,33,34: #n; #H; napply (instrmode_destruct … H)
635 ##| ##*: #H; napply (instrmode_destruct … H)
639 nlemma eq_to_eqim25 : ∀i2.MODE_DIR1_and_IMM1 = i2 → eq_im MODE_DIR1_and_IMM1 i2 = true.
640 #t2; ncases t2; nnormalize;
641 ##[ ##25: #H; napply refl_eq
642 ##| ##31,32,33,34: #n; #H; napply (instrmode_destruct … H)
643 ##| ##*: #H; napply (instrmode_destruct … H)
647 nlemma eq_to_eqim26 : ∀i2.MODE_IX0_and_IMM1 = i2 → eq_im MODE_IX0_and_IMM1 i2 = true.
648 #t2; ncases t2; nnormalize;
649 ##[ ##26: #H; napply refl_eq
650 ##| ##31,32,33,34: #n; #H; napply (instrmode_destruct … H)
651 ##| ##*: #H; napply (instrmode_destruct … H)
655 nlemma eq_to_eqim27 : ∀i2.MODE_IX0p_and_IMM1 = i2 → eq_im MODE_IX0p_and_IMM1 i2 = true.
656 #t2; ncases t2; nnormalize;
657 ##[ ##27: #H; napply refl_eq
658 ##| ##31,32,33,34: #n; #H; napply (instrmode_destruct … H)
659 ##| ##*: #H; napply (instrmode_destruct … H)
663 nlemma eq_to_eqim28 : ∀i2.MODE_IX1_and_IMM1 = i2 → eq_im MODE_IX1_and_IMM1 i2 = true.
664 #t2; ncases t2; nnormalize;
665 ##[ ##28: #H; napply refl_eq
666 ##| ##31,32,33,34: #n; #H; napply (instrmode_destruct … H)
667 ##| ##*: #H; napply (instrmode_destruct … H)
671 nlemma eq_to_eqim29 : ∀i2.MODE_IX1p_and_IMM1 = i2 → eq_im MODE_IX1p_and_IMM1 i2 = true.
672 #t2; ncases t2; nnormalize;
673 ##[ ##29: #H; napply refl_eq
674 ##| ##31,32,33,34: #n; #H; napply (instrmode_destruct … H)
675 ##| ##*: #H; napply (instrmode_destruct … H)
679 nlemma eq_to_eqim30 : ∀i2.MODE_SP1_and_IMM1 = i2 → eq_im MODE_SP1_and_IMM1 i2 = true.
680 #t2; ncases t2; nnormalize;
681 ##[ ##30: #H; napply refl_eq
682 ##| ##31,32,33,34: #n; #H; napply (instrmode_destruct … H)
683 ##| ##*: #H; napply (instrmode_destruct … H)
687 nlemma eq_to_eqim31 : ∀n1,i2.MODE_DIRn n1 = i2 → eq_im (MODE_DIRn n1) i2 = true.
690 nchange with (eq_oct n1 n2 = true);
691 nrewrite > (instrmode_destruct_MODE_DIRn n1 n2 H);
692 nrewrite > (eq_to_eqoct n2 n2 (refl_eq …));
694 ##| ##32,33,34: #n; #H; nnormalize; napply (instrmode_destruct … H)
695 ##| ##*: #H; nnormalize; napply (instrmode_destruct … H)
699 nlemma eq_to_eqim32 : ∀n1,i2.MODE_DIRn_and_IMM1 n1 = i2 → eq_im (MODE_DIRn_and_IMM1 n1) i2 = true.
702 nchange with (eq_oct n1 n2 = true);
703 nrewrite > (instrmode_destruct_MODE_DIRn_and_IMM1 … H);
704 nrewrite > (eq_to_eqoct n2 n2 (refl_eq …));
706 ##| ##31,33,34: #n; #H; nnormalize; napply (instrmode_destruct … H)
707 ##| ##*: #H; nnormalize; napply (instrmode_destruct … H)
711 nlemma eq_to_eqim33 : ∀n1,i2.MODE_TNY n1 = i2 → eq_im (MODE_TNY n1) i2 = true.
714 nchange with (eq_ex n1 n2 = true);
715 nrewrite > (instrmode_destruct_MODE_TNY … H);
716 nrewrite > (eq_to_eqex n2 n2 (refl_eq …));
718 ##| ##31,32,34: #n; #H; nnormalize; napply (instrmode_destruct … H)
719 ##| ##*: #H; nnormalize; napply (instrmode_destruct … H)
723 nlemma eq_to_eqim34 : ∀n1,i2.MODE_SRT n1 = i2 → eq_im (MODE_SRT n1) i2 = true.
726 nchange with (eq_bit n1 n2 = true);
727 nrewrite > (instrmode_destruct_MODE_SRT … H);
728 nrewrite > (eq_to_eqbit n2 n2 (refl_eq …));
730 ##| ##31,32,33: #n; #H; nnormalize; napply (instrmode_destruct … H)
731 ##| ##*: #H; nnormalize; napply (instrmode_destruct … H)
735 nlemma eq_to_eqim : ∀i1,i2.i1 = i2 → eq_im i1 i2 = true.
737 ##[ ##1: napply eq_to_eqim1 ##| ##2: napply eq_to_eqim2
738 ##| ##3: napply eq_to_eqim3 ##| ##4: napply eq_to_eqim4
739 ##| ##5: napply eq_to_eqim5 ##| ##6: napply eq_to_eqim6
740 ##| ##7: napply eq_to_eqim7 ##| ##8: napply eq_to_eqim8
741 ##| ##9: napply eq_to_eqim9 ##| ##10: napply eq_to_eqim10
742 ##| ##11: napply eq_to_eqim11 ##| ##12: napply eq_to_eqim12
743 ##| ##13: napply eq_to_eqim13 ##| ##14: napply eq_to_eqim14
744 ##| ##15: napply eq_to_eqim15 ##| ##16: napply eq_to_eqim16
745 ##| ##17: napply eq_to_eqim17 ##| ##18: napply eq_to_eqim18
746 ##| ##19: napply eq_to_eqim19 ##| ##20: napply eq_to_eqim20
747 ##| ##21: napply eq_to_eqim21 ##| ##22: napply eq_to_eqim22
748 ##| ##23: napply eq_to_eqim23 ##| ##24: napply eq_to_eqim24
749 ##| ##25: napply eq_to_eqim25 ##| ##26: napply eq_to_eqim26
750 ##| ##27: napply eq_to_eqim27 ##| ##28: napply eq_to_eqim28
751 ##| ##29: napply eq_to_eqim29 ##| ##30: napply eq_to_eqim30
752 ##| ##31: napply eq_to_eqim31 ##| ##32: napply eq_to_eqim32
753 ##| ##33: napply eq_to_eqim33 ##| ##34: napply eq_to_eqim34