proposition: Lemma ReadCurrentSymbols_Step_Realise : forall st, ReadCurrentSymbols_Step st ⊨ ReadCurrentSymbols_Step_Rel st.
proof: Proof. intros (readSymbols,i). eapply Realise_monotone. { unfold ReadCurrentSymbols_Step. now auto with nocore TMdb. } { intros tin (yout, tout). TMSimp. split. { intros tps1 tps2 tp HL1 HL2 HCons HKnown. destruct H; TMSimp. { rename H into HIsCons_cons, H0 into HGotoCurrent, H1 into IsCons_nil, H2 into HReadCurrent, H4 into HGoToNext. specialize HIsCons_cons with (1 := HCons) as (HIsCons_cons&_). specialize HGotoCurrent with (1 := HIsCons_cons) as (HGotoCurrent&->). specialize HReadCurrent with (1 := HGotoCurrent) as (HReadCurrent&->). specialize HGoToNext with (1 := HReadCurrent). destruct ymid1, tps2 as [ | tp' tps2']; try easy. { split. auto. destruct (finSucc_opt i) as [i'| ] eqn:Ei. - reflexivity. - exfalso. apply finSucc_opt_None' in Ei. apply Nat.eqb_eq in HL1. apply Nat.eqb_eq in HL2. cbn in *. lia. } { split; auto. enough (finSucc_opt i = None) as -> by reflexivity. apply finSucc_opt_None. apply Nat.eqb_eq in HL1. apply Nat.eqb_eq in HL2. cbn in *. lia. } } { specialize H with (1 := HCons) as (_&H); congruence. } } { intros tps HNil. destruct H; TMSimp. { specialize H1 with (1 := HNil) as (_&H1); congruence. } { now specialize H2 with (1 := HNil) as (H0&_). } } } 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)