proposition: Corollary MoveToSymbol_L_correct_moveleft ls x ls' m rs : (forall x, List.In x ls -> stop x = false) -> stop x = true -> MoveToSymbol_L_Fun stop f (tape_move_left' (ls ++ x :: ls') m rs) = midtape ls' (f x) (rev (map f ls) ++ m :: rs).
proof: Proof. intros HStopL HStopX. destruct ls as [ | s s'] eqn:E; cbn. - rewrite MoveToSymbol_L_Fun_equation. cbn. rewrite HStopX. reflexivity. - rewrite MoveToSymbol_L_correct_midtape; auto with list. rewrite <- !app_assoc. reflexivity. 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)