Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: x0 ⊆ u13.
Assume H1: atleastp u3 x0.
Assume H2: ∀ x1 . x1 ∈ x0 ⟶ ∀ x2 . x2 ∈ x0 ⟶ (x1 = x2 ⟶ ∀ x3 : ο . x3) ⟶ TwoRamseyGraph_3_5_13 x1 x2.
Apply unknownprop_95c6cbd2308b27a7edcd2a1d9389b377988e902d740d05dc7c88e6b8da945ab9 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.
Assume H6: x1 = x2 ⟶ ∀ x4 : ο . x4.
Assume H7: x1 = x3 ⟶ ∀ x4 : ο . x4.
Assume H8: x2 = x3 ⟶ ∀ x4 : ο . x4.
Claim L9: ...
...
Claim L10: ...
...
Claim L11: TwoRamseyGraph_3_5_13 x1 x3
...
Apply unknownprop_f13b7928572ea386063941f294a7de5e613d504b56c8df5d720e8c3911580df6 with x1, False leaving 2 subgoals.
Apply H0 with x1.
The subproof is completed by applying H3.
Let x4 of type ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι be given.
Assume H12: Church13_p x4.
Assume H13: x1 = x4 0 u1 u2 u3 u4 u5 u6 u7 u8 u9 u10 u11 u12.
Apply unknownprop_f13b7928572ea386063941f294a7de5e613d504b56c8df5d720e8c3911580df6 with x2, False leaving 2 subgoals.
Apply H0 with x2.
The subproof is completed by applying H4.
Let x5 of type ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι be given.
Assume H14: Church13_p x5.
Assume H15: x2 = x5 0 u1 u2 u3 u4 u5 u6 u7 u8 u9 u10 u11 u12.
Apply unknownprop_f13b7928572ea386063941f294a7de5e613d504b56c8df5d720e8c3911580df6 with x3, False leaving 2 subgoals.
Apply H0 with x3.
The subproof is completed by applying H5.
Let x6 of type ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι be given.
Assume H16: Church13_p x6.
Assume H17: x3 = x6 0 u1 u2 u3 u4 u5 u6 u7 u8 u9 u10 u11 u12.
Claim L18: x4 = x5 ⟶ ∀ x7 : ο . x7
Assume H18: x4 = x5.
Apply H6.
Apply H15 with λ x7 x8 . x1 = x8.
Apply H18 with λ x7 x8 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . x1 = x7 0 u1 u2 u3 u4 u5 u6 u7 u8 u9 u10 u11 u12.
The subproof is completed by applying H13.
Claim L19: x4 = x6 ⟶ ∀ x7 : ο . x7
Assume H19: x4 = x6.
Apply H7.
Apply H17 with λ x7 x8 . x1 = x8.
Apply H19 with λ x7 x8 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . x1 = x7 0 u1 u2 u3 u4 u5 u6 u7 u8 u9 u10 u11 u12.
The subproof is completed by applying H13.
Claim L20: x5 = x6 ⟶ ∀ x7 : ο . x7
Assume H20: x5 = x6.
Apply H8.
Apply H17 with λ x7 x8 . x2 = x8.
Apply H20 with λ x7 x8 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . x2 = x7 0 u1 u2 u3 u4 u5 u6 u7 u8 u9 u10 u11 u12.
The subproof is completed by applying H15.
Claim L21: TwoRamseyGraph_3_5_Church13 x4 x5 = λ x7 x8 . x7
Apply L9 with x4, x5 leaving 4 subgoals.
The subproof is completed by applying H12.
The subproof is completed by applying H14.
The subproof is completed by applying H13.
The subproof is completed by applying H15.
Claim L22: TwoRamseyGraph_3_5_Church13 x5 x6 = λ x7 x8 . x7
Apply L10 with x5, x6 leaving 4 subgoals.
The subproof is completed by applying H14.
The subproof is completed by applying H16.
The subproof is completed by applying H15.
The subproof is completed by applying H17.
Claim L23: TwoRamseyGraph_3_5_Church13 x4 x6 = λ x7 x8 . x7
Apply L11 with x4, x6 leaving 4 subgoals.
The subproof is completed by applying H12.
The subproof is completed by applying H16.
The subproof is completed by applying H13.
The subproof is completed by applying H17.
Apply unknownprop_873d0c5e2eeb5a2985fa84b3e7b54248cf283ca6d92cca41f458c7c4e6e2a64b with x4, x5, x6 leaving 9 subgoals.
The subproof is completed by applying H12.
The subproof is completed by applying H14.
The subproof is completed by applying H16.
The subproof is completed by applying L18.
The subproof is completed by applying L19.
The subproof is completed by applying L20.
The subproof is completed by applying L21.
The subproof is completed by applying L22.
The subproof is completed by applying L23.
■