Search for blocks/addresses/...

Proofgold Proof

pf
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.
Let x6 of type ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι) be given.
Let x7 of type ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι) be given.
Let x8 of type ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι) be given.
Let x9 of type ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι) be given.
Assume H0: ChurchNum_3ary_proj_p x0.
Assume H1: ChurchNum_3ary_proj_p x1.
Assume H2: ChurchNum_3ary_proj_p x2.
Assume H3: ChurchNum_3ary_proj_p x3.
Assume H4: ChurchNum_3ary_proj_p x4.
Assume H5: ChurchNum_8ary_proj_p x5.
Assume H6: ChurchNum_8ary_proj_p x6.
Assume H7: ChurchNum_8ary_proj_p x7.
Assume H8: ChurchNum_8ary_proj_p x8.
Assume H9: ChurchNum_8ary_proj_p x9.
Assume H10: TwoRamseyGraph_4_5_24_ChurchNums_3x8 x0 x5 x1 x6 = λ x10 x11 . x11.
Assume H11: TwoRamseyGraph_4_5_24_ChurchNums_3x8 x0 x5 x2 x7 = λ x10 x11 . x11.
Assume H12: TwoRamseyGraph_4_5_24_ChurchNums_3x8 x0 x5 x3 x8 = λ x10 x11 . x11.
Assume H13: TwoRamseyGraph_4_5_24_ChurchNums_3x8 x0 x5 x4 x9 = λ x10 x11 . x11.
Assume H14: TwoRamseyGraph_4_5_24_ChurchNums_3x8 x1 x6 x2 x7 = λ x10 x11 . x11.
Assume H15: TwoRamseyGraph_4_5_24_ChurchNums_3x8 x1 x6 x3 x8 = λ x10 x11 . x11.
Assume H16: TwoRamseyGraph_4_5_24_ChurchNums_3x8 x1 x6 x4 x9 = λ x10 x11 . x11.
Assume H17: TwoRamseyGraph_4_5_24_ChurchNums_3x8 x2 x7 x3 x8 = λ x10 x11 . x11.
Assume H18: TwoRamseyGraph_4_5_24_ChurchNums_3x8 x2 x7 x4 x9 = λ x10 x11 . x11.
Assume H19: TwoRamseyGraph_4_5_24_ChurchNums_3x8 x3 x8 x4 x9 = λ x10 x11 . x11.
Let x10 of type (((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι)) → (((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι)) → ι be given.
Assume H20: ∀ x11 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x12 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ap (x10 x11 x12) 0 = ChurchNums_3x8_to_u24 x11 x12.
Assume H21: ∀ x11 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x12 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ap (x10 x11 x12) u1 = ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt7_id_ge7_rot2 x12 x11) (ChurchNums_8_perm_1_2_3_4_5_6_7_0 x12).
Assume H22: ∀ x11 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x12 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ap (x10 x11 x12) u2 = ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt6_id_ge6_rot2 x12 x11) (ChurchNums_8_perm_2_3_4_5_6_7_0_1 x12).
Assume H23: ∀ x11 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x12 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ap (x10 x11 x12) u3 = ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt5_id_ge5_rot2 x12 x11) (ChurchNums_8_perm_3_4_5_6_7_0_1_2 x12).
Assume H24: ∀ x11 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x12 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ap (x10 x11 x12) u4 = ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt4_id_ge4_rot2 x12 x11) (ChurchNums_8_perm_4_5_6_7_0_1_2_3 x12).
Assume H25: ∀ x11 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x12 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_3ary_proj_p x11 ⟶ ChurchNum_8ary_proj_p x12 ⟶ ∀ x13 . x13 ∈ u5 ⟶ ∀ x14 . x14 ∈ u5 ⟶ ap (x10 x11 x12) x13 = ap (x10 x11 x12) x14 ⟶ x13 = x14.
Assume H26: ∀ x11 x12 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x13 x14 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ... ⟶ ... ⟶ ... ⟶ ... ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 x11 x13 x12 x14 = λ x15 x16 . x16) ⟶ ∀ x15 . x15 ∈ u5 ⟶ ∀ x16 . x16 ∈ u5 ⟶ ap (x10 x11 x13) x15 = ap (x10 x12 x14) x16 ⟶ ∀ x17 : ο . (x12 = ChurchNums_8x3_to_3_lt5_id_ge5_rot2 x13 x11 ⟶ x14 = ChurchNums_8_perm_3_4_5_6_7_0_1_2 x13 ⟶ x17) ⟶ (x11 = ChurchNums_8x3_to_3_lt5_id_ge5_rot2 x14 x12 ⟶ x13 = ChurchNums_8_perm_3_4_5_6_7_0_1_2 x14 ⟶ x17) ⟶ x17.
...
■