Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι → ι → ι → ι → ι → ι → ι be given.
Assume H0: Church6_p x0.
Let x1 of type ι → ι → ι → ι → ι → ι → ι be given.
Assume H1: Church6_p x1.
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 (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) = 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) (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) = x2 leaving 6 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) (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))) (λ 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) (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))) (λ 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) (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))) (λ 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) (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))) (λ x3 x4 x5 x6 x7 x8 . x6).
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) (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 . x7))) (λ x3 x4 x5 x6 x7 x8 . x7).
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) (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 . x8))) (λ x3 x4 x5 x6 x7 x8 . x8).
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) (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) = x2 leaving 6 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) (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))) (λ 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) (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))) (λ 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) (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))) (λ 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) (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))) (λ x3 x4 x5 x6 x7 x8 . x6).
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) (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 . x7))) (λ x3 x4 x5 x6 x7 x8 . x7).
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) (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 . x8))) (λ x3 x4 x5 x6 x7 x8 . x8).
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) (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) = x2 leaving 6 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) (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))) (λ 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) (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))) (λ 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) (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))) (λ 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) (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 ... ...)) ....
...
...
...
...
...
...
■