proposition: Lemma inverse_simulation q t q' ts' : TM.eval M' (Some q) (| encode_tape t |) q' ts' -> exists k, steps M k (q, t) = None.
proof: Proof. move=> /TM_facts.TM_eval_iff => - [k Hk]. exists k. elim: k q t q' ts' Hk; first done. move=> k IH q t q' ts' Hk. rewrite (steps_plus 1 k). case Hqt: (steps M 1 (q, t)) => [[q'' t'']|]; last done. move: Hqt => /simulation_step [t'''] [H'qt Et''t''']. move: Hk => /=. rewrite H'qt. have : canonize_tape t''' = canonize_tape (encode_tape t''). { rewrite Et''t'''. by case: (t'''). } by move=> /TM_loopM_canonize_tape /[apply] => - [?] /IH. Qed.
imports: Undecidability(TM.SBTM TM.Util.SBTM_facts) Undecidability.Shared.Libs.PSL.FiniteTypes.FinTypes PeanoNat Lia List ssreflect ssrbool ssrfun