proposition: Corollary MoveToSymbol_correct_moveright ls m rs x rs' : (forall x, List.In x rs -> stop x = false) -> stop x = true -> MoveToSymbol_Fun stop f (tape_move_right' ls m (rs ++ x :: rs')) = midtape (rev (map f rs) ++ m :: ls) (f x) rs'.
proof: Proof. intros HStopR HStopX. destruct rs as [ | s s'] eqn:E; cbn. - rewrite MoveToSymbol_Fun_equation. cbn. rewrite HStopX. reflexivity. - rewrite MoveToSymbol_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)