unistep_aux

diff --git a/matita/matita/lib/turing/multi_universal/unistep_aux.ma b/matita/matita/lib/turing/multi_universal/unistep_aux.ma
index adfa29b8dc7714d331daf65258c3e82961302e12..06427b3bb638889731844709de706c61c39f0e50 100644 (file)
--- a/matita/matita/lib/turing/multi_universal/unistep_aux.ma
+++ b/matita/matita/lib/turing/multi_universal/unistep_aux.ma
@@ -12,6 +12,7 @@
 include "turing/multi_universal/moves_2.ma".
 include "turing/multi_universal/match.ma".
 include "turing/multi_universal/copy.ma".
+include "turing/multi_universal/alphabet.ma".
 
 (*
 
@@ -50,38 +51,6 @@ include "turing/multi_universal/copy.ma".
   cfg_to_obj
 *)
 
-inductive unialpha : Type[0] ≝ 
-| bit : bool → 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 ] ].
-  
-definition DeqUnialpha ≝ mk_DeqSet unialpha unialpha_eq ?.
-* [ #x * [ #y cases x cases y normalize % // #Hfalse destruct
-         | *: normalize % #Hfalse destruct ]
-  | * [ #y ] normalize % #H1 destruct % ]
-qed.
-
-lemma unialpha_unique : 
-  uniqueb DeqUnialpha [bit true;bit false;bar] = true.
-// qed.
-
-lemma unialpha_complete :∀x:DeqUnialpha. 
-  memb ? x [bit true;bit false;bar] = true.
-* // * //
-qed.
-
-definition FSUnialpha ≝ 
-  mk_FinSet DeqUnialpha [bit true;bit false;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 ].
-
 definition obj ≝ 0.
 definition cfg ≝ 1.
 definition prg ≝ 2.