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: |
|---|
| validstatfield-putrkvs | proved | all subs proved
| validval-putrkvs,
validvals-putrkvs,
validvals-put-any,
validref-put-statfield-03,
validref-putrkvs,
validrefval-ref,
validrefval-def,
validval-def,
validrefkeyval-def,
validvals-one,
validvals-append,
validfield-def,
validvals-voidtype-01,
validvals-voidtype,
validstatfield-index,
validstatfield-storekey-def,
|
| validvals-putrkvs | proved | all subs proved
| validval-putrkvs,
validrefkeyvalues-def,
|
| validval-putrkvs | proved | all subs proved
| validvals-voidtype-02,
validref-putrkvs,
validrefval-ref,
validrefval-def,
validval-def,
validrefkeyval-def,
|
| initsubset-mode | proved | all subs proved
| initsubset-mode-02,
initsubset-mode-01,
initsubset-trans,
|
| initsubset-put-statfield-int | proved | all subs proved
| initsubset-put-statfield-01,
validfield-def,
validstatfield-storekey-def,
initsubset-put-statfield,
|
| okbytearray-putrkvs | proved | all subs proved
| validref-bytearray,
validref-putrkvs,
validrefnotnull-def,
validrefnotnull-bytearray,
|
| validstatfields-throw-predef-01 | proved | all subs proved
| validstatfields-throw-predef,
|
| validstatfields-throw-predef-02 | proved | all subs proved
| validstatfields-throw-predef,
|
| initsubset-mode-02 | proved | all subs proved
| validstatfield-mode,
initsubset-def,
|
| initsubset-mode-01 | proved | all subs proved
| validstatfield-mode,
initsubset-def,
|
| initsubset-put-statfield-01 | proved | all subs proved
| validstatfield-void,
validstatfield-storekey-def,
validstatfield-put-statfield,
validstatfields-put-statfield-03,
initsubset-def,
|
| validstatfields-throw-predef | proved | all subs proved
| validstatfields-addobj,
validstatfields-void,
validstatfields-put-statfield,
|
| validref-putrkvs | proved | all subs proved
| validref-put-statfield-03,
validref-put-badarrayindex,
validref-null,
validrefval-ref,
validval-def,
validrefkeyval-def,
validref-put-any-01,
validvals-put-any,
validvals-one,
validvals-append,
|
| validstatfields-put-byteval | proved | all subs proved
| validstatfields-put-byteval-01,
|
| validfieldlist-mode-01 | proved | all subs proved
| validfieldlist-mode,
|
| initsubset-initerror-04 | proved | all subs proved
| validstatfield-void,
validstatfield-put-statfield,
validstatfields-put-statfield-06,
validstatfields-put-statfield-03,
initsubset-def,
|
| validstatfields-put-statfield | proved | all subs proved
| validstatfields-put-statfield-01,
|
| validstatfields-put-byteval-01 | proved | all subs proved
| validstatfields-put-norefval-field,
|
| validvals-put-any | proved | all subs proved
| validval-put-any,
validrefkeyvalues-def,
|
| validfieldlist-mode | proved | all subs proved
| validfieldlist-put-statfield,
|
| initsubset-put-statfield | proved | all subs proved
| validstatfield-put-statfield,
validstatfields-put-statfield-02,
validstatfield-void,
initsubset-def,
validstatfield-index,
|
| validstatfield-mode | proved | all subs proved
| validfield-put-statfield-01,
validstatfield-storekey-def,
|
| validstatfields-put-statfield-03 | proved | all subs proved
| validstatfield-storekey-def,
validstatfields-storekeys-def,
validstatfields-void,
validstatfields-put-statfield-01,
|
| validstatfields-put-statfield-06 | proved | all subs proved
| validstatfield-void,
validstatfield-put-statfield,
validstatfields-storekeys-def,
validstatfields-initundone,
validstatfields-put-statfield-01,
|
| initsubset-initerror-01 | proved | all subs proved
| initsubset-initerror,
initsubset-trans,
|
| validstatfields-levelsubset | proved | all subs proved
| validstatfield-levelsubset,
validstatfields-rec,
validstatfields-empty,
|
| initsubset-initerror | proved | all subs proved
| validfield-put-statfield,
validstatfield-storekey-def,
initsubset-def,
|
| validstatfields-put-statfield-02 | proved | all subs proved
| validstatfield-put-statfield,
validstatfields-storekeys-def,
validstatfield-index,
|
| validfieldlist-put-statfield | proved | all subs proved
| validfield-put-statfield,
validfieldlist-rec,
validfieldlist-empty,
|
| validfield-put-statfield-01 | proved | all subs proved
| validfield-put-statfield,
|
| validstatfield-levelsubset | proved | all subs proved
| validfield-levelsubset,
levelsubset-tdnameex,
validstatfield-storekey-def,
|
| validstatfields-put-norefval-field | proved | all subs proved
| validstatfield-put-norefval,
validstatfield-level-expand,
|
| validstatfields-put-statfield-01 | proved | all subs proved
| validstatfield-put-statfield,
validstatfields-rec,
validstatfields-empty,
|
| validval-put-any | proved | all subs proved
| validval-field-norefval,
validref-null,
validref-put-badarrayindex,
validref-put-statfield-03,
validref-put-any-01,
validrefval-ref,
validrefval-def,
validval-def,
validrefkeyval-def,
|
| validstatfields-put-statfield-05 | proved | all subs proved
| validstatfield-put-statfield,
validstatfields-rec,
|
| validstatfields-put-statfield-04 | proved | all subs proved
| validstatfield-put-statfield,
validstatfields-rec,
|
| validstatfields-put-other-statfield | proved | all subs proved
| validstatfield-put-statfield,
validstatfield-level-expand,
|
| validstatfields-put-norefval-field-better | proved | all subs proved
| validstatfield-put-norefval,
validstatfield-level-expand,
|
| validstatfield-put-norefval | proved | all subs proved
| validref-put-norefval,
validrefval-ref,
validrefval-def,
validrefval-put-statfield-01,
validfield-def,
validstatfield-index,
validstatfield-storekey-def,
|
| validfield-levelsubset | proved | all subs proved
| validref-levelsubset-01,
validrefval-ref,
validrefval-def,
levelsubset-typeex,
validfield-def,
|
| validref-put-any-01 | proved | all subs proved
| validref-put-any,
|
| validstatfield-put-statfield | proved | all subs proved
| validrefval-put-statfield-01,
validfield-def,
validstatfield-storekey-def,
|
| validfield-put-statfield | proved | all subs proved
| validrefval-put-statfield-01,
validfield-def,
|
| initsubset-addclass-01 | proved | all subs proved
| initsubset-addclass,
initsubset-trans,
|
| initsubset-addclass | proved | all subs proved
| validstatfield-index,
validstatfield-addclass-other,
validstatfields-addclass,
initsubset-def,
|
| validref-levelsubset-01 | proved | all subs proved
| validref-levelsubset,
|
| validref-put-any | proved | all subs proved
| validref-put-array-any,
validref-put-field-any,
|
| validrefval-put-statfield-01 | proved | all subs proved
| validrefval-put-statfield,
|
| validsubset-put-statfield-02 | proved | all subs proved
| validsubset-put-statfield,
|
| validsubset-put-statfield-01 | proved | all subs proved
| validsubset-put-statfield,
|
| validsubset-addclass-01 | proved | all subs proved
| validsubset-addclass,
validsubset-trans,
|
| validstatfields-addclass-other | proved | all subs proved
| validstatfield-addclass-other,
validstatfields-storekeys-def,
|
| validstatfield-throw-predef | proved | all subs proved
| validrefval-addobj,
validrefval-put-statfield,
validfield-def,
validstatfield-index,
validstatfield-storekey-def,
|
| validrefnotnull-put-statfield-02 | proved | all subs proved
| validref-put-statfield-02,
validrefnotnull-def,
validrefnotnull-notnull,
validrefnotnull-put-statfield-01,
|
| validreflist-getarray-less-03 | proved | all subs proved
| validreflist-getarray-less-02,
|
| validreflist-getarray-less | proved | all subs proved
| validreflist-getarray-less-01,
|
| validmode-throw-predef-02 | proved | all subs proved
| validmode-throw-predef,
|
| validmode-throw-predef-01 | proved | all subs proved
| validmode-throw-predef,
|
| validmode-put-statfield-02 | proved | all subs proved
| validmode-put-statfield,
|
| validmode-put-statfield-01 | proved | all subs proved
| validmode-put-statfield,
|
| initsubset-initerror-03 | proved | all subs proved
| initsubset-initerror-02,
initsubset-trans,
|
| initsubset-addobj | proved | all subs proved
| initsubset-addobj-01,
initsubset-trans,
|
| validsubset-put-statfield | proved | all subs proved
| junkref-put-refval-statfield-01,
junkref-null,
junkref-put-statfield,
validref-put-statfield-03,
validsubset-def,
|
| validsubset-addclass | proved | all subs proved
| junkref-notin,
junkref-ac,
validref-ac,
validsubset-def,
|
| validstatfields-addobj | proved | all subs proved
| validstatfield-addobj,
validstatfields-rec,
validstatfields-empty,
|
| validrefval-put-statfield | proved | all subs proved
| validref-put-statfield-03,
validrefval-def,
|
| validref-put-statfield-02 | proved | all subs proved
| validref-null,
validref-put-statfield,
validref-put-statfield-01,
|
| validreflist-getarray-less-02 | proved | all subs proved
| validref-arrayreftype,
validref-forward-array-01,
validrefnotnull-def,
validreflist-rec,
validreflist-empty,
validrefnotnull-notnull,
|
| validreflist-getarray-less-01 | proved | all subs proved
| validref-arrayreftype,
junkref-array,
junkref-is-junk,
validref-junkref,
validref-noreftype,
validref-null,
validref-forward-array-01,
validrefnotnull-def,
validreflist-rec,
validreflist-empty,
validrefnotnull-notnull,
|
| validref-put-field-any | proved | all subs proved
| validref-put-norefval-01,
validref-put-field-refval,
|
| validref-put-array-any | proved | all subs proved
| validref-put-array-refval-02,
validref-put-array-norefval,
|
| validref-levelsubset | proved | all subs proved
| junkref-levelsubset-01,
validref-null,
validref-def,
|
| validmode-throw-predef | proved | all subs proved
| junkref-predefined,
validref-def,
validref-mode,
validmodeval-def,
validmode-def,
|
| validmode-put-statfield | proved | all subs proved
| validref-put-statfield-03,
validmodeval-def,
validmode-def,
|
| validrefnotnull-bytearray | proved | all subs proved
| validrefnotnull-primarray,
okbytearray-01,
|
| initsubset-initerror-02 | proved | all subs proved
| validrefval-ref,
validref-ac,
validrefval-def,
validfield-def,
validstatfield-storekey-def,
initsubset-def,
|
| initsubset-addobj-01 | proved | all subs proved
| validstatfield-addobj,
initsubset-def,
|
| validstatfields-addclass | proved | all subs proved
| validref-ac,
validrefval-ref,
validrefval-def,
validval-def,
validfieldinits-def,
validfield-def,
validstatfield-storekey-def,
validstatfields-storekeys-def,
|
| validstatfield-addclass-other | proved | all subs proved
| validrefval-ref,
validref-ac,
validrefval-def,
validfield-def,
validstatfield-storekey-def,
|
| validmode-addclass | proved | all subs proved
| validref-ac,
validmodeval-def,
validmode-def,
|
| validref-intarray-put-01 | proved | all subs proved
| validref-put-statfield-01,
validref-is-junk,
validref-put-array-norefval,
|
| validref-put-array-refval-03 | proved | all subs proved
| validref-put-array-refval-02,
|
| validreflist-getarray | proved | all subs proved
| validref-forward-array-01,
validref-arrayreftype,
validreflist-def,
|
| validrefnotnull-array-len-subset | proved | all subs proved
| validrefnotnull-array-01,
validrefnotnull-notnull,
validrefnotnull-array,
|
| validstatfield-addclass-same | proved | all subs proved
| validrefval-ref,
validref-ac,
validrefval-def,
validval-def,
validfield-def,
validstatfield-storekey-def,
|
| validstatfields-addobj-01 | proved | all subs proved
| validstatfield-addobj,
validstatfield-level-expand,
|
| validstatfields-subset | proved | all subs proved
| validstatfield-subset,
validstatfield-level-expand,
|
| validref-bytearray | proved | all subs proved
| validref-primarray,
validref-null,
okbytearray-02,
|
| validref-mode | proved | all subs proved
| validref-null,
validref-put-statfield,
|
| junkref-levelsubset-01 | proved | all subs proved
| junkref-levelsubset,
|
| validref-put-array-refval-02 | proved | all subs proved
| validref-put-array-refval,
|
| validref-put-field-refval | proved | all subs proved
| validref-put-refval,
|
| validref-put-statfield-01 | proved | all subs proved
| validref-null,
validref-put-statfield,
|
| validref-forward-array-01 | proved | all subs proved
| validref-forward-array,
|
| validrefnotnull-array | proved | all subs proved
| validref-array,
validrefnotnull-def,
validrefnotnull-notnull,
|
| validrefnotnull-primarray | proved | all subs proved
| validref-primarray,
validref-okarray,
validrefnotnull-def,
|
| validstatfield-addobj | proved | all subs proved
| validfield-superset,
validstatfield-storekey-def,
|
| validstatfield-subset | proved | all subs proved
| validfield-superset,
validstatfield-index,
validstatfield-storekey-def,
|
| validref-ac | proved | all subs proved
| validref-null,
validref-put-statfield,
|
| validref-put-statfield-03 | proved | all subs proved
| validref-null,
validref-put-statfield,
|
| validsubset-okbytearray-01 | proved | all subs proved
| validsubset-okbytearray,
|
| validsubset-addobj-02 | proved | all subs proved
| validsubset-addobj-01,
validsubset-trans,
|
| validstatfields-union | proved | all subs proved
| validstatfield-union,
validstatfield-level-expand,
|
| validrefkeynotnull-put-statfield | proved | all subs proved
| validrefvalnotnull-put-statfield,
validrefkeynotnull-def,
|
| validrefkeynotnull-addobj | proved | all subs proved
| validrefvalnotnull-addobj,
validrefkeynotnull-def,
|
| validref-throw | proved | all subs proved
| validref-addobj,
validref-null,
validref-put-statfield,
|
| validref-put-field-refval-01 | proved | all subs proved
| validref-put-refval,
|
| validref-put-field | proved | all subs proved
| validref-noreftype,
validref-type-forward,
validref-put-refval,
|
| validref-put-array-refval-01 | proved | all subs proved
| validref-put-array-refval,
|
| validref-class-rec-better-keep | proved | all subs proved
| validref-class-rec-better,
|
| validref-bytearray-level | proved | all subs proved
| validref-bytearray-level-01,
|
| validref-addarray-same-01 | proved | all subs proved
| validref-addarray-same,
|
| validfieldlist-superset | proved | all subs proved
| validfield-superset,
validfieldlist-rec,
validfieldlist-empty,
|
| junkref-addarray-newref-put | proved | all subs proved
| junkrefs-addarray-newref-put,
junkrefs-newref-03,
junkref-def,
|
| validsubset-okbytearray | proved | all subs proved
| okbytearray-validref,
validsubset-def,
|
| validsubset-addobj-01 | proved | all subs proved
| junkreflist-def,
validsubset-addobj,
|
| junkref-ac | proved | all subs proved
| junkref-put-statfield,
junkref-put-refval-statfield-01,
junkref-null,
|
| validstatfield-union | proved | all subs proved
| validrefval-union,
validfield-def,
validstatfield-index,
validstatfield-storekey-def,
|
| validrefnotnull-put-statfield-01 | proved | all subs proved
| validrefnotnull-put-statfield,
validrefnotnull-notnull,
|
| validrefnotnull-array-01 | proved | all subs proved
| validref-array-02,
validrefnotnull-def,
validrefnotnull-notnull,
|
| validref-array | proved | all subs proved
| validref-array-02,
|
| validref-arrayreftype | proved | all subs proved
| validref-array-rec,
validref-is-junk,
|
| validrefvalnotnull-put-statfield | proved | all subs proved
| validrefnotnull-notnull,
validrefnotnull-put-statfield,
validrefvalnotnull-def,
|
| validrefvalnotnull-addobj | proved | all subs proved
| validrefnotnull-addobj,
validrefvalnotnull-def,
|
| validref-put-refval | proved | all subs proved
| junkref-put-refval,
validref-null,
validref-def,
|
| validref-put-array-refval | proved | all subs proved
| junkref-put-refval-01,
validref-def,
|
| validref-forward-array | proved | all subs proved
| validref-supertype,
validref-array-rec,
validref-is-junk,
validref-null,
|
| validref-class-rec-better | proved | all subs proved
| validref-null,
validref-is-junk,
validref-class-rec,
|
| validref-bytearray-level-01 | proved | all subs proved
| validref-null,
okbytearray-validref,
|
| validref-primarray | proved | all subs proved
| junkrefs-primarray,
junkref-def,
validref-def,
validref-null,
validref-okarray,
|
| validref-addarray-same | proved | all subs proved
| junkref-is-junk,
junkref-addarray-03,
validref-def,
|
| validref-put-statfield | proved | all subs proved
| junkref-put-refval-statfield-01,
junkref-put-statfield,
validref-def,
|
| validfield-superset | proved | all subs proved
| validrefval-superset,
validfield-def,
|
| junkref-levelsubset | proved | all subs proved
| junkrefs-levelsubset-01,
junkref-def,
|
| junkrefs-addarray-newref-put | proved | all subs proved
| junkrefs-addarray,
junkrefs-put-ba,
|
| junkref-not-hasclasstype | proved | all subs proved
| junkref-not-hasclasstype-01,
|
| junkref-okarray-byte | proved | all subs proved
| bytearray-is-no-junk,
|
| junkref-put-ba | proved | all subs proved
| junkrefs-put-ba,
junkref-def,
|
| junkref-rec-keep-case | proved | all subs proved
| junkref-rec-case,
|
| okbytearray | proved | all subs proved
| okbytearray-01,
validrefvalnotnull-def,
validrefkeynotnull-def,
|
| validfieldinits-junkref | proved | all subs proved
| junkreflist-def,
validfieldinits-def-01,
|
| validfieldinits-validreflist | proved | all subs proved
| validref-voidtype,
validref-supertype,
validrefval-ref,
validval-def,
validreflist-rec,
validfieldinits-rec,
validreflist-empty,
validfieldinits-empty,
|
| validmode-throw-typeex | proved | all subs proved
| validref-typeex-01,
validmodeval-def,
validmode-def,
|
| validref-forward-01 | proved | all subs proved
| validref-forward,
|
| validref-hasnoclasstype-level | proved | all subs proved
| junkref-not-hasclasstype-01,
validref-def,
|
| validref-object-01 | proved | all subs proved
| validref-bad-type,
validref-supertype,
|
| validref-putrkvs-norefval | proved | all subs proved
| validref-put-norefval-equiv,
validref-put-norefval,
|
| validrefkeynotnull-addarray | proved | all subs proved
| validrefnotnull-addarray,
validrefvalnotnull-def,
validrefkeynotnull-def,
|
| validrefkeynotnull-put-byteval | proved | all subs proved
| validrefnotnull-put-byteval,
validrefnotnull-notnull,
validrefvalnotnull-def,
validrefkeynotnull-in,
validrefkeynotnull-def,
|
| validrefnotnull-addarray-01 | proved | all subs proved
| validrefnotnull-addarray,
|
| validrefnotnull-array-02 | proved | all subs proved
| validref-array-01,
validrefnotnull-def,
validrefnotnull-notnull,
|
| validrefnotnull-getarray-subset | proved | all subs proved
| validref-isarrayref,
validrefnotnull-def,
validrefnotnull-notnull,
|
| validrefnotnull-is-junk | proved | all subs proved
| validref-is-junk-better,
validrefnotnull-def,
validrefnotnull-notnull,
validrefnotnull-null,
|
| validrefnotnull-no-type | proved | all subs proved
| validref-no-type,
validrefnotnull-def,
validrefnotnull-notnull,
|
| validrefnotnull-type | proved | all subs proved
| validref-type,
validrefnotnull-def,
validrefnotnull-notnull,
|
| validrefnotnull-typeex | proved | all subs proved
| validref-typeex-01,
validrefnotnull-def,
|
| validrefnotnull-union-at-right | proved | all subs proved
| junkref-class,
junkref-is-junk,
validref-def,
validref-class,
validrefnotnull-def,
validrefnotnull-notnull,
|
| validrefvalnotnull-addarray | proved | all subs proved
| validrefnotnull-addarray,
validrefvalnotnull-def,
|
| validstatfields-put-array-norefval | proved | all subs proved
| validstatfields-validstatfield-01,
validstatfield-put-array-norefval,
validstatfield-level-expand,
|
| validsubset-predefined-01 | proved | all subs proved
| validsubset-predefined,
validsubset-trans,
|
| validsubset-predefined-02 | proved | all subs proved
| validsubset-predefined,
|
| validsubset-predefined-03 | proved | all subs proved
| validsubset-predefined,
|
| junkrefs-levelsubset-01 | proved | all subs proved
| junkrefs-levelsubset,
|
| bytearray-is-no-junk | proved | all subs proved
| junkref-array,
|
| junkref-rec-case | proved | all subs proved
| junkref-class,
junkref-array,
junkref-null,
junkref-is-junk,
|
| junkrefs-put-ba | proved | all subs proved
| junkref-array,
junkrefs-put-refval-01,
|
| validrefval-superset | proved | all subs proved
| validref-subset,
validrefval-def,
|
| validfieldinits-def-01 | proved | all subs proved
| validref-def,
validref-null,
validrefval-junkref,
validref-is-junk,
validrefval-ref,
validval-def,
junkreflist-rec,
validfieldinits-rec,
junkreflist-empty,
validfieldinits-empty,
|
| validref-voidtype | proved | all subs proved
| validref-is-junk,
validref-null,
|
| junkref-addarray-03 | proved | all subs proved
| junkref-array,
|
| validref-class-rec | proved | all subs proved
| validref-junkref,
junkref-class,
validref-def,
|
| validref-forward | proved | all subs proved
| junkref-class-01,
junkref-is-junk,
validref-def,
|
| validref-array-rec | proved | all subs proved
| validref-junkref,
junkref-array,
validref-def,
|
| junkref-not-hasclasstype-01 | proved | all subs proved
| junkref-array,
junkref-is-junk,
|
| validref-bad-type | proved | all subs proved
| validref-is-junk,
validref-null,
|
| junkref-put-refval-01 | proved | all subs proved
| junkrefs-put-null-02,
junkref-null,
validref-def,
validref-junkref,
junkrefs-junkref,
junkrefs-put-refval-02,
junkref-def,
|
| validref-put-norefval-01 | proved | all subs proved
| validref-put-norefval,
|
| junkref-put-refval | proved | all subs proved
| junkrefs-put-null-01,
junkrefs-null,
junkrefs-junkref,
junkrefs-put-refval-01,
junkref-def,
validref-def,
|
| validref-put-norefval-equiv | proved | all subs proved
| junkref-put-norefval-equiv,
validref-null,
validref-def,
validref-put-norefval,
|
| validrefnotnull-put-byteval | proved | all subs proved
| validref-put-byteval,
validrefnotnull-def,
validrefnotnull-notnull,
|
| validref-array-02 | proved | all subs proved
| validref-is-junk,
|
| validref-array-01 | proved | all subs proved
| validref-is-junk,
|
| okbytearray-01 | proved | all subs proved
| okbytearray-02,
validrefnotnull-def,
|
| validref-isarrayref | proved | all subs proved
| validref-is-junk,
|
| validref-is-junk-better | proved | all subs proved
| validref-is-junk,
|
| validref-no-type | proved | all subs proved
| validref-is-junk,
validref-null,
|
| validref-okarray | proved | all subs proved
| validref-def,
validref-is-junk,
|
| validref-type | proved | all subs proved
| validref-is-junk,
|
| validref-typeex-01 | proved | all subs proved
| validref-typeex,
|
| validref-class | proved | all subs proved
| junkref-class-01,
junkref-is-junk,
validref-def,
|
| validrefnotnull-addarray | proved | all subs proved
| validref-addarray,
validrefnotnull-def,
|
| validrefnotnull-addobj | proved | all subs proved
| validref-addobj,
validrefnotnull-notnull,
validrefnotnull-def,
|
| validrefnotnull-put-statfield | proved | all subs proved
| junkref-put-refval-statfield-01,
validref-def,
validrefnotnull-def,
validrefnotnull-notnull,
|
| validrefval-addobj | proved | all subs proved
| validref-addobj,
validrefval-def,
|
| validrefval-union | proved | all subs proved
| validref-union,
validrefval-ref,
validrefval-def,
|
| validstatfield-put-array-norefval | proved | all subs proved
| validref-put-array-norefval,
validrefval-ref,
validrefval-def,
validfield-def,
validstatfield-index,
validstatfield-storekey-def,
|
| validsubset-addobj | proved | all subs proved
| junkref-addobj-01,
validref-addobj,
validsubset-def,
|
| okbytearray-validref | proved | all subs proved
| junkref-array,
validref-def,
validref-null,
okbytearray-02,
|
| validsubset-trans | proved | all subs proved
| validref-runtimetype,
validref-junkref,
validsubset-def,
|
| validsubset-predefined | proved | all subs proved
| junkref-predefined,
validref-addobj,
validsubset-def,
|
| junkref-put-statfield | proved | all subs proved
| junkrefs-put-statfield,
junkref-def,
junkref-put-refval-statfield-01,
|
| validrefval-addarray | proved | all subs proved
| validref-addarray,
validrefval-def,
|
| validrefnotnull-subset | proved | all subs proved
| validref-subset,
validrefnotnull-def,
validrefnotnull-notnull,
|
| validrefnotnull-putbar | proved | all subs proved
| validrefnotnull-validref,
validref-put-array-norefval,
validrefnotnull-def,
validrefnotnull-notnull,
|
| validrefnotnull-no-newref | proved | all subs proved
| validref-newref,
validrefnotnull-def,
|
| validrefnotnull-no-len | proved | all subs proved
| validref-no-len,
validrefnotnull-def,
validrefnotnull-notnull,
|
| validrefnotnull-isarray | proved | all subs proved
| validref-is-junk,
validrefnotnull-def,
validrefnotnull-notnull,
|
| validrefnotnull-addarray-len | proved | all subs proved
| validref-addarray-other-01,
validrefnotnull-def,
validrefnotnull-notnull,
|
| validreflist-supertype | proved | all subs proved
| validref-supertype,
validreflist-def,
|
| validreflist-no-reftype | proved | all subs proved
| validref-null,
validref-is-junk,
validreflist-def,
|
| validreflist-addarray | proved | all subs proved
| validref-addarray,
validreflist-rec,
validreflist-empty,
|
| validrefkeynotnull-union-01 | proved | all subs proved
| validrefkeynotnull-union,
|
| validrefkeynotnull-refval-in | proved | all subs proved
| validref-notin,
validrefnotnull-def,
validrefvalnotnull-def,
validrefkeynotnull-def,
|
| validrefkeynotnull-notnewref | proved | all subs proved
| validref-newref,
validrefnotnull-def,
validrefnotnull-notnull,
validrefvalnotnull-def,
validrefkeynotnull-def,
validrefkeynotnull-notnull,
|
| validref-union-left | proved | all subs proved
| validref-subset,
|
| validref-typele | proved | all subs proved
| validref-is-junk,
|
| validref-subset-01 | proved | all subs proved
| junkref-keyin,
validref-null,
validref-def,
validref-subset,
|
| validref-refin | proved | all subs proved
| validref-null,
validref-notin,
|
| validref-putbar | proved | all subs proved
| validref-put-array-norefval,
|
| validref-put-badfield | proved | all subs proved
| junkref-put-badfield,
validref-noreftype,
validref-def,
|
| validref-put-array-norefval-01 | proved | all subs proved
| validref-put-array-norefval,
|
| validref-not-tdnameex | proved | all subs proved
| validref-is-junk,
|
| validref-no-obj | proved | all subs proved
| validref-is-junk,
validref-null,
|
| validref-newref-subset | proved | all subs proved
| validref-newref,
|
| validref-isarray | proved | all subs proved
| validref-is-junk,
|
| validref-intarray-put | proved | all subs proved
| validref-null,
validref-is-junk,
validref-put-array-norefval,
|
| validref-array-notin | proved | all subs proved
| validref-is-junk,
|
| validref-addarray-get-01 | proved | all subs proved
| validref-newref,
|
| validref-addarray-get | proved | all subs proved
| validref-newref,
|
| validmode-superset | proved | all subs proved
| validref-subset,
validmodeval-def,
validmode-def,
|
| validmode-addarray | proved | all subs proved
| validref-addarray,
validmodeval-def,
validmode-def,
|
| valid-typeex | proved | all subs proved
| validref-is-junk,
validrefnotnull-def,
validrefnotnull-notnull,
|
| nojunkref-typeex-02 | proved | all subs proved
| nojunkref-typeex-01,
|
| junkref-put-field | proved | all subs proved
| junkrefs-put-refval,
junkref-def,
|
| junkref-field-reftype | proved | all subs proved
| junkref-is-junk,
junkref-class-01,
|
| junkref-class-02 | proved | all subs proved
| junkref-noreftype,
junkref-class,
|
| junkref-addarray-04 | proved | all subs proved
| junkref-addarray-newref,
validref-def,
validref-notin,
validreflist-def,
junkref-array,
|
| validref-runtimetype | proved | all subs proved
| validref-def,
validref-junkref,
|
| validstatfields-validstatfield-01 | proved | all subs proved
| validstatfield-level-expand,
|
| validref-union | proved | all subs proved
| junkref-union,
junkref-keyin,
validref-null,
validref-def,
|
| validref-put-byteval | proved | all subs proved
| junkref-put-norefval,
validref-null,
validref-def,
|
| validref-no-len | proved | all subs proved
| validref-array-len-in,
validref-null,
|
| validref-addarray-other-01 | proved | all subs proved
| junkref-newref,
junkref-addarray-02,
validref-def,
|
| validrefkeynotnull-union | proved | all subs proved
| junkref-union,
junkref-keyin,
validref-def,
validrefnotnull-def,
validrefnotnull-notnull,
validrefvalnotnull-def,
validrefkeynotnull-def,
|
| validref-typeex | proved | all subs proved
| nojunkref-typeex,
validref-def,
|
| validref-addobj | proved | all subs proved
| junkref-newref,
junkref-addobj,
validref-null,
validref-def,
|
| validref-put-badarrayindex | proved | all subs proved
| junkref-put-badarrayindex,
validref-null,
validref-def,
|
| validref-put-norefval | proved | all subs proved
| junkref-put-norefval,
validref-def,
|
| validref-noreftype | proved | all subs proved
| junkref-noreftype,
validref-def,
|
| validref-put-array-norefval | proved | all subs proved
| junkref-put-array-norefval,
validref-null,
validref-def,
|
| validref-newref | proved | all subs proved
| junkref-newref,
validref-def,
|
| junkref-predefined | proved | all subs proved
| junkref-addobj-01,
|
| validref-subset | proved | all subs proved
| junkref-subset,
junkref-keyin,
validref-null,
validref-def,
|
| validref-addarray | proved | all subs proved
| junkref-newref,
junkref-addarray-newref,
validref-null,
validref-def,
|
| validref-supertype | proved | all subs proved
| validref-junkref,
validref-def,
|
| validrefval-junkref | proved | all subs proved
| validref-junkref,
validrefval-ref,
junkref-null,
|
| validref-is-junk | proved | all subs proved
| junkref-not-valid-01,
validref-def,
|
| okbytearray-02 | proved | all subs proved
| junkref-okbytearray,
validref-def,
|
| nojunkref-typeex-01 | proved | all subs proved
| nojunkref-typeex,
|
| junkrefs-levelsubset | proved | all subs proved
| levelsubset-is-array,
junkrefs-array,
levelsubset-is-obj,
junkrefs-class,
junkrefs-is-junk,
junkrefs-null,
junkrefs-empty,
|
| junkrefs-put-refval-02 | proved | all subs proved
| junkrefs-sametype,
junkref-def,
junkref-noreftype,
junkrefs-array,
junkrefs-class,
junkrefs-is-junk,
junkrefs-null,
junkrefs-empty,
|
| junkrefs-put-refval-01 | proved | all subs proved
| junkrefs-array,
junkrefs-subtype,
junkref-def,
junkref-noreftype,
junkrefs-class,
junkrefs-is-junk,
junkrefs-null-02,
junkrefs-put-notin,
junkrefs-empty,
|
| junkrefs-put-refval | proved | all subs proved
| junkrefs-array,
junkrefs-subtype,
junkref-def,
junkref-noreftype,
junkrefs-class,
junkrefs-is-junk,
junkrefs-null-02,
junkrefs-put-notin,
junkrefs-empty,
|
| junkref-class-01 | proved | all subs proved
| junkrefs-runtimetype,
junkrefs-one,
junkrefs-subtype,
junkrefs-null-02,
junkrefs-class,
junkref-def,
|
| junkref-class | proved | all subs proved
| junkrefs-runtimetype,
junkrefs-one,
junkrefs-subtype,
junkrefs-null-02,
junkrefs-class,
junkref-def,
|
| validref-notin | proved | all subs proved
| junkref-notin,
validref-def,
|
| junkref-put-refval-statfield-01 | proved | all subs proved
| junkref-put-refval-statfield,
|
| junkref-array | proved | all subs proved
| junkrefs-runtimetype,
junkrefs-one,
junkrefs-subtype,
junkrefs-null-02,
junkrefs-array,
junkref-def,
|
| junkref-addbytearray | proved | all subs proved
| junkref-addarray-noreftype,
|
| junkref-not-okreftype-01 | proved | all subs proved
| junkref-null,
junkref-is-junk,
junkref-not-okreftype,
|
| junkref-notypeex | proved | all subs proved
| nojunkref-typeex,
|
| junkref-putbar | proved | all subs proved
| junkref-put-array-norefval,
|
| junkref-putbar-01 | proved | all subs proved
| junkref-put-array-norefval,
|
| junkref-union-disjoint | proved | all subs proved
| junkrefs-union-disjoint,
junkref-def,
|
| junkrefs-newref | proved | all subs proved
| junkrefs-notin,
|
| junkrefs-newref-04 | proved | all subs proved
| junkrefs-newref-01,
junkref-newref,
|
| junkrefs-notin-03 | proved | all subs proved
| junkrefs-notin,
|
| validref-addobj-this | proved | all subs proved
| junkref-addobj-01,
validref-def,
|
| validref-put-badarrayfield | proved | all subs proved
| junkref-put-badarrayfield,
validref-def,
|
| validref-put-badclassfield | proved | all subs proved
| junkref-put-badclassfield,
validref-def,
|
| validref-put-null | proved | all subs proved
| junkref-put-null,
validref-def,
|
| validrefkeynotnull-put-shortval | proved | all subs proved
| validrefnotnull-put-shortval,
validrefnotnull-notnull,
validrefvalnotnull-def,
validrefkeynotnull-in,
validrefkeynotnull-def,
|
| validrefkeynotnull-subset | proved | all subs proved
| junkref-subset,
junkref-keyin,
validref-def,
validrefnotnull-def,
validrefnotnull-notnull,
validrefvalnotnull-def,
validrefkeynotnull-def,
|
| validrefnotnull-junk | proved | all subs proved
| validref-junkref,
validrefnotnull-def,
|
| junkref-addarray-noreftype | proved | all subs proved
| junkrefs-addarray-noreftype,
junkref-def,
|
| junkrefs-runtimetype | proved | all subs proved
| junkrefs-supertype,
junkrefs-null-02,
junkrefs-is-junk,
|
| junkref-not-okreftype | proved | all subs proved
| junkref-null,
junkref-is-junk,
|
| junkref-put-refval-statfield | proved | all subs proved
| junkrefs-sametype,
junkrefs-null-02,
junkrefs-put-statfield,
junkrefs-put-refval-statfield,
junkref-def,
|
| junkrefs-union-disjoint | proved | all subs proved
| junkrefs-array,
junkrefs-null-02,
junkrefs-notin-01,
junkrefs-class,
junkrefs-is-junk,
junkrefs-null,
junkrefs-one,
|
| levelsubset-is-array | proved | all subs proved
| levelsubset-typeex,
|
| levelsubset-is-obj | proved | all subs proved
| levelsubset-classex,
|
| junkrefs-notin | proved | all subs proved
| junkrefs-array,
junkrefs-class,
junkrefs-null-02,
junkrefs-is-junk,
junkrefs-notin-02,
junkrefs-notin-01,
|
| junkref-okbytearray | proved | all subs proved
| junkref-is-junk,
|
| junkref-addarray-newref | proved | all subs proved
| junkrefs-addarray,
junkrefs-newref-03,
junkref-def,
|
| junkref-addarray-02 | proved | all subs proved
| junkref-subset,
|
| junkref-addobj | proved | all subs proved
| junkrefs-sametype,
junkrefs-newref-03,
junkrefs-addobj,
junkref-def,
|
| junkref-not-valid-01 | proved | all subs proved
| junkref-is-junk,
|
| junkref-newref | proved | all subs proved
| junkrefs-newref-01,
junkref-def,
|
| validref-array-len-in | proved | all subs proved
| junkref-is-junk,
validref-def,
|
| junkref-noreftype | proved | all subs proved
| junkref-is-junk,
|
| junkref-put-array-norefval | proved | all subs proved
| junkrefs-put-array-norefval,
junkref-def,
|
| junkref-put-badarrayfield | proved | all subs proved
| junkrefs-put-badarrayfield,
junkref-def,
|
| junkref-put-badarrayindex | proved | all subs proved
| junkrefs-junkref,
junkrefs-put-badarrayindex,
junkref-def,
|
| junkref-put-badclassfield | proved | all subs proved
| junkrefs-put-badclassfield,
junkref-def,
|
| junkref-put-badfield | proved | all subs proved
| junkrefs-junkref,
junkrefs-sametype,
junkrefs-null-02,
junkrefs-is-junk,
junkrefs-put-badfield,
junkref-def,
|
| junkref-put-norefval | proved | all subs proved
| junkrefs-put-norefval,
junkref-def,
|
| junkref-put-norefval-equiv | proved | all subs proved
| junkrefs-put-norefval-equiv,
junkref-def,
junkref-put-norefval-01,
|
| junkref-put-null | proved | all subs proved
| junkrefs-junkref,
junkrefs-put-null-01,
junkref-def,
|
| nojunkref-typeex | proved | all subs proved
| junkref-is-junk,
|
| validrefnotnull-put-shortval | proved | all subs proved
| junkref-put-norefval-01,
validref-def,
validrefnotnull-def,
validrefnotnull-notnull,
|
| junkref-union | proved | all subs proved
| junkref-subset,
|
| junkref-keyin | proved | all subs proved
| junkref-is-junk,
junkref-null,
|
| validstatfield-level-expand | proved | all subs proved
| validstatfields-class-01,
validstatfields-validstatfield,
|
| junkref-notin | proved | all subs proved
| junkref-is-junk,
junkref-null,
|
| junkref-addobj-01 | proved | all subs proved
| junkrefs-array,
junkrefs-sametype,
junkrefs-null-02,
junkref-is-junk,
junkrefs-addobj,
junkrefs-class,
junkref-def,
|
| validref-junkref | proved | all subs proved
| junkref-null,
validref-def,
|
| validrefkeynotnull-has-field | proved | all subs proved
| junkref-is-junk,
validref-def,
validrefnotnull-def,
validrefnotnull-notnull,
validrefvalnotnull-def,
validrefkeynotnull-def,
|
| validref-type-forward-01 | proved | all subs proved
| validref-type-forward,
|
| validref-subtype-01 | proved | all subs proved
| validref-subtype,
|
| validref-put-shortval | proved | all subs proved
| junkref-put-norefval-01,
validref-def,
|
| validref-okreftype | proved | all subs proved
| junkref-is-junk,
junkref-null,
validref-def,
|
| validref-object | proved | all subs proved
| junkref-is-junk,
validref-def,
|
| validref-isobj | proved | all subs proved
| junkref-is-junk,
validref-def,
|
| validmode-put-nonnull-01 | proved | all subs proved
| validmode,
validmode-put-nonnull,
|
| same-subclasses-tdnameex-03 | proved | all subs proved
| same-subclasses-tdnameex-01,
|
| same-subclasses-tdnameex | proved | all subs proved
| same-subclasses-tdnameex-01,
|
| junkrefs-subclass | proved | all subs proved
| junkrefs-is-junk,
junkrefs-sametype,
junkrefs-null,
|
| junkrefs-sametype-01 | proved | all subs proved
| junkrefs-supertype,
|
| junkrefs-bytearray | proved | all subs proved
| junkrefs-primarray,
|
| junkref-voidarray | proved | all subs proved
| junkref-is-junk,
|
| junkref-void | proved | all subs proved
| junkref-is-junk,
|
| junkref-tdnameex | proved | all subs proved
| junkref-is-junk,
junkref-null,
|
| junkref-primarray-level | proved | all subs proved
| junkref-primarray-level-01,
|
| junkref-not-valid | proved | all subs proved
| junkref-is-junk,
|
| junkref-not-is-array | proved | all subs proved
| junkref-is-junk,
junkref-null,
|
| junkref-is_array | proved | all subs proved
| junkref-is-junk,
junkref-null,
|
| junkref-classtype | proved | all subs proved
| junkref-is-junk,
|
| junkref-bad-type | proved | all subs proved
| junkref-is-junk,
junkref-null,
|
| junkref-addarray-01 | proved | all subs proved
| junkrefs-sametype,
junkrefs-addarray,
junkrefs-null-02,
junkrefs-array,
junkref-def,
|
| junkref-abstract | proved | all subs proved
| junkref-is-junk,
|
| is_valid_ref-levelsubset | proved | all subs proved
| levelsubset-typeex,
levelsubset-classex,
|
| validvals-voidtype-02 | proved | all subs proved
| validvals-voidtype,
|
| validstatfields-void | proved | all subs proved
| validstatfield-void,
validstatfields-storekeys-def,
|
| validvals-voidtype-01 | proved | all subs proved
| validvals-voidtype,
|
| validstatfields-class-01 | proved | all subs proved
| validstatfield-void,
validstatfield-index,
validfield-one,
validstatfield-storekey-def,
validfieldlist-def-01,
validstatfields-class,
|
| validrefnotnull-validref | proved | all subs proved
| validrefnotnull-def,
validrefnotnull-notnull,
|
| validrefkeynotnull-notnull | proved | all subs proved
| validrefnotnull-notnull,
validrefvalnotnull-def,
validrefkeynotnull-def,
|
| validref-subtype | proved | all subs proved
| validref-null,
validref-def,
|
| validref-type-forward | proved | all subs proved
| validref-null,
validref-def,
|
| validmode-put-nonnull | proved | all subs proved
| validmode,
|
| same-subclasses-tdnameex-01 | proved | all subs proved
| same-subclasses-tdnameex-02,
|
| junkrefs-supertype | proved | all subs proved
| junkrefs-array,
junkrefs-class,
junkrefs-is-junk,
junkrefs-null,
junkrefs-one,
|
| junkrefs-put-notin | proved | all subs proved
| junkrefs-array,
junkrefs-class,
junkrefs-is-junk,
junkrefs-null-02,
junkrefs-empty,
|
| junkrefs-notin-01 | proved | all subs proved
| junkrefs-is-junk,
junkrefs-null-02,
|
| junkrefs-notin-02 | proved | all subs proved
| junkrefs-one,
|
| junkrefs-primarray | proved | all subs proved
| junkrefs-array,
junkrefs-null-02,
junkrefs-is-junk,
|
| junkrefs-put-null-02 | proved | all subs proved
| junkrefs-null-02,
junkrefs-array,
junkrefs-class,
junkrefs-is-junk,
junkrefs-null,
junkrefs-empty,
|
| junkrefs-put-null-01 | proved | all subs proved
| junkrefs-array,
junkrefs-null-02,
junkrefs-class,
junkrefs-is-junk,
junkrefs-null,
junkrefs-empty,
|
| junkref-put-norefval-01 | proved | all subs proved
| junkrefs-put-norefval-01,
junkref-def,
|
| junkrefs-put-norefval-equiv | proved | all subs proved
| junkrefs-array,
junkrefs-class,
junkrefs-null-02,
junkrefs-is-junk,
junkrefs-empty,
junkrefs-put-norefval-01,
|
| junkrefs-put-norefval | proved | all subs proved
| junkrefs-put-norefval-01,
|
| junkrefs-put-badfield | proved | all subs proved
| junkrefs-array,
junkrefs-class,
junkrefs-null-02,
junkrefs-is-junk,
junkrefs-empty,
|
| junkrefs-put-badclassfield | proved | all subs proved
| junkrefs-array,
junkrefs-class,
junkrefs-null-02,
junkrefs-is-junk,
junkrefs-empty,
|
| junkrefs-put-badarrayindex | proved | all subs proved
| junkrefs-array,
junkrefs-class,
junkrefs-null-02,
junkrefs-is-junk,
junkrefs-empty,
|
| junkrefs-put-badarrayfield | proved | all subs proved
| junkrefs-array,
junkrefs-class,
junkrefs-null-02,
junkrefs-is-junk,
junkrefs-empty,
|
| junkrefs-put-array-norefval | proved | all subs proved
| junkrefs-array,
junkrefs-class,
junkrefs-null-02,
junkrefs-is-junk,
junkrefs-empty,
|
| junkref-primarray-level-01 | proved | all subs proved
| junkrefs-array,
junkrefs-null-02,
junkrefs-is-junk,
junkref-def,
|
| junkrefs-newref-01 | proved | all subs proved
| junkrefs-one,
|
| junkrefs-addarray-noreftype | proved | all subs proved
| junkrefs-null-02,
junkrefs-array,
|
| junkrefs-newref-03 | proved | all subs proved
| junkrefs-newref-02,
|
| junkref-subset | proved | all subs proved
| junkrefs-subset,
junkrefs-typein,
junkrefs-null-02,
junkref-def,
|
| junkrefs-sametype | proved | all subs proved
| junkrefs-subtype,
junkrefs-is-junk,
|
| junkref-null | proved | all subs proved
| junkrefs-null-02,
junkref-def,
|
| junkref-is-junk | proved | all subs proved
| junkrefs-one,
junkref-def,
|
| levelsubset-classex | proved | all subs proved
| levelsubset-classex-01,
|
| levelsubset-typeex | proved | all subs proved
| levelsubset-all-types,
|
| initsubset-init | proved | all subs proved
| initsubset-initdone-forward,
|
| initsubset-init-forward | proved | all subs proved
| initsubset-initdone-forward,
|
| initsubset-validstatfields-forward | proved | all subs proved
| initsubset-validstatfield-forward,
validstatfields-storekeys-def,
|
| junkref-isarray-typeex | proved | all subs proved
| junkrefs-one,
junkrefs-is-junk,
junkrefs-array,
junkref-def,
|
| junkref-primarray-lvl | proved | all subs proved
| junkrefs-array,
junkrefs-null-02,
junkrefs-is-junk,
junkref-def,
|
| junkrefs-append | proved | all subs proved
| junkrefs-array,
junkrefs-class,
junkrefs-null-02,
junkrefs-is-junk,
junkrefs-empty,
|
| junkrefs-delete-01 | proved | all subs proved
| junkrefs-delete,
|
| junkrefs-delete-02 | proved | all subs proved
| junkrefs-array,
junkrefs-class,
junkrefs-null-02,
junkrefs-is-junk,
junkrefs-empty,
|
| junkrefs-null-01 | proved | all subs proved
| junkrefs-array,
junkrefs-class,
junkrefs-is-junk,
junkrefs-empty,
junkrefs-null-02,
|
| junkrefs-null-03 | proved | all subs proved
| junkrefs-null-02,
|
| junkrefs-put-notin-butlast | proved | all subs proved
| junkrefs-array,
junkrefs-class,
junkrefs-null-02,
junkrefs-is-junk,
junkrefs-one,
|
| junkrefs-put-null | proved | all subs proved
| junkrefs-array,
junkrefs-null-02,
junkrefs-class,
junkrefs-is-junk,
junkrefs-null,
junkrefs-empty,
|
| same-subclasses-is-obj | proved | all subs proved
| same-subclasses-classex,
|
| same-subclasses-tdnameex-04 | proved | all subs proved
| same-subclasses-interfaceex,
same-subclasses-classex-01,
|
| same-subclasses-tdnameex-05 | proved | all subs proved
| same-subclasses-tdnameex-02,
|
| validmode-addobj | proved | all subs proved
| validref-null,
validmodeval-def,
validmode-def,
|
| validmode-noval-put-01 | proved | all subs proved
| validmode-noval-put,
|
| validref-isvalidref | proved | all subs proved
| validref-array-03,
|
| validref-not-junkrefs | proved | all subs proved
| junkrefs-subtype,
junkref-def,
junkrefs-null-02,
validref-def,
|
| validrefkeynotnull-union-same-02 | proved | all subs proved
| validrefkeynotnull-union-same-01,
|
| validreflist-one-01 | proved | all subs proved
| validreflist-one,
|
| validreflist-rec-01 | proved | all subs proved
| validreflist-rec,
|
| validrefnotnull | proved | all subs proved
| validrefnotnull-not,
validrefnotnull-null,
|
| validrefnotnull-isvalidref | proved | all subs proved
| validref-array-03,
validrefnotnull-def,
validrefnotnull-notnull,
|
| validstatfield-validref | proved | all subs proved
| validrefval-ref,
validval-def,
validfield-one,
validstatfield-storekey-def,
validref-null,
|
| validstatfields-empty-01 | proved | all subs proved
| validfieldlist-empty,
validstatfields-def,
|
| validval-field-byteval | proved | all subs proved
| validval-field-norefval,
|
| validval-field-shortval | proved | all subs proved
| validval-field-norefval,
|
| validval-index-byteval | proved | all subs proved
| validval-index-norefval,
|
| validval-null | proved | all subs proved
| validref-null,
validrefval-ref,
validval-def,
|
| validvals-append-01 | proved | all subs proved
| validvals-append,
|
| initsubset-initdone-forward | proved | all subs proved
| initsubset-def,
|
| initsubset-trans | proved | all subs proved
| validstatfields-storekeys-def,
initsubset-def,
|
| initsubset-validstatfield-forward | proved | all subs proved
| validstatfields-storekeys-def,
validstatfield-storekey-def,
initsubset-def,
|
| junkrefs-addobj | proved | all subs proved
| junkrefs-array,
junkrefs-class,
junkrefs-is-junk,
junkrefs-null,
junkrefs-empty,
|
| junkrefs-junkref | proved | all subs proved
| junkref-def,
|
| junkrefs-put-refval-statfield | proved | all subs proved
| junkrefs-array,
junkrefs-class,
junkrefs-is-junk,
junkrefs-null,
junkrefs-empty,
|
| junkrefs-put-statfield | proved | all subs proved
| junkrefs-array,
junkrefs-class,
junkrefs-is-junk,
junkrefs-null,
junkrefs-empty,
|
| junkrefs-subset | proved | all subs proved
| junkrefs-array,
junkrefs-class,
junkrefs-is-junk,
junkrefs-null,
junkrefs-empty,
|
| junkrefs-typein | proved | all subs proved
| junkrefs-is-junk,
|
| junkrefs-addarray | proved | all subs proved
| junkrefs-array,
junkrefs-class,
junkrefs-is-junk,
junkrefs-null,
junkrefs-empty,
|
| junkrefs-delete | proved | all subs proved
| junkrefs-class,
junkrefs-array,
junkrefs-is-junk,
junkrefs-null,
junkrefs-empty,
|
| junkrefs-newref-02 | proved | all subs proved
| junkrefs-is-junk,
|
| junkrefs-put-norefval-01 | proved | all subs proved
| junkrefs-array,
junkrefs-class,
junkrefs-is-junk,
junkrefs-null,
junkrefs-empty,
|
| junkrefs-one | proved | all subs proved
| junkrefs-array,
junkrefs-class,
junkrefs-is-junk,
junkrefs-null,
|
| levelsubset-classex-01 | proved | all subs proved
| levelsubset-def,
|
| levelsubset-all-types | proved | all subs proved
| levelsubset-def,
|
| same-subclasses-classex | proved | all subs proved
| same-subclasses-one-def,
|
| same-subclasses-interfaceex | proved | all subs proved
| same-subclasses-one-def,
|
| same-subclasses-classex-01 | proved | all subs proved
| same-subclasses-one-def,
|
| same-subclasses-tdnameex-02 | proved | all subs proved
| same-subclasses-one-def,
|
| junkreflist-rec | proved | all subs proved
| junkreflist-def,
|
| junkreflist-empty | proved | all subs proved
| junkreflist-def,
|
| validfieldinits-rec | proved | all subs proved
| validfieldinits-def,
|
| validfieldinits-empty | proved | all subs proved
| validfieldinits-def,
|
| validfieldlist-rec | proved | all subs proved
| validfieldlist-def-01,
|
| validmode-noval-put | proved | all subs proved
| validmodeval-def,
validmode-def,
|
| validmode | proved | all subs proved
| validmodeval-def,
validmode-def,
|
| junkrefs-subtype | proved | all subs proved
| junkrefs-array,
junkrefs-class,
junkrefs-is-junk,
junkrefs-null,
junkrefs-empty,
|
| junkrefs-null-02 | proved | all subs proved
| junkrefs-null,
|
| validrefkeynotnull-in | proved | all subs proved
| validrefkeynotnull-def,
|
| validrefkeynotnull-union-same-01 | proved | all subs proved
| validrefkeynotnull-def,
|
| validreflist-empty | proved | all subs proved
| validreflist-def,
|
| validreflist-one | proved | all subs proved
| validreflist-def,
|
| validreflist-rec | proved | all subs proved
| validreflist-def,
|
| validrefnotnull-not | proved | all subs proved
| validrefnotnull-def,
|
| validrefnotnull-null | proved | all subs proved
| validrefnotnull-def,
|
| validref-array-03 | proved | all subs proved
| validref-def,
|
| validrefnotnull-notnull | proved | all subs proved
| validrefnotnull-def,
|
| validstatfields-validstatfield | proved | all subs proved
| validstatfields-class,
validstatfields-def,
|
| levelsubset-tdnameex | proved | all subs proved
| levelsubset-def,
|
| validvals-one | proved | all subs proved
| validrefkeyvalues-def,
|
| validfield-one | proved | all subs proved
| validval-def,
validfield-def,
|
| validfieldlist-empty | proved | all subs proved
| validfieldlist-def-01,
|
| validstatfields-empty | proved | all subs proved
| validstatfields-storekeys-def,
|
| validstatfield-index | proved | all subs proved
| validstatfield-storekey-def,
|
| validstatfields-rec | proved | all subs proved
| validstatfields-storekeys-def,
|
| validstatfields-initundone | proved | all subs proved
| validstatfield-storekey-def,
validstatfields-storekeys-def,
|
| validstatfield-void | proved | all subs proved
| validstatfield-storekey-def,
|
| validval-index-norefval | proved | all subs proved
| validval-def,
validrefkeyval-def,
|
| validval-field-norefval | proved | all subs proved
| validval-def,
validrefkeyval-def,
|
| validref-null | proved | all subs proved
| validref-def,
|
| validrefval-ref | proved | all subs proved
| validrefval-def,
|
| validvals-append | proved | all subs proved
| validrefkeyvalues-def,
|
| validvals-voidtype | proved | all subs proved
| validrefkeyval-def,
validrefkeyvalues-def,
|
| validval-int | proved | all subs proved
| validval-def,
|
| validsubset-validref-forward | proved | all subs proved
| validsubset-def,
|
| validsubset-same | proved | all subs proved
| validsubset-def,
|
| validstatfields-one | proved | all subs proved
| validstatfields-storekeys-def,
|
| validstatfield-putbytearray-noreftype | proved | all subs proved
| validfield-def,
validstatfield-storekey-def,
|
| validstatfield-put-statfield-int | proved | all subs proved
| validfield-def,
validstatfield-storekey-def,
|
| validstatfield-primtype-level | proved | all subs proved
| validfield-def,
validstatfield-storekey-def,
|
| validstatfield-other-statfield | proved | all subs proved
| validstatfield-storekey-def,
|
| validrefkeynotnull-validrefnotnull | proved | all subs proved
| validrefvalnotnull-def,
validrefkeynotnull-def,
|
| validrefkeynotnull-union-same | proved | all subs proved
| validrefkeynotnull-def,
|
| validrefkeynotnull-statfield-intersect | proved | all subs proved
| validrefnotnull-def,
validrefvalnotnull-def,
validrefkeynotnull-def,
|
| validrefkeynotnull-no-newrefs | proved | all subs proved
| validrefkeynotnull-def,
|
| validref-subtype-02 | proved | all subs proved
| validref-def,
|
| validref-arraytype | proved | all subs proved
| validref-def,
|
| validmode-01 | proved | all subs proved
| validmode-def,
|
| validfieldlist-one-01 | proved | all subs proved
| validfieldlist-def-01,
|
| validfieldinits-one | proved | all subs proved
| validfieldinits-def,
|
| same-subclasses-typeex | proved | all subs proved
| same-subclasses-one-def,
|
| same-subclasses-trans | proved | all subs proved
| same-subclasses-one-def,
|
| same-subclasses-subclass | proved | all subs proved
| same-subclasses-one-def,
|
| same-subclasses-ref | proved | all subs proved
| same-subclasses-one-def,
|
| same-subclasses-is-array | proved | all subs proved
| same-subclasses-one-def,
|
| same-subclasses-interfaceex-01 | proved | all subs proved
| same-subclasses-one-def,
|
| same-subclasses-classex-02 | proved | all subs proved
| same-subclasses-one-def,
|
| levelsubset-trans | proved | all subs proved
| levelsubset-def,
|
| levelsubset-ref | proved | all subs proved
| levelsubset-def,
|
| levelsubset-classex-03 | proved | all subs proved
| levelsubset-def,
|
| levelsubset-classex-02 | proved | all subs proved
| levelsubset-def,
|
| junkrefs-union | proved | all subs proved
| junkrefs-array,
junkrefs-class,
junkrefs-is-junk,
junkrefs-null,
junkrefs-empty,
|
| junkrefs-inttype | proved | all subs proved
| junkrefs-is-junk,
|
| junkrefs-empty-01 | proved | all subs proved
| junkrefs-empty,
|
| initsubset-same | proved | all subs proved
| initsubset-def,
|
| validrefkeyvalues-def | axiom | | |
| validsubset-def | axiom | | |
| validstatfields-def | axiom | | |
| validstatfields-class | axiom | | |
| validrefkeyval-def | axiom | | |
| validmode-def | axiom | | |
| validmodeval-def | axiom | | |
| validfieldlist-def-01 | axiom | | |
| validfieldinits-def | axiom | | |
| validval-def | axiom | | |
| same-subclasses-one-def | axiom | | |
| validrefnotnull-def | axiom | | |
| validrefkeynotnull-def | axiom | | |
| validrefvalnotnull-def | axiom | | |
| levelsubset-def | axiom | | |
| junkrefs-empty | axiom | | |
| junkreflist-def | axiom | | |
| junkrefs-null | axiom | | |
| junkrefs-is-junk | axiom | | |
| junkrefs-class | axiom | | |
| validreflist-def | axiom | | |
| validref-def | axiom | | |
| junkref-def | axiom | | |
| junkrefs-array | axiom | | |
| validstatfields-storekeys-def | axiom | | |
| validfield-def | axiom | | |
| validrefval-def | axiom | | |
| validstatfield-storekey-def | axiom | | |
| initsubset-def | axiom | | |