proposition: Lemma ReadCurrentSymbols_Loop_Terminates st : projT1 (ReadCurrentSymbols_Loop st) ↓ ReadCurrentSymbols_Loop_T st.
proof: Proof. eapply TerminatesIn_monotone. { unfold ReadCurrentSymbols_Loop. now auto with nocore TMdb. } { revert st. apply StateWhileCoInduction. intros (readSymbols&i). intros. unfold ReadCurrentSymbols_Loop_T in *. unfold ReadCurrentSymbols_Step_T in *. destruct HT as [ (tps1&tps2&tp&HL1&HL2&HRead&HCons&Hk) | (tps&HNil&Hk)]. { eexists. repeat split. left. eauto. intros ymid tmid (HStep_cons&HStep_nil). clear HStep_nil. cbn in *. destruct ymid as [ (readSymbols'&i') | result ]. - specialize HStep_cons with (1 := HL1) (2 := HL2) (3 := HCons) (4 := HRead). destruct tps2 as [ | tp' tps2']; cbn in *. + TMSimp. congruence. + destruct HStep_cons as (HStep_cons1&HStep_cons2). destruct (finSucc_opt i) as [ i'' | ] eqn:Ei; inv HStep_cons2; rename i'' into i'. eexists. split. 2: apply Hk. left. exists (tps1 ++ [tp]), (tps2'), tp'. repeat split. * simpl_list. cbn. apply finSucc_opt_Some' in Ei. apply Nat.eqb_eq. apply Nat.eqb_eq in HL1. lia. * simpl_list. cbn. apply finSucc_opt_Some' in Ei. apply Nat.eqb_eq. apply Nat.eqb_eq in HL2. lia. * apply insertKnownSymbol_correct. now apply Nat.eqb_eq. assumption. * assumption. * reflexivity. - specialize HStep_cons with (1 := HL1) (2 := HL2) (3 := HCons) (4 := HRead). destruct tps2 as [ | tp' tps2']; cbn in *. + lia. + lia. } { eexists. repeat split. right. eauto. intros ymid tmid (HStep_cons&HStep_nil). clear HStep_cons. cbn in *. destruct ymid as [ (readSymbols'&i') | result ]. - specialize HStep_nil with (1 := HNil) as (?&?). congruence. - 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)