[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 abs-reduce0, abs-reduce, abs-peb-empty, abs-fwd,
apeb/inj is used by abs-reduce0, abs-reduce, abs-peb-empty,
apeb/sel-04 is used by abs-reduce0, abs-reduce, abs-fwd, abs-fillcount-valid-headers, abs-fillcount-empty-vidhdr, abs-fillcount-empty-echdr, abs-data-at,
apeb/sel-05 is used by abs-reduce0, abs-reduce, abs-fwd, abs-fillcount-valid-headers, abs-fillcount-empty-vidhdr, abs-data-at,
apeb/sel-06 is used by abs-reduce0, abs-reduce, abs-fwd, abs-fillcount-valid-headers, abs-fillcount-empty-vidhdr, abs-data-at,
apeb/sel-07 is used by abs-reduce0, abs-reduce, abs-fwd, abs-fillcount-valid-headers, abs-data-at,
apeb/sel-08 is used by abs-reduce0, abs-reduce, abs-fwd, abs-fillcount-valid-headers, abs-fillcount-empty-vidhdr, abs-fillcount-empty-echdr, abs-data-at, abs-bad,

Used from specification nat-basic

nat-basic/c is used by abs-fillcount-valid-headers, abs-data-at,
nat-basic/f is used by abs-size-apebs0, abs-reduce0, abs-reduce, abs-fwd, abs-fillcount-valid-headers, abs-fillcount-empty-vidhdr, abs-fillcount-empty-echdr, abs-data-at, abs-bad,
nat-basic/lf is used by abs-size-apebs0,
nat-basic/lf-01 is used by abs-size-apebs0, abs-reduce0, abs-reduce, abs-fwd, abs-fillcount-valid-headers, abs-fillcount-empty-vidhdr, abs-fillcount-empty-echdr, abs-data-at, abs-bad,
nat-basic/lf-02 is used by abs-size-apebs0,
nat-basic/ls-02 is used by abs-size-apebs0,
nat-basic/ref is used by abs-size-apebs0,

Used from specification aecheader

aecheader/disj-01 is used by abs-reduce0, abs-reduce, abs-peb-empty, abs-fwd, abs-fillcount-valid-headers, abs-fillcount-empty-vidhdr, abs-data-at,
aecheader/not-garbage-valid-imp-empty is used by abs-peb-empty,
aecheader/test-01 is used by abs-peb-empty, abs-fillcount-valid-headers, abs-fillcount-empty-vidhdr,
aecheader/test-03 is used by abs-fillcount-valid-headers,

Used from specification array-splice

array-splice/buffer/emparray-at is used by abs-peb-empty,
array-splice/buffer/emparray-len is used by abs-peb-empty,

Used from specification encoding-page-size-nonempty

encoding-page-size-nonempty/encoding-vidheader/is-encoded-pagesize is used by is-encoded-vidheader-emptypage,
encoding-page-size-nonempty/encoding-echeader/is-encoded-pagesize is used by is-encoded-echeader-emptypage,
encoding-page-size-nonempty/encoding-vidheader/is-encoded-not-garbage-pagesize is used by abs-fillcount-valid-headers,
encoding-page-size-nonempty/encoding-vidheader/is-encoded-size is used by is-encoded-vidheader-emptypage,
encoding-page-size-nonempty/encoding-echeader/is-encoded-size is used by is-encoded-echeader-emptypage,

Used from specification mtd-base

mtd-base/mtd-cons-peb-size is used by abs-data-at,

Used from specification avidheader

avidheader/disj-01 is used by abs-reduce0, abs-reduce, abs-peb-empty, abs-fwd, abs-fillcount-valid-headers, abs-fillcount-empty-vidhdr, abs-data-at,
avidheader/not-garbage-valid-imp-empty is used by abs-peb-empty,
avidheader/test-01 is used by abs-peb-empty, abs-fillcount-valid-headers, abs-fillcount-empty-vidhdr,

Used from specification peb

peb/elim is used by abs-reduce0, abs-reduce, abs-fwd,
peb/inj is used by abs-reduce0, abs-reduce,
peb/sel-05 is used by abs-reduce0, abs-reduce, abs-peb-empty, abs-fwd, abs-fillcount-valid-headers, abs-fillcount-empty-vidhdr, abs-fillcount-empty-echdr, abs-data-at, abs-bad,
peb/sel-06 is used by abs-reduce0, abs-reduce, abs-peb-empty, abs-fwd, abs-fillcount-valid-headers, abs-fillcount-empty-vidhdr, abs-fillcount-empty-echdr, abs-data-at,
peb/sel-07 is used by abs-reduce0, abs-reduce, abs-peb-empty, abs-fwd, abs-fillcount-valid-headers, abs-fillcount-empty-vidhdr, abs-data-at,

Used from specification nat

nat/lels is used by subarray-emptypeb1, subarray-emptypeb0, abs-reduce0, abs-reduce, abs-peb-empty, abs-data-at,
nat/lels-02 is used by is-encoded-vidheader-emptypage, is-encoded-echeader-emptypage,
nat/ls-le-simp is used by subarray-emptypeb1, subarray-emptypeb0, abs-reduce0, abs-reduce, abs-peb-empty, abs-data-at,

Used from specification ubi-io-abs

ubi-io-abs/subarray-emptypeb0 is used by subarray-emptypeb0, abs-peb-empty,
ubi-io-abs/subarray-emptypeb1 is used by subarray-emptypeb1, abs-peb-empty,

Used from specification array-copy

array-copy/buffer/subarray-at is used by abs-data-at,
array-copy/buffer/subarray-elim is used by is-encoded-vidheader-emptypage, is-encoded-echeader-emptypage, abs-size-apebs0, abs-fillcount-valid-headers, abs-fillcount-empty-vidhdr, abs-data-at,

Used from specification eraseblock

eraseblock/empbuf-eq-emptypage is used by is-encoded-vidheader-emptypage, is-encoded-echeader-emptypage,
eraseblock/emptyleb-at is used by abs-peb-empty,
eraseblock/emptyleb-size is used by abs-peb-empty,
eraseblock/emptypage-at is used by subarray-emptypeb1, subarray-emptypeb0,
eraseblock/emptypage-size is used by subarray-emptypeb1, subarray-emptypeb0, is-encoded-vidheader-emptypage, is-encoded-echeader-emptypage,
eraseblock/isempty-empbuf is used by is-encoded-vidheader-emptypage, is-encoded-echeader-emptypage,
eraseblock/lebsize-neq-zero is used by abs-data-at,
eraseblock/page-size is used by abs-peb-empty, abs-fillcount-empty-vidhdr,
eraseblock/subarray-emptypeb-eq-emptyleb is used by abs-peb-empty,

Used from specification nat-mult

nat-mult/mult-a is used by abs-peb-empty,
nat-mult/mult-c is used by abs-peb-empty,

Used from specification array

array/buffer/Extension is used by subarray-emptypeb1, subarray-emptypeb0, abs-peb-empty,
array/apebs/Put-other is used by abs-reduce0, abs-reduce,
array/pebs/Put-other is used by abs-reduce0, abs-reduce,
array/apebs/Put-same is used by abs-reduce0, abs-reduce,
array/apebs/Size-put is used by abs-reduce0, abs-reduce,
array/pebs/Size-put is used by abs-reduce0, abs-reduce,
array/pebs/cgetput is used by abs-reduce0, abs-reduce,

Used from specification encoding-fixed-size-nonempty

encoding-fixed-size-nonempty/encoding-vidheader/is-encoded-nonempty is used by is-encoded-vidheader-emptypage,
encoding-fixed-size-nonempty/encoding-echeader/is-encoded-nonempty is used by is-encoded-echeader-emptypage,