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/oct_lemmas.ma".
24 include "freescale/bitrigesim_lemmas.ma".
25 include "freescale/exadecim_lemmas.ma".
26 include "freescale/opcode_base.ma".
28 (* ********************************************** *)
29 (* MATTONI BASE PER DEFINIRE LE TABELLE DELLE MCU *)
30 (* ********************************************** *)
32 ndefinition instr_mode_destruct1 :
33 Πi2.ΠP:Prop.MODE_INH = i2 → match i2 with [ MODE_INH ⇒ P → P | _ ⇒ P ].
37 ##[ ##1: #H; napply (λx:P.x)
38 ##| ##2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H;
40 nchange with (match MODE_INH with [ MODE_INH ⇒ False | _ ⇒ True ]);
41 nrewrite > H; nnormalize; napply I
42 ##| ##31,32,33,34: #n; #H;
44 nchange with (match MODE_INH with [ MODE_INH ⇒ False | _ ⇒ True ]);
45 nrewrite > H; nnormalize; napply I
49 ndefinition instr_mode_destruct2 :
50 Πi2.ΠP:Prop.MODE_INHA = i2 → match i2 with [ MODE_INHA ⇒ P → P | _ ⇒ P ].
54 ##[ ##2: #H; napply (λx:P.x)
55 ##| ##1,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H;
57 nchange with (match MODE_INHA with [ MODE_INHA ⇒ False | _ ⇒ True ]);
58 nrewrite > H; nnormalize; napply I
59 ##| ##31,32,33,34: #n; #H;
61 nchange with (match MODE_INHA with [ MODE_INHA ⇒ False | _ ⇒ True ]);
62 nrewrite > H; nnormalize; napply I
66 ndefinition instr_mode_destruct3 :
67 Πi2.ΠP:Prop.MODE_INHX = i2 → match i2 with [ MODE_INHX ⇒ P → P | _ ⇒ P ].
71 ##[ ##3: #H; napply (λx:P.x)
72 ##| ##1,2,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H;
74 nchange with (match MODE_INHX with [ MODE_INHX ⇒ False | _ ⇒ True ]);
75 nrewrite > H; nnormalize; napply I
76 ##| ##31,32,33,34: #n; #H;
78 nchange with (match MODE_INHX with [ MODE_INHX ⇒ False | _ ⇒ True ]);
79 nrewrite > H; nnormalize; napply I
83 ndefinition instr_mode_destruct4 :
84 Πi2.ΠP:Prop.MODE_INHH = i2 → match i2 with [ MODE_INHH ⇒ P → P | _ ⇒ P ].
88 ##[ ##4: #H; napply (λx:P.x)
89 ##| ##1,2,3,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H;
91 nchange with (match MODE_INHH with [ MODE_INHH ⇒ False | _ ⇒ True ]);
92 nrewrite > H; nnormalize; napply I
93 ##| ##31,32,33,34: #n; #H;
95 nchange with (match MODE_INHH with [ MODE_INHH ⇒ False | _ ⇒ True ]);
96 nrewrite > H; nnormalize; napply I
100 ndefinition instr_mode_destruct5 :
101 Πi2.ΠP:Prop.MODE_INHX0ADD = i2 → match i2 with [ MODE_INHX0ADD ⇒ P → P | _ ⇒ P ].
105 ##[ ##5: #H; napply (λx:P.x)
106 ##| ##1,2,3,4,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H;
108 nchange with (match MODE_INHX0ADD with [ MODE_INHX0ADD ⇒ False | _ ⇒ True ]);
109 nrewrite > H; nnormalize; napply I
110 ##| ##31,32,33,34: #n; #H;
112 nchange with (match MODE_INHX0ADD with [ MODE_INHX0ADD ⇒ False | _ ⇒ True ]);
113 nrewrite > H; nnormalize; napply I
117 ndefinition instr_mode_destruct6 :
118 Πi2.ΠP:Prop.MODE_INHX1ADD = i2 → match i2 with [ MODE_INHX1ADD ⇒ P → P | _ ⇒ P ].
122 ##[ ##6: #H; napply (λx:P.x)
123 ##| ##1,2,3,4,5,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H;
125 nchange with (match MODE_INHX1ADD with [ MODE_INHX1ADD ⇒ False | _ ⇒ True ]);
126 nrewrite > H; nnormalize; napply I
127 ##| ##31,32,33,34: #n; #H;
129 nchange with (match MODE_INHX1ADD with [ MODE_INHX1ADD ⇒ False | _ ⇒ True ]);
130 nrewrite > H; nnormalize; napply I
134 ndefinition instr_mode_destruct7 :
135 Πi2.ΠP:Prop.MODE_INHX2ADD = i2 → match i2 with [ MODE_INHX2ADD ⇒ P → P | _ ⇒ P ].
139 ##[ ##7: #H; napply (λx:P.x)
140 ##| ##1,2,3,4,5,6,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H;
142 nchange with (match MODE_INHX2ADD with [ MODE_INHX2ADD ⇒ False | _ ⇒ True ]);
143 nrewrite > H; nnormalize; napply I
144 ##| ##31,32,33,34: #n; #H;
146 nchange with (match MODE_INHX2ADD with [ MODE_INHX2ADD ⇒ False | _ ⇒ True ]);
147 nrewrite > H; nnormalize; napply I
151 ndefinition instr_mode_destruct8 :
152 Πi2.ΠP:Prop.MODE_IMM1 = i2 → match i2 with [ MODE_IMM1 ⇒ P → P | _ ⇒ P ].
156 ##[ ##8: #H; napply (λx:P.x)
157 ##| ##1,2,3,4,5,6,7,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H;
159 nchange with (match MODE_IMM1 with [ MODE_IMM1 ⇒ False | _ ⇒ True ]);
160 nrewrite > H; nnormalize; napply I
161 ##| ##31,32,33,34: #n; #H;
163 nchange with (match MODE_IMM1 with [ MODE_IMM1 ⇒ False | _ ⇒ True ]);
164 nrewrite > H; nnormalize; napply I
168 ndefinition instr_mode_destruct9 :
169 Πi2.ΠP:Prop.MODE_IMM1EXT = i2 → match i2 with [ MODE_IMM1EXT ⇒ P → P | _ ⇒ P ].
173 ##[ ##9: #H; napply (λx:P.x)
174 ##| ##1,2,3,4,5,6,7,8,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H;
176 nchange with (match MODE_IMM1EXT with [ MODE_IMM1EXT ⇒ False | _ ⇒ True ]);
177 nrewrite > H; nnormalize; napply I
178 ##| ##31,32,33,34: #n; #H;
180 nchange with (match MODE_IMM1EXT with [ MODE_IMM1EXT ⇒ False | _ ⇒ True ]);
181 nrewrite > H; nnormalize; napply I
185 ndefinition instr_mode_destruct10 :
186 Πi2.ΠP:Prop.MODE_IMM2 = i2 → match i2 with [ MODE_IMM2 ⇒ P → P | _ ⇒ P ].
190 ##[ ##10: #H; napply (λx:P.x)
191 ##| ##1,2,3,4,5,6,7,8,9,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H;
193 nchange with (match MODE_IMM2 with [ MODE_IMM2 ⇒ False | _ ⇒ True ]);
194 nrewrite > H; nnormalize; napply I
195 ##| ##31,32,33,34: #n; #H;
197 nchange with (match MODE_IMM2 with [ MODE_IMM2 ⇒ False | _ ⇒ True ]);
198 nrewrite > H; nnormalize; napply I
202 ndefinition instr_mode_destruct11 :
203 Πi2.ΠP:Prop.MODE_DIR1 = i2 → match i2 with [ MODE_DIR1 ⇒ P → P | _ ⇒ P ].
207 ##[ ##11: #H; napply (λx:P.x)
208 ##| ##1,2,3,4,5,6,7,8,9,10,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H;
210 nchange with (match MODE_DIR1 with [ MODE_DIR1 ⇒ False | _ ⇒ True ]);
211 nrewrite > H; nnormalize; napply I
212 ##| ##31,32,33,34: #n; #H;
214 nchange with (match MODE_DIR1 with [ MODE_DIR1 ⇒ False | _ ⇒ True ]);
215 nrewrite > H; nnormalize; napply I
219 ndefinition instr_mode_destruct12 :
220 Πi2.ΠP:Prop.MODE_DIR2 = i2 → match i2 with [ MODE_DIR2 ⇒ P → P | _ ⇒ P ].
224 ##[ ##12: #H; napply (λx:P.x)
225 ##| ##1,2,3,4,5,6,7,8,9,10,11,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H;
227 nchange with (match MODE_DIR2 with [ MODE_DIR2 ⇒ False | _ ⇒ True ]);
228 nrewrite > H; nnormalize; napply I
229 ##| ##31,32,33,34: #n; #H;
231 nchange with (match MODE_DIR2 with [ MODE_DIR2 ⇒ False | _ ⇒ True ]);
232 nrewrite > H; nnormalize; napply I
236 ndefinition instr_mode_destruct13 :
237 Πi2.ΠP:Prop.MODE_IX0 = i2 → match i2 with [ MODE_IX0 ⇒ P → P | _ ⇒ P ].
241 ##[ ##13: #H; napply (λx:P.x)
242 ##| ##1,2,3,4,5,6,7,8,9,10,11,12,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H;
244 nchange with (match MODE_IX0 with [ MODE_IX0 ⇒ False | _ ⇒ True ]);
245 nrewrite > H; nnormalize; napply I
246 ##| ##31,32,33,34: #n; #H;
248 nchange with (match MODE_IX0 with [ MODE_IX0 ⇒ False | _ ⇒ True ]);
249 nrewrite > H; nnormalize; napply I
253 ndefinition instr_mode_destruct14 :
254 Πi2.ΠP:Prop.MODE_IX1 = i2 → match i2 with [ MODE_IX1 ⇒ P → P | _ ⇒ P ].
258 ##[ ##14: #H; napply (λx:P.x)
259 ##| ##1,2,3,4,5,6,7,8,9,10,11,12,13,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H;
261 nchange with (match MODE_IX1 with [ MODE_IX1 ⇒ False | _ ⇒ True ]);
262 nrewrite > H; nnormalize; napply I
263 ##| ##31,32,33,34: #n; #H;
265 nchange with (match MODE_IX1 with [ MODE_IX1 ⇒ False | _ ⇒ True ]);
266 nrewrite > H; nnormalize; napply I
270 ndefinition instr_mode_destruct15 :
271 Πi2.ΠP:Prop.MODE_IX2 = i2 → match i2 with [ MODE_IX2 ⇒ P → P | _ ⇒ P ].
275 ##[ ##15: #H; napply (λx:P.x)
276 ##| ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H;
278 nchange with (match MODE_IX2 with [ MODE_IX2 ⇒ False | _ ⇒ True ]);
279 nrewrite > H; nnormalize; napply I
280 ##| ##31,32,33,34: #n; #H;
282 nchange with (match MODE_IX2 with [ MODE_IX2 ⇒ False | _ ⇒ True ]);
283 nrewrite > H; nnormalize; napply I
287 ndefinition instr_mode_destruct16 :
288 Πi2.ΠP:Prop.MODE_SP1 = i2 → match i2 with [ MODE_SP1 ⇒ P → P | _ ⇒ P ].
292 ##[ ##16: #H; napply (λx:P.x)
293 ##| ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H;
295 nchange with (match MODE_SP1 with [ MODE_SP1 ⇒ False | _ ⇒ True ]);
296 nrewrite > H; nnormalize; napply I
297 ##| ##31,32,33,34: #n; #H;
299 nchange with (match MODE_SP1 with [ MODE_SP1 ⇒ False | _ ⇒ True ]);
300 nrewrite > H; nnormalize; napply I
304 ndefinition instr_mode_destruct17 :
305 Πi2.ΠP:Prop.MODE_SP2 = i2 → match i2 with [ MODE_SP2 ⇒ P → P | _ ⇒ P ].
309 ##[ ##17: #H; napply (λx:P.x)
310 ##| ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,18,19,20,21,22,23,24,25,26,27,28,29,30: #H;
312 nchange with (match MODE_SP2 with [ MODE_SP2 ⇒ False | _ ⇒ True ]);
313 nrewrite > H; nnormalize; napply I
314 ##| ##31,32,33,34: #n; #H;
316 nchange with (match MODE_SP2 with [ MODE_SP2 ⇒ False | _ ⇒ True ]);
317 nrewrite > H; nnormalize; napply I
321 ndefinition instr_mode_destruct18 :
322 Πi2.ΠP:Prop.MODE_DIR1_to_DIR1 = i2 → match i2 with [ MODE_DIR1_to_DIR1 ⇒ P → P | _ ⇒ P ].
326 ##[ ##18: #H; napply (λx:P.x)
327 ##| ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,19,20,21,22,23,24,25,26,27,28,29,30: #H;
329 nchange with (match MODE_DIR1_to_DIR1 with [ MODE_DIR1_to_DIR1 ⇒ False | _ ⇒ True ]);
330 nrewrite > H; nnormalize; napply I
331 ##| ##31,32,33,34: #n; #H;
333 nchange with (match MODE_DIR1_to_DIR1 with [ MODE_DIR1_to_DIR1 ⇒ False | _ ⇒ True ]);
334 nrewrite > H; nnormalize; napply I
338 ndefinition instr_mode_destruct19 :
339 Πi2.ΠP:Prop.MODE_IMM1_to_DIR1 = i2 → match i2 with [ MODE_IMM1_to_DIR1 ⇒ P → P | _ ⇒ P ].
343 ##[ ##19: #H; napply (λx:P.x)
344 ##| ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,20,21,22,23,24,25,26,27,28,29,30: #H;
346 nchange with (match MODE_IMM1_to_DIR1 with [ MODE_IMM1_to_DIR1 ⇒ False | _ ⇒ True ]);
347 nrewrite > H; nnormalize; napply I
348 ##| ##31,32,33,34: #n; #H;
350 nchange with (match MODE_IMM1_to_DIR1 with [ MODE_IMM1_to_DIR1 ⇒ False | _ ⇒ True ]);
351 nrewrite > H; nnormalize; napply I
355 ndefinition instr_mode_destruct20 :
356 Πi2.ΠP:Prop.MODE_IX0p_to_DIR1 = i2 → match i2 with [ MODE_IX0p_to_DIR1 ⇒ P → P | _ ⇒ P ].
360 ##[ ##20: #H; napply (λx:P.x)
361 ##| ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,21,22,23,24,25,26,27,28,29,30: #H;
363 nchange with (match MODE_IX0p_to_DIR1 with [ MODE_IX0p_to_DIR1 ⇒ False | _ ⇒ True ]);
364 nrewrite > H; nnormalize; napply I
365 ##| ##31,32,33,34: #n; #H;
367 nchange with (match MODE_IX0p_to_DIR1 with [ MODE_IX0p_to_DIR1 ⇒ False | _ ⇒ True ]);
368 nrewrite > H; nnormalize; napply I
372 ndefinition instr_mode_destruct21 :
373 Πi2.ΠP:Prop.MODE_DIR1_to_IX0p = i2 → match i2 with [ MODE_DIR1_to_IX0p ⇒ P → P | _ ⇒ P ].
377 ##[ ##21: #H; napply (λx:P.x)
378 ##| ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,22,23,24,25,26,27,28,29,30: #H;
380 nchange with (match MODE_DIR1_to_IX0p with [ MODE_DIR1_to_IX0p ⇒ False | _ ⇒ True ]);
381 nrewrite > H; nnormalize; napply I
382 ##| ##31,32,33,34: #n; #H;
384 nchange with (match MODE_DIR1_to_IX0p with [ MODE_DIR1_to_IX0p ⇒ False | _ ⇒ True ]);
385 nrewrite > H; nnormalize; napply I
389 ndefinition instr_mode_destruct22 :
390 Πi2.ΠP:Prop.MODE_INHA_and_IMM1 = i2 → match i2 with [ MODE_INHA_and_IMM1 ⇒ P → P | _ ⇒ P ].
394 ##[ ##22: #H; napply (λx:P.x)
395 ##| ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,23,24,25,26,27,28,29,30: #H;
397 nchange with (match MODE_INHA_and_IMM1 with [ MODE_INHA_and_IMM1 ⇒ False | _ ⇒ True ]);
398 nrewrite > H; nnormalize; napply I
399 ##| ##31,32,33,34: #n; #H;
401 nchange with (match MODE_INHA_and_IMM1 with [ MODE_INHA_and_IMM1 ⇒ False | _ ⇒ True ]);
402 nrewrite > H; nnormalize; napply I
406 ndefinition instr_mode_destruct23 :
407 Πi2.ΠP:Prop.MODE_INHX_and_IMM1 = i2 → match i2 with [ MODE_INHX_and_IMM1 ⇒ P → P | _ ⇒ P ].
411 ##[ ##23: #H; napply (λx:P.x)
412 ##| ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,24,25,26,27,28,29,30: #H;
414 nchange with (match MODE_INHX_and_IMM1 with [ MODE_INHX_and_IMM1 ⇒ False | _ ⇒ True ]);
415 nrewrite > H; nnormalize; napply I
416 ##| ##31,32,33,34: #n; #H;
418 nchange with (match MODE_INHX_and_IMM1 with [ MODE_INHX_and_IMM1 ⇒ False | _ ⇒ True ]);
419 nrewrite > H; nnormalize; napply I
423 ndefinition instr_mode_destruct24 :
424 Πi2.ΠP:Prop.MODE_IMM1_and_IMM1 = i2 → match i2 with [ MODE_IMM1_and_IMM1 ⇒ P → P | _ ⇒ P ].
428 ##[ ##24: #H; napply (λx:P.x)
429 ##| ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,25,26,27,28,29,30: #H;
431 nchange with (match MODE_IMM1_and_IMM1 with [ MODE_IMM1_and_IMM1 ⇒ False | _ ⇒ True ]);
432 nrewrite > H; nnormalize; napply I
433 ##| ##31,32,33,34: #n; #H;
435 nchange with (match MODE_IMM1_and_IMM1 with [ MODE_IMM1_and_IMM1 ⇒ False | _ ⇒ True ]);
436 nrewrite > H; nnormalize; napply I
440 ndefinition instr_mode_destruct25 :
441 Πi2.ΠP:Prop.MODE_DIR1_and_IMM1 = i2 → match i2 with [ MODE_DIR1_and_IMM1 ⇒ P → P | _ ⇒ P ].
445 ##[ ##25: #H; napply (λx:P.x)
446 ##| ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,26,27,28,29,30: #H;
448 nchange with (match MODE_DIR1_and_IMM1 with [ MODE_DIR1_and_IMM1 ⇒ False | _ ⇒ True ]);
449 nrewrite > H; nnormalize; napply I
450 ##| ##31,32,33,34: #n; #H;
452 nchange with (match MODE_DIR1_and_IMM1 with [ MODE_DIR1_and_IMM1 ⇒ False | _ ⇒ True ]);
453 nrewrite > H; nnormalize; napply I
457 ndefinition instr_mode_destruct26 :
458 Πi2.ΠP:Prop.MODE_IX0_and_IMM1 = i2 → match i2 with [ MODE_IX0_and_IMM1 ⇒ P → P | _ ⇒ P ].
462 ##[ ##26: #H; napply (λx:P.x)
463 ##| ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,27,28,29,30: #H;
465 nchange with (match MODE_IX0_and_IMM1 with [ MODE_IX0_and_IMM1 ⇒ False | _ ⇒ True ]);
466 nrewrite > H; nnormalize; napply I
467 ##| ##31,32,33,34: #n; #H;
469 nchange with (match MODE_IX0_and_IMM1 with [ MODE_IX0_and_IMM1 ⇒ False | _ ⇒ True ]);
470 nrewrite > H; nnormalize; napply I
474 ndefinition instr_mode_destruct27 :
475 Πi2.ΠP:Prop.MODE_IX0p_and_IMM1 = i2 → match i2 with [ MODE_IX0p_and_IMM1 ⇒ P → P | _ ⇒ P ].
479 ##[ ##27: #H; napply (λx:P.x)
480 ##| ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,28,29,30: #H;
482 nchange with (match MODE_IX0p_and_IMM1 with [ MODE_IX0p_and_IMM1 ⇒ False | _ ⇒ True ]);
483 nrewrite > H; nnormalize; napply I
484 ##| ##31,32,33,34: #n; #H;
486 nchange with (match MODE_IX0p_and_IMM1 with [ MODE_IX0p_and_IMM1 ⇒ False | _ ⇒ True ]);
487 nrewrite > H; nnormalize; napply I
491 ndefinition instr_mode_destruct28 :
492 Πi2.ΠP:Prop.MODE_IX1_and_IMM1 = i2 → match i2 with [ MODE_IX1_and_IMM1 ⇒ P → P | _ ⇒ P ].
496 ##[ ##28: #H; napply (λx:P.x)
497 ##| ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,29,30: #H;
499 nchange with (match MODE_IX1_and_IMM1 with [ MODE_IX1_and_IMM1 ⇒ False | _ ⇒ True ]);
500 nrewrite > H; nnormalize; napply I
501 ##| ##31,32,33,34: #n; #H;
503 nchange with (match MODE_IX1_and_IMM1 with [ MODE_IX1_and_IMM1 ⇒ False | _ ⇒ True ]);
504 nrewrite > H; nnormalize; napply I
508 ndefinition instr_mode_destruct29 :
509 Πi2.ΠP:Prop.MODE_IX1p_and_IMM1 = i2 → match i2 with [ MODE_IX1p_and_IMM1 ⇒ P → P | _ ⇒ P ].
513 ##[ ##29: #H; napply (λx:P.x)
514 ##| ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,30: #H;
516 nchange with (match MODE_IX1p_and_IMM1 with [ MODE_IX1p_and_IMM1 ⇒ False | _ ⇒ True ]);
517 nrewrite > H; nnormalize; napply I
518 ##| ##31,32,33,34: #n; #H;
520 nchange with (match MODE_IX1p_and_IMM1 with [ MODE_IX1p_and_IMM1 ⇒ False | _ ⇒ True ]);
521 nrewrite > H; nnormalize; napply I
525 ndefinition instr_mode_destruct30 :
526 Πi2.ΠP:Prop.MODE_SP1_and_IMM1 = i2 → match i2 with [ MODE_SP1_and_IMM1 ⇒ P → P | _ ⇒ P ].
530 ##[ ##30: #H; napply (λx:P.x)
531 ##| ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29: #H;
533 nchange with (match MODE_SP1_and_IMM1 with [ MODE_SP1_and_IMM1 ⇒ False | _ ⇒ True ]);
534 nrewrite > H; nnormalize; napply I
535 ##| ##31,32,33,34: #n; #H;
537 nchange with (match MODE_SP1_and_IMM1 with [ MODE_SP1_and_IMM1 ⇒ False | _ ⇒ True ]);
538 nrewrite > H; nnormalize; napply I
542 nlemma instr_mode_destruct_MODE_DIRn : ∀n1,n2.MODE_DIRn n1 = MODE_DIRn n2 → n1 = n2.
544 nchange with (match MODE_DIRn n2 with [ MODE_DIRn a ⇒ n1 = a | _ ⇒ False ]);
550 ndefinition instr_mode_destruct31 :
551 Πn1,i2.ΠP:Prop.MODE_DIRn n1 = i2 →
553 [ MODE_DIRn n2 ⇒ match n1 with
554 [ o0 ⇒ match n2 with [ o0 ⇒ P → P | _ ⇒ P ] | o1 ⇒ match n2 with [ o1 ⇒ P → P | _ ⇒ P ]
555 | o2 ⇒ match n2 with [ o2 ⇒ P → P | _ ⇒ P ] | o3 ⇒ match n2 with [ o3 ⇒ P → P | _ ⇒ P ]
556 | o4 ⇒ match n2 with [ o4 ⇒ P → P | _ ⇒ P ] | o5 ⇒ match n2 with [ o5 ⇒ P → P | _ ⇒ P ]
557 | o6 ⇒ match n2 with [ o6 ⇒ P → P | _ ⇒ P ] | o7 ⇒ match n2 with [ o7 ⇒ P → P | _ ⇒ P ]]
562 ##[ ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H;
564 nchange with (match MODE_DIRn n1 with [ MODE_DIRn a ⇒ False | _ ⇒ True ]);
565 nrewrite > H; nnormalize; napply I
566 ##| ##32,33,34: #n; #H;
568 nchange with (match MODE_DIRn n1 with [ MODE_DIRn n1 ⇒ False | _ ⇒ True ]);
569 nrewrite > H; nnormalize; napply I
574 ##[ ##1,10,19,28,37,46,55,64: #H; napply (λx:P.x)
575 ##| ##*: #H; napply (oct_destruct … (instr_mode_destruct_MODE_DIRn … H))
579 nlemma instr_mode_destruct_MODE_DIRn_and_IMM1 : ∀n1,n2.MODE_DIRn_and_IMM1 n1 = MODE_DIRn_and_IMM1 n2 → n1 = n2.
581 nchange with (match MODE_DIRn_and_IMM1 n2 with [ MODE_DIRn_and_IMM1 a ⇒ n1 = a | _ ⇒ False ]);
587 ndefinition instr_mode_destruct32 :
588 Πn1,i2.ΠP:Prop.MODE_DIRn_and_IMM1 n1 = i2 →
590 [ MODE_DIRn_and_IMM1 n2 ⇒ match n1 with
591 [ o0 ⇒ match n2 with [ o0 ⇒ P → P | _ ⇒ P ] | o1 ⇒ match n2 with [ o1 ⇒ P → P | _ ⇒ P ]
592 | o2 ⇒ match n2 with [ o2 ⇒ P → P | _ ⇒ P ] | o3 ⇒ match n2 with [ o3 ⇒ P → P | _ ⇒ P ]
593 | o4 ⇒ match n2 with [ o4 ⇒ P → P | _ ⇒ P ] | o5 ⇒ match n2 with [ o5 ⇒ P → P | _ ⇒ P ]
594 | o6 ⇒ match n2 with [ o6 ⇒ P → P | _ ⇒ P ] | o7 ⇒ match n2 with [ o7 ⇒ P → P | _ ⇒ P ]]
599 ##[ ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H;
601 nchange with (match MODE_DIRn_and_IMM1 n1 with [ MODE_DIRn_and_IMM1 a ⇒ False | _ ⇒ True ]);
602 nrewrite > H; nnormalize; napply I
603 ##| ##31,33,34: #n; #H;
605 nchange with (match MODE_DIRn_and_IMM1 n1 with [ MODE_DIRn_and_IMM1 n1 ⇒ False | _ ⇒ True ]);
606 nrewrite > H; nnormalize; napply I
611 ##[ ##1,10,19,28,37,46,55,64: #H; napply (λx:P.x)
612 ##| ##*: #H; napply (oct_destruct … (instr_mode_destruct_MODE_DIRn_and_IMM1 … H))
616 nlemma instr_mode_destruct_MODE_TNY : ∀n1,n2.MODE_TNY n1 = MODE_TNY n2 → n1 = n2.
618 nchange with (match MODE_TNY n2 with [ MODE_TNY a ⇒ n1 = a | _ ⇒ False ]);
624 ndefinition instr_mode_destruct33 :
625 Πn1,i2.ΠP:Prop.MODE_TNY n1 = i2 →
627 [ MODE_TNY n2 ⇒ match n1 with
628 [ x0 ⇒ match n2 with [ x0 ⇒ P → P | _ ⇒ P ] | x1 ⇒ match n2 with [ x1 ⇒ P → P | _ ⇒ P ]
629 | x2 ⇒ match n2 with [ x2 ⇒ P → P | _ ⇒ P ] | x3 ⇒ match n2 with [ x3 ⇒ P → P | _ ⇒ P ]
630 | x4 ⇒ match n2 with [ x4 ⇒ P → P | _ ⇒ P ] | x5 ⇒ match n2 with [ x5 ⇒ P → P | _ ⇒ P ]
631 | x6 ⇒ match n2 with [ x6 ⇒ P → P | _ ⇒ P ] | x7 ⇒ match n2 with [ x7 ⇒ P → P | _ ⇒ P ]
632 | x8 ⇒ match n2 with [ x8 ⇒ P → P | _ ⇒ P ] | x9 ⇒ match n2 with [ x9 ⇒ P → P | _ ⇒ P ]
633 | xA ⇒ match n2 with [ xA ⇒ P → P | _ ⇒ P ] | xB ⇒ match n2 with [ xB ⇒ P → P | _ ⇒ P ]
634 | xC ⇒ match n2 with [ xC ⇒ P → P | _ ⇒ P ] | xD ⇒ match n2 with [ xD ⇒ P → P | _ ⇒ P ]
635 | xE ⇒ match n2 with [ xE ⇒ P → P | _ ⇒ P ] | xF ⇒ match n2 with [ xF ⇒ P → P | _ ⇒ P ]]
640 ##[ ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H;
642 nchange with (match MODE_TNY n1 with [ MODE_TNY a ⇒ False | _ ⇒ True ]);
643 nrewrite > H; nnormalize; napply I
644 ##| ##31,32,34: #n; #H;
646 nchange with (match MODE_TNY n1 with [ MODE_TNY n1 ⇒ False | _ ⇒ True ]);
647 nrewrite > H; nnormalize; napply I
652 ##[ ##1,18,35,52,69,86,103,120,137,154,171,188,205,222,239,256: #H; napply (λx:P.x)
653 ##| ##*: #H; napply (exadecim_destruct … (instr_mode_destruct_MODE_TNY … H))
657 nlemma instr_mode_destruct_MODE_SRT : ∀n1,n2.MODE_SRT n1 = MODE_SRT n2 → n1 = n2.
659 nchange with (match MODE_SRT n2 with [ MODE_SRT a ⇒ n1 = a | _ ⇒ False ]);
665 ndefinition instr_mode_destruct34 :
666 Πn1,i2.ΠP:Prop.MODE_SRT n1 = i2 →
668 [ MODE_SRT n2 ⇒ match n1 with
669 [ t00 ⇒ match n2 with [ t00 ⇒ P → P | _ ⇒ P ] | t01 ⇒ match n2 with [ t01 ⇒ P → P | _ ⇒ P ]
670 | t02 ⇒ match n2 with [ t02 ⇒ P → P | _ ⇒ P ] | t03 ⇒ match n2 with [ t03 ⇒ P → P | _ ⇒ P ]
671 | t04 ⇒ match n2 with [ t04 ⇒ P → P | _ ⇒ P ] | t05 ⇒ match n2 with [ t05 ⇒ P → P | _ ⇒ P ]
672 | t06 ⇒ match n2 with [ t06 ⇒ P → P | _ ⇒ P ] | t07 ⇒ match n2 with [ t07 ⇒ P → P | _ ⇒ P ]
673 | t08 ⇒ match n2 with [ t08 ⇒ P → P | _ ⇒ P ] | t09 ⇒ match n2 with [ t09 ⇒ P → P | _ ⇒ P ]
674 | t0A ⇒ match n2 with [ t0A ⇒ P → P | _ ⇒ P ] | t0B ⇒ match n2 with [ t0B ⇒ P → P | _ ⇒ P ]
675 | t0C ⇒ match n2 with [ t0C ⇒ P → P | _ ⇒ P ] | t0D ⇒ match n2 with [ t0D ⇒ P → P | _ ⇒ P ]
676 | t0E ⇒ match n2 with [ t0E ⇒ P → P | _ ⇒ P ] | t0F ⇒ match n2 with [ t0F ⇒ P → P | _ ⇒ P ]
677 | t10 ⇒ match n2 with [ t10 ⇒ P → P | _ ⇒ P ] | t11 ⇒ match n2 with [ t11 ⇒ P → P | _ ⇒ P ]
678 | t12 ⇒ match n2 with [ t12 ⇒ P → P | _ ⇒ P ] | t13 ⇒ match n2 with [ t13 ⇒ P → P | _ ⇒ P ]
679 | t14 ⇒ match n2 with [ t14 ⇒ P → P | _ ⇒ P ] | t15 ⇒ match n2 with [ t15 ⇒ P → P | _ ⇒ P ]
680 | t16 ⇒ match n2 with [ t16 ⇒ P → P | _ ⇒ P ] | t17 ⇒ match n2 with [ t17 ⇒ P → P | _ ⇒ P ]
681 | t18 ⇒ match n2 with [ t18 ⇒ P → P | _ ⇒ P ] | t19 ⇒ match n2 with [ t19 ⇒ P → P | _ ⇒ P ]
682 | t1A ⇒ match n2 with [ t1A ⇒ P → P | _ ⇒ P ] | t1B ⇒ match n2 with [ t1B ⇒ P → P | _ ⇒ P ]
683 | t1C ⇒ match n2 with [ t1C ⇒ P → P | _ ⇒ P ] | t1D ⇒ match n2 with [ t1D ⇒ P → P | _ ⇒ P ]
684 | t1E ⇒ match n2 with [ t1E ⇒ P → P | _ ⇒ P ] | t1F ⇒ match n2 with [ t1F ⇒ P → P | _ ⇒ P ]]
689 ##[ ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H;
691 nchange with (match MODE_SRT n1 with [ MODE_SRT a ⇒ False | _ ⇒ True ]);
692 nrewrite > H; nnormalize; napply I
693 ##| ##31,32,33: #n; #H;
695 nchange with (match MODE_SRT n1 with [ MODE_SRT n1 ⇒ False | _ ⇒ True ]);
696 nrewrite > H; nnormalize; napply I
699 ##[ ##1: ncases n2; nnormalize;
700 ##[ ##1: #H; napply (λx:P.x)
701 ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
703 ##| ##2: ncases n2; nnormalize;
704 ##[ ##2: #H; napply (λx:P.x)
705 ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
707 ##| ##3: ncases n2; nnormalize;
708 ##[ ##3: #H; napply (λx:P.x)
709 ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
711 ##| ##4: ncases n2; nnormalize;
712 ##[ ##4: #H; napply (λx:P.x)
713 ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
715 ##| ##5: ncases n2; nnormalize;
716 ##[ ##5: #H; napply (λx:P.x)
717 ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
719 ##| ##6: ncases n2; nnormalize;
720 ##[ ##6: #H; napply (λx:P.x)
721 ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
723 ##| ##7: ncases n2; nnormalize;
724 ##[ ##7: #H; napply (λx:P.x)
725 ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
727 ##| ##8: ncases n2; nnormalize;
728 ##[ ##8: #H; napply (λx:P.x)
729 ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
731 ##| ##9: ncases n2; nnormalize;
732 ##[ ##9: #H; napply (λx:P.x)
733 ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
735 ##| ##10: ncases n2; nnormalize;
736 ##[ ##10: #H; napply (λx:P.x)
737 ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
739 ##| ##11: ncases n2; nnormalize;
740 ##[ ##11: #H; napply (λx:P.x)
741 ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
743 ##| ##12: ncases n2; nnormalize;
744 ##[ ##12: #H; napply (λx:P.x)
745 ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
747 ##| ##13: ncases n2; nnormalize;
748 ##[ ##13: #H; napply (λx:P.x)
749 ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
751 ##| ##14: ncases n2; nnormalize;
752 ##[ ##14: #H; napply (λx:P.x)
753 ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
755 ##| ##15: ncases n2; nnormalize;
756 ##[ ##15: #H; napply (λx:P.x)
757 ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
759 ##| ##16: ncases n2; nnormalize;
760 ##[ ##16: #H; napply (λx:P.x)
761 ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
763 ##| ##17: ncases n2; nnormalize;
764 ##[ ##17: #H; napply (λx:P.x)
765 ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
767 ##| ##18: ncases n2; nnormalize;
768 ##[ ##18: #H; napply (λx:P.x)
769 ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
771 ##| ##19: ncases n2; nnormalize;
772 ##[ ##19: #H; napply (λx:P.x)
773 ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
775 ##| ##20: ncases n2; nnormalize;
776 ##[ ##20: #H; napply (λx:P.x)
777 ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
779 ##| ##21: ncases n2; nnormalize;
780 ##[ ##21: #H; napply (λx:P.x)
781 ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
783 ##| ##22: ncases n2; nnormalize;
784 ##[ ##22: #H; napply (λx:P.x)
785 ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
787 ##| ##23: ncases n2; nnormalize;
788 ##[ ##23: #H; napply (λx:P.x)
789 ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
791 ##| ##24: ncases n2; nnormalize;
792 ##[ ##24: #H; napply (λx:P.x)
793 ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
795 ##| ##25: ncases n2; nnormalize;
796 ##[ ##25: #H; napply (λx:P.x)
797 ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
799 ##| ##26: ncases n2; nnormalize;
800 ##[ ##26: #H; napply (λx:P.x)
801 ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
803 ##| ##27: ncases n2; nnormalize;
804 ##[ ##27: #H; napply (λx:P.x)
805 ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
807 ##| ##28: ncases n2; nnormalize;
808 ##[ ##28: #H; napply (λx:P.x)
809 ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
811 ##| ##29: ncases n2; nnormalize;
812 ##[ ##29: #H; napply (λx:P.x)
813 ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
815 ##| ##30: ncases n2; nnormalize;
816 ##[ ##30: #H; napply (λx:P.x)
817 ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
819 ##| ##31: ncases n2; nnormalize;
820 ##[ ##31: #H; napply (λx:P.x)
821 ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
823 ##| ##32: ncases n2; nnormalize;
824 ##[ ##32: #H; napply (λx:P.x)
825 ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
831 ndefinition instr_mode_destruct_aux ≝
832 Πi1,i2.ΠP:Prop.i1 = i2 →
834 [ MODE_INH ⇒ match i2 with [ MODE_INH ⇒ P → P | _ ⇒ P ]
835 | MODE_INHA ⇒ match i2 with [ MODE_INHA ⇒ P → P | _ ⇒ P ]
836 | MODE_INHX ⇒ match i2 with [ MODE_INHX ⇒ P → P | _ ⇒ P ]
837 | MODE_INHH ⇒ match i2 with [ MODE_INHH ⇒ P → P | _ ⇒ P ]
838 | MODE_INHX0ADD ⇒ match i2 with [ MODE_INHX0ADD ⇒ P → P | _ ⇒ P ]
839 | MODE_INHX1ADD ⇒ match i2 with [ MODE_INHX1ADD ⇒ P → P | _ ⇒ P ]
840 | MODE_INHX2ADD ⇒ match i2 with [ MODE_INHX2ADD ⇒ P → P | _ ⇒ P ]
841 | MODE_IMM1 ⇒ match i2 with [ MODE_IMM1 ⇒ P → P | _ ⇒ P ]
842 | MODE_IMM1EXT ⇒ match i2 with [ MODE_IMM1EXT ⇒ P → P | _ ⇒ P ]
843 | MODE_IMM2 ⇒ match i2 with [ MODE_IMM2 ⇒ P → P | _ ⇒ P ]
844 | MODE_DIR1 ⇒ match i2 with [ MODE_DIR1 ⇒ P → P | _ ⇒ P ]
845 | MODE_DIR2 ⇒ match i2 with [ MODE_DIR2 ⇒ P → P | _ ⇒ P ]
846 | MODE_IX0 ⇒ match i2 with [ MODE_IX0 ⇒ P → P | _ ⇒ P ]
847 | MODE_IX1 ⇒ match i2 with [ MODE_IX1 ⇒ P → P | _ ⇒ P ]
848 | MODE_IX2 ⇒ match i2 with [ MODE_IX2 ⇒ P → P | _ ⇒ P ]
849 | MODE_SP1 ⇒ match i2 with [ MODE_SP1 ⇒ P → P | _ ⇒ P ]
850 | MODE_SP2 ⇒ match i2 with [ MODE_SP2 ⇒ P → P | _ ⇒ P ]
851 | MODE_DIR1_to_DIR1 ⇒ match i2 with [ MODE_DIR1_to_DIR1 ⇒ P → P | _ ⇒ P ]
852 | MODE_IMM1_to_DIR1 ⇒ match i2 with [ MODE_IMM1_to_DIR1 ⇒ P → P | _ ⇒ P ]
853 | MODE_IX0p_to_DIR1 ⇒ match i2 with [ MODE_IX0p_to_DIR1 ⇒ P → P | _ ⇒ P ]
854 | MODE_DIR1_to_IX0p ⇒ match i2 with [ MODE_DIR1_to_IX0p ⇒ P → P | _ ⇒ P ]
855 | MODE_INHA_and_IMM1 ⇒ match i2 with [ MODE_INHA_and_IMM1 ⇒ P → P | _ ⇒ P ]
856 | MODE_INHX_and_IMM1 ⇒ match i2 with [ MODE_INHX_and_IMM1 ⇒ P → P | _ ⇒ P ]
857 | MODE_IMM1_and_IMM1 ⇒ match i2 with [ MODE_IMM1_and_IMM1 ⇒ P → P | _ ⇒ P ]
858 | MODE_DIR1_and_IMM1 ⇒ match i2 with [ MODE_DIR1_and_IMM1 ⇒ P → P | _ ⇒ P ]
859 | MODE_IX0_and_IMM1 ⇒ match i2 with [ MODE_IX0_and_IMM1 ⇒ P → P | _ ⇒ P ]
860 | MODE_IX0p_and_IMM1 ⇒ match i2 with [ MODE_IX0p_and_IMM1 ⇒ P → P | _ ⇒ P ]
861 | MODE_IX1_and_IMM1 ⇒ match i2 with [ MODE_IX1_and_IMM1 ⇒ P → P | _ ⇒ P ]
862 | MODE_IX1p_and_IMM1 ⇒ match i2 with [ MODE_IX1p_and_IMM1 ⇒ P → P | _ ⇒ P ]
863 | MODE_SP1_and_IMM1 ⇒ match i2 with [ MODE_SP1_and_IMM1 ⇒ P → P | _ ⇒ P ]
864 | MODE_DIRn n1 ⇒ match i2 with
865 [ MODE_DIRn n2 ⇒ match n1 with
866 [ o0 ⇒ match n2 with [ o0 ⇒ P → P | _ ⇒ P ] | o1 ⇒ match n2 with [ o1 ⇒ P → P | _ ⇒ P ]
867 | o2 ⇒ match n2 with [ o2 ⇒ P → P | _ ⇒ P ] | o3 ⇒ match n2 with [ o3 ⇒ P → P | _ ⇒ P ]
868 | o4 ⇒ match n2 with [ o4 ⇒ P → P | _ ⇒ P ] | o5 ⇒ match n2 with [ o5 ⇒ P → P | _ ⇒ P ]
869 | o6 ⇒ match n2 with [ o6 ⇒ P → P | _ ⇒ P ] | o7 ⇒ match n2 with [ o7 ⇒ P → P | _ ⇒ P ]]
871 | MODE_DIRn_and_IMM1 n1 ⇒ match i2 with
872 [ MODE_DIRn_and_IMM1 n2 ⇒ match n1 with
873 [ o0 ⇒ match n2 with [ o0 ⇒ P → P | _ ⇒ P ] | o1 ⇒ match n2 with [ o1 ⇒ P → P | _ ⇒ P ]
874 | o2 ⇒ match n2 with [ o2 ⇒ P → P | _ ⇒ P ] | o3 ⇒ match n2 with [ o3 ⇒ P → P | _ ⇒ P ]
875 | o4 ⇒ match n2 with [ o4 ⇒ P → P | _ ⇒ P ] | o5 ⇒ match n2 with [ o5 ⇒ P → P | _ ⇒ P ]
876 | o6 ⇒ match n2 with [ o6 ⇒ P → P | _ ⇒ P ] | o7 ⇒ match n2 with [ o7 ⇒ P → P | _ ⇒ P ]]
878 | MODE_TNY e1 ⇒ match i2 with
879 [ MODE_TNY e2 ⇒ match e1 with
880 [ x0 ⇒ match e2 with [ x0 ⇒ P → P | _ ⇒ P ] | x1 ⇒ match e2 with [ x1 ⇒ P → P | _ ⇒ P ]
881 | x2 ⇒ match e2 with [ x2 ⇒ P → P | _ ⇒ P ] | x3 ⇒ match e2 with [ x3 ⇒ P → P | _ ⇒ P ]
882 | x4 ⇒ match e2 with [ x4 ⇒ P → P | _ ⇒ P ] | x5 ⇒ match e2 with [ x5 ⇒ P → P | _ ⇒ P ]
883 | x6 ⇒ match e2 with [ x6 ⇒ P → P | _ ⇒ P ] | x7 ⇒ match e2 with [ x7 ⇒ P → P | _ ⇒ P ]
884 | x8 ⇒ match e2 with [ x8 ⇒ P → P | _ ⇒ P ] | x9 ⇒ match e2 with [ x9 ⇒ P → P | _ ⇒ P ]
885 | xA ⇒ match e2 with [ xA ⇒ P → P | _ ⇒ P ] | xB ⇒ match e2 with [ xB ⇒ P → P | _ ⇒ P ]
886 | xC ⇒ match e2 with [ xC ⇒ P → P | _ ⇒ P ] | xD ⇒ match e2 with [ xD ⇒ P → P | _ ⇒ P ]
887 | xE ⇒ match e2 with [ xE ⇒ P → P | _ ⇒ P ] | xF ⇒ match e2 with [ xF ⇒ P → P | _ ⇒ P ]]
889 | MODE_SRT t1 ⇒ match i2 with
890 [ MODE_SRT t2 ⇒ match t1 with
891 [ t00 ⇒ match t2 with [ t00 ⇒ P → P | _ ⇒ P ] | t01 ⇒ match t2 with [ t01 ⇒ P → P | _ ⇒ P ]
892 | t02 ⇒ match t2 with [ t02 ⇒ P → P | _ ⇒ P ] | t03 ⇒ match t2 with [ t03 ⇒ P → P | _ ⇒ P ]
893 | t04 ⇒ match t2 with [ t04 ⇒ P → P | _ ⇒ P ] | t05 ⇒ match t2 with [ t05 ⇒ P → P | _ ⇒ P ]
894 | t06 ⇒ match t2 with [ t06 ⇒ P → P | _ ⇒ P ] | t07 ⇒ match t2 with [ t07 ⇒ P → P | _ ⇒ P ]
895 | t08 ⇒ match t2 with [ t08 ⇒ P → P | _ ⇒ P ] | t09 ⇒ match t2 with [ t09 ⇒ P → P | _ ⇒ P ]
896 | t0A ⇒ match t2 with [ t0A ⇒ P → P | _ ⇒ P ] | t0B ⇒ match t2 with [ t0B ⇒ P → P | _ ⇒ P ]
897 | t0C ⇒ match t2 with [ t0C ⇒ P → P | _ ⇒ P ] | t0D ⇒ match t2 with [ t0D ⇒ P → P | _ ⇒ P ]
898 | t0E ⇒ match t2 with [ t0E ⇒ P → P | _ ⇒ P ] | t0F ⇒ match t2 with [ t0F ⇒ P → P | _ ⇒ P ]
899 | t10 ⇒ match t2 with [ t10 ⇒ P → P | _ ⇒ P ] | t11 ⇒ match t2 with [ t11 ⇒ P → P | _ ⇒ P ]
900 | t12 ⇒ match t2 with [ t12 ⇒ P → P | _ ⇒ P ] | t13 ⇒ match t2 with [ t13 ⇒ P → P | _ ⇒ P ]
901 | t14 ⇒ match t2 with [ t14 ⇒ P → P | _ ⇒ P ] | t15 ⇒ match t2 with [ t15 ⇒ P → P | _ ⇒ P ]
902 | t16 ⇒ match t2 with [ t16 ⇒ P → P | _ ⇒ P ] | t17 ⇒ match t2 with [ t17 ⇒ P → P | _ ⇒ P ]
903 | t18 ⇒ match t2 with [ t18 ⇒ P → P | _ ⇒ P ] | t19 ⇒ match t2 with [ t19 ⇒ P → P | _ ⇒ P ]
904 | t1A ⇒ match t2 with [ t1A ⇒ P → P | _ ⇒ P ] | t1B ⇒ match t2 with [ t1B ⇒ P → P | _ ⇒ P ]
905 | t1C ⇒ match t2 with [ t1C ⇒ P → P | _ ⇒ P ] | t1D ⇒ match t2 with [ t1D ⇒ P → P | _ ⇒ P ]
906 | t1E ⇒ match t2 with [ t1E ⇒ P → P | _ ⇒ P ] | t1F ⇒ match t2 with [ t1F ⇒ P → P | _ ⇒ P ]]
910 ndefinition instr_mode_destruct : instr_mode_destruct_aux.
912 ##[ ##1: napply instr_mode_destruct1 ##| ##2: napply instr_mode_destruct2
913 ##| ##3: napply instr_mode_destruct3 ##| ##4: napply instr_mode_destruct4
914 ##| ##5: napply instr_mode_destruct5 ##| ##6: napply instr_mode_destruct6
915 ##| ##7: napply instr_mode_destruct7 ##| ##8: napply instr_mode_destruct8
916 ##| ##9: napply instr_mode_destruct9 ##| ##10: napply instr_mode_destruct10
917 ##| ##11: napply instr_mode_destruct11 ##| ##12: napply instr_mode_destruct12
918 ##| ##13: napply instr_mode_destruct13 ##| ##14: napply instr_mode_destruct14
919 ##| ##15: napply instr_mode_destruct15 ##| ##16: napply instr_mode_destruct16
920 ##| ##17: napply instr_mode_destruct17 ##| ##18: napply instr_mode_destruct18
921 ##| ##19: napply instr_mode_destruct19 ##| ##20: napply instr_mode_destruct20
922 ##| ##21: napply instr_mode_destruct21 ##| ##22: napply instr_mode_destruct22
923 ##| ##23: napply instr_mode_destruct23 ##| ##24: napply instr_mode_destruct24
924 ##| ##25: napply instr_mode_destruct25 ##| ##26: napply instr_mode_destruct26
925 ##| ##27: napply instr_mode_destruct27 ##| ##28: napply instr_mode_destruct28
926 ##| ##29: napply instr_mode_destruct29 ##| ##30: napply instr_mode_destruct30
927 ##| ##31: napply instr_mode_destruct31 ##| ##32: napply instr_mode_destruct32
928 ##| ##33: napply instr_mode_destruct33 ##| ##34: napply instr_mode_destruct34