helm/software/matita/contribs/ng_assembly/freescale/opcode_base_lemmas_opcode1.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* ********************************************************************** *)
  16 (*                          Progetto FreeScale                            *)
  17 (*                                                                        *)
  18 (*   Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it                   *)
  19 (*     Cosimo Oliboni, oliboni@cs.unibo.it                                *)
  20 (*                                                                        *)
  21 (* ********************************************************************** *)
  22
  23 include "freescale/bool_lemmas.ma".
  24 include "freescale/opcode_base.ma".
  25
  26 (* ********************************************** *)
  27 (* MATTONI BASE PER DEFINIRE LE TABELLE DELLE MCU *)
  28 (* ********************************************** *)
  29
  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
  36  ##]
  37 nqed.
  38
  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
  45  ##]
  46 nqed.
  47
  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
  54  ##]
  55 nqed.
  56
  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
  63  ##]
  64 nqed.
  65
  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
  72  ##]
  73 nqed.
  74
  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
  81  ##]
  82 nqed.
  83
  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
  90  ##]
  91 nqed.
  92
  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
  99  ##]
 100 nqed.
 101
 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
 108  ##]
 109 nqed.
 110
 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
 117  ##]
 118 nqed.
 119
 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
 126  ##]
 127 nqed.
 128
 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
 135  ##]
 136 nqed.
 137
 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
 144  ##]
 145 nqed.
 146
 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
 153  ##]
 154 nqed.
 155
 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
 162  ##]
 163 nqed.
 164
 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
 171  ##]
 172 nqed.
 173
 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
 180  ##]
 181 nqed.
 182
 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
 189  ##]
 190 nqed.
 191
 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
 198  ##]
 199 nqed.
 200
 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
 207  ##]
 208 nqed.
 209
 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
 216  ##]
 217 nqed.
 218
 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
 225  ##]
 226 nqed.
 227
 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
 234  ##]
 235 nqed.
 236
 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
 243  ##]
 244 nqed.
 245
 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
 252  ##]
 253 nqed.
 254
 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
 261  ##]
 262 nqed.
 263
 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
 270  ##]
 271 nqed.
 272
 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
 279  ##]
 280 nqed.
 281
 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
 288  ##]
 289 nqed.
 290
 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
 297  ##]
 298 nqed.
 299
 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
 306  ##]
 307 nqed.
 308
 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
 315  ##]
 316 nqed.
 317
 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
 324  ##]
 325 nqed.
 326
 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
 333  ##]
 334 nqed.
 335
 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
 342  ##]
 343 nqed.
 344
 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
 351  ##]
 352 nqed.
 353
 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
 360  ##]
 361 nqed.
 362
 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
 369  ##]
 370 nqed.
 371
 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
 378  ##]
 379 nqed.
 380
 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
 387  ##]
 388 nqed.
 389
 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
 396  ##]
 397 nqed.
 398
 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
 405  ##]
 406 nqed.
 407
 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
 414  ##]
 415 nqed.
 416
 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
 423  ##]
 424 nqed.
 425
 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
 432  ##]
 433 nqed.
 434
 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
 441  ##]
 442 nqed.
 443
 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
 450  ##]
 451 nqed.
 452
 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
 459  ##]
 460 nqed.
 461
 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
 468  ##]
 469 nqed.
 470
 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
 477  ##]
 478 nqed.
 479
 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
 486  ##]
 487 nqed.
 488
 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
 495  ##]
 496 nqed.
 497
 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
 504  ##]
 505 nqed.
 506
 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
 513  ##]
 514 nqed.
 515
 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
 522  ##]
 523 nqed.
 524
 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
 531  ##]
 532 nqed.
 533
 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
 540  ##]
 541 nqed.
 542
 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
 549  ##]
 550 nqed.
 551
 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
 558  ##]
 559 nqed.
 560
 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
 567  ##]
 568 nqed.
 569
 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
 576  ##]
 577 nqed.
 578
 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
 585  ##]
 586 nqed.
 587
 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
 594  ##]
 595 nqed.
 596
 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
 603  ##]
 604 nqed.
 605
 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
 612  ##]
 613 nqed.
 614
 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
 621  ##]
 622 nqed.
 623
 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
 630  ##]
 631 nqed.
 632
 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
 639  ##]
 640 nqed.
 641
 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
 648  ##]
 649 nqed.
 650
 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
 657  ##]
 658 nqed.
 659
 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
 666  ##]
 667 nqed.
 668
 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
 675  ##]
 676 nqed.
 677
 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
 684  ##]
 685 nqed.
 686
 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
 693  ##]
 694 nqed.
 695
 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
 702  ##]
 703 nqed.
 704
 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
 711  ##]
 712 nqed.
 713
 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
 720  ##]
 721 nqed.
 722
 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
 729  ##]
 730 nqed.
 731
 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
 738  ##]
 739 nqed.
 740
 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
 747  ##]
 748 nqed.
 749
 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
 756  ##]
 757 nqed.
 758
 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
 765  ##]
 766 nqed.
 767
 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
 774  ##]
 775 nqed.
 776
 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
 783  ##]
 784 nqed.
 785
 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
 792  ##]
 793 nqed.
 794
 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
 801  ##]
 802 nqed.
 803
 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
 810  ##]
 811 nqed.
 812
 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
 819  ##]
 820 nqed.
 821
 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
 828  ##]
 829 nqed.
 830
 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
 837  ##]
 838 nqed.
 839
 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
 846  ##]
 847 nqed.
 848
 849 ndefinition opcode_destruct_aux ≝
 850 Πop1,op2.ΠP:Prop.op1 = op2 →
 851  match op1 with
 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 ]
 943   ].
 944
 945 ndefinition opcode_destruct : opcode_destruct_aux.
 946  #op1; ncases op1;
 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 ##]
 970 nqed.