Proofgold Address

Param nat_p^nat_p : ι → ο
Definition False^False := ∀ x0 : ο . x0
Definition not^not := λ x0 : ο . x0 ⟶ False
Param finite^finite : ι → ο
Definition infinite^infinite := λ x0 . not (finite x0)
Definition Subq^Subq := λ x0 x1 . ∀ x2 . x2 ∈ x0 ⟶ x2 ∈ x1
Definition and^and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Definition bij^bij := λ x0 x1 . λ x2 : ι → ι . and (and (∀ x3 . x3 ∈ x0 ⟶ x2 x3 ∈ x1) (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ x2 x3 = x2 x4 ⟶ x3 = x4)) (∀ x3 . x3 ∈ x1 ⟶ ∀ x4 : ο . (∀ x5 . and (x5 ∈ x0) (x2 x5 = x3) ⟶ x4) ⟶ x4)
Definition equip^equip := λ x0 x1 . ∀ x2 : ο . (∀ x3 : ι → ι . bij x0 x1 x3 ⟶ x2) ⟶ x2
Param ordsucc^ordsucc : ι → ι
Known nat_ind^nat_ind : ∀ x0 : ι → ο . x0 0 ⟶ (∀ x1 . nat_p x1 ⟶ x0 x1 ⟶ x0 (ordsucc x1)) ⟶ ∀ x1 . nat_p x1 ⟶ x0 x1
Known FalseE^FalseE : False ⟶ ∀ x0 : ο . x0
Known infinite_Finite_Subq_ex^{infinite_Finite_Subq_ex} : ∀ x0 . infinite x0 ⟶ ∀ x1 . nat_p x1 ⟶ ∀ x2 : ο . (∀ x3 . and (x3 ⊆ x0) (equip x3 x1) ⟶ x2) ⟶ x2
Definition nIn^nIn := λ x0 x1 . not (x0 ∈ x1)
Known EmptyE^EmptyE : ∀ x0 . nIn x0 0
Known andI^andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Known Subq_ref^Subq_ref : ∀ x0 . x0 ⊆ x0
Known Subq_Empty^Subq_Empty : ∀ x0 . 0 ⊆ x0
Known equip_ref^equip_ref : ∀ x0 . equip x0 x0
Known equip_0_Empty^{equip_0_Empty} : ∀ x0 . equip x0 0 ⟶ x0 = 0
Known dneg^dneg : ∀ x0 : ο . not (not x0) ⟶ x0
Param binunion^binunion : ι → ι → ι
Param Sing^Sing : ι → ι
Param nat_primrec^nat_primrec : ι → (ι → ι → ι) → ι → ι
Known nat_primrec_0^{nat_primrec_0} : ∀ x0 . ∀ x1 : ι → ι → ι . nat_primrec x0 x1 0 = x0
Known nat_primrec_S^{nat_primrec_S} : ∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 . nat_p x2 ⟶ nat_primrec x0 x1 (ordsucc x2) = x1 x2 (nat_primrec x0 x1 x2)
Param omega^omega : ι
Known ReplE_impred^ReplE_impred : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ prim5 x0 x1 ⟶ ∀ x3 : ο . (∀ x4 . x4 ∈ x0 ⟶ x2 = x1 x4 ⟶ x3) ⟶ x3
Known omega_nat_p^omega_nat_p : ∀ x0 . x0 ∈ omega ⟶ nat_p x0
Known ordsuccI2^ordsuccI2 : ∀ x0 . x0 ∈ ordsucc x0
Definition inj^inj := λ x0 x1 . λ x2 : ι → ι . and (∀ x3 . x3 ∈ x0 ⟶ x2 x3 ∈ x1) (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ x2 x3 = x2 x4 ⟶ x3 = x4)
Definition atleastp^atleastp := λ x0 x1 . ∀ x2 : ο . (∀ x3 : ι → ι . inj x0 x1 x3 ⟶ x2) ⟶ x2
Known atleastp_omega_infinite^{atleastp_omega_infinite} : ∀ x0 . atleastp omega x0 ⟶ infinite x0
Known ReplI^ReplI : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ x0 ⟶ x1 x2 ∈ prim5 x0 x1
Param ordinal^ordinal : ι → ο
Known ordinal_trichotomy_or_impred^{ordinal_trichotomy_or_impred} : ∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ ∀ x2 : ο . (x0 ∈ x1 ⟶ x2) ⟶ (x0 = x1 ⟶ x2) ⟶ (x1 ∈ x0 ⟶ x2) ⟶ x2
Known nat_p_ordinal^{nat_p_ordinal} : ∀ x0 . nat_p x0 ⟶ ordinal x0
Known least_ordinal_ex^{least_ordinal_ex} : ∀ x0 : ι → ο . (∀ x1 : ο . (∀ x2 . and (ordinal x2) (x0 x2) ⟶ x1) ⟶ x1) ⟶ ∀ x1 : ο . (∀ x2 . and (and (ordinal x2) (x0 x2)) (∀ x3 . x3 ∈ x2 ⟶ not (x0 x3)) ⟶ x1) ⟶ x1
Known equip_sym^equip_sym : ∀ x0 x1 . equip x0 x1 ⟶ equip x1 x0
Param setminus^setminus : ι → ι → ι
Known eb0c4..^{binunion_remove1_eq} : ∀ x0 x1 . x1 ∈ x0 ⟶ x0 = binunion (setminus x0 (Sing x1)) (Sing x1)
Known setminusE^setminusE : ∀ x0 x1 x2 . x2 ∈ setminus x0 x1 ⟶ and (x2 ∈ x0) (nIn x2 x1)
Known SingI^SingI : ∀ x0 . x0 ∈ Sing x0
Known omega_ordsucc^{omega_ordsucc} : ∀ x0 . x0 ∈ omega ⟶ ordsucc x0 ∈ omega
Known nat_p_omega^nat_p_omega : ∀ x0 . nat_p x0 ⟶ x0 ∈ omega
Known ordinal_ordsucc_In_Subq^{ordinal_ordsucc_In_Subq} : ∀ x0 . ordinal x0 ⟶ ∀ x1 . x1 ∈ x0 ⟶ ordsucc x1 ⊆ x0
Known 9c223..^{equip_ordsucc_remove1} : ∀ x0 x1 x2 . x2 ∈ x0 ⟶ equip x0 (ordsucc x1) ⟶ equip (setminus x0 (Sing x2)) x1
Known nat_p_trans^nat_p_trans : ∀ x0 . nat_p x0 ⟶ ∀ x1 . x1 ∈ x0 ⟶ nat_p x1
Param SNo^SNo : ι → ο
Param minus_SNo^minus_SNo : ι → ι
Param add_SNo^add_SNo : ι → ι → ι
Known add_SNo_rotate_3_1^{add_SNo_rotate_3_1} : ∀ x0 x1 x2 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ add_SNo x0 (add_SNo x1 x2) = add_SNo x2 (add_SNo x0 x1)
Known SNo_minus_SNo^{SNo_minus_SNo} : ∀ x0 . SNo x0 ⟶ SNo (minus_SNo x0)
Known add_SNo_minus_L2^{add_SNo_minus_L2} : ∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ add_SNo (minus_SNo x0) (add_SNo x0 x1) = x1
Known add_SNo_0R^add_SNo_0R : ∀ x0 . SNo x0 ⟶ add_SNo x0 0 = x0
Known omega_SNo^omega_SNo : ∀ x0 . x0 ∈ omega ⟶ SNo x0
Known add_SNo_omega_SR : ∀ x0 . x0 ∈ omega ⟶ ∀ x1 . x1 ∈ omega ⟶ add_SNo x0 (ordsucc x1) = ordsucc (add_SNo x0 x1)
Known add_SNo_In_omega^{add_SNo_In_omega} : ∀ x0 . x0 ∈ omega ⟶ ∀ x1 . x1 ∈ omega ⟶ add_SNo x0 x1 ∈ omega
Known Subq_tra^Subq_tra : ∀ x0 x1 x2 . x0 ⊆ x1 ⟶ x1 ⊆ x2 ⟶ x0 ⊆ x2
Known Eps_i_ex^Eps_i_ex : ∀ x0 : ι → ο . (∀ x1 : ο . (∀ x2 . x0 x2 ⟶ x1) ⟶ x1) ⟶ x0 (prim0 x0)
Param int^int : ι
Param SNoLe^SNoLe : ι → ι → ο
Known aa7e8..^{nonneg_int_nat_p} : ∀ x0 . x0 ∈ int ⟶ SNoLe 0 x0 ⟶ nat_p x0
Known int_add_SNo^int_add_SNo : ∀ x0 . x0 ∈ int ⟶ ∀ x1 . x1 ∈ int ⟶ add_SNo x0 x1 ∈ int
Known Subq_omega_int^{Subq_omega_int} : omega ⊆ int
Known int_minus_SNo^{int_minus_SNo} : ∀ x0 . x0 ∈ int ⟶ minus_SNo x0 ∈ int
Known add_SNo_minus_Le2b^{add_SNo_minus_Le2b} : ∀ x0 x1 x2 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNoLe (add_SNo x2 x1) x0 ⟶ SNoLe x2 (add_SNo x0 (minus_SNo x1))
Known SNo_0^SNo_0 : SNo 0
Known add_SNo_0L^add_SNo_0L : ∀ x0 . SNo x0 ⟶ add_SNo 0 x0 = x0
Known ordinal_Subq_SNoLe^{ordinal_Subq_SNoLe} : ∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ x0 ⊆ x1 ⟶ SNoLe x0 x1
Known Eps_i_ax^Eps_i_ax : ∀ x0 : ι → ο . ∀ x1 . x0 x1 ⟶ x0 (prim0 x0)
Known Empty_eq^Empty_eq : ∀ x0 . (∀ x1 . nIn x1 x0) ⟶ x0 = 0
Known finite_Empty^finite_Empty : finite 0
Known nat_ordsucc^nat_ordsucc : ∀ x0 . nat_p x0 ⟶ nat_p (ordsucc x0)
Known ordsuccI1^ordsuccI1 : ∀ x0 . x0 ⊆ ordsucc x0
Known infinite_remove1^{infinite_remove1} : ∀ x0 . infinite x0 ⟶ ∀ x1 . infinite (setminus x0 (Sing x1))
Known binunion_Subq_min^{binunion_Subq_min} : ∀ x0 x1 x2 . x0 ⊆ x2 ⟶ x1 ⊆ x2 ⟶ binunion x0 x1 ⊆ x2
Known setminus_Subq^{setminus_Subq} : ∀ x0 x1 . setminus x0 x1 ⊆ x0
Known SingE^SingE : ∀ x0 x1 . x1 ∈ Sing x0 ⟶ x1 = x0
Known e8bc0..^{equip_adjoin_ordsucc} : ∀ x0 x1 x2 . nIn x2 x1 ⟶ equip x0 x1 ⟶ equip (ordsucc x0) (binunion x1 (Sing x2))
Known setminusE2^setminusE2 : ∀ x0 x1 x2 . x2 ∈ setminus x0 x1 ⟶ nIn x2 x1
Definition or^or := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Known ordsuccE^ordsuccE : ∀ x0 x1 . x1 ∈ ordsucc x0 ⟶ or (x1 ∈ x0) (x1 = x0)
Known and3I^and3I : ∀ x0 x1 x2 : ο . x0 ⟶ x1 ⟶ x2 ⟶ and (and x0 x1) x2
Theorem infiniteRamsey^{infiniteRamsey} : ∀ x0 . nat_p x0 ⟶ ∀ x1 . nat_p x1 ⟶ ∀ x2 . infinite x2 ⟶ ∀ x3 : ι → ι . (∀ x4 . x4 ⊆ x2 ⟶ equip x4 x1 ⟶ x3 x4 ∈ x0) ⟶ ∀ x4 : ο . (∀ x5 . and (x5 ⊆ x2) (∀ x6 : ο . (∀ x7 . and (x7 ∈ x0) (and (infinite x5) (∀ x8 . x8 ⊆ x5 ⟶ equip x8 x1 ⟶ x3 x8 = x7)) ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4 (proof)