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: |
|---|
| dups-05 | proved | all subs proved
| set2set,
dups,
dups-03,
|
| dups-04 | proved | all subs proved
| set2set,
dups,
dups-03,
|
| dups-03 | proved | all subs proved
| intempty,
dups-02,
|
| intempty-01 | proved | all subs proved
| intempty-02,
|
| dups-01 | proved | all subs proved
| in-01,
dups,
|
| intempty-02 | proved | all subs proved
| in,
|
| dups-02 | proved | all subs proved
| in,
|
| intempty | proved | all subs proved
| in,
|
| dups | proved | all subs proved
| in-01,
set2list-empty,
set2list-rec,
|
| in-union | proved | all subs proved
| in,
|
| firstN-01 | proved | all subs proved
| in,
|
| set2set | proved | all subs proved
| list2set-rec,
list2set-empty,
set2list-empty,
set2list-rec,
|
| in | proved | all subs proved
| list2set-rec,
list2set-empty,
|
| in-01 | proved | all subs proved
| set2list-empty,
set2list-rec,
|
| subset | proved | all subs proved
| list2set-rec,
|
| set2list-one | proved | all subs proved
| set2list-empty,
set2list-rec,
|
| list2set-one | proved | all subs proved
| list2set-empty,
list2set-rec,
|
| list2set-empty-01 | proved | all subs proved
| list2set-rec,
list2set-empty,
|
| list2set-append | proved | all subs proved
| list2set-rec,
list2set-empty,
|
| len | proved | all subs proved
| set2list-empty,
set2list-rec,
|
| firstN | proved | all subs proved
| list2set-rec,
list2set-empty,
|
| empty | proved | all subs proved
| set2list-empty,
set2list-rec,
|
| list2set-empty | axiom | | |
| list2set-rec | axiom | | |
| set2list-rec | axiom | | |
| set2list-empty | axiom | | |