[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 le-unmap, le-size-1, le-size-0, le-refl, le-mapped, le-inv, ebm-vol-inv-write, ebm-vol-inv-lebsize,
nat-basic/lf-01 is used by le-unmap, le-size-1, le-size-0, le-mapped, le-inv,
nat-basic/lf-02 is used by le-size-1, le-size-0,
nat-basic/ls-02 is used by le-size-1, le-size-0,

Used from specification nat

nat/lels is used by le-unmap,
nat/ls-le-simp is used by le-unmap, ebm-vol-inv-lebsize,

Used from specification aleb

aleb/aleb-not-mapped is used by le-unmap, le-mapped, le-inv, ebm-vol-inv-write,
aleb/disj is used by le-unmap, le-refl, le-mapped, le-inv,
aleb/ex is used by le-unmap, le-refl, le-mapped, le-inv, ebm-vol-inv-write,
aleb/inj is used by le-unmap, le-inv,
aleb/sel is used by le-unmap, le-inv, ebm-vol-inv-write, ebm-vol-inv-lebsize,
aleb/test-01 is used by le-unmap, ebm-vol-inv-write,
aleb/test-02 is used by le-unmap, le-mapped, le-inv, ebm-vol-inv-write, ebm-vol-inv-lebsize,

Used from specification array

array/avolume/Put-other is used by le-unmap, ebm-vol-inv-write,
array/avolume/Put-same is used by le-unmap, ebm-vol-inv-write,
array/avolume/Size-put is used by le-unmap, ebm-vol-inv-write,
array/avolume/cgetput is used by le-unmap,
array/avolume/cngetput is used by le-unmap,