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

lebref/disj is used by rm-v-subseteq, lebrefs-lref, in-rm-v-same, in-rm-v-in, in-rm-v, eq-entry-in-lref-in,
lebref/elim is used by rm-v-subseteq, in-rm-v-same, in-rm-v-in, in-rm-v,
lebref/inj is used by in-rm-v-same,

Used from specification list-set

list-set/erasequeue-base/subset is used by rm-v-subseteq,
list-set/erasequeue-base/sub-in is used by in-vl-subset,
list-set/erasequeue-base/subset-empty is used by subseteq-lebrefs-subseteq,
list-set/erasequeue-base/subset-rec is used by subseteq-lebrefs-subseteq,

Used from specification nat-basic

nat-basic/a is used by in-vl-in-lebrefs,
nat-basic/c is used by in-vl-in-lebrefs,
nat-basic/oz is used by in-vl-in-lebrefs,

Used from specification set-union

set-union/lebrefset/One is used by subseteq-lebrefs-subseteq, lebrefs-lref, lebrefs-append-none, lebrefs-append-lref, in-vl-in-lebrefs,
set-union/lebrefset/Union is used by in-vl-in-lebrefs,
set-union/lebrefset/una is used by subseteq-lebrefs-subseteq, lebrefs-none, lebrefs-lref, lebrefs-append-none, lebrefs-append-lref, in-vl-in-lebrefs,
set-union/lebrefset/unadd is used by subseteq-lebrefs-subseteq, lebrefs-lref, lebrefs-append-none, lebrefs-append-lref, in-vl-in-lebrefs,
set-union/lebrefset/unc is used by subseteq-lebrefs-subseteq, lebrefs-none, lebrefs-lref, lebrefs-append-none, lebrefs-append-lref, in-vl-in-lebrefs,
set-union/lebrefset/une is used by subseteq-lebrefs-subseteq, lebrefs-none, lebrefs-lref, lebrefs-append-none, lebrefs-append-lref, in-vl-in-lebrefs,

Used from specification set-basic

set-basic/lebrefset/In-empty is used by in-vl-in-lebrefs,
set-basic/lebrefset/In-insert is used by in-vl-in-lebrefs,
set-basic/lebrefset/Size-insert is used by in-vl-in-lebrefs,
set-basic/lebrefset/eq-04 is used by lebrefs-append-lref,
set-basic/lebrefset/in-04 is used by in-vl-in-lebrefs,
set-basic/lebrefset/ne is used by in-vl-in-lebrefs,
set-basic/lebrefset/ne-01 is used by in-vl-in-lebrefs,
set-basic/lebrefset/size-zero is used by lebrefs-none, in-vl-in-lebrefs,
set-basic/lebrefset/size-zero-01 is used by lebrefs-none, in-vl-in-lebrefs,
set-basic/lebrefset/sub-add-03 is used by subseteq-lebrefs-subseteq,
set-basic/lebrefset/sub-e is used by subseteq-lebrefs-subseteq,

Used from specification erasequeueentry

erasequeueentry/elim is used by subseteq-lebrefs-subseteq, rm-vl-notin-before, rm-vl-in-before-h, rm-vl-in-before, rm-vl-append-same, rm-v-subseteq, lebrefs-append-none, lebrefs-append-lref, in-vl-in-lebrefs, in-rm-v-same, in-rm-v-in, in-rm-v, in-prepend-other, in-prepend, in-concat, in-append-other, in-append,
erasequeueentry/inj is used by rm-vl-notin-before, rm-vl-in-before-h, rm-vl-in-before, in-vl-in-lebrefs, in-vl-append0, in-vl-append, in-rm-v-same, in-rm-v, in-prepend-vl,
erasequeueentry/sel-01 is used by rm-vl-append-same, lebrefs-none, lebrefs-lref,
erasequeueentry/sel-02 is used by in-single, in-rm-v, in-prepend-other, in-prepend, in-concat, in-append-other, in-append,

Used from specification list

list/erasequeue-base/One is used by rm-vl-append-same, lebrefs-none, lebrefs-lref,
list/erasequeue-base/c is used by rm-vl-append-same, lebrefs-none, lebrefs-lref,
list/erasequeue-base/Nil is used by rm-vl-append-same, lebrefs-append-none, lebrefs-append-lref,
list/erasequeue-base/a is used by subseteq-lebrefs-subseteq, rm-vl-notin-before, rm-vl-in-before-h, rm-vl-in-before, rm-vl-append-same, rm-v-subseteq, lebrefs-append-none, lebrefs-append-lref, in-vl-in-lebrefs, in-vl-append0, in-vl-append, in-rm-v-same, in-rm-v-in, in-rm-v, in-prepend-vl, in-prepend-other, in-prepend, in-concat, in-append-other, in-append,
list/erasequeue-base/app-08 is used by rm-vl-append-same,
list/erasequeue-base/c is used by subseteq-lebrefs-subseteq, rm-vl-notin-before, rm-vl-in-before-h, rm-vl-in-before, rm-vl-append-same, rm-v-subseteq, lebrefs-append-none, lebrefs-append-lref, in-vl-in-lebrefs, in-rm-v-same, in-rm-v-in, in-rm-v,
list/erasequeue-base/in-01 is used by rm-v-subseteq,
list/erasequeue-base/in-06 is used by rm-v-subseteq,
list/erasequeue-base/in-17 is used by in-vl-append0, in-vl-append, in-single, in-append-other, in-append,
list/erasequeue-base/in-append is used by in-vl-append0, in-vl-append, in-concat, in-append-other, in-append,
list/erasequeue-base/in-empty is used by rm-vl-notin-before, rm-vl-in-before-h, rm-vl-in-before, rm-v-subseteq, in-vl-in-lebrefs, in-rm-v-same, in-rm-v-in, in-rm-v, in-empty-vl, in-empty,
list/erasequeue-base/in-rec is used by rm-vl-notin-before, rm-vl-in-before-h, rm-vl-in-before, in-vl-in-lebrefs, in-rm-v-same, in-rm-v-in, in-rm-v, in-prepend-vl, in-prepend-other, in-prepend,