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: |
|---|
| exists-one | proved | all subs proved
| exists-in-def,
|
| forall-one | proved | all subs proved
| forall-in-def,
|
| indexWhere-le-length | proved | all subs proved
| indexWhere-length-ls,
|
| filter-forall2 | proved | all subs proved
| forall-rec,
forall-base,
filter-forall,
|
| filter-forall | proved | all subs proved
| forall-rec,
|
| indexWhere-length-ls | proved | all subs proved
| indexWhere-rec2,
indexWhere-rec1,
indexWhere-base,
|
| forall-in-def | proved | all subs proved
| forall-rec,
forall-base,
|
| exists-in-def | proved | all subs proved
| exists-rec,
exists-base,
|
| indexWhere-one | proved | all subs proved
| indexWhere-base,
indexWhere-rec2,
indexWhere-rec1,
|
| indexWhere-app-split | proved | all subs proved
| indexWhere-rec2,
indexWhere-rec1,
exists-rec,
exists-base,
|
| forall-1l | proved | all subs proved
| forall-rec,
forall-base,
|
| forall-l | proved | all subs proved
| forall-rec,
forall-base,
|
| exists-forall | proved | all subs proved
| exists-rec,
forall-rec,
exists-base,
forall-base,
|
| exists-get-def | proved | all subs proved
| exists-rec,
exists-base,
|
| forall-rmpos | proved | all subs proved
| forall-rec,
forall-base,
|
| indexWhere-length-eq | proved | all subs proved
| indexWhere-rec2,
indexWhere-rec1,
exists-rec,
indexWhere-base,
exists-base,
|
| exists-append | proved | all subs proved
| exists-rec,
exists-base,
|
| filter-exists | proved | all subs proved
| exists-rec,
|
| forall-get-def | proved | all subs proved
| forall-rec,
forall-base,
|
| forall-append | proved | all subs proved
| forall-rec,
forall-base,
|
| indexWhere-get | proved | all subs proved
| indexWhere-rec2,
indexWhere-rec1,
exists-rec,
exists-base,
|
| forall-exists | proved | all subs proved
| forall-rec,
exists-rec,
exists-base,
forall-base,
|
| indexWhere-length-notle | proved | all subs proved
| indexWhere-rec2,
indexWhere-rec1,
exists-rec,
indexWhere-base,
exists-base,
|
| forall-base | axiom | | |
| forall-rec | axiom | | |
| exists-base | axiom | | |
| exists-rec | axiom | | |
| indexWhere-rec1 | axiom | | |
| indexWhere-rec2 | axiom | | |
| indexWhere-base | axiom | | |