proposition: Theorem PCP_FST B : entailment_FSTeq (solvable' B) -> PCPb B.
proof: Proof. intros H. specialize (H Acz FST_interp). unshelve eapply PCP_ZFeq. - exact Acz. - exact Acz_interp. - intros N. apply AEmpty. - apply Acz_ZFeq'. - apply Acz_standard. - specialize (H (fun _ : nat => AEmpty) FST_FSTeq). assert (HE : @min_model Acz Acz_interp = @min_model' Acz FST_interp). { unfold min_model, min_model'. f_equal. } apply min_embed' in H. apply impl_sat in H. + rewrite <- HE in H. apply min_correct in H; trivial. apply Acz_ZFeq'. + intros phi Hp % in_rev. specialize (@min_axioms' Acz Acz_interp). intros HA. rewrite <- HE. apply HA; trivial. apply Acz_ZFeq'. Qed.
imports: Undecidability.FOL(Syntax.Facts Semantics.Tarski.FullFacts Deduction.FullNDFacts ZF FST) Undecidability.FOL.Sets(Models.Aczel Models.ZF_model ZF minZF FST) Undecidability.FOL.Reductions(PCPb_to_ZF PCPb_to_ZFeq PCPb_to_minZF PCPb_to_minZFeq PCPb_to_ZFD) Lia Undecidability.PCP(PCP) Undecidability(Shared.ListAutomation)