[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 ubi-base

bflipset-cons(0,0)id-set(0,0)mapped-pebs-add-empty-vol(11,3)valid-ebatbl-map(34,3)valid-eraseqd-nodups-middle1(7,0)valid-eraseqp-rec(0,0)valid-global-sqn(0,0)valid-vtbl-in-wlar(2,0)valid-wl-erasing-update-ec(27,0)valid-wl-write-unmapped(46,10)
bflipset-subarray-add(9,0)idset-idexpt(13,2)mapped-pebs-at(3,0)valid-ebatbl-move-vtbl(10,1)valid-eraseqd-nodups-middle2(7,0)valid-eraseqp-rem-middle(9,0)valid-global-sqn-add-valid(18,3)valid-vtbl-sqns-notempty(7,0)valid-wl-free(20,1)valid-wl-write-valid(48,10)
bflipset-subarray-erase-old(9,0)idset-idexpt-fwd(7,1)mapped-pebs-rem-notmapped(3,1)valid-ebatbl-remap(68,0)valid-eraseqd-nodups0(2,0)valid-eraseqp-update-other(21,0)valid-global-sqn-array-0(1,0)valid-vtbl-update-other-pebs(2,0)valid-wl-free-echdr(3,0)wl-threshold-nonzero(0,0)
bflipset-subarray-erase-old-add(9,0)idset-mapped-pebs-write-unused(7,3)mapped-pebs-remap(52,6)valid-ebatbl-unmap(53,0)valid-eraseqd-nodups1(9,1)valid-eraseqp-valid-lebref(10,2)valid-global-sqn-inc(3,0)valid-vtbl-update-other-wlar(2,0)valid-wl-map(20,3)write-once-inv(0,0)
bflipset-subarray-next(12,0)idset-refl(1,0)mapped-pebs-unmap(43,5)valid-ebatbl-update-vhdrs-unused(22,0)valid-eraseqd-one(4,3)valid-eraseqw(0,0)valid-global-sqn-invalidate(11,2)valid-vtbl-update-vols(6,1)valid-wl-markbad(20,4)
bitflip-cons-add(9,2)idset-trans-intersect(5,0)mapped-pebs-unused(3,1)valid-ebatbl-update-wlar-unused(22,0)valid-eraseqd-rec(0,0)valid-eraseqw-free(16,6)valid-global-sqn-next(17,4)valid-vtbl-wlar-status(2,0)valid-wl-next-bad(16,2)
bitflip-cons-del(4,0)idset-weaken(3,0)ubi-cons(0,0)valid-ebatbl-write-data(22,0)valid-eraseqd-rem-middle(11,1)valid-eraseqw-free-in(5,0)valid-global-sqn-next-max(21,2)valid-wl(0,0)valid-wl-next-free(31,0)
bitflip-cons-set(15,2)idset-write-notin(2,0)unique-sqns(0,0)valid-eraseq-array-0(1,0)valid-eraseqp-append(11,0)valid-eraseqw-size-left(3,0)valid-global-sqn-not-leq(3,0)valid-wl-array-0(1,0)valid-wl-next-invalid-erase(16,2)
bitflip-cons-set-used(13,0)in-valid-eraseqp-valid-lref(17,0)unique-sqns-2-valid-pebs(9,2)valid-eraseq-next-erasing(16,0)valid-eraseqp-base(0,0)valid-eraseqw-size-middle(3,0)valid-global-sqn-not-ls(3,0)valid-wl-ebatbl-used-imp-mapped(13,0)valid-wl-next-valid-erase(19,2)
bitflips-cons-empty(1,0)is-vtbl-pnum(7,0)unique-sqns-update(22,7)valid-eraseq-prev-erasing(20,0)valid-eraseqp-in(5,0)valid-eraseqw-subarray-shift(18,0)valid-global-sqn-notin(3,1)valid-wl-ebatbl-used-imp-valid-ehdr(11,0)valid-wl-next-valid-update(35,7)
bitflips-cons-in(3,0)ls-at-subarray-pebs(2,0)unique-sqns-write-valid(22,3)valid-eraseqd-append(16,0)valid-eraseqp-in0(4,1)valid-eraseqw-unmap(6,0)valid-global-sqn-write-valid(24,3)valid-wl-erase(12,0)valid-wl-next-valid-use(27,5)
datasize-alignup(7,3)ls-at-subarray-wlar(2,0)valid-ebatbl(0,0)valid-eraseqd-base(0,0)valid-eraseqp-invalidate(25,1)valid-eraseqw-update-ec(19,0)valid-vtbl(0,0)valid-wl-erasing-invalidate(23,4)valid-wl-use(41,9)
erase-worker-inv(0,0)mapped-pebs(0,0)valid-ebatbl-add-unmapped-vol(37,0)valid-eraseqd-nodups-middle0(7,0)valid-eraseqp-one(5,3)valid-eraseqw-use(19,0)valid-vtbl-buf(2,0)valid-wl-erasing-invalidate0(22,3)valid-wl-used-echdr(3,0)