Proofgold Address

Definition and^and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
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)
Definition atleastp^atleastp := λ x0 x1 . ∀ x2 : ο . (∀ x3 : ι → ι . inj x0 x1 x3 ⟶ x2) ⟶ x2
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
Known 3ed86.. : ∀ x0 . atleastp u5 x0 ⟶ ∀ x1 : ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ (x2 = x3 ⟶ ∀ x7 : ο . x7) ⟶ (x2 = x4 ⟶ ∀ x7 : ο . x7) ⟶ (x2 = x5 ⟶ ∀ x7 : ο . x7) ⟶ (x2 = x6 ⟶ ∀ x7 : ο . x7) ⟶ (x3 = x4 ⟶ ∀ x7 : ο . x7) ⟶ (x3 = x5 ⟶ ∀ x7 : ο . x7) ⟶ (x3 = x6 ⟶ ∀ x7 : ο . x7) ⟶ (x4 = x5 ⟶ ∀ x7 : ο . x7) ⟶ (x4 = x6 ⟶ ∀ x7 : ο . x7) ⟶ (x5 = x6 ⟶ ∀ x7 : ο . x7) ⟶ x1) ⟶ x1
Definition or^or := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Definition False^False := ∀ x0 : ο . x0
Definition not^not := λ x0 : ο . x0 ⟶ False
Known xm^xm : ∀ x0 : ο . or x0 (not x0)
Known FalseE^FalseE : False ⟶ ∀ x0 : ο . x0
Param nat_p^nat_p : ι → ο
Known 4fb58..^{Pigeonhole_not_atleastp_ordsucc} : ∀ x0 . nat_p x0 ⟶ not (atleastp (ordsucc x0) x0)
Known nat_5^nat_5 : nat_p 5
Known atleastp_tra^atleastp_tra : ∀ x0 x1 x2 . atleastp x0 x1 ⟶ atleastp x1 x2 ⟶ atleastp x0 x2
Param ap^ap : ι → ι → ι
Param lam^Sigma : ι → (ι → ι) → ι
Param If_i^If_i : ο → ι → ι → ι
Param inv^inv : ι → (ι → ι) → ι → ι
Known andI^andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Known surj_rinv^surj_rinv : ∀ x0 x1 . ∀ x2 : ι → ι . (∀ x3 . x3 ∈ x1 ⟶ ∀ x4 : ο . (∀ x5 . and (x5 ∈ x0) (x2 x5 = x3) ⟶ x4) ⟶ x4) ⟶ ∀ x3 . x3 ∈ x1 ⟶ and (inv x0 x2 x3 ∈ x0) (x2 (inv x0 x2 x3) = x3)
Known dneg^dneg : ∀ x0 : ο . not (not x0) ⟶ x0
Known In_0_5^In_0_5 : 0 ∈ 5
Known tuple_5_0_eq^tuple_5_0_eq : ∀ x0 x1 x2 x3 x4 . ap (lam 5 (λ x6 . If_i (x6 = 0) x0 (If_i (x6 = 1) x1 (If_i (x6 = 2) x2 (If_i (x6 = 3) x3 x4))))) 0 = x0
Known In_1_5^In_1_5 : 1 ∈ 5
Known tuple_5_1_eq^tuple_5_1_eq : ∀ x0 x1 x2 x3 x4 . ap (lam 5 (λ x6 . If_i (x6 = 0) x0 (If_i (x6 = 1) x1 (If_i (x6 = 2) x2 (If_i (x6 = 3) x3 x4))))) 1 = x1
Known In_2_5^In_2_5 : 2 ∈ 5
Known tuple_5_2_eq^tuple_5_2_eq : ∀ x0 x1 x2 x3 x4 . ap (lam 5 (λ x6 . If_i (x6 = 0) x0 (If_i (x6 = 1) x1 (If_i (x6 = 2) x2 (If_i (x6 = 3) x3 x4))))) 2 = x2
Known In_3_5^In_3_5 : 3 ∈ 5
Known tuple_5_3_eq^tuple_5_3_eq : ∀ x0 x1 x2 x3 x4 . ap (lam 5 (λ x6 . If_i (x6 = 0) x0 (If_i (x6 = 1) x1 (If_i (x6 = 2) x2 (If_i (x6 = 3) x3 x4))))) 3 = x3
Known In_4_5^In_4_5 : 4 ∈ 5
Known tuple_5_4_eq^tuple_5_4_eq : ∀ x0 x1 x2 x3 x4 . ap (lam 5 (λ x6 . If_i (x6 = 0) x0 (If_i (x6 = 1) x1 (If_i (x6 = 2) x2 (If_i (x6 = 3) x3 x4))))) 4 = x4
Known nat_In_atleastp : ∀ x0 . nat_p x0 ⟶ ∀ x1 . x1 ∈ x0 ⟶ atleastp x1 x0
Known nat_6^nat_6 : nat_p 6
Known In_5_6^In_5_6 : u5 ∈ u6
Theorem a753e.. : ∀ x0 . atleastp u6 x0 ⟶ ∀ x1 : ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ (x2 = x3 ⟶ ∀ x8 : ο . x8) ⟶ (x2 = x4 ⟶ ∀ x8 : ο . x8) ⟶ (x2 = x5 ⟶ ∀ x8 : ο . x8) ⟶ (x2 = x6 ⟶ ∀ x8 : ο . x8) ⟶ (x2 = x7 ⟶ ∀ x8 : ο . x8) ⟶ (x3 = x4 ⟶ ∀ x8 : ο . x8) ⟶ (x3 = x5 ⟶ ∀ x8 : ο . x8) ⟶ (x3 = x6 ⟶ ∀ x8 : ο . x8) ⟶ (x3 = x7 ⟶ ∀ x8 : ο . x8) ⟶ (x4 = x5 ⟶ ∀ x8 : ο . x8) ⟶ (x4 = x6 ⟶ ∀ x8 : ο . x8) ⟶ (x4 = x7 ⟶ ∀ x8 : ο . x8) ⟶ (x5 = x6 ⟶ ∀ x8 : ο . x8) ⟶ (x5 = x7 ⟶ ∀ x8 : ο . x8) ⟶ (x6 = x7 ⟶ ∀ x8 : ο . x8) ⟶ x1) ⟶ x1 (proof)
Definition Subq^Subq := λ x0 x1 . ∀ x2 . x2 ∈ x0 ⟶ x2 ∈ x1
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 setminus^setminus : ι → ι → ι
Definition setprod^setprod := λ x0 x1 . lam x0 (λ x2 . x1)
Param Sing^Sing : ι → ι
Known tuple_2_1_eq^tuple_2_1_eq : ∀ x0 x1 . ap (lam 2 (λ x3 . If_i (x3 = 0) x0 x1)) 1 = x1
Known tuple_2_0_eq^tuple_2_0_eq : ∀ x0 x1 . ap (lam 2 (λ x3 . If_i (x3 = 0) x0 x1)) 0 = x0
Known orIR^orIR : ∀ x0 x1 : ο . x1 ⟶ or x0 x1
Known orIL^orIL : ∀ x0 x1 : ο . x0 ⟶ or x0 x1
Known ap1_Sigma^ap1_Sigma : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ lam x0 x1 ⟶ ap x2 1 ∈ x1 (ap x2 0)
Known setminusE1^setminusE1 : ∀ x0 x1 x2 . x2 ∈ setminus x0 x1 ⟶ x2 ∈ x0
Known ap0_Sigma^ap0_Sigma : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ lam x0 x1 ⟶ ap x2 0 ∈ x0
Definition nIn^nIn := λ x0 x1 . not (x0 ∈ x1)
Known setminusE2^setminusE2 : ∀ x0 x1 x2 . x2 ∈ setminus x0 x1 ⟶ nIn x2 x1
Known SingI^SingI : ∀ x0 . x0 ∈ Sing x0
Known tuple_Sigma_eta^{tuple_Sigma_eta} : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ lam x0 x1 ⟶ lam 2 (λ x4 . If_i (x4 = 0) (ap x2 0) (ap x2 1)) = x2
Known d03c6.. : ∀ x0 . atleastp u4 x0 ⟶ ∀ x1 : ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ (x2 = x3 ⟶ ∀ x6 : ο . x6) ⟶ (x2 = x4 ⟶ ∀ x6 : ο . x6) ⟶ (x2 = x5 ⟶ ∀ x6 : ο . x6) ⟶ (x3 = x4 ⟶ ∀ x6 : ο . x6) ⟶ (x3 = x5 ⟶ ∀ x6 : ο . x6) ⟶ (x4 = x5 ⟶ ∀ x6 : ο . x6) ⟶ x1) ⟶ x1
Theorem 3ebe9.. : ∀ x0 x1 : ι → ι → ι → ι → ο . (∀ x2 x3 x4 x5 . x0 x2 x3 x4 x5 ⟶ x0 x4 x5 x2 x3) ⟶ (∀ x2 . x2 ∈ u6 ⟶ ∀ x3 . x3 ∈ u6 ⟶ not (x0 x2 x3 x2 x3)) ⟶ (∀ x2 . x2 ∈ u6 ⟶ ∀ x3 . x3 ∈ u6 ⟶ x1 x2 x3 x2 x3) ⟶ (∀ x2 . x2 ∈ u6 ⟶ ∀ x3 . x3 ∈ u6 ⟶ ∀ x4 . x4 ∈ u6 ⟶ ∀ x5 . x5 ∈ u6 ⟶ (x2 = u5 ⟶ x3 = u5 ⟶ False) ⟶ (x4 = u5 ⟶ x5 = u5 ⟶ False) ⟶ x0 x2 x3 x4 x5 ⟶ x1 x2 x3 x4 x5) ⟶ (∀ x2 . x2 ∈ u6 ⟶ ∀ x3 . x3 ∈ u6 ⟶ ∀ x4 . x4 ∈ u6 ⟶ ∀ x5 . x5 ∈ u6 ⟶ (x2 = u5 ⟶ x3 = u5 ⟶ False) ⟶ (x4 = u5 ⟶ x5 = u5 ⟶ False) ⟶ (x2 = x4 ⟶ x3 = x5 ⟶ False) ⟶ x1 x2 x3 x4 x5 ⟶ x0 x2 x3 x4 x5) ⟶ (∀ x2 . x2 ∈ u6 ⟶ ∀ x3 . x3 ∈ u6 ⟶ ∀ x4 . x4 ∈ u6 ⟶ ∀ x5 . x5 ∈ u6 ⟶ ∀ x6 . x6 ∈ u6 ⟶ ∀ x7 . x7 ∈ u6 ⟶ ∀ x8 . x8 ∈ u6 ⟶ ∀ x9 . x9 ∈ u6 ⟶ x0 x2 x3 x4 x5 ⟶ x0 x2 x3 x6 x7 ⟶ x0 x2 x3 x8 x9 ⟶ x0 x4 x5 x6 x7 ⟶ x0 x4 x5 x8 x9 ⟶ x0 x6 x7 x8 x9 ⟶ False) ⟶ (∀ x2 . x2 ∈ u6 ⟶ ∀ x3 . x3 ∈ u6 ⟶ ∀ x4 . x4 ∈ u6 ⟶ ∀ x5 . x5 ∈ u6 ⟶ ∀ x6 . x6 ∈ u6 ⟶ ∀ x7 . x7 ∈ u6 ⟶ ∀ x8 . x8 ∈ u6 ⟶ ∀ x9 . x9 ∈ u6 ⟶ ∀ x10 . x10 ∈ u6 ⟶ ∀ x11 . x11 ∈ u6 ⟶ ∀ x12 . x12 ∈ u6 ⟶ ∀ x13 . x13 ∈ u6 ⟶ not (x1 x2 x3 x4 x5) ⟶ not (x1 x2 x3 x6 x7) ⟶ not (x1 x2 x3 x8 x9) ⟶ not (x1 x2 x3 x10 x11) ⟶ not (x1 x2 x3 x12 x13) ⟶ not (x1 x4 x5 x6 x7) ⟶ not (x1 x4 x5 x8 x9) ⟶ not (x1 x4 x5 x10 x11) ⟶ not (x1 x4 x5 x12 x13) ⟶ not (x1 x6 x7 x8 x9) ⟶ not (x1 x6 x7 x10 x11) ⟶ not (x1 x6 x7 x12 x13) ⟶ not (x1 x8 x9 x10 x11) ⟶ not (x1 x8 x9 x12 x13) ⟶ not (x1 x10 x11 x12 x13) ⟶ False) ⟶ not (TwoRamseyProp_atleastp u4 u6 (setminus (setprod u6 u6) (Sing (lam 2 (λ x2 . If_i (x2 = 0) u5 u5))))) (proof)
Param TwoRamseyProp^{TwoRamseyProp} : ι → ι → ι → ο
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
Definition u18 := ordsucc u17
Definition u19 := ordsucc u18
Definition u20 := ordsucc u19
Definition u21 := ordsucc u20
Definition u22 := ordsucc u21
Definition u23 := ordsucc u22
Definition u24 := ordsucc u23
Definition u25 := ordsucc u24
Definition u26 := ordsucc u25
Definition u27 := ordsucc u26
Definition u28 := ordsucc u27
Definition u29 := ordsucc u28
Definition u30 := ordsucc u29
Definition u31 := ordsucc u30
Definition u32 := ordsucc u31
Definition u33 := ordsucc u32
Definition u34 := ordsucc u33
Definition u35 := ordsucc u34
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
Known 46dcf.. : ∀ x0 x1 x2 x3 . atleastp x2 x3 ⟶ TwoRamseyProp x0 x1 x2 ⟶ TwoRamseyProp x0 x1 x3
Param equip^equip : ι → ι → ο
Known equip_atleastp^{equip_atleastp} : ∀ x0 x1 . equip x0 x1 ⟶ atleastp x0 x1
Known equip_sym^equip_sym : ∀ x0 x1 . equip x0 x1 ⟶ equip x1 x0
Known 903ea.. : equip (setminus (setprod u6 u6) (Sing (lam 2 (λ x0 . If_i (x0 = 0) u5 u5)))) u35
Theorem df3e1.. : ∀ x0 x1 : ι → ι → ι → ι → ο . (∀ x2 x3 x4 x5 . x0 x2 x3 x4 x5 ⟶ x0 x4 x5 x2 x3) ⟶ (∀ x2 . x2 ∈ u6 ⟶ ∀ x3 . x3 ∈ u6 ⟶ not (x0 x2 x3 x2 x3)) ⟶ (∀ x2 . x2 ∈ u6 ⟶ ∀ x3 . x3 ∈ u6 ⟶ x1 x2 x3 x2 x3) ⟶ (∀ x2 . x2 ∈ u6 ⟶ ∀ x3 . x3 ∈ u6 ⟶ ∀ x4 . x4 ∈ u6 ⟶ ∀ x5 . x5 ∈ u6 ⟶ (x2 = u5 ⟶ x3 = u5 ⟶ False) ⟶ (x4 = u5 ⟶ x5 = u5 ⟶ False) ⟶ x0 x2 x3 x4 x5 ⟶ x1 x2 x3 x4 x5) ⟶ (∀ x2 . x2 ∈ u6 ⟶ ∀ x3 . x3 ∈ u6 ⟶ ∀ x4 . x4 ∈ u6 ⟶ ∀ x5 . x5 ∈ u6 ⟶ (x2 = u5 ⟶ x3 = u5 ⟶ False) ⟶ (x4 = u5 ⟶ x5 = u5 ⟶ False) ⟶ (x2 = x4 ⟶ x3 = x5 ⟶ False) ⟶ x1 x2 x3 x4 x5 ⟶ x0 x2 x3 x4 x5) ⟶ (∀ x2 . x2 ∈ u6 ⟶ ∀ x3 . x3 ∈ u6 ⟶ ∀ x4 . x4 ∈ u6 ⟶ ∀ x5 . x5 ∈ u6 ⟶ ∀ x6 . x6 ∈ u6 ⟶ ∀ x7 . x7 ∈ u6 ⟶ ∀ x8 . x8 ∈ u6 ⟶ ∀ x9 . x9 ∈ u6 ⟶ x0 x2 x3 x4 x5 ⟶ x0 x2 x3 x6 x7 ⟶ x0 x2 x3 x8 x9 ⟶ x0 x4 x5 x6 x7 ⟶ x0 x4 x5 x8 x9 ⟶ x0 x6 x7 x8 x9 ⟶ False) ⟶ (∀ x2 . x2 ∈ u6 ⟶ ∀ x3 . x3 ∈ u6 ⟶ ∀ x4 . x4 ∈ u6 ⟶ ∀ x5 . x5 ∈ u6 ⟶ ∀ x6 . x6 ∈ u6 ⟶ ∀ x7 . x7 ∈ u6 ⟶ ∀ x8 . x8 ∈ u6 ⟶ ∀ x9 . x9 ∈ u6 ⟶ ∀ x10 . x10 ∈ u6 ⟶ ∀ x11 . x11 ∈ u6 ⟶ ∀ x12 . x12 ∈ u6 ⟶ ∀ x13 . x13 ∈ u6 ⟶ not (x1 x2 x3 x4 x5) ⟶ not (x1 x2 x3 x6 x7) ⟶ not (x1 x2 x3 x8 x9) ⟶ not (x1 x2 x3 x10 x11) ⟶ not (x1 x2 x3 x12 x13) ⟶ not (x1 x4 x5 x6 x7) ⟶ not (x1 x4 x5 x8 x9) ⟶ not (x1 x4 x5 x10 x11) ⟶ not (x1 x4 x5 x12 x13) ⟶ not (x1 x6 x7 x8 x9) ⟶ not (x1 x6 x7 x10 x11) ⟶ not (x1 x6 x7 x12 x13) ⟶ not (x1 x8 x9 x10 x11) ⟶ not (x1 x8 x9 x12 x13) ⟶ not (x1 x10 x11 x12 x13) ⟶ False) ⟶ not (TwoRamseyProp 4 6 35) (proof)