[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,

Lemma dependency for Specification typefuns

A lemma (entry) may depend on lemmas (entries) below its position, but never on lemmas above its position. This means the list is a topological order of the dependency graph. An entry 'all subs proved' means that all used lemmas are (transitively) proved.

Name: Status: Subs proved? Used:
typele-elemtype-01provedall subs proved typele-elemtype,
transitivity-01provedall subs proved subclass, transitivity,
typele-elemtypeprovedall subs proved class-le, ref, jtclass, subtype-noclasstype, has-classtype, subtype-norec,
transitivityprovedall subs proved subarray1, array-le, array, dims-base, jtdims-pos, elemtype-04, elemtype-08, jtclass, hasct-04, dims-zero, subbasic1, subarray2, elemtype-rec, elemtype-base, has-classtype, subtype-norec, class-le, le-02, le-03, le-11, le-04, le-17, le-10, le-19, le-15, le-18, le-14, le-16, le-09, le-13, le-06, le-12, le-05, le-08, le-01, le-07, le,
elemtype-dims-01provedall subs proved dims-pos, dims-base, elemtype-base, mktype_rec, mkarraydims-02, dims-rec, elemtype-rec, mkarraytype-zero, elemtype-dims, mkarraydims-01,
mkarraydims-02provedall subs proved dims-succ, mkarraytype-zero, mktype_rec,
elemtype-dimsprovedall subs proved dims-pos-01, elemtype-07, dims-succ, elemtype-04, dims-zero, elemtype-06, dims-prim-09, elemtype-05, dims-prim-08, dims-prim-07, dims-prim-06, dims-prim-05, elemtype-rec, elemtype-base, dims-prim-04, elemtype-03, dims-prim-03, elemtype-02, dims-prim-02, elemtype-01, dims-prim-01, elemtype, elemtype-08, dims-prim,
subtype-noclasstypeprovedall subs proved elemtype-base, dims-base, subarray1, elemtype-rec, dims-rec, elemtype-04, subarray2, subbasic2, hasct-05, jtclass, has-classtype, dims-succ, hasct-04, dims-zero, dims-prim-09, le-03, dims-prim-08, le-04, dims-prim-07, le-10, dims-prim-06, le-15, dims-prim-05, le-14, dims-prim-04, le-09, dims-prim-03, le-06, dims-prim-02, le-05, dims-prim-01, le-01, dims-pos, dims-prim, le,
subtype-norecprovedall subs proved elemtype-base, subarray1, elemtype-rec, subarray2, hasct-05, elemtype-07, dims-succ, dims-base, subarray3, dims-pos-01, dims-rec, subclass, subbasic2, hasct-04, elemtype-04, dims-zero, hasct-07, elemtype-06, dims-prim-09, le-03, hasct-06, elemtype-05, dims-prim-08, le-04, hasct-09, dims-prim-07, le-10, hasct-11, dims-prim-06, le-15, hasct-10, dims-prim-05, le-14, hasct-08, dims-prim-04, le-09, hasct-03, elemtype-03, dims-prim-03, le-06, hasct-02, elemtype-02, dims-prim-02, le-05, hasct-01, elemtype-01, dims-prim-01, le-01, hasct, dims-pos, elemtype, jtclass, elemtype-08, has-classtype, dims-prim, le,
le-noreftype-01provedall subs proved subbasic2, is-reftype, le-noreftype,
dims-zero-01provedall subs proved hasclasstype, elemtype-08, has-classtype,
le-noreftypeprovedall subs proved subbasic1, is-reftype, ref,
dims-succprovedall subs proved dims-pos-01, dims-base, dims-rec,
elemtype-08provedall subs proved dims-pos-01, dims-base, dims-rec, elemtype-07, elemtype-04, dims-zero, elemtype-06, dims-prim-09, elemtype-05, dims-prim-08, dims-prim-07, dims-prim-06, dims-prim-05, elemtype-rec, elemtype-base, dims-prim-04, elemtype-03, dims-prim-03, elemtype-02, dims-prim-02, elemtype-01, dims-prim-01, elemtype, dims-prim,
bytearrayprovedall subs proved le-06, subarray1, le-13, array,
is_primtype-01provedall subs proved typeex-prim-07, typeex-prim-06, typeex-prim-05, typeex-prim-04, typeex-prim-03, typeex-prim-02, typeex-prim, typeex-prim-01, is_primtype,
le-hasctprovedall subs proved has-classtype, hasct-05, array, hasct-04, le-03, le-02, le-04, le-11, le-10, le-17, le-15, le-19, le-14, le-18, le-09, le-16, le-06, le-13, le-05, le-12, le-01, le-08, le, le-07,
subsups-hasct-01provedall subs proved subsups-hasct, has-classtype,
subtype-objectprovedall subs proved subarray2, typeex-array, classex-object-01, subclass, typeex-class, subbasic1,
subtype-reflexivityprovedall subs proved ref, is_subtype-level, tdnameex-def, tdname+ex-def, jtclass, has-classtype,
transitivity-02provedall subs proved class-le,
typeex-02provedall subs proved tdnameex-04, typeex-class,
typex-jtelemtypeprovedall subs proved jtelemtype-02, jtclass, has-classtype, typeex-def,
typeex-prim-03provedall subs proved hasct-03, typeex-def,
typeex-prim-02provedall subs proved hasct-02, typeex-def,
typeex-primprovedall subs proved hasct-01, typeex-def,
typeex-prim-01provedall subs proved hasct, typeex-def,
subsups-hasctprovedall subs proved elemtype-07, subsups-arr, subsups-empty-01, elemtype-04, subsups-cla, subsups-abstract, subsups-void, subsups-01, subsups-03, subsups-02, subsups, subsups-byte, subsups-short, subsups-int, subsups-bool, has-classtype,
dims-pos-01provedall subs proved dims-pos,
typeex-arrayprovedall subs proved elemtype-07, jtclass, has-classtype, hasct-05, typeex-def,
array-leprovedall subs proved subarray1, subarray2, le-02, le-11, le-17, le-19, le-18, le-16, le-13, le-12, le-08, le-07,
arrayprovedall subs proved subarray1, subarray3, le-03, le-04, le-10, le-15, le-14, le-09, le-06, le-05, le-01, le,
jtdims-posprovedall subs proved dims-base, dims-pos, dims-rec,
typeex-classprovedall subs proved elemtype-04, jtclass, hasct-04, typeex-def,
class-leprovedall subs proved subarray3, subclass, le-02, le-11, le-17, le-19, le-18, le-16, le-13, le-12, le-08, le-07,
refprovedall subs proved subarray1, subclass, le-03, le-04, le-10, le-15, le-14, le-09, le-06, le-05, le-01, le,
jtelemtype-02provedall subs proved jtelemtype, elemtype-rec, elemtype-base,
typeex-prim-08provedall subs proved hasct-06, typeex-def,
tdnameex-08provedall subs proved tdnameex, tdnameex-09,
tdnameex-06provedall subs proved tdnameex-04, typeex-01,
subtype-predefprovedall subs proved subarray3, elemtype-rec, tdname+predef-01, tdname+predef-02, tdname+predef-03, subclass, subbasic2, has-classtype, tdname+predef, elemtype-04, jtclass, hasct-04, is_subtype-level,
subtype-hasctprovedall subs proved elemtype-rec, elemtype-07, subtype-05, subtype-04, elemtype-04, subtype-07, subtype-06, subtype-09, subtype-11, subtype-10, subtype-08, subtype-03, subtype-02, subtype-01, subtype, has-classtype,
prim-classtypeprovedall subs proved has-classtype, hasct-05, hasct-04, is_primtype, hasct-07, hasct-06, hasct-09, hasct-11, hasct-10, hasct-08, hasct-03, hasct-02, hasct-01, hasct,
mkarraydimsprovedall subs proved mkarraydims-01, has-classtype,
le-biggerprovedall subs proved subarray1, elemtype-07, subarray2, elemtype-04, le-02, elemtype-06, le-11, elemtype-05, le-17, le-19, le-18, le-16, le-13, elemtype-03, le-12, elemtype-02, le-08, elemtype-01, le-07, elemtype,
hasclass-classprovedall subs proved hasclasstype, elemtype-base, has-classtype,
classex-03provedall subs proved classex-01, classex-02,
class-le-class-01provedall subs proved class-le-class, subclass,
tdnameex-09provedall subs proved tdnameex-def, tdnameex-01,
typeex-01provedall subs proved tdnameex-def, classex-def, tdnameex-01, tdname+ex-def,
tdnameex-04provedall subs proved tdnameex, classex-notpredef, classex-def, tdname+ex-def,
subtypeprovedall subs proved subtype-arr, subtype-obj, subtype-cla, isreftype-07, isreftype-06, isreftype-09, isreftype-11, isreftype-10, isreftype-08, isreftype-03, isreftype-02, isreftype-01, isreftype, subtype-other,
subtype-01provedall subs proved subtype-arr, subtype-obj, subtype-cla, isreftype-07, isreftype-06, isreftype-09, isreftype-11, isreftype-10, isreftype-08, isreftype-03, isreftype-02, isreftype-01, isreftype, subtype-other,
subtype-02provedall subs proved subtype-arr, subtype-obj, subtype-cla, isreftype-07, isreftype-06, isreftype-09, isreftype-11, isreftype-10, isreftype-08, isreftype-03, isreftype-02, isreftype-01, isreftype, subtype-other,
subtype-03provedall subs proved subtype-arr, subtype-obj, subtype-cla, isreftype-07, isreftype-06, isreftype-09, isreftype-11, isreftype-10, isreftype-08, isreftype-03, isreftype-02, isreftype-01, isreftype, subtype-other,
subtype-08provedall subs proved subtype-arr, subtype-obj, subtype-cla, is-reftype, isreftype-08, subtype-other,
subtype-10provedall subs proved subtype-arr, subtype-obj, subtype-cla, is-reftype, isreftype-10, subtype-other,
subtype-11provedall subs proved subtype-arr, subtype-obj, subtype-cla, is-reftype, isreftype-11, subtype-other,
subtype-09provedall subs proved subtype-arr, subtype-obj, subtype-cla, is-reftype, isreftype-09, subtype-other,
subtype-06provedall subs proved subtype-arr, subtype-obj, subtype-cla, isreftype-07, isreftype-06, isreftype-09, isreftype-11, isreftype-10, isreftype-08, isreftype-03, isreftype-02, isreftype-01, isreftype, subtype-other,
subtype-07provedall subs proved subtype-arr, subtype-obj, subtype-cla, isreftype-07, isreftype-06, isreftype-09, isreftype-11, isreftype-10, isreftype-08, isreftype-03, isreftype-02, isreftype-01, isreftype, subtype-other,
subtype-04provedall subs proved is-reftype, subtype-arr, subtype-cla, subtype-obj, isreftype-04, subtype-cla-01, isreftype-07, isreftype-06, isreftype-09, isreftype-11, isreftype-10, isreftype-08, isreftype-03, isreftype-02, isreftype-01, isreftype, subtype-other,
subtype-05provedall subs proved isreftype-04, subtype-arr, isreftype-05, subtype-obj, subtype-cla-01, isreftype-07, isreftype-06, isreftype-09, isreftype-11, isreftype-10, isreftype-08, isreftype-03, isreftype-02, isreftype-01, isreftype, subtype-other,
subsups-boolprovedall subs proved isreftype, subsups-other,
subsups-intprovedall subs proved isreftype-01, subsups-other,
subsups-shortprovedall subs proved isreftype-02, subsups-other,
subsups-byteprovedall subs proved isreftype-03, subsups-other,
subsupsprovedall subs proved isreftype-08, subsups-other,
subsups-02provedall subs proved isreftype-10, subsups-other,
subsups-03provedall subs proved isreftype-11, subsups-other,
subsups-01provedall subs proved isreftype-09, subsups-other,
subsups-voidprovedall subs proved isreftype-06, subsups-other,
subsups-abstractprovedall subs proved isreftype-07, subsups-other,
hasctprovedall subs proved elemtype, has-classtype,
hasct-01provedall subs proved elemtype-01, has-classtype,
hasct-02provedall subs proved elemtype-02, has-classtype,
hasct-03provedall subs proved elemtype-03, has-classtype,
hasct-06provedall subs proved elemtype-05, has-classtype,
hasct-07provedall subs proved elemtype-06, has-classtype,
hasct-04provedall subs proved elemtype-04, has-classtype,
hasct-05provedall subs proved elemtype-07, has-classtype,
jtelemtypeprovedall subs proved elemtype-07, elemtype-04, elemtype-06, elemtype-05, elemtype-base, elemtype-03, elemtype-02, elemtype-01, elemtype,
typeex-prim-04provedall subs proved hasct-08, typeex-def,
typeex-prim-05provedall subs proved hasct-10, typeex-def,
typeex-prim-06provedall subs proved hasct-11, typeex-def,
typeex-prim-07provedall subs proved hasct-09, typeex-def,
mkarraydims-01provedall subs proved elemtype-07, mktype_base, mktype_rec,
hasclasstypeprovedall subs proved elemtype-04, has-classtype,
dims-posprovedall subs proved dims-base, dims-rec, dims-zero, 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,
classex-02provedall subs proved classex-def, classex,
class-le-classprovedall subs proved subclass, subclass-01,
le-16provedall subs proved subbasic2, le-09,
le-02provedall subs proved subbasic2, le-03,
leprovedall subs proved subbasic1, le-07,
le-01provedall subs proved subbasic1, le-08,
le-05provedall subs proved subbasic1, le-12,
le-06provedall subs proved subbasic1, le-13,
le-14provedall subs proved subbasic1, le-18,
le-15provedall subs proved subbasic1, le-19,
le-10provedall subs proved subbasic1, le-17,
le-04provedall subs proved subbasic1, le-11,
is_primtype-02provedall subs proved jtelemtype-03, jtelemtype-04, jtelemtype-05, jtelemtype-06, elemtype-03, elemtype-02, elemtype-01, elemtype, is_primtype,
is_primtype-03provedall subs proved isreftype-09, isreftype-11, isreftype-10, isreftype-08, isreftype-03, isreftype-02, isreftype-01, isreftype, is_primtype,
mkarraydims-reftypeprovedall subs proved isreftype-05, mktype_rec, mktype_base,
mktype-oneprovedall subs proved mkarraytype-zero, mkdims, mktype_rec,
reftypeprovedall subs proved is-reftype, reftype-01,
subsups-emptyprovedall subs proved subsups-empty-01, subclass-other,
subtype-object-01provedall subs proved subarray2, subclass, typele-object,
tdnameex-03provedall subs proved tdname+ex-def, tdnameex-02,
tdnameex-05provedall subs proved tdnameex, tdname+ex-def,
tdnameex-07provedall subs proved tdnameex-01, tdnameex-02,
typeex-hasnoclasstypeprovedall subs proved jtclass, typeex-def, has-classtype, typeex,
subclass-01provedall subs proved subarray2, subclass, subbasic1,
classexprovedall subs proved classex-def,
classex-01provedall subs proved classex-def,
jtelemtype-03provedall subs proved elemtype-rec, elemtype-base,
jtelemtype-04provedall subs proved elemtype-rec, elemtype-base,
jtelemtype-05provedall subs proved elemtype-rec, elemtype-base,
jtelemtype-06provedall subs proved elemtype-rec, elemtype-base,
mkarraytype-zeroprovedall subs proved mktype_base,
mkdimsprovedall subs proved mktype_rec,
reftype-01provedall subs proved is-reftype,
subsups-empty-01provedall subs proved subclass-pre, subclass-other,
isreftype-04provedall subs proved is-reftype,
isreftype-05provedall subs proved is-reftype,
subtype-cla-01provedall subs proved subtype-cla,
isreftype-07provedall subs proved is-reftype,
isreftype-06provedall subs proved is-reftype,
isreftype-03provedall subs proved is-reftype,
isreftype-02provedall subs proved is-reftype,
isreftype-01provedall subs proved is-reftype,
isreftypeprovedall subs proved is-reftype,
isreftype-08provedall subs proved is-reftype,
isreftype-09provedall subs proved is-reftype,
isreftype-10provedall subs proved is-reftype,
isreftype-11provedall subs proved is-reftype,
elemtype-06provedall subs proved elemtype-rec, elemtype-base,
dims-prim-09provedall subs proved dims-base, dims-rec,
elemtype-05provedall subs proved elemtype-rec, elemtype-base,
dims-prim-08provedall subs proved dims-rec, dims-base,
dims-prim-07provedall subs proved dims-base, dims-rec,
dims-prim-06provedall subs proved dims-base, dims-rec,
dims-prim-05provedall subs proved dims-base, dims-rec,
dims-prim-04provedall subs proved dims-base, dims-rec,
elemtype-03provedall subs proved elemtype-rec, elemtype-base,
dims-prim-03provedall subs proved dims-base, dims-rec,
elemtype-02provedall subs proved elemtype-rec, elemtype-base,
dims-prim-02provedall subs proved dims-base, dims-rec,
elemtype-01provedall subs proved elemtype-rec, elemtype-base,
dims-prim-01provedall subs proved dims-base, dims-rec,
elemtypeprovedall subs proved elemtype-rec, elemtype-base,
dims-primprovedall subs proved dims-rec, dims-base,
classex-object-01provedall subs proved interfaceex-object, classex-object, tdnameex-def, tdname+ex-def,
typele-objectprovedall subs proved subbasic1,
tdname+predef-01provedall subs proved tdname+ex-def,
tdname+predef-02provedall subs proved tdname+ex-def,
tdname+predef-03provedall subs proved tdname+ex-def,
tdname+predefprovedall subs proved tdname+ex-def,
tdnameex-02provedall subs proved tdname+ex-def,
tdnameexprovedall subs proved tdnameex-def,
dims-zeroprovedall subs proved dims-rec, dims-base,
le-03provedall subs proved subbasic1,
le-11provedall subs proved subbasic2,
le-17provedall subs proved subbasic2,
le-19provedall subs proved subbasic2,
le-18provedall subs proved subbasic2,
le-09provedall subs proved subbasic1,
le-13provedall subs proved subbasic2,
le-12provedall subs proved subbasic2,
le-08provedall subs proved subbasic2,
le-07provedall subs proved subbasic2,
tdnameex-01provedall subs proved tdnameex-def,
elemtype-07provedall subs proved elemtype-base, elemtype-rec,
elemtype-04provedall subs proved elemtype-rec, elemtype-base,
typeexprovedall subs proved jtclass, typeex-def, has-classtype,
hasct-08provedall subs proved elemtype-rec, elemtype-base, has-classtype,
hasct-10provedall subs proved elemtype-base, has-classtype,
hasct-11provedall subs proved elemtype-base, has-classtype,
hasct-09provedall subs proved elemtype-base, has-classtype,
subsups-cla-01provedall subs proved subsups-cla,
subclass-pre-01provedall subs proved subclass-pre,
subclass-other-02provedall subs proved subclass-other,
subclass-other-01provedall subs proved subclass-other,
reftype-classprovedall subs proved is-reftype,
prim-voidprovedall subs proved is_primtype,
prim-shortprovedall subs proved is_primtype,
prim-longprovedall subs proved is_primtype,
prim-intprovedall subs proved is_primtype,
prim-floatprovedall subs proved is_primtype,
prim-doubleprovedall subs proved is_primtype,
prim-charprovedall subs proved is_primtype,
prim-byteprovedall subs proved is_primtype,
prim-boolprovedall subs proved is_primtype,
prim-abstractprovedall subs proved is_primtype,
mkdims-voidprovedall subs proved mktype_rec, mktype_base,
mkarraydims-typrovedall subs proved mktype_rec, mktype_base,
mkarraydims-recprovedall subs proved mktype_rec, mktype_base,
mkarraydims-arrayprovedall subs proved mktype_rec,
jtelemtype-classprovedall subs proved elemtype-rec, elemtype-base,
jtelemtype-01provedall subs proved has-classtype,
interfaceex-noclassprovedall subs proved classex-nointerface,
hasclass-noprovedall subs proved elemtype-base, is-reftype, has-classtype,
class+predefprovedall subs proved classex-def,
typeex-defaxiom
classex-notpredefaxiom
is_subtype-levelaxiom
jtclassaxiom
subtype-otheraxiom
subtype-claaxiom
subtype-objaxiom
subtype-arraxiom
subsups-arraxiom
subsups-claaxiom
subsups-otheraxiom
subclass-preaxiom
subclass-otheraxiom
mktype_baseaxiom
subbasic2axiom
subbasic1axiom
is_primtypeaxiom
classex-nointerfaceaxiom
is-reftypeaxiom
mktype_recaxiom
elemtype-baseaxiom
elemtype-recaxiom
has-classtypeaxiom
dims-recaxiom
dims-baseaxiom
tdname+ex-defaxiom
tdnameex-defaxiom
classex-objectaxiom
interfaceex-objectaxiom
subclassaxiom
classex-defaxiom
subarray2axiom
subarray3axiom
subarray1axiom