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