Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrRJn../b558b..
PUR8p../3a6f8..
vout
PrRJn../62e69.. 9.89 bars
TMS3W../36d48.. ownership of b4523.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMcmF../0925c.. ownership of 3e746.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMNUb../a6806.. ownership of c1dff.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMQJ7../a7fc9.. ownership of 222db.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMJ4i../036fc.. ownership of b67dd.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMLbH../397a3.. ownership of 96dcc.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMdRa../f8614.. ownership of 9fc1b.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMXeY../5ad4c.. ownership of e6296.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMVwe../8e8bb.. ownership of 6c9e3.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMbXY../eeaf4.. ownership of e54e0.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMNEX../7f7eb.. ownership of 4eec6.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMFuz../c96af.. ownership of 690aa.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMHUV../28c17.. ownership of 91074.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMd16../0b27a.. ownership of 15d7f.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMExJ../ebf5f.. ownership of 49c7e.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMUUU../2a436.. ownership of 37a44.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMdku../52a39.. ownership of 692bd.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMd5J../e2617.. ownership of 214de.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMUNT../8f1ef.. ownership of fd6e0.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMVPH../2fd53.. ownership of 035b4.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMLTj../7a2d4.. ownership of b270b.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMMEv../94c5e.. ownership of 53995.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMcS9../325cf.. ownership of a3b2d.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMdTd../3d40f.. ownership of 51d5e.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMGye../a2d31.. ownership of f2017.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMbky../e2971.. ownership of 270bc.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMW4u../0a223.. ownership of 289a1.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMPfg../92a83.. ownership of 7b46a.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMXA5../c9ac6.. ownership of 5281f.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMRyk../86385.. ownership of 3c725.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMazw../d8e7a.. ownership of 5715b.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMKLC../b9748.. ownership of 1fb29.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMLj5../7dda5.. ownership of a1757.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMHbM../a454f.. ownership of 85109.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMWvQ../40a6b.. ownership of 81e66.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMcvm../a75b0.. ownership of 35207.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMPgB../28b9c.. ownership of f91a2.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMa4B../1e242.. ownership of d961c.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMKV5../a586f.. ownership of 58949.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMa4K../235cd.. ownership of 7bb12.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMU9t../b3140.. ownership of 675f4.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMExo../11243.. ownership of 50806.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMQGB../ffeb0.. ownership of 4b34b.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMLjF../7c584.. ownership of 61bcd.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMS2K../7e1a5.. ownership of 7f2e4.. as obj with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMSB3../93bb6.. ownership of 0562a.. as obj with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMceb../90eda.. ownership of b8e07.. as obj with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMJHU../0adf4.. ownership of be573.. as obj with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMHtT../410f2.. ownership of 91922.. as obj with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMPug../be666.. ownership of 58d0d.. as obj with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMFDq../bb66b.. ownership of adebb.. as obj with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMZNe../ae597.. ownership of 4d085.. as obj with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMMpb../d8ef3.. ownership of da724.. as obj with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMaQL../d5cea.. ownership of cc559.. as obj with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMXXK../a5c0c.. ownership of a9894.. as obj with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMGqi../67f51.. ownership of 3827e.. as obj with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMSQP../e09bc.. ownership of c6963.. as obj with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMGyg../b1ee7.. ownership of 9937c.. as obj with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
PUWiW../4f471.. doc published by PrQUS..
Param SNoSNo : ι → ο
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 andand := λ 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)