freescale porting, work in progress

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

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/aux_bases.ma b/helm/software/matita/contribs/ng_assembly/freescale/aux_bases.ma
index 58898142df2d18944b47cc8d6b660c47f34a7da2..1d49e79c577e4545bb721b46a81d51aae863462e 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/freescale/aux_bases.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/aux_bases.ma
@@ -37,27 +37,6 @@ ninductive oct : Type ≝
 | o6: oct
 | o7: oct.
 
-(*ndefinition oct_ind :
- ΠP:oct → Prop.P o0 → P o1 → P o2 → P o3 → P o4 → P o5 → P o6 → P o7 → Πn:oct.P n ≝
-λP:oct → Prop.
-λp:P o0.λp1:P o1.λp2:P o2.λp3:P o3.λp4:P o4.λp5:P o5.λp6:P o6.λp7:P o7.λn:oct.
- match n with
-  [ o0 ⇒ p | o1 ⇒ p1 | o2 ⇒ p2 | o3 ⇒ p3 | o4 ⇒ p4 | o5 ⇒ p5 | o6 ⇒ p6 | o7 ⇒ p7 ]. 
-
-ndefinition oct_rec :
- ΠP:oct → Set.P o0 → P o1 → P o2 → P o3 → P o4 → P o5 → P o6 → P o7 → Πn:oct.P n ≝
-λP:oct → Set.
-λp:P o0.λp1:P o1.λp2:P o2.λp3:P o3.λp4:P o4.λp5:P o5.λp6:P o6.λp7:P o7.λn:oct.
- match n with
-  [ o0 ⇒ p | o1 ⇒ p1 | o2 ⇒ p2 | o3 ⇒ p3 | o4 ⇒ p4 | o5 ⇒ p5 | o6 ⇒ p6 | o7 ⇒ p7 ]. 
-
-ndefinition oct_rect :
- ΠP:oct → Type.P o0 → P o1 → P o2 → P o3 → P o4 → P o5 → P o6 → P o7 → Πn:oct.P n ≝
-λP:oct → Type.
-λp:P o0.λp1:P o1.λp2:P o2.λp3:P o3.λp4:P o4.λp5:P o5.λp6:P o6.λp7:P o7.λn:oct.
- match n with
-  [ o0 ⇒ p | o1 ⇒ p1 | o2 ⇒ p2 | o3 ⇒ p3 | o4 ⇒ p4 | o5 ⇒ p5 | o6 ⇒ p6 | o7 ⇒ p7 ].
-*)
 (* operatore = *)
 ndefinition eq_oct ≝
 λn1,n2:oct.
@@ -136,54 +115,6 @@ ninductive bitrigesim : Type ≝
 | t1E: bitrigesim
 | t1F: bitrigesim.
 
-(*ndefinition bitrigesim_ind :
- ΠP:bitrigesim → Prop.P t00 → P t01 → P t02 → P t03 → P t04 → P t05 → P t06 → P t07 →
-                      P t08 → P t09 → P t0A → P t0B → P t0C → P t0D → P t0E → P t0F →
-                      P t10 → P t11 → P t12 → P t13 → P t14 → P t15 → P t16 → P t17 →
-                      P t18 → P t19 → P t1A → P t1B → P t1C → P t1D → P t1E → P t1F → Πt:bitrigesim.P t ≝                      
-λP:bitrigesim → Prop.
-λp:P t00.λp1:P t01.λp2:P t02.λp3:P t03.λp4:P t04.λp5:P t05.λp6:P t06.λp7:P t07.
-λp8:P t08.λp9:P t09.λp10:P t0A.λp11:P t0B.λp12:P t0C.λp13:P t0D.λp14:P t0E.λp15:P t0F.
-λp16:P t10.λp17:P t11.λp18:P t12.λp19:P t13.λp20:P t14.λp21:P t15.λp22:P t16.λp23:P t17.
-λp24:P t18.λp25:P t19.λp26:P t1A.λp27:P t1B.λp28:P t1C.λp29:P t1D.λp30:P t1E.λp31:P t1F.λt:bitrigesim.
- match t with
-  [ t00 ⇒ p   | t01 ⇒ p1  | t02 ⇒ p2  | t03 ⇒ p3  | t04 ⇒ p4  | t05 ⇒ p5  | t06 ⇒ p6  | t07 ⇒ p7
-  | t08 ⇒ p8  | t09 ⇒ p9  | t0A ⇒ p10 | t0B ⇒ p11 | t0C ⇒ p12 | t0D ⇒ p13 | t0E ⇒ p14 | t0F ⇒ p15
-  | t10 ⇒ p16 | t11 ⇒ p17 | t12 ⇒ p18 | t13 ⇒ p19 | t14 ⇒ p20 | t15 ⇒ p21 | t16 ⇒ p22 | t17 ⇒ p23
-  | t18 ⇒ p24 | t19 ⇒ p25 | t1A ⇒ p26 | t1B ⇒ p27 | t1C ⇒ p28 | t1D ⇒ p29 | t1E ⇒ p30 | t1F ⇒ p31 ].    
-
-ndefinition bitrigesim_rec :
- ΠP:bitrigesim → Set.P t00 → P t01 → P t02 → P t03 → P t04 → P t05 → P t06 → P t07 →
-                     P t08 → P t09 → P t0A → P t0B → P t0C → P t0D → P t0E → P t0F →
-                     P t10 → P t11 → P t12 → P t13 → P t14 → P t15 → P t16 → P t17 →
-                     P t18 → P t19 → P t1A → P t1B → P t1C → P t1D → P t1E → P t1F → Πt:bitrigesim.P t ≝                      
-λP:bitrigesim → Set.
-λp:P t00.λp1:P t01.λp2:P t02.λp3:P t03.λp4:P t04.λp5:P t05.λp6:P t06.λp7:P t07.
-λp8:P t08.λp9:P t09.λp10:P t0A.λp11:P t0B.λp12:P t0C.λp13:P t0D.λp14:P t0E.λp15:P t0F.
-λp16:P t10.λp17:P t11.λp18:P t12.λp19:P t13.λp20:P t14.λp21:P t15.λp22:P t16.λp23:P t17.
-λp24:P t18.λp25:P t19.λp26:P t1A.λp27:P t1B.λp28:P t1C.λp29:P t1D.λp30:P t1E.λp31:P t1F.λt:bitrigesim.
- match t with
-  [ t00 ⇒ p   | t01 ⇒ p1  | t02 ⇒ p2  | t03 ⇒ p3  | t04 ⇒ p4  | t05 ⇒ p5  | t06 ⇒ p6  | t07 ⇒ p7
-  | t08 ⇒ p8  | t09 ⇒ p9  | t0A ⇒ p10 | t0B ⇒ p11 | t0C ⇒ p12 | t0D ⇒ p13 | t0E ⇒ p14 | t0F ⇒ p15
-  | t10 ⇒ p16 | t11 ⇒ p17 | t12 ⇒ p18 | t13 ⇒ p19 | t14 ⇒ p20 | t15 ⇒ p21 | t16 ⇒ p22 | t17 ⇒ p23
-  | t18 ⇒ p24 | t19 ⇒ p25 | t1A ⇒ p26 | t1B ⇒ p27 | t1C ⇒ p28 | t1D ⇒ p29 | t1E ⇒ p30 | t1F ⇒ p31 ].  
-
-ndefinition bitrigesim_rect :
- ΠP:bitrigesim → Type.P t00 → P t01 → P t02 → P t03 → P t04 → P t05 → P t06 → P t07 →
-                      P t08 → P t09 → P t0A → P t0B → P t0C → P t0D → P t0E → P t0F →
-                      P t10 → P t11 → P t12 → P t13 → P t14 → P t15 → P t16 → P t17 →
-                      P t18 → P t19 → P t1A → P t1B → P t1C → P t1D → P t1E → P t1F → Πt:bitrigesim.P t ≝                      
-λP:bitrigesim → Type.
-λp:P t00.λp1:P t01.λp2:P t02.λp3:P t03.λp4:P t04.λp5:P t05.λp6:P t06.λp7:P t07.
-λp8:P t08.λp9:P t09.λp10:P t0A.λp11:P t0B.λp12:P t0C.λp13:P t0D.λp14:P t0E.λp15:P t0F.
-λp16:P t10.λp17:P t11.λp18:P t12.λp19:P t13.λp20:P t14.λp21:P t15.λp22:P t16.λp23:P t17.
-λp24:P t18.λp25:P t19.λp26:P t1A.λp27:P t1B.λp28:P t1C.λp29:P t1D.λp30:P t1E.λp31:P t1F.λt:bitrigesim.
- match t with
-  [ t00 ⇒ p   | t01 ⇒ p1  | t02 ⇒ p2  | t03 ⇒ p3  | t04 ⇒ p4  | t05 ⇒ p5  | t06 ⇒ p6  | t07 ⇒ p7
-  | t08 ⇒ p8  | t09 ⇒ p9  | t0A ⇒ p10 | t0B ⇒ p11 | t0C ⇒ p12 | t0D ⇒ p13 | t0E ⇒ p14 | t0F ⇒ p15
-  | t10 ⇒ p16 | t11 ⇒ p17 | t12 ⇒ p18 | t13 ⇒ p19 | t14 ⇒ p20 | t15 ⇒ p21 | t16 ⇒ p22 | t17 ⇒ p23
-  | t18 ⇒ p24 | t19 ⇒ p25 | t1A ⇒ p26 | t1B ⇒ p27 | t1C ⇒ p28 | t1D ⇒ p29 | t1E ⇒ p30 | t1F ⇒ p31 ].  
-*)
 (* operatore = *)
 ndefinition eq_bitrig ≝
 λt1,t2:bitrigesim.