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