Proofgold Address

Definition Subq^Subq := λ x0 x1 . ∀ x2 . x2 ∈ x0 ⟶ x2 ∈ x1
Param ordsucc^ordsucc : ι → ι
Definition u1 := 1
Definition u2 := ordsucc u1
Definition u3 := ordsucc u2
Definition u4 := ordsucc u3
Definition u5 := ordsucc u4
Definition u6 := ordsucc u5
Definition u7 := ordsucc u6
Definition u8 := ordsucc u7
Param atleastp^atleastp : ι → ι → ο
Definition False^False := ∀ x0 : ο . x0
Definition not^not := λ x0 : ο . x0 ⟶ False
Param u22 : ι
Definition 94591.. := λ x0 x1 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . λ x2 x3 . x0 (x1 x2 x2 x2 x3 x3 x3 x3 x2 x3 x3 x2 x3 x3 x3 x3 x2 x3 x2 x3 x3 x3 x3) (x1 x2 x2 x3 x2 x3 x3 x2 x3 x3 x3 x3 x2 x2 x3 x3 x3 x3 x3 x3 x3 x3 x2) (x1 x2 x3 x2 x2 x3 x2 x3 x3 x2 x3 x3 x3 x3 x3 x2 x3 x3 x3 x3 x3 x3 x2) (x1 x3 x2 x2 x2 x2 x3 x3 x3 x3 x2 x3 x3 x3 x2 x3 x3 x3 x2 x3 x3 x3 x3) (x1 x3 x3 x3 x2 x2 x2 x2 x3 x3 x3 x2 x3 x3 x3 x3 x2 x3 x3 x2 x3 x3 x3) (x1 x3 x3 x2 x3 x2 x2 x3 x2 x3 x3 x3 x2 x2 x3 x3 x3 x3 x3 x3 x3 x2 x3) (x1 x3 x2 x3 x3 x2 x3 x2 x2 x2 x3 x3 x3 x3 x3 x2 x3 x3 x3 x3 x3 x2 x3) (x1 x2 x3 x3 x3 x3 x2 x2 x2 x3 x2 x3 x3 x3 x2 x3 x3 x3 x3 x2 x3 x3 x3) (x1 x3 x3 x2 x3 x3 x3 x2 x3 x2 x3 x3 x2 x2 x2 x3 x3 x3 x3 x2 x3 x3 x3) (x1 x3 x3 x3 x2 x3 x3 x3 x2 x3 x2 x2 x3 x2 x3 x3 x2 x3 x3 x3 x3 x2 x3) (x1 x2 x3 x3 x3 x2 x3 x3 x3 x3 x2 x2 x3 x3 x2 x2 x3 x3 x3 x3 x3 x3 x3) (x1 x3 x2 x3 x3 x3 x2 x3 x3 x2 x3 x3 x2 x3 x3 x2 x2 x3 x2 x3 x3 x3 x3) (x1 x3 x2 x3 x3 x3 x2 x3 x3 x2 x2 x3 x3 x2 x3 x3 x3 x2 x3 x3 x2 x3 x3) (x1 x3 x3 x3 x2 x3 x3 x3 x2 x2 x3 x2 x3 x3 x2 x3 x3 x2 x3 x3 x2 x3 x3) (x1 x3 x3 x2 x3 x3 x3 x2 x3 x3 x3 x2 x2 x3 x3 x2 x3 x2 x3 x3 x2 x3 x3) (x1 x2 x3 x3 x3 x2 x3 x3 x3 x3 x2 x3 x2 x3 x3 x3 x2 x2 x3 x3 x2 x3 x3) (x1 x3 x3 x3 x3 x3 x3 x3 x3 x3 x3 x3 x3 x2 x2 x2 x2 x2 x2 x3 x3 x3 x2) (x1 x2 x3 x3 x2 x3 x3 x3 x3 x3 x3 x3 x2 x3 x3 x3 x3 x2 x2 x2 x3 x2 x3) (x1 x3 x3 x3 x3 x2 x3 x3 x2 x2 x3 x3 x3 x3 x3 x3 x3 x3 x2 x2 x2 x3 x2) (x1 x3 x3 x3 x3 x3 x3 x3 x3 x3 x3 x3 x3 x2 x2 x2 x2 x3 x3 x2 x2 x2 x3) (x1 x3 x3 x3 x3 x3 x2 x2 x3 x3 x2 x3 x3 x3 x3 x3 x3 x3 x2 x3 x2 x2 x2) (x1 x3 x2 x2 x3 x3 x3 x3 x3 x3 x3 x3 x3 x3 x3 x3 x3 x2 x3 x2 x3 x2 x2)
Param 55574.. : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι
Definition 0aea9.. := λ x0 x1 . x0 ∈ u22 ⟶ x1 ∈ u22 ⟶ 94591.. (55574.. x0) (55574.. x1) = λ x3 x4 . x3
Definition and^and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Param TwoRamseyGraph_3_6_17 : ι → ι → ο
Known 1e4e8.. : ∀ x0 . x0 ⊆ u8 ⟶ atleastp u3 x0 ⟶ (∀ x1 . x1 ∈ x0 ⟶ ∀ x2 . x2 ∈ x0 ⟶ (x1 = x2 ⟶ ∀ x3 : ο . x3) ⟶ not (TwoRamseyGraph_3_6_17 x1 x2)) ⟶ ∀ x1 : ο . (∀ x2 . and (x2 ∈ x0) (x2 ∈ u4) ⟶ x1) ⟶ x1
Param u17 : ι
Known a0edc.. : ∀ x0 . x0 ∈ u17 ⟶ ∀ x1 . x1 ∈ u17 ⟶ TwoRamseyGraph_3_6_17 x0 x1 ⟶ 0aea9.. x0 x1
Known 078d9.. : u8 ⊆ u17
Theorem 2e7e5.. : ∀ x0 . x0 ⊆ u8 ⟶ atleastp u3 x0 ⟶ (∀ x1 . x1 ∈ x0 ⟶ ∀ x2 . x2 ∈ x0 ⟶ (x1 = x2 ⟶ ∀ x3 : ο . x3) ⟶ not (0aea9.. x1 x2)) ⟶ ∀ x1 : ο . (∀ x2 . and (x2 ∈ x0) (x2 ∈ u4) ⟶ x1) ⟶ x1 (proof)
Definition u9 := ordsucc u8
Definition u10 := ordsucc u9
Definition u11 := ordsucc u10
Param u19 : ι
Param u21 : ι
Param ordinal^ordinal : ι → ο
Param nat_p^nat_p : ι → ο
Param equip^equip : ι → ι → ο
Known 2ec5a.. : ∀ x0 . nat_p x0 ⟶ ∀ x1 . atleastp (ordsucc x0) x1 ⟶ (∀ x2 . x2 ∈ x1 ⟶ ordinal x2) ⟶ ∀ x2 : ο . (∀ x3 x4 . equip x0 x3 ⟶ x4 ∈ x1 ⟶ x3 ⊆ x1 ⟶ x3 ⊆ x4 ⟶ x2) ⟶ x2
Known nat_3^nat_3 : nat_p 3
Param binunion^binunion : ι → ι → ι
Param Sing^Sing : ι → ι
Definition nSubq^nSubq := λ x0 x1 . not (x0 ⊆ x1)
Known be1cd.. : ∀ x0 . nat_p x0 ⟶ ∀ x1 . equip (ordsucc x0) x1 ⟶ (∀ x2 . x2 ∈ x1 ⟶ ordinal x2) ⟶ ∀ x2 : ο . (∀ x3 x4 . equip x0 x3 ⟶ x4 ∈ x1 ⟶ x3 ⊆ x1 ⟶ x3 ⊆ x4 ⟶ x1 = binunion x3 (Sing x4) ⟶ x2) ⟶ x2
Known nat_2^nat_2 : nat_p 2
Definition nIn^nIn := λ x0 x1 . not (x0 ∈ x1)
Param setminus^setminus : ι → ι → ι
Known 090fa.. : ∀ x0 . x0 ∈ setminus u11 u6 ⟶ ∀ x1 : ι → ο . x1 u6 ⟶ x1 u7 ⟶ x1 u8 ⟶ x1 u9 ⟶ x1 u10 ⟶ x1 x0
Known setminusI^setminusI : ∀ x0 x1 x2 . x2 ∈ x0 ⟶ nIn x2 x1 ⟶ x2 ∈ setminus x0 x1
Known 620a1.. : ∀ x0 . x0 ⊆ u6 ⟶ atleastp u4 x0 ⟶ not (∀ x1 . x1 ∈ x0 ⟶ ∀ x2 . x2 ∈ x0 ⟶ (x1 = x2 ⟶ ∀ x3 : ο . x3) ⟶ not (0aea9.. x1 x2))
Definition or^or := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Known binunionE^binunionE : ∀ x0 x1 x2 . x2 ∈ binunion x0 x1 ⟶ or (x2 ∈ x0) (x2 ∈ x1)
Known nat_trans^nat_trans : ∀ x0 . nat_p x0 ⟶ ∀ x1 . x1 ∈ x0 ⟶ x1 ⊆ x0
Known nat_6^nat_6 : nat_p 6
Known SingE^SingE : ∀ x0 x1 . x1 ∈ Sing x0 ⟶ x1 = x0
Known equip_atleastp^{equip_atleastp} : ∀ x0 x1 . equip x0 x1 ⟶ atleastp x0 x1
Param setsum^setsum : ι → ι → ι
Known equip_tra^equip_tra : ∀ x0 x1 x2 . equip x0 x1 ⟶ equip x1 x2 ⟶ equip x0 x2
Param add_nat^add_nat : ι → ι → ι
Known 480b2.. : add_nat u3 u1 = u4
Known c88e0.. : ∀ x0 x1 x2 x3 . nat_p x0 ⟶ nat_p x1 ⟶ equip x0 x2 ⟶ equip x1 x3 ⟶ equip (add_nat x0 x1) (setsum x2 x3)
Known nat_1^nat_1 : nat_p 1
Known equip_sym^equip_sym : ∀ x0 x1 . equip x0 x1 ⟶ equip x1 x0
Known 5169f..^equip_Sing_1 : ∀ x0 . equip (Sing x0) u1
Known d778e.. : ∀ x0 x1 x2 x3 . equip x0 x2 ⟶ equip x1 x3 ⟶ (∀ x4 . x4 ∈ x0 ⟶ nIn x4 x1) ⟶ equip (binunion x0 x1) (setsum x2 x3)
Known equip_ref^equip_ref : ∀ x0 . equip x0 x0
Known In_irref^In_irref : ∀ x0 . nIn x0 x0
Known Subq_tra^Subq_tra : ∀ x0 x1 x2 . x0 ⊆ x1 ⟶ x1 ⊆ x2 ⟶ x0 ⊆ x2
Known bd770.. : u6 ⊆ u8
Known 021ac.. : u7 ⊆ u8
Known ordsuccE^ordsuccE : ∀ x0 x1 . x1 ∈ ordsucc x0 ⟶ or (x1 ∈ x0) (x1 = x0)
Known a2937.. : ∀ x0 . x0 ⊆ u8 ⟶ atleastp u2 x0 ⟶ (∀ x1 . x1 ∈ x0 ⟶ not (TwoRamseyGraph_3_6_17 x1 u8)) ⟶ (∀ x1 . x1 ∈ x0 ⟶ not (TwoRamseyGraph_3_6_17 x1 u9)) ⟶ (∀ x1 . x1 ∈ x0 ⟶ ∀ x2 . x2 ∈ x0 ⟶ (x1 = x2 ⟶ ∀ x3 : ο . x3) ⟶ not (TwoRamseyGraph_3_6_17 x1 x2)) ⟶ ∀ x1 : ο . (∀ x2 . and (x2 ∈ x0) (x2 ∈ u4) ⟶ x1) ⟶ x1
Known b4ae4.. : u11 ⊆ u17
Known c0db6.. : ∀ x0 . x0 ⊆ u8 ⟶ atleastp u2 x0 ⟶ (∀ x1 . x1 ∈ x0 ⟶ not (TwoRamseyGraph_3_6_17 x1 u8)) ⟶ (∀ x1 . x1 ∈ x0 ⟶ not (TwoRamseyGraph_3_6_17 x1 u10)) ⟶ (∀ x1 . x1 ∈ x0 ⟶ ∀ x2 . x2 ∈ x0 ⟶ (x1 = x2 ⟶ ∀ x3 : ο . x3) ⟶ not (TwoRamseyGraph_3_6_17 x1 x2)) ⟶ ∀ x1 : ο . (∀ x2 . and (x2 ∈ x0) (x2 ∈ u4) ⟶ x1) ⟶ x1
Known 896c4.. : 55574.. u9 = λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 . x10
Known 89d98.. : 55574.. u10 = λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 . x11
Known cases_4^cases_4 : ∀ x0 . x0 ∈ u4 ⟶ ∀ x1 : ι → ο . x1 0 ⟶ x1 u1 ⟶ x1 u2 ⟶ x1 u3 ⟶ x1 x0
Known 7410a.. : 55574.. 0 = λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 . x1
Known e86b0.. : 55574.. u17 = λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 . x18
Known aafc6.. : 55574.. u1 = λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 . x2
Known 667cd.. : 55574.. u21 = λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 . x22
Known fa851.. : 55574.. u2 = λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 . x3
Known 9379b.. : 55574.. u3 = λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 . x4
Known binunion_Subq_min^{binunion_Subq_min} : ∀ x0 x1 x2 . x0 ⊆ x2 ⟶ x1 ⊆ x2 ⟶ binunion x0 x1 ⊆ x2
Known nat_8^nat_8 : nat_p 8
Known nat_p_ordinal^{nat_p_ordinal} : ∀ x0 . nat_p x0 ⟶ ordinal x0
Known nat_p_trans^nat_p_trans : ∀ x0 . nat_p x0 ⟶ ∀ x1 . x1 ∈ x0 ⟶ nat_p x1
Known nat_11^nat_11 : nat_p u11
Theorem d2f0d.. : ∀ x0 . x0 ⊆ u11 ⟶ atleastp u4 x0 ⟶ (∀ x1 . x1 ∈ x0 ⟶ not (0aea9.. x1 u17)) ⟶ (∀ x1 . x1 ∈ x0 ⟶ not (0aea9.. x1 u19)) ⟶ (∀ x1 . x1 ∈ x0 ⟶ not (0aea9.. x1 u21)) ⟶ not (∀ x1 . x1 ∈ x0 ⟶ ∀ x2 . x2 ∈ x0 ⟶ (x1 = x2 ⟶ ∀ x3 : ο . x3) ⟶ not (0aea9.. x1 x2)) (proof)
Param u18 : ι
Known nat_4^nat_4 : nat_p 4
Known 86c65.. : nat_p u18
Param u12 : ι
Param u13 : ι
Param u14 : ι
Param u15 : ι
Param u16 : ι
Known 7618f.. : ∀ x0 . x0 ∈ setminus u18 u12 ⟶ ∀ x1 : ι → ο . x1 u12 ⟶ x1 u13 ⟶ x1 u14 ⟶ x1 u15 ⟶ x1 u16 ⟶ x1 u17 ⟶ x1 x0
Known 9cadc.. : ∀ x0 . x0 ⊆ u12 ⟶ atleastp u5 x0 ⟶ not (∀ x1 . x1 ∈ x0 ⟶ ∀ x2 . x2 ∈ x0 ⟶ (x1 = x2 ⟶ ∀ x3 : ο . x3) ⟶ not (TwoRamseyGraph_3_6_17 x1 x2))
Known 893fe.. : add_nat u4 u1 = u5
Known 2d2af.. : u12 ⊆ u17
Known nat_12^nat_12 : nat_p u12
Known 2ab0d.. : 55574.. u12 = λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 . x13
Known 1435b.. : 55574.. u19 = λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 . x20
Known 0b155.. : 55574.. u13 = λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 . x14
Known 38fc2.. : 55574.. u14 = λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 . x15
Known 134b9.. : 55574.. u15 = λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 . x16
Known b8157.. : 55574.. u16 = λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 . x17
Known 66f20.. : ∀ x0 . x0 ∈ u17 ⟶ ∀ x1 : ι → ο . x1 0 ⟶ x1 u1 ⟶ x1 u2 ⟶ x1 u3 ⟶ x1 u4 ⟶ x1 u5 ⟶ x1 u6 ⟶ x1 u7 ⟶ x1 u8 ⟶ x1 u9 ⟶ x1 u10 ⟶ x1 u11 ⟶ x1 u12 ⟶ x1 u13 ⟶ x1 u14 ⟶ x1 u15 ⟶ x1 u16 ⟶ x1 x0
Known Subq_ref^Subq_ref : ∀ x0 . x0 ⊆ x0
Known 3ed90.. : 0 ∈ 11
Known c92a5.. : 1 ∈ 11
Known f5815.. : 2 ∈ 11
Known 157cb.. : 3 ∈ 11
Known 52414.. : 4 ∈ 11
Known 4f9f7.. : 5 ∈ 11
Known db527.. : 6 ∈ 11
Known 45b9a.. : 7 ∈ 11
Known 15f81.. : 8 ∈ 11
Known 2c8c5.. : 9 ∈ 11
Known 9be62.. : 10 ∈ 11
Known FalseE^FalseE : False ⟶ ∀ x0 : ο . x0
Known 76683.. : 55574.. u11 = λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 . x12
Theorem 82d29.. : ∀ x0 . x0 ⊆ u18 ⟶ atleastp u5 x0 ⟶ (∀ x1 . x1 ∈ x0 ⟶ not (0aea9.. x1 u19)) ⟶ (∀ x1 . x1 ∈ x0 ⟶ not (0aea9.. x1 u21)) ⟶ not (∀ x1 . x1 ∈ x0 ⟶ ∀ x2 . x2 ∈ x0 ⟶ (x1 = x2 ⟶ ∀ x3 : ο . x3) ⟶ not (0aea9.. x1 x2)) (proof)