[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 unchNorec-put-nopathex,
store/javastore/Subset is used by pseq-subset,
store/javastore/At-same is used by unchNorec-put-nopathex,
store/javastore/In-store is used by unchNorec-isobj, maxpath-object,
store/javastore/notmemlookup is used by validref-pseq, unchNorec-isobj, unchNorec-isarray, pseq-subset, getbytearray-pseq-nojunk,

Used from specification cyclic

cyclic/cyclic-array is used by pseq-sym-01, pseq-subset, cyclic-pseq,
cyclic/cyclic-class is used by pseq-sym-01, pseq-subset, cyclic-pseq,
cyclic/cyclic-def-shortest is used by cyclic-pseq,
cyclic/cyclic-def-simple is used by unchanged-cyclic, maxpath-object, maxpath-array, cyclic-pseq,
cyclic/cyclic-one is used by cyclic-pseq,
cyclic/cyclic-subset is used by pseq-subset-01,
cyclic/exvalidrefs-maxlength is used by maxpath-object, maxpath-array,
cyclic/pathex-array is used by unchanged-junkrefs-level, unchanged-array-forward,
cyclic/pathex-class is used by unchanged-junkrefs-level, unchanged-class-forward,
cyclic/pathex-def is used by unchanged-pathex-append, unchanged-pathex, unchNorec-validrefs-pathex,
cyclic/pathex-junkref is used by unchanged-put-nopathex,
cyclic/pathex-levelsubset-equiv is used by unchanged-levelsubset-equiv, unchanged-levelsubset,
cyclic/pathex-not-is-validref is used by unchanged-lookup-generic,
cyclic/pathex-one is used by unchanged-type-in,
cyclic/pathex-put-nopathex is used by unchanged-put-nopathex,
cyclic/pathex-trans is used by unchanged-put-nopathex, unchanged-pathex-unchanged,
cyclic/pathex-validrefs-in is used by unchanged-validrefs-unchNorec, unchanged-pathex,
cyclic/validrefs-append-01 is used by unchanged-pathex-append,
cyclic/validrefs-applast-array is used by cyclic-pseq,
cyclic/validrefs-applast-class is used by cyclic-pseq,
cyclic/validrefs-array is used by unchNorec-validrefs, maxpath-array, cyclic-pseq,
cyclic/validrefs-class is used by unchNorec-validrefs, maxpath-object, cyclic-pseq,
cyclic/validrefs-is-junk is used by unchNorec-validrefs-pathex, unchNorec-validrefs, cyclic-pseq,
cyclic/validrefs-one is used by cyclic-pseq,
cyclic/validrefs-prefix is used by unchNorec-validrefs-pathex,
cyclic/validrefs-primtype is used by cyclic-pseq,
cyclic/validrefs-sametype is used by cyclic-pseq,
cyclic/validrefs-superclass is used by unchNorec-validrefs-pathex, maxpath-object, maxpath-array,
cyclic/cyclic-not-null is used by pseq-sym-01, pseq-subset, cyclic-pseq,
cyclic/pathex-not-is-validref-01 is used by unchanged-junkrefs-level,
cyclic/pathex-not-is-validref-02 is used by unchanged-junkrefs-level,
cyclic/pathex-null-01 is used by unchanged-type-in, unchanged-null,
cyclic/pathex-one is used by unchanged-validrefs-unchNorec, unchanged-unchNorec-same-01, unchanged-unchNorec-same, unchanged-type-in, unchanged-type, unchanged-pathex, unchanged-junkrefs-level, unchanged-isobj, unchanged-isarray, unchanged-getbar, unchanged-class-forward, unchanged-array-forward, unchNorec-validrefs-pathex, unchNorec-put-nopathex,
cyclic/validrefs-empty is used by unchNorec-validrefs,
cyclic/validrefs-not is used by unchanged-validrefs-unchNorec, unchanged-pathex, maxpath-object, maxpath-array, cyclic-pseq,
cyclic/validrefs-null-02 is used by unchNorec-validrefs-pathex, unchNorec-validrefs, maxpath-array, cyclic-pseq,
cyclic/validrefs-sametype is used by unchanged-cyclic,

Used from specification list

list/references/In is used by unchNorec-validrefs-pathex,
list/bytelist/c-02 is used by getbytearray-pseq-nojunk-02, getbytearray-pseq-02,
list/references/Last is used by cyclic-pseq,
list/references/Nil is used by cyclic-pseq,
list/bytelist/Nil is used by getbytearray-pseq-nojunk-02, getbytearray-pseq-02,
list/references/a is used by unchanged-validrefs-unchNorec, unchanged-pathex-append, unchanged-pathex, unchanged-junkrefs-level, unchanged-junkrefs, unchanged-junkref-level, unchanged-junkref, unchanged-cyclic, unchNorec-validrefs-pathex, unchNorec-validrefs, unchNorec-junkrefs, maxpath-object, maxpath-array, cyclic-pseq,
list/bytelist/a is used by getbytearray-pseq-nojunk-02, getbytearray-pseq-02,
list/references/app is used by maxpath-object,
list/references/app-02-ant is used by unchanged-pathex-append, unchanged-junkref-level, unchanged-junkref, unchNorec-validrefs-pathex, maxpath-object, maxpath-array, cyclic-pseq,
list/bytelist/c is used by getbytearray-pseq-nojunk-02, getbytearray-pseq-02,
list/references/c is used by unchanged-validrefs-unchNorec, unchanged-pathex-append, unchanged-pathex, unchanged-junkrefs-level, unchanged-junkrefs, unchanged-junkref-level, unchanged-junkref, unchanged-cyclic, unchNorec-validrefs-pathex, unchNorec-validrefs, unchNorec-junkrefs, maxpath-object, maxpath-array, cyclic-pseq,
list/references/c-03 is used by cyclic-pseq,
list/references/c-05 is used by cyclic-pseq,
list/references/c-07 is used by unchanged-pathex-append,
list/references/c-08 is used by unchanged-pathex-append, unchanged-junkrefs-level, unchanged-junkrefs, unchanged-junkref-level, unchanged-junkref, unchanged-cyclic, unchNorec-validrefs-pathex, maxpath-object, maxpath-array, cyclic-pseq,
list/bytelist/e is used by getbytearray-pseq-nojunk-02, getbytearray-pseq-02,
list/references/e is used by unchanged-pathex-append, unchanged-junkref-level, unchanged-junkref, unchNorec-validrefs-pathex, maxpath-object, maxpath-array, getbytearray-pseq-nojunk-02, getbytearray-pseq-02, cyclic-pseq,
list/references/e-01 is used by unchanged-validrefs-unchNorec, unchanged-pathex-append, unchanged-pathex, unchanged-junkrefs-level, unchanged-junkrefs, unchanged-junkref-level, unchanged-junkref, unchanged-cyclic, unchNorec-validrefs-pathex, unchNorec-validrefs, unchNorec-junkrefs, maxpath-object, maxpath-array, cyclic-pseq,
list/references/e-02 is used by maxpath-object,
list/bytelist/first is used by getbytearray-pseq-nojunk-02, getbytearray-pseq-02,
list/references/first is used by getbytearray-pseq-nojunk-02, getbytearray-pseq-02, cyclic-pseq,
list/references/first-01 is used by cyclic-pseq,
list/references/first-app is used by cyclic-pseq,
list/references/in-01 is used by cyclic-pseq,
list/references/in-06 is used by unchanged-pathex-append, unchanged-cyclic, unchNorec-validrefs-pathex, unchNorec-validrefs, unchNorec-junkrefs, maxpath-object, maxpath-array, cyclic-pseq,
list/references/in-17 is used by unchanged-validrefs-unchNorec, unchanged-pathex-append, unchanged-pathex, unchanged-cyclic, unchNorec-validrefs-pathex, unchNorec-validrefs, unchNorec-junkrefs, maxpath-object, maxpath-array, cyclic-pseq,
list/references/in-append is used by unchanged-validrefs-unchNorec, unchanged-pathex-append, unchanged-pathex, unchanged-cyclic, unchNorec-validrefs-pathex, unchNorec-validrefs, unchNorec-junkrefs, maxpath-object, maxpath-array, cyclic-pseq,
list/references/in-empty is used by unchanged-validrefs-unchNorec, maxpath-object, cyclic-pseq,
list/references/len is used by maxpath-object, maxpath-array,
list/references/len-02 is used by maxpath-object, maxpath-array,
list/bytelist/rest is used by getbytearray-pseq-nojunk-02, getbytearray-pseq-02,

Used from specification storefuns

storefuns/instore-01 is used by validref-pseq, unchNorec-isobj, unchNorec-isarray, pseq-subset, maxpath-object, getbytearray-pseq-nojunk-02, getbytearray-pseq-nojunk, getbytearray-pseq-02, getbytearray-pseq,

Used from specification int-basic2

int-basic2/add-a is used by getbytearray-pseq-nojunk-02, getbytearray-pseq-nojunk, getbytearray-pseq-02, getbytearray-pseq,
int-basic2/add-c is used by getbytearray-pseq-nojunk-02, getbytearray-pseq-nojunk, getbytearray-pseq-02, getbytearray-pseq,
int-basic2/ax-04 is used by getbytearray-pseq-nojunk-02, getbytearray-pseq-nojunk, getbytearray-pseq-02, getbytearray-pseq,
int-basic2/ls-02 is used by getbytearray-pseq-nojunk-02, getbytearray-pseq-02,

Used from specification valuefuns

valuefuns/okval-noval is used by unchNorec-isobj, unchNorec-isarray,
valuefuns/okval-refval is used by maxpath-object,
valuefuns/refval-xtra is used by pseq-sym-01, pseq-subset, cyclic-pseq,
valuefuns/typeval-xtra is used by getbytearray-pseq-nojunk,

Used from specification junkrefs

junkrefs/is_valid_ref-levelsubset is used by unchanged-junkrefs-level,
junkrefs/junkref-array is used by unchanged-rec-generic, pseq-sym-01, pseq-subset, maxpath-array, cyclic-pseq,
junkrefs/junkref-class is used by unchanged-rec-generic, pseq-sym-01, pseq-subset, maxpath-object, cyclic-pseq,
junkrefs/junkref-def is used by unchanged-junkref-level, unchanged-junkref, getbytearray-pseq-nojunk-02, getbytearray-pseq-02,
junkrefs/junkref-is-junk is used by unchanged-rec-generic, unchNorec-put-nopathex, pseq-sym-01, pseq-subset, cyclic-pseq,
junkrefs/junkref-subset is used by pseq-subset-01,
junkrefs/junkrefs-array is used by unchanged-junkrefs-level, unchanged-junkrefs, unchNorec-junkrefs,
junkrefs/junkrefs-class is used by unchanged-junkrefs-level, unchanged-junkrefs, unchNorec-junkrefs,
junkrefs/junkrefs-is-junk is used by unchanged-junkrefs-level, unchanged-junkrefs, unchanged-junkref, unchNorec-junkrefs,
junkrefs/junkrefs-one is used by getbytearray-pseq-nojunk-02, getbytearray-pseq-02,
junkrefs/validref-def is used by unchanged-validref,
junkrefs/validref-okreftype is used by validref-pseq, getbytearray-pseq-nojunk, getbytearray-pseq-02, getbytearray-pseq,
junkrefs/junkref-bad-type is used by unchanged-rec-generic,
junkrefs/junkref-keyin is used by validref-pseq, pseq-subset, getbytearray-pseq-nojunk,
junkrefs/junkref-not-valid-01 is used by unchanged-validref, unchanged-rec-generic, unchNorec-put-nopathex,
junkrefs/junkref-null is used by pseq-sym-01, pseq-subset, cyclic-pseq,
junkrefs/junkrefs-empty is used by unchanged-junkrefs-level, unchanged-junkrefs, unchNorec-junkrefs,
junkrefs/junkrefs-null-02 is used by unchanged-junkrefs-level, unchanged-junkrefs, unchanged-junkref, unchNorec-junkrefs,
junkrefs/junkrefs-runtimetype is used by unchanged-junkref-level,
junkrefs/junkrefs-sametype is used by unchanged-junkref,
junkrefs/levelsubset-is-array is used by unchanged-junkrefs-level,
junkrefs/levelsubset-is-obj is used by unchanged-junkrefs-level,
junkrefs/okbytearray-validref is used by unchanged-okbar,

Used from specification fieldspec

fieldspec/elim is used by unchanged-rec-generic, unchanged-junkrefs-level, unchanged-class-forward, unchNorec-validrefs, unchNorec-junkrefs, unchNorec-isobj, maxpath-object,
fieldspec/sel-03 is used by unchanged-rec-generic, unchanged-junkrefs-level, unchanged-class-forward, unchNorec-validrefs, unchNorec-junkrefs, maxpath-object,

Used from specification intnat

intnat/labs is used by getbytearray-pseq-nojunk-02, getbytearray-pseq-02,

Used from specification int-abs

int-abs/abs is used by getbytearray-pseq-nojunk-02, getbytearray-pseq-02,
int-abs/abs-09 is used by getbytearray-pseq-nojunk-02, getbytearray-pseq-02,
int-abs/abs-16 is used by getbytearray-pseq-nojunk-02, getbytearray-pseq-02,
int-abs/anti is used by getbytearray-pseq-nojunk-02, getbytearray-pseq-nojunk, getbytearray-pseq-02, getbytearray-pseq,
int-abs/bet is used by getbytearray-pseq-nojunk-02, getbytearray-pseq-02,
int-abs/bet-01 is used by getbytearray-pseq-nojunk-02, getbytearray-pseq-02,
int-abs/elim-sub is used by getbytearray-pseq-nojunk-02, getbytearray-pseq-02,
int-abs/forward-le is used by unchNorec-index0, pseq-subset, getbytearray-pseq-nojunk-02, getbytearray-pseq-02,
int-abs/forward-le-01 is used by unchanged-rec-generic, unchanged-lookup-generic, unchanged-junkrefs-level, unchanged-junkrefs, unchanged-getbar, unchanged-array-forward, unchNorec-validrefs, unchNorec-transitivity, unchNorec-sym, unchNorec-junkrefs, unchNorec-isarray, unchNorec-index0, unchNorec-index, unchNorec-def-keep, pseq-sym-01, pseq-subset, maxpath-array-ls, maxpath-array, getbytearray-pseq-nojunk-02, getbytearray-pseq-nojunk, getbytearray-pseq-02, getbytearray-pseq, cyclic-pseq,
int-abs/forward-le-02 is used by getbytearray-pseq-nojunk, getbytearray-pseq,
int-abs/forward-le-04 is used by unchanged-getbar, getbytearray-pseq-nojunk,
int-abs/forward-le-05 is used by unchanged-rec-generic, unchanged-lookup-generic, unchanged-junkrefs-level, unchanged-junkrefs, unchanged-getbar, unchanged-array-forward, unchNorec-validrefs, unchNorec-transitivity, unchNorec-sym, unchNorec-junkrefs, unchNorec-isarray, unchNorec-index0, unchNorec-index, unchNorec-def-keep, pseq-sym-01, pseq-subset, maxpath-array-ls, maxpath-array, getbytearray-pseq-nojunk-02, getbytearray-pseq-02, cyclic-pseq,
int-abs/forward-lele is used by unchanged-getbar, getbytearray-pseq,
int-abs/forward-lels is used by unchanged-junkrefs-level, unchanged-getbar, unchNorec-junkrefs, unchNorec-index0, pseq-subset,
int-abs/forward-lsle is used by unchanged-getbar, unchNorec-index0, pseq-subset, getbytearray-pseq-nojunk-02, getbytearray-pseq-02,
int-abs/le-add is used by getbytearray-pseq-nojunk-02, getbytearray-pseq-02,
int-abs/lels is used by validref-pseq, unchanged-rec-generic, unchanged-lookup-generic, unchanged-junkrefs-level, unchanged-junkrefs, unchanged-getbar, unchanged-array-forward, unchNorec-validrefs, unchNorec-transitivity, unchNorec-sym, unchNorec-junkrefs, unchNorec-isobj, unchNorec-isarray, unchNorec-index0, unchNorec-index, unchNorec-field, unchNorec-def-keep, pseq-sym-01, pseq-subset, maxpath-array-ls, maxpath-array, getbytearray-pseq-nojunk-02, getbytearray-pseq-nojunk, getbytearray-pseq-02, getbytearray-pseq, cyclic-pseq,
int-abs/lels-01 is used by validref-pseq, unchanged-rec-generic, unchanged-lookup-generic, unchanged-junkrefs-level, unchanged-junkrefs, unchanged-getbar, unchanged-array-forward, unchNorec-validrefs, unchNorec-transitivity, unchNorec-sym, unchNorec-junkrefs, unchNorec-isobj, unchNorec-isarray, unchNorec-index0, unchNorec-index, unchNorec-field, unchNorec-def-keep, pseq-sym-01, pseq-subset, maxpath-array-ls, maxpath-array, getbytearray-pseq-nojunk-02, getbytearray-pseq-nojunk, getbytearray-pseq-02, getbytearray-pseq, cyclic-pseq,
int-abs/lels-02 is used by getbytearray-pseq-nojunk-02, getbytearray-pseq-02,
int-abs/lels-03 is used by unchanged-rec-generic, unchanged-lookup-generic, unchanged-junkrefs-level, unchanged-junkrefs, unchanged-getbar, unchanged-array-forward, unchNorec-validrefs, unchNorec-transitivity, unchNorec-sym, unchNorec-junkrefs, unchNorec-isarray, unchNorec-index, unchNorec-def-keep, pseq-sym-01, pseq-subset, maxpath-array-ls, maxpath-array, getbytearray-pseq-nojunk-02, getbytearray-pseq-02, cyclic-pseq,
int-abs/lels-04 is used by unchanged-rec-generic, unchanged-lookup-generic, unchanged-junkrefs-level, unchanged-junkrefs, unchanged-getbar, unchanged-array-forward, unchNorec-validrefs, unchNorec-transitivity, unchNorec-sym, unchNorec-junkrefs, unchNorec-isarray, unchNorec-index0, unchNorec-index, unchNorec-def-keep, pseq-sym-01, pseq-subset, maxpath-array-ls, maxpath-array, getbytearray-pseq-nojunk-02, getbytearray-pseq-02, cyclic-pseq,
int-abs/leone is used by getbytearray-pseq-nojunk-02, getbytearray-pseq-02,
int-abs/lep-01 is used by getbytearray-pseq-nojunk-02, getbytearray-pseq-02,
int-abs/ler is used by getbytearray-pseq-nojunk, getbytearray-pseq,
int-abs/mone-06 is used by getbytearray-pseq-nojunk-02, getbytearray-pseq-02,
int-abs/numle-02 is used by getbytearray-pseq-nojunk-02, getbytearray-pseq-02,
int-abs/numleledel-01 is used by getbytearray-pseq-nojunk-02, getbytearray-pseq-02,
int-abs/numls-02 is used by getbytearray-pseq-nojunk-02, getbytearray-pseq-02,
int-abs/numsub is used by getbytearray-pseq-nojunk-02, getbytearray-pseq-02,
int-abs/sub-add-05 is used by getbytearray-pseq-nojunk-02, getbytearray-pseq-02,
int-abs/sub-le-01 is used by getbytearray-pseq-nojunk-02, getbytearray-pseq-02,
int-abs/sub-ls-01 is used by getbytearray-pseq-nojunk-02, getbytearray-pseq-02,
int-abs/succ-01 is used by getbytearray-pseq-nojunk-02, getbytearray-pseq-02,
int-abs/zero-gels is used by unchanged-getbar,
int-abs/zero-gels-04 is used by unchNorec-isarray, getbytearray-pseq-nojunk-02, getbytearray-pseq-02,

Used from specification okfuns

okfuns/gfts-all is used by unchNorec-isobj, maxpath-object,
okfuns/good-field-def is used by unchNorec-isobj,
okfuns/is-any-array is used by unchNorec-isarray, getbytearray-pseq-nojunk-02, getbytearray-pseq-02,
okfuns/is-real-array-def is used by unchNorec-isarray-01,
okfuns/is_array-arraytype is used by pseq-sym-01, pseq-subset, cyclic-pseq,
okfuns/is_array-noreftype is used by pseq-sym-01, pseq-subset,
okfuns/is_array-norefval is used by pseq-sym-01, cyclic-pseq,
okfuns/is_array-notin-01 is used by pseq-subset,
okfuns/okarrayNotNull is used by unchNorec-isarray, getbytearray-pseq-nojunk-02, getbytearray-pseq-02,
okfuns/okreftype is used by validref-pseq, unchNorec-isarray, getbytearray-pseq-nojunk, getbytearray-pseq-02, getbytearray-pseq,
okfuns/good-field-field is used by unchNorec-isobj,
okfuns/good-field-field-01 is used by maxpath-object,
okfuns/good-field-index is used by unchNorec-isobj,
okfuns/is_array-arraytype is used by unchanged-junkrefs, unchNorec-validrefs, unchNorec-junkrefs, pseq-sym-01, cyclic-pseq,
okfuns/is_array-bytearray-01 is used by getbytearray-pseq-nojunk-02, getbytearray-pseq-02,
okfuns/is_array-classtype is used by unchanged-junkrefs-level, pseq-subset, cyclic-pseq,
okfuns/is_array-lenfield is used by pseq-subset,
okfuns/is_array-noreftype is used by pseq-subset,
okfuns/is_array-norefval is used by pseq-sym-01, pseq-subset, cyclic-pseq,
okfuns/is_array-type-04 is used by pseq-sym-01, pseq-subset,
okfuns/isarray-null is used by unchNorec-isarray-01, unchNorec-isarray,
okfuns/isarray-type is used by unchanged-lookup-generic, getbytearray-pseq-nojunk-02,
okfuns/okarray-05 is used by unchNorec-isarray, getbytearray-pseq-nojunk-02, getbytearray-pseq-02,
okfuns/okarray-type-03 is used by getbytearray-pseq-nojunk-02, getbytearray-pseq-02,
okfuns/okbar is used by unchanged-okbar, unchanged-getbar,
okfuns/okbar-len is used by unchanged-getbar,
okfuns/okbytearray-length-zero is used by unchanged-getbar,
okfuns/okbytearray-type is used by unchanged-getbar,
okfuns/oktype-byte is used by getbytearray-pseq-nojunk-02, getbytearray-pseq-02,
okfuns/oktype-okval is used by unchNorec-isarray,

Used from specification storekey

storekey/ex-03 is used by unchanged-field-lookup,
storekey/elim-03 is used by unchanged-lookup-generic, unchNorec-isobj,
storekey/elim-04 is used by unchanged-rec-generic, unchanged-lookup-generic,
storekey/sel-05 is used by unchanged-junkrefs-level, unchanged-junkrefs,
storekey/test is used by unchanged-field-lookup, unchNorec-isobj,
storekey/test-01 is used by unchanged-lookup-generic, unchNorec-isobj,
storekey/test-05 is used by unchanged-lookup-generic, unchNorec-isobj,
storekey/test-08 is used by unchanged-rec-generic, unchanged-lookup-generic,

Used from specification typefuns

typefuns/array is used by unchNorec-isarray,
typefuns/bytearray is used by getbytearray-pseq-nojunk-02, getbytearray-pseq-nojunk, getbytearray-pseq-02, getbytearray-pseq,
typefuns/class-le is used by unchanged-junkrefs-level, unchNorec-validrefs, unchNorec-junkrefs, cyclic-pseq,
typefuns/isreftype-04 is used by cyclic-pseq,
typefuns/le-noreftype-01 is used by pseq-sym-01, pseq-subset, cyclic-pseq,
typefuns/ref is used by unchNorec-isarray, maxpath-object, maxpath-array, getbytearray-pseq-02, cyclic-pseq,
typefuns/reftype-class is used by cyclic-pseq,
typefuns/subarray1 is used by unchNorec-isarray,
typefuns/subbasic2 is used by unchNorec-validrefs-pathex,
typefuns/subclass is used by pseq-subset, cyclic-pseq,
typefuns/subtype-object-01 is used by unchNorec-validrefs-pathex,

Used from specification nat-basic1

nat-basic1/f is used by maxpath-object, maxpath-array-ls, maxpath-array,
nat-basic1/less-1 is used by maxpath-array,
nat-basic1/lf-01 is used by maxpath-object, maxpath-array,
nat-basic1/ls-02 is used by maxpath-array-ls,
nat-basic1/z is used by maxpath-object,

Used from specification classnamefuns

classnamefuns/le-reflexive is used by pseq-subset, cyclic-pseq,

Used from specification int-basic1

int-basic1/irref is used by unchNorec-index0, pseq-subset, getbytearray-pseq-nojunk, getbytearray-pseq,
int-basic1/ls-01 is used by getbytearray-pseq-nojunk-02, getbytearray-pseq-02,
int-basic1/lst-01 is used by unchanged-getbar,

Used from specification refkey

refkey/inj is used by unchNorec-put-nopathex,
refkey/inj-01 is used by unchNorec-put-nopathex,

Used from specification set-basic

set-basic/reflistset/In-empty is used by maxpath-object, maxpath-array,
set-basic/reflistset/size-zero is used by maxpath-object, maxpath-array,
set-basic/reflistset/size-zero-01 is used by maxpath-object, maxpath-array,

Used from specification oelem

oelem/intlista/lel is used by getbytearray-pseq-nojunk-02, getbytearray-pseq-nojunk, getbytearray-pseq-02, getbytearray-pseq,
oelem/intlista/ls-le is used by unchanged-getbar,

Used from specification javatype

javatype/diff is used by unchanged-rec-generic, unchanged-lookup-generic, unchanged-junkrefs-level, unchNorec-transitivity, unchNorec-sym, unchNorec-def-keep, pseq-sym-01, pseq-subset, cyclic-pseq,
javatype/diff-01 is used by unchanged-rec-generic, unchanged-lookup-generic, unchanged-junkrefs-level, unchNorec-transitivity, unchNorec-sym, unchNorec-length-intro, unchNorec-index, unchNorec-def-keep, pseq-sym-01, pseq-subset, getbytearray-pseq-nojunk-02, cyclic-pseq,
javatype/disj-22 is used by getbytearray-pseq-nojunk,
javatype/elim-01 is used by unchanged-rec-generic, unchanged-junkrefs-level, unchNorec-validrefs, unchNorec-junkrefs, unchNorec-isarray,
javatype/elim-02 is used by unchanged-rec-generic, unchanged-lookup-generic, unchanged-junkrefs-level, unchanged-field-lookup, unchNorec-validrefs, unchNorec-transitivity, unchNorec-sym, unchNorec-junkrefs, unchNorec-isobj, unchNorec-field0, unchNorec-field, unchNorec-def-keep, pseq-sym-01, pseq-subset, maxpath-object, cyclic-pseq,
javatype/inj-01 is used by getbytearray-pseq-02,
javatype/inj-02 is used by maxpath-object,
javatype/sel-01 is used by unchanged-rec-generic, unchanged-junkrefs-level, unchNorec-validrefs, unchNorec-isarray, getbytearray-pseq-nojunk-02, getbytearray-pseq-02,
javatype/sel-02 is used by unchanged-rec-generic, unchanged-junkrefs-level, unchNorec-isobj, unchNorec-field0, unchNorec-field, pseq-sym-01, pseq-subset, cyclic-pseq,
javatype/test-09 is used by unchanged-rec-generic, unchanged-junkrefs-level, unchanged-getbar, unchNorec-validrefs, unchNorec-junkrefs, unchNorec-isarray, getbytearray-pseq-nojunk-02, getbytearray-pseq-nojunk, getbytearray-pseq-02, getbytearray-pseq,
javatype/test-10 is used by unchanged-rec-generic, unchanged-lookup-generic, unchanged-junkrefs-level, unchNorec-validrefs, unchNorec-transitivity, unchNorec-sym, unchNorec-junkrefs, unchNorec-isobj, unchNorec-field0, unchNorec-field, unchNorec-def-keep, pseq-sym-01, pseq-subset, maxpath-object, cyclic-pseq,
javatype/test-16 is used by unchanged-getbar, unchNorec-isarray, getbytearray-pseq-nojunk, getbytearray-pseq-02, getbytearray-pseq,
javatype/test-28 is used by unchNorec-isobj, unchNorec-field, pseq-sym-01, pseq-subset,

Used from specification javavalue

javavalue/ex-04 is used by getbytearray-pseq-02,
javavalue/refva-sel is used by pseq-subset, cyclic-pseq,
javavalue/diff-08 is used by getbytearray-pseq-nojunk-02,
javavalue/disj-41 is used by unchNorec-isobj, unchNorec-isarray,
javavalue/elim-02 is used by unchNorec-isarray, getbytearray-pseq-02,
javavalue/elim-10 is used by unchNorec-isobj, unchNorec-isarray,
javavalue/elim-13 is used by unchanged-junkrefs-level, unchanged-class-forward, unchanged-array-forward, unchNorec-validrefs, unchNorec-junkrefs, pseq-sym-01, pseq-subset,
javavalue/elim-refval is used by unchanged-rec-generic,
javavalue/refva-sel is used by pseq-sym-01, pseq-subset, cyclic-pseq,
javavalue/refval is used by cyclic-pseq,
javavalue/sel-04 is used by getbytearray-pseq-02,
javavalue/sel-09 is used by validref-pseq, unchanged-rec-generic, unchanged-junkrefs-level, unchanged-class-forward, unchanged-array-forward, unchNorec-validrefs, unchNorec-junkrefs, unchNorec-isarray, pseq-sym-01, pseq-subset, maxpath-object, maxpath-array, getbytearray-pseq-nojunk, getbytearray-pseq-02, getbytearray-pseq,
javavalue/sel-11 is used by unchanged-getbar, unchNorec-isobj, unchNorec-isarray, maxpath-object,
javavalue/test-01 is used by unchNorec-isarray,
javavalue/test-02 is used by pseq-subset,
javavalue/test-19 is used by validref-pseq, unchanged-rec-generic, unchanged-junkrefs-level, unchanged-class-forward, unchanged-array-forward, unchNorec-validrefs, unchNorec-junkrefs, unchNorec-isarray, pseq-sym-01, pseq-subset, maxpath-object, maxpath-array, getbytearray-pseq-nojunk, getbytearray-pseq-02, getbytearray-pseq,
javavalue/test-25 is used by unchNorec-isarray, getbytearray-pseq-02,
javavalue/test-40 is used by getbytearray-pseq-02,
javavalue/test-92 is used by unchNorec-isobj, unchNorec-isarray, maxpath-object,

Used from specification storearrays

storearrays/extension-01 is used by unchanged-getbar,
storearrays/getByteArray-all is used by getbytearray-pseq-nojunk, getbytearray-pseq,
storearrays/getbar-rec is used by getbytearray-pseq-nojunk-02, getbytearray-pseq-02,
storearrays/is_arrayref is used by unchNorec-isarray, getbytearray-pseq-02,
storearrays/bar-empty is used by getbytearray-pseq-nojunk, getbytearray-pseq,
storearrays/bar-empty-01 is used by getbytearray-pseq-nojunk-02, getbytearray-pseq-nojunk, getbytearray-pseq-02, getbytearray-pseq,

Used from specification list-dup

list-dup/references/c is used by cyclic-pseq,
list-dup/references/c-02 is used by maxpath-object, maxpath-array,
list-dup/references/dups-cons is used by unchanged-cyclic, maxpath-object, maxpath-array, cyclic-pseq,
list-dup/references/e-01 is used by unchanged-cyclic, maxpath-object, cyclic-pseq,
list-dup/references/f is used by maxpath-object, cyclic-pseq,
list-dup/references/rec is used by unchanged-cyclic, maxpath-object, maxpath-array,

Used from specification list-data

list-data/references/elim-list is used by unchanged-junkrefs, cyclic-pseq,
list-data/references/elim-list-c is used by unchanged-validrefs-unchNorec, unchanged-pathex-append, unchanged-pathex, unchanged-junkrefs-level, unchanged-junkref-level, unchanged-junkref, unchanged-cyclic, unchNorec-validrefs-pathex, unchNorec-validrefs, unchNorec-junkrefs, maxpath-object, maxpath-array,
list-data/references/l is used by maxpath-object, maxpath-array,
list-data/references/size-01 is used by maxpath-object,

Used from specification specialkeys

specialkeys/type-04 is used by unchNorec-put-nopathex,

Used from specification storefunsx

storefunsx/lookup-xtra is used by validref-pseq, unchNorec-isobj, unchNorec-isarray, pseq-subset, getbytearray-pseq-nojunk,

Used from specification javastore

javastore/at-other-16 is used by unchNorec-put-nopathex,
javastore/look-ins is used by unchNorec-put-nopathex,

Used from specification addfuns

addfuns/has_reffield-class is used by maxpath-object,
addfuns/instfields-index-01 is used by unchanged-field-lookup,
addfuns/is-any-object is used by unchNorec-isobj, maxpath-object,
addfuns/is-real-object-def is used by unchNorec-isobj-01,
addfuns/is-valid-ref is used by unchanged-lookup-generic,
addfuns/is-valid-ref-stronger-def is used by unchanged-junkrefs-level, unchanged-junkrefs, unchNorec-validrefs, unchNorec-junkrefs, unchNorec-isvalidref, pseq-sym-01, pseq-subset, cyclic-pseq,
addfuns/is_obj-arraytype is used by pseq-sym-01, cyclic-pseq,
addfuns/is_obj-classtype is used by pseq-subset,
addfuns/is_obj-def is used by unchNorec-isobj, maxpath-object,
addfuns/is_obj-field-in is used by pseq-subset,
addfuns/is_obj-field-noreftype is used by pseq-sym-01, pseq-subset,
addfuns/is_obj-field-norefval is used by pseq-sym-01, pseq-subset, cyclic-pseq,
addfuns/is_obj-notin-01 is used by pseq-subset,
addfuns/instfields-index-01 is used by unchanged-rec-generic, unchanged-lookup-generic,
addfuns/instfields-index-02 is used by unchanged-rec-generic, unchanged-class-forward,
addfuns/instfields-special is used by maxpath-object,
addfuns/is_obj-01 is used by maxpath-object,
addfuns/is_obj-arraytype is used by pseq-sym-01, pseq-subset, cyclic-pseq,
addfuns/is_obj-classtype is used by unchanged-junkrefs-level, unchanged-junkrefs, unchanged-field-lookup, unchNorec-validrefs-pathex, unchNorec-validrefs, unchNorec-junkrefs, cyclic-pseq,
addfuns/is_obj-field-norefval is used by pseq-sym-01, pseq-subset,
addfuns/is_obj-null is used by unchanged-type-in,
addfuns/is_valid_ref is used by pseq-sym-01, cyclic-pseq,
addfuns/is_valid_ref-01 is used by pseq-sym-01,
addfuns/is_valid_ref-array is used by getbytearray-pseq-nojunk-02, getbytearray-pseq-02,
addfuns/is_valid_ref-array-01 is used by unchanged-rec-generic, unchanged-junkrefs-level, unchNorec-put-nopathex, pseq-sym-01, pseq-subset,
addfuns/is_valid_ref-isarray is used by unchanged-junkrefs-level, unchanged-isarray, maxpath-array,
addfuns/is_valid_ref-isobj is used by unchanged-unchNorec-same, unchanged-type-in, unchanged-junkrefs-level, unchanged-isobj, pseq-sym-01, maxpath-object, cyclic-pseq,
addfuns/is_valid_ref-no-arraytype is used by unchanged-junkrefs-level, unchNorec-validrefs-pathex,
addfuns/is_valid_ref-notin-01 is used by unchanged-type-in,
addfuns/is_valid_ref-null is used by maxpath-object, maxpath-array,
addfuns/is_valid_ref-okbytearray is used by unchanged-getbar,
addfuns/is_valid_ref-type-01 is used by unchanged-rec-generic, unchanged-junkrefs-level,
addfuns/is_valid_ref-typeex is used by cyclic-pseq,
addfuns/isarray-isobj-01 is used by pseq-sym-01, cyclic-pseq,
addfuns/isobj-classtype is used by unchanged-lookup-generic,
addfuns/isobj-instfields is used by maxpath-object,
addfuns/isobj-null-02 is used by unchNorec-isobj-01, unchNorec-isobj,

Used from specification nat

nat/eqle-one is used by maxpath-object, maxpath-array,
nat/l-num-06 is used by maxpath-object,
nat/le-add is used by maxpath-object, maxpath-array,
nat/le-num-02 is used by maxpath-object, maxpath-array,
nat/lels is used by pseq-sym-01, pseq-subset, maxpath-array, cyclic-pseq,
nat/lels-01 is used by maxpath-array-ls,
nat/let is used by maxpath-object, maxpath-array,
nat/lez is used by maxpath-object, maxpath-array,
nat/lez-01 is used by maxpath-object, maxpath-array,
nat/succ-01 is used by maxpath-object, maxpath-array,

Used from specification list-last

list-last/references/l-01 is used by unchanged-pathex-append,
list-last/references/l is used by maxpath-object,
list-last/references/l-02 is used by unchanged-pathex-append, maxpath-object,
list-last/references/l-05 is used by maxpath-object, maxpath-array,
list-last/references/last-01 is used by unchNorec-validrefs-pathex,
list-last/references/last-elim is used by maxpath-object,
list-last/references/lin-01 is used by unchanged-pathex-append,

Used from specification nat-basic2

nat-basic2/a is used by maxpath-object, maxpath-array,
nat-basic2/c is used by maxpath-object, maxpath-array,
nat-basic2/l is used by maxpath-object,
nat-basic2/s is used by maxpath-array,

Used from specification set-union

set-union/reflistset/ext is used by maxpath-object, maxpath-array,