proposition: Theorem PCP_HF2 B rho : standard M -> rho ⊨ solvable B -> exists s, derivable B s s.
proof: Proof. Proof using M_ZF VIEQ. intros VIN (n & f & s & X & [[[[H1 H2] H3] H4] H5]). assert (H1' : htrans n) by apply H1. clear H1. assert (H4' : M_opair n X ∈ f) by apply H4. clear H4. assert (H5' : M_opair s s ∈ X) by apply H5. clear H5. assert (H2' : M_function f). { intros x y y' H H'. apply VIEQ. eapply H2. apply H. apply H'. } clear H2. assert (H3' : M_opair ∅ (M_enc_stack B) ∈ f). { erewrite <- eval_enc_stack. apply H3. } destruct H3 as [_ H3]. assert (H3'' : forall k x y, k ∈ n -> M_opair k x ∈ f -> M_combinations B x y -> M_opair (σ k) y ∈ f). { intros k x y Hn Hk Hy. apply (H3 k x y); auto. fold sat. eapply M_combinations_spec; eauto. } clear H3. destruct (@M_solutions_el B f n X (M_opair s s)) as (u&v&H1&H2); trivial. now split. exists u. apply opair_inj in H1 as [H ->]. apply enc_string_inj in H as ->. apply H2. 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)