[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-unique, is-encoded-split-one, is-encoded-size, is-encoded-pad-unique, is-encoded-pad-too-small,
nat-basic/add-base is used by is-encoded-unique, is-encoded-split-one, is-encoded-pad-too-small,
nat-basic/c is used by is-encoded-unique, is-encoded-split-one, is-encoded-size, is-encoded-pad-unique, is-encoded-pad-too-small,
nat-basic/eq-01 is used by is-encoded-unique, is-encoded-split-one, is-encoded-size,
nat-basic/eq-02 is used by is-encoded-split-one,
nat-basic/f is used by is-encoded-too-small, is-encoded-split-one, is-encoded-pad-too-small,
nat-basic/l is used by is-encoded-split-one,
nat-basic/lf-01 is used by is-encoded-split-one,
nat-basic/lf-02 is used by is-encoded-too-small, is-encoded-split-one,
nat-basic/nls-fst is used by is-encoded-unique, is-encoded-split-one, is-encoded-pad-too-small,
nat-basic/one-01 is used by is-encoded-size,
nat-basic/oz is used by is-encoded-unique, is-encoded-split-one, is-encoded-size,
nat-basic/s-04 is used by is-encoded-split-one, is-encoded-size,
nat-basic/z-01 is used by is-encoded-unique, is-encoded-split-one,

Used from specification array-splice

array-splice/buffer/append-a is used by is-encoded-unique, is-encoded-split-one, is-encoded-size, is-encoded-pad-unique, is-encoded-pad-too-small, is-encoded-pad-empbuf,
array-splice/buffer/append-eq-emptyar is used by is-encoded-split-one, is-encoded-pad-empbuf,
array-splice/buffer/append-inj is used by is-encoded-unique, is-encoded-split-one, is-encoded-pad-unique,
array-splice/buffer/append-left-size0 is used by is-encoded-split-one,
array-splice/buffer/append-len is used by is-encoded-unique, is-encoded-split-one, is-encoded-size, is-encoded-pad-unique, is-encoded-pad-too-small,
array-splice/buffer/append-right-size0 is used by is-encoded-split-one,
array-splice/buffer/append-zero-left is used by is-encoded-pad-too-small, is-encoded-pad-empbuf,
array-splice/buffer/append-zero-right is used by is-encoded-split-one,

Used from specification set-union

set-union/nat-set/Delete is used by is-encoded-split-one,
set-union/nat-set/del-addeq-05 is used by is-encoded-split-one,
set-union/nat-set/del-e-01 is used by is-encoded-split-one,
set-union/nat-set/del-e-02 is used by is-encoded-split-one,
set-union/nat-set/del-eq is used by is-encoded-unique,
set-union/nat-set/del-feq is used by is-encoded-split-one,
set-union/nat-set/del-size is used by is-encoded-unique, is-encoded-split-one, is-encoded-size,
set-union/nat-set/del-size-02 is used by is-encoded-split-one,

Used from specification nat

nat/add-01 is used by is-encoded-unique, is-encoded-split-one,
nat/elim-pred-c is used by is-encoded-unique, is-encoded-split-one, is-encoded-size,
nat/le-def is used by is-encoded-unique, is-encoded-split-one, is-encoded-size,
nat/le-num-03 is used by is-encoded-split-one,
nat/lels is used by is-encoded-unique, is-encoded-split-one,
nat/lep-02 is used by is-encoded-unique, is-encoded-split-one,
nat/ls is used by is-encoded-split-one,
nat/ls-01 is used by is-encoded-unique, is-encoded-split-one, is-encoded-size,

Used from specification encoding-fixed-size

encoding-fixed-size/encoding-nat/encoding-requires-space is used by is-encoded-unique, is-encoded-too-small, is-encoded-split-one, is-encoded-pad-too-small, is-encoded-pad-empbuf,
encoding-fixed-size/encoding-nat/is-encoded-size is used by is-encoded-unique, is-encoded-split-one, is-encoded-size,

Used from specification set-basic

set-basic/nat-set/Extension is used by is-encoded-split-one,
set-basic/nat-set/Size-insert is used by is-encoded-split-one,
set-basic/nat-set/In-empty is used by is-encoded-split-one,
set-basic/nat-set/In-insert is used by is-encoded-split-one,
set-basic/nat-set/Size-empty is used by is-encoded-unique, is-encoded-too-small, is-encoded-split-one, is-encoded-size, is-encoded-pad-too-small, is-encoded-pad-empbuf,
set-basic/nat-set/ne is used by is-encoded-split-one,
set-basic/nat-set/ne-01 is used by is-encoded-unique, is-encoded-split-one, is-encoded-size,
set-basic/nat-set/size-zero is used by is-encoded-split-one, is-encoded-pad-too-small,
set-basic/nat-set/size-zero-01 is used by is-encoded-unique, is-encoded-too-small, is-encoded-split-one, is-encoded-size, is-encoded-pad-too-small, is-encoded-pad-empbuf,

Used from specification encoding

encoding/encoding-nat/is-encoded-prefix is used by is-encoded-unique, is-encoded-split-one,
encoding/encoding-nat/is-encoded-unique is used by is-encoded-split-one,

Used from specification align

align/is-aligned-add is used by is-encoded-pad-unique, is-encoded-pad-too-small,
align/is-aligned-zero is used by is-encoded-pad-empbuf,

Used from specification oelem

oelem/nat-set/irreflexivity is used by is-encoded-size,

Used from specification nat-mult

nat-mult/coef-17 is used by is-encoded-unique, is-encoded-split-one,
nat-mult/ls-01 is used by is-encoded-too-small,
nat-mult/mult-a is used by is-encoded-unique, is-encoded-too-small, is-encoded-split-one, is-encoded-size, is-encoded-pad-empbuf,
nat-mult/mult-c is used by is-encoded-unique, is-encoded-too-small, is-encoded-split-one, is-encoded-size, is-encoded-pad-empbuf,
nat-mult/rsucc-02 is used by is-encoded-unique, is-encoded-split-one, is-encoded-size,
nat-mult/zero is used by is-encoded-unique, is-encoded-too-small, is-encoded-split-one, is-encoded-size,
nat-mult/zero-02 is used by is-encoded-split-one,
nat-mult/zero-06 is used by is-encoded-unique, is-encoded-pad-empbuf,

Used from specification eraseblock

eraseblock/page-size is used by is-encoded-pad-unique, is-encoded-pad-too-small, is-encoded-pad-empbuf,

Used from specification array

array/buffer/Size-mkarray is used by is-encoded-unique, is-encoded-split-one, is-encoded-size, is-encoded-pad-too-small, is-encoded-pad-empbuf,
array/buffer/size-0 is used by is-encoded-too-small,