proposition: Lemma midtape_right_midtape {Σ : finType} l m r1 c r2 n : n = S (length r1) -> Nat.iter n (@tape_move_right Σ) (midtape l m (r1 ++ c :: r2)) = midtape (rev r1 ++ m :: l) c r2.
proof: Proof. intros ->. induction r1 in m, c, r2 |- * using rev_ind; cbn. - reflexivity. - rewrite app_length. cbn. rewrite Nat.add_comm. cbn. rewrite <- app_assoc, Nat_iter_S'. cbn. rewrite (IHr1 m x (c :: r2)). cbn. now rewrite rev_app_distr. Qed.
imports: Undecidability.TM.Compound.TMTac Undecidability.TM.Basic.Mono Undecidability.TM.Compound.Multi Undecidability.TM.Combinators.Combinators Undecidability.TM.Compound.WriteString