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: |
|---|
| mult-pos | proved | all subs proved
| mult-c,
mult-a,
mult-pos-02,
le-def,
|
| mult-pos-02 | proved | all subs proved
| ls-zero-01,
mult-def-any,
le-zero,
ls-le-trans,
|
| le-trans | proved | all subs proved
| less-irref,
le-ls-trans,
le-ls-neq,
|
| add-pos | proved | all subs proved
| less-irref,
le-ls-trans,
add-c,
add-a,
ls-add-02,
ls-le-trans,
le-def,
|
| ls-le-trans | proved | all subs proved
| less-trans,
le-ls-neq,
|
| le-ls-trans | proved | all subs proved
| less-trans,
le-ls-neq,
|
| le-ls-neq | proved | all subs proved
| less-irref,
less-trans,
less-totality,
le-def,
|
| ls-add-02 | proved | all subs proved
| add-c,
add-a,
ls-add,
|
| le-add-01 | proved | all subs proved
| add-c,
add-a,
ls-add,
le-def,
|
| le-add | proved | all subs proved
| add-c,
add-a,
ls-add-01,
le-def,
|
| less-totality | proved | all subs proved
| less-same,
|
| less-trans | proved | all subs proved
| less-same,
|
| ls-add | proved | all subs proved
| less-def-any,
less-same,
ls-not,
add-def-any,
|
| ls-add-01 | proved | all subs proved
| less-def-any,
less-same,
ls-not,
add-def-any,
|
| square-sqrt-01 | proved | all subs proved
| square-abs,
mult-c,
mult-a,
square-int-nlz,
scale-abs,
getint-abs,
mult-abs,
abs-not-neg,
square-sqrt,
|
| mult-le | proved | all subs proved
| mult-c,
mult-a,
mult-ls,
le-def,
|
| le-same | proved | all subs proved
| less-same,
le-def,
|
| abs-neg | proved | all subs proved
| neg-any-def,
ls-zero-01,
abs-any-def,
|
| square-abs | proved | all subs proved
| le-zero,
abs-pos,
mult-def-any,
mult-c,
mult-a,
mult-abs,
|
| mult-ls | proved | all subs proved
| less-def-any,
mult-def-any,
ls-zero,
|
| less-same | proved | all subs proved
| sub-same,
ls-def,
|
| ls-zero-01 | proved | all subs proved
| less-def-any,
|
| square-pos-01 | proved | all subs proved
| le-def,
mult-def-any,
ls-not,
ls-zero,
mult-c,
mult-a,
mult-zero-01,
|
| square-ls | proved | all subs proved
| abs-any-def,
ls-not,
less-def-any,
mult-def-any,
|
| abs-zero | proved | all subs proved
| le-zero,
abs-pos,
|
| square-sqrt | proved | all subs proved
| mult-def-any,
le-zero,
|
| abs-not-neg | proved | all subs proved
| le-zero,
abs-any-def,
|
| ls-zero | proved | all subs proved
| sub-def-any,
ls-def,
|
| less-def-any | proved | all subs proved
| sub-def-any,
ls-def,
|
| sub-same | proved | all subs proved
| sub-def-any,
|
| add-a | proved | all subs proved
| add-def-any,
|
| abs-pos | proved | all subs proved
| abs-any-def,
le-zero,
|
| sub-add | proved | all subs proved
| sub-def-any,
add-def-any,
|
| square-scale-01 | proved | all subs proved
| square-scale,
|
| square-pos | proved | all subs proved
| le-zero,
mult-def-any,
|
| mult-dist | proved | all subs proved
| mult-def-any,
add-def-any,
|
| le-ref | proved | all subs proved
| less-irref,
le-def,
|
| dec2int-not-neg | proved | all subs proved
| le-pos,
|
| add-same | proved | all subs proved
| add-def-any,
|
| square-int-nlz | proved | all subs proved
| mult-def-any,
|
| square-scale | proved | all subs proved
| mult-def-any,
|
| mult-abs | proved | all subs proved
| abs-any-def,
scale-abs,
getint-abs,
mult-def,
|
| mult-a | proved | all subs proved
| mult-def-any,
|
| sub-def-any | proved | all subs proved
| sub-zero,
sub-def,
|
| le-pos | proved | all subs proved
| sub-zero,
ls-def,
le-def,
|
| less-irref | proved | all subs proved
| sub-id,
ls-def,
|
| add-def-any | proved | all subs proved
| add-c,
add-zero-01,
add-def,
|
| le-zero | proved | all subs proved
| sub-zero,
ls-def,
le-def,
|
| square-sqrt-02 | proved | all subs proved
| mult-def-any,
|
| square-isSquare | proved | all subs proved
| mult-def-any,
|
| mult-eq-same | proved | all subs proved
| mult-def-any,
|
| mult-zero-01 | proved | all subs proved
| mult-def,
|
| mult-c | proved | all subs proved
| mult-def,
|
| getint-abs | proved | all subs proved
| abs-def,
|
| scale-abs | proved | all subs proved
| abs-def,
|
| mult-def-any | proved | all subs proved
| mult-def,
|
| ls-not | proved | all subs proved
| le-def,
|
| sub-id | proved | all subs proved
| sub-def,
|
| sub-zero | proved | all subs proved
| sub-def,
|
| add-zero-01 | proved | all subs proved
| add-def,
|
| add-c | proved | all subs proved
| add-def,
|
| abs-any-def | proved | all subs proved
| abs-def,
|
| neg-any-def | proved | all subs proved
| neg-def,
|
| mult-zero | proved | all subs proved
| mult-def,
zero-def,
|
| mult-one | proved | all subs proved
| mult-def,
one-def,
|
| add-zero | proved | all subs proved
| add-def,
zero-def,
|
| add-scale-neq | proved | all subs proved
| add-def,
|
| add-scale-eq | proved | all subs proved
| add-def,
|
| sub-def | axiom | | |
| neg-def | axiom | | |
| one-def | axiom | | |
| mult-def | axiom | | |
| ls-def | axiom | | |
| zero-def | axiom | | |
| le-def | axiom | | |
| add-def | axiom | | |
| abs-def | axiom | | |