--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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.
+*)
projects / helm.git / commitdiff