X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Ffreescale%2Fprod.ma;h=e382b0dd19da0460355b2c0102c0d55e96d60d05;hb=633b66b935bbc2c38a5abc2be958359335123258;hp=48d054d3a501fba7b682dde0d815938724fea97f;hpb=a687cf5e3e9ae6fb6ead058c4a191002f21fa951;p=helm.git diff --git a/helm/software/matita/contribs/ng_assembly/freescale/prod.ma b/helm/software/matita/contribs/ng_assembly/freescale/prod.ma index 48d054d3a..e382b0dd1 100644 --- a/helm/software/matita/contribs/ng_assembly/freescale/prod.ma +++ b/helm/software/matita/contribs/ng_assembly/freescale/prod.ma @@ -29,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 ]. @@ -72,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 ]. @@ -118,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 ]. @@ -167,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 ].