Used simplifier rules/spec theorems by specification

Used from specification store

• store/javastore/Del-at is used by look-del-01,
• store/javastore/Subset is used by subset-eqval, subset-band-01, subset-band,
• store/javastore/rew is used by shift-out,
• store/javastore/subset-elem-eq-01 is used by mode-noval-subset,
• store/javastore/At-other is used by lookup-if,
• store/javastore/At-same is used by lookup-if,
• store/javastore/Del-at is used by refp,
• store/javastore/In-insert is used by uninit-type, uninit-mod, typeout, type-01, type, sk-01, sk, short-in, mode-in, mode, int-in, instore-02, instore-01, instore, init-in-01, init-in, in-01, endfinmode, byte-in, arraytype-in,

Used from specification int-basic2

• int-basic2/succ-01 is used by subset-band,

Used from specification fieldspec

• fieldspec/elim is used by all-classes-02,
• fieldspec/inj is used by short-in, shift-out, int-in, init-in, byte-in, at-other-49, at-other-48, at-other-47, at-other-46, at-other-45, at-other-44, at-other-43, at-other-42, at-other-39, at-other-38, at-other-37, at-other-36, at-other-35, at-other-34, at-other-30, at-other-29, at-other-28, at-other-27, at-other-26, at-other-25, at-other-15, at-other-14, at-other-13, at-other-12, at-other-11, at-other-10, arraytype-in, all-classes-02,
• fieldspec/inj-01 is used by at-other-type-04, at-other-type-03, at-other-type-02, at-other-type-01, at-other-type, at-other-field, at-other-class, at-other-50, at-other-09, at-other-08,
• fieldspec/sel-01 is used by all-classes-02, all-classes-01,

Used from specification int-abs

• int-abs/forward-lels is used by subset-band-01, subset-band,
• int-abs/forward-lsle is used by subset-band-01, subset-band,
• int-abs/lels-01 is used by subset-band-01, subset-band,

Used from specification string-append

• string-append/assoc is used by all-classes-02,
• string-append/chartostring-01 is used by all-classes-02,

Used from specification ostore

• ostore/javastore/inkeys-01 is used by all-classes,

Used from specification storekey

• storekey/disj is used by sk-01, sk, at-other-01, at-other,
• storekey/elim-03 is used by all-classes-02,
• storekey/inj-03 is used by short-in, shift-out, int-in, init-in, byte-in, at-other-type-04, at-other-type-03, at-other-type-02, at-other-type-01, at-other-type, at-other-field, at-other-class, at-other-50, at-other-49, at-other-48, at-other-47, at-other-46, at-other-45, at-other-44, at-other-43, at-other-42, at-other-39, at-other-38, at-other-37, at-other-36, at-other-35, at-other-34, at-other-30, at-other-29, at-other-28, at-other-27, at-other-26, at-other-25, at-other-15, at-other-14, at-other-13, at-other-12, at-other-11, at-other-10, at-other-09, at-other-08, arraytype-in, all-classes-02,
• storekey/inj-04 is used by at-other-33,
• storekey/sel-05 is used by all-classes-02, all-classes-01,
• storekey/test-05 is used by all-classes-02, all-classes-01,

Used from specification fieldname

• fieldname/inj is used by init-in-01, init-in, endfinmode, at-other-field, at-other-50, at-other-43, at-other-42, at-other-40,

Used from specification nat-basic1

• nat-basic1/f is used by all-classes-02,
• nat-basic1/ls-02 is used by all-classes-02,
• nat-basic1/one-01 is used by all-classes-02,
• nat-basic1/ref-1 is used by all-classes-02, all-classes-01,

Used from specification int-basic1

• int-basic1/lf-01 is used by subset-band-01, subset-band,
• int-basic1/ls-01 is used by subset-band-01, subset-band,
• int-basic1/trans-01 is used by subset-band-01, subset-band,

Used from specification string-less

• string-less/Length-rec is used by all-classes-02,

Used from specification set-basic

• set-basic/javastore/sel is used by all-classes-02,
• set-basic/javastore/In-empty is used by all-classes-02,
• set-basic/javastore/ne-01 is used by all-classes-01,
• set-basic/javastore/size-zero is used by all-classes-02,
• set-basic/javastore/size-zero-01 is used by all-classes-02, all-classes-01,

Used from specification refkey

• refkey/inj is used by at-other-43, at-other-39, at-other-38, at-other-37, at-other-36, at-other-35, at-other-34, at-other-30, at-other-29, at-other-28, at-other-27, at-other-26, at-other-25,
• refkey/elim is used by all-classes-02,
• refkey/inj is used by type, sk-01, sk, look-del-01, instore-02, init-in-01, in-01, all-classes-02,
• refkey/inj-01 is used by type-at, type, sk-01, sk, look-ins, length-at, instore-02, init-in-01, in-01, at-other-type-10, at-other-type-09, at-other-type-08, at-other-type-07, at-other-type-06, at-other-type-05, at-other-type-04, at-other-type-03, at-other-type-02, at-other-type-01, at-other-type, at-other-field, at-other-class-01, at-other-class, at-other-51, at-other-50, at-other-40, at-other-33, at-other-23, at-other-22, at-other-20, at-other-19, at-other-18, at-other-16, at-other-09, at-other-08, at-other-07, at-other-06, at-other-05, at-other-04, at-other-03, at-other-02, at-other-01, at-other,
• refkey/sel-02 is used by all-classes-02, all-classes-01,

Used from specification javatype

• javatype/disj-01 is used by at-other-type,
• javatype/disj-06 is used by byte-in, at-other-45, at-other-35, at-other-26, at-other-10,
• javatype/disj-09 is used by at-other-48, at-other-38, at-other-29, at-other-14,
• javatype/disj-10 is used by at-other-type-03,
• javatype/disj-13 is used by at-other-type-04,
• javatype/disj-15 is used by at-other-09, at-other-08,
• javatype/disj-21 is used by short-in, at-other-46, at-other-36, at-other-27, at-other-11,
• javatype/disj-22 is used by at-other-49, at-other-39, at-other-30, at-other-15, arraytype-in,
• javatype/disj-26 is used by int-in, at-other-44, at-other-34, at-other-25, at-other-12,
• javatype/disj-27 is used by at-other-47, at-other-37, at-other-28, at-other-13,
• javatype/disj-33 is used by at-other-type-02,
• javatype/disj-34 is used by at-other-type-01,

Used from specification specialkeys

• specialkeys/endfinallymode is used by endfinmode-in,
• specialkeys/out is used by at-other-43, at-other-39, at-other-38, at-other-37, at-other-36, at-other-35, at-other-34, at-other-30, at-other-29, at-other-28, at-other-27, at-other-26, at-other-25,
• specialkeys/diff is used by look-ins-01, at-other-31,
• specialkeys/diff-01 is used by type-01, instore, at-other-41,
• specialkeys/diff-02 is used by typeout, look-type, look-out, instore-01,
• specialkeys/diff-03 is used by uninit-mod,
• specialkeys/diff-05 is used by uninit-type,
• specialkeys/endfin-eq is used by endfinmode,
• specialkeys/len is used by length-at, at-other-18,
• specialkeys/length-02 is used by at-other-class-01,
• specialkeys/mode-02 is used by short-in, int-in, init-in, byte-in, at-other-49, at-other-48, at-other-47, at-other-46, at-other-45, at-other-44, at-other-42, at-other-15, at-other-14, at-other-13, at-other-12, at-other-11, at-other-10, arraytype-in,
• specialkeys/mode-03 is used by short-in, int-in, init-in, byte-in, at-other-49, at-other-48, at-other-47, at-other-46, at-other-45, at-other-44, at-other-42, at-other-15, at-other-14, at-other-13, at-other-12, at-other-11, at-other-10, arraytype-in,
• specialkeys/mode-04 is used by mode-in, at-other-17,
• specialkeys/mode-06 is used by mode, lookup-put-mode, at-other-21,
• specialkeys/mode-neq is used by at-mode,
• specialkeys/out-02 is used by look-out-01,
• specialkeys/out-03 is used by shift-out,
• specialkeys/out-04 is used by at-other-24,
• specialkeys/out-05 is used by at-other-32,
• specialkeys/th-01 is used by short-in, int-in, init-in, byte-in, arraytype-in,
• specialkeys/type-03 is used by type-at, type, at-other-19,
• specialkeys/type-04 is used by at-other-51,
• specialkeys/type-05 is used by init-in-01, endfinmode, at-other-40,
• specialkeys/type-07 is used by at-other-type-08, at-other-04,
• specialkeys/type-08 is used by at-other-type-10, at-other-03,
• specialkeys/type-09 is used by at-other-type-09, at-other-02,
• specialkeys/type-10 is used by at-other-type-07, at-other-05,
• specialkeys/type-11 is used by at-other-type-05, at-other-06,
• specialkeys/type-12 is used by at-other-type-06, at-other-07,
• specialkeys/type-neq is used by at-other-20,

Used from specification classname

• classname/elim is used by all-classes-02,
• classname/inj is used by at-other-class-01, at-other-class, all-classes-02,
• classname/sel is used by all-classes-02, all-classes-01,

Used from specification intops

• intops/band-commutativity is used by subset-band-01, subset-band,

Used from specification nat

• nat/fle is used by all-classes-02,
• nat/fle-01 is used by all-classes-02,
• nat/lels is used by all-classes-02,
• nat/lels-01 is used by all-classes-02,
• nat/lels-03 is used by all-classes-02,
• nat/ls-01 is used by all-classes-02,
• nat/succ-01 is used by all-classes-02,

Used from specification nat-basic2

• nat-basic2/a is used by all-classes-02,
• nat-basic2/c is used by all-classes-02,
• nat-basic2/s is used by all-classes-02,

Used from specification set-union

• set-union/javastore/del-rax is used by all-classes-02,
• set-union/javastore/del-size is used by all-classes-02,