| λ x0 x1 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 . x0 (x1 x2 x8 x10 x6 x5 x9 x3 x7 x4 x11) (x1 x3 x2 x4 x5 x11 x8 x7 x10 x9 x6) (x1 x4 x5 x2 x3 x7 x6 x9 x8 x11 x10) (x1 x5 x9 x8 x2 x10 x11 x4 x3 x6 x7) (x1 x6 x10 x9 x11 x2 x7 x8 x4 x3 x5) (x1 x7 x3 x5 x4 x6 x2 x11 x9 x10 x8) (x1 x8 x7 x6 x10 x4 x3 x2 x11 x5 x9) (x1 x9 x6 x11 x7 x3 x5 x10 x2 x8 x4) (x1 x10 x11 x7 x8 x9 x4 x5 x6 x2 x3) (x1 x11 x4 x3 x9 x8 x10 x6 x5 x7 x2) |
|
| type |
|---|
| (ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι |
|
|
|
|
|
|
|
|
|