+(* 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.
+