helm/software/matita/contribs/ng_assembly/freescale/opcode_base_lemmas_instrmode1.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: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
  19 (*   Ultima modifica: 05/08/2009                                          *)
  20 (*                                                                        *)
  21 (* ********************************************************************** *)
  22
  23 include "num/oct_lemmas.ma".
  24 include "num/bitrigesim_lemmas.ma".
  25 include "num/exadecim_lemmas.ma".
  26 include "freescale/opcode_base.ma".
  27
  28 (* ********************************************** *)
  29 (* MATTONI BASE PER DEFINIRE LE TABELLE DELLE MCU *)
  30 (* ********************************************** *)
  31
  32 ndefinition instr_mode_destruct1 :
  33  Πi2.ΠP:Prop.MODE_INH = i2 → match i2 with [ MODE_INH ⇒ P → P | _ ⇒ P ].
  34  #i2; #P;
  35  ncases i2;
  36  nnormalize;
  37  ##[ ##1: #H; napply (λx:P.x)
  38  ##| ##2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H;
  39      napply False_ind;
  40      nchange with (match MODE_INH with [ MODE_INH ⇒ False | _ ⇒ True ]);
  41      nrewrite > H; nnormalize; napply I
  42  ##| ##31,32,33,34: #n; #H;
  43      napply False_ind;
  44      nchange with (match MODE_INH with [ MODE_INH ⇒ False | _ ⇒ True ]);
  45      nrewrite > H; nnormalize; napply I
  46  ##]
  47 nqed.
  48
  49 ndefinition instr_mode_destruct2 :
  50  Πi2.ΠP:Prop.MODE_INHA = i2 → match i2 with [ MODE_INHA ⇒ P → P | _ ⇒ P ].
  51  #i2; #P;
  52  ncases i2;
  53  nnormalize;
  54  ##[ ##2: #H; napply (λx:P.x)
  55  ##| ##1,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H;
  56      napply False_ind;
  57      nchange with (match MODE_INHA with [ MODE_INHA ⇒ False | _ ⇒ True ]);
  58      nrewrite > H; nnormalize; napply I
  59  ##| ##31,32,33,34: #n; #H;
  60      napply False_ind;
  61      nchange with (match MODE_INHA with [ MODE_INHA ⇒ False | _ ⇒ True ]);
  62      nrewrite > H; nnormalize; napply I
  63  ##]
  64 nqed.
  65
  66 ndefinition instr_mode_destruct3 :
  67  Πi2.ΠP:Prop.MODE_INHX = i2 → match i2 with [ MODE_INHX ⇒ P → P | _ ⇒ P ].
  68  #i2; #P;
  69  ncases i2;
  70  nnormalize;
  71  ##[ ##3: #H; napply (λx:P.x)
  72  ##| ##1,2,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H;
  73      napply False_ind;
  74      nchange with (match MODE_INHX with [ MODE_INHX ⇒ False | _ ⇒ True ]);
  75      nrewrite > H; nnormalize; napply I
  76  ##| ##31,32,33,34: #n; #H;
  77      napply False_ind;
  78      nchange with (match MODE_INHX with [ MODE_INHX ⇒ False | _ ⇒ True ]);
  79      nrewrite > H; nnormalize; napply I
  80  ##]
  81 nqed.
  82
  83 ndefinition instr_mode_destruct4 :
  84  Πi2.ΠP:Prop.MODE_INHH = i2 → match i2 with [ MODE_INHH ⇒ P → P | _ ⇒ P ].
  85  #i2; #P;
  86  ncases i2;
  87  nnormalize;
  88  ##[ ##4: #H; napply (λx:P.x)
  89  ##| ##1,2,3,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H;
  90      napply False_ind;
  91      nchange with (match MODE_INHH with [ MODE_INHH ⇒ False | _ ⇒ True ]);
  92      nrewrite > H; nnormalize; napply I
  93  ##| ##31,32,33,34: #n; #H;
  94      napply False_ind;
  95      nchange with (match MODE_INHH with [ MODE_INHH ⇒ False | _ ⇒ True ]);
  96      nrewrite > H; nnormalize; napply I
  97  ##]
  98 nqed.
  99
 100 ndefinition instr_mode_destruct5 :
 101  Πi2.ΠP:Prop.MODE_INHX0ADD = i2 → match i2 with [ MODE_INHX0ADD ⇒ P → P | _ ⇒ P ].
 102  #i2; #P;
 103  ncases i2;
 104  nnormalize;
 105  ##[ ##5: #H; napply (λx:P.x)
 106  ##| ##1,2,3,4,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H;
 107      napply False_ind;
 108      nchange with (match MODE_INHX0ADD with [ MODE_INHX0ADD ⇒ False | _ ⇒ True ]);
 109      nrewrite > H; nnormalize; napply I
 110  ##| ##31,32,33,34: #n; #H;
 111      napply False_ind;
 112      nchange with (match MODE_INHX0ADD with [ MODE_INHX0ADD ⇒ False | _ ⇒ True ]);
 113      nrewrite > H; nnormalize; napply I
 114  ##]
 115 nqed.
 116
 117 ndefinition instr_mode_destruct6 :
 118  Πi2.ΠP:Prop.MODE_INHX1ADD = i2 → match i2 with [ MODE_INHX1ADD ⇒ P → P | _ ⇒ P ].
 119  #i2; #P;
 120  ncases i2;
 121  nnormalize;
 122  ##[ ##6: #H; napply (λx:P.x)
 123  ##| ##1,2,3,4,5,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H;
 124      napply False_ind;
 125      nchange with (match MODE_INHX1ADD with [ MODE_INHX1ADD ⇒ False | _ ⇒ True ]);
 126      nrewrite > H; nnormalize; napply I
 127  ##| ##31,32,33,34: #n; #H;
 128      napply False_ind;
 129      nchange with (match MODE_INHX1ADD with [ MODE_INHX1ADD ⇒ False | _ ⇒ True ]);
 130      nrewrite > H; nnormalize; napply I
 131  ##]
 132 nqed.
 133
 134 ndefinition instr_mode_destruct7 :
 135  Πi2.ΠP:Prop.MODE_INHX2ADD = i2 → match i2 with [ MODE_INHX2ADD ⇒ P → P | _ ⇒ P ].
 136  #i2; #P;
 137  ncases i2;
 138  nnormalize;
 139  ##[ ##7: #H; napply (λx:P.x)
 140  ##| ##1,2,3,4,5,6,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H;
 141      napply False_ind;
 142      nchange with (match MODE_INHX2ADD with [ MODE_INHX2ADD ⇒ False | _ ⇒ True ]);
 143      nrewrite > H; nnormalize; napply I
 144  ##| ##31,32,33,34: #n; #H;
 145      napply False_ind;
 146      nchange with (match MODE_INHX2ADD with [ MODE_INHX2ADD ⇒ False | _ ⇒ True ]);
 147      nrewrite > H; nnormalize; napply I
 148  ##]
 149 nqed.
 150
 151 ndefinition instr_mode_destruct8 :
 152  Πi2.ΠP:Prop.MODE_IMM1 = i2 → match i2 with [ MODE_IMM1 ⇒ P → P | _ ⇒ P ].
 153  #i2; #P;
 154  ncases i2;
 155  nnormalize;
 156  ##[ ##8: #H; napply (λx:P.x)
 157  ##| ##1,2,3,4,5,6,7,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H;
 158      napply False_ind;
 159      nchange with (match MODE_IMM1 with [ MODE_IMM1 ⇒ False | _ ⇒ True ]);
 160      nrewrite > H; nnormalize; napply I
 161  ##| ##31,32,33,34: #n; #H;
 162      napply False_ind;
 163      nchange with (match MODE_IMM1 with [ MODE_IMM1 ⇒ False | _ ⇒ True ]);
 164      nrewrite > H; nnormalize; napply I
 165  ##]
 166 nqed.
 167
 168 ndefinition instr_mode_destruct9 :
 169  Πi2.ΠP:Prop.MODE_IMM1EXT = i2 → match i2 with [ MODE_IMM1EXT ⇒ P → P | _ ⇒ P ].
 170  #i2; #P;
 171  ncases i2;
 172  nnormalize;
 173  ##[ ##9: #H; napply (λx:P.x)
 174  ##| ##1,2,3,4,5,6,7,8,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H;
 175      napply False_ind;
 176      nchange with (match MODE_IMM1EXT with [ MODE_IMM1EXT ⇒ False | _ ⇒ True ]);
 177      nrewrite > H; nnormalize; napply I
 178  ##| ##31,32,33,34: #n; #H;
 179      napply False_ind;
 180      nchange with (match MODE_IMM1EXT with [ MODE_IMM1EXT ⇒ False | _ ⇒ True ]);
 181      nrewrite > H; nnormalize; napply I
 182  ##]
 183 nqed.
 184
 185 ndefinition instr_mode_destruct10 :
 186  Πi2.ΠP:Prop.MODE_IMM2 = i2 → match i2 with [ MODE_IMM2 ⇒ P → P | _ ⇒ P ].
 187  #i2; #P;
 188  ncases i2;
 189  nnormalize;
 190  ##[ ##10: #H; napply (λx:P.x)
 191  ##| ##1,2,3,4,5,6,7,8,9,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H;
 192      napply False_ind;
 193      nchange with (match MODE_IMM2 with [ MODE_IMM2 ⇒ False | _ ⇒ True ]);
 194      nrewrite > H; nnormalize; napply I
 195  ##| ##31,32,33,34: #n; #H;
 196      napply False_ind;
 197      nchange with (match MODE_IMM2 with [ MODE_IMM2 ⇒ False | _ ⇒ True ]);
 198      nrewrite > H; nnormalize; napply I
 199  ##]
 200 nqed.
 201
 202 ndefinition instr_mode_destruct11 :
 203  Πi2.ΠP:Prop.MODE_DIR1 = i2 → match i2 with [ MODE_DIR1 ⇒ P → P | _ ⇒ P ].
 204  #i2; #P;
 205  ncases i2;
 206  nnormalize;
 207  ##[ ##11: #H; napply (λx:P.x)
 208  ##| ##1,2,3,4,5,6,7,8,9,10,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H;
 209      napply False_ind;
 210      nchange with (match MODE_DIR1 with [ MODE_DIR1 ⇒ False | _ ⇒ True ]);
 211      nrewrite > H; nnormalize; napply I
 212  ##| ##31,32,33,34: #n; #H;
 213      napply False_ind;
 214      nchange with (match MODE_DIR1 with [ MODE_DIR1 ⇒ False | _ ⇒ True ]);
 215      nrewrite > H; nnormalize; napply I
 216  ##]
 217 nqed.
 218
 219 ndefinition instr_mode_destruct12 :
 220  Πi2.ΠP:Prop.MODE_DIR2 = i2 → match i2 with [ MODE_DIR2 ⇒ P → P | _ ⇒ P ].
 221  #i2; #P;
 222  ncases i2;
 223  nnormalize;
 224  ##[ ##12: #H; napply (λx:P.x)
 225  ##| ##1,2,3,4,5,6,7,8,9,10,11,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H;
 226      napply False_ind;
 227      nchange with (match MODE_DIR2 with [ MODE_DIR2 ⇒ False | _ ⇒ True ]);
 228      nrewrite > H; nnormalize; napply I
 229  ##| ##31,32,33,34: #n; #H;
 230      napply False_ind;
 231      nchange with (match MODE_DIR2 with [ MODE_DIR2 ⇒ False | _ ⇒ True ]);
 232      nrewrite > H; nnormalize; napply I
 233  ##]
 234 nqed.
 235
 236 ndefinition instr_mode_destruct13 :
 237  Πi2.ΠP:Prop.MODE_IX0 = i2 → match i2 with [ MODE_IX0 ⇒ P → P | _ ⇒ P ].
 238  #i2; #P;
 239  ncases i2;
 240  nnormalize;
 241  ##[ ##13: #H; napply (λx:P.x)
 242  ##| ##1,2,3,4,5,6,7,8,9,10,11,12,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H;
 243      napply False_ind;
 244      nchange with (match MODE_IX0 with [ MODE_IX0 ⇒ False | _ ⇒ True ]);
 245      nrewrite > H; nnormalize; napply I
 246  ##| ##31,32,33,34: #n; #H;
 247      napply False_ind;
 248      nchange with (match MODE_IX0 with [ MODE_IX0 ⇒ False | _ ⇒ True ]);
 249      nrewrite > H; nnormalize; napply I
 250  ##]
 251 nqed.
 252
 253 ndefinition instr_mode_destruct14 :
 254  Πi2.ΠP:Prop.MODE_IX1 = i2 → match i2 with [ MODE_IX1 ⇒ P → P | _ ⇒ P ].
 255  #i2; #P;
 256  ncases i2;
 257  nnormalize;
 258  ##[ ##14: #H; napply (λx:P.x)
 259  ##| ##1,2,3,4,5,6,7,8,9,10,11,12,13,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H;
 260      napply False_ind;
 261      nchange with (match MODE_IX1 with [ MODE_IX1 ⇒ False | _ ⇒ True ]);
 262      nrewrite > H; nnormalize; napply I
 263  ##| ##31,32,33,34: #n; #H;
 264      napply False_ind;
 265      nchange with (match MODE_IX1 with [ MODE_IX1 ⇒ False | _ ⇒ True ]);
 266      nrewrite > H; nnormalize; napply I
 267  ##]
 268 nqed.
 269
 270 ndefinition instr_mode_destruct15 :
 271  Πi2.ΠP:Prop.MODE_IX2 = i2 → match i2 with [ MODE_IX2 ⇒ P → P | _ ⇒ P ].
 272  #i2; #P;
 273  ncases i2;
 274  nnormalize;
 275  ##[ ##15: #H; napply (λx:P.x)
 276  ##| ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H;
 277      napply False_ind;
 278      nchange with (match MODE_IX2 with [ MODE_IX2 ⇒ False | _ ⇒ True ]);
 279      nrewrite > H; nnormalize; napply I
 280  ##| ##31,32,33,34: #n; #H;
 281      napply False_ind;
 282      nchange with (match MODE_IX2 with [ MODE_IX2 ⇒ False | _ ⇒ True ]);
 283      nrewrite > H; nnormalize; napply I
 284  ##]
 285 nqed.
 286
 287 ndefinition instr_mode_destruct16 :
 288  Πi2.ΠP:Prop.MODE_SP1 = i2 → match i2 with [ MODE_SP1 ⇒ P → P | _ ⇒ P ].
 289  #i2; #P;
 290  ncases i2;
 291  nnormalize;
 292  ##[ ##16: #H; napply (λx:P.x)
 293  ##| ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H;
 294      napply False_ind;
 295      nchange with (match MODE_SP1 with [ MODE_SP1 ⇒ False | _ ⇒ True ]);
 296      nrewrite > H; nnormalize; napply I
 297  ##| ##31,32,33,34: #n; #H;
 298      napply False_ind;
 299      nchange with (match MODE_SP1 with [ MODE_SP1 ⇒ False | _ ⇒ True ]);
 300      nrewrite > H; nnormalize; napply I
 301  ##]
 302 nqed.
 303
 304 ndefinition instr_mode_destruct17 :
 305  Πi2.ΠP:Prop.MODE_SP2 = i2 → match i2 with [ MODE_SP2 ⇒ P → P | _ ⇒ P ].
 306  #i2; #P;
 307  ncases i2;
 308  nnormalize;
 309  ##[ ##17: #H; napply (λx:P.x)
 310  ##| ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,18,19,20,21,22,23,24,25,26,27,28,29,30: #H;
 311      napply False_ind;
 312      nchange with (match MODE_SP2 with [ MODE_SP2 ⇒ False | _ ⇒ True ]);
 313      nrewrite > H; nnormalize; napply I
 314  ##| ##31,32,33,34: #n; #H;
 315      napply False_ind;
 316      nchange with (match MODE_SP2 with [ MODE_SP2 ⇒ False | _ ⇒ True ]);
 317      nrewrite > H; nnormalize; napply I
 318  ##]
 319 nqed.
 320
 321 ndefinition instr_mode_destruct18 :
 322  Πi2.ΠP:Prop.MODE_DIR1_to_DIR1 = i2 → match i2 with [ MODE_DIR1_to_DIR1 ⇒ P → P | _ ⇒ P ].
 323  #i2; #P;
 324  ncases i2;
 325  nnormalize;
 326  ##[ ##18: #H; napply (λx:P.x)
 327  ##| ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,19,20,21,22,23,24,25,26,27,28,29,30: #H;
 328      napply False_ind;
 329      nchange with (match MODE_DIR1_to_DIR1 with [ MODE_DIR1_to_DIR1 ⇒ False | _ ⇒ True ]);
 330      nrewrite > H; nnormalize; napply I
 331  ##| ##31,32,33,34: #n; #H;
 332      napply False_ind;
 333      nchange with (match MODE_DIR1_to_DIR1 with [ MODE_DIR1_to_DIR1 ⇒ False | _ ⇒ True ]);
 334      nrewrite > H; nnormalize; napply I
 335  ##]
 336 nqed.
 337
 338 ndefinition instr_mode_destruct19 :
 339  Πi2.ΠP:Prop.MODE_IMM1_to_DIR1 = i2 → match i2 with [ MODE_IMM1_to_DIR1 ⇒ P → P | _ ⇒ P ].
 340  #i2; #P;
 341  ncases i2;
 342  nnormalize;
 343  ##[ ##19: #H; napply (λx:P.x)
 344  ##| ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,20,21,22,23,24,25,26,27,28,29,30: #H;
 345      napply False_ind;
 346      nchange with (match MODE_IMM1_to_DIR1 with [ MODE_IMM1_to_DIR1 ⇒ False | _ ⇒ True ]);
 347      nrewrite > H; nnormalize; napply I
 348  ##| ##31,32,33,34: #n; #H;
 349      napply False_ind;
 350      nchange with (match MODE_IMM1_to_DIR1 with [ MODE_IMM1_to_DIR1 ⇒ False | _ ⇒ True ]);
 351      nrewrite > H; nnormalize; napply I
 352  ##]
 353 nqed.
 354
 355 ndefinition instr_mode_destruct20 :
 356  Πi2.ΠP:Prop.MODE_IX0p_to_DIR1 = i2 → match i2 with [ MODE_IX0p_to_DIR1 ⇒ P → P | _ ⇒ P ].
 357  #i2; #P;
 358  ncases i2;
 359  nnormalize;
 360  ##[ ##20: #H; napply (λx:P.x)
 361  ##| ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,21,22,23,24,25,26,27,28,29,30: #H;
 362      napply False_ind;
 363      nchange with (match MODE_IX0p_to_DIR1 with [ MODE_IX0p_to_DIR1 ⇒ False | _ ⇒ True ]);
 364      nrewrite > H; nnormalize; napply I
 365  ##| ##31,32,33,34: #n; #H;
 366      napply False_ind;
 367      nchange with (match MODE_IX0p_to_DIR1 with [ MODE_IX0p_to_DIR1 ⇒ False | _ ⇒ True ]);
 368      nrewrite > H; nnormalize; napply I
 369  ##]
 370 nqed.
 371
 372 ndefinition instr_mode_destruct21 :
 373  Πi2.ΠP:Prop.MODE_DIR1_to_IX0p = i2 → match i2 with [ MODE_DIR1_to_IX0p ⇒ P → P | _ ⇒ P ].
 374  #i2; #P;
 375  ncases i2;
 376  nnormalize;
 377  ##[ ##21: #H; napply (λx:P.x)
 378  ##| ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,22,23,24,25,26,27,28,29,30: #H;
 379      napply False_ind;
 380      nchange with (match MODE_DIR1_to_IX0p with [ MODE_DIR1_to_IX0p ⇒ False | _ ⇒ True ]);
 381      nrewrite > H; nnormalize; napply I
 382  ##| ##31,32,33,34: #n; #H;
 383      napply False_ind;
 384      nchange with (match MODE_DIR1_to_IX0p with [ MODE_DIR1_to_IX0p ⇒ False | _ ⇒ True ]);
 385      nrewrite > H; nnormalize; napply I
 386  ##]
 387 nqed.
 388
 389 ndefinition instr_mode_destruct22 :
 390  Πi2.ΠP:Prop.MODE_INHA_and_IMM1 = i2 → match i2 with [ MODE_INHA_and_IMM1 ⇒ P → P | _ ⇒ P ].
 391  #i2; #P;
 392  ncases i2;
 393  nnormalize;
 394  ##[ ##22: #H; napply (λx:P.x)
 395  ##| ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,23,24,25,26,27,28,29,30: #H;
 396      napply False_ind;
 397      nchange with (match MODE_INHA_and_IMM1 with [ MODE_INHA_and_IMM1 ⇒ False | _ ⇒ True ]);
 398      nrewrite > H; nnormalize; napply I
 399  ##| ##31,32,33,34: #n; #H;
 400      napply False_ind;
 401      nchange with (match MODE_INHA_and_IMM1 with [ MODE_INHA_and_IMM1 ⇒ False | _ ⇒ True ]);
 402      nrewrite > H; nnormalize; napply I
 403  ##]
 404 nqed.
 405
 406 ndefinition instr_mode_destruct23 :
 407  Πi2.ΠP:Prop.MODE_INHX_and_IMM1 = i2 → match i2 with [ MODE_INHX_and_IMM1 ⇒ P → P | _ ⇒ P ].
 408  #i2; #P;
 409  ncases i2;
 410  nnormalize;
 411  ##[ ##23: #H; napply (λx:P.x)
 412  ##| ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,24,25,26,27,28,29,30: #H;
 413      napply False_ind;
 414      nchange with (match MODE_INHX_and_IMM1 with [ MODE_INHX_and_IMM1 ⇒ False | _ ⇒ True ]);
 415      nrewrite > H; nnormalize; napply I
 416  ##| ##31,32,33,34: #n; #H;
 417      napply False_ind;
 418      nchange with (match MODE_INHX_and_IMM1 with [ MODE_INHX_and_IMM1 ⇒ False | _ ⇒ True ]);
 419      nrewrite > H; nnormalize; napply I
 420  ##]
 421 nqed.
 422
 423 ndefinition instr_mode_destruct24 :
 424  Πi2.ΠP:Prop.MODE_IMM1_and_IMM1 = i2 → match i2 with [ MODE_IMM1_and_IMM1 ⇒ P → P | _ ⇒ P ].
 425  #i2; #P;
 426  ncases i2;
 427  nnormalize;
 428  ##[ ##24: #H; napply (λx:P.x)
 429  ##| ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,25,26,27,28,29,30: #H;
 430      napply False_ind;
 431      nchange with (match MODE_IMM1_and_IMM1 with [ MODE_IMM1_and_IMM1 ⇒ False | _ ⇒ True ]);
 432      nrewrite > H; nnormalize; napply I
 433  ##| ##31,32,33,34: #n; #H;
 434      napply False_ind;
 435      nchange with (match MODE_IMM1_and_IMM1 with [ MODE_IMM1_and_IMM1 ⇒ False | _ ⇒ True ]);
 436      nrewrite > H; nnormalize; napply I
 437  ##]
 438 nqed.
 439
 440 ndefinition instr_mode_destruct25 :
 441  Πi2.ΠP:Prop.MODE_DIR1_and_IMM1 = i2 → match i2 with [ MODE_DIR1_and_IMM1 ⇒ P → P | _ ⇒ P ].
 442  #i2; #P;
 443  ncases i2;
 444  nnormalize;
 445  ##[ ##25: #H; napply (λx:P.x)
 446  ##| ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,26,27,28,29,30: #H;
 447      napply False_ind;
 448      nchange with (match MODE_DIR1_and_IMM1 with [ MODE_DIR1_and_IMM1 ⇒ False | _ ⇒ True ]);
 449      nrewrite > H; nnormalize; napply I
 450  ##| ##31,32,33,34: #n; #H;
 451      napply False_ind;
 452      nchange with (match MODE_DIR1_and_IMM1 with [ MODE_DIR1_and_IMM1 ⇒ False | _ ⇒ True ]);
 453      nrewrite > H; nnormalize; napply I
 454  ##]
 455 nqed.
 456
 457 ndefinition instr_mode_destruct26 :
 458  Πi2.ΠP:Prop.MODE_IX0_and_IMM1 = i2 → match i2 with [ MODE_IX0_and_IMM1 ⇒ P → P | _ ⇒ P ].
 459  #i2; #P;
 460  ncases i2;
 461  nnormalize;
 462  ##[ ##26: #H; napply (λx:P.x)
 463  ##| ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,27,28,29,30: #H;
 464      napply False_ind;
 465      nchange with (match MODE_IX0_and_IMM1 with [ MODE_IX0_and_IMM1 ⇒ False | _ ⇒ True ]);
 466      nrewrite > H; nnormalize; napply I
 467  ##| ##31,32,33,34: #n; #H;
 468      napply False_ind;
 469      nchange with (match MODE_IX0_and_IMM1 with [ MODE_IX0_and_IMM1 ⇒ False | _ ⇒ True ]);
 470      nrewrite > H; nnormalize; napply I
 471  ##]
 472 nqed.
 473
 474 ndefinition instr_mode_destruct27 :
 475  Πi2.ΠP:Prop.MODE_IX0p_and_IMM1 = i2 → match i2 with [ MODE_IX0p_and_IMM1 ⇒ P → P | _ ⇒ P ].
 476  #i2; #P;
 477  ncases i2;
 478  nnormalize;
 479  ##[ ##27: #H; napply (λx:P.x)
 480  ##| ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,28,29,30: #H;
 481      napply False_ind;
 482      nchange with (match MODE_IX0p_and_IMM1 with [ MODE_IX0p_and_IMM1 ⇒ False | _ ⇒ True ]);
 483      nrewrite > H; nnormalize; napply I
 484  ##| ##31,32,33,34: #n; #H;
 485      napply False_ind;
 486      nchange with (match MODE_IX0p_and_IMM1 with [ MODE_IX0p_and_IMM1 ⇒ False | _ ⇒ True ]);
 487      nrewrite > H; nnormalize; napply I
 488  ##]
 489 nqed.
 490
 491 ndefinition instr_mode_destruct28 :
 492  Πi2.ΠP:Prop.MODE_IX1_and_IMM1 = i2 → match i2 with [ MODE_IX1_and_IMM1 ⇒ P → P | _ ⇒ P ].
 493  #i2; #P;
 494  ncases i2;
 495  nnormalize;
 496  ##[ ##28: #H; napply (λx:P.x)
 497  ##| ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,29,30: #H;
 498      napply False_ind;
 499      nchange with (match MODE_IX1_and_IMM1 with [ MODE_IX1_and_IMM1 ⇒ False | _ ⇒ True ]);
 500      nrewrite > H; nnormalize; napply I
 501  ##| ##31,32,33,34: #n; #H;
 502      napply False_ind;
 503      nchange with (match MODE_IX1_and_IMM1 with [ MODE_IX1_and_IMM1 ⇒ False | _ ⇒ True ]);
 504      nrewrite > H; nnormalize; napply I
 505  ##]
 506 nqed.
 507
 508 ndefinition instr_mode_destruct29 :
 509  Πi2.ΠP:Prop.MODE_IX1p_and_IMM1 = i2 → match i2 with [ MODE_IX1p_and_IMM1 ⇒ P → P | _ ⇒ P ].
 510  #i2; #P;
 511  ncases i2;
 512  nnormalize;
 513  ##[ ##29: #H; napply (λx:P.x)
 514  ##| ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,30: #H;
 515      napply False_ind;
 516      nchange with (match MODE_IX1p_and_IMM1 with [ MODE_IX1p_and_IMM1 ⇒ False | _ ⇒ True ]);
 517      nrewrite > H; nnormalize; napply I
 518  ##| ##31,32,33,34: #n; #H;
 519      napply False_ind;
 520      nchange with (match MODE_IX1p_and_IMM1 with [ MODE_IX1p_and_IMM1 ⇒ False | _ ⇒ True ]);
 521      nrewrite > H; nnormalize; napply I
 522  ##]
 523 nqed.
 524
 525 ndefinition instr_mode_destruct30 :
 526  Πi2.ΠP:Prop.MODE_SP1_and_IMM1 = i2 → match i2 with [ MODE_SP1_and_IMM1 ⇒ P → P | _ ⇒ P ].
 527  #i2; #P;
 528  ncases i2;
 529  nnormalize;
 530  ##[ ##30: #H; napply (λx:P.x)
 531  ##| ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29: #H;
 532      napply False_ind;
 533      nchange with (match MODE_SP1_and_IMM1 with [ MODE_SP1_and_IMM1 ⇒ False | _ ⇒ True ]);
 534      nrewrite > H; nnormalize; napply I
 535  ##| ##31,32,33,34: #n; #H;
 536      napply False_ind;
 537      nchange with (match MODE_SP1_and_IMM1 with [ MODE_SP1_and_IMM1 ⇒ False | _ ⇒ True ]);
 538      nrewrite > H; nnormalize; napply I
 539  ##]
 540 nqed.
 541
 542 nlemma instr_mode_destruct_MODE_DIRn : ∀n1,n2.MODE_DIRn n1 = MODE_DIRn n2 → n1 = n2.
 543  #n1; #n2; #H;
 544  nchange with (match MODE_DIRn n2 with [ MODE_DIRn a ⇒ n1 = a | _ ⇒ False ]);
 545  nrewrite < H;
 546  nnormalize;
 547  napply refl_eq.
 548 nqed.
 549
 550 ndefinition instr_mode_destruct31 :
 551  Πn1,i2.ΠP:Prop.MODE_DIRn n1 = i2 →
 552   match i2 with
 553    [ MODE_DIRn n2 ⇒ match n1 with
 554     [ o0 ⇒ match n2 with [ o0 ⇒ P → P | _ ⇒ P ] | o1 ⇒ match n2 with [ o1 ⇒ P → P | _ ⇒ P ]
 555     | o2 ⇒ match n2 with [ o2 ⇒ P → P | _ ⇒ P ] | o3 ⇒ match n2 with [ o3 ⇒ P → P | _ ⇒ P ]
 556     | o4 ⇒ match n2 with [ o4 ⇒ P → P | _ ⇒ P ] | o5 ⇒ match n2 with [ o5 ⇒ P → P | _ ⇒ P ]
 557     | o6 ⇒ match n2 with [ o6 ⇒ P → P | _ ⇒ P ] | o7 ⇒ match n2 with [ o7 ⇒ P → P | _ ⇒ P ]]
 558    | _ ⇒ P ].
 559  #n1; #i2; #P;
 560  ncases i2;
 561  nnormalize;
 562  ##[ ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H;
 563      napply False_ind;
 564      nchange with (match MODE_DIRn n1 with [ MODE_DIRn a ⇒ False | _ ⇒ True ]);
 565      nrewrite > H; nnormalize; napply I
 566  ##| ##32,33,34: #n; #H;
 567      napply False_ind;
 568      nchange with (match MODE_DIRn n1 with [ MODE_DIRn n1 ⇒ False | _ ⇒ True ]);
 569      nrewrite > H; nnormalize; napply I
 570  ##| ##31: #n2;
 571      ncases n1;
 572      ncases n2;
 573      nnormalize;
 574      ##[ ##1,10,19,28,37,46,55,64: #H; napply (λx:P.x)
 575      ##| ##*: #H; napply (oct_destruct … (instr_mode_destruct_MODE_DIRn … H))
 576      ##]
 577 nqed.
 578
 579 nlemma instr_mode_destruct_MODE_DIRn_and_IMM1 : ∀n1,n2.MODE_DIRn_and_IMM1 n1 = MODE_DIRn_and_IMM1 n2 → n1 = n2.
 580  #n1; #n2; #H;
 581  nchange with (match MODE_DIRn_and_IMM1 n2 with [ MODE_DIRn_and_IMM1 a ⇒ n1 = a | _ ⇒ False ]);
 582  nrewrite < H;
 583  nnormalize;
 584  napply refl_eq.
 585 nqed.
 586
 587 ndefinition instr_mode_destruct32 :
 588  Πn1,i2.ΠP:Prop.MODE_DIRn_and_IMM1 n1 = i2 →
 589   match i2 with
 590    [ MODE_DIRn_and_IMM1 n2 ⇒ match n1 with
 591     [ o0 ⇒ match n2 with [ o0 ⇒ P → P | _ ⇒ P ] | o1 ⇒ match n2 with [ o1 ⇒ P → P | _ ⇒ P ]
 592     | o2 ⇒ match n2 with [ o2 ⇒ P → P | _ ⇒ P ] | o3 ⇒ match n2 with [ o3 ⇒ P → P | _ ⇒ P ]
 593     | o4 ⇒ match n2 with [ o4 ⇒ P → P | _ ⇒ P ] | o5 ⇒ match n2 with [ o5 ⇒ P → P | _ ⇒ P ]
 594     | o6 ⇒ match n2 with [ o6 ⇒ P → P | _ ⇒ P ] | o7 ⇒ match n2 with [ o7 ⇒ P → P | _ ⇒ P ]]
 595    | _ ⇒ P ].
 596  #n1; #i2; #P;
 597  ncases i2;
 598  nnormalize;
 599  ##[ ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H;
 600      napply False_ind;
 601      nchange with (match MODE_DIRn_and_IMM1 n1 with [ MODE_DIRn_and_IMM1 a ⇒ False | _ ⇒ True ]);
 602      nrewrite > H; nnormalize; napply I
 603  ##| ##31,33,34: #n; #H;
 604      napply False_ind;
 605      nchange with (match MODE_DIRn_and_IMM1 n1 with [ MODE_DIRn_and_IMM1 n1 ⇒ False | _ ⇒ True ]);
 606      nrewrite > H; nnormalize; napply I
 607  ##| ##32: #n2;
 608      ncases n1;
 609      ncases n2;
 610      nnormalize;
 611      ##[ ##1,10,19,28,37,46,55,64: #H; napply (λx:P.x)
 612      ##| ##*: #H; napply (oct_destruct … (instr_mode_destruct_MODE_DIRn_and_IMM1 … H))
 613      ##]
 614 nqed.
 615
 616 nlemma instr_mode_destruct_MODE_TNY : ∀n1,n2.MODE_TNY n1 = MODE_TNY n2 → n1 = n2.
 617  #n1; #n2; #H;
 618  nchange with (match MODE_TNY n2 with [ MODE_TNY a ⇒ n1 = a | _ ⇒ False ]);
 619  nrewrite < H;
 620  nnormalize;
 621  napply refl_eq.
 622 nqed.
 623
 624 ndefinition instr_mode_destruct33 :
 625  Πn1,i2.ΠP:Prop.MODE_TNY n1 = i2 →
 626   match i2 with
 627    [ MODE_TNY n2 ⇒ match n1 with
 628     [ x0 ⇒ match n2 with [ x0 ⇒ P → P | _ ⇒ P ] | x1 ⇒ match n2 with [ x1 ⇒ P → P | _ ⇒ P ]
 629     | x2 ⇒ match n2 with [ x2 ⇒ P → P | _ ⇒ P ] | x3 ⇒ match n2 with [ x3 ⇒ P → P | _ ⇒ P ]
 630     | x4 ⇒ match n2 with [ x4 ⇒ P → P | _ ⇒ P ] | x5 ⇒ match n2 with [ x5 ⇒ P → P | _ ⇒ P ]
 631     | x6 ⇒ match n2 with [ x6 ⇒ P → P | _ ⇒ P ] | x7 ⇒ match n2 with [ x7 ⇒ P → P | _ ⇒ P ]
 632     | x8 ⇒ match n2 with [ x8 ⇒ P → P | _ ⇒ P ] | x9 ⇒ match n2 with [ x9 ⇒ P → P | _ ⇒ P ]
 633     | xA ⇒ match n2 with [ xA ⇒ P → P | _ ⇒ P ] | xB ⇒ match n2 with [ xB ⇒ P → P | _ ⇒ P ]
 634     | xC ⇒ match n2 with [ xC ⇒ P → P | _ ⇒ P ] | xD ⇒ match n2 with [ xD ⇒ P → P | _ ⇒ P ]
 635     | xE ⇒ match n2 with [ xE ⇒ P → P | _ ⇒ P ] | xF ⇒ match n2 with [ xF ⇒ P → P | _ ⇒ P ]]
 636    | _ ⇒ P ].
 637  #n1; #i2; #P;
 638  ncases i2;
 639  nnormalize;
 640  ##[ ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H;
 641      napply False_ind;
 642      nchange with (match MODE_TNY n1 with [ MODE_TNY a ⇒ False | _ ⇒ True ]);
 643      nrewrite > H; nnormalize; napply I
 644  ##| ##31,32,34: #n; #H;
 645      napply False_ind;
 646      nchange with (match MODE_TNY n1 with [ MODE_TNY n1 ⇒ False | _ ⇒ True ]);
 647      nrewrite > H; nnormalize; napply I
 648  ##| ##33: #n2;
 649      ncases n1;
 650      ncases n2;
 651      nnormalize;
 652      ##[ ##1,18,35,52,69,86,103,120,137,154,171,188,205,222,239,256: #H; napply (λx:P.x)
 653      ##| ##*: #H; napply (exadecim_destruct … (instr_mode_destruct_MODE_TNY … H))
 654      ##]
 655 nqed.
 656
 657 nlemma instr_mode_destruct_MODE_SRT : ∀n1,n2.MODE_SRT n1 = MODE_SRT n2 → n1 = n2.
 658  #n1; #n2; #H;
 659  nchange with (match MODE_SRT n2 with [ MODE_SRT a ⇒ n1 = a | _ ⇒ False ]);
 660  nrewrite < H;
 661  nnormalize;
 662  napply refl_eq.
 663 nqed.
 664
 665 ndefinition instr_mode_destruct34 :
 666  Πn1,i2.ΠP:Prop.MODE_SRT n1 = i2 →
 667   match i2 with
 668    [ MODE_SRT n2 ⇒ match n1 with
 669     [ t00 ⇒ match n2 with [ t00 ⇒ P → P | _ ⇒ P ] | t01 ⇒ match n2 with [ t01 ⇒ P → P | _ ⇒ P ]
 670     | t02 ⇒ match n2 with [ t02 ⇒ P → P | _ ⇒ P ] | t03 ⇒ match n2 with [ t03 ⇒ P → P | _ ⇒ P ]
 671     | t04 ⇒ match n2 with [ t04 ⇒ P → P | _ ⇒ P ] | t05 ⇒ match n2 with [ t05 ⇒ P → P | _ ⇒ P ]
 672     | t06 ⇒ match n2 with [ t06 ⇒ P → P | _ ⇒ P ] | t07 ⇒ match n2 with [ t07 ⇒ P → P | _ ⇒ P ]
 673     | t08 ⇒ match n2 with [ t08 ⇒ P → P | _ ⇒ P ] | t09 ⇒ match n2 with [ t09 ⇒ P → P | _ ⇒ P ]
 674     | t0A ⇒ match n2 with [ t0A ⇒ P → P | _ ⇒ P ] | t0B ⇒ match n2 with [ t0B ⇒ P → P | _ ⇒ P ]
 675     | t0C ⇒ match n2 with [ t0C ⇒ P → P | _ ⇒ P ] | t0D ⇒ match n2 with [ t0D ⇒ P → P | _ ⇒ P ]
 676     | t0E ⇒ match n2 with [ t0E ⇒ P → P | _ ⇒ P ] | t0F ⇒ match n2 with [ t0F ⇒ P → P | _ ⇒ P ]
 677     | t10 ⇒ match n2 with [ t10 ⇒ P → P | _ ⇒ P ] | t11 ⇒ match n2 with [ t11 ⇒ P → P | _ ⇒ P ]
 678     | t12 ⇒ match n2 with [ t12 ⇒ P → P | _ ⇒ P ] | t13 ⇒ match n2 with [ t13 ⇒ P → P | _ ⇒ P ]
 679     | t14 ⇒ match n2 with [ t14 ⇒ P → P | _ ⇒ P ] | t15 ⇒ match n2 with [ t15 ⇒ P → P | _ ⇒ P ]
 680     | t16 ⇒ match n2 with [ t16 ⇒ P → P | _ ⇒ P ] | t17 ⇒ match n2 with [ t17 ⇒ P → P | _ ⇒ P ]
 681     | t18 ⇒ match n2 with [ t18 ⇒ P → P | _ ⇒ P ] | t19 ⇒ match n2 with [ t19 ⇒ P → P | _ ⇒ P ]
 682     | t1A ⇒ match n2 with [ t1A ⇒ P → P | _ ⇒ P ] | t1B ⇒ match n2 with [ t1B ⇒ P → P | _ ⇒ P ]
 683     | t1C ⇒ match n2 with [ t1C ⇒ P → P | _ ⇒ P ] | t1D ⇒ match n2 with [ t1D ⇒ P → P | _ ⇒ P ]
 684     | t1E ⇒ match n2 with [ t1E ⇒ P → P | _ ⇒ P ] | t1F ⇒ match n2 with [ t1F ⇒ P → P | _ ⇒ P ]]
 685    | _ ⇒ P ].
 686  #n1; #i2; #P;
 687  ncases i2;
 688  nnormalize;
 689  ##[ ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H;
 690      napply False_ind;
 691      nchange with (match MODE_SRT n1 with [ MODE_SRT a ⇒ False | _ ⇒ True ]);
 692      nrewrite > H; nnormalize; napply I
 693  ##| ##31,32,33: #n; #H;
 694      napply False_ind;
 695      nchange with (match MODE_SRT n1 with [ MODE_SRT n1 ⇒ False | _ ⇒ True ]);
 696      nrewrite > H; nnormalize; napply I
 697  ##| ##34: #n2;
 698      ncases n1;
 699      ##[ ##1: ncases n2; nnormalize;
 700               ##[ ##1: #H; napply (λx:P.x)
 701               ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
 702               ##]
 703      ##| ##2: ncases n2; nnormalize;
 704               ##[ ##2: #H; napply (λx:P.x)
 705               ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
 706               ##]
 707      ##| ##3: ncases n2; nnormalize;
 708               ##[ ##3: #H; napply (λx:P.x)
 709               ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
 710               ##]
 711      ##| ##4: ncases n2; nnormalize;
 712               ##[ ##4: #H; napply (λx:P.x)
 713               ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
 714               ##]
 715      ##| ##5: ncases n2; nnormalize;
 716               ##[ ##5: #H; napply (λx:P.x)
 717               ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
 718               ##]
 719      ##| ##6: ncases n2; nnormalize;
 720               ##[ ##6: #H; napply (λx:P.x)
 721               ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
 722               ##]
 723      ##| ##7: ncases n2; nnormalize;
 724               ##[ ##7: #H; napply (λx:P.x)
 725               ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
 726               ##]
 727      ##| ##8: ncases n2; nnormalize;
 728               ##[ ##8: #H; napply (λx:P.x)
 729               ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
 730               ##]
 731      ##| ##9: ncases n2; nnormalize;
 732               ##[ ##9: #H; napply (λx:P.x)
 733               ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
 734               ##]
 735      ##| ##10: ncases n2; nnormalize;
 736               ##[ ##10: #H; napply (λx:P.x)
 737               ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
 738               ##]
 739      ##| ##11: ncases n2; nnormalize;
 740               ##[ ##11: #H; napply (λx:P.x)
 741               ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
 742               ##]
 743      ##| ##12: ncases n2; nnormalize;
 744               ##[ ##12: #H; napply (λx:P.x)
 745               ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
 746               ##]
 747      ##| ##13: ncases n2; nnormalize;
 748               ##[ ##13: #H; napply (λx:P.x)
 749               ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
 750               ##]
 751      ##| ##14: ncases n2; nnormalize;
 752               ##[ ##14: #H; napply (λx:P.x)
 753               ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
 754               ##]
 755      ##| ##15: ncases n2; nnormalize;
 756               ##[ ##15: #H; napply (λx:P.x)
 757               ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
 758               ##]
 759      ##| ##16: ncases n2; nnormalize;
 760               ##[ ##16: #H; napply (λx:P.x)
 761               ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
 762               ##]
 763      ##| ##17: ncases n2; nnormalize;
 764               ##[ ##17: #H; napply (λx:P.x)
 765               ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
 766               ##]
 767      ##| ##18: ncases n2; nnormalize;
 768               ##[ ##18: #H; napply (λx:P.x)
 769               ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
 770               ##]
 771      ##| ##19: ncases n2; nnormalize;
 772               ##[ ##19: #H; napply (λx:P.x)
 773               ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
 774               ##]
 775      ##| ##20: ncases n2; nnormalize;
 776               ##[ ##20: #H; napply (λx:P.x)
 777               ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
 778               ##]
 779      ##| ##21: ncases n2; nnormalize;
 780               ##[ ##21: #H; napply (λx:P.x)
 781               ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
 782               ##]
 783      ##| ##22: ncases n2; nnormalize;
 784               ##[ ##22: #H; napply (λx:P.x)
 785               ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
 786               ##]
 787      ##| ##23: ncases n2; nnormalize;
 788               ##[ ##23: #H; napply (λx:P.x)
 789               ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
 790               ##]
 791      ##| ##24: ncases n2; nnormalize;
 792               ##[ ##24: #H; napply (λx:P.x)
 793               ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
 794               ##]
 795      ##| ##25: ncases n2; nnormalize;
 796               ##[ ##25: #H; napply (λx:P.x)
 797               ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
 798               ##]
 799      ##| ##26: ncases n2; nnormalize;
 800               ##[ ##26: #H; napply (λx:P.x)
 801               ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
 802               ##]
 803      ##| ##27: ncases n2; nnormalize;
 804               ##[ ##27: #H; napply (λx:P.x)
 805               ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
 806               ##]
 807      ##| ##28: ncases n2; nnormalize;
 808               ##[ ##28: #H; napply (λx:P.x)
 809               ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
 810               ##]
 811      ##| ##29: ncases n2; nnormalize;
 812               ##[ ##29: #H; napply (λx:P.x)
 813               ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
 814               ##]
 815      ##| ##30: ncases n2; nnormalize;
 816               ##[ ##30: #H; napply (λx:P.x)
 817               ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
 818               ##]
 819      ##| ##31: ncases n2; nnormalize;
 820               ##[ ##31: #H; napply (λx:P.x)
 821               ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
 822               ##]
 823      ##| ##32: ncases n2; nnormalize;
 824               ##[ ##32: #H; napply (λx:P.x)
 825               ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
 826               ##]
 827      ##]
 828  ##]
 829 nqed.
 830
 831 ndefinition instr_mode_destruct_aux ≝
 832 Πi1,i2.ΠP:Prop.i1 = i2 →
 833  match i1 with
 834   [ MODE_INH ⇒ match i2 with [ MODE_INH ⇒ P → P | _ ⇒ P ]
 835   | MODE_INHA ⇒ match i2 with [ MODE_INHA ⇒ P → P | _ ⇒ P ]
 836   | MODE_INHX ⇒ match i2 with [ MODE_INHX ⇒ P → P | _ ⇒ P ]
 837   | MODE_INHH ⇒ match i2 with [ MODE_INHH ⇒ P → P | _ ⇒ P ]
 838   | MODE_INHX0ADD ⇒ match i2 with [ MODE_INHX0ADD ⇒ P → P | _ ⇒ P ]
 839   | MODE_INHX1ADD ⇒ match i2 with [ MODE_INHX1ADD ⇒ P → P | _ ⇒ P ]
 840   | MODE_INHX2ADD ⇒ match i2 with [ MODE_INHX2ADD ⇒ P → P | _ ⇒ P ]
 841   | MODE_IMM1 ⇒ match i2 with [ MODE_IMM1 ⇒ P → P | _ ⇒ P ]
 842   | MODE_IMM1EXT ⇒ match i2 with [ MODE_IMM1EXT ⇒ P → P | _ ⇒ P ]
 843   | MODE_IMM2 ⇒ match i2 with [ MODE_IMM2 ⇒ P → P | _ ⇒ P ]
 844   | MODE_DIR1 ⇒ match i2 with [ MODE_DIR1 ⇒ P → P | _ ⇒ P ]
 845   | MODE_DIR2 ⇒ match i2 with [ MODE_DIR2 ⇒ P → P | _ ⇒ P ]
 846   | MODE_IX0 ⇒ match i2 with [ MODE_IX0 ⇒ P → P | _ ⇒ P ]
 847   | MODE_IX1 ⇒ match i2 with [ MODE_IX1 ⇒ P → P | _ ⇒ P ]
 848   | MODE_IX2 ⇒ match i2 with [ MODE_IX2 ⇒ P → P | _ ⇒ P ]
 849   | MODE_SP1 ⇒ match i2 with [ MODE_SP1 ⇒ P → P | _ ⇒ P ]
 850   | MODE_SP2 ⇒ match i2 with [ MODE_SP2 ⇒ P → P | _ ⇒ P ]
 851   | MODE_DIR1_to_DIR1  ⇒ match i2 with [ MODE_DIR1_to_DIR1  ⇒ P → P | _ ⇒ P ]
 852   | MODE_IMM1_to_DIR1 ⇒ match i2 with [ MODE_IMM1_to_DIR1 ⇒ P → P | _ ⇒ P ]
 853   | MODE_IX0p_to_DIR1 ⇒ match i2 with [ MODE_IX0p_to_DIR1 ⇒ P → P | _ ⇒ P ]
 854   | MODE_DIR1_to_IX0p ⇒ match i2 with [ MODE_DIR1_to_IX0p ⇒ P → P | _ ⇒ P ]
 855   | MODE_INHA_and_IMM1 ⇒ match i2 with [ MODE_INHA_and_IMM1 ⇒ P → P | _ ⇒ P ]
 856   | MODE_INHX_and_IMM1 ⇒ match i2 with [ MODE_INHX_and_IMM1 ⇒ P → P | _ ⇒ P ]
 857   | MODE_IMM1_and_IMM1 ⇒ match i2 with [ MODE_IMM1_and_IMM1 ⇒ P → P | _ ⇒ P ]
 858   | MODE_DIR1_and_IMM1 ⇒ match i2 with [ MODE_DIR1_and_IMM1 ⇒ P → P | _ ⇒ P ]
 859   | MODE_IX0_and_IMM1 ⇒ match i2 with [ MODE_IX0_and_IMM1 ⇒ P → P | _ ⇒ P ]
 860   | MODE_IX0p_and_IMM1 ⇒ match i2 with [ MODE_IX0p_and_IMM1 ⇒ P → P | _ ⇒ P ]
 861   | MODE_IX1_and_IMM1 ⇒ match i2 with [ MODE_IX1_and_IMM1 ⇒ P → P | _ ⇒ P ]
 862   | MODE_IX1p_and_IMM1 ⇒ match i2 with [ MODE_IX1p_and_IMM1 ⇒ P → P | _ ⇒ P ]
 863   | MODE_SP1_and_IMM1 ⇒ match i2 with [ MODE_SP1_and_IMM1 ⇒ P → P | _ ⇒ P ]
 864   | MODE_DIRn n1 ⇒ match i2 with
 865    [ MODE_DIRn n2 ⇒ match n1 with
 866     [ o0 ⇒ match n2 with [ o0 ⇒ P → P | _ ⇒ P ] | o1 ⇒ match n2 with [ o1 ⇒ P → P | _ ⇒ P ]
 867     | o2 ⇒ match n2 with [ o2 ⇒ P → P | _ ⇒ P ] | o3 ⇒ match n2 with [ o3 ⇒ P → P | _ ⇒ P ]
 868     | o4 ⇒ match n2 with [ o4 ⇒ P → P | _ ⇒ P ] | o5 ⇒ match n2 with [ o5 ⇒ P → P | _ ⇒ P ]
 869     | o6 ⇒ match n2 with [ o6 ⇒ P → P | _ ⇒ P ] | o7 ⇒ match n2 with [ o7 ⇒ P → P | _ ⇒ P ]]
 870    | _ ⇒ P ]
 871   | MODE_DIRn_and_IMM1 n1 ⇒ match i2 with
 872    [ MODE_DIRn_and_IMM1 n2 ⇒ match n1 with
 873     [ o0 ⇒ match n2 with [ o0 ⇒ P → P | _ ⇒ P ] | o1 ⇒ match n2 with [ o1 ⇒ P → P | _ ⇒ P ]
 874     | o2 ⇒ match n2 with [ o2 ⇒ P → P | _ ⇒ P ] | o3 ⇒ match n2 with [ o3 ⇒ P → P | _ ⇒ P ]
 875     | o4 ⇒ match n2 with [ o4 ⇒ P → P | _ ⇒ P ] | o5 ⇒ match n2 with [ o5 ⇒ P → P | _ ⇒ P ]
 876     | o6 ⇒ match n2 with [ o6 ⇒ P → P | _ ⇒ P ] | o7 ⇒ match n2 with [ o7 ⇒ P → P | _ ⇒ P ]]
 877    | _ ⇒ P ]
 878   | MODE_TNY e1 ⇒ match i2 with
 879    [ MODE_TNY e2 ⇒ match e1 with
 880     [ x0 ⇒ match e2 with [ x0 ⇒ P → P | _ ⇒ P ] | x1 ⇒ match e2 with [ x1 ⇒ P → P | _ ⇒ P ]
 881     | x2 ⇒ match e2 with [ x2 ⇒ P → P | _ ⇒ P ] | x3 ⇒ match e2 with [ x3 ⇒ P → P | _ ⇒ P ]
 882     | x4 ⇒ match e2 with [ x4 ⇒ P → P | _ ⇒ P ] | x5 ⇒ match e2 with [ x5 ⇒ P → P | _ ⇒ P ]
 883     | x6 ⇒ match e2 with [ x6 ⇒ P → P | _ ⇒ P ] | x7 ⇒ match e2 with [ x7 ⇒ P → P | _ ⇒ P ]
 884     | x8 ⇒ match e2 with [ x8 ⇒ P → P | _ ⇒ P ] | x9 ⇒ match e2 with [ x9 ⇒ P → P | _ ⇒ P ]
 885     | xA ⇒ match e2 with [ xA ⇒ P → P | _ ⇒ P ] | xB ⇒ match e2 with [ xB ⇒ P → P | _ ⇒ P ]
 886     | xC ⇒ match e2 with [ xC ⇒ P → P | _ ⇒ P ] | xD ⇒ match e2 with [ xD ⇒ P → P | _ ⇒ P ]
 887     | xE ⇒ match e2 with [ xE ⇒ P → P | _ ⇒ P ] | xF ⇒ match e2 with [ xF ⇒ P → P | _ ⇒ P ]]
 888    | _ ⇒ P ]
 889   | MODE_SRT t1 ⇒ match i2 with
 890    [ MODE_SRT t2 ⇒ match t1 with
 891     [ t00 ⇒ match t2 with [ t00 ⇒ P → P | _ ⇒ P ] | t01 ⇒ match t2 with [ t01 ⇒ P → P | _ ⇒ P ]
 892     | t02 ⇒ match t2 with [ t02 ⇒ P → P | _ ⇒ P ] | t03 ⇒ match t2 with [ t03 ⇒ P → P | _ ⇒ P ]
 893     | t04 ⇒ match t2 with [ t04 ⇒ P → P | _ ⇒ P ] | t05 ⇒ match t2 with [ t05 ⇒ P → P | _ ⇒ P ]
 894     | t06 ⇒ match t2 with [ t06 ⇒ P → P | _ ⇒ P ] | t07 ⇒ match t2 with [ t07 ⇒ P → P | _ ⇒ P ]
 895     | t08 ⇒ match t2 with [ t08 ⇒ P → P | _ ⇒ P ] | t09 ⇒ match t2 with [ t09 ⇒ P → P | _ ⇒ P ]
 896     | t0A ⇒ match t2 with [ t0A ⇒ P → P | _ ⇒ P ] | t0B ⇒ match t2 with [ t0B ⇒ P → P | _ ⇒ P ]
 897     | t0C ⇒ match t2 with [ t0C ⇒ P → P | _ ⇒ P ] | t0D ⇒ match t2 with [ t0D ⇒ P → P | _ ⇒ P ]
 898     | t0E ⇒ match t2 with [ t0E ⇒ P → P | _ ⇒ P ] | t0F ⇒ match t2 with [ t0F ⇒ P → P | _ ⇒ P ]
 899     | t10 ⇒ match t2 with [ t10 ⇒ P → P | _ ⇒ P ] | t11 ⇒ match t2 with [ t11 ⇒ P → P | _ ⇒ P ]
 900     | t12 ⇒ match t2 with [ t12 ⇒ P → P | _ ⇒ P ] | t13 ⇒ match t2 with [ t13 ⇒ P → P | _ ⇒ P ]
 901     | t14 ⇒ match t2 with [ t14 ⇒ P → P | _ ⇒ P ] | t15 ⇒ match t2 with [ t15 ⇒ P → P | _ ⇒ P ]
 902     | t16 ⇒ match t2 with [ t16 ⇒ P → P | _ ⇒ P ] | t17 ⇒ match t2 with [ t17 ⇒ P → P | _ ⇒ P ]
 903     | t18 ⇒ match t2 with [ t18 ⇒ P → P | _ ⇒ P ] | t19 ⇒ match t2 with [ t19 ⇒ P → P | _ ⇒ P ]
 904     | t1A ⇒ match t2 with [ t1A ⇒ P → P | _ ⇒ P ] | t1B ⇒ match t2 with [ t1B ⇒ P → P | _ ⇒ P ]
 905     | t1C ⇒ match t2 with [ t1C ⇒ P → P | _ ⇒ P ] | t1D ⇒ match t2 with [ t1D ⇒ P → P | _ ⇒ P ]
 906     | t1E ⇒ match t2 with [ t1E ⇒ P → P | _ ⇒ P ] | t1F ⇒ match t2 with [ t1F ⇒ P → P | _ ⇒ P ]]
 907     | _ ⇒ P ]
 908   ].
 909
 910 ndefinition instr_mode_destruct : instr_mode_destruct_aux.
 911  #t1; ncases t1;
 912  ##[ ##1: napply instr_mode_destruct1 ##| ##2: napply instr_mode_destruct2
 913  ##| ##3: napply instr_mode_destruct3 ##| ##4: napply instr_mode_destruct4
 914  ##| ##5: napply instr_mode_destruct5 ##| ##6: napply instr_mode_destruct6
 915  ##| ##7: napply instr_mode_destruct7 ##| ##8: napply instr_mode_destruct8
 916  ##| ##9: napply instr_mode_destruct9 ##| ##10: napply instr_mode_destruct10
 917  ##| ##11: napply instr_mode_destruct11 ##| ##12: napply instr_mode_destruct12
 918  ##| ##13: napply instr_mode_destruct13 ##| ##14: napply instr_mode_destruct14
 919  ##| ##15: napply instr_mode_destruct15 ##| ##16: napply instr_mode_destruct16
 920  ##| ##17: napply instr_mode_destruct17 ##| ##18: napply instr_mode_destruct18
 921  ##| ##19: napply instr_mode_destruct19 ##| ##20: napply instr_mode_destruct20
 922  ##| ##21: napply instr_mode_destruct21 ##| ##22: napply instr_mode_destruct22
 923  ##| ##23: napply instr_mode_destruct23 ##| ##24: napply instr_mode_destruct24
 924  ##| ##25: napply instr_mode_destruct25 ##| ##26: napply instr_mode_destruct26
 925  ##| ##27: napply instr_mode_destruct27 ##| ##28: napply instr_mode_destruct28
 926  ##| ##29: napply instr_mode_destruct29 ##| ##30: napply instr_mode_destruct30
 927  ##| ##31: napply instr_mode_destruct31 ##| ##32: napply instr_mode_destruct32
 928  ##| ##33: napply instr_mode_destruct33 ##| ##34: napply instr_mode_destruct34
 929  ##]
 930 nqed.