fact: Fixpoint WriteString_sem_fix (str : list sig) : pRel sig unit 1 := match str with | nil => Nop_Rel | [x] => Write_Rel x | x :: str' => WriteMove_Rel x D |_tt ∘ WriteString_sem_fix str' end.
imports: Undecidability(TM.Util.TM_facts TM.Basic.Mono TM.Combinators.Combinators TM.Compound.Multi) List Undecidability(TMTac) Coq(List)