[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 okbytearray-put-byteval-equiv, okarray-put-okval-01, okarray-put-okval, okarray-put-06, okarray-08, isarray-put-array-badindex, gft-out, gengft,
store/javastore/Del-at is used by onlymod-is-update,
store/javastore/Del-in is used by onlymod-is-update,
store/javastore/Extension is used by onlymod-is-update, copy-same-01-01, copy-same-01, copy-comp,
store/javastore/In-insert is used by update-keyin-01, update-keyin, okclass-03, hasKeys-put-01,
store/javastore/Subset is used by subset-okarray, subset-len-01, subset-len, subset-exactarray, okarray-substore, isarray-subset,
store/javastore/rew is used by update-putfis-sw, update-put-rew, update-put-notin, update-put,
store/javastore/subset-elem-eq is used by okreftype-subset-01, getarray-subset,
store/javastore/superset-elem-eq is used by okreftype-subset, okarray-subset, is_array-subset, good-field-subset, getbar-subset,
store/javastore/At-other is used by okarray-new, exactarray-new,
store/javastore/At-same is used by okbytearray-put-byteval-equiv, okarray-put-okval-01, okarray-put-okval, okarray-put-06, okarray-08, instore-afterputs, gengft,
store/javastore/Del-in is used by validFields-del, onlymod-is-update,
store/javastore/In-empty is used by validFields-empty-01,
store/javastore/In-insert is used by onlymod-is-update, okstore-out, okstore-other, okstore-mode, okstore-jvmref, okstore-03, okstore-02, okstore-01, okbytearray-put-byteval-equiv, okarray-put-okval-01, okarray-put-08, okarray-put-07, okarray-new, isarray-put-field, isarray-put-array-badindex, isarray-put, instore-afterputs, infis-notin-01, good-field-put, gft-out, gft-null, gft-not-01, gengft, exactarray-put-02, exactarray-put-01, exactarray-put, exactarray-new, exactarray-08,
store/javastore/In-store is used by okarray-union-03, okarray-union, okarray-type-01, okarray-substore, okarray-subset, okarray-putba, okarray-putar, okarray-put-okval-01, okarray-put-08, okarray-put-07, okarray-put-02, okarray-primput, okarray-onlymod, okarray-okarray, okarray-new-01, okarray-new, okarray-length-01, okarray-01, mode-02-01, instore-rec-03, instore-rec-01, instore-one, instore-null, instore-afterputs, inst-single, inst-in, infis-notin-01, infis-jvmref, exactarray-type-03, exactarray-putin, exactarray-putbar, exactarray-putar, exactarray-put-07, exactarray-put-03, exactarray-put-02, exactarray-put-01, exactarray-primput, exactarray-new-01, exactarray-new, exactarray-length-01, exactarray-in, exactarray-02-01, exactarray-01-01,
store/javastore/Size-empty is used by onlymod-is-update,
store/javastore/del-notin is used by onlymod-is-update,
store/javastore/empty is used by onlymod-is-update,
store/javastore/in-pair is used by okarray-union-03, okarray-union, okarray-substore, okarray-subset, okarray-putba, okarray-putar, okarray-put-okval-01, okarray-put-02, okarray-primput, okarray-onlymod, okarray-okarray-01, instore-rec-03, instore-one, instore-afterputs, inst-single, infis-notin-01, infis-jvmref, exactarray-putin, exactarray-putbar, exactarray-putar, exactarray-put-02, exactarray-primput,
store/javastore/ins-same is used by comp-same,
store/javastore/insin is used by okarray-new, gengft, exactarray-new,
store/javastore/insins is used by update-putfis-sw, update-put-same,
store/javastore/lookupisempty is used by onlymod-is-update,
store/javastore/notmemlookup is used by union-okarray, subset-okarray, onlymod-is-update, okstore-03, okbytearray-put-byteval-equiv, okbytearray-put-byteval, okbytearray-index-in, okarray-union-03, okarray-substore, okarray-putbar-same-03, okarray-putbar-01, okarray-put-08, isarray-put-field, isarray-put-array-badindex, is_array-union, is_array-type-02, is_array-subset, infis-notin-01, good-field-put, getbar-subset, getarray-subset, exactarray-put-01, comp-same,
store/javastore/size is used by onlymod-is-update,
store/javastore/subset-elem-eq-02 is used by okarray-subset,
store/javastore/superset-elem-in-01 is used by subset-exactarray, okreftype-subset-01, okreftype-subset, okarray-subset, good-field-subset,

Used from specification list

list/fieldinit-assoclista/One is used by inst-single,
list/javavalues/Last is used by okbytearray,
list/storekeys/Last is used by keys-put-notin,
list/fieldinit-assoclista/Nil is used by getkeys-app,
list/references/Nil is used by nonnullrefs-dups-key,
list/storekeys/Nil is used by hasKeys-app, getkeys-app,
list/storekeys/a is used by validFields-rec, validFields-fis, validFields-empty-01, nonnullrefs-in-key, nonnullrefs-dups-key, keys-put-notin, keys-put-in, keys-length, keys-in, keys-empty, keys-at, isarray-length-06, isarray-length-05, isarray-length-04, isarray-length-03, is_array-length-06, is_array-length-05, is_array-length-04, is_array-length-03, is_array-length-02, is_array-keyin, hasKeys-put-02, hasKeys-put-01, hasKeys-put, hasKeys-one, hasKeys-app, hasKeys-all, good-rec-01, good-one, gfts-put, gfts-null, gfts-not-01, gfts-in, gfts-all, getkeys-one, getkeys-app, gengfts, dups-fis-keys,
list/refkeyvalues-assoclista/a is used by okbytearray-put-field-03, okbytearray-put-byteval,
list/fieldinit-assoclista/a is used by vals-one, vals-length, vals-in, vals-at, validFields-rec, validFields-fis, validFields-empty-01, validFields-del, update-union-switch, update-refs, update-rec-02, update-rec-01, update-putfis-sw, update-put-same, update-put-rew, update-put-notin, update-put, update-one, update-newref, update-mode, update-length, update-keyin-01, update-keyin, update-init-01, update-init, update-in-03, update-ex-nodups, update-atin, update-at-notin, update-at, onlymod-is-update, okarrays-put-02, okarrays-put, okarrays-one-01, okarrays-not, okarrays-all, okarray-update, nonnullrefs-in-key, nonnullrefs-in, nonnullrefs-dups-key, nonnullrefs-dups, keys-put-notin, keys-put-in, keys-length, keys-in, keys-empty, keys-at, instore-rec-01, instore-one, instore-afterputs, inst-single, infis-notin-01, infis-jvmref, getvals-rec-01, getkeys-one, getkeys-app, getbar-update-01, getbar-update, dups-fis-keys,
list/references/a is used by nonnullrefs-in-key, nonnullrefs-in, nonnullrefs-dups-key, nonnullrefs-dups,
list/javavalues/a is used by vals-one, vals-length, vals-in, vals-at, okbytearray, nonnullrefs-in-key, nonnullrefs-in, nonnullrefs-dups-key, nonnullrefs-dups, getvals-rec-01,
list/bytelist/a is used by okbar-putbar-same, okarray-putbar-same-02, okarray-putbar-same-01, okarray-putbar-same, isarray-putbar,
list/javavalues/app is used by vals-one,
list/fieldinit-assoclista/app is used by vals-one, update-one, okarrays-one-01, instore-one, instore-afterputs, inst-single,
list/storekeys/app is used by hasKeys-one, good-one,
list/storekeys/app-01 is used by keys-put-notin, keys-put-in, getkeys-app,
list/javavalues/app-01 is used by getvals-rec-01,
list/javavalues/app-02-ant is used by vals-at,
list/fieldinit-assoclista/app-02-ant is used by update-in-03,
list/storekeys/app-02-ant is used by keys-empty, keys-at, isarray-length-05, isarray-length-03,
list/bytelist/app-02-ant is used by okbar-putbar-same, okarray-putbar-same-02, okarray-putbar-same-01, okarray-putbar-same, isarray-putbar,
list/storekeys/app-03 is used by getkeys-one,
list/storekeys/c is used by hasKeys-put-02, hasKeys-put-01, hasKeys-put, hasKeys-app, hasKeys-all, gfts-put, gfts-null, gfts-not-01, gfts-in, gfts-all, gengfts,
list/fieldinit-assoclista/c is used by vals-length, vals-in, vals-at, validFields-empty-01, validFields-del, update-union-switch, update-refs, update-rec-02, update-putfis-sw, update-put-same, update-put-rew, update-put-notin, update-put, update-newref, update-mode, update-length, update-keyin-01, update-keyin, update-init-01, update-init, update-in-03, update-ex-nodups, update-atin, update-at-notin, update-at, onlymod-is-update, okarrays-put-02, okarrays-put, okarrays-not, okarrays-all, okarray-update, nonnullrefs-in-key, nonnullrefs-in, nonnullrefs-dups-key, nonnullrefs-dups, keys-put-in, keys-length, keys-in, keys-empty, keys-at, instore-null, instore-afterputs, inst-single, inst-in, infis-notin-01, infis-jvmref, getkeys-app, getbar-update-01, getbar-update,
list/bytelist/c is used by okbar-putbar-same, okarray-putbar-same-02, okarray-putbar-same-01, okarray-putbar-same, isarray-putbar,
list/references/c is used by nonnullrefs-in, nonnullrefs-dups,
list/javavalues/c-07 is used by vals-at,
list/bytelist/c-07 is used by okbar-putbar-same, okarray-putbar-same-02, okarray-putbar-same-01, okarray-putbar-same, isarray-putbar,
list/storekeys/c-07 is used by keys-at,
list/bytelist/c-08 is used by okbar-putbar-same, okarray-putbar-same-02, okarray-putbar-same-01, okarray-putbar-same, isarray-putbar,
list/javavalues/e is used by vals-at,
list/storekeys/e is used by keys-put-in, keys-empty, keys-at, isarray-length-05, isarray-length-03,
list/bytelist/e is used by okbar-putbar-same, okarray-putbar-same-02, okarray-putbar-same-01, okarray-putbar-same, isarray-putbar,
list/fieldinit-assoclista/e is used by update-in-03,
list/javavalues/e-01 is used by vals-at,
list/fieldinit-assoclista/e-01 is used by vals-at, validFields-empty-01, update-rec-02, keys-at,
list/storekeys/e-01 is used by keys-at, isarray-length-05,
list/bytelist/e-01 is used by okbar-putbar-same, okarray-putbar-same-02, okarray-putbar-same-01, okarray-putbar-same, isarray-putbar,
list/storekeys/e-02 is used by isarray-length-03,
list/storekeys/in-06 is used by hasKeys-put-02, gfts-null, gfts-all,
list/fieldinit-assoclista/in-06 is used by vals-in, update-ex-nodups,
list/references/in-06 is used by nonnullrefs-in,
list/javavalues/in-17 is used by vals-in, okbytearray,
list/storekeys/in-17 is used by keys-in, hasKeys-all, gfts-in,
list/fieldinit-assoclista/in-17 is used by okarrays-all,
list/references/in-17 is used by nonnullrefs-in-key,
list/storekeys/in-append is used by keys-in, hasKeys-all, gfts-in,
list/references/in-append is used by nonnullrefs-in-key,
list/javavalues/in-append is used by vals-in, okbytearray,
list/fieldinit-assoclista/in-append is used by okarrays-all,
list/javavalues/in-empty is used by vals-in, okbytearray,
list/storekeys/in-empty is used by keys-in, hasKeys-all, gfts-in,
list/fieldinit-assoclista/in-empty is used by vals-in, okarrays-all,
list/references/in-empty is used by nonnullrefs-in-key,
list/javavalues/len is used by vals-length,
list/fieldinit-assoclista/len is used by vals-length, vals-at, keys-length, keys-at,
list/storekeys/len is used by keys-length,
list/javavalues/len-02 is used by vals-length,
list/fieldinit-assoclista/len-02 is used by vals-length, vals-at, keys-length, keys-at,
list/storekeys/len-02 is used by keys-length,

Used from specification storefuns

storefuns/instore-02 is used by update-in-03, okclass-03,
storefuns/lookup-last-rec is used by okbytearray-is-byte, isarray-length-05, isarray-length-03, isarray-length-02,
storefuns/lookup-two is used by isarray-keyin,
storefuns/put-rkvs-switch-01 is used by okbytearray-put-field-03, okbytearray-put-byteval,
storefuns/in-del is used by okarray-del, isarray-del-01, isarray-del, good-field-del,
storefuns/in-empty is used by onlymod-is-update,
storefuns/in-put-rkvs is used by okbytearray-put-byteval,
storefuns/init-put is used by update-init,
storefuns/init-put-01 is used by update-init-01,
storefuns/instore-01 is used by validFields-rec, validFields-putfis, validFields-fis, validFields-del, update-length, union-okarray, subset-okarray, subset-len-01, subset-len, subset-exactarray, onlymod-is-update, okstore-out, okstore-03, okreftype-union, okreftype-subset-01, okreftype-subset, okreftype-put, okreftype-notin, okclass-int, okclass-copy, okclass-03, okbytearray-put-field, okbytearray-put-byteval-equiv, okbytearray-put-byteval, okbytearray-not, okbytearray-index-in, okbytearray, okbar-putbar, okbar-norefval, okbar-byteval, okarray-union-03, okarray-union, okarray-supertype, okarray-substore, okarray-subset, okarray-putbar-same-03, okarray-putbar-other, okarray-putbar-01, okarray-putba, okarray-putar, okarray-put-samefield-01, okarray-put-other, okarray-put-okval-01, okarray-put-okval, okarray-put-badfield, okarray-put-08, okarray-put-07, okarray-put-06, okarray-put-02, okarray-primput, okarray-onlymod, okarray-okarray-01, okarray-okarray, okarray-new, okarray-length-01, okarray-getbar-len, okarray-del, okarray-copy-01, okarray-copy, okarray-byte-01, okarray-byte, okarray-08, okarray-05, okarray-01, mode, isarray-update, isarray-union, isarray-type-02, isarray-type-01, isarray-subset, isarray-reftype, isarray-putbar, isarray-put-samefield-01, isarray-put-samefield, isarray-put-okval, isarray-put-jvmref, isarray-put-field, isarray-put-array-badindex, isarray-put, isarray-okval, isarray-okreftype, isarray-okarray-01, isarray-okarray, isarray-notin-01, isarray-notin, isarray-length-07, isarray-lenfield, isarray-keyin, isarray-isarrayref, isarray-bytearray, isarray-arrayreftype, isarray-abstract, is_array-union-disjoint, is_array-primtype-01, is_array-nottypeex, is_array-norefval, is_array-noreftype, is_array-byte-noref, is_array-abstract, intval-01, instore-null, instore-afterputs, inst-single, inst-in, infis-jvmref, hasKeys-put-01, hasKeys-app, hasKeys-all, good-field-subset, gft-not-01, getintarray-subset, getbar-subset, getarray-subset-02, getarray-subset, gengft, exactarray-type-03, exactarray-putin, exactarray-putbar, exactarray-putar, exactarray-put-06, exactarray-put-05, exactarray-put-03, exactarray-put-02, exactarray-put-01, exactarray-put, exactarray-primput, exactarray-new, exactarray-lenin, exactarray-length-01, exactarray-in, exactarray-copy-01, exactarray-copy, exactarray-08, exactarray-06, exactarray-02-01, exactarray-01-01, copy-comp, byteval,
storefuns/instore-02 is used by okstore-other, okstore-jvmref, okstore-03, okstore-02, okstore-01, okarray-put-07, okarray-copy-01, exactref-put-01, exactarray-putin, exactarray-put-07, exactarray-put-06, exactarray-put-05, exactarray-put-03, exactarray-put-02, exactarray-put-01, exactarray-put, exactarray-primput, exactarray-08, exactarray-06, exactarray-02-01,
storefuns/look-del is used by okarray-del, isarray-del, is_array-del, good-field-del,
storefuns/lookup-put-rkvs-notin is used by okbytearray-put-byteval,
storefuns/mode-01 is used by okstore-mode, mode-02-01,
storefuns/mode-notin is used by okstore-08,
storefuns/newref-01 is used by okbar-new, okarray-new, isarray-newref, exactarray-new,
storefuns/newref-02 is used by update-newref,
storefuns/newref-03 is used by okbar-new, okarray-new, exactarray-new-01, exactarray-new,
storefuns/newref-in-02 is used by okarray-new-01, isarray-newref,
storefuns/put-rkvs-absorb-01 is used by okbytearray-put-field-03, okbytearray-put-byteval,
storefuns/ref-in is used by okstore-out,
storefuns/refin is used by okbytearray-put-field, okbytearray-put-byteval-equiv, okarray-put-samefield-01, isarray-put-samefield-01, exactarray-primput, exactarray-new,

Used from specification int-basic2

int-basic2/add-a is used by okbytearray, okarray-putbar-same-03, okarray-copy-01, okarray-byte-01, getbytearray-mkjavavalues, exactarray-copy-01, copy-same-02, copy-same-01-01, copy-same-01, copy-same, copy-comp, comp-same, byteval-01, byteval,
int-basic2/add-c is used by okbytearray, okbar-putbar-same, okarray-putbar-same-03, okarray-putbar-same-02, okarray-putbar-same-01, okarray-copy-01, okarray-byte-01, getbytearray-mkjavavalues, getarray-subset-02, exactarray-copy-01, copy-same-02, copy-same-01-01, copy-same-01, copy-same, copy-comp, comp-same, bytevalues-eq, byteval-01, byteval,
int-basic2/add-in is used by copy-comp,
int-basic2/add-less is used by copy-comp,
int-basic2/ax-04 is used by okbytearray, okarray-copy-01, getbytearray-mkjavavalues, copy-comp,
int-basic2/ls is used by okbytearray, copy-same-01-01, copy-same-01, copy-comp,
int-basic2/ls-01 is used by okarray-byte-01, copy-comp, byteval,
int-basic2/ls-02 is used by copy-comp,
int-basic2/lst-04 is used by copy-comp,
int-basic2/zero-02 is used by okbytearray, copy-comp,

Used from specification valuefuns

valuefuns/init_val_byte is used by oktype-03,
valuefuns/init_val_short is used by oktype-03,
valuefuns/okval-refval is used by is_array-primtype-01,
valuefuns/val2int-int-01 is used by okarray-length-02, okarray-length-01, isarray-length, exactarray-length-01,
valuefuns/init_val_abst is used by oktype-03,
valuefuns/init_val_array is used by oktype-03,
valuefuns/init_val_bool is used by oktype-03,
valuefuns/init_val_char is used by oktype-03,
valuefuns/init_val_class is used by oktype-03,
valuefuns/init_val_double is used by oktype-03,
valuefuns/init_val_float is used by oktype-03,
valuefuns/init_val_int is used by oktype-03,
valuefuns/init_val_long is used by oktype-03,
valuefuns/init_val_void is used by oktype-03,
valuefuns/intval-xtra is used by okarray-union-03, okarray-subset, okarray-put-07, okarray-put-02, okarray-primput, okarray-onlymod, okarray-okarray, okarray-length-02, okarray-length-01, okarray-intval-01, isarray-length, exactarray-put-02, exactarray-primput, exactarray-length-01, exactarray-intval-01, exactarray-in,
valuefuns/okprim-letype is used by okarray-primput,
valuefuns/okprimtype-abstract is used by okprim-oktype,
valuefuns/okprimtype-array is used by okprim-oktype,
valuefuns/okprimtype-bool is used by okprim-oktype,
valuefuns/okprimtype-byte is used by okprim-oktype, okarray-put-02,
valuefuns/okprimtype-char is used by okprim-oktype,
valuefuns/okprimtype-class is used by okprim-oktype,
valuefuns/okprimtype-double is used by okprim-oktype,
valuefuns/okprimtype-float is used by okprim-oktype,
valuefuns/okprimtype-int is used by okprim-oktype,
valuefuns/okprimtype-long is used by okprim-oktype,
valuefuns/okprimtype-short is used by okprim-oktype,
valuefuns/okprimtype-void is used by okprim-oktype,
valuefuns/okval-abstract is used by okval-oktype,
valuefuns/okval-array is used by okval-oktype, oktype-okval,
valuefuns/okval-bool is used by okval-oktype, oktype-okval,
valuefuns/okval-byte is used by okval-oktype, oktype-okval, isarray-put-byte,
valuefuns/okval-char is used by okval-oktype, oktype-okval,
valuefuns/okval-class is used by okval-oktype, oktype-okval,
valuefuns/okval-double is used by okval-oktype, oktype-okval,
valuefuns/okval-float is used by okval-oktype, oktype-okval,
valuefuns/okval-int is used by okval-oktype, oktype-okval,
valuefuns/okval-long is used by okval-oktype, oktype-okval,
valuefuns/okval-noval is used by isarray-put-array-badindex,
valuefuns/okval-reftype is used by oktype-reftype, isarray-okarray, is_array-norefval,
valuefuns/okval-refval-01 is used by isarray-arrayrefval, is_array-noreftype,
valuefuns/okval-short is used by okval-oktype, oktype-okval,
valuefuns/okval-subtype-01 is used by isarray-arrayreftype,
valuefuns/okval-supertype is used by okarray-supertype,
valuefuns/okval-void is used by okval-oktype, oktype-okval,
valuefuns/refval-xtra is used by okarray-update-01, okarray-union-03, okarray-subset, okarray-refval, okarray-putba, okarray-okarray-01, okarray-getbar-len, isarray-length-05, isarray-length-03, isarray-length-02, isarray-keyin, exactarray-put-02,
valuefuns/typeval-xtra is used by isarray-put-okval, is_array-notypeval,
valuefuns/val2int-int is used by okarray-length-01, exactarray-length-01,
valuefuns/val2int-int-01 is used by exactarray-length,

Used from specification valuesfuns

valuesfuns/bytevals-inj is used by getbytearray-mkjavavalues,
valuesfuns/bytevalues-eq is used by bytevalues-eq,
valuesfuns/isbytelist-all is used by getbytearray-mkjavavalues,
valuesfuns/nonnullrefs-no is used by nonnullrefs-in, nonnullrefs-dups,
valuesfuns/nonnullrefs-one-no is used by nonnullrefs-in-key, nonnullrefs-dups-key,
valuesfuns/nonnullrefs-append is used by nonnullrefs-in-key, nonnullrefs-dups-key,
valuesfuns/nonnullrefs-empty is used by nonnullrefs-in-key, nonnullrefs-dups-key,
valuesfuns/nonnullrefs-null is used by nonnullrefs-in-key,
valuesfuns/nonnullrefs-ok is used by nonnullrefs-in,
valuesfuns/nonnullrefs-one-yes is used by nonnullrefs-in-key, nonnullrefs-dups-key,
valuesfuns/nonnullrefs-yes is used by nonnullrefs-in, nonnullrefs-dups,

Used from specification int-div

int-div/divmod-rew is used by copy-comp,
int-div/mod-zero-03 is used by copy-comp,
int-div/div-elim-pospos is used by copy-comp,

Used from specification fieldspec

fieldspec/elim is used by okarrays-rec-01, okarrays-put-02, okarrays-put, okarrays-one-01, okarrays-not, okarrays-all, okarray-put-samefield-01, isarray-put-samefield-01, isarray-put-samefield, good-field-subset, good-field-put, good-field-field-03, gfts-not, gft-out, gft-not-01, gft-not, gengfts, gengft, exactarray-put-01,
fieldspec/inj is used by okarrays-all, gengft,
fieldspec/inj-01 is used by okarrays-not, gft-not-01, gengft,
fieldspec/sel-03 is used by okarrays-rec-01, okarrays-one-01, okarrays-all, isarray-put-samefield-01, isarray-put-samefield, gengfts, gengft,

Used from specification intnat

intnat/num-n2i-ls-06 is used by getbytearray-mkjavavalues, getarray-subset,
intnat/abs-eq is used by okbar-bytes2int-same, getarray-subset,
intnat/abs-succ-03 is used by okbytearray,
intnat/abs-zero is used by getbytearray-mkjavavalues, getarray-subset,
intnat/i2i-pos-01 is used by okbytearray-getarray-length,
intnat/labs is used by okbytearray, okarray-copy-01,
intnat/n2n is used by okarray-getbar-len,
intnat/nat2int is used by getbytearray-mkjavavalues, getarray-subset,
intnat/nat2int-08 is used by getarray-subset,
intnat/num-n2i-ls-02 is used by getbytearray-mkjavavalues, getarray-subset,
intnat/pos-int is used by getbytearray-mkjavavalues,
intnat/rax-04 is used by okarray-copy-01,

Used from specification int-abs

int-abs/numadd-01 is used by copy-comp,
int-abs/sub-add-01 is used by copy-comp,
int-abs/sub-sub is used by copy-comp,
int-abs/Sub-def is used by copy-comp,
int-abs/abs-16 is used by okbytearray,
int-abs/absle is used by okbar-bytes2int-same, okarray-copy-01, getarray-subset,
int-abs/anti is used by okarray-copy-01,
int-abs/bet is used by okbytearray,
int-abs/elim-sub is used by okbytearray, okarray-copy-01, copy-comp,
int-abs/forward-le is used by isarray-isarrayref, getarray-subset-02, copy-comp,
int-abs/forward-le-01 is used by union-okarray, subset-okarray, subset-len-01, subset-len, subset-exactarray, okbytearray-put-field, okbytearray-put-byteval-equiv, okbytearray-put-byteval, okbytearray-not, okbytearray-is-byte, okbytearray-index-in, okbytearray, okbar-putbar, okbar-put-01, okbar-norefval, okbar-byteval, okarray-union-03, okarray-union, okarray-supertype, okarray-substore, okarray-subset, okarray-putbar-same-03, okarray-putbar-other, okarray-putbar-01, okarray-putba, okarray-putar, okarray-put-samefield-01, okarray-put-other, okarray-put-okval-01, okarray-put-okval, okarray-put-badfield, okarray-put-08, okarray-put-07, okarray-put-06, okarray-put-02, okarray-primput, okarray-onlymod, okarray-okarray-01, okarray-okarray, okarray-new, okarray-length-01, okarray-intval, okarray-int-put-02, okarray-getbar-len, okarray-del, okarray-copy-01, okarray-copy, okarray-byte-01, okarray-byte, okarray-08, okarray-05, okarray-01, isarray-update, isarray-putbar, isarray-put-field, isarray-put-array-badindex, isarray-put, isarray-okval, isarray-okarray, isarray-notin-01, isarray-keyin, isarray-isarrayref, isarray-arrayrefval, isarray-arrayreftype, is_array-primtype-01, is_array-norefval, is_array-noreftype, is_array-byte-noref, intval-01, getbar-subset, getarray-subset-02, getarray-subset, exactarray-putbar, exactarray-putar, exactarray-put-06, exactarray-put-05, exactarray-put-02, exactarray-put, exactarray-primput, exactarray-lenin, exactarray-in, exactarray-copy-01, exactarray-copy, exactarray-08, exactarray-06, copy-same-01-01, copy-comp, comp-same, bytevalues-eq, byteval-01, byteval,
int-abs/forward-le-02 is used by okbytearray-put-byteval-equiv, okbytearray, okbar-len, okarray-len, isarray-put-array-badindex, isarray-length-05, isarray-length-03, isarray-length-02, isarray-len, getarray-subset, exactarray-length, exactarray-len, copy-comp,
int-abs/forward-le-05 is used by union-okarray, subset-okarray, subset-exactarray, okbytearray-put-field, okbytearray-put-byteval-equiv, okbytearray-not, okbytearray-length-zero, okbytearray-is-byte, okbytearray-index-in, okbytearray, okbar-putbar, okbar-put-01, okbar-norefval, okbar-byteval, okarray-union-03, okarray-union, okarray-supertype, okarray-substore, okarray-subset, okarray-putbar-same-03, okarray-putbar-other, okarray-putbar-01, okarray-putba, okarray-putar, okarray-put-other, okarray-put-okval-01, okarray-put-okval, okarray-put-badfield, okarray-put-08, okarray-put-07, okarray-put-06, okarray-put-02, okarray-primput, okarray-onlymod, okarray-okarray-01, okarray-okarray, okarray-int-put-02, okarray-del, okarray-copy, okarray-byte, okarray-08, isarray-update, isarray-putbar, isarray-put-field, isarray-put-array-badindex, isarray-put, isarray-okval, isarray-okarray, isarray-notin-01, isarray-keyin, isarray-isarrayref, isarray-arrayrefval, isarray-arrayreftype, isarray-abstract, is_array-primtype-01, is_array-norefval, is_array-noreftype, is_array-byte-noref, getbytearray-mkjavavalues, getbar-subset, getarray-subset-02, getarray-subset, exactarray-putbar, exactarray-putar, exactarray-put-02, exactarray-put, exactarray-primput, exactarray-lenin, exactarray-in, exactarray-copy-01, exactarray-08, copy-comp, byteval-01,
int-abs/forward-lele is used by okbytearray-put-byteval-equiv, copy-same-01, copy-comp, comp-same,
int-abs/forward-lels is used by okbytearray-put-byteval, okbytearray-is-byte, okbytearray, okarray-intval, okarray-byte, isarray-keyin, is_array-norefval, is_array-noreftype, intval-01, exactarray-copy-01, copy-same-01-01, copy-same-01, copy-comp, comp-same,
int-abs/forward-lsle is used by okbytearray-put-byteval-equiv, okbytearray, okarray-byte-01, isarray-put-array-badindex, isarray-isarrayref, getbytearray-mkjavavalues, getarray-subset-02, getarray-subset, copy-comp, byteval,
int-abs/le-add is used by copy-same-01-01, copy-comp, comp-same,
int-abs/lels is used by union-okarray, subset-okarray, subset-len, subset-exactarray, okbytearray-put-field, okbytearray-put-byteval-equiv, okbytearray-put-byteval, okbytearray-not, okbytearray-is-byte, okbytearray-index-in-zero, okbytearray-index-in, okbytearray, okbar-putbar, okbar-norefval, okbar-byteval, okarray-union-03, okarray-union, okarray-type-01, okarray-supertype, okarray-substore, okarray-subset, okarray-putbar-same-03, okarray-putbar-other, okarray-putbar-01, okarray-putba, okarray-putar, okarray-put-samefield-01, okarray-put-other, okarray-put-okval-01, okarray-put-okval, okarray-put-badfield, okarray-put-08, okarray-put-07, okarray-put-06, okarray-put-02, okarray-primput, okarray-onlymod, okarray-okarray-01, okarray-okarray, okarray-new, okarray-length-01, okarray-getbar-len, okarray-del, okarray-copy-01, okarray-copy, okarray-byte-01, okarray-byte, okarray-08, okarray-05, okarray-01, isarray-update, isarray-putbar, isarray-put-field, isarray-put-array-badindex, isarray-put, isarray-okval, isarray-okarray, isarray-notin-01, isarray-keyin, isarray-isarrayref, isarray-arrayrefval, isarray-arrayreftype, isarray-abstract, is_array-primtype-01, is_array-norefval, is_array-noreftype, is_array-byte-noref, intval-01, getbytearray-mkjavavalues, getbar-subset, getarray-subset-02, getarray-subset, exactarray-putbar, exactarray-putar, exactarray-put-02, exactarray-put, exactarray-lenin, exactarray-in, exactarray-copy-01, exactarray-08, copy-same-01-01, copy-same-01, copy-comp, comp-same, byteval-01, byteval,
int-abs/lels-01 is used by union-okarray, subset-okarray, subset-len, subset-exactarray, short-length-01, short-length, okbytearray-put-field, okbytearray-put-byteval-equiv, okbytearray-put-byteval, okbytearray-not, okbytearray-length-zero, okbytearray-is-byte, okbytearray-index-in, okbytearray-getarray-length, okbytearray, okbar-putbar, okbar-norefval, okbar-byteval, okbar-bytes2int-same, okarray-union-03, okarray-union, okarray-type-01, okarray-supertype, okarray-substore, okarray-subset, okarray-putbar-same-03, okarray-putbar-other, okarray-putbar-01, okarray-putba, okarray-putar, okarray-put-samefield-01, okarray-put-other, okarray-put-okval-01, okarray-put-okval, okarray-put-badfield, okarray-put-08, okarray-put-07, okarray-put-06, okarray-put-02, okarray-primput, okarray-onlymod, okarray-okarray-01, okarray-okarray, okarray-new, okarray-length-01, okarray-getbar-len, okarray-del, okarray-copy-01, okarray-copy, okarray-byte-01, okarray-byte, okarray-08, okarray-05, okarray-01, isarray-update, isarray-putbar, isarray-put-field, isarray-put-array-badindex, isarray-put, isarray-okval, isarray-okarray, isarray-notin-01, isarray-keyin, isarray-isarrayref, isarray-arrayrefval, isarray-arrayreftype, isarray-abstract, is_array-primtype-01, is_array-norefval, is_array-noreftype, is_array-byte-noref, intval-01, getbytearray-mkjavavalues, getbar-subset, getarray-subset-02, getarray-subset, exactarray-putbar, exactarray-putar, exactarray-put-06, exactarray-put-02, exactarray-put, exactarray-lenin, exactarray-in, exactarray-copy-01, exactarray-08, copy-same-01-01, copy-same-01, copy-comp, comp-same, bytevalues-eq, byteval-01, byteval,
int-abs/lels-02 is used by okbytearray-length-zero, okbytearray-index-in-zero, isarray-abstract, getbytearray-mkjavavalues, getarray-subset, copy-comp,
int-abs/lels-03 is used by union-okarray, subset-okarray, subset-exactarray, okbytearray-put-field, okbytearray-put-byteval-equiv, okbytearray-put-byteval, okbytearray-not, okbytearray-index-in, okbytearray, okbar-putbar, okbar-norefval, okbar-byteval, okarray-union-03, okarray-union, okarray-supertype, okarray-substore, okarray-subset, okarray-putbar-same-03, okarray-putbar-other, okarray-putbar-01, okarray-putba, okarray-putar, okarray-put-samefield-01, okarray-put-other, okarray-put-okval-01, okarray-put-okval, okarray-put-badfield, okarray-put-08, okarray-put-07, okarray-put-06, okarray-put-02, okarray-primput, okarray-onlymod, okarray-okarray-01, okarray-okarray, okarray-len, okarray-del, okarray-copy-01, okarray-copy, okarray-byte, okarray-08, isarray-update, isarray-putbar, isarray-put-field, isarray-put-array-badindex, isarray-put, isarray-okval, isarray-okarray, isarray-notin-01, isarray-isarrayref, isarray-arrayrefval, isarray-arrayreftype, is_array-primtype-01, is_array-norefval, is_array-noreftype, is_array-byte-noref, intval-01, getbytearray-mkjavavalues, getbar-subset, getarray-subset-02, exactarray-putbar, exactarray-putar, exactarray-put-02, exactarray-put, exactarray-lenin, exactarray-len, exactarray-in, exactarray-copy-01, exactarray-08, copy-same-01-01, copy-same-01, copy-comp, comp-same, byteval-01,
int-abs/lels-04 is used by union-okarray, subset-okarray, subset-exactarray, okbytearray-put-field, okbytearray-put-byteval-equiv, okbytearray-put-byteval, okbytearray-not, okbytearray-is-byte, okbytearray-index-in, okbytearray, okbar-putbar, okbar-norefval, okbar-byteval, okarray-union-03, okarray-union, okarray-supertype, okarray-substore, okarray-subset, okarray-putbar-same-03, okarray-putbar-other, okarray-putbar-01, okarray-putba, okarray-putar, okarray-put-samefield-01, okarray-put-other, okarray-put-okval-01, okarray-put-okval, okarray-put-badfield, okarray-put-08, okarray-put-07, okarray-put-06, okarray-put-02, okarray-primput, okarray-onlymod, okarray-okarray-01, okarray-okarray, okarray-del, okarray-copy-01, okarray-copy, okarray-byte-01, okarray-byte, okarray-08, isarray-update, isarray-putbar, isarray-put-field, isarray-put-array-badindex, isarray-put, isarray-okval, isarray-okarray, isarray-notin-01, isarray-keyin, isarray-isarrayref, isarray-arrayrefval, isarray-arrayreftype, is_array-primtype-01, is_array-norefval, is_array-noreftype, is_array-byte-noref, intval-01, getbar-subset, getarray-subset-02, getarray-subset, exactarray-putbar, exactarray-putar, exactarray-put-02, exactarray-put, exactarray-lenin, exactarray-length, exactarray-in, exactarray-copy-01, exactarray-08, copy-same-01-01, copy-same-01, copy-comp, comp-same, bytevalues-eq, byteval-01, byteval,
int-abs/lep is used by copy-same-01-01, copy-same-01, copy-comp,
int-abs/lep-02 is used by copy-same-01,
int-abs/ler is used by copy-comp,
int-abs/minus-ass is used by copy-comp,
int-abs/minus-sub is used by copy-comp,
int-abs/mone-06 is used by okarray-copy-01, copy-comp,
int-abs/neg-07 is used by copy-comp,
int-abs/numle-02 is used by okarray-copy-01, copy-comp,
int-abs/numleledel is used by short-length-01, short-length,
int-abs/numleledel-01 is used by okarray-copy-01, copy-comp,
int-abs/numls-02 is used by okbytearray, okarray-copy-01, copy-comp,
int-abs/numsub is used by okbytearray, okarray-copy-01,
int-abs/sub-add-01 is used by copy-same-01-01, copy-same-01, copy-comp,
int-abs/sub-add-06 is used by copy-comp,
int-abs/sub-add-09 is used by copy-comp,
int-abs/sub-eq is used by copy-comp,
int-abs/sub-eq-01 is used by copy-comp,
int-abs/sub-le is used by copy-comp,
int-abs/sub-le-01 is used by copy-comp,
int-abs/sub-ls is used by copy-comp,
int-abs/sub-ls-01 is used by copy-comp,
int-abs/sub-sub-03 is used by copy-comp,
int-abs/sub-sub-04 is used by copy-comp,
int-abs/sub-zero-01 is used by copy-comp,
int-abs/succ-01 is used by okbytearray, okarray-copy-01, copy-comp,
int-abs/succ-02 is used by copy-comp,
int-abs/zero-gels-01 is used by okbytearray-put-byteval-equiv, okbytearray, okarray-union-03, isarray-put-array-badindex, getarray-subset, copy-comp,
int-abs/zero-gels-04 is used by okbytearray-put-byteval-equiv, okarray-primput, copy-same-01-01, copy-comp,
int-abs/zero-gs is used by okarray-copy-01, comp-same,

Used from specification storekey

storekey/ex-03 is used by okarray-put-08,
storekey/ex-04 is used by okarrays-put, good-field-index, gft-not-01,
storekey/disj is used by copy-same-01-01, copy-same-01,
storekey/elim-03 is used by okbytearray-put-field-04, okarrays-not, good-field-subset, good-field-field, gfts-not, gft-not-01, gft-not, gengft,
storekey/inj-03 is used by okarrays-not, gft-not-01, gengft,
storekey/inj-04 is used by okbytearray-put-byteval-equiv, okarray-put-okval-01, okarray-put-okval, okarray-put-06, okarray-put-02, okarray-primput, okarray-08, isarray-put-array-badindex, exactarray-put-02, exactarray-put, exactarray-08, copy-same-01-01, copy-same-01,
storekey/sel-05 is used by okarrays-put-02, gft-out, gengft, exactarray-put-01,
storekey/sel-06 is used by okarray-putbar-same-03,
storekey/test is used by okarrays-rec-01, okarrays-put, okarrays-not, okarrays-all, okarray-putbar-same-03, good-field-put, good-field-in,
storekey/test-01 is used by okarrays-rec-01, okarrays-put-02, okarrays-put, okarrays-one-01, okarrays-one, okarrays-not, okarrays-all, mode-01, goodfields-putba, good-rec-01, good-field-subset, good-field-rew, good-field-put, good-field-in-01, good-field-in, good-field-del, good-field-def, gft-union, gft-put, gft-out, gft-null, gft-not-01, gengft,
storekey/test-02 is used by okarrays-rec-01, okarrays-put-02, okarrays-put, okarrays-one-01, okarrays-one, okarrays-not, okarrays-all, mode-01, goodfields-putba, good-rec-01, good-field-rew, good-field-put, good-field-del, gft-union, gft-put, gft-null,
storekey/test-05 is used by okarrays-put-02, okarrays-not, good-field-subset, gfts-not, gft-out, gft-not-01, gft-not, gengft, exactarray-put-01,
storekey/test-06 is used by okarrays-put-02, good-field-put, gft-out, exactarray-put-01,
storekey/test-07 is used by okarrays-put-02, gft-out,
storekey/test-08 is used by okarrays-put-02, okarray-putbar-same-03, good-field-put, gft-out,

Used from specification fieldname

fieldname/inj is used by okbytearray-put-field-02, gft-out-01, gft-mode-01,

Used from specification typefuns

typefuns/le-noreftype is used by isarray-okarray,
typefuns/le-noreftype-01 is used by isarray-okarray,
typefuns/array is used by union-okarray, subset-okarray, subset-len, okarray-union-03, okarray-union, okarray-type-02, okarray-type-01, okarray-supertype, okarray-substore, okarray-subset, okarray-putbar-other, okarray-putba, okarray-put-samefield-01, okarray-put-other, okarray-put-okval-01, okarray-put-okval, okarray-put-badfield, okarray-put-08, okarray-put-07, okarray-primput, okarray-onlymod, okarray-okarray-01, okarray-okarray, okarray-new-01, okarray-new, okarray-length-01, okarray-len, okarray-del, okarray-copy, okarray-08, okarray-05, okarray-01, isarray-update, isarray-put-field, isarray-put-array-badindex, isarray-put, isarray-okval, isarray-okarray, isarray-notin-01, isarray-keyin, isarray-isarrayref, isarray-arrayreftype, isarray-abstract, is_array-primtype-01, is_array-norefval, is_array-noreftype, intval-01, getarray-subset-02, getarray-subset, copy-comp,
typefuns/bytearray is used by okbytearray-type, okbytearray-put-field, okbytearray-put-byteval-equiv, okbytearray-put-byteval, okbytearray-not, okbytearray-index-in, okbytearray, okbar-putbar, okbar-norefval, okbar-byteval, okarray-type-03, okarray-putbar-same-03, okarray-putbar-01, okarray-putar, okarray-put-06, okarray-put-02, okarray-getbar-len, okarray-copy-01, okarray-byte-01, okarray-byte, isarray-putbar, is_array-byte-noref, getbar-subset, byteval,
typefuns/elemtype-03 is used by is_array-okbytearray, is_array-okarray, is_array-bytearray-01, is_array-bytearray,
typefuns/elemtype-05 is used by is_array-notypeval, is_array-noreftype,
typefuns/elemtype-06 is used by is_array-abstract,
typefuns/elemtype-07 is used by is_array-primtype, is_array-okbytearray, is_array-okarray, is_array-hasnoclasstype-01, is_array-bytearray-01, is_array-bytearray,
typefuns/elemtype-base is used by is_array-typele, is_array-arraytype,
typefuns/elemtype-rec is used by is_array-nottypeex, is_array-norefval, is_array-noreftype, is_array-abstract,
typefuns/is_primtype-01 is used by is_array-primtype,
typefuns/is_primtype-02 is used by is_array-primtype,
typefuns/is_primtype-03 is used by is_array-primtype-01,
typefuns/isreftype is used by oktype-refval,
typefuns/isreftype-01 is used by oktype-refval,
typefuns/isreftype-02 is used by oktype-refval,
typefuns/isreftype-03 is used by oktype-refval,
typefuns/isreftype-04 is used by oktype-refval,
typefuns/isreftype-05 is used by oktype-refval, isarray-reftype,
typefuns/isreftype-06 is used by oktype-refval,
typefuns/isreftype-07 is used by oktype-refval,
typefuns/isreftype-08 is used by oktype-refval,
typefuns/isreftype-09 is used by oktype-refval,
typefuns/isreftype-10 is used by oktype-refval,
typefuns/isreftype-11 is used by oktype-refval,
typefuns/jtelemtype-class is used by is_array-typele, is_array-classtype,
typefuns/le-01 is used by okarray-08,
typefuns/le-02 is used by isarray-abstract,
typefuns/le-08 is used by okarray-08, intval-01,
typefuns/le-noreftype-01 is used by is_array-noreftype,
typefuns/prim-abstract is used by is_array-primtype,
typefuns/prim-void is used by is_array-primtype-01, is_array-primtype,
typefuns/ref is used by isarray-update, isarray-put-field, isarray-put-array-badindex, isarray-put, isarray-okval, isarray-okarray, isarray-notin-01, isarray-keyin, isarray-isarrayref, isarray-arrayreftype, is_array-primtype-01, is_array-norefval, getarray-subset-02, getarray-subset, exactarray-type-03, exactarray-type-02,
typefuns/subarray1 is used by union-okarray, subset-okarray, okarray-supertype, okarray-substore, okarray-subset, okarray-putba, okarray-put-samefield-01, okarray-put-okval-01, okarray-put-okval, okarray-put-badfield, okarray-put-07, okarray-onlymod, okarray-okarray-01, okarray-okarray, okarray-08, isarray-update, isarray-put-field, isarray-put-array-badindex, isarray-put, isarray-okarray,
typefuns/subarray2 is used by isarray-okreftype,
typefuns/subclass-01 is used by isarray-okreftype, is_array-typele,
typefuns/subtype-object is used by is_array-typele,
typefuns/transitivity is used by okarray-supertype, isarray-arrayreftype,
typefuns/typeex is used by is_array-hasnoclasstype-01, is_array-hasnoclasstype,
typefuns/typeex-array is used by is_array-primtype, is_array-okbytearray, is_array-okarray, is_array-nottypeex, is_array-norefval, is_array-noreftype, is_array-hasnoclasstype-01, is_array-bytearray-01, is_array-bytearray,
typefuns/typeex-prim-03 is used by is_array-okbytearray, is_array-okarray, is_array-bytearray-01, is_array-bytearray,
typefuns/typeex-prim-08 is used by is_array-notypeval,

Used from specification pair

pair/fieldinit/elim is used by vals-in, vals-at, validFields-fis, update-rec-01, update-put-notin, update-put, update-length, update-in-03, update-ex-nodups, okarray-update, nonnullrefs-in-key, nonnullrefs-in, nonnullrefs-dups-key, nonnullrefs-dups, keys-put-in, keys-at, instore-rec-03, instore-null, instore-afterputs, inst-in, getvals-rec-01, getkeys-one,
pair/fieldinit/inj is used by vals-in, vals-at, okarrays-all, keys-at,
pair/fieldinit/sel-01 is used by update-union-switch, update-putfis-sw, update-put-same, update-put-rew, update-keyin-01, update-keyin, update-at-notin, onlymod-is-update, instore-afterputs,
pair/fieldinit/sel-02 is used by validFields-rec, validFields-fis, update-union-switch, update-putfis-sw, update-put-same, update-put-rew, update-keyin-01, update-keyin, update-at-notin, onlymod-is-update, keys-put-notin, keys-put-in, keys-in, instore-afterputs, dups-fis-keys,

Used from specification nat-basic1

nat-basic1/f is used by vals-at, onlymod-is-update, keys-at, getbytearray-mkjavavalues, getarray-subset,
nat-basic1/z is used by getbytearray-mkjavavalues, getarray-subset,

Used from specification list-set

list-set/fieldinit-assoclista/subset is used by update-ex-nodups,
list-set/fieldinit-assoclista/sub-notin is used by update-ex-nodups,
list-set/fieldinit-assoclista/subset-empty-01 is used by update-ex-nodups,

Used from specification int-basic1

int-basic1/forward-pos is used by okbytearray, copy-comp,
int-basic1/ls-01 is used by okbytearray, okarray-primput, okarray-copy-01, okarray-byte-01, isarray-abstract, getarray-subset, copy-comp,
int-basic1/numlsf is used by short-length,

Used from specification set-basic

set-basic/references/eq-03 is used by update-refs,
set-basic/references/ne-01 is used by okarray-union-02, is_array-union-disjoint,

Used from specification refkey

refkey/inj is used by exactarray-out,
refkey/elim is used by update-at-01, okstore-out, okbar-put, okarrays-put-03, okarray-put-07, okarray-out, exactref-put-01, exactarray-put-07, exactarray-out,
refkey/inj is used by update-putfis-sw, update-put-rew, update-put-notin, update-put, update-keyin-01, update-keyin, onlymod-is-update, okstore-other, okstore-03, okstore-02, okstore-01, okclass-03, okbytearray-put-byteval-equiv, okarrays-put, okarray-put-okval-01, okarray-put-okval, okarray-put-06, okarray-primput, okarray-new, okarray-08, isarray-put-array-badindex, is_array-put-jvmref, infis-notin-01, good-field-put, gft-null, gengft, exactarray-new,
refkey/inj-01 is used by update-putfis-sw, update-put-rew, update-put-notin, update-put, update-atin, onlymod-is-update, okstore-other, okstore-03, okstore-02, okbytearray-put-byteval-equiv, okarrays-not, okarray-put-okval-01, okarray-put-okval, okarray-put-08, okarray-put-07, okarray-put-06, okarray-put-02, okarray-primput, okarray-08, isarray-put-field, isarray-put-array-badindex, isarray-put, is_array-put-jvmref, instore-afterputs, infis-notin-01, good-field-put, gft-null, gft-not-01, gengft, exactarray-put-02, exactarray-put-01, exactarray-put, exactarray-08, copy-same-01-01, copy-same-01,
refkey/sel-01 is used by update-refs, okbytearray-put-byteval-01, okbytearray-put-byteval, okbar-put-byte-01, okarray-update, okarray-putbar-same-03, okarray-put-02, okarray-02,
refkey/sel-02 is used by okarray-putbar-same-03,

Used from specification oelem

oelem/intlista/irreflexivity is used by okbytearray, okarray-copy-01, isarray-keyin, exactarray-length-02, copy-comp, byteval-01,
oelem/intlista/lel is used by okbytearray-put-byteval-equiv, okbytearray-length-zero, okarray-put-06, okarray-08, isarray-put-array-badindex, copy-comp,
oelem/intlista/transitivity is used by okbytearray, copy-comp,

Used from specification javatype

javatype/diff is used by is_array-classtype,
javatype/diff-01 is used by isarray-okreftype,
javatype/disj-02 is used by oktype-refval, oktype-03, is_array-noreftype, is_array-abstract,
javatype/disj-03 is used by oktype-03,
javatype/disj-06 is used by oktype-refval, is_array-okbytearray, is_array-okarray, is_array-bytearray-01, is_array-bytearray,
javatype/disj-07 is used by oktype-03,
javatype/disj-08 is used by oktype-03, is_array-okbytearray, is_array-okarray, is_array-bytearray-01, is_array-bytearray,
javatype/disj-12 is used by oktype-03,
javatype/disj-14 is used by oktype-03,
javatype/disj-17 is used by oktype-03,
javatype/disj-18 is used by oktype-03,
javatype/disj-19 is used by oktype-refval,
javatype/disj-21 is used by oktype-refval,
javatype/disj-24 is used by oktype-03,
javatype/disj-25 is used by oktype-refval,
javatype/disj-26 is used by oktype-refval,
javatype/disj-27 is used by oktype-refval,
javatype/disj-38 is used by oktype-03,
javatype/disj-39 is used by oktype-refval,
javatype/disj-44 is used by oktype-03,
javatype/disj-45 is used by oktype-refval,
javatype/elim-01 is used by union-okarray, subset-okarray, okarrays-put, okarrays-not, okarray-union-03, okarray-union, okarray-supertype, okarray-substore, okarray-subset, okarray-putbar-other, okarray-putba, okarray-put-samefield-01, okarray-put-other, okarray-put-okval-01, okarray-put-okval, okarray-put-badfield, okarray-put-08, okarray-put-07, okarray-primput, okarray-onlymod, okarray-okarray-01, okarray-okarray, okarray-length-01, okarray-del, okarray-copy, okarray-08, isarray-update, isarray-union, isarray-subset, isarray-reftype, isarray-put-samefield-01, isarray-put-samefield, isarray-put-okval, isarray-put-jvmref, isarray-put-field, isarray-put-array-badindex, isarray-put, isarray-okval, isarray-okreftype, isarray-okarray, isarray-notin-01, isarray-length-07, isarray-lenfield, isarray-keyin, isarray-isarrayref, isarray-abstract, is_array-nottypeex, is_array-norefval, is_array-noreftype, getintarray-subset, getarray-subset-02, getarray-subset, copy-comp,
javatype/elim-02 is used by is_array-typele,
javatype/inj-01 is used by subset-exactarray, okbytearray-put-field, okbytearray-put-byteval-equiv, okbytearray-bad-type, okbar-putbar, okarray-putbar-same-03, okarray-putbar-01, isarray-putbar, isarray-bytearray, is_array-byte-noref, exactarray-putin, exactarray-put-06, exactarray-put-05, exactarray-put-03, exactarray-put-02, exactarray-put, exactarray-primput, exactarray-copy, exactarray-08, exactarray-06, exactarray-02-01,
javatype/sel-01 is used by okbytearray-isarray, isarray-update, isarray-union, isarray-subset, isarray-putbar, isarray-put-samefield-01, isarray-put-samefield, isarray-put-okval, isarray-put-jvmref, isarray-put-field, isarray-put-byte, isarray-put-array-badindex, isarray-put, isarray-okval, isarray-okarray-01, isarray-notin-01, isarray-keyin, isarray-isarrayref, isarray-bytearray, isarray-arrayreftype, isarray-abstract, is_array-primtype-01, is_array-norefval, is_array-noreftype, is_array-byte-noref, getarray-subset-02, getarray-subset, exactarray-type-03, exactarray-type-02,
javatype/test-02 is used by okarray-put-03,
javatype/test-04 is used by okarray-put-03,
javatype/test-09 is used by union-okarray, subset-okarray, okbytearray-isarray, okarrays-put, okarrays-not, okarray-union-03, okarray-union, okarray-supertype, okarray-substore, okarray-subset, okarray-putbar-other, okarray-putba, okarray-put-samefield-01, okarray-put-other, okarray-put-okval-01, okarray-put-okval, okarray-put-badfield, okarray-put-08, okarray-put-07, okarray-primput, okarray-onlymod, okarray-okarray-01, okarray-okarray, okarray-length-01, okarray-del, okarray-copy, okarray-08, isarray-update, isarray-union, isarray-subset, isarray-reftype, isarray-putbar, isarray-put-samefield-01, isarray-put-samefield, isarray-put-okval, isarray-put-jvmref, isarray-put-field, isarray-put-array-badindex, isarray-put, isarray-okval, isarray-okreftype, isarray-okarray-01, isarray-okarray, isarray-notin-01, isarray-length-07, isarray-lenfield, isarray-keyin, isarray-isarrayref, isarray-bytearray, isarray-arrayreftype, isarray-abstract, is_array-primtype-01, is_array-nottypeex, is_array-norefval, is_array-noreftype, is_array-byte-noref, getintarray-subset, getarray-subset-02, getarray-subset, copy-comp,
javatype/test-23 is used by isarray-put-okval,
javatype/test-28 is used by isarray-type-02, isarray-type-01,

Used from specification javavalue

Used from specification storearrays

storearrays/arrayCopy-rec is used by okarray-copy-01,
storearrays/comp-same is used by copy-comp,
storearrays/copy-at is used by copy-same-01-01, copy-same-01, copy-comp,
storearrays/copy-bet-bet is used by copy-comp,
storearrays/copy-bet-low is used by copy-comp,
storearrays/copy-between is used by copy-same-01-01, copy-comp,
storearrays/copy-in-between is used by exactarray-copy-01,
storearrays/copy-lower is used by copy-same-01-01, copy-same-01, copy-comp,
storearrays/copy-upper is used by copy-same-01, copy-comp,
storearrays/extension-01 is used by getbar-subset,
storearrays/get-alleq is used by copy-comp, comp-same,
storearrays/get-get is used by getbytearray-mkjavavalues,
storearrays/get-length-01 is used by getbytearray-mkjavavalues,
storearrays/getArray-all is used by getbytearray-mkjavavalues, getarray-bytes,
storearrays/getArray-one is used by okbytearray,
storearrays/getArray-rec is used by okbytearray,
storearrays/getArray-zero is used by okbytearray,
storearrays/getByteArray is used by getbytearray-mkjavavalues, getarray-bytes,
storearrays/getByteArray-all is used by getbytearray-mkjavavalues, getarray-bytes,
storearrays/getarray-get is used by getarray-subset,
storearrays/getarray-length is used by getarray-subset,
storearrays/getarray-subset is used by getarray-subset-02,
storearrays/getbar-len-03 is used by okbytearray-getarray-length, okbar-bytes2int-same,
storearrays/getintarray-subset is used by getintarray-subset,
storearrays/is_arrayref is used by union-okarray, subset-okarray, subset-exactarray, okbytearray-put-byteval-equiv, okbar-putbar, okbar-norefval, okarray-union-03, okarray-union, okarray-substore, okarray-subset, okarray-putbar-same-03, okarray-putbar-01, okarray-putba, okarray-putar, isarray-update, isarray-put-array-badindex, isarray-notin-01, isarray-keyin, isarray-isarrayref, getarray-subset-02, getarray-subset, exactarray-putbar, exactarray-putar, exactarray-put-02, exactarray-put, exactarray-lenin, exactarray-in, exactarray-copy-01, exactarray-08, copy-comp,
storearrays/putBar-rec is used by okbar-putbar-same, okarray-putbar-same-02, okarray-putbar-same-01, okarray-putbar-same, isarray-putbar,
storearrays/putByteArray is used by okarray-putbar,
storearrays/putByteArray-all is used by okbar-putbar-04, okarray-putbar-05, okarray-putbar-02, okarray-putbar-01,
storearrays/putar-in is used by exactarray-putar,
storearrays/putbar-atother-01 is used by okarray-putbar-same-03,
storearrays/putbar-in is used by exactarray-putbar,
storearrays/Comp-get-02 is used by copy-comp, comp-same,
storearrays/arrayref is used by okbytearray-put-field, okarray-put-samefield-01, okarray-put-badfield, okarray-put-08, isarray-put-field, isarray-put, exactarray-put-01,
storearrays/arrayref-01 is used by okarray-new, exactarray-new,
storearrays/copy-arref is used by okarray-copy, exactarray-copy,
storearrays/copy-at is used by okarray-copy, copy-same-01-01, copy-same-01,
storearrays/copy-atfield is used by copy-same-01-01, copy-same-01, copy-comp,
storearrays/copy-bet-up is used by copy-comp,
storearrays/copy-between is used by copy-same-01-01, copy-same-01,
storearrays/copy-in is used by copy-same-01-01, copy-same-01, copy-comp,
storearrays/copy-in-01 is used by exactarray-copy,
storearrays/copy-in-02 is used by okclass-copy, exactarray-copy-01,
storearrays/copy-in-between is used by copy-same-01-01, copy-same-01, copy-comp,
storearrays/copy-in-lower is used by exactarray-copy-01, copy-same-01-01, copy-same-01, copy-comp,
storearrays/copy-in-upper is used by exactarray-copy-01, copy-same-01-01, copy-same-01, copy-comp,
storearrays/copy-infs is used by copy-same-01-01, copy-same-01, copy-comp,
storearrays/copy-length is used by okarray-copy, exactarray-copy-01, exactarray-copy,
storearrays/copy-length-02 is used by okarray-copy, exactarray-copy-01, exactarray-copy,
storearrays/copy-lower is used by copy-same-01-01, copy-same-01,
storearrays/copy-type is used by okclass-copy, okarray-copy, exactarray-copy-01, exactarray-copy,
storearrays/copy-type-01 is used by okclass-copy, okarray-copy, exactarray-copy-01, exactarray-copy,
storearrays/copy-upper is used by copy-same-01-01, copy-same-01,
storearrays/copy-zero is used by okarray-copy-01,
storearrays/get-empty is used by getbytearray-mkjavavalues,
storearrays/get-length-04 is used by getbytearray-mkjavavalues,
storearrays/getByteArray-put is used by getbar-update,
storearrays/getbar-len-03 is used by okarray-getbar-len,
storearrays/getbar-ref is used by getbar-update-01,
storearrays/is_arrayref-02 is used by mode-02-01,
storearrays/is_arrayref-03 is used by okarray-put-okval-01, okarray-put-okval, okarray-put-06, okarray-put-02, okarray-primput, okarray-08, exactarray-putin, exactarray-put-06, exactarray-primput,
storearrays/isarray is used by okarray-put-other, okarray-put-okval-01, okarray-put-07, exactarray-put-07, exactarray-put-05, exactarray-put-03, exactarray-06, exactarray-02-01,
storearrays/isarray-02 is used by okbytearray-put-byteval-equiv, okarray-primput, exactarray-primput,
storearrays/isarrayref-del is used by okarray-del,
storearrays/isarrayref-mod is used by okarray-onlymod,
storearrays/isarrayref-putbar-other is used by okarray-putbar-other,
storearrays/putBar-at-fskey is used by goodfields-putba,
storearrays/putBar-at-len is used by okbar-putbar, okarray-putbar-same-03, okarray-putbar-same-02, okarray-putbar-same-01, okarray-putbar-other, okarray-putbar-01, okarray-putba, exactarray-putbar,
storearrays/putBar-at-type is used by okbar-putbar, okarray-putbar-same-03, okarray-putbar-other, okarray-putbar-01, okarray-putba, is_array-putbar-01, is_array-putbar, exactarray-putbar,
storearrays/putBar-empty is used by okbar-putbar-same, okarray-putbar-same-02, okarray-putbar-same-01, okarray-putbar-same, isarray-putbar,
storearrays/putBar-in is used by okarray-putbar-same-03,
storearrays/putar-atref is used by okarray-putar,
storearrays/putar-inref is used by okarray-putar, exactarray-putar,
storearrays/putarray-length is used by okarray-putar, exactarray-putar,
storearrays/putarray-type is used by okarray-putar, exactarray-putar,
storearrays/putbar-atref-01 is used by okbar-putbar, okarray-putbar-other, okarray-putbar-01, okarray-putba,
storearrays/putbar-byte is used by okarray-putbar-same-03,
storearrays/putbar-inref is used by okbar-putbar, okarray-putbar-other, okarray-putbar-01, okarray-putba, goodfields-putba, exactarray-putbar,

Used from specification list-dup

list-dup/storekeys/app-05 is used by dups-fis-keys,
list-dup/storekeys/dups-cons is used by nonnullrefs-in-key, nonnullrefs-dups-key,
list-dup/references/dups-cons is used by nonnullrefs-dups,
list-dup/storekeys/e-01 is used by update-ex-nodups,
list-dup/references/e-01 is used by nonnullrefs-dups-key,
list-dup/storekeys/f is used by dups-fis-keys,
list-dup/references/rec is used by nonnullrefs-dups-key,

Used from specification list-data

list-data/fieldinit-assoclista/elim-list-c is used by update-rec-02,
list-data/javavalues/l is used by getbytearray-mkjavavalues, getarray-subset,
list-data/fieldinit-assoclista/l is used by vals-at, keys-at,
list-data/bytelist/length-neq is used by okbar-bytes2int-same,
list-data/javavalues/size-01 is used by vals-length,
list-data/fieldinit-assoclista/size-01 is used by vals-length, keys-length,
list-data/storekeys/size-01 is used by keys-length,

Used from specification list-del

list-del/javavalues/extension is used by getarray-subset,
list-del/javavalues/get-rec is used by vals-at,
list-del/storekeys/get-rec is used by keys-at,
list-del/javavalues/in-get is used by getbytearray-mkjavavalues,
list-del/fieldinit-assoclista/get-succ is used by vals-at, keys-at,
list-del/javavalues/get-zero-01 is used by vals-at,
list-del/fieldinit-assoclista/get-zero-01 is used by vals-at, keys-at,
list-del/storekeys/get-zero-01 is used by keys-at,

Used from specification specialkeys

specialkeys/mode is used by gft-mode-01,
specialkeys/mode-01 is used by mode-03,
specialkeys/out is used by gft-out-01, exactarray-out,
specialkeys/diff is used by okstore-out, okstore-mode,
specialkeys/len is used by okbytearray-put-byteval-equiv, okarrays-put, okarray-put-okval-01, okarray-put-okval, okarray-put-06, okarray-put-02, okarray-primput, okarray-new, okarray-08, isarray-put-array-badindex, exactarray-putin, exactarray-put-06, exactarray-put-02, exactarray-put-01, exactarray-put, exactarray-primput, exactarray-08,
specialkeys/length-02 is used by okbytearray-put-field-02, okbytearray-put-field-01,
specialkeys/length-04 is used by okarray-putbar-same-03,
specialkeys/mode-01 is used by mode-03, gft-mode-01,
specialkeys/mode-02 is used by okstore-jvmref,
specialkeys/mode-06 is used by update-mode, okstore-03,
specialkeys/mode-ref is used by mode-02,
specialkeys/out-01 is used by gft-out-01, exactarray-out,
specialkeys/out-02 is used by okstore-out, okstore-03, okarray-out, gft-out,
specialkeys/out-03 is used by okstore-jvmref,
specialkeys/type-03 is used by okarrays-put, okarray-put-02, okarray-primput, gengft, exactarray-put-01,
specialkeys/type-04 is used by okarray-new, exactarray-new,
specialkeys/type-05 is used by okbytearray-put-field-02, okbytearray-put-field-01, gft-out-01, gft-mode-01,
specialkeys/type-neq is used by isarray-put,

Used from specification storefunsx

storefunsx/classOf is used by okclass-02,
storefunsx/instore-inrefs is used by is_array-union-disjoint,
storefunsx/onlyModified is used by onlymod-is-update, okarray-onlymod,
storefunsx/onlymod-other is used by okarray-onlymod,
storefunsx/refs-def is used by okarray-union-02,
storefunsx/refs-notin is used by is_array-union-disjoint,
storefunsx/reftypep is used by okclass-copy, okclass-03,
storefunsx/union-at-left is used by is_array-union-disjoint,
storefunsx/union-at-right-01 is used by union-okarray, okarray-union-03, is_array-union,
storefunsx/union-rec is used by update-union-switch,
storefunsx/classof-02 is used by okclass-02,
storefunsx/classof-06 is used by okclass-02,
storefunsx/instore-inrefs-01 is used by update-refs,
storefunsx/instore-inrefs-02 is used by okarray-union-01,
storefunsx/lookup-xtra is used by union-okarray, subset-okarray, onlymod-is-update, okstore-03, okbytearray-put-byteval-equiv, okbytearray-put-byteval, okbytearray-index-in, okarray-union-03, okarray-substore, okarray-putbar-same-03, okarray-putbar-01, okarray-put-08, isarray-put-field, isarray-put-array-badindex, is_array-union, is_array-type-02, is_array-subset, good-field-put, getbar-subset, getarray-subset, exactarray-put-01, comp-same,
storefunsx/onlymod-del is used by onlymod-is-update,
storefunsx/onlymod-in is used by onlymod-is-update,
storefunsx/onlymod-put is used by onlymod-is-update,
storefunsx/onlymod-same is used by onlymod-is-update,
storefunsx/refs-empty-01 is used by okarray-union-02, is_array-union-disjoint,
storefunsx/refs-put is used by update-refs,
storefunsx/reftype-02 is used by okclass-int, okclass-copy, okclass-02, mode,
storefunsx/reftype-int-02 is used by okclass-int,
storefunsx/reftype-jvmref is used by okclass-copy, okclass-01,
storefunsx/reftype-mode is used by mode,
storefunsx/reftype-out is used by okclass-out,
storefunsx/union-at-left is used by union-okarray, okarray-union-03,
storefunsx/union-at-right-01 is used by union-okarray, isarray-union, is_array-union-disjoint,
storefunsx/union-at-right-03 is used by okarray-union, gft-union,
storefunsx/union-in is used by union-okarray, okarray-union-03, isarray-union,
storefunsx/union-in-02 is used by okarray-union, gft-union,
storefunsx/union-subset is used by okreftype-union, okarray-union-04, okarray-union-03,
storefunsx/union-subset-left is used by isarray-union-disjoint,

Used from specification javastore

javastore/at-other-01 is used by okbytearray-put-field, okarray-put-samefield-01, okarray-put-badfield, okarray-put-08, isarray-put-field, isarray-put,
javastore/at-other-16 is used by update-length, update-at-notin, okstore-01, okclass-03, okbytearray-put-field, okarrays-put-02, okarray-put-samefield-01, okarray-put-badfield, okarray-put-08, isarray-put-samefield-01, isarray-put-samefield, isarray-put-field, isarray-put, is_array-put-field, instore-afterputs, good-field-put, gft-null, exactarray-put-01,
javastore/at-other-20 is used by isarray-put, is_array-put,
javastore/at-other-21 is used by okarrays-mode, mode-02-01, mode-01,
javastore/at-other-32 is used by okarray-out,
javastore/at-other-41 is used by okstore-mode, mode-02-01, mode,
javastore/in-01 is used by okstore-jvmref, okreftype-put, okarray-put-other, okarray-put-07, isarray-put-01, infis-jvmref, hasKeys-put, good-field-put, gft-put, gengft, exactref-put-01, exactarray-put-07, exactarray-put-05, exactarray-put-03, exactarray-06, exactarray-02-01, copy-same-01-01, copy-same-01,
javastore/instore-02 is used by okstore-03, okstore-02, okbytearray-put-field, okbytearray-put-byteval-equiv, okarray-put-samefield-01, okarray-put-okval, okarray-put-badfield, okarray-put-06, okarray-put-02, okarray-primput, okarray-new, okarray-08, isarray-put-samefield-01, isarray-put-samefield, isarray-put, instore-afterputs, hasKeys-put-02, gengft, exactarray-putin, exactarray-put-06, exactarray-primput, exactarray-new, copy-same-01-01, copy-same-01,
javastore/length-at is used by okbytearray-put-byteval-equiv, okarray-putbar-same-02, okarray-putbar-same-01, okarray-put-okval-01, okarray-put-okval, okarray-put-06, okarray-copy-01, okarray-08, isarray-put-array-badindex, exactarray-putin, exactarray-put-06, exactarray-put-02, exactarray-put, exactarray-primput, exactarray-08,
javastore/look-del-01 is used by onlymod-is-update,
javastore/look-ins is used by update-at, okstore-jvmref, okreftype-put, okarray-put-other, okarray-put-07, isarray-put-01, is_array-put-jvmref, is_array-put-01, infis-jvmref, good-field-put, gft-put, gengft, exactref-put-01, exactarray-put-07, exactarray-put-05, exactarray-put-03, exactarray-06, exactarray-02-01, copy-same-01-01, copy-same-01,
javastore/look-type is used by okstore-out, okclass-out,
javastore/lookup-if is used by update-mode, update-atin, onlymod-is-update, okstore-other, okstore-03, okstore-02, okarrays-put, okarrays-not, okarray-put-02, okarray-primput, okarray-new, infis-notin-01, gft-not-01, exactarray-new, copy-same-01-01, copy-same-01,
javastore/mode is used by mode-02-01, mode-01,
javastore/sk is used by copy-same-01-01, copy-same-01,
javastore/type is used by okclass-int, okbytearray-put-byteval-equiv, okarray-put-okval-01, okarray-put-okval, okarray-put-06, okarray-put-02, okarray-primput, okarray-08, isarray-put-okval, isarray-put-array-badindex, exactarray-putin, exactarray-put-06, exactarray-put-02, exactarray-put, exactarray-primput, exactarray-08,
javastore/type-01 is used by okstore-mode, mode-02-01, mode,
javastore/type-at is used by okclass-int, okbytearray-put-byteval-equiv, okarray-put-okval-01, okarray-put-okval, okarray-put-06, okarray-08, isarray-put-okval, isarray-put-array-badindex, is_array-put-okval, is_array-put-byte, exactarray-putin, exactarray-put-06, exactarray-put-02, exactarray-put, exactarray-primput, exactarray-08,
javastore/typeout is used by okstore-out, okclass-out,

Used from specification assoclist

assoclist/fieldinit/assoc-no is used by nonnullrefs-in-key, nonnullrefs-in, nonnullrefs-dups-key, nonnullrefs-dups,
assoclist/fieldinit/in-put is used by validFields-putfis,
assoclist/fieldinit/put-no is used by update-putfis-sw, keys-put-in,
assoclist/fieldinit/assoc-no is used by update-atin, nonnullrefs-dups-key, nonnullrefs-dups,
assoclist/fieldinit/assoc-yes is used by update-atin, nonnullrefs-in-key, nonnullrefs-in, nonnullrefs-dups-key, nonnullrefs-dups,
assoclist/fieldinit/cons is used by validFields-rec, instore-afterputs,
assoclist/fieldinit/empty is used by validFields-empty, update-put-same, update-keyin-01, update-atin, nonnullrefs-in, nonnullrefs-dups, keys-put-in, keys-in, instore-afterputs,
assoclist/fieldinit/in-append is used by validFields-rec, validFields-fis, update-put-same, update-put-rew, update-put-notin, update-keyin-01, update-keyin, update-at-notin, okarrays-put-02, okarrays-put, okarrays-not, nonnullrefs-in-key, nonnullrefs-dups-key, keys-in, instore-afterputs,
assoclist/fieldinit/in-assoclist-01 is used by vals-at-in,
assoclist/fieldinit/in-put is used by validFields-putfis, keys-put,
assoclist/fieldinit/incons is used by update-put-same,
assoclist/fieldinit/infirst is used by nonnullrefs-in, nonnullrefs-dups,
assoclist/fieldinit/inkeys-n is used by nonnullrefs-in, nonnullrefs-dups,
assoclist/fieldinit/inkeys-nc is used by update-atin, keys-put-in,
assoclist/fieldinit/inone is used by validFields-rec, validFields-fis, update-put-same, update-put-rew, update-put-notin, update-keyin-01, update-keyin, update-at-notin, okarrays-put-02, okarrays-put, okarrays-not, nonnullrefs-in-key, nonnullrefs-dups-key, keys-in, instore-afterputs,
assoclist/fieldinit/inrec is used by infis-notin-01,
assoclist/fieldinit/insnotin is used by keys-put-notin, dups-fis-keys,
assoclist/fieldinit/put-empty is used by update-putfis-sw, keys-put-in,
assoclist/fieldinit/put-in is used by update-ex-nodups,
assoclist/fieldinit/put-yes is used by update-putfis-sw, keys-put-in,
assoclist/fieldinit/unique-add is used by validFields-fis,
assoclist/fieldinit/unique-e is used by validFields-empty, instore-afterputs,
assoclist/fieldinit/unique-put is used by validFields-putfis,

Used from specification classname

classname/inj is used by okbytearray-put-field-01,

Used from specification int-mult

int-mult/dist-lsplit is used by copy-comp,
int-mult/dist-sub-split is used by copy-comp,
int-mult/numls-02 is used by copy-comp,
int-mult/zero-ge-add is used by copy-comp,
int-mult/zero-ls-02 is used by copy-comp,
int-mult/Mult-zero is used by copy-comp,
int-mult/add-mult-two is used by copy-comp,
int-mult/associativity is used by exactarray-lenin, copy-comp,
int-mult/commutativity is used by exactarray-lenin, copy-comp,
int-mult/dist-rmerge is used by copy-comp,
int-mult/le-pos is used by exactarray-lenin,
int-mult/ls-sub is used by copy-comp,
int-mult/minus-left is used by copy-comp,
int-mult/minus-one-01 is used by copy-comp,
int-mult/numle-04 is used by copy-comp,
int-mult/one is used by copy-comp,
int-mult/succ-rmerge is used by copy-comp,
int-mult/zero-ge is used by exactarray-lenin,
int-mult/zero-gr-02 is used by copy-comp,
int-mult/zero-ls is used by exactarray-lenin,

Used from specification nat

nat/elim-pred-c is used by vals-at, onlymod-is-update, keys-at,
nat/eq is used by onlymod-is-update,
nat/fle-01 is used by getarray-subset,
nat/le-ls-simp is used by getarray-subset,
nat/lels is used by vals-at, onlymod-is-update, keys-at, getarray-subset,
nat/lels-01 is used by onlymod-is-update,
nat/leprf is used by onlymod-is-update,
nat/ls-le-simp is used by vals-at, keys-at, getbytearray-mkjavavalues,
nat/pred-03 is used by onlymod-is-update,
nat/succ-01 is used by vals-at, keys-at,

Used from specification nat-basic2

nat-basic2/a is used by vals-length, vals-at, onlymod-is-update, okbytearray, okarray-copy-01, keys-length, keys-at,
nat-basic2/c is used by vals-length, vals-at, onlymod-is-update, okbytearray, okarray-copy-01, keys-length, keys-at,
nat-basic2/eq-01 is used by vals-length, keys-length,
nat-basic2/oz is used by vals-at, keys-at,
nat-basic2/s is used by vals-at, okbytearray, okarray-copy-01, keys-at,

Used from specification set-union

set-union/references/int-a is used by okarray-union-02, isarray-union-disjoint, is_array-union-disjoint,
set-union/references/int-c is used by okarray-union-02, isarray-union-disjoint, is_array-union-disjoint,
set-union/references/int-empty-02 is used by okarray-union-02, is_array-union-disjoint,

Used from specification byte

byte/inshort is used by short-length,
byte/short-in is used by short-length-01,
byte/sis-in is used by short-length,

Used from specification bytes

bytes/bytes2int-diff is used by okbar-bytes2int-same,