proposition: Lemma simulation_halt q t : step M (q, t) = None -> SR.rewt srs (encode_config q t) [⦈; ⦇].
proof: Proof. rewrite /step. move: t => [[ls a] rs]. move E: (trans' M (q, a)) => [[[q'' a''] d]|]; first done. move=> _. elim: ls. { elim: rs. { apply: SR.rewS; [|by apply: SR.rewR]. by move: E => /In_srs_f /In_srsE /SR.rewB => /(_ [] []). } move=> r rs IH. apply: SR.rewS; [|by eassumption]. move: E => /In_srs_dr /(_ r) /In_srsE /SR.rewB. by move=> /(_ [⦇] (map encode_symbol rs ++ [⦈])). } move=> l ls IH. apply: SR.rewS; [|by eassumption]. move: E => /In_srs_dl /(_ l) /In_srsE /SR.rewB. move=> /(_ (⦇ :: rev (map encode_symbol ls)) (map encode_symbol rs ++ [⦈])). by rewrite /= -!app_assoc. Qed.
imports: Undecidability(TM.SBTM TM.Util.SBTM_facts) PeanoNat Lia List ssreflect ssrbool ssrfun