proposition: Lemma midtape_left_midtape {Σ : finType} (l1 l2 : list Σ) m m' r n : n = S (length l1) -> Nat.iter n (@tape_move_left Σ) (midtape (rev l1 ++ [m'] ++ l2) m r) = midtape l2 m' (l1 ++ m :: r).
proof: Proof. intros ->. induction l1 in m, m', l2 |- *. - cbn. reflexivity. - cbn. rewrite <- app_assoc. rewrite Nat_iter_S'. now rewrite (IHl1 (m' :: l2) m a). Qed.
imports: Undecidability.TM.Compound.TMTac Undecidability.TM.Basic.Mono Undecidability.TM.Compound.Multi Undecidability.TM.Combinators.Combinators Undecidability.TM.Compound.WriteString