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.
Assume H0: Church13_p x0.
Assume H1: Church13_p x1.
Assume H2: Church13_p x2.
Assume H3: x0 = x1 ⟶ ∀ x3 : ο . x3.
Assume H4: x0 = x2 ⟶ ∀ x3 : ο . x3.
Assume H5: x1 = x2 ⟶ ∀ x3 : ο . x3.
Assume H6: TwoRamseyGraph_3_5_Church13 x0 x1 = λ x3 x4 . x3.
Assume H7: TwoRamseyGraph_3_5_Church13 x1 x2 = λ x3 x4 . x3.
Assume H8: TwoRamseyGraph_3_5_Church13 x0 x2 = λ x3 x4 . x3.
Apply unknownprop_37c1c08bb86d5b4e33948419b156e3861ea73d89bb0a60079717ef1ce7fe0047 with x0, False leaving 2 subgoals.
The subproof is completed by applying H0.
Let x3 of type (ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι be given.
Let x4 of type (ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι be given.
Assume H9: ∀ x5 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church13_p x5 ⟶ Church13_p (x3 x5).
Assume H10: ∀ x5 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church13_p x5 ⟶ Church13_p (x4 x5).
Assume H11: ∀ x5 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . x3 (x4 x5) = x5.
Assume H12: ∀ x5 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . x4 (x3 x5) = x5.
Assume H13: ∀ x5 x6 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church13_p x5 ⟶ Church13_p x6 ⟶ TwoRamseyGraph_3_5_Church13 x5 x6 = TwoRamseyGraph_3_5_Church13 (x3 x5) (x3 x6).
Assume H14: x3 x0 = λ x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 . x5.
Apply unknownprop_ab84de89d5602abf23d4f25476840d5800c1a057ab19ebfe5fa8eab4afa3e505 with x3 x1, x3 x2 leaving 8 subgoals.
Apply H9 with x1.
The subproof is completed by applying H1.
Apply H9 with x2.
The subproof is completed by applying H2.
Apply H14 with λ x5 x6 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . x5 = x3 x1 ⟶ ∀ x7 : ο . x7.
Assume H15: x3 x0 = x3 x1.
Apply H3.
Apply H12 with x0, λ x5 x6 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . x5 = x1.
Apply H12 with x1, λ x5 x6 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . x4 (x3 x0) = x5.
set y5 to be x4 (x3 x0)
set y6 to be y5 (x4 x2)
Claim L16: ∀ x7 : (ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι) → ο . x7 y6 ⟶ x7 y5
Let x7 of type (ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι) → ο be given.
Assume H16: x7 (y6 (y5 x3)).
set y8 to be λ x8 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . x7
Apply H15 with λ x9 x10 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . y8 (y6 x9) (y6 x10).
The subproof is completed by applying H16.
Let x7 of type (ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι) → ο be given.
Apply L16 with λ x8 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . x7 x8 y6 ⟶ x7 y6 x8.
Assume H17: x7 y6 y6.
The subproof is completed by applying H17.
Apply H14 with λ x5 x6 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . x5 = x3 x2 ⟶ ∀ x7 : ο . x7.
Assume H15: x3 x0 = x3 x2.
Apply H4.
Apply H12 with x0, λ x5 x6 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . x5 = x2.
Apply H12 with x2, λ x5 x6 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . x4 (x3 x0) = x5.
set y5 to be x4 (x3 x0)
set y6 to be y5 (x4 x3)
Claim L16: ∀ x7 : (ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι) → ο . x7 y6 ⟶ x7 y5
Let x7 of type (ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι) → ο be given.
Assume H16: x7 (y6 (y5 x4)).
set y8 to be λ x8 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . x7
Apply H15 with λ x9 x10 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . y8 (y6 x9) (y6 x10).
The subproof is completed by applying H16.
Let x7 of type (ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι) → ο be given.
Apply L16 with λ x8 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . x7 x8 y6 ⟶ x7 y6 x8.
Assume H17: x7 y6 y6.
The subproof is completed by applying H17.
Assume H15: x3 x1 = x3 x2.
Apply H5.
Apply H12 with x1, λ x5 x6 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . x5 = x2.
Apply H12 with x2, λ x5 x6 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . x4 (x3 x1) = x5.
set y5 to be ...
set y6 to be ...
Claim L16: ...
...
Let x7 of type (ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι) → ο be given.
Apply L16 with λ x8 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . x7 x8 y6 ⟶ x7 y6 x8.
Assume H17: x7 y6 y6.
The subproof is completed by applying H17.
...
...
...
■