[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 validstatfield-throw-predef, validstatfield-put-norefval, validrefkeynotnull-put-shortval, validrefkeynotnull-put-byteval, validref-put-refval, validref-put-null, validref-put-badfield, validmode-put-statfield, validfield-put-statfield, junkrefs-put-null-01, junkrefs-put-null, junkrefs-put-norefval-equiv, junkrefs-put-badfield, junkref-put-null, junkref-put-badfield,
store/javastore/Subset is used by junkrefs-subset, junkref-subset,
store/javastore/subset-elem-eq is used by validref-subset-01,
store/javastore/subset-elem-eq-01 is used by validrefnotnull-array-len-subset,
store/javastore/superset-elem-eq is used by validrefkeynotnull-subset, validref-subset, validmode-superset, validfield-superset, junkrefs-subset,
store/javastore/At-other is used by validval-put-any, validrefkeynotnull-put-statfield, validmode-noval-put, junkrefs-put-refval-02, junkrefs-put-refval-01, junkrefs-put-refval, junkrefs-put-null-02, junkrefs-put-null-01, junkrefs-put-null, junkrefs-put-norefval-01, junkrefs-put-badfield, junkrefs-put-badclassfield, junkrefs-put-badarrayindex, junkrefs-put-badarrayfield, junkrefs-put-array-norefval,
store/javastore/At-same is used by validval-put-any, validstatfield-putrkvs, validstatfield-put-statfield-int, validstatfield-put-norefval, validrefkeynotnull-put-shortval, validrefkeynotnull-put-byteval, validref-put-badfield, validmode-throw-predef, junkrefs-put-refval-02, junkrefs-put-refval-01, junkrefs-put-refval, junkrefs-put-null-02, junkrefs-put-null-01, junkrefs-put-null, junkrefs-put-norefval-equiv, junkrefs-put-norefval-01, junkrefs-put-badfield, junkrefs-put-badclassfield, junkrefs-put-badarrayfield, junkrefs-put-array-norefval, junkref-put-refval-statfield, junkref-put-null, junkref-put-field, junkref-put-badfield, initsubset-put-statfield-int,
store/javastore/In-insert is used by validstatfield-put-statfield-int, validstatfield-put-norefval, validrefkeynotnull-put-statfield, validrefkeynotnull-put-shortval, validrefkeynotnull-put-byteval, validmode-throw-predef, validmode-put-statfield, validmode-noval-put, initsubset-put-statfield-int,
store/javastore/In-store is used by validrefnotnull-union-at-right, validref-not-tdnameex, junkrefs-union, junkref-field-reftype, junkref-class-02, junkref-class-01,
store/javastore/notmemlookup is used by validrefnotnull-union-at-right, validrefnotnull-array-len-subset, validrefkeynotnull-union, validrefkeynotnull-subset, validref-union, validref-subset, validmode-put-nonnull, validfieldinits-def-01, junkrefs-union, junkrefs-subset, junkref-subset,
store/javastore/sub-ref is used by validstatfield-addobj, junkref-addarray-02,
store/javastore/superset-elem-in-01 is used by validrefkeynotnull-subset, validmode-superset, validfield-superset,

Used from specification addarray

addarray/add-at-01 is used by validrefkeynotnull-addarray, validref-addarray, junkrefs-addarray, junkref-addarray-newref-put, junkref-addarray-newref,
addarray/add-at-02 is used by validref-addarray-other-01,
addarray/addarray-at-newref is used by junkref-addarray-04,
addarray/addarray-getintarray-other is used by validref-addarray-get,
addarray/addarray-getintarray-other-01 is used by validref-addarray-get-01,
addarray/is_array-addarray-any is used by junkref-addarray-04,
addarray/is_array-addarray-prim is used by junkrefs-addarray-noreftype,
addarray/isarray-init-01 is used by junkref-addarray-01,
addarray/isarray-init-02 is used by junkref-addarray-01,
addarray/add-at-ok is used by junkrefs-addarray-noreftype, junkrefs-addarray, junkref-addarray-04, junkref-addarray-01,
addarray/add-in is used by junkrefs-addarray-newref-put, junkref-addarray-01,
addarray/addarray-mode is used by validmode-addarray,
addarray/at-1dim is used by junkref-addarray-03,
addarray/in-init-09 is used by validrefkeynotnull-addarray,
addarray/is_array-addarray is used by validref-addarray-same, junkref-addarray-03,
addarray/is_array-other-addarray is used by junkrefs-addarray,
addarray/is_obj-addarray is used by junkrefs-addarray,
addarray/is_obj-addarray-01 is used by validref-addarray-same,
addarray/length-1dim is used by junkref-addarray-03,
addarray/length-1init-01 is used by junkrefs-addarray-noreftype, junkrefs-addarray, junkref-addarray-04, junkref-addarray-01,
addarray/length-init is used by junkref-addarray-01,
addarray/lookup-1init is used by junkrefs-addarray,
addarray/mode-1init-01 is used by validmode-addarray,
addarray/okarray-04 is used by junkrefs-addarray-newref-put,
addarray/okreftype-init-02 is used by junkref-addarray-01,
addarray/stsubset-03 is used by junkref-addarray-02,
addarray/type-1dim is used by validref-addarray-same,
addarray/type-1init is used by junkrefs-addarray-noreftype, junkrefs-addarray-newref-put, junkrefs-addarray, junkref-addarray-noreftype, junkref-addarray-newref-put, junkref-addarray-newref, junkref-addarray-04, junkref-addarray-01,

Used from specification list

list/bytelist/elim-first is used by junkref-putbar,
list/references/Last is used by junkref-class-01, junkref-class,
list/storekeys/Nil is used by nojunkref-typeex-01,
list/references/Nil is used by junkrefs-put-notin-butlast, junkrefs-null-01, junkrefs-notin,
list/storekeys/Two is used by validrefnotnull-union-at-right, validref-class,
list/references/Two is used by junkref-isarray-typeex,
list/fieldinit-assoclista/a is used by validfieldinits-validreflist, validfieldinits-rec, validfieldinits-def-01, initsubset-initerror-02,
list/refkeyvalues-assoclista/a is used by validvals-append-01, validvals-append, validstatfield-putrkvs, validref-putrkvs,
list/storekeys/a is used by validstatfields-rec, validstatfields-put-statfield-05, validstatfields-put-statfield-04, validstatfields-put-statfield-01, validstatfields-levelsubset, validstatfields-initundone, validfieldlist-rec, validfieldlist-put-statfield, nojunkref-typeex-02, nojunkref-typeex-01,
list/references/a is used by validref-primarray, validref-not-junkrefs, validfieldinits-validreflist, junkrefs-union-disjoint, junkrefs-union, junkrefs-supertype, junkrefs-subtype, junkrefs-subset, junkrefs-subclass, junkrefs-sametype-01, junkrefs-runtimetype, junkrefs-put-statfield, junkrefs-put-refval-statfield, junkrefs-put-refval-02, junkrefs-put-refval-01, junkrefs-put-refval, junkrefs-put-null-02, junkrefs-put-null-01, junkrefs-put-null, junkrefs-put-notin-butlast, junkrefs-put-notin, junkrefs-put-norefval-equiv, junkrefs-put-norefval-01, junkrefs-put-badfield, junkrefs-put-badclassfield, junkrefs-put-badarrayindex, junkrefs-put-badarrayfield, junkrefs-put-array-norefval, junkrefs-primarray, junkrefs-one, junkrefs-null-03, junkrefs-null-01, junkrefs-notin-01, junkrefs-notin, junkrefs-newref-03, junkrefs-levelsubset, junkrefs-junkref, junkrefs-inttype, junkrefs-delete-02, junkrefs-delete, junkrefs-append, junkrefs-addobj, junkrefs-addarray-noreftype, junkrefs-addarray, junkref-union-disjoint, junkref-subset, junkref-put-statfield, junkref-put-refval-statfield, junkref-put-refval-01, junkref-put-refval, junkref-put-null, junkref-put-norefval-equiv, junkref-put-norefval-01, junkref-put-norefval, junkref-put-field, junkref-put-badfield, junkref-put-badclassfield, junkref-put-badarrayindex, junkref-put-badarrayfield, junkref-put-ba, junkref-put-array-norefval, junkref-primarray-lvl, junkref-primarray-level-01, junkref-null, junkref-levelsubset, junkref-isarray-typeex, junkref-class-01, junkref-class, junkref-array, junkref-addobj-01, junkref-addobj, junkref-addarray-noreftype, junkref-addarray-newref-put, junkref-addarray-newref, junkref-addarray-01,
list/bytelist/a is used by validrefnotnull-putbar, validref-putbar, junkref-putbar-01, junkref-putbar,
list/javavalues/a is used by validreflist-rec, validfieldinits-validreflist, junkreflist-rec,
list/storekeys/app is used by nojunkref-typeex-01,
list/references/app is used by junkrefs-union-disjoint, junkrefs-supertype, junkrefs-one,
list/references/app-02-ant is used by validref-not-junkrefs, junkrefs-union-disjoint, junkrefs-supertype, junkrefs-subtype, junkrefs-put-statfield, junkrefs-put-refval-statfield, junkrefs-put-refval-02, junkrefs-put-refval-01, junkrefs-put-refval, junkrefs-put-null-02, junkrefs-put-null-01, junkrefs-put-null, junkrefs-put-notin-butlast, junkrefs-put-norefval-01, junkrefs-put-badfield, junkrefs-put-badclassfield, junkrefs-put-badarrayindex, junkrefs-put-badarrayfield, junkrefs-put-array-norefval, junkrefs-notin, junkrefs-levelsubset, junkrefs-junkref, junkrefs-delete-02, junkrefs-append, junkrefs-addobj, junkrefs-addarray, junkref-union-disjoint, junkref-subset, junkref-put-statfield, junkref-put-norefval-equiv, junkref-put-norefval-01, junkref-put-norefval, junkref-put-field, junkref-put-badfield, junkref-put-badclassfield, junkref-put-badarrayfield, junkref-put-ba, junkref-put-array-norefval, junkref-primarray-level-01, junkref-levelsubset, junkref-isarray-typeex, junkref-class-01, junkref-class, junkref-array, junkref-addobj-01, junkref-addobj, junkref-addarray-newref-put, junkref-addarray-newref, junkref-addarray-01,
list/storekeys/app-02-ant is used by nojunkref-typeex-02, nojunkref-typeex-01,
list/bytelist/app-02-ant is used by validrefnotnull-putbar, validref-putbar, junkref-putbar-01, junkref-putbar,
list/fieldinit-assoclista/c is used by validref-ac, validfieldinits-validreflist, validfieldinits-def-01, junkref-ac,
list/javavalues/c is used by validreflist-addarray,
list/references/c is used by validref-primarray, validfieldinits-validreflist, junkrefs-union-disjoint, junkrefs-union, junkrefs-typein, junkrefs-supertype, junkrefs-subtype, junkrefs-subset, junkrefs-subclass, junkrefs-put-statfield, junkrefs-put-refval-statfield, junkrefs-put-refval-02, junkrefs-put-refval-01, junkrefs-put-refval, junkrefs-put-null-02, junkrefs-put-null-01, junkrefs-put-null, junkrefs-put-notin-butlast, junkrefs-put-notin, junkrefs-put-norefval-equiv, junkrefs-put-norefval-01, junkrefs-put-badfield, junkrefs-put-badclassfield, junkrefs-put-badarrayindex, junkrefs-put-badarrayfield, junkrefs-put-array-norefval, junkrefs-primarray, junkrefs-null-03, junkrefs-null-01, junkrefs-notin, junkrefs-levelsubset, junkrefs-inttype, junkrefs-delete-02, junkrefs-delete, junkrefs-append, junkrefs-addobj, junkrefs-addarray-noreftype, junkrefs-addarray, junkref-union-disjoint, junkref-subset, junkref-put-statfield, junkref-put-refval-statfield, junkref-put-refval-01, junkref-put-refval, junkref-put-null, junkref-put-norefval-equiv, junkref-put-norefval-01, junkref-put-norefval, junkref-put-field, junkref-put-badfield, junkref-put-badclassfield, junkref-put-badarrayindex, junkref-put-badarrayfield, junkref-put-ba, junkref-put-array-norefval, junkref-primarray-lvl, junkref-primarray-level-01, junkref-null, junkref-levelsubset, junkref-class-01, junkref-class, junkref-array, junkref-addobj-01, junkref-addobj, junkref-addarray-noreftype, junkref-addarray-newref-put, junkref-addarray-newref, junkref-addarray-01,
list/refkeyvalues-assoclista/c is used by validstatfield-putrkvs, validref-putrkvs,
list/storekeys/c is used by validstatfields-put-statfield-01, validstatfields-levelsubset, validstatfields-initundone, validstatfields-addobj, validfieldlist-superset, validfieldlist-put-statfield, nojunkref-typeex-01,
list/bytelist/c is used by validrefnotnull-putbar, validref-putbar, junkref-putbar-01,
list/bytelist/c-07 is used by validrefnotnull-putbar, validref-putbar, junkref-putbar-01, junkref-putbar,
list/references/c-08 is used by validref-not-junkrefs, junkrefs-union-disjoint, junkrefs-supertype, junkrefs-subtype, junkrefs-put-statfield, junkrefs-put-refval-statfield, junkrefs-put-refval-02, junkrefs-put-refval-01, junkrefs-put-refval, junkrefs-put-null-02, junkrefs-put-null-01, junkrefs-put-null, junkrefs-put-notin-butlast, junkrefs-put-norefval-01, junkrefs-put-badfield, junkrefs-put-badclassfield, junkrefs-put-badarrayindex, junkrefs-put-badarrayfield, junkrefs-put-array-norefval, junkrefs-null-01, junkrefs-notin, junkrefs-levelsubset, junkrefs-junkref, junkrefs-delete-02, junkrefs-append, junkrefs-addobj, junkrefs-addarray, junkref-union-disjoint, junkref-subset, junkref-put-statfield, junkref-put-norefval-equiv, junkref-put-norefval-01, junkref-put-norefval, junkref-put-field, junkref-put-badfield, junkref-put-badclassfield, junkref-put-badarrayfield, junkref-put-ba, junkref-put-array-norefval, junkref-primarray-level-01, junkref-levelsubset, junkref-isarray-typeex, junkref-class-01, junkref-class, junkref-array, junkref-addobj-01, junkref-addobj, junkref-addarray-newref-put, junkref-addarray-newref, junkref-addarray-01,
list/bytelist/c-08 is used by validrefnotnull-putbar, validref-putbar, junkref-putbar-01, junkref-putbar,
list/storekeys/e is used by nojunkref-typeex-02,
list/references/e is used by validref-not-junkrefs, junkrefs-union-disjoint, junkrefs-supertype, junkrefs-subtype, junkrefs-put-statfield, junkrefs-put-refval-statfield, junkrefs-put-refval-02, junkrefs-put-refval-01, junkrefs-put-refval, junkrefs-put-null-02, junkrefs-put-null-01, junkrefs-put-null, junkrefs-put-notin-butlast, junkrefs-put-norefval-01, junkrefs-put-badfield, junkrefs-put-badclassfield, junkrefs-put-badarrayindex, junkrefs-put-badarrayfield, junkrefs-put-array-norefval, junkrefs-notin, junkrefs-levelsubset, junkrefs-junkref, junkrefs-delete-02, junkrefs-append, junkrefs-addobj, junkrefs-addarray, junkref-union-disjoint, junkref-subset, junkref-put-statfield, junkref-put-norefval-equiv, junkref-put-norefval-01, junkref-put-norefval, junkref-put-field, junkref-put-badfield, junkref-put-badclassfield, junkref-put-badarrayfield, junkref-put-ba, junkref-put-array-norefval, junkref-primarray-level-01, junkref-newref, junkref-levelsubset, junkref-isarray-typeex, junkref-is-junk, junkref-class-01, junkref-class, junkref-array, junkref-addobj-01, junkref-addobj, junkref-addarray-newref-put, junkref-addarray-newref, junkref-addarray-01,
list/bytelist/e is used by validrefnotnull-putbar, validref-putbar, junkref-putbar-01, junkref-putbar,
list/storekeys/e-01 is used by nojunkref-typeex-01,
list/references/e-01 is used by validref-primarray, junkrefs-union-disjoint, junkrefs-union, junkrefs-supertype, junkrefs-subtype, junkrefs-subset, junkrefs-subclass, junkrefs-put-statfield, junkrefs-put-refval-statfield, junkrefs-put-refval-02, junkrefs-put-refval-01, junkrefs-put-refval, junkrefs-put-null-02, junkrefs-put-null-01, junkrefs-put-null, junkrefs-put-notin, junkrefs-put-norefval-equiv, junkrefs-put-norefval-01, junkrefs-put-badfield, junkrefs-put-badclassfield, junkrefs-put-badarrayindex, junkrefs-put-badarrayfield, junkrefs-put-array-norefval, junkrefs-primarray, junkrefs-null-03, junkrefs-null-01, junkrefs-levelsubset, junkrefs-inttype, junkrefs-delete-02, junkrefs-delete, junkrefs-append, junkrefs-addobj, junkrefs-addarray-noreftype, junkrefs-addarray, junkref-union-disjoint, junkref-subset, junkref-put-statfield, junkref-put-refval-statfield, junkref-put-refval-01, junkref-put-refval, junkref-put-null, junkref-put-norefval-equiv, junkref-put-norefval-01, junkref-put-norefval, junkref-put-field, junkref-put-badfield, junkref-put-badclassfield, junkref-put-badarrayindex, junkref-put-badarrayfield, junkref-put-ba, junkref-put-array-norefval, junkref-primarray-lvl, junkref-primarray-level-01, junkref-null, junkref-levelsubset, junkref-class-01, junkref-class, junkref-array, junkref-addobj-01, junkref-addobj, junkref-addarray-noreftype, junkref-addarray-newref-put, junkref-addarray-newref, junkref-addarray-01,
list/bytelist/e-01 is used by validrefnotnull-putbar, validref-putbar, junkref-putbar-01, junkref-putbar,
list/storekeys/e-02 is used by nojunkref-typeex-01,
list/references/e-02 is used by junkrefs-put-notin-butlast, junkrefs-notin,
list/references/e-03 is used by junkrefs-null-01, junkrefs-notin,
list/references/first is used by junkrefs-null-01, junkref-newref, junkref-isarray-typeex, junkref-is-junk, junkref-class-01, junkref-class, junkref-array,
list/references/first-02 is used by junkrefs-null-01, junkrefs-notin,
list/javavalues/in-06 is used by validreflist-rec,
list/references/in-06 is used by junkrefs-put-notin-butlast, junkrefs-put-notin, junkrefs-delete,
list/storekeys/in-06 is used by validstatfields-rec, validstatfields-put-statfield-01, validfieldlist-rec, validfieldlist-put-statfield,
list/fieldinit-assoclista/in-06 is used by validfieldinits-rec,
list/storekeys/in-08 is used by validstatfields-initundone,
list/references/in-14 is used by junkrefs-put-notin-butlast, junkrefs-notin,
list/storekeys/in-14 is used by validstatfields-initundone,
list/references/in-15 is used by junkrefs-put-notin-butlast, junkrefs-notin,
list/refkeyvalues-assoclista/in-17 is used by validvals-one,
list/javavalues/in-17 is used by validreflist-one, junkreflist-rec,
list/storekeys/in-17 is used by validstatfields-one, validfieldlist-one-01, validfieldlist-mode-01,
list/references/in-17 is used by junkrefs-put-refval-01, junkrefs-put-refval, junkrefs-put-notin-butlast, junkrefs-put-notin, junkrefs-notin, junkrefs-delete,
list/fieldinit-assoclista/in-17 is used by validfieldinits-one,
list/refkeyvalues-assoclista/in-append is used by validvals-append,
list/javavalues/in-append is used by junkreflist-rec,
list/references/in-append is used by junkrefs-put-refval-01, junkrefs-put-refval, junkrefs-put-notin-butlast, junkrefs-put-notin, junkrefs-notin, junkrefs-delete,
list/fieldinit-assoclista/in-empty is used by validfieldinits-empty, junkref-predefined,
list/storekeys/in-empty is used by validstatfields-initundone, validstatfields-empty, validstatfield-primtype-level, validrefnotnull-union-at-right, validref-forward, validfieldlist-empty,
list/references/in-empty is used by junkrefs-put-refval-01, junkrefs-put-refval, junkrefs-put-notin-butlast,
list/javavalues/in-empty is used by validreflist-empty, junkreflist-empty,
list/references/len is used by junkref-primarray-level-01,
list/bytelist/len is used by junkref-putbar,
list/bytelist/len-02 is used by junkref-putbar,
list/references/len-02 is used by junkref-primarray-level-01,

Used from specification storefuns

storefuns/init-existing is used by validstatfields-subset, initsubset-init-forward, initsubset-init,
storefuns/init-put-04 is used by validstatfields-put-statfield-06, validstatfields-put-other-statfield, validstatfields-put-norefval-field-better, validstatfield-put-statfield, validstatfield-put-norefval, initsubset-put-statfield-01, initsubset-put-statfield, initsubset-initerror-04, initsubset-initerror,
storefuns/init-put-05 is used by initsubset-initerror-04,
storefuns/init-put-08 is used by initsubset-put-statfield-01, initsubset-initerror,
storefuns/initdone-put-rkvs is used by validstatfield-putrkvs,
storefuns/lookup-put-rkvs-notin is used by validval-putrkvs, validstatfield-putrkvs,
storefuns/lookup-rec-01 is used by nojunkref-typeex-01,
storefuns/lookup-two is used by validref-class, nojunkref-typeex-01,
storefuns/newref is used by validref-newref-subset,
storefuns/newref-def is used by validref-newref-subset,
storefuns/put-refkeyvalues-rec is used by validref-putrkvs-norefval, validref-putrkvs,
storefuns/put-rkvs-append is used by validstatfield-putrkvs,
storefuns/put-rkvs-switch is used by validref-putrkvs-norefval,
storefuns/del-notin is used by junkrefs-notin-03,
storefuns/in-put-rkvs is used by validstatfield-putrkvs, validref-putrkvs-norefval, validmode-put-nonnull,
storefuns/init is used by initsubset-addclass,
storefuns/init-01 is used by initsubset-addclass,
storefuns/init-error is used by initsubset-initerror-04, initsubset-initerror,
storefuns/init-mode-03 is used by validstatfield-throw-predef, validstatfield-mode, initsubset-mode-02, initsubset-mode-01,
storefuns/init-mode-05 is used by initsubset-mode-02, initsubset-mode-01,
storefuns/init-put is used by validstatfields-put-norefval-field,
storefuns/init-put-08 is used by initsubset-put-statfield,
storefuns/init-put-12 is used by validstatfields-put-norefval-field-better, initsubset-initerror-04, initsubset-initerror,
storefuns/init-put-17 is used by validstatfield-put-statfield-int, initsubset-put-statfield-int,
storefuns/init-put-24 is used by validstatfield-put-norefval, initsubset-put-statfield-01,
storefuns/initdone-02 is used by validstatfields-put-array-norefval, validstatfield-put-array-norefval,
storefuns/instore-01 is used by validval-put-any, validstatfields-class-01, validstatfield-validref, validstatfield-union, validstatfield-throw-predef, validstatfield-putrkvs, validstatfield-put-statfield, validstatfield-put-norefval, validstatfield-put-array-norefval, validstatfield-addclass-other, validrefnotnull-union-at-right, validrefnotnull-putbar, validrefnotnull-array-len-subset, validrefkeynotnull-union, validrefkeynotnull-subset, validrefkeynotnull-statfield-intersect, validrefkeynotnull-refval-in, validrefkeynotnull-put-shortval, validrefkeynotnull-put-byteval, validrefkeynotnull-addobj, validrefkeynotnull-addarray, validref-union, validref-subset, validref-putrkvs-norefval, validref-putbar, validref-put-norefval-equiv, validref-primarray, validref-not-tdnameex, validref-newref-subset, validfieldinits-def-01, validfield-superset, validfield-one, okbytearray-validref, junkrefs-union-disjoint, junkrefs-union, junkrefs-subset, junkrefs-put-notin-butlast, junkrefs-put-norefval-equiv, junkrefs-put-ba, junkrefs-primarray, junkref-union-disjoint, junkref-subset, junkref-putbar-01, junkref-putbar, junkref-put-norefval-equiv, junkref-field-reftype, junkref-classtype, junkref-class-02, junkref-class-01, initsubset-initerror-02,
storefuns/instore-02 is used by validsubset-put-statfield,
storefuns/look-del is used by junkrefs-delete-02, junkrefs-delete,
storefuns/lookup-one is used by validreflist-getarray-less-03, validreflist-getarray-less-02, validreflist-getarray-less-01, validreflist-getarray-less, nojunkref-typeex-01,
storefuns/lookup-put-rkvs-notin is used by validstatfield-putrkvs, validref-putrkvs-norefval, validmode-put-nonnull,
storefuns/newjvmref is used by validrefkeynotnull-notnewref,
storefuns/newref-01 is used by validsubset-predefined-03, validsubset-predefined-02, validsubset-predefined-01, validsubset-predefined, validsubset-addobj-02, validsubset-addobj-01, validsubset-addobj, validstatfields-throw-predef-02, validstatfields-throw-predef-01, validstatfields-throw-predef, validstatfields-addobj-01, validstatfields-addobj, validstatfield-throw-predef, validstatfield-addobj, validrefvalnotnull-addobj, validrefvalnotnull-addarray, validrefval-addobj, validrefval-addarray, validrefnotnull-no-newref, validrefnotnull-addobj, validrefnotnull-addarray-len, validrefnotnull-addarray, validrefkeynotnull-notnewref, validrefkeynotnull-no-newrefs, validrefkeynotnull-addobj, validrefkeynotnull-addarray, validref-throw, validref-newref-subset, validref-newref, validref-addobj-this, validref-addobj, validref-addarray-other-01, validref-addarray-get-01, validref-addarray-get, validref-addarray, validmode-throw-predef-02, validmode-throw-predef-01, validmode-throw-predef, validmode-addobj, validmode-addarray, junkrefs-newref-02, junkrefs-newref-01, junkrefs-newref, junkrefs-addobj, junkrefs-addarray-newref-put, junkrefs-addarray, junkref-predefined, junkref-newref, junkref-addobj-01, junkref-addobj, junkref-addarray-newref-put, junkref-addarray-newref, junkref-addarray-04, junkref-addarray-02, junkref-addarray-01, initsubset-addobj-01, initsubset-addobj,
storefuns/newref-03 is used by validrefkeynotnull-addarray, junkrefs-newref,
storefuns/newref-in-02 is used by validrefkeynotnull-no-newrefs,
storefuns/newref-in-03 is used by validstatfield-throw-predef,
storefuns/newrefsnew is used by validreflist-addarray,
storefuns/put-refkeyvalues-empty is used by validref-putrkvs,
storefuns/put-rkvs-absorb is used by validref-putrkvs-norefval,
storefuns/put-rkvs-one is used by validstatfield-putrkvs,
storefuns/subset-notin is used by validref-newref-subset,

Used from specification int-basic2

Used from specification valuefuns

valuefuns/okval-case is used by validval-index-byteval, validval-field-shortval, validval-field-byteval, validrefnotnull-putbar, validref-putbar,
valuefuns/okval-refval is used by junkref-field-reftype,
valuefuns/okval-refval-01 is used by validfieldinits-validreflist,
valuefuns/val2int-int-01 is used by validref-array,
valuefuns/initial-value is used by junkref-addarray-03,
valuefuns/intval-xtra is used by validrefnotnull-array-len-subset, validref-array, junkrefs-put-ba,
valuefuns/okprimtype-byte is used by junkref-addbytearray,
valuefuns/okprimtype-refval is used by junkrefs-addarray-noreftype,
valuefuns/okval-byte is used by validstatfields-put-byteval-01, junkref-putbar-01, junkref-putbar,
valuefuns/okval-int is used by validval-int, validstatfield-put-statfield-int, validref-intarray-put-01, validref-intarray-put, initsubset-put-statfield-int,
valuefuns/okval-reftype is used by validstatfields-addclass, validstatfield-union, validstatfield-throw-predef, validstatfield-putrkvs, validstatfield-put-norefval, validstatfield-put-array-norefval, validstatfield-primtype-level, validstatfield-addclass-same, validstatfield-addclass-other, validfield-superset, validfield-one, junkrefs-put-norefval-equiv, junkref-addarray-04, initsubset-initerror-02,
valuefuns/okval-refval is used by validval-put-any, validval-null, validstatfield-validref, validstatfield-putrkvs, validref-putrkvs, junkrefs-put-refval-02, junkrefs-put-refval-01, junkrefs-put-refval, junkrefs-put-null-02, junkrefs-put-null-01, junkrefs-put-null, junkrefs-put-norefval-equiv, junkrefs-put-norefval-01, junkref-class-02, junkref-class-01,
valuefuns/okval-refval-01 is used by validval-putrkvs, validval-put-any, validref-putrkvs, validfield-one,
valuefuns/okval-short is used by validval-field-shortval, validrefnotnull-put-shortval, validref-put-shortval,
valuefuns/okval-void is used by validval-put-any, validval-field-norefval, validstatfields-put-norefval-field-better, validstatfields-put-norefval-field,
valuefuns/refval-xtra is used by validstatfield-validref, validrefval-junkref, validreflist-getarray-less-01, validrefkeynotnull-notnewref, validrefkeynotnull-no-newrefs, validref-forward-array, validref-forward, validref-class, validmode-addobj, nojunkref-typeex-02, nojunkref-typeex-01, junkrefs-put-refval, junkref-class-02, junkref-class-01,
valuefuns/typeval-xtra is used by validref-put-badfield, validfieldinits-def-01, junkrefs-put-badfield, junkref-put-refval-01,

Used from specification valuesfuns

valuesfuns/nonnullrefs-no is used by validfieldinits-validreflist,
valuesfuns/mkjavavalues is used by junkref-addbytearray,
valuesfuns/mkvalsr-empty is used by validfieldinits-validreflist,
valuesfuns/mkvalsr-rec is used by validfieldinits-validreflist,
valuesfuns/nonnullrefs-empty is used by validfieldinits-validreflist,
valuesfuns/nonnullrefs-yes is used by validfieldinits-validreflist,

Used from specification fieldspec

Used from specification intnat

intnat/num-i2n-le-02 is used by junkrefs-addarray-noreftype, junkref-addarray-04,
intnat/num-n2i-ls-02 is used by junkref-addarray-01,
intnat/labs is used by validreflist-getarray-less-02, validreflist-getarray-less-01, junkref-not-hasclasstype-01,
intnat/le is used by junkref-addarray-01,
intnat/nat2int is used by junkref-addarray-01,
intnat/nat2int-04 is used by junkref-addarray-01,
intnat/num-n2i-ls-02 is used by junkrefs-addarray-noreftype, junkrefs-addarray, junkref-addarray-04, junkref-addarray-01,
intnat/rax-04 is used by validreflist-getarray-less-02, validreflist-getarray-less-01,

Used from specification int-abs

Used from specification okfuns

okfuns/gfts-all is used by validrefnotnull-union-at-right, junkrefs-union, junkref-field-reftype, junkref-class-02, junkref-class-01,
okfuns/good-field-def is used by validstatfields-addclass, validstatfield-union, validstatfield-putrkvs, validstatfield-put-statfield-int, validstatfield-put-statfield, validstatfield-put-norefval, validstatfield-addclass-same, validstatfield-addclass-other, validfield-superset, validfield-put-statfield, validfield-one, initsubset-put-statfield-int, initsubset-initerror-02,
okfuns/is-any-array is used by validval-put-any, okbytearray-validref, junkrefs-put-ba, junkrefs-addarray-newref-put, junkref-addarray-01,
okfuns/is-real-array-def is used by validval-put-any, validref-putrkvs, same-subclasses-is-array, levelsubset-is-array, junkrefs-primarray, junkref-voidarray, junkref-addarray-01, junkref-abstract, is_valid_ref-levelsubset,
okfuns/is_array-arraytype is used by validref-voidtype,
okfuns/is_array-noreftype is used by junkrefs-primarray,
okfuns/is_array-put is used by junkrefs-put-norefval-01,
okfuns/is_array-put-01 is used by junkrefs-put-refval-02, junkrefs-put-null-02, junkrefs-put-null-01, junkrefs-put-badfield, junkrefs-put-badclassfield, junkrefs-put-badarrayindex, junkrefs-put-array-norefval,
okfuns/is_array-put-field is used by junkrefs-put-null-01, junkrefs-put-norefval-equiv,
okfuns/is_array-put-okval is used by junkrefs-put-refval-02, junkrefs-put-null-02,
okfuns/is_array-put-samefield is used by junkrefs-put-refval-01,
okfuns/is_array-union-disjoint is used by junkrefs-union-disjoint,
okfuns/keys-in is used by validstatfields-addclass,
okfuns/keys-in-01 is used by junkref-addobj-01,
okfuns/okarrayNotNull is used by validrefnotnull-putbar, validref-putbar, validref-primarray, okbytearray-validref, junkrefs-put-ba, junkrefs-primarray, junkref-putbar-01, junkref-putbar, junkref-addarray-01,
okfuns/okbytearray-01 is used by validrefnotnull-putbar, validref-putbar, okbytearray-validref, junkrefs-bytearray, junkref-putbar-01, junkref-putbar, junkref-okarray-byte, bytearray-is-no-junk,
okfuns/okreftype is used by validrefnotnull-putbar, validref-putbar, validref-primarray, validref-okreftype, okbytearray-validref, junkrefs-primarray, junkref-putbar-01, junkref-putbar, junkref-not-okreftype,
okfuns/vals-in is used by validsubset-addobj-01,
okfuns/getkeys-empty is used by junkref-predefined,
okfuns/getvals-empty is used by validfieldinits-validreflist, validfieldinits-def-01,
okfuns/getvals-rec-01 is used by validfieldinits-validreflist, validfieldinits-def-01,
okfuns/gft-mode-01 is used by validstatfield-throw-predef,
okfuns/gft-put is used by validfield-put-statfield,
okfuns/good-field-field is used by validfield-put-statfield,
okfuns/good-field-field-01 is used by validstatfield-union, validstatfield-throw-predef, validstatfield-putrkvs, validstatfield-putbytearray-noreftype, validstatfield-put-statfield, validstatfield-put-norefval, validstatfield-put-array-norefval, validstatfield-primtype-level, validstatfield-addclass-other, validrefnotnull-union-at-right, junkrefs-union, junkref-field-reftype, junkref-class-02, junkref-class-01, initsubset-initerror-02,
okfuns/good-field-in is used by validfield-put-statfield,
okfuns/good-field-in-01 is used by validfield-put-statfield,
okfuns/good-field-index is used by validfield-put-statfield,
okfuns/good-field-put is used by validstatfield-put-array-norefval,
okfuns/is_array-arrayreftype is used by validref-arrayreftype,
okfuns/is_array-arraytype is used by validval-put-any, validref-putrkvs, junkref-primarray-level-01,
okfuns/is_array-bytearray is used by okbytearray-validref, junkrefs-put-ba,
okfuns/is_array-bytearray-01 is used by junkref-okbytearray,
okfuns/is_array-classtype is used by validref-isobj,
okfuns/is_array-del is used by junkrefs-delete-02, junkrefs-delete,
okfuns/is_array-hasnoclasstype is used by junkref-primarray-level-01,
okfuns/is_array-hasnoclasstype-01 is used by junkref-not-hasclasstype-01,
okfuns/is_array-is-array is used by same-subclasses-is-array, junkref-not-valid, junkref-not-is-array,
okfuns/is_array-isarrayref is used by validref-isarrayref,
okfuns/is_array-lenfield is used by validref-array-len-in, junkrefs-union, junkrefs-subset,
okfuns/is_array-length-01 is used by validref-array-01,
okfuns/is_array-length-07 is used by validref-array-02, junkrefs-put-ba,
okfuns/is_array-newref is used by junkrefs-addarray,
okfuns/is_array-notin-01 is used by validref-array-notin, junkrefs-union, junkrefs-subset,
okfuns/is_array-notypeval is used by junkrefs-put-badfield,
okfuns/is_array-null is used by validref-array-rec, validref-array-03,
okfuns/is_array-okarray is used by bytearray-is-no-junk,
okfuns/is_array-okarray-01 is used by validref-okarray, junkrefs-primarray,
okfuns/is_array-primtype is used by junkref-primarray-lvl,
okfuns/is_array-primtype-01 is used by junkref-primarray-lvl,
okfuns/is_array-put-01 is used by junkrefs-put-refval-01, junkrefs-put-refval, junkrefs-put-null, junkrefs-put-notin, junkrefs-put-badclassfield,
okfuns/is_array-put-field is used by junkrefs-put-notin-butlast, junkrefs-put-badarrayfield,
okfuns/is_array-put-jvmref is used by junkrefs-put-statfield, junkrefs-put-refval-statfield,
okfuns/is_array-put-okval is used by junkrefs-put-array-norefval,
okfuns/is_array-reftype is used by junkrefs-put-badfield,
okfuns/is_array-subset is used by junkrefs-subset,
okfuns/is_array-type-01 is used by junkrefs-put-refval-02, junkrefs-put-badclassfield,
okfuns/is_array-type-02 is used by junkrefs-union, junkrefs-subset,
okfuns/is_array-type-04 is used by validrefnotnull-union-at-right, validref-class, junkref-field-reftype, junkref-classtype,
okfuns/is_array-typele is used by validref-no-obj, validref-forward, validref-array-03,
okfuns/is_array-union is used by junkrefs-union,
okfuns/isarray-bytearray is used by junkref-okbytearray,
okfuns/isarray-length-07 is used by junkrefs-primarray,
okfuns/isarray-null is used by junkrefs-put-ba, junkref-isarray-typeex,
okfuns/isarray-okarray is used by junkrefs-primarray,
okfuns/okarray-01 is used by junkref-okarray-byte,
okfuns/okarray-04 is used by validrefnotnull-primarray,
okfuns/okarray-05 is used by validval-put-any, validrefnotnull-putbar, validrefnotnull-primarray, validref-putbar, validref-primarray, okbytearray-validref, junkrefs-put-ba, junkrefs-primarray, junkrefs-bytearray, junkref-putbar-01, junkref-putbar,
okfuns/okarray-jvmref-01 is used by junkref-okarray-byte,
okfuns/okarray-okarray-02 is used by junkref-okarray-byte,
okfuns/okarray-type-03 is used by okbytearray-validref,
okfuns/okbar is used by validsubset-okbytearray, okbytearray-validref, okbytearray-putrkvs,
okfuns/okbar-norefval is used by bytearray-is-no-junk,
okfuns/okbytearray-02 is used by validrefnotnull-bytearray, validref-bytearray, junkrefs-bytearray,
okfuns/okreftype-null is used by junkref-not-okreftype-01, junkref-not-okreftype,
okfuns/oktype-byte is used by validrefnotnull-putbar, validref-putbar, validref-put-byteval, okbytearray-validref, junkrefs-put-ba, junkref-putbar-01, junkref-putbar,
okfuns/oktype-class is used by junkref-addarray-01,
okfuns/oktype-okval is used by validstatfields-put-norefval-field-better, validstatfields-put-norefval-field, validstatfield-put-norefval, validref-putrkvs-norefval, validref-put-norefval-equiv, validref-put-norefval-01, validref-put-norefval, validref-primarray, validfieldinits-def-01, junkrefs-put-refval-01, junkrefs-put-refval, junkrefs-put-null-01, junkrefs-put-null, junkrefs-put-notin-butlast, junkrefs-put-norefval-01, junkrefs-put-norefval, junkrefs-primarray, junkref-put-norefval, junkref-addobj-01,
okfuns/vals-at-in-01 is used by validfieldinits-junkref,

Used from specification storekey

Used from specification typefuns

typefuns/array-le is used by junkrefs-put-refval-02, junkref-put-refval-01,
typefuns/classex-def is used by levelsubset-classex-03, levelsubset-classex,
typefuns/is-reftype is used by junkref-field-reftype,
typefuns/le-hasct is used by validref-primarray, junkref-primarray-level-01,
typefuns/le-noreftype-01 is used by validref-put-field, junkrefs-primarray,
typefuns/subclass-01 is used by validrefnotnull-union-at-right, validref-forward, same-subclasses-typeex,
typefuns/subtype-object is used by same-subclasses-typeex,
typefuns/tdname+ex-def is used by validstatfield-primtype-level, same-subclasses-typeex, same-subclasses-tdnameex-01, same-subclasses-is-array, levelsubset-all-types,
typefuns/tdnameex-def is used by validstatfields-empty-01, same-subclasses-typeex, same-subclasses-tdnameex-04, same-subclasses-tdnameex-02, same-subclasses-is-array, levelsubset-tdnameex, levelsubset-all-types,
typefuns/typeex-def is used by same-subclasses-typeex, same-subclasses-is-array, levelsubset-all-types,
typefuns/array is used by validref-type, validref-primarray, validref-okarray, validref-isarrayref, validref-intarray-put-01, validref-intarray-put, validref-forward-array, validref-arraytype, validref-arrayreftype, validref-array-notin, validref-array-len-in, validref-array-02, validref-array-01, junkrefs-primarray, junkref-primarray-lvl,
typefuns/bytearray is used by validrefnotnull-putbar, validref-putbar, okbytearray-validref, okbytearray-02, junkrefs-put-ba, junkref-putbar-01, junkref-putbar,
typefuns/class-le is used by validref-not-tdnameex, validref-class, validref-addobj-this, junkrefs-union, junkrefs-put-badclassfield,
typefuns/classex is used by same-subclasses-classex, junkref-predefined,
typefuns/classex-01 is used by validsubset-addobj-01, same-subclasses-classex,
typefuns/classex-02 is used by same-subclasses-classex, levelsubset-classex-02,
typefuns/classex-nointerface is used by levelsubset-classex-03,
typefuns/classex-notpredef is used by same-subclasses-typeex, same-subclasses-is-array, levelsubset-all-types,
typefuns/classex-object is used by same-subclasses-typeex,
typefuns/classex-object-01 is used by same-subclasses-tdnameex,
typefuns/dims-pos is used by junkref-not-hasclasstype-01,
typefuns/dims-succ is used by junkref-not-hasclasstype-01,
typefuns/elemtype-01 is used by validref-addarray-same-01,
typefuns/elemtype-05 is used by validval-put-any, validref-putrkvs, junkref-voidarray,
typefuns/elemtype-06 is used by junkref-abstract,
typefuns/elemtype-07 is used by validref-putrkvs, junkref-voidarray, junkref-addarray-01, junkref-abstract,
typefuns/elemtype-rec is used by validval-put-any, junkrefs-primarray,
typefuns/hasclass-class is used by junkref-not-hasclasstype-01,
typefuns/hasct-05 is used by junkref-primarray-level-01, junkref-not-hasclasstype-01,
typefuns/interfaceex-noclass is used by levelsubset-classex-02,
typefuns/interfaceex-notpredef is used by levelsubset-classex-03, levelsubset-classex-02,
typefuns/interfaceex-object is used by same-subclasses-typeex,
typefuns/is_abstract-predef is used by junkref-predefined,
typefuns/is_primtype-01 is used by validstatfield-primtype-level, junkrefs-primarray,
typefuns/is_primtype-02 is used by junkrefs-primarray,
typefuns/is_primtype-03 is used by validstatfield-primtype-level, junkrefs-primarray,
typefuns/isreftype-01 is used by validstatfield-put-statfield-int, junkrefs-put-null-01, junkref-put-refval, initsubset-put-statfield-int,
typefuns/isreftype-04 is used by validval-null,
typefuns/isreftype-06 is used by validval-put-any, validref-putrkvs, validref-put-refval, validref-put-null, validref-put-badfield, junkrefs-put-null-01, junkrefs-put-null, junkref-put-refval, junkref-put-null,
typefuns/jtclass is used by same-subclasses-typeex, same-subclasses-is-array, levelsubset-all-types,
typefuns/jtelemtype-class is used by junkref-addarray-01,
typefuns/le-02 is used by junkref-field-reftype,
typefuns/le-04 is used by validfieldinits-def-01, junkrefs-put-badfield, junkref-put-refval-01,
typefuns/le-06 is used by okbytearray-validref,
typefuns/le-08 is used by validref-type, validref-intarray-put-01, validref-intarray-put, junkrefs-inttype, junkref-put-refval,
typefuns/le-11 is used by validref-voidtype, junkrefs-put-refval, junkref-put-refval, junkref-put-field,
typefuns/le-13 is used by junkrefs-put-ba,
typefuns/le-hasct is used by validref-hasnoclasstype-level, junkref-primarray-level-01, junkref-not-hasclasstype-01,
typefuns/le-noreftype is used by validref-noreftype, junkrefs-put-badfield,
typefuns/le-noreftype-01 is used by junkrefs-put-refval-02, junkrefs-put-refval-01, junkrefs-put-refval, junkref-put-refval-01, junkref-class-02, junkref-class-01,
typefuns/prim-abstract is used by junkrefs-primarray,
typefuns/prim-byte is used by validrefnotnull-bytearray, validref-bytearray, junkrefs-bytearray, junkref-addbytearray,
typefuns/prim-classtype is used by validref-primarray,
typefuns/prim-void is used by junkrefs-primarray,
typefuns/ref is used by validref-type-forward, validref-runtimetype, validref-put-field-refval-01, validref-put-field-refval, validref-put-array-refval-02, validref-addarray-same, junkrefs-supertype, junkrefs-subclass, junkrefs-sametype, junkref-put-refval-statfield, junkref-put-badfield, junkref-primarray-lvl, junkref-isarray-typeex, junkref-class-01, junkref-class, junkref-array, junkref-addobj-01, junkref-addarray-noreftype, junkref-addarray-01,
typefuns/reftype is used by validfieldinits-validreflist, junkref-not-hasclasstype-01, junkref-field-reftype,
typefuns/subarray1 is used by validref-put-array-refval-02, validref-forward-array, validref-arrayreftype, validref-addarray-same, okbytearray-validref, junkrefs-primarray, junkref-primarray-lvl, junkref-addarray-noreftype, junkref-addarray-01,
typefuns/subbasic2 is used by validreflist-no-reftype, validref-bad-type,
typefuns/subclass is used by validrefnotnull-union-at-right, validref-subtype, validref-addobj-this, validmode-throw-predef, junkref-classtype, junkref-addobj-01,
typefuns/subclass-01 is used by validref-isobj,
typefuns/subtype-object is used by validfieldinits-validreflist,
typefuns/subtype-object-01 is used by validref-object-01, validref-object,
typefuns/tdnameex is used by same-subclasses-typeex, same-subclasses-tdnameex-02, levelsubset-tdnameex,
typefuns/tdnameex-01 is used by same-subclasses-typeex, same-subclasses-tdnameex-02, levelsubset-tdnameex,
typefuns/tdnameex-02 is used by validstatfield-primtype-level,
typefuns/tdnameex-03 is used by same-subclasses-typeex, same-subclasses-tdnameex-01, same-subclasses-is-array,
typefuns/tdnameex-04 is used by validref-not-tdnameex,
typefuns/tdnameex-05 is used by junkref-addarray-01,
typefuns/tdnameex-def is used by validstatfields-empty-01,
typefuns/transitivity is used by validref-supertype, validref-forward-array, junkrefs-subtype, junkrefs-put-refval-02, junkref-put-refval-01, junkref-put-refval,
typefuns/transitivity-01 is used by validref-subtype-02,
typefuns/typeex-array is used by junkrefs-primarray, junkref-addarray-01,
typefuns/typeex-class is used by validref-subtype-02, validref-addobj-this, same-subclasses-typeex, junkref-addarray-01,
typefuns/typeex-prim is used by validstatfield-put-statfield-int, validref-addarray-same-01, initsubset-put-statfield-int,
typefuns/typeex-prim-08 is used by validstatfield-addclass-same,

Used from specification fieldname

fieldname/inj is used by validstatfields-throw-predef, validstatfields-put-statfield-06, validstatfields-put-statfield-05, initsubset-put-statfield-01, initsubset-put-statfield, initsubset-initerror-04, initsubset-initerror,

Used from specification pair

pair/fieldinit/elim is used by validref-ac, validfieldinits-validreflist, validfieldinits-rec, validfieldinits-one, validfieldinits-def-01, junkref-ac,
pair/refkeyvalues/elim is used by validvals-putrkvs, validvals-put-any, validvals-one, validvals-append, validref-putrkvs,
pair/fieldinit/inj is used by validfieldinits-rec, validfieldinits-one,
pair/refkeyvalues/sel-01 is used by validvals-voidtype, validvals-putrkvs, validvals-put-any, validvals-one, validvals-append, validstatfield-putrkvs,
pair/fieldinit/sel-01 is used by validfieldinits-validreflist, validfieldinits-def-01,
pair/refkeyvalues/sel-02 is used by validvals-voidtype, validvals-putrkvs, validvals-put-any, validvals-one, validvals-append, validstatfield-putrkvs,
pair/fieldinit/sel-02 is used by validref-ac, validfieldinits-validreflist, validfieldinits-def-01, junkref-ac,

Used from specification classnamefuns

Used from specification nat-basic1

nat-basic1/f is used by junkref-addarray-01,
nat-basic1/ref-1 is used by junkref-putbar, junkref-primarray-level-01, junkref-addarray-01,
nat-basic1/z is used by junkrefs-addarray-noreftype, junkrefs-addarray, junkref-addarray-04, junkref-addarray-01,

Used from specification oelem

oelem/intlista/irreflexivity is used by validreflist-getarray-less-02, validreflist-getarray-less-01,
oelem/intlista/lel is used by junkrefs-put-refval-02, junkrefs-put-null-02, junkrefs-put-array-norefval,

Used from specification set-basic

set-basic/references/ne-01 is used by junkrefs-union-disjoint, junkref-union-disjoint,

Used from specification refkey

Used from specification javatype

javatype/ex-02 is used by validref-type, junkref-not-hasclasstype-01,
javatype/diff-01 is used by junkref-not-hasclasstype-01,
javatype/disj-02 is used by validval-put-any, validref-putrkvs, junkref-voidarray, junkref-field-reftype, junkref-class-01, junkref-abstract,
javatype/disj-06 is used by validref-put-byteval,
javatype/disj-07 is used by junkref-addarray-01,
javatype/disj-09 is used by validval-null, junkref-addarray-01,
javatype/disj-10 is used by junkrefs-put-ba,
javatype/disj-14 is used by validref-addarray-same-01,
javatype/disj-21 is used by validrefnotnull-put-shortval, validref-put-shortval,
javatype/disj-22 is used by junkrefs-put-ba,
javatype/disj-26 is used by validstatfield-put-statfield-int, validref-addarray-same-01, junkref-put-refval, initsubset-put-statfield-int,
javatype/disj-33 is used by validval-field-byteval, validstatfields-put-byteval-01,
javatype/elim-01 is used by validref-putrkvs, validref-put-array-refval-03, validref-put-array-refval-02, validref-primarray, validref-okarray, validref-isarrayref, validref-forward-array, validref-arrayreftype, validref-array-len-in, junkrefs-primarray, junkref-primarray-level-01,
javatype/elim-02 is used by validrefnotnull-union-at-right, validref-put-badclassfield, validref-not-tdnameex, validref-addobj-this, same-subclasses-typeex, junkrefs-union, junkrefs-put-badclassfield, junkref-put-badclassfield, junkref-class-02, junkref-class-01, junkref-addarray-01,
javatype/inj-01 is used by validrefnotnull-type, validref-type, validref-primarray, okbytearray-validref, junkrefs-put-ba, junkrefs-addarray-newref-put, junkref-put-ba, junkref-addarray-newref-put,
javatype/inj-02 is used by validrefnotnull-union-at-right, junkrefs-union, junkref-class-01,
javatype/sel-01 is used by validrefnotnull-putbar, validref-type, validref-putbar, validref-put-array-refval-03, validref-forward-array, validref-arrayreftype, okbytearray-validref, junkrefs-put-ba, junkrefs-primarray, junkrefs-addarray-noreftype, junkrefs-addarray-newref-put, junkrefs-addarray, junkref-putbar-01, junkref-putbar, junkref-primarray-lvl, junkref-not-hasclasstype-01, junkref-addarray-04, junkref-addarray-01,
javatype/sel-02 is used by validrefnotnull-union-at-right, validref-put-badclassfield, validref-not-tdnameex, validref-class, junkrefs-put-badclassfield, junkref-put-badclassfield, junkref-field-reftype, junkref-classtype, junkref-addobj-01,
javatype/test-07 is used by junkref-addarray-01,
javatype/test-09 is used by validref-putrkvs, validref-put-array-refval-03, validref-put-array-refval-02, validref-primarray, validref-isarrayref, validref-forward-array, validref-arrayreftype, okbytearray-validref, junkrefs-put-ba, junkrefs-primarray, junkrefs-addarray-newref-put, junkref-primarray-lvl, junkref-primarray-level-01, junkref-addarray-01,
javatype/test-10 is used by validrefnotnull-union-at-right, validref-put-badclassfield, validref-not-tdnameex, validref-addobj-this, same-subclasses-typeex, junkrefs-union, junkrefs-put-badclassfield, junkref-put-badclassfield, junkref-field-reftype, junkref-classtype, junkref-class-02, junkref-class-01, junkref-addarray-01,
javatype/test-22 is used by validref-voidtype, junkref-addarray-01,
javatype/test-23 is used by validref-voidtype,
javatype/test-28 is used by junkref-put-refval-01,

Used from specification javavalue

Used from specification storearrays

storearrays/get-rec-01 is used by validreflist-getarray-less-02, validreflist-getarray-less-01,
storearrays/getarray-in is used by validreflist-getarray,
storearrays/getarray-subset is used by validrefnotnull-getarray-subset,
storearrays/putBar-rec is used by validrefnotnull-putbar, validref-putbar, junkref-putbar-01, junkref-putbar,
storearrays/get-zero is used by validreflist-getarray-less-02, validreflist-getarray-less-01,
storearrays/pubBar-init is used by validstatfield-putbytearray-noreftype,
storearrays/putBar-at-type is used by validrefnotnull-putbar, validref-putbar, junkref-putbar-01, junkref-putbar,
storearrays/putBar-empty is used by validrefnotnull-putbar, validref-putbar, junkref-putbar-01, junkref-putbar,
storearrays/putbar-atfs-01 is used by validstatfield-putbytearray-noreftype,
storearrays/putbar-infs is used by validstatfield-putbytearray-noreftype,

Used from specification list-data

Used from specification specialkeys

specialkeys/type is used by validvals-voidtype-02, junkref-put-badfield,
specialkeys/uninit is used by validvals-voidtype-01,
specialkeys/length-01 is used by validstatfields-put-norefval-field-better,
specialkeys/length-02 is used by validval-field-byteval, validstatfields-put-byteval-01, junkrefs-put-null-01, junkrefs-put-ba, junkref-put-refval,
specialkeys/length-03 is used by junkrefs-put-null-01, junkref-put-refval,
specialkeys/length-diff is used by validval-field-shortval, validrefnotnull-put-shortval, validrefkeynotnull-put-shortval, validref-put-shortval,
specialkeys/mode-02 is used by validstatfield-throw-predef, validmode-put-statfield-02, validmode-put-statfield-01, validmode-put-statfield, validfieldlist-mode-01, validfieldlist-mode,
specialkeys/mode-03 is used by validfieldlist-mode-01, validfieldlist-mode,
specialkeys/mode-06 is used by validmode-noval-put-01,
specialkeys/mode-key is used by validstatfields-throw-predef, validstatfield-mode,
specialkeys/mode-ref is used by validsubset-put-statfield-02, validstatfields-throw-predef, validstatfield-throw-predef, validstatfield-mode, validref-throw, validref-mode, validfieldlist-mode,
specialkeys/type-01 is used by validref-put-refval, validref-put-null, junkrefs-put-refval, junkrefs-put-null-01, junkrefs-put-null, junkref-put-null, junkref-put-field, junkref-put-badfield,
specialkeys/type-03 is used by validval-put-any, junkref-put-refval-01,
specialkeys/type-04 is used by validval-put-any, junkrefs-put-null-01, junkrefs-put-badfield,
specialkeys/type-05 is used by validref-put-refval, validref-put-null, junkrefs-put-refval, junkrefs-put-null-01, junkrefs-put-null, junkref-put-null, junkref-put-field,
specialkeys/type-06 is used by validval-put-any,
specialkeys/type-09 is used by validstatfields-put-byteval-01, validrefnotnull-put-byteval, validrefkeynotnull-put-byteval, validref-put-byteval,
specialkeys/type-fieldspec is used by validval-put-any,
specialkeys/type-neq is used by validval-put-any, validstatfields-put-norefval-field, junkrefs-put-refval-01, junkrefs-put-refval, junkrefs-put-norefval-equiv,
specialkeys/uninit-02 is used by validstatfields-put-norefval-field-better, validstatfield-put-norefval,
specialkeys/uninit-eq is used by validstatfields-put-statfield-06, validstatfields-put-other-statfield, validstatfield-put-statfield, initsubset-put-statfield-01, initsubset-put-statfield, initsubset-initerror-04, initsubset-initerror,

Used from specification storefunsx

storefunsx/instore-inrefs is used by junkrefs-union-disjoint, junkref-union-disjoint,
storefunsx/refs-notin is used by junkref-union-disjoint,
storefunsx/union-at-left is used by junkrefs-union-disjoint, junkref-union-disjoint,
storefunsx/union-at-right-01 is used by validrefnotnull-union-at-right, validrefkeynotnull-union, validref-union, junkrefs-union,
storefunsx/instore-inrefs-01 is used by validrefkeynotnull-statfield-intersect,
storefunsx/lookup-xtra is used by validrefnotnull-union-at-right, validrefnotnull-array-len-subset, validrefkeynotnull-union, validrefkeynotnull-subset, validref-union, validref-subset, validmode-put-nonnull, validfieldinits-def-01, junkrefs-union, junkrefs-subset, junkref-subset,
storefunsx/refs-empty-01 is used by junkrefs-union-disjoint, junkref-union-disjoint,
storefunsx/refs-notin is used by validrefkeynotnull-statfield-intersect,
storefunsx/union-at-left is used by validrefnotnull-union-at-right, junkrefs-union,
storefunsx/union-at-right-01 is used by validstatfield-union, validrefkeynotnull-union-same-01, validrefkeynotnull-union-same, validrefkeynotnull-union, junkrefs-union-disjoint, junkrefs-union, junkref-union-disjoint,
storefunsx/union-in is used by validstatfield-union, validrefkeynotnull-union,
storefunsx/union-init is used by validstatfields-union, validstatfield-union,
storefunsx/union-subset is used by junkref-union,
storefunsx/union-subset-left is used by validref-union-left,

Used from specification predefined

predefined/le-06 is used by validmode-throw-predef-02,
predefined/le-09 is used by validmode-throw-predef-01,
predefined/predef-02 is used by validsubset-predefined-03, validstatfields-throw-predef-02, validmode-throw-predef-01,
predefined/predef-08 is used by validsubset-predefined-02, validstatfields-throw-predef-01, validmode-throw-predef-02,

Used from specification javastore

Used from specification assoclist

assoclist/fieldinit/in-append is used by validfieldinits-def-01,
assoclist/refkeyvalues/inassoc is used by validvals-voidtype,
assoclist/refkeyvalues/lastoccurrence-key is used by validstatfield-putrkvs,
assoclist/fieldinit/empty is used by validfieldinits-def-01,
assoclist/fieldinit/in-assoclist is used by junkref-addobj-01,
assoclist/fieldinit/in-assoclist-01 is used by validstatfields-addclass,
assoclist/fieldinit/inone is used by validfieldinits-def-01,

Used from specification classname

classname/inj is used by validref-no-obj, validref-array-03, validmode-throw-predef-02, validmode-throw-predef-01, validmode-put-statfield-02,

Used from specification addfuns

addfuns/ac-init-03 is used by initsubset-initerror-02,
addfuns/ac-init-05 is used by initsubset-initerror-02,
addfuns/ac-lookup is used by validstatfields-addclass,
addfuns/ac-lookup-06 is used by validstatfields-addclass,
addfuns/ac-no1 is used by validref-ac, junkref-ac,
addfuns/ac-no2 is used by validref-ac, junkref-ac,
addfuns/add-in-09 is used by junkref-addobj-01,
addfuns/add-ref is used by validref-addobj, junkref-addobj,
addfuns/addclass-base is used by validref-ac, junkref-ac,
addfuns/addclass-yes is used by validref-ac, junkref-ac,
addfuns/instfields-subclass is used by validrefnotnull-union-at-right,
addfuns/is-any-object is used by validrefnotnull-union-at-right, junkrefs-union, junkref-field-reftype, junkref-classtype, junkref-class-01,
addfuns/is-real-object-def is used by validrefnotnull-union-at-right, same-subclasses-is-obj, levelsubset-is-obj, junkrefs-union, junkref-not-valid, junkref-field-reftype, junkref-classtype, junkref-class-01, is_valid_ref-levelsubset,
addfuns/is-valid-ref is used by junkref-not-valid,
addfuns/is-valid-ref-stronger-def is used by validref-voidtype, validref-isarrayref, validref-addarray-same, junkrefs-union-disjoint, junkrefs-union, junkrefs-supertype, junkrefs-subtype, junkrefs-subset, junkrefs-put-statfield, junkrefs-put-refval-statfield, junkrefs-put-refval-02, junkrefs-put-refval-01, junkrefs-put-refval, junkrefs-put-null-02, junkrefs-put-null-01, junkrefs-put-null, junkrefs-put-notin-butlast, junkrefs-put-notin, junkrefs-put-norefval-equiv, junkrefs-put-norefval-01, junkrefs-put-badfield, junkrefs-put-badclassfield, junkrefs-put-badarrayindex, junkrefs-put-badarrayfield, junkrefs-put-array-norefval, junkrefs-primarray, junkrefs-one, junkrefs-null-01, junkrefs-notin, junkrefs-levelsubset, junkrefs-delete-02, junkrefs-append, junkrefs-addobj, junkrefs-addarray, junkref-primarray-level-01, junkref-not-valid, junkref-classtype, junkref-addobj-01, junkref-abstract, is_valid_ref-levelsubset,
addfuns/is_obj-classtype is used by validref-voidtype,
addfuns/is_obj-def is used by validrefnotnull-union-at-right, junkrefs-union, junkref-field-reftype, junkref-class-01,
addfuns/is_obj-full-expand is used by validref-not-tdnameex, junkref-class-02,
addfuns/is_obj-put is used by junkrefs-put-null-01, junkrefs-put-null, junkrefs-put-norefval-01,
addfuns/is_obj-put-01 is used by junkrefs-put-badfield, junkrefs-put-badclassfield, junkrefs-put-badarrayfield,
addfuns/is_obj-put-badfield is used by junkrefs-put-badclassfield,
addfuns/is_obj-put-equiv is used by junkrefs-put-norefval-equiv,
addfuns/is_obj-put-samefield-01 is used by junkrefs-put-refval-01, junkrefs-put-refval,
addfuns/is_valid_ref-put-samefield is used by junkrefs-put-notin-butlast,
addfuns/is_valid_ref-reftype is used by junkref-not-hasclasstype-01,
addfuns/statfields-index-01 is used by validstatfields-put-other-statfield,
addfuns/statfields-same-class-01 is used by validstatfields-subset, validstatfields-put-other-statfield, validstatfields-initundone, validstatfields-class-01, validstatfields-addclass, initsubset-initerror-04, initsubset-addclass,
addfuns/validfieldinits-all is used by junkref-addobj-01,
addfuns/validfieldinits-rec is used by validfieldinits-def-01,
addfuns/ac-in-04 is used by validstatfields-addclass, validstatfield-addclass-same,
addfuns/ac-in-06 is used by validstatfield-addclass-other, initsubset-initerror-02,
addfuns/ac-in-09 is used by validsubset-addclass,
addfuns/ac-init-03 is used by validstatfield-addclass-other, initsubset-initerror-02, initsubset-addclass,
addfuns/ac-init-05 is used by initsubset-addclass,
addfuns/ac-init-09 is used by initsubset-initerror-02,
addfuns/ac-init-11 is used by initsubset-initerror-02,
addfuns/ac-lookup is used by validstatfield-addclass-same,
addfuns/ac-lookup-02 is used by validstatfield-addclass-other, initsubset-initerror-02,
addfuns/ac-mode is used by validmode-addclass,
addfuns/ac-shift-02 is used by validref-ac, junkref-ac,
addfuns/add-at is used by validstatfield-throw-predef, validrefkeynotnull-addobj,
addfuns/add-goodfield is used by validstatfield-throw-predef,
addfuns/add-in-02 is used by validsubset-predefined, validsubset-addobj,
addfuns/add-in-03 is used by validrefkeynotnull-addobj,
addfuns/add-in-09 is used by junkref-addobj,
addfuns/add-init is used by validstatfield-throw-predef,
addfuns/add-mode is used by validmode-addobj,
addfuns/add-ref is used by junkrefs-addobj,
addfuns/add-type is used by validref-addobj-this, junkref-addobj-01, junkref-addobj,
addfuns/add-type-01 is used by validmode-throw-predef,
addfuns/addclass-mode-in is used by validmode-addclass,
addfuns/ao-init is used by validstatfields-addobj-01, validstatfield-addobj, initsubset-addobj-01,
addfuns/ao-init-02 is used by initsubset-addobj-01,
addfuns/instfields-Object is used by validrefnotnull-union-at-right, validref-forward,
addfuns/instfields-abstract is used by validref-class, junkref-field-reftype, junkref-class-01,
addfuns/instfields-predef is used by junkref-predefined,
addfuns/instfields-special is used by junkrefs-put-null, junkref-field-reftype, junkref-class-02, junkref-class-01,
addfuns/instfields-subclass is used by validrefnotnull-union-at-right, validref-forward,
addfuns/instfields-type is used by validref-addobj-this, junkref-addobj-01,
addfuns/instfields-type-01 is used by junkrefs-put-refval, junkrefs-put-null, junkref-put-field,
addfuns/is_array-addobj is used by junkrefs-addobj,
addfuns/is_obj-01 is used by same-subclasses-is-obj,
addfuns/is_obj-addobj is used by junkrefs-addobj,
addfuns/is_obj-addobj-01 is used by junkref-addobj-01,
addfuns/is_obj-array is used by validrefnotnull-isarray, validref-isarray, junkrefs-primarray,
addfuns/is_obj-array-01 is used by junkref-isarray-typeex,
addfuns/is_obj-arraytype is used by validref-voidtype, validref-arraytype, junkrefs-put-badarrayfield,
addfuns/is_obj-classtype is used by validreflist-no-reftype, validref-object, validref-bad-type, junkref-bad-type,
addfuns/is_obj-del is used by junkrefs-delete-02, junkrefs-delete,
addfuns/is_obj-hasclasstype is used by junkref-primarray-level-01,
addfuns/is_obj-isarray is used by junkrefs-delete, junkref-rec-keep-case, junkref-rec-case,
addfuns/is_obj-newref is used by junkrefs-addarray,
addfuns/is_obj-not-tdnameex is used by junkref-tdnameex,
addfuns/is_obj-notin-01 is used by junkrefs-subset,
addfuns/is_obj-null is used by validref-class-rec-better, validref-class-rec, validref-arraytype,
addfuns/is_obj-put-01 is used by junkrefs-put-refval-01, junkrefs-put-refval, junkrefs-put-notin-butlast, junkrefs-put-notin, junkrefs-put-badarrayfield,
addfuns/is_obj-put-index is used by junkrefs-put-refval-02, junkrefs-put-null-02, junkrefs-put-badarrayindex, junkrefs-put-array-norefval,
addfuns/is_obj-put-statfield is used by junkrefs-put-statfield, junkrefs-put-refval-statfield,
addfuns/is_obj-reftype is used by junkrefs-put-badfield,
addfuns/is_obj-subset is used by junkrefs-subset,
addfuns/is_obj-type is used by junkrefs-union, junkrefs-subset,
addfuns/is_obj-type-01 is used by junkrefs-put-badfield,
addfuns/is_obj-type-02 is used by validref-isarrayref, junkref-is_array, junkref-abstract,
addfuns/is_obj-union is used by junkrefs-union,
addfuns/is_obj-union-disjoint is used by junkrefs-union-disjoint,
addfuns/is_valid_ref is used by validrefnotnull-union-at-right, validrefnotnull-isvalidref, validref-no-obj, validref-isvalidref, validref-isobj, validref-forward, validref-class, junkrefs-put-refval, junkref-field-reftype,
addfuns/is_valid_ref-01 is used by validrefnotnull-isvalidref, validrefnotnull-isarray, validref-isvalidref, validref-isarray, junkrefs-union-disjoint, junkrefs-delete, junkref-rec-case, junkref-isarray-typeex, junkref-is_array,
addfuns/is_valid_ref-array is used by validref-forward-array, validref-arrayreftype, validref-array-len-in, junkref-voidarray, junkref-okbytearray, junkref-not-is-array, junkref-not-hasclasstype-01,
addfuns/is_valid_ref-array-01 is used by validref-type, validref-okarray, validref-array-notin, validref-array-02, validref-array-01, junkrefs-primarray,
addfuns/is_valid_ref-del is used by junkrefs-delete-02,
addfuns/is_valid_ref-del-01 is used by junkrefs-delete-02,
addfuns/is_valid_ref-field-in is used by validrefkeynotnull-has-field,
addfuns/is_valid_ref-int is used by junkrefs-inttype,
addfuns/is_valid_ref-isarray is used by validreflist-getarray-less-01, junkrefs-delete, junkref-rec-keep-case, junkref-rec-case,
addfuns/is_valid_ref-isobj is used by validrefnotnull-union-at-right, validref-forward, validref-class-rec-better, validref-class, junkrefs-put-refval, junkref-rec-keep-case,
addfuns/is_valid_ref-new is used by junkrefs-newref-02, junkrefs-newref-01, junkrefs-addobj,
addfuns/is_valid_ref-no-arraytype is used by validreflist-no-reftype, validref-object, validref-bad-type, junkref-bad-type,
addfuns/is_valid_ref-notin is used by junkrefs-notin-02, junkrefs-notin-01, junkref-notin,
addfuns/is_valid_ref-notin-01 is used by validref-okreftype, validref-no-type, validfieldinits-def-01, junkrefs-typein, junkref-not-okreftype, junkref-keyin,
addfuns/is_valid_ref-primarray is used by junkref-primarray-lvl,
addfuns/is_valid_ref-put-01 is used by junkrefs-put-statfield, junkrefs-put-notin-butlast, junkrefs-put-notin,
addfuns/is_valid_ref-reftype is used by junkref-put-badfield, junkref-noreftype,
addfuns/is_valid_ref-type is used by junkrefs-subclass,
addfuns/is_valid_ref-type-01 is used by validref-not-tdnameex, junkref-tdnameex,
addfuns/is_valid_ref-typeex is used by nojunkref-typeex, junkref-not-okreftype-01, junkref-isarray-typeex,
addfuns/is_valid_ref-typeval is used by validref-okreftype, validfieldinits-def-01, junkref-put-badfield, junkref-not-okreftype,
addfuns/is_valid_ref-void is used by junkref-void,
addfuns/isarray-isobj-01 is used by validrefnotnull-isvalidref, validref-isvalidref, validref-forward, junkref-rec-keep-case, junkref-rec-case,
addfuns/isobj-array-01 is used by junkrefs-put-refval, junkrefs-put-null,
addfuns/isobj-instfields is used by junkrefs-union, junkref-class-01,
addfuns/isobj-isarray is used by is_valid_ref-levelsubset,
addfuns/isobj-type-08 is used by same-subclasses-is-obj, is_valid_ref-levelsubset,
addfuns/mode-addobj is used by validmode-addobj,
addfuns/statfields-index is used by validstatfields-addclass-other,
addfuns/statfields-index-01 is used by validstatfields-subset, validstatfields-put-statfield-06, validstatfields-initundone, validstatfields-class-01, validstatfields-addclass, initsubset-put-statfield-01, initsubset-initerror-04,
addfuns/statfields-predef is used by validstatfield-primtype-level,
addfuns/statfields-same-class-01 is used by validstatfields-put-statfield-06, validstatfields-addclass-other,
addfuns/statfields-special is used by validstatfields-put-statfield-06, validstatfields-addclass, validstatfield-void, validstatfield-union, validstatfield-throw-predef, validstatfield-putrkvs, validstatfield-put-norefval, validstatfield-put-array-norefval, validstatfield-primtype-level, validstatfield-mode, validstatfield-addclass-same, validfieldlist-mode-01, initsubset-put-statfield-01, initsubset-initerror-04, initsubset-initerror-02,
addfuns/stsubset-addobj is used by validstatfield-addobj,
addfuns/validfieldinits-empty is used by validfieldinits-def-01, junkref-predefined,

Used from specification nat

nat/lels is used by junkrefs-addarray-noreftype, junkref-addarray-04, junkref-addarray-01,
nat/lels-01 is used by junkref-addarray-01,
nat/ler is used by junkref-addarray-01,
nat/ls-le-simp is used by junkref-addarray-01,

Used from specification nat-basic2

nat-basic2/a is used by validreflist-getarray-less-02, validreflist-getarray-less-01, junkref-putbar, junkref-primarray-level-01,
nat-basic2/c is used by validreflist-getarray-less-02, validreflist-getarray-less-01, junkref-putbar, junkref-primarray-level-01,
nat-basic2/s is used by validreflist-getarray-less-02, validreflist-getarray-less-01, junkref-putbar, junkref-primarray-level-01,

Used from specification set-union

set-union/references/int-empty-01 is used by validrefkeynotnull-statfield-intersect,
set-union/references/int-a is used by validref-union-left, junkrefs-union-disjoint, junkref-union-disjoint,
set-union/references/int-c is used by validref-union-left, junkrefs-union-disjoint, junkref-union-disjoint,
set-union/references/int-empty-02 is used by junkrefs-union-disjoint, junkref-union-disjoint,

Used from specification list-del

list-del/javavalues/get-in is used by junkrefs-addarray-noreftype, junkref-addarray-04,
list-del/javavalues/in-get is used by junkref-addarray-01,