[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 encoding-page-size-nonempty

encoding-page-size-nonempty/encoding-echeader/is-encoded-unique is used by reduce-initial,

Used from specification nat-basic

Used from specification mtd-base

mtd-base/mtd-valid-peb is used by reduce-initial,

Used from specification nat

nat/elim-sub is used by reduce-initial,
nat/le-def is used by reduce-initial,

Used from specification peb

peb/elim is used by reduce-initial,
peb/inj is used by reduce-initial,
peb/sel-05 is used by reduce-initial,
peb/sel-06 is used by reduce-initial,
peb/sel-07 is used by reduce-initial,

Used from specification align

align/is-aligned-same is used by reduce-initial,

Used from specification nat-mult

nat-mult/mult-a is used by reduce-initial,
nat-mult/mult-c is used by reduce-initial,
nat-mult/two-02 is used by reduce-initial,

Used from specification eraseblock

eraseblock/lebsize-pebsize is used by reduce-initial,
eraseblock/page-size is used by reduce-initial,
eraseblock/pebsize-le-page-size is used by reduce-initial,
eraseblock/pebsize-minus-eb-page-size is used by reduce-initial,

Used from specification echeader

echeader/inj is used by reduce-initial,

Used from specification array

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