proposition: Lemma inverse_simulation q t k : steps k ((encode_state q), (encode_tape (Vector.hd t))) = None -> exists q' t', TM.eval M q t q' t'.
proof: Proof. elim: k q t; first done. move=> k IH q t. move Hq: (TM.halt q) => [|]. { move=> _. exists q, t. by apply: TM.eval_halt. } move: (Hq) => /simulation_step => /(_ (Vector.hd t)). move=> [k1]. move Hk1: (steps (S k1) _) => [[q' t']|]; last done. move=> [] Hq't'. move: Hk1 => /steps_sync H /H{H} /steps_truncate. move E: (TM_step _) Hq't' => [q'' t'']. move=> [] -> -> /steps_truncate /IH. move=> [q'''] [t'''] /TM_facts.TM_eval_iff [n Hn]. exists q''', t'''. apply /TM_facts.TM_eval_iff. exists (S n). rewrite /= /TM_facts.haltConf Hq -Hn -E (Vector.eta t) /=. move: (Vector.tl t). by apply: Vector.case0. Qed.
imports: Undecidability(TM.SBTM TM.Util.SBTM_facts) Undecidability.Shared.Libs.PSL.FiniteTypes.FinTypes PeanoNat Lia List ssreflect ssrbool ssrfun