Proofgold Proof

pf

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

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

Assume H0: ChurchNum_3ary_proj_p x0.

Assume H1: ChurchNum_8ary_proj_p x1.

Apply H0 with λ x2 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNums_8x3_to_3_lt6_id_ge6_rot2 (ChurchNums_8_perm_4_5_6_7_0_1_2_3 x1) (ChurchNums_8x3_to_3_lt4_id_ge4_rot2 x1 x2) = ChurchNums_8x3_lt2_id_ge2_rot2 x1 x2 leaving 3 subgoals.

Apply H1 with λ x2 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNums_8x3_to_3_lt6_id_ge6_rot2 (ChurchNums_8_perm_4_5_6_7_0_1_2_3 x2) (ChurchNums_8x3_to_3_lt4_id_ge4_rot2 x2 (λ x3 x4 x5 : (ι → ι) → ι → ι . x3)) = ChurchNums_8x3_lt2_id_ge2_rot2 x2 (λ x3 x4 x5 : (ι → ι) → ι → ι . x3) leaving 8 subgoals.

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

Assume H2: x2 (ChurchNums_8x3_to_3_lt6_id_ge6_rot2 (ChurchNums_8_perm_4_5_6_7_0_1_2_3 (λ x3 x4 x5 x6 x7 x8 x9 x10 : (ι → ι) → ι → ι . x3)) (ChurchNums_8x3_to_3_lt4_id_ge4_rot2 (λ x3 x4 x5 x6 x7 x8 x9 x10 : (ι → ι) → ι → ι . x3) (λ x3 x4 x5 : (ι → ι) → ι → ι . x3))) (ChurchNums_8x3_lt2_id_ge2_rot2 (λ x3 x4 x5 x6 x7 x8 x9 x10 : (ι → ι) → ι → ι . x3) (λ x3 x4 x5 : (ι → ι) → ι → ι . x3)).

The subproof is completed by applying H2.

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

Assume H2: x2 (ChurchNums_8x3_to_3_lt6_id_ge6_rot2 (ChurchNums_8_perm_4_5_6_7_0_1_2_3 (λ x3 x4 x5 x6 x7 x8 x9 x10 : (ι → ι) → ι → ι . x4)) (ChurchNums_8x3_to_3_lt4_id_ge4_rot2 (λ x3 x4 x5 x6 x7 x8 x9 x10 : (ι → ι) → ι → ι . x4) (λ x3 x4 x5 : (ι → ι) → ι → ι . x3))) (ChurchNums_8x3_lt2_id_ge2_rot2 (λ x3 x4 x5 x6 x7 x8 x9 x10 : (ι → ι) → ι → ι . x4) (λ x3 x4 x5 : (ι → ι) → ι → ι . x3)).

The subproof is completed by applying H2.

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

Assume H2: x2 (ChurchNums_8x3_to_3_lt6_id_ge6_rot2 (ChurchNums_8_perm_4_5_6_7_0_1_2_3 (λ x3 x4 x5 x6 x7 x8 x9 x10 : (ι → ι) → ι → ι . x5)) (ChurchNums_8x3_to_3_lt4_id_ge4_rot2 (λ x3 x4 x5 x6 x7 x8 x9 x10 : (ι → ι) → ι → ι . x5) (λ x3 x4 x5 : (ι → ι) → ι → ι . x3))) (ChurchNums_8x3_lt2_id_ge2_rot2 (λ x3 x4 x5 x6 x7 x8 x9 x10 : (ι → ι) → ι → ι . x5) (λ x3 x4 x5 : (ι → ι) → ι → ι . x3)).

The subproof is completed by applying H2.

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

Assume H2: x2 (ChurchNums_8x3_to_3_lt6_id_ge6_rot2 (ChurchNums_8_perm_4_5_6_7_0_1_2_3 (λ x3 x4 x5 x6 x7 x8 x9 x10 : (ι → ι) → ι → ι . x6)) (ChurchNums_8x3_to_3_lt4_id_ge4_rot2 (λ x3 x4 x5 x6 x7 x8 x9 x10 : (ι → ι) → ι → ι . x6) (λ x3 x4 x5 : (ι → ι) → ι → ι . x3))) (ChurchNums_8x3_lt2_id_ge2_rot2 (λ x3 x4 x5 x6 x7 x8 x9 x10 : (ι → ι) → ι → ι . x6) (λ x3 x4 x5 : (ι → ι) → ι → ι . x3)).

The subproof is completed by applying H2.

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

Assume H2: x2 (ChurchNums_8x3_to_3_lt6_id_ge6_rot2 (ChurchNums_8_perm_4_5_6_7_0_1_2_3 (λ x3 x4 x5 x6 x7 x8 x9 x10 : (ι → ι) → ι → ι . x7)) (ChurchNums_8x3_to_3_lt4_id_ge4_rot2 (λ x3 x4 x5 x6 x7 x8 x9 x10 : (ι → ι) → ι → ι . x7) (λ x3 x4 x5 : (ι → ι) → ι → ι . x3))) (ChurchNums_8x3_lt2_id_ge2_rot2 (λ x3 x4 x5 x6 x7 x8 x9 x10 : (ι → ι) → ι → ι . x7) (λ x3 x4 x5 : (ι → ι) → ι → ι . x3)).

The subproof is completed by applying H2.

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

Assume H2: x2 (ChurchNums_8x3_to_3_lt6_id_ge6_rot2 (ChurchNums_8_perm_4_5_6_7_0_1_2_3 (λ x3 x4 x5 x6 x7 x8 x9 x10 : (ι → ι) → ι → ι . x8)) (ChurchNums_8x3_to_3_lt4_id_ge4_rot2 (λ x3 x4 x5 x6 x7 x8 x9 x10 : (ι → ι) → ι → ι . x8) (λ x3 x4 x5 : (ι → ι) → ι → ι . x3))) (ChurchNums_8x3_lt2_id_ge2_rot2 (λ x3 x4 x5 x6 x7 x8 x9 x10 : (ι → ι) → ι → ι . x8) (λ x3 x4 x5 : (ι → ι) → ι → ι . x3)).

The subproof is completed by applying H2.

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

Assume H2: x2 (ChurchNums_8x3_to_3_lt6_id_ge6_rot2 (ChurchNums_8_perm_4_5_6_7_0_1_2_3 (λ x3 x4 x5 x6 x7 x8 x9 x10 : (ι → ι) → ι → ι . x9)) (ChurchNums_8x3_to_3_lt4_id_ge4_rot2 (λ x3 x4 x5 x6 x7 x8 x9 x10 : (ι → ι) → ι → ι . x9) (λ x3 x4 x5 : (ι → ι) → ι → ι . x3))) (ChurchNums_8x3_lt2_id_ge2_rot2 (λ x3 x4 x5 x6 x7 x8 x9 x10 : (ι → ι) → ι → ι . x9) (λ x3 x4 x5 : (ι → ι) → ι → ι . x3)).

The subproof is completed by applying H2.

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

Assume H2: x2 (ChurchNums_8x3_to_3_lt6_id_ge6_rot2 (ChurchNums_8_perm_4_5_6_7_0_1_2_3 (λ x3 x4 x5 x6 x7 x8 x9 x10 : (ι → ι) → ι → ι . x10)) (ChurchNums_8x3_to_3_lt4_id_ge4_rot2 (λ x3 x4 x5 x6 x7 x8 x9 x10 : (ι → ι) → ι → ι . x10) (λ x3 x4 x5 : (ι → ι) → ι → ι . x3))) (ChurchNums_8x3_lt2_id_ge2_rot2 (λ x3 x4 x5 x6 x7 x8 x9 x10 : (ι → ι) → ι → ι . x10) (λ x3 x4 x5 : (ι → ι) → ι → ι . x3)).

The subproof is completed by applying H2.

Apply H1 with λ x2 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNums_8x3_to_3_lt6_id_ge6_rot2 (ChurchNums_8_perm_4_5_6_7_0_1_2_3 x2) (ChurchNums_8x3_to_3_lt4_id_ge4_rot2 x2 (λ x3 x4 x5 : (ι → ι) → ι → ι . x4)) = ChurchNums_8x3_lt2_id_ge2_rot2 x2 (λ x3 x4 x5 : (ι → ι) → ι → ι . x4) leaving 8 subgoals.

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

Assume H2: x2 (ChurchNums_8x3_to_3_lt6_id_ge6_rot2 (ChurchNums_8_perm_4_5_6_7_0_1_2_3 (λ x3 x4 x5 x6 x7 x8 x9 x10 : (ι → ι) → ι → ι . x3)) (ChurchNums_8x3_to_3_lt4_id_ge4_rot2 (λ x3 x4 x5 x6 x7 x8 x9 x10 : (ι → ι) → ι → ι . x3) (λ x3 x4 x5 : (ι → ι) → ι → ι . x4))) (ChurchNums_8x3_lt2_id_ge2_rot2 (λ x3 x4 x5 x6 x7 x8 x9 x10 : (ι → ι) → ι → ι . x3) (λ x3 x4 x5 : (ι → ι) → ι → ι . x4)).

The subproof is completed by applying H2.

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

Assume H2: x2 (ChurchNums_8x3_to_3_lt6_id_ge6_rot2 (ChurchNums_8_perm_4_5_6_7_0_1_2_3 (λ x3 x4 x5 x6 x7 x8 x9 x10 : (ι → ι) → ι → ι . x4)) (ChurchNums_8x3_to_3_lt4_id_ge4_rot2 (λ x3 x4 x5 x6 x7 x8 x9 x10 : (ι → ι) → ι → ι . x4) (λ x3 x4 x5 : (ι → ι) → ι → ι . x4))) (ChurchNums_8x3_lt2_id_ge2_rot2 (λ x3 x4 x5 x6 x7 x8 x9 x10 : (ι → ι) → ι → ι . x4) (λ x3 x4 x5 : (ι → ι) → ι → ι . x4)).

The subproof is completed by applying H2.

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

Assume H2: x2 (ChurchNums_8x3_to_3_lt6_id_ge6_rot2 (ChurchNums_8_perm_4_5_6_7_0_1_2_3 (λ x3 x4 x5 x6 x7 x8 x9 x10 : (ι → ι) → ι → ι . x5)) (ChurchNums_8x3_to_3_lt4_id_ge4_rot2 (λ x3 x4 x5 x6 x7 x8 x9 x10 : (ι → ι) → ι → ι . x5) (λ x3 x4 x5 : (ι → ι) → ι → ι . x4))) (ChurchNums_8x3_lt2_id_ge2_rot2 (λ x3 x4 x5 x6 x7 x8 x9 x10 : (ι → ι) → ι → ι . x5) (λ x3 x4 x5 : (ι → ι) → ι → ι . x4)).

The subproof is completed by applying H2.

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

Assume H2: x2 (ChurchNums_8x3_to_3_lt6_id_ge6_rot2 (ChurchNums_8_perm_4_5_6_7_0_1_2_3 (λ x3 x4 x5 x6 x7 x8 x9 x10 : (ι → ι) → ι → ι . x6)) (ChurchNums_8x3_to_3_lt4_id_ge4_rot2 (λ x3 x4 x5 x6 x7 x8 x9 x10 : (ι → ι) → ι → ι . x6) (λ x3 x4 x5 : (ι → ι) → ι → ι . x4))) (ChurchNums_8x3_lt2_id_ge2_rot2 (λ x3 x4 x5 x6 x7 x8 x9 x10 : (ι → ι) → ι → ι . x6) (λ x3 x4 x5 : (ι → ι) → ι → ι . x4)).

...

...

...

...

...

...

■