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