Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: x0 ⊆ u12.
Assume H1: atleastp u5 x0.
Assume H2: ∀ x1 . x1 ∈ x0 ⟶ ∀ x2 . x2 ∈ x0 ⟶ (x1 = x2 ⟶ ∀ x3 : ο . x3) ⟶ not (TwoRamseyGraph_3_6_17 x1 x2).
Claim L3: ...
...
Apply unknownprop_45d11dce2d0b092bd17c01d64c29c5885c90b43dc7cb762c6d6ada999ea508c5 with u1, setminus x0 u8, False leaving 3 subgoals.
The subproof is completed by applying nat_1.
Assume H4: atleastp (setminus x0 u8) u1.
Claim L5: ...
...
Claim L6: ...
...
Apply L6 with False.
Let x1 of type ι be given.
Assume H7: x1 ⊆ u12.
Assume H8: atleastp u4 (binintersect x1 u8).
Assume H9: ∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ not (TwoRamseyGraph_3_6_17 x2 x3).
Assume H10: u8 ∈ x1.
Apply unknownprop_19c5bea28ef119e30d80f4e7c578df826b34bc3d0b15978a12c7c1b896ec3046 with binintersect x1 u8, False leaving 2 subgoals.
The subproof is completed by applying H8.
Let x2 of type ι be given.
Assume H11: x2 ∈ binintersect x1 u8.
Let x3 of type ι be given.
Assume H12: x3 ∈ binintersect x1 u8.
Let x4 of type ι be given.
Assume H13: x4 ∈ binintersect x1 u8.
Let x5 of type ι be given.
Assume H14: x5 ∈ binintersect x1 u8.
Assume H15: x2 = x3 ⟶ ∀ x6 : ο . x6.
Assume H16: x2 = x4 ⟶ ∀ x6 : ο . x6.
Assume H17: x2 = x5 ⟶ ∀ x6 : ο . x6.
Assume H18: x3 = x4 ⟶ ∀ x6 : ο . x6.
Assume H19: x3 = x5 ⟶ ∀ x6 : ο . x6.
Assume H20: x4 = x5 ⟶ ∀ x6 : ο . x6.
Apply binintersectE with x1, u8, x2, False leaving 2 subgoals.
The subproof is completed by applying H11.
Assume H21: x2 ∈ x1.
Assume H22: x2 ∈ u8.
Apply binintersectE with x1, u8, x3, False leaving 2 subgoals.
The subproof is completed by applying H12.
Assume H23: x3 ∈ x1.
Assume H24: x3 ∈ u8.
Apply binintersectE with x1, u8, x4, False leaving 2 subgoals.
The subproof is completed by applying H13.
Assume H25: x4 ∈ x1.
Assume H26: x4 ∈ u8.
Apply binintersectE with x1, u8, x5, False leaving 2 subgoals.
The subproof is completed by applying H14.
Assume H27: x5 ∈ x1.
Assume H28: x5 ∈ u8.
Claim L29: ...
...
Claim L30: ...
...
Claim L31: ...
...
Claim L32: ...
...
Claim L33: ...
...
Claim L34: ...
...
Claim L35: ...
...
Claim L36: ...
...
Apply unknownprop_39eded3fceade33502100460a606e7a1c03e6da22fb6008fad791b8587f951e7 with u17_to_Church17 x2, u17_to_Church17 x3, u17_to_Church17 x4, u17_to_Church17 x5 leaving 14 subgoals.
Apply unknownprop_a1e277f419507eb6211f44d9457aefea2a8b3e26b2ee84f0795856dfe97fcf6e with x2.
The subproof is completed by applying H22.
Apply unknownprop_a1e277f419507eb6211f44d9457aefea2a8b3e26b2ee84f0795856dfe97fcf6e with x3.
The subproof is completed by applying H24.
Apply unknownprop_a1e277f419507eb6211f44d9457aefea2a8b3e26b2ee84f0795856dfe97fcf6e with x4.
The subproof is completed by applying H26.
Apply unknownprop_a1e277f419507eb6211f44d9457aefea2a8b3e26b2ee84f0795856dfe97fcf6e with x5.
The subproof is completed by applying H28.
Apply unknownprop_46a7f5ba218e301f19d33cc265134a2df7adfd3de64e750dc665649ee8f6340d with u17_to_Church17 x2, λ x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 . x14, TwoRamseyGraph_3_6_Church17 (u17_to_Church17 x2) (λ x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 . x14) = λ x6 x7 . x7 leaving 4 subgoals.
Apply unknownprop_f44342ed74648c23c8734d945bc8b2c1af5a9cb594ef51477e7844cb71f944f8 with x2.
The subproof is completed by applying L29.
The subproof is completed by applying unknownprop_c37600b80efb18922b2424c0ae3622d88c262b6e7e6fb3aa0f6bc2b0ba9f1be7.
Assume H37: TwoRamseyGraph_3_6_Church17 (u17_to_Church17 x2) (λ x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 . x14) = λ x6 x7 . x6.
Apply L30 with TwoRamseyGraph_3_6_Church17 (u17_to_Church17 x2) (λ x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 . x14) = λ x6 x7 . x7.
Assume H38: x2 ∈ u17.
Assume H39: u8 ∈ u17.
Apply unknownprop_8f7d877f09ad2d2b6bd165b15d072d92366514d5c83c4caef2b25c48dd454e7b with λ x6 x7 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . TwoRamseyGraph_3_6_Church17 (u17_to_Church17 x2) x7 = λ x8 x9 . x8.
The subproof is completed by applying H37.
Assume H37: TwoRamseyGraph_3_6_Church17 (u17_to_Church17 x2) (λ x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 . x14) = λ x6 x7 . x7.
The subproof is completed by applying H37.
Apply unknownprop_46a7f5ba218e301f19d33cc265134a2df7adfd3de64e750dc665649ee8f6340d with u17_to_Church17 x3, λ x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 . x14, TwoRamseyGraph_3_6_Church17 (u17_to_Church17 x3) (λ x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 . x14) = λ x6 x7 . x7 leaving 4 subgoals.
Apply unknownprop_f44342ed74648c23c8734d945bc8b2c1af5a9cb594ef51477e7844cb71f944f8 with x3.
The subproof is completed by applying L31.
The subproof is completed by applying unknownprop_c37600b80efb18922b2424c0ae3622d88c262b6e7e6fb3aa0f6bc2b0ba9f1be7.
Assume H37: TwoRamseyGraph_3_6_Church17 (u17_to_Church17 x3) (λ x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 . x14) = λ x6 x7 . x6.
Apply L32 with TwoRamseyGraph_3_6_Church17 (u17_to_Church17 x3) (λ x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 . x14) = λ x6 x7 . x7.
Assume H38: x3 ∈ u17.
...
...
...
...
...
...
...
...
...
...
...
■