nelim fixed

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

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/prod.ma b/helm/software/matita/contribs/ng_assembly/freescale/prod.ma
index 24bea4f216099aac89e4461753eb3cc681bbfd1b..e382b0dd19da0460355b2c0102c0d55e96d60d05 100644 (file)
--- a/helm/software/matita/contribs/ng_assembly/freescale/prod.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/prod.ma
@@ -13,15 +13,11 @@
 (**************************************************************************)
 
 (* ********************************************************************** *)
-(*                           Progetto FreeScale                           *)
+(*                          Progetto FreeScale                            *)
 (*                                                                        *)
-(* Sviluppato da:                                                         *)
-(*   Cosimo Oliboni, oliboni@cs.unibo.it                                  *)
+(*   Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it                   *)
+(*     Cosimo Oliboni, oliboni@cs.unibo.it                                *)
 (*                                                                        *)
-(* Questo materiale fa parte della tesi:                                  *)
-(*   "Formalizzazione Interattiva dei Microcontroller a 8bit FreeScale"   *)
-(*                                                                        *)
-(*                    data ultima modifica 15/11/2007                     *)
 (* ********************************************************************** *)
 
 include "freescale/bool.ma".
@@ -33,33 +29,6 @@ include "freescale/bool.ma".
 ninductive ProdT (T1:Type) (T2:Type) : Type ≝
  pair : T1 → T2 → ProdT T1 T2.
 
-ndefinition ProdT_ind
- : ΠT1,T2:Type.ΠP:ProdT T1 T2 → Prop.
-   (Πt:T1.Πt1:T2.P (pair T1 T2 t t1)) →
-   Πp:ProdT T1 T2.P p ≝
-λT1,T2:Type.λP:ProdT T1 T2 → Prop.
-λf:Πt:T1.Πt1:T2.P (pair T1 T2 t t1).
-λp:ProdT T1 T2.
- match p with [ pair t t1 ⇒ f t t1 ].
-
-ndefinition ProdT_rec
- : ΠT1,T2:Type.ΠP:ProdT T1 T2 → Set.
-   (Πt:T1.Πt1:T2.P (pair T1 T2 t t1)) →
-   Πp:ProdT T1 T2.P p ≝
-λT1,T2:Type.λP:ProdT T1 T2 → Set.
-λf:Πt:T1.Πt1:T2.P (pair T1 T2 t t1).
-λp:ProdT T1 T2.
- match p with [ pair t t1 ⇒ f t t1 ].
-
-ndefinition ProdT_rect
- : ΠT1,T2:Type.ΠP:ProdT T1 T2 → Type.
-   (Πt:T1.Πt1:T2.P (pair T1 T2 t t1)) →
-   Πp:ProdT T1 T2.P p ≝
-λT1,T2:Type.λP:ProdT T1 T2 → Type.
-λf:Πt:T1.Πt1:T2.P (pair T1 T2 t t1).
-λp:ProdT T1 T2.
- match p with [ pair t t1 ⇒ f t t1 ].
-
 ndefinition fst ≝
 λT1,T2:Type.λp:ProdT T1 T2.match p with [ pair  x _ ⇒ x ].
 
@@ -76,33 +45,6 @@ ndefinition eq_pair ≝
 ninductive Prod3T (T1:Type) (T2:Type) (T3:Type) : Type ≝
 triple : T1 → T2 → T3 → Prod3T T1 T2 T3.
 
-ndefinition Prod3T_ind
- : ΠT1,T2,T3:Type.ΠP:Prod3T T1 T2 T3 → Prop.
-   (Πt:T1.Πt1:T2.Πt2:T3.P (triple T1 T2 T3 t t1 t2)) →
-   Πp:Prod3T T1 T2 T3.P p ≝
-λT1,T2,T3:Type.λP:Prod3T T1 T2 T3 → Prop.
-λf:Πt:T1.Πt1:T2.Πt2:T3.P (triple T1 T2 T3 t t1 t2).
-λp:Prod3T T1 T2 T3.
- match p with [ triple t t1 t2 ⇒ f t t1 t2 ].
-
-ndefinition Prod3T_rec
- : ΠT1,T2,T3:Type.ΠP:Prod3T T1 T2 T3 → Set.
-   (Πt:T1.Πt1:T2.Πt2:T3.P (triple T1 T2 T3 t t1 t2)) →
-   Πp:Prod3T T1 T2 T3.P p ≝
-λT1,T2,T3:Type.λP:Prod3T T1 T2 T3 → Set.
-λf:Πt:T1.Πt1:T2.Πt2:T3.P (triple T1 T2 T3 t t1 t2).
-λp:Prod3T T1 T2 T3.
- match p with [ triple t t1 t2 ⇒ f t t1 t2 ].
-
-ndefinition Prod3T_rect
- : ΠT1,T2,T3:Type.ΠP:Prod3T T1 T2 T3 → Type.
-   (Πt:T1.Πt1:T2.Πt2:T3.P (triple T1 T2 T3 t t1 t2)) →
-   Πp:Prod3T T1 T2 T3.P p ≝
-λT1,T2,T3:Type.λP:Prod3T T1 T2 T3 → Type.
-λf:Πt:T1.Πt1:T2.Πt2:T3.P (triple T1 T2 T3 t t1 t2).
-λp:Prod3T T1 T2 T3.
- match p with [ triple t t1 t2 ⇒ f t t1 t2 ].
-
 ndefinition fst3T ≝
 λT1.λT2.λT3.λp:Prod3T T1 T2 T3.match p with [ triple x _ _ ⇒ x ].
 
@@ -122,33 +64,6 @@ ndefinition eq_triple ≝
 ninductive Prod4T (T1:Type) (T2:Type) (T3:Type) (T4:Type) : Type ≝
 quadruple : T1 → T2 → T3 → T4 → Prod4T T1 T2 T3 T4.
 
-ndefinition Prod4T_ind
- : ΠT1,T2,T3,T4:Type.ΠP:Prod4T T1 T2 T3 T4 → Prop.
-   (Πt:T1.Πt1:T2.Πt2:T3.Πt3:T4.P (quadruple T1 T2 T3 T4 t t1 t2 t3)) →
-   Πp:Prod4T T1 T2 T3 T4.P p ≝
-λT1,T2,T3,T4:Type.λP:Prod4T T1 T2 T3 T4 → Prop.
-λf:Πt:T1.Πt1:T2.Πt2:T3.Πt3:T4.P (quadruple T1 T2 T3 T4 t t1 t2 t3).
-λp:Prod4T T1 T2 T3 T4.
- match p with [ quadruple t t1 t2 t3 ⇒ f t t1 t2 t3 ].
-
-ndefinition Prod4T_rec
- : ΠT1,T2,T3,T4:Type.ΠP:Prod4T T1 T2 T3 T4 → Set.
-   (Πt:T1.Πt1:T2.Πt2:T3.Πt3:T4.P (quadruple T1 T2 T3 T4 t t1 t2 t3)) →
-   Πp:Prod4T T1 T2 T3 T4.P p ≝
-λT1,T2,T3,T4:Type.λP:Prod4T T1 T2 T3 T4 → Set.
-λf:Πt:T1.Πt1:T2.Πt2:T3.Πt3:T4.P (quadruple T1 T2 T3 T4 t t1 t2 t3).
-λp:Prod4T T1 T2 T3 T4.
- match p with [ quadruple t t1 t2 t3 ⇒ f t t1 t2 t3 ].
-
-ndefinition Prod4T_rect
- : ΠT1,T2,T3,T4:Type.ΠP:Prod4T T1 T2 T3 T4 → Type.
-   (Πt:T1.Πt1:T2.Πt2:T3.Πt3:T4.P (quadruple T1 T2 T3 T4 t t1 t2 t3)) →
-   Πp:Prod4T T1 T2 T3 T4.P p ≝
-λT1,T2,T3,T4:Type.λP:Prod4T T1 T2 T3 T4 → Type.
-λf:Πt:T1.Πt1:T2.Πt2:T3.Πt3:T4.P (quadruple T1 T2 T3 T4 t t1 t2 t3).
-λp:Prod4T T1 T2 T3 T4.
- match p with [ quadruple t t1 t2 t3 ⇒ f t t1 t2 t3 ].
-
 ndefinition fst4T ≝
 λT1.λT2.λT3.λT4.λp:Prod4T T1 T2 T3 T4.match p with [ quadruple x _ _ _ ⇒ x ].
 
@@ -171,33 +86,6 @@ ndefinition eq_quadruple ≝
 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.
 
-ndefinition Prod5T_ind
- : ΠT1,T2,T3,T4,T5:Type.ΠP:Prod5T T1 T2 T3 T4 T5 → Prop.
-   (Πt:T1.Πt1:T2.Πt2:T3.Πt3:T4.Πt4:T5.P (quintuple T1 T2 T3 T4 T5 t t1 t2 t3 t4)) →
-   Πp:Prod5T T1 T2 T3 T4 T5.P p ≝
-λT1,T2,T3,T4,T5:Type.λP:Prod5T T1 T2 T3 T4 T5 → Prop.
-λf:Πt:T1.Πt1:T2.Πt2:T3.Πt3:T4.Πt4:T5.P (quintuple T1 T2 T3 T4 T5 t t1 t2 t3 t4).
-λp:Prod5T T1 T2 T3 T4 T5.
- match p with [ quintuple t t1 t2 t3 t4 ⇒ f t t1 t2 t3 t4 ].
-
-ndefinition Prod5T_rec
- : ΠT1,T2,T3,T4,T5:Type.ΠP:Prod5T T1 T2 T3 T4 T5 → Set.
-   (Πt:T1.Πt1:T2.Πt2:T3.Πt3:T4.Πt4:T5.P (quintuple T1 T2 T3 T4 T5 t t1 t2 t3 t4)) →
-   Πp:Prod5T T1 T2 T3 T4 T5.P p ≝
-λT1,T2,T3,T4,T5:Type.λP:Prod5T T1 T2 T3 T4 T5 → Set.
-λf:Πt:T1.Πt1:T2.Πt2:T3.Πt3:T4.Πt4:T5.P (quintuple T1 T2 T3 T4 T5 t t1 t2 t3 t4).
-λp:Prod5T T1 T2 T3 T4 T5.
- match p with [ quintuple t t1 t2 t3 t4 ⇒ f t t1 t2 t3 t4 ].
-
-ndefinition Prod5T_rect
- : ΠT1,T2,T3,T4,T5:Type.ΠP:Prod5T T1 T2 T3 T4 T5 → Type.
-   (Πt:T1.Πt1:T2.Πt2:T3.Πt3:T4.Πt4:T5.P (quintuple T1 T2 T3 T4 T5 t t1 t2 t3 t4)) →
-   Πp:Prod5T T1 T2 T3 T4 T5.P p ≝
-λT1,T2,T3,T4,T5:Type.λP:Prod5T T1 T2 T3 T4 T5 → Type.
-λf:Πt:T1.Πt1:T2.Πt2:T3.Πt3:T4.Πt4:T5.P (quintuple T1 T2 T3 T4 T5 t t1 t2 t3 t4).
-λp:Prod5T T1 T2 T3 T4 T5.
- match p with [ quintuple t t1 t2 t3 t4 ⇒ f t t1 t2 t3 t4 ].
-
 ndefinition fst5T ≝
 λT1.λT2.λT3.λT4.λT5.λp:Prod5T T1 T2 T3 T4 T5.match p with [ quintuple x _ _ _ _ ⇒ x ].