Proofgold Asset

Param SNo^SNo : ι → ο
Param 1eb0a.. : ι → ο
Param bbc71.. : ι → ι → ι → ι → ι → ι → ι → ι → ι
Known d5242.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ SNo x5 ⟶ SNo x6 ⟶ SNo x7 ⟶ 1eb0a.. (bbc71.. x0 x1 x2 x3 x4 x5 x6 x7)
Param 8dd2c.. : ι → ι
Definition and^and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Known 340c0.. : ∀ x0 . 1eb0a.. x0 ⟶ and (SNo (8dd2c.. x0)) (∀ x1 : ο . (∀ x2 . and (SNo x2) (∀ x3 : ο . (∀ x4 . and (SNo x4) (∀ x5 : ο . (∀ x6 . and (SNo x6) (∀ x7 : ο . (∀ x8 . and (SNo x8) (∀ x9 : ο . (∀ x10 . and (SNo x10) (∀ x11 : ο . (∀ x12 . and (SNo x12) (∀ x13 : ο . (∀ x14 . and (SNo x14) (x0 = bbc71.. (8dd2c.. x0) x2 x4 x6 x8 x10 x12 x14) ⟶ x13) ⟶ x13) ⟶ x11) ⟶ x11) ⟶ x9) ⟶ x9) ⟶ x7) ⟶ x7) ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3) ⟶ x1) ⟶ x1)
Known 95571.. : ∀ x0 . 1eb0a.. x0 ⟶ SNo (8dd2c.. x0)
Known 212d5.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ SNo x5 ⟶ SNo x6 ⟶ SNo x7 ⟶ 8dd2c.. (bbc71.. x0 x1 x2 x3 x4 x5 x6 x7) = x0
Param d4639.. : (ι → ι) → ι → ι
Known 26f49.. : ∀ x0 : ι → ι . (∀ x1 . 1eb0a.. x1 ⟶ and (SNo (x0 x1)) (∀ x2 : ο . (∀ x3 . and (SNo x3) (∀ x4 : ο . (∀ x5 . and (SNo x5) (∀ x6 : ο . (∀ x7 . and (SNo x7) (∀ x8 : ο . (∀ x9 . and (SNo x9) (∀ x10 : ο . (∀ x11 . and (SNo x11) (∀ x12 : ο . (∀ x13 . and (SNo x13) (∀ x14 : ο . (∀ x15 . and (SNo x15) (x1 = bbc71.. (x0 x1) x3 x5 x7 x9 x11 x13 x15) ⟶ x14) ⟶ x14) ⟶ x12) ⟶ x12) ⟶ x10) ⟶ x10) ⟶ x8) ⟶ x8) ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2)) ⟶ ∀ x1 . 1eb0a.. x1 ⟶ and (SNo (d4639.. x0 x1)) (∀ x2 : ο . (∀ x3 . and (SNo x3) (∀ x4 : ο . (∀ x5 . and (SNo x5) (∀ x6 : ο . (∀ x7 . and (SNo x7) (∀ x8 : ο . (∀ x9 . and (SNo x9) (∀ x10 : ο . (∀ x11 . and (SNo x11) (∀ x12 : ο . (∀ x13 . and (SNo x13) (x1 = bbc71.. (x0 x1) (d4639.. x0 x1) x3 x5 x7 x9 x11 x13) ⟶ x12) ⟶ x12) ⟶ x10) ⟶ x10) ⟶ x8) ⟶ x8) ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2)
Known fd099.. : ∀ x0 : ι → ι . (∀ x1 . 1eb0a.. x1 ⟶ and (SNo (x0 x1)) (∀ x2 : ο . (∀ x3 . and (SNo x3) (∀ x4 : ο . (∀ x5 . and (SNo x5) (∀ x6 : ο . (∀ x7 . and (SNo x7) (∀ x8 : ο . (∀ x9 . and (SNo x9) (∀ x10 : ο . (∀ x11 . and (SNo x11) (∀ x12 : ο . (∀ x13 . and (SNo x13) (∀ x14 : ο . (∀ x15 . and (SNo x15) (x1 = bbc71.. (x0 x1) x3 x5 x7 x9 x11 x13 x15) ⟶ x14) ⟶ x14) ⟶ x12) ⟶ x12) ⟶ x10) ⟶ x10) ⟶ x8) ⟶ x8) ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2)) ⟶ ∀ x1 . 1eb0a.. x1 ⟶ SNo (d4639.. x0 x1)
Known 33b4a.. : ∀ x0 : ι → ι . (∀ x1 . 1eb0a.. x1 ⟶ and (SNo (x0 x1)) (∀ x2 : ο . (∀ x3 . and (SNo x3) (∀ x4 : ο . (∀ x5 . and (SNo x5) (∀ x6 : ο . (∀ x7 . and (SNo x7) (∀ x8 : ο . (∀ x9 . and (SNo x9) (∀ x10 : ο . (∀ x11 . and (SNo x11) (∀ x12 : ο . (∀ x13 . and (SNo x13) (∀ x14 : ο . (∀ x15 . and (SNo x15) (x1 = bbc71.. (x0 x1) x3 x5 x7 x9 x11 x13 x15) ⟶ x14) ⟶ x14) ⟶ x12) ⟶ x12) ⟶ x10) ⟶ x10) ⟶ x8) ⟶ x8) ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2)) ⟶ (∀ x1 . 1eb0a.. x1 ⟶ SNo (x0 x1)) ⟶ ∀ x1 x2 x3 x4 x5 x6 x7 x8 . SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ SNo x5 ⟶ SNo x6 ⟶ SNo x7 ⟶ SNo x8 ⟶ d4639.. x0 (bbc71.. x1 x2 x3 x4 x5 x6 x7 x8) = x2
Param 50208.. : (ι → ι) → (ι → ι) → ι → ι
Known 9b0e1.. : ∀ x0 : ι → ι . (∀ x1 . 1eb0a.. x1 ⟶ and (SNo (x0 x1)) (∀ x2 : ο . (∀ x3 . and (SNo x3) (∀ x4 : ο . (∀ x5 . and (SNo x5) (∀ x6 : ο . (∀ x7 . and (SNo x7) (∀ x8 : ο . (∀ x9 . and (SNo x9) (∀ x10 : ο . (∀ x11 . and (SNo x11) (∀ x12 : ο . (∀ x13 . and (SNo x13) (∀ x14 : ο . (∀ x15 . and (SNo x15) (x1 = bbc71.. (x0 x1) x3 x5 x7 x9 x11 x13 x15) ⟶ x14) ⟶ x14) ⟶ x12) ⟶ x12) ⟶ x10) ⟶ x10) ⟶ x8) ⟶ x8) ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2)) ⟶ (∀ x1 . 1eb0a.. x1 ⟶ SNo (x0 x1)) ⟶ ∀ x1 : ι → ι . (∀ x2 . 1eb0a.. x2 ⟶ and (SNo (x1 x2)) (∀ x3 : ο . (∀ x4 . and (SNo x4) (∀ x5 : ο . (∀ x6 . and (SNo x6) (∀ x7 : ο . (∀ x8 . and (SNo x8) (∀ x9 : ο . (∀ x10 . and (SNo x10) (∀ x11 : ο . (∀ x12 . and (SNo x12) (∀ x13 : ο . (∀ x14 . and (SNo x14) (x2 = bbc71.. (x0 x2) (x1 x2) x4 x6 x8 x10 x12 x14) ⟶ x13) ⟶ x13) ⟶ x11) ⟶ x11) ⟶ x9) ⟶ x9) ⟶ x7) ⟶ x7) ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3)) ⟶ ∀ x2 . 1eb0a.. x2 ⟶ and (SNo (50208.. x0 x1 x2)) (∀ x3 : ο . (∀ x4 . and (SNo x4) (∀ x5 : ο . (∀ x6 . and (SNo x6) (∀ x7 : ο . (∀ x8 . and (SNo x8) (∀ x9 : ο . (∀ x10 . and (SNo x10) (∀ x11 : ο . (∀ x12 . and (SNo x12) (x2 = bbc71.. (x0 x2) (x1 x2) (50208.. x0 x1 x2) x4 x6 x8 x10 x12) ⟶ x11) ⟶ x11) ⟶ x9) ⟶ x9) ⟶ x7) ⟶ x7) ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3)
Known 1131a.. : ∀ x0 : ι → ι . (∀ x1 . 1eb0a.. x1 ⟶ and (SNo (x0 x1)) (∀ x2 : ο . (∀ x3 . and (SNo x3) (∀ x4 : ο . (∀ x5 . and (SNo x5) (∀ x6 : ο . (∀ x7 . and (SNo x7) (∀ x8 : ο . (∀ x9 . and (SNo x9) (∀ x10 : ο . (∀ x11 . and (SNo x11) (∀ x12 : ο . (∀ x13 . and (SNo x13) (∀ x14 : ο . (∀ x15 . and (SNo x15) (x1 = bbc71.. (x0 x1) x3 x5 x7 x9 x11 x13 x15) ⟶ x14) ⟶ x14) ⟶ x12) ⟶ x12) ⟶ x10) ⟶ x10) ⟶ x8) ⟶ x8) ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2)) ⟶ (∀ x1 . 1eb0a.. x1 ⟶ SNo (x0 x1)) ⟶ ∀ x1 : ι → ι . (∀ x2 . 1eb0a.. x2 ⟶ and (SNo (x1 x2)) (∀ x3 : ο . (∀ x4 . and (SNo x4) (∀ x5 : ο . (∀ x6 . and (SNo x6) (∀ x7 : ο . (∀ x8 . and (SNo x8) (∀ x9 : ο . (∀ x10 . and (SNo x10) (∀ x11 : ο . (∀ x12 . and (SNo x12) (∀ x13 : ο . (∀ x14 . and (SNo x14) (x2 = bbc71.. (x0 x2) (x1 x2) x4 x6 x8 x10 x12 x14) ⟶ x13) ⟶ x13) ⟶ x11) ⟶ x11) ⟶ x9) ⟶ x9) ⟶ x7) ⟶ x7) ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3)) ⟶ ∀ x2 . 1eb0a.. x2 ⟶ SNo (50208.. x0 x1 x2)
Known 90339.. : ∀ x0 : ι → ι . (∀ x1 . 1eb0a.. x1 ⟶ and (SNo (x0 x1)) (∀ x2 : ο . (∀ x3 . and (SNo x3) (∀ x4 : ο . (∀ x5 . and (SNo x5) (∀ x6 : ο . (∀ x7 . and (SNo x7) (∀ x8 : ο . (∀ x9 . and (SNo x9) (∀ x10 : ο . (∀ x11 . and (SNo x11) (∀ x12 : ο . (∀ x13 . and (SNo x13) (∀ x14 : ο . (∀ x15 . and (SNo x15) (x1 = bbc71.. (x0 x1) x3 x5 x7 x9 x11 x13 x15) ⟶ x14) ⟶ x14) ⟶ x12) ⟶ x12) ⟶ x10) ⟶ x10) ⟶ x8) ⟶ x8) ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2)) ⟶ (∀ x1 . 1eb0a.. x1 ⟶ SNo (x0 x1)) ⟶ ∀ x1 : ι → ι . (∀ x2 . 1eb0a.. x2 ⟶ and (SNo (x1 x2)) (∀ x3 : ο . (∀ x4 . and (SNo x4) (∀ x5 : ο . (∀ x6 . and (SNo x6) (∀ x7 : ο . (∀ x8 . and (SNo x8) (∀ x9 : ο . (∀ x10 . and (SNo x10) (∀ x11 : ο . (∀ x12 . and (SNo x12) (∀ x13 : ο . (∀ x14 . and (SNo x14) (x2 = bbc71.. (x0 x2) (x1 x2) x4 x6 x8 x10 x12 x14) ⟶ x13) ⟶ x13) ⟶ x11) ⟶ x11) ⟶ x9) ⟶ x9) ⟶ x7) ⟶ x7) ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3)) ⟶ (∀ x2 . 1eb0a.. x2 ⟶ SNo (x1 x2)) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 . SNo x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ SNo x5 ⟶ SNo x6 ⟶ SNo x7 ⟶ SNo x8 ⟶ SNo x9 ⟶ 50208.. x0 x1 (bbc71.. x2 x3 x4 x5 x6 x7 x8 x9) = x4
Param 8d7df.. : (ι → ι) → (ι → ι) → (ι → ι) → ι → ι
Known 0a376.. : ∀ x0 : ι → ι . (∀ x1 . 1eb0a.. x1 ⟶ and (SNo (x0 x1)) (∀ x2 : ο . (∀ x3 . and (SNo x3) (∀ x4 : ο . (∀ x5 . and (SNo x5) (∀ x6 : ο . (∀ x7 . and (SNo x7) (∀ x8 : ο . (∀ x9 . and (SNo x9) (∀ x10 : ο . (∀ x11 . and (SNo x11) (∀ x12 : ο . (∀ x13 . and (SNo x13) (∀ x14 : ο . (∀ x15 . and (SNo x15) (x1 = bbc71.. (x0 x1) x3 x5 x7 x9 x11 x13 x15) ⟶ x14) ⟶ x14) ⟶ x12) ⟶ x12) ⟶ x10) ⟶ x10) ⟶ x8) ⟶ x8) ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2)) ⟶ (∀ x1 . 1eb0a.. x1 ⟶ SNo (x0 x1)) ⟶ ∀ x1 : ι → ι . (∀ x2 . 1eb0a.. x2 ⟶ and (SNo (x1 x2)) (∀ x3 : ο . (∀ x4 . and (SNo x4) (∀ x5 : ο . (∀ x6 . and (SNo x6) (∀ x7 : ο . (∀ x8 . and (SNo x8) (∀ x9 : ο . (∀ x10 . and (SNo x10) (∀ x11 : ο . (∀ x12 . and (SNo x12) (∀ x13 : ο . (∀ x14 . and (SNo x14) (x2 = bbc71.. (x0 x2) (x1 x2) x4 x6 x8 x10 x12 x14) ⟶ x13) ⟶ x13) ⟶ x11) ⟶ x11) ⟶ x9) ⟶ x9) ⟶ x7) ⟶ x7) ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3)) ⟶ (∀ x2 . 1eb0a.. x2 ⟶ SNo (x1 x2)) ⟶ ∀ x2 : ι → ι . (∀ x3 . 1eb0a.. x3 ⟶ and (SNo (x2 x3)) (∀ x4 : ο . (∀ x5 . and (SNo x5) (∀ x6 : ο . (∀ x7 . and (SNo x7) (∀ x8 : ο . (∀ x9 . and (SNo x9) (∀ x10 : ο . (∀ x11 . and (SNo x11) (∀ x12 : ο . (∀ x13 . and (SNo x13) (x3 = bbc71.. (x0 x3) (x1 x3) (x2 x3) x5 x7 x9 x11 x13) ⟶ x12) ⟶ x12) ⟶ x10) ⟶ x10) ⟶ x8) ⟶ x8) ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4)) ⟶ ∀ x3 . 1eb0a.. x3 ⟶ and (SNo (8d7df.. x0 x1 x2 x3)) (∀ x4 : ο . (∀ x5 . and (SNo x5) (∀ x6 : ο . (∀ x7 . and (SNo x7) (∀ x8 : ο . (∀ x9 . and (SNo x9) (∀ x10 : ο . (∀ x11 . and (SNo x11) (x3 = bbc71.. (x0 x3) (x1 x3) (x2 x3) (8d7df.. x0 x1 x2 x3) x5 x7 x9 x11) ⟶ x10) ⟶ x10) ⟶ x8) ⟶ x8) ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4)
Known 5e734.. : ∀ x0 : ι → ι . (∀ x1 . 1eb0a.. x1 ⟶ and (SNo (x0 x1)) (∀ x2 : ο . (∀ x3 . and (SNo x3) (∀ x4 : ο . (∀ x5 . and (SNo x5) (∀ x6 : ο . (∀ x7 . and (SNo x7) (∀ x8 : ο . (∀ x9 . and (SNo x9) (∀ x10 : ο . (∀ x11 . and (SNo x11) (∀ x12 : ο . (∀ x13 . and (SNo x13) (∀ x14 : ο . (∀ x15 . and (SNo x15) (x1 = bbc71.. (x0 x1) x3 x5 x7 x9 x11 x13 x15) ⟶ x14) ⟶ x14) ⟶ x12) ⟶ x12) ⟶ x10) ⟶ x10) ⟶ x8) ⟶ x8) ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2)) ⟶ (∀ x1 . 1eb0a.. x1 ⟶ SNo (x0 x1)) ⟶ ∀ x1 : ι → ι . (∀ x2 . 1eb0a.. x2 ⟶ and (SNo (x1 x2)) (∀ x3 : ο . (∀ x4 . and (SNo x4) (∀ x5 : ο . (∀ x6 . and (SNo x6) (∀ x7 : ο . (∀ x8 . and (SNo x8) (∀ x9 : ο . (∀ x10 . and (SNo x10) (∀ x11 : ο . (∀ x12 . and (SNo x12) (∀ x13 : ο . (∀ x14 . and (SNo x14) (x2 = bbc71.. (x0 x2) (x1 x2) x4 x6 x8 x10 x12 x14) ⟶ x13) ⟶ x13) ⟶ x11) ⟶ x11) ⟶ x9) ⟶ x9) ⟶ x7) ⟶ x7) ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3)) ⟶ (∀ x2 . 1eb0a.. x2 ⟶ SNo (x1 x2)) ⟶ ∀ x2 : ι → ι . (∀ x3 . 1eb0a.. x3 ⟶ and (SNo (x2 x3)) (∀ x4 : ο . (∀ x5 . and (SNo x5) (∀ x6 : ο . (∀ x7 . and (SNo x7) (∀ x8 : ο . (∀ x9 . and (SNo x9) (∀ x10 : ο . (∀ x11 . and (SNo x11) (∀ x12 : ο . (∀ x13 . and (SNo x13) (x3 = bbc71.. (x0 x3) (x1 x3) (x2 x3) x5 x7 x9 x11 x13) ⟶ x12) ⟶ x12) ⟶ x10) ⟶ x10) ⟶ x8) ⟶ x8) ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4)) ⟶ ∀ x3 . 1eb0a.. x3 ⟶ SNo (8d7df.. x0 x1 x2 x3)
Known 71a99.. : ∀ x0 : ι → ι . (∀ x1 . 1eb0a.. x1 ⟶ and (SNo (x0 x1)) (∀ x2 : ο . (∀ x3 . and (SNo x3) (∀ x4 : ο . (∀ x5 . and (SNo x5) (∀ x6 : ο . (∀ x7 . and (SNo x7) (∀ x8 : ο . (∀ x9 . and (SNo x9) (∀ x10 : ο . (∀ x11 . and (SNo x11) (∀ x12 : ο . (∀ x13 . and (SNo x13) (∀ x14 : ο . (∀ x15 . and (SNo x15) (x1 = bbc71.. (x0 x1) x3 x5 x7 x9 x11 x13 x15) ⟶ x14) ⟶ x14) ⟶ x12) ⟶ x12) ⟶ x10) ⟶ x10) ⟶ x8) ⟶ x8) ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2)) ⟶ (∀ x1 . 1eb0a.. x1 ⟶ SNo (x0 x1)) ⟶ ∀ x1 : ι → ι . (∀ x2 . 1eb0a.. x2 ⟶ and (SNo (x1 x2)) (∀ x3 : ο . (∀ x4 . and (SNo x4) (∀ x5 : ο . (∀ x6 . and (SNo x6) (∀ x7 : ο . (∀ x8 . and (SNo x8) (∀ x9 : ο . (∀ x10 . and (SNo x10) (∀ x11 : ο . (∀ x12 . and (SNo x12) (∀ x13 : ο . (∀ x14 . and (SNo x14) (x2 = bbc71.. (x0 x2) (x1 x2) x4 x6 x8 x10 x12 x14) ⟶ x13) ⟶ x13) ⟶ x11) ⟶ x11) ⟶ x9) ⟶ x9) ⟶ x7) ⟶ x7) ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3)) ⟶ (∀ x2 . 1eb0a.. x2 ⟶ SNo (x1 x2)) ⟶ ∀ x2 : ι → ι . (∀ x3 . 1eb0a.. x3 ⟶ and (SNo (x2 x3)) (∀ x4 : ο . (∀ x5 . and (SNo x5) (∀ x6 : ο . (∀ x7 . and (SNo x7) (∀ x8 : ο . (∀ x9 . and (SNo x9) (∀ x10 : ο . (∀ x11 . and (SNo x11) (∀ x12 : ο . (∀ x13 . and (SNo x13) (x3 = bbc71.. (x0 x3) (x1 x3) (x2 x3) x5 x7 x9 x11 x13) ⟶ x12) ⟶ x12) ⟶ x10) ⟶ x10) ⟶ x8) ⟶ x8) ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4)) ⟶ (∀ x3 . 1eb0a.. x3 ⟶ SNo (x2 x3)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 . SNo x3 ⟶ SNo x4 ⟶ SNo x5 ⟶ SNo x6 ⟶ SNo x7 ⟶ SNo x8 ⟶ SNo x9 ⟶ SNo x10 ⟶ 8d7df.. x0 x1 x2 (bbc71.. x3 x4 x5 x6 x7 x8 x9 x10) = x6
Param 41ec1.. : (ι → ι) → (ι → ι) → (ι → ι) → (ι → ι) → ι → ι
Known 15adc.. : ∀ x0 : ι → ι . (∀ x1 . 1eb0a.. x1 ⟶ and (SNo (x0 x1)) (∀ x2 : ο . (∀ x3 . and (SNo x3) (∀ x4 : ο . (∀ x5 . and (SNo x5) (∀ x6 : ο . (∀ x7 . and (SNo x7) (∀ x8 : ο . (∀ x9 . and (SNo x9) (∀ x10 : ο . (∀ x11 . and (SNo x11) (∀ x12 : ο . (∀ x13 . and (SNo x13) (∀ x14 : ο . (∀ x15 . and (SNo x15) (x1 = bbc71.. (x0 x1) x3 x5 x7 x9 x11 x13 x15) ⟶ x14) ⟶ x14) ⟶ x12) ⟶ x12) ⟶ x10) ⟶ x10) ⟶ x8) ⟶ x8) ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2)) ⟶ (∀ x1 . 1eb0a.. x1 ⟶ SNo (x0 x1)) ⟶ ∀ x1 : ι → ι . (∀ x2 . 1eb0a.. x2 ⟶ and (SNo (x1 x2)) (∀ x3 : ο . (∀ x4 . and (SNo x4) (∀ x5 : ο . (∀ x6 . and (SNo x6) (∀ x7 : ο . (∀ x8 . and (SNo x8) (∀ x9 : ο . (∀ x10 . and (SNo x10) (∀ x11 : ο . (∀ x12 . and (SNo x12) (∀ x13 : ο . (∀ x14 . and (SNo x14) (x2 = bbc71.. (x0 x2) (x1 x2) x4 x6 x8 x10 x12 x14) ⟶ x13) ⟶ x13) ⟶ x11) ⟶ x11) ⟶ x9) ⟶ x9) ⟶ x7) ⟶ x7) ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3)) ⟶ (∀ x2 . 1eb0a.. x2 ⟶ SNo (x1 x2)) ⟶ ∀ x2 : ι → ι . (∀ x3 . 1eb0a.. x3 ⟶ and (SNo (x2 x3)) (∀ x4 : ο . (∀ x5 . and (SNo x5) (∀ x6 : ο . (∀ x7 . and (SNo x7) (∀ x8 : ο . (∀ x9 . and (SNo x9) (∀ x10 : ο . (∀ x11 . and (SNo x11) (∀ x12 : ο . (∀ x13 . and (SNo x13) (x3 = bbc71.. (x0 x3) (x1 x3) (x2 x3) x5 x7 x9 x11 x13) ⟶ x12) ⟶ x12) ⟶ x10) ⟶ x10) ⟶ x8) ⟶ x8) ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4)) ⟶ (∀ x3 . 1eb0a.. x3 ⟶ SNo (x2 x3)) ⟶ ∀ x3 : ι → ι . (∀ x4 . 1eb0a.. x4 ⟶ and (SNo (x3 x4)) (∀ x5 : ο . (∀ x6 . and (SNo x6) (∀ x7 : ο . (∀ x8 . and (SNo x8) (∀ x9 : ο . (∀ x10 . and (SNo x10) (∀ x11 : ο . (∀ x12 . and (SNo x12) (x4 = bbc71.. (x0 x4) (x1 x4) (x2 x4) (x3 x4) x6 x8 x10 x12) ⟶ x11) ⟶ x11) ⟶ x9) ⟶ x9) ⟶ x7) ⟶ x7) ⟶ x5) ⟶ x5)) ⟶ ∀ x4 . 1eb0a.. x4 ⟶ and (SNo (41ec1.. x0 x1 x2 x3 x4)) (∀ x5 : ο . (∀ x6 . and (SNo x6) (∀ x7 : ο . (∀ x8 . and (SNo x8) (∀ x9 : ο . (∀ x10 . and (SNo x10) (x4 = bbc71.. (x0 x4) (x1 x4) (x2 x4) (x3 x4) (41ec1.. x0 x1 x2 x3 x4) x6 x8 x10) ⟶ x9) ⟶ x9) ⟶ x7) ⟶ x7) ⟶ x5) ⟶ x5)
Known af528.. : ∀ x0 : ι → ι . (∀ x1 . 1eb0a.. x1 ⟶ and (SNo (x0 x1)) (∀ x2 : ο . (∀ x3 . and (SNo x3) (∀ x4 : ο . (∀ x5 . and (SNo x5) (∀ x6 : ο . (∀ x7 . and (SNo x7) (∀ x8 : ο . (∀ x9 . and (SNo x9) (∀ x10 : ο . (∀ x11 . and (SNo x11) (∀ x12 : ο . (∀ x13 . and (SNo x13) (∀ x14 : ο . (∀ x15 . and (SNo x15) (x1 = bbc71.. (x0 x1) x3 x5 x7 x9 x11 x13 x15) ⟶ x14) ⟶ x14) ⟶ x12) ⟶ x12) ⟶ x10) ⟶ x10) ⟶ x8) ⟶ x8) ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2)) ⟶ (∀ x1 . 1eb0a.. x1 ⟶ SNo (x0 x1)) ⟶ ∀ x1 : ι → ι . (∀ x2 . 1eb0a.. x2 ⟶ and (SNo (x1 x2)) (∀ x3 : ο . (∀ x4 . and (SNo x4) (∀ x5 : ο . (∀ x6 . and (SNo x6) (∀ x7 : ο . (∀ x8 . and (SNo x8) (∀ x9 : ο . (∀ x10 . and (SNo x10) (∀ x11 : ο . (∀ x12 . and (SNo x12) (∀ x13 : ο . (∀ x14 . and (SNo x14) (x2 = bbc71.. (x0 x2) (x1 x2) x4 x6 x8 x10 x12 x14) ⟶ x13) ⟶ x13) ⟶ x11) ⟶ x11) ⟶ x9) ⟶ x9) ⟶ x7) ⟶ x7) ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3)) ⟶ (∀ x2 . 1eb0a.. x2 ⟶ SNo (x1 x2)) ⟶ ∀ x2 : ι → ι . (∀ x3 . 1eb0a.. x3 ⟶ and (SNo (x2 x3)) (∀ x4 : ο . (∀ x5 . and (SNo x5) (∀ x6 : ο . (∀ x7 . and (SNo x7) (∀ x8 : ο . (∀ x9 . and (SNo x9) (∀ x10 : ο . (∀ x11 . and (SNo x11) (∀ x12 : ο . (∀ x13 . and (SNo x13) (x3 = bbc71.. (x0 x3) (x1 x3) (x2 x3) x5 x7 x9 x11 x13) ⟶ x12) ⟶ x12) ⟶ x10) ⟶ x10) ⟶ x8) ⟶ x8) ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4)) ⟶ (∀ x3 . 1eb0a.. x3 ⟶ SNo (x2 x3)) ⟶ ∀ x3 : ι → ι . (∀ x4 . 1eb0a.. x4 ⟶ and (SNo (x3 x4)) (∀ x5 : ο . (∀ x6 . and (SNo x6) (∀ x7 : ο . (∀ x8 . and (SNo x8) (∀ x9 : ο . (∀ x10 . and (SNo x10) (∀ x11 : ο . (∀ x12 . and (SNo x12) (x4 = bbc71.. (x0 x4) (x1 x4) (x2 x4) (x3 x4) x6 x8 x10 x12) ⟶ x11) ⟶ x11) ⟶ x9) ⟶ x9) ⟶ x7) ⟶ x7) ⟶ x5) ⟶ x5)) ⟶ ∀ x4 . 1eb0a.. x4 ⟶ SNo (41ec1.. x0 x1 x2 x3 x4)
Known 26f65.. : ∀ x0 : ι → ι . (∀ x1 . 1eb0a.. x1 ⟶ and (SNo (x0 x1)) (∀ x2 : ο . (∀ x3 . and (SNo x3) (∀ x4 : ο . (∀ x5 . and (SNo x5) (∀ x6 : ο . (∀ x7 . and (SNo x7) (∀ x8 : ο . (∀ x9 . and (SNo x9) (∀ x10 : ο . (∀ x11 . and (SNo x11) (∀ x12 : ο . (∀ x13 . and (SNo x13) (∀ x14 : ο . (∀ x15 . and (SNo x15) (x1 = bbc71.. (x0 x1) x3 x5 x7 x9 x11 x13 x15) ⟶ x14) ⟶ x14) ⟶ x12) ⟶ x12) ⟶ x10) ⟶ x10) ⟶ x8) ⟶ x8) ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2)) ⟶ (∀ x1 . 1eb0a.. x1 ⟶ SNo (x0 x1)) ⟶ ∀ x1 : ι → ι . (∀ x2 . 1eb0a.. x2 ⟶ and (SNo (x1 x2)) (∀ x3 : ο . (∀ x4 . and (SNo x4) (∀ x5 : ο . (∀ x6 . and (SNo x6) (∀ x7 : ο . (∀ x8 . and (SNo x8) (∀ x9 : ο . (∀ x10 . and (SNo x10) (∀ x11 : ο . (∀ x12 . and (SNo x12) (∀ x13 : ο . (∀ x14 . and (SNo x14) (x2 = bbc71.. (x0 x2) (x1 x2) x4 x6 x8 x10 x12 x14) ⟶ x13) ⟶ x13) ⟶ x11) ⟶ x11) ⟶ x9) ⟶ x9) ⟶ x7) ⟶ x7) ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3)) ⟶ (∀ x2 . 1eb0a.. x2 ⟶ SNo (x1 x2)) ⟶ ∀ x2 : ι → ι . (∀ x3 . 1eb0a.. x3 ⟶ and (SNo (x2 x3)) (∀ x4 : ο . (∀ x5 . and (SNo x5) (∀ x6 : ο . (∀ x7 . and (SNo x7) (∀ x8 : ο . (∀ x9 . and (SNo x9) (∀ x10 : ο . (∀ x11 . and (SNo x11) (∀ x12 : ο . (∀ x13 . and (SNo x13) (x3 = bbc71.. (x0 x3) (x1 x3) (x2 x3) x5 x7 x9 x11 x13) ⟶ x12) ⟶ x12) ⟶ x10) ⟶ x10) ⟶ x8) ⟶ x8) ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4)) ⟶ (∀ x3 . 1eb0a.. x3 ⟶ SNo (x2 x3)) ⟶ ∀ x3 : ι → ι . (∀ x4 . 1eb0a.. x4 ⟶ and (SNo (x3 x4)) (∀ x5 : ο . (∀ x6 . and (SNo x6) (∀ x7 : ο . (∀ x8 . and (SNo x8) (∀ x9 : ο . (∀ x10 . and (SNo x10) (∀ x11 : ο . (∀ x12 . and (SNo x12) (x4 = bbc71.. (x0 x4) (x1 x4) (x2 x4) (x3 x4) x6 x8 x10 x12) ⟶ x11) ⟶ x11) ⟶ x9) ⟶ x9) ⟶ x7) ⟶ x7) ⟶ x5) ⟶ x5)) ⟶ (∀ x4 . 1eb0a.. x4 ⟶ SNo (x3 x4)) ⟶ ∀ x4 x5 x6 x7 x8 x9 x10 x11 . SNo x4 ⟶ SNo x5 ⟶ SNo x6 ⟶ SNo x7 ⟶ SNo x8 ⟶ SNo x9 ⟶ SNo x10 ⟶ SNo x11 ⟶ 41ec1.. x0 x1 x2 x3 (bbc71.. x4 x5 x6 x7 x8 x9 x10 x11) = x8
Param 28f5a.. : (ι → ι) → (ι → ι) → (ι → ι) → (ι → ι) → (ι → ι) → ι → ι
Known baa4b.. : ∀ x0 : ι → ι . (∀ x1 . 1eb0a.. x1 ⟶ and (SNo (x0 x1)) (∀ x2 : ο . (∀ x3 . and (SNo x3) (∀ x4 : ο . (∀ x5 . and (SNo x5) (∀ x6 : ο . (∀ x7 . and (SNo x7) (∀ x8 : ο . (∀ x9 . and (SNo x9) (∀ x10 : ο . (∀ x11 . and (SNo x11) (∀ x12 : ο . (∀ x13 . and (SNo x13) (∀ x14 : ο . (∀ x15 . and (SNo x15) (x1 = bbc71.. (x0 x1) x3 x5 x7 x9 x11 x13 x15) ⟶ x14) ⟶ x14) ⟶ x12) ⟶ x12) ⟶ x10) ⟶ x10) ⟶ x8) ⟶ x8) ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2)) ⟶ (∀ x1 . 1eb0a.. x1 ⟶ SNo (x0 x1)) ⟶ ∀ x1 : ι → ι . (∀ x2 . 1eb0a.. x2 ⟶ and (SNo (x1 x2)) (∀ x3 : ο . (∀ x4 . and (SNo x4) (∀ x5 : ο . (∀ x6 . and (SNo x6) (∀ x7 : ο . (∀ x8 . and (SNo x8) (∀ x9 : ο . (∀ x10 . and (SNo x10) (∀ x11 : ο . (∀ x12 . and (SNo x12) (∀ x13 : ο . (∀ x14 . and (SNo x14) (x2 = bbc71.. (x0 x2) (x1 x2) x4 x6 x8 x10 x12 x14) ⟶ x13) ⟶ x13) ⟶ x11) ⟶ x11) ⟶ x9) ⟶ x9) ⟶ x7) ⟶ x7) ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3)) ⟶ (∀ x2 . 1eb0a.. x2 ⟶ SNo (x1 x2)) ⟶ ∀ x2 : ι → ι . (∀ x3 . 1eb0a.. x3 ⟶ and (SNo (x2 x3)) (∀ x4 : ο . (∀ x5 . and (SNo x5) (∀ x6 : ο . (∀ x7 . and (SNo x7) (∀ x8 : ο . (∀ x9 . and (SNo x9) (∀ x10 : ο . (∀ x11 . and (SNo x11) (∀ x12 : ο . (∀ x13 . and (SNo x13) (x3 = bbc71.. (x0 x3) (x1 x3) (x2 x3) x5 x7 x9 x11 x13) ⟶ x12) ⟶ x12) ⟶ x10) ⟶ x10) ⟶ x8) ⟶ x8) ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4)) ⟶ (∀ x3 . 1eb0a.. x3 ⟶ SNo (x2 x3)) ⟶ ∀ x3 : ι → ι . (∀ x4 . 1eb0a.. x4 ⟶ and (SNo (x3 x4)) (∀ x5 : ο . (∀ x6 . and (SNo x6) (∀ x7 : ο . (∀ x8 . and (SNo x8) (∀ x9 : ο . (∀ x10 . and (SNo x10) (∀ x11 : ο . (∀ x12 . and (SNo x12) (x4 = bbc71.. (x0 x4) (x1 x4) (x2 x4) (x3 x4) x6 x8 x10 x12) ⟶ x11) ⟶ x11) ⟶ x9) ⟶ x9) ⟶ x7) ⟶ x7) ⟶ x5) ⟶ x5)) ⟶ (∀ x4 . 1eb0a.. x4 ⟶ SNo (x3 x4)) ⟶ ∀ x4 : ι → ι . (∀ x5 . 1eb0a.. x5 ⟶ and (SNo (x4 x5)) (∀ x6 : ο . (∀ x7 . and (SNo x7) (∀ x8 : ο . (∀ x9 . and (SNo x9) (∀ x10 : ο . (∀ x11 . and (SNo x11) (x5 = bbc71.. (x0 x5) (x1 x5) (x2 x5) (x3 x5) (x4 x5) x7 x9 x11) ⟶ x10) ⟶ x10) ⟶ x8) ⟶ x8) ⟶ x6) ⟶ x6)) ⟶ ∀ x5 . 1eb0a.. x5 ⟶ and (SNo (28f5a.. x0 x1 x2 x3 x4 x5)) (∀ x6 : ο . (∀ x7 . and (SNo x7) (∀ x8 : ο . (∀ x9 . and (SNo x9) (x5 = bbc71.. (x0 x5) (x1 x5) (x2 x5) (x3 x5) (x4 x5) (28f5a.. x0 x1 x2 x3 x4 x5) x7 x9) ⟶ x8) ⟶ x8) ⟶ x6) ⟶ x6)
Known 69bbd.. : ∀ x0 : ι → ι . (∀ x1 . 1eb0a.. x1 ⟶ and (SNo (x0 x1)) (∀ x2 : ο . (∀ x3 . and (SNo x3) (∀ x4 : ο . (∀ x5 . and (SNo x5) (∀ x6 : ο . (∀ x7 . and (SNo x7) (∀ x8 : ο . (∀ x9 . and (SNo x9) (∀ x10 : ο . (∀ x11 . and (SNo x11) (∀ x12 : ο . (∀ x13 . and (SNo x13) (∀ x14 : ο . (∀ x15 . and (SNo x15) (x1 = bbc71.. (x0 x1) x3 x5 x7 x9 x11 x13 x15) ⟶ x14) ⟶ x14) ⟶ x12) ⟶ x12) ⟶ x10) ⟶ x10) ⟶ x8) ⟶ x8) ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2)) ⟶ (∀ x1 . 1eb0a.. x1 ⟶ SNo (x0 x1)) ⟶ ∀ x1 : ι → ι . (∀ x2 . 1eb0a.. x2 ⟶ and (SNo (x1 x2)) (∀ x3 : ο . (∀ x4 . and (SNo x4) (∀ x5 : ο . (∀ x6 . and (SNo x6) (∀ x7 : ο . (∀ x8 . and (SNo x8) (∀ x9 : ο . (∀ x10 . and (SNo x10) (∀ x11 : ο . (∀ x12 . and (SNo x12) (∀ x13 : ο . (∀ x14 . and (SNo x14) (x2 = bbc71.. (x0 x2) (x1 x2) x4 x6 x8 x10 x12 x14) ⟶ x13) ⟶ x13) ⟶ x11) ⟶ x11) ⟶ x9) ⟶ x9) ⟶ x7) ⟶ x7) ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3)) ⟶ (∀ x2 . 1eb0a.. x2 ⟶ SNo (x1 x2)) ⟶ ∀ x2 : ι → ι . (∀ x3 . 1eb0a.. x3 ⟶ and (SNo (x2 x3)) (∀ x4 : ο . (∀ x5 . and (SNo x5) (∀ x6 : ο . (∀ x7 . and (SNo x7) (∀ x8 : ο . (∀ x9 . and (SNo x9) (∀ x10 : ο . (∀ x11 . and (SNo x11) (∀ x12 : ο . (∀ x13 . and (SNo x13) (x3 = bbc71.. (x0 x3) (x1 x3) (x2 x3) x5 x7 x9 x11 x13) ⟶ x12) ⟶ x12) ⟶ x10) ⟶ x10) ⟶ x8) ⟶ x8) ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4)) ⟶ (∀ x3 . 1eb0a.. x3 ⟶ SNo (x2 x3)) ⟶ ∀ x3 : ι → ι . (∀ x4 . 1eb0a.. x4 ⟶ and (SNo (x3 x4)) (∀ x5 : ο . (∀ x6 . and (SNo x6) (∀ x7 : ο . (∀ x8 . and (SNo x8) (∀ x9 : ο . (∀ x10 . and (SNo x10) (∀ x11 : ο . (∀ x12 . and (SNo x12) (x4 = bbc71.. (x0 x4) (x1 x4) (x2 x4) (x3 x4) x6 x8 x10 x12) ⟶ x11) ⟶ x11) ⟶ x9) ⟶ x9) ⟶ x7) ⟶ x7) ⟶ x5) ⟶ x5)) ⟶ (∀ x4 . 1eb0a.. x4 ⟶ SNo (x3 x4)) ⟶ ∀ x4 : ι → ι . (∀ x5 . 1eb0a.. x5 ⟶ and (SNo (x4 x5)) (∀ x6 : ο . (∀ x7 . and (SNo x7) (∀ x8 : ο . (∀ x9 . and (SNo x9) (∀ x10 : ο . (∀ x11 . and (SNo x11) (x5 = bbc71.. (x0 x5) (x1 x5) (x2 x5) (x3 x5) (x4 x5) x7 x9 x11) ⟶ x10) ⟶ x10) ⟶ x8) ⟶ x8) ⟶ x6) ⟶ x6)) ⟶ ∀ x5 . 1eb0a.. x5 ⟶ SNo (28f5a.. x0 x1 x2 x3 x4 x5)
Known 62fb0.. : ∀ x0 : ι → ι . (∀ x1 . 1eb0a.. x1 ⟶ and (SNo (x0 x1)) (∀ x2 : ο . (∀ x3 . and (SNo x3) (∀ x4 : ο . (∀ x5 . and (SNo x5) (∀ x6 : ο . (∀ x7 . and (SNo x7) (∀ x8 : ο . (∀ x9 . and (SNo x9) (∀ x10 : ο . (∀ x11 . and (SNo x11) (∀ x12 : ο . (∀ x13 . and (SNo x13) (∀ x14 : ο . (∀ x15 . and (SNo x15) (x1 = bbc71.. (x0 x1) x3 x5 x7 x9 x11 x13 x15) ⟶ x14) ⟶ x14) ⟶ x12) ⟶ x12) ⟶ x10) ⟶ x10) ⟶ x8) ⟶ x8) ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2)) ⟶ (∀ x1 . 1eb0a.. x1 ⟶ SNo (x0 x1)) ⟶ ∀ x1 : ι → ι . (∀ x2 . 1eb0a.. x2 ⟶ and (SNo (x1 x2)) (∀ x3 : ο . (∀ x4 . and (SNo x4) (∀ x5 : ο . (∀ x6 . and (SNo x6) (∀ x7 : ο . (∀ x8 . and (SNo x8) (∀ x9 : ο . (∀ x10 . and (SNo x10) (∀ x11 : ο . (∀ x12 . and (SNo x12) (∀ x13 : ο . (∀ x14 . and (SNo x14) (x2 = bbc71.. (x0 x2) (x1 x2) x4 x6 x8 x10 x12 x14) ⟶ x13) ⟶ x13) ⟶ x11) ⟶ x11) ⟶ x9) ⟶ x9) ⟶ x7) ⟶ x7) ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3)) ⟶ (∀ x2 . 1eb0a.. x2 ⟶ SNo (x1 x2)) ⟶ ∀ x2 : ι → ι . (∀ x3 . 1eb0a.. x3 ⟶ and (SNo (x2 x3)) (∀ x4 : ο . (∀ x5 . and (SNo x5) (∀ x6 : ο . (∀ x7 . and (SNo x7) (∀ x8 : ο . (∀ x9 . and (SNo x9) (∀ x10 : ο . (∀ x11 . and (SNo x11) (∀ x12 : ο . (∀ x13 . and (SNo x13) (x3 = bbc71.. (x0 x3) (x1 x3) (x2 x3) x5 x7 x9 x11 x13) ⟶ x12) ⟶ x12) ⟶ x10) ⟶ x10) ⟶ x8) ⟶ x8) ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4)) ⟶ (∀ x3 . 1eb0a.. x3 ⟶ SNo (x2 x3)) ⟶ ∀ x3 : ι → ι . (∀ x4 . 1eb0a.. x4 ⟶ and (SNo (x3 x4)) (∀ x5 : ο . (∀ x6 . and (SNo x6) (∀ x7 : ο . (∀ x8 . and (SNo x8) (∀ x9 : ο . (∀ x10 . and (SNo x10) (∀ x11 : ο . (∀ x12 . and (SNo x12) (x4 = bbc71.. (x0 x4) (x1 x4) (x2 x4) (x3 x4) x6 x8 x10 x12) ⟶ x11) ⟶ x11) ⟶ x9) ⟶ x9) ⟶ x7) ⟶ x7) ⟶ x5) ⟶ x5)) ⟶ (∀ x4 . 1eb0a.. x4 ⟶ SNo (x3 x4)) ⟶ ∀ x4 : ι → ι . (∀ x5 . 1eb0a.. x5 ⟶ and (SNo (x4 x5)) (∀ x6 : ο . (∀ x7 . and (SNo x7) (∀ x8 : ο . (∀ x9 . and (SNo x9) (∀ x10 : ο . (∀ x11 . and (SNo x11) (x5 = bbc71.. (x0 x5) (x1 x5) (x2 x5) (x3 x5) (x4 x5) x7 x9 x11) ⟶ x10) ⟶ x10) ⟶ x8) ⟶ x8) ⟶ x6) ⟶ x6)) ⟶ (∀ x5 . 1eb0a.. x5 ⟶ SNo (x4 x5)) ⟶ ∀ x5 x6 x7 x8 x9 x10 x11 x12 . SNo x5 ⟶ SNo x6 ⟶ SNo x7 ⟶ SNo x8 ⟶ SNo x9 ⟶ SNo x10 ⟶ SNo x11 ⟶ SNo x12 ⟶ 28f5a.. x0 x1 x2 x3 x4 (bbc71.. x5 x6 x7 x8 x9 x10 x11 x12) = x10
Param 717b4.. : (ι → ι) → (ι → ι) → (ι → ι) → (ι → ι) → (ι → ι) → (ι → ι) → ι → ι
Known 42518.. : ∀ x0 : ι → ι . (∀ x1 . 1eb0a.. x1 ⟶ and (SNo (x0 x1)) (∀ x2 : ο . (∀ x3 . and (SNo x3) (∀ x4 : ο . (∀ x5 . and (SNo x5) (∀ x6 : ο . (∀ x7 . and (SNo x7) (∀ x8 : ο . (∀ x9 . and (SNo x9) (∀ x10 : ο . (∀ x11 . and (SNo x11) (∀ x12 : ο . (∀ x13 . and (SNo x13) (∀ x14 : ο . (∀ x15 . and (SNo x15) (x1 = bbc71.. (x0 x1) x3 x5 x7 x9 x11 x13 x15) ⟶ x14) ⟶ x14) ⟶ x12) ⟶ x12) ⟶ x10) ⟶ x10) ⟶ x8) ⟶ x8) ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2)) ⟶ (∀ x1 . 1eb0a.. x1 ⟶ SNo (x0 x1)) ⟶ ∀ x1 : ι → ι . (∀ x2 . 1eb0a.. x2 ⟶ and (SNo (x1 x2)) (∀ x3 : ο . (∀ x4 . and (SNo x4) (∀ x5 : ο . (∀ x6 . and (SNo x6) (∀ x7 : ο . (∀ x8 . and (SNo x8) (∀ x9 : ο . (∀ x10 . and (SNo x10) (∀ x11 : ο . (∀ x12 . and (SNo x12) (∀ x13 : ο . (∀ x14 . and (SNo x14) (x2 = bbc71.. (x0 x2) (x1 x2) x4 x6 x8 x10 x12 x14) ⟶ x13) ⟶ x13) ⟶ x11) ⟶ x11) ⟶ x9) ⟶ x9) ⟶ x7) ⟶ x7) ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3)) ⟶ (∀ x2 . 1eb0a.. x2 ⟶ SNo (x1 x2)) ⟶ ∀ x2 : ι → ι . (∀ x3 . 1eb0a.. x3 ⟶ and (SNo (x2 x3)) (∀ x4 : ο . (∀ x5 . and (SNo x5) (∀ x6 : ο . (∀ x7 . and (SNo x7) (∀ x8 : ο . (∀ x9 . and (SNo x9) (∀ x10 : ο . (∀ x11 . and (SNo x11) (∀ x12 : ο . (∀ x13 . and (SNo x13) (x3 = bbc71.. (x0 x3) (x1 x3) (x2 x3) x5 x7 x9 x11 x13) ⟶ x12) ⟶ x12) ⟶ x10) ⟶ x10) ⟶ x8) ⟶ x8) ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4)) ⟶ (∀ x3 . 1eb0a.. x3 ⟶ SNo (x2 x3)) ⟶ ∀ x3 : ι → ι . (∀ x4 . 1eb0a.. x4 ⟶ and (SNo (x3 x4)) (∀ x5 : ο . (∀ x6 . and (SNo x6) (∀ x7 : ο . (∀ x8 . and (SNo x8) (∀ x9 : ο . (∀ x10 . and (SNo x10) (∀ x11 : ο . (∀ x12 . and (SNo x12) (x4 = bbc71.. (x0 x4) (x1 x4) (x2 x4) (x3 x4) x6 x8 x10 x12) ⟶ x11) ⟶ x11) ⟶ x9) ⟶ x9) ⟶ x7) ⟶ x7) ⟶ x5) ⟶ x5)) ⟶ (∀ x4 . 1eb0a.. x4 ⟶ SNo (x3 x4)) ⟶ ∀ x4 : ι → ι . (∀ x5 . 1eb0a.. x5 ⟶ and (SNo (x4 x5)) (∀ x6 : ο . (∀ x7 . and (SNo x7) (∀ x8 : ο . (∀ x9 . and (SNo x9) (∀ x10 : ο . (∀ x11 . and (SNo x11) (x5 = bbc71.. (x0 x5) (x1 x5) (x2 x5) (x3 x5) (x4 x5) x7 x9 x11) ⟶ x10) ⟶ x10) ⟶ x8) ⟶ x8) ⟶ x6) ⟶ x6)) ⟶ (∀ x5 . 1eb0a.. x5 ⟶ SNo (x4 x5)) ⟶ ∀ x5 : ι → ι . (∀ x6 . 1eb0a.. x6 ⟶ and (SNo (x5 x6)) (∀ x7 : ο . (∀ x8 . and (SNo x8) (∀ x9 : ο . (∀ x10 . and (SNo x10) (x6 = bbc71.. (x0 x6) (x1 x6) (x2 x6) (x3 x6) (x4 x6) (x5 x6) x8 x10) ⟶ x9) ⟶ x9) ⟶ x7) ⟶ x7)) ⟶ ∀ x6 . 1eb0a.. x6 ⟶ and (SNo (717b4.. x0 x1 x2 x3 x4 x5 x6)) (∀ x7 : ο . (∀ x8 . and (SNo x8) (x6 = bbc71.. (x0 x6) (x1 x6) (x2 x6) (x3 x6) (x4 x6) (x5 x6) (717b4.. x0 x1 x2 x3 x4 x5 x6) x8) ⟶ x7) ⟶ x7)
Known 9599d.. : ∀ x0 : ι → ι . (∀ x1 . 1eb0a.. x1 ⟶ and (SNo (x0 x1)) (∀ x2 : ο . (∀ x3 . and (SNo x3) (∀ x4 : ο . (∀ x5 . and (SNo x5) (∀ x6 : ο . (∀ x7 . and (SNo x7) (∀ x8 : ο . (∀ x9 . and (SNo x9) (∀ x10 : ο . (∀ x11 . and (SNo x11) (∀ x12 : ο . (∀ x13 . and (SNo x13) (∀ x14 : ο . (∀ x15 . and (SNo x15) (x1 = bbc71.. (x0 x1) x3 x5 x7 x9 x11 x13 x15) ⟶ x14) ⟶ x14) ⟶ x12) ⟶ x12) ⟶ x10) ⟶ x10) ⟶ x8) ⟶ x8) ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2)) ⟶ (∀ x1 . 1eb0a.. x1 ⟶ SNo (x0 x1)) ⟶ ∀ x1 : ι → ι . (∀ x2 . 1eb0a.. x2 ⟶ and (SNo (x1 x2)) (∀ x3 : ο . (∀ x4 . and (SNo x4) (∀ x5 : ο . (∀ x6 . and (SNo x6) (∀ x7 : ο . (∀ x8 . and (SNo x8) (∀ x9 : ο . (∀ x10 . and (SNo x10) (∀ x11 : ο . (∀ x12 . and (SNo x12) (∀ x13 : ο . (∀ x14 . and (SNo x14) (x2 = bbc71.. (x0 x2) (x1 x2) x4 x6 x8 x10 x12 x14) ⟶ x13) ⟶ x13) ⟶ x11) ⟶ x11) ⟶ x9) ⟶ x9) ⟶ x7) ⟶ x7) ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3)) ⟶ (∀ x2 . 1eb0a.. x2 ⟶ SNo (x1 x2)) ⟶ ∀ x2 : ι → ι . (∀ x3 . 1eb0a.. x3 ⟶ and (SNo (x2 x3)) (∀ x4 : ο . (∀ x5 . and (SNo x5) (∀ x6 : ο . (∀ x7 . and (SNo x7) (∀ x8 : ο . (∀ x9 . and (SNo x9) (∀ x10 : ο . (∀ x11 . and (SNo x11) (∀ x12 : ο . (∀ x13 . and (SNo x13) (x3 = bbc71.. (x0 x3) (x1 x3) (x2 x3) x5 x7 x9 x11 x13) ⟶ x12) ⟶ x12) ⟶ x10) ⟶ x10) ⟶ x8) ⟶ x8) ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4)) ⟶ (∀ x3 . 1eb0a.. x3 ⟶ SNo (x2 x3)) ⟶ ∀ x3 : ι → ι . (∀ x4 . 1eb0a.. x4 ⟶ and (SNo (x3 x4)) (∀ x5 : ο . (∀ x6 . and (SNo x6) (∀ x7 : ο . (∀ x8 . and (SNo x8) (∀ x9 : ο . (∀ x10 . and (SNo x10) (∀ x11 : ο . (∀ x12 . and (SNo x12) (x4 = bbc71.. (x0 x4) (x1 x4) (x2 x4) (x3 x4) x6 x8 x10 x12) ⟶ x11) ⟶ x11) ⟶ x9) ⟶ x9) ⟶ x7) ⟶ x7) ⟶ x5) ⟶ x5)) ⟶ (∀ x4 . 1eb0a.. x4 ⟶ SNo (x3 x4)) ⟶ ∀ x4 : ι → ι . (∀ x5 . 1eb0a.. x5 ⟶ and (SNo (x4 x5)) (∀ x6 : ο . (∀ x7 . and (SNo x7) (∀ x8 : ο . (∀ x9 . and (SNo x9) (∀ x10 : ο . (∀ x11 . and (SNo x11) (x5 = bbc71.. (x0 x5) (x1 x5) (x2 x5) (x3 x5) (x4 x5) x7 x9 x11) ⟶ x10) ⟶ x10) ⟶ x8) ⟶ x8) ⟶ x6) ⟶ x6)) ⟶ (∀ x5 . 1eb0a.. x5 ⟶ SNo (x4 x5)) ⟶ ∀ x5 : ι → ι . (∀ x6 . 1eb0a.. x6 ⟶ and (SNo (x5 x6)) (∀ x7 : ο . (∀ x8 . and (SNo x8) (∀ x9 : ο . (∀ x10 . and (SNo x10) (x6 = bbc71.. (x0 x6) (x1 x6) (x2 x6) (x3 x6) (x4 x6) (x5 x6) x8 x10) ⟶ x9) ⟶ x9) ⟶ x7) ⟶ x7)) ⟶ ∀ x6 . 1eb0a.. x6 ⟶ SNo (717b4.. x0 x1 x2 x3 x4 x5 x6)
Known c7d23.. : ∀ x0 : ι → ι . (∀ x1 . 1eb0a.. x1 ⟶ and (SNo (x0 x1)) (∀ x2 : ο . (∀ x3 . and (SNo x3) (∀ x4 : ο . (∀ x5 . and (SNo x5) (∀ x6 : ο . (∀ x7 . and (SNo x7) (∀ x8 : ο . (∀ x9 . and (SNo x9) (∀ x10 : ο . (∀ x11 . and (SNo x11) (∀ x12 : ο . (∀ x13 . and (SNo x13) (∀ x14 : ο . (∀ x15 . and (SNo x15) (x1 = bbc71.. (x0 x1) x3 x5 x7 x9 x11 x13 x15) ⟶ x14) ⟶ x14) ⟶ x12) ⟶ x12) ⟶ x10) ⟶ x10) ⟶ x8) ⟶ x8) ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2)) ⟶ (∀ x1 . 1eb0a.. x1 ⟶ SNo (x0 x1)) ⟶ ∀ x1 : ι → ι . (∀ x2 . 1eb0a.. x2 ⟶ and (SNo (x1 x2)) (∀ x3 : ο . (∀ x4 . and (SNo x4) (∀ x5 : ο . (∀ x6 . and (SNo x6) (∀ x7 : ο . (∀ x8 . and (SNo x8) (∀ x9 : ο . (∀ x10 . and (SNo x10) (∀ x11 : ο . (∀ x12 . and (SNo x12) (∀ x13 : ο . (∀ x14 . and (SNo x14) (x2 = bbc71.. (x0 x2) (x1 x2) x4 x6 x8 x10 x12 x14) ⟶ x13) ⟶ x13) ⟶ x11) ⟶ x11) ⟶ x9) ⟶ x9) ⟶ x7) ⟶ x7) ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3)) ⟶ (∀ x2 . 1eb0a.. x2 ⟶ SNo (x1 x2)) ⟶ ∀ x2 : ι → ι . (∀ x3 . 1eb0a.. x3 ⟶ and (SNo (x2 x3)) (∀ x4 : ο . (∀ x5 . and (SNo x5) (∀ x6 : ο . (∀ x7 . and (SNo x7) (∀ x8 : ο . (∀ x9 . and (SNo x9) (∀ x10 : ο . (∀ x11 . and (SNo x11) (∀ x12 : ο . (∀ x13 . and (SNo x13) (x3 = bbc71.. (x0 x3) (x1 x3) (x2 x3) x5 x7 x9 x11 x13) ⟶ x12) ⟶ x12) ⟶ x10) ⟶ x10) ⟶ x8) ⟶ x8) ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4)) ⟶ (∀ x3 . 1eb0a.. x3 ⟶ SNo (x2 x3)) ⟶ ∀ x3 : ι → ι . (∀ x4 . 1eb0a.. x4 ⟶ and (SNo (x3 x4)) (∀ x5 : ο . (∀ x6 . and (SNo x6) (∀ x7 : ο . (∀ x8 . and (SNo x8) (∀ x9 : ο . (∀ x10 . and (SNo x10) (∀ x11 : ο . (∀ x12 . and (SNo x12) (x4 = bbc71.. (x0 x4) (x1 x4) (x2 x4) (x3 x4) x6 x8 x10 x12) ⟶ x11) ⟶ x11) ⟶ x9) ⟶ x9) ⟶ x7) ⟶ x7) ⟶ x5) ⟶ x5)) ⟶ (∀ x4 . 1eb0a.. x4 ⟶ SNo (x3 x4)) ⟶ ∀ x4 : ι → ι . (∀ x5 . 1eb0a.. x5 ⟶ and (SNo (x4 x5)) (∀ x6 : ο . (∀ x7 . and (SNo x7) (∀ x8 : ο . (∀ x9 . and (SNo x9) (∀ x10 : ο . (∀ x11 . and (SNo x11) (x5 = bbc71.. (x0 x5) (x1 x5) (x2 x5) (x3 x5) (x4 x5) x7 x9 x11) ⟶ x10) ⟶ x10) ⟶ x8) ⟶ x8) ⟶ x6) ⟶ x6)) ⟶ (∀ x5 . 1eb0a.. x5 ⟶ SNo (x4 x5)) ⟶ ∀ x5 : ι → ι . (∀ x6 . 1eb0a.. x6 ⟶ and (SNo (x5 x6)) (∀ x7 : ο . (∀ x8 . and (SNo x8) (∀ x9 : ο . (∀ x10 . and (SNo x10) (x6 = bbc71.. (x0 x6) (x1 x6) (x2 x6) (x3 x6) (x4 x6) (x5 x6) x8 x10) ⟶ x9) ⟶ x9) ⟶ x7) ⟶ x7)) ⟶ (∀ x6 . 1eb0a.. x6 ⟶ SNo (x5 x6)) ⟶ ∀ x6 x7 x8 x9 x10 x11 x12 x13 . SNo x6 ⟶ SNo x7 ⟶ SNo x8 ⟶ SNo x9 ⟶ SNo x10 ⟶ SNo x11 ⟶ SNo x12 ⟶ SNo x13 ⟶ 717b4.. x0 x1 x2 x3 x4 x5 (bbc71.. x6 x7 x8 x9 x10 x11 x12 x13) = x12
Param 053de.. : (ι → ι) → (ι → ι) → (ι → ι) → (ι → ι) → (ι → ι) → (ι → ι) → (ι → ι) → ι → ι
Known 0b166.. : ∀ x0 : ι → ι . (∀ x1 . 1eb0a.. x1 ⟶ and (SNo (x0 x1)) (∀ x2 : ο . (∀ x3 . and (SNo x3) (∀ x4 : ο . (∀ x5 . and (SNo x5) (∀ x6 : ο . (∀ x7 . and (SNo x7) (∀ x8 : ο . (∀ x9 . and (SNo x9) (∀ x10 : ο . (∀ x11 . and (SNo x11) (∀ x12 : ο . (∀ x13 . and (SNo x13) (∀ x14 : ο . (∀ x15 . and (SNo x15) (x1 = bbc71.. (x0 x1) x3 x5 x7 x9 x11 x13 x15) ⟶ x14) ⟶ x14) ⟶ x12) ⟶ x12) ⟶ x10) ⟶ x10) ⟶ x8) ⟶ x8) ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2)) ⟶ (∀ x1 . 1eb0a.. x1 ⟶ SNo (x0 x1)) ⟶ ∀ x1 : ι → ι . (∀ x2 . 1eb0a.. x2 ⟶ and (SNo (x1 x2)) (∀ x3 : ο . (∀ x4 . and (SNo x4) (∀ x5 : ο . (∀ x6 . and (SNo x6) (∀ x7 : ο . (∀ x8 . and (SNo x8) (∀ x9 : ο . (∀ x10 . and (SNo x10) (∀ x11 : ο . (∀ x12 . and (SNo x12) (∀ x13 : ο . (∀ x14 . and (SNo x14) (x2 = bbc71.. (x0 x2) (x1 x2) x4 x6 x8 x10 x12 x14) ⟶ x13) ⟶ x13) ⟶ x11) ⟶ x11) ⟶ x9) ⟶ x9) ⟶ x7) ⟶ x7) ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3)) ⟶ (∀ x2 . 1eb0a.. x2 ⟶ SNo (x1 x2)) ⟶ ∀ x2 : ι → ι . (∀ x3 . 1eb0a.. x3 ⟶ and (SNo (x2 x3)) (∀ x4 : ο . (∀ x5 . and (SNo x5) (∀ x6 : ο . (∀ x7 . and (SNo x7) (∀ x8 : ο . (∀ x9 . and (SNo x9) (∀ x10 : ο . (∀ x11 . and (SNo x11) (∀ x12 : ο . (∀ x13 . and (SNo x13) (x3 = bbc71.. (x0 x3) (x1 x3) (x2 x3) x5 x7 x9 x11 x13) ⟶ x12) ⟶ x12) ⟶ x10) ⟶ x10) ⟶ x8) ⟶ x8) ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4)) ⟶ (∀ x3 . 1eb0a.. x3 ⟶ SNo (x2 x3)) ⟶ ∀ x3 : ι → ι . (∀ x4 . 1eb0a.. x4 ⟶ and (SNo (x3 x4)) (∀ x5 : ο . (∀ x6 . and (SNo x6) (∀ x7 : ο . (∀ x8 . and (SNo x8) (∀ x9 : ο . (∀ x10 . and (SNo x10) (∀ x11 : ο . (∀ x12 . and (SNo x12) (x4 = bbc71.. (x0 x4) (x1 x4) (x2 x4) (x3 x4) x6 x8 x10 x12) ⟶ x11) ⟶ x11) ⟶ x9) ⟶ x9) ⟶ x7) ⟶ x7) ⟶ x5) ⟶ x5)) ⟶ (∀ x4 . 1eb0a.. x4 ⟶ SNo (x3 x4)) ⟶ ∀ x4 : ι → ι . (∀ x5 . 1eb0a.. x5 ⟶ and (SNo (x4 x5)) (∀ x6 : ο . (∀ x7 . and (SNo x7) (∀ x8 : ο . (∀ x9 . and (SNo x9) (∀ x10 : ο . (∀ x11 . and (SNo x11) (x5 = bbc71.. (x0 x5) (x1 x5) (x2 x5) (x3 x5) (x4 x5) x7 x9 x11) ⟶ x10) ⟶ x10) ⟶ x8) ⟶ x8) ⟶ x6) ⟶ x6)) ⟶ (∀ x5 . 1eb0a.. x5 ⟶ SNo (x4 x5)) ⟶ ∀ x5 : ι → ι . (∀ x6 . 1eb0a.. x6 ⟶ and (SNo (x5 x6)) (∀ x7 : ο . (∀ x8 . and (SNo x8) (∀ x9 : ο . (∀ x10 . and (SNo x10) (x6 = bbc71.. (x0 x6) (x1 x6) (x2 x6) (x3 x6) (x4 x6) (x5 x6) x8 x10) ⟶ x9) ⟶ x9) ⟶ x7) ⟶ x7)) ⟶ (∀ x6 . 1eb0a.. x6 ⟶ SNo (x5 x6)) ⟶ ∀ x6 : ι → ι . (∀ x7 . 1eb0a.. x7 ⟶ and (SNo (x6 x7)) (∀ x8 : ο . (∀ x9 . and (SNo x9) (x7 = bbc71.. (x0 x7) (x1 x7) (x2 x7) (x3 x7) (x4 x7) (x5 x7) (x6 x7) x9) ⟶ x8) ⟶ x8)) ⟶ ∀ x7 . 1eb0a.. x7 ⟶ and (SNo (053de.. x0 x1 x2 x3 x4 x5 x6 x7)) (x7 = bbc71.. (x0 x7) (x1 x7) (x2 x7) (x3 x7) (x4 x7) (x5 x7) (x6 x7) (053de.. x0 x1 x2 x3 x4 x5 x6 x7))
Known 0c70a.. : ∀ x0 : ι → ι . (∀ x1 . 1eb0a.. x1 ⟶ and (SNo (x0 x1)) (∀ x2 : ο . (∀ x3 . and (SNo x3) (∀ x4 : ο . (∀ x5 . and (SNo x5) (∀ x6 : ο . (∀ x7 . and (SNo x7) (∀ x8 : ο . (∀ x9 . and (SNo x9) (∀ x10 : ο . (∀ x11 . and (SNo x11) (∀ x12 : ο . (∀ x13 . and (SNo x13) (∀ x14 : ο . (∀ x15 . and (SNo x15) (x1 = bbc71.. (x0 x1) x3 x5 x7 x9 x11 x13 x15) ⟶ x14) ⟶ x14) ⟶ x12) ⟶ x12) ⟶ x10) ⟶ x10) ⟶ x8) ⟶ x8) ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2)) ⟶ (∀ x1 . 1eb0a.. x1 ⟶ SNo (x0 x1)) ⟶ ∀ x1 : ι → ι . (∀ x2 . 1eb0a.. x2 ⟶ and (SNo (x1 x2)) (∀ x3 : ο . (∀ x4 . and (SNo x4) (∀ x5 : ο . (∀ x6 . and (SNo x6) (∀ x7 : ο . (∀ x8 . and (SNo x8) (∀ x9 : ο . (∀ x10 . and (SNo x10) (∀ x11 : ο . (∀ x12 . and (SNo x12) (∀ x13 : ο . (∀ x14 . and (SNo x14) (x2 = bbc71.. (x0 x2) (x1 x2) x4 x6 x8 x10 x12 x14) ⟶ x13) ⟶ x13) ⟶ x11) ⟶ x11) ⟶ x9) ⟶ x9) ⟶ x7) ⟶ x7) ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3)) ⟶ (∀ x2 . 1eb0a.. x2 ⟶ SNo (x1 x2)) ⟶ ∀ x2 : ι → ι . (∀ x3 . 1eb0a.. x3 ⟶ and (SNo (x2 x3)) (∀ x4 : ο . (∀ x5 . and (SNo x5) (∀ x6 : ο . (∀ x7 . and (SNo x7) (∀ x8 : ο . (∀ x9 . and (SNo x9) (∀ x10 : ο . (∀ x11 . and (SNo x11) (∀ x12 : ο . (∀ x13 . and (SNo x13) (x3 = bbc71.. (x0 x3) (x1 x3) (x2 x3) x5 x7 x9 x11 x13) ⟶ x12) ⟶ x12) ⟶ x10) ⟶ x10) ⟶ x8) ⟶ x8) ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4)) ⟶ (∀ x3 . 1eb0a.. x3 ⟶ SNo (x2 x3)) ⟶ ∀ x3 : ι → ι . (∀ x4 . 1eb0a.. x4 ⟶ and (SNo (x3 x4)) (∀ x5 : ο . (∀ x6 . and (SNo x6) (∀ x7 : ο . (∀ x8 . and (SNo x8) (∀ x9 : ο . (∀ x10 . and (SNo x10) (∀ x11 : ο . (∀ x12 . and (SNo x12) (x4 = bbc71.. (x0 x4) (x1 x4) (x2 x4) (x3 x4) x6 x8 x10 x12) ⟶ x11) ⟶ x11) ⟶ x9) ⟶ x9) ⟶ x7) ⟶ x7) ⟶ x5) ⟶ x5)) ⟶ (∀ x4 . 1eb0a.. x4 ⟶ SNo (x3 x4)) ⟶ ∀ x4 : ι → ι . (∀ x5 . 1eb0a.. x5 ⟶ and (SNo (x4 x5)) (∀ x6 : ο . (∀ x7 . and (SNo x7) (∀ x8 : ο . (∀ x9 . and (SNo x9) (∀ x10 : ο . (∀ x11 . and (SNo x11) (x5 = bbc71.. (x0 x5) (x1 x5) (x2 x5) (x3 x5) (x4 x5) x7 x9 x11) ⟶ x10) ⟶ x10) ⟶ x8) ⟶ x8) ⟶ x6) ⟶ x6)) ⟶ (∀ x5 . 1eb0a.. x5 ⟶ SNo (x4 x5)) ⟶ ∀ x5 : ι → ι . (∀ x6 . 1eb0a.. x6 ⟶ and (SNo (x5 x6)) (∀ x7 : ο . (∀ x8 . and (SNo x8) (∀ x9 : ο . (∀ x10 . and (SNo x10) (x6 = bbc71.. (x0 x6) (x1 x6) (x2 x6) (x3 x6) (x4 x6) (x5 x6) x8 x10) ⟶ x9) ⟶ x9) ⟶ x7) ⟶ x7)) ⟶ (∀ x6 . 1eb0a.. x6 ⟶ SNo (x5 x6)) ⟶ ∀ x6 : ι → ι . (∀ x7 . 1eb0a.. x7 ⟶ and (SNo (x6 x7)) (∀ x8 : ο . (∀ x9 . and (SNo x9) (x7 = bbc71.. (x0 x7) (x1 x7) (x2 x7) (x3 x7) (x4 x7) (x5 x7) (x6 x7) x9) ⟶ x8) ⟶ x8)) ⟶ ∀ x7 . 1eb0a.. x7 ⟶ SNo (053de.. x0 x1 x2 x3 x4 x5 x6 x7)
Known 48feb.. : ∀ x0 : ι → ι . (∀ x1 . 1eb0a.. x1 ⟶ and (SNo (x0 x1)) (∀ x2 : ο . (∀ x3 . and (SNo x3) (∀ x4 : ο . (∀ x5 . and (SNo x5) (∀ x6 : ο . (∀ x7 . and (SNo x7) (∀ x8 : ο . (∀ x9 . and (SNo x9) (∀ x10 : ο . (∀ x11 . and (SNo x11) (∀ x12 : ο . (∀ x13 . and (SNo x13) (∀ x14 : ο . (∀ x15 . and (SNo x15) (x1 = bbc71.. (x0 x1) x3 x5 x7 x9 x11 x13 x15) ⟶ x14) ⟶ x14) ⟶ x12) ⟶ x12) ⟶ x10) ⟶ x10) ⟶ x8) ⟶ x8) ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2)) ⟶ (∀ x1 . 1eb0a.. x1 ⟶ SNo (x0 x1)) ⟶ ∀ x1 : ι → ι . (∀ x2 . 1eb0a.. x2 ⟶ and (SNo (x1 x2)) (∀ x3 : ο . (∀ x4 . and (SNo x4) (∀ x5 : ο . (∀ x6 . and (SNo x6) (∀ x7 : ο . (∀ x8 . and (SNo x8) (∀ x9 : ο . (∀ x10 . and (SNo x10) (∀ x11 : ο . (∀ x12 . and (SNo x12) (∀ x13 : ο . (∀ x14 . and (SNo x14) (x2 = bbc71.. (x0 x2) (x1 x2) x4 x6 x8 x10 x12 x14) ⟶ x13) ⟶ x13) ⟶ x11) ⟶ x11) ⟶ x9) ⟶ x9) ⟶ x7) ⟶ x7) ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3)) ⟶ (∀ x2 . 1eb0a.. x2 ⟶ SNo (x1 x2)) ⟶ ∀ x2 : ι → ι . (∀ x3 . 1eb0a.. x3 ⟶ and (SNo (x2 x3)) (∀ x4 : ο . (∀ x5 . and (SNo x5) (∀ x6 : ο . (∀ x7 . and (SNo x7) (∀ x8 : ο . (∀ x9 . and (SNo x9) (∀ x10 : ο . (∀ x11 . and (SNo x11) (∀ x12 : ο . (∀ x13 . and (SNo x13) (x3 = bbc71.. (x0 x3) (x1 x3) (x2 x3) x5 x7 x9 x11 x13) ⟶ x12) ⟶ x12) ⟶ x10) ⟶ x10) ⟶ x8) ⟶ x8) ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4)) ⟶ (∀ x3 . 1eb0a.. x3 ⟶ SNo (x2 x3)) ⟶ ∀ x3 : ι → ι . (∀ x4 . 1eb0a.. x4 ⟶ and (SNo (x3 x4)) (∀ x5 : ο . (∀ x6 . and (SNo x6) (∀ x7 : ο . (∀ x8 . and (SNo x8) (∀ x9 : ο . (∀ x10 . and (SNo x10) (∀ x11 : ο . (∀ x12 . and (SNo x12) (x4 = bbc71.. (x0 x4) (x1 x4) (x2 x4) (x3 x4) x6 x8 x10 x12) ⟶ x11) ⟶ x11) ⟶ x9) ⟶ x9) ⟶ x7) ⟶ x7) ⟶ x5) ⟶ x5)) ⟶ (∀ x4 . 1eb0a.. x4 ⟶ SNo (x3 x4)) ⟶ ∀ x4 : ι → ι . (∀ x5 . 1eb0a.. x5 ⟶ and (SNo (x4 x5)) (∀ x6 : ο . (∀ x7 . and (SNo x7) (∀ x8 : ο . (∀ x9 . and (SNo x9) (∀ x10 : ο . (∀ x11 . and (SNo x11) (x5 = bbc71.. (x0 x5) (x1 x5) (x2 x5) (x3 x5) (x4 x5) x7 x9 x11) ⟶ x10) ⟶ x10) ⟶ x8) ⟶ x8) ⟶ x6) ⟶ x6)) ⟶ (∀ x5 . 1eb0a.. x5 ⟶ SNo (x4 x5)) ⟶ ∀ x5 : ι → ι . (∀ x6 . 1eb0a.. x6 ⟶ and (SNo (x5 x6)) (∀ x7 : ο . (∀ x8 . and (SNo x8) (∀ x9 : ο . (∀ x10 . and (SNo x10) (x6 = bbc71.. (x0 x6) (x1 x6) (x2 x6) (x3 x6) (x4 x6) (x5 x6) x8 x10) ⟶ x9) ⟶ x9) ⟶ x7) ⟶ x7)) ⟶ (∀ x6 . 1eb0a.. x6 ⟶ SNo (x5 x6)) ⟶ ∀ x6 : ι → ι . (∀ x7 . 1eb0a.. x7 ⟶ and (SNo (x6 x7)) (∀ x8 : ο . (∀ x9 . and (SNo x9) (x7 = bbc71.. (x0 x7) (x1 x7) (x2 x7) (x3 x7) (x4 x7) (x5 x7) (x6 x7) x9) ⟶ x8) ⟶ x8)) ⟶ (∀ x7 . 1eb0a.. x7 ⟶ SNo (x6 x7)) ⟶ ∀ x7 x8 x9 x10 x11 x12 x13 x14 . SNo x7 ⟶ SNo x8 ⟶ SNo x9 ⟶ SNo x10 ⟶ SNo x11 ⟶ SNo x12 ⟶ SNo x13 ⟶ SNo x14 ⟶ 053de.. x0 x1 x2 x3 x4 x5 x6 (bbc71.. x7 x8 x9 x10 x11 x12 x13 x14) = x14
Definition c6963.. := d4639.. 8dd2c..
Definition a9894.. := 50208.. 8dd2c.. c6963..
Definition da724.. := 8d7df.. 8dd2c.. c6963.. a9894..
Definition adebb.. := 41ec1.. 8dd2c.. c6963.. a9894.. da724..
Definition 91922.. := 28f5a.. 8dd2c.. c6963.. a9894.. da724.. adebb..
Definition b8e07.. := 717b4.. 8dd2c.. c6963.. a9894.. da724.. adebb.. 91922..
Definition 7f2e4.. := 053de.. 8dd2c.. c6963.. a9894.. da724.. adebb.. 91922.. b8e07..
Theorem 4b34b.. : ∀ x0 . 1eb0a.. x0 ⟶ and (SNo (c6963.. x0)) (∀ x1 : ο . (∀ x2 . and (SNo x2) (∀ x3 : ο . (∀ x4 . and (SNo x4) (∀ x5 : ο . (∀ x6 . and (SNo x6) (∀ x7 : ο . (∀ x8 . and (SNo x8) (∀ x9 : ο . (∀ x10 . and (SNo x10) (∀ x11 : ο . (∀ x12 . and (SNo x12) (x0 = bbc71.. (8dd2c.. x0) (c6963.. x0) x2 x4 x6 x8 x10 x12) ⟶ x11) ⟶ x11) ⟶ x9) ⟶ x9) ⟶ x7) ⟶ x7) ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3) ⟶ x1) ⟶ x1) (proof)
Theorem 675f4.. : ∀ x0 . 1eb0a.. x0 ⟶ SNo (c6963.. x0) (proof)
Theorem 58949.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ SNo x5 ⟶ SNo x6 ⟶ SNo x7 ⟶ c6963.. (bbc71.. x0 x1 x2 x3 x4 x5 x6 x7) = x1 (proof)
Theorem f91a2.. : ∀ x0 . 1eb0a.. x0 ⟶ and (SNo (a9894.. x0)) (∀ x1 : ο . (∀ x2 . and (SNo x2) (∀ x3 : ο . (∀ x4 . and (SNo x4) (∀ x5 : ο . (∀ x6 . and (SNo x6) (∀ x7 : ο . (∀ x8 . and (SNo x8) (∀ x9 : ο . (∀ x10 . and (SNo x10) (x0 = bbc71.. (8dd2c.. x0) (c6963.. x0) (a9894.. x0) x2 x4 x6 x8 x10) ⟶ x9) ⟶ x9) ⟶ x7) ⟶ x7) ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3) ⟶ x1) ⟶ x1) (proof)
Theorem 81e66.. : ∀ x0 . 1eb0a.. x0 ⟶ SNo (a9894.. x0) (proof)
Theorem a1757.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ SNo x5 ⟶ SNo x6 ⟶ SNo x7 ⟶ a9894.. (bbc71.. x0 x1 x2 x3 x4 x5 x6 x7) = x2 (proof)
Theorem 5715b.. : ∀ x0 . 1eb0a.. x0 ⟶ and (SNo (da724.. x0)) (∀ x1 : ο . (∀ x2 . and (SNo x2) (∀ x3 : ο . (∀ x4 . and (SNo x4) (∀ x5 : ο . (∀ x6 . and (SNo x6) (∀ x7 : ο . (∀ x8 . and (SNo x8) (x0 = bbc71.. (8dd2c.. x0) (c6963.. x0) (a9894.. x0) (da724.. x0) x2 x4 x6 x8) ⟶ x7) ⟶ x7) ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3) ⟶ x1) ⟶ x1) (proof)
Theorem 5281f.. : ∀ x0 . 1eb0a.. x0 ⟶ SNo (da724.. x0) (proof)
Theorem 289a1.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ SNo x5 ⟶ SNo x6 ⟶ SNo x7 ⟶ da724.. (bbc71.. x0 x1 x2 x3 x4 x5 x6 x7) = x3 (proof)
Theorem f2017.. : ∀ x0 . 1eb0a.. x0 ⟶ and (SNo (adebb.. x0)) (∀ x1 : ο . (∀ x2 . and (SNo x2) (∀ x3 : ο . (∀ x4 . and (SNo x4) (∀ x5 : ο . (∀ x6 . and (SNo x6) (x0 = bbc71.. (8dd2c.. x0) (c6963.. x0) (a9894.. x0) (da724.. x0) (adebb.. x0) x2 x4 x6) ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3) ⟶ x1) ⟶ x1) (proof)
Theorem a3b2d.. : ∀ x0 . 1eb0a.. x0 ⟶ SNo (adebb.. x0) (proof)
Theorem b270b.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ SNo x5 ⟶ SNo x6 ⟶ SNo x7 ⟶ adebb.. (bbc71.. x0 x1 x2 x3 x4 x5 x6 x7) = x4 (proof)
Theorem fd6e0.. : ∀ x0 . 1eb0a.. x0 ⟶ and (SNo (91922.. x0)) (∀ x1 : ο . (∀ x2 . and (SNo x2) (∀ x3 : ο . (∀ x4 . and (SNo x4) (x0 = bbc71.. (8dd2c.. x0) (c6963.. x0) (a9894.. x0) (da724.. x0) (adebb.. x0) (91922.. x0) x2 x4) ⟶ x3) ⟶ x3) ⟶ x1) ⟶ x1) (proof)
Theorem 692bd.. : ∀ x0 . 1eb0a.. x0 ⟶ SNo (91922.. x0) (proof)
Theorem 49c7e.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ SNo x5 ⟶ SNo x6 ⟶ SNo x7 ⟶ 91922.. (bbc71.. x0 x1 x2 x3 x4 x5 x6 x7) = x5 (proof)
Theorem 91074.. : ∀ x0 . 1eb0a.. x0 ⟶ and (SNo (b8e07.. x0)) (∀ x1 : ο . (∀ x2 . and (SNo x2) (x0 = bbc71.. (8dd2c.. x0) (c6963.. x0) (a9894.. x0) (da724.. x0) (adebb.. x0) (91922.. x0) (b8e07.. x0) x2) ⟶ x1) ⟶ x1) (proof)
Theorem 4eec6.. : ∀ x0 . 1eb0a.. x0 ⟶ SNo (b8e07.. x0) (proof)
Theorem 6c9e3.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ SNo x5 ⟶ SNo x6 ⟶ SNo x7 ⟶ b8e07.. (bbc71.. x0 x1 x2 x3 x4 x5 x6 x7) = x6 (proof)
Theorem 9fc1b.. : ∀ x0 . 1eb0a.. x0 ⟶ and (SNo (7f2e4.. x0)) (x0 = bbc71.. (8dd2c.. x0) (c6963.. x0) (a9894.. x0) (da724.. x0) (adebb.. x0) (91922.. x0) (b8e07.. x0) (7f2e4.. x0)) (proof)
Theorem b67dd.. : ∀ x0 . 1eb0a.. x0 ⟶ SNo (7f2e4.. x0) (proof)
Theorem c1dff.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ SNo x5 ⟶ SNo x6 ⟶ SNo x7 ⟶ 7f2e4.. (bbc71.. x0 x1 x2 x3 x4 x5 x6 x7) = x7 (proof)
Theorem b4523.. : ∀ x0 . 1eb0a.. x0 ⟶ x0 = bbc71.. (8dd2c.. x0) (c6963.. x0) (a9894.. x0) (da724.. x0) (adebb.. x0) (91922.. x0) (b8e07.. x0) (7f2e4.. x0) (proof)