proposition: Lemma binary_simulation Σ (M : TM Σ 1) : {M' : TM (finType_CS bool) 1 | (forall q t t', eval M (start M) t q t' -> exists q, eval M' (start M') ([| encode_tape' (Vector.nth t Fin0) |] ) q ([| encode_tape' (Vector.nth t' Fin0) |] )) /\ (forall t, (exists q t', eval M' (start M') ([| encode_tape' (Vector.nth t Fin0) |] ) q t') -> (exists q t', eval M (start M) t q t')) }.
proof: Proof. exists (projT1 (StateWhile (@Step Σ M) (start M))). split. - intros q' t t' [n H] % TM_eval_iff. edestruct @Sim_Terminates with (M := (existT _ M (fun _ : state M => tt))) (T := fun tin k => tin = t /\ 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 t), n. split. { reflexivity. } split. 2: now unfold ge. split. 2:lia. rewrite (destruct_tape t). reflexivity. -- exists cstate. eapply TM_eval_iff. exists (x * n + k). unfold Relabel, initc in H1. cbn in H1. rewrite (destruct_tape t) in *. etransitivity. { exact H1. } cbn. repeat apply f_equal. eapply (Sim_Realise (M := (existT _ M (fun _ : state M => tt))) (R := fun tin '(_,tout) => exists q', eval M (start M) tin q' tout)) in H1. + specialize (H1 (Vector.hd t) eq_refl) as [t'_sig [[q'_ [n' H1] % TM_eval_iff] H2]]. cbn in H2. subst. f_equal. eapply loop_injective in H. 2: eassumption. now inv H. + clear k H0 H1. intros tin k [q'_ tout] Hter. cbn in *. exists q'_. eapply TM_eval_iff. exists k. exact Hter. - intros t (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. * rewrite (destruct_tape t) in *. specialize (H (Vector.hd t) eq_refl) as [t'_sig [[q'_ H1] H2]]. 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