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