helm/software/matita/contribs/ng_assembly/freescale/opcode_base_lemmas_instrmode1.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* ********************************************************************** *)
  16 (*                          Progetto FreeScale                            *)
  17 (*                                                                        *)
  18 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
  19 (*   Ultima modifica: 05/08/2009                                          *)
  20 (*                                                                        *)
  21 (* ********************************************************************** *)
  22
  23 include "num/oct_lemmas.ma".
  24 include "num/bitrigesim_lemmas.ma".
  25 include "num/exadecim_lemmas.ma".
  26 include "freescale/opcode_base.ma".
  27
  28 (* ********************************************** *)
  29 (* MATTONI BASE PER DEFINIRE LE TABELLE DELLE MCU *)
  30 (* ********************************************** *)
  31
  32 nlemma instrmode_destruct_MODE_DIRn : ∀n1,n2.MODE_DIRn n1 = MODE_DIRn n2 → n1 = n2.
  33  #n1; #n2; #H;
  34  nchange with (match MODE_DIRn n2 with [ MODE_DIRn a ⇒ n1 = a | _ ⇒ False ]);
  35  nrewrite < H;
  36  nnormalize;
  37  napply refl_eq.
  38 nqed.
  39
  40 nlemma instrmode_destruct_MODE_DIRn_and_IMM1 : ∀n1,n2.MODE_DIRn_and_IMM1 n1 = MODE_DIRn_and_IMM1 n2 → n1 = n2.
  41  #n1; #n2; #H;
  42  nchange with (match MODE_DIRn_and_IMM1 n2 with [ MODE_DIRn_and_IMM1 a ⇒ n1 = a | _ ⇒ False ]);
  43  nrewrite < H;
  44  nnormalize;
  45  napply refl_eq.
  46 nqed.
  47
  48 nlemma instrmode_destruct_MODE_TNY : ∀e1,e2.MODE_TNY e1 = MODE_TNY e2 → e1 = e2.
  49  #e1; #e2; #H;
  50  nchange with (match MODE_TNY e2 with [ MODE_TNY a ⇒ e1 = a | _ ⇒ False ]);
  51  nrewrite < H;
  52  nnormalize;
  53  napply refl_eq.
  54 nqed.
  55
  56 nlemma instrmode_destruct_MODE_SRT : ∀t1,t2.MODE_SRT t1 = MODE_SRT t2 → t1 = t2.
  57  #t1; #t2; #H;
  58  nchange with (match MODE_SRT t2 with [ MODE_SRT a ⇒ t1 = a | _ ⇒ False ]);
  59  nrewrite < H;
  60  nnormalize;
  61  napply refl_eq.
  62 nqed.
  63
  64 ndefinition instrmode_destruct_aux ≝
  65 Πi1,i2.ΠP:Prop.i1 = i2 →
  66  match eq_im i1 i2 with [ true ⇒ P → P | false ⇒ P ].
  67
  68 ndefinition instrmode_destruct : instrmode_destruct_aux.
  69  #t1; #t2; #P; #H;
  70  nrewrite < H;
  71  nelim t1;
  72  nnormalize;
  73  ##[ ##31,32,33,34: #sub; nelim sub; nnormalize ##]
  74  napply (λx.x).
  75 nqed.
  76
  77 nlemma symmetric_eqim : symmetricT instr_mode bool eq_im.
  78  #i1; #i2;
  79  ncases i1;
  80  ##[ ##1: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
  81  ##| ##2: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
  82  ##| ##3: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
  83  ##| ##4: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
  84  ##| ##5: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
  85  ##| ##6: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
  86  ##| ##7: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
  87  ##| ##8: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
  88  ##| ##9: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
  89  ##| ##10: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
  90  ##| ##11: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
  91  ##| ##12: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
  92  ##| ##13: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
  93  ##| ##14: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
  94  ##| ##15: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
  95  ##| ##16: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
  96  ##| ##17: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
  97  ##| ##18: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
  98  ##| ##19: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
  99  ##| ##20: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
 100  ##| ##21: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
 101  ##| ##22: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
 102  ##| ##23: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
 103  ##| ##24: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
 104  ##| ##25: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
 105  ##| ##26: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
 106  ##| ##27: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
 107  ##| ##28: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
 108  ##| ##29: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
 109  ##| ##30: ncases i2; nnormalize; ##[ ##31,32,33,34: #n ##] napply refl_eq
 110  ##| ##31: ncases i2; #n1;
 111      ##[ ##31: #n2;
 112                nchange with (eq_oct n2 n1 = eq_oct n1 n2);
 113                nrewrite > (symmetric_eqoct n1 n2);
 114      ##| ##32,33,34: #n2; nnormalize
 115      ##]
 116      nnormalize; napply refl_eq
 117  ##| ##32: ncases i2; #n1;
 118      ##[ ##32: #n2;
 119                nchange with (eq_oct n2 n1 = eq_oct n1 n2);
 120                nrewrite > (symmetric_eqoct n1 n2);
 121      ##| ##31,33,34: #n2; nnormalize
 122      ##]
 123      nnormalize; napply refl_eq
 124  ##| ##33: ncases i2; #n1;
 125      ##[ ##33: #n2;
 126                nchange with (eq_ex n2 n1 = eq_ex n1 n2);
 127                nrewrite > (symmetric_eqex n1 n2);
 128      ##| ##31,32,34: #n2; nnormalize
 129      ##]
 130      nnormalize; napply refl_eq
 131  ##| ##34: ncases i2; #n1;
 132      ##[ ##34: #n2;
 133                nchange with (eq_bit n2 n1 = eq_bit n1 n2);
 134                nrewrite > (symmetric_eqbit n1 n2);
 135      ##| ##31,32,33: #n2; nnormalize
 136      ##]
 137      nnormalize; napply refl_eq
 138  ##]
 139 nqed.
 140
 141 nlemma eqim_to_eq1 : ∀i2.eq_im MODE_INH i2 = true → MODE_INH = i2.
 142  #i2; ncases i2; nnormalize;
 143  ##[ ##1: #H; napply refl_eq
 144  ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
 145  ##| ##*: #H; napply (bool_destruct … H)
 146  ##]
 147 nqed.
 148
 149 nlemma eqim_to_eq2 : ∀i2.eq_im MODE_INHA i2 = true → MODE_INHA = i2.
 150  #i2; ncases i2; nnormalize;
 151  ##[ ##2: #H; napply refl_eq
 152  ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
 153  ##| ##*: #H; napply (bool_destruct … H)
 154  ##]
 155 nqed.
 156
 157 nlemma eqim_to_eq3 : ∀i2.eq_im MODE_INHX i2 = true → MODE_INHX = i2.
 158  #i2; ncases i2; nnormalize;
 159  ##[ ##3: #H; napply refl_eq
 160  ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
 161  ##| ##*: #H; napply (bool_destruct … H)
 162  ##]
 163 nqed.
 164
 165 nlemma eqim_to_eq4 : ∀i2.eq_im MODE_INHH i2 = true → MODE_INHH = i2.
 166  #i2; ncases i2; nnormalize;
 167  ##[ ##4: #H; napply refl_eq
 168  ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
 169  ##| ##*: #H; napply (bool_destruct … H)
 170  ##]
 171 nqed.
 172
 173 nlemma eqim_to_eq5 : ∀i2.eq_im MODE_INHX0ADD i2 = true → MODE_INHX0ADD = i2.
 174  #i2; ncases i2; nnormalize;
 175  ##[ ##5: #H; napply refl_eq
 176  ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
 177  ##| ##*: #H; napply (bool_destruct … H)
 178  ##]
 179 nqed.
 180
 181 nlemma eqim_to_eq6 : ∀i2.eq_im MODE_INHX1ADD i2 = true → MODE_INHX1ADD = i2.
 182  #i2; ncases i2; nnormalize;
 183  ##[ ##6: #H; napply refl_eq
 184  ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
 185  ##| ##*: #H; napply (bool_destruct … H)
 186  ##]
 187 nqed.
 188
 189 nlemma eqim_to_eq7 : ∀i2.eq_im MODE_INHX2ADD i2 = true → MODE_INHX2ADD = i2.
 190  #i2; ncases i2; nnormalize;
 191  ##[ ##7: #H; napply refl_eq
 192  ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
 193  ##| ##*: #H; napply (bool_destruct … H)
 194  ##]
 195 nqed.
 196
 197 nlemma eqim_to_eq8 : ∀i2.eq_im MODE_IMM1 i2 = true → MODE_IMM1 = i2.
 198  #i2; ncases i2; nnormalize;
 199  ##[ ##8: #H; napply refl_eq
 200  ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
 201  ##| ##*: #H; napply (bool_destruct … H)
 202  ##]
 203 nqed.
 204
 205 nlemma eqim_to_eq9 : ∀i2.eq_im MODE_IMM1EXT i2 = true → MODE_IMM1EXT = i2.
 206  #i2; ncases i2; nnormalize;
 207  ##[ ##9: #H; napply refl_eq
 208  ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
 209  ##| ##*: #H; napply (bool_destruct … H)
 210  ##]
 211 nqed.
 212
 213 nlemma eqim_to_eq10 : ∀i2.eq_im MODE_IMM2 i2 = true → MODE_IMM2 = i2.
 214  #i2; ncases i2; nnormalize;
 215  ##[ ##10: #H; napply refl_eq
 216  ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
 217  ##| ##*: #H; napply (bool_destruct … H)
 218  ##]
 219 nqed.
 220
 221 nlemma eqim_to_eq11 : ∀i2.eq_im MODE_DIR1 i2 = true → MODE_DIR1 = i2.
 222  #i2; ncases i2; nnormalize;
 223  ##[ ##11: #H; napply refl_eq
 224  ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
 225  ##| ##*: #H; napply (bool_destruct … H)
 226  ##]
 227 nqed.
 228
 229 nlemma eqim_to_eq12 : ∀i2.eq_im MODE_DIR2 i2 = true → MODE_DIR2 = i2.
 230  #i2; ncases i2; nnormalize;
 231  ##[ ##12: #H; napply refl_eq
 232  ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
 233  ##| ##*: #H; napply (bool_destruct … H)
 234  ##]
 235 nqed.
 236
 237 nlemma eqim_to_eq13 : ∀i2.eq_im MODE_IX0 i2 = true → MODE_IX0 = i2.
 238  #i2; ncases i2; nnormalize;
 239  ##[ ##13: #H; napply refl_eq
 240  ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
 241  ##| ##*: #H; napply (bool_destruct … H)
 242  ##]
 243 nqed.
 244
 245 nlemma eqim_to_eq14 : ∀i2.eq_im MODE_IX1 i2 = true → MODE_IX1 = i2.
 246  #i2; ncases i2; nnormalize;
 247  ##[ ##14: #H; napply refl_eq
 248  ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
 249  ##| ##*: #H; napply (bool_destruct … H)
 250  ##]
 251 nqed.
 252
 253 nlemma eqim_to_eq15 : ∀i2.eq_im MODE_IX2 i2 = true → MODE_IX2 = i2.
 254  #i2; ncases i2; nnormalize;
 255  ##[ ##15: #H; napply refl_eq
 256  ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
 257  ##| ##*: #H; napply (bool_destruct … H)
 258  ##]
 259 nqed.
 260
 261 nlemma eqim_to_eq16 : ∀i2.eq_im MODE_SP1 i2 = true → MODE_SP1 = i2.
 262  #i2; ncases i2; nnormalize;
 263  ##[ ##16: #H; napply refl_eq
 264  ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
 265  ##| ##*: #H; napply (bool_destruct … H)
 266  ##]
 267 nqed.
 268
 269 nlemma eqim_to_eq17 : ∀i2.eq_im MODE_SP2 i2 = true → MODE_SP2 = i2.
 270  #i2; ncases i2; nnormalize;
 271  ##[ ##17: #H; napply refl_eq
 272  ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
 273  ##| ##*: #H; napply (bool_destruct … H)
 274  ##]
 275 nqed.
 276
 277 nlemma eqim_to_eq18 : ∀i2.eq_im MODE_DIR1_to_DIR1 i2 = true → MODE_DIR1_to_DIR1 = i2.
 278  #i2; ncases i2; nnormalize;
 279  ##[ ##18: #H; napply refl_eq
 280  ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
 281  ##| ##*: #H; napply (bool_destruct … H)
 282  ##]
 283 nqed.
 284
 285 nlemma eqim_to_eq19 : ∀i2.eq_im MODE_IMM1_to_DIR1 i2 = true → MODE_IMM1_to_DIR1 = i2.
 286  #i2; ncases i2; nnormalize;
 287  ##[ ##19: #H; napply refl_eq
 288  ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
 289  ##| ##*: #H; napply (bool_destruct … H)
 290  ##]
 291 nqed.
 292
 293 nlemma eqim_to_eq20 : ∀i2.eq_im MODE_IX0p_to_DIR1 i2 = true → MODE_IX0p_to_DIR1 = i2.
 294  #i2; ncases i2; nnormalize;
 295  ##[ ##20: #H; napply refl_eq
 296  ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
 297  ##| ##*: #H; napply (bool_destruct … H)
 298  ##]
 299 nqed.
 300
 301 nlemma eqim_to_eq21 : ∀i2.eq_im MODE_DIR1_to_IX0p i2 = true → MODE_DIR1_to_IX0p = i2.
 302  #i2; ncases i2; nnormalize;
 303  ##[ ##21: #H; napply refl_eq
 304  ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
 305  ##| ##*: #H; napply (bool_destruct … H)
 306  ##]
 307 nqed.
 308
 309 nlemma eqim_to_eq22 : ∀i2.eq_im MODE_INHA_and_IMM1 i2 = true → MODE_INHA_and_IMM1 = i2.
 310  #i2; ncases i2; nnormalize;
 311  ##[ ##22: #H; napply refl_eq
 312  ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
 313  ##| ##*: #H; napply (bool_destruct … H)
 314  ##]
 315 nqed.
 316
 317 nlemma eqim_to_eq23 : ∀i2.eq_im MODE_INHX_and_IMM1 i2 = true → MODE_INHX_and_IMM1 = i2.
 318  #i2; ncases i2; nnormalize;
 319  ##[ ##23: #H; napply refl_eq
 320  ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
 321  ##| ##*: #H; napply (bool_destruct … H)
 322  ##]
 323 nqed.
 324
 325 nlemma eqim_to_eq24 : ∀i2.eq_im MODE_IMM1_and_IMM1 i2 = true → MODE_IMM1_and_IMM1 = i2.
 326  #i2; ncases i2; nnormalize;
 327  ##[ ##24: #H; napply refl_eq
 328  ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
 329  ##| ##*: #H; napply (bool_destruct … H)
 330  ##]
 331 nqed.
 332
 333 nlemma eqim_to_eq25 : ∀i2.eq_im MODE_DIR1_and_IMM1 i2 = true → MODE_DIR1_and_IMM1 = i2.
 334  #i2; ncases i2; nnormalize;
 335  ##[ ##25: #H; napply refl_eq
 336  ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
 337  ##| ##*: #H; napply (bool_destruct … H)
 338  ##]
 339 nqed.
 340
 341 nlemma eqim_to_eq26 : ∀i2.eq_im MODE_IX0_and_IMM1 i2 = true → MODE_IX0_and_IMM1 = i2.
 342  #i2; ncases i2; nnormalize;
 343  ##[ ##26: #H; napply refl_eq
 344  ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
 345  ##| ##*: #H; napply (bool_destruct … H)
 346  ##]
 347 nqed.
 348
 349 nlemma eqim_to_eq27 : ∀i2.eq_im MODE_IX0p_and_IMM1 i2 = true → MODE_IX0p_and_IMM1 = i2.
 350  #i2; ncases i2; nnormalize;
 351  ##[ ##27: #H; napply refl_eq
 352  ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
 353  ##| ##*: #H; napply (bool_destruct … H)
 354  ##]
 355 nqed.
 356
 357 nlemma eqim_to_eq28 : ∀i2.eq_im MODE_IX1_and_IMM1 i2 = true → MODE_IX1_and_IMM1 = i2.
 358  #i2; ncases i2; nnormalize;
 359  ##[ ##28: #H; napply refl_eq
 360  ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
 361  ##| ##*: #H; napply (bool_destruct … H)
 362  ##]
 363 nqed.
 364
 365 nlemma eqim_to_eq29 : ∀i2.eq_im MODE_IX1p_and_IMM1 i2 = true → MODE_IX1p_and_IMM1 = i2.
 366  #i2; ncases i2; nnormalize;
 367  ##[ ##29: #H; napply refl_eq
 368  ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
 369  ##| ##*: #H; napply (bool_destruct … H)
 370  ##]
 371 nqed.
 372
 373 nlemma eqim_to_eq30 : ∀i2.eq_im MODE_SP1_and_IMM1 i2 = true → MODE_SP1_and_IMM1 = i2.
 374  #i2; ncases i2; nnormalize;
 375  ##[ ##30: #H; napply refl_eq
 376  ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
 377  ##| ##*: #H; napply (bool_destruct … H)
 378  ##]
 379 nqed.
 380
 381 nlemma eqim_to_eq31 : ∀n1,i2.eq_im (MODE_DIRn n1) i2 = true → MODE_DIRn n1 = i2.
 382  #n1; #i2; ncases i2;
 383  ##[ ##31: #n2; #H;
 384      nchange in H:(%) with (eq_oct n1 n2 = true);
 385      nrewrite > (eqoct_to_eq … H);
 386      napply refl_eq
 387  ##| ##32,33,34: nnormalize; #n2; #H; napply (bool_destruct … H)
 388  ##| ##*: nnormalize; #H; napply (bool_destruct … H)
 389  ##]
 390 nqed.
 391
 392 nlemma eqim_to_eq32 : ∀n1,i2.eq_im (MODE_DIRn_and_IMM1 n1) i2 = true → MODE_DIRn_and_IMM1 n1 = i2.
 393  #n1; #i2; ncases i2;
 394  ##[ ##32: #n2; #H;
 395      nchange in H:(%) with (eq_oct n1 n2 = true);
 396      nrewrite > (eqoct_to_eq … H);
 397      napply refl_eq
 398  ##| ##31,33,34: nnormalize; #n2; #H; napply (bool_destruct … H)
 399  ##| ##*: nnormalize; #H; napply (bool_destruct … H)
 400  ##]
 401 nqed.
 402
 403 nlemma eqim_to_eq33 : ∀n1,i2.eq_im (MODE_TNY n1) i2 = true → MODE_TNY n1 = i2.
 404  #n1; #i2; ncases i2;
 405  ##[ ##33: #n2; #H;
 406      nchange in H:(%) with (eq_ex n1 n2 = true);
 407      nrewrite > (eqex_to_eq … H);
 408      napply refl_eq
 409  ##| ##31,32,34: nnormalize; #n2; #H; napply (bool_destruct … H)
 410  ##| ##*: nnormalize; #H; napply (bool_destruct … H)
 411  ##]
 412 nqed.
 413
 414 nlemma eqim_to_eq34 : ∀n1,i2.eq_im (MODE_SRT n1) i2 = true → MODE_SRT n1 = i2.
 415  #n1; #i2; ncases i2;
 416  ##[ ##34: #n2; #H;
 417      nchange in H:(%) with (eq_bit n1 n2 = true);
 418      nrewrite > (eqbit_to_eq … H);
 419      napply refl_eq
 420  ##| ##31,32,33: nnormalize; #n2; #H; napply (bool_destruct … H)
 421  ##| ##*: nnormalize; #H; napply (bool_destruct … H)
 422  ##]
 423 nqed.
 424
 425 nlemma eqim_to_eq : ∀i1,i2.eq_im i1 i2 = true → i1 = i2.
 426  #i1; ncases i1;
 427  ##[ ##1: napply eqim_to_eq1 ##| ##2: napply eqim_to_eq2
 428  ##| ##3: napply eqim_to_eq3 ##| ##4: napply eqim_to_eq4
 429  ##| ##5: napply eqim_to_eq5 ##| ##6: napply eqim_to_eq6
 430  ##| ##7: napply eqim_to_eq7 ##| ##8: napply eqim_to_eq8
 431  ##| ##9: napply eqim_to_eq9 ##| ##10: napply eqim_to_eq10
 432  ##| ##11: napply eqim_to_eq11 ##| ##12: napply eqim_to_eq12
 433  ##| ##13: napply eqim_to_eq13 ##| ##14: napply eqim_to_eq14
 434  ##| ##15: napply eqim_to_eq15 ##| ##16: napply eqim_to_eq16
 435  ##| ##17: napply eqim_to_eq17 ##| ##18: napply eqim_to_eq18
 436  ##| ##19: napply eqim_to_eq19 ##| ##20: napply eqim_to_eq20
 437  ##| ##21: napply eqim_to_eq21 ##| ##22: napply eqim_to_eq22
 438  ##| ##23: napply eqim_to_eq23 ##| ##24: napply eqim_to_eq24
 439  ##| ##25: napply eqim_to_eq25 ##| ##26: napply eqim_to_eq26
 440  ##| ##27: napply eqim_to_eq27 ##| ##28: napply eqim_to_eq28
 441  ##| ##29: napply eqim_to_eq29 ##| ##30: napply eqim_to_eq30
 442  ##| ##31: napply eqim_to_eq31 ##| ##32: napply eqim_to_eq32
 443  ##| ##33: napply eqim_to_eq33 ##| ##34: napply eqim_to_eq34
 444  ##]
 445 nqed.
 446
 447 nlemma eq_to_eqim1 : ∀i2.MODE_INH = i2 → eq_im MODE_INH i2 = true.
 448  #t2; ncases t2; nnormalize;
 449  ##[ ##1: #H; napply refl_eq
 450  ##| ##31,32,33,34: #n; #H; napply (instrmode_destruct … H)
 451  ##| ##*: #H; napply (instrmode_destruct … H)
 452  ##]
 453 nqed.
 454
 455 nlemma eq_to_eqim2 : ∀i2.MODE_INHA = i2 → eq_im MODE_INHA i2 = true.
 456  #t2; ncases t2; nnormalize;
 457  ##[ ##2: #H; napply refl_eq
 458  ##| ##31,32,33,34: #n; #H; napply (instrmode_destruct … H)
 459  ##| ##*: #H; napply (instrmode_destruct … H)
 460  ##]
 461 nqed.
 462
 463 nlemma eq_to_eqim3 : ∀i2.MODE_INHX = i2 → eq_im MODE_INHX i2 = true.
 464  #t2; ncases t2; nnormalize;
 465  ##[ ##3: #H; napply refl_eq
 466  ##| ##31,32,33,34: #n; #H; napply (instrmode_destruct … H)
 467  ##| ##*: #H; napply (instrmode_destruct … H)
 468  ##]
 469 nqed.
 470
 471 nlemma eq_to_eqim4 : ∀i2.MODE_INHH = i2 → eq_im MODE_INHH i2 = true.
 472  #t2; ncases t2; nnormalize;
 473  ##[ ##4: #H; napply refl_eq
 474  ##| ##31,32,33,34: #n; #H; napply (instrmode_destruct … H)
 475  ##| ##*: #H; napply (instrmode_destruct … H)
 476  ##]
 477 nqed.
 478
 479 nlemma eq_to_eqim5 : ∀i2.MODE_INHX0ADD = i2 → eq_im MODE_INHX0ADD i2 = true.
 480  #t2; ncases t2; nnormalize;
 481  ##[ ##5: #H; napply refl_eq
 482  ##| ##31,32,33,34: #n; #H; napply (instrmode_destruct … H)
 483  ##| ##*: #H; napply (instrmode_destruct … H)
 484  ##]
 485 nqed.
 486
 487 nlemma eq_to_eqim6 : ∀i2.MODE_INHX1ADD = i2 → eq_im MODE_INHX1ADD i2 = true.
 488  #t2; ncases t2; nnormalize;
 489  ##[ ##6: #H; napply refl_eq
 490  ##| ##31,32,33,34: #n; #H; napply (instrmode_destruct … H)
 491  ##| ##*: #H; napply (instrmode_destruct … H)
 492  ##]
 493 nqed.
 494
 495 nlemma eq_to_eqim7 : ∀i2.MODE_INHX2ADD = i2 → eq_im MODE_INHX2ADD i2 = true.
 496  #t2; ncases t2; nnormalize;
 497  ##[ ##7: #H; napply refl_eq
 498  ##| ##31,32,33,34: #n; #H; napply (instrmode_destruct … H)
 499  ##| ##*: #H; napply (instrmode_destruct … H)
 500  ##]
 501 nqed.
 502
 503 nlemma eq_to_eqim8 : ∀i2.MODE_IMM1 = i2 → eq_im MODE_IMM1 i2 = true.
 504  #t2; ncases t2; nnormalize;
 505  ##[ ##8: #H; napply refl_eq
 506  ##| ##31,32,33,34: #n; #H; napply (instrmode_destruct … H)
 507  ##| ##*: #H; napply (instrmode_destruct … H)
 508  ##]
 509 nqed.
 510
 511 nlemma eq_to_eqim9 : ∀i2.MODE_IMM1EXT = i2 → eq_im MODE_IMM1EXT i2 = true.
 512  #t2; ncases t2; nnormalize;
 513  ##[ ##9: #H; napply refl_eq
 514  ##| ##31,32,33,34: #n; #H; napply (instrmode_destruct … H)
 515  ##| ##*: #H; napply (instrmode_destruct … H)
 516  ##]
 517 nqed.
 518
 519 nlemma eq_to_eqim10 : ∀i2.MODE_IMM2 = i2 → eq_im MODE_IMM2 i2 = true.
 520  #t2; ncases t2; nnormalize;
 521  ##[ ##10: #H; napply refl_eq
 522  ##| ##31,32,33,34: #n; #H; napply (instrmode_destruct … H)
 523  ##| ##*: #H; napply (instrmode_destruct … H)
 524  ##]
 525 nqed.
 526
 527 nlemma eq_to_eqim11 : ∀i2.MODE_DIR1 = i2 → eq_im MODE_DIR1 i2 = true.
 528  #t2; ncases t2; nnormalize;
 529  ##[ ##11: #H; napply refl_eq
 530  ##| ##31,32,33,34: #n; #H; napply (instrmode_destruct … H)
 531  ##| ##*: #H; napply (instrmode_destruct … H)
 532  ##]
 533 nqed.
 534
 535 nlemma eq_to_eqim12 : ∀i2.MODE_DIR2 = i2 → eq_im MODE_DIR2 i2 = true.
 536  #t2; ncases t2; nnormalize;
 537  ##[ ##12: #H; napply refl_eq
 538  ##| ##31,32,33,34: #n; #H; napply (instrmode_destruct … H)
 539  ##| ##*: #H; napply (instrmode_destruct … H)
 540  ##]
 541 nqed.
 542
 543 nlemma eq_to_eqim13 : ∀i2.MODE_IX0 = i2 → eq_im MODE_IX0 i2 = true.
 544  #t2; ncases t2; nnormalize;
 545  ##[ ##13: #H; napply refl_eq
 546  ##| ##31,32,33,34: #n; #H; napply (instrmode_destruct … H)
 547  ##| ##*: #H; napply (instrmode_destruct … H)
 548  ##]
 549 nqed.
 550
 551 nlemma eq_to_eqim14 : ∀i2.MODE_IX1 = i2 → eq_im MODE_IX1 i2 = true.
 552  #t2; ncases t2; nnormalize;
 553  ##[ ##14: #H; napply refl_eq
 554  ##| ##31,32,33,34: #n; #H; napply (instrmode_destruct … H)
 555  ##| ##*: #H; napply (instrmode_destruct … H)
 556  ##]
 557 nqed.
 558
 559 nlemma eq_to_eqim15 : ∀i2.MODE_IX2 = i2 → eq_im MODE_IX2 i2 = true.
 560  #t2; ncases t2; nnormalize;
 561  ##[ ##15: #H; napply refl_eq
 562  ##| ##31,32,33,34: #n; #H; napply (instrmode_destruct … H)
 563  ##| ##*: #H; napply (instrmode_destruct … H)
 564  ##]
 565 nqed.
 566
 567 nlemma eq_to_eqim16 : ∀i2.MODE_SP1 = i2 → eq_im MODE_SP1 i2 = true.
 568  #t2; ncases t2; nnormalize;
 569  ##[ ##16: #H; napply refl_eq
 570  ##| ##31,32,33,34: #n; #H; napply (instrmode_destruct … H)
 571  ##| ##*: #H; napply (instrmode_destruct … H)
 572  ##]
 573 nqed.
 574
 575 nlemma eq_to_eqim17 : ∀i2.MODE_SP2 = i2 → eq_im MODE_SP2 i2 = true.
 576  #t2; ncases t2; nnormalize;
 577  ##[ ##17: #H; napply refl_eq
 578  ##| ##31,32,33,34: #n; #H; napply (instrmode_destruct … H)
 579  ##| ##*: #H; napply (instrmode_destruct … H)
 580  ##]
 581 nqed.
 582
 583 nlemma eq_to_eqim18 : ∀i2.MODE_DIR1_to_DIR1 = i2 → eq_im MODE_DIR1_to_DIR1 i2 = true.
 584  #t2; ncases t2; nnormalize;
 585  ##[ ##18: #H; napply refl_eq
 586  ##| ##31,32,33,34: #n; #H; napply (instrmode_destruct … H)
 587  ##| ##*: #H; napply (instrmode_destruct … H)
 588  ##]
 589 nqed.
 590
 591 nlemma eq_to_eqim19 : ∀i2.MODE_IMM1_to_DIR1 = i2 → eq_im MODE_IMM1_to_DIR1 i2 = true.
 592  #t2; ncases t2; nnormalize;
 593  ##[ ##19: #H; napply refl_eq
 594  ##| ##31,32,33,34: #n; #H; napply (instrmode_destruct … H)
 595  ##| ##*: #H; napply (instrmode_destruct … H)
 596  ##]
 597 nqed.
 598
 599 nlemma eq_to_eqim20 : ∀i2.MODE_IX0p_to_DIR1 = i2 → eq_im MODE_IX0p_to_DIR1 i2 = true.
 600  #t2; ncases t2; nnormalize;
 601  ##[ ##20: #H; napply refl_eq
 602  ##| ##31,32,33,34: #n; #H; napply (instrmode_destruct … H)
 603  ##| ##*: #H; napply (instrmode_destruct … H)
 604  ##]
 605 nqed.
 606
 607 nlemma eq_to_eqim21 : ∀i2.MODE_DIR1_to_IX0p = i2 → eq_im MODE_DIR1_to_IX0p i2 = true.
 608  #t2; ncases t2; nnormalize;
 609  ##[ ##21: #H; napply refl_eq
 610  ##| ##31,32,33,34: #n; #H; napply (instrmode_destruct … H)
 611  ##| ##*: #H; napply (instrmode_destruct … H)
 612  ##]
 613 nqed.
 614
 615 nlemma eq_to_eqim22 : ∀i2.MODE_INHA_and_IMM1 = i2 → eq_im MODE_INHA_and_IMM1 i2 = true.
 616  #t2; ncases t2; nnormalize;
 617  ##[ ##22: #H; napply refl_eq
 618  ##| ##31,32,33,34: #n; #H; napply (instrmode_destruct … H)
 619  ##| ##*: #H; napply (instrmode_destruct … H)
 620  ##]
 621 nqed.
 622
 623 nlemma eq_to_eqim23 : ∀i2.MODE_INHX_and_IMM1 = i2 → eq_im MODE_INHX_and_IMM1 i2 = true.
 624  #t2; ncases t2; nnormalize;
 625  ##[ ##23: #H; napply refl_eq
 626  ##| ##31,32,33,34: #n; #H; napply (instrmode_destruct … H)
 627  ##| ##*: #H; napply (instrmode_destruct … H)
 628  ##]
 629 nqed.
 630
 631 nlemma eq_to_eqim24 : ∀i2.MODE_IMM1_and_IMM1 = i2 → eq_im MODE_IMM1_and_IMM1 i2 = true.
 632  #t2; ncases t2; nnormalize;
 633  ##[ ##24: #H; napply refl_eq
 634  ##| ##31,32,33,34: #n; #H; napply (instrmode_destruct … H)
 635  ##| ##*: #H; napply (instrmode_destruct … H)
 636  ##]
 637 nqed.
 638
 639 nlemma eq_to_eqim25 : ∀i2.MODE_DIR1_and_IMM1 = i2 → eq_im MODE_DIR1_and_IMM1 i2 = true.
 640  #t2; ncases t2; nnormalize;
 641  ##[ ##25: #H; napply refl_eq
 642  ##| ##31,32,33,34: #n; #H; napply (instrmode_destruct … H)
 643  ##| ##*: #H; napply (instrmode_destruct … H)
 644  ##]
 645 nqed.
 646
 647 nlemma eq_to_eqim26 : ∀i2.MODE_IX0_and_IMM1 = i2 → eq_im MODE_IX0_and_IMM1 i2 = true.
 648  #t2; ncases t2; nnormalize;
 649  ##[ ##26: #H; napply refl_eq
 650  ##| ##31,32,33,34: #n; #H; napply (instrmode_destruct … H)
 651  ##| ##*: #H; napply (instrmode_destruct … H)
 652  ##]
 653 nqed.
 654
 655 nlemma eq_to_eqim27 : ∀i2.MODE_IX0p_and_IMM1 = i2 → eq_im MODE_IX0p_and_IMM1 i2 = true.
 656  #t2; ncases t2; nnormalize;
 657  ##[ ##27: #H; napply refl_eq
 658  ##| ##31,32,33,34: #n; #H; napply (instrmode_destruct … H)
 659  ##| ##*: #H; napply (instrmode_destruct … H)
 660  ##]
 661 nqed.
 662
 663 nlemma eq_to_eqim28 : ∀i2.MODE_IX1_and_IMM1 = i2 → eq_im MODE_IX1_and_IMM1 i2 = true.
 664  #t2; ncases t2; nnormalize;
 665  ##[ ##28: #H; napply refl_eq
 666  ##| ##31,32,33,34: #n; #H; napply (instrmode_destruct … H)
 667  ##| ##*: #H; napply (instrmode_destruct … H)
 668  ##]
 669 nqed.
 670
 671 nlemma eq_to_eqim29 : ∀i2.MODE_IX1p_and_IMM1 = i2 → eq_im MODE_IX1p_and_IMM1 i2 = true.
 672  #t2; ncases t2; nnormalize;
 673  ##[ ##29: #H; napply refl_eq
 674  ##| ##31,32,33,34: #n; #H; napply (instrmode_destruct … H)
 675  ##| ##*: #H; napply (instrmode_destruct … H)
 676  ##]
 677 nqed.
 678
 679 nlemma eq_to_eqim30 : ∀i2.MODE_SP1_and_IMM1 = i2 → eq_im MODE_SP1_and_IMM1 i2 = true.
 680  #t2; ncases t2; nnormalize;
 681  ##[ ##30: #H; napply refl_eq
 682  ##| ##31,32,33,34: #n; #H; napply (instrmode_destruct … H)
 683  ##| ##*: #H; napply (instrmode_destruct … H)
 684  ##]
 685 nqed.
 686
 687 nlemma eq_to_eqim31 : ∀n1,i2.MODE_DIRn n1 = i2 → eq_im (MODE_DIRn n1) i2 = true.
 688  #n1; #t2; ncases t2;
 689  ##[ ##31: #n2; #H;
 690      nchange with (eq_oct n1 n2 = true);
 691      nrewrite > (instrmode_destruct_MODE_DIRn n1 n2 H);
 692      nrewrite > (eq_to_eqoct n2 n2 (refl_eq …));
 693      napply refl_eq
 694  ##| ##32,33,34: #n; #H; nnormalize; napply (instrmode_destruct … H)
 695  ##| ##*: #H; nnormalize; napply (instrmode_destruct … H)
 696  ##]
 697 nqed.
 698
 699 nlemma eq_to_eqim32 : ∀n1,i2.MODE_DIRn_and_IMM1 n1 = i2 → eq_im (MODE_DIRn_and_IMM1 n1) i2 = true.
 700  #n1; #t2; ncases t2;
 701  ##[ ##32: #n2; #H;
 702      nchange with (eq_oct n1 n2 = true);
 703      nrewrite > (instrmode_destruct_MODE_DIRn_and_IMM1 … H);
 704      nrewrite > (eq_to_eqoct n2 n2 (refl_eq …));
 705      napply refl_eq
 706  ##| ##31,33,34: #n; #H; nnormalize; napply (instrmode_destruct … H)
 707  ##| ##*: #H; nnormalize; napply (instrmode_destruct … H)
 708  ##]
 709 nqed.
 710
 711 nlemma eq_to_eqim33 : ∀n1,i2.MODE_TNY n1 = i2 → eq_im (MODE_TNY n1) i2 = true.
 712  #n1; #t2; ncases t2;
 713  ##[ ##33: #n2; #H;
 714      nchange with (eq_ex n1 n2 = true);
 715      nrewrite > (instrmode_destruct_MODE_TNY … H);
 716      nrewrite > (eq_to_eqex n2 n2 (refl_eq …));
 717      napply refl_eq
 718  ##| ##31,32,34: #n; #H; nnormalize; napply (instrmode_destruct … H)
 719  ##| ##*: #H; nnormalize; napply (instrmode_destruct … H)
 720  ##]
 721 nqed.
 722
 723 nlemma eq_to_eqim34 : ∀n1,i2.MODE_SRT n1 = i2 → eq_im (MODE_SRT n1) i2 = true.
 724  #n1; #t2; ncases t2;
 725  ##[ ##34: #n2; #H;
 726      nchange with (eq_bit n1 n2 = true);
 727      nrewrite > (instrmode_destruct_MODE_SRT … H);
 728      nrewrite > (eq_to_eqbit n2 n2 (refl_eq …));
 729      napply refl_eq
 730  ##| ##31,32,33: #n; #H; nnormalize; napply (instrmode_destruct … H)
 731  ##| ##*: #H; nnormalize; napply (instrmode_destruct … H)
 732  ##]
 733 nqed.
 734
 735 nlemma eq_to_eqim : ∀i1,i2.i1 = i2 → eq_im i1 i2 = true.
 736  #i1; ncases i1;
 737  ##[ ##1: napply eq_to_eqim1 ##| ##2: napply eq_to_eqim2
 738  ##| ##3: napply eq_to_eqim3 ##| ##4: napply eq_to_eqim4
 739  ##| ##5: napply eq_to_eqim5 ##| ##6: napply eq_to_eqim6
 740  ##| ##7: napply eq_to_eqim7 ##| ##8: napply eq_to_eqim8
 741  ##| ##9: napply eq_to_eqim9 ##| ##10: napply eq_to_eqim10
 742  ##| ##11: napply eq_to_eqim11 ##| ##12: napply eq_to_eqim12
 743  ##| ##13: napply eq_to_eqim13 ##| ##14: napply eq_to_eqim14
 744  ##| ##15: napply eq_to_eqim15 ##| ##16: napply eq_to_eqim16
 745  ##| ##17: napply eq_to_eqim17 ##| ##18: napply eq_to_eqim18
 746  ##| ##19: napply eq_to_eqim19 ##| ##20: napply eq_to_eqim20
 747  ##| ##21: napply eq_to_eqim21 ##| ##22: napply eq_to_eqim22
 748  ##| ##23: napply eq_to_eqim23 ##| ##24: napply eq_to_eqim24
 749  ##| ##25: napply eq_to_eqim25 ##| ##26: napply eq_to_eqim26
 750  ##| ##27: napply eq_to_eqim27 ##| ##28: napply eq_to_eqim28
 751  ##| ##29: napply eq_to_eqim29 ##| ##30: napply eq_to_eqim30
 752  ##| ##31: napply eq_to_eqim31 ##| ##32: napply eq_to_eqim32
 753  ##| ##33: napply eq_to_eqim33 ##| ##34: napply eq_to_eqim34
 754  ##]
 755 nqed.