proposition: Lemma Shift_fun_move t s c : current t = Some c -> f c = false -> Shift_fun c (tape_move_right' (left t) s (right t)) = Shift_fun s t.
proof: Proof. intros HC Hf. destruct t; cbn in *; inv HC. rename l into ls, l0 into rs. revert ls s c Hf. induction rs; intros; cbn in *. - do 3 (rewrite Shift_fun_equation; cbn). rewrite Hf. reflexivity. - rewrite Shift_fun_equation; cbn. symmetry. rewrite Shift_fun_equation; cbn. symmetry. cbn. rewrite !Hf; cbn. destruct (f a) eqn:Ea; cbn in *; auto. rewrite Shift_fun_equation; cbn; auto. now rewrite Ea. 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)