proposition: Lemma Shift_fun_mirror (s : sig) (t t' : tape sig) : mirror_tape t' = Shift_fun s (mirror_tape t) -> Shift_L_fun s t = t'.
proof: Proof. destruct t as [ | r rs | l ls | ls m rs ]. - rewrite Shift_fun_equation. simpl_tape. cbn. intros -> % mirror_tape_inv_midtape. rewrite Shift_L_fun_equation; cbn. reflexivity. - rewrite Shift_fun_equation. simpl_tape. cbn. intros -> % mirror_tape_inv_midtape. rewrite Shift_L_fun_equation; cbn. reflexivity. - rewrite Shift_fun_equation. simpl_tape. cbn. intros -> % mirror_tape_inv_midtape. rewrite Shift_L_fun_equation; cbn. reflexivity. - revert s rs m t'. induction ls as [ | l ls' IH]; intros; cbn in *. + do 2 (rewrite Shift_fun_equation in H; cbn in H). destruct (f m) eqn:Em. * apply mirror_tape_inv_midtape in H as ->. do 1 (rewrite Shift_L_fun_equation; cbn). now rewrite Em. * apply mirror_tape_inv_midtape in H as ->. do 2 (rewrite Shift_L_fun_equation; cbn). now rewrite Em. + do 1 (rewrite Shift_fun_equation in H; cbn in H). do 1 (rewrite Shift_L_fun_equation; cbn). destruct (f m) eqn:Em. * now apply mirror_tape_inv_midtape in H as ->. * specialize IH with (1 := H). auto. 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)