X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fturing%2Fmulti_universal%2FnormalTM.ma;h=6459cedd9590e282e642f62e40b880bd599c40ae;hb=10bb008413e04d44051590a8069e4f16f6f56102;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..6459cedd9 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 
@@ -187,6 +205,18 @@ definition low_mv ≝ λm.
   | N ⇒ null
   ].
 
+lemma injective_low_char: injective … low_char.
+#c1 #c2 cases c1 cases c2 normalize //
+  [#b1 #H destruct
+  |#b1 #H destruct
+  |#b1 #b2 #H destruct //
+  ]
+qed.   
+
+lemma injective_low_mv: injective … low_mv.
+#m1 #m2 cases m1 cases m2 // normalize #H destruct
+qed.
+   
 (******************************** tuple encoding ******************************)
 definition tuple_type ≝ λn.
  (Nat_to n × (option FinBool)) × (Nat_to n × (option FinBool) × move).