Proofgold Address

Param atleastp^atleastp : ι → ι → ο
Param equip^equip : ι → ι → ο
Known 2c48a..^{atleastp_antisym_equip} : ∀ x0 x1 . atleastp x0 x1 ⟶ atleastp x1 x0 ⟶ equip x0 x1
Param add_nat^add_nat : ι → ι → ι
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
Param nat_p^nat_p : ι → ο
Known add_nat_SR^add_nat_SR : ∀ x0 x1 . nat_p x1 ⟶ add_nat x0 (ordsucc x1) = ordsucc (add_nat x0 x1)
Known nat_2^nat_2 : nat_p 2
Known nat_1^nat_1 : nat_p 1
Known nat_0^nat_0 : nat_p 0
Known add_nat_0R^add_nat_0R : ∀ x0 . add_nat x0 0 = x0
Theorem 008c0.. : add_nat u3 u3 = u6 (proof)
Definition False^False := ∀ x0 : ο . x0
Definition not^not := λ x0 : ο . x0 ⟶ False
Definition nIn^nIn := λ x0 x1 . not (x0 ∈ x1)
Param setsum^setsum : ι → ι → ι
Param binunion^binunion : ι → ι → ι
Known 1fe14.. : ∀ x0 x1 x2 x3 . atleastp x0 x2 ⟶ atleastp x1 x3 ⟶ (∀ x4 . x4 ∈ x2 ⟶ nIn x4 x3) ⟶ atleastp (setsum x0 x1) (binunion x2 x3)
Param setminus^setminus : ι → ι → ι
Definition Subq^Subq := λ x0 x1 . ∀ x2 . x2 ∈ x0 ⟶ x2 ∈ x1
Known set_ext^set_ext : ∀ x0 x1 . x0 ⊆ x1 ⟶ x1 ⊆ x0 ⟶ x0 = x1
Definition or^or := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Known xm^xm : ∀ x0 : ο . or x0 (not x0)
Known binunionI1^binunionI1 : ∀ x0 x1 x2 . x2 ∈ x0 ⟶ x2 ∈ binunion x0 x1
Known binunionE^binunionE : ∀ x0 x1 x2 . x2 ∈ binunion x0 x1 ⟶ or (x2 ∈ x0) (x2 ∈ x1)
Known FalseE^FalseE : False ⟶ ∀ x0 : ο . x0
Known binunionI2^binunionI2 : ∀ x0 x1 x2 . x2 ∈ x1 ⟶ x2 ∈ binunion x0 x1
Known setminusI^setminusI : ∀ x0 x1 x2 . x2 ∈ x0 ⟶ nIn x2 x1 ⟶ x2 ∈ setminus x0 x1
Known setminusE1^setminusE1 : ∀ x0 x1 x2 . x2 ∈ setminus x0 x1 ⟶ x2 ∈ x0
Theorem 16482.. : ∀ x0 x1 . binunion x0 x1 = binunion x0 (setminus x1 x0) (proof)
Param binintersect^binintersect : ι → ι → ι
Definition u7 := ordsucc u6
Known atleastp_tra^atleastp_tra : ∀ x0 x1 x2 . atleastp x0 x1 ⟶ atleastp x1 x2 ⟶ atleastp x0 x2
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 48e0f.. : ∀ x0 . nat_p x0 ⟶ ∀ x1 . or (atleastp x1 x0) (atleastp (ordsucc x0) x1)
Known 4fb58..^{Pigeonhole_not_atleastp_ordsucc} : ∀ x0 . nat_p x0 ⟶ not (atleastp (ordsucc x0) x0)
Known nat_5^nat_5 : nat_p 5
Known equip_atleastp^{equip_atleastp} : ∀ x0 x1 . equip x0 x1 ⟶ atleastp x0 x1
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_3^nat_3 : nat_p 3
Known equip_ref^equip_ref : ∀ x0 . equip x0 x0
Known setminusE2^setminusE2 : ∀ x0 x1 x2 . x2 ∈ setminus x0 x1 ⟶ nIn x2 x1
Known binintersectE1^{binintersectE1} : ∀ x0 x1 x2 . x2 ∈ binintersect x0 x1 ⟶ x2 ∈ x0
Known binunion_com^binunion_com : ∀ x0 x1 . binunion x0 x1 = binunion x1 x0
Known binintersect_com^{binintersect_com} : ∀ x0 x1 . binintersect x0 x1 = binintersect x1 x0
Known a8a92.. : ∀ x0 x1 . x0 = binunion (setminus x0 x1) (binintersect x0 x1)
Known equip_sym^equip_sym : ∀ x0 x1 . equip x0 x1 ⟶ equip x1 x0
Known bd216.. : add_nat u5 u2 = u7
Theorem 0831e.. : ∀ x0 x1 . atleastp u3 (binintersect x0 x1) ⟶ atleastp x0 u5 ⟶ atleastp x1 u5 ⟶ atleastp (binunion x0 x1) u7 (proof)
Definition u8 := ordsucc u7
Definition u9 := ordsucc u8
Theorem 63ef9.. : add_nat u7 u2 = u9 (proof)
Definition u10 := ordsucc u9
Definition u11 := ordsucc u10
Definition u12 := ordsucc u11
Definition u13 := ordsucc u12
Definition u14 := ordsucc u13
Definition u15 := ordsucc u14
Definition u16 := ordsucc u15
Definition u17 := ordsucc u16
Known nat_7^nat_7 : nat_p 7
Known nat_6^nat_6 : nat_p 6
Known nat_4^nat_4 : nat_p 4
Theorem 442f5.. : add_nat u9 u8 = u17 (proof)
Param Sing^Sing : ι → ι
Known 7f437.. : ∀ x0 x1 x2 . x2 ∈ x0 ⟶ atleastp x0 (ordsucc x1) ⟶ atleastp (setminus x0 (Sing x2)) x1
Param Sep^Sep : ι → (ι → ο) → ι
Definition and^and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Definition DirGraphOutNeighbors := λ x0 . λ x1 : ι → ι → ο . λ x2 . {x3 ∈ x0|and (x2 = x3 ⟶ ∀ x4 : ο . x4) (x1 x2 x3)}
Known 7fc90.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 x3 . x1 x2 x3 ⟶ x1 x3 x2) ⟶ (∀ x2 . x2 ⊆ x0 ⟶ atleastp u3 x2 ⟶ not (∀ x3 . x3 ∈ x2 ⟶ ∀ x4 . x4 ∈ x2 ⟶ (x3 = x4 ⟶ ∀ x5 : ο . x5) ⟶ x1 x3 x4)) ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ DirGraphOutNeighbors x0 x1 x2 ⟶ ∀ x4 . x4 ∈ DirGraphOutNeighbors x0 x1 x2 ⟶ (x3 = x4 ⟶ ∀ x5 : ο . x5) ⟶ not (x1 x3 x4)
Definition u18 := ordsucc u17
Known b4538.. : ∀ x0 : ι → ι → ο . (∀ x1 x2 . x0 x1 x2 ⟶ x0 x2 x1) ⟶ (∀ x1 . x1 ⊆ u18 ⟶ atleastp u3 x1 ⟶ not (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ x0 x2 x3)) ⟶ (∀ x1 . x1 ⊆ u18 ⟶ atleastp u6 x1 ⟶ not (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ not (x0 x2 x3))) ⟶ ∀ x1 . x1 ∈ u18 ⟶ equip (DirGraphOutNeighbors u18 x0 x1) u5
Known dneg^dneg : ∀ x0 : ο . not (not x0) ⟶ x0
Known binunion_Subq_min^{binunion_Subq_min} : ∀ x0 x1 x2 . x0 ⊆ x2 ⟶ x1 ⊆ x2 ⟶ binunion x0 x1 ⊆ x2
Known Sep_Subq^Sep_Subq : ∀ x0 . ∀ x1 : ι → ο . Sep x0 x1 ⊆ x0
Known SingE^SingE : ∀ x0 x1 . x1 ∈ Sing x0 ⟶ x1 = x0
Known 561b1.. : add_nat u5 u1 = u6
Known 04353.. : ∀ x0 x1 . x1 ∈ x0 ⟶ atleastp u1 x0
Known SingI^SingI : ∀ x0 . x0 ∈ Sing x0
Known binintersectI^{binintersectI} : ∀ x0 x1 x2 . x2 ∈ x0 ⟶ x2 ∈ x1 ⟶ x2 ∈ binintersect x0 x1
Known SepI^SepI : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . x2 ∈ x0 ⟶ x1 x2 ⟶ x2 ∈ Sep x0 x1
Known SepE1^SepE1 : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . x2 ∈ Sep x0 x1 ⟶ x2 ∈ x0
Known andI^andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Known neq_i_sym^neq_i_sym : ∀ x0 x1 . (x0 = x1 ⟶ ∀ x2 : ο . x2) ⟶ x1 = x0 ⟶ ∀ x2 : ο . x2
Known SepE2^SepE2 : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . x2 ∈ Sep x0 x1 ⟶ x1 x2
Theorem 52ae1.. : ∀ x0 : ι → ι → ο . (∀ x1 x2 . x0 x1 x2 ⟶ x0 x2 x1) ⟶ (∀ x1 . x1 ⊆ u18 ⟶ atleastp u3 x1 ⟶ not (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ x0 x2 x3)) ⟶ (∀ x1 . x1 ⊆ u18 ⟶ atleastp u6 x1 ⟶ not (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ not (x0 x2 x3))) ⟶ ∀ x1 . x1 ∈ u18 ⟶ ∀ x2 . x2 ∈ u18 ⟶ (x1 = x2 ⟶ ∀ x3 : ο . x3) ⟶ not (x0 x1 x2) ⟶ atleastp u1 (binintersect (DirGraphOutNeighbors u18 x0 x1) (DirGraphOutNeighbors u18 x0 x2)) (proof)
Param UPair^UPair : ι → ι → ι
Definition TwoRamseyProp^{TwoRamseyProp} := λ x0 x1 x2 . ∀ x3 : ι → ι → ο . (∀ x4 x5 . x3 x4 x5 ⟶ x3 x5 x4) ⟶ or (∀ x4 : ο . (∀ x5 . and (x5 ⊆ x2) (and (equip x0 x5) (∀ x6 . x6 ∈ x5 ⟶ ∀ x7 . x7 ∈ x5 ⟶ (x6 = x7 ⟶ ∀ x8 : ο . x8) ⟶ x3 x6 x7)) ⟶ x4) ⟶ x4) (∀ x4 : ο . (∀ x5 . and (x5 ⊆ x2) (and (equip x1 x5) (∀ x6 . x6 ∈ x5 ⟶ ∀ x7 . x7 ∈ x5 ⟶ (x6 = x7 ⟶ ∀ x8 : ο . x8) ⟶ not (x3 x6 x7))) ⟶ x4) ⟶ x4)
Known Subq_tra^Subq_tra : ∀ x0 x1 x2 . x0 ⊆ x1 ⟶ x1 ⊆ x2 ⟶ x0 ⊆ x2
Known setminus_Subq^{setminus_Subq} : ∀ x0 x1 . setminus x0 x1 ⊆ x0
Known f3bb6.. : add_nat 4 2 = 6
Known ada03.. : ∀ x0 x1 . x1 ∈ x0 ⟶ ∀ x2 . x2 ∈ x0 ⟶ (x1 = x2 ⟶ ∀ x3 : ο . x3) ⟶ atleastp u2 x0
Known UPairI1^UPairI1 : ∀ x0 x1 . x0 ∈ UPair x0 x1
Known UPairI2^UPairI2 : ∀ x0 x1 . x1 ∈ UPair x0 x1
Known setminusE^setminusE : ∀ x0 x1 x2 . x2 ∈ setminus x0 x1 ⟶ and (x2 ∈ x0) (nIn x2 x1)
Known UPairE^UPairE : ∀ x0 x1 x2 . x0 ∈ UPair x1 x2 ⟶ or (x0 = x1) (x0 = x2)
Known 46dcf.. : ∀ x0 x1 x2 x3 . atleastp x2 x3 ⟶ TwoRamseyProp x0 x1 x2 ⟶ TwoRamseyProp x0 x1 x3
Known TwoRamseyProp_3_4_9^{TwoRamseyProp_3_4_9} : TwoRamseyProp 3 4 9
Known nat_8^nat_8 : nat_p 8
Known nat_17^nat_17 : nat_p 17
Known 80238.. : ∀ x0 x1 . x0 ⊆ x1 ⟶ x1 = binunion x0 (setminus x1 x0)
Known c558f.. : ∀ x0 x1 x2 x3 . atleastp x0 x2 ⟶ atleastp x1 x3 ⟶ atleastp (binunion x0 x1) (setsum x2 x3)
Known nat_9^nat_9 : nat_p 9
Known b3e89.. : ∀ x0 x1 . atleastp (UPair x0 x1) u2
Theorem 2b310.. : ∀ x0 : ι → ι → ο . (∀ x1 x2 . x0 x1 x2 ⟶ x0 x2 x1) ⟶ (∀ x1 . x1 ⊆ u18 ⟶ atleastp u3 x1 ⟶ not (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ x0 x2 x3)) ⟶ (∀ x1 . x1 ⊆ u18 ⟶ atleastp u6 x1 ⟶ not (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ not (x0 x2 x3))) ⟶ ∀ x1 . x1 ∈ u18 ⟶ ∀ x2 . x2 ∈ u18 ⟶ (x1 = x2 ⟶ ∀ x3 : ο . x3) ⟶ not (x0 x1 x2) ⟶ atleastp (binintersect (DirGraphOutNeighbors u18 x0 x1) (DirGraphOutNeighbors u18 x0 x2)) u2 (proof)
Known orIL^orIL : ∀ x0 x1 : ο . x0 ⟶ or x0 x1
Known orIR^orIR : ∀ x0 x1 : ο . x1 ⟶ or x0 x1
Theorem 86f86.. : ∀ x0 : ι → ι → ο . (∀ x1 x2 . x0 x1 x2 ⟶ x0 x2 x1) ⟶ (∀ x1 . x1 ⊆ u18 ⟶ atleastp u3 x1 ⟶ not (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ x0 x2 x3)) ⟶ (∀ x1 . x1 ⊆ u18 ⟶ atleastp u6 x1 ⟶ not (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ not (x0 x2 x3))) ⟶ ∀ x1 . x1 ∈ u18 ⟶ ∀ x2 . x2 ∈ u18 ⟶ (x1 = x2 ⟶ ∀ x3 : ο . x3) ⟶ not (x0 x1 x2) ⟶ or (equip (binintersect (DirGraphOutNeighbors u18 x0 x1) (DirGraphOutNeighbors u18 x0 x2)) u1) (equip (binintersect (DirGraphOutNeighbors u18 x0 x1) (DirGraphOutNeighbors u18 x0 x2)) u2) (proof)