Release 0.5.9.

[helm.git] / helm / software / matita / contribs / ng_assembly / common / prod.ma

diff --git a/helm/software/matita/contribs/ng_assembly/common/prod.ma b/helm/software/matita/contribs/ng_assembly/common/prod.ma
index 1080533d174f6ea77cecf45b84be841f6d193c6b..5be106fcb33faaa57a21b6ee69b74e53f90c0224 100644 (file)
--- a/helm/software/matita/contribs/ng_assembly/common/prod.ma
+++ b/helm/software/matita/contribs/ng_assembly/common/prod.ma
@@ -16,7 +16,7 @@
 (*                          Progetto FreeScale                            *)
 (*                                                                        *)
 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
-(*   Sviluppo: 2008-2010                                                  *)
+(*   Ultima modifica: 05/08/2009                                          *)
 (*                                                                        *)
 (* ********************************************************************** *)
 
@@ -36,11 +36,11 @@ ndefinition snd ≝
 λT1,T2:Type.λp:ProdT T1 T2.match p with [ pair  _ x ⇒ x ].
 
 ndefinition eq_pair ≝
-λT1,T2:Type.
+λT1,T2:Type.λp1,p2:ProdT T1 T2.
 λf1:T1 → T1 → bool.λf2:T2 → T2 → bool.
-λp1,p2:ProdT T1 T2.
- (f1 (fst … p1) (fst … p2)) ⊗
- (f2 (snd … p1) (snd … p2)).
+ match p1 with [ pair x1 y1 ⇒
+  match p2 with [ pair x2 y2 ⇒
+   (f1 x1 x2) ⊗ (f2 y1 y2) ]].
 
 ninductive Prod3T (T1:Type) (T2:Type) (T3:Type) : Type ≝
 triple : T1 → T2 → T3 → Prod3T T1 T2 T3.
@@ -55,12 +55,11 @@ ndefinition thd3T ≝
 λT1.λT2.λT3.λp:Prod3T T1 T2 T3.match p with [ triple _ _ x ⇒ x ].
 
 ndefinition eq_triple ≝
-λT1,T2,T3:Type.
+λT1,T2,T3:Type.λp1,p2:Prod3T T1 T2 T3.
 λf1:T1 → T1 → bool.λf2:T2 → T2 → bool.λf3:T3 → T3 → bool.
-λp1,p2:Prod3T T1 T2 T3.
- (f1 (fst3T … p1) (fst3T … p2)) ⊗
- (f2 (snd3T … p1) (snd3T … p2)) ⊗
- (f3 (thd3T … p1) (thd3T … p2)).
+ match p1 with [ triple x1 y1 z1 ⇒
+  match p2 with [ triple x2 y2 z2 ⇒
+   (f1 x1 x2) ⊗ (f2 y1 y2) ⊗ (f3 z1 z2) ]].
 
 ninductive Prod4T (T1:Type) (T2:Type) (T3:Type) (T4:Type) : Type ≝
 quadruple : T1 → T2 → T3 → T4 → Prod4T T1 T2 T3 T4.
@@ -78,13 +77,11 @@ ndefinition fth4T ≝
 λT1.λT2.λT3.λT4.λp:Prod4T T1 T2 T3 T4.match p with [ quadruple _ _ _ x ⇒ x ].
 
 ndefinition eq_quadruple ≝
-λT1,T2,T3,T4:Type.
+λT1,T2,T3,T4:Type.λp1,p2:Prod4T T1 T2 T3 T4.
 λf1:T1 → T1 → bool.λf2:T2 → T2 → bool.λf3:T3 → T3 → bool.λf4:T4 → T4 → bool.
-λp1,p2:Prod4T T1 T2 T3 T4.
- (f1 (fst4T … p1) (fst4T … p2)) ⊗
- (f2 (snd4T … p1) (snd4T … p2)) ⊗
- (f3 (thd4T … p1) (thd4T … p2)) ⊗
- (f4 (fth4T … p1) (fth4T … p2)).
+ match p1 with [ quadruple x1 y1 z1 w1 ⇒
+  match p2 with [ quadruple x2 y2 z2 w2 ⇒
+   (f1 x1 x2) ⊗ (f2 y1 y2) ⊗ (f3 z1 z2) ⊗ (f4 w1 w2) ]].
 
 ninductive Prod5T (T1:Type) (T2:Type) (T3:Type) (T4:Type) (T5:Type) : Type ≝
 quintuple : T1 → T2 → T3 → T4 → T5 → Prod5T T1 T2 T3 T4 T5.
@@ -98,18 +95,15 @@ ndefinition snd5T ≝
 ndefinition thd5T ≝
 λT1.λT2.λT3.λT4.λT5.λp:Prod5T T1 T2 T3 T4 T5.match p with [ quintuple _ _ x _ _ ⇒ x ].
 
-ndefinition fth5T ≝
+ndefinition frth5T ≝
 λT1.λT2.λT3.λT4.λT5.λp:Prod5T T1 T2 T3 T4 T5.match p with [ quintuple _ _ _ x _ ⇒ x ].
 
-ndefinition fft5T ≝
+ndefinition ffth5T ≝
 λT1.λT2.λT3.λT4.λT5.λp:Prod5T T1 T2 T3 T4 T5.match p with [ quintuple _ _ _ _ x ⇒ x ].
 
 ndefinition eq_quintuple ≝
-λT1,T2,T3,T4,T5:Type.
+λT1,T2,T3,T4,T5:Type.λp1,p2:Prod5T T1 T2 T3 T4 T5.
 λf1:T1 → T1 → bool.λf2:T2 → T2 → bool.λf3:T3 → T3 → bool.λf4:T4 → T4 → bool.λf5:T5 → T5 → bool.
-λp1,p2:Prod5T T1 T2 T3 T4 T5.
- (f1 (fst5T … p1) (fst5T … p2)) ⊗
- (f2 (snd5T … p1) (snd5T … p2)) ⊗
- (f3 (thd5T … p1) (thd5T … p2)) ⊗
- (f4 (fth5T … p1) (fth5T … p2)) ⊗
- (f5 (fft5T … p1) (fft5T … p2)).
+ match p1 with [ quintuple x1 y1 z1 w1 v1 ⇒
+  match p2 with [ quintuple x2 y2 z2 w2 v2 ⇒
+   (f1 x1 x2) ⊗ (f2 y1 y2) ⊗ (f3 z1 z2) ⊗ (f4 w1 w2) ⊗ (f5 v1 v2) ]].