Claim L0: ...

...

Let x0 of type ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι) be given.

Let x1 of type ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι) be given.

Let x2 of type ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι) be given.

Assume H1: ChurchNum_8ary_proj_p x1.

Assume H2: ChurchNum_3ary_proj_p x0.

Assume H3: ChurchNum_8ary_proj_p x2.

Apply L0 with ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt4_id_ge4_rot2 x1 (λ x3 x4 x5 : (ι → ι) → ι → ι . x3)) (ChurchNums_8_perm_4_5_6_7_0_1_2_3 x1) = ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt7_id_ge7_rot2 x2 x0) (ChurchNums_8_perm_1_2_3_4_5_6_7_0 x2) ⟶ and (x0 = ChurchNums_8x3_to_3_lt5_id_ge5_rot2 x1 (λ x3 x4 x5 : (ι → ι) → ι → ι . x3)) (x2 = ChurchNums_8_perm_3_4_5_6_7_0_1_2 x1).

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

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

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

Assume H6: ∀ x4 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x5 x6 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . x4 = ChurchNums_8x3_to_3_lt5_id_ge5_rot2 x5 (λ x7 x8 x9 : (ι → ι) → ι → ι . x7) ⟶ x6 = ChurchNums_8_perm_3_4_5_6_7_0_1_2 x5 ⟶ x3 x4 x5 x6.

Apply H4 with x0, x1, x2.

Apply H1 with λ x4 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . x3 x0 x4 x2 leaving 8 subgoals.

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

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

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

The subproof is completed by applying neq_4_1.

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

Assume H7: ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt4_id_ge4_rot2 (λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x4) (λ x4 x5 x6 : (ι → ι) → ι → ι . x4)) (ChurchNums_8_perm_4_5_6_7_0_1_2_3 (λ 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)).

Apply neq_4_2.

The subproof is completed by applying H7.

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

Assume H7: ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt4_id_ge4_rot2 (λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x4) (λ x4 x5 x6 : (ι → ι) → ι → ι . x4)) (ChurchNums_8_perm_4_5_6_7_0_1_2_3 (λ 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)).

Apply neq_4_3.

The subproof is completed by applying H7.

Apply H6 with λ x4 x5 x6 : (ι → ι) → ι → ι . x4, λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x4, λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x7 leaving 2 subgoals.

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

Assume H7: x4 (λ x5 x6 x7 : (ι → ι) → ι → ι . x5) (ChurchNums_8x3_to_3_lt5_id_ge5_rot2 (λ x5 x6 x7 x8 x9 x10 x11 x12 : (ι → ι) → ι → ι . x5) (λ x5 x6 x7 : (ι → ι) → ι → ι . x5)).

The subproof is completed by applying H7.

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

Assume H7: x4 (λ x5 x6 x7 x8 x9 x10 x11 x12 : (ι → ι) → ι → ι . x8) (ChurchNums_8_perm_3_4_5_6_7_0_1_2 (λ x5 x6 x7 x8 x9 x10 x11 x12 : (ι → ι) → ι → ι . x5)).

The subproof is completed by applying H7.

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

Assume H7: ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt4_id_ge4_rot2 (λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x4) (λ x4 x5 x6 : (ι → ι) → ι → ι . x4)) (ChurchNums_8_perm_4_5_6_7_0_1_2_3 (λ 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 : (ι → ι) → ι → ι . x8) (λ x4 x5 x6 : (ι → ι) → ι → ι . x4)) (ChurchNums_8_perm_1_2_3_4_5_6_7_0 (λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x8)).

Apply neq_5_4.

Let x4 of type ι → ι → ο be given.

The subproof is completed by applying H7 with λ x5 x6 . x4 x6 x5.

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

...

■

Proofgold Proof