proposition: Lemma MoveToSymbol_L_Realise : MoveToSymbol_L ⊨ MoveToSymbol_L_Rel.
proof: Proof. eapply Realise_monotone. - eapply Mirror_Realise. eapply MoveToSymbol_Realise. - intros tin (y&tout) H. hnf in *. rewrite (destruct_tape tin) in *. cbn in *. rewrite mirror_tapes_nth in H. cbn in H. symmetry in H. apply MoveToSymbol_mirror in H as ->. reflexivity. 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)