proposition: Lemma Sim_Realise {Σ} (L : finType) (M : pTM Σ L 1) R : M ⊨ R -> Relabel (StateWhile (@Step Σ (projT1 M)) (start (projT1 M))) (projT2 M) ⊨ fun t '(l, t') => forall t_sig, t = [| encode_tape' t_sig |] -> exists t_sig', R [| t_sig |] (l, [| t_sig' |]) /\ t' = [| encode_tape' t_sig' |].
proof: Proof. intros HM. eapply Realise_monotone. { eapply Relabel_Realise, WhileStep_Realise. } intros ? ? ?. TMSimp. specialize (H0 _ eq_refl). TMSimp. repeat eexists. unfold Realise in HM. eapply TM_eval_iff in H as [k H]. now eapply HM in H. Qed.
imports: Undecidability.TM.Compound.TMTac Undecidability.TM.Basic.Mono Undecidability.TM.Compound.Multi Undecidability.TM.Combinators.Combinators Undecidability.TM.Compound.WriteString