[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 ubi-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:
valid-wl-mapprovedall subs proved valid-ebatbl, valid-vtbl, valid-wl, valid-wl-use,
valid-eraseqp-in0provedall subs proved valid-eraseqp-in, valid-eraseqw,
valid-eraseqp-appendprovedall subs proved valid-eraseqp-rec, valid-eraseqp-base, valid-eraseqp-one,
valid-eraseqd-nodups0provedall subs proved valid-eraseqd-nodups1,
valid-eraseqd-appendprovedall subs proved valid-eraseqd-rec, valid-eraseqd-base, valid-eraseqd-one,
valid-wl-useprovedall subs proved valid-wl,
valid-eraseqp-inprovedall subs proved valid-eraseqw,
valid-eraseqp-oneprovedall subs proved valid-eraseqp-base, valid-eraseqp-rec,
valid-eraseqd-nodups1provedall subs proved valid-eraseqd-rec,
valid-eraseqd-oneprovedall subs proved valid-eraseqd-base, valid-eraseqd-rec,
valid-wl-write-validprovedall subs proved valid-wl,
valid-wl-write-unmappedprovedall subs proved valid-ebatbl, valid-vtbl, valid-wl,
valid-wl-used-echdrprovedall subs proved valid-wl,
valid-wl-next-valid-useprovedall subs proved ls-at-subarray-pebs, ls-at-subarray-wlar, valid-wl,
valid-wl-next-valid-updateprovedall subs proved ls-at-subarray-pebs, ls-at-subarray-wlar, unique-sqns, valid-wl,
valid-wl-next-valid-eraseprovedall subs proved ls-at-subarray-pebs, ls-at-subarray-wlar, valid-wl,
valid-wl-next-invalid-eraseprovedall subs proved ls-at-subarray-pebs, ls-at-subarray-wlar, valid-wl,
valid-wl-next-freeprovedall subs proved ls-at-subarray-pebs, ls-at-subarray-wlar, valid-wl,
valid-wl-next-badprovedall subs proved ls-at-subarray-pebs, ls-at-subarray-wlar, valid-wl,
valid-wl-markbadprovedall subs proved valid-wl,
valid-wl-free-echdrprovedall subs proved valid-wl,
valid-wl-freeprovedall subs proved valid-wl,
valid-wl-erasing-update-ecprovedall subs proved valid-wl,
valid-wl-erasing-invalidate0provedall subs proved valid-wl,
valid-wl-erasing-invalidateprovedall subs proved valid-wl,
valid-wl-eraseprovedall subs proved valid-wl,
valid-wl-ebatbl-used-imp-valid-ehdrprovedall subs proved valid-ebatbl, valid-wl,
valid-wl-ebatbl-used-imp-mappedprovedall subs proved valid-ebatbl, valid-wl,
valid-wl-array-0provedall subs proved valid-wl,
valid-vtbl-wlar-statusprovedall subs proved valid-vtbl,
valid-vtbl-update-volsprovedall subs proved valid-vtbl,
valid-vtbl-update-other-wlarprovedall subs proved valid-vtbl,
valid-vtbl-update-other-pebsprovedall subs proved valid-vtbl,
valid-vtbl-sqns-notemptyprovedall subs proved valid-vtbl, valid-wl,
valid-vtbl-in-wlarprovedall subs proved valid-vtbl,
valid-vtbl-bufprovedall subs proved valid-vtbl,
valid-global-sqn-write-validprovedall subs proved valid-global-sqn,
valid-global-sqn-notinprovedall subs proved valid-global-sqn,
valid-global-sqn-not-lsprovedall subs proved valid-global-sqn,
valid-global-sqn-not-leqprovedall subs proved valid-global-sqn,
valid-global-sqn-next-maxprovedall subs proved valid-global-sqn,
valid-global-sqn-nextprovedall subs proved valid-global-sqn,
valid-global-sqn-invalidateprovedall subs proved valid-global-sqn,
valid-global-sqn-incprovedall subs proved valid-global-sqn,
valid-global-sqn-array-0provedall subs proved valid-global-sqn,
valid-global-sqn-add-validprovedall subs proved valid-global-sqn,
valid-eraseqw-useprovedall subs proved valid-eraseqw,
valid-eraseqw-update-ecprovedall subs proved valid-eraseqw,
valid-eraseqw-unmapprovedall subs proved valid-eraseqw,
valid-eraseqw-subarray-shiftprovedall subs proved ls-at-subarray-wlar, valid-eraseqw,
valid-eraseqw-size-middleprovedall subs proved valid-eraseqw,
valid-eraseqw-size-leftprovedall subs proved valid-eraseqw,
valid-eraseqw-free-inprovedall subs proved valid-eraseqw,
valid-eraseqw-freeprovedall subs proved valid-eraseqw,
valid-eraseqp-valid-lebrefprovedall subs proved valid-eraseqp-rec,
valid-eraseqp-update-otherprovedall subs proved valid-eraseqp-rec, valid-eraseqp-base,
valid-eraseqp-rem-middleprovedall subs proved valid-eraseqp-rec,
valid-eraseqp-invalidateprovedall subs proved valid-eraseqp-rec, valid-eraseqp-base,
valid-eraseqd-rem-middleprovedall subs proved valid-eraseqd-rec,
valid-eraseqd-nodups-middle2provedall subs proved valid-eraseqd-rec,
valid-eraseqd-nodups-middle1provedall subs proved valid-eraseqd-rec,
valid-eraseqd-nodups-middle0provedall subs proved valid-eraseqd-rec,
valid-eraseq-prev-erasingprovedall subs proved ls-at-subarray-wlar, valid-eraseqw,
valid-eraseq-next-erasingprovedall subs proved ls-at-subarray-wlar, valid-eraseqw,
valid-eraseq-array-0provedall subs proved valid-eraseqw,
valid-ebatbl-write-dataprovedall subs proved valid-ebatbl,
valid-ebatbl-update-wlar-unusedprovedall subs proved valid-ebatbl,
valid-ebatbl-update-vhdrs-unusedprovedall subs proved valid-ebatbl,
valid-ebatbl-unmapprovedall subs proved valid-ebatbl,
valid-ebatbl-remapprovedall subs proved valid-ebatbl,
valid-ebatbl-move-vtblprovedall subs proved valid-ebatbl,
valid-ebatbl-mapprovedall subs proved valid-ebatbl,
valid-ebatbl-add-unmapped-volprovedall subs proved valid-ebatbl,
unique-sqns-write-validprovedall subs proved unique-sqns,
unique-sqns-updateprovedall subs proved unique-sqns,
unique-sqns-2-valid-pebsprovedall subs proved unique-sqns,
mapped-pebs-unusedprovedall subs proved valid-ebatbl, mapped-pebs,
mapped-pebs-unmapprovedall subs proved mapped-pebs, valid-ebatbl,
mapped-pebs-remapprovedall subs proved mapped-pebs, valid-ebatbl,
mapped-pebs-rem-notmappedprovedall subs proved valid-ebatbl, mapped-pebs,
mapped-pebs-atprovedall subs proved mapped-pebs,
mapped-pebs-add-empty-volprovedall subs proved mapped-pebs,
is-vtbl-pnumprovedall subs proved valid-ebatbl, valid-wl,
in-valid-eraseqp-valid-lrefprovedall subs proved valid-eraseqp-rec,
idset-write-notinprovedall subs proved id-set,
idset-weakenprovedall subs proved id-set,
idset-trans-intersectprovedall subs proved id-set,
idset-reflprovedall subs proved id-set,
idset-mapped-pebs-write-unusedprovedall subs proved mapped-pebs, id-set, valid-ebatbl,
idset-idexpt-fwdprovedall subs proved id-set,
idset-idexptprovedall subs proved id-set,
bitflips-cons-inprovedall subs proved bflipset-cons,
bitflips-cons-emptyprovedall subs proved bflipset-cons,
bitflip-cons-set-usedprovedall subs proved bflipset-cons,
bitflip-cons-setprovedall subs proved bflipset-cons,
bitflip-cons-delprovedall subs proved bflipset-cons,
bitflip-cons-addprovedall subs proved bflipset-cons,
bflipset-subarray-nextprovedall subs proved ls-at-subarray-wlar, bflipset-cons,
bflipset-subarray-erase-old-addprovedall subs proved ls-at-subarray-wlar, bflipset-cons,
bflipset-subarray-erase-oldprovedall subs proved ls-at-subarray-wlar, bflipset-cons,
bflipset-subarray-addprovedall subs proved ls-at-subarray-wlar, bflipset-cons,
ls-at-subarray-pebsprovedall subs proved
valid-vtblaxiom
valid-global-sqnaxiom
valid-eraseqp-baseaxiom
valid-eraseqd-baseaxiom
valid-eraseqd-recaxiom
valid-eraseqwaxiom
unique-sqnsaxiom
valid-wlaxiom
valid-eraseqp-recaxiom
valid-ebatblaxiom
mapped-pebsaxiom
id-setaxiom
bflipset-consaxiom
ls-at-subarray-wlarprovedall subs proved