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 L0 with ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt4_id_ge4_rot2 x2 x0) (ChurchNums_8_perm_4_5_6_7_0_1_2_3 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) ⟶ and (x1 = ChurchNums_8x3_to_3_lt5_id_ge5_rot2 x2 x0) (x3 = ChurchNums_8_perm_3_4_5_6_7_0_1_2 x2).

Let x4 of type (((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι)) → (((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι)) → (((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι)) → (((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι)) → ο be given.

Assume H5: ∀ x5 x6 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x7 x8 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . x4 x5 x6 x7 x8 ⟶ ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt4_id_ge4_rot2 x7 x5) (ChurchNums_8_perm_4_5_6_7_0_1_2_3 x7) = ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt7_id_ge7_rot2 x8 x6) (ChurchNums_8_perm_1_2_3_4_5_6_7_0 x8) ⟶ and (x6 = ChurchNums_8x3_to_3_lt5_id_ge5_rot2 x7 x5) (x8 = ChurchNums_8_perm_3_4_5_6_7_0_1_2 x7).

Assume H6: ∀ x5 x6 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x7 x8 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . (ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt4_id_ge4_rot2 x7 x5) (ChurchNums_8_perm_4_5_6_7_0_1_2_3 x7) = ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt7_id_ge7_rot2 x8 x6) (ChurchNums_8_perm_1_2_3_4_5_6_7_0 x8) ⟶ ∀ x9 : ο . x9) ⟶ x4 x5 x6 x7 x8.

Assume H7: ∀ x5 x6 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x7 x8 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . x6 = ChurchNums_8x3_to_3_lt5_id_ge5_rot2 x7 x5 ⟶ x8 = ChurchNums_8_perm_3_4_5_6_7_0_1_2 x7 ⟶ x4 x5 x6 x7 x8.

Apply H1 with λ x5 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt4_id_ge4_rot2 x2 x5) (ChurchNums_8_perm_4_5_6_7_0_1_2_3 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) ⟶ and (x1 = ChurchNums_8x3_to_3_lt5_id_ge5_rot2 x2 x5) (x3 = ChurchNums_8_perm_3_4_5_6_7_0_1_2 x2) leaving 3 subgoals.

Apply unknownprop_7bea65489b9a4965499d3b965b74bf879a52239254ee12ba9cc342399ede9ad2 with x1, x2, x3 leaving 3 subgoals.

The subproof is completed by applying H2.

The subproof is completed by applying H3.

The subproof is completed by applying H4.

Apply H5 with λ x5 x6 x7 : (ι → ι) → ι → ι . x6, x1, x2, x3.

Apply H2 with λ x5 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . x4 (λ x6 x7 x8 : (ι → ι) → ι → ι . x7) x1 x5 x3 leaving 8 subgoals.

Apply H3 with λ x5 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . x4 (λ x6 x7 x8 : (ι → ι) → ι → ι . x7) x5 (λ x6 x7 x8 x9 x10 x11 x12 x13 : (ι → ι) → ι → ι . x6) x3 leaving 3 subgoals.

Apply H4 with λ x5 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . x4 (λ x6 x7 x8 : (ι → ι) → ι → ι . x7) (λ x6 x7 x8 : (ι → ι) → ι → ι . x6) (λ x6 x7 x8 x9 x10 x11 x12 x13 : (ι → ι) → ι → ι . x6) x5 leaving 8 subgoals.

Apply H6 with λ x5 x6 x7 : (ι → ι) → ι → ι . x6, λ x5 x6 x7 : (ι → ι) → ι → ι . x5, λ x5 x6 x7 x8 x9 x10 x11 x12 : (ι → ι) → ι → ι . x5, λ x5 x6 x7 x8 x9 x10 x11 x12 : (ι → ι) → ι → ι . x5.

Assume H8: ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt4_id_ge4_rot2 (λ x5 x6 x7 x8 x9 x10 x11 x12 : (ι → ι) → ι → ι . x5) (λ x5 x6 x7 : (ι → ι) → ι → ι . x6)) (ChurchNums_8_perm_4_5_6_7_0_1_2_3 (λ x5 x6 x7 x8 x9 x10 x11 x12 : (ι → ι) → ι → ι . x5)) = ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt7_id_ge7_rot2 (λ x5 x6 x7 x8 x9 x10 x11 x12 : (ι → ι) → ι → ι . x5) (λ x5 x6 x7 : (ι → ι) → ι → ι . x5)) (ChurchNums_8_perm_1_2_3_4_5_6_7_0 (λ x5 x6 x7 x8 x9 x10 x11 x12 : (ι → ι) → ι → ι . x5)).

Apply unknownprop_fac08972bb876bc2457930272ed91a55b92fbe2a965f8dbfa94c531b056fd466.

The subproof is completed by applying H8.

Apply H6 with λ x5 x6 x7 : (ι → ι) → ι → ι . x6, λ x5 x6 x7 : (ι → ι) → ι → ι . x5, λ x5 x6 x7 x8 x9 x10 x11 x12 : (ι → ι) → ι → ι . x5, λ x5 x6 x7 x8 x9 x10 x11 x12 : (ι → ι) → ι → ι . x6.

Assume H8: ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt4_id_ge4_rot2 (λ x5 x6 x7 x8 x9 x10 x11 x12 : (ι → ι) → ι → ι . x5) (λ x5 x6 x7 : (ι → ι) → ι → ι . x6)) (ChurchNums_8_perm_4_5_6_7_0_1_2_3 (λ x5 x6 x7 x8 x9 x10 x11 x12 : (ι → ι) → ι → ι . x5)) = ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt7_id_ge7_rot2 (λ x5 x6 x7 x8 x9 x10 x11 x12 : (ι → ι) → ι → ι . x6) (λ x5 x6 x7 : (ι → ι) → ι → ι . x5)) (ChurchNums_8_perm_1_2_3_4_5_6_7_0 (λ x5 x6 x7 x8 x9 x10 x11 x12 : (ι → ι) → ι → ι . x6)).

Apply unknownprop_9925a94179f9b96e15bb2f5f3151446cc17d0f38ddaec97b207a42442fb0efed.

The subproof is completed by applying H8.

Apply H6 with λ x5 x6 x7 : (ι → ι) → ι → ι . x6, λ x5 x6 x7 : (ι → ι) → ι → ι . x5, λ x5 x6 x7 x8 x9 x10 x11 x12 : (ι → ι) → ι → ι . x5, λ x5 x6 x7 x8 x9 x10 x11 x12 : (ι → ι) → ι → ι . x7.

Assume H8: ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt4_id_ge4_rot2 (λ x5 x6 x7 x8 x9 x10 x11 x12 : (ι → ι) → ι → ι . x5) (λ x5 x6 x7 : (ι → ι) → ι → ι . x6)) (ChurchNums_8_perm_4_5_6_7_0_1_2_3 (λ x5 x6 x7 x8 x9 x10 x11 x12 : (ι → ι) → ι → ι . x5)) = ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt7_id_ge7_rot2 (λ x5 x6 x7 x8 x9 x10 x11 x12 : (ι → ι) → ι → ι . x7) (λ x5 x6 x7 : (ι → ι) → ι → ι . x5)) (ChurchNums_8_perm_1_2_3_4_5_6_7_0 (λ x5 x6 x7 x8 x9 x10 x11 x12 : (ι → ι) → ι → ι . x7)).

Apply unknownprop_21d350f752803e70816c84c0f32485027c6c1878657f7263a7ebfa87995c9b6a.

The subproof is completed by applying H8.

Apply H6 with λ x5 x6 x7 : (ι → ι) → ι → ι . x6, λ x5 x6 x7 : (ι → ι) → ι → ι . x5, λ x5 x6 x7 x8 x9 x10 x11 x12 : (ι → ι) → ι → ι . x5, λ x5 x6 x7 x8 x9 x10 x11 x12 : (ι → ι) → ι → ι . x8.

...

■

Proofgold Proof