Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι be given.
Assume H0: ∀ x1 . x1 ∈ u17 ⟶ Church17_p (x0 x1).
Assume H1: ∀ x1 . x1 ∈ u17 ⟶ ∀ x2 . x2 ∈ u17 ⟶ x0 x1 = x0 x2 ⟶ x1 = x2.
Let x1 of type ι → ι → ο be given.
Assume H2: ∀ x2 x3 . x1 x2 x3 ⟶ x2 ∈ u17 ⟶ x3 ∈ u17 ⟶ TwoRamseyGraph_3_6_Church17 (x0 x2) (x0 x3) = λ x4 x5 . x4.
Let x2 of type ι be given.
Assume H3: x2 ⊆ u17.
Assume H4: atleastp u3 x2.
Assume H5: ∀ x3 . x3 ∈ x2 ⟶ ∀ x4 . x4 ∈ x2 ⟶ (x3 = x4 ⟶ ∀ x5 : ο . x5) ⟶ x1 x3 x4.
Apply unknownprop_95c6cbd2308b27a7edcd2a1d9389b377988e902d740d05dc7c88e6b8da945ab9 with x2, False leaving 2 subgoals.
The subproof is completed by applying H4.
Let x3 of type ι be given.
Assume H6: x3 ∈ x2.
Let x4 of type ι be given.
Assume H7: x4 ∈ x2.
Let x5 of type ι be given.
Assume H8: x5 ∈ x2.
Assume H9: x3 = x4 ⟶ ∀ x6 : ο . x6.
Assume H10: x3 = x5 ⟶ ∀ x6 : ο . x6.
Assume H11: x4 = x5 ⟶ ∀ x6 : ο . x6.
Claim L12: x3 ∈ u17
Apply H3 with x3.
The subproof is completed by applying H6.
Claim L13: x4 ∈ u17
Apply H3 with x4.
The subproof is completed by applying H7.
Claim L14: x5 ∈ u17
Apply H3 with x5.
The subproof is completed by applying H8.
Claim L15: TwoRamseyGraph_3_6_Church17 (x0 x3) (x0 x4) = λ x6 x7 . x6
Apply H2 with x3, x4 leaving 3 subgoals.
Apply H5 with x3, x4 leaving 3 subgoals.
The subproof is completed by applying H6.
The subproof is completed by applying H7.
The subproof is completed by applying H9.
The subproof is completed by applying L12.
The subproof is completed by applying L13.
Claim L16: TwoRamseyGraph_3_6_Church17 (x0 x4) (x0 x5) = λ x6 x7 . x6
Apply H2 with x4, x5 leaving 3 subgoals.
Apply H5 with x4, x5 leaving 3 subgoals.
The subproof is completed by applying H7.
The subproof is completed by applying H8.
The subproof is completed by applying H11.
The subproof is completed by applying L13.
The subproof is completed by applying L14.
Claim L17: TwoRamseyGraph_3_6_Church17 (x0 x3) (x0 x5) = λ x6 x7 . x6
Apply H2 with x3, x5 leaving 3 subgoals.
Apply H5 with x3, x5 leaving 3 subgoals.
The subproof is completed by applying H6.
The subproof is completed by applying H8.
The subproof is completed by applying H10.
The subproof is completed by applying L12.
The subproof is completed by applying L14.
Claim L18: x0 x3 = x0 x4 ⟶ ∀ x6 : ο . x6
Assume H18: x0 x3 = x0 x4.
Apply H9.
Apply H1 with x3, x4 leaving 3 subgoals.
The subproof is completed by applying L12.
The subproof is completed by applying L13.
The subproof is completed by applying H18.
Claim L19: x0 x3 = x0 x5 ⟶ ∀ x6 : ο . x6
Assume H19: x0 x3 = x0 x5.
Apply H10.
Apply H1 with x3, x5 leaving 3 subgoals.
The subproof is completed by applying L12.
The subproof is completed by applying L14.
The subproof is completed by applying H19.
Claim L20: x0 x4 = x0 x5 ⟶ ∀ x6 : ο . x6
Assume H20: x0 x4 = x0 x5.
Apply H11.
Apply H1 with x4, x5 leaving 3 subgoals.
The subproof is completed by applying L13.
The subproof is completed by applying L14.
The subproof is completed by applying H20.
Apply unknownprop_cbcfee5dff5e691bd336d521185cf4e19ac6075512774f25fde1bea7c0141e4d with x0 x3, x0 x4, x0 x5 leaving 9 subgoals.
Apply H0 with x3.
The subproof is completed by applying L12.
Apply H0 with x4.
The subproof is completed by applying L13.
Apply H0 with x5.
The subproof is completed by applying L14.
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 L15.
The subproof is completed by applying L17.
The subproof is completed by applying L16.
■