[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 ebm-order-write-same, ebm-order-trans, ebm-order-antisym, ebm-initial-imp-cons, ebm-cons-write, ebm-cons-leb-size-le, ebm-cons-leb-size,
nat-basic/lf-01 is used by ebm-order-write-same, ebm-order-trans, ebm-order-antisym,

Used from specification store

store/abstract-volumes/k-Extension is used by ebm-order-antisym,
store/abstract-volumes/At-other is used by ebm-order-write-same, ebm-cons-write,
store/abstract-volumes/At-same is used by ebm-order-write-same, ebm-cons-write,
store/abstract-volumes/In-empty is used by ebm-initial-imp-cons,
store/abstract-volumes/in-neq is used by ebm-order-write-same, ebm-cons-write,
store/abstract-volumes/insin is used by ebm-order-write-same, ebm-cons-write,

Used from specification nat

nat/fle-01 is used by ebm-order-write-same,
nat/le-def is used by ebm-cons-leb-size-le,
nat/le-ls-simp is used by ebm-order-write-same,
nat/lels is used by ebm-order-write-same,
nat/ls-le-simp is used by ebm-cons-leb-size-le,

Used from specification leb

leb/disj is used by ebm-order-antisym,
leb/disj-01 is used by ebm-order-antisym,
leb/disj-02 is used by ebm-order-write-same, ebm-order-antisym,
leb/elim is used by ebm-cons-write,
leb/sel is used by ebm-cons-write, ebm-cons-leb-size-le, ebm-cons-leb-size,
leb/sel-01 is used by ebm-cons-write, ebm-cons-leb-size-le,
leb/test-03 is used by ebm-order-antisym, ebm-cons-write, ebm-cons-leb-size-le, ebm-cons-leb-size,

Used from specification array

array/abstract-volume/Extension is used by ebm-order-antisym,
array/abstract-volume/Put-other is used by ebm-order-write-same, ebm-cons-write,
array/abstract-volume/Put-same is used by ebm-order-write-same, ebm-cons-write,
array/abstract-volume/Size-put is used by ebm-order-write-same, ebm-cons-write,
array/abstract-volume/cgetput is used by ebm-order-write-same,
array/abstract-volume/cngetput is used by ebm-order-write-same,