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: |
|---|
| allwritesOK-at-most-one-write | proved | all subs proved
| allwritesOK-ind-at-most-one-write,
allWritesOK-def,
|
| allwritesOK-persist-one-write | proved | all subs proved
| allwritesOK-ind-persist-one-write,
allWritesOK-def,
restrict-vp,
restrict-loc,
restrict-W,
|
| allwritesOK-ind-persist-one-write | proved | all subs proved
| allWritesOKInd-recR,
restrict-vp,
restrict-loc,
restrict-W,
restrict-b-append,
restrict-l-append,
restrict-write-one,
restrict-W-append,
allwritesOK-ind-swap-flags-persist-one-write,
allWritesOKInd-recW,
restrict-b-empty,
restrict-l-empty,
restrict-W-empty,
|
| allwritesOK-ind-at-most-one-write | proved | all subs proved
| allwritesOK-ind-pending-not-in,
allWritesOKInd-recW,
allWritesOKInd-recR,
restrict-vp,
restrict-thread,
restrict-W,
|
| allreadsOK-filter-persisted | proved | all subs proved
| allreadsOK-ind-filter-persisted,
restrict-vp,
allReadsOK-def,
|
| allwritesOK-filter-persisted | proved | all subs proved
| allWritesOK-ind-filter-persisted,
allWritesOK-def,
restrict-vp,
|
| allwritesOK-add-read | proved | all subs proved
| allwritesOK-ind-add-read,
allWritesOK-def,
|
| overwrite-persist-one-write-restrict-true | proved | all subs proved
| overwrite-rec-read,
at-overwrite-mem-update-other,
restrict-W-append,
restrict-l-one,
restrict-l-append,
at-overwrite-no-write,
mem-update-swap,
overwrite-base,
overwrite-rec-write,
restrict-vp,
restrict-true-false,
restrict-b-append,
overwrite-persist-one-write,
restrict-true-true,
restrict-loc,
restrict-W,
|
| allwritesOK-add-write | proved | all subs proved
| allwritesOK-ind-add-write,
allWritesOK-def,
restrict-vp,
restrict-thread,
|
| allreadsok-add-write | proved | all subs proved
| allreadsok-ind-add-write,
allReadsOK-def,
|
| lastwrite-to-update | proved | all subs proved
| overwrite-attach-read,
overwrite-attach-write,
restrict-vp,
restrict-loc,
restrict-W,
|
| rely-persist | proved | all subs proved
| hist-more-persisted-persistDependetReads,
hist-more-persisted-rec,
hist-more-persisted-append,
restrict-thread,
rely-def,
|
| allreadsok-add-read | proved | all subs proved
| allreadsok-ind-add-read,
allReadsOK-def,
|
| allreadsok-ind-add-read | proved | all subs proved
| allReadsOKInd-recR,
lastPersistedOrElse-recR,
overwrite-rec-read,
allReadsOKInd-recW,
lastPersistedOrElse-recW,
overwrite-rec-write,
allreadsok-ind-one,
lastPersistedOrElse-base,
overwrite-base,
allReadsOKInd-base,
hist-ind,
|
| hist-more-persisted-persistDependetReads | proved | all subs proved
| hist-more-persisted-refl,
persistDependentReads-nextwrite,
persistDependentReads-otherwrite,
hist-more-persisted-rec,
persistDependentReads-read,
persistDependentReads-otherread,
hist-more-persisted-base1,
persistDependentReads-base,
|
| overwrite-attach-write | proved | all subs proved
| overwrite-rec-read,
overwrite-rec-write,
overwrite-base,
overwrite-one-write,
hist-ind,
|
| overwrite-attach-read | proved | all subs proved
| overwrite-rec-write,
overwrite-rec-read,
overwrite-base,
overwrite-one-read,
|
| allreadsok-ind-add-write | proved | all subs proved
| allReadsOKInd-recR,
allReadsOKInd-recW,
allreadsok-ind-one,
allReadsOKInd-base,
hist-ind,
|
| allwritesOK-ind-add-write | proved | all subs proved
| allWritesOKInd-recW,
allWritesOKInd-recR,
allwritesOK-ind-one,
restrict-vp,
restrict-thread,
|
| restrict-true-true | proved | all subs proved
| restrict-vp,
restrict-bool-one,
restrict-b-append,
|
| restrict-true-false | proved | all subs proved
| restrict-vp,
restrict-bool-one,
restrict-b-append,
|
| allwritesOK-ind-add-read | proved | all subs proved
| allWritesOKInd-recW,
allWritesOKInd-recR,
allwritesOK-ind-one,
allWritesOKInd-base,
|
| allwritesOK-ind-swap-flags-persist-one-write | proved | all subs proved
| allwritesOK-ind-swap-to-non-pending,
persisted-update-same,
persisted-update-swap,
pending-update-swap,
allWritesOKInd-recW,
allWritesOKInd-recR,
allWritesOKInd-base,
|
| allWritesOK-ind-filter-persisted | proved | all subs proved
| allWritesOK-ind-filter-persisted-upd-true,
allWritesOKInd-recW,
allWritesOKInd-recR,
allWritesOKInd-base,
|
| allreadsOK-ind-filter-persisted | proved | all subs proved
| allreadsOK-ind-filter-persisted-upd-false,
allReadsOKInd-recW,
allReadsOKInd-recR,
allReadsOKInd-base,
|
| allwritesOK-ind-pending-not-in | proved | all subs proved
| restrict-vp,
restrict-thread,
restrict-W,
allwritesOK-ind-pending-zero-write,
|
| restrict-false-false | proved | all subs proved
| restrict-vp,
restrict-bool-one,
restrict-b-append,
|
| restrict-l-W-other | proved | all subs proved
| restrict-loc,
restrict-l-one,
restrict-l-append,
|
| allReadsOK-one | proved | all subs proved
| allreadsok-ind-one,
allReadsOK-def,
|
| restrict-write-W | proved | all subs proved
| restrict-W,
restrict-write-one,
restrict-W-append,
|
| rely-refl | proved | all subs proved
| hist-more-persisted-refl,
restrict-thread,
rely-def,
|
| rely-stable-write-one | proved | all subs proved
| rely-stable-write-empty,
hist-more-persisted-rec,
restrict-thread,
rely-def,
restrict-vp,
|
| allwritesOK-one-unpersisted-write-no-persisted-after | proved | all subs proved
| allwritesOK-ind-one-unpersisted-write-no-persisted-after,
allWritesOK-def,
restrict-vp,
restrict-loc,
restrict-W,
|
| allwritesOK-persist-dependent-reads | proved | all subs proved
| allwritesOK-ind-persist-dependent-reads,
allWritesOK-def,
|
| restrict-write-attach-R | proved | all subs proved
| restrict-W,
restrict-write-one,
restrict-W-append,
|
| allreadsok-persist | proved | all subs proved
| allreadsok-ind-persist,
allReadsOK-def,
|
| first-vol-write-size2 | proved | all subs proved
| first-vol-write-size3,
first-vol-write-size,
restrict-vp,
restrict-loc,
restrict-W,
|
| restrict-false-true | proved | all subs proved
| restrict-vp,
restrict-bool-one,
restrict-b-append,
|
| allReadsOK-no-initial-unpersisted-read | proved | all subs proved
| restrict-events,
restrict-vp,
restrict-loc,
allReadsOK-ind-no-initial-unpersisted-read,
allReadsOK-def,
|
| allwritesOK-one | proved | all subs proved
| allwritesOK-ind-one,
allWritesOK-def,
|
| rely-attach | proved | all subs proved
| hist-more-persisted-refl,
hist-more-persisted-size-eq,
restrict-thread,
rely-def,
|
| restrict-false-attach-true | proved | all subs proved
| restrict-vp,
restrict-bool-one,
restrict-b-append,
|
| restrict-l-R-other | proved | all subs proved
| restrict-loc,
restrict-l-one,
restrict-l-append,
|
| restrict-l-W-same | proved | all subs proved
| restrict-loc,
restrict-l-one,
restrict-l-append,
|
| first-vol-write-head-restricted | proved | all subs proved
| first-vol-write-rec-read,
first-vol-write-rec-write-other,
first-vol-write-rec-write-unpersisted,
first-vol-write-rec-write-persisted,
hist-ind,
restrict-vp,
restrict-loc,
restrict-W,
|
| restrict-l-R-same | proved | all subs proved
| restrict-loc,
restrict-l-one,
restrict-l-append,
|
| allReadsOK-nowrites-allpersisted | proved | all subs proved
| restrict-vp,
restrict-loc,
restrict-W,
allReadsOK-nowrites-allpersisted-ind,
allReadsOK-def,
|
| restrict-true-attach-true | proved | all subs proved
| restrict-vp,
restrict-bool-one,
restrict-b-append,
|
| restrict-write-R | proved | all subs proved
| restrict-W,
restrict-write-one,
restrict-W-append,
|
| restrict-false-attach-false | proved | all subs proved
| restrict-vp,
restrict-bool-one,
restrict-b-append,
|
| restrict-true-attach-false | proved | all subs proved
| restrict-vp,
restrict-bool-one,
restrict-b-append,
|
| allWritesOK-ind-filter-persisted-upd-true | proved | all subs proved
| persisted-update-swap,
allWritesOKInd-recW,
allWritesOKInd-recR,
allWritesOKInd-base,
|
| hist-more-persisted-append | proved | all subs proved
| hist-more-persisted-rec,
|
| overwrite-one-write | proved | all subs proved
| overwrite-base,
overwrite-rec-write,
|
| allReadsOK-nowrites-allpersisted-ind | proved | all subs proved
| allReadsOKInd-recW,
allReadsOKInd-recR,
restrict-vp,
restrict-loc,
restrict-W,
|
| overwrite-persist-one-write | proved | all subs proved
| overwrite-rec-read,
overwrite-rec-write,
|
| at-overwrite-no-write | proved | all subs proved
| overwrite-rec-write,
overwrite-rec-read,
overwrite-base,
restrict-W,
restrict-loc,
|
| at-overwrite-mem-update-other | proved | all subs proved
| mem-update-same,
mem-update-swap,
overwrite-rec-write,
overwrite-rec-read,
overwrite-base,
|
| first-vol-write-rec-write-persisted | proved | all subs proved
| firstVolWrite-def,
|
| first-vol-write-rec-write-unpersisted | proved | all subs proved
| firstVolWrite-def,
|
| first-vol-write-rec-write-other | proved | all subs proved
| firstVolWrite-def,
|
| first-vol-write-rec-read | proved | all subs proved
| firstVolWrite-def,
|
| allreadsOK-ind-filter-persisted-upd-false | proved | all subs proved
| persisted-update-same,
mem-update-same,
allReadsOKInd-recW,
allReadsOKInd-recR,
allReadsOKInd-base,
|
| hist-more-persisted-size-eq | proved | all subs proved
| hist-more-persisted-rec,
hist-more-persisted-base2,
hist-more-persisted-base1,
|
| allwritesOK-ind-pending-zero-write | proved | all subs proved
| allWritesOKInd-recR,
allWritesOKInd-recW,
restrict-vp,
restrict-thread,
restrict-W,
|
| allwritesOK-ind-one | proved | all subs proved
| allWritesOKInd-recW,
allWritesOKInd-base,
allWritesOKInd-recR,
|
| allReadsOK-ind-no-initial-unpersisted-read | proved | all subs proved
| allReadsOKInd-recW,
allReadsOKInd-recR,
restrict-events,
restrict-vp,
restrict-loc,
|
| first-vol-write-size | proved | all subs proved
| hist-ind,
firstVolWrite-def,
restrict-vp,
restrict-loc,
restrict-W,
|
| first-vol-write-size3 | proved | all subs proved
| firstVolWrite-def,
|
| allreadsok-ind-persist | proved | all subs proved
| mem-update-swap,
persisted-update-swap,
persisted-update-same,
mem-update-same,
persistDependentReads-nextwrite,
persistDependentReads-otherwrite,
persistDependentReads-read,
persistDependentReads-otherread,
allReadsOKInd-recR,
allReadsOKInd-base,
persistDependentReads-base,
allReadsOKInd-recW,
|
| allwritesOK-ind-swap-to-non-pending | proved | all subs proved
| pending-update-swap,
allWritesOKInd-recW,
allWritesOKInd-recR,
allWritesOKInd-base,
|
| allwritesOK-ind-persist-dependent-reads | proved | all subs proved
| persistDependentReads-nextwrite,
persistDependentReads-otherwrite,
allWritesOKInd-recW,
persistDependentReads-read,
persistDependentReads-otherread,
allWritesOKInd-recR,
allWritesOKInd-base,
persistDependentReads-base,
|
| restrict-W-empty | proved | all subs proved
| restrict-W,
|
| restrict-l-empty | proved | all subs proved
| restrict-loc,
|
| restrict-b-empty | proved | all subs proved
| restrict-vp,
|
| overwrite-one-read | proved | all subs proved
| overwrite-base,
overwrite-rec-read,
|
| allwritesOK-ind-one-unpersisted-write-no-persisted-after | proved | all subs proved
| pending-update-swap,
persisted-update-swap,
allWritesOKInd-recR,
persisted-update-same,
allWritesOKInd-recW,
restrict-vp,
restrict-loc,
restrict-W,
|
| rely-stable-write-empty | proved | all subs proved
| hist-more-persisted-rec,
hist-more-persisted-base1,
restrict-thread,
rely-def,
restrict-vp,
|
| hist-more-persisted-refl | proved | all subs proved
| hist-more-persisted-rec,
hist-more-persisted-base1,
|
| restrict-W-append | proved | all subs proved
| restrict-W,
|
| restrict-write-one | proved | all subs proved
| restrict-W,
|
| allreadsok-ind-one | proved | all subs proved
| allReadsOKInd-recW,
allReadsOKInd-base,
allReadsOKInd-recR,
|
| restrict-l-append | proved | all subs proved
| restrict-loc,
|
| restrict-l-one | proved | all subs proved
| restrict-loc,
|
| restrict-b-append | proved | all subs proved
| restrict-vp,
|
| restrict-bool-one | proved | all subs proved
| restrict-vp,
|
| restrict-w-l-swap | proved | all subs proved
| restrict-W,
restrict-loc,
|
| first-vol-write-split | proved | all subs proved
| firstVolWrite-def,
|
| allwritesOK-ind-unpersisted-one-write | proved | all subs proved
| allWritesOKInd-recR,
allWritesOKInd-recW,
|
| take-first-vol-write-no-unpersisted-writes | proved | all subs proved
| firstVolWrite-def,
restrict-vp,
restrict-loc,
restrict-W,
|
| restrict-read-W | proved | all subs proved
| restrict-R,
|
| events-one | proved | all subs proved
| restrict-events,
|
| restrict-l-t-swap | proved | all subs proved
| restrict-loc,
restrict-thread,
|
| persistDependentReads-restrict-other-loc | proved | all subs proved
| persistDependentReads-nextwrite,
persistDependentReads-read,
persistDependentReads-otherwrite,
persistDependentReads-otherread,
persistDependentReads-base,
restrict-loc,
|
| restrict-w-b-swap | proved | all subs proved
| restrict-W,
restrict-vp,
|
| restrict-t-append | proved | all subs proved
| restrict-thread,
|
| allReadsOK-tailread | proved | all subs proved
| allReadsOK-def,
allReadsOKInd-recR,
|
| restrict-read-one | proved | all subs proved
| restrict-R,
|
| persistDependentReads-restrict-single-W | proved | all subs proved
| persistDependentReads-otherread,
persistDependentReads-read,
persistDependentReads-otherwrite,
persistDependentReads-nextwrite,
hist-ind,
restrict-vp,
restrict-thread,
restrict-loc,
|
| persistDependentReads-restrict-empty | proved | all subs proved
| persistDependentReads-otherread,
persistDependentReads-read,
persistDependentReads-otherwrite,
persistDependentReads-nextwrite,
persistDependentReads-base,
hist-ind,
restrict-vp,
restrict-thread,
restrict-loc,
|
| events-append | proved | all subs proved
| restrict-events,
|
| restrict-b-idem | proved | all subs proved
| restrict-vp,
|
| events-empty | proved | all subs proved
| restrict-events,
|
| overwrite-persist-dependent-reads | proved | all subs proved
| persistDependentReads-nextwrite,
persistDependentReads-otherwrite,
overwrite-rec-write,
persistDependentReads-read,
persistDependentReads-otherread,
overwrite-rec-read,
overwrite-base,
persistDependentReads-base,
|
| persistDependentReads-restrict-same-loc | proved | all subs proved
| persistDependentReads-otherwrite,
persistDependentReads-otherread,
persistDependentReads-nextwrite,
persistDependentReads-read,
persistDependentReads-base,
restrict-loc,
|
| rely-unpersisted-subset | proved | all subs proved
| hist-more-persisted-rec,
hist-more-persisted-base2,
hist-more-persisted-base1,
restrict-vp,
restrict-thread,
rely-def,
|
| restrict-true-false-empty | proved | all subs proved
| restrict-vp,
|
| hist-more-persisted-trans | proved | all subs proved
| hist-more-persisted-base2,
hist-more-persisted-rec,
hist-more-persisted-base1,
|
| restrict-w-t-swap | proved | all subs proved
| restrict-W,
restrict-thread,
|
| event-persistDependentReads | proved | all subs proved
| persistDependentReads-nextwrite,
persistDependentReads-otherwrite,
persistDependentReads-read,
persistDependentReads-otherread,
persistDependentReads-base,
restrict-events,
|
| overwrite-persist-dependent-reads-restrict-true | proved | all subs proved
| persistDependentReads-nextwrite,
persistDependentReads-otherwrite,
overwrite-rec-write,
persistDependentReads-read,
persistDependentReads-otherread,
overwrite-rec-read,
overwrite-base,
persistDependentReads-base,
restrict-vp,
|
| restrict-t-one | proved | all subs proved
| restrict-thread,
|
| restrict-read-R | proved | all subs proved
| restrict-R,
|
| restrict-t-b-empty-expand-loc | proved | all subs proved
| restrict-vp,
restrict-thread,
restrict-loc,
|
| restrict-l-b-swap | proved | all subs proved
| restrict-loc,
restrict-vp,
|
| restrict-t-empty | proved | all subs proved
| restrict-thread,
|
| nowrites-lastPersistedtrue | proved | all subs proved
| lastPersistedOrElse-recR,
lastPersistedOrElse-recW,
lastPersistedOrElse-base,
restrict-vp,
restrict-loc,
restrict-W,
|
| persist-dependent-reads-unchanged-writes | proved | all subs proved
| persistDependentReads-read,
persistDependentReads-otherread,
persistDependentReads-nextwrite,
persistDependentReads-otherwrite,
persistDependentReads-base,
hist-ind,
restrict-W,
|
| restrict-t-b-swap | proved | all subs proved
| restrict-thread,
restrict-vp,
|
| restrict-read-attach-W | proved | all subs proved
| restrict-R,
|
| allReadsOK-firstreadpersisted | proved | all subs proved
| allReadsOKInd-recR,
allReadsOK-def,
|
| lastPersisted-false-ex-persisted-write | proved | all subs proved
| lastPersistedOrElse-recW,
lastPersistedOrElse-recR,
lastPersistedOrElse-base,
|
| restrict-R-empty | proved | all subs proved
| restrict-R,
|
| hist-more-persisted-base2 | axiom | | |
| lastPersistedOrElse-base | axiom | | |
| lastPersistedOrElse-recW | axiom | | |
| lastPersistedOrElse-recR | axiom | | |
| allWritesOKInd-base | axiom | | |
| pending-update-swap | proved | all subs proved
| |
| hist-ind | proved | all subs proved
| |
| allReadsOKInd-recW | axiom | | |
| allReadsOKInd-base | axiom | | |
| mem-update-same | proved | all subs proved
| |
| persisted-update-same | proved | all subs proved
| |
| persisted-update-swap | proved | all subs proved
| |
| mem-update-swap | proved | all subs proved
| |
| allReadsOKInd-recR | axiom | | |
| overwrite-base | axiom | | |
| hist-more-persisted-base1 | axiom | | |
| hist-more-persisted-rec | axiom | | |
| rely-def | axiom | | |
| overwrite-rec-write | axiom | | |
| overwrite-rec-read | axiom | | |
| persistDependentReads-base | axiom | | |
| persistDependentReads-otherread | axiom | | |
| persistDependentReads-otherwrite | axiom | | |
| persistDependentReads-read | axiom | | |
| persistDependentReads-nextwrite | axiom | | |
| allWritesOK-def | axiom | | |
| restrict-events | axiom | | |
| allReadsOK-def | axiom | | |
| restrict-R | axiom | | |
| restrict-loc | axiom | | |
| restrict-W | axiom | | |
| restrict-thread | axiom | | |
| restrict-vp | axiom | | |
| allWritesOKInd-recR | axiom | | |
| allWritesOKInd-recW | axiom | | |
| firstVolWrite-def | axiom | | |