proposition: Lemma pcp_hand_inv p q : lc ⊳ p∕q -> In (p,q) lc \/ exists x y p' q', In (x,y) lc /\ lc ⊳ p'∕q' /\ p = x++p' /\ q = y++q' /\ (x <> nil /\ y = nil \/ x = nil /\ y <> nil \/ x <> nil /\ y <> nil ).
proof: Proof. induction 1 as [ x y H | x y p q H1 H2 IH2 ]. + left; auto. + destruct x as [ | a x ]; [ destruct y as [ | b y ] | ]. * simpl; auto. * right; exists nil, (b::y), p, q; simpl; repeat split; auto. right; left; split; auto; discriminate. * right; exists (a::x), y, p, q; simpl; repeat split; auto. destruct y. - left; split; auto; discriminate. - right; right; split; discriminate. Qed.
imports: List Undecidability.PCP.PCP Undecidability.PCP.Util.Facts Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts MoreEnumerabilityFacts ListEnumerabilityFacts) Coq.Init.Wf Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list utils_nat finite)