proposition: Lemma Shift_fun_correct_midtape_stop s ls m rs r h rs' : f m = false -> f r = false -> f h = true -> (forall x, In x rs -> f x = false) -> Shift_fun s (midtape ls m (rs ++ r :: h :: rs')) = midtape (rev rs ++ m :: s :: ls) r rs'.
proof: Proof. revert s ls m. induction rs as [ | r' rs IH]; intros; cbn in *. - do 3 (rewrite Shift_fun_equation; cbn). rewrite H, H0, H1. reflexivity. - do 1 (rewrite Shift_fun_equation; cbn). rewrite <- !app_assoc. cbn. rewrite H. rewrite IH; 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)