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: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
  19 (*   Ultima modifica: 05/08/2009                                          *)
  20 (*                                                                        *)
  21 (* ********************************************************************** *)
  22
  23 include "freescale/opcode_base_lemmas_instrmode1.ma".
  24
  25 (* ********************************************** *)
  26 (* MATTONI BASE PER DEFINIRE LE TABELLE DELLE MCU *)
  27 (* ********************************************** *)
  28
  29 nlemma decidable_im1 : ∀x:instr_mode.decidable (MODE_INH = x).
  30  #x; nnormalize; nelim x;
  31  ##[ ##1: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
  32  ##| ##31,32,33,34: #n; ##]
  33  ##[ ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (instrmode_destruct … H) ##]
  34 nqed.
  35
  36 nlemma decidable_im2 : ∀x:instr_mode.decidable (MODE_INHA = x).
  37  #x; nnormalize; nelim x;
  38  ##[ ##2: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
  39  ##| ##31,32,33,34: #n; ##]
  40  ##[ ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (instrmode_destruct … H) ##]
  41 nqed.
  42
  43 nlemma decidable_im3 : ∀x:instr_mode.decidable (MODE_INHX = x).
  44  #x; nnormalize; nelim x;
  45  ##[ ##3: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
  46  ##| ##31,32,33,34: #n; ##]
  47  ##[ ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (instrmode_destruct … H) ##]
  48 nqed.
  49
  50 nlemma decidable_im4 : ∀x:instr_mode.decidable (MODE_INHH = x).
  51  #x; nnormalize; nelim x;
  52  ##[ ##4: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
  53  ##| ##31,32,33,34: #n; ##]
  54  ##[ ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (instrmode_destruct … H) ##]
  55 nqed.
  56
  57 nlemma decidable_im5 : ∀x:instr_mode.decidable (MODE_INHX0ADD = x).
  58  #x; nnormalize; nelim x;
  59  ##[ ##5: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
  60  ##| ##31,32,33,34: #n; ##]
  61  ##[ ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (instrmode_destruct … H) ##]
  62 nqed.
  63
  64 nlemma decidable_im6 : ∀x:instr_mode.decidable (MODE_INHX1ADD = x).
  65  #x; nnormalize; nelim x;
  66  ##[ ##6: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
  67  ##| ##31,32,33,34: #n; ##]
  68  ##[ ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (instrmode_destruct … H) ##]
  69 nqed.
  70
  71 nlemma decidable_im7 : ∀x:instr_mode.decidable (MODE_INHX2ADD = x).
  72  #x; nnormalize; nelim x;
  73  ##[ ##7: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
  74  ##| ##31,32,33,34: #n; ##]
  75  ##[ ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (instrmode_destruct … H) ##]
  76 nqed.
  77
  78 nlemma decidable_im8 : ∀x:instr_mode.decidable (MODE_IMM1 = x).
  79  #x; nnormalize; nelim x;
  80  ##[ ##8: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
  81  ##| ##31,32,33,34: #n; ##]
  82  ##[ ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (instrmode_destruct … H) ##]
  83 nqed.
  84
  85 nlemma decidable_im9 : ∀x:instr_mode.decidable (MODE_IMM1EXT = x).
  86  #x; nnormalize; nelim x;
  87  ##[ ##9: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
  88  ##| ##31,32,33,34: #n; ##]
  89  ##[ ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (instrmode_destruct … H) ##]
  90 nqed.
  91
  92 nlemma decidable_im10 : ∀x:instr_mode.decidable (MODE_IMM2 = x).
  93  #x; nnormalize; nelim x;
  94  ##[ ##10: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
  95  ##| ##31,32,33,34: #n; ##]
  96  ##[ ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (instrmode_destruct … H) ##]
  97 nqed.
  98
  99 nlemma decidable_im11 : ∀x:instr_mode.decidable (MODE_DIR1 = x).
 100  #x; nnormalize; nelim x;
 101  ##[ ##11: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
 102  ##| ##31,32,33,34: #n; ##]
 103  ##[ ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (instrmode_destruct … H) ##]
 104 nqed.
 105
 106 nlemma decidable_im12 : ∀x:instr_mode.decidable (MODE_DIR2 = x).
 107  #x; nnormalize; nelim x;
 108  ##[ ##12: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
 109  ##| ##31,32,33,34: #n; ##]
 110  ##[ ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (instrmode_destruct … H) ##]
 111 nqed.
 112
 113 nlemma decidable_im13 : ∀x:instr_mode.decidable (MODE_IX0 = x).
 114  #x; nnormalize; nelim x;
 115  ##[ ##13: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
 116  ##| ##31,32,33,34: #n; ##]
 117  ##[ ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (instrmode_destruct … H) ##]
 118 nqed.
 119
 120 nlemma decidable_im14 : ∀x:instr_mode.decidable (MODE_IX1 = x).
 121  #x; nnormalize; nelim x;
 122  ##[ ##14: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
 123  ##| ##31,32,33,34: #n; ##]
 124  ##[ ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (instrmode_destruct … H) ##]
 125 nqed.
 126
 127 nlemma decidable_im15 : ∀x:instr_mode.decidable (MODE_IX2 = x).
 128  #x; nnormalize; nelim x;
 129  ##[ ##15: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
 130  ##| ##31,32,33,34: #n; ##]
 131  ##[ ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (instrmode_destruct … H) ##]
 132 nqed.
 133
 134 nlemma decidable_im16 : ∀x:instr_mode.decidable (MODE_SP1 = x).
 135  #x; nnormalize; nelim x;
 136  ##[ ##16: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
 137  ##| ##31,32,33,34: #n; ##]
 138  ##[ ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (instrmode_destruct … H) ##]
 139 nqed.
 140
 141 nlemma decidable_im17 : ∀x:instr_mode.decidable (MODE_SP2 = x).
 142  #x; nnormalize; nelim x;
 143  ##[ ##17: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
 144  ##| ##31,32,33,34: #n; ##]
 145  ##[ ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (instrmode_destruct … H) ##]
 146 nqed.
 147
 148 nlemma decidable_im18 : ∀x:instr_mode.decidable (MODE_DIR1_to_DIR1 = x).
 149  #x; nnormalize; nelim x;
 150  ##[ ##18: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
 151  ##| ##31,32,33,34: #n; ##]
 152  ##[ ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (instrmode_destruct … H) ##]
 153 nqed.
 154
 155 nlemma decidable_im19 : ∀x:instr_mode.decidable (MODE_IMM1_to_DIR1 = x).
 156  #x; nnormalize; nelim x;
 157  ##[ ##19: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
 158  ##| ##31,32,33,34: #n; ##]
 159  ##[ ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (instrmode_destruct … H) ##]
 160 nqed.
 161
 162 nlemma decidable_im20 : ∀x:instr_mode.decidable (MODE_IX0p_to_DIR1 = x).
 163  #x; nnormalize; nelim x;
 164  ##[ ##20: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
 165  ##| ##31,32,33,34: #n; ##]
 166  ##[ ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (instrmode_destruct … H) ##]
 167 nqed.
 168
 169 nlemma decidable_im21 : ∀x:instr_mode.decidable (MODE_DIR1_to_IX0p = x).
 170  #x; nnormalize; nelim x;
 171  ##[ ##21: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
 172  ##| ##31,32,33,34: #n; ##]
 173  ##[ ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (instrmode_destruct … H) ##]
 174 nqed.
 175
 176 nlemma decidable_im22 : ∀x:instr_mode.decidable (MODE_INHA_and_IMM1 = x).
 177  #x; nnormalize; nelim x;
 178  ##[ ##22: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
 179  ##| ##31,32,33,34: #n; ##]
 180  ##[ ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (instrmode_destruct … H) ##]
 181 nqed.
 182
 183 nlemma decidable_im23 : ∀x:instr_mode.decidable (MODE_INHX_and_IMM1 = x).
 184  #x; nnormalize; nelim x;
 185  ##[ ##23: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
 186  ##| ##31,32,33,34: #n; ##]
 187  ##[ ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (instrmode_destruct … H) ##]
 188 nqed.
 189
 190 nlemma decidable_im24 : ∀x:instr_mode.decidable (MODE_IMM1_and_IMM1 = x).
 191  #x; nnormalize; nelim x;
 192  ##[ ##24: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
 193  ##| ##31,32,33,34: #n; ##]
 194  ##[ ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (instrmode_destruct … H) ##]
 195 nqed.
 196
 197 nlemma decidable_im25 : ∀x:instr_mode.decidable (MODE_DIR1_and_IMM1 = x).
 198  #x; nnormalize; nelim x;
 199  ##[ ##25: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
 200  ##| ##31,32,33,34: #n; ##]
 201  ##[ ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (instrmode_destruct … H) ##]
 202 nqed.
 203
 204 nlemma decidable_im26 : ∀x:instr_mode.decidable (MODE_IX0_and_IMM1 = x).
 205  #x; nnormalize; nelim x;
 206  ##[ ##26: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
 207  ##| ##31,32,33,34: #n; ##]
 208  ##[ ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (instrmode_destruct … H) ##]
 209 nqed.
 210
 211 nlemma decidable_im27 : ∀x:instr_mode.decidable (MODE_IX0p_and_IMM1 = x).
 212  #x; nnormalize; nelim x;
 213  ##[ ##27: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
 214  ##| ##31,32,33,34: #n; ##]
 215  ##[ ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (instrmode_destruct … H) ##]
 216 nqed.
 217
 218 nlemma decidable_im28 : ∀x:instr_mode.decidable (MODE_IX1_and_IMM1 = x).
 219  #x; nnormalize; nelim x;
 220  ##[ ##28: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
 221  ##| ##31,32,33,34: #n; ##]
 222  ##[ ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (instrmode_destruct … H) ##]
 223 nqed.
 224
 225 nlemma decidable_im29 : ∀x:instr_mode.decidable (MODE_IX1p_and_IMM1 = x).
 226  #x; nnormalize; nelim x;
 227  ##[ ##29: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
 228  ##| ##31,32,33,34: #n; ##]
 229  ##[ ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (instrmode_destruct … H) ##]
 230 nqed.
 231
 232 nlemma decidable_im30 : ∀x:instr_mode.decidable (MODE_SP1_and_IMM1 = x).
 233  #x; nnormalize; nelim x;
 234  ##[ ##30: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
 235  ##| ##31,32,33,34: #n; ##]
 236  ##[ ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (instrmode_destruct … H) ##]
 237 nqed.
 238
 239 nlemma decidable_im31 : ∀n.∀x:instr_mode.decidable ((MODE_DIRn n) = x).
 240  #n1; #x; nnormalize; nelim x;
 241  ##[ ##31: #n2; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_oct n1 n2) …);
 242            ##[ ##1: #H; nrewrite > H; napply (or2_intro1 (? = ?) (? ≠ ?) (refl_eq …))
 243            ##| ##2: #H; napply (or2_intro2 (? = ?) (? ≠ ?) ?); #H1; napply (H (instrmode_destruct_MODE_DIRn … H1))
 244            ##]
 245  ##| ##32,33,34: #n; ##]
 246  ##[ ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (instrmode_destruct … H) ##]
 247 nqed.
 248
 249 nlemma decidable_im32 : ∀n.∀x:instr_mode.decidable ((MODE_DIRn_and_IMM1 n) = x).
 250  #n1; #x; nnormalize; nelim x;
 251  ##[ ##32: #n2; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_oct n1 n2) …);
 252            ##[ ##1: #H; nrewrite > H; napply (or2_intro1 (? = ?) (? ≠ ?) (refl_eq …))
 253            ##| ##2: #H; napply (or2_intro2 (? = ?) (? ≠ ?) ?); #H1; napply (H (instrmode_destruct_MODE_DIRn_and_IMM1 … H1))
 254            ##]
 255  ##| ##31,33,34: #n; ##]
 256  ##[ ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (instrmode_destruct … H) ##]
 257 nqed.
 258
 259 nlemma decidable_im33 : ∀n.∀x:instr_mode.decidable ((MODE_TNY n) = x).
 260  #n1; #x; nnormalize; nelim x;
 261  ##[ ##33: #n2; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_ex n1 n2) …);
 262            ##[ ##1: #H; nrewrite > H; napply (or2_intro1 (? = ?) (? ≠ ?) (refl_eq …))
 263            ##| ##2: #H; napply (or2_intro2 (? = ?) (? ≠ ?) ?); #H1; napply (H (instrmode_destruct_MODE_TNY … H1))
 264            ##]
 265  ##| ##31,32,34: #n; ##]
 266  ##[ ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (instrmode_destruct … H) ##]
 267 nqed.
 268
 269 nlemma decidable_im34 : ∀n.∀x:instr_mode.decidable ((MODE_SRT n) = x).
 270  #n1; #x; nnormalize; nelim x;
 271  ##[ ##34: #n2; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_bit n1 n2) …);
 272            ##[ ##1: #H; nrewrite > H; napply (or2_intro1 (? = ?) (? ≠ ?) (refl_eq …))
 273            ##| ##2: #H; napply (or2_intro2 (? = ?) (? ≠ ?) ?); #H1; napply (H (instrmode_destruct_MODE_SRT … H1))
 274            ##]
 275  ##| ##31,32,33: #n; ##]
 276  ##[ ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (instrmode_destruct … H) ##]
 277 nqed.
 278
 279 nlemma decidable_im : ∀x,y:instr_mode.decidable (x = y).
 280  #x; nelim x;
 281  ##[ ##1: napply decidable_im1 ##| ##2: napply decidable_im2
 282  ##| ##3: napply decidable_im3 ##| ##4: napply decidable_im4
 283  ##| ##5: napply decidable_im5 ##| ##6: napply decidable_im6
 284  ##| ##7: napply decidable_im7 ##| ##8: napply decidable_im8
 285  ##| ##9: napply decidable_im9 ##| ##10: napply decidable_im10
 286  ##| ##11: napply decidable_im11 ##| ##12: napply decidable_im12
 287  ##| ##13: napply decidable_im13 ##| ##14: napply decidable_im14
 288  ##| ##15: napply decidable_im15 ##| ##16: napply decidable_im16
 289  ##| ##17: napply decidable_im17 ##| ##18: napply decidable_im18
 290  ##| ##19: napply decidable_im19 ##| ##20: napply decidable_im20
 291  ##| ##21: napply decidable_im21 ##| ##22: napply decidable_im22
 292  ##| ##23: napply decidable_im23 ##| ##24: napply decidable_im24
 293  ##| ##25: napply decidable_im25 ##| ##26: napply decidable_im26
 294  ##| ##27: napply decidable_im27 ##| ##28: napply decidable_im28
 295  ##| ##29: napply decidable_im29 ##| ##30: napply decidable_im30
 296  ##| ##31: napply decidable_im31 ##| ##32: napply decidable_im32
 297  ##| ##33: napply decidable_im33 ##| ##34: napply decidable_im34
 298  ##]
 299 nqed.
 300
 301 nlemma neqim_to_neq1 : ∀i2.(eq_im MODE_INH i2 = false) → (MODE_INH ≠ i2).
 302  #i2; nelim i2; nnormalize;
 303  ##[ ##1: #H; napply (bool_destruct … H)
 304  ##| ##31,32,33,34: #n ##]
 305  ##[ ##*: #H; #H1; napply (instrmode_destruct … H1)
 306  ##]
 307 nqed.
 308
 309 nlemma neqim_to_neq2 : ∀i2.(eq_im MODE_INHA i2 = false) → (MODE_INHA ≠ i2).
 310  #i2; nelim i2; nnormalize;
 311  ##[ ##2: #H; napply (bool_destruct … H)
 312  ##| ##31,32,33,34: #n ##]
 313  ##[ ##*: #H; #H1; napply (instrmode_destruct … H1)
 314  ##]
 315 nqed.
 316
 317 nlemma neqim_to_neq3 : ∀i2.(eq_im MODE_INHX i2 = false) → (MODE_INHX ≠ i2).
 318  #i2; nelim i2; nnormalize;
 319  ##[ ##3: #H; napply (bool_destruct … H)
 320  ##| ##31,32,33,34: #n ##]
 321  ##[ ##*: #H; #H1; napply (instrmode_destruct … H1)
 322  ##]
 323 nqed.
 324
 325 nlemma neqim_to_neq4 : ∀i2.(eq_im MODE_INHH i2 = false) → (MODE_INHH ≠ i2).
 326  #i2; nelim i2; nnormalize;
 327  ##[ ##4: #H; napply (bool_destruct … H)
 328  ##| ##31,32,33,34: #n ##]
 329  ##[ ##*: #H; #H1; napply (instrmode_destruct … H1)
 330  ##]
 331 nqed.
 332
 333 nlemma neqim_to_neq5 : ∀i2.(eq_im MODE_INHX0ADD i2 = false) → (MODE_INHX0ADD ≠ i2).
 334  #i2; nelim i2; nnormalize;
 335  ##[ ##5: #H; napply (bool_destruct … H)
 336  ##| ##31,32,33,34: #n ##]
 337  ##[ ##*: #H; #H1; napply (instrmode_destruct … H1)
 338  ##]
 339 nqed.
 340
 341 nlemma neqim_to_neq6 : ∀i2.(eq_im MODE_INHX1ADD i2 = false) → (MODE_INHX1ADD ≠ i2).
 342  #i2; nelim i2; nnormalize;
 343  ##[ ##6: #H; napply (bool_destruct … H)
 344  ##| ##31,32,33,34: #n ##]
 345  ##[ ##*: #H; #H1; napply (instrmode_destruct … H1)
 346  ##]
 347 nqed.
 348
 349 nlemma neqim_to_neq7 : ∀i2.(eq_im MODE_INHX2ADD i2 = false) → (MODE_INHX2ADD ≠ i2).
 350  #i2; nelim i2; nnormalize;
 351  ##[ ##7: #H; napply (bool_destruct … H)
 352  ##| ##31,32,33,34: #n ##]
 353  ##[ ##*: #H; #H1; napply (instrmode_destruct … H1)
 354  ##]
 355 nqed.
 356
 357 nlemma neqim_to_neq8 : ∀i2.(eq_im MODE_IMM1 i2 = false) → (MODE_IMM1 ≠ i2).
 358  #i2; nelim i2; nnormalize;
 359  ##[ ##8: #H; napply (bool_destruct … H)
 360  ##| ##31,32,33,34: #n ##]
 361  ##[ ##*: #H; #H1; napply (instrmode_destruct … H1)
 362  ##]
 363 nqed.
 364
 365 nlemma neqim_to_neq9 : ∀i2.(eq_im MODE_IMM1EXT i2 = false) → (MODE_IMM1EXT ≠ i2).
 366  #i2; nelim i2; nnormalize;
 367  ##[ ##9: #H; napply (bool_destruct … H)
 368  ##| ##31,32,33,34: #n ##]
 369  ##[ ##*: #H; #H1; napply (instrmode_destruct … H1)
 370  ##]
 371 nqed.
 372
 373 nlemma neqim_to_neq10 : ∀i2.(eq_im MODE_IMM2 i2 = false) → (MODE_IMM2 ≠ i2).
 374  #i2; nelim i2; nnormalize;
 375  ##[ ##10: #H; napply (bool_destruct … H)
 376  ##| ##31,32,33,34: #n ##]
 377  ##[ ##*: #H; #H1; napply (instrmode_destruct … H1)
 378  ##]
 379 nqed.
 380
 381 nlemma neqim_to_neq11 : ∀i2.(eq_im MODE_DIR1 i2 = false) → (MODE_DIR1 ≠ i2).
 382  #i2; nelim i2; nnormalize;
 383  ##[ ##11: #H; napply (bool_destruct … H)
 384  ##| ##31,32,33,34: #n ##]
 385  ##[ ##*: #H; #H1; napply (instrmode_destruct … H1)
 386  ##]
 387 nqed.
 388
 389 nlemma neqim_to_neq12 : ∀i2.(eq_im MODE_DIR2 i2 = false) → (MODE_DIR2 ≠ i2).
 390  #i2; nelim i2; nnormalize;
 391  ##[ ##12: #H; napply (bool_destruct … H)
 392  ##| ##31,32,33,34: #n ##]
 393  ##[ ##*: #H; #H1; napply (instrmode_destruct … H1)
 394  ##]
 395 nqed.
 396
 397 nlemma neqim_to_neq13 : ∀i2.(eq_im MODE_IX0 i2 = false) → (MODE_IX0 ≠ i2).
 398  #i2; nelim i2; nnormalize;
 399  ##[ ##13: #H; napply (bool_destruct … H)
 400  ##| ##31,32,33,34: #n ##]
 401  ##[ ##*: #H; #H1; napply (instrmode_destruct … H1)
 402  ##]
 403 nqed.
 404
 405 nlemma neqim_to_neq14 : ∀i2.(eq_im MODE_IX1 i2 = false) → (MODE_IX1 ≠ i2).
 406  #i2; nelim i2; nnormalize;
 407  ##[ ##14: #H; napply (bool_destruct … H)
 408  ##| ##31,32,33,34: #n ##]
 409  ##[ ##*: #H; #H1; napply (instrmode_destruct … H1)
 410  ##]
 411 nqed.
 412
 413 nlemma neqim_to_neq15 : ∀i2.(eq_im MODE_IX2 i2 = false) → (MODE_IX2 ≠ i2).
 414  #i2; nelim i2; nnormalize;
 415  ##[ ##15: #H; napply (bool_destruct … H)
 416  ##| ##31,32,33,34: #n ##]
 417  ##[ ##*: #H; #H1; napply (instrmode_destruct … H1)
 418  ##]
 419 nqed.
 420
 421 nlemma neqim_to_neq16 : ∀i2.(eq_im MODE_SP1 i2 = false) → (MODE_SP1 ≠ i2).
 422  #i2; nelim i2; nnormalize;
 423  ##[ ##16: #H; napply (bool_destruct … H)
 424  ##| ##31,32,33,34: #n ##]
 425  ##[ ##*: #H; #H1; napply (instrmode_destruct … H1)
 426  ##]
 427 nqed.
 428
 429 nlemma neqim_to_neq17 : ∀i2.(eq_im MODE_SP2 i2 = false) → (MODE_SP2 ≠ i2).
 430  #i2; nelim i2; nnormalize;
 431  ##[ ##17: #H; napply (bool_destruct … H)
 432  ##| ##31,32,33,34: #n ##]
 433  ##[ ##*: #H; #H1; napply (instrmode_destruct … H1)
 434  ##]
 435 nqed.
 436
 437 nlemma neqim_to_neq18 : ∀i2.(eq_im MODE_DIR1_to_DIR1 i2 = false) → (MODE_DIR1_to_DIR1 ≠ i2).
 438  #i2; nelim i2; nnormalize;
 439  ##[ ##18: #H; napply (bool_destruct … H)
 440  ##| ##31,32,33,34: #n ##]
 441  ##[ ##*: #H; #H1; napply (instrmode_destruct … H1)
 442  ##]
 443 nqed.
 444
 445 nlemma neqim_to_neq19 : ∀i2.(eq_im MODE_IMM1_to_DIR1 i2 = false) → (MODE_IMM1_to_DIR1 ≠ i2).
 446  #i2; nelim i2; nnormalize;
 447  ##[ ##19: #H; napply (bool_destruct … H)
 448  ##| ##31,32,33,34: #n ##]
 449  ##[ ##*: #H; #H1; napply (instrmode_destruct … H1)
 450  ##]
 451 nqed.
 452
 453 nlemma neqim_to_neq20 : ∀i2.(eq_im MODE_IX0p_to_DIR1 i2 = false) → (MODE_IX0p_to_DIR1 ≠ i2).
 454  #i2; nelim i2; nnormalize;
 455  ##[ ##20: #H; napply (bool_destruct … H)
 456  ##| ##31,32,33,34: #n ##]
 457  ##[ ##*: #H; #H1; napply (instrmode_destruct … H1)
 458  ##]
 459 nqed.
 460
 461 nlemma neqim_to_neq21 : ∀i2.(eq_im MODE_DIR1_to_IX0p i2 = false) → (MODE_DIR1_to_IX0p ≠ i2).
 462  #i2; nelim i2; nnormalize;
 463  ##[ ##21: #H; napply (bool_destruct … H)
 464  ##| ##31,32,33,34: #n ##]
 465  ##[ ##*: #H; #H1; napply (instrmode_destruct … H1)
 466  ##]
 467 nqed.
 468
 469 nlemma neqim_to_neq22 : ∀i2.(eq_im MODE_INHA_and_IMM1 i2 = false) → (MODE_INHA_and_IMM1 ≠ i2).
 470  #i2; nelim i2; nnormalize;
 471  ##[ ##22: #H; napply (bool_destruct … H)
 472  ##| ##31,32,33,34: #n ##]
 473  ##[ ##*: #H; #H1; napply (instrmode_destruct … H1)
 474  ##]
 475 nqed.
 476
 477 nlemma neqim_to_neq23 : ∀i2.(eq_im MODE_INHX_and_IMM1 i2 = false) → (MODE_INHX_and_IMM1 ≠ i2).
 478  #i2; nelim i2; nnormalize;
 479  ##[ ##23: #H; napply (bool_destruct … H)
 480  ##| ##31,32,33,34: #n ##]
 481  ##[ ##*: #H; #H1; napply (instrmode_destruct … H1)
 482  ##]
 483 nqed.
 484
 485 nlemma neqim_to_neq24 : ∀i2.(eq_im MODE_IMM1_and_IMM1 i2 = false) → (MODE_IMM1_and_IMM1 ≠ i2).
 486  #i2; nelim i2; nnormalize;
 487  ##[ ##24: #H; napply (bool_destruct … H)
 488  ##| ##31,32,33,34: #n ##]
 489  ##[ ##*: #H; #H1; napply (instrmode_destruct … H1)
 490  ##]
 491 nqed.
 492
 493 nlemma neqim_to_neq25 : ∀i2.(eq_im MODE_DIR1_and_IMM1 i2 = false) → (MODE_DIR1_and_IMM1 ≠ i2).
 494  #i2; nelim i2; nnormalize;
 495  ##[ ##25: #H; napply (bool_destruct … H)
 496  ##| ##31,32,33,34: #n ##]
 497  ##[ ##*: #H; #H1; napply (instrmode_destruct … H1)
 498  ##]
 499 nqed.
 500
 501 nlemma neqim_to_neq26 : ∀i2.(eq_im MODE_IX0_and_IMM1 i2 = false) → (MODE_IX0_and_IMM1 ≠ i2).
 502  #i2; nelim i2; nnormalize;
 503  ##[ ##26: #H; napply (bool_destruct … H)
 504  ##| ##31,32,33,34: #n ##]
 505  ##[ ##*: #H; #H1; napply (instrmode_destruct … H1)
 506  ##]
 507 nqed.
 508
 509 nlemma neqim_to_neq27 : ∀i2.(eq_im MODE_IX0p_and_IMM1 i2 = false) → (MODE_IX0p_and_IMM1 ≠ i2).
 510  #i2; nelim i2; nnormalize;
 511  ##[ ##27: #H; napply (bool_destruct … H)
 512  ##| ##31,32,33,34: #n ##]
 513  ##[ ##*: #H; #H1; napply (instrmode_destruct … H1)
 514  ##]
 515 nqed.
 516
 517 nlemma neqim_to_neq28 : ∀i2.(eq_im MODE_IX1_and_IMM1 i2 = false) → (MODE_IX1_and_IMM1 ≠ i2).
 518  #i2; nelim i2; nnormalize;
 519  ##[ ##28: #H; napply (bool_destruct … H)
 520  ##| ##31,32,33,34: #n ##]
 521  ##[ ##*: #H; #H1; napply (instrmode_destruct … H1)
 522  ##]
 523 nqed.
 524
 525 nlemma neqim_to_neq29 : ∀i2.(eq_im MODE_IX1p_and_IMM1 i2 = false) → (MODE_IX1p_and_IMM1 ≠ i2).
 526  #i2; nelim i2; nnormalize;
 527  ##[ ##29: #H; napply (bool_destruct … H)
 528  ##| ##31,32,33,34: #n ##]
 529  ##[ ##*: #H; #H1; napply (instrmode_destruct … H1)
 530  ##]
 531 nqed.
 532
 533 nlemma neqim_to_neq30 : ∀i2.(eq_im MODE_SP1_and_IMM1 i2 = false) → (MODE_SP1_and_IMM1 ≠ i2).
 534  #i2; nelim i2; nnormalize;
 535  ##[ ##30: #H; napply (bool_destruct … H)
 536  ##| ##31,32,33,34: #n ##]
 537  ##[ ##*: #H; #H1; napply (instrmode_destruct … H1)
 538  ##]
 539 nqed.
 540
 541 nlemma neqim_to_neq31 : ∀n.∀i2.(eq_im (MODE_DIRn n) i2 = false) → ((MODE_DIRn n) ≠ i2).
 542  #n1; #i2; nelim i2;
 543  ##[ ##31: #n2; #H; nchange in H:(%) with (eq_oct n1 n2 = false);
 544            nnormalize; #H1; napply (neqoct_to_neq … H); napply (instrmode_destruct_MODE_DIRn … H1)
 545  ##| ##32,33,34: #n ##]
 546  ##[ ##*: nnormalize; #H; #H1; napply (instrmode_destruct … H1)
 547  ##]
 548 nqed.
 549
 550 nlemma neqim_to_neq32 : ∀n.∀i2.(eq_im (MODE_DIRn_and_IMM1 n) i2 = false) → ((MODE_DIRn_and_IMM1 n) ≠ i2).
 551  #n1; #i2; nelim i2;
 552  ##[ ##32: #n2; #H; nchange in H:(%) with (eq_oct n1 n2 = false);
 553            nnormalize; #H1; napply (neqoct_to_neq … H); napply (instrmode_destruct_MODE_DIRn_and_IMM1 … H1)
 554  ##| ##31,33,34: #n ##]
 555  ##[ ##*: nnormalize; #H; #H1; napply (instrmode_destruct … H1)
 556  ##]
 557 nqed.
 558
 559 nlemma neqim_to_neq33 : ∀n.∀i2.(eq_im (MODE_TNY n) i2 = false) → ((MODE_TNY n) ≠ i2).
 560  #n1; #i2; nelim i2;
 561  ##[ ##33: #n2; #H; nchange in H:(%) with (eq_ex n1 n2 = false);
 562            nnormalize; #H1; napply (neqex_to_neq … H); napply (instrmode_destruct_MODE_TNY … H1)
 563  ##| ##31,32,34: #n ##]
 564  ##[ ##*: nnormalize; #H; #H1; napply (instrmode_destruct … H1)
 565  ##]
 566 nqed.
 567
 568 nlemma neqim_to_neq34 : ∀n.∀i2.(eq_im (MODE_SRT n) i2 = false) → ((MODE_SRT n) ≠ i2).
 569  #n1; #i2; nelim i2;
 570  ##[ ##34: #n2; #H; nchange in H:(%) with (eq_bit n1 n2 = false);
 571            nnormalize; #H1; napply (neqbit_to_neq … H); napply (instrmode_destruct_MODE_SRT … H1)
 572  ##| ##31,32,33: #n ##]
 573  ##[ ##*: nnormalize; #H; #H1; napply (instrmode_destruct … H1)
 574  ##]
 575 nqed.
 576
 577 nlemma neqim_to_neq : ∀i1,i2.(eq_im i1 i2 = false) → (i1 ≠ i2).
 578  #i1; nelim i1;
 579  ##[ ##1: napply neqim_to_neq1 ##| ##2: napply neqim_to_neq2
 580  ##| ##3: napply neqim_to_neq3 ##| ##4: napply neqim_to_neq4
 581  ##| ##5: napply neqim_to_neq5 ##| ##6: napply neqim_to_neq6
 582  ##| ##7: napply neqim_to_neq7 ##| ##8: napply neqim_to_neq8
 583  ##| ##9: napply neqim_to_neq9 ##| ##10: napply neqim_to_neq10
 584  ##| ##11: napply neqim_to_neq11 ##| ##12: napply neqim_to_neq12
 585  ##| ##13: napply neqim_to_neq13 ##| ##14: napply neqim_to_neq14
 586  ##| ##15: napply neqim_to_neq15 ##| ##16: napply neqim_to_neq16
 587  ##| ##17: napply neqim_to_neq17 ##| ##18: napply neqim_to_neq18
 588  ##| ##19: napply neqim_to_neq19 ##| ##20: napply neqim_to_neq20
 589  ##| ##21: napply neqim_to_neq21 ##| ##22: napply neqim_to_neq22
 590  ##| ##23: napply neqim_to_neq23 ##| ##24: napply neqim_to_neq24
 591  ##| ##25: napply neqim_to_neq25 ##| ##26: napply neqim_to_neq26
 592  ##| ##27: napply neqim_to_neq27 ##| ##28: napply neqim_to_neq28
 593  ##| ##29: napply neqim_to_neq29 ##| ##30: napply neqim_to_neq30
 594  ##| ##31: napply neqim_to_neq31 ##| ##32: napply neqim_to_neq32
 595  ##| ##33: napply neqim_to_neq33 ##| ##34: napply neqim_to_neq34
 596  ##]
 597 nqed.
 598
 599 nlemma neq_to_neqim1 : ∀i2.MODE_INH ≠ i2 → eq_im MODE_INH i2 = false.
 600  #i2; nelim i2; nnormalize;
 601  ##[ ##1: #H; nelim (H (refl_eq …))
 602  ##| ##31,32,33,34: #n; ##]
 603  ##[ ##*: #H; napply refl_eq
 604  ##]
 605 nqed.
 606
 607 nlemma neq_to_neqim2 : ∀i2.MODE_INHA ≠ i2 → eq_im MODE_INHA i2 = false.
 608  #i2; nelim i2; nnormalize;
 609  ##[ ##2: #H; nelim (H (refl_eq …))
 610  ##| ##31,32,33,34: #n; ##]
 611  ##[ ##*: #H; napply refl_eq
 612  ##]
 613 nqed.
 614
 615 nlemma neq_to_neqim3 : ∀i2.MODE_INHX ≠ i2 → eq_im MODE_INHX i2 = false.
 616  #i2; nelim i2; nnormalize;
 617  ##[ ##3: #H; nelim (H (refl_eq …))
 618  ##| ##31,32,33,34: #n; ##]
 619  ##[ ##*: #H; napply refl_eq
 620  ##]
 621 nqed.
 622
 623 nlemma neq_to_neqim4 : ∀i2.MODE_INHH ≠ i2 → eq_im MODE_INHH i2 = false.
 624  #i2; nelim i2; nnormalize;
 625  ##[ ##4: #H; nelim (H (refl_eq …))
 626  ##| ##31,32,33,34: #n; ##]
 627  ##[ ##*: #H; napply refl_eq
 628  ##]
 629 nqed.
 630
 631 nlemma neq_to_neqim5 : ∀i2.MODE_INHX0ADD ≠ i2 → eq_im MODE_INHX0ADD i2 = false.
 632  #i2; nelim i2; nnormalize;
 633  ##[ ##5: #H; nelim (H (refl_eq …))
 634  ##| ##31,32,33,34: #n; ##]
 635  ##[ ##*: #H; napply refl_eq
 636  ##]
 637 nqed.
 638
 639 nlemma neq_to_neqim6 : ∀i2.MODE_INHX1ADD ≠ i2 → eq_im MODE_INHX1ADD i2 = false.
 640  #i2; nelim i2; nnormalize;
 641  ##[ ##6: #H; nelim (H (refl_eq …))
 642  ##| ##31,32,33,34: #n; ##]
 643  ##[ ##*: #H; napply refl_eq
 644  ##]
 645 nqed.
 646
 647 nlemma neq_to_neqim7 : ∀i2.MODE_INHX2ADD ≠ i2 → eq_im MODE_INHX2ADD i2 = false.
 648  #i2; nelim i2; nnormalize;
 649  ##[ ##7: #H; nelim (H (refl_eq …))
 650  ##| ##31,32,33,34: #n; ##]
 651  ##[ ##*: #H; napply refl_eq
 652  ##]
 653 nqed.
 654
 655 nlemma neq_to_neqim8 : ∀i2.MODE_IMM1 ≠ i2 → eq_im MODE_IMM1 i2 = false.
 656  #i2; nelim i2; nnormalize;
 657  ##[ ##8: #H; nelim (H (refl_eq …))
 658  ##| ##31,32,33,34: #n; ##]
 659  ##[ ##*: #H; napply refl_eq
 660  ##]
 661 nqed.
 662
 663 nlemma neq_to_neqim9 : ∀i2.MODE_IMM1EXT ≠ i2 → eq_im MODE_IMM1EXT i2 = false.
 664  #i2; nelim i2; nnormalize;
 665  ##[ ##9: #H; nelim (H (refl_eq …))
 666  ##| ##31,32,33,34: #n; ##]
 667  ##[ ##*: #H; napply refl_eq
 668  ##]
 669 nqed.
 670
 671 nlemma neq_to_neqim10 : ∀i2.MODE_IMM2 ≠ i2 → eq_im MODE_IMM2 i2 = false.
 672  #i2; nelim i2; nnormalize;
 673  ##[ ##10: #H; nelim (H (refl_eq …))
 674  ##| ##31,32,33,34: #n; ##]
 675  ##[ ##*: #H; napply refl_eq
 676  ##]
 677 nqed.
 678
 679 nlemma neq_to_neqim11 : ∀i2.MODE_DIR1 ≠ i2 → eq_im MODE_DIR1 i2 = false.
 680  #i2; nelim i2; nnormalize;
 681  ##[ ##11: #H; nelim (H (refl_eq …))
 682  ##| ##31,32,33,34: #n; ##]
 683  ##[ ##*: #H; napply refl_eq
 684  ##]
 685 nqed.
 686
 687 nlemma neq_to_neqim12 : ∀i2.MODE_DIR2 ≠ i2 → eq_im MODE_DIR2 i2 = false.
 688  #i2; nelim i2; nnormalize;
 689  ##[ ##12: #H; nelim (H (refl_eq …))
 690  ##| ##31,32,33,34: #n; ##]
 691  ##[ ##*: #H; napply refl_eq
 692  ##]
 693 nqed.
 694
 695 nlemma neq_to_neqim13 : ∀i2.MODE_IX0 ≠ i2 → eq_im MODE_IX0 i2 = false.
 696  #i2; nelim i2; nnormalize;
 697  ##[ ##13: #H; nelim (H (refl_eq …))
 698  ##| ##31,32,33,34: #n; ##]
 699  ##[ ##*: #H; napply refl_eq
 700  ##]
 701 nqed.
 702
 703 nlemma neq_to_neqim14 : ∀i2.MODE_IX1 ≠ i2 → eq_im MODE_IX1 i2 = false.
 704  #i2; nelim i2; nnormalize;
 705  ##[ ##14: #H; nelim (H (refl_eq …))
 706  ##| ##31,32,33,34: #n; ##]
 707  ##[ ##*: #H; napply refl_eq
 708  ##]
 709 nqed.
 710
 711 nlemma neq_to_neqim15 : ∀i2.MODE_IX2 ≠ i2 → eq_im MODE_IX2 i2 = false.
 712  #i2; nelim i2; nnormalize;
 713  ##[ ##15: #H; nelim (H (refl_eq …))
 714  ##| ##31,32,33,34: #n; ##]
 715  ##[ ##*: #H; napply refl_eq
 716  ##]
 717 nqed.
 718
 719 nlemma neq_to_neqim16 : ∀i2.MODE_SP1 ≠ i2 → eq_im MODE_SP1 i2 = false.
 720  #i2; nelim i2; nnormalize;
 721  ##[ ##16: #H; nelim (H (refl_eq …))
 722  ##| ##31,32,33,34: #n; ##]
 723  ##[ ##*: #H; napply refl_eq
 724  ##]
 725 nqed.
 726
 727 nlemma neq_to_neqim17 : ∀i2.MODE_SP2 ≠ i2 → eq_im MODE_SP2 i2 = false.
 728  #i2; nelim i2; nnormalize;
 729  ##[ ##17: #H; nelim (H (refl_eq …))
 730  ##| ##31,32,33,34: #n; ##]
 731  ##[ ##*: #H; napply refl_eq
 732  ##]
 733 nqed.
 734
 735 nlemma neq_to_neqim18 : ∀i2.MODE_DIR1_to_DIR1 ≠ i2 → eq_im MODE_DIR1_to_DIR1 i2 = false.
 736  #i2; nelim i2; nnormalize;
 737  ##[ ##18: #H; nelim (H (refl_eq …))
 738  ##| ##31,32,33,34: #n; ##]
 739  ##[ ##*: #H; napply refl_eq
 740  ##]
 741 nqed.
 742
 743 nlemma neq_to_neqim19 : ∀i2.MODE_IMM1_to_DIR1 ≠ i2 → eq_im MODE_IMM1_to_DIR1 i2 = false.
 744  #i2; nelim i2; nnormalize;
 745  ##[ ##19: #H; nelim (H (refl_eq …))
 746  ##| ##31,32,33,34: #n; ##]
 747  ##[ ##*: #H; napply refl_eq
 748  ##]
 749 nqed.
 750
 751 nlemma neq_to_neqim20 : ∀i2.MODE_IX0p_to_DIR1 ≠ i2 → eq_im MODE_IX0p_to_DIR1 i2 = false.
 752  #i2; nelim i2; nnormalize;
 753  ##[ ##20: #H; nelim (H (refl_eq …))
 754  ##| ##31,32,33,34: #n; ##]
 755  ##[ ##*: #H; napply refl_eq
 756  ##]
 757 nqed.
 758
 759 nlemma neq_to_neqim21 : ∀i2.MODE_DIR1_to_IX0p ≠ i2 → eq_im MODE_DIR1_to_IX0p i2 = false.
 760  #i2; nelim i2; nnormalize;
 761  ##[ ##21: #H; nelim (H (refl_eq …))
 762  ##| ##31,32,33,34: #n; ##]
 763  ##[ ##*: #H; napply refl_eq
 764  ##]
 765 nqed.
 766
 767 nlemma neq_to_neqim22 : ∀i2.MODE_INHA_and_IMM1≠ i2 → eq_im MODE_INHA_and_IMM1 i2 = false.
 768  #i2; nelim i2; nnormalize;
 769  ##[ ##22: #H; nelim (H (refl_eq …))
 770  ##| ##31,32,33,34: #n; ##]
 771  ##[ ##*: #H; napply refl_eq
 772  ##]
 773 nqed.
 774
 775 nlemma neq_to_neqim23 : ∀i2.MODE_INHX_and_IMM1 ≠ i2 → eq_im MODE_INHX_and_IMM1 i2 = false.
 776  #i2; nelim i2; nnormalize;
 777  ##[ ##23: #H; nelim (H (refl_eq …))
 778  ##| ##31,32,33,34: #n; ##]
 779  ##[ ##*: #H; napply refl_eq
 780  ##]
 781 nqed.
 782
 783 nlemma neq_to_neqim24 : ∀i2.MODE_IMM1_and_IMM1 ≠ i2 → eq_im MODE_IMM1_and_IMM1 i2 = false.
 784  #i2; nelim i2; nnormalize;
 785  ##[ ##24: #H; nelim (H (refl_eq …))
 786  ##| ##31,32,33,34: #n; ##]
 787  ##[ ##*: #H; napply refl_eq
 788  ##]
 789 nqed.
 790
 791 nlemma neq_to_neqim25 : ∀i2.MODE_DIR1_and_IMM1 ≠ i2 → eq_im MODE_DIR1_and_IMM1 i2 = false.
 792  #i2; nelim i2; nnormalize;
 793  ##[ ##25: #H; nelim (H (refl_eq …))
 794  ##| ##31,32,33,34: #n; ##]
 795  ##[ ##*: #H; napply refl_eq
 796  ##]
 797 nqed.
 798
 799 nlemma neq_to_neqim26 : ∀i2.MODE_IX0_and_IMM1 ≠ i2 → eq_im MODE_IX0_and_IMM1 i2 = false.
 800  #i2; nelim i2; nnormalize;
 801  ##[ ##26: #H; nelim (H (refl_eq …))
 802  ##| ##31,32,33,34: #n; ##]
 803  ##[ ##*: #H; napply refl_eq
 804  ##]
 805 nqed.
 806
 807 nlemma neq_to_neqim27 : ∀i2.MODE_IX0p_and_IMM1 ≠ i2 → eq_im MODE_IX0p_and_IMM1 i2 = false.
 808  #i2; nelim i2; nnormalize;
 809  ##[ ##27: #H; nelim (H (refl_eq …))
 810  ##| ##31,32,33,34: #n; ##]
 811  ##[ ##*: #H; napply refl_eq
 812  ##]
 813 nqed.
 814
 815 nlemma neq_to_neqim28 : ∀i2.MODE_IX1_and_IMM1 ≠ i2 → eq_im MODE_IX1_and_IMM1 i2 = false.
 816  #i2; nelim i2; nnormalize;
 817  ##[ ##28: #H; nelim (H (refl_eq …))
 818  ##| ##31,32,33,34: #n; ##]
 819  ##[ ##*: #H; napply refl_eq
 820  ##]
 821 nqed.
 822
 823 nlemma neq_to_neqim29 : ∀i2.MODE_IX1p_and_IMM1 ≠ i2 → eq_im MODE_IX1p_and_IMM1 i2 = false.
 824  #i2; nelim i2; nnormalize;
 825  ##[ ##29: #H; nelim (H (refl_eq …))
 826  ##| ##31,32,33,34: #n; ##]
 827  ##[ ##*: #H; napply refl_eq
 828  ##]
 829 nqed.
 830
 831 nlemma neq_to_neqim30 : ∀i2.MODE_SP1_and_IMM1 ≠ i2 → eq_im MODE_SP1_and_IMM1 i2 = false.
 832  #i2; nelim i2; nnormalize;
 833  ##[ ##30: #H; nelim (H (refl_eq …))
 834  ##| ##31,32,33,34: #n; ##]
 835  ##[ ##*: #H; napply refl_eq
 836  ##]
 837 nqed.
 838
 839 nlemma neq_to_neqim31 : ∀n.∀i2.(MODE_DIRn n) ≠ i2 → eq_im (MODE_DIRn n) i2 = false.
 840  #n1; #i2; nelim i2;
 841  ##[ ##31: #n2; #H; nchange with (eq_oct n1 n2 = false); napply (neq_to_neqoct n1 n2 ?);
 842            nnormalize; #H1; nrewrite > H1 in H:(%); #H; nelim (H (refl_eq …))
 843  ##| ##32,33,34: #n; ##]
 844  ##[ ##*: #H; nnormalize; napply refl_eq
 845  ##]
 846 nqed.
 847
 848 nlemma neq_to_neqim32 : ∀n.∀i2.(MODE_DIRn_and_IMM1 n) ≠ i2 → eq_im (MODE_DIRn_and_IMM1 n) i2 = false.
 849  #n1; #i2; nelim i2;
 850  ##[ ##32: #n2; #H; nchange with (eq_oct n1 n2 = false); napply (neq_to_neqoct n1 n2 ?);
 851            nnormalize; #H1; nrewrite > H1 in H:(%); #H; nelim (H (refl_eq …))
 852  ##| ##31,33,34: #n; ##]
 853  ##[ ##*: #H; nnormalize; napply refl_eq
 854  ##]
 855 nqed.
 856
 857 nlemma neq_to_neqim33 : ∀n.∀i2.(MODE_TNY n) ≠ i2 → eq_im (MODE_TNY n) i2 = false.
 858  #n1; #i2; nelim i2;
 859  ##[ ##33: #n2; #H; nchange with (eq_ex n1 n2 = false); napply (neq_to_neqex n1 n2 ?);
 860            nnormalize; #H1; nrewrite > H1 in H:(%); #H; nelim (H (refl_eq …))
 861  ##| ##31,32,34: #n; ##]
 862  ##[ ##*: #H; nnormalize; napply refl_eq
 863  ##]
 864 nqed.
 865
 866 nlemma neq_to_neqim34 : ∀n.∀i2.(MODE_SRT n) ≠ i2 → eq_im (MODE_SRT n) i2 = false.
 867  #n1; #i2; nelim i2;
 868  ##[ ##34: #n2; #H; nchange with (eq_bit n1 n2 = false); napply (neq_to_neqbit n1 n2 ?);
 869            nnormalize; #H1; nrewrite > H1 in H:(%); #H; nelim (H (refl_eq …))
 870  ##| ##31,32,33: #n; ##]
 871  ##[ ##*: #H; nnormalize; napply refl_eq
 872  ##]
 873 nqed.
 874
 875 nlemma neq_to_neqim : ∀i1,i2.i1 ≠ i2 → eq_im i1 i2 = false.
 876  #i1; nelim i1;
 877  ##[ ##1: napply neq_to_neqim1 ##| ##2: napply neq_to_neqim2
 878  ##| ##3: napply neq_to_neqim3 ##| ##4: napply neq_to_neqim4
 879  ##| ##5: napply neq_to_neqim5 ##| ##6: napply neq_to_neqim6
 880  ##| ##7: napply neq_to_neqim7 ##| ##8: napply neq_to_neqim8
 881  ##| ##9: napply neq_to_neqim9 ##| ##10: napply neq_to_neqim10
 882  ##| ##11: napply neq_to_neqim11 ##| ##12: napply neq_to_neqim12
 883  ##| ##13: napply neq_to_neqim13 ##| ##14: napply neq_to_neqim14
 884  ##| ##15: napply neq_to_neqim15 ##| ##16: napply neq_to_neqim16
 885  ##| ##17: napply neq_to_neqim17 ##| ##18: napply neq_to_neqim18
 886  ##| ##19: napply neq_to_neqim19 ##| ##20: napply neq_to_neqim20
 887  ##| ##21: napply neq_to_neqim21 ##| ##22: napply neq_to_neqim22
 888  ##| ##23: napply neq_to_neqim23 ##| ##24: napply neq_to_neqim24
 889  ##| ##25: napply neq_to_neqim25 ##| ##26: napply neq_to_neqim26
 890  ##| ##27: napply neq_to_neqim27 ##| ##28: napply neq_to_neqim28
 891  ##| ##29: napply neq_to_neqim29 ##| ##30: napply neq_to_neqim30
 892  ##| ##31: napply neq_to_neqim31 ##| ##32: napply neq_to_neqim32
 893  ##| ##33: napply neq_to_neqim33 ##| ##34: napply neq_to_neqim34
 894  ##]
 895 nqed.