Proofgold Address

Definition or^or := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Definition and^and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Definition 5fab1.. := λ x0 x1 x2 x3 . or (x0 ∈ x2) (and (x0 = x2) (x1 ∈ x3))
Definition False^False := ∀ x0 : ο . x0
Definition not^not := λ x0 : ο . x0 ⟶ False
Definition nIn^nIn := λ x0 x1 . not (x0 ∈ x1)
Known In_irref^In_irref : ∀ x0 . nIn x0 x0
Theorem 6c980.. : ∀ x0 x1 . not (5fab1.. x0 x1 x0 x1) (proof)
Definition Subq^Subq := λ x0 x1 . ∀ x2 . x2 ∈ x0 ⟶ x2 ∈ x1
Definition TransSet^TransSet := λ x0 . ∀ x1 . x1 ∈ x0 ⟶ x1 ⊆ x0
Known orIL^orIL : ∀ x0 x1 : ο . x0 ⟶ or x0 x1
Known orIR^orIR : ∀ x0 x1 : ο . x1 ⟶ or x0 x1
Known andI^andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Theorem 783a2.. : ∀ x0 x1 x2 x3 x4 x5 . TransSet x4 ⟶ TransSet x5 ⟶ 5fab1.. x0 x1 x2 x3 ⟶ 5fab1.. x2 x3 x4 x5 ⟶ 5fab1.. x0 x1 x4 x5 (proof)
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 TwoRamseyGraph_4_6_Church6_squared_a := λ x0 x1 x2 x3 : ι → ι → ι → ι → ι → ι → ι . λ x4 x5 . x0 (x1 (x2 (x3 x4 x5 x4 x5 x4 x5) (x3 x4 x4 x5 x5 x4 x5) (x3 x5 x5 x4 x4 x4 x5) (x3 x5 x4 x4 x5 x4 x5) (x3 x5 x5 x4 x4 x5 x5) (x3 x4 x5 x4 x4 x5 x4)) (x2 (x3 x5 x4 x5 x4 x5 x4) (x3 x4 x4 x5 x5 x5 x4) (x3 x5 x5 x4 x4 x5 x4) (x3 x4 x5 x5 x4 x5 x4) (x3 x5 x5 x4 x4 x5 x5) (x3 x5 x4 x4 x4 x5 x4)) (x2 (x3 x4 x5 x4 x5 x5 x4) (x3 x5 x5 x4 x4 x4 x5) (x3 x4 x4 x5 x5 x4 x5) (x3 x4 x5 x5 x4 x5 x4) (x3 x4 x4 x5 x5 x5 x5) (x3 x4 x4 x4 x5 x5 x4)) (x2 (x3 x5 x4 x5 x4 x4 x5) (x3 x5 x5 x4 x4 x5 x4) (x3 x4 x4 x5 x5 x5 x4) (x3 x5 x4 x4 x5 x4 x5) (x3 x4 x4 x5 x5 x5 x5) (x3 x4 x4 x5 x4 x5 x4)) (x2 (x3 x4 x5 x5 x4 x4 x5) (x3 x5 x4 x4 x5 x5 x5) (x3 x4 x5 x5 x4 x4 x4) (x3 x4 x5 x5 x4 x4 x4) (x3 x5 x4 x4 x5 x5 x5) (x3 x5 x5 x5 x5 x4 x4)) (x2 (x3 x5 x4 x4 x5 x5 x4) (x3 x4 x5 x5 x4 x5 x5) (x3 x5 x4 x4 x5 x4 x4) (x3 x5 x4 x4 x5 x4 x4) (x3 x4 x5 x5 x4 x5 x5) (x3 x5 x5 x5 x5 x4 x4))) (x1 (x2 (x3 x4 x4 x5 x5 x5 x4) (x3 x4 x5 x4 x5 x5 x4) (x3 x4 x5 x5 x5 x4 x5) (x3 x5 x4 x4 x4 x4 x5) (x3 x5 x4 x4 x5 x5 x4) (x3 x5 x4 x5 x5 x5 x4)) (x2 (x3 x4 x4 x5 x5 x4 x5) (x3 x5 x4 x5 x4 x4 x5) (x3 x5 x4 x5 x5 x5 x4) (x3 x4 x5 x4 x4 x5 x4) (x3 x4 x5 x5 x4 x4 x5) (x3 x4 x5 x5 x5 x5 x4)) (x2 (x3 x5 x5 x4 x4 x4 x5) (x3 x4 x5 x4 x5 x5 x4) (x3 x5 x5 x4 x5 x4 x5) (x3 x4 x4 x5 x4 x5 x4) (x3 x4 x5 x5 x4 x5 x4) (x3 x5 x5 x5 x4 x5 x4)) (x2 (x3 x5 x5 x4 x4 x5 x4) (x3 x5 x4 x5 x4 x4 x5) (x3 x5 x5 x5 x4 x5 x4) (x3 x4 x4 x4 x5 x4 x5) (x3 x5 x4 x4 x5 x4 x5) (x3 x5 x5 x4 x5 x5 x4)) (x2 (x3 x4 x5 x4 x5 x5 x5) (x3 x5 x4 x5 x4 x4 x4) (x3 x5 x4 x5 x4 x5 x5) (x3 x5 x5 x5 x5 x4 x4) (x3 x5 x5 x5 x5 x5 x4) (x3 x5 x4 x5 x4 x4 x4)) (x2 (x3 x5 x4 x5 x4 x5 x5) (x3 x4 x5 x4 x5 x4 x4) (x3 x4 x5 x4 x5 x5 x5) (x3 x5 x5 x5 x5 x4 x4) (x3 x5 x5 x5 x5 x4 x5) (x3 x4 x5 x4 x5 x4 x4))) (x1 (x2 (x3 x5 x5 x4 x4 x4 x5) (x3 x4 x5 x5 x5 x5 x4) (x3 x4 x4 x5 x5 x4 x5) (x3 x5 x4 x4 x5 x5 x4) (x3 x5 x5 x4 x4 x5 x5) (x3 x5 x5 x4 x5 x4 x4)) (x2 (x3 x5 x5 x4 x4 x5 x4) (x3 x5 x4 x5 x5 x4 x5) (x3 x4 x4 x5 x5 x5 x4) (x3 x4 x5 x5 x4 x4 x5) (x3 x5 x5 x4 x4 x5 x5) (x3 x5 x5 x5 x4 x4 x4)) (x2 (x3 x4 x4 x5 x5 x5 x4) (x3 x5 x5 x4 x5 x5 x4) (x3 x5 x5 x4 x4 x4 x5) (x3 x4 x5 x5 x4 x4 x5) (x3 x4 x4 x5 x5 x5 x5) (x3 x4 x5 x5 x5 x4 x4)) (x2 (x3 x4 x4 x5 x5 x4 x5) (x3 x5 x5 x5 x4 x4 x5) (x3 x5 x5 x4 x4 x5 x4) (x3 x5 x4 x4 x5 x5 x4) (x3 x4 x4 x5 x5 x5 x5) (x3 x5 x4 x5 x5 x4 x4)) (x2 (x3 x4 x5 x4 x5 x4 x4) (x3 x4 x5 x4 x5 x5 x5) (x3 x4 x5 x4 x5 x4 x4) (x3 x5 x5 x5 x5 x5 x5) (x3 x5 x4 x5 x4 x5 x5) (x3 x5 x5 x5 x5 x5 x4)) (x2 (x3 x5 x4 x5 x4 x4 x4) (x3 x5 x4 x5 x4 x5 x5) (x3 x5 x4 x5 x4 x4 x4) (x3 x5 x5 x5 x5 x5 x5) (x3 x4 x5 x4 x5 x5 x5) (x3 x5 x5 x5 x5 x5 x4))) (x1 (x2 (x3 x5 x4 x4 x5 x4 x5) (x3 x5 x4 x4 x4 x5 x5) (x3 x5 x4 x4 x5 x5 x5) (x3 x4 x4 x5 x5 x4 x5) (x3 x5 x5 x4 x5 x5 x4) (x3 x4 x4 x5 x5 x4 x4)) (x2 (x3 x4 x5 x5 x4 x5 x4) (x3 x4 x5 x4 x4 x5 x5) (x3 x4 x5 x5 x4 x5 x5) (x3 x4 x4 x5 x5 x5 x4) (x3 x5 x5 x5 x4 x4 x5) (x3 x4 x4 x5 x5 x4 x4)) (x2 (x3 x4 x5 x5 x4 x5 x4) (x3 x4 x4 x5 x4 x5 x5) (x3 x4 x5 x5 x4 x5 x5) (x3 x5 x5 x4 x4 x5 x4) (x3 x4 x5 x5 x5 x5 x4) (x3 x5 x5 x4 x4 x4 x4)) (x2 (x3 x5 x4 x4 x5 x4 x5) (x3 x4 x4 x4 x5 x5 x5) (x3 x5 x4 x4 x5 x5 x5) (x3 x5 x5 x4 x4 x4 x5) (x3 x5 x4 x5 x5 x4 x5) (x3 x5 x5 x4 x4 x4 x4)) (x2 (x3 x4 x5 x5 x4 x4 x4) (x3 x4 x5 x5 x4 x4 x4) (x3 x5 x4 x4 x5 x5 x5) (x3 x4 x5 x5 x4 x4 x5) (x3 x5 x5 x5 x5 x5 x5) (x3 x5 x4 x4 x5 x5 x4)) (x2 (x3 x5 x4 x4 x5 x4 x4) (x3 x5 x4 x4 x5 x4 x4) (x3 x4 x5 x5 x4 x5 x5) (x3 x5 x4 x4 x5 x5 x4) (x3 x5 x5 x5 x5 x5 x5) (x3 x4 x5 x5 x4 x5 x4))) (x1 (x2 (x3 x5 x5 x4 x4 x5 x4) (x3 x5 x4 x4 x5 x5 x5) (x3 x5 x5 x4 x4 x5 x4) (x3 x5 x5 x4 x5 x5 x5) (x3 x4 x5 x4 x4 x5 x4) (x3 x4 x4 x5 x5 x5 x4)) (x2 (x3 x5 x5 x4 x4 x4 x5) (x3 x4 x5 x5 x4 x5 x5) (x3 x5 x5 x4 x4 x4 x5) (x3 x5 x5 x5 x4 x5 x5) (x3 x5 x4 x4 x4 x4 x5) (x3 x4 x4 x5 x5 x5 x4)) (x2 (x3 x4 x4 x5 x5 x4 x5) (x3 x4 x5 x5 x4 x5 x5) (x3 x4 x4 x5 x5 x5 x4) (x3 x4 x5 x5 x5 x5 x5) (x3 x4 x4 x4 x5 x5 x4) (x3 x5 x5 x4 x4 x5 x4)) (x2 (x3 x4 x4 x5 x5 x5 x4) (x3 x5 x4 x4 x5 x5 x5) (x3 x4 x4 x5 x5 x4 x5) (x3 x5 x4 x5 x5 x5 x5) (x3 x4 x4 x5 x4 x4 x5) (x3 x5 x5 x4 x4 x5 x4)) (x2 (x3 x5 x5 x5 x5 x5 x5) (x3 x5 x4 x5 x4 x5 x4) (x3 x5 x5 x5 x5 x5 x5) (x3 x5 x4 x5 x4 x5 x5) (x3 x5 x4 x5 x4 x4 x5) (x3 x4 x4 x4 x4 x4 x4)) (x2 (x3 x5 x5 x5 x5 x5 x5) (x3 x4 x5 x4 x5 x4 x5) (x3 x5 x5 x5 x5 x5 x5) (x3 x4 x5 x4 x5 x5 x5) (x3 x4 x5 x4 x5 x5 x4) (x3 x4 x4 x4 x4 x4 x4))) (x1 (x2 (x3 x4 x5 x4 x4 x5 x5) (x3 x5 x4 x5 x5 x5 x4) (x3 x5 x5 x4 x5 x5 x5) (x3 x4 x4 x5 x5 x5 x4) (x3 x4 x4 x5 x5 x4 x4) (x3 x4 x5 x5 x4 x5 x4)) (x2 (x3 x5 x4 x4 x4 x5 x5) (x3 x4 x5 x5 x5 x4 x5) (x3 x5 x5 x5 x4 x5 x5) (x3 x4 x4 x5 x5 x4 x5) (x3 x4 x4 x5 x5 x4 x4) (x3 x5 x4 x4 x5 x5 x4)) (x2 (x3 x4 x4 x4 x5 x5 x5) (x3 x5 x5 x5 x4 x5 x4) (x3 x4 x5 x5 x5 x5 x5) (x3 x5 x5 x4 x4 x4 x5) (x3 x5 x5 x4 x4 x4 x4) (x3 x5 x4 x4 x5 x5 x4)) (x2 (x3 x4 x4 x5 x4 x5 x5) (x3 x5 x5 x4 x5 x4 x5) (x3 x5 x4 x5 x5 x5 x5) (x3 x5 x5 x4 x4 x5 x4) (x3 x5 x5 x4 x4 x4 x4) (x3 x4 x5 x5 x4 x5 x4)) (x2 (x3 x5 x5 x5 x5 x4 x4) (x3 x5 x5 x5 x5 x4 x4) (x3 x4 x4 x4 x4 x5 x5) (x3 x4 x4 x4 x4 x5 x5) (x3 x5 x5 x5 x5 x4 x4) (x3 x5 x5 x5 x5 x4 x4)) (x2 (x3 x4 x4 x4 x4 x4 x4) (x3 x4 x4 x4 x4 x4 x4) (x3 x4 x4 x4 x4 x4 x4) (x3 x4 x4 x4 x4 x4 x4) (x3 x4 x4 x4 x4 x4 x4) (x3 x4 x4 x4 x4 x4 x4)))
Param nth_6_tuple : ι → ι → ι → ι → ι → ι → ι → ι
Definition TwoRamseyGraph_4_6_35_a := λ x0 x1 x2 x3 . TwoRamseyGraph_4_6_Church6_squared_a (nth_6_tuple x0) (nth_6_tuple x1) (nth_6_tuple x2) (nth_6_tuple x3) = λ x5 x6 . x5
Param ordinal^ordinal : ι → ο
Known ordinal_trichotomy_or_impred^{ordinal_trichotomy_or_impred} : ∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ ∀ x2 : ο . (x0 ∈ x1 ⟶ x2) ⟶ (x0 = x1 ⟶ x2) ⟶ (x1 ∈ x0 ⟶ x2) ⟶ x2
Known FalseE^FalseE : False ⟶ ∀ x0 : ο . x0
Known dd650.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u6 ⟶ TwoRamseyGraph_4_6_35_a x0 x1 x0 x1
Param nat_p^nat_p : ι → ο
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_6^nat_6 : nat_p 6
Theorem 6e6b6.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u6 ⟶ ∀ x2 . x2 ∈ u6 ⟶ ∀ x3 . x3 ∈ u6 ⟶ not (TwoRamseyGraph_4_6_35_a x0 x1 x2 x3) ⟶ or (5fab1.. x0 x1 x2 x3) (5fab1.. x2 x3 x0 x1) (proof)
Known In_0_1^In_0_1 : 0 ∈ 1
Theorem 952a3.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u6 ⟶ 5fab1.. 0 x0 u1 x1 (proof)
Known In_0_2^In_0_2 : 0 ∈ 2
Theorem 0bf10.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u6 ⟶ 5fab1.. 0 x0 u2 x1 (proof)
Known In_1_2^In_1_2 : 1 ∈ 2
Theorem be78a.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u6 ⟶ 5fab1.. u1 x0 u2 x1 (proof)
Known In_0_3^In_0_3 : 0 ∈ 3
Theorem 695f7.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u6 ⟶ 5fab1.. 0 x0 u3 x1 (proof)
Known In_1_3^In_1_3 : 1 ∈ 3
Theorem 21a98.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u6 ⟶ 5fab1.. u1 x0 u3 x1 (proof)
Known In_2_3^In_2_3 : 2 ∈ 3
Theorem 938fd.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u6 ⟶ 5fab1.. u2 x0 u3 x1 (proof)
Known In_0_4^In_0_4 : 0 ∈ 4
Theorem cc19c.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u6 ⟶ 5fab1.. 0 x0 u4 x1 (proof)
Known In_1_4^In_1_4 : 1 ∈ 4
Theorem 9e4a0.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u6 ⟶ 5fab1.. u1 x0 u4 x1 (proof)
Known In_2_4^In_2_4 : 2 ∈ 4
Theorem 663cd.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u6 ⟶ 5fab1.. u2 x0 u4 x1 (proof)
Known In_3_4^In_3_4 : 3 ∈ 4
Theorem 1bd57.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u6 ⟶ 5fab1.. u3 x0 u4 x1 (proof)
Known In_0_5^In_0_5 : 0 ∈ 5
Theorem 15d0d.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u6 ⟶ 5fab1.. 0 x0 u5 x1 (proof)
Known In_1_5^In_1_5 : 1 ∈ 5
Theorem e87d5.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u6 ⟶ 5fab1.. u1 x0 u5 x1 (proof)
Known In_2_5^In_2_5 : 2 ∈ 5
Theorem 8a4c6.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u6 ⟶ 5fab1.. u2 x0 u5 x1 (proof)
Known In_3_5^In_3_5 : 3 ∈ 5
Theorem b05ce.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u6 ⟶ 5fab1.. u3 x0 u5 x1 (proof)
Known In_4_5^In_4_5 : 4 ∈ 5
Theorem 8c8c2.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u6 ⟶ 5fab1.. u4 x0 u5 x1 (proof)
Known In_no2cycle^In_no2cycle : ∀ x0 x1 . x0 ∈ x1 ⟶ x1 ∈ x0 ⟶ False
Theorem c3b75.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u6 ⟶ not (5fab1.. u1 x0 0 x1) (proof)
Theorem cb619.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u6 ⟶ not (5fab1.. u2 x0 0 x1) (proof)
Theorem 4a2be.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u6 ⟶ not (5fab1.. u3 x0 0 x1) (proof)
Theorem bfb87.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u6 ⟶ not (5fab1.. u4 x0 0 x1) (proof)
Theorem 3a4b3.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u6 ⟶ not (5fab1.. u5 x0 0 x1) (proof)
Theorem 97337.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u6 ⟶ not (5fab1.. u2 x0 u1 x1) (proof)
Theorem 5b609.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u6 ⟶ not (5fab1.. u3 x0 u1 x1) (proof)
Theorem a4c20.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u6 ⟶ not (5fab1.. u4 x0 u1 x1) (proof)
Theorem 05944.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u6 ⟶ not (5fab1.. u5 x0 u1 x1) (proof)
Theorem a5181.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u6 ⟶ not (5fab1.. u3 x0 u2 x1) (proof)
Theorem 2f248.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u6 ⟶ not (5fab1.. u4 x0 u2 x1) (proof)
Theorem fcb65.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u6 ⟶ not (5fab1.. u5 x0 u2 x1) (proof)
Theorem adc16.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u6 ⟶ not (5fab1.. u4 x0 u3 x1) (proof)
Theorem 8a34d.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u6 ⟶ not (5fab1.. u5 x0 u3 x1) (proof)
Theorem d5869.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u6 ⟶ not (5fab1.. u5 x0 u4 x1) (proof)
Theorem c2374.. : ∀ x0 . x0 ∈ u6 ⟶ 5fab1.. x0 0 x0 u1 (proof)
Theorem 75bff.. : ∀ x0 . x0 ∈ u6 ⟶ 5fab1.. x0 0 x0 u2 (proof)
Theorem 875a5.. : ∀ x0 . x0 ∈ u6 ⟶ 5fab1.. x0 u1 x0 u2 (proof)
Theorem 2bf26.. : ∀ x0 . x0 ∈ u6 ⟶ 5fab1.. x0 0 x0 u3 (proof)
Theorem 1cab7.. : ∀ x0 . x0 ∈ u6 ⟶ 5fab1.. x0 u1 x0 u3 (proof)
Theorem 86ea6.. : ∀ x0 . x0 ∈ u6 ⟶ 5fab1.. x0 u2 x0 u3 (proof)
Theorem 86f2e.. : ∀ x0 . x0 ∈ u6 ⟶ 5fab1.. x0 0 x0 u4 (proof)
Theorem c8ace.. : ∀ x0 . x0 ∈ u6 ⟶ 5fab1.. x0 u1 x0 u4 (proof)
Theorem 12360.. : ∀ x0 . x0 ∈ u6 ⟶ 5fab1.. x0 u2 x0 u4 (proof)
Theorem a409f.. : ∀ x0 . x0 ∈ u6 ⟶ 5fab1.. x0 u3 x0 u4 (proof)
Theorem 67cca.. : ∀ x0 . x0 ∈ u6 ⟶ 5fab1.. x0 0 x0 u5 (proof)
Theorem 153b7.. : ∀ x0 . x0 ∈ u6 ⟶ 5fab1.. x0 u1 x0 u5 (proof)
Theorem 95c3f.. : ∀ x0 . x0 ∈ u6 ⟶ 5fab1.. x0 u2 x0 u5 (proof)
Theorem 3aa97.. : ∀ x0 . x0 ∈ u6 ⟶ 5fab1.. x0 u3 x0 u5 (proof)
Theorem 0c8db.. : ∀ x0 . x0 ∈ u6 ⟶ 5fab1.. x0 u4 x0 u5 (proof)
Theorem a7820.. : ∀ x0 . x0 ∈ u6 ⟶ not (5fab1.. x0 0 x0 0) (proof)
Theorem c2f7f.. : ∀ x0 . x0 ∈ u6 ⟶ not (5fab1.. x0 u1 x0 0) (proof)
Theorem 4902e.. : ∀ x0 . x0 ∈ u6 ⟶ not (5fab1.. x0 u2 x0 0) (proof)
Theorem 0c398.. : ∀ x0 . x0 ∈ u6 ⟶ not (5fab1.. x0 u3 x0 0) (proof)
Theorem 6ad4c.. : ∀ x0 . x0 ∈ u6 ⟶ not (5fab1.. x0 u4 x0 0) (proof)
Theorem f33f9.. : ∀ x0 . x0 ∈ u6 ⟶ not (5fab1.. x0 u5 x0 0) (proof)
Theorem 659dc.. : ∀ x0 . x0 ∈ u6 ⟶ not (5fab1.. x0 u1 x0 u1) (proof)
Theorem 65f34.. : ∀ x0 . x0 ∈ u6 ⟶ not (5fab1.. x0 u2 x0 u1) (proof)
Theorem 5dff1.. : ∀ x0 . x0 ∈ u6 ⟶ not (5fab1.. x0 u3 x0 u1) (proof)
Theorem ad774.. : ∀ x0 . x0 ∈ u6 ⟶ not (5fab1.. x0 u4 x0 u1) (proof)
Theorem 5776b.. : ∀ x0 . x0 ∈ u6 ⟶ not (5fab1.. x0 u5 x0 u1) (proof)
Theorem 3fb7d.. : ∀ x0 . x0 ∈ u6 ⟶ not (5fab1.. x0 u2 x0 u2) (proof)
Theorem d5175.. : ∀ x0 . x0 ∈ u6 ⟶ not (5fab1.. x0 u3 x0 u2) (proof)
Theorem 9225d.. : ∀ x0 . x0 ∈ u6 ⟶ not (5fab1.. x0 u4 x0 u2) (proof)
Theorem 5a216.. : ∀ x0 . x0 ∈ u6 ⟶ not (5fab1.. x0 u5 x0 u2) (proof)
Theorem 99a85.. : ∀ x0 . x0 ∈ u6 ⟶ not (5fab1.. x0 u3 x0 u3) (proof)
Theorem cde57.. : ∀ x0 . x0 ∈ u6 ⟶ not (5fab1.. x0 u4 x0 u3) (proof)
Theorem f8c71.. : ∀ x0 . x0 ∈ u6 ⟶ not (5fab1.. x0 u5 x0 u3) (proof)
Theorem e8b66.. : ∀ x0 . x0 ∈ u6 ⟶ not (5fab1.. x0 u4 x0 u4) (proof)
Theorem da55d.. : ∀ x0 . x0 ∈ u6 ⟶ not (5fab1.. x0 u5 x0 u4) (proof)
Theorem ab59c.. : ∀ x0 . x0 ∈ u6 ⟶ not (5fab1.. x0 u5 x0 u5) (proof)
Known 33924.. : nth_6_tuple u4 = λ x1 x2 x3 x4 x5 x6 . x5
Known fed6d.. : nth_6_tuple u5 = λ x1 x2 x3 x4 x5 x6 . x6
Known cases_6^cases_6 : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 : ι → ο . x1 0 ⟶ x1 u1 ⟶ x1 u2 ⟶ x1 u3 ⟶ x1 u4 ⟶ x1 u5 ⟶ x1 x0
Known a1243.. : nth_6_tuple 0 = λ x1 x2 x3 x4 x5 x6 . x1
Known a7cad.. : nth_6_tuple u1 = λ x1 x2 x3 x4 x5 x6 . x2
Known a0d60.. : nth_6_tuple u2 = λ x1 x2 x3 x4 x5 x6 . x3
Known 89684.. : nth_6_tuple u3 = λ x1 x2 x3 x4 x5 x6 . x4
Theorem 2e599.. : ∀ x0 . x0 ∈ u6 ⟶ TwoRamseyGraph_4_6_35_a u4 u4 u5 x0 (proof)
Theorem ff9a1.. : ∀ x0 . x0 ∈ u6 ⟶ TwoRamseyGraph_4_6_35_a u4 u5 u5 x0 (proof)