λ x0 x1 x2 . ∀ x3 : ι → ι → ι → ο . (∀ x4 . x3 c4def.. x4 x4) ⟶ (∀ x4 x5 x6 x7 x8 . x3 x4 x6 x7 ⟶ x3 x5 x7 x8 ⟶ x3 (6b90c.. x4 x5) x6 x8) ⟶ (∀ x4 . x3 c9248.. x4 236c6..) ⟶ (∀ x4 x5 x6 . x3 x4 x5 x6 ⟶ x3 (a6e19.. x4) x5 (0b8ef.. x6)) ⟶ (∀ x4 x5 x6 . x3 x4 x5 x6 ⟶ x3 (2fe34.. x4) x5 (6c5f4.. x6)) ⟶ (∀ x4 x5 x6 x7 x8 . e05e6.. x5 ⟶ x3 x4 (cfc98.. x6 x7) x8 ⟶ x3 (3e00e.. x4 x5) (cfc98.. (0b8ef.. x6) x7) x8) ⟶ (∀ x4 x5 x6 x7 x8 . e05e6.. x4 ⟶ x3 x5 (cfc98.. x6 x7) x8 ⟶ x3 (3e00e.. x4 x5) (cfc98.. (6c5f4.. x6) x7) x8) ⟶ (∀ x4 x5 x6 x7 x8 . x3 x4 x6 x7 ⟶ x3 x5 x6 x8 ⟶ x3 (f9341.. x4 x5) x6 (cfc98.. x7 x8)) ⟶ (∀ x4 x5 x6 x7 . x3 x4 x5 x7 ⟶ x3 (1fa6d.. x4) (cfc98.. x5 x6) x7) ⟶ (∀ x4 x5 x6 x7 . x3 x4 x6 x7 ⟶ x3 (3a365.. x4) (cfc98.. x5 x6) x7) ⟶ x3 x0 x1 x2 |
|