X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fturing%2Fmulti_universal%2Falphabet.ma;h=1c4cd806073449a11932a251dba46b405e1fc5d5;hb=632dfd0a57c9951d0efbd769d6f433c4ef68a314;hp=8a68596699ef2489557d728ba045bb49ecd5b970;hpb=e47584d3cc500acd8ffb533810daabd3b2ff8300;p=helm.git

diff --git a/matita/matita/lib/turing/multi_universal/alphabet.ma b/matita/matita/lib/turing/multi_universal/alphabet.ma
index 8a6859669..1c4cd8060 100644
--- a/matita/matita/lib/turing/multi_universal/alphabet.ma
+++ b/matita/matita/lib/turing/multi_universal/alphabet.ma
@@ -1,18 +1,16 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
+(*
+    ||M||  This file is part of HELM, an Hypertextual, Electronic   
+    ||A||  Library of Mathematics, developed at the Computer Science 
+    ||T||  Department of the University of Bologna, Italy.           
+    ||I||                                                            
+    ||T||  
+    ||A||  
+    \   /  This file is distributed under the terms of the       
+     \ /   GNU General Public License Version 2   
+      V_____________________________________________________________*)
 
 include "basics/finset.ma".
+include "basics/lists/list.ma".
 
 inductive unialpha : Type[0] ≝ 
 | bit  : bool → unialpha
@@ -44,7 +42,18 @@ definition FSUnialpha ≝
   mk_FinSet DeqUnialpha [bit true;bit false;null;bar] 
   unialpha_unique unialpha_complete.
 
+unification hint  0 ≔ ; 
+    X ≟ FSUnialpha
+(* ---------------------------------------- *) ⊢ 
+    unialpha ≡ FinSetcarr X.
+    
 (*************************** testing characters *******************************)
 definition is_bit ≝ λc.match c with [ bit _ ⇒ true | _ ⇒ false ].
-definition is_bar ≝ λc.match c with [ bar ⇒ true | _ ⇒ false ].
-definition is_null ≝ λc.match c with [ null ⇒ true | _ ⇒ false ].
\ No newline at end of file
+definition is_bar ≝ λc:DeqUnialpha. c == bar.
+definition is_null ≝ λc:DeqUnialpha. c == null.
+
+definition only_bits ≝ λl.
+  ∀c.mem ? c l → is_bit c = true.
+
+definition no_bars ≝ λl.
+  ∀c.mem ? c l → is_bar c = false.