proposition: Lemma ReadCurrent_Sem : ReadCurrent ⊨c(ReadCurrent_steps) ReadCurrent_Rel.
proof: Proof. unfold ReadCurrent_steps. eapply RealiseIn_monotone. { unfold ReadCurrent. now auto with nocore TMdb. } { reflexivity. } { intros tin (yout, tout) H. intros tps1 tps2 tp HCons. unfold atCons_current in *. TMSimp. destruct tp as [ | r rs | l ls | ls m rs ]; cbn in *; hnf in HCons; TMSimp. all: (split; hnf; auto). } 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)