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.
Claim L20: ...
...
Claim L21: ...
...
Claim L22: ...
...
Claim L23: ...
...
Claim L24: ...
...
Claim L25: ...
...
Claim L26: ...
...
Claim L27: ...
...
Claim L28: ∀ x10 x11 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x12 x13 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ... ⟶ ... ⟶ ... ⟶ ... ⟶ ... ⟶ ∀ x14 . ... ⟶ ∀ x15 . ... ⟶ ap ((λ x16 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . λ x17 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . lam 5 (λ x18 . If_i (x18 = 0) (ChurchNums_3x8_to_u24 x16 x17) (If_i (x18 = 1) (ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt7_id_ge7_rot2 x17 x16) (ChurchNums_8_perm_1_2_3_4_5_6_7_0 x17)) (If_i (x18 = 2) (ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt6_id_ge6_rot2 x17 x16) (ChurchNums_8_perm_2_3_4_5_6_7_0_1 x17)) (If_i (x18 = 3) (ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt5_id_ge5_rot2 x17 x16) (ChurchNums_8_perm_3_4_5_6_7_0_1_2 x17)) (ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt4_id_ge4_rot2 x17 x16) (ChurchNums_8_perm_4_5_6_7_0_1_2_3 x17))))))) x10 x12) x14 = ap ((λ x16 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . λ x17 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . lam 5 ...) ... ...) ... ⟶ ∀ x16 : ο . (x11 = ChurchNums_8x3_to_3_lt5_id_ge5_rot2 x12 x10 ⟶ x13 = ChurchNums_8_perm_3_4_5_6_7_0_1_2 x12 ⟶ x16) ⟶ (x10 = ChurchNums_8x3_to_3_lt5_id_ge5_rot2 x13 x11 ⟶ x12 = ChurchNums_8_perm_3_4_5_6_7_0_1_2 x13 ⟶ x16) ⟶ x16
...
Apply unknownprop_39301bd614c212adbaebf467cd0b807c24c84feb4d0124878a6e71219c59eaba with x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, λ x10 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . λ x11 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . lam 5 (λ x12 . If_i (x12 = 0) (ChurchNums_3x8_to_u24 x10 x11) (If_i (x12 = 1) (ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt7_id_ge7_rot2 x11 x10) (ChurchNums_8_perm_1_2_3_4_5_6_7_0 x11)) (If_i (x12 = 2) (ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt6_id_ge6_rot2 x11 x10) (ChurchNums_8_perm_2_3_4_5_6_7_0_1 x11)) (If_i (x12 = 3) (ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt5_id_ge5_rot2 x11 x10) (ChurchNums_8_perm_3_4_5_6_7_0_1_2 x11)) (ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt4_id_ge4_rot2 x11 x10) (ChurchNums_8_perm_4_5_6_7_0_1_2_3 x11)))))) leaving 27 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.
The subproof is completed by applying H4.
The subproof is completed by applying H5.
The subproof is completed by applying H6.
The subproof is completed by applying H7.
The subproof is completed by applying H8.
The subproof is completed by applying H9.
The subproof is completed by applying H10.
The subproof is completed by applying H11.
The subproof is completed by applying H12.
The subproof is completed by applying H13.
The subproof is completed by applying H14.
The subproof is completed by applying H15.
The subproof is completed by applying H16.
The subproof is completed by applying H17.
The subproof is completed by applying H18.
The subproof is completed by applying H19.
The subproof is completed by applying L20.
The subproof is completed by applying L21.
The subproof is completed by applying L22.
The subproof is completed by applying L23.
The subproof is completed by applying L24.
The subproof is completed by applying L26.
The subproof is completed by applying L28.
■