[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 apeb

apeb/elim is used by delta-atomic-leb-change,
apeb/sel-04 is used by delta-atomic-leb-change,
apeb/sel-05 is used by delta-atomic-leb-change,
apeb/sel-07 is used by delta-atomic-leb-change,
apeb/sel-08 is used by delta-atomic-leb-change,
apeb/upd-05 is used by delta-atomic-leb-change,

Used from specification nat-basic

nat-basic/a is used by sum-of-differences-rem, sum-of-differences-in, in-ecs-n, in-delta, ecs-n-write, ecs-n-empty, delta-write, delta-atomic-leb-change,
nat-basic/add-base is used by delta-write, delta-atomic-leb-change,
nat-basic/c is used by sum-of-differences-rem, sum-of-differences-in, in-ecs-n, in-delta, ecs-n-write, ecs-n-empty, delta-write, delta-atomic-leb-change,
nat-basic/eq-01 is used by sum-of-differences-rem, delta-write,
nat-basic/eq-02 is used by delta-write,
nat-basic/f is used by sum-of-differences-in, in-ecs-n, in-ecs, in-delta, ecs-write-same, ecs-write, ecs-n-write, delta-write-same, delta-write, delta-atomic-leb-change,
nat-basic/l-01 is used by delta-write,
nat-basic/l-02 is used by sum-of-differences-in,
nat-basic/lf is used by in-ecs-n, ecs-n-write,
nat-basic/lf-01 is used by delta-write,
nat-basic/lf-02 is used by in-ecs-n,
nat-basic/ls-02 is used by in-ecs-n, ecs-n-write,
nat-basic/nls-fst is used by sum-of-differences-in,
nat-basic/oz is used by ecs-n-empty,
nat-basic/s-04 is used by in-ecs-n, ecs-n-write,
nat-basic/succ is used by in-ecs-n, ecs-n-write, ecs-n-empty,
nat-basic/zero is used by delta-atomic-leb-change,
nat-basic/zero-01 is used by in-ecs-n, ecs-n-write,

Used from specification bag-union

bag-union/nat-bag/del-empty is used by sum-of-differences-rem, bag-rem-eq-empty-elim,
bag-union/nat-bag/del-rec is used by sum-of-differences-rem, ecs-n-write, bag-rem-eq-empty-elim,
bag-union/nat-bag/in-add is used by sum-of-differences-rem, in-ecs-n,
bag-union/nat-bag/in-at is used by sum-of-differences-rem,
bag-union/nat-bag/in-emp is used by sum-of-differences-rem, sum-of-differences-in, in-ecs-n,

Used from specification avidheader

avidheader/test-03 is used by delta-atomic-leb-change,
avidheader/upd-06 is used by delta-atomic-leb-change,

Used from specification nat

nat/add-01 is used by sum-of-differences-rem,
nat/anti is used by in-ecs-n, delta-write,
nat/elim-sub is used by delta-write, delta-atomic-leb-change,
nat/eq-01 is used by sum-of-differences-rem, in-delta, delta-write,
nat/eq-02 is used by delta-write,
nat/fle-01 is used by in-ecs-n, ecs-n-write,
nat/ge is used by sum-of-differences-rem, sum-of-differences-in, in-delta, delta-atomic-leb-change,
nat/gr-def is used by delta-write, delta-atomic-leb-change,
nat/le-def is used by sum-of-differences-in, in-ecs, ecs-write, ecs-empty, delta-write, delta-atomic-leb-change,
nat/le-ls-simp is used by delta-write-same, delta-write, delta-atomic-leb-change,
nat/lels is used by in-ecs-n, ecs-write, ecs-n-write, delta-write-same, delta-write, delta-atomic-leb-change,
nat/lels-02 is used by ecs-n-write,
nat/lels-03 is used by in-ecs-n, ecs-n-write, delta-write,
nat/lep is used by delta-atomic-leb-change,
nat/lep-02 is used by delta-write,
nat/ler is used by in-ecs-n, in-ecs, ecs-write, ecs-n-write, delta-write,
nat/let is used by delta-write, delta-atomic-leb-change,
nat/ls-le-simp is used by in-delta, ecs-n-write, delta-write-same, delta-atomic-leb-change,
nat/prop-07 is used by delta-write,
nat/succ-01 is used by in-ecs-n, ecs-n-write, ecs-n-empty,
nat/zero is used by delta-write,

Used from specification error-class

error-class/esuccess is used by delta-atomic-leb-change,
error-class/not-esuccess is used by delta-atomic-leb-change,

Used from specification bag-max

bag-max/bag-rem-notmax is used by delta-write,
bag-max/in-rec is used by sum-of-differences-in, in-ecs-n,
bag-max/bag-add-nonempty is used by ecs-n-empty,
bag-max/bag-rem-empty is used by bag-rem-eq-empty-elim,
bag-max/bag-remadd-in is used by ecs-write-same, ecs-n-write,
bag-max/max-one is used by delta-write,

Used from specification bag-basic

bag-basic/nat-bag/bag-add2-eq-elim is used by ecs-n-write,
bag-basic/nat-bag/insert-inj is used by ecs-write, ecs-n-write,

Used from specification wlarray

wlarray/elim-update-status is used by delta-atomic-leb-change,

Used from specification ubi-io-pre

ubi-io-pre/write-data-wl-pre is used by delta-atomic-leb-change,
ubi-io-pre/write-vidhdr-pre is used by delta-atomic-leb-change,

Used from specification align

align/alignup-lower-bound is used by delta-atomic-leb-change,
align/alignup-same is used by delta-atomic-leb-change,
align/alignup-same0 is used by delta-atomic-leb-change,
align/is-aligned-zero is used by delta-atomic-leb-change,

Used from specification wlentry

wlentry/elim-02 is used by in-ecs-n, ecs-write, ecs-n-write, delta-write-same, delta-write, delta-atomic-leb-change,
wlentry/inj-03 is used by in-ecs-n, ecs-n-write, delta-atomic-leb-change,
wlentry/sel-05 is used by in-ecs-n, in-ecs, ecs-write-same, ecs-n-write, delta-write, delta-atomic-leb-change,

Used from specification eraseblock

eraseblock/page-size is used by delta-atomic-leb-change,

Used from specification oelem

oelem/nat-set/irreflexivity is used by in-ecs-n, in-ecs, ecs-write, ecs-n-write, ecs-empty, delta-write,
oelem/nat-set/transitivity is used by in-ecs-n,

Used from specification array

array/wlarray-base/Put-other is used by delta-atomic-leb-change,
array/wlarray-base/Put-other is used by ecs-n-write, delta-atomic-leb-change,
array/apebs/Put-same is used by delta-atomic-leb-change,
array/wlarray-base/Put-same is used by ecs-n-write, delta-atomic-leb-change,
array/apebs/Size-put is used by delta-atomic-leb-change,
array/wlarray-base/Size-put is used by ecs-write, ecs-n-write, delta-atomic-leb-change,
array/wlarray-base/cgetput is used by delta-atomic-leb-change,
array/wlarray-base/ngp-07 is used by ecs-n-write,

Used from specification ebaentry

ebaentry/disj is used by delta-atomic-leb-change,
ebaentry/elim is used by delta-atomic-leb-change,
ebaentry/inj is used by delta-atomic-leb-change,

Used from specification ubi-asm

ubi-asm/ls-max is used by delta-write,