From: Cosimo Oliboni <??>
Date: Fri, 14 Aug 2009 01:45:24 +0000 (+0000)
Subject:  freescale porting, work in progress
X-Git-Tag: make_still_working~3544
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=cad56a7b9eadce5aef71c5b14192181a847dde27;p=helm.git

 freescale porting, work in progress
---

diff --git a/helm/software/matita/contribs/ng_assembly/depends b/helm/software/matita/contribs/ng_assembly/depends
index 26c8f7e8d..bb7ca3697 100644
--- a/helm/software/matita/contribs/ng_assembly/depends
+++ b/helm/software/matita/contribs/ng_assembly/depends
@@ -22,6 +22,7 @@ freescale/load_write.ma freescale/model.ma freescale/translation.ma
 common/nat_lemmas.ma common/nat.ma num/bool_lemmas.ma
 freescale/table_RS08.ma common/list.ma freescale/opcode_base.ma
 common/list_utility_lemmas.ma common/list_lemmas.ma common/list_utility.ma
+universe/exadecim_lib.ma universe/exadecim.ma
 freescale/table_RS08_tests.ma freescale/opcode.ma freescale/table_RS08.ma
 universe/quatern.ma universe/universe.ma
 universe/ascii.ma universe/universe.ma
diff --git a/helm/software/matita/contribs/ng_assembly/universe/exadecim_lib.ma b/helm/software/matita/contribs/ng_assembly/universe/exadecim_lib.ma
new file mode 100755
index 000000000..c034d83b7
--- /dev/null
+++ b/helm/software/matita/contribs/ng_assembly/universe/exadecim_lib.ma
@@ -0,0 +1,354 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* ********************************************************************** *)
+(*                          Progetto FreeScale                            *)
+(*                                                                        *)
+(*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
+(*   Ultima modifica: 05/08/2009                                          *)
+(*                                                                        *)
+(* ********************************************************************** *)
+
+include "universe/exadecim.ma".
+
+(* operazioni su EX_UN *)
+
+(* scheletro di funzione a 1 argomento *)
+ndefinition farg1_unex ≝
+λT:Type.λf1,f2,f3,f4,f5,f6,f7,f8,f9,f10,f11,f12,f13,f14,f15,f16:T.λe2:S_UN EX_UN.
+ match getelem ? e2 return λx.member_list ? x eq_UN EX_UN = true → T with
+  [ ux0 ⇒ λq:(true = true).f1   | ux1 ⇒ λq:(true = true).f2
+  | ux2 ⇒ λq:(true = true).f3   | ux3 ⇒ λq:(true = true).f4
+  | ux4 ⇒ λq:(true = true).f5   | ux5 ⇒ λq:(true = true).f6
+  | ux6 ⇒ λq:(true = true).f7   | ux7 ⇒ λq:(true = true).f8
+  | ux8 ⇒ λq:(true = true).f9   | ux9 ⇒ λq:(true = true).f10
+  | uxA ⇒ λq:(true = true).f11  | uxB ⇒ λq:(true = true).f12
+  | uxC ⇒ λq:(true = true).f13  | uxD ⇒ λq:(true = true).f14
+  | uxE ⇒ λq:(true = true).f15  | uxF ⇒ λq:(true = true).f16
+  | _ ⇒ λq:(false = true).False_rect_Type0 ? (bool_destruct … q)
+  ] (getdim1 ? e2).
+
+(* scheletro di funzione a 2 argomenti *)
+ndefinition farg2_unex ≝
+λ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.
+ match getelem ? e1 return λx.member_list ? x eq_UN EX_UN = true → S_UN EX_UN → T with
+  [ ux0 ⇒ λp:(true = true).f1
+  | ux1 ⇒ λp:(true = true).f2
+  | ux2 ⇒ λp:(true = true).f3
+  | ux3 ⇒ λp:(true = true).f4
+  | ux4 ⇒ λp:(true = true).f5
+  | ux5 ⇒ λp:(true = true).f6
+  | ux6 ⇒ λp:(true = true).f7
+  | ux7 ⇒ λp:(true = true).f8
+  | ux8 ⇒ λp:(true = true).f9
+  | ux9 ⇒ λp:(true = true).f10
+  | uxA ⇒ λp:(true = true).f11
+  | uxB ⇒ λp:(true = true).f12
+  | uxC ⇒ λp:(true = true).f13
+  | uxD ⇒ λp:(true = true).f14
+  | uxE ⇒ λp:(true = true).f15
+  | uxF ⇒ λp:(true = true).f16
+  | _ ⇒ λp:(false = true).False_rect_Type0 ? (bool_destruct … p)
+  ] (getdim1 ? e1).
+
+(* scheletro di funzione a 2 argomenti simmetrica *)
+ndefinition farg2sym_unex ≝
+λT:Type.
+λf00,f01,f02,f03,f04,f05,f06,f07,f08,f09,f0A,f0B,f0C,f0D,f0E,f0F:T.
+λf11,f12,f13,f14,f15,f16,f17,f18,f19,f1A,f1B,f1C,f1D,f1E,f1F:T.
+λf22,f23,f24,f25,f26,f27,f28,f29,f2A,f2B,f2C,f2D,f2E,f2F:T.
+λf33,f34,f35,f36,f37,f38,f39,f3A,f3B,f3C,f3D,f3E,f3F:T.
+λf44,f45,f46,f47,f48,f49,f4A,f4B,f4C,f4D,f4E,f4F:T.
+λf55,f56,f57,f58,f59,f5A,f5B,f5C,f5D,f5E,f5F:T.
+λf66,f67,f68,f69,f6A,f6B,f6C,f6D,f6E,f6F:T.
+λf77,f78,f79,f7A,f7B,f7C,f7D,f7E,f7F:T.
+λf88,f89,f8A,f8B,f8C,f8D,f8E,f8F:T.
+λf99,f9A,f9B,f9C,f9D,f9E,f9F:T.
+λfAA,fAB,fAC,fAD,fAE,fAF:T.
+λfBB,fBC,fBD,fBE,fBF:T.
+λfCC,fCD,fCE,fCF:T.
+λfDD,fDE,fDF:T.
+λfEE,fEF:T.
+λfFF:T.
+ farg2_unex ?
+  (farg1_unex ? f00 f01 f02 f03 f04 f05 f06 f07 f08 f09 f0A f0B f0C f0D f0E f0F)
+  (farg1_unex ? f01 f11 f12 f13 f14 f15 f16 f17 f18 f19 f1A f1B f1C f1D f1E f1F)
+  (farg1_unex ? f02 f12 f22 f23 f24 f25 f26 f27 f28 f29 f2A f2B f2C f2D f2E f2F)
+  (farg1_unex ? f03 f13 f23 f33 f34 f35 f36 f37 f38 f39 f3A f3B f3C f3D f3E f3F)
+  (farg1_unex ? f04 f14 f24 f34 f44 f45 f46 f47 f48 f49 f4A f4B f4C f4D f4E f4F)
+  (farg1_unex ? f05 f15 f25 f35 f45 f55 f56 f57 f58 f59 f5A f5B f5C f5D f5E f5F)
+  (farg1_unex ? f06 f16 f26 f36 f46 f56 f66 f67 f68 f69 f6A f6B f6C f6D f6E f6F)
+  (farg1_unex ? f07 f17 f27 f37 f47 f57 f67 f77 f78 f79 f7A f7B f7C f7D f7E f7F)
+  (farg1_unex ? f08 f18 f28 f38 f48 f58 f68 f78 f88 f89 f8A f8B f8C f8D f8E f8F)
+  (farg1_unex ? f09 f19 f29 f39 f49 f59 f69 f79 f89 f99 f9A f9B f9C f9D f9E f9F)
+  (farg1_unex ? f0A f1A f2A f3A f4A f5A f6A f7A f8A f9A fAA fAB fAC fAD fAE fAF)
+  (farg1_unex ? f0B f1B f2B f3B f4B f5B f6B f7B f8B f9B fAB fBB fBC fBD fBE fBF)
+  (farg1_unex ? f0C f1C f2C f3C f4C f5C f6C f7C f8C f9C fAC fBC fCC fCD fCE fCF)
+  (farg1_unex ? f0D f1D f2D f3D f4D f5D f6D f7D f8D f9D fAD fBD fCD fDD fDE fDF)
+  (farg1_unex ? f0E f1E f2E f3E f4E f5E f6E f7E f8E f9E fAE fBE fCE fDE fEE fEF)
+  (farg1_unex ? f0F f1F f2F f3F f4F f5F f6F f7F f8F f9F fAF fBF fCF fDF fEF fFF).
+
+(* operatore = *)
+ndefinition eq_unex ≝ λe1,e2:S_UN EX_UN.eq_SUN ? e1 e2.
+
+(* operatore < *) 
+ndefinition lt_unex ≝
+ farg2_unex ?
+  (farg1_unex ? false true  true  true  true  true  true  true  true  true  true  true  true  true  true  true)
+  (farg1_unex ? false false true  true  true  true  true  true  true  true  true  true  true  true  true  true)
+  (farg1_unex ? false false false true  true  true  true  true  true  true  true  true  true  true  true  true)
+  (farg1_unex ? false false false false true  true  true  true  true  true  true  true  true  true  true  true)
+  (farg1_unex ? false false false false false true  true  true  true  true  true  true  true  true  true  true)
+  (farg1_unex ? false false false false false false true  true  true  true  true  true  true  true  true  true)
+  (farg1_unex ? false false false false false false false true  true  true  true  true  true  true  true  true)
+  (farg1_unex ? false false false false false false false false true  true  true  true  true  true  true  true)
+  (farg1_unex ? false false false false false false false false false true  true  true  true  true  true  true)
+  (farg1_unex ? false false false false false false false false false false true  true  true  true  true  true)
+  (farg1_unex ? false false false false false false false false false false false true  true  true  true  true)
+  (farg1_unex ? false false false false false false false false false false false false true  true  true  true)
+  (farg1_unex ? false false false false false false false false false false false false false true  true  true)
+  (farg1_unex ? false false false false false false false false false false false false false false true  true)
+  (farg1_unex ? false false false false false false false false false false false false false false false true)
+  (farg1_unex ? false false false false false false false false false false false false false false false false).
+
+(* operatore ≤ *)
+ndefinition le_unex ≝
+ farg2_unex ?
+  (farg1_unex ? true  true  true  true  true  true  true  true  true  true  true  true  true  true  true  true)
+  (farg1_unex ? false true  true  true  true  true  true  true  true  true  true  true  true  true  true  true)
+  (farg1_unex ? false false true  true  true  true  true  true  true  true  true  true  true  true  true  true)
+  (farg1_unex ? false false false true  true  true  true  true  true  true  true  true  true  true  true  true)
+  (farg1_unex ? false false false false true  true  true  true  true  true  true  true  true  true  true  true)
+  (farg1_unex ? false false false false false true  true  true  true  true  true  true  true  true  true  true)
+  (farg1_unex ? false false false false false false true  true  true  true  true  true  true  true  true  true)
+  (farg1_unex ? false false false false false false false true  true  true  true  true  true  true  true  true)
+  (farg1_unex ? false false false false false false false false true  true  true  true  true  true  true  true)
+  (farg1_unex ? false false false false false false false false false true  true  true  true  true  true  true)
+  (farg1_unex ? false false false false false false false false false false true  true  true  true  true  true)
+  (farg1_unex ? false false false false false false false false false false false true  true  true  true  true)
+  (farg1_unex ? false false false false false false false false false false false false true  true  true  true)
+  (farg1_unex ? false false false false false false false false false false false false false true  true  true)
+  (farg1_unex ? false false false false false false false false false false false false false false true  true)
+  (farg1_unex ? false false false false false false false false false false false false false false false true).
+
+(* operatore > *)
+ndefinition gt_unex ≝ λe1,e2:S_UN EX_UN.⊖(le_unex e1 e2).
+
+(* operatore ≥ *)
+ndefinition ge_unex ≝ λe1,e2:S_UN EX_UN.⊖(lt_unex e1 e2).
+
+(* opeartore and : simmetrico per costruzione *)
+ndefinition and_unex ≝
+ farg2sym_unex ?
+  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
+  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
+  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
+  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
+  un_x4 un_x4 un_x4 un_x4 un_x0 un_x0 un_x0 un_x0 un_x4 un_x4 un_x4 un_x4
+  un_x5 un_x4 un_x5 un_x0 un_x1 un_x0 un_x1 un_x4 un_x5 un_x4 un_x5
+  un_x6 un_x6 un_x0 un_x0 un_x2 un_x2 un_x4 un_x4 un_x6 un_x6
+  un_x7 un_x0 un_x1 un_x2 un_x3 un_x4 un_x5 un_x6 un_x7
+  un_x8 un_x8 un_x8 un_x8 un_x8 un_x8 un_x8 un_x8
+  un_x9 un_x8 un_x9 un_x8 un_x9 un_x8 un_x9
+  un_xA un_xA un_x8 un_x8 un_xA un_xA
+  un_xB un_x8 un_x9 un_xA un_xB
+  un_xC un_xC un_xC un_xC
+  un_xD un_xC un_xD
+  un_xE un_xE
+  un_xF.
+
+(*
+ esiste una regola semplice per ottenere associativo per costruzione?
+ ragionando in matrice simmetrico e' : a(i,j) = a(j,i) → A = trasposta(A)
+ ragionando in matrice associativo e' : a(a(i,j),k) = a(i,a(j,k)) → come espresso?
+
+nlemma pippo : un_x3 = (and_unex un_x3 un_xF).
+ nnormalize;
+ perche' non riduce?
+
+nlemma symmetric_farg2unex1 :
+ ∀T:Type.
+ ∀f00,f01,f02,f03,f04,f05,f06,f07,f08,f09,f0A,f0B,f0C,f0D,f0E,f0F:T.
+ ∀f11,f12,f13,f14,f15,f16,f17,f18,f19,f1A,f1B,f1C,f1D,f1E,f1F:T.
+ ∀f22,f23,f24,f25,f26,f27,f28,f29,f2A,f2B,f2C,f2D,f2E,f2F:T.
+ ∀f33,f34,f35,f36,f37,f38,f39,f3A,f3B,f3C,f3D,f3E,f3F:T.
+ ∀f44,f45,f46,f47,f48,f49,f4A,f4B,f4C,f4D,f4E,f4F:T.
+ ∀f55,f56,f57,f58,f59,f5A,f5B,f5C,f5D,f5E,f5F:T.
+ ∀f66,f67,f68,f69,f6A,f6B,f6C,f6D,f6E,f6F:T.
+ ∀f77,f78,f79,f7A,f7B,f7C,f7D,f7E,f7F:T.
+ ∀f88,f89,f8A,f8B,f8C,f8D,f8E,f8F:T.
+ ∀f99,f9A,f9B,f9C,f9D,f9E,f9F:T.
+ ∀fAA,fAB,fAC,fAD,fAE,fAF:T.
+ ∀fBB,fBC,fBD,fBE,fBF:T.
+ ∀fCC,fCD,fCE,fCF:T.
+ ∀fDD,fDE,fDF:T.
+ ∀fEE,fEF:T.
+ ∀fFF:T.
+ ∀dim1.∀dim2.∀y:S_UN EX_UN.
+  (fsym_unex T f00 f01 f02 f03 f04 f05 f06 f07 f08 f09 f0A f0B f0C f0D f0E f0F
+               f11 f12 f13 f14 f15 f16 f17 f18 f19 f1A f1B f1C f1D f1E f1F
+               f22 f23 f24 f25 f26 f27 f28 f29 f2A f2B f2C f2D f2E f2F
+               f33 f34 f35 f36 f37 f38 f39 f3A f3B f3C f3D f3E f3F
+               f44 f45 f46 f47 f48 f49 f4A f4B f4C f4D f4E f4F
+               f55 f56 f57 f58 f59 f5A f5B f5C f5D f5E f5F
+               f66 f67 f68 f69 f6A f6B f6C f6D f6E f6F
+               f77 f78 f79 f7A f7B f7C f7D f7E f7F
+               f88 f89 f8A f8B f8C f8D f8E f8F
+               f99 f9A f9B f9C f9D f9E f9F
+               fAA fAB fAC fAD fAE fAF
+               fBB fBC fBD fBE fBF
+               fCC fCD fCE fCF
+               fDD fDE fDF
+               fEE fEF
+               fFF
+               (S_EL EX_UN ux0 dim1 dim2) y) =
+  (fsym_unex T f00 f01 f02 f03 f04 f05 f06 f07 f08 f09 f0A f0B f0C f0D f0E f0F
+               f11 f12 f13 f14 f15 f16 f17 f18 f19 f1A f1B f1C f1D f1E f1F
+               f22 f23 f24 f25 f26 f27 f28 f29 f2A f2B f2C f2D f2E f2F
+               f33 f34 f35 f36 f37 f38 f39 f3A f3B f3C f3D f3E f3F
+               f44 f45 f46 f47 f48 f49 f4A f4B f4C f4D f4E f4F
+               f55 f56 f57 f58 f59 f5A f5B f5C f5D f5E f5F
+               f66 f67 f68 f69 f6A f6B f6C f6D f6E f6F
+               f77 f78 f79 f7A f7B f7C f7D f7E f7F
+               f88 f89 f8A f8B f8C f8D f8E f8F
+               f99 f9A f9B f9C f9D f9E f9F
+               fAA fAB fAC fAD fAE fAF
+               fBB fBC fBD fBE fBF
+               fCC fCD fCE fCF
+               fDD fDE fDF
+               fEE fEF
+               fFF
+               y (S_EL EX_UN ux0 dim1 dim2)).
+ #T;
+ #f00; #f01; #f02; #f03; #f04; #f05; #f06; #f07; #f08; #f09; #f0A; #f0B; #f0C; #f0D; #f0E; #f0F;
+ #f11; #f12; #f13; #f14; #f15; #f16; #f17; #f18; #f19; #f1A; #f1B; #f1C; #f1D; #f1E; #f1F;
+ #f22; #f23; #f24; #f25; #f26; #f27; #f28; #f29; #f2A; #f2B; #f2C; #f2D; #f2E; #f2F;
+ #f33; #f34; #f35; #f36; #f37; #f38; #f39; #f3A; #f3B; #f3C; #f3D; #f3E; #f3F;
+ #f44; #f45; #f46; #f47; #f48; #f49; #f4A; #f4B; #f4C; #f4D; #f4E; #f4F;
+ #f55; #f56; #f57; #f58; #f59; #f5A; #f5B; #f5C; #f5D; #f5E; #f5F;
+ #f66; #f67; #f68; #f69; #f6A; #f6B; #f6C; #f6D; #f6E; #f6F;
+ #f77; #f78; #f79; #f7A; #f7B; #f7C; #f7D; #f7E; #f7F;
+ #f88; #f89; #f8A; #f8B; #f8C; #f8D; #f8E; #f8F;
+ #f99; #f9A; #f9B; #f9C; #f9D; #f9E; #f9F;
+ #fAA; #fAB; #fAC; #fAD; #fAE; #fAF;
+ #fBB; #fBC; #fBD; #fBE; #fBF;
+ #fCC; #fCD; #fCE; #fCF;
+ #fDD; #fDE; #fDF;
+ #fEE; #fEF;
+ #fFF;
+ #dim11; #dim12; #y; nelim y;
+ ##[ ##2: #F; nelim F
+ ##| ##1: #u; ncases u;
+          ##[ ##13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28: #dim21; #dim22; nnormalize; napply refl_eq
+          ##| ##*: #dim21; nnormalize in dim21:(%); napply (bool_destruct … dim21)
+          ##]
+ ##]
+nqed.
+
+... e cosi via fino a
+
+nlemma symmetric_farg2unex :
+ ∀T:Type.
+ ∀f00,f01,f02,f03,f04,f05,f06,f07,f08,f09,f0A,f0B,f0C,f0D,f0E,f0F:T.
+ ∀f11,f12,f13,f14,f15,f16,f17,f18,f19,f1A,f1B,f1C,f1D,f1E,f1F:T.
+ ∀f22,f23,f24,f25,f26,f27,f28,f29,f2A,f2B,f2C,f2D,f2E,f2F:T.
+ ∀f33,f34,f35,f36,f37,f38,f39,f3A,f3B,f3C,f3D,f3E,f3F:T.
+ ∀f44,f45,f46,f47,f48,f49,f4A,f4B,f4C,f4D,f4E,f4F:T.
+ ∀f55,f56,f57,f58,f59,f5A,f5B,f5C,f5D,f5E,f5F:T.
+ ∀f66,f67,f68,f69,f6A,f6B,f6C,f6D,f6E,f6F:T.
+ ∀f77,f78,f79,f7A,f7B,f7C,f7D,f7E,f7F:T.
+ ∀f88,f89,f8A,f8B,f8C,f8D,f8E,f8F:T.
+ ∀f99,f9A,f9B,f9C,f9D,f9E,f9F:T.
+ ∀fAA,fAB,fAC,fAD,fAE,fAF:T.
+ ∀fBB,fBC,fBD,fBE,fBF:T.
+ ∀fCC,fCD,fCE,fCF:T.
+ ∀fDD,fDE,fDF:T.
+ ∀fEE,fEF:T.
+ ∀fFF:T.
+ ∀x,y:S_UN EX_UN.
+  (fsym_unex T f00 f01 f02 f03 f04 f05 f06 f07 f08 f09 f0A f0B f0C f0D f0E f0F
+               f11 f12 f13 f14 f15 f16 f17 f18 f19 f1A f1B f1C f1D f1E f1F
+               f22 f23 f24 f25 f26 f27 f28 f29 f2A f2B f2C f2D f2E f2F
+               f33 f34 f35 f36 f37 f38 f39 f3A f3B f3C f3D f3E f3F
+               f44 f45 f46 f47 f48 f49 f4A f4B f4C f4D f4E f4F
+               f55 f56 f57 f58 f59 f5A f5B f5C f5D f5E f5F
+               f66 f67 f68 f69 f6A f6B f6C f6D f6E f6F
+               f77 f78 f79 f7A f7B f7C f7D f7E f7F
+               f88 f89 f8A f8B f8C f8D f8E f8F
+               f99 f9A f9B f9C f9D f9E f9F
+               fAA fAB fAC fAD fAE fAF
+               fBB fBC fBD fBE fBF
+               fCC fCD fCE fCF
+               fDD fDE fDF
+               fEE fEF
+               fFF
+               x y) =
+  (fsym_unex T f00 f01 f02 f03 f04 f05 f06 f07 f08 f09 f0A f0B f0C f0D f0E f0F
+               f11 f12 f13 f14 f15 f16 f17 f18 f19 f1A f1B f1C f1D f1E f1F
+               f22 f23 f24 f25 f26 f27 f28 f29 f2A f2B f2C f2D f2E f2F
+               f33 f34 f35 f36 f37 f38 f39 f3A f3B f3C f3D f3E f3F
+               f44 f45 f46 f47 f48 f49 f4A f4B f4C f4D f4E f4F
+               f55 f56 f57 f58 f59 f5A f5B f5C f5D f5E f5F
+               f66 f67 f68 f69 f6A f6B f6C f6D f6E f6F
+               f77 f78 f79 f7A f7B f7C f7D f7E f7F
+               f88 f89 f8A f8B f8C f8D f8E f8F
+               f99 f9A f9B f9C f9D f9E f9F
+               fAA fAB fAC fAD fAE fAF
+               fBB fBC fBD fBE fBF
+               fCC fCD fCE fCF
+               fDD fDE fDF
+               fEE fEF
+               fFF
+               y x).
+ #T;
+ #f00; #f01; #f02; #f03; #f04; #f05; #f06; #f07; #f08; #f09; #f0A; #f0B; #f0C; #f0D; #f0E; #f0F;
+ #f11; #f12; #f13; #f14; #f15; #f16; #f17; #f18; #f19; #f1A; #f1B; #f1C; #f1D; #f1E; #f1F;
+ #f22; #f23; #f24; #f25; #f26; #f27; #f28; #f29; #f2A; #f2B; #f2C; #f2D; #f2E; #f2F;
+ #f33; #f34; #f35; #f36; #f37; #f38; #f39; #f3A; #f3B; #f3C; #f3D; #f3E; #f3F;
+ #f44; #f45; #f46; #f47; #f48; #f49; #f4A; #f4B; #f4C; #f4D; #f4E; #f4F;
+ #f55; #f56; #f57; #f58; #f59; #f5A; #f5B; #f5C; #f5D; #f5E; #f5F;
+ #f66; #f67; #f68; #f69; #f6A; #f6B; #f6C; #f6D; #f6E; #f6F;
+ #f77; #f78; #f79; #f7A; #f7B; #f7C; #f7D; #f7E; #f7F;
+ #f88; #f89; #f8A; #f8B; #f8C; #f8D; #f8E; #f8F;
+ #f99; #f9A; #f9B; #f9C; #f9D; #f9E; #f9F;
+ #fAA; #fAB; #fAC; #fAD; #fAE; #fAF;
+ #fBB; #fBC; #fBD; #fBE; #fBF;
+ #fCC; #fCD; #fCE; #fCF;
+ #fDD; #fDE; #fDF;
+ #fEE; #fEF;
+ #fFF;
+ #x; nelim x;
+ ##[ ##2: #F; nelim F
+ ##| ##1: #u; ncases u;
+          ##[ ##13: #dim1; #dim2; napply (sym_unex1 T … dim1 dim2)
+          ##| ##14: #dim1; #dim2; napply (sym_unex1 T … dim1 dim2)
+          ##| ##15: #dim1; #dim2; napply (sym_unex1 T … dim1 dim2)
+          ##| ##16: #dim1; #dim2; napply (sym_unex1 T … dim1 dim2)
+          ##| ##17: #dim1; #dim2; napply (sym_unex1 T … dim1 dim2)
+          ##| ##18: #dim1; #dim2; napply (sym_unex1 T … dim1 dim2)
+          ##| ##19: #dim1; #dim2; napply (sym_unex1 T … dim1 dim2)
+          ##| ##20: #dim1; #dim2; napply (sym_unex1 T … dim1 dim2)
+          ##| ##21: #dim1; #dim2; napply (sym_unex1 T … dim1 dim2)
+          ##| ##22: #dim1; #dim2; napply (sym_unex1 T … dim1 dim2)
+          ##| ##23: #dim1; #dim2; napply (sym_unex1 T … dim1 dim2)
+          ##| ##24: #dim1; #dim2; napply (sym_unex1 T … dim1 dim2)
+          ##| ##25: #dim1; #dim2; napply (sym_unex1 T … dim1 dim2)
+          ##| ##26: #dim1; #dim2; napply (sym_unex1 T … dim1 dim2)
+          ##| ##27: #dim1; #dim2; napply (sym_unex1 T … dim1 dim2)
+          ##| ##28: #dim1; #dim2; napply (sym_unex1 T … dim1 dim2)
+          ##| ##*: #dim1; nnormalize in dim1:(%) napply (bool_destruct … dim1)
+          ##]
+ ##]
+nqed.
+*)