proposition: Lemma simulation q t k : steps M k (q, t) = None -> SR.rewt (srs ++ map SR.swap srs) (encode_config q t) [⦈; ⦇].
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 ?. move=> /IH. apply: SR.rewS. apply /SR_facts.rew_app_inv. by left. - move: E => /simulation_halt /SR_facts.rewt_subset + _. apply. apply: incl_appl. by apply: incl_refl. Qed.
imports: Undecidability(TM.SBTM TM.Util.SBTM_facts) Undecidability(StringRewriting.Reductions.SBTM_HALT_to_SR) PeanoNat Lia List ssreflect ssrbool ssrfun