proposition: Lemma inverse_simulation_back_step q t x q' t' : SR.rew (map SR.swap srs) (encode_config q t) x -> step M (q, t) = Some (q', t') -> exists q'' t'', x = encode_config q'' t'' /\ step M (q'', t'') = Some (q, t).
proof: Proof. have reassoc (n m : nat) (u v : list nat) : u ++ (n :: m :: v) = (u ++ [n]) ++ m :: v. { by rewrite -app_assoc. } move=> /rew_swap. move Ey: (encode_config q t) => y Hxy. case: Hxy Ey => u v > /In_srsI []. - move=> > _ H. exfalso. apply: (left_marker_nth q t (length u)). rewrite H. rewrite nth_error_app2; first by lia. by have ->: S (length u) - length u = 1 by lia. - move: t => [[??]?] > E b /encode_config_eq_app [->] [->] [-> ->]. by rewrite /step E. - move: t => [[??]?] > E b /encode_config_eq_app [->] [->] [-> ->]. by rewrite /step E. - move: t => [[ls ?] rs] q'' a ? a' E H _. move: H E. rewrite !(reassoc ⦇). move=> /encode_config_eq_app [->] [->] [/app_left_marker] [-> ->]. move: rs => [|r rs]. { by case: a'. } move=> [] /encode_symbol_inj -> -> E. exists q'', ([], a, rs). split; first done. by rewrite /step E. - move: t => [[ls ?] rs] q'' a ? a' E b H _. move: H E. move=> /encode_config_eq_app [->] [->] [->]. move: rs => [|r rs]. { by case: a'. } move=> [] /encode_symbol_inj -> -> E. exists q'', (b :: ls, a, rs). split; first by rewrite /= -!app_assoc. by rewrite /step E. - move: t => [[ls ?] rs] q'' a ? a' E H _. move: H E. rewrite !(reassoc #a'). move=> /encode_config_eq_app [->] [->] []. move: ls => [|l ls]. { move=> /(@app_inj_tail nat _ []) []. by case: a'. } move=> /= /(@app_inj_tail nat _ (_ :: _)) [-> /encode_symbol_inj ->]. move: rs => [|r rs]; last by case: r. move=> [->] E. exists q'', (ls, a, []). split; first done. by rewrite /step E. - move: t => [[ls ?] rs] q'' a ? a' E b H _. move: H E. rewrite !(reassoc #a'). move=> /encode_config_eq_app [->] [->] [+ ->]. move: ls => [|l ls]. { move=> /(@app_inj_tail nat _ []) []. by case: a'. } cbn. move=> /(@app_inj_tail nat _ (_ :: _)) [-> /encode_symbol_inj ->] E. exists q'', (ls, a, b :: rs). split; first done. by rewrite /step E. Qed.
imports: Undecidability(TM.SBTM TM.Util.SBTM_facts) Undecidability(StringRewriting.Reductions.SBTM_HALT_to_SR) PeanoNat Lia List ssreflect ssrbool ssrfun