proposition: Lemma MoveToSymbol_correct t str1 str2 x : (forall x, List.In x str1 -> stop x = false) -> (stop x = true) -> tape_local t = str1 ++ x :: str2 -> MoveToSymbol_Fun stop f t = midtape (rev (map f str1) ++ left t) (f x) str2.
proof: Proof. intros H H0. destruct t as [ | r rs | l ls | ls m rs]; cbn in *. 1,3: rewrite MoveToSymbol_Fun_equation; cbn; destruct str1; cbn in *; try congruence. 1: destruct str1; cbn in *; congruence. revert m ls str1 H. revert rs. refine (@size_induction _ (@length sig) _ _); intros [ | s rs'] IH; intros. - rewrite MoveToSymbol_Fun_equation; cbn. destruct str1; cbn in *; inv H1. + rewrite H0. cbn. auto. + destruct str1; cbn in *; congruence. - rewrite MoveToSymbol_Fun_equation; cbn. destruct (stop m) eqn:E1. + cbn. destruct str1; cbn in *; inv H1; eauto. specialize (H _ ltac:(eauto)). congruence. + destruct str1; cbn in *; inv H1. * congruence. * simpl_list. eapply IH; cbn; eauto. 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)