[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 validrefs-putshort-field, validrefs-putbyte-field, validrefs-put-notin-03, validrefs-put-badclassfield-01, validrefs-put-badclassfield, validrefs-put-badarrayfield-01, validrefs-put-badarrayfield, validrefs-put-array-badindex, pathex-put-pathex-array-refval, pathex-put-nopathex, pathex-lookup-put-other, cyclic-put-statfield,
store/javastore/At-other-num is used by validrefs-putshort-field,
store/javastore/Subset is used by validrefs-subset, cyclic-subset,
store/javastore/subset-elem-eq-01 is used by validref-refs-last-valid-subset,
store/javastore/superset-elem-eq is used by validrefs-subset-equiv, validrefs-subset-01, cyclic-subset-01,
store/javastore/At-other is used by validrefs-putbyte-01, junkrefs-put-nopathex,
store/javastore/At-same is used by validrefs-set-null, validrefs-putshort-field, validrefs-putbyte-field, validrefs-putbyte-01, validrefs-put-notin-03, validrefs-put-badclassfield-01, validrefs-put-badclassfield, validrefs-put-array-badindex, pathex-put-pathex-array-refval, pathex-put-nopathex, pathex-put-cyclic, pathex-lookup-put-other, junkrefs-put-nopathex, cyclic-put-statfield-01, cyclic-put-statfield,
store/javastore/In-store is used by validrefs-lastelem, validrefs-all-same, validref-refs-last-valid-subset, exvalidrefs-nodups, exvalidrefs-maxlength, exvalidrefs-03, exvalidrefs,
store/javastore/notmemlookup is used by validrefs-subset-equiv, validrefs-subset-01, validrefs-subset, validrefs-putshort-field, validrefs-all-same, validref-refs-last-valid-subset, cyclic-subset-01, cyclic-subset,

Used from specification addarray

addarray/add-at-ok is used by cyclic-addrefarray, cyclic-addarray-this-01, cyclic-addarray-noreftype,
addarray/addarray-subset is used by cyclic-addarray-this-01,
addarray/at-1dim is used by cyclic-addarray-this,
addarray/is_array-addarray is used by cyclic-addarray-this,
addarray/is_array-other-addarray is used by validrefs-addarray-junkref, validrefs-addarray,
addarray/is_obj-addarray is used by validrefs-addarray-junkref, validrefs-addarray,
addarray/is_obj-addarray-01 is used by cyclic-addarray-this,
addarray/is_obj-addarray-02 is used by cyclic-addarray-this-01,
addarray/length-1dim is used by cyclic-addarray-this,
addarray/length-1init-01 is used by cyclic-addrefarray, cyclic-addarray-this-01, cyclic-addarray-noreftype,
addarray/lookup-1init is used by validrefs-addarray-junkref, validrefs-addarray, cyclic-addarray-other,
addarray/type-1dim is used by cyclic-addarray-this,
addarray/type-1init is used by cyclic-addrefarray, cyclic-addarray-this-01, cyclic-addarray-noreftype,

Used from specification list

Used from specification storefuns

storefuns/look-del is used by validrefs-delete, exvalidrefs-maxlength, cyclic-delete,
storefuns/del-notin-01 is used by validrefs-maxlen,
storefuns/instore-01 is used by validrefs-subset-equiv, validrefs-subset-01, validrefs-subset, validrefs-put-notin-01, validrefs-primarray, validrefs-lastelem, validrefs-applast-array-null, validrefs-all-same, validref-refs-last-valid-subset, exvalidrefs-nodups, exvalidrefs-maxlength, exvalidrefs-03, exvalidrefs, cyclic-subset-01, cyclic-addobj,
storefuns/look-del is used by validrefs-delete-03, validrefs-delete, validrefs-del-junkrefs, exvalidrefs-nodups, exvalidrefs-maxlength, exvalidrefs-03, exvalidrefs,
storefuns/newref-01 is used by validrefs-superset-junkref, validrefs-newref, validrefs-addobj-new, validrefs-addobj-junkref, validrefs-addobj-01, validrefs-addarray-junkref, validrefs-addarray, validref-nopath-superset, pathex-no-newref, pathex-addobj, cyclic-addrefarray, cyclic-addobj-other-01, cyclic-addobj-other, cyclic-addobj, cyclic-addarray-this-01, cyclic-addarray-this, cyclic-addarray-other,
storefuns/newref-del-01 is used by validrefs-del, exvalidrefs-maxlength,
storefuns/newref-in-03 is used by cyclic-addobj,

Used from specification int-basic2

int-basic2/add-c is used by pathex-putbar-03,

Used from specification valuefuns

valuefuns/okval-case is used by validrefs-all-same,
valuefuns/okval-reftype is used by validref-refs-last-valid-subset,
valuefuns/initial-value is used by cyclic-addarray-this,
valuefuns/intval-xtra is used by validrefs-lastelem, exvalidrefs-maxlength,
valuefuns/okprimtype-refval is used by cyclic-addarray-noreftype,
valuefuns/okval-class is used by exvalidrefs-nodups, exvalidrefs-03, exvalidrefs,
valuefuns/okval-reftype is used by validrefs-applast-array-null, exvalidrefs-maxlength,
valuefuns/okval-refval is used by validrefs-set-null, validrefs-primarray, validrefs-lastelem, validrefs-addobj-01, validref-refs-last-valid-subset, pathex-put-pathex-array-refval, pathex-put-cyclic,
valuefuns/okval-void is used by exvalidrefs-maxlength,
valuefuns/refval-xtra is used by validrefs-applast-array-null, validrefs-applast-array, exvalidrefs,
valuefuns/typeval-xtra is used by validrefs-all-same,

Used from specification setlist

setlist/references/dups-03 is used by validrefs-put-notin-03, pathex-put-pathex-array-refval, pathex-def-nodups,
setlist/references/in is used by validrefs-put-notin-03, pathex-put-pathex-array-refval,
setlist/references/list2set-empty is used by validrefs-put-notin-03, pathex-put-pathex-array-refval,
setlist/references/list2set-rec is used by validrefs-put-notin-03, pathex-put-pathex-array-refval,

Used from specification junkrefs

junkrefs/junkref-array is used by validrefs-subset-equiv, validrefs-subset-01, validrefs-subset, validrefs-putshort-field, validrefs-putbyte-field, validrefs-putbar-01, validrefs-put-last, validrefs-put-badclassfield-01, validrefs-put-badclassfield, validrefs-put-badarrayfield-01, validrefs-put-badarrayfield, validrefs-del-junkrefs, validrefs-addobj-junkref, validrefs-addarray-junkref, pathex-put-nopathex, junkref-update-equiv, exvalidrefs-maxlength,
junkrefs/junkref-class is used by validrefs-subset-equiv, validrefs-subset-01, validrefs-subset, validrefs-putshort-field, validrefs-putbyte-field, validrefs-putbar-01, validrefs-put-last, validrefs-put-badclassfield-01, validrefs-put-badclassfield, validrefs-put-badarrayfield-01, validrefs-put-badarrayfield, validrefs-del-junkrefs, validrefs-addobj-junkref, validrefs-addarray-junkref, junkref-update-equiv, exvalidrefs-nodups, exvalidrefs-maxlength, exvalidrefs-03,
junkrefs/junkref-class-01 is used by pathex-put-nopathex, exvalidrefs,
junkrefs/junkref-def is used by pathex-junkref, junkref-update-equiv, junkref-put-nopathexplus-equiv, junkref-put-nopathex-equiv-01, junkref-put-nopathex, exvalidrefs-nodups, exvalidrefs-maxlength, exvalidrefs-03, exvalidrefs,
junkrefs/junkref-is-junk is used by validrefs-subset-equiv, validrefs-subset-01, validrefs-subset, validrefs-putbyte-field, validrefs-put-badclassfield-01, validrefs-put-badclassfield, validrefs-put-badarrayfield-01, validrefs-put-badarrayfield, validrefs-del-junkrefs, junkref-update-equiv, exvalidrefs-nodups, exvalidrefs-maxlength, exvalidrefs-03, exvalidrefs,
junkrefs/junkref-put-badarrayfield is used by validrefs-put-badarrayfield-01,
junkrefs/junkref-put-badclassfield is used by validrefs-put-badclassfield-01,
junkrefs/junkref-putbar is used by pathex-putbar-03,
junkrefs/junkrefs-array is used by validrefs-junkrefs-append, validrefs-junkrefs-01, validrefs-junkrefs, validrefs-del-junkrefs, junkrefs-put-nopathexplus-equiv, junkrefs-put-nopathex-equiv, junkrefs-put-nopathex, junkref-update-equiv,
junkrefs/junkrefs-class is used by validrefs-junkrefs-append, validrefs-junkrefs-01, validrefs-junkrefs, validrefs-del-junkrefs, junkrefs-put-nopathexplus-equiv, junkrefs-put-nopathex-equiv, junkrefs-put-nopathex, junkref-update-equiv,
junkrefs/junkrefs-delete-01 is used by exvalidrefs-nodups, exvalidrefs-maxlength, exvalidrefs-03, exvalidrefs,
junkrefs/junkrefs-is-junk is used by validrefs-junkrefs-append, validrefs-junkrefs-01, junkrefs-put-nopathexplus-equiv, junkrefs-put-nopathex-equiv, junkrefs-put-nopathex,
junkrefs/junkrefs-null is used by validrefs-junkrefs, junkrefs-put-nopathexplus-equiv,
junkrefs/junkrefs-one is used by junkref-update-equiv,
junkrefs/junkrefs-sametype-01 is used by exvalidrefs-nodups, exvalidrefs-maxlength, exvalidrefs-03,
junkrefs/validref-array-rec is used by validrefs-levelsubset-01,
junkrefs/validref-class-rec is used by validrefs-levelsubset-01,
junkrefs/validref-def is used by validref-nopathex-put,
junkrefs/validref-forward-01 is used by validrefs-addobj-01, validref-refs-last-valid-subset,
junkrefs/validref-forward-array-01 is used by validref-refs-last-valid-subset,
junkrefs/validref-is-junk is used by validrefs-levelsubset-01, validrefs-addobj-01, validref-refs-last-valid-subset, pathex-levelsubset-01, pathex-addobj,
junkrefs/validref-newref is used by validrefs-addobj-01,
junkrefs/validref-runtimetype is used by validrefs-subset-equiv-01, validrefs-subset-equiv, pathex-subset-equiv, pathex-subset-02, pathex-levelsubset-equiv,
junkrefs/validref-type-forward is used by validref-refs-last-valid-subset,
junkrefs/validrefnotnull-def is used by validref-nopath-superset,
junkrefs/junkref-keyin is used by cyclic-subset-01, cyclic-subset,
junkrefs/junkref-newref is used by validrefs-addobj-junkref, validrefs-addarray-junkref, cyclic-addrefarray, cyclic-addobj, cyclic-addarray-this-01,
junkrefs/junkref-noreftype is used by pathex-put-nopathex,
junkrefs/junkref-not-valid-01 is used by validrefs-putshort-field, validrefs-putbyte-field, validrefs-putbar-01, validrefs-put-last, validrefs-put-badclassfield, validrefs-del-junkrefs, pathex-subset-equiv, pathex-putshortfield, pathex-putbyteval-01, pathex-putbyte-field, pathex-put-nopathex, pathex-put-last, exvalidrefs-maxlength, cyclic-put-nopathex,
junkrefs/junkref-null is used by validrefs-subset-equiv, validrefs-putshort-field, validrefs-putbyte-field, validrefs-putbar-01, validrefs-put-last, validrefs-put-badclassfield-01, validrefs-put-badclassfield, validrefs-put-badarrayfield-01, validrefs-put-badarrayfield, validrefs-addobj-junkref, validrefs-addarray-junkref, pathex-put-nopathex, exvalidrefs-maxlength, exvalidrefs, cyclic-addrefarray, cyclic-addobj,
junkrefs/junkref-voidarray is used by exvalidrefs-maxlength,
junkrefs/junkrefs-delete-02 is used by exvalidrefs,
junkrefs/junkrefs-empty is used by validrefs-junkrefs-01, validrefs-junkrefs,
junkrefs/junkrefs-junkref is used by junkref-put-nopathexplus-equiv, exvalidrefs-nodups, exvalidrefs-maxlength, exvalidrefs-03,
junkrefs/junkrefs-notin-03 is used by exvalidrefs-nodups, exvalidrefs-maxlength, exvalidrefs-03, exvalidrefs,
junkrefs/junkrefs-null-02 is used by validrefs-junkrefs-01, validrefs-del-junkrefs, junkrefs-put-nopathexplus-equiv, junkrefs-put-nopathex-equiv, junkrefs-put-nopathex, junkref-update-equiv,
junkrefs/junkrefs-runtimetype is used by validrefs-junkrefs-append, pathex-junkref,
junkrefs/junkrefs-sametype is used by exvalidrefs,
junkrefs/junkrefs-subtype is used by junkref-update-equiv, exvalidrefs,
junkrefs/levelsubset-is-array is used by validrefs-levelsubset,
junkrefs/levelsubset-is-obj is used by validrefs-levelsubset,
junkrefs/nojunkref-typeex is used by exvalidrefs,
junkrefs/validref-array-02 is used by validref-refs-last-valid-subset,
junkrefs/validref-array-len-in is used by validref-refs-last-valid-subset,
junkrefs/validref-junkref is used by validrefs-subset-equiv, pathex-subset, pathex-putbar-02,
junkrefs/validref-newref is used by validrefs-subset-notnew, validref-nopath-superset,
junkrefs/validref-null is used by validrefs-levelsubset-01, validrefs-addobj-01,
junkrefs/validrefnotnull-notnull is used by validref-nopath-superset, pathex-nopathex-diff,
junkrefs/validrefnotnull-validref is used by validrefs-subset-notnew,

Used from specification fieldspec

Used from specification intnat

intnat/num-i2n-le-02 is used by cyclic-addrefarray, cyclic-addarray-this-01, cyclic-addarray-noreftype,
intnat/num-n2i-ls-02 is used by cyclic-addrefarray, cyclic-addarray-this-01, cyclic-addarray-noreftype,

Used from specification int-abs

Used from specification okfuns

okfuns/gfts-all is used by validrefs-lastelem, validrefs-all-same, validrefs-addobj-01, validref-refs-last-valid-subset, exvalidrefs-nodups, exvalidrefs-maxlength, exvalidrefs-03, exvalidrefs,
okfuns/good-field-def is used by validrefs-all-same,
okfuns/is-any-array is used by validrefs-primarray, validrefs-lastelem, validrefs-applast-array-null, validrefs-all-same, validref-refs-last-valid-subset, exvalidrefs-maxlength,
okfuns/is-real-array-def is used by validrefs-primarray, validrefs-applast-array-null, validrefs-all-same, validref-refs-last-valid-subset,
okfuns/is_array-arraytype is used by validrefs-putbyte-field, validrefs-put-notin-03, validrefs-put-badclassfield-01, validrefs-put-badclassfield, validrefs-put-badarrayfield, validrefs-levelsubset-01,
okfuns/is_array-classtype is used by validrefs-subset-equiv,
okfuns/is_array-notin-01 is used by validrefs-subset-equiv, validrefs-subset,
okfuns/is_array-put-01 is used by validrefs-putbyte-01, pathex-put-nopathex, junkrefs-put-nopathex,
okfuns/is_array-put-field is used by validrefs-putshort-field,
okfuns/is_array-put-okval is used by pathex-put-pathex-array-refval,
okfuns/isarray-type is used by exvalidrefs-maxlength,
okfuns/keys-in is used by nopathex-update, cyclic-addobj,
okfuns/okarray-okarray-01 is used by okarray-put-nopath-01,
okfuns/okarray-put-other is used by okarray-put-nopath,
okfuns/okarrayNotNull is used by validrefs-primarray, validrefs-lastelem, validrefs-applast-array-null, validrefs-all-same, validref-refs-last-valid-subset, exvalidrefs-maxlength,
okfuns/okbar-putbar-05 is used by pathex-putbar,
okfuns/okbar-putbar-same is used by pathex-putbar-03, cyclic-putbar,
okfuns/okbytearray-01 is used by validrefs-putbar-01, validrefs-putbar, okbar-nopath,
okfuns/okreftype is used by validrefs-primarray, validrefs-all-same,
okfuns/update-ex-nodups is used by nopathex-update,
okfuns/update-put-notin is used by nopathex-update,
okfuns/update-rec is used by nopathex-update,
okfuns/update-rec-01 is used by junkref-update,
okfuns/validFields is used by validrefs-addobj-01,
okfuns/getkeys-app is used by nopathex-update,
okfuns/getkeys-empty is used by nopathex-update,
okfuns/getkeys-one is used by nopathex-update,
okfuns/getkeys-rec is used by nopathex-update,
okfuns/good-field-field is used by validrefs-all-same,
okfuns/good-field-field-01 is used by validrefs-lastelem, validrefs-all-same, validrefs-addobj-01, validref-refs-last-valid-subset, exvalidrefs-nodups, exvalidrefs-maxlength, exvalidrefs-03, exvalidrefs,
okfuns/good-field-index is used by validrefs-all-same,
okfuns/is_array-arraytype is used by validrefs-put-notin-03, validrefs-put-badclassfield, validrefs-put-badarrayfield-01, validrefs-put-badarrayfield, validrefs-all-same, pathexplus-pathex, junkrefs-put-nopathexplus-equiv,
okfuns/is_array-bytearray-01 is used by validrefs-bytearray,
okfuns/is_array-classtype is used by validrefs-subset-equiv, validrefs-putbyte-field, validrefs-put-badclassfield-01, validrefs-put-badarrayfield, validrefs-all-same, pathexplus-pathex, junkrefs-put-nopathexplus-equiv,
okfuns/is_array-del is used by validrefs-delete-03, validrefs-delete, validrefs-del-junkrefs,
okfuns/is_array-is-array is used by validrefs-lastelem, validrefs-junkrefs, exvalidrefs-maxlength,
okfuns/is_array-lenfield is used by validrefs-subset-equiv, validrefs-subset-01, validrefs-subset,
okfuns/is_array-length-07 is used by validrefs-primarray, validrefs-lastelem, exvalidrefs-maxlength,
okfuns/is_array-notin is used by validrefs-maxlen, exvalidrefs-maxlength,
okfuns/is_array-okarray is used by validrefs-putbar-01, okbar-nopath,
okfuns/is_array-okarray-01 is used by validrefs-primarray,
okfuns/is_array-okbytearray is used by validrefs-putbyte-01, validrefs-putbar, validrefs-bytearray,
okfuns/is_array-put-01 is used by validrefs-set-null, validrefs-putbyte-field, validrefs-putbyte-01, validrefs-putbyte, validrefs-put-notin-03, validrefs-put-notin, validrefs-put-last, validrefs-put-badclassfield-01, validrefs-put-badclassfield, pathex-put-nopathex, junkrefs-put-nopathexplus-equiv, junkrefs-put-nopathex-equiv, junkrefs-put-nopathex,
okfuns/is_array-put-byte is used by validrefs-putbyte-01, validrefs-putbyte,
okfuns/is_array-put-field is used by validrefs-put-notin-02, validrefs-put-notin-01, validrefs-put-badarrayfield-01, validrefs-put-badarrayfield,
okfuns/is_array-put-jvmref is used by validrefs-put-statfield,
okfuns/is_array-putbar-01 is used by validrefs-putbar-01, validrefs-putbar,
okfuns/is_array-subset is used by validrefs-subset-equiv, validrefs-subset-01, validrefs-subset,
okfuns/is_array-type-01 is used by validrefs-put-badclassfield-01, validrefs-put-badclassfield, exvalidrefs,
okfuns/is_array-type-02 is used by validrefs-subset-equiv, validrefs-subset-01, validrefs-subset,
okfuns/is_array-type-04 is used by pathex-put-cyclic,
okfuns/is_array-typeex is used by validrefs-not-in,
okfuns/is_array-typele is used by okbar-nopath, junkrefs-put-nopathexplus-equiv, exvalidrefs-nodups, exvalidrefs-03, cyclic-def-simple,
okfuns/is_array-update is used by junkref-update-equiv,
okfuns/isarray-bytearray is used by validrefs-bytearray,
okfuns/isarray-type-02 is used by validref-refs-last-valid-subset,
okfuns/keys-empty is used by validrefs-addobj-01, pathex-addobj,
okfuns/okarray-01 is used by okarray-put-nopath-01,
okfuns/okarray-04 is used by validrefs-primarray,
okfuns/okarray-05 is used by validrefs-putbar-01, validrefs-putbar, validrefs-primarray, validrefs-lastelem, validrefs-applast-array-null, validrefs-all-same, validref-refs-last-valid-subset, okarray-put-nopath-01, okarray-put-nopath, exvalidrefs-maxlength,
okfuns/okarray-jvmref-01 is used by okarray-put-nopath-01,
okfuns/okarray-refval is used by okarray-put-nopath-01,
okfuns/okarray-subset-01 is used by validref-refs-last-valid-subset,
okfuns/okarray-type-03 is used by validrefs-putbar-01,
okfuns/okbar-norefval is used by validrefs-putbyte-01, validrefs-putbyte, validrefs-bytearray, okbar-nopath,
okfuns/okbytearray-type is used by validrefs-putbyte-01, validrefs-putbar, validrefs-bytearray,
okfuns/oktype-class is used by pathex-put-cyclic,
okfuns/oktype-okval is used by validrefs-set-null, validrefs-put-notin-02, validrefs-put-notin-01, validrefs-primarray, validrefs-lastelem, validrefs-applast-array-null, validrefs-all-same, validref-refs-last-valid-subset, pathex-put-cyclic, exvalidrefs-maxlength, cyclic-addobj,
okfuns/oktype-short is used by validrefs-putshort-field,
okfuns/subset-okarray is used by validref-refs-last-valid-subset,
okfuns/update-at is used by junkref-update-equiv,
okfuns/update-empty is used by nopathex-update, junkref-update,
okfuns/update-length is used by junkref-update-equiv,
okfuns/update-type is used by junkref-update-equiv,

Used from specification storekey

storekey/elim-03 is used by validrefs-all-same,
storekey/elim-04 is used by pathex-put-pathex-array-refval,
storekey/inj-03 is used by validrefs-putshort-field, validrefs-putbyte-field, validrefs-put-badclassfield-01, validrefs-put-badclassfield, validrefs-put-badarrayfield-01,
storekey/inj-04 is used by validrefs-putbyte-01, validrefs-putbyte, validrefs-put-array-badindex, pathex-put-pathex-array-refval,
storekey/sel-05 is used by cyclic-addobj,
storekey/test is used by validrefs-all-same,
storekey/test-01 is used by validrefs-all-same,
storekey/test-05 is used by validrefs-all-same, cyclic-addobj,
storekey/test-08 is used by pathex-put-pathex-array-refval,

Used from specification typefuns

typefuns/classex-object is used by pathex-addobj,
typefuns/le-bigger is used by exvalidrefs-maxlength,
typefuns/le-noreftype is used by pathex-put-cyclic,
typefuns/le-noreftype-01 is used by validrefs-primarray, pathex-put-cyclic,
typefuns/array is used by validrefs-primarray, validrefs-all-same, validref-refs-last-valid-subset, pathex-put-pathex-array-refval, exvalidrefs-maxlength,
typefuns/bytearray is used by validrefs-bytearray,
typefuns/class-le is used by validrefs-put-badclassfield-01, validrefs-put-badclassfield, validrefs-lastelem, validrefs-all-same, validref-refs-last-valid-subset, pathex-put-cyclic, junkrefs-put-nopathexplus-equiv, exvalidrefs-nodups, exvalidrefs-03,
typefuns/classex-02 is used by pathex-addobj,
typefuns/elemtype-07 is used by validrefs-primarray, validrefs-all-same,
typefuns/elemtype-rec is used by validrefs-applast-array-null, validref-refs-last-valid-subset,
typefuns/is_primtype-01 is used by validrefs-primarray,
typefuns/is_primtype-02 is used by validrefs-primarray,
typefuns/is_primtype-03 is used by validrefs-primarray,
typefuns/isreftype-01 is used by validrefs-primtype-03, pathex-put-cyclic,
typefuns/isreftype-02 is used by validrefs-primtype-02,
typefuns/isreftype-03 is used by validrefs-primtype-01,
typefuns/isreftype-06 is used by validrefs-void,
typefuns/le-06 is used by validrefs-bytearray,
typefuns/le-08 is used by pathex-put-cyclic,
typefuns/le-11 is used by pathex-put-cyclic,
typefuns/le-noreftype is used by validrefs-primarray, validrefs-addobj-01,
typefuns/le-noreftype-01 is used by validrefs-primtype, validrefs-lastelem, validrefs-addobj-01, pathex-put-nopathex, pathex-put-cyclic,
typefuns/prim-abstract is used by validrefs-primarray,
typefuns/prim-void is used by validrefs-primarray,
typefuns/ref is used by validrefs-subtype, validrefs-sametype, validrefs-applast-class-null, validrefs-applast-class, validrefs-applast-array-null, validrefs-applast-array, validrefs-all-same, pathexplus-pathex, pathex-put-pathex-array-refval, pathex-put-nopathex, pathex-def-simple, pathex-class, pathex-array, junkref-update-equiv, exvalidrefs-nodups, exvalidrefs-maxlength, exvalidrefs-03, exvalidrefs, cyclic-one, cyclic-def-simple, cyclic-def-object, cyclic-class, cyclic-array, cyclic-addrefarray, cyclic-addarray-this-01, cyclic-addarray-this, cyclic-addarray-noreftype,
typefuns/subarray1 is used by validrefs-primarray, validrefs-bytearray, validrefs-all-same, pathex-put-pathex-array-refval, exvalidrefs-maxlength, cyclic-addrefarray, cyclic-addarray-this-01, cyclic-addarray-this, cyclic-addarray-noreftype,
typefuns/subbasic1 is used by junkrefs-put-nopathexplus-equiv,
typefuns/subbasic2 is used by pathex-validrefs-in,
typefuns/subclass is used by validrefs-addobj-01, pathexplus-pathex, pathex-put-cyclic, pathex-addobj, exvalidrefs-nodups, exvalidrefs-03, cyclic-addobj,
typefuns/subtype-object-01 is used by pathex-validrefs-in,
typefuns/transitivity is used by validrefs-superclass, validrefs-subtype, exvalidrefs-nodups, exvalidrefs-03, exvalidrefs,
typefuns/transitivity-01 is used by pathex-put-cyclic, exvalidrefs-nodups,
typefuns/typeex-array is used by validrefs-primarray, validrefs-applast-array-null, validrefs-all-same, validref-refs-last-valid-subset,

Used from specification pair

pair/fieldinit/elim is used by nopathex-update, junkref-update,

Used from specification classnamefuns

classnamefuns/le-reflexive is used by validrefs-addobj-01, pathexplus-pathex, pathex-put-cyclic, pathex-addobj, exvalidrefs-nodups, cyclic-addobj,
classnamefuns/le-transitive is used by exvalidrefs-nodups, exvalidrefs-03,

Used from specification nat-basic1

nat-basic1/f is used by validrefs-maxlen,
nat-basic1/one is used by validrefs-nodups-01, validrefs-nodups,
nat-basic1/ref-1 is used by validrefs-subset-equiv, validrefs-putbar-01, pathex-putbar-03, pathex-put-nopathex, junkrefs-put-nopathexplus-equiv, cyclic-def-shortest,
nat-basic1/z is used by cyclic-addrefarray, cyclic-addarray-this-01, cyclic-addarray-noreftype,

Used from specification list-set

list-set/references/subset is used by validrefs-nodups,
list-set/fieldinit-assoclista/subset is used by nopathex-update,
list-set/references/sub-in is used by validrefs-nodups,
list-set/references/subset-empty is used by validrefs-nodups,
list-set/references/subset-rec is used by validrefs-nodups,
list-set/references/subset-ref is used by validrefs-nodups,

Used from specification oelem

oelem/intlista/irreflexivity is used by validrefs-subset, validref-refs-last-valid-subset,
oelem/intlista/lel is used by validrefs-putbyte-01, validrefs-putbyte, validrefs-put-array-badindex, pathex-put-pathex-array-refval,
oelem/intlista/transitivity is used by validrefs-put-array-badindex,

Used from specification refkey

Used from specification javatype

Used from specification javavalue

Used from specification storearrays

storearrays/is_arrayref is used by validrefs-all-same, validref-refs-last-valid-subset,
storearrays/putBar-rec is used by pathex-putbar-03, pathex-putbar, cyclic-putbar,
storearrays/putByteArray-all is used by pathex-putbar-02, cyclic-putbar-05, cyclic-putbar-03, cyclic-putbar-02,
storearrays/putbar-refval is used by validrefs-putbar-01, validrefs-putbar,
storearrays/putBar-at-len is used by validrefs-putbar-01, validrefs-putbar,
storearrays/putBar-at-type is used by validrefs-putbar-01, validrefs-putbar,
storearrays/putBar-empty is used by pathex-putbar-03, pathex-putbar, cyclic-putbar,
storearrays/putbar-atfs-01 is used by validrefs-putbar-01, validrefs-putbar,
storearrays/putbar-atref-01 is used by validrefs-putbar-01, validrefs-putbar,

Used from specification list-dup

list-dup/references/dups is used by validrefs-nodups-01, validrefs-nodups,
list-dup/references/a is used by validrefs-put-notin-03, pathex-put-pathex-array-refval, pathex-def-nodups,
list-dup/storekeys/a is used by nopathex-update,
list-dup/references/c is used by pathex-put-cyclic, exvalidrefs-nodups, exvalidrefs-maxlength, exvalidrefs-03, exvalidrefs, cyclic-one, cyclic-addobj,
list-dup/references/c-02 is used by validrefs-nodups, pathex-def-nodups, exvalidrefs-nodups, cyclic-put-nopathex, cyclic-put-badclassfield,
list-dup/references/dups-cons is used by validrefs-set-null, validrefs-put-notin-03, validrefs-put-badclassfield-01, validrefs-put-badclassfield, validrefs-put-badarrayfield-01, validrefs-put-badarrayfield, validrefs-nodups, validrefs-maxlen, pathex-put-pathex-array-refval, pathex-put-last, pathex-put-cyclic, pathex-levelsubset-01, exvalidrefs-nodups, exvalidrefs-maxlength, exvalidrefs-03, exvalidrefs, cyclic-subset-01, cyclic-subset, cyclic-putbyte-01, cyclic-putbar-05, cyclic-putbar-04, cyclic-put-statfield-01, cyclic-put-statfield, cyclic-put-nopathex, cyclic-put-badclassfield, cyclic-one, cyclic-delete, cyclic-def-simple, cyclic-def-shortest, cyclic-def-object, cyclic-class, cyclic-array, cyclic-addrefarray, cyclic-addobj-other-01, cyclic-addobj-other, cyclic-addobj, cyclic-addarray-this-01, cyclic-addarray-other,
list-dup/storekeys/dups-cons is used by nopathex-update,
list-dup/references/e-01 is used by validrefs-set-null, validrefs-put-notin-03, validrefs-put-badclassfield, validrefs-nodups, pathex-put-pathex-array-refval, exvalidrefs-nodups, exvalidrefs-maxlength, exvalidrefs-03, exvalidrefs, cyclic-subset-01, cyclic-subset, cyclic-putbar-05, cyclic-putbar-04, cyclic-put-statfield-01, cyclic-put-statfield, cyclic-not-null, cyclic-delete, cyclic-def-simple, cyclic-def-shortest, cyclic-def-object, cyclic-class, cyclic-array, cyclic-addrefarray, cyclic-addobj-other-01, cyclic-addobj-other, cyclic-addobj, cyclic-addarray-this-01, cyclic-addarray-this, cyclic-addarray-other, cyclic-addarray-noreftype,
list-dup/storekeys/e-01 is used by nopathex-update,
list-dup/references/f is used by pathex-put-last, pathex-put-cyclic, exvalidrefs-nodups, exvalidrefs-maxlength, exvalidrefs-03, exvalidrefs, cyclic-putbyte-01, cyclic-def-shortest,
list-dup/references/f-01 is used by validrefs-put-notin-03, pathex-put-pathex-array-refval, pathex-def-nodups,
list-dup/storekeys/f-01 is used by nopathex-update,
list-dup/references/rec is used by validrefs-nodups, pathex-put-last, pathex-def-nodups, exvalidrefs-nodups, exvalidrefs-maxlength, exvalidrefs-03, exvalidrefs, cyclic-subset-01, cyclic-subset, cyclic-putbar-05, cyclic-putbar-04, cyclic-put-statfield-01, cyclic-put-statfield, cyclic-not-null, cyclic-delete, cyclic-def-simple, cyclic-def-shortest, cyclic-def-object, cyclic-class, cyclic-array, cyclic-addrefarray, cyclic-addobj-other-01, cyclic-addobj-other, cyclic-addobj, cyclic-addarray-this-01, cyclic-addarray-this, cyclic-addarray-other, cyclic-addarray-noreftype,

Used from specification list-data

Used from specification specialkeys

specialkeys/len is used by validrefs-put-notin-03,
specialkeys/length-02 is used by validrefs-putbyte-field, pathex-put-cyclic,
specialkeys/length-03 is used by pathex-put-cyclic,
specialkeys/length-diff is used by validrefs-putshort-field,
specialkeys/type-01 is used by pathex-put-cyclic,
specialkeys/type-03 is used by validrefs-put-notin-03, pathex-put-nopathex,
specialkeys/type-04 is used by pathex-put-nopathex, pathex-put-cyclic, junkrefs-put-nopathex,
specialkeys/type-05 is used by pathex-put-cyclic, cyclic-addobj,
specialkeys/type-08 is used by validrefs-putshort-field,
specialkeys/type-11 is used by pathex-put-cyclic,
specialkeys/type-neq is used by pathex-put-cyclic,

Used from specification storefunsx

storefunsx/refs-def is used by validrefs-maxlen, exvalidrefs-nodups, exvalidrefs-maxlength, exvalidrefs-03, exvalidrefs,
storefunsx/lookup-xtra is used by validrefs-subset-equiv, validrefs-subset-01, validrefs-subset, validrefs-putshort-field, validrefs-all-same, validref-refs-last-valid-subset, cyclic-subset-01, cyclic-subset,
storefunsx/refs-del is used by validrefs-maxlen, exvalidrefs-nodups, exvalidrefs-maxlength, exvalidrefs-03, exvalidrefs,

Used from specification javastore

Used from specification assoclist

assoclist/fieldinit/ex is used by nopathex-update,
assoclist/fieldinit/lookup-02 is used by validrefs-addobj-01,
assoclist/fieldinit/empty is used by nopathex-update, junkref-update,
assoclist/fieldinit/in-01 is used by validrefs-addobj-01, nopathex-update,
assoclist/fieldinit/in-append is used by nopathex-update, junkref-update,
assoclist/fieldinit/in-assoclist is used by cyclic-addobj,
assoclist/fieldinit/inone is used by nopathex-update, junkref-update,
assoclist/fieldinit/unique-02 is used by validrefs-addobj-01,

Used from specification predefined

predefined/le-01 is used by pathex-addobj,

Used from specification addfuns

addfuns/add-in-09 is used by validrefs-addobj-01,
addfuns/add-notin is used by cyclic-addobj,
addfuns/has_reffield-array is used by validrefs-lastelem, exvalidrefs-maxlength,
addfuns/has_reffield-class is used by validrefs-lastelem, exvalidrefs-maxlength,
addfuns/instfields-predef is used by validrefs-addobj-01,
addfuns/instfields-subclass-in is used by exvalidrefs-nodups, exvalidrefs-03,
addfuns/is-any-object is used by validrefs-lastelem, validrefs-addobj-01, validref-refs-last-valid-subset, exvalidrefs-nodups, exvalidrefs-maxlength, exvalidrefs-03, exvalidrefs,
addfuns/is-real-object-def is used by validrefs-addobj-01, validref-refs-last-valid-subset, pathex-addobj, exvalidrefs-nodups, exvalidrefs-03, exvalidrefs,
addfuns/is-valid-ref-stronger-def is used by validrefs-superclass, validrefs-subset-equiv, validrefs-subset-01, validrefs-subset, validrefs-set-null, validrefs-sametype, validrefs-put-statfield, validrefs-put-notin-02, validrefs-put-notin-01, validrefs-put-notin, validrefs-put-last, validrefs-put-badclassfield-01, validrefs-put-badclassfield, validrefs-put-badarrayfield-01, validrefs-put-badarrayfield, validrefs-put-array-badindex, validrefs-prefix, validrefs-postfix, validrefs-one, validrefs-not-in-01, validrefs-not-in, validrefs-newref, validrefs-maxlen, validrefs-levelsubset-01, validrefs-lastelem, validrefs-junkrefs-append, validrefs-junkrefs-01, validrefs-junkrefs, validrefs-has-null, validrefs-delete-03, validrefs-delete, validrefs-delcycle-01, validrefs-delcycle, validrefs-del-junkrefs, validrefs-contains-null, validrefs-append, validrefs-all-same, validrefs-addobj-notin, validrefs-addobj-junkref, validrefs-addobj, validrefs-addarray-junkref, validrefs-addarray, pathexplus-pathex, pathex-put-nopathex, junkrefs-put-nopathexplus-equiv, junkrefs-put-nopathex-equiv, junkrefs-put-nopathex, junkref-update-equiv, exvalidrefs-maxlength, cyclic-addrefarray, cyclic-addarray-this, cyclic-addarray-noreftype,
addfuns/is_array-addobj-01 is used by validrefs-addobj-01,
addfuns/is_obj-addobj-01 is used by validrefs-addobj-01,
addfuns/is_obj-arraytype is used by validrefs-put-notin-03, cyclic-addrefarray,
addfuns/is_obj-classtype is used by validrefs-subset-equiv, validrefs-putbyte-field, validrefs-put-badclassfield-01, validrefs-put-badclassfield, validrefs-put-badarrayfield, cyclic-addarray-noreftype,
addfuns/is_obj-def is used by validrefs-lastelem, validrefs-addobj-01, validref-refs-last-valid-subset, exvalidrefs-nodups, exvalidrefs-maxlength, exvalidrefs-03, exvalidrefs,
addfuns/is_obj-full-expand is used by validrefs-all-same,
addfuns/is_obj-notin-01 is used by validrefs-subset,
addfuns/is_obj-put-01 is used by validrefs-putshort-field, junkrefs-put-nopathex,
addfuns/is_obj-put-samefield is used by validrefs-putshort-field,
addfuns/is_obj-put-samefield-01 is used by validrefs-set-null, pathex-put-cyclic,
addfuns/is_obj-putbar is used by validrefs-putbar-01, validrefs-putbar,
addfuns/is_valid_ref-def is used by validrefs-put-notin-03,
addfuns/is_valid_ref-new is used by validref-nopath-superset,
addfuns/is_valid_ref-put-01 is used by validrefs-put-notin-02, validrefs-put-notin-01, pathex-put-nopathex, junkrefs-put-nopathex-equiv,
addfuns/is_valid_ref-put-samefield is used by validrefs-put-notin-01,
addfuns/is_valid_ref-put-samefield-01 is used by validrefs-put-notin-02,
addfuns/is_valid_ref-reftype is used by pathex-put-nopathex,
addfuns/isvalidref-put-array-badindex is used by validrefs-put-array-badindex,
addfuns/validfieldinits-all is used by cyclic-addobj,
addfuns/add-in-06 is used by validrefs-addobj-01,
addfuns/add-in-09 is used by cyclic-addobj,
addfuns/add-new-01 is used by validrefs-addobj-01,
addfuns/add-ref is used by validrefs-addobj-notin, validrefs-addobj-junkref, validrefs-addobj-01, validrefs-addobj, cyclic-addobj-other-01, cyclic-addobj-other,
addfuns/add-type is used by validrefs-addobj-01, pathex-addobj, cyclic-addobj,
addfuns/add-type-02 is used by validrefs-addobj-01,
addfuns/add-type-04 is used by validrefs-addobj-01,
addfuns/instfields-Object is used by pathex-addobj, exvalidrefs-nodups, exvalidrefs-03,
addfuns/instfields-predef is used by pathex-addobj,
addfuns/instfields-special is used by validrefs-lastelem, validrefs-addobj-01, validref-refs-last-valid-subset,
addfuns/instfields-subclass is used by exvalidrefs-nodups, exvalidrefs-03,
addfuns/instfields-type is used by validrefs-addobj-01, pathex-addobj, cyclic-addobj,
addfuns/instfields-type-01 is used by validrefs-set-null, pathex-put-cyclic,
addfuns/is_array-addobj is used by validrefs-addobj-notin, validrefs-addobj-junkref, validrefs-addobj,
addfuns/is_array-validref is used by validrefs-not-in,
addfuns/is_obj-01 is used by validrefs-lastelem, validrefs-junkrefs, exvalidrefs-maxlength,
addfuns/is_obj-addobj is used by validrefs-addobj-notin, validrefs-addobj-junkref, validrefs-addobj,
addfuns/is_obj-arraytype is used by validrefs-putbyte-field, validrefs-put-notin-03, validrefs-put-badclassfield-01, validrefs-put-badarrayfield-01, validrefs-put-badarrayfield, validrefs-levelsubset-01,
addfuns/is_obj-classtype is used by validrefs-all-same, pathexplus-pathex, pathex-validrefs-in, junkrefs-put-nopathexplus-equiv, exvalidrefs-nodups, exvalidrefs-maxlength, exvalidrefs-03,
addfuns/is_obj-del is used by validrefs-delete-03, validrefs-delete, validrefs-del-junkrefs, exvalidrefs-nodups, exvalidrefs-03, exvalidrefs,
addfuns/is_obj-isarray is used by validrefs-type, validrefs-subset-equiv, validrefs-putbyte-field, validrefs-putbyte, validrefs-put-notin-03, validrefs-put-badclassfield, validrefs-put-badarrayfield-01, validrefs-levelsubset-01, validrefs-levelsubset,
addfuns/is_obj-notin is used by validrefs-maxlen, exvalidrefs-nodups, exvalidrefs-03, exvalidrefs,
addfuns/is_obj-notin-01 is used by validrefs-subset-equiv,
addfuns/is_obj-null is used by cyclic-def-simple, cyclic-def-object,
addfuns/is_obj-put-01 is used by validrefs-set-null, validrefs-putbyte-field, validrefs-put-notin-03, validrefs-put-notin-02, validrefs-put-notin-01, validrefs-put-notin, validrefs-put-last, validrefs-put-badarrayfield-01, pathex-put-nopathex, junkrefs-put-nopathexplus-equiv, junkrefs-put-nopathex-equiv, junkrefs-put-nopathex,
addfuns/is_obj-put-index is used by validrefs-putbyte-01, validrefs-putbyte, validrefs-put-array-badindex, pathex-put-pathex-array-refval,
addfuns/is_obj-put-statfield is used by validrefs-put-statfield,
addfuns/is_obj-reftype is used by exvalidrefs,
addfuns/is_obj-subset is used by validrefs-subset-equiv, validrefs-subset-01, validrefs-subset,
addfuns/is_obj-type is used by validrefs-subset-equiv, validrefs-subset-01, validrefs-subset,
addfuns/is_obj-type-02 is used by pathex-put-pathex-array-refval,
addfuns/is_obj-typeex is used by validrefs-not-in,
addfuns/is_obj-typele is used by junkrefs-put-nopathexplus-equiv, cyclic-def-object,
addfuns/is_obj-update is used by junkref-update-equiv,
addfuns/is_obj-validref is used by validrefs-not-in,
addfuns/is_valid_ref is used by validrefs-trans-01, validrefs-subtype, validrefs-subset-equiv, validrefs-putshort-field, validrefs-putbyte-field, validrefs-putbyte-01, validrefs-putbar-01, validrefs-putbar, validrefs-put-notin-03, validrefs-levelsubset-01, validrefs-addobj-01, validref-refs-last-valid-subset, pathex-put-cyclic, exvalidrefs-nodups, exvalidrefs-03, exvalidrefs, cyclic-def-simple,
addfuns/is_valid_ref-01 is used by validrefs-type, validrefs-subset-equiv, validrefs-putbyte-field, validrefs-putbyte-01, validrefs-putbyte, validrefs-put-notin-03, validrefs-put-array-badindex, validrefs-levelsubset-01, validrefs-levelsubset, pathex-put-pathex-array-refval, cyclic-addarray-this-01,
addfuns/is_valid_ref-03 is used by pathex-not-is-validref,
addfuns/is_valid_ref-addobj is used by validrefs-addobj-junkref, validrefs-addobj-01, validrefs-addobj,
addfuns/is_valid_ref-array is used by validrefs-bytearray, pathex-put-pathex-array-refval, exvalidrefs-maxlength,
addfuns/is_valid_ref-array-01 is used by validrefs-primarray, validref-refs-last-valid-subset,
addfuns/is_valid_ref-del is used by validrefs-delete-02,
addfuns/is_valid_ref-del-01 is used by validrefs-delete,
addfuns/is_valid_ref-field-in is used by validref-refs-last-valid-subset,
addfuns/is_valid_ref-isarray is used by validrefs-type, validrefs-subset-equiv, validrefs-subset-01, validrefs-putbyte-01, validrefs-putbyte, validrefs-put-notin-03, validrefs-put-array-badindex, validrefs-levelsubset-01, validrefs-levelsubset, validrefs-junkrefs-01, validrefs-junkrefs, pathex-put-pathex-array-refval, pathex-put-nopathex, junkrefs-put-nopathexplus-equiv, junkrefs-put-nopathex, cyclic-addarray-this-01,
addfuns/is_valid_ref-isobj is used by validrefs-type, validrefs-trans-01, validrefs-subtype, validrefs-subset-equiv, validrefs-subset-01, validrefs-putshort-field, validrefs-putbyte-field, validrefs-putbyte-01, validrefs-putbar-01, validrefs-putbar, validrefs-put-notin-03, validrefs-levelsubset-01, validrefs-junkrefs-01, validrefs-junkrefs, validrefs-addobj-01, validref-refs-last-valid-subset, pathex-put-nopathex, pathex-put-cyclic, junkrefs-put-nopathexplus-equiv, junkrefs-put-nopathex, exvalidrefs-nodups, exvalidrefs-maxlength, exvalidrefs-03, exvalidrefs, cyclic-one, cyclic-def-object, cyclic-addobj,
addfuns/is_valid_ref-new is used by validrefs-newref, validrefs-addobj-01,
addfuns/is_valid_ref-no-arraytype is used by pathex-validrefs-in,
addfuns/is_valid_ref-notin-01 is used by validrefs-subset-equiv, validref-refs-last-valid-subset,
addfuns/is_valid_ref-null is used by validrefs-put-notin-03, validrefs-applast-array, pathexplus-pathex,
addfuns/is_valid_ref-obj is used by pathex-addobj,
addfuns/is_valid_ref-okbytearray is used by validrefs-bytearray,
addfuns/is_valid_ref-put-01 is used by validrefs-put-statfield, validrefs-put-notin-03, validrefs-put-notin-01, validrefs-put-notin, validrefs-put-last, pathex-putstatfield, pathex-put-nopathex, junkrefs-put-nopathexplus-equiv,
addfuns/is_valid_ref-put-byte is used by validrefs-putbyte,
addfuns/is_valid_ref-put-index is used by validrefs-putbyte-01, validrefs-putbyte, validrefs-put-array-badindex,
addfuns/is_valid_ref-reftype is used by validrefs-primtype, validrefs-lastelem, validrefs-addobj-01, pathex-put-nopathex, pathex-put-cyclic,
addfuns/is_valid_ref-type is used by validref-nopath-superset, pathexplus-pathex, pathex-one, pathex-def-simple,
addfuns/is_valid_ref-typeval-01 is used by validrefs-addobj-01,
addfuns/is_valid_ref-update is used by junkref-update-equiv,
addfuns/isarray-isobj is used by validrefs-junkrefs,
addfuns/isarray-isobj-01 is used by validrefs-trans-01, validrefs-subtype, validrefs-subset-equiv, validrefs-set-null, validrefs-putshort-field, validrefs-putbyte-field, validrefs-putbyte-01, validrefs-putbar-01, validrefs-putbar, validrefs-put-notin-03, validrefs-put-badclassfield, validrefs-put-array-badindex, validrefs-levelsubset-01, validrefs-addobj-01, validref-refs-last-valid-subset, exvalidrefs-nodups, exvalidrefs-maxlength, exvalidrefs-03, exvalidrefs, cyclic-def-simple,
addfuns/isobj-array-01 is used by validrefs-junkrefs,
addfuns/isobj-arraytype is used by validref-refs-last-valid-subset,
addfuns/isobj-arraytype-02 is used by validref-refs-last-valid-subset,
addfuns/isobj-classtype is used by exvalidrefs-maxlength,
addfuns/isobj-instfields is used by validrefs-lastelem, validref-refs-last-valid-subset, exvalidrefs-maxlength, exvalidrefs,
addfuns/isobj-isarray is used by validrefs-junkrefs,
addfuns/isobj-notin-05 is used by exvalidrefs-maxlength,
addfuns/reffield-del is used by exvalidrefs-maxlength,
addfuns/reffield-null is used by exvalidrefs-maxlength,
addfuns/validref-new is used by pathex-no-newref,

Used from specification nat

nat/add-num-03 is used by validrefs-nodups-01, validrefs-nodups,
nat/anti is used by validrefs-maxlen,
nat/l-num-03 is used by validrefs-nodups,
nat/lels is used by validrefs-maxlen, exvalidrefs-nodups, exvalidrefs-maxlength, exvalidrefs-03, exvalidrefs, cyclic-addrefarray, cyclic-addarray-this-01, cyclic-addarray-noreftype,
nat/lels-01 is used by validrefs-maxlen,
nat/lep-02 is used by validrefs-maxlen,
nat/ler is used by validrefs-maxlen,
nat/let is used by validrefs-maxlen,

Used from specification list-last

list-last/references/l-02 is used by pathex-put-pathex-array-refval, exvalidrefs-maxlength,
list-last/references/b is used by validrefs-put-badclassfield,
list-last/references/bapp is used by validrefs-put-badclassfield-01, validrefs-put-badarrayfield-01, validrefs-put-badarrayfield, pathexplus-pathex,
list-last/references/bin is used by validrefs-put-badclassfield,
list-last/references/bl is used by pathexplus-pathex,
list-last/references/butlast-def is used by cyclic-put-badclassfield, cyclic-put-badarrayfield,
list-last/references/butlast-last is used by validref-nopath-superset, cyclic-def-shortest,
list-last/references/l is used by validrefs-trans-01, validrefs-set-null, validrefs-nodups, validrefs-lastelem, validrefs-junkrefs-append, validrefs-junkrefs, validref-nopath-superset, pathexplus-pathex, pathex-trans, pathex-subset-equiv, pathex-putstatfield, pathex-putshortfield, pathex-putbyteval-01, pathex-putbyte-field, pathex-put-pathex-array-refval, pathex-put-nopathex, pathex-put-cyclic, pathex-one, pathex-null, pathex-not-is-validref, pathex-noreftype, pathex-levelsubset-01, pathex-junkref, pathex-def-nodups, pathex-class, pathex-array, okbar-nopath, junkrefs-put-nopathexplus-equiv, exvalidrefs-nodups, exvalidrefs-maxlength, exvalidrefs-03, exvalidrefs,
list-last/references/l-02 is used by validrefs-trans-01, validrefs-set-null, validrefs-nodups, validrefs-lastelem, validrefs-junkrefs-append, validrefs-junkrefs, validref-nopath-superset, pathexplus-pathex, pathex-trans, pathex-subset-equiv, pathex-putstatfield, pathex-putshortfield, pathex-putbyteval-01, pathex-putbyte-field, pathex-put-pathex-array-refval, pathex-put-nopathex, pathex-put-cyclic, pathex-not-is-validref, pathex-noreftype, pathex-levelsubset-01, pathex-junkref, pathex-def-nodups, pathex-class, pathex-array, okbar-nopath, exvalidrefs-nodups, exvalidrefs-03, exvalidrefs,
list-last/references/l-05 is used by pathex-put-pathex-array-refval, pathex-array, pathex-addobj, junkrefs-put-nopathexplus-equiv, exvalidrefs-nodups, exvalidrefs-maxlength, exvalidrefs-03, exvalidrefs,
list-last/references/l-in is used by validrefs-junkrefs, pathex-put-pathex-array-refval,
list-last/references/lapp is used by validrefs-nodups, pathex-trans,
list-last/references/lapp-01 is used by validrefs-nodups-01, validrefs-nodups, pathex-put-pathex-array-refval, pathex-def-nodups,
list-last/references/lapp-04 is used by validrefs-put-last, pathex-put-last,
list-last/references/last-01 is used by validrefs-nopathex, pathex-validrefs-in, pathex-put-last, exvalidrefs-maxlength,
list-last/references/last-def is used by validrefs-applast-class-null, validrefs-applast-class, validrefs-applast-array-null, validrefs-applast-array, pathex-class, pathex-array, exvalidrefs-nodups, exvalidrefs-maxlength, exvalidrefs-03, exvalidrefs,
list-last/references/last-elim is used by validrefs-append-01, pathexplus-pathex, pathex-put-last, pathex-put-cyclic, pathex-noreftype, exvalidrefs-maxlength, cyclic-def-shortest,
list-last/references/lin-01 is used by validrefs-set-null, validrefs-put-last, pathex-put-pathex-array-refval, pathex-put-last, pathex-not-is-validref-01, pathex-not-is-validref,
list-last/references/lin-02 is used by validrefs-set-null,

Used from specification nat-basic2

Used from specification set-union

set-union/references/del-in is used by validrefs-maxlen,
set-union/references/int-a is used by validrefs-put-notin-03, pathex-put-pathex-array-refval,
set-union/references/int-c is used by validrefs-put-notin-03, pathex-put-pathex-array-refval,
set-union/references/int-e is used by validrefs-put-notin-03, pathex-put-pathex-array-refval,
set-union/references/int-ins is used by validrefs-put-notin-03, pathex-put-pathex-array-refval,
set-union/references/size-del-leq is used by validrefs-maxlen, exvalidrefs-nodups, exvalidrefs-maxlength, exvalidrefs-03, exvalidrefs,

Used from specification list-del

list-del/javavalues/get-in is used by cyclic-addrefarray, cyclic-addarray-this-01, cyclic-addarray-noreftype,