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: |
|---|
| eq-zero | proved | all subs proved
| equality-any,
|
| equality-any | proved | all subs proved
| eq-same,
mkDecimal-zero,
scale-base,
scale-zero,
intvalue-zero,
getint-zero,
intvalue-base,
Equality,
mkDecimal-rec,
|
| test-truncate-01 | proved | all subs proved
| intvalue-base,
eq-same,
scale-base,
truncate-really-def,
|
| test-inc-01 | proved | all subs proved
| eq-same,
mkDecimal-rec,
scale-base,
intvalue-base,
inc-def,
|
| eq-same | proved | all subs proved
| scale-neq-01,
intvalue-zero,
scale-zero,
intvalue-rec,
intvalue-base,
scale-base,
mkDecimal-rec,
Equality,
|
| mkDecimal-negated | proved | all subs proved
| mkDecimal-constructor,
getint-neg-01,
scale-negate,
Equality,
|
| mkDecimal-maxScale-le | proved | all subs proved
| scale-base,
maxScale-zero,
maxScale-zero-01,
intvalue-base,
mkDecimal-maxScale-le-scale,
mkDecimal-maxScale-le-int,
Equality,
|
| mkDecimal-constructor | proved | all subs proved
| mkDecimal-selectors,
|
| mkDecimal-maxScale-le-int | proved | all subs proved
| maxScale-rec,
maxScale-le-zero,
maxScale-base,
maxScale-not-negt,
intvalue-base,
maxScale-zero,
intvalue-zero,
intvalue-rec,
|
| mkDecimal-maxScale-le-scale | proved | all subs proved
| maxScale-base,
maxScale-zero,
maxScale-le-zero,
maxScale-rec,
scale-rec,
scale-base,
|
| scale-neq-01 | proved | all subs proved
| scale-neq,
|
| mkDecimal-reduce-int | proved | all subs proved
| maxScale-not-negt,
maxScale-rec,
maxScale-base,
maxScale-zero,
maxScale-min,
intvalue-base,
intvalue-rec,
|
| getint-neg-02 | proved | all subs proved
| getint-pos-01,
intvalue-zero,
intvalue-base,
mkDecimal-rec,
|
| ex-mkDecimal | proved | all subs proved
| scale-not-neg,
mkDecimal-selectors,
|
| dec2int-def-any | proved | all subs proved
| dec2int-zero-01,
scale-base,
intvalue-base,
dec2int-def,
dec2int-zero,
mkDecimal-rec,
|
| scale-neq | proved | all subs proved
| scale-le,
|
| maxScale-min | proved | all subs proved
| maxScale-not-negt,
|
| scale-negate | proved | all subs proved
| scale-zero,
scale-base,
mkDecimal-rec,
|
| getint-neg-01 | proved | all subs proved
| getint-neg,
|
| maxScale-le-zero | proved | all subs proved
| maxScale-not-negt,
|
| maxScale-zero-01 | proved | all subs proved
| maxScale-not-negt,
maxScale-base,
maxScale-rec,
maxScale-zero,
|
| getint-pos-01 | proved | all subs proved
| getint-pos,
intvalue-zero,
getint-zero,
|
| mkDecimal-selectors | proved | all subs proved
| Equality,
scale-rec,
mkDecimal-scale-not-neg,
scale-base,
intvalue-base,
intvalue-rec,
gen,
|
| dec2int-zero | proved | all subs proved
| scale-base,
scale-not-neg,
intvalue-base,
dec2int-def,
|
| mkDecimal-reduce-scale | proved | all subs proved
| maxScale-rec,
maxScale-base,
maxScale-zero,
maxScale-not-negt,
scale-base,
scale-rec,
|
| mkDecimal-maxScale-nle | proved | all subs proved
| intvalue-base,
scale-base,
mkDecimal-maxScale-nle-int,
mkDecimal-maxScale-nle-scale,
Equality,
|
| mkDecimal-enlarge | proved | all subs proved
| mkDecimal-rec,
mkDecimal-scale-not-neg,
|
| maxScale-pot10-nls | proved | all subs proved
| maxScale-rec,
maxScale-not-negt,
|
| maxScale-pot10-add | proved | all subs proved
| maxScale-pot10-01,
|
| scale-le | proved | all subs proved
| scale-base,
scale-zero,
scale-rec,
|
| mkDecimal-maxScale-nle-scale | proved | all subs proved
| maxScale-rec,
scale-base,
maxScale-base,
scale-zero,
scale-rec,
|
| mkDecimal-maxScale-nle-int | proved | all subs proved
| maxScale-rec,
intvalue-base,
maxScale-base,
maxScale-zero,
intvalue-zero,
intvalue-rec,
|
| mkDecimal-scale-not-neg | proved | all subs proved
| scale-base,
scale-zero,
scale-rec,
intvalue-rec,
intvalue-base,
Equality,
|
| maxScale-pot10-01 | proved | all subs proved
| maxScale-rec,
maxScale-zero,
maxScale-base,
|
| maxScale-not-negt | proved | all subs proved
| maxScale-base,
maxScale-zero,
maxScale-rec,
|
| getint-pos | proved | all subs proved
| intvalue-base,
intvalue-zero,
intvalue-rec,
|
| getint-neg | proved | all subs proved
| intvalue-base,
intvalue-zero,
intvalue-rec,
|
| getint-zero | proved | all subs proved
| intvalue-base,
intvalue-rec,
intvalue-zero,
|
| mkDecimal-zero | proved | all subs proved
| scale-zero,
intvalue-zero,
Equality,
|
| scale-not-neg | proved | all subs proved
| scale-rec,
scale-base,
gen,
|
| mkDecimal-rec | proved | all subs proved
| scale-rec,
scale-zero,
intvalue-zero,
intvalue-rec,
Equality,
|
| dec2int-zero-01 | proved | all subs proved
| scale-zero,
intvalue-zero,
dec2int-def,
|
| maxScale-pot10-02 | proved | all subs proved
| maxScale-zero,
maxScale-rec,
|
| maxScale-pot10 | proved | all subs proved
| maxScale-zero,
maxScale-rec,
maxScale-base,
|
| intvalue-mod-10 | proved | all subs proved
| scale-base,
scale-zero,
scale-rec,
intvalue-rec,
intvalue-base,
gen,
|
| truncate-really-def | axiom | | |
| inc-def | axiom | | |
| maxScale-rec | axiom | | |
| maxScale-zero | axiom | | |
| maxScale-base | axiom | | |
| gen | axiom | | |
| scale-rec | axiom | | |
| Equality | axiom | | |
| intvalue-rec | axiom | | |
| intvalue-zero | axiom | | |
| scale-zero | axiom | | |
| dec2int-def | axiom | | |
| intvalue-base | axiom | | |
| scale-base | axiom | | |