[Imprint][Data Privacy Statement][E-Mail]

Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Lemma dependency for Specification persistence-base

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:
lpt-free-unref-replay-lptprovedall subs proved replay-lpt-at-above, replay-lpt-at, replay-lpt-size, lpt-free-unref,
gc-heap-update-logprovedall subs proved gc-heap-update-log-h, gc-heap,
gc-heap-updateprovedall subs proved gc-heap-update-h, gc-heap,
gc-heap-freeprovedall subs proved gc-heap-free-h, gc-heap,
gc-heap-append-logprovedall subs proved gc-heap-append-log-h, gc-heap,
cleanup-lpt-to-nprovedall subs proved cleanup-lpt-n-at, cleanup-lpt-n-size, cleanup-lpt,
abs-istore-replay-lpt-unchangedprovedall subs proved replay-lpt-at, avol-replay-lpt-unchanged, replay-lpt-size, abs-istore-def,
abs-istore-crashprovedall subs proved replay-lpt-at-above, replay-lpt-at, lpt-free-unref, flash-lpt-cons, replay-lpt-size, replay-log, abs-istore-def,
abs-gstore-replay-lpt-unchangedprovedall subs proved replay-lpt-at, avol-replay-lpt-unchanged, replay-lpt-size, abs-gstore-def,
abs-gstore-crashprovedall subs proved replay-lpt-at, lpt-free-unref, flash-lpt-cons, replay-lpt-size, replay-log, abs-gstore-def, abs-istore-def, bufs-log-only, lpt-ram-flash,
gc-heap-update-log-hprovedall subs proved gc-heap-write-above, gc-heap-rec, gc-heap-base,
gc-heap-update-hprovedall subs proved gc-heap-in-h, gc-heap-write-above, gc-heap-rec, gc-heap-base,
gc-heap-free-hprovedall subs proved gc-heap-in-h, gc-heap-write-above, gc-heap-rec, gc-heap-base,
gc-heap-append-log-hprovedall subs proved gc-heap-in-h,
cleanup-lpt-n-atprovedall subs proved cleanup-lpt-n-read-above, cleanup-lpt-n-size, cleanup-lpt-rec, cleanup-lpt-base,
replay-lpt-atprovedall subs proved replay-lpt-size, replay-lpt-at-above, replay-lpt-rec, replay-lpt-base,
id-idx-gcheapprovedall subs proved gc-heap-ididx-h, gc-heap,
gc-heap-write-otherprovedall subs proved gc-heap-write-other-h, gc-heap,
gc-heap-write-nochangeprovedall subs proved gc-heap-write-nochange-h, gc-heap,
gc-heap-remove-wbufsprovedall subs proved remove-wbufs, gc-heap-remove-wbufs-h, gc-heap,
gc-heap-inprovedall subs proved gc-heap-in-h, gc-heap,
gc-heap-fill-freeprovedall subs proved gc-heap-fill-free-h, gc-heap,
gc-heap-allocateprovedall subs proved gc-heap-allocate-h, gc-heap,
bin-heap-inv-write-otherprovedall subs proved gc-heap-in-h, gc-heap,
gc-heap-ididx-hprovedall subs proved gc-heap-rec, gc-heap-base,
gc-heap-write-other-hprovedall subs proved gc-heap-rec, gc-heap-base,
gc-heap-write-nochange-hprovedall subs proved gc-heap-rec, gc-heap-base,
gc-heap-remove-wbufs-hprovedall subs proved gc-heap-rec, gc-heap-base, remove-wbufs,
gc-heap-write-aboveprovedall subs proved gc-heap-rec, gc-heap-base,
gc-heap-fill-free-hprovedall subs proved gc-heap-rec, gc-heap-base,
gc-heap-allocate-hprovedall subs proved gc-heap-rec, gc-heap-base,
cleanup-lpt-n-sizeprovedall subs proved cleanup-lpt-rec, cleanup-lpt-base,
cleanup-lpt-n-read-aboveprovedall subs proved cleanup-lpt-rec, cleanup-lpt-base,
gc-heap-in-hprovedall subs proved gc-heap-rec, gc-heap-base,
replay-lpt-at-aboveprovedall subs proved replay-lpt-rec, replay-lpt-base,
replay-lpt-sizeprovedall subs proved replay-lpt-rec, replay-lpt-base,
replay-log-sizeprovedall subs proved replay-log,
replay-log-baseprovedall subs proved replay-log,
replay-log-at-otherprovedall subs proved replay-log,
replay-log-atprovedall subs proved replay-log,
replay-log-append-oneprovedall subs proved replay-log,
remove-wbufs-sizeprovedall subs proved remove-wbufs,
remove-wbufs-recprovedall subs proved remove-wbufs,
remove-wbufs-emptyprovedall subs proved remove-wbufs,
remove-wbufs-atprovedall subs proved remove-wbufs,
lpt-ram-flash-write-sameprovedall subs proved lpt-ram-flash,
lpt-ram-flash-write-non-groupprovedall subs proved lpt-ram-flash,
lpt-ram-flash-write-log-bufprovedall subs proved bufs-log-only, lpt-ram-flash,
lpt-ram-flash-write-logprovedall subs proved lpt-ram-flash,
lpt-ram-flash-write-allocateprovedall subs proved lpt-ram-flash,
lpt-ram-flash-reflprovedall subs proved lpt-ram-flash,
lpt-ram-flash-id-idxprovedall subs proved lpt-ram-flash,
lpt-ram-flash-commitprovedall subs proved lpt-ram-flash,
lpt-ram-flash-cleanupprovedall subs proved cleanup-lpt, lpt-ram-flash,
lpt-ram-flash-allocateprovedall subs proved lpt-ram-flash,
lpt-leb-size-writeprovedall subs proved lpt-leb-size,
lpt-leb-size-id-idxprovedall subs proved lpt-leb-size,
lpt-leb-size-cleanupprovedall subs proved cleanup-lpt, lpt-leb-size,
lpt-leb-size-atprovedall subs proved lpt-leb-size,
lpt-free-unref-writeprovedall subs proved lpt-free-unref,
lpt-free-unref-replay-logprovedall subs proved replay-log, lpt-free-unref,
lpt-free-unref-remove-wbufsprovedall subs proved lpt-free-unref, remove-wbufs,
lpt-free-unref-cleanup-lptprovedall subs proved lpt-free-unref, cleanup-lpt,
log-group-block-write-otherprovedall subs proved log-group-block,
log-group-block-write-atprovedall subs proved log-group-block,
log-group-block-remove-wbufsprovedall subs proved remove-wbufs, log-group-block,
log-group-block-id-idxprovedall subs proved log-group-block,
log-group-block-emptyprovedall subs proved log-group-block,
log-disjoint-istoreprovedall subs proved abs-gstore-def, abs-istore-def,
id-idx-lpt-free-unrefprovedall subs proved lpt-free-unref,
id-idx-freelist-consprovedall subs proved freelist-cons,
id-idx-abs-istoreprovedall subs proved abs-istore-def,
id-idx-abs-gstoreprovedall subs proved abs-gstore-def,
freelist-cons-write-lpt-otherprovedall subs proved freelist-cons,
freelist-cons-remove-wbufsprovedall subs proved remove-wbufs, freelist-cons,
freelist-cons-first-freeprovedall subs proved freelist-cons,
freelist-cons-allocprovedall subs proved freelist-cons,
freelist-cons-addprovedall subs proved freelist-cons,
free-unref-atprovedall subs proved lpt-free-unref,
cleanup-lpt-sizeprovedall subs proved cleanup-lpt,
bufs-log-only-write-lpt-same-flagsprovedall subs proved bufs-log-only,
bufs-log-only-write-lpt-freeprovedall subs proved bufs-log-only,
bufs-log-only-rembufprovedall subs proved bufs-log-only,
bufs-log-only-notfreeprovedall subs proved bufs-log-only,
bufs-log-only-id-idxprovedall subs proved bufs-log-only,
bufs-log-only-emptyprovedall subs proved bufs-log-only,
buf-ro-rw-mode-write-vol-otherprovedall subs proved buf-ro-rw-mode,
buf-ro-rw-mode-write-other-fieldsprovedall subs proved buf-ro-rw-mode,
buf-ro-rw-mode-write-lpt-otherprovedall subs proved buf-ro-rw-mode,
buf-ro-rw-mode-writeprovedall subs proved buf-ro-rw-mode,
buf-ro-rw-mode-switchprovedall subs proved buf-ro-rw-mode,
buf-ro-rw-mode-nobufferprovedall subs proved buf-ro-rw-mode,
buf-ro-rw-mode-leb-sizeprovedall subs proved buf-ro-rw-mode,
buf-ro-rw-mode-id-idxprovedall subs proved buf-ro-rw-mode,
binheap-inv-remove-wbufsprovedall subs proved remove-wbufs,
bin-heap-inv-cleanup-lptprovedall subs proved cleanup-lpt,
avol-replay-lpt-unchanged-write-rightprovedall subs proved avol-replay-lpt-unchanged,
avol-replay-lpt-unchanged-sizeprovedall subs proved avol-replay-lpt-unchanged,
avol-replay-lpt-unchanged-reflprovedall subs proved avol-replay-lpt-unchanged,
avol-replay-lpt-unchanged-extract-rightprovedall subs proved avol-replay-lpt-unchanged,
avol-cleanup-lpt-unchanged-reflprovedall subs proved avol-cleanup-lpt-unchanged,
avol-cleanup-lpt-unchanged-extract-rightprovedall subs proved avol-cleanup-lpt-unchanged,
abs-nodes-inv-flashsizeprovedall subs proved abs-nodes-inv-flashsize-h,
abs-istore-set-refsizeprovedall subs proved abs-istore-def,
abs-istore-set-lebsizeprovedall subs proved abs-istore-def,
abs-istore-reduce-write-idcircleprovedall subs proved abs-istore-def,
abs-istore-reduce-writeprovedall subs proved abs-istore-def,
abs-istore-lpt-change-otherprovedall subs proved abs-istore-def,
abs-istore-idcircleprovedall subs proved abs-istore-def,
abs-istore-cleanup-lptprovedall subs proved avol-cleanup-lpt-unchanged, abs-istore-def, cleanup-lpt,
abs-istore-avol-change-otherprovedall subs proved abs-istore-def,
abs-gstore-set-refsizeprovedall subs proved abs-gstore-def,
abs-gstore-set-lebsizeprovedall subs proved abs-gstore-def,
abs-gstore-reduce-write-idcircleprovedall subs proved abs-gstore-def,
abs-gstore-reduce-writeprovedall subs proved abs-gstore-def,
abs-gstore-lpt-change-otherprovedall subs proved abs-gstore-def,
abs-gstore-idcircleprovedall subs proved abs-gstore-def,
abs-gstore-cleanup-lptprovedall subs proved avol-cleanup-lpt-unchanged, abs-gstore-def, cleanup-lpt,
abs-gstore-avol-change-otherprovedall subs proved abs-gstore-def,
replay-lpt-baseaxiom
replay-lpt-recaxiom
lpt-leb-sizeaxiom
log-group-blockaxiom
gc-heap-baseaxiom
gc-heap-recaxiom
freelist-consaxiom
cleanup-lpt-baseaxiom
cleanup-lpt-recaxiom
buf-ro-rw-modeaxiom
remove-wbufsaxiom
gc-heapaxiom
abs-nodes-inv-flashsize-hprovedall subs proved
avol-replay-lpt-unchangedaxiom
lpt-ram-flashaxiom
bufs-log-onlyaxiom
abs-istore-defaxiom
replay-logaxiom
flash-lpt-consaxiom
lpt-free-unrefaxiom
cleanup-lptaxiom
avol-cleanup-lpt-unchangedaxiom
abs-gstore-defaxiom