proposition: Theorem PCP_ZF1 B s : derivable B s s -> forall rho, rho ⊨ solvable B.
proof: Proof. Proof using VIEQ M_ZF. intros H rho. destruct (derivable_derivations H) as [n Hn]. unfold solvable. exists (numeral n), (M_enc_derivations B n), (M_enc_string s), (M_enc_stack (derivations B n)). split; [split; [split; [split |] |] |]. - apply numeral_omega. - unfold function'. intros k x y H1 H2. apply VIEQ. apply (enc_derivations_fun H1 H2). - apply enc_derivations_solutions. - cbn. apply derivations_enc_derivations. - now apply enc_stack_el. Qed.
imports: Undecidability.FOL.ZF Undecidability.FOL.Syntax.Facts Undecidability.FOL.Semantics.Tarski.FullFacts Undecidability.FOL.Sets.ZF Lia Undecidability.PCP(PCP Util.PCP_facts Reductions.PCPb_iff_dPCPb) Undecidability(Shared.ListAutomation)