Proofgold Address

Definition Church17_lt8 := λ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . ∀ x1 : (ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι) → ο . x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x2) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x3) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x4) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x5) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x6) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x7) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x8) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x9) ⟶ x1 x0
Definition TwoRamseyGraph_3_6_Church17 := λ x0 x1 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . λ x2 x3 . x0 (x1 x2 x2 x2 x3 x3 x3 x3 x2 x3 x3 x2 x3 x3 x3 x3 x2 x3) (x1 x2 x2 x3 x2 x3 x3 x2 x3 x3 x3 x3 x2 x2 x3 x3 x3 x3) (x1 x2 x3 x2 x2 x3 x2 x3 x3 x2 x3 x3 x3 x3 x3 x2 x3 x3) (x1 x3 x2 x2 x2 x2 x3 x3 x3 x3 x2 x3 x3 x3 x2 x3 x3 x3) (x1 x3 x3 x3 x2 x2 x2 x2 x3 x3 x3 x2 x3 x3 x3 x3 x2 x3) (x1 x3 x3 x2 x3 x2 x2 x3 x2 x3 x3 x3 x2 x2 x3 x3 x3 x3) (x1 x3 x2 x3 x3 x2 x3 x2 x2 x2 x3 x3 x3 x3 x3 x2 x3 x3) (x1 x2 x3 x3 x3 x3 x2 x2 x2 x3 x2 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) (x1 x3 x3 x3 x2 x3 x3 x3 x2 x3 x2 x2 x3 x2 x3 x3 x2 x3) (x1 x2 x3 x3 x3 x2 x3 x3 x3 x3 x2 x2 x3 x3 x2 x2 x3 x3) (x1 x3 x2 x3 x3 x3 x2 x3 x3 x2 x3 x3 x2 x3 x3 x2 x2 x3) (x1 x3 x2 x3 x3 x3 x2 x3 x3 x2 x2 x3 x3 x2 x3 x3 x3 x2) (x1 x3 x3 x3 x2 x3 x3 x3 x2 x2 x3 x2 x3 x3 x2 x3 x3 x2) (x1 x3 x3 x2 x3 x3 x3 x2 x3 x3 x3 x2 x2 x3 x3 x2 x3 x2) (x1 x2 x3 x3 x3 x2 x3 x3 x3 x3 x2 x3 x2 x3 x3 x3 x2 x2) (x1 x3 x3 x3 x3 x3 x3 x3 x3 x3 x3 x3 x3 x2 x2 x2 x2 x2)
Param 84660.. : (ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι) → ο
Definition False^False := ∀ x0 : ο . x0
Known FalseE^FalseE : False ⟶ ∀ x0 : ο . x0
Known 768c1.. : ((λ x1 x2 . x2) = λ x1 x2 . x1) ⟶ ∀ x0 : ο . x0
Known 89411.. : 84660.. (λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x1)
Known 3a574.. : 84660.. (λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x3)
Theorem 14b16.. : ∀ x0 x1 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_lt8 x0 ⟶ Church17_lt8 x1 ⟶ (TwoRamseyGraph_3_6_Church17 x0 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x11) = λ x3 x4 . x4) ⟶ (TwoRamseyGraph_3_6_Church17 x0 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x18) = λ x3 x4 . x4) ⟶ (TwoRamseyGraph_3_6_Church17 x1 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x11) = λ x3 x4 . x4) ⟶ (TwoRamseyGraph_3_6_Church17 x1 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x18) = λ x3 x4 . x4) ⟶ (TwoRamseyGraph_3_6_Church17 x0 x1 = λ x3 x4 . x4) ⟶ ∀ x2 : ο . (84660.. x0 ⟶ x2) ⟶ (84660.. x1 ⟶ x2) ⟶ x2 (proof)
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 not^not := λ x0 : ο . x0 ⟶ False
Param TwoRamseyGraph_3_6_17 : ι → ι → ο
Param u15 : ι
Definition and^and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Known e8716.. : ∀ x0 . atleastp u2 x0 ⟶ ∀ x1 : ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ x1) ⟶ x1
Param Church17_p : (ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι) → ο
Param u17_to_Church17 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι
Param u16 : ι
Definition u17 := ordsucc u16
Known 67bc1.. : ∀ x0 . x0 ∈ u8 ⟶ Church17_lt8 (u17_to_Church17 x0)
Definition or^or := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Known d8d63.. : ∀ x0 x1 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x0 ⟶ Church17_p x1 ⟶ or (TwoRamseyGraph_3_6_Church17 x0 x1 = λ x3 x4 . x3) (TwoRamseyGraph_3_6_Church17 x0 x1 = λ x3 x4 . x4)
Known e7def.. : Church17_p (λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x8)
Known d0d1e.. : ∀ x0 . x0 ∈ u17 ⟶ ∀ x1 . x1 ∈ u17 ⟶ (TwoRamseyGraph_3_6_Church17 (u17_to_Church17 x0) (u17_to_Church17 x1) = λ x3 x4 . x3) ⟶ TwoRamseyGraph_3_6_17 x0 x1
Known 6a4e9.. : u8 ∈ u17
Known 48ba7.. : u17_to_Church17 u8 = λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 . x9
Known 7e8b2.. : Church17_p (λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x15)
Known 31b8d.. : u15 ∈ u17
Known c424d.. : u17_to_Church17 u15 = λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 . x16
Known andI^andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Known b4098.. : ∀ x0 . x0 ∈ u17 ⟶ 84660.. (u17_to_Church17 x0) ⟶ x0 ∈ u4
Known 078d9.. : u8 ⊆ u17
Known 27a8a.. : ∀ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_lt8 x0 ⟶ Church17_p x0
Theorem bc8bd.. : ∀ 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 u15)) ⟶ (∀ 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 (proof)
Known f1b43.. : 84660.. (λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x2)
Theorem 13c46.. : ∀ x0 x1 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_lt8 x0 ⟶ Church17_lt8 x1 ⟶ (TwoRamseyGraph_3_6_Church17 x0 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x13) = λ x3 x4 . x4) ⟶ (TwoRamseyGraph_3_6_Church17 x0 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x15) = λ x3 x4 . x4) ⟶ (TwoRamseyGraph_3_6_Church17 x1 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x13) = λ x3 x4 . x4) ⟶ (TwoRamseyGraph_3_6_Church17 x1 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x15) = λ x3 x4 . x4) ⟶ (TwoRamseyGraph_3_6_Church17 x0 x1 = λ x3 x4 . x4) ⟶ ∀ x2 : ο . (84660.. x0 ⟶ x2) ⟶ (84660.. x1 ⟶ x2) ⟶ x2 (proof)
Definition u9 := ordsucc u8
Definition u10 := ordsucc u9
Param u12 : ι
Known 4f699.. : Church17_p (λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x10)
Known e886d.. : u10 ∈ u17
Known d7087.. : u17_to_Church17 u10 = λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 . x11
Known d5e0f.. : Church17_p (λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x12)
Known a1a10.. : u12 ∈ u17
Known a52d8.. : u17_to_Church17 u12 = λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 . x13
Theorem 6d6a7.. : ∀ x0 . x0 ⊆ u8 ⟶ atleastp u2 x0 ⟶ (∀ x1 . x1 ∈ x0 ⟶ not (TwoRamseyGraph_3_6_17 x1 u10)) ⟶ (∀ x1 . x1 ∈ x0 ⟶ not (TwoRamseyGraph_3_6_17 x1 u12)) ⟶ (∀ 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 (proof)
Known 3badb.. : 84660.. (λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x0)
Theorem c08c6.. : ∀ x0 x1 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_lt8 x0 ⟶ Church17_lt8 x1 ⟶ (TwoRamseyGraph_3_6_Church17 x0 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x12) = λ x3 x4 . x4) ⟶ (TwoRamseyGraph_3_6_Church17 x0 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x16) = λ x3 x4 . x4) ⟶ (TwoRamseyGraph_3_6_Church17 x0 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x17) = λ x3 x4 . x4) ⟶ (TwoRamseyGraph_3_6_Church17 x1 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x12) = λ x3 x4 . x4) ⟶ (TwoRamseyGraph_3_6_Church17 x1 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x16) = λ x3 x4 . x4) ⟶ (TwoRamseyGraph_3_6_Church17 x1 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x17) = λ x3 x4 . x4) ⟶ (TwoRamseyGraph_3_6_Church17 x0 x1 = λ x3 x4 . x4) ⟶ ∀ x2 : ο . (84660.. x0 ⟶ x2) ⟶ (84660.. x1 ⟶ x2) ⟶ x2 (proof)
Definition u13 := ordsucc u12
Definition u14 := ordsucc u13
Known a8b9a.. : Church17_p (λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x9)
Known fd1a6.. : u9 ∈ u17
Known a3fb1.. : u17_to_Church17 u9 = λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 . x10
Known 51598.. : Church17_p (λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x13)
Known 7315d.. : u13 ∈ u17
Known 0975c.. : u17_to_Church17 u13 = λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 . x14
Known 15dad.. : Church17_p (λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x14)
Known 35e01.. : u14 ∈ u17
Known cf897.. : u17_to_Church17 u14 = λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 . x15
Theorem 0f921.. : ∀ x0 . x0 ⊆ u8 ⟶ atleastp u2 x0 ⟶ (∀ x1 . x1 ∈ x0 ⟶ not (TwoRamseyGraph_3_6_17 x1 u9)) ⟶ (∀ x1 . x1 ∈ x0 ⟶ not (TwoRamseyGraph_3_6_17 x1 u13)) ⟶ (∀ x1 . x1 ∈ x0 ⟶ not (TwoRamseyGraph_3_6_17 x1 u14)) ⟶ (∀ 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 (proof)
Theorem f2049.. : ∀ x0 x1 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_lt8 x0 ⟶ Church17_lt8 x1 ⟶ (TwoRamseyGraph_3_6_Church17 x0 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x15) = λ x3 x4 . x4) ⟶ (TwoRamseyGraph_3_6_Church17 x0 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x16) = λ x3 x4 . x4) ⟶ (TwoRamseyGraph_3_6_Church17 x0 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x17) = λ x3 x4 . x4) ⟶ (TwoRamseyGraph_3_6_Church17 x1 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x15) = λ x3 x4 . x4) ⟶ (TwoRamseyGraph_3_6_Church17 x1 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x16) = λ x3 x4 . x4) ⟶ (TwoRamseyGraph_3_6_Church17 x1 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x17) = λ x3 x4 . x4) ⟶ (TwoRamseyGraph_3_6_Church17 x0 x1 = λ x3 x4 . x4) ⟶ ∀ x2 : ο . (84660.. x0 ⟶ x2) ⟶ (84660.. x1 ⟶ x2) ⟶ x2 (proof)
Theorem 7eaa0.. : ∀ x0 . x0 ⊆ u8 ⟶ atleastp u2 x0 ⟶ (∀ x1 . x1 ∈ x0 ⟶ not (TwoRamseyGraph_3_6_17 x1 u12)) ⟶ (∀ x1 . x1 ∈ x0 ⟶ not (TwoRamseyGraph_3_6_17 x1 u13)) ⟶ (∀ x1 . x1 ∈ x0 ⟶ not (TwoRamseyGraph_3_6_17 x1 u14)) ⟶ (∀ 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 (proof)
Theorem 02b51.. : ∀ x0 x1 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_lt8 x0 ⟶ Church17_lt8 x1 ⟶ (TwoRamseyGraph_3_6_Church17 x0 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x15) = λ x3 x4 . x4) ⟶ (TwoRamseyGraph_3_6_Church17 x0 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x16) = λ x3 x4 . x4) ⟶ (TwoRamseyGraph_3_6_Church17 x0 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x18) = λ x3 x4 . x4) ⟶ (TwoRamseyGraph_3_6_Church17 x1 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x15) = λ x3 x4 . x4) ⟶ (TwoRamseyGraph_3_6_Church17 x1 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x16) = λ x3 x4 . x4) ⟶ (TwoRamseyGraph_3_6_Church17 x1 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x18) = λ x3 x4 . x4) ⟶ (TwoRamseyGraph_3_6_Church17 x0 x1 = λ x3 x4 . x4) ⟶ ∀ x2 : ο . (84660.. x0 ⟶ x2) ⟶ (84660.. x1 ⟶ x2) ⟶ x2 (proof)
Theorem b1955.. : ∀ x0 . x0 ⊆ u8 ⟶ atleastp u2 x0 ⟶ (∀ x1 . x1 ∈ x0 ⟶ not (TwoRamseyGraph_3_6_17 x1 u12)) ⟶ (∀ x1 . x1 ∈ x0 ⟶ not (TwoRamseyGraph_3_6_17 x1 u13)) ⟶ (∀ x1 . x1 ∈ x0 ⟶ not (TwoRamseyGraph_3_6_17 x1 u15)) ⟶ (∀ 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 (proof)
Theorem 904e1.. : ∀ x0 x1 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_lt8 x0 ⟶ Church17_lt8 x1 ⟶ (TwoRamseyGraph_3_6_Church17 x0 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x15) = λ x3 x4 . x4) ⟶ (TwoRamseyGraph_3_6_Church17 x0 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x17) = λ x3 x4 . x4) ⟶ (TwoRamseyGraph_3_6_Church17 x0 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x18) = λ x3 x4 . x4) ⟶ (TwoRamseyGraph_3_6_Church17 x1 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x15) = λ x3 x4 . x4) ⟶ (TwoRamseyGraph_3_6_Church17 x1 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x17) = λ x3 x4 . x4) ⟶ (TwoRamseyGraph_3_6_Church17 x1 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x18) = λ x3 x4 . x4) ⟶ (TwoRamseyGraph_3_6_Church17 x0 x1 = λ x3 x4 . x4) ⟶ ∀ x2 : ο . (84660.. x0 ⟶ x2) ⟶ (84660.. x1 ⟶ x2) ⟶ x2 (proof)
Theorem e49bb.. : ∀ x0 . x0 ⊆ u8 ⟶ atleastp u2 x0 ⟶ (∀ x1 . x1 ∈ x0 ⟶ not (TwoRamseyGraph_3_6_17 x1 u12)) ⟶ (∀ x1 . x1 ∈ x0 ⟶ not (TwoRamseyGraph_3_6_17 x1 u14)) ⟶ (∀ x1 . x1 ∈ x0 ⟶ not (TwoRamseyGraph_3_6_17 x1 u15)) ⟶ (∀ 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 (proof)
Theorem e0cec.. : ∀ x0 x1 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_lt8 x0 ⟶ Church17_lt8 x1 ⟶ (TwoRamseyGraph_3_6_Church17 x0 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x16) = λ x3 x4 . x4) ⟶ (TwoRamseyGraph_3_6_Church17 x0 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x17) = λ x3 x4 . x4) ⟶ (TwoRamseyGraph_3_6_Church17 x0 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x18) = λ x3 x4 . x4) ⟶ (TwoRamseyGraph_3_6_Church17 x1 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x16) = λ x3 x4 . x4) ⟶ (TwoRamseyGraph_3_6_Church17 x1 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x17) = λ x3 x4 . x4) ⟶ (TwoRamseyGraph_3_6_Church17 x1 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x18) = λ x3 x4 . x4) ⟶ (TwoRamseyGraph_3_6_Church17 x0 x1 = λ x3 x4 . x4) ⟶ ∀ x2 : ο . (84660.. x0 ⟶ x2) ⟶ (84660.. x1 ⟶ x2) ⟶ x2 (proof)
Theorem 1318a.. : ∀ x0 . x0 ⊆ u8 ⟶ atleastp u2 x0 ⟶ (∀ x1 . x1 ∈ x0 ⟶ not (TwoRamseyGraph_3_6_17 x1 u13)) ⟶ (∀ x1 . x1 ∈ x0 ⟶ not (TwoRamseyGraph_3_6_17 x1 u14)) ⟶ (∀ x1 . x1 ∈ x0 ⟶ not (TwoRamseyGraph_3_6_17 x1 u15)) ⟶ (∀ 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 (proof)
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
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
Known a0edc.. : ∀ x0 . x0 ∈ u17 ⟶ ∀ x1 . x1 ∈ u17 ⟶ TwoRamseyGraph_3_6_17 x0 x1 ⟶ 0aea9.. x0 x1
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)
Param u21 : ι
Definition nIn^nIn := λ x0 x1 . not (x0 ∈ x1)
Param u11 : ι
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_4^nat_4 : nat_p 4
Param binunion^binunion : ι → ι → ι
Param Sing^Sing : ι → ι
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_3^nat_3 : nat_p 3
Definition nSubq^nSubq := λ x0 x1 . not (x0 ⊆ x1)
Known nat_2^nat_2 : nat_p 2
Param setminus^setminus : ι → ι → ι
Known ee881.. : ∀ x0 . x0 ∈ setminus u16 u12 ⟶ ∀ x1 : ι → ο . x1 u12 ⟶ x1 u13 ⟶ x1 u14 ⟶ x1 u15 ⟶ x1 x0
Known setminusI^setminusI : ∀ x0 x1 x2 . x2 ∈ x0 ⟶ nIn x2 x1 ⟶ x2 ∈ setminus x0 x1
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 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 893fe.. : add_nat u4 u1 = u5
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 SingE^SingE : ∀ x0 x1 . x1 ∈ Sing x0 ⟶ x1 = x0
Known 2d2af.. : u12 ⊆ u17
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_12^nat_12 : nat_p u12
Known 49949.. : ∀ x0 . x0 ∈ setminus u12 u6 ⟶ ∀ x1 : ι → ο . x1 u6 ⟶ x1 u7 ⟶ x1 u8 ⟶ x1 u9 ⟶ x1 u10 ⟶ x1 u11 ⟶ x1 x0
Known Subq_tra^Subq_tra : ∀ x0 x1 x2 . x0 ⊆ x1 ⟶ x1 ⊆ x2 ⟶ x0 ⊆ x2
Known bd770.. : u6 ⊆ u8
Known 021ac.. : u7 ⊆ u8
Known 9e99f.. : 55574.. u8 = λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 . x9
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 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 ordsuccE^ordsuccE : ∀ x0 x1 . x1 ∈ ordsucc x0 ⟶ or (x1 ∈ x0) (x1 = x0)
Known 5786d.. : ∀ x0 . x0 ∈ setminus u13 u6 ⟶ ∀ x1 : ι → ο . x1 u6 ⟶ x1 u7 ⟶ x1 u8 ⟶ x1 u9 ⟶ x1 u10 ⟶ x1 u11 ⟶ x1 u12 ⟶ x1 x0
Known 151b0.. : 55574.. u7 = λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 . x8
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 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 bf41f.. : ∀ x0 . x0 ∈ setminus u12 u8 ⟶ ∀ x1 : ι → ο . x1 u8 ⟶ x1 u9 ⟶ x1 u10 ⟶ x1 u11 ⟶ x1 x0
Known a1137.. : ∀ x0 . x0 ∈ setminus u14 u6 ⟶ ∀ x1 : ι → ο . x1 u6 ⟶ x1 u7 ⟶ x1 u8 ⟶ x1 u9 ⟶ x1 u10 ⟶ x1 u11 ⟶ x1 u12 ⟶ x1 u13 ⟶ x1 x0
Known 8ef56.. : 55574.. u6 = λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 . x7
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 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 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
Known ordsuccI1^ordsuccI1 : ∀ x0 . x0 ⊆ ordsucc x0
Known dneg^dneg : ∀ x0 : ο . not (not x0) ⟶ x0
Known neq_i_sym^neq_i_sym : ∀ x0 x1 . (x0 = x1 ⟶ ∀ x2 : ο . x2) ⟶ x1 = x0 ⟶ ∀ x2 : ο . x2
Known 0b225.. : u13 = u8 ⟶ ∀ x0 : ο . x0
Known 0420f.. : ∀ x0 . x0 ∈ setminus u15 u6 ⟶ ∀ x1 : ι → ο . x1 u6 ⟶ x1 u7 ⟶ x1 u8 ⟶ x1 u9 ⟶ x1 u10 ⟶ x1 u11 ⟶ x1 u12 ⟶ x1 u13 ⟶ x1 u14 ⟶ x1 x0
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 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 xm^xm : ∀ x0 : ο . or x0 (not x0)
Known nat_8^nat_8 : nat_p 8
Known 3a7bc.. : u15 = u9 ⟶ ∀ x0 : ο . x0
Known f5ab5.. : u14 = u10 ⟶ ∀ x0 : ο . x0
Known nat_0^nat_0 : nat_p 0
Known cases_8^cases_8 : ∀ x0 . x0 ∈ u8 ⟶ ∀ x1 : ι → ο . x1 0 ⟶ x1 u1 ⟶ x1 u2 ⟶ x1 u3 ⟶ x1 u4 ⟶ x1 u5 ⟶ x1 u6 ⟶ x1 u7 ⟶ x1 x0
Known In_0_4^In_0_4 : 0 ∈ 4
Known In_1_4^In_1_4 : 1 ∈ 4
Known In_2_4^In_2_4 : 2 ∈ 4
Known In_3_4^In_3_4 : 3 ∈ 4
Known 4b742.. : u15 = u4 ⟶ ∀ x0 : ο . x0
Known 5f4d4.. : 55574.. u4 = λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 . x5
Known 07eba.. : u12 = u5 ⟶ ∀ x0 : ο . x0
Known b535d.. : 55574.. u5 = λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 . x6
Known 62d80.. : u14 = u6 ⟶ ∀ x0 : ο . x0
Known d9b35.. : u13 = u7 ⟶ ∀ x0 : ο . x0
Known a6a6c.. : u12 = u8 ⟶ ∀ x0 : ο . x0
Known 22885.. : u12 = u9 ⟶ ∀ x0 : ο . x0
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 620a1.. : ∀ x0 . x0 ⊆ u6 ⟶ atleastp u4 x0 ⟶ not (∀ x1 . x1 ∈ x0 ⟶ ∀ x2 . x2 ∈ x0 ⟶ (x1 = x2 ⟶ ∀ x3 : ο . x3) ⟶ not (0aea9.. x1 x2))
Known nat_6^nat_6 : nat_p 6
Known 480b2.. : add_nat u3 u1 = u4
Known Subq_ref^Subq_ref : ∀ x0 . x0 ⊆ x0
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_16^nat_16 : nat_p u16
Theorem 50d90.. : ∀ x0 . x0 ⊆ u16 ⟶ atleastp u5 x0 ⟶ (∀ x1 . x1 ∈ x0 ⟶ not (0aea9.. x1 u17)) ⟶ (∀ x1 . x1 ∈ x0 ⟶ not (0aea9.. x1 u21)) ⟶ not (∀ x1 . x1 ∈ x0 ⟶ ∀ x2 . x2 ∈ x0 ⟶ (x1 = x2 ⟶ ∀ x3 : ο . x3) ⟶ not (0aea9.. x1 x2)) (proof)