Proofgold Address

Definition or^or := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Definition and^and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Definition In2_lexicographic := λ x0 x1 x2 x3 . or (x1 ∈ x3) (and (x1 = x3) (x0 ∈ x2))
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 94e96.. : ∀ x0 x1 . not (In2_lexicographic 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 65c2b.. : ∀ x0 x1 x2 x3 x4 x5 . TransSet x4 ⟶ TransSet x5 ⟶ In2_lexicographic x0 x1 x2 x3 ⟶ In2_lexicographic x2 x3 x4 x5 ⟶ In2_lexicographic 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
Param TwoRamseyGraph_4_6_35_a : ι → ι → ι → ι → ο
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 67627.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u6 ⟶ ∀ x2 . x2 ∈ u6 ⟶ ∀ x3 . x3 ∈ u6 ⟶ not (TwoRamseyGraph_4_6_35_a x0 x1 x2 x3) ⟶ or (In2_lexicographic x0 x1 x2 x3) (In2_lexicographic x2 x3 x0 x1) (proof)
Known In_0_1^In_0_1 : 0 ∈ 1
Theorem e709e.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u6 ⟶ In2_lexicographic x0 0 x1 u1 (proof)
Known In_0_2^In_0_2 : 0 ∈ 2
Theorem 0d8f3.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u6 ⟶ In2_lexicographic x0 0 x1 u2 (proof)
Known In_1_2^In_1_2 : 1 ∈ 2
Theorem b8306.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u6 ⟶ In2_lexicographic x0 u1 x1 u2 (proof)
Known In_0_3^In_0_3 : 0 ∈ 3
Theorem 27f34.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u6 ⟶ In2_lexicographic x0 0 x1 u3 (proof)
Known In_1_3^In_1_3 : 1 ∈ 3
Theorem 36690.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u6 ⟶ In2_lexicographic x0 u1 x1 u3 (proof)
Known In_2_3^In_2_3 : 2 ∈ 3
Theorem 27a87.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u6 ⟶ In2_lexicographic x0 u2 x1 u3 (proof)
Known In_0_4^In_0_4 : 0 ∈ 4
Theorem 3f697.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u6 ⟶ In2_lexicographic x0 0 x1 u4 (proof)
Known In_1_4^In_1_4 : 1 ∈ 4
Theorem be5f9.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u6 ⟶ In2_lexicographic x0 u1 x1 u4 (proof)
Known In_2_4^In_2_4 : 2 ∈ 4
Theorem 952f7.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u6 ⟶ In2_lexicographic x0 u2 x1 u4 (proof)
Known In_3_4^In_3_4 : 3 ∈ 4
Theorem e60e7.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u6 ⟶ In2_lexicographic x0 u3 x1 u4 (proof)
Known In_0_5^In_0_5 : 0 ∈ 5
Theorem 03171.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u6 ⟶ In2_lexicographic x0 0 x1 u5 (proof)
Known In_1_5^In_1_5 : 1 ∈ 5
Theorem 9750a.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u6 ⟶ In2_lexicographic x0 u1 x1 u5 (proof)
Known In_2_5^In_2_5 : 2 ∈ 5
Theorem f1e9b.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u6 ⟶ In2_lexicographic x0 u2 x1 u5 (proof)
Known In_3_5^In_3_5 : 3 ∈ 5
Theorem b30df.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u6 ⟶ In2_lexicographic x0 u3 x1 u5 (proof)
Known In_4_5^In_4_5 : 4 ∈ 5
Theorem 035bb.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u6 ⟶ In2_lexicographic x0 u4 x1 u5 (proof)
Known In_no2cycle^In_no2cycle : ∀ x0 x1 . x0 ∈ x1 ⟶ x1 ∈ x0 ⟶ False
Theorem 6f0f0.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u6 ⟶ not (In2_lexicographic x0 u1 x1 0) (proof)
Theorem 1b2aa.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u6 ⟶ not (In2_lexicographic x0 u2 x1 0) (proof)
Theorem 829cc.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u6 ⟶ not (In2_lexicographic x0 u3 x1 0) (proof)
Theorem 1c740.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u6 ⟶ not (In2_lexicographic x0 u4 x1 0) (proof)
Theorem 196b9.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u6 ⟶ not (In2_lexicographic x0 u5 x1 0) (proof)
Theorem 97a37.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u6 ⟶ not (In2_lexicographic x0 u2 x1 u1) (proof)
Theorem b27e1.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u6 ⟶ not (In2_lexicographic x0 u3 x1 u1) (proof)
Theorem 52c59.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u6 ⟶ not (In2_lexicographic x0 u4 x1 u1) (proof)
Theorem 2efb1.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u6 ⟶ not (In2_lexicographic x0 u5 x1 u1) (proof)
Theorem 696a1.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u6 ⟶ not (In2_lexicographic x0 u3 x1 u2) (proof)
Theorem dd794.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u6 ⟶ not (In2_lexicographic x0 u4 x1 u2) (proof)
Theorem dd382.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u6 ⟶ not (In2_lexicographic x0 u5 x1 u2) (proof)
Theorem ffa46.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u6 ⟶ not (In2_lexicographic x0 u4 x1 u3) (proof)
Theorem e28f6.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u6 ⟶ not (In2_lexicographic x0 u5 x1 u3) (proof)
Theorem 1f4d3.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u6 ⟶ not (In2_lexicographic x0 u5 x1 u4) (proof)
Theorem 0b098.. : ∀ x0 . x0 ∈ u6 ⟶ In2_lexicographic 0 x0 u1 x0 (proof)
Theorem 5e815.. : ∀ x0 . x0 ∈ u6 ⟶ In2_lexicographic 0 x0 u2 x0 (proof)
Theorem 6bdbd.. : ∀ x0 . x0 ∈ u6 ⟶ In2_lexicographic u1 x0 u2 x0 (proof)
Theorem 0b5bd.. : ∀ x0 . x0 ∈ u6 ⟶ In2_lexicographic 0 x0 u3 x0 (proof)
Theorem d2a78.. : ∀ x0 . x0 ∈ u6 ⟶ In2_lexicographic u1 x0 u3 x0 (proof)
Theorem 07268.. : ∀ x0 . x0 ∈ u6 ⟶ In2_lexicographic u2 x0 u3 x0 (proof)
Theorem e04f2.. : ∀ x0 . x0 ∈ u6 ⟶ In2_lexicographic 0 x0 u4 x0 (proof)
Theorem e1002.. : ∀ x0 . x0 ∈ u6 ⟶ In2_lexicographic u1 x0 u4 x0 (proof)
Theorem 58234.. : ∀ x0 . x0 ∈ u6 ⟶ In2_lexicographic u2 x0 u4 x0 (proof)
Theorem b7796.. : ∀ x0 . x0 ∈ u6 ⟶ In2_lexicographic u3 x0 u4 x0 (proof)
Theorem 6fa01.. : ∀ x0 . x0 ∈ u6 ⟶ In2_lexicographic 0 x0 u5 x0 (proof)
Theorem 740f5.. : ∀ x0 . x0 ∈ u6 ⟶ In2_lexicographic u1 x0 u5 x0 (proof)
Theorem 90d47.. : ∀ x0 . x0 ∈ u6 ⟶ In2_lexicographic u2 x0 u5 x0 (proof)
Theorem 0a7a8.. : ∀ x0 . x0 ∈ u6 ⟶ In2_lexicographic u3 x0 u5 x0 (proof)
Theorem bb6fa.. : ∀ x0 . x0 ∈ u6 ⟶ In2_lexicographic u4 x0 u5 x0 (proof)
Theorem b5ca8.. : ∀ x0 . x0 ∈ u6 ⟶ not (In2_lexicographic 0 x0 0 x0) (proof)
Theorem 15042.. : ∀ x0 . x0 ∈ u6 ⟶ not (In2_lexicographic u1 x0 0 x0) (proof)
Theorem 4ed6e.. : ∀ x0 . x0 ∈ u6 ⟶ not (In2_lexicographic u2 x0 0 x0) (proof)
Theorem aa680.. : ∀ x0 . x0 ∈ u6 ⟶ not (In2_lexicographic u3 x0 0 x0) (proof)
Theorem be2c5.. : ∀ x0 . x0 ∈ u6 ⟶ not (In2_lexicographic u4 x0 0 x0) (proof)
Theorem fb400.. : ∀ x0 . x0 ∈ u6 ⟶ not (In2_lexicographic u5 x0 0 x0) (proof)
Theorem 69e13.. : ∀ x0 . x0 ∈ u6 ⟶ not (In2_lexicographic u1 x0 u1 x0) (proof)
Theorem b695a.. : ∀ x0 . x0 ∈ u6 ⟶ not (In2_lexicographic u2 x0 u1 x0) (proof)
Theorem e7d59.. : ∀ x0 . x0 ∈ u6 ⟶ not (In2_lexicographic u3 x0 u1 x0) (proof)
Theorem a3e6e.. : ∀ x0 . x0 ∈ u6 ⟶ not (In2_lexicographic u4 x0 u1 x0) (proof)
Theorem dadcc.. : ∀ x0 . x0 ∈ u6 ⟶ not (In2_lexicographic u5 x0 u1 x0) (proof)
Theorem 05e9c.. : ∀ x0 . x0 ∈ u6 ⟶ not (In2_lexicographic u2 x0 u2 x0) (proof)
Theorem a73b8.. : ∀ x0 . x0 ∈ u6 ⟶ not (In2_lexicographic u3 x0 u2 x0) (proof)
Theorem b6f90.. : ∀ x0 . x0 ∈ u6 ⟶ not (In2_lexicographic u4 x0 u2 x0) (proof)
Theorem 6bc25.. : ∀ x0 . x0 ∈ u6 ⟶ not (In2_lexicographic u5 x0 u2 x0) (proof)
Theorem 52f87.. : ∀ x0 . x0 ∈ u6 ⟶ not (In2_lexicographic u3 x0 u3 x0) (proof)
Theorem dc51f.. : ∀ x0 . x0 ∈ u6 ⟶ not (In2_lexicographic u4 x0 u3 x0) (proof)
Theorem 447d5.. : ∀ x0 . x0 ∈ u6 ⟶ not (In2_lexicographic u5 x0 u3 x0) (proof)
Theorem a58bd.. : ∀ x0 . x0 ∈ u6 ⟶ not (In2_lexicographic u4 x0 u4 x0) (proof)
Theorem 2313b.. : ∀ x0 . x0 ∈ u6 ⟶ not (In2_lexicographic u5 x0 u4 x0) (proof)
Theorem 56b5c.. : ∀ x0 . x0 ∈ u6 ⟶ not (In2_lexicographic u5 x0 u5 x0) (proof)