proposition: Lemma simulation_halt q t : step M (q, t) = None -> TM_step (encode_config (q, t)) = TM_facts.mk_mconfig None (| encode_tape t |).
proof: Proof. rewrite /step /TM_facts.step /=. move: t => [[ls a] rs] /=. by case: (trans' M _) => [[[? ?] d]|] /=. Qed.
imports: Undecidability(TM.SBTM TM.Util.SBTM_facts) Undecidability.Shared.Libs.PSL.FiniteTypes.FinTypes PeanoNat Lia List ssreflect ssrbool ssrfun