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 *)
19 (* Cosimo Oliboni, oliboni@cs.unibo.it *)
21 (* Questo materiale fa parte della tesi: *)
22 (* "Formalizzazione Interattiva dei Microcontroller a 8bit FreeScale" *)
24 (* data ultima modifica 15/11/2007 *)
25 (* ********************************************************************** *)
27 include "freescale/aux_bases_lemmas.ma".
28 include "freescale/exadecim_lemmas.ma".
29 include "freescale/opcode_base.ma".
31 (* ********************************************** *)
32 (* MATTONI BASE PER DEFINIRE LE TABELLE DELLE MCU *)
33 (* ********************************************** *)
35 ndefinition instr_mode_destruct1 :
36 Πi2.ΠP:Prop.MODE_INH = i2 → match i2 with [ MODE_INH ⇒ P → P | _ ⇒ P ].
40 ##[ ##1: #H; napply (λx:P.x)
41 ##| ##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;
42 napply (False_ind ??);
43 nchange with (match MODE_INH with [ MODE_INH ⇒ False | _ ⇒ True ]);
44 nrewrite > H; nnormalize; napply I
45 ##| ##31,32,33,34: #n; #H;
46 napply (False_ind ??);
47 nchange with (match MODE_INH with [ MODE_INH ⇒ False | _ ⇒ True ]);
48 nrewrite > H; nnormalize; napply I
52 ndefinition instr_mode_destruct2 :
53 Πi2.ΠP:Prop.MODE_INHA = i2 → match i2 with [ MODE_INHA ⇒ P → P | _ ⇒ P ].
57 ##[ ##2: #H; napply (λx:P.x)
58 ##| ##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;
59 napply (False_ind ??);
60 nchange with (match MODE_INHA with [ MODE_INHA ⇒ False | _ ⇒ True ]);
61 nrewrite > H; nnormalize; napply I
62 ##| ##31,32,33,34: #n; #H;
63 napply (False_ind ??);
64 nchange with (match MODE_INHA with [ MODE_INHA ⇒ False | _ ⇒ True ]);
65 nrewrite > H; nnormalize; napply I
69 ndefinition instr_mode_destruct3 :
70 Πi2.ΠP:Prop.MODE_INHX = i2 → match i2 with [ MODE_INHX ⇒ P → P | _ ⇒ P ].
74 ##[ ##3: #H; napply (λx:P.x)
75 ##| ##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;
76 napply (False_ind ??);
77 nchange with (match MODE_INHX with [ MODE_INHX ⇒ False | _ ⇒ True ]);
78 nrewrite > H; nnormalize; napply I
79 ##| ##31,32,33,34: #n; #H;
80 napply (False_ind ??);
81 nchange with (match MODE_INHX with [ MODE_INHX ⇒ False | _ ⇒ True ]);
82 nrewrite > H; nnormalize; napply I
86 ndefinition instr_mode_destruct4 :
87 Πi2.ΠP:Prop.MODE_INHH = i2 → match i2 with [ MODE_INHH ⇒ P → P | _ ⇒ P ].
91 ##[ ##4: #H; napply (λx:P.x)
92 ##| ##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;
93 napply (False_ind ??);
94 nchange with (match MODE_INHH with [ MODE_INHH ⇒ False | _ ⇒ True ]);
95 nrewrite > H; nnormalize; napply I
96 ##| ##31,32,33,34: #n; #H;
97 napply (False_ind ??);
98 nchange with (match MODE_INHH with [ MODE_INHH ⇒ False | _ ⇒ True ]);
99 nrewrite > H; nnormalize; napply I
103 ndefinition instr_mode_destruct5 :
104 Πi2.ΠP:Prop.MODE_INHX0ADD = i2 → match i2 with [ MODE_INHX0ADD ⇒ P → P | _ ⇒ P ].
108 ##[ ##5: #H; napply (λx:P.x)
109 ##| ##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;
110 napply (False_ind ??);
111 nchange with (match MODE_INHX0ADD with [ MODE_INHX0ADD ⇒ False | _ ⇒ True ]);
112 nrewrite > H; nnormalize; napply I
113 ##| ##31,32,33,34: #n; #H;
114 napply (False_ind ??);
115 nchange with (match MODE_INHX0ADD with [ MODE_INHX0ADD ⇒ False | _ ⇒ True ]);
116 nrewrite > H; nnormalize; napply I
120 ndefinition instr_mode_destruct6 :
121 Πi2.ΠP:Prop.MODE_INHX1ADD = i2 → match i2 with [ MODE_INHX1ADD ⇒ P → P | _ ⇒ P ].
125 ##[ ##6: #H; napply (λx:P.x)
126 ##| ##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;
127 napply (False_ind ??);
128 nchange with (match MODE_INHX1ADD with [ MODE_INHX1ADD ⇒ False | _ ⇒ True ]);
129 nrewrite > H; nnormalize; napply I
130 ##| ##31,32,33,34: #n; #H;
131 napply (False_ind ??);
132 nchange with (match MODE_INHX1ADD with [ MODE_INHX1ADD ⇒ False | _ ⇒ True ]);
133 nrewrite > H; nnormalize; napply I
137 ndefinition instr_mode_destruct7 :
138 Πi2.ΠP:Prop.MODE_INHX2ADD = i2 → match i2 with [ MODE_INHX2ADD ⇒ P → P | _ ⇒ P ].
142 ##[ ##7: #H; napply (λx:P.x)
143 ##| ##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;
144 napply (False_ind ??);
145 nchange with (match MODE_INHX2ADD with [ MODE_INHX2ADD ⇒ False | _ ⇒ True ]);
146 nrewrite > H; nnormalize; napply I
147 ##| ##31,32,33,34: #n; #H;
148 napply (False_ind ??);
149 nchange with (match MODE_INHX2ADD with [ MODE_INHX2ADD ⇒ False | _ ⇒ True ]);
150 nrewrite > H; nnormalize; napply I
154 ndefinition instr_mode_destruct8 :
155 Πi2.ΠP:Prop.MODE_IMM1 = i2 → match i2 with [ MODE_IMM1 ⇒ P → P | _ ⇒ P ].
159 ##[ ##8: #H; napply (λx:P.x)
160 ##| ##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;
161 napply (False_ind ??);
162 nchange with (match MODE_IMM1 with [ MODE_IMM1 ⇒ False | _ ⇒ True ]);
163 nrewrite > H; nnormalize; napply I
164 ##| ##31,32,33,34: #n; #H;
165 napply (False_ind ??);
166 nchange with (match MODE_IMM1 with [ MODE_IMM1 ⇒ False | _ ⇒ True ]);
167 nrewrite > H; nnormalize; napply I
171 ndefinition instr_mode_destruct9 :
172 Πi2.ΠP:Prop.MODE_IMM1EXT = i2 → match i2 with [ MODE_IMM1EXT ⇒ P → P | _ ⇒ P ].
176 ##[ ##9: #H; napply (λx:P.x)
177 ##| ##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;
178 napply (False_ind ??);
179 nchange with (match MODE_IMM1EXT with [ MODE_IMM1EXT ⇒ False | _ ⇒ True ]);
180 nrewrite > H; nnormalize; napply I
181 ##| ##31,32,33,34: #n; #H;
182 napply (False_ind ??);
183 nchange with (match MODE_IMM1EXT with [ MODE_IMM1EXT ⇒ False | _ ⇒ True ]);
184 nrewrite > H; nnormalize; napply I
188 ndefinition instr_mode_destruct10 :
189 Πi2.ΠP:Prop.MODE_IMM2 = i2 → match i2 with [ MODE_IMM2 ⇒ P → P | _ ⇒ P ].
193 ##[ ##10: #H; napply (λx:P.x)
194 ##| ##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;
195 napply (False_ind ??);
196 nchange with (match MODE_IMM2 with [ MODE_IMM2 ⇒ False | _ ⇒ True ]);
197 nrewrite > H; nnormalize; napply I
198 ##| ##31,32,33,34: #n; #H;
199 napply (False_ind ??);
200 nchange with (match MODE_IMM2 with [ MODE_IMM2 ⇒ False | _ ⇒ True ]);
201 nrewrite > H; nnormalize; napply I
205 ndefinition instr_mode_destruct11 :
206 Πi2.ΠP:Prop.MODE_DIR1 = i2 → match i2 with [ MODE_DIR1 ⇒ P → P | _ ⇒ P ].
210 ##[ ##11: #H; napply (λx:P.x)
211 ##| ##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;
212 napply (False_ind ??);
213 nchange with (match MODE_DIR1 with [ MODE_DIR1 ⇒ False | _ ⇒ True ]);
214 nrewrite > H; nnormalize; napply I
215 ##| ##31,32,33,34: #n; #H;
216 napply (False_ind ??);
217 nchange with (match MODE_DIR1 with [ MODE_DIR1 ⇒ False | _ ⇒ True ]);
218 nrewrite > H; nnormalize; napply I
222 ndefinition instr_mode_destruct12 :
223 Πi2.ΠP:Prop.MODE_DIR2 = i2 → match i2 with [ MODE_DIR2 ⇒ P → P | _ ⇒ P ].
227 ##[ ##12: #H; napply (λx:P.x)
228 ##| ##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;
229 napply (False_ind ??);
230 nchange with (match MODE_DIR2 with [ MODE_DIR2 ⇒ False | _ ⇒ True ]);
231 nrewrite > H; nnormalize; napply I
232 ##| ##31,32,33,34: #n; #H;
233 napply (False_ind ??);
234 nchange with (match MODE_DIR2 with [ MODE_DIR2 ⇒ False | _ ⇒ True ]);
235 nrewrite > H; nnormalize; napply I
239 ndefinition instr_mode_destruct13 :
240 Πi2.ΠP:Prop.MODE_IX0 = i2 → match i2 with [ MODE_IX0 ⇒ P → P | _ ⇒ P ].
244 ##[ ##13: #H; napply (λx:P.x)
245 ##| ##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;
246 napply (False_ind ??);
247 nchange with (match MODE_IX0 with [ MODE_IX0 ⇒ False | _ ⇒ True ]);
248 nrewrite > H; nnormalize; napply I
249 ##| ##31,32,33,34: #n; #H;
250 napply (False_ind ??);
251 nchange with (match MODE_IX0 with [ MODE_IX0 ⇒ False | _ ⇒ True ]);
252 nrewrite > H; nnormalize; napply I
256 ndefinition instr_mode_destruct14 :
257 Πi2.ΠP:Prop.MODE_IX1 = i2 → match i2 with [ MODE_IX1 ⇒ P → P | _ ⇒ P ].
261 ##[ ##14: #H; napply (λx:P.x)
262 ##| ##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;
263 napply (False_ind ??);
264 nchange with (match MODE_IX1 with [ MODE_IX1 ⇒ False | _ ⇒ True ]);
265 nrewrite > H; nnormalize; napply I
266 ##| ##31,32,33,34: #n; #H;
267 napply (False_ind ??);
268 nchange with (match MODE_IX1 with [ MODE_IX1 ⇒ False | _ ⇒ True ]);
269 nrewrite > H; nnormalize; napply I
273 ndefinition instr_mode_destruct15 :
274 Πi2.ΠP:Prop.MODE_IX2 = i2 → match i2 with [ MODE_IX2 ⇒ P → P | _ ⇒ P ].
278 ##[ ##15: #H; napply (λx:P.x)
279 ##| ##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;
280 napply (False_ind ??);
281 nchange with (match MODE_IX2 with [ MODE_IX2 ⇒ False | _ ⇒ True ]);
282 nrewrite > H; nnormalize; napply I
283 ##| ##31,32,33,34: #n; #H;
284 napply (False_ind ??);
285 nchange with (match MODE_IX2 with [ MODE_IX2 ⇒ False | _ ⇒ True ]);
286 nrewrite > H; nnormalize; napply I
290 ndefinition instr_mode_destruct16 :
291 Πi2.ΠP:Prop.MODE_SP1 = i2 → match i2 with [ MODE_SP1 ⇒ P → P | _ ⇒ P ].
295 ##[ ##16: #H; napply (λx:P.x)
296 ##| ##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;
297 napply (False_ind ??);
298 nchange with (match MODE_SP1 with [ MODE_SP1 ⇒ False | _ ⇒ True ]);
299 nrewrite > H; nnormalize; napply I
300 ##| ##31,32,33,34: #n; #H;
301 napply (False_ind ??);
302 nchange with (match MODE_SP1 with [ MODE_SP1 ⇒ False | _ ⇒ True ]);
303 nrewrite > H; nnormalize; napply I
307 ndefinition instr_mode_destruct17 :
308 Πi2.ΠP:Prop.MODE_SP2 = i2 → match i2 with [ MODE_SP2 ⇒ P → P | _ ⇒ P ].
312 ##[ ##17: #H; napply (λx:P.x)
313 ##| ##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;
314 napply (False_ind ??);
315 nchange with (match MODE_SP2 with [ MODE_SP2 ⇒ False | _ ⇒ True ]);
316 nrewrite > H; nnormalize; napply I
317 ##| ##31,32,33,34: #n; #H;
318 napply (False_ind ??);
319 nchange with (match MODE_SP2 with [ MODE_SP2 ⇒ False | _ ⇒ True ]);
320 nrewrite > H; nnormalize; napply I
324 ndefinition instr_mode_destruct18 :
325 Πi2.ΠP:Prop.MODE_DIR1_to_DIR1 = i2 → match i2 with [ MODE_DIR1_to_DIR1 ⇒ P → P | _ ⇒ P ].
329 ##[ ##18: #H; napply (λx:P.x)
330 ##| ##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;
331 napply (False_ind ??);
332 nchange with (match MODE_DIR1_to_DIR1 with [ MODE_DIR1_to_DIR1 ⇒ False | _ ⇒ True ]);
333 nrewrite > H; nnormalize; napply I
334 ##| ##31,32,33,34: #n; #H;
335 napply (False_ind ??);
336 nchange with (match MODE_DIR1_to_DIR1 with [ MODE_DIR1_to_DIR1 ⇒ False | _ ⇒ True ]);
337 nrewrite > H; nnormalize; napply I
341 ndefinition instr_mode_destruct19 :
342 Πi2.ΠP:Prop.MODE_IMM1_to_DIR1 = i2 → match i2 with [ MODE_IMM1_to_DIR1 ⇒ P → P | _ ⇒ P ].
346 ##[ ##19: #H; napply (λx:P.x)
347 ##| ##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;
348 napply (False_ind ??);
349 nchange with (match MODE_IMM1_to_DIR1 with [ MODE_IMM1_to_DIR1 ⇒ False | _ ⇒ True ]);
350 nrewrite > H; nnormalize; napply I
351 ##| ##31,32,33,34: #n; #H;
352 napply (False_ind ??);
353 nchange with (match MODE_IMM1_to_DIR1 with [ MODE_IMM1_to_DIR1 ⇒ False | _ ⇒ True ]);
354 nrewrite > H; nnormalize; napply I
358 ndefinition instr_mode_destruct20 :
359 Πi2.ΠP:Prop.MODE_IX0p_to_DIR1 = i2 → match i2 with [ MODE_IX0p_to_DIR1 ⇒ P → P | _ ⇒ P ].
363 ##[ ##20: #H; napply (λx:P.x)
364 ##| ##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;
365 napply (False_ind ??);
366 nchange with (match MODE_IX0p_to_DIR1 with [ MODE_IX0p_to_DIR1 ⇒ False | _ ⇒ True ]);
367 nrewrite > H; nnormalize; napply I
368 ##| ##31,32,33,34: #n; #H;
369 napply (False_ind ??);
370 nchange with (match MODE_IX0p_to_DIR1 with [ MODE_IX0p_to_DIR1 ⇒ False | _ ⇒ True ]);
371 nrewrite > H; nnormalize; napply I
375 ndefinition instr_mode_destruct21 :
376 Πi2.ΠP:Prop.MODE_DIR1_to_IX0p = i2 → match i2 with [ MODE_DIR1_to_IX0p ⇒ P → P | _ ⇒ P ].
380 ##[ ##21: #H; napply (λx:P.x)
381 ##| ##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;
382 napply (False_ind ??);
383 nchange with (match MODE_DIR1_to_IX0p with [ MODE_DIR1_to_IX0p ⇒ False | _ ⇒ True ]);
384 nrewrite > H; nnormalize; napply I
385 ##| ##31,32,33,34: #n; #H;
386 napply (False_ind ??);
387 nchange with (match MODE_DIR1_to_IX0p with [ MODE_DIR1_to_IX0p ⇒ False | _ ⇒ True ]);
388 nrewrite > H; nnormalize; napply I
392 ndefinition instr_mode_destruct22 :
393 Πi2.ΠP:Prop.MODE_INHA_and_IMM1 = i2 → match i2 with [ MODE_INHA_and_IMM1 ⇒ P → P | _ ⇒ P ].
397 ##[ ##22: #H; napply (λx:P.x)
398 ##| ##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;
399 napply (False_ind ??);
400 nchange with (match MODE_INHA_and_IMM1 with [ MODE_INHA_and_IMM1 ⇒ False | _ ⇒ True ]);
401 nrewrite > H; nnormalize; napply I
402 ##| ##31,32,33,34: #n; #H;
403 napply (False_ind ??);
404 nchange with (match MODE_INHA_and_IMM1 with [ MODE_INHA_and_IMM1 ⇒ False | _ ⇒ True ]);
405 nrewrite > H; nnormalize; napply I
409 ndefinition instr_mode_destruct23 :
410 Πi2.ΠP:Prop.MODE_INHX_and_IMM1 = i2 → match i2 with [ MODE_INHX_and_IMM1 ⇒ P → P | _ ⇒ P ].
414 ##[ ##23: #H; napply (λx:P.x)
415 ##| ##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;
416 napply (False_ind ??);
417 nchange with (match MODE_INHX_and_IMM1 with [ MODE_INHX_and_IMM1 ⇒ False | _ ⇒ True ]);
418 nrewrite > H; nnormalize; napply I
419 ##| ##31,32,33,34: #n; #H;
420 napply (False_ind ??);
421 nchange with (match MODE_INHX_and_IMM1 with [ MODE_INHX_and_IMM1 ⇒ False | _ ⇒ True ]);
422 nrewrite > H; nnormalize; napply I
426 ndefinition instr_mode_destruct24 :
427 Πi2.ΠP:Prop.MODE_IMM1_and_IMM1 = i2 → match i2 with [ MODE_IMM1_and_IMM1 ⇒ P → P | _ ⇒ P ].
431 ##[ ##24: #H; napply (λx:P.x)
432 ##| ##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;
433 napply (False_ind ??);
434 nchange with (match MODE_IMM1_and_IMM1 with [ MODE_IMM1_and_IMM1 ⇒ False | _ ⇒ True ]);
435 nrewrite > H; nnormalize; napply I
436 ##| ##31,32,33,34: #n; #H;
437 napply (False_ind ??);
438 nchange with (match MODE_IMM1_and_IMM1 with [ MODE_IMM1_and_IMM1 ⇒ False | _ ⇒ True ]);
439 nrewrite > H; nnormalize; napply I
443 ndefinition instr_mode_destruct25 :
444 Πi2.ΠP:Prop.MODE_DIR1_and_IMM1 = i2 → match i2 with [ MODE_DIR1_and_IMM1 ⇒ P → P | _ ⇒ P ].
448 ##[ ##25: #H; napply (λx:P.x)
449 ##| ##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;
450 napply (False_ind ??);
451 nchange with (match MODE_DIR1_and_IMM1 with [ MODE_DIR1_and_IMM1 ⇒ False | _ ⇒ True ]);
452 nrewrite > H; nnormalize; napply I
453 ##| ##31,32,33,34: #n; #H;
454 napply (False_ind ??);
455 nchange with (match MODE_DIR1_and_IMM1 with [ MODE_DIR1_and_IMM1 ⇒ False | _ ⇒ True ]);
456 nrewrite > H; nnormalize; napply I
460 ndefinition instr_mode_destruct26 :
461 Πi2.ΠP:Prop.MODE_IX0_and_IMM1 = i2 → match i2 with [ MODE_IX0_and_IMM1 ⇒ P → P | _ ⇒ P ].
465 ##[ ##26: #H; napply (λx:P.x)
466 ##| ##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;
467 napply (False_ind ??);
468 nchange with (match MODE_IX0_and_IMM1 with [ MODE_IX0_and_IMM1 ⇒ False | _ ⇒ True ]);
469 nrewrite > H; nnormalize; napply I
470 ##| ##31,32,33,34: #n; #H;
471 napply (False_ind ??);
472 nchange with (match MODE_IX0_and_IMM1 with [ MODE_IX0_and_IMM1 ⇒ False | _ ⇒ True ]);
473 nrewrite > H; nnormalize; napply I
477 ndefinition instr_mode_destruct27 :
478 Πi2.ΠP:Prop.MODE_IX0p_and_IMM1 = i2 → match i2 with [ MODE_IX0p_and_IMM1 ⇒ P → P | _ ⇒ P ].
482 ##[ ##27: #H; napply (λx:P.x)
483 ##| ##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;
484 napply (False_ind ??);
485 nchange with (match MODE_IX0p_and_IMM1 with [ MODE_IX0p_and_IMM1 ⇒ False | _ ⇒ True ]);
486 nrewrite > H; nnormalize; napply I
487 ##| ##31,32,33,34: #n; #H;
488 napply (False_ind ??);
489 nchange with (match MODE_IX0p_and_IMM1 with [ MODE_IX0p_and_IMM1 ⇒ False | _ ⇒ True ]);
490 nrewrite > H; nnormalize; napply I
494 ndefinition instr_mode_destruct28 :
495 Πi2.ΠP:Prop.MODE_IX1_and_IMM1 = i2 → match i2 with [ MODE_IX1_and_IMM1 ⇒ P → P | _ ⇒ P ].
499 ##[ ##28: #H; napply (λx:P.x)
500 ##| ##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;
501 napply (False_ind ??);
502 nchange with (match MODE_IX1_and_IMM1 with [ MODE_IX1_and_IMM1 ⇒ False | _ ⇒ True ]);
503 nrewrite > H; nnormalize; napply I
504 ##| ##31,32,33,34: #n; #H;
505 napply (False_ind ??);
506 nchange with (match MODE_IX1_and_IMM1 with [ MODE_IX1_and_IMM1 ⇒ False | _ ⇒ True ]);
507 nrewrite > H; nnormalize; napply I
511 ndefinition instr_mode_destruct29 :
512 Πi2.ΠP:Prop.MODE_IX1p_and_IMM1 = i2 → match i2 with [ MODE_IX1p_and_IMM1 ⇒ P → P | _ ⇒ P ].
516 ##[ ##29: #H; napply (λx:P.x)
517 ##| ##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;
518 napply (False_ind ??);
519 nchange with (match MODE_IX1p_and_IMM1 with [ MODE_IX1p_and_IMM1 ⇒ False | _ ⇒ True ]);
520 nrewrite > H; nnormalize; napply I
521 ##| ##31,32,33,34: #n; #H;
522 napply (False_ind ??);
523 nchange with (match MODE_IX1p_and_IMM1 with [ MODE_IX1p_and_IMM1 ⇒ False | _ ⇒ True ]);
524 nrewrite > H; nnormalize; napply I
528 ndefinition instr_mode_destruct30 :
529 Πi2.ΠP:Prop.MODE_SP1_and_IMM1 = i2 → match i2 with [ MODE_SP1_and_IMM1 ⇒ P → P | _ ⇒ P ].
533 ##[ ##30: #H; napply (λx:P.x)
534 ##| ##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;
535 napply (False_ind ??);
536 nchange with (match MODE_SP1_and_IMM1 with [ MODE_SP1_and_IMM1 ⇒ False | _ ⇒ True ]);
537 nrewrite > H; nnormalize; napply I
538 ##| ##31,32,33,34: #n; #H;
539 napply (False_ind ??);
540 nchange with (match MODE_SP1_and_IMM1 with [ MODE_SP1_and_IMM1 ⇒ False | _ ⇒ True ]);
541 nrewrite > H; nnormalize; napply I
545 nlemma instr_mode_destruct_MODE_DIRn : ∀n1,n2.MODE_DIRn n1 = MODE_DIRn n2 → n1 = n2.
547 nchange with (match MODE_DIRn n2 with [ MODE_DIRn a ⇒ n1 = a | _ ⇒ False ]);
553 ndefinition instr_mode_destruct31 :
554 Πn1,i2.ΠP:Prop.MODE_DIRn n1 = i2 →
556 [ MODE_DIRn n2 ⇒ match n1 with
557 [ o0 ⇒ match n2 with [ o0 ⇒ P → P | _ ⇒ P ] | o1 ⇒ match n2 with [ o1 ⇒ P → P | _ ⇒ P ]
558 | o2 ⇒ match n2 with [ o2 ⇒ P → P | _ ⇒ P ] | o3 ⇒ match n2 with [ o3 ⇒ P → P | _ ⇒ P ]
559 | o4 ⇒ match n2 with [ o4 ⇒ P → P | _ ⇒ P ] | o5 ⇒ match n2 with [ o5 ⇒ P → P | _ ⇒ P ]
560 | o6 ⇒ match n2 with [ o6 ⇒ P → P | _ ⇒ P ] | o7 ⇒ match n2 with [ o7 ⇒ P → P | _ ⇒ P ]]
565 ##[ ##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;
566 napply (False_ind ??);
567 nchange with (match MODE_DIRn n1 with [ MODE_DIRn a ⇒ False | _ ⇒ True ]);
568 nrewrite > H; nnormalize; napply I
569 ##| ##32,33,34: #n; #H;
570 napply (False_ind ??);
571 nchange with (match MODE_DIRn n1 with [ MODE_DIRn n1 ⇒ False | _ ⇒ True ]);
572 nrewrite > H; nnormalize; napply I
577 ##[ ##1,10,19,28,37,46,55,64: #H; napply (λx:P.x)
578 ##| ##*: #H; napply (oct_destruct ??? (instr_mode_destruct_MODE_DIRn ?? H))
582 nlemma instr_mode_destruct_MODE_DIRn_and_IMM1 : ∀n1,n2.MODE_DIRn_and_IMM1 n1 = MODE_DIRn_and_IMM1 n2 → n1 = n2.
584 nchange with (match MODE_DIRn_and_IMM1 n2 with [ MODE_DIRn_and_IMM1 a ⇒ n1 = a | _ ⇒ False ]);
590 ndefinition instr_mode_destruct32 :
591 Πn1,i2.ΠP:Prop.MODE_DIRn_and_IMM1 n1 = i2 →
593 [ MODE_DIRn_and_IMM1 n2 ⇒ match n1 with
594 [ o0 ⇒ match n2 with [ o0 ⇒ P → P | _ ⇒ P ] | o1 ⇒ match n2 with [ o1 ⇒ P → P | _ ⇒ P ]
595 | o2 ⇒ match n2 with [ o2 ⇒ P → P | _ ⇒ P ] | o3 ⇒ match n2 with [ o3 ⇒ P → P | _ ⇒ P ]
596 | o4 ⇒ match n2 with [ o4 ⇒ P → P | _ ⇒ P ] | o5 ⇒ match n2 with [ o5 ⇒ P → P | _ ⇒ P ]
597 | o6 ⇒ match n2 with [ o6 ⇒ P → P | _ ⇒ P ] | o7 ⇒ match n2 with [ o7 ⇒ P → P | _ ⇒ P ]]
602 ##[ ##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;
603 napply (False_ind ??);
604 nchange with (match MODE_DIRn_and_IMM1 n1 with [ MODE_DIRn_and_IMM1 a ⇒ False | _ ⇒ True ]);
605 nrewrite > H; nnormalize; napply I
606 ##| ##31,33,34: #n; #H;
607 napply (False_ind ??);
608 nchange with (match MODE_DIRn_and_IMM1 n1 with [ MODE_DIRn_and_IMM1 n1 ⇒ False | _ ⇒ True ]);
609 nrewrite > H; nnormalize; napply I
614 ##[ ##1,10,19,28,37,46,55,64: #H; napply (λx:P.x)
615 ##| ##*: #H; napply (oct_destruct ??? (instr_mode_destruct_MODE_DIRn_and_IMM1 ?? H))
619 nlemma instr_mode_destruct_MODE_TNY : ∀n1,n2.MODE_TNY n1 = MODE_TNY n2 → n1 = n2.
621 nchange with (match MODE_TNY n2 with [ MODE_TNY a ⇒ n1 = a | _ ⇒ False ]);
627 ndefinition instr_mode_destruct33 :
628 Πn1,i2.ΠP:Prop.MODE_TNY n1 = i2 →
630 [ MODE_TNY n2 ⇒ match n1 with
631 [ x0 ⇒ match n2 with [ x0 ⇒ P → P | _ ⇒ P ] | x1 ⇒ match n2 with [ x1 ⇒ P → P | _ ⇒ P ]
632 | x2 ⇒ match n2 with [ x2 ⇒ P → P | _ ⇒ P ] | x3 ⇒ match n2 with [ x3 ⇒ P → P | _ ⇒ P ]
633 | x4 ⇒ match n2 with [ x4 ⇒ P → P | _ ⇒ P ] | x5 ⇒ match n2 with [ x5 ⇒ P → P | _ ⇒ P ]
634 | x6 ⇒ match n2 with [ x6 ⇒ P → P | _ ⇒ P ] | x7 ⇒ match n2 with [ x7 ⇒ P → P | _ ⇒ P ]
635 | x8 ⇒ match n2 with [ x8 ⇒ P → P | _ ⇒ P ] | x9 ⇒ match n2 with [ x9 ⇒ P → P | _ ⇒ P ]
636 | xA ⇒ match n2 with [ xA ⇒ P → P | _ ⇒ P ] | xB ⇒ match n2 with [ xB ⇒ P → P | _ ⇒ P ]
637 | xC ⇒ match n2 with [ xC ⇒ P → P | _ ⇒ P ] | xD ⇒ match n2 with [ xD ⇒ P → P | _ ⇒ P ]
638 | xE ⇒ match n2 with [ xE ⇒ P → P | _ ⇒ P ] | xF ⇒ match n2 with [ xF ⇒ P → P | _ ⇒ P ]]
643 ##[ ##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;
644 napply (False_ind ??);
645 nchange with (match MODE_TNY n1 with [ MODE_TNY a ⇒ False | _ ⇒ True ]);
646 nrewrite > H; nnormalize; napply I
647 ##| ##31,32,34: #n; #H;
648 napply (False_ind ??);
649 nchange with (match MODE_TNY n1 with [ MODE_TNY n1 ⇒ False | _ ⇒ True ]);
650 nrewrite > H; nnormalize; napply I
655 ##[ ##1,18,35,52,69,86,103,120,137,154,171,188,205,222,239,256: #H; napply (λx:P.x)
656 ##| ##*: #H; napply (exadecim_destruct ??? (instr_mode_destruct_MODE_TNY ?? H))
660 nlemma instr_mode_destruct_MODE_SRT : ∀n1,n2.MODE_SRT n1 = MODE_SRT n2 → n1 = n2.
662 nchange with (match MODE_SRT n2 with [ MODE_SRT a ⇒ n1 = a | _ ⇒ False ]);
668 ndefinition instr_mode_destruct34 :
669 Πn1,i2.ΠP:Prop.MODE_SRT n1 = i2 →
671 [ MODE_SRT n2 ⇒ match n1 with
672 [ t00 ⇒ match n2 with [ t00 ⇒ P → P | _ ⇒ P ] | t01 ⇒ match n2 with [ t01 ⇒ P → P | _ ⇒ P ]
673 | t02 ⇒ match n2 with [ t02 ⇒ P → P | _ ⇒ P ] | t03 ⇒ match n2 with [ t03 ⇒ P → P | _ ⇒ P ]
674 | t04 ⇒ match n2 with [ t04 ⇒ P → P | _ ⇒ P ] | t05 ⇒ match n2 with [ t05 ⇒ P → P | _ ⇒ P ]
675 | t06 ⇒ match n2 with [ t06 ⇒ P → P | _ ⇒ P ] | t07 ⇒ match n2 with [ t07 ⇒ P → P | _ ⇒ P ]
676 | t08 ⇒ match n2 with [ t08 ⇒ P → P | _ ⇒ P ] | t09 ⇒ match n2 with [ t09 ⇒ P → P | _ ⇒ P ]
677 | t0A ⇒ match n2 with [ t0A ⇒ P → P | _ ⇒ P ] | t0B ⇒ match n2 with [ t0B ⇒ P → P | _ ⇒ P ]
678 | t0C ⇒ match n2 with [ t0C ⇒ P → P | _ ⇒ P ] | t0D ⇒ match n2 with [ t0D ⇒ P → P | _ ⇒ P ]
679 | t0E ⇒ match n2 with [ t0E ⇒ P → P | _ ⇒ P ] | t0F ⇒ match n2 with [ t0F ⇒ P → P | _ ⇒ P ]
680 | t10 ⇒ match n2 with [ t10 ⇒ P → P | _ ⇒ P ] | t11 ⇒ match n2 with [ t11 ⇒ P → P | _ ⇒ P ]
681 | t12 ⇒ match n2 with [ t12 ⇒ P → P | _ ⇒ P ] | t13 ⇒ match n2 with [ t13 ⇒ P → P | _ ⇒ P ]
682 | t14 ⇒ match n2 with [ t14 ⇒ P → P | _ ⇒ P ] | t15 ⇒ match n2 with [ t15 ⇒ P → P | _ ⇒ P ]
683 | t16 ⇒ match n2 with [ t16 ⇒ P → P | _ ⇒ P ] | t17 ⇒ match n2 with [ t17 ⇒ P → P | _ ⇒ P ]
684 | t18 ⇒ match n2 with [ t18 ⇒ P → P | _ ⇒ P ] | t19 ⇒ match n2 with [ t19 ⇒ P → P | _ ⇒ P ]
685 | t1A ⇒ match n2 with [ t1A ⇒ P → P | _ ⇒ P ] | t1B ⇒ match n2 with [ t1B ⇒ P → P | _ ⇒ P ]
686 | t1C ⇒ match n2 with [ t1C ⇒ P → P | _ ⇒ P ] | t1D ⇒ match n2 with [ t1D ⇒ P → P | _ ⇒ P ]
687 | t1E ⇒ match n2 with [ t1E ⇒ P → P | _ ⇒ P ] | t1F ⇒ match n2 with [ t1F ⇒ P → P | _ ⇒ P ]]
692 ##[ ##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;
693 napply (False_ind ??);
694 nchange with (match MODE_SRT n1 with [ MODE_SRT a ⇒ False | _ ⇒ True ]);
695 nrewrite > H; nnormalize; napply I
696 ##| ##31,32,33: #n; #H;
697 napply (False_ind ??);
698 nchange with (match MODE_SRT n1 with [ MODE_SRT n1 ⇒ False | _ ⇒ True ]);
699 nrewrite > H; nnormalize; napply I
702 ##[ ##1: ncases n2; nnormalize;
703 ##[ ##1: #H; napply (λx:P.x)
704 ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
706 ##| ##2: ncases n2; nnormalize;
707 ##[ ##2: #H; napply (λx:P.x)
708 ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
710 ##| ##3: ncases n2; nnormalize;
711 ##[ ##3: #H; napply (λx:P.x)
712 ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
714 ##| ##4: ncases n2; nnormalize;
715 ##[ ##4: #H; napply (λx:P.x)
716 ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
718 ##| ##5: ncases n2; nnormalize;
719 ##[ ##5: #H; napply (λx:P.x)
720 ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
722 ##| ##6: ncases n2; nnormalize;
723 ##[ ##6: #H; napply (λx:P.x)
724 ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
726 ##| ##7: ncases n2; nnormalize;
727 ##[ ##7: #H; napply (λx:P.x)
728 ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
730 ##| ##8: ncases n2; nnormalize;
731 ##[ ##8: #H; napply (λx:P.x)
732 ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
734 ##| ##9: ncases n2; nnormalize;
735 ##[ ##9: #H; napply (λx:P.x)
736 ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
738 ##| ##10: ncases n2; nnormalize;
739 ##[ ##10: #H; napply (λx:P.x)
740 ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
742 ##| ##11: ncases n2; nnormalize;
743 ##[ ##11: #H; napply (λx:P.x)
744 ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
746 ##| ##12: ncases n2; nnormalize;
747 ##[ ##12: #H; napply (λx:P.x)
748 ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
750 ##| ##13: ncases n2; nnormalize;
751 ##[ ##13: #H; napply (λx:P.x)
752 ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
754 ##| ##14: ncases n2; nnormalize;
755 ##[ ##14: #H; napply (λx:P.x)
756 ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
758 ##| ##15: ncases n2; nnormalize;
759 ##[ ##15: #H; napply (λx:P.x)
760 ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
762 ##| ##16: ncases n2; nnormalize;
763 ##[ ##16: #H; napply (λx:P.x)
764 ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
766 ##| ##17: ncases n2; nnormalize;
767 ##[ ##17: #H; napply (λx:P.x)
768 ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
770 ##| ##18: ncases n2; nnormalize;
771 ##[ ##18: #H; napply (λx:P.x)
772 ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
774 ##| ##19: ncases n2; nnormalize;
775 ##[ ##19: #H; napply (λx:P.x)
776 ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
778 ##| ##20: ncases n2; nnormalize;
779 ##[ ##20: #H; napply (λx:P.x)
780 ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
782 ##| ##21: ncases n2; nnormalize;
783 ##[ ##21: #H; napply (λx:P.x)
784 ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
786 ##| ##22: ncases n2; nnormalize;
787 ##[ ##22: #H; napply (λx:P.x)
788 ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
790 ##| ##23: ncases n2; nnormalize;
791 ##[ ##23: #H; napply (λx:P.x)
792 ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
794 ##| ##24: ncases n2; nnormalize;
795 ##[ ##24: #H; napply (λx:P.x)
796 ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
798 ##| ##25: ncases n2; nnormalize;
799 ##[ ##25: #H; napply (λx:P.x)
800 ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
802 ##| ##26: ncases n2; nnormalize;
803 ##[ ##26: #H; napply (λx:P.x)
804 ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
806 ##| ##27: ncases n2; nnormalize;
807 ##[ ##27: #H; napply (λx:P.x)
808 ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
810 ##| ##28: ncases n2; nnormalize;
811 ##[ ##28: #H; napply (λx:P.x)
812 ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
814 ##| ##29: ncases n2; nnormalize;
815 ##[ ##29: #H; napply (λx:P.x)
816 ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
818 ##| ##30: ncases n2; nnormalize;
819 ##[ ##30: #H; napply (λx:P.x)
820 ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
822 ##| ##31: ncases n2; nnormalize;
823 ##[ ##31: #H; napply (λx:P.x)
824 ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
826 ##| ##32: ncases n2; nnormalize;
827 ##[ ##32: #H; napply (λx:P.x)
828 ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
834 ndefinition instr_mode_destruct_aux ≝
835 Πi1,i2.ΠP:Prop.i1 = i2 →
837 [ MODE_INH ⇒ match i2 with [ MODE_INH ⇒ P → P | _ ⇒ P ]
838 | MODE_INHA ⇒ match i2 with [ MODE_INHA ⇒ P → P | _ ⇒ P ]
839 | MODE_INHX ⇒ match i2 with [ MODE_INHX ⇒ P → P | _ ⇒ P ]
840 | MODE_INHH ⇒ match i2 with [ MODE_INHH ⇒ P → P | _ ⇒ P ]
841 | MODE_INHX0ADD ⇒ match i2 with [ MODE_INHX0ADD ⇒ P → P | _ ⇒ P ]
842 | MODE_INHX1ADD ⇒ match i2 with [ MODE_INHX1ADD ⇒ P → P | _ ⇒ P ]
843 | MODE_INHX2ADD ⇒ match i2 with [ MODE_INHX2ADD ⇒ P → P | _ ⇒ P ]
844 | MODE_IMM1 ⇒ match i2 with [ MODE_IMM1 ⇒ P → P | _ ⇒ P ]
845 | MODE_IMM1EXT ⇒ match i2 with [ MODE_IMM1EXT ⇒ P → P | _ ⇒ P ]
846 | MODE_IMM2 ⇒ match i2 with [ MODE_IMM2 ⇒ P → P | _ ⇒ P ]
847 | MODE_DIR1 ⇒ match i2 with [ MODE_DIR1 ⇒ P → P | _ ⇒ P ]
848 | MODE_DIR2 ⇒ match i2 with [ MODE_DIR2 ⇒ P → P | _ ⇒ P ]
849 | MODE_IX0 ⇒ match i2 with [ MODE_IX0 ⇒ P → P | _ ⇒ P ]
850 | MODE_IX1 ⇒ match i2 with [ MODE_IX1 ⇒ P → P | _ ⇒ P ]
851 | MODE_IX2 ⇒ match i2 with [ MODE_IX2 ⇒ P → P | _ ⇒ P ]
852 | MODE_SP1 ⇒ match i2 with [ MODE_SP1 ⇒ P → P | _ ⇒ P ]
853 | MODE_SP2 ⇒ match i2 with [ MODE_SP2 ⇒ P → P | _ ⇒ P ]
854 | MODE_DIR1_to_DIR1 ⇒ match i2 with [ MODE_DIR1_to_DIR1 ⇒ P → P | _ ⇒ P ]
855 | MODE_IMM1_to_DIR1 ⇒ match i2 with [ MODE_IMM1_to_DIR1 ⇒ P → P | _ ⇒ P ]
856 | MODE_IX0p_to_DIR1 ⇒ match i2 with [ MODE_IX0p_to_DIR1 ⇒ P → P | _ ⇒ P ]
857 | MODE_DIR1_to_IX0p ⇒ match i2 with [ MODE_DIR1_to_IX0p ⇒ P → P | _ ⇒ P ]
858 | MODE_INHA_and_IMM1 ⇒ match i2 with [ MODE_INHA_and_IMM1 ⇒ P → P | _ ⇒ P ]
859 | MODE_INHX_and_IMM1 ⇒ match i2 with [ MODE_INHX_and_IMM1 ⇒ P → P | _ ⇒ P ]
860 | MODE_IMM1_and_IMM1 ⇒ match i2 with [ MODE_IMM1_and_IMM1 ⇒ P → P | _ ⇒ P ]
861 | MODE_DIR1_and_IMM1 ⇒ match i2 with [ MODE_DIR1_and_IMM1 ⇒ P → P | _ ⇒ P ]
862 | MODE_IX0_and_IMM1 ⇒ match i2 with [ MODE_IX0_and_IMM1 ⇒ P → P | _ ⇒ P ]
863 | MODE_IX0p_and_IMM1 ⇒ match i2 with [ MODE_IX0p_and_IMM1 ⇒ P → P | _ ⇒ P ]
864 | MODE_IX1_and_IMM1 ⇒ match i2 with [ MODE_IX1_and_IMM1 ⇒ P → P | _ ⇒ P ]
865 | MODE_IX1p_and_IMM1 ⇒ match i2 with [ MODE_IX1p_and_IMM1 ⇒ P → P | _ ⇒ P ]
866 | MODE_SP1_and_IMM1 ⇒ match i2 with [ MODE_SP1_and_IMM1 ⇒ P → P | _ ⇒ P ]
867 | MODE_DIRn n1 ⇒ match i2 with
868 [ MODE_DIRn n2 ⇒ match n1 with
869 [ o0 ⇒ match n2 with [ o0 ⇒ P → P | _ ⇒ P ] | o1 ⇒ match n2 with [ o1 ⇒ P → P | _ ⇒ P ]
870 | o2 ⇒ match n2 with [ o2 ⇒ P → P | _ ⇒ P ] | o3 ⇒ match n2 with [ o3 ⇒ P → P | _ ⇒ P ]
871 | o4 ⇒ match n2 with [ o4 ⇒ P → P | _ ⇒ P ] | o5 ⇒ match n2 with [ o5 ⇒ P → P | _ ⇒ P ]
872 | o6 ⇒ match n2 with [ o6 ⇒ P → P | _ ⇒ P ] | o7 ⇒ match n2 with [ o7 ⇒ P → P | _ ⇒ P ]]
874 | MODE_DIRn_and_IMM1 n1 ⇒ match i2 with
875 [ MODE_DIRn_and_IMM1 n2 ⇒ match n1 with
876 [ o0 ⇒ match n2 with [ o0 ⇒ P → P | _ ⇒ P ] | o1 ⇒ match n2 with [ o1 ⇒ P → P | _ ⇒ P ]
877 | o2 ⇒ match n2 with [ o2 ⇒ P → P | _ ⇒ P ] | o3 ⇒ match n2 with [ o3 ⇒ P → P | _ ⇒ P ]
878 | o4 ⇒ match n2 with [ o4 ⇒ P → P | _ ⇒ P ] | o5 ⇒ match n2 with [ o5 ⇒ P → P | _ ⇒ P ]
879 | o6 ⇒ match n2 with [ o6 ⇒ P → P | _ ⇒ P ] | o7 ⇒ match n2 with [ o7 ⇒ P → P | _ ⇒ P ]]
881 | MODE_TNY e1 ⇒ match i2 with
882 [ MODE_TNY e2 ⇒ match e1 with
883 [ x0 ⇒ match e2 with [ x0 ⇒ P → P | _ ⇒ P ] | x1 ⇒ match e2 with [ x1 ⇒ P → P | _ ⇒ P ]
884 | x2 ⇒ match e2 with [ x2 ⇒ P → P | _ ⇒ P ] | x3 ⇒ match e2 with [ x3 ⇒ P → P | _ ⇒ P ]
885 | x4 ⇒ match e2 with [ x4 ⇒ P → P | _ ⇒ P ] | x5 ⇒ match e2 with [ x5 ⇒ P → P | _ ⇒ P ]
886 | x6 ⇒ match e2 with [ x6 ⇒ P → P | _ ⇒ P ] | x7 ⇒ match e2 with [ x7 ⇒ P → P | _ ⇒ P ]
887 | x8 ⇒ match e2 with [ x8 ⇒ P → P | _ ⇒ P ] | x9 ⇒ match e2 with [ x9 ⇒ P → P | _ ⇒ P ]
888 | xA ⇒ match e2 with [ xA ⇒ P → P | _ ⇒ P ] | xB ⇒ match e2 with [ xB ⇒ P → P | _ ⇒ P ]
889 | xC ⇒ match e2 with [ xC ⇒ P → P | _ ⇒ P ] | xD ⇒ match e2 with [ xD ⇒ P → P | _ ⇒ P ]
890 | xE ⇒ match e2 with [ xE ⇒ P → P | _ ⇒ P ] | xF ⇒ match e2 with [ xF ⇒ P → P | _ ⇒ P ]]
892 | MODE_SRT t1 ⇒ match i2 with
893 [ MODE_SRT t2 ⇒ match t1 with
894 [ t00 ⇒ match t2 with [ t00 ⇒ P → P | _ ⇒ P ] | t01 ⇒ match t2 with [ t01 ⇒ P → P | _ ⇒ P ]
895 | t02 ⇒ match t2 with [ t02 ⇒ P → P | _ ⇒ P ] | t03 ⇒ match t2 with [ t03 ⇒ P → P | _ ⇒ P ]
896 | t04 ⇒ match t2 with [ t04 ⇒ P → P | _ ⇒ P ] | t05 ⇒ match t2 with [ t05 ⇒ P → P | _ ⇒ P ]
897 | t06 ⇒ match t2 with [ t06 ⇒ P → P | _ ⇒ P ] | t07 ⇒ match t2 with [ t07 ⇒ P → P | _ ⇒ P ]
898 | t08 ⇒ match t2 with [ t08 ⇒ P → P | _ ⇒ P ] | t09 ⇒ match t2 with [ t09 ⇒ P → P | _ ⇒ P ]
899 | t0A ⇒ match t2 with [ t0A ⇒ P → P | _ ⇒ P ] | t0B ⇒ match t2 with [ t0B ⇒ P → P | _ ⇒ P ]
900 | t0C ⇒ match t2 with [ t0C ⇒ P → P | _ ⇒ P ] | t0D ⇒ match t2 with [ t0D ⇒ P → P | _ ⇒ P ]
901 | t0E ⇒ match t2 with [ t0E ⇒ P → P | _ ⇒ P ] | t0F ⇒ match t2 with [ t0F ⇒ P → P | _ ⇒ P ]
902 | t10 ⇒ match t2 with [ t10 ⇒ P → P | _ ⇒ P ] | t11 ⇒ match t2 with [ t11 ⇒ P → P | _ ⇒ P ]
903 | t12 ⇒ match t2 with [ t12 ⇒ P → P | _ ⇒ P ] | t13 ⇒ match t2 with [ t13 ⇒ P → P | _ ⇒ P ]
904 | t14 ⇒ match t2 with [ t14 ⇒ P → P | _ ⇒ P ] | t15 ⇒ match t2 with [ t15 ⇒ P → P | _ ⇒ P ]
905 | t16 ⇒ match t2 with [ t16 ⇒ P → P | _ ⇒ P ] | t17 ⇒ match t2 with [ t17 ⇒ P → P | _ ⇒ P ]
906 | t18 ⇒ match t2 with [ t18 ⇒ P → P | _ ⇒ P ] | t19 ⇒ match t2 with [ t19 ⇒ P → P | _ ⇒ P ]
907 | t1A ⇒ match t2 with [ t1A ⇒ P → P | _ ⇒ P ] | t1B ⇒ match t2 with [ t1B ⇒ P → P | _ ⇒ P ]
908 | t1C ⇒ match t2 with [ t1C ⇒ P → P | _ ⇒ P ] | t1D ⇒ match t2 with [ t1D ⇒ P → P | _ ⇒ P ]
909 | t1E ⇒ match t2 with [ t1E ⇒ P → P | _ ⇒ P ] | t1F ⇒ match t2 with [ t1F ⇒ P → P | _ ⇒ P ]]
913 ndefinition instr_mode_destruct : instr_mode_destruct_aux.
915 ##[ ##1: napply instr_mode_destruct1 ##| ##2: napply instr_mode_destruct2
916 ##| ##3: napply instr_mode_destruct3 ##| ##4: napply instr_mode_destruct4
917 ##| ##5: napply instr_mode_destruct5 ##| ##6: napply instr_mode_destruct6
918 ##| ##7: napply instr_mode_destruct7 ##| ##8: napply instr_mode_destruct8
919 ##| ##9: napply instr_mode_destruct9 ##| ##10: napply instr_mode_destruct10
920 ##| ##11: napply instr_mode_destruct11 ##| ##12: napply instr_mode_destruct12
921 ##| ##13: napply instr_mode_destruct13 ##| ##14: napply instr_mode_destruct14
922 ##| ##15: napply instr_mode_destruct15 ##| ##16: napply instr_mode_destruct16
923 ##| ##17: napply instr_mode_destruct17 ##| ##18: napply instr_mode_destruct18
924 ##| ##19: napply instr_mode_destruct19 ##| ##20: napply instr_mode_destruct20
925 ##| ##21: napply instr_mode_destruct21 ##| ##22: napply instr_mode_destruct22
926 ##| ##23: napply instr_mode_destruct23 ##| ##24: napply instr_mode_destruct24
927 ##| ##25: napply instr_mode_destruct25 ##| ##26: napply instr_mode_destruct26
928 ##| ##27: napply instr_mode_destruct27 ##| ##28: napply instr_mode_destruct28
929 ##| ##29: napply instr_mode_destruct29 ##| ##30: napply instr_mode_destruct30
930 ##| ##31: napply instr_mode_destruct31 ##| ##32: napply instr_mode_destruct32
931 ##| ##33: napply instr_mode_destruct33 ##| ##34: napply instr_mode_destruct34