proposition: Lemma MoveToSymbol_Realise : MoveToSymbol ⊨ MoveToSymbol_Rel.
proof: Proof. eapply Realise_monotone. { unfold MoveToSymbol. eapply While_Realise. eapply RealiseIn_Realise. eapply MoveToSymbol_Step_Sem. } { eapply WhileInduction; intros; hnf in *. - destruct HLastStep as (H1&H2); TMSimp. destruct (current _) as [s | ] eqn:E. + destruct (f s) eqn:E'; cbn in *; inv H2. rewrite MoveToSymbol_Fun_equation. rewrite E, E'. cbn. now apply MoveToSymbol_Step_true. + rewrite MoveToSymbol_Step_None; auto. now rewrite MoveToSymbol_Fun_equation, E. - destruct HStar as (H1&H2); TMSimp. destruct (current _) as [s | ] eqn:E; cbn in *. + destruct (f s) eqn:E'; cbn in *; inv H2. erewrite MoveToSymbol_Step_false; eauto. eapply MoveToSymbol_skip; eauto. + inv H2. } Qed.
imports: Undecidability(TM.Util.Prelim) Undecidability(TM.Basic.Mono) Undecidability(TM.Combinators.Combinators) Undecidability(TM.Compound.TMTac) Undecidability(TM.Compound.Multi) Coq(FunInd) Coq(Recdef)