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: |
|---|
| map-ifn-0 | proved | all subs proved
| map-ifn-at,
map-ifn-size,
|
| map-if-size | proved | all subs proved
| valid-indices-indiceswhere,
map-indices-size,
mapif-def,
|
| map-if-at | proved | all subs proved
| indices-where-in,
valid-indices-nodups,
valid-indices-indiceswhere,
map-indices-at,
mapif-def,
|
| map-ifn-size | proved | all subs proved
| valid-indices-indiceswhere-h,
map-indices-size,
mapifn-def,
|
| map-ifn-at | proved | all subs proved
| indices-where-in-h,
valid-indices,
valid-indices-nodups-h,
valid-indices-indiceswhere-h,
map-indices-at,
mapifn-def,
|
| valid-indices-indiceswhere | proved | all subs proved
| indices-where-in,
valid-indices-nonrec,
|
| valid-indices-nodups | proved | all subs proved
| valid-indices-nodups-h,
indiceswhere,
|
| valid-indices-indiceswhere-h | proved | all subs proved
| valid-indices-indiceswhere-h-strong,
valid-indices-nonrec,
|
| valid-indices-nodups-h | proved | all subs proved
| valid-indices-indiceswhere-h-strong,
indiceswhere-rec,
indiceswhere-base,
|
| indices-where-in | proved | all subs proved
| indices-where-in-h,
indiceswhere,
|
| valid-indices-write | proved | all subs proved
| valid-indices-simp,
valid-indices,
|
| map-indices-append | proved | all subs proved
| mapindices-rec,
mapindices-base,
map-indices-one,
valid-indices,
|
| valid-indices-simp | proved | all subs proved
| valid-indices,
|
| valid-indices-indiceswhere-h-strong | proved | all subs proved
| indiceswhere-rec,
indiceswhere-base,
|
| valid-indices-nonrec | proved | all subs proved
| valid-indices,
|
| map-indices-one | proved | all subs proved
| mapindices-base,
mapindices-rec,
|
| map-indices-size | proved | all subs proved
| mapindices-rec,
mapindices-base,
valid-indices,
|
| map-indices-at | proved | all subs proved
| mapindices-rec,
mapindices-base,
valid-indices,
|
| indices-where-in-h | proved | all subs proved
| indiceswhere-rec,
indiceswhere-base,
|
| valid-indices-one | proved | all subs proved
| valid-indices,
|
| valid-indices-append | proved | all subs proved
| valid-indices,
|
| map-set-empty | proved | all subs proved
| mapset-def,
|
| map-indices-empty | proved | all subs proved
| mapindices-at,
mapindices-size,
|
| map-ifn-full | proved | all subs proved
| indiceswhere,
mapifn-def,
mapif-def,
|
| mapset-def | axiom | | |
| mapindices-size | axiom | | |
| mapindices-at | axiom | | |
| mapindices-base | axiom | | |
| mapindices-rec | axiom | | |
| mapifn-def | axiom | | |
| valid-indices | axiom | | |
| mapif-def | axiom | | |
| indiceswhere-base | axiom | | |
| indiceswhere-rec | axiom | | |
| indiceswhere | axiom | | |