proposition: Theorem WhileStep_Realise : StateWhile Step (start M) ⊨ fun t '(q', t') => forall t_sig, t = [| encode_tape' t_sig |] -> exists t_sig', eval M (start M) [| t_sig |] q' [| t_sig' |] /\ t' = [| encode_tape' t_sig'|].
proof: Proof. generalize (start M). intros q. eapply Realise_monotone. { now auto with nocore TMdb. } intros t (l, t') ? t_sig E. TMSimp. unfold tapes in *. rename t'_0 into t'. remember ([|encode_tape' t_sig|]) as tin. remember (l, [|t'|]) as cout. induction H in t_sig, l, t', Heqtin, Heqcout |- *. - TMSimp. specialize (H _ eq_refl). rename l0 into q. destruct (halt q) eqn:Eq. + inv Heqcout. destruct H as [[= ->] [= ->]]. + inv Heqcout. destruct trans as [q' T] eqn:Eqt. rewrite (destruct_vector_single T) in *. destruct (Vector.hd T) as [c' m] eqn:ET. destruct H as [[= ->] [= ->]]. specialize (IHStateWhile_Rel _ _ _ eq_refl eq_refl) as [t_sig' [H1 [= ->]]]. exists t_sig'. split; try reflexivity. econstructor; eassumption. - inv Heqcout. specialize (H _ eq_refl). rename l0 into q. destruct (halt q) eqn:Eq. + destruct H as [[= ->] [= ->]]. eexists; split; try reflexivity. now econstructor. + destruct trans as [q' T] eqn:Eqt. destruct Vector.hd as [c' m]. destruct H as [[= ->] [= ->]]. Qed.
imports: Undecidability.TM.Compound.TMTac Undecidability.TM.Basic.Mono Undecidability.TM.Compound.Multi Undecidability.TM.Combinators.Combinators Undecidability.TM.Compound.WriteString