proposition: Lemma WriteString_Fun_eq (sig' : Type) (t : tape sig') (str : list sig') : WriteString_Fun t str = match str with | nil => t | [x] => tape_write t (Some x) | x :: str' => WriteString_Fun (doAct t (Some x, D)) str' end.
proof: Proof. destruct str; auto. Qed.
imports: Undecidability(TM.Util.TM_facts TM.Basic.Mono TM.Combinators.Combinators TM.Compound.Multi) List Undecidability(TMTac) Coq(List)