[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/f is used by abs-size1, abs-size0, abs-nobuffer, abs-mapped-is-mapped-rev, abs-mapped-is-mapped,
nat-basic/lf is used by abs-size0,
nat-basic/lf-01 is used by abs-size1, abs-size0, abs-nobuffer, abs-mapped-is-mapped-rev, abs-mapped-is-mapped,
nat-basic/lf-02 is used by abs-size1, abs-size0,
nat-basic/ls-02 is used by abs-size1, abs-size0,

Used from specification wbuf

wbuf/elim is used by abs-mapped-is-mapped-rev, abs-mapped-is-mapped,
wbuf/sel-01 is used by abs-mapped-is-mapped-rev,
wbuf/sel-03 is used by abs-mapped-is-mapped-rev,

Used from specification aleb

aleb/aleb-not-mapped is used by abs-mapped-is-mapped-rev, abs-mapped-is-mapped,
aleb/disj is used by abs-mapped-is-mapped-rev, abs-mapped-is-mapped,
aleb/sel is used by abs-mapped-is-mapped-rev,

Used from specification array-copy

array-copy/buffer/subarray-elim is used by abs-size1, abs-size0,

Used from specification bufleb

bufleb/disj is used by abs-nobuffer,

Used from specification oelem

oelem/nat-set/irreflexivity is used by abs-size1, abs-size0,

Used from specification array

array/avolume/Extension is used by abs-nobuffer,