proposition: Lemma MoveToSymbol_Step_Sem : MoveToSymbol_Step ⊨c(3) MoveToSymbol_Step_Rel.
proof: Proof. eapply RealiseIn_monotone. { unfold MoveToSymbol_Step. eapply Switch_RealiseIn. { eapply ReadChar_Sem. } cbn. instantiate (2 := fun o : option sig => match o with Some x => if f x then _ else _ | None => _ end). intros [ | ]; cbn. - destruct (f e). + instantiate (1 := 1). apply Return_RealiseIn. eapply Write_Sem. + apply Return_RealiseIn. eapply WriteMove_Sem. - apply Return_RealiseIn. eapply Nop_Sem. } { (cbn; lia). } { unfold MoveToSymbol_Step_Rel, MoveToSymbol_Step_Fun. 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)