proposition: Lemma Shift_Realise (s : sig) : Shift s ⊨ Shift_Rel s.
proof: Proof. eapply Realise_monotone. { apply StateWhile_Realise. intros. eapply RealiseIn_Realise. apply Shift_Step_Sem. } { apply StateWhileInduction; intros; cbn in *. - destruct (current tin[@Fin0]) eqn:E. + destruct (f e) eqn:Ee; TMSimp. * now rewrite Shift_fun_equation, E, Ee. * now rewrite Shift_fun_equation, E, Ee. + now rewrite Shift_fun_equation, E. - destruct (current tin[@Fin0]) eqn:E. + destruct (f e) eqn:Ee; TMSimp; inv H0. symmetry. now rewrite Shift_fun_equation, E, Ee. + now rewrite Shift_fun_equation, E. } 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)