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:                                                         *)
  19 (*   Cosimo Oliboni, oliboni@cs.unibo.it                                  *)
  20 (*                                                                        *)
  21 (* Questo materiale fa parte della tesi:                                  *)
  22 (*   "Formalizzazione Interattiva dei Microcontroller a 8bit FreeScale"   *)
  23 (*                                                                        *)
  24 (*                    data ultima modifica 15/11/2007                     *)
  25 (* ********************************************************************** *)
  26
  27 include "freescale/bool_lemmas.ma".
  28 include "freescale/opcode_base.ma".
  29
  30 (* ********************************************** *)
  31 (* MATTONI BASE PER DEFINIRE LE TABELLE DELLE MCU *)
  32 (* ********************************************** *)
  33
  34 ndefinition opcode_destruct1 : Πop2.ΠP:Prop.ADC = op2 → match op2 with [ ADC ⇒ P → P | _ ⇒ P ].
  35  #op2; #P; ncases op2; nnormalize;
  36  ##[ ##1: #H; napply (λx:P.x)
  37  ##| ##*: #H; napply (False_ind ??);
  38           nchange with (match ADC with [ ADC ⇒ False | _ ⇒ True ]);
  39           nrewrite > H; nnormalize; napply I
  40  ##]
  41 nqed.
  42
  43 ndefinition opcode_destruct2 : Πop2.ΠP:Prop.ADD = op2 → match op2 with [ ADD ⇒ P → P | _ ⇒ P ].
  44  #op2; #P; ncases op2; nnormalize;
  45  ##[ ##2: #H; napply (λx:P.x)
  46  ##| ##*: #H; napply (False_ind ??);
  47           nchange with (match ADD with [ ADD ⇒ False | _ ⇒ True ]);
  48           nrewrite > H; nnormalize; napply I
  49  ##]
  50 nqed.
  51
  52 ndefinition opcode_destruct3 : Πop2.ΠP:Prop.AIS = op2 → match op2 with [ AIS ⇒ P → P | _ ⇒ P ].
  53  #op2; #P; ncases op2; nnormalize;
  54  ##[ ##3: #H; napply (λx:P.x)
  55  ##| ##*: #H; napply (False_ind ??);
  56           nchange with (match AIS with [ AIS ⇒ False | _ ⇒ True ]);
  57           nrewrite > H; nnormalize; napply I
  58  ##]
  59 nqed.
  60
  61 ndefinition opcode_destruct4 : Πop2.ΠP:Prop.AIX = op2 → match op2 with [ AIX ⇒ P → P | _ ⇒ P ].
  62  #op2; #P; ncases op2; nnormalize;
  63  ##[ ##4: #H; napply (λx:P.x)
  64  ##| ##*: #H; napply (False_ind ??);
  65           nchange with (match AIX with [ AIX ⇒ False | _ ⇒ True ]);
  66           nrewrite > H; nnormalize; napply I
  67  ##]
  68 nqed.
  69
  70 ndefinition opcode_destruct5 : Πop2.ΠP:Prop.AND = op2 → match op2 with [ AND ⇒ P → P | _ ⇒ P ].
  71  #op2; #P; ncases op2; nnormalize;
  72  ##[ ##5: #H; napply (λx:P.x)
  73  ##| ##*: #H; napply (False_ind ??);
  74           nchange with (match AND with [ AND ⇒ False | _ ⇒ True ]);
  75           nrewrite > H; nnormalize; napply I
  76  ##]
  77 nqed.
  78
  79 ndefinition opcode_destruct6 : Πop2.ΠP:Prop.ASL = op2 → match op2 with [ ASL ⇒ P → P | _ ⇒ P ].
  80  #op2; #P; ncases op2; nnormalize;
  81  ##[ ##6: #H; napply (λx:P.x)
  82  ##| ##*: #H; napply (False_ind ??);
  83           nchange with (match ASL with [ ASL ⇒ False | _ ⇒ True ]);
  84           nrewrite > H; nnormalize; napply I
  85  ##]
  86 nqed.
  87
  88 ndefinition opcode_destruct7 : Πop2.ΠP:Prop.ASR = op2 → match op2 with [ ASR ⇒ P → P | _ ⇒ P ].
  89  #op2; #P; ncases op2; nnormalize;
  90  ##[ ##7: #H; napply (λx:P.x)
  91  ##| ##*: #H; napply (False_ind ??);
  92           nchange with (match ASR with [ ASR ⇒ False | _ ⇒ True ]);
  93           nrewrite > H; nnormalize; napply I
  94  ##]
  95 nqed.
  96
  97 ndefinition opcode_destruct8 : Πop2.ΠP:Prop.BCC = op2 → match op2 with [ BCC ⇒ P → P | _ ⇒ P ].
  98  #op2; #P; ncases op2; nnormalize;
  99  ##[ ##8: #H; napply (λx:P.x)
 100  ##| ##*: #H; napply (False_ind ??);
 101           nchange with (match BCC with [ BCC ⇒ False | _ ⇒ True ]);
 102           nrewrite > H; nnormalize; napply I
 103  ##]
 104 nqed.
 105
 106 ndefinition opcode_destruct9 : Πop2.ΠP:Prop.BCLRn = op2 → match op2 with [ BCLRn ⇒ P → P | _ ⇒ P ].
 107  #op2; #P; ncases op2; nnormalize;
 108  ##[ ##9: #H; napply (λx:P.x)
 109  ##| ##*: #H; napply (False_ind ??);
 110           nchange with (match BCLRn with [ BCLRn ⇒ False | _ ⇒ True ]);
 111           nrewrite > H; nnormalize; napply I
 112  ##]
 113 nqed.
 114
 115 ndefinition opcode_destruct10 : Πop2.ΠP:Prop.BCS = op2 → match op2 with [ BCS ⇒ P → P | _ ⇒ P ].
 116  #op2; #P; ncases op2; nnormalize;
 117  ##[ ##10: #H; napply (λx:P.x)
 118  ##| ##*: #H; napply (False_ind ??);
 119           nchange with (match BCS with [ BCS ⇒ False | _ ⇒ True ]);
 120           nrewrite > H; nnormalize; napply I
 121  ##]
 122 nqed.
 123
 124 ndefinition opcode_destruct11 : Πop2.ΠP:Prop.BEQ = op2 → match op2 with [ BEQ ⇒ P → P | _ ⇒ P ].
 125  #op2; #P; ncases op2; nnormalize;
 126  ##[ ##11: #H; napply (λx:P.x)
 127  ##| ##*: #H; napply (False_ind ??);
 128           nchange with (match BEQ with [ BEQ ⇒ False | _ ⇒ True ]);
 129           nrewrite > H; nnormalize; napply I
 130  ##]
 131 nqed.
 132
 133 ndefinition opcode_destruct12 : Πop2.ΠP:Prop.BGE = op2 → match op2 with [ BGE ⇒ P → P | _ ⇒ P ].
 134  #op2; #P; ncases op2; nnormalize;
 135  ##[ ##12: #H; napply (λx:P.x)
 136  ##| ##*: #H; napply (False_ind ??);
 137           nchange with (match BGE with [ BGE ⇒ False | _ ⇒ True ]);
 138           nrewrite > H; nnormalize; napply I
 139  ##]
 140 nqed.
 141
 142 ndefinition opcode_destruct13 : Πop2.ΠP:Prop.BGND = op2 → match op2 with [ BGND ⇒ P → P | _ ⇒ P ].
 143  #op2; #P; ncases op2; nnormalize;
 144  ##[ ##13: #H; napply (λx:P.x)
 145  ##| ##*: #H; napply (False_ind ??);
 146           nchange with (match BGND with [ BGND ⇒ False | _ ⇒ True ]);
 147           nrewrite > H; nnormalize; napply I
 148  ##]
 149 nqed.
 150
 151 ndefinition opcode_destruct14 : Πop2.ΠP:Prop.BGT = op2 → match op2 with [ BGT ⇒ P → P | _ ⇒ P ].
 152  #op2; #P; ncases op2; nnormalize;
 153  ##[ ##14: #H; napply (λx:P.x)
 154  ##| ##*: #H; napply (False_ind ??);
 155           nchange with (match BGT with [ BGT ⇒ False | _ ⇒ True ]);
 156           nrewrite > H; nnormalize; napply I
 157  ##]
 158 nqed.
 159
 160 ndefinition opcode_destruct15 : Πop2.ΠP:Prop.BHCC = op2 → match op2 with [ BHCC ⇒ P → P | _ ⇒ P ].
 161  #op2; #P; ncases op2; nnormalize;
 162  ##[ ##15: #H; napply (λx:P.x)
 163  ##| ##*: #H; napply (False_ind ??);
 164           nchange with (match BHCC with [ BHCC ⇒ False | _ ⇒ True ]);
 165           nrewrite > H; nnormalize; napply I
 166  ##]
 167 nqed.
 168
 169 ndefinition opcode_destruct16 : Πop2.ΠP:Prop.BHCS = op2 → match op2 with [ BHCS ⇒ P → P | _ ⇒ P ].
 170  #op2; #P; ncases op2; nnormalize;
 171  ##[ ##16: #H; napply (λx:P.x)
 172  ##| ##*: #H; napply (False_ind ??);
 173           nchange with (match BHCS with [ BHCS ⇒ False | _ ⇒ True ]);
 174           nrewrite > H; nnormalize; napply I
 175  ##]
 176 nqed.
 177
 178 ndefinition opcode_destruct17 : Πop2.ΠP:Prop.BHI = op2 → match op2 with [ BHI ⇒ P → P | _ ⇒ P ].
 179  #op2; #P; ncases op2; nnormalize;
 180  ##[ ##17: #H; napply (λx:P.x)
 181  ##| ##*: #H; napply (False_ind ??);
 182           nchange with (match BHI with [ BHI ⇒ False | _ ⇒ True ]);
 183           nrewrite > H; nnormalize; napply I
 184  ##]
 185 nqed.
 186
 187 ndefinition opcode_destruct18 : Πop2.ΠP:Prop.BIH = op2 → match op2 with [ BIH ⇒ P → P | _ ⇒ P ].
 188  #op2; #P; ncases op2; nnormalize;
 189  ##[ ##18: #H; napply (λx:P.x)
 190  ##| ##*: #H; napply (False_ind ??);
 191           nchange with (match BIH with [ BIH ⇒ False | _ ⇒ True ]);
 192           nrewrite > H; nnormalize; napply I
 193  ##]
 194 nqed.
 195
 196 ndefinition opcode_destruct19 : Πop2.ΠP:Prop.BIL = op2 → match op2 with [ BIL ⇒ P → P | _ ⇒ P ].
 197  #op2; #P; ncases op2; nnormalize;
 198  ##[ ##19: #H; napply (λx:P.x)
 199  ##| ##*: #H; napply (False_ind ??);
 200           nchange with (match BIL with [ BIL ⇒ False | _ ⇒ True ]);
 201           nrewrite > H; nnormalize; napply I
 202  ##]
 203 nqed.
 204
 205 ndefinition opcode_destruct20 : Πop2.ΠP:Prop.BIT = op2 → match op2 with [ BIT ⇒ P → P | _ ⇒ P ].
 206  #op2; #P; ncases op2; nnormalize;
 207  ##[ ##20: #H; napply (λx:P.x)
 208  ##| ##*: #H; napply (False_ind ??);
 209           nchange with (match BIT with [ BIT ⇒ False | _ ⇒ True ]);
 210           nrewrite > H; nnormalize; napply I
 211  ##]
 212 nqed.
 213
 214 ndefinition opcode_destruct21 : Πop2.ΠP:Prop.BLE = op2 → match op2 with [ BLE ⇒ P → P | _ ⇒ P ].
 215  #op2; #P; ncases op2; nnormalize;
 216  ##[ ##21: #H; napply (λx:P.x)
 217  ##| ##*: #H; napply (False_ind ??);
 218           nchange with (match BLE with [ BLE ⇒ False | _ ⇒ True ]);
 219           nrewrite > H; nnormalize; napply I
 220  ##]
 221 nqed.
 222
 223 ndefinition opcode_destruct22 : Πop2.ΠP:Prop.BLS = op2 → match op2 with [ BLS ⇒ P → P | _ ⇒ P ].
 224  #op2; #P; ncases op2; nnormalize;
 225  ##[ ##22: #H; napply (λx:P.x)
 226  ##| ##*: #H; napply (False_ind ??);
 227           nchange with (match BLS with [ BLS ⇒ False | _ ⇒ True ]);
 228           nrewrite > H; nnormalize; napply I
 229  ##]
 230 nqed.
 231
 232 ndefinition opcode_destruct23 : Πop2.ΠP:Prop.BLT = op2 → match op2 with [ BLT ⇒ P → P | _ ⇒ P ].
 233  #op2; #P; ncases op2; nnormalize;
 234  ##[ ##23: #H; napply (λx:P.x)
 235  ##| ##*: #H; napply (False_ind ??);
 236           nchange with (match BLT with [ BLT ⇒ False | _ ⇒ True ]);
 237           nrewrite > H; nnormalize; napply I
 238  ##]
 239 nqed.
 240
 241 ndefinition opcode_destruct24 : Πop2.ΠP:Prop.BMC = op2 → match op2 with [ BMC ⇒ P → P | _ ⇒ P ].
 242  #op2; #P; ncases op2; nnormalize;
 243  ##[ ##24: #H; napply (λx:P.x)
 244  ##| ##*: #H; napply (False_ind ??);
 245           nchange with (match BMC with [ BMC ⇒ False | _ ⇒ True ]);
 246           nrewrite > H; nnormalize; napply I
 247  ##]
 248 nqed.
 249
 250 ndefinition opcode_destruct25 : Πop2.ΠP:Prop.BMI = op2 → match op2 with [ BMI ⇒ P → P | _ ⇒ P ].
 251  #op2; #P; ncases op2; nnormalize;
 252  ##[ ##25: #H; napply (λx:P.x)
 253  ##| ##*: #H; napply (False_ind ??);
 254           nchange with (match BMI with [ BMI ⇒ False | _ ⇒ True ]);
 255           nrewrite > H; nnormalize; napply I
 256  ##]
 257 nqed.
 258
 259 ndefinition opcode_destruct26 : Πop2.ΠP:Prop.BMS = op2 → match op2 with [ BMS ⇒ P → P | _ ⇒ P ].
 260  #op2; #P; ncases op2; nnormalize;
 261  ##[ ##26: #H; napply (λx:P.x)
 262  ##| ##*: #H; napply (False_ind ??);
 263           nchange with (match BMS with [ BMS ⇒ False | _ ⇒ True ]);
 264           nrewrite > H; nnormalize; napply I
 265  ##]
 266 nqed.
 267
 268 ndefinition opcode_destruct27 : Πop2.ΠP:Prop.BNE = op2 → match op2 with [ BNE ⇒ P → P | _ ⇒ P ].
 269  #op2; #P; ncases op2; nnormalize;
 270  ##[ ##27: #H; napply (λx:P.x)
 271  ##| ##*: #H; napply (False_ind ??);
 272           nchange with (match BNE with [ BNE ⇒ False | _ ⇒ True ]);
 273           nrewrite > H; nnormalize; napply I
 274  ##]
 275 nqed.
 276
 277 ndefinition opcode_destruct28 : Πop2.ΠP:Prop.BPL = op2 → match op2 with [ BPL ⇒ P → P | _ ⇒ P ].
 278  #op2; #P; ncases op2; nnormalize;
 279  ##[ ##28: #H; napply (λx:P.x)
 280  ##| ##*: #H; napply (False_ind ??);
 281           nchange with (match BPL with [ BPL ⇒ False | _ ⇒ True ]);
 282           nrewrite > H; nnormalize; napply I
 283  ##]
 284 nqed.
 285
 286 ndefinition opcode_destruct29 : Πop2.ΠP:Prop.BRA = op2 → match op2 with [ BRA ⇒ P → P | _ ⇒ P ].
 287  #op2; #P; ncases op2; nnormalize;
 288  ##[ ##29: #H; napply (λx:P.x)
 289  ##| ##*: #H; napply (False_ind ??);
 290           nchange with (match BRA with [ BRA ⇒ False | _ ⇒ True ]);
 291           nrewrite > H; nnormalize; napply I
 292  ##]
 293 nqed.
 294
 295 ndefinition opcode_destruct30 : Πop2.ΠP:Prop.BRCLRn = op2 → match op2 with [ BRCLRn ⇒ P → P | _ ⇒ P ].
 296  #op2; #P; ncases op2; nnormalize;
 297  ##[ ##30: #H; napply (λx:P.x)
 298  ##| ##*: #H; napply (False_ind ??);
 299           nchange with (match BRCLRn with [ BRCLRn ⇒ False | _ ⇒ True ]);
 300           nrewrite > H; nnormalize; napply I
 301  ##]
 302 nqed.
 303
 304 ndefinition opcode_destruct31 : Πop2.ΠP:Prop.BRN = op2 → match op2 with [ BRN ⇒ P → P | _ ⇒ P ].
 305  #op2; #P; ncases op2; nnormalize;
 306  ##[ ##31: #H; napply (λx:P.x)
 307  ##| ##*: #H; napply (False_ind ??);
 308           nchange with (match BRN with [ BRN ⇒ False | _ ⇒ True ]);
 309           nrewrite > H; nnormalize; napply I
 310  ##]
 311 nqed.
 312
 313 ndefinition opcode_destruct32 : Πop2.ΠP:Prop.BRSETn = op2 → match op2 with [ BRSETn ⇒ P → P | _ ⇒ P ].
 314  #op2; #P; ncases op2; nnormalize;
 315  ##[ ##32: #H; napply (λx:P.x)
 316  ##| ##*: #H; napply (False_ind ??);
 317           nchange with (match BRSETn with [ BRSETn ⇒ False | _ ⇒ True ]);
 318           nrewrite > H; nnormalize; napply I
 319  ##]
 320 nqed.
 321
 322 ndefinition opcode_destruct33 : Πop2.ΠP:Prop.BSETn = op2 → match op2 with [ BSETn ⇒ P → P | _ ⇒ P ].
 323  #op2; #P; ncases op2; nnormalize;
 324  ##[ ##33: #H; napply (λx:P.x)
 325  ##| ##*: #H; napply (False_ind ??);
 326           nchange with (match BSETn with [ BSETn ⇒ False | _ ⇒ True ]);
 327           nrewrite > H; nnormalize; napply I
 328  ##]
 329 nqed.
 330
 331 ndefinition opcode_destruct34 : Πop2.ΠP:Prop.BSR = op2 → match op2 with [ BSR ⇒ P → P | _ ⇒ P ].
 332  #op2; #P; ncases op2; nnormalize;
 333  ##[ ##34: #H; napply (λx:P.x)
 334  ##| ##*: #H; napply (False_ind ??);
 335           nchange with (match BSR with [ BSR ⇒ False | _ ⇒ True ]);
 336           nrewrite > H; nnormalize; napply I
 337  ##]
 338 nqed.
 339
 340 ndefinition opcode_destruct35 : Πop2.ΠP:Prop.CBEQA = op2 → match op2 with [ CBEQA ⇒ P → P | _ ⇒ P ].
 341  #op2; #P; ncases op2; nnormalize;
 342  ##[ ##35: #H; napply (λx:P.x)
 343  ##| ##*: #H; napply (False_ind ??);
 344           nchange with (match CBEQA with [ CBEQA ⇒ False | _ ⇒ True ]);
 345           nrewrite > H; nnormalize; napply I
 346  ##]
 347 nqed.
 348
 349 ndefinition opcode_destruct36 : Πop2.ΠP:Prop.CBEQX = op2 → match op2 with [ CBEQX ⇒ P → P | _ ⇒ P ].
 350  #op2; #P; ncases op2; nnormalize;
 351  ##[ ##36: #H; napply (λx:P.x)
 352  ##| ##*: #H; napply (False_ind ??);
 353           nchange with (match CBEQX with [ CBEQX ⇒ False | _ ⇒ True ]);
 354           nrewrite > H; nnormalize; napply I
 355  ##]
 356 nqed.
 357
 358 ndefinition opcode_destruct37 : Πop2.ΠP:Prop.CLC = op2 → match op2 with [ CLC ⇒ P → P | _ ⇒ P ].
 359  #op2; #P; ncases op2; nnormalize;
 360  ##[ ##37: #H; napply (λx:P.x)
 361  ##| ##*: #H; napply (False_ind ??);
 362           nchange with (match CLC with [ CLC ⇒ False | _ ⇒ True ]);
 363           nrewrite > H; nnormalize; napply I
 364  ##]
 365 nqed.
 366
 367 ndefinition opcode_destruct38 : Πop2.ΠP:Prop.CLI = op2 → match op2 with [ CLI ⇒ P → P | _ ⇒ P ].
 368  #op2; #P; ncases op2; nnormalize;
 369  ##[ ##38: #H; napply (λx:P.x)
 370  ##| ##*: #H; napply (False_ind ??);
 371           nchange with (match CLI with [ CLI ⇒ False | _ ⇒ True ]);
 372           nrewrite > H; nnormalize; napply I
 373  ##]
 374 nqed.
 375
 376 ndefinition opcode_destruct39 : Πop2.ΠP:Prop.CLR = op2 → match op2 with [ CLR ⇒ P → P | _ ⇒ P ].
 377  #op2; #P; ncases op2; nnormalize;
 378  ##[ ##39: #H; napply (λx:P.x)
 379  ##| ##*: #H; napply (False_ind ??);
 380           nchange with (match CLR with [ CLR ⇒ False | _ ⇒ True ]);
 381           nrewrite > H; nnormalize; napply I
 382  ##]
 383 nqed.
 384
 385 ndefinition opcode_destruct40 : Πop2.ΠP:Prop.CMP = op2 → match op2 with [ CMP ⇒ P → P | _ ⇒ P ].
 386  #op2; #P; ncases op2; nnormalize;
 387  ##[ ##40: #H; napply (λx:P.x)
 388  ##| ##*: #H; napply (False_ind ??);
 389           nchange with (match CMP with [ CMP ⇒ False | _ ⇒ True ]);
 390           nrewrite > H; nnormalize; napply I
 391  ##]
 392 nqed.
 393
 394 ndefinition opcode_destruct41 : Πop2.ΠP:Prop.COM = op2 → match op2 with [ COM ⇒ P → P | _ ⇒ P ].
 395  #op2; #P; ncases op2; nnormalize;
 396  ##[ ##41: #H; napply (λx:P.x)
 397  ##| ##*: #H; napply (False_ind ??);
 398           nchange with (match COM with [ COM ⇒ False | _ ⇒ True ]);
 399           nrewrite > H; nnormalize; napply I
 400  ##]
 401 nqed.
 402
 403 ndefinition opcode_destruct42 : Πop2.ΠP:Prop.CPHX = op2 → match op2 with [ CPHX ⇒ P → P | _ ⇒ P ].
 404  #op2; #P; ncases op2; nnormalize;
 405  ##[ ##42: #H; napply (λx:P.x)
 406  ##| ##*: #H; napply (False_ind ??);
 407           nchange with (match CPHX with [ CPHX ⇒ False | _ ⇒ True ]);
 408           nrewrite > H; nnormalize; napply I
 409  ##]
 410 nqed.
 411
 412 ndefinition opcode_destruct43 : Πop2.ΠP:Prop.CPX = op2 → match op2 with [ CPX ⇒ P → P | _ ⇒ P ].
 413  #op2; #P; ncases op2; nnormalize;
 414  ##[ ##43: #H; napply (λx:P.x)
 415  ##| ##*: #H; napply (False_ind ??);
 416           nchange with (match CPX with [ CPX ⇒ False | _ ⇒ True ]);
 417           nrewrite > H; nnormalize; napply I
 418  ##]
 419 nqed.
 420
 421 ndefinition opcode_destruct44 : Πop2.ΠP:Prop.DAA = op2 → match op2 with [ DAA ⇒ P → P | _ ⇒ P ].
 422  #op2; #P; ncases op2; nnormalize;
 423  ##[ ##44: #H; napply (λx:P.x)
 424  ##| ##*: #H; napply (False_ind ??);
 425           nchange with (match DAA with [ DAA ⇒ False | _ ⇒ True ]);
 426           nrewrite > H; nnormalize; napply I
 427  ##]
 428 nqed.
 429
 430 ndefinition opcode_destruct45 : Πop2.ΠP:Prop.DBNZ = op2 → match op2 with [ DBNZ ⇒ P → P | _ ⇒ P ].
 431  #op2; #P; ncases op2; nnormalize;
 432  ##[ ##45: #H; napply (λx:P.x)
 433  ##| ##*: #H; napply (False_ind ??);
 434           nchange with (match DBNZ with [ DBNZ ⇒ False | _ ⇒ True ]);
 435           nrewrite > H; nnormalize; napply I
 436  ##]
 437 nqed.
 438
 439 ndefinition opcode_destruct46 : Πop2.ΠP:Prop.DEC = op2 → match op2 with [ DEC ⇒ P → P | _ ⇒ P ].
 440  #op2; #P; ncases op2; nnormalize;
 441  ##[ ##46: #H; napply (λx:P.x)
 442  ##| ##*: #H; napply (False_ind ??);
 443           nchange with (match DEC with [ DEC ⇒ False | _ ⇒ True ]);
 444           nrewrite > H; nnormalize; napply I
 445  ##]
 446 nqed.
 447
 448 ndefinition opcode_destruct47 : Πop2.ΠP:Prop.DIV = op2 → match op2 with [ DIV ⇒ P → P | _ ⇒ P ].
 449  #op2; #P; ncases op2; nnormalize;
 450  ##[ ##47: #H; napply (λx:P.x)
 451  ##| ##*: #H; napply (False_ind ??);
 452           nchange with (match DIV with [ DIV ⇒ False | _ ⇒ True ]);
 453           nrewrite > H; nnormalize; napply I
 454  ##]
 455 nqed.
 456
 457 ndefinition opcode_destruct48 : Πop2.ΠP:Prop.EOR = op2 → match op2 with [ EOR ⇒ P → P | _ ⇒ P ].
 458  #op2; #P; ncases op2; nnormalize;
 459  ##[ ##48: #H; napply (λx:P.x)
 460  ##| ##*: #H; napply (False_ind ??);
 461           nchange with (match EOR with [ EOR ⇒ False | _ ⇒ True ]);
 462           nrewrite > H; nnormalize; napply I
 463  ##]
 464 nqed.
 465
 466 ndefinition opcode_destruct49 : Πop2.ΠP:Prop.INC = op2 → match op2 with [ INC ⇒ P → P | _ ⇒ P ].
 467  #op2; #P; ncases op2; nnormalize;
 468  ##[ ##49: #H; napply (λx:P.x)
 469  ##| ##*: #H; napply (False_ind ??);
 470           nchange with (match INC with [ INC ⇒ False | _ ⇒ True ]);
 471           nrewrite > H; nnormalize; napply I
 472  ##]
 473 nqed.
 474
 475 ndefinition opcode_destruct50 : Πop2.ΠP:Prop.JMP = op2 → match op2 with [ JMP ⇒ P → P | _ ⇒ P ].
 476  #op2; #P; ncases op2; nnormalize;
 477  ##[ ##50: #H; napply (λx:P.x)
 478  ##| ##*: #H; napply (False_ind ??);
 479           nchange with (match JMP with [ JMP ⇒ False | _ ⇒ True ]);
 480           nrewrite > H; nnormalize; napply I
 481  ##]
 482 nqed.
 483
 484 ndefinition opcode_destruct51 : Πop2.ΠP:Prop.JSR = op2 → match op2 with [ JSR ⇒ P → P | _ ⇒ P ].
 485  #op2; #P; ncases op2; nnormalize;
 486  ##[ ##51: #H; napply (λx:P.x)
 487  ##| ##*: #H; napply (False_ind ??);
 488           nchange with (match JSR with [ JSR ⇒ False | _ ⇒ True ]);
 489           nrewrite > H; nnormalize; napply I
 490  ##]
 491 nqed.
 492
 493 ndefinition opcode_destruct52 : Πop2.ΠP:Prop.LDA = op2 → match op2 with [ LDA ⇒ P → P | _ ⇒ P ].
 494  #op2; #P; ncases op2; nnormalize;
 495  ##[ ##52: #H; napply (λx:P.x)
 496  ##| ##*: #H; napply (False_ind ??);
 497           nchange with (match LDA with [ LDA ⇒ False | _ ⇒ True ]);
 498           nrewrite > H; nnormalize; napply I
 499  ##]
 500 nqed.
 501
 502 ndefinition opcode_destruct53 : Πop2.ΠP:Prop.LDHX = op2 → match op2 with [ LDHX ⇒ P → P | _ ⇒ P ].
 503  #op2; #P; ncases op2; nnormalize;
 504  ##[ ##53: #H; napply (λx:P.x)
 505  ##| ##*: #H; napply (False_ind ??);
 506           nchange with (match LDHX with [ LDHX ⇒ False | _ ⇒ True ]);
 507           nrewrite > H; nnormalize; napply I
 508  ##]
 509 nqed.
 510
 511 ndefinition opcode_destruct54 : Πop2.ΠP:Prop.LDX = op2 → match op2 with [ LDX ⇒ P → P | _ ⇒ P ].
 512  #op2; #P; ncases op2; nnormalize;
 513  ##[ ##54: #H; napply (λx:P.x)
 514  ##| ##*: #H; napply (False_ind ??);
 515           nchange with (match LDX with [ LDX ⇒ False | _ ⇒ True ]);
 516           nrewrite > H; nnormalize; napply I
 517  ##]
 518 nqed.
 519
 520 ndefinition opcode_destruct55 : Πop2.ΠP:Prop.LSR = op2 → match op2 with [ LSR ⇒ P → P | _ ⇒ P ].
 521  #op2; #P; ncases op2; nnormalize;
 522  ##[ ##55: #H; napply (λx:P.x)
 523  ##| ##*: #H; napply (False_ind ??);
 524           nchange with (match LSR with [ LSR ⇒ False | _ ⇒ True ]);
 525           nrewrite > H; nnormalize; napply I
 526  ##]
 527 nqed.
 528
 529 ndefinition opcode_destruct56 : Πop2.ΠP:Prop.MOV = op2 → match op2 with [ MOV ⇒ P → P | _ ⇒ P ].
 530  #op2; #P; ncases op2; nnormalize;
 531  ##[ ##56: #H; napply (λx:P.x)
 532  ##| ##*: #H; napply (False_ind ??);
 533           nchange with (match MOV with [ MOV ⇒ False | _ ⇒ True ]);
 534           nrewrite > H; nnormalize; napply I
 535  ##]
 536 nqed.
 537
 538 ndefinition opcode_destruct57 : Πop2.ΠP:Prop.MUL = op2 → match op2 with [ MUL ⇒ P → P | _ ⇒ P ].
 539  #op2; #P; ncases op2; nnormalize;
 540  ##[ ##57: #H; napply (λx:P.x)
 541  ##| ##*: #H; napply (False_ind ??);
 542           nchange with (match MUL with [ MUL ⇒ False | _ ⇒ True ]);
 543           nrewrite > H; nnormalize; napply I
 544  ##]
 545 nqed.
 546
 547 ndefinition opcode_destruct58 : Πop2.ΠP:Prop.NEG = op2 → match op2 with [ NEG ⇒ P → P | _ ⇒ P ].
 548  #op2; #P; ncases op2; nnormalize;
 549  ##[ ##58: #H; napply (λx:P.x)
 550  ##| ##*: #H; napply (False_ind ??);
 551           nchange with (match NEG with [ NEG ⇒ False | _ ⇒ True ]);
 552           nrewrite > H; nnormalize; napply I
 553  ##]
 554 nqed.
 555
 556 ndefinition opcode_destruct59 : Πop2.ΠP:Prop.NOP = op2 → match op2 with [ NOP ⇒ P → P | _ ⇒ P ].
 557  #op2; #P; ncases op2; nnormalize;
 558  ##[ ##59: #H; napply (λx:P.x)
 559  ##| ##*: #H; napply (False_ind ??);
 560           nchange with (match NOP with [ NOP ⇒ False | _ ⇒ True ]);
 561           nrewrite > H; nnormalize; napply I
 562  ##]
 563 nqed.
 564
 565 ndefinition opcode_destruct60 : Πop2.ΠP:Prop.NSA = op2 → match op2 with [ NSA ⇒ P → P | _ ⇒ P ].
 566  #op2; #P; ncases op2; nnormalize;
 567  ##[ ##60: #H; napply (λx:P.x)
 568  ##| ##*: #H; napply (False_ind ??);
 569           nchange with (match NSA with [ NSA ⇒ False | _ ⇒ True ]);
 570           nrewrite > H; nnormalize; napply I
 571  ##]
 572 nqed.
 573
 574 ndefinition opcode_destruct61 : Πop2.ΠP:Prop.ORA = op2 → match op2 with [ ORA ⇒ P → P | _ ⇒ P ].
 575  #op2; #P; ncases op2; nnormalize;
 576  ##[ ##61: #H; napply (λx:P.x)
 577  ##| ##*: #H; napply (False_ind ??);
 578           nchange with (match ORA with [ ORA ⇒ False | _ ⇒ True ]);
 579           nrewrite > H; nnormalize; napply I
 580  ##]
 581 nqed.
 582
 583 ndefinition opcode_destruct62 : Πop2.ΠP:Prop.PSHA = op2 → match op2 with [ PSHA ⇒ P → P | _ ⇒ P ].
 584  #op2; #P; ncases op2; nnormalize;
 585  ##[ ##62: #H; napply (λx:P.x)
 586  ##| ##*: #H; napply (False_ind ??);
 587           nchange with (match PSHA with [ PSHA ⇒ False | _ ⇒ True ]);
 588           nrewrite > H; nnormalize; napply I
 589  ##]
 590 nqed.
 591
 592 ndefinition opcode_destruct63 : Πop2.ΠP:Prop.PSHH = op2 → match op2 with [ PSHH ⇒ P → P | _ ⇒ P ].
 593  #op2; #P; ncases op2; nnormalize;
 594  ##[ ##63: #H; napply (λx:P.x)
 595  ##| ##*: #H; napply (False_ind ??);
 596           nchange with (match PSHH with [ PSHH ⇒ False | _ ⇒ True ]);
 597           nrewrite > H; nnormalize; napply I
 598  ##]
 599 nqed.
 600
 601 ndefinition opcode_destruct64 : Πop2.ΠP:Prop.PSHX = op2 → match op2 with [ PSHX ⇒ P → P | _ ⇒ P ].
 602  #op2; #P; ncases op2; nnormalize;
 603  ##[ ##64: #H; napply (λx:P.x)
 604  ##| ##*: #H; napply (False_ind ??);
 605           nchange with (match PSHX with [ PSHX ⇒ False | _ ⇒ True ]);
 606           nrewrite > H; nnormalize; napply I
 607  ##]
 608 nqed.
 609
 610 ndefinition opcode_destruct65 : Πop2.ΠP:Prop.PULA = op2 → match op2 with [ PULA ⇒ P → P | _ ⇒ P ].
 611  #op2; #P; ncases op2; nnormalize;
 612  ##[ ##65: #H; napply (λx:P.x)
 613  ##| ##*: #H; napply (False_ind ??);
 614           nchange with (match PULA with [ PULA ⇒ False | _ ⇒ True ]);
 615           nrewrite > H; nnormalize; napply I
 616  ##]
 617 nqed.
 618
 619 ndefinition opcode_destruct66 : Πop2.ΠP:Prop.PULH = op2 → match op2 with [ PULH ⇒ P → P | _ ⇒ P ].
 620  #op2; #P; ncases op2; nnormalize;
 621  ##[ ##66: #H; napply (λx:P.x)
 622  ##| ##*: #H; napply (False_ind ??);
 623           nchange with (match PULH with [ PULH ⇒ False | _ ⇒ True ]);
 624           nrewrite > H; nnormalize; napply I
 625  ##]
 626 nqed.
 627
 628 ndefinition opcode_destruct67 : Πop2.ΠP:Prop.PULX = op2 → match op2 with [ PULX ⇒ P → P | _ ⇒ P ].
 629  #op2; #P; ncases op2; nnormalize;
 630  ##[ ##67: #H; napply (λx:P.x)
 631  ##| ##*: #H; napply (False_ind ??);
 632           nchange with (match PULX with [ PULX ⇒ False | _ ⇒ True ]);
 633           nrewrite > H; nnormalize; napply I
 634  ##]
 635 nqed.
 636
 637 ndefinition opcode_destruct68 : Πop2.ΠP:Prop.ROL = op2 → match op2 with [ ROL ⇒ P → P | _ ⇒ P ].
 638  #op2; #P; ncases op2; nnormalize;
 639  ##[ ##68: #H; napply (λx:P.x)
 640  ##| ##*: #H; napply (False_ind ??);
 641           nchange with (match ROL with [ ROL ⇒ False | _ ⇒ True ]);
 642           nrewrite > H; nnormalize; napply I
 643  ##]
 644 nqed.
 645
 646 ndefinition opcode_destruct69 : Πop2.ΠP:Prop.ROR = op2 → match op2 with [ ROR ⇒ P → P | _ ⇒ P ].
 647  #op2; #P; ncases op2; nnormalize;
 648  ##[ ##69: #H; napply (λx:P.x)
 649  ##| ##*: #H; napply (False_ind ??);
 650           nchange with (match ROR with [ ROR ⇒ False | _ ⇒ True ]);
 651           nrewrite > H; nnormalize; napply I
 652  ##]
 653 nqed.
 654
 655 ndefinition opcode_destruct70 : Πop2.ΠP:Prop.RSP = op2 → match op2 with [ RSP ⇒ P → P | _ ⇒ P ].
 656  #op2; #P; ncases op2; nnormalize;
 657  ##[ ##70: #H; napply (λx:P.x)
 658  ##| ##*: #H; napply (False_ind ??);
 659           nchange with (match RSP with [ RSP ⇒ False | _ ⇒ True ]);
 660           nrewrite > H; nnormalize; napply I
 661  ##]
 662 nqed.
 663
 664 ndefinition opcode_destruct71 : Πop2.ΠP:Prop.RTI = op2 → match op2 with [ RTI ⇒ P → P | _ ⇒ P ].
 665  #op2; #P; ncases op2; nnormalize;
 666  ##[ ##71: #H; napply (λx:P.x)
 667  ##| ##*: #H; napply (False_ind ??);
 668           nchange with (match RTI with [ RTI ⇒ False | _ ⇒ True ]);
 669           nrewrite > H; nnormalize; napply I
 670  ##]
 671 nqed.
 672
 673 ndefinition opcode_destruct72 : Πop2.ΠP:Prop.RTS = op2 → match op2 with [ RTS ⇒ P → P | _ ⇒ P ].
 674  #op2; #P; ncases op2; nnormalize;
 675  ##[ ##72: #H; napply (λx:P.x)
 676  ##| ##*: #H; napply (False_ind ??);
 677           nchange with (match RTS with [ RTS ⇒ False | _ ⇒ True ]);
 678           nrewrite > H; nnormalize; napply I
 679  ##]
 680 nqed.
 681
 682 ndefinition opcode_destruct73 : Πop2.ΠP:Prop.SBC = op2 → match op2 with [ SBC ⇒ P → P | _ ⇒ P ].
 683  #op2; #P; ncases op2; nnormalize;
 684  ##[ ##73: #H; napply (λx:P.x)
 685  ##| ##*: #H; napply (False_ind ??);
 686           nchange with (match SBC with [ SBC ⇒ False | _ ⇒ True ]);
 687           nrewrite > H; nnormalize; napply I
 688  ##]
 689 nqed.
 690
 691 ndefinition opcode_destruct74 : Πop2.ΠP:Prop.SEC = op2 → match op2 with [ SEC ⇒ P → P | _ ⇒ P ].
 692  #op2; #P; ncases op2; nnormalize;
 693  ##[ ##74: #H; napply (λx:P.x)
 694  ##| ##*: #H; napply (False_ind ??);
 695           nchange with (match SEC with [ SEC ⇒ False | _ ⇒ True ]);
 696           nrewrite > H; nnormalize; napply I
 697  ##]
 698 nqed.
 699
 700 ndefinition opcode_destruct75 : Πop2.ΠP:Prop.SEI = op2 → match op2 with [ SEI ⇒ P → P | _ ⇒ P ].
 701  #op2; #P; ncases op2; nnormalize;
 702  ##[ ##75: #H; napply (λx:P.x)
 703  ##| ##*: #H; napply (False_ind ??);
 704           nchange with (match SEI with [ SEI ⇒ False | _ ⇒ True ]);
 705           nrewrite > H; nnormalize; napply I
 706  ##]
 707 nqed.
 708
 709 ndefinition opcode_destruct76 : Πop2.ΠP:Prop.SHA = op2 → match op2 with [ SHA ⇒ P → P | _ ⇒ P ].
 710  #op2; #P; ncases op2; nnormalize;
 711  ##[ ##76: #H; napply (λx:P.x)
 712  ##| ##*: #H; napply (False_ind ??);
 713           nchange with (match SHA with [ SHA ⇒ False | _ ⇒ True ]);
 714           nrewrite > H; nnormalize; napply I
 715  ##]
 716 nqed.
 717
 718 ndefinition opcode_destruct77 : Πop2.ΠP:Prop.SLA = op2 → match op2 with [ SLA ⇒ P → P | _ ⇒ P ].
 719  #op2; #P; ncases op2; nnormalize;
 720  ##[ ##77: #H; napply (λx:P.x)
 721  ##| ##*: #H; napply (False_ind ??);
 722           nchange with (match SLA with [ SLA ⇒ False | _ ⇒ True ]);
 723           nrewrite > H; nnormalize; napply I
 724  ##]
 725 nqed.
 726
 727 ndefinition opcode_destruct78 : Πop2.ΠP:Prop.STA = op2 → match op2 with [ STA ⇒ P → P | _ ⇒ P ].
 728  #op2; #P; ncases op2; nnormalize;
 729  ##[ ##78: #H; napply (λx:P.x)
 730  ##| ##*: #H; napply (False_ind ??);
 731           nchange with (match STA with [ STA ⇒ False | _ ⇒ True ]);
 732           nrewrite > H; nnormalize; napply I
 733  ##]
 734 nqed.
 735
 736 ndefinition opcode_destruct79 : Πop2.ΠP:Prop.STHX = op2 → match op2 with [ STHX ⇒ P → P | _ ⇒ P ].
 737  #op2; #P; ncases op2; nnormalize;
 738  ##[ ##79: #H; napply (λx:P.x)
 739  ##| ##*: #H; napply (False_ind ??);
 740           nchange with (match STHX with [ STHX ⇒ False | _ ⇒ True ]);
 741           nrewrite > H; nnormalize; napply I
 742  ##]
 743 nqed.
 744
 745 ndefinition opcode_destruct80 : Πop2.ΠP:Prop.STOP = op2 → match op2 with [ STOP ⇒ P → P | _ ⇒ P ].
 746  #op2; #P; ncases op2; nnormalize;
 747  ##[ ##80: #H; napply (λx:P.x)
 748  ##| ##*: #H; napply (False_ind ??);
 749           nchange with (match STOP with [ STOP ⇒ False | _ ⇒ True ]);
 750           nrewrite > H; nnormalize; napply I
 751  ##]
 752 nqed.
 753
 754 ndefinition opcode_destruct81 : Πop2.ΠP:Prop.STX = op2 → match op2 with [ STX ⇒ P → P | _ ⇒ P ].
 755  #op2; #P; ncases op2; nnormalize;
 756  ##[ ##81: #H; napply (λx:P.x)
 757  ##| ##*: #H; napply (False_ind ??);
 758           nchange with (match STX with [ STX ⇒ False | _ ⇒ True ]);
 759           nrewrite > H; nnormalize; napply I
 760  ##]
 761 nqed.
 762
 763 ndefinition opcode_destruct82 : Πop2.ΠP:Prop.SUB = op2 → match op2 with [ SUB ⇒ P → P | _ ⇒ P ].
 764  #op2; #P; ncases op2; nnormalize;
 765  ##[ ##82: #H; napply (λx:P.x)
 766  ##| ##*: #H; napply (False_ind ??);
 767           nchange with (match SUB with [ SUB ⇒ False | _ ⇒ True ]);
 768           nrewrite > H; nnormalize; napply I
 769  ##]
 770 nqed.
 771
 772 ndefinition opcode_destruct83 : Πop2.ΠP:Prop.SWI = op2 → match op2 with [ SWI ⇒ P → P | _ ⇒ P ].
 773  #op2; #P; ncases op2; nnormalize;
 774  ##[ ##83: #H; napply (λx:P.x)
 775  ##| ##*: #H; napply (False_ind ??);
 776           nchange with (match SWI with [ SWI ⇒ False | _ ⇒ True ]);
 777           nrewrite > H; nnormalize; napply I
 778  ##]
 779 nqed.
 780
 781 ndefinition opcode_destruct84 : Πop2.ΠP:Prop.TAP = op2 → match op2 with [ TAP ⇒ P → P | _ ⇒ P ].
 782  #op2; #P; ncases op2; nnormalize;
 783  ##[ ##84: #H; napply (λx:P.x)
 784  ##| ##*: #H; napply (False_ind ??);
 785           nchange with (match TAP with [ TAP ⇒ False | _ ⇒ True ]);
 786           nrewrite > H; nnormalize; napply I
 787  ##]
 788 nqed.
 789
 790 ndefinition opcode_destruct85 : Πop2.ΠP:Prop.TAX = op2 → match op2 with [ TAX ⇒ P → P | _ ⇒ P ].
 791  #op2; #P; ncases op2; nnormalize;
 792  ##[ ##85: #H; napply (λx:P.x)
 793  ##| ##*: #H; napply (False_ind ??);
 794           nchange with (match TAX with [ TAX ⇒ False | _ ⇒ True ]);
 795           nrewrite > H; nnormalize; napply I
 796  ##]
 797 nqed.
 798
 799 ndefinition opcode_destruct86 : Πop2.ΠP:Prop.TPA = op2 → match op2 with [ TPA ⇒ P → P | _ ⇒ P ].
 800  #op2; #P; ncases op2; nnormalize;
 801  ##[ ##86: #H; napply (λx:P.x)
 802  ##| ##*: #H; napply (False_ind ??);
 803           nchange with (match TPA with [ TPA ⇒ False | _ ⇒ True ]);
 804           nrewrite > H; nnormalize; napply I
 805  ##]
 806 nqed.
 807
 808 ndefinition opcode_destruct87 : Πop2.ΠP:Prop.TST = op2 → match op2 with [ TST ⇒ P → P | _ ⇒ P ].
 809  #op2; #P; ncases op2; nnormalize;
 810  ##[ ##87: #H; napply (λx:P.x)
 811  ##| ##*: #H; napply (False_ind ??);
 812           nchange with (match TST with [ TST ⇒ False | _ ⇒ True ]);
 813           nrewrite > H; nnormalize; napply I
 814  ##]
 815 nqed.
 816
 817 ndefinition opcode_destruct88 : Πop2.ΠP:Prop.TSX = op2 → match op2 with [ TSX ⇒ P → P | _ ⇒ P ].
 818  #op2; #P; ncases op2; nnormalize;
 819  ##[ ##88: #H; napply (λx:P.x)
 820  ##| ##*: #H; napply (False_ind ??);
 821           nchange with (match TSX with [ TSX ⇒ False | _ ⇒ True ]);
 822           nrewrite > H; nnormalize; napply I
 823  ##]
 824 nqed.
 825
 826 ndefinition opcode_destruct89 : Πop2.ΠP:Prop.TXA = op2 → match op2 with [ TXA ⇒ P → P | _ ⇒ P ].
 827  #op2; #P; ncases op2; nnormalize;
 828  ##[ ##89: #H; napply (λx:P.x)
 829  ##| ##*: #H; napply (False_ind ??);
 830           nchange with (match TXA with [ TXA ⇒ False | _ ⇒ True ]);
 831           nrewrite > H; nnormalize; napply I
 832  ##]
 833 nqed.
 834
 835 ndefinition opcode_destruct90 : Πop2.ΠP:Prop.TXS = op2 → match op2 with [ TXS ⇒ P → P | _ ⇒ P ].
 836  #op2; #P; ncases op2; nnormalize;
 837  ##[ ##90: #H; napply (λx:P.x)
 838  ##| ##*: #H; napply (False_ind ??);
 839           nchange with (match TXS with [ TXS ⇒ False | _ ⇒ True ]);
 840           nrewrite > H; nnormalize; napply I
 841  ##]
 842 nqed.
 843
 844 ndefinition opcode_destruct91 : Πop2.ΠP:Prop.WAIT = op2 → match op2 with [ WAIT ⇒ P → P | _ ⇒ P ].
 845  #op2; #P; ncases op2; nnormalize;
 846  ##[ ##91: #H; napply (λx:P.x)
 847  ##| ##*: #H; napply (False_ind ??);
 848           nchange with (match WAIT with [ WAIT ⇒ False | _ ⇒ True ]);
 849           nrewrite > H; nnormalize; napply I
 850  ##]
 851 nqed.
 852
 853 ndefinition opcode_destruct_aux ≝
 854 Πop1,op2.ΠP:Prop.op1 = op2 →
 855  match op1 with
 856   [ ADC ⇒ match op2 with [ ADC ⇒ P → P | _ ⇒ P ]
 857   | ADD ⇒ match op2 with [ ADD ⇒ P → P | _ ⇒ P ]
 858   | AIS ⇒ match op2 with [ AIS ⇒ P → P | _ ⇒ P ]
 859   | AIX ⇒ match op2 with [ AIX ⇒ P → P | _ ⇒ P ]
 860   | AND ⇒ match op2 with [ AND ⇒ P → P | _ ⇒ P ]
 861   | ASL ⇒ match op2 with [ ASL ⇒ P → P | _ ⇒ P ]
 862   | ASR ⇒ match op2 with [ ASR ⇒ P → P | _ ⇒ P ]
 863   | BCC ⇒ match op2 with [ BCC ⇒ P → P | _ ⇒ P ]
 864   | BCLRn ⇒ match op2 with [ BCLRn ⇒ P → P | _ ⇒ P ]
 865   | BCS ⇒ match op2 with [ BCS ⇒ P → P | _ ⇒ P ]
 866   | BEQ ⇒ match op2 with [ BEQ ⇒ P → P | _ ⇒ P ]
 867   | BGE ⇒ match op2 with [ BGE ⇒ P → P | _ ⇒ P ]
 868   | BGND ⇒ match op2 with [ BGND ⇒ P → P | _ ⇒ P ]
 869   | BGT ⇒ match op2 with [ BGT ⇒ P → P | _ ⇒ P ]
 870   | BHCC ⇒ match op2 with [ BHCC ⇒ P → P | _ ⇒ P ]
 871   | BHCS ⇒ match op2 with [ BHCS ⇒ P → P | _ ⇒ P ]
 872   | BHI ⇒ match op2 with [ BHI ⇒ P → P | _ ⇒ P ]
 873   | BIH ⇒ match op2 with [ BIH ⇒ P → P | _ ⇒ P ]
 874   | BIL ⇒ match op2 with [ BIL ⇒ P → P | _ ⇒ P ]
 875   | BIT ⇒ match op2 with [ BIT ⇒ P → P | _ ⇒ P ]
 876   | BLE ⇒ match op2 with [ BLE ⇒ P → P | _ ⇒ P ]
 877   | BLS ⇒ match op2 with [ BLS ⇒ P → P | _ ⇒ P ]
 878   | BLT ⇒ match op2 with [ BLT ⇒ P → P | _ ⇒ P ]
 879   | BMC ⇒ match op2 with [ BMC ⇒ P → P | _ ⇒ P ]
 880   | BMI ⇒ match op2 with [ BMI ⇒ P → P | _ ⇒ P ]
 881   | BMS ⇒ match op2 with [ BMS ⇒ P → P | _ ⇒ P ]
 882   | BNE ⇒ match op2 with [ BNE ⇒ P → P | _ ⇒ P ]
 883   | BPL ⇒ match op2 with [ BPL ⇒ P → P | _ ⇒ P ]
 884   | BRA ⇒ match op2 with [ BRA ⇒ P → P | _ ⇒ P ]
 885   | BRCLRn ⇒ match op2 with [ BRCLRn ⇒ P → P | _ ⇒ P ]
 886   | BRN ⇒ match op2 with [ BRN ⇒ P → P | _ ⇒ P ]
 887   | BRSETn ⇒ match op2 with [ BRSETn ⇒ P → P | _ ⇒ P ]
 888   | BSETn ⇒ match op2 with [ BSETn ⇒ P → P | _ ⇒ P ]
 889   | BSR ⇒ match op2 with [ BSR ⇒ P → P | _ ⇒ P ]
 890   | CBEQA ⇒ match op2 with [ CBEQA ⇒ P → P | _ ⇒ P ]
 891   | CBEQX ⇒ match op2 with [ CBEQX ⇒ P → P | _ ⇒ P ]
 892   | CLC ⇒ match op2 with [ CLC ⇒ P → P | _ ⇒ P ]
 893   | CLI ⇒ match op2 with [ CLI ⇒ P → P | _ ⇒ P ]
 894   | CLR ⇒ match op2 with [ CLR ⇒ P → P | _ ⇒ P ]
 895   | CMP ⇒ match op2 with [ CMP ⇒ P → P | _ ⇒ P ]
 896   | COM ⇒ match op2 with [ COM ⇒ P → P | _ ⇒ P ]
 897   | CPHX ⇒ match op2 with [ CPHX ⇒ P → P | _ ⇒ P ]
 898   | CPX ⇒ match op2 with [ CPX ⇒ P → P | _ ⇒ P ]
 899   | DAA ⇒ match op2 with [ DAA ⇒ P → P | _ ⇒ P ]
 900   | DBNZ ⇒ match op2 with [ DBNZ ⇒ P → P | _ ⇒ P ]
 901   | DEC ⇒ match op2 with [ DEC ⇒ P → P | _ ⇒ P ]
 902   | DIV ⇒ match op2 with [ DIV ⇒ P → P | _ ⇒ P ]
 903   | EOR ⇒ match op2 with [ EOR ⇒ P → P | _ ⇒ P ]
 904   | INC ⇒ match op2 with [ INC ⇒ P → P | _ ⇒ P ]
 905   | JMP ⇒ match op2 with [ JMP ⇒ P → P | _ ⇒ P ]
 906   | JSR ⇒ match op2 with [ JSR ⇒ P → P | _ ⇒ P ]
 907   | LDA ⇒ match op2 with [ LDA ⇒ P → P | _ ⇒ P ]
 908   | LDHX ⇒ match op2 with [ LDHX ⇒ P → P | _ ⇒ P ]
 909   | LDX ⇒ match op2 with [ LDX ⇒ P → P | _ ⇒ P ]
 910   | LSR ⇒ match op2 with [ LSR ⇒ P → P | _ ⇒ P ]
 911   | MOV ⇒ match op2 with [ MOV ⇒ P → P | _ ⇒ P ]
 912   | MUL ⇒ match op2 with [ MUL ⇒ P → P | _ ⇒ P ]
 913   | NEG ⇒ match op2 with [ NEG ⇒ P → P | _ ⇒ P ]
 914   | NOP ⇒ match op2 with [ NOP ⇒ P → P | _ ⇒ P ]
 915   | NSA ⇒ match op2 with [ NSA ⇒ P → P | _ ⇒ P ]
 916   | ORA ⇒ match op2 with [ ORA ⇒ P → P | _ ⇒ P ]
 917   | PSHA ⇒ match op2 with [ PSHA ⇒ P → P | _ ⇒ P ]
 918   | PSHH ⇒ match op2 with [ PSHH ⇒ P → P | _ ⇒ P ]
 919   | PSHX ⇒ match op2 with [ PSHX ⇒ P → P | _ ⇒ P ]
 920   | PULA ⇒ match op2 with [ PULA ⇒ P → P | _ ⇒ P ]
 921   | PULH ⇒ match op2 with [ PULH ⇒ P → P | _ ⇒ P ]
 922   | PULX ⇒ match op2 with [ PULX ⇒ P → P | _ ⇒ P ]
 923   | ROL ⇒ match op2 with [ ROL ⇒ P → P | _ ⇒ P ]
 924   | ROR ⇒ match op2 with [ ROR ⇒ P → P | _ ⇒ P ]
 925   | RSP ⇒ match op2 with [ RSP ⇒ P → P | _ ⇒ P ]
 926   | RTI ⇒ match op2 with [ RTI ⇒ P → P | _ ⇒ P ]
 927   | RTS ⇒ match op2 with [ RTS ⇒ P → P | _ ⇒ P ]
 928   | SBC ⇒ match op2 with [ SBC ⇒ P → P | _ ⇒ P ]
 929   | SEC ⇒ match op2 with [ SEC ⇒ P → P | _ ⇒ P ]
 930   | SEI ⇒ match op2 with [ SEI ⇒ P → P | _ ⇒ P ]
 931   | SHA ⇒ match op2 with [ SHA ⇒ P → P | _ ⇒ P ]
 932   | SLA ⇒ match op2 with [ SLA ⇒ P → P | _ ⇒ P ]
 933   | STA ⇒ match op2 with [ STA ⇒ P → P | _ ⇒ P ]
 934   | STHX ⇒ match op2 with [ STHX ⇒ P → P | _ ⇒ P ]
 935   | STOP ⇒ match op2 with [ STOP ⇒ P → P | _ ⇒ P ]
 936   | STX ⇒ match op2 with [ STX ⇒ P → P | _ ⇒ P ]
 937   | SUB ⇒ match op2 with [ SUB ⇒ P → P | _ ⇒ P ]
 938   | SWI ⇒ match op2 with [ SWI ⇒ P → P | _ ⇒ P ]
 939   | TAP ⇒ match op2 with [ TAP ⇒ P → P | _ ⇒ P ]
 940   | TAX ⇒ match op2 with [ TAX ⇒ P → P | _ ⇒ P ]
 941   | TPA ⇒ match op2 with [ TPA ⇒ P → P | _ ⇒ P ]
 942   | TST ⇒ match op2 with [ TST ⇒ P → P | _ ⇒ P ]
 943   | TSX ⇒ match op2 with [ TSX ⇒ P → P | _ ⇒ P ]
 944   | TXA ⇒ match op2 with [ TXA ⇒ P → P | _ ⇒ P ]
 945   | TXS ⇒ match op2 with [ TXS ⇒ P → P | _ ⇒ P ]
 946   | WAIT ⇒ match op2 with [ WAIT ⇒ P → P | _ ⇒ P ]
 947   ].
 948
 949 ndefinition opcode_destruct : opcode_destruct_aux.
 950  #op1; ncases op1;
 951  ##[ ##1: napply opcode_destruct1 ##| ##2: napply opcode_destruct2 ##| ##3: napply opcode_destruct3 ##| ##4: napply opcode_destruct4
 952  ##| ##5: napply opcode_destruct5 ##| ##6: napply opcode_destruct6 ##| ##7: napply opcode_destruct7 ##| ##8: napply opcode_destruct8
 953  ##| ##9: napply opcode_destruct9 ##| ##10: napply opcode_destruct10 ##| ##11: napply opcode_destruct11 ##| ##12: napply opcode_destruct12
 954  ##| ##13: napply opcode_destruct13 ##| ##14: napply opcode_destruct14 ##| ##15: napply opcode_destruct15 ##| ##16: napply opcode_destruct16
 955  ##| ##17: napply opcode_destruct17 ##| ##18: napply opcode_destruct18 ##| ##19: napply opcode_destruct19 ##| ##20: napply opcode_destruct20
 956  ##| ##21: napply opcode_destruct21 ##| ##22: napply opcode_destruct22 ##| ##23: napply opcode_destruct23 ##| ##24: napply opcode_destruct24
 957  ##| ##25: napply opcode_destruct25 ##| ##26: napply opcode_destruct26 ##| ##27: napply opcode_destruct27 ##| ##28: napply opcode_destruct28
 958  ##| ##29: napply opcode_destruct29 ##| ##30: napply opcode_destruct30 ##| ##31: napply opcode_destruct31 ##| ##32: napply opcode_destruct32
 959  ##| ##33: napply opcode_destruct33 ##| ##34: napply opcode_destruct34 ##| ##35: napply opcode_destruct35 ##| ##36: napply opcode_destruct36
 960  ##| ##37: napply opcode_destruct37 ##| ##38: napply opcode_destruct38 ##| ##39: napply opcode_destruct39 ##| ##40: napply opcode_destruct40
 961  ##| ##41: napply opcode_destruct41 ##| ##42: napply opcode_destruct42 ##| ##43: napply opcode_destruct43 ##| ##44: napply opcode_destruct44
 962  ##| ##45: napply opcode_destruct45 ##| ##46: napply opcode_destruct46 ##| ##47: napply opcode_destruct47 ##| ##48: napply opcode_destruct48
 963  ##| ##49: napply opcode_destruct49 ##| ##50: napply opcode_destruct50 ##| ##51: napply opcode_destruct51 ##| ##52: napply opcode_destruct52
 964  ##| ##53: napply opcode_destruct53 ##| ##54: napply opcode_destruct54 ##| ##55: napply opcode_destruct55 ##| ##56: napply opcode_destruct56
 965  ##| ##57: napply opcode_destruct57 ##| ##58: napply opcode_destruct58 ##| ##59: napply opcode_destruct59 ##| ##60: napply opcode_destruct60
 966  ##| ##61: napply opcode_destruct61 ##| ##62: napply opcode_destruct62 ##| ##63: napply opcode_destruct63 ##| ##64: napply opcode_destruct64
 967  ##| ##65: napply opcode_destruct65 ##| ##66: napply opcode_destruct66 ##| ##67: napply opcode_destruct67 ##| ##68: napply opcode_destruct68
 968  ##| ##69: napply opcode_destruct69 ##| ##70: napply opcode_destruct70 ##| ##71: napply opcode_destruct71 ##| ##72: napply opcode_destruct72
 969  ##| ##73: napply opcode_destruct73 ##| ##74: napply opcode_destruct74 ##| ##75: napply opcode_destruct75 ##| ##76: napply opcode_destruct76
 970  ##| ##77: napply opcode_destruct77 ##| ##78: napply opcode_destruct78 ##| ##79: napply opcode_destruct79 ##| ##80: napply opcode_destruct80
 971  ##| ##81: napply opcode_destruct81 ##| ##82: napply opcode_destruct82 ##| ##83: napply opcode_destruct83 ##| ##84: napply opcode_destruct84
 972  ##| ##85: napply opcode_destruct85 ##| ##86: napply opcode_destruct86 ##| ##87: napply opcode_destruct87 ##| ##88: napply opcode_destruct88
 973  ##| ##89: napply opcode_destruct89 ##| ##90: napply opcode_destruct90 ##| ##91: napply opcode_destruct91 ##]
 974 nqed.