mod change (-x)

[helm.git] / helm / software / matita / contribs / ng_assembly / num / bitrigesim.ma

diff --git a/helm/software/matita/contribs/ng_assembly/num/bitrigesim.ma b/helm/software/matita/contribs/ng_assembly/num/bitrigesim.ma
old mode 100755 (executable)
new mode 100644 (file)
index 63eae86..fdfb9fb
--- 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 *)