[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 node-header-size-add-eq-0, leb-size-aligned-2-node-header, 2-node-header-size-add-eq-0,
nat-basic/add-base is used by leb-size-aligned-2-node-header,
nat-basic/c is used by node-header-size-add-eq-0, leb-size-aligned-2-node-header, 2-node-header-size-add-eq-0,
nat-basic/f is used by leb-size-aligned-2-node-header,
nat-basic/z-01 is used by node-header-size-add-eq-0, 2-node-header-size-add-eq-0,
nat-basic/zero is used by leb-size-aligned-2-node-header,

Used from specification nat

nat/lels is used by node-header-size-ls-2-node-header-size,

Used from specification align

align/is-aligned-def is used by leb-size-aligned-2-node-header,
align/is-aligned-elim is used by is-aligned-pagesize-imp-2headersize, headersize2-mod-pagesize-is-0,
align/is-aligned-multiple-1 is used by page-size-aligned-node-header, leb-size-aligned-node-header, is-aligned-pagesize-imp-headersize,
align/is-aligned-of-mod is used by is-aligned-nodeheadersize-mod-pagesize,

Used from specification eraseblock

eraseblock/isempty-empbuf is used by validtrailer-neq-empty,
eraseblock/lebsize-page-size-is-aligned is used by leb-size-aligned-2-node-header,
eraseblock/page-size is used by leb-size-aligned-2-node-header, is-aligned-pagesize-imp-2headersize, is-aligned-nodeheadersize-mod-pagesize, headersize2-mod-pagesize-is-0,

Used from specification nat-mult

nat-mult/modeq-01 is used by leb-size-aligned-2-node-header,
nat-mult/mult-a is used by page-size-aligned-node-header, node-header-size-ls-2-node-header-size, leb-size-aligned-node-header, leb-size-aligned-2-node-header, is-aligned-pagesize-imp-headersize, is-aligned-pagesize-imp-2headersize, headersize2-mod-pagesize-is-0, 2-node-header-size-add-eq-0,
nat-mult/mult-c is used by page-size-aligned-node-header, node-header-size-ls-2-node-header-size, leb-size-aligned-node-header, leb-size-aligned-2-node-header, is-aligned-pagesize-imp-headersize, is-aligned-pagesize-imp-2headersize, headersize2-mod-pagesize-is-0, 2-node-header-size-add-eq-0,
nat-mult/one-01 is used by headersize2-mod-pagesize-is-0,
nat-mult/two-zero-01 is used by leb-size-aligned-2-node-header, is-aligned-pagesize-imp-2headersize, headersize2-mod-pagesize-is-0, 2-node-header-size-add-eq-0,
nat-mult/twole is used by node-header-size-ls-2-node-header-size,
nat-mult/zero-01 is used by headersize2-mod-pagesize-is-0,
nat-mult/zero-02 is used by headersize2-mod-pagesize-is-0,
nat-mult/zero-03 is used by headersize2-mod-pagesize-is-0,
nat-mult/zero-06 is used by headersize2-mod-pagesize-is-0,

Used from specification array

array/buffer/Extension is used by validtrailer-neq-0,
array/buffer/Size-mkarray is used by validtrailer-neq-0,

Used from specification nat-div

nat-div/modex is used by headersize2-mod-pagesize-is-0,
nat-div/div-elim is used by leb-size-aligned-2-node-header,
nat-div/mod-zero is used by headersize2-mod-pagesize-is-0,