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_to_3_lt3_id_ge3_rot2 x3 x1) (ChurchNums_8_perm_5_6_7_0_1_2_3_4 x3) (ChurchNums_8x3_to_3_lt3_id_ge3_rot2 y4 x2) (ChurchNums_8_perm_5_6_7_0_1_2_3_4 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_to_3_lt3_id_ge3_rot2 y4 x2) (ChurchNums_8_perm_5_6_7_0_1_2_3_4 y4) (ChurchNums_8x3_to_3_lt3_id_ge3_rot2 y5 x3) (ChurchNums_8_perm_5_6_7_0_1_2_3_4 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_266b045b7feec883828879c5a024148e89e16bb857c96ef92a5dc784837a0218 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_f9a5b512b4c0716d5551eefd2fbe0f6752347561eae79cb6493c7f4b21c5b31c with x2, y4, λ x7 x8 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . TwoRamseyGraph_4_5_24_ChurchNums_3x8 x8 (ChurchNums_8_perm_1_2_3_4_5_6_7_0 (ChurchNums_8_perm_4_5_6_7_0_1_2_3 y4)) (ChurchNums_8x3_to_3_lt7_id_ge7_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_1_2_3_4_5_6_7_0 (ChurchNums_8_perm_4_5_6_7_0_1_2_3 y5)) = TwoRamseyGraph_4_5_24_ChurchNums_3x8 (ChurchNums_8x3_to_3_lt3_id_ge3_rot2 y4 x2) (ChurchNums_8_perm_5_6_7_0_1_2_3_4 y4) (ChurchNums_8x3_to_3_lt3_id_ge3_rot2 y5 x3) (ChurchNums_8_perm_5_6_7_0_1_2_3_4 y5), λ x7 : ι → ι → ι . x6 leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H2.
Apply unknownprop_f9a5b512b4c0716d5551eefd2fbe0f6752347561eae79cb6493c7f4b21c5b31c with x3, y5, λ x7 x8 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . TwoRamseyGraph_4_5_24_ChurchNums_3x8 (ChurchNums_8x3_to_3_lt3_id_ge3_rot2 y4 x2) (ChurchNums_8_perm_1_2_3_4_5_6_7_0 (ChurchNums_8_perm_4_5_6_7_0_1_2_3 y4)) x8 (ChurchNums_8_perm_1_2_3_4_5_6_7_0 (ChurchNums_8_perm_4_5_6_7_0_1_2_3 y5)) = TwoRamseyGraph_4_5_24_ChurchNums_3x8 (ChurchNums_8x3_to_3_lt3_id_ge3_rot2 y4 x2) (ChurchNums_8_perm_5_6_7_0_1_2_3_4 y4) (ChurchNums_8x3_to_3_lt3_id_ge3_rot2 y5 x3) (ChurchNums_8_perm_5_6_7_0_1_2_3_4 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_to_3_lt3_id_ge3_rot2 y4 x2) (ChurchNums_8_perm_1_2_3_4_5_6_7_0 (ChurchNums_8_perm_4_5_6_7_0_1_2_3 y4)) (ChurchNums_8x3_to_3_lt3_id_ge3_rot2 y5 x3) (ChurchNums_8_perm_1_2_3_4_5_6_7_0 (ChurchNums_8_perm_4_5_6_7_0_1_2_3 y5))) (TwoRamseyGraph_4_5_24_ChurchNums_3x8 (ChurchNums_8x3_to_3_lt3_id_ge3_rot2 y4 x2) (ChurchNums_8_perm_5_6_7_0_1_2_3_4 y4) (ChurchNums_8x3_to_3_lt3_id_ge3_rot2 y5 x3) (ChurchNums_8_perm_5_6_7_0_1_2_3_4 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.
■