added null character to the alphabet

diff --git a/matita/matita/lib/turing/multi_universal/alphabet.ma b/matita/matita/lib/turing/multi_universal/alphabet.ma
index deb1dceec1f4247d133d5a4bb4e9caf104f3dc0c..8a68596699ef2489557d728ba045bb49ecd5b970 100644 (file)
--- a/matita/matita/lib/turing/multi_universal/alphabet.ma
+++ b/matita/matita/lib/turing/multi_universal/alphabet.ma
@@ -15,33 +15,36 @@
 include "basics/finset.ma".
 
 inductive unialpha : Type[0] ≝ 
-| bit : bool → unialpha
-| bar : unialpha.
+| bit  : bool → unialpha
+| null : unialpha
+| bar  : unialpha.
 
 definition unialpha_eq ≝ 
   λa1,a2.match a1 with
   [ bit x ⇒ match a2 with [ bit y ⇒ ¬ xorb x y | _ ⇒ false ]
-  | bar ⇒ match a2 with [ bar ⇒ true | _ ⇒ false ] ].
+  | bar ⇒ match a2 with [ bar ⇒ true | _ ⇒ false ] 
+  | null ⇒ match a2 with [ null ⇒ true | _ ⇒ false ] ].
   
 definition DeqUnialpha ≝ mk_DeqSet unialpha unialpha_eq ?.
 * [ #x * [ #y cases x cases y normalize % // #Hfalse destruct
          | *: normalize % #Hfalse destruct ]
-  | * [ #y ] normalize % #H1 destruct % ]
+  | *: * [1,4: #y ] normalize % #H1 destruct % ]
 qed.
 
 lemma unialpha_unique : 
-  uniqueb DeqUnialpha [bit true;bit false;bar] = true.
+  uniqueb DeqUnialpha [bit true;bit false;null;bar] = true.
 // qed.
 
 lemma unialpha_complete :∀x:DeqUnialpha. 
-  memb ? x [bit true;bit false;bar] = true.
+  memb ? x [bit true;bit false;null;bar] = true.
 * // * //
 qed.
 
 definition FSUnialpha ≝ 
-  mk_FinSet DeqUnialpha [bit true;bit false;bar] 
+  mk_FinSet DeqUnialpha [bit true;bit false;null;bar] 
   unialpha_unique unialpha_complete.
 
 (*************************** testing characters *******************************)
 definition is_bit ≝ λc.match c with [ bit _ ⇒ true | _ ⇒ false ].
-definition is_bar ≝ λc.match c with [ bar ⇒ true | _ ⇒ false ].
\ No newline at end of file
+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