Proofgold Asset

Param 4402e.. : ι → (ι → ι → ο) → ο
Param cf2df.. : ι → (ι → ι → ο) → ο
Param Subq^Subq : ι → ι → ο
Param setminus^setminus : ι → ι → ι
Param Sing^Sing : ι → ι
Param 7f677.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ο
Param 2426f.. : ι → (ι → ι → ο) → ο
Known edbc7.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ 4402e.. x0 x1 ⟶ cf2df.. x0 x1 ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ⊆ setminus x0 (Sing x2) ⟶ ∀ x4 . x4 ∈ x3 ⟶ ∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ 7f677.. x1 x4 x5 x6 x7 x8 x9 x10 ⟶ 2426f.. x0 x1
Param 58366.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ο
Known fa676.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ 4402e.. x0 x1 ⟶ cf2df.. x0 x1 ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ⊆ setminus x0 (Sing x2) ⟶ ∀ x4 . x4 ∈ x3 ⟶ ∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ 58366.. x1 x4 x5 x6 x7 x8 x9 x10 ⟶ 2426f.. x0 x1
Param c9184.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ο
Known 1fb85.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ 4402e.. x0 x1 ⟶ cf2df.. x0 x1 ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ⊆ setminus x0 (Sing x2) ⟶ ∀ x4 . x4 ∈ x3 ⟶ ∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ c9184.. x1 x4 x5 x6 x7 x8 x9 x10 ⟶ 2426f.. x0 x1
Param e7595.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ο
Known a1199.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ 4402e.. x0 x1 ⟶ cf2df.. x0 x1 ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ⊆ setminus x0 (Sing x2) ⟶ ∀ x4 . x4 ∈ x3 ⟶ ∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ e7595.. x1 x4 x5 x6 x7 x8 x9 x10 ⟶ 2426f.. x0 x1
Param 8c395.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ο
Known 11597.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ 4402e.. x0 x1 ⟶ cf2df.. x0 x1 ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ⊆ setminus x0 (Sing x2) ⟶ ∀ x4 . x4 ∈ x3 ⟶ ∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ 8c395.. x1 x4 x5 x6 x7 x8 x9 x10 ⟶ 2426f.. x0 x1
Param 88b7c.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ο
Known 31721.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ 4402e.. x0 x1 ⟶ cf2df.. x0 x1 ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ⊆ setminus x0 (Sing x2) ⟶ ∀ x4 . x4 ∈ x3 ⟶ ∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ 88b7c.. x1 x4 x5 x6 x7 x8 x9 x10 ⟶ 2426f.. x0 x1
Param ae506.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ο
Known 997f9.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ 4402e.. x0 x1 ⟶ cf2df.. x0 x1 ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ⊆ setminus x0 (Sing x2) ⟶ ∀ x4 . x4 ∈ x3 ⟶ ∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ae506.. x1 x4 x5 x6 x7 x8 x9 x10 ⟶ 2426f.. x0 x1
Param 98053.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ο
Known fa633.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ 4402e.. x0 x1 ⟶ cf2df.. x0 x1 ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ⊆ setminus x0 (Sing x2) ⟶ ∀ x4 . x4 ∈ x3 ⟶ ∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ 98053.. x1 x4 x5 x6 x7 x8 x9 x10 ⟶ 2426f.. x0 x1
Param 5db61.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ο
Known 0c7ba.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ 4402e.. x0 x1 ⟶ cf2df.. x0 x1 ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ⊆ setminus x0 (Sing x2) ⟶ ∀ x4 . x4 ∈ x3 ⟶ ∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ 5db61.. x1 x4 x5 x6 x7 x8 x9 x10 ⟶ 2426f.. x0 x1
Param 182cc.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ο
Known baebc.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ 4402e.. x0 x1 ⟶ cf2df.. x0 x1 ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ⊆ setminus x0 (Sing x2) ⟶ ∀ x4 . x4 ∈ x3 ⟶ ∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ 182cc.. x1 x4 x5 x6 x7 x8 x9 x10 ⟶ 2426f.. x0 x1
Param 796c4.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ο
Known 06ff5.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ 4402e.. x0 x1 ⟶ cf2df.. x0 x1 ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ⊆ setminus x0 (Sing x2) ⟶ ∀ x4 . x4 ∈ x3 ⟶ ∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ 796c4.. x1 x4 x5 x6 x7 x8 x9 x10 ⟶ 2426f.. x0 x1
Param 084ea.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ο
Known d2797.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ 4402e.. x0 x1 ⟶ cf2df.. x0 x1 ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ⊆ setminus x0 (Sing x2) ⟶ ∀ x4 . x4 ∈ x3 ⟶ ∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ 084ea.. x1 x4 x5 x6 x7 x8 x9 x10 ⟶ 2426f.. x0 x1
Param 3819d.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ο
Known 47c02.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ 4402e.. x0 x1 ⟶ cf2df.. x0 x1 ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ⊆ setminus x0 (Sing x2) ⟶ ∀ x4 . x4 ∈ x3 ⟶ ∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ 3819d.. x1 x4 x5 x6 x7 x8 x9 x10 ⟶ 2426f.. x0 x1
Param 6ca1f.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ο
Known 7465c.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ 4402e.. x0 x1 ⟶ cf2df.. x0 x1 ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ⊆ setminus x0 (Sing x2) ⟶ ∀ x4 . x4 ∈ x3 ⟶ ∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ 6ca1f.. x1 x4 x5 x6 x7 x8 x9 x10 ⟶ 2426f.. x0 x1
Param 99de9.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ο
Known beaad.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ 4402e.. x0 x1 ⟶ cf2df.. x0 x1 ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ⊆ setminus x0 (Sing x2) ⟶ ∀ x4 . x4 ∈ x3 ⟶ ∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ 99de9.. x1 x4 x5 x6 x7 x8 x9 x10 ⟶ 2426f.. x0 x1
Param cb525.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ο
Known 94ea3.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ 4402e.. x0 x1 ⟶ cf2df.. x0 x1 ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ⊆ setminus x0 (Sing x2) ⟶ ∀ x4 . x4 ∈ x3 ⟶ ∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ cb525.. x1 x4 x5 x6 x7 x8 x9 x10 ⟶ 2426f.. x0 x1
Param 3109c.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ο
Known 5b472.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ 4402e.. x0 x1 ⟶ cf2df.. x0 x1 ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ⊆ setminus x0 (Sing x2) ⟶ ∀ x4 . x4 ∈ x3 ⟶ ∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ 3109c.. x1 x4 x5 x6 x7 x8 x9 x10 ⟶ 2426f.. x0 x1
Param 2319a.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ο
Known 87967.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ 4402e.. x0 x1 ⟶ cf2df.. x0 x1 ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ⊆ setminus x0 (Sing x2) ⟶ ∀ x4 . x4 ∈ x3 ⟶ ∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ 2319a.. x1 x4 x5 x6 x7 x8 x9 x10 ⟶ 2426f.. x0 x1
Param 323f1.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ο
Known 85413.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ 4402e.. x0 x1 ⟶ cf2df.. x0 x1 ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ⊆ setminus x0 (Sing x2) ⟶ ∀ x4 . x4 ∈ x3 ⟶ ∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ 323f1.. x1 x4 x5 x6 x7 x8 x9 x10 ⟶ 2426f.. x0 x1
Param 16c0f.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ο
Known cf81d.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ 4402e.. x0 x1 ⟶ cf2df.. x0 x1 ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ⊆ setminus x0 (Sing x2) ⟶ ∀ x4 . x4 ∈ x3 ⟶ ∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ 16c0f.. x1 x4 x5 x6 x7 x8 x9 x10 ⟶ 2426f.. x0 x1
Param 36d58.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ο
Known 4221f.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ 4402e.. x0 x1 ⟶ cf2df.. x0 x1 ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ⊆ setminus x0 (Sing x2) ⟶ ∀ x4 . x4 ∈ x3 ⟶ ∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ 36d58.. x1 x4 x5 x6 x7 x8 x9 x10 ⟶ 2426f.. x0 x1
Param 28e31.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ο
Known a5918.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ 4402e.. x0 x1 ⟶ cf2df.. x0 x1 ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ⊆ setminus x0 (Sing x2) ⟶ ∀ x4 . x4 ∈ x3 ⟶ ∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ 28e31.. x1 x4 x5 x6 x7 x8 x9 x10 ⟶ 2426f.. x0 x1
Param 02f3e.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ο
Known 45e44.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ 4402e.. x0 x1 ⟶ cf2df.. x0 x1 ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ⊆ setminus x0 (Sing x2) ⟶ ∀ x4 . x4 ∈ x3 ⟶ ∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ 02f3e.. x1 x4 x5 x6 x7 x8 x9 x10 ⟶ 2426f.. x0 x1
Param 28532.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ο
Known c912e.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ 4402e.. x0 x1 ⟶ cf2df.. x0 x1 ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ⊆ setminus x0 (Sing x2) ⟶ ∀ x4 . x4 ∈ x3 ⟶ ∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ 28532.. x1 x4 x5 x6 x7 x8 x9 x10 ⟶ 2426f.. x0 x1
Param e8ae3.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ο
Known 2805f.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ 4402e.. x0 x1 ⟶ cf2df.. x0 x1 ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ⊆ setminus x0 (Sing x2) ⟶ ∀ x4 . x4 ∈ x3 ⟶ ∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ e8ae3.. x1 x4 x5 x6 x7 x8 x9 x10 ⟶ 2426f.. x0 x1
Param 468d8.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ο
Known 7e21c.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ 4402e.. x0 x1 ⟶ cf2df.. x0 x1 ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ⊆ setminus x0 (Sing x2) ⟶ ∀ x4 . x4 ∈ x3 ⟶ ∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ 468d8.. x1 x4 x5 x6 x7 x8 x9 x10 ⟶ 2426f.. x0 x1
Param 58615.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ο
Known dd300.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ 4402e.. x0 x1 ⟶ cf2df.. x0 x1 ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ⊆ setminus x0 (Sing x2) ⟶ ∀ x4 . x4 ∈ x3 ⟶ ∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ 58615.. x1 x4 x5 x6 x7 x8 x9 x10 ⟶ 2426f.. x0 x1
Param ae7a6.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ο
Known 3576d.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ 4402e.. x0 x1 ⟶ cf2df.. x0 x1 ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ⊆ setminus x0 (Sing x2) ⟶ ∀ x4 . x4 ∈ x3 ⟶ ∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ae7a6.. x1 x4 x5 x6 x7 x8 x9 x10 ⟶ 2426f.. x0 x1
Param 185eb.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ο
Known afa84.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ 4402e.. x0 x1 ⟶ cf2df.. x0 x1 ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ⊆ setminus x0 (Sing x2) ⟶ ∀ x4 . x4 ∈ x3 ⟶ ∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ 185eb.. x1 x4 x5 x6 x7 x8 x9 x10 ⟶ 2426f.. x0 x1
Param 18ba2.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ο
Known 3a23f.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ 4402e.. x0 x1 ⟶ cf2df.. x0 x1 ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ⊆ setminus x0 (Sing x2) ⟶ ∀ x4 . x4 ∈ x3 ⟶ ∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ 18ba2.. x1 x4 x5 x6 x7 x8 x9 x10 ⟶ 2426f.. x0 x1
Param 8b2a4.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ο
Known ff9a0.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ 4402e.. x0 x1 ⟶ cf2df.. x0 x1 ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ⊆ setminus x0 (Sing x2) ⟶ ∀ x4 . x4 ∈ x3 ⟶ ∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ 8b2a4.. x1 x4 x5 x6 x7 x8 x9 x10 ⟶ 2426f.. x0 x1
Param 13b0f.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ο
Known a9c4f.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ 4402e.. x0 x1 ⟶ cf2df.. x0 x1 ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ⊆ setminus x0 (Sing x2) ⟶ ∀ x4 . x4 ∈ x3 ⟶ ∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ 13b0f.. x1 x4 x5 x6 x7 x8 x9 x10 ⟶ 2426f.. x0 x1
Param c8dd3.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ο
Known 1bb98.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ 4402e.. x0 x1 ⟶ cf2df.. x0 x1 ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ⊆ setminus x0 (Sing x2) ⟶ ∀ x4 . x4 ∈ x3 ⟶ ∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ c8dd3.. x1 x4 x5 x6 x7 x8 x9 x10 ⟶ 2426f.. x0 x1
Param 2bd79.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ο
Known f1900.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ 4402e.. x0 x1 ⟶ cf2df.. x0 x1 ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ⊆ setminus x0 (Sing x2) ⟶ ∀ x4 . x4 ∈ x3 ⟶ ∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ 2bd79.. x1 x4 x5 x6 x7 x8 x9 x10 ⟶ 2426f.. x0 x1
Param 2fb86.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ο
Known cf6ac.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ 4402e.. x0 x1 ⟶ cf2df.. x0 x1 ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ⊆ setminus x0 (Sing x2) ⟶ ∀ x4 . x4 ∈ x3 ⟶ ∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ 2fb86.. x1 x4 x5 x6 x7 x8 x9 x10 ⟶ 2426f.. x0 x1
Param 81638.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ο
Known b32f6.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ 4402e.. x0 x1 ⟶ cf2df.. x0 x1 ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ⊆ setminus x0 (Sing x2) ⟶ ∀ x4 . x4 ∈ x3 ⟶ ∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ 81638.. x1 x4 x5 x6 x7 x8 x9 x10 ⟶ 2426f.. x0 x1
Param 70d65.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ο
Known 94959.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ 4402e.. x0 x1 ⟶ cf2df.. x0 x1 ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ⊆ setminus x0 (Sing x2) ⟶ ∀ x4 . x4 ∈ x3 ⟶ ∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ 70d65.. x1 x4 x5 x6 x7 x8 x9 x10 ⟶ 2426f.. x0 x1
Param 843b8.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ο
Known 22ac1.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ 4402e.. x0 x1 ⟶ cf2df.. x0 x1 ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ⊆ setminus x0 (Sing x2) ⟶ ∀ x4 . x4 ∈ x3 ⟶ ∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ 843b8.. x1 x4 x5 x6 x7 x8 x9 x10 ⟶ 2426f.. x0 x1
Param de02c.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ο
Known 91d4c.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ 4402e.. x0 x1 ⟶ cf2df.. x0 x1 ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ⊆ setminus x0 (Sing x2) ⟶ ∀ x4 . x4 ∈ x3 ⟶ ∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ de02c.. x1 x4 x5 x6 x7 x8 x9 x10 ⟶ 2426f.. x0 x1
Param 80533.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ο
Known 45cda.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ 4402e.. x0 x1 ⟶ cf2df.. x0 x1 ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ⊆ setminus x0 (Sing x2) ⟶ ∀ x4 . x4 ∈ x3 ⟶ ∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ 80533.. x1 x4 x5 x6 x7 x8 x9 x10 ⟶ 2426f.. x0 x1
Param 2452c.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ο
Known 6b7c1.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ 4402e.. x0 x1 ⟶ cf2df.. x0 x1 ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ⊆ setminus x0 (Sing x2) ⟶ ∀ x4 . x4 ∈ x3 ⟶ ∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ 2452c.. x1 x4 x5 x6 x7 x8 x9 x10 ⟶ 2426f.. x0 x1
Param 7c934.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ο
Known 7e550.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ 4402e.. x0 x1 ⟶ cf2df.. x0 x1 ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ⊆ setminus x0 (Sing x2) ⟶ ∀ x4 . x4 ∈ x3 ⟶ ∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ 7c934.. x1 x4 x5 x6 x7 x8 x9 x10 ⟶ 2426f.. x0 x1
Param b0193.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ο
Known 16283.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ 4402e.. x0 x1 ⟶ cf2df.. x0 x1 ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ⊆ setminus x0 (Sing x2) ⟶ ∀ x4 . x4 ∈ x3 ⟶ ∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ b0193.. x1 x4 x5 x6 x7 x8 x9 x10 ⟶ 2426f.. x0 x1
Param 2c4f5.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ο
Known face1.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ 4402e.. x0 x1 ⟶ cf2df.. x0 x1 ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ⊆ setminus x0 (Sing x2) ⟶ ∀ x4 . x4 ∈ x3 ⟶ ∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ 2c4f5.. x1 x4 x5 x6 x7 x8 x9 x10 ⟶ 2426f.. x0 x1
Param a643d.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ο
Known 90f58.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ 4402e.. x0 x1 ⟶ cf2df.. x0 x1 ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ⊆ setminus x0 (Sing x2) ⟶ ∀ x4 . x4 ∈ x3 ⟶ ∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ a643d.. x1 x4 x5 x6 x7 x8 x9 x10 ⟶ 2426f.. x0 x1
Param 59105.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ο
Known 65695.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ 4402e.. x0 x1 ⟶ cf2df.. x0 x1 ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ⊆ setminus x0 (Sing x2) ⟶ ∀ x4 . x4 ∈ x3 ⟶ ∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ 59105.. x1 x4 x5 x6 x7 x8 x9 x10 ⟶ 2426f.. x0 x1
Param 1d4b1.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ο
Known d577e.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ 4402e.. x0 x1 ⟶ cf2df.. x0 x1 ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ⊆ setminus x0 (Sing x2) ⟶ ∀ x4 . x4 ∈ x3 ⟶ ∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ 1d4b1.. x1 x4 x5 x6 x7 x8 x9 x10 ⟶ 2426f.. x0 x1
Param bd1a2.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ο
Known 511b2.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ 4402e.. x0 x1 ⟶ cf2df.. x0 x1 ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ⊆ setminus x0 (Sing x2) ⟶ ∀ x4 . x4 ∈ x3 ⟶ ∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ bd1a2.. x1 x4 x5 x6 x7 x8 x9 x10 ⟶ 2426f.. x0 x1
Param 99e5f.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ο
Known 0f0d9.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ 4402e.. x0 x1 ⟶ cf2df.. x0 x1 ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ⊆ setminus x0 (Sing x2) ⟶ ∀ x4 . x4 ∈ x3 ⟶ ∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ 99e5f.. x1 x4 x5 x6 x7 x8 x9 x10 ⟶ 2426f.. x0 x1
Param 7c036.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ο
Known 7e72e.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ 4402e.. x0 x1 ⟶ cf2df.. x0 x1 ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ⊆ setminus x0 (Sing x2) ⟶ ∀ x4 . x4 ∈ x3 ⟶ ∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ 7c036.. x1 x4 x5 x6 x7 x8 x9 x10 ⟶ 2426f.. x0 x1
Param a5b26.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ο
Known 23d5e.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ 4402e.. x0 x1 ⟶ cf2df.. x0 x1 ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ⊆ setminus x0 (Sing x2) ⟶ ∀ x4 . x4 ∈ x3 ⟶ ∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ a5b26.. x1 x4 x5 x6 x7 x8 x9 x10 ⟶ 2426f.. x0 x1
Param 27260.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ο
Known 4ca7b.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ 4402e.. x0 x1 ⟶ cf2df.. x0 x1 ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ⊆ setminus x0 (Sing x2) ⟶ ∀ x4 . x4 ∈ x3 ⟶ ∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ 27260.. x1 x4 x5 x6 x7 x8 x9 x10 ⟶ 2426f.. x0 x1
Param ba9c9.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ο
Known c37d7.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ 4402e.. x0 x1 ⟶ cf2df.. x0 x1 ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ⊆ setminus x0 (Sing x2) ⟶ ∀ x4 . x4 ∈ x3 ⟶ ∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ ba9c9.. x1 x4 x5 x6 x7 x8 x9 x10 ⟶ 2426f.. x0 x1
Param 13471.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ο
Known 05bb1.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ 4402e.. x0 x1 ⟶ cf2df.. x0 x1 ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ⊆ setminus x0 (Sing x2) ⟶ ∀ x4 . x4 ∈ x3 ⟶ ∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ 13471.. x1 x4 x5 x6 x7 x8 x9 x10 ⟶ 2426f.. x0 x1
Param 28e61.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ο
Known 82265.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ 4402e.. x0 x1 ⟶ cf2df.. x0 x1 ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ⊆ setminus x0 (Sing x2) ⟶ ∀ x4 . x4 ∈ x3 ⟶ ∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ 28e61.. x1 x4 x5 x6 x7 x8 x9 x10 ⟶ 2426f.. x0 x1
Param df271.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ο
Known 7975f.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ 4402e.. x0 x1 ⟶ cf2df.. x0 x1 ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ⊆ setminus x0 (Sing x2) ⟶ ∀ x4 . x4 ∈ x3 ⟶ ∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ df271.. x1 x4 x5 x6 x7 x8 x9 x10 ⟶ 2426f.. x0 x1
Param 7f522.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ο
Known f0e9b.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ 4402e.. x0 x1 ⟶ cf2df.. x0 x1 ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ⊆ setminus x0 (Sing x2) ⟶ ∀ x4 . x4 ∈ x3 ⟶ ∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ 7f522.. x1 x4 x5 x6 x7 x8 x9 x10 ⟶ 2426f.. x0 x1
Param d8477.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ο
Known 85d1f.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ 4402e.. x0 x1 ⟶ cf2df.. x0 x1 ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ⊆ setminus x0 (Sing x2) ⟶ ∀ x4 . x4 ∈ x3 ⟶ ∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ d8477.. x1 x4 x5 x6 x7 x8 x9 x10 ⟶ 2426f.. x0 x1
Param 04ac1.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ο
Known 7a316.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ 4402e.. x0 x1 ⟶ cf2df.. x0 x1 ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ⊆ setminus x0 (Sing x2) ⟶ ∀ x4 . x4 ∈ x3 ⟶ ∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ 04ac1.. x1 x4 x5 x6 x7 x8 x9 x10 ⟶ 2426f.. x0 x1
Param 21422.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ο
Known ccf11.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ 4402e.. x0 x1 ⟶ cf2df.. x0 x1 ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ⊆ setminus x0 (Sing x2) ⟶ ∀ x4 . x4 ∈ x3 ⟶ ∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ 21422.. x1 x4 x5 x6 x7 x8 x9 x10 ⟶ 2426f.. x0 x1
Param 948b9.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ο
Known 09738.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ 4402e.. x0 x1 ⟶ cf2df.. x0 x1 ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ⊆ setminus x0 (Sing x2) ⟶ ∀ x4 . x4 ∈ x3 ⟶ ∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ 948b9.. x1 x4 x5 x6 x7 x8 x9 x10 ⟶ 2426f.. x0 x1
Param 09fea.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ο
Known 0ccd5.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ 4402e.. x0 x1 ⟶ cf2df.. x0 x1 ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ⊆ setminus x0 (Sing x2) ⟶ ∀ x4 . x4 ∈ x3 ⟶ ∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ 09fea.. x1 x4 x5 x6 x7 x8 x9 x10 ⟶ 2426f.. x0 x1
Param f68ad.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ο
Known f4d86.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ 4402e.. x0 x1 ⟶ cf2df.. x0 x1 ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ⊆ setminus x0 (Sing x2) ⟶ ∀ x4 . x4 ∈ x3 ⟶ ∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ f68ad.. x1 x4 x5 x6 x7 x8 x9 x10 ⟶ 2426f.. x0 x1
Param a53de.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ο
Known 3f704.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ 4402e.. x0 x1 ⟶ cf2df.. x0 x1 ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ⊆ setminus x0 (Sing x2) ⟶ ∀ x4 . x4 ∈ x3 ⟶ ∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ a53de.. x1 x4 x5 x6 x7 x8 x9 x10 ⟶ 2426f.. x0 x1
Param f9bfa.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ο
Known 7745f.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ 4402e.. x0 x1 ⟶ cf2df.. x0 x1 ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ⊆ setminus x0 (Sing x2) ⟶ ∀ x4 . x4 ∈ x3 ⟶ ∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ f9bfa.. x1 x4 x5 x6 x7 x8 x9 x10 ⟶ 2426f.. x0 x1
Param 9733c.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ο
Known 152ec.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ 4402e.. x0 x1 ⟶ cf2df.. x0 x1 ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ⊆ setminus x0 (Sing x2) ⟶ ∀ x4 . x4 ∈ x3 ⟶ ∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ 9733c.. x1 x4 x5 x6 x7 x8 x9 x10 ⟶ 2426f.. x0 x1
Param b3861.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ο
Known 4e529.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ 4402e.. x0 x1 ⟶ cf2df.. x0 x1 ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ⊆ setminus x0 (Sing x2) ⟶ ∀ x4 . x4 ∈ x3 ⟶ ∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ b3861.. x1 x4 x5 x6 x7 x8 x9 x10 ⟶ 2426f.. x0 x1
Param 836ee.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ο
Known b1728.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ 4402e.. x0 x1 ⟶ cf2df.. x0 x1 ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ⊆ setminus x0 (Sing x2) ⟶ ∀ x4 . x4 ∈ x3 ⟶ ∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ 836ee.. x1 x4 x5 x6 x7 x8 x9 x10 ⟶ 2426f.. x0 x1
Param 1c500.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ο
Known 2342d.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ 4402e.. x0 x1 ⟶ cf2df.. x0 x1 ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ⊆ setminus x0 (Sing x2) ⟶ ∀ x4 . x4 ∈ x3 ⟶ ∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ 1c500.. x1 x4 x5 x6 x7 x8 x9 x10 ⟶ 2426f.. x0 x1
Param bb926.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ο
Known 4355c.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ 4402e.. x0 x1 ⟶ cf2df.. x0 x1 ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ⊆ setminus x0 (Sing x2) ⟶ ∀ x4 . x4 ∈ x3 ⟶ ∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ bb926.. x1 x4 x5 x6 x7 x8 x9 x10 ⟶ 2426f.. x0 x1
Param b9d10.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ο
Known 9dbdc.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ 4402e.. x0 x1 ⟶ cf2df.. x0 x1 ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ⊆ setminus x0 (Sing x2) ⟶ ∀ x4 . x4 ∈ x3 ⟶ ∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ b9d10.. x1 x4 x5 x6 x7 x8 x9 x10 ⟶ 2426f.. x0 x1
Param atleastp^atleastp : ι → ι → ο
Param ordsucc^ordsucc : ι → ι
Param u7 : ι
Definition u8 := ordsucc u7
Definition and^and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Known e2ea8.. : ∀ x0 x1 . atleastp (ordsucc x0) x1 ⟶ ∀ x2 : ο . (∀ x3 . and (x3 ∈ x1) (atleastp x0 (setminus x1 (Sing x3))) ⟶ x2) ⟶ x2
Definition 0c39d.. := λ x0 . λ x1 : ι → ι → ο . ∀ x2 : ο . (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ 7f677.. x1 x3 x4 x5 x6 x7 x8 x9 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ 58366.. x1 x3 x4 x5 x6 x7 x8 x9 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ c9184.. x1 x3 x4 x5 x6 x7 x8 x9 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ e7595.. x1 x3 x4 x5 x6 x7 x8 x9 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ 8c395.. x1 x3 x4 x5 x6 x7 x8 x9 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ 88b7c.. x1 x3 x4 x5 x6 x7 x8 x9 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ae506.. x1 x3 x4 x5 x6 x7 x8 x9 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ 98053.. x1 x3 x4 x5 x6 x7 x8 x9 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ 5db61.. x1 x3 x4 x5 x6 x7 x8 x9 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ 182cc.. x1 x3 x4 x5 x6 x7 x8 x9 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ 796c4.. x1 x3 x4 x5 x6 x7 x8 x9 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ 084ea.. x1 x3 x4 x5 x6 x7 x8 x9 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ 3819d.. x1 x3 x4 x5 x6 x7 x8 x9 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ 6ca1f.. x1 x3 x4 x5 x6 x7 x8 x9 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ 99de9.. x1 x3 x4 x5 x6 x7 x8 x9 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ cb525.. x1 x3 x4 x5 x6 x7 x8 x9 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ 3109c.. x1 x3 x4 x5 x6 x7 x8 x9 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ 2319a.. x1 x3 x4 x5 x6 x7 x8 x9 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ 323f1.. x1 x3 x4 x5 x6 x7 x8 x9 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ 16c0f.. x1 x3 x4 x5 x6 x7 x8 x9 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ 36d58.. x1 x3 x4 x5 x6 x7 x8 x9 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ 28e31.. x1 x3 x4 x5 x6 x7 x8 x9 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ 02f3e.. x1 x3 x4 x5 x6 x7 x8 x9 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ 28532.. x1 x3 x4 x5 x6 x7 x8 x9 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ e8ae3.. x1 x3 x4 x5 x6 x7 x8 x9 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ 468d8.. x1 x3 x4 x5 x6 x7 x8 x9 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ 58615.. x1 x3 x4 x5 x6 x7 x8 x9 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ae7a6.. x1 x3 x4 x5 x6 x7 x8 x9 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ 185eb.. x1 x3 x4 x5 x6 x7 x8 x9 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ 18ba2.. x1 x3 x4 x5 x6 x7 x8 x9 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ 8b2a4.. x1 x3 x4 x5 x6 x7 x8 x9 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ 13b0f.. x1 x3 x4 x5 x6 x7 x8 x9 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ c8dd3.. x1 x3 x4 x5 x6 x7 x8 x9 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ 2bd79.. x1 x3 x4 x5 x6 x7 x8 x9 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ 2fb86.. x1 x3 x4 x5 x6 x7 x8 x9 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ 81638.. x1 x3 x4 x5 x6 x7 x8 x9 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ 70d65.. x1 x3 x4 x5 x6 x7 x8 x9 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ 843b8.. x1 x3 x4 x5 x6 x7 x8 x9 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ de02c.. x1 x3 x4 x5 x6 x7 x8 x9 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ 80533.. x1 x3 x4 x5 x6 x7 x8 x9 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ 2452c.. x1 x3 x4 x5 x6 x7 x8 x9 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ 7c934.. x1 x3 x4 x5 x6 x7 x8 x9 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ b0193.. x1 x3 x4 x5 x6 x7 x8 x9 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ 2c4f5.. x1 x3 x4 x5 x6 x7 x8 x9 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ a643d.. x1 x3 x4 x5 x6 x7 x8 x9 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ 59105.. x1 x3 x4 x5 x6 x7 x8 x9 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ 1d4b1.. x1 x3 x4 x5 x6 x7 x8 x9 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ bd1a2.. x1 x3 x4 x5 x6 x7 x8 x9 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ 99e5f.. x1 x3 x4 x5 x6 x7 x8 x9 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ 7c036.. x1 x3 x4 x5 x6 x7 x8 x9 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ a5b26.. x1 x3 x4 x5 x6 x7 x8 x9 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ 27260.. x1 x3 x4 x5 x6 x7 x8 x9 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ba9c9.. x1 x3 x4 x5 x6 x7 x8 x9 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ 13471.. x1 x3 x4 x5 x6 x7 x8 x9 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ 28e61.. x1 x3 x4 x5 x6 x7 x8 x9 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ df271.. x1 x3 x4 x5 x6 x7 x8 x9 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ 7f522.. x1 x3 x4 x5 x6 x7 x8 x9 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ d8477.. x1 x3 x4 x5 x6 x7 x8 x9 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ 04ac1.. x1 x3 x4 x5 x6 x7 x8 x9 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ 21422.. x1 x3 x4 x5 x6 x7 x8 x9 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ 948b9.. x1 x3 x4 x5 x6 x7 x8 x9 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ 09fea.. x1 x3 x4 x5 x6 x7 x8 x9 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ f68ad.. x1 x3 x4 x5 x6 x7 x8 x9 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ a53de.. x1 x3 x4 x5 x6 x7 x8 x9 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ f9bfa.. x1 x3 x4 x5 x6 x7 x8 x9 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ 9733c.. x1 x3 x4 x5 x6 x7 x8 x9 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ b3861.. x1 x3 x4 x5 x6 x7 x8 x9 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ 836ee.. x1 x3 x4 x5 x6 x7 x8 x9 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ 1c500.. x1 x3 x4 x5 x6 x7 x8 x9 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ bb926.. x1 x3 x4 x5 x6 x7 x8 x9 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ b9d10.. x1 x3 x4 x5 x6 x7 x8 x9 ⟶ x2) ⟶ x2
Known a8fb8.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ atleastp u7 x0 ⟶ 4402e.. x0 x1 ⟶ cf2df.. x0 x1 ⟶ 0c39d.. x0 x1
Known setminus_Subq^{setminus_Subq} : ∀ x0 x1 . setminus x0 x1 ⊆ x0
Known Subq_ref^Subq_ref : ∀ x0 . x0 ⊆ x0
Known e7c7c.. : ∀ x0 x1 . ∀ x2 : ι → ι → ο . x0 ⊆ x1 ⟶ cf2df.. x1 x2 ⟶ cf2df.. x0 x2
Known a55d1.. : ∀ x0 x1 . ∀ x2 : ι → ι → ο . x0 ⊆ x1 ⟶ 4402e.. x1 x2 ⟶ 4402e.. x0 x2
Known setminusE1^setminusE1 : ∀ x0 x1 x2 . x2 ∈ setminus x0 x1 ⟶ x2 ∈ x0
Theorem dfeca.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ atleastp u8 x0 ⟶ 4402e.. x0 x1 ⟶ cf2df.. x0 x1 ⟶ 2426f.. x0 x1 (proof)