[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 array-splice

array-splice/avolume/range-eq-ext is used by mapped-full-range-eq, lebs-range-eq,
array-splice/buffer/append-a is used by lebs-write-last, lebs-write-below, lebs-write-above, lebs-size-mappedfull, lebs-size, lebs-range-eq, lebs-idexpt-below, lebs-crash,
array-splice/buffer/append-eq-left is used by lebs-write-last, lebs-write-above, lebs-range-eq, lebs-idexpt-below, lebs-crash,
array-splice/buffer/append-eq-right is used by lebs-write-below, lebs-write-above,
array-splice/buffer/append-len is used by lebs-size-mappedfull, lebs-size,
array-splice/buffer/append-prefix-left is used by lebs-write-last, lebs-crash,
array-splice/buffer/emparray-len is used by lebs-write-last, lebs-size-mappedfull, lebs-size, lebs-crash,
array-splice/buffer/mkemparray0-append-right is used by lebs-crash,

Used from specification encoding-lpt

encoding-lpt/lptlebs-zero is used by disk-layout-avol-neq-0,

Used from specification nat-basic

nat-basic/a is used by mapped-full-zero, mapped-full-range-eq, mapped-full-last, mapped-full-idexpt-below, mapped-full-aligndown-vol, lebs-write-last, lebs-write-below, lebs-write-above, lebs-size-mappedfull, lebs-size, lebs-range-eq, lebs-idexpt-below, lebs-crash, disk-layout-size-vol-orphans, disk-layout-same-size, disk-layout-orphans-below-main, disk-layout-not1-unfold, disk-layout-main-not-below-lpt, disk-layout-lpt-below-main, disk-layout-log-not-0, disk-layout-log-neq-orphans, disk-layout-log-above-main, disk-layout-avol-neq-1, disk-layout-avol-neq-0, disk-layout-avol-le-5, disk-layout-2-unfold, disk-layout-1-unfold,
nat-basic/add-base is used by mapped-full-zero,
nat-basic/c is used by mapped-full-zero, mapped-full-range-eq, mapped-full-last, mapped-full-idexpt-below, mapped-full-aligndown-vol, lebs-write-last, lebs-write-below, lebs-write-above, lebs-size-mappedfull, lebs-size, lebs-range-eq, lebs-idexpt-below, lebs-crash, disk-layout-size-vol-orphans, disk-layout-same-size, disk-layout-orphans-below-main, disk-layout-not1-unfold, disk-layout-main-not-below-lpt, disk-layout-lpt-below-main, disk-layout-log-not-0, disk-layout-log-neq-orphans, disk-layout-log-above-main, disk-layout-avol-neq-1, disk-layout-avol-neq-0, disk-layout-avol-le-5, disk-layout-2-unfold, disk-layout-1-unfold,
nat-basic/eq-01 is used by lebs-size-mappedfull, lebs-size, disk-layout-not1-unfold, disk-layout-2-unfold, disk-layout-1-unfold,
nat-basic/f is used by mapped-full-range-eq, mapped-full-last, mapped-full-idexpt-below, mapped-full-aligndown-vol, lebs-write-last, lebs-write-below, lebs-write-above, lebs-size-mappedfull, lebs-size, lebs-range-eq, lebs-idexpt-below, lebs-crash, disk-layout-main-not-below-lpt, disk-layout-lpt-below-main, disk-layout-avol-le-5,
nat-basic/l is used by mapped-full-range-eq, mapped-full-last, lebs-size-mappedfull, lebs-range-eq, lebs-crash, disk-layout-lpt-below-main,
nat-basic/l-01 is used by mapped-full-range-eq, mapped-full-last, mapped-full-idexpt-below, mapped-full-aligndown-vol, lebs-size-mappedfull, lebs-crash,
nat-basic/l-02 is used by lebs-write-below, lebs-idexpt-below,
nat-basic/l-05 is used by disk-layout-main-not-below-lpt,
nat-basic/lf is used by mapped-full-last, mapped-full-idexpt-below, lebs-size-mappedfull, lebs-crash,
nat-basic/lf-01 is used by mapped-full-idexpt-below, mapped-full-aligndown-vol, lebs-idexpt-below, lebs-crash,
nat-basic/lf-02 is used by disk-layout-main-not-below-lpt, disk-layout-avol-le-5,
nat-basic/ls-02 is used by mapped-full-last, lebs-size-mappedfull, lebs-crash,
nat-basic/nls-fst is used by lebs-size-mappedfull, lebs-size, disk-layout-lpt-below-main, disk-layout-avol-le-5,
nat-basic/s-04 is used by mapped-full-last, lebs-size-mappedfull, lebs-crash,
nat-basic/succ is used by mapped-full-last, mapped-full-idexpt-below, lebs-write-below, lebs-write-above, lebs-size-mappedfull, lebs-size, lebs-range-eq, lebs-idexpt-below, lebs-crash,
nat-basic/z-01 is used by disk-layout-avol-neq-0,

Used from specification nat

nat/add-01 is used by lebs-range-eq,
nat/add-num-03 is used by disk-layout-orphans-below-main, disk-layout-avol-neq-1,
nat/elim-sub is used by mapped-full-range-eq, lebs-range-eq,
nat/eq-02 is used by lebs-size-mappedfull, lebs-size,
nat/fle is used by mapped-full-range-eq, mapped-full-idexpt-below, lebs-range-eq,
nat/fle-01 is used by mapped-full-range-eq, mapped-full-last, mapped-full-idexpt-below, mapped-full-aligndown-vol, lebs-size-mappedfull, lebs-range-eq, lebs-crash, disk-layout-avol-le-5,
nat/le-def is used by mapped-full-range-eq, lebs-size-mappedfull, lebs-size,
nat/le-ls-simp is used by mapped-full-zero, mapped-full-write-above, mapped-full-range-eq,
nat/le-num-06 is used by disk-layout-size-vol-orphans, disk-layout-log-above-main,
nat/lels is used by mapped-full-last, mapped-full-aligndown-vol, lebs-write-last, lebs-write-below, lebs-write-above, lebs-range-eq, lebs-crash,
nat/lels-02 is used by mapped-full-last,
nat/lels-03 is used by lebs-write-last, lebs-write-below, lebs-write-above, lebs-range-eq, lebs-idexpt-below, lebs-crash,
nat/lep is used by mapped-full-range-eq, mapped-full-last, lebs-size-mappedfull, lebs-range-eq, lebs-crash,
nat/lep-02 is used by mapped-full-last, lebs-write-last,
nat/ler is used by mapped-full-last, lebs-write-last,
nat/let is used by mapped-full-range-eq, mapped-full-last,
nat/ls-01 is used by mapped-full-range-eq,
nat/ls-le-simp is used by mapped-full-write-below, mapped-full-idexpt-below, lebs-write-last, lebs-write-below, lebs-write-above, lebs-range-eq, lebs-crash,
nat/sub-add is used by lebs-range-eq,
nat/succ-01 is used by lebs-write-last, lebs-write-below, lebs-write-above, lebs-range-eq, lebs-idexpt-below, lebs-crash,
nat/zero is used by lebs-write-last, lebs-crash,

Used from specification aleb

aleb/aleb-not-mapped is used by lebs-size,
aleb/disj is used by mapped-full-aligndown-vol, lebs-crash,
aleb/ex is used by mapped-full-write-below, mapped-full-write-above, mapped-full-range-eq, mapped-full-idexpt-below, mapped-full-aligndown-vol, lebs-write-below, lebs-size-mappedfull, lebs-size, lebs-crash,
aleb/inj is used by lebs-size-mappedfull,
aleb/sel is used by mapped-full-range-eq, mapped-full-last, mapped-full-idexpt-below, mapped-full-aligndown-vol, lebs-write-last, lebs-size-mappedfull, lebs-size, lebs-crash,
aleb/test-02 is used by mapped-full-range-eq, mapped-full-last, mapped-full-idexpt-below, mapped-full-aligndown-vol, lebs-write-last, lebs-crash,

Used from specification ebm-vol-inv

ebm-vol-inv/ebm-vol-le is used by mapped-full-aligndown-vol, lebs-crash,
ebm-vol-inv/ebm-vol-inv-lebsize is used by lebs-size,
ebm-vol-inv/le-mapped is used by lebs-crash,
ebm-vol-inv/le-size-0 is used by mapped-full-aligndown-vol,
ebm-vol-inv/le-size-1 is used by lebs-crash,

Used from specification superblock

Used from specification array-copy

array-copy/avolume/Idexcept is used by mapped-full-idexpt-below, lebs-idexpt-below,
array-copy/avolume/idexcept-size is used by mapped-full-idexpt-below, lebs-idexpt-below,

Used from specification oelem

oelem/nat-set/irreflexivity is used by mapped-full-last, lebs-size-mappedfull, lebs-crash,
oelem/nat-set/transitivity is used by mapped-full-idexpt-below, lebs-size-mappedfull, lebs-crash,

Used from specification nat-mult

nat-mult/mult-a is used by lebs-size-mappedfull, lebs-size, disk-layout-lpt-below-main, disk-layout-avol-neq-0,
nat-mult/mult-c is used by lebs-size-mappedfull, lebs-size, disk-layout-lpt-below-main, disk-layout-avol-neq-0,
nat-mult/numeral-21 is used by disk-layout-lpt-below-main,
nat-mult/one is used by disk-layout-lpt-below-main,
nat-mult/rsucc-02 is used by lebs-size-mappedfull, lebs-size,
nat-mult/zero is used by lebs-size-mappedfull, lebs-size,

Used from specification array

array/avolume/Put-other is used by mapped-full-last,
array/avolume/Put-same is used by mapped-full-write-below, mapped-full-write-above, mapped-full-last, lebs-write-last,
array/buffer/Size-mkarray is used by lebs-size-mappedfull, lebs-size,
array/avolume/Size-put is used by mapped-full-write-below, mapped-full-write-above, mapped-full-last, lebs-write-last, lebs-write-below, lebs-write-above,
array/avolume/cngetput is used by mapped-full-write-below, mapped-full-write-above, lebs-write-below,
array/avolume/ngp-07 is used by mapped-full-last, lebs-write-above,