[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 wbuf-cons-nbytes-ls-pagesize,
nat-basic/c is used by wbuf-cons-nbytes-ls-pagesize,
nat-basic/f is used by wbuf-cons-nbytes-ls-pagesize, wbuf-cons-nbytes-le-pagesize, wbuf-cons-nbytes-aligned,
nat-basic/l-02 is used by wbuf-cons-nbytes-ls-pagesize,
nat-basic/lf is used by wbuf-cons-nbytes-ls-pagesize,
nat-basic/lf-01 is used by wbuf-cons-nbytes-ls-pagesize, wbuf-cons-nbytes-le-pagesize, wbuf-cons-nbytes-aligned,
nat-basic/lf-02 is used by wbuf-cons-nbytes-ls-pagesize,
nat-basic/succ is used by wbuf-cons-nbytes-ls-pagesize,

Used from specification nat

nat/fle is used by wbuf-cons-nbytes-le-pagesize,
nat/fle-01 is used by wbuf-cons-nbytes-le-pagesize,

Used from specification wbuf

wbuf/sel-01 is used by wbuf-cons-nbytes-ls-pagesize, wbuf-cons-nbytes-le-pagesize, wbuf-cons-nbytes-aligned,
wbuf/sel-02 is used by wbuf-cons-nbytes-ls-pagesize, wbuf-cons-nbytes-le-pagesize, wbuf-cons-nbytes-aligned,
wbuf/sel-03 is used by wbuf-cons-nbytes-ls-pagesize, wbuf-cons-nbytes-le-pagesize, wbuf-cons-nbytes-aligned,

Used from specification aleb

aleb/ex is used by wbuf-cons-nbytes-ls-pagesize, wbuf-cons-nbytes-le-pagesize, wbuf-cons-nbytes-aligned,

Used from specification align

align/is-aligned-ls-eq-zero is used by wbuf-cons-nbytes-aligned,
align/is-aligned-zero is used by wbuf-cons-nbytes-aligned,

Used from specification oelem

oelem/nat-set/irreflexivity is used by wbuf-cons-nbytes-le-pagesize,
oelem/nat-set/transitivity is used by wbuf-cons-nbytes-ls-pagesize,

Used from specification eraseblock

eraseblock/page-size is used by wbuf-cons-nbytes-ls-pagesize, wbuf-cons-nbytes-le-pagesize, wbuf-cons-nbytes-aligned,