proposition: Lemma MPCP_PCP x y A : A <<= x0/y0 :: R -> x ++ tau1 A = y ++ tau2 A -> exists B, B <<= P /\ (#_L x) ++ tau1 B = # :: #_R y ++ tau2 B.
proof: Proof. revert x y; induction A; cbn -[fresh P] in *; intros. - rewrite !app_nil_r in H0. subst. exists [e]. firstorder. cbn -[fresh]. enough ((#_L y ++ [#]) ++ [$] = # :: #_R y ++ [$]) by now autorewrite with list in *. now rewrite hash_swap. - destruct a as (x', y'). assert ( (x ++ x') ++ tau1 A = (y ++ y') ++ tau2 A) by now simpl_list. eapply IHA in H1 as (B & ? & ?) ; [ | firstorder]. rewrite hash_L_app, hash_R_app in H2. autorewrite with list in H2. destruct (is_cons x' || is_cons y') eqn:E. + exists ( (#_L x' / #_R y') :: B). split. * intros ? [ <- | ]; [ | eauto]. unfold P. rewrite in_app_iff, in_map_iff. right. exists (x', y'). split; [easy|]. eapply filter_In. eauto. * eassumption. + exists B. rewrite orb_false_iff, <- !not_true_iff_false, !is_cons_true_iff in E. destruct E. destruct x', y'; firstorder congruence. Qed.
imports: Bool List Undecidability.PCP.PCP Undecidability.PCP.Util.Facts Undecidability.PCP.Util.PCP_facts Undecidability.Synthetic.Definitions