[Imprint][Data Privacy Statement][E-Mail]

Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Lemma dependency for Specification int-mult

A lemma (entry) may depend on lemmas (entries) below its position, but never on lemmas above its position. This means the list is a topological order of the dependency graph. An entry 'all subs proved' means that all used lemmas are (transitively) proved.

Name: Status: Subs proved? Used:
modeqp-negprovedall subs proved commutativity, associativity, minus-left, modneqp,
threeprovedall subs proved one-01, three-01, eq-same-02, zero-le, one, modneqp, commutativity, associativity,
modeqp-posprovedall subs proved modneqp,
modneqpprovedall subs proved associativity, ls-pos, ls-forward, commutativity, modlep-03,
modlep-04provedall subs proved modlep-03,
modlep-03provedall subs proved commutativity, associativity, one, dist-rsplit, modlep-02,
square-eq-02provedall subs proved commutativity, associativity, numsucc, one, dist-lsplit, square-eq-01,
mods-ls-01provedall subs proved commutativity, modlep-02,
mods-ls-04provedall subs proved commutativity, modlsp-02, mods-ls-02,
mods-lsprovedall subs proved commutativity, modlep-02,
square-injectprovedall subs proved eq-pos, eq-succ-01, le-pos, commutativity, associativity, numls-04, numsucc, one, dist-lsplit, zero-ge, square-interval,
square-intervalprovedall subs proved le-pos, numle-03, zero-ls, commutativity, associativity, numsucc, one, dist-lsplit, numls-04, square-ls-02,
mods-ls-02provedall subs proved commutativity, modlep-01,
modlep-02provedall subs proved modlep-01,
square-eq-01provedall subs proved square-ls-02, commutativity, associativity, one, dist-lsplit,
square-le-05provedall subs proved commutativity, associativity, numsucc, one, dist-lsplit, square-le-04,
mod-neqprovedall subs proved modeqp-01, modeqp, modeqp-02, commutativity, modeqp-03,
mods-ls-03provedall subs proved commutativity, modlep-01,
square-ls-03provedall subs proved commutativity, associativity, numsucc, one, dist-lsplit, square-ls-02,
modlep-01provedall subs proved modlep,
square-ls-02provedall subs proved square-ls, square-le, commutativity, associativity, one, dist-lsplit,
modeqp-03provedall subs proved eq-neg, commutativity, associativity, minus-left, modeqp-01,
square-le-04provedall subs proved square-le, mult-gt-both, commutativity, associativity, one, dist-lsplit,
modzero-07provedall subs proved zero-ls, commutativity, associativity, Mult-zero, minus-left, modlep,
square-exprovedall subs proved one-01, zero-gr, square-le, le-one, one, numle-03, le-dist-02, dist-lsplit, commutativity, associativity, square-ls,
square-one-leprovedall subs proved commutativity, associativity, square-le,
le-twoprovedall subs proved commutativity, associativity, Mult-zero, numls-02, modlsp-02, modlep,
square-le-06provedall subs proved one, modlep, commutativity, associativity, zero-gr-01,
modeqp-02provedall subs proved commutativity, associativity, minus-left, modeqp,
modeqp-01provedall subs proved modeqp,
square-leprovedall subs proved commutativity, associativity, square-ls,
modlepprovedall subs proved modlsp, eq-pos, modeqp, commutativity, associativity, le-pos,
neq-5-not-evenprovedall subs proved odd-even,
two-moneprovedall subs proved minus-left, commutativity, associativity, Mult-zero, modeqp,
7-not-evenprovedall subs proved odd-even,
square-eqprovedall subs proved eq-pos, abs-eqneg, minus-left, square-ls, square-abs, abs-eqall, commutativity, associativity, square-zero, pls-pos,
5-not-evenprovedall subs proved odd-even,
neq-3-not-evenprovedall subs proved odd-even,
square-evenprovedall subs proved numdist, modeqp, ex-two, commutativity, associativity, one, dist-lsplit,
neq-9-not-evenprovedall subs proved odd-even,
square-gez-02provedall subs proved commutativity, associativity, square-lez, square-le-01, square-le-02,
mods-eqprovedall subs proved modeqp,
neq-7-not-evenprovedall subs proved odd-even,
square-le-02provedall subs proved square-lez, ls-same, commutativity, associativity, square-abs, abs-eqall,
three-01provedall subs proved two-oddeq,
square-lsprovedall subs proved square-lez-01, pls-pos, square-abs, abs-eqall, commutativity, associativity, square-lez, ple-pos,
modeqpprovedall subs proved dist-lsplit, one, dist-rsplit, commutativity, associativity, zero-eq, zero-ge-add, ls-add, Mult-zero,
odd-evenprovedall subs proved commutativity, associativity, two-oddeq,
square-ls-04provedall subs proved square-lez-01, commutativity, associativity, one, dist-lsplit,
square-minusprovedall subs proved commutativity, associativity, square-lez-01,
two-oddeqprovedall subs proved dist-sub-split, commutativity, associativity, eq-one,
zero-ge-addprovedall subs proved ls-add, zero-ls, minus-one-02, commutativity, associativity, one, dist-lsplit, zero-ge-03,
square-lez-01provedall subs proved zero-le-case, commutativity, associativity,
square-absprovedall subs proved commutativity, associativity, square-lez, abs-eqall,
square-gez-01provedall subs proved commutativity, associativity, square-gez,
pzero-grprovedall subs proved zero-le-case,
zero-le-twoprovedall subs proved zero-le-case,
eq-one-negprovedall subs proved one, minus-one-01, commutativity, associativity, eq-one, minus-left,
square-zero-02provedall subs proved commutativity, associativity, dist-lsplit, one, square-zero-01,
neq-twoprovedall subs proved commutativity, associativity, eq-one,
modzero-08provedall subs proved modzero, mods-nls, commutativity, associativity, abs-eqall,
zero-ge-caseprovedall subs proved commutativity, associativity, zero-ge-03, zero-ge,
square-le-01provedall subs proved commutativity, associativity, square-lez, ls-same,
square-zero-01provedall subs proved commutativity, associativity, square-lez, one, numls-13, numsucc, dist-lsplit,
zero-ge-03provedall subs proved zero-ls-03, commutativity, associativity, zero-ge-01,
eq-oneprovedall subs proved zero-gr-02, zero-gr-01, square-lez, one, minus-left, minus-one-01, commutativity, associativity, zero-left, pzero-ls, pls-pos,
square-gezprovedall subs proved commutativity, associativity, square-lez,
zero-le-caseprovedall subs proved commutativity, associativity, zero-le-03, zero-le,
abs-eqallprovedall subs proved zero-ge-02, zero-le-02, zero-gr-01, zero-ge-01, commutativity, associativity, minus-left,
modlsp-06provedall subs proved commutativity, associativity, minus-left, modlsp-03,
abs-lsprovedall subs proved modzero-06,
square-ls-01provedall subs proved commutativity, associativity, square-lez,
exdivmodprovedall subs proved one, dist-lsplit, commutativity, associativity, minus-left, exdivmodpos,
modzero-03provedall subs proved commutativity, associativity, minus-one, one, dist-rsplit, zero-ge-01,
modlsp-05provedall subs proved modlsp-04,
mods-zero-07provedall subs proved modzero,
square-le-03provedall subs proved commutativity, associativity, square-lez,
two-leoneprovedall subs proved le-one, commutativity,
modzero-02provedall subs proved commutativity, associativity, minus-one, one, dist-rsplit, zero-ge-01,
modzero-01provedall subs proved zero-left, commutativity, associativity, minus-one, one, dist-rsplit, zero-ge-01,
pzero-lsprovedall subs proved zero-ls-case,
modzeroprovedall subs proved commutativity, associativity, zero-left, modlsp-02,
modlsp-04provedall subs proved commutativity, associativity, minus-left, modlsp-02,
zero-le-03provedall subs proved zero-gr-03, commutativity, associativity, zero-le-01,
zero-ge-01provedall subs proved zero-ls-01, commutativity, associativity, zero-ge,
square-zeroprovedall subs proved commutativity, associativity, zero-eq,
abs-eqnegprovedall subs proved commutativity, associativity, eq-neg, minus-left,
exdivmodposprovedall subs proved commutativity, associativity, one, dist-lsplit, auxexdivmod-01,
ls-addprovedall subs proved zero-gr, commutativity, associativity, one-01, modlsp-02,
eq-same-02provedall subs proved commutativity, associativity, one, eq-same,
le-oneprovedall subs proved zero-gr-01, Mult-zero, commutativity, associativity, ls-same-05,
modzero-06provedall subs proved commutativity, associativity, minus-one, one, dist-rsplit, zero-ls-01,
square-lezprovedall subs proved zero-ls-case,
modlsp-03provedall subs proved commutativity, associativity, one, dist-rsplit, modlsp-02,
modzero-04provedall subs proved commutativity, associativity, minus-one, one, dist-rsplit, zero-ls-01,
abs-ls-sameprovedall subs proved commutativity, associativity, ls-same, abs-not-neg, Mult-zero,
pnls-negprovedall subs proved ple-neg,
two-zeroprovedall subs proved commutativity, associativity, zero-eq,
zero-neqprovedall subs proved commutativity, associativity, Mult-zero, zero-eq,
le-same-05provedall subs proved commutativity, associativity, Mult-zero, le-same-04,
short-mult-maxprovedall subs proved le-pos, zero-gr, ls-pos, commutativity, associativity, zero-ge-02, zero-gr-02,
modzero-05provedall subs proved commutativity, associativity, minus-one, one, dist-rsplit, zero-ls-01,
eq-same-01provedall subs proved commutativity, associativity, one, eq-same,
eq-pos-01provedall subs proved commutativity, associativity, eq-pos,
mult-pos-posprovedall subs proved commutativity, associativity, one, eq-same,
zero-neq-01provedall subs proved commutativity, associativity, Mult-zero, zero-eq,
abs-ls-same-01provedall subs proved one, eq-dist, zero-le-01, succ-rmerge, minus-left, le-same-01, minus-one-01, zero-left, commutativity, associativity, mods-nls,
zero-ls-twoprovedall subs proved commutativity, associativity, zero-ls-01, zero-ls-02,
numls-07provedall subs proved zero-gr, le-same-03, zero-gr-03, zero-le-01, commutativity, associativity, ls-same-02, zero-ls-03, ls-same-04,
eq-same-03provedall subs proved commutativity, associativity, one, eq-same,
numle-07provedall subs proved zero-ls, zero-left, le-same-02, associativity, zero-ls-03, le-same, commutativity,
le-same-02provedall subs proved commutativity, associativity, one, le-neg,
le-same-03provedall subs proved commutativity, associativity, one, le-neg,
auxexdivmod-01provedall subs proved one-01, le-same, commutativity, associativity, one, dist-lsplit, Mult-zero, auxexdivmod,
ls-same-05provedall subs proved ls-same-04,
le-same-04provedall subs proved commutativity, associativity, zero-left, one, le-pos-01,
zero-le-02provedall subs proved zero-gr-02, commutativity, associativity, zero-le,
zero-ge-02provedall subs proved zero-ls-02, commutativity, associativity, zero-ge,
eq-posprovedall subs proved commutativity, associativity, Mult-zero, eq-nonzero,
eq-sameprovedall subs proved Mult-zero, commutativity, associativity, one, eq-nonzero,
mult-gt-bothprovedall subs proved zero-le, zero-left, numle-10, commutativity, associativity, ls-pos, ls-forward,
zero-eqprovedall subs proved commutativity, associativity, Mult-zero, eq-nonzero,
eq-negprovedall subs proved commutativity, associativity, Mult-zero, eq-nonzero,
ple-negprovedall subs proved pls-neg,
modlsp-02provedall subs proved modlsp-01,
abs-not-negprovedall subs proved zero-ls-02,
zero-ls-caseprovedall subs proved commutativity, associativity, zero-ls-03, zero-ls,
zero-ls-01provedall subs proved commutativity, associativity, zero-ls-03, zero-ls,
zero-le-01provedall subs proved commutativity, associativity, Mult-zero, le-neg,
eq-nonzero-03provedall subs proved commutativity, associativity, eq-nonzero,
le-neg-01provedall subs proved commutativity, associativity, le-neg,
le-same-06provedall subs proved commutativity, associativity, le-same,
pnle-posprovedall subs proved commutativity, associativity, zero-le, zero-left, pls-pos,
ls-twoprovedall subs proved commutativity, associativity, zero-ge,
two-eqprovedall subs proved eq-nonzero,
ple-pos-betterprovedall subs proved commutativity, associativity, zero-ls-02, zero-left, ple-pos,
le-absprovedall subs proved commutativity, associativity, ls-forward, le-pos-01,
zero-ls-subprovedall subs proved commutativity, associativity, zero-ls-03, zero-ls,
numabsprovedall subs proved commutativity, associativity, Mult-zero, numabs-01,
eq-nonzero-02provedall subs proved commutativity, associativity, eq-nonzero,
zero-ge-add-01provedall subs proved commutativity, associativity, zero-ls-02,
pnle-negprovedall subs proved pls-neg,
numle-11provedall subs proved commutativity, associativity, le-neg,
zero-gr-addprovedall subs proved zero-gr-case, succ-lsplit,
mult-gt-oneprovedall subs proved commutativity, associativity, le-same,
eq-nonzero-01provedall subs proved commutativity, associativity, eq-nonzero,
pnls-posprovedall subs proved commutativity, associativity, zero-ls-02, zero-left, ple-pos,
mod-nleprovedall subs proved dist-sub-split, zero-le, commutativity, associativity, one,
ls-same-02provedall subs proved commutativity, associativity, one, ls-neg,
le-same-01provedall subs proved commutativity, associativity, one, le-pos,
zero-gr-caseprovedall subs proved commutativity, associativity, zero-gr-03, zero-gr-01, zero-gr,
mods-nlsprovedall subs proved one, dist-lsplit, zero-gr-01, minus-left, associativity, Mult-zero, ls-same, commutativity,
ls-same-04provedall subs proved commutativity, associativity, ls-same,
pls-negprovedall subs proved commutativity, associativity, ls-neg,
numabs-01provedall subs proved commutativity, associativity, zero-ls,
modlsp-01provedall subs proved modlsp,
zero-ls-03provedall subs proved commutativity, associativity, zero-ls, zero-left, ls-neg,
le-pos-01provedall subs proved commutativity, associativity, le-pos,
ple-posprovedall subs proved commutativity, associativity, ls-pos, pls-pos,
numle-10provedall subs proved commutativity, associativity, le-pos,
zero-leprovedall subs proved commutativity, associativity, Mult-zero, le-pos,
le-sameprovedall subs proved commutativity, associativity, one, le-pos,
le-negprovedall subs proved commutativity, associativity, ls-neg,
zero-geprovedall subs proved Mult-zero, le-pos,
zero-ls-02provedall subs proved commutativity, associativity, zero-ls, Mult-zero,
eq-nonzeroprovedall subs proved ls-pos, commutativity, associativity, ls-neg,
pnls-negposprovedall subs proved ls-pos, commutativity, associativity, ls-neg, ls-forward,
mod-nlsprovedall subs proved zero-gr-add-02, associativity, Mult-zero, numls-12, commutativity,
ls-pos-02provedall subs proved ls-pos-01,
ls-same-03provedall subs proved commutativity, associativity, one, ls-neg,
zero-ge-add-02provedall subs proved commutativity, associativity, zero-left, zero-ls, dist-lsplit,
pnls-posnegprovedall subs proved ls-neg, commutativity, associativity, ls-pos, ls-forward,
numls-11provedall subs proved commutativity, associativity, ls-neg,
mult-sub-lesseqprovedall subs proved commutativity, associativity, le-pos,
mult-add-greaterprovedall subs proved commutativity, associativity, zero-ls, dist-lsplit,
two-le-02provedall subs proved commutativity, associativity, le-pos, dist-lsplit,
noeth-modlepprovedall subs proved ls-add-02, ls-pos, ls-forward, Mult-zero, ls-pos-01, numsucc, one, dist-lsplit, minus-one-01, dist-sub-split, commutativity, associativity, minus-left,
modlspprovedall subs proved commutativity, associativity, one, dist-rsplit, ls-pos,
ls-pos-01provedall subs proved commutativity, associativity, ls-pos,
le-posprovedall subs proved commutativity, associativity, ls-pos,
zero-gr-add-02provedall subs proved one, dist-lsplit, zero-gr-02, commutativity, associativity, Mult-zero,
pls-posprovedall subs proved commutativity, associativity, ls-pos,
auxexdivmodprovedall subs proved commutativity, associativity, ls-pos, zero-gr,
zero-gr-03provedall subs proved zero-gr-01, commutativity, associativity, zero-left, zero-gr-02,
ls-sameprovedall subs proved commutativity, associativity, one, ls-pos,
ls-negprovedall subs proved commutativity, associativity, minus-left, ls-pos,
zero-lsprovedall subs proved commutativity, associativity, Mult-zero, ls-pos,
est-nleprovedall subs proved commutativity, associativity, ls-pos, ls-forward,
pls-pos-01provedall subs proved commutativity, associativity, ls-pos, ls-forward,
zero-gr-add-01provedall subs proved commutativity, associativity, zero-gr-02,
ls-subprovedall subs proved commutativity, associativity, ls-pos,
noeth-ls-posprovedall subs proved commutativity, associativity, ls-pos,
two-ls-02provedall subs proved commutativity, associativity, ls-pos, dist-lsplit,
mult-sub-lessprovedall subs proved commutativity, associativity, ls-pos,
mult-posprovedall subs proved commutativity, associativity, zero-gr-01,
numls-10provedall subs proved commutativity, associativity, ls-pos,
pls-pos-02provedall subs proved commutativity, associativity, ls-pos, ls-forward,
ls-same-01provedall subs proved commutativity, associativity, one, ls-pos,
zero-gr-01provedall subs proved commutativity, associativity, minus-left, zero-gr,
ls-posprovedall subs proved dist-lsplit, one, dist-rsplit, commutativity, associativity, zero-gr, Mult-zero,
zero-gr-02provedall subs proved commutativity, associativity, zero-gr, zero-left,
ls-two-02provedall subs proved commutativity, associativity, zero-gr,
ls-two-01provedall subs proved commutativity, associativity, zero-gr,
ls-two-03provedall subs proved commutativity, associativity, zero-gr,
zero-grprovedall subs proved minus-left, commutativity, associativity, zero-left, noeth-zero-ls,
noeth-zero-lsprovedall subs proved ls-forward, minus-one-02, one, dist-lsplit, commutativity, associativity, minus-left,
minus-one-02provedall subs proved commutativity, associativity, minus-one-01,
minus-oneprovedall subs proved commutativity, associativity, minus-one-01,
ex-twoprovedall subs proved commutativity, associativity, one, numeq-03,
minus-one-01provedall subs proved commutativity, associativity, Mult-zero, numsucc,
numleneg-01provedall subs proved commutativity, associativity, minus-left,
numls-06provedall subs proved commutativity, associativity, ls-add-02,
numlsneg-03provedall subs proved commutativity, associativity, minus-left,
add-mult-twoprovedall subs proved commutativity, associativity, one, numeq-03,
two-sub-01provedall subs proved commutativity, associativity, one, numeq-03,
numleneg-03provedall subs proved commutativity, associativity, minus-left,
numlsnegprovedall subs proved commutativity, associativity, minus-left,
numlenegprovedall subs proved commutativity, associativity, minus-left,
numlsneg-02provedall subs proved commutativity, associativity, minus-left,
numleneg-02provedall subs proved commutativity, associativity, minus-left,
numlsneg-01provedall subs proved commutativity, associativity, minus-left,
eq-succ-01provedall subs proved dist-lsplit,
numls-13provedall subs proved commutativity, associativity, one, dist-lsplit,
numls-02provedall subs proved commutativity, associativity, dist-lsplit,
numdistprovedall subs proved commutativity, associativity, eq-dist,
numls-04provedall subs proved commutativity, associativity, one, dist-lsplit,
numeq-03provedall subs proved commutativity, associativity, one, dist-lsplit,
le-dist-02provedall subs proved commutativity, associativity, dist-lsplit,
numle-03provedall subs proved commutativity, associativity, one, dist-lsplit,
ls-add-02provedall subs proved commutativity, associativity, dist-lsplit,
numls-12provedall subs proved commutativity, associativity, one, dist-lsplit,
numsuccprovedall subs proved commutativity, associativity, one, eq-dist,
minus-leftprovedall subs proved commutativity, associativity, zero-left, dist-sub-split,
two-subprovedall subs proved commutativity, associativity, dist-lsplit,
numeq-01provedall subs proved commutativity, associativity, eq-dist,
two-ls-04provedall subs proved commutativity, associativity, dist-lsplit,
numle-01provedall subs proved commutativity, associativity, dist-lsplit,
ls-dist-06provedall subs proved commutativity, associativity, one, dist-lsplit,
two-lsprovedall subs proved commutativity, associativity, dist-lsplit,
numeq-04provedall subs proved commutativity, associativity, one, dist-lsplit,
numsubprovedall subs proved commutativity, associativity, one, dist-lsplit,
two-le-01provedall subs proved commutativity, associativity, dist-lsplit,
numls-09provedall subs proved commutativity, associativity, one, dist-lsplit,
two-le-04provedall subs proved commutativity, associativity, dist-lsplit,
numleprovedall subs proved commutativity, associativity, dist-lsplit,
ls-dist-03provedall subs proved commutativity, associativity, one, dist-lsplit,
numls-03provedall subs proved commutativity, associativity, one, dist-lsplit,
ls-same-06provedall subs proved commutativity, associativity, one, dist-lsplit,
two-predprovedall subs proved commutativity, associativity, dist-lsplit,
numle-06provedall subs proved commutativity, associativity, dist-lsplit,
numle-12provedall subs proved commutativity, associativity, one, dist-lsplit,
two-le-03provedall subs proved commutativity, associativity, dist-lsplit,
numle-09provedall subs proved commutativity, associativity, one, dist-lsplit,
two-ls-03provedall subs proved commutativity, associativity, dist-lsplit,
ls-dist-02provedall subs proved commutativity, associativity, dist-lsplit,
ls-dist-05provedall subs proved commutativity, associativity, one, dist-lsplit,
numlsprovedall subs proved commutativity, associativity, dist-lsplit,
numls-05provedall subs proved commutativity, associativity, one, dist-lsplit,
ls-distprovedall subs proved commutativity, associativity, dist-lsplit,
numle-08provedall subs proved commutativity, associativity, one, dist-lsplit,
numls-08provedall subs proved commutativity, associativity, one, dist-lsplit,
numeq-02provedall subs proved commutativity, associativity, eq-succ,
numle-02provedall subs proved commutativity, associativity, dist-lsplit,
numle-05provedall subs proved commutativity, associativity, one, dist-lsplit,
two-leprovedall subs proved commutativity, associativity, dist-lsplit,
ls-dist-01provedall subs proved commutativity, associativity, dist-lsplit,
ls-dist-04provedall subs proved commutativity, associativity, one, dist-lsplit,
ls-add-03provedall subs proved commutativity, associativity, dist-lsplit,
numls-01provedall subs proved commutativity, associativity, dist-lsplit,
numeqprovedall subs proved commutativity, associativity, dist-lsplit,
le-dist-01provedall subs proved commutativity, associativity, dist-lsplit,
numle-04provedall subs proved commutativity, associativity, one, dist-lsplit,
two-ls-01provedall subs proved commutativity, associativity, dist-lsplit,
le-distprovedall subs proved commutativity, associativity, dist-lsplit,
numle-13provedall subs proved commutativity, associativity, one, dist-lsplit,
succ-rmergeprovedall subs proved commutativity, associativity, one, dist-rsplit,
eq-succprovedall subs proved commutativity, associativity, one, dist-rsplit,
dist-sub-splitprovedall subs proved commutativity, associativity, dist-rsplit,
one-01provedall subs proved commutativity, associativity, one,
ls-forwardprovedall subs proved commutativity, associativity, zero-left,
eq-distprovedall subs proved commutativity, associativity, dist-rsplit,
dist-lsplitprovedall subs proved commutativity, associativity, dist-rsplit,
neq-not-zeroprovedall subs proved commutativity, associativity, Mult-zero,
pred-rmergeprovedall subs proved commutativity, associativity, one, dist-rsplit,
dist-sub-mergeprovedall subs proved commutativity, associativity, dist-rsplit,
neq-not-zero-01provedall subs proved commutativity, associativity, Mult-zero,
associativityprovedall subs proved commutativity, one, dist-rsplit, Mult-zero,
oneprovedall subs proved zero-left, succ-lsplit,
commutativityprovedall subs proved succ-lsplit, succ-rsplit, zero-left, Mult-zero,
dist-rmergeprovedall subs proved dist-rsplit,
succ-lsplitprovedall subs proved succ-rsplit, Mult-zero,
zero-leftprovedall subs proved succ-rsplit,
dist-rsplitprovedall subs proved succ-rsplit, Mult-zero,
succ-rsplitprovedall subs proved Mult-succ,
Mult-succaxiom
Mult-zeroaxiom