proposition: Lemma simulation q t k : steps M k (q, t) = None -> exists q' ts', TM.eval M' (Some q) (| encode_tape t |) q' ts'.
proof: Proof. elim: k q t; first done. move=> k IH q t. rewrite (steps_plus 1 k). case E: (steps M 1 _) => [[q' t']|]. - move: E => /simulation_step [t'' [HM' Ht't'']] /IH. move=> [q'''] [t'''] /TM_facts.TM_eval_iff [k']. rewrite Ht't''. move=> /TM_loopM_canonize_tape => /(_ t''). move=> /(_ ltac:(by case: (t''))). move=> [{}t''' ?]. exists q''', t'''. apply /TM_facts.TM_eval_iff. exists (S k'). by rewrite /= HM'. - move=> _. exists None, (| encode_tape t |). apply /TM_facts.TM_eval_iff. exists 1. move: E. rewrite /= /step /TM_facts.step /=. move: t => [[ls a] rs] /=. by case: (trans' M (q, a)) => [[[??]?]|]. Qed.
imports: Undecidability(TM.SBTM TM.Util.SBTM_facts) Undecidability.Shared.Libs.PSL.FiniteTypes.FinTypes PeanoNat Lia List ssreflect ssrbool ssrfun