Proofgold Asset

Param f14aa.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ο
Param not^not : ο → ο
Definition e8fec.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 . ∀ x11 : ο . (f14aa.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 ⟶ (x1 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x2 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x3 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x4 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x5 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x6 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x7 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x8 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x9 = x10 ⟶ ∀ x12 : ο . x12) ⟶ x0 x1 x10 ⟶ not (x0 x2 x10) ⟶ not (x0 x3 x10) ⟶ x0 x4 x10 ⟶ not (x0 x5 x10) ⟶ not (x0 x6 x10) ⟶ not (x0 x7 x10) ⟶ x0 x8 x10 ⟶ not (x0 x9 x10) ⟶ x11) ⟶ x11
Definition d8325.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 . ∀ x11 : ο . (f14aa.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 ⟶ (x1 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x2 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x3 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x4 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x5 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x6 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x7 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x8 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x9 = x10 ⟶ ∀ x12 : ο . x12) ⟶ x0 x1 x10 ⟶ x0 x2 x10 ⟶ not (x0 x3 x10) ⟶ x0 x4 x10 ⟶ not (x0 x5 x10) ⟶ not (x0 x6 x10) ⟶ not (x0 x7 x10) ⟶ x0 x8 x10 ⟶ not (x0 x9 x10) ⟶ x11) ⟶ x11
Param 13ddc.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ο
Definition e0b94.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 . ∀ x11 : ο . (13ddc.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 ⟶ (x1 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x2 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x3 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x4 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x5 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x6 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x7 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x8 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x9 = x10 ⟶ ∀ x12 : ο . x12) ⟶ x0 x1 x10 ⟶ x0 x2 x10 ⟶ not (x0 x3 x10) ⟶ x0 x4 x10 ⟶ not (x0 x5 x10) ⟶ not (x0 x6 x10) ⟶ not (x0 x7 x10) ⟶ x0 x8 x10 ⟶ not (x0 x9 x10) ⟶ x11) ⟶ x11
Param 130d9.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ο
Definition f63e8.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 . ∀ x11 : ο . (130d9.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 ⟶ (x1 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x2 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x3 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x4 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x5 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x6 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x7 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x8 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x9 = x10 ⟶ ∀ x12 : ο . x12) ⟶ x0 x1 x10 ⟶ x0 x2 x10 ⟶ not (x0 x3 x10) ⟶ not (x0 x4 x10) ⟶ not (x0 x5 x10) ⟶ not (x0 x6 x10) ⟶ not (x0 x7 x10) ⟶ x0 x8 x10 ⟶ not (x0 x9 x10) ⟶ x11) ⟶ x11
Param 0788d.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ο
Definition 251ab.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 . ∀ x11 : ο . (0788d.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 ⟶ (x1 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x2 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x3 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x4 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x5 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x6 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x7 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x8 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x9 = x10 ⟶ ∀ x12 : ο . x12) ⟶ x0 x1 x10 ⟶ x0 x2 x10 ⟶ x0 x3 x10 ⟶ not (x0 x4 x10) ⟶ not (x0 x5 x10) ⟶ not (x0 x6 x10) ⟶ not (x0 x7 x10) ⟶ x0 x8 x10 ⟶ not (x0 x9 x10) ⟶ x11) ⟶ x11
Param 65996.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ο
Definition 732e2.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 . ∀ x11 : ο . (65996.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 ⟶ (x1 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x2 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x3 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x4 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x5 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x6 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x7 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x8 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x9 = x10 ⟶ ∀ x12 : ο . x12) ⟶ x0 x1 x10 ⟶ x0 x2 x10 ⟶ x0 x3 x10 ⟶ not (x0 x4 x10) ⟶ not (x0 x5 x10) ⟶ not (x0 x6 x10) ⟶ not (x0 x7 x10) ⟶ x0 x8 x10 ⟶ not (x0 x9 x10) ⟶ x11) ⟶ x11
Param 24120.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ο
Definition 576d3.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 . ∀ x11 : ο . (24120.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 ⟶ (x1 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x2 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x3 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x4 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x5 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x6 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x7 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x8 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x9 = x10 ⟶ ∀ x12 : ο . x12) ⟶ not (x0 x1 x10) ⟶ not (x0 x2 x10) ⟶ x0 x3 x10 ⟶ not (x0 x4 x10) ⟶ not (x0 x5 x10) ⟶ not (x0 x6 x10) ⟶ not (x0 x7 x10) ⟶ x0 x8 x10 ⟶ not (x0 x9 x10) ⟶ x11) ⟶ x11
Param 58722.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ο
Definition 1a8a9.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 . ∀ x11 : ο . (58722.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 ⟶ (x1 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x2 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x3 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x4 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x5 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x6 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x7 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x8 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x9 = x10 ⟶ ∀ x12 : ο . x12) ⟶ not (x0 x1 x10) ⟶ x0 x2 x10 ⟶ x0 x3 x10 ⟶ not (x0 x4 x10) ⟶ not (x0 x5 x10) ⟶ not (x0 x6 x10) ⟶ not (x0 x7 x10) ⟶ x0 x8 x10 ⟶ not (x0 x9 x10) ⟶ x11) ⟶ x11
Definition 9ab74.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 . ∀ x11 : ο . (58722.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 ⟶ (x1 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x2 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x3 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x4 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x5 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x6 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x7 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x8 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x9 = x10 ⟶ ∀ x12 : ο . x12) ⟶ x0 x1 x10 ⟶ x0 x2 x10 ⟶ x0 x3 x10 ⟶ not (x0 x4 x10) ⟶ not (x0 x5 x10) ⟶ not (x0 x6 x10) ⟶ not (x0 x7 x10) ⟶ x0 x8 x10 ⟶ not (x0 x9 x10) ⟶ x11) ⟶ x11
Param 093ca.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ο
Definition 0f519.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 . ∀ x11 : ο . (093ca.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 ⟶ (x1 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x2 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x3 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x4 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x5 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x6 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x7 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x8 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x9 = x10 ⟶ ∀ x12 : ο . x12) ⟶ not (x0 x1 x10) ⟶ x0 x2 x10 ⟶ x0 x3 x10 ⟶ not (x0 x4 x10) ⟶ not (x0 x5 x10) ⟶ not (x0 x6 x10) ⟶ not (x0 x7 x10) ⟶ x0 x8 x10 ⟶ not (x0 x9 x10) ⟶ x11) ⟶ x11
Param 06d7e.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ο
Definition 1dd74.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 . ∀ x11 : ο . (06d7e.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 ⟶ (x1 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x2 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x3 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x4 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x5 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x6 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x7 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x8 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x9 = x10 ⟶ ∀ x12 : ο . x12) ⟶ x0 x1 x10 ⟶ x0 x2 x10 ⟶ x0 x3 x10 ⟶ not (x0 x4 x10) ⟶ not (x0 x5 x10) ⟶ not (x0 x6 x10) ⟶ not (x0 x7 x10) ⟶ x0 x8 x10 ⟶ not (x0 x9 x10) ⟶ x11) ⟶ x11
Param 21189.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ο
Definition 5932b.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 . ∀ x11 : ο . (21189.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 ⟶ (x1 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x2 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x3 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x4 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x5 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x6 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x7 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x8 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x9 = x10 ⟶ ∀ x12 : ο . x12) ⟶ x0 x1 x10 ⟶ x0 x2 x10 ⟶ x0 x3 x10 ⟶ not (x0 x4 x10) ⟶ not (x0 x5 x10) ⟶ not (x0 x6 x10) ⟶ not (x0 x7 x10) ⟶ x0 x8 x10 ⟶ not (x0 x9 x10) ⟶ x11) ⟶ x11
Param 8c9ed.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ο
Definition 53b49.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 . ∀ x11 : ο . (8c9ed.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 ⟶ (x1 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x2 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x3 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x4 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x5 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x6 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x7 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x8 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x9 = x10 ⟶ ∀ x12 : ο . x12) ⟶ x0 x1 x10 ⟶ x0 x2 x10 ⟶ not (x0 x3 x10) ⟶ x0 x4 x10 ⟶ not (x0 x5 x10) ⟶ not (x0 x6 x10) ⟶ not (x0 x7 x10) ⟶ x0 x8 x10 ⟶ not (x0 x9 x10) ⟶ x11) ⟶ x11
Param 47203.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ο
Definition 50a7f.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 . ∀ x11 : ο . (47203.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 ⟶ (x1 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x2 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x3 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x4 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x5 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x6 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x7 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x8 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x9 = x10 ⟶ ∀ x12 : ο . x12) ⟶ x0 x1 x10 ⟶ not (x0 x2 x10) ⟶ x0 x3 x10 ⟶ x0 x4 x10 ⟶ not (x0 x5 x10) ⟶ not (x0 x6 x10) ⟶ not (x0 x7 x10) ⟶ x0 x8 x10 ⟶ not (x0 x9 x10) ⟶ x11) ⟶ x11
Definition efbf0.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 . ∀ x11 : ο . (130d9.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 ⟶ (x1 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x2 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x3 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x4 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x5 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x6 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x7 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x8 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x9 = x10 ⟶ ∀ x12 : ο . x12) ⟶ x0 x1 x10 ⟶ x0 x2 x10 ⟶ not (x0 x3 x10) ⟶ x0 x4 x10 ⟶ not (x0 x5 x10) ⟶ not (x0 x6 x10) ⟶ not (x0 x7 x10) ⟶ x0 x8 x10 ⟶ not (x0 x9 x10) ⟶ x11) ⟶ x11
Param 58208.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ο
Definition c13a7.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 . ∀ x11 : ο . (58208.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 ⟶ (x1 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x2 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x3 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x4 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x5 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x6 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x7 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x8 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x9 = x10 ⟶ ∀ x12 : ο . x12) ⟶ x0 x1 x10 ⟶ x0 x2 x10 ⟶ not (x0 x3 x10) ⟶ x0 x4 x10 ⟶ not (x0 x5 x10) ⟶ not (x0 x6 x10) ⟶ not (x0 x7 x10) ⟶ x0 x8 x10 ⟶ not (x0 x9 x10) ⟶ x11) ⟶ x11
Param 2122d.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ο
Definition 9002a.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 . ∀ x11 : ο . (2122d.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 ⟶ (x1 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x2 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x3 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x4 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x5 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x6 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x7 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x8 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x9 = x10 ⟶ ∀ x12 : ο . x12) ⟶ x0 x1 x10 ⟶ not (x0 x2 x10) ⟶ x0 x3 x10 ⟶ x0 x4 x10 ⟶ not (x0 x5 x10) ⟶ not (x0 x6 x10) ⟶ not (x0 x7 x10) ⟶ x0 x8 x10 ⟶ not (x0 x9 x10) ⟶ x11) ⟶ x11
Param 4e6fe.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ο
Definition 62379.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 . ∀ x11 : ο . (4e6fe.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 ⟶ (x1 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x2 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x3 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x4 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x5 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x6 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x7 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x8 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x9 = x10 ⟶ ∀ x12 : ο . x12) ⟶ not (x0 x1 x10) ⟶ x0 x2 x10 ⟶ x0 x3 x10 ⟶ x0 x4 x10 ⟶ not (x0 x5 x10) ⟶ not (x0 x6 x10) ⟶ not (x0 x7 x10) ⟶ x0 x8 x10 ⟶ not (x0 x9 x10) ⟶ x11) ⟶ x11
Param 5c8a3.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ο
Definition 2e38c.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 . ∀ x11 : ο . (5c8a3.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 ⟶ (x1 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x2 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x3 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x4 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x5 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x6 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x7 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x8 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x9 = x10 ⟶ ∀ x12 : ο . x12) ⟶ not (x0 x1 x10) ⟶ x0 x2 x10 ⟶ not (x0 x3 x10) ⟶ x0 x4 x10 ⟶ not (x0 x5 x10) ⟶ not (x0 x6 x10) ⟶ not (x0 x7 x10) ⟶ x0 x8 x10 ⟶ not (x0 x9 x10) ⟶ x11) ⟶ x11
Param 02d0f.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ο
Definition 0897f.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 . ∀ x11 : ο . (02d0f.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 ⟶ (x1 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x2 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x3 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x4 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x5 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x6 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x7 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x8 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x9 = x10 ⟶ ∀ x12 : ο . x12) ⟶ x0 x1 x10 ⟶ x0 x2 x10 ⟶ not (x0 x3 x10) ⟶ x0 x4 x10 ⟶ not (x0 x5 x10) ⟶ not (x0 x6 x10) ⟶ not (x0 x7 x10) ⟶ x0 x8 x10 ⟶ not (x0 x9 x10) ⟶ x11) ⟶ x11
Param e9fc9.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ο
Definition 306f8.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 . ∀ x11 : ο . (e9fc9.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 ⟶ (x1 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x2 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x3 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x4 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x5 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x6 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x7 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x8 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x9 = x10 ⟶ ∀ x12 : ο . x12) ⟶ x0 x1 x10 ⟶ x0 x2 x10 ⟶ not (x0 x3 x10) ⟶ not (x0 x4 x10) ⟶ x0 x5 x10 ⟶ not (x0 x6 x10) ⟶ not (x0 x7 x10) ⟶ x0 x8 x10 ⟶ not (x0 x9 x10) ⟶ x11) ⟶ x11
Param 2ffc8.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ο
Definition 9ed6a.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 . ∀ x11 : ο . (2ffc8.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 ⟶ (x1 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x2 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x3 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x4 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x5 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x6 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x7 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x8 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x9 = x10 ⟶ ∀ x12 : ο . x12) ⟶ x0 x1 x10 ⟶ x0 x2 x10 ⟶ not (x0 x3 x10) ⟶ not (x0 x4 x10) ⟶ x0 x5 x10 ⟶ not (x0 x6 x10) ⟶ not (x0 x7 x10) ⟶ x0 x8 x10 ⟶ not (x0 x9 x10) ⟶ x11) ⟶ x11
Param ba015.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ο
Definition fee51.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 . ∀ x11 : ο . (ba015.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 ⟶ (x1 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x2 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x3 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x4 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x5 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x6 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x7 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x8 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x9 = x10 ⟶ ∀ x12 : ο . x12) ⟶ x0 x1 x10 ⟶ not (x0 x2 x10) ⟶ not (x0 x3 x10) ⟶ not (x0 x4 x10) ⟶ x0 x5 x10 ⟶ not (x0 x6 x10) ⟶ not (x0 x7 x10) ⟶ x0 x8 x10 ⟶ not (x0 x9 x10) ⟶ x11) ⟶ x11
Param 010eb.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ο
Definition bae07.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 . ∀ x11 : ο . (010eb.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 ⟶ (x1 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x2 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x3 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x4 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x5 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x6 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x7 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x8 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x9 = x10 ⟶ ∀ x12 : ο . x12) ⟶ x0 x1 x10 ⟶ x0 x2 x10 ⟶ not (x0 x3 x10) ⟶ not (x0 x4 x10) ⟶ x0 x5 x10 ⟶ not (x0 x6 x10) ⟶ not (x0 x7 x10) ⟶ x0 x8 x10 ⟶ not (x0 x9 x10) ⟶ x11) ⟶ x11
Definition cd4ee.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 . ∀ x11 : ο . (f14aa.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 ⟶ (x1 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x2 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x3 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x4 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x5 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x6 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x7 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x8 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x9 = x10 ⟶ ∀ x12 : ο . x12) ⟶ x0 x1 x10 ⟶ x0 x2 x10 ⟶ not (x0 x3 x10) ⟶ not (x0 x4 x10) ⟶ x0 x5 x10 ⟶ not (x0 x6 x10) ⟶ not (x0 x7 x10) ⟶ x0 x8 x10 ⟶ not (x0 x9 x10) ⟶ x11) ⟶ x11
Param 13b7c.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ο
Definition 22563.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 . ∀ x11 : ο . (13b7c.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 ⟶ (x1 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x2 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x3 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x4 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x5 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x6 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x7 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x8 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x9 = x10 ⟶ ∀ x12 : ο . x12) ⟶ x0 x1 x10 ⟶ x0 x2 x10 ⟶ not (x0 x3 x10) ⟶ not (x0 x4 x10) ⟶ x0 x5 x10 ⟶ not (x0 x6 x10) ⟶ not (x0 x7 x10) ⟶ x0 x8 x10 ⟶ not (x0 x9 x10) ⟶ x11) ⟶ x11
Param 87273.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ο
Definition bdc7f.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 . ∀ x11 : ο . (87273.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 ⟶ (x1 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x2 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x3 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x4 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x5 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x6 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x7 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x8 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x9 = x10 ⟶ ∀ x12 : ο . x12) ⟶ x0 x1 x10 ⟶ x0 x2 x10 ⟶ not (x0 x3 x10) ⟶ not (x0 x4 x10) ⟶ x0 x5 x10 ⟶ not (x0 x6 x10) ⟶ not (x0 x7 x10) ⟶ x0 x8 x10 ⟶ not (x0 x9 x10) ⟶ x11) ⟶ x11
Definition dfb78.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 . ∀ x11 : ο . (130d9.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 ⟶ (x1 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x2 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x3 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x4 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x5 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x6 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x7 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x8 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x9 = x10 ⟶ ∀ x12 : ο . x12) ⟶ x0 x1 x10 ⟶ x0 x2 x10 ⟶ not (x0 x3 x10) ⟶ not (x0 x4 x10) ⟶ x0 x5 x10 ⟶ not (x0 x6 x10) ⟶ not (x0 x7 x10) ⟶ x0 x8 x10 ⟶ not (x0 x9 x10) ⟶ x11) ⟶ x11
Definition f8ada.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 . ∀ x11 : ο . (58208.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 ⟶ (x1 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x2 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x3 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x4 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x5 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x6 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x7 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x8 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x9 = x10 ⟶ ∀ x12 : ο . x12) ⟶ x0 x1 x10 ⟶ x0 x2 x10 ⟶ not (x0 x3 x10) ⟶ not (x0 x4 x10) ⟶ x0 x5 x10 ⟶ not (x0 x6 x10) ⟶ not (x0 x7 x10) ⟶ x0 x8 x10 ⟶ not (x0 x9 x10) ⟶ x11) ⟶ x11
Param 90d0e.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ο
Definition d3342.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 . ∀ x11 : ο . (90d0e.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 ⟶ (x1 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x2 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x3 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x4 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x5 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x6 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x7 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x8 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x9 = x10 ⟶ ∀ x12 : ο . x12) ⟶ x0 x1 x10 ⟶ not (x0 x2 x10) ⟶ not (x0 x3 x10) ⟶ not (x0 x4 x10) ⟶ x0 x5 x10 ⟶ not (x0 x6 x10) ⟶ not (x0 x7 x10) ⟶ x0 x8 x10 ⟶ not (x0 x9 x10) ⟶ x11) ⟶ x11
Param 055d9.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ο
Definition 0f762.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 . ∀ x11 : ο . (055d9.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 ⟶ (x1 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x2 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x3 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x4 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x5 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x6 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x7 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x8 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x9 = x10 ⟶ ∀ x12 : ο . x12) ⟶ x0 x1 x10 ⟶ x0 x2 x10 ⟶ not (x0 x3 x10) ⟶ not (x0 x4 x10) ⟶ x0 x5 x10 ⟶ not (x0 x6 x10) ⟶ not (x0 x7 x10) ⟶ x0 x8 x10 ⟶ not (x0 x9 x10) ⟶ x11) ⟶ x11
Param b0e38.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ο
Definition 55451.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 . ∀ x11 : ο . (b0e38.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 ⟶ (x1 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x2 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x3 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x4 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x5 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x6 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x7 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x8 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x9 = x10 ⟶ ∀ x12 : ο . x12) ⟶ x0 x1 x10 ⟶ x0 x2 x10 ⟶ not (x0 x3 x10) ⟶ not (x0 x4 x10) ⟶ x0 x5 x10 ⟶ not (x0 x6 x10) ⟶ not (x0 x7 x10) ⟶ x0 x8 x10 ⟶ not (x0 x9 x10) ⟶ x11) ⟶ x11
Definition f380c.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 . ∀ x11 : ο . (093ca.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 ⟶ (x1 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x2 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x3 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x4 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x5 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x6 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x7 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x8 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x9 = x10 ⟶ ∀ x12 : ο . x12) ⟶ x0 x1 x10 ⟶ x0 x2 x10 ⟶ not (x0 x3 x10) ⟶ not (x0 x4 x10) ⟶ x0 x5 x10 ⟶ not (x0 x6 x10) ⟶ not (x0 x7 x10) ⟶ x0 x8 x10 ⟶ not (x0 x9 x10) ⟶ x11) ⟶ x11
Param 96162.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ο
Definition 42e23.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 . ∀ x11 : ο . (96162.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 ⟶ (x1 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x2 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x3 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x4 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x5 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x6 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x7 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x8 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x9 = x10 ⟶ ∀ x12 : ο . x12) ⟶ x0 x1 x10 ⟶ x0 x2 x10 ⟶ not (x0 x3 x10) ⟶ not (x0 x4 x10) ⟶ x0 x5 x10 ⟶ not (x0 x6 x10) ⟶ not (x0 x7 x10) ⟶ x0 x8 x10 ⟶ not (x0 x9 x10) ⟶ x11) ⟶ x11
Definition 8bcec.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 . ∀ x11 : ο . (06d7e.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 ⟶ (x1 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x2 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x3 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x4 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x5 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x6 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x7 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x8 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x9 = x10 ⟶ ∀ x12 : ο . x12) ⟶ x0 x1 x10 ⟶ x0 x2 x10 ⟶ not (x0 x3 x10) ⟶ not (x0 x4 x10) ⟶ x0 x5 x10 ⟶ not (x0 x6 x10) ⟶ not (x0 x7 x10) ⟶ x0 x8 x10 ⟶ not (x0 x9 x10) ⟶ x11) ⟶ x11
Param f3db6.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ο
Definition 1c6c9.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 . ∀ x11 : ο . (f3db6.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 ⟶ (x1 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x2 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x3 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x4 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x5 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x6 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x7 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x8 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x9 = x10 ⟶ ∀ x12 : ο . x12) ⟶ x0 x1 x10 ⟶ x0 x2 x10 ⟶ not (x0 x3 x10) ⟶ not (x0 x4 x10) ⟶ x0 x5 x10 ⟶ not (x0 x6 x10) ⟶ not (x0 x7 x10) ⟶ x0 x8 x10 ⟶ not (x0 x9 x10) ⟶ x11) ⟶ x11
Param 1a9c5.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ο
Definition 754da.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 . ∀ x11 : ο . (1a9c5.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 ⟶ (x1 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x2 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x3 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x4 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x5 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x6 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x7 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x8 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x9 = x10 ⟶ ∀ x12 : ο . x12) ⟶ x0 x1 x10 ⟶ x0 x2 x10 ⟶ not (x0 x3 x10) ⟶ not (x0 x4 x10) ⟶ x0 x5 x10 ⟶ not (x0 x6 x10) ⟶ not (x0 x7 x10) ⟶ x0 x8 x10 ⟶ not (x0 x9 x10) ⟶ x11) ⟶ x11
Param d2a2c.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ο
Definition a4ce7.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 . ∀ x11 : ο . (d2a2c.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 ⟶ (x1 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x2 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x3 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x4 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x5 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x6 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x7 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x8 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x9 = x10 ⟶ ∀ x12 : ο . x12) ⟶ x0 x1 x10 ⟶ x0 x2 x10 ⟶ not (x0 x3 x10) ⟶ not (x0 x4 x10) ⟶ x0 x5 x10 ⟶ not (x0 x6 x10) ⟶ not (x0 x7 x10) ⟶ x0 x8 x10 ⟶ not (x0 x9 x10) ⟶ x11) ⟶ x11
Param a13f2.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ο
Definition 60a51.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 . ∀ x11 : ο . (a13f2.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 ⟶ (x1 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x2 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x3 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x4 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x5 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x6 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x7 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x8 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x9 = x10 ⟶ ∀ x12 : ο . x12) ⟶ x0 x1 x10 ⟶ x0 x2 x10 ⟶ not (x0 x3 x10) ⟶ not (x0 x4 x10) ⟶ x0 x5 x10 ⟶ not (x0 x6 x10) ⟶ not (x0 x7 x10) ⟶ x0 x8 x10 ⟶ not (x0 x9 x10) ⟶ x11) ⟶ x11
Param d3618.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ο
Definition ea33e.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 . ∀ x11 : ο . (d3618.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 ⟶ (x1 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x2 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x3 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x4 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x5 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x6 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x7 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x8 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x9 = x10 ⟶ ∀ x12 : ο . x12) ⟶ x0 x1 x10 ⟶ x0 x2 x10 ⟶ not (x0 x3 x10) ⟶ not (x0 x4 x10) ⟶ not (x0 x5 x10) ⟶ not (x0 x6 x10) ⟶ not (x0 x7 x10) ⟶ x0 x8 x10 ⟶ not (x0 x9 x10) ⟶ x11) ⟶ x11
Param fb26f.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ο
Definition 9fce6.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 . ∀ x11 : ο . (fb26f.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 ⟶ (x1 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x2 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x3 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x4 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x5 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x6 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x7 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x8 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x9 = x10 ⟶ ∀ x12 : ο . x12) ⟶ x0 x1 x10 ⟶ x0 x2 x10 ⟶ x0 x3 x10 ⟶ not (x0 x4 x10) ⟶ not (x0 x5 x10) ⟶ not (x0 x6 x10) ⟶ not (x0 x7 x10) ⟶ x0 x8 x10 ⟶ not (x0 x9 x10) ⟶ x11) ⟶ x11
Param 2dac5.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ο
Definition 0aaf4.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 . ∀ x11 : ο . (2dac5.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 ⟶ (x1 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x2 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x3 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x4 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x5 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x6 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x7 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x8 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x9 = x10 ⟶ ∀ x12 : ο . x12) ⟶ x0 x1 x10 ⟶ x0 x2 x10 ⟶ x0 x3 x10 ⟶ not (x0 x4 x10) ⟶ not (x0 x5 x10) ⟶ not (x0 x6 x10) ⟶ not (x0 x7 x10) ⟶ x0 x8 x10 ⟶ not (x0 x9 x10) ⟶ x11) ⟶ x11
Param a4abc.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ο
Definition ce3b4.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 . ∀ x11 : ο . (a4abc.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 ⟶ (x1 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x2 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x3 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x4 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x5 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x6 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x7 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x8 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x9 = x10 ⟶ ∀ x12 : ο . x12) ⟶ x0 x1 x10 ⟶ x0 x2 x10 ⟶ not (x0 x3 x10) ⟶ not (x0 x4 x10) ⟶ not (x0 x5 x10) ⟶ not (x0 x6 x10) ⟶ not (x0 x7 x10) ⟶ x0 x8 x10 ⟶ not (x0 x9 x10) ⟶ x11) ⟶ x11
Definition 27e6e.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 . ∀ x11 : ο . (a4abc.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 ⟶ (x1 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x2 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x3 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x4 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x5 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x6 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x7 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x8 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x9 = x10 ⟶ ∀ x12 : ο . x12) ⟶ not (x0 x1 x10) ⟶ not (x0 x2 x10) ⟶ x0 x3 x10 ⟶ not (x0 x4 x10) ⟶ not (x0 x5 x10) ⟶ not (x0 x6 x10) ⟶ not (x0 x7 x10) ⟶ x0 x8 x10 ⟶ not (x0 x9 x10) ⟶ x11) ⟶ x11
Definition a89de.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 . ∀ x11 : ο . (a4abc.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 ⟶ (x1 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x2 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x3 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x4 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x5 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x6 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x7 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x8 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x9 = x10 ⟶ ∀ x12 : ο . x12) ⟶ x0 x1 x10 ⟶ not (x0 x2 x10) ⟶ x0 x3 x10 ⟶ not (x0 x4 x10) ⟶ not (x0 x5 x10) ⟶ not (x0 x6 x10) ⟶ not (x0 x7 x10) ⟶ x0 x8 x10 ⟶ not (x0 x9 x10) ⟶ x11) ⟶ x11
Param c7001.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ο
Definition f5fe1.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 . ∀ x11 : ο . (c7001.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 ⟶ (x1 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x2 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x3 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x4 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x5 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x6 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x7 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x8 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x9 = x10 ⟶ ∀ x12 : ο . x12) ⟶ x0 x1 x10 ⟶ x0 x2 x10 ⟶ x0 x3 x10 ⟶ not (x0 x4 x10) ⟶ not (x0 x5 x10) ⟶ not (x0 x6 x10) ⟶ not (x0 x7 x10) ⟶ x0 x8 x10 ⟶ not (x0 x9 x10) ⟶ x11) ⟶ x11
Definition fd185.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 . ∀ x11 : ο . (a4abc.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 ⟶ (x1 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x2 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x3 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x4 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x5 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x6 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x7 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x8 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x9 = x10 ⟶ ∀ x12 : ο . x12) ⟶ x0 x1 x10 ⟶ x0 x2 x10 ⟶ x0 x3 x10 ⟶ not (x0 x4 x10) ⟶ not (x0 x5 x10) ⟶ not (x0 x6 x10) ⟶ not (x0 x7 x10) ⟶ x0 x8 x10 ⟶ not (x0 x9 x10) ⟶ x11) ⟶ x11
Param f51b8.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ο
Definition b7bfe.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 . ∀ x11 : ο . (f51b8.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 ⟶ (x1 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x2 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x3 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x4 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x5 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x6 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x7 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x8 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x9 = x10 ⟶ ∀ x12 : ο . x12) ⟶ x0 x1 x10 ⟶ x0 x2 x10 ⟶ x0 x3 x10 ⟶ not (x0 x4 x10) ⟶ not (x0 x5 x10) ⟶ not (x0 x6 x10) ⟶ not (x0 x7 x10) ⟶ x0 x8 x10 ⟶ not (x0 x9 x10) ⟶ x11) ⟶ x11
Definition 86078.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 . ∀ x11 : ο . (d3618.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 ⟶ (x1 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x2 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x3 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x4 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x5 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x6 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x7 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x8 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x9 = x10 ⟶ ∀ x12 : ο . x12) ⟶ x0 x1 x10 ⟶ x0 x2 x10 ⟶ not (x0 x3 x10) ⟶ not (x0 x4 x10) ⟶ x0 x5 x10 ⟶ not (x0 x6 x10) ⟶ not (x0 x7 x10) ⟶ x0 x8 x10 ⟶ not (x0 x9 x10) ⟶ x11) ⟶ x11
Param dcb32.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ο
Definition d29be.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 . ∀ x11 : ο . (dcb32.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 ⟶ (x1 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x2 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x3 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x4 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x5 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x6 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x7 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x8 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x9 = x10 ⟶ ∀ x12 : ο . x12) ⟶ x0 x1 x10 ⟶ not (x0 x2 x10) ⟶ not (x0 x3 x10) ⟶ not (x0 x4 x10) ⟶ x0 x5 x10 ⟶ not (x0 x6 x10) ⟶ not (x0 x7 x10) ⟶ x0 x8 x10 ⟶ not (x0 x9 x10) ⟶ x11) ⟶ x11
Definition 5cc7a.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 . ∀ x11 : ο . (dcb32.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 ⟶ (x1 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x2 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x3 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x4 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x5 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x6 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x7 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x8 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x9 = x10 ⟶ ∀ x12 : ο . x12) ⟶ x0 x1 x10 ⟶ x0 x2 x10 ⟶ not (x0 x3 x10) ⟶ not (x0 x4 x10) ⟶ x0 x5 x10 ⟶ not (x0 x6 x10) ⟶ not (x0 x7 x10) ⟶ x0 x8 x10 ⟶ not (x0 x9 x10) ⟶ x11) ⟶ x11
Definition 49015.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 . ∀ x11 : ο . (c7001.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 ⟶ (x1 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x2 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x3 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x4 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x5 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x6 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x7 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x8 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x9 = x10 ⟶ ∀ x12 : ο . x12) ⟶ x0 x1 x10 ⟶ x0 x2 x10 ⟶ not (x0 x3 x10) ⟶ not (x0 x4 x10) ⟶ x0 x5 x10 ⟶ not (x0 x6 x10) ⟶ not (x0 x7 x10) ⟶ x0 x8 x10 ⟶ not (x0 x9 x10) ⟶ x11) ⟶ x11
Definition 9dea4.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 . ∀ x11 : ο . (a4abc.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 ⟶ (x1 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x2 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x3 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x4 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x5 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x6 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x7 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x8 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x9 = x10 ⟶ ∀ x12 : ο . x12) ⟶ x0 x1 x10 ⟶ x0 x2 x10 ⟶ not (x0 x3 x10) ⟶ not (x0 x4 x10) ⟶ x0 x5 x10 ⟶ not (x0 x6 x10) ⟶ not (x0 x7 x10) ⟶ x0 x8 x10 ⟶ not (x0 x9 x10) ⟶ x11) ⟶ x11
Definition f0075.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 . ∀ x11 : ο . (f51b8.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 ⟶ (x1 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x2 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x3 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x4 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x5 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x6 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x7 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x8 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x9 = x10 ⟶ ∀ x12 : ο . x12) ⟶ x0 x1 x10 ⟶ x0 x2 x10 ⟶ not (x0 x3 x10) ⟶ not (x0 x4 x10) ⟶ x0 x5 x10 ⟶ not (x0 x6 x10) ⟶ not (x0 x7 x10) ⟶ x0 x8 x10 ⟶ not (x0 x9 x10) ⟶ x11) ⟶ x11
Param a1497.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ο
Definition 0a362.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 . ∀ x11 : ο . (a1497.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 ⟶ (x1 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x2 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x3 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x4 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x5 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x6 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x7 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x8 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x9 = x10 ⟶ ∀ x12 : ο . x12) ⟶ not (x0 x1 x10) ⟶ x0 x2 x10 ⟶ x0 x3 x10 ⟶ not (x0 x4 x10) ⟶ not (x0 x5 x10) ⟶ not (x0 x6 x10) ⟶ not (x0 x7 x10) ⟶ x0 x8 x10 ⟶ not (x0 x9 x10) ⟶ x11) ⟶ x11
Param d2e51.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ο
Definition 6b1e6.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 . ∀ x11 : ο . (d2e51.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 ⟶ (x1 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x2 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x3 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x4 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x5 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x6 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x7 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x8 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x9 = x10 ⟶ ∀ x12 : ο . x12) ⟶ x0 x1 x10 ⟶ not (x0 x2 x10) ⟶ x0 x3 x10 ⟶ not (x0 x4 x10) ⟶ not (x0 x5 x10) ⟶ not (x0 x6 x10) ⟶ not (x0 x7 x10) ⟶ x0 x8 x10 ⟶ not (x0 x9 x10) ⟶ x11) ⟶ x11
Param 8acce.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ο
Definition e9c43.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 . ∀ x11 : ο . (8acce.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 ⟶ (x1 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x2 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x3 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x4 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x5 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x6 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x7 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x8 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x9 = x10 ⟶ ∀ x12 : ο . x12) ⟶ x0 x1 x10 ⟶ x0 x2 x10 ⟶ x0 x3 x10 ⟶ not (x0 x4 x10) ⟶ not (x0 x5 x10) ⟶ not (x0 x6 x10) ⟶ not (x0 x7 x10) ⟶ x0 x8 x10 ⟶ not (x0 x9 x10) ⟶ x11) ⟶ x11
Param 1ecf8.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ο
Definition a3d78.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 . ∀ x11 : ο . (1ecf8.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 ⟶ (x1 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x2 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x3 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x4 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x5 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x6 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x7 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x8 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x9 = x10 ⟶ ∀ x12 : ο . x12) ⟶ x0 x1 x10 ⟶ x0 x2 x10 ⟶ not (x0 x3 x10) ⟶ not (x0 x4 x10) ⟶ not (x0 x5 x10) ⟶ not (x0 x6 x10) ⟶ not (x0 x7 x10) ⟶ x0 x8 x10 ⟶ not (x0 x9 x10) ⟶ x11) ⟶ x11
Definition 11982.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 . ∀ x11 : ο . (1ecf8.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 ⟶ (x1 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x2 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x3 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x4 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x5 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x6 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x7 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x8 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x9 = x10 ⟶ ∀ x12 : ο . x12) ⟶ not (x0 x1 x10) ⟶ x0 x2 x10 ⟶ x0 x3 x10 ⟶ not (x0 x4 x10) ⟶ not (x0 x5 x10) ⟶ not (x0 x6 x10) ⟶ not (x0 x7 x10) ⟶ x0 x8 x10 ⟶ not (x0 x9 x10) ⟶ x11) ⟶ x11
Param aa64f.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ο
Definition fe4dd.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 . ∀ x11 : ο . (aa64f.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 ⟶ (x1 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x2 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x3 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x4 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x5 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x6 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x7 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x8 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x9 = x10 ⟶ ∀ x12 : ο . x12) ⟶ not (x0 x1 x10) ⟶ x0 x2 x10 ⟶ x0 x3 x10 ⟶ not (x0 x4 x10) ⟶ not (x0 x5 x10) ⟶ not (x0 x6 x10) ⟶ not (x0 x7 x10) ⟶ x0 x8 x10 ⟶ not (x0 x9 x10) ⟶ x11) ⟶ x11
Param c705c.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ο
Definition b5215.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 . ∀ x11 : ο . (c705c.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 ⟶ (x1 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x2 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x3 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x4 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x5 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x6 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x7 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x8 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x9 = x10 ⟶ ∀ x12 : ο . x12) ⟶ x0 x1 x10 ⟶ x0 x2 x10 ⟶ x0 x3 x10 ⟶ not (x0 x4 x10) ⟶ not (x0 x5 x10) ⟶ not (x0 x6 x10) ⟶ not (x0 x7 x10) ⟶ x0 x8 x10 ⟶ not (x0 x9 x10) ⟶ x11) ⟶ x11
Param 70a3c.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ο
Definition f982a.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 . ∀ x11 : ο . (70a3c.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 ⟶ (x1 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x2 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x3 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x4 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x5 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x6 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x7 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x8 = x10 ⟶ ∀ x12 : ο . x12) ⟶ (x9 = x10 ⟶ ∀ x12 : ο . x12) ⟶ x0 x1 x10 ⟶ not (x0 x2 x10) ⟶ x0 x3 x10 ⟶ x0 x4 x10 ⟶ not (x0 x5 x10) ⟶ not (x0 x6 x10) ⟶ not (x0 x7 x10) ⟶ x0 x8 x10 ⟶ not (x0 x9 x10) ⟶ x11) ⟶ x11