proposition: Lemma ReadB_Realise n : ReadB n ⊨ fun t '(l, t') => forall t_sig : tape (Fin.t n), t = [| encode_tape t_sig |] -> t' = t /\ l = current t_sig.
proof: Proof. eapply Realise_monotone. { exact (proj2_sig (ReadB_canonical n)). } pose (Rel := (fun n (t : Vector.t _ 1) '(l, t') => match t with | [| midtape ls _ rs |] => forall rs' (c_i : Fin.t n), rs = encode_sym c_i ++ rs' -> t' = t /\ l = Some c_i | _ => t' = t /\ l = None end) : forall n, Vector.t (tape bool) 1 -> option (Fin.t n) * Vector.t (tape bool) 1 -> Prop). transitivity (Rel n). - induction n. + subst Rel. cbn. intros tp (l, t') (-> & [ _ ->]). eapply Vector.caseS' with (v := tp). clear tp. intros t nl. eapply Vector.case0 with (v := nl). clear nl. destruct t; eauto. intros rs' c_i ->. inv c_i. + intros t (l, t') (? & tright & (-> & ->) & H). rewrite (destruct_tape t) in *. cbn in *. destruct (Vector.hd t); cbn in *. * now destruct H as (-> & [] & ->). * now destruct H as (-> & [] & ->). * now destruct H as (-> & [] & ->). * intros rs' c_i ->. destruct H as ([] & tps & ? & ? & tps' & [-> ->] & H0). rewrite (destruct_tape tps) in *. cbn in *. rename l0 into ls. revert H0. rewrite H. clear H. rewrite (destruct_tape t'). eapply Fin.caseS' with (p := c_i); clear c_i. -- cbn. now intros (-> & [] & <-). -- intros c_i. change (Fin.FS c_i) with (Fin.R 1 c_i) in *. unfold encode_sym. cbn in *. pose proof (Fin.R_sanity 1 c_i) as E. cbn in E. rewrite E. clear E. cbn. intros (o & tout & ? & ?). eapply IHn in H. cbn in H. destruct (H _ _ eq_refl) as [-> ->]. cbn in *. now destruct H0 as (-> & [] & <-). - intros t (l, t'). unfold Rel. intros H. intros t_sig ->. destruct t_sig; cbn in *; eauto. Qed.
imports: Undecidability.TM.Compound.TMTac Undecidability.TM.Basic.Mono Undecidability.TM.Compound.Multi Undecidability.TM.Combinators.Combinators