helm/software/matita/contribs/ng_assembly/freescale/opcode_base_lemmas_instrmode2.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/opcode_base_lemmas_instrmode1.ma".
  28
  29 (* ********************************************** *)
  30 (* MATTONI BASE PER DEFINIRE LE TABELLE DELLE MCU *)
  31 (* ********************************************** *)
  32
  33 nlemma symmetric_eqinstrmode : symmetricT instr_mode bool eq_instrmode.
  34  #i1; #i2;
  35  ncases i1;
  36  ##[ ##1: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply (refl_eq ??)
  37  ##| ##2: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply (refl_eq ??)
  38  ##| ##3: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply (refl_eq ??)
  39  ##| ##4: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply (refl_eq ??)
  40  ##| ##5: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply (refl_eq ??)
  41  ##| ##6: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply (refl_eq ??)
  42  ##| ##7: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply (refl_eq ??)
  43  ##| ##8: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply (refl_eq ??)
  44  ##| ##9: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply (refl_eq ??)
  45  ##| ##10: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply (refl_eq ??)
  46  ##| ##11: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply (refl_eq ??)
  47  ##| ##12: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply (refl_eq ??)
  48  ##| ##13: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply (refl_eq ??)
  49  ##| ##14: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply (refl_eq ??)
  50  ##| ##15: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply (refl_eq ??)
  51  ##| ##16: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply (refl_eq ??)
  52  ##| ##17: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply (refl_eq ??)
  53  ##| ##18: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply (refl_eq ??)
  54  ##| ##19: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply (refl_eq ??)
  55  ##| ##20: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply (refl_eq ??)
  56  ##| ##21: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply (refl_eq ??)
  57  ##| ##22: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply (refl_eq ??)
  58  ##| ##23: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply (refl_eq ??)
  59  ##| ##24: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply (refl_eq ??)
  60  ##| ##25: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply (refl_eq ??)
  61  ##| ##26: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply (refl_eq ??)
  62  ##| ##27: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply (refl_eq ??)
  63  ##| ##28: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply (refl_eq ??)
  64  ##| ##29: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply (refl_eq ??)
  65  ##| ##30: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply (refl_eq ??)
  66  ##| ##31: ncases i2; #n1;
  67      ##[ ##31: #n2;
  68                nchange with (eq_oct n2 n1 = eq_oct n1 n2);
  69                nrewrite > (symmetric_eqoct n1 n2);
  70      ##| ##32,33,34: #n2; nnormalize
  71      ##]
  72      nnormalize; napply (refl_eq ??)
  73  ##| ##32: ncases i2; #n1;
  74      ##[ ##32: #n2;
  75                nchange with (eq_oct n2 n1 = eq_oct n1 n2);
  76                nrewrite > (symmetric_eqoct n1 n2);
  77      ##| ##31,33,34: #n2; nnormalize
  78      ##]
  79      nnormalize; napply (refl_eq ??)
  80  ##| ##33: ncases i2; #n1;
  81      ##[ ##33: #n2;
  82                nchange with (eq_ex n2 n1 = eq_ex n1 n2);
  83                nrewrite > (symmetric_eqex n1 n2);
  84      ##| ##31,32,34: #n2; nnormalize
  85      ##]
  86      nnormalize; napply (refl_eq ??)
  87  ##| ##34: ncases i2; #n1;
  88      ##[ ##34: #n2;
  89                nchange with (eq_bitrig n2 n1 = eq_bitrig n1 n2);
  90                nrewrite > (symmetric_eqbitrig n1 n2);
  91      ##| ##31,32,33: #n2; nnormalize
  92      ##]
  93      nnormalize; napply (refl_eq ??)
  94  ##]
  95 nqed.
  96
  97 nlemma eqinstrmode_to_eq1 : ∀i2.eq_instrmode MODE_INH i2 = true → MODE_INH = i2.
  98  #i2; ncases i2; nnormalize;
  99  ##[ ##1: #H; napply (refl_eq ??)
 100  ##| ##31,32,33,34: #n; #H; napply (bool_destruct ??? H)
 101  ##| ##*: #H; napply (bool_destruct ??? H)
 102  ##]
 103 nqed.
 104
 105 nlemma eqinstrmode_to_eq2 : ∀i2.eq_instrmode MODE_INHA i2 = true → MODE_INHA = i2.
 106  #i2; ncases i2; nnormalize;
 107  ##[ ##2: #H; napply (refl_eq ??)
 108  ##| ##31,32,33,34: #n; #H; napply (bool_destruct ??? H)
 109  ##| ##*: #H; napply (bool_destruct ??? H)
 110  ##]
 111 nqed.
 112
 113 nlemma eqinstrmode_to_eq3 : ∀i2.eq_instrmode MODE_INHX i2 = true → MODE_INHX = i2.
 114  #i2; ncases i2; nnormalize;
 115  ##[ ##3: #H; napply (refl_eq ??)
 116  ##| ##31,32,33,34: #n; #H; napply (bool_destruct ??? H)
 117  ##| ##*: #H; napply (bool_destruct ??? H)
 118  ##]
 119 nqed.
 120
 121 nlemma eqinstrmode_to_eq4 : ∀i2.eq_instrmode MODE_INHH i2 = true → MODE_INHH = i2.
 122  #i2; ncases i2; nnormalize;
 123  ##[ ##4: #H; napply (refl_eq ??)
 124  ##| ##31,32,33,34: #n; #H; napply (bool_destruct ??? H)
 125  ##| ##*: #H; napply (bool_destruct ??? H)
 126  ##]
 127 nqed.
 128
 129 nlemma eqinstrmode_to_eq5 : ∀i2.eq_instrmode MODE_INHX0ADD i2 = true → MODE_INHX0ADD = i2.
 130  #i2; ncases i2; nnormalize;
 131  ##[ ##5: #H; napply (refl_eq ??)
 132  ##| ##31,32,33,34: #n; #H; napply (bool_destruct ??? H)
 133  ##| ##*: #H; napply (bool_destruct ??? H)
 134  ##]
 135 nqed.
 136
 137 nlemma eqinstrmode_to_eq6 : ∀i2.eq_instrmode MODE_INHX1ADD i2 = true → MODE_INHX1ADD = i2.
 138  #i2; ncases i2; nnormalize;
 139  ##[ ##6: #H; napply (refl_eq ??)
 140  ##| ##31,32,33,34: #n; #H; napply (bool_destruct ??? H)
 141  ##| ##*: #H; napply (bool_destruct ??? H)
 142  ##]
 143 nqed.
 144
 145 nlemma eqinstrmode_to_eq7 : ∀i2.eq_instrmode MODE_INHX2ADD i2 = true → MODE_INHX2ADD = i2.
 146  #i2; ncases i2; nnormalize;
 147  ##[ ##7: #H; napply (refl_eq ??)
 148  ##| ##31,32,33,34: #n; #H; napply (bool_destruct ??? H)
 149  ##| ##*: #H; napply (bool_destruct ??? H)
 150  ##]
 151 nqed.
 152
 153 nlemma eqinstrmode_to_eq8 : ∀i2.eq_instrmode MODE_IMM1 i2 = true → MODE_IMM1 = i2.
 154  #i2; ncases i2; nnormalize;
 155  ##[ ##8: #H; napply (refl_eq ??)
 156  ##| ##31,32,33,34: #n; #H; napply (bool_destruct ??? H)
 157  ##| ##*: #H; napply (bool_destruct ??? H)
 158  ##]
 159 nqed.
 160
 161 nlemma eqinstrmode_to_eq9 : ∀i2.eq_instrmode MODE_IMM1EXT i2 = true → MODE_IMM1EXT = i2.
 162  #i2; ncases i2; nnormalize;
 163  ##[ ##9: #H; napply (refl_eq ??)
 164  ##| ##31,32,33,34: #n; #H; napply (bool_destruct ??? H)
 165  ##| ##*: #H; napply (bool_destruct ??? H)
 166  ##]
 167 nqed.
 168
 169 nlemma eqinstrmode_to_eq10 : ∀i2.eq_instrmode MODE_IMM2 i2 = true → MODE_IMM2 = i2.
 170  #i2; ncases i2; nnormalize;
 171  ##[ ##10: #H; napply (refl_eq ??)
 172  ##| ##31,32,33,34: #n; #H; napply (bool_destruct ??? H)
 173  ##| ##*: #H; napply (bool_destruct ??? H)
 174  ##]
 175 nqed.
 176
 177 nlemma eqinstrmode_to_eq11 : ∀i2.eq_instrmode MODE_DIR1 i2 = true → MODE_DIR1 = i2.
 178  #i2; ncases i2; nnormalize;
 179  ##[ ##11: #H; napply (refl_eq ??)
 180  ##| ##31,32,33,34: #n; #H; napply (bool_destruct ??? H)
 181  ##| ##*: #H; napply (bool_destruct ??? H)
 182  ##]
 183 nqed.
 184
 185 nlemma eqinstrmode_to_eq12 : ∀i2.eq_instrmode MODE_DIR2 i2 = true → MODE_DIR2 = i2.
 186  #i2; ncases i2; nnormalize;
 187  ##[ ##12: #H; napply (refl_eq ??)
 188  ##| ##31,32,33,34: #n; #H; napply (bool_destruct ??? H)
 189  ##| ##*: #H; napply (bool_destruct ??? H)
 190  ##]
 191 nqed.
 192
 193 nlemma eqinstrmode_to_eq13 : ∀i2.eq_instrmode MODE_IX0 i2 = true → MODE_IX0 = i2.
 194  #i2; ncases i2; nnormalize;
 195  ##[ ##13: #H; napply (refl_eq ??)
 196  ##| ##31,32,33,34: #n; #H; napply (bool_destruct ??? H)
 197  ##| ##*: #H; napply (bool_destruct ??? H)
 198  ##]
 199 nqed.
 200
 201 nlemma eqinstrmode_to_eq14 : ∀i2.eq_instrmode MODE_IX1 i2 = true → MODE_IX1 = i2.
 202  #i2; ncases i2; nnormalize;
 203  ##[ ##14: #H; napply (refl_eq ??)
 204  ##| ##31,32,33,34: #n; #H; napply (bool_destruct ??? H)
 205  ##| ##*: #H; napply (bool_destruct ??? H)
 206  ##]
 207 nqed.
 208
 209 nlemma eqinstrmode_to_eq15 : ∀i2.eq_instrmode MODE_IX2 i2 = true → MODE_IX2 = i2.
 210  #i2; ncases i2; nnormalize;
 211  ##[ ##15: #H; napply (refl_eq ??)
 212  ##| ##31,32,33,34: #n; #H; napply (bool_destruct ??? H)
 213  ##| ##*: #H; napply (bool_destruct ??? H)
 214  ##]
 215 nqed.
 216
 217 nlemma eqinstrmode_to_eq16 : ∀i2.eq_instrmode MODE_SP1 i2 = true → MODE_SP1 = i2.
 218  #i2; ncases i2; nnormalize;
 219  ##[ ##16: #H; napply (refl_eq ??)
 220  ##| ##31,32,33,34: #n; #H; napply (bool_destruct ??? H)
 221  ##| ##*: #H; napply (bool_destruct ??? H)
 222  ##]
 223 nqed.
 224
 225 nlemma eqinstrmode_to_eq17 : ∀i2.eq_instrmode MODE_SP2 i2 = true → MODE_SP2 = i2.
 226  #i2; ncases i2; nnormalize;
 227  ##[ ##17: #H; napply (refl_eq ??)
 228  ##| ##31,32,33,34: #n; #H; napply (bool_destruct ??? H)
 229  ##| ##*: #H; napply (bool_destruct ??? H)
 230  ##]
 231 nqed.
 232
 233 nlemma eqinstrmode_to_eq18 : ∀i2.eq_instrmode MODE_DIR1_to_DIR1 i2 = true → MODE_DIR1_to_DIR1 = i2.
 234  #i2; ncases i2; nnormalize;
 235  ##[ ##18: #H; napply (refl_eq ??)
 236  ##| ##31,32,33,34: #n; #H; napply (bool_destruct ??? H)
 237  ##| ##*: #H; napply (bool_destruct ??? H)
 238  ##]
 239 nqed.
 240
 241 nlemma eqinstrmode_to_eq19 : ∀i2.eq_instrmode MODE_IMM1_to_DIR1 i2 = true → MODE_IMM1_to_DIR1 = i2.
 242  #i2; ncases i2; nnormalize;
 243  ##[ ##19: #H; napply (refl_eq ??)
 244  ##| ##31,32,33,34: #n; #H; napply (bool_destruct ??? H)
 245  ##| ##*: #H; napply (bool_destruct ??? H)
 246  ##]
 247 nqed.
 248
 249 nlemma eqinstrmode_to_eq20 : ∀i2.eq_instrmode MODE_IX0p_to_DIR1 i2 = true → MODE_IX0p_to_DIR1 = i2.
 250  #i2; ncases i2; nnormalize;
 251  ##[ ##20: #H; napply (refl_eq ??)
 252  ##| ##31,32,33,34: #n; #H; napply (bool_destruct ??? H)
 253  ##| ##*: #H; napply (bool_destruct ??? H)
 254  ##]
 255 nqed.
 256
 257 nlemma eqinstrmode_to_eq21 : ∀i2.eq_instrmode MODE_DIR1_to_IX0p i2 = true → MODE_DIR1_to_IX0p = i2.
 258  #i2; ncases i2; nnormalize;
 259  ##[ ##21: #H; napply (refl_eq ??)
 260  ##| ##31,32,33,34: #n; #H; napply (bool_destruct ??? H)
 261  ##| ##*: #H; napply (bool_destruct ??? H)
 262  ##]
 263 nqed.
 264
 265 nlemma eqinstrmode_to_eq22 : ∀i2.eq_instrmode MODE_INHA_and_IMM1 i2 = true → MODE_INHA_and_IMM1 = i2.
 266  #i2; ncases i2; nnormalize;
 267  ##[ ##22: #H; napply (refl_eq ??)
 268  ##| ##31,32,33,34: #n; #H; napply (bool_destruct ??? H)
 269  ##| ##*: #H; napply (bool_destruct ??? H)
 270  ##]
 271 nqed.
 272
 273 nlemma eqinstrmode_to_eq23 : ∀i2.eq_instrmode MODE_INHX_and_IMM1 i2 = true → MODE_INHX_and_IMM1 = i2.
 274  #i2; ncases i2; nnormalize;
 275  ##[ ##23: #H; napply (refl_eq ??)
 276  ##| ##31,32,33,34: #n; #H; napply (bool_destruct ??? H)
 277  ##| ##*: #H; napply (bool_destruct ??? H)
 278  ##]
 279 nqed.
 280
 281 nlemma eqinstrmode_to_eq24 : ∀i2.eq_instrmode MODE_IMM1_and_IMM1 i2 = true → MODE_IMM1_and_IMM1 = i2.
 282  #i2; ncases i2; nnormalize;
 283  ##[ ##24: #H; napply (refl_eq ??)
 284  ##| ##31,32,33,34: #n; #H; napply (bool_destruct ??? H)
 285  ##| ##*: #H; napply (bool_destruct ??? H)
 286  ##]
 287 nqed.
 288
 289 nlemma eqinstrmode_to_eq25 : ∀i2.eq_instrmode MODE_DIR1_and_IMM1 i2 = true → MODE_DIR1_and_IMM1 = i2.
 290  #i2; ncases i2; nnormalize;
 291  ##[ ##25: #H; napply (refl_eq ??)
 292  ##| ##31,32,33,34: #n; #H; napply (bool_destruct ??? H)
 293  ##| ##*: #H; napply (bool_destruct ??? H)
 294  ##]
 295 nqed.
 296
 297 nlemma eqinstrmode_to_eq26 : ∀i2.eq_instrmode MODE_IX0_and_IMM1 i2 = true → MODE_IX0_and_IMM1 = i2.
 298  #i2; ncases i2; nnormalize;
 299  ##[ ##26: #H; napply (refl_eq ??)
 300  ##| ##31,32,33,34: #n; #H; napply (bool_destruct ??? H)
 301  ##| ##*: #H; napply (bool_destruct ??? H)
 302  ##]
 303 nqed.
 304
 305 nlemma eqinstrmode_to_eq27 : ∀i2.eq_instrmode MODE_IX0p_and_IMM1 i2 = true → MODE_IX0p_and_IMM1 = i2.
 306  #i2; ncases i2; nnormalize;
 307  ##[ ##27: #H; napply (refl_eq ??)
 308  ##| ##31,32,33,34: #n; #H; napply (bool_destruct ??? H)
 309  ##| ##*: #H; napply (bool_destruct ??? H)
 310  ##]
 311 nqed.
 312
 313 nlemma eqinstrmode_to_eq28 : ∀i2.eq_instrmode MODE_IX1_and_IMM1 i2 = true → MODE_IX1_and_IMM1 = i2.
 314  #i2; ncases i2; nnormalize;
 315  ##[ ##28: #H; napply (refl_eq ??)
 316  ##| ##31,32,33,34: #n; #H; napply (bool_destruct ??? H)
 317  ##| ##*: #H; napply (bool_destruct ??? H)
 318  ##]
 319 nqed.
 320
 321 nlemma eqinstrmode_to_eq29 : ∀i2.eq_instrmode MODE_IX1p_and_IMM1 i2 = true → MODE_IX1p_and_IMM1 = i2.
 322  #i2; ncases i2; nnormalize;
 323  ##[ ##29: #H; napply (refl_eq ??)
 324  ##| ##31,32,33,34: #n; #H; napply (bool_destruct ??? H)
 325  ##| ##*: #H; napply (bool_destruct ??? H)
 326  ##]
 327 nqed.
 328
 329 nlemma eqinstrmode_to_eq30 : ∀i2.eq_instrmode MODE_SP1_and_IMM1 i2 = true → MODE_SP1_and_IMM1 = i2.
 330  #i2; ncases i2; nnormalize;
 331  ##[ ##30: #H; napply (refl_eq ??)
 332  ##| ##31,32,33,34: #n; #H; napply (bool_destruct ??? H)
 333  ##| ##*: #H; napply (bool_destruct ??? H)
 334  ##]
 335 nqed.
 336
 337 nlemma eqinstrmode_to_eq31 : ∀n1,i2.eq_instrmode (MODE_DIRn n1) i2 = true → MODE_DIRn n1 = i2.
 338  #n1; #i2; ncases i2;
 339  ##[ ##31: #n2; #H;
 340      nchange in H:(%) with (eq_oct n1 n2 = true);
 341      nrewrite > (eqoct_to_eq ?? H);
 342      napply (refl_eq ??)
 343  ##| ##32,33,34: nnormalize; #n2; #H; napply (bool_destruct ??? H)
 344  ##| ##*: nnormalize; #H; napply (bool_destruct ??? H)
 345  ##]
 346 nqed.
 347
 348 nlemma eqinstrmode_to_eq32 : ∀n1,i2.eq_instrmode (MODE_DIRn_and_IMM1 n1) i2 = true → MODE_DIRn_and_IMM1 n1 = i2.
 349  #n1; #i2; ncases i2;
 350  ##[ ##32: #n2; #H;
 351      nchange in H:(%) with (eq_oct n1 n2 = true);
 352      nrewrite > (eqoct_to_eq ?? H);
 353      napply (refl_eq ??)
 354  ##| ##31,33,34: nnormalize; #n2; #H; napply (bool_destruct ??? H)
 355  ##| ##*: nnormalize; #H; napply (bool_destruct ??? H)
 356  ##]
 357 nqed.
 358
 359 nlemma eqinstrmode_to_eq33 : ∀n1,i2.eq_instrmode (MODE_TNY n1) i2 = true → MODE_TNY n1 = i2.
 360  #n1; #i2; ncases i2;
 361  ##[ ##33: #n2; #H;
 362      nchange in H:(%) with (eq_ex n1 n2 = true);
 363      nrewrite > (eqex_to_eq ?? H);
 364      napply (refl_eq ??)
 365  ##| ##31,32,34: nnormalize; #n2; #H; napply (bool_destruct ??? H)
 366  ##| ##*: nnormalize; #H; napply (bool_destruct ??? H)
 367  ##]
 368 nqed.
 369
 370 nlemma eqinstrmode_to_eq34 : ∀n1,i2.eq_instrmode (MODE_SRT n1) i2 = true → MODE_SRT n1 = i2.
 371  #n1; #i2; ncases i2;
 372  ##[ ##34: #n2; #H;
 373      nchange in H:(%) with (eq_bitrig n1 n2 = true);
 374      nrewrite > (eqbitrig_to_eq ?? H);
 375      napply (refl_eq ??)
 376  ##| ##31,32,33: nnormalize; #n2; #H; napply (bool_destruct ??? H)
 377  ##| ##*: nnormalize; #H; napply (bool_destruct ??? H)
 378  ##]
 379 nqed.
 380
 381 nlemma eqinstrmode_to_eq : ∀i1,i2.eq_instrmode i1 i2 = true → i1 = i2.
 382  #i1; ncases i1;
 383  ##[ ##1: napply eqinstrmode_to_eq1 ##| ##2: napply eqinstrmode_to_eq2
 384  ##| ##3: napply eqinstrmode_to_eq3 ##| ##4: napply eqinstrmode_to_eq4
 385  ##| ##5: napply eqinstrmode_to_eq5 ##| ##6: napply eqinstrmode_to_eq6
 386  ##| ##7: napply eqinstrmode_to_eq7 ##| ##8: napply eqinstrmode_to_eq8
 387  ##| ##9: napply eqinstrmode_to_eq9 ##| ##10: napply eqinstrmode_to_eq10
 388  ##| ##11: napply eqinstrmode_to_eq11 ##| ##12: napply eqinstrmode_to_eq12
 389  ##| ##13: napply eqinstrmode_to_eq13 ##| ##14: napply eqinstrmode_to_eq14
 390  ##| ##15: napply eqinstrmode_to_eq15 ##| ##16: napply eqinstrmode_to_eq16
 391  ##| ##17: napply eqinstrmode_to_eq17 ##| ##18: napply eqinstrmode_to_eq18
 392  ##| ##19: napply eqinstrmode_to_eq19 ##| ##20: napply eqinstrmode_to_eq20
 393  ##| ##21: napply eqinstrmode_to_eq21 ##| ##22: napply eqinstrmode_to_eq22
 394  ##| ##23: napply eqinstrmode_to_eq23 ##| ##24: napply eqinstrmode_to_eq24
 395  ##| ##25: napply eqinstrmode_to_eq25 ##| ##26: napply eqinstrmode_to_eq26
 396  ##| ##27: napply eqinstrmode_to_eq27 ##| ##28: napply eqinstrmode_to_eq28
 397  ##| ##29: napply eqinstrmode_to_eq29 ##| ##30: napply eqinstrmode_to_eq30
 398  ##| ##31: napply eqinstrmode_to_eq31 ##| ##32: napply eqinstrmode_to_eq32
 399  ##| ##33: napply eqinstrmode_to_eq33 ##| ##34: napply eqinstrmode_to_eq34
 400  ##]
 401 nqed.
 402
 403 nlemma eq_to_eqinstrmode1 : ∀i2.MODE_INH = i2 → eq_instrmode MODE_INH i2 = true.
 404  #t2; ncases t2; nnormalize;
 405  ##[ ##1: #H; napply (refl_eq ??)
 406  ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct ??? H)
 407  ##| ##*: #H; napply (instr_mode_destruct ??? H)
 408  ##]
 409 nqed.
 410
 411 nlemma eq_to_eqinstrmode2 : ∀i2.MODE_INHA = i2 → eq_instrmode MODE_INHA i2 = true.
 412  #t2; ncases t2; nnormalize;
 413  ##[ ##2: #H; napply (refl_eq ??)
 414  ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct ??? H)
 415  ##| ##*: #H; napply (instr_mode_destruct ??? H)
 416  ##]
 417 nqed.
 418
 419 nlemma eq_to_eqinstrmode3 : ∀i2.MODE_INHX = i2 → eq_instrmode MODE_INHX i2 = true.
 420  #t2; ncases t2; nnormalize;
 421  ##[ ##3: #H; napply (refl_eq ??)
 422  ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct ??? H)
 423  ##| ##*: #H; napply (instr_mode_destruct ??? H)
 424  ##]
 425 nqed.
 426
 427 nlemma eq_to_eqinstrmode4 : ∀i2.MODE_INHH = i2 → eq_instrmode MODE_INHH i2 = true.
 428  #t2; ncases t2; nnormalize;
 429  ##[ ##4: #H; napply (refl_eq ??)
 430  ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct ??? H)
 431  ##| ##*: #H; napply (instr_mode_destruct ??? H)
 432  ##]
 433 nqed.
 434
 435 nlemma eq_to_eqinstrmode5 : ∀i2.MODE_INHX0ADD = i2 → eq_instrmode MODE_INHX0ADD i2 = true.
 436  #t2; ncases t2; nnormalize;
 437  ##[ ##5: #H; napply (refl_eq ??)
 438  ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct ??? H)
 439  ##| ##*: #H; napply (instr_mode_destruct ??? H)
 440  ##]
 441 nqed.
 442
 443 nlemma eq_to_eqinstrmode6 : ∀i2.MODE_INHX1ADD = i2 → eq_instrmode MODE_INHX1ADD i2 = true.
 444  #t2; ncases t2; nnormalize;
 445  ##[ ##6: #H; napply (refl_eq ??)
 446  ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct ??? H)
 447  ##| ##*: #H; napply (instr_mode_destruct ??? H)
 448  ##]
 449 nqed.
 450
 451 nlemma eq_to_eqinstrmode7 : ∀i2.MODE_INHX2ADD = i2 → eq_instrmode MODE_INHX2ADD i2 = true.
 452  #t2; ncases t2; nnormalize;
 453  ##[ ##7: #H; napply (refl_eq ??)
 454  ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct ??? H)
 455  ##| ##*: #H; napply (instr_mode_destruct ??? H)
 456  ##]
 457 nqed.
 458
 459 nlemma eq_to_eqinstrmode8 : ∀i2.MODE_IMM1 = i2 → eq_instrmode MODE_IMM1 i2 = true.
 460  #t2; ncases t2; nnormalize;
 461  ##[ ##8: #H; napply (refl_eq ??)
 462  ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct ??? H)
 463  ##| ##*: #H; napply (instr_mode_destruct ??? H)
 464  ##]
 465 nqed.
 466
 467 nlemma eq_to_eqinstrmode9 : ∀i2.MODE_IMM1EXT = i2 → eq_instrmode MODE_IMM1EXT i2 = true.
 468  #t2; ncases t2; nnormalize;
 469  ##[ ##9: #H; napply (refl_eq ??)
 470  ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct ??? H)
 471  ##| ##*: #H; napply (instr_mode_destruct ??? H)
 472  ##]
 473 nqed.
 474
 475 nlemma eq_to_eqinstrmode10 : ∀i2.MODE_IMM2 = i2 → eq_instrmode MODE_IMM2 i2 = true.
 476  #t2; ncases t2; nnormalize;
 477  ##[ ##10: #H; napply (refl_eq ??)
 478  ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct ??? H)
 479  ##| ##*: #H; napply (instr_mode_destruct ??? H)
 480  ##]
 481 nqed.
 482
 483 nlemma eq_to_eqinstrmode11 : ∀i2.MODE_DIR1 = i2 → eq_instrmode MODE_DIR1 i2 = true.
 484  #t2; ncases t2; nnormalize;
 485  ##[ ##11: #H; napply (refl_eq ??)
 486  ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct ??? H)
 487  ##| ##*: #H; napply (instr_mode_destruct ??? H)
 488  ##]
 489 nqed.
 490
 491 nlemma eq_to_eqinstrmode12 : ∀i2.MODE_DIR2 = i2 → eq_instrmode MODE_DIR2 i2 = true.
 492  #t2; ncases t2; nnormalize;
 493  ##[ ##12: #H; napply (refl_eq ??)
 494  ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct ??? H)
 495  ##| ##*: #H; napply (instr_mode_destruct ??? H)
 496  ##]
 497 nqed.
 498
 499 nlemma eq_to_eqinstrmode13 : ∀i2.MODE_IX0 = i2 → eq_instrmode MODE_IX0 i2 = true.
 500  #t2; ncases t2; nnormalize;
 501  ##[ ##13: #H; napply (refl_eq ??)
 502  ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct ??? H)
 503  ##| ##*: #H; napply (instr_mode_destruct ??? H)
 504  ##]
 505 nqed.
 506
 507 nlemma eq_to_eqinstrmode14 : ∀i2.MODE_IX1 = i2 → eq_instrmode MODE_IX1 i2 = true.
 508  #t2; ncases t2; nnormalize;
 509  ##[ ##14: #H; napply (refl_eq ??)
 510  ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct ??? H)
 511  ##| ##*: #H; napply (instr_mode_destruct ??? H)
 512  ##]
 513 nqed.
 514
 515 nlemma eq_to_eqinstrmode15 : ∀i2.MODE_IX2 = i2 → eq_instrmode MODE_IX2 i2 = true.
 516  #t2; ncases t2; nnormalize;
 517  ##[ ##15: #H; napply (refl_eq ??)
 518  ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct ??? H)
 519  ##| ##*: #H; napply (instr_mode_destruct ??? H)
 520  ##]
 521 nqed.
 522
 523 nlemma eq_to_eqinstrmode16 : ∀i2.MODE_SP1 = i2 → eq_instrmode MODE_SP1 i2 = true.
 524  #t2; ncases t2; nnormalize;
 525  ##[ ##16: #H; napply (refl_eq ??)
 526  ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct ??? H)
 527  ##| ##*: #H; napply (instr_mode_destruct ??? H)
 528  ##]
 529 nqed.
 530
 531 nlemma eq_to_eqinstrmode17 : ∀i2.MODE_SP2 = i2 → eq_instrmode MODE_SP2 i2 = true.
 532  #t2; ncases t2; nnormalize;
 533  ##[ ##17: #H; napply (refl_eq ??)
 534  ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct ??? H)
 535  ##| ##*: #H; napply (instr_mode_destruct ??? H)
 536  ##]
 537 nqed.
 538
 539 nlemma eq_to_eqinstrmode18 : ∀i2.MODE_DIR1_to_DIR1 = i2 → eq_instrmode MODE_DIR1_to_DIR1 i2 = true.
 540  #t2; ncases t2; nnormalize;
 541  ##[ ##18: #H; napply (refl_eq ??)
 542  ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct ??? H)
 543  ##| ##*: #H; napply (instr_mode_destruct ??? H)
 544  ##]
 545 nqed.
 546
 547 nlemma eq_to_eqinstrmode19 : ∀i2.MODE_IMM1_to_DIR1 = i2 → eq_instrmode MODE_IMM1_to_DIR1 i2 = true.
 548  #t2; ncases t2; nnormalize;
 549  ##[ ##19: #H; napply (refl_eq ??)
 550  ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct ??? H)
 551  ##| ##*: #H; napply (instr_mode_destruct ??? H)
 552  ##]
 553 nqed.
 554
 555 nlemma eq_to_eqinstrmode20 : ∀i2.MODE_IX0p_to_DIR1 = i2 → eq_instrmode MODE_IX0p_to_DIR1 i2 = true.
 556  #t2; ncases t2; nnormalize;
 557  ##[ ##20: #H; napply (refl_eq ??)
 558  ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct ??? H)
 559  ##| ##*: #H; napply (instr_mode_destruct ??? H)
 560  ##]
 561 nqed.
 562
 563 nlemma eq_to_eqinstrmode21 : ∀i2.MODE_DIR1_to_IX0p = i2 → eq_instrmode MODE_DIR1_to_IX0p i2 = true.
 564  #t2; ncases t2; nnormalize;
 565  ##[ ##21: #H; napply (refl_eq ??)
 566  ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct ??? H)
 567  ##| ##*: #H; napply (instr_mode_destruct ??? H)
 568  ##]
 569 nqed.
 570
 571 nlemma eq_to_eqinstrmode22 : ∀i2.MODE_INHA_and_IMM1 = i2 → eq_instrmode MODE_INHA_and_IMM1 i2 = true.
 572  #t2; ncases t2; nnormalize;
 573  ##[ ##22: #H; napply (refl_eq ??)
 574  ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct ??? H)
 575  ##| ##*: #H; napply (instr_mode_destruct ??? H)
 576  ##]
 577 nqed.
 578
 579 nlemma eq_to_eqinstrmode23 : ∀i2.MODE_INHX_and_IMM1 = i2 → eq_instrmode MODE_INHX_and_IMM1 i2 = true.
 580  #t2; ncases t2; nnormalize;
 581  ##[ ##23: #H; napply (refl_eq ??)
 582  ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct ??? H)
 583  ##| ##*: #H; napply (instr_mode_destruct ??? H)
 584  ##]
 585 nqed.
 586
 587 nlemma eq_to_eqinstrmode24 : ∀i2.MODE_IMM1_and_IMM1 = i2 → eq_instrmode MODE_IMM1_and_IMM1 i2 = true.
 588  #t2; ncases t2; nnormalize;
 589  ##[ ##24: #H; napply (refl_eq ??)
 590  ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct ??? H)
 591  ##| ##*: #H; napply (instr_mode_destruct ??? H)
 592  ##]
 593 nqed.
 594
 595 nlemma eq_to_eqinstrmode25 : ∀i2.MODE_DIR1_and_IMM1 = i2 → eq_instrmode MODE_DIR1_and_IMM1 i2 = true.
 596  #t2; ncases t2; nnormalize;
 597  ##[ ##25: #H; napply (refl_eq ??)
 598  ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct ??? H)
 599  ##| ##*: #H; napply (instr_mode_destruct ??? H)
 600  ##]
 601 nqed.
 602
 603 nlemma eq_to_eqinstrmode26 : ∀i2.MODE_IX0_and_IMM1 = i2 → eq_instrmode MODE_IX0_and_IMM1 i2 = true.
 604  #t2; ncases t2; nnormalize;
 605  ##[ ##26: #H; napply (refl_eq ??)
 606  ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct ??? H)
 607  ##| ##*: #H; napply (instr_mode_destruct ??? H)
 608  ##]
 609 nqed.
 610
 611 nlemma eq_to_eqinstrmode27 : ∀i2.MODE_IX0p_and_IMM1 = i2 → eq_instrmode MODE_IX0p_and_IMM1 i2 = true.
 612  #t2; ncases t2; nnormalize;
 613  ##[ ##27: #H; napply (refl_eq ??)
 614  ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct ??? H)
 615  ##| ##*: #H; napply (instr_mode_destruct ??? H)
 616  ##]
 617 nqed.
 618
 619 nlemma eq_to_eqinstrmode28 : ∀i2.MODE_IX1_and_IMM1 = i2 → eq_instrmode MODE_IX1_and_IMM1 i2 = true.
 620  #t2; ncases t2; nnormalize;
 621  ##[ ##28: #H; napply (refl_eq ??)
 622  ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct ??? H)
 623  ##| ##*: #H; napply (instr_mode_destruct ??? H)
 624  ##]
 625 nqed.
 626
 627 nlemma eq_to_eqinstrmode29 : ∀i2.MODE_IX1p_and_IMM1 = i2 → eq_instrmode MODE_IX1p_and_IMM1 i2 = true.
 628  #t2; ncases t2; nnormalize;
 629  ##[ ##29: #H; napply (refl_eq ??)
 630  ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct ??? H)
 631  ##| ##*: #H; napply (instr_mode_destruct ??? H)
 632  ##]
 633 nqed.
 634
 635 nlemma eq_to_eqinstrmode30 : ∀i2.MODE_SP1_and_IMM1 = i2 → eq_instrmode MODE_SP1_and_IMM1 i2 = true.
 636  #t2; ncases t2; nnormalize;
 637  ##[ ##30: #H; napply (refl_eq ??)
 638  ##| ##31,32,33,34: #n; #H; napply (instr_mode_destruct ??? H)
 639  ##| ##*: #H; napply (instr_mode_destruct ??? H)
 640  ##]
 641 nqed.
 642
 643 nlemma eq_to_eqinstrmode31 : ∀n1,i2.MODE_DIRn n1 = i2 → eq_instrmode (MODE_DIRn n1) i2 = true.
 644  #n1; #t2; ncases t2;
 645  ##[ ##31: #n2; #H;
 646      nchange with (eq_oct n1 n2 = true);
 647      nrewrite > (instr_mode_destruct_MODE_DIRn ?? H);
 648      nrewrite > (eq_to_eqoct n2 n2 (refl_eq ??));
 649      napply (refl_eq ??)
 650  ##| ##32,33,34: #n; #H; nnormalize; napply (instr_mode_destruct ??? H)
 651  ##| ##*: #H; nnormalize; napply (instr_mode_destruct ??? H)
 652  ##]
 653 nqed.
 654
 655 nlemma eq_to_eqinstrmode32 : ∀n1,i2.MODE_DIRn_and_IMM1 n1 = i2 → eq_instrmode (MODE_DIRn_and_IMM1 n1) i2 = true.
 656  #n1; #t2; ncases t2;
 657  ##[ ##32: #n2; #H;
 658      nchange with (eq_oct n1 n2 = true);
 659      nrewrite > (instr_mode_destruct_MODE_DIRn_and_IMM1 ?? H);
 660      nrewrite > (eq_to_eqoct n2 n2 (refl_eq ??));
 661      napply (refl_eq ??)
 662  ##| ##31,33,34: #n; #H; nnormalize; napply (instr_mode_destruct ??? H)
 663  ##| ##*: #H; nnormalize; napply (instr_mode_destruct ??? H)
 664  ##]
 665 nqed.
 666
 667 nlemma eq_to_eqinstrmode33 : ∀n1,i2.MODE_TNY n1 = i2 → eq_instrmode (MODE_TNY n1) i2 = true.
 668  #n1; #t2; ncases t2;
 669  ##[ ##33: #n2; #H;
 670      nchange with (eq_ex n1 n2 = true);
 671      nrewrite > (instr_mode_destruct_MODE_TNY ?? H);
 672      nrewrite > (eq_to_eqex n2 n2 (refl_eq ??));
 673      napply (refl_eq ??)
 674  ##| ##31,32,34: #n; #H; nnormalize; napply (instr_mode_destruct ??? H)
 675  ##| ##*: #H; nnormalize; napply (instr_mode_destruct ??? H)
 676  ##]
 677 nqed.
 678
 679 nlemma eq_to_eqinstrmode34 : ∀n1,i2.MODE_SRT n1 = i2 → eq_instrmode (MODE_SRT n1) i2 = true.
 680  #n1; #t2; ncases t2;
 681  ##[ ##34: #n2; #H;
 682      nchange with (eq_bitrig n1 n2 = true);
 683      nrewrite > (instr_mode_destruct_MODE_SRT ?? H);
 684      nrewrite > (eq_to_eqbitrig n2 n2 (refl_eq ??));
 685      napply (refl_eq ??)
 686  ##| ##31,32,33: #n; #H; nnormalize; napply (instr_mode_destruct ??? H)
 687  ##| ##*: #H; nnormalize; napply (instr_mode_destruct ??? H)
 688  ##]
 689 nqed.
 690
 691 nlemma eq_to_eqinstrmode : ∀i1,i2.i1 = i2 → eq_instrmode i1 i2 = true.
 692  #i1; ncases i1;
 693  ##[ ##1: napply eq_to_eqinstrmode1 ##| ##2: napply eq_to_eqinstrmode2
 694  ##| ##3: napply eq_to_eqinstrmode3 ##| ##4: napply eq_to_eqinstrmode4
 695  ##| ##5: napply eq_to_eqinstrmode5 ##| ##6: napply eq_to_eqinstrmode6
 696  ##| ##7: napply eq_to_eqinstrmode7 ##| ##8: napply eq_to_eqinstrmode8
 697  ##| ##9: napply eq_to_eqinstrmode9 ##| ##10: napply eq_to_eqinstrmode10
 698  ##| ##11: napply eq_to_eqinstrmode11 ##| ##12: napply eq_to_eqinstrmode12
 699  ##| ##13: napply eq_to_eqinstrmode13 ##| ##14: napply eq_to_eqinstrmode14
 700  ##| ##15: napply eq_to_eqinstrmode15 ##| ##16: napply eq_to_eqinstrmode16
 701  ##| ##17: napply eq_to_eqinstrmode17 ##| ##18: napply eq_to_eqinstrmode18
 702  ##| ##19: napply eq_to_eqinstrmode19 ##| ##20: napply eq_to_eqinstrmode20
 703  ##| ##21: napply eq_to_eqinstrmode21 ##| ##22: napply eq_to_eqinstrmode22
 704  ##| ##23: napply eq_to_eqinstrmode23 ##| ##24: napply eq_to_eqinstrmode24
 705  ##| ##25: napply eq_to_eqinstrmode25 ##| ##26: napply eq_to_eqinstrmode26
 706  ##| ##27: napply eq_to_eqinstrmode27 ##| ##28: napply eq_to_eqinstrmode28
 707  ##| ##29: napply eq_to_eqinstrmode29 ##| ##30: napply eq_to_eqinstrmode30
 708  ##| ##31: napply eq_to_eqinstrmode31 ##| ##32: napply eq_to_eqinstrmode32
 709  ##| ##33: napply eq_to_eqinstrmode33 ##| ##34: napply eq_to_eqinstrmode34
 710  ##]
 711 nqed.