proposition: Lemma Shift_L_Realise (s : sig) : Shift_L s ⊨ Shift_L_Rel s.
proof: Proof. eapply Realise_monotone. { unfold Shift_L. apply Mirror_Realise, Shift_Realise. } { intros tin ([], tout) H. hnf in H; hnf. rewrite (destruct_tape tin) in *. rewrite (destruct_tape tout) in *. now apply Shift_fun_mirror in H. } 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)