proposition: Lemma MoveToSymbol_correct_midtape_end tl c tr : (forall x, List.In x (c::tr) -> stop x = false) -> MoveToSymbol_Fun stop f (midtape tl c tr) = rightof (hd (f c) (map f (rev tr))) (List.tl (map f (rev tr) ++ f c::tl)).
proof: Proof. revert c tl. revert tr. cbn. refine (@size_induction _ (@length sig) _ _); intros [ | c' tr'] IH; intros. all:rewrite MoveToSymbol_Fun_equation. all:cbn. all:erewrite (H c);[ |now eauto]. - rewrite MoveToSymbol_Fun_equation;cbn. eauto. - rewrite IH. 2,3:now eauto. destruct (rev tr'); cbn. { easy. } now rewrite map_app, <- app_assoc. 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)