proposition: Lemma simulation q t : (exists q' t', TM.eval M q t q' t') -> exists k, steps k ((encode_state q), (encode_tape (Vector.hd t))) = None.
proof: Proof. move=> [q'] [t'] /TM_facts.TM_eval_iff [n]. elim: n q t. { move=> q t. rewrite /= /TM_facts.haltConf /=. case E: (TM.halt q) => [|]; last done. move: E => /simulation_halt H _. exists 1. by apply: H. } move=> n IH q t. rewrite /= /TM_facts.haltConf /=. case E: (TM.halt q) => [|]. { move: E => /simulation_halt H _. exists 1. by apply: H. } rewrite (Vector.eta t). move: E => /simulation_step => /(_ (Vector.hd t)) [k1]. move: (VectorDef.tl t). apply: Vector.case0. move: (TM_step _) => [q'' ts''] Hk1 /IH [k2 Hk2] /=. exists ((S k1) + k2). rewrite (steps_plus). move: (encode_state q, _) Hk1 Hk2 => x. move Hk1: (steps (S k1) x) => [[q''' t''']|] /=; last done. move=> [] <- Ht''' /(@steps_truncate M'). rewrite -Ht'''. by move=> /steps_truncate. Qed.
imports: Undecidability(TM.SBTM TM.Util.SBTM_facts) Undecidability.Shared.Libs.PSL.FiniteTypes.FinTypes PeanoNat Lia List ssreflect ssrbool ssrfun