proposition: Lemma prv_to_min_inductive { p : peirce } A n : binZF <<= A -> A ⊢ rm_const_fm (inductive $n) -> A ⊢ is_inductive $n.
proof: Proof. cbn. intros HA HI. apply CI. - apply CE1 in HI. use_exists' HI x. clear HI. apply (ExI x). cbn. assert1 H. apply CE in H as [H1 H2]. apply CI; trivial. change (∃ $0 ≡' ↑ n ∧ x`[↑] ∈' $0) with (∃ $0 ≡' $n`[↑] ∧ x`[↑] ∈' $0) in H2. now simpl_ex_in H2. - apply CE2 in HI. prv_all' x. apply (AllE x) in HI. cbn in HI. simpl_ex_in HI. change (∃ $0 ≡' ↑ n ∧ x`[↑] ∈' $0) with (∃ $0 ≡' $n`[↑] ∧ x`[↑] ∈' $0) in HI. simpl_ex_in HI. rewrite imps in *. use_exists' HI y. clear HI. assert1 H. apply (ExI y). cbn. subsimpl. apply CI. + apply CE1 in H. use_exists' H a. clear H. assert1 H. apply CE in H as [H1 H2]. simpl_ex_in H1. prv_all' b. apply (AllE b) in H2. cbn in H2. subsimpl_in H2. eapply iff_equiv; try apply H2; try tauto. intros B HB. clear H2. eapply Weak in H1; try apply HB. split; intros H2. * use_exists' H1 z. clear H1. assert1 H. apply CE in H as [H H']. apply prv_ex_eq in H; try rewrite <- HB; auto. cbn in H. subsimpl_in H. rewrite ?eq_subst in H. cbn in H. subsimpl_in H. apply prv_ex_eq in H; try rewrite <- HB; auto. cbn in H. subsimpl_in H. eapply Weak in H2. apply (DE H2). 3: auto. -- apply (ExI x). cbn. subsimpl. apply CI; auto. apply (AllE x) in H'. cbn in H'. subsimpl_in H'. apply CE2 in H'. eapply IE. apply (Weak H'); auto. apply DI1. rewrite ?eq_subst. cbn. subsimpl. apply minZF_refl. rewrite <- HB. auto 6. -- apply (ExI z). cbn. subsimpl. apply CI. ++ apply (AllE z) in H'. cbn in H'. subsimpl_in H'. apply CE2 in H'. eapply IE. apply (Weak H'); auto. apply DI2. rewrite ?eq_subst. cbn. subsimpl. apply minZF_refl. rewrite <- HB. auto 6. ++ apply (AllE b) in H. cbn in H. subsimpl_in H. apply CE2 in H. eapply IE. apply (Weak H); auto. rewrite ?eq_subst. cbn. subsimpl. apply DI2. auto. * use_exists' H1 z. clear H1. assert1 H. apply CE in H as [H H']. apply prv_ex_eq in H; try rewrite <- HB; auto. cbn in H. subsimpl_in H. rewrite ?eq_subst in H. cbn in H. subsimpl_in H. apply prv_ex_eq in H; try rewrite <- HB; auto. cbn in H. subsimpl_in H. eapply Weak in H2. use_exists' H2 c. 2: auto. clear H2. assert1 H1. apply CE in H1 as [H1 H2]. apply (AllE c) in H'. cbn in H'. subsimpl_in H'. apply CE1 in H'. eapply Weak in H'. apply (IE H') in H1. 2: auto. clear H'. apply (DE H1). -- apply DI1. eapply minZF_elem. rewrite <- HB, HA. auto 8. 3: apply (Weak H2); auto. apply minZF_refl. rewrite <- HB, HA. auto 8. rewrite ?eq_subst. cbn. subsimpl. auto. -- apply DI2. apply (AllE b) in H. cbn in H. subsimpl_in H. apply CE1 in H. eapply DE'. rewrite ?eq_subst. cbn. subsimpl. rewrite ?eq_subst in H. cbn in H. subsimpl_in H. eapply IE. apply (Weak H). auto. eapply minZF_elem. rewrite <- HB, HA. auto 8. 3: apply (Weak H2); auto. 2: auto. apply minZF_refl. rewrite <- HB, HA. auto 8. + apply CE2 in H. change (∃ $0 ≡' ↑ n ∧ y`[↑] ∈' $0) with (∃ $0 ≡' $n`[↑] ∧ y`[↑] ∈' $0) in H. now simpl_ex_in H. Qed.
imports: Undecidability.FOL.Syntax.Facts Undecidability.FOL.Syntax.Asimpl Undecidability.FOL.Semantics.Tarski.FullFacts Undecidability.FOL.Deduction.FullNDFacts Undecidability.FOL.Sets(binZF ZF) Undecidability.FOL.Reductions.PCPb_to_ZF Undecidability(Shared.ListAutomation) Morphisms Undecidability.FOL(Reductions.PCPb_to_ZFeq)