proposition: Lemma ΓPCP_completeness_ind {Q P x y v w n} : incl Q P -> der ΓPCP n (PCPf' Q P (encode_pair (encode_word' bullet x) (encode_list encode_bool v)) (encode_pair (encode_word' bullet y) (encode_list encode_bool w))) -> exists A, incl A P /\ x ++ v ++ tau1 A = y ++ w ++ tau2 A.
proof: Proof. elim: n Q x y v w; first by move=> > _ /derE. move=> n IH Q x y v w HQ /derE. move=> [ζ [s [k [+ [+]]]]]. have Hu (r) : r = arr r (arr r r) -> False. { move /(f_equal size) => /=. by lia. } rewrite /ΓPCP /In -/ΓPCP. case; last case; last case; last case; last case; last done. all: move=> <-. { case: k=> [|k] /=; last by move=> /Forall_cons_iff [/not_ΓPCP_rrr]. move=> _. case. do 7 (move=> _). move=> ->. case=> /encode_word'_injective + /encode_list_injective. move=> -> ->. do 6 (move=> _). exists []. by constructor. } all: case: k=> [|k]. 1,3,5,7: move=> _ /=; case=> <- *; exfalso; apply: Hu; by eassumption. all: case: k=> [|k]. 2,4,6,8: by move=> /= /Forall_cons_iff [_] /Forall_cons_iff [/not_ΓPCP_rrr]. all: rewrite substitute_arrP /arguments /target. all: move=> /Forall_cons_iff [Hder _]; rewrite ? substitute_pairP. { move=> [H0] [[_ [H123 H4]]] [_] [[_ [H5 Hv]]] [_ [H6 Hw]]. move: H123 HQ. case: Q; first done. move=> [v' w'] Q. rewrite /encode_list -/encode_list /encode_word_pair -/encode_word_pair. rewrite ? substitute_pairP. move=> [_ [[_ [H1 H2]] H3]]. move: Hder. rewrite ? transparent_encode_pair //. rewrite H1 H2 H4 H5 H6. move /IH => /(_ (incl_refl P)). move=> [A [HAP HxyA]]. move /(_ (v', w')). move /(_ (in_eq _ _)) => ?. move: v w Hv Hw => [|? ?] [|? ?]. { exists ((v', w') :: A). constructor; [by apply /incl_cons | by assumption]. } all: by rewrite /= H0. } { move=> [H0] [[_ [H12 H3]]] H4. move: H12 HQ. case: Q; first done. move=> ? Q. rewrite /encode_list -/encode_list ? substitute_pairP. move=> [_ [_ H2]]. move=> /incl_cons_inv [_ HQ]. move: Hder. rewrite ? transparent_encode_pair => //. rewrite H2 H3 H4. move /IH. by apply. } { move=> [H0] [H1] [_] [[_ [H2]]] H34 H5. move: H34. case: v; first done. move=> a v. rewrite /encode_list -/encode_list substitute_pairP. move=> [_ [H3 H4]]. move: Hder. rewrite ? transparent_encode_pair => //. rewrite H1 H2 H3 H4 H5 -encode_word'_last. move /IH. rewrite -/(app [a] v). move /(_ HQ) => [A [?]]. rewrite - ? app_assoc => ?. by exists A. } { move=> [H0] [H1] [_] [H5] [_ [H2 H34]]. move: H34. case: w; first done. move=> a w. rewrite /encode_list -/encode_list substitute_pairP. move=> [_ [H3 H4]]. move: Hder. rewrite ? transparent_encode_pair => //. rewrite H1 H2 H3 H4 H5 -encode_word'_last. move /IH. rewrite -/(app [a] w). move /(_ HQ) => [A [?]]. rewrite - ? app_assoc => ?. by exists A. } Qed.
imports: List Lia ssreflect ssrbool ssrfun Undecidability.HilbertCalculi.HSC Undecidability.HilbertCalculi.Util.HSCFacts Undecidability.PCP.PCP