Used simplifier rules/spec theorems by specification

Used from specification store

• store/javastore/At-other is used by lookup-put-rkvs-mode, lookup-put-ex-first, lookup-list-put-ex, initdone-uninit, init-put-nonvoid, init-put-24, at-put-other-01,
• store/javastore/Extension is used by del-switch, del-put-switch, del-put, del-notin-01,
• store/javastore/In-insert is used by in-put-rkvs,
• store/javastore/Subset is used by subset-notin, subset-delete, stsubset-new, del-subset-del, del-subset,
• store/javastore/in-neq is used by newrefs-two, newrefs-three,
• store/javastore/indef-01 is used by newref-put-01,
• store/javastore/notmemlookup is used by del-switch, del-put-switch, del-put, del-notin-01,
• store/javastore/rew is used by put-rkvs-switch, put-put-switch, lookup-put-rkvs,
• store/javastore/size-subset is used by del-refs-size,
• store/javastore/subset-put-01 is used by subset-put-notin,
• store/javastore/superset-elem-eq is used by lookup-subset, in-list-subset,
• store/javastore/superset-elem-in-01 is used by in-list-subset,
• store/javastore/At-other is used by lookup-put-rkvs-notin, lookup-put-rkvs-01, lookup-put-rkvs, init-put-04, init-06, init-05, at-put-other,
• store/javastore/At-same is used by put-put-first-01, lookup-put-ex-first, lookup-list-put-ex, at-put-same-04, at-put-same-02, at-put-same, at-put-first-04, at-put-first-02, at-put-first-01,
• store/javastore/Del-in is used by indel, del-subset-del,
• store/javastore/In-empty is used by newref-empty, maxref-exists, in-empty,
• store/javastore/In-insert is used by stsubset-new, normal-out, normal-lookup-02, normal-lookup-01, newrefs-three, newrefs-new, newref-02, new-out, new-mode-01, new-insert, instore-02, initundone-03, initundone-02, initerror-03, initdone-uninit, initdone-06, initP-put, init-put-short, init-put-nonvoid, init-put-field, init-put-24, init-put-23, init-put-22, init-put-21, init-put-20, init-put-18, init-put-17, init-put-16, init-put-15, init-put-14, init-put-13, init-put-12, init-put-11, init-put-10, init-put-09, init-put-07, init-put-06, init-put-04, init-put-03, init-put-01, init-out-02, init-out-01, init-error, init-endfmode-01, init-done-01, init-done, init-06, init-05, in-put-same, in-put-rkvs-mode, in-put-rkvs-01, in-put-keys, in-put, in-mode-put, in-list-put, del-put-switch, del-put,
• store/javastore/In-store is used by uninit-def, uninit-03, uninit-02, uninit-01, subset-put-notin, initundone-05, initundone-04, initundone-03, initundone-02, initundone-01, initerror-04, initerror-01, initdone-put-rkvs, initdone-at-type-05, initdone-at-type-04, initdone-at-type-03, initdone-at-type-02, initdone-at-type-01, initdone-at-type, initdone-06, initdone-04, initdone-03, initdone-02, initdone-01, initP-put, init-total, init-put-short, init-put-rkvs-01, init-put-notnull, init-put-nonvoid, init-put-index, init-put-24, init-put-22, init-put-21, init-put-20, init-put-19, init-put-18, init-put-17, init-put-16, init-put-15, init-put-14, init-put-13, init-put-12, init-put-11, init-put-10, init-put-09, init-put-08, init-put-07, init-put-05, init-put-04, init-put-03, init-put-02, init-put-01, init-put, init-out-02, init-out-01, init-out, init-mode-05, init-mode-04, init-mode-03, init-endfmode-01, init-endfmode, init-done-01, init-done, init-06, init-05, init-02, init-01, init,
• store/javastore/del-put is used by newref-put-01,
• store/javastore/empty is used by del-refs-size,
• store/javastore/in-pair is used by uninit-03, uninit-01, initundone-05, initundone-04, initundone-03, initundone-02, initundone-01, initerror-05, initerror-04, initdone-uninit, initdone-put-rkvs, initdone-at-type-05, initdone-at-type-04, initdone-at-type-03, initdone-at-type-02, initdone-at-type-01, initdone-at-type, initdone-06, initdone-04, initdone-03, initdone-02, initdone-01, init-total, init-put-short, init-put-rkvs-01, init-put-notnull, init-put-nonvoid, init-put-index, init-put-24, init-put-22, init-put-21, init-put-20, init-put-19, init-put-18, init-put-17, init-put-16, init-put-15, init-put-14, init-put-13, init-put-12, init-put-11, init-put-10, init-put-09, init-put-08, init-put-07, init-put-04, init-put-03, init-put-02, init-put-01, init-put, init-out-02, init-out-01, init-out, init-mode-05, init-mode-04, init-mode-03, init-error, init-endfmode-01, init-endfmode, init-done-01, init-def, init-06, init-05, init-01,
• store/javastore/insin is used by stsubset-new, initP-put, init-put-short, init-put-12, init-put-11, init-put-10, init-done,
• store/javastore/insins is used by put-rkvs-absorb, newref-put-01, lookup-put-rkvs,
• store/javastore/notmemlookup is used by subset-delete, stsubset-new, initundone-03, initundone-02, initundone-01, initerror-03, init-total, init-put-short, init-put-01, init-out-01, del-notin-01,
• store/javastore/size is used by del-refs-size,
• store/javastore/subset-elem-eq-02 is used by lookup-subset,

Used from specification list

• list/storekeys/Last is used by lookup-put-other, lookup-put-ex-first,
• list/refkeyvalues-assoclista/Nil is used by put-rkvs-append,
• list/storekeys/Nil is used by put-sks-fs-array, put-list-intro-01, put-last-rec-better, put-last-rec, mode-put-sks-array, mode-at-type-05, mode-at-type-04, mode-at-type-03, mode-at-type-02, mode-at-type-01, mode-at-type, lookup-put-ex-first, lookup-list-put-ex, lookup-list-list-append, lookup-list-intro-02, lookup-list-intro-01, lookup-list-butlast, lookup-last-rec, lookup-append, initdone-at-type-05, initdone-at-type-04, initdone-at-type-03, initdone-at-type-02, initdone-at-type-01, initdone-at-type, init-put-field-01, in-put-keys, in-mode-put, at-put-last-other, at-put-keys-01,
• list/references/Two is used by newrefs-two, newrefs-three,
• list/storekeys/a is used by put-sks-fs-array-01, put-sks-fs-array, put-rec-01, put-put-switch, put-list-intro-01, put-last-rec-better, put-last-rec, mode-put-sks-array-01, mode-put-sks-array, mode-at-type-05, mode-at-type-04, mode-at-type-03, mode-at-type-02, mode-at-type-01, mode-at-type, lookup-subset, lookup-rec-refval, lookup-rec-01, lookup-put-other, lookup-put-keys-02, lookup-put-keys, lookup-put-ex-first, lookup-list-put-ex, lookup-list-list-append, lookup-list-intro-06, lookup-list-intro-04, lookup-list-intro-03, lookup-list-intro-02, lookup-list-intro-01, lookup-list-butlast, lookup-last-rec, lookup-append, instore-two, instore-rec-01, initdone-at-type-05, initdone-at-type-04, initdone-at-type-03, initdone-at-type-02, initdone-at-type-01, initdone-at-type, init-put-field-01, in-put-keys, in-put, in-mode-put, in-list-subset, in-list-put, at-put-same-01, at-put-same, at-put-other-03, at-put-other-02, at-put-other-01, at-put-last-other-01, at-put-last-other, at-put-keys-02, at-put-keys-01, at-put-first-rec-04, at-put-first-rec-02, at-put-first-06,
• list/references/a is used by newrefs-two, newrefs-three, newrefs-rest, newrefs-rec-01, newrefs-rec, newrefs-one-01, newrefs-null, newrefs-new-01, newrefs-new, newrefs-length, newrefs-last-01, newrefs-jvmref, newrefs-in, newrefs-first, newrefs-empty, newrefs-butlast-01, newrefs-01, newrefs, newreflist-null-01, newreflist-dups-01, newref-newreflist-subset,
• list/refkeyvalues-assoclista/a is used by put-rkvs-switch-01, put-rkvs-switch, put-rkvs-rec, put-rkvs-one, put-rkvs-list-02, put-rkvs-list-01, put-rkvs-list, put-rkvs-last, put-rkvs-append, put-rkvs-absorb-01, put-rkvs-absorb, lookup-put-rkvs-notin, lookup-put-rkvs-mode, lookup-put-rkvs-diff-03, lookup-put-rkvs-diff-02, lookup-put-rkvs-diff-01, lookup-put-rkvs-diff, lookup-put-rkvs, init-put-rkvs, in-put-rkvs-mode, in-put-rkvs-01, in-put-rkvs,
• list/refkeyvalues-assoclista/app is used by put-rkvs-one,
• list/references/app is used by newrefs-one-01, newrefs-last-01,
• list/storekeys/app is used by put-put-switch, put-last-rec, lookup-subset, lookup-rec-refval, lookup-put-ex-first, lookup-list-put-ex, lookup-list-intro-02, lookup-list-intro-01, lookup-last-rec, lookup-append, instore-two, instore-rec-01, in-put, in-list-subset, in-list-put, at-put-same, at-put-other-02, at-put-other-01, at-put-last-other,
• list/references/app-01 is used by newrefs-two, newrefs-three, newrefs-rec-01, newrefs-butlast-01,
• list/storekeys/app-01 is used by lookup-put-ex-first, lookup-list-put-ex,
• list/storekeys/app-02-ant is used by put-last-rec, lookup-put-keys-02, lookup-put-ex-first, lookup-list-intro-06, lookup-list-intro-04, lookup-list-intro-03, lookup-list-intro-02, lookup-list-intro-01, lookup-last-rec, lookup-append, in-put-keys, at-put-same-01, at-put-other-03, at-put-last-other, at-put-keys-01, at-put-first-rec-04, at-put-first-rec-02, at-put-first-06,
• list/references/app-02-ant is used by newrefs-empty,
• list/storekeys/c is used by put-put-switch, put-last-rec, lookup-subset, lookup-rec-refval, lookup-put-other, lookup-put-ex-first, lookup-list-put-ex, lookup-list-intro-02, lookup-list-intro-01, lookup-last-rec, lookup-append, instore-rec-01, in-put-keys, in-put, in-list-subset, in-list-put, at-put-same, at-put-other-02, at-put-other-01, at-put-last-other, at-put-keys-01,
• list/references/c is used by newrefs-two, newrefs-three, newrefs-rest, newrefs-rec-01, newrefs-one-01, newrefs-null, newrefs-new-01, newrefs-new, newrefs-length, newrefs-last-01, newrefs-jvmref, newrefs-in, newrefs-first, newrefs-empty, newrefs-butlast-01, newreflist-dups-01, newref-newreflist-subset,
• list/refkeyvalues-assoclista/c is used by put-rkvs-append, lookup-put-rkvs-notin, lookup-put-rkvs, in-put-rkvs,
• list/storekeys/c-03 is used by in-put,
• list/storekeys/c-04 is used by lookup-put-ex-first, lookup-list-put-ex,
• list/storekeys/c-05 is used by lookup-put-ex-first,
• list/references/c-07 is used by newrefs-rest,
• list/references/c-08 is used by newrefs-rest, newrefs-first,
• list/storekeys/e is used by put-two, put-list-intro, put-last-rec, lookup-two, lookup-sk-list-append, lookup-put-keys-02, lookup-put-keys-01, lookup-put-ex-first, lookup-list-intro-06, lookup-list-intro-04, lookup-list-intro-03, lookup-list-intro-01, lookup-last-rec, in-put-keys, at-put-same-01, at-put-other-03, at-put-last-other, at-put-keys-01, at-put-first-rec-04, at-put-first-rec-03, at-put-first-rec-02, at-put-first-rec-01, at-put-first-06, at-put-first-05, at-put-first-03,
• list/references/e is used by newrefs-empty,
• list/references/e-01 is used by newrefs-jvmref,
• list/storekeys/e-01 is used by put-put-switch, put-last-rec, lookup-subset, lookup-rec-refval, lookup-put-ex-first, lookup-list-intro-02, lookup-list-intro-01, lookup-last-rec, lookup-append, instore-rec-01, in-put, in-list-subset, in-list-put, at-put-same, at-put-other-02, at-put-other-01, at-put-last-other,
• list/refkeyvalues-assoclista/e-02 is used by put-rkvs-switch, put-rkvs-last, put-rkvs-absorb,
• list/storekeys/e-02 is used by put-last-rec, lookup-put-ex-first, lookup-list-intro-01, lookup-list-butlast, lookup-last-rec, in-put-keys, in-put, at-put-last-other-01, at-put-last-other, at-put-keys-02, at-put-keys-01,
• list/storekeys/e-03 is used by lookup-put-ex-first, lookup-list-put-ex,
• list/storekeys/first is used by lookup-put-ex-first,
• list/storekeys/fr is used by put-rec-01, lookup-rec-01,
• list/references/in-06 is used by newreflist-null-01,
• list/storekeys/in-06 is used by put-put-switch, in-list-put, at-put-other-02, at-put-other-01,
• list/references/in-14 is used by newrefs-one-01, newreflist-null-01,
• list/storekeys/in-17 is used by at-put-other-03, at-put-first-03,
• list/references/in-17 is used by newrefs-rec, newrefs-one, newrefs-null, newrefs-new, newrefs-last-01, newrefs-in, newrefs-01, newrefs, newref-newreflist-subset,
• list/references/in-append is used by newrefs-rec, newrefs-null, newrefs-new, newrefs-last-01, newrefs-in, newrefs, newref-newreflist-subset,
• list/storekeys/in-append is used by at-put-other-03,
• list/storekeys/in-empty is used by put-put-switch, at-put-other-01,
• list/references/in-empty is used by newrefs-null, newrefs-new, newrefs-last-01, newrefs-in, newrefs-base, newref-newreflist-subset,
• list/storekeys/len is used by in-put, in-mode-put, at-put-last-other-01,
• list/refkeyvalues-assoclista/len is used by put-rkvs-switch, put-rkvs-absorb,
• list/references/len is used by newrefs-length,
• list/refkeyvalues-assoclista/len-02 is used by put-rkvs-switch, put-rkvs-absorb,
• list/storekeys/len-02 is used by in-put, in-mode-put, at-put-last-other-01,
• list/references/len-02 is used by newrefs-length,

Used from specification valuefuns

• valuefuns/refval-xtra is used by at-put-other-01,

Used from specification fieldspec

• fieldspec/elim is used by uninit-def, init-put-nonvoid, init-put-field, init-put-23, init-put-06, init-def,
• fieldspec/inj is used by lookup-put-rkvs-diff-03, lookup-put-keys-02, lookup-put-keys-01, initdone-uninit, initdone-06, init-put-nonvoid, init-put-field, init-put-24, init-put-22, init-put-21, init-put-20, init-put-18, init-put-17, init-put-16, init-put-15, init-put-14, init-put-13, init-put-09, init-put-07, init-put-05, init-out-02, init-out-01, init-mode-05, init-mode-04, init-endfmode-02, init-endfmode-01, init-done-01, in-put-keys-02, at-put-keys, at-put-first-rec-04, at-put-first-rec-03, at-put-first-03,
• fieldspec/inj-01 is used by lookup-put-keys-01, initdone-uninit, initdone-06, init-put-nonvoid, init-put-field, init-put-24, init-put-22, init-put-21, init-put-20, init-put-18, init-put-17, init-put-16, init-put-15, init-put-14, init-put-13, init-put-09, init-put-07, init-put-05, init-out-02, init-out-01, init-mode-05, init-endfmode-01, init-done-01, at-put-first-rec-03,
• fieldspec/sel-02 is used by uninit-def, init-put-field, init-put-23, init-put-06, init-def,
• fieldspec/sel-03 is used by uninit-def, init-put-field-01, init-put-field, init-put-23, init-put-06, init-def,

Used from specification ostore

• ostore/javastore/butmin-in is used by in-butmin,
• ostore/javastore/butmin-in is used by in-butmin-01,
• ostore/javastore/min-in is used by in-min, in-butmin,

Used from specification storekey

• storekey/disj is used by lookup-put-rkvs-diff-02, lookup-put-rkvs-diff-01, initundone-02, initerror-02, init-put-06, at-put-other-03,
• storekey/elim-03 is used by uninit-def, init-put-field, init-put-23, init-put-06, init-def,
• storekey/inj-03 is used by lookup-put-rkvs-diff-03, lookup-put-keys-02, lookup-put-keys-01, initdone-uninit, initdone-06, init-put-nonvoid, init-put-field, init-put-24, init-put-22, init-put-21, init-put-20, init-put-18, init-put-17, init-put-16, init-put-15, init-put-14, init-put-13, init-put-09, init-put-07, init-put-05, init-put-03, init-out-02, init-out-01, init-mode-05, init-mode-04, init-endfmode-02, init-endfmode-01, init-done-01, in-put-keys-02, at-put-keys, at-put-first-rec-04, at-put-first-rec-03, at-put-first-03,
• storekey/sel-05 is used by uninit-def, init-put-field-01, init-put-field, init-put-23, init-put-06, init-def,
• storekey/test is used by init-put-field, init-put-23, init-put-06,
• storekey/test-01 is used by init-put-field, init-put-23, init-put-06,
• storekey/test-05 is used by uninit-def, init-put-field-01, init-put-field, init-put-23, init-put-06, init-def,
• storekey/test-06 is used by init-put-06,
• storekey/test-07 is used by init-put-field, init-put-23, init-put-06,

Used from specification typefuns

• typefuns/tdnameex-def is used by init-put-index,

Used from specification fieldname

• fieldname/inj is used by uninit-def, lookup-put-rkvs-diff-03, lookup-put-keys-02, lookup-put-keys-01, initundone-04, initerror-04, initdone-uninit, init-put-field, init-put-23, init-put-06, init-out-02, init-out-01, init-mode-05, init-mode-04, init-endfmode-02, init-endfmode-01, init-done-01, init-def, in-put-keys-02, at-put-keys, at-put-first-rec-04, at-put-first-rec-03, at-put-first-03,

Used from specification pair

• pair/refkeyvalues/elim is used by put-rkvs-switch, put-rkvs-rec, put-rkvs-one-01, put-rkvs-last, put-rkvs-append, put-rkvs-absorb, lookup-put-rkvs-notin, lookup-put-rkvs, in-put-rkvs,

Used from specification nat-basic1

• nat-basic1/one is used by in-put, in-mode-put, at-put-last-other-01,
• nat-basic1/ref-1 is used by put-rkvs-switch, put-rkvs-absorb, del-refs-size,
• nat-basic1/z is used by newrefs-rec-01, newrefs-last-01, newrefs-jvmref, newrefs-butlast-01, newref-newreflist-subset,

Used from specification oelem

• oelem/references/ls-le is used by newref-same,

Used from specification refkey

• refkey/elim is used by uninit-def, subset-delete, ref-in, newrefs-rec, newrefs-new-01, newrefs-new, newref-put-in, newref-exists, newref-del-01, newref-del, newref-def, newref-02, new-out, new-mode-01, new-insert, init-put-field, init-put-23, init-put-06, init-def, in-list-put, in-butmin, exists-twonew, exists-fournew, delete-at,
• refkey/inj is used by put-put-switch, newrefs-two, newrefs-three, newref-put-01, lookup-put-rkvs-diff-03, lookup-put-rkvs-diff-02, lookup-put-rkvs-diff-01, lookup-put-rkvs-diff, lookup-put-ex-first, lookup-list-put-ex, initundone-04, initundone-03, initundone-02, initerror-04, initerror-03, initerror-02, initdone-06, init-put-nonvoid, init-put-24, init-put-22, init-put-21, init-put-20, init-put-18, init-put-17, init-put-16, init-put-15, init-put-14, init-put-13, init-put-09, init-put-08, init-put-07, init-put-03, init-done-01, indel, in-put-keys, in-put, in-list-put, in-butmin, del-subset-del, del-put-switch, del-put, at-put-other-01,
• refkey/inj-01 is used by newrefs-three, newrefs-new, newref-02, lookup-put-ex-first, lookup-list-put-ex, instore-02, initundone-03, initerror-03, initerror-02, initdone-06, init-put-nonvoid, init-put-field, init-put-24, init-put-23, init-put-22, init-put-21, init-put-20, init-put-18, init-put-17, init-put-16, init-put-15, init-put-14, init-put-13, init-put-09, init-put-08, init-put-07, init-put-06, init-put-03, init-done-01, in-put-keys, in-put, in-list-put, del-put-switch, at-put-other-01,
• refkey/sel-01 is used by uninit-def, stsubset-new, newrefs-rec, newrefs-new, newref-put, newref-in-03, newref-in-02, newref-in-01, newref-del, newref-def, newref-03, newref-02, new-out, new-mode-01, new-insert, init-put-field, init-put-23, init-put-06, init-def,
• refkey/sel-02 is used by uninit-def, init-put-field, init-put-23, init-put-06, init-def,

Used from specification javatype

• javatype/disj-06 is used by init-put-field-03, init-put-18, init-put-09,
• javatype/disj-09 is used by init-put-field-06, init-put-21, init-put-15,
• javatype/disj-21 is used by initdone-06, init-put-field-04, init-put-13,
• javatype/disj-22 is used by init-put-field-07, init-put-22, init-put-16,
• javatype/disj-26 is used by init-put-field-02, init-put-17, init-put-07,
• javatype/disj-27 is used by init-put-field-05, init-put-20, init-put-14,

Used from specification javavalue

• javavalue/disj-33 is used by init-put-short,
• javavalue/elim-refval is used by at-put-other-01,
• javavalue/inj-03 is used by lookup-subset-01, lookup-put-ex-first, lookup-list-put-ex,
• javavalue/inj-12 is used by uninit-02, initP-put, init-total, init-put-11, init-put-10, init-error, init-done-01, init-done, init,
• javavalue/refva-sel is used by lookup-rec-refval,
• javavalue/sel-09 is used by put-list-intro-01, put-last-rec-better, lookup-put-ex-first, lookup-list-put-ex, lookup-list-list-append, lookup-list-butlast,
• javavalue/test-125 is used by init-put-short,
• javavalue/test-68 is used by normal-return, normal-lookup-02, normal-lookup-01,
• javavalue/test-77 is used by normal-throw,

Used from specification list-dup

• list-dup/references/c is used by newrefs-one, newrefs,
• list-dup/storekeys/dups-cons is used by at-put-same,
• list-dup/references/dups-cons is used by newrefs-rec, newrefs,
• list-dup/references/e-01 is used by newrefs-base, newreflist-dups-01,
• list-dup/references/rec is used by newreflist-dups-01,

Used from specification list-data

• list-data/storekeys/lf-01 is used by in-put,
• list-data/references/elim-list-c is used by newrefs-jvmref,
• list-data/storekeys/elim-list-c is used by lookup-rec-refval, lookup-put-ex-first, in-put,
• list-data/storekeys/l is used by in-put, in-mode-put, at-put-last-other-01,
• list-data/references/l is used by newrefs-jvmref,
• list-data/references/size-01 is used by newrefs-length,

Used from specification list-del

• list-del/references/firstN-dups-04 is used by newrefs-firstn,
• list-del/references/firstN-in-04 is used by newrefs-firstn,
• list-del/references/get-zero is used by newrefs-jvmref,
• list-del/references/lastN-dups-01 is used by newrefs-lastn,
• list-del/references/lastN-in-01 is used by newrefs-lastn,

Used from specification specialkeys

• specialkeys/mode is used by mode-notin,
• specialkeys/mode-01 is used by mode-del,
• specialkeys/diff is used by normal-out,
• specialkeys/diff-04 is used by init-out-01,
• specialkeys/diff-06 is used by initundone-03,
• specialkeys/diff-07 is used by initundone-02, init-put-06,
• specialkeys/endfin-diff-02 is used by init-endfmode-01,
• specialkeys/endfin-eq is used by init-endfmode-02, init-endfmode-01,
• specialkeys/length-01 is used by initundone-03, initerror-03,
• specialkeys/length-02 is used by at-put-keys-05,
• specialkeys/mode-02 is used by init-mode-05, init-mode-04,
• specialkeys/mode-03 is used by new-mode,
• specialkeys/mode-06 is used by normal-lookup-02, normal-lookup-01, new-mode-01, lookup-put-rkvs-mode, in-put-rkvs-mode,
• specialkeys/out-02 is used by new-out,
• specialkeys/out-03 is used by init-out-02, init-out-01,
• specialkeys/th-01 is used by in-mode-put,
• specialkeys/type-05 is used by initundone-04, initerror-04, in-put-keys-01, at-put-keys-03,
• specialkeys/uninit-01 is used by init-put-23, init-put-01,
• specialkeys/uninit-02 is used by init-put-nonvoid, init-put-field, init-put-16, init-put-15, init-put-14, init-put-13, init-put-09, init-put-07,
• specialkeys/uninit-eq is used by initdone-uninit, init-put-24, init-done-01,

Used from specification javastore

• javastore/all-classes is used by uninit-def, init-def,
• javastore/at-other is used by put-sks-fs-array,
• javastore/at-other-10 is used by mode-at-type-01,
• javastore/at-other-11 is used by mode-at-type-02,
• javastore/at-other-12 is used by mode-at-type,
• javastore/at-other-13 is used by mode-at-type-03,
• javastore/at-other-14 is used by mode-at-type-04,
• javastore/at-other-15 is used by mode-at-type-05,
• javastore/at-other-16 is used by put-put-switch, lookup-put-ex-first, lookup-list-put-ex, in-list-put, at-put-other-02, at-put-keys-01, at-put-first-rec, at-put-first-02,
• javastore/at-other-17 is used by mode-put-sks-array,
• javastore/in-01 is used by instore-02, init-put-02, init-put-01, del-put,
• javastore/init-in is used by init-mode-05, init-mode-04,
• javastore/init-in-01 is used by initundone-04, initerror-04,
• javastore/instore-02 is used by init-put-24, init-put-08, init-put-03, init-done-01,
• javastore/look-del-01 is used by del-subset-del,
• javastore/look-ins is used by lookup-put-ex-first, lookup-list-put-ex, init-put-02, init-put-01, del-put, at-put-last-other,
• javastore/look-ins-01 is used by normal-out,
• javastore/lookup-if is used by stsubset-new, normal-lookup-02, normal-lookup-01, newref-put-01, initundone-04, initundone-03, initundone-02, initerror-04, initerror-03, initerror-02, initdone-06, initP-put, init-put-short, init-put-field, init-put-23, init-put-22, init-put-21, init-put-20, init-put-18, init-put-17, init-put-16, init-put-15, init-put-14, init-put-13, init-put-12, init-put-11, init-put-10, init-put-09, init-put-08, init-put-07, init-put-06, init-put-03, init-out-02, init-out-01, init-mode-05, init-mode-04, init-error, init-endfmode-01, init-done-01, init-done, del-put-switch, at-put-first,
• javastore/mode is used by mode-01,
• javastore/sk is used by initundone-02, initerror-02,
• javastore/uninit-mod is used by init-mode-04,
• javastore/uninit-type is used by initundone-04,

Used from specification assoclist

• assoclist/refkeyvalues/in-append is used by put-rkvs-absorb,
• assoclist/refkeyvalues/empty is used by put-rkvs-absorb, in-put-rkvs,
• assoclist/refkeyvalues/in-append is used by put-rkvs-switch, lookup-put-rkvs-notin, in-put-rkvs,
• assoclist/refkeyvalues/inone is used by put-rkvs-switch, put-rkvs-absorb, lookup-put-rkvs-notin, in-put-rkvs,

Used from specification classname

• classname/inj is used by in-put-keys-01, in-mode-put, at-put-keys-05, at-put-keys-03,

Used from specification reference

• reference/no-maximum is used by newref-exists, maxref-exists-01, maxref-exists, exists-twonew, exists-fournew,
• reference/totality is used by newref-same,
• reference/irreflexivity is used by newref-same, newref-exists, exists-twonew, exists-fournew,
• reference/lel-01 is used by newref-exists,
• reference/next-ls is used by newref-in,
• reference/next-neq is used by newref-jvmref,
• reference/next-neq-01 is used by newref-jvmref,
• reference/nll is used by newref-exists, maxref-exists-01, maxref-exists,
• reference/sls is used by newref-same,
• reference/transitivity is used by newref-same, newref-exists, maxref-exists-01, maxref-exists, exists-twonew, exists-fournew,

Used from specification nat

• nat/add-01 is used by newrefs-last-01, newrefs-butlast-01,
• nat/add-num-03 is used by newrefs-last-01, newrefs-butlast-01,
• nat/elim-pred-c is used by newrefs-rec-01, del-refs-size,
• nat/lels-01 is used by del-refs-size,
• nat/lep-01 is used by del-refs-size,
• nat/ler is used by del-refs-size,
• nat/let is used by del-refs-size,
• nat/pred-03 is used by newrefs-rec-01, newrefs-last-01, newrefs-butlast-01, del-refs-size,

Used from specification list-last

• list-last/references/bc is used by newrefs-butlast-01,
• list-last/references/l-02 is used by newrefs-last-01,
• list-last/storekeys/prefix-rec is used by lookup-put-ex-first,
• list-last/references/b is used by newrefs-butlast-01,
• list-last/storekeys/b is used by in-put,
• list-last/storekeys/bapp is used by in-put,
• list-last/storekeys/butlast-def is used by in-mode-put,
• list-last/references/l is used by newrefs-last-01,
• list-last/storekeys/l-02 is used by in-put,
• list-last/references/l-05 is used by newrefs-last-01,
• list-last/storekeys/l-06 is used by in-put,
• list-last/storekeys/last-def is used by in-mode-put,
• list-last/refkeyvalues-assoclista/last-elim is used by put-rkvs-switch, put-rkvs-last, put-rkvs-absorb,
• list-last/storekeys/last-elim is used by lookup-list-butlast, in-put, at-put-last-other-01, at-put-keys-02,
• list-last/references/lin-01 is used by newrefs-last-01, newrefs-last,
• list-last/storekeys/lin-02 is used by at-put-same,
• list-last/storekeys/prefix-empty is used by lookup-put-ex-first,
• list-last/storekeys/prefix-one-01 is used by lookup-put-ex-first,
• list-last/storekeys/prefix-rec-03 is used by lookup-put-ex-first,

Used from specification nat-basic2

• nat-basic2/a is used by put-rkvs-switch, put-rkvs-absorb, newrefs-rec-01, newrefs-null, newrefs-new-01, newrefs-new, newrefs-length, newrefs-last-01, newrefs-last, newrefs-empty, newrefs-butlast-01, newreflist-dups-01, newref-newreflist-subset, in-put, in-mode-put, del-refs-size, at-put-last-other-01,
• nat-basic2/c is used by put-rkvs-switch, put-rkvs-absorb, newrefs-rec-01, newrefs-null, newrefs-new-01, newrefs-new, newrefs-length, newrefs-last-01, newrefs-last, newrefs-empty, newrefs-butlast-01, newreflist-dups-01, newref-newreflist-subset, in-put, in-mode-put, del-refs-size, at-put-last-other-01,
• nat-basic2/eq-01 is used by newrefs-length,
• nat-basic2/one is used by in-put, at-put-last-other-01,
• nat-basic2/one-03 is used by in-mode-put,
• nat-basic2/oz is used by newrefs-rec-01, newrefs-last, newrefs-empty, newrefs-butlast-01, newref-newreflist-subset, in-mode-put,
• nat-basic2/pred is used by newref-newreflist-subset,
• nat-basic2/s is used by put-rkvs-switch, put-rkvs-absorb,
• nat-basic2/succ is used by newrefs-null, newrefs-new-01, newrefs-new, newrefs-length, newrefs-last-01, newrefs-in, newrefs-empty, newrefs-butlast-01, newreflist-dups-01, newref-newreflist-subset,
• nat-basic2/z-01 is used by newrefs-last-01, newrefs-butlast-01,

Used from specification initstate

• initstate/disj-01 is used by initP-put, init-done-01, init-done,
• initstate/disj-02 is used by initP-put, init-done-01, init-done,
• initstate/disj-03 is used by uninit-02, init-total, init,