Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Let x3 of type ι be given.
Let x4 of type ι be given.
Assume H0: TwoRamseyProp x0 x2 x4.
Assume H1: atleastp x1 x0.
Assume H2: atleastp x3 x2.
Let x5 of type ιιο be given.
Assume H3: ∀ x6 x7 . x5 x6 x7x5 x7 x6.
Apply H0 with x5, or (∃ x6 . and (x6x4) (and (atleastp x1 x6) (∀ x7 . x7x6∀ x8 . x8x6(x7 = x8∀ x9 : ο . x9)x5 x7 x8))) (∃ x6 . and (x6x4) (and (atleastp x3 x6) (∀ x7 . x7x6∀ x8 . x8x6(x7 = x8∀ x9 : ο . x9)not (x5 x7 x8)))) leaving 3 subgoals.
The subproof is completed by applying H3.
Assume H4: ∃ x6 . and (x6x4) (and (equip x0 x6) (∀ x7 . x7x6∀ x8 . x8x6(x7 = x8∀ x9 : ο . x9)x5 x7 x8)).
Apply H4 with or (∃ x6 . and (x6x4) (and (atleastp x1 x6) (∀ x7 . x7x6∀ x8 . x8x6(x7 = x8∀ x9 : ο . x9)x5 x7 x8))) (∃ x6 . and (x6x4) (and (atleastp x3 x6) (∀ x7 . x7x6∀ x8 . x8x6(x7 = x8∀ x9 : ο . x9)not (x5 x7 x8)))).
Let x6 of type ι be given.
Assume H5: (λ x7 . and (x7x4) (and (equip x0 x7) (∀ x8 . x8x7∀ x9 . x9x7(x8 = x9∀ x10 : ο . x10)x5 x8 x9))) x6.
Apply H5 with or (∃ x7 . and (x7x4) (and (atleastp x1 x7) (∀ x8 . x8x7∀ x9 . x9x7(x8 = x9∀ x10 : ο . x10)x5 x8 x9))) (∃ x7 . and (x7x4) (and (atleastp x3 x7) (∀ x8 . x8x7∀ x9 . x9x7(x8 = x9∀ x10 : ο . x10)not (x5 x8 x9)))).
Assume H6: x6x4.
Assume H7: and (equip x0 x6) (∀ x7 . x7x6∀ x8 . x8x6(x7 = x8∀ x9 : ο . x9)x5 x7 x8).
Apply H7 with or (∃ x7 . and (x7x4) (and (atleastp x1 x7) (∀ x8 . ...∀ x9 . ......x5 x8 ...))) ....
...
...