proposition: Lemma inverse_simulation q t : SR.rewt (srs ++ map SR.swap srs) (encode_config q t) [⦈; ⦇] -> exists k, steps M k (q, t) = None.
proof: Proof. move Eu: (encode_config q t) => u. move Ev: ([⦈; ⦇]) => v Huv. elim: Huv q t Eu Ev. { by move=> ?? [[??]?] <-. } move=> x y z + _ + q t ??. subst x z. case E: (step M (q, t)) => [[q' t']|]; first last. { move=> *. by exists 1. } move=> /SR_facts.rew_app_inv []. { move: (E) => /inverse_simulation_step /[apply] ->. move=> /(_ _ _ erefl erefl) [k Hk]. exists (1+k). by rewrite steps_plus /= E. } move: (E) => /inverse_simulation_back_step /[apply] [[q'']] [t''] [-> H'']. move=> /(_ _ _ erefl erefl) [[|k] Hk]; first done. exists k. move: Hk. by rewrite (steps_plus 1 k) /= H''. Qed.
imports: Undecidability(TM.SBTM TM.Util.SBTM_facts) Undecidability(StringRewriting.Reductions.SBTM_HALT_to_SR) PeanoNat Lia List ssreflect ssrbool ssrfun