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: |
|---|
| unmodified-payload | proved | | payload-save-load-same,
at-payload,
in-payload,
unmodified,
|
| payload-save-load-same | proved | | save-same-payload-same,
|
| unmodified-same-payload-subseteq | proved | | save-same-payload-same,
unmodified,
|
| unmodified-same-payload | proved | | save-same-payload-same,
unmodified,
|
| payload-mod-0 | proved | all subs proved
| payload-mod,
|
| payload-keys-0 | proved | all subs proved
| payload-keys,
|
| look-subrange | proved | all subs proved
| range,
in-keyrange-in-ri,
at-range,
look,
|
| keys-mod-0 | proved | all subs proved
| keys-mod,
|
| save-same-payload-same | invalid | | payload-one,
payload-split,
payload-base,
|
| payload-mod | proved | all subs proved
| payload-drop-lower,
payload-rec,
payload-base,
|
| payload-keys | proved | all subs proved
| in-keys,
in-payload,
|
| in-keyrange-in-ri | proved | all subs proved
| range,
|
| keys-mod | proved | all subs proved
| keys-drop-lower,
keys-rec,
keys-base,
|
| unmodified-write-dirty | proved | all subs proved
| unmodified-dirty,
|
| unmodified-key-range-node | proved | all subs proved
| range,
unmodified,
|
| range-put | proved | all subs proved
| range-one,
range-first,
range-last,
range-inner,
at-range,
|
| range-load-save | proved | all subs proved
| range,
|
| range-emp | proved | all subs proved
| range,
|
| payload-shift-left | proved | all subs proved
| at-payload,
in-payload,
|
| payload-copy-right-upper | proved | all subs proved
| payload-drop-lower,
payload-rec,
payload-base,
|
| payload-copy-right-lower-0 | proved | all subs proved
| payload-copy-right-lower,
|
| look-scan-range | proved | all subs proved
| range,
look,
|
| keys-shift-left | proved | all subs proved
| in-keys,
|
| key-range-replace-branches | proved | all subs proved
| range,
|
| in-playload-data | proved | all subs proved
| in-payload,
payload-rec,
payload-base,
|
| in-keyrange-in-ri-data | proved | all subs proved
| range,
|
| unmodified-dirty | proved | all subs proved
| unmodified,
|
| payload-split | invalid | all subs proved
| payload-rec,
payload-base,
|
| payload-one | proved | all subs proved
| payload-base,
payload-rec,
|
| at-payload | proved | all subs proved
| payload-rec,
payload-base,
|
| payload-drop-lower | proved | all subs proved
| payload-rec,
payload-base,
|
| payload-copy-right-lower | proved | all subs proved
| payload-rec,
payload-base,
|
| at-range | proved | all subs proved
| range-one,
range-first,
range-last,
range-inner,
|
| in-keys | proved | all subs proved
| keys-rec,
keys-base,
|
| keys-drop-lower | proved | all subs proved
| keys-rec,
keys-base,
|
| in-payload | proved | all subs proved
| payload-rec,
payload-base,
|
| range | proved | all subs proved
| range-inner,
range-last,
range-first,
range-one,
|
| unmodified-write-other | proved | all subs proved
| unmodified,
|
| unmodified-sorted-node | proved | all subs proved
| unmodified,
|
| unmodified-sorted-leaf | proved | all subs proved
| unmodified,
|
| unmodified-save | proved | all subs proved
| unmodified,
|
| unmodified-reload | proved | all subs proved
| unmodified,
|
| unmodified-load-key-node | proved | all subs proved
| unmodified,
|
| unmodified-load-key-leaf | proved | all subs proved
| unmodified,
|
| unmodified-load-adr-node | proved | all subs proved
| unmodified,
|
| unmodified-load | proved | all subs proved
| unmodified,
|
| unmodified-clean-leaf-subseteq | proved | all subs proved
| unmodified,
|
| unmodified-clean-leaf | proved | all subs proved
| unmodified,
|
| unmodified-clean-fwd-zbrar2 | proved | all subs proved
| unmodified,
|
| unmodified-clean-fwd-zbrar | proved | all subs proved
| unmodified,
|
| unmodified-clean-eq-keys-subseteq | proved | all subs proved
| unmodified,
|
| unmodified-clean-eq-keys | proved | all subs proved
| unmodified,
|
| unmodified-clean-eq-adr-subseteq | proved | all subs proved
| unmodified,
|
| range-le | proved | all subs proved
| range-first,
range-inner,
|
| range-last-2 | proved | all subs proved
| range-last,
|
| range-gt | proved | all subs proved
| range-last,
range-inner,
|
| payload-drop-upper | proved | all subs proved
| payload-rec,
payload-base,
|
| nsize-size | proved | all subs proved
| nsze-underfull,
nsze-overfull,
nsze-ok,
|
| look-true | proved | all subs proved
| look,
|
| look-in | proved | all subs proved
| look,
|
| look-false | proved | all subs proved
| look,
|
| look-empty | proved | all subs proved
| look,
|
| look-at | proved | all subs proved
| look,
|
| keys-drop-upper | proved | all subs proved
| keys-rec,
keys-base,
|
| keep-range | proved | all subs proved
| range-last,
range-one,
range-first,
range-inner,
|
| unmodified | axiom | | |
| nsze-ok | axiom | | |
| nsze-overfull | axiom | | |
| nsze-underfull | axiom | | |
| look | axiom | | |
| keys-base | axiom | | |
| keys-rec | axiom | | |
| range-inner | axiom | | |
| range-last | axiom | | |
| range-first | axiom | | |
| range-one | axiom | | |
| payload-base | axiom | | |
| payload-rec | axiom | | |