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: |
|---|---|---|---|
| lf | proved | all subs proved | fr-07, lf-01, l, lfr, |
| fr-01 | proved | all subs proved | fr-02, fr, |
| fr | proved | all subs proved | fr-02, fr-07, |
| lfr | proved | all subs proved | fr-02, fr-07, l, |
| fr-03 | proved | all subs proved | fr-07, |
| lr-01 | proved | all subs proved | lr-02, size-add, disj-nil-add, elim-list-c, |
| le-one-01 | proved | all subs proved | sel-add-dottail, l, size-add, disj-nil-add, gen-list, fr-07, lf-01, |
| eq-one | proved | all subs proved | disj-nil-add, l, size-add, elim-list-c, fr-07, lf-01, |
| lr-02 | proved | all subs proved | l, length-rest, |
| fr-07 | proved | all subs proved | inj-add, elim-list-c, fr-02, |
| elim-list | proved | all subs proved | sel-add-dottail, sel-add-dothead, fr-02, |
| lr-04 | proved | all subs proved | l, length-rest, size-nil, |
| lr | proved | all subs proved | l, length-rest, |
| length-rest-intro | proved | all subs proved | l, length-rest, |
| lr-06 | proved | all subs proved | l, length-rest, size-nil, |
| fr-04 | proved | all subs proved | fr-02, elim-list-c, |
| lr-05 | proved | all subs proved | length-rest, l, |
| fr-02 | proved | all subs proved | elim-list-c, |
| lf-01 | proved | all subs proved | inj-add, l, size-add, disj-nil-add, size-nil, elim-list-c, |
| length-rest | proved | all subs proved | size-add, elim-list-c, |
| lr-03 | proved | all subs proved | disj-nil-add, size-add, elim-list-c, |
| elim-list-c | proved | all subs proved | f, gen-list, sel-add-dottail, sel-add-dothead, |
| le-one | proved | all subs proved | l, |
| f | proved | all subs proved | inj-add, |
| l | proved | all subs proved | size-add, gen-list, size-nil, |
| p-fr | proved | all subs proved | sel-add-dottail, sel-add-dothead, |
| exa | proved | all subs proved | disj-nil-add, gen-list, |
| inj-add | axiom | ||
| gen-list | axiom | ||
| disj-nil-add | axiom | ||
| size-nil | axiom | ||
| sel-add-dothead | axiom | ||
| sel-add-dottail | axiom | ||
| size-add | axiom |