[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/Extension is used by putBar-rew, get-eqex-03, copy-succ,
store/javastore/Subset is used by stsub-copy, putarray-subset-new-01,
store/javastore/rew is used by putar-rew, putByteArray-put-switch, putBar-rew-01, putBar-lastrec, putArray-put-switch-02, putArray-put-switch-01, putArray-put-switch, putArray-put, putAr-lastrec,
store/javastore/subset-elem-eq is used by getintarray-subset, getbytearray-subset, getarray-subset,
store/javastore/At-other is used by putbar-refval,
store/javastore/At-same is used by putbar-refval, putAr-get-other-01, putAr-get-other, getbar-putbar-same-01,
store/javastore/In-insert is used by putar-inother, putar-in-02, putar-in-01, putBar-rew, putArray-in, isarray-02, is_arrayref-03, is_arrayref-02, is_arrayref-01, copy-succ, copy-in-lower, copy-in-between, arrayref-02, arrayref-01,
store/javastore/insins is used by putbar-put-override, putar-rew, putByteArray-put-switch, putArray-put-switch-02, putArray-put-switch,
store/javastore/notmemlookup is used by getbytearray-subset, getarray-subset, get-eqex-03,
store/javastore/subset-elem-eq-02 is used by putarray-subset-new-01,
store/javastore/superset-elem-in-01 is used by putarray-subset-new-01,

Used from specification list

list/javavalues/Cons is used by putArray-put,
list/javavalues/Noassoc is used by putAr-lastrec,
list/javavalues/One is used by putArray-one, putAr-lastrec,
list/bytelist/a is used by putByteArray-append,
list/javavalues/c is used by putArray-put, putArray-one, putAr-lastrec,
list/javavalues/first-01 is used by get-first,
list/javavalues/firsteq-01 is used by get-rest,
list/bytelist/len-01 is used by getbar-appeq, bar-neq-soffset, bar-neq,
list/javavalues/len-05 is used by putArray-put,
list/javavalues/Last is used by putar-getar, putArray-put, getintarray-rec-last, getbar-lastrec, getarray-put=set, getarray-put-03, getarray-put-02, getarray-offset, getarray-in-01, getArray-rec-01, get-rest, get-rec-01, get-put-01, get-length, get-get, get-first, get-empty, get-del-01, get-alleq, at=get-offset, at=get, Comp-get-01,
list/intlista/Last is used by getintarray-rec-last, getintarray-one, getintarray-max-rec-01, getintarray-max-rec, getintarray-in-02,
list/bytelist/Last is used by getbar-lastrec,
list/intlista/Nil is used by getintarray-rec-last, getintarray-one,
list/javavalues/Nil is used by putar-getar, putArray-put, putArray-append, putAr-lastrec, getarray-put=set, getarray-offset, getArray-rec-01, get-first, bytevalues,
list/storekeys/Nil is used by getbar-put-01,
list/bytelist/Nil is used by putByteArray-append, putBar-lastrec, getbar-lastrec, bytevalues,
list/javavalues/a is used by putarray-field, putar-rew, putar-inref, putar-inother, putar-infs, putar-in-02, putar-in-01, putar-in, putar-getar-02, putar-getar-01, putar-getar, putar-atref, putar-atother, putar-atfs, putar-at, putBar-rec, putArray-put-switch-02, putArray-put-switch-01, putArray-put-switch, putArray-put, putArray-in, putArray-append, putAr-lastrec, putAr-get-other-01, putAr-get-other, getintarray-rec-last, getintarray-rec-first, getbar-rec, getbar-lastrec, getbar-anyrec, getbar-5rec, getbar-3rec, getbar-2rec, getarray-union-03, getarray-union, getarray-put=set, getarray-put-03, getarray-put-02, getarray-put-01, getarray-offset-02, getarray-offset-01, getarray-offset, getarray-in-01, getArray-rec-01, get-sublist, get-rest, get-rec-01, get-put-01, get-length, get-first, get-empty, get-del-01, get-alleq, extension, bytevalues, bar-restn, bar-neq, Comp-get-01,
list/bytelist/a is used by putbar-refval, putbar-put-override, putbar-override, putbar-getbar-le, putByteArray-put-switch-01, putByteArray-put-switch, putByteArray-append, putBar-unrec, putBar-rew-01, putBar-rec, putBar-lastrec, pubBar-init, getbar-restn-01, getbar-rec, getbar-putbar-same-01, getbar-one, getbar-lastrec, getbar-appeq-01, getbar-anyrec, getbar-5rec, getbar-3rec, getbar-2rec, getba-neq-01, getba-eq, getarray-putbar-01, getarray-putbar, getar-putbar-01, get-put-01, extension, bytevalues, bar-zero, bar-restn, bar-len-01, bar-len,
list/intlista/a is used by getintarray-rec-last, getintarray-rec-first, getintarray-one, getintarray-in-02, getintarray-empty-02,
list/storekeys/a is used by getbar-put-01,
list/javavalues/app is used by putar-getar, getarray-offset-01, getarray-offset, get-rec-01,
list/bytelist/app is used by getbar-one, getba-eq,
list/intlista/app-01 is used by getintarray-rec-last, getintarray-rec-first,
list/bytelist/app-01 is used by putbar-getbar-le, getbar-rec, getbar-putbar-same-01, getbar-lastrec, getbar-anyrec, getbar-5rec, getbar-3rec, getbar-2rec, getba-eq, bytevalues,
list/javavalues/app-01 is used by putar-getar-01, putar-getar, getarray-union-03, getarray-union, getarray-put-01, getarray-offset-02, getarray-offset, getArray-rec-01, get-sublist, get-rec-01,
list/intlista/app-02-ant is used by getintarray-empty-02,
list/bytelist/app-02-ant is used by putbar-refval, putbar-put-override, putbar-override, putbar-getbar-le, putByteArray-put-switch-01, putByteArray-put-switch, putByteArray-append, putBar-unrec, putBar-rew-01, putBar-lastrec, pubBar-init, getbar-putbar-same-01, getarray-putbar-01, getarray-putbar, getar-putbar-01, extension, bar-zero, bar-len-01, bar-len,
list/javavalues/app-02-ant is used by putar-in, get-empty,
list/javavalues/app-03 is used by getarray-put=set, getarray-put-03, getarray-put-02, getarray-offset, get-rest, get-rec-01, get-del-01,
list/bytelist/app-03 is used by get-put-01,
list/bytelist/app-05 is used by getbar-restn-01,
list/javavalues/app-06 is used by get-alleq, Comp-get-01,
list/intlista/c is used by getintarray-rec-first, getintarray-empty-02,
list/bytelist/c is used by putbar-refval, putbar-put-override, putbar-override, putbar-getbar-le, putByteArray-put-switch-01, putByteArray-put-switch, putByteArray-append, putBar-rew-01, putBar-rec, putBar-lastrec, pubBar-init, getbar-rec, getbar-putbar-same-01, getbar-putbar, getbar-one, getbar-5rec, getbar-3rec, getbar-2rec, getba-neq-01, getba-eq, getarray-putbar-01, getarray-putbar, getar-putbar-01, getar-putbar, extension, bytevalues, bar-zero, bar-restn,
list/javavalues/c is used by putarray-field, putar-rew, putar-inref, putar-inother, putar-infs, putar-in-02, putar-in-01, putar-in, putar-getar-02, putar-getar-01, putar-getar, putar-atref, putar-atother, putar-atfs, putar-at, putArray-put-switch-02, putArray-put-switch-01, putArray-put-switch, putArray-in, putArray-append, putAr-get-other-01, putAr-get-other, get-sublist, get-rest, bytevalues,
list/bytelist/c-03 is used by bar-len-01, bar-len,
list/intlista/c-04 is used by getintarray-rec-last, getintarray-one,
list/javavalues/c-04 is used by putar-getar, getarray-put=set, getarray-put-03, getarray-put-02, getarray-offset, getArray-rec-01, get-rec-01, get-del-01, get-alleq, Comp-get-01,
list/bytelist/c-04 is used by getbytearray-one, getbar-one, getbar-lastrec, getba-eq, get-put-01,
list/javavalues/c-06 is used by get-rest,
list/bytelist/c-06 is used by getba-neq-01, extension,
list/bytelist/c-07 is used by putbar-refval, putbar-put-override, putbar-override, putbar-getbar-le, putByteArray-put-switch-01, putByteArray-put-switch, putByteArray-append, putBar-unrec, putBar-rew-01, putBar-lastrec, pubBar-init, getbar-putbar-same-01, getarray-putbar-01, getarray-putbar, getar-putbar-01, bar-restn,
list/bytelist/c-08 is used by putbar-refval, putbar-put-override, putbar-override, putbar-getbar-le, putByteArray-put-switch-01, putByteArray-put-switch, putByteArray-append, putBar-unrec, putBar-rew-01, putBar-lastrec, pubBar-init, getbar-putbar-same-01, getarray-putbar-01, getarray-putbar, getar-putbar-01,
list/intlista/e is used by getintarray-empty-02,
list/bytelist/e is used by putbar-refval, putbar-put-override, putbar-override, putbar-getbar-le, putByteArray-put-switch-01, putByteArray-put-switch, putByteArray-append, putBar-unrec, putBar-rew-01, putBar-one, putBar-lastrec, pubBar-init, getbar-putbar-same-01, getarray-putbar-01, getarray-putbar, getar-putbar-01, extension, bar-zero, bar-len-01, bar-len,
list/javavalues/e is used by putar-in, get-empty,
list/bytelist/e-01 is used by putbar-refval, putbar-put-override, putbar-override, putbar-getbar-le, putByteArray-put-switch-01, putByteArray-put-switch, putByteArray-append, putBar-unrec, putBar-rew-01, putBar-rec, putBar-lastrec, pubBar-init, getbar-putbar-same-01, getarray-putbar-01, getarray-putbar, getar-putbar-01, extension,
list/bytelist/first is used by putBar-one,
list/javavalues/first is used by get-first,
list/javavalues/in-08 is used by get-rest,
list/bytelist/in-13 is used by bar-len-01, bar-len,
list/bytelist/in-14 is used by getba-neq-01, bar-len-01, bar-len,
list/javavalues/in-14 is used by get-rest,
list/javavalues/in-15 is used by putar-getar, get-rest,
list/javavalues/in-17 is used by getarray-in-01, get-rest,
list/intlista/in-17 is used by getintarray-in-02,
list/bytelist/in-17 is used by getba-neq-01,
list/intlista/in-append is used by getintarray-in-02,
list/javavalues/in-append is used by getarray-in-01, get-rest,
list/bytelist/in-append is used by getba-neq-01,
list/intlista/in-empty is used by getintarray-in-02,
list/javavalues/len is used by putar-rew, putar-inother, putar-in-02, putar-getar, putar-atother, putar-at, putArray-put-switch, putArray-in, putArray-append, putAr-lastrec, putAr-get-other-01, putAr-get-other, get-length,
list/bytelist/len is used by putbar-put-override, putbar-override, putbar-getbar-le, putByteArray-append, putBar-lastrec, getbar-putbar-same-01,
list/javavalues/len-02 is used by putar-rew, putar-inother, putar-in-02, putar-getar, putar-atother, putar-at, putArray-put-switch, putArray-in, putArray-append, putAr-lastrec, putAr-get-other-01, putAr-get-other, get-length,
list/bytelist/len-02 is used by putbar-put-override, putbar-override, putbar-getbar-le, putByteArray-append, putBar-lastrec, getbar-putbar-same-01,
list/bytelist/rest is used by putBar-one,
list/javavalues/rest is used by get-rest,

Used from specification storefuns

storefuns/init-existing is used by putbytearray-init,
storefuns/instore-02 is used by putar-in,
storefuns/put-last-rec is used by getbar-put-01,
storefuns/in-del is used by isarrayref-del, get-eqex-03,
storefuns/initdone-02 is used by pubBar-init, copy-init,
storefuns/initerror-02 is used by copy-init-02,
storefuns/initundone-02 is used by copy-init-01,
storefuns/instore-01 is used by stsub-copy, putarray-subset-new-01, putar-inother, putar-in-02, putArray-in, isarrayref-mod, getintarray-subset, getbar-union-01, getarray-union-03, getarray-union-02, getarray-union-01, getarray-union, copy-in-lower,
storefuns/instore-02 is used by copy-in-02, copy-in-01,
storefuns/look-del is used by get-eqex-03, get-del-01, get-del,
storefuns/newref-01 is used by stsub-copy,
storefuns/newref-02 is used by copy-new,
storefuns/newref-03 is used by stsub-copy,
storefuns/put-one is used by getbar-put-01,
storefuns/refin is used by putar-inother, putar-in-02,

Used from specification int-basic2

Used from specification valuesfuns

valuesfuns/bytevals-at is used by getar-at, bar-at,
valuesfuns/intvalues-at is used by getintarray-in, getintarray-at,
valuesfuns/mkjavavalues-restn is used by getbar-restn-04,
valuesfuns/vals-at is used by putbar-byte,
valuesfuns/bytevals-inj is used by getarray=getbytearray,
valuesfuns/bytevalues-empty is used by getbar-lastrec, get-put-01, extension, bytevalues, bar-len-01, bar-len, bar-empty-01,
valuesfuns/bytevalues-empty-01 is used by getbar-len-01, extension, bar-empty,
valuesfuns/bytevalues-len is used by getbytearray-putbar-length, getbar-len, bar-neq, bar-length, bar-len-02,
valuesfuns/bytevalues-one is used by getbar-lastrec, get-put-01, bar-len-01, bar-len,
valuesfuns/bytevalues-rec is used by getbar-rec, getbar-5rec, getbar-3rec, getbar-2rec, extension, bytevalues, bar-restn,
valuesfuns/intvalues-append is used by getintarray-rec-last,
valuesfuns/intvalues-empty is used by getintarray-rec-last, getintarray-empty,
valuesfuns/intvalues-empty-01 is used by getintarray-empty-01,
valuesfuns/intvalues-len is used by getintarray-length, getintarray-in, getintarray-at,
valuesfuns/intvalues-one is used by getintarray-rec-last,
valuesfuns/intvalues-rec is used by getintarray-rec-first,
valuesfuns/mkjava-bvs is used by putbar-getbar,
valuesfuns/mkjava-empty is used by putbar-in,
valuesfuns/mkjava-len is used by putbar-inother-01, putbar-inother, putbar-in-02, putbar-getbar, putbar-byte, putbar-atother-01, putbar-atother, putBar-in,
valuesfuns/mkvalsb-empty is used by putBar-empty,
valuesfuns/mkvalsb-rec is used by putBar-rec,

Used from specification int-div

int-div/mod-pred is used by copy-bet-bet,
int-div/mod-pred-01 is used by copy-bet-bet,
int-div/mod-zero-05 is used by copy-bet-bet,
int-div/mod-same is used by copy-bet-bet,
int-div/mod-zero-04 is used by copy-bet-bet,

Used from specification intnat

intnat/num-i2n-le-02 is used by getarray-in,
intnat/num-i2n-ls-02 is used by getintarray-at, getbytearray-subset, getarray-get,
intnat/num-n2i-ls-02 is used by putbar-byte,
intnat/num-n2i-ls-06 is used by getintarray-in, getarray-in,
intnat/sub is used by getbar-restn,
intnat/Nat2int-zero is used by get-get,
intnat/abs-eq is used by getintarray-length-01, getintarray-length, getbytearray-subset, getbytearray-putbar-length, getbytearray-put-index-length, getbar-length-01, getbar-appeq, getarray-put=set, getarray-length-01, getarray-length, get-length-04, bar-neq-soffset, bar-neq, bar-length, bar-len-02, at=get-offset, at=get,
intnat/abs-pred is used by getba-neq-01, getba-eq, getarray-union-03, copy-upper, copy-new, copy-lower, copy-init-02, copy-init-01, copy-init, copy-infs, copy-in-upper, copy-in-lower, copy-in-between, copy-in-02, copy-in-01, copy-in, copy-ident, copy-between, copy-bet-up, copy-bet-low, copy-bet-bet, copy-atfield, copy-at, comp-same,
intnat/abs-succ-03 is used by getarray-put=set, getarray-put-03, getarray-put-02, getarray-in-01, get-rest, get-rec-01, get-length, get-get, get-first, get-del-01, get-alleq, at=get-offset, at=get, Comp-get-01,
intnat/abs-zero is used by putbar-getbar-le, putAr-get-other-01, putAr-get-other, getintarray-in, getintarray-at, getbytearray-subset, getbar-restn, getbar-length, getbar-len-03, getarray-in, getarray-get, get-get,
intnat/add-nonneg-int-to-nat is used by getbar-restn-04,
intnat/i2i-pos is used by getarray-in, get-get,
intnat/i2i-pos-01 is used by getintarray-in, getbar-len, getarray-in,
intnat/ini2-abs is used by Comp-get,
intnat/inj is used by putbar-getbar,
intnat/inni-le is used by getar-at, bar-at,
intnat/inni-ls is used by getbar-restn, get-get,
intnat/labs is used by getintarray-in-02, getintarray-in, getarray-union, getarray-put=set, getarray-put-03, getarray-put-02, getarray-put-01, getarray-offset, getarray-in-01, get-rest, get-rec-01, get-put-01, get-length, get-get, get-first, get-del-01, get-alleq, extension, at=get-offset, at=get, Comp-get-01,
intnat/labs-01 is used by getintarray-in,
intnat/le is used by putAr-lastrec,
intnat/minus-one is used by putar-getar,
intnat/n2i-add is used by putbar-put-override, putbar-override, putbar-getbar-le, putar-rew, putar-inother, putar-in-02, putar-getar, putar-atother, putar-at, putByteArray-append, putBar-lastrec, putArray-put-switch, putArray-put, putArray-in, putArray-append, putAr-lastrec, getbar-putbar-same-01, get-sublist, bar-restn,
intnat/n2n is used by getbar-restn, get-get, bar-len-03,
intnat/nat2int is used by putbar-put-override, putbar-getbar-le, putar-at, putByteArray-append, putArray-in, getbar-restn-01, getbar-restn, getbar-putbar-same-01, get-sublist, bar-sublist, bar-len-03,
intnat/nat2int-02 is used by putar-getar, get-get,
intnat/nat2int-07 is used by putBar-lastrec, putArray-put, putAr-lastrec,
intnat/nat2int-08 is used by putbar-override, putar-rew, putar-inother, putar-in-02, putar-atother, putByteArray-append, putBar-lastrec, putArray-put-switch, putArray-put, putArray-in, putAr-lastrec, getintarray-in, getbytearray-subset, getbar-restn, getarray-in, bar-sublist,
intnat/nat2int-14 is used by get-get,
intnat/num-i2n-le-02 is used by getarray-offset, get-put-01,
intnat/num-n2i-eq is used by putar-getar,
intnat/num-n2i-ls-02 is used by putbytearray-in, putbar-put-override, putbar-override, putbar-byte, putar-rew, putar-getar, putar-at, getintarray-in, getintarray-at, getbytearray-subset, getarray-in, getarray-get,
intnat/num-n2i-ls-07 is used by putbar-getbar-le,
intnat/pos-add is used by get-sublist,
intnat/pos-int is used by getar-at, get-sublist, get-rest-01, get-length-04, bar-restn, bar-at-01, bar-at,
intnat/rax is used by putbar-getbar-le, putar-at, get-length,
intnat/rax-01 is used by getarray-offset, get-put-01,
intnat/rax-04 is used by putAr-get-other-01, putAr-get-other, getintarray-in-02, getarray-union, getarray-put-01, extension,

Used from specification int-abs

int-abs/Abs-pos is used by copy-bet-bet,
int-abs/numadd-01 is used by copy-lower, copy-in-lower, copy-between, copy-bet-up, copy-bet-low, copy-bet-bet,
int-abs/sub-add-08 is used by copy-bet-low,
int-abs/Sub-def is used by getba-neq-01, getba-eq, getarray-union-03, getarray-offset, get-ateq, extension, copy-bet-up, copy-bet-low, copy-bet-bet, comp-same, bar-neq-soffset,
int-abs/abs is used by getarray-offset, get-put-01,
int-abs/abs-03 is used by copy-bet-bet,
int-abs/abs-06 is used by copy-bet-bet,
int-abs/abs-16 is used by getintarray-in, getarray-put=set, getarray-put-03, getarray-put-02, getarray-in-01, get-rest, get-rec-01, get-length, get-get, get-first, get-del-01, get-alleq, at=get-offset, at=get, Comp-get-01,
int-abs/absle is used by getintarray-in-02, getintarray-in, getarray-union, getarray-put=set, getarray-put-01, extension, at=get-offset, at=get, Comp-get,
int-abs/anti is used by putbar-put-override, putbar-getbar-le, putar-getar, putArray-in, getintarray-rec-last, getintarray-in-02, getintarray-empty-02, getbar-lastrec, getba-neq-01, getba-eq, getarray-put=set, getarray-offset, getarray-in-01, getArray-rec-01, get-rest, get-rec-01, get-length-01, get-get, get-first, get-alleq, extension, copy-in-between, copy-bet-low, comp-same, bar-zero, at=get-offset, at=get, arrayComp-02, arrayComp-01,
int-abs/bet is used by getba-neq-01, getarray-put=set, getarray-put-03, getarray-put-02, getarray-offset, getarray-in-01, get-rest, get-rec-01, get-put-01, get-length, get-get, get-first, get-empty, get-del-01, get-alleq, copy-in-between, bar-len, at=get-offset, at=get, Comp-get-01,
int-abs/bet-01 is used by getarray-put=set, extension, at=get-offset, at=get, arrayComp-02,
int-abs/elim-sub is used by putbar-getbar-le, putbar-byte, putar-getar-01, putar-getar, putar-at, putBar-unrec, getintarray-rec-last, getintarray-rec-first, getintarray-put-upper-02, getintarray-in-02, getbar-restn-04, getbar-restn-01, getbar-rec, getbar-lastrec, getbar-anyrec, getbar-5rec, getbar-3rec, getbar-2rec, getarray-union, getarray-put=set, getarray-put-03, getarray-put-02, getarray-put-01, getarray-offset-02, getarray-in-01, getArray-rec-01, get-sublist, get-rest, get-rec-01, get-length, get-get, get-first, get-del-01, get-alleq, extension, comp-same, bar-sublist, bar-neq, at=get-offset, at=get, Comp-get-01,
int-abs/forward-le is used by isarray-02, getintarray-in, getintarray-at, getbytearray-subset, getbar-5rec, getbar-3rec, getbar-2rec, getarray-union-02, getarray-offset-01, getarray-offset, getarray-in, getarray-get, copy-bet-bet, comp-same,
int-abs/forward-le-01 is used by putbar-put-override, putbar-override, putbar-getbar-le, putbar-byte, putar-getar-01, putar-getar, putar-at, putByteArray-put-switch-01, putByteArray-put-switch, putByteArray-append, putArray-put-switch, putArray-put, putAr-get-other-01, putAr-get-other, isarrayref-putbar-other, isarrayref-mod, isarrayref-del, isarray-02, isarray, is_arrayref-03, is_arrayref-02, is_arrayref-01, getintarray-subset-01, getintarray-subset, getintarray-rec-last, getintarray-rec-first, getintarray-put-other-02, getintarray-length-01, getintarray-length, getintarray-in-02, getintarray-in-01, getintarray-in, getbytearray-subset, getbar-restn-04, getbar-restn-01, getbar-rec, getbar-mod-01, getbar-length, getbar-len-03, getbar-len, getbar-lastrec, getbar-anyrec, getbar-5rec, getbar-3rec, getbar-2rec, getba-neq-01, getba-neq, getba-eq, getarray-union-03, getarray-union-02, getarray-union-01, getarray-union, getarray-superset, getarray-subset, getarray-put=set, getarray-put-01, getarray-offset-02, getarray-offset-01, getarray-offset, getarray-length, getarray-in-01, getarray-in, getArray-rec-01, get-sublist, get-rest, get-rec-01, get-length-01, get-eqex-03, get-alleq, extension-01, extension, copy-succ, copy-at-01, copy-arref, comp-same, comp-next, comp-copy, bar-sublist, bar-restn, bar-neq-soffset, bar-neq-same, bar-neq, bar-length, at=get-offset, at=get, arrayref-02, arrayref-01, arrayref, arrayComp-08, arrayComp-07, arrayComp-05, arrayComp-04, arrayComp-02, arrayComp-01, Comp-get-01,
int-abs/forward-le-02 is used by getintarray-empty-01, getbytearray-subset, getbar-restn, getbar-len-01, getarray-in, comp-same,
int-abs/forward-le-04 is used by getintarray-in-02, getintarray-empty-02, get-alleq, extension, copy-in-02, copy-in-01, bar-zero,
int-abs/forward-le-05 is used by putbar-put-override, putbar-getbar-le, putar-getar-01, putar-getar, putar-at, putByteArray-put-switch, isarrayref-putbar-other, isarrayref-mod, isarrayref-del, isarray-02, isarray, is_arrayref-03, is_arrayref-02, is_arrayref-01, getintarray-zero, getintarray-subset-01, getintarray-subset, getintarray-rec-last, getintarray-rec-first, getintarray-max-rec-01, getintarray-max-rec, getintarray-in-02, getintarray-in-01, getintarray-in, getintarray-at, getbytearray-subset, getbytearray-length-zero, getbar-rec, getbar-mod-01, getbar-lastrec, getba-neq-01, getba-neq, getba-eq, getarray-union-03, getarray-union-02, getarray-union-01, getarray-superset, getarray-subset, getarray-put=set, getarray-put-03, getarray-put-02, getarray-put-01, getarray-offset, getarray-in-01, getarray-in, getarray-get, getArray-rec-01, get-rest, get-rec-01, get-put-01, get-length, get-eqex-03, get-del-01, get-alleq, extension-01, extension, copy-upper, copy-lower, copy-in-upper, copy-in-lower, copy-in-between, copy-ident, copy-between, copy-bet-up, copy-bet-low, copy-bet-bet, copy-at-01, copy-arref, comp-same, comp-next, comp-copy, bar-len, at=get-offset, at=get, arrayref-02, arrayref-01, arrayref, arrayComp-08, arrayComp-07, arrayComp-05, arrayComp-04, arrayComp-03, arrayComp-01, Comp-get-01,
int-abs/forward-lele is used by putbar-put-override, putbar-getbar-le, putar-at, putArray-in, getbar-length-01, getbar-anyrec, getarray-offset, getarray-in-01, get-alleq, extension, copy-bet-up, copy-bet-low, comp-copy, bar-neq-soffset, at=get-offset, at=get,
int-abs/forward-lels is used by putbytearray-in, putbar-put-override, putbar-override, putbar-byte, isarray-02, getintarray-in, getbar-restn, getba-neq-01, getarray-put=set, getarray-in-01, getarray-in, get-puteq, get-ateq, copy-in-between, copy-between, copy-bet-up, copy-bet-low, copy-bet-bet, copy-arref, comp-same, bar-sublist, bar-neq-soffset, at=get-offset, arrayref-02, arrayref-01, Comp-get-02, Comp-get,
int-abs/forward-lsle is used by putbar-put-override, putbar-override, putbar-getbar-le, putar-rew, putar-at, putArray-put, isarray-02, getbytearray-subset, getarray-union-03, getarray-union-02, getarray-offset, get-get, get-alleq, copy-upper, copy-in-upper, copy-bet-up, copy-bet-bet, comp-same, at=get,
int-abs/le-add is used by putbar-getbar-le, putar-getar, putar-at, putBar-lastrec, putArray-put, putAr-lastrec, getbytearray-subset, getarray-subset, getarray-put=set, bar-sublist,
int-abs/lels is used by putbar-put-override, putbar-override, putbar-inother-01, putbar-inother, putbar-in-02, putbar-byte, putbar-atother-01, putbar-atother, putarray-subset-new-01, putar-rew, putar-inother, putar-in-02, putar-getar-01, putar-getar, putar-atother, putar-at, putByteArray-put-switch, putBar-rew, putBar-in, putArray-in, isarrayref-putbar-other, isarrayref-put, isarrayref-mod, isarrayref-del, isarray-02, isarray, is_arrayref-03, is_arrayref-02, is_arrayref-01, getintarray-subset-01, getintarray-subset, getintarray-rec-last, getintarray-put-other-02, getintarray-in-02, getintarray-in-01, getintarray-in, getintarray-empty-02, getintarray-at, getbytearray-subset, getbytearray-put-index-length, getbar-put-other, getbar-put-02, getbar-put, getbar-lastrec, getba-neq-01, getba-neq, getba-eq, getarray-union-03, getarray-union-02, getarray-union-01, getarray-union, getarray-superset, getarray-subset, getarray-put=set, getarray-put-05, getarray-put-03, getarray-put-02, getarray-put-01, getarray-offset, getarray-in-01, getarray-in, getarray-get, getArray-rec-01, get-rest, get-rec-01, get-puteq, get-put-01, get-length-01, get-length, get-get, get-first, get-empty, get-del-01, get-ateq-01, get-ateq, get-alleq, extension-01, extension, copy-upper, copy-succ, copy-new, copy-lower, copy-init-02, copy-init-01, copy-init, copy-infs, copy-in-upper, copy-in-lower, copy-in-between, copy-in-02, copy-in-01, copy-in, copy-ident, copy-between, copy-bet-up, copy-bet-low, copy-bet-bet, copy-atfield, copy-at-01, copy-at, copy-arref, comp-same, comp-next, comp-copy, bar-zero, bar-length, at=get-offset, at=get, arrayref-02, arrayref-01, arrayref, arrayComp-08, arrayComp-07, arrayComp-05, arrayComp-04, arrayComp-03, arrayComp-02, arrayComp-01, Comp-get-02, Comp-get-01, Comp-get,
int-abs/lels-01 is used by putbar-put-override, putbar-override, putbar-inother-01, putbar-inother, putbar-in-02, putbar-getbar-le, putbar-byte, putbar-atother-01, putbar-atother, putarray-subset-new-01, putar-rew, putar-inother, putar-in-02, putar-getar-01, putar-getar, putar-atother, putar-at, putByteArray-put-switch-01, putByteArray-put-switch, putByteArray-append, putBar-rew, putBar-lastrec, putBar-in, putArray-put-switch, putArray-put, putArray-in, putAr-lastrec, putAr-get-other-01, putAr-get-other, isarrayref-putbar-other, isarrayref-put, isarrayref-mod, isarrayref-del, isarray-03, isarray-02, isarray, is_arrayref-03, is_arrayref-02, is_arrayref-01, getintarray-zero, getintarray-subset-01, getintarray-subset, getintarray-rec-first, getintarray-put-upper-02, getintarray-put-upper-01, getintarray-put-other-02, getintarray-in-02, getintarray-in-01, getintarray-in, getintarray-empty-02, getintarray-empty-01, getintarray-at, getbytearray-subset, getbytearray-putbar-length, getbytearray-put-index-length, getbytearray-length-zero, getbar-restn-04, getbar-restn-03, getbar-restn-02, getbar-restn-01, getbar-restn, getbar-rec, getbar-putbar-same-01, getbar-put-02, getbar-mod-01, getbar-len-02, getbar-len-01, getbar-anyrec, getbar-5rec, getbar-3rec, getbar-2rec, getba-neq-01, getba-neq, getba-eq, getarray-union-03, getarray-union-02, getarray-union-01, getarray-union, getarray-superset, getarray-subset, getarray-put=set, getarray-put-03, getarray-put-02, getarray-put-01, getarray-offset-02, getarray-offset-01, getarray-offset, getarray-in-01, getarray-in, getarray-get, get-zero, get-sublist, get-rest, get-rec-01, get-puteq, get-put-01, get-length-02, get-empty, get-del-01, get-ateq-01, get-ateq, get-alleq, extension-01, extension, copy-upper-01, copy-upper, copy-succ, copy-lower, copy-in-upper-01, copy-in-upper, copy-in-lower, copy-in-between, copy-between, copy-bet-up, copy-bet-low, copy-bet-bet, copy-at-01, copy-arref, comp-same, comp-next, comp-copy, bar-zero, bar-sublist, bar-restn, bar-neq-soffset, bar-neq-same, bar-neq, bar-len, bar-firstn, bar-eq-sub, bar-empty, at=get-offset, at=get, arrayref-02, arrayref-01, arrayref, arrayComp-08, arrayComp-07, arrayComp-05, arrayComp-04, arrayComp-03, arrayComp-02, arrayComp-01, Comp-get-02, Comp-get-01,
int-abs/lels-02 is used by putbar-put-override, putbar-getbar-le, putar-at, putAr-get-other-01, putAr-get-other, getintarray-in, getbytearray-subset, getba-eq, getarray-put=set, getarray-offset, getarray-in, get-rest, get-rec-01, extension, copy-in-between, copy-bet-bet, comp-same, comp-next,
int-abs/lels-03 is used by putbar-override, putbar-inother-01, putbar-inother, putbar-in-02, putbar-byte, putbar-atother-01, putbar-atother, putBar-rew, putBar-in, putArray-put-switch, putArray-in, isarrayref-putbar-other, isarrayref-mod, isarrayref-del, isarray-02, isarray, is_arrayref-03, is_arrayref-02, is_arrayref-01, getintarray-subset-01, getintarray-subset, getintarray-max-rec-01, getintarray-max-rec, getintarray-in-01, getintarray-in, getintarray-empty-02, getbytearray-subset, getba-neq-01, getba-neq, getba-eq, getarray-union-03, getarray-union-02, getarray-union-01, getarray-superset, getarray-subset, getarray-put-03, getarray-put-02, getarray-in-01, getarray-in, get-sublist, get-puteq, get-put-01, get-del-01, get-ateq-01, get-ateq, get-alleq, extension-01, extension, copy-upper, copy-new, copy-lower, copy-init-02, copy-init-01, copy-init, copy-infs, copy-in-upper, copy-in-lower, copy-in-between, copy-in-02, copy-in-01, copy-in, copy-ident, copy-between, copy-bet-up, copy-bet-low, copy-bet-bet, copy-atfield, copy-at-01, copy-at, copy-arref, comp-same, comp-copy, bar-zero, bar-restn, arrayref-02, arrayref-01, arrayref, arrayComp-08, arrayComp-07, arrayComp-06, arrayComp-05, arrayComp-04, arrayComp-03, Comp-get-02, Comp-get-01, Comp-get,
int-abs/lels-04 is used by putbar-put-override, putbar-override, putbar-inother-01, putbar-inother, putbar-in-02, putbar-getbar-le, putbar-byte, putbar-atother-01, putbar-atother, putar-rew, putar-inother, putar-in-02, putar-getar-01, putar-atother, putar-at, putByteArray-put-switch-01, putByteArray-put-switch, putByteArray-append, putBar-rew, putBar-in, putArray-put-switch, putArray-in, isarrayref-putbar-other, isarrayref-mod, isarrayref-del, isarray-02, isarray, is_arrayref-03, is_arrayref-02, is_arrayref-01, getintarray-subset-01, getintarray-subset, getintarray-rec-first, getintarray-put-upper-01, getintarray-in-02, getintarray-in-01, getbar-restn-04, getbar-restn-03, getbar-restn-02, getbar-restn-01, getbar-restn, getbar-rec, getbar-mod-01, getbar-length, getbar-len-03, getbar-len-02, getbar-anyrec, getbar-5rec, getbar-3rec, getbar-2rec, getba-neq-01, getba-neq, getarray-union-03, getarray-union-02, getarray-union-01, getarray-union, getarray-superset, getarray-put=set, getarray-put-01, getarray-offset-02, getarray-offset, getarray-in-01, get-sublist, get-puteq, get-ateq-01, get-ateq, get-alleq, extension-01, extension, copy-succ, copy-in-between, copy-between, copy-bet-up, copy-bet-low, copy-bet-bet, copy-at-01, copy-arref, comp-same, comp-next, bar-sublist, bar-neq-soffset, bar-neq-same, bar-neq, bar-firstn, bar-eq-sub, at=get-offset, at=get, arrayref-02, arrayref-01, arrayref, arrayComp-08, arrayComp-07, arrayComp-05, arrayComp-04, arrayComp-02, arrayComp-01, Comp-get-02, Comp-get-01,
int-abs/leone is used by putar-getar, getba-eq, getarray-offset-02, getarray-offset, get-put-01, get-get, get-first, copy-bet-up, copy-bet-low, copy-bet-bet, comp-same, Comp-get-01,
int-abs/lep is used by putbar-put-override, putbar-byte, putar-at, putByteArray-append, putArray-in, getbar-restn-04, getbar-restn-01, getbar-anyrec, getarray-put=set, getarray-offset, getarray-in-01, copy-succ, bar-sublist, bar-neq-soffset, bar-neq, at=get-offset,
int-abs/lep-01 is used by putar-getar, getba-eq, getarray-union-03, extension, copy-upper, arrayComp-05, arrayComp-04, arrayComp-03, arrayComp-02,
int-abs/lep-02 is used by copy-upper-01, copy-succ, copy-in-upper-01, copy-bet-up, copy-bet-low, copy-bet-bet, comp-copy,
int-abs/ler is used by putbar-put-override, putbar-getbar-le, putar-inother, putar-in-02, putar-getar, putBar-lastrec, putArray-in, putAr-lastrec, getarray-put=set, getarray-offset, copy-succ, copy-between, copy-bet-up, copy-bet-low, copy-bet-bet, at=get-offset, at=get, arrayComp-02,
int-abs/les is used by getarray-offset, copy-in-between, copy-between, copy-bet-up, copy-bet-low, copy-bet-bet,
int-abs/lsone is used by putar-at, isarray-03, get-alleq, copy-lower, copy-in-lower,
int-abs/minus-add is used by getarray-offset, copy-bet-bet,
int-abs/minus-sub is used by getarray-offset,
int-abs/mone-05 is used by putbar-put-override, putByteArray-put-switch, get-rest,
int-abs/mone-06 is used by putbar-put-override, putbar-getbar-le, putar-getar-01, putar-getar, getintarray-rec-last, getintarray-rec-first, getintarray-in-02, getbar-rec, getbar-putbar-same-01, getbar-lastrec, getbar-5rec, getbar-3rec, getbar-2rec, getba-neq-01, getarray-union, getarray-put-01, getarray-offset-02, getarray-offset, getArray-rec-01, get-sublist, get-rest, get-rec-01, extension, copy-succ, copy-bet-bet, comp-same, at=get-offset,
int-abs/neg-06 is used by getarray-offset,
int-abs/negle-13 is used by getarray-offset,
int-abs/numadd-01 is used by putbar-getbar-le, putar-at,
int-abs/numle-02 is used by putbar-put-override, putbar-getbar-le, putByteArray-put-switch-01, putByteArray-append, putArray-put, getbar-5rec, getbar-3rec, getbar-2rec, getba-neq-01, getba-eq, getarray-union-03, getarray-offset, get-rest, get-rec-01, comp-same,
int-abs/numle-03 is used by putbar-put-override, putByteArray-put-switch, get-rest,
int-abs/numleledel is used by getarray-offset, get-alleq,
int-abs/numleledel-01 is used by putbar-put-override, putByteArray-put-switch-01, putByteArray-append, putArray-put, getbar-5rec, getbar-3rec, getbar-2rec, getba-neq-01, getba-eq, getarray-union-03, getarray-offset, get-rest, get-rec-01,
int-abs/numls-02 is used by putbar-put-override, putbar-getbar-le, putar-getar-01, putar-getar, getintarray-rec-last, getintarray-rec-first, getintarray-in-02, getbar-rec, getbar-putbar-same-01, getbar-lastrec, getbar-5rec, getbar-3rec, getbar-2rec, getba-neq-01, getarray-union, getarray-put=set, getarray-put-03, getarray-put-02, getarray-put-01, getarray-offset-02, getarray-offset, getarray-in-01, getArray-rec-01, get-sublist, get-rest, get-rec-01, get-length, get-del-01, get-alleq, extension, copy-succ, copy-bet-bet, at=get-offset, at=get, Comp-get-01,
int-abs/numls-03 is used by putByteArray-append,
int-abs/numlsledel-01 is used by getbar-5rec, getbar-3rec, getbar-2rec,
int-abs/numsub is used by putar-getar-01, putar-getar, getintarray-rec-last, getintarray-rec-first, getintarray-max-rec-01, getintarray-max-rec, getintarray-in-02, getbar-rec, getbar-putbar-same-01, getbar-lastrec, getbar-5rec, getbar-3rec, getbar-2rec, getarray-union, getarray-put=set, getarray-put-03, getarray-put-02, getarray-put-01, getarray-offset-02, getarray-offset, getarray-in-01, getArray-rec-01, get-sublist, get-rest, get-rec-01, get-del-01, get-alleq, copy-upper, copy-succ, copy-lower, copy-in-lower, copy-in-between, copy-ident, copy-bet-up, copy-bet-low, copy-bet-bet, at=get-offset, Comp-get-01,
int-abs/sub-add is used by putbar-byte, getbar-restn-04, getbar-restn-01, getarray-offset, get-get, get-first, bar-neq,
int-abs/sub-add-01 is used by getarray-union-03, copy-upper, copy-succ, copy-lower, copy-in-upper, copy-in-lower, copy-in-between, copy-between, copy-bet-up, copy-bet-low, copy-bet-bet, comp-same, arrayComp-02,
int-abs/sub-add-04 is used by copy-between, copy-bet-up, copy-bet-low, copy-bet-bet,
int-abs/sub-add-05 is used by putar-getar, putar-at, copy-bet-up, copy-bet-low,
int-abs/sub-add-06 is used by getarray-union-03, copy-bet-bet,
int-abs/sub-add-09 is used by getarray-offset,
int-abs/sub-eq is used by getarray-put=set, copy-upper, copy-lower, copy-in-upper, copy-in-lower, copy-in-between, copy-ident, copy-between, copy-bet-up, copy-bet-low, copy-bet-bet,
int-abs/sub-eq-01 is used by getba-neq-01, getarray-offset, copy-in-between,
int-abs/sub-le is used by getarray-union-03, getarray-offset, copy-upper, copy-in-upper, copy-in-between, copy-between, copy-bet-up, copy-bet-low, copy-bet-bet, comp-same, bar-neq-soffset,
int-abs/sub-le-01 is used by getbar-restn-02, getbar-len-02, getba-eq, getarray-union-03, getarray-offset, get-ateq, extension, copy-bet-up, copy-bet-low, copy-bet-bet, comp-same, bar-neq-soffset, arrayComp-02,
int-abs/sub-ls is used by get-ateq, extension, copy-lower, copy-in-lower, copy-bet-up, copy-bet-low, copy-bet-bet, comp-same, bar-restn, arrayComp-02,
int-abs/sub-ls-01 is used by getba-neq-01, getarray-offset, copy-lower, copy-in-lower, copy-in-between, copy-between, copy-bet-up, copy-bet-low, copy-bet-bet,
int-abs/sub-pred is used by extension, arrayComp-02,
int-abs/sub-sub is used by getarray-offset, copy-bet-up, copy-bet-low, copy-bet-bet, bar-restn,
int-abs/sub-sub-03 is used by copy-bet-bet,
int-abs/sub-sub-04 is used by copy-bet-bet, bar-neq-soffset,
int-abs/sub-zero-01 is used by getarray-union-02, copy-at-01, comp-copy, bar-restn,
int-abs/succ-01 is used by putbar-put-override, putbar-override, putar-rew, putar-inother, putar-in-02, putar-atother, putar-at, putByteArray-put-switch, putArray-put-switch, putArray-in, getintarray-in-02, getba-neq-01, getarray-union-03, getarray-put-01, getarray-offset, getarray-in-01, get-sublist, extension, copy-bet-up, copy-bet-low, copy-bet-bet, comp-same, bar-restn, Comp-get-01,
int-abs/succ-02 is used by putbar-put-override, putbar-override, putbar-getbar-le, putar-rew, putar-inother, putar-in-02, putar-getar, putar-atother, putar-at, putByteArray-put-switch-01, putByteArray-append, putBar-lastrec, putArray-put-switch, putArray-in, putAr-lastrec, getbar-putbar-same-01, getba-neq-01, getba-eq, getarray-put=set, getarray-put-01, getarray-in-01, get-sublist, get-get, get-first, get-alleq, extension, copy-in-upper, copy-in-between, copy-between, copy-bet-up, copy-bet-low, copy-bet-bet, comp-next, bar-restn, at=get-offset, at=get, arrayComp-02, arrayComp-01,
int-abs/zero-gels is used by isarray-01, getintarray-in-02, getarray-offset, comp-negative,
int-abs/zero-gels-01 is used by comp-same,
int-abs/zero-gels-02 is used by get-rest,
int-abs/zero-gels-04 is used by putbar-put-override, putbar-byte, putar-getar-01, getintarray-rec-first, getintarray-put-other-02, getintarray-empty-02, getbar-restn-01, getba-neq-01, getarray-union, getarray-put=set, getarray-put-01, getarray-offset, extension, copy-succ, comp-same, bar-zero, bar-neq, at=get-offset, at=get,
int-abs/zero-gs is used by putbar-put-override, putbar-override, putByteArray-append, putArray-put-switch, putAr-get-other-01, putAr-get-other, getarray-subset, extension, comp-copy, bar-restn, at=get-offset,

Used from specification ostore

ostore/javastore/inkeys-01 is used by getarray-union-03,
ostore/javastore/notempty is used by getarray-union-03,

Used from specification storekey

storekey/ex-03 is used by putArray-at, getbar-put,
storekey/ex-04 is used by putBar-rew,
storekey/disj is used by putar-atfs, putBar-rew-01, putArray-put-switch-01, getarray-put-03, get-put-01, copy-succ, copy-atfield,
storekey/elim-04 is used by putbytearray-in, putar-rew, putArray-in, getbar-put,
storekey/inj-04 is used by putbar-refval, putar-rew, putar-inother, putar-in-02, putar-getar, putar-atother, putar-at, putByteArray-put-switch, putBar-rew, putBar-lastrec, putArray-put-switch, putArray-put, putArray-in, putAr-lastrec, putAr-get-other-01, putAr-get-other, isarray-02, is_arrayref-03, getarray-put=set, getarray-put-01, copy-upper, copy-succ, copy-lower, copy-in-upper, copy-in-lower, copy-in-between, copy-ident, copy-between, copy-bet-up, copy-bet-low, copy-bet-bet, comp-next,
storekey/sel-06 is used by putar-rew, putArray-in, putAr-lastrec,
storekey/test is used by putarray-subset-new-01, putBar-rew, putBar-in, putArray-in,
storekey/test-01 is used by putarray-field, putar-rew, putBar-rew, putBar-in, putArray-put-switch-02, putArray-in, getbar-put, getbar-mode,
storekey/test-02 is used by putBar-rew, putBar-in, putArray-put-switch-02, putArray-in, getbar-put,
storekey/test-05 is used by putarray-mode, putBar-at-mode, getbar-put-04,
storekey/test-06 is used by putarray-field, putar-rew, putArray-put-switch-02, putArray-in, putAr-lastrec, getarray-put-04, get-put-03, get-put-02, arrayref-02,
storekey/test-07 is used by getbar-mode,
storekey/test-08 is used by putArray-in, getbar-put,

Used from specification nat-basic1

nat-basic1/f is used by putbar-byte, putAr-get-other-01, putAr-get-other, getintarray-in, getintarray-at, getbytearray-subset, getbar-restn, getarray-in, getarray-get, get-get,
nat-basic1/less-1 is used by getbytearray-subset,
nat-basic1/neq-01 is used by get-get,
nat-basic1/numls-01 is used by bar-len-01,
nat-basic1/one-01 is used by bar-len-01,
nat-basic1/ref-1 is used by putbar-byte, putAr-lastrec, getbar-restn-01, bar-sublist,
nat-basic1/z is used by putbytearray-in, putbar-put-override, putbar-override, putbar-byte, putar-rew, putar-getar, putar-at, getintarray-in, getintarray-at, getbytearray-subset, getbar-restn, getarray-in, getarray-get,

Used from specification int-basic1

int-basic1/forward-pos is used by getba-eq, getarray-union-03, getarray-put=set, getarray-put-03, getarray-put-02, getarray-offset, getarray-in-01, get-rest, get-rec-01, get-put-01, get-length, get-del-01, get-alleq, copy-bet-bet, at=get-offset, at=get, Comp-get-01,
int-basic1/lf-02 is used by get-get, get-first, get-empty,
int-basic1/lf-03 is used by get-first,
int-basic1/ls-01 is used by putbar-put-override, putar-rew, putar-inother, putar-in-02, putar-getar, putar-atother, putar-at, putByteArray-put-switch, putArray-in, getintarray-put-other-02, getintarray-in-02, getintarray-in, getintarray-empty-01, getintarray-at, getbytearray-subset, getbytearray-put-index-length, getbar-mod-01, getbar-len-01, getba-eq, getarray-union-03, getarray-put=set, getarray-put-01, getarray-offset, getarray-in-01, getarray-in, getarray-get, get-rest, get-rec-01, get-put-01, get-length-02, get-alleq, extension, copy-succ, copy-bet-bet, comp-same, comp-next, bar-empty, at=get, arrayComp-03, arrayComp-01, Comp-get-01,
int-basic1/lst-01 is used by copy-succ, copy-in-upper,
int-basic1/numlsf is used by putArray-put,
int-basic1/numlslsdel-01 is used by get-rest,
int-basic1/two-ls is used by getarray-offset-01,

Used from specification set-basic

set-basic/references/ne-01 is used by getbar-union-02,
set-basic/javastore/ne-01 is used by getarray-union-03,
set-basic/references/size-zero-01 is used by getbar-union-02,

Used from specification refkey

refkey/elim is used by putarray-subset-new-01, putar-rew, putBar-in, putArray-in, getbar-put, getbar-mode, getByteArray-put-01, get-put-02,
refkey/inj is used by putbar-refval, putar-rew, putByteArray-put-switch, putBar-rew-01, putBar-lastrec, putArray-put-switch-02, putArray-put-switch-01, putArray-put-switch, putArray-put, putArray-in, putAr-lastrec, putAr-get-other-01, putAr-get-other, isarray-02, copy-upper, copy-lower, copy-in-lower, copy-ident, copy-bet-up, copy-bet-low, copy-bet-bet, copy-atfield, arrayref-02, arrayref-01,
refkey/inj-01 is used by putbar-refval, putarray-field, putar-rew, putar-inother, putar-in-02, putar-getar, putar-atother, putar-atfs, putar-at, putBar-rew, putBar-lastrec, putArray-put-switch-02, putArray-put-switch-01, putArray-put, putArray-in, putAr-lastrec, putAr-get-other-01, putAr-get-other, isarray-02, is_arrayref-03, getarray-put=set, getarray-put-03, getarray-put-01, get-puteq, get-put-01, get-put, copy-succ, copy-in-lower, copy-in-between, copy-between, copy-bet-bet, comp-next, arrayref-02, arrayref-01,
refkey/sel-01 is used by putbytearray-in, putBar-in, putArray-in, putAr-lastrec,
refkey/sel-02 is used by putbytearray-in, putBar-in, putArray-in, putAr-lastrec, isarrayref-put, getbar-put-04, get-put-03,

Used from specification oelem

oelem/intlista/irreflexivity is used by putbar-getbar-le, putar-rew, putar-inother, putar-in-02, putar-getar, putar-atother, putByteArray-put-switch-01, putBar-lastrec, putArray-put, putArray-in, putAr-lastrec, getintarray-in-02, getbar-putbar-same-01, getbar-put-02, getba-eq, getarray-union-03, getarray-union-01, getarray-union, getarray-put=set, getarray-put-03, getarray-put-02, getarray-put-01, getarray-offset, getarray-in-01, get-zero, get-rest, get-rec-01, get-put-01, get-length, get-get, get-first, get-del-01, get-alleq, extension, copy-upper-01, copy-succ, copy-in-upper-01, copy-bet-up, copy-bet-low, copy-bet-bet, at=get-offset, at=get, arrayComp-02, arrayComp-01, Comp-get-01,
oelem/intlista/lel is used by putar-inother, putar-in-02, putByteArray-put-switch, putArray-in, isarray-02, getintarray-zero, getbytearray-length-zero, getarray-put=set, getarray-in-01, extension, copy-bet-bet, comp-same, at=get-offset, at=get,
oelem/intlista/ls-le is used by get-rest, copy-succ,
oelem/intlista/seq is used by isarray-03,
oelem/intlista/sls is used by putar-in-02, copy-succ, copy-in-between, copy-between, copy-bet-bet,
oelem/intlista/transitivity is used by getbytearray-subset, getba-eq, getarray-union-03, copy-bet-bet, comp-same,

Used from specification javavalue

javavalue/byteval is used by getar-at,
javavalue/disj-74 is used by putbar-refval,
javavalue/elim-03 is used by putBar-unrec,
javavalue/inj-07 is used by putBar-rew,
javavalue/sel-08 is used by putbar-getbar-le, getbar-putbar-same-01,
javavalue/sel-09 is used by copy-ref,
javavalue/test-19 is used by copy-ref,
javavalue/test-36 is used by putBar-unrec,

Used from specification list-data

list-data/bytelist/elim-list-c is used by putBar-rec,
list-data/javavalues/elim-list-c is used by get-rest,
list-data/javavalues/l is used by putar-rew, putar-getar, putar-at, getintarray-in, getarray-in, getarray-get, get-length-02,
list-data/intlista/l is used by getintarray-at,
list-data/bytelist/l is used by putbytearray-in, putbar-put-override, putbar-override, putbar-byte, getbytearray-put-index-length, getbar-len-01,
list-data/bytelist/length-neq is used by getbar-appeq, bar-neq,
list-data/javavalues/lf-01 is used by putar-getar,
list-data/javavalues/size-01 is used by putar-in-02, putar-getar, putar-at, putArray-put, putArray-in, putArray-append, putAr-lastrec, get-length-03, get-length-01,
list-data/bytelist/size-01 is used by putbar-put-override, putbar-override, putbar-getbar-le, putByteArray-append, putBar-lastrec, getbytearray-subset, getbar-putbar-same-01,

Used from specification list-del

list-del/bytelist/extension is used by getbytearray-subset,
list-del/bytelist/first-sub is used by bar-firstn,
list-del/bytelist/firstN-rec-01 is used by putbar-getbar-le,
list-del/javavalues/get-butlast is used by get-get, at=get-offset, at=get,
list-del/javavalues/get-last is used by get-get, at=get-offset, at=get,
list-del/intlista/in-get is used by getintarray-in,
list-del/javavalues/in-get is used by getarray-in,
list-del/javavalues/put-butlast is used by getarray-put=set,
list-del/javavalues/put-last is used by getarray-put=set,
list-del/bytelist/rest-empty is used by getbar-restn-01,
list-del/bytelist/rest-len is used by getbar-restn,
list-del/bytelist/restN-append is used by getbar-restn-01,
list-del/javavalues/sub-zerorec is used by get-sublist,
list-del/bytelist/sublist-all is used by bar-sublist,
list-del/bytelist/sublist-append is used by bar-sublist,
list-del/bytelist/sublist-append-01 is used by bar-sublist,
list-del/bytelist/firstN-zero is used by putbar-getbar-le,
list-del/javavalues/get-succ is used by putar-at,
list-del/javavalues/get-zero is used by putar-getar,
list-del/javavalues/get-zero-01 is used by putar-at,
list-del/javavalues/one-03 is used by get-get, at=get-offset, at=get,
list-del/javavalues/put-one is used by getarray-put=set,
list-del/bytelist/restN-rec is used by bar-restn,
list-del/bytelist/restN-zero is used by bar-restn,
list-del/javavalues/sub-rec is used by get-sublist,
list-del/javavalues/sub-zerozero is used by get-sublist,

Used from specification specialkeys

specialkeys/length is used by copy-length-02, copy-length,
specialkeys/mode is used by putarray-mode, putBar-at-mode, copy-mode-01, copy-mode,
specialkeys/type is used by copy-type-01, copy-type,
specialkeys/len is used by get-put-03, get-put-02, arrayref-01,
specialkeys/length-01 is used by get-put-05,
specialkeys/length-02 is used by getbar-put-04, getbar-put-03,
specialkeys/length-04 is used by putarray-length, putBar-at-len,
specialkeys/mode-01 is used by putarray-mode, putBar-at-mode,
specialkeys/mode-02 is used by getbar-mode,
specialkeys/mode-03 is used by getbar-mode,
specialkeys/mode-04 is used by is_arrayref-02,
specialkeys/mode-05 is used by getbar-mode,
specialkeys/out-04 is used by is_arrayref-01,
specialkeys/type-03 is used by putbytearray-in,
specialkeys/type-06 is used by putarray-type, putBar-at-type,

Used from specification storefunsx

storefunsx/eqex is used by get-eqex-03, get-eqex-01,
storefunsx/onlyModified is used by isarrayref-mod, getbar-mod-01,
storefunsx/onlymod-length is used by getbar-mod,
storefunsx/refs-def is used by getbar-union-02, getbar-union,
storefunsx/reftypep is used by copy-ref,
storefunsx/union-at-right is used by getarray-union-03,
storefunsx/union-at-right-02 is used by getbar-union-01, getarray-union,
storefunsx/eqex-ref is used by get-eqex-03,
storefunsx/eqex-sym is used by get-eqex-03, get-eqex-02,
storefunsx/eqex-trans is used by get-eqex-03,
storefunsx/lookup-xtra is used by getbytearray-subset, getarray-subset,
storefunsx/union-at-right-01 is used by getarray-union-03,

Used from specification javastore

javastore/at-other-16 is used by putAr-get-other-01, putAr-get-other,
javastore/in-01 is used by putar-inother,
javastore/instore-02 is used by putar-inother, putar-in-02,
javastore/at-other-16 is used by getarray-put-06,
javastore/in-01 is used by putar-inref, putArray-in, isarray, copy-succ, copy-in,
javastore/instore-02 is used by copy-succ, copy-in-upper, copy-in-between,
javastore/length-at is used by getintarray-put-other-02, getbytearray-put-index-length,
javastore/look-ins is used by putar-getar-01, putar-atref, putBar-rew, putAr-get-other-01, getintarray-put-other-01, getarray-put-other, getarray-put-02, getByteArray-put, copy-succ, copy-lower, copy-between, copy-at, comp-next,
javastore/lookup-if is used by putbar-getbar-le, putarray-field, putar-getar, putar-atother, putar-atfs, putar-at, putBar-rew, getarray-put=set, getarray-put-03, getarray-put-01, get-puteq, get-put-01, get-put, copy-upper, copy-succ, copy-lower, copy-ident, copy-between, copy-bet-up, copy-bet-low, copy-bet-bet, copy-atfield, comp-next,
javastore/sk is used by putar-infs, copy-succ, copy-infs,
javastore/sk-01 is used by arrayref,

Used from specification classname

classname/inj is used by getbar-put-04, getbar-put-03,

Used from specification int-mult

int-mult/dist-lsplit is used by comp-same,
int-mult/Mult-zero is used by copy-bet-low, comp-same,
int-mult/add-mult-two is used by copy-bet-up, copy-bet-low, copy-bet-bet, comp-same,
int-mult/associativity is used by copy-bet-up, copy-bet-low, copy-bet-bet, copy-at-01, comp-same,
int-mult/commutativity is used by copy-bet-up, copy-bet-low, copy-bet-bet, copy-at-01, comp-same,
int-mult/dist-rmerge is used by copy-bet-bet,
int-mult/eq-pos is used by copy-bet-bet,
int-mult/ls-pos is used by copy-at-01,
int-mult/ls-sub is used by comp-same,
int-mult/numeq-03 is used by copy-bet-bet,
int-mult/numle-04 is used by copy-bet-up, copy-bet-low, copy-bet-bet,
int-mult/numls-01 is used by copy-bet-low,
int-mult/numls-05 is used by copy-bet-up, copy-bet-low,
int-mult/numsub is used by copy-bet-low,
int-mult/one is used by copy-bet-up, copy-bet-low, copy-bet-bet, comp-same,
int-mult/succ-rmerge is used by copy-bet-bet,
int-mult/two-sub-01 is used by copy-bet-up, copy-bet-bet,
int-mult/zero-ge is used by copy-at-01,
int-mult/zero-ls-02 is used by comp-same,

Used from specification nat

nat/elim-sub is used by getbar-restn,
nat/elim-pred-c is used by putbar-getbar-le,
nat/elim-sub is used by bar-sublist,
nat/eq-02 is used by getbar-restn,
nat/fle is used by putbar-byte,
nat/fle-01 is used by putbar-byte,
nat/le-ls-simp is used by getbar-restn,
nat/lels is used by putbar-byte, putAr-get-other-01, putAr-get-other, getintarray-in, getintarray-at, getarray-in, getar-at, bar-at,
nat/lels-01 is used by putAr-lastrec, putAr-get-other-01, putAr-get-other, getbar-restn-04, getbar-restn-01, getbar-restn, bar-sublist,
nat/lep is used by getbar-restn-04,
nat/ler is used by putAr-lastrec, getbar-restn-01, bar-sublist,
nat/lez is used by putbar-byte,
nat/lez-01 is used by getbar-restn,
nat/ls-01 is used by getarray-offset, get-put-01,
nat/ls-le-simp is used by putAr-get-other-01, putAr-get-other, getintarray-in, getintarray-at, getarray-in,
nat/pred-03 is used by putbar-getbar-le, getarray-offset, get-put-01,
nat/succ-01 is used by putAr-get-other-01, putAr-get-other,

Used from specification nat-basic2

nat-basic2/a is used by putbar-put-override, putbar-override, putbar-getbar-le, putar-rew, putar-inother, putar-in-02, putar-getar, putar-atother, putar-at, putByteArray-append, putBar-lastrec, putArray-put-switch, putArray-put, putArray-in, putArray-append, putAr-lastrec, putAr-get-other-01, putAr-get-other, getintarray-in-02, getbar-restn-04, getbar-restn, getbar-putbar-same-01, getarray-union, getarray-put=set, getarray-put-03, getarray-put-02, getarray-put-01, getarray-offset, getarray-in-01, get-sublist, get-rest, get-rec-01, get-put-01, get-length, get-get, get-first, get-del-01, get-alleq, extension, bar-sublist, bar-restn, at=get-offset, at=get, Comp-get-01,
nat-basic2/c is used by putbar-put-override, putbar-override, putbar-getbar-le, putar-rew, putar-inother, putar-in-02, putar-getar, putar-atother, putar-at, putByteArray-append, putBar-lastrec, putArray-put-switch, putArray-put, putArray-in, putArray-append, putAr-lastrec, putAr-get-other-01, putAr-get-other, getintarray-in-02, getbar-restn-04, getbar-restn, getbar-putbar-same-01, getarray-union, getarray-put=set, getarray-put-03, getarray-put-02, getarray-put-01, getarray-offset, getarray-in-01, get-sublist, get-rest, get-rec-01, get-put-01, get-length, get-get, get-first, get-del-01, get-alleq, extension, bar-sublist, bar-restn, at=get-offset, at=get, Comp-get-01,
nat-basic2/eq is used by bar-sublist,
nat-basic2/eq-01 is used by putbar-getbar-le, getbar-restn, get-length,
nat-basic2/l-02 is used by putAr-get-other-01, putAr-get-other, getbar-restn-04,
nat-basic2/s is used by putAr-get-other-01, putAr-get-other, getintarray-in-02, getarray-union, getarray-put=set, getarray-put-03, getarray-put-02, getarray-put-01, getarray-offset, getarray-in-01, get-rest, get-rec-01, get-put-01, get-length, get-get, get-first, get-del-01, get-alleq, extension, at=get-offset, at=get, Comp-get-01,
nat-basic2/succ is used by putArray-put, get-sublist, bar-restn,
nat-basic2/z is used by bar-sublist,

Used from specification set-union

set-union/references/int-empty-01 is used by getbar-union,
set-union/references/int-a is used by getbar-union-02,
set-union/references/int-c is used by getbar-union-02,
set-union/references/int-empty-02 is used by getbar-union-02,

Used from specification intlist

intlist/max-last-max is used by getintarray-max-rec,
intlist/max-last-not-max is used by getintarray-max-rec-01,