proposition: Lemma simulation_step q t q' t' : step M (q, t) = Some (q', t') -> SR.rew srs (encode_config q t) (encode_config q' t').
proof: Proof. rewrite /step. move: t => [[ls a] rs]. move E: (trans' M (q, a)) => [[[q'' a''] d]|]; last done. move=> [] <- <- /=. move: d ls rs E => [] => [[|l ls] rs|ls [|r rs]]. - move=> /In_srs_l1 /In_srsE /SR.rewB. by move=> /(_ [] (map encode_symbol rs ++ [⦈])). - move=> /In_srs_l2 /(_ l) /In_srsE /SR.rewB. move=> /(_ (⦇ :: rev (map encode_symbol ls)) (map encode_symbol rs ++ [⦈])). by rewrite /= -!app_assoc. - move=> /In_srs_r1 /In_srsE /SR.rewB. move=> /(_ (⦇ :: rev (map encode_symbol ls)) []). by rewrite /= -!app_assoc. - move=> /In_srs_r2 /(_ r) /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