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: |
|---|
| at-save-1 | proved | all subs proved
| at-save-0,
|
| at-load-1 | proved | all subs proved
| at-load-0,
|
| at-save-0 | proved | all subs proved
| at-save,
|
| at-load-0 | proved | all subs proved
| at-load,
|
| scan-strong | proved | all subs proved
| scan-le,
scan-lt-0,
scan-le-0,
scan-max-0,
|
| scan-given-0 | proved | all subs proved
| scan-given,
|
| save-load-save | proved | all subs proved
| at-save-out-lower,
save-load-save-br,
at-load,
at-save-out-upper,
at-save,
save-size,
|
| scan-max-0 | proved | all subs proved
| scan-max,
|
| scan-le-0 | proved | all subs proved
| scan-le,
|
| scan-lt-0 | proved | all subs proved
| scan-lt,
|
| scan-given | proved | all subs proved
| scan-entry,
scan-branch,
|
| at-save | proved | all subs proved
| save-size,
save-branches-rec,
save-branches-base,
|
| at-load | proved | all subs proved
| load-size,
load-branches-rec,
load-branches-base,
|
| scan-min-eq | proved | all subs proved
| scan-min,
|
| scan-entry-0 | proved | all subs proved
| scan-entry,
|
| scan-branch-0 | proved | all subs proved
| scan-branch,
|
| load-child | proved | all subs proved
| load-branch-child,
|
| scan-min | proved | all subs proved
| scan-rec,
scan-base,
|
| scan-max | proved | all subs proved
| scan-rec,
scan-base,
|
| scan-lt | proved | all subs proved
| scan-rec,
scan-base,
|
| scan-le | proved | all subs proved
| scan-rec,
scan-base,
|
| scan-entry | proved | all subs proved
| scan-rec,
scan-base,
|
| scan-branch | proved | all subs proved
| scan-rec,
scan-base,
|
| at-save-out-upper | proved | all subs proved
| save-branches-rec,
save-branches-base,
|
| save-load-save-br | proved | all subs proved
| load-entry,
save-entry,
load-branch,
save-branch,
|
| at-save-out-lower | proved | all subs proved
| save-branches-rec,
save-branches-base,
|
| load-branch-child | proved | all subs proved
| load-entry,
load-branch,
|
| save-size | proved | all subs proved
| save-branches-rec,
save-branches-base,
|
| load-size | proved | all subs proved
| load-branches-rec,
load-branches-base,
|
| size-shr | proved | all subs proved
| shr,
|
| size-shl | proved | all subs proved
| shl,
|
| scan-last | proved | all subs proved
| scan-rec,
scan-base,
|
| save-properties | proved | all subs proved
| save-node,
|
| save-branches-last | proved | all subs proved
| save-branches-base,
save-branches-rec,
|
| load-save-key | proved | all subs proved
| load-entry,
save-entry,
load-branch,
save-branch,
|
| load-save-entry | proved | all subs proved
| load-entry,
save-entry,
load-branch,
save-branch,
|
| load-save-branch | proved | all subs proved
| load-entry,
save-entry,
load-branch,
save-branch,
|
| load-properties | proved | all subs proved
| load-node,
|
| load-branches-last | proved | all subs proved
| load-branches-base,
load-branches-rec,
|
| at-shr | proved | all subs proved
| shr,
|
| at-shl | proved | all subs proved
| shl,
|
| scan-base | axiom | | |
| scan-rec | axiom | | |
| save-node | axiom | | |
| save-branch | axiom | | |
| save-entry | axiom | | |
| load-node | axiom | | |
| load-branch | axiom | | |
| load-entry | axiom | | |
| shr | axiom | | |
| shl | axiom | | |
| save-branches-base | axiom | | |
| save-branches-rec | axiom | | |
| load-branches-base | axiom | | |
| load-branches-rec | axiom | | |