Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrRJn../166cc..
PUe3N../ac628..
vout
PrRJn../62026.. 9.90 bars
TMHfp../bc053.. ownership of 212d5.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMK4Y../b2ecc.. ownership of 7c2f0.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMWbW../d17fb.. ownership of 95571.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMLRB../e4277.. ownership of 57b8e.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMXnR../255c6.. ownership of 340c0.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMc7q../73130.. ownership of 14a4e.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMVpd../5a868.. ownership of 48feb.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMK6q../1a96a.. ownership of 2e86c.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMcSR../f6eb4.. ownership of 0c70a.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMPLh../c1564.. ownership of 4271d.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMRnz../4b8dd.. ownership of 0b166.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMJZs../57740.. ownership of d4d9f.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMRep../1b57d.. ownership of c7d23.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMc6d../a04fe.. ownership of 5d3eb.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMGmB../20ed0.. ownership of 9599d.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMJTk../a7837.. ownership of 45530.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMKFT../c9f27.. ownership of 42518.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMZga../97e6a.. ownership of 026e3.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMJzZ../ae315.. ownership of 62fb0.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMRoR../9b662.. ownership of f7dd6.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMZ8d../82696.. ownership of 69bbd.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMXVj../41396.. ownership of 02fca.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMRp5../9aca3.. ownership of baa4b.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMGBT../7cd41.. ownership of 247af.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMGQN../04083.. ownership of 26f65.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMUE1../124c1.. ownership of ce924.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMWkZ../a4a26.. ownership of af528.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMTU4../55d4d.. ownership of 0b170.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMdXr../34db6.. ownership of 15adc.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMJne../8cfe4.. ownership of 6885b.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMPBZ../47abc.. ownership of 71a99.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMHto../89810.. ownership of 500fb.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMTD5../82f77.. ownership of 5e734.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMYZX../299df.. ownership of 4d8ab.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMFJW../14700.. ownership of 0a376.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMbjc../1e61d.. ownership of 8229c.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMNbY../a2eac.. ownership of 90339.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMSnB../6da3b.. ownership of 2d6ce.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMXpL../9f4c3.. ownership of 1131a.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMWoL../3ac23.. ownership of 69127.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMFnB../ac3b7.. ownership of 9b0e1.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMG2i../c16e1.. ownership of 95977.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMGjF../9e57f.. ownership of 33b4a.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMLFB../508eb.. ownership of b64a3.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMdLn../64efb.. ownership of fd099.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMcfP../bc673.. ownership of 90c9e.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMZEy../57a82.. ownership of 26f49.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMbad../6634b.. ownership of 35aad.. as prop with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMUif../bacc5.. ownership of 8dd2c.. as obj with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMKWq../a9b76.. ownership of efba5.. as obj with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMGNc../3162f.. ownership of 053de.. as obj with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMN2B../c49a0.. ownership of 170bf.. as obj with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMcpM../57153.. ownership of 717b4.. as obj with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMQgf../fa000.. ownership of 579bf.. as obj with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMZGm../e0f74.. ownership of 28f5a.. as obj with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMWf1../ccde3.. ownership of 91cba.. as obj with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMNBC../1d4a3.. ownership of 41ec1.. as obj with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMM7L../4b716.. ownership of 9166d.. as obj with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMdtw../ea6ff.. ownership of 8d7df.. as obj with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMHai../897b7.. ownership of e75aa.. as obj with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMRtX../9dc58.. ownership of 50208.. as obj with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMJZq../014fb.. ownership of 60027.. as obj with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMa8q../ad440.. ownership of d4639.. as obj with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
TMT3L../d48dd.. ownership of 01f77.. as obj with payaddr PrQUS.. rightscost 0.00 controlledby PrQUS.. upto 0
PUY4m../84f0e.. doc published by PrQUS..
Param SNoSNo : ι → ο
Definition andand := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Param bbc71.. : ι → ι → ι → ι → ι → ι → ι → ι → ι
Definition 1eb0a.. := λ 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) (∀ x15 : ο . (∀ x16 . and (SNo x16) (x0 = bbc71.. x2 x4 x6 x8 x10 x12 x14 x16) ⟶ x15) ⟶ x15) ⟶ x13) ⟶ x13) ⟶ x11) ⟶ x11) ⟶ x9) ⟶ x9) ⟶ x7) ⟶ x7) ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3) ⟶ x1) ⟶ x1
Known andIandI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Theorem 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) (proof)
Definition d4639.. := λ x0 : ι → ι . λ x1 . prim0 (λ 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) (x1 = bbc71.. (x0 x1) x2 x4 x6 x8 x10 x12 x14) ⟶ x13) ⟶ x13) ⟶ x11) ⟶ x11) ⟶ x9) ⟶ x9) ⟶ x7) ⟶ x7) ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3))
Known Eps_i_exEps_i_ex : ∀ x0 : ι → ο . (∀ x1 : ο . (∀ x2 . x0 x2 ⟶ x1) ⟶ x1) ⟶ x0 (prim0 x0)
Theorem 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) (proof)
Theorem 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) (proof)
Known babe8.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ SNo x5 ⟶ SNo x6 ⟶ SNo x7 ⟶ SNo x8 ⟶ SNo x9 ⟶ SNo x10 ⟶ SNo x11 ⟶ SNo x12 ⟶ SNo x13 ⟶ SNo x14 ⟶ SNo x15 ⟶ bbc71.. x0 x1 x2 x3 x4 x5 x6 x7 = bbc71.. x8 x9 x10 x11 x12 x13 x14 x15 ⟶ x1 = x9
Theorem 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 (proof)
Definition 50208.. := λ x0 x1 : ι → ι . λ x2 . prim0 (λ 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) (x2 = bbc71.. (x0 x2) (x1 x2) x3 x5 x7 x9 x11 x13) ⟶ x12) ⟶ x12) ⟶ x10) ⟶ x10) ⟶ x8) ⟶ x8) ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4))
Theorem 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) (proof)
Theorem 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) (proof)
Known 6488e.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ SNo x5 ⟶ SNo x6 ⟶ SNo x7 ⟶ SNo x8 ⟶ SNo x9 ⟶ SNo x10 ⟶ SNo x11 ⟶ SNo x12 ⟶ SNo x13 ⟶ SNo x14 ⟶ SNo x15 ⟶ bbc71.. x0 x1 x2 x3 x4 x5 x6 x7 = bbc71.. x8 x9 x10 x11 x12 x13 x14 x15 ⟶ x2 = x10
Theorem 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 (proof)
Definition 8d7df.. := λ x0 x1 x2 : ι → ι . λ x3 . prim0 (λ x4 . and (SNo x4) (∀ x5 : ο . (∀ x6 . and (SNo x6) (∀ x7 : ο . (∀ x8 . and (SNo x8) (∀ x9 : ο . (∀ x10 . and (SNo x10) (∀ x11 : ο . (∀ x12 . and (SNo x12) (x3 = bbc71.. (x0 x3) (x1 x3) (x2 x3) x4 x6 x8 x10 x12) ⟶ x11) ⟶ x11) ⟶ x9) ⟶ x9) ⟶ x7) ⟶ x7) ⟶ x5) ⟶ x5))
Theorem 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) (proof)
Theorem 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) (proof)
Known ad01a.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ SNo x5 ⟶ SNo x6 ⟶ SNo x7 ⟶ SNo x8 ⟶ SNo x9 ⟶ SNo x10 ⟶ SNo x11 ⟶ SNo x12 ⟶ SNo x13 ⟶ SNo x14 ⟶ SNo x15 ⟶ bbc71.. x0 x1 x2 x3 x4 x5 x6 x7 = bbc71.. x8 x9 x10 x11 x12 x13 x14 x15 ⟶ x3 = x11
Theorem 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 (proof)
Definition 41ec1.. := λ x0 x1 x2 x3 : ι → ι . λ x4 . prim0 (λ x5 . and (SNo x5) (∀ x6 : ο . (∀ x7 . and (SNo x7) (∀ x8 : ο . (∀ x9 . and (SNo x9) (∀ x10 : ο . (∀ x11 . and (SNo x11) (x4 = bbc71.. (x0 x4) (x1 x4) (x2 x4) (x3 x4) x5 x7 x9 x11) ⟶ x10) ⟶ x10) ⟶ x8) ⟶ x8) ⟶ x6) ⟶ x6))
Theorem 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) (proof)
Theorem 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) (proof)
Known f4559.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ SNo x5 ⟶ SNo x6 ⟶ SNo x7 ⟶ SNo x8 ⟶ SNo x9 ⟶ SNo x10 ⟶ SNo x11 ⟶ SNo x12 ⟶ SNo x13 ⟶ SNo x14 ⟶ SNo x15 ⟶ bbc71.. x0 x1 x2 x3 x4 x5 x6 x7 = bbc71.. x8 x9 x10 x11 x12 x13 x14 x15 ⟶ x4 = x12
Theorem 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 (proof)
Definition 28f5a.. := λ x0 x1 x2 x3 x4 : ι → ι . λ x5 . prim0 (λ x6 . and (SNo x6) (∀ x7 : ο . (∀ x8 . and (SNo x8) (∀ x9 : ο . (∀ x10 . and (SNo x10) (x5 = bbc71.. (x0 x5) (x1 x5) (x2 x5) (x3 x5) (x4 x5) x6 x8 x10) ⟶ x9) ⟶ x9) ⟶ x7) ⟶ x7))
Theorem 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) (proof)
Theorem 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) (proof)
Known f56fc.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ SNo x5 ⟶ SNo x6 ⟶ SNo x7 ⟶ SNo x8 ⟶ SNo x9 ⟶ SNo x10 ⟶ SNo x11 ⟶ SNo x12 ⟶ SNo x13 ⟶ SNo x14 ⟶ SNo x15 ⟶ bbc71.. x0 x1 x2 x3 x4 x5 x6 x7 = bbc71.. x8 x9 x10 x11 x12 x13 x14 x15 ⟶ x5 = x13
Theorem 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 (proof)
Definition 717b4.. := λ x0 x1 x2 x3 x4 x5 : ι → ι . λ x6 . prim0 (λ x7 . and (SNo x7) (∀ x8 : ο . (∀ x9 . and (SNo x9) (x6 = bbc71.. (x0 x6) (x1 x6) (x2 x6) (x3 x6) (x4 x6) (x5 x6) x7 x9) ⟶ x8) ⟶ x8))
Theorem 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) (proof)
Theorem 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) (proof)
Known 4a66b.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ SNo x5 ⟶ SNo x6 ⟶ SNo x7 ⟶ SNo x8 ⟶ SNo x9 ⟶ SNo x10 ⟶ SNo x11 ⟶ SNo x12 ⟶ SNo x13 ⟶ SNo x14 ⟶ SNo x15 ⟶ bbc71.. x0 x1 x2 x3 x4 x5 x6 x7 = bbc71.. x8 x9 x10 x11 x12 x13 x14 x15 ⟶ x6 = x14
Theorem 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 (proof)
Definition 053de.. := λ x0 x1 x2 x3 x4 x5 x6 : ι → ι . λ x7 . prim0 (λ x8 . and (SNo x8) (x7 = bbc71.. (x0 x7) (x1 x7) (x2 x7) (x3 x7) (x4 x7) (x5 x7) (x6 x7) x8))
Theorem 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)) (proof)
Theorem 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) (proof)
Known 7c302.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ SNo x5 ⟶ SNo x6 ⟶ SNo x7 ⟶ SNo x8 ⟶ SNo x9 ⟶ SNo x10 ⟶ SNo x11 ⟶ SNo x12 ⟶ SNo x13 ⟶ SNo x14 ⟶ SNo x15 ⟶ bbc71.. x0 x1 x2 x3 x4 x5 x6 x7 = bbc71.. x8 x9 x10 x11 x12 x13 x14 x15 ⟶ x7 = x15
Theorem 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 (proof)
Definition 8dd2c.. := λ x0 . prim0 (λ x1 . and (SNo 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) (x0 = bbc71.. x1 x3 x5 x7 x9 x11 x13 x15) ⟶ x14) ⟶ x14) ⟶ x12) ⟶ x12) ⟶ x10) ⟶ x10) ⟶ x8) ⟶ x8) ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2))
Theorem 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) (proof)
Theorem 95571.. : ∀ x0 . 1eb0a.. x0 ⟶ SNo (8dd2c.. x0) (proof)
Known cca09.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ SNo x5 ⟶ SNo x6 ⟶ SNo x7 ⟶ SNo x8 ⟶ SNo x9 ⟶ SNo x10 ⟶ SNo x11 ⟶ SNo x12 ⟶ SNo x13 ⟶ SNo x14 ⟶ SNo x15 ⟶ bbc71.. x0 x1 x2 x3 x4 x5 x6 x7 = bbc71.. x8 x9 x10 x11 x12 x13 x14 x15 ⟶ x0 = x8
Theorem 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 (proof)