[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 cyclic

cyclic/cyclic-def is used by nosharing-nocycle,
cyclic/pathex-array is used by disjoint-forward-array,
cyclic/pathex-class is used by disjoint-forward-field,
cyclic/pathex-def is used by sharing-twopaths, sharing-pathex-field-self-01, sharing-pathex-field-self,
cyclic/pathex-def-simple is used by unchanged-put-nosharing, putbar-classfield-onlymod, hasSharing-pathex, hasSharing-dd-help, disjoint-nopathex, disjoint-def-pathex,
cyclic/pathex-subset-equiv is used by disjoint-subset,
cyclic/pathex-trans is used by disjoint-pathex-forward,
cyclic/validrefs-append is used by hasSharing-dd-help,
cyclic/validrefs-array is used by hassharing-validrefs-dups, hasSharing-pathex, ex-validrefs-fits-stronger, ex-fits-validrefs-stronger,
cyclic/validrefs-class is used by putbar-classfield-onlymod, hassharing-validrefs-dups, hasSharing-pathex, ex-validrefs-fits-stronger, ex-fits-validrefs-stronger,
cyclic/validrefs-is-junk is used by hassharing-validrefs-dups, hasSharing-pathex, ex-validrefs-fits-stronger,
cyclic/validrefs-newref is used by disjoint-newref-02, disjoint-newref-01, disjoint-newref,
cyclic/validrefs-nopathex is used by hassharing-validrefs-dups, fits-pathex, disjoint-nojunk-newref-subset-01, disjoint-nojunk-newref-subset,
cyclic/validrefs-null is used by ex-validrefs-fits-stronger,
cyclic/validrefs-one is used by sharing-pathex-field-self-01, sharing-pathex-field-self, putbar-classfield-onlymod, ex-fits-validrefs-stronger, disjoint-nojunk-newref-subset-01, disjoint-nojunk-newref-subset,
cyclic/validrefs-postfix is used by hassharing-validrefs-dups, hasSharing-dd-help,
cyclic/validrefs-prefix is used by hassharing-validrefs-dups, hasSharing-dd-help,
cyclic/validrefs-sametype-02 is used by hasSharing-pathex,
cyclic/validrefs-subset-equiv-01 is used by disjoint-nojunk-newref-subset-01, disjoint-nojunk-newref-subset,
cyclic/validrefs-superclass is used by ex-fits-validrefs-stronger,
cyclic/okbar-nopath is used by getbar-onlyModified-all, getbar-onlyModified,
cyclic/pathex-no-newref is used by disjoint-nojunk-newref-subset-01, disjoint-nojunk-newref-subset,
cyclic/pathex-not-is-validref-01 is used by disjoint-nopathex-same,
cyclic/pathex-null is used by disjoint-pathex-forward-both, disjoint-forward-field, disjoint-forward-array,
cyclic/pathex-null-01 is used by disjoint-pathex-forward-both,
cyclic/pathex-one is used by unchanged-lookup-list-generic, unchanged-fits, putBar-onlyMod, hassharing-validrefs-dups, fits-pathex, disjoint-nopathex-same, disjoint-nopath-both, disjoint-nojunk-newref-subset-01, disjoint-nojunk-newref-subset, disjoint-forward-field, disjoint-forward-array,
cyclic/validrefs-empty is used by hassharing-validrefs-dups,
cyclic/validrefs-nopathex-01 is used by hasSharing-dd-help,
cyclic/validrefs-not is used by hassharing-validrefs-dups, hasSharing-pathex,
cyclic/validrefs-null-02 is used by sharing-pathex-field-self-01, sharing-pathex-field-self, hassharing-validrefs-dups, hasSharing-pathex, hasSharing-dd-help, ex-fits-validrefs-stronger, disjoint-nojunk-newref-subset-01, disjoint-nojunk-newref-subset,
cyclic/validrefs-sametype is used by putbar-classfield-onlymod, nosharing-nocycle, hassharing-validrefs-dups, hasSharing-pathex,

Used from specification store

store/javastore/At-other is used by fits-put-stronger, fits-put-short-02, fits-put-short-01, fits-put-short, fits-put-other, fits-put-05-stronger, fits-put-05, fits-put-04, fits-put-03, fits-put-01, fits-put, at-put-prim,
store/javastore/rew is used by put-switch-primval-index-index, put-switch-primval-index-field, put-switch-primval-field-index, put-switch-primval-field-field,
store/javastore/superset-elem-eq is used by fits-superset, fits-subset, disjoint-nojunk-newref-subset-01, disjoint-nojunk-newref-subset,
store/javastore/At-other is used by fits-put-02-stronger, fits-put-02,
store/javastore/At-same is used by hasSharing-put-index-refval, fits-put-stronger, fits-put-short-02, fits-put-short-01, fits-put-short, fits-put-other, fits-put-05-stronger, fits-put-05, fits-put-04, fits-put-03, fits-put-02-stronger, fits-put-02, fits-put-01, fits-put, at-put-prim,
store/javastore/notmemlookup is used by fits-superset, fits-subset, fits-in,
store/javastore/sub-ref is used by hasSharing-addobj-same, hasSharing-addarray,

Used from specification addarray

addarray/add-at-ok is used by addarray-disjoint-nosharing,
addarray/subset-addarray-01 is used by hasSharing-addarray,
addarray/add-at-ok is used by addarray-disjoint-nosharing-01,
addarray/addarray-subset is used by addarray-disjoint-nosharing-01, addarray-disjoint-nosharing,
addarray/length-1init-01 is used by addarray-disjoint-nosharing-01, addarray-disjoint-nosharing,
addarray/type-1init is used by addarray-disjoint-nosharing-01, addarray-disjoint-nosharing,

Used from specification list

list/references/In is used by hassharing-validrefs-dups,
list/references/Noassoc is used by hassharing-validrefs-dups,
list/references/a is used by hassharing-validrefs-dups,
list/references/firsteq-01 is used by hasSharing-pathex,
list/references/split-first is used by hasSharing-dd-help,
list/references/Last is used by disjoint-forward-field-02, disjoint-forward-field, disjoint-forward-array-01, disjoint-forward-array,
list/storekeys/Last is used by hasSharing-put-index-refval, fits-put-other,
list/references/Nil is used by hasSharing-pathex,
list/storekeys/Nil is used by put-switch-primval-index-index, put-switch-primval-index-field, put-switch-primval-field-index, put-switch-primval-field-field, hasSharing-put-index-refval, fits-put-other, fits-no-refval, fits-append,
list/storekeys/Two is used by sharing-pathex-field-self-01, sharing-pathex-field-self,
list/references/Two is used by putbar-classfield-onlymod, disjoint-forward-field-02, disjoint-forward-array-01,
list/javavalues/a is used by hasSharing-put-index-refval,
list/bytelist/a is used by hasSharing-putbar, getbar-onlyModified-all,
list/storekeys/a is used by unchanged-lookup-list-generic, unchanged-fits, sharing-twopaths, sharing-pathex-field-self-01, sharing-pathex-field-self, put-switch-primval-index-index, put-switch-primval-index-field, put-switch-primval-field-index, put-switch-primval-field-field, nosharing-forward, lookup-statfield, hassharing-validrefs-dups, hassharing-bytearray, hasSharing-put-statfield, hasSharing-put-index-refval, hasSharing-object-rec, hasSharing-def-better, hasSharing-array-forward, hasSharing-addobj-same, fits-storekeys-one, fits-rec, fits-put-stronger, fits-put-short-02, fits-put-short-01, fits-put-short, fits-put-other, fits-put-05, fits-put-04, fits-put-03, fits-put-02, fits-put-01, fits-put, fits-null, fits-no-refval-01, fits-no-refval, fits-no-reftype-01, fits-no-reftype, fits-in, fits-append, ex-validrefs-fits-stronger, ex-fits-validrefs-stronger, at-put-prim, addarray-disjoint-nosharing-01, addarray-disjoint-nosharing,
list/references/a is used by unchanged-put-nosharing, sharing-twopaths, sharing-pathex-field-self-01, sharing-pathex-field-self, putbar-classfield-onlymod, nosharing-nocycle, hassharing-validrefs-dups, hasSharing-rec, hasSharing-put-index-refval, hasSharing-pathex, hasSharing-different-disjoint, hasSharing-dd-help, fits-pathex, ex-validrefs-fits-stronger, ex-validrefs-fits, ex-fits-validrefs-stronger, ex-fits-validrefs, disjoint-symmetric, disjoint-subset-01, disjoint-pathex-forward, disjoint-nopathex-same, disjoint-nopathex, disjoint-nopath-both, disjoint-nojunk-newref-subset-01, disjoint-nojunk-newref-subset, disjoint-newref-02, disjoint-newref-01, disjoint-newref, disjoint-forward-field-02, disjoint-forward-field, disjoint-forward-array-01, disjoint-forward-array, disjoint-def-pathex, disjoint-def-fits,
list/storekeys/app is used by unchanged-lookup-list-generic, lookup-statfield, hasSharing-put-index-refval, hasSharing-addobj-same, fits-storekeys-one, fits-put-stronger, fits-put-short, fits-put-other, fits-put-05, fits-put-04, fits-put-03, fits-put-02, fits-put-01, fits-put, fits-no-refval, fits-no-reftype-01, fits-no-reftype, fits-in, fits-append, ex-validrefs-fits-stronger, ex-fits-validrefs-stronger, at-put-prim, addarray-disjoint-nosharing-01, addarray-disjoint-nosharing,
list/references/app is used by sharing-twopaths, sharing-pathex-field-self-01, sharing-pathex-field-self, hassharing-validrefs-dups, hasSharing-pathex, hasSharing-dd-help, fits-pathex, ex-validrefs-fits, ex-fits-validrefs-stronger, ex-fits-validrefs, disjoint-nojunk-newref-subset-01, disjoint-nojunk-newref-subset, disjoint-forward-field-02, disjoint-forward-array-01,
list/storekeys/app-01 is used by sharing-pathex-field-self-01, sharing-pathex-field-self, nosharing-forward, hassharing-validrefs-dups, hasSharing-put-index-refval, hasSharing-object-rec, hasSharing-array-forward, hasSharing-addobj-same, fits-put-other, addarray-disjoint-nosharing-01, addarray-disjoint-nosharing,
list/storekeys/app-02-ant is used by unchanged-fits, sharing-twopaths, sharing-pathex-field-self-01, sharing-pathex-field-self, put-switch-primval-index-field, put-switch-primval-field-index, put-switch-primval-field-field, nosharing-forward, hassharing-validrefs-dups, hassharing-bytearray, hasSharing-put-index-refval, hasSharing-object-rec, hasSharing-def-better, hasSharing-array-forward, hasSharing-addobj-same, fits-put-short-02, fits-put-short-01, fits-put-other, fits-no-refval-01, fits-no-refval, addarray-disjoint-nosharing-01, addarray-disjoint-nosharing,
list/bytelist/app-02-ant is used by hasSharing-putbar,
list/references/app-02-ant is used by unchanged-put-nosharing, sharing-twopaths, sharing-pathex-field-self-01, sharing-pathex-field-self, putbar-classfield-onlymod, hassharing-validrefs-dups, hasSharing-pathex, hasSharing-dd-help, ex-validrefs-fits, disjoint-nopathex, disjoint-def-pathex, disjoint-def-fits,
list/references/app-03 is used by hasSharing-dd-help,
list/storekeys/app-04 is used by sharing-twopaths, sharing-pathex-field-self-01, sharing-pathex-field-self, hassharing-validrefs-dups, hasSharing-put-index-refval, hasSharing-def-better,
list/storekeys/c is used by unchanged-lookup-list-generic, unchanged-fits, sharing-pathex-field-self-01, sharing-pathex-field-self, nosharing-forward, lookup-statfield, hassharing-validrefs-dups, hassharing-bytearray, hasSharing-put-statfield, hasSharing-put-index-refval, hasSharing-array-forward, hasSharing-addobj-same, fits-superset, fits-subset, fits-rec, fits-put-stronger, fits-put-statfield, fits-put-short-02, fits-put-short-01, fits-put-short, fits-put-other, fits-put-05-stronger, fits-put-05, fits-put-04, fits-put-03, fits-put-02-stronger, fits-put-02, fits-put-01, fits-put, fits-null, fits-no-refval, fits-no-reftype-01, fits-no-reftype, fits-in, fits-append, ex-validrefs-fits-stronger, ex-fits-validrefs-stronger, at-put-prim, addarray-disjoint-nosharing-01, addarray-disjoint-nosharing,
list/bytelist/c is used by hasSharing-putbar, getbar-onlyModified-all,
list/references/c is used by unchanged-put-nosharing, sharing-twopaths, sharing-pathex-field-self-01, sharing-pathex-field-self, nosharing-nocycle, hassharing-validrefs-dups, hasSharing-pathex, hasSharing-different-disjoint, hasSharing-dd-help, ex-validrefs-fits-stronger, ex-validrefs-fits, disjoint-nopathex, disjoint-nojunk-newref-subset-01, disjoint-nojunk-newref-subset, disjoint-newref-02, disjoint-newref-01, disjoint-newref, disjoint-def-pathex, disjoint-def-fits,
list/storekeys/c-03 is used by sharing-pathex-field-self-01, sharing-pathex-field-self,
list/references/c-03 is used by hasSharing-pathex,
list/storekeys/c-04 is used by hasSharing-dups-object, hasSharing-dups-array, hasSharing-addobj-same,
list/references/c-05 is used by hasSharing-pathex,
list/storekeys/c-05 is used by fits-put-other,
list/storekeys/c-06 is used by hasSharing-addobj-same,
list/bytelist/c-06 is used by getbar-onlyModified-all,
list/storekeys/c-07 is used by unchanged-fits, hassharing-bytearray, hasSharing-put-index-refval, hasSharing-addobj-same, fits-put-other, addarray-disjoint-nosharing-01, addarray-disjoint-nosharing,
list/bytelist/c-07 is used by hasSharing-putbar,
list/storekeys/c-08 is used by unchanged-fits, hassharing-bytearray, hasSharing-put-index-refval, hasSharing-addobj-same, fits-put-other, addarray-disjoint-nosharing-01, addarray-disjoint-nosharing,
list/references/c-08 is used by unchanged-put-nosharing, sharing-twopaths, sharing-pathex-field-self-01, sharing-pathex-field-self, putbar-classfield-onlymod, nosharing-nocycle, hassharing-validrefs-dups, hasSharing-pathex, hasSharing-dd-help, ex-validrefs-fits, ex-fits-validrefs-stronger, disjoint-nopathex, disjoint-def-pathex, disjoint-def-fits,
list/bytelist/c-08 is used by hasSharing-putbar,
list/bytelist/e is used by hasSharing-putbar,
list/storekeys/e is used by unchanged-lookup-list-generic, unchanged-fits, sharing-pathex-field-self-01, sharing-pathex-field-self, nosharing-forward, hassharing-validrefs-dups, hassharing-bytearray, hasSharing-put-index-refval, hasSharing-object-rec, hasSharing-dups-object, hasSharing-dups-array, hasSharing-array-forward, hasSharing-addobj-same, fits-put-short-02, fits-put-short-01, fits-put-other, fits-no-refval-01, fits-no-refval, addarray-disjoint-nosharing-01, addarray-disjoint-nosharing,
list/references/e is used by unchanged-put-nosharing, sharing-twopaths, sharing-pathex-field-self-01, sharing-pathex-field-self, putbar-classfield-onlymod, hassharing-validrefs-dups, hasSharing-pathex, hasSharing-dd-help, ex-validrefs-fits, disjoint-nopathex, disjoint-def-pathex, disjoint-def-fits,
list/bytelist/e-01 is used by hasSharing-putbar,
list/storekeys/e-01 is used by unchanged-fits, sharing-pathex-field-self-01, sharing-pathex-field-self, nosharing-forward, lookup-statfield, hassharing-bytearray, hasSharing-put-statfield, hasSharing-put-index-refval, hasSharing-addobj-same, fits-rec, fits-put-other, fits-null, fits-no-refval, fits-no-reftype-01, fits-no-reftype, fits-in, ex-fits-validrefs-stronger, at-put-prim, addarray-disjoint-nosharing-01, addarray-disjoint-nosharing,
list/references/e-01 is used by unchanged-put-nosharing, sharing-twopaths, sharing-pathex-field-self-01, sharing-pathex-field-self, nosharing-nocycle, hassharing-validrefs-dups, hasSharing-pathex, hasSharing-different-disjoint, hasSharing-dd-help, ex-validrefs-fits-stronger, ex-validrefs-fits, ex-fits-validrefs-stronger, disjoint-nopathex, disjoint-nojunk-newref-subset-01, disjoint-nojunk-newref-subset, disjoint-newref-02, disjoint-newref-01, disjoint-newref, disjoint-def-pathex, disjoint-def-fits,
list/references/e-02 is used by hasSharing-pathex, hasSharing-dd-help,
list/storekeys/e-02 is used by put-switch-primval-index-index, put-switch-primval-index-field, put-switch-primval-field-index, put-switch-primval-field-field, hasSharing-put-index-refval, fits-put-other, fits-no-refval,
list/storekeys/e-03 is used by hasSharing-put-index-refval,
list/references/e-03 is used by hasSharing-dd-help,
list/references/first is used by putbar-classfield-onlymod,
list/references/fr is used by hassharing-validrefs-dups, hasSharing-pathex,
list/references/in-01 is used by hasSharing-dd-help, disjoint-forward-field-02, disjoint-forward-array-01,
list/references/in-06 is used by unchanged-put-nosharing, hassharing-validrefs-dups, hasSharing-rec, hasSharing-put-index-refval, disjoint-symmetric, disjoint-nopathex-same, disjoint-nopathex, disjoint-nopath-both, disjoint-newref-02, disjoint-newref-01, disjoint-newref, disjoint-forward-field-02, disjoint-forward-array-01,
list/references/in-08 is used by hasSharing-pathex,
list/references/in-11 is used by hasSharing-dd-help,
list/references/in-14 is used by hasSharing-pathex, hasSharing-dd-help,
list/references/in-15 is used by hasSharing-pathex, hasSharing-dd-help,
list/references/in-17 is used by unchanged-put-nosharing, hassharing-one, hasSharing-rec, hasSharing-put-index-refval, hasSharing-pathex, hasSharing-different-disjoint, hasSharing-dd-help, disjoint-symmetric, disjoint-subset-01, disjoint-pathex-forward, disjoint-one, disjoint-nopathex-same, disjoint-nopathex, disjoint-nopath-both, disjoint-nojunk-newref-subset-01, disjoint-nojunk-newref-subset, disjoint-newref-02, disjoint-newref-01, disjoint-newref, disjoint-forward-field-02, disjoint-forward-field, disjoint-forward-array-01, disjoint-forward-array,
list/storekeys/in-17 is used by fits-no-reftype-01, fits-no-reftype,
list/references/in-append is used by hasSharing-rec, hasSharing-pathex, hasSharing-different-disjoint, hasSharing-dd-help, disjoint-symmetric, disjoint-subset-01, disjoint-pathex-forward, disjoint-nojunk-newref-subset-01, disjoint-nojunk-newref-subset, disjoint-newref-02, disjoint-newref-01, disjoint-newref, disjoint-forward-field, disjoint-forward-array,
list/storekeys/in-append is used by fits-no-reftype-01, fits-no-reftype,
list/references/in-empty is used by hassharing-validrefs-dups, disjoint-nojunk-newref-subset-01, disjoint-nojunk-newref-subset,
list/storekeys/in-empty is used by put-switch-primval-index-field, put-switch-primval-field-index, fits-no-reftype-01, fits-no-reftype,
list/references/inapp-07 is used by hasSharing-pathex,
list/references/inapp-10 is used by hasSharing-dd-help,
list/references/len is used by sharing-twopaths, sharing-pathex-field-self-01, sharing-pathex-field-self, hassharing-validrefs-dups, hasSharing-pathex, hasSharing-dd-help, ex-validrefs-fits-stronger, ex-validrefs-fits, ex-fits-validrefs-stronger,
list/storekeys/len is used by ex-validrefs-fits-stronger, ex-fits-validrefs-stronger,
list/references/len-02 is used by sharing-twopaths, sharing-pathex-field-self-01, sharing-pathex-field-self, hassharing-validrefs-dups, hasSharing-pathex, hasSharing-dd-help, ex-validrefs-fits-stronger, ex-validrefs-fits, ex-fits-validrefs-stronger,
list/storekeys/len-02 is used by ex-validrefs-fits-stronger, ex-fits-validrefs-stronger,
list/references/ni is used by hasSharing-pathex,

Used from specification storefuns

Used from specification int-basic2

int-basic2/add-a is used by getbar-onlyModified-all,
int-basic2/add-c is used by hasSharing-putbar, getbar-onlyModified-all,
int-basic2/ax-04 is used by getbar-onlyModified-all,

Used from specification valuefuns

valuefuns/refval-xtra is used by sharing-twopaths, sharing-pathex-field-self-01, sharing-pathex-field-self, putbar-classfield-onlymod, put-switch-primval-index-index, put-switch-primval-index-field, put-switch-primval-field-index, put-switch-primval-field-field, nosharing-forward, hassharing-validrefs-dups, hassharing-bytearray, hasSharing-subset, hasSharing-putbar, hasSharing-put-statfield, hasSharing-put-shortval, hasSharing-put-index-refval, hasSharing-put-byteval-01, hasSharing-put-byteval, hasSharing-object-rec, hasSharing-def-better, hasSharing-dd-help, hasSharing-array-forward, hasSharing-addobj-same, disjoint-forward-field, disjoint-forward-array, disjoint-def-fits, addarray-disjoint-nosharing-01, addarray-disjoint-nosharing,

Used from specification valuesfuns

valuesfuns/javavalues-in is used by disjoint-def-fits, addarray-disjoint-nosharing,
valuesfuns/mkvalsr-at is used by addarray-disjoint-nosharing,
valuesfuns/nonnullrefs-dups is used by addarray-disjoint-nosharing-01,
valuesfuns/nonnullrefs-in is used by addarray-disjoint-nosharing-01,
valuesfuns/javavalues-in is used by addarray-disjoint-nosharing-01,
valuesfuns/mkvalsr-len is used by addarray-disjoint-nosharing,
valuesfuns/mkvalsr-one is used by hasSharing-put-index-refval,
valuesfuns/mkvalsr-rec is used by hasSharing-put-index-refval,

Used from specification junkrefs

junkrefs/junkref-array is used by unchanged-lookup-list-generic, unchanged-fits, lookup-statfield, fits-superset, fits-subset, fits-put-stronger, fits-put-statfield, fits-put-short-02, fits-put-short-01, fits-put-short, fits-put-05-stronger, fits-put-05, fits-put-04, fits-put-03, fits-put-02-stronger, fits-put-02, fits-put-01, fits-put, fits-no-refval, fits-no-reftype-01, fits-no-reftype, fits-in, ex-fits-validrefs-stronger, disjoint-forward-array, at-put-prim,
junkrefs/junkref-class is used by unchanged-lookup-list-generic, unchanged-fits, putbar-classfield-onlymod, lookup-statfield, fits-superset, fits-subset, fits-put-stronger, fits-put-statfield, fits-put-short-02, fits-put-short-01, fits-put-short, fits-put-05-stronger, fits-put-05, fits-put-04, fits-put-03, fits-put-02-stronger, fits-put-02, fits-put-01, fits-put, fits-no-refval, fits-no-reftype-01, fits-no-reftype, fits-in, ex-fits-validrefs-stronger, disjoint-forward-field, at-put-prim,
junkrefs/junkref-is-junk is used by unchanged-lookup-list-generic, unchanged-fits, putbar-classfield-onlymod, lookup-statfield, fits-superset, fits-subset, fits-put-stronger, fits-put-statfield, fits-put-short-02, fits-put-short-01, fits-put-short, fits-put-05-stronger, fits-put-05, fits-put-04, fits-put-03, fits-put-02-stronger, fits-put-02, fits-put-01, fits-put, fits-no-refval, fits-no-reftype-01, fits-no-reftype, fits-in, ex-fits-validrefs-stronger, disjoint-forward-field, disjoint-forward-array, at-put-prim,
junkrefs/validref-forward is used by nosharing-forward,
junkrefs/validref-object is used by hasSharing-put-index-refval,
junkrefs/validreflist-def is used by disjoint-def-fits, addarray-disjoint-nosharing-01, addarray-disjoint-nosharing,
junkrefs/validreflist-no-reftype is used by addarray-disjoint-nosharing-01, addarray-disjoint-nosharing,
junkrefs/validreflist-one is used by hasSharing-put-index-refval,
junkrefs/validreflist-rec is used by hasSharing-put-index-refval,
junkrefs/validreflist-supertype is used by addarray-disjoint-nosharing-01, addarray-disjoint-nosharing,
junkrefs/validrefnotnull-def is used by nosharing-forward,
junkrefs/junkref-bad-type is used by unchanged-lookup-list-generic, hasSharing-put-index-refval,
junkrefs/junkref-keyin is used by disjoint-nojunk-newref-subset-01, disjoint-nojunk-newref-subset,
junkrefs/junkref-newref is used by disjoint-nojunk-newref-subset-01, disjoint-nojunk-newref-subset,
junkrefs/junkref-noreftype is used by fits-no-reftype-01, fits-no-reftype,
junkrefs/junkref-not-valid-01 is used by unchanged-lookup-list-generic, unchanged-fits, fits-put-01, fits-pathex, ex-fits-validrefs-stronger,
junkrefs/junkref-notin is used by fits-in-01, addarray-disjoint-nosharing-01, addarray-disjoint-nosharing,
junkrefs/junkref-null is used by unchanged-fits, lookup-statfield, hasSharing-put-statfield, hasSharing-addobj-same, fits-superset, fits-subset, fits-put-stronger, fits-put-short-02, fits-put-short-01, fits-put-short, fits-put-05-stronger, fits-put-05, fits-put-04, fits-put-03, fits-put-02-stronger, fits-put-01, fits-put, fits-in, ex-fits-validrefs-stronger, at-put-prim, addarray-disjoint-nosharing-01, addarray-disjoint-nosharing,
junkrefs/junkref-putbar-01 is used by hasSharing-putbar,
junkrefs/validfieldinits-junkref is used by hasSharing-addobj-same,
junkrefs/validfieldinits-validreflist is used by hasSharing-addobj-same,
junkrefs/validref-junkref is used by disjoint-def-fits, addarray-disjoint-nosharing-01, addarray-disjoint-nosharing,
junkrefs/validref-null is used by nosharing-forward, hasSharing-put-index-refval,
junkrefs/validref-object-01 is used by hasSharing-put-index-refval,
junkrefs/validreflist-one-01 is used by hasSharing-put-index-refval,
junkrefs/validreflist-rec-01 is used by hasSharing-put-index-refval,
junkrefs/validrefnotnull-junk is used by fits-pathex-01,
junkrefs/validrefnotnull-notnull is used by nosharing-forward, fits-pathex-01,

Used from specification fieldspec

Used from specification intnat

intnat/num-i2n-le-02 is used by addarray-disjoint-nosharing-01, addarray-disjoint-nosharing,
intnat/abs-eq is used by addarray-disjoint-nosharing-01, addarray-disjoint-nosharing,
intnat/inni-ls is used by addarray-disjoint-nosharing,
intnat/labs is used by getbar-onlyModified-all, addarray-disjoint-nosharing,
intnat/num-n2i-ls-02 is used by addarray-disjoint-nosharing-01, addarray-disjoint-nosharing,

Used from specification int-abs

Used from specification pointers

pointers/unchanged-junkref is used by unchanged-lookup-list-generic,
pointers/unchanged-lookup-generic is used by unchanged-lookup-list-generic, unchanged-fits,
pointers/unchanged-put-nopathex is used by unchanged-put-nosharing,
pointers/unchanged-rec-generic is used by unchanged-lookup-list-generic, unchanged-fits,
pointers/unchanged-symmetric is used by unchanged-lookup-list-generic,
pointers/unchanged-type is used by unchanged-fits,
pointers/unchanged-null is used by unchanged-fits,

Used from specification okfuns

okfuns/is_array-badlength is used by fits-put-short-02, fits-put-short-01, fits-put-05-stronger, fits-put-05, fits-put-04,
okfuns/is_array-notypeval is used by fits-put-05,
okfuns/nonnullrefs-dups is used by hasSharing-addobj-same,
okfuns/nonnullrefs-dups-key is used by hasSharing-addobj-same,
okfuns/nonnullrefs-in is used by hasSharing-addobj-same,
okfuns/nonnullrefs-in-key is used by hasSharing-addobj-same,
okfuns/okarrayNotNull is used by fits-put-stronger, fits-put-01, fits-put,
okfuns/okbar-putbar-same is used by hasSharing-putbar,
okfuns/okbytearray-01 is used by hasSharing-putbar,
okfuns/is_array-arraytype is used by unchanged-lookup-list-generic, unchanged-fits, lookup-statfield, hasSharing-pathex, fits-superset, fits-subset, fits-put-stronger, fits-put-statfield, fits-put-short-02, fits-put-short-01, fits-put-short, fits-put-05-stronger, fits-put-05, fits-put-04, fits-put-03, fits-put-02-stronger, fits-put-02, fits-put-01, fits-put, fits-no-refval, fits-no-reftype-01, fits-no-reftype, fits-in, ex-fits-validrefs-stronger, at-put-prim,
okfuns/is_array-classtype is used by unchanged-lookup-list-generic, lookup-statfield, hassharing-validrefs-dups, fits-superset, fits-subset, fits-put-stronger, fits-put-short-02, fits-put-short-01, fits-put-short, fits-put-05-stronger, fits-put-05, fits-put-02-stronger, fits-put-02, fits-put-01, fits-put, fits-no-refval, ex-validrefs-fits-stronger, ex-fits-validrefs-stronger,
okfuns/is_array-lenfield is used by fits-superset, fits-subset,
okfuns/is_array-notin-01 is used by fits-subset,
okfuns/is_array-okarray is used by fits-put-stronger, fits-put,
okfuns/is_array-type-02 is used by fits-superset, fits-subset,
okfuns/is_array-type-04 is used by putbar-classfield-onlymod,
okfuns/keys-notin is used by hasSharing-addobj-same,
okfuns/keys-notin-02 is used by hasSharing-addobj-same,
okfuns/okarray-05 is used by hasSharing-putbar, hasSharing-put-byteval, fits-put-stronger, fits-put-02-stronger, fits-put-02, fits-put-01, fits-put,
okfuns/okarray-type-03 is used by fits-put-stronger, fits-put-02-stronger, fits-put-02, fits-put-01, fits-put,
okfuns/okbar is used by putbar-classfield-onlymod,
okfuns/okbytearray-not is used by hassharing-bytearray,
okfuns/okbytearray-type is used by putbar-classfield-onlymod, hassharing-bytearray,
okfuns/oktype-byte is used by fits-put-stronger, fits-put-01, fits-put,

Used from specification storekey

Used from specification typefuns

typefuns/le-noreftype-01 is used by fits-no-reftype-01, fits-no-reftype,
typefuns/ref is used by hassharing-validrefs-dups, hasSharing-pathex, ex-fits-validrefs-stronger,
typefuns/subclass is used by putbar-classfield-onlymod, ex-fits-validrefs-stronger,
typefuns/subtype-object-01 is used by addarray-disjoint-nosharing-01, addarray-disjoint-nosharing,

Used from specification classnamefuns

classnamefuns/le-reflexive is used by putbar-classfield-onlymod, ex-fits-validrefs-stronger,

Used from specification nat-basic1

nat-basic1/f is used by hasSharing-dd-help, addarray-disjoint-nosharing-01, addarray-disjoint-nosharing,
nat-basic1/lf-01 is used by hasSharing-dd-help,
nat-basic1/lf-02 is used by hasSharing-dd-help,
nat-basic1/ls-02 is used by hasSharing-dd-help,
nat-basic1/neq-01 is used by hasSharing-dd-help,
nat-basic1/one is used by addarray-disjoint-nosharing,
nat-basic1/ref-1 is used by sharing-twopaths, sharing-pathex-field-self-01, sharing-pathex-field-self, hassharing-validrefs-dups, hasSharing-pathex, hasSharing-dd-help, ex-validrefs-fits-stronger, ex-validrefs-fits,
nat-basic1/z is used by sharing-twopaths, sharing-pathex-field-self-01, sharing-pathex-field-self, hassharing-validrefs-dups, hasSharing-dd-help, ex-validrefs-fits-stronger, ex-validrefs-fits, addarray-disjoint-nosharing-01, addarray-disjoint-nosharing,

Used from specification int-basic1

int-basic1/forward-pos is used by unchanged-fits, addarray-disjoint-nosharing,
int-basic1/irref is used by getbar-onlyModified-all,
int-basic1/ls-01 is used by unchanged-fits,

Used from specification refkey

Used from specification oelem

oelem/intlista/lel is used by fits-put-stronger, fits-put, addarray-disjoint-nosharing,
oelem/intlista/transitivity is used by unchanged-fits, addarray-disjoint-nosharing,

Used from specification javatype

Used from specification javavalue

Used from specification storearrays

storearrays/getByteArray-all is used by getbar-onlyModified,
storearrays/getbar-rec is used by getbar-onlyModified-all,
storearrays/putBar-rec is used by hasSharing-putbar,
storearrays/putbar-atref is used by putbar-classfield-onlymod,
storearrays/bar-empty is used by getbar-onlyModified,
storearrays/bar-empty-01 is used by getbar-onlyModified-all,
storearrays/putBar-empty is used by hasSharing-putbar,
storearrays/putbar-atref is used by putBar-onlyMod,

Used from specification list-dup

list-dup/references/c-02 is used by hassharing-validrefs-dups,
list-dup/references/dups-cons is used by nosharing-nocycle,
list-dup/references/e-01 is used by nosharing-nocycle, hassharing-validrefs-dups,
list-dup/references/rec is used by nosharing-nocycle, hassharing-validrefs-dups,

Used from specification list-data

list-data/references/elim-list is used by disjoint-def-pathex,
list-data/storekeys/elim-list-c is used by hasSharing-addobj-same, fits-rec, fits-put-other, fits-no-refval, ex-fits-validrefs-stronger, addarray-disjoint-nosharing-01, addarray-disjoint-nosharing,
list-data/references/elim-list-c is used by unchanged-put-nosharing, sharing-twopaths, sharing-pathex-field-self-01, sharing-pathex-field-self, nosharing-nocycle, hassharing-validrefs-dups, hasSharing-pathex, hasSharing-different-disjoint, hasSharing-dd-help, ex-validrefs-fits-stronger, ex-validrefs-fits, disjoint-nopathex, disjoint-nojunk-newref-subset-01, disjoint-nojunk-newref-subset, disjoint-newref-02, disjoint-newref-01, disjoint-newref, disjoint-def-fits,
list-data/storekeys/l is used by hassharing-validrefs-dups, hasSharing-dd-help, ex-validrefs-fits-stronger, ex-validrefs-fits,
list-data/references/l is used by sharing-twopaths, sharing-pathex-field-self-01, sharing-pathex-field-self, hasSharing-dd-help, ex-validrefs-fits, ex-fits-validrefs-stronger, ex-fits-validrefs, addarray-disjoint-nosharing,
list-data/javavalues/l is used by addarray-disjoint-nosharing-01,
list-data/references/size-01 is used by ex-validrefs-fits-stronger, ex-validrefs-fits,
list-data/storekeys/size-01 is used by sharing-twopaths, sharing-pathex-field-self-01, sharing-pathex-field-self, hassharing-validrefs-dups, hasSharing-dd-help, ex-validrefs-fits-stronger, ex-fits-validrefs-stronger, ex-fits-validrefs,

Used from specification specialkeys

specialkeys/len is used by hasSharing-put-index-refval,
specialkeys/length-diff is used by hasSharing-put-shortval,
specialkeys/type-03 is used by hasSharing-put-index-refval,
specialkeys/type-04 is used by fits-put-short-02, fits-put-short-01, fits-put-05-stronger, fits-put-05, fits-put-04,
specialkeys/type-09 is used by hasSharing-put-byteval-01,

Used from specification list-del

list-del/storekeys/firstN-num-rec is used by ex-validrefs-fits-stronger,
list-del/references/get-append-grt is used by hasSharing-dd-help,
list-del/javavalues/get-in is used by addarray-disjoint-nosharing-01,
list-del/references/get-last is used by hassharing-validrefs-dups,
list-del/references/get-last2 is used by sharing-twopaths, sharing-pathex-field-self-01, sharing-pathex-field-self, ex-validrefs-fits, ex-fits-validrefs,
list-del/references/get-numrec is used by hasSharing-dd-help,
list-del/references/del-n is used by disjoint-forward-field-02, disjoint-forward-array-01,
list-del/storekeys/first-all is used by hassharing-validrefs-dups, hasSharing-dd-help,
list-del/storekeys/first-all-01 is used by sharing-twopaths, sharing-pathex-field-self-01, sharing-pathex-field-self, ex-validrefs-fits,
list-del/storekeys/firstN-empty is used by ex-validrefs-fits-stronger,
list-del/storekeys/firstN-zero is used by ex-validrefs-fits-stronger,
list-del/references/get-app is used by hasSharing-dd-help,
list-del/references/get-append-grt-02 is used by hasSharing-dd-help,
list-del/references/get-append-less is used by hasSharing-dd-help,
list-del/references/get-in is used by addarray-disjoint-nosharing,
list-del/references/get-last-03 is used by hasSharing-dd-help,
list-del/references/get-nodups is used by addarray-disjoint-nosharing,
list-del/references/get-succ is used by hasSharing-dd-help, ex-validrefs-fits-stronger, ex-fits-validrefs-stronger,
list-del/references/get-zero is used by hasSharing-dd-help,
list-del/references/get-zero-01 is used by ex-validrefs-fits-stronger, ex-fits-validrefs-stronger,
list-del/references/in is used by disjoint-forward-field, disjoint-forward-array,
list-del/references/in-01 is used by disjoint-forward-field, disjoint-forward-array,
list-del/references/one is used by disjoint-forward-field-02, disjoint-forward-array-01,

Used from specification storefunsx

storefunsx/lookup-xtra is used by fits-superset, fits-subset, fits-in,

Used from specification javastore

javastore/at-other-01 is used by fits-put-short-02, fits-put-short-01, fits-put-05-stronger, fits-put-05,
javastore/at-other-16 is used by fits-put-short, fits-put-other, fits-put-03,
javastore/length-at is used by hasSharing-put-index-refval, fits-put-02-stronger, fits-put-02, fits-put-01,
javastore/look-ins is used by lookup-statfield, hasSharing-put-index-refval, fits-put-statfield, fits-put-short, fits-put-03,
javastore/type-at is used by hasSharing-put-index-refval, fits-put-02-stronger, fits-put-02, fits-put-01,

Used from specification addfuns

addfuns/add-in-09 is used by hasSharing-addobj-same,
addfuns/is-valid-ref-stronger-def is used by putbar-classfield-onlymod, hasSharing-pathex, fits-superset, fits-subset, fits-put-stronger, fits-put-statfield, fits-put-short-02, fits-put-short-01, fits-put-short, fits-put-05-stronger, fits-put-05, fits-put-04, fits-put-03, fits-put-02-stronger, fits-put-02, fits-put-01, fits-put, fits-no-refval, fits-no-reftype-01, fits-in, ex-validrefs-fits-stronger, ex-fits-validrefs-stronger, at-put-prim,
addfuns/is_obj-notin-01 is used by fits-subset,
addfuns/is_obj-type-01 is used by fits-put-05,
addfuns/is_valid_ref is used by unchanged-lookup-list-generic,
addfuns/is_valid_ref-def is used by fits-no-reftype,
addfuns/is_valid_ref-typeval is used by fits-put-short-02, fits-put-short-01, fits-put-05-stronger, fits-put-04,
addfuns/add-type is used by hasSharing-addobj-same,
addfuns/instfields-index is used by putbar-classfield-onlymod, put-switch-primval-index-index, lookup-statfield, hassharing-validrefs-dups, hasSharing-put-index-refval, fits-superset, fits-subset, fits-put-05, fits-put-02, fits-put, fits-in, ex-validrefs-fits-stronger, ex-fits-validrefs-stronger,
addfuns/instfields-index-01 is used by unchanged-lookup-list-generic, unchanged-fits, fits-put-stronger, fits-put-01,
addfuns/instfields-index-02 is used by fits-put-statfield, fits-put-short-02, fits-put-short-01, fits-put-short, fits-put-05-stronger, fits-put-04, fits-put-03, fits-put-02-stronger, fits-no-refval, fits-no-reftype-01, fits-no-reftype, disjoint-forward-field, at-put-prim,
addfuns/instfields-nodups is used by hasSharing-addobj-same,
addfuns/instfields-type is used by hasSharing-addobj-same,
addfuns/is_obj-arraytype is used by unchanged-lookup-list-generic, unchanged-fits, hassharing-validrefs-dups, fits-put-statfield, fits-put-04, fits-put-03, fits-no-reftype-01, fits-no-reftype, fits-in, ex-validrefs-fits-stronger, at-put-prim,
addfuns/is_obj-classtype is used by unchanged-lookup-list-generic, unchanged-fits, lookup-statfield, hasSharing-pathex, fits-superset, fits-subset, fits-put-stronger, fits-put-statfield, fits-put-short-02, fits-put-short-01, fits-put-short, fits-put-05-stronger, fits-put-05, fits-put-04, fits-put-03, fits-put-02-stronger, fits-put-02, fits-put-01, fits-put, fits-no-refval, fits-no-reftype-01, fits-no-reftype, fits-in, ex-fits-validrefs-stronger, at-put-prim,
addfuns/is_obj-type is used by fits-superset, fits-subset,
addfuns/is_valid_ref is used by unchanged-fits, lookup-statfield, hassharing-validrefs-dups,
addfuns/is_valid_ref-01 is used by unchanged-fits,
addfuns/is_valid_ref-array-01 is used by unchanged-lookup-list-generic, unchanged-fits, fits-put-01, disjoint-forward-array,
addfuns/is_valid_ref-isobj is used by unchanged-lookup-list-generic, lookup-statfield, hassharing-validrefs-dups, disjoint-forward-field,
addfuns/is_valid_ref-no-arraytype is used by unchanged-lookup-list-generic, fits-no-reftype-01, fits-no-reftype,
addfuns/is_valid_ref-okbytearray is used by putbar-classfield-onlymod, putBar-onlyMod,
addfuns/is_valid_ref-type is used by sharing-pathex-field-self-01, sharing-pathex-field-self,
addfuns/is_valid_ref-type-01 is used by disjoint-forward-field,
addfuns/isarray-isobj-01 is used by unchanged-lookup-list-generic, unchanged-fits, lookup-statfield, hassharing-validrefs-dups,
addfuns/stsubset-addobj is used by hasSharing-addobj-same,

Used from specification nat

nat/add-01 is used by hasSharing-dd-help,
nat/add-num-01 is used by hassharing-validrefs-dups, hasSharing-dd-help,
nat/add-num-03 is used by hasSharing-dd-help,
nat/elim-pred-c is used by ex-validrefs-fits-stronger,
nat/fle is used by addarray-disjoint-nosharing,
nat/fle-01 is used by hasSharing-dd-help,
nat/le-add is used by hasSharing-dd-help,
nat/le-ls-simp is used by ex-validrefs-fits-stronger,
nat/lels is used by hasSharing-dd-help, addarray-disjoint-nosharing-01, addarray-disjoint-nosharing,
nat/lels-01 is used by sharing-twopaths, sharing-pathex-field-self-01, sharing-pathex-field-self, hassharing-validrefs-dups, hasSharing-dd-help, ex-validrefs-fits-stronger, ex-validrefs-fits,
nat/lep-02 is used by ex-validrefs-fits-stronger,
nat/ler is used by hasSharing-dd-help,
nat/lez is used by ex-validrefs-fits-stronger,
nat/lez-01 is used by ex-validrefs-fits-stronger,
nat/pred-03 is used by hasSharing-dd-help, ex-validrefs-fits-stronger,
nat/zero is used by hasSharing-dd-help,

Used from specification list-last

list-last/references/l-02 is used by hasSharing-dd-help,
list-last/storekeys/l-02 is used by fits-no-reftype-01, fits-no-reftype,
list-last/storekeys/prefix-rec is used by fits-no-refval, ex-fits-validrefs-stronger,
list-last/storekeys/b is used by fits-no-reftype-01,
list-last/storekeys/bapp is used by fits-no-reftype-01,
list-last/storekeys/bin-01 is used by fits-no-reftype-01,
list-last/storekeys/butlast-def is used by put-switch-primval-index-field, put-switch-primval-field-index, put-switch-primval-field-field, fits-no-refval-01,
list-last/references/l is used by sharing-twopaths, sharing-pathex-field-self-01, sharing-pathex-field-self, hasSharing-pathex, hasSharing-dd-help, fits-pathex, ex-validrefs-fits, ex-fits-validrefs, disjoint-nojunk-newref-subset-01, disjoint-nojunk-newref-subset,
list-last/storekeys/l is used by fits-no-reftype-01, fits-no-reftype,
list-last/references/l-02 is used by sharing-twopaths, sharing-pathex-field-self-01, sharing-pathex-field-self, hasSharing-pathex, fits-pathex, ex-validrefs-fits, disjoint-nojunk-newref-subset-01, disjoint-nojunk-newref-subset,
list-last/references/l-in is used by disjoint-nojunk-newref-subset-01, disjoint-nojunk-newref-subset,
list-last/references/lapp-04 is used by hasSharing-dd-help,
list-last/references/last-01 is used by hasSharing-dd-help,
list-last/references/last-def is used by putbar-classfield-onlymod, hasSharing-pathex,
list-last/storekeys/last-elim is used by put-switch-primval-index-index, put-switch-primval-index-field, put-switch-primval-field-index, put-switch-primval-field-field, fits-no-refval,
list-last/references/last-elim is used by hasSharing-pathex, hasSharing-dd-help,
list-last/references/lin-01 is used by hasSharing-dd-help, fits-pathex, disjoint-nojunk-newref-subset-01, disjoint-nojunk-newref-subset,
list-last/storekeys/lin-02 is used by fits-no-reftype-01, fits-no-reftype,
list-last/storekeys/postifx-app-03 is used by hasSharing-put-index-refval,
list-last/storekeys/prefix-app-05 is used by sharing-twopaths,
list-last/storekeys/prefix-empty is used by hasSharing-put-index-refval, fits-put-other, fits-no-refval, ex-fits-validrefs-stronger,
list-last/storekeys/prefix-nil is used by fits-no-refval, ex-fits-validrefs-stronger,
list-last/storekeys/prefix-one is used by hasSharing-put-index-refval, fits-put-other,
list-last/storekeys/prefix-one-01 is used by fits-put-other,
list-last/storekeys/prefix-rec-03 is used by fits-put-other,
list-last/storekeys/prefix-self is used by fits-no-refval-01, ex-fits-validrefs,

Used from specification nat-basic2

nat-basic2/a is used by sharing-twopaths, sharing-pathex-field-self-01, sharing-pathex-field-self, hassharing-validrefs-dups, hasSharing-pathex, hasSharing-dd-help, ex-validrefs-fits-stronger, ex-validrefs-fits, ex-fits-validrefs-stronger,
nat-basic2/c is used by sharing-twopaths, sharing-pathex-field-self-01, sharing-pathex-field-self, hassharing-validrefs-dups, hasSharing-pathex, hasSharing-dd-help, ex-validrefs-fits-stronger, ex-validrefs-fits, ex-fits-validrefs-stronger,
nat-basic2/eq is used by hasSharing-dd-help,
nat-basic2/eq-01 is used by sharing-twopaths, sharing-pathex-field-self-01, sharing-pathex-field-self, hasSharing-dd-help, ex-validrefs-fits-stronger, ex-validrefs-fits, ex-fits-validrefs-stronger,
nat-basic2/eqs is used by hasSharing-dd-help,
nat-basic2/l is used by hasSharing-pathex,
nat-basic2/l-01 is used by hasSharing-dd-help,
nat-basic2/l-02 is used by hasSharing-dd-help,
nat-basic2/oz is used by hassharing-validrefs-dups, hasSharing-dd-help, ex-validrefs-fits-stronger,
nat-basic2/s is used by hassharing-validrefs-dups, hasSharing-pathex, hasSharing-dd-help, ex-validrefs-fits-stronger,
nat-basic2/z-01 is used by hasSharing-dd-help,