proposition: Lemma ΓPCP_step {P x y v w} : In (v, w) P -> hsc ΓPCP (PCPf' P P (encode_pair (encode_word' bullet x) (encode_list encode_bool v)) (encode_pair (encode_word' bullet y) (encode_list encode_bool w))) -> hsc ΓPCP (PCPf P x y).
proof: Proof. move /(@in_split _ _) => [R [Q ?]] ?. have : hsc ΓPCP (PCPf' ((v, w) :: Q) P (encode_pair (encode_word' bullet x) bullet) (encode_pair (encode_word' bullet y) bullet)). { apply: hsc_arr; last eassumption. evar (ζ : nat -> formula). instantiate (ζ := fun x => match x with | 0 => _ | 1 => _ | 2 => _ | 3 => _ | 4 => _ | 5 => _ | _ => _ end). apply: (hscI (ζ := ζ)). { rewrite /ΓPCP. do 1 right. left. by reflexivity. } by rewrite /ζ substitute_arrP /PCPf' ? transparent_encode_pair. } move /ΓPCP_saturate. apply. by eassumption. Qed.
imports: List Lia ssreflect ssrbool ssrfun Undecidability.HilbertCalculi.HSC Undecidability.HilbertCalculi.Util.HSCFacts Undecidability.PCP.PCP