[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 absexpt-vols-write, absexpt-vols-abs, absexpt-v-vols-write, absexpt-pebs-write, absexpt-mapped-abs, absexpt-idset, absexpt-id-apebs-used, absexpt-avols-write, abs-unmap-twice, abs-unmap, abs-queue-subset, abs-queue-notin, abs-lebrefs-subset-noterased-some, abs-lebrefs-subset, abs-idset-fwd, abs-id-apebs-used, abs-erase-emptyq, abs-erase, abs-absexpt-v, abs-absexpt,
apeb/inj is used by absexpt-pebs-write, absexpt-mapped-abs, absexpt-idset, absexpt-id-apebs-used, abs-unmap, abs-idset-fwd, abs-id-apebs-used, abs-erase,
apeb/sel-05 is used by absexpt-pebs-write, absexpt-idset,
apeb/sel-06 is used by absexpt-vols-write, absexpt-vols-abs, absexpt-v-vols-write, absexpt-mapped-abs, absexpt-avols-write, abs-unmap-twice, abs-queue-subset, abs-queue-notin, abs-lebrefs-subset-noterased-some, abs-lebrefs-subset, abs-erase-emptyq, abs-absexpt-v, abs-absexpt,
apeb/sel-07 is used by absexpt-vols-write, absexpt-vols-abs, absexpt-v-vols-write, absexpt-mapped-abs, absexpt-avols-write, abs-unmap-twice, abs-queue-subset, abs-queue-notin, abs-lebrefs-subset-noterased-some, abs-lebrefs-subset, abs-erase-emptyq, abs-absexpt-v, abs-absexpt,

Used from specification lebref

lebref/disj is used by absf-size, absf-at, abs-lebrefs-subset-noterased-some, abs-lebrefs-subset,
lebref/inj is used by abs-unmap, abs-queue-notin, abs-lebrefs-subset-noterased-some,

Used from specification nat-basic

nat-basic/a is used by absf-size, absf-at,
nat-basic/c is used by absf-size, absf-at,
nat-basic/f is used by absf-size, absf-at, absexpt-vols-write, absexpt-vols-abs, absexpt-v-vols-write, absexpt-pebs-write, absexpt-mapped-abs, absexpt-idset, absexpt-id-apebs-used, absexpt-avols-write, abs-vols-unmapped, abs-vols-size, abs-vols-mapped, abs-unmap-twice, abs-unmap, abs-queue-subset, abs-queue-notin, abs-lebrefs-subset-noterased-some, abs-lebrefs-subset, abs-idset-fwd, abs-id-apebs-used, abs-erase-emptyq, abs-erase, abs-avols-size, abs-absexpt-v, abs-absexpt,
nat-basic/lf is used by absf-at, abs-vols-size, abs-avols-size,
nat-basic/lf-01 is used by absexpt-vols-write, absexpt-vols-abs, absexpt-v-vols-write, absexpt-pebs-write, absexpt-mapped-abs, absexpt-idset, absexpt-id-apebs-used, absexpt-avols-write, abs-vols-unmapped, abs-vols-size, abs-vols-mapped, abs-unmap-twice, abs-unmap, abs-queue-subset, abs-queue-notin, abs-lebrefs-subset-noterased-some, abs-lebrefs-subset, abs-idset-fwd, abs-id-apebs-used, abs-erase-emptyq, abs-erase, abs-avols-size, abs-absexpt-v, abs-absexpt,
nat-basic/lf-02 is used by absexpt-pebs-write, absexpt-mapped-abs, absexpt-idset, abs-vols-size,
nat-basic/s-04 is used by absf-at,
nat-basic/succ is used by absf-size, absf-at, abs-vols-size, abs-avols-size,
nat-basic/zero-01 is used by absf-at,

Used from specification erasequeue

erasequeue/in-empty-vl is used by abs-erase-emptyq,
erasequeue/in-rm-v-in is used by absexpt-vols-abs,
erasequeue/in-rm-v-same is used by absexpt-vols-abs,
erasequeue/in-vl-append is used by abs-unmap, abs-queue-notin,
erasequeue/in-vl-append0 is used by abs-queue-notin,
erasequeue/in-vl-in-lebrefs is used by absf-size, absf-at, abs-lebrefs-subset-noterased-some, abs-lebrefs-subset,
erasequeue/in-vl-subset is used by abs-queue-subset,
erasequeue/rm-vl-notin is used by abs-erase,
erasequeue/rm-vl-notin-before is used by abs-erase,

Used from specification avidheader

avidheader/elim is used by absexpt-pebs-write, absexpt-idset,
avidheader/sel-06 is used by absexpt-pebs-write, absexpt-idset,
avidheader/sel-08 is used by absexpt-pebs-write, absexpt-idset,
avidheader/test-03 is used by absexpt-pebs-write, absexpt-idset,

Used from specification set-union

set-union/lebrefset/subdef is used by abs-lebrefs-subset-noterased-some, abs-lebrefs-subset,
set-union/nat-set/Delete is used by absexpt-idset,

Used from specification nat

nat/fle is used by absf-at, absexpt-idset, abs-vols-size, abs-idset-fwd, abs-avols-size,
nat/fle-01 is used by absf-at, absexpt-idset, abs-vols-size, abs-idset-fwd, abs-avols-size,
nat/le-ls-simp is used by absexpt-pebs-write, absexpt-idset, abs-idset-fwd,
nat/lels is used by absf-at, absexpt-pebs-write, absexpt-idset, abs-vols-size, abs-unmap, abs-idset-fwd, abs-erase-emptyq, abs-erase, abs-avols-size,
nat/lels-02 is used by absf-at,
nat/lels-03 is used by absf-size, absf-at,
nat/ler is used by absf-at,
nat/lez is used by absf-at,
nat/ls-le-simp is used by absf-at, abs-unmap, abs-erase-emptyq, abs-erase,
nat/succ-01 is used by absf-size, absf-at,

Used from specification store

store/volumes/At-in-out is used by absexpt-vols-abs, absexpt-v-vols-write,
store/abstract-volumes/At-in-out is used by absexpt-v-vols-write,
store/volumes/At-other is used by absexpt-vols-write, absexpt-vols-abs, absexpt-v-vols-write, abs-unmap, abs-erase-emptyq, abs-erase,
store/abstract-volumes/At-other is used by absexpt-vols-abs, absexpt-v-vols-write, absexpt-avols-write, abs-unmap-twice, abs-unmap, abs-erase-emptyq, abs-erase,
store/volumes/At-same is used by absexpt-vols-write, absexpt-vols-abs, absexpt-v-vols-write, abs-unmap, abs-erase-emptyq, abs-erase,
store/abstract-volumes/At-same is used by absexpt-vols-abs, absexpt-v-vols-write, absexpt-avols-write, abs-unmap-twice, abs-unmap, abs-erase-emptyq, abs-erase,
store/volumes/In-insert is used by absexpt-vols-abs, absexpt-v-vols-write, abs-unmap, abs-erase-emptyq, abs-erase,
store/abstract-volumes/In-insert is used by absexpt-vols-abs, absexpt-v-vols-write, abs-unmap-twice, abs-unmap, abs-erase-emptyq, abs-erase,
store/volumes/in-neq is used by absexpt-vols-write, absexpt-vols-abs, absexpt-v-vols-write, abs-unmap, abs-erase-emptyq, abs-erase,
store/abstract-volumes/in-neq is used by absexpt-vols-abs, absexpt-v-vols-write, absexpt-avols-write, abs-unmap-twice, abs-unmap, abs-erase-emptyq, abs-erase,
store/volumes/insin is used by absexpt-vols-write, absexpt-vols-abs, absexpt-v-vols-write, abs-unmap, abs-erase-emptyq, abs-erase,
store/abstract-volumes/insin is used by absexpt-vols-abs, absexpt-v-vols-write, absexpt-avols-write, abs-unmap-twice, abs-unmap, abs-erase-emptyq, abs-erase,
store/abstract-volumes/notmemlookup is used by abs-unmap-twice,
store/volumes/notmemlookup is used by absexpt-v-vols-write, abs-unmap-twice, abs-erase-emptyq,

Used from specification set-basic

set-basic/lebrefset/In-insert is used by abs-lebrefs-subset-noterased-some,

Used from specification leb

leb/disj is used by absexpt-pebs-write, absexpt-mapped-abs, absexpt-idset, absexpt-id-apebs-used, abs-idset-fwd, abs-id-apebs-used,
leb/disj-02 is used by abs-unmap-twice, abs-unmap,
leb/elim is used by absexpt-pebs-write, absexpt-idset, absexpt-id-apebs-used, abs-idset-fwd, abs-id-apebs-used,
leb/sel is used by absexpt-mapped-abs,
leb/sel-01 is used by absexpt-mapped-abs,
leb/test-01 is used by abs-unmap-twice, abs-unmap,
leb/test-02 is used by absexpt-vols-abs, abs-lebrefs-subset-noterased-some, abs-lebrefs-subset, abs-erase-emptyq, abs-erase,
leb/test-03 is used by absexpt-pebs-write, absexpt-mapped-abs, absexpt-idset, absexpt-id-apebs-used, abs-idset-fwd, abs-id-apebs-used,

Used from specification wlentry

wlentry/elim-02 is used by absexpt-pebs-write, absexpt-idset,
wlentry/sel-04 is used by absexpt-pebs-write, absexpt-idset, absexpt-id-apebs-used, abs-id-apebs-used,

Used from specification list

list/erasequeue-base/a is used by abs-unmap, abs-queue-notin,

Used from specification array-copy

array-copy/abstract-volume/at-fill-mkarray is used by absexpt-vols-abs,
array-copy/ebatbl/at-fill-mkarray is used by absexpt-vols-abs,
array-copy/ebatbl/size-fill is used by absexpt-vols-abs,
array-copy/abstract-volume/size-fill is used by absexpt-vols-abs,

Used from specification oelem

oelem/nat-set/irreflexivity is used by absexpt-idset, abs-vols-size, abs-idset-fwd, abs-avols-size,
oelem/nat-set/transitivity is used by abs-vols-size, abs-avols-size,

Used from specification array

array/apebs/Put-other is used by absexpt-pebs-write, absexpt-id-apebs-used, abs-id-apebs-used,
array/ebatbl/Put-other is used by absexpt-vols-write, abs-unmap, abs-erase-emptyq, abs-erase,
array/abstract-volume/Put-other is used by absf-at, absexpt-avols-write, abs-unmap-twice, abs-unmap, abs-erase-emptyq, abs-erase,
array/ebatbl/Put-same is used by absexpt-vols-write, abs-unmap, abs-erase-emptyq, abs-erase,
array/apebs/Put-same is used by absexpt-id-apebs-used, abs-id-apebs-used,
array/abstract-volume/Put-same is used by absf-at, abs-unmap-twice, abs-unmap, abs-erase-emptyq, abs-erase,
array/abstract-volume/Size-mkarray is used by absf-size, absexpt-vols-abs,
array/ebatbl/Size-mkarray is used by absexpt-vols-abs,
array/abstract-volume/Size-put is used by absf-size, absexpt-avols-write, abs-unmap-twice, abs-unmap, abs-erase-emptyq, abs-erase,
array/ebatbl/Size-put is used by absexpt-vols-write, abs-unmap, abs-erase-emptyq, abs-erase,
array/apebs/cgetput is used by absexpt-pebs-write,
array/ebatbl/cgetput is used by abs-unmap, abs-erase-emptyq, abs-erase,
array/abstract-volume/cngetput is used by abs-unmap-twice, abs-unmap, abs-erase-emptyq, abs-erase,
array/ebatbl/cngetput is used by abs-unmap, abs-erase-emptyq, abs-erase,

Used from specification ebaentry

ebaentry/disj is used by absexpt-pebs-write, absexpt-mapped-abs, absexpt-idset, absexpt-id-apebs-used, abs-vols-mapped, abs-idset-fwd, abs-id-apebs-used,
ebaentry/elim is used by absexpt-pebs-write, absexpt-idset, absexpt-id-apebs-used, abs-idset-fwd, abs-id-apebs-used,
ebaentry/sel is used by absexpt-mapped-abs,

Used from specification ubi-base

ubi-base/id-set is used by absexpt-idset, abs-idset-fwd,
ubi-base/mapped-pebs is used by abs-idset-fwd,
ubi-base/mapped-pebs-at is used by absexpt-idset,
ubi-base/valid-ebatbl is used by absexpt-pebs-write, absexpt-idset, absexpt-id-apebs-used, abs-idset-fwd, abs-id-apebs-used,