Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: x0 ⊆ u17.
Assume H1: atleastp u4 x0.
Assume H2: ∀ x1 . x1 ∈ x0 ⟶ ∀ x2 . x2 ∈ x0 ⟶ (x1 = x2 ⟶ ∀ x3 : ο . x3) ⟶ not (TwoRamseyGraph_4_4_17 x1 x2).
Apply unknownprop_19c5bea28ef119e30d80f4e7c578df826b34bc3d0b15978a12c7c1b896ec3046 with x0, False leaving 2 subgoals.
The subproof is completed by applying H1.
Let x1 of type ι be given.
Assume H3: x1 ∈ x0.
Let x2 of type ι be given.
Assume H4: x2 ∈ x0.
Let x3 of type ι be given.
Assume H5: x3 ∈ x0.
Let x4 of type ι be given.
Assume H6: x4 ∈ x0.
Assume H7: x1 = x2 ⟶ ∀ x5 : ο . x5.
Assume H8: x1 = x3 ⟶ ∀ x5 : ο . x5.
Assume H9: x1 = x4 ⟶ ∀ x5 : ο . x5.
Assume H10: x2 = x3 ⟶ ∀ x5 : ο . x5.
Assume H11: x2 = x4 ⟶ ∀ x5 : ο . x5.
Assume H12: x3 = x4 ⟶ ∀ x5 : ο . x5.
Claim L13: ...
...
Claim L14: ...
...
Claim L15: ...
...
Claim L16: ...
...
Claim L17: ...
...
Claim L18: ...
...
Apply unknownprop_fa363309151222d666a5df6648c3d7cbb9db9b9ba87cc04000ea2b8b969c70c7 with x1, False leaving 2 subgoals.
Apply H0 with x1.
The subproof is completed by applying H3.
Let x5 of type ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι be given.
Assume H19: Church17_p x5.
Assume H20: x1 = x5 0 u1 u2 u3 u4 u5 u6 u7 u8 u9 u10 u11 u12 u13 u14 u15 u16.
Apply unknownprop_fa363309151222d666a5df6648c3d7cbb9db9b9ba87cc04000ea2b8b969c70c7 with x2, False leaving 2 subgoals.
Apply H0 with x2.
The subproof is completed by applying H4.
Let x6 of type ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι be given.
Assume H21: Church17_p x6.
Assume H22: x2 = x6 0 u1 u2 u3 u4 u5 u6 u7 u8 u9 u10 u11 u12 u13 u14 u15 u16.
Apply unknownprop_fa363309151222d666a5df6648c3d7cbb9db9b9ba87cc04000ea2b8b969c70c7 with x3, False leaving 2 subgoals.
Apply H0 with x3.
The subproof is completed by applying H5.
Let x7 of type ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι be given.
Assume H23: Church17_p x7.
Assume H24: x3 = x7 0 u1 u2 u3 u4 u5 u6 u7 u8 u9 u10 u11 u12 u13 u14 u15 u16.
Apply unknownprop_fa363309151222d666a5df6648c3d7cbb9db9b9ba87cc04000ea2b8b969c70c7 with x4, False leaving 2 subgoals.
Apply H0 with x4.
The subproof is completed by applying H6.
Let x8 of type ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι be given.
Assume H25: Church17_p x8.
Assume H26: x4 = x8 0 u1 u2 u3 u4 u5 u6 u7 u8 u9 u10 u11 u12 u13 u14 u15 u16.
Claim L27: ...
...
Claim L28: ...
...
Claim L29: ...
...
Claim L30: ...
...
Claim L31: ...
...
Claim L32: ...
...
Claim L33: ...
...
Claim L34: ...
...
Claim L35: ...
...
Claim L36: ...
...
Claim L37: ...
...
Claim L38: ...
...
Claim L39: TwoRamseyGraph_4_4_Church17 x7 x8 = λ x9 x10 . x10
Apply unknownprop_805df3bfbf10a3f532039c4e52b4f89518eefb765fbde3dea103a4efdc804215 with x7, x8, TwoRamseyGraph_4_4_Church17 x7 x8 = λ x9 x10 . x10 leaving 4 subgoals.
The subproof is completed by applying H23.
The subproof is completed by applying H25.
Assume H39: TwoRamseyGraph_4_4_Church17 x7 x8 = λ x9 x10 . x9.
Apply FalseE with TwoRamseyGraph_4_4_Church17 x7 x8 = λ x9 x10 . x10.
Apply L18.
Let x9 of type ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι be given.
Let x10 of type ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι be given.
Assume H40: Church17_p x9.
Assume H41: Church17_p x10.
Assume H42: x3 = x9 0 u1 u2 u3 u4 u5 u6 u7 u8 u9 u10 u11 u12 u13 u14 u15 u16.
Assume H43: x4 = x10 0 u1 u2 u3 u4 u5 u6 u7 u8 u9 u10 u11 ... ... ... ... ....
...
...
Apply unknownprop_0622a2b3aafa59ebcc3706a1ebb97b2d68596d563b882a30d4a0969ed018220b with x5, x6, x7, x8 leaving 16 subgoals.
The subproof is completed by applying H19.
The subproof is completed by applying H21.
The subproof is completed by applying H23.
The subproof is completed by applying H25.
The subproof is completed by applying L27.
The subproof is completed by applying L28.
The subproof is completed by applying L29.
The subproof is completed by applying L30.
The subproof is completed by applying L31.
The subproof is completed by applying L32.
The subproof is completed by applying L34.
The subproof is completed by applying L35.
The subproof is completed by applying L36.
The subproof is completed by applying L37.
The subproof is completed by applying L38.
The subproof is completed by applying L39.
■