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: |
|---|
| notin-down-eq-notin-down | proved | all subs proved
| notin-notin-nodes-down,
|
| notin-notin-nodes-down | proved | all subs proved
| down-store-notin-notin,
nodes-gstore-in,
|
| adr-in-ri-in-gstore | proved | all subs proved
| down-store-notin-notin,
nodes-gstore-in,
|
| abs-log-split-head | proved | all subs proved
| abs-log-eq-butlast,
|
| down-store-notin-notin | proved | all subs proved
| valid-group-nodes-entire,
down-block-explicit,
down-store-at,
down-store-in,
|
| abs-log-eq-butlast | proved | all subs proved
| abs-log-append-one,
|
| valid-group-nodes-single-end | proved | all subs proved
| valid-group-nodes-last-end-nosimp,
|
| valid-group-nodes-shorter-prefix | proved | all subs proved
| valid-group-nodes-shorter-prefix-right,
valid-group-nodes-prefixn-append-nonend,
valid-group-nodes-rec,
induction-rev-list,
valid-group-nodes-ls,
|
| valid-group-nodes-drop | proved | all subs proved
| valid-group-nodes-ls,
valid-group-nodes-le,
|
| remove-refsize0-down | proved | all subs proved
| valid-group-nodes-entire,
down-block-explicit,
down-store-at,
down-store-in,
|
| refsize-nonzero-notin-ginval | proved | all subs proved
| down-store-at,
down-store-adr-in-explicit,
nodes-gstore-in,
size-0,
|
| refsize-0-notin-index | proved | all subs proved
| size-0,
|
| nodes-write-same-flushed | proved | all subs proved
| nodes-write-at-other,
down-store-adr-in-explicit,
down-store-write-same,
valid-group-nodes-entire,
nodes-gstore-at,
down-store-at,
down-store-in,
nodes-gstore-in,
down-block-explicit,
|
| nodes-crash-down | proved | all subs proved
| valid-group-nodes-entire,
nodes-gstore-at,
down-store-adr-in-explicit,
down-block-explicit,
down-store-at,
down-store-in,
nodes-gstore-in,
|
| nodes-append-subseteq-nodown | proved | all subs proved
| nodes-write-at-other,
valid-group-nodes-ls,
down-store-write-same,
down-block-explicit,
down-store-adr-in-explicit-simp,
nodes-gstore-at,
down-store-in,
down-store-at,
down-store-adr-in-explicit,
nodes-gstore-in,
|
| lebs-dom-remove-refsize0 | proved | all subs proved
| down-store-adr-in-explicit,
nodes-gstore-in,
size-0,
|
| in-nodes-down-at-same | proved | all subs proved
| valid-group-nodes-entire,
down-block,
down-store-in,
down-store-adr-in-explicit-simp,
down-store-at,
down-store-adr-in-explicit,
nodes-gstore-in,
|
| dom-remove-refsize0-down | proved | all subs proved
| valid-group-nodes-entire,
down-block-explicit,
down-store-at,
down-store-in,
|
| abs-log-write-last | proved | all subs proved
| abs-log-change-other,
abs-log-append-one,
|
| valid-group-nodes-last-end-nosimp | proved | all subs proved
| valid-group-nodes-last-end,
|
| valid-group-nodes-shorter-prefix-right | proved | all subs proved
| valid-group-nodes-prefixn-append-nonend,
valid-group-nodes-rec,
induction-rev-list,
valid-group-nodes-ls,
|
| valid-group-nodes-le | proved | all subs proved
| valid-group-nodes-ls,
|
| size-0 | proved | all subs proved
| down-block,
down-store-at,
down-store-adr-in-explicit,
nodes-gstore-in,
|
| down-store-adr-in-explicit-simp | proved | all subs proved
| down-store-at,
down-store-adr-in-explicit,
down-store-in,
|
| valid-group-nodes-entire | proved | all subs proved
| valid-group-nodes-ls,
valid-group-nodes-rec,
valid-group-nodes-base,
induction-rev-list,
|
| abs-log-append-one | proved | all subs proved
| abs-log-rec,
abs-log-base,
abs-log-one,
|
| valid-journal-head-valid-group-nodes | proved | all subs proved
| valid-group-nodes-last-end,
valid-group-nodes-base,
|
| valid-group-nodes-drop-superfluous-prefixn | proved | all subs proved
| valid-group-nodes-prefixn-append-nonend,
valid-group-nodes-rec,
valid-group-nodes-base,
induction-rev-list,
|
| nodes-referenced-adrs-leb | proved | all subs proved
| down-block-explicit,
down-store-at,
down-store-adr-in-explicit,
nodes-gstore-in,
|
| nodes-except-refsize-down | proved | all subs proved
| down-except-refsize,
nodes-except-refsize,
|
| nodes-append-subseteq | proved | all subs proved
| nodes-write-at-other,
valid-group-nodes-ls,
down-store-write-same,
nodes-gstore-at,
down-store-in,
down-store-at,
down-store-adr-in-explicit,
nodes-gstore-in,
valid-group-nodes-rec,
down-block-explicit,
|
| in-restr-notin-log | proved | all subs proved
| abs-log-adr-explicit-in-leb-notin,
|
| in-restr-eq-notin-log | proved | all subs proved
| abs-log-toset-inter-restr-empty,
|
| ginval-down | proved | all subs proved
| down-store-at,
down-store-at-diff,
down-store-in,
|
| adr-in-ri-leb-notin-ginval | proved | all subs proved
| down-store-at,
down-store-adr-in-explicit,
nodes-gstore-in,
|
| adr-in-index-node-key | proved | all subs proved
| valid-group-nodes-ls,
nodes-gstore-at,
down-block-explicit,
down-store-at,
down-store-adr-in-explicit,
nodes-gstore-in,
|
| abs-log-gcrash-down | proved | all subs proved
| down-block-explicit,
down-block,
down-store-in,
down-store-at,
abs-log-rec,
abs-log-base,
|
| abs-log-except-refsize-down | proved | all subs proved
| down-except-refsize,
abs-log-except-refsize,
|
| valid-group-nodes-last-end | proved | all subs proved
| valid-group-nodes-rec,
valid-group-nodes-base,
|
| valid-group-nodes-prefixn-append-nonend | proved | all subs proved
| valid-group-nodes-rec,
|
| nodes-except-refsize | proved | all subs proved
| nodes-gstore-at,
nodes-gstore-in,
|
| nodes-write-at-other | proved | all subs proved
| nodes-gstore-in,
nodes-gstore-at,
|
| abs-log-adr-explicit-in-leb-notin | proved | all subs proved
| abs-log-rec,
abs-log-base,
|
| abs-log-toset-inter-restr-empty | proved | all subs proved
| abs-log-rec,
abs-log-base,
|
| down-store-at-diff | proved | all subs proved
| down-store-in,
down-store-at,
|
| down-store-adr-in-explicit | proved | all subs proved
| down-store-in,
down-store-at,
|
| valid-group-nodes-ls | proved | all subs proved
| valid-group-nodes-rec,
valid-group-nodes-base,
induction-rev-list,
|
| abs-log-change-other | proved | all subs proved
| abs-log-rec,
abs-log-base,
|
| down-block-explicit | proved | all subs proved
| down-block,
|
| abs-log-except-refsize | proved | all subs proved
| abs-log-rec,
abs-log-base,
|
| down-except-refsize | proved | all subs proved
| down-block,
down-store-at,
down-store-in,
|
| abs-log-one | proved | all subs proved
| abs-log-base,
abs-log-rec,
|
| valid-group-nodes-app-transaction-prefix | proved | all subs proved
| valid-group-nodes-rec,
|
| valid-group-nodes-app-transaction | proved | all subs proved
| valid-group-nodes-rec,
|
| ri-cons-range-restrict-notin-gstore | proved | all subs proved
| nodes-gstore-in,
|
| range-rem-in | proved | all subs proved
| nodes-gstore-at,
nodes-gstore-in,
|
| nodes-write-nochange | proved | all subs proved
| nodes-gstore-at,
nodes-gstore-in,
|
| nodes-transaction | proved | all subs proved
| nodes-gstore-at,
nodes-gstore-in,
|
| nodes-remove-refsize0 | proved | all subs proved
| nodes-gstore-at,
refsize0-addresses,
nodes-gstore-in,
|
| nodes-remove-ginval-notin | proved | all subs proved
| nodes-gstore-at,
nodes-gstore-in,
|
| nodes-no-change-eq | proved | all subs proved
| nodes-gstore-at,
nodes-gstore-in,
|
| nodes-ginval-rem-01 | proved | all subs proved
| nodes-gstore-at,
nodes-gstore-in,
|
| nodes-ginval-rem | proved | all subs proved
| nodes-gstore-at,
nodes-gstore-in,
|
| nodes-ginval-inter | proved | all subs proved
| nodes-gstore-at,
nodes-gstore-in,
|
| nodes-empty | proved | all subs proved
| nodes-gstore-in,
|
| nodes-dealloc | proved | all subs proved
| nodes-gstore-at,
nodes-gstore-in,
|
| nodes-allocate | proved | all subs proved
| nodes-gstore-at,
nodes-gstore-in,
|
| new-adrs-gstore | proved | all subs proved
| nodes-gstore-in,
|
| keys-remove-leb | proved | all subs proved
| toSet-diff-get,
|
| index-update-adr-in | proved | all subs proved
| toSet-diff-in,
toSet-diff-get,
|
| in-nodes-in-gstore | proved | all subs proved
| nodes-gstore-in,
|
| ginval-extract-nodes | proved | all subs proved
| nodes-gstore-at,
nodes-gstore-in,
|
| ginval-extract-abs-log | proved | all subs proved
| abs-log-rec,
abs-log-base,
|
| down-store-write | proved | all subs proved
| down-store-at,
down-store-in,
|
| down-store-dealloc | proved | all subs proved
| down-store-at,
down-store-in,
|
| down-empty | proved | all subs proved
| down-store-in,
|
| adr-in-ri-notin-nodes | proved | all subs proved
| nodes-gstore-in,
|
| addresses-restr-subseteq0 | proved | all subs proved
| adresses-restr-subseteq,
|
| abs-log-write-nochange | proved | all subs proved
| abs-log-rec,
abs-log-base,
|
| abs-log-no-change-eq | proved | all subs proved
| abs-log-rec,
abs-log-base,
|
| abs-log-new | proved | all subs proved
| nodes-gstore-in,
abs-log-rec,
abs-log-base,
|
| abs-log-del | proved | all subs proved
| abs-log-rec,
abs-log-base,
|
| induction-rev-list | proved | all subs proved
| |
| valid-group-nodes-base | axiom | | |
| refsize0-addresses | axiom | | |
| valid-group-nodes-rec | axiom | | |
| down-store-write-same | proved | all subs proved
| |
| toSet-diff-get | proved | all subs proved
| |
| toSet-diff-in | proved | all subs proved
| |
| nodes-gstore-at | axiom | | |
| adresses-restr-subseteq | proved | all subs proved
| |
| nodes-gstore-in | axiom | | |
| down-store-at | axiom | | |
| down-store-in | axiom | | |
| down-block | axiom | | |
| abs-log-base | axiom | | |
| abs-log-rec | axiom | | |