Let x0 of type ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι be given.

Assume H0: Church17_p x0.

Apply H0 with λ x1 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . or ((λ x2 x3 . x1 x2 x2 x2 x2 x2 x2 x2 x2 x2 x3 x3 x3 x3 x3 x3 x3 x3) = λ x2 x3 . x2) ((λ x2 x3 . x1 x3 x3 x3 x3 x3 x3 x3 x3 x3 x2 x2 x2 x2 x2 x2 x2 x2) = λ x2 x3 . x2) leaving 17 subgoals.

Apply orIL with (λ x1 x2 . (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x3) x1 x1 x1 x1 x1 x1 x1 x1 x1 x2 x2 x2 x2 x2 x2 x2 x2) = λ x1 x2 . x1, (λ x1 x2 . (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x3) x2 x2 x2 x2 x2 x2 x2 x2 x2 x1 x1 x1 x1 x1 x1 x1 x1) = λ x1 x2 . x1.

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

Assume H1: x1 (λ x2 x3 . (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x4) x2 x2 x2 x2 x2 x2 x2 x2 x2 x3 x3 x3 x3 x3 x3 x3 x3) (λ x2 x3 . x2).

The subproof is completed by applying H1.

Apply orIL with (λ x1 x2 . (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x4) x1 x1 x1 x1 x1 x1 x1 x1 x1 x2 x2 x2 x2 x2 x2 x2 x2) = λ x1 x2 . x1, (λ x1 x2 . (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x4) x2 x2 x2 x2 x2 x2 x2 x2 x2 x1 x1 x1 x1 x1 x1 x1 x1) = λ x1 x2 . x1.

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

Assume H1: x1 (λ x2 x3 . (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x5) x2 x2 x2 x2 x2 x2 x2 x2 x2 x3 x3 x3 x3 x3 x3 x3 x3) (λ x2 x3 . x2).

The subproof is completed by applying H1.

Apply orIL with (λ x1 x2 . (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x5) x1 x1 x1 x1 x1 x1 x1 x1 x1 x2 x2 x2 x2 x2 x2 x2 x2) = λ x1 x2 . x1, (λ x1 x2 . (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x5) x2 x2 x2 x2 x2 x2 x2 x2 x2 x1 x1 x1 x1 x1 x1 x1 x1) = λ x1 x2 . x1.

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

Assume H1: x1 (λ x2 x3 . (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x6) x2 x2 x2 x2 x2 x2 x2 x2 x2 x3 x3 x3 x3 ... ... ... ...) ....

...

■

Proofgold Proof