[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/a is used by union-write-above, union-write, union-subset, in-union-ext, in-index-in-union-1, in-index-in-union, disj-write, disj-rec, disj-in-both,
nat-basic/add-base is used by union-write-above, union-write, union-subset, in-union-ext, in-index-in-union-1, in-index-in-union, disj-write, disj-rec, disj-in-both,
nat-basic/c is used by union-write-above, union-write, union-subset, in-union-ext, in-index-in-union-1, in-index-in-union, disj-write, disj-rec, disj-in-both,
nat-basic/f is used by union-write-above, union-write, union-subset, union-eq-rem-subseteq, subseteq-union-one-add, subseteq-union-one, subseteq-union-diff-one, inter-union-empty-one-empty, in-union-ext, in-index-in-union, disj-write, disj-union-rem, disj-rec, disj-in-both,
nat-basic/l is used by union-subset, in-union-ext,
nat-basic/l-01 is used by union-subset, in-union-ext,
nat-basic/lf is used by union-write,
nat-basic/lf-01 is used by union-write,
nat-basic/lf-02 is used by union-write, subseteq-union-diff-one,
nat-basic/ls-02 is used by union-write, union-subset, in-union-ext, disj-rec,
nat-basic/neq-01 is used by union-write,
nat-basic/neq-04 is used by union-write,
nat-basic/ref is used by union-write-above, union-write, union-subset, in-union-ext,
nat-basic/s-04 is used by union-write, union-subset, in-union-ext, in-index-in-union, disj-rec,
nat-basic/succ is used by union-write-above, union-write, union-subset, in-union-ext, in-index-in-union,
nat-basic/trans is used by union-write,
nat-basic/zero-01 is used by union-write, in-index-in-union,

Used from specification nat

nat/le-rec is used by in-index-in-union,
nat/anti is used by union-write, union-subset, in-union-ext, in-index-in-union-1,
nat/fle is used by union-write, subseteq-union-one-add, subseteq-union-one, inter-union-empty-one-empty, disj-write, disj-union-rem,
nat/fle-01 is used by union-subset, in-union-ext,
nat/le-ls-simp is used by union-subset, in-union-ext,
nat/lels is used by union-write, union-subset, in-union-ext, in-index-in-union-1, in-index-in-union,
nat/lels-02 is used by union-write,
nat/lels-03 is used by union-write-above, union-write,
nat/lep is used by union-subset, in-union-ext,
nat/ler is used by union-write,
nat/let is used by union-subset, in-union-ext,
nat/lez is used by union-write, in-index-in-union-1,
nat/lez-01 is used by in-index-in-union,
nat/succ-01 is used by union-write-above, union-write,

Used from specification set-union

set-union/address-list-set/Difference is used by subseteq-union-diff-one, disj-union-rem,
set-union/address-list-set/diff-union-03 is used by union-write,
set-union/address-list-set/empty-intersection-diff is used by union-write,
set-union/address-list-set/subdef is used by union-eq-rem-subseteq, subseteq-union-one, subseteq-union-diff-one,
set-union/address-list-set/unrax is used by disj-union-rem,
set-union/address-list-set/unsub-union-01 is used by union-subset,
set-union/address-list-set/Delete is used by union-eq-rem-subseteq,
set-union/address-list-set/Difference is used by disj-union-rem,
set-union/address-list-set/Intersect is used by union-write, inter-union-empty-one-empty,
set-union/address-list-set/diff-e-01 is used by union-write,
set-union/address-list-set/diff-idem is used by union-write,
set-union/address-list-set/diff-union is used by subseteq-union-diff-one,
set-union/address-list-set/int-a is used by union-write, inter-union-empty-one-empty, disj-in-both,
set-union/address-list-set/int-c is used by union-write, inter-union-empty-one-empty, disj-write, disj-in-both,
set-union/address-list-set/int-empty-02 is used by disj-in-both,
set-union/address-list-set/una is used by union-write, union-union-one, union-subset, subseteq-union-diff-one, in-union-ext, in-index-in-union-1, in-index-in-union, disj-union-rem,
set-union/address-list-set/unc is used by union-write, union-union-one, union-subset, subseteq-union-diff-one, in-union-ext, in-index-in-union-1, in-index-in-union, disj-union-rem,
set-union/address-list-set/une is used by union-write,
set-union/address-list-set/uneq is used by union-union-one,
set-union/address-list-set/unin is used by in-union-ext, disj-union-rem,
set-union/address-list-set/unin-01 is used by subseteq-union-diff-one, in-union-ext, in-index-in-union-1, in-index-in-union, disj-union-rem,

Used from specification set-basic

set-basic/address-list-set/Extension is used by union-write, union-eq-rem-subseteq, inter-union-empty-one-empty, disj-union-rem,
set-basic/address-list-set/sub-insert-01 is used by subseteq-union-one-add,
set-basic/address-list-set/In-empty is used by union-write, inter-union-empty-one-empty, in-union-ext,
set-basic/address-list-set/ne-01 is used by union-write, union-eq-rem-subseteq, subseteq-union-diff-one, inter-union-empty-one-empty, in-union-ext, in-index-in-union-1, in-index-in-union, disj-union-rem, disj-in-both,
set-basic/address-list-set/size-zero is used by union-write, inter-union-empty-one-empty, disj-write, disj-rec,
set-basic/address-list-set/size-zero-01 is used by union-write, union-eq-rem-subseteq, subseteq-union-diff-one, inter-union-empty-one-empty, in-union-ext, in-index-in-union-1, in-index-in-union, disj-write, disj-union-rem, disj-rec, disj-in-both,
set-basic/address-list-set/sub-e is used by union-subset,
set-basic/address-list-set/sub-ntrans-01 is used by union-subset,

Used from specification array

array/address-set-array/Put-other is used by union-write, disj-write,
array/address-set-array/Put-same is used by union-write, disj-write,
array/address-set-array/cngetput is used by union-write-above,