[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/At-other is used by compatstatic-mode, compat-put, compat-addobj,
store/javastore/At-same is used by compatstatic-mode, compat-throw-02, compat-put, compat-addobj,
store/javastore/In-insert is used by compatval-put, compatstatic-mode, compat-put, compat-addobj, compat-addclass,
store/javastore/In-store is used by compatobj-isobj,
store/javastore/insin is used by compat-throw-02,
store/javastore/notmemlookup is used by compatobj-isobj, compatarray-isarray, compat-put, compat-addclass,

Used from specification list

list/storekeys/in-empty is used by compat-addobj,

Used from specification storefuns

storefuns/init-put-03 is used by compat-addclass,
storefuns/init-put-04 is used by compat-put,
storefuns/init-mode-03 is used by compatstatic-mode,
storefuns/instore-01 is used by compatval-put, compatstatic-mode, compatrefs-mode, compatobj-isobj, compatfields-mode, compatarray-void, compatarray-mode, compatarray-isarray-01, compatarray-isarray, compatarray-abstract, compat-throw-02, compat-put, compat-newref, compat-addobj, compat-addclass,
storefuns/newref-01 is used by compat-newref, compat-addobj,
storefuns/newref-03 is used by compat-newref, compat-addobj,
storefuns/newref-in-01 is used by compat-addobj,
storefuns/refin is used by compat-put,

Used from specification valuefuns

valuefuns/initial-okval is used by compat-addclass,
valuefuns/initial-value is used by compat-addclass,
valuefuns/initial-value-01 is used by compat-addclass,
valuefuns/initial-value-02 is used by compat-addclass,
valuefuns/okval-abstract is used by compatarray-abstract,
valuefuns/okval-class is used by compat-throw-02,
valuefuns/okval-refval is used by compatval-put, compatval-addclass, compatstatic-mode, compatarray-mode, compat-throw-02, compat-addobj,
valuefuns/okval-refval-01 is used by compatval-put, compatval-addclass, compatstatic-mode,
valuefuns/okval-void is used by compatstatic-mode, compatarray-void,
valuefuns/typeval-xtra is used by compatobj-isobj, compatarray-isarray, compat-addobj,

Used from specification fieldspec

fieldspec/elim is used by compatval-put, compatstatic-mode, compatobj-isobj, compatfields-mode, compat-put, compat-addobj, compat-addclass,
fieldspec/inj is used by compatstatic-mode, compat-put, compat-addclass,
fieldspec/inj-01 is used by compatstatic-mode, compat-put, compat-addclass,
fieldspec/sel-03 is used by compatstatic-mode, compatobj-isobj, compatfields-mode, compat-put, compat-addobj, compat-addclass,

Used from specification int-abs

int-abs/forward-le-01 is used by compatarray-void, compatarray-mode, compatarray-isarray-01, compatarray-isarray, compat-put, compat-addobj, compat-addclass,
int-abs/forward-le-05 is used by compatarray-void, compatarray-mode, compatarray-isarray-01, compatarray-isarray, compatarray-abstract, compat-put, compat-addobj, compat-addclass,
int-abs/forward-lels is used by compatarray-mode,
int-abs/lels is used by compatarray-void, compatarray-mode, compatarray-isarray-01, compatarray-isarray, compatarray-abstract, compat-put, compat-addobj, compat-addclass,
int-abs/lels-01 is used by compatarray-void, compatarray-mode, compatarray-isarray-01, compatarray-isarray, compatarray-abstract, compat-put, compat-addobj, compat-addclass,
int-abs/lels-02 is used by compatarray-abstract,
int-abs/lels-03 is used by compatarray-void, compatarray-mode, compatarray-isarray-01, compatarray-isarray, compat-put, compat-addobj, compat-addclass,
int-abs/lels-04 is used by compatarray-void, compatarray-mode, compatarray-isarray-01, compatarray-isarray, compat-put, compat-addobj, compat-addclass,

Used from specification okfuns

okfuns/asgcomp is used by compatval-put, compatval-addclass, compat-throw-02, compat-addobj,
okfuns/gfts-all is used by compatobj-isobj,
okfuns/good-field-02 is used by compatobj-isobj,
okfuns/is-any-array is used by compatarray-isarray-01, compatarray-isarray,
okfuns/keys-in-01 is used by compat-addclass,
okfuns/okarrayNotNull is used by compatarray-isarray-01, compatarray-isarray,
okfuns/okreftype is used by compatarray-isarray,
okfuns/asgcomp is used by compatval-put, compatval-addclass, compatstatic-mode, compatfields-mode, compatarray-void, compatarray-mode, compat-throw-02, compat-addobj,
okfuns/good-field-index is used by compatobj-isobj,
okfuns/isarray-len is used by compatarray-isarray-01,
okfuns/isarray-lenfield is used by compatarray-isarray-01,
okfuns/isarray-type is used by compatarray-isarray-01,
okfuns/keys-empty is used by compat-addclass,
okfuns/okarray-05 is used by compatarray-isarray-01,
okfuns/oktype-okval is used by compatobj-isobj, compatarray-isarray-01, compatarray-isarray,

Used from specification storekey

storekey/elim-03 is used by compatstatic-mode, compatobj-isobj, compatfields-mode, compat-addobj, compat-addclass,
storekey/inj-03 is used by compatstatic-mode, compat-put, compat-addclass,
storekey/sel-05 is used by compatobj-isobj, compat-put, compat-addclass,
storekey/test is used by compatstatic-mode, compatfields-mode, compat-put, compat-addobj, compat-addclass,
storekey/test-01 is used by compatstatic-mode, compatobj-isobj, compatfields-mode, compat-put, compat-addobj, compat-addclass,
storekey/test-02 is used by compatstatic-mode, compatobj-isobj, compatfields-mode, compat-put, compat-addobj, compat-addclass,
storekey/test-05 is used by compatstatic-mode, compatobj-isobj, compatfields-mode, compat-addobj, compat-addclass,
storekey/test-07 is used by compat-put, compat-addclass,
storekey/test-08 is used by compat-addclass,

Used from specification fieldname

fieldname/inj is used by compat-addclass,

Used from specification typefuns

typefuns/is_subtype-level is used by compatarray-void, compat-throw-02, compat-addobj,
typefuns/tdnameex-def is used by compatstatic-mode, compat-put, compat-addobj, compat-addclass,
typefuns/elemtype-04 is used by compat-throw-02, compat-addobj,
typefuns/elemtype-rec is used by compatrefs-mode, compat-put, compat-addobj, compat-addclass,
typefuns/hasclass-no is used by compat-addobj,
typefuns/hasclasstype is used by compat-newref, compat-addobj,
typefuns/hasct-04 is used by compat-throw-02, compat-addobj,
typefuns/hasct-05 is used by compat-put, compat-addobj, compat-addclass,
typefuns/hasct-06 is used by compatarray-void,
typefuns/isreftype-04 is used by compat-throw-02, compat-addobj,
typefuns/isreftype-06 is used by compatarray-void, compat-addobj,
typefuns/jtclass is used by compatarray-void, compat-throw-02, compat-addobj,
typefuns/le-11 is used by compatarray-void,
typefuns/le-noreftype is used by compat-addobj,
typefuns/le-noreftype-01 is used by compat-addobj,
typefuns/ref is used by compatarray-isarray,
typefuns/subarray1 is used by compatarray-isarray,
typefuns/subclass is used by compat-throw-02,
typefuns/tdname+ex-def is used by compatval-put, compatval-addclass, compatstatic-mode, compatrefs-mode, compatfields-mode, compatarray-mode, compat-throw-02, compat-put, compat-addobj, compat-addclass,
typefuns/tdname+predef-02 is used by compat-throw-02, compat-addobj,
typefuns/tdnameex-def is used by compatval-put, compatval-addclass, compatstatic-mode, compatrefs-mode, compatfields-mode, compatarray-mode, compat-throw-02, compat-put, compat-addobj, compat-addclass,
typefuns/transitivity is used by compat-addobj,

Used from specification int-basic1

int-basic1/ls-01 is used by compatarray-abstract,

Used from specification refkey

refkey/elim is used by compat-addclass,
refkey/inj is used by compat-put, compat-addobj,
refkey/inj-01 is used by compatval-put, compat-put, compat-addobj, compat-addclass,

Used from specification javatype

javatype/diff is used by compat-put, compat-addobj, compat-addclass,
javatype/diff-01 is used by compatrefs-mode, compat-put, compat-addobj, compat-addclass,
javatype/disj-02 is used by compat-addclass,
javatype/disj-09 is used by compatobj-isobj, compat-throw-02,
javatype/disj-22 is used by compatarray-isarray,
javatype/elim-01 is used by compatarray-mode, compatarray-isarray-01, compatarray-isarray, compat-put, compat-addobj, compat-addclass,
javatype/elim-02 is used by compatobj-mode, compatobj-isobj, compat-put, compat-addobj, compat-addclass,
javatype/sel-01 is used by compatarray-void, compatarray-isarray-01, compatarray-isarray, compatarray-abstract, compat-put, compat-addobj, compat-addclass,
javatype/sel-02 is used by compatobj-isobj, compat-throw-02, compat-put, compat-addobj, compat-addclass,
javatype/test-09 is used by compatarray-void, compatarray-mode, compatarray-isarray-01, compatarray-isarray, compatarray-abstract, compat-put, compat-addobj, compat-addclass,
javatype/test-10 is used by compatobj-mode, compatobj-isobj, compat-put, compat-addobj, compat-addclass,
javatype/test-28 is used by compat-addobj,

Used from specification javavalue

javavalue/diff is used by compat-put, compat-addobj, compat-addclass,
javavalue/diff-01 is used by compat-put, compat-addobj,
javavalue/disj-41 is used by compat-put, compat-addclass,
javavalue/disj-46 is used by compat-throw-02, compat-put, compat-addobj,
javavalue/disj-53 is used by compat-throw-02, compat-put, compat-addobj,
javavalue/disj-54 is used by compat-addobj,
javavalue/elim-02 is used by compatarray-void, compatarray-mode, compatarray-isarray-01, compatarray-isarray, compatarray-abstract, compat-put, compat-addobj, compat-addclass,
javavalue/elim-10 is used by compatval-put, compatval-addclass, compatrefs-mode, compatobj-isobj, compatarray-void, compatarray-isarray-01, compatarray-isarray, compat-throw-02, compat-put, compat-addobj, compat-addclass,
javavalue/elim-11 is used by compat-addobj,
javavalue/elim-12 is used by compat-put, compat-addobj,
javavalue/elim-13 is used by compatval-put, compatval-addclass, compatstatic-mode, compatarray-void, compatarray-mode, compat-addobj,
javavalue/inj-03 is used by compatarray-void,
javavalue/inj-09 is used by compat-addobj,
javavalue/sel-04 is used by compatarray-isarray,
javavalue/sel-09 is used by compatval-put, compatval-addclass, compatstatic-mode, compatarray-mode, compatarray-isarray, compat-throw-02, compat-newref, compat-addobj, compat-addclass,
javavalue/sel-11 is used by compatval-put, compatval-addclass, compatrefs-mode, compatarray-isarray, compat-throw-02, compat-put, compat-addobj, compat-addclass,
javavalue/sel-14 is used by compat-throw-02,
javavalue/sel-15 is used by compat-throw-02,
javavalue/test-113 is used by compat-addobj,
javavalue/test-114 is used by compat-throw-02,
javavalue/test-117 is used by compat-addobj,
javavalue/test-118 is used by compat-throw-02,
javavalue/test-119 is used by compat-addobj,
javavalue/test-120 is used by compat-throw-02, compat-put, compat-addobj,
javavalue/test-19 is used by compatval-put, compatval-addclass, compatstatic-mode, compatarray-void, compatarray-mode, compatarray-isarray, compat-throw-02, compat-newref, compat-addobj,
javavalue/test-25 is used by compatarray-void, compatarray-mode, compatarray-isarray-01, compatarray-isarray, compatarray-abstract, compat-put, compat-addobj, compat-addclass,
javavalue/test-91 is used by compatobj-isobj, compatarray-isarray,
javavalue/test-92 is used by compatval-put, compatval-addclass, compatrefs-mode, compatobj-isobj, compatarray-void, compatarray-isarray-01, compatarray-isarray, compat-throw-02, compat-put, compat-addobj, compat-addclass,

Used from specification storearrays

storearrays/arrayref is used by compat-put,
storearrays/is_arrayref-02 is used by compatarray-mode,

Used from specification specialkeys

specialkeys/mode-01 is used by compatstatic-mode,
specialkeys/mode-02 is used by compatstatic-mode, compat-addclass,
specialkeys/mode-03 is used by compat-addclass,
specialkeys/mode-neq is used by compat-put,
specialkeys/type-neq is used by compatval-put, compat-put,
specialkeys/uninit-02 is used by compat-put,
specialkeys/uninit-eq is used by compat-put, compat-addclass,

Used from specification storefunsx

storefunsx/lookup-xtra is used by compatobj-isobj, compatarray-isarray, compat-put, compat-addclass,

Used from specification javastore

javastore/at-other-01 is used by compat-put,
javastore/at-other-16 is used by compat-put,
javastore/at-other-20 is used by compatval-put, compat-put,
javastore/at-other-21 is used by compatstatic-mode, compatrefs-mode, compatobj-mode, compatfields-mode, compatarray-mode, compat-throw-02,
javastore/instore-02 is used by compat-put,
javastore/look-ins is used by compat-addobj,
javastore/mode is used by compatfields-mode, compatarray-mode,
javastore/type-01 is used by compatstatic-mode, compatrefs-mode, compatfields-mode, compatarray-mode, compat-throw-02,

Used from specification assoclist

assoclist/fieldinit/empty is used by compat-addobj,

Used from specification predefined

predefined/predef is used by compat-addclass,

Used from specification addfuns

addfuns/ac-init-03 is used by compat-addclass,
addfuns/ac-lookup is used by compat-addclass,
addfuns/ac-lookup-06 is used by compat-addclass,
addfuns/ac-mode-01 is used by compat-addclass,
addfuns/add-in-04 is used by compat-addobj,
addfuns/add-isarray is used by compat-addobj,
addfuns/addclass-base is used by compat-addclass,
addfuns/addobj-base is used by compat-addobj,
addfuns/is-any-object is used by compatobj-isobj,
addfuns/is_obj-def is used by compatobj-isobj,
addfuns/okfieldinits-at is used by compat-addclass,
addfuns/okfieldinits-class is used by compat-addclass,
addfuns/okfieldinits-index is used by compat-addclass,
addfuns/statfields-predef is used by compat-addclass,
addfuns/ac-in-02 is used by compat-addclass,
addfuns/ac-in-04 is used by compat-addclass,
addfuns/ac-in-06 is used by compat-addclass,
addfuns/ac-in-09 is used by compat-addclass,
addfuns/ac-isarray is used by compat-addclass,
addfuns/ac-lookup-02 is used by compat-addclass,
addfuns/ac-lookup-04 is used by compatval-addclass, compat-addclass,
addfuns/ac-refin is used by compatval-addclass, compat-addclass,
addfuns/add-at is used by compat-addobj,
addfuns/add-at-01 is used by compat-addobj,
addfuns/add-in is used by compat-addobj,
addfuns/add-in-01 is used by compat-addobj,
addfuns/add-in-03 is used by compat-addobj,
addfuns/add-init is used by compat-addobj,
addfuns/add-length is used by compat-addobj,
addfuns/add-ref is used by compat-addobj,
addfuns/add-type-01 is used by compat-addobj,
addfuns/add-type-02 is used by compat-addobj,
addfuns/addobj-mode-01 is used by compat-addobj,
addfuns/instfields-predef is used by compat-addobj,
addfuns/mode-addobj is used by compat-addobj,
addfuns/okfieldinits-empty is used by compat-addclass,
addfuns/statfields-abstract is used by compat-addclass,
addfuns/statfields-special is used by compatstatic-mode, compat-addclass,