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: |
|---|
| rm-vl-lebrefs-subseteq | proved | all subs proved
| rm-v-subseteq,
subseteq-lebrefs-subseteq,
|
| subseteq-lebrefs-subseteq | proved | all subs proved
| queue-in-vl,
in-vl-in-lebrefs,
lebrefs-rec,
lebrefs-base,
|
| rm-vl-notin | proved | all subs proved
| rm-vl-in-before-h,
queue-in-vl,
|
| rm-vl-in-before | proved | all subs proved
| queue-rm-vl-rec,
rm-vl-in-before-h,
queue-in-vl,
|
| lebrefs-none-notin | proved | all subs proved
| queue-in-vl,
in-vl-in-lebrefs,
|
| lebrefs-append-none | proved | all subs proved
| lebrefs-rec,
lebrefs-base,
lebrefs-none,
|
| lebrefs-append-lref | proved | all subs proved
| lebrefs-rec,
lebrefs-base,
lebrefs-lref,
|
| eq-entry-in-lref-in | proved | all subs proved
| queue-in-vl,
in-vl-in-lebrefs,
|
| rm-v-subseteq | proved | all subs proved
| queue-rm-v-rec,
queue-rm-v-base,
|
| rm-vl-in-before-h | proved | all subs proved
| queue-rm-vl-rec,
queue-rm-vl-base,
|
| lebrefs-none | proved | all subs proved
| lebrefs-base,
lebrefs-rec,
|
| lebrefs-lref | proved | all subs proved
| lebrefs-base,
lebrefs-rec,
|
| in-vl-in-lebrefs | proved | all subs proved
| lebrefs-rec,
lebrefs-base,
queue-in-vl,
|
| rm-vl-notin-before | proved | all subs proved
| queue-rm-vl-rec,
queue-rm-vl-base,
queue-in-vl,
|
| rm-vl-append-same | proved | all subs proved
| queue-rm-vl-rec,
queue-rm-vl-base,
|
| in-vl-subset | proved | all subs proved
| queue-in-vl,
|
| in-vl-append0 | proved | all subs proved
| queue-in-vl,
|
| in-vl-append | proved | all subs proved
| queue-in-vl,
|
| in-single | proved | all subs proved
| queue-in,
|
| in-rm-v-same | proved | all subs proved
| queue-rm-v-rec,
queue-rm-v-base,
queue-in-vl,
|
| in-rm-v-in | proved | all subs proved
| queue-rm-v-rec,
queue-rm-v-base,
queue-in-vl,
|
| in-rm-v | proved | all subs proved
| queue-rm-v-rec,
queue-rm-v-base,
queue-in,
|
| in-prepend-vl | proved | all subs proved
| queue-in-vl,
|
| in-prepend-other | proved | all subs proved
| queue-in,
|
| in-prepend | proved | all subs proved
| queue-in,
|
| in-empty-vl | proved | all subs proved
| queue-in-vl,
|
| in-empty | proved | all subs proved
| queue-in,
|
| in-concat | proved | all subs proved
| queue-in,
|
| in-append-other | proved | all subs proved
| queue-in,
|
| in-append | proved | all subs proved
| queue-in,
|
| queue-rm-vl-base | axiom | | |
| queue-rm-vl-rec | axiom | | |
| lebrefs-base | axiom | | |
| lebrefs-rec | axiom | | |
| queue-rm-v-base | axiom | | |
| queue-rm-v-rec | axiom | | |
| queue-in | axiom | | |
| queue-in-vl | axiom | | |