proposition: Lemma Step_Realise q : Step q ⊨ fun t '(q_, t') => forall t_sig, t = [| encode_tape' t_sig |] -> if halt q then q_ = inr q /\ t' = t else let '(q', a) := trans M (q, [| current t_sig |]) in let '(c', m) := Vector.hd a in q_ = inl q' /\ t' = [| encode_tape' (mv m (wr c' t_sig)) |].
proof: Proof. eapply Realise_monotone. { unfold Step. eapply Switch_Realise. { now auto with nocore TMdb. } cbn. intros c_i. instantiate (1 := fun c_i => _). cbn. instantiate (1 := ltac:(destruct (halt q); refine _)). destruct (halt q). { cbn. now auto with nocore TMdb. } instantiate (1 := ltac:(destruct (trans (q, [|map_opt g c_i|])); refine _)). cbn. destruct (trans (q, [|map_opt g c_i|])). instantiate (1 := ltac:(destruct (Vector.hd t))). destruct (Vector.hd t). now auto with nocore TMdb. } intros t (q_, t') ? t_sig ->. TMSimp. rename t'_0 into t'. destruct (halt q) eqn:Eq. - TMSimp. split. { reflexivity. } eapply H. reflexivity. - specialize (H _ eq_refl) as [[= ->] ->]. cbn in *. assert (Efg : forall o, map_opt g (map_opt f o) = o). { intros [s | ]; cbn; now rewrite ?Hg. } rewrite Efg in H0. clear Efg. destruct trans as [q' T] eqn:Eqt. destruct Vector.hd as [c' m]. TMSimp. split. { reflexivity. } now eapply H0, H. Qed.
imports: Undecidability.TM.Compound.TMTac Undecidability.TM.Basic.Mono Undecidability.TM.Compound.Multi Undecidability.TM.Combinators.Combinators Undecidability.TM.Compound.WriteString