Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι be given.
Assume H0: x0 u12 = λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 . x13.
Assume H1: x0 u13 = λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 . x14.
Assume H2: x0 u14 = λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 . x15.
Assume H3: x0 u15 = λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 . x16.
Assume H4: x0 u16 = λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 . x17.
Let x1 of type ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι be given.
Assume H5: Church17_p x1.
Apply H5 with λ x2 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . 479e1.. x0 x2 x2 = λ x3 x4 . x4 leaving 17 subgoals.
Let x2 of type (ι → ι → ι) → (ι → ι → ι) → ο be given.
Assume H6: x2 (479e1.. x0 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x3) (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x3)) (λ x3 x4 . x4).
The subproof is completed by applying H6.
Let x2 of type (ι → ι → ι) → (ι → ι → ι) → ο be given.
Assume H6: x2 (479e1.. x0 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x4) (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x4)) (λ x3 x4 . x4).
The subproof is completed by applying H6.
Let x2 of type (ι → ι → ι) → (ι → ι → ι) → ο be given.
Assume H6: x2 (479e1.. x0 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x5) (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x5)) (λ x3 x4 . x4).
The subproof is completed by applying H6.
Let x2 of type (ι → ι → ι) → (ι → ι → ι) → ο be given.
Assume H6: x2 (479e1.. x0 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x6) (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x6)) (λ x3 x4 . x4).
The subproof is completed by applying H6.
Let x2 of type (ι → ι → ι) → (ι → ι → ι) → ο be given.
Assume H6: x2 (479e1.. x0 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x7) (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x7)) (λ x3 x4 . x4).
The subproof is completed by applying H6.
Let x2 of type (ι → ι → ι) → (ι → ι → ι) → ο be given.
Assume H6: x2 (479e1.. x0 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x8) (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x8)) (λ x3 x4 . x4).
The subproof is completed by applying H6.
Let x2 of type (ι → ι → ι) → (ι → ι → ι) → ο be given.
Assume H6: x2 (479e1.. x0 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x9) (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x9)) (λ x3 x4 . x4).
The subproof is completed by applying H6.
Let x2 of type (ι → ι → ι) → (ι → ι → ι) → ο be given.
Assume H6: x2 (479e1.. x0 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x10) (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x10)) (λ x3 x4 . x4).
The subproof is completed by applying H6.
Let x2 of type (ι → ι → ι) → (ι → ι → ι) → ο be given.
Assume H6: x2 (479e1.. x0 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x11) (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x11)) (λ x3 x4 . x4).
The subproof is completed by applying H6.
Let x2 of type (ι → ι → ι) → (ι → ι → ι) → ο be given.
Assume H6: x2 (479e1.. x0 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x12) (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x12)) (λ x3 x4 . x4).
The subproof is completed by applying H6.
Let x2 of type (ι → ι → ι) → (ι → ι → ι) → ο be given.
Assume H6: x2 (479e1.. x0 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x13) (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x13)) (λ x3 x4 . x4).
The subproof is completed by applying H6.
Let x2 of type (ι → ι → ι) → (ι → ι → ι) → ο be given.
Assume H6: x2 (479e1.. x0 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x14) (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x14)) (λ x3 x4 . x4).
The subproof is completed by applying H6.
Let x2 of type (ι → ι → ι) → (ι → ι → ι) → ο be given.
Assume H6: x2 (479e1.. x0 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x15) (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x15)) (λ x3 x4 . x4).
The subproof is completed by applying H6.
Let x2 of type (ι → ι → ι) → (ι → ι → ι) → ο be given.
Assume H6: x2 (479e1.. x0 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x16) (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x16)) (λ x3 x4 . x4).
The subproof is completed by applying H6.
Let x2 of type (ι → ι → ι) → (ι → ι → ι) → ο be given.
Assume H6: x2 (479e1.. x0 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x17) (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x17)) (λ x3 x4 . x4).
The subproof is completed by applying H6.
Let x2 of type (ι → ι → ι) → (ι → ι → ι) → ο be given.
Assume H6: x2 (479e1.. x0 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x18) (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x18)) (λ x3 x4 . x4).
The subproof is completed by applying H6.
Let x2 of type (ι → ι → ι) → (ι → ι → ι) → ο be given.
Assume H6: x2 (479e1.. x0 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x19) (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x19)) (λ x3 x4 . x4).
The subproof is completed by applying H6.
■