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

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:
ac-init-firstprovedall subs proved ac-init, ac-init-03,
ac-init-otherprovedall subs proved ac-init-03,
ac-init-03provedall subs proved ac-init-04, ac-init-05,
nouninit-addclassprovedall subs proved ac-init-01, ac-init-04,
is_valid_ref-addobjprovedall subs proved addobj-isarray, is-valid-ref, is-valid-ref-stronger-def, isobj-addobj-02, add-ref, is-real-object-def, validref-addobj, is_valid_ref-def,
ac-uninitsetprovedall subs proved ac-init-04,
ac-init-11provedall subs proved ac-init-10, ac-init-09,
ac-init-08provedall subs proved ac-init-07, ac-init-06,
validref-addobjprovedall subs proved validref-isarray, validref-isobj, validref, addobj-isarray, isobj-addobj-02, is-valid-ref,
ac-initprovedall subs proved ac-in, ac-lookup-03, ac-init-02, ac-init-01, addclass-yes, ac-no1, ac-no2, addclass-base,
ac-init-09provedall subs proved ac-in-05,
ac-init-10provedall subs proved ac-in, ac-in-05,
ac-init-06provedall subs proved ac-in-05,
ac-init-07provedall subs proved ac-in, ac-in-05,
ac-init-04provedall subs proved ac-uninit, ac-in-01, ac-in-07,
ac-dups-01provedall subs proved ac-dups-03,
ac-okarraysprovedall subs proved ac-okarray-01, ac-lookup-04,
add-init-newrefprovedall subs proved ao-init,
addclass-okbytearrayprovedall subs proved addclass-okarray,
addclass-union-swprovedall subs proved ac-in-03-02, ac-refin,
addclass-validFieldsprovedall subs proved ac-refin, ac-in-03-02, ac-in-09,
addobj-addclass-swprovedall subs proved ac-lookup-05, ac-lookup-06, ac-in-01, ac-lookup-03, ac-lookup, ac-in, ac-lookup-02, ac-in-10, ac-in-11, add-ref, add-type, add-in-09, add-notin, ac-refin, ac-in-03-02, ac-lookup-04, add-in-08, add-in-04,
addobj-initprovedall subs proved ao-init,
addobj-init-01provedall subs proved ao-init,
addobj-init-02provedall subs proved ao-init,
addobj-okbytearrayprovedall subs proved add-okbar,
is_array-addobjprovedall subs proved addobj-isarray, add-ref,
is_obj-addobjprovedall subs proved isobj-addobj-02, add-ref, is-real-object-def,
isobj-addclassprovedall subs proved ac-in-03-02, ac-in-08, ac-refin, ac-lookup-04, isobj-all,
ac-dups-03provedall subs proved ac-no1, ac-no2, addclass-no2, ac-bad-02, addclass-no, ac-bad, ac-del, addclass-yes, addclass-no1,
ac-init-02provedall subs proved ac-in-04, ac-lookup-03, addclass-yes, ac-no1, ac-no2, addclass-base,
ac-init-05provedall subs proved ac-in-07,
ac-uninitprovedall subs proved ac-in-01, ac-refin,
ac-in-05provedall subs proved ac-lookup, ac-in-04,
ac-okarray-01provedall subs proved ac-refin, ac-oktype, ac-isarray, ac-lookup-04, ac-okreftype,
addclass-okarrayprovedall subs proved ac-in-10, ac-refin, ac-oktype, ac-isarray, ac-lookup-04, ac-lookup-06,
ao-initprovedall subs proved ao-init-01, ao-init-02,
add-okbarprovedall subs proved addobj-okarray,
ac-in-03-02provedall subs proved addclass-yes, ac-no1, ac-no2, ac-in-08, addclass-base, ac-in-09, ac-refin,
ac-init-01provedall subs proved ac-in, ac-in-04, ac-lookup-03, addclass-yes, ac-no1, ac-no2, addclass-base,
addobj-isarrayprovedall subs proved addobj-okarray, add-ref, add-in-04,
isobj-addobj-02provedall subs proved isobj-classtype, isobj-type-06, isobj-type-05, isobj-null-02, isobj-isobj, isobj-addobj-03, add-ref, add-in-04, is-any-object,
reffield-delprovedall subs proved has_reffield-array, isobj-del-03, has_reffield-class, is-valid-ref, validref-del-01, has_reffield-no,
nouninit-addobjprovedall subs proved ao-init-01,
isvalidref-put-array-badindexprovedall subs proved is_array-validref, validref-isobj, isobj-put-index-02, is-valid-ref, validref-put-01, is-valid-ref-stronger-def, is-real-object-def, is_obj-put-index, is_valid_ref-def,
is_valid_ref-put-samefieldprovedall subs proved instfields-special, isobj-put-badfield, isobj-put-02, validref-isobj, is-valid-ref-stronger-def, isobj-put-samefield, is-real-object-def, validref-put-samefield, is_valid_ref-def,
is_valid_ref-put-indexprovedall subs proved is_obj-put-index, is-valid-ref-stronger-def, is-real-object-def,
is_valid_ref-put-equivprovedall subs proved is-real-object-def, is_obj-put-equiv, is-valid-ref-stronger-def,
is_valid_ref-put-byteprovedall subs proved isarray-isobj-01, is_obj-put-index, is-valid-ref-stronger-def,
is_valid_ref-notin-02provedall subs proved validref-notin-02, is_valid_ref-def,
is_valid_ref-del-01provedall subs proved isobj-isarray, validref-isobj, is-valid-ref-stronger-def, isobj-del-03, is-real-object-def, validref-del-01, is_valid_ref-def,
is_valid_ref-addobj-01provedall subs proved isobj-isarray, add-type, is-real-object-def, validref-addobj-01, is_valid_ref-def,
is_obj-refval-01provedall subs proved is-real-object-def, is_obj-no-refval-03,
is_obj-refvalprovedall subs proved is-real-object-def, is_obj-no-refval-02,
is_obj-addobj-01provedall subs proved isobj-addobj-04, add-type, instfields-type, is-real-object-def,
exactarray-addobj-01provedall subs proved exactarray-addobj,
addclass-mode-inprovedall subs proved ac-in-01, ac-refin,
add-okarray-04provedall subs proved add-okarray,
add-okarray-03provedall subs proved add-okarray,
add-okarray-02provedall subs proved add-okarray,
add-okarray-01provedall subs proved add-okarray,
add-init-newref-02provedall subs proved ao-init-02,
add-init-newref-01provedall subs proved ao-init-01,
ac-okclassprovedall subs proved ac-refin, ac-lookup-04, ac-reftype,
ac-dupsprovedall subs proved ac-dups-02,
isobj-addobj-03provedall subs proved add-goodfield, add-in-07, is_obj-def,
validref-put-samefieldprovedall subs proved isobj-put-samefield, is-valid-ref, validref-put-samefield-01,
is_obj-put-equivprovedall subs proved isobj-put-samefield, isobj-put-04, is-real-object-def,
is_obj-put-indexprovedall subs proved isobj-put-index-02, is-real-object-def,
validref-notin-02provedall subs proved validref-notin,
validref-del-01provedall subs proved isobj-del-03, is-valid-ref,
validref-addobj-01provedall subs proved validref-isobj, addobj-isarray-01, validref,
is_obj-no-refval-03provedall subs proved is-real-object-def, is_obj-no-refval-01,
is_obj-no-refval-02provedall subs proved is-real-object-def, is_obj-no-refval,
isobj-addobj-04provedall subs proved validfieldinits-all, instfields-index, add-in-09, add-in-08, add-type-04, is_obj-def, add-type, instfields-type, add-type-02, is-any-object,
exactarray-addobjprovedall subs proved add-ref, add-in-04, add-in-01, add-isarray, add-in-07,
ac-in-11provedall subs proved addclass-yes, ac-no1, ac-no2, ac-refin, addclass-base,
ac-lookup-05provedall subs proved ac-lookup-04, addclass-yes, ac-no1, ac-no2, addclass-base,
ac-in-10provedall subs proved addclass-yes, ac-no1, ac-no2, ac-refin, addclass-base,
addobj-okarrayprovedall subs proved addobj-oktype, add-isarray, add-ref, add-in-04, add-okreftype,
add-okarrayprovedall subs proved add-oktype, add-ref, add-isarray, add-in-07, add-okreftype,
ao-init-02provedall subs proved add-in-07,
ao-init-01provedall subs proved add-uninit, add-in-04, add-in-07,
ac-reftypeprovedall subs proved ac-in-09,
ac-okreftypeprovedall subs proved ac-refin, ac-lookup-04,
ac-in-07provedall subs proved ac-lookup-02, ac-in-06,
ac-in-01provedall subs proved ac-in-06,
ac-in-04provedall subs proved ac-in,
ac-in-08provedall subs proved ac-in-09, addclass-yes, ac-no2, ac-no1, addclass-base,
ac-delprovedall subs proved addclass-yes, ac-no1, ac-no2, ac-del-02,
ac-dups-02provedall subs proved ac-no1, ac-no2, addclass-no2, ac-bad-02, addclass-no, addclass-yes, addclass-no1,
ac-classprovedall subs proved ac-refin, ac-lookup-04,
ac-dups-05provedall subs proved ac-bad-03, ac-bad-01, ac-del-01, addclass-yes, ac-no1, ac-no2,
ac-in-02provedall subs proved addclass-yes, ac-no1, ac-no2, ac-refin, addclass-base,
ac-in-03provedall subs proved addclass-yes, ac-no2, ac-no1, addclass-base, ac-refin,
ac-mode-01provedall subs proved ac-mode, addclass-yes, ac-no2, ac-no1, addclass-base,
ac-newrefsprovedall subs proved ac-new,
ac-okarrayprovedall subs proved ac-refin, ac-oktype, ac-isarray, ac-lookup-04,
ac-out-01provedall subs proved ac-lookup-02,
ac-typeprovedall subs proved addclass-yes, ac-no2, ac-no1, addclass-base, ac-lookup-04,
add-mode-02provedall subs proved add-mode,
add-okarray-05provedall subs proved addobj-oktype, add-ref, add-isarray, add-in-07, add-okreftype,
add-update-sameprovedall subs proved add-nput-01, add-dupput, addobj-rec-01, addobj-base,
addclass-exactarrayprovedall subs proved ac-refin, ac-in-09, ac-isarray, ac-lookup-04,
addclass-update-swprovedall subs proved addclass-switch-01,
addobj-getintarrayprovedall subs proved addobj-getintarray-01, add-ref,
addobj-initdoneprovedall subs proved addobj-initundone, addobj-initerror,
addobj-put-switch-01provedall subs proved addobj-put-switch,
addobj-throw-subsetprovedall subs proved stsubset-addobj,
addobj-union-switchprovedall subs proved addobj-put-switch,
endfinallymode-04provedall subs proved ac-lookup-02,
endfinallymode-05provedall subs proved ac-lookup-06,
instore-addobj-recprovedall subs proved add-in-07, add-in-04, add-ref,
is_array-addobj-01provedall subs proved addobj-isarray-01, add-type,
is_obj-bytearrayprovedall subs proved isobj-bytearray, is-real-object-def,
is_obj-delprovedall subs proved isobj-del-03, is-real-object-def,
is_obj-put-01provedall subs proved isobj-put-04, is-real-object-def,
is_obj-put-samefieldprovedall subs proved isobj-put-samefield, is-real-object-def,
is_obj-put-statfieldprovedall subs proved is_obj-null, isobj-null-02, isobj-put-statfield, is-real-object-def,
is_obj-updateprovedall subs proved isobj-update, is-real-object-def,
is_valid_refprovedall subs proved validref-isobj, validref, is-real-object-def, is_valid_ref-def,
is_valid_ref-02provedall subs proved is-any-object, is_obj-def, is-real-object-def, validref-02, is_valid_ref-def,
is_valid_ref-arrayprovedall subs proved is_obj-type-02, isobj-type-07, is-real-object-def, is-valid-ref-stronger-def,
is_valid_ref-newprovedall subs proved validref-new, is_valid_ref-def,
is_valid_ref-notinprovedall subs proved validref-notin, is_valid_ref-def,
is_valid_ref-putprovedall subs proved isarray-isobj, isobj-put-02, isobj-put-04, isobj-isarray, is-valid-ref, is-valid-ref-stronger-def, is-real-object-def, is_valid_ref-def,
is_valid_ref-put-01provedall subs proved validref-isobj, is-valid-ref-stronger-def, isobj-put-04, is-real-object-def, validref-put-01, is_valid_ref-def,
is_valid_ref-typeprovedall subs proved isobj-classtype, isobj-typeex, is-any-object, isobj-array-01, validref-isobj, is-real-object-def, is_valid_ref-def,
is_valid_ref-typeexprovedall subs proved isobj-array-01, isobj-type-08, isobj-isarray, isarray-isobj, is-valid-ref, is-real-object-def, is_valid_ref-def,
is_valid_ref-typeex-02provedall subs proved is_obj-typeex-02, is_valid_ref-def,
is_valid_ref-updateprovedall subs proved isobj-update, is-valid-ref, is-valid-ref-stronger-def, is-real-object-def, is_valid_ref-def,
isobj-addobjprovedall subs proved add-ref, add-in-04, add-in-07, isobj-all,
refcount-addobjprovedall subs proved add-refs,
validref-okreftypeprovedall subs proved validref-01, isarray-isobj, validref,
ac-del-02provedall subs proved addclass-yes, ac-no1, ac-no2,
ac-bad-02provedall subs proved addclass-yes, ac-no1, ac-no2, addclass-no2,
ac-badprovedall subs proved addclass-yes, ac-no1, ac-no2, addclass-no,
ac-bad-03provedall subs proved addclass-yes, ac-no1, ac-no2, addclass-base, ac-one3,
ac-bad-01provedall subs proved addclass-yes, ac-no1, ac-no2, addclass-base, ac-one2,
ac-del-01provedall subs proved addclass-yes, ac-no1, ac-no2, addclass-base, ac-del-03,
ac-in-06provedall subs proved addclass-yes, ac-no1, ac-no2, addclass-base,
ac-modeprovedall subs proved addclass-yes, ac-no2, ac-no1, addclass-base,
ac-newprovedall subs proved addclass-yes, ac-no2, ac-no1, addclass-base,
add-modeprovedall subs proved add-mode-01,
add-dupputprovedall subs proved add-in-04, add-type, add-notin, add-in-09, add-in-08, add-ref,
ac-isarrayprovedall subs proved addclass-yes, ac-no2, ac-no1, addclass-base,
addclass-switch-01provedall subs proved addclass-yes, ac-no2, ac-no1, addclass-base,
ac-in-09provedall subs proved addclass-yes, ac-no1, ac-no2, addclass-base,
ac-lookup-03provedall subs proved addclass-yes, ac-no1, ac-no2, addclass-base,
ac-lookupprovedall subs proved ac-no1, addclass-yes, ac-no2, addclass-base,
ac-inprovedall subs proved addclass-yes, ac-no2, ac-no1, addclass-base,
addobj-getintarray-01provedall subs proved addobj-getarray-01,
addobj-initundoneprovedall subs proved addobj-at-03, addobj-in,
addobj-initerrorprovedall subs proved addobj-at-03, addobj-in,
add-okreftypeprovedall subs proved add-ref, add-in-04,
stsubset-addobjprovedall subs proved add-in-03, add-in-04, add-ref,
addobj-put-switchprovedall subs proved ao-put,
add-uninitprovedall subs proved add-in-04, add-in-03,
ac-lookup-02provedall subs proved addclass-yes, ac-no1, ac-no2, addclass-base,
ac-lookup-06provedall subs proved addclass-yes, ac-no1, ac-no2, addclass-base,
isobj-bytearrayprovedall subs proved isobj-type-07, isobj-arraytype,
is_obj-no-refvalprovedall subs proved is_obj-def, isobj-instfields, is-any-object, is-real-object-def,
is_obj-no-refval-01provedall subs proved is_obj-def, isobj-instfields, is-any-object, is-real-object-def,
isobj-put-statfieldprovedall subs proved isobj-isobj-01, isobj-classtype, isobj-type-06, isobj-type-05, isobj-null-02, isobj-isobj, isobj-put-01, is-any-object,
validref-02provedall subs proved isobj-isobj, is-valid-ref,
is_obj-type-02provedall subs proved isobj-type-07, is-real-object-def,
validref-newprovedall subs proved isobj-newref-02, is-valid-ref,
isobj-put-04provedall subs proved isobj-isobj-01, isobj-classtype, isobj-type-06, isobj-type-05, isobj-null-02, isobj-isobj, isobj-put-01, is-any-object,
isobj-array-01provedall subs proved isarray-isobj, isobj-type-08,
is_obj-typeex-02provedall subs proved isobj-type-08, is-real-object-def,
isobj-updateprovedall subs proved isobj-isobj-01, isobj-classtype, isobj-type-06, isobj-type-05, isobj-null-02, isobj-isobj, isobj-update-01, is-any-object,
ac-refinprovedall subs proved addclass-yes, ac-no2, ac-no1, addclass-base,
ac-lookup-04provedall subs proved addclass-yes, ac-no1, ac-no2, addclass-base,
add-goodfieldprovedall subs proved add-ref, add-in-04,
add-in-07provedall subs proved add-ref, add-in-04,
add-type-04provedall subs proved add-type, add-type-02,
isobj-put-index-02provedall subs proved isobj-isobj-01, isobj-classtype, isobj-type-06, isobj-type-05, isobj-null-02, isobj-isobj, isobj-put-index-01, is-any-object,
add-refsprovedall subs proved add-in-02, add-in-01,
addobj-isarray-01provedall subs proved add-type,
isobj-del-03provedall subs proved isobj-classtype, isobj-type-06, isobj-type-05, isobj-null-02, isobj-isobj, isobj-del-01, is-any-object,
validref-notinprovedall subs proved isobj-notin-05, is-valid-ref,
validrefprovedall subs proved validref-isarray, validref-01,
isobj-put-samefieldprovedall subs proved isobj-put-samefield-01, is-any-object, isobj-put-samefield-03,
validref-put-samefield-01provedall subs proved isobj-put-samefield-03, is-valid-ref,
validref-putprovedall subs proved isobj-put-02, is-valid-ref,
validFields-addobjprovedall subs proved haskeys-addobj,
reffield-nullprovedall subs proved validref-null, has_reffield-no,
mode-addobjprovedall subs proved add-in-04, add-in-03,
isvalidref-arrayprovedall subs proved validref-isarray, isobj-array, validref-01,
isobj-typeprovedall subs proved isobj-type-01,
isobj-putbar-02provedall subs proved isobj-putbar-01, is-real-object-def,
isobj-modeprovedall subs proved isobj-null, isobj-put,
isobj-addobj-01provedall subs proved add-at, add-in-03, is_obj-def,
is_valid_ref-voidprovedall subs proved validref-isarray, isobj-void, is-real-object-def, is_valid_ref-def,
is_valid_ref-typeval-01provedall subs proved validref-typeval, is-real-object-def, is_valid_ref-def,
is_valid_ref-typevalprovedall subs proved validref-typeval, is_valid_ref-def,
is_valid_ref-typeex-01provedall subs proved validref-isarray, is_obj-typeex-01, is_valid_ref-def,
is_valid_ref-type-typevalprovedall subs proved isarray-isobj, isobj-type-06, isobj-isarray, is-valid-ref, is-real-object-def, is_valid_ref-def,
is_valid_ref-putbytearrayprovedall subs proved is-valid-ref, is_obj-arraytype, isobj-arraytype, is-valid-ref-stronger-def, isobj-putbar-01, is-real-object-def, is_valid_ref-def,
is_valid_ref-put-samefield-01provedall subs proved isobj-put-samefield-03, validref-isobj, is-valid-ref-stronger-def, is-real-object-def, is_valid_ref-def,
is_valid_ref-primtype-01provedall subs proved validref-primtype-01, is-real-object-def, is_valid_ref-def,
is_valid_ref-primtypeprovedall subs proved validref-primtype, is-real-object-def, is_valid_ref-def,
is_valid_ref-primarrayprovedall subs proved isobj-arraytype-02, is-valid-ref, is-real-object-def, is_valid_ref-def,
is_valid_ref-nullprovedall subs proved validref-null, is_valid_ref-def,
is_valid_ref-notin-01provedall subs proved validref-notin-01, is_valid_ref-def,
is_valid_ref-isobjprovedall subs proved validref-isobj, is_valid_ref-def, is-real-object-def,
is_valid_ref-intprovedall subs proved is_valid_ref-reftype,
is_valid_ref-field-inprovedall subs proved instfields-Object, isobj-field-in, is-real-object-def, is_valid_ref-def,
is_valid_ref-delprovedall subs proved validref-del, is_valid_ref-def,
is_valid_ref-array-01provedall subs proved is_obj-arraytype, isobj-arraytype, is-real-object-def, is-valid-ref-stronger-def,
is_valid_ref-03provedall subs proved is_valid_ref-def,
is_valid_ref-01provedall subs proved validref-isobj, is-real-object-def, is_valid_ref-def,
is_obj-union-disjointprovedall subs proved isobj-union-disjoint, is-real-object-def,
is_obj-typeleprovedall subs proved isobj-classtype, isobj-type-08, is-real-object-def,
is_obj-typeexprovedall subs proved isobj-type-08, is-real-object-def,
is_obj-put-samefield-01provedall subs proved isobj-put-samefield-03, is-real-object-def,
is_obj-putprovedall subs proved isobj-put-02, is-real-object-def,
is_obj-notin-01provedall subs proved is_obj-def, isobj-instfields, is-any-object, is-real-object-def,
is_obj-notinprovedall subs proved isobj-notin-05, is-real-object-def,
is_obj-newrefprovedall subs proved isobj-newref-02, is-real-object-def,
is_obj-isarrayprovedall subs proved isarray-isobj-01,
is_obj-field-inprovedall subs proved isobj-field-in, is-real-object-def,
is_obj-arraytype-02provedall subs proved isobj-arraytype-02, is-real-object-def,
is_obj-arraytype-01provedall subs proved isobj-arraytype-01, is-real-object-def,
is_obj-array-01provedall subs proved isarray-isobj, is-real-object-def,
instore-addobjprovedall subs proved add-notin, add-in-08, add-nput, addobj-rec-01, addobj-base,
endfinallymode-01provedall subs proved endfinallymode-02,
endfinallymodeprovedall subs proved add-in-04, add-in-03,
del-addobjprovedall subs proved add-ref, add-in-04,
addobj-union-rewprovedall subs proved add-in-04, add-in-06, add-type-02, add-type, add-in-09, add-notin, add-in-08, add-ref,
addobj-unionprovedall subs proved add-ref, add-type, add-in-09, add-notin, add-in-08, add-in-04,
addobj-typeprovedall subs proved add-type, instfields-type,
addobj-subsetprovedall subs proved addobj-at-03, addobj-in,
addobj-putprovedall subs proved ao-put,
addobj-getarrayprovedall subs proved addobj-getarray-01, add-ref,
addobj-delswprovedall subs proved add-ref, add-type, add-notin, add-in-09, add-in-08, add-in-04,
addobj-at-other-02provedall subs proved addobj-at-other,
addobj-at-other-01provedall subs proved addobj-at-other,
addobj-addobj-switchprovedall subs proved add-type, add-notin, add-in-09, add-ref, add-in-08, add-in-04,
addclass-switchprovedall subs proved addclass-yes, ac-no1, ac-no2, addclass-base,
add-type-03provedall subs proved add-type, add-ref,
add-putbar-rewprovedall subs proved add-ref, add-type, add-notin, add-in-09, add-in-08, add-in-04,
add-put-04provedall subs proved add-in-09,
add-out-02provedall subs proved ao-put,
add-outprovedall subs proved add-out-01,
add-okstoreprovedall subs proved add-in-04, add-in-01, add-type, add-type-02, add-in, add-ref, add-refin,
add-okclass-01provedall subs proved add-reftype-01, add-ref, add-in-04,
add-okclassprovedall subs proved add-type, add-type-02, add-reftype,
add-new-01provedall subs proved new-add,
add-newprovedall subs proved new-add,
add-lengthprovedall subs proved add-notin, add-ref,
add-initundoneprovedall subs proved add-nput, ao-put,
add-initerrorprovedall subs proved add-nput, ao-put,
add-initdone-01provedall subs proved add-nput, ao-put,
add-classofprovedall subs proved add-type, add-type-02,
add-classprovedall subs proved add-ref, add-in-04,
ac-shift-03provedall subs proved addclass-yes, ac-no1, ac-no2, ac-one1, addclass-base,
ac-shift-02provedall subs proved addclass-no1, addclass-yes, ac-no2, ac-no1, ac-one1, addclass-base,
ac-shiftprovedall subs proved addclass-yes, ac-no2, ac-no1, addclass-base,
ac-refsprovedall subs proved addclass-yes, ac-no2, ac-no1, addclass-base,
ac-outprovedall subs proved addclass-yes, ac-no2, ac-no1, addclass-base,
ac-getbarprovedall subs proved addclass-yes, ac-no1, ac-no2, addclass-base,
ac-dups-04provedall subs proved ac-one3, ac-one2, ac-one1, addclass-yes, ac-no1, ac-no2,
haskeys-addobjprovedall subs proved addobj-rec-01, addobj-base,
validref-01provedall subs proved is-valid-ref, validref-isobj,
isobj-arrayprovedall subs proved isobj-arraytype, isobj-null-02,
isobj-type-01provedall subs proved is_obj, isobj-jvmref,
isobj-put-samefield-01provedall subs proved isobj-null-01, is_obj-def, isobj-put-samefield-02,
isobj-nullprovedall subs proved isobj-jvmref,
isobj-isobjprovedall subs proved is_obj-def, isobj-typein, isobj-null-01, is-any-object,
add-atprovedall subs proved add-ref,
validref-typevalprovedall subs proved isobj-type-06, is-valid-ref,
isobj-typeexprovedall subs proved isobj-type-03,
isobj-putbar-01provedall subs proved isobj-type-03, is_obj-def, isobj-classtype, isobj-type-06, isobj-type-05, isobj-null-02, is-any-object, isobj-putbar,
validref-put-01provedall subs proved isobj-put-01, is-any-object, is-valid-ref,
validref-nullprovedall subs proved isobj-null-02, is-valid-ref,
validref-notin-01provedall subs proved isobj-type-05, is-valid-ref,
is_valid_ref-reftypeprovedall subs proved isobj-reftype, is-real-object-def, is-valid-ref-stronger-def,
validref-delprovedall subs proved isobj-del-04, is-valid-ref,
is_obj-arraytypeprovedall subs proved isobj-arraytype, is-real-object-def,
is_valid_ref-defprovedall subs proved is-valid-ref, validref-isobj, is-valid-ref-stronger-def, is-real-object-def,
isobj-union-disjointprovedall subs proved isobj-subset,
isobj-type-08provedall subs proved isobj-arraytype,
isobj-type-07provedall subs proved isobj-classtype,
is_obj-nullprovedall subs proved isobj-null-02, is-real-object-def,
isobj-put-samefield-03provedall subs proved isobj-put-samefield-02, isobj-classtype, isobj-type-06, isobj-type-05, isobj-null-02, is-any-object,
isobj-put-02provedall subs proved isobj-put-03, is-any-object,
isobj-notin-05provedall subs proved isobj-notin-04, is-any-object,
isobj-instfieldsprovedall subs proved isobj-type-03,
isobj-newref-02provedall subs proved isobj-newref-01, is-any-object,
isarray-isobj-01provedall subs proved isobj-isarray, is-real-object-def,
isobj-field-inprovedall subs proved instfields-subclass-01, is_obj-def, is-any-object,
isobj-arraytype-02provedall subs proved isobj-classtype,
isobj-arraytype-01provedall subs proved is-any-object, isobj-null-02,
isarray-isobjprovedall subs proved isobj-isarray,
endfinallymode-02provedall subs proved add-ref,
instfields-typeprovedall subs proved instfields-type-01,
addobj-inprovedall subs proved addobj-in-02,
addobj-at-03provedall subs proved addobj-at-01,
addobj-getarray-01provedall subs proved add-ref,
addobj-at-otherprovedall subs proved add-ref,
add-nput-01provedall subs proved addobj-rec-01, addobj-rec,
add-out-01provedall subs proved add-ref,
add-refinprovedall subs proved add-in-03,
add-inprovedall subs proved add-in-02,
add-in-01provedall subs proved add-in-02,
add-reftype-01provedall subs proved add-in-02,
add-reftypeprovedall subs proved add-in-02,
add-isarrayprovedall subs proved addobj-rec-01, addobj-base,
new-addprovedall subs proved add-in-02,
add-mode-01provedall subs proved add-ref,
ao-putprovedall subs proved addobj-rec-01, addobj-base,
add-nputprovedall subs proved addobj-rec-01, addobj-base,
add-in-09provedall subs proved addobj-rec-01, addobj-base,
add-notinprovedall subs proved addobj-rec-01, addobj-base,
add-type-02provedall subs proved add-in-08,
add-typeprovedall subs proved addobj-rec-01, addobj-base,
add-in-04provedall subs proved addobj-rec, addobj-base, add-in-02, add-in-03,
ac-del-03provedall subs proved ac-one3, ac-one1, ac-one2,
ac-no1provedall subs proved addclass-no,
add-field-01provedall subs proved addobj-base, add-one,
add-field-03provedall subs proved addobj-base, add-one,
add-ginsprovedall subs proved addobj-rec, addobj-rec-01, add-one, addobj-base,
add-in-05provedall subs proved add-in-06,
add-nput-02provedall subs proved addobj-rec-01, addobj-base, add-one,
add-oktype-02provedall subs proved add-oktype-01,
add-putprovedall subs proved addobj-base, add-one,
add-put-03provedall subs proved addobj-base, add-one,
add-put-05provedall subs proved addobj-base, add-one,
add-put-06provedall subs proved addobj-base, add-one,
add-reftype-02provedall subs proved add-in-02,
addobj-atprovedall subs proved add-ref,
addobj-at-02provedall subs proved addobj-at-01,
addobj-at-nullprovedall subs proved add-ref,
addobj-at-other-03provedall subs proved addobj-rec-01, addobj-base,
addobj-at-thisprovedall subs proved addobj-base, add-one,
addobj-at-this-01provedall subs proved addobj-base, add-one,
addobj-in-01provedall subs proved addobj-in-02,
endfinallymode-03provedall subs proved add-ref,
getByteArray-addobjectprovedall subs proved addobj-rec-01, addobj-base,
getByteArray-addobject-01provedall subs proved addobj-rec-01, addobj-base,
instfields-index-02provedall subs proved instfields-index-01,
is_obj-arrayprovedall subs proved isobj-arraytype, is-real-object-def,
is_obj-classtypeprovedall subs proved isobj-classtype, is-real-object-def,
is_obj-del-01provedall subs proved isobj-del-04, is-real-object-def,
is_obj-hasclasstypeprovedall subs proved isobj-hasclasstype, is-real-object-def,
is_obj-isobj-01provedall subs proved isobj-isobj-01, is-real-object-def,
is_obj-put-badfieldprovedall subs proved isobj-put-badfield, is-real-object-def,
is_obj-putbarprovedall subs proved isobj-putbar, is-real-object-def,
is_obj-reftypeprovedall subs proved isobj-reftype, is-real-object-def,
is_obj-subsetprovedall subs proved isobj-type-05, isobj-subset, is-real-object-def,
is_obj-typeprovedall subs proved isobj-type-05, is-real-object-def,
is_obj-type-01provedall subs proved isobj-type-06, is-real-object-def,
is_obj-unionprovedall subs proved isobj-type-05, isobj-union-01, is-real-object-def,
is_obj-validrefprovedall subs proved validref-isobj, is-real-object-def,
isobj-delprovedall subs proved isobj-all,
isobj-notinprovedall subs proved isobj-all, isobj-jvmref,
isobj-notin-01provedall subs proved is_obj, isobj-jvmref,
isobj-notin-02provedall subs proved is_obj, isobj-jvmref,
isobj-notin-03provedall subs proved isobj-notin-04,
isobj-putrefprovedall subs proved isobj-all,
isobj-recprovedall subs proved isobj-all,
isobj-type-02provedall subs proved isobj-type-03,
isobj-unionprovedall subs proved isobj-all,
newref-addobjprovedall subs proved addobj-rec-01, addobj-base,
newref-addobj-inprovedall subs proved add-in-02,
okarray-addobjprovedall subs proved addobj-rec-01, addobj-base,
valid-type-typevalprovedall subs proved isobj-type-03, is-any-object, is-valid-ref,
validfieldinits-one-01provedall subs proved validfieldinits-one,
validfieldinits-one-02provedall subs proved validfieldinits-one,
validref-reftypeprovedall subs proved isobj-reftype, is-valid-ref,
ac-one3provedall subs proved addclass-base, addclass-no2,
ac-one2provedall subs proved addclass-base, addclass-no1,
addclass-noprovedall subs proved addclass-no1,
ac-one1provedall subs proved addclass-base, addclass-yes,
add-oktypeprovedall subs proved addobj-oktype,
add-oktype-01provedall subs proved addobj-oktype,
ac-no2provedall subs proved addclass-no2,
addobj-at-01provedall subs proved addobj-keysrec, addobj-keysempty,
add-oneprovedall subs proved addobj-rec, addobj-base,
addobj-in-02provedall subs proved addobj-keysrec, addobj-keysempty,
add-in-06provedall subs proved addobj-rec,
instfields-index-01provedall subs proved instfields-index,
instfields-type-01provedall subs proved instfields-special,
isobj-hasclasstypeprovedall subs proved is-any-object,
isobj-union-01provedall subs proved is_obj-def, is-any-object,
instfields-Objectprovedall subs proved instfields-predef,
validref-primtypeprovedall subs proved is-any-object, is-valid-ref,
validref-primtype-01provedall subs proved is-any-object, is-valid-ref,
isobj-put-badfieldprovedall subs proved is_obj-def, is-any-object,
is_obj-typeex-01provedall subs proved is-any-object, is-real-object-def,
isobj-voidprovedall subs proved is-any-object,
isobj-isarrayprovedall subs proved is-any-object,
add-in-08provedall subs proved addobj-rec, addobj-base,
isobj-del-01provedall subs proved is_obj-def,
instfields-subclass-01provedall subs proved instfields-index, instfields-subclass,
isobj-typeinprovedall subs proved is_obj-def,
isobj-putprovedall subs proved is_obj,
isobj-newref-01provedall subs proved is_obj-def,
isobj-notin-04provedall subs proved is_obj-def,
isobj-put-03provedall subs proved is_obj-def,
isobj-put-index-01provedall subs proved is_obj-def,
isobj-null-01provedall subs proved is_obj-def,
isobj-put-samefield-02provedall subs proved is_obj-def,
isobj-putbarprovedall subs proved is_obj-def, is-any-object,
isobj-jvmrefprovedall subs proved is_obj,
isobj-arraytypeprovedall subs proved is-any-object,
isobj-allprovedall subs proved is_obj,
isobj-subsetprovedall subs proved is_obj-def, is-any-object,
isobj-isobj-01provedall subs proved is-any-object,
isobj-classtypeprovedall subs proved is-any-object,
isobj-update-01provedall subs proved is_obj-def,
is_array-validrefprovedall subs proved is-valid-ref,
add-in-02provedall subs proved addobj-rec, addobj-base,
addobj-rec-01provedall subs proved addobj-rec,
add-in-03provedall subs proved addobj-rec, addobj-base,
add-refprovedall subs proved addobj-rec, addobj-base,
isobj-type-03provedall subs proved is_obj-def,
validfieldinits-oneprovedall subs proved validfieldinits-all,
validref-isarrayprovedall subs proved is-valid-ref,
validref-isobjprovedall subs proved is-valid-ref,
isobj-del-04provedall subs proved is-any-object,
isobj-type-05provedall subs proved is-any-object,
isobj-null-02provedall subs proved is-any-object,
isobj-put-01provedall subs proved is_obj-def,
isobj-reftypeprovedall subs proved is-any-object,
isobj-type-06provedall subs proved is-any-object,
validref-primtype-02provedall subs proved is-any-object, is-valid-ref,
validfieldinits-recprovedall subs proved validfieldinits-all,
validfieldinits-emptyprovedall subs proved validfieldinits-all,
statfields-same-class-01provedall subs proved statfields-same-class,
statfields-index-01provedall subs proved statfields-index,
okfieldinits-oneprovedall subs proved okfieldinits-empty, okfieldinits-rec,
okfieldinits-indexprovedall subs proved okfieldinits-rec,
okfieldinits-classprovedall subs proved okfieldinits-rec, okfieldinits-empty,
okfieldinits-atprovedall subs proved okfieldinits-rec,
okfieldinits-abstractprovedall subs proved okfieldinits-rec, okfieldinits-empty,
isobj-typeleprovedall subs proved is_obj-def,
isobj-type-04provedall subs proved is_obj-def,
isobj-newrefprovedall subs proved is_obj,
isobj-fieldtypeprovedall subs proved is_obj-def,
isobj-del-02provedall subs proved is_obj-def,
is_valid_ref-type-01provedall subs proved is-real-object-def, is-valid-ref-stronger-def,
is_valid_ref-okbytearrayprovedall subs proved is-valid-ref-stronger-def,
is_valid_ref-objprovedall subs proved is-real-object-def, is-valid-ref-stronger-def,
is_valid_ref-no-arraytypeprovedall subs proved is-real-object-def, is-valid-ref-stronger-def,
is_valid_ref-isarrayprovedall subs proved is-valid-ref-stronger-def,
is_obj-putbaprovedall subs proved is_obj,
is_obj-not-tdnameexprovedall subs proved is-real-object-def,
is_obj-not-classex-02provedall subs proved is-real-object-def,
is_obj-not-classex-01provedall subs proved is-real-object-def,
is_obj-not-classexprovedall subs proved is-real-object-def,
is_obj-no-interfaceprovedall subs proved is-real-object-def,
is_obj-full-expandprovedall subs proved is_obj-def, is-any-object, is-real-object-def,
is_obj-field-norefvalprovedall subs proved is_obj-def, is-any-object, is-real-object-def,
is_obj-field-noreftypeprovedall subs proved instfields-special, is_obj-def, is-any-object, is-real-object-def,
is_obj-01provedall subs proved is-real-object-def,
instfields-subclass-inprovedall subs proved instfields-subclass,
eqmode-01provedall subs proved addobj-base,
addobj-mode-01provedall subs proved addobj-base,
addobj-modeprovedall subs proved addobj-keysempty,
addobj-keys-oneprovedall subs proved addobj-keysempty, addobj-keysrec,
add-type-01provedall subs proved addobj-base,
add-tputprovedall subs proved addobj-rec,
add-put-02provedall subs proved addobj-rec,
add-put-01provedall subs proved addobj-rec,
add-initundone-01provedall subs proved addobj-base,
add-initerror-01provedall subs proved addobj-base,
add-initdoneprovedall subs proved addobj-base,
add-initprovedall subs proved addobj-base,
add-gputprovedall subs proved addobj-rec,
add-gins-01provedall subs proved addobj-rec,
add-field-same-02provedall subs proved addobj-rec,
add-field-same-01provedall subs proved addobj-rec,
add-field-sameprovedall subs proved addobj-rec,
add-field-ifprovedall subs proved addobj-rec,
add-field-02provedall subs proved addobj-rec,
add-fieldprovedall subs proved addobj-rec,
add-at-01provedall subs proved addobj-base,
ac-shift-01provedall subs proved addclass-yes,
ac-lookup-01provedall subs proved addclass-base,
statfields-same-classaxiom
statfields-indexaxiom
has_reffield-noaxiom
has_reffield-classaxiom
has_reffield-arrayaxiom
okfieldinits-emptyaxiom
okfieldinits-recaxiom
validfieldinits-allaxiom
is-valid-ref-stronger-defaxiom
is_objaxiom
is-any-objectaxiom
is_obj-defaxiom
is-real-object-defaxiom
is-valid-refaxiom
instfields-specialaxiom
instfields-subclassaxiom
instfields-indexaxiom
instfields-predefaxiom
addobj-keysemptyaxiom
addobj-keysrecaxiom
addobj-oktypeprovedall subs proved
addobj-recaxiom
addobj-baseaxiom
ac-oktypeprovedall subs proved
addclass-no1axiom
addclass-no2axiom
addclass-baseaxiom
addclass-yesaxiom