cfg_to_obj completed (modulo daemons)

[helm.git] / matita / matita / lib / turing / multi_universal / normalTM.ma

diff --git a/matita/matita/lib/turing/multi_universal/normalTM.ma b/matita/matita/lib/turing/multi_universal/normalTM.ma
index 13ef8a66c6e992fcfe9f0c6d8a675555c664967e..8e3af494a032715a3f6f90affcfd77770549aa9a 100644 (file)
--- 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