[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 isobj-put-samefield-01, isobj-put-03, addobj-at-01, add-field-same-02, add-field-same,
store/javastore/Extension is used by del-addobj, addobj-union-rew, addobj-union, addobj-delsw, addobj-addobj-switch, addobj-addclass-sw, addclass-union-sw, add-putbar-rew, add-dupput,
store/javastore/In-insert is used by addobj-in-02, ac-in,
store/javastore/Subset is used by stsubset-addobj, isobj-subset, addobj-subset,
store/javastore/notmemlookup is used by del-addobj, addobj-delsw, addclass-union-sw,
store/javastore/rew is used by ao-put, addobj-out-put, addclass-switch-01, addclass-switch, add-put-02, add-nput-02, add-nput-01, add-nput, add-gins, ac-shift-03, ac-shift-02, ac-shift, ac-out, ac-del-01, ac-del,
store/javastore/subset-delete is used by addobj-throw-subset,
store/javastore/subset-put-01 is used by addobj-throw-subset,
store/javastore/superset-elem-eq is used by is_obj-subset,
store/javastore/At-same is used by isobj-put-samefield-01, isobj-put-03, is_obj-put-statfield, is_obj-put-equiv, addobj-at-this-01, addobj-at-this, add-put-06, add-put-05,
store/javastore/In-insert is used by isobj-put-03, isobj-put-02, instore-addobj, addobj-in-02, add-in-08, add-in-06, add-in-03, ac-refin, ac-init-01, ac-init, ac-in-11, ac-in-10, ac-in,
store/javastore/In-store is used by isobj-update-01, isobj-union-01, isobj-union, isobj-typele, isobj-typein, isobj-type-04, isobj-type-03, isobj-type-01, isobj-subset, isobj-rec, isobj-putref, isobj-putbar-01, isobj-putbar, isobj-put-samefield-02, isobj-put-samefield-01, isobj-put-index-01, isobj-put-badfield, isobj-put-03, isobj-put-01, isobj-put, isobj-notin-04, isobj-notin-02, isobj-notin-01, isobj-notin, isobj-newref-01, isobj-newref, isobj-isobj, isobj-fieldtype, isobj-field-in, isobj-del-02, isobj-del-01, isobj-del, isobj-all, isobj-addobj-03, isobj-addobj-01, isobj-addobj, isobj-addclass, is_valid_ref-02, is_obj-putba, is_obj-notin-01, is_obj-no-refval-01, is_obj-no-refval, is_obj-full-expand, is_obj-field-norefval, is_obj-field-noreftype, instore-addobj-rec, exactarray-addobj, ao-init-02, ao-init-01, addobj-throw-subset, addobj-initundone, addobj-initerror, addclass-exactarray, add-okarray-05, add-okarray, add-in-07, ac-okarray-01, ac-okarray, ac-init-05, ac-init-04, ac-init-02, ac-init-01, ac-init, ac-in-07, ac-in-05,
store/javastore/in-pair is used by isobj-update-01, isobj-union-01, isobj-rec, isobj-putref, isobj-putbar-01, isobj-put-samefield-02, isobj-put-samefield-01, isobj-put-index-01, isobj-put-badfield, isobj-put-03, isobj-del-01, isobj-del, isobj-all, isobj-addobj-03, isobj-addobj-01, isobj-addobj, isobj-addclass, instore-addobj-rec, instore-addobj, exactarray-addobj, addobj-initundone, addclass-exactarray, add-type-04, add-in-07, ac-okarray, ac-init-02, ac-init-01, ac-in-07, ac-in-05,
store/javastore/ins3 is used by add-put-02,
store/javastore/insin is used by isobj-put-samefield-01,
store/javastore/insins is used by add-put-01, add-put, add-gins, ac-shift-03, ac-shift-02, ac-dups-04, ac-dups-02, ac-del-03, ac-del-02, ac-del-01, ac-del,
store/javastore/notmemlookup is used by stsubset-addobj, isobj-putbar, isobj-addclass, is_obj-union, is_obj-type, is_obj-subset, ao-init-01, addclass-union-sw, addclass-okarray, addclass-exactarray, ac-okreftype, ac-okclass, ac-okarray-01, ac-okarray, ac-class,
store/javastore/sub-ref is used by addobj-throw-subset,
store/javastore/superset-elem-in-01 is used by isobj-subset,

Used from specification list

list/fieldinit-assoclista/Nil is used by add-nput-02, add-nput-01, ac-dups-03, ac-dups-02, ac-del-01, ac-del, ac-bad-03, ac-bad-02, ac-bad-01, ac-bad,
list/javavalues/a is used by addobj-getarray-01,
list/fieldinit-assoclista/a is used by validfieldinits-rec, okfieldinits-one, okfieldinits-index, okfieldinits-class, okfieldinits-at, okfieldinits-abstract, okarray-addobj, newref-addobj, instore-addobj, haskeys-addobj, getByteArray-addobject-01, getByteArray-addobject, ao-put, addobj-rec-01, addobj-at-other-03, addclass-switch-01, addclass-switch, addclass-no, add-update-same, add-type, add-tput, add-ref, add-put-02, add-put-01, add-one, add-nput-02, add-nput-01, add-nput, add-notin, add-isarray, add-in-09, add-in-08, add-in-06, add-in-04, add-in-03, add-in-02, add-gput, add-gins-01, add-gins, add-field-same-02, add-field-same-01, add-field-same, add-field-if, add-field-02, add-field, add-dupput, ac-type, ac-shift-03, ac-shift-02, ac-shift-01, ac-shift, ac-refs, ac-refin, ac-out, ac-one3, ac-one2, ac-one1, ac-no2, ac-no1, ac-new, ac-mode-01, ac-mode, ac-lookup-06, ac-lookup-05, ac-lookup-04, ac-lookup-03, ac-lookup-02, ac-lookup, ac-isarray, ac-init-11, ac-init-10, ac-init-09, ac-init-08, ac-init-07, ac-init-06, ac-init-02, ac-init-01, ac-init, ac-in-11, ac-in-10, ac-in-09, ac-in-08, ac-in-06, ac-in-03-02, ac-in-03, ac-in-02, ac-in, ac-getbar, ac-dups-05, ac-dups-04, ac-dups-03, ac-dups-02, ac-dups-01, ac-dups, ac-del-02, ac-del-01, ac-del, ac-bad-03, ac-bad-02, ac-bad-01, ac-bad,
list/storekeys/a is used by okfieldinits-index, okfieldinits-class, isobj-rec, is_obj-arraytype-01, addobj-keys-one, addobj-in-02, addobj-at-other-02, addobj-at-01, add-put-03,
list/storekeys/app is used by addobj-keys-one,
list/fieldinit-assoclista/app is used by okfieldinits-one, add-update-same, add-one, ac-one3, ac-one2, ac-one1,
list/javavalues/app-01 is used by addobj-getarray-01,
list/storekeys/app-02-ant is used by addobj-at-other-02,
list/fieldinit-assoclista/c is used by okfieldinits-index, okfieldinits-class, okfieldinits-at, okfieldinits-abstract, okarray-addobj, newref-addobj, instore-addobj-rec, instore-addobj, haskeys-addobj, getByteArray-addobject-01, getByteArray-addobject, ao-put, addobj-union-switch, addobj-at-other-03, addclass-update-sw, addclass-switch-01, addclass-switch, add-update-same, add-type, add-ref, add-nput-02, add-nput-01, add-nput, add-notin, add-isarray, add-in-09, add-in-08, add-in-06, add-in-04, add-in-03, add-in-02, add-gins, ac-type, ac-shift-03, ac-shift-02, ac-shift-01, ac-shift, ac-refs, ac-refin, ac-out, ac-new, ac-mode-01, ac-mode, ac-lookup-06, ac-lookup-05, ac-lookup-04, ac-lookup-03, ac-lookup-02, ac-lookup, ac-isarray, ac-init-02, ac-init-01, ac-init, ac-in-11, ac-in-10, ac-in-09, ac-in-08, ac-in-06, ac-in-03-02, ac-in-03, ac-in-02, ac-in, ac-getbar, ac-dups-03, ac-dups-02, ac-dups-01, ac-dups, ac-del-01, ac-del, ac-bad-03, ac-bad-02, ac-bad-01, ac-bad,
list/storekeys/c is used by addobj-in-02, addobj-at-01,
list/storekeys/e is used by addobj-at-other-02, addobj-at-other-01, add-put-06,
list/fieldinit-assoclista/in-06 is used by validfieldinits-rec,
list/storekeys/in-06 is used by isobj-rec, addobj-in-02, addobj-at-01,
list/fieldinit-assoclista/in-17 is used by validfieldinits-one,
list/storekeys/in-17 is used by okfieldinits-index, okfieldinits-class,
list/storekeys/in-append is used by okfieldinits-index, okfieldinits-class,
list/storekeys/in-empty is used by okfieldinits-index, okfieldinits-class, is_valid_ref-field-in, addobj-in-02, addobj-at-01,
list/fieldinit-assoclista/in-empty is used by validfieldinits-empty,

Used from specification storefuns

storefuns/deleteref is used by del-addobj,
storefuns/init-04 is used by addobj-init,
storefuns/init-existing is used by addobj-init-02,
storefuns/initdone is used by ao-init, addobj-initdone, ac-init-11, ac-init-08, ac-init-03, ac-init,
storefuns/initerror is used by ao-init-02, addobj-initerror, ac-init-09, ac-init-06, ac-init-05, ac-init-02, ac-init,
storefuns/initundone is used by ao-init-01, addobj-initundone, ac-init-10, ac-init-07, ac-init-04, ac-init-01, ac-init,
storefuns/instore-02 is used by add-in-02,
storefuns/list_ok is used by ac-newrefs,
storefuns/look-del is used by del-addobj, addobj-delsw,
storefuns/lookup-rec is used by addobj-at-this-01,
storefuns/lookup-rec-01 is used by addobj-at-other,
storefuns/lookup-staticfield is used by addobj-at-null,
storefuns/lookup-two is used by isobj-arraytype-01, addobj-at-this,
storefuns/newref-def is used by new-add,
storefuns/newref-same is used by newref-addobj-in,
storefuns/put-rec is used by add-put-05,
storefuns/put-rec-01 is used by add-put-06, add-put-04,
storefuns/in-del is used by isobj-notin-02, isobj-del-04, isobj-del-03, isobj-del-02, isobj-del-01, isobj-del, del-addobj, addobj-delsw,
storefuns/init-02 is used by ao-init, addobj-initdone, ac-init-03,
storefuns/init-03 is used by ao-init, addobj-initdone, ac-init-03,
storefuns/init-error is used by add-initerror-01, add-initerror,
storefuns/init-put-10 is used by ac-init-02, ac-init,
storefuns/init-put-11 is used by add-initundone-01, add-initundone, ac-init-01, ac-init,
storefuns/init-put-12 is used by add-initdone-01, add-initdone,
storefuns/init-total is used by addobj-initdone, ac-init-03,
storefuns/initdone-04 is used by add-initdone, add-init,
storefuns/initerror-04 is used by add-initerror-01,
storefuns/initundone-04 is used by add-initundone-01,
storefuns/instore-01 is used by validref-put-samefield, validref-primtype-02, validref-primtype-01, validref-primtype, validref-okreftype, validfieldinits-rec, valid-type-typeval, stsubset-addobj, isobj-void, isobj-update-01, isobj-update, isobj-union-01, isobj-typele, isobj-type-04, isobj-type-01, isobj-subset, isobj-reftype, isobj-rec, isobj-putbar-01, isobj-putbar, isobj-put-statfield, isobj-put-samefield-03, isobj-put-samefield-02, isobj-put-samefield-01, isobj-put-samefield, isobj-put-index-02, isobj-put-index-01, isobj-put-badfield, isobj-put-04, isobj-put-03, isobj-put-02, isobj-notin-04, isobj-notin, isobj-newref-01, isobj-newref, isobj-isobj-01, isobj-isobj, isobj-isarray, isobj-fieldtype, isobj-field-in, isobj-del-03, isobj-del-01, isobj-del, isobj-bytearray, isobj-arraytype-01, isobj-all, isobj-addobj-03, isobj-addobj-02, isobj-addobj-01, isobj-addobj, isobj-addclass, is_valid_ref-type, is_valid_ref-put-samefield, is_valid_ref-put-equiv, is_valid_ref-02, is_obj-union-disjoint, is_obj-typeex-01, is_obj-put-samefield, is_obj-put-equiv, is_obj-notin-01, is_obj-no-refval-01, is_obj-no-refval, is_obj-full-expand, is_obj-field-norefval, is_obj-field-noreftype, instore-addobj-rec, endfinallymode, del-addobj, addobj-union, addobj-subset, addobj-okarray, addclass-validFields, addclass-okarray, add-uninit, add-okclass-01, add-okarray-05, add-okarray, add-in-04, add-in-03, ac-uninit, ac-okarray-01, ac-okarray, ac-in-11, ac-in-10, ac-in-06, ac-in-03-02, ac-in-03, ac-in-02,
storefuns/instore-02 is used by add-in-02, ac-in-09, ac-in-08,
storefuns/look-del is used by reffield-del, isobj-del-03, isobj-del-01, isobj-del, is_valid_ref-del-01, is_obj-del, del-addobj, addobj-delsw,
storefuns/lookup-one is used by addobj-at-other-01,
storefuns/newjvmref is used by ac-new,
storefuns/newref-01 is used by validref-new, stsubset-addobj, nouninit-addobj, isobj-newref-02, isobj-newref-01, isobj-newref, isobj-addobj-01, endfinallymode-01, del-addobj, addobj-union-rew, addobj-union, addobj-throw-subset, addobj-subset, addobj-okbytearray, add-out, add-mode, add-at,
storefuns/newref-02 is used by ac-new,
storefuns/newref-03 is used by stsubset-addobj, isobj-newref-01, isobj-newref, del-addobj, addobj-union, addobj-subset, add-at,
storefuns/newref-in is used by refcount-addobj,
storefuns/newref-in-01 is used by stsubset-addobj,
storefuns/newref-jvmref is used by endfinallymode-03, add-init-newref-02, add-init-newref-01, add-init-newref,
storefuns/newref-put-01 is used by newref-addobj,
storefuns/newrefsnew is used by add-mode-02,
storefuns/put-one is used by add-put-06,
storefuns/put-put-first-01 is used by add-put-03,
storefuns/refin is used by isobj-put-samefield-01, ac-in-03,

Used from specification int-basic2

int-basic2/add-a is used by addobj-getarray-01, add-putbar-rew,
int-basic2/add-c is used by addobj-getarray-01, add-putbar-rew,
int-basic2/ax-04 is used by addobj-getarray-01,

Used from specification valuefuns

valuefuns/okval-array is used by is_obj-no-refval-01,
valuefuns/okval-class is used by is_obj-no-refval,
valuefuns/okval-int is used by isobj-fieldtype,
valuefuns/okval-reftype is used by is_obj-field-norefval,
valuefuns/okval-refval-01 is used by is_obj-field-noreftype,
valuefuns/okval-void is used by is_valid_ref-put-samefield,
valuefuns/refval-xtra is used by isobj-arraytype-01, is_obj-refval-01, is_obj-refval, ac-okreftype, ac-okarray-01,
valuefuns/typeval-xtra is used by is_valid_ref-typeval-01, is_valid_ref-type-typeval, is_obj-type-01,

Used from specification fieldinit

fieldinit/lookup-01 is used by ac-lookup,
fieldinit/lookup-02 is used by ac-lookup,
fieldinit/lookup-03 is used by ac-lookup,
fieldinit/shift is used by ac-shift-03, ac-shift-02,

Used from specification fieldspec

Used from specification intnat

intnat/labs is used by addobj-getarray-01,
intnat/rax-04 is used by addobj-getarray-01,

Used from specification int-abs

int-abs/absle is used by addobj-getarray-01,
int-abs/ax-02 is used by reffield-del,
int-abs/elim-sub is used by addobj-getarray-01,
int-abs/forward-le-01 is used by isobj-bytearray, addobj-okarray, addobj-getarray-01, addclass-okarray, add-okarray-05, add-okarray, ac-okarray-01, ac-okarray,
int-abs/forward-le-02 is used by isvalidref-put-array-badindex,
int-abs/forward-le-05 is used by reffield-del, addobj-okarray, addclass-okarray, add-okarray-05, add-okarray, ac-okarray-01, ac-okarray,
int-abs/lels is used by reffield-del, isobj-putbar-01, isobj-bytearray, addobj-okarray, addobj-getarray-01, addclass-okarray, add-putbar-rew, add-okarray-05, add-okarray, ac-okarray-01, ac-okarray,
int-abs/lels-01 is used by isobj-putbar-01, isobj-bytearray, addobj-okarray, addobj-getarray-01, addclass-okarray, add-putbar-rew, add-okarray-05, add-okarray, ac-okarray-01, ac-okarray,
int-abs/lels-03 is used by reffield-del, addobj-okarray, addclass-okarray, add-putbar-rew, add-okarray-05, add-okarray, ac-okarray-01, ac-okarray,
int-abs/lels-04 is used by addobj-okarray, addobj-getarray-01, addclass-okarray, add-putbar-rew, add-okarray-05, add-okarray, ac-okarray-01, ac-okarray,
int-abs/mone-06 is used by addobj-getarray-01,
int-abs/numls-02 is used by addobj-getarray-01,
int-abs/numsub is used by addobj-getarray-01,
int-abs/zero-gels-04 is used by addobj-getarray-01,

Used from specification okfuns

okfuns/exactarray-01 is used by exactarray-addobj, addclass-exactarray,
okfuns/exactreftype is used by exactarray-addobj, addclass-exactarray,
okfuns/gfts-all is used by isobj-update-01, isobj-union-01, isobj-subset, isobj-putbar-01, isobj-putbar, isobj-put-samefield-01, isobj-put-index-01, isobj-put-badfield, isobj-put-03, isobj-fieldtype, isobj-field-in, isobj-del-01, isobj-all, isobj-addobj-04, isobj-addobj-03, isobj-addobj-01, is_obj-notin-01, is_obj-no-refval-01, is_obj-no-refval, is_obj-field-norefval, is_obj-field-noreftype,
okfuns/gfts-not-01 is used by isobj-put-samefield-02,
okfuns/gfts-put is used by isobj-put-index-01,
okfuns/good-field-02 is used by isobj-putbar,
okfuns/good-field-def is used by isobj-update-01, isobj-putbar-01, isobj-addobj-04, isobj-addobj-01, isobj-addobj, isobj-addclass, add-goodfield,
okfuns/good-field-field is used by isobj-union-01, isobj-subset,
okfuns/hasKeys-all is used by addclass-validFields,
okfuns/instore-empty is used by instore-addobj-rec, instore-addobj,
okfuns/instore-rec-03 is used by instore-addobj-rec, instore-addobj,
okfuns/is-any-array is used by validref-typeval, validref-put-01, validref-primtype-02, validref-primtype-01, validref-primtype, validref-okreftype, validref-notin-01, valid-type-typeval, addobj-isarray,
okfuns/is-real-array-def is used by isvalidref-put-array-badindex, isobj-array-01, isarray-isobj-01, is_valid_ref-void, is_valid_ref-typeex-01, is_valid_ref-type-typeval, is_valid_ref-put, is_valid_ref-primarray, is_valid_ref-del-01, is_valid_ref-def, is_valid_ref-addobj-01, is_valid_ref-addobj, is_array-addobj-01, is_array-addobj,
okfuns/is_array-arraytype is used by is_valid_ref-putbytearray,
okfuns/is_array-put-field is used by is_valid_ref-put-equiv,
okfuns/is_javastore is used by add-okstore,
okfuns/isarray-put is used by validref-put,
okfuns/isarray-put-01 is used by is_valid_ref-put,
okfuns/isarray-put-array-badindex is used by isvalidref-put-array-badindex,
okfuns/isarray-put-field is used by is_valid_ref-put,
okfuns/isarray-put-samefield is used by validref-put-samefield-01,
okfuns/isarray-put-samefield-01 is used by validref-put-samefield,
okfuns/isarray-type-03 is used by addobj-isarray-01,
okfuns/keys-in-01 is used by isobj-addobj-04, instfields-type,
okfuns/okarrayNotNull is used by isobj-bytearray, addobj-okarray, addclass-okarray,
okfuns/okarrayOfLength is used by add-okarray-05, add-okarray, ac-okarray-01, ac-okarray,
okfuns/okarrays-all is used by ac-okarrays,
okfuns/okbytearray-01 is used by isobj-bytearray, addclass-okbytearray, add-okbar,
okfuns/okclass is used by add-okclass-01, add-okclass, ac-okclass,
okfuns/okreftype is used by validref-okreftype, isobj-bytearray, isobj-array, addclass-okarray, add-okreftype, add-okarray-05, ac-okreftype, ac-okarray,
okfuns/okstore is used by add-okstore,
okfuns/update-put-rew is used by add-update-same,
okfuns/update-rec is used by addobj-union-switch, addclass-update-sw, add-update-same,
okfuns/update-rec-01 is used by addobj-union-switch, addclass-update-sw,
okfuns/validFields is used by validFields-addobj, addclass-validFields,
okfuns/getkeys-app is used by okfieldinits-index, okfieldinits-class,
okfuns/getkeys-empty is used by okfieldinits-index, okfieldinits-class,
okfuns/getkeys-one is used by okfieldinits-index, okfieldinits-class,
okfuns/gft-put is used by isobj-putref,
okfuns/gft-union is used by isobj-union,
okfuns/gfts-in is used by isobj-all,
okfuns/gfts-put is used by isobj-put-01, isobj-put,
okfuns/good-field-del is used by isobj-del-01, isobj-del,
okfuns/good-field-field is used by isobj-update-01, isobj-union-01, isobj-subset, isobj-putbar-01, isobj-putbar, isobj-addobj-01, isobj-addclass,
okfuns/good-field-field-01 is used by isobj-fieldtype, is_obj-no-refval-01, is_obj-no-refval, is_obj-field-norefval, is_obj-field-noreftype,
okfuns/good-field-in is used by isobj-update-01, isobj-addobj, add-goodfield,
okfuns/good-field-in-01 is used by isobj-update-01, isobj-field-in, isobj-addobj, is_obj-notin-01, add-goodfield,
okfuns/good-field-index is used by isobj-update-01, isobj-union-01, isobj-subset, isobj-putbar-01, isobj-putbar, isobj-addobj-01, isobj-addobj, isobj-addclass, add-goodfield,
okfuns/good-field-put is used by isobj-put-index-01,
okfuns/good-field-rew is used by isobj-put-samefield-01, isobj-put-badfield, isobj-put-03,
okfuns/good-one is used by is_obj-putba,
okfuns/goodfields-putba is used by is_obj-putba,
okfuns/hasKeys-put is used by haskeys-addobj,
okfuns/is_array-arraytype is used by is_valid_ref-putbytearray, is_valid_ref-no-arraytype,
okfuns/is_array-del is used by is_valid_ref-del-01,
okfuns/is_array-is-array is used by is_valid_ref-update, is_valid_ref, is_array-validref,
okfuns/is_array-okbytearray is used by is_valid_ref-okbytearray,
okfuns/is_array-put-01 is used by isvalidref-put-array-badindex, is_valid_ref-put-01,
okfuns/is_array-put-byte is used by is_valid_ref-put-byte,
okfuns/is_array-put-field is used by is_valid_ref-put-samefield-01, is_valid_ref-put-samefield,
okfuns/is_array-reftype is used by is_valid_ref-reftype,
okfuns/is_array-type-03 is used by is_valid_ref-02,
okfuns/is_array-type-04 is used by is_valid_ref-type-01,
okfuns/is_array-typeex is used by is_valid_ref-typeex,
okfuns/is_array-typeex-01 is used by is_valid_ref-typeex-02,
okfuns/is_array-typele is used by is_valid_ref-type, is_valid_ref-obj, is_valid_ref-field-in,
okfuns/is_array-update is used by is_valid_ref-update,
okfuns/isarray-del is used by validref-del-01, reffield-del,
okfuns/isarray-del-01 is used by validref-del,
okfuns/isarray-newref is used by validref-new,
okfuns/isarray-notin is used by validref-notin,
okfuns/isarray-null is used by validref-null,
okfuns/isarray-reftype is used by validref-reftype,
okfuns/isarray-type-01 is used by isobj-isarray,
okfuns/isarray-update is used by is_valid_ref-update,
okfuns/okarray-01 is used by ac-okarrays,
okfuns/okarray-05 is used by validref-primtype-02, validref-primtype-01, validref-primtype, validref-okreftype, valid-type-typeval, isobj-bytearray, addclass-okbytearray,
okfuns/okarray-06 is used by okarray-addobj,
okfuns/okarray-jvmref is used by ac-okarrays,
okfuns/okarray-jvmref-01 is used by ac-okarrays,
okfuns/okarray-put-other is used by validref-put-01,
okfuns/okbar-new is used by addobj-okbytearray,
okfuns/okbytearray-02 is used by addclass-okbytearray,
okfuns/okreftype-02 is used by ac-okreftype,
okfuns/okstore-08 is used by add-okstore,
okfuns/oktype-array is used by validfieldinits-one-02,
okfuns/oktype-byte is used by isobj-bytearray,
okfuns/oktype-class is used by validfieldinits-one-01,
okfuns/oktype-okval is used by validfieldinits-rec, validfieldinits-one, isobj-putbar, isobj-put-samefield-03, isobj-put-samefield-02, isobj-put-samefield-01, isobj-put-samefield, isobj-put-03, isobj-put-02, isobj-addobj-04, is_valid_ref-put-samefield-01, is_valid_ref-put-samefield, is_valid_ref-put, is_obj-put-samefield-01, is_obj-put-samefield, is_obj-put-equiv, is_obj-put, addclass-okarray,
okfuns/oktype-st is used by addobj-oktype, addobj-okarray, add-oktype-01, add-oktype, add-okarray-05, add-okarray, ac-oktype, ac-okarray-01, ac-okarray,
okfuns/update-at is used by isobj-update-01, isobj-update, is_valid_ref-update, is_obj-update,
okfuns/update-empty is used by addobj-union-switch, addclass-update-sw, add-update-same,
okfuns/update-in is used by isobj-update-01, isobj-update,
okfuns/update-put-same is used by add-update-same,

Used from specification storekey

storekey/ex-03 is used by instfields-subclass-01, addobj-addclass-sw, add-putbar-rew,
storekey/ex-04 is used by statfields-index-01, isobj-addobj-04, instfields-subclass-01, instfields-index-01,
storekey/sel-05 is used by is_obj-put-equiv,
storekey/disj is used by addclass-switch, ac-in,
storekey/elim-03 is used by validfieldinits-rec, okfieldinits-index, okfieldinits-class, okfieldinits-at, okfieldinits-abstract, isobj-subset, isobj-put-samefield-01, isobj-put-03, isobj-addobj-04, isobj-addclass, is_valid_ref-put-equiv, is_obj-put-equiv, instfields-index-02, addclass-switch-01, addclass-switch, ac-type, ac-shift-03, ac-shift-02, ac-shift, ac-refs, ac-refin, ac-out, ac-okarrays, ac-no1, ac-new, ac-mode-01, ac-mode, ac-lookup-06, ac-lookup-05, ac-lookup-04, ac-lookup-03, ac-lookup-02, ac-lookup, ac-isarray, ac-init-02, ac-init-01, ac-init, ac-in-11, ac-in-10, ac-in-09, ac-in-08, ac-in-06, ac-in-03-02, ac-in-03, ac-in-02, ac-in, ac-getbar, ac-dups-05, ac-dups-04, ac-dups-03, ac-dups-02, ac-del-02, ac-del-01, ac-del, ac-bad-03, ac-bad-02, ac-bad-01, ac-bad,
storekey/elim-04 is used by add-putbar-rew,
storekey/inj-03 is used by okfieldinits-class, okfieldinits-at, okfieldinits-abstract, isobj-put-samefield-01, isobj-put-03, endfinallymode-05, addobj-addclass-sw, add-field-same-02, add-field-same, ac-shift-03, ac-shift-02, ac-shift, ac-out, ac-mode-01, ac-mode, ac-lookup-03, ac-lookup-02, ac-lookup-01, ac-lookup, ac-init-02, ac-init-01, ac-init, ac-in-06, ac-in,
storekey/sel-05 is used by validfieldinits-rec, validfieldinits-one-02, validfieldinits-one-01, okfieldinits-class, okfieldinits-at, isobj-addobj-04, instfields-index-02, ac-shift-03, ac-shift-02, ac-in,
storekey/sel-06 is used by add-putbar-rew,
storekey/test is used by validfieldinits-rec, validfieldinits-one, okfieldinits-index, isobj-update-01, isobj-putbar-01, isobj-put-samefield-01, isobj-put-03, isobj-addobj-04, isobj-addobj-01, isobj-addclass, addclass-switch-01, addclass-switch, add-putbar-rew, ac-type, ac-shift-03, ac-shift-02, ac-shift, ac-refs, ac-refin, ac-out, ac-okarrays, ac-new, ac-mode-01, ac-mode, ac-lookup-06, ac-lookup-05, ac-lookup-04, ac-lookup-03, ac-lookup-02, ac-lookup, ac-isarray, ac-init-02, ac-init-01, ac-init, ac-in-11, ac-in-10, ac-in-09, ac-in-08, ac-in-06, ac-in-03-02, ac-in-03, ac-in-02, ac-in, ac-getbar, ac-dups-05, ac-dups-04, ac-dups-03, ac-dups-02, ac-del-02, ac-del-01, ac-del, ac-bad-03, ac-bad-02, ac-bad-01, ac-bad,
storekey/test-01 is used by validfieldinits-rec, validfieldinits-one, okfieldinits-one, isobj-update-01, isobj-union-01, isobj-subset, isobj-putbar-01, isobj-putbar, isobj-put-samefield-01, isobj-put-badfield, isobj-put-03, isobj-addobj-04, isobj-addobj-01, isobj-addobj, isobj-addclass, is_valid_ref-put-equiv, instfields-subclass-01, instfields-index-02, addobj-addclass-sw, addclass-switch-01, addclass-switch, add-goodfield, ac-type, ac-shift-03, ac-shift-02, ac-shift, ac-refs, ac-refin, ac-out, ac-okarrays, ac-new, ac-mode-01, ac-mode, ac-lookup-06, ac-lookup-05, ac-lookup-04, ac-lookup-03, ac-lookup-02, ac-lookup, ac-isarray, ac-init-02, ac-init-01, ac-init, ac-in-11, ac-in-10, ac-in-09, ac-in-08, ac-in-06, ac-in-03-02, ac-in-03, ac-in-02, ac-in, ac-getbar, ac-dups-05, ac-dups-04, ac-dups-03, ac-dups-02, ac-del-02, ac-del-01, ac-del, ac-bad-03, ac-bad-02, ac-bad-01, ac-bad,
storekey/test-02 is used by validfieldinits-rec, validfieldinits-one, okfieldinits-one, okfieldinits-index, isobj-putbar, isobj-put-samefield-01, isobj-put-badfield, isobj-put-03, isobj-addobj-04, isobj-addobj, is_valid_ref-put-equiv, addobj-addclass-sw, addclass-switch-01, add-goodfield, ac-type, ac-shift-03, ac-shift-02, ac-shift, ac-refs, ac-refin, ac-out, ac-okarrays, ac-new, ac-mode-01, ac-mode, ac-lookup-06, ac-lookup-05, ac-isarray, ac-in-11, ac-in-10, ac-in-03-02, ac-in-03, ac-in-02, ac-getbar,
storekey/test-05 is used by validfieldinits-rec, validfieldinits-one-02, validfieldinits-one-01, okfieldinits-index, okfieldinits-class, okfieldinits-at, okfieldinits-abstract, isobj-subset, isobj-put-samefield-01, isobj-put-03, isobj-addobj-04, isobj-addclass, is_valid_ref-put-equiv, is_obj-put-equiv, addclass-switch-01, addclass-switch, ac-type, ac-shift-03, ac-shift-02, ac-shift, ac-refs, ac-refin, ac-out, ac-okarrays, ac-no1, ac-new, ac-mode-01, ac-mode, ac-lookup-06, ac-lookup-05, ac-lookup-04, ac-lookup-03, ac-lookup-02, ac-lookup, ac-isarray, ac-init-02, ac-init-01, ac-init, ac-in-11, ac-in-10, ac-in-09, ac-in-08, ac-in-06, ac-in-03-02, ac-in-03, ac-in-02, ac-in, ac-getbar, ac-dups-05, ac-dups-04, ac-dups-03, ac-dups-02, ac-del-02, ac-del-01, ac-del, ac-bad-03, ac-bad-02, ac-bad-01, ac-bad,
storekey/test-07 is used by validfieldinits-rec, addclass-switch, add-putbar-rew, ac-shift-03, ac-shift-02, ac-no2, ac-lookup-05, ac-lookup-04, ac-lookup-03, ac-lookup-02, ac-lookup, ac-init-02, ac-init-01, ac-init, ac-in-11, ac-in-09, ac-in-08, ac-in-06, ac-in, ac-dups-05, ac-dups-04, ac-dups-03, ac-dups-02, ac-del-02, ac-del-01, ac-del, ac-bad-03, ac-bad-02, ac-bad-01, ac-bad,
storekey/test-08 is used by add-putbar-rew, ac-in,

Used from specification typefuns

typefuns/array-le is used by is_valid_ref-putbytearray,
typefuns/classex-def is used by is_obj-no-interface,
typefuns/elemtype-base is used by isobj-type-08,
typefuns/subtype-object is used by is_valid_ref-type, is_obj-typele,
typefuns/typeex-def is used by is_valid_ref-typeex, is_obj-typele, is_obj-typeex-02, is_obj-typeex,
typefuns/array is used by validfieldinits-one-02, isobj-array, is_obj-array, addclass-okarray, add-okarray-05, ac-okarray,
typefuns/bytearray is used by isobj-bytearray,
typefuns/classex-02 is used by is_obj-not-classex-02,
typefuns/classex-03 is used by is_obj-not-tdnameex,
typefuns/elemtype-04 is used by is_valid_ref-addobj-01, is_array-addobj-01,
typefuns/elemtype-05 is used by is_valid_ref-void, is_valid_ref-type-typeval,
typefuns/elemtype-07 is used by is_valid_ref-primarray,
typefuns/elemtype-rec is used by isobj-type-08,
typefuns/hasclasstype is used by isobj-hasclasstype,
typefuns/interfaceex-noclass is used by is_obj-no-interface,
typefuns/interfaceex-notpredef is used by is_obj-no-interface,
typefuns/is_abstract-predef is used by is_obj-not-classex-02,
typefuns/is_primtype-01 is used by is_valid_ref-primarray,
typefuns/is_primtype-02 is used by is_valid_ref-primarray,
typefuns/isreftype-01 is used by is_valid_ref-int,
typefuns/isreftype-04 is used by isobj-reftype,
typefuns/jtclass is used by is_valid_ref-typeex, is_obj-typele, is_obj-typeex-02, is_obj-typeex,
typefuns/prim-abstract is used by is_valid_ref-primarray,
typefuns/prim-void is used by is_valid_ref-primarray,
typefuns/subclass is used by isobj-typele, isobj-field-in, is_valid_ref-type, instfields-subclass-in,
typefuns/subclass-01 is used by validref-okreftype,
typefuns/tdnameex is used by is_obj-not-tdnameex,
typefuns/tdnameex-04 is used by is_valid_ref-typeex, is_valid_ref-type, is_obj-typele, is_obj-typeex-02, is_obj-typeex,
typefuns/tdnameex-def is used by addobj-init-02,
typefuns/typeex-02 is used by is_obj-typeex-01,
typefuns/typeex-array is used by is_valid_ref-primarray,
typefuns/typeex-class is used by is_valid_ref-type, is_valid_ref-addobj-01, is_array-addobj-01,

Used from specification fieldname

fieldname/inj is used by endfinallymode-05, add-initundone, add-initerror, add-initdone-01, add-field-same, ac-type, ac-mode-01, ac-in-03,

Used from specification pair

pair/fieldinit/elim is used by okfieldinits-index, okfieldinits-class, instore-addobj-rec, instore-addobj, ao-put, addobj-union-switch, addobj-rec-01, addobj-at-other-03, addclass-update-sw, addclass-switch-01, addclass-switch, add-update-same, add-type, add-nput-02, add-nput-01, add-nput, add-notin, add-in-09, add-gins, ac-type, ac-shift-03, ac-shift-02, ac-shift, ac-refin, ac-out, ac-no2, ac-no1, ac-new, ac-mode-01, ac-mode, ac-lookup-04, ac-lookup-03, ac-lookup-02, ac-lookup, ac-isarray, ac-init-02, ac-init-01, ac-init, ac-in-11, ac-in-10, ac-in-09, ac-in-08, ac-in-06, ac-in-03-02, ac-in-03, ac-in-02, ac-in, ac-getbar, ac-dups-03, ac-dups-02, ac-del-01, ac-del, ac-bad-03, ac-bad-02, ac-bad-01, ac-bad,
pair/fieldinit/inj is used by validfieldinits-rec, validfieldinits-one,
pair/fieldinit/sel-01 is used by instore-addobj-rec, instore-addobj,
pair/fieldinit/sel-02 is used by instore-addobj-rec, instore-addobj, addclass-switch-01, addclass-switch, ac-type, ac-shift-03, ac-shift-02, ac-shift, ac-refs, ac-refin, ac-out, ac-new, ac-mode-01, ac-mode, ac-lookup-06, ac-lookup-05, ac-lookup-04, ac-lookup-03, ac-lookup-02, ac-lookup, ac-isarray, ac-init-02, ac-init-01, ac-init, ac-in-11, ac-in-10, ac-in-09, ac-in-08, ac-in-06, ac-in-03-02, ac-in-03, ac-in-02, ac-in, ac-getbar, ac-dups-05, ac-dups-04, ac-dups-03, ac-dups-02, ac-del-02, ac-del-01, ac-del, ac-bad-03, ac-bad-02, ac-bad-01, ac-bad,

Used from specification classnamefuns

classnamefuns/le-reflexive is used by isobj-typele,

Used from specification oelem

oelem/intlista/irreflexivity is used by addobj-getarray-01,

Used from specification set-basic

set-basic/references/In-insert is used by add-refs,
set-basic/references/add-01 is used by ac-refs,
set-basic/classnames/ne-01 is used by nouninit-addobj, nouninit-addclass, ac-uninitset, ac-init-first,
set-basic/references/ne-01 is used by refcount-addobj, is_obj-union-disjoint,
set-basic/references/size-ins is used by refcount-addobj,
set-basic/classnames/size-zero-01 is used by nouninit-addobj, nouninit-addclass, ac-uninitset, ac-init-first,

Used from specification refkey

refkey/elim is used by addobj-put-switch-01, addobj-at, add-putbar-rew, ac-mode-01,
refkey/inj is used by isobj-put-samefield-01, isobj-put-03, is_obj-put-statfield, is_obj-put-equiv, ao-put, addobj-in-02, addobj-at-this, addobj-at-other-03, addobj-at-01, addclass-switch-01, addclass-switch, add-put-02, add-nput-02, add-nput-01, add-nput, add-gins, add-field-same-02, add-field-same, ac-shift-03, ac-shift-02, ac-shift, ac-init-02, ac-init-01, ac-init, ac-in-11, ac-in-10, ac-in, ac-del-01, ac-del,
refkey/inj-01 is used by isobj-put-samefield-01, isobj-put-03, isobj-put-02, is_obj-put-statfield, is_obj-put-equiv, ao-put, addobj-in-02, addobj-at-this, addobj-at-other-03, addobj-at-01, addclass-switch-01, addclass-switch, add-type, add-nput-02, add-nput-01, add-nput, add-notin, add-in-09, add-in-08, add-in-06, add-in-03, add-gins, add-field-same-02, add-field-same, add-field-if, add-field-03, add-field-02, add-at-01, ac-type, ac-shift-03, ac-shift-02, ac-shift, ac-lookup-06, ac-lookup-05, ac-lookup-03, ac-lookup-02, ac-lookup-01, ac-lookup, ac-init-01, ac-init, ac-in-11, ac-in-10, ac-in, ac-del-01, ac-del,
refkey/sel-01 is used by isobj-putref, isobj-putbar-01, isobj-putbar, add-putbar-rew, ac-refs,
refkey/sel-02 is used by isobj-putbar-01, isobj-putbar, add-putbar-rew,

Used from specification javatype

javatype/ex-02 is used by is_valid_ref-putbytearray,
javatype/diff is used by validref-okreftype, isobj-arraytype,
javatype/disj-02 is used by is_valid_ref-void, is_valid_ref-type-typeval,
javatype/disj-07 is used by is_valid_ref-addobj-01, is_array-addobj-01,
javatype/disj-09 is used by is_valid_ref-addobj-01, is_array-addobj-01,
javatype/elim-01 is used by valid-type-typeval, addclass-okarray, add-okarray-05, ac-okarrays, ac-okarray,
javatype/elim-02 is used by valid-type-typeval, isobj-update, isobj-union-01, isobj-subset, isobj-reftype, isobj-putbar-01, isobj-putbar, isobj-put-statfield, isobj-put-samefield-03, isobj-put-samefield, isobj-put-index-02, isobj-put-badfield, isobj-put-04, isobj-put-02, isobj-isarray, isobj-field-in, isobj-arraytype-01, is_valid_ref-type, is_obj-notin-01, is_obj-no-refval-01, is_obj-no-refval, is_obj-full-expand, instfields-subclass-in,
javatype/inj-02 is used by isobj-type-04, isobj-type-01, is_valid_ref-type, is_obj-notin-01, is_obj-no-refval-01, is_obj-no-refval,
javatype/sel-02 is used by isobj-subset, isobj-putbar-01, isobj-put-samefield-03, isobj-put-samefield, isobj-put-badfield, isobj-put-02, isobj-isobj-01, isobj-isobj, isobj-addobj-04, is_valid_ref-addobj-01, is_valid_ref-02, is_obj-not-tdnameex, is_obj-not-classex-02, is_obj-not-classex-01, is_obj-no-interface, is_obj-field-norefval, is_obj-field-noreftype, is_obj-addobj-01,
javatype/test-01 is used by validref-primtype-01, add-okarray-02,
javatype/test-02 is used by validref-primtype, add-okarray-01,
javatype/test-03 is used by validref-primtype-01, add-okarray-02,
javatype/test-04 is used by validref-primtype, add-okarray-01,
javatype/test-09 is used by valid-type-typeval, addclass-okarray, add-okarray-05, ac-okarrays, ac-okarray,
javatype/test-10 is used by isobj-update, isobj-union-01, isobj-subset, isobj-reftype, isobj-putbar-01, isobj-putbar, isobj-put-statfield, isobj-put-samefield-03, isobj-put-samefield, isobj-put-index-02, isobj-put-badfield, isobj-put-04, isobj-put-02, isobj-isobj-01, isobj-isobj, isobj-field-in, isobj-arraytype-01, isobj-addobj-04, is_valid_ref-type, is_valid_ref-02, is_obj-notin-01, is_obj-no-refval-01, is_obj-no-refval, is_obj-full-expand, is_obj-field-norefval, is_obj-field-noreftype, instfields-subclass-in,
javatype/test-13 is used by validref-primtype-02, add-okarray-03,
javatype/test-14 is used by add-okarray-04,
javatype/test-16 is used by isobj-type-07, isobj-arraytype-02,
javatype/test-20 is used by validref-primtype-02, add-okarray-03,
javatype/test-21 is used by add-okarray-04,
javatype/test-22 is used by isobj-void,
javatype/test-28 is used by isobj-arraytype-01,

Used from specification javavalue

javavalue/refva-sel is used by is_obj-refval-01, is_obj-refval,
javavalue/disj-20 is used by addclass-okarray, addclass-exactarray, ac-okarray-01, ac-okarray,
javavalue/disj-41 is used by isobj-addclass, ac-okclass, ac-class,
javavalue/elim-02 is used by isobj-bytearray, addobj-okarray, addclass-okarray, ac-okarrays,
javavalue/elim-10 is used by validref-okreftype, valid-type-typeval, isobj-update, isobj-union-01, isobj-subset, isobj-putbar-01, isobj-putbar, isobj-put-statfield, isobj-put-samefield-03, isobj-put-samefield, isobj-put-index-02, isobj-put-badfield, isobj-put-04, isobj-put-02, isobj-field-in, isobj-arraytype-01, is_valid_ref-typeval-01, is_valid_ref-type-typeval, is_obj-full-expand, is_obj-field-norefval, is_obj-field-noreftype, addclass-okarray, add-okarray-05, ac-okarray,
javavalue/elim-13 is used by exactarray-addobj-01, add-oktype-02,
javavalue/elim-refval is used by isobj-arraytype-01, ac-okreftype, ac-okarray-01,
javavalue/inj-03 is used by ac-okreftype, ac-okarray-01,
javavalue/inj-07 is used by add-putbar-rew,
javavalue/inj-09 is used by instore-addobj, addobj-union-rew, addobj-union, addobj-type, addobj-isarray-01, addobj-delsw, addobj-addobj-switch, addobj-addclass-sw, add-type-04, add-type-01, add-type, add-putbar-rew, add-okclass, add-dupput, add-classof,
javavalue/inj-12 is used by addobj-addclass-sw, add-initundone-01, add-initundone, ac-lookup-03, ac-init-10, ac-init-09, ac-init-07, ac-init-06, ac-init-02, ac-init-01, ac-init,
javavalue/sel-09 is used by validref-okreftype, validfieldinits-one-02, validfieldinits-one-01, isobj-bytearray, isobj-arraytype-01, isobj-array, exactarray-addobj, addclass-okarray, addclass-exactarray, add-reftype-01, add-reftype, add-okreftype, add-okclass-01, add-okclass, add-okarray-05, add-okarray, ac-okreftype, ac-okclass, ac-okarray,
javavalue/sel-11 is used by validref-okreftype, isobj-void, isobj-typele, isobj-type-04, isobj-type-01, isobj-subset, isobj-putbar-01, isobj-put-samefield-03, isobj-put-samefield, isobj-put-badfield, isobj-put-02, isobj-isobj-01, isobj-isobj, isobj-arraytype-02, isobj-arraytype-01, isobj-addobj-04, is_valid_ref-void, is_valid_ref-typeex-01, is_valid_ref-type, is_valid_ref-primarray, is_valid_ref-addobj-01, is_valid_ref-02, is_obj-typeex-01, is_obj-notin-01, is_obj-no-refval-01, is_obj-no-refval, is_obj-addobj-01, is_array-addobj-01,
javavalue/test-19 is used by validref-okreftype, validfieldinits-one-02, validfieldinits-one-01, isobj-bytearray, isobj-arraytype-01, isobj-array, exactarray-addobj, addclass-okarray, addclass-exactarray, add-reftype-01, add-reftype, add-okreftype, add-okarray-05, ac-okreftype, ac-okarray-01, ac-okarray,
javavalue/test-24 is used by isobj-fieldtype,
javavalue/test-25 is used by isobj-bytearray, addobj-okarray, addclass-okarray, ac-okarrays,
javavalue/test-91 is used by isobj-putbar, addclass-okarray, addclass-exactarray, ac-okreftype, ac-okarray,
javavalue/test-92 is used by validref-okreftype, isobj-union-01, isobj-subset, isobj-putbar-01, isobj-putbar, isobj-put-samefield-03, isobj-put-samefield, isobj-put-badfield, isobj-put-02, isobj-isobj-01, isobj-isobj, isobj-field-in, isobj-arraytype-01, isobj-addobj-04, is_valid_ref-type, is_valid_ref-02, is_obj-typeex-01, is_obj-notin-01, is_obj-no-refval-01, is_obj-no-refval, is_obj-full-expand, is_obj-field-norefval, is_obj-field-noreftype, addclass-okarray, add-type-03, add-okstore, add-okarray-05, ac-okarray,

Used from specification storearrays

storearrays/get-rec-01 is used by addobj-getarray-01,
storearrays/getArray-all is used by addobj-getarray,
storearrays/getintarray is used by addobj-getintarray-01,
storearrays/getintarray-def is used by addobj-getintarray,
storearrays/putBar-in is used by add-putbar-rew,
storearrays/putbar-atother-01 is used by add-putbar-rew,
storearrays/putbar-atref-01 is used by add-putbar-rew,
storearrays/arrayref is used by ac-isarray,
storearrays/get-put-05 is used by ac-getbar,
storearrays/getArray-zero is used by addobj-getarray-01,
storearrays/getByteArray-put is used by getByteArray-addobject, ac-getbar,
storearrays/getbar-ref is used by getByteArray-addobject-01,
storearrays/isarray is used by add-isarray,
storearrays/putBar-at-fskey is used by isobj-putbar-01, isobj-putbar, add-putbar-rew,
storearrays/putBar-at-type is used by isobj-putbar-02, isobj-putbar-01, isobj-putbar, is_valid_ref-putbytearray, is_obj-putbar, is_obj-putba,
storearrays/putBar-in is used by isobj-putbar-01, isobj-putbar, add-putbar-rew,
storearrays/putbar-atfs-01 is used by add-putbar-rew,
storearrays/putbar-byte is used by add-putbar-rew,
storearrays/putbar-in-01 is used by isobj-putbar,
storearrays/putbar-infs is used by add-putbar-rew,
storearrays/putbar-inref is used by is_obj-putba, add-putbar-rew,

Used from specification specialkeys

specialkeys/endfinallymode is used by endfinallymode-05, endfinallymode-04, endfinallymode-03, endfinallymode-02, endfinallymode,
specialkeys/mode is used by mode-addobj, isobj-mode, addclass-mode-in, add-mode-01,
specialkeys/out is used by add-out-02, add-out-01, ac-out-01,
specialkeys/type is used by is_obj-put-equiv, instfields-type-01,
specialkeys/uninit is used by addobj-initundone, add-uninit, ac-uninit,
specialkeys/diff-01 is used by addobj-mode-01, addobj-mode,
specialkeys/endfin-key is used by endfinallymode-05,
specialkeys/length-01 is used by addclass-okarray,
specialkeys/mode-01 is used by isobj-mode,
specialkeys/mode-02 is used by ac-mode-01, ac-mode,
specialkeys/mode-03 is used by ac-mode-01,
specialkeys/out-02 is used by addobj-out-put,
specialkeys/out-03 is used by ac-out,
specialkeys/type-03 is used by add-putbar-rew, add-at-01,
specialkeys/type-04 is used by add-length,
specialkeys/type-05 is used by add-initundone, add-initerror, add-initdone-01, ac-type, ac-in-03,
specialkeys/type-06 is used by isobj-putbar-01, is_obj-put-equiv,
specialkeys/type-neq is used by isobj-put-03, isobj-put-02, is_valid_ref-put-equiv, is_valid_ref-put, is_obj-put-equiv,

Used from specification storefunsx

storefunsx/classOf is used by add-classof, add-class, ac-class,
storefunsx/init is used by addobj-init-01, ac-init-other, ac-init-first,
storefunsx/instore-inrefs is used by is_obj-union-disjoint,
storefunsx/nouninit is used by nouninit-addobj, nouninit-addclass,
storefunsx/refs-def is used by validref-notin-02, refcount-addobj, isobj-notin-03, add-refs,
storefunsx/refs-notin is used by is_obj-union-disjoint,
storefunsx/reftypep is used by add-reftype-02, add-reftype-01, add-reftype, ac-reftype,
storefunsx/uninit is used by ac-uninitset,
storefunsx/union-at-left is used by is_obj-union-disjoint, addobj-union-rew, addobj-union,
storefunsx/union-at-right-01 is used by is_obj-union, addobj-union-rew, addclass-union-sw,
storefunsx/eqmode-01 is used by eqmode-01,
storefunsx/lookup-xtra is used by stsubset-addobj, isobj-putbar, isobj-addclass, is_obj-union, is_obj-type, is_obj-subset, del-addobj, addobj-delsw, addclass-union-sw, addclass-okarray, addclass-exactarray, ac-okreftype, ac-okclass, ac-okarray-01, ac-okarray, ac-class,
storefunsx/nouninit-undone is used by nouninit-addobj,
storefunsx/refs-empty-01 is used by refcount-addobj, is_obj-union-disjoint,
storefunsx/refs-notin is used by isobj-notin-01,
storefunsx/refs-put is used by ac-refs,
storefunsx/reftype-02 is used by add-okclass-01,
storefunsx/reftype-jvmref is used by add-okclass-01,
storefunsx/union-at-left is used by addobj-union-rew, addobj-union, addclass-union-sw,
storefunsx/union-at-right-01 is used by isobj-union-01, is_obj-union-disjoint, addobj-union-rew, addobj-union,
storefunsx/union-at-right-03 is used by isobj-union,
storefunsx/union-in is used by isobj-union-01, addobj-union-rew, addobj-union, addclass-union-sw,
storefunsx/union-in-02 is used by isobj-union,
storefunsx/union-newref-02 is used by addobj-union-rew,
storefunsx/union-subset-left is used by isobj-union-disjoint,

Used from specification javastore

javastore/instore-02 is used by add-in-08,
javastore/at-other-16 is used by isobj-put-samefield-03, isobj-put-samefield-02, isobj-put-samefield-01, isobj-put-samefield, isobj-put-badfield, is_valid_ref-put-samefield-01, is_valid_ref-put-samefield, is_obj-put-samefield-01, is_obj-put-samefield, is_obj-put-equiv, is_obj-put-badfield, addobj-at-other-03, addobj-at-01,
javastore/at-other-20 is used by isobj-put-03, isobj-put-02, is_valid_ref-put, is_obj-put,
javastore/at-other-23 is used by isobj-put-badfield,
javastore/at-other-type is used by add-field-same-01,
javastore/in-01 is used by validref-put-01, isobj-putref, isobj-put-statfield, isobj-put-04, isobj-put-01, isobj-put, add-in-04, ac-in-03-02,
javastore/instore-02 is used by isobj-put-samefield-03, isobj-put-samefield-02, isobj-put-samefield-01, isobj-put-samefield, isobj-put-badfield, add-in-08, ac-in-06, ac-in-03,
javastore/look-ins is used by validref-put-01, isobj-putref, isobj-put-statfield, isobj-put-04, isobj-put-01, isobj-put, is_valid_ref-put-01, is_obj-put-statfield, is_obj-put-equiv, is_obj-put-01, addobj-at-01, add-ref, ac-lookup-04,
javastore/lookup-if is used by instore-addobj, addobj-mode-01, addobj-mode, add-type-01, add-type, add-notin, add-in-09, add-field-if, add-field-03, add-field-02, add-field-01, add-field, add-at-01, ac-type, ac-mode-01, ac-mode, ac-lookup-06, ac-lookup-05, ac-lookup-03, ac-lookup-02, ac-lookup-01, ac-lookup, ac-init-02, ac-init-01, ac-init,
javastore/shift-out is used by ac-out,
javastore/sk-01 is used by ac-in-02,
javastore/type is used by isobj-put-index-02, isobj-put-index-01,
javastore/type-at is used by isvalidref-put-array-badindex, isobj-put-index-02, isobj-put-index-01, is_obj-put-index,

Used from specification assoclist

assoclist/fieldinit/assoc-no is used by okfieldinits-at, ac-lookup,
assoclist/fieldinit/lookup-append is used by add-dupput,
assoclist/fieldinit/lookup-append-01 is used by add-dupput,
assoclist/fieldinit/put-no is used by add-gins, ac-shift-03,
assoclist/fieldinit/assoc-no is used by add-in-09,
assoclist/fieldinit/assoc-yes is used by okfieldinits-at, add-in-09, add-dupput, ac-lookup,
assoclist/fieldinit/cons is used by instore-addobj,
assoclist/fieldinit/empty is used by okfieldinits-at, okfieldinits-abstract, instore-addobj, add-nput, add-in-09, add-in-08, add-in-06, ac-type, ac-lookup, ac-init, ac-in-03, ac-in,
assoclist/fieldinit/in-02 is used by ac-init-07, ac-init-06,
assoclist/fieldinit/in-03 is used by add-dupput,
assoclist/fieldinit/in-04 is used by ac-init-10, ac-init-09,
assoclist/fieldinit/in-append is used by instore-addobj, addobj-at-other-03, add-type, add-nput-02, add-nput-01, add-nput, add-notin, add-in-08, add-dupput, ac-type, ac-mode-01, ac-lookup-06, ac-in-10, ac-in-03,
assoclist/fieldinit/in-assoclist-01 is used by isobj-addobj-04,
assoclist/fieldinit/inkeys-nc is used by okfieldinits-at, okfieldinits-abstract, add-in-09, add-in-06, ac-lookup-03, ac-lookup, ac-init-02, ac-init-01, ac-init, ac-in,
assoclist/fieldinit/inone is used by instore-addobj, addobj-at-other-03, add-type, add-nput-02, add-nput-01, add-nput, add-notin, add-in-08, add-dupput, ac-type, ac-mode-01, ac-lookup-06, ac-in-10, ac-in-03,
assoclist/fieldinit/inrec is used by ac-lookup-03, ac-init-02, ac-init-01, ac-init, ac-in,
assoclist/fieldinit/lookup is used by ac-init-07, ac-init-06,
assoclist/fieldinit/lookup-01 is used by ac-init-10, ac-init-09,
assoclist/fieldinit/not is used by instore-addobj,
assoclist/fieldinit/one-01 is used by add-dupput,
assoclist/fieldinit/put-empty is used by add-gins, ac-shift-03, ac-shift-02,
assoclist/fieldinit/put-no is used by add-gins-01,
assoclist/fieldinit/put-yes is used by add-gins, ac-shift-03, ac-shift-02,
assoclist/fieldinit/unique-e is used by instore-addobj,

Used from specification predefined

predefined/predef is used by instfields-Object,

Used from specification classname

classname/inj is used by add-field-same-02,

Used from specification nat-basic2

nat-basic2/a is used by refcount-addobj, addobj-getarray-01,
nat-basic2/c is used by refcount-addobj, addobj-getarray-01,
nat-basic2/s is used by addobj-getarray-01,

Used from specification initstate

initstate/disj-01 is used by ac-init-02, ac-init,
initstate/disj-02 is used by ac-init-01, ac-init,
initstate/disj-03 is used by add-initundone-01, add-initundone,

Used from specification set-union

set-union/references/ext is used by add-refs,
set-union/classnames/Delete is used by ac-init-first,
set-union/references/int-a is used by isobj-union-disjoint, is_obj-union-disjoint,
set-union/references/int-c is used by isobj-union-disjoint, is_obj-union-disjoint,
set-union/references/int-empty-02 is used by is_obj-union-disjoint,