proposition: Lemma Shift_Step_Sem (s : sig) : Shift_Step s ⊨c(3) Shift_Step_Rel s.
proof: Proof. eapply RealiseIn_monotone. { unfold Shift_Step. eapply Switch_RealiseIn with (R2 := fun (c : option sig) => match c with Some c => if f c then _ else _ | None => _ end). - apply ReadChar_Sem. - intros [ c | ]; [ destruct (f c) | ]; apply Return_RealiseIn. + apply Write_Sem. + apply WriteMove_Sem. + apply Write_Sem. } { reflexivity. } { intros tin (yout, tout) H. TMSimp. destruct (current _); [|now TMSimp]. destruct (f _); now TMSimp. } 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)