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

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* ********************************************************************** *)
  16 (*                          Progetto FreeScale                            *)
  17 (*                                                                        *)
  18 (*   Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it                   *)
  19 (*     Cosimo Oliboni, oliboni@cs.unibo.it                                *)
  20 (*                                                                        *)
  21 (* ********************************************************************** *)
  22
  23 include "freescale/bool_lemmas.ma".
  24 include "freescale/bitrigesim.ma".
  25
  26 (* ************* *)
  27 (* BITRIGESIMALI *)
  28 (* ************* *)
  29
  30 ndefinition bitrigesim_destruct1 :
  31 Πt2:bitrigesim.ΠP:Prop.t00 = t2 → match t2 with [ t00 ⇒ P → P | _ ⇒ P ].
  32  #t2; #P;
  33  ncases t2;
  34  nnormalize; #H;
  35  ##[ ##1: napply (λx:P.x)
  36  ##| ##*: napply False_ind;
  37           nchange with (match t00 with [ t00 ⇒ False | _ ⇒ True ]);
  38           nrewrite > H; nnormalize; napply I
  39  ##]
  40 nqed.
  41
  42 ndefinition bitrigesim_destruct2 :
  43 Πt2:bitrigesim.ΠP:Prop.t01 = t2 → match t2 with [ t01 ⇒ P → P | _ ⇒ P ].
  44  #t2; #P;
  45  ncases t2;
  46  nnormalize; #H;
  47  ##[ ##2: napply (λx:P.x)
  48  ##| ##*: napply False_ind;
  49           nchange with (match t01 with [ t01 ⇒ False | _ ⇒ True ]);
  50           nrewrite > H; nnormalize; napply I
  51  ##]
  52 nqed.
  53
  54 ndefinition bitrigesim_destruct3 :
  55 Πt2:bitrigesim.ΠP:Prop.t02 = t2 → match t2 with [ t02 ⇒ P → P | _ ⇒ P ].
  56  #t2; #P;
  57  ncases t2;
  58  nnormalize; #H;
  59  ##[ ##3: napply (λx:P.x)
  60  ##| ##*: napply False_ind;
  61           nchange with (match t02 with [ t02 ⇒ False | _ ⇒ True ]);
  62           nrewrite > H; nnormalize; napply I
  63  ##]
  64 nqed.
  65
  66 ndefinition bitrigesim_destruct4 :
  67 Πt2:bitrigesim.ΠP:Prop.t03 = t2 → match t2 with [ t03 ⇒ P → P | _ ⇒ P ].
  68  #t2; #P;
  69  ncases t2;
  70  nnormalize; #H;
  71  ##[ ##4: napply (λx:P.x)
  72  ##| ##*: napply False_ind;
  73           nchange with (match t03 with [ t03 ⇒ False | _ ⇒ True ]);
  74           nrewrite > H; nnormalize; napply I
  75  ##]
  76 nqed.
  77
  78 ndefinition bitrigesim_destruct5 :
  79 Πt2:bitrigesim.ΠP:Prop.t04 = t2 → match t2 with [ t04 ⇒ P → P | _ ⇒ P ].
  80  #t2; #P;
  81  ncases t2;
  82  nnormalize; #H;
  83  ##[ ##5: napply (λx:P.x)
  84  ##| ##*: napply False_ind;
  85           nchange with (match t04 with [ t04 ⇒ False | _ ⇒ True ]);
  86           nrewrite > H; nnormalize; napply I
  87  ##]
  88 nqed.
  89
  90 ndefinition bitrigesim_destruct6 :
  91 Πt2:bitrigesim.ΠP:Prop.t05 = t2 → match t2 with [ t05 ⇒ P → P | _ ⇒ P ].
  92  #t2; #P;
  93  ncases t2;
  94  nnormalize; #H;
  95  ##[ ##6: napply (λx:P.x)
  96  ##| ##*: napply False_ind;
  97           nchange with (match t05 with [ t05 ⇒ False | _ ⇒ True ]);
  98           nrewrite > H; nnormalize; napply I
  99  ##]
 100 nqed.
 101
 102 ndefinition bitrigesim_destruct7 :
 103 Πt2:bitrigesim.ΠP:Prop.t06 = t2 → match t2 with [ t06 ⇒ P → P | _ ⇒ P ].
 104  #t2; #P;
 105  ncases t2;
 106  nnormalize; #H;
 107  ##[ ##7: napply (λx:P.x)
 108  ##| ##*: napply False_ind;
 109           nchange with (match t06 with [ t06 ⇒ False | _ ⇒ True ]);
 110           nrewrite > H; nnormalize; napply I
 111  ##]
 112 nqed.
 113
 114 ndefinition bitrigesim_destruct8 :
 115 Πt2:bitrigesim.ΠP:Prop.t07 = t2 → match t2 with [ t07 ⇒ P → P | _ ⇒ P ].
 116  #t2; #P;
 117  ncases t2;
 118  nnormalize; #H;
 119  ##[ ##8: napply (λx:P.x)
 120  ##| ##*: napply False_ind;
 121           nchange with (match t07 with [ t07 ⇒ False | _ ⇒ True ]);
 122           nrewrite > H; nnormalize; napply I
 123  ##]
 124 nqed.
 125
 126 ndefinition bitrigesim_destruct9 :
 127 Πt2:bitrigesim.ΠP:Prop.t08 = t2 → match t2 with [ t08 ⇒ P → P | _ ⇒ P ].
 128  #t2; #P;
 129  ncases t2;
 130  nnormalize; #H;
 131  ##[ ##9: napply (λx:P.x)
 132  ##| ##*: napply False_ind;
 133           nchange with (match t08 with [ t08 ⇒ False | _ ⇒ True ]);
 134           nrewrite > H; nnormalize; napply I
 135  ##]
 136 nqed.
 137
 138 ndefinition bitrigesim_destruct10 :
 139 Πt2:bitrigesim.ΠP:Prop.t09 = t2 → match t2 with [ t09 ⇒ P → P | _ ⇒ P ].
 140  #t2; #P;
 141  ncases t2;
 142  nnormalize; #H;
 143  ##[ ##10: napply (λx:P.x)
 144  ##| ##*: napply False_ind;
 145           nchange with (match t09 with [ t09 ⇒ False | _ ⇒ True ]);
 146           nrewrite > H; nnormalize; napply I
 147  ##]
 148 nqed.
 149
 150 ndefinition bitrigesim_destruct11 :
 151 Πt2:bitrigesim.ΠP:Prop.t0A = t2 → match t2 with [ t0A ⇒ P → P | _ ⇒ P ].
 152  #t2; #P;
 153  ncases t2;
 154  nnormalize; #H;
 155  ##[ ##11: napply (λx:P.x)
 156  ##| ##*: napply False_ind;
 157           nchange with (match t0A with [ t0A ⇒ False | _ ⇒ True ]);
 158           nrewrite > H; nnormalize; napply I
 159  ##]
 160 nqed.
 161
 162 ndefinition bitrigesim_destruct12 :
 163 Πt2:bitrigesim.ΠP:Prop.t0B = t2 → match t2 with [ t0B ⇒ P → P | _ ⇒ P ].
 164  #t2; #P;
 165  ncases t2;
 166  nnormalize; #H;
 167  ##[ ##12: napply (λx:P.x)
 168  ##| ##*: napply False_ind;
 169           nchange with (match t0B with [ t0B ⇒ False | _ ⇒ True ]);
 170           nrewrite > H; nnormalize; napply I
 171  ##]
 172 nqed.
 173
 174 ndefinition bitrigesim_destruct13 :
 175 Πt2:bitrigesim.ΠP:Prop.t0C = t2 → match t2 with [ t0C ⇒ P → P | _ ⇒ P ].
 176  #t2; #P;
 177  ncases t2;
 178  nnormalize; #H;
 179  ##[ ##13: napply (λx:P.x)
 180  ##| ##*: napply False_ind;
 181           nchange with (match t0C with [ t0C ⇒ False | _ ⇒ True ]);
 182           nrewrite > H; nnormalize; napply I
 183  ##]
 184 nqed.
 185
 186 ndefinition bitrigesim_destruct14 :
 187 Πt2:bitrigesim.ΠP:Prop.t0D = t2 → match t2 with [ t0D ⇒ P → P | _ ⇒ P ].
 188  #t2; #P;
 189  ncases t2;
 190  nnormalize; #H;
 191  ##[ ##14: napply (λx:P.x)
 192  ##| ##*: napply False_ind;
 193           nchange with (match t0D with [ t0D ⇒ False | _ ⇒ True ]);
 194           nrewrite > H; nnormalize; napply I
 195  ##]
 196 nqed.
 197
 198 ndefinition bitrigesim_destruct15 :
 199 Πt2:bitrigesim.ΠP:Prop.t0E = t2 → match t2 with [ t0E ⇒ P → P | _ ⇒ P ].
 200  #t2; #P;
 201  ncases t2;
 202  nnormalize; #H;
 203  ##[ ##15: napply (λx:P.x)
 204  ##| ##*: napply False_ind;
 205           nchange with (match t0E with [ t0E ⇒ False | _ ⇒ True ]);
 206           nrewrite > H; nnormalize; napply I
 207  ##]
 208 nqed.
 209
 210 ndefinition bitrigesim_destruct16 :
 211 Πt2:bitrigesim.ΠP:Prop.t0F = t2 → match t2 with [ t0F ⇒ P → P | _ ⇒ P ].
 212  #t2; #P;
 213  ncases t2;
 214  nnormalize; #H;
 215  ##[ ##16: napply (λx:P.x)
 216  ##| ##*: napply False_ind;
 217           nchange with (match t0F with [ t0F ⇒ False | _ ⇒ True ]);
 218           nrewrite > H; nnormalize; napply I
 219  ##]
 220 nqed.
 221
 222 ndefinition bitrigesim_destruct17 :
 223 Πt2:bitrigesim.ΠP:Prop.t10 = t2 → match t2 with [ t10 ⇒ P → P | _ ⇒ P ].
 224  #t2; #P;
 225  ncases t2;
 226  nnormalize; #H;
 227  ##[ ##17: napply (λx:P.x)
 228  ##| ##*: napply False_ind;
 229           nchange with (match t10 with [ t10 ⇒ False | _ ⇒ True ]);
 230           nrewrite > H; nnormalize; napply I
 231  ##]
 232 nqed.
 233
 234 ndefinition bitrigesim_destruct18 :
 235 Πt2:bitrigesim.ΠP:Prop.t11 = t2 → match t2 with [ t11 ⇒ P → P | _ ⇒ P ].
 236  #t2; #P;
 237  ncases t2;
 238  nnormalize; #H;
 239  ##[ ##18: napply (λx:P.x)
 240  ##| ##*: napply False_ind;
 241           nchange with (match t11 with [ t11 ⇒ False | _ ⇒ True ]);
 242           nrewrite > H; nnormalize; napply I
 243  ##]
 244 nqed.
 245
 246 ndefinition bitrigesim_destruct19 :
 247 Πt2:bitrigesim.ΠP:Prop.t12 = t2 → match t2 with [ t12 ⇒ P → P | _ ⇒ P ].
 248  #t2; #P;
 249  ncases t2;
 250  nnormalize; #H;
 251  ##[ ##19: napply (λx:P.x)
 252  ##| ##*: napply False_ind;
 253           nchange with (match t12 with [ t12 ⇒ False | _ ⇒ True ]);
 254           nrewrite > H; nnormalize; napply I
 255  ##]
 256 nqed.
 257
 258 ndefinition bitrigesim_destruct20 :
 259 Πt2:bitrigesim.ΠP:Prop.t13 = t2 → match t2 with [ t13 ⇒ P → P | _ ⇒ P ].
 260  #t2; #P;
 261  ncases t2;
 262  nnormalize; #H;
 263  ##[ ##20: napply (λx:P.x)
 264  ##| ##*: napply False_ind;
 265           nchange with (match t13 with [ t13 ⇒ False | _ ⇒ True ]);
 266           nrewrite > H; nnormalize; napply I
 267  ##]
 268 nqed.
 269
 270 ndefinition bitrigesim_destruct21 :
 271 Πt2:bitrigesim.ΠP:Prop.t14 = t2 → match t2 with [ t14 ⇒ P → P | _ ⇒ P ].
 272  #t2; #P;
 273  ncases t2;
 274  nnormalize; #H;
 275  ##[ ##21: napply (λx:P.x)
 276  ##| ##*: napply False_ind;
 277           nchange with (match t14 with [ t14 ⇒ False | _ ⇒ True ]);
 278           nrewrite > H; nnormalize; napply I
 279  ##]
 280 nqed.
 281
 282 ndefinition bitrigesim_destruct22 :
 283 Πt2:bitrigesim.ΠP:Prop.t15 = t2 → match t2 with [ t15 ⇒ P → P | _ ⇒ P ].
 284  #t2; #P;
 285  ncases t2;
 286  nnormalize; #H;
 287  ##[ ##22: napply (λx:P.x)
 288  ##| ##*: napply False_ind;
 289           nchange with (match t15 with [ t15 ⇒ False | _ ⇒ True ]);
 290           nrewrite > H; nnormalize; napply I
 291  ##]
 292 nqed.
 293
 294 ndefinition bitrigesim_destruct23 :
 295 Πt2:bitrigesim.ΠP:Prop.t16 = t2 → match t2 with [ t16 ⇒ P → P | _ ⇒ P ].
 296  #t2; #P;
 297  ncases t2;
 298  nnormalize; #H;
 299  ##[ ##23: napply (λx:P.x)
 300  ##| ##*: napply False_ind;
 301           nchange with (match t16 with [ t16 ⇒ False | _ ⇒ True ]);
 302           nrewrite > H; nnormalize; napply I
 303  ##]
 304 nqed.
 305
 306 ndefinition bitrigesim_destruct24 :
 307 Πt2:bitrigesim.ΠP:Prop.t17 = t2 → match t2 with [ t17 ⇒ P → P | _ ⇒ P ].
 308  #t2; #P;
 309  ncases t2;
 310  nnormalize; #H;
 311  ##[ ##24: napply (λx:P.x)
 312  ##| ##*: napply False_ind;
 313           nchange with (match t17 with [ t17 ⇒ False | _ ⇒ True ]);
 314           nrewrite > H; nnormalize; napply I
 315  ##]
 316 nqed.
 317
 318 ndefinition bitrigesim_destruct25 :
 319 Πt2:bitrigesim.ΠP:Prop.t18 = t2 → match t2 with [ t18 ⇒ P → P | _ ⇒ P ].
 320  #t2; #P;
 321  ncases t2;
 322  nnormalize; #H;
 323  ##[ ##25: napply (λx:P.x)
 324  ##| ##*: napply False_ind;
 325           nchange with (match t18 with [ t18 ⇒ False | _ ⇒ True ]);
 326           nrewrite > H; nnormalize; napply I
 327  ##]
 328 nqed.
 329
 330 ndefinition bitrigesim_destruct26 :
 331 Πt2:bitrigesim.ΠP:Prop.t19 = t2 → match t2 with [ t19 ⇒ P → P | _ ⇒ P ].
 332  #t2; #P;
 333  ncases t2;
 334  nnormalize; #H;
 335  ##[ ##26: napply (λx:P.x)
 336  ##| ##*: napply False_ind;
 337           nchange with (match t19 with [ t19 ⇒ False | _ ⇒ True ]);
 338           nrewrite > H; nnormalize; napply I
 339  ##]
 340 nqed.
 341
 342 ndefinition bitrigesim_destruct27 :
 343 Πt2:bitrigesim.ΠP:Prop.t1A = t2 → match t2 with [ t1A ⇒ P → P | _ ⇒ P ].
 344  #t2; #P;
 345  ncases t2;
 346  nnormalize; #H;
 347  ##[ ##27: napply (λx:P.x)
 348  ##| ##*: napply False_ind;
 349           nchange with (match t1A with [ t1A ⇒ False | _ ⇒ True ]);
 350           nrewrite > H; nnormalize; napply I
 351  ##]
 352 nqed.
 353
 354 ndefinition bitrigesim_destruct28 :
 355 Πt2:bitrigesim.ΠP:Prop.t1B = t2 → match t2 with [ t1B ⇒ P → P | _ ⇒ P ].
 356  #t2; #P;
 357  ncases t2;
 358  nnormalize; #H;
 359  ##[ ##28: napply (λx:P.x)
 360  ##| ##*: napply False_ind;
 361           nchange with (match t1B with [ t1B ⇒ False | _ ⇒ True ]);
 362           nrewrite > H; nnormalize; napply I
 363  ##]
 364 nqed.
 365
 366 ndefinition bitrigesim_destruct29 :
 367 Πt2:bitrigesim.ΠP:Prop.t1C = t2 → match t2 with [ t1C ⇒ P → P | _ ⇒ P ].
 368  #t2; #P;
 369  ncases t2;
 370  nnormalize; #H;
 371  ##[ ##29: napply (λx:P.x)
 372  ##| ##*: napply False_ind;
 373           nchange with (match t1C with [ t1C ⇒ False | _ ⇒ True ]);
 374           nrewrite > H; nnormalize; napply I
 375  ##]
 376 nqed.
 377
 378 ndefinition bitrigesim_destruct30 :
 379 Πt2:bitrigesim.ΠP:Prop.t1D = t2 → match t2 with [ t1D ⇒ P → P | _ ⇒ P ].
 380  #t2; #P;
 381  ncases t2;
 382  nnormalize; #H;
 383  ##[ ##30: napply (λx:P.x)
 384  ##| ##*: napply False_ind;
 385           nchange with (match t1D with [ t1D ⇒ False | _ ⇒ True ]);
 386           nrewrite > H; nnormalize; napply I
 387  ##]
 388 nqed.
 389
 390 ndefinition bitrigesim_destruct31 :
 391 Πt2:bitrigesim.ΠP:Prop.t1E = t2 → match t2 with [ t1E ⇒ P → P | _ ⇒ P ].
 392  #t2; #P;
 393  ncases t2;
 394  nnormalize; #H;
 395  ##[ ##31: napply (λx:P.x)
 396  ##| ##*: napply False_ind;
 397           nchange with (match t1E with [ t1E ⇒ False | _ ⇒ True ]);
 398           nrewrite > H; nnormalize; napply I
 399  ##]
 400 nqed.
 401
 402 ndefinition bitrigesim_destruct32 :
 403 Πt2:bitrigesim.ΠP:Prop.t1F = t2 → match t2 with [ t1F ⇒ P → P | _ ⇒ P ].
 404  #t2; #P;
 405  ncases t2;
 406  nnormalize; #H;
 407  ##[ ##32: napply (λx:P.x)
 408  ##| ##*: napply False_ind;
 409           nchange with (match t1F with [ t1F ⇒ False | _ ⇒ True ]);
 410           nrewrite > H; nnormalize; napply I
 411  ##]
 412 nqed.
 413
 414 ndefinition bitrigesim_destruct_aux ≝
 415 Πt1,t2:bitrigesim.ΠP:Prop.t1 = t2 →
 416  match t1 with
 417   [ t00 ⇒ match t2 with [ t00 ⇒ P → P | _ ⇒ P ]
 418   | t01 ⇒ match t2 with [ t01 ⇒ P → P | _ ⇒ P ]
 419   | t02 ⇒ match t2 with [ t02 ⇒ P → P | _ ⇒ P ]
 420   | t03 ⇒ match t2 with [ t03 ⇒ P → P | _ ⇒ P ]
 421   | t04 ⇒ match t2 with [ t04 ⇒ P → P | _ ⇒ P ]
 422   | t05 ⇒ match t2 with [ t05 ⇒ P → P | _ ⇒ P ]
 423   | t06 ⇒ match t2 with [ t06 ⇒ P → P | _ ⇒ P ]
 424   | t07 ⇒ match t2 with [ t07 ⇒ P → P | _ ⇒ P ]
 425   | t08 ⇒ match t2 with [ t08 ⇒ P → P | _ ⇒ P ]
 426   | t09 ⇒ match t2 with [ t09 ⇒ P → P | _ ⇒ P ]
 427   | t0A ⇒ match t2 with [ t0A ⇒ P → P | _ ⇒ P ]
 428   | t0B ⇒ match t2 with [ t0B ⇒ P → P | _ ⇒ P ]
 429   | t0C ⇒ match t2 with [ t0C ⇒ P → P | _ ⇒ P ]
 430   | t0D ⇒ match t2 with [ t0D ⇒ P → P | _ ⇒ P ]
 431   | t0E ⇒ match t2 with [ t0E ⇒ P → P | _ ⇒ P ]
 432   | t0F ⇒ match t2 with [ t0F ⇒ P → P | _ ⇒ P ]
 433   | t10 ⇒ match t2 with [ t10 ⇒ P → P | _ ⇒ P ]
 434   | t11 ⇒ match t2 with [ t11 ⇒ P → P | _ ⇒ P ]
 435   | t12 ⇒ match t2 with [ t12 ⇒ P → P | _ ⇒ P ]
 436   | t13 ⇒ match t2 with [ t13 ⇒ P → P | _ ⇒ P ]
 437   | t14 ⇒ match t2 with [ t14 ⇒ P → P | _ ⇒ P ]
 438   | t15 ⇒ match t2 with [ t15 ⇒ P → P | _ ⇒ P ]
 439   | t16 ⇒ match t2 with [ t16 ⇒ P → P | _ ⇒ P ]
 440   | t17 ⇒ match t2 with [ t17 ⇒ P → P | _ ⇒ P ]
 441   | t18 ⇒ match t2 with [ t18 ⇒ P → P | _ ⇒ P ]
 442   | t19 ⇒ match t2 with [ t19 ⇒ P → P | _ ⇒ P ]
 443   | t1A ⇒ match t2 with [ t1A ⇒ P → P | _ ⇒ P ]
 444   | t1B ⇒ match t2 with [ t1B ⇒ P → P | _ ⇒ P ]
 445   | t1C ⇒ match t2 with [ t1C ⇒ P → P | _ ⇒ P ]
 446   | t1D ⇒ match t2 with [ t1D ⇒ P → P | _ ⇒ P ]
 447   | t1E ⇒ match t2 with [ t1E ⇒ P → P | _ ⇒ P ]
 448   | t1F ⇒ match t2 with [ t1F ⇒ P → P | _ ⇒ P ]
 449   ].
 450
 451 ndefinition bitrigesim_destruct : bitrigesim_destruct_aux.
 452  #t1;
 453  ncases t1;
 454  ##[ ##1: napply bitrigesim_destruct1
 455  ##| ##2: napply bitrigesim_destruct2
 456  ##| ##3: napply bitrigesim_destruct3
 457  ##| ##4: napply bitrigesim_destruct4
 458  ##| ##5: napply bitrigesim_destruct5
 459  ##| ##6: napply bitrigesim_destruct6
 460  ##| ##7: napply bitrigesim_destruct7
 461  ##| ##8: napply bitrigesim_destruct8
 462  ##| ##9: napply bitrigesim_destruct9
 463  ##| ##10: napply bitrigesim_destruct10
 464  ##| ##11: napply bitrigesim_destruct11
 465  ##| ##12: napply bitrigesim_destruct12
 466  ##| ##13: napply bitrigesim_destruct13
 467  ##| ##14: napply bitrigesim_destruct14
 468  ##| ##15: napply bitrigesim_destruct15
 469  ##| ##16: napply bitrigesim_destruct16
 470  ##| ##17: napply bitrigesim_destruct17
 471  ##| ##18: napply bitrigesim_destruct18
 472  ##| ##19: napply bitrigesim_destruct19
 473  ##| ##20: napply bitrigesim_destruct20
 474  ##| ##21: napply bitrigesim_destruct21
 475  ##| ##22: napply bitrigesim_destruct22
 476  ##| ##23: napply bitrigesim_destruct23
 477  ##| ##24: napply bitrigesim_destruct24
 478  ##| ##25: napply bitrigesim_destruct25
 479  ##| ##26: napply bitrigesim_destruct26
 480  ##| ##27: napply bitrigesim_destruct27
 481  ##| ##28: napply bitrigesim_destruct28
 482  ##| ##29: napply bitrigesim_destruct29
 483  ##| ##30: napply bitrigesim_destruct30
 484  ##| ##31: napply bitrigesim_destruct31
 485  ##| ##32: napply bitrigesim_destruct32
 486  ##]
 487 nqed.
 488
 489 nlemma symmetric_eqbit : symmetricT bitrigesim bool eq_bit.
 490  #t1;
 491  nelim t1;
 492  ##[ ##1: #t2; nelim t2; nnormalize; napply refl_eq
 493  ##| ##2: #t2; nelim t2; nnormalize; napply refl_eq
 494  ##| ##3: #t2; nelim t2; nnormalize; napply refl_eq
 495  ##| ##4: #t2; nelim t2; nnormalize; napply refl_eq
 496  ##| ##5: #t2; nelim t2; nnormalize; napply refl_eq
 497  ##| ##6: #t2; nelim t2; nnormalize; napply refl_eq
 498  ##| ##7: #t2; nelim t2; nnormalize; napply refl_eq
 499  ##| ##8: #t2; nelim t2; nnormalize; napply refl_eq
 500  ##| ##9: #t2; nelim t2; nnormalize; napply refl_eq
 501  ##| ##10: #t2; nelim t2; nnormalize; napply refl_eq
 502  ##| ##11: #t2; nelim t2; nnormalize; napply refl_eq
 503  ##| ##12: #t2; nelim t2; nnormalize; napply refl_eq
 504  ##| ##13: #t2; nelim t2; nnormalize; napply refl_eq
 505  ##| ##14: #t2; nelim t2; nnormalize; napply refl_eq
 506  ##| ##15: #t2; nelim t2; nnormalize; napply refl_eq
 507  ##| ##16: #t2; nelim t2; nnormalize; napply refl_eq
 508  ##| ##17: #t2; nelim t2; nnormalize; napply refl_eq
 509  ##| ##18: #t2; nelim t2; nnormalize; napply refl_eq
 510  ##| ##19: #t2; nelim t2; nnormalize; napply refl_eq
 511  ##| ##20: #t2; nelim t2; nnormalize; napply refl_eq
 512  ##| ##21: #t2; nelim t2; nnormalize; napply refl_eq
 513  ##| ##22: #t2; nelim t2; nnormalize; napply refl_eq
 514  ##| ##23: #t2; nelim t2; nnormalize; napply refl_eq
 515  ##| ##24: #t2; nelim t2; nnormalize; napply refl_eq
 516  ##| ##25: #t2; nelim t2; nnormalize; napply refl_eq
 517  ##| ##26: #t2; nelim t2; nnormalize; napply refl_eq
 518  ##| ##27: #t2; nelim t2; nnormalize; napply refl_eq
 519  ##| ##28: #t2; nelim t2; nnormalize; napply refl_eq
 520  ##| ##29: #t2; nelim t2; nnormalize; napply refl_eq
 521  ##| ##30: #t2; nelim t2; nnormalize; napply refl_eq
 522  ##| ##31: #t2; nelim t2; nnormalize; napply refl_eq
 523  ##| ##32: #t2; nelim t2; nnormalize; napply refl_eq
 524  ##]
 525 nqed.
 526
 527 nlemma eqbit_to_eq1 : ∀t2.eq_bit t00 t2 = true → t00 = t2.
 528  #t2; ncases t2; nnormalize; #H; ##[ ##1: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 529 nqed.
 530
 531 nlemma eqbit_to_eq2 : ∀t2.eq_bit t01 t2 = true → t01 = t2.
 532  #t2; ncases t2; nnormalize; #H; ##[ ##2: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 533 nqed.
 534
 535 nlemma eqbit_to_eq3 : ∀t2.eq_bit t02 t2 = true → t02 = t2.
 536  #t2; ncases t2; nnormalize; #H; ##[ ##3: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 537 nqed.
 538
 539 nlemma eqbit_to_eq4 : ∀t2.eq_bit t03 t2 = true → t03 = t2.
 540  #t2; ncases t2; nnormalize; #H; ##[ ##4: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 541 nqed.
 542
 543 nlemma eqbit_to_eq5 : ∀t2.eq_bit t04 t2 = true → t04 = t2.
 544  #t2; ncases t2; nnormalize; #H; ##[ ##5: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 545 nqed.
 546
 547 nlemma eqbit_to_eq6 : ∀t2.eq_bit t05 t2 = true → t05 = t2.
 548  #t2; ncases t2; nnormalize; #H; ##[ ##6: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 549 nqed.
 550
 551 nlemma eqbit_to_eq7 : ∀t2.eq_bit t06 t2 = true → t06 = t2.
 552  #t2; ncases t2; nnormalize; #H; ##[ ##7: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 553 nqed.
 554
 555 nlemma eqbit_to_eq8 : ∀t2.eq_bit t07 t2 = true → t07 = t2.
 556  #t2; ncases t2; nnormalize; #H; ##[ ##8: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 557 nqed.
 558
 559 nlemma eqbit_to_eq9 : ∀t2.eq_bit t08 t2 = true → t08 = t2.
 560  #t2; ncases t2; nnormalize; #H; ##[ ##9: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 561 nqed.
 562
 563 nlemma eqbit_to_eq10 : ∀t2.eq_bit t09 t2 = true → t09 = t2.
 564  #t2; ncases t2; nnormalize; #H; ##[ ##10: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 565 nqed.
 566
 567 nlemma eqbit_to_eq11 : ∀t2.eq_bit t0A t2 = true → t0A = t2.
 568  #t2; ncases t2; nnormalize; #H; ##[ ##11: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 569 nqed.
 570
 571 nlemma eqbit_to_eq12 : ∀t2.eq_bit t0B t2 = true → t0B = t2.
 572  #t2; ncases t2; nnormalize; #H; ##[ ##12: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 573 nqed.
 574
 575 nlemma eqbit_to_eq13 : ∀t2.eq_bit t0C t2 = true → t0C = t2.
 576  #t2; ncases t2; nnormalize; #H; ##[ ##13: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 577 nqed.
 578
 579 nlemma eqbit_to_eq14 : ∀t2.eq_bit t0D t2 = true → t0D = t2.
 580  #t2; ncases t2; nnormalize; #H; ##[ ##14: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 581 nqed.
 582
 583 nlemma eqbit_to_eq15 : ∀t2.eq_bit t0E t2 = true → t0E = t2.
 584  #t2; ncases t2; nnormalize; #H; ##[ ##15: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 585 nqed.
 586
 587 nlemma eqbit_to_eq16 : ∀t2.eq_bit t0F t2 = true → t0F = t2.
 588  #t2; ncases t2; nnormalize; #H; ##[ ##16: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 589 nqed.
 590
 591 nlemma eqbit_to_eq17 : ∀t2.eq_bit t10 t2 = true → t10 = t2.
 592  #t2; ncases t2; nnormalize; #H; ##[ ##17: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 593 nqed.
 594
 595 nlemma eqbit_to_eq18 : ∀t2.eq_bit t11 t2 = true → t11 = t2.
 596  #t2; ncases t2; nnormalize; #H; ##[ ##18: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 597 nqed.
 598
 599 nlemma eqbit_to_eq19 : ∀t2.eq_bit t12 t2 = true → t12 = t2.
 600  #t2; ncases t2; nnormalize; #H; ##[ ##19: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 601 nqed.
 602
 603 nlemma eqbit_to_eq20 : ∀t2.eq_bit t13 t2 = true → t13 = t2.
 604  #t2; ncases t2; nnormalize; #H; ##[ ##20: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 605 nqed.
 606
 607 nlemma eqbit_to_eq21 : ∀t2.eq_bit t14 t2 = true → t14 = t2.
 608  #t2; ncases t2; nnormalize; #H; ##[ ##21: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 609 nqed.
 610
 611 nlemma eqbit_to_eq22 : ∀t2.eq_bit t15 t2 = true → t15 = t2.
 612  #t2; ncases t2; nnormalize; #H; ##[ ##22: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 613 nqed.
 614
 615 nlemma eqbit_to_eq23 : ∀t2.eq_bit t16 t2 = true → t16 = t2.
 616  #t2; ncases t2; nnormalize; #H; ##[ ##23: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 617 nqed.
 618
 619 nlemma eqbit_to_eq24 : ∀t2.eq_bit t17 t2 = true → t17 = t2.
 620  #t2; ncases t2; nnormalize; #H; ##[ ##24: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 621 nqed.
 622
 623 nlemma eqbit_to_eq25 : ∀t2.eq_bit t18 t2 = true → t18 = t2.
 624  #t2; ncases t2; nnormalize; #H; ##[ ##25: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 625 nqed.
 626
 627 nlemma eqbit_to_eq26 : ∀t2.eq_bit t19 t2 = true → t19 = t2.
 628  #t2; ncases t2; nnormalize; #H; ##[ ##26: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 629 nqed.
 630
 631 nlemma eqbit_to_eq27 : ∀t2.eq_bit t1A t2 = true → t1A = t2.
 632  #t2; ncases t2; nnormalize; #H; ##[ ##27: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 633 nqed.
 634
 635 nlemma eqbit_to_eq28 : ∀t2.eq_bit t1B t2 = true → t1B = t2.
 636  #t2; ncases t2; nnormalize; #H; ##[ ##28: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 637 nqed.
 638
 639 nlemma eqbit_to_eq29 : ∀t2.eq_bit t1C t2 = true → t1C = t2.
 640  #t2; ncases t2; nnormalize; #H; ##[ ##29: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 641 nqed.
 642
 643 nlemma eqbit_to_eq30 : ∀t2.eq_bit t1D t2 = true → t1D = t2.
 644  #t2; ncases t2; nnormalize; #H; ##[ ##30: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 645 nqed.
 646
 647 nlemma eqbit_to_eq31 : ∀t2.eq_bit t1E t2 = true → t1E = t2.
 648  #t2; ncases t2; nnormalize; #H; ##[ ##31: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 649 nqed.
 650
 651 nlemma eqbit_to_eq32 : ∀t2.eq_bit t1F t2 = true → t1F = t2.
 652  #t2; ncases t2; nnormalize; #H; ##[ ##32: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 653 nqed.
 654
 655 nlemma eqbit_to_eq : ∀t1,t2.eq_bit t1 t2 = true → t1 = t2.
 656  #t1;
 657  ncases t1;
 658  ##[ ##1: napply eqbit_to_eq1
 659  ##| ##2: napply eqbit_to_eq2
 660  ##| ##3: napply eqbit_to_eq3
 661  ##| ##4: napply eqbit_to_eq4
 662  ##| ##5: napply eqbit_to_eq5
 663  ##| ##6: napply eqbit_to_eq6
 664  ##| ##7: napply eqbit_to_eq7
 665  ##| ##8: napply eqbit_to_eq8
 666  ##| ##9: napply eqbit_to_eq9
 667  ##| ##10: napply eqbit_to_eq10
 668  ##| ##11: napply eqbit_to_eq11
 669  ##| ##12: napply eqbit_to_eq12
 670  ##| ##13: napply eqbit_to_eq13
 671  ##| ##14: napply eqbit_to_eq14
 672  ##| ##15: napply eqbit_to_eq15
 673  ##| ##16: napply eqbit_to_eq16
 674  ##| ##17: napply eqbit_to_eq17
 675  ##| ##18: napply eqbit_to_eq18
 676  ##| ##19: napply eqbit_to_eq19
 677  ##| ##20: napply eqbit_to_eq20
 678  ##| ##21: napply eqbit_to_eq21
 679  ##| ##22: napply eqbit_to_eq22
 680  ##| ##23: napply eqbit_to_eq23
 681  ##| ##24: napply eqbit_to_eq24
 682  ##| ##25: napply eqbit_to_eq25
 683  ##| ##26: napply eqbit_to_eq26
 684  ##| ##27: napply eqbit_to_eq27
 685  ##| ##28: napply eqbit_to_eq28
 686  ##| ##29: napply eqbit_to_eq29
 687  ##| ##30: napply eqbit_to_eq30
 688  ##| ##31: napply eqbit_to_eq31
 689  ##| ##32: napply eqbit_to_eq32
 690  ##]
 691 nqed.
 692
 693 nlemma eq_to_eqbit1 : ∀t2.t00 = t2 → eq_bit t00 t2 = true.
 694  #t2; ncases t2; nnormalize; #H; ##[ ##1: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 695 nqed.
 696
 697 nlemma eq_to_eqbit2 : ∀t2.t01 = t2 → eq_bit t01 t2 = true.
 698  #t2; ncases t2; nnormalize; #H; ##[ ##2: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 699 nqed.
 700
 701 nlemma eq_to_eqbit3 : ∀t2.t02 = t2 → eq_bit t02 t2 = true.
 702  #t2; ncases t2; nnormalize; #H; ##[ ##3: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 703 nqed.
 704
 705 nlemma eq_to_eqbit4 : ∀t2.t03 = t2 → eq_bit t03 t2 = true.
 706  #t2; ncases t2; nnormalize; #H; ##[ ##4: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 707 nqed.
 708
 709 nlemma eq_to_eqbit5 : ∀t2.t04 = t2 → eq_bit t04 t2 = true.
 710  #t2; ncases t2; nnormalize; #H; ##[ ##5: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 711 nqed.
 712
 713 nlemma eq_to_eqbit6 : ∀t2.t05 = t2 → eq_bit t05 t2 = true.
 714  #t2; ncases t2; nnormalize; #H; ##[ ##6: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 715 nqed.
 716
 717 nlemma eq_to_eqbit7 : ∀t2.t06 = t2 → eq_bit t06 t2 = true.
 718  #t2; ncases t2; nnormalize; #H; ##[ ##7: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 719 nqed.
 720
 721 nlemma eq_to_eqbit8 : ∀t2.t07 = t2 → eq_bit t07 t2 = true.
 722  #t2; ncases t2; nnormalize; #H; ##[ ##8: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 723 nqed.
 724
 725 nlemma eq_to_eqbit9 : ∀t2.t08 = t2 → eq_bit t08 t2 = true.
 726  #t2; ncases t2; nnormalize; #H; ##[ ##9: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 727 nqed.
 728
 729 nlemma eq_to_eqbit10 : ∀t2.t09 = t2 → eq_bit t09 t2 = true.
 730  #t2; ncases t2; nnormalize; #H; ##[ ##10: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 731 nqed.
 732
 733 nlemma eq_to_eqbit11 : ∀t2.t0A = t2 → eq_bit t0A t2 = true.
 734  #t2; ncases t2; nnormalize; #H; ##[ ##11: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 735 nqed.
 736
 737 nlemma eq_to_eqbit12 : ∀t2.t0B = t2 → eq_bit t0B t2 = true.
 738  #t2; ncases t2; nnormalize; #H; ##[ ##12: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 739 nqed.
 740
 741 nlemma eq_to_eqbit13 : ∀t2.t0C = t2 → eq_bit t0C t2 = true.
 742  #t2; ncases t2; nnormalize; #H; ##[ ##13: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 743 nqed.
 744
 745 nlemma eq_to_eqbit14 : ∀t2.t0D = t2 → eq_bit t0D t2 = true.
 746  #t2; ncases t2; nnormalize; #H; ##[ ##14: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 747 nqed.
 748
 749 nlemma eq_to_eqbit15 : ∀t2.t0E = t2 → eq_bit t0E t2 = true.
 750  #t2; ncases t2; nnormalize; #H; ##[ ##15: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 751 nqed.
 752
 753 nlemma eq_to_eqbit16 : ∀t2.t0F = t2 → eq_bit t0F t2 = true.
 754  #t2; ncases t2; nnormalize; #H; ##[ ##16: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 755 nqed.
 756
 757 nlemma eq_to_eqbit17 : ∀t2.t10 = t2 → eq_bit t10 t2 = true.
 758  #t2; ncases t2; nnormalize; #H; ##[ ##17: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 759 nqed.
 760
 761 nlemma eq_to_eqbit18 : ∀t2.t11 = t2 → eq_bit t11 t2 = true.
 762  #t2; ncases t2; nnormalize; #H; ##[ ##18: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 763 nqed.
 764
 765 nlemma eq_to_eqbit19 : ∀t2.t12 = t2 → eq_bit t12 t2 = true.
 766  #t2; ncases t2; nnormalize; #H; ##[ ##19: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 767 nqed.
 768
 769 nlemma eq_to_eqbit20 : ∀t2.t13 = t2 → eq_bit t13 t2 = true.
 770  #t2; ncases t2; nnormalize; #H; ##[ ##20: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 771 nqed.
 772
 773 nlemma eq_to_eqbit21 : ∀t2.t14 = t2 → eq_bit t14 t2 = true.
 774  #t2; ncases t2; nnormalize; #H; ##[ ##21: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 775 nqed.
 776
 777 nlemma eq_to_eqbit22 : ∀t2.t15 = t2 → eq_bit t15 t2 = true.
 778  #t2; ncases t2; nnormalize; #H; ##[ ##22: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 779 nqed.
 780
 781 nlemma eq_to_eqbit23 : ∀t2.t16 = t2 → eq_bit t16 t2 = true.
 782  #t2; ncases t2; nnormalize; #H; ##[ ##23: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 783 nqed.
 784
 785 nlemma eq_to_eqbit24 : ∀t2.t17 = t2 → eq_bit t17 t2 = true.
 786  #t2; ncases t2; nnormalize; #H; ##[ ##24: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 787 nqed.
 788
 789 nlemma eq_to_eqbit25 : ∀t2.t18 = t2 → eq_bit t18 t2 = true.
 790  #t2; ncases t2; nnormalize; #H; ##[ ##25: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 791 nqed.
 792
 793 nlemma eq_to_eqbit26 : ∀t2.t19 = t2 → eq_bit t19 t2 = true.
 794  #t2; ncases t2; nnormalize; #H; ##[ ##26: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 795 nqed.
 796
 797 nlemma eq_to_eqbit27 : ∀t2.t1A = t2 → eq_bit t1A t2 = true.
 798  #t2; ncases t2; nnormalize; #H; ##[ ##27: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 799 nqed.
 800
 801 nlemma eq_to_eqbit28 : ∀t2.t1B = t2 → eq_bit t1B t2 = true.
 802  #t2; ncases t2; nnormalize; #H; ##[ ##28: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 803 nqed.
 804
 805 nlemma eq_to_eqbit29 : ∀t2.t1C = t2 → eq_bit t1C t2 = true.
 806  #t2; ncases t2; nnormalize; #H; ##[ ##29: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 807 nqed.
 808
 809 nlemma eq_to_eqbit30 : ∀t2.t1D = t2 → eq_bit t1D t2 = true.
 810  #t2; ncases t2; nnormalize; #H; ##[ ##30: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 811 nqed.
 812
 813 nlemma eq_to_eqbit31 : ∀t2.t1E = t2 → eq_bit t1E t2 = true.
 814  #t2; ncases t2; nnormalize; #H; ##[ ##31: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 815 nqed.
 816
 817 nlemma eq_to_eqbit32 : ∀t2.t1F = t2 → eq_bit t1F t2 = true.
 818  #t2; ncases t2; nnormalize; #H; ##[ ##32: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 819 nqed.
 820
 821 nlemma eq_to_eqbit : ∀t1,t2.t1 = t2 → eq_bit t1 t2 = true.
 822  #t1;
 823  ncases t1;
 824  ##[ ##1: napply eq_to_eqbit1
 825  ##| ##2: napply eq_to_eqbit2
 826  ##| ##3: napply eq_to_eqbit3
 827  ##| ##4: napply eq_to_eqbit4
 828  ##| ##5: napply eq_to_eqbit5
 829  ##| ##6: napply eq_to_eqbit6
 830  ##| ##7: napply eq_to_eqbit7
 831  ##| ##8: napply eq_to_eqbit8
 832  ##| ##9: napply eq_to_eqbit9
 833  ##| ##10: napply eq_to_eqbit10
 834  ##| ##11: napply eq_to_eqbit11
 835  ##| ##12: napply eq_to_eqbit12
 836  ##| ##13: napply eq_to_eqbit13
 837  ##| ##14: napply eq_to_eqbit14
 838  ##| ##15: napply eq_to_eqbit15
 839  ##| ##16: napply eq_to_eqbit16
 840  ##| ##17: napply eq_to_eqbit17
 841  ##| ##18: napply eq_to_eqbit18
 842  ##| ##19: napply eq_to_eqbit19
 843  ##| ##20: napply eq_to_eqbit20
 844  ##| ##21: napply eq_to_eqbit21
 845  ##| ##22: napply eq_to_eqbit22
 846  ##| ##23: napply eq_to_eqbit23
 847  ##| ##24: napply eq_to_eqbit24
 848  ##| ##25: napply eq_to_eqbit25
 849  ##| ##26: napply eq_to_eqbit26
 850  ##| ##27: napply eq_to_eqbit27
 851  ##| ##28: napply eq_to_eqbit28
 852  ##| ##29: napply eq_to_eqbit29
 853  ##| ##30: napply eq_to_eqbit30
 854  ##| ##31: napply eq_to_eqbit31
 855  ##| ##32: napply eq_to_eqbit32
 856  ##]
 857 nqed.