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

lebref/disj is used by vols-is-max-is-min-eraseq, valid-eraseq-stronger-prev-append-lref, valid-eraseq-stronger-one, valid-eraseq-stronger-next-append-lref,
lebref/elim is used by valid-eraseq-stronger-one,
lebref/inj is used by valid-eraseq-strong-notinvols,
lebref/sel-01 is used by valid-eraseq-stronger-prev-append-lref, valid-eraseq-stronger-one, valid-eraseq-stronger-next-append-lref,
lebref/sel-02 is used by valid-eraseq-stronger-prev-append-lref, valid-eraseq-stronger-one, valid-eraseq-stronger-next-append-lref,

Used from specification recovery-entry

recovery-entry/elim is used by valid-recs-sqns-update, valid-recs-next-update, valid-recs-next-samerecs, valid-recs-next-add, valid-recs-in-nonempty-sqns,
recovery-entry/inj is used by valid-recs-sqns-update, valid-recs-next-update, valid-recs-next-add,
recovery-entry/sel-01 is used by valid-recs-sqns-update,
recovery-entry/sel-02 is used by valid-recs-sqns-update, valid-recs-next-update, valid-recs-next-samerecs,

Used from specification apeb

Used from specification nat-basic

Used from specification aecheader

aecheader/inj is used by vols-is-max-is-min-eraseq, vols-is-max-is-max-vols,
aecheader/test-02 is used by vols-is-max-is-max-vols,

Used from specification erasequeue

erasequeue/in-append is used by valid-eraseq-stronger-next-append-none, valid-eraseq-stronger-next-append-lref,
erasequeue/in-concat is used by in-eraseq-strong-not-valid,
erasequeue/in-prepend is used by valid-eraseq-stronger-no-maxsqnum,
erasequeue/queue-in is used by vols-is-max-is-min-eraseq, indices-erasing-eraseq,
erasequeue/queue-in-vl is used by vols-is-max-is-min-eraseq,
erasequeue/in-append-other is used by valid-eraseq-stronger-prev-append-lref, valid-eraseq-strong-notinvols,
erasequeue/in-concat is used by valid-eraseq-stronger-prev-append-lref, valid-eraseq-strong-notinvols,
erasequeue/in-empty is used by valid-eraseq-stronger-prev-append-lref, valid-eraseq-stronger-one, valid-eraseq-stronger-no-maxsqnum, valid-eraseq-strong-notinvols, in-eraseq-strong-not-valid,
erasequeue/in-single is used by valid-eraseq-stronger-prev-append-lref, valid-eraseq-strong-notinvols, in-eraseq-strong-not-valid,
erasequeue/in-vl-in-lebrefs is used by vols-is-max-is-min-eraseq,

Used from specification bag-union

Used from specification avidheader

avidheader/disj-02 is used by vols-is-max-is-min-eraseq, vols-is-max-is-max-vols,
avidheader/elim is used by vols-is-max-is-min-eraseq, vols-is-max-is-max-vols,
avidheader/inj is used by vols-is-max-is-max-vols,
avidheader/sel-06 is used by vols-is-max-is-max-vols, valid-recs-next-update, valid-recs-next-add,
avidheader/sel-08 is used by vols-is-max-is-max-vols, valid-recs-next-update, valid-recs-next-add,
avidheader/sel-10 is used by vols-is-max-is-max-vols,
avidheader/test-03 is used by vols-is-max-is-min-eraseq, vols-is-max-is-max-vols,

Used from specification nat

Used from specification store

store/recovery-entries/At-other is used by valid-recs-next-update,
store/volumes/Extension is used by vols-le-antisym,
store/vtbl/Extension is used by vols-is-max-is-max-vols,
store/recovery-entries/In-insert is used by valid-recs-next-add,
store/recovery-entries/At-in-out is used by valid-recs-next-add,
store/recovery-entries/At-other is used by valid-recs-sqns-update, valid-recs-next-update,
store/volumes/At-other is used by disj-shift,
store/volumes/At-same is used by disj-shift,
store/recovery-entries/At-same is used by valid-recs-sqns-update, valid-recs-next-update, valid-recs-next-add,
store/recovery-entries/Del-in is used by disj-shift, disj-remove,
store/recovery-entries/In-empty is used by valid-recs-sqns-emptyset, valid-recs-emptyset,
store/recovery-entries/in-neq is used by valid-recs-sqns-update, valid-recs-next-update,
store/volumes/in-neq is used by disj-shift,
store/volumes/insin is used by disj-shift,
store/recovery-entries/insin is used by valid-recs-sqns-update, valid-recs-next-update, valid-recs-next-add,
store/recovery-entries/k-At-same is used by valid-recs-next-add,
store/volumes/notmemlookup is used by vols-le-antisym, vols-is-max-is-min-eraseq,
store/recovery-entries/notmemlookup is used by valid-recs-next-add,

Used from specification bag-max

bag-max/max-rec is used by vols-is-max-is-min-eraseq, valid-eraseq-stronger-prev-append-lref, valid-eraseq-stronger-next,
bag-max/bag-add-nonempty is used by vols-is-max-is-min-eraseq, valid-eraseq-stronger-prev-append-lref, valid-eraseq-stronger-next, ubi-io-initial-valid-sqns-h, ubi-cons-same-vtbl,
bag-max/bag-empty-notin is used by valid-recs-in-nonempty-sqns,
bag-max/bag-union-one is used by valid-eraseq-stronger-prev-append-lref, valid-eraseq-stronger-next-append-lref, valid-eraseq-stronger-next, ubi-io-initial-valid-sqns-h,
bag-max/max-add-bigger is used by valid-eraseq-stronger-prev-append-lref,
bag-max/max-add-one-different is used by vols-is-max-is-min-eraseq, valid-eraseq-stronger-prev-append-lref, valid-eraseq-stronger-next-append-lref, valid-eraseq-stronger-next, ubi-cons-same-vtbl,
bag-max/max-rec-simp is used by valid-eraseq-stronger-next-append-lref, valid-eraseq-stronger-next,
bag-max/unique-elems-addtwice is used by vols-is-max-is-min-eraseq, vols-is-max-is-max-vols, ubi-cons-same-vtbl,
bag-max/unique-elems-empty is used by ubi-io-initial-unique-sqns,

Used from specification wlstatus

wlstatus/disj-01 is used by vols-is-max-is-min-eraseq, vols-is-max-is-max-vols, valid-wl-map-indices, valid-recs-in-nonempty-sqns, ubi-cons-same-vtbl,
wlstatus/disj-02 is used by vols-is-max-is-min-eraseq, vols-is-max-is-max-vols, valid-wl-map-indices, valid-recs-in-nonempty-sqns, ubi-cons-same-vtbl,
wlstatus/disj-03 is used by vols-is-max-is-min-eraseq, vols-is-max-is-max-vols, valid-wl-map-indices, valid-vtbl-map-indices-erasing, valid-recs-next-update, valid-recs-in-nonempty-sqns, ubi-cons-same-vtbl,
wlstatus/disj-04 is used by vols-is-max-is-min-eraseq,
wlstatus/disj-05 is used by vols-is-max-is-min-eraseq, vols-is-max-is-max-vols, valid-wl-map-indices,
wlstatus/disj-06 is used by vols-is-max-is-min-eraseq, vols-is-max-is-max-vols,

Used from specification valid-peb

Used from specification lebadress

lebadress/elim is used by valid-recs-next-update, valid-recs-next-samerecs, valid-recs-next-add,
lebadress/inj is used by valid-recs-next-update, valid-recs-next-add,
lebadress/sel-01 is used by valid-recs-next-update, valid-recs-next-samerecs, valid-recs-next-add, valid-recs-in-nonempty-sqns,
lebadress/sel-02 is used by valid-recs-next-update, valid-recs-next-samerecs, valid-recs-next-add, valid-recs-in-nonempty-sqns,

Used from specification sqns

sqns/valid-peb-in-sqnums-h is used by valid-recs-in-nonempty-sqns,
sqns/valid-sqns is used by ubi-io-initial-valid-sqns,
sqns/valid-sqns-extract-sqn-h is used by valid-eraseq-stronger-prev-append-lref, valid-eraseq-stronger-next,
sqns/valid-sqns-extract2-sqn is used by vols-is-max-is-min-eraseq, vols-is-max-is-max-vols, ubi-cons-same-vtbl,
sqns/valid-sqns-extract2-sqn-h is used by valid-eraseq-stronger-prev-append-lref,
sqns/valid-sqns-base is used by ubi-io-initial-valid-sqns-h,
sqns/valid-sqns-rec is used by valid-eraseq-stronger-prev-append-lref, valid-eraseq-stronger-next-append-none, valid-eraseq-stronger-next-append-lref, valid-eraseq-stronger-next, ubi-io-initial-valid-sqns-h,
sqns/valid-sqns-subarray is used by valid-recs-in-nonempty-sqns, valid-eraseq-stronger-prev-append-lref, valid-eraseq-stronger-next-append-none, valid-eraseq-stronger-next-append-lref, valid-eraseq-stronger-next,

Used from specification nat-list-less

nat-list-less/ls-base is used by indices-erasing-write-notin,
nat-list-less/ls-rec is used by indices-erasing-write-notin,

Used from specification ubi-base

ubi-base/in-valid-eraseqp-valid-lref is used by vols-is-max-is-min-eraseq,
ubi-base/unique-sqns is used by vols-is-max-is-min-eraseq, vols-is-max-is-max-vols, ubi-io-initial-unique-sqns, ubi-cons-same-vtbl,
ubi-base/valid-ebatbl is used by vols-is-max-is-min-eraseq, vols-is-max-is-max-vols,
ubi-base/valid-eraseqd-rec is used by valid-eraseq-strong-imp-q,
ubi-base/valid-eraseqp-rec is used by valid-eraseq-strong-imp-p,
ubi-base/valid-eraseqw is used by vols-is-max-is-min-eraseq, vols-is-max-is-max-vols, valid-eraseq-map-indices-nostatchange, indices-erasing-eraseq,
ubi-base/valid-vtbl is used by vols-is-max-is-min-eraseq, vols-is-max-is-max-vols, valid-vtbl-map-indices-erasing, ubi-cons-same-vtbl,
ubi-base/valid-wl is used by vols-is-max-is-min-eraseq, vols-is-max-is-max-vols, valid-wl-map-indices, valid-recs-in-nonempty-sqns, ubi-cons-same-vtbl,
ubi-base/is-vtbl-pnum is used by vols-is-max-is-max-vols, ubi-cons-same-vtbl,
ubi-base/ubi-cons is used by vols-is-max-is-min-eraseq, vols-is-max-is-max-vols, ubi-cons-same-vtbl,
ubi-base/valid-eraseqd-base is used by valid-eraseq-strong-imp-q,
ubi-base/valid-eraseqp-base is used by valid-eraseq-strong-imp-p,
ubi-base/valid-vtbl-in-wlar is used by vols-is-max-is-max-vols,
ubi-base/valid-vtbl-wlar-status is used by vols-is-max-is-min-eraseq,

Used from specification erasequeueentry

Used from specification wlentry

Used from specification list

list/erasequeue-base/One is used by valid-eraseq-stronger-one, valid-eraseq-strong-notinvols,
list/erasequeue-base/c is used by valid-eraseq-stronger-one, valid-eraseq-strong-notinvols,
list/erasequeue-base/Nil is used by valid-eraseq-stronger-prev-append-lref, valid-eraseq-stronger-next-append-none, valid-eraseq-stronger-next-append-lref, valid-eraseq-strong-notinvols,
list/erasequeue-base/a is used by valid-eraseq-stronger-prev-append-lref, valid-eraseq-stronger-no-maxsqnum, valid-eraseq-stronger-next-append-none, valid-eraseq-stronger-next-append-lref, valid-eraseq-stronger-next, valid-eraseq-stronger-imp-strong, valid-eraseq-strong-notinvols, valid-eraseq-strong-imp-q, valid-eraseq-strong-imp-p, in-eraseq-strong-valid, in-eraseq-strong-not-valid,
list/nat-list-set/a is used by indices-set-erasing, indices-erasing-write-prepend, indices-erasing-write-notin, indices-erasing-eraseq, indices-erasing-at,
list/nat-list-set/c is used by indices-set-erasing, indices-erasing-write-notin, indices-erasing-eraseq, indices-erasing-at,
list/erasequeue-base/c is used by valid-eraseq-stronger-prev-append-lref, valid-eraseq-stronger-no-maxsqnum, valid-eraseq-stronger-next-append-none, valid-eraseq-stronger-next-append-lref, valid-eraseq-stronger-next, valid-eraseq-stronger-imp-strong, valid-eraseq-strong-notinvols, valid-eraseq-strong-imp-q, valid-eraseq-strong-imp-p, in-eraseq-strong-valid, in-eraseq-strong-not-valid,
list/erasequeue-base/in-empty is used by in-eraseq-strong-valid,
list/nat-list-set/in-empty is used by indices-erasing-at,
list/nat-list-set/in-rec is used by indices-erasing-at,
list/erasequeue-base/in-rec is used by in-eraseq-strong-valid,

Used from specification encoding-vtbl

encoding-vtbl/is-encoded-unique is used by vols-is-max-is-min-eraseq, vols-is-max-is-max-vols, valid-vtbl-map-indices-erasing,

Used from specification array-copy

array-copy/wlarray-base/at-subarray is used by valid-recs-next-update, valid-recs-next-samerecs, valid-recs-next-add,
array-copy/apebs/subarray-at is used by valid-recs-next-update, valid-eraseq-stronger-prev-append-lref, valid-eraseq-stronger-next-append-none, valid-eraseq-stronger-next-append-lref, valid-eraseq-stronger-next,
array-copy/wlarray-base/size-subarray is used by valid-recs-in-nonempty-sqns,
array-copy/apebs/size-subarray is used by valid-recs-next-update, valid-recs-next-samerecs, valid-recs-next-add, valid-recs-in-nonempty-sqns, valid-eraseq-stronger-prev-append-lref, valid-eraseq-stronger-next-append-none, valid-eraseq-stronger-next-append-lref, valid-eraseq-stronger-next,
array-copy/apebs/subarray-at is used by valid-recs-next-update, valid-recs-next-samerecs, valid-recs-next-add, valid-recs-in-nonempty-sqns, valid-eraseq-stronger-prev-append-lref, valid-eraseq-stronger-next-append-none, valid-eraseq-stronger-next-append-lref, valid-eraseq-stronger-next,
array-copy/wlarray-base/subarray-at is used by valid-recs-next-update, valid-recs-next-samerecs, valid-recs-next-add, valid-recs-in-nonempty-sqns,
array-copy/wlarray-base/subarray-elim is used by valid-recs-next-update, valid-recs-next-samerecs, valid-recs-next-add,
array-copy/apebs/subarray-elim is used by valid-recs-next-update, valid-recs-next-samerecs, valid-recs-next-add, valid-eraseq-stronger-prev-append-lref, valid-eraseq-stronger-next-append-none, valid-eraseq-stronger-next-append-lref, valid-eraseq-stronger-next,

Used from specification vtbl-conv

vtbl-conv/to-vtbl-at is used by vols-is-max-is-max-vols, in-eraseq-strong-valid, in-eraseq-strong-not-valid,
vtbl-conv/to-vtbl-in is used by vols-is-max-is-max-vols, in-eraseq-strong-valid, in-eraseq-strong-not-valid,

Used from specification oelem

Used from specification array

array/ebatbl/Extension is used by vols-le-antisym,
array/wlarray-base/Put-other is used by indices-set-erasing,
array/wlarray-base/Put-other is used by valid-recs-next-update, valid-recs-next-samerecs, valid-recs-next-add,
array/wlarray-base/Put-same is used by indices-set-erasing, indices-erasing-write-prepend,
array/apebs/Size-mkarray is used by valid-recs-emptyset,
array/ebatbl/Size-put is used by disj-shift,
array/wlarray-base/Size-put is used by valid-recs-next-update, valid-recs-next-samerecs, valid-recs-next-add, indices-set-erasing, indices-erasing-write-prepend, indices-erasing-write-notin,
array/wlarray-base/cgetput is used by valid-recs-next-update, valid-recs-next-samerecs, valid-recs-next-add,
array/ebatbl/cngetput is used by disj-shift,
array/wlarray-base/cputput is used by valid-recs-next-update,
array/wlarray-base/ngp-06 is used by valid-recs-next-add,
array/wlarray-base/ngp-07 is used by valid-recs-next-update, valid-recs-next-samerecs, valid-recs-next-add, indices-erasing-write-notin,
array/wlarray-base/ngp-09 is used by valid-recs-next-samerecs, valid-recs-next-add,

Used from specification ebaentry

ebaentry/disj is used by vols-is-max-is-max-vols, unmapped-vols-unmapped,
ebaentry/inj is used by vols-is-max-is-max-vols,

Used from specification list-set

list-set/erasequeue-base/subset is used by indices-erasing-eraseq,

Used from specification set-union

set-union/lebrefset/subdef is used by vols-is-max-is-min-eraseq,

Used from specification ubi-io-inv

ubi-io-inv/initial is used by ubi-io-initial-valid-sqns-h,
ubi-io-inv/peb-initial is used by ubi-io-initial-valid-sqns-h,

Used from specification array-indices

array-indices/wlarray-base/map-indices-at is used by valid-wl-map-indices, valid-vtbl-map-indices-erasing, valid-eraseq-map-indices-nostatchange,
array-indices/wlarray-base/map-indices-size is used by valid-wl-map-indices, valid-vtbl-map-indices-erasing, valid-eraseq-map-indices-nostatchange,