proposition: Corollary MoveToSymbol_L_correct t str1 str2 x : (forall x, List.In x str1 -> stop x = false) -> (stop x = true) -> tape_local_l t = str1 ++ x :: str2 -> MoveToSymbol_L_Fun stop f t = midtape str2 (f x) (rev (map f str1) ++ right t).
proof: Proof. intros. pose proof (@MoveToSymbol_correct (mirror_tape t) str1 str2 x) as Lmove. simpl_tape in Lmove. repeat spec_assert Lmove by auto. erewrite (MoveToSymbol_mirror' (t' := mirror_tape (MoveToSymbol_L_Fun stop f t))) in Lmove; simpl_tape in *; eauto. now apply mirror_tape_inv_midtape in Lmove. Qed.
imports: Undecidability(TM.Util.Prelim) Undecidability(TM.Basic.Mono) Undecidability(TM.Combinators.Combinators) Undecidability(TM.Compound.TMTac) Undecidability(TM.Compound.Multi) Coq(FunInd) Coq(Recdef)