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