Used simplifier rules/spec theorems by specification

Used from specification list

• list/classnames/in-empty is used by subsups-empty-01, subsups-empty,

Used from specification int-basic2

• int-basic2/zero-06 is used by elemtype-dims-01,
• int-basic2/add-a is used by subtype-norec, subtype-noclasstype, mkdims, mkarraydims-rec, mkarraydims-array, mkarraydims-02, mkarraydims-01, jtdims-pos, elemtype-dims-01, elemtype-dims, elemtype-08, dims-zero, dims-succ, dims-prim-09, dims-prim-08, dims-prim-07, dims-prim-06, dims-prim-05, dims-prim-04, dims-prim-03, dims-prim-02, dims-prim-01, dims-prim, dims-pos,
• int-basic2/add-c is used by subtype-norec, subtype-noclasstype, mkdims, mkarraydims-rec, mkarraydims-array, mkarraydims-02, mkarraydims-01, jtdims-pos, elemtype-dims-01, elemtype-dims, elemtype-08, dims-zero, dims-succ, dims-prim-09, dims-prim-08, dims-prim-07, dims-prim-06, dims-prim-05, dims-prim-04, dims-prim-03, dims-prim-02, dims-prim-01, dims-prim, dims-pos,
• int-basic2/add-in is used by subtype-norec, mkarraydims-02, elemtype-dims-01, elemtype-dims, dims-succ,
• int-basic2/ax-04 is used by mkdims, mkarraydims-rec, mkarraydims-array, mkarraydims-02, elemtype-dims-01,

Used from specification intnat

• intnat/abs-pred is used by elemtype-dims-01,
• intnat/labs is used by mkarraydims-rec, mkarraydims-02, mkarraydims-01,
• intnat/rax-04 is used by mkarraydims-rec, mkarraydims-02, mkarraydims-01,

Used from specification int-abs

• int-abs/absle is used by mkarraydims-rec, mkarraydims-02, mkarraydims-01,
• int-abs/anti is used by mkarraydims-rec, mkarraydims-02,
• int-abs/ax-02 is used by typele-elemtype, transitivity, subtype-norec,
• int-abs/elim-sub is used by mkdims, mkarraydims-rec, mkarraydims-02, mkarraydims-01, elemtype-dims-01,
• int-abs/forward-le-01 is used by mkdims, mkarraydims-rec, mkarraydims-array, mkarraydims-02, mkarraydims-01, elemtype-dims-01, dims-pos,
• int-abs/forward-le-02 is used by dims-pos,
• int-abs/forward-le-05 is used by mkarraydims-rec, mkarraydims-02, mkarraydims-01, elemtype-dims-01,
• int-abs/forward-lsle is used by dims-pos,
• int-abs/lels is used by transitivity, subtype-norec, subtype-noclasstype, mkdims-void, mkarraydims-ty, mkarraydims-reftype, mkarraydims-02, mkarraydims-01, elemtype-dims-01, dims-pos,
• int-abs/lels-01 is used by subtype-norec, subtype-noclasstype, mkdims-void, mkdims, mkarraydims-ty, mkarraydims-rec, mkarraydims-array, elemtype-dims-01,
• int-abs/lels-02 is used by mkarraydims-rec, elemtype-dims-01,
• int-abs/lels-03 is used by subtype-norec, subtype-noclasstype,
• int-abs/lels-04 is used by mkdims-void, mkdims, mkarraydims-ty, mkarraydims-reftype, mkarraydims-rec, mkarraydims-array, elemtype-dims-01,
• int-abs/leone is used by elemtype-dims-01,
• int-abs/ler is used by subtype-norec,
• int-abs/mone-05 is used by jtdims-pos,
• int-abs/mone-06 is used by mkdims, mkarraydims-rec, mkarraydims-array, mkarraydims-02, mkarraydims-01, elemtype-dims-01,
• int-abs/numadd-01 is used by subtype-norec, mkarraydims-rec, elemtype-dims-01, elemtype-dims, elemtype-08, dims-zero, dims-succ, dims-prim-09, dims-prim-08, dims-prim-07, dims-prim-06, dims-prim-05, dims-prim-04, dims-prim-03, dims-prim-02, dims-prim-01, dims-prim,
• int-abs/numle-02 is used by mkarraydims-02,
• int-abs/numle-03 is used by jtdims-pos,
• int-abs/numleledel-01 is used by mkarraydims-02,
• int-abs/numls-02 is used by mkdims, mkarraydims-rec, mkarraydims-array, mkarraydims-02, mkarraydims-01, elemtype-dims-01,
• int-abs/numsub is used by mkdims, mkarraydims-rec, mkarraydims-array, elemtype-dims-01,
• int-abs/sub-add-01 is used by elemtype-dims-01,
• int-abs/sub-eq is used by elemtype-dims-01,
• int-abs/sub-le-01 is used by elemtype-dims-01,
• int-abs/succ-02 is used by subtype-norec, subtype-noclasstype,
• int-abs/zero-gels-01 is used by dims-pos,
• int-abs/zero-gs is used by mkarraydims-rec, dims-pos,

Used from specification classnamefuns

• classnamefuns/le-reflexive is used by ref,
• classnamefuns/le-object is used by subtype-object-01,
• classnamefuns/le-reflexive is used by subclass-01,
• classnamefuns/le-transitive is used by transitivity-02, transitivity,

Used from specification int-basic1

• int-basic1/irref is used by mkarraydims-rec, mkarraydims-02, mkarraydims-01,
• int-basic1/ls-01 is used by elemtype-dims-01,

Used from specification set-basic

• set-basic/classnames/ne-01 is used by subtype-hasct, subtype-04,
• set-basic/classnames/size-zero-01 is used by subtype-hasct, subtype-04,

Used from specification javatype

• javatype/ex-02 is used by subtype-object-01, subtype-object, subtype-norec, subtype-11, subtype-10, subtype-09, subtype-08, subclass-01,
• javatype/ex-03 is used by subtype-object-01, subtype-object, subtype-norec, subtype-noclasstype, subtype-hasct, subtype-11, subtype-10, subtype-09, subtype-08, hasct-08, hasclasstype,
• javatype/diff is used by jtelemtype-class,
• javatype/diff-01 is used by subclass-01,
• javatype/disj-01 is used by subtype-01, subtype,
• javatype/disj-02 is used by subtype-07, subtype-06,
• javatype/disj-03 is used by subtype-07, le-bigger, bytearray, array-le, array,
• javatype/disj-04 is used by subtype-05, subtype-04, subtype, prim-classtype, le-bigger, class-le, array-le,
• javatype/disj-05 is used by subtype, prim-classtype, le-bigger, bytearray, array-le, array,
• javatype/disj-06 is used by subtype-06, subtype-03, prim-void,
• javatype/disj-07 is used by subtype-07, subtype-05, subtype-04, le-bigger, class-le, array-le,
• javatype/disj-08 is used by subtype-07, subtype-03, prim-abstract,
• javatype/disj-09 is used by subtype-06, subtype-05, subtype-04, le-bigger, class-le, array-le,
• javatype/disj-10 is used by subtype-01, prim-classtype, le-bigger, bytearray, array-le, array,
• javatype/disj-11 is used by subtype-03, prim-classtype, le-bigger, bytearray, array-le, array,
• javatype/disj-12 is used by subtype-07, subtype-02, prim-abstract,
• javatype/disj-13 is used by subtype-05, subtype-04, subtype-01, prim-classtype, le-bigger, class-le, array-le,
• javatype/disj-14 is used by subtype-07, subtype-01, prim-abstract,
• javatype/disj-15 is used by transitivity, subtype-noclasstype, subtype-hasct, subtype-05, subtype-04, subsups-hasct, bytearray, array-le,
• javatype/disj-16 is used by subtype-05, subtype-04, subtype-02, prim-classtype, le-bigger, class-le, array-le,
• javatype/disj-17 is used by subtype-07, subtype, prim-abstract,
• javatype/disj-18 is used by subtype-07, prim-abstract,
• javatype/disj-19 is used by subtype-06, prim-void,
• javatype/disj-20 is used by subtype-09, prim-classtype, le-bigger, bytearray, array-le, array,
• javatype/disj-21 is used by subtype-06, subtype-02, prim-void,
• javatype/disj-22 is used by subtype-06, mkdims-void, le-bigger, bytearray, array-le, array,
• javatype/disj-23 is used by subtype-09, subtype-05, subtype-04, prim-classtype, class-le, array-le,
• javatype/disj-24 is used by subtype-07, prim-abstract,
• javatype/disj-25 is used by subtype-06, prim-void,
• javatype/disj-26 is used by subtype-06, subtype-01, prim-void,
• javatype/disj-27 is used by subtype-06, subtype, prim-void,
• javatype/disj-28 is used by subtype-02, prim-classtype, le-bigger, bytearray, array-le, array,
• javatype/disj-29 is used by subtype-05, subtype-04, subtype-03, prim-classtype, le-bigger, class-le, array-le,
• javatype/disj-30 is used by subtype-11, prim-classtype, le-bigger, bytearray, array-le, array,
• javatype/disj-31 is used by subtype-11, subtype-05, subtype-04, prim-classtype, class-le, array-le,
• javatype/disj-32 is used by subtype-03, subtype-02,
• javatype/disj-33 is used by subtype-03, subtype-01,
• javatype/disj-34 is used by subtype-02, subtype-01,
• javatype/disj-35 is used by subtype-03, subtype,
• javatype/disj-36 is used by subtype-02, subtype,
• javatype/disj-38 is used by subtype-07, prim-abstract,
• javatype/disj-39 is used by subtype-06, prim-void,
• javatype/disj-40 is used by subtype-10, prim-classtype, le-bigger, bytearray, array-le, array,
• javatype/disj-41 is used by subtype-10, subtype-05, subtype-04, prim-classtype, class-le, array-le,
• javatype/disj-44 is used by subtype-07, prim-abstract,
• javatype/disj-45 is used by subtype-06, prim-void,
• javatype/disj-46 is used by subtype-08, prim-classtype, le-bigger, bytearray, array-le, array,
• javatype/disj-47 is used by subtype-08, subtype-05, subtype-04, prim-classtype, hasct-08, class-le, array-le,
• javatype/disj-51 is used by subtype-03,
• javatype/disj-52 is used by subtype-03,
• javatype/disj-53 is used by subtype-03,
• javatype/disj-54 is used by subtype-03,
• javatype/disj-55 is used by subtype-02,
• javatype/disj-56 is used by subtype-02,
• javatype/disj-57 is used by subtype-02,
• javatype/disj-58 is used by subtype-02,
• javatype/disj-59 is used by subtype-01,
• javatype/disj-60 is used by subtype-01,
• javatype/disj-61 is used by subtype-01,
• javatype/disj-62 is used by subtype-01,
• javatype/disj-63 is used by subtype,
• javatype/disj-64 is used by subtype,
• javatype/disj-65 is used by subtype,
• javatype/disj-66 is used by subtype,
• javatype/elim-01 is used by transitivity, subtype-predef, subtype-norec, subtype-noclasstype, subtype-hasct, subtype-05, subsups-hasct, le-hasct, elemtype-dims-01,
• javatype/elim-02 is used by typele-elemtype, typeex-02, transitivity, subtype-predef, subtype-norec, subclass-01, jtelemtype-01, class-le-class,
• javatype/inj-01 is used by subtype-noclasstype, subtype-hasct, subtype-05, mktype-one, mkdims, mkarraydims-rec, mkarraydims-array, le-hasct, elemtype-dims-01, elemtype-dims, bytearray,
• javatype/inj-02 is used by transitivity, subtype-hasct, subtype-05, subtype-04, le-bigger, elemtype-08, class-le-class-01, class-le-class, array-le,
• javatype/sel-01 is used by subtype-hasct, subtype-05, le-hasct, elemtype-08, elemtype-07, dims-succ, dims-pos, bytearray, array-le, array,
• javatype/sel-02 is used by typeex-class, transitivity, subtype-predef, subtype-norec, subtype-noclasstype, subtype-04, subsups-cla-01, subclass-01, class-le,
• javatype/test-01 is used by subtype-04, subtype-02, le-12, le-05, isreftype-02, hasct-02, class-le,
• javatype/test-02 is used by subtype-04, subtype-03, le-13, le-06, isreftype-03, hasct-03, class-le,
• javatype/test-03 is used by subtype-05, subtype-02, le-12, le-05, jtelemtype, isreftype-02, elemtype-02, dims-prim-02, bytearray, array-le, array,
• javatype/test-04 is used by subtype-05, subtype-03, le-13, le-06, jtelemtype, isreftype-03, elemtype-03, dims-prim-03, bytearray, array-le, array,
• javatype/test-07 is used by subtype-07, subtype-04, le-03, le-02, isreftype-07, hasct-07, class-le,
• javatype/test-08 is used by subtype-07, subtype-05, le-03, le-02, jtelemtype, isreftype-07, elemtype-06, dims-prim-09, bytearray, array-le, array,
• javatype/test-09 is used by transitivity, subtype-norec, subtype-noclasstype, subtype-hasct, subtype-05, subsups-hasct, le-hasct, isreftype-05, elemtype-dims-01, elemtype-08, elemtype-07, dims-succ, dims-pos, array-le, array,
• javatype/test-10 is used by typele-object, typele-elemtype, typeex-02, transitivity, subtype-predef, subtype-object, subtype-norec, subtype-noclasstype, subtype-hasct, subtype-04, subsups-hasct, subsups-cla-01, subclass-01, isreftype-04, hasct-04, hasclasstype, class-le-class, class-le,
• javatype/test-12 is used by subtype-08, subtype-04, le-16, le-09, isreftype-08, class-le,
• javatype/test-13 is used by subtype-05, subtype-01, le-08, le-01, jtelemtype, isreftype-01, elemtype-01, dims-prim-01, bytearray, array-le, array,
• javatype/test-14 is used by subtype-05, subtype, le-07, le, jtelemtype, isreftype, elemtype, dims-prim, bytearray, array-le, array,
• javatype/test-15 is used by subtype-10, subtype-04, le-18, le-14, isreftype-10, hasct-10, class-le,
• javatype/test-16 is used by subtype-predef, subtype-norec, subtype-05, subtype-04, mkarraydims-ty, isreftype-05, class-le,
• javatype/test-18 is used by subtype-11, subtype-04, le-19, le-15, isreftype-11, hasct-11, class-le,
• javatype/test-19 is used by subtype-09, subtype-04, le-17, le-10, isreftype-09, hasct-09, class-le,
• javatype/test-20 is used by subtype-04, subtype-01, le-08, le-01, isreftype-01, hasct-01, class-le,
• javatype/test-21 is used by subtype-04, subtype, le-07, le, isreftype, hasct, class-le,
• javatype/test-22 is used by subtype-06, subtype-04, le-11, le-04, isreftype-06, hasct-06, class-le,
• javatype/test-23 is used by subtype-06, subtype-05, le-11, le-04, jtelemtype, isreftype-06, elemtype-05, dims-prim-08, bytearray, array-le, array,
• javatype/test-26 is used by subtype-08, subtype-05, le-16, le-09, jtelemtype-06, jtelemtype, isreftype-08, hasct-08, elemtype-dims, elemtype-08, dims-prim-04, bytearray, array-le, array,
• javatype/test-27 is used by subtype-10, subtype-05, le-18, le-14, jtelemtype-05, jtelemtype, isreftype-10, hasct-10, elemtype-dims, elemtype-08, dims-prim-05, bytearray, array-le, array,
• javatype/test-28 is used by transitivity, subtype-05, subtype-04, jtelemtype, elemtype-04, dims-zero, bytearray, array-le, array,
• javatype/test-31 is used by subtype-11, subtype-05, le-19, le-15, jtelemtype-04, jtelemtype, isreftype-11, hasct-11, elemtype-dims, elemtype-08, dims-prim-06, bytearray, array-le, array,
• javatype/test-32 is used by subtype-09, subtype-05, le-17, le-10, jtelemtype-03, jtelemtype, isreftype-09, hasct-09, elemtype-dims, elemtype-08, dims-prim-07, bytearray, array-le, array,

Used from specification classname

• classname/inj is used by subtype-predef, subtype-norec, subtype-noclasstype, class-le-class-01,

Used from specification predefined

• predefined/class-le-predef is used by class-le-class-01, class-le-class,
• predefined/le-01 is used by transitivity,
• predefined/le-06 is used by subtype-predef,
• predefined/obj-predefs is used by subsups-empty-01,
• predefined/predef is used by tdname+predef-01,
• predefined/predef-08 is used by tdname+predef, class+predef,
• predefined/predef-10 is used by tdname+predef-03,
• predefined/predef-13 is used by tdname+predef-02,
• predefined/subclass-object is used by classex-object-01,

Used from specification nat-basic2

• nat-basic2/a is used by mkarraydims-rec, mkarraydims-02, mkarraydims-01,
• nat-basic2/c is used by mkarraydims-rec, mkarraydims-02, mkarraydims-01,
• nat-basic2/s is used by mkarraydims-rec, mkarraydims-02, mkarraydims-01,