[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 is-encoded-size, is-encoded-emptypage-middle, is-encoded-emptypage-append,
nat-basic/c is used by is-encoded-size, is-encoded-emptypage-middle, is-encoded-emptypage-append,
nat-basic/eq-01 is used by is-encoded-size,
nat-basic/succ is used by is-encoded-size,

Used from specification encoding-page-size-nonempty

encoding-page-size-nonempty/encoding-ref-node/is-encoded-pagesize is used by is-encoded-emptypage,
encoding-page-size-nonempty/encoding-ref-node/is-encoded-size is used by is-encoded-unique, is-encoded-size, is-encoded-emptypage-middle, is-encoded-emptypage-append, is-encoded-emptypage, is-encoded-empty, is-encoded-app-one, is-encoded-app,
encoding-page-size-nonempty/encoding-ref-node/is-encoded-unique is used by is-encoded-unique, is-encoded-app-one, is-encoded-app,

Used from specification array-splice

array-splice/buffer/append-a is used by is-encoded-emptypage-middle, is-encoded-emptypage-append,
array-splice/buffer/append-inj is used by is-encoded-unique, is-encoded-emptypage-middle, is-encoded-emptypage-append,
array-splice/buffer/array-split1 is used by is-encoded-emptypage-middle, is-encoded-emptypage-append,
array-splice/buffer/append-a is used by is-encoded-unique, is-encoded-size, is-encoded-one, is-encoded-emptypage-middle, is-encoded-emptypage-append, is-encoded-empty, is-encoded-app-one, is-encoded-app,
array-splice/buffer/append-eq-emptyar is used by is-encoded-unique, is-encoded-emptypage-middle, is-encoded-emptypage-append, is-encoded-empty,
array-splice/buffer/append-eq-left is used by is-encoded-app-one,
array-splice/buffer/append-left-size0 is used by is-encoded-emptypage-middle, is-encoded-emptypage-append,
array-splice/buffer/append-len is used by is-encoded-size, is-encoded-emptypage-middle, is-encoded-emptypage-append,
array-splice/buffer/append-zero-left is used by is-encoded-app-one, is-encoded-app,
array-splice/buffer/append-zero-right is used by is-encoded-one, is-encoded-emptypage-append,

Used from specification nat

nat/add-num-03 is used by is-encoded-emptypage-append,
nat/le-def is used by is-encoded-emptypage-middle, is-encoded-emptypage-append,
nat/lels is used by is-encoded-emptypage-append,
nat/lels-02 is used by is-encoded-emptypage,
nat/ls-le-simp is used by is-encoded-emptypage-append,

Used from specification ref-node

ref-node/inj is used by is-encoded-unique,

Used from specification list-data

list-data/nat-list-set/size-01 is used by is-encoded-size,

Used from specification align

align/is-aligned-add is used by is-encoded-emptypage-middle, is-encoded-emptypage-append,
align/is-aligned-le-eq-zero is used by is-encoded-emptypage-middle, is-encoded-emptypage-append,
align/is-aligned-ls-eq-zero is used by is-encoded-emptypage-middle, is-encoded-emptypage-append,
align/is-aligned-multiplier is used by is-encoded-pagealigned,
align/is-aligned-same is used by is-encoded-emptypage-middle, is-encoded-emptypage-append,
align/is-aligned-zero is used by is-encoded-emptypage-middle, is-encoded-emptypage-append,

Used from specification list

list/nat-list-set/One is used by is-encoded-one,
list/nat-list-set/c is used by is-encoded-one,
list/nat-list-set/Nil is used by is-encoded-app-one, is-encoded-app,
list/nat-list-set/a is used by is-encoded-unique, is-encoded-size, is-encoded-emptypage-middle, is-encoded-emptypage-append, is-encoded-empty, is-encoded-app-one, is-encoded-app,
list/nat-list-set/c is used by is-encoded-unique, is-encoded-size, is-encoded-emptypage-middle, is-encoded-emptypage-append, is-encoded-empty, is-encoded-app-one, is-encoded-app,
list/nat-list-set/c-06 is used by is-encoded-unique,
list/nat-list-set/e-01 is used by is-encoded-unique, is-encoded-empty,
list/nat-list-set/len-05 is used by is-encoded-size,

Used from specification array-copy

array-copy/buffer/subarray-elim is used by is-encoded-emptypage,

Used from specification nat-mult

nat-mult/coef-14 is used by is-encoded-emptypage-append,
nat-mult/mult-a is used by is-encoded-size, is-encoded-pagealigned, is-encoded-emptypage-append,
nat-mult/mult-c is used by is-encoded-size, is-encoded-pagealigned, is-encoded-emptypage-append,
nat-mult/rsucc-02 is used by is-encoded-size,
nat-mult/two-02 is used by is-encoded-emptypage-append,
nat-mult/zero is used by is-encoded-size,

Used from specification eraseblock

eraseblock/empbuf-eq-emptypage is used by is-encoded-emptypage,
eraseblock/emptypage-at is used by is-encoded-emptypage-append,
eraseblock/emptypage-size is used by is-encoded-emptypage-middle, is-encoded-emptypage-append, is-encoded-emptypage,
eraseblock/isempty-empbuf is used by is-encoded-emptypage,
eraseblock/page-size is used by is-encoded-unique, is-encoded-pagealigned, is-encoded-emptypage-middle, is-encoded-emptypage-append, is-encoded-empty,
eraseblock/page-size-plus-eq-0 is used by is-encoded-emptypage-middle, is-encoded-emptypage-append,

Used from specification array

array/buffer/Extension is used by is-encoded-emptypage-middle, is-encoded-emptypage-append,
array/buffer/Size-mkarray is used by is-encoded-unique, is-encoded-size, is-encoded-emptypage-middle, is-encoded-emptypage-append, is-encoded-empty,

Used from specification encoding-fixed-size-nonempty

encoding-fixed-size-nonempty/encoding-ref-node/is-encoded-nonempty is used by is-encoded-emptypage,