Msg reporting via HLogger in the error window made asynchronous => speedup.

[helm.git] / matita / matita / lib / turing / universal / alphabet.ma

diff --git a/matita/matita/lib/turing/universal/alphabet.ma b/matita/matita/lib/turing/universal/alphabet.ma
index 04701aeec180b8b868e7388f186cb173900bb2ef..bf2484f29fadf94ae268dc9a7dad93ec54bfafac 100644 (file)
--- a/matita/matita/lib/turing/universal/alphabet.ma
+++ b/matita/matita/lib/turing/universal/alphabet.ma
@@ -39,10 +39,18 @@ definition DeqUnialpha ≝ mk_DeqSet unialpha unialpha_eq ?.
   |*: * [1,6,11,16: #y ] normalize % #H1 destruct % ]
 qed.
 
-axiom unialpha_unique : uniqueb DeqUnialpha [bit true;bit false;comma;bar;grid] = true.
+lemma unialpha_unique : 
+  uniqueb DeqUnialpha [bit true;bit false;null;comma;bar;grid] = true.
+// qed.
+
+lemma unialpha_complete :∀x:DeqUnialpha. 
+  memb ? x [bit true;bit false;null;comma;bar;grid] = true.
+* // * //
+qed.
 
 definition FSUnialpha ≝ 
-  mk_FinSet DeqUnialpha [bit true;bit false;null;comma;bar;grid] unialpha_unique.
+  mk_FinSet DeqUnialpha [bit true;bit false;null;comma;bar;grid] 
+  unialpha_unique unialpha_complete.
 
 definition is_bit ≝ λc.match c with [ bit _ ⇒ true | _ ⇒ false ].