proposition: Lemma TM_sTM_simulation n Σ (M : TM Σ n) : {M' : TM ((sigList (EncodeTapes.sigTape Σ)) ^+) 1 | (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. exists (M' M). now apply TM_sTM_simulation'. Qed.
imports: Undecidability.TM(Single.StepTM TM) Undecidability.TM.Code.Code Undecidability.TM(Single.EncodeTapes) Undecidability.Synthetic.Definitions