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 "num/bool_lemmas.ma".
24 include "freescale/opcode_base.ma".
26 (* ********************************************** *)
27 (* MATTONI BASE PER DEFINIRE LE TABELLE DELLE MCU *)
28 (* ********************************************** *)
30 ndefinition opcode_destruct1 : Πop2.ΠP:Prop.ADC = op2 → match op2 with [ ADC ⇒ P → P | _ ⇒ P ].
31 #op2; #P; ncases op2; nnormalize;
32 ##[ ##1: #H; napply (λx:P.x)
33 ##| ##*: #H; napply False_ind;
34 nchange with (match ADC with [ ADC ⇒ False | _ ⇒ True ]);
35 nrewrite > H; nnormalize; napply I
39 ndefinition opcode_destruct2 : Πop2.ΠP:Prop.ADD = op2 → match op2 with [ ADD ⇒ P → P | _ ⇒ P ].
40 #op2; #P; ncases op2; nnormalize;
41 ##[ ##2: #H; napply (λx:P.x)
42 ##| ##*: #H; napply False_ind;
43 nchange with (match ADD with [ ADD ⇒ False | _ ⇒ True ]);
44 nrewrite > H; nnormalize; napply I
48 ndefinition opcode_destruct3 : Πop2.ΠP:Prop.AIS = op2 → match op2 with [ AIS ⇒ P → P | _ ⇒ P ].
49 #op2; #P; ncases op2; nnormalize;
50 ##[ ##3: #H; napply (λx:P.x)
51 ##| ##*: #H; napply False_ind;
52 nchange with (match AIS with [ AIS ⇒ False | _ ⇒ True ]);
53 nrewrite > H; nnormalize; napply I
57 ndefinition opcode_destruct4 : Πop2.ΠP:Prop.AIX = op2 → match op2 with [ AIX ⇒ P → P | _ ⇒ P ].
58 #op2; #P; ncases op2; nnormalize;
59 ##[ ##4: #H; napply (λx:P.x)
60 ##| ##*: #H; napply False_ind;
61 nchange with (match AIX with [ AIX ⇒ False | _ ⇒ True ]);
62 nrewrite > H; nnormalize; napply I
66 ndefinition opcode_destruct5 : Πop2.ΠP:Prop.AND = op2 → match op2 with [ AND ⇒ P → P | _ ⇒ P ].
67 #op2; #P; ncases op2; nnormalize;
68 ##[ ##5: #H; napply (λx:P.x)
69 ##| ##*: #H; napply False_ind;
70 nchange with (match AND with [ AND ⇒ False | _ ⇒ True ]);
71 nrewrite > H; nnormalize; napply I
75 ndefinition opcode_destruct6 : Πop2.ΠP:Prop.ASL = op2 → match op2 with [ ASL ⇒ P → P | _ ⇒ P ].
76 #op2; #P; ncases op2; nnormalize;
77 ##[ ##6: #H; napply (λx:P.x)
78 ##| ##*: #H; napply False_ind;
79 nchange with (match ASL with [ ASL ⇒ False | _ ⇒ True ]);
80 nrewrite > H; nnormalize; napply I
84 ndefinition opcode_destruct7 : Πop2.ΠP:Prop.ASR = op2 → match op2 with [ ASR ⇒ P → P | _ ⇒ P ].
85 #op2; #P; ncases op2; nnormalize;
86 ##[ ##7: #H; napply (λx:P.x)
87 ##| ##*: #H; napply False_ind;
88 nchange with (match ASR with [ ASR ⇒ False | _ ⇒ True ]);
89 nrewrite > H; nnormalize; napply I
93 ndefinition opcode_destruct8 : Πop2.ΠP:Prop.BCC = op2 → match op2 with [ BCC ⇒ P → P | _ ⇒ P ].
94 #op2; #P; ncases op2; nnormalize;
95 ##[ ##8: #H; napply (λx:P.x)
96 ##| ##*: #H; napply False_ind;
97 nchange with (match BCC with [ BCC ⇒ False | _ ⇒ True ]);
98 nrewrite > H; nnormalize; napply I
102 ndefinition opcode_destruct9 : Πop2.ΠP:Prop.BCLRn = op2 → match op2 with [ BCLRn ⇒ P → P | _ ⇒ P ].
103 #op2; #P; ncases op2; nnormalize;
104 ##[ ##9: #H; napply (λx:P.x)
105 ##| ##*: #H; napply False_ind;
106 nchange with (match BCLRn with [ BCLRn ⇒ False | _ ⇒ True ]);
107 nrewrite > H; nnormalize; napply I
111 ndefinition opcode_destruct10 : Πop2.ΠP:Prop.BCS = op2 → match op2 with [ BCS ⇒ P → P | _ ⇒ P ].
112 #op2; #P; ncases op2; nnormalize;
113 ##[ ##10: #H; napply (λx:P.x)
114 ##| ##*: #H; napply False_ind;
115 nchange with (match BCS with [ BCS ⇒ False | _ ⇒ True ]);
116 nrewrite > H; nnormalize; napply I
120 ndefinition opcode_destruct11 : Πop2.ΠP:Prop.BEQ = op2 → match op2 with [ BEQ ⇒ P → P | _ ⇒ P ].
121 #op2; #P; ncases op2; nnormalize;
122 ##[ ##11: #H; napply (λx:P.x)
123 ##| ##*: #H; napply False_ind;
124 nchange with (match BEQ with [ BEQ ⇒ False | _ ⇒ True ]);
125 nrewrite > H; nnormalize; napply I
129 ndefinition opcode_destruct12 : Πop2.ΠP:Prop.BGE = op2 → match op2 with [ BGE ⇒ P → P | _ ⇒ P ].
130 #op2; #P; ncases op2; nnormalize;
131 ##[ ##12: #H; napply (λx:P.x)
132 ##| ##*: #H; napply False_ind;
133 nchange with (match BGE with [ BGE ⇒ False | _ ⇒ True ]);
134 nrewrite > H; nnormalize; napply I
138 ndefinition opcode_destruct13 : Πop2.ΠP:Prop.BGND = op2 → match op2 with [ BGND ⇒ P → P | _ ⇒ P ].
139 #op2; #P; ncases op2; nnormalize;
140 ##[ ##13: #H; napply (λx:P.x)
141 ##| ##*: #H; napply False_ind;
142 nchange with (match BGND with [ BGND ⇒ False | _ ⇒ True ]);
143 nrewrite > H; nnormalize; napply I
147 ndefinition opcode_destruct14 : Πop2.ΠP:Prop.BGT = op2 → match op2 with [ BGT ⇒ P → P | _ ⇒ P ].
148 #op2; #P; ncases op2; nnormalize;
149 ##[ ##14: #H; napply (λx:P.x)
150 ##| ##*: #H; napply False_ind;
151 nchange with (match BGT with [ BGT ⇒ False | _ ⇒ True ]);
152 nrewrite > H; nnormalize; napply I
156 ndefinition opcode_destruct15 : Πop2.ΠP:Prop.BHCC = op2 → match op2 with [ BHCC ⇒ P → P | _ ⇒ P ].
157 #op2; #P; ncases op2; nnormalize;
158 ##[ ##15: #H; napply (λx:P.x)
159 ##| ##*: #H; napply False_ind;
160 nchange with (match BHCC with [ BHCC ⇒ False | _ ⇒ True ]);
161 nrewrite > H; nnormalize; napply I
165 ndefinition opcode_destruct16 : Πop2.ΠP:Prop.BHCS = op2 → match op2 with [ BHCS ⇒ P → P | _ ⇒ P ].
166 #op2; #P; ncases op2; nnormalize;
167 ##[ ##16: #H; napply (λx:P.x)
168 ##| ##*: #H; napply False_ind;
169 nchange with (match BHCS with [ BHCS ⇒ False | _ ⇒ True ]);
170 nrewrite > H; nnormalize; napply I
174 ndefinition opcode_destruct17 : Πop2.ΠP:Prop.BHI = op2 → match op2 with [ BHI ⇒ P → P | _ ⇒ P ].
175 #op2; #P; ncases op2; nnormalize;
176 ##[ ##17: #H; napply (λx:P.x)
177 ##| ##*: #H; napply False_ind;
178 nchange with (match BHI with [ BHI ⇒ False | _ ⇒ True ]);
179 nrewrite > H; nnormalize; napply I
183 ndefinition opcode_destruct18 : Πop2.ΠP:Prop.BIH = op2 → match op2 with [ BIH ⇒ P → P | _ ⇒ P ].
184 #op2; #P; ncases op2; nnormalize;
185 ##[ ##18: #H; napply (λx:P.x)
186 ##| ##*: #H; napply False_ind;
187 nchange with (match BIH with [ BIH ⇒ False | _ ⇒ True ]);
188 nrewrite > H; nnormalize; napply I
192 ndefinition opcode_destruct19 : Πop2.ΠP:Prop.BIL = op2 → match op2 with [ BIL ⇒ P → P | _ ⇒ P ].
193 #op2; #P; ncases op2; nnormalize;
194 ##[ ##19: #H; napply (λx:P.x)
195 ##| ##*: #H; napply False_ind;
196 nchange with (match BIL with [ BIL ⇒ False | _ ⇒ True ]);
197 nrewrite > H; nnormalize; napply I
201 ndefinition opcode_destruct20 : Πop2.ΠP:Prop.BIT = op2 → match op2 with [ BIT ⇒ P → P | _ ⇒ P ].
202 #op2; #P; ncases op2; nnormalize;
203 ##[ ##20: #H; napply (λx:P.x)
204 ##| ##*: #H; napply False_ind;
205 nchange with (match BIT with [ BIT ⇒ False | _ ⇒ True ]);
206 nrewrite > H; nnormalize; napply I
210 ndefinition opcode_destruct21 : Πop2.ΠP:Prop.BLE = op2 → match op2 with [ BLE ⇒ P → P | _ ⇒ P ].
211 #op2; #P; ncases op2; nnormalize;
212 ##[ ##21: #H; napply (λx:P.x)
213 ##| ##*: #H; napply False_ind;
214 nchange with (match BLE with [ BLE ⇒ False | _ ⇒ True ]);
215 nrewrite > H; nnormalize; napply I
219 ndefinition opcode_destruct22 : Πop2.ΠP:Prop.BLS = op2 → match op2 with [ BLS ⇒ P → P | _ ⇒ P ].
220 #op2; #P; ncases op2; nnormalize;
221 ##[ ##22: #H; napply (λx:P.x)
222 ##| ##*: #H; napply False_ind;
223 nchange with (match BLS with [ BLS ⇒ False | _ ⇒ True ]);
224 nrewrite > H; nnormalize; napply I
228 ndefinition opcode_destruct23 : Πop2.ΠP:Prop.BLT = op2 → match op2 with [ BLT ⇒ P → P | _ ⇒ P ].
229 #op2; #P; ncases op2; nnormalize;
230 ##[ ##23: #H; napply (λx:P.x)
231 ##| ##*: #H; napply False_ind;
232 nchange with (match BLT with [ BLT ⇒ False | _ ⇒ True ]);
233 nrewrite > H; nnormalize; napply I
237 ndefinition opcode_destruct24 : Πop2.ΠP:Prop.BMC = op2 → match op2 with [ BMC ⇒ P → P | _ ⇒ P ].
238 #op2; #P; ncases op2; nnormalize;
239 ##[ ##24: #H; napply (λx:P.x)
240 ##| ##*: #H; napply False_ind;
241 nchange with (match BMC with [ BMC ⇒ False | _ ⇒ True ]);
242 nrewrite > H; nnormalize; napply I
246 ndefinition opcode_destruct25 : Πop2.ΠP:Prop.BMI = op2 → match op2 with [ BMI ⇒ P → P | _ ⇒ P ].
247 #op2; #P; ncases op2; nnormalize;
248 ##[ ##25: #H; napply (λx:P.x)
249 ##| ##*: #H; napply False_ind;
250 nchange with (match BMI with [ BMI ⇒ False | _ ⇒ True ]);
251 nrewrite > H; nnormalize; napply I
255 ndefinition opcode_destruct26 : Πop2.ΠP:Prop.BMS = op2 → match op2 with [ BMS ⇒ P → P | _ ⇒ P ].
256 #op2; #P; ncases op2; nnormalize;
257 ##[ ##26: #H; napply (λx:P.x)
258 ##| ##*: #H; napply False_ind;
259 nchange with (match BMS with [ BMS ⇒ False | _ ⇒ True ]);
260 nrewrite > H; nnormalize; napply I
264 ndefinition opcode_destruct27 : Πop2.ΠP:Prop.BNE = op2 → match op2 with [ BNE ⇒ P → P | _ ⇒ P ].
265 #op2; #P; ncases op2; nnormalize;
266 ##[ ##27: #H; napply (λx:P.x)
267 ##| ##*: #H; napply False_ind;
268 nchange with (match BNE with [ BNE ⇒ False | _ ⇒ True ]);
269 nrewrite > H; nnormalize; napply I
273 ndefinition opcode_destruct28 : Πop2.ΠP:Prop.BPL = op2 → match op2 with [ BPL ⇒ P → P | _ ⇒ P ].
274 #op2; #P; ncases op2; nnormalize;
275 ##[ ##28: #H; napply (λx:P.x)
276 ##| ##*: #H; napply False_ind;
277 nchange with (match BPL with [ BPL ⇒ False | _ ⇒ True ]);
278 nrewrite > H; nnormalize; napply I
282 ndefinition opcode_destruct29 : Πop2.ΠP:Prop.BRA = op2 → match op2 with [ BRA ⇒ P → P | _ ⇒ P ].
283 #op2; #P; ncases op2; nnormalize;
284 ##[ ##29: #H; napply (λx:P.x)
285 ##| ##*: #H; napply False_ind;
286 nchange with (match BRA with [ BRA ⇒ False | _ ⇒ True ]);
287 nrewrite > H; nnormalize; napply I
291 ndefinition opcode_destruct30 : Πop2.ΠP:Prop.BRCLRn = op2 → match op2 with [ BRCLRn ⇒ P → P | _ ⇒ P ].
292 #op2; #P; ncases op2; nnormalize;
293 ##[ ##30: #H; napply (λx:P.x)
294 ##| ##*: #H; napply False_ind;
295 nchange with (match BRCLRn with [ BRCLRn ⇒ False | _ ⇒ True ]);
296 nrewrite > H; nnormalize; napply I
300 ndefinition opcode_destruct31 : Πop2.ΠP:Prop.BRN = op2 → match op2 with [ BRN ⇒ P → P | _ ⇒ P ].
301 #op2; #P; ncases op2; nnormalize;
302 ##[ ##31: #H; napply (λx:P.x)
303 ##| ##*: #H; napply False_ind;
304 nchange with (match BRN with [ BRN ⇒ False | _ ⇒ True ]);
305 nrewrite > H; nnormalize; napply I
309 ndefinition opcode_destruct32 : Πop2.ΠP:Prop.BRSETn = op2 → match op2 with [ BRSETn ⇒ P → P | _ ⇒ P ].
310 #op2; #P; ncases op2; nnormalize;
311 ##[ ##32: #H; napply (λx:P.x)
312 ##| ##*: #H; napply False_ind;
313 nchange with (match BRSETn with [ BRSETn ⇒ False | _ ⇒ True ]);
314 nrewrite > H; nnormalize; napply I
318 ndefinition opcode_destruct33 : Πop2.ΠP:Prop.BSETn = op2 → match op2 with [ BSETn ⇒ P → P | _ ⇒ P ].
319 #op2; #P; ncases op2; nnormalize;
320 ##[ ##33: #H; napply (λx:P.x)
321 ##| ##*: #H; napply False_ind;
322 nchange with (match BSETn with [ BSETn ⇒ False | _ ⇒ True ]);
323 nrewrite > H; nnormalize; napply I
327 ndefinition opcode_destruct34 : Πop2.ΠP:Prop.BSR = op2 → match op2 with [ BSR ⇒ P → P | _ ⇒ P ].
328 #op2; #P; ncases op2; nnormalize;
329 ##[ ##34: #H; napply (λx:P.x)
330 ##| ##*: #H; napply False_ind;
331 nchange with (match BSR with [ BSR ⇒ False | _ ⇒ True ]);
332 nrewrite > H; nnormalize; napply I
336 ndefinition opcode_destruct35 : Πop2.ΠP:Prop.CBEQA = op2 → match op2 with [ CBEQA ⇒ P → P | _ ⇒ P ].
337 #op2; #P; ncases op2; nnormalize;
338 ##[ ##35: #H; napply (λx:P.x)
339 ##| ##*: #H; napply False_ind;
340 nchange with (match CBEQA with [ CBEQA ⇒ False | _ ⇒ True ]);
341 nrewrite > H; nnormalize; napply I
345 ndefinition opcode_destruct36 : Πop2.ΠP:Prop.CBEQX = op2 → match op2 with [ CBEQX ⇒ P → P | _ ⇒ P ].
346 #op2; #P; ncases op2; nnormalize;
347 ##[ ##36: #H; napply (λx:P.x)
348 ##| ##*: #H; napply False_ind;
349 nchange with (match CBEQX with [ CBEQX ⇒ False | _ ⇒ True ]);
350 nrewrite > H; nnormalize; napply I
354 ndefinition opcode_destruct37 : Πop2.ΠP:Prop.CLC = op2 → match op2 with [ CLC ⇒ P → P | _ ⇒ P ].
355 #op2; #P; ncases op2; nnormalize;
356 ##[ ##37: #H; napply (λx:P.x)
357 ##| ##*: #H; napply False_ind;
358 nchange with (match CLC with [ CLC ⇒ False | _ ⇒ True ]);
359 nrewrite > H; nnormalize; napply I
363 ndefinition opcode_destruct38 : Πop2.ΠP:Prop.CLI = op2 → match op2 with [ CLI ⇒ P → P | _ ⇒ P ].
364 #op2; #P; ncases op2; nnormalize;
365 ##[ ##38: #H; napply (λx:P.x)
366 ##| ##*: #H; napply False_ind;
367 nchange with (match CLI with [ CLI ⇒ False | _ ⇒ True ]);
368 nrewrite > H; nnormalize; napply I
372 ndefinition opcode_destruct39 : Πop2.ΠP:Prop.CLR = op2 → match op2 with [ CLR ⇒ P → P | _ ⇒ P ].
373 #op2; #P; ncases op2; nnormalize;
374 ##[ ##39: #H; napply (λx:P.x)
375 ##| ##*: #H; napply False_ind;
376 nchange with (match CLR with [ CLR ⇒ False | _ ⇒ True ]);
377 nrewrite > H; nnormalize; napply I
381 ndefinition opcode_destruct40 : Πop2.ΠP:Prop.CMP = op2 → match op2 with [ CMP ⇒ P → P | _ ⇒ P ].
382 #op2; #P; ncases op2; nnormalize;
383 ##[ ##40: #H; napply (λx:P.x)
384 ##| ##*: #H; napply False_ind;
385 nchange with (match CMP with [ CMP ⇒ False | _ ⇒ True ]);
386 nrewrite > H; nnormalize; napply I
390 ndefinition opcode_destruct41 : Πop2.ΠP:Prop.COM = op2 → match op2 with [ COM ⇒ P → P | _ ⇒ P ].
391 #op2; #P; ncases op2; nnormalize;
392 ##[ ##41: #H; napply (λx:P.x)
393 ##| ##*: #H; napply False_ind;
394 nchange with (match COM with [ COM ⇒ False | _ ⇒ True ]);
395 nrewrite > H; nnormalize; napply I
399 ndefinition opcode_destruct42 : Πop2.ΠP:Prop.CPHX = op2 → match op2 with [ CPHX ⇒ P → P | _ ⇒ P ].
400 #op2; #P; ncases op2; nnormalize;
401 ##[ ##42: #H; napply (λx:P.x)
402 ##| ##*: #H; napply False_ind;
403 nchange with (match CPHX with [ CPHX ⇒ False | _ ⇒ True ]);
404 nrewrite > H; nnormalize; napply I
408 ndefinition opcode_destruct43 : Πop2.ΠP:Prop.CPX = op2 → match op2 with [ CPX ⇒ P → P | _ ⇒ P ].
409 #op2; #P; ncases op2; nnormalize;
410 ##[ ##43: #H; napply (λx:P.x)
411 ##| ##*: #H; napply False_ind;
412 nchange with (match CPX with [ CPX ⇒ False | _ ⇒ True ]);
413 nrewrite > H; nnormalize; napply I
417 ndefinition opcode_destruct44 : Πop2.ΠP:Prop.DAA = op2 → match op2 with [ DAA ⇒ P → P | _ ⇒ P ].
418 #op2; #P; ncases op2; nnormalize;
419 ##[ ##44: #H; napply (λx:P.x)
420 ##| ##*: #H; napply False_ind;
421 nchange with (match DAA with [ DAA ⇒ False | _ ⇒ True ]);
422 nrewrite > H; nnormalize; napply I
426 ndefinition opcode_destruct45 : Πop2.ΠP:Prop.DBNZ = op2 → match op2 with [ DBNZ ⇒ P → P | _ ⇒ P ].
427 #op2; #P; ncases op2; nnormalize;
428 ##[ ##45: #H; napply (λx:P.x)
429 ##| ##*: #H; napply False_ind;
430 nchange with (match DBNZ with [ DBNZ ⇒ False | _ ⇒ True ]);
431 nrewrite > H; nnormalize; napply I
435 ndefinition opcode_destruct46 : Πop2.ΠP:Prop.DEC = op2 → match op2 with [ DEC ⇒ P → P | _ ⇒ P ].
436 #op2; #P; ncases op2; nnormalize;
437 ##[ ##46: #H; napply (λx:P.x)
438 ##| ##*: #H; napply False_ind;
439 nchange with (match DEC with [ DEC ⇒ False | _ ⇒ True ]);
440 nrewrite > H; nnormalize; napply I
444 ndefinition opcode_destruct47 : Πop2.ΠP:Prop.DIV = op2 → match op2 with [ DIV ⇒ P → P | _ ⇒ P ].
445 #op2; #P; ncases op2; nnormalize;
446 ##[ ##47: #H; napply (λx:P.x)
447 ##| ##*: #H; napply False_ind;
448 nchange with (match DIV with [ DIV ⇒ False | _ ⇒ True ]);
449 nrewrite > H; nnormalize; napply I
453 ndefinition opcode_destruct48 : Πop2.ΠP:Prop.EOR = op2 → match op2 with [ EOR ⇒ P → P | _ ⇒ P ].
454 #op2; #P; ncases op2; nnormalize;
455 ##[ ##48: #H; napply (λx:P.x)
456 ##| ##*: #H; napply False_ind;
457 nchange with (match EOR with [ EOR ⇒ False | _ ⇒ True ]);
458 nrewrite > H; nnormalize; napply I
462 ndefinition opcode_destruct49 : Πop2.ΠP:Prop.INC = op2 → match op2 with [ INC ⇒ P → P | _ ⇒ P ].
463 #op2; #P; ncases op2; nnormalize;
464 ##[ ##49: #H; napply (λx:P.x)
465 ##| ##*: #H; napply False_ind;
466 nchange with (match INC with [ INC ⇒ False | _ ⇒ True ]);
467 nrewrite > H; nnormalize; napply I
471 ndefinition opcode_destruct50 : Πop2.ΠP:Prop.JMP = op2 → match op2 with [ JMP ⇒ P → P | _ ⇒ P ].
472 #op2; #P; ncases op2; nnormalize;
473 ##[ ##50: #H; napply (λx:P.x)
474 ##| ##*: #H; napply False_ind;
475 nchange with (match JMP with [ JMP ⇒ False | _ ⇒ True ]);
476 nrewrite > H; nnormalize; napply I
480 ndefinition opcode_destruct51 : Πop2.ΠP:Prop.JSR = op2 → match op2 with [ JSR ⇒ P → P | _ ⇒ P ].
481 #op2; #P; ncases op2; nnormalize;
482 ##[ ##51: #H; napply (λx:P.x)
483 ##| ##*: #H; napply False_ind;
484 nchange with (match JSR with [ JSR ⇒ False | _ ⇒ True ]);
485 nrewrite > H; nnormalize; napply I
489 ndefinition opcode_destruct52 : Πop2.ΠP:Prop.LDA = op2 → match op2 with [ LDA ⇒ P → P | _ ⇒ P ].
490 #op2; #P; ncases op2; nnormalize;
491 ##[ ##52: #H; napply (λx:P.x)
492 ##| ##*: #H; napply False_ind;
493 nchange with (match LDA with [ LDA ⇒ False | _ ⇒ True ]);
494 nrewrite > H; nnormalize; napply I
498 ndefinition opcode_destruct53 : Πop2.ΠP:Prop.LDHX = op2 → match op2 with [ LDHX ⇒ P → P | _ ⇒ P ].
499 #op2; #P; ncases op2; nnormalize;
500 ##[ ##53: #H; napply (λx:P.x)
501 ##| ##*: #H; napply False_ind;
502 nchange with (match LDHX with [ LDHX ⇒ False | _ ⇒ True ]);
503 nrewrite > H; nnormalize; napply I
507 ndefinition opcode_destruct54 : Πop2.ΠP:Prop.LDX = op2 → match op2 with [ LDX ⇒ P → P | _ ⇒ P ].
508 #op2; #P; ncases op2; nnormalize;
509 ##[ ##54: #H; napply (λx:P.x)
510 ##| ##*: #H; napply False_ind;
511 nchange with (match LDX with [ LDX ⇒ False | _ ⇒ True ]);
512 nrewrite > H; nnormalize; napply I
516 ndefinition opcode_destruct55 : Πop2.ΠP:Prop.LSR = op2 → match op2 with [ LSR ⇒ P → P | _ ⇒ P ].
517 #op2; #P; ncases op2; nnormalize;
518 ##[ ##55: #H; napply (λx:P.x)
519 ##| ##*: #H; napply False_ind;
520 nchange with (match LSR with [ LSR ⇒ False | _ ⇒ True ]);
521 nrewrite > H; nnormalize; napply I
525 ndefinition opcode_destruct56 : Πop2.ΠP:Prop.MOV = op2 → match op2 with [ MOV ⇒ P → P | _ ⇒ P ].
526 #op2; #P; ncases op2; nnormalize;
527 ##[ ##56: #H; napply (λx:P.x)
528 ##| ##*: #H; napply False_ind;
529 nchange with (match MOV with [ MOV ⇒ False | _ ⇒ True ]);
530 nrewrite > H; nnormalize; napply I
534 ndefinition opcode_destruct57 : Πop2.ΠP:Prop.MUL = op2 → match op2 with [ MUL ⇒ P → P | _ ⇒ P ].
535 #op2; #P; ncases op2; nnormalize;
536 ##[ ##57: #H; napply (λx:P.x)
537 ##| ##*: #H; napply False_ind;
538 nchange with (match MUL with [ MUL ⇒ False | _ ⇒ True ]);
539 nrewrite > H; nnormalize; napply I
543 ndefinition opcode_destruct58 : Πop2.ΠP:Prop.NEG = op2 → match op2 with [ NEG ⇒ P → P | _ ⇒ P ].
544 #op2; #P; ncases op2; nnormalize;
545 ##[ ##58: #H; napply (λx:P.x)
546 ##| ##*: #H; napply False_ind;
547 nchange with (match NEG with [ NEG ⇒ False | _ ⇒ True ]);
548 nrewrite > H; nnormalize; napply I
552 ndefinition opcode_destruct59 : Πop2.ΠP:Prop.NOP = op2 → match op2 with [ NOP ⇒ P → P | _ ⇒ P ].
553 #op2; #P; ncases op2; nnormalize;
554 ##[ ##59: #H; napply (λx:P.x)
555 ##| ##*: #H; napply False_ind;
556 nchange with (match NOP with [ NOP ⇒ False | _ ⇒ True ]);
557 nrewrite > H; nnormalize; napply I
561 ndefinition opcode_destruct60 : Πop2.ΠP:Prop.NSA = op2 → match op2 with [ NSA ⇒ P → P | _ ⇒ P ].
562 #op2; #P; ncases op2; nnormalize;
563 ##[ ##60: #H; napply (λx:P.x)
564 ##| ##*: #H; napply False_ind;
565 nchange with (match NSA with [ NSA ⇒ False | _ ⇒ True ]);
566 nrewrite > H; nnormalize; napply I
570 ndefinition opcode_destruct61 : Πop2.ΠP:Prop.ORA = op2 → match op2 with [ ORA ⇒ P → P | _ ⇒ P ].
571 #op2; #P; ncases op2; nnormalize;
572 ##[ ##61: #H; napply (λx:P.x)
573 ##| ##*: #H; napply False_ind;
574 nchange with (match ORA with [ ORA ⇒ False | _ ⇒ True ]);
575 nrewrite > H; nnormalize; napply I
579 ndefinition opcode_destruct62 : Πop2.ΠP:Prop.PSHA = op2 → match op2 with [ PSHA ⇒ P → P | _ ⇒ P ].
580 #op2; #P; ncases op2; nnormalize;
581 ##[ ##62: #H; napply (λx:P.x)
582 ##| ##*: #H; napply False_ind;
583 nchange with (match PSHA with [ PSHA ⇒ False | _ ⇒ True ]);
584 nrewrite > H; nnormalize; napply I
588 ndefinition opcode_destruct63 : Πop2.ΠP:Prop.PSHH = op2 → match op2 with [ PSHH ⇒ P → P | _ ⇒ P ].
589 #op2; #P; ncases op2; nnormalize;
590 ##[ ##63: #H; napply (λx:P.x)
591 ##| ##*: #H; napply False_ind;
592 nchange with (match PSHH with [ PSHH ⇒ False | _ ⇒ True ]);
593 nrewrite > H; nnormalize; napply I
597 ndefinition opcode_destruct64 : Πop2.ΠP:Prop.PSHX = op2 → match op2 with [ PSHX ⇒ P → P | _ ⇒ P ].
598 #op2; #P; ncases op2; nnormalize;
599 ##[ ##64: #H; napply (λx:P.x)
600 ##| ##*: #H; napply False_ind;
601 nchange with (match PSHX with [ PSHX ⇒ False | _ ⇒ True ]);
602 nrewrite > H; nnormalize; napply I
606 ndefinition opcode_destruct65 : Πop2.ΠP:Prop.PULA = op2 → match op2 with [ PULA ⇒ P → P | _ ⇒ P ].
607 #op2; #P; ncases op2; nnormalize;
608 ##[ ##65: #H; napply (λx:P.x)
609 ##| ##*: #H; napply False_ind;
610 nchange with (match PULA with [ PULA ⇒ False | _ ⇒ True ]);
611 nrewrite > H; nnormalize; napply I
615 ndefinition opcode_destruct66 : Πop2.ΠP:Prop.PULH = op2 → match op2 with [ PULH ⇒ P → P | _ ⇒ P ].
616 #op2; #P; ncases op2; nnormalize;
617 ##[ ##66: #H; napply (λx:P.x)
618 ##| ##*: #H; napply False_ind;
619 nchange with (match PULH with [ PULH ⇒ False | _ ⇒ True ]);
620 nrewrite > H; nnormalize; napply I
624 ndefinition opcode_destruct67 : Πop2.ΠP:Prop.PULX = op2 → match op2 with [ PULX ⇒ P → P | _ ⇒ P ].
625 #op2; #P; ncases op2; nnormalize;
626 ##[ ##67: #H; napply (λx:P.x)
627 ##| ##*: #H; napply False_ind;
628 nchange with (match PULX with [ PULX ⇒ False | _ ⇒ True ]);
629 nrewrite > H; nnormalize; napply I
633 ndefinition opcode_destruct68 : Πop2.ΠP:Prop.ROL = op2 → match op2 with [ ROL ⇒ P → P | _ ⇒ P ].
634 #op2; #P; ncases op2; nnormalize;
635 ##[ ##68: #H; napply (λx:P.x)
636 ##| ##*: #H; napply False_ind;
637 nchange with (match ROL with [ ROL ⇒ False | _ ⇒ True ]);
638 nrewrite > H; nnormalize; napply I
642 ndefinition opcode_destruct69 : Πop2.ΠP:Prop.ROR = op2 → match op2 with [ ROR ⇒ P → P | _ ⇒ P ].
643 #op2; #P; ncases op2; nnormalize;
644 ##[ ##69: #H; napply (λx:P.x)
645 ##| ##*: #H; napply False_ind;
646 nchange with (match ROR with [ ROR ⇒ False | _ ⇒ True ]);
647 nrewrite > H; nnormalize; napply I
651 ndefinition opcode_destruct70 : Πop2.ΠP:Prop.RSP = op2 → match op2 with [ RSP ⇒ P → P | _ ⇒ P ].
652 #op2; #P; ncases op2; nnormalize;
653 ##[ ##70: #H; napply (λx:P.x)
654 ##| ##*: #H; napply False_ind;
655 nchange with (match RSP with [ RSP ⇒ False | _ ⇒ True ]);
656 nrewrite > H; nnormalize; napply I
660 ndefinition opcode_destruct71 : Πop2.ΠP:Prop.RTI = op2 → match op2 with [ RTI ⇒ P → P | _ ⇒ P ].
661 #op2; #P; ncases op2; nnormalize;
662 ##[ ##71: #H; napply (λx:P.x)
663 ##| ##*: #H; napply False_ind;
664 nchange with (match RTI with [ RTI ⇒ False | _ ⇒ True ]);
665 nrewrite > H; nnormalize; napply I
669 ndefinition opcode_destruct72 : Πop2.ΠP:Prop.RTS = op2 → match op2 with [ RTS ⇒ P → P | _ ⇒ P ].
670 #op2; #P; ncases op2; nnormalize;
671 ##[ ##72: #H; napply (λx:P.x)
672 ##| ##*: #H; napply False_ind;
673 nchange with (match RTS with [ RTS ⇒ False | _ ⇒ True ]);
674 nrewrite > H; nnormalize; napply I
678 ndefinition opcode_destruct73 : Πop2.ΠP:Prop.SBC = op2 → match op2 with [ SBC ⇒ P → P | _ ⇒ P ].
679 #op2; #P; ncases op2; nnormalize;
680 ##[ ##73: #H; napply (λx:P.x)
681 ##| ##*: #H; napply False_ind;
682 nchange with (match SBC with [ SBC ⇒ False | _ ⇒ True ]);
683 nrewrite > H; nnormalize; napply I
687 ndefinition opcode_destruct74 : Πop2.ΠP:Prop.SEC = op2 → match op2 with [ SEC ⇒ P → P | _ ⇒ P ].
688 #op2; #P; ncases op2; nnormalize;
689 ##[ ##74: #H; napply (λx:P.x)
690 ##| ##*: #H; napply False_ind;
691 nchange with (match SEC with [ SEC ⇒ False | _ ⇒ True ]);
692 nrewrite > H; nnormalize; napply I
696 ndefinition opcode_destruct75 : Πop2.ΠP:Prop.SEI = op2 → match op2 with [ SEI ⇒ P → P | _ ⇒ P ].
697 #op2; #P; ncases op2; nnormalize;
698 ##[ ##75: #H; napply (λx:P.x)
699 ##| ##*: #H; napply False_ind;
700 nchange with (match SEI with [ SEI ⇒ False | _ ⇒ True ]);
701 nrewrite > H; nnormalize; napply I
705 ndefinition opcode_destruct76 : Πop2.ΠP:Prop.SHA = op2 → match op2 with [ SHA ⇒ P → P | _ ⇒ P ].
706 #op2; #P; ncases op2; nnormalize;
707 ##[ ##76: #H; napply (λx:P.x)
708 ##| ##*: #H; napply False_ind;
709 nchange with (match SHA with [ SHA ⇒ False | _ ⇒ True ]);
710 nrewrite > H; nnormalize; napply I
714 ndefinition opcode_destruct77 : Πop2.ΠP:Prop.SLA = op2 → match op2 with [ SLA ⇒ P → P | _ ⇒ P ].
715 #op2; #P; ncases op2; nnormalize;
716 ##[ ##77: #H; napply (λx:P.x)
717 ##| ##*: #H; napply False_ind;
718 nchange with (match SLA with [ SLA ⇒ False | _ ⇒ True ]);
719 nrewrite > H; nnormalize; napply I
723 ndefinition opcode_destruct78 : Πop2.ΠP:Prop.STA = op2 → match op2 with [ STA ⇒ P → P | _ ⇒ P ].
724 #op2; #P; ncases op2; nnormalize;
725 ##[ ##78: #H; napply (λx:P.x)
726 ##| ##*: #H; napply False_ind;
727 nchange with (match STA with [ STA ⇒ False | _ ⇒ True ]);
728 nrewrite > H; nnormalize; napply I
732 ndefinition opcode_destruct79 : Πop2.ΠP:Prop.STHX = op2 → match op2 with [ STHX ⇒ P → P | _ ⇒ P ].
733 #op2; #P; ncases op2; nnormalize;
734 ##[ ##79: #H; napply (λx:P.x)
735 ##| ##*: #H; napply False_ind;
736 nchange with (match STHX with [ STHX ⇒ False | _ ⇒ True ]);
737 nrewrite > H; nnormalize; napply I
741 ndefinition opcode_destruct80 : Πop2.ΠP:Prop.STOP = op2 → match op2 with [ STOP ⇒ P → P | _ ⇒ P ].
742 #op2; #P; ncases op2; nnormalize;
743 ##[ ##80: #H; napply (λx:P.x)
744 ##| ##*: #H; napply False_ind;
745 nchange with (match STOP with [ STOP ⇒ False | _ ⇒ True ]);
746 nrewrite > H; nnormalize; napply I
750 ndefinition opcode_destruct81 : Πop2.ΠP:Prop.STX = op2 → match op2 with [ STX ⇒ P → P | _ ⇒ P ].
751 #op2; #P; ncases op2; nnormalize;
752 ##[ ##81: #H; napply (λx:P.x)
753 ##| ##*: #H; napply False_ind;
754 nchange with (match STX with [ STX ⇒ False | _ ⇒ True ]);
755 nrewrite > H; nnormalize; napply I
759 ndefinition opcode_destruct82 : Πop2.ΠP:Prop.SUB = op2 → match op2 with [ SUB ⇒ P → P | _ ⇒ P ].
760 #op2; #P; ncases op2; nnormalize;
761 ##[ ##82: #H; napply (λx:P.x)
762 ##| ##*: #H; napply False_ind;
763 nchange with (match SUB with [ SUB ⇒ False | _ ⇒ True ]);
764 nrewrite > H; nnormalize; napply I
768 ndefinition opcode_destruct83 : Πop2.ΠP:Prop.SWI = op2 → match op2 with [ SWI ⇒ P → P | _ ⇒ P ].
769 #op2; #P; ncases op2; nnormalize;
770 ##[ ##83: #H; napply (λx:P.x)
771 ##| ##*: #H; napply False_ind;
772 nchange with (match SWI with [ SWI ⇒ False | _ ⇒ True ]);
773 nrewrite > H; nnormalize; napply I
777 ndefinition opcode_destruct84 : Πop2.ΠP:Prop.TAP = op2 → match op2 with [ TAP ⇒ P → P | _ ⇒ P ].
778 #op2; #P; ncases op2; nnormalize;
779 ##[ ##84: #H; napply (λx:P.x)
780 ##| ##*: #H; napply False_ind;
781 nchange with (match TAP with [ TAP ⇒ False | _ ⇒ True ]);
782 nrewrite > H; nnormalize; napply I
786 ndefinition opcode_destruct85 : Πop2.ΠP:Prop.TAX = op2 → match op2 with [ TAX ⇒ P → P | _ ⇒ P ].
787 #op2; #P; ncases op2; nnormalize;
788 ##[ ##85: #H; napply (λx:P.x)
789 ##| ##*: #H; napply False_ind;
790 nchange with (match TAX with [ TAX ⇒ False | _ ⇒ True ]);
791 nrewrite > H; nnormalize; napply I
795 ndefinition opcode_destruct86 : Πop2.ΠP:Prop.TPA = op2 → match op2 with [ TPA ⇒ P → P | _ ⇒ P ].
796 #op2; #P; ncases op2; nnormalize;
797 ##[ ##86: #H; napply (λx:P.x)
798 ##| ##*: #H; napply False_ind;
799 nchange with (match TPA with [ TPA ⇒ False | _ ⇒ True ]);
800 nrewrite > H; nnormalize; napply I
804 ndefinition opcode_destruct87 : Πop2.ΠP:Prop.TST = op2 → match op2 with [ TST ⇒ P → P | _ ⇒ P ].
805 #op2; #P; ncases op2; nnormalize;
806 ##[ ##87: #H; napply (λx:P.x)
807 ##| ##*: #H; napply False_ind;
808 nchange with (match TST with [ TST ⇒ False | _ ⇒ True ]);
809 nrewrite > H; nnormalize; napply I
813 ndefinition opcode_destruct88 : Πop2.ΠP:Prop.TSX = op2 → match op2 with [ TSX ⇒ P → P | _ ⇒ P ].
814 #op2; #P; ncases op2; nnormalize;
815 ##[ ##88: #H; napply (λx:P.x)
816 ##| ##*: #H; napply False_ind;
817 nchange with (match TSX with [ TSX ⇒ False | _ ⇒ True ]);
818 nrewrite > H; nnormalize; napply I
822 ndefinition opcode_destruct89 : Πop2.ΠP:Prop.TXA = op2 → match op2 with [ TXA ⇒ P → P | _ ⇒ P ].
823 #op2; #P; ncases op2; nnormalize;
824 ##[ ##89: #H; napply (λx:P.x)
825 ##| ##*: #H; napply False_ind;
826 nchange with (match TXA with [ TXA ⇒ False | _ ⇒ True ]);
827 nrewrite > H; nnormalize; napply I
831 ndefinition opcode_destruct90 : Πop2.ΠP:Prop.TXS = op2 → match op2 with [ TXS ⇒ P → P | _ ⇒ P ].
832 #op2; #P; ncases op2; nnormalize;
833 ##[ ##90: #H; napply (λx:P.x)
834 ##| ##*: #H; napply False_ind;
835 nchange with (match TXS with [ TXS ⇒ False | _ ⇒ True ]);
836 nrewrite > H; nnormalize; napply I
840 ndefinition opcode_destruct91 : Πop2.ΠP:Prop.WAIT = op2 → match op2 with [ WAIT ⇒ P → P | _ ⇒ P ].
841 #op2; #P; ncases op2; nnormalize;
842 ##[ ##91: #H; napply (λx:P.x)
843 ##| ##*: #H; napply False_ind;
844 nchange with (match WAIT with [ WAIT ⇒ False | _ ⇒ True ]);
845 nrewrite > H; nnormalize; napply I
849 ndefinition opcode_destruct_aux ≝
850 Πop1,op2.ΠP:Prop.op1 = op2 →
852 [ ADC ⇒ match op2 with [ ADC ⇒ P → P | _ ⇒ P ]
853 | ADD ⇒ match op2 with [ ADD ⇒ P → P | _ ⇒ P ]
854 | AIS ⇒ match op2 with [ AIS ⇒ P → P | _ ⇒ P ]
855 | AIX ⇒ match op2 with [ AIX ⇒ P → P | _ ⇒ P ]
856 | AND ⇒ match op2 with [ AND ⇒ P → P | _ ⇒ P ]
857 | ASL ⇒ match op2 with [ ASL ⇒ P → P | _ ⇒ P ]
858 | ASR ⇒ match op2 with [ ASR ⇒ P → P | _ ⇒ P ]
859 | BCC ⇒ match op2 with [ BCC ⇒ P → P | _ ⇒ P ]
860 | BCLRn ⇒ match op2 with [ BCLRn ⇒ P → P | _ ⇒ P ]
861 | BCS ⇒ match op2 with [ BCS ⇒ P → P | _ ⇒ P ]
862 | BEQ ⇒ match op2 with [ BEQ ⇒ P → P | _ ⇒ P ]
863 | BGE ⇒ match op2 with [ BGE ⇒ P → P | _ ⇒ P ]
864 | BGND ⇒ match op2 with [ BGND ⇒ P → P | _ ⇒ P ]
865 | BGT ⇒ match op2 with [ BGT ⇒ P → P | _ ⇒ P ]
866 | BHCC ⇒ match op2 with [ BHCC ⇒ P → P | _ ⇒ P ]
867 | BHCS ⇒ match op2 with [ BHCS ⇒ P → P | _ ⇒ P ]
868 | BHI ⇒ match op2 with [ BHI ⇒ P → P | _ ⇒ P ]
869 | BIH ⇒ match op2 with [ BIH ⇒ P → P | _ ⇒ P ]
870 | BIL ⇒ match op2 with [ BIL ⇒ P → P | _ ⇒ P ]
871 | BIT ⇒ match op2 with [ BIT ⇒ P → P | _ ⇒ P ]
872 | BLE ⇒ match op2 with [ BLE ⇒ P → P | _ ⇒ P ]
873 | BLS ⇒ match op2 with [ BLS ⇒ P → P | _ ⇒ P ]
874 | BLT ⇒ match op2 with [ BLT ⇒ P → P | _ ⇒ P ]
875 | BMC ⇒ match op2 with [ BMC ⇒ P → P | _ ⇒ P ]
876 | BMI ⇒ match op2 with [ BMI ⇒ P → P | _ ⇒ P ]
877 | BMS ⇒ match op2 with [ BMS ⇒ P → P | _ ⇒ P ]
878 | BNE ⇒ match op2 with [ BNE ⇒ P → P | _ ⇒ P ]
879 | BPL ⇒ match op2 with [ BPL ⇒ P → P | _ ⇒ P ]
880 | BRA ⇒ match op2 with [ BRA ⇒ P → P | _ ⇒ P ]
881 | BRCLRn ⇒ match op2 with [ BRCLRn ⇒ P → P | _ ⇒ P ]
882 | BRN ⇒ match op2 with [ BRN ⇒ P → P | _ ⇒ P ]
883 | BRSETn ⇒ match op2 with [ BRSETn ⇒ P → P | _ ⇒ P ]
884 | BSETn ⇒ match op2 with [ BSETn ⇒ P → P | _ ⇒ P ]
885 | BSR ⇒ match op2 with [ BSR ⇒ P → P | _ ⇒ P ]
886 | CBEQA ⇒ match op2 with [ CBEQA ⇒ P → P | _ ⇒ P ]
887 | CBEQX ⇒ match op2 with [ CBEQX ⇒ P → P | _ ⇒ P ]
888 | CLC ⇒ match op2 with [ CLC ⇒ P → P | _ ⇒ P ]
889 | CLI ⇒ match op2 with [ CLI ⇒ P → P | _ ⇒ P ]
890 | CLR ⇒ match op2 with [ CLR ⇒ P → P | _ ⇒ P ]
891 | CMP ⇒ match op2 with [ CMP ⇒ P → P | _ ⇒ P ]
892 | COM ⇒ match op2 with [ COM ⇒ P → P | _ ⇒ P ]
893 | CPHX ⇒ match op2 with [ CPHX ⇒ P → P | _ ⇒ P ]
894 | CPX ⇒ match op2 with [ CPX ⇒ P → P | _ ⇒ P ]
895 | DAA ⇒ match op2 with [ DAA ⇒ P → P | _ ⇒ P ]
896 | DBNZ ⇒ match op2 with [ DBNZ ⇒ P → P | _ ⇒ P ]
897 | DEC ⇒ match op2 with [ DEC ⇒ P → P | _ ⇒ P ]
898 | DIV ⇒ match op2 with [ DIV ⇒ P → P | _ ⇒ P ]
899 | EOR ⇒ match op2 with [ EOR ⇒ P → P | _ ⇒ P ]
900 | INC ⇒ match op2 with [ INC ⇒ P → P | _ ⇒ P ]
901 | JMP ⇒ match op2 with [ JMP ⇒ P → P | _ ⇒ P ]
902 | JSR ⇒ match op2 with [ JSR ⇒ P → P | _ ⇒ P ]
903 | LDA ⇒ match op2 with [ LDA ⇒ P → P | _ ⇒ P ]
904 | LDHX ⇒ match op2 with [ LDHX ⇒ P → P | _ ⇒ P ]
905 | LDX ⇒ match op2 with [ LDX ⇒ P → P | _ ⇒ P ]
906 | LSR ⇒ match op2 with [ LSR ⇒ P → P | _ ⇒ P ]
907 | MOV ⇒ match op2 with [ MOV ⇒ P → P | _ ⇒ P ]
908 | MUL ⇒ match op2 with [ MUL ⇒ P → P | _ ⇒ P ]
909 | NEG ⇒ match op2 with [ NEG ⇒ P → P | _ ⇒ P ]
910 | NOP ⇒ match op2 with [ NOP ⇒ P → P | _ ⇒ P ]
911 | NSA ⇒ match op2 with [ NSA ⇒ P → P | _ ⇒ P ]
912 | ORA ⇒ match op2 with [ ORA ⇒ P → P | _ ⇒ P ]
913 | PSHA ⇒ match op2 with [ PSHA ⇒ P → P | _ ⇒ P ]
914 | PSHH ⇒ match op2 with [ PSHH ⇒ P → P | _ ⇒ P ]
915 | PSHX ⇒ match op2 with [ PSHX ⇒ P → P | _ ⇒ P ]
916 | PULA ⇒ match op2 with [ PULA ⇒ P → P | _ ⇒ P ]
917 | PULH ⇒ match op2 with [ PULH ⇒ P → P | _ ⇒ P ]
918 | PULX ⇒ match op2 with [ PULX ⇒ P → P | _ ⇒ P ]
919 | ROL ⇒ match op2 with [ ROL ⇒ P → P | _ ⇒ P ]
920 | ROR ⇒ match op2 with [ ROR ⇒ P → P | _ ⇒ P ]
921 | RSP ⇒ match op2 with [ RSP ⇒ P → P | _ ⇒ P ]
922 | RTI ⇒ match op2 with [ RTI ⇒ P → P | _ ⇒ P ]
923 | RTS ⇒ match op2 with [ RTS ⇒ P → P | _ ⇒ P ]
924 | SBC ⇒ match op2 with [ SBC ⇒ P → P | _ ⇒ P ]
925 | SEC ⇒ match op2 with [ SEC ⇒ P → P | _ ⇒ P ]
926 | SEI ⇒ match op2 with [ SEI ⇒ P → P | _ ⇒ P ]
927 | SHA ⇒ match op2 with [ SHA ⇒ P → P | _ ⇒ P ]
928 | SLA ⇒ match op2 with [ SLA ⇒ P → P | _ ⇒ P ]
929 | STA ⇒ match op2 with [ STA ⇒ P → P | _ ⇒ P ]
930 | STHX ⇒ match op2 with [ STHX ⇒ P → P | _ ⇒ P ]
931 | STOP ⇒ match op2 with [ STOP ⇒ P → P | _ ⇒ P ]
932 | STX ⇒ match op2 with [ STX ⇒ P → P | _ ⇒ P ]
933 | SUB ⇒ match op2 with [ SUB ⇒ P → P | _ ⇒ P ]
934 | SWI ⇒ match op2 with [ SWI ⇒ P → P | _ ⇒ P ]
935 | TAP ⇒ match op2 with [ TAP ⇒ P → P | _ ⇒ P ]
936 | TAX ⇒ match op2 with [ TAX ⇒ P → P | _ ⇒ P ]
937 | TPA ⇒ match op2 with [ TPA ⇒ P → P | _ ⇒ P ]
938 | TST ⇒ match op2 with [ TST ⇒ P → P | _ ⇒ P ]
939 | TSX ⇒ match op2 with [ TSX ⇒ P → P | _ ⇒ P ]
940 | TXA ⇒ match op2 with [ TXA ⇒ P → P | _ ⇒ P ]
941 | TXS ⇒ match op2 with [ TXS ⇒ P → P | _ ⇒ P ]
942 | WAIT ⇒ match op2 with [ WAIT ⇒ P → P | _ ⇒ P ]
945 ndefinition opcode_destruct : opcode_destruct_aux.
947 ##[ ##1: napply opcode_destruct1 ##| ##2: napply opcode_destruct2 ##| ##3: napply opcode_destruct3 ##| ##4: napply opcode_destruct4
948 ##| ##5: napply opcode_destruct5 ##| ##6: napply opcode_destruct6 ##| ##7: napply opcode_destruct7 ##| ##8: napply opcode_destruct8
949 ##| ##9: napply opcode_destruct9 ##| ##10: napply opcode_destruct10 ##| ##11: napply opcode_destruct11 ##| ##12: napply opcode_destruct12
950 ##| ##13: napply opcode_destruct13 ##| ##14: napply opcode_destruct14 ##| ##15: napply opcode_destruct15 ##| ##16: napply opcode_destruct16
951 ##| ##17: napply opcode_destruct17 ##| ##18: napply opcode_destruct18 ##| ##19: napply opcode_destruct19 ##| ##20: napply opcode_destruct20
952 ##| ##21: napply opcode_destruct21 ##| ##22: napply opcode_destruct22 ##| ##23: napply opcode_destruct23 ##| ##24: napply opcode_destruct24
953 ##| ##25: napply opcode_destruct25 ##| ##26: napply opcode_destruct26 ##| ##27: napply opcode_destruct27 ##| ##28: napply opcode_destruct28
954 ##| ##29: napply opcode_destruct29 ##| ##30: napply opcode_destruct30 ##| ##31: napply opcode_destruct31 ##| ##32: napply opcode_destruct32
955 ##| ##33: napply opcode_destruct33 ##| ##34: napply opcode_destruct34 ##| ##35: napply opcode_destruct35 ##| ##36: napply opcode_destruct36
956 ##| ##37: napply opcode_destruct37 ##| ##38: napply opcode_destruct38 ##| ##39: napply opcode_destruct39 ##| ##40: napply opcode_destruct40
957 ##| ##41: napply opcode_destruct41 ##| ##42: napply opcode_destruct42 ##| ##43: napply opcode_destruct43 ##| ##44: napply opcode_destruct44
958 ##| ##45: napply opcode_destruct45 ##| ##46: napply opcode_destruct46 ##| ##47: napply opcode_destruct47 ##| ##48: napply opcode_destruct48
959 ##| ##49: napply opcode_destruct49 ##| ##50: napply opcode_destruct50 ##| ##51: napply opcode_destruct51 ##| ##52: napply opcode_destruct52
960 ##| ##53: napply opcode_destruct53 ##| ##54: napply opcode_destruct54 ##| ##55: napply opcode_destruct55 ##| ##56: napply opcode_destruct56
961 ##| ##57: napply opcode_destruct57 ##| ##58: napply opcode_destruct58 ##| ##59: napply opcode_destruct59 ##| ##60: napply opcode_destruct60
962 ##| ##61: napply opcode_destruct61 ##| ##62: napply opcode_destruct62 ##| ##63: napply opcode_destruct63 ##| ##64: napply opcode_destruct64
963 ##| ##65: napply opcode_destruct65 ##| ##66: napply opcode_destruct66 ##| ##67: napply opcode_destruct67 ##| ##68: napply opcode_destruct68
964 ##| ##69: napply opcode_destruct69 ##| ##70: napply opcode_destruct70 ##| ##71: napply opcode_destruct71 ##| ##72: napply opcode_destruct72
965 ##| ##73: napply opcode_destruct73 ##| ##74: napply opcode_destruct74 ##| ##75: napply opcode_destruct75 ##| ##76: napply opcode_destruct76
966 ##| ##77: napply opcode_destruct77 ##| ##78: napply opcode_destruct78 ##| ##79: napply opcode_destruct79 ##| ##80: napply opcode_destruct80
967 ##| ##81: napply opcode_destruct81 ##| ##82: napply opcode_destruct82 ##| ##83: napply opcode_destruct83 ##| ##84: napply opcode_destruct84
968 ##| ##85: napply opcode_destruct85 ##| ##86: napply opcode_destruct86 ##| ##87: napply opcode_destruct87 ##| ##88: napply opcode_destruct88
969 ##| ##89: napply opcode_destruct89 ##| ##90: napply opcode_destruct90 ##| ##91: napply opcode_destruct91 ##]