proposition: Lemma ReadCurrentSymbols_Terminates : projT1 ReadCurrentSymbols ↓ ReadCurrentSymbols_T.
proof: Proof. unfold ReadCurrentSymbols. destruct (finMin_opt n) as [min| ] eqn:E. { eapply TerminatesIn_monotone. { now auto with nocore TMdb. } { intros tin k (T&HEncT&Hk). pose proof finMin_opt_Some E as (n'&E'). pose proof finMin_opt_Some_val E as E_val. pose (T' := Vector.cast T E'). exists 1, (ReadCurrentSymbols_Loop_steps_cons (vector_to_list (Vector.tl T')) (Vector.hd T')). repeat split; try lia. { rewrite <- Hk. clear. subst n T'. rewrite !vector_cast_refl. rewrite (Vector.eta T). reflexivity. } { intros tmid [] HMove. cbn in HMove. hnf. left. exists (nil), (vector_to_list (Vector.tl T')), (Vector.hd T'). cbn. rewrite E_val. cbn. repeat split; auto. - rewrite Vector.length_to_list. apply Nat.eqb_eq. lia. - apply knowsFirstSymbols_nil. - rewrite HMove. hnf in HEncT. cbn in *. rewrite HEncT. clear. subst n T'. cbn. rewrite !vector_cast_refl. rewrite (Vector.eta T). cbn. hnf. f_equal. now rewrite !map_app, !List.map_map, <- !app_assoc. } } } { eapply TerminatesIn_monotone. { now auto with nocore TMdb. } { intros tin k (T&HEnc&Hk). rewrite <- Hk. apply finMin_opt_None in E. revert E. clear. intros E. revert T. subst. apply Vector.case0. apply Nat.le_add_r. } } 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)