[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 nat-basic

nat-basic/a is used by ebm-cons-is-aligned-fill, ebm-cons-above-fillcount,
nat-basic/add-base is used by ebm-cons-above-fillcount,
nat-basic/c is used by ebm-cons-is-aligned-fill, ebm-cons-above-fillcount,
nat-basic/f is used by ebm-cons-aligned, ebm-cons-above-fillcount,
nat-basic/l is used by ebm-cons-above-fillcount,
nat-basic/l-06 is used by ebm-cons-above-fillcount,
nat-basic/lf-01 is used by ebm-cons-above-fillcount,

Used from specification ebm-base

ebm-base/ebm-cons is used by ebm-cons-aligned, ebm-cons-above-fillcount,
ebm-base/ebm-cons-def is used by ebm-cons-aligned, ebm-cons-above-fillcount,
ebm-base/ebm-cons-leb-size is used by ebm-cons-lebsize,
ebm-base/valid-leb-def is used by ebm-cons-aligned, ebm-cons-above-fillcount,

Used from specification nat

nat/elim-sub is used by ebm-cons-above-fillcount,
nat/fle is used by ebm-cons-above-fillcount,
nat/fle-01 is used by ebm-cons-above-fillcount,
nat/lels is used by ebm-cons-above-fillcount,
nat/ler is used by ebm-cons-above-fillcount,
nat/let is used by ebm-cons-above-fillcount,
nat/ls-le-simp is used by ebm-cons-above-fillcount,

Used from specification aleb

aleb/disj is used by abs-leb-eq-mapped,
aleb/ex is used by abs-leb-eq-mapped,
aleb/inj is used by abs-leb-eq-mapped,
aleb/test-02 is used by abs-leb-eq-mapped,

Used from specification leb

leb/sel is used by ebm-cons-aligned, ebm-cons-above-fillcount,
leb/sel-01 is used by ebm-cons-aligned, ebm-cons-above-fillcount,
leb/test-03 is used by ebm-cons-aligned, ebm-cons-above-fillcount,

Used from specification align

align/is-aligned-add is used by ebm-cons-is-aligned-fill,

Used from specification eraseblock

eraseblock/emptyleb-at is used by ebm-cons-above-fillcount,
eraseblock/emptyleb-size is used by ebm-cons-above-fillcount,
eraseblock/lebsize-neq-zero is used by ebm-cons-above-fillcount,
eraseblock/page-size is used by ebm-cons-is-aligned-fill,

Used from specification array-splice

array-splice/buffer/range-eq-ext is used by ebm-cons-above-fillcount,