Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: x0 ⊆ u16.
Assume H1: atleastp u6 x0.
Assume H2: ∀ x1 . x1 ∈ x0 ⟶ ∀ x2 . x2 ∈ x0 ⟶ (x1 = x2 ⟶ ∀ x3 : ο . x3) ⟶ not (TwoRamseyGraph_3_6_17 x1 x2).
Claim L3: ...
...
Claim L4: ...
...
Claim L5: ...
...
Claim L6: ...
...
Claim L7: ...
...
Claim L8: ...
...
Claim L9: ...
...
Claim L10: ...
...
Claim L11: ...
...
Claim L12: ...
...
Claim L13: ...
...
Claim L14: ...
...
Claim L15: ...
...
Claim L16: ...
...
Claim L17: ...
...
Claim L18: ...
...
Claim L19: ...
...
Claim L20: ...
...
Claim L21: ...
...
Claim L22: (λ x1 x2 . and (TwoRamseyGraph_3_6_17 x1 x2) (x1 = x2 ⟶ ∀ x3 : ο . x3)) 0 u7
Apply andI with TwoRamseyGraph_3_6_17 0 u7, 0 = u7 ⟶ ∀ x1 : ο . x1 leaving 2 subgoals.
Assume H22: 0 ∈ u17.
Assume H23: u7 ∈ u17.
Apply unknownprop_84aaefca7211a57d89e0df96a1f742653d3cc05f82d5ab568090ade3cb9ffcfd with λ x1 x2 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . TwoRamseyGraph_3_6_Church17 x2 (u17_to_Church17 u7) = λ x3 x4 . x3.
Apply unknownprop_9d497d8c5ab47bb0417256780d394d93b6598b5e679bac7f2c3c702196ebcca4 with λ x1 x2 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . TwoRamseyGraph_3_6_Church17 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x3) x2 = λ x3 x4 . x3.
Let x1 of type (ι → ι → ι) → (ι → ι → ι) → ο be given.
Assume H24: ....
...
...
Claim L23: (λ x1 x2 . and (TwoRamseyGraph_3_6_17 x1 x2) (x1 = x2 ⟶ ∀ x3 : ο . x3)) u10 u14
Apply andI with TwoRamseyGraph_3_6_17 u10 u14, u10 = u14 ⟶ ∀ x1 : ο . x1 leaving 2 subgoals.
Assume H23: u10 ∈ u17.
Assume H24: u14 ∈ u17.
Apply unknownprop_c1a95e8160789154b1ae102566f570f1aea3813572fb362eeefeb21832fd0653 with λ x1 x2 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . TwoRamseyGraph_3_6_Church17 x2 (u17_to_Church17 u14) = λ x3 x4 . x3.
Apply unknownprop_c9b34bc382b6d599e61c555eac34a76c451754eb682c17d99a93f2a1e695d561 with λ x1 x2 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . TwoRamseyGraph_3_6_Church17 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x13) x2 = λ x3 x4 . x3.
Let x1 of type (ι → ι → ι) → (ι → ι → ι) → ο be given.
Assume H25: x1 (TwoRamseyGraph_3_6_Church17 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x12) (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x16)) (λ x2 x3 . x2).
The subproof is completed by applying H25.
Assume H23: u10 = u14.
Apply unknownprop_3e7054688acb8ba4a0f18423b649f383cf90ecfc4f6200e2e049d580ebc2dc1f.
Let x1 of type ι → ι → ο be given.
The subproof is completed by applying H23 with λ x2 x3 . x1 x3 x2.
Apply unknownprop_c18b6193e550b83006174e9a39facd53a8842bb45a3743eb46ab3a970c091d9d with λ x1 x2 . and (TwoRamseyGraph_3_6_17 x1 x2) (x1 = x2 ⟶ ∀ x3 : ο . x3), u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12, x0, False leaving 14 subgoals.
The subproof is completed by applying unknownprop_9c7296d0e1b426393b918922dca14768e21a9144fb20f59ffa35f52b8b015e54.
The subproof is completed by applying unknownprop_ac5261da9745d31a8bb999158a58d18491f973a34391722145ebc7375438f7d8.
The subproof is completed by applying L4.
The subproof is completed by applying unknownprop_6e747c16685bdb4eaee901f472b70c0f041f4106aa60440cc165be6e8835727d.
The subproof is completed by applying unknownprop_c21ba5695b1d95da76a10179e8a88254ffe230dfdf6a6df2f9b5ee9d0562acd5.
The subproof is completed by applying unknownprop_ffb148d18f258a6f2e8b9af29fd6bea695bdd737e09f02c9ed6ace715b49951e.
The subproof is completed by applying unknownprop_5236a0eac529d064f7d4286c27876c5cf1e6aa8482e677668f1eb521e10e6be9.
The subproof is completed by applying unknownprop_991646d91cf5e2f3eac2db7f6827c54bc2cbba5f33c26bd9a4d54268790991f8.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying L3.
The subproof is completed by applying L5.
Let x1 of type ι be given.
Assume H24: x1 ⊆ u16.
Assume H25: atleastp u6 x1.
Assume H26: ∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ not (and (TwoRamseyGraph_3_6_17 x2 x3) (x2 = x3 ⟶ ∀ x4 : ο . x4)).
Assume H27: u12 ∈ x1.
Assume H28: u13 ∈ x1.
Apply unknownprop_85e35c3e63ae72d4bc8526ee5d4148db605a84f9758edbfa851d2df21f3fa608 with λ x2 x3 . and (TwoRamseyGraph_3_6_17 x2 x3) (x2 = x3 ⟶ ∀ x4 : ο . x4), x1 leaving 22 subgoals.
The subproof is completed by applying L6.
The subproof is completed by applying L7.
The subproof is completed by applying L8.
The subproof is completed by applying L9.
The subproof is completed by applying L10.
The subproof is completed by applying L11.
The subproof is completed by applying L12.
The subproof is completed by applying L13.
The subproof is completed by applying L14.
The subproof is completed by applying L15.
The subproof is completed by applying L16.
The subproof is completed by applying L17.
The subproof is completed by applying L18.
The subproof is completed by applying L19.
The subproof is completed by applying L6.
The subproof is completed by applying L7.
The subproof is completed by applying L20.
The subproof is completed by applying H24.
The subproof is completed by applying H25.
The subproof is completed by applying H27.
The subproof is completed by applying H28.
The subproof is completed by applying H26.
Let x1 of type ι be given.
Assume H24: x1 ⊆ u16.
Assume H25: atleastp u6 x1.
Assume H26: ∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ not (and (TwoRamseyGraph_3_6_17 x2 x3) (x2 = x3 ⟶ ∀ x4 : ο . x4)).
Assume H27: u12 ∈ x1.
Assume H28: u14 ∈ x1.
Apply unknownprop_0000c65f9de36d25804b682992bd488961ddb64d511e3c734ef831a829c7802f with λ x2 x3 . and (TwoRamseyGraph_3_6_17 x2 x3) (x2 = x3 ⟶ ∀ x4 : ο . x4), x1 leaving 22 subgoals.
The subproof is completed by applying L6.
The subproof is completed by applying L7.
The subproof is completed by applying L8.
The subproof is completed by applying L9.
The subproof is completed by applying L10.
The subproof is completed by applying L11.
The subproof is completed by applying L12.
The subproof is completed by applying L13.
The subproof is completed by applying L14.
The subproof is completed by applying L15.
The subproof is completed by applying L16.
The subproof is completed by applying L17.
The subproof is completed by applying L18.
The subproof is completed by applying L19.
The subproof is completed by applying L21.
The subproof is completed by applying L22.
The subproof is completed by applying L23.
The subproof is completed by applying H24.
The subproof is completed by applying H25.
The subproof is completed by applying H27.
The subproof is completed by applying H28.
The subproof is completed by applying H26.
■