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: |
|---|
| ar-elems-extract1 | proved | all subs proved
| ar-elems1,
ar-elems-append,
elems-rec,
elems,
|
| ar-elems-append | proved | all subs proved
| elems-base,
ar-elems-append-not-lower-h,
ar-elems-append-lower-h,
elems,
|
| ar-elems-update | proved | all subs proved
| ar-elems-update-h,
elems,
|
| ar-elems-id-size1 | proved | all subs proved
| ar-elems-size,
elems,
|
| ar-elems-id-size | proved | all subs proved
| ar-elems-size,
elems,
|
| ar-elems-update-h | proved | all subs proved
| ar-elems-in-h,
ar-elems-update-h0,
elems-rec,
elems-base,
|
| ar-elems-size | proved | all subs proved
| ar-elems-size-h,
elems,
|
| ar-elems-append-not-lower-h | proved | all subs proved
| ar-elems-append-lower-h,
elems-base,
elems-rec,
|
| ar-elems-in | proved | all subs proved
| ar-elems-in-h,
elems,
|
| ar-elems-in-exists | proved | all subs proved
| ar-elems-in-exists-h,
elems,
|
| ar-elems-append-lower-h | proved | all subs proved
| elems-rec,
elems-base,
|
| ar-elems1 | proved | all subs proved
| elems-base,
elems-rec,
elems,
|
| ar-elems-in-exists-h | proved | all subs proved
| elems-rec,
elems-base,
|
| ar-elems-size-h | proved | all subs proved
| elems-rec,
elems-base,
|
| ar-elems-in-h | proved | all subs proved
| elems-rec,
|
| ar-elems-update-h0 | proved | all subs proved
| elems-rec,
elems-base,
|
| elems-rec | axiom | | |
| elems | axiom | | |
| elems-base | axiom | | |