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.
Apply unknownprop_d2bdc72216c61557c2c68a0fa574d18b9f5fc8558043c48c267a1d8bcfe1eba5 with x0, x3, (TwoRamseyGraph_4_5_24_ChurchNums_3x8 (λ x6 x7 x8 : (ι → ι) → ι → ι . x6) (λ x6 x7 x8 x9 x10 x11 x12 x13 : (ι → ι) → ι → ι . x9) x0 x3 = λ x6 x7 . x7) ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 (λ x6 x7 x8 : (ι → ι) → ι → ι . x6) (λ x6 x7 x8 x9 x10 x11 x12 x13 : (ι → ι) → ι → ι . x9) x1 x4 = λ x6 x7 . x7) ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 (λ x6 x7 x8 : (ι → ι) → ι → ι . x6) (λ x6 x7 x8 x9 x10 x11 x12 x13 : (ι → ι) → ι → ι . x9) x2 x5 = λ x6 x7 . x7) ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 x0 x3 x1 x4 = λ x6 x7 . x7) ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 x0 x3 x2 x5 = λ x6 x7 . x7) ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 x1 x4 x2 x5 = λ x6 x7 . x7) ⟶ ∀ x6 : ο . ((x0 = λ x7 x8 x9 : (ι → ι) → ι → ι . x8) ⟶ (x3 = λ x7 x8 x9 x10 x11 x12 x13 x14 : (ι → ι) → ι → ι . x9) ⟶ x6) ⟶ ((x0 = λ x7 x8 x9 : (ι → ι) → ι → ι . x8) ⟶ (x3 = λ x7 x8 x9 x10 x11 x12 x13 x14 : (ι → ι) → ι → ι . x12) ⟶ x6) ⟶ ((x0 = λ x7 x8 x9 : (ι → ι) → ι → ι . x8) ⟶ (x3 = λ x7 x8 x9 x10 x11 x12 x13 x14 : (ι → ι) → ι → ι . x13) ⟶ x6) ⟶ ((x0 = λ x7 x8 x9 : (ι → ι) → ι → ι . x9) ⟶ (x3 = λ x7 x8 x9 x10 x11 x12 x13 x14 : (ι → ι) → ι → ι . x8) ⟶ x6) ⟶ ((x0 = λ x7 x8 x9 : (ι → ι) → ι → ι . x9) ⟶ (x3 = λ x7 x8 x9 x10 x11 x12 x13 x14 : (ι → ι) → ι → ι . x12) ⟶ x6) ⟶ x6 leaving 16 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H4.
The subproof is completed by applying H7.
Assume H10: x0 = λ x6 x7 x8 : (ι → ι) → ι → ι . x6.
Assume H11: x3 = λ x6 x7 x8 x9 x10 x11 x12 x13 : (ι → ι) → ι → ι . x9.
Apply H10 with λ x6 x7 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . (TwoRamseyGraph_4_5_24_ChurchNums_3x8 (λ x8 x9 x10 : (ι → ι) → ι → ι . x8) (λ x8 x9 x10 x11 x12 x13 x14 x15 : (ι → ι) → ι → ι . x11) x7 x3 = λ x8 x9 . x9) ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 (λ x8 x9 x10 : (ι → ι) → ι → ι . x8) (λ x8 x9 x10 x11 x12 x13 x14 x15 : (ι → ι) → ι → ι . x11) x1 x4 = λ x8 x9 . x9) ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 (λ x8 x9 x10 : (ι → ι) → ι → ι . x8) (λ x8 x9 x10 x11 x12 x13 x14 x15 : (ι → ι) → ι → ι . x11) x2 x5 = λ x8 x9 . x9) ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 x7 x3 x1 x4 = λ x8 x9 . x9) ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 x7 x3 x2 x5 = λ x8 x9 . x9) ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 x1 x4 x2 x5 = λ x8 x9 . x9) ⟶ ∀ x8 : ο . ((x7 = λ x9 x10 x11 : (ι → ι) → ι → ι . x10) ⟶ (x3 = λ x9 x10 x11 x12 x13 x14 x15 x16 : (ι → ι) → ι → ι . x11) ⟶ x8) ⟶ ((x7 = λ x9 x10 x11 : (ι → ι) → ι → ι . x10) ⟶ (x3 = λ x9 x10 x11 x12 x13 x14 x15 x16 : (ι → ι) → ι → ι . x14) ⟶ x8) ⟶ ((x7 = λ x9 x10 x11 : (ι → ι) → ι → ι . x10) ⟶ (x3 = λ x9 x10 x11 x12 x13 x14 x15 x16 : (ι → ι) → ι → ι . x15) ⟶ x8) ⟶ ((x7 = λ x9 x10 x11 : (ι → ι) → ι → ι . x11) ⟶ (x3 = λ x9 x10 x11 x12 x13 x14 x15 x16 : (ι → ι) → ι → ι . x10) ⟶ x8) ⟶ ((x7 = λ x9 x10 x11 : (ι → ι) → ι → ι . x11) ⟶ (x3 = λ x9 x10 x11 x12 x13 x14 x15 x16 : (ι → ι) → ι → ι . x14) ⟶ x8) ⟶ x8.
Apply H11 with λ x6 x7 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ... ⟶ ... ⟶ ... ⟶ ... ⟶ ... ⟶ ... ⟶ ∀ x8 : ο . ... ⟶ ... ⟶ ... ⟶ ... ⟶ (... ⟶ x7 = ... ⟶ x8) ⟶ x8.
...
...
...
...
...
...
...
...
...
...
...
...
...
■