Search for blocks/addresses/...

Proofgold Proof

pf
Claim L0: ...
...
Let x0 of type ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι) be given.
Let x1 of type ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι) be given.
Let x2 of type ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι) be given.
Let x3 of type ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι) be given.
Let x4 of type ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι) be given.
Let x5 of type ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι) be given.
Assume H1: ChurchNum_3ary_proj_p x0.
Assume H2: ChurchNum_3ary_proj_p x1.
Assume H3: ChurchNum_3ary_proj_p x2.
Assume H4: ChurchNum_8ary_proj_p x3.
Assume H5: ChurchNum_8ary_proj_p x4.
Assume H6: ChurchNum_8ary_proj_p x5.
Assume H7: TwoRamseyGraph_4_5_24_ChurchNums_3x8 (λ x6 x7 x8 : (ι → ι) → ι → ι . x6) (λ x6 x7 x8 x9 x10 x11 x12 x13 : (ι → ι) → ι → ι . x6) x0 x3 = λ x6 x7 . x7.
Assume H8: TwoRamseyGraph_4_5_24_ChurchNums_3x8 (λ x6 x7 x8 : (ι → ι) → ι → ι . x6) (λ x6 x7 x8 x9 x10 x11 x12 x13 : (ι → ι) → ι → ι . x6) x1 x4 = λ x6 x7 . x7.
Assume H9: TwoRamseyGraph_4_5_24_ChurchNums_3x8 (λ x6 x7 x8 : (ι → ι) → ι → ι . x6) (λ x6 x7 x8 x9 x10 x11 x12 x13 : (ι → ι) → ι → ι . x6) x2 x5 = λ x6 x7 . x7.
Assume H10: TwoRamseyGraph_4_5_24_ChurchNums_3x8 (λ x6 x7 x8 : (ι → ι) → ι → ι . x6) (λ x6 x7 x8 x9 x10 x11 x12 x13 : (ι → ι) → ι → ι . x9) x0 x3 = λ x6 x7 . x7.
Assume H11: TwoRamseyGraph_4_5_24_ChurchNums_3x8 (λ x6 x7 x8 : (ι → ι) → ι → ι . x6) (λ x6 x7 x8 x9 x10 x11 x12 x13 : (ι → ι) → ι → ι . x9) x1 x4 = λ x6 x7 . x7.
Assume H12: TwoRamseyGraph_4_5_24_ChurchNums_3x8 (λ x6 x7 x8 : (ι → ι) → ι → ι . x6) (λ x6 x7 x8 x9 x10 x11 x12 x13 : (ι → ι) → ι → ι . x9) x2 x5 = λ x6 x7 . x7.
Assume H13: TwoRamseyGraph_4_5_24_ChurchNums_3x8 x0 x3 x1 x4 = λ x6 x7 . x7.
Assume H14: TwoRamseyGraph_4_5_24_ChurchNums_3x8 x0 x3 x2 x5 = λ x6 x7 . x7.
Assume H15: TwoRamseyGraph_4_5_24_ChurchNums_3x8 x1 x4 x2 x5 = λ x6 x7 . x7.
Claim L16: ...
...
Claim L17: ...
...
Claim L18: ...
...
Apply unknownprop_7567a5f7b9f72f46492d3565224993c701b43caf8236745d250970a5a196a98f with x0, x1, x2, x3, x4, x5, False leaving 20 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
The subproof is completed by applying H4.
The subproof is completed by applying H5.
The subproof is completed by applying H6.
The subproof is completed by applying H7.
The subproof is completed by applying H8.
The subproof is completed by applying H9.
The subproof is completed by applying H10.
The subproof is completed by applying H11.
The subproof is completed by applying H12.
The subproof is completed by applying H13.
The subproof is completed by applying H14.
The subproof is completed by applying H15.
Assume H19: x0 = λ x6 x7 x8 : (ι → ι) → ι → ι . x7.
Assume H20: x3 = λ x6 x7 x8 x9 x10 x11 x12 x13 : (ι → ι) → ι → ι . x8.
Apply unknownprop_7567a5f7b9f72f46492d3565224993c701b43caf8236745d250970a5a196a98f with x1, x0, x2, x4, x3, x5, False leaving 20 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H1.
The subproof is completed by applying H3.
The subproof is completed by applying H5.
The subproof is completed by applying H4.
The subproof is completed by applying H6.
The subproof is completed by applying H8.
The subproof is completed by applying H7.
The subproof is completed by applying H9.
The subproof is completed by applying H11.
The subproof is completed by applying H10.
The subproof is completed by applying H12.
The subproof is completed by applying L16.
The subproof is completed by applying H15.
The subproof is completed by applying H14.
Assume H21: x1 = λ x6 x7 x8 : (ι → ι) → ι → ι . x7.
Assume H22: x4 = λ x6 x7 x8 x9 x10 x11 x12 x13 : (ι → ι) → ι → ι . x8.
Claim L23: (TwoRamseyGraph_4_5_24_ChurchNums_3x8 x0 x3 x1 x4 = λ x6 x7 . x7) ⟶ False
Apply H19 with λ x6 x7 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . (TwoRamseyGraph_4_5_24_ChurchNums_3x8 x7 x3 x1 x4 = λ x8 x9 . x9) ⟶ False.
Apply H20 with λ x6 x7 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . (TwoRamseyGraph_4_5_24_ChurchNums_3x8 (λ x8 x9 x10 : (ι → ι) → ι → ι . x9) x7 x1 x4 = λ x8 x9 . x9) ⟶ False.
Apply H21 with λ x6 x7 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . (TwoRamseyGraph_4_5_24_ChurchNums_3x8 (λ x8 x9 x10 : (ι → ι) → ι → ι . x9) (λ x8 x9 x10 x11 x12 x13 x14 x15 : (ι → ι) → ι → ι . x10) x7 x4 = λ x8 x9 . x9) ⟶ False.
Apply H22 with λ x6 x7 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . (TwoRamseyGraph_4_5_24_ChurchNums_3x8 (λ x8 x9 x10 : (ι → ι) → ι → ι . x9) (λ x8 x9 x10 x11 x12 x13 x14 x15 : (ι → ι) → ι → ι . x10) (λ x8 x9 x10 : (ι → ι) → ι → ι . x9) x7 = λ x8 x9 . x9) ⟶ False.
Assume H23: TwoRamseyGraph_4_5_24_ChurchNums_3x8 (λ x6 x7 x8 : (ι → ι) → ι → ι . x7) (λ x6 x7 x8 x9 x10 x11 x12 x13 : (ι → ι) → ι → ι . x8) (λ x6 x7 x8 : (ι → ι) → ι → ι . x7) (λ x6 x7 x8 x9 x10 x11 x12 x13 : (ι → ι) → ι → ι . x8) = λ x6 x7 . x7.
Apply L0.
The subproof is completed by applying H23.
Apply L23.
The subproof is completed by applying H13.
Assume H21: x1 = λ x6 x7 x8 : (ι → ι) → ι → ι . x7.
Assume H22: x4 = λ x6 x7 x8 x9 x10 x11 x12 x13 : (ι → ι) → ι → ι . x11.
Apply unknownprop_7567a5f7b9f72f46492d3565224993c701b43caf8236745d250970a5a196a98f with x2, x0, x1, x5, x3, x4, False leaving 20 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
The subproof is completed by applying H6.
The subproof is completed by applying H4.
The subproof is completed by applying H5.
The subproof is completed by applying H9.
The subproof is completed by applying H7.
The subproof is completed by applying H8.
The subproof is completed by applying H12.
The subproof is completed by applying H10.
The subproof is completed by applying H11.
The subproof is completed by applying L17.
The subproof is completed by applying L18.
The subproof is completed by applying H13.
Assume H23: x2 = λ x6 x7 x8 : (ι → ι) → ι → ι . x7.
Assume H24: x5 = λ x6 x7 x8 x9 x10 x11 x12 x13 : (ι → ι) → ι → ι . x8.
Claim L25: (TwoRamseyGraph_4_5_24_ChurchNums_3x8 x0 x3 x2 x5 = λ x6 x7 . x7) ⟶ False
Apply H19 with λ x6 x7 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ... = ... ⟶ False.
...
Apply L25.
The subproof is completed by applying H14.
...
...
...
...
...
...
...
...
...
...
...
■