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