Proofgold Address

Definition False^False := ∀ x0 : ο . x0
Definition not^not := λ x0 : ο . x0 ⟶ False
Definition or^or := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Definition and^and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Definition Subq^Subq := λ x0 x1 . ∀ x2 . x2 ∈ x0 ⟶ x2 ∈ x1
Param atleastp^atleastp : ι → ι → ο
Definition TwoRamseyProp_atleastp := λ x0 x1 x2 . ∀ x3 : ι → ι → ο . (∀ x4 x5 . x3 x4 x5 ⟶ x3 x5 x4) ⟶ or (∀ x4 : ο . (∀ x5 . and (x5 ⊆ x2) (and (atleastp x0 x5) (∀ x6 . x6 ∈ x5 ⟶ ∀ x7 . x7 ∈ x5 ⟶ (x6 = x7 ⟶ ∀ x8 : ο . x8) ⟶ x3 x6 x7)) ⟶ x4) ⟶ x4) (∀ x4 : ο . (∀ x5 . and (x5 ⊆ x2) (and (atleastp x1 x5) (∀ x6 . x6 ∈ x5 ⟶ ∀ x7 . x7 ∈ x5 ⟶ (x6 = x7 ⟶ ∀ x8 : ο . x8) ⟶ not (x3 x6 x7))) ⟶ x4) ⟶ x4)
Param ordsucc^ordsucc : ι → ι
Known f03aa.. : ∀ x0 . atleastp 3 x0 ⟶ ∀ x1 : ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ (x2 = x3 ⟶ ∀ x5 : ο . x5) ⟶ (x2 = x4 ⟶ ∀ x5 : ο . x5) ⟶ (x3 = x4 ⟶ ∀ x5 : ο . x5) ⟶ x1) ⟶ x1
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)
Param inv^inv : ι → (ι → ι) → ι → ι
Param nat_p^nat_p : ι → ο
Known PigeonHole_nat^{PigeonHole_nat} : ∀ x0 . nat_p x0 ⟶ ∀ x1 : ι → ι . (∀ x2 . x2 ∈ ordsucc x0 ⟶ x1 x2 ∈ x0) ⟶ not (∀ x2 . x2 ∈ ordsucc x0 ⟶ ∀ x3 . x3 ∈ ordsucc x0 ⟶ x1 x2 = x1 x3 ⟶ x2 = x3)
Known nat_3^nat_3 : nat_p 3
Known surj_inv_inj^surj_inv_inj : ∀ x0 x1 . ∀ x2 : ι → ι . (∀ x3 . x3 ∈ x1 ⟶ ∀ x4 : ο . (∀ x5 . and (x5 ∈ x0) (x2 x5 = x3) ⟶ x4) ⟶ x4) ⟶ inj x1 x0 (inv x0 x2)
Param ap^ap : ι → ι → ι
Param lam^Sigma : ι → (ι → ι) → ι
Param If_i^If_i : ο → ι → ι → ι
Known dneg^dneg : ∀ x0 : ο . not (not x0) ⟶ x0
Known xm^xm : ∀ x0 : ο . or x0 (not x0)
Known prop_ext_2^prop_ext_2 : ∀ x0 x1 : ο . (x0 ⟶ x1) ⟶ (x1 ⟶ x0) ⟶ x0 = x1
Definition nIn^nIn := λ x0 x1 . not (x0 ∈ x1)
Known FalseE^FalseE : False ⟶ ∀ x0 : ο . x0
Known andI^andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Known In_2_3^In_2_3 : 2 ∈ 3
Known tuple_3_2_eq^tuple_3_2_eq : ∀ x0 x1 x2 . ap (lam 3 (λ x4 . If_i (x4 = 0) x0 (If_i (x4 = 1) x1 x2))) 2 = x2
Known In_1_3^In_1_3 : 1 ∈ 3
Known tuple_3_1_eq^tuple_3_1_eq : ∀ x0 x1 x2 . ap (lam 3 (λ x4 . If_i (x4 = 0) x0 (If_i (x4 = 1) x1 x2))) 1 = x1
Known In_0_3^In_0_3 : 0 ∈ 3
Known tuple_3_0_eq^tuple_3_0_eq : ∀ x0 x1 x2 . ap (lam 3 (λ x4 . If_i (x4 = 0) x0 (If_i (x4 = 1) x1 x2))) 0 = x0
Known In_0_4^In_0_4 : 0 ∈ 4
Param binunion^binunion : ι → ι → ι
Param Sep^Sep : ι → (ι → ο) → ι
Param setminus^setminus : ι → ι → ι
Param Sing^Sing : ι → ι
Param bij^bij : ι → ι → (ι → ι) → ο
Definition equip^equip := λ x0 x1 . ∀ x2 : ο . (∀ x3 : ι → ι . bij x0 x1 x3 ⟶ x2) ⟶ x2
Known a6047.. : ∀ x0 . x0 ⊆ prim4 3 ⟶ ∀ x1 . x1 ⊆ prim4 3 ⟶ (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x1 ⟶ ∀ x4 : ο . (∀ x5 . and (x5 ∈ 3) (∀ x6 : ο . (∀ x7 . and (x7 ∈ 3) (and (and (x5 = x7 ⟶ ∀ x8 : ο . x8) (x5 ∈ x2 = x5 ∈ x3)) (x7 ∈ x2 = x7 ∈ x3)) ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) ⟶ ∀ x2 : ο . (atleastp x0 1 ⟶ x2) ⟶ (atleastp x1 1 ⟶ x2) ⟶ (equip 2 x0 ⟶ equip 2 x1 ⟶ x2) ⟶ x2
Known 89205.. : ∀ x0 x1 . (∀ x2 . x2 ∈ x0 ⟶ nIn x2 x1) ⟶ atleastp 6 (binunion x0 x1) ⟶ atleastp x0 1 ⟶ atleastp x1 (prim4 2) ⟶ False
Known atleastp_tra^atleastp_tra : ∀ x0 x1 x2 . atleastp x0 x1 ⟶ atleastp x1 x2 ⟶ atleastp x0 x2
Known equip_atleastp^{equip_atleastp} : ∀ x0 x1 . equip x0 x1 ⟶ atleastp x0 x1
Known binunion_com^binunion_com : ∀ x0 x1 . binunion x0 x1 = binunion x1 x0
Known 4fb58..^{Pigeonhole_not_atleastp_ordsucc} : ∀ x0 . nat_p x0 ⟶ not (atleastp (ordsucc x0) x0)
Known nat_5^nat_5 : nat_p 5
Param setsum^setsum : ι → ι → ι
Known 385ef.. : ∀ x0 x1 x2 x3 . atleastp x0 x2 ⟶ atleastp x1 x3 ⟶ (∀ x4 . x4 ∈ x0 ⟶ nIn x4 x1) ⟶ atleastp (binunion x0 x1) (setsum x2 x3)
Known equip_sym^equip_sym : ∀ x0 x1 . equip x0 x1 ⟶ equip x1 x0
Known 5b991.. : equip 4 (setsum 2 2)
Known nat_In_atleastp : ∀ x0 . nat_p x0 ⟶ ∀ x1 . x1 ∈ x0 ⟶ atleastp x1 x0
Known In_4_5^In_4_5 : 4 ∈ 5
Known equip_tra^equip_tra : ∀ x0 x1 x2 . equip x0 x1 ⟶ equip x1 x2 ⟶ equip x0 x2
Known SepE^SepE : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . x2 ∈ Sep x0 x1 ⟶ and (x2 ∈ x0) (x1 x2)
Known ReplE_impred^ReplE_impred : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ prim5 x0 x1 ⟶ ∀ x3 : ο . (∀ x4 . x4 ∈ x0 ⟶ x2 = x1 x4 ⟶ x3) ⟶ x3
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
Known setminusI^setminusI : ∀ x0 x1 x2 . x2 ∈ x0 ⟶ nIn x2 x1 ⟶ x2 ∈ setminus x0 x1
Known In_irref^In_irref : ∀ x0 . nIn x0 x0
Known SingE^SingE : ∀ x0 x1 . x1 ∈ Sing x0 ⟶ x1 = x0
Known setminusE1^setminusE1 : ∀ x0 x1 x2 . x2 ∈ setminus x0 x1 ⟶ x2 ∈ x0
Known bijI^bijI : ∀ x0 x1 . ∀ x2 : ι → ι . (∀ 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) ⟶ bij x0 x1 x2
Known ReplI^ReplI : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ x0 ⟶ x1 x2 ∈ prim5 x0 x1
Known set_ext^set_ext : ∀ x0 x1 . x0 ⊆ x1 ⟶ x1 ⊆ x0 ⟶ x0 = x1
Known dfb49.. : ∀ x0 x1 . x1 ⊆ prim4 (ordsucc x0) ⟶ (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ ∀ x4 : ο . (∀ x5 . and (x5 ∈ ordsucc x0) (x5 ∈ x2 = x5 ∈ x3) ⟶ x4) ⟶ x4) ⟶ atleastp x1 (prim4 x0)
Known setminusE^setminusE : ∀ x0 x1 x2 . x2 ∈ setminus x0 x1 ⟶ and (x2 ∈ x0) (nIn x2 x1)
Known PowerI^PowerI : ∀ x0 x1 . x1 ⊆ x0 ⟶ x1 ∈ prim4 x0
Known SingI^SingI : ∀ x0 . x0 ∈ Sing x0
Known Sep_Subq^Sep_Subq : ∀ x0 . ∀ x1 : ι → ο . Sep x0 x1 ⊆ x0
Known binunionI2^binunionI2 : ∀ x0 x1 x2 . x2 ∈ x1 ⟶ x2 ∈ binunion x0 x1
Known SepI^SepI : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . x2 ∈ x0 ⟶ x1 x2 ⟶ x2 ∈ Sep x0 x1
Known binunionI1^binunionI1 : ∀ x0 x1 x2 . x2 ∈ x0 ⟶ x2 ∈ binunion x0 x1
Known binunion_Subq_min^{binunion_Subq_min} : ∀ x0 x1 x2 . x0 ⊆ x2 ⟶ x1 ⊆ x2 ⟶ binunion x0 x1 ⊆ x2
Known PowerE^PowerE : ∀ x0 x1 . x1 ∈ prim4 x0 ⟶ x1 ⊆ x0
Theorem not_TwoRamseyProp_atleast_3_6_Power_4 : not (TwoRamseyProp_atleastp 3 6 (prim4 4)) (proof)
Param TwoRamseyProp^{TwoRamseyProp} : ι → ι → ι → ο
Known TwoRamseyProp_atleastp_atleastp : ∀ x0 x1 x2 x3 x4 . TwoRamseyProp x0 x2 x4 ⟶ atleastp x1 x0 ⟶ atleastp x3 x2 ⟶ TwoRamseyProp_atleastp x1 x3 x4
Known atleastp_ref : ∀ x0 . atleastp x0 x0
Theorem 4618e..^{not_TwoRamseyProp_3_6_Power_4} : not (TwoRamseyProp 3 6 (prim4 4)) (proof)
Known nat_7^nat_7 : nat_p 7
Known In_6_7^In_6_7 : 6 ∈ 7
Theorem 1d99f..^{not_TwoRamseyProp_3_7_Power_4} : not (TwoRamseyProp 3 7 (prim4 4)) (proof)
Known nat_8^nat_8 : nat_p 8
Known In_6_8^In_6_8 : 6 ∈ 8
Theorem b6366..^{not_TwoRamseyProp_3_8_Power_4} : not (TwoRamseyProp 3 8 (prim4 4)) (proof)
Known nat_9^nat_9 : nat_p 9
Known In_6_9^In_6_9 : 6 ∈ 9
Theorem f990b..^{not_TwoRamseyProp_3_9_Power_4} : not (TwoRamseyProp 3 9 (prim4 4)) (proof)
Known nat_10^nat_10 : nat_p 10
Known 1beb5.. : 6 ∈ 10
Theorem a1e0f..^{not_TwoRamseyProp_3_10_Power_4} : not (TwoRamseyProp 3 10 (prim4 4)) (proof)
Known nat_4^nat_4 : nat_p 4
Known In_3_4^In_3_4 : 3 ∈ 4
Theorem f5ebc..^{not_TwoRamseyProp_4_6_Power_4} : not (TwoRamseyProp 4 6 (prim4 4)) (proof)
Theorem a1968..^{not_TwoRamseyProp_4_7_Power_4} : not (TwoRamseyProp 4 7 (prim4 4)) (proof)
Theorem fa29b..^{not_TwoRamseyProp_4_8_Power_4} : not (TwoRamseyProp 4 8 (prim4 4)) (proof)
Theorem 5914c..^{not_TwoRamseyProp_4_9_Power_4} : not (TwoRamseyProp 4 9 (prim4 4)) (proof)
Known In_3_5^In_3_5 : 3 ∈ 5
Theorem c0836..^{not_TwoRamseyProp_5_6_Power_4} : not (TwoRamseyProp 5 6 (prim4 4)) (proof)
Theorem c6b25..^{not_TwoRamseyProp_5_7_Power_4} : not (TwoRamseyProp 5 7 (prim4 4)) (proof)
Theorem f4df6..^{not_TwoRamseyProp_5_8_Power_4} : not (TwoRamseyProp 5 8 (prim4 4)) (proof)
Known nat_6^nat_6 : nat_p 6
Known In_3_6^In_3_6 : 3 ∈ 6
Theorem 3ce96..^{not_TwoRamseyProp_6_6_Power_4} : not (TwoRamseyProp 6 6 (prim4 4)) (proof)
Theorem c642e..^{not_TwoRamseyProp_6_7_Power_4} : not (TwoRamseyProp 6 7 (prim4 4)) (proof)