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/aux_bases_lemmas.ma".
24 include "freescale/exadecim_lemmas.ma".
25 include "freescale/opcode_base.ma".
27 (* ********************************************** *)
28 (* MATTONI BASE PER DEFINIRE LE TABELLE DELLE MCU *)
29 (* ********************************************** *)
31 ndefinition instr_mode_destruct1 :
32 Πi2.ΠP:Prop.MODE_INH = i2 → match i2 with [ MODE_INH ⇒ P → P | _ ⇒ P ].
36 ##[ ##1: #H; napply (λx:P.x)
37 ##| ##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;
38 napply (False_ind (λ_.?) ?);
39 nchange with (match MODE_INH with [ MODE_INH ⇒ False | _ ⇒ True ]);
40 nrewrite > H; nnormalize; napply I
41 ##| ##31,32,33,34: #n; #H;
42 napply (False_ind (λ_.?) ?);
43 nchange with (match MODE_INH with [ MODE_INH ⇒ False | _ ⇒ True ]);
44 nrewrite > H; nnormalize; napply I
48 ndefinition instr_mode_destruct2 :
49 Πi2.ΠP:Prop.MODE_INHA = i2 → match i2 with [ MODE_INHA ⇒ P → P | _ ⇒ P ].
53 ##[ ##2: #H; napply (λx:P.x)
54 ##| ##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;
55 napply (False_ind (λ_.?) ?);
56 nchange with (match MODE_INHA with [ MODE_INHA ⇒ False | _ ⇒ True ]);
57 nrewrite > H; nnormalize; napply I
58 ##| ##31,32,33,34: #n; #H;
59 napply (False_ind (λ_.?) ?);
60 nchange with (match MODE_INHA with [ MODE_INHA ⇒ False | _ ⇒ True ]);
61 nrewrite > H; nnormalize; napply I
65 ndefinition instr_mode_destruct3 :
66 Πi2.ΠP:Prop.MODE_INHX = i2 → match i2 with [ MODE_INHX ⇒ P → P | _ ⇒ P ].
70 ##[ ##3: #H; napply (λx:P.x)
71 ##| ##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;
72 napply (False_ind (λ_.?) ?);
73 nchange with (match MODE_INHX with [ MODE_INHX ⇒ False | _ ⇒ True ]);
74 nrewrite > H; nnormalize; napply I
75 ##| ##31,32,33,34: #n; #H;
76 napply (False_ind (λ_.?) ?);
77 nchange with (match MODE_INHX with [ MODE_INHX ⇒ False | _ ⇒ True ]);
78 nrewrite > H; nnormalize; napply I
82 ndefinition instr_mode_destruct4 :
83 Πi2.ΠP:Prop.MODE_INHH = i2 → match i2 with [ MODE_INHH ⇒ P → P | _ ⇒ P ].
87 ##[ ##4: #H; napply (λx:P.x)
88 ##| ##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;
89 napply (False_ind (λ_.?) ?);
90 nchange with (match MODE_INHH with [ MODE_INHH ⇒ False | _ ⇒ True ]);
91 nrewrite > H; nnormalize; napply I
92 ##| ##31,32,33,34: #n; #H;
93 napply (False_ind (λ_.?) ?);
94 nchange with (match MODE_INHH with [ MODE_INHH ⇒ False | _ ⇒ True ]);
95 nrewrite > H; nnormalize; napply I
99 ndefinition instr_mode_destruct5 :
100 Πi2.ΠP:Prop.MODE_INHX0ADD = i2 → match i2 with [ MODE_INHX0ADD ⇒ P → P | _ ⇒ P ].
104 ##[ ##5: #H; napply (λx:P.x)
105 ##| ##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;
106 napply (False_ind (λ_.?) ?);
107 nchange with (match MODE_INHX0ADD with [ MODE_INHX0ADD ⇒ False | _ ⇒ True ]);
108 nrewrite > H; nnormalize; napply I
109 ##| ##31,32,33,34: #n; #H;
110 napply (False_ind (λ_.?) ?);
111 nchange with (match MODE_INHX0ADD with [ MODE_INHX0ADD ⇒ False | _ ⇒ True ]);
112 nrewrite > H; nnormalize; napply I
116 ndefinition instr_mode_destruct6 :
117 Πi2.ΠP:Prop.MODE_INHX1ADD = i2 → match i2 with [ MODE_INHX1ADD ⇒ P → P | _ ⇒ P ].
121 ##[ ##6: #H; napply (λx:P.x)
122 ##| ##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;
123 napply (False_ind (λ_.?) ?);
124 nchange with (match MODE_INHX1ADD with [ MODE_INHX1ADD ⇒ False | _ ⇒ True ]);
125 nrewrite > H; nnormalize; napply I
126 ##| ##31,32,33,34: #n; #H;
127 napply (False_ind (λ_.?) ?);
128 nchange with (match MODE_INHX1ADD with [ MODE_INHX1ADD ⇒ False | _ ⇒ True ]);
129 nrewrite > H; nnormalize; napply I
133 ndefinition instr_mode_destruct7 :
134 Πi2.ΠP:Prop.MODE_INHX2ADD = i2 → match i2 with [ MODE_INHX2ADD ⇒ P → P | _ ⇒ P ].
138 ##[ ##7: #H; napply (λx:P.x)
139 ##| ##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;
140 napply (False_ind (λ_.?) ?);
141 nchange with (match MODE_INHX2ADD with [ MODE_INHX2ADD ⇒ False | _ ⇒ True ]);
142 nrewrite > H; nnormalize; napply I
143 ##| ##31,32,33,34: #n; #H;
144 napply (False_ind (λ_.?) ?);
145 nchange with (match MODE_INHX2ADD with [ MODE_INHX2ADD ⇒ False | _ ⇒ True ]);
146 nrewrite > H; nnormalize; napply I
150 ndefinition instr_mode_destruct8 :
151 Πi2.ΠP:Prop.MODE_IMM1 = i2 → match i2 with [ MODE_IMM1 ⇒ P → P | _ ⇒ P ].
155 ##[ ##8: #H; napply (λx:P.x)
156 ##| ##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;
157 napply (False_ind (λ_.?) ?);
158 nchange with (match MODE_IMM1 with [ MODE_IMM1 ⇒ False | _ ⇒ True ]);
159 nrewrite > H; nnormalize; napply I
160 ##| ##31,32,33,34: #n; #H;
161 napply (False_ind (λ_.?) ?);
162 nchange with (match MODE_IMM1 with [ MODE_IMM1 ⇒ False | _ ⇒ True ]);
163 nrewrite > H; nnormalize; napply I
167 ndefinition instr_mode_destruct9 :
168 Πi2.ΠP:Prop.MODE_IMM1EXT = i2 → match i2 with [ MODE_IMM1EXT ⇒ P → P | _ ⇒ P ].
172 ##[ ##9: #H; napply (λx:P.x)
173 ##| ##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;
174 napply (False_ind (λ_.?) ?);
175 nchange with (match MODE_IMM1EXT with [ MODE_IMM1EXT ⇒ False | _ ⇒ True ]);
176 nrewrite > H; nnormalize; napply I
177 ##| ##31,32,33,34: #n; #H;
178 napply (False_ind (λ_.?) ?);
179 nchange with (match MODE_IMM1EXT with [ MODE_IMM1EXT ⇒ False | _ ⇒ True ]);
180 nrewrite > H; nnormalize; napply I
184 ndefinition instr_mode_destruct10 :
185 Πi2.ΠP:Prop.MODE_IMM2 = i2 → match i2 with [ MODE_IMM2 ⇒ P → P | _ ⇒ P ].
189 ##[ ##10: #H; napply (λx:P.x)
190 ##| ##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;
191 napply (False_ind (λ_.?) ?);
192 nchange with (match MODE_IMM2 with [ MODE_IMM2 ⇒ False | _ ⇒ True ]);
193 nrewrite > H; nnormalize; napply I
194 ##| ##31,32,33,34: #n; #H;
195 napply (False_ind (λ_.?) ?);
196 nchange with (match MODE_IMM2 with [ MODE_IMM2 ⇒ False | _ ⇒ True ]);
197 nrewrite > H; nnormalize; napply I
201 ndefinition instr_mode_destruct11 :
202 Πi2.ΠP:Prop.MODE_DIR1 = i2 → match i2 with [ MODE_DIR1 ⇒ P → P | _ ⇒ P ].
206 ##[ ##11: #H; napply (λx:P.x)
207 ##| ##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;
208 napply (False_ind (λ_.?) ?);
209 nchange with (match MODE_DIR1 with [ MODE_DIR1 ⇒ False | _ ⇒ True ]);
210 nrewrite > H; nnormalize; napply I
211 ##| ##31,32,33,34: #n; #H;
212 napply (False_ind (λ_.?) ?);
213 nchange with (match MODE_DIR1 with [ MODE_DIR1 ⇒ False | _ ⇒ True ]);
214 nrewrite > H; nnormalize; napply I
218 ndefinition instr_mode_destruct12 :
219 Πi2.ΠP:Prop.MODE_DIR2 = i2 → match i2 with [ MODE_DIR2 ⇒ P → P | _ ⇒ P ].
223 ##[ ##12: #H; napply (λx:P.x)
224 ##| ##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;
225 napply (False_ind (λ_.?) ?);
226 nchange with (match MODE_DIR2 with [ MODE_DIR2 ⇒ False | _ ⇒ True ]);
227 nrewrite > H; nnormalize; napply I
228 ##| ##31,32,33,34: #n; #H;
229 napply (False_ind (λ_.?) ?);
230 nchange with (match MODE_DIR2 with [ MODE_DIR2 ⇒ False | _ ⇒ True ]);
231 nrewrite > H; nnormalize; napply I
235 ndefinition instr_mode_destruct13 :
236 Πi2.ΠP:Prop.MODE_IX0 = i2 → match i2 with [ MODE_IX0 ⇒ P → P | _ ⇒ P ].
240 ##[ ##13: #H; napply (λx:P.x)
241 ##| ##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;
242 napply (False_ind (λ_.?) ?);
243 nchange with (match MODE_IX0 with [ MODE_IX0 ⇒ False | _ ⇒ True ]);
244 nrewrite > H; nnormalize; napply I
245 ##| ##31,32,33,34: #n; #H;
246 napply (False_ind (λ_.?) ?);
247 nchange with (match MODE_IX0 with [ MODE_IX0 ⇒ False | _ ⇒ True ]);
248 nrewrite > H; nnormalize; napply I
252 ndefinition instr_mode_destruct14 :
253 Πi2.ΠP:Prop.MODE_IX1 = i2 → match i2 with [ MODE_IX1 ⇒ P → P | _ ⇒ P ].
257 ##[ ##14: #H; napply (λx:P.x)
258 ##| ##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;
259 napply (False_ind (λ_.?) ?);
260 nchange with (match MODE_IX1 with [ MODE_IX1 ⇒ False | _ ⇒ True ]);
261 nrewrite > H; nnormalize; napply I
262 ##| ##31,32,33,34: #n; #H;
263 napply (False_ind (λ_.?) ?);
264 nchange with (match MODE_IX1 with [ MODE_IX1 ⇒ False | _ ⇒ True ]);
265 nrewrite > H; nnormalize; napply I
269 ndefinition instr_mode_destruct15 :
270 Πi2.ΠP:Prop.MODE_IX2 = i2 → match i2 with [ MODE_IX2 ⇒ P → P | _ ⇒ P ].
274 ##[ ##15: #H; napply (λx:P.x)
275 ##| ##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;
276 napply (False_ind (λ_.?) ?);
277 nchange with (match MODE_IX2 with [ MODE_IX2 ⇒ False | _ ⇒ True ]);
278 nrewrite > H; nnormalize; napply I
279 ##| ##31,32,33,34: #n; #H;
280 napply (False_ind (λ_.?) ?);
281 nchange with (match MODE_IX2 with [ MODE_IX2 ⇒ False | _ ⇒ True ]);
282 nrewrite > H; nnormalize; napply I
286 ndefinition instr_mode_destruct16 :
287 Πi2.ΠP:Prop.MODE_SP1 = i2 → match i2 with [ MODE_SP1 ⇒ P → P | _ ⇒ P ].
291 ##[ ##16: #H; napply (λx:P.x)
292 ##| ##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;
293 napply (False_ind (λ_.?) ?);
294 nchange with (match MODE_SP1 with [ MODE_SP1 ⇒ False | _ ⇒ True ]);
295 nrewrite > H; nnormalize; napply I
296 ##| ##31,32,33,34: #n; #H;
297 napply (False_ind (λ_.?) ?);
298 nchange with (match MODE_SP1 with [ MODE_SP1 ⇒ False | _ ⇒ True ]);
299 nrewrite > H; nnormalize; napply I
303 ndefinition instr_mode_destruct17 :
304 Πi2.ΠP:Prop.MODE_SP2 = i2 → match i2 with [ MODE_SP2 ⇒ P → P | _ ⇒ P ].
308 ##[ ##17: #H; napply (λx:P.x)
309 ##| ##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;
310 napply (False_ind (λ_.?) ?);
311 nchange with (match MODE_SP2 with [ MODE_SP2 ⇒ False | _ ⇒ True ]);
312 nrewrite > H; nnormalize; napply I
313 ##| ##31,32,33,34: #n; #H;
314 napply (False_ind (λ_.?) ?);
315 nchange with (match MODE_SP2 with [ MODE_SP2 ⇒ False | _ ⇒ True ]);
316 nrewrite > H; nnormalize; napply I
320 ndefinition instr_mode_destruct18 :
321 Πi2.ΠP:Prop.MODE_DIR1_to_DIR1 = i2 → match i2 with [ MODE_DIR1_to_DIR1 ⇒ P → P | _ ⇒ P ].
325 ##[ ##18: #H; napply (λx:P.x)
326 ##| ##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;
327 napply (False_ind (λ_.?) ?);
328 nchange with (match MODE_DIR1_to_DIR1 with [ MODE_DIR1_to_DIR1 ⇒ False | _ ⇒ True ]);
329 nrewrite > H; nnormalize; napply I
330 ##| ##31,32,33,34: #n; #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
337 ndefinition instr_mode_destruct19 :
338 Πi2.ΠP:Prop.MODE_IMM1_to_DIR1 = i2 → match i2 with [ MODE_IMM1_to_DIR1 ⇒ P → P | _ ⇒ P ].
342 ##[ ##19: #H; napply (λx:P.x)
343 ##| ##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;
344 napply (False_ind (λ_.?) ?);
345 nchange with (match MODE_IMM1_to_DIR1 with [ MODE_IMM1_to_DIR1 ⇒ False | _ ⇒ True ]);
346 nrewrite > H; nnormalize; napply I
347 ##| ##31,32,33,34: #n; #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
354 ndefinition instr_mode_destruct20 :
355 Πi2.ΠP:Prop.MODE_IX0p_to_DIR1 = i2 → match i2 with [ MODE_IX0p_to_DIR1 ⇒ P → P | _ ⇒ P ].
359 ##[ ##20: #H; napply (λx:P.x)
360 ##| ##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;
361 napply (False_ind (λ_.?) ?);
362 nchange with (match MODE_IX0p_to_DIR1 with [ MODE_IX0p_to_DIR1 ⇒ False | _ ⇒ True ]);
363 nrewrite > H; nnormalize; napply I
364 ##| ##31,32,33,34: #n; #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
371 ndefinition instr_mode_destruct21 :
372 Πi2.ΠP:Prop.MODE_DIR1_to_IX0p = i2 → match i2 with [ MODE_DIR1_to_IX0p ⇒ P → P | _ ⇒ P ].
376 ##[ ##21: #H; napply (λx:P.x)
377 ##| ##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;
378 napply (False_ind (λ_.?) ?);
379 nchange with (match MODE_DIR1_to_IX0p with [ MODE_DIR1_to_IX0p ⇒ False | _ ⇒ True ]);
380 nrewrite > H; nnormalize; napply I
381 ##| ##31,32,33,34: #n; #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
388 ndefinition instr_mode_destruct22 :
389 Πi2.ΠP:Prop.MODE_INHA_and_IMM1 = i2 → match i2 with [ MODE_INHA_and_IMM1 ⇒ P → P | _ ⇒ P ].
393 ##[ ##22: #H; napply (λx:P.x)
394 ##| ##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;
395 napply (False_ind (λ_.?) ?);
396 nchange with (match MODE_INHA_and_IMM1 with [ MODE_INHA_and_IMM1 ⇒ False | _ ⇒ True ]);
397 nrewrite > H; nnormalize; napply I
398 ##| ##31,32,33,34: #n; #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
405 ndefinition instr_mode_destruct23 :
406 Πi2.ΠP:Prop.MODE_INHX_and_IMM1 = i2 → match i2 with [ MODE_INHX_and_IMM1 ⇒ P → P | _ ⇒ P ].
410 ##[ ##23: #H; napply (λx:P.x)
411 ##| ##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;
412 napply (False_ind (λ_.?) ?);
413 nchange with (match MODE_INHX_and_IMM1 with [ MODE_INHX_and_IMM1 ⇒ False | _ ⇒ True ]);
414 nrewrite > H; nnormalize; napply I
415 ##| ##31,32,33,34: #n; #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
422 ndefinition instr_mode_destruct24 :
423 Πi2.ΠP:Prop.MODE_IMM1_and_IMM1 = i2 → match i2 with [ MODE_IMM1_and_IMM1 ⇒ P → P | _ ⇒ P ].
427 ##[ ##24: #H; napply (λx:P.x)
428 ##| ##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;
429 napply (False_ind (λ_.?) ?);
430 nchange with (match MODE_IMM1_and_IMM1 with [ MODE_IMM1_and_IMM1 ⇒ False | _ ⇒ True ]);
431 nrewrite > H; nnormalize; napply I
432 ##| ##31,32,33,34: #n; #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
439 ndefinition instr_mode_destruct25 :
440 Πi2.ΠP:Prop.MODE_DIR1_and_IMM1 = i2 → match i2 with [ MODE_DIR1_and_IMM1 ⇒ P → P | _ ⇒ P ].
444 ##[ ##25: #H; napply (λx:P.x)
445 ##| ##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;
446 napply (False_ind (λ_.?) ?);
447 nchange with (match MODE_DIR1_and_IMM1 with [ MODE_DIR1_and_IMM1 ⇒ False | _ ⇒ True ]);
448 nrewrite > H; nnormalize; napply I
449 ##| ##31,32,33,34: #n; #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
456 ndefinition instr_mode_destruct26 :
457 Πi2.ΠP:Prop.MODE_IX0_and_IMM1 = i2 → match i2 with [ MODE_IX0_and_IMM1 ⇒ P → P | _ ⇒ P ].
461 ##[ ##26: #H; napply (λx:P.x)
462 ##| ##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;
463 napply (False_ind (λ_.?) ?);
464 nchange with (match MODE_IX0_and_IMM1 with [ MODE_IX0_and_IMM1 ⇒ False | _ ⇒ True ]);
465 nrewrite > H; nnormalize; napply I
466 ##| ##31,32,33,34: #n; #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
473 ndefinition instr_mode_destruct27 :
474 Πi2.ΠP:Prop.MODE_IX0p_and_IMM1 = i2 → match i2 with [ MODE_IX0p_and_IMM1 ⇒ P → P | _ ⇒ P ].
478 ##[ ##27: #H; napply (λx:P.x)
479 ##| ##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;
480 napply (False_ind (λ_.?) ?);
481 nchange with (match MODE_IX0p_and_IMM1 with [ MODE_IX0p_and_IMM1 ⇒ False | _ ⇒ True ]);
482 nrewrite > H; nnormalize; napply I
483 ##| ##31,32,33,34: #n; #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
490 ndefinition instr_mode_destruct28 :
491 Πi2.ΠP:Prop.MODE_IX1_and_IMM1 = i2 → match i2 with [ MODE_IX1_and_IMM1 ⇒ P → P | _ ⇒ P ].
495 ##[ ##28: #H; napply (λx:P.x)
496 ##| ##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;
497 napply (False_ind (λ_.?) ?);
498 nchange with (match MODE_IX1_and_IMM1 with [ MODE_IX1_and_IMM1 ⇒ False | _ ⇒ True ]);
499 nrewrite > H; nnormalize; napply I
500 ##| ##31,32,33,34: #n; #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
507 ndefinition instr_mode_destruct29 :
508 Πi2.ΠP:Prop.MODE_IX1p_and_IMM1 = i2 → match i2 with [ MODE_IX1p_and_IMM1 ⇒ P → P | _ ⇒ P ].
512 ##[ ##29: #H; napply (λx:P.x)
513 ##| ##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;
514 napply (False_ind (λ_.?) ?);
515 nchange with (match MODE_IX1p_and_IMM1 with [ MODE_IX1p_and_IMM1 ⇒ False | _ ⇒ True ]);
516 nrewrite > H; nnormalize; napply I
517 ##| ##31,32,33,34: #n; #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
524 ndefinition instr_mode_destruct30 :
525 Πi2.ΠP:Prop.MODE_SP1_and_IMM1 = i2 → match i2 with [ MODE_SP1_and_IMM1 ⇒ P → P | _ ⇒ P ].
529 ##[ ##30: #H; napply (λx:P.x)
530 ##| ##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;
531 napply (False_ind (λ_.?) ?);
532 nchange with (match MODE_SP1_and_IMM1 with [ MODE_SP1_and_IMM1 ⇒ False | _ ⇒ True ]);
533 nrewrite > H; nnormalize; napply I
534 ##| ##31,32,33,34: #n; #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
541 nlemma instr_mode_destruct_MODE_DIRn : ∀n1,n2.MODE_DIRn n1 = MODE_DIRn n2 → n1 = n2.
543 nchange with (match MODE_DIRn n2 with [ MODE_DIRn a ⇒ n1 = a | _ ⇒ False ]);
549 ndefinition instr_mode_destruct31 :
550 Πn1,i2.ΠP:Prop.MODE_DIRn n1 = i2 →
552 [ MODE_DIRn n2 ⇒ match n1 with
553 [ o0 ⇒ match n2 with [ o0 ⇒ P → P | _ ⇒ P ] | o1 ⇒ match n2 with [ o1 ⇒ P → P | _ ⇒ P ]
554 | o2 ⇒ match n2 with [ o2 ⇒ P → P | _ ⇒ P ] | o3 ⇒ match n2 with [ o3 ⇒ P → P | _ ⇒ P ]
555 | o4 ⇒ match n2 with [ o4 ⇒ P → P | _ ⇒ P ] | o5 ⇒ match n2 with [ o5 ⇒ P → P | _ ⇒ P ]
556 | o6 ⇒ match n2 with [ o6 ⇒ P → P | _ ⇒ P ] | o7 ⇒ match n2 with [ o7 ⇒ P → P | _ ⇒ P ]]
561 ##[ ##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;
562 napply (False_ind (λ_.?) ?);
563 nchange with (match MODE_DIRn n1 with [ MODE_DIRn a ⇒ False | _ ⇒ True ]);
564 nrewrite > H; nnormalize; napply I
565 ##| ##32,33,34: #n; #H;
566 napply (False_ind (λ_.?) ?);
567 nchange with (match MODE_DIRn n1 with [ MODE_DIRn n1 ⇒ False | _ ⇒ True ]);
568 nrewrite > H; nnormalize; napply I
573 ##[ ##1,10,19,28,37,46,55,64: #H; napply (λx:P.x)
574 ##| ##*: #H; napply (oct_destruct ??? (instr_mode_destruct_MODE_DIRn ?? H))
578 nlemma instr_mode_destruct_MODE_DIRn_and_IMM1 : ∀n1,n2.MODE_DIRn_and_IMM1 n1 = MODE_DIRn_and_IMM1 n2 → n1 = n2.
580 nchange with (match MODE_DIRn_and_IMM1 n2 with [ MODE_DIRn_and_IMM1 a ⇒ n1 = a | _ ⇒ False ]);
586 ndefinition instr_mode_destruct32 :
587 Πn1,i2.ΠP:Prop.MODE_DIRn_and_IMM1 n1 = i2 →
589 [ MODE_DIRn_and_IMM1 n2 ⇒ match n1 with
590 [ o0 ⇒ match n2 with [ o0 ⇒ P → P | _ ⇒ P ] | o1 ⇒ match n2 with [ o1 ⇒ P → P | _ ⇒ P ]
591 | o2 ⇒ match n2 with [ o2 ⇒ P → P | _ ⇒ P ] | o3 ⇒ match n2 with [ o3 ⇒ P → P | _ ⇒ P ]
592 | o4 ⇒ match n2 with [ o4 ⇒ P → P | _ ⇒ P ] | o5 ⇒ match n2 with [ o5 ⇒ P → P | _ ⇒ P ]
593 | o6 ⇒ match n2 with [ o6 ⇒ P → P | _ ⇒ P ] | o7 ⇒ match n2 with [ o7 ⇒ P → P | _ ⇒ P ]]
598 ##[ ##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;
599 napply (False_ind (λ_.?) ?);
600 nchange with (match MODE_DIRn_and_IMM1 n1 with [ MODE_DIRn_and_IMM1 a ⇒ False | _ ⇒ True ]);
601 nrewrite > H; nnormalize; napply I
602 ##| ##31,33,34: #n; #H;
603 napply (False_ind (λ_.?) ?);
604 nchange with (match MODE_DIRn_and_IMM1 n1 with [ MODE_DIRn_and_IMM1 n1 ⇒ False | _ ⇒ True ]);
605 nrewrite > H; nnormalize; napply I
610 ##[ ##1,10,19,28,37,46,55,64: #H; napply (λx:P.x)
611 ##| ##*: #H; napply (oct_destruct ??? (instr_mode_destruct_MODE_DIRn_and_IMM1 ?? H))
615 nlemma instr_mode_destruct_MODE_TNY : ∀n1,n2.MODE_TNY n1 = MODE_TNY n2 → n1 = n2.
617 nchange with (match MODE_TNY n2 with [ MODE_TNY a ⇒ n1 = a | _ ⇒ False ]);
623 ndefinition instr_mode_destruct33 :
624 Πn1,i2.ΠP:Prop.MODE_TNY n1 = i2 →
626 [ MODE_TNY n2 ⇒ match n1 with
627 [ x0 ⇒ match n2 with [ x0 ⇒ P → P | _ ⇒ P ] | x1 ⇒ match n2 with [ x1 ⇒ P → P | _ ⇒ P ]
628 | x2 ⇒ match n2 with [ x2 ⇒ P → P | _ ⇒ P ] | x3 ⇒ match n2 with [ x3 ⇒ P → P | _ ⇒ P ]
629 | x4 ⇒ match n2 with [ x4 ⇒ P → P | _ ⇒ P ] | x5 ⇒ match n2 with [ x5 ⇒ P → P | _ ⇒ P ]
630 | x6 ⇒ match n2 with [ x6 ⇒ P → P | _ ⇒ P ] | x7 ⇒ match n2 with [ x7 ⇒ P → P | _ ⇒ P ]
631 | x8 ⇒ match n2 with [ x8 ⇒ P → P | _ ⇒ P ] | x9 ⇒ match n2 with [ x9 ⇒ P → P | _ ⇒ P ]
632 | xA ⇒ match n2 with [ xA ⇒ P → P | _ ⇒ P ] | xB ⇒ match n2 with [ xB ⇒ P → P | _ ⇒ P ]
633 | xC ⇒ match n2 with [ xC ⇒ P → P | _ ⇒ P ] | xD ⇒ match n2 with [ xD ⇒ P → P | _ ⇒ P ]
634 | xE ⇒ match n2 with [ xE ⇒ P → P | _ ⇒ P ] | xF ⇒ match n2 with [ xF ⇒ P → P | _ ⇒ P ]]
639 ##[ ##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;
640 napply (False_ind (λ_.?) ?);
641 nchange with (match MODE_TNY n1 with [ MODE_TNY a ⇒ False | _ ⇒ True ]);
642 nrewrite > H; nnormalize; napply I
643 ##| ##31,32,34: #n; #H;
644 napply (False_ind (λ_.?) ?);
645 nchange with (match MODE_TNY n1 with [ MODE_TNY n1 ⇒ False | _ ⇒ True ]);
646 nrewrite > H; nnormalize; napply I
651 ##[ ##1,18,35,52,69,86,103,120,137,154,171,188,205,222,239,256: #H; napply (λx:P.x)
652 ##| ##*: #H; napply (exadecim_destruct ??? (instr_mode_destruct_MODE_TNY ?? H))
656 nlemma instr_mode_destruct_MODE_SRT : ∀n1,n2.MODE_SRT n1 = MODE_SRT n2 → n1 = n2.
658 nchange with (match MODE_SRT n2 with [ MODE_SRT a ⇒ n1 = a | _ ⇒ False ]);
664 ndefinition instr_mode_destruct34 :
665 Πn1,i2.ΠP:Prop.MODE_SRT n1 = i2 →
667 [ MODE_SRT n2 ⇒ match n1 with
668 [ t00 ⇒ match n2 with [ t00 ⇒ P → P | _ ⇒ P ] | t01 ⇒ match n2 with [ t01 ⇒ P → P | _ ⇒ P ]
669 | t02 ⇒ match n2 with [ t02 ⇒ P → P | _ ⇒ P ] | t03 ⇒ match n2 with [ t03 ⇒ P → P | _ ⇒ P ]
670 | t04 ⇒ match n2 with [ t04 ⇒ P → P | _ ⇒ P ] | t05 ⇒ match n2 with [ t05 ⇒ P → P | _ ⇒ P ]
671 | t06 ⇒ match n2 with [ t06 ⇒ P → P | _ ⇒ P ] | t07 ⇒ match n2 with [ t07 ⇒ P → P | _ ⇒ P ]
672 | t08 ⇒ match n2 with [ t08 ⇒ P → P | _ ⇒ P ] | t09 ⇒ match n2 with [ t09 ⇒ P → P | _ ⇒ P ]
673 | t0A ⇒ match n2 with [ t0A ⇒ P → P | _ ⇒ P ] | t0B ⇒ match n2 with [ t0B ⇒ P → P | _ ⇒ P ]
674 | t0C ⇒ match n2 with [ t0C ⇒ P → P | _ ⇒ P ] | t0D ⇒ match n2 with [ t0D ⇒ P → P | _ ⇒ P ]
675 | t0E ⇒ match n2 with [ t0E ⇒ P → P | _ ⇒ P ] | t0F ⇒ match n2 with [ t0F ⇒ P → P | _ ⇒ P ]
676 | t10 ⇒ match n2 with [ t10 ⇒ P → P | _ ⇒ P ] | t11 ⇒ match n2 with [ t11 ⇒ P → P | _ ⇒ P ]
677 | t12 ⇒ match n2 with [ t12 ⇒ P → P | _ ⇒ P ] | t13 ⇒ match n2 with [ t13 ⇒ P → P | _ ⇒ P ]
678 | t14 ⇒ match n2 with [ t14 ⇒ P → P | _ ⇒ P ] | t15 ⇒ match n2 with [ t15 ⇒ P → P | _ ⇒ P ]
679 | t16 ⇒ match n2 with [ t16 ⇒ P → P | _ ⇒ P ] | t17 ⇒ match n2 with [ t17 ⇒ P → P | _ ⇒ P ]
680 | t18 ⇒ match n2 with [ t18 ⇒ P → P | _ ⇒ P ] | t19 ⇒ match n2 with [ t19 ⇒ P → P | _ ⇒ P ]
681 | t1A ⇒ match n2 with [ t1A ⇒ P → P | _ ⇒ P ] | t1B ⇒ match n2 with [ t1B ⇒ P → P | _ ⇒ P ]
682 | t1C ⇒ match n2 with [ t1C ⇒ P → P | _ ⇒ P ] | t1D ⇒ match n2 with [ t1D ⇒ P → P | _ ⇒ P ]
683 | t1E ⇒ match n2 with [ t1E ⇒ P → P | _ ⇒ P ] | t1F ⇒ match n2 with [ t1F ⇒ P → P | _ ⇒ P ]]
688 ##[ ##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;
689 napply (False_ind (λ_.?) ?);
690 nchange with (match MODE_SRT n1 with [ MODE_SRT a ⇒ False | _ ⇒ True ]);
691 nrewrite > H; nnormalize; napply I
692 ##| ##31,32,33: #n; #H;
693 napply (False_ind (λ_.?) ?);
694 nchange with (match MODE_SRT n1 with [ MODE_SRT n1 ⇒ False | _ ⇒ True ]);
695 nrewrite > H; nnormalize; napply I
698 ##[ ##1: ncases n2; nnormalize;
699 ##[ ##1: #H; napply (λx:P.x)
700 ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
702 ##| ##2: ncases n2; nnormalize;
703 ##[ ##2: #H; napply (λx:P.x)
704 ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
706 ##| ##3: ncases n2; nnormalize;
707 ##[ ##3: #H; napply (λx:P.x)
708 ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
710 ##| ##4: ncases n2; nnormalize;
711 ##[ ##4: #H; napply (λx:P.x)
712 ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
714 ##| ##5: ncases n2; nnormalize;
715 ##[ ##5: #H; napply (λx:P.x)
716 ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
718 ##| ##6: ncases n2; nnormalize;
719 ##[ ##6: #H; napply (λx:P.x)
720 ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
722 ##| ##7: ncases n2; nnormalize;
723 ##[ ##7: #H; napply (λx:P.x)
724 ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
726 ##| ##8: ncases n2; nnormalize;
727 ##[ ##8: #H; napply (λx:P.x)
728 ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
730 ##| ##9: ncases n2; nnormalize;
731 ##[ ##9: #H; napply (λx:P.x)
732 ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
734 ##| ##10: ncases n2; nnormalize;
735 ##[ ##10: #H; napply (λx:P.x)
736 ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
738 ##| ##11: ncases n2; nnormalize;
739 ##[ ##11: #H; napply (λx:P.x)
740 ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
742 ##| ##12: ncases n2; nnormalize;
743 ##[ ##12: #H; napply (λx:P.x)
744 ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
746 ##| ##13: ncases n2; nnormalize;
747 ##[ ##13: #H; napply (λx:P.x)
748 ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
750 ##| ##14: ncases n2; nnormalize;
751 ##[ ##14: #H; napply (λx:P.x)
752 ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
754 ##| ##15: ncases n2; nnormalize;
755 ##[ ##15: #H; napply (λx:P.x)
756 ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
758 ##| ##16: ncases n2; nnormalize;
759 ##[ ##16: #H; napply (λx:P.x)
760 ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
762 ##| ##17: ncases n2; nnormalize;
763 ##[ ##17: #H; napply (λx:P.x)
764 ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
766 ##| ##18: ncases n2; nnormalize;
767 ##[ ##18: #H; napply (λx:P.x)
768 ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
770 ##| ##19: ncases n2; nnormalize;
771 ##[ ##19: #H; napply (λx:P.x)
772 ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
774 ##| ##20: ncases n2; nnormalize;
775 ##[ ##20: #H; napply (λx:P.x)
776 ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
778 ##| ##21: ncases n2; nnormalize;
779 ##[ ##21: #H; napply (λx:P.x)
780 ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
782 ##| ##22: ncases n2; nnormalize;
783 ##[ ##22: #H; napply (λx:P.x)
784 ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
786 ##| ##23: ncases n2; nnormalize;
787 ##[ ##23: #H; napply (λx:P.x)
788 ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
790 ##| ##24: ncases n2; nnormalize;
791 ##[ ##24: #H; napply (λx:P.x)
792 ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
794 ##| ##25: ncases n2; nnormalize;
795 ##[ ##25: #H; napply (λx:P.x)
796 ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
798 ##| ##26: ncases n2; nnormalize;
799 ##[ ##26: #H; napply (λx:P.x)
800 ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
802 ##| ##27: ncases n2; nnormalize;
803 ##[ ##27: #H; napply (λx:P.x)
804 ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
806 ##| ##28: ncases n2; nnormalize;
807 ##[ ##28: #H; napply (λx:P.x)
808 ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
810 ##| ##29: ncases n2; nnormalize;
811 ##[ ##29: #H; napply (λx:P.x)
812 ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
814 ##| ##30: ncases n2; nnormalize;
815 ##[ ##30: #H; napply (λx:P.x)
816 ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
818 ##| ##31: ncases n2; nnormalize;
819 ##[ ##31: #H; napply (λx:P.x)
820 ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
822 ##| ##32: ncases n2; nnormalize;
823 ##[ ##32: #H; napply (λx:P.x)
824 ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
830 ndefinition instr_mode_destruct_aux ≝
831 Πi1,i2.ΠP:Prop.i1 = i2 →
833 [ MODE_INH ⇒ match i2 with [ MODE_INH ⇒ P → P | _ ⇒ P ]
834 | MODE_INHA ⇒ match i2 with [ MODE_INHA ⇒ P → P | _ ⇒ P ]
835 | MODE_INHX ⇒ match i2 with [ MODE_INHX ⇒ P → P | _ ⇒ P ]
836 | MODE_INHH ⇒ match i2 with [ MODE_INHH ⇒ P → P | _ ⇒ P ]
837 | MODE_INHX0ADD ⇒ match i2 with [ MODE_INHX0ADD ⇒ P → P | _ ⇒ P ]
838 | MODE_INHX1ADD ⇒ match i2 with [ MODE_INHX1ADD ⇒ P → P | _ ⇒ P ]
839 | MODE_INHX2ADD ⇒ match i2 with [ MODE_INHX2ADD ⇒ P → P | _ ⇒ P ]
840 | MODE_IMM1 ⇒ match i2 with [ MODE_IMM1 ⇒ P → P | _ ⇒ P ]
841 | MODE_IMM1EXT ⇒ match i2 with [ MODE_IMM1EXT ⇒ P → P | _ ⇒ P ]
842 | MODE_IMM2 ⇒ match i2 with [ MODE_IMM2 ⇒ P → P | _ ⇒ P ]
843 | MODE_DIR1 ⇒ match i2 with [ MODE_DIR1 ⇒ P → P | _ ⇒ P ]
844 | MODE_DIR2 ⇒ match i2 with [ MODE_DIR2 ⇒ P → P | _ ⇒ P ]
845 | MODE_IX0 ⇒ match i2 with [ MODE_IX0 ⇒ P → P | _ ⇒ P ]
846 | MODE_IX1 ⇒ match i2 with [ MODE_IX1 ⇒ P → P | _ ⇒ P ]
847 | MODE_IX2 ⇒ match i2 with [ MODE_IX2 ⇒ P → P | _ ⇒ P ]
848 | MODE_SP1 ⇒ match i2 with [ MODE_SP1 ⇒ P → P | _ ⇒ P ]
849 | MODE_SP2 ⇒ match i2 with [ MODE_SP2 ⇒ P → P | _ ⇒ P ]
850 | MODE_DIR1_to_DIR1 ⇒ match i2 with [ MODE_DIR1_to_DIR1 ⇒ P → P | _ ⇒ P ]
851 | MODE_IMM1_to_DIR1 ⇒ match i2 with [ MODE_IMM1_to_DIR1 ⇒ P → P | _ ⇒ P ]
852 | MODE_IX0p_to_DIR1 ⇒ match i2 with [ MODE_IX0p_to_DIR1 ⇒ P → P | _ ⇒ P ]
853 | MODE_DIR1_to_IX0p ⇒ match i2 with [ MODE_DIR1_to_IX0p ⇒ P → P | _ ⇒ P ]
854 | MODE_INHA_and_IMM1 ⇒ match i2 with [ MODE_INHA_and_IMM1 ⇒ P → P | _ ⇒ P ]
855 | MODE_INHX_and_IMM1 ⇒ match i2 with [ MODE_INHX_and_IMM1 ⇒ P → P | _ ⇒ P ]
856 | MODE_IMM1_and_IMM1 ⇒ match i2 with [ MODE_IMM1_and_IMM1 ⇒ P → P | _ ⇒ P ]
857 | MODE_DIR1_and_IMM1 ⇒ match i2 with [ MODE_DIR1_and_IMM1 ⇒ P → P | _ ⇒ P ]
858 | MODE_IX0_and_IMM1 ⇒ match i2 with [ MODE_IX0_and_IMM1 ⇒ P → P | _ ⇒ P ]
859 | MODE_IX0p_and_IMM1 ⇒ match i2 with [ MODE_IX0p_and_IMM1 ⇒ P → P | _ ⇒ P ]
860 | MODE_IX1_and_IMM1 ⇒ match i2 with [ MODE_IX1_and_IMM1 ⇒ P → P | _ ⇒ P ]
861 | MODE_IX1p_and_IMM1 ⇒ match i2 with [ MODE_IX1p_and_IMM1 ⇒ P → P | _ ⇒ P ]
862 | MODE_SP1_and_IMM1 ⇒ match i2 with [ MODE_SP1_and_IMM1 ⇒ P → P | _ ⇒ P ]
863 | MODE_DIRn n1 ⇒ match i2 with
864 [ MODE_DIRn n2 ⇒ match n1 with
865 [ o0 ⇒ match n2 with [ o0 ⇒ P → P | _ ⇒ P ] | o1 ⇒ match n2 with [ o1 ⇒ P → P | _ ⇒ P ]
866 | o2 ⇒ match n2 with [ o2 ⇒ P → P | _ ⇒ P ] | o3 ⇒ match n2 with [ o3 ⇒ P → P | _ ⇒ P ]
867 | o4 ⇒ match n2 with [ o4 ⇒ P → P | _ ⇒ P ] | o5 ⇒ match n2 with [ o5 ⇒ P → P | _ ⇒ P ]
868 | o6 ⇒ match n2 with [ o6 ⇒ P → P | _ ⇒ P ] | o7 ⇒ match n2 with [ o7 ⇒ P → P | _ ⇒ P ]]
870 | MODE_DIRn_and_IMM1 n1 ⇒ match i2 with
871 [ MODE_DIRn_and_IMM1 n2 ⇒ match n1 with
872 [ o0 ⇒ match n2 with [ o0 ⇒ P → P | _ ⇒ P ] | o1 ⇒ match n2 with [ o1 ⇒ P → P | _ ⇒ P ]
873 | o2 ⇒ match n2 with [ o2 ⇒ P → P | _ ⇒ P ] | o3 ⇒ match n2 with [ o3 ⇒ P → P | _ ⇒ P ]
874 | o4 ⇒ match n2 with [ o4 ⇒ P → P | _ ⇒ P ] | o5 ⇒ match n2 with [ o5 ⇒ P → P | _ ⇒ P ]
875 | o6 ⇒ match n2 with [ o6 ⇒ P → P | _ ⇒ P ] | o7 ⇒ match n2 with [ o7 ⇒ P → P | _ ⇒ P ]]
877 | MODE_TNY e1 ⇒ match i2 with
878 [ MODE_TNY e2 ⇒ match e1 with
879 [ x0 ⇒ match e2 with [ x0 ⇒ P → P | _ ⇒ P ] | x1 ⇒ match e2 with [ x1 ⇒ P → P | _ ⇒ P ]
880 | x2 ⇒ match e2 with [ x2 ⇒ P → P | _ ⇒ P ] | x3 ⇒ match e2 with [ x3 ⇒ P → P | _ ⇒ P ]
881 | x4 ⇒ match e2 with [ x4 ⇒ P → P | _ ⇒ P ] | x5 ⇒ match e2 with [ x5 ⇒ P → P | _ ⇒ P ]
882 | x6 ⇒ match e2 with [ x6 ⇒ P → P | _ ⇒ P ] | x7 ⇒ match e2 with [ x7 ⇒ P → P | _ ⇒ P ]
883 | x8 ⇒ match e2 with [ x8 ⇒ P → P | _ ⇒ P ] | x9 ⇒ match e2 with [ x9 ⇒ P → P | _ ⇒ P ]
884 | xA ⇒ match e2 with [ xA ⇒ P → P | _ ⇒ P ] | xB ⇒ match e2 with [ xB ⇒ P → P | _ ⇒ P ]
885 | xC ⇒ match e2 with [ xC ⇒ P → P | _ ⇒ P ] | xD ⇒ match e2 with [ xD ⇒ P → P | _ ⇒ P ]
886 | xE ⇒ match e2 with [ xE ⇒ P → P | _ ⇒ P ] | xF ⇒ match e2 with [ xF ⇒ P → P | _ ⇒ P ]]
888 | MODE_SRT t1 ⇒ match i2 with
889 [ MODE_SRT t2 ⇒ match t1 with
890 [ t00 ⇒ match t2 with [ t00 ⇒ P → P | _ ⇒ P ] | t01 ⇒ match t2 with [ t01 ⇒ P → P | _ ⇒ P ]
891 | t02 ⇒ match t2 with [ t02 ⇒ P → P | _ ⇒ P ] | t03 ⇒ match t2 with [ t03 ⇒ P → P | _ ⇒ P ]
892 | t04 ⇒ match t2 with [ t04 ⇒ P → P | _ ⇒ P ] | t05 ⇒ match t2 with [ t05 ⇒ P → P | _ ⇒ P ]
893 | t06 ⇒ match t2 with [ t06 ⇒ P → P | _ ⇒ P ] | t07 ⇒ match t2 with [ t07 ⇒ P → P | _ ⇒ P ]
894 | t08 ⇒ match t2 with [ t08 ⇒ P → P | _ ⇒ P ] | t09 ⇒ match t2 with [ t09 ⇒ P → P | _ ⇒ P ]
895 | t0A ⇒ match t2 with [ t0A ⇒ P → P | _ ⇒ P ] | t0B ⇒ match t2 with [ t0B ⇒ P → P | _ ⇒ P ]
896 | t0C ⇒ match t2 with [ t0C ⇒ P → P | _ ⇒ P ] | t0D ⇒ match t2 with [ t0D ⇒ P → P | _ ⇒ P ]
897 | t0E ⇒ match t2 with [ t0E ⇒ P → P | _ ⇒ P ] | t0F ⇒ match t2 with [ t0F ⇒ P → P | _ ⇒ P ]
898 | t10 ⇒ match t2 with [ t10 ⇒ P → P | _ ⇒ P ] | t11 ⇒ match t2 with [ t11 ⇒ P → P | _ ⇒ P ]
899 | t12 ⇒ match t2 with [ t12 ⇒ P → P | _ ⇒ P ] | t13 ⇒ match t2 with [ t13 ⇒ P → P | _ ⇒ P ]
900 | t14 ⇒ match t2 with [ t14 ⇒ P → P | _ ⇒ P ] | t15 ⇒ match t2 with [ t15 ⇒ P → P | _ ⇒ P ]
901 | t16 ⇒ match t2 with [ t16 ⇒ P → P | _ ⇒ P ] | t17 ⇒ match t2 with [ t17 ⇒ P → P | _ ⇒ P ]
902 | t18 ⇒ match t2 with [ t18 ⇒ P → P | _ ⇒ P ] | t19 ⇒ match t2 with [ t19 ⇒ P → P | _ ⇒ P ]
903 | t1A ⇒ match t2 with [ t1A ⇒ P → P | _ ⇒ P ] | t1B ⇒ match t2 with [ t1B ⇒ P → P | _ ⇒ P ]
904 | t1C ⇒ match t2 with [ t1C ⇒ P → P | _ ⇒ P ] | t1D ⇒ match t2 with [ t1D ⇒ P → P | _ ⇒ P ]
905 | t1E ⇒ match t2 with [ t1E ⇒ P → P | _ ⇒ P ] | t1F ⇒ match t2 with [ t1F ⇒ P → P | _ ⇒ P ]]
909 ndefinition instr_mode_destruct : instr_mode_destruct_aux.
911 ##[ ##1: napply instr_mode_destruct1 ##| ##2: napply instr_mode_destruct2
912 ##| ##3: napply instr_mode_destruct3 ##| ##4: napply instr_mode_destruct4
913 ##| ##5: napply instr_mode_destruct5 ##| ##6: napply instr_mode_destruct6
914 ##| ##7: napply instr_mode_destruct7 ##| ##8: napply instr_mode_destruct8
915 ##| ##9: napply instr_mode_destruct9 ##| ##10: napply instr_mode_destruct10
916 ##| ##11: napply instr_mode_destruct11 ##| ##12: napply instr_mode_destruct12
917 ##| ##13: napply instr_mode_destruct13 ##| ##14: napply instr_mode_destruct14
918 ##| ##15: napply instr_mode_destruct15 ##| ##16: napply instr_mode_destruct16
919 ##| ##17: napply instr_mode_destruct17 ##| ##18: napply instr_mode_destruct18
920 ##| ##19: napply instr_mode_destruct19 ##| ##20: napply instr_mode_destruct20
921 ##| ##21: napply instr_mode_destruct21 ##| ##22: napply instr_mode_destruct22
922 ##| ##23: napply instr_mode_destruct23 ##| ##24: napply instr_mode_destruct24
923 ##| ##25: napply instr_mode_destruct25 ##| ##26: napply instr_mode_destruct26
924 ##| ##27: napply instr_mode_destruct27 ##| ##28: napply instr_mode_destruct28
925 ##| ##29: napply instr_mode_destruct29 ##| ##30: napply instr_mode_destruct30
926 ##| ##31: napply instr_mode_destruct31 ##| ##32: napply instr_mode_destruct32
927 ##| ##33: napply instr_mode_destruct33 ##| ##34: napply instr_mode_destruct34