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: |
|---|
| refsize-cons-crash | proved | all subs proved
| restrict-range-notin-lebs,
|
| referenced-adrs-lookup-keys-nodups | proved | all subs proved
| referenced-adrs-split-one,
referenced-adrs-in,
referenced-adrs-split,
keys-eq-one,
keys-split,
keys-one,
keys-app,
referenced-adrs-rec,
keys-base-01,
referenced-adrs-base,
|
| referenced-adrs-eq-one-lookup | proved | all subs proved
| referenced-adrs-split-one,
|
| nds-one | proved | all subs proved
| nds-eq-one,
|
| keys-rem | proved | all subs proved
| keys-inodekey-in,
keys-in,
|
| keys-empty | proved | all subs proved
| keys-in,
keys-base,
|
| restrict-range-notin-lebs | proved | all subs proved
| lebs-in-ri-in-gstore,
|
| keys-split | proved | all subs proved
| keys-rec-01,
keys-base-01,
keys-app,
|
| keys-eq-one | proved | all subs proved
| keys-rec-01,
keys-base-01,
keys-one,
|
| referenced-adrs-split | proved | all subs proved
| referenced-adrs-rec,
referenced-adrs-base,
referenced-adrs-app,
|
| referenced-adrs-split-one | proved | all subs proved
| referenced-adrs-in,
referenced-adrs-one,
referenced-adrs-base,
referenced-adrs-rec,
referenced-adrs-app,
|
| nds-eq-one | proved | all subs proved
| nds-eq-empty,
nds-rec,
nds-base,
|
| keys-in | proved | all subs proved
| keys-inodekeys,
keys-inodekey-in,
|
| transaction-length0 | proved | all subs proved
| transaction-length,
|
| transaction-empty | proved | all subs proved
| transaction-empty-right,
transaction,
|
| refsize-cons-in-ri-0 | proved | all subs proved
| lebs-in-ri-in-gstore,
|
| referenced-adrs-subseteq-range | proved | all subs proved
| referenced-adrs-in,
|
| referenced-adrs-nodups | proved | all subs proved
| referenced-adrs-in,
referenced-adrs-rec,
referenced-adrs-base,
|
| referenced-adrs-lookup-keys-lookup | proved | all subs proved
| keys-one,
keys-app,
referenced-adrs-rec,
keys-base-01,
referenced-adrs-base,
|
| referenced-adrs-lookup-keys-in-dom | proved | all subs proved
| keys-one,
keys-app,
referenced-adrs-rec,
keys-base-01,
referenced-adrs-base,
|
| referenced-adrs-lookup-key-cons | proved | all subs proved
| key-cons-one,
key-cons-app,
referenced-adrs-rec,
key-cons-base,
referenced-adrs-base,
|
| referenced-adrs-inter-empty | proved | all subs proved
| referenced-adrs-in,
|
| keys-rec-full | proved | all subs proved
| keys-inodekey-in,
keys-rec,
|
| transaction-length | proved | all subs proved
| transaction,
|
| transaction-empty-right | proved | all subs proved
| transaction,
|
| lebs-in-ri-in-gstore | proved | all subs proved
| lebs-index,
|
| referenced-adrs-one | proved | all subs proved
| referenced-adrs-base,
referenced-adrs-rec,
|
| referenced-adrs-app | proved | all subs proved
| referenced-adrs-rec,
referenced-adrs-base,
|
| key-cons-app | proved | all subs proved
| key-cons-rec,
key-cons-base,
|
| key-cons-one | proved | all subs proved
| key-cons-base,
key-cons-rec,
|
| referenced-adrs-in | proved | all subs proved
| referenced-adrs-rec,
referenced-adrs-base,
|
| nds-eq-empty | proved | all subs proved
| nds-rec,
nds-base,
|
| keys-app | proved | all subs proved
| keys-rec-01,
keys-base-01,
|
| keys-inodekey-in | proved | all subs proved
| keys-rec,
keys-base,
|
| keys-inodekeys | proved | all subs proved
| keys-rec,
keys-base,
|
| keys-one | proved | all subs proved
| keys-base-01,
keys-rec-01,
|
| valid-journal-head-emptylog | proved | all subs proved
| valid-journal-head,
|
| transaction-prefix-last-nonend | proved | all subs proved
| transaction-prefix,
|
| transaction-prefix-is-transaction-prefix | proved | all subs proved
| transaction-prefix,
transaction,
|
| transaction-prefix-empty | proved | all subs proved
| transaction-prefix,
|
| transaction-prefix-app-nonlast | proved | all subs proved
| transaction-prefix,
|
| transaction-prefix-app-last | proved | all subs proved
| transaction,
transaction-prefix,
|
| transaction-prefix-app | proved | all subs proved
| transaction-prefix,
|
| transaction-last-nend | proved | all subs proved
| transaction,
|
| nodes-cons-write-other | proved | all subs proved
| nodes-cons,
|
| nodes-cons-write-app | proved | all subs proved
| ladrlist-to-adr-split,
nodes-cons,
transaction,
|
| nodes-cons-rec | proved | all subs proved
| nodes-cons,
|
| nds-length | proved | all subs proved
| nds-rec,
nds-base,
|
| nds-app | proved | all subs proved
| nds-rec,
nds-base,
|
| lebs-write-subseteq0 | proved | all subs proved
| lebs-index,
|
| lebs-write-subseteq | proved | all subs proved
| lebs-index,
|
| lebs-write | proved | all subs proved
| in-data-explicit,
lebs-index,
|
| lebs-rem-subseteq | proved | all subs proved
| in-rem-keys-in-data,
lebs-index,
|
| lebs-range | proved | all subs proved
| lebs-index,
lebs-set,
|
| lebs-lookup-subseteq | proved | all subs proved
| in-data-explicit,
lebs-index,
lebs-set,
|
| lebs-in-ri-in-gstore-explicit | proved | all subs proved
| in-data-explicit,
lebs-index,
|
| lebs-empty | proved | all subs proved
| lebs-index,
|
| lebs-del-subseteq-set | proved | all subs proved
| lebs-set,
|
| lebs-del-subseteq | proved | all subs proved
| lebs-index,
|
| keys-len | proved | all subs proved
| keys-rec-01,
keys-base-01,
|
| key-cons-ext | proved | all subs proved
| key-cons-rec,
key-cons-base,
|
| inos-write | proved | all subs proved
| inos-node-store-def,
|
| inos-greater-rem | proved | all subs proved
| inos-node-store-def,
|
| inos-greater-notin | proved | all subs proved
| inos-node-store-def,
|
| inos-greater-del | proved | all subs proved
| inos-node-store-def,
|
| inos-empty | proved | all subs proved
| inos-node-store-def,
|
| inos-dom | proved | all subs proved
| inos-node-store-def,
|
| index-update-range | proved | all subs proved
| ri-inj-index-update,
range-write-in,
|
| flashsize-one | proved | all subs proved
| flashsize-nodes-base,
flashsize-nodes-rec,
|
| flashsize-app | proved | all subs proved
| flashsize-nodes-rec,
flashsize-nodes-base,
|
| except-refsizeeq-valid-head | proved | all subs proved
| valid-journal-head,
|
| transaction-prefix | axiom | | |
| referenced-adrs-base | axiom | | |
| referenced-adrs-rec | axiom | | |
| transaction | axiom | | |
| ladrlist-to-adr-split | proved | all subs proved
| |
| nodes-cons | axiom | | |
| nds-base | axiom | | |
| nds-rec | axiom | | |
| in-rem-keys-in-data | proved | all subs proved
| |
| in-data-explicit | proved | all subs proved
| |
| lebs-set | axiom | | |
| lebs-index | axiom | | |
| keys-rec | axiom | | |
| keys-base | axiom | | |
| keys-base-01 | axiom | | |
| keys-rec-01 | axiom | | |
| key-cons-base | axiom | | |
| key-cons-rec | axiom | | |
| inos-node-store-def | axiom | | |
| range-write-in | proved | all subs proved
| |
| ri-inj-index-update | proved | all subs proved
| |
| flashsize-nodes-base | axiom | | |
| flashsize-nodes-rec | axiom | | |
| valid-journal-head | axiom | | |