proposition: Lemma TM_sTM_simulation' : (forall q t t', eval M (start M) t q t' -> exists q, eval M' (start M') (enc_tape [] t) q (enc_tape [] t')) /\ (forall t, (exists q t', eval M' (start M') (enc_tape [] t) q t') -> (exists q t', eval M (start M) t q t')).
proof: Proof. split. - intros q t t'. repeat setoid_rewrite TM_eval_iff. intros [k H]. assert (H0 : M ↓ (fun t' k' => t = t' /\ k' = k)). { intros ? ? []. subst. eauto. } eapply (ToSingleTape_Terminates' (pM := mk_pTM M)) in H0. specialize (H0 (enc_tape [] t)). destruct (H0 (Loop_steps (start (projT1 (mk_pTM M))) t k)) as [[q'' t''] H1]. * now exists t, k. * pose proof (H2 := ToSingleTape_Realise' (pM := mk_pTM M)). specialize (H2 (fun t '(f,t') => exists outc k, loopM (initc M t) k = Some outc /\ ctapes outc = t')). edestruct H2 as (t''' & [[q''' t''''] (k' & HH & <-)] & H3). + intros ? ? ? ?. now exists outc, k0. + eapply H1. + reflexivity. + eexists q'', _. unfold initc in H1. etransitivity. { eapply H1. } repeat apply f_equal. eapply loop_injective in HH. 2: exact H. inv HH. unfold contains_tapes in H3. cbn in H3. rewrite (destruct_tape t'') in *. cbn in *. rewrite H3. reflexivity. - intros t. intros (q & t' & [k H] % TM_eval_iff). pose proof (ToSingleTape_Realise' (pM := mk_pTM M)). specialize (H0 (fun t '(f,t') => exists outc k, loopM (initc M t) k = Some outc /\ ctapes outc = t')). edestruct H0. * intros ? ? ? ?. now exists outc, k0. * eapply H. * reflexivity. * intuition idtac. destruct H2 as (? & ? & ? & ?). subst. destruct x0 as [q'' t'']. exists q'', t''. eapply TM_eval_iff. now exists x1. Qed.
imports: Undecidability.TM(Single.StepTM TM) Undecidability.TM.Code.Code Undecidability.TM(Single.EncodeTapes) Undecidability.Synthetic.Definitions