Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: x0 ⊆ u12.
Assume H1: atleastp u5 x0.
Assume H2: u8 ∈ x0.
Assume H3: u9 ∈ x0.
Assume H4: ∀ x1 . x1 ∈ x0 ⟶ ∀ x2 . x2 ∈ x0 ⟶ (x1 = x2 ⟶ ∀ x3 : ο . x3) ⟶ not (TwoRamseyGraph_3_6_17 x1 x2).
Claim L5: ...
...
Apply unknownprop_95c6cbd2308b27a7edcd2a1d9389b377988e902d740d05dc7c88e6b8da945ab9 with binintersect x0 u8, False leaving 2 subgoals.
The subproof is completed by applying L5.
Let x1 of type ι be given.
Assume H6: x1 ∈ binintersect x0 u8.
Let x2 of type ι be given.
Assume H7: x2 ∈ binintersect x0 u8.
Let x3 of type ι be given.
Assume H8: x3 ∈ binintersect x0 u8.
Assume H9: x1 = x2 ⟶ ∀ x4 : ο . x4.
Assume H10: x1 = x3 ⟶ ∀ x4 : ο . x4.
Assume H11: x2 = x3 ⟶ ∀ x4 : ο . x4.
Apply binintersectE with x0, u8, x1, False leaving 2 subgoals.
The subproof is completed by applying H6.
Assume H12: x1 ∈ x0.
Assume H13: x1 ∈ u8.
Apply binintersectE with x0, u8, x2, False leaving 2 subgoals.
The subproof is completed by applying H7.
Assume H14: x2 ∈ x0.
Assume H15: x2 ∈ u8.
Apply binintersectE with x0, u8, x3, False leaving 2 subgoals.
The subproof is completed by applying H8.
Assume H16: x3 ∈ x0.
Assume H17: x3 ∈ u8.
Claim L18: ...
...
Claim L19: ...
...
Claim L20: ...
...
Claim L21: ...
...
Apply unknownprop_ac637069183b0ef4f1754ba500cebdf1fc690defd66bf5aa2631e325b804843b with u17_to_Church17 x1, u17_to_Church17 x2, u17_to_Church17 x3 leaving 12 subgoals.
Apply unknownprop_a1e277f419507eb6211f44d9457aefea2a8b3e26b2ee84f0795856dfe97fcf6e with x1.
The subproof is completed by applying H13.
Apply unknownprop_a1e277f419507eb6211f44d9457aefea2a8b3e26b2ee84f0795856dfe97fcf6e with x2.
The subproof is completed by applying H15.
Apply unknownprop_a1e277f419507eb6211f44d9457aefea2a8b3e26b2ee84f0795856dfe97fcf6e with x3.
The subproof is completed by applying H17.
Apply unknownprop_46a7f5ba218e301f19d33cc265134a2df7adfd3de64e750dc665649ee8f6340d with u17_to_Church17 x1, λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x12, TwoRamseyGraph_3_6_Church17 (u17_to_Church17 x1) (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x12) = λ x4 x5 . x5 leaving 4 subgoals.
The subproof is completed by applying L19.
The subproof is completed by applying unknownprop_c37600b80efb18922b2424c0ae3622d88c262b6e7e6fb3aa0f6bc2b0ba9f1be7.
Assume H22: TwoRamseyGraph_3_6_Church17 (u17_to_Church17 x1) (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x12) = λ x4 x5 . x4.
Apply FalseE with TwoRamseyGraph_3_6_Church17 (u17_to_Church17 x1) (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x12) = λ x4 x5 . x5.
Apply H4 with x1, u8 leaving 4 subgoals.
The subproof is completed by applying H12.
The subproof is completed by applying H2.
Assume H23: x1 = u8.
Apply In_irref with u8.
Apply H23 with λ x4 x5 . x4 ∈ u8.
The subproof is completed by applying H13.
Assume H23: x1 ∈ u17.
Assume H24: u8 ∈ u17.
Apply unknownprop_8f7d877f09ad2d2b6bd165b15d072d92366514d5c83c4caef2b25c48dd454e7b with λ x4 x5 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . TwoRamseyGraph_3_6_Church17 (u17_to_Church17 x1) x5 = λ x6 x7 . x6.
The subproof is completed by applying H22.
Assume H22: TwoRamseyGraph_3_6_Church17 (u17_to_Church17 x1) (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x12) = λ x4 x5 . x5.
The subproof is completed by applying H22.
Apply unknownprop_46a7f5ba218e301f19d33cc265134a2df7adfd3de64e750dc665649ee8f6340d with u17_to_Church17 x1, λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x13, TwoRamseyGraph_3_6_Church17 (u17_to_Church17 x1) (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x13) = λ x4 x5 . x5 leaving 4 subgoals.
The subproof is completed by applying L19.
The subproof is completed by applying unknownprop_7fcbe5b61ad12e38a6853aaa6fe3dd0299d75fe061e77a480a4e344498540b83.
Assume H22: TwoRamseyGraph_3_6_Church17 (u17_to_Church17 x1) (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x13) = λ x4 x5 . x4.
Apply FalseE with TwoRamseyGraph_3_6_Church17 (u17_to_Church17 x1) (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x13) = λ x4 x5 . x5.
Apply H4 with x1, u9 leaving 4 subgoals.
The subproof is completed by applying H12.
The subproof is completed by applying H3.
Assume H23: x1 = u9.
Apply In_no2cycle with u8, u9 leaving 2 subgoals.
The subproof is completed by applying In_8_9.
Apply H23 with λ x4 x5 . x4 ∈ u8.
The subproof is completed by applying H13.
Assume H23: x1 ∈ u17.
Assume H24: u9 ∈ u17.
Apply unknownprop_08c2582e457fa5da2b4ee2676b94e0e9b149b350b636df86eee53e8e8dded2c1 with λ x4 x5 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . TwoRamseyGraph_3_6_Church17 (u17_to_Church17 x1) x5 = λ x6 x7 . x6.
The subproof is completed by applying H22.
Assume H22: TwoRamseyGraph_3_6_Church17 (u17_to_Church17 x1) (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x13) = λ x4 x5 . x5.
The subproof is completed by applying H22.
Apply unknownprop_46a7f5ba218e301f19d33cc265134a2df7adfd3de64e750dc665649ee8f6340d with u17_to_Church17 x2, λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x12, TwoRamseyGraph_3_6_Church17 (u17_to_Church17 x2) (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x12) = λ x4 x5 . x5 leaving 4 subgoals.
The subproof is completed by applying L20.
The subproof is completed by applying unknownprop_c37600b80efb18922b2424c0ae3622d88c262b6e7e6fb3aa0f6bc2b0ba9f1be7.
Assume H22: TwoRamseyGraph_3_6_Church17 (u17_to_Church17 x2) (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x12) = λ x4 x5 . x4.
Apply FalseE with TwoRamseyGraph_3_6_Church17 (u17_to_Church17 x2) ... = ....
...
...
...
...
...
...
...
...
■