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.
Assume H1: ChurchNum_3ary_proj_p x0.
Assume H2: ChurchNum_8ary_proj_p x2.
Assume H3: ChurchNum_3ary_proj_p x1.
Assume H4: ChurchNum_8ary_proj_p x3.
Apply H1 with λ x4 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . (TwoRamseyGraph_4_5_24_ChurchNums_3x8 x4 x2 x1 x3 = λ x5 x6 . x6) ⟶ ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt6_id_ge6_rot2 x2 x4) (ChurchNums_8_perm_2_3_4_5_6_7_0_1 x2) = ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt7_id_ge7_rot2 x3 x1) (ChurchNums_8_perm_1_2_3_4_5_6_7_0 x3) ⟶ False leaving 3 subgoals.
Apply H3 with λ x4 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . (TwoRamseyGraph_4_5_24_ChurchNums_3x8 (λ x5 x6 x7 : (ι → ι) → ι → ι . x5) x2 x4 x3 = λ x5 x6 . x6) ⟶ ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt6_id_ge6_rot2 x2 (λ x5 x6 x7 : (ι → ι) → ι → ι . x5)) (ChurchNums_8_perm_2_3_4_5_6_7_0_1 x2) = ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt7_id_ge7_rot2 x3 x4) (ChurchNums_8_perm_1_2_3_4_5_6_7_0 x3) ⟶ False leaving 3 subgoals.
Apply H2 with λ x4 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . (TwoRamseyGraph_4_5_24_ChurchNums_3x8 (λ x5 x6 x7 : (ι → ι) → ι → ι . x5) x4 (λ x5 x6 x7 : (ι → ι) → ι → ι . x5) x3 = λ x5 x6 . x6) ⟶ ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt6_id_ge6_rot2 x4 (λ x5 x6 x7 : (ι → ι) → ι → ι . x5)) (ChurchNums_8_perm_2_3_4_5_6_7_0_1 x4) = ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt7_id_ge7_rot2 x3 (λ x5 x6 x7 : (ι → ι) → ι → ι . x5)) (ChurchNums_8_perm_1_2_3_4_5_6_7_0 x3) ⟶ False leaving 8 subgoals.
Apply H4 with λ x4 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . (TwoRamseyGraph_4_5_24_ChurchNums_3x8 (λ x5 x6 x7 : (ι → ι) → ι → ι . x5) (λ x5 x6 x7 x8 x9 x10 x11 x12 : (ι → ι) → ι → ι . x5) (λ x5 x6 x7 : (ι → ι) → ι → ι . x5) x4 = λ x5 x6 . x6) ⟶ ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt6_id_ge6_rot2 (λ x5 x6 x7 x8 x9 x10 x11 x12 : (ι → ι) → ι → ι . x5) (λ x5 x6 x7 : (ι → ι) → ι → ι . x5)) (ChurchNums_8_perm_2_3_4_5_6_7_0_1 (λ x5 x6 x7 x8 x9 x10 x11 x12 : (ι → ι) → ι → ι . x5)) = ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt7_id_ge7_rot2 x4 (λ x5 x6 x7 : (ι → ι) → ι → ι . x5)) (ChurchNums_8_perm_1_2_3_4_5_6_7_0 x4) ⟶ False leaving 8 subgoals.
Assume H5: TwoRamseyGraph_4_5_24_ChurchNums_3x8 (λ x4 x5 x6 : (ι → ι) → ι → ι . x4) (λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x4) (λ x4 x5 x6 : (ι → ι) → ι → ι . x4) (λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x4) = λ x4 x5 . x5.
Apply FalseE with ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt6_id_ge6_rot2 (λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x4) (λ x4 x5 x6 : (ι → ι) → ι → ι . x4)) (ChurchNums_8_perm_2_3_4_5_6_7_0_1 (λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x4)) = ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt7_id_ge7_rot2 (λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x4) (λ x4 x5 x6 : (ι → ι) → ι → ι . x4)) (ChurchNums_8_perm_1_2_3_4_5_6_7_0 (λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x4)) ⟶ False.
Apply L0.
The subproof is completed by applying H5.
Assume H5: TwoRamseyGraph_4_5_24_ChurchNums_3x8 (λ x4 x5 x6 : (ι → ι) → ι → ι . x4) (λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x4) (λ x4 x5 x6 : (ι → ι) → ι → ι . x4) (λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x5) = λ x4 x5 . x5.
Apply FalseE with ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt6_id_ge6_rot2 (λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x4) (λ x4 x5 x6 : (ι → ι) → ι → ι . x4)) (ChurchNums_8_perm_2_3_4_5_6_7_0_1 (λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x4)) = ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt7_id_ge7_rot2 (λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x5) (λ x4 x5 x6 : (ι → ι) → ι → ι . x4)) (ChurchNums_8_perm_1_2_3_4_5_6_7_0 (λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x5)) ⟶ False.
Apply L0.
The subproof is completed by applying H5.
Assume H5: TwoRamseyGraph_4_5_24_ChurchNums_3x8 (λ x4 x5 x6 : (ι → ι) → ι → ι . x4) (λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x4) (λ x4 x5 x6 : (ι → ι) → ι → ι . x4) (λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x6) = λ x4 x5 . x5.
Apply FalseE with ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt6_id_ge6_rot2 (λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x4) (λ x4 x5 x6 : (ι → ι) → ι → ι . x4)) (ChurchNums_8_perm_2_3_4_5_6_7_0_1 (λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x4)) = ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt7_id_ge7_rot2 (λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x6) (λ x4 x5 x6 : (ι → ι) → ι → ι . x4)) (ChurchNums_8_perm_1_2_3_4_5_6_7_0 (λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x6)) ⟶ False.
Apply L0.
The subproof is completed by applying H5.
Assume H5: TwoRamseyGraph_4_5_24_ChurchNums_3x8 (λ x4 x5 x6 : (ι → ι) → ι → ι . x4) (λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x4) (λ x4 x5 x6 : (ι → ι) → ι → ι . x4) (λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x7) = λ x4 x5 . x5.
Assume H6: ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt6_id_ge6_rot2 (λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x4) (λ x4 x5 x6 : (ι → ι) → ι → ι . x4)) (ChurchNums_8_perm_2_3_4_5_6_7_0_1 (λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x4)) = ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt7_id_ge7_rot2 (λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x7) (λ x4 x5 x6 : (ι → ι) → ι → ι . x4)) (ChurchNums_8_perm_1_2_3_4_5_6_7_0 (λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x7)).
Apply neq_4_2.
Let x4 of type ι → ι → ο be given.
The subproof is completed by applying H6 with λ x5 x6 . x4 x6 x5.
Assume H5: ....
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
■