Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrPFB../0907d..
PUPo2../dd19e..
vout
PrPFB../fa92e.. 0.07 bars
TMJ6q../f6da8.. ownership of 3bb0e.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMXAu../0a674.. ownership of 1733a.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMQ3x../9079f.. ownership of 01f0f.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMbjg../c3eb7.. ownership of 9ac2f.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMG5e../05b6a.. ownership of 93614.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRhZ../ac70c.. ownership of 92850.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMSe9../defba.. ownership of 99402.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMTmt../97619.. ownership of 76fed.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMXhh../e3eb1.. ownership of 1d3b6.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMEpF../6dd0c.. ownership of 029be.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMcj5../a5235.. ownership of e72cf.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMQvF../4fbba.. ownership of 80213.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMHrJ../09763.. ownership of 56696.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMYZi../280a9.. ownership of 0e4b7.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMT1y../9025b.. ownership of 6f859.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMKm4../0f0f8.. ownership of 2ff2d.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMXEM../06c38.. ownership of 4feb2.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMWho../f6c6e.. ownership of 1594b.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRPV../504e0.. ownership of ea5da.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMVtD../28564.. ownership of 4af86.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMcvx../050b8.. ownership of e5e84.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMGZ1../33913.. ownership of d4c19.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMZY9../1427b.. ownership of 98e52.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMLRz../81c6a.. ownership of 00995.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMPjw../8e99c.. ownership of f5575.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMFUm../cd8b2.. ownership of 08c3a.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMGXP../063a7.. ownership of e894a.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMUQ2../148c3.. ownership of 7d971.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMSr6../8e3bf.. ownership of badf6.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMc5U../44a3c.. ownership of 6a6b4.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMR73../18291.. ownership of 33130.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMQMU../6c400.. ownership of 909e5.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMZtZ../89920.. ownership of ef640.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMU7R../08e6a.. ownership of 067b5.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMFEf../b7513.. ownership of 0bb81.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMZva../235fa.. ownership of 8cd44.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMNrA../f6de2.. ownership of 0b692.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMV65../34239.. ownership of b4f6b.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMUwP../fcd9d.. ownership of 342cc.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMa2Z../e86c9.. ownership of f9492.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMaFG../f0f87.. ownership of f6176.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMYYy../7b664.. ownership of e17e5.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMKPH../7c390.. ownership of 46112.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMQ7b../780b8.. ownership of a5e15.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMWJF../f14ea.. ownership of 9d539.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMJYd../f32ba.. ownership of f98a9.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
PUJrJ../e3248.. doc published by PrGxv..
Param SNoSNo : ι → ο
Param add_SNoadd_SNo : ι → ι → ι
Known SNo_add_SNoSNo_add_SNo : ∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ SNo (add_SNo x0 x1)
Known SNo_add_SNo_30SNo_add_SNo_30 : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 . 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 ⟶ SNo x16 ⟶ SNo x17 ⟶ SNo x18 ⟶ SNo x19 ⟶ SNo x20 ⟶ SNo x21 ⟶ SNo x22 ⟶ SNo x23 ⟶ SNo x24 ⟶ SNo x25 ⟶ SNo x26 ⟶ SNo x27 ⟶ SNo x28 ⟶ SNo x29 ⟶ SNo (add_SNo x0 (add_SNo x1 (add_SNo x2 (add_SNo x3 (add_SNo x4 (add_SNo x5 (add_SNo x6 (add_SNo x7 (add_SNo x8 (add_SNo x9 (add_SNo x10 (add_SNo x11 (add_SNo x12 (add_SNo x13 (add_SNo x14 (add_SNo x15 (add_SNo x16 (add_SNo x17 (add_SNo x18 (add_SNo x19 (add_SNo x20 (add_SNo x21 (add_SNo x22 (add_SNo x23 (add_SNo x24 (add_SNo x25 (add_SNo x26 (add_SNo x27 (add_SNo x28 x29)))))))))))))))))))))))))))))
Theorem 9d539.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 . 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 ⟶ SNo x16 ⟶ SNo x17 ⟶ SNo x18 ⟶ SNo x19 ⟶ SNo x20 ⟶ SNo x21 ⟶ SNo x22 ⟶ SNo x23 ⟶ SNo x24 ⟶ SNo x25 ⟶ SNo x26 ⟶ SNo x27 ⟶ SNo x28 ⟶ SNo x29 ⟶ SNo x30 ⟶ SNo (add_SNo x0 (add_SNo x1 (add_SNo x2 (add_SNo x3 (add_SNo x4 (add_SNo x5 (add_SNo x6 (add_SNo x7 (add_SNo x8 (add_SNo x9 (add_SNo x10 (add_SNo x11 (add_SNo x12 (add_SNo x13 (add_SNo x14 (add_SNo x15 (add_SNo x16 (add_SNo x17 (add_SNo x18 (add_SNo x19 (add_SNo x20 (add_SNo x21 (add_SNo x22 (add_SNo x23 (add_SNo x24 (add_SNo x25 (add_SNo x26 (add_SNo x27 (add_SNo x28 (add_SNo x29 x30)))))))))))))))))))))))))))))) (proof)
Theorem 46112.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 . 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 ⟶ SNo x16 ⟶ SNo x17 ⟶ SNo x18 ⟶ SNo x19 ⟶ SNo x20 ⟶ SNo x21 ⟶ SNo x22 ⟶ SNo x23 ⟶ SNo x24 ⟶ SNo x25 ⟶ SNo x26 ⟶ SNo x27 ⟶ SNo x28 ⟶ SNo x29 ⟶ SNo x30 ⟶ SNo x31 ⟶ SNo (add_SNo x0 (add_SNo x1 (add_SNo x2 (add_SNo x3 (add_SNo x4 (add_SNo x5 (add_SNo x6 (add_SNo x7 (add_SNo x8 (add_SNo x9 (add_SNo x10 (add_SNo x11 (add_SNo x12 (add_SNo x13 (add_SNo x14 (add_SNo x15 (add_SNo x16 (add_SNo x17 (add_SNo x18 (add_SNo x19 (add_SNo x20 (add_SNo x21 (add_SNo x22 (add_SNo x23 (add_SNo x24 (add_SNo x25 (add_SNo x26 (add_SNo x27 (add_SNo x28 (add_SNo x29 (add_SNo x30 x31))))))))))))))))))))))))))))))) (proof)
Theorem f6176.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 . 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 ⟶ SNo x16 ⟶ SNo x17 ⟶ SNo x18 ⟶ SNo x19 ⟶ SNo x20 ⟶ SNo x21 ⟶ SNo x22 ⟶ SNo x23 ⟶ SNo x24 ⟶ SNo x25 ⟶ SNo x26 ⟶ SNo x27 ⟶ SNo x28 ⟶ SNo x29 ⟶ SNo x30 ⟶ SNo x31 ⟶ SNo x32 ⟶ SNo (add_SNo x0 (add_SNo x1 (add_SNo x2 (add_SNo x3 (add_SNo x4 (add_SNo x5 (add_SNo x6 (add_SNo x7 (add_SNo x8 (add_SNo x9 (add_SNo x10 (add_SNo x11 (add_SNo x12 (add_SNo x13 (add_SNo x14 (add_SNo x15 (add_SNo x16 (add_SNo x17 (add_SNo x18 (add_SNo x19 (add_SNo x20 (add_SNo x21 (add_SNo x22 (add_SNo x23 (add_SNo x24 (add_SNo x25 (add_SNo x26 (add_SNo x27 (add_SNo x28 (add_SNo x29 (add_SNo x30 (add_SNo x31 x32)))))))))))))))))))))))))))))))) (proof)
Theorem 342cc.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 x33 . 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 ⟶ SNo x16 ⟶ SNo x17 ⟶ SNo x18 ⟶ SNo x19 ⟶ SNo x20 ⟶ SNo x21 ⟶ SNo x22 ⟶ SNo x23 ⟶ SNo x24 ⟶ SNo x25 ⟶ SNo x26 ⟶ SNo x27 ⟶ SNo x28 ⟶ SNo x29 ⟶ SNo x30 ⟶ SNo x31 ⟶ SNo x32 ⟶ SNo x33 ⟶ SNo (add_SNo x0 (add_SNo x1 (add_SNo x2 (add_SNo x3 (add_SNo x4 (add_SNo x5 (add_SNo x6 (add_SNo x7 (add_SNo x8 (add_SNo x9 (add_SNo x10 (add_SNo x11 (add_SNo x12 (add_SNo x13 (add_SNo x14 (add_SNo x15 (add_SNo x16 (add_SNo x17 (add_SNo x18 (add_SNo x19 (add_SNo x20 (add_SNo x21 (add_SNo x22 (add_SNo x23 (add_SNo x24 (add_SNo x25 (add_SNo x26 (add_SNo x27 (add_SNo x28 (add_SNo x29 (add_SNo x30 (add_SNo x31 (add_SNo x32 x33))))))))))))))))))))))))))))))))) (proof)
Theorem 0b692.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 x33 x34 . 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 ⟶ SNo x16 ⟶ SNo x17 ⟶ SNo x18 ⟶ SNo x19 ⟶ SNo x20 ⟶ SNo x21 ⟶ SNo x22 ⟶ SNo x23 ⟶ SNo x24 ⟶ SNo x25 ⟶ SNo x26 ⟶ SNo x27 ⟶ SNo x28 ⟶ SNo x29 ⟶ SNo x30 ⟶ SNo x31 ⟶ SNo x32 ⟶ SNo x33 ⟶ SNo x34 ⟶ SNo (add_SNo x0 (add_SNo x1 (add_SNo x2 (add_SNo x3 (add_SNo x4 (add_SNo x5 (add_SNo x6 (add_SNo x7 (add_SNo x8 (add_SNo x9 (add_SNo x10 (add_SNo x11 (add_SNo x12 (add_SNo x13 (add_SNo x14 (add_SNo x15 (add_SNo x16 (add_SNo x17 (add_SNo x18 (add_SNo x19 (add_SNo x20 (add_SNo x21 (add_SNo x22 (add_SNo x23 (add_SNo x24 (add_SNo x25 (add_SNo x26 (add_SNo x27 (add_SNo x28 (add_SNo x29 (add_SNo x30 (add_SNo x31 (add_SNo x32 (add_SNo x33 x34)))))))))))))))))))))))))))))))))) (proof)
Theorem 0bb81.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 x33 x34 x35 . 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 ⟶ SNo x16 ⟶ SNo x17 ⟶ SNo x18 ⟶ SNo x19 ⟶ SNo x20 ⟶ SNo x21 ⟶ SNo x22 ⟶ SNo x23 ⟶ SNo x24 ⟶ SNo x25 ⟶ SNo x26 ⟶ SNo x27 ⟶ SNo x28 ⟶ SNo x29 ⟶ SNo x30 ⟶ SNo x31 ⟶ SNo x32 ⟶ SNo x33 ⟶ SNo x34 ⟶ SNo x35 ⟶ SNo (add_SNo x0 (add_SNo x1 (add_SNo x2 (add_SNo x3 (add_SNo x4 (add_SNo x5 (add_SNo x6 (add_SNo x7 (add_SNo x8 (add_SNo x9 (add_SNo x10 (add_SNo x11 (add_SNo x12 (add_SNo x13 (add_SNo x14 (add_SNo x15 (add_SNo x16 (add_SNo x17 (add_SNo x18 (add_SNo x19 (add_SNo x20 (add_SNo x21 (add_SNo x22 (add_SNo x23 (add_SNo x24 (add_SNo x25 (add_SNo x26 (add_SNo x27 (add_SNo x28 (add_SNo x29 (add_SNo x30 (add_SNo x31 (add_SNo x32 (add_SNo x33 (add_SNo x34 x35))))))))))))))))))))))))))))))))))) (proof)
Theorem ef640.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 x33 x34 x35 x36 . 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 ⟶ SNo x16 ⟶ SNo x17 ⟶ SNo x18 ⟶ SNo x19 ⟶ SNo x20 ⟶ SNo x21 ⟶ SNo x22 ⟶ SNo x23 ⟶ SNo x24 ⟶ SNo x25 ⟶ SNo x26 ⟶ SNo x27 ⟶ SNo x28 ⟶ SNo x29 ⟶ SNo x30 ⟶ SNo x31 ⟶ SNo x32 ⟶ SNo x33 ⟶ SNo x34 ⟶ SNo x35 ⟶ SNo x36 ⟶ SNo (add_SNo x0 (add_SNo x1 (add_SNo x2 (add_SNo x3 (add_SNo x4 (add_SNo x5 (add_SNo x6 (add_SNo x7 (add_SNo x8 (add_SNo x9 (add_SNo x10 (add_SNo x11 (add_SNo x12 (add_SNo x13 (add_SNo x14 (add_SNo x15 (add_SNo x16 (add_SNo x17 (add_SNo x18 (add_SNo x19 (add_SNo x20 (add_SNo x21 (add_SNo x22 (add_SNo x23 (add_SNo x24 (add_SNo x25 (add_SNo x26 (add_SNo x27 (add_SNo x28 (add_SNo x29 (add_SNo x30 (add_SNo x31 (add_SNo x32 (add_SNo x33 (add_SNo x34 (add_SNo x35 x36)))))))))))))))))))))))))))))))))))) (proof)
Theorem 33130.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 x33 x34 x35 x36 x37 . 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 ⟶ SNo x16 ⟶ SNo x17 ⟶ SNo x18 ⟶ SNo x19 ⟶ SNo x20 ⟶ SNo x21 ⟶ SNo x22 ⟶ SNo x23 ⟶ SNo x24 ⟶ SNo x25 ⟶ SNo x26 ⟶ SNo x27 ⟶ SNo x28 ⟶ SNo x29 ⟶ SNo x30 ⟶ SNo x31 ⟶ SNo x32 ⟶ SNo x33 ⟶ SNo x34 ⟶ SNo x35 ⟶ SNo x36 ⟶ SNo x37 ⟶ SNo (add_SNo x0 (add_SNo x1 (add_SNo x2 (add_SNo x3 (add_SNo x4 (add_SNo x5 (add_SNo x6 (add_SNo x7 (add_SNo x8 (add_SNo x9 (add_SNo x10 (add_SNo x11 (add_SNo x12 (add_SNo x13 (add_SNo x14 (add_SNo x15 (add_SNo x16 (add_SNo x17 (add_SNo x18 (add_SNo x19 (add_SNo x20 (add_SNo x21 (add_SNo x22 (add_SNo x23 (add_SNo x24 (add_SNo x25 (add_SNo x26 (add_SNo x27 (add_SNo x28 (add_SNo x29 (add_SNo x30 (add_SNo x31 (add_SNo x32 (add_SNo x33 (add_SNo x34 (add_SNo x35 (add_SNo x36 x37))))))))))))))))))))))))))))))))))))) (proof)
Theorem badf6.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 x33 x34 x35 x36 x37 x38 . 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 ⟶ SNo x16 ⟶ SNo x17 ⟶ SNo x18 ⟶ SNo x19 ⟶ SNo x20 ⟶ SNo x21 ⟶ SNo x22 ⟶ SNo x23 ⟶ SNo x24 ⟶ SNo x25 ⟶ SNo x26 ⟶ SNo x27 ⟶ SNo x28 ⟶ SNo x29 ⟶ SNo x30 ⟶ SNo x31 ⟶ SNo x32 ⟶ SNo x33 ⟶ SNo x34 ⟶ SNo x35 ⟶ SNo x36 ⟶ SNo x37 ⟶ SNo x38 ⟶ SNo (add_SNo x0 (add_SNo x1 (add_SNo x2 (add_SNo x3 (add_SNo x4 (add_SNo x5 (add_SNo x6 (add_SNo x7 (add_SNo x8 (add_SNo x9 (add_SNo x10 (add_SNo x11 (add_SNo x12 (add_SNo x13 (add_SNo x14 (add_SNo x15 (add_SNo x16 (add_SNo x17 (add_SNo x18 (add_SNo x19 (add_SNo x20 (add_SNo x21 (add_SNo x22 (add_SNo x23 (add_SNo x24 (add_SNo x25 (add_SNo x26 (add_SNo x27 (add_SNo x28 (add_SNo x29 (add_SNo x30 (add_SNo x31 (add_SNo x32 (add_SNo x33 (add_SNo x34 (add_SNo x35 (add_SNo x36 (add_SNo x37 x38)))))))))))))))))))))))))))))))))))))) (proof)
Theorem e894a.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 x33 x34 x35 x36 x37 x38 x39 . 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 ⟶ SNo x16 ⟶ SNo x17 ⟶ SNo x18 ⟶ SNo x19 ⟶ SNo x20 ⟶ SNo x21 ⟶ SNo x22 ⟶ SNo x23 ⟶ SNo x24 ⟶ SNo x25 ⟶ SNo x26 ⟶ SNo x27 ⟶ SNo x28 ⟶ SNo x29 ⟶ SNo x30 ⟶ SNo x31 ⟶ SNo x32 ⟶ SNo x33 ⟶ SNo x34 ⟶ SNo x35 ⟶ SNo x36 ⟶ SNo x37 ⟶ SNo x38 ⟶ SNo x39 ⟶ SNo (add_SNo x0 (add_SNo x1 (add_SNo x2 (add_SNo x3 (add_SNo x4 (add_SNo x5 (add_SNo x6 (add_SNo x7 (add_SNo x8 (add_SNo x9 (add_SNo x10 (add_SNo x11 (add_SNo x12 (add_SNo x13 (add_SNo x14 (add_SNo x15 (add_SNo x16 (add_SNo x17 (add_SNo x18 (add_SNo x19 (add_SNo x20 (add_SNo x21 (add_SNo x22 (add_SNo x23 (add_SNo x24 (add_SNo x25 (add_SNo x26 (add_SNo x27 (add_SNo x28 (add_SNo x29 (add_SNo x30 (add_SNo x31 (add_SNo x32 (add_SNo x33 (add_SNo x34 (add_SNo x35 (add_SNo x36 (add_SNo x37 (add_SNo x38 x39))))))))))))))))))))))))))))))))))))))) (proof)
Theorem f5575.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 x33 x34 x35 x36 x37 x38 x39 x40 . 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 ⟶ SNo x16 ⟶ SNo x17 ⟶ SNo x18 ⟶ SNo x19 ⟶ SNo x20 ⟶ SNo x21 ⟶ SNo x22 ⟶ SNo x23 ⟶ SNo x24 ⟶ SNo x25 ⟶ SNo x26 ⟶ SNo x27 ⟶ SNo x28 ⟶ SNo x29 ⟶ SNo x30 ⟶ SNo x31 ⟶ SNo x32 ⟶ SNo x33 ⟶ SNo x34 ⟶ SNo x35 ⟶ SNo x36 ⟶ SNo x37 ⟶ SNo x38 ⟶ SNo x39 ⟶ SNo x40 ⟶ SNo (add_SNo x0 (add_SNo x1 (add_SNo x2 (add_SNo x3 (add_SNo x4 (add_SNo x5 (add_SNo x6 (add_SNo x7 (add_SNo x8 (add_SNo x9 (add_SNo x10 (add_SNo x11 (add_SNo x12 (add_SNo x13 (add_SNo x14 (add_SNo x15 (add_SNo x16 (add_SNo x17 (add_SNo x18 (add_SNo x19 (add_SNo x20 (add_SNo x21 (add_SNo x22 (add_SNo x23 (add_SNo x24 (add_SNo x25 (add_SNo x26 (add_SNo x27 (add_SNo x28 (add_SNo x29 (add_SNo x30 (add_SNo x31 (add_SNo x32 (add_SNo x33 (add_SNo x34 (add_SNo x35 (add_SNo x36 (add_SNo x37 (add_SNo x38 (add_SNo x39 x40)))))))))))))))))))))))))))))))))))))))) (proof)
Param minus_SNominus_SNo : ι → ι
Known minus_add_SNo_distr_m_30minus_add_SNo_distr_m_30 : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 . 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 ⟶ SNo x16 ⟶ SNo x17 ⟶ SNo x18 ⟶ SNo x19 ⟶ SNo x20 ⟶ SNo x21 ⟶ SNo x22 ⟶ SNo x23 ⟶ SNo x24 ⟶ SNo x25 ⟶ SNo x26 ⟶ SNo x27 ⟶ SNo x28 ⟶ SNo x29 ⟶ SNo x30 ⟶ minus_SNo (add_SNo (minus_SNo x0) (add_SNo (minus_SNo x1) (add_SNo (minus_SNo x2) (add_SNo (minus_SNo x3) (add_SNo (minus_SNo x4) (add_SNo (minus_SNo x5) (add_SNo (minus_SNo x6) (add_SNo (minus_SNo x7) (add_SNo (minus_SNo x8) (add_SNo (minus_SNo x9) (add_SNo (minus_SNo x10) (add_SNo (minus_SNo x11) (add_SNo (minus_SNo x12) (add_SNo (minus_SNo x13) (add_SNo (minus_SNo x14) (add_SNo (minus_SNo x15) (add_SNo (minus_SNo x16) (add_SNo (minus_SNo x17) (add_SNo (minus_SNo x18) (add_SNo (minus_SNo x19) (add_SNo (minus_SNo x20) (add_SNo (minus_SNo x21) (add_SNo (minus_SNo x22) (add_SNo (minus_SNo x23) (add_SNo (minus_SNo x24) (add_SNo (minus_SNo x25) (add_SNo (minus_SNo x26) (add_SNo (minus_SNo x27) (add_SNo (minus_SNo x28) (add_SNo (minus_SNo x29) x30)))))))))))))))))))))))))))))) = add_SNo x0 (add_SNo x1 (add_SNo x2 (add_SNo x3 (add_SNo x4 (add_SNo x5 (add_SNo x6 (add_SNo x7 (add_SNo x8 (add_SNo x9 (add_SNo x10 (add_SNo x11 (add_SNo x12 (add_SNo x13 (add_SNo x14 (add_SNo x15 (add_SNo x16 (add_SNo x17 (add_SNo x18 (add_SNo x19 (add_SNo x20 (add_SNo x21 (add_SNo x22 (add_SNo x23 (add_SNo x24 (add_SNo x25 (add_SNo x26 (add_SNo x27 (add_SNo x28 (add_SNo x29 (minus_SNo x30))))))))))))))))))))))))))))))
Known SNo_minus_SNoSNo_minus_SNo : ∀ x0 . SNo x0 ⟶ SNo (minus_SNo x0)
Known minus_add_SNo_distr_mminus_add_SNo_distr_m : ∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ minus_SNo (add_SNo (minus_SNo x0) x1) = add_SNo x0 (minus_SNo x1)
Theorem 98e52.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 . 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 ⟶ SNo x16 ⟶ SNo x17 ⟶ SNo x18 ⟶ SNo x19 ⟶ SNo x20 ⟶ SNo x21 ⟶ SNo x22 ⟶ SNo x23 ⟶ SNo x24 ⟶ SNo x25 ⟶ SNo x26 ⟶ SNo x27 ⟶ SNo x28 ⟶ SNo x29 ⟶ SNo x30 ⟶ SNo x31 ⟶ minus_SNo (add_SNo (minus_SNo x0) (add_SNo (minus_SNo x1) (add_SNo (minus_SNo x2) (add_SNo (minus_SNo x3) (add_SNo (minus_SNo x4) (add_SNo (minus_SNo x5) (add_SNo (minus_SNo x6) (add_SNo (minus_SNo x7) (add_SNo (minus_SNo x8) (add_SNo (minus_SNo x9) (add_SNo (minus_SNo x10) (add_SNo (minus_SNo x11) (add_SNo (minus_SNo x12) (add_SNo (minus_SNo x13) (add_SNo (minus_SNo x14) (add_SNo (minus_SNo x15) (add_SNo (minus_SNo x16) (add_SNo (minus_SNo x17) (add_SNo (minus_SNo x18) (add_SNo (minus_SNo x19) (add_SNo (minus_SNo x20) (add_SNo (minus_SNo x21) (add_SNo (minus_SNo x22) (add_SNo (minus_SNo x23) (add_SNo (minus_SNo x24) (add_SNo (minus_SNo x25) (add_SNo (minus_SNo x26) (add_SNo (minus_SNo x27) (add_SNo (minus_SNo x28) (add_SNo (minus_SNo x29) (add_SNo (minus_SNo x30) x31))))))))))))))))))))))))))))))) = add_SNo x0 (add_SNo x1 (add_SNo x2 (add_SNo x3 (add_SNo x4 (add_SNo x5 (add_SNo x6 (add_SNo x7 (add_SNo x8 (add_SNo x9 (add_SNo x10 (add_SNo x11 (add_SNo x12 (add_SNo x13 (add_SNo x14 (add_SNo x15 (add_SNo x16 (add_SNo x17 (add_SNo x18 (add_SNo x19 (add_SNo x20 (add_SNo x21 (add_SNo x22 (add_SNo x23 (add_SNo x24 (add_SNo x25 (add_SNo x26 (add_SNo x27 (add_SNo x28 (add_SNo x29 (add_SNo x30 (minus_SNo x31))))))))))))))))))))))))))))))) (proof)
Theorem e5e84.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 . 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 ⟶ SNo x16 ⟶ SNo x17 ⟶ SNo x18 ⟶ SNo x19 ⟶ SNo x20 ⟶ SNo x21 ⟶ SNo x22 ⟶ SNo x23 ⟶ SNo x24 ⟶ SNo x25 ⟶ SNo x26 ⟶ SNo x27 ⟶ SNo x28 ⟶ SNo x29 ⟶ SNo x30 ⟶ SNo x31 ⟶ SNo x32 ⟶ minus_SNo (add_SNo (minus_SNo x0) (add_SNo (minus_SNo x1) (add_SNo (minus_SNo x2) (add_SNo (minus_SNo x3) (add_SNo (minus_SNo x4) (add_SNo (minus_SNo x5) (add_SNo (minus_SNo x6) (add_SNo (minus_SNo x7) (add_SNo (minus_SNo x8) (add_SNo (minus_SNo x9) (add_SNo (minus_SNo x10) (add_SNo (minus_SNo x11) (add_SNo (minus_SNo x12) (add_SNo (minus_SNo x13) (add_SNo (minus_SNo x14) (add_SNo (minus_SNo x15) (add_SNo (minus_SNo x16) (add_SNo (minus_SNo x17) (add_SNo (minus_SNo x18) (add_SNo (minus_SNo x19) (add_SNo (minus_SNo x20) (add_SNo (minus_SNo x21) (add_SNo (minus_SNo x22) (add_SNo (minus_SNo x23) (add_SNo (minus_SNo x24) (add_SNo (minus_SNo x25) (add_SNo (minus_SNo x26) (add_SNo (minus_SNo x27) (add_SNo (minus_SNo x28) (add_SNo (minus_SNo x29) (add_SNo (minus_SNo x30) (add_SNo (minus_SNo x31) x32)))))))))))))))))))))))))))))))) = add_SNo x0 (add_SNo x1 (add_SNo x2 (add_SNo x3 (add_SNo x4 (add_SNo x5 (add_SNo x6 (add_SNo x7 (add_SNo x8 (add_SNo x9 (add_SNo x10 (add_SNo x11 (add_SNo x12 (add_SNo x13 (add_SNo x14 (add_SNo x15 (add_SNo x16 (add_SNo x17 (add_SNo x18 (add_SNo x19 (add_SNo x20 (add_SNo x21 (add_SNo x22 (add_SNo x23 (add_SNo x24 (add_SNo x25 (add_SNo x26 (add_SNo x27 (add_SNo x28 (add_SNo x29 (add_SNo x30 (add_SNo x31 (minus_SNo x32)))))))))))))))))))))))))))))))) (proof)
Theorem ea5da.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 x33 . 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 ⟶ SNo x16 ⟶ SNo x17 ⟶ SNo x18 ⟶ SNo x19 ⟶ SNo x20 ⟶ SNo x21 ⟶ SNo x22 ⟶ SNo x23 ⟶ SNo x24 ⟶ SNo x25 ⟶ SNo x26 ⟶ SNo x27 ⟶ SNo x28 ⟶ SNo x29 ⟶ SNo x30 ⟶ SNo x31 ⟶ SNo x32 ⟶ SNo x33 ⟶ minus_SNo (add_SNo (minus_SNo x0) (add_SNo (minus_SNo x1) (add_SNo (minus_SNo x2) (add_SNo (minus_SNo x3) (add_SNo (minus_SNo x4) (add_SNo (minus_SNo x5) (add_SNo (minus_SNo x6) (add_SNo (minus_SNo x7) (add_SNo (minus_SNo x8) (add_SNo (minus_SNo x9) (add_SNo (minus_SNo x10) (add_SNo (minus_SNo x11) (add_SNo (minus_SNo x12) (add_SNo (minus_SNo x13) (add_SNo (minus_SNo x14) (add_SNo (minus_SNo x15) (add_SNo (minus_SNo x16) (add_SNo (minus_SNo x17) (add_SNo (minus_SNo x18) (add_SNo (minus_SNo x19) (add_SNo (minus_SNo x20) (add_SNo (minus_SNo x21) (add_SNo (minus_SNo x22) (add_SNo (minus_SNo x23) (add_SNo (minus_SNo x24) (add_SNo (minus_SNo x25) (add_SNo (minus_SNo x26) (add_SNo (minus_SNo x27) (add_SNo (minus_SNo x28) (add_SNo (minus_SNo x29) (add_SNo (minus_SNo x30) (add_SNo (minus_SNo x31) (add_SNo (minus_SNo x32) x33))))))))))))))))))))))))))))))))) = add_SNo x0 (add_SNo x1 (add_SNo x2 (add_SNo x3 (add_SNo x4 (add_SNo x5 (add_SNo x6 (add_SNo x7 (add_SNo x8 (add_SNo x9 (add_SNo x10 (add_SNo x11 (add_SNo x12 (add_SNo x13 (add_SNo x14 (add_SNo x15 (add_SNo x16 (add_SNo x17 (add_SNo x18 (add_SNo x19 (add_SNo x20 (add_SNo x21 (add_SNo x22 (add_SNo x23 (add_SNo x24 (add_SNo x25 (add_SNo x26 (add_SNo x27 (add_SNo x28 (add_SNo x29 (add_SNo x30 (add_SNo x31 (add_SNo x32 (minus_SNo x33))))))))))))))))))))))))))))))))) (proof)
Theorem 4feb2.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 x33 x34 . 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 ⟶ SNo x16 ⟶ SNo x17 ⟶ SNo x18 ⟶ SNo x19 ⟶ SNo x20 ⟶ SNo x21 ⟶ SNo x22 ⟶ SNo x23 ⟶ SNo x24 ⟶ SNo x25 ⟶ SNo x26 ⟶ SNo x27 ⟶ SNo x28 ⟶ SNo x29 ⟶ SNo x30 ⟶ SNo x31 ⟶ SNo x32 ⟶ SNo x33 ⟶ SNo x34 ⟶ minus_SNo (add_SNo (minus_SNo x0) (add_SNo (minus_SNo x1) (add_SNo (minus_SNo x2) (add_SNo (minus_SNo x3) (add_SNo (minus_SNo x4) (add_SNo (minus_SNo x5) (add_SNo (minus_SNo x6) (add_SNo (minus_SNo x7) (add_SNo (minus_SNo x8) (add_SNo (minus_SNo x9) (add_SNo (minus_SNo x10) (add_SNo (minus_SNo x11) (add_SNo (minus_SNo x12) (add_SNo (minus_SNo x13) (add_SNo (minus_SNo x14) (add_SNo (minus_SNo x15) (add_SNo (minus_SNo x16) (add_SNo (minus_SNo x17) (add_SNo (minus_SNo x18) (add_SNo (minus_SNo x19) (add_SNo (minus_SNo x20) (add_SNo (minus_SNo x21) (add_SNo (minus_SNo x22) (add_SNo (minus_SNo x23) (add_SNo (minus_SNo x24) (add_SNo (minus_SNo x25) (add_SNo (minus_SNo x26) (add_SNo (minus_SNo x27) (add_SNo (minus_SNo x28) (add_SNo (minus_SNo x29) (add_SNo (minus_SNo x30) (add_SNo (minus_SNo x31) (add_SNo (minus_SNo x32) (add_SNo (minus_SNo x33) x34)))))))))))))))))))))))))))))))))) = add_SNo x0 (add_SNo x1 (add_SNo x2 (add_SNo x3 (add_SNo x4 (add_SNo x5 (add_SNo x6 (add_SNo x7 (add_SNo x8 (add_SNo x9 (add_SNo x10 (add_SNo x11 (add_SNo x12 (add_SNo x13 (add_SNo x14 (add_SNo x15 (add_SNo x16 (add_SNo x17 (add_SNo x18 (add_SNo x19 (add_SNo x20 (add_SNo x21 (add_SNo x22 (add_SNo x23 (add_SNo x24 (add_SNo x25 (add_SNo x26 (add_SNo x27 (add_SNo x28 (add_SNo x29 (add_SNo x30 (add_SNo x31 (add_SNo x32 (add_SNo x33 (minus_SNo x34)))))))))))))))))))))))))))))))))) (proof)
Theorem 6f859.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 x33 x34 x35 . 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 ⟶ SNo x16 ⟶ SNo x17 ⟶ SNo x18 ⟶ SNo x19 ⟶ SNo x20 ⟶ SNo x21 ⟶ SNo x22 ⟶ SNo x23 ⟶ SNo x24 ⟶ SNo x25 ⟶ SNo x26 ⟶ SNo x27 ⟶ SNo x28 ⟶ SNo x29 ⟶ SNo x30 ⟶ SNo x31 ⟶ SNo x32 ⟶ SNo x33 ⟶ SNo x34 ⟶ SNo x35 ⟶ minus_SNo (add_SNo (minus_SNo x0) (add_SNo (minus_SNo x1) (add_SNo (minus_SNo x2) (add_SNo (minus_SNo x3) (add_SNo (minus_SNo x4) (add_SNo (minus_SNo x5) (add_SNo (minus_SNo x6) (add_SNo (minus_SNo x7) (add_SNo (minus_SNo x8) (add_SNo (minus_SNo x9) (add_SNo (minus_SNo x10) (add_SNo (minus_SNo x11) (add_SNo (minus_SNo x12) (add_SNo (minus_SNo x13) (add_SNo (minus_SNo x14) (add_SNo (minus_SNo x15) (add_SNo (minus_SNo x16) (add_SNo (minus_SNo x17) (add_SNo (minus_SNo x18) (add_SNo (minus_SNo x19) (add_SNo (minus_SNo x20) (add_SNo (minus_SNo x21) (add_SNo (minus_SNo x22) (add_SNo (minus_SNo x23) (add_SNo (minus_SNo x24) (add_SNo (minus_SNo x25) (add_SNo (minus_SNo x26) (add_SNo (minus_SNo x27) (add_SNo (minus_SNo x28) (add_SNo (minus_SNo x29) (add_SNo (minus_SNo x30) (add_SNo (minus_SNo x31) (add_SNo (minus_SNo x32) (add_SNo (minus_SNo x33) (add_SNo (minus_SNo x34) x35))))))))))))))))))))))))))))))))))) = add_SNo x0 (add_SNo x1 (add_SNo x2 (add_SNo x3 (add_SNo x4 (add_SNo x5 (add_SNo x6 (add_SNo x7 (add_SNo x8 (add_SNo x9 (add_SNo x10 (add_SNo x11 (add_SNo x12 (add_SNo x13 (add_SNo x14 (add_SNo x15 (add_SNo x16 (add_SNo x17 (add_SNo x18 (add_SNo x19 (add_SNo x20 (add_SNo x21 (add_SNo x22 (add_SNo x23 (add_SNo x24 (add_SNo x25 (add_SNo x26 (add_SNo x27 (add_SNo x28 (add_SNo x29 (add_SNo x30 (add_SNo x31 (add_SNo x32 (add_SNo x33 (add_SNo x34 (minus_SNo x35))))))))))))))))))))))))))))))))))) (proof)
Theorem 56696.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 x33 x34 x35 x36 . 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 ⟶ SNo x16 ⟶ SNo x17 ⟶ SNo x18 ⟶ SNo x19 ⟶ SNo x20 ⟶ SNo x21 ⟶ SNo x22 ⟶ SNo x23 ⟶ SNo x24 ⟶ SNo x25 ⟶ SNo x26 ⟶ SNo x27 ⟶ SNo x28 ⟶ SNo x29 ⟶ SNo x30 ⟶ SNo x31 ⟶ SNo x32 ⟶ SNo x33 ⟶ SNo x34 ⟶ SNo x35 ⟶ SNo x36 ⟶ minus_SNo (add_SNo (minus_SNo x0) (add_SNo (minus_SNo x1) (add_SNo (minus_SNo x2) (add_SNo (minus_SNo x3) (add_SNo (minus_SNo x4) (add_SNo (minus_SNo x5) (add_SNo (minus_SNo x6) (add_SNo (minus_SNo x7) (add_SNo (minus_SNo x8) (add_SNo (minus_SNo x9) (add_SNo (minus_SNo x10) (add_SNo (minus_SNo x11) (add_SNo (minus_SNo x12) (add_SNo (minus_SNo x13) (add_SNo (minus_SNo x14) (add_SNo (minus_SNo x15) (add_SNo (minus_SNo x16) (add_SNo (minus_SNo x17) (add_SNo (minus_SNo x18) (add_SNo (minus_SNo x19) (add_SNo (minus_SNo x20) (add_SNo (minus_SNo x21) (add_SNo (minus_SNo x22) (add_SNo (minus_SNo x23) (add_SNo (minus_SNo x24) (add_SNo (minus_SNo x25) (add_SNo (minus_SNo x26) (add_SNo (minus_SNo x27) (add_SNo (minus_SNo x28) (add_SNo (minus_SNo x29) (add_SNo (minus_SNo x30) (add_SNo (minus_SNo x31) (add_SNo (minus_SNo x32) (add_SNo (minus_SNo x33) (add_SNo (minus_SNo x34) (add_SNo (minus_SNo x35) x36)))))))))))))))))))))))))))))))))))) = add_SNo x0 (add_SNo x1 (add_SNo x2 (add_SNo x3 (add_SNo x4 (add_SNo x5 (add_SNo x6 (add_SNo x7 (add_SNo x8 (add_SNo x9 (add_SNo x10 (add_SNo x11 (add_SNo x12 (add_SNo x13 (add_SNo x14 (add_SNo x15 (add_SNo x16 (add_SNo x17 (add_SNo x18 (add_SNo x19 (add_SNo x20 (add_SNo x21 (add_SNo x22 (add_SNo x23 (add_SNo x24 (add_SNo x25 (add_SNo x26 (add_SNo x27 (add_SNo x28 (add_SNo x29 (add_SNo x30 (add_SNo x31 (add_SNo x32 (add_SNo x33 (add_SNo x34 (add_SNo x35 (minus_SNo x36)))))))))))))))))))))))))))))))))))) (proof)
Theorem e72cf.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 x33 x34 x35 x36 x37 . 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 ⟶ SNo x16 ⟶ SNo x17 ⟶ SNo x18 ⟶ SNo x19 ⟶ SNo x20 ⟶ SNo x21 ⟶ SNo x22 ⟶ SNo x23 ⟶ SNo x24 ⟶ SNo x25 ⟶ SNo x26 ⟶ SNo x27 ⟶ SNo x28 ⟶ SNo x29 ⟶ SNo x30 ⟶ SNo x31 ⟶ SNo x32 ⟶ SNo x33 ⟶ SNo x34 ⟶ SNo x35 ⟶ SNo x36 ⟶ SNo x37 ⟶ minus_SNo (add_SNo (minus_SNo x0) (add_SNo (minus_SNo x1) (add_SNo (minus_SNo x2) (add_SNo (minus_SNo x3) (add_SNo (minus_SNo x4) (add_SNo (minus_SNo x5) (add_SNo (minus_SNo x6) (add_SNo (minus_SNo x7) (add_SNo (minus_SNo x8) (add_SNo (minus_SNo x9) (add_SNo (minus_SNo x10) (add_SNo (minus_SNo x11) (add_SNo (minus_SNo x12) (add_SNo (minus_SNo x13) (add_SNo (minus_SNo x14) (add_SNo (minus_SNo x15) (add_SNo (minus_SNo x16) (add_SNo (minus_SNo x17) (add_SNo (minus_SNo x18) (add_SNo (minus_SNo x19) (add_SNo (minus_SNo x20) (add_SNo (minus_SNo x21) (add_SNo (minus_SNo x22) (add_SNo (minus_SNo x23) (add_SNo (minus_SNo x24) (add_SNo (minus_SNo x25) (add_SNo (minus_SNo x26) (add_SNo (minus_SNo x27) (add_SNo (minus_SNo x28) (add_SNo (minus_SNo x29) (add_SNo (minus_SNo x30) (add_SNo (minus_SNo x31) (add_SNo (minus_SNo x32) (add_SNo (minus_SNo x33) (add_SNo (minus_SNo x34) (add_SNo (minus_SNo x35) (add_SNo (minus_SNo x36) x37))))))))))))))))))))))))))))))))))))) = add_SNo x0 (add_SNo x1 (add_SNo x2 (add_SNo x3 (add_SNo x4 (add_SNo x5 (add_SNo x6 (add_SNo x7 (add_SNo x8 (add_SNo x9 (add_SNo x10 (add_SNo x11 (add_SNo x12 (add_SNo x13 (add_SNo x14 (add_SNo x15 (add_SNo x16 (add_SNo x17 (add_SNo x18 (add_SNo x19 (add_SNo x20 (add_SNo x21 (add_SNo x22 (add_SNo x23 (add_SNo x24 (add_SNo x25 (add_SNo x26 (add_SNo x27 (add_SNo x28 (add_SNo x29 (add_SNo x30 (add_SNo x31 (add_SNo x32 (add_SNo x33 (add_SNo x34 (add_SNo x35 (add_SNo x36 (minus_SNo x37))))))))))))))))))))))))))))))))))))) (proof)
Theorem 1d3b6.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 x33 x34 x35 x36 x37 x38 . 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 ⟶ SNo x16 ⟶ SNo x17 ⟶ SNo x18 ⟶ SNo x19 ⟶ SNo x20 ⟶ SNo x21 ⟶ SNo x22 ⟶ SNo x23 ⟶ SNo x24 ⟶ SNo x25 ⟶ SNo x26 ⟶ SNo x27 ⟶ SNo x28 ⟶ SNo x29 ⟶ SNo x30 ⟶ SNo x31 ⟶ SNo x32 ⟶ SNo x33 ⟶ SNo x34 ⟶ SNo x35 ⟶ SNo x36 ⟶ SNo x37 ⟶ SNo x38 ⟶ minus_SNo (add_SNo (minus_SNo x0) (add_SNo (minus_SNo x1) (add_SNo (minus_SNo x2) (add_SNo (minus_SNo x3) (add_SNo (minus_SNo x4) (add_SNo (minus_SNo x5) (add_SNo (minus_SNo x6) (add_SNo (minus_SNo x7) (add_SNo (minus_SNo x8) (add_SNo (minus_SNo x9) (add_SNo (minus_SNo x10) (add_SNo (minus_SNo x11) (add_SNo (minus_SNo x12) (add_SNo (minus_SNo x13) (add_SNo (minus_SNo x14) (add_SNo (minus_SNo x15) (add_SNo (minus_SNo x16) (add_SNo (minus_SNo x17) (add_SNo (minus_SNo x18) (add_SNo (minus_SNo x19) (add_SNo (minus_SNo x20) (add_SNo (minus_SNo x21) (add_SNo (minus_SNo x22) (add_SNo (minus_SNo x23) (add_SNo (minus_SNo x24) (add_SNo (minus_SNo x25) (add_SNo (minus_SNo x26) (add_SNo (minus_SNo x27) (add_SNo (minus_SNo x28) (add_SNo (minus_SNo x29) (add_SNo (minus_SNo x30) (add_SNo (minus_SNo x31) (add_SNo (minus_SNo x32) (add_SNo (minus_SNo x33) (add_SNo (minus_SNo x34) (add_SNo (minus_SNo x35) (add_SNo (minus_SNo x36) (add_SNo (minus_SNo x37) x38)))))))))))))))))))))))))))))))))))))) = add_SNo x0 (add_SNo x1 (add_SNo x2 (add_SNo x3 (add_SNo x4 (add_SNo x5 (add_SNo x6 (add_SNo x7 (add_SNo x8 (add_SNo x9 (add_SNo x10 (add_SNo x11 (add_SNo x12 (add_SNo x13 (add_SNo x14 (add_SNo x15 (add_SNo x16 (add_SNo x17 (add_SNo x18 (add_SNo x19 (add_SNo x20 (add_SNo x21 (add_SNo x22 (add_SNo x23 (add_SNo x24 (add_SNo x25 (add_SNo x26 (add_SNo x27 (add_SNo x28 (add_SNo x29 (add_SNo x30 (add_SNo x31 (add_SNo x32 (add_SNo x33 (add_SNo x34 (add_SNo x35 (add_SNo x36 (add_SNo x37 (minus_SNo x38)))))))))))))))))))))))))))))))))))))) (proof)
Theorem 99402.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 x33 x34 x35 x36 x37 x38 x39 . 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 ⟶ SNo x16 ⟶ SNo x17 ⟶ SNo x18 ⟶ SNo x19 ⟶ SNo x20 ⟶ SNo x21 ⟶ SNo x22 ⟶ SNo x23 ⟶ SNo x24 ⟶ SNo x25 ⟶ SNo x26 ⟶ SNo x27 ⟶ SNo x28 ⟶ SNo x29 ⟶ SNo x30 ⟶ SNo x31 ⟶ SNo x32 ⟶ SNo x33 ⟶ SNo x34 ⟶ SNo x35 ⟶ SNo x36 ⟶ SNo x37 ⟶ SNo x38 ⟶ SNo x39 ⟶ minus_SNo (add_SNo (minus_SNo x0) (add_SNo (minus_SNo x1) (add_SNo (minus_SNo x2) (add_SNo (minus_SNo x3) (add_SNo (minus_SNo x4) (add_SNo (minus_SNo x5) (add_SNo (minus_SNo x6) (add_SNo (minus_SNo x7) (add_SNo (minus_SNo x8) (add_SNo (minus_SNo x9) (add_SNo (minus_SNo x10) (add_SNo (minus_SNo x11) (add_SNo (minus_SNo x12) (add_SNo (minus_SNo x13) (add_SNo (minus_SNo x14) (add_SNo (minus_SNo x15) (add_SNo (minus_SNo x16) (add_SNo (minus_SNo x17) (add_SNo (minus_SNo x18) (add_SNo (minus_SNo x19) (add_SNo (minus_SNo x20) (add_SNo (minus_SNo x21) (add_SNo (minus_SNo x22) (add_SNo (minus_SNo x23) (add_SNo (minus_SNo x24) (add_SNo (minus_SNo x25) (add_SNo (minus_SNo x26) (add_SNo (minus_SNo x27) (add_SNo (minus_SNo x28) (add_SNo (minus_SNo x29) (add_SNo (minus_SNo x30) (add_SNo (minus_SNo x31) (add_SNo (minus_SNo x32) (add_SNo (minus_SNo x33) (add_SNo (minus_SNo x34) (add_SNo (minus_SNo x35) (add_SNo (minus_SNo x36) (add_SNo (minus_SNo x37) (add_SNo (minus_SNo x38) x39))))))))))))))))))))))))))))))))))))))) = add_SNo x0 (add_SNo x1 (add_SNo x2 (add_SNo x3 (add_SNo x4 (add_SNo x5 (add_SNo x6 (add_SNo x7 (add_SNo x8 (add_SNo x9 (add_SNo x10 (add_SNo x11 (add_SNo x12 (add_SNo x13 (add_SNo x14 (add_SNo x15 (add_SNo x16 (add_SNo x17 (add_SNo x18 (add_SNo x19 (add_SNo x20 (add_SNo x21 (add_SNo x22 (add_SNo x23 (add_SNo x24 (add_SNo x25 (add_SNo x26 (add_SNo x27 (add_SNo x28 (add_SNo x29 (add_SNo x30 (add_SNo x31 (add_SNo x32 (add_SNo x33 (add_SNo x34 (add_SNo x35 (add_SNo x36 (add_SNo x37 (add_SNo x38 (minus_SNo x39))))))))))))))))))))))))))))))))))))))) (proof)
Theorem 93614.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 x33 x34 x35 x36 x37 x38 x39 x40 . 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 ⟶ SNo x16 ⟶ SNo x17 ⟶ SNo x18 ⟶ SNo x19 ⟶ SNo x20 ⟶ SNo x21 ⟶ SNo x22 ⟶ SNo x23 ⟶ SNo x24 ⟶ SNo x25 ⟶ SNo x26 ⟶ SNo x27 ⟶ SNo x28 ⟶ SNo x29 ⟶ SNo x30 ⟶ SNo x31 ⟶ SNo x32 ⟶ SNo x33 ⟶ SNo x34 ⟶ SNo x35 ⟶ SNo x36 ⟶ SNo x37 ⟶ SNo x38 ⟶ SNo x39 ⟶ SNo x40 ⟶ minus_SNo (add_SNo (minus_SNo x0) (add_SNo (minus_SNo x1) (add_SNo (minus_SNo x2) (add_SNo (minus_SNo x3) (add_SNo (minus_SNo x4) (add_SNo (minus_SNo x5) (add_SNo (minus_SNo x6) (add_SNo (minus_SNo x7) (add_SNo (minus_SNo x8) (add_SNo (minus_SNo x9) (add_SNo (minus_SNo x10) (add_SNo (minus_SNo x11) (add_SNo (minus_SNo x12) (add_SNo (minus_SNo x13) (add_SNo (minus_SNo x14) (add_SNo (minus_SNo x15) (add_SNo (minus_SNo x16) (add_SNo (minus_SNo x17) (add_SNo (minus_SNo x18) (add_SNo (minus_SNo x19) (add_SNo (minus_SNo x20) (add_SNo (minus_SNo x21) (add_SNo (minus_SNo x22) (add_SNo (minus_SNo x23) (add_SNo (minus_SNo x24) (add_SNo (minus_SNo x25) (add_SNo (minus_SNo x26) (add_SNo (minus_SNo x27) (add_SNo (minus_SNo x28) (add_SNo (minus_SNo x29) (add_SNo (minus_SNo x30) (add_SNo (minus_SNo x31) (add_SNo (minus_SNo x32) (add_SNo (minus_SNo x33) (add_SNo (minus_SNo x34) (add_SNo (minus_SNo x35) (add_SNo (minus_SNo x36) (add_SNo (minus_SNo x37) (add_SNo (minus_SNo x38) (add_SNo (minus_SNo x39) x40)))))))))))))))))))))))))))))))))))))))) = add_SNo x0 (add_SNo x1 (add_SNo x2 (add_SNo x3 (add_SNo x4 (add_SNo x5 (add_SNo x6 (add_SNo x7 (add_SNo x8 (add_SNo x9 (add_SNo x10 (add_SNo x11 (add_SNo x12 (add_SNo x13 (add_SNo x14 (add_SNo x15 (add_SNo x16 (add_SNo x17 (add_SNo x18 (add_SNo x19 (add_SNo x20 (add_SNo x21 (add_SNo x22 (add_SNo x23 (add_SNo x24 (add_SNo x25 (add_SNo x26 (add_SNo x27 (add_SNo x28 (add_SNo x29 (add_SNo x30 (add_SNo x31 (add_SNo x32 (add_SNo x33 (add_SNo x34 (add_SNo x35 (add_SNo x36 (add_SNo x37 (add_SNo x38 (add_SNo x39 (minus_SNo x40)))))))))))))))))))))))))))))))))))))))) (proof)
Theorem 01f0f.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 x33 x34 x35 x36 x37 x38 x39 x40 x41 . 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 ⟶ SNo x16 ⟶ SNo x17 ⟶ SNo x18 ⟶ SNo x19 ⟶ SNo x20 ⟶ SNo x21 ⟶ SNo x22 ⟶ SNo x23 ⟶ SNo x24 ⟶ SNo x25 ⟶ SNo x26 ⟶ SNo x27 ⟶ SNo x28 ⟶ SNo x29 ⟶ SNo x30 ⟶ SNo x31 ⟶ SNo x32 ⟶ SNo x33 ⟶ SNo x34 ⟶ SNo x35 ⟶ SNo x36 ⟶ SNo x37 ⟶ SNo x38 ⟶ SNo x39 ⟶ SNo x40 ⟶ SNo x41 ⟶ minus_SNo (add_SNo (minus_SNo x0) (add_SNo (minus_SNo x1) (add_SNo (minus_SNo x2) (add_SNo (minus_SNo x3) (add_SNo (minus_SNo x4) (add_SNo (minus_SNo x5) (add_SNo (minus_SNo x6) (add_SNo (minus_SNo x7) (add_SNo (minus_SNo x8) (add_SNo (minus_SNo x9) (add_SNo (minus_SNo x10) (add_SNo (minus_SNo x11) (add_SNo (minus_SNo x12) (add_SNo (minus_SNo x13) (add_SNo (minus_SNo x14) (add_SNo (minus_SNo x15) (add_SNo (minus_SNo x16) (add_SNo (minus_SNo x17) (add_SNo (minus_SNo x18) (add_SNo (minus_SNo x19) (add_SNo (minus_SNo x20) (add_SNo (minus_SNo x21) (add_SNo (minus_SNo x22) (add_SNo (minus_SNo x23) (add_SNo (minus_SNo x24) (add_SNo (minus_SNo x25) (add_SNo (minus_SNo x26) (add_SNo (minus_SNo x27) (add_SNo (minus_SNo x28) (add_SNo (minus_SNo x29) (add_SNo (minus_SNo x30) (add_SNo (minus_SNo x31) (add_SNo (minus_SNo x32) (add_SNo (minus_SNo x33) (add_SNo (minus_SNo x34) (add_SNo (minus_SNo x35) (add_SNo (minus_SNo x36) (add_SNo (minus_SNo x37) (add_SNo (minus_SNo x38) (add_SNo (minus_SNo x39) (add_SNo (minus_SNo x40) x41))))))))))))))))))))))))))))))))))))))))) = add_SNo x0 (add_SNo x1 (add_SNo x2 (add_SNo x3 (add_SNo x4 (add_SNo x5 (add_SNo x6 (add_SNo x7 (add_SNo x8 (add_SNo x9 (add_SNo x10 (add_SNo x11 (add_SNo x12 (add_SNo x13 (add_SNo x14 (add_SNo x15 (add_SNo x16 (add_SNo x17 (add_SNo x18 (add_SNo x19 (add_SNo x20 (add_SNo x21 (add_SNo x22 (add_SNo x23 (add_SNo x24 (add_SNo x25 (add_SNo x26 (add_SNo x27 (add_SNo x28 (add_SNo x29 (add_SNo x30 (add_SNo x31 (add_SNo x32 (add_SNo x33 (add_SNo x34 (add_SNo x35 (add_SNo x36 (add_SNo x37 (add_SNo x38 (add_SNo x39 (add_SNo x40 (minus_SNo x41))))))))))))))))))))))))))))))))))))))))) (proof)
Theorem 3bb0e.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 x33 x34 x35 x36 x37 x38 x39 x40 x41 x42 . 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 ⟶ SNo x16 ⟶ SNo x17 ⟶ SNo x18 ⟶ SNo x19 ⟶ SNo x20 ⟶ SNo x21 ⟶ SNo x22 ⟶ SNo x23 ⟶ SNo x24 ⟶ SNo x25 ⟶ SNo x26 ⟶ SNo x27 ⟶ SNo x28 ⟶ SNo x29 ⟶ SNo x30 ⟶ SNo x31 ⟶ SNo x32 ⟶ SNo x33 ⟶ SNo x34 ⟶ SNo x35 ⟶ SNo x36 ⟶ SNo x37 ⟶ SNo x38 ⟶ SNo x39 ⟶ SNo x40 ⟶ SNo x41 ⟶ SNo x42 ⟶ minus_SNo (add_SNo (minus_SNo x0) (add_SNo (minus_SNo x1) (add_SNo (minus_SNo x2) (add_SNo (minus_SNo x3) (add_SNo (minus_SNo x4) (add_SNo (minus_SNo x5) (add_SNo (minus_SNo x6) (add_SNo (minus_SNo x7) (add_SNo (minus_SNo x8) (add_SNo (minus_SNo x9) (add_SNo (minus_SNo x10) (add_SNo (minus_SNo x11) (add_SNo (minus_SNo x12) (add_SNo (minus_SNo x13) (add_SNo (minus_SNo x14) (add_SNo (minus_SNo x15) (add_SNo (minus_SNo x16) (add_SNo (minus_SNo x17) (add_SNo (minus_SNo x18) (add_SNo (minus_SNo x19) (add_SNo (minus_SNo x20) (add_SNo (minus_SNo x21) (add_SNo (minus_SNo x22) (add_SNo (minus_SNo x23) (add_SNo (minus_SNo x24) (add_SNo (minus_SNo x25) (add_SNo (minus_SNo x26) (add_SNo (minus_SNo x27) (add_SNo (minus_SNo x28) (add_SNo (minus_SNo x29) (add_SNo (minus_SNo x30) (add_SNo (minus_SNo x31) (add_SNo (minus_SNo x32) (add_SNo (minus_SNo x33) (add_SNo (minus_SNo x34) (add_SNo (minus_SNo x35) (add_SNo (minus_SNo x36) (add_SNo (minus_SNo x37) (add_SNo (minus_SNo x38) (add_SNo (minus_SNo x39) (add_SNo (minus_SNo x40) (add_SNo (minus_SNo x41) x42)))))))))))))))))))))))))))))))))))))))))) = add_SNo x0 (add_SNo x1 (add_SNo x2 (add_SNo x3 (add_SNo x4 (add_SNo x5 (add_SNo x6 (add_SNo x7 (add_SNo x8 (add_SNo x9 (add_SNo x10 (add_SNo x11 (add_SNo x12 (add_SNo x13 (add_SNo x14 (add_SNo x15 (add_SNo x16 (add_SNo x17 (add_SNo x18 (add_SNo x19 (add_SNo x20 (add_SNo x21 (add_SNo x22 (add_SNo x23 (add_SNo x24 (add_SNo x25 (add_SNo x26 (add_SNo x27 (add_SNo x28 (add_SNo x29 (add_SNo x30 (add_SNo x31 (add_SNo x32 (add_SNo x33 (add_SNo x34 (add_SNo x35 (add_SNo x36 (add_SNo x37 (add_SNo x38 (add_SNo x39 (add_SNo x40 (add_SNo x41 (minus_SNo x42)))))))))))))))))))))))))))))))))))))))))) (proof)