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: |
|---|
| in-crash-at-gstore | proved | all subs proved
| crash-group-in,
crash-group-at,
in-crash-in-gstore,
|
| icrash-remove-refsize0-prefix | proved | all subs proved
| crash-index-at,
crash-index-in,
dom-istore-crash-refm-refsize0,
|
| fwd-inv-loghead | proved | all subs proved
| elems-append,
|
| fwd-in-log-in-gstore | proved | all subs proved
| elems-def,
elems-in-notin-ginval,
|
| fwd-in-gstore-loghead | proved | all subs proved
| elems-append,
|
| elems-subseteq-add-diff-notin | proved | all subs proved
| elems-in-fwd,
elems-in-diff,
elems-def,
|
| in-crash-in-gstore | proved | all subs proved
| crash-group-at,
crash-group-in,
|
| dom-istore-crash-refm-refsize0 | proved | all subs proved
| crash-index-at,
crash-index-in,
|
| elems-in-notin-ginval | proved | all subs proved
| elems-def,
|
| elems-append | proved | all subs proved
| elems-def,
|
| elems-in-diff | proved | all subs proved
| elems-def,
|
| elems-in-fwd | proved | all subs proved
| elems-def,
|
| store-diff-union-elems-notin | proved | all subs proved
| elems-def,
|
| inv-crash | proved | all subs proved
| fwd-inv-iblock,
crash-index-at,
crash-index-in,
|
| icrash-refsize-cons | proved | all subs proved
| crash-index-at,
crash-index-in,
|
| icrash-inv | proved | all subs proved
| fwd-inv-iblock,
crash-index-at,
crash-index-in,
|
| fwd-in-gstore0 | proved | all subs proved
| elems-def,
|
| elems-prepend | proved | all subs proved
| elems-def,
|
| elems-minus | proved | all subs proved
| elems-def,
|
| elems-log-subset-gstore-union-ginval | proved | all subs proved
| elems-def,
|
| elems-empty | proved | all subs proved
| elems-def,
|
| dom-istore-crash | proved | all subs proved
| crash-index-in,
|
| dom-gstore-crash | proved | all subs proved
| crash-group-in,
|
| dom-disj-in-l | proved | all subs proved
| dom-disj-in-r,
|
| crash-update-reverted | proved | all subs proved
| crash-group-in,
crash-group-at,
|
| crash-gstore-inv | proved | all subs proved
| crash-group-at,
crash-group-in,
|
| fwd-inv-iblock | proved | all subs proved
| |
| elems-def | axiom | | |
| crash-index-at | axiom | | |
| crash-index-in | axiom | | |
| dom-disj-in-r | proved | all subs proved
| |
| crash-group-in | axiom | | |
| crash-group-at | axiom | | |