-record normalTM : Type[0] ≝
-{ no_states : nat;
- pos_no_states : (0 < no_states);
- ntrans : trans_source no_states → trans_target no_states;
- nhalt : initN no_states → bool
-}.
-
-definition normalTM_to_TM ≝ λM:normalTM.
- mk_TM FinBool (initN (no_states M))
- (ntrans M) (mk_Sig ?? 0 (pos_no_states M)) (nhalt M).
-
-coercion normalTM_to_TM.
-
-definition nconfig ≝ λn. config FinBool (initN n).
-
-(*
-definition normalTM ≝ λn,t,h.
- λk:0<n.mk_TM FinBool (initN n) t (mk_Sig ?? 0 k) h. *)
-