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