proposition: Lemma ReadCurrentSymbols_Realise : ReadCurrentSymbols ⊨ ReadCurrentSymbols_Rel.
proof: Proof. clear pM F. unfold ReadCurrentSymbols. destruct (finMin_opt n) as [min| ] eqn:E; swap 1 2. { eapply Realise_monotone. { now auto with TMdb. } { intros tin (yout, tout) H. intros T HEncT. unfold contains_tapes in *. TMSimp. apply finMin_opt_None in E as ->. revert T. now apply Vector.case0. } } { eapply Realise_monotone. { now auto with nocore TMdb. } { intros tin (yout, tout) H. intros T HEncT. unfold contains_tapes in *. TMSimp. rename H0 into HLoop_cons, H1 into HLoop_nil. clear HLoop_nil. pose proof finMin_opt_Some E as (n'&E'). pose (T' := Vector.cast T E'). pose proof finMin_opt_Some_val E as E_val. specialize (HLoop_cons nil (Vector.hd T') (vector_to_list (Vector.tl T'))). cbn in *. rewrite E_val in HLoop_cons. subst. specialize HLoop_cons with (1 := eq_refl). spec_assert HLoop_cons. { rewrite Vector.length_to_list. apply Nat.eqb_eq. reflexivity. } spec_assert HLoop_cons. { hnf. cbn. clear. subst T'. rewrite (Vector.eta T). cbn. f_equal. simpl_list. now rewrite vector_cast_refl. } spec_assert HLoop_cons as [HLoop_cons1 ->] by (cbn; tauto). rewrite vector_to_list_eta in HLoop_cons1. subst T'. rewrite vector_cast_refl in *. split; auto. destruct (finSucc_opt min) as [minSucc | ] eqn:E2. - pose proof finSucc_opt_Some' E2 as E2_val. rewrite E_val in E2_val. now apply insertKnownSymbols_correct_cons. - apply finSucc_opt_None' in E2. apply Nat.succ_inj in E2. assert (n' = 0) as -> by lia. cbn. compute [insertKnownSymbol]. destruct_fin min. cbn. rewrite (destruct_tape T). reflexivity. } } Qed.
imports: Undecidability.TM.Basic.Mono Undecidability.TM.Combinators.Combinators Undecidability.TM.Code.Code Undecidability.TM.Single.EncodeTapes Undecidability.TM.Compound(TMTac MoveToSymbol Multi Shift)