proposition: Lemma WriteB_Realise (n : nat) (c : option (Fin.t n)) : WriteB c ⊨ fun t '(_, t') => forall t_sig, t = [| encode_tape t_sig |] -> t' = [| encode_tape (wr c t_sig) |].
proof: Proof. destruct c as [c | ]. - eapply Realise_monotone. { unfold WriteB. eapply Switch_Realise. { eapply TestLeftof_Realise. } intros []. { instantiate (1 := fun b => if b then _ else _). cbn. eapply RealiseIn_Realise, WriteString_Sem. } pose proof (@WriteString_MoveBack (finType_CS bool) false (encode_sym c ++ [true])). cbn in H. replace (|encode_sym c ++ [true]|) with (S n) in H. 2:rewrite app_length, length_encode_sym; cbn; lia. cbn. eapply H. } intros t ([], t') ? ? ->. TMSimp. f_equal. destruct t_sig eqn:E; cbn - [skipn]. + cbn in *. TMSimp. now rewrite app_nil_r. + cbn in *. TMSimp. generalize (encode_sym t ++ true :: encode_string l). clear. intros. replace (encode_sym c ++ true :: false :: l) with ((encode_sym c ++ [true]) ++ false :: l). { generalize (encode_sym c ++ [true]). generalize false. intros. generalize b at 1 4. intros. induction l0 in b0, b, l |- * using rev_ind; cbn. * reflexivity. * rewrite rev_app_distr. cbn. rewrite WriteString_Fun_eq. destruct l0 as [ | x0 l0 _] using rev_ind. -- cbn. reflexivity. -- rewrite rev_app_distr. cbn. rewrite <- !app_assoc. specialize (IHl0 (b0 :: l) b x). rewrite rev_app_distr in IHl0. cbn in *. rewrite <- app_assoc in IHl0. cbn in IHl0. eassumption. } now rewrite <- app_assoc. + cbn in *. TMSimp. rewrite <- app_assoc. cbn. repeat f_equal. rewrite encode_string_app. cbn. rewrite !rev_app_distr. cbn. rewrite rev_app_distr. cbn. now rewrite <- app_assoc. + cbn in *. TMSimp. rewrite <- app_assoc. cbn -[skipn]. repeat f_equal. replace (encode_sym t ++ true :: encode_string l0) with ((encode_sym t ++ [true]) ++ encode_string l0). { pose proof (length_encode_sym t). destruct (encode_sym) eqn:E. * cbn in *. subst. reflexivity. * cbn in *. inv H. rewrite skipn_app. generalize (encode_string l0). intros ?. replace (S (length l1 )) with (length (l1 ++ [true])). { now rewrite Nat.sub_diag, skipn_all. } rewrite app_length. simpl. lia. } now rewrite <- app_assoc. - cbn. eapply Realise_monotone. { now auto with nocore TMdb. } intros t ([], t') ->. eauto. Qed.
imports: Undecidability.TM.Compound.TMTac Undecidability.TM.Basic.Mono Undecidability.TM.Compound.Multi Undecidability.TM.Combinators.Combinators Undecidability.TM.Compound.WriteString