proposition: Lemma loop_deductive { p : peirce } phi : minZFeq' ⊢ phi ↔ rm_const_fm (embed phi).
proof: Proof. induction phi using form_ind_subst; cbn. - apply CI; apply II; auto. - rewrite (vec_inv2 t). cbn. destruct Vector.hd as [x|[]], (Vector.hd (Vector.tl t)) as [y|[]]. cbn. destruct P0; cbn in *; apply CI; apply II. + apply elem_iff; auto. + apply elem_iff; auto. + apply equal_iff; auto. + apply equal_iff; auto. - destruct b0; cbn in *; apply CI; apply II. + apply CE1 in IHphi1. apply CE1 in IHphi2. apply CI; eapply IE. 1,3: eapply Weak; eauto. eapply CE1; auto. eapply CE2; auto. + apply CE2 in IHphi1. apply CE2 in IHphi2. apply CI; eapply IE. 1,3: eapply Weak; eauto. eapply CE1; auto. eapply CE2; auto. + apply CE1 in IHphi1. apply CE1 in IHphi2. eapply DE; try now apply Ctx. * apply DI1. eapply IE; try now apply Ctx. eapply Weak; try apply IHphi1. auto. * apply DI2. eapply IE; try now apply Ctx. eapply Weak; try apply IHphi2. auto. + apply CE2 in IHphi1. apply CE2 in IHphi2. eapply DE; try now apply Ctx. * apply DI1. eapply IE; try now apply Ctx. eapply Weak; try apply IHphi1. auto. * apply DI2. eapply IE; try now apply Ctx. eapply Weak; try apply IHphi2. auto. + apply CE2 in IHphi1. apply CE1 in IHphi2. apply II. eapply IE. eapply Weak; eauto. eapply IE. auto. eapply IE; try now apply Ctx. eapply Weak; eauto. + apply CE1 in IHphi1. apply CE2 in IHphi2. apply II. eapply IE. eapply Weak; eauto. eapply IE. auto. eapply IE; try now apply Ctx. eapply Weak; eauto. - destruct q; cbn in *; apply CI; apply II. + prv_all' x. rewrite rm_const_fm_subst, <- embed_subst. eapply IE. * eapply Weak; try eapply CE1, H. auto. * apply AllE. auto. + prv_all' x. eapply IE. * eapply Weak; try eapply CE2, H. auto. * rewrite embed_subst, <- rm_const_fm_subst. apply AllE. auto. + assert1 H'. use_exists' H' x. apply ExI with x. rewrite rm_const_fm_subst, <- embed_subst. eapply IE; try now apply Ctx. eapply Weak; try eapply CE1, H. auto. + assert1 H'. use_exists' H' x. apply ExI with x. rewrite rm_const_fm_subst, <- embed_subst. eapply IE; try now apply Ctx. eapply Weak; try eapply CE2, H. auto. Qed.
imports: Undecidability.FOL(Semantics.Tarski.FullFacts Syntax.Facts Deduction.FullNDFacts) Undecidability.FOL.Sets(ZF minZF) Undecidability.FOL.Reductions(PCPb_to_ZF PCPb_to_minZF PCPb_to_ZFD) Undecidability(Shared.ListAutomation)