[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 real-multdiv

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:
square-le-05provedall subs proved mult-com, mult-ass, mult-one, distr, square-le-05a, two-def,
square-interval-01provedall subs proved two-def, square-interval, mult-com, mult-ass, mult-one, distr,
square-intervalprovedall subs proved zero-ls-02, le-posint, square-le-04, mult-com, mult-ass, mult-one, distr,
square-le-05aprovedall subs proved mult-com, mult-ass, mult-one, distr, square-le-04,
square-ls-03provedall subs proved mult-com, mult-ass, mult-one, distr, square-ls-03a, two-def,
square-ls-04aprovedall subs proved mult-com, mult-ass, mult-one, distr, square-ls-04,
square-eq-oneprovedall subs proved abs-ite, mult-com, mult-ass, mult-one, square-eq,
square-le-oneprovedall subs proved mult-com, mult-ass, ls-same-05, square-gr-one, abs-ite, mult-one, square-le,
square-gr-oneprovedall subs proved ls-same-05, abs-ite, mult-com, mult-ass, mult-one, square-ls,
square-eqprovedall subs proved abs-ite, square-ls,
square-ls-04provedall subs proved square-ge-one, two-def, mult-com, mult-ass, mult-one, distr,
square-ls-03aprovedall subs proved mult-com, mult-ass, mult-one, distr, square-ls-02,
square-le-04provedall subs proved square-ls, mult-com, mult-ass, mult-one, distr,
square-zero-01aprovedall subs proved mult-com, mult-ass, zero-ls-02, mult-zero, num-distr-addboth-ls1, distr, mult-one, square-ls-02,
square-ls-oneprovedall subs proved abs-ite, mult-com, mult-ass, mult-one, square-ls,
square-lsprovedall subs proved abs-ite, square-le,
square-ls-02provedall subs proved mult-gt-both, square-le, mult-com, mult-ass, mult-one, distr,
square-ge-oneprovedall subs proved abs-ite, mult-com, mult-ass, mult-one, square-le,
square-gez-01provedall subs proved mult-com, mult-ass, square-gez,
twice-le-zeroprovedall subs proved mult-com, mult-ass, zero-le, zero-le-03, two-def,
square-minusprovedall subs proved mult-com, mult-ass, square-lez-01, mult-zero,
invmult-le-neg-addprovedall subs proved minus-left, distr, mult-com, mult-ass, invmult-gr-neg-add, invmult-le-neg,
invmult-le-pos-addprovedall subs proved invmult-gr-pos-add, mult-com, mult-ass, minus-left, distr, invmult-le-pos,
invmult-gr-pos-addprovedall subs proved mult-com, mult-ass, minus-left, distr, invmult-gr-pos,
invmult-gr-neg-addprovedall subs proved mult-com, mult-ass, minus-left, distr, invmult-gr-neg,
square-lez-01provedall subs proved zero-le, zero-le-01, mult-com, mult-ass, mult-zero,
zero-le-03provedall subs proved zero-gr-03, mult-com, mult-ass, zero-le-01,
square-gezprovedall subs proved mult-com, mult-ass, square-lez,
square-leprovedall subs proved ls-pos-01, ls-forward, zero-ls-01, ls-pos, ls-neg, zero-le, le-pos-01, zero-le-01, mult-zero, le-pos, ple-pos, le-neg-01, minus-left, mult-com, mult-ass, le-neg, abs-ite,
inv-twiceprovedall subs proved inv-eq, mult-zero, mult-com, mult-ass, inv-def,
square-ls-01provedall subs proved mult-com, mult-ass, square-lez,
inv-gr-posprovedall subs proved inv-le-pos,
abs-eqallprovedall subs proved eq-nonzero, neq-not-zero, zero-ge-02, zero-neq, zero-ge-01, zero-ls-02, mult-com, mult-ass, zero-ls-01, eq-neg, minus-left, abs-ite,
abs-le-one-multipleprovedall subs proved ls-same, ls-same-03, mult-zero, le-same-01, mult-com, mult-ass, le-same-02, minus-left, abs-ite,
square-zero-01provedall subs proved mult-com, mult-ass, mult-one, distr, zero-le-02, two-def,
pzero-grprovedall subs proved mult-com, mult-ass, zero-gr-03, zero-gr,
inv-gr-negprovedall subs proved inv-le-neg,
square-eq-03provedall subs proved square-eq-02, mult-com, mult-ass, mult-one, distr,
zero-gr-caseprovedall subs proved zero-le-01, zero-le, mult-com, mult-ass, zero-gr-03,
zero-le-caseprovedall subs proved zero-gr, mult-zero, zero-le, mult-com, mult-ass, zero-le-01,
zero-ge-03provedall subs proved zero-ls-03, mult-com, mult-ass, zero-ge-01,
pzero-lsprovedall subs proved mult-com, mult-ass, zero-ge, zero-ge-02,
invmult-ls-neg-addprovedall subs proved invmult-ge-neg-add, mult-com, mult-ass, minus-left, distr, invmult-ls-neg,
square-le-03provedall subs proved mult-com, mult-ass, square-lez,
abs-ls-multiple-oneprovedall subs proved le-same-01, le-same-02, ls-same, ls-same-03, minus-left, mult-com, mult-ass, mult-zero, abs-ite,
invmult-ls-pos-addprovedall subs proved minus-left, distr, mult-com, mult-ass, invmult-ge-pos-add, invmult-ls-pos,
ls-twoprovedall subs proved mult-com, mult-ass, zero-ge-01,
zero-ge-caseprovedall subs proved zero-ls, zero-ls-01, mult-zero, mult-com, mult-ass, zero-ge-01,
invmult-ge-pos-addprovedall subs proved mult-com, mult-ass, minus-left, distr, invmult-ge-pos,
invmult-ge-neg-addprovedall subs proved mult-com, mult-ass, minus-left, distr, invmult-ge-neg,
square-eq-02provedall subs proved square-eq-01, two-def, mult-com, mult-ass, mult-zero, num-distr-addboth-eq1, mult-one, distr,
inv-le-negprovedall subs proved le-neg-01, mult-com, mult-ass, inv-def,
invmult-gr-negprovedall subs proved mult-com, mult-ass, invmult-le-neg,
ls-same-05provedall subs proved le-same-01, mult-com, ls-same-04,
zero-le-02provedall subs proved zero-gr-02, mult-com, mult-ass, zero-le,
le-same-02provedall subs proved eq-same-03, mult-com, mult-ass, mult-one, ls-neg,
invmult-gr-posprovedall subs proved mult-com, mult-ass, invmult-le-pos,
zero-le-01provedall subs proved zero-gr-01, mult-com, mult-ass, minus-left, zero-le,
zero-gr-03provedall subs proved zero-gr-01, mult-com, mult-ass, mult-zero, zero-gr-02,
zero-ge-01provedall subs proved zero-ls-01, mult-com, mult-ass, zero-ge,
zero-ge-02provedall subs proved zero-ls-02, mult-com, mult-ass, zero-ge,
inv-le-posprovedall subs proved le-pos-01, mult-com, mult-ass, inv-def,
square-lezprovedall subs proved minus-left, mult-com, mult-ass, zero-ls-02, order,
inv-eqprovedall subs proved eq-neg-01, eq-pos-01, mult-com, mult-ass, inv-def,
zero-ge-add-01provedall subs proved mult-com, mult-ass, zero-ls-02,
abs-ls-one-multipleprovedall subs proved le-same, le-same-03, ls-same-01, ls-same-02, minus-left, mult-com, mult-ass, mult-zero, abs-ite,
ls-two-01provedall subs proved mult-com, mult-ass, zero-gr-01,
ls-two-02provedall subs proved mult-com, mult-ass, zero-gr-01,
ls-two-03provedall subs proved mult-com, mult-ass, zero-gr-01,
zero-ls-caseprovedall subs proved zero-ge, zero-ls-03, mult-com, mult-ass, zero-ls-02,
mult-gt-oneprovedall subs proved mult-com, mult-ass, le-same,
inv-ge-negprovedall subs proved inv-ls-neg,
square-zero-02provedall subs proved mult-com, mult-ass, mult-one, distr, zero-ls-02,
abs-ls-sameprovedall subs proved ls-same, zero-ls-02, mult-com, mult-ass, ls-same-02, minus-left, zero-gr-01, abs-ite,
zero-gr-add-01provedall subs proved mult-com, mult-ass, zero-gr-01,
mult-posprovedall subs proved mult-com, mult-ass, zero-gr-01,
square-zeroprovedall subs proved mult-com, mult-ass, mult-zero, zero-eq,
square-absprovedall subs proved zero-ls-02, mult-com, mult-ass, eq-neg, zero-ls-01, abs-ite,
twice-ls-zeroprovedall subs proved mult-com, mult-ass, zero-ls-02, zero-ls-01,
mods-zero-07provedall subs proved mult-zero, zero-gr-02, mult-com, mult-ass, zero-ls-02,
inv-ge-posprovedall subs proved inv-ls-pos,
two-le-02provedall subs proved mult-com, mult-ass, le-posint, mult-zero, num-distr-addboth-le1, distr,
le-same-04provedall subs proved ls-same-01, ls-same-02, mult-zero, le-same, mult-com, mult-ass, le-same-03, minus-left, abs-ite,
le-same-06provedall subs proved mult-com, mult-ass, le-same,
le-same-05provedall subs proved le-same, le-same-03, minus-left, mult-com, mult-ass, mult-zero, abs-ite,
abs-not-negprovedall subs proved zero-ls-02, mult-com, mult-ass, zero-gr-01, minus-left, abs-ite,
mult-pos-posprovedall subs proved mult-com, mult-ass, mult-one, eq-same-02,
eq-same-02provedall subs proved mult-com, mult-ass, mult-one, eq-same,
ls-same-04provedall subs proved mult-com, mult-ass, ls-same,
eq-same-03provedall subs proved mult-com, mult-ass, mult-one, eq-same,
invmult-le-posprovedall subs proved le-pos, mult-ass, mult-com, mult-one, inv-def,
eq-pos-01provedall subs proved mult-com, mult-ass, eq-pos,
eq-neg-01provedall subs proved mult-com, eq-neg,
inv-ls-posprovedall subs proved ls-pos-01, mult-com, mult-ass, inv-def,
invmult-ge-negprovedall subs proved mult-com, mult-ass, invmult-ls-neg,
zero-eqprovedall subs proved mult-com, mult-ass, mult-zero, zero-neq-01, zero-neq,
le-posintprovedall subs proved le-pos,
square-eq-01provedall subs proved mult-gt-both, mult-com, mult-ass, mult-one, distr,
invmult-ge-posprovedall subs proved mult-com, mult-ass, invmult-ls-pos,
invmult-le-negprovedall subs proved le-neg, mult-ass, mult-com, mult-one, inv-def,
le-same-01provedall subs proved ls-same, mult-one, le-pos, mult-com, mult-ass, zero-gr,
le-neg-01provedall subs proved mult-com, mult-ass, le-neg,
le-pos-01provedall subs proved mult-com, mult-ass, le-pos,
inv-ls-negprovedall subs proved ls-neg-01, mult-com, mult-ass, inv-def,
zero-geprovedall subs proved mult-com, mult-ass, mult-zero, le-pos,
zero-ls-01provedall subs proved mult-com, mult-ass, zero-ls-03, zero-ls,
zero-leprovedall subs proved mult-com, mult-ass, mult-zero, le-pos,
le-same-03provedall subs proved mult-com, mult-ass, mult-one, le-neg,
le-sameprovedall subs proved mult-com, mult-ass, mult-one, le-pos,
zero-ls-02provedall subs proved mult-com, mult-ass, zero-ls, mult-zero,
zero-gr-02provedall subs proved mult-com, mult-ass, zero-gr, mult-zero,
zero-gr-01provedall subs proved mult-zero, zero-gr, mult-com, mult-ass, minus-left, order,
mods-lsprovedall subs proved mult-com, mult-ass, le-pos,
zero-ge-add-02provedall subs proved mult-zero, zero-ls, mult-com, mult-ass, mult-one, distr, ls-pos,
pnle-posprovedall subs proved mult-com, mult-ass, ls-pos, ls-forward, le-pos,
two-ls-02provedall subs proved mult-com, mult-ass, ls-posint, mult-zero, num-distr-addboth-ls1, distr, two-def,
eq-same-01provedall subs proved mult-com, mult-ass, mult-one, eq-same,
mult-add-greaterprovedall subs proved mult-com, mult-ass, zero-ls, distr,
noeth-zero-lsprovedall subs proved mult-com, mult-ass, zero-gr, abs-ite,
two-eqprovedall subs proved mult-com, mult-ass, eq-nonzero-int,
le-negintprovedall subs proved le-neg,
pls-negprovedall subs proved mult-com, mult-ass, eq-neg, ls-neg,
pnle-negprovedall subs proved mult-com, mult-ass, le-neg,
inv-multprovedall subs proved inv-def, mult-one, eq-nonzero-02, mult-com, mult-ass,
le-absprovedall subs proved ls-neg, ls-pos, ls-forward, le-pos, mult-com, mult-ass, le-neg, minus-left, abs-ite,
eq-nonzero-02provedall subs proved mult-com, mult-ass, eq-nonzero,
eq-nonzero-intprovedall subs proved eq-nonzero,
ls-neg-01provedall subs proved mult-com, ls-neg,
eq-posprovedall subs proved eq-nonzero,
invmult-ls-negprovedall subs proved ls-neg, mult-ass, mult-com, mult-one, inv-def,
ls-same-03provedall subs proved mult-com, mult-ass, mult-one, ls-neg,
ls-sameprovedall subs proved mult-com, mult-ass, mult-one, ls-pos,
le-negprovedall subs proved mult-com, mult-ass, ls-neg, minus-left, distr, order,
ple-posprovedall subs proved mult-com, mult-ass, ls-pos,
ls-pos-01provedall subs proved mult-com, mult-ass, ls-pos,
zero-grprovedall subs proved mult-com, mult-ass, mult-zero, ls-pos,
invmult-ls-posprovedall subs proved invmult-eq, mult-ass, mult-com, mult-one, inv-def, ls-pos,
zero-ls-03provedall subs proved mult-com, mult-ass, mult-zero, ls-neg,
eq-negprovedall subs proved eq-nonzero,
zero-neqprovedall subs proved minus-left, zero-neq-01, mult-com, mult-ass, mult-zero,
eq-sameprovedall subs proved mult-zero, mult-com, mult-ass, mult-one, eq-nonzero,
ls-posintprovedall subs proved ls-pos,
ls-same-02provedall subs proved mult-com, mult-ass, mult-one, ls-neg,
ls-same-01provedall subs proved mult-com, mult-ass, mult-one, ls-pos,
mult-gt-bothprovedall subs proved mult-com, mult-ass, ls-pos, ls-forward,
zero-lsprovedall subs proved mult-com, mult-ass, mult-zero, ls-pos,
le-posprovedall subs proved mult-ass, ls-pos, minus-left, mult-com, distr, order,
pls-posprovedall subs proved mult-com, mult-ass, ls-pos, ls-forward,
est-nleprovedall subs proved mult-com, mult-ass, ls-pos, ls-forward,
two-sub-01provedall subs proved mult-com, mult-ass, two-sub, minus-left,
eq-nonzero-03provedall subs proved mult-com, mult-ass, eq-nonzero,
eq-nonzero-01provedall subs proved mult-com, mult-ass, eq-nonzero,
two-sub-03provedall subs proved mult-com, mult-ass, mult-zero, num-distr-addboth-eq1, two-sub, distr, two-def,
two-sub-02provedall subs proved mult-com, mult-ass, two-sub, minus-left, two-def,
two-sub-05provedall subs proved mult-com, mult-ass, two-sub, minus-left, distr, two-def,
two-sub-04provedall subs proved mult-com, mult-ass, two-sub, mult-zero, num-distr-addboth-eq1, minus-left, distr, two-def,
pnls-posprovedall subs proved mult-com, mult-ass, ls-pos, ls-forward,
ple-pos-betterprovedall subs proved mult-com, mult-ass, ls-pos, ls-forward,
ple-negprovedall subs proved mult-com, mult-ass, ls-neg,
pnls-posnegprovedall subs proved mult-com, mult-ass, ls-neg, ls-forward, ls-pos,
pnls-negposprovedall subs proved mult-com, mult-ass, ls-neg, ls-forward, ls-pos,
ls-negintprovedall subs proved ls-neg,
pls-pos-02provedall subs proved mult-com, mult-ass, ls-pos, ls-forward,
pls-pos-01provedall subs proved mult-com, mult-ass, ls-pos, ls-forward,
ls-pos-02provedall subs proved mult-com, mult-ass, ls-pos, abs-ite,
pnls-negprovedall subs proved mult-com, mult-ass, ls-neg,
ls-negprovedall subs proved minus-left, distr, order, mult-com, mult-ass, ls-forward,
eq-nonzeroprovedall subs proved mult-one, inv-def, mult-com, mult-ass, minus-left, distr,
two-subprovedall subs proved minus-left, mult-com, mult-ass, mult-one, num-distr,
zero-neq-01provedall subs proved minus-left, order, mult-com, mult-ass, mult-zero,
ls-posprovedall subs proved mult-com, mult-ass, ls-forward, minus-left, distr, order,
abs-eqnegprovedall subs proved mult-com, mult-ass, minus-left, abs-ite,
inv-mult-add-eqprovedall subs proved mult-com, mult-ass, minus-left,
minus-one-01provedall subs proved mult-com, mult-ass, mult-one, minus-left,
neq-not-zeroprovedall subs proved mult-com, mult-ass, mult-zero,
minus-leftprovedall subs proved mult-ass, mult-zero, distr, mult-com,
ls-forwardprovedall subs proved mult-com, mult-ass, mult-zero,
two-lsprovedall subs proved mult-com, mult-ass, mult-zero, num-distr-addboth-ls1, distr,
two-leprovedall subs proved mult-com, mult-ass, mult-zero, num-distr-addboth-le1, distr,
two-ls-01provedall subs proved mult-com, mult-ass, mult-zero, num-distr-addboth-ls1, distr,
two-ls-03provedall subs proved mult-com, mult-ass, mult-zero, num-distr-addboth-ls1, distr,
two-ls-04provedall subs proved mult-com, mult-ass, mult-zero, num-distr-addboth-ls1, distr,
minus-oneprovedall subs proved mult-zero, mult-com, mult-ass, mult-one, distr,
two-le-01provedall subs proved mult-com, mult-ass, mult-zero, num-distr-addboth-le1, distr,
two-le-03provedall subs proved mult-com, mult-ass, mult-zero, num-distr-addboth-le1, distr,
two-le-04provedall subs proved mult-com, mult-ass, mult-zero, num-distr-addboth-le1, distr,
neq-not-zero-01provedall subs proved mult-com, mult-ass, mult-zero,
posint-factorprovedall subs proved mult-com, mult-ass, mult-zero, num-distr,
mult-zeroprovedall subs proved mult-com, mult-ass, num-distr-eq1,
add-mult-twoprovedall subs proved mult-com, mult-ass, mult-one, succ-lsplit, two-def,
num-distr-eq1provedall subs proved mult-com, mult-ass, distr,
succ-lsplitprovedall subs proved mult-com, mult-ass, mult-one, distr,
num-distrprovedall subs proved mult-com, mult-ass, distr,
invmult-eqprovedall subs proved mult-ass, mult-com, mult-one, inv-def,
num-distr-addboth-eq1provedall subs proved mult-com, mult-ass, distr,
num-distr-addboth-le1provedall subs proved mult-com, mult-ass, distr,
num-distr-addboth-ls1provedall subs proved mult-com, mult-ass, distr,
num-distr-le1provedall subs proved mult-com, mult-ass, distr,
num-distr-le2provedall subs proved mult-com, mult-ass, distr,
num-distr-addboth-ls2provedall subs proved mult-com, mult-ass, distr,
ls-distprovedall subs proved mult-com, mult-ass, distr,
num-distr-add-eq1provedall subs proved mult-com, mult-ass, distr,
num-distr-add-eq2provedall subs proved mult-com, mult-ass, distr,
num-distr-addboth-le2provedall subs proved mult-com, mult-ass, distr,
eq-distprovedall subs proved mult-com, mult-ass, distr,
eq-succprovedall subs proved mult-com, mult-ass, mult-one, distr,
num-distr-addboth-eq2provedall subs proved mult-com, mult-ass, distr,
ls-dist-03provedall subs proved mult-com, mult-ass, mult-one, distr,
ls-dist-04provedall subs proved mult-com, mult-ass, mult-one, distr,
ls-dist-05provedall subs proved mult-com, mult-ass, mult-one, distr,
ls-dist-06provedall subs proved mult-com, mult-ass, mult-one, distr,
ls-dist-01provedall subs proved mult-com, mult-ass, distr,
ls-dist-02provedall subs proved mult-com, mult-ass, distr,
num-distr-ls1provedall subs proved mult-com, mult-ass, distr,
num-distr-ls2provedall subs proved mult-com, mult-ass, distr,
succ-rmergeprovedall subs proved mult-com, mult-ass, mult-one, distr,
le-dist-01provedall subs proved mult-com, mult-ass, distr,
le-dist-02provedall subs proved mult-com, mult-ass, distr,
ls-add-03provedall subs proved mult-com, mult-ass, distr,
ls-add-02provedall subs proved mult-com, mult-ass, distr,
num-distr-eq2provedall subs proved mult-com, mult-ass, distr,
eq-succ-01provedall subs proved mult-com, mult-ass, distr,
le-distprovedall subs proved mult-com, mult-ass, distr,
num-distr-add-ls1provedall subs proved mult-com, mult-ass, distr,
num-distr-add-ls2provedall subs proved mult-com, mult-ass, distr,
succ-rsplitprovedall subs proved mult-com, mult-ass, mult-one, distr,
num-distr-add-le1provedall subs proved mult-com, mult-ass, distr,
num-distr-add-le2provedall subs proved mult-com, mult-ass, distr,
orderaxiom
inv-defaxiom
abs-iteprovedall subs proved
two-defaxiom
distraxiom
mult-oneaxiom
mult-assaxiom
mult-comaxiom