[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/junkref-put-nopathex is used by junkref-put-other-fieldclass,
cyclic/pathex-def-simple is used by nopathex-runtimetype, nopathex-badarrayfield,
cyclic/pathex-noreftype is used by junkref-put-other-fieldclass,
cyclic/pathex-not-is-validref-01 is used by nopathex-badclassfield,
cyclic/validrefs-array is used by validrefs-not-contains,
cyclic/validrefs-class is used by validrefs-not-contains,
cyclic/validrefs-is-junk is used by validrefs-not-contains, nopathex-badarrayfield,
cyclic/validrefs-one is used by validrefs-not-contains, nopathex-badarrayfield,
cyclic/pathex-one is used by nopathex-badclassfield,
cyclic/validrefs-not is used by nopathex-badarrayfield,
cyclic/validrefs-null-02 is used by validrefs-not-contains, nopathex-badarrayfield,

Used from specification list

list/javatypes/firsteq-01 is used by contains-trans-01, contains-subspec-better, contains-subspec, contains-not-hasclasstype-level-01, contains-levelsubset,
list/javatypes/lastoc-rew is used by contains-type-def-nodups,
list/javatypes/Last is used by validrefs-not-contains, same-subclasses-01, nopathex-badclassfield, nopathex-badarrayfield, contains-typeex-03, contains-typeex-02, contains-type-rec, contains-type-def-nodups, contains-trans, contains-subtype, contains-subspec-better, contains-subspec, contains-shortarray-03, contains-not-hasclasstype-level-01, contains-levelsubset, contains-intarray-03, contains-field-def-case, contains-bytearray-03, contains-boolarray-03, contains-array-elemtype-ex, contains-array-elemtype-05, contains-array-elemtype,
list/javatypes/Nil is used by validrefs-not-contains, same-subclasses-01, contains-type-rec, contains-type-def-nodups, contains-trans-01, contains-subtype, contains-subspec-better, contains-subspec, contains-shortarray-03, contains-shortarray, contains-not-hasclasstype-level-01, contains-levelsubset, contains-intarray-03, contains-intarray, contains-bytearray-03, contains-bytearray, contains-boolarray-03, contains-boolarray, contains-array-elemtype-ex, contains-array-elemtype, contains-append,
list/javatypes/a is used by validrefs-not-contains, same-subclasses-01, nopathex-badclassfield, nopathex-badarrayfield, contains-typeex-05, contains-typeex-04, contains-typeex-03, contains-typeex-02, contains-typeex-01, contains-typeex, contains-type-rec, contains-type-def-nodups, contains-two, contains-trans-01, contains-trans, contains-supertype, contains-subtype, contains-subspec-better, contains-subspec, contains-shortarray-03, contains-shortarray-01, contains-shortarray, contains-short, contains-rec-01, contains-primtype-05, contains-primtype-04, contains-not-hasclasstype-level-01, contains-levelsubset, contains-intarray-03, contains-intarray-01, contains-intarray, contains-int, contains-field-def-case, contains-bytearray-03, contains-bytearray-01, contains-bytearray, contains-byte, contains-boolarray-03, contains-boolarray-01, contains-boolarray, contains-bool, contains-array-elemtype-ex, contains-array-elemtype-05, contains-array-elemtype, contains-array, contains-append,
list/references/a is used by validrefs-not-contains, nopathex-runtimetype, nopathex-badarrayfield, junkref-subspec-samesubclasses,
list/references/app is used by validrefs-not-contains, nopathex-runtimetype, nopathex-badarrayfield,
list/javatypes/app is used by contains-typeex-04, contains-typeex-01, contains-typeex, contains-two, contains-supertype, contains-subspec-better, contains-subspec, contains-shortarray-01, contains-shortarray, contains-short, contains-primtype-05, contains-primtype-04, contains-not-hasclasstype-level-01, contains-levelsubset, contains-intarray-01, contains-intarray, contains-int, contains-field-def-case, contains-bytearray, contains-byte, contains-boolarray-01, contains-boolarray, contains-bool, contains-append,
list/javatypes/app-02-ant is used by same-subclasses-01, nopathex-badclassfield, nopathex-badarrayfield, contains-type-rec, contains-type-def-nodups, contains-trans-01, contains-subtype, contains-subspec-better, contains-subspec, contains-shortarray, contains-not-hasclasstype-level-01, contains-levelsubset, contains-intarray, contains-field-def-case, contains-bytearray, contains-boolarray, contains-array-elemtype-ex, contains-array-elemtype, contains-append,
list/references/app-02-ant is used by validrefs-not-contains, nopathex-runtimetype, nopathex-badarrayfield,
list/javatypes/app-04 is used by contains-bytearray-01,
list/javatypes/app-06 is used by contains-levelsubset,
list/javatypes/c is used by same-subclasses-01, contains-typeex-04, contains-type-rec, contains-type-def-nodups, contains-trans-01, contains-trans, contains-supertype, contains-subtype, contains-subspec-better, contains-subspec, contains-shortarray-01, contains-shortarray, contains-rec-01, contains-primtype-05, contains-not-hasclasstype-level-01, contains-levelsubset, contains-intarray-01, contains-intarray, contains-field-def-case, contains-bytearray-01, contains-bytearray, contains-boolarray-01, contains-boolarray, contains-array-elemtype-ex, contains-array-elemtype-05, contains-array-elemtype, contains-array, contains-append,
list/references/c is used by validrefs-not-contains, nopathex-runtimetype, nopathex-badarrayfield, junkref-subspec-samesubclasses,
list/javatypes/c-03 is used by contains-trans-01, contains-subspec-better, contains-subspec, contains-shortarray-01, contains-shortarray, contains-not-hasclasstype-level-01, contains-levelsubset, contains-intarray-01, contains-intarray, contains-boolarray-01, contains-boolarray,
list/javatypes/c-04 is used by contains-shortarray-02, contains-intarray-02, contains-bytearray-02, contains-boolarray-02,
list/javatypes/c-05 is used by contains-subspec-better, contains-subspec, contains-shortarray, contains-levelsubset, contains-intarray, contains-bytearray, contains-boolarray,
list/javatypes/c-08 is used by nopathex-badclassfield, nopathex-badarrayfield, contains-not-hasclasstype-level-01, contains-field-def-case, contains-append,
list/references/c-08 is used by validrefs-not-contains, nopathex-runtimetype, nopathex-badarrayfield,
list/references/e is used by validrefs-not-contains, nopathex-runtimetype, nopathex-badarrayfield,
list/javatypes/e is used by same-subclasses-01, nopathex-badclassfield, nopathex-badarrayfield, contains-type-rec, contains-trans-01, contains-subspec-better, contains-subspec, contains-shortarray-02, contains-shortarray, contains-not-hasclasstype-level-01, contains-levelsubset, contains-length, contains-intarray-02, contains-intarray, contains-field-def-case, contains-bytearray-02, contains-bytearray, contains-boolarray-02, contains-boolarray, contains-append,
list/references/e-01 is used by validrefs-not-contains, nopathex-runtimetype, nopathex-badarrayfield, junkref-subspec-samesubclasses,
list/javatypes/e-01 is used by same-subclasses-01, contains-typeex-04, contains-type-rec, contains-type-def-nodups, contains-trans-01, contains-supertype, contains-subtype, contains-subspec-better, contains-subspec, contains-shortarray-01, contains-rec-01, contains-primtype-05, contains-not-hasclasstype-level-01, contains-intarray-01, contains-field-def-case, contains-bytearray-01, contains-boolarray-01, contains-array-elemtype-ex, contains-array-elemtype, contains-array,
list/javatypes/e-02 is used by same-subclasses-01, contains-type-rec, contains-type-def-nodups, contains-trans-01, contains-subtype, contains-subspec-better, contains-subspec, contains-shortarray, contains-not-hasclasstype-level-01, contains-levelsubset, contains-intarray, contains-bytearray, contains-boolarray, contains-array-elemtype-ex, contains-array-elemtype, contains-append,
list/references/e-02 is used by validrefs-not-contains, nopathex-badarrayfield,
list/javatypes/e-03 is used by contains-append,
list/references/first is used by validrefs-not-contains,
list/javatypes/first is used by nopathex-badclassfield, contains-length, contains-field-def-case, contains-bytearray-01, contains-bytearray,
list/javatypes/first-01 is used by same-subclasses-01, contains-type-rec, contains-type-def-nodups, contains-subtype, contains-array-elemtype-ex, contains-array-elemtype,
list/javatypes/first-02 is used by contains-trans-01, contains-append,
list/javatypes/fr is used by contains-trans-01, contains-subspec-better, contains-subspec, contains-not-hasclasstype-level-01,
list/javatypes/in-06 is used by contains-typeex-04, contains-type-def-nodups, contains-subtype, contains-subspec-better, contains-subspec, contains-not-hasclasstype-level-01, contains-levelsubset, contains-array-elemtype,
list/javatypes/in-08 is used by contains-trans-01, contains-subspec-better, contains-subspec, contains-not-hasclasstype-level-01,
list/javatypes/in-14 is used by same-subclasses-01, contains-trans-01, contains-subspec-better, contains-subspec, contains-shortarray, contains-not-hasclasstype-level-01, contains-levelsubset, contains-intarray, contains-bytearray, contains-boolarray, contains-append,
list/javatypes/in-15 is used by same-subclasses-01, contains-trans-01, contains-subspec-better, contains-subspec, contains-shortarray, contains-not-hasclasstype-level-01, contains-levelsubset, contains-intarray, contains-bytearray, contains-boolarray, contains-append,
list/javatypes/in-17 is used by same-subclasses-01, contains-typeex-05, contains-typeex-04, contains-type-def-nodups, contains-trans-01, contains-subspec-better, contains-subspec, contains-shortarray, contains-not-hasclasstype-level-01, contains-levelsubset, contains-intarray, contains-bytearray, contains-boolarray, contains-append,
list/javatypes/in-append is used by same-subclasses-01, contains-typeex-05, contains-typeex-04, contains-type-def-nodups, contains-trans-01, contains-subspec-better, contains-subspec, contains-shortarray, contains-not-hasclasstype-level-01, contains-levelsubset, contains-intarray, contains-bytearray, contains-boolarray, contains-append,
list/javatypes/in-empty is used by contains-typeex-04, contains-type-def-nodups, contains-subtype, contains-subspec-better, contains-subspec, contains-shortarray, contains-not-hasclasstype-level-01, contains-levelsubset, contains-intarray, contains-boolarray, contains-array-elemtype,
list/storekeys/in-empty is used by contains-predefined,
list/javatypes/inapp-07 is used by contains-subspec-better, contains-subspec, contains-levelsubset,
list/references/len is used by junkref-subspec-samesubclasses,
list/javatypes/len is used by same-subclasses-01, contains-type-def-nodups, contains-trans-01, contains-subtype, contains-subspec-better, contains-subspec, contains-not-hasclasstype-level-01, contains-levelsubset, contains-array-elemtype-ex, contains-array-elemtype,
list/references/len-02 is used by junkref-subspec-samesubclasses,
list/javatypes/len-02 is used by same-subclasses-01, contains-type-def-nodups, contains-trans-01, contains-subtype, contains-subspec-better, contains-subspec, contains-not-hasclasstype-level-01, contains-levelsubset, contains-array-elemtype-ex, contains-array-elemtype,
list/javatypes/ni is used by contains-subspec-better, contains-subspec, contains-levelsubset,

Used from specification storefuns

storefuns/instore-01 is used by validstatfield-subspec-samesubclasses, validref-subspec-samesubclasses,

Used from specification int-basic2

Used from specification valuefuns

valuefuns/okval-reftype is used by validstatfield-subspec-samesubclasses,

Used from specification junkrefs

junkrefs/junkref-array is used by same-subclasses-array-forward, junkref-subspec-samesubclasses,
junkrefs/junkref-class is used by same-subclasses-class-forward, junkref-subspec-samesubclasses,
junkrefs/junkref-def is used by junkref-subspec-samesubclasses,
junkrefs/junkref-is-junk is used by validref-subspec-samesubclasses-01, validref-subspec-samesubclasses, same-subclasses-class-forward, same-subclasses-array-forward, junkref-subspec-samesubclasses,
junkrefs/junkref-not-hasclasstype is used by validref-subspec-samesubclasses,
junkrefs/junkref-not-hasclasstype-01 is used by validref-subspec-samesubclasses-01,
junkrefs/junkref-primarray-level-01 is used by junkref-subspec-samesubclasses,
junkrefs/junkref-put-badarrayfield is used by junkref-put-other-fieldclass,
junkrefs/junkref-put-badclassfield is used by junkref-put-other-fieldclass,
junkrefs/junkrefs-array is used by junkref-subspec-samesubclasses,
junkrefs/junkrefs-class is used by junkref-subspec-samesubclasses,
junkrefs/junkrefs-is-junk is used by junkref-subspec-samesubclasses,
junkrefs/junkrefs-sametype is used by junkref-subspec-samesubclasses,
junkrefs/levelsubset-def is used by contains-levelsubset,
junkrefs/same-subclasses-one-def is used by contains-subspec-better,
junkrefs/same-subclasses-subclass is used by validref-subspec-samesubclasses, same-subclasses-subclass, same-subclasses-forward, same-subclasses-array-forward,
junkrefs/same-subclasses-tdnameex-03 is used by same-subclasses-contains-typeex-01, contains-subspec-better,
junkrefs/same-subclasses-tdnameex-05 is used by same-subclasses-contains-typeex-01, contains-subspec-better,
junkrefs/same-subclasses-trans is used by same-subclasses-contains-trans,
junkrefs/validfield-def is used by validstatfield-subspec-samesubclasses,
junkrefs/validref-def is used by validref-subspec-samesubclasses-01,
junkrefs/validref-hasnoclasstype-level is used by validstatfield-subspec-samesubclasses,
junkrefs/validref-okreftype is used by validref-subspec-samesubclasses,
junkrefs/validrefval-def is used by validstatfield-subspec-samesubclasses,
junkrefs/validstatfield-storekey-def is used by validstatfield-subspec-samesubclasses,
junkrefs/junkref-not-hasclasstype-01 is used by validref-subspec-samesubclasses-01, validref-subspec-samesubclasses,
junkrefs/junkref-null is used by validref-subspec-samesubclasses, junkref-subspec-samesubclasses,
junkrefs/junkref-put-refval-statfield-01 is used by junkref-put-other-fieldclass,
junkrefs/junkrefs-junkref is used by junkref-subspec-samesubclasses,
junkrefs/junkrefs-null-02 is used by junkref-subspec-samesubclasses,
junkrefs/junkrefs-runtimetype is used by junkref-subspec-samesubclasses,
junkrefs/levelsubset-classex-02 is used by contains-subspec,
junkrefs/levelsubset-typeex is used by contains-subspec, contains-levelsubset,
junkrefs/nojunkref-typeex is used by same-subclasses-class-forward,
junkrefs/same-subclasses-is-array is used by same-subclasses-is-array,
junkrefs/same-subclasses-is-obj is used by same-subclasses-is-obj,
junkrefs/same-subclasses-tdnameex is used by same-subclasses-contains-typeex-02, same-subclasses-01,
junkrefs/same-subclasses-tdnameex-01 is used by same-subclasses-contains-typeex-01, same-subclasses-01, contains-subspec-better,
junkrefs/same-subclasses-tdnameex-03 is used by same-subclasses-01, contains-subspec-better,
junkrefs/same-subclasses-tdnameex-04 is used by same-subclasses-contains-tdnameex-01,
junkrefs/same-subclasses-tdnameex-05 is used by same-subclasses-contains-tdnameex-02,
junkrefs/validrefval-ref is used by validstatfield-subspec-samesubclasses,
junkrefs/validstatfield-index is used by validstatfield-subspec-samesubclasses,

Used from specification fieldspec

Used from specification intnat

intnat/labs is used by contains-objectarray, contains-not-has-classtype-01, contains-not-has-classtype, contains-array-elemtype-11, contains-array-elemtype-06, contains-array-elemtype-04, contains-array-elemtype-02, contains-array-elemtype-01,

Used from specification int-abs

int-abs/abs-le-succ is used by contains-objectarray, contains-not-has-classtype-01, contains-not-has-classtype, contains-array-elemtype-11, contains-array-elemtype-06, contains-array-elemtype-04, contains-array-elemtype-02, contains-array-elemtype-01,
int-abs/ax-02 is used by validref-subspec-samesubclasses-01, same-subclasses-contains-typeex-02, contains-array-elemtype-ex,
int-abs/forward-le-01 is used by validrefs-not-contains, same-subclasses-array-forward, junkref-subspec-samesubclasses,
int-abs/forward-le-05 is used by validrefs-not-contains, same-subclasses-array-forward, junkref-subspec-samesubclasses,
int-abs/lels is used by same-subclasses-array-forward, junkref-subspec-samesubclasses, contains-objectarray, contains-not-has-classtype-01, contains-not-has-classtype, contains-array-elemtype-11, contains-array-elemtype-06, contains-array-elemtype-04, contains-array-elemtype-02, contains-array-elemtype-01,
int-abs/lels-01 is used by same-subclasses-array-forward, junkref-subspec-samesubclasses,
int-abs/lels-03 is used by same-subclasses-array-forward, junkref-subspec-samesubclasses,
int-abs/lels-04 is used by same-subclasses-array-forward, junkref-subspec-samesubclasses,
int-abs/lsone is used by contains-array-elemtype-ex,
int-abs/numadd-01 is used by contains-array-elemtype-ex, contains-array-elemtype-06, contains-array-elemtype-01,
int-abs/succ-02 is used by contains-array-elemtype-ex,

Used from specification okfuns

okfuns/is_array-typeex is used by same-subclasses-array-forward,
okfuns/okreftype is used by validref-subspec-samesubclasses,
okfuns/good-field-field-01 is used by validstatfield-subspec-samesubclasses,
okfuns/is_array-arraytype is used by same-subclasses-array-forward, junkref-subspec-samesubclasses,
okfuns/is_array-classtype is used by validrefs-not-contains,
okfuns/is_array-hasnoclasstype is used by same-subclasses-array-forward,
okfuns/is_array-null is used by same-subclasses-array-forward,
okfuns/is_array-reftype is used by validrefs-not-contains,
okfuns/is_array-type-01 is used by same-subclasses-array-forward,
okfuns/is_array-type-04 is used by nopathex-badclassfield,
okfuns/is_array-typeex is used by validrefs-not-contains, nopathex-badarrayfield,

Used from specification storekey

storekey/elim-03 is used by validstatfield-subspec-samesubclasses,
storekey/sel-05 is used by validstatfield-subspec-samesubclasses,
storekey/test is used by validstatfield-subspec-samesubclasses,
storekey/test-01 is used by validstatfield-subspec-samesubclasses,
storekey/test-05 is used by validstatfield-subspec-samesubclasses,

Used from specification typefuns

Used from specification classnamefuns

Used from specification nat-basic1

nat-basic1/f is used by contains-levelsubset, contains-array-elemtype-ex,
nat-basic1/one-01 is used by contains-levelsubset,
nat-basic1/ref-1 is used by same-subclasses-01, junkref-subspec-samesubclasses, contains-type-def-nodups, contains-trans-01, contains-subtype, contains-subspec-better, contains-subspec, contains-not-hasclasstype-level-01, contains-levelsubset, contains-array-elemtype-ex, contains-array-elemtype,
nat-basic1/z is used by contains-array-elemtype-ex,

Used from specification javatype

Used from specification javavalue

javavalue/elim-10 is used by validref-subspec-samesubclasses,
javavalue/elim-13 is used by validstatfield-subspec-samesubclasses, validrefs-not-contains, junkref-subspec-samesubclasses,
javavalue/sel-09 is used by validref-subspec-samesubclasses, same-subclasses-class-forward, same-subclasses-array-forward, junkref-subspec-samesubclasses,
javavalue/sel-11 is used by validref-subspec-samesubclasses,
javavalue/test-19 is used by validstatfield-subspec-samesubclasses, validrefs-not-contains, validref-subspec-samesubclasses, same-subclasses-class-forward, same-subclasses-array-forward, junkref-subspec-samesubclasses,
javavalue/test-92 is used by validref-subspec-samesubclasses,

Used from specification list-dup

list-dup/javatypes/a is used by contains-type-def-nodups,
list-dup/javatypes/c-02 is used by contains-type-def-nodups,
list-dup/javatypes/dups-cons is used by contains-trans, contains-subtype, contains-subspec-better, contains-subspec, contains-not-hasclasstype-level-01, contains-levelsubset, contains-array-elemtype,
list-dup/javatypes/e-01 is used by contains-type-def-nodups, contains-subtype, contains-subspec-better, contains-subspec, contains-not-hasclasstype-level-01, contains-levelsubset, contains-array-elemtype,
list-dup/javatypes/f-01 is used by contains-type-def-nodups,
list-dup/javatypes/rec is used by contains-type-def-nodups, contains-subtype, contains-not-hasclasstype-level-01,

Used from specification list-data

list-data/references/elim-list-c is used by validrefs-not-contains, nopathex-runtimetype, nopathex-badarrayfield, junkref-subspec-samesubclasses,
list-data/javatypes/elim-list-c is used by same-subclasses-01, contains-typeex-04, contains-type-rec, contains-type-def-nodups, contains-trans-01, contains-supertype, contains-subtype, contains-subspec-better, contains-subspec, contains-shortarray-01, contains-shortarray, contains-rec-01, contains-primtype-05, contains-not-hasclasstype-level-01, contains-levelsubset, contains-intarray-01, contains-intarray, contains-field-def-case, contains-bytearray-01, contains-bytearray, contains-boolarray-01, contains-boolarray, contains-array-elemtype-ex, contains-array-elemtype, contains-array, contains-append,
list-data/javatypes/l is used by contains-levelsubset, contains-array-elemtype-ex,
list-data/javatypes/length-rest is used by contains-levelsubset,
list-data/javatypes/size-01 is used by contains-array-elemtype-ex,

Used from specification specialkeys

specialkeys/type-04 is used by nopathex-badarrayfield, junkref-put-other-fieldclass,

Used from specification addfuns

addfuns/is-real-object-def is used by same-subclasses-class-forward,
addfuns/is-valid-ref-stronger-def is used by validrefs-not-contains, same-subclasses-class-forward, same-subclasses-array-forward, nopathex-badclassfield, junkref-subspec-samesubclasses,
addfuns/is_obj-arraytype is used by same-subclasses-array-forward,
addfuns/is_obj-typeex is used by same-subclasses-class-forward,
addfuns/is_valid_ref-typeex is used by validref-subspec-samesubclasses-01, validref-subspec-samesubclasses, same-subclasses-array-forward,
addfuns/isobj-type-08 is used by same-subclasses-class-forward,
addfuns/instfields-predef is used by contains-predefined,
addfuns/is_obj-01 is used by same-subclasses-class-forward,
addfuns/is_obj-arraytype is used by validrefs-not-contains,
addfuns/is_obj-classtype is used by validrefs-not-contains,
addfuns/is_obj-hasclasstype is used by same-subclasses-class-forward,
addfuns/is_obj-no-interface is used by validrefs-not-contains, nopathex-badclassfield,
addfuns/is_obj-null is used by same-subclasses-class-forward,
addfuns/is_obj-reftype is used by validrefs-not-contains,
addfuns/is_obj-typeex is used by validrefs-not-contains,
addfuns/is_valid_ref-array is used by same-subclasses-array-forward,
addfuns/is_valid_ref-array-01 is used by same-subclasses-class-forward, nopathex-badarrayfield,
addfuns/is_valid_ref-typeex is used by validrefs-not-contains, nopathex-badclassfield,
addfuns/isobj-array-01 is used by same-subclasses-class-forward,
addfuns/statfields-special is used by validstatfield-subspec-samesubclasses,

Used from specification predefined

predefined/le-01 is used by contains-objectarray,

Used from specification nat

nat/fle is used by contains-array-elemtype-ex,
nat/le-ls-simp is used by same-subclasses-01,
nat/lels is used by contains-array-elemtype-ex,
nat/lels-01 is used by contains-levelsubset, contains-array-elemtype-ex,
nat/ls-01 is used by contains-levelsubset,
nat/pred-03 is used by contains-levelsubset,

Used from specification list-last

list-last/javatypes/butlast-last is used by contains-levelsubset, contains-field-def-case,
list-last/references/l is used by validrefs-not-contains, nopathex-runtimetype, nopathex-badarrayfield,
list-last/javatypes/l is used by nopathex-badclassfield, contains-length, contains-field-def-case,
list-last/javatypes/l-02 is used by contains-field-def-case,
list-last/references/l-02 is used by validrefs-not-contains, nopathex-runtimetype, nopathex-badarrayfield,
list-last/references/l-05 is used by validrefs-not-contains,
list-last/javatypes/last-01 is used by nopathex-badclassfield, nopathex-badarrayfield, contains-field-def-case,
list-last/references/last-elim is used by validrefs-not-contains, nopathex-badarrayfield,
list-last/javatypes/last-elim is used by contains-levelsubset,
list-last/javatypes/lb is used by contains-levelsubset,

Used from specification nat-basic2