proposition: Lemma WriteString_fix_Sem (str : list sig) : WriteString str ⊨c(WriteString_steps (length str)) (WriteString_sem_fix str).
proof: Proof. induction str as [ | s [ | s' str'] IH ]. - apply Nop_Sem. - apply Write_Sem. - change (WriteString (s :: s' :: str')) with (WriteMove s D;; WriteString (s' :: str')). eapply RealiseIn_monotone. { apply Seq_RealiseIn. - apply WriteMove_Sem. - apply IH. } { unfold WriteString_steps. cbn. lia. } { intros t1 t3 H. destruct H as (()&t2&H1&H2). change (WriteString_sem_fix (s :: s' :: str')) with (WriteMove_Rel s D |_tt ∘ WriteString_sem_fix (s' :: str')). exists t2. split; auto. } Qed.
imports: Undecidability(TM.Util.TM_facts TM.Basic.Mono TM.Combinators.Combinators TM.Compound.Multi) List Undecidability(TMTac) Coq(List)