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: |
|---|
| sqrt-isSquare | proved | all subs proved
| isSquare-square,
sqrt-exact-def,
isSquare-def,
|
| sqrt-exact-square | proved | all subs proved
| isSquare-square,
sqrt-exact-def,
|
| sqrt-exact-def | proved | all subs proved
| isSquare-isSquare,
isSquare-scale,
sqrt-even-precision-def,
|
| test-div-04 | proved | all subs proved
| test-divides-04,
div-exact-def,
div-def,
|
| test-div-03 | proved | all subs proved
| test-divides-03,
div-exact-def,
div-def,
|
| test-div-02 | proved | all subs proved
| test-divides-02,
div-exact-def,
div-def,
|
| test-div-01 | proved | all subs proved
| test-divides-01,
div-precision-def,
|
| test-divides-04 | proved | all subs proved
| divides-def,
|
| test-divides-03 | proved | all subs proved
| divides-def,
|
| test-divides-02 | proved | all subs proved
| divides-def,
|
| test-divides-01 | proved | all subs proved
| divides-def,
|
| isSquare-square | proved | all subs proved
| isSquare-def,
|
| isSquare-scale | proved | all subs proved
| isSquare-def,
|
| isSquare-isSquare | proved | all subs proved
| isSquare-def,
|
| test-sqrt-05 | proved | all subs proved
| sqrt-odd-precision-def,
|
| test-sqrt-04 | proved | all subs proved
| sqrt-even-precision-def,
|
| test-sqrt-03 | proved | all subs proved
| sqrt-odd-precision-def,
|
| test-sqrt-02 | proved | all subs proved
| sqrt-even-precision-def,
|
| test-sqrt-01 | proved | all subs proved
| sqrt-even-precision-def,
sqrt-def,
|
| isSquare-pos | proved | all subs proved
| isSquare-def,
|
| sqrt-odd-precision-def | axiom | | |
| sqrt-def | axiom | | |
| divides-def | axiom | | |
| div-def | axiom | | |
| div-exact-def | axiom | | |
| div-precision-def | axiom | | |
| sqrt-even-precision-def | axiom | | |
| isSquare-def | axiom | | |