proposition: Lemma MoveB_Realise (n : nat) m : MoveB m n ⊨ fun t '(l, t') => forall t_sig, t = [| encode_tape t_sig |] -> t' = [| @encode_tape n (mv m t_sig) |].
proof: Proof. epose (R := _). eapply Realise_monotone. { unfold MoveB. eapply Switch_Realise. { eapply TestLeftof_Realise. } instantiate (1 := R m). subst R. instantiate (1 := fun m b => if b then _ else _). cbn. intros []. { cbn. instantiate (1 := match m0 with Rmove => _ | _ => _ end). cbn. destruct m. all: now auto with nocore TMdb. } now auto with nocore TMdb. } subst R. assert (forall n c rs, Nat.iter n (fun t : tape bool => tape_move_left t) (leftof c rs) = leftof c rs) as Eleft. { clear. intros. clear. induction n; cbn. { reflexivity. } rewrite Nat_iter_S', IHn. reflexivity. } intros t ([], t') ? t_sig ->. TMSimp. f_equal. destruct t_sig. - TMSimp. assert (Nat.iter n (fun t : tape bool => tape_move t m) niltape = niltape) as ->. { induction n; cbn. { reflexivity. } rewrite Nat_iter_S', IHn. now destruct m. } now destruct m. - cbn in *. TMSimp. destruct m. + TMSimp. now rewrite Eleft. + TMSimp. reflexivity. + TMSimp. now rewrite Nat_iter_id. - TMSimp. destruct m. + cbn. rewrite <- !Nat_iter_S' with (f := fun t0 => tape_move_left t0). rewrite Nat_iter_S. cbn. pose proof (@midtape_left_midtape (finType_CS bool)). cbn in H. erewrite <- H. 2: reflexivity. rewrite Nat_iter_S'. rewrite length_encode_sym. reflexivity. + enough (forall c rs, Nat.iter n (fun t : tape bool => tape_move_right t) (rightof c rs) = rightof c rs) as -> by reflexivity. intros. clear. induction n; cbn. { reflexivity. } rewrite Nat_iter_S', IHn. reflexivity. + now rewrite Nat_iter_id. - TMSimp. rename l into rs, l0 into ls. rewrite <- !Nat_iter_S' with (f := fun t0 => tape_move t0 m). destruct m. + cbn. destruct rs. * cbn. rewrite Nat_iter_S. cbn. now rewrite Eleft. * cbn. pose proof (@midtape_left_midtape (finType_CS bool)). cbn in H. rewrite encode_string_app, rev_app_distr. cbn. rewrite rev_app_distr. cbn. rewrite Nat_iter_S. cbn. rewrite <- app_assoc. erewrite <- H. 2:reflexivity. rewrite length_encode_sym. reflexivity. + cbn. destruct ls. * cbn. pose proof (@midtape_right_rightof (finType_CS bool)). cbn in H. rewrite H. 2:now rewrite length_encode_sym. reflexivity. * cbn. rewrite Nat_iter_S'. pose proof (@midtape_right_midtape (finType_CS bool)). cbn in H. rewrite H. { cbn. rewrite encode_string_app. cbn. rewrite !rev_app_distr. cbn. rewrite rev_app_distr. cbn. rewrite <- app_assoc. reflexivity. } now rewrite length_encode_sym. + cbn. rewrite Nat_iter_id. reflexivity. Qed.
imports: Undecidability.TM.Compound.TMTac Undecidability.TM.Basic.Mono Undecidability.TM.Compound.Multi Undecidability.TM.Combinators.Combinators Undecidability.TM.Compound.WriteString