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: |
|---|
| abs-single-FO-one-pending | proved | all subs proved
| abs-loc-no-w-last-fo-then-no-pending,
abs-def,
|
| abs-single-FO-no-pending | proved | all subs proved
| abs-loc-no-w-no-fo-then-no-pending,
abs-loc-no-w-last-fo-then-no-pending,
abs-def,
|
| abs-loc-no-w-last-fo-then-no-pending | proved | all subs proved
| absloc-recW-FO,
absloc-persistfirstFO,
abs-loc-no-w-last-firstfo-then-no-pending,
|
| abs-leading-last-FO-no-pending | proved | all subs proved
| abs-loc-no-w-last-firstfo-then-no-pending,
abs-def,
|
| abs-leading-last-FO-one-pending | proved | all subs proved
| abs-loc-no-w-last-firstfo-then-no-pending,
abs-def,
|
| abs-addWrite | proved | all subs proved
| absloc-addWrite,
abs-def,
|
| abs-persist-firstPersistW | proved | all subs proved
| absloc-persist-firstPersistW,
abs-def,
abs-firstPersistW-is-in-hist,
abs-firstPersistW-firstVolWrite-correct-loc,
abs-def-reduce,
|
| absloc-persist-firstPersistW | proved | all subs proved
| absloc-recR,
absloc-persist-leading-firstPersistW,
|
| absloc-addWrite | proved | all subs proved
| absloc-recW-W,
absloc-recW-FO,
absloc-recW-empty-one,
absloc-recW-empty,
absloc-recW-W-one2,
absloc-recR,
absloc-recW-W-one,
absloc-recW-FO-one,
absloc-recW-W-one3,
absloc-base,
|
| abs-loc-no-w-last-firstfo-then-no-pending | proved | all subs proved
| abs-loc-no-w-no-fo-then-no-pending,
absloc-recW-W,
absloc-recW-empty,
absloc-no-W-leading-W,
absloc-recW-FO,
|
| abs-persistFO | proved | all subs proved
| absloc-prepend-FO,
absloc-persistfirstFO,
abs-def,
|
| abs-addRead | proved | all subs proved
| absloc-addRead,
abs-def,
|
| abs-addReadReader | proved | all subs proved
| absloc-addReader,
absloc-addReadReader,
abs-def-reduce,
|
| abs-addReadFO | proved | all subs proved
| absloc-addReadFO,
abs-def,
|
| abs-addWriteFO | proved | all subs proved
| absloc-addWriteFO,
abs-def,
|
| abs-h-p-nowritesh-allpersisted | proved | all subs proved
| abs-h-p-nowritesh-allpersisted-aux,
abs-def,
|
| abs-h-p-nowritesh-lastPersisted | proved | all subs proved
| pofl-empty-all-l-persisted,
|
| pofl-empty-all-l-persisted | proved | all subs proved
| absloc-nowritesp-nowritesh,
abs-def,
|
| abs-h-p-nowritesh-allpersisted-aux | proved | all subs proved
| absloc-base,
absloc-nowritesp-nowritesh,
|
| absloc-persist-leading-firstPersistW | proved | all subs proved
| absloc-persist-DependentReads,
absloc-recW-W,
absloc-prepend-FO,
absloc-recW-FO,
absloc-recW-empty,
|
| absloc-addWriteFO | proved | all subs proved
| absloc-recW-W,
absloc-recW-FO,
absloc-recW-empty,
absloc-recW-FO-one2,
absloc-recR,
absloc-base,
|
| abs-loc-no-w-no-fo-then-no-pending | proved | all subs proved
| absloc-recW-W,
absloc-recW-FO,
absloc-recW-empty,
absloc-no-W-leading-W,
absloc-recR,
|
| absloc-addReadFO | proved | all subs proved
| absloc-recW-W,
absloc-recW-FO,
absloc-recW-empty,
absloc-recW-FO-one2,
absloc-recR,
absloc-base,
|
| absloc-recW-W-one3 | proved | all subs proved
| absloc-base,
absloc-recW-W-one2,
|
| absloc-addReadReader | proved | all subs proved
| absloc-recW-W,
absloc-recW-FO,
absloc-recW-empty,
absloc-recR,
absloc-recR-one,
absloc-base,
|
| absloc-addRead | proved | all subs proved
| absloc-recW-W,
absloc-recW-FO,
absloc-recW-empty,
absloc-recR,
absloc-recR-one,
absloc-base,
|
| absloc-persistfirstFO | proved | all subs proved
| absloc-recW-FO,
absloc-recR,
absloc-prepend-FO,
absloc-base,
|
| abs-persistFO-weak | proved | all subs proved
| absloc-persistFO,
abs-def-reduce,
|
| abs-persistWrite | proved | all subs proved
| absloc-persistWrite,
abs-leading-write-h-restricted-non-empty,
abs-def-reduce,
|
| absloc-recW-FO-one3 | proved | all subs proved
| absloc-recW-FO-one2,
|
| abs-firstPersistW-in-p-when-firstVolWrite-in-h | proved | all subs proved
| absloc-recR,
absloc-recW-W,
absloc-recW-FO,
absloc-recW-empty,
abs-def,
abs-firstPersistW-is-in-hist,
|
| absloc-persist-DependentReads | proved | all subs proved
| absloc-recR,
absloc-base,
|
| absloc-nowritesp-nowritesh | proved | all subs proved
| absloc-recW-FO,
absloc-recW-empty,
absloc-recR,
|
| abs-firstPersistW-firstVolWrite-correct-loc | proved | all subs proved
| absloc-recR,
absloc-base,
abs-def,
|
| abs-firstPersistW-is-in-hist | proved | all subs proved
| absloc-recR,
absloc-base,
abs-def,
|
| abs-leading-write-h-restricted-non-empty | proved | all subs proved
| absloc-recR,
absloc-base,
abs-def,
|
| absloc-persistWrite | proved | all subs proved
| absloc-recR,
absloc-base,
absloc-recW-W,
|
| absloc-no-W-leading-W | proved | all subs proved
| absloc-recW-W,
absloc-recW-FO,
absloc-recW-empty,
|
| absloc-persistFO | proved | all subs proved
| absloc-recW-FO,
absloc-recW-empty,
absloc-recR,
absloc-base,
|
| absloc-recW-FO-one | proved | all subs proved
| absloc-recW-FO,
|
| absloc-recW-W-one | proved | all subs proved
| absloc-base,
absloc-recW-W,
|
| absloc-recW-W-one2 | proved | all subs proved
| absloc-recW-W,
|
| absloc-recW-empty-one | proved | all subs proved
| absloc-recW-empty,
|
| abs-def-reduce | proved | all subs proved
| abs-def,
|
| absloc-addReader | proved | all subs proved
| absloc-recW-W,
absloc-recW-FO,
absloc-recW-empty,
absloc-recR,
absloc-base,
|
| absloc-recW-FO-one2 | proved | all subs proved
| absloc-recW-empty,
absloc-recW-FO,
|
| absloc-recR-one | proved | all subs proved
| absloc-base,
absloc-recR,
|
| absloc-prepend-FO | proved | all subs proved
| absloc-recW-FO,
absloc-recR,
absloc-base,
|
| abs-firstVolWrite-head | proved | all subs proved
| absloc-recW-W,
absloc-recR,
absloc-base,
abs-def,
|
| abs-apply-firstPersistW | proved | all subs proved
| absloc-recW-W,
absloc-recW-FO,
absloc-recR,
absloc-base,
abs-def,
|
| abs-firstPersistW-is-firstVolWrite | proved | all subs proved
| absloc-recW-W,
absloc-recW-FO,
absloc-recR,
absloc-base,
abs-def,
|
| abs-noReadFO | proved | all subs proved
| absloc-base,
abs-def,
|
| absloc-recW-empty | axiom | | |
| absloc-recW-W | axiom | | |
| abs-def | axiom | | |
| absloc-base | axiom | | |
| absloc-recR | axiom | | |
| absloc-recW-FO | axiom | | |