proposition: Lemma HaltTM_Σ_to_HaltTM_bool_correct : HaltsTM M ts <-> HaltsTM M' ts'.
proof: Proof. unfold M', ts'. split. - intros (q' & t' & [n H] % TM_eval_iff). destruct (Sim_Terminates (M := (existT _ M (fun _ : state M => tt))) (T := fun tin k => tin = ts /\ k >= n)). + intros tin k [-> Hk]. cbn. exists (mk_mconfig q' t'). eapply @loop_monotone. { exact H. } eapply Hk. + destruct H0 as [k H0]. cbn in H0. edestruct H0 as [[] H1]. -- exists (Vector.hd ts), n. split. { reflexivity. } split. 2: now unfold ge. split. 2:lia. apply (Vector.caseS' ts). intros ?. apply (Vector.case0). reflexivity. -- exists cstate. eexists ctapes. eapply TM_eval_iff. exists (x * n + k). unfold Relabel, initc in H1. cbn in H1. revert H1. apply (Vector.caseS' ts). intros ?. cbn. intros t0. pattern t0. apply Vector.case0. intros H1. exact H1. - intros (q' & t' & [n H] % TM_eval_iff). eapply (Sim_Realise (M := (existT _ M (fun _ : state M => tt))) (R := fun tin '(_,tout) => exists q', eval M (start M) tin q' tout)) in H. + revert H. apply (Vector.caseS' ts). intros ?. cbn. intros t0. pattern t0. apply Vector.case0. clear ts. rename h into t. intros H. specialize (H t eq_refl) as [t'_sig [[q'_ H1] H2]]. cbn in H1. cbn in H2. subst. exists q'_, [|t'_sig|]. eassumption. + intros tin k [q'_ tout] Hter. cbn in *. exists q'_. eapply TM_eval_iff. exists k. exact Hter. Qed.
imports: Undecidability.TM.Compound.TMTac Undecidability.TM.Basic.Mono Undecidability.TM.Compound.Multi Undecidability.TM.Combinators.Combinators Undecidability.TM.Compound.WriteString