proposition: Lemma P_BPCP x : i_P x x -> dPCPb R.
proof: Proof. Proof using HS2 HS1 HP HI HF3 HF2 HF1 HD HE1 HE2 HE3 HER1 HER3. intros H. destruct (P_drv H) as (s&t&H1&H2&H3); subst. assert (ienc s == ienc t) as H4. - apply HE3 with x. now apply HE2. easy. - apply ienc_inj in H4. exists t. congruence. destruct (@HP x x) as [Hx _]. 1:easy. intros Hcc. apply Hx. now apply HE3 with (ienc s). Qed.
imports: Lia Arith Undecidability.PCP.PCP Undecidability.PCP.Util.PCP_facts Undecidability.Synthetic.DecidabilityFacts Undecidability(FOL.Utils.FullSyntax) Undecidability(FOL.FSAT) Undecidability.Shared.ListAutomation