[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,

Theorem base summary for Specification persistence-base

abs-gstore-avol-change-other(61,0)abs-istore-idcircle(12,3)avol-replay-lpt-unchanged-size(2,0)bufs-log-only(0,0)flash-lpt-cons(0,0)gc-heap-fill-free-h(7,2)gc-heap-write-nochange-h(11,3)log-group-block-write-other(8,0)lpt-ram-flash-commit(1,0)replay-log-append-one(10,4)
abs-gstore-cleanup-lpt(30,6)abs-istore-lpt-change-other(67,0)avol-replay-lpt-unchanged-write-right(11,1)bufs-log-only-empty(1,0)free-unref-at(3,1)gc-heap-free(3,1)gc-heap-write-other(3,1)lpt-free-unref(0,0)lpt-ram-flash-id-idx(25,6)replay-log-at(4,1)
abs-gstore-crash(88,25)abs-istore-reduce-write(25,3)bin-heap-inv-cleanup-lpt(30,11)bufs-log-only-id-idx(11,2)freelist-cons(0,0)gc-heap-free-h(15,6)gc-heap-write-other-h(11,3)lpt-free-unref-cleanup-lpt(19,5)lpt-ram-flash-refl(1,0)replay-log-at-other(3,1)
abs-gstore-def(0,0)abs-istore-reduce-write-idcircle(28,5)bin-heap-inv-write-other(45,19)bufs-log-only-notfree(2,0)freelist-cons-add(10,0)gc-heap-ididx-h(9,3)id-idx-abs-gstore(37,12)lpt-free-unref-remove-wbufs(20,5)lpt-ram-flash-write-allocate(1,0)replay-log-base(1,0)
abs-gstore-idcircle(17,6)abs-istore-replay-lpt-unchanged(33,7)bin-heap-inv-write-other-fields(27,9)bufs-log-only-rembuf(2,0)freelist-cons-alloc(6,0)gc-heap-in(3,1)id-idx-abs-istore(37,12)lpt-free-unref-replay-log(9,2)lpt-ram-flash-write-log(2,0)replay-log-size(1,0)
abs-gstore-lpt-change-other(75,0)abs-istore-set-lebsize(17,3)binheap-inv-remove-wbufs(21,6)bufs-log-only-write-lpt-free(11,0)freelist-cons-first-free(4,1)gc-heap-in-h(11,2)id-idx-freelist-cons(16,6)lpt-free-unref-replay-lpt(20,5)lpt-ram-flash-write-log-buf(9,2)replay-lpt-at(36,18)
abs-gstore-reduce-write(24,3)abs-istore-set-refsize(16,4)buf-ro-rw-mode(0,0)bufs-log-only-write-lpt-same-flags(12,0)freelist-cons-remove-wbufs(8,2)gc-heap-rec(0,0)id-idx-gcheap(5,2)lpt-free-unref-write(15,0)lpt-ram-flash-write-non-group(10,1)replay-lpt-at-above(17,1)
abs-gstore-reduce-write-idcircle(26,5)abs-nodes-inv-flashsize(2,1)buf-ro-rw-mode-id-idx(7,2)cleanup-lpt(0,0)freelist-cons-write-lpt-other(12,0)gc-heap-remove-wbufs(2,2)id-idx-lpt-free-unref(21,6)lpt-leb-size(0,0)lpt-ram-flash-write-same(21,5)replay-lpt-base(0,0)
abs-gstore-replay-lpt-unchanged(45,13)abs-nodes-inv-flashsize-h(18,7)buf-ro-rw-mode-leb-size(1,0)cleanup-lpt-base(0,0)gc-heap(0,0)gc-heap-remove-wbufs-h(23,4)id-idx-write-both(14,4)lpt-leb-size-at(3,1)read-gblock-inv(0,0)replay-lpt-rec(0,0)
abs-gstore-set-lebsize(17,3)avol-cleanup-lpt-unchanged(0,0)buf-ro-rw-mode-nobuffer(1,0)cleanup-lpt-n-at(11,2)gc-heap-allocate(3,1)gc-heap-update(3,1)log-disjoint-istore(11,3)lpt-leb-size-cleanup(11,1)remove-wbufs(0,0)replay-lpt-size(15,1)
abs-gstore-set-refsize(16,4)avol-cleanup-lpt-unchanged-extract-right(4,1)buf-ro-rw-mode-switch(2,0)cleanup-lpt-n-read-above(9,1)gc-heap-allocate-h(10,3)gc-heap-update-h(21,7)log-group-block(0,0)lpt-leb-size-id-idx(17,5)remove-wbufs-at(6,2)set-less-ar0(4,1)
abs-istore-avol-change-other(53,0)avol-cleanup-lpt-unchanged-refl(1,0)buf-ro-rw-mode-write(2,0)cleanup-lpt-n-size(8,2)gc-heap-append-log(3,1)gc-heap-update-log(3,1)log-group-block-empty(1,0)lpt-leb-size-write(19,0)remove-wbufs-empty(1,0)set-less-ar1(4,1)
abs-istore-cleanup-lpt(22,2)avol-replay-lpt-unchanged(0,0)buf-ro-rw-mode-write-lpt-other(9,0)cleanup-lpt-rec(0,0)gc-heap-append-log-h(12,5)gc-heap-update-log-h(16,5)log-group-block-id-idx(6,1)lpt-ram-flash(0,0)remove-wbufs-rec(15,5)
abs-istore-crash(53,19)avol-replay-lpt-unchanged-extract-right(4,0)buf-ro-rw-mode-write-other-fields(5,0)cleanup-lpt-size(1,0)gc-heap-base(0,0)gc-heap-write-above(8,3)log-group-block-remove-wbufs(10,3)lpt-ram-flash-allocate(7,1)remove-wbufs-size(1,0)
abs-istore-def(0,0)avol-replay-lpt-unchanged-refl(1,0)buf-ro-rw-mode-write-vol-other(6,0)cleanup-lpt-to-n(6,2)gc-heap-fill-free(2,1)gc-heap-write-nochange(3,1)log-group-block-write-at(6,0)lpt-ram-flash-cleanup(13,3)replay-log(0,0)