Search for blocks/addresses/...

Proofgold Proof

pf
Assume H0: TwoRamseyProp_atleastp 3 6 (prim4 4).
Claim L1: ...
...
Apply H0 with λ x0 x1 . ∀ x2 . x2 ∈ 4 ⟶ ∀ x3 . x3 ∈ 4 ⟶ x2 ∈ x0 = x2 ∈ x1 ⟶ x3 ∈ x0 = x3 ∈ x1 ⟶ x2 = x3, False leaving 3 subgoals.
The subproof is completed by applying L1.
Assume H2: ∃ x0 . and (x0 ⊆ prim4 4) (and (atleastp 3 x0) (∀ x1 . x1 ∈ x0 ⟶ ∀ x2 . x2 ∈ x0 ⟶ (x1 = x2 ⟶ ∀ x3 : ο . x3) ⟶ (λ x3 x4 . ∀ x5 . x5 ∈ 4 ⟶ ∀ x6 . x6 ∈ 4 ⟶ x5 ∈ x3 = x5 ∈ x4 ⟶ x6 ∈ x3 = x6 ∈ x4 ⟶ x5 = x6) x1 x2)).
Apply H2 with False.
Let x0 of type ι be given.
Assume H3: (λ x1 . and (x1 ⊆ prim4 4) (and (atleastp 3 x1) (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ ∀ x4 . x4 ∈ 4 ⟶ ∀ x5 . x5 ∈ 4 ⟶ x4 ∈ x2 = x4 ∈ x3 ⟶ x5 ∈ x2 = x5 ∈ x3 ⟶ x4 = x5))) x0.
Apply H3 with False.
Assume H4: x0 ⊆ prim4 4.
Assume H5: and (atleastp 3 x0) (∀ x1 . x1 ∈ x0 ⟶ ∀ x2 . x2 ∈ x0 ⟶ (x1 = x2 ⟶ ∀ x3 : ο . x3) ⟶ ∀ x3 . x3 ∈ 4 ⟶ ∀ x4 . x4 ∈ 4 ⟶ x3 ∈ x1 = x3 ∈ x2 ⟶ x4 ∈ x1 = x4 ∈ x2 ⟶ x3 = x4).
Apply H5 with False.
Assume H6: atleastp 3 x0.
Assume H7: ∀ x1 . x1 ∈ x0 ⟶ ∀ x2 . x2 ∈ x0 ⟶ (x1 = x2 ⟶ ∀ x3 : ο . x3) ⟶ (λ x3 x4 . ∀ x5 . x5 ∈ 4 ⟶ ∀ x6 . x6 ∈ 4 ⟶ x5 ∈ x3 = x5 ∈ x4 ⟶ x6 ∈ x3 = x6 ∈ x4 ⟶ x5 = x6) x1 x2.
Apply unknownprop_95c6cbd2308b27a7edcd2a1d9389b377988e902d740d05dc7c88e6b8da945ab9 with x0, False leaving 2 subgoals.
The subproof is completed by applying H6.
Let x1 of type ι be given.
Assume H8: x1 ∈ x0.
Let x2 of type ι be given.
Assume H9: x2 ∈ x0.
Let x3 of type ι be given.
Assume H10: x3 ∈ x0.
Assume H11: x1 = x2 ⟶ ∀ x4 : ο . x4.
Assume H12: x1 = x3 ⟶ ∀ x4 : ο . x4.
Assume H13: x2 = x3 ⟶ ∀ x4 : ο . x4.
Claim L14: ...
...
Claim L15: ...
...
Claim L16: ...
...
Claim L17: ...
...
Claim L18: ...
...
Claim L19: ...
...
Claim L20: ...
...
Apply L20 with False.
Let x4 of type ι → ι be given.
Assume H21: ∀ x5 . x5 ∈ 4 ⟶ ∃ x6 . and (x6 ∈ 3) (x4 x6 = x5).
Claim L22: inj 4 3 (inv 3 ...)
...
Apply L22 with False.
Apply PigeonHole_nat with 3, inv 3 x4.
The subproof is completed by applying nat_3.
...
■