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-one-01 | proved | all subs proved
| square-le-one,
|
| square-four | proved | all subs proved
| Square-def,
inverse-i,
Sqrt-def,
|
| square-le-one | proved | all subs proved
| Square-def,
square-not-neg,
two-ls-pospos,
Sqrt-def,
one-01,
square-two,
square-three,
|
| inverse-i | proved | all subs proved
| inverse-ii,
Square-def,
|
| root-le | proved | all subs proved
| root-nls,
Square-def,
square-nls,
|
| square-three | proved | all subs proved
| square-not-neg-02,
root-abs,
two-le-three,
Sqrt-def,
|
| square-two | proved | all subs proved
| square-not-neg-02,
root-abs,
two-le-two,
Sqrt-def,
|
| one-01 | proved | all subs proved
| root-abs,
Square-def,
Sqrt-def,
|
| square-nls | proved | all subs proved
| two-not-neg,
square-not-neg,
two-ls-pospos,
Sqrt-def,
|
| inverse-ii | proved | all subs proved
| root-pos,
root-abs,
Square-def,
Sqrt-def,
|
| two-ex | proved | all subs proved
| two-even,
|
| two-even-01 | proved | all subs proved
| add-even,
two-even,
|
| square-not-neg-03 | proved | all subs proved
| square-not-neg-02,
|
| square-not-neg-01 | proved | all subs proved
| square-not-neg,
|
| root-elim | proved | all subs proved
| root-abs,
Square-def,
Sqrt-def,
|
| euler-four-square-identity2 | proved | all subs proved
| two-plus,
two-pm,
two-minus,
|
| two-even | proved | all subs proved
| zero,
two-mult,
one,
neq,
Square-def,
two-plus,
|
| add-even | proved | all subs proved
| even,
|
| square-not-neg-02 | proved | all subs proved
| square-not-neg-05,
root-pos,
zero-01,
|
| square-not-neg | proved | all subs proved
| root-pos,
|
| root-abs | proved | all subs proved
| root-pos,
|
| two-pm | proved | all subs proved
| two-mult,
two-plus,
|
| two-identity | proved | all subs proved
| two-mult,
two-minus,
two-plus,
|
| square-not-neg-04 | proved | all subs proved
| square-not-neg-05,
|
| minus-01 | proved | all subs proved
| minus,
|
| four-square-le-zero | proved | all subs proved
| zero-i,
zero,
Square-def,
two-not-neg,
|
| euler-four-square-identity | proved | all subs proved
| two-plus,
two-mult,
two-minus,
|
| div | proved | all subs proved
| zero,
two-mult,
|
| neq | proved | all subs proved
| Square-def,
|
| one | proved | all subs proved
| Square-def,
|
| two-le-two | proved | all subs proved
| Square-def,
|
| two-le-three | proved | all subs proved
| Square-def,
|
| zero-01 | proved | all subs proved
| Square-def,
Sqrt-def,
|
| square-not-neg-05 | proved | all subs proved
| Square-def,
Sqrt-def,
|
| two-ls-pospos | proved | all subs proved
| Square-def,
|
| root-nls | proved | all subs proved
| Square-def,
Sqrt-def,
|
| minus | proved | all subs proved
| Square-def,
|
| root-pos | proved | all subs proved
| Square-def,
Sqrt-def,
|
| two-not-neg | proved | all subs proved
| Square-def,
|
| zero-i | proved | all subs proved
| Square-def,
|
| two-minus | proved | all subs proved
| Square-def,
|
| two-plus | proved | all subs proved
| Square-def,
|
| two-mult | proved | all subs proved
| Square-def,
|
| zero | proved | all subs proved
| Square-def,
|
| even | proved | all subs proved
| Square-def,
|
| two-ls | proved | all subs proved
| Square-def,
|
| positive | proved | all subs proved
| Square-def,
|
| le-plus | proved | all subs proved
| Square-def,
|
| le | proved | all subs proved
| Square-def,
|
| abs-01 | proved | all subs proved
| Square-def,
|
| abs | proved | all subs proved
| Square-def,
|
| Sqrt-def | axiom | | |
| Square-def | axiom | | |