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-subspec-samesubclasses | proved | all subs proved
| validref-subspec-samesubclasses-01,
|
| validref-subspec-samesubclasses-01 | proved | all subs proved
| same-subclasses-subclass,
junkref-subspec-samesubclasses,
|
| same-subclasses-contains-trans | proved | all subs proved
| contains-typeex-02,
same-subclasses-contains-tdnameex,
contains-subspec-better,
same-subclasses-all-def,
|
| validref-subspec-samesubclasses | proved | all subs proved
| same-subclasses-subclass,
contains-typeex-02,
contains-supertype-04,
same-subclasses-all-def,
junkref-subspec-samesubclasses,
|
| contains-subspec-better | proved | all subs proved
| contains-array-elemtype-06,
contains-type-def,
same-subclasses-forward,
contains-not-hasclasstype-level-01,
same-subclasses-contains-typeex-02,
same-subclasses-all-def,
contains-type-rec,
contains-one,
contains-rec-01,
same-subclasses-contains-typeex-01,
contains-typeex-05,
contains-typeex,
same-subclasses-contains-typeex,
contains-type-def-nodups,
|
| junkref-subspec-samesubclasses | proved | all subs proved
| same-subclasses-array-forward,
same-subclasses-is-array,
same-subclasses-class-forward,
same-subclasses-is-obj,
|
| contains-subspec | proved | all subs proved
| contains-type-def,
contains-typeex-02,
contains-typeex,
same-subclasses-forward,
contains-not-hasclasstype-level-01,
contains-type-rec,
contains-one,
contains-rec-01,
contains-type-def-nodups,
|
| same-subclasses-array-forward | proved | all subs proved
| contains-typeex-03,
contains-type-rec,
contains-typeex-02,
contains-supertype-04,
contains-array-elemtype-06,
contains-trans,
same-subclasses-all-def,
|
| same-subclasses-contains-typeex-01 | proved | all subs proved
| contains-array-elemtype-06,
contains-not-has-classtype-01,
contains-typeex-03,
same-subclasses-all-def,
|
| same-subclasses-forward | proved | all subs proved
| contains-type-rec,
contains-supertype-04,
contains-array-elemtype-06,
contains-trans,
contains-not-has-classtype-01,
same-subclasses-all-def,
|
| contains-array-elemtype-06 | proved | all subs proved
| contains-array-elemtype-01,
contains-array-elemtype-11,
contains-array-elemtype-08,
contains-array-elemtype-07,
|
| contains-not-has-classtype-01 | proved | all subs proved
| contains-no-reftype,
contains-array-elemtype-08,
|
| contains-array-elemtype-07 | proved | all subs proved
| contains-array-elemtype,
contains-array-elemtype-09,
contains-array-elemtype-08,
|
| contains-array-elemtype-11 | proved | all subs proved
| contains-array-elemtype-08,
contains-array-elemtype-05,
|
| contains-objectarray | proved | all subs proved
| contains-type-rec,
contains-array-elemtype-02,
contains-array-elemtype-08,
contains-typeex-03,
|
| contains-array-elemtype-08 | proved | all subs proved
| contains-array-elemtype-09,
contains-array-elemtype-10,
contains-supertype-04,
contains-type-rec,
contains-typeex-02,
contains-typeex-03,
|
| same-subclasses | proved | all subs proved
| contains-array-elemtype-01,
same-subclasses-01,
|
| junkref-put-other-fieldclass | proved | all subs proved
| nopathex-badarrayfield,
nopathex-badclassfield,
|
| same-subclasses-01 | proved | all subs proved
| contains-array-elemtype-ex,
contains-array-elemtype-04,
contains-typeex-03,
contains-typeex,
contains-trans,
contains-typeex-05,
contains-rec-01,
contains-type-rec,
same-subclasses-all-def,
contains-two,
contains-type-def,
|
| same-subclasses-class-forward | proved | all subs proved
| contains-type-rec,
contains-array-elemtype,
contains-array-elemtype-01,
contains-trans,
same-subclasses-all-def,
|
| nopathex-badarrayfield | proved | all subs proved
| contains-typeex,
contains-field-def,
contains-type-def,
contains-typeex-03,
validrefs-not-contains,
contains-length,
|
| contains-array-elemtype-05 | proved | all subs proved
| contains-array-elemtype-ex,
contains-type-def,
|
| contains-array-elemtype-09 | proved | all subs proved
| contains-typeex-03,
contains-type-rec,
|
| contains-bytearray-04 | proved | all subs proved
| contains-array-elemtype-04,
contains-primtype,
contains-type-rec,
|
| contains-subex | proved | all subs proved
| contains-array-elemtype-01,
|
| contains-supertype-05 | proved | all subs proved
| contains-supertype-02,
|
| contains-primtype | proved | all subs proved
| contains-no-reftype,
|
| contains-supertype-02 | proved | all subs proved
| contains-supertype-04,
contains-field-def-case,
|
| contains-array-elemtype-ex | proved | all subs proved
| contains-supertype,
contains-rec,
contains-typeex,
contains-typeex-05,
contains-rec-01,
contains-two,
|
| contains-array-elemtype-01 | proved | all subs proved
| contains-array-elemtype,
|
| contains-typeex-03 | proved | all subs proved
| contains-typeex-05,
contains-type-def,
|
| same-subclasses-subclass | proved | all subs proved
| contains-supertype-04,
same-subclasses-all-def,
|
| contains-supertype-03 | proved | all subs proved
| contains-supertype-04,
|
| contains-subtype-01 | proved | all subs proved
| contains-subtype,
|
| contains-shortarray-03 | proved | all subs proved
| contains-shortarray-02,
contains-shortarray,
contains-type-def,
|
| contains-primtype-03 | proved | all subs proved
| contains-no-reftype,
|
| contains-primtype-02 | proved | all subs proved
| contains-no-reftype,
|
| contains-primtype-01 | proved | all subs proved
| contains-no-reftype,
|
| contains-not-hasclasstype-level | proved | all subs proved
| contains-not-hasclasstype-level-01,
|
| contains-not-has-classtype | proved | all subs proved
| contains-type-rec,
contains-no-reftype,
|
| contains-intarray-03 | proved | all subs proved
| contains-intarray-02,
contains-intarray,
contains-type-def,
|
| contains-bytearray-03 | proved | all subs proved
| contains-bytearray-02,
contains-bytearray,
contains-type-def,
|
| contains-boolarray-03 | proved | all subs proved
| contains-boolarray-02,
contains-boolarray,
contains-type-def,
|
| contains-trans | proved | all subs proved
| contains-trans-01,
contains-type-def,
contains-type-def-nodups,
|
| nopathex-badclassfield | proved | all subs proved
| contains-type-def,
contains-typeex-02,
contains-one,
contains-field-def,
nopathex-runtimetype,
|
| contains-subtype | proved | all subs proved
| contains-rec,
contains-rec-01,
contains-two,
contains-type-def-nodups,
|
| contains-shortarray-02 | proved | all subs proved
| contains-shortarray-01,
|
| contains-array-elemtype-02 | proved | all subs proved
| contains-typeex-02,
contains-type-rec,
|
| contains-not-hasclasstype-level-01 | proved | all subs proved
| contains-one,
contains-rec-01,
contains-type-def-nodups,
|
| contains-no-reftype | proved | all subs proved
| contains-type-rec,
|
| contains-intarray-02 | proved | all subs proved
| contains-intarray-01,
|
| contains-array-elemtype-04 | proved | all subs proved
| contains-type-rec,
|
| contains-bytearray-02 | proved | all subs proved
| contains-bytearray-01,
|
| contains-boolarray-02 | proved | all subs proved
| contains-boolarray-01,
|
| contains-typeex-05 | proved | all subs proved
| contains-typeex-04,
|
| contains-supertype-04 | proved | all subs proved
| contains-type-rec,
|
| contains-array-elemtype-10 | proved | all subs proved
| contains-typeex-02,
contains-type-rec,
|
| contains-array-elemtype | proved | all subs proved
| contains-rec-01,
contains-rec,
contains-two,
contains-type-def,
contains-type-def-nodups,
|
| contains-levelsubset | proved | all subs proved
| contains-type-rec,
contains-one,
contains-rec-01,
contains-type-def-nodups,
|
| contains-predefined | proved | all subs proved
| contains-type-rec,
|
| contains-boolarray-01 | proved | all subs proved
| contains-one,
contains-bool,
contains-rec-01,
|
| contains-boolarray | proved | all subs proved
| contains-one,
contains-bool,
contains-rec-01,
|
| contains-bytearray-01 | proved | all subs proved
| contains-byte,
contains-one,
contains-rec-01,
|
| contains-bytearray | proved | all subs proved
| contains-byte,
contains-one,
contains-rec-01,
|
| contains-intarray-01 | proved | all subs proved
| contains-one,
contains-int,
contains-rec-01,
|
| contains-intarray | proved | all subs proved
| contains-one,
contains-int,
contains-rec-01,
|
| contains-shortarray-01 | proved | all subs proved
| contains-one,
contains-short,
contains-rec-01,
|
| contains-shortarray | proved | all subs proved
| contains-one,
contains-short,
contains-rec-01,
|
| same-subclasses-contains-typeex-02 | proved | all subs proved
| same-subclasses-all-def,
same-subclasses-contains-tdnameex-03,
|
| same-subclasses-contains-typeex | proved | all subs proved
| same-subclasses-contains-tdnameex,
|
| contains-type-def-nodups | proved | all subs proved
| contains-rec,
contains-append,
contains-rec-01,
contains-type-def,
|
| contains-typeex-04 | proved | all subs proved
| contains-one,
contains-rec-01,
contains-typeex,
|
| nopathex-runtimetype | proved | all subs proved
| validrefs-not-contains,
|
| contains-type-rec | proved | all subs proved
| contains-rec,
contains-rec-01,
contains-two,
contains-typeex,
contains-type-def,
|
| contains-typeex-02 | proved | all subs proved
| contains-typeex,
contains-type-def,
|
| contains-supertype-01 | proved | all subs proved
| contains-supertype,
|
| contains-array | proved | all subs proved
| contains-supertype,
contains-rec,
|
| same-subclasses-contains-tdnameex-03 | proved | all subs proved
| same-subclasses-contains-tdnameex-02,
|
| same-subclasses-contains-tdnameex | proved | all subs proved
| same-subclasses-contains-tdnameex-01,
|
| validrefs-not-contains | proved | all subs proved
| contains-rec,
contains-two,
contains-type-def,
|
| contains-append | proved | all subs proved
| contains-rec-01,
contains-one,
|
| contains-trans-01 | proved | all subs proved
| contains-rec,
contains-rec-01,
|
| contains-field-def-case | proved | all subs proved
| contains-rec,
contains-two,
contains-rec-01,
contains-type-def,
contains-one,
contains-field-def,
|
| contains-short | proved | all subs proved
| contains-rec-01,
contains-one,
|
| contains-int | proved | all subs proved
| contains-rec-01,
contains-one,
|
| contains-byte | proved | all subs proved
| contains-rec-01,
contains-one,
|
| contains-bool | proved | all subs proved
| contains-rec-01,
contains-one,
|
| contains-typeex | proved | all subs proved
| contains-one,
contains-rec-01,
|
| contains-supertype | proved | all subs proved
| contains-rec,
contains-one,
contains-rec-01,
|
| contains-primtype-04 | proved | all subs proved
| contains-rec-01,
contains-one,
|
| contains-primtype-05 | proved | all subs proved
| contains-one,
contains-rec-01,
|
| contains-typeex-01 | proved | all subs proved
| contains-one,
contains-rec-01,
|
| same-subclasses-is-array | proved | all subs proved
| same-subclasses-all-def,
|
| same-subclasses-is-obj | proved | all subs proved
| same-subclasses-all-def,
|
| contains-length | proved | all subs proved
| contains-one,
contains-field-def,
|
| contains-rec-01 | proved | all subs proved
| contains-rec,
|
| same-subclasses-contains-tdnameex-01 | proved | all subs proved
| same-subclasses-all-def,
|
| same-subclasses-contains-tdnameex-02 | proved | all subs proved
| same-subclasses-all-def,
|
| contains-two | proved | all subs proved
| contains-one,
contains-rec,
|
| same-subclasses-all-def | axiom | | |
| contains-field-def | axiom | | |
| contains-type-def | axiom | | |
| contains-rec | axiom | | |
| contains-one | axiom | | |