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

store/javastore/Del-at is used by subset-size, onlymod-del,
store/javastore/Extension is used by union-empty-01, subset-is-union, refs-empty-01, eqex-tput, eqex-mode, eqex-at,
store/javastore/In-insert is used by onlymod-put-01, eqex-tput,
store/javastore/Subset is used by union-subset-left, union-subset, subset-size, subset-is-union, refs-equal,
store/javastore/ins is used by subset-is-union,
store/javastore/notmemlookup is used by eqex-tput,
store/javastore/subset-put-01 is used by subset-size,
store/javastore/subset-put-02 is used by subset-size, subset-is-union,
store/javastore/At-same is used by exception-03,
store/javastore/Del-at is used by subset-size, subset-is-union, onlymod-del,
store/javastore/Del-in is used by subset-size, subset-is-union, onlymod-del,
store/javastore/In-empty is used by union-empty-01, union-def, union-at-right-01, refs-empty-01,
store/javastore/In-insert is used by union-def, union-at-right-01, union-at-left, subset-is-union, onlymod-shift, onlymod-put-01, onlymod-put, eqex-tput, classof-01, classof,
store/javastore/In-store is used by union-init-01, union-init, union-in, union-def, subset-size, subset-is-union, onlymod-init-02, onlymod-init-01, eq-mod,
store/javastore/del-notin is used by subset-size, subset-is-union,
store/javastore/in-pair is used by union-init-01, union-init, union-in, union-def, subset-size, onlymod-init-02, onlymod-init-01, eq-mod,
store/javastore/insin is used by union-def, eqex-tput, classof,
store/javastore/insins is used by subset-is-union,
store/javastore/lookupisempty is used by subset-size, onlymod-del,
store/javastore/notmemlookup is used by union-at-right-02, subset-size, subset-is-union, refs-empty-01, onlymod-type, onlymod-length, eqex-tput, eqex-at, classof-01,
store/javastore/subset-empty is used by subset-is-union, refs-equal,

Used from specification list

list/classnames/a is used by initdone-rec,
list/classnames/in-06 is used by initdone-rec,
list/classnames/in-17 is used by initdone-one,
list/classnames/in-empty is used by initdone-empty,

Used from specification storefuns

storefuns/delete-at is used by refs-equal,
storefuns/init-04 is used by union-init-02,
storefuns/init-05 is used by nouninit-put-statfield, nouninit-put-03, nouninit-put-01, nouninit-put,
storefuns/init-existing is used by union-init-03,
storefuns/init-put-04 is used by init-set,
storefuns/initdone is used by union-init, onlymod-init, eq-mod,
storefuns/initerror is used by union-init, onlymod-init-02, eq-mod,
storefuns/initundone is used by union-init-01, onlymod-init-01, eq-mod,
storefuns/instore is used by union-in-01,
storefuns/look-del is used by eqex-tput,
storefuns/newref-def is used by union-newref-02, union-newref-01, union-newref,
storefuns/newref-same is used by newref-same,
storefuns/refin-del is used by refs-equal, refs-del,
storefuns/subset-delete is used by subset-size,
storefuns/uninit is used by uninit-uninit,
storefuns/del-notin is used by refs-del,
storefuns/del-notin-01 is used by refs-equal,
storefuns/in-del is used by refs-equal, eqex-tput, eqex-at,
storefuns/in-empty is used by refs-equal, refs-empty,
storefuns/init-done is used by init-set,
storefuns/init-mode-04 is used by nouninit-mode-01, nouninit-mode,
storefuns/init-put-01 is used by nouninit-put-02,
storefuns/init-put-11 is used by nouninit-put-01, nouninit-put,
storefuns/initdone-05 is used by union-init-02,
storefuns/instore-01 is used by union-subset-left, union-init-01, union-init, union-in-01, subset-size, refs-notin, onlymod-shift, onlymod-put-01, onlymod-put, onlymod-init-02, onlymod-init-01, eqex-tput, classof-02,
storefuns/instore-02 is used by reftype-put, reftype-int-02, reftype-04, reftype-03, refs-put,
storefuns/look-del is used by eqex-tput, eqex-at,
storefuns/mode-01 is used by reftype-mode,
storefuns/mode-del is used by eqex-mode,
storefuns/mode-notin is used by mode-notin,
storefuns/newref-01 is used by union-newref-01, union-newref, eqmode-length, eqmode-01, eq-mod,
storefuns/newref-03 is used by union-newref-02,
storefuns/ref-in is used by reftype-out,
storefuns/subset-notin is used by refs-equal,

Used from specification fieldspec

fieldspec/inj is used by nouninit-put-statfield, nouninit-put-03, nouninit-put-01, nouninit-put, init-set, eq-mod,
fieldspec/inj-01 is used by nouninit-put-statfield, nouninit-put-03, nouninit-put-01, nouninit-put, init-set,

Used from specification ostore

ostore/javastore/Keys is used by union-at-right, subset-is-union,
ostore/javastore/del-01 is used by subset-is-union,
ostore/javastore/empty is used by union-keys, subset-is-union,
ostore/javastore/insert-03 is used by union-keys, subset-is-union,
ostore/javastore/notempty is used by union-at-right, subset-is-union,

Used from specification storekey

storekey/inj-03 is used by nouninit-put-statfield, nouninit-put-03, nouninit-put-01, nouninit-put, init-set, eq-mod,

Used from specification fieldname

fieldname/inj is used by nouninit-put-01, nouninit-put, init-set, eq-mod,

Used from specification nat-basic1

nat-basic1/f is used by subset-size,
nat-basic1/less-1 is used by subset-size,
nat-basic1/one-01 is used by subset-size,

Used from specification int-basic1

int-basic1/irref is used by eqmode-length,

Used from specification set-basic

set-basic/references/Size-insert is used by subset-size,
set-basic/references/sel is used by refs-equal,
set-basic/classnames/In-empty is used by uninit-empty, nouninit-empty,
set-basic/javastore/In-empty is used by subset-is-union,
set-basic/references/In-empty is used by refs-empty-01, refs-empty,
set-basic/classnames/In-insert is used by uninit-rec,
set-basic/javastore/In-insert is used by subset-is-union,
set-basic/references/In-insert is used by refs-put,
set-basic/references/Size-empty is used by subset-size, refs-equal,
set-basic/references/eq is used by subset-size,
set-basic/classnames/in-04 is used by uninit-one, initerror-one, init-one,
set-basic/javastore/ne-01 is used by union-at-right, subset-is-union,
set-basic/classnames/ne-01 is used by uninit-uninit, uninit-rec, nouninit-undone, nouninit-put-statfield, nouninit-put-03, nouninit-put-02, nouninit-put-01, nouninit-put, nouninit-mode-01, init-set,
set-basic/references/ne-01 is used by subset-size, refs-put, refs-equal-in, refs-equal, mode-notin-02, instore-inrefs-02,
set-basic/javastore/size-zero is used by subset-is-union,
set-basic/references/size-zero is used by refs-empty,
set-basic/classnames/size-zero-01 is used by uninit-uninit, uninit-rec, nouninit-undone, nouninit-put-statfield, nouninit-put-03, nouninit-put-02, nouninit-put-01, nouninit-put, nouninit-mode-01, init-set,
set-basic/javastore/size-zero-01 is used by subset-is-union,
set-basic/references/size-zero-01 is used by refs-put, refs-empty, mode-notin-02,
set-basic/references/size-zero-02 is used by subset-size, refs-equal,

Used from specification refkey

refkey/elim is used by subset-size, reftype-out, refs-put, refs-equal, refs-empty-01, onlymod-shift, eqex-at,
refkey/inj is used by onlymod-shift, onlymod-put-01, nouninit-put-statfield, nouninit-put-03, nouninit-put-01, nouninit-put, init-set, eqmode-length, eqex-tput, classof-01,
refkey/inj-01 is used by onlymod-shift, onlymod-put, nouninit-put-statfield, nouninit-put-03, nouninit-put-01, nouninit-put, init-set, eqex-tput, classof-01,
refkey/sel-01 is used by subset-size,

Used from specification javatype

javatype/inj-02 is used by exception-01, eq-mod, classof-03,

Used from specification javavalue

javavalue/elim-12 is used by eq-mod,
javavalue/elim-refval is used by reftype-out, reftype-01,
javavalue/inj-09 is used by classof,
javavalue/inj-11 is used by eq-mod,
javavalue/inj-12 is used by nouninit-put-01, nouninit-put,
javavalue/sel-09 is used by reftype-out, reftype-jvmref, reftype-int-02, reftype-03, reftype-02,
javavalue/sel-11 is used by classof-03,
javavalue/sel-15 is used by exception-03, exception-01,
javavalue/test-120 is used by exception-03, exception-01, eq-mod,
javavalue/test-19 is used by reftype-out, reftype-jvmref, reftype-int-02, reftype-03, reftype-02,
javavalue/test-77 is used by exception-02,

Used from specification specialkeys

specialkeys/mode is used by onlymod-mode, eqex-mode,
specialkeys/out is used by reftype-out,
specialkeys/uninit is used by union-init-01,
specialkeys/diff-01 is used by classof-05,
specialkeys/mode-01 is used by onlymod-mode, eqex-mode,
specialkeys/mode-02 is used by eq-mod,
specialkeys/mode-05 is used by eqmode-length,
specialkeys/out-01 is used by reftype-out,
specialkeys/out-02 is used by reftype-out,
specialkeys/type-04 is used by onlymod-shift, eqmode-length,
specialkeys/uninit-02 is used by nouninit-put-03,
specialkeys/uninit-eq is used by nouninit-put-statfield, nouninit-put-01, nouninit-put, init-set,

Used from specification javastore

javastore/in-01 is used by classof-07,
javastore/init-in is used by eq-mod,
javastore/init-in-01 is used by eq-mod,
javastore/look-ins is used by onlymod-put-01, onlymod-put, eq-mod, classof-07,
javastore/look-type is used by classof-04,
javastore/lookup-if is used by union-def, union-at-right-01, union-at-left, subset-is-union, onlymod-shift, onlymod-put-01, onlymod-put, exception-01, eqmode-length, eqex-tput, eq-mod, classof-05, classof-01, classof,
javastore/type-01 is used by classof-05,
javastore/typeout is used by classof-04,
javastore/uninit-mod is used by eq-mod,
javastore/uninit-type is used by eq-mod,

Used from specification nat

nat/le-ls-simp is used by subset-size,
nat/lels is used by subset-size, refs-equal,
nat/lels-01 is used by subset-size,
nat/lels-03 is used by subset-size,
nat/leprf is used by refs-equal,
nat/let is used by subset-size,
nat/ls-01 is used by subset-size,
nat/ls-le-simp is used by subset-size,

Used from specification nat-basic2

nat-basic2/a is used by subset-size,
nat-basic2/c is used by subset-size,
nat-basic2/s is used by subset-size,

Used from specification initstate

initstate/disj-02 is used by nouninit-put,
initstate/disj-03 is used by nouninit-put-01,

Used from specification set-union

set-union/references/del-size is used by subset-size, refs-equal,
set-union/references/ext is used by union-refs, refs-put, refs-empty-01, refs-empty, refs-del, newref-same,
set-union/javastore/ext is used by subset-is-union,
set-union/references/int-empty-01 is used by union-subset-left,
set-union/javastore/Delete is used by subset-is-union,
set-union/javastore/Intersect is used by subset-is-union,
set-union/references/Union is used by union-refs,
set-union/references/del-in is used by subset-size, refs-equal,
set-union/references/del-rax is used by refs-del,
set-union/references/del-size is used by refs-equal,
set-union/javastore/int-a is used by subset-is-union,
set-union/javastore/int-c is used by subset-is-union,
set-union/javastore/int-e is used by subset-is-union,
set-union/javastore/int-empty-02 is used by subset-is-union,
set-union/javastore/int-ins is used by subset-is-union,
set-union/javastore/intdel-empty is used by subset-is-union,
set-union/references/size-del-leq is used by subset-size,
set-union/references/una is used by union-refs,
set-union/javastore/una is used by union-keys,
set-union/javastore/unadd is used by union-keys,
set-union/references/unc is used by union-refs,
set-union/javastore/unc is used by union-keys,
set-union/javastore/une is used by union-keys,