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