proposition: Lemma Step_Realise : Step ⊨ Step_Rel.
proof: Proof. unfold Step, Step_Rel. destruct (halt q). { eapply Realise_monotone. { now auto with nocore TMdb. } { intros tin (yout, tout) H. intros T HEncT. TMSimp. eauto. } } { eapply Realise_monotone. { now auto with nocore TMdb. } { intros tin (yout, tout) H. intros T HEncT. unfold step. cbn. destruct (trans (q, current_chars T)) as [q' act] eqn:E'. TMSimp. rename H into HReadCurrenSymbols, H1 into HMoveToStart1, H2 into HDoActions, H3 into HMoveToStart2. specialize HReadCurrenSymbols with (1 := HEncT) as [HReadCurrenSymbols ->]. specialize HMoveToStart1 with (1 := HReadCurrenSymbols). specialize HDoActions with (2 := HMoveToStart1). spec_assert HDoActions. { apply Nat.eqb_eq. apply Vector.length_to_list. } specialize HMoveToStart2 with (1 := HDoActions). split. - eapply atStart_contains; [|eassumption|]. now rewrite map_vect_list_length, Vector.length_to_list. rewrite E'. cbn. now rewrite map_vect_list_eq. - rewrite E'. cbn. reflexivity. } } Qed.
imports: Undecidability.TM.Basic.Mono Undecidability.TM.Combinators.Combinators Undecidability.TM.Code.Code Undecidability.TM.Single.EncodeTapes Undecidability.TM.Compound(TMTac MoveToSymbol Multi Shift)