helm/software/matita/contribs/ng_assembly/universe/exadecim_lib.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 "universe/exadecim.ma".
  24
  25 (* operazioni su EX_UN *)
  26
  27 (* scheletro di funzione a 1 argomento *)
  28 ndefinition farg1_unex ≝
  29 λT:Type.λf1,f2,f3,f4,f5,f6,f7,f8,f9,f10,f11,f12,f13,f14,f15,f16:T.λe2:S_UN EX_UN.
  30  match getelem ? e2 return λx.member_list ? x eq_UN EX_UN = true → T with
  31   [ ux0 ⇒ λq:(true = true).f1   | ux1 ⇒ λq:(true = true).f2
  32   | ux2 ⇒ λq:(true = true).f3   | ux3 ⇒ λq:(true = true).f4
  33   | ux4 ⇒ λq:(true = true).f5   | ux5 ⇒ λq:(true = true).f6
  34   | ux6 ⇒ λq:(true = true).f7   | ux7 ⇒ λq:(true = true).f8
  35   | ux8 ⇒ λq:(true = true).f9   | ux9 ⇒ λq:(true = true).f10
  36   | uxA ⇒ λq:(true = true).f11  | uxB ⇒ λq:(true = true).f12
  37   | uxC ⇒ λq:(true = true).f13  | uxD ⇒ λq:(true = true).f14
  38   | uxE ⇒ λq:(true = true).f15  | uxF ⇒ λq:(true = true).f16
  39   | _ ⇒ λq:(false = true).False_rect_Type0 ? (bool_destruct … q)
  40   ] (getdim1 ? e2).
  41
  42 (* scheletro di funzione a 2 argomenti *)
  43 ndefinition farg2_unex ≝
  44 λT:Type.λf1,f2,f3,f4,f5,f6,f7,f8,f9,f10,f11,f12,f13,f14,f15,f16:S_UN EX_UN → T.λe1:S_UN EX_UN.
  45  match getelem ? e1 return λx.member_list ? x eq_UN EX_UN = true → S_UN EX_UN → T with
  46   [ ux0 ⇒ λp:(true = true).f1
  47   | ux1 ⇒ λp:(true = true).f2
  48   | ux2 ⇒ λp:(true = true).f3
  49   | ux3 ⇒ λp:(true = true).f4
  50   | ux4 ⇒ λp:(true = true).f5
  51   | ux5 ⇒ λp:(true = true).f6
  52   | ux6 ⇒ λp:(true = true).f7
  53   | ux7 ⇒ λp:(true = true).f8
  54   | ux8 ⇒ λp:(true = true).f9
  55   | ux9 ⇒ λp:(true = true).f10
  56   | uxA ⇒ λp:(true = true).f11
  57   | uxB ⇒ λp:(true = true).f12
  58   | uxC ⇒ λp:(true = true).f13
  59   | uxD ⇒ λp:(true = true).f14
  60   | uxE ⇒ λp:(true = true).f15
  61   | uxF ⇒ λp:(true = true).f16
  62   | _ ⇒ λp:(false = true).False_rect_Type0 ? (bool_destruct … p)
  63   ] (getdim1 ? e1).
  64
  65 (* scheletro di funzione a 2 argomenti simmetrica *)
  66 ndefinition farg2sym_unex ≝
  67 λT:Type.
  68 λf00,f01,f02,f03,f04,f05,f06,f07,f08,f09,f0A,f0B,f0C,f0D,f0E,f0F:T.
  69 λf11,f12,f13,f14,f15,f16,f17,f18,f19,f1A,f1B,f1C,f1D,f1E,f1F:T.
  70 λf22,f23,f24,f25,f26,f27,f28,f29,f2A,f2B,f2C,f2D,f2E,f2F:T.
  71 λf33,f34,f35,f36,f37,f38,f39,f3A,f3B,f3C,f3D,f3E,f3F:T.
  72 λf44,f45,f46,f47,f48,f49,f4A,f4B,f4C,f4D,f4E,f4F:T.
  73 λf55,f56,f57,f58,f59,f5A,f5B,f5C,f5D,f5E,f5F:T.
  74 λf66,f67,f68,f69,f6A,f6B,f6C,f6D,f6E,f6F:T.
  75 λf77,f78,f79,f7A,f7B,f7C,f7D,f7E,f7F:T.
  76 λf88,f89,f8A,f8B,f8C,f8D,f8E,f8F:T.
  77 λf99,f9A,f9B,f9C,f9D,f9E,f9F:T.
  78 λfAA,fAB,fAC,fAD,fAE,fAF:T.
  79 λfBB,fBC,fBD,fBE,fBF:T.
  80 λfCC,fCD,fCE,fCF:T.
  81 λfDD,fDE,fDF:T.
  82 λfEE,fEF:T.
  83 λfFF:T.
  84  farg2_unex ?
  85   (farg1_unex ? f00 f01 f02 f03 f04 f05 f06 f07 f08 f09 f0A f0B f0C f0D f0E f0F)
  86   (farg1_unex ? f01 f11 f12 f13 f14 f15 f16 f17 f18 f19 f1A f1B f1C f1D f1E f1F)
  87   (farg1_unex ? f02 f12 f22 f23 f24 f25 f26 f27 f28 f29 f2A f2B f2C f2D f2E f2F)
  88   (farg1_unex ? f03 f13 f23 f33 f34 f35 f36 f37 f38 f39 f3A f3B f3C f3D f3E f3F)
  89   (farg1_unex ? f04 f14 f24 f34 f44 f45 f46 f47 f48 f49 f4A f4B f4C f4D f4E f4F)
  90   (farg1_unex ? f05 f15 f25 f35 f45 f55 f56 f57 f58 f59 f5A f5B f5C f5D f5E f5F)
  91   (farg1_unex ? f06 f16 f26 f36 f46 f56 f66 f67 f68 f69 f6A f6B f6C f6D f6E f6F)
  92   (farg1_unex ? f07 f17 f27 f37 f47 f57 f67 f77 f78 f79 f7A f7B f7C f7D f7E f7F)
  93   (farg1_unex ? f08 f18 f28 f38 f48 f58 f68 f78 f88 f89 f8A f8B f8C f8D f8E f8F)
  94   (farg1_unex ? f09 f19 f29 f39 f49 f59 f69 f79 f89 f99 f9A f9B f9C f9D f9E f9F)
  95   (farg1_unex ? f0A f1A f2A f3A f4A f5A f6A f7A f8A f9A fAA fAB fAC fAD fAE fAF)
  96   (farg1_unex ? f0B f1B f2B f3B f4B f5B f6B f7B f8B f9B fAB fBB fBC fBD fBE fBF)
  97   (farg1_unex ? f0C f1C f2C f3C f4C f5C f6C f7C f8C f9C fAC fBC fCC fCD fCE fCF)
  98   (farg1_unex ? f0D f1D f2D f3D f4D f5D f6D f7D f8D f9D fAD fBD fCD fDD fDE fDF)
  99   (farg1_unex ? f0E f1E f2E f3E f4E f5E f6E f7E f8E f9E fAE fBE fCE fDE fEE fEF)
 100   (farg1_unex ? f0F f1F f2F f3F f4F f5F f6F f7F f8F f9F fAF fBF fCF fDF fEF fFF).
 101
 102 (* operatore = *)
 103 ndefinition eq_unex ≝ λe1,e2:S_UN EX_UN.eq_SUN ? e1 e2.
 104
 105 (* operatore < *)
 106 ndefinition lt_unex ≝
 107  farg2_unex ?
 108   (farg1_unex ? false true  true  true  true  true  true  true  true  true  true  true  true  true  true  true)
 109   (farg1_unex ? false false true  true  true  true  true  true  true  true  true  true  true  true  true  true)
 110   (farg1_unex ? false false false true  true  true  true  true  true  true  true  true  true  true  true  true)
 111   (farg1_unex ? false false false false true  true  true  true  true  true  true  true  true  true  true  true)
 112   (farg1_unex ? false false false false false true  true  true  true  true  true  true  true  true  true  true)
 113   (farg1_unex ? false false false false false false true  true  true  true  true  true  true  true  true  true)
 114   (farg1_unex ? false false false false false false false true  true  true  true  true  true  true  true  true)
 115   (farg1_unex ? false false false false false false false false true  true  true  true  true  true  true  true)
 116   (farg1_unex ? false false false false false false false false false true  true  true  true  true  true  true)
 117   (farg1_unex ? false false false false false false false false false false true  true  true  true  true  true)
 118   (farg1_unex ? false false false false false false false false false false false true  true  true  true  true)
 119   (farg1_unex ? false false false false false false false false false false false false true  true  true  true)
 120   (farg1_unex ? false false false false false false false false false false false false false true  true  true)
 121   (farg1_unex ? false false false false false false false false false false false false false false true  true)
 122   (farg1_unex ? false false false false false false false false false false false false false false false true)
 123   (farg1_unex ? false false false false false false false false false false false false false false false false).
 124
 125 (* operatore ≤ *)
 126 ndefinition le_unex ≝
 127  farg2_unex ?
 128   (farg1_unex ? true  true  true  true  true  true  true  true  true  true  true  true  true  true  true  true)
 129   (farg1_unex ? false true  true  true  true  true  true  true  true  true  true  true  true  true  true  true)
 130   (farg1_unex ? false false true  true  true  true  true  true  true  true  true  true  true  true  true  true)
 131   (farg1_unex ? false false false true  true  true  true  true  true  true  true  true  true  true  true  true)
 132   (farg1_unex ? false false false false true  true  true  true  true  true  true  true  true  true  true  true)
 133   (farg1_unex ? false false false false false true  true  true  true  true  true  true  true  true  true  true)
 134   (farg1_unex ? false false false false false false true  true  true  true  true  true  true  true  true  true)
 135   (farg1_unex ? false false false false false false false true  true  true  true  true  true  true  true  true)
 136   (farg1_unex ? false false false false false false false false true  true  true  true  true  true  true  true)
 137   (farg1_unex ? false false false false false false false false false true  true  true  true  true  true  true)
 138   (farg1_unex ? false false false false false false false false false false true  true  true  true  true  true)
 139   (farg1_unex ? false false false false false false false false false false false true  true  true  true  true)
 140   (farg1_unex ? false false false false false false false false false false false false true  true  true  true)
 141   (farg1_unex ? false false false false false false false false false false false false false true  true  true)
 142   (farg1_unex ? false false false false false false false false false false false false false false true  true)
 143   (farg1_unex ? false false false false false false false false false false false false false false false true).
 144
 145 (* operatore > *)
 146 ndefinition gt_unex ≝ λe1,e2:S_UN EX_UN.⊖(le_unex e1 e2).
 147
 148 (* operatore ≥ *)
 149 ndefinition ge_unex ≝ λe1,e2:S_UN EX_UN.⊖(lt_unex e1 e2).
 150
 151 (* opeartore and : simmetrico per costruzione *)
 152 ndefinition and_unex ≝
 153  farg2sym_unex ?
 154   un_x0 un_x0 un_x0 un_x0 un_x0 un_x0 un_x0 un_x0 un_x0 un_x0 un_x0 un_x0 un_x0 un_x0 un_x0 un_x0
 155   un_x1 un_x0 un_x1 un_x0 un_x1 un_x0 un_x1 un_x0 un_x1 un_x0 un_x1 un_x0 un_x1 un_x0 un_x1
 156   un_x2 un_x2 un_x0 un_x0 un_x2 un_x2 un_x0 un_x0 un_x2 un_x2 un_x0 un_x0 un_x2 un_x2
 157   un_x3 un_x0 un_x1 un_x2 un_x3 un_x0 un_x1 un_x2 un_x3 un_x0 un_x1 un_x2 un_x3
 158   un_x4 un_x4 un_x4 un_x4 un_x0 un_x0 un_x0 un_x0 un_x4 un_x4 un_x4 un_x4
 159   un_x5 un_x4 un_x5 un_x0 un_x1 un_x0 un_x1 un_x4 un_x5 un_x4 un_x5
 160   un_x6 un_x6 un_x0 un_x0 un_x2 un_x2 un_x4 un_x4 un_x6 un_x6
 161   un_x7 un_x0 un_x1 un_x2 un_x3 un_x4 un_x5 un_x6 un_x7
 162   un_x8 un_x8 un_x8 un_x8 un_x8 un_x8 un_x8 un_x8
 163   un_x9 un_x8 un_x9 un_x8 un_x9 un_x8 un_x9
 164   un_xA un_xA un_x8 un_x8 un_xA un_xA
 165   un_xB un_x8 un_x9 un_xA un_xB
 166   un_xC un_xC un_xC un_xC
 167   un_xD un_xC un_xD
 168   un_xE un_xE
 169   un_xF.
 170
 171 (*
 172  esiste una regola semplice per ottenere associativo per costruzione?
 173  ragionando in matrice simmetrico e' : a(i,j) = a(j,i) → A = trasposta(A)
 174  ragionando in matrice associativo e' : a(a(i,j),k) = a(i,a(j,k)) → come espresso?
 175
 176 nlemma pippo : un_x3 = (and_unex un_x3 un_xF).
 177  nnormalize;
 178  perche' non riduce?
 179
 180 nlemma symmetric_farg2unex1 :
 181  ∀T:Type.
 182  ∀f00,f01,f02,f03,f04,f05,f06,f07,f08,f09,f0A,f0B,f0C,f0D,f0E,f0F:T.
 183  ∀f11,f12,f13,f14,f15,f16,f17,f18,f19,f1A,f1B,f1C,f1D,f1E,f1F:T.
 184  ∀f22,f23,f24,f25,f26,f27,f28,f29,f2A,f2B,f2C,f2D,f2E,f2F:T.
 185  ∀f33,f34,f35,f36,f37,f38,f39,f3A,f3B,f3C,f3D,f3E,f3F:T.
 186  ∀f44,f45,f46,f47,f48,f49,f4A,f4B,f4C,f4D,f4E,f4F:T.
 187  ∀f55,f56,f57,f58,f59,f5A,f5B,f5C,f5D,f5E,f5F:T.
 188  ∀f66,f67,f68,f69,f6A,f6B,f6C,f6D,f6E,f6F:T.
 189  ∀f77,f78,f79,f7A,f7B,f7C,f7D,f7E,f7F:T.
 190  ∀f88,f89,f8A,f8B,f8C,f8D,f8E,f8F:T.
 191  ∀f99,f9A,f9B,f9C,f9D,f9E,f9F:T.
 192  ∀fAA,fAB,fAC,fAD,fAE,fAF:T.
 193  ∀fBB,fBC,fBD,fBE,fBF:T.
 194  ∀fCC,fCD,fCE,fCF:T.
 195  ∀fDD,fDE,fDF:T.
 196  ∀fEE,fEF:T.
 197  ∀fFF:T.
 198  ∀dim1.∀dim2.∀y:S_UN EX_UN.
 199   (fsym_unex T f00 f01 f02 f03 f04 f05 f06 f07 f08 f09 f0A f0B f0C f0D f0E f0F
 200                f11 f12 f13 f14 f15 f16 f17 f18 f19 f1A f1B f1C f1D f1E f1F
 201                f22 f23 f24 f25 f26 f27 f28 f29 f2A f2B f2C f2D f2E f2F
 202                f33 f34 f35 f36 f37 f38 f39 f3A f3B f3C f3D f3E f3F
 203                f44 f45 f46 f47 f48 f49 f4A f4B f4C f4D f4E f4F
 204                f55 f56 f57 f58 f59 f5A f5B f5C f5D f5E f5F
 205                f66 f67 f68 f69 f6A f6B f6C f6D f6E f6F
 206                f77 f78 f79 f7A f7B f7C f7D f7E f7F
 207                f88 f89 f8A f8B f8C f8D f8E f8F
 208                f99 f9A f9B f9C f9D f9E f9F
 209                fAA fAB fAC fAD fAE fAF
 210                fBB fBC fBD fBE fBF
 211                fCC fCD fCE fCF
 212                fDD fDE fDF
 213                fEE fEF
 214                fFF
 215                (S_EL EX_UN ux0 dim1 dim2) y) =
 216   (fsym_unex T f00 f01 f02 f03 f04 f05 f06 f07 f08 f09 f0A f0B f0C f0D f0E f0F
 217                f11 f12 f13 f14 f15 f16 f17 f18 f19 f1A f1B f1C f1D f1E f1F
 218                f22 f23 f24 f25 f26 f27 f28 f29 f2A f2B f2C f2D f2E f2F
 219                f33 f34 f35 f36 f37 f38 f39 f3A f3B f3C f3D f3E f3F
 220                f44 f45 f46 f47 f48 f49 f4A f4B f4C f4D f4E f4F
 221                f55 f56 f57 f58 f59 f5A f5B f5C f5D f5E f5F
 222                f66 f67 f68 f69 f6A f6B f6C f6D f6E f6F
 223                f77 f78 f79 f7A f7B f7C f7D f7E f7F
 224                f88 f89 f8A f8B f8C f8D f8E f8F
 225                f99 f9A f9B f9C f9D f9E f9F
 226                fAA fAB fAC fAD fAE fAF
 227                fBB fBC fBD fBE fBF
 228                fCC fCD fCE fCF
 229                fDD fDE fDF
 230                fEE fEF
 231                fFF
 232                y (S_EL EX_UN ux0 dim1 dim2)).
 233  #T;
 234  #f00; #f01; #f02; #f03; #f04; #f05; #f06; #f07; #f08; #f09; #f0A; #f0B; #f0C; #f0D; #f0E; #f0F;
 235  #f11; #f12; #f13; #f14; #f15; #f16; #f17; #f18; #f19; #f1A; #f1B; #f1C; #f1D; #f1E; #f1F;
 236  #f22; #f23; #f24; #f25; #f26; #f27; #f28; #f29; #f2A; #f2B; #f2C; #f2D; #f2E; #f2F;
 237  #f33; #f34; #f35; #f36; #f37; #f38; #f39; #f3A; #f3B; #f3C; #f3D; #f3E; #f3F;
 238  #f44; #f45; #f46; #f47; #f48; #f49; #f4A; #f4B; #f4C; #f4D; #f4E; #f4F;
 239  #f55; #f56; #f57; #f58; #f59; #f5A; #f5B; #f5C; #f5D; #f5E; #f5F;
 240  #f66; #f67; #f68; #f69; #f6A; #f6B; #f6C; #f6D; #f6E; #f6F;
 241  #f77; #f78; #f79; #f7A; #f7B; #f7C; #f7D; #f7E; #f7F;
 242  #f88; #f89; #f8A; #f8B; #f8C; #f8D; #f8E; #f8F;
 243  #f99; #f9A; #f9B; #f9C; #f9D; #f9E; #f9F;
 244  #fAA; #fAB; #fAC; #fAD; #fAE; #fAF;
 245  #fBB; #fBC; #fBD; #fBE; #fBF;
 246  #fCC; #fCD; #fCE; #fCF;
 247  #fDD; #fDE; #fDF;
 248  #fEE; #fEF;
 249  #fFF;
 250  #dim11; #dim12; #y; nelim y;
 251  ##[ ##2: #F; nelim F
 252  ##| ##1: #u; ncases u;
 253           ##[ ##13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28: #dim21; #dim22; nnormalize; napply refl_eq
 254           ##| ##*: #dim21; nnormalize in dim21:(%); napply (bool_destruct … dim21)
 255           ##]
 256  ##]
 257 nqed.
 258
 259 ... e cosi via fino a
 260
 261 nlemma symmetric_farg2unex :
 262  ∀T:Type.
 263  ∀f00,f01,f02,f03,f04,f05,f06,f07,f08,f09,f0A,f0B,f0C,f0D,f0E,f0F:T.
 264  ∀f11,f12,f13,f14,f15,f16,f17,f18,f19,f1A,f1B,f1C,f1D,f1E,f1F:T.
 265  ∀f22,f23,f24,f25,f26,f27,f28,f29,f2A,f2B,f2C,f2D,f2E,f2F:T.
 266  ∀f33,f34,f35,f36,f37,f38,f39,f3A,f3B,f3C,f3D,f3E,f3F:T.
 267  ∀f44,f45,f46,f47,f48,f49,f4A,f4B,f4C,f4D,f4E,f4F:T.
 268  ∀f55,f56,f57,f58,f59,f5A,f5B,f5C,f5D,f5E,f5F:T.
 269  ∀f66,f67,f68,f69,f6A,f6B,f6C,f6D,f6E,f6F:T.
 270  ∀f77,f78,f79,f7A,f7B,f7C,f7D,f7E,f7F:T.
 271  ∀f88,f89,f8A,f8B,f8C,f8D,f8E,f8F:T.
 272  ∀f99,f9A,f9B,f9C,f9D,f9E,f9F:T.
 273  ∀fAA,fAB,fAC,fAD,fAE,fAF:T.
 274  ∀fBB,fBC,fBD,fBE,fBF:T.
 275  ∀fCC,fCD,fCE,fCF:T.
 276  ∀fDD,fDE,fDF:T.
 277  ∀fEE,fEF:T.
 278  ∀fFF:T.
 279  ∀x,y:S_UN EX_UN.
 280   (fsym_unex T f00 f01 f02 f03 f04 f05 f06 f07 f08 f09 f0A f0B f0C f0D f0E f0F
 281                f11 f12 f13 f14 f15 f16 f17 f18 f19 f1A f1B f1C f1D f1E f1F
 282                f22 f23 f24 f25 f26 f27 f28 f29 f2A f2B f2C f2D f2E f2F
 283                f33 f34 f35 f36 f37 f38 f39 f3A f3B f3C f3D f3E f3F
 284                f44 f45 f46 f47 f48 f49 f4A f4B f4C f4D f4E f4F
 285                f55 f56 f57 f58 f59 f5A f5B f5C f5D f5E f5F
 286                f66 f67 f68 f69 f6A f6B f6C f6D f6E f6F
 287                f77 f78 f79 f7A f7B f7C f7D f7E f7F
 288                f88 f89 f8A f8B f8C f8D f8E f8F
 289                f99 f9A f9B f9C f9D f9E f9F
 290                fAA fAB fAC fAD fAE fAF
 291                fBB fBC fBD fBE fBF
 292                fCC fCD fCE fCF
 293                fDD fDE fDF
 294                fEE fEF
 295                fFF
 296                x y) =
 297   (fsym_unex T f00 f01 f02 f03 f04 f05 f06 f07 f08 f09 f0A f0B f0C f0D f0E f0F
 298                f11 f12 f13 f14 f15 f16 f17 f18 f19 f1A f1B f1C f1D f1E f1F
 299                f22 f23 f24 f25 f26 f27 f28 f29 f2A f2B f2C f2D f2E f2F
 300                f33 f34 f35 f36 f37 f38 f39 f3A f3B f3C f3D f3E f3F
 301                f44 f45 f46 f47 f48 f49 f4A f4B f4C f4D f4E f4F
 302                f55 f56 f57 f58 f59 f5A f5B f5C f5D f5E f5F
 303                f66 f67 f68 f69 f6A f6B f6C f6D f6E f6F
 304                f77 f78 f79 f7A f7B f7C f7D f7E f7F
 305                f88 f89 f8A f8B f8C f8D f8E f8F
 306                f99 f9A f9B f9C f9D f9E f9F
 307                fAA fAB fAC fAD fAE fAF
 308                fBB fBC fBD fBE fBF
 309                fCC fCD fCE fCF
 310                fDD fDE fDF
 311                fEE fEF
 312                fFF
 313                y x).
 314  #T;
 315  #f00; #f01; #f02; #f03; #f04; #f05; #f06; #f07; #f08; #f09; #f0A; #f0B; #f0C; #f0D; #f0E; #f0F;
 316  #f11; #f12; #f13; #f14; #f15; #f16; #f17; #f18; #f19; #f1A; #f1B; #f1C; #f1D; #f1E; #f1F;
 317  #f22; #f23; #f24; #f25; #f26; #f27; #f28; #f29; #f2A; #f2B; #f2C; #f2D; #f2E; #f2F;
 318  #f33; #f34; #f35; #f36; #f37; #f38; #f39; #f3A; #f3B; #f3C; #f3D; #f3E; #f3F;
 319  #f44; #f45; #f46; #f47; #f48; #f49; #f4A; #f4B; #f4C; #f4D; #f4E; #f4F;
 320  #f55; #f56; #f57; #f58; #f59; #f5A; #f5B; #f5C; #f5D; #f5E; #f5F;
 321  #f66; #f67; #f68; #f69; #f6A; #f6B; #f6C; #f6D; #f6E; #f6F;
 322  #f77; #f78; #f79; #f7A; #f7B; #f7C; #f7D; #f7E; #f7F;
 323  #f88; #f89; #f8A; #f8B; #f8C; #f8D; #f8E; #f8F;
 324  #f99; #f9A; #f9B; #f9C; #f9D; #f9E; #f9F;
 325  #fAA; #fAB; #fAC; #fAD; #fAE; #fAF;
 326  #fBB; #fBC; #fBD; #fBE; #fBF;
 327  #fCC; #fCD; #fCE; #fCF;
 328  #fDD; #fDE; #fDF;
 329  #fEE; #fEF;
 330  #fFF;
 331  #x; nelim x;
 332  ##[ ##2: #F; nelim F
 333  ##| ##1: #u; ncases u;
 334           ##[ ##13: #dim1; #dim2; napply (sym_unex1 T … dim1 dim2)
 335           ##| ##14: #dim1; #dim2; napply (sym_unex1 T … dim1 dim2)
 336           ##| ##15: #dim1; #dim2; napply (sym_unex1 T … dim1 dim2)
 337           ##| ##16: #dim1; #dim2; napply (sym_unex1 T … dim1 dim2)
 338           ##| ##17: #dim1; #dim2; napply (sym_unex1 T … dim1 dim2)
 339           ##| ##18: #dim1; #dim2; napply (sym_unex1 T … dim1 dim2)
 340           ##| ##19: #dim1; #dim2; napply (sym_unex1 T … dim1 dim2)
 341           ##| ##20: #dim1; #dim2; napply (sym_unex1 T … dim1 dim2)
 342           ##| ##21: #dim1; #dim2; napply (sym_unex1 T … dim1 dim2)
 343           ##| ##22: #dim1; #dim2; napply (sym_unex1 T … dim1 dim2)
 344           ##| ##23: #dim1; #dim2; napply (sym_unex1 T … dim1 dim2)
 345           ##| ##24: #dim1; #dim2; napply (sym_unex1 T … dim1 dim2)
 346           ##| ##25: #dim1; #dim2; napply (sym_unex1 T … dim1 dim2)
 347           ##| ##26: #dim1; #dim2; napply (sym_unex1 T … dim1 dim2)
 348           ##| ##27: #dim1; #dim2; napply (sym_unex1 T … dim1 dim2)
 349           ##| ##28: #dim1; #dim2; napply (sym_unex1 T … dim1 dim2)
 350           ##| ##*: #dim1; nnormalize in dim1:(%) napply (bool_destruct … dim1)
 351           ##]
 352  ##]
 353 nqed.
 354 *)