X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fturing%2Fmulti_universal%2FnormalTM.ma;h=8e3af494a032715a3f6f90affcfd77770549aa9a;hb=dabd7add16b4e678f48bc15cd0d992b80fbc9216;hp=13ef8a66c6e992fcfe9f0c6d8a675555c664967e;hpb=1f740f74d94187a2376228a86faf79ea949c0dff;p=helm.git

diff --git a/matita/matita/lib/turing/multi_universal/normalTM.ma b/matita/matita/lib/turing/multi_universal/normalTM.ma
index 13ef8a66c..8e3af494a 100644
--- a/matita/matita/lib/turing/multi_universal/normalTM.ma
+++ b/matita/matita/lib/turing/multi_universal/normalTM.ma
@@ -80,16 +80,34 @@ record normalTM : Type[0] ≝
   nhalt : initN no_states → bool
 }.
 
+lemma decomp_target : ∀n.∀tg: trans_target n. 
+  ∃qout,cout,m. tg = 〈qout,cout,m〉.
+#n * * #q #c #m %{q} %{c} %{m} //
+qed.
+
 (* A normal machine is just a special case of Turing Machine. *)
 
+definition nstart_state ≝ λM.mk_Sig ?? 0 (pos_no_states M).
+
 definition normalTM_to_TM ≝ λM:normalTM.
   mk_TM FinBool (initN (no_states M)) 
-   (ntrans M) (mk_Sig ?? 0 (pos_no_states M)) (nhalt M).
+   (ntrans M) (nstart_state M) (nhalt M).
 
 coercion normalTM_to_TM.
 
 definition nconfig ≝ λn. config FinBool (initN n).
 
+(* A normal machine has a non empty graph *)
+
+definition sample_input: ∀M.trans_source (no_states M).
+#M % [@(nstart_state M) | %]
+qed.
+
+lemma nTM_nog: ∀M. graph_enum ?? (ntrans M) ≠ [ ].
+#M % #H lapply(graph_enum_complete ?? (ntrans M) (sample_input M) ? (refl ??))
+>H normalize #Hd destruct
+qed.
+
 (******************************** tuples **************************************)
 
 (* By general results on FinSets we know that every function f between two