λ x0 x1 x2 . ∀ x3 : ι → ι → ι → ο . (∀ x4 . 74e69.. x4 ⟶ x3 c4def.. x4 x4) ⟶ (∀ x4 x5 x6 x7 x8 . x3 x7 x4 x5 ⟶ x3 x8 x5 x6 ⟶ x3 (6b90c.. x7 x8) x4 x6) ⟶ (∀ x4 . 74e69.. x4 ⟶ x3 c9248.. x4 5e331..) ⟶ (∀ x4 x5 x6 x7 . 74e69.. x6 ⟶ x3 x7 x4 x5 ⟶ x3 (a6e19.. x7) x4 (a3eb9.. x5 x6)) ⟶ (∀ x4 x5 x6 x7 . 74e69.. x5 ⟶ x3 x7 x4 x6 ⟶ x3 (2fe34.. x7) x4 (a3eb9.. x5 x6)) ⟶ (∀ x4 x5 x6 x7 x8 x9 . x3 x8 (bf68c.. x4 x6) x7 ⟶ x3 x9 (bf68c.. x5 x6) x7 ⟶ x3 (3e00e.. x8 x9) (bf68c.. (a3eb9.. x4 x5) x6) x7) ⟶ (∀ x4 x5 x6 x7 x8 . x3 x7 x4 x5 ⟶ x3 x8 x4 x6 ⟶ x3 (f9341.. x7 x8) x4 (bf68c.. x5 x6)) ⟶ (∀ x4 x5 x6 x7 . 74e69.. x5 ⟶ x3 x7 x4 x6 ⟶ x3 (1fa6d.. x7) (bf68c.. x4 x5) x6) ⟶ (∀ x4 x5 x6 x7 . 74e69.. x4 ⟶ x3 x7 x5 x6 ⟶ x3 (3a365.. x7) (bf68c.. x4 x5) x6) ⟶ x3 x0 x1 x2 |
|