proposition: Lemma ReadCurrentSymbols_Loop_Realise st : ReadCurrentSymbols_Loop st ⊨ ReadCurrentSymbols_Loop_Rel st.
proof: Proof. eapply Realise_monotone. { unfold ReadCurrentSymbols_Loop. now auto with nocore TMdb. } { revert st. apply StateWhileInduction; intros; rename l into st. { destruct st as [ readSymbols i]; cbn in *. destruct HLastStep as [HLastStepCons HLastStepNil]. cbn. split; [intros tps1 tp tps2 HL1 HL2 HCons HRead | intros tps HL HNil HRead]; TMSimp. { specialize HLastStepCons with (1 := HL1) (2 := HL2) (3 := HCons) (4 := HRead). destruct tps2 as [ | tp' tps2']; cbn in *. - destruct HLastStepCons as [HLastStepCons HLastStepCons']; inv HLastStepCons'. split; auto. destruct (finSucc_opt i) as [i'| ]; auto. - destruct HLastStepCons as [ HLastStepCons HLastStepCons']. destruct (finSucc_opt i) as [i' | ]; [congruence|easy]. } { specialize HLastStepNil with (1 := HNil). destruct HLastStepNil as [H1 H2]. inv H2. split; auto. } } { destruct st as [ readSymbols i]; cbn in *. destruct HStar as [HStar_cons HStar_nil]. destruct HLastStep as [HLastStep_cons HLastStep_nil]. cbn in *. cbn. split; [intros tps1 tp tps2 HL1 HL2 HCons HRead | intros tps HL HNil HRead]. { specialize HStar_cons with (1 := HL1) (2 := HL2) (3 := HCons) (4 := HRead). destruct tps2 as [ | tp' tps2']; cbn in *. - destruct HStar_cons as [HStar1 HStar2]. inv HStar2. - destruct HStar_cons as [HStar1 HStar2]. destruct (finSucc_opt i) as [i' | ] eqn:E; [|easy]. inv HStar2. specialize HLastStep_cons with (3 := HStar1). apply Nat.eqb_eq in HL1. apply Nat.eqb_eq in HL2. spec_assert HLastStep_cons. { simpl_list; cbn. apply Nat.eqb_eq. apply finSucc_opt_Some' in E. lia. } spec_assert HLastStep_cons. { simpl_list; cbn. apply Nat.eqb_eq. apply finSucc_opt_Some' in E. lia. } spec_assert HLastStep_cons as [HLastStep_cons ->]. { cbn. apply insertKnownSymbol_correct; auto. } cbn in *. rewrite <- app_assoc in HLastStep_cons. split; now auto. } { specialize HStar_nil with (1 := HNil) as [HStar1 HStar2]; inv HStar2. } } } 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)