proposition: Fact MPCP_SR x y A : A <<= P -> x <<= Sigma -> y <<= Sigma -> tau1 A = x ++ [#] ++ y ++ tau2 A -> y ++ x ≻* y0.
proof: Proof. intros ?. revert x y. induction A; intros. - exfalso. destruct x; inv H2. - assert (a el P) as [ -> | [ -> | [ | [-> | (? & ? & ->)]]]] % P_inv by (now apply H). + exfalso. cbn -[fresh] in H2. destruct x. { inv H2. destruct (sep_doll H4). } inversion H2. edestruct doll_sig; eauto. + cbn -[fresh] in *. autorewrite with list in *. cbn -[fresh] in *. eapply list_prefix_inv in H2 as [<- ?]; [destruct y|..]. * reflexivity. * exfalso. inversion H2. edestruct doll_sig; eauto. * intros E. edestruct hash_sig; eauto. * intros E. edestruct hash_sig; eauto. + destruct a as (u, v). cbn -[fresh] in H2. edestruct (split_inv H2) as (x' & ->). { intros E. edestruct hash_sig. { unfold Sigma. rewrite !in_app_iff. do 2 right. now eapply sym_word_l; eauto. } reflexivity. } econstructor. { eapply rewB. now eassumption. } enough ( (y ++ v) ++ x' ≻* y0) by now autorewrite with list in *. eapply IHA; autorewrite with list in *. * eauto. * eapply app_incl_R. eassumption. * eapply incl_app; eauto. * now eapply app_inv_head in H2. + cbn -[fresh] in H2. destruct x; [inv H2 |]. * simpl_list. change y with ([] ++ y). eapply IHA; eauto using cons_incl. * inversion H2. edestruct hash_sig; eauto. + cbn -[fresh] in *. rename x1 into a. destruct x. * inversion H2. edestruct hash_sig; eauto. * inv H2. replace (y ++ n :: x) with ((y ++ [n]) ++ x) by now simpl_list. eapply IHA. ** eapply cons_incl. eassumption. ** eapply cons_incl. eassumption. ** eapply incl_app. { eassumption. } now eapply incl_sing. ** simpl_list. eassumption. Qed.
imports: List Undecidability.PCP.PCP Undecidability.PCP.Util.Facts Undecidability.PCP.Util.PCP_facts Undecidability.StringRewriting.SR Undecidability.StringRewriting.Util.Definitions Undecidability.Synthetic.Definitions