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) ⟶ 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: x7 = x8 ⟶ ∀ x9 : ο . x9
Assume H32: x7 = x8.
...
Claim L33: TwoRamseyGraph_4_4_Church17 x5 x6 = λ x9 x10 . x9
Apply L13 with x5, x6 leaving 4 subgoals.
The subproof is completed by applying H19.
The subproof is completed by applying H21.
The subproof is completed by applying H20.
The subproof is completed by applying H22.
Claim L34: TwoRamseyGraph_4_4_Church17 x5 x7 = λ x9 x10 . x9
Apply L14 with x5, x7 leaving 4 subgoals.
The subproof is completed by applying H19.
The subproof is completed by applying H23.
The subproof is completed by applying H20.
The subproof is completed by applying H24.
Claim L35: TwoRamseyGraph_4_4_Church17 x5 x8 = λ x9 x10 . x9
Apply L15 with x5, x8 leaving 4 subgoals.
The subproof is completed by applying H19.
The subproof is completed by applying H25.
The subproof is completed by applying H20.
The subproof is completed by applying H26.
Claim L36: TwoRamseyGraph_4_4_Church17 x6 x7 = λ x9 x10 . x9
Apply L16 with x6, x7 leaving 4 subgoals.
The subproof is completed by applying H21.
The subproof is completed by applying H23.
The subproof is completed by applying H22.
The subproof is completed by applying H24.
Claim L37: TwoRamseyGraph_4_4_Church17 x6 x8 = λ x9 x10 . x9
Apply L17 with x6, x8 leaving 4 subgoals.
The subproof is completed by applying H21.
The subproof is completed by applying H25.
The subproof is completed by applying H22.
The subproof is completed by applying H26.
Claim L38: TwoRamseyGraph_4_4_Church17 x7 x8 = λ x9 x10 . x9
Apply L18 with x7, x8 leaving 4 subgoals.
The subproof is completed by applying H23.
The subproof is completed by applying H25.
The subproof is completed by applying H24.
The subproof is completed by applying H26.
Apply unknownprop_600304c5ef13e538022ba8291ad91324a1e2aaa5ae55e716967d35f2c83846df 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 L33.
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.
■