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.
Let x5 of type ι be given.
Let x6 of type ι be given.
Let x7 of type ι be given.
Let x8 of type ι be given.
Assume H0: ∀ x9 . x9 ∈ x8 ⟶ ∀ x10 : ι → ο . x10 x0 ⟶ x10 x1 ⟶ x10 x2 ⟶ x10 x3 ⟶ x10 x4 ⟶ x10 x5 ⟶ x10 x6 ⟶ x10 x7 ⟶ x10 x9.
Assume H1: x0 = x1 ⟶ ∀ x9 : ο . x9.
Assume H2: x0 = x2 ⟶ ∀ x9 : ο . x9.
Assume H3: x1 = x2 ⟶ ∀ x9 : ο . x9.
Assume H4: x0 = x3 ⟶ ∀ x9 : ο . x9.
Assume H5: x1 = x3 ⟶ ∀ x9 : ο . x9.
Assume H6: x2 = x3 ⟶ ∀ x9 : ο . x9.
Assume H7: x0 = x4 ⟶ ∀ x9 : ο . x9.
Assume H8: x1 = x4 ⟶ ∀ x9 : ο . x9.
Assume H9: x2 = x4 ⟶ ∀ x9 : ο . x9.
Assume H10: x3 = x4 ⟶ ∀ x9 : ο . x9.
Assume H11: x0 = x5 ⟶ ∀ x9 : ο . x9.
Assume H12: x1 = x5 ⟶ ∀ x9 : ο . x9.
Assume H13: x2 = x5 ⟶ ∀ x9 : ο . x9.
Assume H14: x3 = x5 ⟶ ∀ x9 : ο . x9.
Assume H15: x4 = x5 ⟶ ∀ x9 : ο . x9.
Assume H16: x0 = x6 ⟶ ∀ x9 : ο . x9.
Assume H17: x1 = x6 ⟶ ∀ x9 : ο . x9.
Assume H18: x2 = x6 ⟶ ∀ x9 : ο . x9.
Assume H19: x3 = x6 ⟶ ∀ x9 : ο . x9.
Assume H20: x4 = x6 ⟶ ∀ x9 : ο . x9.
Assume H21: x5 = x6 ⟶ ∀ x9 : ο . x9.
Assume H22: x0 = x7 ⟶ ∀ x9 : ο . x9.
Assume H23: x1 = x7 ⟶ ∀ x9 : ο . x9.
Assume H24: x2 = x7 ⟶ ∀ x9 : ο . x9.
Assume H25: x3 = x7 ⟶ ∀ x9 : ο . x9.
Assume H26: x4 = x7 ⟶ ∀ x9 : ο . x9.
Assume H27: x5 = x7 ⟶ ∀ x9 : ο . x9.
Assume H28: x6 = x7 ⟶ ∀ x9 : ο . x9.
Assume H29: TwoRamseyProp_atleastp 3 4 x8.
Claim L30: ...
...
Claim L31: ...
...
Claim L32: ...
...
Claim L33: ...
...
Claim L34: ...
...
Claim L35: ...
...
Claim L36: ...
...
Claim L37: ...
...
Claim L38: ...
...
Claim L39: ...
...
Claim L40: ...
...
Claim L41: ...
...
Claim L42: ...
...
Claim L43: ...
...
Claim L44: ...
...
Claim L45: ...
...
Claim L46: ...
...
Claim L47: ...
...
Claim L48: ...
...
Claim L49: ...
...
Claim L50: ...
...
Claim L51: ...
...
Claim L52: ...
...
Claim L53: ...
...
Claim L54: ...
...
Claim L55: ...
...
Claim L56: ...
...
Claim L57: ...
...
Claim L58: ...
...
Apply unknownprop_7117ac08b60a122733928a67f30c882b7b2238137ce67aa64f4040a7f87be08c with x0, x1, x2, x3, x4, x5, x6, x7, x8, λ x9 x10 . ∀ x11 : ι → ι → ο . x11 x0 x6 ⟶ x11 x6 x0 ⟶ x11 x0 x7 ⟶ x11 x7 x0 ⟶ x11 x1 x4 ⟶ x11 x4 x1 ⟶ x11 x1 x5 ⟶ x11 x5 x1 ⟶ x11 x2 x3 ⟶ x11 x3 x2 ⟶ x11 x2 x5 ⟶ x11 x5 x2 ⟶ x11 x2 x7 ⟶ x11 x7 x2 ⟶ x11 x3 x4 ⟶ x11 x4 x3 ⟶ x11 x3 x6 ⟶ x11 x6 x3 ⟶ x11 x4 x7 ⟶ x11 x7 x4 ⟶ x11 x5 x6 ⟶ x11 x6 x5 ⟶ x11 x9 x10, False leaving 58 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
■