[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 ubi-io-inv-extract, ubi-io-initial-imp-inv, reduce-initial, reduce,
apeb/inj is used by reduce-initial, reduce,
apeb/sel-04 is used by ubi-io-inv-extract, ubi-io-initial-imp-inv, reduce-initial, reduce, peb-inv-write-vidhdr, peb-inv-write-echdr, peb-inv-empty-vidhdr, peb-inv-empty-echdr,
apeb/sel-05 is used by ubi-io-inv-extract, ubi-io-initial-imp-inv, reduce-initial, reduce, peb-inv-write-vidhdr, peb-inv-write-echdr, peb-inv-empty-vidhdr, peb-inv-empty-echdr,
apeb/sel-06 is used by ubi-io-inv-extract, ubi-io-initial-imp-inv, reduce-initial, reduce, peb-inv-write-vidhdr, peb-inv-write-echdr, peb-inv-size, peb-inv-markbad, peb-inv-empty-vidhdr, peb-inv-empty-echdr, inv-size,
apeb/sel-07 is used by ubi-io-inv-extract, ubi-io-initial-imp-inv, reduce-initial, reduce, peb-inv-write-vidhdr, peb-inv-write-echdr, peb-inv-empty-vidhdr, peb-inv-empty-echdr,
apeb/sel-08 is used by ubi-io-inv-extract, ubi-io-initial-imp-inv, reduce-initial, reduce, peb-inv-write-vidhdr, peb-inv-write-echdr, peb-inv-markbad, peb-inv-empty-vidhdr, peb-inv-empty-echdr,

Used from specification aecheader

aecheader/disj-01 is used by peb-inv-empty-echdr,
aecheader/test-01 is used by peb-inv-write-vidhdr,
aecheader/test-03 is used by peb-inv-empty-vidhdr,

Used from specification array-splice

array-splice/buffer/emparray-len is used by peb-inv-write-vidhdr, peb-inv-write-echdr, peb-inv-empty-vidhdr, peb-inv-empty-echdr,
array-splice/buffer/mkemparray-eq is used by peb-inv-write-vidhdr, peb-inv-write-echdr, peb-inv-empty-vidhdr, peb-inv-empty-echdr,

Used from specification nat-basic

nat-basic/f is used by ubi-io-inv-extract, ubi-io-initial-imp-inv, reduce-initial, reduce, inv-size,

Used from specification nat

nat/lez is used by peb-inv-write-vidhdr, peb-inv-write-echdr, peb-inv-empty-vidhdr, peb-inv-empty-echdr,
nat/sub-base is used by peb-inv-write-vidhdr, peb-inv-write-echdr, peb-inv-empty-vidhdr, peb-inv-empty-echdr,

Used from specification align

align/is-aligned-zero is used by peb-inv-write-vidhdr, peb-inv-write-echdr, peb-inv-empty-vidhdr, peb-inv-empty-echdr,

Used from specification array-copy

array-copy/buffer/subarray-elim is used by peb-inv-write-vidhdr, peb-inv-write-echdr, peb-inv-empty-vidhdr, peb-inv-empty-echdr,

Used from specification eraseblock

eraseblock/page-size is used by peb-inv-write-vidhdr, peb-inv-write-echdr, peb-inv-empty-vidhdr, peb-inv-empty-echdr,

Used from specification array

array/apebs/Put-other is used by reduce-initial, reduce,
array/apebs/Put-same is used by reduce-initial, reduce,
array/apebs/Size-put is used by reduce-initial, reduce,