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: |
|---|
| trim-number-01 | proved | all subs proved
| natstring-chars,
right-trim-app,
trim-number,
|
| right-trim-app | proved | all subs proved
| butlast-in,
butlast-length,
butlast-app,
last-in,
last-app,
right-trim-rec,
|
| butlast-in | proved | all subs proved
| char-in-01,
char-in,
butlast-def,
|
| natstring-chars | proved | all subs proved
| char-in-app,
char-in-one,
in-def,
|
| last-in | proved | all subs proved
| char-in-rec,
last-def,
|
| char-in | proved | all subs proved
| char-in-rec,
char-in-empty,
|
| trim-number-02 | proved | all subs proved
| right-trim-trim,
trim-number,
|
| right-trim-trim | proved | all subs proved
| butlast-length,
right-trim-done,
right-trim-empty,
right-trim-rec,
|
| char-in-app | proved | all subs proved
| char-in-01,
in-def,
|
| char-in-rec | proved | all subs proved
| char-in-01,
in-def,
|
| test-downcaseFirst | proved | all subs proved
| downcase-A,
String-downcaseFirst-def,
|
| substring-app-rec | proved | all subs proved
| substring-offset-rec,
|
| prefix-empty-01 | proved | all subs proved
| prefix-def,
prefix-empty,
|
| downcase-A | proved | all subs proved
| Char-downcase-yes,
|
| substring-offset-rec | proved | all subs proved
| substring-def,
|
| last-app | proved | all subs proved
| last-def,
|
| butlast-app | proved | all subs proved
| butlast-def,
|
| butlast-length | proved | all subs proved
| butlast-def,
|
| prefix-empty | proved | all subs proved
| prefix-def,
|
| char-in-one | proved | all subs proved
| in-def,
|
| char-in-empty | proved | all subs proved
| in-def,
|
| char-in-01 | proved | all subs proved
| in-def,
|
| upcase-a | proved | all subs proved
| Char-upcase-yes,
|
| substring-zero-rec | proved | all subs proved
| substring-def,
|
| substring-all | proved | all subs proved
| substring-def,
|
| prefix-reflexive | proved | all subs proved
| prefix-def,
|
| prefix-num-01 | proved | all subs proved
| prefix-def,
|
| prefix-num | proved | all subs proved
| prefix-def,
|
| downcase-rec | proved | all subs proved
| String-downcase-rec,
|
| downcase-lower-a | proved | all subs proved
| Char-downcase-no,
|
| downcase-C | proved | all subs proved
| Char-downcase-yes,
|
| downcase-B | proved | all subs proved
| Char-downcase-yes,
|
| Char-upcase-yes | axiom | | |
| trim-number | axiom | | |
| String-downcaseFirst-def | axiom | | |
| substring-def | axiom | | |
| right-trim-empty | axiom | | |
| right-trim-done | axiom | | |
| right-trim-rec | axiom | | |
| prefix-def | axiom | | |
| last-def | axiom | | |
| String-downcase-rec | axiom | | |
| Char-downcase-no | axiom | | |
| Char-downcase-yes | axiom | | |
| in-def | axiom | | |
| butlast-def | axiom | | |