proposition: Lemma inverse_simulation_step q t x q' t' : SR.rew srs (encode_config q t) x -> step M (q, t) = Some (q', t') -> x = encode_config 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 Ey: (encode_config q t) => y Hyx. move: t Hyx Ey => [[ls a] rs] [] u v > /In_srsI []. - move=> > + H. move: H. rewrite (reassoc ⦇). move=> /encode_config_eq_app [<-] [<-]. by rewrite /step => _ ->. - move=> > + b H. move: H. rewrite (reassoc #b). move=> /encode_config_eq_app [<-] [<-]. by rewrite /step => _ ->. - move=> > + b H. move: H. move=> /encode_config_eq_app [<-] [<-]. by rewrite /step => _ ->. - move=> q'' a'' > + H. move: H. rewrite !(reassoc ⦇). move=> /encode_config_eq_app [<-] [<-] []. case: ls => [|l ?] /=. + rewrite /step. by move=> -> -> -> [] <- <-. + move=> /(app_inj_tail _ (_ :: _) _ (#l)) []. by case: l. - move=> ???? + b H. move: H. rewrite !(reassoc #b). move=> /encode_config_eq_app [<-] [<-] []. case: ls => [|l ?] /=. + move=> /(@app_inj_tail nat _ []) []. by case: b. + rewrite /step. move=> -> -> -> [] <- <- /=. by rewrite -app_assoc. - move=> > + H. move: H. move=> /encode_config_eq_app [<-] [<-] [->]. case: rs => [|r ?]; last by case: r. case: v; last done. rewrite /step. move=> _ -> [] <- <- /=. by rewrite -app_assoc. - move=> ???? + b H. move: H. move=> /encode_config_eq_app [<-] [<-] [->]. case: rs => [|r ?]; first by case: b. move=> [/encode_symbol_inj ->] ->. rewrite /step. move=> -> [] <- <- /=. by rewrite -app_assoc. Qed.
imports: Undecidability(TM.SBTM TM.Util.SBTM_facts) PeanoNat Lia List ssreflect ssrbool ssrfun