fact: Definition CaseChar_TM : TM sig 1 := {| trans := fun '(_, sym) => (Some (f sym[@Fin0]), [| (None, Nmove) |]); start := None; halt := fun s => match s with | None => false | Some _ => true end; |}.
imports: Undecidability.TM(Util.TM_facts)