[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,
Used simplifier rules/spec theorems by specification
Used from specification apeb
- apeb/elim
is used by
valid-wl-write-valid,
valid-wl-write-unmapped,
valid-wl-use,
valid-wl-next-valid-use,
valid-wl-next-valid-update,
valid-wl-next-valid-erase,
valid-wl-next-invalid-erase,
valid-wl-next-free,
valid-wl-next-bad,
valid-wl-markbad,
valid-wl-map,
valid-wl-free,
valid-wl-erasing-update-ec,
valid-wl-erasing-invalidate0,
valid-wl-erasing-invalidate,
valid-wl-erase,
valid-wl-ebatbl-used-imp-mapped,
valid-vtbl-update-vols,
valid-vtbl-sqns-notempty,
valid-global-sqn-next,
valid-global-sqn-invalidate,
valid-global-sqn-add-valid,
valid-eraseqp-valid-lebref,
valid-eraseqp-update-other,
valid-eraseqp-rem-middle,
valid-eraseqp-one,
valid-eraseqp-invalidate,
valid-eraseqp-append,
valid-ebatbl-write-data,
valid-ebatbl-update-wlar-unused,
valid-ebatbl-update-vhdrs-unused,
valid-ebatbl-unmap,
valid-ebatbl-remap,
valid-ebatbl-move-vtbl,
valid-ebatbl-map,
valid-ebatbl-add-unmapped-vol,
unique-sqns-update,
unique-sqns-2-valid-pebs,
mapped-pebs-unmap,
mapped-pebs-remap,
in-valid-eraseqp-valid-lref,
- apeb/inj
is used by
valid-wl-write-valid,
valid-wl-write-unmapped,
valid-wl-use,
valid-wl-next-valid-use,
valid-wl-next-valid-update,
valid-wl-next-valid-erase,
valid-wl-next-invalid-erase,
valid-wl-next-free,
valid-wl-next-bad,
valid-wl-markbad,
valid-wl-map,
valid-wl-free,
valid-wl-erasing-invalidate0,
valid-wl-erasing-invalidate,
valid-eraseqp-invalidate,
valid-ebatbl-write-data,
valid-ebatbl-update-vhdrs-unused,
valid-ebatbl-remap,
valid-ebatbl-map,
- apeb/sel-04
is used by
valid-wl-write-unmapped,
valid-wl-used-echdr,
valid-wl-use,
valid-wl-next-valid-use,
valid-wl-next-valid-update,
valid-wl-next-valid-erase,
valid-wl-next-invalid-erase,
valid-wl-next-free,
valid-wl-next-bad,
valid-wl-markbad,
valid-wl-map,
valid-wl-free-echdr,
valid-wl-free,
valid-wl-erasing-update-ec,
valid-wl-erasing-invalidate0,
valid-wl-erasing-invalidate,
valid-wl-erase,
valid-wl-ebatbl-used-imp-valid-ehdr,
valid-wl-ebatbl-used-imp-mapped,
valid-vtbl-sqns-notempty,
- apeb/sel-05
is used by
valid-wl-write-valid,
valid-wl-write-unmapped,
valid-wl-used-echdr,
valid-wl-use,
valid-wl-next-valid-use,
valid-wl-next-valid-update,
valid-wl-next-valid-erase,
valid-wl-next-invalid-erase,
valid-wl-next-free,
valid-wl-next-bad,
valid-wl-markbad,
valid-wl-map,
valid-wl-free,
valid-wl-erasing-update-ec,
valid-wl-erasing-invalidate0,
valid-wl-erasing-invalidate,
valid-wl-erase,
valid-wl-ebatbl-used-imp-valid-ehdr,
valid-wl-ebatbl-used-imp-mapped,
valid-vtbl-sqns-notempty,
valid-vtbl-buf,
valid-global-sqn-write-valid,
valid-global-sqn-next-max,
valid-global-sqn-add-valid,
valid-eraseqp-one,
valid-eraseqp-append,
valid-ebatbl-write-data,
valid-ebatbl-update-wlar-unused,
valid-ebatbl-update-vhdrs-unused,
valid-ebatbl-unmap,
valid-ebatbl-remap,
valid-ebatbl-move-vtbl,
valid-ebatbl-map,
valid-ebatbl-add-unmapped-vol,
unique-sqns-write-valid,
unique-sqns-update,
unique-sqns-2-valid-pebs,
mapped-pebs-unmap,
mapped-pebs-remap,
is-vtbl-pnum,
- apeb/sel-06
is used by
valid-wl-write-unmapped,
valid-wl-use,
valid-wl-next-valid-use,
valid-wl-next-valid-update,
valid-vtbl-buf,
- apeb/sel-08
is used by
valid-wl-write-unmapped,
valid-wl-used-echdr,
valid-wl-use,
valid-wl-next-valid-use,
valid-wl-next-valid-update,
valid-wl-next-valid-erase,
valid-wl-next-invalid-erase,
valid-wl-next-free,
valid-wl-next-bad,
valid-wl-markbad,
valid-wl-map,
valid-wl-free-echdr,
valid-wl-free,
valid-wl-erasing-update-ec,
valid-wl-erasing-invalidate0,
valid-wl-erasing-invalidate,
valid-wl-erase,
valid-wl-ebatbl-used-imp-valid-ehdr,
valid-wl-ebatbl-used-imp-mapped,
valid-vtbl-sqns-notempty,
is-vtbl-pnum,
Used from specification nat-basic
- nat-basic/a
is used by
valid-wl-next-valid-use,
valid-wl-next-valid-update,
valid-wl-next-valid-erase,
valid-wl-next-invalid-erase,
valid-wl-next-free,
valid-wl-next-bad,
valid-global-sqn-next-max,
valid-global-sqn-next,
valid-global-sqn-inc,
valid-eraseqw-subarray-shift,
valid-eraseq-prev-erasing,
valid-eraseq-next-erasing,
ls-at-subarray-wlar,
ls-at-subarray-pebs,
bflipset-subarray-next,
bflipset-subarray-erase-old-add,
bflipset-subarray-erase-old,
bflipset-subarray-add,
- nat-basic/add-base
is used by
valid-wl-next-valid-use,
valid-wl-next-valid-update,
valid-wl-next-valid-erase,
valid-wl-next-invalid-erase,
valid-wl-next-free,
valid-wl-next-bad,
ls-at-subarray-wlar,
ls-at-subarray-pebs,
- nat-basic/c
is used by
valid-wl-next-valid-use,
valid-wl-next-valid-update,
valid-wl-next-valid-erase,
valid-wl-next-invalid-erase,
valid-wl-next-free,
valid-wl-next-bad,
valid-global-sqn-next-max,
valid-global-sqn-next,
valid-global-sqn-inc,
valid-eraseqw-subarray-shift,
valid-eraseq-prev-erasing,
valid-eraseq-next-erasing,
ls-at-subarray-wlar,
ls-at-subarray-pebs,
bflipset-subarray-next,
bflipset-subarray-erase-old-add,
bflipset-subarray-erase-old,
bflipset-subarray-add,
- nat-basic/f
is used by
valid-wl-write-valid,
valid-wl-write-unmapped,
valid-wl-used-echdr,
valid-wl-use,
valid-wl-next-valid-use,
valid-wl-next-valid-update,
valid-wl-next-valid-erase,
valid-wl-next-invalid-erase,
valid-wl-next-free,
valid-wl-next-bad,
valid-wl-markbad,
valid-wl-map,
valid-wl-free-echdr,
valid-wl-free,
valid-wl-erasing-update-ec,
valid-wl-erasing-invalidate0,
valid-wl-erasing-invalidate,
valid-wl-erase,
valid-wl-ebatbl-used-imp-valid-ehdr,
valid-wl-ebatbl-used-imp-mapped,
valid-vtbl-wlar-status,
valid-vtbl-update-vols,
valid-vtbl-sqns-notempty,
valid-vtbl-buf,
valid-global-sqn-write-valid,
valid-global-sqn-not-ls,
valid-global-sqn-next-max,
valid-global-sqn-next,
valid-global-sqn-invalidate,
valid-global-sqn-inc,
valid-global-sqn-add-valid,
valid-eraseqw-use,
valid-eraseqw-update-ec,
valid-eraseqw-unmap,
valid-eraseqw-subarray-shift,
valid-eraseqw-free-in,
valid-eraseqp-valid-lebref,
valid-eraseqp-update-other,
valid-eraseqp-rem-middle,
valid-eraseqp-one,
valid-eraseqp-invalidate,
valid-eraseqp-in,
valid-eraseqp-append,
valid-eraseq-prev-erasing,
valid-eraseq-next-erasing,
valid-ebatbl-write-data,
valid-ebatbl-update-wlar-unused,
valid-ebatbl-update-vhdrs-unused,
valid-ebatbl-unmap,
valid-ebatbl-remap,
valid-ebatbl-move-vtbl,
valid-ebatbl-map,
valid-ebatbl-add-unmapped-vol,
unique-sqns-write-valid,
unique-sqns-update,
unique-sqns-2-valid-pebs,
mapped-pebs-unused,
mapped-pebs-unmap,
mapped-pebs-remap,
mapped-pebs-rem-notmapped,
mapped-pebs-at,
mapped-pebs-add-empty-vol,
is-vtbl-pnum,
in-valid-eraseqp-valid-lref,
idset-weaken,
idset-trans-intersect,
idset-mapped-pebs-write-unused,
idset-idexpt-fwd,
idset-idexpt,
datasize-alignup,
bitflips-cons-in,
bitflip-cons-set-used,
bitflip-cons-set,
bitflip-cons-del,
bitflip-cons-add,
bflipset-subarray-next,
bflipset-subarray-erase-old-add,
bflipset-subarray-erase-old,
bflipset-subarray-add,
- nat-basic/l-02
is used by
valid-wl-next-valid-update,
valid-global-sqn-inc,
- nat-basic/lf
is used by
valid-wl-use,
valid-wl-next-valid-use,
valid-wl-next-valid-update,
valid-wl-next-valid-erase,
valid-wl-next-invalid-erase,
valid-wl-next-free,
valid-wl-next-bad,
valid-global-sqn-next,
valid-eraseqw-subarray-shift,
valid-eraseq-prev-erasing,
valid-eraseq-next-erasing,
bflipset-subarray-next,
bflipset-subarray-erase-old-add,
bflipset-subarray-erase-old,
bflipset-subarray-add,
- nat-basic/lf-01
is used by
valid-wl-write-valid,
valid-wl-write-unmapped,
valid-wl-use,
valid-wl-next-valid-use,
valid-wl-next-valid-update,
valid-wl-next-valid-erase,
valid-wl-next-invalid-erase,
valid-wl-next-free,
valid-wl-next-bad,
valid-wl-markbad,
valid-wl-map,
valid-wl-erasing-invalidate0,
valid-wl-erasing-invalidate,
valid-wl-ebatbl-used-imp-mapped,
idset-weaken,
idset-trans-intersect,
idset-mapped-pebs-write-unused,
idset-idexpt-fwd,
idset-idexpt,
- nat-basic/lf-02
is used by
valid-wl-write-valid,
valid-wl-write-unmapped,
valid-wl-use,
valid-wl-next-valid-use,
valid-wl-next-valid-update,
valid-wl-next-valid-erase,
valid-wl-next-invalid-erase,
valid-wl-next-free,
valid-wl-next-bad,
valid-wl-markbad,
valid-wl-map,
valid-wl-erasing-invalidate0,
valid-wl-erasing-invalidate,
valid-wl-ebatbl-used-imp-valid-ehdr,
valid-eraseqp-valid-lebref,
valid-ebatbl-update-wlar-unused,
valid-ebatbl-update-vhdrs-unused,
valid-ebatbl-unmap,
valid-ebatbl-remap,
valid-ebatbl-move-vtbl,
valid-ebatbl-map,
valid-ebatbl-add-unmapped-vol,
mapped-pebs-unused,
mapped-pebs-unmap,
mapped-pebs-remap,
mapped-pebs-rem-notmapped,
in-valid-eraseqp-valid-lref,
idset-mapped-pebs-write-unused,
bitflip-cons-add,
- nat-basic/ls-02
is used by
valid-wl-write-valid,
valid-wl-write-unmapped,
valid-wl-use,
valid-wl-next-valid-use,
valid-wl-next-valid-update,
valid-wl-next-valid-erase,
valid-wl-next-invalid-erase,
valid-wl-next-free,
valid-wl-next-bad,
valid-wl-erasing-invalidate0,
valid-global-sqn-not-ls,
valid-global-sqn-next-max,
valid-global-sqn-next,
valid-eraseqw-subarray-shift,
valid-eraseq-prev-erasing,
valid-eraseq-next-erasing,
bflipset-subarray-next,
bflipset-subarray-erase-old-add,
bflipset-subarray-erase-old,
bflipset-subarray-add,
- nat-basic/s-04
is used by
valid-wl-next-valid-use,
valid-wl-next-valid-update,
valid-wl-next-valid-erase,
valid-wl-next-invalid-erase,
valid-wl-next-free,
valid-wl-next-bad,
valid-global-sqn-next-max,
valid-eraseqw-subarray-shift,
valid-eraseq-prev-erasing,
valid-eraseq-next-erasing,
bflipset-subarray-next,
bflipset-subarray-erase-old-add,
bflipset-subarray-erase-old,
bflipset-subarray-add,
- nat-basic/succ
is used by
valid-wl-use,
valid-wl-next-valid-use,
valid-wl-next-valid-update,
valid-wl-next-valid-erase,
valid-wl-next-invalid-erase,
valid-wl-next-free,
valid-wl-next-bad,
valid-eraseqw-subarray-shift,
valid-eraseq-prev-erasing,
valid-eraseq-next-erasing,
bflipset-subarray-next,
bflipset-subarray-erase-old-add,
bflipset-subarray-erase-old,
- nat-basic/zero-01
is used by
valid-wl-array-0,
valid-eraseq-array-0,
Used from specification aecheader
- aecheader/elim
is used by
valid-wl-use,
valid-wl-next-valid-use,
valid-wl-next-valid-update,
- aecheader/inj
is used by
valid-wl-write-unmapped,
valid-wl-next-free,
valid-wl-free-echdr,
valid-wl-free,
- aecheader/sel
is used by
valid-wl-used-echdr,
valid-wl-next-valid-use,
- aecheader/test-02
is used by
valid-wl-write-unmapped,
valid-wl-ebatbl-used-imp-valid-ehdr,
Used from specification erasequeue
- erasequeue/in-concat
is used by
valid-eraseqw-free,
valid-eraseqp-valid-lebref,
valid-eraseqd-rem-middle,
valid-eraseqd-nodups1,
- erasequeue/in-append
is used by
valid-eraseqw-unmap,
valid-eraseqd-append,
valid-eraseq-prev-erasing,
valid-eraseq-next-erasing,
- erasequeue/in-append-other
is used by
valid-eraseqw-unmap,
valid-eraseqd-append,
valid-eraseq-prev-erasing,
valid-eraseq-next-erasing,
- erasequeue/in-concat
is used by
valid-eraseqw-size-middle,
valid-eraseqw-free,
valid-eraseqp-update-other,
valid-eraseqp-in0,
valid-eraseqd-rem-middle,
valid-eraseqd-nodups1,
valid-eraseqd-nodups-middle2,
valid-eraseqd-nodups-middle1,
valid-eraseqd-nodups-middle0,
- erasequeue/in-empty
is used by
valid-eraseqp-valid-lebref,
valid-eraseqd-one,
valid-eraseqd-nodups1,
valid-eraseqd-nodups-middle0,
valid-eraseqd-append,
valid-eraseq-array-0,
- erasequeue/in-prepend
is used by
valid-eraseqw-size-middle,
valid-eraseqw-size-left,
valid-eraseqp-in0,
valid-eraseqd-nodups-middle2,
valid-eraseqd-nodups-middle1,
valid-eraseqd-nodups-middle0,
valid-eraseqd-append,
- erasequeue/in-prepend-other
is used by
valid-eraseqd-nodups-middle2,
valid-eraseqd-nodups-middle0,
valid-eraseqd-append,
- erasequeue/in-single
is used by
valid-eraseqw-free,
valid-eraseqp-valid-lebref,
valid-eraseqp-update-other,
valid-eraseqd-nodups1,
Used from specification bag-union
- bag-union/nat-bag/del-rec
is used by
valid-wl-write-unmapped,
valid-wl-use,
valid-wl-markbad,
valid-wl-erasing-invalidate0,
valid-wl-erasing-invalidate,
- bag-union/nat-bag/diff-empty
is used by
valid-wl-write-valid,
valid-wl-write-unmapped,
valid-wl-use,
valid-wl-markbad,
valid-wl-erasing-invalidate0,
valid-wl-erasing-invalidate,
valid-global-sqn-write-valid,
valid-global-sqn-invalidate,
valid-global-sqn-add-valid,
unique-sqns-write-valid,
unique-sqns-update,
- bag-union/nat-bag/diff-empty1
is used by
valid-global-sqn-add-valid,
- bag-union/nat-bag/in-at
is used by
valid-wl-next-valid-update,
- bag-union/nat-bag/subset-emp
is used by
valid-global-sqn-add-valid,
- bag-union/nat-bag/union-ass
is used by
valid-wl-write-valid,
valid-wl-write-unmapped,
valid-wl-use,
valid-wl-next-valid-use,
valid-wl-next-valid-update,
valid-wl-next-valid-erase,
valid-wl-next-free,
valid-wl-next-bad,
valid-wl-markbad,
valid-wl-erasing-invalidate0,
valid-wl-erasing-invalidate,
valid-global-sqn-write-valid,
valid-global-sqn-next-max,
valid-global-sqn-next,
valid-global-sqn-invalidate,
valid-global-sqn-add-valid,
unique-sqns-write-valid,
unique-sqns-update,
- bag-union/nat-bag/union-com
is used by
valid-wl-write-valid,
valid-wl-write-unmapped,
valid-wl-use,
valid-wl-next-valid-use,
valid-wl-next-valid-update,
valid-wl-next-valid-erase,
valid-wl-next-free,
valid-wl-next-bad,
valid-wl-markbad,
valid-wl-erasing-invalidate0,
valid-wl-erasing-invalidate,
valid-global-sqn-write-valid,
valid-global-sqn-next-max,
valid-global-sqn-next,
valid-global-sqn-invalidate,
valid-global-sqn-add-valid,
unique-sqns-write-valid,
unique-sqns-update,
- bag-union/nat-bag/union-diff-distr
is used by
valid-global-sqn-add-valid,
- bag-union/nat-bag/union-empty
is used by
valid-wl-write-valid,
valid-wl-write-unmapped,
valid-wl-use,
valid-wl-next-valid-use,
valid-wl-next-valid-update,
valid-wl-next-valid-erase,
valid-wl-next-free,
valid-wl-next-bad,
valid-wl-markbad,
valid-wl-erasing-invalidate0,
valid-wl-erasing-invalidate,
valid-global-sqn-write-valid,
valid-global-sqn-next-max,
valid-global-sqn-next,
valid-global-sqn-invalidate,
valid-global-sqn-add-valid,
unique-sqns-write-valid,
unique-sqns-update,
Used from specification avidheader
- avidheader/elim
is used by
valid-wl-ebatbl-used-imp-valid-ehdr,
valid-ebatbl-unmap,
valid-ebatbl-remap,
valid-ebatbl-map,
valid-ebatbl-add-unmapped-vol,
mapped-pebs-unmap,
mapped-pebs-remap,
- avidheader/inj
is used by
valid-wl-write-unmapped,
- avidheader/sel-06
is used by
valid-wl-ebatbl-used-imp-valid-ehdr,
valid-global-sqn-next-max,
valid-ebatbl-unmap,
valid-ebatbl-remap,
valid-ebatbl-map,
valid-ebatbl-add-unmapped-vol,
mapped-pebs-unmap,
mapped-pebs-remap,
- avidheader/sel-08
is used by
valid-wl-ebatbl-used-imp-valid-ehdr,
valid-global-sqn-next-max,
valid-ebatbl-unmap,
valid-ebatbl-remap,
valid-ebatbl-map,
valid-ebatbl-add-unmapped-vol,
mapped-pebs-unmap,
mapped-pebs-remap,
- avidheader/sel-10
is used by
valid-wl-write-unmapped,
valid-wl-use,
valid-wl-next-valid-update,
valid-wl-ebatbl-used-imp-valid-ehdr,
valid-global-sqn-next-max,
- avidheader/test-03
is used by
valid-wl-ebatbl-used-imp-valid-ehdr,
valid-ebatbl-unmap,
valid-ebatbl-remap,
valid-ebatbl-map,
valid-ebatbl-add-unmapped-vol,
mapped-pebs-unmap,
mapped-pebs-remap,
Used from specification set-union
- set-union/nat-set/Delete
is used by
mapped-pebs-unmap,
mapped-pebs-remap,
idset-weaken,
idset-idexpt-fwd,
bitflip-cons-del,
bflipset-subarray-erase-old-add,
bflipset-subarray-erase-old,
- set-union/nat-set/Intersect
is used by
idset-trans-intersect,
- set-union/nat-set/del-in-03
is used by
mapped-pebs-rem-notmapped,
- set-union/nat-set/int-a
is used by
idset-trans-intersect,
- set-union/nat-set/int-c
is used by
idset-trans-intersect,
Used from specification nat
- nat/fle
is used by
valid-wl-write-valid,
valid-wl-write-unmapped,
valid-wl-use,
valid-wl-markbad,
valid-wl-erasing-invalidate0,
valid-wl-erasing-invalidate,
valid-global-sqn-write-valid,
valid-global-sqn-next-max,
valid-global-sqn-next,
valid-global-sqn-invalidate,
valid-global-sqn-add-valid,
valid-ebatbl-remap,
datasize-alignup,
bitflip-cons-add,
- nat/fle-01
is used by
valid-wl-write-valid,
valid-wl-write-unmapped,
valid-wl-use,
valid-wl-next-valid-use,
valid-wl-next-valid-update,
valid-wl-next-valid-erase,
valid-wl-next-invalid-erase,
valid-wl-next-free,
valid-wl-next-bad,
valid-wl-markbad,
valid-wl-erasing-invalidate0,
valid-wl-erasing-invalidate,
valid-global-sqn-next-max,
valid-global-sqn-next,
valid-global-sqn-inc,
datasize-alignup,
- nat/ge
is used by
datasize-alignup,
- nat/gr-def
is used by
valid-wl-write-valid,
valid-wl-write-unmapped,
valid-wl-use,
valid-wl-next-valid-update,
valid-wl-next-valid-erase,
valid-wl-markbad,
valid-wl-map,
valid-wl-erasing-invalidate0,
valid-wl-erasing-invalidate,
valid-global-sqn-write-valid,
valid-global-sqn-notin,
valid-global-sqn-not-ls,
valid-global-sqn-not-leq,
valid-global-sqn-next-max,
valid-global-sqn-next,
valid-global-sqn-invalidate,
valid-global-sqn-inc,
valid-global-sqn-add-valid,
- nat/le-def
is used by
valid-wl-next-valid-use,
valid-wl-next-valid-update,
valid-wl-next-valid-erase,
valid-wl-next-invalid-erase,
valid-wl-next-free,
valid-wl-next-bad,
datasize-alignup,
- nat/le-ls-simp
is used by
valid-wl-next-valid-use,
valid-wl-next-valid-update,
valid-wl-next-valid-erase,
valid-wl-next-invalid-erase,
valid-wl-next-free,
valid-wl-next-bad,
valid-wl-markbad,
valid-wl-erasing-invalidate,
valid-global-sqn-write-valid,
valid-global-sqn-not-leq,
valid-global-sqn-next-max,
valid-global-sqn-next,
valid-global-sqn-invalidate,
valid-eraseqw-use,
valid-eraseqw-update-ec,
valid-eraseqw-size-middle,
valid-eraseqw-size-left,
valid-eraseqw-free,
valid-ebatbl-write-data,
valid-ebatbl-update-wlar-unused,
valid-ebatbl-update-vhdrs-unused,
valid-ebatbl-unmap,
valid-ebatbl-remap,
valid-ebatbl-move-vtbl,
valid-ebatbl-add-unmapped-vol,
datasize-alignup,
bitflip-cons-set-used,
bitflip-cons-add,
- nat/lels
is used by
valid-wl-write-valid,
valid-wl-write-unmapped,
valid-wl-use,
valid-wl-next-valid-use,
valid-wl-next-valid-update,
valid-wl-next-valid-erase,
valid-wl-next-invalid-erase,
valid-wl-next-free,
valid-wl-next-bad,
valid-wl-markbad,
valid-wl-map,
valid-wl-erasing-invalidate0,
valid-wl-erasing-invalidate,
valid-vtbl-sqns-notempty,
valid-global-sqn-write-valid,
valid-global-sqn-next-max,
valid-global-sqn-next,
valid-global-sqn-invalidate,
valid-global-sqn-inc,
valid-global-sqn-add-valid,
valid-eraseqw-use,
valid-eraseqw-update-ec,
valid-eraseqw-free,
valid-eraseqp-invalidate,
valid-eraseq-prev-erasing,
valid-ebatbl-write-data,
valid-ebatbl-update-wlar-unused,
valid-ebatbl-update-vhdrs-unused,
valid-ebatbl-unmap,
valid-ebatbl-remap,
valid-ebatbl-move-vtbl,
valid-ebatbl-add-unmapped-vol,
unique-sqns-write-valid,
bitflip-cons-set-used,
bitflip-cons-add,
- nat/lels-02
is used by
valid-wl-write-unmapped,
valid-wl-use,
valid-wl-next-valid-use,
valid-wl-next-valid-update,
valid-wl-next-valid-erase,
valid-wl-next-invalid-erase,
valid-wl-next-free,
valid-wl-next-bad,
valid-wl-erasing-invalidate0,
- nat/lels-03
is used by
valid-wl-next-valid-use,
valid-wl-next-valid-update,
valid-wl-next-valid-erase,
valid-global-sqn-next-max,
valid-global-sqn-next,
valid-eraseqw-subarray-shift,
valid-eraseq-prev-erasing,
valid-eraseq-next-erasing,
datasize-alignup,
bflipset-subarray-next,
bflipset-subarray-erase-old-add,
bflipset-subarray-erase-old,
bflipset-subarray-add,
- nat/ler
is used by
valid-wl-next-valid-use,
valid-wl-next-valid-update,
valid-wl-next-valid-erase,
valid-wl-next-invalid-erase,
valid-wl-next-free,
valid-wl-next-bad,
- nat/let
is used by
datasize-alignup,
- nat/ls-le-simp
is used by
valid-wl-write-valid,
valid-wl-write-unmapped,
valid-wl-use,
valid-wl-next-valid-update,
valid-wl-markbad,
valid-wl-map,
valid-wl-erasing-invalidate0,
valid-wl-erasing-invalidate,
valid-vtbl-sqns-notempty,
valid-global-sqn-write-valid,
valid-global-sqn-next-max,
valid-global-sqn-next,
valid-global-sqn-invalidate,
valid-global-sqn-add-valid,
valid-eraseqp-invalidate,
valid-eraseq-prev-erasing,
valid-ebatbl-remap,
valid-ebatbl-add-unmapped-vol,
unique-sqns-write-valid,
- nat/succ-01
is used by
valid-wl-next-valid-use,
valid-wl-next-valid-update,
valid-wl-next-valid-erase,
valid-wl-next-invalid-erase,
valid-wl-next-free,
valid-wl-next-bad,
valid-global-sqn-next-max,
valid-global-sqn-next,
valid-eraseqw-subarray-shift,
valid-eraseq-prev-erasing,
valid-eraseq-next-erasing,
bflipset-subarray-next,
bflipset-subarray-erase-old-add,
bflipset-subarray-erase-old,
bflipset-subarray-add,
Used from specification store
- store/volumes/At-other
is used by
mapped-pebs-unmap,
- store/vtbl/ins
is used by
valid-vtbl-update-vols,
- store/volumes/At-in-out
is used by
valid-ebatbl-add-unmapped-vol,
mapped-pebs-add-empty-vol,
- store/volumes/At-other
is used by
valid-ebatbl-unmap,
valid-ebatbl-remap,
valid-ebatbl-map,
valid-ebatbl-add-unmapped-vol,
mapped-pebs-unmap,
mapped-pebs-remap,
mapped-pebs-add-empty-vol,
- store/volumes/At-same
is used by
valid-ebatbl-unmap,
valid-ebatbl-remap,
valid-ebatbl-map,
valid-ebatbl-add-unmapped-vol,
mapped-pebs-unmap,
mapped-pebs-remap,
mapped-pebs-add-empty-vol,
- store/volumes/In-insert
is used by
valid-ebatbl-add-unmapped-vol,
mapped-pebs-unmap,
mapped-pebs-remap,
mapped-pebs-add-empty-vol,
- store/volumes/in-neq
is used by
valid-ebatbl-unmap,
valid-ebatbl-remap,
valid-ebatbl-map,
valid-ebatbl-add-unmapped-vol,
mapped-pebs-unmap,
mapped-pebs-remap,
mapped-pebs-add-empty-vol,
- store/volumes/ins-same-01
is used by
valid-ebatbl-map,
- store/volumes/insin
is used by
valid-ebatbl-unmap,
valid-ebatbl-remap,
valid-ebatbl-map,
valid-ebatbl-add-unmapped-vol,
mapped-pebs-unmap,
mapped-pebs-remap,
- store/volumes/notmemlookup
is used by
valid-ebatbl-add-unmapped-vol,
is-vtbl-pnum,
Used from specification bag-max
- bag-max/bag-rem-empty
is used by
valid-wl-write-valid,
- bag-max/max-rec
is used by
valid-wl-markbad,
valid-wl-erasing-invalidate,
valid-global-sqn-next-max,
valid-global-sqn-next,
valid-global-sqn-add-valid,
- bag-max/unique-elems-subset
is used by
valid-wl-next-valid-update,
- bag-max/bag-add-nonempty
is used by
valid-wl-write-unmapped,
valid-wl-use,
valid-wl-next-valid-use,
valid-wl-next-valid-update,
valid-wl-next-valid-erase,
valid-wl-markbad,
valid-wl-erasing-invalidate0,
valid-wl-erasing-invalidate,
valid-global-sqn-write-valid,
valid-global-sqn-next-max,
valid-global-sqn-next,
valid-global-sqn-add-valid,
- bag-max/bag-diff-one
is used by
valid-wl-write-valid,
valid-wl-write-unmapped,
valid-wl-use,
valid-wl-markbad,
valid-wl-erasing-invalidate0,
valid-wl-erasing-invalidate,
valid-global-sqn-write-valid,
valid-global-sqn-invalidate,
valid-global-sqn-add-valid,
unique-sqns-write-valid,
unique-sqns-update,
- bag-max/bag-empty-notin
is used by
valid-global-sqn-notin,
- bag-max/bag-rem-notmax
is used by
valid-wl-write-valid,
- bag-max/bag-remadd-in
is used by
valid-wl-write-valid,
valid-global-sqn-write-valid,
unique-sqns-write-valid,
- bag-max/bag-single-max
is used by
valid-global-sqn-add-valid,
- bag-max/bag-union-one
is used by
valid-wl-write-valid,
valid-wl-write-unmapped,
valid-wl-use,
valid-wl-next-valid-use,
valid-wl-next-valid-update,
valid-wl-next-valid-erase,
valid-global-sqn-write-valid,
valid-global-sqn-next-max,
valid-global-sqn-next,
valid-global-sqn-invalidate,
valid-global-sqn-add-valid,
unique-sqns-write-valid,
unique-sqns-update,
- bag-max/max-add-bigger
is used by
valid-wl-next-valid-update,
- bag-max/max-add-one-different
is used by
valid-wl-write-valid,
valid-wl-write-unmapped,
valid-wl-use,
valid-wl-next-valid-use,
valid-wl-next-valid-update,
valid-wl-markbad,
valid-wl-erasing-invalidate0,
valid-wl-erasing-invalidate,
- bag-max/max-add-smaller
is used by
valid-global-sqn-next-max,
valid-global-sqn-next,
valid-global-sqn-add-valid,
- bag-max/max-in-ls
is used by
valid-global-sqn-notin,
- bag-max/max-one
is used by
valid-wl-write-valid,
valid-wl-next-valid-use,
valid-wl-next-valid-erase,
valid-global-sqn-next-max,
valid-global-sqn-next,
- bag-max/max-rec-simp
is used by
valid-wl-write-valid,
valid-wl-write-unmapped,
valid-wl-use,
valid-wl-next-valid-erase,
valid-wl-markbad,
valid-wl-erasing-invalidate0,
valid-wl-erasing-invalidate,
valid-global-sqn-write-valid,
valid-global-sqn-add-valid,
- bag-max/max-rem-ls
is used by
valid-wl-write-valid,
valid-wl-use,
valid-global-sqn-invalidate,
valid-global-sqn-add-valid,
- bag-max/unique-elems-add
is used by
valid-wl-next-valid-update,
unique-sqns-write-valid,
unique-sqns-update,
- bag-max/unique-elems-addtwice
is used by
unique-sqns-2-valid-pebs,
- bag-max/unique-elems-rem
is used by
unique-sqns-update,
- bag-max/unique-elems-rem-notin
is used by
unique-sqns-update,
Used from specification set-basic
- set-basic/nat-set/Extension
is used by
mapped-pebs-unmap,
mapped-pebs-remap,
mapped-pebs-add-empty-vol,
- set-basic/nat-set/In-empty
is used by
bitflips-cons-empty,
- set-basic/nat-set/In-insert
is used by
mapped-pebs-remap,
bitflip-cons-add,
bflipset-subarray-erase-old-add,
bflipset-subarray-add,
- set-basic/nat-set/ne-01
is used by
idset-weaken,
idset-trans-intersect,
idset-idexpt-fwd,
idset-idexpt,
bitflips-cons-in,
bitflip-cons-set-used,
bitflip-cons-set,
bitflip-cons-del,
bflipset-subarray-next,
bflipset-subarray-erase-old-add,
bflipset-subarray-erase-old,
bflipset-subarray-add,
- set-basic/nat-set/size-zero-01
is used by
idset-weaken,
idset-trans-intersect,
idset-idexpt-fwd,
idset-idexpt,
bitflips-cons-in,
bitflip-cons-set-used,
bitflip-cons-set,
bitflip-cons-del,
bflipset-subarray-next,
bflipset-subarray-erase-old-add,
bflipset-subarray-erase-old,
bflipset-subarray-add,
Used from specification wlstatus
- wlstatus/disj-01
is used by
valid-wl-write-valid,
valid-wl-write-unmapped,
valid-wl-used-echdr,
valid-wl-use,
valid-wl-next-valid-use,
valid-wl-next-valid-update,
valid-wl-next-valid-erase,
valid-wl-next-invalid-erase,
valid-wl-next-free,
valid-wl-next-bad,
valid-wl-markbad,
valid-wl-map,
valid-wl-free-echdr,
valid-wl-free,
valid-wl-erasing-update-ec,
valid-wl-erasing-invalidate0,
valid-wl-erasing-invalidate,
valid-wl-erase,
valid-wl-ebatbl-used-imp-valid-ehdr,
valid-wl-ebatbl-used-imp-mapped,
valid-vtbl-sqns-notempty,
valid-ebatbl-move-vtbl,
valid-ebatbl-add-unmapped-vol,
- wlstatus/disj-02
is used by
valid-wl-write-valid,
valid-wl-write-unmapped,
valid-wl-used-echdr,
valid-wl-use,
valid-wl-next-valid-use,
valid-wl-next-valid-update,
valid-wl-next-valid-erase,
valid-wl-next-invalid-erase,
valid-wl-next-free,
valid-wl-next-bad,
valid-wl-markbad,
valid-wl-map,
valid-wl-free,
valid-wl-erasing-update-ec,
valid-wl-erasing-invalidate0,
valid-wl-erasing-invalidate,
valid-wl-erase,
valid-wl-ebatbl-used-imp-valid-ehdr,
valid-wl-ebatbl-used-imp-mapped,
valid-vtbl-sqns-notempty,
is-vtbl-pnum,
- wlstatus/disj-03
is used by
valid-wl-write-valid,
valid-wl-write-unmapped,
valid-wl-used-echdr,
valid-wl-use,
valid-wl-next-valid-use,
valid-wl-next-valid-update,
valid-wl-next-valid-erase,
valid-wl-next-invalid-erase,
valid-wl-next-free,
valid-wl-markbad,
valid-wl-map,
valid-wl-erasing-update-ec,
valid-wl-erasing-invalidate0,
valid-wl-erasing-invalidate,
valid-wl-erase,
valid-wl-ebatbl-used-imp-valid-ehdr,
valid-wl-ebatbl-used-imp-mapped,
valid-vtbl-sqns-notempty,
valid-eraseqw-use,
valid-eraseq-prev-erasing,
valid-ebatbl-unmap,
valid-ebatbl-remap,
valid-ebatbl-move-vtbl,
valid-ebatbl-add-unmapped-vol,
- wlstatus/disj-04
is used by
valid-wl-next-free,
valid-wl-next-bad,
valid-wl-markbad,
valid-wl-free-echdr,
valid-wl-free,
- wlstatus/disj-05
is used by
valid-wl-write-unmapped,
valid-wl-next-valid-update,
valid-wl-next-valid-erase,
valid-wl-next-invalid-erase,
valid-wl-next-free,
valid-wl-free-echdr,
valid-wl-free,
valid-wl-erasing-update-ec,
valid-wl-erasing-invalidate0,
valid-wl-erasing-invalidate,
valid-wl-erase,
valid-eraseqw-free-in,
- wlstatus/disj-06
is used by
valid-wl-write-unmapped,
valid-wl-next-valid-update,
valid-wl-next-valid-erase,
valid-wl-next-invalid-erase,
valid-wl-next-free,
valid-wl-erasing-update-ec,
valid-wl-erasing-invalidate0,
valid-wl-erasing-invalidate,
valid-wl-erase,
Used from specification valid-peb
- valid-peb/valid-peb0
is used by
valid-wl-use,
valid-global-sqn-next,
unique-sqns-update,
- valid-peb/valid-peb2
is used by
valid-wl-write-unmapped,
valid-wl-use,
valid-wl-next-valid-use,
valid-wl-next-valid-update,
- valid-peb/valid-peb-bad
is used by
valid-wl-next-valid-use,
valid-wl-next-valid-update,
valid-wl-next-valid-erase,
valid-wl-next-bad,
valid-wl-markbad,
- valid-peb/valid-peb-imp-valid-peb0
is used by
valid-wl-erasing-invalidate0,
valid-wl-erasing-invalidate,
valid-global-sqn-next,
valid-global-sqn-invalidate,
valid-eraseqp-valid-lebref,
unique-sqns-update,
in-valid-eraseqp-valid-lref,
- valid-peb/valid-peb-leb
is used by
valid-wl-write-valid,
valid-wl-write-unmapped,
valid-wl-use,
valid-wl-map,
valid-wl-ebatbl-used-imp-mapped,
valid-vtbl-sqns-notempty,
valid-global-sqn-write-valid,
valid-eraseqp-valid-lebref,
unique-sqns-write-valid,
unique-sqns-update,
is-vtbl-pnum,
in-valid-eraseqp-valid-lref,
- valid-peb/valid-peb-unique
is used by
valid-wl-write-valid,
valid-wl-write-unmapped,
valid-wl-use,
valid-wl-next-valid-use,
valid-wl-next-valid-update,
valid-wl-next-valid-erase,
valid-wl-next-invalid-erase,
valid-wl-next-free,
valid-wl-next-bad,
valid-wl-markbad,
valid-wl-free,
valid-wl-erasing-update-ec,
valid-wl-erasing-invalidate0,
valid-wl-erasing-invalidate,
valid-wl-erase,
valid-global-sqn-write-valid,
valid-global-sqn-next-max,
valid-global-sqn-next,
valid-global-sqn-invalidate,
valid-global-sqn-add-valid,
valid-eraseqp-valid-lebref,
unique-sqns-write-valid,
unique-sqns-update,
unique-sqns-2-valid-pebs,
in-valid-eraseqp-valid-lref,
- valid-peb/valid-peb-valid-vidhdr
is used by
valid-wl-write-unmapped,
valid-wl-map,
valid-wl-ebatbl-used-imp-mapped,
is-vtbl-pnum,
- valid-peb/valid-peb-vidhdr-empty
is used by
valid-wl-next-free,
valid-wl-free,
- valid-peb/valid-peb-vol
is used by
valid-wl-write-valid,
valid-wl-write-unmapped,
valid-wl-use,
valid-wl-map,
valid-wl-ebatbl-used-imp-mapped,
valid-vtbl-sqns-notempty,
valid-global-sqn-write-valid,
valid-eraseqp-valid-lebref,
unique-sqns-write-valid,
unique-sqns-update,
is-vtbl-pnum,
in-valid-eraseqp-valid-lref,
- valid-peb/valid-peb0-bad
is used by
valid-wl-write-valid,
valid-wl-write-unmapped,
valid-wl-use,
valid-wl-next-invalid-erase,
- valid-peb/valid-peb0-imp-valid-peb
is used by
valid-wl-write-valid,
valid-wl-write-unmapped,
valid-wl-use,
valid-global-sqn-write-valid,
valid-global-sqn-next-max,
valid-global-sqn-add-valid,
unique-sqns-write-valid,
Used from specification sqns
- sqns/valid-sqns-extract-sqn
is used by
valid-wl-write-valid,
- sqns/valid-sqns-extract-sqn-h
is used by
valid-wl-next-valid-use,
valid-wl-next-valid-erase,
- sqns/valid-sqns-extract2-sqn
is used by
valid-wl-write-unmapped,
valid-wl-use,
valid-wl-markbad,
valid-wl-erasing-invalidate0,
valid-wl-erasing-invalidate,
unique-sqns-2-valid-pebs,
- sqns/valid-sqns-extract2-sqn-h
is used by
valid-wl-next-valid-update,
- sqns/valid-sqns-subseteq
is used by
valid-wl-next-valid-update,
- sqns/valid-sqns-write
is used by
valid-wl-write-valid,
valid-wl-write-unmapped,
valid-wl-use,
valid-wl-markbad,
valid-wl-erasing-invalidate0,
valid-wl-erasing-invalidate,
valid-global-sqn-write-valid,
valid-global-sqn-invalidate,
valid-global-sqn-add-valid,
unique-sqns-write-valid,
unique-sqns-update,
- sqns/valid-peb-in-sqnums
is used by
valid-wl-write-valid,
valid-global-sqn-write-valid,
unique-sqns-write-valid,
- sqns/valid-peb-sqns-nonempty
is used by
valid-global-sqn-add-valid,
- sqns/valid-peb-sqns-nonempty0
is used by
valid-wl-write-valid,
valid-wl-use,
valid-wl-map,
valid-vtbl-sqns-notempty,
valid-global-sqn-write-valid,
valid-global-sqn-invalidate,
- sqns/valid-sqns-array-0
is used by
valid-global-sqn-array-0,
- sqns/valid-sqns-rec
is used by
valid-wl-next-valid-use,
valid-wl-next-valid-update,
valid-wl-next-valid-erase,
valid-wl-next-invalid-erase,
valid-wl-next-free,
valid-wl-next-bad,
valid-global-sqn-next-max,
valid-global-sqn-next,
- sqns/valid-sqns-subarray
is used by
valid-wl-next-valid-use,
valid-wl-next-valid-update,
valid-wl-next-valid-erase,
valid-wl-next-invalid-erase,
valid-wl-next-free,
valid-wl-next-bad,
valid-global-sqn-next-max,
valid-global-sqn-next,
Used from specification align
- erasequeueentry/elim
is used by
valid-eraseqp-valid-lebref,
valid-eraseqp-update-other,
valid-eraseqp-rem-middle,
valid-eraseqp-invalidate,
valid-eraseqp-append,
valid-eraseqd-rem-middle,
valid-eraseqd-nodups1,
valid-eraseqd-nodups-middle2,
valid-eraseqd-nodups-middle1,
valid-eraseqd-nodups-middle0,
valid-eraseqd-append,
in-valid-eraseqp-valid-lref,
- erasequeueentry/inj
is used by
valid-eraseqp-valid-lebref,
in-valid-eraseqp-valid-lref,
- erasequeueentry/sel-01
is used by
valid-eraseqp-one,
- erasequeueentry/sel-02
is used by
valid-eraseqp-one,
valid-eraseqd-one,
valid-eraseqd-nodups-middle2,
valid-eraseqd-nodups-middle1,
Used from specification list
- list/erasequeue-base/One
is used by
valid-eraseqp-one,
valid-eraseqd-one,
- list/erasequeue-base/c
is used by
valid-eraseqp-one,
valid-eraseqd-one,
- list/erasequeue-base/Nil
is used by
valid-eraseqp-rem-middle,
valid-eraseqp-append,
valid-eraseqd-rem-middle,
valid-eraseqd-nodups-middle2,
valid-eraseqd-nodups-middle1,
valid-eraseqd-append,
- list/erasequeue-base/a
is used by
valid-eraseqw-unmap,
valid-eraseqw-size-middle,
valid-eraseqw-size-left,
valid-eraseqw-free,
valid-eraseqp-valid-lebref,
valid-eraseqp-update-other,
valid-eraseqp-rem-middle,
valid-eraseqp-invalidate,
valid-eraseqp-in0,
valid-eraseqp-append,
valid-eraseqd-rem-middle,
valid-eraseqd-nodups1,
valid-eraseqd-nodups0,
valid-eraseqd-nodups-middle2,
valid-eraseqd-nodups-middle1,
valid-eraseqd-nodups-middle0,
valid-eraseqd-append,
valid-eraseq-prev-erasing,
valid-eraseq-next-erasing,
in-valid-eraseqp-valid-lref,
- list/erasequeue-base/c
is used by
valid-eraseqp-valid-lebref,
valid-eraseqp-update-other,
valid-eraseqp-rem-middle,
valid-eraseqp-invalidate,
valid-eraseqp-append,
valid-eraseqd-rem-middle,
valid-eraseqd-nodups1,
valid-eraseqd-nodups-middle2,
valid-eraseqd-nodups-middle1,
valid-eraseqd-nodups-middle0,
valid-eraseqd-append,
in-valid-eraseqp-valid-lref,
- list/erasequeue-base/in-06
is used by
valid-eraseqp-valid-lebref,
- list/erasequeue-base/in-empty
is used by
in-valid-eraseqp-valid-lref,
- list/erasequeue-base/in-rec
is used by
in-valid-eraseqp-valid-lref,
Used from specification wlentry
- wlentry/elim-02
is used by
valid-wl-write-valid,
valid-wl-write-unmapped,
valid-wl-use,
valid-wl-next-valid-use,
valid-wl-next-valid-update,
valid-wl-next-valid-erase,
valid-wl-next-invalid-erase,
valid-wl-next-free,
valid-wl-next-bad,
valid-wl-markbad,
valid-wl-map,
valid-wl-free,
valid-wl-erasing-update-ec,
valid-wl-erasing-invalidate0,
valid-wl-erasing-invalidate,
valid-wl-erase,
valid-wl-ebatbl-used-imp-valid-ehdr,
valid-wl-ebatbl-used-imp-mapped,
valid-vtbl-update-vols,
valid-vtbl-sqns-notempty,
valid-eraseqw-use,
valid-eraseqw-update-ec,
valid-eraseqw-unmap,
valid-eraseqw-subarray-shift,
valid-eraseqw-free,
valid-eraseqp-in0,
valid-eraseq-prev-erasing,
valid-eraseq-next-erasing,
valid-ebatbl-write-data,
valid-ebatbl-update-wlar-unused,
valid-ebatbl-update-vhdrs-unused,
valid-ebatbl-unmap,
valid-ebatbl-remap,
valid-ebatbl-move-vtbl,
valid-ebatbl-map,
valid-ebatbl-add-unmapped-vol,
mapped-pebs-unmap,
mapped-pebs-remap,
bitflip-cons-set-used,
bitflip-cons-set,
bitflip-cons-del,
bitflip-cons-add,
bflipset-subarray-next,
bflipset-subarray-erase-old-add,
bflipset-subarray-erase-old,
bflipset-subarray-add,
- wlentry/inj-03
is used by
valid-wl-write-valid,
valid-wl-write-unmapped,
valid-wl-use,
valid-wl-next-valid-use,
valid-wl-next-valid-update,
valid-wl-next-valid-erase,
valid-wl-next-invalid-erase,
valid-wl-next-free,
valid-wl-next-bad,
valid-wl-markbad,
valid-wl-map,
valid-wl-free,
valid-wl-erasing-update-ec,
valid-wl-erasing-invalidate0,
valid-wl-erasing-invalidate,
valid-wl-erase,
valid-eraseqw-use,
valid-eraseqw-update-ec,
valid-eraseqw-unmap,
valid-eraseqw-subarray-shift,
valid-eraseqw-free,
valid-eraseqp-in0,
valid-eraseq-prev-erasing,
valid-eraseq-next-erasing,
valid-ebatbl-update-wlar-unused,
valid-ebatbl-update-vhdrs-unused,
valid-ebatbl-unmap,
valid-ebatbl-remap,
valid-ebatbl-move-vtbl,
valid-ebatbl-map,
valid-ebatbl-add-unmapped-vol,
bitflip-cons-set-used,
bitflip-cons-set,
bitflip-cons-add,
bflipset-subarray-erase-old-add,
bflipset-subarray-erase-old,
bflipset-subarray-add,
- wlentry/sel-04
is used by
valid-wl-write-valid,
valid-wl-write-unmapped,
valid-wl-used-echdr,
valid-wl-use,
valid-wl-next-valid-use,
valid-wl-next-valid-erase,
valid-wl-next-invalid-erase,
valid-wl-next-free,
valid-wl-next-bad,
valid-wl-markbad,
valid-wl-map,
valid-wl-free-echdr,
valid-wl-free,
valid-wl-erasing-update-ec,
valid-wl-erasing-invalidate0,
valid-wl-erasing-invalidate,
valid-wl-erase,
valid-wl-ebatbl-used-imp-valid-ehdr,
valid-wl-ebatbl-used-imp-mapped,
valid-vtbl-wlar-status,
valid-vtbl-sqns-notempty,
valid-eraseqw-use,
valid-eraseqw-update-ec,
valid-eraseqw-unmap,
valid-eraseqw-subarray-shift,
valid-eraseqw-free-in,
valid-eraseqw-free,
valid-eraseqp-in,
valid-eraseq-prev-erasing,
valid-eraseq-next-erasing,
valid-ebatbl-write-data,
valid-ebatbl-update-wlar-unused,
valid-ebatbl-update-vhdrs-unused,
valid-ebatbl-unmap,
valid-ebatbl-remap,
valid-ebatbl-add-unmapped-vol,
mapped-pebs-unused,
mapped-pebs-unmap,
mapped-pebs-remap,
mapped-pebs-rem-notmapped,
is-vtbl-pnum,
idset-mapped-pebs-write-unused,
bitflips-cons-in,
bitflip-cons-set-used,
bitflip-cons-set,
bitflip-cons-del,
bitflip-cons-add,
bflipset-subarray-next,
bflipset-subarray-erase-old-add,
bflipset-subarray-erase-old,
bflipset-subarray-add,
- wlentry/sel-05
is used by
valid-wl-write-valid,
valid-wl-write-unmapped,
valid-wl-used-echdr,
valid-wl-use,
valid-wl-next-valid-use,
valid-wl-next-valid-erase,
valid-wl-next-invalid-erase,
valid-wl-next-free,
valid-wl-next-bad,
valid-wl-markbad,
valid-wl-map,
valid-wl-free-echdr,
valid-wl-free,
valid-wl-erasing-update-ec,
valid-wl-erasing-invalidate0,
valid-wl-erasing-invalidate,
valid-wl-erase,
valid-wl-ebatbl-used-imp-valid-ehdr,
valid-wl-ebatbl-used-imp-mapped,
valid-vtbl-sqns-notempty,
Used from specification array-copy
- array-copy/apebs/Idexcept
is used by
idset-mapped-pebs-write-unused,
idset-idexpt-fwd,
idset-idexpt,
- array-copy/ebatbl/at-fill-mkarray
is used by
valid-ebatbl-add-unmapped-vol,
mapped-pebs-add-empty-vol,
- array-copy/apebs/idexcept-size
is used by
idset-mapped-pebs-write-unused,
idset-idexpt-fwd,
idset-idexpt,
- array-copy/ebatbl/size-fill
is used by
valid-ebatbl-add-unmapped-vol,
mapped-pebs-add-empty-vol,
- array-copy/wlarray-base/size-subarray
is used by
valid-wl-next-valid-use,
valid-wl-next-valid-update,
valid-wl-next-valid-erase,
valid-wl-next-invalid-erase,
valid-wl-next-free,
valid-wl-next-bad,
valid-eraseqw-subarray-shift,
valid-eraseq-prev-erasing,
valid-eraseq-next-erasing,
bflipset-subarray-next,
bflipset-subarray-erase-old-add,
bflipset-subarray-erase-old,
bflipset-subarray-add,
- array-copy/wlarray-base/subarray-at
is used by
valid-wl-next-valid-use,
valid-wl-next-valid-update,
valid-wl-next-valid-erase,
valid-wl-next-invalid-erase,
valid-wl-next-free,
valid-wl-next-bad,
ls-at-subarray-wlar,
- array-copy/apebs/subarray-at
is used by
valid-wl-next-valid-use,
valid-wl-next-valid-update,
valid-wl-next-valid-erase,
valid-wl-next-invalid-erase,
valid-wl-next-free,
valid-wl-next-bad,
ls-at-subarray-pebs,
Used from specification datasize
Used from specification eraseblock
Used from specification oelem
- oelem/nat-set/irreflexivity
is used by
valid-wl-write-valid,
valid-wl-write-unmapped,
valid-wl-use,
valid-wl-next-valid-use,
valid-wl-next-valid-update,
valid-wl-next-invalid-erase,
valid-wl-next-bad,
valid-wl-markbad,
valid-wl-erasing-invalidate0,
valid-wl-erasing-invalidate,
valid-global-sqn-write-valid,
valid-global-sqn-next-max,
valid-global-sqn-next,
valid-global-sqn-add-valid,
valid-eraseqw-subarray-shift,
valid-eraseqw-free-in,
valid-eraseqp-in,
valid-eraseq-prev-erasing,
valid-eraseq-next-erasing,
bflipset-subarray-next,
bflipset-subarray-erase-old-add,
bflipset-subarray-erase-old,
bflipset-subarray-add,
- oelem/nat-set/ls-le
is used by
valid-eraseq-prev-erasing,
- oelem/nat-set/sls
is used by
valid-wl-write-valid,
valid-eraseqw-subarray-shift,
valid-eraseq-prev-erasing,
valid-eraseq-next-erasing,
bflipset-subarray-next,
- oelem/nat-set/transitivity
is used by
valid-wl-use,
valid-wl-next-valid-use,
valid-wl-next-valid-update,
valid-wl-next-valid-erase,
valid-wl-next-invalid-erase,
valid-wl-next-free,
valid-wl-next-bad,
valid-global-sqn-next,
valid-eraseqw-subarray-shift,
valid-eraseq-prev-erasing,
valid-eraseq-next-erasing,
bflipset-subarray-next,
bflipset-subarray-erase-old-add,
bflipset-subarray-erase-old,
bflipset-subarray-add,
Used from specification vtbl-conv
Used from specification array
- array/apebs/Put-other
is used by
valid-eraseqp-invalidate,
- array/ebatbl/Put-other
is used by
mapped-pebs-unmap,
- array/apebs/Put-other
is used by
valid-wl-write-valid,
valid-wl-write-unmapped,
valid-wl-use,
valid-wl-markbad,
valid-wl-erasing-invalidate0,
valid-wl-erasing-invalidate,
valid-vtbl-update-other-pebs,
valid-eraseqp-invalidate,
valid-ebatbl-write-data,
valid-ebatbl-update-vhdrs-unused,
valid-ebatbl-move-vtbl,
valid-ebatbl-add-unmapped-vol,
- array/wlarray-base/Put-other
is used by
valid-wl-use,
valid-wl-next-valid-use,
valid-wl-next-valid-update,
valid-wl-next-valid-erase,
valid-wl-next-invalid-erase,
valid-wl-next-free,
valid-wl-next-bad,
valid-wl-markbad,
valid-wl-free,
valid-wl-erasing-update-ec,
valid-wl-erasing-invalidate0,
valid-wl-erase,
valid-vtbl-update-other-wlar,
valid-eraseqw-use,
valid-eraseqw-update-ec,
valid-eraseqw-unmap,
valid-eraseqw-subarray-shift,
valid-eraseqw-free,
valid-eraseq-prev-erasing,
valid-eraseq-next-erasing,
valid-ebatbl-update-wlar-unused,
valid-ebatbl-unmap,
valid-ebatbl-remap,
valid-ebatbl-move-vtbl,
valid-ebatbl-map,
valid-ebatbl-add-unmapped-vol,
bitflip-cons-set-used,
bitflip-cons-set,
bflipset-subarray-next,
bflipset-subarray-erase-old-add,
bflipset-subarray-erase-old,
bflipset-subarray-add,
- array/ebatbl/Put-other
is used by
valid-ebatbl-unmap,
valid-ebatbl-remap,
valid-ebatbl-map,
mapped-pebs-unmap,
mapped-pebs-remap,
- array/wlarray-base/Put-same
is used by
valid-wl-use,
valid-wl-next-valid-use,
valid-wl-next-valid-update,
valid-wl-next-valid-erase,
valid-wl-next-invalid-erase,
valid-wl-next-free,
valid-wl-next-bad,
valid-wl-markbad,
valid-wl-map,
valid-wl-free,
valid-wl-erasing-update-ec,
valid-wl-erasing-invalidate0,
valid-wl-erase,
valid-eraseqw-use,
valid-eraseqw-update-ec,
valid-eraseqw-unmap,
valid-eraseqw-subarray-shift,
valid-eraseqw-free,
valid-eraseq-prev-erasing,
valid-eraseq-next-erasing,
valid-ebatbl-update-wlar-unused,
valid-ebatbl-unmap,
valid-ebatbl-remap,
valid-ebatbl-map,
valid-ebatbl-add-unmapped-vol,
bitflip-cons-set-used,
bitflip-cons-set,
bflipset-subarray-next,
bflipset-subarray-erase-old-add,
bflipset-subarray-erase-old,
bflipset-subarray-add,
- array/apebs/Put-same
is used by
valid-wl-markbad,
valid-wl-erasing-invalidate0,
valid-wl-erasing-invalidate,
valid-eraseqp-update-other,
valid-eraseqp-invalidate,
valid-ebatbl-write-data,
valid-ebatbl-update-vhdrs-unused,
- array/ebatbl/Put-same
is used by
valid-ebatbl-unmap,
valid-ebatbl-remap,
valid-ebatbl-map,
mapped-pebs-unmap,
mapped-pebs-remap,
- array/wlarray-base/Size-mkarray
is used by
valid-wl-array-0,
valid-eraseq-array-0,
- array/ebatbl/Size-mkarray
is used by
valid-ebatbl-add-unmapped-vol,
mapped-pebs-add-empty-vol,
- array/wlarray-base/Size-put
is used by
valid-wl-use,
valid-wl-next-valid-use,
valid-wl-next-valid-update,
valid-wl-next-valid-erase,
valid-wl-next-invalid-erase,
valid-wl-next-free,
valid-wl-next-bad,
valid-wl-markbad,
valid-wl-map,
valid-wl-free,
valid-wl-erasing-update-ec,
valid-wl-erasing-invalidate0,
valid-wl-erase,
valid-vtbl-update-other-wlar,
valid-eraseqw-use,
valid-eraseqw-update-ec,
valid-eraseqw-unmap,
valid-eraseqw-subarray-shift,
valid-eraseqw-free,
valid-eraseq-prev-erasing,
valid-eraseq-next-erasing,
valid-ebatbl-update-wlar-unused,
valid-ebatbl-unmap,
valid-ebatbl-remap,
valid-ebatbl-move-vtbl,
valid-ebatbl-map,
valid-ebatbl-add-unmapped-vol,
bitflip-cons-set-used,
bitflip-cons-set,
bflipset-subarray-next,
bflipset-subarray-erase-old-add,
bflipset-subarray-erase-old,
bflipset-subarray-add,
- array/apebs/Size-put
is used by
valid-vtbl-update-other-pebs,
valid-eraseqp-update-other,
valid-eraseqp-invalidate,
valid-ebatbl-write-data,
valid-ebatbl-update-vhdrs-unused,
valid-ebatbl-move-vtbl,
valid-ebatbl-add-unmapped-vol,
idset-write-notin,
- array/ebatbl/Size-put
is used by
valid-vtbl-update-vols,
valid-ebatbl-unmap,
valid-ebatbl-remap,
valid-ebatbl-map,
mapped-pebs-unmap,
mapped-pebs-remap,
- array/apebs/cgetput
is used by
valid-wl-write-valid,
valid-wl-write-unmapped,
valid-wl-use,
valid-wl-markbad,
valid-wl-erasing-invalidate0,
valid-wl-erasing-invalidate,
valid-ebatbl-write-data,
valid-ebatbl-update-vhdrs-unused,
- array/ebatbl/cgetput
is used by
valid-ebatbl-remap,
- array/wlarray-base/cgetput
is used by
valid-wl-next-valid-update,
valid-eraseqw-use,
valid-eraseqw-update-ec,
valid-eraseqw-free,
valid-eraseq-prev-erasing,
valid-ebatbl-update-wlar-unused,
valid-ebatbl-move-vtbl,
valid-ebatbl-add-unmapped-vol,
- array/wlarray-base/cngetput
is used by
valid-wl-next-valid-erase,
valid-wl-next-invalid-erase,
valid-wl-next-free,
valid-wl-next-bad,
valid-wl-markbad,
valid-wl-free,
valid-wl-erasing-update-ec,
valid-wl-erasing-invalidate0,
valid-wl-erase,
bitflip-cons-set,
- array/apebs/cngetput
is used by
valid-wl-write-unmapped,
valid-wl-use,
valid-wl-markbad,
valid-wl-map,
valid-wl-erasing-invalidate0,
valid-wl-erasing-invalidate,
valid-eraseqp-update-other,
idset-write-notin,
- array/apebs/ngp-07
is used by
valid-wl-write-valid,
- array/ebatbl/put-same-content
is used by
valid-ebatbl-map,
Used from specification ebaentry
- ebaentry/disj
is used by
valid-wl-write-unmapped,
valid-wl-map,
valid-ebatbl-unmap,
valid-ebatbl-map,
valid-ebatbl-add-unmapped-vol,
mapped-pebs-unmap,
mapped-pebs-add-empty-vol,
- ebaentry/inj
is used by
valid-ebatbl-unmap,
valid-ebatbl-remap,
valid-ebatbl-map,
mapped-pebs-unmap,
mapped-pebs-remap,
Used from specification min-max