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