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.
Assume H0: ChurchNum_3ary_proj_p x0.
Assume H1: ChurchNum_3ary_proj_p x1.
Assume H2: ChurchNum_8ary_proj_p x2.
Assume H3: ChurchNum_8ary_proj_p x3.
Claim L4: ChurchNum_3ary_proj_p (ChurchNums_8x3_to_3_lt4_id_ge4_rot2 x2 x0)
Apply unknownprop_2eb24842eca1af01a473a7d70b456a32088af46ce59a955c3e1171fe5453acfe with x2, x0 leaving 2 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H0.
Claim L5: ChurchNum_3ary_proj_p (ChurchNums_8x3_to_3_lt4_id_ge4_rot2 x3 x1)
Apply unknownprop_2eb24842eca1af01a473a7d70b456a32088af46ce59a955c3e1171fe5453acfe with x3, x1 leaving 2 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying H1.
Claim L6: ChurchNum_8ary_proj_p (ChurchNums_8_perm_4_5_6_7_0_1_2_3 x2)
Apply unknownprop_0eb3496ff031982dfcd5abc5bf174762796e7c83210d20f8bb4ebc7eda4e83af with x2.
The subproof is completed by applying H2.
Claim L7: ChurchNum_8ary_proj_p (ChurchNums_8_perm_4_5_6_7_0_1_2_3 x3)
Apply unknownprop_0eb3496ff031982dfcd5abc5bf174762796e7c83210d20f8bb4ebc7eda4e83af with x3.
The subproof is completed by applying H3.
set y4 to be TwoRamseyGraph_4_5_24_ChurchNums_3x8 x0 x2 x1 x3
set y5 to be TwoRamseyGraph_4_5_24_ChurchNums_3x8 (ChurchNums_8x3_lt1_id_ge1_rot2 x3 x1) (ChurchNums_8_perm_7_0_1_2_3_4_5_6 x3) (ChurchNums_8x3_lt1_id_ge1_rot2 y4 x2) (ChurchNums_8_perm_7_0_1_2_3_4_5_6 y4)
Claim L8: ∀ x6 : (ι → ι → ι) → ο . x6 y5 ⟶ x6 y4
Let x6 of type (ι → ι → ι) → ο be given.
Assume H8: x6 (TwoRamseyGraph_4_5_24_ChurchNums_3x8 (ChurchNums_8x3_lt1_id_ge1_rot2 y4 x2) (ChurchNums_8_perm_7_0_1_2_3_4_5_6 y4) (ChurchNums_8x3_lt1_id_ge1_rot2 y5 x3) (ChurchNums_8_perm_7_0_1_2_3_4_5_6 y5)).
Apply unknownprop_ad30852621f640163d998df0793731af08ba3ec532e4cad640aa88356d3b9d87 with x2, x3, y4, y5, λ x7 : ι → ι → ι . x6 leaving 5 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
Apply unknownprop_5e1d335079696633b22b22a6f344040d3cb18267c0da5410cf760e08d1dbb4e3 with ChurchNums_8x3_to_3_lt4_id_ge4_rot2 y4 x2, ChurchNums_8x3_to_3_lt4_id_ge4_rot2 y5 x3, ChurchNums_8_perm_4_5_6_7_0_1_2_3 y4, ChurchNums_8_perm_4_5_6_7_0_1_2_3 y5, λ x7 : ι → ι → ι . x6 leaving 5 subgoals.
The subproof is completed by applying L4.
The subproof is completed by applying L5.
The subproof is completed by applying L6.
The subproof is completed by applying L7.
Apply unknownprop_10e17461d7ca1765349d3e02d585a69f8a74bcfc1e8db5d6cda017bb31003670 with x2, y4, λ x7 x8 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . TwoRamseyGraph_4_5_24_ChurchNums_3x8 x8 (ChurchNums_8_perm_3_4_5_6_7_0_1_2 (ChurchNums_8_perm_4_5_6_7_0_1_2_3 y4)) (ChurchNums_8x3_to_3_lt5_id_ge5_rot2 (ChurchNums_8_perm_4_5_6_7_0_1_2_3 y5) (ChurchNums_8x3_to_3_lt4_id_ge4_rot2 y5 x3)) (ChurchNums_8_perm_3_4_5_6_7_0_1_2 (ChurchNums_8_perm_4_5_6_7_0_1_2_3 y5)) = TwoRamseyGraph_4_5_24_ChurchNums_3x8 (ChurchNums_8x3_lt1_id_ge1_rot2 y4 x2) (ChurchNums_8_perm_7_0_1_2_3_4_5_6 y4) (ChurchNums_8x3_lt1_id_ge1_rot2 y5 x3) (ChurchNums_8_perm_7_0_1_2_3_4_5_6 y5), λ x7 : ι → ι → ι . x6 leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H2.
Apply unknownprop_10e17461d7ca1765349d3e02d585a69f8a74bcfc1e8db5d6cda017bb31003670 with x3, y5, λ x7 x8 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . TwoRamseyGraph_4_5_24_ChurchNums_3x8 (ChurchNums_8x3_lt1_id_ge1_rot2 y4 x2) (ChurchNums_8_perm_3_4_5_6_7_0_1_2 (ChurchNums_8_perm_4_5_6_7_0_1_2_3 y4)) x8 (ChurchNums_8_perm_3_4_5_6_7_0_1_2 (ChurchNums_8_perm_4_5_6_7_0_1_2_3 y5)) = TwoRamseyGraph_4_5_24_ChurchNums_3x8 (ChurchNums_8x3_lt1_id_ge1_rot2 y4 x2) (ChurchNums_8_perm_7_0_1_2_3_4_5_6 y4) (ChurchNums_8x3_lt1_id_ge1_rot2 y5 x3) (ChurchNums_8_perm_7_0_1_2_3_4_5_6 y5) leaving 3 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H3.
Let x7 of type (ι → ι → ι) → (ι → ι → ι) → ο be given.
Assume H9: x7 (TwoRamseyGraph_4_5_24_ChurchNums_3x8 (ChurchNums_8x3_lt1_id_ge1_rot2 y4 x2) (ChurchNums_8_perm_3_4_5_6_7_0_1_2 (ChurchNums_8_perm_4_5_6_7_0_1_2_3 y4)) (ChurchNums_8x3_lt1_id_ge1_rot2 y5 x3) (ChurchNums_8_perm_3_4_5_6_7_0_1_2 (ChurchNums_8_perm_4_5_6_7_0_1_2_3 y5))) (TwoRamseyGraph_4_5_24_ChurchNums_3x8 (ChurchNums_8x3_lt1_id_ge1_rot2 y4 x2) (ChurchNums_8_perm_7_0_1_2_3_4_5_6 y4) (ChurchNums_8x3_lt1_id_ge1_rot2 y5 x3) (ChurchNums_8_perm_7_0_1_2_3_4_5_6 y5)).
The subproof is completed by applying H9.
The subproof is completed by applying H8.
Let x6 of type (ι → ι → ι) → (ι → ι → ι) → ο be given.
Apply L8 with λ x7 : ι → ι → ι . x6 x7 y5 ⟶ x6 y5 x7.
Assume H9: x6 y5 y5.
The subproof is completed by applying H9.
■