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
Definition u9 := ordsucc u8
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
Param atleastp^atleastp : ι → ι → ο
Definition False^False := ∀ x0 : ο . x0
Definition not^not := λ x0 : ο . x0 ⟶ False
Definition u18 := ordsucc u17
Definition u19 := ordsucc u18
Definition u20 := ordsucc u19
Definition u21 := ordsucc u20
Definition u22 := ordsucc u21
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
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 nIn^nIn := λ x0 x1 . not (x0 ∈ x1)
Known 865bf.. : ∀ x0 . atleastp u3 x0 ⟶ (∀ x1 . x1 ∈ x0 ⟶ ordinal x1) ⟶ ∀ x1 : ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ x2 ∈ x3 ⟶ x3 ∈ x4 ⟶ x1) ⟶ x1
Known equip_atleastp^{equip_atleastp} : ∀ x0 x1 . equip x0 x1 ⟶ atleastp x0 x1
Definition 00974.. := λ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . ∀ x1 : (ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι) → ο . x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 . x2) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 . x3) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 . x4) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 . x5) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 . x6) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 . x7) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 . x8) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 . x9) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 . x10) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 . x11) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 . x12) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 . x13) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 . x14) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 . x15) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 . x16) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 . x17) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 . x18) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 . x19) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 . x20) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 . x21) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 . x22) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 . x23) ⟶ x1 x0
Param setminus^setminus : ι → ι → ι
Known 4fd0a.. : ∀ x0 . x0 ∈ setminus u17 u12 ⟶ ∀ x1 : ι → ο . x1 u12 ⟶ x1 u13 ⟶ x1 u14 ⟶ x1 u15 ⟶ x1 u16 ⟶ x1 x0
Known setminusI^setminusI : ∀ x0 x1 x2 . x2 ∈ x0 ⟶ nIn x2 x1 ⟶ x2 ∈ setminus x0 x1
Param TwoRamseyGraph_3_6_17 : ι → ι → ο
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))
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 a0edc.. : ∀ x0 . x0 ∈ u17 ⟶ ∀ x1 . x1 ∈ u17 ⟶ TwoRamseyGraph_3_6_17 x0 x1 ⟶ 0aea9.. x0 x1
Known 2d2af.. : u12 ⊆ u17
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_12^nat_12 : nat_p u12
Known 27661.. : ∀ x0 . x0 ∈ setminus u12 u10 ⟶ ∀ x1 : ι → ο . x1 u10 ⟶ x1 u11 ⟶ x1 x0
Known ordsuccE^ordsuccE : ∀ x0 x1 . x1 ∈ ordsucc x0 ⟶ or (x1 ∈ x0) (x1 = x0)
Known c8243.. : ∀ x0 x1 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . 00974.. x0 ⟶ 00974.. x1 ⟶ (94591.. x0 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . x13) = λ x3 x4 . x4) ⟶ (94591.. x0 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . x14) = λ x3 x4 . x4) ⟶ (94591.. x0 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . x15) = λ x3 x4 . x4) ⟶ (94591.. x0 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . x21) = λ x3 x4 . x4) ⟶ (94591.. x0 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . x23) = λ x3 x4 . x4) ⟶ (94591.. x1 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . x13) = λ x3 x4 . x4) ⟶ (94591.. x1 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . x14) = λ x3 x4 . x4) ⟶ (94591.. x1 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . x15) = λ x3 x4 . x4) ⟶ (94591.. x1 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . x21) = λ x3 x4 . x4) ⟶ (94591.. x1 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . x23) = λ x3 x4 . x4) ⟶ 94591.. x0 x1 = λ x3 x4 . x3
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 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 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 fc2d4.. : ∀ x0 . x0 ∈ setminus u13 u10 ⟶ ∀ x1 : ι → ο . x1 u10 ⟶ x1 u11 ⟶ x1 u12 ⟶ x1 x0
Known d1edb.. : ∀ x0 x1 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . 00974.. x0 ⟶ 00974.. x1 ⟶ (94591.. x0 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . x14) = λ x3 x4 . x4) ⟶ (94591.. x0 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . x15) = λ x3 x4 . x4) ⟶ (94591.. x0 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . x16) = λ x3 x4 . x4) ⟶ (94591.. x0 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . x21) = λ x3 x4 . x4) ⟶ (94591.. x0 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . x23) = λ x3 x4 . x4) ⟶ (94591.. x1 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . x14) = λ x3 x4 . x4) ⟶ (94591.. x1 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . x15) = λ x3 x4 . x4) ⟶ (94591.. x1 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . x16) = λ x3 x4 . x4) ⟶ (94591.. x1 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . x21) = λ x3 x4 . x4) ⟶ (94591.. x1 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . x23) = λ x3 x4 . x4) ⟶ 94591.. x0 x1 = λ x3 x4 . x3
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 98cac.. : ∀ x0 . x0 ∈ setminus u14 u10 ⟶ ∀ x1 : ι → ο . x1 u10 ⟶ x1 u11 ⟶ x1 u12 ⟶ x1 u13 ⟶ x1 x0
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 7676f.. : ∀ x0 x1 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . 00974.. x0 ⟶ 00974.. x1 ⟶ (94591.. x0 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . x15) = λ x3 x4 . x4) ⟶ (94591.. x0 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . x16) = λ x3 x4 . x4) ⟶ (94591.. x0 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . x17) = λ x3 x4 . x4) ⟶ (94591.. x0 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . x21) = λ x3 x4 . x4) ⟶ (94591.. x0 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . x23) = λ x3 x4 . x4) ⟶ (94591.. x1 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . x15) = λ x3 x4 . x4) ⟶ (94591.. x1 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . x16) = λ x3 x4 . x4) ⟶ (94591.. x1 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . x17) = λ x3 x4 . x4) ⟶ (94591.. x1 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . x21) = λ x3 x4 . x4) ⟶ (94591.. x1 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . x23) = λ x3 x4 . x4) ⟶ 94591.. x0 x1 = λ x3 x4 . x3
Known 332b1.. : ∀ x0 . x0 ∈ setminus u15 u10 ⟶ ∀ x1 : ι → ο . 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 be4bb.. : ∀ x0 x1 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . 00974.. x0 ⟶ 00974.. x1 ⟶ (94591.. x0 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . x13) = λ x3 x4 . x4) ⟶ (94591.. x0 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . x15) = λ x3 x4 . x4) ⟶ (94591.. x0 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . x18) = λ x3 x4 . x4) ⟶ (94591.. x0 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . x21) = λ x3 x4 . x4) ⟶ (94591.. x0 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . x23) = λ x3 x4 . x4) ⟶ (94591.. x1 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . x13) = λ x3 x4 . x4) ⟶ (94591.. x1 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . x15) = λ x3 x4 . x4) ⟶ (94591.. x1 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . x18) = λ x3 x4 . x4) ⟶ (94591.. x1 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . x21) = λ x3 x4 . x4) ⟶ (94591.. x1 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . x23) = λ x3 x4 . x4) ⟶ 94591.. x0 x1 = λ x3 x4 . x3
Known 16203.. : ∀ x0 x1 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . 00974.. x0 ⟶ 00974.. x1 ⟶ (94591.. x0 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . x15) = λ x3 x4 . x4) ⟶ (94591.. x0 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . x16) = λ x3 x4 . x4) ⟶ (94591.. x0 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . x18) = λ x3 x4 . x4) ⟶ (94591.. x0 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . x21) = λ x3 x4 . x4) ⟶ (94591.. x0 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . x23) = λ x3 x4 . x4) ⟶ (94591.. x1 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . x15) = λ x3 x4 . x4) ⟶ (94591.. x1 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . x16) = λ x3 x4 . x4) ⟶ (94591.. x1 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . x18) = λ x3 x4 . x4) ⟶ (94591.. x1 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . x21) = λ x3 x4 . x4) ⟶ (94591.. x1 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . x23) = λ x3 x4 . x4) ⟶ 94591.. x0 x1 = λ x3 x4 . x3
Known b72e6.. : ∀ x0 x1 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . 00974.. x0 ⟶ 00974.. x1 ⟶ (94591.. x0 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . x15) = λ x3 x4 . x4) ⟶ (94591.. x0 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . x17) = λ x3 x4 . x4) ⟶ (94591.. x0 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . x18) = λ x3 x4 . x4) ⟶ (94591.. x0 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . x21) = λ x3 x4 . x4) ⟶ (94591.. x0 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . x23) = λ x3 x4 . x4) ⟶ (94591.. x1 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . x15) = λ x3 x4 . x4) ⟶ (94591.. x1 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . x17) = λ x3 x4 . x4) ⟶ (94591.. x1 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . x18) = λ x3 x4 . x4) ⟶ (94591.. x1 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . x21) = λ x3 x4 . x4) ⟶ (94591.. x1 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . x23) = λ x3 x4 . x4) ⟶ 94591.. x0 x1 = λ x3 x4 . x3
Known 1aedf.. : ∀ x0 x1 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . 00974.. x0 ⟶ 00974.. x1 ⟶ (94591.. x0 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . x16) = λ x3 x4 . x4) ⟶ (94591.. x0 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . x17) = λ x3 x4 . x4) ⟶ (94591.. x0 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . x18) = λ x3 x4 . x4) ⟶ (94591.. x0 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . x21) = λ x3 x4 . x4) ⟶ (94591.. x0 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . x23) = λ x3 x4 . x4) ⟶ (94591.. x1 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . x16) = λ x3 x4 . x4) ⟶ (94591.. x1 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . x17) = λ x3 x4 . x4) ⟶ (94591.. x1 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . x18) = λ x3 x4 . x4) ⟶ (94591.. x1 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . x21) = λ x3 x4 . x4) ⟶ (94591.. x1 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . x23) = λ x3 x4 . x4) ⟶ 94591.. x0 x1 = λ x3 x4 . x3
Known 853d4.. : ∀ x0 . x0 ∈ setminus u16 u10 ⟶ ∀ x1 : ι → ο . x1 u10 ⟶ x1 u11 ⟶ x1 u12 ⟶ x1 u13 ⟶ x1 u14 ⟶ x1 u15 ⟶ x1 x0
Known 7f524.. : ∀ x0 x1 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . 00974.. x0 ⟶ 00974.. x1 ⟶ (94591.. x0 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . x13) = λ x3 x4 . x4) ⟶ (94591.. x0 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . x14) = λ x3 x4 . x4) ⟶ (94591.. x0 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . x19) = λ x3 x4 . x4) ⟶ (94591.. x0 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . x21) = λ x3 x4 . x4) ⟶ (94591.. x0 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . x23) = λ x3 x4 . x4) ⟶ (94591.. x1 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . x13) = λ x3 x4 . x4) ⟶ (94591.. x1 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . x14) = λ x3 x4 . x4) ⟶ (94591.. x1 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . x19) = λ x3 x4 . x4) ⟶ (94591.. x1 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . x21) = λ x3 x4 . x4) ⟶ (94591.. x1 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . x23) = λ x3 x4 . x4) ⟶ 94591.. x0 x1 = λ x3 x4 . x3
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 44418.. : ∀ x0 . x0 ∈ u10 ⟶ ∀ x1 : ι → ο . x1 0 ⟶ x1 u1 ⟶ x1 u2 ⟶ x1 u3 ⟶ x1 u4 ⟶ x1 u5 ⟶ x1 u6 ⟶ x1 u7 ⟶ x1 u8 ⟶ x1 u9 ⟶ x1 x0
Known EmptyE^EmptyE : ∀ x0 . nIn x0 0
Known cases_1^cases_1 : ∀ x0 . x0 ∈ u1 ⟶ ∀ x1 : ι → ο . x1 0 ⟶ x1 x0
Known cases_2^cases_2 : ∀ x0 . x0 ∈ u2 ⟶ ∀ x1 : ι → ο . x1 0 ⟶ x1 u1 ⟶ x1 x0
Known cases_3^cases_3 : ∀ x0 . x0 ∈ u3 ⟶ ∀ x1 : ι → ο . x1 0 ⟶ x1 u1 ⟶ x1 u2 ⟶ 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 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 In_no2cycle^In_no2cycle : ∀ x0 x1 . x0 ∈ x1 ⟶ x1 ∈ x0 ⟶ False
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 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 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 bb555.. : 55574.. u18 = λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 . x19
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 54789.. : 55574.. u20 = λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 . x21
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 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 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 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 18048.. : ∀ x0 x1 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . 00974.. x0 ⟶ 00974.. x1 ⟶ or (94591.. x0 x1 = λ x3 x4 . x3) (94591.. x0 x1 = λ x3 x4 . x4)
Known FalseE^FalseE : False ⟶ ∀ x0 : ο . x0
Known d91eb.. : ∀ x0 . x0 ∈ u22 ⟶ 00974.. (55574.. x0)
Known In_no3cycle^In_no3cycle : ∀ x0 x1 x2 . x0 ∈ x1 ⟶ x1 ∈ x2 ⟶ x2 ∈ x0 ⟶ False
Known In_no4cycle^In_no4cycle : ∀ x0 x1 x2 x3 . x0 ∈ x1 ⟶ x1 ∈ x2 ⟶ x2 ∈ x3 ⟶ x3 ∈ x0 ⟶ False
Known e46ec.. : u17 ⊆ u22
Known 86222.. : ∀ x0 . x0 ∈ setminus u10 u6 ⟶ ∀ x1 : ι → ο . x1 u6 ⟶ x1 u7 ⟶ x1 u8 ⟶ x1 u9 ⟶ x1 x0
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_17^nat_17 : nat_p u17
Theorem c3170.. : ∀ x0 . x0 ⊆ u17 ⟶ atleastp u5 x0 ⟶ (∀ x1 . x1 ∈ x0 ⟶ not (0aea9.. x1 u18)) ⟶ (∀ x1 . x1 ∈ x0 ⟶ not (0aea9.. x1 u20)) ⟶ not (∀ x1 . x1 ∈ x0 ⟶ ∀ x2 . x2 ∈ x0 ⟶ (x1 = x2 ⟶ ∀ x3 : ο . x3) ⟶ not (0aea9.. x1 x2)) (proof)
Known nat_5^nat_5 : nat_p 5
Known dcb62.. : ∀ x0 . x0 ∈ setminus u22 u17 ⟶ ∀ x1 : ι → ο . x1 u17 ⟶ x1 u18 ⟶ x1 u19 ⟶ x1 u20 ⟶ x1 u21 ⟶ x1 x0
Known 5f797.. : 0aea9.. u17 u18
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 46814.. : 0 ∈ 12
Known 2b77d.. : 1 ∈ 12
Known 7c2ac.. : 2 ∈ 12
Known 2f583.. : 3 ∈ 12
Known e4fc0.. : 4 ∈ 12
Known 04716.. : 5 ∈ 12
Known fbe39.. : 6 ∈ 12
Known 35d73.. : 7 ∈ 12
Known 5196c.. : 8 ∈ 12
Known 4fa36.. : 9 ∈ 12
Known 42552.. : 10 ∈ 12
Known fee2e.. : 11 ∈ 12
Known a1a10.. : u12 ∈ u17
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 7315d.. : u13 ∈ u17
Known 35e01.. : u14 ∈ u17
Known 31b8d.. : u15 ∈ u17
Known dfaf3.. : u16 ∈ u17
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 6eb03.. : 0aea9.. u17 u20
Known 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))
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 c1d56.. : u17 ⊆ u21
Known e0489.. : u17 ∈ u18
Known 4a27e.. : 0aea9.. u18 u19
Known 2d95b.. : u17 ⊆ u20
Known 42954.. : u17 = u20 ⟶ ∀ x0 : ο . x0
Known 994f0.. : 0aea9.. u18 u21
Known 25029.. : u18 ∈ u19
Known f355c.. : 0aea9.. u19 u20
Known 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))
Known edc13.. : u18 = u19 ⟶ ∀ x0 : ο . x0
Known ordsuccI1^ordsuccI1 : ∀ x0 . x0 ⊆ ordsucc x0
Known 9ea5b.. : u19 ∈ u20
Known 11aea.. : 0aea9.. u20 u21
Known c955e.. : u20 ∈ u21
Known 5922f.. : ∀ x0 . x0 ⊆ u17 ⟶ atleastp u6 x0 ⟶ not (∀ x1 . x1 ∈ x0 ⟶ ∀ x2 . x2 ∈ x0 ⟶ (x1 = x2 ⟶ ∀ x3 : ο . x3) ⟶ not (TwoRamseyGraph_3_6_17 x1 x2))
Known 561b1.. : add_nat u5 u1 = u6
Known Subq_tra^Subq_tra : ∀ x0 x1 x2 . x0 ⊆ x1 ⟶ x1 ⊆ x2 ⟶ x0 ⊆ x2
Known daa33.. : nat_p u22
Theorem 8432f.. : ∀ x0 . x0 ⊆ u22 ⟶ atleastp u7 x0 ⟶ not (∀ x1 . x1 ∈ x0 ⟶ ∀ x2 . x2 ∈ x0 ⟶ (x1 = x2 ⟶ ∀ x3 : ο . x3) ⟶ not (0aea9.. x1 x2)) (proof)
Definition and^and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
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)
Known ebffb.. : ∀ x0 x1 . 0aea9.. x0 x1 ⟶ 0aea9.. x1 x0
Known 907a2.. : ∀ x0 . x0 ⊆ u22 ⟶ atleastp u3 x0 ⟶ not (∀ x1 . x1 ∈ x0 ⟶ ∀ x2 . x2 ∈ x0 ⟶ (x1 = x2 ⟶ ∀ x3 : ο . x3) ⟶ 0aea9.. x1 x2)
Theorem 3738e.. : not (TwoRamseyProp_atleastp u3 u7 u22) (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 not_TwoRamseyProp_3_7_22^{not_TwoRamseyProp_3_7_22} : not (TwoRamseyProp 3 7 22) (proof)