X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Fnum%2Fbitrigesim.ma;h=fdfb9fbd23690006d215452da623b8de8e9d6ac2;hb=3cf6181bded05eb63140d1b2ba4f2f5791a73b48;hp=63eae8657a123c6fe49e065c9ba52607175ca93b;hpb=38fccc2b774e493a94eedef76342b56079c0e694;p=helm.git

diff --git a/helm/software/matita/contribs/ng_assembly/num/bitrigesim.ma b/helm/software/matita/contribs/ng_assembly/num/bitrigesim.ma
index 63eae8657..fdfb9fbd2 100755
--- a/helm/software/matita/contribs/ng_assembly/num/bitrigesim.ma
+++ b/helm/software/matita/contribs/ng_assembly/num/bitrigesim.ma
@@ -16,7 +16,7 @@
 (*                          Progetto FreeScale                            *)
 (*                                                                        *)
 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
-(*   Ultima modifica: 05/08/2009                                          *)
+(*   Sviluppo: 2008-2010                                                  *)
 (*                                                                        *)
 (* ********************************************************************** *)
 
@@ -64,38 +64,22 @@ ninductive bitrigesim : Type ≝
 ndefinition eq_bit ≝
 λt1,t2:bitrigesim.
  match t1 with
-  [ t00 ⇒ match t2 with [ t00 ⇒ true | _ ⇒ false ]
-  | t01 ⇒ match t2 with [ t01 ⇒ true | _ ⇒ false ]
-  | t02 ⇒ match t2 with [ t02 ⇒ true | _ ⇒ false ]
-  | t03 ⇒ match t2 with [ t03 ⇒ true | _ ⇒ false ]
-  | t04 ⇒ match t2 with [ t04 ⇒ true | _ ⇒ false ]
-  | t05 ⇒ match t2 with [ t05 ⇒ true | _ ⇒ false ]
-  | t06 ⇒ match t2 with [ t06 ⇒ true | _ ⇒ false ]
-  | t07 ⇒ match t2 with [ t07 ⇒ true | _ ⇒ false ]
-  | t08 ⇒ match t2 with [ t08 ⇒ true | _ ⇒ false ]
-  | t09 ⇒ match t2 with [ t09 ⇒ true | _ ⇒ false ]
-  | t0A ⇒ match t2 with [ t0A ⇒ true | _ ⇒ false ]
-  | t0B ⇒ match t2 with [ t0B ⇒ true | _ ⇒ false ]
-  | t0C ⇒ match t2 with [ t0C ⇒ true | _ ⇒ false ]
-  | t0D ⇒ match t2 with [ t0D ⇒ true | _ ⇒ false ]
-  | t0E ⇒ match t2 with [ t0E ⇒ true | _ ⇒ false ]
-  | t0F ⇒ match t2 with [ t0F ⇒ true | _ ⇒ false ]
-  | t10 ⇒ match t2 with [ t10 ⇒ true | _ ⇒ false ]
-  | t11 ⇒ match t2 with [ t11 ⇒ true | _ ⇒ false ]
-  | t12 ⇒ match t2 with [ t12 ⇒ true | _ ⇒ false ]
-  | t13 ⇒ match t2 with [ t13 ⇒ true | _ ⇒ false ]
-  | t14 ⇒ match t2 with [ t14 ⇒ true | _ ⇒ false ]
-  | t15 ⇒ match t2 with [ t15 ⇒ true | _ ⇒ false ]
-  | t16 ⇒ match t2 with [ t16 ⇒ true | _ ⇒ false ]
-  | t17 ⇒ match t2 with [ t17 ⇒ true | _ ⇒ false ]
-  | t18 ⇒ match t2 with [ t18 ⇒ true | _ ⇒ false ]
-  | t19 ⇒ match t2 with [ t19 ⇒ true | _ ⇒ false ]
-  | t1A ⇒ match t2 with [ t1A ⇒ true | _ ⇒ false ]
-  | t1B ⇒ match t2 with [ t1B ⇒ true | _ ⇒ false ]
-  | t1C ⇒ match t2 with [ t1C ⇒ true | _ ⇒ false ]
-  | t1D ⇒ match t2 with [ t1D ⇒ true | _ ⇒ false ]
-  | t1E ⇒ match t2 with [ t1E ⇒ true | _ ⇒ false ]
-  | t1F ⇒ match t2 with [ t1F ⇒ true | _ ⇒ false ]
+  [ t00 ⇒ match t2 with [ t00 ⇒ true | _ ⇒ false ] | t01 ⇒ match t2 with [ t01 ⇒ true | _ ⇒ false ]
+  | t02 ⇒ match t2 with [ t02 ⇒ true | _ ⇒ false ] | t03 ⇒ match t2 with [ t03 ⇒ true | _ ⇒ false ]
+  | t04 ⇒ match t2 with [ t04 ⇒ true | _ ⇒ false ] | t05 ⇒ match t2 with [ t05 ⇒ true | _ ⇒ false ]
+  | t06 ⇒ match t2 with [ t06 ⇒ true | _ ⇒ false ] | t07 ⇒ match t2 with [ t07 ⇒ true | _ ⇒ false ]
+  | t08 ⇒ match t2 with [ t08 ⇒ true | _ ⇒ false ] | t09 ⇒ match t2 with [ t09 ⇒ true | _ ⇒ false ]
+  | t0A ⇒ match t2 with [ t0A ⇒ true | _ ⇒ false ] | t0B ⇒ match t2 with [ t0B ⇒ true | _ ⇒ false ]
+  | t0C ⇒ match t2 with [ t0C ⇒ true | _ ⇒ false ] | t0D ⇒ match t2 with [ t0D ⇒ true | _ ⇒ false ]
+  | t0E ⇒ match t2 with [ t0E ⇒ true | _ ⇒ false ] | t0F ⇒ match t2 with [ t0F ⇒ true | _ ⇒ false ]
+  | t10 ⇒ match t2 with [ t10 ⇒ true | _ ⇒ false ] | t11 ⇒ match t2 with [ t11 ⇒ true | _ ⇒ false ]
+  | t12 ⇒ match t2 with [ t12 ⇒ true | _ ⇒ false ] | t13 ⇒ match t2 with [ t13 ⇒ true | _ ⇒ false ]
+  | t14 ⇒ match t2 with [ t14 ⇒ true | _ ⇒ false ] | t15 ⇒ match t2 with [ t15 ⇒ true | _ ⇒ false ]
+  | t16 ⇒ match t2 with [ t16 ⇒ true | _ ⇒ false ] | t17 ⇒ match t2 with [ t17 ⇒ true | _ ⇒ false ]
+  | t18 ⇒ match t2 with [ t18 ⇒ true | _ ⇒ false ] | t19 ⇒ match t2 with [ t19 ⇒ true | _ ⇒ false ]
+  | t1A ⇒ match t2 with [ t1A ⇒ true | _ ⇒ false ] | t1B ⇒ match t2 with [ t1B ⇒ true | _ ⇒ false ]
+  | t1C ⇒ match t2 with [ t1C ⇒ true | _ ⇒ false ] | t1D ⇒ match t2 with [ t1D ⇒ true | _ ⇒ false ]
+  | t1E ⇒ match t2 with [ t1E ⇒ true | _ ⇒ false ] | t1F ⇒ match t2 with [ t1F ⇒ true | _ ⇒ false ]
   ].
 
 (* iteratore sui bitrigesimali *)