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: |
|---|
| exlarger | proved | all subs proved
| less-append,
|
| val-total-01 | proved | all subs proved
| insorted,
eqpos,
Char-less,
|
| eqpos | proved | all subs proved
| length-one,
len-app,
|
| less-append | proved | all subs proved
| Char-irref,
Less-rec,
less-empty,
Irreflexivity,
|
| val-trans | proved | all subs proved
| Char-irref,
val-trans-01,
Less-rec,
Less-notempty,
less-empty,
|
| val-total | proved | all subs proved
| Char-irref,
Char-total,
Less-rec,
Less-empty,
less-empty,
|
| length-one | proved | all subs proved
| len-str,
|
| insorted | proved | all subs proved
| pos-str-03,
pos-str-02,
len-str-01,
Sortedchars,
|
| less-empty | proved | all subs proved
| Less-empty,
|
| val-trans-01 | proved | all subs proved
| Char-trans,
|
| pos-z | proved | all subs proved
| pos-str-03,
pos-str-02,
Sortedchars,
|
| pos-capital-z | proved | all subs proved
| pos-str-03,
pos-str-02,
Sortedchars,
|
| pos-1 | proved | all subs proved
| pos-str-03,
pos-str-02,
Sortedchars,
|
| neq-one | proved | all subs proved
| len-app,
|
| pos-2 | proved | all subs proved
| pos-str-03,
pos-str-02,
Sortedchars,
|
| pos-0 | proved | all subs proved
| pos-str-03,
pos-str-02,
Sortedchars,
|
| pos-capital-b | proved | all subs proved
| pos-str-03,
pos-str-02,
Sortedchars,
|
| pos-capital-c | proved | all subs proved
| pos-str-03,
pos-str-02,
Sortedchars,
|
| pos-capital-a | proved | all subs proved
| pos-str-03,
pos-str-02,
Sortedchars,
|
| val-irref | proved | all subs proved
| Char-irref,
Less-rec,
|
| eq-one | proved | all subs proved
| len-app,
|
| sortedchars-divided | proved | all subs proved
| Sortedchars,
|
| pos-c | proved | all subs proved
| pos-str-03,
pos-str-02,
Sortedchars,
|
| pos-a | proved | all subs proved
| pos-str-03,
pos-str-02,
Sortedchars,
|
| pos-b | proved | all subs proved
| pos-str-03,
pos-str-02,
Sortedchars,
|
| Irreflexivity | axiom | | |
| len-str-01 | proved | all subs proved
| |
| len-str | proved | all subs proved
| |
| Char-total | axiom | | |
| Char-less | axiom | | |
| len-app | proved | all subs proved
| |
| Sortedchars | axiom | | |
| pos-str-02 | proved | all subs proved
| |
| pos-str-03 | proved | all subs proved
| |
| Less-notempty | axiom | | |
| Less-rec | axiom | | |
| Char-irref | axiom | | |
| Char-trans | axiom | | |
| Less-empty | axiom | | |