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

Assume H0: Church6_p x0.

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

Apply H0 with λ x2 : ι → ι → ι → ι → ι → ι → ι . Church6_squared_permutation__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5 x2 x1 = permargs_i_3_2_1_0_4_5 x1 leaving 6 subgoals.

Apply H1 with λ x2 : ι → ι → ι → ι → ι → ι → ι . Church6_squared_permutation__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5 (λ x3 x4 x5 x6 x7 x8 . x3) x2 = permargs_i_3_2_1_0_4_5 x2 leaving 4 subgoals.

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

Assume H2: x2 (Church6_squared_permutation__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5 (λ x3 x4 x5 x6 x7 x8 . x3) (λ x3 x4 x5 x6 x7 x8 . x3)) (permargs_i_3_2_1_0_4_5 (λ x3 x4 x5 x6 x7 x8 . x3)).

The subproof is completed by applying H2.

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

Assume H2: x2 (Church6_squared_permutation__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5 (λ x3 x4 x5 x6 x7 x8 . x3) (λ x3 x4 x5 x6 x7 x8 . x4)) (permargs_i_3_2_1_0_4_5 (λ x3 x4 x5 x6 x7 x8 . x4)).

The subproof is completed by applying H2.

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

Assume H2: x2 (Church6_squared_permutation__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5 (λ x3 x4 x5 x6 x7 x8 . x3) (λ x3 x4 x5 x6 x7 x8 . x5)) (permargs_i_3_2_1_0_4_5 (λ x3 x4 x5 x6 x7 x8 . x5)).

The subproof is completed by applying H2.

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

Assume H2: x2 (Church6_squared_permutation__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5 (λ x3 x4 x5 x6 x7 x8 . x3) (λ x3 x4 x5 x6 x7 x8 . x6)) (permargs_i_3_2_1_0_4_5 (λ x3 x4 x5 x6 x7 x8 . x6)).

The subproof is completed by applying H2.

Apply H1 with λ x2 : ι → ι → ι → ι → ι → ι → ι . Church6_squared_permutation__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5 (λ x3 x4 x5 x6 x7 x8 . x4) x2 = permargs_i_3_2_1_0_4_5 x2 leaving 4 subgoals.

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

Assume H2: x2 (Church6_squared_permutation__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5 (λ x3 x4 x5 x6 x7 x8 . x4) (λ x3 x4 x5 x6 x7 x8 . x3)) (permargs_i_3_2_1_0_4_5 (λ x3 x4 x5 x6 x7 x8 . x3)).

The subproof is completed by applying H2.

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

Assume H2: x2 (Church6_squared_permutation__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5 (λ x3 x4 x5 x6 x7 x8 . x4) (λ x3 x4 x5 x6 x7 x8 . x4)) (permargs_i_3_2_1_0_4_5 (λ x3 x4 x5 x6 x7 x8 . x4)).

The subproof is completed by applying H2.

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

Assume H2: x2 (Church6_squared_permutation__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5 (λ x3 x4 x5 x6 x7 x8 . x4) (λ x3 x4 x5 x6 x7 x8 . x5)) (permargs_i_3_2_1_0_4_5 (λ x3 x4 x5 x6 x7 x8 . x5)).

The subproof is completed by applying H2.

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

Assume H2: x2 (Church6_squared_permutation__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5 (λ x3 x4 x5 x6 x7 x8 . x4) (λ x3 x4 x5 x6 x7 x8 . x6)) (permargs_i_3_2_1_0_4_5 (λ x3 x4 x5 x6 x7 x8 . x6)).

The subproof is completed by applying H2.

Apply H1 with λ x2 : ι → ι → ι → ι → ι → ι → ι . Church6_squared_permutation__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5 (λ x3 x4 x5 x6 x7 x8 . x5) x2 = permargs_i_3_2_1_0_4_5 x2 leaving 4 subgoals.

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

Assume H2: x2 (Church6_squared_permutation__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5 (λ x3 x4 x5 x6 x7 x8 . x5) (λ x3 x4 x5 x6 x7 x8 . x3)) (permargs_i_3_2_1_0_4_5 (λ x3 x4 x5 x6 x7 x8 . x3)).

The subproof is completed by applying H2.

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

Assume H2: x2 (Church6_squared_permutation__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5 (λ x3 x4 x5 x6 x7 x8 . x5) (λ x3 x4 x5 x6 x7 x8 . x4)) (permargs_i_3_2_1_0_4_5 (λ x3 x4 x5 x6 x7 x8 . x4)).

The subproof is completed by applying H2.

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

Assume H2: x2 (Church6_squared_permutation__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5 (λ x3 x4 x5 x6 x7 x8 . x5) (λ x3 x4 x5 x6 x7 x8 . x5)) (permargs_i_3_2_1_0_4_5 (λ x3 x4 x5 x6 x7 x8 . x5)).

The subproof is completed by applying H2.

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

Assume H2: x2 (Church6_squared_permutation__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5 (λ x3 x4 x5 x6 x7 x8 . x5) (λ x3 x4 x5 x6 x7 x8 . x6)) (permargs_i_3_2_1_0_4_5 (λ x3 x4 x5 x6 x7 x8 . x6)).

The subproof is completed by applying H2.

Apply H1 with λ x2 : ι → ι → ι → ι → ι → ι → ι . Church6_squared_permutation__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5 (λ x3 x4 x5 x6 x7 x8 . x6) x2 = permargs_i_3_2_1_0_4_5 x2 leaving 4 subgoals.

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

Assume H2: x2 (Church6_squared_permutation__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5 (λ x3 x4 x5 x6 x7 x8 . x6) (λ x3 x4 x5 x6 x7 x8 . x3)) (permargs_i_3_2_1_0_4_5 (λ x3 x4 x5 x6 x7 x8 . x3)).

The subproof is completed by applying H2.

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

Assume H2: x2 (Church6_squared_permutation__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5 (λ x3 x4 x5 x6 x7 x8 . x6) (λ x3 x4 x5 x6 x7 x8 . x4)) (permargs_i_3_2_1_0_4_5 (λ x3 x4 x5 x6 x7 x8 . x4)).

The subproof is completed by applying H2.

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

Assume H2: x2 (Church6_squared_permutation__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5 (λ x3 x4 x5 x6 x7 x8 . x6) (λ x3 x4 x5 x6 x7 x8 . x5)) (permargs_i_3_2_1_0_4_5 (λ x3 x4 x5 x6 x7 x8 . x5)).

The subproof is completed by applying H2.

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

Assume H2: x2 (Church6_squared_permutation__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5 (λ x3 x4 x5 x6 x7 x8 . x6) (λ x3 x4 x5 x6 x7 x8 . x6)) (permargs_i_3_2_1_0_4_5 (λ x3 x4 x5 x6 x7 x8 . x6)).

The subproof is completed by applying H2.

Apply H1 with λ x2 : ι → ι → ι → ι → ι → ι → ι . Church6_squared_permutation__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5 (λ x3 x4 x5 x6 x7 x8 . x7) x2 = permargs_i_3_2_1_0_4_5 x2 leaving 4 subgoals.

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

Assume H2: x2 (Church6_squared_permutation__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5 (λ x3 x4 x5 x6 x7 x8 . x7) (λ x3 x4 x5 x6 x7 x8 . x3)) (permargs_i_3_2_1_0_4_5 (λ x3 x4 x5 x6 x7 x8 . x3)).

The subproof is completed by applying H2.

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

Assume H2: x2 (Church6_squared_permutation__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5 (λ x3 x4 x5 x6 x7 x8 . x7) ...) ....

...

■

Proofgold Proof