Proofgold Address

Definition and^and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Param Subq^Subq : ι → ι → ο
Param atleastp^atleastp : ι → ι → ο
Param ordsucc^ordsucc : ι → ι
Definition False^False := ∀ x0 : ο . x0
Definition not^not := λ x0 : ο . x0 ⟶ False
Known andI^andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Known a6a5a.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 . (∀ x9 . x9 ∈ x8 ⟶ ∀ x10 : ι → ο . x10 x0 ⟶ x10 x1 ⟶ x10 x2 ⟶ x10 x3 ⟶ x10 x4 ⟶ x10 x5 ⟶ x10 x6 ⟶ x10 x7 ⟶ x10 x9) ⟶ ∀ x9 . x9 ⊆ x8 ⟶ atleastp 3 x9 ⟶ ∀ x10 : ο . (x0 ∈ x9 ⟶ x1 ∈ x9 ⟶ x2 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x1 ∈ x9 ⟶ x3 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x2 ∈ x9 ⟶ x3 ∈ x9 ⟶ x10) ⟶ (x1 ∈ x9 ⟶ x2 ∈ x9 ⟶ x3 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x1 ∈ x9 ⟶ x4 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x2 ∈ x9 ⟶ x4 ∈ x9 ⟶ x10) ⟶ (x1 ∈ x9 ⟶ x2 ∈ x9 ⟶ x4 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x3 ∈ x9 ⟶ x4 ∈ x9 ⟶ x10) ⟶ (x1 ∈ x9 ⟶ x3 ∈ x9 ⟶ x4 ∈ x9 ⟶ x10) ⟶ (x2 ∈ x9 ⟶ x3 ∈ x9 ⟶ x4 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x1 ∈ x9 ⟶ x5 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x2 ∈ x9 ⟶ x5 ∈ x9 ⟶ x10) ⟶ (x1 ∈ x9 ⟶ x2 ∈ x9 ⟶ x5 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x3 ∈ x9 ⟶ x5 ∈ x9 ⟶ x10) ⟶ (x1 ∈ x9 ⟶ x3 ∈ x9 ⟶ x5 ∈ x9 ⟶ x10) ⟶ (x2 ∈ x9 ⟶ x3 ∈ x9 ⟶ x5 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x4 ∈ x9 ⟶ x5 ∈ x9 ⟶ x10) ⟶ (x1 ∈ x9 ⟶ x4 ∈ x9 ⟶ x5 ∈ x9 ⟶ x10) ⟶ (x2 ∈ x9 ⟶ x4 ∈ x9 ⟶ x5 ∈ x9 ⟶ x10) ⟶ (x3 ∈ x9 ⟶ x4 ∈ x9 ⟶ x5 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x1 ∈ x9 ⟶ x6 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x2 ∈ x9 ⟶ x6 ∈ x9 ⟶ x10) ⟶ (x1 ∈ x9 ⟶ x2 ∈ x9 ⟶ x6 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x3 ∈ x9 ⟶ x6 ∈ x9 ⟶ x10) ⟶ (x1 ∈ x9 ⟶ x3 ∈ x9 ⟶ x6 ∈ x9 ⟶ x10) ⟶ (x2 ∈ x9 ⟶ x3 ∈ x9 ⟶ x6 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x4 ∈ x9 ⟶ x6 ∈ x9 ⟶ x10) ⟶ (x1 ∈ x9 ⟶ x4 ∈ x9 ⟶ x6 ∈ x9 ⟶ x10) ⟶ (x2 ∈ x9 ⟶ x4 ∈ x9 ⟶ x6 ∈ x9 ⟶ x10) ⟶ (x3 ∈ x9 ⟶ x4 ∈ x9 ⟶ x6 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x5 ∈ x9 ⟶ x6 ∈ x9 ⟶ x10) ⟶ (x1 ∈ x9 ⟶ x5 ∈ x9 ⟶ x6 ∈ x9 ⟶ x10) ⟶ (x2 ∈ x9 ⟶ x5 ∈ x9 ⟶ x6 ∈ x9 ⟶ x10) ⟶ (x3 ∈ x9 ⟶ x5 ∈ x9 ⟶ x6 ∈ x9 ⟶ x10) ⟶ (x4 ∈ x9 ⟶ x5 ∈ x9 ⟶ x6 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x1 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x2 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x1 ∈ x9 ⟶ x2 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x3 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x1 ∈ x9 ⟶ x3 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x2 ∈ x9 ⟶ x3 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x4 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x1 ∈ x9 ⟶ x4 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x2 ∈ x9 ⟶ x4 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x3 ∈ x9 ⟶ x4 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x5 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x1 ∈ x9 ⟶ x5 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x2 ∈ x9 ⟶ x5 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x3 ∈ x9 ⟶ x5 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x4 ∈ x9 ⟶ x5 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x6 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x1 ∈ x9 ⟶ x6 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x2 ∈ x9 ⟶ x6 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x3 ∈ x9 ⟶ x6 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x4 ∈ x9 ⟶ x6 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x5 ∈ x9 ⟶ x6 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ x10
Known c14f6.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 . (∀ x9 . x9 ∈ x8 ⟶ ∀ x10 : ι → ο . x10 x0 ⟶ x10 x1 ⟶ x10 x2 ⟶ x10 x3 ⟶ x10 x4 ⟶ x10 x5 ⟶ x10 x6 ⟶ x10 x7 ⟶ x10 x9) ⟶ ∀ x9 . x9 ⊆ x8 ⟶ atleastp 4 x9 ⟶ ∀ x10 : ο . (x0 ∈ x9 ⟶ x1 ∈ x9 ⟶ x2 ∈ x9 ⟶ x3 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x1 ∈ x9 ⟶ x2 ∈ x9 ⟶ x4 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x1 ∈ x9 ⟶ x3 ∈ x9 ⟶ x4 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x2 ∈ x9 ⟶ x3 ∈ x9 ⟶ x4 ∈ x9 ⟶ x10) ⟶ (x1 ∈ x9 ⟶ x2 ∈ x9 ⟶ x3 ∈ x9 ⟶ x4 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x1 ∈ x9 ⟶ x2 ∈ x9 ⟶ x5 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x1 ∈ x9 ⟶ x3 ∈ x9 ⟶ x5 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x2 ∈ x9 ⟶ x3 ∈ x9 ⟶ x5 ∈ x9 ⟶ x10) ⟶ (x1 ∈ x9 ⟶ x2 ∈ x9 ⟶ x3 ∈ x9 ⟶ x5 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x1 ∈ x9 ⟶ x4 ∈ x9 ⟶ x5 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x2 ∈ x9 ⟶ x4 ∈ x9 ⟶ x5 ∈ x9 ⟶ x10) ⟶ (x1 ∈ x9 ⟶ x2 ∈ x9 ⟶ x4 ∈ x9 ⟶ x5 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x3 ∈ x9 ⟶ x4 ∈ x9 ⟶ x5 ∈ x9 ⟶ x10) ⟶ (x1 ∈ x9 ⟶ x3 ∈ x9 ⟶ x4 ∈ x9 ⟶ x5 ∈ x9 ⟶ x10) ⟶ (x2 ∈ x9 ⟶ x3 ∈ x9 ⟶ x4 ∈ x9 ⟶ x5 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x1 ∈ x9 ⟶ x2 ∈ x9 ⟶ x6 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x1 ∈ x9 ⟶ x3 ∈ x9 ⟶ x6 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x2 ∈ x9 ⟶ x3 ∈ x9 ⟶ x6 ∈ x9 ⟶ x10) ⟶ (x1 ∈ x9 ⟶ x2 ∈ x9 ⟶ x3 ∈ x9 ⟶ x6 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x1 ∈ x9 ⟶ x4 ∈ x9 ⟶ x6 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x2 ∈ x9 ⟶ x4 ∈ x9 ⟶ x6 ∈ x9 ⟶ x10) ⟶ (x1 ∈ x9 ⟶ x2 ∈ x9 ⟶ x4 ∈ x9 ⟶ x6 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x3 ∈ x9 ⟶ x4 ∈ x9 ⟶ x6 ∈ x9 ⟶ x10) ⟶ (x1 ∈ x9 ⟶ x3 ∈ x9 ⟶ x4 ∈ x9 ⟶ x6 ∈ x9 ⟶ x10) ⟶ (x2 ∈ x9 ⟶ x3 ∈ x9 ⟶ x4 ∈ x9 ⟶ x6 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x1 ∈ x9 ⟶ x5 ∈ x9 ⟶ x6 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x2 ∈ x9 ⟶ x5 ∈ x9 ⟶ x6 ∈ x9 ⟶ x10) ⟶ (x1 ∈ x9 ⟶ x2 ∈ x9 ⟶ x5 ∈ x9 ⟶ x6 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x3 ∈ x9 ⟶ x5 ∈ x9 ⟶ x6 ∈ x9 ⟶ x10) ⟶ (x1 ∈ x9 ⟶ x3 ∈ x9 ⟶ x5 ∈ x9 ⟶ x6 ∈ x9 ⟶ x10) ⟶ (x2 ∈ x9 ⟶ x3 ∈ x9 ⟶ x5 ∈ x9 ⟶ x6 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x4 ∈ x9 ⟶ x5 ∈ x9 ⟶ x6 ∈ x9 ⟶ x10) ⟶ (x1 ∈ x9 ⟶ x4 ∈ x9 ⟶ x5 ∈ x9 ⟶ x6 ∈ x9 ⟶ x10) ⟶ (x2 ∈ x9 ⟶ x4 ∈ x9 ⟶ x5 ∈ x9 ⟶ x6 ∈ x9 ⟶ x10) ⟶ (x3 ∈ x9 ⟶ x4 ∈ x9 ⟶ x5 ∈ x9 ⟶ x6 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x1 ∈ x9 ⟶ x2 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x1 ∈ x9 ⟶ x3 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x2 ∈ x9 ⟶ x3 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x1 ∈ x9 ⟶ x2 ∈ x9 ⟶ x3 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x1 ∈ x9 ⟶ x4 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x2 ∈ x9 ⟶ x4 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x1 ∈ x9 ⟶ x2 ∈ x9 ⟶ x4 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x3 ∈ x9 ⟶ x4 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x1 ∈ x9 ⟶ x3 ∈ x9 ⟶ x4 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x2 ∈ x9 ⟶ x3 ∈ x9 ⟶ x4 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x1 ∈ x9 ⟶ x5 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x2 ∈ x9 ⟶ x5 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x1 ∈ x9 ⟶ x2 ∈ x9 ⟶ x5 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x3 ∈ x9 ⟶ x5 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x1 ∈ x9 ⟶ x3 ∈ x9 ⟶ x5 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x2 ∈ x9 ⟶ x3 ∈ x9 ⟶ x5 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x4 ∈ x9 ⟶ x5 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x1 ∈ x9 ⟶ x4 ∈ x9 ⟶ x5 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x2 ∈ x9 ⟶ x4 ∈ x9 ⟶ x5 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x3 ∈ x9 ⟶ x4 ∈ x9 ⟶ x5 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x1 ∈ x9 ⟶ x6 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x2 ∈ x9 ⟶ x6 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x1 ∈ x9 ⟶ x2 ∈ x9 ⟶ x6 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x3 ∈ x9 ⟶ x6 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x1 ∈ x9 ⟶ x3 ∈ x9 ⟶ x6 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x2 ∈ x9 ⟶ x3 ∈ x9 ⟶ x6 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x4 ∈ x9 ⟶ x6 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x1 ∈ x9 ⟶ x4 ∈ x9 ⟶ x6 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x2 ∈ x9 ⟶ x4 ∈ x9 ⟶ x6 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x3 ∈ x9 ⟶ x4 ∈ x9 ⟶ x6 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x0 ∈ x9 ⟶ x5 ∈ x9 ⟶ x6 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x1 ∈ x9 ⟶ x5 ∈ x9 ⟶ x6 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x2 ∈ x9 ⟶ x5 ∈ x9 ⟶ x6 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x3 ∈ x9 ⟶ x5 ∈ x9 ⟶ x6 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ (x4 ∈ x9 ⟶ x5 ∈ x9 ⟶ x6 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10) ⟶ x10
Theorem 70922.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 . (∀ x9 . x9 ∈ x8 ⟶ ∀ x10 : ι → ο . x10 x0 ⟶ x10 x1 ⟶ x10 x2 ⟶ x10 x3 ⟶ x10 x4 ⟶ x10 x5 ⟶ x10 x6 ⟶ x10 x7 ⟶ x10 x9) ⟶ (x0 = x1 ⟶ ∀ x9 : ο . x9) ⟶ (x0 = x2 ⟶ ∀ x9 : ο . x9) ⟶ (x1 = x2 ⟶ ∀ x9 : ο . x9) ⟶ (x0 = x3 ⟶ ∀ x9 : ο . x9) ⟶ (x1 = x3 ⟶ ∀ x9 : ο . x9) ⟶ (x2 = x3 ⟶ ∀ x9 : ο . x9) ⟶ (x0 = x4 ⟶ ∀ x9 : ο . x9) ⟶ (x1 = x4 ⟶ ∀ x9 : ο . x9) ⟶ (x2 = x4 ⟶ ∀ x9 : ο . x9) ⟶ (x3 = x4 ⟶ ∀ x9 : ο . x9) ⟶ (x0 = x5 ⟶ ∀ x9 : ο . x9) ⟶ (x1 = x5 ⟶ ∀ x9 : ο . x9) ⟶ (x2 = x5 ⟶ ∀ x9 : ο . x9) ⟶ (x3 = x5 ⟶ ∀ x9 : ο . x9) ⟶ (x4 = x5 ⟶ ∀ x9 : ο . x9) ⟶ (x0 = x6 ⟶ ∀ x9 : ο . x9) ⟶ (x1 = x6 ⟶ ∀ x9 : ο . x9) ⟶ (x2 = x6 ⟶ ∀ x9 : ο . x9) ⟶ (x3 = x6 ⟶ ∀ x9 : ο . x9) ⟶ (x4 = x6 ⟶ ∀ x9 : ο . x9) ⟶ (x5 = x6 ⟶ ∀ x9 : ο . x9) ⟶ (x0 = x7 ⟶ ∀ x9 : ο . x9) ⟶ (x1 = x7 ⟶ ∀ x9 : ο . x9) ⟶ (x2 = x7 ⟶ ∀ x9 : ο . x9) ⟶ (x3 = x7 ⟶ ∀ x9 : ο . x9) ⟶ (x4 = x7 ⟶ ∀ x9 : ο . x9) ⟶ (x5 = x7 ⟶ ∀ x9 : ο . x9) ⟶ (x6 = x7 ⟶ ∀ x9 : ο . x9) ⟶ ∀ x9 : ι → ι → ο . (∀ x10 : ο . x9 x0 x1 ⟶ x10) ⟶ (∀ x10 : ο . x9 x0 x2 ⟶ x10) ⟶ (∀ x10 : ο . x9 x1 x2 ⟶ x10) ⟶ (∀ x10 : ο . x9 x0 x3 ⟶ x10) ⟶ (∀ x10 : ο . x9 x1 x3 ⟶ x10) ⟶ x9 x2 x3 ⟶ (∀ x10 : ο . x9 x0 x4 ⟶ x10) ⟶ x9 x1 x4 ⟶ (∀ x10 : ο . x9 x2 x4 ⟶ x10) ⟶ x9 x3 x4 ⟶ (∀ x10 : ο . x9 x0 x5 ⟶ x10) ⟶ x9 x1 x5 ⟶ x9 x2 x5 ⟶ (∀ x10 : ο . x9 x3 x5 ⟶ x10) ⟶ (∀ x10 : ο . x9 x4 x5 ⟶ x10) ⟶ x9 x0 x6 ⟶ (∀ x10 : ο . x9 x1 x6 ⟶ x10) ⟶ (∀ x10 : ο . x9 x2 x6 ⟶ x10) ⟶ x9 x3 x6 ⟶ (∀ x10 : ο . x9 x4 x6 ⟶ x10) ⟶ x9 x5 x6 ⟶ x9 x0 x7 ⟶ (∀ x10 : ο . x9 x1 x7 ⟶ x10) ⟶ x9 x2 x7 ⟶ (∀ x10 : ο . x9 x3 x7 ⟶ x10) ⟶ x9 x4 x7 ⟶ (∀ x10 : ο . x9 x5 x7 ⟶ x10) ⟶ (∀ x10 : ο . x9 x6 x7 ⟶ x10) ⟶ and (∀ x10 . x10 ⊆ x8 ⟶ atleastp 3 x10 ⟶ ∀ x11 : ο . (∀ x12 . x12 ∈ x10 ⟶ ∀ x13 . x13 ∈ x10 ⟶ (x12 = x13 ⟶ ∀ x14 : ο . x14) ⟶ not (x9 x12 x13) ⟶ x11) ⟶ x11) (∀ x10 . x10 ⊆ x8 ⟶ atleastp 4 x10 ⟶ ∀ x11 : ο . (∀ x12 . x12 ∈ x10 ⟶ ∀ x13 . x13 ∈ x10 ⟶ (x12 = x13 ⟶ ∀ x14 : ο . x14) ⟶ x9 x12 x13 ⟶ x11) ⟶ x11) (proof)
Definition or^or := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x2) ⟶ (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 FalseE^FalseE : False ⟶ ∀ x0 : ο . x0
Theorem 052c4.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 . (∀ x9 . x9 ∈ x8 ⟶ ∀ x10 : ι → ο . x10 x0 ⟶ x10 x1 ⟶ x10 x2 ⟶ x10 x3 ⟶ x10 x4 ⟶ x10 x5 ⟶ x10 x6 ⟶ x10 x7 ⟶ x10 x9) ⟶ (x0 = x1 ⟶ ∀ x9 : ο . x9) ⟶ (x0 = x2 ⟶ ∀ x9 : ο . x9) ⟶ (x1 = x2 ⟶ ∀ x9 : ο . x9) ⟶ (x0 = x3 ⟶ ∀ x9 : ο . x9) ⟶ (x1 = x3 ⟶ ∀ x9 : ο . x9) ⟶ (x2 = x3 ⟶ ∀ x9 : ο . x9) ⟶ (x0 = x4 ⟶ ∀ x9 : ο . x9) ⟶ (x1 = x4 ⟶ ∀ x9 : ο . x9) ⟶ (x2 = x4 ⟶ ∀ x9 : ο . x9) ⟶ (x3 = x4 ⟶ ∀ x9 : ο . x9) ⟶ (x0 = x5 ⟶ ∀ x9 : ο . x9) ⟶ (x1 = x5 ⟶ ∀ x9 : ο . x9) ⟶ (x2 = x5 ⟶ ∀ x9 : ο . x9) ⟶ (x3 = x5 ⟶ ∀ x9 : ο . x9) ⟶ (x4 = x5 ⟶ ∀ x9 : ο . x9) ⟶ (x0 = x6 ⟶ ∀ x9 : ο . x9) ⟶ (x1 = x6 ⟶ ∀ x9 : ο . x9) ⟶ (x2 = x6 ⟶ ∀ x9 : ο . x9) ⟶ (x3 = x6 ⟶ ∀ x9 : ο . x9) ⟶ (x4 = x6 ⟶ ∀ x9 : ο . x9) ⟶ (x5 = x6 ⟶ ∀ x9 : ο . x9) ⟶ (x0 = x7 ⟶ ∀ x9 : ο . x9) ⟶ (x1 = x7 ⟶ ∀ x9 : ο . x9) ⟶ (x2 = x7 ⟶ ∀ x9 : ο . x9) ⟶ (x3 = x7 ⟶ ∀ x9 : ο . x9) ⟶ (x4 = x7 ⟶ ∀ x9 : ο . x9) ⟶ (x5 = x7 ⟶ ∀ x9 : ο . x9) ⟶ (x6 = x7 ⟶ ∀ x9 : ο . x9) ⟶ not (TwoRamseyProp_atleastp 3 4 x8) (proof)
Param TwoRamseyProp^{TwoRamseyProp} : ι → ι → ι → ο
Known cases_8^cases_8 : ∀ x0 . x0 ∈ 8 ⟶ ∀ x1 : ι → ο . x1 0 ⟶ x1 1 ⟶ x1 2 ⟶ x1 3 ⟶ x1 4 ⟶ x1 5 ⟶ x1 6 ⟶ x1 7 ⟶ x1 x0
Known neq_0_1^neq_0_1 : 0 = 1 ⟶ ∀ x0 : ο . x0
Known neq_0_2^neq_0_2 : 0 = 2 ⟶ ∀ x0 : ο . x0
Known neq_1_2^neq_1_2 : 1 = 2 ⟶ ∀ x0 : ο . x0
Known neq_i_sym^neq_i_sym : ∀ x0 x1 . (x0 = x1 ⟶ ∀ x2 : ο . x2) ⟶ x1 = x0 ⟶ ∀ x2 : ο . x2
Known neq_3_0^neq_3_0 : 3 = 0 ⟶ ∀ x0 : ο . x0
Known neq_3_1^neq_3_1 : 3 = 1 ⟶ ∀ x0 : ο . x0
Known neq_3_2^neq_3_2 : 3 = 2 ⟶ ∀ x0 : ο . x0
Known neq_4_0^neq_4_0 : 4 = 0 ⟶ ∀ x0 : ο . x0
Known neq_4_1^neq_4_1 : 4 = 1 ⟶ ∀ x0 : ο . x0
Known neq_4_2^neq_4_2 : 4 = 2 ⟶ ∀ x0 : ο . x0
Known neq_4_3^neq_4_3 : 4 = 3 ⟶ ∀ x0 : ο . x0
Known neq_5_0^neq_5_0 : 5 = 0 ⟶ ∀ x0 : ο . x0
Known neq_5_1^neq_5_1 : 5 = 1 ⟶ ∀ x0 : ο . x0
Known neq_5_2^neq_5_2 : 5 = 2 ⟶ ∀ x0 : ο . x0
Known neq_5_3^neq_5_3 : 5 = 3 ⟶ ∀ x0 : ο . x0
Known neq_5_4^neq_5_4 : 5 = 4 ⟶ ∀ x0 : ο . x0
Known neq_6_0^neq_6_0 : 6 = 0 ⟶ ∀ x0 : ο . x0
Known neq_6_1^neq_6_1 : 6 = 1 ⟶ ∀ x0 : ο . x0
Known neq_6_2^neq_6_2 : 6 = 2 ⟶ ∀ x0 : ο . x0
Known neq_6_3^neq_6_3 : 6 = 3 ⟶ ∀ x0 : ο . x0
Known neq_6_4^neq_6_4 : 6 = 4 ⟶ ∀ x0 : ο . x0
Known neq_6_5^neq_6_5 : 6 = 5 ⟶ ∀ x0 : ο . x0
Known neq_7_0^neq_7_0 : 7 = 0 ⟶ ∀ x0 : ο . x0
Known neq_7_1^neq_7_1 : 7 = 1 ⟶ ∀ x0 : ο . x0
Known neq_7_2^neq_7_2 : 7 = 2 ⟶ ∀ x0 : ο . x0
Known neq_7_3^neq_7_3 : 7 = 3 ⟶ ∀ x0 : ο . x0
Known neq_7_4^neq_7_4 : 7 = 4 ⟶ ∀ x0 : ο . x0
Known neq_7_5^neq_7_5 : 7 = 5 ⟶ ∀ x0 : ο . x0
Known neq_7_6^neq_7_6 : 7 = 6 ⟶ ∀ x0 : ο . x0
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_4_8^{not_TwoRamseyProp_3_4_8} : not (TwoRamseyProp 3 4 8) (proof)
Param UPair^UPair : ι → ι → ι
Param Sing^Sing : ι → ι
Known In_Power_3_cases_impred : ∀ x0 . x0 ∈ prim4 3 ⟶ ∀ x1 : ο . (x0 = 0 ⟶ x1) ⟶ (x0 = 1 ⟶ x1) ⟶ (x0 = Sing 1 ⟶ x1) ⟶ (x0 = 2 ⟶ x1) ⟶ (x0 = Sing 2 ⟶ x1) ⟶ (x0 = UPair 0 2 ⟶ x1) ⟶ (x0 = UPair 1 2 ⟶ x1) ⟶ (x0 = 3 ⟶ x1) ⟶ x1
Known not_Empty_eq_Sing : ∀ x0 . 0 = Sing x0 ⟶ ∀ x1 : ο . x1
Definition nIn^nIn := λ x0 x1 . not (x0 ∈ x1)
Known nIn_not_eq_Sing : ∀ x0 x1 . nIn x0 x1 ⟶ x1 = Sing x0 ⟶ ∀ x2 : ο . x2
Known In_irref^In_irref : ∀ x0 . nIn x0 x0
Known nIn_2_1^nIn_2_1 : nIn 2 1
Known neq_2_1^neq_2_1 : 2 = 1 ⟶ ∀ x0 : ο . x0
Known SingE^SingE : ∀ x0 x1 . x1 ∈ Sing x0 ⟶ x1 = x0
Known In_0_2^In_0_2 : 0 ∈ 2
Known not_Empty_eq_UPair : ∀ x0 x1 . 0 = UPair x0 x1 ⟶ ∀ x2 : ο . x2
Known nIn_not_eq_UPair_2 : ∀ x0 x1 x2 . nIn x1 x2 ⟶ x2 = UPair x0 x1 ⟶ ∀ x3 : ο . x3
Known nIn_not_eq_UPair_1 : ∀ x0 x1 x2 . nIn x0 x2 ⟶ x2 = UPair x0 x1 ⟶ ∀ x3 : ο . x3
Known UPairE^UPairE : ∀ x0 x1 x2 . x0 ∈ UPair x1 x2 ⟶ or (x0 = x1) (x0 = x2)
Known neq_1_0^neq_1_0 : 1 = 0 ⟶ ∀ x0 : ο . x0
Known In_0_3^In_0_3 : 0 ∈ 3
Known In_1_3^In_1_3 : 1 ∈ 3
Theorem not_TwoRamseyProp_atleast_3_4_Power_3 : not (TwoRamseyProp_atleastp 3 4 (prim4 3)) (proof)
Param nat_p^nat_p : ι → ο
Known nat_In_atleastp : ∀ x0 . nat_p x0 ⟶ ∀ x1 . x1 ∈ x0 ⟶ atleastp x1 x0
Known nat_5^nat_5 : nat_p 5
Known In_4_5^In_4_5 : 4 ∈ 5
Theorem 6bca8..^{not_TwoRamseyProp_3_5_Power_3} : not (TwoRamseyProp 3 5 (prim4 3)) (proof)
Known nat_6^nat_6 : nat_p 6
Known In_4_6^In_4_6 : 4 ∈ 6
Theorem ff590..^{not_TwoRamseyProp_3_6_Power_3} : not (TwoRamseyProp 3 6 (prim4 3)) (proof)
Known nat_ordsucc^nat_ordsucc : ∀ x0 . nat_p x0 ⟶ nat_p (ordsucc x0)
Theorem nat_7^nat_7 : nat_p 7 (proof)
Theorem nat_8^nat_8 : nat_p 8 (proof)
Theorem nat_9^nat_9 : nat_p 9 (proof)
Theorem nat_10^nat_10 : nat_p 10 (proof)
Known In_4_7^In_4_7 : 4 ∈ 7
Theorem 54668..^{not_TwoRamseyProp_3_7_Power_3} : not (TwoRamseyProp 3 7 (prim4 3)) (proof)
Known In_4_8^In_4_8 : 4 ∈ 8
Theorem df26e..^{not_TwoRamseyProp_3_8_Power_3} : not (TwoRamseyProp 3 8 (prim4 3)) (proof)
Known In_4_9^In_4_9 : 4 ∈ 9
Theorem 69d43..^{not_TwoRamseyProp_3_9_Power_3} : not (TwoRamseyProp 3 9 (prim4 3)) (proof)
Known nat_ordsucc_in_ordsucc^{nat_ordsucc_in_ordsucc} : ∀ x0 . nat_p x0 ⟶ ∀ x1 . x1 ∈ x0 ⟶ ordsucc x1 ∈ ordsucc x0
Known In_3_9^In_3_9 : 3 ∈ 9
Theorem 35ffd.. : 4 ∈ 10 (proof)
Theorem 7f909..^{not_TwoRamseyProp_3_10_Power_3} : not (TwoRamseyProp 3 10 (prim4 3)) (proof)
Known nat_4^nat_4 : nat_p 4
Known In_3_4^In_3_4 : 3 ∈ 4
Theorem ce62b..^{not_TwoRamseyProp_4_4_Power_3} : not (TwoRamseyProp 4 4 (prim4 3)) (proof)
Theorem fe972..^{not_TwoRamseyProp_4_5_Power_3} : not (TwoRamseyProp 4 5 (prim4 3)) (proof)
Theorem 33278..^{not_TwoRamseyProp_4_6_Power_3} : not (TwoRamseyProp 4 6 (prim4 3)) (proof)
Theorem e1864..^{not_TwoRamseyProp_4_7_Power_3} : not (TwoRamseyProp 4 7 (prim4 3)) (proof)
Theorem 95a55..^{not_TwoRamseyProp_4_8_Power_3} : not (TwoRamseyProp 4 8 (prim4 3)) (proof)
Theorem 8b769..^{not_TwoRamseyProp_4_9_Power_3} : not (TwoRamseyProp 4 9 (prim4 3)) (proof)
Known In_3_5^In_3_5 : 3 ∈ 5
Theorem cd2fd..^{not_TwoRamseyProp_5_5_Power_3} : not (TwoRamseyProp 5 5 (prim4 3)) (proof)
Theorem eff2c..^{not_TwoRamseyProp_5_6_Power_3} : not (TwoRamseyProp 5 6 (prim4 3)) (proof)
Theorem 73405..^{not_TwoRamseyProp_5_7_Power_3} : not (TwoRamseyProp 5 7 (prim4 3)) (proof)
Theorem 41978..^{not_TwoRamseyProp_5_8_Power_3} : not (TwoRamseyProp 5 8 (prim4 3)) (proof)
Known In_3_6^In_3_6 : 3 ∈ 6
Theorem 3de2e..^{not_TwoRamseyProp_6_6_Power_3} : not (TwoRamseyProp 6 6 (prim4 3)) (proof)
Theorem 84f84..^{not_TwoRamseyProp_6_7_Power_3} : not (TwoRamseyProp 6 7 (prim4 3)) (proof)