From e47584d3cc500acd8ffb533810daabd3b2ff8300 Mon Sep 17 00:00:00 2001
From: Wilmer Ricciotti <ricciott@cs.unibo.it>
Date: Wed, 16 Jan 2013 16:01:54 +0000
Subject: [PATCH] added null character to the alphabet

---
 .../lib/turing/multi_universal/alphabet.ma    | 19 +++++++++++--------
 1 file changed, 11 insertions(+), 8 deletions(-)

diff --git a/matita/matita/lib/turing/multi_universal/alphabet.ma b/matita/matita/lib/turing/multi_universal/alphabet.ma
index deb1dceec..8a6859669 100644
--- 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
-- 
2.39.2