Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι be given.
Let x1 of type ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι be given.
Let x2 of type ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι be given.
Let x3 of type ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι be given.
Let x4 of type ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι be given.
Assume H0: Church13_p x0.
Assume H1: Church13_p x1.
Assume H2: Church13_p x2.
Assume H3: Church13_p x3.
Assume H4: Church13_p x4.
Assume H5: x0 = x1 ⟶ ∀ x5 : ο . x5.
Assume H6: x0 = x2 ⟶ ∀ x5 : ο . x5.
Assume H7: x0 = x3 ⟶ ∀ x5 : ο . x5.
Assume H8: x0 = x4 ⟶ ∀ x5 : ο . x5.
Assume H9: x1 = x2 ⟶ ∀ x5 : ο . x5.
Assume H10: x1 = x3 ⟶ ∀ x5 : ο . x5.
Assume H11: x1 = x4 ⟶ ∀ x5 : ο . x5.
Assume H12: x2 = x3 ⟶ ∀ x5 : ο . x5.
Assume H13: x2 = x4 ⟶ ∀ x5 : ο . x5.
Assume H14: x3 = x4 ⟶ ∀ x5 : ο . x5.
Assume H15: TwoRamseyGraph_3_5_Church13 x0 x1 = λ x5 x6 . x6.
Assume H16: TwoRamseyGraph_3_5_Church13 x0 x2 = λ x5 x6 . x6.
Assume H17: TwoRamseyGraph_3_5_Church13 x0 x3 = λ x5 x6 . x6.
Assume H18: TwoRamseyGraph_3_5_Church13 x0 x4 = λ x5 x6 . x6.
Assume H19: TwoRamseyGraph_3_5_Church13 x1 x2 = λ x5 x6 . x6.
Assume H20: TwoRamseyGraph_3_5_Church13 x1 x3 = λ x5 x6 . x6.
Assume H21: TwoRamseyGraph_3_5_Church13 x1 x4 = λ x5 x6 . x6.
Assume H22: TwoRamseyGraph_3_5_Church13 x2 x3 = λ x5 x6 . x6.
Assume H23: TwoRamseyGraph_3_5_Church13 x2 x4 = λ x5 x6 . x6.
Assume H24: TwoRamseyGraph_3_5_Church13 x3 x4 = λ x5 x6 . x6.
Apply unknownprop_37c1c08bb86d5b4e33948419b156e3861ea73d89bb0a60079717ef1ce7fe0047 with x0, False leaving 2 subgoals.
The subproof is completed by applying H0.
Let x5 of type (ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι be given.
Let x6 of type (ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι be given.
Assume H25: ∀ x7 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church13_p x7 ⟶ Church13_p (x5 x7).
Assume H26: ∀ x7 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church13_p x7 ⟶ Church13_p (x6 x7).
Assume H27: ∀ x7 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . x5 (x6 x7) = x7.
Assume H28: ∀ x7 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . x6 (x5 x7) = x7.
Assume H29: ∀ x7 x8 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church13_p x7 ⟶ Church13_p x8 ⟶ TwoRamseyGraph_3_5_Church13 x7 x8 = TwoRamseyGraph_3_5_Church13 (x5 x7) (x5 x8).
Assume H30: x5 x0 = λ x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x7.
Apply unknownprop_1ac6c2cb709c59fcef720a9dd88a74b82d0a33f832e6c8c08d3d6a9c6beaa8b4 with x5 x1, x5 x2, x5 x3, x5 x4 leaving 24 subgoals.
Apply H25 with x1.
The subproof is completed by applying H1.
Apply H25 with x2.
The subproof is completed by applying H2.
Apply H25 with x3.
The subproof is completed by applying H3.
Apply H25 with x4.
The subproof is completed by applying H4.
Apply H30 with λ x7 x8 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . x7 = x5 x1 ⟶ ∀ x9 : ο . x9.
Assume H31: x5 x0 = x5 x1.
Apply H5.
Apply H28 with x0, λ x7 x8 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . x7 = x1.
Apply H28 with x1, λ x7 x8 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . x6 (x5 x0) = x7.
set y7 to be x6 (x5 x0)
set y8 to be y7 (x6 x2)
Claim L32: ∀ x9 : (ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι) → ο . x9 y8 ⟶ x9 y7
Let x9 of type (ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι) → ο be given.
Assume H32: x9 (y8 (y7 x3)).
set y10 to be λ x10 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . x9
Apply H31 with λ x11 x12 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . y10 (y8 x11) (y8 x12).
The subproof is completed by applying H32.
Let x9 of type (ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι) → ο be given.
Apply L32 with λ x10 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . x9 x10 y8 ⟶ x9 y8 x10.
Assume H33: x9 y8 y8.
The subproof is completed by applying H33.
Apply H30 with λ x7 x8 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . ... ⟶ ∀ x9 : ο . x9.
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
■