proposition: Theorem dPCP_HFD B : dPCPb B -> HFeq ⊢ solvable B.
proof: Proof. intros [s H]. edestruct (derivable_derivations H) as [n Hn]. unfold solvable. apply ExI with (tnumeral n). cbn. apply ExI with (enc_derivations B n). cbn. apply ExI with (enc_string s). cbn. subsimpl. apply ExI with (enc_stack (derivations B n)). cbn. rewrite !enc_stack_subst, !combinations_subst. cbn. subsimpl. repeat apply CI. - specialize (@HF_numeral HFeq n (fun phi H => H)). apply CE1. - specialize (@HF_numeral HFeq n (fun phi H => H)). apply CE2. - prv_all x. prv_all y. prv_all z. apply enc_derivations_functional. - apply enc_derivations_base. - prv_all x. prv_all y. prv_all z. rewrite !combinations_subst. cbn. subsimpl. apply combinations_step. - apply enc_derivations_step. - now apply enc_stack_spec. Qed.
imports: Undecidability.FOL.ZF Undecidability.FOL.Syntax.Facts Undecidability.FOL.Semantics.Tarski.FullFacts Undecidability.FOL.Sets.ZF Undecidability.FOL.Reductions.PCPb_to_HF Undecidability.PCP(PCP Util.PCP_facts Reductions.PCPb_iff_dPCPb) Undecidability(Shared.ListAutomation)