proposition: Fact SR_MPCP x : x <<= Sigma -> x ≻* y0 -> exists A, A <<= P /\ tau1 A = x ++ [#] ++ tau2 A.
proof: Proof. intros. revert H. pattern x; refine (rewt_induct _ _ H0). - exists [e]. cbn. firstorder. now simpl_list. - clear x H0. intros. inv H. destruct H1 as (A & ? & ?). { pose (app_incl_l H2). pose (app_incl_R (app_incl_R H2)). repeat eapply incl_app; try assumption. eauto. } exists (cards x1 ++ [(u / v)] ++ cards y1 ++ [ [#] / [#] ] ++ A). split. + repeat (eapply incl_app); try assumption; unfold P. * eapply cards_subset. eapply app_incl_l. eassumption. * eapply incl_appr. eapply incl_appl. now apply incl_sing. * eapply cards_subset. eapply app_incl_R. eapply app_incl_R. eassumption. * eauto. + simpl_list. cbn. rewrite H1. now simpl_list. 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