proposition: Lemma simulation_step q t q' t' : step M (q, t) = Some (q', t') -> { t'' | TM_step (encode_config (q, t)) = TM_facts.mk_mconfig (Some q') (| t'' |) /\ encode_tape t' = canonize_tape t'' }.
proof: Proof. rewrite /step /TM_facts.step /=. move: t => [[ls a] rs] /=. case: (trans' M _) => [[[? ?] d]|] /=; last done. move=> [] -> <-. case: d => /=. - case: ls => [|??] /=; eexists; split; reflexivity. - case: rs => [|??] /=; eexists; split; reflexivity. Qed.
imports: Undecidability(TM.SBTM TM.Util.SBTM_facts) Undecidability.Shared.Libs.PSL.FiniteTypes.FinTypes PeanoNat Lia List ssreflect ssrbool ssrfun