proposition: Lemma PCP_MPCP x y B : B <<= P -> x <<= Sigma -> y <<= Sigma -> (#_L x) ++ tau1 B = # :: (#_R y) ++ tau2 B -> exists A, A <<= x0/y0::R /\ x ++ tau1 A = y ++ tau2 A.
proof: Proof. revert x y. induction B; cbn -[fresh P] in *; intros. - exfalso. rewrite !app_nil_r in H2. eapply hash_L_diff in H2 as []. - assert (a el P) as [ -> | [ -> | (x' & y' & ? & -> & ?) ] ] % P_inv by intuition; cbn -[fresh P] in *. + exfalso. setoid_rewrite app_comm_cons in H2 at 2. eapply list_prefix_inv in H2 as [[] % hash_L_diff E2]. * now eapply doll_hash_L. * rewrite <- hash_swap. rewrite in_app_iff. intros [ | [ | []]]. { eapply doll_hash_L; eauto. } now eapply fresh_spec in H3 as []. + exists []. assert ((#_L x ++ [#]) ++ $ :: tau1 B = (# :: #_R y) ++ $ :: tau2 B) by now simpl_list. eapply list_prefix_inv in H3. { rewrite hash_swap in H3. inv H3. inv H4. eapply hash_R_inv in H6 as ->. firstorder. } * rewrite in_app_iff. intros [ | [ | []]]. { eapply doll_hash_L in H4; eauto. } now eapply fresh_spec in H4 as []. * rewrite <- hash_swap. rewrite in_app_iff. intros [ | [ | []]]. { eapply doll_hash_L; eauto. } now eapply fresh_spec in H4 as []. + assert ((#_L x ++ #_L x') ++ tau1 B = # :: (#_R y ++ #_R y') ++ tau2 B) by now simpl_list. rewrite <- hash_L_app, <- hash_R_app in H5. eapply IHB in H5 as (A & ? & ?). * exists (x' / y' :: A). intuition idtac; try inv H7; auto with datatypes; cbn; now autorewrite with list in *. * eapply incl_cons_inv. eassumption. * eapply incl_app. { eauto. } intros ? ?. destruct H3. { inv H3. eauto. } eapply R_Sigma, sym_word_l; eauto. * eapply incl_app. { eauto. } intros ? ?. destruct H3. { inv H3. eauto. } eapply R_Sigma, sym_word_R; eauto. Qed.
imports: Bool List Undecidability.PCP.PCP Undecidability.PCP.Util.Facts Undecidability.PCP.Util.PCP_facts Undecidability.Synthetic.Definitions