proposition: Lemma WriteString_Sem str : WriteString str ⊨c(WriteString_steps (length str)) (WriteString_Rel str).
proof: Proof. eapply RealiseIn_monotone. { apply WriteString_fix_Sem. } { reflexivity. } { induction str as [ | s [ | s' str'] IH]; intros tin (yout, tout) H. - cbn. now TMSimp. - cbn. now TMSimp. - change (WriteString_sem_fix (s :: s' :: str')) with ((WriteMove_Rel s D |_tt ∘ WriteString_sem_fix (s' :: str'))) in H. destruct H as (tmid&H1&H2). hnf in H1. apply IH in H2. now TMSimp. } Qed.
imports: Undecidability(TM.Util.TM_facts TM.Basic.Mono TM.Combinators.Combinators TM.Compound.Multi) List Undecidability(TMTac) Coq(List)