proposition: Lemma WriteString_MoveBack {Σ : finType} (x : Σ) l : (WriteString Rmove (x :: l) ;; MoveM Lmove (|l|)) ⊨ fun t '(_, t') => t' = Vector.map (fun t => midtape (left t) x (l ++ skipn (|l|) (right t))) t.
proof: Proof. eapply Realise_monotone. { now auto with nocore TMdb. } intros t ([], t') ([] & t1 & ? & ?). TMSimp. f_equal. rename t_0 into t. induction l in x, t |- *. - reflexivity. - cbn [length plus]. rewrite Nat_iter_S'. rewrite WriteString_Fun_eq. setoid_rewrite IHl. clear. destruct t; cbn. + now rewrite skipn_nil. + reflexivity. + now rewrite skipn_nil. + unfold tape_move_left'. unfold tape_move_right'. cbn. destruct l1; cbn. * now rewrite skipn_nil. * reflexivity. Qed.
imports: Undecidability.TM.Compound.TMTac Undecidability.TM.Basic.Mono Undecidability.TM.Compound.Multi Undecidability.TM.Combinators.Combinators Undecidability.TM.Compound.WriteString